filename.txt

(define-fun |220.220.221.-1| () Address
  (ip_constructor 220 220 221 (- 1)))
(define-fun |\|1.0.0.6\|_auto_src_2| () Address
  (ip_constructor 165 165 167 (- 1)))
(define-fun |\|1.0.0.6\|_auto_dst_3| () Address
  (ip_constructor 0 0 0 0))
(define-fun |\|1.0.0.3\|_auto_dst_0| () Address
  (ip_constructor 220 220 (- 1) (- 1)))
(define-fun |\|1.0.0.9\|_auto_dst_4| () Address
  (ip_constructor 202 0 0 (- 1)))
(define-fun |\|1.0.0.9\|_auto_dstp_3| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.7\|_auto_dst_2| () Address
  (ip_constructor (- 1) (- 1) (- 1) (- 1)))
(define-fun |\|1.0.0.2\|_auto_dstp_1| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.5\|_auto_src_2| () Address
  (ip_constructor 0 0 0 0))
(define-fun |\|1.0.0.10\|_auto_src_0| () Address
  (ip_constructor 17 56 (- 1) (- 1)))
(define-fun |\|1.0.0.8\|_auto_dst_1| () Address
  (ip_constructor 94 142 249 (- 1)))
(define-fun |\|1.0.0.5\|_auto_srcp_1| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.6\|_auto_src_1| () Address
  (ip_constructor 220 220 222 (- 1)))
(define-fun |\|1.0.0.4\|_auto_src_1| () Address
  (ip_constructor 0 0 0 0))
(define-fun |\|1.0.0.6\|_auto_proto_0| () Int
  0)
(define-fun |\|1.0.0.6\|_auto_dstp_0| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.6\|_auto_src_3| () Address
  (ip_constructor 0 0 0 0))
(define-fun |\|1.0.0.01\|_auto_src_3| () Address
  (ip_constructor 204 0 0 2))
(define-fun |94.142.251.1| () Address
  (ip_constructor 94 142 251 1))
(define-fun |\|1.0.0.7\|_auto_proto_2| () Int
  0)
(define-fun |17.56.26.-1| () Address
  (ip_constructor 17 56 26 (- 1)))
(define-fun |165.165.167.-1| () Address
  (ip_constructor 165 165 167 (- 1)))
(define-fun |\|1.0.0.2\|_auto_dst_0| () Address
  (ip_constructor 220 220 (- 1) (- 1)))
(define-fun |\|1.0.0.9\|_auto_proto_3| () Int
  0)
(define-fun |\|1.0.0.01\|_auto_proto_3| () Int
  0)
(define-fun |\|1.0.0.9\|_auto_dstp_1| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.7\|_auto_srcp_0| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.6\|_auto_srcp_1| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.3\|_auto_src_2| () Address
  (ip_constructor 220 220 222 (- 1)))
(define-fun |1.0.0.7| () Address
  (ip_constructor 1 0 0 7))
(define-fun |\|1.0.0.4\|_auto_srcp_2| () PortRange
  (port_range_constructor 0 65535))
(define-fun |1.0.0.4| () Address
  (ip_constructor 1 0 0 4))
(define-fun |\|1.0.0.3\|_auto_dstp_0| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.10\|_auto_srcp_0| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.2\|_auto_srcp_1| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.5\|_auto_srcp_2| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.7\|_auto_src_0| () Address
  (ip_constructor 0 0 0 0))
(define-fun |\|1.0.0.7\|_auto_dstp_2| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.01\|_auto_src_1| () Address
  (ip_constructor 0 0 0 0))
(define-fun |\|1.0.0.8\|_auto_src_0| () Address
  (ip_constructor 94 142 249 (- 1)))
(define-fun |1.0.0.8| () Address
  (ip_constructor 1 0 0 8))
(define-fun |\|1.0.0.8\|_auto_srcp_0| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.01\|_auto_src_0| () Address
  (ip_constructor 220 220 (- 1) (- 1)))
(define-fun |\|1.0.0.9\|_auto_srcp_4| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.3\|_auto_src_5| () Address
  (ip_constructor 0 0 0 0))
(define-fun |\|1.0.0.6\|_auto_srcp_2| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.3\|_auto_src_1| () Address
  (ip_constructor 165 165 167 (- 1)))
(define-fun |\|1.0.0.9\|_auto_srcp_1| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.9\|_auto_srcp_0| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.8\|_auto_proto_1| () Int
  0)
(define-fun |\|1.0.0.2\|_auto_dst_1| () Address
  (ip_constructor 0 0 0 0))
(define-fun |204.0.0.2| () Address
  (ip_constructor 204 0 0 2))
(define-fun |\|1.0.0.01\|_auto_proto_1| () Int
  0)
(define-fun |\|1.0.0.3\|_auto_dstp_5| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.4\|_auto_dstp_1| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.3\|_auto_proto_1| () Int
  0)
(define-fun |\|1.0.0.5\|_auto_proto_2| () Int
  0)
(define-fun |\|1.0.0.4\|_auto_srcp_0| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.5\|_auto_srcp_0| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.3\|_auto_dst_4| () Address
  (ip_constructor 0 0 0 0))
(define-fun |\|1.0.0.01\|_auto_proto_0| () Int
  0)
(define-fun |\|1.0.0.3\|_auto_srcp_2| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.3\|_auto_dstp_3| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.6\|_auto_dst_0| () Address
  (ip_constructor 165 165 (- 1) (- 1)))
(define-fun |\|1.0.0.9\|_auto_src_4| () Address
  (ip_constructor 204 0 0 2))
(define-fun |\|1.0.0.2\|_auto_src_0| () Address
  (ip_constructor 220 220 (- 1) (- 1)))
(define-fun |1.0.0.11| () Address
  (ip_constructor 1 0 0 11))
(define-fun |\|1.0.0.10\|_auto_proto_1| () Int
  0)
(define-fun |\|1.0.0.01\|_auto_proto_2| () Int
  0)
(define-fun |\|1.0.0.5\|_auto_proto_1| () Int
  0)
(define-fun |\|1.0.0.2\|_auto_proto_0| () Int
  0)
(define-fun |\|1.0.0.9\|_auto_proto_4| () Int
  0)
(define-fun |\|1.0.0.7\|_auto_dst_0| () Address
  (ip_constructor 0 0 0 0))
(define-fun |\|1.0.0.9\|_auto_proto_1| () Int
  0)
(define-fun |\|1.0.0.9\|_auto_proto_2| () Int
  0)
(define-fun |202.0.0.-1| () Address
  (ip_constructor 202 0 0 (- 1)))
(define-fun |\|1.0.0.6\|_auto_dstp_3| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.10\|_auto_dst_1| () Address
  (ip_constructor 0 0 0 0))
(define-fun |\|1.0.0.3\|_auto_srcp_4| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.6\|_auto_dstp_2| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.8\|_auto_dst_0| () Address
  (ip_constructor 17 56 26 (- 1)))
(define-fun |\|1.0.0.5\|_auto_proto_0| () Int
  0)
(define-fun |\|1.0.0.7\|_auto_dstp_1| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.3\|_auto_src_4| () Address
  (ip_constructor 0 0 0 0))
