%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : SWC539_1 : TPTP v9.2.1. Bugfixed v9.1.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n003.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 : Wed Jun 3 08:59:23 AM UTC 2026 % Result : Theorem 3.94s 4.13s % Output : Proof 3.94s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.13 % Problem : SWC539_1 : TPTP v9.2.1. Bugfixed v9.1.0. % 0.11/0.14 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.17/0.35 % Computer : n003.cluster.edu % 0.17/0.35 % Model : x86_64 x86_64 % 0.17/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.35 % Memory : 8042.1875MB % 0.17/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.35 % CPULimit : 300 % 0.17/0.35 % WCLimit : 300 % 0.17/0.35 % DateTime : Tue Jun 2 19:52:14 EDT 2026 % 0.17/0.35 % CPUTime : % 0.37/0.58 %----Proving TF0_ARI % 3.94/4.13 --- Run --finite-model-find --decision=internal at 45... % 3.94/4.13 % SZS status Theorem % 3.94/4.13 % SZS output start Proof % 3.94/4.13 ( % 3.94/4.13 (declare-sort tptp.set_0 0) % 3.94/4.13 (declare-sort tptp.set_2 0) % 3.94/4.13 (declare-const tptp.g_s99_84 tptp.set_2) % 3.94/4.13 (declare-const tptp.g_s98_83 tptp.set_2) % 3.94/4.13 (declare-const tptp.g_s96_82 tptp.set_2) % 3.94/4.13 (declare-const tptp.g_s95_81 tptp.set_2) % 3.94/4.13 (declare-const tptp.g_s93_80 tptp.set_2) % 3.94/4.13 (declare-const tptp.g_s108_79 tptp.set_2) % 3.94/4.13 (declare-const tptp.g_s107_92 tptp.set_2) % 3.94/4.13 (declare-const tptp.g_s106_91 tptp.set_2) % 3.94/4.13 (declare-const tptp.g_s105_90 tptp.set_2) % 3.94/4.13 (declare-const tptp.g_s104_89 tptp.set_2) % 3.94/4.13 (declare-const tptp.g_s103_88 tptp.set_2) % 3.94/4.13 (declare-const tptp.g_s102_87 tptp.set_2) % 3.94/4.13 (declare-const tptp.g_s101_86 tptp.set_2) % 3.94/4.13 (declare-const tptp.g_s100_85 tptp.set_2) % 3.94/4.13 (declare-const tptp.g_s97_78 tptp.set_2) % 3.94/4.13 (declare-const tptp.g_s94_77 tptp.set_2) % 3.94/4.13 (declare-const tptp.g_s64_64 tptp.set_2) % 3.94/4.13 (declare-const tptp.g_s62_62 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s61_61 tptp.set_2) % 3.94/4.13 (declare-const tptp.g_s57_57 Int) % 3.94/4.13 (declare-const tptp.g_s56_56 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s9_9 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s55_55 tptp.set_2) % 3.94/4.13 (declare-const tptp.g_s54_54 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s53_53 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s52_52 tptp.set_2) % 3.94/4.13 (declare-const tptp.g_s51_51 Int) % 3.94/4.13 (declare-const tptp.g_s50_50 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s8_8 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s49_49 tptp.set_2) % 3.94/4.13 (declare-const tptp.g_s48_48 Int) % 3.94/4.13 (declare-const tptp.g_s46_47 Int) % 3.94/4.13 (declare-const tptp.g_s47_46 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s45_45 tptp.set_2) % 3.94/4.13 (declare-const tptp.g_s44_44 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s19_19 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s18_18 Int) % 3.94/4.13 (declare-const tptp.g_s76_76 tptp.set_2) % 3.94/4.13 (declare-const tptp.g_s17_17 Int) % 3.94/4.13 (declare-const tptp.g_s75_75 Int) % 3.94/4.13 (declare-const tptp.g_s16_16 Int) % 3.94/4.13 (declare-const tptp.g_s74_74 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s15_15 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s73_73 tptp.set_2) % 3.94/4.13 (declare-const tptp.g_s14_14 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s72_72 Int) % 3.94/4.13 (declare-const tptp.g_s13_13 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s71_71 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s12_12 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s11_11 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s70_70 tptp.set_2) % 3.94/4.13 (declare-const tptp.g_s69_69 Int) % 3.94/4.13 (declare-const tptp.g_s10_10 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s60_60 Int) % 3.94/4.13 (declare-const tptp.max_int Int) % 3.94/4.13 (declare-const tptp.g_s28_28 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s59_59 tptp.set_0) % 3.94/4.13 (declare-const tptp.min_int Int) % 3.94/4.13 (declare-const tptp.g_s27_27 tptp.set_2) % 3.94/4.13 (declare-const tptp.g_s0_0 tptp.set_0) % 3.94/4.13 (declare-const tptp.mem2 (-> Int Int tptp.set_2 Bool)) % 3.94/4.13 (declare-const tptp.g_s65_65 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s6_6 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s58_58 tptp.set_2) % 3.94/4.13 (declare-const tptp.mem0 (-> Int tptp.set_0 Bool)) % 3.94/4.13 (declare-const tptp.g_s26_26 Int) % 3.94/4.13 (declare-const tptp.g_s1_1 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s66_66 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s7_7 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s63_63 Int) % 3.94/4.13 (declare-const tptp.g_s4_4 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s67_67 tptp.set_2) % 3.94/4.13 (declare-const tptp.g_s68_68 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s20_20 Int) % 3.94/4.13 (declare-const tptp.g_s21_21 tptp.set_2) % 3.94/4.13 (declare-const tptp.g_s2_2 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s22_22 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s23_23 Int) % 3.94/4.13 (declare-const tptp.g_s24_24 tptp.set_2) % 3.94/4.13 (declare-const tptp.g_s25_25 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s3_3 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s29_29 Int) % 3.94/4.13 (declare-const tptp.g_s30_30 tptp.set_2) % 3.94/4.13 (declare-const tptp.g_s31_31 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s32_32 Int) % 3.94/4.13 (declare-const tptp.g_s33_33 tptp.set_2) % 3.94/4.13 (declare-const tptp.g_s5_5 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s34_34 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s35_35 Int) % 3.94/4.13 (declare-const tptp.g_s36_36 tptp.set_2) % 3.94/4.13 (declare-const tptp.g_s37_37 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s38_38 Int) % 3.94/4.13 (declare-const tptp.g_s39_39 tptp.set_2) % 3.94/4.13 (declare-const tptp.g_s40_40 tptp.set_0) % 3.94/4.13 (declare-const tptp.g_s41_41 Int) % 3.94/4.13 (declare-const tptp.g_s42_42 tptp.set_2) % 3.94/4.13 (declare-const tptp.g_s43_43 tptp.set_2) % 3.94/4.13 (define @t1 () (@var "X_23" Int)) % 3.94/4.13 (define @t2 () (@var "X_22" Int)) % 3.94/4.13 (define @t3 () (@var "X_7" tptp.set_2)) % 3.94/4.13 (define @t4 () (@var "X_21" Int)) % 3.94/4.13 (define @t5 () (@var "X_19" Int)) % 3.94/4.13 (define @t6 () (@var "X_20" Int)) % 3.94/4.13 (define @t7 () (@var "X_17" Int)) % 3.94/4.13 (define @t8 () (@var "X_9" tptp.set_2)) % 3.94/4.13 (define @t9 () (@var "X_18" Int)) % 3.94/4.13 (define @t10 () (@var "X_16" Int)) % 3.94/4.13 (define @t11 () (@var "X_15" Int)) % 3.94/4.13 (define @t12 () (@var "X_6" Int)) % 3.94/4.13 (define @t13 () (@var "X_14" Int)) % 3.94/4.13 (define @t14 () (@var "X_13" Int)) % 3.94/4.13 (define @t15 () (@var "X_12" Int)) % 3.94/4.13 (define @t16 () (@var "X_10" Int)) % 3.94/4.13 (define @t17 () (@var "X_11" Int)) % 3.94/4.13 (define @t18 () (@var "X_8" Int)) % 3.94/4.13 (define @t19 () (@var "X_5" Int)) % 3.94/4.13 (define @t20 () (@var "X_42" Int)) % 3.94/4.13 (define @t21 () (@var "X_41" Int)) % 3.94/4.13 (define @t22 () (@var "X_26" tptp.set_2)) % 3.94/4.13 (define @t23 () (@var "X_40" Int)) % 3.94/4.13 (define @t24 () (@var "X_38" Int)) % 3.94/4.13 (define @t25 () (@var "X_39" Int)) % 3.94/4.13 (define @t26 () (@var "X_36" Int)) % 3.94/4.13 (define @t27 () (@var "X_28" tptp.set_2)) % 3.94/4.13 (define @t28 () (@var "X_37" Int)) % 3.94/4.13 (define @t29 () (@var "X_35" Int)) % 3.94/4.13 (define @t30 () (@var "X_34" Int)) % 3.94/4.13 (define @t31 () (@var "X_25" Int)) % 3.94/4.13 (define @t32 () (@var "X_33" Int)) % 3.94/4.13 (define @t33 () (@var "X_32" Int)) % 3.94/4.13 (define @t34 () (@var "X_31" Int)) % 3.94/4.13 (define @t35 () (@var "X_29" Int)) % 3.94/4.13 (define @t36 () (@var "X_30" Int)) % 3.94/4.13 (define @t37 () (@var "X_27" Int)) % 3.94/4.13 (define @t38 () (@var "X_24" Int)) % 3.94/4.13 (define @t39 () (@var "X_213" Int)) % 3.94/4.13 (define @t40 () (@var "X_212" Int)) % 3.94/4.13 (define @t41 () (@var "X_197" tptp.set_2)) % 3.94/4.13 (define @t42 () (@var "X_211" Int)) % 3.94/4.13 (define @t43 () (@var "X_209" Int)) % 3.94/4.13 (define @t44 () (@var "X_210" Int)) % 3.94/4.13 (define @t45 () (@var "X_207" Int)) % 3.94/4.13 (define @t46 () (@var "X_199" tptp.set_2)) % 3.94/4.13 (define @t47 () (@var "X_208" Int)) % 3.94/4.13 (define @t48 () (@var "X_206" Int)) % 3.94/4.13 (define @t49 () (@var "X_205" Int)) % 3.94/4.13 (define @t50 () (@var "X_196" Int)) % 3.94/4.13 (define @t51 () (@var "X_204" Int)) % 3.94/4.13 (define @t52 () (@var "X_203" Int)) % 3.94/4.13 (define @t53 () (@var "X_202" Int)) % 3.94/4.13 (define @t54 () (@var "X_200" Int)) % 3.94/4.13 (define @t55 () (@var "X_201" Int)) % 3.94/4.13 (define @t56 () (@var "X_198" Int)) % 3.94/4.13 (define @t57 () (@var "X_195" Int)) % 3.94/4.13 (define @t58 () (@var "X_639" Int)) % 3.94/4.13 (define @t59 () (@var "X_638" Int)) % 3.94/4.13 (define @t60 () (@var "X_637" Int)) % 3.94/4.13 (define @t61 () (@var "X_635" Int)) % 3.94/4.13 (define @t62 () (@var "X_636" Int)) % 3.94/4.13 (define @t63 () (@var "X_655" Int)) % 3.94/4.13 (define @t64 () (@var "X_654" Int)) % 3.94/4.13 (define @t65 () (@var "X_653" Int)) % 3.94/4.13 (define @t66 () (@var "X_651" Int)) % 3.94/4.13 (define @t67 () (@var "X_652" Int)) % 3.94/4.13 (define @t68 () (@var "X_649" Int)) % 3.94/4.13 (define @t69 () (@var "X_641" tptp.set_2)) % 3.94/4.13 (define @t70 () (@var "X_650" Int)) % 3.94/4.13 (define @t71 () (@var "X_648" Int)) % 3.94/4.13 (define @t72 () (@var "X_647" Int)) % 3.94/4.13 (define @t73 () (@var "X_640" Int)) % 3.94/4.13 (define @t74 () (@var "X_646" Int)) % 3.94/4.13 (define @t75 () (@var "X_645" Int)) % 3.94/4.13 (define @t76 () (@var "X_644" Int)) % 3.94/4.13 (define @t77 () (@var "X_642" Int)) % 3.94/4.13 (define @t78 () (@var "X_643" Int)) % 3.94/4.13 (define @t79 () (@var "X_656" Int)) % 3.94/4.13 (define @t80 () (@var "X_661" Int)) % 3.94/4.13 (define @t81 () (@var "X_660" Int)) % 3.94/4.13 (define @t82 () (@var "X_659" Int)) % 3.94/4.13 (define @t83 () (@var "X_657" Int)) % 3.94/4.13 (define @t84 () (@var "X_658" Int)) % 3.94/4.13 (define @t85 () (@var "X_677" Int)) % 3.94/4.13 (define @t86 () (@var "X_676" Int)) % 3.94/4.13 (define @t87 () (@var "X_675" Int)) % 3.94/4.13 (define @t88 () (@var "X_673" Int)) % 3.94/4.13 (define @t89 () (@var "X_674" Int)) % 3.94/4.13 (define @t90 () (@var "X_671" Int)) % 3.94/4.13 (define @t91 () (@var "X_663" tptp.set_2)) % 3.94/4.13 (define @t92 () (@var "X_672" Int)) % 3.94/4.13 (define @t93 () (@var "X_670" Int)) % 3.94/4.13 (define @t94 () (@var "X_669" Int)) % 3.94/4.13 (define @t95 () (@var "X_662" Int)) % 3.94/4.13 (define @t96 () (@var "X_668" Int)) % 3.94/4.13 (define @t97 () (@var "X_667" Int)) % 3.94/4.13 (define @t98 () (@var "X_666" Int)) % 3.94/4.13 (define @t99 () (@var "X_664" Int)) % 3.94/4.13 (define @t100 () (@var "X_665" Int)) % 3.94/4.13 (define @t101 () (@var "X_678" Int)) % 3.94/4.13 (define @t102 () (@var "X_232" Int)) % 3.94/4.13 (define @t103 () (@var "X_231" Int)) % 3.94/4.13 (define @t104 () (@var "X_216" tptp.set_2)) % 3.94/4.13 (define @t105 () (@var "X_230" Int)) % 3.94/4.13 (define @t106 () (@var "X_228" Int)) % 3.94/4.13 (define @t107 () (@var "X_229" Int)) % 3.94/4.13 (define @t108 () (@var "X_226" Int)) % 3.94/4.13 (define @t109 () (@var "X_218" tptp.set_2)) % 3.94/4.13 (define @t110 () (@var "X_227" Int)) % 3.94/4.13 (define @t111 () (@var "X_225" Int)) % 3.94/4.13 (define @t112 () (@var "X_224" Int)) % 3.94/4.13 (define @t113 () (@var "X_215" Int)) % 3.94/4.13 (define @t114 () (@var "X_223" Int)) % 3.94/4.13 (define @t115 () (@var "X_222" Int)) % 3.94/4.13 (define @t116 () (@var "X_221" Int)) % 3.94/4.13 (define @t117 () (@var "X_219" Int)) % 3.94/4.13 (define @t118 () (@var "X_220" Int)) % 3.94/4.13 (define @t119 () (@var "X_217" Int)) % 3.94/4.13 (define @t120 () (@var "X_214" Int)) % 3.94/4.13 (define @t121 () (@var "X_683" Int)) % 3.94/4.13 (define @t122 () (@var "X_682" Int)) % 3.94/4.13 (define @t123 () (@var "X_681" Int)) % 3.94/4.13 (define @t124 () (@var "X_679" Int)) % 3.94/4.13 (define @t125 () (@var "X_680" Int)) % 3.94/4.13 (define @t126 () (@var "X_699" Int)) % 3.94/4.13 (define @t127 () (@var "X_698" Int)) % 3.94/4.13 (define @t128 () (@var "X_697" Int)) % 3.94/4.13 (define @t129 () (@var "X_695" Int)) % 3.94/4.13 (define @t130 () (@var "X_696" Int)) % 3.94/4.13 (define @t131 () (@var "X_693" Int)) % 3.94/4.13 (define @t132 () (@var "X_685" tptp.set_2)) % 3.94/4.13 (define @t133 () (@var "X_694" Int)) % 3.94/4.13 (define @t134 () (@var "X_692" Int)) % 3.94/4.13 (define @t135 () (@var "X_691" Int)) % 3.94/4.13 (define @t136 () (@var "X_684" Int)) % 3.94/4.13 (define @t137 () (@var "X_690" Int)) % 3.94/4.13 (define @t138 () (@var "X_689" Int)) % 3.94/4.13 (define @t139 () (@var "X_688" Int)) % 3.94/4.13 (define @t140 () (@var "X_686" Int)) % 3.94/4.13 (define @t141 () (@var "X_687" Int)) % 3.94/4.13 (define @t142 () (@var "X_700" Int)) % 3.94/4.13 (define @t143 () (@var "X_705" Int)) % 3.94/4.13 (define @t144 () (@var "X_704" Int)) % 3.94/4.13 (define @t145 () (@var "X_703" Int)) % 3.94/4.13 (define @t146 () (@var "X_701" Int)) % 3.94/4.13 (define @t147 () (@var "X_702" Int)) % 3.94/4.13 (define @t148 () (@var "X_721" Int)) % 3.94/4.13 (define @t149 () (@var "X_720" Int)) % 3.94/4.13 (define @t150 () (@var "X_719" Int)) % 3.94/4.13 (define @t151 () (@var "X_717" Int)) % 3.94/4.13 (define @t152 () (@var "X_718" Int)) % 3.94/4.13 (define @t153 () (@var "X_715" Int)) % 3.94/4.13 (define @t154 () (@var "X_707" tptp.set_2)) % 3.94/4.13 (define @t155 () (@var "X_716" Int)) % 3.94/4.13 (define @t156 () (@var "X_714" Int)) % 3.94/4.13 (define @t157 () (@var "X_713" Int)) % 3.94/4.13 (define @t158 () (@var "X_706" Int)) % 3.94/4.13 (define @t159 () (@var "X_712" Int)) % 3.94/4.13 (define @t160 () (@var "X_711" Int)) % 3.94/4.13 (define @t161 () (@var "X_710" Int)) % 3.94/4.13 (define @t162 () (@var "X_708" Int)) % 3.94/4.13 (define @t163 () (@var "X_709" Int)) % 3.94/4.13 (define @t164 () (@var "X_251" Int)) % 3.94/4.13 (define @t165 () (@var "X_250" Int)) % 3.94/4.13 (define @t166 () (@var "X_235" tptp.set_2)) % 3.94/4.13 (define @t167 () (@var "X_249" Int)) % 3.94/4.13 (define @t168 () (@var "X_247" Int)) % 3.94/4.13 (define @t169 () (@var "X_248" Int)) % 3.94/4.13 (define @t170 () (@var "X_245" Int)) % 3.94/4.13 (define @t171 () (@var "X_237" tptp.set_2)) % 3.94/4.13 (define @t172 () (@var "X_246" Int)) % 3.94/4.13 (define @t173 () (@var "X_244" Int)) % 3.94/4.13 (define @t174 () (@var "X_243" Int)) % 3.94/4.13 (define @t175 () (@var "X_234" Int)) % 3.94/4.13 (define @t176 () (@var "X_242" Int)) % 3.94/4.13 (define @t177 () (@var "X_241" Int)) % 3.94/4.13 (define @t178 () (@var "X_240" Int)) % 3.94/4.13 (define @t179 () (@var "X_238" Int)) % 3.94/4.13 (define @t180 () (@var "X_239" Int)) % 3.94/4.13 (define @t181 () (@var "X_236" Int)) % 3.94/4.13 (define @t182 () (@var "X_233" Int)) % 3.94/4.13 (define @t183 () (@var "X_270" Int)) % 3.94/4.13 (define @t184 () (@var "X_269" Int)) % 3.94/4.13 (define @t185 () (@var "X_254" tptp.set_2)) % 3.94/4.13 (define @t186 () (@var "X_268" Int)) % 3.94/4.13 (define @t187 () (@var "X_266" Int)) % 3.94/4.13 (define @t188 () (@var "X_267" Int)) % 3.94/4.13 (define @t189 () (@var "X_264" Int)) % 3.94/4.13 (define @t190 () (@var "X_256" tptp.set_2)) % 3.94/4.13 (define @t191 () (@var "X_265" Int)) % 3.94/4.13 (define @t192 () (@var "X_263" Int)) % 3.94/4.13 (define @t193 () (@var "X_262" Int)) % 3.94/4.13 (define @t194 () (@var "X_253" Int)) % 3.94/4.13 (define @t195 () (@var "X_261" Int)) % 3.94/4.13 (define @t196 () (@var "X_260" Int)) % 3.94/4.13 (define @t197 () (@var "X_259" Int)) % 3.94/4.13 (define @t198 () (@var "X_257" Int)) % 3.94/4.13 (define @t199 () (@var "X_258" Int)) % 3.94/4.13 (define @t200 () (@var "X_255" Int)) % 3.94/4.13 (define @t201 () (@var "X_252" Int)) % 3.94/4.13 (define @t202 () (@var "X_289" Int)) % 3.94/4.13 (define @t203 () (@var "X_288" Int)) % 3.94/4.13 (define @t204 () (@var "X_273" tptp.set_2)) % 3.94/4.13 (define @t205 () (@var "X_287" Int)) % 3.94/4.13 (define @t206 () (@var "X_285" Int)) % 3.94/4.13 (define @t207 () (@var "X_286" Int)) % 3.94/4.13 (define @t208 () (@var "X_283" Int)) % 3.94/4.13 (define @t209 () (@var "X_275" tptp.set_2)) % 3.94/4.13 (define @t210 () (@var "X_284" Int)) % 3.94/4.13 (define @t211 () (@var "X_282" Int)) % 3.94/4.13 (define @t212 () (@var "X_281" Int)) % 3.94/4.13 (define @t213 () (@var "X_272" Int)) % 3.94/4.13 (define @t214 () (@var "X_280" Int)) % 3.94/4.13 (define @t215 () (@var "X_279" Int)) % 3.94/4.13 (define @t216 () (@var "X_278" Int)) % 3.94/4.13 (define @t217 () (@var "X_276" Int)) % 3.94/4.13 (define @t218 () (@var "X_277" Int)) % 3.94/4.13 (define @t219 () (@var "X_274" Int)) % 3.94/4.13 (define @t220 () (@var "X_271" Int)) % 3.94/4.13 (define @t221 () (@var "X_290" Int)) % 3.94/4.13 (define @t222 () (@var "X_291" Int)) % 3.94/4.13 (define @t223 () (@var "X_296" Int)) % 3.94/4.13 (define @t224 () (@var "X_295" Int)) % 3.94/4.13 (define @t225 () (@var "X_294" Int)) % 3.94/4.13 (define @t226 () (@var "X_292" Int)) % 3.94/4.13 (define @t227 () (@var "X_293" Int)) % 3.94/4.13 (define @t228 () (@var "X_61" Int)) % 3.94/4.13 (define @t229 () (@var "X_60" Int)) % 3.94/4.13 (define @t230 () (@var "X_45" tptp.set_2)) % 3.94/4.13 (define @t231 () (@var "X_59" Int)) % 3.94/4.13 (define @t232 () (@var "X_57" Int)) % 3.94/4.13 (define @t233 () (@var "X_58" Int)) % 3.94/4.13 (define @t234 () (@var "X_55" Int)) % 3.94/4.13 (define @t235 () (@var "X_47" tptp.set_2)) % 3.94/4.13 (define @t236 () (@var "X_56" Int)) % 3.94/4.13 (define @t237 () (@var "X_54" Int)) % 3.94/4.13 (define @t238 () (@var "X_53" Int)) % 3.94/4.13 (define @t239 () (@var "X_44" Int)) % 3.94/4.13 (define @t240 () (@var "X_52" Int)) % 3.94/4.13 (define @t241 () (@var "X_51" Int)) % 3.94/4.13 (define @t242 () (@var "X_50" Int)) % 3.94/4.13 (define @t243 () (@var "X_48" Int)) % 3.94/4.13 (define @t244 () (@var "X_49" Int)) % 3.94/4.13 (define @t245 () (@var "X_46" Int)) % 3.94/4.13 (define @t246 () (@var "X_43" Int)) % 3.94/4.13 (define @t247 () (@var "X_312" Int)) % 3.94/4.13 (define @t248 () (@var "X_311" Int)) % 3.94/4.13 (define @t249 () (@var "X_310" Int)) % 3.94/4.13 (define @t250 () (@var "X_308" Int)) % 3.94/4.13 (define @t251 () (@var "X_309" Int)) % 3.94/4.13 (define @t252 () (@var "X_306" Int)) % 3.94/4.13 (define @t253 () (@var "X_298" tptp.set_2)) % 3.94/4.13 (define @t254 () (@var "X_307" Int)) % 3.94/4.13 (define @t255 () (@var "X_305" Int)) % 3.94/4.13 (define @t256 () (@var "X_304" Int)) % 3.94/4.13 (define @t257 () (@var "X_297" Int)) % 3.94/4.13 (define @t258 () (@var "X_303" Int)) % 3.94/4.13 (define @t259 () (@var "X_302" Int)) % 3.94/4.13 (define @t260 () (@var "X_301" Int)) % 3.94/4.13 (define @t261 () (@var "X_299" Int)) % 3.94/4.13 (define @t262 () (@var "X_300" Int)) % 3.94/4.13 (define @t263 () (@var "X_313" Int)) % 3.94/4.13 (define @t264 () (@var "X_318" Int)) % 3.94/4.13 (define @t265 () (@var "X_317" Int)) % 3.94/4.13 (define @t266 () (@var "X_316" Int)) % 3.94/4.13 (define @t267 () (@var "X_314" Int)) % 3.94/4.13 (define @t268 () (@var "X_315" Int)) % 3.94/4.13 (define @t269 () (@var "X_334" Int)) % 3.94/4.13 (define @t270 () (@var "X_333" Int)) % 3.94/4.13 (define @t271 () (@var "X_332" Int)) % 3.94/4.13 (define @t272 () (@var "X_330" Int)) % 3.94/4.13 (define @t273 () (@var "X_331" Int)) % 3.94/4.13 (define @t274 () (@var "X_328" Int)) % 3.94/4.13 (define @t275 () (@var "X_320" tptp.set_2)) % 3.94/4.13 (define @t276 () (@var "X_329" Int)) % 3.94/4.13 (define @t277 () (@var "X_327" Int)) % 3.94/4.13 (define @t278 () (@var "X_326" Int)) % 3.94/4.13 (define @t279 () (@var "X_319" Int)) % 3.94/4.13 (define @t280 () (@var "X_325" Int)) % 3.94/4.13 (define @t281 () (@var "X_324" Int)) % 3.94/4.13 (define @t282 () (@var "X_323" Int)) % 3.94/4.13 (define @t283 () (@var "X_321" Int)) % 3.94/4.13 (define @t284 () (@var "X_322" Int)) % 3.94/4.13 (define @t285 () (@var "X_335" Int)) % 3.94/4.13 (define @t286 () (@var "X_340" Int)) % 3.94/4.13 (define @t287 () (@var "X_339" Int)) % 3.94/4.13 (define @t288 () (@var "X_338" Int)) % 3.94/4.13 (define @t289 () (@var "X_336" Int)) % 3.94/4.13 (define @t290 () (@var "X_337" Int)) % 3.94/4.13 (define @t291 () (@var "X_80" Int)) % 3.94/4.13 (define @t292 () (@var "X_79" Int)) % 3.94/4.13 (define @t293 () (@var "X_64" tptp.set_2)) % 3.94/4.13 (define @t294 () (@var "X_78" Int)) % 3.94/4.13 (define @t295 () (@var "X_76" Int)) % 3.94/4.13 (define @t296 () (@var "X_77" Int)) % 3.94/4.13 (define @t297 () (@var "X_74" Int)) % 3.94/4.13 (define @t298 () (@var "X_66" tptp.set_2)) % 3.94/4.13 (define @t299 () (@var "X_75" Int)) % 3.94/4.13 (define @t300 () (@var "X_73" Int)) % 3.94/4.13 (define @t301 () (@var "X_72" Int)) % 3.94/4.13 (define @t302 () (@var "X_63" Int)) % 3.94/4.13 (define @t303 () (@var "X_71" Int)) % 3.94/4.13 (define @t304 () (@var "X_70" Int)) % 3.94/4.13 (define @t305 () (@var "X_69" Int)) % 3.94/4.13 (define @t306 () (@var "X_67" Int)) % 3.94/4.13 (define @t307 () (@var "X_68" Int)) % 3.94/4.13 (define @t308 () (@var "X_65" Int)) % 3.94/4.13 (define @t309 () (@var "X_62" Int)) % 3.94/4.13 (define @t310 () (@var "X_356" Int)) % 3.94/4.13 (define @t311 () (@var "X_355" Int)) % 3.94/4.13 (define @t312 () (@var "X_354" Int)) % 3.94/4.13 (define @t313 () (@var "X_352" Int)) % 3.94/4.13 (define @t314 () (@var "X_353" Int)) % 3.94/4.13 (define @t315 () (@var "X_350" Int)) % 3.94/4.13 (define @t316 () (@var "X_342" tptp.set_2)) % 3.94/4.13 (define @t317 () (@var "X_351" Int)) % 3.94/4.13 (define @t318 () (@var "X_349" Int)) % 3.94/4.13 (define @t319 () (@var "X_348" Int)) % 3.94/4.13 (define @t320 () (@var "X_341" Int)) % 3.94/4.13 (define @t321 () (@var "X_347" Int)) % 3.94/4.13 (define @t322 () (@var "X_346" Int)) % 3.94/4.13 (define @t323 () (@var "X_345" Int)) % 3.94/4.13 (define @t324 () (@var "X_343" Int)) % 3.94/4.13 (define @t325 () (@var "X_344" Int)) % 3.94/4.13 (define @t326 () (@var "X_357" Int)) % 3.94/4.13 (define @t327 () (@var "X_362" Int)) % 3.94/4.13 (define @t328 () (@var "X_361" Int)) % 3.94/4.13 (define @t329 () (@var "X_360" Int)) % 3.94/4.13 (define @t330 () (@var "X_358" Int)) % 3.94/4.13 (define @t331 () (@var "X_359" Int)) % 3.94/4.13 (define @t332 () (@var "X_378" Int)) % 3.94/4.13 (define @t333 () (@var "X_377" Int)) % 3.94/4.13 (define @t334 () (@var "X_376" Int)) % 3.94/4.13 (define @t335 () (@var "X_374" Int)) % 3.94/4.13 (define @t336 () (@var "X_375" Int)) % 3.94/4.13 (define @t337 () (@var "X_372" Int)) % 3.94/4.13 (define @t338 () (@var "X_364" tptp.set_2)) % 3.94/4.13 (define @t339 () (@var "X_373" Int)) % 3.94/4.13 (define @t340 () (@var "X_371" Int)) % 3.94/4.13 (define @t341 () (@var "X_370" Int)) % 3.94/4.13 (define @t342 () (@var "X_363" Int)) % 3.94/4.13 (define @t343 () (@var "X_369" Int)) % 3.94/4.13 (define @t344 () (@var "X_368" Int)) % 3.94/4.13 (define @t345 () (@var "X_367" Int)) % 3.94/4.13 (define @t346 () (@var "X_365" Int)) % 3.94/4.13 (define @t347 () (@var "X_366" Int)) % 3.94/4.13 (define @t348 () (@var "X_379" Int)) % 3.94/4.13 (define @t349 () (@var "X_384" Int)) % 3.94/4.13 (define @t350 () (@var "X_383" Int)) % 3.94/4.13 (define @t351 () (@var "X_382" Int)) % 3.94/4.13 (define @t352 () (@var "X_380" Int)) % 3.94/4.13 (define @t353 () (@var "X_381" Int)) % 3.94/4.13 (define @t354 () (@var "X_99" Int)) % 3.94/4.13 (define @t355 () (@var "X_98" Int)) % 3.94/4.13 (define @t356 () (@var "X_83" tptp.set_2)) % 3.94/4.13 (define @t357 () (@var "X_97" Int)) % 3.94/4.13 (define @t358 () (@var "X_95" Int)) % 3.94/4.13 (define @t359 () (@var "X_96" Int)) % 3.94/4.13 (define @t360 () (@var "X_93" Int)) % 3.94/4.13 (define @t361 () (@var "X_85" tptp.set_2)) % 3.94/4.13 (define @t362 () (@var "X_94" Int)) % 3.94/4.13 (define @t363 () (@var "X_92" Int)) % 3.94/4.13 (define @t364 () (@var "X_91" Int)) % 3.94/4.13 (define @t365 () (@var "X_82" Int)) % 3.94/4.13 (define @t366 () (@var "X_90" Int)) % 3.94/4.13 (define @t367 () (@var "X_89" Int)) % 3.94/4.13 (define @t368 () (@var "X_88" Int)) % 3.94/4.13 (define @t369 () (@var "X_86" Int)) % 3.94/4.13 (define @t370 () (@var "X_87" Int)) % 3.94/4.13 (define @t371 () (@var "X_84" Int)) % 3.94/4.13 (define @t372 () (@var "X_81" Int)) % 3.94/4.13 (define @t373 () (@var "X_400" Int)) % 3.94/4.13 (define @t374 () (@var "X_399" Int)) % 3.94/4.13 (define @t375 () (@var "X_398" Int)) % 3.94/4.13 (define @t376 () (@var "X_396" Int)) % 3.94/4.13 (define @t377 () (@var "X_397" Int)) % 3.94/4.13 (define @t378 () (@var "X_394" Int)) % 3.94/4.13 (define @t379 () (@var "X_386" tptp.set_2)) % 3.94/4.13 (define @t380 () (@var "X_395" Int)) % 3.94/4.13 (define @t381 () (@var "X_393" Int)) % 3.94/4.13 (define @t382 () (@var "X_392" Int)) % 3.94/4.13 (define @t383 () (@var "X_385" Int)) % 3.94/4.13 (define @t384 () (@var "X_391" Int)) % 3.94/4.13 (define @t385 () (@var "X_390" Int)) % 3.94/4.13 (define @t386 () (@var "X_389" Int)) % 3.94/4.13 (define @t387 () (@var "X_387" Int)) % 3.94/4.13 (define @t388 () (@var "X_388" Int)) % 3.94/4.13 (define @t389 () (@var "X_401" Int)) % 3.94/4.13 (define @t390 () (@var "X_406" Int)) % 3.94/4.13 (define @t391 () (@var "X_405" Int)) % 3.94/4.13 (define @t392 () (@var "X_404" Int)) % 3.94/4.13 (define @t393 () (@var "X_402" Int)) % 3.94/4.13 (define @t394 () (@var "X_403" Int)) % 3.94/4.13 (define @t395 () (@var "X_422" Int)) % 3.94/4.13 (define @t396 () (@var "X_421" Int)) % 3.94/4.13 (define @t397 () (@var "X_420" Int)) % 3.94/4.13 (define @t398 () (@var "X_418" Int)) % 3.94/4.13 (define @t399 () (@var "X_419" Int)) % 3.94/4.13 (define @t400 () (@var "X_416" Int)) % 3.94/4.13 (define @t401 () (@var "X_408" tptp.set_2)) % 3.94/4.13 (define @t402 () (@var "X_417" Int)) % 3.94/4.13 (define @t403 () (@var "X_415" Int)) % 3.94/4.13 (define @t404 () (@var "X_414" Int)) % 3.94/4.13 (define @t405 () (@var "X_407" Int)) % 3.94/4.13 (define @t406 () (@var "X_413" Int)) % 3.94/4.13 (define @t407 () (@var "X_412" Int)) % 3.94/4.13 (define @t408 () (@var "X_411" Int)) % 3.94/4.13 (define @t409 () (@var "X_409" Int)) % 3.94/4.13 (define @t410 () (@var "X_410" Int)) % 3.94/4.13 (define @t411 () (@var "X_423" Int)) % 3.94/4.13 (define @t412 () (@var "X_428" Int)) % 3.94/4.13 (define @t413 () (@var "X_427" Int)) % 3.94/4.13 (define @t414 () (@var "X_426" Int)) % 3.94/4.13 (define @t415 () (@var "X_424" Int)) % 3.94/4.13 (define @t416 () (@var "X_425" Int)) % 3.94/4.13 (define @t417 () (@var "X_118" Int)) % 3.94/4.13 (define @t418 () (@var "X_117" Int)) % 3.94/4.13 (define @t419 () (@var "X_102" tptp.set_2)) % 3.94/4.13 (define @t420 () (@var "X_116" Int)) % 3.94/4.13 (define @t421 () (@var "X_114" Int)) % 3.94/4.13 (define @t422 () (@var "X_115" Int)) % 3.94/4.13 (define @t423 () (@var "X_112" Int)) % 3.94/4.13 (define @t424 () (@var "X_104" tptp.set_2)) % 3.94/4.13 (define @t425 () (@var "X_113" Int)) % 3.94/4.13 (define @t426 () (@var "X_111" Int)) % 3.94/4.13 (define @t427 () (@var "X_110" Int)) % 3.94/4.13 (define @t428 () (@var "X_101" Int)) % 3.94/4.13 (define @t429 () (@var "X_109" Int)) % 3.94/4.13 (define @t430 () (@var "X_108" Int)) % 3.94/4.13 (define @t431 () (@var "X_107" Int)) % 3.94/4.13 (define @t432 () (@var "X_105" Int)) % 3.94/4.13 (define @t433 () (@var "X_106" Int)) % 3.94/4.13 (define @t434 () (@var "X_103" Int)) % 3.94/4.13 (define @t435 () (@var "X_100" Int)) % 3.94/4.13 (define @t436 () (@var "X_444" Int)) % 3.94/4.13 (define @t437 () (@var "X_443" Int)) % 3.94/4.13 (define @t438 () (@var "X_442" Int)) % 3.94/4.13 (define @t439 () (@var "X_440" Int)) % 3.94/4.13 (define @t440 () (@var "X_441" Int)) % 3.94/4.13 (define @t441 () (@var "X_438" Int)) % 3.94/4.13 (define @t442 () (@var "X_430" tptp.set_2)) % 3.94/4.13 (define @t443 () (@var "X_439" Int)) % 3.94/4.13 (define @t444 () (@var "X_437" Int)) % 3.94/4.13 (define @t445 () (@var "X_436" Int)) % 3.94/4.13 (define @t446 () (@var "X_429" Int)) % 3.94/4.13 (define @t447 () (@var "X_435" Int)) % 3.94/4.13 (define @t448 () (@var "X_434" Int)) % 3.94/4.13 (define @t449 () (@var "X_433" Int)) % 3.94/4.13 (define @t450 () (@var "X_431" Int)) % 3.94/4.13 (define @t451 () (@var "X_432" Int)) % 3.94/4.13 (define @t452 () (@var "X_445" Int)) % 3.94/4.13 (define @t453 () (@var "X_450" Int)) % 3.94/4.13 (define @t454 () (@var "X_449" Int)) % 3.94/4.13 (define @t455 () (@var "X_448" Int)) % 3.94/4.13 (define @t456 () (@var "X_446" Int)) % 3.94/4.13 (define @t457 () (@var "X_447" Int)) % 3.94/4.13 (define @t458 () (@var "X_466" Int)) % 3.94/4.13 (define @t459 () (@var "X_465" Int)) % 3.94/4.13 (define @t460 () (@var "X_464" Int)) % 3.94/4.13 (define @t461 () (@var "X_462" Int)) % 3.94/4.13 (define @t462 () (@var "X_463" Int)) % 3.94/4.13 (define @t463 () (@var "X_460" Int)) % 3.94/4.13 (define @t464 () (@var "X_452" tptp.set_2)) % 3.94/4.13 (define @t465 () (@var "X_461" Int)) % 3.94/4.13 (define @t466 () (@var "X_459" Int)) % 3.94/4.13 (define @t467 () (@var "X_458" Int)) % 3.94/4.13 (define @t468 () (@var "X_451" Int)) % 3.94/4.13 (define @t469 () (@var "X_457" Int)) % 3.94/4.13 (define @t470 () (@var "X_456" Int)) % 3.94/4.13 (define @t471 () (@var "X_455" Int)) % 3.94/4.13 (define @t472 () (@var "X_453" Int)) % 3.94/4.13 (define @t473 () (@var "X_454" Int)) % 3.94/4.13 (define @t474 () (@var "X_479" Int)) % 3.94/4.13 (define @t475 () (@var "X_478" Int)) % 3.94/4.13 (define @t476 () (@var "X_477" Int)) % 3.94/4.13 (define @t477 () (@var "X_475" Int)) % 3.94/4.13 (define @t478 () (@var "X_467" tptp.set_2)) % 3.94/4.13 (define @t479 () (@var "X_476" Int)) % 3.94/4.13 (define @t480 () (@var "X_474" Int)) % 3.94/4.13 (define @t481 () (@var "X_473" Int)) % 3.94/4.13 (define @t482 () (@var "X_472" Int)) % 3.94/4.13 (define @t483 () (@var "X_471" Int)) % 3.94/4.13 (define @t484 () (@var "X_470" Int)) % 3.94/4.13 (define @t485 () (@var "X_468" Int)) % 3.94/4.13 (define @t486 () (@var "X_469" Int)) % 3.94/4.13 (define @t487 () (@var "X_492" Int)) % 3.94/4.13 (define @t488 () (@var "X_491" Int)) % 3.94/4.13 (define @t489 () (@var "X_490" Int)) % 3.94/4.13 (define @t490 () (@var "X_488" Int)) % 3.94/4.13 (define @t491 () (@var "X_480" tptp.set_2)) % 3.94/4.13 (define @t492 () (@var "X_489" Int)) % 3.94/4.13 (define @t493 () (@var "X_487" Int)) % 3.94/4.13 (define @t494 () (@var "X_486" Int)) % 3.94/4.13 (define @t495 () (@var "X_485" Int)) % 3.94/4.13 (define @t496 () (@var "X_484" Int)) % 3.94/4.13 (define @t497 () (@var "X_483" Int)) % 3.94/4.13 (define @t498 () (@var "X_481" Int)) % 3.94/4.13 (define @t499 () (@var "X_482" Int)) % 3.94/4.13 (define @t500 () (not (= tptp.g_s48_48 0))) % 3.94/4.13 (define @t501 () (@var "X_137" Int)) % 3.94/4.13 (define @t502 () (@var "X_136" Int)) % 3.94/4.13 (define @t503 () (@var "X_121" tptp.set_2)) % 3.94/4.13 (define @t504 () (@var "X_135" Int)) % 3.94/4.13 (define @t505 () (@var "X_133" Int)) % 3.94/4.13 (define @t506 () (@var "X_134" Int)) % 3.94/4.13 (define @t507 () (@var "X_131" Int)) % 3.94/4.13 (define @t508 () (@var "X_123" tptp.set_2)) % 3.94/4.13 (define @t509 () (@var "X_132" Int)) % 3.94/4.13 (define @t510 () (@var "X_130" Int)) % 3.94/4.13 (define @t511 () (@var "X_129" Int)) % 3.94/4.13 (define @t512 () (@var "X_120" Int)) % 3.94/4.13 (define @t513 () (@var "X_128" Int)) % 3.94/4.13 (define @t514 () (@var "X_127" Int)) % 3.94/4.13 (define @t515 () (@var "X_126" Int)) % 3.94/4.13 (define @t516 () (@var "X_124" Int)) % 3.94/4.13 (define @t517 () (@var "X_125" Int)) % 3.94/4.13 (define @t518 () (@var "X_122" Int)) % 3.94/4.13 (define @t519 () (@var "X_119" Int)) % 3.94/4.13 (define @t520 () (@var "X_505" Int)) % 3.94/4.13 (define @t521 () (@var "X_504" Int)) % 3.94/4.13 (define @t522 () (@var "X_503" Int)) % 3.94/4.13 (define @t523 () (@var "X_501" Int)) % 3.94/4.13 (define @t524 () (@var "X_493" tptp.set_2)) % 3.94/4.13 (define @t525 () (@var "X_502" Int)) % 3.94/4.13 (define @t526 () (@var "X_500" Int)) % 3.94/4.13 (define @t527 () (@var "X_499" Int)) % 3.94/4.13 (define @t528 () (@var "X_498" Int)) % 3.94/4.13 (define @t529 () (@var "X_497" Int)) % 3.94/4.13 (define @t530 () (@var "X_496" Int)) % 3.94/4.13 (define @t531 () (@var "X_494" Int)) % 3.94/4.13 (define @t532 () (@var "X_495" Int)) % 3.94/4.13 (define @t533 () (@var "X_506" Int)) % 3.94/4.13 (define @t534 () (@var "X_508" Int)) % 3.94/4.13 (define @t535 () (@var "X_507" Int)) % 3.94/4.13 (define @t536 () (@var "X_509" Int)) % 3.94/4.13 (define @t537 () (@var "X_511" Int)) % 3.94/4.13 (define @t538 () (@var "X_510" Int)) % 3.94/4.13 (define @t539 () (@var "X_512" Int)) % 3.94/4.13 (define @t540 () (@var "X_514" Int)) % 3.94/4.13 (define @t541 () (@var "X_513" Int)) % 3.94/4.13 (define @t542 () (@var "X_515" Int)) % 3.94/4.13 (define @t543 () (@var "X_516" Int)) % 3.94/4.13 (define @t544 () (@var "X_517" Int)) % 3.94/4.13 (define @t545 () (@var "X_518" Int)) % 3.94/4.13 (define @t546 () (@var "X_156" Int)) % 3.94/4.13 (define @t547 () (@var "X_155" Int)) % 3.94/4.13 (define @t548 () (@var "X_140" tptp.set_2)) % 3.94/4.13 (define @t549 () (@var "X_154" Int)) % 3.94/4.13 (define @t550 () (@var "X_152" Int)) % 3.94/4.13 (define @t551 () (@var "X_153" Int)) % 3.94/4.13 (define @t552 () (@var "X_150" Int)) % 3.94/4.13 (define @t553 () (@var "X_142" tptp.set_2)) % 3.94/4.13 (define @t554 () (@var "X_151" Int)) % 3.94/4.13 (define @t555 () (@var "X_149" Int)) % 3.94/4.13 (define @t556 () (@var "X_148" Int)) % 3.94/4.13 (define @t557 () (@var "X_139" Int)) % 3.94/4.13 (define @t558 () (@var "X_147" Int)) % 3.94/4.13 (define @t559 () (@var "X_146" Int)) % 3.94/4.13 (define @t560 () (@var "X_145" Int)) % 3.94/4.13 (define @t561 () (@var "X_143" Int)) % 3.94/4.13 (define @t562 () (@var "X_144" Int)) % 3.94/4.13 (define @t563 () (@var "X_141" Int)) % 3.94/4.13 (define @t564 () (@var "X_138" Int)) % 3.94/4.13 (define @t565 () (@var "X_523" Int)) % 3.94/4.13 (define @t566 () (@var "X_522" Int)) % 3.94/4.13 (define @t567 () (@var "X_521" Int)) % 3.94/4.13 (define @t568 () (@var "X_519" Int)) % 3.94/4.13 (define @t569 () (@var "X_520" Int)) % 3.94/4.13 (define @t570 () (@var "X_539" Int)) % 3.94/4.13 (define @t571 () (@var "X_538" Int)) % 3.94/4.13 (define @t572 () (@var "X_537" Int)) % 3.94/4.13 (define @t573 () (@var "X_535" Int)) % 3.94/4.13 (define @t574 () (@var "X_536" Int)) % 3.94/4.13 (define @t575 () (@var "X_533" Int)) % 3.94/4.13 (define @t576 () (@var "X_525" tptp.set_2)) % 3.94/4.13 (define @t577 () (@var "X_534" Int)) % 3.94/4.13 (define @t578 () (@var "X_532" Int)) % 3.94/4.13 (define @t579 () (@var "X_531" Int)) % 3.94/4.13 (define @t580 () (@var "X_524" Int)) % 3.94/4.13 (define @t581 () (@var "X_530" Int)) % 3.94/4.13 (define @t582 () (@var "X_529" Int)) % 3.94/4.13 (define @t583 () (@var "X_528" Int)) % 3.94/4.13 (define @t584 () (@var "X_526" Int)) % 3.94/4.13 (define @t585 () (@var "X_527" Int)) % 3.94/4.13 (define @t586 () (@var "X_540" Int)) % 3.94/4.13 (define @t587 () (@var "X_541" Int)) % 3.94/4.13 (define @t588 () (@var "X_542" Int)) % 3.94/4.13 (define @t589 () (@var "X_543" Int)) % 3.94/4.13 (define @t590 () (@var "X_548" Int)) % 3.94/4.13 (define @t591 () (@var "X_547" Int)) % 3.94/4.13 (define @t592 () (@var "X_546" Int)) % 3.94/4.13 (define @t593 () (@var "X_544" Int)) % 3.94/4.13 (define @t594 () (@var "X_545" Int)) % 3.94/4.13 (define @t595 () (@var "X_564" Int)) % 3.94/4.13 (define @t596 () (@var "X_563" Int)) % 3.94/4.13 (define @t597 () (@var "X_562" Int)) % 3.94/4.13 (define @t598 () (@var "X_560" Int)) % 3.94/4.13 (define @t599 () (@var "X_561" Int)) % 3.94/4.13 (define @t600 () (@var "X_558" Int)) % 3.94/4.13 (define @t601 () (@var "X_550" tptp.set_2)) % 3.94/4.13 (define @t602 () (@var "X_559" Int)) % 3.94/4.13 (define @t603 () (@var "X_557" Int)) % 3.94/4.13 (define @t604 () (@var "X_556" Int)) % 3.94/4.13 (define @t605 () (@var "X_549" Int)) % 3.94/4.13 (define @t606 () (@var "X_555" Int)) % 3.94/4.13 (define @t607 () (@var "X_554" Int)) % 3.94/4.13 (define @t608 () (@var "X_553" Int)) % 3.94/4.13 (define @t609 () (@var "X_551" Int)) % 3.94/4.13 (define @t610 () (@var "X_552" Int)) % 3.94/4.13 (define @t611 () (@var "X_175" Int)) % 3.94/4.13 (define @t612 () (@var "X_174" Int)) % 3.94/4.13 (define @t613 () (@var "X_159" tptp.set_2)) % 3.94/4.13 (define @t614 () (@var "X_173" Int)) % 3.94/4.13 (define @t615 () (@var "X_171" Int)) % 3.94/4.13 (define @t616 () (@var "X_172" Int)) % 3.94/4.13 (define @t617 () (@var "X_169" Int)) % 3.94/4.13 (define @t618 () (@var "X_161" tptp.set_2)) % 3.94/4.13 (define @t619 () (@var "X_170" Int)) % 3.94/4.13 (define @t620 () (@var "X_168" Int)) % 3.94/4.13 (define @t621 () (@var "X_167" Int)) % 3.94/4.13 (define @t622 () (@var "X_158" Int)) % 3.94/4.13 (define @t623 () (@var "X_166" Int)) % 3.94/4.13 (define @t624 () (@var "X_165" Int)) % 3.94/4.13 (define @t625 () (@var "X_164" Int)) % 3.94/4.13 (define @t626 () (@var "X_162" Int)) % 3.94/4.13 (define @t627 () (@var "X_163" Int)) % 3.94/4.13 (define @t628 () (@var "X_160" Int)) % 3.94/4.13 (define @t629 () (@var "X_157" Int)) % 3.94/4.13 (define @t630 () (@var "X_565" Int)) % 3.94/4.13 (define @t631 () (@var "X_570" Int)) % 3.94/4.13 (define @t632 () (@var "X_569" Int)) % 3.94/4.13 (define @t633 () (@var "X_568" Int)) % 3.94/4.13 (define @t634 () (@var "X_566" Int)) % 3.94/4.13 (define @t635 () (@var "X_567" Int)) % 3.94/4.13 (define @t636 () (@var "X_586" Int)) % 3.94/4.13 (define @t637 () (@var "X_585" Int)) % 3.94/4.13 (define @t638 () (@var "X_584" Int)) % 3.94/4.13 (define @t639 () (@var "X_582" Int)) % 3.94/4.13 (define @t640 () (@var "X_583" Int)) % 3.94/4.13 (define @t641 () (@var "X_580" Int)) % 3.94/4.13 (define @t642 () (@var "X_572" tptp.set_2)) % 3.94/4.13 (define @t643 () (@var "X_581" Int)) % 3.94/4.13 (define @t644 () (@var "X_579" Int)) % 3.94/4.13 (define @t645 () (@var "X_578" Int)) % 3.94/4.13 (define @t646 () (@var "X_571" Int)) % 3.94/4.13 (define @t647 () (@var "X_577" Int)) % 3.94/4.13 (define @t648 () (@var "X_576" Int)) % 3.94/4.13 (define @t649 () (@var "X_575" Int)) % 3.94/4.13 (define @t650 () (@var "X_573" Int)) % 3.94/4.13 (define @t651 () (@var "X_574" Int)) % 3.94/4.13 (define @t652 () (@var "X_587" Int)) % 3.94/4.13 (define @t653 () (@var "X_592" Int)) % 3.94/4.13 (define @t654 () (@var "X_591" Int)) % 3.94/4.13 (define @t655 () (@var "X_590" Int)) % 3.94/4.13 (define @t656 () (@var "X_588" Int)) % 3.94/4.13 (define @t657 () (@var "X_589" Int)) % 3.94/4.13 (define @t658 () (@var "X_608" Int)) % 3.94/4.13 (define @t659 () (@var "X_607" Int)) % 3.94/4.13 (define @t660 () (@var "X_606" Int)) % 3.94/4.13 (define @t661 () (@var "X_604" Int)) % 3.94/4.13 (define @t662 () (@var "X_605" Int)) % 3.94/4.13 (define @t663 () (@var "X_602" Int)) % 3.94/4.13 (define @t664 () (@var "X_594" tptp.set_2)) % 3.94/4.13 (define @t665 () (@var "X_603" Int)) % 3.94/4.13 (define @t666 () (@var "X_601" Int)) % 3.94/4.13 (define @t667 () (@var "X_600" Int)) % 3.94/4.13 (define @t668 () (@var "X_593" Int)) % 3.94/4.13 (define @t669 () (@var "X_599" Int)) % 3.94/4.13 (define @t670 () (@var "X_598" Int)) % 3.94/4.13 (define @t671 () (@var "X_597" Int)) % 3.94/4.13 (define @t672 () (@var "X_595" Int)) % 3.94/4.13 (define @t673 () (@var "X_596" Int)) % 3.94/4.13 (define @t674 () (@var "X_194" Int)) % 3.94/4.13 (define @t675 () (@var "X_193" Int)) % 3.94/4.13 (define @t676 () (@var "X_178" tptp.set_2)) % 3.94/4.13 (define @t677 () (@var "X_192" Int)) % 3.94/4.13 (define @t678 () (@var "X_190" Int)) % 3.94/4.13 (define @t679 () (@var "X_191" Int)) % 3.94/4.13 (define @t680 () (@var "X_188" Int)) % 3.94/4.13 (define @t681 () (@var "X_180" tptp.set_2)) % 3.94/4.13 (define @t682 () (@var "X_189" Int)) % 3.94/4.13 (define @t683 () (@var "X_187" Int)) % 3.94/4.13 (define @t684 () (@var "X_186" Int)) % 3.94/4.13 (define @t685 () (@var "X_177" Int)) % 3.94/4.13 (define @t686 () (@var "X_185" Int)) % 3.94/4.13 (define @t687 () (@var "X_184" Int)) % 3.94/4.13 (define @t688 () (@var "X_183" Int)) % 3.94/4.13 (define @t689 () (@var "X_181" Int)) % 3.94/4.13 (define @t690 () (@var "X_182" Int)) % 3.94/4.13 (define @t691 () (@var "X_179" Int)) % 3.94/4.13 (define @t692 () (@var "X_176" Int)) % 3.94/4.13 (define @t693 () (@var "X_609" Int)) % 3.94/4.13 (define @t694 () (@var "X_614" Int)) % 3.94/4.13 (define @t695 () (@var "X_613" Int)) % 3.94/4.13 (define @t696 () (@var "X_612" Int)) % 3.94/4.13 (define @t697 () (@var "X_610" Int)) % 3.94/4.13 (define @t698 () (@var "X_611" Int)) % 3.94/4.13 (define @t699 () (@var "X_630" Int)) % 3.94/4.13 (define @t700 () (@var "X_629" Int)) % 3.94/4.13 (define @t701 () (@var "X_628" Int)) % 3.94/4.13 (define @t702 () (@var "X_626" Int)) % 3.94/4.13 (define @t703 () (@var "X_627" Int)) % 3.94/4.13 (define @t704 () (@var "X_624" Int)) % 3.94/4.13 (define @t705 () (@var "X_616" tptp.set_2)) % 3.94/4.13 (define @t706 () (@var "X_625" Int)) % 3.94/4.13 (define @t707 () (@var "X_623" Int)) % 3.94/4.13 (define @t708 () (@var "X_622" Int)) % 3.94/4.13 (define @t709 () (@var "X_615" Int)) % 3.94/4.13 (define @t710 () (@var "X_621" Int)) % 3.94/4.13 (define @t711 () (@var "X_620" Int)) % 3.94/4.13 (define @t712 () (@var "X_619" Int)) % 3.94/4.13 (define @t713 () (@var "X_617" Int)) % 3.94/4.13 (define @t714 () (@var "X_618" Int)) % 3.94/4.13 (define @t715 () (@var "X_631" Int)) % 3.94/4.13 (define @t716 () (@var "X_632" Int)) % 3.94/4.13 (define @t717 () (@var "X_633" Int)) % 3.94/4.13 (define @t718 () (@var "X_634" Int)) % 3.94/4.13 (define @t719 () (@var "X_722" Int)) % 3.94/4.13 (define @t720 () (tptp.mem0 @t719 tptp.g_s22_22)) % 3.94/4.13 (define @t721 () (@var "X_723" Int)) % 3.94/4.13 (define @t722 () (@var "X_724" Int)) % 3.94/4.13 (define @t723 () (tptp.mem0 @t722 tptp.g_s25_25)) % 3.94/4.13 (define @t724 () (@var "X_725" Int)) % 3.94/4.13 (define @t725 () (@var "X_806" Int)) % 3.94/4.13 (define @t726 () (@var "X_798" tptp.set_2)) % 3.94/4.13 (define @t727 () (@var "X_807" Int)) % 3.94/4.13 (define @t728 () (@var "X_805" Int)) % 3.94/4.13 (define @t729 () (@var "X_804" Int)) % 3.94/4.13 (define @t730 () (@var "X_803" Int)) % 3.94/4.13 (define @t731 () (@var "X_802" Int)) % 3.94/4.13 (define @t732 () (@var "X_801" Int)) % 3.94/4.13 (define @t733 () (@var "X_799" Int)) % 3.94/4.13 (define @t734 () (@var "X_800" Int)) % 3.94/4.13 (define @t735 () (@var "X_816" Int)) % 3.94/4.13 (define @t736 () (@var "X_808" tptp.set_2)) % 3.94/4.13 (define @t737 () (@var "X_817" Int)) % 3.94/4.13 (define @t738 () (@var "X_815" Int)) % 3.94/4.13 (define @t739 () (@var "X_814" Int)) % 3.94/4.13 (define @t740 () (@var "X_813" Int)) % 3.94/4.13 (define @t741 () (@var "X_812" Int)) % 3.94/4.13 (define @t742 () (@var "X_811" Int)) % 3.94/4.13 (define @t743 () (@var "X_809" Int)) % 3.94/4.13 (define @t744 () (@var "X_810" Int)) % 3.94/4.13 (define @t745 () (@var "X_826" Int)) % 3.94/4.13 (define @t746 () (@var "X_818" tptp.set_2)) % 3.94/4.13 (define @t747 () (@var "X_827" Int)) % 3.94/4.13 (define @t748 () (@var "X_825" Int)) % 3.94/4.13 (define @t749 () (@var "X_824" Int)) % 3.94/4.13 (define @t750 () (@var "X_823" Int)) % 3.94/4.13 (define @t751 () (@var "X_822" Int)) % 3.94/4.13 (define @t752 () (@var "X_821" Int)) % 3.94/4.13 (define @t753 () (@var "X_819" Int)) % 3.94/4.13 (define @t754 () (@var "X_820" Int)) % 3.94/4.13 (define @t755 () (@var "X_836" Int)) % 3.94/4.13 (define @t756 () (@var "X_828" tptp.set_2)) % 3.94/4.13 (define @t757 () (@var "X_837" Int)) % 3.94/4.13 (define @t758 () (@var "X_835" Int)) % 3.94/4.13 (define @t759 () (@var "X_834" Int)) % 3.94/4.13 (define @t760 () (@var "X_833" Int)) % 3.94/4.13 (define @t761 () (@var "X_832" Int)) % 3.94/4.13 (define @t762 () (@var "X_831" Int)) % 3.94/4.13 (define @t763 () (@var "X_829" Int)) % 3.94/4.13 (define @t764 () (@var "X_830" Int)) % 3.94/4.13 (define @t765 () (@var "X_846" Int)) % 3.94/4.13 (define @t766 () (tptp.mem0 @t765 tptp.g_s6_6)) % 3.94/4.13 (define @t767 () (@var "X_838" tptp.set_2)) % 3.94/4.13 (define @t768 () (@var "X_847" Int)) % 3.94/4.13 (define @t769 () (tptp.mem2 @t768 @t765 @t767)) % 3.94/4.13 (define @t770 () (@list @t768)) % 3.94/4.13 (define @t771 () (exists @t770 @t769)) % 3.94/4.13 (define @t772 () (=> @t771 @t766)) % 3.94/4.13 (define @t773 () (@list @t765)) % 3.94/4.13 (define @t774 () (forall @t773 @t772)) % 3.94/4.13 (define @t775 () (@var "X_845" Int)) % 3.94/4.13 (define @t776 () (@var "X_844" Int)) % 3.94/4.13 (define @t777 () (tptp.mem2 @t776 @t775 @t767)) % 3.94/4.13 (define @t778 () (@list @t775)) % 3.94/4.13 (define @t779 () (exists @t778 @t777)) % 3.94/4.13 (define @t780 () (tptp.mem0 @t776 tptp.g_s65_65)) % 3.94/4.13 (define @t781 () (= @t780 @t779)) % 3.94/4.13 (define @t782 () (@list @t776)) % 3.94/4.13 (define @t783 () (forall @t782 @t781)) % 3.94/4.13 (define @t784 () (@var "X_843" Int)) % 3.94/4.13 (define @t785 () (@var "X_842" Int)) % 3.94/4.13 (define @t786 () (= @t785 @t784)) % 3.94/4.13 (define @t787 () (@var "X_841" Int)) % 3.94/4.13 (define @t788 () (tptp.mem2 @t787 @t784 @t767)) % 3.94/4.13 (define @t789 () (tptp.mem2 @t787 @t785 @t767)) % 3.94/4.13 (define @t790 () (and @t789 @t788)) % 3.94/4.13 (define @t791 () (@list @t787 @t785 @t784)) % 3.94/4.13 (define @t792 () (forall @t791 (=> @t790 @t786))) % 3.94/4.13 (define @t793 () (@var "X_839" Int)) % 3.94/4.13 (define @t794 () (@var "X_840" Int)) % 3.94/4.13 (define @t795 () (tptp.mem2 @t794 @t793 tptp.g_s104_89)) % 3.94/4.13 (define @t796 () (@list @t793 @t794)) % 3.94/4.13 (define @t797 () (forall @t796 (= (tptp.mem2 @t794 @t793 @t767) @t795))) % 3.94/4.13 (define @t798 () (and @t797 @t792 @t783 @t774)) % 3.94/4.13 (define @t799 () (@list @t767)) % 3.94/4.13 (define @t800 () (exists @t799 @t798)) % 3.94/4.13 (define @t801 () (@var "X_856" Int)) % 3.94/4.13 (define @t802 () (@var "X_848" tptp.set_2)) % 3.94/4.13 (define @t803 () (@var "X_857" Int)) % 3.94/4.13 (define @t804 () (@var "X_855" Int)) % 3.94/4.13 (define @t805 () (@var "X_854" Int)) % 3.94/4.13 (define @t806 () (@var "X_853" Int)) % 3.94/4.13 (define @t807 () (@var "X_852" Int)) % 3.94/4.13 (define @t808 () (@var "X_851" Int)) % 3.94/4.13 (define @t809 () (@var "X_849" Int)) % 3.94/4.13 (define @t810 () (@var "X_850" Int)) % 3.94/4.13 (define @t811 () (@var "X_866" Int)) % 3.94/4.13 (define @t812 () (@var "X_858" tptp.set_2)) % 3.94/4.13 (define @t813 () (@var "X_867" Int)) % 3.94/4.13 (define @t814 () (@var "X_865" Int)) % 3.94/4.13 (define @t815 () (@var "X_864" Int)) % 3.94/4.13 (define @t816 () (@var "X_863" Int)) % 3.94/4.13 (define @t817 () (@var "X_862" Int)) % 3.94/4.13 (define @t818 () (@var "X_861" Int)) % 3.94/4.13 (define @t819 () (@var "X_859" Int)) % 3.94/4.13 (define @t820 () (@var "X_860" Int)) % 3.94/4.13 (define @t821 () (@var "X_876" Int)) % 3.94/4.13 (define @t822 () (@var "X_868" tptp.set_2)) % 3.94/4.13 (define @t823 () (@var "X_877" Int)) % 3.94/4.13 (define @t824 () (@var "X_875" Int)) % 3.94/4.14 (define @t825 () (@var "X_874" Int)) % 3.94/4.14 (define @t826 () (@var "X_873" Int)) % 3.94/4.14 (define @t827 () (@var "X_872" Int)) % 3.94/4.14 (define @t828 () (@var "X_871" Int)) % 3.94/4.14 (define @t829 () (@var "X_869" Int)) % 3.94/4.14 (define @t830 () (@var "X_870" Int)) % 3.94/4.14 (define @t831 () (@var "X_886" Int)) % 3.94/4.14 (define @t832 () (@var "X_878" tptp.set_2)) % 3.94/4.14 (define @t833 () (@var "X_887" Int)) % 3.94/4.14 (define @t834 () (@var "X_885" Int)) % 3.94/4.14 (define @t835 () (@var "X_884" Int)) % 3.94/4.14 (define @t836 () (@var "X_883" Int)) % 3.94/4.14 (define @t837 () (@var "X_882" Int)) % 3.94/4.14 (define @t838 () (@var "X_881" Int)) % 3.94/4.14 (define @t839 () (@var "X_879" Int)) % 3.94/4.14 (define @t840 () (@var "X_880" Int)) % 3.94/4.14 (define @t841 () (@var "X_726" Int)) % 3.94/4.14 (define @t842 () (tptp.mem0 @t841 tptp.g_s71_71)) % 3.94/4.14 (define @t843 () (@var "X_727" Int)) % 3.94/4.14 (define @t844 () (@var "X_736" Int)) % 3.94/4.14 (define @t845 () (@var "X_728" tptp.set_2)) % 3.94/4.14 (define @t846 () (@var "X_737" Int)) % 3.94/4.14 (define @t847 () (@var "X_735" Int)) % 3.94/4.14 (define @t848 () (@var "X_734" Int)) % 3.94/4.14 (define @t849 () (@var "X_733" Int)) % 3.94/4.14 (define @t850 () (@var "X_732" Int)) % 3.94/4.14 (define @t851 () (@var "X_731" Int)) % 3.94/4.14 (define @t852 () (@var "X_729" Int)) % 3.94/4.14 (define @t853 () (@var "X_730" Int)) % 3.94/4.14 (define @t854 () (@var "X_746" Int)) % 3.94/4.14 (define @t855 () (@var "X_738" tptp.set_2)) % 3.94/4.14 (define @t856 () (@var "X_747" Int)) % 3.94/4.14 (define @t857 () (@var "X_745" Int)) % 3.94/4.14 (define @t858 () (@var "X_744" Int)) % 3.94/4.14 (define @t859 () (@var "X_743" Int)) % 3.94/4.14 (define @t860 () (@var "X_742" Int)) % 3.94/4.14 (define @t861 () (@var "X_741" Int)) % 3.94/4.14 (define @t862 () (@var "X_739" Int)) % 3.94/4.14 (define @t863 () (@var "X_740" Int)) % 3.94/4.14 (define @t864 () (@var "X_756" Int)) % 3.94/4.14 (define @t865 () (@var "X_748" tptp.set_2)) % 3.94/4.14 (define @t866 () (@var "X_757" Int)) % 3.94/4.14 (define @t867 () (@var "X_755" Int)) % 3.94/4.14 (define @t868 () (@var "X_754" Int)) % 3.94/4.14 (define @t869 () (@var "X_753" Int)) % 3.94/4.14 (define @t870 () (@var "X_752" Int)) % 3.94/4.14 (define @t871 () (@var "X_751" Int)) % 3.94/4.14 (define @t872 () (@var "X_749" Int)) % 3.94/4.14 (define @t873 () (@var "X_750" Int)) % 3.94/4.14 (define @t874 () (@var "X_766" Int)) % 3.94/4.14 (define @t875 () (@var "X_758" tptp.set_2)) % 3.94/4.14 (define @t876 () (@var "X_767" Int)) % 3.94/4.14 (define @t877 () (@var "X_765" Int)) % 3.94/4.14 (define @t878 () (@var "X_764" Int)) % 3.94/4.14 (define @t879 () (@var "X_763" Int)) % 3.94/4.14 (define @t880 () (@var "X_762" Int)) % 3.94/4.14 (define @t881 () (@var "X_761" Int)) % 3.94/4.14 (define @t882 () (@var "X_759" Int)) % 3.94/4.14 (define @t883 () (@var "X_760" Int)) % 3.94/4.14 (define @t884 () (@var "X_776" Int)) % 3.94/4.14 (define @t885 () (@var "X_768" tptp.set_2)) % 3.94/4.14 (define @t886 () (@var "X_777" Int)) % 3.94/4.14 (define @t887 () (@var "X_775" Int)) % 3.94/4.14 (define @t888 () (@var "X_774" Int)) % 3.94/4.14 (define @t889 () (@var "X_773" Int)) % 3.94/4.14 (define @t890 () (@var "X_772" Int)) % 3.94/4.14 (define @t891 () (@var "X_771" Int)) % 3.94/4.14 (define @t892 () (@var "X_769" Int)) % 3.94/4.14 (define @t893 () (@var "X_770" Int)) % 3.94/4.14 (define @t894 () (@var "X_786" Int)) % 3.94/4.14 (define @t895 () (@var "X_778" tptp.set_2)) % 3.94/4.14 (define @t896 () (@var "X_787" Int)) % 3.94/4.14 (define @t897 () (@var "X_785" Int)) % 3.94/4.14 (define @t898 () (@var "X_784" Int)) % 3.94/4.14 (define @t899 () (@var "X_783" Int)) % 3.94/4.14 (define @t900 () (@var "X_782" Int)) % 3.94/4.14 (define @t901 () (@var "X_781" Int)) % 3.94/4.14 (define @t902 () (@var "X_779" Int)) % 3.94/4.14 (define @t903 () (@var "X_780" Int)) % 3.94/4.14 (define @t904 () (@var "X_796" Int)) % 3.94/4.14 (define @t905 () (@var "X_788" tptp.set_2)) % 3.94/4.14 (define @t906 () (@var "X_797" Int)) % 3.94/4.14 (define @t907 () (@var "X_795" Int)) % 3.94/4.14 (define @t908 () (@var "X_794" Int)) % 3.94/4.14 (define @t909 () (@var "X_793" Int)) % 3.94/4.14 (define @t910 () (@var "X_792" Int)) % 3.94/4.14 (define @t911 () (@var "X_791" Int)) % 3.94/4.14 (define @t912 () (@var "X_789" Int)) % 3.94/4.14 (define @t913 () (@var "X_790" Int)) % 3.94/4.14 (define @t914 () (@var "X_957" Int)) % 3.94/4.14 (define @t915 () (@var "X_956" Int)) % 3.94/4.14 (define @t916 () (= @t915 @t914)) % 3.94/4.14 (define @t917 () (tptp.mem0 @t914 tptp.g_s37_37)) % 3.94/4.14 (define @t918 () (@var "X_955" Int)) % 3.94/4.14 (define @t919 () (tptp.mem0 @t918 tptp.g_s66_66)) % 3.94/4.14 (define @t920 () (tptp.mem2 @t918 @t914 tptp.g_s104_89)) % 3.94/4.14 (define @t921 () (tptp.mem0 @t915 tptp.g_s37_37)) % 3.94/4.14 (define @t922 () (tptp.mem2 @t918 @t915 tptp.g_s104_89)) % 3.94/4.14 (define @t923 () (and @t922 @t919 @t921 @t920 @t919 @t917)) % 3.94/4.14 (define @t924 () (@list @t918 @t915 @t914)) % 3.94/4.14 (define @t925 () (forall @t924 (=> @t923 @t916))) % 3.94/4.14 (define @t926 () (@var "X_953" Int)) % 3.94/4.14 (define @t927 () (tptp.mem0 @t926 tptp.g_s37_37)) % 3.94/4.14 (define @t928 () (@var "X_954" Int)) % 3.94/4.14 (define @t929 () (tptp.mem0 @t928 tptp.g_s66_66)) % 3.94/4.14 (define @t930 () (and @t929 @t927)) % 3.94/4.14 (define @t931 () (tptp.mem2 @t928 @t926 tptp.g_s104_89)) % 3.94/4.14 (define @t932 () (and @t931 @t929 @t927)) % 3.94/4.14 (define @t933 () (@list @t926 @t928)) % 3.94/4.14 (define @t934 () (forall @t933 (=> @t932 @t930))) % 3.94/4.14 (define @t935 () (and @t934 @t925)) % 3.94/4.14 (define @t936 () (not @t935)) % 3.94/4.14 (define @t937 () (@var "BOUND_VARIABLE_14855" Int)) % 3.94/4.14 (define @t938 () (not (tptp.mem2 @t937 @t765 @t767))) % 3.94/4.14 (define @t939 () (or @t938 @t766)) % 3.94/4.14 (define @t940 () (@list @t765 @t937)) % 3.94/4.14 (define @t941 () (forall @t940 @t939)) % 3.94/4.14 (define @t942 () (not @t941)) % 3.94/4.14 (define @t943 () (not (forall @t778 (not @t777)))) % 3.94/4.14 (define @t944 () (forall @t782 (= @t780 @t943))) % 3.94/4.14 (define @t945 () (not @t944)) % 3.94/4.14 (define @t946 () (not @t788)) % 3.94/4.14 (define @t947 () (not @t789)) % 3.94/4.14 (define @t948 () (or @t947 @t946 @t786)) % 3.94/4.14 (define @t949 () (forall @t791 @t948)) % 3.94/4.14 (define @t950 () (not @t949)) % 3.94/4.14 (define @t951 () (not @t797)) % 3.94/4.14 (define @t952 () (or @t951 @t950 @t945 @t942)) % 3.94/4.14 (define @t953 () (and @t797 @t949 @t944 @t941)) % 3.94/4.14 (define @t954 () (forall @t799 (not @t953))) % 3.94/4.14 (define @t955 () (not @t954)) % 3.94/4.14 (define @t956 () (@list @t937)) % 3.94/4.14 (define @t957 () (forall @t956 @t939)) % 3.94/4.14 (define @t958 () (forall @t956 @t938)) % 3.94/4.14 (define @t959 () (or @t958 @t766)) % 3.94/4.14 (define @t960 () (forall @t770 (not @t769))) % 3.94/4.14 (define @t961 () (not @t960)) % 3.94/4.14 (define @t962 () (forall @t799 @t952)) % 3.94/4.14 (define @t963 () (@quantifiers_skolemize @t962 0)) % 3.94/4.14 (define @t964 () (not (forall @t940 (or (not (tptp.mem2 @t937 @t765 @t963)) @t766)))) % 3.94/4.14 (define @t965 () (not (forall @t782 (= @t780 (not (forall @t778 (not (tptp.mem2 @t776 @t775 @t963)))))))) % 3.94/4.14 (define @t966 () (forall @t791 (or (not (tptp.mem2 @t787 @t785 @t963)) (not (tptp.mem2 @t787 @t784 @t963)) @t786))) % 3.94/4.14 (define @t967 () (not @t966)) % 3.94/4.14 (define @t968 () (tptp.mem2 @t794 @t793 @t963)) % 3.94/4.14 (define @t969 () (forall @t796 (= @t795 @t968))) % 3.94/4.14 (define @t970 () (not @t969)) % 3.94/4.14 (define @t971 () (or @t970 @t967 @t965 @t964)) % 3.94/4.14 (define @t972 () (not @t971)) % 3.94/4.14 (define @t973 () (not @t962)) % 3.94/4.14 (define @t974 () (forall @t796 (= @t968 @t795))) % 3.94/4.14 (define @t975 () (not @t974)) % 3.94/4.14 (define @t976 () (or @t975 @t967 @t965 @t964)) % 3.94/4.14 (define @t977 () (not @t976)) % 3.94/4.14 (define @t978 () (@list true)) % 3.94/4.14 (define @t979 () (@list @t971)) % 3.94/4.14 (define @t980 () (not @t917)) % 3.94/4.14 (define @t981 () (not @t920)) % 3.94/4.14 (define @t982 () (not @t921)) % 3.94/4.14 (define @t983 () (not @t919)) % 3.94/4.14 (define @t984 () (not @t922)) % 3.94/4.14 (define @t985 () (or @t984 @t983 @t982 @t981 @t980 @t916)) % 3.94/4.14 (define @t986 () (forall @t924 @t985)) % 3.94/4.14 (define @t987 () (@quantifiers_skolemize @t986 2)) % 3.94/4.14 (define @t988 () (@quantifiers_skolemize @t986 1)) % 3.94/4.14 (define @t989 () (= @t988 @t987)) % 3.94/4.14 (define @t990 () (= @t987 @t988)) % 3.94/4.14 (define @t991 () (@quantifiers_skolemize @t986 0)) % 3.94/4.14 (define @t992 () (tptp.mem2 @t991 @t988 @t963)) % 3.94/4.14 (define @t993 () (not @t992)) % 3.94/4.14 (define @t994 () (tptp.mem2 @t991 @t987 @t963)) % 3.94/4.14 (define @t995 () (not @t994)) % 3.94/4.14 (define @t996 () (or @t995 @t993 @t990)) % 3.94/4.14 (define @t997 () (or @t995 @t993 @t989)) % 3.94/4.14 (define @t998 () (@list false)) % 3.94/4.14 (define @t999 () (not @t927)) % 3.94/4.14 (define @t1000 () (not @t929)) % 3.94/4.14 (define @t1001 () (not @t931)) % 3.94/4.14 (define @t1002 () (or @t1001 @t1000 @t999 @t930)) % 3.94/4.14 (define @t1003 () (forall @t933 @t1002)) % 3.94/4.14 (define @t1004 () (@quantifiers_skolemize @t1003 1)) % 3.94/4.14 (define @t1005 () (tptp.mem0 @t1004 tptp.g_s66_66)) % 3.94/4.14 (define @t1006 () (@quantifiers_skolemize @t1003 0)) % 3.94/4.14 (define @t1007 () (tptp.mem0 @t1006 tptp.g_s37_37)) % 3.94/4.14 (define @t1008 () (and @t1005 @t1007)) % 3.94/4.14 (define @t1009 () (not @t1007)) % 3.94/4.14 (define @t1010 () (not @t1005)) % 3.94/4.14 (define @t1011 () (or (not (tptp.mem2 @t1004 @t1006 tptp.g_s104_89)) @t1010 @t1009 @t1008)) % 3.94/4.14 (define @t1012 () (@list true false false)) % 3.94/4.14 (define @t1013 () (not @t1011)) % 3.94/4.14 (define @t1014 () (not @t1003)) % 3.94/4.14 (define @t1015 () (or @t984 @t983 @t982 @t981 @t980)) % 3.94/4.14 (define @t1016 () (or @t984 @t983 @t982 @t981 @t983 @t980)) % 3.94/4.14 (define @t1017 () (or @t1001 @t1000 @t999)) % 3.94/4.14 (define @t1018 () (not @t986)) % 3.94/4.14 (define @t1019 () (tptp.mem2 @t991 @t987 tptp.g_s104_89)) % 3.94/4.14 (define @t1020 () (not @t1019)) % 3.94/4.14 (define @t1021 () (tptp.mem2 @t991 @t988 tptp.g_s104_89)) % 3.94/4.14 (define @t1022 () (not @t1021)) % 3.94/4.14 (define @t1023 () (or @t1022 (not (tptp.mem0 @t991 tptp.g_s66_66)) (not (tptp.mem0 @t988 tptp.g_s37_37)) @t1020 (not (tptp.mem0 @t987 tptp.g_s37_37)) @t989)) % 3.94/4.14 (define @t1024 () (not @t1023)) % 3.94/4.14 (define @t1025 () (@list @t1023)) % 3.94/4.14 (define @t1026 () (= @t1019 @t994)) % 3.94/4.14 (define @t1027 () (= @t1021 @t992)) % 3.94/4.14 (define @t1028 () (not @t1027)) % 3.94/4.14 (assume @p1 (= tptp.min_int (- 2147483648))) % 3.94/4.14 (assume @p2 (= tptp.max_int 2147483647)) % 3.94/4.14 (assume @p3 (and (not (forall (@list @t19) (= (tptp.mem0 @t19 tptp.g_s0_0) false))) (forall (@list @t18) (=> (tptp.mem0 @t18 tptp.g_s0_0) true)) (exists (@list @t12 @t3) (and (exists (@list @t8) (and (forall (@list @t16 @t17) (= (tptp.mem2 @t17 @t16 @t8) (tptp.mem2 @t17 @t16 @t3))) (forall (@list @t15 @t14 @t13) (=> (and (tptp.mem2 @t15 @t14 @t8) (tptp.mem2 @t15 @t13 @t8)) (= @t14 @t13))) (forall (@list @t11) (= (and (>= @t11 1) (<= @t11 @t12)) (exists (@list @t10) (tptp.mem2 @t11 @t10 @t8)))) (forall (@list @t7) (=> (exists (@list @t9) (tptp.mem2 @t9 @t7 @t8)) (tptp.mem0 @t7 tptp.g_s0_0))))) (forall (@list @t5) (=> (tptp.mem0 @t5 tptp.g_s0_0) (exists (@list @t6) (tptp.mem2 @t6 @t5 @t3)))) (forall (@list @t4 @t2 @t1) (=> (and (tptp.mem2 @t2 @t4 @t3) (tptp.mem2 @t1 @t4 @t3)) (= @t2 @t1))))))) % 3.94/4.14 (assume @p4 (and (not (forall (@list @t38) (= (tptp.mem0 @t38 tptp.g_s1_1) false))) (forall (@list @t37) (=> (tptp.mem0 @t37 tptp.g_s1_1) true)) (exists (@list @t31 @t22) (and (exists (@list @t27) (and (forall (@list @t35 @t36) (= (tptp.mem2 @t36 @t35 @t27) (tptp.mem2 @t36 @t35 @t22))) (forall (@list @t34 @t33 @t32) (=> (and (tptp.mem2 @t34 @t33 @t27) (tptp.mem2 @t34 @t32 @t27)) (= @t33 @t32))) (forall (@list @t30) (= (and (>= @t30 1) (<= @t30 @t31)) (exists (@list @t29) (tptp.mem2 @t30 @t29 @t27)))) (forall (@list @t26) (=> (exists (@list @t28) (tptp.mem2 @t28 @t26 @t27)) (tptp.mem0 @t26 tptp.g_s1_1))))) (forall (@list @t24) (=> (tptp.mem0 @t24 tptp.g_s1_1) (exists (@list @t25) (tptp.mem2 @t25 @t24 @t22)))) (forall (@list @t23 @t21 @t20) (=> (and (tptp.mem2 @t21 @t23 @t22) (tptp.mem2 @t20 @t23 @t22)) (= @t21 @t20))))))) % 3.94/4.14 (assume @p5 (and (not (forall (@list @t57) (= (tptp.mem0 @t57 tptp.g_s10_10) false))) (forall (@list @t56) (=> (tptp.mem0 @t56 tptp.g_s10_10) true)) (exists (@list @t50 @t41) (and (exists (@list @t46) (and (forall (@list @t54 @t55) (= (tptp.mem2 @t55 @t54 @t46) (tptp.mem2 @t55 @t54 @t41))) (forall (@list @t53 @t52 @t51) (=> (and (tptp.mem2 @t53 @t52 @t46) (tptp.mem2 @t53 @t51 @t46)) (= @t52 @t51))) (forall (@list @t49) (= (and (>= @t49 1) (<= @t49 @t50)) (exists (@list @t48) (tptp.mem2 @t49 @t48 @t46)))) (forall (@list @t45) (=> (exists (@list @t47) (tptp.mem2 @t47 @t45 @t46)) (tptp.mem0 @t45 tptp.g_s10_10))))) (forall (@list @t43) (=> (tptp.mem0 @t43 tptp.g_s10_10) (exists (@list @t44) (tptp.mem2 @t44 @t43 @t41)))) (forall (@list @t42 @t40 @t39) (=> (and (tptp.mem2 @t40 @t42 @t41) (tptp.mem2 @t39 @t42 @t41)) (= @t40 @t39))))))) % 3.94/4.14 (assume @p6 (not (tptp.mem0 tptp.g_s63_63 tptp.g_s66_66))) % 3.94/4.14 (assume @p7 (and (forall (@list @t61 @t62) (=> (tptp.mem2 @t62 @t61 tptp.g_s67_67) (and (>= @t62 0) (<= @t62 tptp.max_int) (tptp.mem0 @t61 tptp.g_s65_65)))) (forall (@list @t60 @t59 @t58) (=> (and (tptp.mem2 @t60 @t59 tptp.g_s67_67) (tptp.mem2 @t60 @t58 tptp.g_s67_67)) (= @t59 @t58))))) % 3.94/4.14 (assume @p8 (exists (@list @t73) (and (exists (@list @t69) (and (forall (@list @t77 @t78) (= (tptp.mem2 @t78 @t77 @t69) (tptp.mem2 @t78 @t77 tptp.g_s67_67))) (forall (@list @t76 @t75 @t74) (=> (and (tptp.mem2 @t76 @t75 @t69) (tptp.mem2 @t76 @t74 @t69)) (= @t75 @t74))) (forall (@list @t72) (= (and (>= @t72 1) (<= @t72 @t73)) (exists (@list @t71) (tptp.mem2 @t72 @t71 @t69)))) (forall (@list @t68) (=> (exists (@list @t70) (tptp.mem2 @t70 @t68 @t69)) (tptp.mem0 @t68 tptp.g_s66_66))))) (forall (@list @t66) (=> (tptp.mem0 @t66 tptp.g_s66_66) (exists (@list @t67) (tptp.mem2 @t67 @t66 tptp.g_s67_67)))) (forall (@list @t65 @t64 @t63) (=> (and (tptp.mem2 @t64 @t65 tptp.g_s67_67) (tptp.mem2 @t63 @t65 tptp.g_s67_67)) (= @t64 @t63)))))) % 3.94/4.14 (assume @p9 (forall (@list @t79) (=> (tptp.mem0 @t79 tptp.g_s68_68) (tptp.mem0 @t79 tptp.g_s12_12)))) % 3.94/4.14 (assume @p10 (tptp.mem0 tptp.g_s69_69 tptp.g_s12_12)) % 3.94/4.14 (assume @p11 (not (tptp.mem0 tptp.g_s69_69 tptp.g_s68_68))) % 3.94/4.14 (assume @p12 (and (forall (@list @t83 @t84) (=> (tptp.mem2 @t84 @t83 tptp.g_s70_70) (and (>= @t84 0) (<= @t84 tptp.max_int) (tptp.mem0 @t83 tptp.g_s12_12)))) (forall (@list @t82 @t81 @t80) (=> (and (tptp.mem2 @t82 @t81 tptp.g_s70_70) (tptp.mem2 @t82 @t80 tptp.g_s70_70)) (= @t81 @t80))))) % 3.94/4.14 (assume @p13 (exists (@list @t95) (and (exists (@list @t91) (and (forall (@list @t99 @t100) (= (tptp.mem2 @t100 @t99 @t91) (tptp.mem2 @t100 @t99 tptp.g_s70_70))) (forall (@list @t98 @t97 @t96) (=> (and (tptp.mem2 @t98 @t97 @t91) (tptp.mem2 @t98 @t96 @t91)) (= @t97 @t96))) (forall (@list @t94) (= (and (>= @t94 1) (<= @t94 @t95)) (exists (@list @t93) (tptp.mem2 @t94 @t93 @t91)))) (forall (@list @t90) (=> (exists (@list @t92) (tptp.mem2 @t92 @t90 @t91)) (tptp.mem0 @t90 tptp.g_s68_68))))) (forall (@list @t88) (=> (tptp.mem0 @t88 tptp.g_s68_68) (exists (@list @t89) (tptp.mem2 @t89 @t88 tptp.g_s70_70)))) (forall (@list @t87 @t86 @t85) (=> (and (tptp.mem2 @t86 @t87 tptp.g_s70_70) (tptp.mem2 @t85 @t87 tptp.g_s70_70)) (= @t86 @t85)))))) % 3.94/4.14 (assume @p14 (forall (@list @t101) (=> (tptp.mem0 @t101 tptp.g_s71_71) (tptp.mem0 @t101 tptp.g_s13_13)))) % 3.94/4.14 (assume @p15 (tptp.mem0 tptp.g_s72_72 tptp.g_s13_13)) % 3.94/4.14 (assume @p16 (and (not (forall (@list @t120) (= (tptp.mem0 @t120 tptp.g_s11_11) false))) (forall (@list @t119) (=> (tptp.mem0 @t119 tptp.g_s11_11) true)) (exists (@list @t113 @t104) (and (exists (@list @t109) (and (forall (@list @t117 @t118) (= (tptp.mem2 @t118 @t117 @t109) (tptp.mem2 @t118 @t117 @t104))) (forall (@list @t116 @t115 @t114) (=> (and (tptp.mem2 @t116 @t115 @t109) (tptp.mem2 @t116 @t114 @t109)) (= @t115 @t114))) (forall (@list @t112) (= (and (>= @t112 1) (<= @t112 @t113)) (exists (@list @t111) (tptp.mem2 @t112 @t111 @t109)))) (forall (@list @t108) (=> (exists (@list @t110) (tptp.mem2 @t110 @t108 @t109)) (tptp.mem0 @t108 tptp.g_s11_11))))) (forall (@list @t106) (=> (tptp.mem0 @t106 tptp.g_s11_11) (exists (@list @t107) (tptp.mem2 @t107 @t106 @t104)))) (forall (@list @t105 @t103 @t102) (=> (and (tptp.mem2 @t103 @t105 @t104) (tptp.mem2 @t102 @t105 @t104)) (= @t103 @t102))))))) % 3.94/4.14 (assume @p17 (not (tptp.mem0 tptp.g_s72_72 tptp.g_s71_71))) % 3.94/4.14 (assume @p18 (and (forall (@list @t124 @t125) (=> (tptp.mem2 @t125 @t124 tptp.g_s73_73) (and (>= @t125 0) (<= @t125 tptp.max_int) (tptp.mem0 @t124 tptp.g_s13_13)))) (forall (@list @t123 @t122 @t121) (=> (and (tptp.mem2 @t123 @t122 tptp.g_s73_73) (tptp.mem2 @t123 @t121 tptp.g_s73_73)) (= @t122 @t121))))) % 3.94/4.14 (assume @p19 (exists (@list @t136) (and (exists (@list @t132) (and (forall (@list @t140 @t141) (= (tptp.mem2 @t141 @t140 @t132) (tptp.mem2 @t141 @t140 tptp.g_s73_73))) (forall (@list @t139 @t138 @t137) (=> (and (tptp.mem2 @t139 @t138 @t132) (tptp.mem2 @t139 @t137 @t132)) (= @t138 @t137))) (forall (@list @t135) (= (and (>= @t135 1) (<= @t135 @t136)) (exists (@list @t134) (tptp.mem2 @t135 @t134 @t132)))) (forall (@list @t131) (=> (exists (@list @t133) (tptp.mem2 @t133 @t131 @t132)) (tptp.mem0 @t131 tptp.g_s71_71))))) (forall (@list @t129) (=> (tptp.mem0 @t129 tptp.g_s71_71) (exists (@list @t130) (tptp.mem2 @t130 @t129 tptp.g_s73_73)))) (forall (@list @t128 @t127 @t126) (=> (and (tptp.mem2 @t127 @t128 tptp.g_s73_73) (tptp.mem2 @t126 @t128 tptp.g_s73_73)) (= @t127 @t126)))))) % 3.94/4.14 (assume @p20 (forall (@list @t142) (=> (tptp.mem0 @t142 tptp.g_s74_74) (tptp.mem0 @t142 tptp.g_s14_14)))) % 3.94/4.14 (assume @p21 (tptp.mem0 tptp.g_s75_75 tptp.g_s14_14)) % 3.94/4.14 (assume @p22 (not (tptp.mem0 tptp.g_s75_75 tptp.g_s74_74))) % 3.94/4.14 (assume @p23 (and (forall (@list @t146 @t147) (=> (tptp.mem2 @t147 @t146 tptp.g_s76_76) (and (>= @t147 0) (<= @t147 tptp.max_int) (tptp.mem0 @t146 tptp.g_s14_14)))) (forall (@list @t145 @t144 @t143) (=> (and (tptp.mem2 @t145 @t144 tptp.g_s76_76) (tptp.mem2 @t145 @t143 tptp.g_s76_76)) (= @t144 @t143))))) % 3.94/4.14 (assume @p24 (exists (@list @t158) (and (exists (@list @t154) (and (forall (@list @t162 @t163) (= (tptp.mem2 @t163 @t162 @t154) (tptp.mem2 @t163 @t162 tptp.g_s76_76))) (forall (@list @t161 @t160 @t159) (=> (and (tptp.mem2 @t161 @t160 @t154) (tptp.mem2 @t161 @t159 @t154)) (= @t160 @t159))) (forall (@list @t157) (= (and (>= @t157 1) (<= @t157 @t158)) (exists (@list @t156) (tptp.mem2 @t157 @t156 @t154)))) (forall (@list @t153) (=> (exists (@list @t155) (tptp.mem2 @t155 @t153 @t154)) (tptp.mem0 @t153 tptp.g_s74_74))))) (forall (@list @t151) (=> (tptp.mem0 @t151 tptp.g_s74_74) (exists (@list @t152) (tptp.mem2 @t152 @t151 tptp.g_s76_76)))) (forall (@list @t150 @t149 @t148) (=> (and (tptp.mem2 @t149 @t150 tptp.g_s76_76) (tptp.mem2 @t148 @t150 tptp.g_s76_76)) (= @t149 @t148)))))) % 3.94/4.14 (assume @p25 (and (not (forall (@list @t182) (= (tptp.mem0 @t182 tptp.g_s12_12) false))) (forall (@list @t181) (=> (tptp.mem0 @t181 tptp.g_s12_12) true)) (exists (@list @t175 @t166) (and (exists (@list @t171) (and (forall (@list @t179 @t180) (= (tptp.mem2 @t180 @t179 @t171) (tptp.mem2 @t180 @t179 @t166))) (forall (@list @t178 @t177 @t176) (=> (and (tptp.mem2 @t178 @t177 @t171) (tptp.mem2 @t178 @t176 @t171)) (= @t177 @t176))) (forall (@list @t174) (= (and (>= @t174 1) (<= @t174 @t175)) (exists (@list @t173) (tptp.mem2 @t174 @t173 @t171)))) (forall (@list @t170) (=> (exists (@list @t172) (tptp.mem2 @t172 @t170 @t171)) (tptp.mem0 @t170 tptp.g_s12_12))))) (forall (@list @t168) (=> (tptp.mem0 @t168 tptp.g_s12_12) (exists (@list @t169) (tptp.mem2 @t169 @t168 @t166)))) (forall (@list @t167 @t165 @t164) (=> (and (tptp.mem2 @t165 @t167 @t166) (tptp.mem2 @t164 @t167 @t166)) (= @t165 @t164))))))) % 3.94/4.14 (assume @p26 (and (not (forall (@list @t201) (= (tptp.mem0 @t201 tptp.g_s13_13) false))) (forall (@list @t200) (=> (tptp.mem0 @t200 tptp.g_s13_13) true)) (exists (@list @t194 @t185) (and (exists (@list @t190) (and (forall (@list @t198 @t199) (= (tptp.mem2 @t199 @t198 @t190) (tptp.mem2 @t199 @t198 @t185))) (forall (@list @t197 @t196 @t195) (=> (and (tptp.mem2 @t197 @t196 @t190) (tptp.mem2 @t197 @t195 @t190)) (= @t196 @t195))) (forall (@list @t193) (= (and (>= @t193 1) (<= @t193 @t194)) (exists (@list @t192) (tptp.mem2 @t193 @t192 @t190)))) (forall (@list @t189) (=> (exists (@list @t191) (tptp.mem2 @t191 @t189 @t190)) (tptp.mem0 @t189 tptp.g_s13_13))))) (forall (@list @t187) (=> (tptp.mem0 @t187 tptp.g_s13_13) (exists (@list @t188) (tptp.mem2 @t188 @t187 @t185)))) (forall (@list @t186 @t184 @t183) (=> (and (tptp.mem2 @t184 @t186 @t185) (tptp.mem2 @t183 @t186 @t185)) (= @t184 @t183))))))) % 3.94/4.14 (assume @p27 (and (not (forall (@list @t220) (= (tptp.mem0 @t220 tptp.g_s14_14) false))) (forall (@list @t219) (=> (tptp.mem0 @t219 tptp.g_s14_14) true)) (exists (@list @t213 @t204) (and (exists (@list @t209) (and (forall (@list @t217 @t218) (= (tptp.mem2 @t218 @t217 @t209) (tptp.mem2 @t218 @t217 @t204))) (forall (@list @t216 @t215 @t214) (=> (and (tptp.mem2 @t216 @t215 @t209) (tptp.mem2 @t216 @t214 @t209)) (= @t215 @t214))) (forall (@list @t212) (= (and (>= @t212 1) (<= @t212 @t213)) (exists (@list @t211) (tptp.mem2 @t212 @t211 @t209)))) (forall (@list @t208) (=> (exists (@list @t210) (tptp.mem2 @t210 @t208 @t209)) (tptp.mem0 @t208 tptp.g_s14_14))))) (forall (@list @t206) (=> (tptp.mem0 @t206 tptp.g_s14_14) (exists (@list @t207) (tptp.mem2 @t207 @t206 @t204)))) (forall (@list @t205 @t203 @t202) (=> (and (tptp.mem2 @t203 @t205 @t204) (tptp.mem2 @t202 @t205 @t204)) (= @t203 @t202))))))) % 3.94/4.14 (assume @p28 (and (forall (@list @t221) (= (tptp.mem0 @t221 tptp.g_s15_15) (or (= @t221 tptp.g_s16_16) (= @t221 tptp.g_s17_17) (= @t221 tptp.g_s18_18)))) (not (= tptp.g_s16_16 tptp.g_s17_17)) (not (= tptp.g_s17_17 tptp.g_s18_18)))) % 3.94/4.14 (assume @p29 (forall (@list @t222) (=> (tptp.mem0 @t222 tptp.g_s19_19) (tptp.mem0 @t222 tptp.g_s0_0)))) % 3.94/4.14 (assume @p30 (tptp.mem0 tptp.g_s20_20 tptp.g_s0_0)) % 3.94/4.14 (assume @p31 (not (tptp.mem0 tptp.g_s20_20 tptp.g_s19_19))) % 3.94/4.14 (assume @p32 (and (forall (@list @t226 @t227) (=> (tptp.mem2 @t227 @t226 tptp.g_s21_21) (and (>= @t227 0) (<= @t227 tptp.max_int) (tptp.mem0 @t226 tptp.g_s0_0)))) (forall (@list @t225 @t224 @t223) (=> (and (tptp.mem2 @t225 @t224 tptp.g_s21_21) (tptp.mem2 @t225 @t223 tptp.g_s21_21)) (= @t224 @t223))))) % 3.94/4.14 (assume @p33 (and (not (forall (@list @t246) (= (tptp.mem0 @t246 tptp.g_s2_2) false))) (forall (@list @t245) (=> (tptp.mem0 @t245 tptp.g_s2_2) true)) (exists (@list @t239 @t230) (and (exists (@list @t235) (and (forall (@list @t243 @t244) (= (tptp.mem2 @t244 @t243 @t235) (tptp.mem2 @t244 @t243 @t230))) (forall (@list @t242 @t241 @t240) (=> (and (tptp.mem2 @t242 @t241 @t235) (tptp.mem2 @t242 @t240 @t235)) (= @t241 @t240))) (forall (@list @t238) (= (and (>= @t238 1) (<= @t238 @t239)) (exists (@list @t237) (tptp.mem2 @t238 @t237 @t235)))) (forall (@list @t234) (=> (exists (@list @t236) (tptp.mem2 @t236 @t234 @t235)) (tptp.mem0 @t234 tptp.g_s2_2))))) (forall (@list @t232) (=> (tptp.mem0 @t232 tptp.g_s2_2) (exists (@list @t233) (tptp.mem2 @t233 @t232 @t230)))) (forall (@list @t231 @t229 @t228) (=> (and (tptp.mem2 @t229 @t231 @t230) (tptp.mem2 @t228 @t231 @t230)) (= @t229 @t228))))))) % 3.94/4.14 (assume @p34 (exists (@list @t257) (and (exists (@list @t253) (and (forall (@list @t261 @t262) (= (tptp.mem2 @t262 @t261 @t253) (tptp.mem2 @t262 @t261 tptp.g_s21_21))) (forall (@list @t260 @t259 @t258) (=> (and (tptp.mem2 @t260 @t259 @t253) (tptp.mem2 @t260 @t258 @t253)) (= @t259 @t258))) (forall (@list @t256) (= (and (>= @t256 1) (<= @t256 @t257)) (exists (@list @t255) (tptp.mem2 @t256 @t255 @t253)))) (forall (@list @t252) (=> (exists (@list @t254) (tptp.mem2 @t254 @t252 @t253)) (tptp.mem0 @t252 tptp.g_s19_19))))) (forall (@list @t250) (=> (tptp.mem0 @t250 tptp.g_s19_19) (exists (@list @t251) (tptp.mem2 @t251 @t250 tptp.g_s21_21)))) (forall (@list @t249 @t248 @t247) (=> (and (tptp.mem2 @t248 @t249 tptp.g_s21_21) (tptp.mem2 @t247 @t249 tptp.g_s21_21)) (= @t248 @t247)))))) % 3.94/4.14 (assume @p35 (forall (@list @t263) (=> (tptp.mem0 @t263 tptp.g_s22_22) (tptp.mem0 @t263 tptp.g_s1_1)))) % 3.94/4.14 (assume @p36 (tptp.mem0 tptp.g_s23_23 tptp.g_s1_1)) % 3.94/4.14 (assume @p37 (not (tptp.mem0 tptp.g_s23_23 tptp.g_s22_22))) % 3.94/4.14 (assume @p38 (and (forall (@list @t267 @t268) (=> (tptp.mem2 @t268 @t267 tptp.g_s24_24) (and (>= @t268 0) (<= @t268 tptp.max_int) (tptp.mem0 @t267 tptp.g_s1_1)))) (forall (@list @t266 @t265 @t264) (=> (and (tptp.mem2 @t266 @t265 tptp.g_s24_24) (tptp.mem2 @t266 @t264 tptp.g_s24_24)) (= @t265 @t264))))) % 3.94/4.14 (assume @p39 (exists (@list @t279) (and (exists (@list @t275) (and (forall (@list @t283 @t284) (= (tptp.mem2 @t284 @t283 @t275) (tptp.mem2 @t284 @t283 tptp.g_s24_24))) (forall (@list @t282 @t281 @t280) (=> (and (tptp.mem2 @t282 @t281 @t275) (tptp.mem2 @t282 @t280 @t275)) (= @t281 @t280))) (forall (@list @t278) (= (and (>= @t278 1) (<= @t278 @t279)) (exists (@list @t277) (tptp.mem2 @t278 @t277 @t275)))) (forall (@list @t274) (=> (exists (@list @t276) (tptp.mem2 @t276 @t274 @t275)) (tptp.mem0 @t274 tptp.g_s22_22))))) (forall (@list @t272) (=> (tptp.mem0 @t272 tptp.g_s22_22) (exists (@list @t273) (tptp.mem2 @t273 @t272 tptp.g_s24_24)))) (forall (@list @t271 @t270 @t269) (=> (and (tptp.mem2 @t270 @t271 tptp.g_s24_24) (tptp.mem2 @t269 @t271 tptp.g_s24_24)) (= @t270 @t269)))))) % 3.94/4.14 (assume @p40 (forall (@list @t285) (=> (tptp.mem0 @t285 tptp.g_s25_25) (tptp.mem0 @t285 tptp.g_s2_2)))) % 3.94/4.14 (assume @p41 (tptp.mem0 tptp.g_s26_26 tptp.g_s2_2)) % 3.94/4.14 (assume @p42 (not (tptp.mem0 tptp.g_s26_26 tptp.g_s25_25))) % 3.94/4.14 (assume @p43 (and (forall (@list @t289 @t290) (=> (tptp.mem2 @t290 @t289 tptp.g_s27_27) (and (>= @t290 0) (<= @t290 tptp.max_int) (tptp.mem0 @t289 tptp.g_s2_2)))) (forall (@list @t288 @t287 @t286) (=> (and (tptp.mem2 @t288 @t287 tptp.g_s27_27) (tptp.mem2 @t288 @t286 tptp.g_s27_27)) (= @t287 @t286))))) % 3.94/4.14 (assume @p44 (and (not (forall (@list @t309) (= (tptp.mem0 @t309 tptp.g_s3_3) false))) (forall (@list @t308) (=> (tptp.mem0 @t308 tptp.g_s3_3) true)) (exists (@list @t302 @t293) (and (exists (@list @t298) (and (forall (@list @t306 @t307) (= (tptp.mem2 @t307 @t306 @t298) (tptp.mem2 @t307 @t306 @t293))) (forall (@list @t305 @t304 @t303) (=> (and (tptp.mem2 @t305 @t304 @t298) (tptp.mem2 @t305 @t303 @t298)) (= @t304 @t303))) (forall (@list @t301) (= (and (>= @t301 1) (<= @t301 @t302)) (exists (@list @t300) (tptp.mem2 @t301 @t300 @t298)))) (forall (@list @t297) (=> (exists (@list @t299) (tptp.mem2 @t299 @t297 @t298)) (tptp.mem0 @t297 tptp.g_s3_3))))) (forall (@list @t295) (=> (tptp.mem0 @t295 tptp.g_s3_3) (exists (@list @t296) (tptp.mem2 @t296 @t295 @t293)))) (forall (@list @t294 @t292 @t291) (=> (and (tptp.mem2 @t292 @t294 @t293) (tptp.mem2 @t291 @t294 @t293)) (= @t292 @t291))))))) % 3.94/4.14 (assume @p45 (exists (@list @t320) (and (exists (@list @t316) (and (forall (@list @t324 @t325) (= (tptp.mem2 @t325 @t324 @t316) (tptp.mem2 @t325 @t324 tptp.g_s27_27))) (forall (@list @t323 @t322 @t321) (=> (and (tptp.mem2 @t323 @t322 @t316) (tptp.mem2 @t323 @t321 @t316)) (= @t322 @t321))) (forall (@list @t319) (= (and (>= @t319 1) (<= @t319 @t320)) (exists (@list @t318) (tptp.mem2 @t319 @t318 @t316)))) (forall (@list @t315) (=> (exists (@list @t317) (tptp.mem2 @t317 @t315 @t316)) (tptp.mem0 @t315 tptp.g_s25_25))))) (forall (@list @t313) (=> (tptp.mem0 @t313 tptp.g_s25_25) (exists (@list @t314) (tptp.mem2 @t314 @t313 tptp.g_s27_27)))) (forall (@list @t312 @t311 @t310) (=> (and (tptp.mem2 @t311 @t312 tptp.g_s27_27) (tptp.mem2 @t310 @t312 tptp.g_s27_27)) (= @t311 @t310)))))) % 3.94/4.14 (assume @p46 (forall (@list @t326) (=> (tptp.mem0 @t326 tptp.g_s28_28) (tptp.mem0 @t326 tptp.g_s3_3)))) % 3.94/4.14 (assume @p47 (tptp.mem0 tptp.g_s29_29 tptp.g_s3_3)) % 3.94/4.14 (assume @p48 (not (tptp.mem0 tptp.g_s29_29 tptp.g_s28_28))) % 3.94/4.14 (assume @p49 (and (forall (@list @t330 @t331) (=> (tptp.mem2 @t331 @t330 tptp.g_s30_30) (and (>= @t331 0) (<= @t331 tptp.max_int) (tptp.mem0 @t330 tptp.g_s3_3)))) (forall (@list @t329 @t328 @t327) (=> (and (tptp.mem2 @t329 @t328 tptp.g_s30_30) (tptp.mem2 @t329 @t327 tptp.g_s30_30)) (= @t328 @t327))))) % 3.94/4.14 (assume @p50 (exists (@list @t342) (and (exists (@list @t338) (and (forall (@list @t346 @t347) (= (tptp.mem2 @t347 @t346 @t338) (tptp.mem2 @t347 @t346 tptp.g_s30_30))) (forall (@list @t345 @t344 @t343) (=> (and (tptp.mem2 @t345 @t344 @t338) (tptp.mem2 @t345 @t343 @t338)) (= @t344 @t343))) (forall (@list @t341) (= (and (>= @t341 1) (<= @t341 @t342)) (exists (@list @t340) (tptp.mem2 @t341 @t340 @t338)))) (forall (@list @t337) (=> (exists (@list @t339) (tptp.mem2 @t339 @t337 @t338)) (tptp.mem0 @t337 tptp.g_s28_28))))) (forall (@list @t335) (=> (tptp.mem0 @t335 tptp.g_s28_28) (exists (@list @t336) (tptp.mem2 @t336 @t335 tptp.g_s30_30)))) (forall (@list @t334 @t333 @t332) (=> (and (tptp.mem2 @t333 @t334 tptp.g_s30_30) (tptp.mem2 @t332 @t334 tptp.g_s30_30)) (= @t333 @t332)))))) % 3.94/4.14 (assume @p51 (forall (@list @t348) (=> (tptp.mem0 @t348 tptp.g_s31_31) (tptp.mem0 @t348 tptp.g_s4_4)))) % 3.94/4.14 (assume @p52 (tptp.mem0 tptp.g_s32_32 tptp.g_s4_4)) % 3.94/4.14 (assume @p53 (not (tptp.mem0 tptp.g_s32_32 tptp.g_s31_31))) % 3.94/4.14 (assume @p54 (and (forall (@list @t352 @t353) (=> (tptp.mem2 @t353 @t352 tptp.g_s33_33) (and (>= @t353 0) (<= @t353 tptp.max_int) (tptp.mem0 @t352 tptp.g_s4_4)))) (forall (@list @t351 @t350 @t349) (=> (and (tptp.mem2 @t351 @t350 tptp.g_s33_33) (tptp.mem2 @t351 @t349 tptp.g_s33_33)) (= @t350 @t349))))) % 3.94/4.14 (assume @p55 (and (not (forall (@list @t372) (= (tptp.mem0 @t372 tptp.g_s4_4) false))) (forall (@list @t371) (=> (tptp.mem0 @t371 tptp.g_s4_4) true)) (exists (@list @t365 @t356) (and (exists (@list @t361) (and (forall (@list @t369 @t370) (= (tptp.mem2 @t370 @t369 @t361) (tptp.mem2 @t370 @t369 @t356))) (forall (@list @t368 @t367 @t366) (=> (and (tptp.mem2 @t368 @t367 @t361) (tptp.mem2 @t368 @t366 @t361)) (= @t367 @t366))) (forall (@list @t364) (= (and (>= @t364 1) (<= @t364 @t365)) (exists (@list @t363) (tptp.mem2 @t364 @t363 @t361)))) (forall (@list @t360) (=> (exists (@list @t362) (tptp.mem2 @t362 @t360 @t361)) (tptp.mem0 @t360 tptp.g_s4_4))))) (forall (@list @t358) (=> (tptp.mem0 @t358 tptp.g_s4_4) (exists (@list @t359) (tptp.mem2 @t359 @t358 @t356)))) (forall (@list @t357 @t355 @t354) (=> (and (tptp.mem2 @t355 @t357 @t356) (tptp.mem2 @t354 @t357 @t356)) (= @t355 @t354))))))) % 3.94/4.14 (assume @p56 (exists (@list @t383) (and (exists (@list @t379) (and (forall (@list @t387 @t388) (= (tptp.mem2 @t388 @t387 @t379) (tptp.mem2 @t388 @t387 tptp.g_s33_33))) (forall (@list @t386 @t385 @t384) (=> (and (tptp.mem2 @t386 @t385 @t379) (tptp.mem2 @t386 @t384 @t379)) (= @t385 @t384))) (forall (@list @t382) (= (and (>= @t382 1) (<= @t382 @t383)) (exists (@list @t381) (tptp.mem2 @t382 @t381 @t379)))) (forall (@list @t378) (=> (exists (@list @t380) (tptp.mem2 @t380 @t378 @t379)) (tptp.mem0 @t378 tptp.g_s31_31))))) (forall (@list @t376) (=> (tptp.mem0 @t376 tptp.g_s31_31) (exists (@list @t377) (tptp.mem2 @t377 @t376 tptp.g_s33_33)))) (forall (@list @t375 @t374 @t373) (=> (and (tptp.mem2 @t374 @t375 tptp.g_s33_33) (tptp.mem2 @t373 @t375 tptp.g_s33_33)) (= @t374 @t373)))))) % 3.94/4.14 (assume @p57 (forall (@list @t389) (=> (tptp.mem0 @t389 tptp.g_s34_34) (tptp.mem0 @t389 tptp.g_s5_5)))) % 3.94/4.14 (assume @p58 (tptp.mem0 tptp.g_s35_35 tptp.g_s5_5)) % 3.94/4.14 (assume @p59 (not (tptp.mem0 tptp.g_s35_35 tptp.g_s34_34))) % 3.94/4.14 (assume @p60 (and (forall (@list @t393 @t394) (=> (tptp.mem2 @t394 @t393 tptp.g_s36_36) (and (>= @t394 0) (<= @t394 tptp.max_int) (tptp.mem0 @t393 tptp.g_s5_5)))) (forall (@list @t392 @t391 @t390) (=> (and (tptp.mem2 @t392 @t391 tptp.g_s36_36) (tptp.mem2 @t392 @t390 tptp.g_s36_36)) (= @t391 @t390))))) % 3.94/4.14 (assume @p61 (exists (@list @t405) (and (exists (@list @t401) (and (forall (@list @t409 @t410) (= (tptp.mem2 @t410 @t409 @t401) (tptp.mem2 @t410 @t409 tptp.g_s36_36))) (forall (@list @t408 @t407 @t406) (=> (and (tptp.mem2 @t408 @t407 @t401) (tptp.mem2 @t408 @t406 @t401)) (= @t407 @t406))) (forall (@list @t404) (= (and (>= @t404 1) (<= @t404 @t405)) (exists (@list @t403) (tptp.mem2 @t404 @t403 @t401)))) (forall (@list @t400) (=> (exists (@list @t402) (tptp.mem2 @t402 @t400 @t401)) (tptp.mem0 @t400 tptp.g_s34_34))))) (forall (@list @t398) (=> (tptp.mem0 @t398 tptp.g_s34_34) (exists (@list @t399) (tptp.mem2 @t399 @t398 tptp.g_s36_36)))) (forall (@list @t397 @t396 @t395) (=> (and (tptp.mem2 @t396 @t397 tptp.g_s36_36) (tptp.mem2 @t395 @t397 tptp.g_s36_36)) (= @t396 @t395)))))) % 3.94/4.14 (assume @p62 (forall (@list @t411) (=> (tptp.mem0 @t411 tptp.g_s37_37) (tptp.mem0 @t411 tptp.g_s6_6)))) % 3.94/4.14 (assume @p63 (tptp.mem0 tptp.g_s38_38 tptp.g_s6_6)) % 3.94/4.14 (assume @p64 (not (tptp.mem0 tptp.g_s38_38 tptp.g_s37_37))) % 3.94/4.14 (assume @p65 (and (forall (@list @t415 @t416) (=> (tptp.mem2 @t416 @t415 tptp.g_s39_39) (and (>= @t416 0) (<= @t416 tptp.max_int) (tptp.mem0 @t415 tptp.g_s6_6)))) (forall (@list @t414 @t413 @t412) (=> (and (tptp.mem2 @t414 @t413 tptp.g_s39_39) (tptp.mem2 @t414 @t412 tptp.g_s39_39)) (= @t413 @t412))))) % 3.94/4.14 (assume @p66 (and (not (forall (@list @t435) (= (tptp.mem0 @t435 tptp.g_s5_5) false))) (forall (@list @t434) (=> (tptp.mem0 @t434 tptp.g_s5_5) true)) (exists (@list @t428 @t419) (and (exists (@list @t424) (and (forall (@list @t432 @t433) (= (tptp.mem2 @t433 @t432 @t424) (tptp.mem2 @t433 @t432 @t419))) (forall (@list @t431 @t430 @t429) (=> (and (tptp.mem2 @t431 @t430 @t424) (tptp.mem2 @t431 @t429 @t424)) (= @t430 @t429))) (forall (@list @t427) (= (and (>= @t427 1) (<= @t427 @t428)) (exists (@list @t426) (tptp.mem2 @t427 @t426 @t424)))) (forall (@list @t423) (=> (exists (@list @t425) (tptp.mem2 @t425 @t423 @t424)) (tptp.mem0 @t423 tptp.g_s5_5))))) (forall (@list @t421) (=> (tptp.mem0 @t421 tptp.g_s5_5) (exists (@list @t422) (tptp.mem2 @t422 @t421 @t419)))) (forall (@list @t420 @t418 @t417) (=> (and (tptp.mem2 @t418 @t420 @t419) (tptp.mem2 @t417 @t420 @t419)) (= @t418 @t417))))))) % 3.94/4.14 (assume @p67 (exists (@list @t446) (and (exists (@list @t442) (and (forall (@list @t450 @t451) (= (tptp.mem2 @t451 @t450 @t442) (tptp.mem2 @t451 @t450 tptp.g_s39_39))) (forall (@list @t449 @t448 @t447) (=> (and (tptp.mem2 @t449 @t448 @t442) (tptp.mem2 @t449 @t447 @t442)) (= @t448 @t447))) (forall (@list @t445) (= (and (>= @t445 1) (<= @t445 @t446)) (exists (@list @t444) (tptp.mem2 @t445 @t444 @t442)))) (forall (@list @t441) (=> (exists (@list @t443) (tptp.mem2 @t443 @t441 @t442)) (tptp.mem0 @t441 tptp.g_s37_37))))) (forall (@list @t439) (=> (tptp.mem0 @t439 tptp.g_s37_37) (exists (@list @t440) (tptp.mem2 @t440 @t439 tptp.g_s39_39)))) (forall (@list @t438 @t437 @t436) (=> (and (tptp.mem2 @t437 @t438 tptp.g_s39_39) (tptp.mem2 @t436 @t438 tptp.g_s39_39)) (= @t437 @t436)))))) % 3.94/4.14 (assume @p68 (forall (@list @t452) (=> (tptp.mem0 @t452 tptp.g_s40_40) (tptp.mem0 @t452 tptp.g_s7_7)))) % 3.94/4.14 (assume @p69 (tptp.mem0 tptp.g_s41_41 tptp.g_s7_7)) % 3.94/4.14 (assume @p70 (not (tptp.mem0 tptp.g_s41_41 tptp.g_s40_40))) % 3.94/4.14 (assume @p71 (and (forall (@list @t456 @t457) (=> (tptp.mem2 @t457 @t456 tptp.g_s42_42) (and (>= @t457 0) (<= @t457 tptp.max_int) (tptp.mem0 @t456 tptp.g_s7_7)))) (forall (@list @t455 @t454 @t453) (=> (and (tptp.mem2 @t455 @t454 tptp.g_s42_42) (tptp.mem2 @t455 @t453 tptp.g_s42_42)) (= @t454 @t453))))) % 3.94/4.14 (assume @p72 (exists (@list @t468) (and (exists (@list @t464) (and (forall (@list @t472 @t473) (= (tptp.mem2 @t473 @t472 @t464) (tptp.mem2 @t473 @t472 tptp.g_s42_42))) (forall (@list @t471 @t470 @t469) (=> (and (tptp.mem2 @t471 @t470 @t464) (tptp.mem2 @t471 @t469 @t464)) (= @t470 @t469))) (forall (@list @t467) (= (and (>= @t467 1) (<= @t467 @t468)) (exists (@list @t466) (tptp.mem2 @t467 @t466 @t464)))) (forall (@list @t463) (=> (exists (@list @t465) (tptp.mem2 @t465 @t463 @t464)) (tptp.mem0 @t463 tptp.g_s40_40))))) (forall (@list @t461) (=> (tptp.mem0 @t461 tptp.g_s40_40) (exists (@list @t462) (tptp.mem2 @t462 @t461 tptp.g_s42_42)))) (forall (@list @t460 @t459 @t458) (=> (and (tptp.mem2 @t459 @t460 tptp.g_s42_42) (tptp.mem2 @t458 @t460 tptp.g_s42_42)) (= @t459 @t458)))))) % 3.94/4.14 (assume @p73 (and (exists (@list @t478) (and (forall (@list @t485 @t486) (= (tptp.mem2 @t486 @t485 @t478) (tptp.mem2 @t486 @t485 tptp.g_s43_43))) (forall (@list @t484 @t483 @t482) (=> (and (tptp.mem2 @t484 @t483 @t478) (tptp.mem2 @t484 @t482 @t478)) (= @t483 @t482))) (forall (@list @t481) (= (tptp.mem0 @t481 tptp.g_s28_28) (exists (@list @t480) (tptp.mem2 @t481 @t480 @t478)))) (forall (@list @t477) (=> (exists (@list @t479) (tptp.mem2 @t479 @t477 @t478)) (tptp.mem0 @t477 tptp.g_s44_44))))) (forall (@list @t476 @t475 @t474) (=> (and (tptp.mem2 @t475 @t476 tptp.g_s43_43) (tptp.mem2 @t474 @t476 tptp.g_s43_43)) (= @t475 @t474))))) % 3.94/4.14 (assume @p74 (and (exists (@list @t491) (and (forall (@list @t498 @t499) (= (tptp.mem2 @t499 @t498 @t491) (tptp.mem2 @t499 @t498 tptp.g_s45_45))) (forall (@list @t497 @t496 @t495) (=> (and (tptp.mem2 @t497 @t496 @t491) (tptp.mem2 @t497 @t495 @t491)) (= @t496 @t495))) (forall (@list @t494) (= (tptp.mem0 @t494 tptp.g_s31_31) (exists (@list @t493) (tptp.mem2 @t494 @t493 @t491)))) (forall (@list @t490) (=> (exists (@list @t492) (tptp.mem2 @t492 @t490 @t491)) (tptp.mem0 @t490 tptp.g_s44_44))))) (forall (@list @t489 @t488 @t487) (=> (and (tptp.mem2 @t488 @t489 tptp.g_s45_45) (tptp.mem2 @t487 @t489 tptp.g_s45_45)) (= @t488 @t487))))) % 3.94/4.14 (assume @p75 (tptp.mem0 tptp.g_s46_47 tptp.g_s47_46)) % 3.94/4.14 (assume @p76 (=> @t500 (tptp.mem0 tptp.g_s46_47 tptp.g_s44_44))) % 3.94/4.14 (assume @p77 (and (not (forall (@list @t519) (= (tptp.mem0 @t519 tptp.g_s6_6) false))) (forall (@list @t518) (=> (tptp.mem0 @t518 tptp.g_s6_6) true)) (exists (@list @t512 @t503) (and (exists (@list @t508) (and (forall (@list @t516 @t517) (= (tptp.mem2 @t517 @t516 @t508) (tptp.mem2 @t517 @t516 @t503))) (forall (@list @t515 @t514 @t513) (=> (and (tptp.mem2 @t515 @t514 @t508) (tptp.mem2 @t515 @t513 @t508)) (= @t514 @t513))) (forall (@list @t511) (= (and (>= @t511 1) (<= @t511 @t512)) (exists (@list @t510) (tptp.mem2 @t511 @t510 @t508)))) (forall (@list @t507) (=> (exists (@list @t509) (tptp.mem2 @t509 @t507 @t508)) (tptp.mem0 @t507 tptp.g_s6_6))))) (forall (@list @t505) (=> (tptp.mem0 @t505 tptp.g_s6_6) (exists (@list @t506) (tptp.mem2 @t506 @t505 @t503)))) (forall (@list @t504 @t502 @t501) (=> (and (tptp.mem2 @t502 @t504 @t503) (tptp.mem2 @t501 @t504 @t503)) (= @t502 @t501))))))) % 3.94/4.14 (assume @p78 (and (exists (@list @t524) (and (forall (@list @t531 @t532) (= (tptp.mem2 @t532 @t531 @t524) (tptp.mem2 @t532 @t531 tptp.g_s49_49))) (forall (@list @t530 @t529 @t528) (=> (and (tptp.mem2 @t530 @t529 @t524) (tptp.mem2 @t530 @t528 @t524)) (= @t529 @t528))) (forall (@list @t527) (= (tptp.mem0 @t527 tptp.g_s37_37) (exists (@list @t526) (tptp.mem2 @t527 @t526 @t524)))) (forall (@list @t523) (=> (exists (@list @t525) (tptp.mem2 @t525 @t523 @t524)) (tptp.mem0 @t523 tptp.g_s44_44))))) (forall (@list @t522 @t521 @t520) (=> (and (tptp.mem2 @t521 @t522 tptp.g_s49_49) (tptp.mem2 @t520 @t522 tptp.g_s49_49)) (= @t521 @t520))))) % 3.94/4.14 (assume @p79 (forall (@list @t533) (= (and (exists (@list @t535) (tptp.mem2 @t535 @t533 tptp.g_s43_43)) (exists (@list @t534) (tptp.mem2 @t534 @t533 tptp.g_s45_45))) false))) % 3.94/4.14 (assume @p80 (forall (@list @t536) (= (and (exists (@list @t538) (tptp.mem2 @t538 @t536 tptp.g_s43_43)) (exists (@list @t537) (tptp.mem2 @t537 @t536 tptp.g_s49_49))) false))) % 3.94/4.14 (assume @p81 (forall (@list @t539) (= (and (exists (@list @t541) (tptp.mem2 @t541 @t539 tptp.g_s49_49)) (exists (@list @t540) (tptp.mem2 @t540 @t539 tptp.g_s45_45))) false))) % 3.94/4.14 (assume @p82 (=> @t500 (not (exists (@list @t542) (tptp.mem2 @t542 tptp.g_s46_47 tptp.g_s43_43))))) % 3.94/4.14 (assume @p83 (=> @t500 (not (exists (@list @t543) (tptp.mem2 @t543 tptp.g_s46_47 tptp.g_s45_45))))) % 3.94/4.14 (assume @p84 (=> @t500 (not (exists (@list @t544) (tptp.mem2 @t544 tptp.g_s46_47 tptp.g_s49_49))))) % 3.94/4.14 (assume @p85 (forall (@list @t545) (=> (tptp.mem0 @t545 tptp.g_s50_50) (tptp.mem0 @t545 tptp.g_s8_8)))) % 3.94/4.14 (assume @p86 (tptp.mem0 tptp.g_s51_51 tptp.g_s8_8)) % 3.94/4.14 (assume @p87 (not (tptp.mem0 tptp.g_s51_51 tptp.g_s50_50))) % 3.94/4.14 (assume @p88 (and (not (forall (@list @t564) (= (tptp.mem0 @t564 tptp.g_s7_7) false))) (forall (@list @t563) (=> (tptp.mem0 @t563 tptp.g_s7_7) true)) (exists (@list @t557 @t548) (and (exists (@list @t553) (and (forall (@list @t561 @t562) (= (tptp.mem2 @t562 @t561 @t553) (tptp.mem2 @t562 @t561 @t548))) (forall (@list @t560 @t559 @t558) (=> (and (tptp.mem2 @t560 @t559 @t553) (tptp.mem2 @t560 @t558 @t553)) (= @t559 @t558))) (forall (@list @t556) (= (and (>= @t556 1) (<= @t556 @t557)) (exists (@list @t555) (tptp.mem2 @t556 @t555 @t553)))) (forall (@list @t552) (=> (exists (@list @t554) (tptp.mem2 @t554 @t552 @t553)) (tptp.mem0 @t552 tptp.g_s7_7))))) (forall (@list @t550) (=> (tptp.mem0 @t550 tptp.g_s7_7) (exists (@list @t551) (tptp.mem2 @t551 @t550 @t548)))) (forall (@list @t549 @t547 @t546) (=> (and (tptp.mem2 @t547 @t549 @t548) (tptp.mem2 @t546 @t549 @t548)) (= @t547 @t546))))))) % 3.94/4.14 (assume @p89 (and (forall (@list @t568 @t569) (=> (tptp.mem2 @t569 @t568 tptp.g_s52_52) (and (>= @t569 0) (<= @t569 tptp.max_int) (tptp.mem0 @t568 tptp.g_s8_8)))) (forall (@list @t567 @t566 @t565) (=> (and (tptp.mem2 @t567 @t566 tptp.g_s52_52) (tptp.mem2 @t567 @t565 tptp.g_s52_52)) (= @t566 @t565))))) % 3.94/4.14 (assume @p90 (exists (@list @t580) (and (exists (@list @t576) (and (forall (@list @t584 @t585) (= (tptp.mem2 @t585 @t584 @t576) (tptp.mem2 @t585 @t584 tptp.g_s52_52))) (forall (@list @t583 @t582 @t581) (=> (and (tptp.mem2 @t583 @t582 @t576) (tptp.mem2 @t583 @t581 @t576)) (= @t582 @t581))) (forall (@list @t579) (= (and (>= @t579 1) (<= @t579 @t580)) (exists (@list @t578) (tptp.mem2 @t579 @t578 @t576)))) (forall (@list @t575) (=> (exists (@list @t577) (tptp.mem2 @t577 @t575 @t576)) (tptp.mem0 @t575 tptp.g_s50_50))))) (forall (@list @t573) (=> (tptp.mem0 @t573 tptp.g_s50_50) (exists (@list @t574) (tptp.mem2 @t574 @t573 tptp.g_s52_52)))) (forall (@list @t572 @t571 @t570) (=> (and (tptp.mem2 @t571 @t572 tptp.g_s52_52) (tptp.mem2 @t570 @t572 tptp.g_s52_52)) (= @t571 @t570)))))) % 3.94/4.14 (assume @p91 (forall (@list @t586) (=> (tptp.mem0 @t586 tptp.g_s53_53) (tptp.mem0 @t586 tptp.g_s8_8)))) % 3.94/4.14 (assume @p92 (forall (@list @t587) (=> (tptp.mem0 @t587 tptp.g_s54_54) (tptp.mem0 @t587 tptp.g_s53_53)))) % 3.94/4.14 (assume @p93 (forall (@list @t588) (=> (tptp.mem0 @t588 tptp.g_s54_54) (tptp.mem0 @t588 tptp.g_s8_8)))) % 3.94/4.14 (assume @p94 (forall (@list @t589) (=> (tptp.mem0 @t589 tptp.g_s54_54) (tptp.mem0 @t589 tptp.g_s50_50)))) % 3.94/4.14 (assume @p95 (tptp.mem0 tptp.g_s51_51 tptp.g_s53_53)) % 3.94/4.14 (assume @p96 (not (tptp.mem0 tptp.g_s51_51 tptp.g_s54_54))) % 3.94/4.14 (assume @p97 (and (forall (@list @t593 @t594) (=> (tptp.mem2 @t594 @t593 tptp.g_s55_55) (and (>= @t594 0) (<= @t594 tptp.max_int) (tptp.mem0 @t593 tptp.g_s53_53)))) (forall (@list @t592 @t591 @t590) (=> (and (tptp.mem2 @t592 @t591 tptp.g_s55_55) (tptp.mem2 @t592 @t590 tptp.g_s55_55)) (= @t591 @t590))))) % 3.94/4.14 (assume @p98 (exists (@list @t605) (and (exists (@list @t601) (and (forall (@list @t609 @t610) (= (tptp.mem2 @t610 @t609 @t601) (tptp.mem2 @t610 @t609 tptp.g_s55_55))) (forall (@list @t608 @t607 @t606) (=> (and (tptp.mem2 @t608 @t607 @t601) (tptp.mem2 @t608 @t606 @t601)) (= @t607 @t606))) (forall (@list @t604) (= (and (>= @t604 1) (<= @t604 @t605)) (exists (@list @t603) (tptp.mem2 @t604 @t603 @t601)))) (forall (@list @t600) (=> (exists (@list @t602) (tptp.mem2 @t602 @t600 @t601)) (tptp.mem0 @t600 tptp.g_s54_54))))) (forall (@list @t598) (=> (tptp.mem0 @t598 tptp.g_s54_54) (exists (@list @t599) (tptp.mem2 @t599 @t598 tptp.g_s55_55)))) (forall (@list @t597 @t596 @t595) (=> (and (tptp.mem2 @t596 @t597 tptp.g_s55_55) (tptp.mem2 @t595 @t597 tptp.g_s55_55)) (= @t596 @t595)))))) % 3.94/4.14 (assume @p99 (and (not (forall (@list @t629) (= (tptp.mem0 @t629 tptp.g_s8_8) false))) (forall (@list @t628) (=> (tptp.mem0 @t628 tptp.g_s8_8) true)) (exists (@list @t622 @t613) (and (exists (@list @t618) (and (forall (@list @t626 @t627) (= (tptp.mem2 @t627 @t626 @t618) (tptp.mem2 @t627 @t626 @t613))) (forall (@list @t625 @t624 @t623) (=> (and (tptp.mem2 @t625 @t624 @t618) (tptp.mem2 @t625 @t623 @t618)) (= @t624 @t623))) (forall (@list @t621) (= (and (>= @t621 1) (<= @t621 @t622)) (exists (@list @t620) (tptp.mem2 @t621 @t620 @t618)))) (forall (@list @t617) (=> (exists (@list @t619) (tptp.mem2 @t619 @t617 @t618)) (tptp.mem0 @t617 tptp.g_s8_8))))) (forall (@list @t615) (=> (tptp.mem0 @t615 tptp.g_s8_8) (exists (@list @t616) (tptp.mem2 @t616 @t615 @t613)))) (forall (@list @t614 @t612 @t611) (=> (and (tptp.mem2 @t612 @t614 @t613) (tptp.mem2 @t611 @t614 @t613)) (= @t612 @t611))))))) % 3.94/4.14 (assume @p100 (forall (@list @t630) (=> (tptp.mem0 @t630 tptp.g_s56_56) (tptp.mem0 @t630 tptp.g_s9_9)))) % 3.94/4.14 (assume @p101 (tptp.mem0 tptp.g_s57_57 tptp.g_s9_9)) % 3.94/4.14 (assume @p102 (not (tptp.mem0 tptp.g_s57_57 tptp.g_s56_56))) % 3.94/4.14 (assume @p103 (and (forall (@list @t634 @t635) (=> (tptp.mem2 @t635 @t634 tptp.g_s58_58) (and (>= @t635 0) (<= @t635 tptp.max_int) (tptp.mem0 @t634 tptp.g_s9_9)))) (forall (@list @t633 @t632 @t631) (=> (and (tptp.mem2 @t633 @t632 tptp.g_s58_58) (tptp.mem2 @t633 @t631 tptp.g_s58_58)) (= @t632 @t631))))) % 3.94/4.14 (assume @p104 (exists (@list @t646) (and (exists (@list @t642) (and (forall (@list @t650 @t651) (= (tptp.mem2 @t651 @t650 @t642) (tptp.mem2 @t651 @t650 tptp.g_s58_58))) (forall (@list @t649 @t648 @t647) (=> (and (tptp.mem2 @t649 @t648 @t642) (tptp.mem2 @t649 @t647 @t642)) (= @t648 @t647))) (forall (@list @t645) (= (and (>= @t645 1) (<= @t645 @t646)) (exists (@list @t644) (tptp.mem2 @t645 @t644 @t642)))) (forall (@list @t641) (=> (exists (@list @t643) (tptp.mem2 @t643 @t641 @t642)) (tptp.mem0 @t641 tptp.g_s56_56))))) (forall (@list @t639) (=> (tptp.mem0 @t639 tptp.g_s56_56) (exists (@list @t640) (tptp.mem2 @t640 @t639 tptp.g_s58_58)))) (forall (@list @t638 @t637 @t636) (=> (and (tptp.mem2 @t637 @t638 tptp.g_s58_58) (tptp.mem2 @t636 @t638 tptp.g_s58_58)) (= @t637 @t636)))))) % 3.94/4.14 (assume @p105 (forall (@list @t652) (=> (tptp.mem0 @t652 tptp.g_s59_59) (tptp.mem0 @t652 tptp.g_s10_10)))) % 3.94/4.14 (assume @p106 (tptp.mem0 tptp.g_s60_60 tptp.g_s10_10)) % 3.94/4.14 (assume @p107 (not (tptp.mem0 tptp.g_s60_60 tptp.g_s59_59))) % 3.94/4.14 (assume @p108 (and (forall (@list @t656 @t657) (=> (tptp.mem2 @t657 @t656 tptp.g_s61_61) (and (>= @t657 0) (<= @t657 tptp.max_int) (tptp.mem0 @t656 tptp.g_s10_10)))) (forall (@list @t655 @t654 @t653) (=> (and (tptp.mem2 @t655 @t654 tptp.g_s61_61) (tptp.mem2 @t655 @t653 tptp.g_s61_61)) (= @t654 @t653))))) % 3.94/4.14 (assume @p109 (exists (@list @t668) (and (exists (@list @t664) (and (forall (@list @t672 @t673) (= (tptp.mem2 @t673 @t672 @t664) (tptp.mem2 @t673 @t672 tptp.g_s61_61))) (forall (@list @t671 @t670 @t669) (=> (and (tptp.mem2 @t671 @t670 @t664) (tptp.mem2 @t671 @t669 @t664)) (= @t670 @t669))) (forall (@list @t667) (= (and (>= @t667 1) (<= @t667 @t668)) (exists (@list @t666) (tptp.mem2 @t667 @t666 @t664)))) (forall (@list @t663) (=> (exists (@list @t665) (tptp.mem2 @t665 @t663 @t664)) (tptp.mem0 @t663 tptp.g_s59_59))))) (forall (@list @t661) (=> (tptp.mem0 @t661 tptp.g_s59_59) (exists (@list @t662) (tptp.mem2 @t662 @t661 tptp.g_s61_61)))) (forall (@list @t660 @t659 @t658) (=> (and (tptp.mem2 @t659 @t660 tptp.g_s61_61) (tptp.mem2 @t658 @t660 tptp.g_s61_61)) (= @t659 @t658)))))) % 3.94/4.14 (assume @p110 (and (not (forall (@list @t692) (= (tptp.mem0 @t692 tptp.g_s9_9) false))) (forall (@list @t691) (=> (tptp.mem0 @t691 tptp.g_s9_9) true)) (exists (@list @t685 @t676) (and (exists (@list @t681) (and (forall (@list @t689 @t690) (= (tptp.mem2 @t690 @t689 @t681) (tptp.mem2 @t690 @t689 @t676))) (forall (@list @t688 @t687 @t686) (=> (and (tptp.mem2 @t688 @t687 @t681) (tptp.mem2 @t688 @t686 @t681)) (= @t687 @t686))) (forall (@list @t684) (= (and (>= @t684 1) (<= @t684 @t685)) (exists (@list @t683) (tptp.mem2 @t684 @t683 @t681)))) (forall (@list @t680) (=> (exists (@list @t682) (tptp.mem2 @t682 @t680 @t681)) (tptp.mem0 @t680 tptp.g_s9_9))))) (forall (@list @t678) (=> (tptp.mem0 @t678 tptp.g_s9_9) (exists (@list @t679) (tptp.mem2 @t679 @t678 @t676)))) (forall (@list @t677 @t675 @t674) (=> (and (tptp.mem2 @t675 @t677 @t676) (tptp.mem2 @t674 @t677 @t676)) (= @t675 @t674))))))) % 3.94/4.14 (assume @p111 (forall (@list @t693) (=> (tptp.mem0 @t693 tptp.g_s62_62) (tptp.mem0 @t693 tptp.g_s11_11)))) % 3.94/4.14 (assume @p112 (tptp.mem0 tptp.g_s63_63 tptp.g_s11_11)) % 3.94/4.14 (assume @p113 (not (tptp.mem0 tptp.g_s63_63 tptp.g_s62_62))) % 3.94/4.14 (assume @p114 (and (forall (@list @t697 @t698) (=> (tptp.mem2 @t698 @t697 tptp.g_s64_64) (and (>= @t698 0) (<= @t698 tptp.max_int) (tptp.mem0 @t697 tptp.g_s11_11)))) (forall (@list @t696 @t695 @t694) (=> (and (tptp.mem2 @t696 @t695 tptp.g_s64_64) (tptp.mem2 @t696 @t694 tptp.g_s64_64)) (= @t695 @t694))))) % 3.94/4.14 (assume @p115 (exists (@list @t709) (and (exists (@list @t705) (and (forall (@list @t713 @t714) (= (tptp.mem2 @t714 @t713 @t705) (tptp.mem2 @t714 @t713 tptp.g_s64_64))) (forall (@list @t712 @t711 @t710) (=> (and (tptp.mem2 @t712 @t711 @t705) (tptp.mem2 @t712 @t710 @t705)) (= @t711 @t710))) (forall (@list @t708) (= (and (>= @t708 1) (<= @t708 @t709)) (exists (@list @t707) (tptp.mem2 @t708 @t707 @t705)))) (forall (@list @t704) (=> (exists (@list @t706) (tptp.mem2 @t706 @t704 @t705)) (tptp.mem0 @t704 tptp.g_s62_62))))) (forall (@list @t702) (=> (tptp.mem0 @t702 tptp.g_s62_62) (exists (@list @t703) (tptp.mem2 @t703 @t702 tptp.g_s64_64)))) (forall (@list @t701 @t700 @t699) (=> (and (tptp.mem2 @t700 @t701 tptp.g_s64_64) (tptp.mem2 @t699 @t701 tptp.g_s64_64)) (= @t700 @t699)))))) % 3.94/4.14 (assume @p116 (forall (@list @t715) (=> (tptp.mem0 @t715 tptp.g_s65_65) (tptp.mem0 @t715 tptp.g_s11_11)))) % 3.94/4.14 (assume @p117 (forall (@list @t716) (=> (tptp.mem0 @t716 tptp.g_s66_66) (tptp.mem0 @t716 tptp.g_s65_65)))) % 3.94/4.14 (assume @p118 (forall (@list @t717) (=> (tptp.mem0 @t717 tptp.g_s66_66) (tptp.mem0 @t717 tptp.g_s11_11)))) % 3.94/4.14 (assume @p119 (forall (@list @t718) (=> (tptp.mem0 @t718 tptp.g_s66_66) (tptp.mem0 @t718 tptp.g_s62_62)))) % 3.94/4.14 (assume @p120 (tptp.mem0 tptp.g_s63_63 tptp.g_s65_65)) % 3.94/4.14 (assume @p121 (forall (@list @t719) (= (exists (@list @t721) (and (tptp.mem2 @t719 @t721 tptp.g_s94_77) @t720 (tptp.mem0 @t721 tptp.g_s37_37))) @t720))) % 3.94/4.14 (assume @p122 (forall (@list @t722) (= (exists (@list @t724) (and (tptp.mem2 @t722 @t724 tptp.g_s97_78) @t723 (tptp.mem0 @t724 tptp.g_s37_37))) @t723))) % 3.94/4.14 (assume @p123 (exists (@list @t726) (and (forall (@list @t733 @t734) (= (tptp.mem2 @t734 @t733 @t726) (tptp.mem2 @t734 @t733 tptp.g_s100_85))) (forall (@list @t732 @t731 @t730) (=> (and (tptp.mem2 @t732 @t731 @t726) (tptp.mem2 @t732 @t730 @t726)) (= @t731 @t730))) (forall (@list @t729) (= (tptp.mem0 @t729 tptp.g_s10_10) (exists (@list @t728) (tptp.mem2 @t729 @t728 @t726)))) (forall (@list @t725) (=> (exists (@list @t727) (tptp.mem2 @t727 @t725 @t726)) (tptp.mem0 @t725 tptp.g_s6_6)))))) % 3.94/4.14 (assume @p124 (exists (@list @t736) (and (forall (@list @t743 @t744) (= (tptp.mem2 @t744 @t743 @t736) (tptp.mem2 @t744 @t743 tptp.g_s101_86))) (forall (@list @t742 @t741 @t740) (=> (and (tptp.mem2 @t742 @t741 @t736) (tptp.mem2 @t742 @t740 @t736)) (= @t741 @t740))) (forall (@list @t739) (= (tptp.mem0 @t739 tptp.g_s10_10) (exists (@list @t738) (tptp.mem2 @t739 @t738 @t736)))) (forall (@list @t735) (=> (exists (@list @t737) (tptp.mem2 @t737 @t735 @t736)) (tptp.mem0 @t735 tptp.g_s6_6)))))) % 3.94/4.14 (assume @p125 (exists (@list @t746) (and (forall (@list @t753 @t754) (= (tptp.mem2 @t754 @t753 @t746) (tptp.mem2 @t754 @t753 tptp.g_s102_87))) (forall (@list @t752 @t751 @t750) (=> (and (tptp.mem2 @t752 @t751 @t746) (tptp.mem2 @t752 @t750 @t746)) (= @t751 @t750))) (forall (@list @t749) (= (tptp.mem0 @t749 tptp.g_s11_11) (exists (@list @t748) (tptp.mem2 @t749 @t748 @t746)))) (forall (@list @t745) (=> (exists (@list @t747) (tptp.mem2 @t747 @t745 @t746)) (tptp.mem0 @t745 tptp.g_s6_6)))))) % 3.94/4.14 (assume @p126 (exists (@list @t756) (and (forall (@list @t763 @t764) (= (tptp.mem2 @t764 @t763 @t756) (tptp.mem2 @t764 @t763 tptp.g_s103_88))) (forall (@list @t762 @t761 @t760) (=> (and (tptp.mem2 @t762 @t761 @t756) (tptp.mem2 @t762 @t760 @t756)) (= @t761 @t760))) (forall (@list @t759) (= (tptp.mem0 @t759 tptp.g_s65_65) (exists (@list @t758) (tptp.mem2 @t759 @t758 @t756)))) (forall (@list @t755) (=> (exists (@list @t757) (tptp.mem2 @t757 @t755 @t756)) (tptp.mem0 @t755 tptp.g_s6_6)))))) % 3.94/4.14 (assume @p127 @t800) % 3.94/4.14 (assume @p128 (exists (@list @t802) (and (forall (@list @t809 @t810) (= (tptp.mem2 @t810 @t809 @t802) (tptp.mem2 @t810 @t809 tptp.g_s105_90))) (forall (@list @t808 @t807 @t806) (=> (and (tptp.mem2 @t808 @t807 @t802) (tptp.mem2 @t808 @t806 @t802)) (= @t807 @t806))) (forall (@list @t805) (= (tptp.mem0 @t805 tptp.g_s11_11) (exists (@list @t804) (tptp.mem2 @t805 @t804 @t802)))) (forall (@list @t801) (=> (exists (@list @t803) (tptp.mem2 @t803 @t801 @t802)) (tptp.mem0 @t801 tptp.g_s6_6)))))) % 3.94/4.14 (assume @p129 (exists (@list @t812) (and (forall (@list @t819 @t820) (= (tptp.mem2 @t820 @t819 @t812) (tptp.mem2 @t820 @t819 tptp.g_s106_91))) (forall (@list @t818 @t817 @t816) (=> (and (tptp.mem2 @t818 @t817 @t812) (tptp.mem2 @t818 @t816 @t812)) (= @t817 @t816))) (forall (@list @t815) (= (tptp.mem0 @t815 tptp.g_s65_65) (exists (@list @t814) (tptp.mem2 @t815 @t814 @t812)))) (forall (@list @t811) (=> (exists (@list @t813) (tptp.mem2 @t813 @t811 @t812)) (tptp.mem0 @t811 tptp.g_s6_6)))))) % 3.94/4.14 (assume @p130 (exists (@list @t822) (and (forall (@list @t829 @t830) (= (tptp.mem2 @t830 @t829 @t822) (tptp.mem2 @t830 @t829 tptp.g_s107_92))) (forall (@list @t828 @t827 @t826) (=> (and (tptp.mem2 @t828 @t827 @t822) (tptp.mem2 @t828 @t826 @t822)) (= @t827 @t826))) (forall (@list @t825) (= (tptp.mem0 @t825 tptp.g_s11_11) (exists (@list @t824) (tptp.mem2 @t825 @t824 @t822)))) (forall (@list @t821) (=> (exists (@list @t823) (tptp.mem2 @t823 @t821 @t822)) (tptp.mem0 @t821 tptp.g_s6_6)))))) % 3.94/4.14 (assume @p131 (exists (@list @t832) (and (forall (@list @t839 @t840) (= (tptp.mem2 @t840 @t839 @t832) (tptp.mem2 @t840 @t839 tptp.g_s108_79))) (forall (@list @t838 @t837 @t836) (=> (and (tptp.mem2 @t838 @t837 @t832) (tptp.mem2 @t838 @t836 @t832)) (= @t837 @t836))) (forall (@list @t835) (= (tptp.mem0 @t835 tptp.g_s13_13) (exists (@list @t834) (tptp.mem2 @t835 @t834 @t832)))) (forall (@list @t831) (=> (exists (@list @t833) (tptp.mem2 @t833 @t831 @t832)) (tptp.mem0 @t831 tptp.g_s6_6)))))) % 3.94/4.14 (assume @p132 (forall (@list @t841) (= (exists (@list @t843) (and (tptp.mem2 @t841 @t843 tptp.g_s108_79) @t842 (tptp.mem0 @t843 tptp.g_s37_37))) @t842))) % 3.94/4.14 (assume @p133 (exists (@list @t845) (and (forall (@list @t852 @t853) (= (tptp.mem2 @t853 @t852 @t845) (tptp.mem2 @t853 @t852 tptp.g_s93_80))) (forall (@list @t851 @t850 @t849) (=> (and (tptp.mem2 @t851 @t850 @t845) (tptp.mem2 @t851 @t849 @t845)) (= @t850 @t849))) (forall (@list @t848) (= (tptp.mem0 @t848 tptp.g_s0_0) (exists (@list @t847) (tptp.mem2 @t848 @t847 @t845)))) (forall (@list @t844) (=> (exists (@list @t846) (tptp.mem2 @t846 @t844 @t845)) (tptp.mem0 @t844 tptp.g_s6_6)))))) % 3.94/4.14 (assume @p134 (exists (@list @t855) (and (forall (@list @t862 @t863) (= (tptp.mem2 @t863 @t862 @t855) (tptp.mem2 @t863 @t862 tptp.g_s94_77))) (forall (@list @t861 @t860 @t859) (=> (and (tptp.mem2 @t861 @t860 @t855) (tptp.mem2 @t861 @t859 @t855)) (= @t860 @t859))) (forall (@list @t858) (= (tptp.mem0 @t858 tptp.g_s1_1) (exists (@list @t857) (tptp.mem2 @t858 @t857 @t855)))) (forall (@list @t854) (=> (exists (@list @t856) (tptp.mem2 @t856 @t854 @t855)) (tptp.mem0 @t854 tptp.g_s6_6)))))) % 3.94/4.14 (assume @p135 (exists (@list @t865) (and (forall (@list @t872 @t873) (= (tptp.mem2 @t873 @t872 @t865) (tptp.mem2 @t873 @t872 tptp.g_s95_81))) (forall (@list @t871 @t870 @t869) (=> (and (tptp.mem2 @t871 @t870 @t865) (tptp.mem2 @t871 @t869 @t865)) (= @t870 @t869))) (forall (@list @t868) (= (tptp.mem0 @t868 tptp.g_s1_1) (exists (@list @t867) (tptp.mem2 @t868 @t867 @t865)))) (forall (@list @t864) (=> (exists (@list @t866) (tptp.mem2 @t866 @t864 @t865)) (tptp.mem0 @t864 tptp.g_s6_6)))))) % 3.94/4.14 (assume @p136 (exists (@list @t875) (and (forall (@list @t882 @t883) (= (tptp.mem2 @t883 @t882 @t875) (tptp.mem2 @t883 @t882 tptp.g_s96_82))) (forall (@list @t881 @t880 @t879) (=> (and (tptp.mem2 @t881 @t880 @t875) (tptp.mem2 @t881 @t879 @t875)) (= @t880 @t879))) (forall (@list @t878) (= (tptp.mem0 @t878 tptp.g_s9_9) (exists (@list @t877) (tptp.mem2 @t878 @t877 @t875)))) (forall (@list @t874) (=> (exists (@list @t876) (tptp.mem2 @t876 @t874 @t875)) (tptp.mem0 @t874 tptp.g_s6_6)))))) % 3.94/4.14 (assume @p137 (exists (@list @t885) (and (forall (@list @t892 @t893) (= (tptp.mem2 @t893 @t892 @t885) (tptp.mem2 @t893 @t892 tptp.g_s97_78))) (forall (@list @t891 @t890 @t889) (=> (and (tptp.mem2 @t891 @t890 @t885) (tptp.mem2 @t891 @t889 @t885)) (= @t890 @t889))) (forall (@list @t888) (= (tptp.mem0 @t888 tptp.g_s2_2) (exists (@list @t887) (tptp.mem2 @t888 @t887 @t885)))) (forall (@list @t884) (=> (exists (@list @t886) (tptp.mem2 @t886 @t884 @t885)) (tptp.mem0 @t884 tptp.g_s6_6)))))) % 3.94/4.14 (assume @p138 (exists (@list @t895) (and (forall (@list @t902 @t903) (= (tptp.mem2 @t903 @t902 @t895) (tptp.mem2 @t903 @t902 tptp.g_s98_83))) (forall (@list @t901 @t900 @t899) (=> (and (tptp.mem2 @t901 @t900 @t895) (tptp.mem2 @t901 @t899 @t895)) (= @t900 @t899))) (forall (@list @t898) (= (tptp.mem0 @t898 tptp.g_s10_10) (exists (@list @t897) (tptp.mem2 @t898 @t897 @t895)))) (forall (@list @t894) (=> (exists (@list @t896) (tptp.mem2 @t896 @t894 @t895)) (tptp.mem0 @t894 tptp.g_s6_6)))))) % 3.94/4.14 (assume @p139 (exists (@list @t905) (and (forall (@list @t912 @t913) (= (tptp.mem2 @t913 @t912 @t905) (tptp.mem2 @t913 @t912 tptp.g_s99_84))) (forall (@list @t911 @t910 @t909) (=> (and (tptp.mem2 @t911 @t910 @t905) (tptp.mem2 @t911 @t909 @t905)) (= @t910 @t909))) (forall (@list @t908) (= (tptp.mem0 @t908 tptp.g_s10_10) (exists (@list @t907) (tptp.mem2 @t908 @t907 @t905)))) (forall (@list @t904) (=> (exists (@list @t906) (tptp.mem2 @t906 @t904 @t905)) (tptp.mem0 @t904 tptp.g_s6_6)))))) % 3.94/4.14 (assume @p140 @t936) % 3.94/4.14 (assume @p141 true) % 3.94/4.14 (step @p142 :rule aci_norm :args ((= (or @t951 (or @t950 (or @t945 @t942))) @t952))) % 3.94/4.14 (step @p143 :rule bool-and-de-morgan :args (@t944 @t941 true)) % 3.94/4.14 (step @p144 :rule refl :args (@t950)) % 3.94/4.14 (step @p145 :rule nary_cong :premises (@p144 @p143) :args ((or @t950 (not (and @t944 @t941))))) % 3.94/4.14 (step @p146 :rule bool-and-de-morgan :args (@t949 @t944 (and @t941))) % 3.94/4.14 (step @p147 :rule trans :premises (@p146 @p145)) % 3.94/4.14 (step @p148 :rule refl :args (@t951)) % 3.94/4.14 (step @p149 :rule nary_cong :premises (@p148 @p147) :args ((or @t951 (not (and @t949 @t944 @t941))))) % 3.94/4.14 (step @p150 :rule bool-and-de-morgan :args (@t797 @t949 (and @t944 @t941))) % 3.94/4.14 (step @p151 :rule trans :premises (@p150 @p149)) % 3.94/4.14 (step @p152 :rule trans :premises (@p151 @p142)) % 3.94/4.14 (step @p153 :rule cong :premises (@p152) :args (@t954)) % 3.94/4.14 (step @p154 :rule cong :premises (@p153) :args (@t955)) % 3.94/4.14 (step @p155 :rule exists-elim :args ((= (exists @t799 @t953) @t955))) % 3.94/4.14 (step @p156 :rule trans :premises (@p155 @p154)) % 3.94/4.14 (step @p157 :rule quant-merge-prenex :args ((= (forall @t773 @t957) @t941))) % 3.94/4.14 (step @p158 :rule refl :args (@t766)) % 3.94/4.14 (step @p159 :rule alpha_equiv :args (@t958 (@list @t937) (@list @t768))) % 3.94/4.14 (step @p160 :rule nary_cong :premises (@p159 @p158) :args (@t959)) % 3.94/4.14 (step @p161 :rule quant-miniscope-or :args ((= @t957 @t959))) % 3.94/4.14 (step @p162 :rule trans :premises (@p161 @p160)) % 3.94/4.14 (step @p163 :rule symm :premises (@p162)) % 3.94/4.14 (step @p164 :rule cong :premises (@p163) :args ((forall @t773 (or @t960 @t766)))) % 3.94/4.14 (step @p165 :rule trans :premises (@p164 @p157)) % 3.94/4.14 (step @p166 :rule bool-double-not-elim :args (@t960)) % 3.94/4.14 (step @p167 :rule nary_cong :premises (@p166 @p158) :args ((or (not @t961) @t766))) % 3.94/4.14 (step @p168 :rule bool-impl-elim :args (@t961 @t766)) % 3.94/4.14 (step @p169 :rule trans :premises (@p168 @p167)) % 3.94/4.14 (step @p170 :rule cong :premises (@p169) :args ((forall @t773 (=> @t961 @t766)))) % 3.94/4.14 (step @p171 :rule trans :premises (@p170 @p165)) % 3.94/4.14 (step @p172 :rule refl :args (@t766)) % 3.94/4.14 (step @p173 :rule exists-elim :args ((= @t771 @t961))) % 3.94/4.14 (step @p174 :rule cong :premises (@p173 @p172) :args (@t772)) % 3.94/4.14 (step @p175 :rule cong :premises (@p174) :args (@t774)) % 3.94/4.14 (step @p176 :rule trans :premises (@p175 @p171)) % 3.94/4.14 (step @p177 :rule exists-elim :args ((= @t779 @t943))) % 3.94/4.14 (step @p178 :rule refl :args (@t780)) % 3.94/4.14 (step @p179 :rule cong :premises (@p178 @p177) :args (@t781)) % 3.94/4.14 (step @p180 :rule cong :premises (@p179) :args (@t783)) % 3.94/4.14 (step @p181 :rule aci_norm :args ((= (or (or @t947 @t946) @t786) @t948))) % 3.94/4.14 (step @p182 :rule refl :args (@t786)) % 3.94/4.14 (step @p183 :rule bool-and-de-morgan :args (@t789 @t788 true)) % 3.94/4.14 (step @p184 :rule nary_cong :premises (@p183 @p182) :args ((or (not @t790) @t786))) % 3.94/4.14 (step @p185 :rule trans :premises (@p184 @p181)) % 3.94/4.14 (step @p186 :rule bool-impl-elim :args (@t790 @t786)) % 3.94/4.14 (step @p187 :rule trans :premises (@p186 @p185)) % 3.94/4.14 (step @p188 :rule cong :premises (@p187) :args (@t792)) % 3.94/4.14 (step @p189 :rule refl :args (@t797)) % 3.94/4.14 (step @p190 :rule nary_cong :premises (@p189 @p188 @p180 @p176) :args (@t798)) % 3.94/4.14 (step @p191 :rule cong :premises (@p190) :args (@t800)) % 3.94/4.14 (step @p192 :rule trans :premises (@p191 @p156)) % 3.94/4.14 (step @p193 :rule eq_resolve :premises (@p127 @p192)) % 3.94/4.14 (step @p194 :rule refl :args (@t972)) % 3.94/4.14 (step @p195 :rule bool-double-not-elim :args (@t962)) % 3.94/4.14 (step @p196 :rule nary_cong :premises (@p195 @p194) :args ((or (not @t973) @t972))) % 3.94/4.14 (step @p197 :rule refl :args (@t964)) % 3.94/4.14 (step @p198 :rule refl :args (@t965)) % 3.94/4.14 (step @p199 :rule refl :args (@t967)) % 3.94/4.14 (step @p200 :rule eq-symm :args (@t968 @t795)) % 3.94/4.14 (step @p201 :rule cong :premises (@p200) :args (@t974)) % 3.94/4.14 (step @p202 :rule cong :premises (@p201) :args (@t975)) % 3.94/4.14 (step @p203 :rule nary_cong :premises (@p202 @p199 @p198 @p197) :args (@t976)) % 3.94/4.14 (step @p204 :rule cong :premises (@p203) :args (@t977)) % 3.94/4.14 (step @p205 :rule refl :args (@t973)) % 3.94/4.14 (step @p206 :rule cong :premises (@p205 @p204) :args ((=> @t973 @t977))) % 3.94/4.14 (assume-push @p355 @t973) % 3.94/4.14 (step @p208 :rule skolemize :premises (@p193)) % 3.94/4.14 (step-pop @p356 :rule scope :premises (@p208)) % 3.94/4.14 (step @p209 :rule process_scope :premises (@p356) :args (@t977)) % 3.94/4.14 (step @p211 :rule eq_resolve :premises (@p209 @p206)) % 3.94/4.14 (step @p212 :rule implies_elim :premises (@p211)) % 3.94/4.14 (step @p213 :rule eq_resolve :premises (@p212 @p196)) % 3.94/4.14 (step @p214 :rule chain_m_resolution :premises (@p213 @p193) :args (@t972 @t978 (@list @t962))) % 3.94/4.14 (step @p215 :rule bool-double-not-elim :args (@t969)) % 3.94/4.14 (step @p216 :rule refl :args (@t971)) % 3.94/4.14 (step @p217 :rule nary_cong :premises (@p216 @p215) :args ((or @t971 (not @t970)))) % 3.94/4.14 (step @p218 :rule cnf_or_neg :args (@t971 0)) % 3.94/4.14 (step @p219 :rule eq_resolve :premises (@p218 @p217)) % 3.94/4.14 (step @p220 :rule reordering :premises (@p219) :args ((or @t969 @t971))) % 3.94/4.14 (step @p221 :rule chain_m_resolution :premises (@p220 @p214) :args (@t969 @t978 @t979)) % 3.94/4.14 (step @p222 :rule bool-double-not-elim :args (@t966)) % 3.94/4.14 (step @p223 :rule nary_cong :premises (@p216 @p222) :args ((or @t971 (not @t967)))) % 3.94/4.14 (step @p224 :rule cnf_or_neg :args (@t971 1)) % 3.94/4.14 (step @p225 :rule eq_resolve :premises (@p224 @p223)) % 3.94/4.14 (step @p226 :rule reordering :premises (@p225) :args ((or @t966 @t971))) % 3.94/4.14 (step @p227 :rule chain_m_resolution :premises (@p226 @p214) :args (@t966 @t978 @t979)) % 3.94/4.14 (step @p228 :rule arith_poly_norm :args ((= (* 1 (- @t987 @t988)) (* -1 (- @t988 @t987))))) % 3.94/4.14 (step @p229 :rule arith_poly_norm_rel :premises (@p228) :args ((= @t990 @t989))) % 3.94/4.14 (step @p230 :rule refl :args (@t993)) % 3.94/4.14 (step @p231 :rule refl :args (@t995)) % 3.94/4.14 (step @p232 :rule nary_cong :premises (@p231 @p230 @p229) :args (@t996)) % 3.94/4.14 (step @p233 :rule refl :args (@t966)) % 3.94/4.14 (step @p234 :rule cong :premises (@p233 @p232) :args ((=> @t966 @t996))) % 3.94/4.14 (assume-push @p357 @t966) % 3.94/4.14 (step @p236 :rule instantiate :premises (@p227) :args ((@list @t991 @t987 @t988))) % 3.94/4.14 (step-pop @p358 :rule scope :premises (@p236)) % 3.94/4.14 (step @p237 :rule process_scope :premises (@p358) :args (@t996)) % 3.94/4.14 (step @p239 :rule eq_resolve :premises (@p237 @p234)) % 3.94/4.14 (step @p240 :rule implies_elim :premises (@p239)) % 3.94/4.14 (step @p241 :rule chain_m_resolution :premises (@p240 @p227) :args (@t997 @t998 (@list @t966))) % 3.94/4.14 (step @p242 :rule instantiate :premises (@p221) :args ((@list @t987 @t991))) % 3.94/4.14 (step @p243 :rule bool-double-not-elim :args (@t1005)) % 3.94/4.14 (step @p244 :rule refl :args (@t1011)) % 3.94/4.14 (step @p245 :rule nary_cong :premises (@p244 @p243) :args ((or @t1011 (not @t1010)))) % 3.94/4.14 (step @p246 :rule cnf_or_neg :args (@t1011 1)) % 3.94/4.14 (step @p247 :rule eq_resolve :premises (@p246 @p245)) % 3.94/4.14 (step @p248 :rule reordering :premises (@p247) :args ((or @t1005 @t1011))) % 3.94/4.14 (step @p249 :rule bool-double-not-elim :args (@t1007)) % 3.94/4.14 (step @p250 :rule nary_cong :premises (@p244 @p249) :args ((or @t1011 (not @t1009)))) % 3.94/4.14 (step @p251 :rule cnf_or_neg :args (@t1011 2)) % 3.94/4.14 (step @p252 :rule eq_resolve :premises (@p251 @p250)) % 3.94/4.14 (step @p253 :rule reordering :premises (@p252) :args ((or @t1007 @t1011))) % 3.94/4.14 (step @p254 :rule cnf_or_neg :args (@t1011 3)) % 3.94/4.14 (step @p255 :rule cnf_and_neg :args (@t1008)) % 3.94/4.14 (step @p256 :rule reordering :premises (@p255) :args ((or @t1010 @t1009 @t1008))) % 3.94/4.14 (step @p257 :rule chain_m_resolution :premises (@p256 @p254 @p253 @p248) :args (@t1011 @t1012 (@list @t1008 @t1007 @t1005))) % 3.94/4.14 (step @p258 :rule refl :args (@t1013)) % 3.94/4.14 (step @p259 :rule bool-double-not-elim :args (@t1003)) % 3.94/4.14 (step @p260 :rule nary_cong :premises (@p259 @p258) :args ((or (not @t1014) @t1013))) % 3.94/4.14 (assume-push @p359 @t1014) % 3.94/4.14 (step @p262 :rule skolemize :premises (@p359)) % 3.94/4.14 (step-pop @p360 :rule scope :premises (@p262)) % 3.94/4.14 (step @p263 :rule process_scope :premises (@p360) :args (@t1013)) % 3.94/4.14 (step @p265 :rule implies_elim :premises (@p263)) % 3.94/4.14 (step @p266 :rule eq_resolve :premises (@p265 @p260)) % 3.94/4.14 (step @p267 :rule chain_m_resolution :premises (@p266 @p257) :args (@t1003 @t998 (@list @t1011))) % 3.94/4.14 (step @p268 :rule aci_norm :args ((= (or @t1015 @t916) @t985))) % 3.94/4.14 (step @p269 :rule refl :args (@t916)) % 3.94/4.14 (step @p270 :rule aci_norm :args ((= @t1016 @t1015))) % 3.94/4.14 (step @p271 :rule aci_norm :args ((= (or @t984 (or @t983 (or @t982 (or @t981 (or @t983 @t980))))) @t1016))) % 3.94/4.14 (step @p272 :rule bool-and-de-morgan :args (@t919 @t917 true)) % 3.94/4.14 (step @p273 :rule refl :args (@t981)) % 3.94/4.14 (step @p274 :rule nary_cong :premises (@p273 @p272) :args ((or @t981 (not (and @t919 @t917))))) % 3.94/4.14 (step @p275 :rule bool-and-de-morgan :args (@t920 @t919 (and @t917))) % 3.94/4.14 (step @p276 :rule trans :premises (@p275 @p274)) % 3.94/4.14 (step @p277 :rule refl :args (@t982)) % 3.94/4.14 (step @p278 :rule nary_cong :premises (@p277 @p276) :args ((or @t982 (not (and @t920 @t919 @t917))))) % 3.94/4.14 (step @p279 :rule bool-and-de-morgan :args (@t921 @t920 (and @t919 @t917))) % 3.94/4.14 (step @p280 :rule trans :premises (@p279 @p278)) % 3.94/4.14 (step @p281 :rule refl :args (@t983)) % 3.94/4.14 (step @p282 :rule nary_cong :premises (@p281 @p280) :args ((or @t983 (not (and @t921 @t920 @t919 @t917))))) % 3.94/4.14 (step @p283 :rule bool-and-de-morgan :args (@t919 @t921 (and @t920 @t919 @t917))) % 3.94/4.14 (step @p284 :rule trans :premises (@p283 @p282)) % 3.94/4.14 (step @p285 :rule refl :args (@t984)) % 3.94/4.14 (step @p286 :rule nary_cong :premises (@p285 @p284) :args ((or @t984 (not (and @t919 @t921 @t920 @t919 @t917))))) % 3.94/4.14 (step @p287 :rule bool-and-de-morgan :args (@t922 @t919 (and @t921 @t920 @t919 @t917))) % 3.94/4.14 (step @p288 :rule trans :premises (@p287 @p286)) % 3.94/4.14 (step @p289 :rule trans :premises (@p288 @p271)) % 3.94/4.14 (step @p290 :rule trans :premises (@p289 @p270)) % 3.94/4.14 (step @p291 :rule nary_cong :premises (@p290 @p269) :args ((or (not @t923) @t916))) % 3.94/4.14 (step @p292 :rule trans :premises (@p291 @p268)) % 3.94/4.14 (step @p293 :rule bool-impl-elim :args (@t923 @t916)) % 3.94/4.14 (step @p294 :rule trans :premises (@p293 @p292)) % 3.94/4.14 (step @p295 :rule cong :premises (@p294) :args (@t925)) % 3.94/4.14 (step @p296 :rule aci_norm :args ((= (or @t1017 @t930) @t1002))) % 3.94/4.14 (step @p297 :rule refl :args (@t930)) % 3.94/4.14 (step @p298 :rule aci_norm :args ((= (or @t1001 (or @t1000 @t999)) @t1017))) % 3.94/4.14 (step @p299 :rule bool-and-de-morgan :args (@t929 @t927 true)) % 3.94/4.14 (step @p300 :rule refl :args (@t1001)) % 3.94/4.14 (step @p301 :rule nary_cong :premises (@p300 @p299) :args ((or @t1001 (not @t930)))) % 3.94/4.14 (step @p302 :rule bool-and-de-morgan :args (@t931 @t929 (and @t927))) % 3.94/4.14 (step @p303 :rule trans :premises (@p302 @p301)) % 3.94/4.14 (step @p304 :rule trans :premises (@p303 @p298)) % 3.94/4.14 (step @p305 :rule nary_cong :premises (@p304 @p297) :args ((or (not @t932) @t930))) % 3.94/4.14 (step @p306 :rule trans :premises (@p305 @p296)) % 3.94/4.14 (step @p307 :rule bool-impl-elim :args (@t932 @t930)) % 3.94/4.14 (step @p308 :rule trans :premises (@p307 @p306)) % 3.94/4.14 (step @p309 :rule cong :premises (@p308) :args (@t934)) % 3.94/4.14 (step @p310 :rule nary_cong :premises (@p309 @p295) :args (@t935)) % 3.94/4.14 (step @p311 :rule cong :premises (@p310) :args (@t936)) % 3.94/4.14 (step @p312 :rule eq_resolve :premises (@p140 @p311)) % 3.94/4.14 (step @p313 :rule not_and :premises (@p312)) % 3.94/4.14 (step @p314 :rule chain_m_resolution :premises (@p313 @p267) :args (@t1018 @t998 (@list @t1003))) % 3.94/4.14 (step @p315 :rule refl :args (@t1024)) % 3.94/4.14 (step @p316 :rule bool-double-not-elim :args (@t986)) % 3.94/4.14 (step @p317 :rule nary_cong :premises (@p316 @p315) :args ((or (not @t1018) @t1024))) % 3.94/4.14 (assume-push @p361 @t1018) % 3.94/4.14 (step @p319 :rule skolemize :premises (@p361)) % 3.94/4.14 (step-pop @p362 :rule scope :premises (@p319)) % 3.94/4.14 (step @p320 :rule process_scope :premises (@p362) :args (@t1024)) % 3.94/4.14 (step @p322 :rule implies_elim :premises (@p320)) % 3.94/4.14 (step @p323 :rule eq_resolve :premises (@p322 @p317)) % 3.94/4.14 (step @p324 :rule chain_m_resolution :premises (@p323 @p314) :args (@t1024 @t978 (@list @t986))) % 3.94/4.14 (step @p325 :rule bool-double-not-elim :args (@t1019)) % 3.94/4.14 (step @p326 :rule refl :args (@t1023)) % 3.94/4.14 (step @p327 :rule nary_cong :premises (@p326 @p325) :args ((or @t1023 (not @t1020)))) % 3.94/4.14 (step @p328 :rule cnf_or_neg :args (@t1023 3)) % 3.94/4.14 (step @p329 :rule eq_resolve :premises (@p328 @p327)) % 3.94/4.14 (step @p330 :rule reordering :premises (@p329) :args ((or @t1019 @t1023))) % 3.94/4.14 (step @p331 :rule chain_m_resolution :premises (@p330 @p324) :args (@t1019 @t978 @t1025)) % 3.94/4.14 (step @p332 :rule cnf_equiv_pos1 :args (@t1026)) % 3.94/4.14 (step @p333 :rule reordering :premises (@p332) :args ((or @t1020 @t994 (not @t1026)))) % 3.94/4.14 (step @p334 :rule chain_m_resolution :premises (@p333 @p331 @p242) :args (@t994 (@list false false) (@list @t1019 @t1026))) % 3.94/4.14 (step @p335 :rule cnf_or_neg :args (@t1023 5)) % 3.94/4.14 (step @p336 :rule chain_m_resolution :premises (@p335 @p324) :args ((not @t989) @t978 @t1025)) % 3.94/4.14 (step @p337 :rule cnf_or_pos :args (@t997)) % 3.94/4.14 (step @p338 :rule reordering :premises (@p337) :args ((or @t989 @t995 @t993 (not @t997)))) % 3.94/4.14 (step @p339 :rule chain_m_resolution :premises (@p338 @p336 @p334 @p241) :args (@t993 @t1012 (@list @t989 @t994 @t997))) % 3.94/4.14 (step @p340 :rule bool-double-not-elim :args (@t1021)) % 3.94/4.14 (step @p341 :rule nary_cong :premises (@p326 @p340) :args ((or @t1023 (not @t1022)))) % 3.94/4.14 (step @p342 :rule cnf_or_neg :args (@t1023 0)) % 3.94/4.14 (step @p343 :rule eq_resolve :premises (@p342 @p341)) % 3.94/4.14 (step @p344 :rule reordering :premises (@p343) :args ((or @t1021 @t1023))) % 3.94/4.14 (step @p345 :rule chain_m_resolution :premises (@p344 @p324) :args (@t1021 @t978 @t1025)) % 3.94/4.14 (step @p346 :rule cnf_equiv_pos1 :args (@t1027)) % 3.94/4.14 (step @p347 :rule reordering :premises (@p346) :args ((or @t1022 @t992 @t1028))) % 3.94/4.14 (step @p348 :rule chain_m_resolution :premises (@p347 @p345 @p339) :args (@t1028 (@list false true) (@list @t1021 @t992))) % 3.94/4.14 (assume-push @p363 @t969) % 3.94/4.14 (step @p350 :rule instantiate :premises (@p221) :args ((@list @t988 @t991))) % 3.94/4.14 (step-pop @p364 :rule scope :premises (@p350)) % 3.94/4.14 (step @p351 :rule process_scope :premises (@p364) :args (@t1027)) % 3.94/4.14 (step @p353 :rule implies_elim :premises (@p351)) % 3.94/4.14 (step @p354 false :rule chain_m_resolution :premises (@p353 @p348 @p221) :args (false (@list true false) (@list @t1027 @t969))) % 3.94/4.14 ) % 3.94/4.14 % SZS output end Proof % 3.94/4.14 % cvc5 exiting %------------------------------------------------------------------------------