%------------------------------------------------------------------------------ % File : ZenonModulo---0.5.0 % Problem : SYN539+1 : TPTP v8.2.0. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : run_zenon_modulo %d %s % Computer : n011.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:54 EDT 2024 % Result : Unknown 1.93s 2.17s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SYN539+1 : TPTP v8.2.0. Released v2.1.0. % 0.00/0.11 % Command : run_zenon_modulo %d %s % 0.11/0.32 % Computer : n011.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 300 % 0.11/0.32 % DateTime : Mon Jun 24 02:47:09 EDT 2024 % 0.11/0.32 % CPUTime : % 1.93/2.16 Zenon error: exhausted search space without finding a proof % 1.93/2.16 (* Current branch: % 1.93/2.16 (zenon_X24 != (a638)) % 1.93/2.16 (zenon_X14 != zenon_X31) % 1.93/2.16 ((a610) != zenon_X30) % 1.93/2.16 (c5_2 (a616) (a597)) % 1.93/2.16 ((a594) != (a620)) % 1.93/2.16 (zenon_X44 != zenon_X31) % 1.93/2.16 (zenon_X1 != (a633)) % 1.93/2.16 (-. (c5_2 zenon_X3 zenon_X48)) % 1.93/2.16 (c5_2 (a633) zenon_X42) % 1.93/2.16 (zenon_X15 != zenon_X19) % 1.93/2.16 (c4_2 zenon_X1 zenon_X19) % 1.93/2.16 (c5_2 zenon_X3 zenon_X23) % 1.93/2.16 (c5_2 zenon_X3 zenon_X19) % 1.93/2.16 (c5_2 (a616) zenon_X48) % 1.93/2.16 (-. (c5_2 (a613) zenon_X24)) % 1.93/2.16 (zenon_X18 != zenon_X31) % 1.93/2.16 (-. (c1_1 (a633))) % 1.93/2.16 (c1_2 (a616) zenon_X13) % 1.93/2.16 (zenon_X4 != zenon_X50) % 1.93/2.16 ((a636) != zenon_X38) % 1.93/2.16 (zenon_X0 != zenon_X3) % 1.93/2.16 (-. (c5_2 zenon_X6 zenon_X15)) % 1.93/2.16 (c2_2 zenon_X1 zenon_X25) % 1.93/2.16 (c2_2 (a637) (a598)) % 1.93/2.16 (c5_2 (a633) (a639)) % 1.93/2.16 (zenon_X40 != zenon_X11) % 1.93/2.16 ((a587) != zenon_X6) % 1.93/2.16 (c1_2 (a594) zenon_X26) % 1.93/2.16 ((a596) != zenon_X3) % 1.93/2.16 (-. (c5_2 zenon_X6 zenon_X30)) % 1.93/2.16 ((a614) != zenon_X17) % 1.93/2.16 (zenon_X44 != (a639)) % 1.93/2.16 (-. (c2_2 (a613) zenon_X16)) % 1.93/2.16 (zenon_X4 != zenon_X15) % 1.93/2.16 (-. (c2_2 (a613) zenon_X20)) % 1.93/2.16 (-. (c5_2 (a616) zenon_X19)) % 1.93/2.16 ((a636) != zenon_X21) % 1.93/2.16 (zenon_X38 != zenon_X19) % 1.93/2.16 ((a597) != zenon_X39) % 1.93/2.16 (c2_2 (a616) zenon_X34) % 1.93/2.16 ((a610) != zenon_X26) % 1.93/2.16 (c2_2 (a594) (a598)) % 1.93/2.16 (-. (c5_2 zenon_X10 zenon_X23)) % 1.93/2.16 ((a636) != (a597)) % 1.93/2.16 ((a636) != zenon_X20) % 1.93/2.16 (c4_2 (a613) zenon_X46) % 1.93/2.16 (c2_2 (a613) (a639)) % 1.93/2.16 (c2_2 zenon_X1 zenon_X23) % 1.93/2.16 (c3_1 (a596)) % 1.93/2.16 (c5_2 (a633) zenon_X40) % 1.93/2.16 (c1_2 zenon_X1 (a639)) % 1.93/2.16 (-. (c5_2 zenon_X3 zenon_X34)) % 1.93/2.16 (-. (c5_2 (a616) zenon_X17)) % 1.93/2.16 ((a638) != zenon_X42) % 1.93/2.16 (zenon_X28 != zenon_X24) % 1.93/2.16 (c4_2 (a637) zenon_X46) % 1.93/2.16 (c2_2 (a613) (a614)) % 1.93/2.16 (zenon_X26 != zenon_X42) % 1.93/2.16 ((a616) != zenon_X8) % 1.93/2.16 (c1_2 zenon_X3 zenon_X13) % 1.93/2.16 (zenon_X38 != zenon_X34) % 1.93/2.16 (zenon_X4 != zenon_X34) % 1.93/2.16 ((a636) != zenon_X25) % 1.93/2.16 (c4_2 (a594) zenon_X50) % 1.93/2.16 ((a614) != zenon_X46) % 1.93/2.16 (-. (c5_2 zenon_X10 zenon_X18)) % 1.93/2.16 (c4_2 zenon_X10 (a614)) % 1.93/2.16 (-. (c5_2 zenon_X3 zenon_X31)) % 1.93/2.16 (zenon_X25 != zenon_X50) % 1.93/2.16 (c4_2 (a613) zenon_X44) % 1.93/2.16 (zenon_X40 != zenon_X30) % 1.93/2.16 (c5_2 zenon_X3 (a614)) % 1.93/2.16 (c4_2 zenon_X10 zenon_X48) % 1.93/2.16 (c5_2 (a633) zenon_X20) % 1.93/2.16 (c4_2 zenon_X6 zenon_X14) % 1.93/2.16 ((a639) != zenon_X9) % 1.93/2.16 (-. (c2_2 (a613) zenon_X5)) % 1.93/2.16 (-. (c5_2 zenon_X1 zenon_X19)) % 1.93/2.16 (c5_2 (a633) zenon_X17) % 1.93/2.16 (c5_2 (a637) zenon_X32) % 1.93/2.16 ((a638) != zenon_X5) % 1.93/2.16 (zenon_X13 != zenon_X34) % 1.93/2.16 (zenon_X19 != zenon_X17) % 1.93/2.16 (c4_2 (a637) zenon_X28) % 1.93/2.16 (-. (c5_2 zenon_X10 zenon_X20)) % 1.93/2.16 (-. (c5_2 zenon_X10 zenon_X33)) % 1.93/2.16 ((a598) != zenon_X23) % 1.93/2.16 ((a614) != zenon_X20) % 1.93/2.16 (-. (c5_2 (a637) zenon_X33)) % 1.93/2.16 (-. (c1_2 zenon_X3 zenon_X4)) % 1.93/2.16 ((a638) != (a597)) % 1.93/2.16 (-. (c4_1 (a620))) % 1.93/2.16 (c5_2 (a594) zenon_X26) % 1.93/2.16 (-. (c5_2 zenon_X10 zenon_X30)) % 1.93/2.16 (c2_2 (a613) (a610)) % 1.93/2.16 (zenon_X26 != (a614)) % 1.93/2.16 (-. (c5_2 (a594) zenon_X38)) % 1.93/2.16 (zenon_X18 != zenon_X14) % 1.93/2.16 (c2_2 zenon_X3 zenon_X28) % 1.93/2.16 (zenon_X20 != zenon_X18) % 1.93/2.16 (zenon_X10 != zenon_X12) % 1.93/2.16 ((a636) != zenon_X31) % 1.93/2.16 (c1_2 (a613) (a636)) % 1.93/2.16 (zenon_X40 != zenon_X13) % 1.93/2.16 (zenon_X40 != zenon_X48) % 1.93/2.16 (c2_2 zenon_X1 (a639)) % 1.93/2.16 (c4_2 zenon_X1 zenon_X33) % 1.93/2.16 ((a636) != zenon_X30) % 1.93/2.16 (c1_2 zenon_X3 zenon_X28) % 1.93/2.16 (zenon_X16 != zenon_X25) % 1.93/2.16 ((a639) != zenon_X34) % 1.93/2.16 (zenon_X16 != zenon_X5) % 1.93/2.16 (zenon_X0 != (a637)) % 1.93/2.16 (zenon_X15 != zenon_X50) % 1.93/2.16 (c2_2 (a594) zenon_X13) % 1.93/2.16 (zenon_X28 != zenon_X15) % 1.93/2.16 (zenon_X11 != zenon_X24) % 1.93/2.16 ((a594) != zenon_X8) % 1.93/2.16 (zenon_X18 != zenon_X19) % 1.93/2.16 (c4_2 zenon_X6 zenon_X16) % 1.93/2.16 (zenon_X17 != zenon_X34) % 1.93/2.16 (-. (c5_2 zenon_X3 zenon_X20)) % 1.93/2.16 (zenon_X30 != zenon_X15) % 1.93/2.16 (c2_2 zenon_X3 zenon_X18) % 1.93/2.16 ((a616) != (a596)) % 1.93/2.16 (-. (c5_2 (a594) zenon_X17)) % 1.93/2.16 (zenon_X24 != zenon_X48) % 1.93/2.16 (zenon_X20 != zenon_X44) % 1.93/2.16 (c2_2 (a613) zenon_X32) % 1.93/2.16 (c5_2 zenon_X1 zenon_X23) % 1.93/2.16 (-. (c1_2 (a587) zenon_X41)) % 1.93/2.16 (-. (c5_2 zenon_X10 zenon_X50)) % 1.93/2.16 (c1_2 (a594) zenon_X18) % 1.93/2.16 (zenon_X23 != zenon_X46) % 1.93/2.16 (zenon_X20 != zenon_X16) % 1.93/2.16 (-. (c1_2 (a596) (a638))) % 1.93/2.16 (zenon_X38 != (a597)) % 1.93/2.16 (c1_2 (a613) zenon_X28) % 1.93/2.16 (c5_2 zenon_X3 zenon_X11) % 1.93/2.16 (c5_2 (a637) (a639)) % 1.93/2.16 ((a596) != zenon_X10) % 1.93/2.16 (zenon_X28 != zenon_X31) % 1.93/2.16 (c5_2 (a613) (a598)) % 1.93/2.16 (zenon_X26 != zenon_X50) % 1.93/2.16 (zenon_X4 != zenon_X24) % 1.93/2.16 (c4_2 (a594) zenon_X42) % 1.93/2.16 ((a610) != zenon_X17) % 1.93/2.16 (zenon_X44 != zenon_X46) % 1.93/2.16 (c1_2 (a613) zenon_X14) % 1.93/2.16 (zenon_X28 != (a614)) % 1.93/2.16 (c1_2 (a616) zenon_X44) % 1.93/2.16 ((a636) != zenon_X28) % 1.93/2.16 (-. (c5_2 zenon_X6 (a614))) % 1.93/2.16 ((a598) != zenon_X46) % 1.93/2.16 (-. (c5_2 zenon_X10 zenon_X34)) % 1.93/2.16 (zenon_X15 != (a598)) % 1.93/2.16 (c1_2 (a613) zenon_X50) % 1.93/2.16 (c1_2 zenon_X1 (a636)) % 1.93/2.16 (zenon_X17 != zenon_X33) % 1.93/2.16 (c5_2 (a633) zenon_X33) % 1.93/2.16 (zenon_X32 != zenon_X18) % 1.93/2.16 (-. (c3_2 (a596) (a636))) % 1.93/2.16 (c4_1 (a594)) % 1.93/2.16 (zenon_X3 != zenon_X12) % 1.93/2.16 (c5_2 (a613) (a639)) % 1.93/2.16 (-. (c5_2 (a616) zenon_X24)) % 1.93/2.16 (c1_2 zenon_X6 zenon_X44) % 1.93/2.16 (-. (c5_2 (a594) zenon_X42)) % 1.93/2.16 (c5_2 (a594) (a598)) % 1.93/2.16 (zenon_X44 != zenon_X38) % 1.93/2.16 (c1_2 zenon_X1 zenon_X25) % 1.93/2.16 ((a610) != zenon_X46) % 1.93/2.16 (c1_2 (a613) zenon_X32) % 1.93/2.16 (-. (c1_2 zenon_X7 zenon_X43)) % 1.93/2.16 (c2_2 zenon_X1 zenon_X24) % 1.93/2.16 (zenon_X24 != zenon_X50) % 1.93/2.16 (zenon_X11 != zenon_X20) % 1.93/2.16 (zenon_X40 != zenon_X32) % 1.93/2.16 (c5_2 zenon_X6 zenon_X20) % 1.93/2.16 (zenon_X33 != zenon_X5) % 1.93/2.16 (c4_2 (a637) zenon_X33) % 1.93/2.16 (c5_2 (a594) (a636)) % 1.93/2.16 (c2_2 zenon_X10 zenon_X44) % 1.93/2.16 (-. (c3_2 (a613) (a636))) % 1.93/2.16 (-. (c5_2 zenon_X6 zenon_X34)) % 1.93/2.16 (zenon_X30 != zenon_X48) % 1.93/2.16 (zenon_X44 != zenon_X14) % 1.93/2.16 ((a639) != zenon_X24) % 1.93/2.16 (zenon_X7 != zenon_X6) % 1.93/2.16 (c5_2 (a616) zenon_X28) % 1.93/2.16 (c4_2 zenon_X10 zenon_X18) % 1.93/2.16 (c1_2 zenon_X1 zenon_X44) % 1.93/2.16 (zenon_X19 != zenon_X42) % 1.93/2.16 (c4_2 (a616) zenon_X46) % 1.93/2.16 (c1_2 zenon_X1 zenon_X14) % 1.93/2.16 ((a638) != zenon_X46) % 1.93/2.16 (zenon_X30 != zenon_X17) % 1.93/2.16 (c2_2 (a616) (a639)) % 1.93/2.16 ((a639) != zenon_X28) % 1.93/2.16 (c2_2 (a594) zenon_X24) % 1.93/2.16 (-. (c5_2 (a594) zenon_X50)) % 1.93/2.16 (-. (c5_2 (a637) (a614))) % 1.93/2.16 (-. (c5_2 zenon_X6 zenon_X50)) % 1.93/2.16 ((a587) != (a613)) % 1.93/2.16 (c5_2 zenon_X3 zenon_X32) % 1.93/2.16 (c4_2 zenon_X6 zenon_X34) % 1.93/2.16 ((a597) != zenon_X17) % 1.93/2.16 (c4_2 zenon_X10 (a638)) % 1.93/2.16 (c5_2 zenon_X3 (a639)) % 1.93/2.16 (zenon_X30 != (a597)) % 1.93/2.16 (c2_2 zenon_X3 (a614)) % 1.93/2.16 (c5_2 zenon_X1 zenon_X31) % 1.93/2.16 (c2_2 zenon_X3 zenon_X5) % 1.93/2.16 (zenon_X46 != zenon_X31) % 1.93/2.16 (zenon_X23 != zenon_X19) % 1.93/2.16 (zenon_X8 != (a613)) % 1.93/2.16 (c4_2 (a613) zenon_X16) % 1.93/2.16 ((a639) != zenon_X33) % 1.93/2.16 (zenon_X38 != zenon_X50) % 1.93/2.16 ((a597) != zenon_X5) % 1.93/2.16 (zenon_X30 != (a614)) % 1.93/2.16 (c5_2 zenon_X1 zenon_X16) % 1.93/2.16 (zenon_X19 != zenon_X31) % 1.93/2.16 (zenon_X28 != zenon_X50) % 1.93/2.16 (zenon_X7 != zenon_X10) % 1.93/2.16 (c1_2 (a616) zenon_X11) % 1.93/2.16 (zenon_X11 != (a638)) % 1.93/2.16 ((a639) != zenon_X23) % 1.93/2.16 (zenon_X16 != zenon_X33) % 1.93/2.16 (c2_2 (a637) zenon_X34) % 1.93/2.16 ((a594) != zenon_X12) % 1.93/2.16 (zenon_X24 != zenon_X34) % 1.93/2.16 ((a614) != zenon_X21) % 1.93/2.16 (zenon_X32 != zenon_X46) % 1.93/2.16 ((a639) != zenon_X46) % 1.93/2.16 ((a636) != zenon_X26) % 1.93/2.16 (c4_2 (a637) zenon_X17) % 1.93/2.16 (c5_2 zenon_X3 zenon_X46) % 1.93/2.16 (zenon_X30 != zenon_X25) % 1.93/2.16 (c1_2 (a594) zenon_X23) % 1.93/2.16 ((a638) != zenon_X48) % 1.93/2.16 (zenon_X30 != zenon_X14) % 1.93/2.16 (c1_2 zenon_X1 zenon_X24) % 1.93/2.16 (c1_0) % 1.93/2.16 (zenon_X28 != zenon_X25) % 1.93/2.16 (-. (c5_2 zenon_X6 zenon_X31)) % 1.93/2.16 (c2_2 (a613) zenon_X4) % 1.93/2.16 ((a598) != zenon_X38) % 1.93/2.16 (-. (c1_2 (a587) (a598))) % 1.93/2.16 (c1_2 zenon_X10 (a636)) % 1.93/2.16 ((a598) != (a638)) % 1.93/2.16 ((a597) != zenon_X48) % 1.93/2.16 ((a613) != zenon_X3) % 1.93/2.16 (c1_2 zenon_X1 zenon_X20) % 1.93/2.16 (-. (c5_2 zenon_X10 (a614))) % 1.93/2.16 (c2_2 zenon_X3 (a639)) % 1.93/2.16 (c5_1 (a596)) % 1.93/2.16 (c1_2 (a637) (a638)) % 1.93/2.16 (-. (c5_2 zenon_X10 zenon_X11)) % 1.93/2.16 (ndr1_1 zenon_X1) % 1.93/2.16 (zenon_X44 != (a614)) % 1.93/2.16 ((a614) != zenon_X34) % 1.93/2.16 ((a597) != zenon_X46) % 1.93/2.16 (c4_2 zenon_X6 zenon_X15) % 1.93/2.16 (-. (c5_2 (a616) zenon_X16)) % 1.93/2.16 (zenon_X13 != zenon_X16) % 1.93/2.16 (c4_2 zenon_X3 zenon_X31) % 1.93/2.16 ((a594) != zenon_X6) % 1.93/2.16 (zenon_X26 != zenon_X17) % 1.93/2.16 (zenon_X17 != zenon_X50) % 1.93/2.16 ((a639) != zenon_X5) % 1.93/2.16 (-. (c5_2 zenon_X6 (a639))) % 1.93/2.16 (c4_2 (a616) zenon_X16) % 1.93/2.16 (zenon_X14 != zenon_X5) % 1.93/2.16 (c5_2 (a594) zenon_X11) % 1.93/2.16 (c2_2 (a596) (a598)) % 1.93/2.16 (c1_2 (a594) (a598)) % 1.93/2.16 (c4_2 zenon_X3 zenon_X48) % 1.93/2.16 (c4_2 (a613) zenon_X23) % 1.93/2.16 (c1_2 (a596) (a598)) % 1.93/2.16 ((a637) != zenon_X10) % 1.93/2.16 (zenon_X5 != zenon_X46) % 1.93/2.16 (zenon_X17 != zenon_X42) % 1.93/2.16 (c5_2 (a613) zenon_X34) % 1.93/2.16 (-. (c1_2 zenon_X0 zenon_X45)) % 1.93/2.16 (zenon_X13 != zenon_X15) % 1.93/2.16 (c5_2 (a633) zenon_X11) % 1.93/2.16 (c2_2 zenon_X10 zenon_X38) % 1.93/2.16 (c4_2 zenon_X10 zenon_X16) % 1.93/2.16 (c2_2 zenon_X1 zenon_X26) % 1.93/2.16 (c1_2 (a594) zenon_X14) % 1.93/2.16 (c2_2 zenon_X1 (a636)) % 1.93/2.16 (zenon_X44 != zenon_X18) % 1.93/2.16 (zenon_X4 != zenon_X18) % 1.93/2.16 (c2_2 zenon_X3 zenon_X32) % 1.93/2.16 (-. (c5_2 (a594) zenon_X40)) % 1.93/2.16 (c2_2 zenon_X1 zenon_X17) % 1.93/2.16 (c2_2 (a594) zenon_X30) % 1.93/2.16 (zenon_X30 != zenon_X42) % 1.93/2.16 (c4_2 (a594) zenon_X4) % 1.93/2.16 ((a614) != zenon_X4) % 1.93/2.16 (c5_2 (a616) zenon_X13) % 1.93/2.16 (c2_2 zenon_X6 zenon_X40) % 1.93/2.16 (zenon_X25 != zenon_X31) % 1.93/2.16 ((a639) != zenon_X19) % 1.93/2.16 (c1_1 (a613)) % 1.93/2.16 (zenon_X14 != zenon_X34) % 1.93/2.16 (c1_2 (a613) (a598)) % 1.93/2.16 ((a636) != (a610)) % 1.93/2.16 (c4_2 zenon_X10 zenon_X15) % 1.93/2.16 (c4_2 zenon_X3 zenon_X50) % 1.93/2.16 (c2_2 zenon_X3 (a636)) % 1.93/2.16 (c4_2 zenon_X10 zenon_X40) % 1.93/2.16 ((a613) != (a596)) % 1.93/2.16 ((a598) != zenon_X9) % 1.93/2.16 (zenon_X0 != (a616)) % 1.93/2.16 (zenon_X28 != zenon_X5) % 1.93/2.16 (c5_2 (a637) (a638)) % 1.93/2.16 (-. (c1_1 zenon_X8)) % 1.93/2.16 (-. (c5_2 (a616) zenon_X46)) % 1.93/2.16 ((a639) != (a610)) % 1.93/2.16 (zenon_X18 != zenon_X13) % 1.93/2.16 (c2_2 zenon_X6 zenon_X20) % 1.93/2.16 ((a610) != zenon_X34) % 1.93/2.16 (c4_2 (a594) zenon_X32) % 1.93/2.16 (-. (c5_2 (a613) zenon_X42)) % 1.93/2.16 (zenon_X13 != (a639)) % 1.93/2.16 (c5_2 (a633) zenon_X31) % 1.93/2.16 (-. (c5_2 zenon_X10 zenon_X5)) % 1.93/2.16 (zenon_X32 != zenon_X50) % 1.93/2.16 (c5_2 zenon_X3 zenon_X15) % 1.93/2.16 (c4_2 zenon_X10 zenon_X5) % 1.93/2.16 (c5_2 zenon_X3 zenon_X14) % 1.93/2.16 (zenon_X13 != zenon_X33) % 1.93/2.16 (zenon_X44 != zenon_X48) % 1.93/2.16 (c2_2 zenon_X10 zenon_X4) % 1.93/2.16 (c2_2 zenon_X3 zenon_X11) % 1.93/2.16 (-. (c5_2 (a594) zenon_X34)) % 1.93/2.16 ((a587) != zenon_X12) % 1.93/2.16 (zenon_X38 != zenon_X13) % 1.93/2.16 (zenon_X1 != zenon_X10) % 1.93/2.16 (-. (c3_2 (a594) (a636))) % 1.93/2.16 (zenon_X31 != (a614)) % 1.93/2.16 ((a638) != zenon_X18) % 1.93/2.16 (zenon_X40 != (a614)) % 1.93/2.16 ((a598) != zenon_X34) % 1.93/2.16 (zenon_X40 != zenon_X46) % 1.93/2.16 (zenon_X8 != (a637)) % 1.93/2.16 ((a639) != zenon_X31) % 1.93/2.16 (zenon_X15 != (a614)) % 1.93/2.16 ((a614) != zenon_X33) % 1.93/2.16 (c1_2 zenon_X10 zenon_X4) % 1.93/2.16 ((a638) != zenon_X19) % 1.93/2.16 (zenon_X33 != zenon_X50) % 1.93/2.16 (c2_2 zenon_X3 zenon_X25) % 1.93/2.16 (c5_2 zenon_X1 zenon_X42) % 1.93/2.16 (c1_1 (a594)) % 1.93/2.16 (-. (c5_1 (a637))) % 1.93/2.16 (c2_2 (a594) zenon_X15) % 1.93/2.16 (c5_2 (a637) zenon_X19) % 1.93/2.16 (c5_2 (a637) zenon_X38) % 1.93/2.16 ((a636) != zenon_X15) % 1.93/2.16 (-. (c2_2 (a613) zenon_X15)) % 1.93/2.16 ((a638) != zenon_X32) % 1.93/2.16 (zenon_X7 != (a633)) % 1.93/2.16 (zenon_X16 != zenon_X48) % 1.93/2.16 (-. (c5_2 (a616) zenon_X38)) % 1.93/2.16 (zenon_X31 != zenon_X5) % 1.93/2.16 ((a587) != (a594)) % 1.93/2.16 (-. (c5_2 (a637) zenon_X20)) % 1.93/2.16 (c5_2 (a637) zenon_X5) % 1.93/2.16 (zenon_X1 != zenon_X6) % 1.93/2.16 (c5_2 (a613) (a610)) % 1.93/2.16 (zenon_X44 != zenon_X26) % 1.93/2.16 (c4_2 zenon_X10 zenon_X13) % 1.93/2.16 (zenon_X13 != zenon_X31) % 1.93/2.16 (zenon_X16 != zenon_X19) % 1.93/2.16 ((a594) != (a637)) % 1.93/2.16 (zenon_X0 != (a633)) % 1.93/2.16 (c2_2 zenon_X3 (a638)) % 1.93/2.16 (zenon_X46 != zenon_X34) % 1.93/2.16 (c5_2 (a633) (a598)) % 1.93/2.16 (c4_2 (a594) zenon_X40) % 1.93/2.16 ((a610) != zenon_X44) % 1.93/2.16 (-. (c5_2 (a616) zenon_X30)) % 1.93/2.16 (c5_2 zenon_X3 zenon_X26) % 1.93/2.16 (c4_2 zenon_X10 zenon_X26) % 1.93/2.16 (zenon_X16 != zenon_X24) % 1.93/2.16 (-. (c5_2 zenon_X1 zenon_X5)) % 1.93/2.16 (zenon_X46 != zenon_X42) % 1.93/2.16 (zenon_X16 != zenon_X34) % 1.93/2.16 (-. (c1_2 (a633) (a639))) % 1.93/2.16 (zenon_X28 != zenon_X17) % 1.93/2.16 (-. (c5_2 (a637) zenon_X23)) % 1.93/2.16 (-. (c5_2 (a637) zenon_X16)) % 1.93/2.16 (c5_2 (a633) zenon_X16) % 1.93/2.16 (c2_2 zenon_X1 zenon_X48) % 1.93/2.16 (zenon_X38 != zenon_X18) % 1.93/2.16 (zenon_X15 != (a639)) % 1.93/2.16 (-. (c2_1 (a616))) % 1.93/2.16 (c5_2 zenon_X1 zenon_X18) % 1.93/2.16 (c2_2 zenon_X1 (a614)) % 1.93/2.16 (c4_2 zenon_X10 zenon_X11) % 1.93/2.16 (c1_2 zenon_X3 zenon_X33) % 1.93/2.16 ((a639) != zenon_X25) % 1.93/2.16 (c5_2 zenon_X1 zenon_X30) % 1.93/2.16 (ndr1_1 zenon_X6) % 1.93/2.16 (c5_2 zenon_X3 (a638)) % 1.93/2.16 (c5_2 (a637) zenon_X44) % 1.93/2.16 (-. (c3_1 (a616))) % 1.93/2.16 ((a636) != zenon_X5) % 1.93/2.16 (-. (c5_2 (a613) zenon_X20)) % 1.93/2.16 (-. (c5_2 (a613) zenon_X26)) % 1.93/2.16 (c4_2 (a613) zenon_X26) % 1.93/2.16 (zenon_X38 != zenon_X32) % 1.93/2.16 (zenon_X31 != zenon_X48) % 1.93/2.16 ((a594) != zenon_X3) % 1.93/2.16 (c2_2 (a616) zenon_X4) % 1.93/2.16 (zenon_X38 != zenon_X48) % 1.93/2.16 (zenon_X44 != zenon_X32) % 1.93/2.16 (c2_2 (a594) zenon_X11) % 1.93/2.16 (zenon_X4 != zenon_X38) % 1.93/2.16 (c5_2 (a594) zenon_X14) % 1.93/2.16 (c4_2 zenon_X3 (a610)) % 1.93/2.16 (zenon_X4 != zenon_X30) % 1.93/2.16 (zenon_X4 != zenon_X14) % 1.93/2.16 ((a633) != (a637)) % 1.93/2.16 (c5_2 (a637) zenon_X50) % 1.93/2.16 (c5_2 zenon_X10 zenon_X4) % 1.93/2.16 ((a598) != (a597)) % 1.93/2.16 (zenon_X16 != zenon_X26) % 1.93/2.16 ((a633) != (a613)) % 1.93/2.16 (-. (c5_2 zenon_X3 zenon_X42)) % 1.93/2.16 (zenon_X20 != zenon_X50) % 1.93/2.16 (c2_2 (a616) (a636)) % 1.93/2.16 (zenon_X1 != (a613)) % 1.93/2.16 (zenon_X11 != zenon_X50) % 1.93/2.16 (zenon_X30 != zenon_X24) % 1.93/2.16 (-. (c3_1 (a613))) % 1.93/2.16 (zenon_X6 != zenon_X8) % 1.93/2.16 (c1_1 (a616)) % 1.93/2.16 (zenon_X1 != (a596)) % 1.93/2.16 (zenon_X44 != (a638)) % 1.93/2.16 (zenon_X40 != zenon_X50) % 1.93/2.16 ((a616) != (a633)) % 1.93/2.16 ((a587) != (a637)) % 1.93/2.16 (zenon_X20 != zenon_X23) % 1.93/2.16 (-. (c5_2 (a616) zenon_X18)) % 1.93/2.16 (-. (c3_2 (a587) (a636))) % 1.93/2.16 (zenon_X11 != zenon_X28) % 1.93/2.16 (c2_2 zenon_X3 zenon_X30) % 1.93/2.16 (zenon_X40 != zenon_X33) % 1.93/2.16 ((a610) != zenon_X28) % 1.93/2.16 (c4_2 (a594) zenon_X38) % 1.93/2.16 (-. (c5_2 zenon_X10 zenon_X13)) % 1.93/2.16 ((a633) != zenon_X10) % 1.93/2.16 (zenon_X8 != zenon_X10) % 1.93/2.16 (-. (c5_2 zenon_X6 (a636))) % 1.93/2.16 (-. (c5_2 (a613) zenon_X48)) % 1.93/2.16 (c1_2 zenon_X10 zenon_X31) % 1.93/2.16 (zenon_X20 != zenon_X24) % 1.93/2.16 ((a616) != (a594)) % 1.93/2.16 (zenon_X4 != zenon_X13) % 1.93/2.16 (-. (c1_2 (a613) zenon_X18)) % 1.93/2.16 (c5_2 (a637) (a636)) % 1.93/2.16 (c1_2 (a613) zenon_X34) % 1.93/2.16 (c5_2 zenon_X3 (a598)) % 1.93/2.16 ((a610) != zenon_X13) % 1.93/2.16 (zenon_X32 != zenon_X24) % 1.93/2.16 ((a638) != zenon_X16) % 1.93/2.16 (c5_2 zenon_X10 zenon_X44) % 1.93/2.16 (c4_2 (a616) zenon_X14) % 1.93/2.16 (c5_2 (a637) (a598)) % 1.93/2.16 (c1_2 zenon_X10 zenon_X44) % 1.93/2.16 (zenon_X11 != zenon_X19) % 1.93/2.16 (zenon_X4 != zenon_X42) % 1.93/2.16 (-. (c5_2 (a613) zenon_X38)) % 1.93/2.16 (c2_2 (a637) zenon_X25) % 1.93/2.16 (c4_2 zenon_X6 zenon_X24) % 1.93/2.16 (zenon_X44 != zenon_X17) % 1.93/2.16 (zenon_X28 != zenon_X33) % 1.93/2.16 (-. (c5_2 (a613) zenon_X18)) % 1.93/2.16 (-. (c2_2 (a633) (a639))) % 1.93/2.16 (zenon_X30 != zenon_X34) % 1.93/2.16 (zenon_X14 != zenon_X33) % 1.93/2.16 (zenon_X5 != zenon_X42) % 1.93/2.16 (zenon_X30 != zenon_X13) % 1.93/2.16 ((a639) != zenon_X26) % 1.93/2.16 (zenon_X4 != zenon_X17) % 1.93/2.16 (zenon_X24 != zenon_X5) % 1.93/2.16 (c2_2 zenon_X1 zenon_X4) % 1.93/2.16 (c5_2 (a633) zenon_X13) % 1.93/2.16 (c5_2 (a594) zenon_X15) % 1.93/2.16 (-. (c5_2 (a616) zenon_X40)) % 1.93/2.16 (zenon_X15 != zenon_X48) % 1.93/2.16 (c4_2 zenon_X10 zenon_X50) % 1.93/2.16 (c4_2 (a616) zenon_X42) % 1.93/2.16 (c1_2 zenon_X3 zenon_X17) % 1.93/2.16 (-. (c5_2 (a637) zenon_X24)) % 1.93/2.16 (-. (c5_2 zenon_X6 zenon_X16)) % 1.93/2.16 (zenon_X25 != zenon_X17) % 1.93/2.16 (zenon_X44 != zenon_X30) % 1.93/2.16 ((a597) != zenon_X50) % 1.93/2.16 (zenon_X20 != zenon_X32) % 1.93/2.16 (c4_2 zenon_X1 zenon_X34) % 1.93/2.16 (c2_2 (a637) zenon_X11) % 1.93/2.16 (-. (c2_2 (a613) zenon_X24)) % 1.93/2.16 (zenon_X32 != zenon_X48) % 1.93/2.16 (-. (c2_2 (a613) zenon_X13)) % 1.93/2.16 (-. (c5_2 zenon_X10 zenon_X32)) % 1.93/2.16 (zenon_X7 != (a594)) % 1.93/2.16 (-. (c5_2 zenon_X10 zenon_X40)) % 1.93/2.16 (zenon_X40 != zenon_X4) % 1.93/2.16 (-. (c1_2 (a613) zenon_X15)) % 1.93/2.16 (c5_2 zenon_X3 (a610)) % 1.93/2.16 (zenon_X19 != zenon_X50) % 1.93/2.16 (-. (c5_2 zenon_X1 zenon_X46)) % 1.93/2.16 (c4_2 (a637) zenon_X20) % 1.93/2.16 (c5_2 zenon_X3 zenon_X13) % 1.93/2.16 (c5_2 zenon_X3 (a636)) % 1.93/2.16 (zenon_X38 != (a610)) % 1.93/2.16 (c4_2 zenon_X3 (a639)) % 1.93/2.16 (c1_2 zenon_X3 zenon_X19) % 1.93/2.16 (-. (c5_1 zenon_X1)) % 1.93/2.16 (c4_2 (a616) zenon_X38) % 1.93/2.16 (c1_2 (a613) zenon_X40) % 1.93/2.16 (c1_2 (a616) zenon_X48) % 1.93/2.16 (-. (c1_2 (a637) zenon_X20)) % 1.93/2.16 (c4_2 zenon_X3 (a597)) % 1.93/2.16 ((a636) != (a614)) % 1.93/2.16 (c4_2 zenon_X10 zenon_X32) % 1.93/2.16 (c2_2 (a637) zenon_X18) % 1.93/2.16 (-. (c5_2 (a637) zenon_X26)) % 1.93/2.16 (c2_2 zenon_X10 zenon_X31) % 1.93/2.16 (-. (c2_2 (a613) zenon_X26)) % 1.93/2.16 (c1_2 (a613) zenon_X11) % 1.93/2.16 (zenon_X25 != zenon_X23) % 1.93/2.16 (c1_2 zenon_X3 zenon_X15) % 1.93/2.16 (-. (c1_2 zenon_X3 (a639))) % 1.93/2.16 ((a587) != zenon_X3) % 1.93/2.16 (c2_2 (a616) zenon_X48) % 1.93/2.16 (zenon_X11 != zenon_X33) % 1.93/2.16 (zenon_X44 != zenon_X11) % 1.93/2.16 (zenon_X30 != zenon_X31) % 1.93/2.16 (zenon_X34 != (a636)) % 1.93/2.16 (c1_2 (a613) (a638)) % 1.93/2.16 (c2_2 (a613) zenon_X40) % 1.93/2.16 (zenon_X44 != (a597)) % 1.93/2.16 (-. (c4_2 (a596) (a598))) % 1.93/2.16 (-. (c5_2 zenon_X6 zenon_X19)) % 1.93/2.16 (zenon_X20 != zenon_X40) % 1.93/2.16 (-. (c5_2 (a616) zenon_X31)) % 1.93/2.16 (c2_2 (a637) zenon_X32) % 1.93/2.16 (c2_2 (a637) (a597)) % 1.93/2.16 ((a598) != zenon_X18) % 1.93/2.16 (-. (c5_2 (a616) (a614))) % 1.93/2.16 (zenon_X32 != zenon_X19) % 1.93/2.16 (c5_2 (a613) zenon_X30) % 1.93/2.16 (ndr1_0) % 1.93/2.16 (-. (c5_2 zenon_X1 zenon_X50)) % 1.93/2.16 (zenon_X16 != zenon_X15) % 1.93/2.16 (-. (c5_2 (a637) zenon_X17)) % 1.93/2.16 ((a636) != zenon_X16) % 1.93/2.16 (zenon_X20 != zenon_X4) % 1.93/2.16 (zenon_X24 != zenon_X26) % 1.93/2.16 (c1_1 zenon_X1) % 1.93/2.16 (c4_2 (a594) zenon_X17) % 1.93/2.16 (c1_2 zenon_X6 zenon_X4) % 1.93/2.16 (zenon_X20 != zenon_X26) % 1.93/2.16 (c1_2 (a613) zenon_X38) % 1.93/2.16 ((a613) != (a637)) % 1.93/2.16 (c5_2 (a594) zenon_X5) % 1.93/2.16 (zenon_X48 != zenon_X42) % 1.93/2.16 (zenon_X6 != zenon_X12) % 1.93/2.16 (c2_2 (a616) zenon_X20) % 1.93/2.16 ((a616) != zenon_X12) % 1.93/2.16 (-. (c5_2 zenon_X10 zenon_X17)) % 1.93/2.16 (-. (c3_1 zenon_X10)) % 1.93/2.16 (-. (c5_2 zenon_X10 (a638))) % 1.93/2.16 (c1_2 (a616) zenon_X50) % 1.93/2.16 (c5_2 (a594) zenon_X16) % 1.93/2.16 (zenon_X13 != zenon_X50) % 1.93/2.16 (c2_2 (a637) zenon_X38) % 1.93/2.16 (ndr1_1 zenon_X7) % 1.93/2.16 (zenon_X40 != zenon_X14) % 1.93/2.16 ((a638) != (a610)) % 1.93/2.16 (zenon_X20 != zenon_X17) % 1.93/2.16 (-. (c3_2 zenon_X7 (a636))) % 1.93/2.16 ((a638) != zenon_X25) % 1.93/2.16 (zenon_X30 != zenon_X16) % 1.93/2.16 (c5_2 zenon_X6 zenon_X48) % 1.93/2.16 (c4_2 (a616) (a598)) % 1.93/2.16 (c5_2 zenon_X1 zenon_X38) % 1.93/2.16 (zenon_X44 != zenon_X25) % 1.93/2.16 (zenon_X15 != zenon_X46) % 1.93/2.16 (-. (c5_2 zenon_X10 (a639))) % 1.93/2.16 (c2_2 zenon_X1 zenon_X14) % 1.93/2.16 (zenon_X20 != zenon_X5) % 1.93/2.16 ((a613) != (a594)) % 1.93/2.16 (c2_2 zenon_X1 zenon_X18) % 1.93/2.16 (zenon_X11 != zenon_X34) % 1.93/2.16 (c5_2 (a616) (a638)) % 1.93/2.16 (-. (c3_1 zenon_X1)) % 1.93/2.16 (c1_2 zenon_X3 zenon_X24) % 1.93/2.16 (zenon_X20 != zenon_X25) % 1.93/2.16 (c1_2 zenon_X1 zenon_X13) % 1.93/2.16 (c5_2 zenon_X1 zenon_X32) % 1.93/2.16 (c2_2 zenon_X3 zenon_X44) % 1.93/2.16 (zenon_X50 != zenon_X42) % 1.93/2.16 (c5_1 zenon_X0) % 1.93/2.16 (zenon_X40 != (a597)) % 1.93/2.16 (-. (c5_2 zenon_X3 zenon_X4)) % 1.93/2.16 (zenon_X15 != (a597)) % 1.93/2.16 (-. (c5_2 zenon_X1 (a598))) % 1.93/2.16 (c5_2 (a594) (a638)) % 1.93/2.16 (-. (c5_2 (a613) zenon_X16)) % 1.93/2.16 (zenon_X34 != zenon_X50) % 1.93/2.16 (-. (c5_2 zenon_X10 (a597))) % 1.93/2.16 (zenon_X25 != zenon_X34) % 1.93/2.16 (-. (c5_1 zenon_X12)) % 1.93/2.16 (-. (c5_2 (a613) zenon_X23)) % 1.93/2.16 (c4_2 (a637) zenon_X14) % 1.93/2.16 (zenon_X15 != zenon_X31) % 1.93/2.16 (zenon_X0 != zenon_X6) % 1.93/2.16 (zenon_X28 != zenon_X16) % 1.93/2.16 (c2_2 zenon_X3 (a610)) % 1.93/2.16 (zenon_X26 != zenon_X46) % 1.93/2.16 (zenon_X31 != zenon_X42) % 1.93/2.16 (c1_2 (a613) zenon_X48) % 1.93/2.16 ((a610) != zenon_X20) % 1.93/2.16 (zenon_X25 != zenon_X26) % 1.93/2.16 (zenon_X16 != zenon_X14) % 1.93/2.16 (c5_0) % 1.93/2.16 (c5_2 zenon_X10 (a598)) % 1.93/2.16 ((a613) != zenon_X6) % 1.93/2.16 (zenon_X38 != zenon_X25) % 1.93/2.16 (c2_2 (a637) (a638)) % 1.93/2.16 (-. (c5_2 (a613) zenon_X44)) % 1.93/2.16 (c4_2 zenon_X1 (a610)) % 1.93/2.16 (zenon_X0 != (a594)) % 1.93/2.16 (c4_2 (a613) zenon_X15) % 1.93/2.16 (-. (c5_2 (a616) zenon_X23)) % 1.93/2.16 (c5_2 (a616) zenon_X44) % 1.93/2.16 (c2_2 (a613) zenon_X14) % 1.93/2.16 ((a638) != zenon_X4) % 1.93/2.16 ((a597) != zenon_X16) % 1.93/2.16 (zenon_X48 != zenon_X26) % 1.93/2.16 ((a613) != zenon_X12) % 1.93/2.16 (zenon_X4 != zenon_X11) % 1.93/2.16 (c4_2 (a616) zenon_X30) % 1.93/2.16 ((a597) != zenon_X4) % 1.93/2.16 (c1_2 zenon_X3 zenon_X26) % 1.93/2.16 (zenon_X14 != (a597)) % 1.93/2.16 (zenon_X10 != zenon_X3) % 1.93/2.16 (-. (c5_2 zenon_X6 zenon_X33)) % 1.93/2.16 (-. (c5_2 (a616) (a598))) % 1.93/2.16 ((a639) != zenon_X11) % 1.93/2.16 (c1_2 (a594) zenon_X19) % 1.93/2.16 (zenon_X24 != zenon_X33) % 1.93/2.16 (zenon_X33 != zenon_X25) % 1.93/2.16 ((a638) != zenon_X17) % 1.93/2.16 ((a616) != zenon_X10) % 1.93/2.16 (zenon_X11 != zenon_X26) % 1.93/2.16 (-. (c5_2 (a613) zenon_X13)) % 1.93/2.16 (-. (c5_2 zenon_X6 zenon_X23)) % 1.93/2.16 (-. (c2_2 (a613) zenon_X23)) % 1.93/2.16 (c5_2 (a633) zenon_X5) % 1.93/2.16 (c5_2 (a633) zenon_X50) % 1.93/2.16 (ndr1_1 (a594)) % 1.93/2.16 (-. (c5_2 zenon_X6 zenon_X24)) % 1.93/2.16 (-. (c3_0)) % 1.93/2.16 (c4_2 zenon_X6 zenon_X38) % 1.93/2.16 (zenon_X40 != zenon_X42) % 1.93/2.16 (-. (c1_2 (a613) zenon_X44)) % 1.93/2.16 (c2_2 (a613) zenon_X34) % 1.93/2.16 (-. (c1_2 zenon_X3 (a638))) % 1.93/2.16 ((a597) != zenon_X28) % 1.93/2.16 (-. (c5_2 zenon_X3 zenon_X16)) % 1.93/2.16 (zenon_X40 != zenon_X15) % 1.93/2.16 (c4_2 zenon_X6 zenon_X18) % 1.93/2.16 (zenon_X44 != zenon_X50) % 1.93/2.16 (c1_2 zenon_X3 zenon_X5) % 1.93/2.16 (zenon_X50 != zenon_X16) % 1.93/2.16 (-. (c5_2 (a594) zenon_X46)) % 1.93/2.16 (ndr1_1 (a587)) % 1.93/2.16 ((a639) != zenon_X17) % 1.93/2.16 (zenon_X30 != zenon_X5) % 1.93/2.16 (-. (c5_2 zenon_X6 (a597))) % 1.93/2.16 ((a597) != zenon_X33) % 1.93/2.16 (c4_2 (a613) zenon_X17) % 1.93/2.16 (zenon_X7 != zenon_X3) % 1.93/2.16 (-. (c5_2 (a637) zenon_X40)) % 1.93/2.16 (-. (c5_2 zenon_X6 (a638))) % 1.93/2.16 ((a598) != zenon_X14) % 1.93/2.16 (c4_2 (a613) zenon_X50) % 1.93/2.16 (zenon_X23 != zenon_X5) % 1.93/2.16 (-. (c5_2 zenon_X10 zenon_X28)) % 1.93/2.16 (-. (c1_1 (a596))) % 1.93/2.16 (-. (c5_2 zenon_X10 zenon_X48)) % 1.93/2.16 (-. (c5_2 zenon_X6 zenon_X46)) % 1.93/2.16 ((a638) != zenon_X34) % 1.93/2.16 (c2_2 (a637) zenon_X19) % 1.93/2.16 (zenon_X44 != zenon_X42) % 1.93/2.16 (c5_2 zenon_X1 zenon_X25) % 1.93/2.16 (-. (c5_2 (a616) zenon_X15)) % 1.93/2.16 (zenon_X14 != (a638)) % 1.93/2.16 (c4_2 zenon_X1 zenon_X5) % 1.93/2.16 (c4_2 (a616) zenon_X31) % 1.93/2.16 (c4_2 zenon_X6 zenon_X33) % 1.93/2.16 (zenon_X14 != zenon_X11) % 1.93/2.16 (zenon_X3 != zenon_X6) % 1.93/2.16 (c5_2 (a616) (a639)) % 1.93/2.16 (zenon_X31 != zenon_X50) % 1.93/2.16 (zenon_X44 != zenon_X13) % 1.93/2.16 (zenon_X18 != (a597)) % 1.93/2.16 (c5_2 (a594) zenon_X20) % 1.93/2.16 (-. (c5_2 zenon_X6 zenon_X38)) % 1.93/2.16 (zenon_X13 != zenon_X11) % 1.93/2.16 ((a597) != zenon_X24) % 1.93/2.16 (-. (c5_2 zenon_X6 zenon_X14)) % 1.93/2.16 (c1_2 (a613) (a610)) % 1.93/2.16 (zenon_X13 != zenon_X17) % 1.93/2.16 (zenon_X5 != zenon_X34) % 1.93/2.16 (-. (c5_2 (a613) zenon_X25)) % 1.93/2.16 (zenon_X11 != zenon_X46) % 1.93/2.16 (c5_2 zenon_X6 zenon_X4) % 1.93/2.16 ((a610) != zenon_X24) % 1.93/2.16 ((a598) != (a610)) % 1.93/2.16 (c5_2 zenon_X1 (a638)) % 1.93/2.16 (c5_2 (a633) zenon_X19) % 1.93/2.16 (c5_2 zenon_X1 zenon_X48) % 1.93/2.16 ((a638) != (a639)) % 1.93/2.16 (zenon_X18 != zenon_X24) % 1.93/2.16 (c5_2 (a633) zenon_X30) % 1.93/2.16 (c3_1 (a587)) % 1.93/2.16 (-. (c5_2 zenon_X7 zenon_X37)) % 1.93/2.16 (zenon_X18 != (a639)) % 1.93/2.16 (zenon_X4 != zenon_X25) % 1.93/2.16 ((a610) != zenon_X5) % 1.93/2.16 (c2_2 zenon_X3 zenon_X40) % 1.93/2.16 (zenon_X48 != zenon_X4) % 1.93/2.16 (c4_2 (a594) (a610)) % 1.93/2.16 (c4_2 (a616) (a614)) % 1.93/2.16 (c5_2 (a616) zenon_X50) % 1.93/2.16 (c4_2 (a613) zenon_X13) % 1.93/2.16 (zenon_X28 != zenon_X42) % 1.93/2.16 (-. (c2_2 (a596) (a597))) % 1.93/2.16 (zenon_X14 != zenon_X13) % 1.93/2.16 (c4_2 (a594) zenon_X33) % 1.93/2.16 ((a633) != zenon_X12) % 1.93/2.16 (zenon_X6 != (a596)) % 1.93/2.16 (-. (c5_2 zenon_X0 (a597))) % 1.93/2.16 (-. (c3_1 zenon_X3)) % 1.93/2.16 ((a610) != zenon_X25) % 1.93/2.16 (c4_2 (a594) (a597)) % 1.93/2.16 (ndr1_1 (a616)) % 1.93/2.16 (zenon_X23 != (a638)) % 1.93/2.16 ((a639) != zenon_X48) % 1.93/2.16 (ndr1_1 zenon_X8) % 1.93/2.16 (zenon_X18 != zenon_X26) % 1.93/2.16 (zenon_X44 != zenon_X15) % 1.93/2.16 ((a594) != zenon_X10) % 1.93/2.16 ((a639) != zenon_X50) % 1.93/2.16 (zenon_X1 != (a637)) % 1.93/2.16 (c1_2 (a594) zenon_X11) % 1.93/2.16 (c5_2 (a596) (a597)) % 1.93/2.16 (zenon_X32 != zenon_X5) % 1.93/2.16 (c5_2 (a633) zenon_X32) % 1.93/2.16 (c5_2 (a613) (a636)) % 1.93/2.16 (zenon_X4 != zenon_X5) % 1.93/2.16 (zenon_X13 != zenon_X24) % 1.93/2.16 (c4_2 (a594) zenon_X31) % 1.93/2.16 (zenon_X30 != zenon_X18) % 1.93/2.16 (c2_2 (a613) zenon_X33) % 1.93/2.16 (c2_2 (a613) zenon_X30) % 1.93/2.16 (zenon_X15 != zenon_X33) % 1.93/2.16 (zenon_X32 != (a610)) % 1.93/2.16 (c5_2 (a594) zenon_X24) % 1.93/2.16 (c5_2 zenon_X3 zenon_X33) % 1.93/2.16 (c2_2 zenon_X8 (a636)) % 1.93/2.16 (zenon_X14 != zenon_X46) % 1.93/2.16 (zenon_X44 != zenon_X34) % 1.93/2.16 (c5_2 (a633) (a597)) % 1.93/2.16 (zenon_X26 != zenon_X34) % 1.93/2.16 (c4_2 (a637) zenon_X16) % 1.93/2.16 (c4_2 (a616) zenon_X5) % 1.93/2.16 (c3_1 zenon_X0) % 1.93/2.16 (zenon_X16 != (a614)) % 1.93/2.16 (c2_2 zenon_X1 zenon_X28) % 1.93/2.16 ((a638) != zenon_X26) % 1.93/2.16 ((a598) != zenon_X25) % 1.93/2.16 (c4_2 (a613) zenon_X31) % 1.93/2.16 (c5_2 (a613) zenon_X33) % 1.93/2.16 (zenon_X40 != zenon_X17) % 1.93/2.16 (c1_2 zenon_X3 zenon_X23) % 1.93/2.16 (c5_2 zenon_X3 zenon_X17) % 1.93/2.16 (c2_2 zenon_X3 zenon_X38) % 1.93/2.16 (c2_2 (a637) zenon_X50) % 1.93/2.16 (zenon_X20 != zenon_X46) % 1.93/2.16 (c5_2 (a613) (a614)) % 1.93/2.16 ((a639) != zenon_X20) % 1.93/2.16 ((a587) != zenon_X1) % 1.93/2.16 ((a616) != zenon_X6) % 1.93/2.16 (zenon_X24 != (a614)) % 1.93/2.16 (c4_2 (a613) zenon_X42) % 1.93/2.16 (zenon_X0 != (a613)) % 1.93/2.16 (zenon_X28 != zenon_X26) % 1.93/2.16 (zenon_X11 != zenon_X31) % 1.93/2.16 (c5_2 zenon_X10 zenon_X31) % 1.93/2.16 (c1_2 (a616) (a639)) % 1.93/2.16 (c1_2 (a616) (a597)) % 1.93/2.16 (zenon_X15 != zenon_X34) % 1.93/2.16 (c4_2 zenon_X6 zenon_X46) % 1.93/2.16 (zenon_X38 != zenon_X11) % 1.93/2.16 (c1_2 (a613) (a614)) % 1.93/2.16 (c2_2 zenon_X1 zenon_X30) % 1.93/2.16 (c2_2 (a637) zenon_X48) % 1.93/2.16 (zenon_X30 != zenon_X46) % 1.93/2.16 (-. (c5_2 zenon_X10 zenon_X15)) % 1.93/2.16 (zenon_X18 != zenon_X11) % 1.93/2.16 (zenon_X38 != zenon_X16) % 1.93/2.16 (zenon_X38 != zenon_X5) % 1.93/2.16 (c1_2 zenon_X1 zenon_X17) % 1.93/2.16 ((a597) != zenon_X23) % 1.93/2.16 (-. (c3_2 (a616) (a636))) % 1.93/2.16 (zenon_X17 != zenon_X5) % 1.93/2.16 (c4_2 zenon_X10 zenon_X28) % 1.93/2.16 (c4_2 (a637) zenon_X30) % 1.93/2.16 (c4_2 zenon_X6 zenon_X32) % 1.93/2.16 ((a598) != zenon_X16) % 1.93/2.16 (zenon_X0 != zenon_X10) % 1.93/2.16 (c5_2 (a633) zenon_X4) % 1.93/2.16 (-. (c5_2 (a616) zenon_X5)) % 1.93/2.16 ((a610) != zenon_X18) % 1.93/2.16 (-. (c3_2 zenon_X10 (a636))) % 1.93/2.16 (c1_2 (a613) zenon_X46) % 1.93/2.16 (c4_2 (a613) zenon_X18) % 1.93/2.16 (zenon_X7 != (a613)) % 1.93/2.16 (c2_2 zenon_X1 zenon_X11) % 1.93/2.16 (-. (c5_2 (a594) (a639))) % 1.93/2.16 (zenon_X25 != zenon_X46) % 1.93/2.16 ((a610) != zenon_X31) % 1.93/2.16 ((a614) != (a639)) % 1.93/2.16 (c5_2 (a594) zenon_X28) % 1.93/2.16 (c5_2 (a613) zenon_X11) % 1.93/2.16 (-. (c5_2 zenon_X10 zenon_X16)) % 1.93/2.16 (-. (c5_2 zenon_X6 zenon_X5)) % 1.93/2.16 (zenon_X28 != (a638)) % 1.93/2.16 (zenon_X40 != (a636)) % 1.93/2.16 (c4_2 (a613) zenon_X38) % 1.93/2.16 (c5_2 zenon_X1 zenon_X11) % 1.93/2.16 (zenon_X46 != zenon_X50) % 1.93/2.16 ((a610) != zenon_X33) % 1.93/2.16 (zenon_X5 != zenon_X48) % 1.93/2.16 (c5_1 (a633)) % 1.93/2.16 (c5_2 zenon_X1 zenon_X28) % 1.93/2.16 (zenon_X23 != zenon_X50) % 1.93/2.16 (ndr1_1 (a637)) % 1.93/2.16 (-. (c1_2 zenon_X3 (a597))) % 1.93/2.16 ((a638) != zenon_X15) % 1.93/2.16 (c1_2 zenon_X1 zenon_X30) % 1.93/2.16 (zenon_X40 != zenon_X31) % 1.93/2.16 (zenon_X46 != zenon_X16) % 1.93/2.16 (-. (c5_2 zenon_X0 zenon_X39)) % 1.93/2.16 ((a636) != zenon_X14) % 1.93/2.16 ((a598) != zenon_X50) % 1.93/2.16 ((a597) != zenon_X34) % 1.93/2.16 (c1_2 (a616) (a638)) % 1.93/2.16 (c4_2 zenon_X10 zenon_X24) % 1.93/2.16 (zenon_X44 != zenon_X5) % 1.93/2.16 (zenon_X40 != zenon_X24) % 1.93/2.16 (c4_2 (a616) (a610)) % 1.93/2.16 (zenon_X28 != zenon_X46) % 1.93/2.16 (zenon_X32 != zenon_X34) % 1.93/2.16 (zenon_X24 != zenon_X42) % 1.93/2.16 (c1_1 zenon_X6) % 1.93/2.16 (c4_2 zenon_X6 zenon_X19) % 1.93/2.16 (c4_2 zenon_X10 zenon_X46) % 1.93/2.16 (zenon_X18 != zenon_X50) % 1.93/2.16 ((a636) != zenon_X18) % 1.93/2.16 (zenon_X30 != zenon_X11) % 1.93/2.16 (c4_2 (a616) (a636)) % 1.93/2.16 ((a636) != zenon_X42) % 1.93/2.16 (c1_2 zenon_X1 (a597)) % 1.93/2.16 (zenon_X26 != zenon_X19) % 1.93/2.16 (zenon_X14 != zenon_X42) % 1.93/2.16 (-. (c3_2 zenon_X8 (a636))) % 1.93/2.16 (zenon_X40 != zenon_X5) % 1.93/2.16 (c2_2 (a637) (a636)) % 1.93/2.16 ((a636) != zenon_X32) % 1.93/2.16 ((a597) != zenon_X19) % 1.93/2.16 (zenon_X31 != zenon_X17) % 1.93/2.16 (c4_2 zenon_X6 (a610)) % 1.93/2.16 (c4_2 (a594) zenon_X48) % 1.93/2.16 (c1_2 zenon_X1 zenon_X15) % 1.93/2.16 (c1_2 zenon_X3 zenon_X38) % 1.93/2.16 (zenon_X44 != zenon_X4) % 1.93/2.16 (-. (c3_2 zenon_X1 (a636))) % 1.93/2.16 (zenon_X40 != zenon_X26) % 1.93/2.16 (zenon_X32 != (a597)) % 1.93/2.16 ((a597) != (a610)) % 1.93/2.16 (zenon_X25 != zenon_X42) % 1.93/2.16 (c1_2 (a613) zenon_X30) % 1.93/2.16 (zenon_X23 != zenon_X48) % 1.93/2.16 (c1_1 zenon_X3) % 1.93/2.16 (c2_2 zenon_X6 zenon_X4) % 1.93/2.16 (c1_2 zenon_X1 (a638)) % 1.93/2.16 (zenon_X44 != zenon_X33) % 1.93/2.16 ((a598) != zenon_X17) % 1.93/2.16 (c2_2 (a613) zenon_X28) % 1.93/2.16 (c2_2 zenon_X1 zenon_X15) % 1.93/2.16 (c4_2 zenon_X6 (a636)) % 1.93/2.16 (c4_2 (a616) zenon_X19) % 1.93/2.16 (zenon_X16 != zenon_X17) % 1.93/2.16 (zenon_X44 != zenon_X28) % 1.93/2.16 (zenon_X14 != (a639)) % 1.93/2.16 (c4_2 zenon_X3 zenon_X40) % 1.93/2.16 (c5_2 zenon_X3 zenon_X40) % 1.93/2.16 (c5_1 zenon_X7) % 1.93/2.16 (zenon_X38 != zenon_X14) % 1.93/2.16 (zenon_X32 != (a614)) % 1.93/2.16 ((a614) != (a638)) % 1.93/2.16 ((a638) != (a636)) % 1.93/2.16 (c1_2 (a594) zenon_X13) % 1.93/2.16 (-. (c5_2 zenon_X6 zenon_X18)) % 1.93/2.16 (c5_2 zenon_X1 zenon_X15) % 1.93/2.16 (c1_2 (a616) zenon_X28) % 1.93/2.16 (c5_2 (a633) zenon_X38) % 1.93/2.16 (-. (c5_2 zenon_X10 zenon_X42)) % 1.93/2.16 (c4_2 zenon_X3 zenon_X20) % 1.93/2.16 ((a636) != zenon_X9) % 1.93/2.16 (ndr1_1 (a613)) % 1.93/2.16 ((a638) != zenon_X50) % 1.93/2.16 (zenon_X18 != zenon_X25) % 1.93/2.16 (zenon_X20 != zenon_X31) % 1.93/2.16 (c4_2 (a613) zenon_X20) % 1.93/2.16 (-. (c5_2 (a594) zenon_X32)) % 1.93/2.16 ((a610) != zenon_X42) % 1.93/2.16 (zenon_X1 != zenon_X3) % 1.93/2.16 (ndr1_1 zenon_X3) % 1.93/2.16 (zenon_X13 != zenon_X25) % 1.93/2.16 (c1_2 zenon_X1 (a614)) % 1.93/2.16 (c3_2 (a637) (a610)) % 1.93/2.16 (c5_2 (a594) zenon_X30) % 1.93/2.16 (c4_2 zenon_X6 (a597)) % 1.93/2.16 (-. (c5_2 (a637) zenon_X42)) % 1.93/2.16 ((a598) != zenon_X21) % 1.93/2.16 (zenon_X14 != zenon_X50) % 1.93/2.16 (zenon_X30 != zenon_X26) % 1.93/2.16 (c4_2 (a637) zenon_X4) % 1.93/2.16 (c1_2 (a613) (a597)) % 1.93/2.16 (c2_2 zenon_X3 zenon_X15) % 1.93/2.16 (c1_2 zenon_X1 zenon_X28) % 1.93/2.16 (c4_2 (a594) zenon_X34) % 1.93/2.16 (zenon_X19 != zenon_X34) % 1.93/2.16 (zenon_X14 != zenon_X25) % 1.93/2.16 (c2_2 zenon_X6 zenon_X44) % 1.93/2.16 ((a598) != zenon_X33) % 1.93/2.16 (c1_2 zenon_X1 zenon_X38) % 1.93/2.16 (zenon_X28 != zenon_X48) % 1.93/2.16 (c4_2 (a637) zenon_X42) % 1.93/2.16 (-. (c1_2 (a596) (a639))) % 1.93/2.16 (-. (c5_2 zenon_X1 (a610))) % 1.93/2.16 (c4_2 (a594) zenon_X46) % 1.93/2.16 (c5_2 (a637) zenon_X31) % 1.93/2.16 (c2_2 (a616) (a638)) % 1.93/2.16 ((a637) != zenon_X3) % 1.93/2.16 (c2_2 (a594) zenon_X16) % 1.93/2.16 (-. (c5_2 (a587) zenon_X36)) % 1.93/2.16 (c2_2 zenon_X3 zenon_X13) % 1.93/2.16 ((a610) != zenon_X23) % 1.93/2.16 (-. (c1_1 (a637))) % 1.93/2.16 ((a596) != zenon_X0) % 1.93/2.16 (zenon_X25 != zenon_X48) % 1.93/2.16 (zenon_X25 != zenon_X5) % 1.93/2.16 (zenon_X0 != zenon_X12) % 1.93/2.16 (zenon_X44 != zenon_X16) % 1.93/2.16 (c5_2 zenon_X3 zenon_X44) % 1.93/2.16 (zenon_X32 != zenon_X15) % 1.93/2.16 (c4_2 (a613) zenon_X24) % 1.93/2.16 (zenon_X38 != zenon_X17) % 1.93/2.16 (zenon_X7 != (a637)) % 1.93/2.16 (zenon_X28 != zenon_X19) % 1.93/2.16 ((a636) != (a639)) % 1.93/2.16 (zenon_X33 != zenon_X42) % 1.93/2.16 (zenon_X32 != zenon_X11) % 1.93/2.16 ((a638) != zenon_X20) % 1.93/2.16 (zenon_X3 != (a633)) % 1.93/2.16 (c2_2 zenon_X1 (a638)) % 1.93/2.16 (c1_2 zenon_X3 zenon_X14) % 1.93/2.16 ((a598) != zenon_X19) % 1.93/2.16 (c4_2 (a616) zenon_X15) % 1.93/2.16 ((a594) != (a633)) % 1.93/2.16 (zenon_X13 != zenon_X48) % 1.93/2.16 (c2_2 (a616) zenon_X50) % 1.93/2.16 (c5_2 (a613) (a597)) % 1.93/2.16 (-. (c3_2 (a613) (a614))) % 1.93/2.16 (c5_2 zenon_X6 zenon_X44) % 1.93/2.16 (c1_2 zenon_X3 zenon_X44) % 1.93/2.16 (zenon_X23 != zenon_X17) % 1.93/2.16 (c5_2 zenon_X3 (a597)) % 1.93/2.16 (zenon_X48 != zenon_X18) % 1.93/2.16 (-. (c5_2 zenon_X7 (a597))) % 1.93/2.16 (c1_2 zenon_X1 zenon_X48) % 1.93/2.16 (zenon_X18 != zenon_X34) % 1.93/2.16 (c4_2 zenon_X3 (a638)) % 1.93/2.16 (-. (ndr1_1 zenon_X12)) % 1.93/2.16 (c1_2 zenon_X6 zenon_X48) % 1.93/2.16 (c2_2 zenon_X3 zenon_X14) % 1.93/2.16 (zenon_X30 != zenon_X23) % 1.93/2.16 (c4_2 zenon_X1 zenon_X40) % 1.93/2.16 (zenon_X25 != zenon_X24) % 1.93/2.16 (c5_2 (a633) zenon_X48) % 1.93/2.16 (-. (c5_2 (a613) zenon_X50)) % 1.93/2.16 (-. (c5_2 (a613) zenon_X46)) % 1.93/2.16 (c2_2 zenon_X10 (a636)) % 1.93/2.16 ((a636) != zenon_X17) % 1.93/2.16 (c1_2 (a613) (a639)) % 1.93/2.16 (zenon_X31 != zenon_X34) % 1.93/2.16 (-. (c5_2 zenon_X10 zenon_X19)) % 1.93/2.16 (zenon_X18 != zenon_X5) % 1.93/2.16 (zenon_X40 != (a639)) % 1.93/2.16 (zenon_X24 != zenon_X46) % 1.93/2.16 (c2_2 (a637) zenon_X44) % 1.93/2.16 (zenon_X16 != zenon_X18) % 1.93/2.16 (zenon_X32 != zenon_X31) % 1.93/2.16 (c4_2 (a637) zenon_X26) % 1.93/2.16 ((a598) != zenon_X42) % 1.93/2.16 (-. (c1_2 zenon_X8 zenon_X51)) % 1.93/2.16 (zenon_X44 != zenon_X24) % 1.93/2.16 (zenon_X11 != zenon_X5) % 1.93/2.16 (zenon_X38 != zenon_X24) % 1.93/2.16 (-. (c5_2 (a613) zenon_X19)) % 1.93/2.16 ((a610) != zenon_X40) % 1.93/2.16 ((a613) != zenon_X10) % 1.93/2.16 (c4_2 zenon_X10 zenon_X34) % 1.93/2.16 (c4_2 zenon_X3 (a614)) % 1.93/2.16 ((a637) != zenon_X12) % 1.93/2.16 ((a614) != zenon_X9) % 1.93/2.16 ((a616) != (a637)) % 1.93/2.16 (zenon_X30 != zenon_X50) % 1.93/2.16 (c2_2 zenon_X1 (a597)) % 1.93/2.16 (zenon_X11 != zenon_X16) % 1.93/2.16 (c5_2 (a594) zenon_X25) % 1.93/2.16 ((a638) != zenon_X9) % 1.93/2.16 (-. (c5_2 zenon_X6 zenon_X28)) % 1.93/2.16 (zenon_X15 != zenon_X11) % 1.93/2.16 ((a598) != zenon_X51) % 1.93/2.16 (c4_2 (a613) zenon_X5) % 1.93/2.16 (c2_2 (a594) zenon_X25) % 1.93/2.16 (zenon_X26 != zenon_X5) % 1.93/2.16 (c4_2 (a616) zenon_X23) % 1.93/2.16 (c4_2 zenon_X10 (a597)) % 1.93/2.16 (-. (c5_2 (a616) zenon_X32)) % 1.93/2.16 (-. (c3_1 zenon_X6)) % 1.93/2.16 (zenon_X4 != zenon_X31) % 1.93/2.16 (-. (c5_2 (a637) zenon_X30)) % 1.93/2.16 (c4_2 zenon_X6 zenon_X23) % 1.93/2.16 (zenon_X44 != zenon_X23) % 1.93/2.16 (-. (c5_2 (a594) zenon_X48)) % 1.93/2.16 (c1_2 zenon_X1 zenon_X31) % 1.93/2.16 (c1_2 (a594) zenon_X20) % 1.93/2.16 (c2_2 (a613) (a598)) % 1.93/2.16 (c2_2 (a594) zenon_X19) % 1.93/2.16 (c2_2 zenon_X3 zenon_X46) % 1.93/2.16 ((a614) != zenon_X5) % 1.93/2.16 (zenon_X40 != zenon_X23) % 1.93/2.16 (zenon_X15 != zenon_X5) % 1.93/2.16 (c4_2 zenon_X6 zenon_X50) % 1.93/2.16 (zenon_X24 != zenon_X23) % 1.93/2.16 (c5_2 zenon_X1 zenon_X20) % 1.93/2.16 (zenon_X38 != zenon_X26) % 1.93/2.16 (c4_2 zenon_X10 zenon_X14) % 1.93/2.16 (zenon_X4 != zenon_X23) % 1.93/2.16 (c2_2 (a594) zenon_X23) % 1.93/2.16 (zenon_X40 != zenon_X16) % 1.93/2.16 (zenon_X8 != zenon_X3) % 1.93/2.16 (zenon_X8 != zenon_X12) % 1.93/2.16 (c5_2 (a633) zenon_X34) % 1.93/2.16 (-. (c5_2 zenon_X6 zenon_X42)) % 1.93/2.16 (c5_2 zenon_X3 zenon_X38) % 1.93/2.16 (-. (c1_2 (a596) zenon_X21)) % 1.93/2.16 (c4_2 zenon_X6 (a638)) % 1.93/2.16 (-. (c5_2 zenon_X1 zenon_X40)) % 1.93/2.16 (zenon_X14 != zenon_X15) % 1.93/2.16 (c1_2 zenon_X10 (a598)) % 1.93/2.16 (zenon_X4 != zenon_X28) % 1.93/2.16 (c1_2 zenon_X3 zenon_X18) % 1.93/2.16 (zenon_X4 != zenon_X19) % 1.93/2.16 ((a597) != zenon_X20) % 1.93/2.16 (zenon_X24 != zenon_X17) % 1.93/2.16 (zenon_X34 != zenon_X42) % 1.93/2.16 (c4_2 (a616) zenon_X18) % 1.93/2.16 (c2_2 zenon_X1 zenon_X42) % 1.93/2.16 (zenon_X40 != (a598)) % 1.93/2.16 (c5_2 (a633) (a636)) % 1.93/2.16 (zenon_X13 != zenon_X19) % 1.93/2.16 (zenon_X32 != zenon_X23) % 1.93/2.16 (-. (c5_2 (a594) zenon_X33)) % 1.93/2.16 (zenon_X11 != (a636)) % 1.93/2.16 (-. (c5_2 zenon_X6 (a610))) % 1.93/2.16 (-. (c3_2 zenon_X3 (a636))) % 1.93/2.16 (zenon_X5 != zenon_X50) % 1.93/2.16 (zenon_X14 != zenon_X19) % 1.93/2.16 (-. (c5_2 zenon_X6 zenon_X11)) % 1.93/2.16 (c5_2 (a594) zenon_X13) % 1.93/2.16 (c2_2 (a637) (a610)) % 1.93/2.16 (zenon_X30 != zenon_X19) % 1.93/2.16 (-. (c1_2 (a596) (a636))) % 1.93/2.16 (-. (c5_2 (a616) zenon_X33)) % 1.93/2.16 ((a614) != zenon_X48) % 1.93/2.16 (zenon_X48 != zenon_X46) % 1.93/2.16 (zenon_X14 != (a614)) % 1.93/2.16 (c4_2 zenon_X3 (a598)) % 1.93/2.16 (zenon_X20 != zenon_X15) % 1.93/2.16 (zenon_X32 != zenon_X33) % 1.93/2.16 ((a614) != zenon_X42) % 1.93/2.16 ((a598) != zenon_X4) % 1.93/2.16 (-. (c2_1 (a637))) % 1.93/2.16 (zenon_X7 != zenon_X1) % 1.93/2.16 ((a639) != zenon_X4) % 1.93/2.16 (zenon_X32 != zenon_X26) % 1.93/2.16 (-. (c5_2 (a637) zenon_X13)) % 1.93/2.16 ((a610) != zenon_X15) % 1.93/2.16 (zenon_X23 != (a614)) % 1.93/2.16 (c2_2 (a594) zenon_X18) % 1.93/2.16 (-. (c2_2 (a613) zenon_X44)) % 1.93/2.16 (zenon_X1 != zenon_X12) % 1.93/2.16 (zenon_X13 != zenon_X28) % 1.93/2.16 (-. (c5_2 zenon_X10 zenon_X25)) % 1.93/2.16 (c4_2 zenon_X3 zenon_X4) % 1.93/2.16 (c2_2 zenon_X1 zenon_X44) % 1.93/2.16 (-. (c5_2 zenon_X3 zenon_X50)) % 1.93/2.16 (zenon_X38 != (a614)) % 1.93/2.16 ((a610) != zenon_X48) % 1.93/2.16 ((a614) != (a597)) % 1.93/2.16 (-. (c5_2 (a616) zenon_X14)) % 1.93/2.16 (c4_2 zenon_X6 zenon_X31) % 1.93/2.16 (c2_2 zenon_X10 (a598)) % 1.93/2.16 (c5_2 zenon_X3 zenon_X25) % 1.93/2.16 (c5_2 (a633) (a610)) % 1.93/2.16 (c4_2 (a613) (a638)) % 1.93/2.16 (zenon_X40 != zenon_X19) % 1.93/2.16 (-. (c5_2 (a613) (a638))) % 1.93/2.16 (c2_2 (a594) zenon_X14) % 1.93/2.16 (-. (c5_2 (a594) (a614))) % 1.93/2.16 (c4_2 (a616) zenon_X25) % 1.93/2.16 (zenon_X33 != zenon_X31) % 1.93/2.16 (zenon_X34 != zenon_X33) % 1.93/2.16 (zenon_X38 != zenon_X15) % 1.93/2.16 (-. (c5_2 (a616) (a636))) % 1.93/2.16 ((a598) != zenon_X5) % 1.93/2.16 ((a610) != zenon_X4) % 1.93/2.16 (zenon_X15 != zenon_X17) % 1.93/2.16 (c1_2 zenon_X1 zenon_X11) % 1.93/2.16 ((a636) != zenon_X48) % 1.93/2.16 (c2_1 (a587)) % 1.93/2.16 (-. (c1_2 zenon_X3 (a610))) % 1.93/2.16 (zenon_X30 != zenon_X32) % 1.93/2.16 (-. (c4_2 (a613) (a614))) % 1.93/2.16 ((a598) != zenon_X24) % 1.93/2.16 (c5_2 (a613) zenon_X40) % 1.93/2.16 (zenon_X11 != zenon_X48) % 1.93/2.16 (c2_2 (a616) zenon_X44) % 1.93/2.16 (zenon_X11 != zenon_X42) % 1.93/2.16 (-. (c5_1 (a613))) % 1.93/2.16 (c1_2 (a616) zenon_X4) % 1.93/2.16 (zenon_X16 != zenon_X31) % 1.93/2.16 ((a598) != (a639)) % 1.93/2.16 (c5_2 zenon_X10 (a636)) % 1.93/2.16 (c2_2 (a616) zenon_X11) % 1.93/2.16 (zenon_X4 != zenon_X32) % 1.93/2.16 (zenon_X32 != zenon_X17) % 1.93/2.16 (-. (c3_2 zenon_X0 (a636))) % 1.93/2.16 (zenon_X48 != zenon_X14) % 1.93/2.16 ((a596) != zenon_X7) % 1.93/2.16 (-. (c1_2 zenon_X8 (a598))) % 1.93/2.16 (-. (c1_2 (a613) zenon_X19)) % 1.93/2.16 (c5_2 zenon_X3 zenon_X28) % 1.93/2.16 (zenon_X11 != (a610)) % 1.93/2.16 (zenon_X13 != zenon_X26) % 1.93/2.16 (zenon_X38 != (a639)) % 1.93/2.16 (c4_2 zenon_X1 zenon_X50) % 1.93/2.16 (-. (c5_2 (a594) zenon_X31)) % 1.93/2.16 (c2_2 zenon_X7 (a636)) % 1.93/2.16 (c2_2 zenon_X3 zenon_X19) % 1.93/2.16 (-. (c5_2 zenon_X1 zenon_X33)) % 1.93/2.16 ((a594) != (a596)) % 1.93/2.16 (c2_2 (a594) zenon_X26) % 1.93/2.16 ((a598) != (a614)) % 1.93/2.16 (-. (c3_1 (a594))) % 1.93/2.16 ((a598) != zenon_X30) % 1.93/2.16 (zenon_X44 != zenon_X19) % 1.93/2.16 ((a596) != zenon_X12) % 1.93/2.16 (c2_2 zenon_X3 (a598)) % 1.93/2.16 (zenon_X33 != zenon_X19) % 1.93/2.16 (zenon_X38 != zenon_X28) % 1.93/2.16 (c5_1 (a587)) % 1.93/2.16 (zenon_X20 != zenon_X38) % 1.93/2.16 ((a597) != zenon_X26) % 1.93/2.16 (c2_2 (a613) (a597)) % 1.93/2.16 (zenon_X18 != zenon_X46) % 1.93/2.16 ((a639) != zenon_X21) % 1.93/2.16 (c5_2 zenon_X1 zenon_X14) % 1.93/2.16 (c1_2 zenon_X1 zenon_X4) % 1.93/2.16 (zenon_X40 != zenon_X18) % 1.93/2.16 (zenon_X40 != zenon_X38) % 1.93/2.16 (c2_2 zenon_X3 zenon_X26) % 1.93/2.16 (zenon_X1 != zenon_X8) % 1.93/2.16 (c5_2 (a613) zenon_X4) % 1.93/2.16 (zenon_X14 != zenon_X24) % 1.93/2.16 (c1_2 zenon_X1 zenon_X26) % 1.93/2.16 (c1_2 (a613) zenon_X33) % 1.93/2.16 (c1_1 zenon_X10) % 1.93/2.16 (c2_2 (a637) zenon_X5) % 1.93/2.16 (c4_2 zenon_X3 zenon_X34) % 1.93/2.16 ((a597) != zenon_X37) % 1.93/2.16 (zenon_X33 != zenon_X46) % 1.93/2.16 ((a636) != zenon_X33) % 1.93/2.16 ((a596) != (a633)) % 1.93/2.16 (c5_2 (a637) zenon_X34) % 1.93/2.16 (-. (c5_2 (a594) zenon_X44)) % 1.93/2.16 (c1_2 (a594) zenon_X25) % 1.93/2.16 (-. (c5_2 (a616) zenon_X25)) % 1.93/2.16 (c5_2 (a633) (a638)) % 1.93/2.16 (c1_2 (a594) zenon_X16) % 1.93/2.16 (c5_2 zenon_X1 zenon_X13) % 1.93/2.16 (c5_2 (a633) zenon_X28) % 1.93/2.16 (zenon_X38 != zenon_X42) % 1.93/2.16 (zenon_X16 != zenon_X42) % 1.93/2.16 (c4_2 zenon_X3 zenon_X42) % 1.93/2.16 (zenon_X13 != zenon_X20) % 1.93/2.16 (c5_2 zenon_X1 zenon_X44) % 1.93/2.16 (zenon_X32 != zenon_X42) % 1.93/2.16 (zenon_X38 != zenon_X46) % 1.93/2.16 (c5_2 (a633) (a614)) % 1.93/2.16 (zenon_X30 != (a639)) % 1.93/2.16 (c1_2 (a594) (a638)) % 1.93/2.16 (zenon_X1 != (a616)) % 1.93/2.16 ((a639) != (a597)) % 1.93/2.16 ((a639) != zenon_X42) % 1.93/2.16 (-. (c1_2 (a633) zenon_X49)) % 1.93/2.16 ((a638) != zenon_X33) % 1.93/2.16 (zenon_X11 != (a598)) % 1.93/2.16 (c1_2 (a613) zenon_X42) % 1.93/2.16 (c1_2 zenon_X1 zenon_X42) % 1.93/2.16 (c4_2 (a616) zenon_X33) % 1.93/2.16 (c4_2 zenon_X6 (a639)) % 1.93/2.16 (c1_2 zenon_X3 zenon_X30) % 1.93/2.16 (zenon_X38 != zenon_X30) % 1.93/2.16 (-. (c5_2 (a594) (a597))) % 1.93/2.16 ((a636) != zenon_X23) % 1.93/2.16 (-. (c5_2 (a587) (a597))) % 1.93/2.16 (zenon_X40 != zenon_X28) % 1.93/2.16 (-. (c2_2 (a613) zenon_X31)) % 1.93/2.16 (c2_2 zenon_X3 zenon_X17) % 1.93/2.16 (-. (c5_2 zenon_X10 zenon_X26)) % 1.93/2.16 (-. (c5_2 (a637) zenon_X14)) % 1.93/2.16 (c1_2 zenon_X6 zenon_X20) % 1.93/2.16 (-. (c5_2 zenon_X6 (a598))) % 1.93/2.16 (c4_2 zenon_X10 zenon_X23) % 1.93/2.16 (zenon_X23 != zenon_X42) % 1.93/2.16 (zenon_X4 != zenon_X26) % 1.93/2.16 (zenon_X28 != zenon_X34) % 1.93/2.16 (c4_2 zenon_X6 zenon_X42) % 1.93/2.16 (c2_2 zenon_X1 zenon_X31) % 1.93/2.16 (-. (c3_1 (a633))) % 1.93/2.16 (c1_2 zenon_X6 zenon_X40) % 1.93/2.16 (ndr1_1 (a596)) % 1.93/2.16 (zenon_X11 != (a614)) % 1.93/2.16 ((a613) != (a616)) % 1.93/2.16 (zenon_X17 != zenon_X48) % 1.93/2.16 (zenon_X13 != zenon_X5) % 1.93/2.16 (zenon_X20 != zenon_X34) % 1.93/2.16 (c4_2 zenon_X6 zenon_X11) % 1.93/2.16 ((a596) != (a637)) % 1.93/2.16 (zenon_X32 != zenon_X28) % 1.93/2.16 (zenon_X38 != (a638)) % 1.93/2.16 (-. (c3_1 zenon_X12)) % 1.93/2.16 (c5_2 (a613) zenon_X28) % 1.93/2.16 (c4_2 zenon_X10 zenon_X33) % 1.93/2.16 (-. (c5_2 zenon_X6 zenon_X13)) % 1.93/2.16 (c5_2 (a633) zenon_X44) % 1.93/2.16 (c5_2 zenon_X1 (a614)) % 1.93/2.16 (c4_2 zenon_X10 (a610)) % 1.93/2.16 (c4_2 (a613) zenon_X19) % 1.93/2.16 (zenon_X13 != (a614)) % 1.93/2.16 ((a610) != zenon_X14) % 1.93/2.16 (c1_2 zenon_X3 zenon_X11) % 1.93/2.16 (zenon_X13 != zenon_X42) % 1.93/2.16 (zenon_X14 != zenon_X26) % 1.93/2.16 ((a597) != zenon_X36) % 1.93/2.16 (zenon_X14 != zenon_X28) % 1.93/2.16 ((a598) != zenon_X28) % 1.93/2.16 (c1_2 zenon_X1 zenon_X23) % 1.93/2.16 ((a597) != zenon_X42) % 1.93/2.16 (c5_2 zenon_X6 zenon_X40) % 1.93/2.16 (-. (c5_2 (a594) zenon_X4)) % 1.93/2.16 (-. (c5_2 zenon_X10 zenon_X46)) % 1.93/2.16 (c5_2 (a616) zenon_X11) % 1.93/2.16 (c4_2 zenon_X10 zenon_X25) % 1.93/2.16 (c2_2 zenon_X3 zenon_X23) % 1.93/2.16 (c1_2 (a613) zenon_X4) % 1.93/2.16 (c5_2 zenon_X1 (a636)) % 1.93/2.16 (c2_2 (a637) (a639)) % 1.93/2.16 (zenon_X44 != (a636)) % 1.93/2.16 (c2_2 zenon_X3 zenon_X33) % 1.93/2.16 (c2_2 zenon_X3 zenon_X24) % 1.93/2.16 (c2_2 (a616) zenon_X13) % 1.93/2.16 (-. (c5_2 zenon_X6 zenon_X25)) % 1.93/2.16 (c4_2 zenon_X10 zenon_X17) % 1.93/2.16 ((a598) != zenon_X20) % 1.93/2.16 (-. (c5_2 (a594) (a610))) % 1.93/2.16 ((a597) != zenon_X31) % 1.93/2.16 (zenon_X7 != (a616)) % 1.93/2.16 ((a596) != zenon_X8) % 1.93/2.16 (zenon_X14 != zenon_X17) % 1.93/2.16 (zenon_X18 != (a614)) % 1.93/2.16 (c5_2 zenon_X1 (a639)) % 1.93/2.16 (zenon_X30 != (a638)) % 1.93/2.16 (c4_2 zenon_X6 zenon_X30) % 1.93/2.16 (c1_2 zenon_X1 zenon_X32) % 1.93/2.16 (c2_2 zenon_X1 zenon_X38) % 1.93/2.16 (-. (c5_2 (a637) zenon_X28)) % 1.93/2.16 (c2_2 (a616) zenon_X28) % 1.93/2.16 ((a614) != zenon_X50) % 1.93/2.16 (c5_2 (a613) zenon_X14) % 1.93/2.16 ((a587) != (a633)) % 1.93/2.16 (c4_2 zenon_X10 zenon_X19) % 1.93/2.16 (-. (c5_2 zenon_X6 zenon_X32)) % 1.93/2.16 (c4_2 (a637) zenon_X40) % 1.93/2.16 (zenon_X25 != (a614)) % 1.93/2.16 (c4_2 (a616) zenon_X24) % 1.93/2.16 (-. (c1_2 (a596) zenon_X9)) % 1.93/2.16 (c2_2 zenon_X0 (a636)) % 1.93/2.16 (zenon_X48 != zenon_X50) % 1.93/2.16 (zenon_X32 != zenon_X14) % 1.93/2.16 (zenon_X28 != zenon_X23) % 1.93/2.16 (-. (c3_2 (a637) (a636))) % 1.93/2.16 (c4_2 zenon_X6 (a598)) % 1.93/2.16 (zenon_X4 != zenon_X46) % 1.93/2.16 (zenon_X14 != zenon_X23) % 1.93/2.16 (-. (c2_2 (a613) zenon_X17)) % 1.93/2.16 (-. (c5_1 zenon_X10)) % 1.93/2.16 ((a610) != zenon_X16) % 1.93/2.16 (zenon_X0 != zenon_X1) % 1.93/2.16 (-. (c5_2 (a613) zenon_X31)) % 1.93/2.16 (zenon_X20 != zenon_X14) % 1.93/2.16 (zenon_X7 != zenon_X12) % 1.93/2.17 (-. (c5_2 zenon_X6 zenon_X26)) % 1.93/2.17 (-. (c5_2 (a613) zenon_X17)) % 1.93/2.17 (c4_2 (a637) zenon_X23) % 1.93/2.17 (c5_2 (a633) zenon_X46) % 1.93/2.17 (zenon_X1 != (a594)) % 1.93/2.17 (-. (c5_2 (a637) zenon_X4)) % 1.93/2.17 (c5_2 (a613) zenon_X32) % 1.93/2.17 (c1_2 (a616) zenon_X20) % 1.93/2.17 (zenon_X11 != zenon_X23) % 1.93/2.17 (c2_2 (a594) (a638)) % 1.93/2.17 (c5_2 zenon_X3 zenon_X24) % 1.93/2.17 (-. (c5_2 zenon_X6 zenon_X17)) % 1.93/2.17 (zenon_X38 != zenon_X31) % 1.93/2.17 (zenon_X18 != zenon_X17) % 1.93/2.17 ((a598) != zenon_X26) % 1.93/2.17 (c5_2 (a637) (a610)) % 1.93/2.17 ((a638) != zenon_X31) % 1.93/2.17 ((a638) != zenon_X21) % 1.93/2.17 (-. (c1_2 (a596) (a597))) % 1.93/2.17 (c4_2 (a637) zenon_X24) % 1.93/2.17 (zenon_X32 != zenon_X25) % 1.93/2.17 (-. (c3_2 zenon_X6 (a636))) % 1.93/2.17 (c5_2 zenon_X1 zenon_X24) % 1.93/2.17 (c2_2 (a613) zenon_X11) % 1.93/2.17 (-. (c2_2 (a613) zenon_X18)) % 1.93/2.17 (c2_2 zenon_X1 zenon_X32) % 1.93/2.17 (zenon_X24 != zenon_X19) % 1.93/2.17 (c4_2 zenon_X6 zenon_X17) % 1.93/2.17 (zenon_X34 != zenon_X48) % 1.93/2.17 (c1_2 (a616) zenon_X34) % 1.93/2.17 (ndr1_1 (a633)) % 1.93/2.17 (-. (c5_2 zenon_X1 zenon_X34)) % 1.93/2.17 ((a598) != zenon_X48) % 1.93/2.17 (zenon_X4 != zenon_X33) % 1.93/2.17 (c5_2 zenon_X3 zenon_X5) % 1.93/2.17 (c1_2 (a594) zenon_X5) % 1.93/2.17 (-. (c5_2 (a616) zenon_X42)) % 1.93/2.17 (-. (c1_2 zenon_X3 (a598))) % 1.93/2.17 (zenon_X23 != zenon_X34) % 1.93/2.17 (-. (c5_2 (a616) (a610))) % 1.93/2.17 (zenon_X15 != zenon_X42) % 1.93/2.17 (zenon_X26 != zenon_X33) % 1.93/2.17 ((a598) != zenon_X32) % 1.93/2.17 ((a610) != zenon_X50) % 1.93/2.17 (c1_2 (a594) zenon_X28) % 1.93/2.17 ((a636) != zenon_X4) % 1.93/2.17 ((a598) != zenon_X41) % 1.93/2.17 (zenon_X18 != zenon_X42) % 1.93/2.17 (c4_2 zenon_X10 zenon_X42) % 1.93/2.17 (c4_2 zenon_X6 zenon_X28) % 1.93/2.17 (zenon_X6 != (a633)) % 1.93/2.17 (zenon_X33 != zenon_X48) % 1.93/2.17 (c2_2 (a637) zenon_X31) % 1.93/2.17 (c4_2 zenon_X10 zenon_X30) % 1.93/2.17 (c1_2 (a594) zenon_X30) % 1.93/2.17 ((a598) != zenon_X13) % 1.93/2.17 (c3_1 zenon_X7) % 1.93/2.17 (c2_2 (a594) zenon_X28) % 1.93/2.17 (c5_2 (a637) zenon_X25) % 1.93/2.17 (-. (c5_2 zenon_X10 zenon_X24)) % 1.93/2.17 (c2_2 zenon_X1 zenon_X13) % 1.93/2.17 (-. (c2_2 (a613) zenon_X25)) % 1.93/2.17 (zenon_X40 != zenon_X34) % 1.93/2.17 (c4_2 (a594) zenon_X44) % 1.93/2.17 (-. (c1_2 zenon_X3 zenon_X40)) % 1.93/2.17 (-. (c5_1 zenon_X3)) % 1.93/2.17 (-. (c4_2 (a637) (a638))) % 1.93/2.17 (-. (c5_1 zenon_X6)) % 1.93/2.17 (-. (c5_1 (a594))) % 1.93/2.17 ((a610) != zenon_X19) % 1.93/2.17 ((a597) != zenon_X25) % 1.93/2.17 (c4_2 zenon_X6 zenon_X5) % 1.93/2.17 (c5_1 zenon_X8) % 1.93/2.17 (-. (c1_2 (a637) zenon_X15)) % 1.93/2.17 (c4_2 (a594) (a639)) % 1.93/2.17 (c5_2 (a594) zenon_X23) % 1.93/2.17 (c2_2 zenon_X1 zenon_X16) % 1.93/2.17 (-. (c5_2 zenon_X10 (a610))) % 1.93/2.17 (-. (c3_1 (a637))) % 1.93/2.17 (c4_2 (a616) zenon_X32) % 1.93/2.17 (c4_2 (a616) zenon_X17) % 1.93/2.17 (c4_2 (a613) zenon_X48) % 1.93/2.17 (zenon_X40 != zenon_X25) % 1.93/2.17 (c4_2 zenon_X1 zenon_X46) % 1.93/2.17 (zenon_X20 != zenon_X19) % 1.93/2.17 (c4_2 (a616) zenon_X26) % 1.93/2.17 ((a598) != zenon_X31) % 1.93/2.17 (zenon_X18 != zenon_X23) % 1.93/2.17 (zenon_X30 != zenon_X33) % 1.93/2.17 (c5_2 zenon_X3 zenon_X30) % 1.93/2.17 (c1_2 zenon_X10 zenon_X38) % 1.93/2.17 (c5_2 (a594) zenon_X18) % 1.93/2.17 (c5_2 (a633) zenon_X15) % 1.93/2.17 (zenon_X38 != zenon_X23) % 1.93/2.17 (c4_2 zenon_X6 (a614)) % 1.93/2.17 (c5_2 zenon_X3 zenon_X18) % 1.93/2.17 (c2_2 (a594) zenon_X5) % 1.93/2.17 (zenon_X19 != zenon_X48) % 1.93/2.17 (zenon_X20 != zenon_X33) % 1.93/2.17 (-. (c4_0)) % 1.93/2.17 (-. (c3_2 (a633) (a636))) % 1.93/2.17 (c1_1 zenon_X12) % 1.93/2.17 (c2_2 zenon_X6 zenon_X48) % 1.93/2.17 (c5_2 zenon_X1 zenon_X26) % 1.93/2.17 (c4_2 zenon_X10 zenon_X20) % 1.93/2.17 (zenon_X11 != zenon_X25) % 1.93/2.17 (c4_2 zenon_X6 zenon_X13) % 1.93/2.17 ((a587) != (a616)) % 1.93/2.17 (c4_2 (a616) zenon_X40) % 1.93/2.17 (zenon_X30 != zenon_X28) % 1.93/2.17 (c4_2 zenon_X1 (a598)) % 1.93/2.17 (c1_2 zenon_X3 zenon_X32) % 1.93/2.17 (zenon_X32 != zenon_X13) % 1.93/2.17 ((a636) != (a598)) % 1.93/2.17 (zenon_X38 != zenon_X33) % 1.93/2.17 (zenon_X18 != zenon_X28) % 1.93/2.17 (-. (c5_2 (a616) zenon_X26)) % 1.93/2.17 (zenon_X23 != zenon_X31) % 1.93/2.17 (zenon_X13 != (a638)) % 1.93/2.17 (zenon_X17 != zenon_X46) % 1.93/2.17 (c5_2 zenon_X1 zenon_X17) % 1.93/2.17 (c4_2 zenon_X3 zenon_X16) % 1.93/2.17 (zenon_X44 != (a598)) % 1.93/2.17 ((a616) != zenon_X3) % 1.93/2.17 (c4_2 (a637) zenon_X13) % 1.93/2.17 (c2_0) % 1.93/2.17 (zenon_X28 != zenon_X20) % 1.93/2.17 (c5_2 (a637) (a597)) % 1.93/2.17 (c2_2 (a587) (a636)) % 1.93/2.17 (c5_2 zenon_X1 (a597)) % 1.93/2.17 (c5_2 (a633) zenon_X14) % 1.93/2.17 (c5_2 (a616) zenon_X34) % 1.93/2.17 ((a636) != zenon_X13) % 1.93/2.17 (c5_2 (a637) zenon_X18) % 1.93/2.17 (-. (c5_2 (a613) zenon_X5)) % 1.93/2.17 (zenon_X20 != zenon_X30) % 1.93/2.17 (c2_2 zenon_X1 zenon_X20) % 1.93/2.17 (c2_2 (a633) (a636)) % 1.93/2.17 (c4_2 zenon_X6 zenon_X26) % 1.93/2.17 (c4_2 (a637) (a614)) % 1.93/2.17 (zenon_X32 != (a639)) % 1.93/2.17 (zenon_X40 != (a638)) % 1.93/2.17 (-. (c3_2 (a633) zenon_X2)) % 1.93/2.17 (c2_2 (a594) (a636)) % 1.93/2.17 (-. (c1_2 (a596) (a614))) % 1.93/2.17 (zenon_X20 != zenon_X48) % 1.93/2.17 (c2_2 (a616) (a597)) % 1.93/2.17 ((a636) != zenon_X50) % 1.93/2.17 (c1_2 zenon_X1 zenon_X18) % 1.93/2.17 ((a614) != (a610)) % 1.93/2.17 (zenon_X13 != zenon_X23) % 1.93/2.17 (zenon_X26 != zenon_X31) % 1.93/2.17 (c5_2 (a616) zenon_X20) % 1.93/2.17 (c4_2 (a594) (a614)) % 1.93/2.17 (zenon_X25 != zenon_X19) % 1.93/2.17 (c1_2 (a594) (a636)) % 1.93/2.17 (-. (c5_2 (a637) zenon_X46)) % 1.93/2.17 (zenon_X6 != (a637)) % 1.93/2.17 (zenon_X18 != zenon_X33) % 1.93/2.17 (c1_2 zenon_X3 zenon_X46) % 1.93/2.17 (c5_2 (a637) zenon_X48) % 1.93/2.17 (c5_2 zenon_X1 zenon_X4) % 1.93/2.17 (c5_2 (a616) zenon_X4) % 1.93/2.17 (c5_2 zenon_X10 zenon_X38) % 1.93/2.17 (zenon_X19 != zenon_X46) % 1.93/2.17 (c2_2 (a594) zenon_X20) % 1.93/2.17 ((a636) != zenon_X24) % 1.93/2.17 (ndr1_1 zenon_X10) % 1.93/2.17 (-. (c1_2 (a637) (a610))) % 1.93/2.17 ((a636) != zenon_X19) % 1.93/2.17 (c2_2 zenon_X6 (a636)) % 1.93/2.17 (zenon_X23 != zenon_X33) % 1.93/2.17 (-. (c5_2 zenon_X10 zenon_X14)) % 1.93/2.17 ((a636) != zenon_X46) % 1.93/2.17 (c5_2 (a637) zenon_X11) % 1.93/2.17 (zenon_X11 != zenon_X17) % 1.93/2.17 (zenon_X10 != zenon_X6) % 1.93/2.17 (c1_2 (a594) zenon_X15) % 1.93/2.17 (c1_2 zenon_X3 zenon_X25) % 1.93/2.17 ((a597) != zenon_X11) % 1.93/2.17 (c1_2 zenon_X3 (a636)) % 1.93/2.17 (zenon_X16 != zenon_X23) % 1.93/2.17 (-. (c1_2 zenon_X3 (a614))) % 1.93/2.17 (c1_2 zenon_X1 zenon_X16) % 1.93/2.17 ((a614) != zenon_X19) % 1.93/2.17 (c1_2 (a594) zenon_X24) % 1.93/2.17 ((a587) != zenon_X10) % 1.93/2.17 ((a639) != zenon_X16) % 1.93/2.17 (c5_2 (a594) zenon_X19) % 1.93/2.17 (c4_2 zenon_X6 zenon_X25) % 1.93/2.17 (zenon_X44 != zenon_X40) % 1.93/2.17 (c4_2 zenon_X10 (a639)) % 1.93/2.17 (zenon_X4 != zenon_X16) % 1.93/2.17 ((a596) != (a587)) % 1.93/2.17 (c2_2 (a613) (a636)) % 1.93/2.17 (c4_2 (a613) zenon_X25) % 1.93/2.17 (zenon_X24 != zenon_X31) % 1.93/2.17 (c2_2 zenon_X3 (a597)) % 1.93/2.17 (zenon_X13 != zenon_X46) % 1.93/2.17 (zenon_X20 != zenon_X42) % 1.93/2.17 (ndr1_1 zenon_X0) % 1.93/2.17 (-. (c5_1 (a616))) % 1.93/2.17 (c2_2 (a596) (a636)) % 1.93/2.17 (zenon_X13 != (a597)) % 1.93/2.17 (zenon_X32 != zenon_X16) % 1.93/2.17 *) % 1.93/2.17 (* NO-PROOF *) % 1.93/2.17 % SZS status GaveUp % 1.93/2.17 Number of rewrites on terms: 0 % 1.93/2.17 Number of rewrites on props: 0 % 1.93/2.17 nodes searched: 48540 % 1.93/2.17 max branch formulas: 2770 % 1.93/2.17 proof nodes created: 1155 % 1.93/2.17 formulas created: 23453 % 1.93/2.17 %------------------------------------------------------------------------------