(define-fun |1.0.0.3| () Address
  (ip_constructor 1 0 0 3))
(define-fun |17.56.27.-1| () Address
  (ip_constructor 17 56 27 (- 1)))
(define-fun |\|1.0.0.5\|_auto_dstp_0| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.9\|_auto_src_1| () Address
  (ip_constructor 17 56 (- 1) (- 1)))
(define-fun |\|1.0.0.7\|_auto_srcp_2| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.5\|_auto_src_0| () Address
  (ip_constructor 165 165 (- 1) (- 1)))
(define-fun |\|1.0.0.01\|_auto_srcp_2| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.3\|_auto_proto_5| () Int
  0)
(define-fun |\|1.0.0.01\|_auto_dst_1| () Address
  (ip_constructor 0 0 0 0))
(define-fun |\|1.0.0.4\|_auto_dst_2| () Address
  (ip_constructor 201 0 0 (- 1)))
(define-fun |\|1.0.0.3\|_auto_dstp_4| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.3\|_auto_dst_5| () Address
  (ip_constructor 0 0 0 0))
(define-fun |1.0.0.12| () Address
  (ip_constructor 1 0 0 12))
(define-fun |\|1.0.0.10\|_auto_dstp_0| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.6\|_auto_src_0| () Address
  (ip_constructor 165 165 (- 1) (- 1)))
(define-fun |\|1.0.0.4\|_auto_proto_0| () Int
  0)
(define-fun |\|1.0.0.7\|_auto_dst_1| () Address
  (ip_constructor 0 0 0 0))
(define-fun |\|1.0.0.5\|_auto_dstp_2| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.01\|_auto_dstp_2| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.01\|_auto_dst_3| () Address
  (ip_constructor 200 0 0 (- 1)))
(define-fun |220.220.222.-1| () Address
  (ip_constructor 220 220 222 (- 1)))
(define-fun |\|1.0.0.8\|_auto_dstp_0| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.3\|_auto_dstp_1| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.7\|_auto_src_1| () Address
  (ip_constructor 0 0 0 0))
(define-fun |\|1.0.0.6\|_auto_srcp_3| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.9\|_auto_dst_3| () Address
  (ip_constructor 0 0 0 0))
(define-fun |\|1.0.0.3\|_auto_srcp_5| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.3\|_auto_dst_2| () Address
  (ip_constructor 165 165 167 (- 1)))
(define-fun |\|1.0.0.9\|_auto_dstp_4| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.3\|_auto_srcp_1| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.5\|_auto_dst_1| () Address
  (ip_constructor 0 0 0 0))
(define-fun |\|1.0.0.10\|_auto_dst_0| () Address
  (ip_constructor 17 56 (- 1) (- 1)))
(define-fun |\|1.0.0.6\|_auto_proto_2| () Int
  0)
(define-fun |\|1.0.0.3\|_auto_proto_3| () Int
  0)
(define-fun |\|1.0.0.7\|_auto_src_2| () Address
  (ip_constructor 204 0 0 2))
(define-fun |1.0.0.01| () Address
  (ip_constructor 1 0 0 1))
(define-fun |\|1.0.0.9\|_auto_src_3| () Address
  (ip_constructor 0 0 0 0))
(define-fun |\|1.0.0.3\|_auto_dst_1| () Address
  (ip_constructor 220 220 222 (- 1)))
(define-fun |165.165.166.-1| () Address
  (ip_constructor 165 165 166 (- 1)))
(define-fun |\|1.0.0.7\|_auto_srcp_1| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.7\|_auto_proto_1| () Int
  0)
(define-fun |\|1.0.0.01\|_auto_srcp_1| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.4\|_auto_proto_2| () Int
  0)
(define-fun |\|1.0.0.3\|_auto_dst_3| () Address
  (ip_constructor 0 0 0 0))
(define-fun |\|1.0.0.8\|_auto_src_1| () Address
  (ip_constructor 17 56 26 (- 1)))
(define-fun |1.0.0.9| () Address
  (ip_constructor 1 0 0 9))
(define-fun |94.142.249.-1| () Address
  (ip_constructor 94 142 249 (- 1)))
(define-fun |\|1.0.0.9\|_auto_dstp_0| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.3\|_auto_dstp_2| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.01\|_auto_dst_0| () Address
  (ip_constructor 220 220 (- 1) (- 1)))
(define-fun |\|1.0.0.9\|_auto_srcp_3| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.4\|_auto_src_0| () Address
  (ip_constructor 165 165 (- 1) (- 1)))
(define-fun |\|1.0.0.6\|_auto_dst_1| () Address
  (ip_constructor 165 165 167 (- 1)))
(define-fun |\|1.0.0.2\|_auto_src_1| () Address
  (ip_constructor 0 0 0 0))
(define-fun |\|1.0.0.6\|_auto_dst_2| () Address
  (ip_constructor 220 220 222 (- 1)))
(define-fun |\|1.0.0.01\|_auto_dst_2| () Address
  (ip_constructor 0 0 0 0))
(define-fun |1.0.0.6| () Address
  (ip_constructor 1 0 0 6))
(define-fun wildcard () Address
  (ip_constructor (- 1) (- 1) (- 1) (- 1)))
(define-fun |\|1.0.0.8\|_auto_srcp_1| () PortRange
  (port_range_constructor 0 65535))
(define-fun |1.0.0.5| () Address
  (ip_constructor 1 0 0 5))
(define-fun |\|1.0.0.9\|_auto_dstp_2| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.01\|_auto_src_2| () Address
  (ip_constructor 0 0 0 0))
(define-fun |\|1.0.0.3\|_auto_src_0| () Address
  (ip_constructor 220 220 (- 1) (- 1)))
(define-fun |\|1.0.0.4\|_auto_dst_1| () Address
  (ip_constructor 0 0 0 0))
(define-fun |\|1.0.0.9\|_auto_src_0| () Address
  (ip_constructor 94 142 249 (- 1)))
(define-fun |\|1.0.0.01\|_auto_srcp_0| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.4\|_auto_srcp_1| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.10\|_auto_src_1| () Address
  (ip_constructor 0 0 0 0))
(define-fun |\|1.0.0.9\|_auto_src_2| () Address
  (ip_constructor 0 0 0 0))
(define-fun |\|1.0.0.3\|_auto_proto_2| () Int
  0)
(define-fun |\|1.0.0.7\|_auto_proto_0| () Int
  0)
(define-fun |\|1.0.0.9\|_auto_dst_1| () Address
  (ip_constructor (- 1) (- 1) (- 1) (- 1)))
(define-fun |\|1.0.0.3\|_auto_proto_0| () Int
  0)
(define-fun |17.56.28.-1| () Address
  (ip_constructor 17 56 28 (- 1)))
(define-fun |\|1.0.0.8\|_auto_dstp_1| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.01\|_auto_srcp_3| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.6\|_auto_srcp_0| () PortRange
  (port_range_constructor 0 65535))
(define-fun |165.165.165.-1| () Address
  (ip_constructor 165 165 165 (- 1)))
(define-fun |\|1.0.0.4\|_auto_dstp_0| () PortRange
  (port_range_constructor 0 65535))
