%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : SWV036+1 : TPTP v9.2.1. Bugfixed v3.3.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n025.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 09:00:23 AM UTC 2026 % Result : Theorem 0.39s 0.77s % Output : Proof 0.39s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.13 % Problem : SWV036+1 : TPTP v9.2.1. Bugfixed v3.3.0. % 0.12/0.14 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.17/0.35 % Computer : n025.cluster.edu % 0.17/0.35 % Model : x86_64 x86_64 % 0.17/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.35 % Memory : 8042.1875MB % 0.17/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.35 % CPULimit : 300 % 0.17/0.35 % WCLimit : 300 % 0.17/0.35 % DateTime : Tue Jun 2 19:53:46 EDT 2026 % 0.17/0.35 % CPUTime : % 0.28/0.53 %----Proving TF0_NAR, FOF, or CNF % 0.39/0.77 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 0.39/0.77 % SZS status Theorem % 0.39/0.77 % SZS output start Proof % 0.39/0.77 ( % 0.39/0.77 (declare-sort $$unsorted 0) % 0.39/0.77 (declare-const tptp.s_values7 $$unsorted) % 0.39/0.77 (declare-const tptp.s_best7 $$unsorted) % 0.39/0.77 (declare-const tptp.s_worst7_init $$unsorted) % 0.39/0.77 (declare-const tptp.pv1388 $$unsorted) % 0.39/0.77 (declare-const tptp.simplex7_init $$unsorted) % 0.39/0.77 (declare-const tptp.s_values7_init $$unsorted) % 0.39/0.77 (declare-const tptp.pvar1400_init $$unsorted) % 0.39/0.77 (declare-const tptp.pvar1401_init $$unsorted) % 0.39/0.77 (declare-const tptp.init $$unsorted) % 0.39/0.77 (declare-const tptp.def $$unsorted) % 0.39/0.77 (declare-const tptp.use $$unsorted) % 0.39/0.77 (declare-const tptp.true Bool) % 0.39/0.77 (declare-const tptp.tptp_update2 (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.39/0.77 (declare-const tptp.s_worst7 $$unsorted) % 0.39/0.77 (declare-const tptp.a_select3 (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.39/0.77 (declare-const tptp.loopcounter $$unsorted) % 0.39/0.77 (declare-const tptp.gt (-> $$unsorted $$unsorted Bool)) % 0.39/0.77 (declare-const tptp.uniform_int_rnd (-> $$unsorted $$unsorted $$unsorted)) % 0.39/0.77 (declare-const tptp.s_sworst7_init $$unsorted) % 0.39/0.77 (declare-const tptp.n3 $$unsorted) % 0.39/0.77 (declare-const tptp.tptp_const_array1 (-> $$unsorted $$unsorted $$unsorted)) % 0.39/0.77 (declare-const tptp.pred (-> $$unsorted $$unsorted)) % 0.39/0.77 (declare-const tptp.tptp_minus_1 $$unsorted) % 0.39/0.77 (declare-const tptp.n0 $$unsorted) % 0.39/0.77 (declare-const tptp.tptp_msub (-> $$unsorted $$unsorted $$unsorted)) % 0.39/0.77 (declare-const tptp.n1 $$unsorted) % 0.39/0.77 (declare-const tptp.succ (-> $$unsorted $$unsorted)) % 0.39/0.77 (declare-const tptp.n5 $$unsorted) % 0.39/0.77 (declare-const tptp.s_best7_init $$unsorted) % 0.39/0.77 (declare-const tptp.lt (-> $$unsorted $$unsorted Bool)) % 0.39/0.77 (declare-const tptp.tptp_update3 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.39/0.77 (declare-const tptp.minus (-> $$unsorted $$unsorted $$unsorted)) % 0.39/0.77 (declare-const tptp.s_sworst7 $$unsorted) % 0.39/0.77 (declare-const tptp.tptp_const_array2 (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.39/0.77 (declare-const tptp.geq (-> $$unsorted $$unsorted Bool)) % 0.39/0.77 (declare-const tptp.leq (-> $$unsorted $$unsorted Bool)) % 0.39/0.77 (declare-const tptp.trans (-> $$unsorted $$unsorted)) % 0.39/0.77 (declare-const tptp.a_select2 (-> $$unsorted $$unsorted $$unsorted)) % 0.39/0.77 (declare-const tptp.inv (-> $$unsorted $$unsorted)) % 0.39/0.77 (declare-const tptp.dim (-> $$unsorted $$unsorted $$unsorted)) % 0.39/0.77 (declare-const tptp.plus (-> $$unsorted $$unsorted $$unsorted)) % 0.39/0.77 (declare-const tptp.pvar1402_init $$unsorted) % 0.39/0.77 (declare-const tptp.tptp_madd (-> $$unsorted $$unsorted $$unsorted)) % 0.39/0.77 (declare-const tptp.sum (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.39/0.77 (declare-const tptp.tptp_mmul (-> $$unsorted $$unsorted $$unsorted)) % 0.39/0.77 (declare-const tptp.tptp_float_0_0 $$unsorted) % 0.39/0.77 (declare-const tptp.s_center7_init $$unsorted) % 0.39/0.77 (declare-const tptp.n4 $$unsorted) % 0.39/0.77 (declare-const tptp.n2 $$unsorted) % 0.39/0.77 (define @t1 () (@var "Y" $$unsorted)) % 0.39/0.77 (define @t2 () (@var "X" $$unsorted)) % 0.39/0.77 (define @t3 () (= @t2 @t1)) % 0.39/0.77 (define @t4 () (tptp.gt @t1 @t2)) % 0.39/0.77 (define @t5 () (tptp.gt @t2 @t1)) % 0.39/0.77 (define @t6 () (@list @t2 @t1)) % 0.39/0.77 (define @t7 () (@var "Z" $$unsorted)) % 0.39/0.77 (define @t8 () (@list @t2 @t1 @t7)) % 0.39/0.77 (define @t9 () (@list @t2)) % 0.39/0.77 (define @t10 () (tptp.leq @t2 @t1)) % 0.39/0.77 (define @t11 () (forall @t6 (=> @t4 @t10))) % 0.39/0.77 (define @t12 () (tptp.succ @t2)) % 0.39/0.77 (define @t13 () (tptp.succ @t1)) % 0.39/0.77 (define @t14 () (@var "C" $$unsorted)) % 0.39/0.77 (define @t15 () (tptp.uniform_int_rnd @t14 @t2)) % 0.39/0.77 (define @t16 () (tptp.leq tptp.n0 @t2)) % 0.39/0.77 (define @t17 () (@list @t2 @t14)) % 0.39/0.77 (define @t18 () (@var "Val" $$unsorted)) % 0.39/0.77 (define @t19 () (@var "I" $$unsorted)) % 0.39/0.77 (define @t20 () (@var "U" $$unsorted)) % 0.39/0.77 (define @t21 () (@var "L" $$unsorted)) % 0.39/0.77 (define @t22 () (tptp.leq @t19 @t20)) % 0.39/0.77 (define @t23 () (@var "J" $$unsorted)) % 0.39/0.77 (define @t24 () (@var "U2" $$unsorted)) % 0.39/0.77 (define @t25 () (@var "L2" $$unsorted)) % 0.39/0.77 (define @t26 () (@var "U1" $$unsorted)) % 0.39/0.77 (define @t27 () (@var "L1" $$unsorted)) % 0.39/0.77 (define @t28 () (@var "A" $$unsorted)) % 0.39/0.77 (define @t29 () (tptp.trans @t28)) % 0.39/0.77 (define @t30 () (@var "N" $$unsorted)) % 0.39/0.77 (define @t31 () (tptp.leq @t23 @t30)) % 0.39/0.77 (define @t32 () (tptp.leq tptp.n0 @t23)) % 0.39/0.77 (define @t33 () (tptp.leq @t19 @t30)) % 0.39/0.77 (define @t34 () (tptp.leq tptp.n0 @t19)) % 0.39/0.77 (define @t35 () (and @t34 @t33 @t32 @t31)) % 0.39/0.77 (define @t36 () (@list @t19 @t23)) % 0.39/0.77 (define @t37 () (forall @t36 (=> @t35 (= (tptp.a_select3 @t28 @t19 @t23) (tptp.a_select3 @t28 @t23 @t19))))) % 0.39/0.77 (define @t38 () (@list @t28 @t30)) % 0.39/0.77 (define @t39 () (tptp.inv @t28)) % 0.39/0.77 (define @t40 () (@var "VAL" $$unsorted)) % 0.39/0.77 (define @t41 () (@var "K" $$unsorted)) % 0.39/0.77 (define @t42 () (tptp.tptp_update3 @t28 @t41 @t41 @t40)) % 0.39/0.77 (define @t43 () (tptp.leq tptp.n0 @t41)) % 0.39/0.77 (define @t44 () (@var "B" $$unsorted)) % 0.39/0.77 (define @t45 () (tptp.tptp_madd @t28 @t44)) % 0.39/0.77 (define @t46 () (= (tptp.a_select3 @t44 @t19 @t23) (tptp.a_select3 @t44 @t23 @t19))) % 0.39/0.77 (define @t47 () (forall @t36 (=> @t35 @t46))) % 0.39/0.77 (define @t48 () (and @t37 @t47)) % 0.39/0.77 (define @t49 () (@list @t28 @t44 @t30)) % 0.39/0.77 (define @t50 () (tptp.tptp_msub @t28 @t44)) % 0.39/0.77 (define @t51 () (tptp.tptp_mmul @t28 (tptp.tptp_mmul @t44 @t29))) % 0.39/0.77 (define @t52 () (forall @t36 (=> @t35 (= (tptp.a_select3 @t51 @t19 @t23) (tptp.a_select3 @t51 @t23 @t19))))) % 0.39/0.77 (define @t53 () (@var "M" $$unsorted)) % 0.39/0.77 (define @t54 () (and @t34 (tptp.leq @t19 @t53) @t32 (tptp.leq @t23 @t53))) % 0.39/0.77 (define @t55 () (@var "E" $$unsorted)) % 0.39/0.77 (define @t56 () (@var "F" $$unsorted)) % 0.39/0.77 (define @t57 () (@var "D" $$unsorted)) % 0.39/0.77 (define @t58 () (tptp.tptp_madd @t28 (tptp.tptp_mmul @t44 (tptp.tptp_mmul (tptp.tptp_madd (tptp.tptp_mmul @t14 (tptp.tptp_mmul @t57 (tptp.trans @t14))) (tptp.tptp_mmul @t55 (tptp.tptp_mmul @t56 (tptp.trans @t55)))) (tptp.trans @t44))))) % 0.39/0.77 (define @t59 () (@var "Body" $$unsorted)) % 0.39/0.77 (define @t60 () (tptp.sum tptp.n0 tptp.tptp_minus_1 @t59)) % 0.39/0.77 (define @t61 () (@list @t59)) % 0.39/0.77 (define @t62 () (tptp.succ @t12)) % 0.39/0.77 (define @t63 () (tptp.succ @t62)) % 0.39/0.77 (define @t64 () (tptp.succ @t63)) % 0.39/0.77 (define @t65 () (tptp.succ @t64)) % 0.39/0.77 (define @t66 () (tptp.pred @t2)) % 0.39/0.77 (define @t67 () (tptp.leq @t12 @t1)) % 0.39/0.77 (define @t68 () (forall @t6 (=> @t67 @t4))) % 0.39/0.77 (define @t69 () (@var "V" $$unsorted)) % 0.39/0.77 (define @t70 () (tptp.tptp_update3 @t2 @t20 @t69 @t40)) % 0.39/0.77 (define @t71 () (@var "VAL2" $$unsorted)) % 0.39/0.77 (define @t72 () (not (= @t19 @t20))) % 0.39/0.77 (define @t73 () (@var "J0" $$unsorted)) % 0.39/0.77 (define @t74 () (@var "I0" $$unsorted)) % 0.39/0.77 (define @t75 () (tptp.leq @t74 @t20)) % 0.39/0.77 (define @t76 () (tptp.leq tptp.n0 @t74)) % 0.39/0.77 (define @t77 () (tptp.tptp_update2 @t2 @t20 @t40)) % 0.39/0.77 (define @t78 () (and (= tptp.pvar1400_init tptp.init) (= tptp.pvar1401_init tptp.init) (= tptp.pvar1402_init tptp.init))) % 0.39/0.77 (define @t79 () (tptp.gt tptp.loopcounter tptp.n1)) % 0.39/0.77 (define @t80 () (=> @t79 @t78)) % 0.39/0.77 (define @t81 () (@var "T" $$unsorted)) % 0.39/0.77 (define @t82 () (tptp.a_select2 tptp.s_center7_init @t81)) % 0.39/0.77 (define @t83 () (tptp.leq @t81 tptp.n2)) % 0.39/0.77 (define @t84 () (tptp.leq tptp.n0 @t81)) % 0.39/0.77 (define @t85 () (and @t84 @t83)) % 0.39/0.77 (define @t86 () (=> @t85 (= @t82 tptp.init))) % 0.39/0.77 (define @t87 () (@list @t81)) % 0.39/0.77 (define @t88 () (forall @t87 @t86)) % 0.39/0.77 (define @t89 () (@var "S" $$unsorted)) % 0.39/0.77 (define @t90 () (tptp.a_select2 tptp.s_values7_init @t89)) % 0.39/0.77 (define @t91 () (tptp.leq @t89 tptp.n3)) % 0.39/0.77 (define @t92 () (tptp.leq tptp.n0 @t89)) % 0.39/0.77 (define @t93 () (and @t92 @t91)) % 0.39/0.77 (define @t94 () (=> @t93 (= @t90 tptp.init))) % 0.39/0.77 (define @t95 () (@list @t89)) % 0.39/0.77 (define @t96 () (forall @t95 @t94)) % 0.39/0.77 (define @t97 () (@var "Q" $$unsorted)) % 0.39/0.77 (define @t98 () (@var "R" $$unsorted)) % 0.39/0.77 (define @t99 () (tptp.a_select3 tptp.simplex7_init @t98 @t97)) % 0.39/0.77 (define @t100 () (tptp.leq @t98 tptp.n3)) % 0.39/0.77 (define @t101 () (tptp.leq tptp.n0 @t98)) % 0.39/0.77 (define @t102 () (and @t101 @t100)) % 0.39/0.77 (define @t103 () (=> @t102 (= @t99 tptp.init))) % 0.39/0.77 (define @t104 () (@list @t98)) % 0.39/0.77 (define @t105 () (forall @t104 @t103)) % 0.39/0.77 (define @t106 () (tptp.leq @t97 tptp.n2)) % 0.39/0.77 (define @t107 () (tptp.leq tptp.n0 @t97)) % 0.39/0.77 (define @t108 () (and @t107 @t106)) % 0.39/0.77 (define @t109 () (=> @t108 @t105)) % 0.39/0.77 (define @t110 () (@list @t97)) % 0.39/0.77 (define @t111 () (forall @t110 @t109)) % 0.39/0.77 (define @t112 () (tptp.leq tptp.pv1388 tptp.n3)) % 0.39/0.77 (define @t113 () (tptp.leq tptp.s_worst7 tptp.n3)) % 0.39/0.77 (define @t114 () (tptp.leq tptp.s_sworst7 tptp.n3)) % 0.39/0.77 (define @t115 () (tptp.leq tptp.n0 tptp.pv1388)) % 0.39/0.77 (define @t116 () (tptp.leq tptp.n0 tptp.s_worst7)) % 0.39/0.77 (define @t117 () (tptp.leq tptp.n0 tptp.s_sworst7)) % 0.39/0.77 (define @t118 () (= tptp.s_worst7_init tptp.init)) % 0.39/0.77 (define @t119 () (= tptp.s_sworst7_init tptp.init)) % 0.39/0.77 (define @t120 () (= tptp.init tptp.init)) % 0.39/0.77 (define @t121 () (and @t120 @t119 @t118 @t117 @t116 @t115 @t114 @t113 @t112 @t111 @t96 @t88 @t80)) % 0.39/0.77 (define @t122 () (tptp.a_select2 tptp.s_values7 tptp.pv1388)) % 0.39/0.77 (define @t123 () (tptp.gt @t122 (tptp.a_select2 tptp.s_values7 tptp.s_best7))) % 0.39/0.77 (define @t124 () (=> @t123 @t121)) % 0.39/0.77 (define @t125 () (@var "P" $$unsorted)) % 0.39/0.77 (define @t126 () (tptp.a_select2 tptp.s_center7_init @t125)) % 0.39/0.77 (define @t127 () (tptp.leq @t125 tptp.n2)) % 0.39/0.77 (define @t128 () (tptp.leq tptp.n0 @t125)) % 0.39/0.77 (define @t129 () (and @t128 @t127)) % 0.39/0.77 (define @t130 () (=> @t129 (= @t126 tptp.init))) % 0.39/0.77 (define @t131 () (@list @t125)) % 0.39/0.77 (define @t132 () (forall @t131 @t130)) % 0.39/0.77 (define @t133 () (@var "O" $$unsorted)) % 0.39/0.77 (define @t134 () (tptp.a_select2 tptp.s_values7_init @t133)) % 0.39/0.77 (define @t135 () (tptp.leq @t133 tptp.n3)) % 0.39/0.77 (define @t136 () (tptp.leq tptp.n0 @t133)) % 0.39/0.77 (define @t137 () (and @t136 @t135)) % 0.39/0.77 (define @t138 () (=> @t137 (= @t134 tptp.init))) % 0.39/0.77 (define @t139 () (@list @t133)) % 0.39/0.77 (define @t140 () (forall @t139 @t138)) % 0.39/0.77 (define @t141 () (tptp.a_select3 tptp.simplex7_init @t30 @t53)) % 0.39/0.77 (define @t142 () (tptp.leq @t30 tptp.n3)) % 0.39/0.77 (define @t143 () (tptp.leq tptp.n0 @t30)) % 0.39/0.77 (define @t144 () (and @t143 @t142)) % 0.39/0.77 (define @t145 () (=> @t144 (= @t141 tptp.init))) % 0.39/0.77 (define @t146 () (@list @t30)) % 0.39/0.77 (define @t147 () (forall @t146 @t145)) % 0.39/0.77 (define @t148 () (tptp.leq @t53 tptp.n2)) % 0.39/0.77 (define @t149 () (tptp.leq tptp.n0 @t53)) % 0.39/0.77 (define @t150 () (and @t149 @t148)) % 0.39/0.77 (define @t151 () (=> @t150 @t147)) % 0.39/0.77 (define @t152 () (@list @t53)) % 0.39/0.77 (define @t153 () (forall @t152 @t151)) % 0.39/0.77 (define @t154 () (tptp.leq tptp.s_best7 tptp.n3)) % 0.39/0.77 (define @t155 () (tptp.leq tptp.n0 tptp.s_best7)) % 0.39/0.77 (define @t156 () (= tptp.s_best7_init tptp.init)) % 0.39/0.77 (define @t157 () (and @t120 @t156 @t118 @t155 @t116 @t115 @t154 @t113 @t112 @t153 @t140 @t132 @t80)) % 0.39/0.77 (define @t158 () (tptp.leq @t122 (tptp.a_select2 tptp.s_values7 tptp.s_worst7))) % 0.39/0.77 (define @t159 () (=> @t158 @t157)) % 0.39/0.77 (define @t160 () (tptp.a_select2 tptp.s_center7_init @t21)) % 0.39/0.77 (define @t161 () (tptp.leq @t21 tptp.n2)) % 0.39/0.77 (define @t162 () (tptp.leq tptp.n0 @t21)) % 0.39/0.77 (define @t163 () (and @t162 @t161)) % 0.39/0.77 (define @t164 () (=> @t163 (= @t160 tptp.init))) % 0.39/0.77 (define @t165 () (@list @t21)) % 0.39/0.78 (define @t166 () (forall @t165 @t164)) % 0.39/0.78 (define @t167 () (tptp.a_select2 tptp.s_values7_init @t41)) % 0.39/0.78 (define @t168 () (tptp.leq @t41 tptp.n3)) % 0.39/0.78 (define @t169 () (and @t43 @t168)) % 0.39/0.78 (define @t170 () (=> @t169 (= @t167 tptp.init))) % 0.39/0.78 (define @t171 () (@list @t41)) % 0.39/0.78 (define @t172 () (forall @t171 @t170)) % 0.39/0.78 (define @t173 () (tptp.a_select3 tptp.simplex7_init @t23 @t19)) % 0.39/0.78 (define @t174 () (tptp.leq @t23 tptp.n3)) % 0.39/0.78 (define @t175 () (and @t32 @t174)) % 0.39/0.78 (define @t176 () (=> @t175 (= @t173 tptp.init))) % 0.39/0.78 (define @t177 () (@list @t23)) % 0.39/0.78 (define @t178 () (forall @t177 @t176)) % 0.39/0.78 (define @t179 () (tptp.leq @t19 tptp.n2)) % 0.39/0.78 (define @t180 () (and @t34 @t179)) % 0.39/0.78 (define @t181 () (=> @t180 @t178)) % 0.39/0.78 (define @t182 () (@list @t19)) % 0.39/0.78 (define @t183 () (forall @t182 @t181)) % 0.39/0.78 (define @t184 () (and @t120 @t156 @t118 @t155 @t116 @t115 @t154 @t113 @t112 @t183 @t172 @t166 @t80)) % 0.39/0.78 (define @t185 () (tptp.leq @t122 (tptp.a_select2 tptp.s_values7 tptp.s_sworst7))) % 0.39/0.78 (define @t186 () (=> @t185 @t184)) % 0.39/0.78 (define @t187 () (@var "H" $$unsorted)) % 0.39/0.78 (define @t188 () (tptp.a_select2 tptp.s_center7_init @t187)) % 0.39/0.78 (define @t189 () (tptp.leq @t187 tptp.n2)) % 0.39/0.78 (define @t190 () (tptp.leq tptp.n0 @t187)) % 0.39/0.78 (define @t191 () (and @t190 @t189)) % 0.39/0.78 (define @t192 () (=> @t191 (= @t188 tptp.init))) % 0.39/0.78 (define @t193 () (@list @t187)) % 0.39/0.78 (define @t194 () (forall @t193 @t192)) % 0.39/0.78 (define @t195 () (@var "G" $$unsorted)) % 0.39/0.78 (define @t196 () (tptp.a_select2 tptp.s_values7_init @t195)) % 0.39/0.78 (define @t197 () (tptp.leq @t195 tptp.n3)) % 0.39/0.78 (define @t198 () (tptp.leq tptp.n0 @t195)) % 0.39/0.78 (define @t199 () (and @t198 @t197)) % 0.39/0.78 (define @t200 () (=> @t199 (= @t196 tptp.init))) % 0.39/0.78 (define @t201 () (@list @t195)) % 0.39/0.78 (define @t202 () (forall @t201 @t200)) % 0.39/0.78 (define @t203 () (tptp.a_select3 tptp.simplex7_init @t56 @t55)) % 0.39/0.78 (define @t204 () (tptp.leq @t56 tptp.n3)) % 0.39/0.78 (define @t205 () (tptp.leq tptp.n0 @t56)) % 0.39/0.78 (define @t206 () (and @t205 @t204)) % 0.39/0.78 (define @t207 () (=> @t206 (= @t203 tptp.init))) % 0.39/0.78 (define @t208 () (@list @t56)) % 0.39/0.78 (define @t209 () (forall @t208 @t207)) % 0.39/0.78 (define @t210 () (tptp.leq @t55 tptp.n2)) % 0.39/0.78 (define @t211 () (tptp.leq tptp.n0 @t55)) % 0.39/0.78 (define @t212 () (and @t211 @t210)) % 0.39/0.78 (define @t213 () (=> @t212 @t209)) % 0.39/0.78 (define @t214 () (@list @t55)) % 0.39/0.78 (define @t215 () (forall @t214 @t213)) % 0.39/0.78 (define @t216 () (and @t156 @t119 @t118 @t155 @t117 @t116 @t154 @t114 @t113 @t215 @t202 @t194 @t80)) % 0.39/0.78 (define @t217 () (not @t185)) % 0.39/0.78 (define @t218 () (=> @t217 @t216)) % 0.39/0.78 (define @t219 () (tptp.a_select2 tptp.s_values7_init tptp.pv1388)) % 0.39/0.78 (define @t220 () (= @t219 tptp.init)) % 0.39/0.78 (define @t221 () (tptp.a_select2 tptp.s_values7_init tptp.s_sworst7)) % 0.39/0.78 (define @t222 () (and @t120 @t119 (= @t221 tptp.init) @t220 @t218 @t186)) % 0.39/0.78 (define @t223 () (not @t158)) % 0.39/0.78 (define @t224 () (=> @t223 @t222)) % 0.39/0.78 (define @t225 () (tptp.a_select2 tptp.s_values7_init tptp.s_worst7)) % 0.39/0.78 (define @t226 () (and @t120 @t118 (= @t225 tptp.init) @t220 @t224 @t159)) % 0.39/0.78 (define @t227 () (not @t123)) % 0.39/0.78 (define @t228 () (=> @t227 @t226)) % 0.39/0.78 (define @t229 () (tptp.a_select2 tptp.s_values7_init tptp.s_best7)) % 0.39/0.78 (define @t230 () (and @t120 @t156 (= @t229 tptp.init) @t220 @t228 @t124)) % 0.39/0.78 (define @t231 () (tptp.a_select2 tptp.s_center7_init @t57)) % 0.39/0.78 (define @t232 () (tptp.leq @t57 tptp.n2)) % 0.39/0.78 (define @t233 () (tptp.leq tptp.n0 @t57)) % 0.39/0.78 (define @t234 () (and @t233 @t232)) % 0.39/0.78 (define @t235 () (=> @t234 (= @t231 tptp.init))) % 0.39/0.78 (define @t236 () (@list @t57)) % 0.39/0.78 (define @t237 () (forall @t236 @t235)) % 0.39/0.78 (define @t238 () (tptp.a_select2 tptp.s_values7_init @t14)) % 0.39/0.78 (define @t239 () (tptp.leq @t14 tptp.n3)) % 0.39/0.78 (define @t240 () (tptp.leq tptp.n0 @t14)) % 0.39/0.78 (define @t241 () (and @t240 @t239)) % 0.39/0.78 (define @t242 () (=> @t241 (= @t238 tptp.init))) % 0.39/0.78 (define @t243 () (@list @t14)) % 0.39/0.78 (define @t244 () (forall @t243 @t242)) % 0.39/0.78 (define @t245 () (tptp.a_select3 tptp.simplex7_init @t44 @t28)) % 0.39/0.78 (define @t246 () (tptp.leq @t44 tptp.n3)) % 0.39/0.78 (define @t247 () (tptp.leq tptp.n0 @t44)) % 0.39/0.78 (define @t248 () (and @t247 @t246)) % 0.39/0.78 (define @t249 () (=> @t248 (= @t245 tptp.init))) % 0.39/0.78 (define @t250 () (@list @t44)) % 0.39/0.78 (define @t251 () (forall @t250 @t249)) % 0.39/0.78 (define @t252 () (tptp.leq @t28 tptp.n2)) % 0.39/0.78 (define @t253 () (tptp.leq tptp.n0 @t28)) % 0.39/0.78 (define @t254 () (and @t253 @t252)) % 0.39/0.78 (define @t255 () (=> @t254 @t251)) % 0.39/0.78 (define @t256 () (@list @t28)) % 0.39/0.78 (define @t257 () (forall @t256 @t255)) % 0.39/0.78 (define @t258 () (tptp.leq tptp.n2 tptp.pv1388)) % 0.39/0.78 (define @t259 () (and @t156 @t119 @t118 @t155 @t117 @t116 @t258 @t154 @t114 @t113 @t112 @t257 @t244 @t237 @t80)) % 0.39/0.78 (define @t260 () (=> @t259 @t230)) % 0.39/0.78 (define @t261 () (not @t260)) % 0.39/0.78 (define @t262 () (= @t2 tptp.n4)) % 0.39/0.78 (define @t263 () (= @t2 tptp.n3)) % 0.39/0.78 (define @t264 () (= @t2 tptp.n2)) % 0.39/0.78 (define @t265 () (= @t2 tptp.n1)) % 0.39/0.78 (define @t266 () (= @t2 tptp.n0)) % 0.39/0.78 (define @t267 () (tptp.succ tptp.n0)) % 0.39/0.78 (define @t268 () (tptp.succ @t267)) % 0.39/0.78 (define @t269 () (tptp.succ @t268)) % 0.39/0.78 (define @t270 () (tptp.succ @t269)) % 0.39/0.78 (define @t271 () (=> @t79 (and (= tptp.init tptp.pvar1400_init) (= tptp.init tptp.pvar1401_init) (= tptp.init tptp.pvar1402_init)))) % 0.39/0.78 (define @t272 () (= tptp.init @t82)) % 0.39/0.78 (define @t273 () (not @t83)) % 0.39/0.78 (define @t274 () (not @t84)) % 0.39/0.78 (define @t275 () (or @t274 @t273 @t272)) % 0.39/0.78 (define @t276 () (forall @t87 @t275)) % 0.39/0.78 (define @t277 () (= tptp.init @t90)) % 0.39/0.78 (define @t278 () (not @t91)) % 0.39/0.78 (define @t279 () (not @t92)) % 0.39/0.78 (define @t280 () (or @t279 @t278 @t277)) % 0.39/0.78 (define @t281 () (forall @t95 @t280)) % 0.39/0.78 (define @t282 () (@var "BOUND_VARIABLE_8787" $$unsorted)) % 0.39/0.78 (define @t283 () (= tptp.init (tptp.a_select3 tptp.simplex7_init @t282 @t97))) % 0.39/0.78 (define @t284 () (not (tptp.leq @t282 tptp.n3))) % 0.39/0.78 (define @t285 () (not (tptp.leq tptp.n0 @t282))) % 0.39/0.78 (define @t286 () (not @t106)) % 0.39/0.78 (define @t287 () (not @t107)) % 0.39/0.78 (define @t288 () (or @t287 @t286 @t285 @t284 @t283)) % 0.39/0.78 (define @t289 () (@list @t97 @t282)) % 0.39/0.78 (define @t290 () (forall @t289 @t288)) % 0.39/0.78 (define @t291 () (= tptp.init tptp.s_worst7_init)) % 0.39/0.78 (define @t292 () (= tptp.init tptp.s_sworst7_init)) % 0.39/0.78 (define @t293 () (and @t292 @t291 @t117 @t116 @t115 @t114 @t113 @t112 @t290 @t281 @t276 @t271)) % 0.39/0.78 (define @t294 () (=> @t123 @t293)) % 0.39/0.78 (define @t295 () (= tptp.init @t126)) % 0.39/0.78 (define @t296 () (not @t127)) % 0.39/0.78 (define @t297 () (not @t128)) % 0.39/0.78 (define @t298 () (or @t297 @t296 @t295)) % 0.39/0.78 (define @t299 () (forall @t131 @t298)) % 0.39/0.78 (define @t300 () (= tptp.init @t134)) % 0.39/0.78 (define @t301 () (not @t135)) % 0.39/0.78 (define @t302 () (not @t136)) % 0.39/0.78 (define @t303 () (or @t302 @t301 @t300)) % 0.39/0.78 (define @t304 () (forall @t139 @t303)) % 0.39/0.78 (define @t305 () (@var "BOUND_VARIABLE_8732" $$unsorted)) % 0.39/0.78 (define @t306 () (= tptp.init (tptp.a_select3 tptp.simplex7_init @t305 @t53))) % 0.39/0.78 (define @t307 () (not (tptp.leq @t305 tptp.n3))) % 0.39/0.78 (define @t308 () (not (tptp.leq tptp.n0 @t305))) % 0.39/0.78 (define @t309 () (not @t148)) % 0.39/0.78 (define @t310 () (not @t149)) % 0.39/0.78 (define @t311 () (or @t310 @t309 @t308 @t307 @t306)) % 0.39/0.78 (define @t312 () (@list @t53 @t305)) % 0.39/0.78 (define @t313 () (forall @t312 @t311)) % 0.39/0.78 (define @t314 () (= tptp.init tptp.s_best7_init)) % 0.39/0.78 (define @t315 () (and @t314 @t291 @t155 @t116 @t115 @t154 @t113 @t112 @t313 @t304 @t299 @t271)) % 0.39/0.78 (define @t316 () (=> @t158 @t315)) % 0.39/0.78 (define @t317 () (= tptp.init @t160)) % 0.39/0.78 (define @t318 () (not @t161)) % 0.39/0.78 (define @t319 () (not @t162)) % 0.39/0.78 (define @t320 () (or @t319 @t318 @t317)) % 0.39/0.78 (define @t321 () (forall @t165 @t320)) % 0.39/0.78 (define @t322 () (= tptp.init @t167)) % 0.39/0.78 (define @t323 () (not @t168)) % 0.39/0.78 (define @t324 () (not @t43)) % 0.39/0.78 (define @t325 () (or @t324 @t323 @t322)) % 0.39/0.78 (define @t326 () (forall @t171 @t325)) % 0.39/0.78 (define @t327 () (@var "BOUND_VARIABLE_8678" $$unsorted)) % 0.39/0.78 (define @t328 () (= tptp.init (tptp.a_select3 tptp.simplex7_init @t327 @t19))) % 0.39/0.78 (define @t329 () (not (tptp.leq @t327 tptp.n3))) % 0.39/0.78 (define @t330 () (not (tptp.leq tptp.n0 @t327))) % 0.39/0.78 (define @t331 () (not @t179)) % 0.39/0.78 (define @t332 () (not @t34)) % 0.39/0.78 (define @t333 () (or @t332 @t331 @t330 @t329 @t328)) % 0.39/0.78 (define @t334 () (@list @t19 @t327)) % 0.39/0.78 (define @t335 () (forall @t334 @t333)) % 0.39/0.78 (define @t336 () (and @t314 @t291 @t155 @t116 @t115 @t154 @t113 @t112 @t335 @t326 @t321 @t271)) % 0.39/0.78 (define @t337 () (=> @t185 @t336)) % 0.39/0.78 (define @t338 () (= tptp.init @t188)) % 0.39/0.78 (define @t339 () (not @t189)) % 0.39/0.78 (define @t340 () (not @t190)) % 0.39/0.78 (define @t341 () (or @t340 @t339 @t338)) % 0.39/0.78 (define @t342 () (forall @t193 @t341)) % 0.39/0.78 (define @t343 () (= tptp.init @t196)) % 0.39/0.78 (define @t344 () (not @t197)) % 0.39/0.78 (define @t345 () (not @t198)) % 0.39/0.78 (define @t346 () (or @t345 @t344 @t343)) % 0.39/0.78 (define @t347 () (forall @t201 @t346)) % 0.39/0.78 (define @t348 () (@var "BOUND_VARIABLE_8629" $$unsorted)) % 0.39/0.78 (define @t349 () (= tptp.init (tptp.a_select3 tptp.simplex7_init @t348 @t55))) % 0.39/0.78 (define @t350 () (not (tptp.leq @t348 tptp.n3))) % 0.39/0.78 (define @t351 () (not (tptp.leq tptp.n0 @t348))) % 0.39/0.78 (define @t352 () (not @t210)) % 0.39/0.78 (define @t353 () (not @t211)) % 0.39/0.78 (define @t354 () (or @t353 @t352 @t351 @t350 @t349)) % 0.39/0.78 (define @t355 () (@list @t55 @t348)) % 0.39/0.78 (define @t356 () (forall @t355 @t354)) % 0.39/0.78 (define @t357 () (and @t314 @t292 @t291 @t155 @t117 @t116 @t154 @t114 @t113 @t356 @t347 @t342 @t271)) % 0.39/0.78 (define @t358 () (=> @t217 @t357)) % 0.39/0.78 (define @t359 () (= tptp.init @t219)) % 0.39/0.78 (define @t360 () (= tptp.init @t221)) % 0.39/0.78 (define @t361 () (and @t292 @t360 @t359 @t358 @t337)) % 0.39/0.78 (define @t362 () (=> @t223 @t361)) % 0.39/0.78 (define @t363 () (= tptp.init @t225)) % 0.39/0.78 (define @t364 () (and @t291 @t363 @t359 @t362 @t316)) % 0.39/0.78 (define @t365 () (=> @t227 @t364)) % 0.39/0.78 (define @t366 () (= tptp.init @t229)) % 0.39/0.78 (define @t367 () (or @t285 @t284 @t283)) % 0.39/0.78 (define @t368 () (or @t287 @t286 @t367)) % 0.39/0.78 (define @t369 () (forall @t289 @t368)) % 0.39/0.78 (define @t370 () (@list @t282)) % 0.39/0.78 (define @t371 () (forall @t370 @t368)) % 0.39/0.78 (define @t372 () (forall @t370 @t367)) % 0.39/0.78 (define @t373 () (or @t287 @t286 @t372)) % 0.39/0.78 (define @t374 () (= tptp.init @t99)) % 0.39/0.78 (define @t375 () (not @t100)) % 0.39/0.78 (define @t376 () (not @t101)) % 0.39/0.78 (define @t377 () (or @t376 @t375 @t374)) % 0.39/0.78 (define @t378 () (forall @t104 @t377)) % 0.39/0.78 (define @t379 () (or @t287 @t286 @t378)) % 0.39/0.78 (define @t380 () (or @t308 @t307 @t306)) % 0.39/0.78 (define @t381 () (or @t310 @t309 @t380)) % 0.39/0.78 (define @t382 () (forall @t312 @t381)) % 0.39/0.78 (define @t383 () (@list @t305)) % 0.39/0.78 (define @t384 () (forall @t383 @t381)) % 0.39/0.78 (define @t385 () (forall @t383 @t380)) % 0.39/0.78 (define @t386 () (or @t310 @t309 @t385)) % 0.39/0.78 (define @t387 () (= tptp.init @t141)) % 0.39/0.78 (define @t388 () (not @t142)) % 0.39/0.78 (define @t389 () (not @t143)) % 0.39/0.78 (define @t390 () (or @t389 @t388 @t387)) % 0.39/0.78 (define @t391 () (forall @t146 @t390)) % 0.39/0.78 (define @t392 () (or @t310 @t309 @t391)) % 0.39/0.78 (define @t393 () (or @t330 @t329 @t328)) % 0.39/0.78 (define @t394 () (or @t332 @t331 @t393)) % 0.39/0.78 (define @t395 () (forall @t334 @t394)) % 0.39/0.78 (define @t396 () (@list @t327)) % 0.39/0.78 (define @t397 () (forall @t396 @t394)) % 0.39/0.78 (define @t398 () (forall @t396 @t393)) % 0.39/0.78 (define @t399 () (or @t332 @t331 @t398)) % 0.39/0.78 (define @t400 () (= tptp.init @t173)) % 0.39/0.78 (define @t401 () (not @t174)) % 0.39/0.78 (define @t402 () (not @t32)) % 0.39/0.78 (define @t403 () (or @t402 @t401 @t400)) % 0.39/0.78 (define @t404 () (forall @t177 @t403)) % 0.39/0.78 (define @t405 () (or @t332 @t331 @t404)) % 0.39/0.78 (define @t406 () (or @t351 @t350 @t349)) % 0.39/0.78 (define @t407 () (or @t353 @t352 @t406)) % 0.39/0.78 (define @t408 () (forall @t355 @t407)) % 0.39/0.78 (define @t409 () (@list @t348)) % 0.39/0.78 (define @t410 () (forall @t409 @t407)) % 0.39/0.78 (define @t411 () (forall @t409 @t406)) % 0.39/0.78 (define @t412 () (or @t353 @t352 @t411)) % 0.39/0.78 (define @t413 () (= tptp.init @t203)) % 0.39/0.78 (define @t414 () (not @t204)) % 0.39/0.78 (define @t415 () (not @t205)) % 0.39/0.78 (define @t416 () (or @t415 @t414 @t413)) % 0.39/0.78 (define @t417 () (forall @t208 @t416)) % 0.39/0.78 (define @t418 () (or @t353 @t352 @t417)) % 0.39/0.78 (define @t419 () (= tptp.init @t231)) % 0.39/0.78 (define @t420 () (not @t232)) % 0.39/0.78 (define @t421 () (not @t233)) % 0.39/0.78 (define @t422 () (or @t421 @t420 @t419)) % 0.39/0.78 (define @t423 () (= tptp.init @t238)) % 0.39/0.78 (define @t424 () (not @t239)) % 0.39/0.78 (define @t425 () (not @t240)) % 0.39/0.78 (define @t426 () (or @t425 @t424 @t423)) % 0.39/0.78 (define @t427 () (@var "BOUND_VARIABLE_8570" $$unsorted)) % 0.39/0.78 (define @t428 () (= tptp.init (tptp.a_select3 tptp.simplex7_init @t427 @t28))) % 0.39/0.78 (define @t429 () (not (tptp.leq @t427 tptp.n3))) % 0.39/0.78 (define @t430 () (not (tptp.leq tptp.n0 @t427))) % 0.39/0.78 (define @t431 () (not @t252)) % 0.39/0.78 (define @t432 () (not @t253)) % 0.39/0.78 (define @t433 () (or @t432 @t431 @t430 @t429 @t428)) % 0.39/0.78 (define @t434 () (or @t430 @t429 @t428)) % 0.39/0.78 (define @t435 () (or @t432 @t431 @t434)) % 0.39/0.78 (define @t436 () (@list @t28 @t427)) % 0.39/0.78 (define @t437 () (forall @t436 @t435)) % 0.39/0.78 (define @t438 () (@list @t427)) % 0.39/0.78 (define @t439 () (forall @t438 @t435)) % 0.39/0.78 (define @t440 () (forall @t438 @t434)) % 0.39/0.78 (define @t441 () (or @t432 @t431 @t440)) % 0.39/0.78 (define @t442 () (= tptp.init @t245)) % 0.39/0.78 (define @t443 () (not @t246)) % 0.39/0.78 (define @t444 () (not @t247)) % 0.39/0.78 (define @t445 () (or @t444 @t443 @t442)) % 0.39/0.78 (define @t446 () (forall @t250 @t445)) % 0.39/0.78 (define @t447 () (or @t432 @t431 @t446)) % 0.39/0.78 (define @t448 () (@list tptp.n0 tptp.pv1388)) % 0.39/0.78 (define @t449 () (@list @t267 tptp.pv1388)) % 0.39/0.78 (define @t450 () (tptp.leq @t268 tptp.pv1388)) % 0.39/0.78 (define @t451 () (tptp.gt tptp.pv1388 @t267)) % 0.39/0.78 (define @t452 () (not @t450)) % 0.39/0.78 (define @t453 () (or @t452 @t451)) % 0.39/0.78 (define @t454 () (@list false false)) % 0.39/0.78 (define @t455 () (tptp.leq @t267 tptp.pv1388)) % 0.39/0.78 (define @t456 () (not @t451)) % 0.39/0.78 (define @t457 () (or @t456 @t455)) % 0.39/0.78 (define @t458 () (tptp.gt tptp.pv1388 tptp.n0)) % 0.39/0.78 (define @t459 () (not @t455)) % 0.39/0.78 (define @t460 () (or @t459 @t458)) % 0.39/0.78 (define @t461 () (not @t458)) % 0.39/0.78 (define @t462 () (or @t461 @t115)) % 0.39/0.78 (define @t463 () (not @t112)) % 0.39/0.78 (define @t464 () (not @t115)) % 0.39/0.78 (define @t465 () (or @t464 @t463 @t359)) % 0.39/0.78 (define @t466 () (@list false false false)) % 0.39/0.78 (define @t467 () (not @t154)) % 0.39/0.78 (define @t468 () (not @t155)) % 0.39/0.78 (define @t469 () (or @t468 @t467 @t366)) % 0.39/0.78 (define @t470 () (forall @t236 @t422)) % 0.39/0.78 (define @t471 () (@list @t57)) % 0.39/0.78 (define @t472 () (not @t470)) % 0.39/0.78 (define @t473 () (@list false)) % 0.39/0.78 (define @t474 () (@list @t470)) % 0.39/0.78 (define @t475 () (forall @t243 @t426)) % 0.39/0.78 (define @t476 () (@list @t14)) % 0.39/0.78 (define @t477 () (not @t475)) % 0.39/0.78 (define @t478 () (@list @t475)) % 0.39/0.78 (define @t479 () (forall @t436 @t433)) % 0.39/0.78 (define @t480 () (@list @t427 @t28)) % 0.39/0.78 (define @t481 () (not @t479)) % 0.39/0.78 (define @t482 () (@list @t479)) % 0.39/0.78 (define @t483 () (not @t271)) % 0.39/0.78 (define @t484 () (not @t113)) % 0.39/0.78 (define @t485 () (not @t114)) % 0.39/0.78 (define @t486 () (not @t116)) % 0.39/0.78 (define @t487 () (not @t117)) % 0.39/0.78 (define @t488 () (not @t291)) % 0.39/0.78 (define @t489 () (not @t292)) % 0.39/0.78 (define @t490 () (not @t357)) % 0.39/0.78 (define @t491 () (not @t314)) % 0.39/0.78 (define @t492 () (or @t487 @t485 @t360)) % 0.39/0.78 (define @t493 () (not @t359)) % 0.39/0.78 (define @t494 () (or @t486 @t484 @t363)) % 0.39/0.78 (assume @p1 (forall @t6 (or @t5 @t4 @t3))) % 0.39/0.78 (assume @p2 (forall @t8 (=> (and @t5 (tptp.gt @t1 @t7)) (tptp.gt @t2 @t7)))) % 0.39/0.78 (assume @p3 (forall @t9 (not (tptp.gt @t2 @t2)))) % 0.39/0.78 (assume @p4 (forall @t9 (tptp.leq @t2 @t2))) % 0.39/0.78 (assume @p5 (forall @t8 (=> (and @t10 (tptp.leq @t1 @t7)) (tptp.leq @t2 @t7)))) % 0.39/0.78 (assume @p6 (forall @t6 (= (tptp.lt @t2 @t1) @t4))) % 0.39/0.78 (assume @p7 (forall @t6 (= (tptp.geq @t2 @t1) (tptp.leq @t1 @t2)))) % 0.39/0.78 (assume @p8 @t11) % 0.39/0.78 (assume @p9 (forall @t6 (=> (and @t10 (not @t3)) @t4))) % 0.39/0.78 (assume @p10 (forall @t6 (= (tptp.leq @t2 (tptp.pred @t1)) @t4))) % 0.39/0.78 (assume @p11 (forall @t9 (tptp.gt @t12 @t2))) % 0.39/0.78 (assume @p12 (forall @t6 (=> @t10 (tptp.leq @t2 @t13)))) % 0.39/0.78 (assume @p13 (forall @t6 (= @t10 (tptp.gt @t13 @t2)))) % 0.39/0.78 (assume @p14 (forall @t17 (=> @t16 (tptp.leq @t15 @t2)))) % 0.39/0.78 (assume @p15 (forall @t17 (=> @t16 (tptp.leq tptp.n0 @t15)))) % 0.39/0.78 (assume @p16 (forall (@list @t19 @t21 @t20 @t18) (=> (and (tptp.leq @t21 @t19) @t22) (= (tptp.a_select2 (tptp.tptp_const_array1 (tptp.dim @t21 @t20) @t18) @t19) @t18)))) % 0.39/0.78 (assume @p17 (forall (@list @t19 @t27 @t26 @t23 @t25 @t24 @t18) (=> (and (tptp.leq @t27 @t19) (tptp.leq @t19 @t26) (tptp.leq @t25 @t23) (tptp.leq @t23 @t24)) (= (tptp.a_select3 (tptp.tptp_const_array2 (tptp.dim @t27 @t26) (tptp.dim @t25 @t24) @t18) @t19 @t23) @t18)))) % 0.39/0.78 (assume @p18 (forall @t38 (=> @t37 (forall @t36 (=> @t35 (= (tptp.a_select3 @t29 @t19 @t23) (tptp.a_select3 @t29 @t23 @t19))))))) % 0.39/0.78 (assume @p19 (forall @t38 (=> @t37 (forall @t36 (=> @t35 (= (tptp.a_select3 @t39 @t19 @t23) (tptp.a_select3 @t39 @t23 @t19))))))) % 0.39/0.78 (assume @p20 (forall @t38 (=> @t37 (forall (@list @t19 @t23 @t41 @t40) (=> (and @t34 @t33 @t32 @t31 @t43 (tptp.leq @t41 @t30)) (= (tptp.a_select3 @t42 @t19 @t23) (tptp.a_select3 @t42 @t23 @t19))))))) % 0.39/0.78 (assume @p21 (forall @t49 (=> @t48 (forall @t36 (=> @t35 (= (tptp.a_select3 @t45 @t19 @t23) (tptp.a_select3 @t45 @t23 @t19))))))) % 0.39/0.78 (assume @p22 (forall @t49 (=> @t48 (forall @t36 (=> @t35 (= (tptp.a_select3 @t50 @t19 @t23) (tptp.a_select3 @t50 @t23 @t19))))))) % 0.39/0.78 (assume @p23 (forall @t49 (=> @t47 @t52))) % 0.39/0.78 (assume @p24 (forall (@list @t28 @t44 @t30 @t53) (=> (forall @t36 (=> @t54 @t46)) @t52))) % 0.39/0.78 (assume @p25 (forall (@list @t28 @t44 @t14 @t57 @t55 @t56 @t30 @t53) (=> (and (forall @t36 (=> @t54 (= (tptp.a_select3 @t57 @t19 @t23) (tptp.a_select3 @t57 @t23 @t19)))) @t37 (forall @t36 (=> @t35 (= (tptp.a_select3 @t56 @t19 @t23) (tptp.a_select3 @t56 @t23 @t19))))) (forall @t36 (=> @t35 (= (tptp.a_select3 @t58 @t19 @t23) (tptp.a_select3 @t58 @t23 @t19))))))) % 0.39/0.78 (assume @p26 (forall @t61 (= @t60 tptp.n0))) % 0.39/0.78 (assume @p27 (forall @t61 (= tptp.tptp_float_0_0 @t60))) % 0.39/0.78 (assume @p28 (= (tptp.succ tptp.tptp_minus_1) tptp.n0)) % 0.39/0.78 (assume @p29 (forall @t9 (= (tptp.plus @t2 tptp.n1) @t12))) % 0.39/0.78 (assume @p30 (forall @t9 (= (tptp.plus tptp.n1 @t2) @t12))) % 0.39/0.78 (assume @p31 (forall @t9 (= (tptp.plus @t2 tptp.n2) @t62))) % 0.39/0.78 (assume @p32 (forall @t9 (= (tptp.plus tptp.n2 @t2) @t62))) % 0.39/0.78 (assume @p33 (forall @t9 (= (tptp.plus @t2 tptp.n3) @t63))) % 0.39/0.78 (assume @p34 (forall @t9 (= (tptp.plus tptp.n3 @t2) @t63))) % 0.39/0.78 (assume @p35 (forall @t9 (= (tptp.plus @t2 tptp.n4) @t64))) % 0.39/0.78 (assume @p36 (forall @t9 (= (tptp.plus tptp.n4 @t2) @t64))) % 0.39/0.78 (assume @p37 (forall @t9 (= (tptp.plus @t2 tptp.n5) @t65))) % 0.39/0.78 (assume @p38 (forall @t9 (= (tptp.plus tptp.n5 @t2) @t65))) % 0.39/0.78 (assume @p39 (forall @t9 (= (tptp.minus @t2 tptp.n1) @t66))) % 0.39/0.78 (assume @p40 (forall @t9 (= (tptp.pred @t12) @t2))) % 0.39/0.78 (assume @p41 (forall @t9 (= (tptp.succ @t66) @t2))) % 0.39/0.78 (assume @p42 (forall @t6 (= (tptp.leq @t12 @t13) @t10))) % 0.39/0.78 (assume @p43 @t68) % 0.39/0.78 (assume @p44 (forall @t6 (=> (tptp.leq (tptp.minus @t2 @t1) @t2) (tptp.leq tptp.n0 @t1)))) % 0.39/0.78 (assume @p45 (forall (@list @t2 @t20 @t69 @t40) (= (tptp.a_select3 @t70 @t20 @t69) @t40))) % 0.39/0.78 (assume @p46 (forall (@list @t19 @t23 @t20 @t69 @t2 @t40 @t71) (=> (and @t72 (= @t23 @t69) (= (tptp.a_select3 @t2 @t20 @t69) @t40)) (= (tptp.a_select3 (tptp.tptp_update3 @t2 @t19 @t23 @t71) @t20 @t69) @t40)))) % 0.39/0.78 (assume @p47 (forall (@list @t19 @t23 @t20 @t69 @t2 @t40) (=> (and (forall (@list @t74 @t73) (=> (and @t76 (tptp.leq tptp.n0 @t73) @t75 (tptp.leq @t73 @t69)) (= (tptp.a_select3 @t2 @t74 @t73) @t40))) @t34 @t22 @t32 (tptp.leq @t23 @t69)) (= (tptp.a_select3 @t70 @t19 @t23) @t40)))) % 0.39/0.78 (assume @p48 (forall (@list @t2 @t20 @t40) (= (tptp.a_select2 @t77 @t20) @t40))) % 0.39/0.78 (assume @p49 (forall (@list @t19 @t20 @t2 @t40 @t71) (=> (and @t72 (= (tptp.a_select2 @t2 @t20) @t40)) (= (tptp.a_select2 (tptp.tptp_update2 @t2 @t19 @t71) @t20) @t40)))) % 0.39/0.78 (assume @p50 (forall (@list @t19 @t20 @t2 @t40) (=> (and (forall (@list @t74) (=> (and @t76 @t75) (= (tptp.a_select2 @t2 @t74) @t40))) @t34 @t22) (= (tptp.a_select2 @t77 @t19) @t40)))) % 0.39/0.78 (assume @p51 tptp.true) % 0.39/0.78 (assume @p52 (not (= tptp.def tptp.use))) % 0.39/0.78 (assume @p53 @t261) % 0.39/0.78 (assume @p54 (tptp.gt tptp.n5 tptp.n4)) % 0.39/0.78 (assume @p55 (tptp.gt tptp.n4 tptp.tptp_minus_1)) % 0.39/0.78 (assume @p56 (tptp.gt tptp.n5 tptp.tptp_minus_1)) % 0.39/0.78 (assume @p57 (tptp.gt tptp.n0 tptp.tptp_minus_1)) % 0.39/0.78 (assume @p58 (tptp.gt tptp.n1 tptp.tptp_minus_1)) % 0.39/0.78 (assume @p59 (tptp.gt tptp.n2 tptp.tptp_minus_1)) % 0.39/0.78 (assume @p60 (tptp.gt tptp.n3 tptp.tptp_minus_1)) % 0.39/0.78 (assume @p61 (tptp.gt tptp.n4 tptp.n0)) % 0.39/0.78 (assume @p62 (tptp.gt tptp.n5 tptp.n0)) % 0.39/0.78 (assume @p63 (tptp.gt tptp.n1 tptp.n0)) % 0.39/0.78 (assume @p64 (tptp.gt tptp.n2 tptp.n0)) % 0.39/0.78 (assume @p65 (tptp.gt tptp.n3 tptp.n0)) % 0.39/0.78 (assume @p66 (tptp.gt tptp.n4 tptp.n1)) % 0.39/0.78 (assume @p67 (tptp.gt tptp.n5 tptp.n1)) % 0.39/0.78 (assume @p68 (tptp.gt tptp.n2 tptp.n1)) % 0.39/0.78 (assume @p69 (tptp.gt tptp.n3 tptp.n1)) % 0.39/0.78 (assume @p70 (tptp.gt tptp.n4 tptp.n2)) % 0.39/0.78 (assume @p71 (tptp.gt tptp.n5 tptp.n2)) % 0.39/0.78 (assume @p72 (tptp.gt tptp.n3 tptp.n2)) % 0.39/0.78 (assume @p73 (tptp.gt tptp.n4 tptp.n3)) % 0.39/0.78 (assume @p74 (tptp.gt tptp.n5 tptp.n3)) % 0.39/0.78 (assume @p75 (forall @t9 (=> (and @t16 (tptp.leq @t2 tptp.n4)) (or @t266 @t265 @t264 @t263 @t262)))) % 0.39/0.78 (assume @p76 (forall @t9 (=> (and @t16 (tptp.leq @t2 tptp.n5)) (or @t266 @t265 @t264 @t263 @t262 (= @t2 tptp.n5))))) % 0.39/0.78 (assume @p77 (forall @t9 (=> (and @t16 (tptp.leq @t2 tptp.n0)) @t266))) % 0.39/0.78 (assume @p78 (forall @t9 (=> (and @t16 (tptp.leq @t2 tptp.n1)) (or @t266 @t265)))) % 0.39/0.78 (assume @p79 (forall @t9 (=> (and @t16 (tptp.leq @t2 tptp.n2)) (or @t266 @t265 @t264)))) % 0.39/0.78 (assume @p80 (forall @t9 (=> (and @t16 (tptp.leq @t2 tptp.n3)) (or @t266 @t265 @t264 @t263)))) % 0.39/0.78 (assume @p81 (= @t270 tptp.n4)) % 0.39/0.78 (assume @p82 (= (tptp.succ @t270) tptp.n5)) % 0.39/0.78 (assume @p83 (= @t267 tptp.n1)) % 0.39/0.78 (assume @p84 (= @t268 tptp.n2)) % 0.39/0.78 (assume @p85 (= @t269 tptp.n3)) % 0.39/0.78 (assume @p86 true) % 0.39/0.78 (step @p87 :rule aci_norm :args ((= (and true @t314 @t366 @t359 @t365 @t294) (and @t314 @t366 @t359 @t365 @t294)))) % 0.39/0.78 (step @p88 :rule aci_norm :args ((= (and true @t292 @t291 @t117 @t116 @t115 @t114 @t113 @t112 @t290 @t281 @t276 @t271) @t293))) % 0.39/0.78 (step @p89 :rule eq-symm :args (tptp.pvar1402_init tptp.init)) % 0.39/0.78 (step @p90 :rule eq-symm :args (tptp.pvar1401_init tptp.init)) % 0.39/0.78 (step @p91 :rule eq-symm :args (tptp.pvar1400_init tptp.init)) % 0.39/0.78 (step @p92 :rule nary_cong :premises (@p91 @p90 @p89) :args (@t78)) % 0.39/0.78 (step @p93 :rule refl :args (@t79)) % 0.39/0.78 (step @p94 :rule cong :premises (@p93 @p92) :args (@t80)) % 0.39/0.78 (step @p95 :rule aci_norm :args ((= (or (or @t274 @t273) @t272) @t275))) % 0.39/0.78 (step @p96 :rule refl :args (@t272)) % 0.39/0.78 (step @p97 :rule bool-and-de-morgan :args (@t84 @t83 true)) % 0.39/0.78 (step @p98 :rule nary_cong :premises (@p97 @p96) :args ((or (not @t85) @t272))) % 0.39/0.78 (step @p99 :rule trans :premises (@p98 @p95)) % 0.39/0.78 (step @p100 :rule bool-impl-elim :args (@t85 @t272)) % 0.39/0.78 (step @p101 :rule trans :premises (@p100 @p99)) % 0.39/0.78 (step @p102 :rule cong :premises (@p101) :args ((forall @t87 (=> @t85 @t272)))) % 0.39/0.78 (step @p103 :rule eq-symm :args (@t82 tptp.init)) % 0.39/0.78 (step @p104 :rule refl :args (@t85)) % 0.39/0.78 (step @p105 :rule cong :premises (@p104 @p103) :args (@t86)) % 0.39/0.78 (step @p106 :rule cong :premises (@p105) :args (@t88)) % 0.39/0.78 (step @p107 :rule trans :premises (@p106 @p102)) % 0.39/0.78 (step @p108 :rule aci_norm :args ((= (or (or @t279 @t278) @t277) @t280))) % 0.39/0.78 (step @p109 :rule refl :args (@t277)) % 0.39/0.78 (step @p110 :rule bool-and-de-morgan :args (@t92 @t91 true)) % 0.39/0.78 (step @p111 :rule nary_cong :premises (@p110 @p109) :args ((or (not @t93) @t277))) % 0.39/0.78 (step @p112 :rule trans :premises (@p111 @p108)) % 0.39/0.78 (step @p113 :rule bool-impl-elim :args (@t93 @t277)) % 0.39/0.78 (step @p114 :rule trans :premises (@p113 @p112)) % 0.39/0.78 (step @p115 :rule cong :premises (@p114) :args ((forall @t95 (=> @t93 @t277)))) % 0.39/0.78 (step @p116 :rule eq-symm :args (@t90 tptp.init)) % 0.39/0.78 (step @p117 :rule refl :args (@t93)) % 0.39/0.78 (step @p118 :rule cong :premises (@p117 @p116) :args (@t94)) % 0.39/0.78 (step @p119 :rule cong :premises (@p118) :args (@t96)) % 0.39/0.78 (step @p120 :rule trans :premises (@p119 @p115)) % 0.39/0.78 (step @p121 :rule aci_norm :args ((= @t368 @t288))) % 0.39/0.78 (step @p122 :rule cong :premises (@p121) :args (@t369)) % 0.39/0.78 (step @p123 :rule quant-merge-prenex :args ((= (forall @t110 @t371) @t369))) % 0.39/0.78 (step @p124 :rule alpha_equiv :args (@t372 (@list @t282) (@list @t98))) % 0.39/0.78 (step @p125 :rule refl :args (@t286)) % 0.39/0.78 (step @p126 :rule refl :args (@t287)) % 0.39/0.78 (step @p127 :rule nary_cong :premises (@p126 @p125 @p124) :args (@t373)) % 0.39/0.78 (step @p128 :rule quant-miniscope-or :args ((= @t371 @t373))) % 0.39/0.78 (step @p129 :rule trans :premises (@p128 @p127)) % 0.39/0.78 (step @p130 :rule symm :premises (@p129)) % 0.39/0.78 (step @p131 :rule cong :premises (@p130) :args ((forall @t110 @t379))) % 0.39/0.78 (step @p132 :rule trans :premises (@p131 @p123)) % 0.39/0.78 (step @p133 :rule trans :premises (@p132 @p122)) % 0.39/0.78 (step @p134 :rule aci_norm :args ((= (or (or @t287 @t286) @t378) @t379))) % 0.39/0.78 (step @p135 :rule refl :args (@t378)) % 0.39/0.78 (step @p136 :rule bool-and-de-morgan :args (@t107 @t106 true)) % 0.39/0.78 (step @p137 :rule nary_cong :premises (@p136 @p135) :args ((or (not @t108) @t378))) % 0.39/0.78 (step @p138 :rule trans :premises (@p137 @p134)) % 0.39/0.78 (step @p139 :rule bool-impl-elim :args (@t108 @t378)) % 0.39/0.78 (step @p140 :rule trans :premises (@p139 @p138)) % 0.39/0.78 (step @p141 :rule cong :premises (@p140) :args ((forall @t110 (=> @t108 @t378)))) % 0.39/0.78 (step @p142 :rule trans :premises (@p141 @p133)) % 0.39/0.78 (step @p143 :rule aci_norm :args ((= (or (or @t376 @t375) @t374) @t377))) % 0.39/0.78 (step @p144 :rule refl :args (@t374)) % 0.39/0.78 (step @p145 :rule bool-and-de-morgan :args (@t101 @t100 true)) % 0.39/0.78 (step @p146 :rule nary_cong :premises (@p145 @p144) :args ((or (not @t102) @t374))) % 0.39/0.78 (step @p147 :rule trans :premises (@p146 @p143)) % 0.39/0.78 (step @p148 :rule bool-impl-elim :args (@t102 @t374)) % 0.39/0.78 (step @p149 :rule trans :premises (@p148 @p147)) % 0.39/0.78 (step @p150 :rule cong :premises (@p149) :args ((forall @t104 (=> @t102 @t374)))) % 0.39/0.78 (step @p151 :rule eq-symm :args (@t99 tptp.init)) % 0.39/0.78 (step @p152 :rule refl :args (@t102)) % 0.39/0.78 (step @p153 :rule cong :premises (@p152 @p151) :args (@t103)) % 0.39/0.78 (step @p154 :rule cong :premises (@p153) :args (@t105)) % 0.39/0.78 (step @p155 :rule trans :premises (@p154 @p150)) % 0.39/0.78 (step @p156 :rule refl :args (@t108)) % 0.39/0.78 (step @p157 :rule cong :premises (@p156 @p155) :args (@t109)) % 0.39/0.78 (step @p158 :rule cong :premises (@p157) :args (@t111)) % 0.39/0.78 (step @p159 :rule trans :premises (@p158 @p142)) % 0.39/0.78 (step @p160 :rule refl :args (@t112)) % 0.39/0.78 (step @p161 :rule refl :args (@t113)) % 0.39/0.78 (step @p162 :rule refl :args (@t114)) % 0.39/0.78 (step @p163 :rule refl :args (@t115)) % 0.39/0.78 (step @p164 :rule refl :args (@t116)) % 0.39/0.78 (step @p165 :rule refl :args (@t117)) % 0.39/0.78 (step @p166 :rule eq-symm :args (tptp.s_worst7_init tptp.init)) % 0.39/0.78 (step @p167 :rule eq-symm :args (tptp.s_sworst7_init tptp.init)) % 0.39/0.78 (step @p168 :rule eq-refl :args (tptp.init)) % 0.39/0.78 (step @p169 :rule nary_cong :premises (@p168 @p167 @p166 @p165 @p164 @p163 @p162 @p161 @p160 @p159 @p120 @p107 @p94) :args (@t121)) % 0.39/0.78 (step @p170 :rule trans :premises (@p169 @p88)) % 0.39/0.78 (step @p171 :rule refl :args (@t123)) % 0.39/0.78 (step @p172 :rule cong :premises (@p171 @p170) :args (@t124)) % 0.39/0.78 (step @p173 :rule aci_norm :args ((= (and true @t291 @t363 @t359 @t362 @t316) @t364))) % 0.39/0.78 (step @p174 :rule aci_norm :args ((= (and true @t314 @t291 @t155 @t116 @t115 @t154 @t113 @t112 @t313 @t304 @t299 @t271) @t315))) % 0.39/0.78 (step @p175 :rule aci_norm :args ((= (or (or @t297 @t296) @t295) @t298))) % 0.39/0.78 (step @p176 :rule refl :args (@t295)) % 0.39/0.78 (step @p177 :rule bool-and-de-morgan :args (@t128 @t127 true)) % 0.39/0.78 (step @p178 :rule nary_cong :premises (@p177 @p176) :args ((or (not @t129) @t295))) % 0.39/0.78 (step @p179 :rule trans :premises (@p178 @p175)) % 0.39/0.78 (step @p180 :rule bool-impl-elim :args (@t129 @t295)) % 0.39/0.78 (step @p181 :rule trans :premises (@p180 @p179)) % 0.39/0.78 (step @p182 :rule cong :premises (@p181) :args ((forall @t131 (=> @t129 @t295)))) % 0.39/0.78 (step @p183 :rule eq-symm :args (@t126 tptp.init)) % 0.39/0.78 (step @p184 :rule refl :args (@t129)) % 0.39/0.78 (step @p185 :rule cong :premises (@p184 @p183) :args (@t130)) % 0.39/0.78 (step @p186 :rule cong :premises (@p185) :args (@t132)) % 0.39/0.78 (step @p187 :rule trans :premises (@p186 @p182)) % 0.39/0.78 (step @p188 :rule aci_norm :args ((= (or (or @t302 @t301) @t300) @t303))) % 0.39/0.78 (step @p189 :rule refl :args (@t300)) % 0.39/0.78 (step @p190 :rule bool-and-de-morgan :args (@t136 @t135 true)) % 0.39/0.78 (step @p191 :rule nary_cong :premises (@p190 @p189) :args ((or (not @t137) @t300))) % 0.39/0.78 (step @p192 :rule trans :premises (@p191 @p188)) % 0.39/0.78 (step @p193 :rule bool-impl-elim :args (@t137 @t300)) % 0.39/0.78 (step @p194 :rule trans :premises (@p193 @p192)) % 0.39/0.78 (step @p195 :rule cong :premises (@p194) :args ((forall @t139 (=> @t137 @t300)))) % 0.39/0.78 (step @p196 :rule eq-symm :args (@t134 tptp.init)) % 0.39/0.78 (step @p197 :rule refl :args (@t137)) % 0.39/0.78 (step @p198 :rule cong :premises (@p197 @p196) :args (@t138)) % 0.39/0.78 (step @p199 :rule cong :premises (@p198) :args (@t140)) % 0.39/0.78 (step @p200 :rule trans :premises (@p199 @p195)) % 0.39/0.78 (step @p201 :rule aci_norm :args ((= @t381 @t311))) % 0.39/0.78 (step @p202 :rule cong :premises (@p201) :args (@t382)) % 0.39/0.78 (step @p203 :rule quant-merge-prenex :args ((= (forall @t152 @t384) @t382))) % 0.39/0.78 (step @p204 :rule alpha_equiv :args (@t385 (@list @t305) (@list @t30))) % 0.39/0.78 (step @p205 :rule refl :args (@t309)) % 0.39/0.78 (step @p206 :rule refl :args (@t310)) % 0.39/0.78 (step @p207 :rule nary_cong :premises (@p206 @p205 @p204) :args (@t386)) % 0.39/0.78 (step @p208 :rule quant-miniscope-or :args ((= @t384 @t386))) % 0.39/0.78 (step @p209 :rule trans :premises (@p208 @p207)) % 0.39/0.78 (step @p210 :rule symm :premises (@p209)) % 0.39/0.78 (step @p211 :rule cong :premises (@p210) :args ((forall @t152 @t392))) % 0.39/0.78 (step @p212 :rule trans :premises (@p211 @p203)) % 0.39/0.78 (step @p213 :rule trans :premises (@p212 @p202)) % 0.39/0.78 (step @p214 :rule aci_norm :args ((= (or (or @t310 @t309) @t391) @t392))) % 0.39/0.78 (step @p215 :rule refl :args (@t391)) % 0.39/0.78 (step @p216 :rule bool-and-de-morgan :args (@t149 @t148 true)) % 0.39/0.78 (step @p217 :rule nary_cong :premises (@p216 @p215) :args ((or (not @t150) @t391))) % 0.39/0.78 (step @p218 :rule trans :premises (@p217 @p214)) % 0.39/0.78 (step @p219 :rule bool-impl-elim :args (@t150 @t391)) % 0.39/0.78 (step @p220 :rule trans :premises (@p219 @p218)) % 0.39/0.78 (step @p221 :rule cong :premises (@p220) :args ((forall @t152 (=> @t150 @t391)))) % 0.39/0.78 (step @p222 :rule trans :premises (@p221 @p213)) % 0.39/0.78 (step @p223 :rule aci_norm :args ((= (or (or @t389 @t388) @t387) @t390))) % 0.39/0.78 (step @p224 :rule refl :args (@t387)) % 0.39/0.78 (step @p225 :rule bool-and-de-morgan :args (@t143 @t142 true)) % 0.39/0.78 (step @p226 :rule nary_cong :premises (@p225 @p224) :args ((or (not @t144) @t387))) % 0.39/0.78 (step @p227 :rule trans :premises (@p226 @p223)) % 0.39/0.78 (step @p228 :rule bool-impl-elim :args (@t144 @t387)) % 0.39/0.78 (step @p229 :rule trans :premises (@p228 @p227)) % 0.39/0.78 (step @p230 :rule cong :premises (@p229) :args ((forall @t146 (=> @t144 @t387)))) % 0.39/0.78 (step @p231 :rule eq-symm :args (@t141 tptp.init)) % 0.39/0.78 (step @p232 :rule refl :args (@t144)) % 0.39/0.78 (step @p233 :rule cong :premises (@p232 @p231) :args (@t145)) % 0.39/0.78 (step @p234 :rule cong :premises (@p233) :args (@t147)) % 0.39/0.78 (step @p235 :rule trans :premises (@p234 @p230)) % 0.39/0.78 (step @p236 :rule refl :args (@t150)) % 0.39/0.78 (step @p237 :rule cong :premises (@p236 @p235) :args (@t151)) % 0.39/0.78 (step @p238 :rule cong :premises (@p237) :args (@t153)) % 0.39/0.78 (step @p239 :rule trans :premises (@p238 @p222)) % 0.39/0.78 (step @p240 :rule refl :args (@t154)) % 0.39/0.78 (step @p241 :rule refl :args (@t155)) % 0.39/0.78 (step @p242 :rule eq-symm :args (tptp.s_best7_init tptp.init)) % 0.39/0.78 (step @p243 :rule nary_cong :premises (@p168 @p242 @p166 @p241 @p164 @p163 @p240 @p161 @p160 @p239 @p200 @p187 @p94) :args (@t157)) % 0.39/0.78 (step @p244 :rule trans :premises (@p243 @p174)) % 0.39/0.78 (step @p245 :rule refl :args (@t158)) % 0.39/0.78 (step @p246 :rule cong :premises (@p245 @p244) :args (@t159)) % 0.39/0.78 (step @p247 :rule aci_norm :args ((= (and true @t292 @t360 @t359 @t358 @t337) @t361))) % 0.39/0.78 (step @p248 :rule aci_norm :args ((= (and true @t314 @t291 @t155 @t116 @t115 @t154 @t113 @t112 @t335 @t326 @t321 @t271) @t336))) % 0.39/0.78 (step @p249 :rule aci_norm :args ((= (or (or @t319 @t318) @t317) @t320))) % 0.39/0.78 (step @p250 :rule refl :args (@t317)) % 0.39/0.78 (step @p251 :rule bool-and-de-morgan :args (@t162 @t161 true)) % 0.39/0.78 (step @p252 :rule nary_cong :premises (@p251 @p250) :args ((or (not @t163) @t317))) % 0.39/0.78 (step @p253 :rule trans :premises (@p252 @p249)) % 0.39/0.78 (step @p254 :rule bool-impl-elim :args (@t163 @t317)) % 0.39/0.78 (step @p255 :rule trans :premises (@p254 @p253)) % 0.39/0.78 (step @p256 :rule cong :premises (@p255) :args ((forall @t165 (=> @t163 @t317)))) % 0.39/0.78 (step @p257 :rule eq-symm :args (@t160 tptp.init)) % 0.39/0.78 (step @p258 :rule refl :args (@t163)) % 0.39/0.78 (step @p259 :rule cong :premises (@p258 @p257) :args (@t164)) % 0.39/0.78 (step @p260 :rule cong :premises (@p259) :args (@t166)) % 0.39/0.78 (step @p261 :rule trans :premises (@p260 @p256)) % 0.39/0.78 (step @p262 :rule aci_norm :args ((= (or (or @t324 @t323) @t322) @t325))) % 0.39/0.78 (step @p263 :rule refl :args (@t322)) % 0.39/0.78 (step @p264 :rule bool-and-de-morgan :args (@t43 @t168 true)) % 0.39/0.78 (step @p265 :rule nary_cong :premises (@p264 @p263) :args ((or (not @t169) @t322))) % 0.39/0.78 (step @p266 :rule trans :premises (@p265 @p262)) % 0.39/0.78 (step @p267 :rule bool-impl-elim :args (@t169 @t322)) % 0.39/0.78 (step @p268 :rule trans :premises (@p267 @p266)) % 0.39/0.78 (step @p269 :rule cong :premises (@p268) :args ((forall @t171 (=> @t169 @t322)))) % 0.39/0.78 (step @p270 :rule eq-symm :args (@t167 tptp.init)) % 0.39/0.78 (step @p271 :rule refl :args (@t169)) % 0.39/0.78 (step @p272 :rule cong :premises (@p271 @p270) :args (@t170)) % 0.39/0.78 (step @p273 :rule cong :premises (@p272) :args (@t172)) % 0.39/0.78 (step @p274 :rule trans :premises (@p273 @p269)) % 0.39/0.78 (step @p275 :rule aci_norm :args ((= @t394 @t333))) % 0.39/0.78 (step @p276 :rule cong :premises (@p275) :args (@t395)) % 0.39/0.78 (step @p277 :rule quant-merge-prenex :args ((= (forall @t182 @t397) @t395))) % 0.39/0.78 (step @p278 :rule alpha_equiv :args (@t398 (@list @t327) (@list @t23))) % 0.39/0.78 (step @p279 :rule refl :args (@t331)) % 0.39/0.78 (step @p280 :rule refl :args (@t332)) % 0.39/0.78 (step @p281 :rule nary_cong :premises (@p280 @p279 @p278) :args (@t399)) % 0.39/0.78 (step @p282 :rule quant-miniscope-or :args ((= @t397 @t399))) % 0.39/0.78 (step @p283 :rule trans :premises (@p282 @p281)) % 0.39/0.78 (step @p284 :rule symm :premises (@p283)) % 0.39/0.78 (step @p285 :rule cong :premises (@p284) :args ((forall @t182 @t405))) % 0.39/0.78 (step @p286 :rule trans :premises (@p285 @p277)) % 0.39/0.78 (step @p287 :rule trans :premises (@p286 @p276)) % 0.39/0.78 (step @p288 :rule aci_norm :args ((= (or (or @t332 @t331) @t404) @t405))) % 0.39/0.78 (step @p289 :rule refl :args (@t404)) % 0.39/0.78 (step @p290 :rule bool-and-de-morgan :args (@t34 @t179 true)) % 0.39/0.78 (step @p291 :rule nary_cong :premises (@p290 @p289) :args ((or (not @t180) @t404))) % 0.39/0.78 (step @p292 :rule trans :premises (@p291 @p288)) % 0.39/0.78 (step @p293 :rule bool-impl-elim :args (@t180 @t404)) % 0.39/0.78 (step @p294 :rule trans :premises (@p293 @p292)) % 0.39/0.78 (step @p295 :rule cong :premises (@p294) :args ((forall @t182 (=> @t180 @t404)))) % 0.39/0.78 (step @p296 :rule trans :premises (@p295 @p287)) % 0.39/0.78 (step @p297 :rule aci_norm :args ((= (or (or @t402 @t401) @t400) @t403))) % 0.39/0.78 (step @p298 :rule refl :args (@t400)) % 0.39/0.78 (step @p299 :rule bool-and-de-morgan :args (@t32 @t174 true)) % 0.39/0.78 (step @p300 :rule nary_cong :premises (@p299 @p298) :args ((or (not @t175) @t400))) % 0.39/0.78 (step @p301 :rule trans :premises (@p300 @p297)) % 0.39/0.78 (step @p302 :rule bool-impl-elim :args (@t175 @t400)) % 0.39/0.78 (step @p303 :rule trans :premises (@p302 @p301)) % 0.39/0.78 (step @p304 :rule cong :premises (@p303) :args ((forall @t177 (=> @t175 @t400)))) % 0.39/0.78 (step @p305 :rule eq-symm :args (@t173 tptp.init)) % 0.39/0.78 (step @p306 :rule refl :args (@t175)) % 0.39/0.78 (step @p307 :rule cong :premises (@p306 @p305) :args (@t176)) % 0.39/0.78 (step @p308 :rule cong :premises (@p307) :args (@t178)) % 0.39/0.78 (step @p309 :rule trans :premises (@p308 @p304)) % 0.39/0.78 (step @p310 :rule refl :args (@t180)) % 0.39/0.78 (step @p311 :rule cong :premises (@p310 @p309) :args (@t181)) % 0.39/0.78 (step @p312 :rule cong :premises (@p311) :args (@t183)) % 0.39/0.78 (step @p313 :rule trans :premises (@p312 @p296)) % 0.39/0.78 (step @p314 :rule nary_cong :premises (@p168 @p242 @p166 @p241 @p164 @p163 @p240 @p161 @p160 @p313 @p274 @p261 @p94) :args (@t184)) % 0.39/0.78 (step @p315 :rule trans :premises (@p314 @p248)) % 0.39/0.78 (step @p316 :rule refl :args (@t185)) % 0.39/0.78 (step @p317 :rule cong :premises (@p316 @p315) :args (@t186)) % 0.39/0.78 (step @p318 :rule aci_norm :args ((= (or (or @t340 @t339) @t338) @t341))) % 0.39/0.78 (step @p319 :rule refl :args (@t338)) % 0.39/0.78 (step @p320 :rule bool-and-de-morgan :args (@t190 @t189 true)) % 0.39/0.78 (step @p321 :rule nary_cong :premises (@p320 @p319) :args ((or (not @t191) @t338))) % 0.39/0.78 (step @p322 :rule trans :premises (@p321 @p318)) % 0.39/0.78 (step @p323 :rule bool-impl-elim :args (@t191 @t338)) % 0.39/0.78 (step @p324 :rule trans :premises (@p323 @p322)) % 0.39/0.78 (step @p325 :rule cong :premises (@p324) :args ((forall @t193 (=> @t191 @t338)))) % 0.39/0.78 (step @p326 :rule eq-symm :args (@t188 tptp.init)) % 0.39/0.78 (step @p327 :rule refl :args (@t191)) % 0.39/0.78 (step @p328 :rule cong :premises (@p327 @p326) :args (@t192)) % 0.39/0.78 (step @p329 :rule cong :premises (@p328) :args (@t194)) % 0.39/0.78 (step @p330 :rule trans :premises (@p329 @p325)) % 0.39/0.78 (step @p331 :rule aci_norm :args ((= (or (or @t345 @t344) @t343) @t346))) % 0.39/0.78 (step @p332 :rule refl :args (@t343)) % 0.39/0.78 (step @p333 :rule bool-and-de-morgan :args (@t198 @t197 true)) % 0.39/0.78 (step @p334 :rule nary_cong :premises (@p333 @p332) :args ((or (not @t199) @t343))) % 0.39/0.78 (step @p335 :rule trans :premises (@p334 @p331)) % 0.39/0.78 (step @p336 :rule bool-impl-elim :args (@t199 @t343)) % 0.39/0.78 (step @p337 :rule trans :premises (@p336 @p335)) % 0.39/0.78 (step @p338 :rule cong :premises (@p337) :args ((forall @t201 (=> @t199 @t343)))) % 0.39/0.78 (step @p339 :rule eq-symm :args (@t196 tptp.init)) % 0.39/0.78 (step @p340 :rule refl :args (@t199)) % 0.39/0.78 (step @p341 :rule cong :premises (@p340 @p339) :args (@t200)) % 0.39/0.78 (step @p342 :rule cong :premises (@p341) :args (@t202)) % 0.39/0.78 (step @p343 :rule trans :premises (@p342 @p338)) % 0.39/0.78 (step @p344 :rule aci_norm :args ((= @t407 @t354))) % 0.39/0.78 (step @p345 :rule cong :premises (@p344) :args (@t408)) % 0.39/0.78 (step @p346 :rule quant-merge-prenex :args ((= (forall @t214 @t410) @t408))) % 0.39/0.78 (step @p347 :rule alpha_equiv :args (@t411 (@list @t348) (@list @t56))) % 0.39/0.78 (step @p348 :rule refl :args (@t352)) % 0.39/0.78 (step @p349 :rule refl :args (@t353)) % 0.39/0.78 (step @p350 :rule nary_cong :premises (@p349 @p348 @p347) :args (@t412)) % 0.39/0.78 (step @p351 :rule quant-miniscope-or :args ((= @t410 @t412))) % 0.39/0.78 (step @p352 :rule trans :premises (@p351 @p350)) % 0.39/0.78 (step @p353 :rule symm :premises (@p352)) % 0.39/0.78 (step @p354 :rule cong :premises (@p353) :args ((forall @t214 @t418))) % 0.39/0.78 (step @p355 :rule trans :premises (@p354 @p346)) % 0.39/0.78 (step @p356 :rule trans :premises (@p355 @p345)) % 0.39/0.78 (step @p357 :rule aci_norm :args ((= (or (or @t353 @t352) @t417) @t418))) % 0.39/0.78 (step @p358 :rule refl :args (@t417)) % 0.39/0.78 (step @p359 :rule bool-and-de-morgan :args (@t211 @t210 true)) % 0.39/0.78 (step @p360 :rule nary_cong :premises (@p359 @p358) :args ((or (not @t212) @t417))) % 0.39/0.78 (step @p361 :rule trans :premises (@p360 @p357)) % 0.39/0.78 (step @p362 :rule bool-impl-elim :args (@t212 @t417)) % 0.39/0.78 (step @p363 :rule trans :premises (@p362 @p361)) % 0.39/0.78 (step @p364 :rule cong :premises (@p363) :args ((forall @t214 (=> @t212 @t417)))) % 0.39/0.78 (step @p365 :rule trans :premises (@p364 @p356)) % 0.39/0.78 (step @p366 :rule aci_norm :args ((= (or (or @t415 @t414) @t413) @t416))) % 0.39/0.78 (step @p367 :rule refl :args (@t413)) % 0.39/0.78 (step @p368 :rule bool-and-de-morgan :args (@t205 @t204 true)) % 0.39/0.78 (step @p369 :rule nary_cong :premises (@p368 @p367) :args ((or (not @t206) @t413))) % 0.39/0.78 (step @p370 :rule trans :premises (@p369 @p366)) % 0.39/0.78 (step @p371 :rule bool-impl-elim :args (@t206 @t413)) % 0.39/0.78 (step @p372 :rule trans :premises (@p371 @p370)) % 0.39/0.78 (step @p373 :rule cong :premises (@p372) :args ((forall @t208 (=> @t206 @t413)))) % 0.39/0.78 (step @p374 :rule eq-symm :args (@t203 tptp.init)) % 0.39/0.78 (step @p375 :rule refl :args (@t206)) % 0.39/0.78 (step @p376 :rule cong :premises (@p375 @p374) :args (@t207)) % 0.39/0.78 (step @p377 :rule cong :premises (@p376) :args (@t209)) % 0.39/0.78 (step @p378 :rule trans :premises (@p377 @p373)) % 0.39/0.78 (step @p379 :rule refl :args (@t212)) % 0.39/0.78 (step @p380 :rule cong :premises (@p379 @p378) :args (@t213)) % 0.39/0.78 (step @p381 :rule cong :premises (@p380) :args (@t215)) % 0.39/0.78 (step @p382 :rule trans :premises (@p381 @p365)) % 0.39/0.78 (step @p383 :rule nary_cong :premises (@p242 @p167 @p166 @p241 @p165 @p164 @p240 @p162 @p161 @p382 @p343 @p330 @p94) :args (@t216)) % 0.39/0.78 (step @p384 :rule refl :args (@t217)) % 0.39/0.78 (step @p385 :rule cong :premises (@p384 @p383) :args (@t218)) % 0.39/0.78 (step @p386 :rule eq-symm :args (@t219 tptp.init)) % 0.39/0.78 (step @p387 :rule eq-symm :args (@t221 tptp.init)) % 0.39/0.78 (step @p388 :rule nary_cong :premises (@p168 @p167 @p387 @p386 @p385 @p317) :args (@t222)) % 0.39/0.78 (step @p389 :rule trans :premises (@p388 @p247)) % 0.39/0.78 (step @p390 :rule refl :args (@t223)) % 0.39/0.78 (step @p391 :rule cong :premises (@p390 @p389) :args (@t224)) % 0.39/0.78 (step @p392 :rule eq-symm :args (@t225 tptp.init)) % 0.39/0.78 (step @p393 :rule nary_cong :premises (@p168 @p166 @p392 @p386 @p391 @p246) :args (@t226)) % 0.39/0.78 (step @p394 :rule trans :premises (@p393 @p173)) % 0.39/0.78 (step @p395 :rule refl :args (@t227)) % 0.39/0.78 (step @p396 :rule cong :premises (@p395 @p394) :args (@t228)) % 0.39/0.78 (step @p397 :rule eq-symm :args (@t229 tptp.init)) % 0.39/0.78 (step @p398 :rule nary_cong :premises (@p168 @p242 @p397 @p386 @p396 @p172) :args (@t230)) % 0.39/0.78 (step @p399 :rule trans :premises (@p398 @p87)) % 0.39/0.78 (step @p400 :rule aci_norm :args ((= (or (or @t421 @t420) @t419) @t422))) % 0.39/0.78 (step @p401 :rule refl :args (@t419)) % 0.39/0.78 (step @p402 :rule bool-and-de-morgan :args (@t233 @t232 true)) % 0.39/0.78 (step @p403 :rule nary_cong :premises (@p402 @p401) :args ((or (not @t234) @t419))) % 0.39/0.78 (step @p404 :rule trans :premises (@p403 @p400)) % 0.39/0.78 (step @p405 :rule bool-impl-elim :args (@t234 @t419)) % 0.39/0.78 (step @p406 :rule trans :premises (@p405 @p404)) % 0.39/0.78 (step @p407 :rule cong :premises (@p406) :args ((forall @t236 (=> @t234 @t419)))) % 0.39/0.78 (step @p408 :rule eq-symm :args (@t231 tptp.init)) % 0.39/0.78 (step @p409 :rule refl :args (@t234)) % 0.39/0.78 (step @p410 :rule cong :premises (@p409 @p408) :args (@t235)) % 0.39/0.78 (step @p411 :rule cong :premises (@p410) :args (@t237)) % 0.39/0.78 (step @p412 :rule trans :premises (@p411 @p407)) % 0.39/0.78 (step @p413 :rule aci_norm :args ((= (or (or @t425 @t424) @t423) @t426))) % 0.39/0.78 (step @p414 :rule refl :args (@t423)) % 0.39/0.78 (step @p415 :rule bool-and-de-morgan :args (@t240 @t239 true)) % 0.39/0.78 (step @p416 :rule nary_cong :premises (@p415 @p414) :args ((or (not @t241) @t423))) % 0.39/0.78 (step @p417 :rule trans :premises (@p416 @p413)) % 0.39/0.78 (step @p418 :rule bool-impl-elim :args (@t241 @t423)) % 0.39/0.78 (step @p419 :rule trans :premises (@p418 @p417)) % 0.39/0.78 (step @p420 :rule cong :premises (@p419) :args ((forall @t243 (=> @t241 @t423)))) % 0.39/0.78 (step @p421 :rule eq-symm :args (@t238 tptp.init)) % 0.39/0.78 (step @p422 :rule refl :args (@t241)) % 0.39/0.78 (step @p423 :rule cong :premises (@p422 @p421) :args (@t242)) % 0.39/0.78 (step @p424 :rule cong :premises (@p423) :args (@t244)) % 0.39/0.78 (step @p425 :rule trans :premises (@p424 @p420)) % 0.39/0.78 (step @p426 :rule aci_norm :args ((= @t435 @t433))) % 0.39/0.78 (step @p427 :rule cong :premises (@p426) :args (@t437)) % 0.39/0.78 (step @p428 :rule quant-merge-prenex :args ((= (forall @t256 @t439) @t437))) % 0.39/0.78 (step @p429 :rule alpha_equiv :args (@t440 (@list @t427) (@list @t44))) % 0.39/0.78 (step @p430 :rule refl :args (@t431)) % 0.39/0.78 (step @p431 :rule refl :args (@t432)) % 0.39/0.78 (step @p432 :rule nary_cong :premises (@p431 @p430 @p429) :args (@t441)) % 0.39/0.78 (step @p433 :rule quant-miniscope-or :args ((= @t439 @t441))) % 0.39/0.78 (step @p434 :rule trans :premises (@p433 @p432)) % 0.39/0.78 (step @p435 :rule symm :premises (@p434)) % 0.39/0.78 (step @p436 :rule cong :premises (@p435) :args ((forall @t256 @t447))) % 0.39/0.78 (step @p437 :rule trans :premises (@p436 @p428)) % 0.39/0.78 (step @p438 :rule trans :premises (@p437 @p427)) % 0.39/0.78 (step @p439 :rule aci_norm :args ((= (or (or @t432 @t431) @t446) @t447))) % 0.39/0.78 (step @p440 :rule refl :args (@t446)) % 0.39/0.78 (step @p441 :rule bool-and-de-morgan :args (@t253 @t252 true)) % 0.39/0.78 (step @p442 :rule nary_cong :premises (@p441 @p440) :args ((or (not @t254) @t446))) % 0.39/0.78 (step @p443 :rule trans :premises (@p442 @p439)) % 0.39/0.78 (step @p444 :rule bool-impl-elim :args (@t254 @t446)) % 0.39/0.78 (step @p445 :rule trans :premises (@p444 @p443)) % 0.39/0.78 (step @p446 :rule cong :premises (@p445) :args ((forall @t256 (=> @t254 @t446)))) % 0.39/0.78 (step @p447 :rule trans :premises (@p446 @p438)) % 0.39/0.78 (step @p448 :rule aci_norm :args ((= (or (or @t444 @t443) @t442) @t445))) % 0.39/0.78 (step @p449 :rule refl :args (@t442)) % 0.39/0.78 (step @p450 :rule bool-and-de-morgan :args (@t247 @t246 true)) % 0.39/0.78 (step @p451 :rule nary_cong :premises (@p450 @p449) :args ((or (not @t248) @t442))) % 0.39/0.78 (step @p452 :rule trans :premises (@p451 @p448)) % 0.39/0.78 (step @p453 :rule bool-impl-elim :args (@t248 @t442)) % 0.39/0.78 (step @p454 :rule trans :premises (@p453 @p452)) % 0.39/0.78 (step @p455 :rule cong :premises (@p454) :args ((forall @t250 (=> @t248 @t442)))) % 0.39/0.78 (step @p456 :rule eq-symm :args (@t245 tptp.init)) % 0.39/0.78 (step @p457 :rule refl :args (@t248)) % 0.39/0.78 (step @p458 :rule cong :premises (@p457 @p456) :args (@t249)) % 0.39/0.78 (step @p459 :rule cong :premises (@p458) :args (@t251)) % 0.39/0.78 (step @p460 :rule trans :premises (@p459 @p455)) % 0.39/0.78 (step @p461 :rule refl :args (@t254)) % 0.39/0.78 (step @p462 :rule cong :premises (@p461 @p460) :args (@t255)) % 0.39/0.78 (step @p463 :rule cong :premises (@p462) :args (@t257)) % 0.39/0.78 (step @p464 :rule trans :premises (@p463 @p447)) % 0.39/0.78 (step @p465 :rule refl :args (@t258)) % 0.39/0.78 (step @p466 :rule nary_cong :premises (@p242 @p167 @p166 @p241 @p165 @p164 @p465 @p240 @p162 @p161 @p160 @p464 @p425 @p412 @p94) :args (@t259)) % 0.39/0.78 (step @p467 :rule cong :premises (@p466 @p399) :args (@t260)) % 0.39/0.78 (step @p468 :rule cong :premises (@p467) :args (@t261)) % 0.39/0.78 (step @p469 :rule eq_resolve :premises (@p53 @p468)) % 0.39/0.78 (step @p470 :rule not_implies_elim1 :premises (@p469)) % 0.39/0.78 (step @p471 :rule and_elim :premises (@p470) :args (0)) % 0.39/0.78 (step @p472 :rule and_elim :premises (@p470) :args (12)) % 0.39/0.78 (step @p473 :rule instantiate :premises (@p472) :args ((@list tptp.pv1388))) % 0.39/0.78 (step @p474 :rule bool-impl-elim :args (@t4 @t10)) % 0.39/0.78 (step @p475 :rule cong :premises (@p474) :args (@t11)) % 0.39/0.78 (step @p476 :rule eq_resolve :premises (@p8 @p475)) % 0.39/0.78 (step @p477 :rule instantiate :premises (@p476) :args (@t448)) % 0.39/0.78 (step @p478 :rule bool-impl-elim :args (@t67 @t4)) % 0.39/0.78 (step @p479 :rule cong :premises (@p478) :args (@t68)) % 0.39/0.78 (step @p480 :rule eq_resolve :premises (@p43 @p479)) % 0.39/0.78 (step @p481 :rule instantiate :premises (@p480) :args (@t448)) % 0.39/0.78 (step @p482 :rule instantiate :premises (@p476) :args (@t449)) % 0.39/0.78 (step @p483 :rule instantiate :premises (@p480) :args (@t449)) % 0.39/0.78 (step @p484 :rule and_elim :premises (@p470) :args (6)) % 0.39/0.78 (step @p485 :rule true_intro :premises (@p484)) % 0.39/0.78 (step @p486 :rule refl :args (tptp.pv1388)) % 0.39/0.78 (step @p487 :rule cong :premises (@p84 @p486) :args (@t450)) % 0.39/0.78 (step @p488 :rule trans :premises (@p487 @p485)) % 0.39/0.78 (step @p489 :rule true_elim :premises (@p488)) % 0.39/0.78 (step @p490 :rule cnf_or_pos :args (@t453)) % 0.39/0.78 (step @p491 :rule reordering :premises (@p490) :args ((or @t452 @t451 (not @t453)))) % 0.39/0.78 (step @p492 :rule chain_m_resolution :premises (@p491 @p489 @p483) :args (@t451 @t454 (@list @t450 @t453))) % 0.39/0.78 (step @p493 :rule cnf_or_pos :args (@t457)) % 0.39/0.78 (step @p494 :rule reordering :premises (@p493) :args ((or @t456 @t455 (not @t457)))) % 0.39/0.78 (step @p495 :rule chain_m_resolution :premises (@p494 @p492 @p482) :args (@t455 @t454 (@list @t451 @t457))) % 0.39/0.78 (step @p496 :rule cnf_or_pos :args (@t460)) % 0.39/0.78 (step @p497 :rule reordering :premises (@p496) :args ((or @t458 @t459 (not @t460)))) % 0.39/0.78 (step @p498 :rule chain_m_resolution :premises (@p497 @p495 @p481) :args (@t458 @t454 (@list @t455 @t460))) % 0.39/0.78 (step @p499 :rule cnf_or_pos :args (@t462)) % 0.39/0.78 (step @p500 :rule reordering :premises (@p499) :args ((or @t115 @t461 (not @t462)))) % 0.39/0.78 (step @p501 :rule chain_m_resolution :premises (@p500 @p498 @p477) :args (@t115 @t454 (@list @t458 @t462))) % 0.39/0.78 (step @p502 :rule and_elim :premises (@p470) :args (10)) % 0.39/0.78 (step @p503 :rule cnf_or_pos :args (@t465)) % 0.39/0.78 (step @p504 :rule reordering :premises (@p503) :args ((or @t359 @t463 @t464 (not @t465)))) % 0.39/0.78 (step @p505 :rule chain_m_resolution :premises (@p504 @p502 @p501 @p473) :args (@t359 @t466 (@list @t112 @t115 @t465))) % 0.39/0.78 (step @p506 :rule instantiate :premises (@p472) :args ((@list tptp.s_best7))) % 0.39/0.78 (step @p507 :rule and_elim :premises (@p470) :args (7)) % 0.39/0.78 (step @p508 :rule and_elim :premises (@p470) :args (3)) % 0.39/0.78 (step @p509 :rule cnf_or_pos :args (@t469)) % 0.39/0.78 (step @p510 :rule reordering :premises (@p509) :args ((or @t366 @t468 @t467 (not @t469)))) % 0.39/0.78 (step @p511 :rule chain_m_resolution :premises (@p510 @p508 @p507 @p506) :args (@t366 @t466 (@list @t155 @t154 @t469))) % 0.39/0.78 (step @p512 :rule and_elim :premises (@p470) :args (13)) % 0.39/0.78 (step @p513 :rule alpha_equiv :args (@t470 @t471 (@list @t81))) % 0.39/0.78 (step @p514 :rule equiv_elim1 :premises (@p513)) % 0.39/0.78 (step @p515 :rule reordering :premises (@p514) :args ((or @t276 @t472))) % 0.39/0.78 (step @p516 :rule chain_m_resolution :premises (@p515 @p512) :args (@t276 @t473 @t474)) % 0.39/0.78 (step @p517 :rule alpha_equiv :args (@t475 @t476 (@list @t89))) % 0.39/0.78 (step @p518 :rule equiv_elim1 :premises (@p517)) % 0.39/0.78 (step @p519 :rule reordering :premises (@p518) :args ((or @t281 @t477))) % 0.39/0.78 (step @p520 :rule chain_m_resolution :premises (@p519 @p472) :args (@t281 @t473 @t478)) % 0.39/0.78 (step @p521 :rule and_elim :premises (@p470) :args (11)) % 0.39/0.78 (step @p522 :rule alpha_equiv :args (@t479 @t480 (@list @t282 @t97))) % 0.39/0.78 (step @p523 :rule equiv_elim1 :premises (@p522)) % 0.39/0.78 (step @p524 :rule reordering :premises (@p523) :args ((or @t290 @t481))) % 0.39/0.78 (step @p525 :rule chain_m_resolution :premises (@p524 @p521) :args (@t290 @t473 @t482)) % 0.39/0.78 (step @p526 :rule and_elim :premises (@p470) :args (14)) % 0.39/0.78 (step @p527 :rule and_elim :premises (@p470) :args (9)) % 0.39/0.78 (step @p528 :rule and_elim :premises (@p470) :args (8)) % 0.39/0.78 (step @p529 :rule and_elim :premises (@p470) :args (5)) % 0.39/0.78 (step @p530 :rule and_elim :premises (@p470) :args (4)) % 0.39/0.78 (step @p531 :rule and_elim :premises (@p470) :args (2)) % 0.39/0.78 (step @p532 :rule and_elim :premises (@p470) :args (1)) % 0.39/0.78 (step @p533 :rule cnf_and_neg :args (@t293)) % 0.39/0.78 (step @p534 :rule reordering :premises (@p533) :args ((or @t293 @t489 @t488 @t487 @t486 @t485 @t484 @t463 @t483 @t464 (not @t290) (not @t281) (not @t276)))) % 0.39/0.78 (step @p535 :rule chain_m_resolution :premises (@p534 @p532 @p531 @p530 @p529 @p528 @p527 @p502 @p526 @p501 @p525 @p520 @p516) :args (@t293 (@list false false false false false false false false false false false false) (@list @t292 @t291 @t117 @t116 @t114 @t113 @t112 @t271 @t115 @t290 @t281 @t276))) % 0.39/0.78 (step @p536 :rule cnf_implies_neg2 :args (@t294)) % 0.39/0.78 (step @p537 :rule chain_m_resolution :premises (@p536 @p535) :args (@t294 @t473 (@list @t293))) % 0.39/0.78 (step @p538 :rule alpha_equiv :args (@t470 @t471 (@list @t187))) % 0.39/0.78 (step @p539 :rule equiv_elim1 :premises (@p538)) % 0.39/0.78 (step @p540 :rule reordering :premises (@p539) :args ((or @t342 @t472))) % 0.39/0.78 (step @p541 :rule chain_m_resolution :premises (@p540 @p512) :args (@t342 @t473 @t474)) % 0.39/0.78 (step @p542 :rule alpha_equiv :args (@t475 @t476 (@list @t195))) % 0.39/0.78 (step @p543 :rule equiv_elim1 :premises (@p542)) % 0.39/0.78 (step @p544 :rule reordering :premises (@p543) :args ((or @t347 @t477))) % 0.39/0.78 (step @p545 :rule chain_m_resolution :premises (@p544 @p472) :args (@t347 @t473 @t478)) % 0.39/0.78 (step @p546 :rule alpha_equiv :args (@t479 @t480 (@list @t348 @t55))) % 0.39/0.78 (step @p547 :rule equiv_elim1 :premises (@p546)) % 0.39/0.78 (step @p548 :rule reordering :premises (@p547) :args ((or @t356 @t481))) % 0.39/0.78 (step @p549 :rule chain_m_resolution :premises (@p548 @p521) :args (@t356 @t473 @t482)) % 0.39/0.78 (step @p550 :rule cnf_and_neg :args (@t357)) % 0.39/0.78 (step @p551 :rule chain_m_resolution :premises (@p550 @p471 @p532 @p531 @p508 @p530 @p529 @p507 @p528 @p527 @p549 @p545 @p541 @p526) :args (@t357 (@list false false false false false false false false false false false false false) (@list @t314 @t292 @t291 @t155 @t117 @t116 @t154 @t114 @t113 @t356 @t347 @t342 @t271))) % 0.39/0.78 (step @p552 :rule cnf_and_pos :args (@t357 12)) % 0.39/0.78 (step @p553 :rule reordering :premises (@p552) :args ((or @t271 @t490))) % 0.39/0.78 (step @p554 :rule cnf_implies_neg2 :args (@t358)) % 0.39/0.78 (step @p555 :rule alpha_equiv :args (@t479 @t480 (@list @t327 @t19))) % 0.39/0.78 (step @p556 :rule equiv_elim1 :premises (@p555)) % 0.39/0.78 (step @p557 :rule reordering :premises (@p556) :args ((or @t335 @t481))) % 0.39/0.78 (step @p558 :rule chain_m_resolution :premises (@p557 @p521) :args (@t335 @t473 @t482)) % 0.39/0.78 (step @p559 :rule alpha_equiv :args (@t475 @t476 (@list @t41))) % 0.39/0.78 (step @p560 :rule equiv_elim1 :premises (@p559)) % 0.39/0.78 (step @p561 :rule reordering :premises (@p560) :args ((or @t326 @t477))) % 0.39/0.78 (step @p562 :rule chain_m_resolution :premises (@p561 @p472) :args (@t326 @t473 @t478)) % 0.39/0.78 (step @p563 :rule alpha_equiv :args (@t470 @t471 (@list @t21))) % 0.39/0.78 (step @p564 :rule equiv_elim1 :premises (@p563)) % 0.39/0.78 (step @p565 :rule reordering :premises (@p564) :args ((or @t321 @t472))) % 0.39/0.78 (step @p566 :rule chain_m_resolution :premises (@p565 @p512) :args (@t321 @t473 @t474)) % 0.39/0.78 (step @p567 :rule cnf_and_neg :args (@t336)) % 0.39/0.78 (step @p568 :rule reordering :premises (@p567) :args ((or @t336 @t491 @t488 @t468 @t486 @t467 @t484 @t463 @t483 @t464 (not @t335) (not @t326) (not @t321)))) % 0.39/0.78 (step @p569 :rule alpha_equiv :args (@t479 @t480 (@list @t305 @t53))) % 0.39/0.78 (step @p570 :rule equiv_elim1 :premises (@p569)) % 0.39/0.78 (step @p571 :rule reordering :premises (@p570) :args ((or @t313 @t481))) % 0.39/0.78 (step @p572 :rule chain_m_resolution :premises (@p571 @p521) :args (@t313 @t473 @t482)) % 0.39/0.78 (step @p573 :rule alpha_equiv :args (@t475 @t476 (@list @t133))) % 0.39/0.78 (step @p574 :rule equiv_elim1 :premises (@p573)) % 0.39/0.78 (step @p575 :rule reordering :premises (@p574) :args ((or @t304 @t477))) % 0.39/0.78 (step @p576 :rule chain_m_resolution :premises (@p575 @p472) :args (@t304 @t473 @t478)) % 0.39/0.78 (step @p577 :rule alpha_equiv :args (@t470 @t471 (@list @t125))) % 0.39/0.78 (step @p578 :rule equiv_elim1 :premises (@p577)) % 0.39/0.78 (step @p579 :rule reordering :premises (@p578) :args ((or @t299 @t472))) % 0.39/0.78 (step @p580 :rule chain_m_resolution :premises (@p579 @p512) :args (@t299 @t473 @t474)) % 0.39/0.78 (step @p581 :rule cnf_and_neg :args (@t315)) % 0.39/0.78 (step @p582 :rule reordering :premises (@p581) :args ((or @t315 @t491 @t488 @t468 @t486 @t467 @t484 @t463 @t483 @t464 (not @t313) (not @t304) (not @t299)))) % 0.39/0.78 (step @p583 :rule cnf_implies_neg2 :args (@t337)) % 0.39/0.78 (step @p584 :rule cnf_implies_neg2 :args (@t316)) % 0.39/0.78 (step @p585 :rule instantiate :premises (@p472) :args ((@list tptp.s_sworst7))) % 0.39/0.78 (step @p586 :rule cnf_or_pos :args (@t492)) % 0.39/0.78 (step @p587 :rule reordering :premises (@p586) :args ((or @t360 @t487 @t485 (not @t492)))) % 0.39/0.78 (step @p588 :rule chain_m_resolution :premises (@p587 @p530 @p528 @p585) :args (@t360 @t466 (@list @t117 @t114 @t492))) % 0.39/0.78 (step @p589 :rule cnf_and_neg :args (@t361)) % 0.39/0.78 (step @p590 :rule reordering :premises (@p589) :args ((or @t361 @t489 @t493 (not @t360) (not @t358) (not @t337)))) % 0.39/0.78 (step @p591 :rule instantiate :premises (@p472) :args ((@list tptp.s_worst7))) % 0.39/0.78 (step @p592 :rule cnf_or_pos :args (@t494)) % 0.39/0.78 (step @p593 :rule reordering :premises (@p592) :args ((or @t363 @t486 @t484 (not @t494)))) % 0.39/0.78 (step @p594 :rule chain_m_resolution :premises (@p593 @p529 @p527 @p591) :args (@t363 @t466 (@list @t116 @t113 @t494))) % 0.39/0.78 (step @p595 :rule cnf_and_neg :args (@t364)) % 0.39/0.78 (step @p596 :rule reordering :premises (@p595) :args ((or @t364 @t488 @t493 (not @t363) (not @t362) (not @t316)))) % 0.39/0.78 (step @p597 :rule cnf_implies_neg2 :args (@t362)) % 0.39/0.78 (step @p598 :rule chain_m_resolution :premises (@p597 @p596 @p594 @p505 @p531 @p590 @p588 @p505 @p532 @p584 @p583 @p582 @p501 @p580 @p576 @p572 @p502 @p527 @p507 @p529 @p508 @p531 @p471 @p568 @p501 @p566 @p562 @p558 @p502 @p527 @p507 @p529 @p508 @p531 @p471 @p554 @p553) :args ((or @t364 @t490) (@list true false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false) (@list @t362 @t363 @t359 @t291 @t361 @t360 @t359 @t292 @t316 @t337 @t315 @t115 @t299 @t304 @t313 @t112 @t113 @t154 @t116 @t155 @t291 @t314 @t336 @t115 @t321 @t326 @t335 @t112 @t113 @t154 @t116 @t155 @t291 @t314 @t358 @t271))) % 0.39/0.78 (step @p599 :rule chain_m_resolution :premises (@p598 @p551) :args (@t364 @t473 (@list @t357))) % 0.39/0.78 (step @p600 :rule cnf_implies_neg2 :args (@t365)) % 0.39/0.78 (step @p601 :rule chain_m_resolution :premises (@p600 @p599) :args (@t365 @t473 (@list @t364))) % 0.39/0.78 (step @p602 :rule not_implies_elim2 :premises (@p469)) % 0.39/0.78 (step @p603 :rule not_and :premises (@p602)) % 0.39/0.78 (step @p604 false :rule chain_m_resolution :premises (@p603 @p601 @p537 @p511 @p505 @p471) :args (false (@list false false false false false) (@list @t365 @t294 @t366 @t359 @t314))) % 0.39/0.78 ) % 0.39/0.78 % SZS output end Proof % 0.39/0.78 % cvc5 exiting %------------------------------------------------------------------------------