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