(define-fun |1.0.0.2| () Address
  (ip_constructor 1 0 0 2))
(define-fun |\|1.0.0.3\|_auto_proto_4| () Int
  0)
(define-fun |\|1.0.0.4\|_auto_dst_0| () Address
  (ip_constructor 165 165 (- 1) (- 1)))
(define-fun |\|1.0.0.3\|_auto_srcp_0| () PortRange
  (port_range_constructor 0 65535))
(define-fun |1.0.0.10| () Address
  (ip_constructor 1 0 0 10))
(define-fun |\|1.0.0.7\|_auto_dstp_0| () PortRange
  (port_range_constructor 0 65535))
(define-fun |220.220.220.-1| () Address
  (ip_constructor 220 220 220 (- 1)))
(define-fun |\|1.0.0.5\|_auto_src_1| () Address
  (ip_constructor 0 0 0 0))
(define-fun |\|1.0.0.3\|_auto_src_3| () Address
  (ip_constructor 0 0 0 0))
(define-fun |\|1.0.0.4\|_auto_proto_1| () Int
  0)
(define-fun |\|1.0.0.8\|_auto_proto_0| () Int
  0)
(define-fun |\|1.0.0.9\|_auto_dst_0| () Address
  (ip_constructor 17 56 26 (- 1)))
(define-fun |200.0.0.-1| () Address
  (ip_constructor 200 0 0 (- 1)))
(define-fun |\|1.0.0.01\|_auto_dstp_3| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.10\|_auto_dstp_1| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.9\|_auto_proto_0| () Int
  0)
(define-fun |\|1.0.0.5\|_auto_dstp_1| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.6\|_auto_dstp_1| () PortRange
  (port_range_constructor 0 65535))
(define-fun null () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.9\|_auto_dst_2| () Address
  (ip_constructor 0 0 0 0))
(define-fun null () Address
  (ip_constructor 0 0 0 0))
(define-fun |\|1.0.0.10\|_auto_srcp_1| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.6\|_auto_proto_3| () Int
  0)
(define-fun |\|1.0.0.01\|_auto_dstp_0| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.2\|_auto_srcp_0| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.10\|_auto_proto_0| () Int
  0)
(define-fun |\|1.0.0.6\|_auto_proto_1| () Int
  0)
(define-fun |\|1.0.0.5\|_auto_dst_2| () Address
  (ip_constructor 0 0 0 0))
(define-fun |\|1.0.0.2\|_auto_dstp_0| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.4\|_auto_src_2| () Address
  (ip_constructor 204 0 0 2))
(define-fun |201.0.0.-1| () Address
  (ip_constructor 201 0 0 (- 1)))
(define-fun |\|1.0.0.3\|_auto_srcp_3| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.4\|_auto_dstp_2| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.5\|_auto_dst_0| () Address
  (ip_constructor 165 165 (- 1) (- 1)))
(define-fun |\|1.0.0.9\|_auto_srcp_2| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.2\|_auto_proto_1| () Int
  0)
(define-fun |\|1.0.0.01\|_auto_dstp_1| () PortRange
  (port_range_constructor 0 65535))
(define-fun |\|1.0.0.6\|_auto_action| () Bool
  true)
(define-fun |\|1.0.0.6\|_auto_default_action| () Bool
  false)
(define-fun |\|1.0.0.6\|_auto_dst_ip_4_3| () Int
  0)
(define-fun |\|1.0.0.6\|_auto_dst_ip_3_3| () Int
  0)
(define-fun |\|1.0.0.6\|_auto_dst_ip_2_3| () Int
  0)
(define-fun |\|1.0.0.6\|_auto_dst_ip_1_3| () Int
  0)
(define-fun |\|1.0.0.6\|_auto_src_ip_4_3| () Int
  0)
(define-fun |\|1.0.0.6\|_auto_src_ip_3_3| () Int
  0)
(define-fun |\|1.0.0.6\|_auto_src_ip_2_3| () Int
  0)
(define-fun |\|1.0.0.6\|_auto_src_ip_1_3| () Int
  0)
(define-fun |\|1.0.0.6\|_auto_dst_ip_4_2| () Int
  (- 1))
(define-fun |\|1.0.0.6\|_auto_dst_ip_3_2| () Int
  222)
(define-fun |\|1.0.0.6\|_auto_dst_ip_2_2| () Int
  220)
(define-fun |\|1.0.0.6\|_auto_dst_ip_1_2| () Int
  220)
(define-fun |\|1.0.0.6\|_auto_src_ip_4_2| () Int
  (- 1))
(define-fun |\|1.0.0.6\|_auto_src_ip_3_2| () Int
  167)
(define-fun |\|1.0.0.6\|_auto_src_ip_2_2| () Int
  165)
(define-fun |\|1.0.0.6\|_auto_src_ip_1_2| () Int
  165)
(define-fun |\|1.0.0.6\|_auto_dst_ip_4_1| () Int
  (- 1))
(define-fun |\|1.0.0.6\|_auto_dst_ip_3_1| () Int
  167)
(define-fun |\|1.0.0.6\|_auto_dst_ip_2_1| () Int
  165)
(define-fun |\|1.0.0.6\|_auto_dst_ip_1_1| () Int
  165)
(define-fun |\|1.0.0.6\|_auto_src_ip_4_1| () Int
  (- 1))
(define-fun |\|1.0.0.6\|_auto_src_ip_3_1| () Int
  222)
(define-fun |\|1.0.0.6\|_auto_src_ip_2_1| () Int
  220)
(define-fun |\|1.0.0.6\|_auto_src_ip_1_1| () Int
  220)
(define-fun |\|1.0.0.6\|_auto_dst_ip_4_0| () Int
  (- 1))
(define-fun |\|1.0.0.6\|_auto_dst_ip_3_0| () Int
  (- 1))
(define-fun |\|1.0.0.6\|_auto_dst_ip_2_0| () Int
  165)
(define-fun |\|1.0.0.6\|_auto_dst_ip_1_0| () Int
  165)
(define-fun |\|1.0.0.6\|_auto_src_ip_4_0| () Int
  (- 1))
(define-fun |\|1.0.0.6\|_auto_src_ip_3_0| () Int
  (- 1))
(define-fun |\|1.0.0.6\|_auto_src_ip_2_0| () Int
  165)
(define-fun |\|1.0.0.6\|_auto_src_ip_1_0| () Int
  165)
(define-fun |\|1.0.0.5\|_auto_action| () Bool
  true)
(define-fun |\|1.0.0.5\|_auto_default_action| () Bool
  false)
(define-fun |\|1.0.0.5\|_auto_dst_ip_4_2| () Int
  0)
(define-fun |\|1.0.0.5\|_auto_dst_ip_3_2| () Int
  0)
(define-fun |\|1.0.0.5\|_auto_dst_ip_2_2| () Int
  0)
(define-fun |\|1.0.0.5\|_auto_dst_ip_1_2| () Int
  0)
(define-fun |\|1.0.0.5\|_auto_src_ip_4_2| () Int
  0)
(define-fun |\|1.0.0.5\|_auto_src_ip_3_2| () Int
  0)
