%------------------------------------------------------------------------------ % File : Refute---2015 % Problem : SWV572-1 : TPTP v6.4.0. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : isabelle tptp_refute %d %s % Computer : n122.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 32218.75MB % OS : Linux 3.10.0-327.10.1.el7.x86_64 % CPULimit : 300s % DateTime : Thu Apr 14 05:29:37 EDT 2016 % Result : GaveUp 193.29s % Output : None % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV572-1 : TPTP v6.4.0. Released v4.1.0. % 0.00/0.04 % Command : isabelle tptp_refute %d %s % 0.03/0.23 % Computer : n122.star.cs.uiowa.edu % 0.03/0.23 % Model : x86_64 x86_64 % 0.03/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % 0.03/0.23 % Memory : 32218.75MB % 0.03/0.23 % OS : Linux 3.10.0-327.10.1.el7.x86_64 % 0.03/0.23 % CPULimit : 300 % 0.03/0.23 % DateTime : Fri Apr 8 17:22:24 CDT 2016 % 0.03/0.23 % CPUTime : % 6.32/5.83 > val it = (): unit % 7.03/6.56 Trying to find a model that refutes: True % 16.34/15.88 Unfolded term: [| !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 % 16.34/15.88 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27 X28 X29 X30 X31 X32 X33 X34 % 16.34/15.88 X35 X36 X37 X38 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 % 16.34/15.88 X52 X53 X54 X55 X56 X57 X58. % 16.34/15.88 bnd_ip (bnd_land U V) (bnd_land W X) (bnd_land Y Z) (bnd_land X1 X2) % 16.34/15.88 (bnd_land X3 X4) (bnd_land X5 X6) (bnd_land X7 X8) (bnd_land X9 X10) % 16.34/15.88 (bnd_land X11 X12) (bnd_land X13 X14) (bnd_land X15 X16) % 16.34/15.88 (bnd_land X17 X18) (bnd_land X19 X20) (bnd_land X21 X22) % 16.34/15.88 (bnd_land X23 X24) (bnd_land X25 X26) (bnd_land X27 X28) % 16.34/15.88 (bnd_land X29 X30) (bnd_land X31 X32) (bnd_land X33 X34) % 16.34/15.88 (bnd_land X35 X36) (bnd_land X37 X38) (bnd_land X39 X40) % 16.34/15.88 (bnd_land X41 X42) (bnd_land X43 X44) (bnd_land X45 X46) % 16.34/15.88 (bnd_land X47 X48) (bnd_land X49 X50) (bnd_land X51 X52) % 16.34/15.88 (bnd_land X53 X54) (bnd_land X55 X56) (bnd_land X57 X58) = % 16.34/15.88 bnd_ipand % 16.34/15.88 (bnd_ip U W Y X1 X3 X5 X7 X9 X11 X13 X15 X17 X19 X21 X23 X25 X27 X29 % 16.34/15.88 X31 X33 X35 X37 X39 X41 X43 X45 X47 X49 X51 X53 X55 X57) % 16.34/15.88 (bnd_ip V X Z X2 X4 X6 X8 X10 X12 X14 X16 X18 X20 X22 X24 X26 X28 X30 % 16.34/15.88 X32 X34 X36 X38 X40 X42 X44 X46 X48 X50 X52 X54 X56 X58); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16. % 16.34/15.88 (((((((~ bnd_ipand U V = W | ~ bnd_ipand X Y = Z) | % 16.34/15.88 ~ bnd_ssNetwork X1) | % 16.34/15.88 ~ bnd_ssNetwork X2) | % 16.34/15.88 ~ bnd_ssSent % 16.34/15.88 (bnd_epacket X2 X3 X4 bnd_e_ip % 16.34/15.88 (bnd_ippacket X U bnd_tcp % 16.34/15.88 (bnd_tcppacket X5 X6 bnd_syn X7)))) | % 16.34/15.88 ~ bnd_ssFirewall (bnd_firewall X8 X2 X1)) | % 16.34/15.88 ~ bnd_ssTCP_FirewallRule % 16.34/15.88 (bnd_tcp_fwrule X8 (bnd_next_rule X9) bnd_deny Z Y W V X5 X6)) | % 16.34/15.88 ~ bnd_ssTCP_NotMatched % 16.34/15.88 (bnd_tcp_not_matched X8 X2 X1 X3 X4 X U bnd_tcp X5 X6 bnd_syn X9 % 16.34/15.88 X10 X11 X12 X13 X14 X15 X16)) | % 16.34/15.88 bnd_ssDenied % 16.34/15.88 (bnd_denied X8 X2 X1 (bnd_next_rule X9) X3 X4 X U bnd_tcp % 16.34/15.88 (bnd_tcppacket X5 X6 bnd_syn X7)); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16. % 16.34/15.88 (((((((~ bnd_ipand U V = W | ~ bnd_ipand X Y = Z) | % 16.34/15.88 ~ bnd_ssNetwork X1) | % 16.34/15.88 ~ bnd_ssNetwork X2) | % 16.34/15.88 ~ bnd_ssSent % 16.34/15.88 (bnd_epacket X2 X3 X4 bnd_e_ip % 16.34/15.88 (bnd_ippacket X U bnd_tcp % 16.34/15.88 (bnd_tcppacket X5 X6 bnd_syn X7)))) | % 16.34/15.88 ~ bnd_ssFirewall (bnd_firewall X8 X2 X1)) | % 16.34/15.88 ~ bnd_ssTCP_FirewallRule % 16.34/15.88 (bnd_tcp_fwrule X8 (bnd_next_rule X9) bnd_permit Z Y W V X5 % 16.34/15.88 X6)) | % 16.34/15.88 ~ bnd_ssTCP_NotMatched % 16.34/15.88 (bnd_tcp_not_matched X8 X2 X1 X3 X4 X U bnd_tcp X5 X6 bnd_syn X9 % 16.34/15.88 X10 X11 X12 X13 X14 X15 X16)) | % 16.34/15.88 bnd_ssSent % 16.34/15.88 (bnd_epacket X1 X3 X4 bnd_e_ip % 16.34/15.88 (bnd_ippacket X U bnd_tcp (bnd_tcppacket X5 X6 bnd_syn X7))); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16. % 16.34/15.88 (((((((~ bnd_ipand U V = W | ~ bnd_ipand X Y = Z) | % 16.34/15.88 ~ bnd_ssNetwork X1) | % 16.34/15.88 ~ bnd_ssNetwork X2) | % 16.34/15.88 ~ bnd_ssSent % 16.34/15.88 (bnd_epacket X2 X3 X4 bnd_e_ip % 16.34/15.88 (bnd_ippacket X U bnd_udp (bnd_udppacket X5 X6 X7)))) | % 16.34/15.88 ~ bnd_ssFirewall (bnd_firewall X8 X2 X1)) | % 16.34/15.88 ~ bnd_ssUDP_FirewallRule % 16.34/15.88 (bnd_udp_fwrule X8 (bnd_next_rule X9) bnd_deny Z Y W V X5 X6)) | % 16.34/15.88 ~ bnd_ssUDP_NotMatched % 16.34/15.88 (bnd_udp_matched X8 X2 X1 X3 X4 X U bnd_udp X5 X6 X9 X10 X11 X12 % 16.34/15.88 X13 X14 X15 X16)) | % 16.34/15.88 bnd_ssDenied % 16.34/15.88 (bnd_denied X8 X2 X1 (bnd_next_rule X9) X3 X4 X U bnd_udp % 16.34/15.88 (bnd_udppacket X5 X6 X7)); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16. % 16.34/15.88 (((((((~ bnd_ipand U V = W | ~ bnd_ipand X Y = Z) | % 16.34/15.88 ~ bnd_ssNetwork X1) | % 16.34/15.88 ~ bnd_ssNetwork X2) | % 16.34/15.88 ~ bnd_ssSent % 16.34/15.88 (bnd_epacket X2 X3 X4 bnd_e_ip % 16.34/15.88 (bnd_ippacket X U bnd_udp (bnd_udppacket X5 X6 X7)))) | % 16.34/15.88 ~ bnd_ssFirewall (bnd_firewall X8 X2 X1)) | % 16.34/15.88 ~ bnd_ssUDP_FirewallRule % 16.34/15.88 (bnd_udp_fwrule X8 (bnd_next_rule X9) bnd_permit Z Y W V X5 % 16.34/15.88 X6)) | % 16.34/15.88 ~ bnd_ssUDP_NotMatched % 16.34/15.88 (bnd_udp_matched X8 X2 X1 X3 X4 X U bnd_udp X5 X6 X9 X10 X11 X12 % 16.34/15.88 X13 X14 X15 X16)) | % 16.34/15.88 bnd_ssSent % 16.34/15.88 (bnd_epacket X1 X3 X4 bnd_e_ip % 16.34/15.88 (bnd_ippacket X U bnd_udp (bnd_udppacket X5 X6 X7))); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16. % 16.34/15.88 (((((((~ bnd_ipand U V = W | ~ bnd_ipand X Y = Z) | % 16.34/15.88 ~ bnd_ssNetwork X1) | % 16.34/15.88 ~ bnd_ssNetwork X2) | % 16.34/15.88 ~ bnd_ssSent % 16.34/15.88 (bnd_epacket X2 X3 X4 bnd_e_ip % 16.34/15.88 (bnd_ippacket X U bnd_tcp % 16.34/15.88 (bnd_tcppacket X5 X6 bnd_syn X7)))) | % 16.34/15.88 ~ bnd_ssFirewall (bnd_firewall X8 X2 X1)) | % 16.34/15.88 ~ bnd_ssTCP_FirewallRule % 16.34/15.88 (bnd_tcp_fwrule X8 (bnd_next_rule X9) bnd_permit Z Y W V X5 % 16.34/15.88 X6)) | % 16.34/15.88 ~ bnd_ssTCP_NotMatched % 16.34/15.88 (bnd_tcp_not_matched X8 X2 X1 X3 X4 X U bnd_tcp X5 X6 bnd_syn X9 % 16.34/15.88 X10 X11 X12 X13 X14 X15 X16)) | % 16.34/15.88 bnd_ssTCP_ClientSynSent (bnd_tcp_clientsynsent X8 X U X5 X6); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16. % 16.34/15.88 (((((((~ bnd_ipand U V = W | ~ bnd_ipand X Y = Z) | % 16.34/15.88 ~ bnd_ssNetwork X1) | % 16.34/15.88 ~ bnd_ssNetwork X2) | % 16.34/15.88 ~ bnd_ssSent % 16.34/15.88 (bnd_epacket X2 X3 X4 bnd_e_ip % 16.34/15.88 (bnd_ippacket X U bnd_udp (bnd_udppacket X5 X6 X7)))) | % 16.34/15.88 ~ bnd_ssFirewall (bnd_firewall X8 X2 X1)) | % 16.34/15.88 ~ bnd_ssUDP_FirewallRule % 16.34/15.88 (bnd_udp_fwrule X8 (bnd_next_rule X9) bnd_permit Z Y W V X5 % 16.34/15.88 X6)) | % 16.34/15.88 ~ bnd_ssUDP_NotMatched % 16.34/15.88 (bnd_udp_matched X8 X2 X1 X3 X4 X U bnd_udp X5 X6 X9 X10 X11 X12 % 16.34/15.88 X13 X14 X15 X16)) | % 16.34/15.88 bnd_ssUDP_ConnectionOpen (bnd_udp_connection_open X8 X U X5 X6); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8. % 16.34/15.88 ((((((~ bnd_ipand U V = W | ~ bnd_ipand X Y = Z) | % 16.34/15.88 ~ bnd_ssNetwork X1) | % 16.34/15.88 ~ bnd_ssNetwork X2) | % 16.34/15.88 ~ bnd_ssSent % 16.34/15.88 (bnd_epacket X2 X3 X4 bnd_e_ip % 16.34/15.88 (bnd_ippacket X U bnd_tcp % 16.34/15.88 (bnd_tcppacket X5 X6 bnd_syn X7)))) | % 16.34/15.88 ~ bnd_ssTCP_FirewallRule % 16.34/15.88 (bnd_tcp_fwrule X8 bnd_first_rule bnd_deny Z Y W V X5 X6)) | % 16.34/15.88 ~ bnd_ssFirewall (bnd_firewall X8 X2 X1)) | % 16.34/15.88 bnd_ssDenied % 16.34/15.88 (bnd_denied X8 X2 X1 bnd_first_rule X3 X4 X U bnd_tcp % 16.34/15.88 (bnd_tcppacket X5 X6 bnd_syn X7)); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 % 16.34/15.88 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27 X28 X29 X30 X31 X32 X33 X34 % 16.34/15.88 X35 X36 X37 X38 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 % 16.34/15.88 X52 X53 X54 X55 X56. % 16.34/15.88 ~ bnd_ip U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 % 16.34/15.88 X15 X16 X17 X18 X19 X20 X21 X22 X23 X24 X25 bnd_n0 = % 16.34/15.88 bnd_ip X26 X27 X28 X29 X30 X31 X32 X33 X34 X35 X36 X37 X38 X39 X40 % 16.34/15.88 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 X52 X53 X54 X55 X56 % 16.34/15.88 bnd_n1; % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 % 16.34/15.88 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27 X28 X29 X30 X31 X32 X33 X34 % 16.34/15.88 X35 X36 X37 X38 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 % 16.34/15.88 X52 X53 X54 X55 X56. % 16.34/15.88 ~ bnd_ip U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 % 16.34/15.88 X15 X16 X17 X18 X19 X20 X21 X22 X23 X24 bnd_n0 X25 = % 16.34/15.88 bnd_ip X26 X27 X28 X29 X30 X31 X32 X33 X34 X35 X36 X37 X38 X39 X40 % 16.34/15.88 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 X52 X53 X54 X55 bnd_n1 % 16.34/15.88 X56; % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 % 16.34/15.88 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27 X28 X29 X30 X31 X32 X33 X34 % 16.34/15.88 X35 X36 X37 X38 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 % 16.34/15.88 X52 X53 X54 X55 X56. % 16.34/15.88 ~ bnd_ip U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 % 16.34/15.88 X15 X16 X17 X18 X19 X20 X21 X22 X23 bnd_n0 X24 X25 = % 16.34/15.88 bnd_ip X26 X27 X28 X29 X30 X31 X32 X33 X34 X35 X36 X37 X38 X39 X40 % 16.34/15.88 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 X52 X53 X54 bnd_n1 X55 % 16.34/15.88 X56; % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 % 16.34/15.88 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27 X28 X29 X30 X31 X32 X33 X34 % 16.34/15.88 X35 X36 X37 X38 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 % 16.34/15.88 X52 X53 X54 X55 X56. % 16.34/15.88 ~ bnd_ip U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 % 16.34/15.88 X15 X16 X17 X18 X19 X20 X21 X22 bnd_n0 X23 X24 X25 = % 16.34/15.88 bnd_ip X26 X27 X28 X29 X30 X31 X32 X33 X34 X35 X36 X37 X38 X39 X40 % 16.34/15.88 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 X52 X53 bnd_n1 X54 X55 % 16.34/15.88 X56; % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 % 16.34/15.88 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27 X28 X29 X30 X31 X32 X33 X34 % 16.34/15.88 X35 X36 X37 X38 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 % 16.34/15.88 X52 X53 X54 X55 X56. % 16.34/15.88 ~ bnd_ip U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 % 16.34/15.88 X15 X16 X17 X18 X19 X20 X21 bnd_n0 X22 X23 X24 X25 = % 16.34/15.88 bnd_ip X26 X27 X28 X29 X30 X31 X32 X33 X34 X35 X36 X37 X38 X39 X40 % 16.34/15.88 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 X52 bnd_n1 X53 X54 X55 % 16.34/15.88 X56; % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 % 16.34/15.88 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27 X28 X29 X30 X31 X32 X33 X34 % 16.34/15.88 X35 X36 X37 X38 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 % 16.34/15.88 X52 X53 X54 X55 X56. % 16.34/15.88 ~ bnd_ip U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 % 16.34/15.88 X15 X16 X17 X18 X19 X20 bnd_n0 X21 X22 X23 X24 X25 = % 16.34/15.88 bnd_ip X26 X27 X28 X29 X30 X31 X32 X33 X34 X35 X36 X37 X38 X39 X40 % 16.34/15.88 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 bnd_n1 X52 X53 X54 X55 % 16.34/15.88 X56; % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 % 16.34/15.88 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27 X28 X29 X30 X31 X32 X33 X34 % 16.34/15.88 X35 X36 X37 X38 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 % 16.34/15.88 X52 X53 X54 X55 X56. % 16.34/15.88 ~ bnd_ip U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 % 16.34/15.88 X15 X16 X17 X18 X19 bnd_n0 X20 X21 X22 X23 X24 X25 = % 16.34/15.88 bnd_ip X26 X27 X28 X29 X30 X31 X32 X33 X34 X35 X36 X37 X38 X39 X40 % 16.34/15.88 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 bnd_n1 X51 X52 X53 X54 X55 % 16.34/15.88 X56; % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 % 16.34/15.88 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27 X28 X29 X30 X31 X32 X33 X34 % 16.34/15.88 X35 X36 X37 X38 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 % 16.34/15.88 X52 X53 X54 X55 X56. % 16.34/15.88 ~ bnd_ip U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 % 16.34/15.88 X15 X16 X17 X18 bnd_n0 X19 X20 X21 X22 X23 X24 X25 = % 16.34/15.88 bnd_ip X26 X27 X28 X29 X30 X31 X32 X33 X34 X35 X36 X37 X38 X39 X40 % 16.34/15.88 X41 X42 X43 X44 X45 X46 X47 X48 X49 bnd_n1 X50 X51 X52 X53 X54 X55 % 16.34/15.88 X56; % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 % 16.34/15.88 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27 X28 X29 X30 X31 X32 X33 X34 % 16.34/15.88 X35 X36 X37 X38 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 % 16.34/15.88 X52 X53 X54 X55 X56. % 16.34/15.88 ~ bnd_ip U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 % 16.34/15.88 X15 X16 X17 bnd_n0 X18 X19 X20 X21 X22 X23 X24 X25 = % 16.34/15.88 bnd_ip X26 X27 X28 X29 X30 X31 X32 X33 X34 X35 X36 X37 X38 X39 X40 % 16.34/15.88 X41 X42 X43 X44 X45 X46 X47 X48 bnd_n1 X49 X50 X51 X52 X53 X54 X55 % 16.34/15.88 X56; % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 % 16.34/15.88 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27 X28 X29 X30 X31 X32 X33 X34 % 16.34/15.88 X35 X36 X37 X38 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 % 16.34/15.88 X52 X53 X54 X55 X56. % 16.34/15.88 ~ bnd_ip U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 % 16.34/15.88 X15 X16 bnd_n0 X17 X18 X19 X20 X21 X22 X23 X24 X25 = % 16.34/15.88 bnd_ip X26 X27 X28 X29 X30 X31 X32 X33 X34 X35 X36 X37 X38 X39 X40 % 16.34/15.88 X41 X42 X43 X44 X45 X46 X47 bnd_n1 X48 X49 X50 X51 X52 X53 X54 X55 % 16.34/15.88 X56; % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 % 16.34/15.88 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27 X28 X29 X30 X31 X32 X33 X34 % 16.34/15.88 X35 X36 X37 X38 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 % 16.34/15.88 X52 X53 X54 X55 X56. % 16.34/15.88 ~ bnd_ip U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 % 16.34/15.88 X15 bnd_n0 X16 X17 X18 X19 X20 X21 X22 X23 X24 X25 = % 16.34/15.88 bnd_ip X26 X27 X28 X29 X30 X31 X32 X33 X34 X35 X36 X37 X38 X39 X40 % 16.34/15.88 X41 X42 X43 X44 X45 X46 bnd_n1 X47 X48 X49 X50 X51 X52 X53 X54 X55 % 16.34/15.88 X56; % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 % 16.34/15.88 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27 X28 X29 X30 X31 X32 X33 X34 % 16.34/15.88 X35 X36 X37 X38 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 % 16.34/15.88 X52 X53 X54 X55 X56. % 16.34/15.88 ~ bnd_ip U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 % 16.34/15.88 bnd_n0 X15 X16 X17 X18 X19 X20 X21 X22 X23 X24 X25 = % 16.34/15.88 bnd_ip X26 X27 X28 X29 X30 X31 X32 X33 X34 X35 X36 X37 X38 X39 X40 % 16.34/15.88 X41 X42 X43 X44 X45 bnd_n1 X46 X47 X48 X49 X50 X51 X52 X53 X54 X55 % 16.34/15.88 X56; % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 % 16.34/15.88 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27 X28 X29 X30 X31 X32 X33 X34 % 16.34/15.88 X35 X36 X37 X38 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 % 16.34/15.88 X52 X53 X54 X55 X56. % 16.34/15.88 ~ bnd_ip U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 bnd_n0 % 16.34/15.88 X14 X15 X16 X17 X18 X19 X20 X21 X22 X23 X24 X25 = % 16.34/15.88 bnd_ip X26 X27 X28 X29 X30 X31 X32 X33 X34 X35 X36 X37 X38 X39 X40 % 16.34/15.88 X41 X42 X43 X44 bnd_n1 X45 X46 X47 X48 X49 X50 X51 X52 X53 X54 X55 % 16.34/15.88 X56; % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 % 16.34/15.88 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27 X28 X29 X30 X31 X32 X33 X34 % 16.34/15.88 X35 X36 X37 X38 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 % 16.34/15.88 X52 X53 X54 X55 X56. % 16.34/15.88 ~ bnd_ip U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 bnd_n0 X13 % 16.34/15.88 X14 X15 X16 X17 X18 X19 X20 X21 X22 X23 X24 X25 = % 16.34/15.88 bnd_ip X26 X27 X28 X29 X30 X31 X32 X33 X34 X35 X36 X37 X38 X39 X40 % 16.34/15.88 X41 X42 X43 bnd_n1 X44 X45 X46 X47 X48 X49 X50 X51 X52 X53 X54 X55 % 16.34/15.88 X56; % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 % 16.34/15.88 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27 X28 X29 X30 X31 X32 X33 X34 % 16.34/15.88 X35 X36 X37 X38 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 % 16.34/15.88 X52 X53 X54 X55 X56. % 16.34/15.88 ~ bnd_ip U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 bnd_n0 X12 X13 % 16.34/15.88 X14 X15 X16 X17 X18 X19 X20 X21 X22 X23 X24 X25 = % 16.34/15.88 bnd_ip X26 X27 X28 X29 X30 X31 X32 X33 X34 X35 X36 X37 X38 X39 X40 % 16.34/15.88 X41 X42 bnd_n1 X43 X44 X45 X46 X47 X48 X49 X50 X51 X52 X53 X54 X55 % 16.34/15.88 X56; % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 % 16.34/15.88 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27 X28 X29 X30 X31 X32 X33 X34 % 16.34/15.88 X35 X36 X37 X38 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 % 16.34/15.88 X52 X53 X54 X55 X56. % 16.34/15.88 ~ bnd_ip U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 bnd_n0 X11 X12 X13 % 16.34/15.88 X14 X15 X16 X17 X18 X19 X20 X21 X22 X23 X24 X25 = % 16.34/15.88 bnd_ip X26 X27 X28 X29 X30 X31 X32 X33 X34 X35 X36 X37 X38 X39 X40 % 16.34/15.88 X41 bnd_n1 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 X52 X53 X54 X55 % 16.34/15.88 X56; % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 % 16.34/15.88 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27 X28 X29 X30 X31 X32 X33 X34 % 16.34/15.88 X35 X36 X37 X38 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 % 16.34/15.88 X52 X53 X54 X55 X56. % 16.34/15.88 ~ bnd_ip U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 bnd_n0 X10 X11 X12 X13 % 16.34/15.88 X14 X15 X16 X17 X18 X19 X20 X21 X22 X23 X24 X25 = % 16.34/15.88 bnd_ip X26 X27 X28 X29 X30 X31 X32 X33 X34 X35 X36 X37 X38 X39 X40 % 16.34/15.88 bnd_n1 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 X52 X53 X54 X55 % 16.34/15.88 X56; % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 % 16.34/15.88 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27 X28 X29 X30 X31 X32 X33 X34 % 16.34/15.88 X35 X36 X37 X38 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 % 16.34/15.88 X52 X53 X54 X55 X56. % 16.34/15.88 ~ bnd_ip U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 bnd_n0 X9 X10 X11 X12 X13 % 16.34/15.88 X14 X15 X16 X17 X18 X19 X20 X21 X22 X23 X24 X25 = % 16.34/15.88 bnd_ip X26 X27 X28 X29 X30 X31 X32 X33 X34 X35 X36 X37 X38 X39 % 16.34/15.88 bnd_n1 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 X52 X53 X54 % 16.34/15.88 X55 X56; % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 % 16.34/15.88 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27 X28 X29 X30 X31 X32 X33 X34 % 16.34/15.88 X35 X36 X37 X38 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 % 16.34/15.88 X52 X53 X54 X55 X56. % 16.34/15.88 ~ bnd_ip U V W X Y Z X1 X2 X3 X4 X5 X6 X7 bnd_n0 X8 X9 X10 X11 X12 X13 % 16.34/15.88 X14 X15 X16 X17 X18 X19 X20 X21 X22 X23 X24 X25 = % 16.34/15.88 bnd_ip X26 X27 X28 X29 X30 X31 X32 X33 X34 X35 X36 X37 X38 bnd_n1 % 16.34/15.88 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 X52 X53 X54 X55 % 16.34/15.88 X56; % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 % 16.34/15.88 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27 X28 X29 X30 X31 X32 X33 X34 % 16.34/15.88 X35 X36 X37 X38 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 % 16.34/15.88 X52 X53 X54 X55 X56. % 16.34/15.88 ~ bnd_ip U V W X Y Z X1 X2 X3 X4 X5 X6 bnd_n0 X7 X8 X9 X10 X11 X12 X13 % 16.34/15.88 X14 X15 X16 X17 X18 X19 X20 X21 X22 X23 X24 X25 = % 16.34/15.88 bnd_ip X26 X27 X28 X29 X30 X31 X32 X33 X34 X35 X36 X37 bnd_n1 X38 % 16.34/15.88 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 X52 X53 X54 X55 % 16.34/15.88 X56; % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 % 16.34/15.88 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27 X28 X29 X30 X31 X32 X33 X34 % 16.34/15.88 X35 X36 X37 X38 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 % 16.34/15.88 X52 X53 X54 X55 X56. % 16.34/15.88 ~ bnd_ip U V W X Y Z X1 X2 X3 X4 X5 bnd_n0 X6 X7 X8 X9 X10 X11 X12 X13 % 16.34/15.88 X14 X15 X16 X17 X18 X19 X20 X21 X22 X23 X24 X25 = % 16.34/15.88 bnd_ip X26 X27 X28 X29 X30 X31 X32 X33 X34 X35 X36 bnd_n1 X37 X38 % 16.34/15.88 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 X52 X53 X54 X55 % 16.34/15.88 X56; % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 % 16.34/15.88 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27 X28 X29 X30 X31 X32 X33 X34 % 16.34/15.88 X35 X36 X37 X38 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 % 16.34/15.88 X52 X53 X54 X55 X56. % 16.34/15.88 ~ bnd_ip U V W X Y Z X1 X2 X3 X4 bnd_n0 X5 X6 X7 X8 X9 X10 X11 X12 X13 % 16.34/15.88 X14 X15 X16 X17 X18 X19 X20 X21 X22 X23 X24 X25 = % 16.34/15.88 bnd_ip X26 X27 X28 X29 X30 X31 X32 X33 X34 X35 bnd_n1 X36 X37 X38 % 16.34/15.88 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 X52 X53 X54 X55 % 16.34/15.88 X56; % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 % 16.34/15.88 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27 X28 X29 X30 X31 X32 X33 X34 % 16.34/15.88 X35 X36 X37 X38 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 % 16.34/15.88 X52 X53 X54 X55 X56. % 16.34/15.88 ~ bnd_ip U V W X Y Z X1 bnd_n0 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 % 16.34/15.88 X14 X15 X16 X17 X18 X19 X20 X21 X22 X23 X24 X25 = % 16.34/15.88 bnd_ip X26 X27 X28 X29 X30 X31 X32 bnd_n1 X33 X34 X35 X36 X37 X38 % 16.34/15.88 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 X52 X53 X54 X55 % 16.34/15.88 X56; % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 % 16.34/15.88 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27 X28 X29 X30 X31 X32 X33 X34 % 16.34/15.88 X35 X36 X37 X38 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 % 16.34/15.88 X52 X53 X54 X55 X56. % 16.34/15.88 ~ bnd_ip U V W X Y Z bnd_n0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 % 16.34/15.88 X14 X15 X16 X17 X18 X19 X20 X21 X22 X23 X24 X25 = % 16.34/15.88 bnd_ip X26 X27 X28 X29 X30 X31 bnd_n1 X32 X33 X34 X35 X36 X37 X38 % 16.34/15.88 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 X52 X53 X54 X55 % 16.34/15.88 X56; % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 % 16.34/15.88 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27 X28 X29 X30 X31 X32 X33 X34 % 16.34/15.88 X35 X36 X37 X38 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 % 16.34/15.88 X52 X53 X54 X55 X56. % 16.34/15.88 ~ bnd_ip U V W X Y bnd_n0 Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 % 16.34/15.88 X14 X15 X16 X17 X18 X19 X20 X21 X22 X23 X24 X25 = % 16.34/15.88 bnd_ip X26 X27 X28 X29 X30 bnd_n1 X31 X32 X33 X34 X35 X36 X37 X38 % 16.34/15.88 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 X52 X53 X54 X55 % 16.34/15.88 X56; % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 % 16.34/15.88 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27 X28 X29 X30 X31 X32 X33 X34 % 16.34/15.88 X35 X36 X37 X38 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 % 16.34/15.88 X52 X53 X54 X55 X56. % 16.34/15.88 ~ bnd_ip U V W X bnd_n0 Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 % 16.34/15.88 X14 X15 X16 X17 X18 X19 X20 X21 X22 X23 X24 X25 = % 16.34/15.88 bnd_ip X26 X27 X28 X29 bnd_n1 X30 X31 X32 X33 X34 X35 X36 X37 X38 % 16.34/15.88 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 X52 X53 X54 X55 % 16.34/15.88 X56; % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 % 16.34/15.88 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27 X28 X29 X30 X31 X32 X33 X34 % 16.34/15.88 X35 X36 X37 X38 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 % 16.34/15.88 X52 X53 X54 X55 X56. % 16.34/15.88 ~ bnd_ip U V W bnd_n0 X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 % 16.34/15.88 X14 X15 X16 X17 X18 X19 X20 X21 X22 X23 X24 X25 = % 16.34/15.88 bnd_ip X26 X27 X28 bnd_n1 X29 X30 X31 X32 X33 X34 X35 X36 X37 X38 % 16.34/15.88 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 X52 X53 X54 X55 % 16.34/15.88 X56; % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 % 16.34/15.88 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27 X28 X29 X30 X31 X32 X33 X34 % 16.34/15.88 X35 X36 X37 X38 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 % 16.34/15.88 X52 X53 X54 X55 X56. % 16.34/15.88 ~ bnd_ip U V bnd_n0 W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 % 16.34/15.88 X14 X15 X16 X17 X18 X19 X20 X21 X22 X23 X24 X25 = % 16.34/15.88 bnd_ip X26 X27 bnd_n1 X28 X29 X30 X31 X32 X33 X34 X35 X36 X37 X38 % 16.34/15.88 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 X52 X53 X54 X55 % 16.34/15.88 X56; % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 % 16.34/15.88 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27 X28 X29 X30 X31 X32 X33 X34 % 16.34/15.88 X35 X36 X37 X38 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 % 16.34/15.88 X52 X53 X54 X55 X56. % 16.34/15.88 ~ bnd_ip U bnd_n0 V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 % 16.34/15.88 X14 X15 X16 X17 X18 X19 X20 X21 X22 X23 X24 X25 = % 16.34/15.88 bnd_ip X26 bnd_n1 X27 X28 X29 X30 X31 X32 X33 X34 X35 X36 X37 X38 % 16.34/15.88 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 X52 X53 X54 X55 % 16.34/15.88 X56; % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 % 16.34/15.88 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27 X28 X29 X30 X31 X32 X33 X34 % 16.34/15.88 X35 X36 X37 X38 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 % 16.34/15.88 X52 X53 X54 X55 X56. % 16.34/15.88 ~ bnd_ip bnd_n0 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 % 16.34/15.88 X14 X15 X16 X17 X18 X19 X20 X21 X22 X23 X24 X25 = % 16.34/15.88 bnd_ip bnd_n1 X26 X27 X28 X29 X30 X31 X32 X33 X34 X35 X36 X37 X38 % 16.34/15.88 X39 X40 X41 X42 X43 X44 X45 X46 X47 X48 X49 X50 X51 X52 X53 X54 X55 % 16.34/15.88 X56; % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8. % 16.34/15.88 ((((((~ bnd_ipand U V = W | ~ bnd_ipand X Y = Z) | % 16.34/15.88 ~ bnd_ssNetwork X1) | % 16.34/15.88 ~ bnd_ssNetwork X2) | % 16.34/15.88 ~ bnd_ssSent % 16.34/15.88 (bnd_epacket X2 X3 X4 bnd_e_ip % 16.34/15.88 (bnd_ippacket X U bnd_tcp % 16.34/15.88 (bnd_tcppacket X5 X6 bnd_syn X7)))) | % 16.34/15.88 ~ bnd_ssTCP_FirewallRule % 16.34/15.88 (bnd_tcp_fwrule X8 bnd_first_rule bnd_permit Z Y W V X5 X6)) | % 16.34/15.88 ~ bnd_ssFirewall (bnd_firewall X8 X2 X1)) | % 16.34/15.88 bnd_ssSent % 16.34/15.88 (bnd_epacket X1 X3 X4 bnd_e_ip % 16.34/15.88 (bnd_ippacket X U bnd_tcp (bnd_tcppacket X5 X6 bnd_syn X7))); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8. % 16.34/15.88 ((((((~ bnd_ipand U V = W | ~ bnd_ipand X Y = Z) | % 16.34/15.88 ~ bnd_ssNetwork X1) | % 16.34/15.88 ~ bnd_ssNetwork X2) | % 16.34/15.88 ~ bnd_ssSent % 16.34/15.88 (bnd_epacket X2 X3 X4 bnd_e_ip % 16.34/15.88 (bnd_ippacket X U bnd_udp (bnd_udppacket X5 X6 X7)))) | % 16.34/15.88 ~ bnd_ssUDP_FirewallRule % 16.34/15.88 (bnd_udp_fwrule X8 bnd_first_rule bnd_deny Z Y W V X5 X6)) | % 16.34/15.88 ~ bnd_ssFirewall (bnd_firewall X8 X2 X1)) | % 16.34/15.88 bnd_ssDenied % 16.34/15.88 (bnd_denied X8 X2 X1 bnd_first_rule X3 X4 X U bnd_udp % 16.34/15.88 (bnd_udppacket X5 X6 X7)); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12. % 16.34/15.88 (((((~ bnd_ssNetwork U | ~ bnd_ssNetwork V) | % 16.34/15.88 ~ bnd_ssFirewall (bnd_firewall W V U)) | % 16.34/15.88 ~ bnd_ssTCP_FirewallRule (bnd_tcp_fwrule W X Y Z X1 X2 X3 X4 X5)) | % 16.34/15.88 ~ bnd_ssSent % 16.34/15.88 (bnd_epacket V X6 X7 bnd_e_ip % 16.34/15.88 (bnd_ippacket X8 X9 bnd_tcp % 16.34/15.88 (bnd_tcppacket X10 X11 bnd_syn X12)))) | % 16.34/15.88 bnd_ipand X9 X3 = X2) | % 16.34/15.88 bnd_ssTCP_NotMatched % 16.34/15.88 (bnd_tcp_not_matched W V U X6 X7 X8 X9 bnd_tcp X10 X11 bnd_syn X Y Z % 16.34/15.88 X1 X2 X3 X4 X5); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12. % 16.34/15.88 (((((~ bnd_ssNetwork U | ~ bnd_ssNetwork V) | % 16.34/15.88 ~ bnd_ssFirewall (bnd_firewall W V U)) | % 16.34/15.88 ~ bnd_ssTCP_FirewallRule (bnd_tcp_fwrule W X Y Z X1 X2 X3 X4 X5)) | % 16.34/15.88 ~ bnd_ssSent % 16.34/15.88 (bnd_epacket V X6 X7 bnd_e_ip % 16.34/15.88 (bnd_ippacket X8 X9 bnd_tcp % 16.34/15.88 (bnd_tcppacket X10 X11 bnd_syn X12)))) | % 16.34/15.88 bnd_ipand X8 X1 = Z) | % 16.34/15.88 bnd_ssTCP_NotMatched % 16.34/15.88 (bnd_tcp_not_matched W V U X6 X7 X8 X9 bnd_tcp X10 X11 bnd_syn X Y Z % 16.34/15.88 X1 X2 X3 X4 X5); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8. % 16.34/15.88 ((((((~ bnd_ipand U V = W | ~ bnd_ipand X Y = Z) | % 16.34/15.88 ~ bnd_ssNetwork X1) | % 16.34/15.88 ~ bnd_ssNetwork X2) | % 16.34/15.88 ~ bnd_ssSent % 16.34/15.88 (bnd_epacket X2 X3 X4 bnd_e_ip % 16.34/15.88 (bnd_ippacket X U bnd_udp (bnd_udppacket X5 X6 X7)))) | % 16.34/15.88 ~ bnd_ssUDP_FirewallRule % 16.34/15.88 (bnd_udp_fwrule X8 bnd_first_rule bnd_permit Z Y W V X5 X6)) | % 16.34/15.88 ~ bnd_ssFirewall (bnd_firewall X8 X2 X1)) | % 16.34/15.88 bnd_ssSent % 16.34/15.88 (bnd_epacket X1 X3 X4 bnd_e_ip % 16.34/15.88 (bnd_ippacket X U bnd_udp (bnd_udppacket X5 X6 X7))); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12. % 16.34/15.88 (((((~ bnd_ssNetwork U | ~ bnd_ssNetwork V) | % 16.34/15.88 ~ bnd_ssFirewall (bnd_firewall W V U)) | % 16.34/15.88 ~ bnd_ssUDP_FirewallRule (bnd_udp_fwrule W X Y Z X1 X2 X3 X4 X5)) | % 16.34/15.88 ~ bnd_ssSent % 16.34/15.88 (bnd_epacket V X6 X7 bnd_e_ip % 16.34/15.88 (bnd_ippacket X8 X9 bnd_udp (bnd_udppacket X10 X11 X12)))) | % 16.34/15.88 bnd_ipand X9 X3 = X2) | % 16.34/15.88 bnd_ssUDP_NotMatched % 16.34/15.88 (bnd_udp_matched W V U X6 X7 X8 X9 bnd_udp X10 X11 X Y Z X1 X2 X3 X4 % 16.34/15.88 X5); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12. % 16.34/15.88 (((((~ bnd_ssNetwork U | ~ bnd_ssNetwork V) | % 16.34/15.88 ~ bnd_ssFirewall (bnd_firewall W V U)) | % 16.34/15.88 ~ bnd_ssUDP_FirewallRule (bnd_udp_fwrule W X Y Z X1 X2 X3 X4 X5)) | % 16.34/15.88 ~ bnd_ssSent % 16.34/15.88 (bnd_epacket V X6 X7 bnd_e_ip % 16.34/15.88 (bnd_ippacket X8 X9 bnd_udp (bnd_udppacket X10 X11 X12)))) | % 16.34/15.88 bnd_ipand X8 X1 = Z) | % 16.34/15.88 bnd_ssUDP_NotMatched % 16.34/15.88 (bnd_udp_matched W V U X6 X7 X8 X9 bnd_udp X10 X11 X Y Z X1 X2 X3 X4 % 16.34/15.88 X5); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12. % 16.34/15.88 (((((~ bnd_ssNetwork U | ~ bnd_ssNetwork V) | % 16.34/15.88 ~ bnd_ssFirewall (bnd_firewall W V U)) | % 16.34/15.88 ~ bnd_ssTCP_FirewallRule (bnd_tcp_fwrule W X Y Z X1 X2 X3 X4 X5)) | % 16.34/15.88 ~ bnd_ssSent % 16.34/15.88 (bnd_epacket V X6 X7 bnd_e_ip % 16.34/15.88 (bnd_ippacket X8 X9 bnd_tcp % 16.34/15.88 (bnd_tcppacket X10 X11 bnd_syn X12)))) | % 16.34/15.88 X11 = X5) | % 16.34/15.88 bnd_ssTCP_NotMatched % 16.34/15.88 (bnd_tcp_not_matched W V U X6 X7 X8 X9 bnd_tcp X10 X11 bnd_syn X Y Z % 16.34/15.88 X1 X2 X3 X4 X5); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12. % 16.34/15.88 (((((~ bnd_ssNetwork U | ~ bnd_ssNetwork V) | % 16.34/15.88 ~ bnd_ssFirewall (bnd_firewall W V U)) | % 16.34/15.88 ~ bnd_ssTCP_FirewallRule (bnd_tcp_fwrule W X Y Z X1 X2 X3 X4 X5)) | % 16.34/15.88 ~ bnd_ssSent % 16.34/15.88 (bnd_epacket V X6 X7 bnd_e_ip % 16.34/15.88 (bnd_ippacket X8 X9 bnd_tcp % 16.34/15.88 (bnd_tcppacket X10 X11 bnd_syn X12)))) | % 16.34/15.88 X10 = X4) | % 16.34/15.88 bnd_ssTCP_NotMatched % 16.34/15.88 (bnd_tcp_not_matched W V U X6 X7 X8 X9 bnd_tcp X10 X11 bnd_syn X Y Z % 16.34/15.88 X1 X2 X3 X4 X5); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12. % 16.34/15.88 (((((~ bnd_ssNetwork U | ~ bnd_ssNetwork V) | % 16.34/15.88 ~ bnd_ssFirewall (bnd_firewall W V U)) | % 16.34/15.88 ~ bnd_ssUDP_FirewallRule (bnd_udp_fwrule W X Y Z X1 X2 X3 X4 X5)) | % 16.34/15.88 ~ bnd_ssSent % 16.34/15.88 (bnd_epacket V X6 X7 bnd_e_ip % 16.34/15.88 (bnd_ippacket X8 X9 bnd_udp (bnd_udppacket X10 X11 X12)))) | % 16.34/15.88 X11 = X5) | % 16.34/15.88 bnd_ssUDP_NotMatched % 16.34/15.88 (bnd_udp_matched W V U X6 X7 X8 X9 bnd_udp X10 X11 X Y Z X1 X2 X3 X4 % 16.34/15.88 X5); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12. % 16.34/15.88 (((((~ bnd_ssNetwork U | ~ bnd_ssNetwork V) | % 16.34/15.88 ~ bnd_ssFirewall (bnd_firewall W V U)) | % 16.34/15.88 ~ bnd_ssUDP_FirewallRule (bnd_udp_fwrule W X Y Z X1 X2 X3 X4 X5)) | % 16.34/15.88 ~ bnd_ssSent % 16.34/15.88 (bnd_epacket V X6 X7 bnd_e_ip % 16.34/15.88 (bnd_ippacket X8 X9 bnd_udp (bnd_udppacket X10 X11 X12)))) | % 16.34/15.88 X10 = X4) | % 16.34/15.88 bnd_ssUDP_NotMatched % 16.34/15.88 (bnd_udp_matched W V U X6 X7 X8 X9 bnd_udp X10 X11 X Y Z X1 X2 X3 X4 % 16.34/15.88 X5); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8. % 16.34/15.88 ((((((~ bnd_ipand U V = W | ~ bnd_ipand X Y = Z) | % 16.34/15.88 ~ bnd_ssNetwork X1) | % 16.34/15.88 ~ bnd_ssNetwork X2) | % 16.34/15.88 ~ bnd_ssSent % 16.34/15.88 (bnd_epacket X2 X3 X4 bnd_e_ip % 16.34/15.88 (bnd_ippacket X U bnd_tcp % 16.34/15.88 (bnd_tcppacket X5 X6 bnd_syn X7)))) | % 16.34/15.88 ~ bnd_ssTCP_FirewallRule % 16.34/15.88 (bnd_tcp_fwrule X8 bnd_first_rule bnd_permit Z Y W V X5 X6)) | % 16.34/15.88 ~ bnd_ssFirewall (bnd_firewall X8 X2 X1)) | % 16.34/15.88 bnd_ssTCP_ClientSynSent (bnd_tcp_clientsynsent X8 X U X5 X6); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8. % 16.34/15.88 ((((((~ bnd_ipand U V = W | ~ bnd_ipand X Y = Z) | % 16.34/15.88 ~ bnd_ssNetwork X1) | % 16.34/15.88 ~ bnd_ssNetwork X2) | % 16.34/15.88 ~ bnd_ssSent % 16.34/15.88 (bnd_epacket X2 X3 X4 bnd_e_ip % 16.34/15.88 (bnd_ippacket X U bnd_udp (bnd_udppacket X5 X6 X7)))) | % 16.34/15.88 ~ bnd_ssUDP_FirewallRule % 16.34/15.88 (bnd_udp_fwrule X8 bnd_first_rule bnd_permit Z Y W V X5 X6)) | % 16.34/15.88 ~ bnd_ssFirewall (bnd_firewall X8 X2 X1)) | % 16.34/15.88 bnd_ssUDP_ConnectionOpen (bnd_udp_connection_open X8 X U X5 X6); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6. % 16.34/15.88 (((((~ bnd_ipand U V = W | ~ bnd_ipand X Y = bnd_ipand U Y) | % 16.34/15.88 ~ bnd_ssNotForwarded % 16.34/15.88 (bnd_not_forwarded (bnd_ippacket Z U X1 X2) X3)) | % 16.34/15.88 ~ bnd_ssRouteEntry % 16.34/15.88 (bnd_route X4 V W bnd_local (bnd_next_route X3))) | % 16.34/15.88 ~ bnd_ssRouteIPPacket % 16.34/15.88 (bnd_route_ip_packet X4 (bnd_ippacket Z U X1 X2))) | % 16.34/15.88 ~ bnd_ssInterface (bnd_interface X4 X Y X5 X6)) | % 16.34/15.88 bnd_ssSendIPPacket (bnd_send_ip_packet X4 U (bnd_ippacket Z U X1 X2)); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7. % 16.34/15.88 (((((~ bnd_ipand U V = W | % 16.34/15.88 ~ bnd_ssNotForwarded % 16.34/15.88 (bnd_not_forwarded (bnd_ippacket X U Y Z) X1)) | % 16.34/15.88 ~ bnd_ipand X2 X3 = bnd_ipand X4 X3) | % 16.34/15.88 ~ bnd_ssRouteEntry (bnd_route X5 V W X4 (bnd_next_route X1))) | % 16.34/15.88 ~ bnd_ssRouteIPPacket % 16.34/15.88 (bnd_route_ip_packet X5 (bnd_ippacket X U Y Z))) | % 16.34/15.88 ~ bnd_ssInterface (bnd_interface X5 X2 X3 X6 X7)) | % 16.34/15.88 bnd_ssSendIPPacket (bnd_send_ip_packet X5 X4 (bnd_ippacket X U Y Z)); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4. % 16.34/15.88 ((((~ bnd_ssNetwork U | ~ bnd_ssNetwork V) | % 16.34/15.88 ~ bnd_ssSent % 16.34/15.88 (bnd_epacket V W X bnd_e_ip % 16.34/15.88 (bnd_ippacket Y Z bnd_tcp % 16.34/15.88 (bnd_tcppacket X1 X2 bnd_finack X3)))) | % 16.34/15.88 ~ bnd_ssTCP_Connection_HalfClosed % 16.34/15.88 (bnd_tcp_connection_halfclosed X4 Y Z X1 X2)) | % 16.34/15.88 ~ bnd_ssFirewall (bnd_firewall X4 V U)) | % 16.34/15.88 bnd_ssSent % 16.34/15.88 (bnd_epacket U W X bnd_e_ip % 16.34/15.88 (bnd_ippacket Y Z bnd_tcp (bnd_tcppacket X1 X2 bnd_finack X3))); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4. % 16.34/15.88 ((((~ bnd_ssNetwork U | ~ bnd_ssNetwork V) | % 16.34/15.88 ~ bnd_ssSent % 16.34/15.88 (bnd_epacket V W X bnd_e_ip % 16.34/15.88 (bnd_ippacket Y Z bnd_tcp % 16.34/15.88 (bnd_tcppacket X1 X2 bnd_fin X3)))) | % 16.34/15.88 ~ bnd_ssTCP_Connection_Open % 16.34/15.88 (bnd_tcp_connection_open X4 Z Y X1 X2)) | % 16.34/15.88 ~ bnd_ssFirewall (bnd_firewall X4 V U)) | % 16.34/15.88 bnd_ssSent % 16.34/15.88 (bnd_epacket U W X bnd_e_ip % 16.34/15.88 (bnd_ippacket Y Z bnd_tcp (bnd_tcppacket X1 X2 bnd_fin X3))); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4. % 16.34/15.88 ((((~ bnd_ssNetwork U | ~ bnd_ssNetwork V) | % 16.34/15.88 ~ bnd_ssSent % 16.34/15.88 (bnd_epacket V W X bnd_e_ip % 16.34/15.88 (bnd_ippacket Y Z bnd_tcp % 16.34/15.88 (bnd_tcppacket X1 X2 bnd_fin X3)))) | % 16.34/15.88 ~ bnd_ssTCP_Connection_Open % 16.34/15.88 (bnd_tcp_connection_open X4 Y Z X1 X2)) | % 16.34/15.88 ~ bnd_ssFirewall (bnd_firewall X4 V U)) | % 16.34/15.88 bnd_ssSent % 16.34/15.88 (bnd_epacket U W X bnd_e_ip % 16.34/15.88 (bnd_ippacket Y Z bnd_tcp (bnd_tcppacket X1 X2 bnd_fin X3))); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5. % 16.34/15.88 ((((~ bnd_ssNetwork U | % 16.34/15.88 ~ bnd_ssSent % 16.34/15.88 (bnd_epacket V W X bnd_e_ip % 16.34/15.88 (bnd_ippacket Y Z bnd_tcp % 16.34/15.88 (bnd_tcppacket X1 X2 bnd_no_syn X3)))) | % 16.34/15.88 ~ bnd_ssNetwork V) | % 16.34/15.88 ~ bnd_ssTCP_Connection_Open % 16.34/15.88 (bnd_tcp_connection_open X4 Z Y X2 X1)) | % 16.34/15.88 ~ bnd_ssFirewall (bnd_firewall X4 V U)) | % 16.34/15.88 bnd_ssSent % 16.34/15.88 (bnd_epacket U W X bnd_e_ip % 16.34/15.88 (bnd_ippacket Y Z bnd_tcp (bnd_tcppacket X1 X2 X5 X3))); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5. % 16.34/15.88 ((((~ bnd_ssNetwork U | % 16.34/15.88 ~ bnd_ssSent % 16.34/15.88 (bnd_epacket V W X bnd_e_ip % 16.34/15.88 (bnd_ippacket Y Z bnd_tcp % 16.34/15.88 (bnd_tcppacket X1 X2 bnd_no_syn X3)))) | % 16.34/15.88 ~ bnd_ssNetwork V) | % 16.34/15.88 ~ bnd_ssTCP_Connection_Open % 16.34/15.88 (bnd_tcp_connection_open X4 Y Z X1 X2)) | % 16.34/15.88 ~ bnd_ssFirewall (bnd_firewall X4 V U)) | % 16.34/15.88 bnd_ssSent % 16.34/15.88 (bnd_epacket U W X bnd_e_ip % 16.34/15.88 (bnd_ippacket Y Z bnd_tcp (bnd_tcppacket X1 X2 X5 X3))); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4. % 16.34/15.88 ((((~ bnd_ssNetwork U | ~ bnd_ssNetwork V) | % 16.34/15.88 ~ bnd_ssSent % 16.34/15.88 (bnd_epacket V W X bnd_e_ip % 16.34/15.88 (bnd_ippacket Y Z bnd_tcp % 16.34/15.88 (bnd_tcppacket X1 X2 bnd_ack X3)))) | % 16.34/15.88 ~ bnd_ssTCP_ClientSynSent (bnd_tcp_clientsynsent X4 Z Y X2 X1)) | % 16.34/15.88 ~ bnd_ssFirewall (bnd_firewall X4 V U)) | % 16.34/15.88 bnd_ssSent % 16.34/15.88 (bnd_epacket U W X bnd_e_ip % 16.34/15.88 (bnd_ippacket Y Z bnd_tcp (bnd_tcppacket X1 X2 bnd_ack X3))); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5. % 16.34/15.88 ((((~ bnd_ssNetwork U | ~ bnd_ssNetwork V) | % 16.34/15.88 ~ bnd_ssSent % 16.34/15.88 (bnd_epacket V W X bnd_e_ip % 16.34/15.88 (bnd_ippacket Y Z bnd_tcp % 16.34/15.88 (bnd_tcppacket X1 X2 bnd_synack X3)))) | % 16.34/15.88 ~ bnd_ssFirewall (bnd_firewall X4 V U)) | % 16.34/15.88 ~ bnd_ssTCP_ClientSynSent (bnd_tcp_clientsynsent X4 Z Y X2 X1)) | % 16.34/15.88 bnd_ssSent % 16.34/15.88 (bnd_epacket U W X bnd_e_ip % 16.34/15.88 (bnd_ippacket Y Z bnd_tcp (bnd_tcppacket X1 X2 X5 X3))); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4. % 16.34/15.88 ((((~ bnd_ssNetwork U | % 16.34/15.88 ~ bnd_ssSent % 16.34/15.88 (bnd_epacket V W X bnd_e_ip % 16.34/15.88 (bnd_ippacket Y Z bnd_udp (bnd_udppacket X1 X2 X3)))) | % 16.34/15.88 ~ bnd_ssNetwork V) | % 16.34/15.88 ~ bnd_ssUDP_ConnectionOpen (bnd_udp_connection_open X4 Z Y X2 X1)) | % 16.34/15.88 ~ bnd_ssFirewall (bnd_firewall X4 V U)) | % 16.34/15.88 bnd_ssSent % 16.34/15.88 (bnd_epacket U W X bnd_e_ip % 16.34/15.88 (bnd_ippacket Y Z bnd_udp (bnd_udppacket X1 X2 X3))); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4. % 16.34/15.88 (((((~ bnd_ssNetwork U | ~ bnd_ssNetwork V) | % 16.34/15.88 ~ bnd_ssFtpServerPort (bnd_ftpServerPort W X Y)) | % 16.34/15.88 ~ bnd_ssTCP_ClientAckSent (bnd_tcp_clientacksent W Z X X1 Y)) | % 16.34/15.88 ~ bnd_ssFirewall (bnd_firewall W V U)) | % 16.34/15.88 ~ bnd_ssSent % 16.34/15.88 (bnd_epacket V X2 X3 bnd_e_ip % 16.34/15.88 (bnd_ippacket X Z bnd_tcp (bnd_tcppacket Y X1 bnd_ack X4)))) | % 16.34/15.88 bnd_ssFtp_Start (bnd_ftp_start_state W Z X X1 Y); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6 X7. % 16.34/15.88 ((((~ bnd_ssNotForwarded % 16.34/15.88 (bnd_not_forwarded (bnd_ippacket U V W X) Y) | % 16.34/15.88 ~ bnd_ssInterface (bnd_interface Z X1 X2 X3 X4)) | % 16.34/15.88 ~ bnd_ssRouteIPPacket % 16.34/15.88 (bnd_route_ip_packet Z (bnd_ippacket U V W X))) | % 16.34/15.88 ~ bnd_ssRouteEntry (bnd_route Z X5 X6 X7 (bnd_next_rule Y))) | % 16.34/15.88 bnd_ipand V X5 = X6) | % 16.34/15.88 bnd_ssNotForwarded % 16.34/15.88 (bnd_not_forwarded (bnd_ippacket U V W X) (bnd_next_rule Y)); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5. % 16.34/15.88 ((((~ bnd_ipand U V = W | ~ bnd_ipand X Y = bnd_ipand U Y) | % 16.34/15.88 ~ bnd_ssInterface (bnd_interface Z X Y X1 X2)) | % 16.34/15.88 ~ bnd_ssRouteEntry (bnd_route Z V W bnd_local bnd_first_route)) | % 16.34/15.88 ~ bnd_ssRouteIPPacket % 16.34/15.88 (bnd_route_ip_packet Z (bnd_ippacket X3 U X4 X5))) | % 16.34/15.88 bnd_ssSendIPPacket (bnd_send_ip_packet Z U (bnd_ippacket X3 U X4 X5)); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6. % 16.34/15.88 ((((~ bnd_ipand U V = W | ~ bnd_ipand X Y = bnd_ipand Z Y) | % 16.34/15.88 ~ bnd_ssRouteEntry (bnd_route X1 V W Z bnd_first_route)) | % 16.34/15.88 ~ bnd_ssRouteIPPacket % 16.34/15.88 (bnd_route_ip_packet X1 (bnd_ippacket X2 U X3 X4))) | % 16.34/15.88 ~ bnd_ssInterface (bnd_interface X1 X Y X5 X6)) | % 16.34/15.88 bnd_ssSendIPPacket % 16.34/15.88 (bnd_send_ip_packet X1 Z (bnd_ippacket X2 U X3 X4)); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4. % 16.34/15.88 ((((~ bnd_ssNetwork U | ~ bnd_ssNetwork V) | % 16.34/15.88 ~ bnd_ssSent % 16.34/15.88 (bnd_epacket V W X bnd_e_ip % 16.34/15.88 (bnd_ippacket Y Z bnd_tcp % 16.34/15.88 (bnd_tcppacket X1 X2 bnd_finack X3)))) | % 16.34/15.88 ~ bnd_ssTCP_Connection_HalfClosed % 16.34/15.88 (bnd_tcp_connection_halfclosed X4 Y Z X1 X2)) | % 16.34/15.88 ~ bnd_ssFirewall (bnd_firewall X4 V U)) | % 16.34/15.88 bnd_ssTCP_Connection_Closed (bnd_tcp_connection_closed X4 Y Z X1 X2); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4. % 16.34/15.88 ((((~ bnd_ssNetwork U | ~ bnd_ssNetwork V) | % 16.34/15.88 ~ bnd_ssSent % 16.34/15.88 (bnd_epacket V W X bnd_e_ip % 16.34/15.88 (bnd_ippacket Y Z bnd_tcp % 16.34/15.88 (bnd_tcppacket X1 X2 bnd_fin X3)))) | % 16.34/15.88 ~ bnd_ssTCP_Connection_Open % 16.34/15.88 (bnd_tcp_connection_open X4 Z Y X1 X2)) | % 16.34/15.88 ~ bnd_ssFirewall (bnd_firewall X4 V U)) | % 16.34/15.88 bnd_ssTCP_Connection_HalfClosed % 16.34/15.88 (bnd_tcp_connection_halfclosed X4 Z Y X1 X2); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4. % 16.34/15.88 ((((~ bnd_ssNetwork U | ~ bnd_ssNetwork V) | % 16.34/15.88 ~ bnd_ssSent % 16.34/15.88 (bnd_epacket V W X bnd_e_ip % 16.34/15.88 (bnd_ippacket Y Z bnd_tcp % 16.34/15.88 (bnd_tcppacket X1 X2 bnd_fin X3)))) | % 16.34/15.88 ~ bnd_ssTCP_Connection_Open % 16.34/15.88 (bnd_tcp_connection_open X4 Y Z X1 X2)) | % 16.34/15.88 ~ bnd_ssFirewall (bnd_firewall X4 V U)) | % 16.34/15.88 bnd_ssTCP_Connection_HalfClosed % 16.34/15.88 (bnd_tcp_connection_halfclosed X4 Y Z X1 X2); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4. % 16.34/15.88 ((((~ bnd_ssNetwork U | ~ bnd_ssNetwork V) | % 16.34/15.88 ~ bnd_ssSent % 16.34/15.88 (bnd_epacket V W X bnd_e_ip % 16.34/15.88 (bnd_ippacket Y Z bnd_tcp % 16.34/15.88 (bnd_tcppacket X1 X2 bnd_ack X3)))) | % 16.34/15.88 ~ bnd_ssTCP_ClientSynSent (bnd_tcp_clientsynsent X4 Z Y X2 X1)) | % 16.34/15.88 ~ bnd_ssFirewall (bnd_firewall X4 V U)) | % 16.34/15.88 bnd_ssTCP_Connection_Open (bnd_tcp_connection_open X4 Z Y X2 X1); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4. % 16.34/15.88 ((((~ bnd_ssNetwork U | ~ bnd_ssNetwork V) | % 16.34/15.88 ~ bnd_ssSent % 16.34/15.88 (bnd_epacket V W X bnd_e_ip % 16.34/15.88 (bnd_ippacket Y Z bnd_tcp % 16.34/15.88 (bnd_tcppacket X1 X2 bnd_synack X3)))) | % 16.34/15.88 ~ bnd_ssFirewall (bnd_firewall X4 V U)) | % 16.34/15.88 ~ bnd_ssTCP_ClientSynSent (bnd_tcp_clientsynsent X4 Z Y X2 X1)) | % 16.34/15.88 bnd_ssTCP_ServerSynAckSent (bnd_tcp_connection_open X4 Z Y X2 X1); % 16.34/15.88 !!U V W X Y Z X1 X2 X3 X4 X5 X6. % 16.34/15.88 (((~ bnd_ssInterface (bnd_interface U V W X Y) | % 16.34/15.88 ~ bnd_ssRouteIPPacket % 16.34/15.88 (bnd_route_ip_packet U (bnd_ippacket Z X1 X2 X3))) | % 16.34/15.88 ~ bnd_ssRouteEntry (bnd_route U X4 X5 X6 bnd_first_rule)) | % 16.34/15.88 bnd_ipand X1 X4 = X5) | % 16.34/15.88 bnd_ssNotForwarded % 16.34/15.88 (bnd_not_forwarded (bnd_ippacket Z X1 X2 X3) bnd_first_rule); % 16.34/15.88 !!U V W X Y Z X1 X2. % 16.34/15.88 ((((~ bnd_ipand U V = bnd_ipand W V | ~ bnd_ssNetwork X) | % 16.34/15.88 ~ bnd_ssArpTable (bnd_arpEntry Y Z W)) | % 16.34/15.88 ~ bnd_ssInterface (bnd_interface Y U V X1 X)) | % 16.34/15.88 ~ bnd_ssSendIPPacket (bnd_send_ip_packet Y W X2)) | % 16.34/15.88 bnd_ssSent (bnd_epacket X Z X1 bnd_e_ip X2); % 16.34/15.88 bnd_ip bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 = % 16.34/15.88 bnd_networkip; % 16.34/15.88 bnd_ip bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 = % 16.34/15.88 bnd_local; % 16.34/15.88 bnd_ip bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 = % 16.34/15.88 bnd_mask0; % 16.34/15.88 bnd_ip bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 = % 16.34/15.88 bnd_mask8; % 16.34/15.88 bnd_ip bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 % 16.34/15.88 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n0 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 = % 16.34/15.88 bnd_mask16; % 16.34/15.88 bnd_ip bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 % 16.34/15.88 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 % 16.34/15.88 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 = % 16.34/15.88 bnd_mask24; % 16.34/15.88 bnd_ip bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 % 16.34/15.88 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 % 16.34/15.88 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 % 16.34/15.88 bnd_n1 bnd_n1 bnd_n1 = % 16.34/15.88 bnd_broadcastip; % 16.34/15.88 bnd_ip bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 % 16.34/15.88 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 % 16.34/15.88 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 % 16.34/15.88 bnd_n1 bnd_n1 bnd_n1 = % 16.34/15.88 bnd_mask32; % 16.34/15.88 bnd_ip bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 % 16.34/15.88 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 % 16.34/15.88 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 = % 16.34/15.88 bnd_c_class; % 16.34/15.88 bnd_ip bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n1 bnd_n0 bnd_n1 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 bnd_n1 bnd_n0 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 % 16.34/15.88 bnd_n1 bnd_n1 bnd_n0 = % 16.34/15.88 bnd_r1_ip_net2; % 16.34/15.88 bnd_ip bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n1 bnd_n0 bnd_n1 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 bnd_n1 % 16.34/15.88 bnd_n1 bnd_n1 bnd_n0 = % 16.34/15.88 bnd_r1_ip_net1; % 16.34/15.88 bnd_ip bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n1 bnd_n0 bnd_n1 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 bnd_n1 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n1 = % 16.34/15.88 bnd_c2_ip; % 16.34/15.88 bnd_ip bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n1 bnd_n0 bnd_n1 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n1 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n1 = % 16.34/15.88 bnd_c1_ip; % 16.34/15.88 bnd_ip bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n1 bnd_n0 bnd_n1 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n1 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n1 bnd_n0 = % 16.34/15.88 bnd_rl1_ip; % 16.34/15.88 bnd_ip bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n1 bnd_n0 bnd_n1 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 bnd_n1 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n1 bnd_n0 = % 16.34/15.88 bnd_s1_ip; % 16.34/15.88 bnd_ip bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n1 bnd_n0 bnd_n1 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 bnd_n1 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 = % 16.34/15.88 bnd_net2_addr; % 16.34/15.88 bnd_ip bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n1 bnd_n0 bnd_n1 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n1 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 = % 16.34/15.88 bnd_net1_addr; % 16.34/15.88 bnd_ip bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 % 16.34/15.88 bnd_n0 bnd_n0 bnd_n0 = % 16.34/15.88 bnd_any; % 16.34/15.88 !!U V W X Y Z. % 16.34/15.88 ((~ bnd_ssDhcpServer U | % 16.34/15.88 ~ bnd_ssRouteIPPacket % 16.34/15.88 (bnd_route_ip_packet U % 16.34/15.88 (bnd_ippacket bnd_networkip bnd_broadcastip bnd_udp V))) | % 16.34/15.88 ~ bnd_ssInterface (bnd_interface U W X Y Z)) | % 16.34/15.88 bnd_ssSent % 16.34/15.88 (bnd_epacket Z bnd_broadcastmac Y bnd_e_ip % 16.34/15.88 (bnd_ippacket bnd_networkip bnd_broadcastip bnd_udp V)); % 16.34/15.88 !!U V W X Y Z. % 16.34/15.88 ((~ bnd_ssDhcpClient U | % 16.34/15.88 ~ bnd_ssRouteIPPacket % 16.34/15.88 (bnd_route_ip_packet U % 16.34/15.88 (bnd_ippacket bnd_networkip bnd_broadcastip bnd_udp V))) | % 16.34/15.88 ~ bnd_ssInterface (bnd_interface U W X Y Z)) | % 16.34/15.88 bnd_ssSent % 16.34/15.88 (bnd_epacket Z bnd_broadcastmac Y bnd_e_ip % 16.34/15.88 (bnd_ippacket bnd_networkip bnd_broadcastip bnd_udp V)); % 16.34/15.88 !!U V W X Y Z. % 16.34/15.88 ((~ bnd_ssRelayagent U | % 16.34/15.88 ~ bnd_ssRouteIPPacket % 16.34/15.88 (bnd_route_ip_packet U % 16.34/15.88 (bnd_ippacket bnd_networkip bnd_broadcastip bnd_udp V))) | % 16.34/15.88 ~ bnd_ssInterface (bnd_interface U W X Y Z)) | % 16.34/15.88 bnd_ssSent % 16.34/15.88 (bnd_epacket Z bnd_broadcastmac Y bnd_e_ip % 16.34/15.88 (bnd_ippacket bnd_networkip bnd_broadcastip bnd_udp V)); % 16.34/15.88 !!U V W X Y Z. % 16.34/15.88 ((~ bnd_ssRouteIPPacket % 16.34/15.88 (bnd_route_ip_packet U % 16.34/15.88 (bnd_ippacket V bnd_broadcastip bnd_udp W)) | % 16.34/15.88 ~ bnd_ssRelayagent U) | % 16.34/15.88 ~ bnd_ssInterface (bnd_interface U V X Y Z)) | % 16.34/15.88 bnd_ssSent % 16.34/15.88 (bnd_epacket Z bnd_broadcastmac Y bnd_e_ip % 16.34/15.88 (bnd_ippacket V bnd_broadcastip bnd_udp W)); % 16.34/15.88 !!U V W X Y Z. % 16.34/15.88 ((~ bnd_ssRouteIPPacket % 16.34/15.88 (bnd_route_ip_packet U % 16.34/15.88 (bnd_ippacket V bnd_broadcastip bnd_udp W)) | % 16.34/15.88 ~ bnd_ssDhcpClient U) | % 16.34/15.88 ~ bnd_ssInterface (bnd_interface U V X Y Z)) | % 16.34/15.88 bnd_ssSent % 16.34/15.88 (bnd_epacket Z bnd_broadcastmac Y bnd_e_ip % 16.34/15.88 (bnd_ippacket V bnd_broadcastip bnd_udp W)); % 16.34/15.88 !!U V W X Y Z. % 16.34/15.88 ((~ bnd_ssRouteIPPacket % 16.34/15.88 (bnd_route_ip_packet U % 16.34/15.88 (bnd_ippacket V bnd_broadcastip bnd_udp W)) | % 16.34/15.88 ~ bnd_ssDhcpServer U) | % 16.34/15.88 ~ bnd_ssInterface (bnd_interface U V X Y Z)) | % 16.34/15.88 bnd_ssSent % 16.34/15.88 (bnd_epacket Z bnd_broadcastmac Y bnd_e_ip % 16.34/15.88 (bnd_ippacket V bnd_broadcastip bnd_udp W)); % 16.34/15.88 !!U V W X Y Z X1. % 16.34/15.88 ((~ bnd_ssRelayagent U | % 16.34/15.88 ~ bnd_ssReceivedIPPacket % 16.34/15.88 (bnd_recv_ip_packet V U % 16.34/15.88 (bnd_ippacket W bnd_broadcastip bnd_udp X))) | % 16.34/15.88 ~ bnd_ssInterface (bnd_interface U Y Z X1 V)) | % 16.34/15.88 bnd_ssReceivedUDPPacket (bnd_recv_udp_packet V U W bnd_broadcastip X); % 16.34/15.88 !!U V W X Y Z X1. % 16.34/15.88 ((~ bnd_ssDhcpClient U | % 16.34/15.88 ~ bnd_ssReceivedIPPacket % 16.34/15.88 (bnd_recv_ip_packet V U % 16.34/15.88 (bnd_ippacket W bnd_broadcastip bnd_udp X))) | % 16.34/15.88 ~ bnd_ssInterface (bnd_interface U Y Z X1 V)) | % 16.34/15.88 bnd_ssReceivedUDPPacket (bnd_recv_udp_packet V U W bnd_broadcastip X); % 16.34/15.88 !!U V W X Y Z X1. % 16.34/15.88 ((~ bnd_ssDhcpServer U | % 16.34/15.88 ~ bnd_ssReceivedIPPacket % 16.34/15.88 (bnd_recv_ip_packet V U % 16.34/15.88 (bnd_ippacket W bnd_broadcastip bnd_udp X))) | % 16.34/15.88 ~ bnd_ssInterface (bnd_interface U Y Z X1 V)) | % 16.34/15.88 bnd_ssReceivedUDPPacket (bnd_recv_udp_packet V U W bnd_broadcastip X); % 16.34/15.88 !!U V W X Y Z X1. % 16.34/15.88 ((~ bnd_ssRelayagent U | % 16.34/15.88 ~ bnd_ssInterface (bnd_interface U V W X Y)) | % 16.34/15.88 ~ bnd_ssReceivedIPPacket % 16.34/15.88 (bnd_recv_ip_packet Y U (bnd_ippacket Z V bnd_udp X1))) | % 16.34/15.88 bnd_ssReceivedUDPPacket (bnd_recv_udp_packet Y U Z V X1); % 16.34/15.88 !!U V W X Y Z X1. % 16.34/15.88 ((~ bnd_ssDhcpClient U | % 16.34/15.88 ~ bnd_ssInterface (bnd_interface U V W X Y)) | % 16.34/15.88 ~ bnd_ssReceivedIPPacket % 16.34/15.88 (bnd_recv_ip_packet Y U (bnd_ippacket Z V bnd_udp X1))) | % 16.34/15.88 bnd_ssReceivedUDPPacket (bnd_recv_udp_packet Y U Z V X1); % 16.34/15.88 !!U V W X Y Z X1. % 16.34/15.88 ((~ bnd_ssDhcpServer U | % 16.34/15.88 ~ bnd_ssInterface (bnd_interface U V W X Y)) | % 16.34/15.88 ~ bnd_ssReceivedIPPacket % 16.34/15.88 (bnd_recv_ip_packet Y U (bnd_ippacket Z V bnd_udp X1))) | % 16.34/15.88 bnd_ssReceivedUDPPacket (bnd_recv_udp_packet Y U Z V X1); % 16.34/15.88 !!U V W X Y Z X1. % 16.34/15.88 ((~ bnd_ssNetwork U | % 16.34/15.88 ~ bnd_ssSent (bnd_epacket U bnd_broadcastmac V bnd_e_ip W)) | % 16.34/15.88 ~ bnd_ssInterface (bnd_interface X Y Z X1 U)) | % 16.34/15.88 bnd_ssReceivedIPPacket (bnd_recv_ip_packet U X W); % 16.34/15.88 !!U V W X Y Z X1. % 16.34/15.88 ((~ bnd_ssNetwork U | ~ bnd_ssInterface (bnd_interface V W X Y U)) | % 16.34/15.88 ~ bnd_ssSent (bnd_epacket U Y Z bnd_e_ip X1)) | % 16.34/15.88 bnd_ssReceivedIPPacket (bnd_recv_ip_packet U V X1); % 16.34/15.88 !!U V W X Y Z. % 16.34/15.88 (~ bnd_ssRouter U | % 16.34/15.88 ~ bnd_ssReceivedIPPacket % 16.34/15.88 (bnd_recv_ip_packet V U (bnd_ippacket W X Y Z))) | % 16.34/15.88 bnd_ssRouteIPPacket (bnd_route_ip_packet U (bnd_ippacket W X Y Z)); % 16.34/15.88 !!U V W X Y. % 16.34/15.88 (~ bnd_ssDhcpServer U | % 16.34/15.88 ~ bnd_ssSendUDPPacket (bnd_send_udp_packet V U W X Y)) | % 16.34/15.88 bnd_ssRouteIPPacket % 16.34/15.88 (bnd_route_ip_packet U (bnd_ippacket W X bnd_udp Y)); % 16.34/15.88 !!U V W X Y. % 16.34/15.88 (~ bnd_ssDhcpClient U | % 16.34/15.88 ~ bnd_ssSendUDPPacket (bnd_send_udp_packet V U W X Y)) | % 16.34/15.88 bnd_ssRouteIPPacket % 16.34/15.88 (bnd_route_ip_packet U (bnd_ippacket W X bnd_udp Y)); % 16.34/15.88 !!U V W X Y. % 16.34/15.88 (~ bnd_ssRelayagent U | % 16.34/15.88 ~ bnd_ssSendUDPPacket (bnd_send_udp_packet V U W X Y)) | % 16.34/15.88 bnd_ssRouteIPPacket % 16.34/15.88 (bnd_route_ip_packet U (bnd_ippacket W X bnd_udp Y)); % 16.34/15.88 !!U V. % 16.34/15.88 (((~ bnd_ssBit U | ~ bnd_land V U = bnd_n0) | ~ bnd_ssBit V) | % 16.34/15.88 U = bnd_n0) | % 16.34/15.88 V = bnd_n0; % 16.34/15.88 !!U V. % 16.34/15.88 ((~ bnd_ssBit U | ~ bnd_ssBit V) | bnd_land V U = bnd_n0) | % 16.34/15.88 bnd_land V U = bnd_n1; % 16.34/15.88 !!U V. % 16.34/15.88 ((~ bnd_ssBit U | ~ bnd_land V U = bnd_n1) | ~ bnd_ssBit V) | % 16.34/15.88 U = bnd_n1; % 16.34/15.88 !!U V. % 16.34/15.88 ((~ bnd_ssBit U | ~ bnd_land V U = bnd_n1) | ~ bnd_ssBit V) | % 16.34/15.88 V = bnd_n1; % 16.34/15.88 bnd_ssUDP_FirewallRule % 16.34/15.88 (bnd_udp_fwrule bnd_fw1 (bnd_next_rule (bnd_next_rule bnd_first_rule)) % 16.34/15.88 bnd_permit bnd_any bnd_any bnd_any bnd_any bnd_port68 bnd_port67); % 16.34/15.88 bnd_ssTCP_FirewallRule % 16.34/15.88 (bnd_tcp_fwrule bnd_fw1 (bnd_next_rule bnd_first_rule) bnd_permit % 16.34/15.88 bnd_any bnd_any bnd_any bnd_any bnd_c1port bnd_s1port); % 16.34/15.88 bnd_ssUDP_FirewallRule % 16.34/15.88 (bnd_udp_fwrule bnd_fw1 (bnd_next_rule bnd_first_rule) bnd_permit % 16.34/15.88 bnd_any bnd_any bnd_any bnd_any bnd_port67 bnd_port68); % 16.34/15.88 bnd_ssTCP_FirewallRule % 16.34/15.88 (bnd_tcp_fwrule bnd_fw1 bnd_first_rule bnd_deny bnd_net2_addr % 16.34/15.88 bnd_c_class bnd_net2_addr bnd_c_class bnd_c1port bnd_s1port); % 16.34/15.88 bnd_ssUDP_FirewallRule % 16.34/15.88 (bnd_udp_fwrule bnd_fw1 bnd_first_rule bnd_permit bnd_any bnd_any % 16.34/15.88 bnd_any bnd_any bnd_port67 bnd_port67); % 16.34/15.88 !!U. ~ bnd_ssBit U | bnd_land bnd_n0 U = bnd_n0; % 16.34/15.88 !!U. ~ bnd_ssBit U | bnd_land U bnd_n0 = bnd_n0; % 16.34/15.88 !!U. ~ bnd_ssBit U | bnd_land bnd_n1 U = U; % 16.34/15.88 !!U. ~ bnd_ssBit U | bnd_land U bnd_n1 = U; % 16.34/15.88 bnd_ssRouteEntry % 16.34/15.88 (bnd_route bnd_r1 bnd_c_class bnd_net2_addr bnd_local % 16.34/15.88 (bnd_next_route bnd_first_route)); % 16.34/15.88 bnd_ssRouteEntry % 16.34/15.88 (bnd_route bnd_rl1 bnd_mask0 bnd_mask0 bnd_r1_ip_net1 % 16.34/15.88 (bnd_next_route bnd_first_route)); % 16.34/15.88 bnd_ssRouteEntry % 16.34/15.88 (bnd_route bnd_s1 bnd_mask0 bnd_mask0 bnd_r1_ip_net2 % 16.34/15.88 (bnd_next_route bnd_first_route)); % 16.34/15.88 bnd_ssRouteEntry % 16.34/15.88 (bnd_route bnd_c1 bnd_mask0 bnd_mask0 bnd_r1_ip_net1 % 16.34/15.88 (bnd_next_route bnd_first_route)); % 16.34/15.88 bnd_ssRouteEntry % 16.34/15.88 (bnd_route bnd_c2 bnd_mask0 bnd_mask0 bnd_r1_ip_net2 % 16.34/15.88 (bnd_next_route bnd_first_route)); % 16.34/15.88 bnd_ssInterface % 16.34/15.88 (bnd_interface bnd_r1 bnd_r1_ip_net1 bnd_c_class bnd_r1_mac_net1 % 16.34/15.88 bnd_con1); % 16.34/15.88 bnd_ssInterface % 16.34/15.88 (bnd_interface bnd_r1 bnd_r1_ip_net2 bnd_c_class bnd_r1_mac_net2 % 16.34/15.88 bnd_net2); % 16.34/15.88 bnd_ssRouteEntry % 16.34/15.88 (bnd_route bnd_r1 bnd_c_class bnd_net1_addr bnd_local bnd_first_route); % 16.34/15.88 bnd_ssRouteEntry % 16.34/15.88 (bnd_route bnd_rl1 bnd_c_class bnd_net1_addr bnd_local bnd_first_route); % 16.34/15.88 bnd_ssRouteEntry % 16.34/15.88 (bnd_route bnd_s1 bnd_c_class bnd_net2_addr bnd_local bnd_first_route); % 16.34/15.88 bnd_ssRouteEntry % 16.34/15.88 (bnd_route bnd_c1 bnd_c_class bnd_net1_addr bnd_local bnd_first_route); % 16.34/15.89 bnd_ssRouteEntry % 16.34/15.89 (bnd_route bnd_c2 bnd_c_class bnd_net2_addr bnd_local bnd_first_route); % 16.34/15.89 bnd_ssArpTable (bnd_arpEntry bnd_r1 bnd_s1_mac bnd_s1_ip); % 16.34/15.89 bnd_ssArpTable (bnd_arpEntry bnd_r1 bnd_c1_mac bnd_c1_ip); % 16.34/15.89 bnd_ssArpTable (bnd_arpEntry bnd_r1 bnd_rl1_mac bnd_rl1_ip); % 16.34/15.89 bnd_ssArpTable (bnd_arpEntry bnd_s1 bnd_r1_mac_net2 bnd_r1_ip_net2); % 16.34/15.89 bnd_ssArpTable (bnd_arpEntry bnd_s1 bnd_c2_mac bnd_c2_ip); % 16.34/15.89 bnd_ssArpTable (bnd_arpEntry bnd_rl1 bnd_r1_mac_net1 bnd_r1_ip_net1); % 16.34/15.89 bnd_ssArpTable (bnd_arpEntry bnd_rl1 bnd_c1_mac bnd_c1_ip); % 16.34/15.89 bnd_ssArpTable (bnd_arpEntry bnd_c1 bnd_r1_mac_net1 bnd_r1_ip_net1); % 16.34/15.89 bnd_ssArpTable (bnd_arpEntry bnd_c1 bnd_rl1_mac bnd_rl1_ip); % 16.34/15.89 bnd_ssArpTable (bnd_arpEntry bnd_c2 bnd_r1_mac_net2 bnd_r1_ip_net2); % 16.34/15.89 bnd_ssArpTable (bnd_arpEntry bnd_s1 bnd_s1_mac bnd_s1_ip); % 16.34/15.89 bnd_ssFirewall (bnd_firewall bnd_fw1 bnd_con1 bnd_net1); % 16.34/15.89 bnd_ssFirewall (bnd_firewall bnd_fw1 bnd_net1 bnd_con1); % 16.34/15.89 ~ bnd_n0 = bnd_n1; ~ bnd_networkip = bnd_broadcastip; % 16.34/15.89 ~ bnd_broadcastip = bnd_any; ~ bnd_broadcastip = bnd_local; % 16.34/15.89 bnd_ssBit bnd_n1; bnd_ssBit bnd_n0; bnd_ssNetwork bnd_net1; % 16.34/15.89 bnd_ssNetwork bnd_con1; bnd_ssNetwork bnd_net2; bnd_ssRouter bnd_r1 |] % 16.34/15.89 ==> True % 16.34/15.89 Adding axioms... % 16.34/15.89 Typedef.type_definition_def % 97.14/96.56 ...done. % 97.24/96.70 Ground types: ?'b, TPTP_Interpret.ind % 97.24/96.70 Translating term (sizes: 1, 1) ... % 143.72/142.94 Invoking SAT solver... % 143.72/142.94 No model exists. % 143.72/142.94 Translating term (sizes: 2, 1) ... % 190.82/189.81 Invoking SAT solver... % 190.82/189.81 No model exists. % 190.82/189.81 Translating term (sizes: 1, 2) ... % 193.29/192.20 Search terminated, number of Boolean variables (100000 allowed) exceeded. % 193.29/192.20 % SZS status Unknown %------------------------------------------------------------------------------