%------------------------------------------------------------------------------ % File : ZenonModulo---0.5.0 % Problem : SYN547+1 : TPTP v8.2.0. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : run_zenon_modulo %d %s % Computer : n008.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Jun 25 02:18:55 EDT 2024 % Result : Unknown 1.07s 1.25s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : SYN547+1 : TPTP v8.2.0. Released v2.1.0. % 0.12/0.12 % Command : run_zenon_modulo %d %s % 0.12/0.33 % Computer : n008.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Mon Jun 24 01:15:39 EDT 2024 % 0.12/0.33 % CPUTime : % 1.07/1.25 Zenon error: exhausted search space without finding a proof % 1.07/1.25 (* Current branch: % 1.07/1.25 ((a601) != (a496)) % 1.07/1.25 ((a460) != zenon_X60) % 1.07/1.25 (-. (c5_1 (a544))) % 1.07/1.25 ((a533) != zenon_X11) % 1.07/1.25 (-. (c4_2 zenon_X19 zenon_X73)) % 1.07/1.25 ((a573) != (a482)) % 1.07/1.25 (-. (c7_2 (a534) zenon_X98)) % 1.07/1.25 (-. (c1_1 (a498))) % 1.07/1.25 ((a553) != zenon_X98) % 1.07/1.25 (-. (c4_2 zenon_X9 zenon_X155)) % 1.07/1.25 ((a521) != (a553)) % 1.07/1.25 (-. (c7_2 zenon_X21 zenon_X147)) % 1.07/1.25 (c5_2 (a544) zenon_X59) % 1.07/1.25 (zenon_X30 != zenon_X9) % 1.07/1.25 (-. (c5_2 (a592) (a535))) % 1.07/1.25 ((a508) != (a573)) % 1.07/1.25 ((a520) != zenon_X27) % 1.07/1.25 (zenon_X29 != zenon_X17) % 1.07/1.25 ((a468) != zenon_X11) % 1.07/1.25 (-. (c4_2 zenon_X19 (a480))) % 1.07/1.25 (-. (c4_2 zenon_X24 (a480))) % 1.07/1.25 ((a498) != zenon_X17) % 1.07/1.25 (zenon_X14 != zenon_X97) % 1.07/1.25 (-. (c8_2 zenon_X9 zenon_X169)) % 1.07/1.25 (-. (c7_2 zenon_X17 (a472))) % 1.07/1.25 (-. (c4_1 (a566))) % 1.07/1.25 ((a463) != (a577)) % 1.07/1.25 (zenon_X30 != zenon_X12) % 1.07/1.25 (zenon_X19 != zenon_X29) % 1.07/1.25 (zenon_X27 != zenon_X11) % 1.07/1.25 ((a460) != zenon_X99) % 1.07/1.25 (-. (c4_2 (a498) (a487))) % 1.07/1.25 (zenon_X13 != (a463)) % 1.07/1.25 (-. (c2_1 (a544))) % 1.07/1.25 (c3_2 (a534) (a495)) % 1.07/1.25 ((a483) != (a578)) % 1.07/1.25 ((a496) != (a498)) % 1.07/1.25 (-. (c6_2 (a482) (a484))) % 1.07/1.25 ((a499) != zenon_X61) % 1.07/1.25 ((a483) != zenon_X64) % 1.07/1.25 (-. (c2_2 (a520) zenon_X50)) % 1.07/1.25 (zenon_X48 != (a545)) % 1.07/1.25 ((a483) != zenon_X50) % 1.07/1.25 (-. (c4_2 (a534) zenon_X48)) % 1.07/1.25 (ndr1_1 zenon_X13) % 1.07/1.25 ((a480) != (a545)) % 1.07/1.25 (-. (c2_2 zenon_X21 (a548))) % 1.07/1.25 ((a500) != zenon_X59) % 1.07/1.25 ((a494) != (a482)) % 1.07/1.25 (-. (c1_2 (a592) (a545))) % 1.07/1.25 (-. (c2_1 (a592))) % 1.07/1.25 (zenon_X28 != (a484)) % 1.07/1.25 (-. (c4_2 (a520) zenon_X14)) % 1.07/1.25 ((a538) != (a520)) % 1.07/1.25 ((a508) != (a601)) % 1.07/1.25 (c8_1 (a471)) % 1.07/1.25 (c5_2 (a544) zenon_X48) % 1.07/1.25 ((a460) != zenon_X56) % 1.07/1.25 (-. (c2_2 (a494) (a553))) % 1.07/1.25 ((a545) != zenon_X8) % 1.07/1.25 (zenon_X0 != (a577)) % 1.07/1.25 ((a499) != zenon_X53) % 1.07/1.25 (zenon_X11 != (a544)) % 1.07/1.25 ((a467) != (a567)) % 1.07/1.25 ((a487) != zenon_X91) % 1.07/1.25 ((a460) != zenon_X49) % 1.07/1.25 ((a500) != (a579)) % 1.07/1.25 (c7_2 (a482) (a553)) % 1.07/1.25 ((a482) != (a577)) % 1.07/1.25 (c4_2 (a544) (a535)) % 1.07/1.25 (-. (c8_2 (a534) zenon_X62)) % 1.07/1.25 (zenon_X19 != (a508)) % 1.07/1.25 ((a577) != zenon_X17) % 1.07/1.25 (-. (c5_2 (a592) (a487))) % 1.07/1.25 (zenon_X39 != (a553)) % 1.07/1.25 ((a460) != (a548)) % 1.07/1.25 (zenon_X90 != (a545)) % 1.07/1.25 ((a548) != zenon_X165) % 1.07/1.25 (-. (c2_2 (a566) (a460))) % 1.07/1.25 ((a472) != zenon_X18) % 1.07/1.25 (-. (c4_2 (a520) zenon_X92)) % 1.07/1.25 (zenon_X29 != zenon_X13) % 1.07/1.25 (-. (c2_2 zenon_X11 (a467))) % 1.07/1.25 (-. (c3_2 (a570) (a553))) % 1.07/1.25 ((a499) != zenon_X56) % 1.07/1.25 ((a460) != zenon_X16) % 1.07/1.25 (-. (c2_2 zenon_X21 zenon_X165)) % 1.07/1.25 ((a548) != zenon_X67) % 1.07/1.25 ((a468) != (a577)) % 1.07/1.25 (zenon_X14 != zenon_X20) % 1.07/1.25 ((a544) != zenon_X12) % 1.07/1.25 ((a472) != (a500)) % 1.07/1.25 ((a487) != zenon_X144) % 1.07/1.25 (-. (c1_2 (a538) (a571))) % 1.07/1.25 ((a495) != zenon_X25) % 1.07/1.25 (-. (c4_2 (a601) zenon_X145)) % 1.07/1.25 (c6_2 zenon_X26 (a553)) % 1.07/1.25 (-. (c8_2 (a482) (a495))) % 1.07/1.25 ((a592) != (a544)) % 1.07/1.25 ((a500) != (a497)) % 1.07/1.25 (-. (c4_2 (a520) zenon_X54)) % 1.07/1.25 (-. (c1_2 (a538) zenon_X54)) % 1.07/1.25 ((a500) != zenon_X35) % 1.07/1.25 (-. (c2_2 (a496) (a553))) % 1.07/1.25 ((a480) != zenon_X150) % 1.07/1.25 ((a577) != (a471)) % 1.07/1.25 (ndr1_1 (a533)) % 1.07/1.25 (zenon_X29 != zenon_X33) % 1.07/1.25 (-. (c3_1 (a520))) % 1.07/1.25 ((a499) != zenon_X83) % 1.07/1.25 ((a482) != zenon_X27) % 1.07/1.25 ((a497) != zenon_X54) % 1.07/1.25 ((a571) != zenon_X16) % 1.07/1.25 (zenon_X59 != zenon_X54) % 1.07/1.25 ((a535) != zenon_X64) % 1.07/1.25 (zenon_X27 != zenon_X26) % 1.07/1.25 (c8_1 zenon_X0) % 1.07/1.25 (c7_2 (a533) (a553)) % 1.07/1.25 ((a482) != (a496)) % 1.07/1.25 (-. (c3_2 (a494) (a495))) % 1.07/1.25 ((a495) != zenon_X55) % 1.07/1.25 (c2_2 (a468) (a467)) % 1.07/1.25 (-. (c2_2 (a520) (a460))) % 1.07/1.25 ((a497) != zenon_X16) % 1.07/1.25 ((a544) != zenon_X9) % 1.07/1.25 ((a571) != zenon_X47) % 1.07/1.25 ((a483) != (a495)) % 1.07/1.25 ((a533) != zenon_X17) % 1.07/1.25 (c8_1 zenon_X27) % 1.07/1.25 (-. (c1_2 (a538) (a480))) % 1.07/1.25 (zenon_X19 != zenon_X21) % 1.07/1.25 ((a535) != zenon_X113) % 1.07/1.25 (-. (c3_1 zenon_X24)) % 1.07/1.25 ((a573) != zenon_X9) % 1.07/1.25 (zenon_X11 != zenon_X30) % 1.07/1.25 ((a468) != zenon_X27) % 1.07/1.25 ((a570) != zenon_X11) % 1.07/1.25 ((a460) != (a487)) % 1.07/1.25 ((a460) != zenon_X47) % 1.07/1.25 (zenon_X29 != zenon_X21) % 1.07/1.25 ((a483) != zenon_X51) % 1.07/1.25 ((a472) != (a545)) % 1.07/1.25 (-. (c2_2 zenon_X12 (a553))) % 1.07/1.25 (c4_2 (a533) (a480)) % 1.07/1.25 ((a566) != zenon_X0) % 1.07/1.25 ((a578) != zenon_X8) % 1.07/1.25 ((a496) != (a566)) % 1.07/1.25 ((a571) != zenon_X67) % 1.07/1.25 (zenon_X24 != (a533)) % 1.07/1.25 ((a548) != zenon_X108) % 1.07/1.25 (zenon_X89 != (a495)) % 1.07/1.25 (c1_1 zenon_X9) % 1.07/1.25 ((a471) != (a463)) % 1.07/1.25 (c1_2 (a601) zenon_X116) % 1.07/1.25 ((a494) != zenon_X22) % 1.07/1.25 (-. (c8_2 zenon_X3 (a483))) % 1.07/1.25 (-. (c4_2 (a494) zenon_X146)) % 1.07/1.25 (zenon_X113 != (a500)) % 1.07/1.25 (-. (c6_1 zenon_X27)) % 1.07/1.25 (zenon_X0 != (a482)) % 1.07/1.25 (-. (c2_2 zenon_X30 zenon_X130)) % 1.07/1.25 (c6_2 zenon_X21 (a553)) % 1.07/1.25 (zenon_X27 != (a566)) % 1.07/1.25 ((a571) != (a567)) % 1.07/1.25 ((a533) != (a566)) % 1.07/1.25 (zenon_X72 != (a495)) % 1.07/1.25 ((a567) != (a535)) % 1.07/1.25 (zenon_X9 != zenon_X26) % 1.07/1.25 ((a520) != (a494)) % 1.07/1.25 (-. (c8_2 (a534) (a495))) % 1.07/1.25 (zenon_X0 != zenon_X19) % 1.07/1.25 (-. (c3_1 (a538))) % 1.07/1.25 (ndr1_1 (a570)) % 1.07/1.25 (zenon_X40 != (a495)) % 1.07/1.25 ((a468) != (a463)) % 1.07/1.25 ((a553) != zenon_X99) % 1.07/1.25 (-. (c4_2 (a463) (a500))) % 1.07/1.25 (c6_2 (a534) (a553)) % 1.07/1.25 (c5_2 (a544) (a484)) % 1.07/1.25 (zenon_X35 != zenon_X2) % 1.07/1.25 ((a494) != zenon_X7) % 1.07/1.25 (-. (c2_2 (a592) zenon_X129)) % 1.07/1.25 (zenon_X9 != (a496)) % 1.07/1.25 ((a521) != zenon_X86) % 1.07/1.25 ((a460) != zenon_X66) % 1.07/1.25 (zenon_X26 != (a566)) % 1.07/1.25 ((a570) != zenon_X21) % 1.07/1.25 (zenon_X35 != (a472)) % 1.07/1.25 ((a566) != (a498)) % 1.07/1.25 (zenon_X9 != zenon_X24) % 1.07/1.25 (-. (c2_2 (a566) (a483))) % 1.07/1.25 ((a533) != (a498)) % 1.07/1.25 (-. (c5_1 zenon_X33)) % 1.07/1.25 ((a482) != (a601)) % 1.07/1.25 (zenon_X29 != (a544)) % 1.07/1.25 (-. (c8_1 zenon_X29)) % 1.07/1.25 ((a535) != zenon_X73) % 1.07/1.25 (zenon_X14 != zenon_X59) % 1.07/1.25 (zenon_X42 != (a495)) % 1.07/1.25 ((a483) != zenon_X46) % 1.07/1.25 ((a497) != (a553)) % 1.07/1.25 ((a483) != zenon_X57) % 1.07/1.25 ((a460) != zenon_X1) % 1.07/1.25 (-. (c7_2 (a498) zenon_X58)) % 1.07/1.25 ((a578) != zenon_X55) % 1.07/1.25 ((a573) != (a592)) % 1.07/1.25 ((a570) != (a601)) % 1.07/1.25 (zenon_X0 != (a570)) % 1.07/1.25 (-. (c3_1 (a463))) % 1.07/1.25 ((a499) != zenon_X58) % 1.07/1.25 (-. (c7_2 (a498) (a553))) % 1.07/1.25 ((a577) != zenon_X24) % 1.07/1.25 (c4_2 (a544) zenon_X92) % 1.07/1.25 ((a471) != (a468)) % 1.07/1.25 ((a500) != (a467)) % 1.07/1.25 (zenon_X123 != (a545)) % 1.07/1.25 (-. (c6_2 zenon_X27 (a480))) % 1.07/1.25 (c8_2 (a498) (a500)) % 1.07/1.25 (-. (c8_2 zenon_X3 (a578))) % 1.07/1.25 ((a573) != (a463)) % 1.07/1.25 ((a483) != zenon_X10) % 1.07/1.25 ((a601) != (a498)) % 1.07/1.25 (-. (c7_2 zenon_X17 (a460))) % 1.07/1.25 (-. (c7_2 (a496) zenon_X114)) % 1.07/1.25 ((a494) != zenon_X13) % 1.07/1.25 (-. (c3_2 (a601) (a553))) % 1.07/1.25 ((a544) != zenon_X27) % 1.07/1.25 (-. (c2_2 (a471) zenon_X126)) % 1.07/1.25 (-. (c2_2 zenon_X19 zenon_X157)) % 1.07/1.25 ((a472) != (a553)) % 1.07/1.25 (-. (c4_2 (a482) zenon_X93)) % 1.07/1.25 (c3_1 zenon_X29) % 1.07/1.25 (zenon_X14 != zenon_X90) % 1.07/1.25 ((a521) != (a467)) % 1.07/1.25 ((a553) != zenon_X120) % 1.07/1.25 ((a578) != zenon_X1) % 1.07/1.25 (zenon_X12 != (a471)) % 1.07/1.25 (-. (c2_2 (a573) (a571))) % 1.07/1.25 (-. (c2_2 (a577) zenon_X127)) % 1.07/1.25 (c5_2 (a544) (a480)) % 1.07/1.25 (zenon_X29 != (a592)) % 1.07/1.25 ((a508) != (a577)) % 1.07/1.25 ((a467) != zenon_X152) % 1.07/1.25 (c3_2 (a592) (a460)) % 1.07/1.25 (-. (c8_2 (a498) (a535))) % 1.07/1.25 (-. (c2_2 (a482) (a521))) % 1.07/1.25 ((a548) != (a495)) % 1.07/1.25 (zenon_X30 != (a494)) % 1.07/1.25 (zenon_X24 != (a538)) % 1.07/1.25 (-. (c4_2 (a573) zenon_X96)) % 1.07/1.25 (ndr1_1 (a520)) % 1.07/1.25 ((a480) != zenon_X97) % 1.07/1.25 ((a534) != zenon_X21) % 1.07/1.25 ((a484) != zenon_X54) % 1.07/1.25 ((a566) != (a592)) % 1.07/1.25 ((a601) != (a463)) % 1.07/1.25 (zenon_X26 != (a498)) % 1.07/1.25 (-. (c2_2 (a544) (a467))) % 1.07/1.25 ((a520) != (a508)) % 1.07/1.25 (c3_2 (a498) zenon_X41) % 1.07/1.25 ((a496) != (a573)) % 1.07/1.25 ((a533) != zenon_X33) % 1.07/1.25 (c3_2 zenon_X30 zenon_X31) % 1.07/1.25 (c1_1 (a570)) % 1.07/1.25 ((a553) != zenon_X132) % 1.07/1.25 ((a535) != (a487)) % 1.07/1.25 (zenon_X30 != (a496)) % 1.07/1.25 ((a592) != zenon_X13) % 1.07/1.25 ((a521) != zenon_X10) % 1.07/1.25 ((a535) != (a548)) % 1.07/1.25 ((a487) != zenon_X94) % 1.07/1.25 ((a498) != zenon_X19) % 1.07/1.25 (-. (c8_2 (a482) zenon_X119)) % 1.07/1.25 ((a494) != zenon_X9) % 1.07/1.25 (-. (c2_2 (a533) (a460))) % 1.07/1.25 (c3_2 (a534) zenon_X39) % 1.07/1.25 (zenon_X26 != zenon_X11) % 1.07/1.25 (zenon_X97 != (a500)) % 1.07/1.25 (-. (c6_1 (a570))) % 1.07/1.25 (zenon_X26 != (a577)) % 1.07/1.25 (zenon_X20 != zenon_X113) % 1.07/1.25 ((a460) != (a500)) % 1.07/1.25 (-. (c5_1 (a463))) % 1.07/1.25 (c1_2 zenon_X32 (a460)) % 1.07/1.25 (zenon_X12 != zenon_X11) % 1.07/1.25 (c3_2 (a520) zenon_X40) % 1.07/1.25 ((a521) != zenon_X16) % 1.07/1.25 (c5_1 (a601)) % 1.07/1.25 ((a573) != (a468)) % 1.07/1.25 ((a535) != (a553)) % 1.07/1.25 ((a468) != zenon_X17) % 1.07/1.25 (-. (c2_2 zenon_X11 zenon_X152)) % 1.07/1.25 (zenon_X38 != (a553)) % 1.07/1.25 (c3_0) % 1.07/1.25 (-. (c8_1 (a544))) % 1.07/1.25 ((a499) != zenon_X15) % 1.07/1.25 (c4_2 (a544) zenon_X20) % 1.07/1.25 (c3_1 (a471)) % 1.07/1.25 (-. (c3_1 (a566))) % 1.07/1.25 (zenon_X27 != zenon_X21) % 1.07/1.25 ((a487) != (a548)) % 1.07/1.25 ((a498) != (a471)) % 1.07/1.25 ((a480) != zenon_X2) % 1.07/1.25 (-. (c4_2 (a534) (a460))) % 1.07/1.25 (ndr1_1 (a566)) % 1.07/1.25 (ndr1_1 (a544)) % 1.07/1.25 ((a487) != zenon_X97) % 1.07/1.25 ((a571) != zenon_X6) % 1.07/1.25 ((a533) != (a463)) % 1.07/1.25 (zenon_X92 != (a500)) % 1.07/1.25 (-. (c7_2 zenon_X24 zenon_X134)) % 1.07/1.25 (-. (c7_2 zenon_X12 (a548))) % 1.07/1.25 (zenon_X14 != zenon_X54) % 1.07/1.25 (-. (c2_1 zenon_X21)) % 1.07/1.25 (-. (c4_1 (a498))) % 1.07/1.25 (c3_2 zenon_X29 (a553)) % 1.07/1.25 (zenon_X24 != (a471)) % 1.07/1.25 (c2_1 zenon_X12) % 1.07/1.25 ((a548) != zenon_X54) % 1.07/1.25 ((a571) != (a487)) % 1.07/1.25 (-. (c7_2 zenon_X27 (a548))) % 1.07/1.25 (zenon_X19 != zenon_X26) % 1.07/1.25 (-. (c6_1 zenon_X9)) % 1.07/1.25 ((a577) != (a520)) % 1.07/1.25 (-. (c2_2 zenon_X9 (a571))) % 1.07/1.25 ((a482) != zenon_X9) % 1.07/1.25 (zenon_X20 != zenon_X54) % 1.07/1.25 (zenon_X73 != (a545)) % 1.07/1.25 (-. (c2_2 (a498) (a467))) % 1.07/1.25 (-. (c4_2 (a498) zenon_X54)) % 1.07/1.25 (c5_2 (a544) zenon_X73) % 1.07/1.25 (c3_2 zenon_X12 (a548)) % 1.07/1.25 (c6_2 zenon_X9 (a553)) % 1.07/1.25 (c3_1 (a601)) % 1.07/1.25 ((a573) != (a533)) % 1.07/1.25 (-. (c2_2 (a538) zenon_X51)) % 1.07/1.25 ((a467) != zenon_X157) % 1.07/1.25 ((a535) != zenon_X65) % 1.07/1.25 (-. (c6_1 zenon_X26)) % 1.07/1.25 (c3_2 (a538) (a499)) % 1.07/1.25 ((a500) != zenon_X2) % 1.07/1.25 (zenon_X116 != zenon_X1) % 1.07/1.25 (-. (c4_2 (a538) (a480))) % 1.07/1.25 ((a545) != (a521)) % 1.07/1.25 ((a468) != (a534)) % 1.07/1.25 (-. (c5_2 (a592) (a484))) % 1.07/1.25 ((a573) != (a566)) % 1.07/1.25 ((a497) != (a460)) % 1.07/1.25 ((a573) != zenon_X29) % 1.07/1.25 ((a467) != zenon_X130) % 1.07/1.25 (-. (c8_2 (a577) (a579))) % 1.07/1.25 (-. (c4_2 zenon_X24 (a545))) % 1.07/1.25 ((a592) != (a601)) % 1.07/1.25 (-. (c8_2 (a498) (a495))) % 1.07/1.25 ((a592) != zenon_X12) % 1.07/1.25 ((a508) != zenon_X24) % 1.07/1.25 (zenon_X27 != zenon_X24) % 1.07/1.25 (c4_2 (a544) zenon_X59) % 1.07/1.25 ((a601) != zenon_X27) % 1.07/1.25 ((a538) != zenon_X30) % 1.07/1.25 ((a535) != zenon_X23) % 1.07/1.25 (c3_2 (a544) zenon_X38) % 1.07/1.25 ((a535) != zenon_X154) % 1.07/1.25 (-. (c1_2 (a566) (a571))) % 1.07/1.25 (zenon_X0 != zenon_X21) % 1.07/1.25 ((a521) != zenon_X52) % 1.07/1.25 ((a482) != zenon_X24) % 1.07/1.25 (c7_2 (a508) (a553)) % 1.07/1.25 (zenon_X0 != zenon_X17) % 1.07/1.25 ((a533) != zenon_X21) % 1.07/1.25 (-. (c7_2 (a566) (a548))) % 1.07/1.25 (-. (c1_2 (a538) zenon_X123)) % 1.07/1.25 (c6_2 zenon_X27 (a553)) % 1.07/1.25 (c3_2 (a508) (a548)) % 1.07/1.25 (c3_2 zenon_X19 (a495)) % 1.07/1.25 (-. (c2_2 zenon_X9 (a535))) % 1.07/1.25 (zenon_X11 != zenon_X33) % 1.07/1.25 ((a570) != (a496)) % 1.07/1.25 (-. (c2_2 (a508) zenon_X57)) % 1.07/1.25 ((a480) != zenon_X123) % 1.07/1.25 (zenon_X20 != (a548)) % 1.07/1.25 (zenon_X20 != (a460)) % 1.07/1.25 (-. (c7_2 zenon_X11 (a553))) % 1.07/1.25 (zenon_X14 != (a460)) % 1.07/1.25 (-. (c6_1 (a496))) % 1.07/1.25 (-. (c1_2 (a538) (a535))) % 1.07/1.25 ((a487) != zenon_X145) % 1.07/1.25 ((a460) != zenon_X2) % 1.07/1.25 (c1_2 zenon_X27 (a487)) % 1.07/1.25 ((a471) != (a538)) % 1.07/1.25 (c3_2 (a544) (a553)) % 1.07/1.25 (c8_2 (a482) (a483)) % 1.07/1.25 (-. (c6_1 zenon_X21)) % 1.07/1.25 (c4_2 (a544) (a548)) % 1.07/1.25 (zenon_X24 != zenon_X19) % 1.07/1.25 (c6_2 (a533) (a553)) % 1.07/1.25 (-. (c7_2 zenon_X26 zenon_X88)) % 1.07/1.25 ((a534) != zenon_X19) % 1.07/1.25 ((a472) != zenon_X58) % 1.07/1.25 (-. (c7_2 (a498) zenon_X61)) % 1.07/1.25 ((a498) != zenon_X30) % 1.07/1.25 (zenon_X26 != zenon_X24) % 1.07/1.25 ((a570) != (a520)) % 1.07/1.25 ((a460) != zenon_X50) % 1.07/1.25 (-. (c6_1 (a534))) % 1.07/1.25 ((a482) != zenon_X11) % 1.07/1.25 (ndr1_1 zenon_X24) % 1.07/1.25 (c3_2 zenon_X9 (a460)) % 1.07/1.25 ((a483) != zenon_X6) % 1.07/1.25 ((a566) != (a520)) % 1.07/1.25 ((a521) != zenon_X57) % 1.07/1.25 (-. (c3_1 zenon_X17)) % 1.07/1.25 (-. (c4_2 zenon_X19 (a500))) % 1.07/1.25 (zenon_X29 != zenon_X26) % 1.07/1.25 (zenon_X28 != (a579)) % 1.07/1.25 ((a553) != zenon_X15) % 1.07/1.25 (zenon_X13 != zenon_X26) % 1.07/1.25 (-. (c6_2 (a534) (a535))) % 1.07/1.25 (-. (c2_2 (a468) zenon_X86)) % 1.07/1.25 ((a553) != zenon_X147) % 1.07/1.25 ((a538) != (a534)) % 1.07/1.25 (zenon_X29 != (a538)) % 1.07/1.25 (zenon_X19 != zenon_X33) % 1.07/1.25 ((a571) != zenon_X46) % 1.07/1.25 ((a468) != zenon_X26) % 1.07/1.25 (zenon_X13 != (a577)) % 1.07/1.25 (c6_2 (a494) (a495)) % 1.07/1.25 (-. (c3_1 (a498))) % 1.07/1.25 (-. (c7_2 zenon_X9 zenon_X132)) % 1.07/1.25 ((a500) != (a545)) % 1.07/1.25 ((a601) != zenon_X26) % 1.07/1.25 ((a482) != (a534)) % 1.07/1.25 ((a544) != zenon_X33) % 1.07/1.25 ((a548) != zenon_X57) % 1.07/1.25 (-. (c8_2 (a494) (a500))) % 1.07/1.25 (zenon_X12 != zenon_X29) % 1.07/1.25 (-. (c6_1 (a538))) % 1.07/1.25 ((a592) != (a471)) % 1.07/1.25 (c5_2 (a570) zenon_X36) % 1.07/1.25 (c1_1 (a482)) % 1.07/1.25 (-. (c6_1 zenon_X12)) % 1.07/1.25 (c5_2 (a494) zenon_X35) % 1.07/1.25 (c5_2 (a544) (a521)) % 1.07/1.25 (c1_2 zenon_X9 (a487)) % 1.07/1.25 (-. (c2_1 zenon_X29)) % 1.07/1.25 ((a494) != (a592)) % 1.07/1.25 ((a460) != (a472)) % 1.07/1.25 (-. (c2_2 (a538) (a521))) % 1.07/1.25 ((a544) != (a534)) % 1.07/1.25 (zenon_X24 != (a463)) % 1.07/1.25 (-. (c4_2 zenon_X24 zenon_X54)) % 1.07/1.25 ((a601) != zenon_X17) % 1.07/1.25 (-. (c4_1 (a577))) % 1.07/1.25 ((a498) != zenon_X33) % 1.07/1.25 ((a578) != (a495)) % 1.07/1.25 ((a460) != (a521)) % 1.07/1.25 ((a535) != zenon_X91) % 1.07/1.25 (-. (c2_2 (a573) (a483))) % 1.07/1.25 (-. (c2_1 zenon_X17)) % 1.07/1.25 ((a592) != zenon_X26) % 1.07/1.25 (zenon_X123 != zenon_X16) % 1.07/1.25 (zenon_X160 != (a553)) % 1.07/1.25 (-. (c7_2 (a471) zenon_X60)) % 1.07/1.25 (c3_2 (a496) zenon_X42) % 1.07/1.25 (zenon_X21 != zenon_X33) % 1.07/1.25 (-. (c7_2 (a573) (a553))) % 1.07/1.25 (-. (c7_2 (a566) zenon_X83)) % 1.07/1.25 ((a487) != (a472)) % 1.07/1.25 ((a566) != (a463)) % 1.07/1.25 (-. (c4_2 zenon_X21 zenon_X170)) % 1.07/1.25 ((a535) != zenon_X165) % 1.07/1.25 ((a592) != (a508)) % 1.07/1.25 (-. (c4_2 zenon_X19 zenon_X20)) % 1.07/1.25 ((a487) != (a484)) % 1.07/1.25 (-. (c2_2 zenon_X11 (a548))) % 1.07/1.25 (zenon_X20 != zenon_X97) % 1.07/1.25 ((a538) != zenon_X33) % 1.07/1.25 (-. (c7_2 (a544) zenon_X124)) % 1.07/1.25 ((a548) != zenon_X110) % 1.07/1.25 (-. (c4_2 zenon_X33 zenon_X123)) % 1.07/1.25 ((a495) != (a535)) % 1.07/1.25 (-. (c7_2 (a538) (a548))) % 1.07/1.25 (-. (c3_2 zenon_X26 (a553))) % 1.07/1.25 ((a535) != zenon_X20) % 1.07/1.25 ((a500) != (a487)) % 1.07/1.25 (-. (c2_2 (a592) (a548))) % 1.07/1.25 ((a498) != zenon_X3) % 1.07/1.25 ((a487) != zenon_X173) % 1.07/1.25 (zenon_X9 != (a498)) % 1.07/1.25 ((a498) != zenon_X11) % 1.07/1.25 ((a460) != (a571)) % 1.07/1.25 (-. (c8_2 (a577) zenon_X55)) % 1.07/1.25 (c7_1 (a498)) % 1.07/1.25 ((a538) != zenon_X9) % 1.07/1.25 (zenon_X24 != (a520)) % 1.07/1.25 (c4_1 (a570)) % 1.07/1.25 ((a566) != zenon_X9) % 1.07/1.25 ((a467) != zenon_X55) % 1.07/1.25 ((a566) != (a601)) % 1.07/1.25 (-. (c8_1 zenon_X30)) % 1.07/1.25 ((a460) != zenon_X169) % 1.07/1.25 ((a535) != (a483)) % 1.07/1.25 (-. (c8_2 zenon_X3 (a535))) % 1.07/1.25 ((a494) != zenon_X33) % 1.07/1.25 (-. (c3_2 zenon_X9 (a553))) % 1.07/1.25 (zenon_X0 != (a534)) % 1.07/1.25 (c1_1 (a538)) % 1.07/1.25 ((a538) != (a533)) % 1.07/1.25 (c2_1 (a570)) % 1.07/1.25 ((a566) != zenon_X19) % 1.07/1.25 ((a578) != (a499)) % 1.07/1.25 (c4_2 (a544) zenon_X48) % 1.07/1.25 ((a573) != zenon_X13) % 1.07/1.25 ((a483) != (a500)) % 1.07/1.25 (zenon_X73 != (a500)) % 1.07/1.25 ((a467) != (a579)) % 1.07/1.25 (c6_2 (a482) (a553)) % 1.07/1.25 ((a480) != (a500)) % 1.07/1.25 (c2_2 (a482) (a483)) % 1.07/1.25 (zenon_X73 != zenon_X16) % 1.07/1.25 (-. (c5_2 (a592) (a548))) % 1.07/1.25 (-. (c2_2 (a520) (a548))) % 1.07/1.25 (-. (c4_2 (a496) (a497))) % 1.07/1.25 ((a467) != (a545)) % 1.07/1.25 (-. (c1_2 (a538) zenon_X113)) % 1.07/1.25 ((a500) != zenon_X16) % 1.07/1.25 (c3_2 (a573) (a548)) % 1.07/1.25 (c7_2 (a494) (a553)) % 1.07/1.25 (-. (c1_2 (a538) zenon_X97)) % 1.07/1.25 (c7_2 (a471) (a472)) % 1.07/1.25 (zenon_X0 != zenon_X9) % 1.07/1.25 (zenon_X28 != (a535)) % 1.07/1.25 (c7_2 (a570) (a553)) % 1.07/1.25 (c5_2 (a544) (a497)) % 1.07/1.25 (c1_1 (a494)) % 1.07/1.25 ((a553) != zenon_X69) % 1.07/1.25 (-. (c4_2 (a468) zenon_X159)) % 1.07/1.25 ((a487) != zenon_X123) % 1.07/1.25 ((a483) != (a579)) % 1.07/1.25 (-. (c4_2 zenon_X21 (a487))) % 1.07/1.25 (c5_2 zenon_X32 (a460)) % 1.07/1.25 (c4_2 (a544) zenon_X123) % 1.07/1.25 (-. (c2_2 (a533) zenon_X108)) % 1.07/1.25 (c7_2 (a498) (a499)) % 1.07/1.25 ((a548) != zenon_X47) % 1.07/1.25 (zenon_X19 != zenon_X27) % 1.07/1.25 (-. (c2_2 (a534) (a483))) % 1.07/1.25 ((a535) != zenon_X46) % 1.07/1.25 (-. (c7_2 zenon_X33 (a499))) % 1.07/1.25 (ndr1_1 zenon_X9) % 1.07/1.25 (-. (c4_2 (a538) zenon_X14)) % 1.07/1.25 (c6_2 (a498) (a500)) % 1.07/1.25 (zenon_X113 != zenon_X54) % 1.07/1.25 (-. (c3_2 (a494) (a553))) % 1.07/1.25 (c5_2 (a573) (a521)) % 1.07/1.25 (c7_2 zenon_X9 (a553)) % 1.07/1.25 (zenon_X9 != zenon_X11) % 1.07/1.25 (-. (c2_2 (a482) zenon_X52)) % 1.07/1.25 ((a566) != (a538)) % 1.07/1.25 (-. (c5_1 zenon_X17)) % 1.07/1.25 ((a571) != (a545)) % 1.07/1.25 (-. (c4_2 (a520) (a521))) % 1.07/1.25 ((a601) != zenon_X29) % 1.07/1.25 (-. (c2_2 zenon_X27 zenon_X168)) % 1.07/1.25 ((a548) != zenon_X127) % 1.07/1.25 ((a460) != zenon_X34) % 1.07/1.25 ((a482) != zenon_X33) % 1.07/1.25 (-. (c1_2 (a592) (a487))) % 1.07/1.25 (-. (c4_2 (a498) zenon_X59)) % 1.07/1.25 ((a482) != zenon_X3) % 1.07/1.25 ((a553) != zenon_X105) % 1.07/1.25 (zenon_X13 != (a534)) % 1.07/1.25 (zenon_X21 != zenon_X17) % 1.07/1.25 ((a496) != (a577)) % 1.07/1.25 ((a570) != zenon_X22) % 1.07/1.25 (-. (c4_2 zenon_X17 (a480))) % 1.07/1.25 (zenon_X0 != zenon_X30) % 1.07/1.25 (c3_2 (a592) (a495)) % 1.07/1.25 (-. (c4_2 zenon_X19 (a545))) % 1.07/1.25 (c4_2 zenon_X9 (a487)) % 1.07/1.25 (zenon_X24 != zenon_X33) % 1.07/1.25 ((a460) != zenon_X25) % 1.07/1.25 (c2_2 (a573) (a548)) % 1.07/1.25 ((a535) != zenon_X54) % 1.07/1.25 ((a592) != (a520)) % 1.07/1.25 (c5_2 (a544) (a535)) % 1.07/1.25 ((a483) != (a548)) % 1.07/1.25 (-. (c7_2 (a566) (a499))) % 1.07/1.25 ((a548) != zenon_X125) % 1.07/1.25 (zenon_X11 != (a573)) % 1.07/1.25 (-. (c2_1 zenon_X26)) % 1.07/1.25 (-. (c2_2 (a566) (a571))) % 1.07/1.25 ((a487) != zenon_X1) % 1.07/1.25 (zenon_X29 != (a494)) % 1.07/1.25 ((a460) != (a578)) % 1.07/1.25 ((a498) != (a538)) % 1.07/1.25 ((a570) != (a533)) % 1.07/1.25 (-. (c2_2 (a534) (a460))) % 1.07/1.25 ((a548) != (a553)) % 1.07/1.25 (c2_1 (a601)) % 1.07/1.25 ((a467) != (a499)) % 1.07/1.25 ((a500) != (a521)) % 1.07/1.25 ((a571) != zenon_X49) % 1.07/1.25 (c6_2 (a494) (a460)) % 1.07/1.25 (-. (c4_2 (a538) (a545))) % 1.07/1.25 ((a460) != zenon_X36) % 1.07/1.25 (c1_1 (a508)) % 1.07/1.25 (-. (c7_2 (a573) zenon_X95)) % 1.07/1.25 ((a521) != zenon_X51) % 1.07/1.25 ((a570) != (a471)) % 1.07/1.25 ((a601) != zenon_X21) % 1.07/1.25 (-. (c4_2 (a566) zenon_X158)) % 1.07/1.25 (-. (c5_2 (a592) (a480))) % 1.07/1.25 (-. (c3_1 (a592))) % 1.07/1.25 (-. (c5_1 zenon_X29)) % 1.07/1.25 ((a508) != (a482)) % 1.07/1.25 (-. (c1_2 (a538) zenon_X90)) % 1.07/1.25 ((a460) != (a495)) % 1.07/1.25 (c3_2 zenon_X19 zenon_X160) % 1.07/1.25 (-. (c4_2 zenon_X19 (a460))) % 1.07/1.25 (c5_2 zenon_X29 (a553)) % 1.07/1.25 ((a460) != zenon_X135) % 1.07/1.25 (-. (c7_2 zenon_X11 zenon_X101)) % 1.07/1.25 (-. (c3_1 zenon_X33)) % 1.07/1.25 ((a578) != (a579)) % 1.07/1.25 ((a592) != zenon_X27) % 1.07/1.25 ((a544) != (a482)) % 1.07/1.25 ((a520) != (a496)) % 1.07/1.25 (-. (c6_2 zenon_X29 zenon_X135)) % 1.07/1.25 (-. (c2_1 (a566))) % 1.07/1.25 ((a577) != zenon_X30) % 1.07/1.25 (c3_2 zenon_X27 (a548)) % 1.07/1.25 ((a535) != zenon_X92) % 1.07/1.25 (-. (c1_1 zenon_X24)) % 1.07/1.25 ((a548) != zenon_X51) % 1.07/1.25 (ndr1_1 zenon_X26) % 1.07/1.25 (c3_2 zenon_X27 (a495)) % 1.07/1.25 ((a553) != zenon_X124) % 1.07/1.25 (c8_1 (a494)) % 1.07/1.25 ((a460) != (a553)) % 1.07/1.25 (-. (c8_2 (a498) (a499))) % 1.07/1.25 ((a535) != zenon_X48) % 1.07/1.25 (c5_2 (a544) zenon_X20) % 1.07/1.25 ((a592) != zenon_X0) % 1.07/1.25 (c1_2 (a601) (a460)) % 1.07/1.25 ((a460) != zenon_X119) % 1.07/1.25 (-. (c7_2 (a570) (a548))) % 1.07/1.25 ((a497) != (a545)) % 1.07/1.25 (-. (c4_1 (a592))) % 1.07/1.25 (c6_2 (a494) (a553)) % 1.07/1.25 ((a480) != zenon_X107) % 1.07/1.25 (c4_2 (a482) (a487)) % 1.07/1.25 ((a553) != zenon_X88) % 1.07/1.25 ((a553) != zenon_X95) % 1.07/1.25 ((a521) != zenon_X54) % 1.07/1.25 ((a553) != zenon_X141) % 1.07/1.25 (zenon_X164 != (a495)) % 1.07/1.25 ((a467) != zenon_X50) % 1.07/1.25 (zenon_X89 != (a553)) % 1.07/1.25 (-. (c4_2 (a534) zenon_X16)) % 1.07/1.25 (-. (c3_1 (a544))) % 1.07/1.25 ((a570) != (a592)) % 1.07/1.25 (-. (c2_1 (a498))) % 1.07/1.25 (-. (c2_2 zenon_X30 (a521))) % 1.07/1.25 (-. (c2_1 zenon_X19)) % 1.07/1.25 ((a578) != (a487)) % 1.07/1.25 (-. (c2_2 zenon_X19 (a467))) % 1.07/1.25 (-. (c8_1 (a463))) % 1.07/1.25 (ndr1_1 zenon_X27) % 1.07/1.25 ((a534) != (a496)) % 1.07/1.25 ((a535) != (a497)) % 1.07/1.25 (-. (c4_2 (a534) zenon_X54)) % 1.07/1.25 (zenon_X135 != (a553)) % 1.07/1.25 (-. (c1_2 (a592) (a571))) % 1.07/1.25 (c3_2 (a520) (a553)) % 1.07/1.25 (c3_2 zenon_X0 (a553)) % 1.07/1.25 (zenon_X5 != (a577)) % 1.07/1.25 (c4_2 zenon_X29 (a553)) % 1.07/1.25 ((a483) != zenon_X67) % 1.07/1.25 (-. (c6_1 (a566))) % 1.07/1.25 ((a480) != zenon_X73) % 1.07/1.25 (-. (c4_2 (a544) (a460))) % 1.07/1.25 ((a496) != zenon_X17) % 1.07/1.25 ((a460) != zenon_X65) % 1.07/1.25 (zenon_X12 != (a496)) % 1.07/1.25 ((a538) != zenon_X21) % 1.07/1.25 ((a553) != zenon_X153) % 1.07/1.25 (zenon_X59 != (a460)) % 1.07/1.25 ((a460) != zenon_X35) % 1.07/1.25 ((a548) != zenon_X86) % 1.07/1.25 ((a494) != (a498)) % 1.07/1.25 ((a553) != zenon_X138) % 1.07/1.25 ((a571) != zenon_X10) % 1.07/1.25 (c1_2 (a482) (a487)) % 1.07/1.25 ((a538) != zenon_X27) % 1.07/1.25 (-. (c1_2 (a566) (a545))) % 1.07/1.25 (-. (c2_2 (a508) (a521))) % 1.07/1.25 (ndr1_0) % 1.07/1.25 (c3_2 (a577) zenon_X37) % 1.07/1.25 (-. (c4_2 (a468) (a487))) % 1.07/1.25 (zenon_X24 != (a566)) % 1.07/1.25 (-. (c4_2 (a508) zenon_X144)) % 1.07/1.25 (c5_2 (a544) zenon_X92) % 1.07/1.25 (zenon_X19 != zenon_X9) % 1.07/1.25 (zenon_X0 != zenon_X26) % 1.07/1.25 ((a494) != zenon_X24) % 1.07/1.25 (-. (c2_2 (a494) (a483))) % 1.07/1.25 ((a570) != (a482)) % 1.07/1.25 ((a544) != (a494)) % 1.07/1.25 ((a545) != zenon_X16) % 1.07/1.25 (-. (c2_1 zenon_X33)) % 1.07/1.25 (-. (c8_2 (a534) (a483))) % 1.07/1.25 ((a494) != zenon_X3) % 1.07/1.25 ((a548) != zenon_X65) % 1.07/1.25 (zenon_X30 != zenon_X21) % 1.07/1.25 (c5_1 zenon_X19) % 1.07/1.25 ((a601) != zenon_X24) % 1.07/1.25 ((a460) != zenon_X124) % 1.07/1.25 (zenon_X26 != (a471)) % 1.07/1.25 (zenon_X24 != zenon_X17) % 1.07/1.25 (zenon_X133 != (a495)) % 1.07/1.25 (-. (c2_2 (a533) (a553))) % 1.07/1.25 ((a548) != zenon_X50) % 1.07/1.25 ((a548) != zenon_X52) % 1.07/1.25 ((a535) != zenon_X4) % 1.07/1.25 ((a570) != (a498)) % 1.07/1.25 (c3_2 (a496) (a497)) % 1.07/1.25 ((a578) != zenon_X66) % 1.07/1.25 (-. (c1_2 (a538) (a545))) % 1.07/1.25 ((a553) != zenon_X58) % 1.07/1.25 (zenon_X0 != (a494)) % 1.07/1.25 (c4_2 zenon_X27 (a487)) % 1.07/1.25 ((a553) != zenon_X174) % 1.07/1.25 (-. (c7_2 (a508) (a548))) % 1.07/1.25 (zenon_X29 != (a463)) % 1.07/1.25 (-. (c8_2 (a482) (a578))) % 1.07/1.25 (c5_2 (a570) (a472)) % 1.07/1.25 (-. (c4_2 (a533) (a487))) % 1.07/1.25 (c2_1 zenon_X27) % 1.07/1.25 (c3_1 (a482)) % 1.07/1.25 (ndr1_1 (a468)) % 1.07/1.25 ((a535) != zenon_X6) % 1.07/1.25 (c5_2 (a566) (a460)) % 1.07/1.25 ((a471) != zenon_X0) % 1.07/1.25 (zenon_X13 != zenon_X24) % 1.07/1.25 ((a508) != (a471)) % 1.07/1.25 (-. (c2_1 zenon_X24)) % 1.07/1.25 ((a460) != (a480)) % 1.07/1.25 (-. (c4_2 (a482) (a484))) % 1.07/1.25 (-. (c2_1 (a508))) % 1.07/1.25 (-. (c2_2 zenon_X0 zenon_X171)) % 1.07/1.25 (-. (c2_2 (a468) (a548))) % 1.07/1.25 ((a592) != (a482)) % 1.07/1.25 (zenon_X11 != (a520)) % 1.07/1.25 ((a533) != (a496)) % 1.07/1.25 (-. (c8_2 (a577) (a483))) % 1.07/1.25 (-. (c1_1 (a471))) % 1.07/1.25 (-. (c4_2 zenon_X19 zenon_X113)) % 1.07/1.25 (zenon_X29 != (a496)) % 1.07/1.25 ((a482) != (a463)) % 1.07/1.25 (-. (c7_1 (a577))) % 1.07/1.25 (zenon_X26 != (a573)) % 1.07/1.25 ((a500) != zenon_X36) % 1.07/1.25 (c3_2 zenon_X26 (a495)) % 1.07/1.25 (-. (c3_2 zenon_X29 zenon_X153)) % 1.07/1.25 ((a573) != zenon_X0) % 1.07/1.25 (-. (c7_2 zenon_X12 zenon_X80)) % 1.07/1.25 ((a460) != zenon_X23) % 1.07/1.25 ((a521) != zenon_X130) % 1.07/1.25 ((a553) != (a545)) % 1.07/1.25 ((a460) != zenon_X58) % 1.07/1.25 (zenon_X29 != (a498)) % 1.07/1.25 ((a534) != (a573)) % 1.07/1.25 (c2_2 zenon_X12 (a548)) % 1.07/1.25 (-. (c7_2 (a471) (a499))) % 1.07/1.25 ((a544) != (a533)) % 1.07/1.25 ((a495) != (a480)) % 1.07/1.25 (c4_2 (a544) (a484)) % 1.07/1.25 ((a553) != zenon_X53) % 1.07/1.25 ((a499) != zenon_X101) % 1.07/1.25 ((a577) != (a538)) % 1.07/1.25 ((a573) != (a544)) % 1.07/1.25 ((a577) != (a592)) % 1.07/1.25 (-. (c1_1 zenon_X11)) % 1.07/1.25 (-. (c4_2 zenon_X24 zenon_X20)) % 1.07/1.25 (-. (c4_2 (a520) (a500))) % 1.07/1.25 (-. (c8_2 zenon_X3 zenon_X4)) % 1.07/1.25 ((a496) != (a471)) % 1.07/1.25 (-. (c7_2 zenon_X27 zenon_X120)) % 1.07/1.25 (zenon_X9 != zenon_X27) % 1.07/1.25 (-. (c4_2 (a538) (a487))) % 1.07/1.25 (-. (c7_2 zenon_X29 zenon_X141)) % 1.07/1.25 ((a495) != zenon_X4) % 1.07/1.25 ((a548) != zenon_X168) % 1.07/1.25 (zenon_X92 != (a545)) % 1.07/1.25 ((a460) != zenon_X64) % 1.07/1.25 (zenon_X90 != zenon_X16) % 1.07/1.25 ((a508) != zenon_X21) % 1.07/1.25 (zenon_X12 != (a577)) % 1.07/1.25 (zenon_X113 != (a460)) % 1.07/1.25 ((a535) != zenon_X144) % 1.07/1.25 (-. (c2_2 (a544) zenon_X128)) % 1.07/1.25 ((a571) != (a495)) % 1.07/1.25 ((a535) != zenon_X2) % 1.07/1.25 (c3_1 zenon_X12) % 1.07/1.25 (-. (c4_2 zenon_X12 zenon_X172)) % 1.07/1.25 ((a533) != zenon_X26) % 1.07/1.25 (zenon_X12 != (a520)) % 1.07/1.25 ((a467) != zenon_X125) % 1.07/1.25 (zenon_X19 != (a471)) % 1.07/1.25 ((a460) != (a535)) % 1.07/1.25 (-. (c5_1 (a471))) % 1.07/1.25 (zenon_X21 != (a498)) % 1.07/1.25 (zenon_X164 != (a553)) % 1.07/1.25 ((a553) != zenon_X34) % 1.07/1.25 (zenon_X85 != (a545)) % 1.07/1.25 (c6_2 (a471) (a579)) % 1.07/1.25 (zenon_X113 != zenon_X16) % 1.07/1.25 ((a533) != zenon_X13) % 1.07/1.25 (zenon_X21 != (a463)) % 1.07/1.25 (c4_2 (a544) (a480)) % 1.07/1.25 (-. (c4_2 zenon_X12 (a548))) % 1.07/1.25 (zenon_X21 != (a471)) % 1.07/1.25 (zenon_X0 != (a463)) % 1.07/1.25 (-. (c1_1 (a544))) % 1.07/1.25 ((a566) != (a471)) % 1.07/1.25 (zenon_X19 != (a601)) % 1.07/1.25 (-. (c2_2 (a496) (a483))) % 1.07/1.25 (c3_2 zenon_X9 zenon_X131) % 1.07/1.25 ((a544) != (a498)) % 1.07/1.25 (zenon_X42 != (a553)) % 1.07/1.25 (c5_2 (a544) zenon_X123) % 1.07/1.25 (-. (c7_2 (a468) zenon_X142)) % 1.07/1.25 ((a570) != zenon_X7) % 1.07/1.25 (c8_2 (a468) (a467)) % 1.07/1.25 (c2_1 zenon_X9) % 1.07/1.25 ((a548) != zenon_X149) % 1.07/1.25 ((a566) != (a482)) % 1.07/1.25 (c1_1 (a566)) % 1.07/1.25 (-. (c1_2 (a538) (a487))) % 1.07/1.25 (-. (c2_2 zenon_X9 (a521))) % 1.07/1.25 ((a460) != zenon_X8) % 1.07/1.25 ((a499) != (a545)) % 1.07/1.25 (ndr1_1 (a573)) % 1.07/1.25 (zenon_X24 != (a534)) % 1.07/1.25 (c5_2 (a494) zenon_X2) % 1.07/1.25 (-. (c4_2 (a496) (a535))) % 1.07/1.25 ((a508) != zenon_X17) % 1.07/1.25 (-. (c4_2 zenon_X17 zenon_X20)) % 1.07/1.25 (zenon_X12 != (a566)) % 1.07/1.25 ((a472) != zenon_X15) % 1.07/1.25 (zenon_X27 != (a463)) % 1.07/1.25 ((a535) != (a571)) % 1.07/1.25 ((a570) != zenon_X26) % 1.07/1.25 (-. (c5_2 (a592) zenon_X35)) % 1.07/1.25 ((a483) != zenon_X65) % 1.07/1.25 (-. (c2_2 (a520) (a535))) % 1.07/1.25 (-. (c2_2 (a573) (a535))) % 1.07/1.25 (c5_2 (a544) zenon_X14) % 1.07/1.25 (zenon_X0 != (a496)) % 1.07/1.25 (zenon_X19 != zenon_X12) % 1.07/1.25 (c7_2 (a496) (a553)) % 1.07/1.25 (-. (c4_2 (a508) (a548))) % 1.07/1.25 (zenon_X19 != (a496)) % 1.07/1.25 ((a520) != zenon_X30) % 1.07/1.25 ((a548) != zenon_X128) % 1.07/1.25 (zenon_X0 != (a498)) % 1.07/1.25 (c1_1 zenon_X12) % 1.07/1.25 (-. (c4_2 (a538) (a500))) % 1.07/1.25 (-. (c1_2 (a566) (a487))) % 1.07/1.25 ((a471) != zenon_X29) % 1.07/1.25 (c3_2 zenon_X24 zenon_X112) % 1.07/1.25 ((a468) != (a508)) % 1.07/1.25 (-. (c4_2 zenon_X33 (a487))) % 1.07/1.25 ((a483) != zenon_X108) % 1.07/1.25 (c8_1 zenon_X21) % 1.07/1.25 (zenon_X14 != zenon_X113) % 1.07/1.25 ((a508) != (a534)) % 1.07/1.25 (zenon_X11 != zenon_X17) % 1.07/1.25 (-. (c1_1 zenon_X0)) % 1.07/1.25 ((a499) != (a548)) % 1.07/1.25 (c5_2 (a570) zenon_X2) % 1.07/1.25 (zenon_X12 != zenon_X17) % 1.07/1.25 (-. (c7_2 zenon_X24 (a553))) % 1.07/1.25 (c3_2 (a498) (a499)) % 1.07/1.25 ((a548) != zenon_X6) % 1.07/1.25 ((a471) != zenon_X17) % 1.07/1.25 ((a483) != zenon_X119) % 1.07/1.25 (-. (c7_2 (a566) (a553))) % 1.07/1.25 (zenon_X0 != (a520)) % 1.07/1.25 ((a573) != zenon_X30) % 1.07/1.25 ((a601) != zenon_X13) % 1.07/1.25 (c8_2 (a577) (a578)) % 1.07/1.25 ((a601) != (a577)) % 1.07/1.25 ((a567) != (a484)) % 1.07/1.25 (c8_1 zenon_X12) % 1.07/1.25 ((a571) != (a553)) % 1.07/1.25 ((a482) != zenon_X26) % 1.07/1.25 (c3_2 (a520) (a495)) % 1.07/1.25 (-. (c2_1 (a577))) % 1.07/1.25 ((a548) != zenon_X126) % 1.07/1.25 (c8_1 (a566)) % 1.07/1.25 ((a548) != zenon_X2) % 1.07/1.25 ((a534) != zenon_X29) % 1.07/1.25 ((a499) != zenon_X60) % 1.07/1.25 (-. (c2_2 (a508) (a553))) % 1.07/1.25 (zenon_X0 != (a533)) % 1.07/1.25 (c4_2 zenon_X29 (a460)) % 1.07/1.25 (zenon_X14 != (a548)) % 1.07/1.25 ((a468) != (a520)) % 1.07/1.25 (-. (c2_2 zenon_X30 (a467))) % 1.07/1.25 ((a460) != zenon_X52) % 1.07/1.25 ((a570) != zenon_X29) % 1.07/1.25 (zenon_X31 != (a545)) % 1.07/1.25 (-. (c4_1 zenon_X11)) % 1.07/1.25 ((a482) != zenon_X21) % 1.07/1.25 (zenon_X97 != zenon_X113) % 1.07/1.25 (-. (c5_2 (a471) (a472))) % 1.07/1.25 ((a483) != zenon_X25) % 1.07/1.25 (-. (c8_2 (a498) (a483))) % 1.07/1.25 (-. (c4_2 (a544) zenon_X54)) % 1.07/1.25 (c5_2 (a498) (a500)) % 1.07/1.25 (c1_2 zenon_X24 (a487)) % 1.07/1.25 ((a471) != (a533)) % 1.07/1.25 (zenon_X59 != (a545)) % 1.07/1.25 ((a553) != (a579)) % 1.07/1.25 (c3_2 (a538) (a472)) % 1.07/1.25 (c3_2 zenon_X30 (a495)) % 1.07/1.25 (-. (c8_2 (a577) (a535))) % 1.07/1.25 ((a534) != zenon_X3) % 1.07/1.25 ((a460) != zenon_X174) % 1.07/1.25 (-. (c4_2 zenon_X17 (a545))) % 1.07/1.25 (zenon_X92 != (a460)) % 1.07/1.25 (-. (c7_2 (a538) zenon_X15)) % 1.07/1.25 (-. (c2_2 (a534) (a521))) % 1.07/1.25 ((a482) != (a520)) % 1.07/1.25 ((a482) != zenon_X19) % 1.07/1.25 (zenon_X12 != (a534)) % 1.07/1.25 ((a483) != zenon_X23) % 1.07/1.25 (zenon_X27 != (a496)) % 1.07/1.25 (-. (c7_2 zenon_X0 (a472))) % 1.07/1.25 ((a592) != (a463)) % 1.07/1.25 (zenon_X9 != zenon_X17) % 1.07/1.25 (-. (c2_2 zenon_X12 (a571))) % 1.07/1.25 ((a571) != zenon_X23) % 1.07/1.25 ((a538) != (a494)) % 1.07/1.25 (c1_1 (a573)) % 1.07/1.25 (-. (c8_2 (a494) (a483))) % 1.07/1.25 ((a494) != (a468)) % 1.07/1.25 ((a487) != (a497)) % 1.07/1.25 (zenon_X26 != zenon_X17) % 1.07/1.25 ((a578) != (a567)) % 1.07/1.25 (-. (c2_2 (a508) (a460))) % 1.07/1.25 ((a570) != (a494)) % 1.07/1.25 ((a592) != (a496)) % 1.07/1.25 ((a495) != zenon_X66) % 1.07/1.25 (-. (c4_2 zenon_X27 (a548))) % 1.07/1.25 (-. (c4_2 (a463) (a545))) % 1.07/1.25 (zenon_X19 != (a570)) % 1.07/1.25 (-. (c2_2 zenon_X26 zenon_X176)) % 1.07/1.25 (-. (c4_2 (a496) zenon_X94)) % 1.07/1.25 (zenon_X24 != zenon_X30) % 1.07/1.25 (-. (c2_2 zenon_X12 zenon_X110)) % 1.07/1.25 (-. (c4_2 (a538) (a535))) % 1.07/1.25 ((a578) != zenon_X16) % 1.07/1.25 ((a520) != (a534)) % 1.07/1.25 (c3_2 (a468) (a545)) % 1.07/1.25 ((a468) != (a566)) % 1.07/1.25 (c6_2 (a496) (a553)) % 1.07/1.25 (zenon_X85 != (a553)) % 1.07/1.25 ((a570) != zenon_X12) % 1.07/1.25 (c3_2 zenon_X27 (a480)) % 1.07/1.25 (-. (c2_2 (a601) zenon_X162)) % 1.07/1.25 (c2_2 (a508) (a548)) % 1.07/1.25 (ndr1_1 (a471)) % 1.07/1.25 ((a487) != zenon_X107) % 1.07/1.25 (zenon_X30 != (a533)) % 1.07/1.25 (c3_1 (a573)) % 1.07/1.25 (-. (c4_2 zenon_X33 (a545))) % 1.07/1.25 (c4_2 (a534) (a535)) % 1.07/1.25 (zenon_X20 != (a545)) % 1.07/1.25 (-. (c4_2 zenon_X17 zenon_X97)) % 1.07/1.25 (-. (c1_2 (a538) (a578))) % 1.07/1.25 ((a535) != zenon_X55) % 1.07/1.25 (-. (c6_1 (a494))) % 1.07/1.25 (-. (c4_2 (a520) zenon_X16)) % 1.07/1.25 (-. (c8_1 (a520))) % 1.07/1.25 ((a494) != (a577)) % 1.07/1.25 (-. (c4_2 zenon_X17 (a535))) % 1.07/1.25 ((a508) != (a498)) % 1.07/1.25 (-. (c4_1 (a468))) % 1.07/1.25 ((a468) != (a538)) % 1.07/1.25 ((a508) != zenon_X26) % 1.07/1.25 (c3_2 (a544) (a495)) % 1.07/1.25 (-. (c6_1 (a508))) % 1.07/1.25 (zenon_X123 != zenon_X54) % 1.07/1.25 (-. (c6_1 (a601))) % 1.07/1.25 ((a480) != zenon_X54) % 1.07/1.25 (ndr1_1 (a577)) % 1.07/1.25 (zenon_X29 != (a566)) % 1.07/1.25 (c8_1 (a533)) % 1.07/1.25 (-. (c4_2 zenon_X26 (a487))) % 1.07/1.25 (-. (c4_2 zenon_X19 zenon_X14)) % 1.07/1.25 (zenon_X27 != (a534)) % 1.07/1.25 (-. (c3_1 (a577))) % 1.07/1.25 (-. (c8_1 zenon_X11)) % 1.07/1.25 ((a573) != zenon_X17) % 1.07/1.25 ((a460) != zenon_X53) % 1.07/1.25 (-. (c2_2 (a573) (a460))) % 1.07/1.25 (-. (c2_1 zenon_X0)) % 1.07/1.25 (c4_2 (a544) zenon_X73) % 1.07/1.25 (c5_2 zenon_X9 (a487)) % 1.07/1.25 ((a533) != (a508)) % 1.07/1.25 (zenon_X9 != zenon_X21) % 1.07/1.25 (c2_2 zenon_X27 (a548)) % 1.07/1.25 (zenon_X0 != zenon_X29) % 1.07/1.25 (zenon_X24 != (a468)) % 1.07/1.25 ((a573) != zenon_X27) % 1.07/1.25 ((a533) != (a534)) % 1.07/1.25 (c3_2 (a520) (a521)) % 1.07/1.25 (-. (c4_2 zenon_X33 zenon_X14)) % 1.07/1.25 ((a601) != (a520)) % 1.07/1.25 (zenon_X30 != (a482)) % 1.07/1.25 ((a578) != (a521)) % 1.07/1.25 ((a499) != (a553)) % 1.07/1.25 ((a535) != zenon_X62) % 1.07/1.25 (-. (c8_1 zenon_X13)) % 1.07/1.25 ((a570) != (a534)) % 1.07/1.25 (-. (c1_1 zenon_X17)) % 1.07/1.25 (zenon_X12 != zenon_X33) % 1.07/1.25 (-. (c2_2 zenon_X27 (a553))) % 1.07/1.25 (-. (c2_2 zenon_X30 (a548))) % 1.07/1.25 ((a578) != (a467)) % 1.07/1.25 (c3_2 zenon_X26 zenon_X89) % 1.07/1.25 ((a468) != (a592)) % 1.07/1.25 ((a467) != zenon_X10) % 1.07/1.25 (-. (c4_2 (a463) zenon_X54)) % 1.07/1.25 ((a534) != (a498)) % 1.07/1.25 ((a480) != zenon_X113) % 1.07/1.25 (zenon_X29 != zenon_X27) % 1.07/1.25 (-. (c3_1 zenon_X11)) % 1.07/1.25 ((a566) != (a544)) % 1.07/1.25 (c3_2 (a468) (a467)) % 1.07/1.25 (zenon_X73 != zenon_X54) % 1.07/1.25 (-. (c3_2 zenon_X13 zenon_X175)) % 1.07/1.25 ((a483) != (a553)) % 1.07/1.25 (-. (c4_2 zenon_X24 (a460))) % 1.07/1.25 ((a487) != zenon_X73) % 1.07/1.25 ((a535) != zenon_X52) % 1.07/1.25 ((a548) != zenon_X152) % 1.07/1.25 (c6_1 (a468)) % 1.07/1.25 (zenon_X21 != (a494)) % 1.07/1.25 (-. (c1_2 (a592) zenon_X116)) % 1.07/1.25 (-. (c4_2 (a534) (a500))) % 1.07/1.25 (-. (c7_2 zenon_X33 (a472))) % 1.07/1.25 ((a533) != (a494)) % 1.07/1.25 (-. (c3_2 (a508) (a553))) % 1.07/1.25 ((a601) != (a471)) % 1.07/1.25 (zenon_X29 != (a508)) % 1.07/1.25 (zenon_X90 != (a500)) % 1.07/1.25 ((a487) != zenon_X8) % 1.07/1.25 (zenon_X97 != zenon_X54) % 1.07/1.25 ((a487) != zenon_X54) % 1.07/1.25 ((a480) != zenon_X20) % 1.07/1.25 (-. (c2_2 (a570) (a460))) % 1.07/1.25 ((a553) != (a484)) % 1.07/1.25 (c5_2 (a573) (a460)) % 1.07/1.25 (-. (c4_2 (a570) zenon_X156)) % 1.07/1.25 ((a487) != zenon_X113) % 1.07/1.25 (-. (c4_2 zenon_X24 zenon_X16)) % 1.07/1.25 (-. (c2_1 zenon_X30)) % 1.07/1.25 (-. (c1_2 (a538) (a548))) % 1.07/1.25 ((a578) != (a480)) % 1.07/1.25 (-. (c7_2 zenon_X33 zenon_X34)) % 1.07/1.25 ((a472) != zenon_X60) % 1.07/1.25 (c5_2 (a544) zenon_X97) % 1.07/1.25 (-. (c4_2 (a533) (a548))) % 1.07/1.25 (c6_2 (a498) (a460)) % 1.07/1.25 ((a487) != zenon_X170) % 1.07/1.25 ((a500) != zenon_X4) % 1.07/1.25 ((a578) != (a535)) % 1.07/1.25 ((a545) != (a567)) % 1.07/1.25 (-. (c7_2 (a498) (a500))) % 1.07/1.25 (zenon_X24 != (a592)) % 1.07/1.25 (-. (c4_2 (a520) (a535))) % 1.07/1.25 ((a538) != zenon_X13) % 1.07/1.25 ((a592) != zenon_X33) % 1.07/1.25 (-. (c8_2 (a498) zenon_X63)) % 1.07/1.25 (c6_2 (a577) (a460)) % 1.07/1.25 (zenon_X12 != zenon_X13) % 1.07/1.25 (c8_1 (a508)) % 1.07/1.25 ((a521) != (a548)) % 1.07/1.25 (c1_1 (a533)) % 1.07/1.25 (c5_1 (a570)) % 1.07/1.25 (c4_2 (a544) zenon_X14) % 1.07/1.25 ((a460) != zenon_X18) % 1.07/1.25 (c3_2 (a471) zenon_X44) % 1.07/1.25 ((a487) != zenon_X90) % 1.07/1.25 (-. (c7_2 (a573) (a472))) % 1.07/1.25 (-. (c2_2 (a544) (a548))) % 1.07/1.25 (zenon_X73 != (a460)) % 1.07/1.25 ((a571) != (a521)) % 1.07/1.25 ((a570) != (a463)) % 1.07/1.25 ((a578) != (a484)) % 1.07/1.25 (-. (c4_2 zenon_X33 (a535))) % 1.07/1.25 (-. (c4_2 zenon_X19 (a548))) % 1.07/1.25 (c3_2 (a482) (a483)) % 1.07/1.25 (c7_1 zenon_X5) % 1.07/1.25 ((a570) != zenon_X24) % 1.07/1.25 ((a601) != zenon_X11) % 1.07/1.25 ((a483) != (a521)) % 1.07/1.25 ((a534) != zenon_X9) % 1.07/1.25 ((a538) != (a601)) % 1.07/1.25 (zenon_X9 != zenon_X13) % 1.07/1.25 (c5_1 (a533)) % 1.07/1.25 ((a500) != (a548)) % 1.07/1.25 (c2_2 (a566) (a548)) % 1.07/1.25 ((a508) != zenon_X11) % 1.07/1.25 ((a548) != zenon_X129) % 1.07/1.25 (-. (c4_2 zenon_X17 (a500))) % 1.07/1.25 ((a548) != (a467)) % 1.07/1.25 (zenon_X12 != (a601)) % 1.07/1.25 (-. (c3_1 (a494))) % 1.07/1.25 (-. (c1_1 (a534))) % 1.07/1.25 ((a545) != (a487)) % 1.07/1.25 ((a487) != zenon_X150) % 1.07/1.25 ((a500) != (a567)) % 1.07/1.25 ((a467) != (a553)) % 1.07/1.25 (-. (c2_2 zenon_X9 (a460))) % 1.07/1.25 (zenon_X21 != (a566)) % 1.07/1.25 (zenon_X30 != zenon_X27) % 1.07/1.25 ((a508) != zenon_X9) % 1.07/1.25 ((a534) != zenon_X26) % 1.07/1.25 ((a468) != (a544)) % 1.07/1.25 (c2_2 (a482) (a460)) % 1.07/1.25 (-. (c5_1 zenon_X24)) % 1.07/1.25 ((a535) != zenon_X146) % 1.07/1.25 (-. (c2_2 zenon_X9 (a553))) % 1.07/1.25 ((a548) != zenon_X16) % 1.07/1.25 (zenon_X19 != (a520)) % 1.07/1.25 (zenon_X135 != zenon_X153) % 1.07/1.25 ((a535) != zenon_X66) % 1.07/1.25 (-. (c2_2 zenon_X9 (a548))) % 1.07/1.25 (zenon_X12 != zenon_X21) % 1.07/1.25 ((a573) != zenon_X33) % 1.07/1.25 (c3_1 zenon_X13) % 1.07/1.25 (c4_2 zenon_X27 (a480)) % 1.07/1.25 (ndr1_1 (a538)) % 1.07/1.25 (c4_1 (a494)) % 1.07/1.25 (zenon_X13 != zenon_X21) % 1.07/1.25 (zenon_X9 != (a463)) % 1.07/1.25 (c1_2 (a544) (a500)) % 1.07/1.25 (-. (c2_2 (a482) (a571))) % 1.07/1.25 ((a500) != zenon_X64) % 1.07/1.25 (-. (c7_2 zenon_X24 zenon_X109)) % 1.07/1.25 (zenon_X97 != zenon_X16) % 1.07/1.25 ((a468) != zenon_X3) % 1.07/1.25 ((a592) != zenon_X9) % 1.07/1.25 (-. (c4_2 zenon_X33 (a500))) % 1.07/1.25 (-. (c2_2 zenon_X13 (a553))) % 1.07/1.25 (-. (c2_2 (a496) (a460))) % 1.07/1.25 ((a483) != (a571)) % 1.07/1.25 (zenon_X27 != (a494)) % 1.07/1.25 (-. (c2_2 (a577) (a548))) % 1.07/1.25 (-. (c7_2 (a471) (a460))) % 1.07/1.25 ((a480) != (a487)) % 1.07/1.25 ((a467) != zenon_X128) % 1.07/1.25 ((a482) != zenon_X29) % 1.07/1.25 (zenon_X29 != zenon_X11) % 1.07/1.25 (-. (c6_1 (a482))) % 1.07/1.25 ((a468) != zenon_X0) % 1.07/1.25 (c8_1 (a573)) % 1.07/1.25 ((a601) != (a534)) % 1.07/1.25 (-. (c4_2 (a538) zenon_X113)) % 1.07/1.25 (-. (c3_2 (a482) (a553))) % 1.07/1.25 ((a592) != (a534)) % 1.07/1.25 ((a570) != (a538)) % 1.07/1.25 ((a573) != (a538)) % 1.07/1.25 (c8_1 (a601)) % 1.07/1.25 (-. (c4_2 (a601) (a487))) % 1.07/1.25 ((a497) != (a484)) % 1.07/1.25 ((a460) != zenon_X67) % 1.07/1.25 ((a487) != zenon_X2) % 1.07/1.25 (zenon_X11 != (a538)) % 1.07/1.25 (zenon_X30 != zenon_X26) % 1.07/1.25 (zenon_X0 != (a544)) % 1.07/1.25 (-. (c2_2 (a534) zenon_X65)) % 1.07/1.25 ((a460) != zenon_X116) % 1.07/1.25 ((a483) != zenon_X55) % 1.07/1.25 (-. (c5_0)) % 1.07/1.25 ((a468) != zenon_X21) % 1.07/1.25 ((a538) != zenon_X0) % 1.07/1.25 ((a467) != zenon_X108) % 1.07/1.25 (zenon_X54 != zenon_X16) % 1.07/1.25 ((a500) != zenon_X20) % 1.07/1.25 (-. (c4_2 (a534) (a545))) % 1.07/1.25 (c7_2 zenon_X21 (a553)) % 1.07/1.25 ((a570) != zenon_X27) % 1.07/1.25 (zenon_X12 != (a468)) % 1.07/1.25 ((a535) != zenon_X57) % 1.07/1.25 ((a535) != zenon_X16) % 1.07/1.25 (-. (c2_2 (a566) zenon_X47)) % 1.07/1.25 (-. (c4_2 zenon_X24 zenon_X14)) % 1.07/1.25 (-. (c4_2 (a498) zenon_X16)) % 1.07/1.25 (zenon_X13 != zenon_X11) % 1.07/1.25 (-. (c4_2 (a498) (a535))) % 1.07/1.25 ((a538) != (a482)) % 1.07/1.25 ((a482) != zenon_X13) % 1.07/1.25 ((a544) != zenon_X24) % 1.07/1.25 (-. (c2_2 (a498) (a548))) % 1.07/1.25 (c5_2 (a573) (a571)) % 1.07/1.25 (-. (c6_1 zenon_X0)) % 1.07/1.25 (c1_2 (a570) (a571)) % 1.07/1.25 ((a487) != zenon_X155) % 1.07/1.25 (-. (c7_2 zenon_X0 zenon_X166)) % 1.07/1.25 (zenon_X92 != zenon_X54) % 1.07/1.25 (-. (c7_0)) % 1.07/1.25 ((a601) != (a468)) % 1.07/1.25 (-. (c6_2 (a577) (a579))) % 1.07/1.25 ((a592) != (a538)) % 1.07/1.25 (ndr1_1 (a498)) % 1.07/1.25 (zenon_X27 != zenon_X33) % 1.07/1.25 ((a544) != (a508)) % 1.07/1.25 ((a570) != zenon_X30) % 1.07/1.25 (-. (c8_1 zenon_X33)) % 1.07/1.25 ((a500) != (a484)) % 1.07/1.25 ((a496) != zenon_X24) % 1.07/1.25 ((a483) != (a499)) % 1.07/1.25 (zenon_X121 != (a553)) % 1.07/1.25 ((a533) != (a520)) % 1.07/1.25 ((a468) != (a498)) % 1.07/1.25 (zenon_X13 != (a471)) % 1.07/1.25 ((a482) != (a468)) % 1.07/1.25 ((a535) != (a499)) % 1.07/1.25 (zenon_X19 != zenon_X30) % 1.07/1.25 (-. (c4_2 zenon_X24 (a535))) % 1.07/1.25 ((a495) != zenon_X63) % 1.07/1.25 (-. (c2_1 (a538))) % 1.07/1.25 (zenon_X160 != (a495)) % 1.07/1.25 (c1_2 zenon_X13 zenon_X111) % 1.07/1.25 ((a500) != zenon_X66) % 1.07/1.25 (-. (c2_2 (a494) (a535))) % 1.07/1.25 ((a460) != zenon_X153) % 1.07/1.25 (-. (c2_2 (a482) (a553))) % 1.07/1.25 ((a535) != zenon_X97) % 1.07/1.25 ((a508) != (a566)) % 1.07/1.25 (-. (c7_2 (a544) (a545))) % 1.07/1.25 (-. (c4_2 (a463) zenon_X14)) % 1.07/1.25 (-. (c2_1 (a520))) % 1.07/1.25 (c5_2 (a482) (a487)) % 1.07/1.25 ((a468) != zenon_X13) % 1.07/1.25 (c5_2 zenon_X27 (a480)) % 1.07/1.25 (-. (c2_2 (a570) zenon_X67)) % 1.07/1.25 (-. (c8_2 (a534) (a500))) % 1.07/1.25 ((a460) != (a484)) % 1.07/1.25 (-. (c8_2 (a482) zenon_X66)) % 1.07/1.25 (c3_2 (a566) (a548)) % 1.07/1.25 (c1_2 (a544) zenon_X54) % 1.07/1.25 (-. (c1_1 zenon_X30)) % 1.07/1.25 (-. (c5_2 (a592) zenon_X36)) % 1.07/1.25 (zenon_X38 != (a495)) % 1.07/1.25 ((a484) != zenon_X16) % 1.07/1.25 (zenon_X27 != (a533)) % 1.07/1.25 (c7_1 (a463)) % 1.07/1.25 ((a553) != zenon_X101) % 1.07/1.25 (-. (c7_2 (a533) zenon_X105)) % 1.07/1.25 ((a499) != zenon_X34) % 1.07/1.25 (-. (c6_1 zenon_X29)) % 1.07/1.25 (c4_2 (a544) (a521)) % 1.07/1.25 ((a484) != (a545)) % 1.07/1.25 (zenon_X26 != (a494)) % 1.07/1.25 (-. (c2_2 (a520) (a467))) % 1.07/1.25 (zenon_X40 != (a553)) % 1.07/1.25 (-. (c2_2 (a482) (a548))) % 1.07/1.25 (zenon_X0 != zenon_X13) % 1.07/1.25 ((a570) != (a468)) % 1.07/1.25 ((a508) != (a496)) % 1.07/1.25 (c3_2 (a468) (a553)) % 1.07/1.25 (-. (c1_1 (a577))) % 1.07/1.25 (-. (c1_1 zenon_X33)) % 1.07/1.25 (c6_2 zenon_X3 (a460)) % 1.07/1.25 ((a548) != zenon_X130) % 1.07/1.25 (-. (c4_2 zenon_X0 zenon_X173)) % 1.07/1.25 (zenon_X133 != (a553)) % 1.07/1.25 ((a533) != (a482)) % 1.07/1.25 (-. (c4_2 zenon_X19 (a487))) % 1.07/1.25 (-. (c2_2 (a498) zenon_X125)) % 1.07/1.25 (zenon_X24 != zenon_X0) % 1.07/1.25 ((a571) != zenon_X8) % 1.07/1.25 (c3_2 zenon_X19 (a553)) % 1.07/1.25 (-. (c2_2 (a538) (a483))) % 1.07/1.25 ((a538) != zenon_X26) % 1.07/1.25 (-. (c4_2 (a520) (a545))) % 1.07/1.25 (c3_2 zenon_X0 zenon_X164) % 1.07/1.25 (c1_2 (a577) (a578)) % 1.07/1.25 (ndr1_1 (a508)) % 1.07/1.25 (c3_2 (a538) (a553)) % 1.07/1.25 ((a484) != zenon_X2) % 1.07/1.25 (-. (c2_2 (a566) (a467))) % 1.07/1.25 (-. (c1_0)) % 1.07/1.25 (-. (c5_1 zenon_X0)) % 1.07/1.25 ((a499) != zenon_X18) % 1.07/1.25 (-. (c4_2 (a508) (a535))) % 1.07/1.25 ((a480) != zenon_X14) % 1.07/1.25 (zenon_X29 != (a533)) % 1.07/1.25 (-. (c2_2 (a534) (a548))) % 1.07/1.25 (zenon_X36 != zenon_X2) % 1.07/1.25 (zenon_X90 != (a460)) % 1.07/1.25 (-. (c7_2 (a508) zenon_X79)) % 1.07/1.25 (-. (c2_2 (a482) (a535))) % 1.07/1.25 ((a487) != zenon_X92) % 1.07/1.25 (zenon_X30 != zenon_X13) % 1.07/1.25 (c8_0) % 1.07/1.25 ((a508) != zenon_X13) % 1.07/1.25 ((a535) != (a545)) % 1.07/1.25 ((a495) != (a499)) % 1.07/1.25 (c3_2 zenon_X21 (a495)) % 1.07/1.25 ((a460) != zenon_X63) % 1.07/1.25 ((a494) != (a573)) % 1.07/1.25 ((a483) != zenon_X47) % 1.07/1.25 (-. (c8_2 (a577) (a467))) % 1.07/1.25 (-. (c1_2 (a538) zenon_X48)) % 1.07/1.25 (zenon_X113 != (a545)) % 1.07/1.25 ((a472) != zenon_X34) % 1.07/1.25 (c3_2 (a538) (a548)) % 1.07/1.25 (zenon_X36 != (a472)) % 1.07/1.25 ((a497) != (a495)) % 1.07/1.25 (-. (c1_2 (a538) (a521))) % 1.07/1.25 (-. (c4_2 zenon_X29 zenon_X174)) % 1.07/1.25 (c5_2 (a573) (a548)) % 1.07/1.25 (-. (c4_2 zenon_X33 zenon_X16)) % 1.07/1.25 ((a499) != (a472)) % 1.07/1.25 ((a548) != zenon_X23) % 1.07/1.25 ((a570) != (a566)) % 1.07/1.25 (c3_2 (a570) (a571)) % 1.07/1.25 ((a553) != zenon_X56) % 1.07/1.25 (zenon_X20 != zenon_X73) % 1.07/1.25 (zenon_X27 != (a508)) % 1.07/1.25 ((a460) != (a567)) % 1.07/1.25 (zenon_X38 != (a545)) % 1.07/1.25 (-. (c1_2 (a538) zenon_X92)) % 1.07/1.25 (-. (c4_2 (a463) (a487))) % 1.07/1.25 (-. (c4_2 (a570) (a548))) % 1.07/1.25 (-. (c7_2 (a544) (a460))) % 1.07/1.25 (-. (c2_2 (a538) (a467))) % 1.07/1.25 ((a494) != (a463)) % 1.07/1.25 (-. (c6_2 (a533) (a480))) % 1.07/1.25 (c7_2 zenon_X26 (a553)) % 1.07/1.25 ((a601) != (a533)) % 1.07/1.25 (-. (c5_1 zenon_X30)) % 1.07/1.25 (-. (c3_2 zenon_X21 (a553))) % 1.07/1.25 (zenon_X27 != (a498)) % 1.07/1.25 (-. (c7_2 (a538) zenon_X53)) % 1.07/1.25 (ndr1_1 (a601)) % 1.07/1.25 ((a544) != zenon_X13) % 1.07/1.25 (zenon_X12 != (a463)) % 1.07/1.25 (c1_2 (a544) zenon_X16) % 1.07/1.25 (-. (c2_2 zenon_X21 (a535))) % 1.07/1.25 (-. (c8_2 zenon_X3 (a467))) % 1.07/1.25 (-. (c7_2 (a573) (a548))) % 1.07/1.25 ((a534) != zenon_X17) % 1.07/1.25 ((a535) != (a472)) % 1.07/1.25 (-. (c7_2 zenon_X17 zenon_X18)) % 1.07/1.25 (-. (c4_1 zenon_X22)) % 1.07/1.25 ((a487) != zenon_X48) % 1.07/1.25 (zenon_X0 != zenon_X33) % 1.07/1.25 (-. (c4_2 (a534) (a487))) % 1.07/1.25 (c3_2 zenon_X29 zenon_X135) % 1.07/1.25 (c8_1 (a534)) % 1.07/1.25 (-. (c3_1 zenon_X27)) % 1.07/1.25 ((a520) != zenon_X9) % 1.07/1.25 (zenon_X14 != zenon_X48) % 1.07/1.25 (ndr1_1 zenon_X21) % 1.07/1.25 (-. (c4_2 (a494) (a548))) % 1.07/1.25 ((a494) != (a471)) % 1.07/1.25 (c5_1 (a577)) % 1.07/1.25 (-. (c7_2 zenon_X17 (a499))) % 1.07/1.25 ((a467) != zenon_X4) % 1.07/1.25 (zenon_X9 != (a471)) % 1.07/1.25 (-. (c4_2 (a544) zenon_X16)) % 1.07/1.25 ((a566) != zenon_X17) % 1.07/1.25 (c5_2 (a544) zenon_X113) % 1.07/1.25 (-. (c4_2 (a544) (a500))) % 1.07/1.25 (ndr1_1 (a496)) % 1.07/1.25 (c3_2 (a468) zenon_X85) % 1.07/1.25 ((a548) != (a545)) % 1.07/1.25 (c5_2 (a570) (a500)) % 1.07/1.25 (c6_2 (a534) (a460)) % 1.07/1.25 (zenon_X9 != zenon_X33) % 1.07/1.25 (zenon_X30 != (a601)) % 1.07/1.25 ((a496) != zenon_X33) % 1.07/1.25 ((a508) != zenon_X33) % 1.07/1.25 ((a544) != zenon_X19) % 1.07/1.25 (zenon_X29 != (a520)) % 1.07/1.25 ((a495) != (a484)) % 1.07/1.25 (-. (c2_2 (a533) (a483))) % 1.07/1.25 ((a548) != zenon_X49) % 1.07/1.25 ((a494) != zenon_X17) % 1.07/1.25 ((a566) != zenon_X33) % 1.07/1.25 (-. (c8_2 (a534) (a578))) % 1.07/1.25 (-. (c4_2 (a471) (a487))) % 1.07/1.25 (-. (c4_2 (a538) zenon_X97)) % 1.07/1.25 (-. (c8_2 (a566) (a567))) % 1.07/1.25 ((a495) != zenon_X62) % 1.07/1.25 (-. (c5_2 (a592) zenon_X2)) % 1.07/1.25 (-. (c2_1 (a494))) % 1.07/1.25 (zenon_X12 != (a498)) % 1.07/1.25 (-. (c4_2 (a471) (a535))) % 1.07/1.25 (c2_1 (a482)) % 1.07/1.25 ((a567) != (a480)) % 1.07/1.25 ((a573) != (a471)) % 1.07/1.25 (zenon_X131 != (a553)) % 1.07/1.25 (zenon_X29 != zenon_X30) % 1.07/1.25 (zenon_X92 != zenon_X16) % 1.07/1.25 (-. (c4_1 zenon_X7)) % 1.07/1.25 (-. (c6_1 (a573))) % 1.07/1.25 ((a460) != (a467)) % 1.07/1.25 (-. (c4_2 zenon_X33 (a480))) % 1.07/1.25 (-. (c8_1 zenon_X19)) % 1.07/1.25 ((a578) != zenon_X4) % 1.07/1.25 (-. (c2_1 (a573))) % 1.07/1.25 (-. (c2_2 (a570) (a553))) % 1.07/1.25 (-. (c1_2 (a538) (a500))) % 1.07/1.25 (-. (c7_2 (a482) zenon_X118)) % 1.07/1.25 (c5_2 (a544) zenon_X90) % 1.07/1.25 ((a460) != zenon_X54) % 1.07/1.25 (c7_2 zenon_X12 (a553)) % 1.07/1.25 (-. (c8_2 zenon_X3 (a495))) % 1.07/1.25 ((a483) != zenon_X49) % 1.07/1.25 (-. (c8_1 zenon_X24)) % 1.07/1.25 (-. (c2_2 (a496) (a571))) % 1.07/1.25 ((a592) != (a533)) % 1.07/1.25 ((a521) != (a495)) % 1.07/1.25 ((a467) != zenon_X63) % 1.07/1.25 ((a460) != zenon_X15) % 1.07/1.25 (-. (c4_2 (a538) (a460))) % 1.07/1.25 (c2_2 (a538) (a548)) % 1.07/1.25 (-. (c7_2 (a577) (a553))) % 1.07/1.25 (zenon_X0 != zenon_X12) % 1.07/1.25 (c6_2 (a508) (a553)) % 1.07/1.25 (zenon_X9 != (a577)) % 1.07/1.25 ((a544) != zenon_X17) % 1.07/1.25 (c5_2 zenon_X27 (a487)) % 1.07/1.25 ((a544) != (a463)) % 1.07/1.25 (-. (c1_1 (a592))) % 1.07/1.25 (-. (c4_2 (a573) (a548))) % 1.07/1.25 (-. (c7_2 (a544) zenon_X99)) % 1.07/1.25 ((a460) != zenon_X51) % 1.07/1.25 (-. (c4_2 zenon_X17 zenon_X113)) % 1.07/1.25 ((a460) != (a579)) % 1.07/1.25 (-. (c8_2 (a494) (a578))) % 1.07/1.25 (-. (c2_1 zenon_X11)) % 1.07/1.25 (zenon_X0 != (a601)) % 1.07/1.25 ((a553) != zenon_X60) % 1.07/1.25 (-. (c8_1 (a577))) % 1.07/1.25 ((a468) != zenon_X9) % 1.07/1.25 (c5_2 (a544) (a487)) % 1.07/1.25 (zenon_X14 != (a521)) % 1.07/1.25 ((a545) != zenon_X1) % 1.07/1.25 (zenon_X123 != (a460)) % 1.07/1.25 (zenon_X14 != zenon_X73) % 1.07/1.25 (-. (c2_2 zenon_X26 (a553))) % 1.07/1.25 (zenon_X21 != zenon_X11) % 1.07/1.25 (c6_2 (a496) (a497)) % 1.07/1.25 ((a520) != zenon_X13) % 1.07/1.25 (-. (c7_2 (a533) (a548))) % 1.07/1.25 ((a553) != zenon_X118) % 1.07/1.25 ((a570) != zenon_X33) % 1.07/1.25 (-. (c5_1 (a573))) % 1.07/1.25 (-. (c1_2 (a538) (a484))) % 1.07/1.25 ((a535) != zenon_X10) % 1.07/1.25 ((a498) != (a577)) % 1.07/1.25 (c4_2 (a544) zenon_X90) % 1.07/1.25 ((a570) != zenon_X9) % 1.07/1.25 (c7_2 zenon_X13 (a553)) % 1.07/1.25 (-. (c8_2 (a482) (a500))) % 1.07/1.25 ((a487) != zenon_X16) % 1.07/1.25 (zenon_X11 != zenon_X24) % 1.07/1.25 (-. (c4_2 zenon_X0 (a487))) % 1.07/1.25 ((a521) != zenon_X65) % 1.07/1.25 ((a570) != (a577)) % 1.07/1.25 ((a566) != zenon_X13) % 1.07/1.25 ((a472) != zenon_X95) % 1.07/1.25 (c1_2 (a544) (a460)) % 1.07/1.25 (c3_2 zenon_X30 (a545)) % 1.07/1.25 (zenon_X12 != (a494)) % 1.07/1.25 (-. (c3_2 zenon_X12 (a553))) % 1.07/1.25 (c3_2 (a482) (a460)) % 1.07/1.25 ((a544) != (a520)) % 1.07/1.25 ((a460) != zenon_X6) % 1.07/1.25 ((a521) != zenon_X50) % 1.07/1.25 (-. (c2_2 (a496) (a535))) % 1.07/1.25 ((a533) != (a577)) % 1.07/1.25 ((a592) != zenon_X30) % 1.07/1.25 ((a487) != zenon_X96) % 1.07/1.25 (-. (c3_1 zenon_X19)) % 1.07/1.25 (-. (c4_2 zenon_X19 zenon_X54)) % 1.07/1.25 ((a471) != zenon_X27) % 1.07/1.25 (c5_2 (a533) (a480)) % 1.07/1.25 (-. (c4_2 zenon_X24 zenon_X73)) % 1.07/1.25 (c5_1 zenon_X13) % 1.07/1.25 ((a578) != zenon_X62) % 1.07/1.25 (zenon_X11 != (a471)) % 1.07/1.25 ((a483) != zenon_X63) % 1.07/1.25 (-. (c1_1 (a496))) % 1.07/1.25 (c5_1 zenon_X12) % 1.07/1.25 ((a482) != zenon_X17) % 1.07/1.25 ((a471) != (a520)) % 1.07/1.25 (c7_1 (a601)) % 1.07/1.25 (-. (c4_2 (a538) zenon_X20)) % 1.07/1.25 ((a496) != zenon_X11) % 1.07/1.25 ((a573) != (a601)) % 1.07/1.25 (-. (c4_2 (a498) (a460))) % 1.07/1.25 (ndr1_1 (a482)) % 1.07/1.25 (c4_2 (a498) (a500)) % 1.07/1.25 ((a553) != zenon_X61) % 1.07/1.25 (zenon_X27 != (a577)) % 1.07/1.25 (c6_2 (a471) (a535)) % 1.07/1.25 (c3_2 (a533) (a480)) % 1.07/1.25 (c1_2 zenon_X29 zenon_X153) % 1.07/1.25 ((a500) != zenon_X25) % 1.07/1.25 (-. (c4_2 (a538) zenon_X16)) % 1.07/1.25 (-. (c3_1 (a533))) % 1.07/1.25 ((a472) != (a548)) % 1.07/1.25 ((a553) != zenon_X80) % 1.07/1.25 ((a553) != zenon_X134) % 1.07/1.25 (-. (c2_2 (a494) zenon_X46)) % 1.07/1.25 ((a553) != zenon_X114) % 1.07/1.25 (c8_1 zenon_X9) % 1.07/1.25 (zenon_X12 != (a508)) % 1.07/1.25 (c1_1 zenon_X27) % 1.07/1.25 ((a495) != (a567)) % 1.07/1.25 ((a483) != zenon_X52) % 1.07/1.25 (zenon_X19 != (a538)) % 1.07/1.25 (-. (c4_2 zenon_X19 zenon_X97)) % 1.07/1.25 ((a578) != zenon_X64) % 1.07/1.25 ((a468) != zenon_X19) % 1.07/1.25 ((a487) != (a521)) % 1.07/1.25 (c8_2 (a534) (a535)) % 1.07/1.25 (zenon_X30 != (a508)) % 1.07/1.25 (-. (c2_2 (a496) (a521))) % 1.07/1.25 (c2_2 (a570) (a571)) % 1.07/1.25 (-. (c2_2 zenon_X9 (a467))) % 1.07/1.25 (c2_2 (a494) (a548)) % 1.07/1.25 (zenon_X14 != (a487)) % 1.07/1.25 (-. (c4_2 zenon_X19 zenon_X16)) % 1.07/1.25 (zenon_X11 != (a463)) % 1.07/1.25 (-. (c3_2 (a533) (a553))) % 1.07/1.25 ((a553) != (a495)) % 1.07/1.25 ((a548) != zenon_X46) % 1.07/1.25 (-. (c1_2 (a566) zenon_X8)) % 1.07/1.25 (c6_2 (a577) (a578)) % 1.07/1.25 (c2_2 (a534) (a535)) % 1.07/1.25 (zenon_X13 != (a496)) % 1.07/1.25 ((a498) != (a463)) % 1.07/1.25 ((a534) != (a471)) % 1.07/1.25 ((a570) != zenon_X13) % 1.07/1.25 ((a500) != (a499)) % 1.07/1.25 (-. (c7_2 zenon_X29 zenon_X140)) % 1.07/1.25 (-. (c2_2 (a573) zenon_X49)) % 1.07/1.25 ((a553) != zenon_X83) % 1.07/1.25 (zenon_X21 != (a577)) % 1.07/1.25 (c8_1 (a482)) % 1.07/1.25 (-. (c7_2 (a498) (a460))) % 1.07/1.25 ((a535) != zenon_X50) % 1.07/1.25 ((a483) != zenon_X62) % 1.07/1.25 ((a577) != zenon_X33) % 1.07/1.25 (zenon_X11 != zenon_X0) % 1.07/1.25 ((a460) != zenon_X57) % 1.07/1.25 (zenon_X19 != (a494)) % 1.07/1.25 (ndr1_1 zenon_X12) % 1.07/1.25 (-. (c5_2 (a592) (a500))) % 1.07/1.25 ((a535) != (a521)) % 1.07/1.25 ((a460) != zenon_X55) % 1.07/1.25 ((a494) != (a566)) % 1.07/1.25 ((a534) != zenon_X33) % 1.07/1.25 (-. (c4_2 (a498) zenon_X14)) % 1.07/1.25 (-. (c7_2 (a494) (a548))) % 1.07/1.25 (c8_1 (a538)) % 1.07/1.25 (-. (c2_2 (a468) (a521))) % 1.07/1.25 (zenon_X14 != (a535)) % 1.07/1.25 (c4_2 (a544) zenon_X113) % 1.07/1.25 ((a544) != (a496)) % 1.07/1.25 (c1_2 (a601) (a487)) % 1.07/1.25 (-. (c8_2 zenon_X3 (a500))) % 1.07/1.25 (c5_2 (a494) (a472)) % 1.07/1.25 (zenon_X48 != zenon_X16) % 1.07/1.25 (-. (c1_2 (a538) zenon_X73)) % 1.07/1.25 (-. (c4_2 zenon_X17 (a487))) % 1.07/1.25 ((a500) != zenon_X54) % 1.07/1.25 (-. (c4_2 zenon_X17 zenon_X54)) % 1.07/1.25 ((a521) != zenon_X23) % 1.07/1.25 (c3_2 zenon_X11 zenon_X74) % 1.07/1.25 ((a535) != zenon_X90) % 1.07/1.25 (c2_2 (a570) (a548)) % 1.07/1.25 (-. (c2_1 (a468))) % 1.07/1.25 (-. (c2_2 (a496) zenon_X23)) % 1.07/1.25 (-. (c7_2 (a538) zenon_X56)) % 1.07/1.25 ((a538) != (a508)) % 1.07/1.25 (zenon_X14 != (a545)) % 1.07/1.25 (-. (c7_2 zenon_X17 (a553))) % 1.07/1.25 ((a520) != zenon_X21) % 1.07/1.25 (-. (c4_2 zenon_X17 zenon_X14)) % 1.07/1.25 (c5_2 zenon_X29 (a460)) % 1.07/1.25 (c6_2 zenon_X12 (a553)) % 1.07/1.25 (zenon_X19 != zenon_X13) % 1.07/1.25 (zenon_X31 != (a553)) % 1.07/1.25 (c4_2 (a544) (a497)) % 1.07/1.25 (-. (c2_2 zenon_X9 zenon_X10)) % 1.07/1.25 (c3_2 zenon_X30 (a553)) % 1.07/1.25 ((a533) != zenon_X9) % 1.07/1.25 (-. (c4_2 zenon_X26 (a535))) % 1.07/1.25 (-. (c2_2 (a533) (a467))) % 1.07/1.25 ((a460) != zenon_X4) % 1.07/1.25 (-. (c1_2 (a566) (a578))) % 1.07/1.25 ((a483) != zenon_X4) % 1.07/1.25 ((a460) != (a545)) % 1.07/1.25 ((a538) != (a463)) % 1.07/1.25 ((a535) != zenon_X49) % 1.07/1.25 (-. (c4_2 zenon_X30 (a487))) % 1.07/1.25 (-. (c7_2 zenon_X33 (a553))) % 1.07/1.25 ((a467) != zenon_X47) % 1.07/1.25 (-. (c4_2 (a463) (a460))) % 1.07/1.25 (zenon_X27 != zenon_X17) % 1.07/1.25 (-. (c2_2 (a508) (a535))) % 1.07/1.25 (-. (c2_2 (a538) (a535))) % 1.07/1.25 (ndr1_1 (a494)) % 1.07/1.25 (c5_1 (a498)) % 1.07/1.25 (zenon_X29 != zenon_X24) % 1.07/1.25 (-. (c7_2 (a577) zenon_X82)) % 1.07/1.25 (zenon_X21 != (a573)) % 1.07/1.25 (zenon_X97 != (a545)) % 1.07/1.25 ((a567) != (a579)) % 1.07/1.25 ((a467) != zenon_X86) % 1.07/1.25 (-. (c3_2 zenon_X13 (a553))) % 1.07/1.25 (-. (c8_1 zenon_X17)) % 1.07/1.25 (c4_2 zenon_X24 (a487)) % 1.07/1.25 ((a601) != zenon_X33) % 1.07/1.25 (zenon_X97 != (a460)) % 1.07/1.25 ((a500) != (a535)) % 1.07/1.25 ((a577) != zenon_X3) % 1.07/1.25 ((a495) != (a545)) % 1.07/1.25 ((a500) != zenon_X62) % 1.07/1.25 (zenon_X20 != zenon_X16) % 1.07/1.25 ((a535) != zenon_X51) % 1.07/1.25 ((a460) != zenon_X108) % 1.07/1.25 (-. (c4_2 (a463) zenon_X90)) % 1.07/1.25 ((a535) != zenon_X149) % 1.07/1.25 (zenon_X97 != (a548)) % 1.07/1.25 (-. (c4_2 (a544) (a545))) % 1.07/1.25 ((a538) != (a496)) % 1.07/1.25 ((a468) != (a496)) % 1.07/1.25 (-. (c4_2 (a463) (a535))) % 1.07/1.25 ((a508) != (a463)) % 1.07/1.25 (-. (c4_2 zenon_X17 zenon_X16)) % 1.07/1.25 (-. (c6_1 (a471))) % 1.07/1.25 (zenon_X19 != (a573)) % 1.07/1.25 (c8_1 (a570)) % 1.07/1.25 (-. (c1_1 zenon_X13)) % 1.07/1.25 (zenon_X24 != (a573)) % 1.07/1.25 ((a487) != zenon_X151) % 1.07/1.25 (-. (c3_1 zenon_X26)) % 1.07/1.25 ((a467) != zenon_X127) % 1.07/1.25 ((a472) != zenon_X166) % 1.07/1.25 ((a480) != zenon_X16) % 1.07/1.25 (zenon_X14 != zenon_X123) % 1.07/1.25 (-. (c4_2 zenon_X13 zenon_X177)) % 1.07/1.25 (zenon_X21 != zenon_X24) % 1.07/1.25 (-. (c1_1 zenon_X29)) % 1.07/1.25 (c3_2 zenon_X27 zenon_X133) % 1.07/1.25 (-. (c6_1 (a533))) % 1.07/1.25 (zenon_X14 != zenon_X92) % 1.07/1.25 ((a460) != zenon_X61) % 1.07/1.25 (-. (c7_2 zenon_X11 (a499))) % 1.07/1.25 (zenon_X9 != (a601)) % 1.07/1.25 (-. (c5_1 (a538))) % 1.07/1.25 ((a544) != zenon_X26) % 1.07/1.25 (zenon_X12 != (a482)) % 1.07/1.25 (zenon_X48 != zenon_X54) % 1.07/1.25 ((a482) != (a471)) % 1.07/1.25 (zenon_X26 != zenon_X33) % 1.07/1.25 (zenon_X19 != (a463)) % 1.07/1.25 ((a468) != zenon_X29) % 1.07/1.25 (-. (c4_2 (a538) zenon_X54)) % 1.07/1.25 ((a571) != zenon_X52) % 1.07/1.25 (-. (c2_2 (a577) (a467))) % 1.07/1.25 (-. (c2_0)) % 1.07/1.25 (-. (c3_2 (a534) (a553))) % 1.07/1.25 ((a570) != (a573)) % 1.07/1.25 (c6_2 (a566) (a567)) % 1.07/1.25 (ndr1_1 (a534)) % 1.07/1.25 (-. (c4_2 zenon_X19 (a535))) % 1.07/1.25 ((a533) != (a468)) % 1.07/1.25 (c6_2 (a471) zenon_X28) % 1.07/1.25 ((a570) != (a508)) % 1.07/1.25 (-. (c1_1 (a463))) % 1.07/1.25 (zenon_X123 != (a500)) % 1.07/1.25 ((a497) != (a579)) % 1.07/1.25 (zenon_X0 != (a508)) % 1.07/1.25 ((a495) != zenon_X64) % 1.07/1.25 (-. (c8_2 (a494) zenon_X64)) % 1.07/1.25 (c4_2 (a544) (a487)) % 1.07/1.25 (zenon_X12 != (a573)) % 1.07/1.25 (c4_2 (a544) zenon_X97) % 1.07/1.25 (-. (c8_1 (a498))) % 1.07/1.25 ((a571) != zenon_X110) % 1.07/1.25 ((a500) != (a495)) % 1.07/1.25 (-. (c7_2 (a471) (a553))) % 1.07/1.25 (c5_2 (a573) (a483)) % 1.07/1.25 ((a480) != (a553)) % 1.07/1.25 (-. (c2_1 (a496))) % 1.07/1.25 ((a487) != zenon_X20) % 1.07/1.25 (c3_2 (a494) (a548)) % 1.07/1.25 (-. (c2_2 (a573) zenon_X6)) % 1.07/1.25 ((a566) != (a577)) % 1.07/1.25 (-. (c3_1 (a468))) % 1.07/1.25 (c7_2 zenon_X27 (a553)) % 1.07/1.25 ((a571) != zenon_X1) % 1.07/1.25 (-. (c1_2 (a592) (a578))) % 1.07/1.25 ((a494) != (a601)) % 1.07/1.25 ((a487) != zenon_X93) % 1.07/1.25 (-. (c2_2 (a494) (a460))) % 1.07/1.25 (-. (c8_2 (a494) (a535))) % 1.07/1.25 ((a538) != zenon_X12) % 1.07/1.25 ((a553) != zenon_X79) % 1.07/1.25 ((a460) != zenon_X46) % 1.07/1.25 ((a553) != zenon_X18) % 1.07/1.25 (c7_2 (a538) (a460)) % 1.07/1.25 (-. (c4_2 (a508) (a487))) % 1.07/1.25 (c3_2 (a496) (a495)) % 1.07/1.25 ((a480) != (a548)) % 1.07/1.25 ((a548) != zenon_X10) % 1.07/1.25 (c6_2 (a592) (a460)) % 1.07/1.25 ((a534) != zenon_X11) % 1.07/1.25 (-. (c1_1 zenon_X19)) % 1.07/1.25 (-. (c2_1 (a534))) % 1.07/1.25 (zenon_X72 != (a553)) % 1.07/1.25 ((a471) != zenon_X33) % 1.07/1.25 ((a533) != zenon_X19) % 1.07/1.25 (-. (c1_1 zenon_X21)) % 1.07/1.25 (-. (c2_2 (a494) (a521))) % 1.07/1.25 (zenon_X12 != (a533)) % 1.07/1.25 (-. (c2_1 (a463))) % 1.07/1.25 (c6_2 (a471) (a472)) % 1.07/1.25 (zenon_X30 != (a534)) % 1.07/1.25 (zenon_X13 != (a498)) % 1.07/1.25 (zenon_X14 != (a484)) % 1.07/1.25 (zenon_X30 != (a544)) % 1.07/1.25 ((a521) != zenon_X6) % 1.07/1.25 (c5_2 zenon_X24 (a487)) % 1.07/1.25 (c6_2 (a471) (a484)) % 1.07/1.25 ((a534) != (a566)) % 1.07/1.25 ((a538) != (a544)) % 1.07/1.25 (c5_1 (a566)) % 1.07/1.25 (-. (c4_2 zenon_X17 (a460))) % 1.07/1.25 ((a534) != (a463)) % 1.07/1.25 ((a487) != zenon_X154) % 1.07/1.25 (-. (c4_2 (a498) (a545))) % 1.07/1.25 (-. (c4_2 (a520) (a487))) % 1.07/1.25 (-. (c4_0)) % 1.07/1.25 ((a460) != (a499)) % 1.07/1.25 ((a535) != zenon_X59) % 1.07/1.25 (c5_2 (a544) (a548)) % 1.07/1.25 (c2_2 (a533) (a548)) % 1.07/1.25 (-. (c8_2 (a482) (a535))) % 1.07/1.25 ((a487) != zenon_X159) % 1.07/1.25 (c6_0) % 1.07/1.25 (-. (c3_2 (a544) (a545))) % 1.07/1.25 (-. (c2_2 zenon_X9 (a483))) % 1.07/1.25 (zenon_X12 != zenon_X9) % 1.07/1.25 (c5_2 (a494) (a460)) % 1.07/1.25 (-. (c4_2 zenon_X33 zenon_X54)) % 1.07/1.25 ((a484) != (a472)) % 1.07/1.25 (c5_1 (a592)) % 1.07/1.25 ((a483) != (a567)) % 1.07/1.25 (-. (c1_1 (a468))) % 1.07/1.25 ((a578) != zenon_X119) % 1.07/1.25 (c3_2 zenon_X21 zenon_X121) % 1.07/1.25 (ndr1_1 zenon_X32) % 1.07/1.25 ((a573) != (a577)) % 1.07/1.25 ((a570) != (a544)) % 1.07/1.25 (zenon_X121 != (a495)) % 1.07/1.25 (zenon_X19 != zenon_X17) % 1.07/1.25 (-. (c4_2 zenon_X17 (a548))) % 1.07/1.25 (zenon_X12 != zenon_X26) % 1.07/1.25 (c1_2 (a544) (a545)) % 1.07/1.25 ((a460) != zenon_X62) % 1.07/1.25 (c2_2 (a520) (a521)) % 1.07/1.25 (c3_2 (a533) (a548)) % 1.07/1.25 ((a480) != (a484)) % 1.07/1.25 (zenon_X31 != (a495)) % 1.07/1.25 (c5_2 (a570) (a460)) % 1.07/1.25 (c5_2 (a482) (a484)) % 1.07/1.25 ((a483) != (a545)) % 1.07/1.25 ((a467) != zenon_X51) % 1.07/1.25 (-. (c1_1 zenon_X26)) % 1.07/1.25 (zenon_X48 != (a460)) % 1.07/1.25 (-. (c1_2 (a538) (a497))) % 1.07/1.25 (zenon_X0 != zenon_X27) % 1.07/1.25 (c1_2 (a601) zenon_X1) % 1.07/1.25 ((a573) != (a498)) % 1.07/1.25 (c3_2 (a538) (a460)) % 1.07/1.25 (c8_1 (a468)) % 1.07/1.25 ((a482) != (a498)) % 1.07/1.25 (-. (c1_2 (a538) zenon_X14)) % 1.07/1.25 (-. (c6_1 (a592))) % 1.07/1.25 ((a494) != zenon_X11) % 1.07/1.25 (-. (c2_2 (a496) (a548))) % 1.07/1.25 (-. (c1_2 (a566) (a567))) % 1.07/1.25 (c5_1 zenon_X11) % 1.07/1.25 ((a535) != zenon_X25) % 1.07/1.25 (-. (c2_2 (a508) (a483))) % 1.07/1.25 (-. (c1_1 (a601))) % 1.07/1.25 ((a566) != zenon_X30) % 1.07/1.25 (zenon_X14 != (a497)) % 1.07/1.25 ((a573) != (a520)) % 1.07/1.25 (zenon_X29 != zenon_X9) % 1.07/1.25 (-. (c3_1 (a496))) % 1.07/1.25 (-. (c4_2 zenon_X33 (a460))) % 1.07/1.25 ((a483) != zenon_X66) % 1.07/1.25 (-. (c2_2 zenon_X21 (a553))) % 1.07/1.25 (c3_2 (a592) (a553)) % 1.07/1.25 (-. (c1_2 (a520) (a521))) % 1.07/1.25 ((a578) != zenon_X25) % 1.07/1.25 (-. (c1_2 (a538) zenon_X59)) % 1.07/1.25 (-. (c2_2 (a520) (a483))) % 1.07/1.25 (-. (c4_2 (a534) zenon_X14)) % 1.07/1.25 (c7_2 (a601) (a553)) % 1.07/1.25 (-. (c1_1 (a520))) % 1.07/1.25 ((a534) != (a577)) % 1.07/1.25 (-. (c3_1 zenon_X30)) % 1.07/1.25 ((a535) != zenon_X123) % 1.07/1.25 (-. (c1_2 (a538) zenon_X16)) % 1.07/1.25 (-. (c4_2 (a538) (a548))) % 1.07/1.25 ((a570) != zenon_X17) % 1.07/1.25 ((a472) != zenon_X61) % 1.07/1.25 (c3_1 zenon_X9) % 1.07/1.25 (zenon_X14 != (a500)) % 1.07/1.25 (c3_2 (a570) (a548)) % 1.07/1.25 (-. (c7_2 (a498) (a472))) % 1.07/1.25 (-. (c2_2 (a570) (a483))) % 1.07/1.25 (-. (c4_2 (a533) zenon_X107)) % 1.07/1.25 (zenon_X13 != zenon_X17) % 1.07/1.25 (-. (c4_1 zenon_X19)) % 1.07/1.25 ((a460) != zenon_X10) % 1.07/1.25 (zenon_X12 != zenon_X27) % 1.07/1.25 ((a495) != (a579)) % 1.07/1.25 (c2_1 (a533)) % 1.07/1.25 ((a521) != zenon_X46) % 1.07/1.25 ((a535) != zenon_X47) % 1.07/1.25 (c3_1 (a570)) % 1.07/1.25 ((a601) != (a544)) % 1.07/1.25 (-. (c4_2 zenon_X26 zenon_X154)) % 1.07/1.25 ((a494) != (a534)) % 1.07/1.25 ((a553) != zenon_X82) % 1.07/1.25 ((a535) != (a484)) % 1.07/1.25 ((a535) != (a579)) % 1.07/1.25 (c2_1 zenon_X13) % 1.07/1.25 (-. (c1_2 (a538) zenon_X20)) % 1.07/1.25 ((a538) != zenon_X17) % 1.07/1.25 (-. (c4_2 (a496) (a487))) % 1.07/1.25 (zenon_X29 != (a577)) % 1.07/1.25 ((a535) != zenon_X63) % 1.07/1.25 (zenon_X59 != zenon_X16) % 1.07/1.25 (c5_2 (a494) (a500)) % 1.07/1.25 (c5_1 zenon_X9) % 1.07/1.25 (-. (c4_2 zenon_X24 (a500))) % 1.07/1.25 (-. (c8_2 (a498) (a467))) % 1.07/1.25 (-. (c3_2 (a496) (a553))) % 1.07/1.25 ((a468) != zenon_X33) % 1.07/1.25 ((a460) != (a483)) % 1.07/1.25 (c3_2 (a592) zenon_X72) % 1.07/1.25 ((a520) != zenon_X26) % 1.07/1.25 (zenon_X13 != zenon_X27) % 1.07/1.25 (-. (c4_2 (a566) (a548))) % 1.07/1.25 (-. (c4_2 (a471) zenon_X91)) % 1.07/1.25 (-. (c4_2 (a463) zenon_X16)) % 1.07/1.25 ((a498) != (a592)) % 1.07/1.25 ((a544) != zenon_X21) % 1.07/1.25 (-. (c5_1 (a520))) % 1.07/1.25 ((a577) != (a544)) % 1.07/1.25 ((a500) != zenon_X63) % 1.07/1.25 (-. (c2_2 (a534) (a553))) % 1.07/1.25 (zenon_X24 != (a498)) % 1.07/1.25 (-. (c4_2 zenon_X30 zenon_X151)) % 1.07/1.25 (-. (c2_1 (a471))) % 1.07/1.25 (-. (c2_2 (a496) zenon_X149)) % 1.07/1.25 ((a494) != (a496)) % 1.07/1.25 (-. (c4_2 (a573) (a487))) % 1.07/1.25 (-. (c8_2 (a577) (a495))) % 1.07/1.25 ((a500) != zenon_X48) % 1.07/1.25 (-. (c2_2 (a471) (a548))) % 1.07/1.25 ((a471) != zenon_X30) % 1.07/1.25 (c8_2 zenon_X32 (a460)) % 1.07/1.25 ((a468) != zenon_X30) % 1.07/1.25 (zenon_X12 != zenon_X24) % 1.07/1.25 ((a548) != (a571)) % 1.07/1.25 (c3_2 zenon_X29 (a460)) % 1.07/1.25 (zenon_X39 != (a495)) % 1.07/1.25 (c3_2 zenon_X0 (a495)) % 1.07/1.25 ((a592) != zenon_X21) % 1.07/1.25 (-. (c4_2 (a494) (a535))) % 1.07/1.25 (c5_2 (a534) (a535)) % 1.07/1.25 (-. (c2_2 (a566) (a535))) % 1.07/1.25 (-. (c7_2 (a468) zenon_X138)) % 1.07/1.25 (zenon_X90 != zenon_X54) % 1.07/1.25 (zenon_X14 != zenon_X16) % 1.07/1.25 (-. (c7_2 zenon_X19 zenon_X143)) % 1.07/1.25 (-. (c7_2 zenon_X33 (a460))) % 1.07/1.25 (-. (c1_2 (a592) zenon_X1)) % 1.07/1.25 (zenon_X13 != zenon_X33) % 1.07/1.25 (zenon_X116 != (a487)) % 1.07/1.25 ((a592) != zenon_X17) % 1.07/1.25 ((a487) != zenon_X59) % 1.07/1.25 ((a471) != (a544)) % 1.07/1.25 (-. (c3_2 zenon_X27 (a553))) % 1.07/1.25 (-. (c2_2 (a601) (a553))) % 1.07/1.25 (-. (c2_2 (a494) (a571))) % 1.07/1.25 (-. (c8_2 (a482) zenon_X25)) % 1.07/1.25 (-. (c4_2 zenon_X27 zenon_X150)) % 1.07/1.25 (-. (c4_2 (a520) (a460))) % 1.07/1.25 (c7_2 (a534) (a553)) % 1.07/1.25 ((a498) != (a520)) % 1.07/1.25 (-. (c7_2 (a494) zenon_X69)) % 1.07/1.25 (c8_2 (a494) (a495)) % 1.07/1.25 ((a566) != zenon_X11) % 1.07/1.25 ((a535) != zenon_X94) % 1.07/1.25 *) % 1.07/1.25 (* NO-PROOF *) % 1.07/1.25 % SZS status GaveUp % 1.07/1.25 Number of rewrites on terms: 0 % 1.07/1.25 Number of rewrites on props: 0 % 1.07/1.25 nodes searched: 20335 % 1.07/1.25 max branch formulas: 3255 % 1.07/1.25 proof nodes created: 1288 % 1.07/1.25 formulas created: 39457 % 1.07/1.25 %------------------------------------------------------------------------------