(define-fun |\|1.0.0.5\|_auto_src_ip_2_2| () Int
  0)
(define-fun |\|1.0.0.5\|_auto_src_ip_1_2| () Int
  0)
(define-fun |\|1.0.0.5\|_auto_dst_ip_4_1| () Int
  0)
(define-fun |\|1.0.0.5\|_auto_dst_ip_3_1| () Int
  0)
(define-fun |\|1.0.0.5\|_auto_dst_ip_2_1| () Int
  0)
(define-fun |\|1.0.0.5\|_auto_dst_ip_1_1| () Int
  0)
(define-fun |\|1.0.0.5\|_auto_src_ip_4_1| () Int
  0)
(define-fun |\|1.0.0.5\|_auto_src_ip_3_1| () Int
  0)
(define-fun |\|1.0.0.5\|_auto_src_ip_2_1| () Int
  0)
(define-fun |\|1.0.0.5\|_auto_src_ip_1_1| () Int
  0)
(define-fun |\|1.0.0.5\|_auto_dst_ip_4_0| () Int
  (- 1))
(define-fun |\|1.0.0.5\|_auto_dst_ip_3_0| () Int
  (- 1))
(define-fun |\|1.0.0.5\|_auto_dst_ip_2_0| () Int
  165)
(define-fun |\|1.0.0.5\|_auto_dst_ip_1_0| () Int
  165)
(define-fun |\|1.0.0.5\|_auto_src_ip_4_0| () Int
  (- 1))
(define-fun |\|1.0.0.5\|_auto_src_ip_3_0| () Int
  (- 1))
(define-fun |\|1.0.0.5\|_auto_src_ip_2_0| () Int
  165)
(define-fun |\|1.0.0.5\|_auto_src_ip_1_0| () Int
  165)
(define-fun |\|1.0.0.8\|_auto_action| () Bool
  true)
(define-fun |\|1.0.0.8\|_auto_default_action| () Bool
  false)
(define-fun |\|1.0.0.8\|_auto_dst_ip_4_1| () Int
  (- 1))
(define-fun |\|1.0.0.8\|_auto_dst_ip_3_1| () Int
  249)
(define-fun |\|1.0.0.8\|_auto_dst_ip_2_1| () Int
  142)
(define-fun |\|1.0.0.8\|_auto_dst_ip_1_1| () Int
  94)
(define-fun |\|1.0.0.8\|_auto_src_ip_4_1| () Int
  (- 1))
(define-fun |\|1.0.0.8\|_auto_src_ip_3_1| () Int
  26)
(define-fun |\|1.0.0.8\|_auto_src_ip_2_1| () Int
  56)
(define-fun |\|1.0.0.8\|_auto_src_ip_1_1| () Int
  17)
(define-fun |\|1.0.0.8\|_auto_dst_ip_4_0| () Int
  (- 1))
(define-fun |\|1.0.0.8\|_auto_dst_ip_3_0| () Int
  26)
(define-fun |\|1.0.0.8\|_auto_dst_ip_2_0| () Int
  56)
(define-fun |\|1.0.0.8\|_auto_dst_ip_1_0| () Int
  17)
(define-fun |\|1.0.0.8\|_auto_src_ip_4_0| () Int
  (- 1))
(define-fun |\|1.0.0.8\|_auto_src_ip_3_0| () Int
  249)
(define-fun |\|1.0.0.8\|_auto_src_ip_2_0| () Int
  142)
(define-fun |\|1.0.0.8\|_auto_src_ip_1_0| () Int
  94)
(define-fun |\|1.0.0.7\|_auto_action| () Bool
  true)
(define-fun |\|1.0.0.7\|_auto_default_action| () Bool
  false)
(define-fun |\|1.0.0.7\|_auto_dst_ip_4_2| () Int
  (- 1))
(define-fun |\|1.0.0.7\|_auto_dst_ip_3_2| () Int
  (- 1))
(define-fun |\|1.0.0.7\|_auto_dst_ip_2_2| () Int
  (- 1))
(define-fun |\|1.0.0.7\|_auto_dst_ip_1_2| () Int
  (- 1))
(define-fun |\|1.0.0.7\|_auto_src_ip_4_2| () Int
  2)
(define-fun |\|1.0.0.7\|_auto_src_ip_3_2| () Int
  0)
(define-fun |\|1.0.0.7\|_auto_src_ip_2_2| () Int
  0)
(define-fun |\|1.0.0.7\|_auto_src_ip_1_2| () Int
  204)
(define-fun |\|1.0.0.7\|_auto_dst_ip_4_1| () Int
  0)
(define-fun |\|1.0.0.7\|_auto_dst_ip_3_1| () Int
  0)
(define-fun |\|1.0.0.7\|_auto_dst_ip_2_1| () Int
  0)
(define-fun |\|1.0.0.7\|_auto_dst_ip_1_1| () Int
  0)
(define-fun |\|1.0.0.7\|_auto_src_ip_4_1| () Int
  0)
(define-fun |\|1.0.0.7\|_auto_src_ip_3_1| () Int
  0)
(define-fun |\|1.0.0.7\|_auto_src_ip_2_1| () Int
  0)
(define-fun |\|1.0.0.7\|_auto_src_ip_1_1| () Int
  0)
(define-fun |\|1.0.0.7\|_auto_dst_ip_4_0| () Int
  0)
(define-fun |\|1.0.0.7\|_auto_dst_ip_3_0| () Int
  0)
(define-fun |\|1.0.0.7\|_auto_dst_ip_2_0| () Int
  0)
(define-fun |\|1.0.0.7\|_auto_dst_ip_1_0| () Int
  0)
(define-fun |\|1.0.0.7\|_auto_src_ip_4_0| () Int
  0)
(define-fun |\|1.0.0.7\|_auto_src_ip_3_0| () Int
  0)
(define-fun |\|1.0.0.7\|_auto_src_ip_2_0| () Int
  0)
(define-fun |\|1.0.0.7\|_auto_src_ip_1_0| () Int
  0)
(define-fun |\|1.0.0.2\|_auto_action| () Bool
  true)
(define-fun |\|1.0.0.2\|_auto_default_action| () Bool
  false)
(define-fun |\|1.0.0.2\|_auto_dst_ip_4_1| () Int
  0)
(define-fun |\|1.0.0.2\|_auto_dst_ip_3_1| () Int
  0)
(define-fun |\|1.0.0.2\|_auto_dst_ip_2_1| () Int
  0)
(define-fun |\|1.0.0.2\|_auto_dst_ip_1_1| () Int
  0)
(define-fun |\|1.0.0.2\|_auto_src_ip_4_1| () Int
  0)
(define-fun |\|1.0.0.2\|_auto_src_ip_3_1| () Int
  0)
(define-fun |\|1.0.0.2\|_auto_src_ip_2_1| () Int
  0)
(define-fun |\|1.0.0.2\|_auto_src_ip_1_1| () Int
  0)
(define-fun |\|1.0.0.2\|_auto_dst_ip_4_0| () Int
  (- 1))
(define-fun |\|1.0.0.2\|_auto_dst_ip_3_0| () Int
  (- 1))
(define-fun |\|1.0.0.2\|_auto_dst_ip_2_0| () Int
  220)
(define-fun |\|1.0.0.2\|_auto_dst_ip_1_0| () Int
  220)
(define-fun |\|1.0.0.2\|_auto_src_ip_4_0| () Int
  (- 1))
(define-fun |\|1.0.0.2\|_auto_src_ip_3_0| () Int
  (- 1))
(define-fun |\|1.0.0.2\|_auto_src_ip_2_0| () Int
  220)
(define-fun |\|1.0.0.2\|_auto_src_ip_1_0| () Int
  220)
(define-fun |\|1.0.0.4\|_auto_action| () Bool
  true)
(define-fun |\|1.0.0.4\|_auto_default_action| () Bool
  false)
(define-fun |\|1.0.0.4\|_auto_dst_ip_4_2| () Int
  (- 1))
(define-fun |\|1.0.0.4\|_auto_dst_ip_3_2| () Int
  0)
(define-fun |\|1.0.0.4\|_auto_dst_ip_2_2| () Int
  0)
(define-fun |\|1.0.0.4\|_auto_dst_ip_1_2| () Int
  201)
(define-fun |\|1.0.0.4\|_auto_src_ip_4_2| () Int
  2)
(define-fun |\|1.0.0.4\|_auto_src_ip_3_2| () Int
  0)
(define-fun |\|1.0.0.4\|_auto_src_ip_2_2| () Int
  0)
(define-fun |\|1.0.0.4\|_auto_src_ip_1_2| () Int
  204)
(define-fun |\|1.0.0.4\|_auto_dst_ip_4_1| () Int
  0)
(define-fun |\|1.0.0.4\|_auto_dst_ip_3_1| () Int
  0)
(define-fun |\|1.0.0.4\|_auto_dst_ip_2_1| () Int
  0)
(define-fun |\|1.0.0.4\|_auto_dst_ip_1_1| () Int
  0)
(define-fun |\|1.0.0.4\|_auto_src_ip_4_1| () Int
  0)
(define-fun |\|1.0.0.4\|_auto_src_ip_3_1| () Int
  0)
(define-fun |\|1.0.0.4\|_auto_src_ip_2_1| () Int
  0)
(define-fun |\|1.0.0.4\|_auto_src_ip_1_1| () Int
  0)
(define-fun |\|1.0.0.4\|_auto_dst_ip_4_0| () Int
  (- 1))
(define-fun |\|1.0.0.4\|_auto_dst_ip_3_0| () Int
  (- 1))
(define-fun |\|1.0.0.4\|_auto_dst_ip_2_0| () Int
  165)
(define-fun |\|1.0.0.4\|_auto_dst_ip_1_0| () Int
  165)
(define-fun |\|1.0.0.4\|_auto_src_ip_4_0| () Int
  (- 1))
(define-fun |\|1.0.0.4\|_auto_src_ip_3_0| () Int
  (- 1))
(define-fun |\|1.0.0.4\|_auto_src_ip_2_0| () Int
  165)
(define-fun |\|1.0.0.4\|_auto_src_ip_1_0| () Int
  165)
(define-fun |\|1.0.0.3\|_auto_action| () Bool
  true)
(define-fun |\|1.0.0.3\|_auto_default_action| () Bool
  false)
(define-fun |\|1.0.0.3\|_auto_dst_ip_4_5| () Int
  0)
(define-fun |\|1.0.0.3\|_auto_dst_ip_3_5| () Int
  0)
(define-fun |\|1.0.0.3\|_auto_dst_ip_2_5| () Int
  0)
(define-fun |\|1.0.0.3\|_auto_dst_ip_1_5| () Int
  0)
(define-fun |\|1.0.0.3\|_auto_src_ip_4_5| () Int
  0)
(define-fun |\|1.0.0.3\|_auto_src_ip_3_5| () Int
  0)
(define-fun |\|1.0.0.3\|_auto_src_ip_2_5| () Int
  0)
(define-fun |\|1.0.0.3\|_auto_src_ip_1_5| () Int
  0)
(define-fun |\|1.0.0.3\|_auto_dst_ip_4_4| () Int
  0)
(define-fun |\|1.0.0.3\|_auto_dst_ip_3_4| () Int
  0)
(define-fun |\|1.0.0.3\|_auto_dst_ip_2_4| () Int
  0)
(define-fun |\|1.0.0.3\|_auto_dst_ip_1_4| () Int
  0)
(define-fun |\|1.0.0.3\|_auto_src_ip_4_4| () Int
  0)
(define-fun |\|1.0.0.3\|_auto_src_ip_3_4| () Int
  0)
(define-fun |\|1.0.0.3\|_auto_src_ip_2_4| () Int
  0)
(define-fun |\|1.0.0.3\|_auto_src_ip_1_4| () Int
  0)
(define-fun |\|1.0.0.3\|_auto_dst_ip_4_3| () Int
  0)
(define-fun |\|1.0.0.3\|_auto_dst_ip_3_3| () Int
  0)
(define-fun |\|1.0.0.3\|_auto_dst_ip_2_3| () Int
  0)
(define-fun |\|1.0.0.3\|_auto_dst_ip_1_3| () Int
  0)
(define-fun |\|1.0.0.3\|_auto_src_ip_4_3| () Int
  0)
(define-fun |\|1.0.0.3\|_auto_src_ip_3_3| () Int
  0)
(define-fun |\|1.0.0.3\|_auto_src_ip_2_3| () Int
  0)
(define-fun |\|1.0.0.3\|_auto_src_ip_1_3| () Int
  0)
(define-fun |\|1.0.0.3\|_auto_dst_ip_4_2| () Int
  (- 1))
(define-fun |\|1.0.0.3\|_auto_dst_ip_3_2| () Int
  167)
(define-fun |\|1.0.0.3\|_auto_dst_ip_2_2| () Int
  165)
(define-fun |\|1.0.0.3\|_auto_dst_ip_1_2| () Int
  165)
(define-fun |\|1.0.0.3\|_auto_src_ip_4_2| () Int
  (- 1))
(define-fun |\|1.0.0.3\|_auto_src_ip_3_2| () Int
  222)
(define-fun |\|1.0.0.3\|_auto_src_ip_2_2| () Int
  220)
(define-fun |\|1.0.0.3\|_auto_src_ip_1_2| () Int
  220)
(define-fun |\|1.0.0.3\|_auto_dst_ip_4_1| () Int
  (- 1))
(define-fun |\|1.0.0.3\|_auto_dst_ip_3_1| () Int
  222)
(define-fun |\|1.0.0.3\|_auto_dst_ip_2_1| () Int
  220)
(define-fun |\|1.0.0.3\|_auto_dst_ip_1_1| () Int
  220)
(define-fun |\|1.0.0.3\|_auto_src_ip_4_1| () Int
  (- 1))
(define-fun |\|1.0.0.3\|_auto_src_ip_3_1| () Int
  167)
(define-fun |\|1.0.0.3\|_auto_src_ip_2_1| () Int
  165)
(define-fun |\|1.0.0.3\|_auto_src_ip_1_1| () Int
  165)
(define-fun |\|1.0.0.3\|_auto_dst_ip_4_0| () Int
  (- 1))
(define-fun |\|1.0.0.3\|_auto_dst_ip_3_0| () Int
  (- 1))
(define-fun |\|1.0.0.3\|_auto_dst_ip_2_0| () Int
  220)
(define-fun |\|1.0.0.3\|_auto_dst_ip_1_0| () Int
  220)
(define-fun |\|1.0.0.3\|_auto_src_ip_4_0| () Int
  (- 1))
(define-fun |\|1.0.0.3\|_auto_src_ip_3_0| () Int
  (- 1))
(define-fun |\|1.0.0.3\|_auto_src_ip_2_0| () Int
  220)
(define-fun |\|1.0.0.3\|_auto_src_ip_1_0| () Int
  220)
(define-fun |\|1.0.0.01\|_auto_action| () Bool
  true)
(define-fun |\|1.0.0.01\|_auto_default_action| () Bool
  false)
(define-fun |\|1.0.0.01\|_auto_dst_ip_4_3| () Int
  (- 1))
(define-fun |\|1.0.0.01\|_auto_dst_ip_3_3| () Int
  0)
(define-fun |\|1.0.0.01\|_auto_dst_ip_2_3| () Int
  0)
(define-fun |\|1.0.0.01\|_auto_dst_ip_1_3| () Int
  200)
(define-fun |\|1.0.0.01\|_auto_src_ip_4_3| () Int
  2)
(define-fun |\|1.0.0.01\|_auto_src_ip_3_3| () Int
  0)
(define-fun |\|1.0.0.01\|_auto_src_ip_2_3| () Int
  0)
(define-fun |\|1.0.0.01\|_auto_src_ip_1_3| () Int
  204)
(define-fun |\|1.0.0.01\|_auto_dst_ip_4_2| () Int
  0)
(define-fun |\|1.0.0.01\|_auto_dst_ip_3_2| () Int
  0)
(define-fun |\|1.0.0.01\|_auto_dst_ip_2_2| () Int
  0)
(define-fun |\|1.0.0.01\|_auto_dst_ip_1_2| () Int
  0)
(define-fun |\|1.0.0.01\|_auto_src_ip_4_2| () Int
  0)
(define-fun |\|1.0.0.01\|_auto_src_ip_3_2| () Int
  0)
(define-fun |\|1.0.0.01\|_auto_src_ip_2_2| () Int
  0)
(define-fun |\|1.0.0.01\|_auto_src_ip_1_2| () Int
  0)
(define-fun |\|1.0.0.01\|_auto_dst_ip_4_1| () Int
  0)
(define-fun |\|1.0.0.01\|_auto_dst_ip_3_1| () Int
  0)
(define-fun |\|1.0.0.01\|_auto_dst_ip_2_1| () Int
  0)
(define-fun |\|1.0.0.01\|_auto_dst_ip_1_1| () Int
  0)
(define-fun |\|1.0.0.01\|_auto_src_ip_4_1| () Int
  0)
(define-fun |\|1.0.0.01\|_auto_src_ip_3_1| () Int
  0)
(define-fun |\|1.0.0.01\|_auto_src_ip_2_1| () Int
  0)
(define-fun |\|1.0.0.01\|_auto_src_ip_1_1| () Int
  0)
(define-fun |\|1.0.0.01\|_auto_dst_ip_4_0| () Int
  (- 1))
(define-fun |\|1.0.0.01\|_auto_dst_ip_3_0| () Int
  (- 1))
(define-fun |\|1.0.0.01\|_auto_dst_ip_2_0| () Int
  220)
(define-fun |\|1.0.0.01\|_auto_dst_ip_1_0| () Int
  220)
(define-fun |\|1.0.0.01\|_auto_src_ip_4_0| () Int
  (- 1))
(define-fun |\|1.0.0.01\|_auto_src_ip_3_0| () Int
  (- 1))
(define-fun |\|1.0.0.01\|_auto_src_ip_2_0| () Int
  220)
(define-fun |\|1.0.0.01\|_auto_src_ip_1_0| () Int
  220)
(define-fun |\|1.0.0.9\|_auto_action| () Bool
  true)
(define-fun |\|1.0.0.9\|_auto_default_action| () Bool
  false)
(define-fun |\|1.0.0.9\|_auto_dst_ip_4_4| () Int
  (- 1))
(define-fun |\|1.0.0.9\|_auto_dst_ip_3_4| () Int
  0)
(define-fun |\|1.0.0.9\|_auto_dst_ip_2_4| () Int
  0)
(define-fun |\|1.0.0.9\|_auto_dst_ip_1_4| () Int
  202)
(define-fun |\|1.0.0.9\|_auto_src_ip_4_4| () Int
  2)
(define-fun |\|1.0.0.9\|_auto_src_ip_3_4| () Int
  0)
(define-fun |\|1.0.0.9\|_auto_src_ip_2_4| () Int
  0)
(define-fun |\|1.0.0.9\|_auto_src_ip_1_4| () Int
  204)
(define-fun |\|1.0.0.9\|_auto_dst_ip_4_3| () Int
  0)
(define-fun |\|1.0.0.9\|_auto_dst_ip_3_3| () Int
  0)
(define-fun |\|1.0.0.9\|_auto_dst_ip_2_3| () Int
  0)
(define-fun |\|1.0.0.9\|_auto_dst_ip_1_3| () Int
  0)
(define-fun |\|1.0.0.9\|_auto_src_ip_4_3| () Int
  0)
(define-fun |\|1.0.0.9\|_auto_src_ip_3_3| () Int
  0)
(define-fun |\|1.0.0.9\|_auto_src_ip_2_3| () Int
  0)
(define-fun |\|1.0.0.9\|_auto_src_ip_1_3| () Int
  0)
(define-fun |\|1.0.0.9\|_auto_dst_ip_4_2| () Int
  0)
(define-fun |\|1.0.0.9\|_auto_dst_ip_3_2| () Int
  0)
(define-fun |\|1.0.0.9\|_auto_dst_ip_2_2| () Int
  0)
(define-fun |\|1.0.0.9\|_auto_dst_ip_1_2| () Int
  0)
(define-fun |\|1.0.0.9\|_auto_src_ip_4_2| () Int
  0)
(define-fun |\|1.0.0.9\|_auto_src_ip_3_2| () Int
  0)
(define-fun |\|1.0.0.9\|_auto_src_ip_2_2| () Int
  0)
(define-fun |\|1.0.0.9\|_auto_src_ip_1_2| () Int
  0)
(define-fun |\|1.0.0.9\|_auto_dst_ip_4_1| () Int
  (- 1))
(define-fun |\|1.0.0.9\|_auto_dst_ip_3_1| () Int
  (- 1))
(define-fun |\|1.0.0.9\|_auto_dst_ip_2_1| () Int
  (- 1))
(define-fun |\|1.0.0.9\|_auto_dst_ip_1_1| () Int
  (- 1))
(define-fun |\|1.0.0.9\|_auto_src_ip_4_1| () Int
  (- 1))
(define-fun |\|1.0.0.9\|_auto_src_ip_3_1| () Int
  (- 1))
(define-fun |\|1.0.0.9\|_auto_src_ip_2_1| () Int
  56)
(define-fun |\|1.0.0.9\|_auto_src_ip_1_1| () Int
  17)
(define-fun |\|1.0.0.9\|_auto_dst_ip_4_0| () Int
  (- 1))
(define-fun |\|1.0.0.9\|_auto_dst_ip_3_0| () Int
  26)
(define-fun |\|1.0.0.9\|_auto_dst_ip_2_0| () Int
  56)
(define-fun |\|1.0.0.9\|_auto_dst_ip_1_0| () Int
  17)
(define-fun |\|1.0.0.9\|_auto_src_ip_4_0| () Int
  (- 1))
(define-fun |\|1.0.0.9\|_auto_src_ip_3_0| () Int
  249)
(define-fun |\|1.0.0.9\|_auto_src_ip_2_0| () Int
  142)
(define-fun |\|1.0.0.9\|_auto_src_ip_1_0| () Int
  94)
(define-fun |\|1.0.0.10\|_auto_action| () Bool
  true)
(define-fun |\|1.0.0.10\|_auto_default_action| () Bool
  false)
(define-fun |\|1.0.0.10\|_auto_dst_ip_4_1| () Int
  0)
(define-fun |\|1.0.0.10\|_auto_dst_ip_3_1| () Int
  0)
(define-fun |\|1.0.0.10\|_auto_dst_ip_2_1| () Int
  0)
(define-fun |\|1.0.0.10\|_auto_dst_ip_1_1| () Int
  0)
(define-fun |\|1.0.0.10\|_auto_src_ip_4_1| () Int
  0)
(define-fun |\|1.0.0.10\|_auto_src_ip_3_1| () Int
  0)
(define-fun |\|1.0.0.10\|_auto_src_ip_2_1| () Int
  0)
(define-fun |\|1.0.0.10\|_auto_src_ip_1_1| () Int
  0)
(define-fun |\|1.0.0.10\|_auto_dst_ip_4_0| () Int
  (- 1))
(define-fun |\|1.0.0.10\|_auto_dst_ip_3_0| () Int
  (- 1))
(define-fun |\|1.0.0.10\|_auto_dst_ip_2_0| () Int
  56)
(define-fun |\|1.0.0.10\|_auto_dst_ip_1_0| () Int
  17)
(define-fun |\|1.0.0.10\|_auto_src_ip_4_0| () Int
  (- 1))
(define-fun |\|1.0.0.10\|_auto_src_ip_3_0| () Int
  (- 1))
(define-fun |\|1.0.0.10\|_auto_src_ip_2_0| () Int
  56)
(define-fun |\|1.0.0.10\|_auto_src_ip_1_0| () Int
  17)
(define-fun |\|1.0.0.11\|_auto_action| () Bool
  true)
(define-fun |\|1.0.0.11\|_auto_default_action| () Bool
  false)
(define-fun deny ((x!0 Node) (x!1 Int)) Bool
  (or (and (= x!0 |1.0.0.6|) (= x!1 29))
      (and (= x!0 |1.0.0.3|) (= x!1 19))
      (and (= x!0 |1.0.0.9|) (= x!1 7))
      (and (= x!0 |1.0.0.8|) (= x!1 2))
      (and (= x!0 |1.0.0.6|) (= x!1 1))
      (and (= x!0 |1.0.0.3|) (= x!1 0))
      (and (= x!0 |1.0.0.6|) (= x!1 30))
      (and (= x!0 |1.0.0.6|) (= x!1 17))
      (and (= x!0 |1.0.0.5|) (= x!1 26))
      (and (= x!0 |1.0.0.5|) (= x!1 22))
      (and (= x!0 |1.0.0.4|) (= x!1 18))
      (and (= x!0 |1.0.0.4|) (= x!1 33))
      (and (= x!0 |1.0.0.3|) (= x!1 26))
      (and (= x!0 |1.0.0.3|) (= x!1 22))
      (and (= x!0 |1.0.0.01|) (= x!1 15))
      (and (= x!0 |1.0.0.01|) (= x!1 30))
      (and (= x!0 |1.0.0.01|) (= x!1 14))
      (and (= x!0 |1.0.0.01|) (= x!1 5))
      (and (= x!0 |1.0.0.01|) (= x!1 18))
      (and (= x!0 |1.0.0.01|) (= x!1 17))
      (and (= x!0 |1.0.0.9|) (= x!1 5))
      (and (= x!0 |1.0.0.11|) (= x!1 9))
      (and (= x!0 |1.0.0.11|) (= x!1 4))
      (and (= x!0 |1.0.0.11|) (= x!1 3))))
(define-fun addrToNode ((x!0 Address)) Node
  (ite (= x!0 (ip_constructor 1 0 0 11)) |1.0.0.11|
  (ite (= x!0 (ip_constructor 1 0 0 10)) |1.0.0.10|
  (ite (= x!0 (ip_constructor 17 56 27 (- 1))) |17.56.27.-1|
  (ite (= x!0 (ip_constructor 1 0 0 9)) |1.0.0.9|
  (ite (= x!0 (ip_constructor 200 0 0 (- 1))) |200.0.0.-1|
  (ite (= x!0 (ip_constructor 201 0 0 (- 1))) |201.0.0.-1|
  (ite (= x!0 (ip_constructor 202 0 0 (- 1))) |202.0.0.-1|
  (ite (= x!0 (ip_constructor 220 220 220 (- 1))) |220.220.220.-1|
  (ite (= x!0 (ip_constructor 220 220 222 (- 1))) |220.220.222.-1|
  (ite (= x!0 (ip_constructor 165 165 166 (- 1))) |165.165.166.-1|
  (ite (= x!0 (ip_constructor 1 0 0 1)) |1.0.0.01|
  (ite (= x!0 (ip_constructor 94 142 251 1)) |94.142.251.1|
  (ite (= x!0 (ip_constructor 17 56 28 (- 1))) |17.56.28.-1|
  (ite (= x!0 (ip_constructor 17 56 26 (- 1))) |17.56.26.-1|
  (ite (= x!0 (ip_constructor 204 0 0 2)) |204.0.0.2|
  (ite (= x!0 (ip_constructor 1 0 0 3)) |1.0.0.3|
  (ite (= x!0 (ip_constructor 1 0 0 4)) |1.0.0.4|
  (ite (= x!0 (ip_constructor 1 0 0 2)) |1.0.0.2|
  (ite (= x!0 (ip_constructor 1 0 0 7)) |1.0.0.7|
  (ite (= x!0 (ip_constructor 1 0 0 8)) |1.0.0.8|
  (ite (= x!0 (ip_constructor 1 0 0 5)) |1.0.0.5|
  (ite (= x!0 (ip_constructor 1 0 0 6)) |1.0.0.6|
  (ite (= x!0 (ip_constructor 220 220 221 (- 1))) |220.220.221.-1|
  (ite (= x!0 (ip_constructor 165 165 167 (- 1))) |165.165.167.-1|
  (ite (= x!0 (ip_constructor 165 165 165 (- 1))) |165.165.165.-1|
  (ite (= x!0 (ip_constructor 94 142 249 (- 1))) |94.142.249.-1|
    |1.0.0.12|)))))))))))))))))))))))))))
(define-fun nodeHasAddr ((x!0 Node) (x!1 Address)) Bool
  (let ((a!1 (ite (= x!1 (ip_constructor 1 0 0 8))
                  (ip_constructor 1 0 0 8)
                  (ite (= x!1 (ip_constructor 202 0 0 (- 1)))
                       (ip_constructor 202 0 0 (- 1))
                       (ip_constructor 61 15 15 15)))))
  (let ((a!2 (ite (= x!1 (ip_constructor 204 0 0 2))
                  (ip_constructor 204 0 0 2)
                  (ite (= x!1 (ip_constructor 1 0 0 1))
                       (ip_constructor 1 0 0 1)
                       a!1))))
  (let ((a!3 (ite (= x!1 (ip_constructor 1 0 0 10))
                  (ip_constructor 1 0 0 10)
                  (ite (= x!1 (ip_constructor 1 0 0 6))
                       (ip_constructor 1 0 0 6)
                       a!2))))
  (let ((a!4 (ite (= x!1 (ip_constructor 17 56 27 (- 1)))
                  (ip_constructor 17 56 27 (- 1))
                  (ite (= x!1 (ip_constructor 165 165 167 (- 1)))
                       (ip_constructor 165 165 167 (- 1))
                       a!3))))
  (let ((a!5 (ite (= x!1 (ip_constructor 94 142 249 (- 1)))
                  (ip_constructor 94 142 249 (- 1))
                  (ite (= x!1 (ip_constructor 1 0 0 9))
                       (ip_constructor 1 0 0 9)
                       a!4))))
  (let ((a!6 (ite (= x!1 (ip_constructor 165 165 166 (- 1)))
                  (ip_constructor 165 165 166 (- 1))
                  (ite (= x!1 (ip_constructor 1 0 0 12))
                       (ip_constructor 1 0 0 12)
                       a!5))))
  (let ((a!7 (ite (= x!1 (ip_constructor 1 0 0 3))
                  (ip_constructor 1 0 0 3)
                  (ite (= x!1 (ip_constructor 220 220 220 (- 1)))
                       (ip_constructor 220 220 220 (- 1))
                       a!6))))
  (let ((a!8 (ite (= x!1 (ip_constructor 220 220 222 (- 1)))
                  (ip_constructor 220 220 222 (- 1))
                  (ite (= x!1 (ip_constructor 220 220 221 (- 1)))
                       (ip_constructor 220 220 221 (- 1))
                       a!7))))
  (let ((a!9 (ite (= x!1 (ip_constructor 17 56 26 (- 1)))
                  (ip_constructor 17 56 26 (- 1))
                  (ite (= x!1 (ip_constructor 200 0 0 (- 1)))
                       (ip_constructor 200 0 0 (- 1))
                       a!8))))
  (let ((a!10 (ite (= x!1 (ip_constructor 94 142 251 1))
                   (ip_constructor 94 142 251 1)
                   (ite (= x!1 (ip_constructor 17 56 28 (- 1)))
                        (ip_constructor 17 56 28 (- 1))
                        a!9))))
  (let ((a!11 (ite (= x!1 (ip_constructor 1 0 0 4))
                   (ip_constructor 1 0 0 4)
                   (ite (= x!1 (ip_constructor 1 0 0 7))
                        (ip_constructor 1 0 0 7)
                        a!10))))
  (let ((a!12 (ite (= x!1 (ip_constructor 201 0 0 (- 1)))
                   (ip_constructor 201 0 0 (- 1))
                   (ite (= x!1 (ip_constructor 1 0 0 11))
                        (ip_constructor 1 0 0 11)
                        a!11))))
  (let ((a!13 (ite (= x!1 (ip_constructor 1 0 0 5))
                   (ip_constructor 1 0 0 5)
                   (ite (= x!1 (ip_constructor 165 165 165 (- 1)))
                        (ip_constructor 165 165 165 (- 1))
                        a!12))))
  (let ((a!14 (ite (= x!1 (ip_constructor 1 0 0 2))
                   (ip_constructor 1 0 0 2)
                   a!13)))
    (or (and (= x!0 |94.142.249.-1|) (= a!14 (ip_constructor 94 142 249 (- 1))))
        (and (= x!0 |165.165.165.-1|)
             (= a!14 (ip_constructor 165 165 165 (- 1))))
        (and (= x!0 |165.165.167.-1|)
             (= a!14 (ip_constructor 165 165 167 (- 1))))
        (and (= x!0 |220.220.221.-1|)
             (= a!14 (ip_constructor 220 220 221 (- 1))))
        (and (= x!0 |1.0.0.6|) (= a!14 (ip_constructor 1 0 0 6)))
        (and (= x!0 |1.0.0.5|) (= a!14 (ip_constructor 1 0 0 5)))
        (and (= x!0 |1.0.0.8|) (= a!14 (ip_constructor 1 0 0 8)))
        (and (= x!0 |1.0.0.7|) (= a!14 (ip_constructor 1 0 0 7)))
        (and (= x!0 |1.0.0.2|) (= a!14 (ip_constructor 1 0 0 2)))
        (and (= x!0 |1.0.0.4|) (= a!14 (ip_constructor 1 0 0 4)))
        (and (= x!0 |1.0.0.3|) (= a!14 (ip_constructor 1 0 0 3)))
        (and (= x!0 |204.0.0.2|) (= a!14 (ip_constructor 204 0 0 2)))
        (and (= x!0 |17.56.26.-1|) (= a!14 (ip_constructor 17 56 26 (- 1))))
        (and (= x!0 |17.56.28.-1|) (= a!14 (ip_constructor 17 56 28 (- 1))))
        (and (= x!0 |94.142.251.1|) (= a!14 (ip_constructor 94 142 251 1)))
        (and (= x!0 |1.0.0.01|) (= a!14 (ip_constructor 1 0 0 1)))
        (and (= x!0 |165.165.166.-1|)
             (= a!14 (ip_constructor 165 165 166 (- 1))))
        (and (= x!0 |220.220.222.-1|)
             (= a!14 (ip_constructor 220 220 222 (- 1))))
        (and (= x!0 |220.220.220.-1|)
             (= a!14 (ip_constructor 220 220 220 (- 1))))
        (and (= x!0 |202.0.0.-1|) (= a!14 (ip_constructor 202 0 0 (- 1))))
        (and (= x!0 |201.0.0.-1|) (= a!14 (ip_constructor 201 0 0 (- 1))))
        (and (= x!0 |200.0.0.-1|) (= a!14 (ip_constructor 200 0 0 (- 1))))
        (and (= x!0 |1.0.0.9|) (= a!14 (ip_constructor 1 0 0 9)))
        (and (= x!0 |17.56.27.-1|) (= a!14 (ip_constructor 17 56 27 (- 1))))
        (and (= x!0 |1.0.0.10|) (= a!14 (ip_constructor 1 0 0 10)))
        (and (= x!0 |1.0.0.11|) (= a!14 (ip_constructor 1 0 0 11)))
        (and (= x!0 |1.0.0.12|) (= a!14 (ip_constructor 1 0 0 12)))))))))))))))))))