%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : SWV125+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 : n027.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:34 AM UTC 2026 % Result : Theorem 0.38s 0.79s % Output : Proof 0.38s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWV125+1 : TPTP v9.2.1. Bugfixed v3.3.0. % 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.16/0.34 % Computer : n027.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Tue Jun 2 19:56:06 EDT 2026 % 0.16/0.34 % CPUTime : % 0.30/0.53 %----Proving TF0_NAR, FOF, or CNF % 0.38/0.79 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 0.38/0.79 % SZS status Theorem % 0.38/0.79 % SZS output start Proof % 0.38/0.79 ( % 0.38/0.79 (declare-sort $$unsorted 0) % 0.38/0.79 (declare-const tptp.pv21 $$unsorted) % 0.38/0.79 (declare-const tptp.pv32 $$unsorted) % 0.38/0.79 (declare-const tptp.pv5 $$unsorted) % 0.38/0.79 (declare-const tptp.sigma $$unsorted) % 0.38/0.79 (declare-const tptp.pv23 $$unsorted) % 0.38/0.79 (declare-const tptp.n1000 $$unsorted) % 0.38/0.79 (declare-const tptp.def $$unsorted) % 0.38/0.79 (declare-const tptp.use $$unsorted) % 0.38/0.79 (declare-const tptp.true Bool) % 0.38/0.79 (declare-const tptp.tptp_update2 (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.38/0.79 (declare-const tptp.pv31 $$unsorted) % 0.38/0.79 (declare-const tptp.a_select3 (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.38/0.79 (declare-const tptp.gt (-> $$unsorted $$unsorted Bool)) % 0.38/0.79 (declare-const tptp.uniform_int_rnd (-> $$unsorted $$unsorted $$unsorted)) % 0.38/0.79 (declare-const tptp.n6 $$unsorted) % 0.38/0.79 (declare-const tptp.n3 $$unsorted) % 0.38/0.79 (declare-const tptp.tptp_const_array1 (-> $$unsorted $$unsorted $$unsorted)) % 0.38/0.79 (declare-const tptp.pred (-> $$unsorted $$unsorted)) % 0.38/0.79 (declare-const tptp.tptp_minus_1 $$unsorted) % 0.38/0.79 (declare-const tptp.n0 $$unsorted) % 0.38/0.79 (declare-const tptp.tptp_msub (-> $$unsorted $$unsorted $$unsorted)) % 0.38/0.79 (declare-const tptp.n1 $$unsorted) % 0.38/0.79 (declare-const tptp.succ (-> $$unsorted $$unsorted)) % 0.38/0.79 (declare-const tptp.n5 $$unsorted) % 0.38/0.79 (declare-const tptp.n7 $$unsorted) % 0.38/0.79 (declare-const tptp.lt (-> $$unsorted $$unsorted Bool)) % 0.38/0.79 (declare-const tptp.tptp_update3 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.38/0.79 (declare-const tptp.minus (-> $$unsorted $$unsorted $$unsorted)) % 0.38/0.79 (declare-const tptp.n588 $$unsorted) % 0.38/0.79 (declare-const tptp.tptp_const_array2 (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.38/0.79 (declare-const tptp.geq (-> $$unsorted $$unsorted Bool)) % 0.38/0.79 (declare-const tptp.leq (-> $$unsorted $$unsorted Bool)) % 0.38/0.79 (declare-const tptp.trans (-> $$unsorted $$unsorted)) % 0.38/0.79 (declare-const tptp.a_select2 (-> $$unsorted $$unsorted $$unsorted)) % 0.38/0.79 (declare-const tptp.inv (-> $$unsorted $$unsorted)) % 0.38/0.79 (declare-const tptp.dim (-> $$unsorted $$unsorted $$unsorted)) % 0.38/0.79 (declare-const tptp.plus (-> $$unsorted $$unsorted $$unsorted)) % 0.38/0.79 (declare-const tptp.tptp_madd (-> $$unsorted $$unsorted $$unsorted)) % 0.38/0.79 (declare-const tptp.sum (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.38/0.79 (declare-const tptp.tptp_mmul (-> $$unsorted $$unsorted $$unsorted)) % 0.38/0.79 (declare-const tptp.tptp_float_0_0 $$unsorted) % 0.38/0.79 (declare-const tptp.n4 $$unsorted) % 0.38/0.79 (declare-const tptp.n2 $$unsorted) % 0.38/0.79 (define @t1 () (@var "Y" $$unsorted)) % 0.38/0.79 (define @t2 () (@var "X" $$unsorted)) % 0.38/0.79 (define @t3 () (= @t2 @t1)) % 0.38/0.79 (define @t4 () (tptp.gt @t1 @t2)) % 0.38/0.79 (define @t5 () (tptp.gt @t2 @t1)) % 0.38/0.79 (define @t6 () (@list @t2 @t1)) % 0.38/0.79 (define @t7 () (@var "Z" $$unsorted)) % 0.38/0.79 (define @t8 () (@list @t2 @t1 @t7)) % 0.38/0.79 (define @t9 () (@list @t2)) % 0.38/0.79 (define @t10 () (tptp.leq @t2 @t7)) % 0.38/0.79 (define @t11 () (tptp.leq @t1 @t7)) % 0.38/0.79 (define @t12 () (tptp.leq @t2 @t1)) % 0.38/0.79 (define @t13 () (and @t12 @t11)) % 0.38/0.79 (define @t14 () (forall @t8 (=> @t13 @t10))) % 0.38/0.79 (define @t15 () (forall @t6 (=> @t4 @t12))) % 0.38/0.79 (define @t16 () (tptp.leq @t2 (tptp.pred @t1))) % 0.38/0.79 (define @t17 () (forall @t6 (= @t16 @t4))) % 0.38/0.79 (define @t18 () (tptp.succ @t2)) % 0.38/0.79 (define @t19 () (tptp.succ @t1)) % 0.38/0.79 (define @t20 () (@var "C" $$unsorted)) % 0.38/0.79 (define @t21 () (tptp.uniform_int_rnd @t20 @t2)) % 0.38/0.79 (define @t22 () (tptp.leq tptp.n0 @t2)) % 0.38/0.79 (define @t23 () (@list @t2 @t20)) % 0.38/0.79 (define @t24 () (@var "Val" $$unsorted)) % 0.38/0.79 (define @t25 () (@var "I" $$unsorted)) % 0.38/0.79 (define @t26 () (@var "U" $$unsorted)) % 0.38/0.79 (define @t27 () (@var "L" $$unsorted)) % 0.38/0.79 (define @t28 () (tptp.leq @t25 @t26)) % 0.38/0.79 (define @t29 () (@var "J" $$unsorted)) % 0.38/0.79 (define @t30 () (@var "U2" $$unsorted)) % 0.38/0.79 (define @t31 () (@var "L2" $$unsorted)) % 0.38/0.79 (define @t32 () (@var "U1" $$unsorted)) % 0.38/0.79 (define @t33 () (@var "L1" $$unsorted)) % 0.38/0.79 (define @t34 () (@var "A" $$unsorted)) % 0.38/0.79 (define @t35 () (tptp.trans @t34)) % 0.38/0.79 (define @t36 () (@var "N" $$unsorted)) % 0.38/0.79 (define @t37 () (tptp.leq @t29 @t36)) % 0.38/0.79 (define @t38 () (tptp.leq tptp.n0 @t29)) % 0.38/0.79 (define @t39 () (tptp.leq @t25 @t36)) % 0.38/0.79 (define @t40 () (tptp.leq tptp.n0 @t25)) % 0.38/0.79 (define @t41 () (and @t40 @t39 @t38 @t37)) % 0.38/0.79 (define @t42 () (@list @t25 @t29)) % 0.38/0.79 (define @t43 () (forall @t42 (=> @t41 (= (tptp.a_select3 @t34 @t25 @t29) (tptp.a_select3 @t34 @t29 @t25))))) % 0.38/0.79 (define @t44 () (@list @t34 @t36)) % 0.38/0.79 (define @t45 () (tptp.inv @t34)) % 0.38/0.79 (define @t46 () (@var "VAL" $$unsorted)) % 0.38/0.79 (define @t47 () (@var "K" $$unsorted)) % 0.38/0.79 (define @t48 () (tptp.tptp_update3 @t34 @t47 @t47 @t46)) % 0.38/0.79 (define @t49 () (@var "B" $$unsorted)) % 0.38/0.79 (define @t50 () (tptp.tptp_madd @t34 @t49)) % 0.38/0.79 (define @t51 () (= (tptp.a_select3 @t49 @t25 @t29) (tptp.a_select3 @t49 @t29 @t25))) % 0.38/0.79 (define @t52 () (forall @t42 (=> @t41 @t51))) % 0.38/0.79 (define @t53 () (and @t43 @t52)) % 0.38/0.79 (define @t54 () (@list @t34 @t49 @t36)) % 0.38/0.79 (define @t55 () (tptp.tptp_msub @t34 @t49)) % 0.38/0.79 (define @t56 () (tptp.tptp_mmul @t34 (tptp.tptp_mmul @t49 @t35))) % 0.38/0.79 (define @t57 () (forall @t42 (=> @t41 (= (tptp.a_select3 @t56 @t25 @t29) (tptp.a_select3 @t56 @t29 @t25))))) % 0.38/0.79 (define @t58 () (@var "M" $$unsorted)) % 0.38/0.79 (define @t59 () (and @t40 (tptp.leq @t25 @t58) @t38 (tptp.leq @t29 @t58))) % 0.38/0.79 (define @t60 () (@var "E" $$unsorted)) % 0.38/0.79 (define @t61 () (@var "F" $$unsorted)) % 0.38/0.79 (define @t62 () (@var "D" $$unsorted)) % 0.38/0.79 (define @t63 () (tptp.tptp_madd @t34 (tptp.tptp_mmul @t49 (tptp.tptp_mmul (tptp.tptp_madd (tptp.tptp_mmul @t20 (tptp.tptp_mmul @t62 (tptp.trans @t20))) (tptp.tptp_mmul @t60 (tptp.tptp_mmul @t61 (tptp.trans @t60)))) (tptp.trans @t49))))) % 0.38/0.79 (define @t64 () (@var "Body" $$unsorted)) % 0.38/0.79 (define @t65 () (tptp.sum tptp.n0 tptp.tptp_minus_1 @t64)) % 0.38/0.79 (define @t66 () (@list @t64)) % 0.38/0.79 (define @t67 () (tptp.succ @t18)) % 0.38/0.79 (define @t68 () (tptp.succ @t67)) % 0.38/0.79 (define @t69 () (tptp.succ @t68)) % 0.38/0.79 (define @t70 () (tptp.succ @t69)) % 0.38/0.79 (define @t71 () (tptp.pred @t2)) % 0.38/0.79 (define @t72 () (forall @t9 (= (tptp.minus @t2 tptp.n1) @t71))) % 0.38/0.79 (define @t73 () (tptp.pred @t18)) % 0.38/0.79 (define @t74 () (forall @t9 (= @t73 @t2))) % 0.38/0.79 (define @t75 () (@var "V" $$unsorted)) % 0.38/0.79 (define @t76 () (tptp.tptp_update3 @t2 @t26 @t75 @t46)) % 0.38/0.79 (define @t77 () (@var "VAL2" $$unsorted)) % 0.38/0.79 (define @t78 () (not (= @t25 @t26))) % 0.38/0.79 (define @t79 () (@var "J0" $$unsorted)) % 0.38/0.79 (define @t80 () (@var "I0" $$unsorted)) % 0.38/0.79 (define @t81 () (tptp.leq @t80 @t26)) % 0.38/0.79 (define @t82 () (tptp.leq tptp.n0 @t80)) % 0.38/0.79 (define @t83 () (tptp.tptp_update2 @t2 @t26 @t46)) % 0.38/0.79 (define @t84 () (tptp.minus tptp.n1000 tptp.n1)) % 0.38/0.79 (define @t85 () (tptp.geq @t84 tptp.n0)) % 0.38/0.79 (define @t86 () (tptp.minus tptp.n4 tptp.n1)) % 0.38/0.79 (define @t87 () (tptp.geq @t86 tptp.n0)) % 0.38/0.79 (define @t88 () (and @t87 @t85)) % 0.38/0.79 (define @t89 () (=> @t88 tptp.true)) % 0.38/0.79 (define @t90 () (tptp.minus tptp.n6 tptp.n1)) % 0.38/0.79 (define @t91 () (tptp.geq @t90 tptp.n0)) % 0.38/0.79 (define @t92 () (=> @t91 @t89)) % 0.38/0.79 (define @t93 () (tptp.leq tptp.n0 (tptp.a_select2 tptp.sigma tptp.pv23))) % 0.38/0.79 (define @t94 () (=> @t93 tptp.true)) % 0.38/0.79 (define @t95 () (tptp.leq tptp.pv23 @t90)) % 0.38/0.79 (define @t96 () (tptp.leq tptp.n0 tptp.pv23)) % 0.38/0.79 (define @t97 () (and @t96 @t95)) % 0.38/0.79 (define @t98 () (tptp.leq tptp.pv5 tptp.n588)) % 0.38/0.79 (define @t99 () (tptp.leq tptp.n0 tptp.pv5)) % 0.38/0.79 (define @t100 () (and @t99 @t98)) % 0.38/0.79 (define @t101 () (tptp.leq tptp.pv5 @t84)) % 0.38/0.79 (define @t102 () (tptp.leq tptp.n7 tptp.n7)) % 0.38/0.79 (define @t103 () (tptp.leq tptp.n6 tptp.n7)) % 0.38/0.79 (define @t104 () (tptp.leq tptp.n5 @t90)) % 0.38/0.79 (define @t105 () (tptp.leq tptp.n5 tptp.n7)) % 0.38/0.79 (define @t106 () (tptp.leq tptp.n4 @t90)) % 0.38/0.79 (define @t107 () (tptp.leq tptp.n4 tptp.n7)) % 0.38/0.79 (define @t108 () (tptp.leq tptp.n3 @t90)) % 0.38/0.79 (define @t109 () (tptp.leq tptp.n3 @t86)) % 0.38/0.79 (define @t110 () (tptp.leq tptp.n3 tptp.n7)) % 0.38/0.79 (define @t111 () (tptp.leq tptp.n2 @t90)) % 0.38/0.79 (define @t112 () (tptp.leq tptp.n2 @t86)) % 0.38/0.79 (define @t113 () (tptp.leq tptp.n2 tptp.n7)) % 0.38/0.79 (define @t114 () (tptp.leq tptp.n1 @t90)) % 0.38/0.79 (define @t115 () (tptp.leq tptp.n1 @t86)) % 0.38/0.79 (define @t116 () (tptp.leq tptp.n1 tptp.n7)) % 0.38/0.79 (define @t117 () (tptp.leq tptp.n0 @t90)) % 0.38/0.79 (define @t118 () (tptp.leq tptp.n0 @t86)) % 0.38/0.79 (define @t119 () (tptp.leq tptp.n0 tptp.n7)) % 0.38/0.79 (define @t120 () (tptp.leq tptp.n0 tptp.n6)) % 0.38/0.79 (define @t121 () (tptp.leq tptp.n0 tptp.n5)) % 0.38/0.79 (define @t122 () (tptp.leq tptp.n0 tptp.n4)) % 0.38/0.79 (define @t123 () (tptp.leq tptp.n0 tptp.n3)) % 0.38/0.79 (define @t124 () (tptp.leq tptp.n0 tptp.n2)) % 0.38/0.79 (define @t125 () (tptp.leq tptp.n0 tptp.n1)) % 0.38/0.79 (define @t126 () (tptp.leq tptp.n0 tptp.n0)) % 0.38/0.79 (define @t127 () (and @t126 @t125 @t124 @t123 @t122 @t121 @t120 @t119 @t99 @t118 @t117 @t116 @t115 @t114 @t113 @t112 @t111 @t110 @t109 @t108 @t107 @t106 @t105 @t104 @t103 @t102 @t98 @t101)) % 0.38/0.79 (define @t128 () (tptp.gt tptp.pv5 tptp.n0)) % 0.38/0.79 (define @t129 () (=> @t128 @t127)) % 0.38/0.79 (define @t130 () (and @t126 @t125 @t124 @t123 @t122 @t121 @t120 @t119 @t99 @t117 @t116 @t114 @t113 @t111 @t110 @t108 @t107 @t106 @t105 @t104 @t103 @t102 @t98 @t101)) % 0.38/0.79 (define @t131 () (not @t128)) % 0.38/0.79 (define @t132 () (=> @t131 @t130)) % 0.38/0.79 (define @t133 () (and @t126 @t125 @t124 @t123 @t99 @t118 @t115 @t112 @t109 @t101 @t132 @t129)) % 0.38/0.79 (define @t134 () (=> @t128 @t133)) % 0.38/0.79 (define @t135 () (and @t132 @t129)) % 0.38/0.79 (define @t136 () (=> @t131 @t135)) % 0.38/0.79 (define @t137 () (and @t126 @t125 @t124 @t123 @t122 @t121 @t120 @t119 @t99 @t117 @t116 @t113 @t110 @t108 @t107 @t105 @t103 @t102 @t101 @t136 @t134)) % 0.38/0.79 (define @t138 () (=> @t128 @t137)) % 0.38/0.79 (define @t139 () (and @t136 @t134)) % 0.38/0.79 (define @t140 () (=> @t131 @t139)) % 0.38/0.79 (define @t141 () (and @t126 @t125 @t124 @t123 @t122 @t121 @t120 @t119 @t99 @t117 @t116 @t114 @t113 @t111 @t110 @t107 @t106 @t105 @t104 @t103 @t102 @t101 @t140 @t138)) % 0.38/0.79 (define @t142 () (and @t140 @t138)) % 0.38/0.79 (define @t143 () (and @t126 @t125 @t124 @t123 @t99 @t118 @t117 @t115 @t114 @t112 @t111 @t109 @t101 (=> @t131 @t142) (=> @t128 @t141))) % 0.38/0.79 (define @t144 () (tptp.leq tptp.pv31 @t90)) % 0.38/0.79 (define @t145 () (tptp.leq tptp.n0 tptp.pv31)) % 0.38/0.79 (define @t146 () (and @t99 @t145 @t98 @t144)) % 0.38/0.79 (define @t147 () (tptp.leq tptp.pv32 @t90)) % 0.38/0.79 (define @t148 () (tptp.leq tptp.n0 tptp.pv32)) % 0.38/0.79 (define @t149 () (and @t99 @t145 @t148 @t98 @t144 @t147)) % 0.38/0.79 (define @t150 () (= tptp.pv31 tptp.pv32)) % 0.38/0.79 (define @t151 () (not @t150)) % 0.38/0.79 (define @t152 () (and (=> @t151 @t149) (=> @t150 @t149))) % 0.38/0.79 (define @t153 () (tptp.leq tptp.pv21 @t90)) % 0.38/0.79 (define @t154 () (tptp.leq tptp.pv21 tptp.n5)) % 0.38/0.79 (define @t155 () (tptp.leq tptp.n0 tptp.pv21)) % 0.38/0.79 (define @t156 () (and @t126 @t99 @t155 @t98 @t154 @t153)) % 0.38/0.79 (define @t157 () (and @t99 @t155 @t98 @t153)) % 0.38/0.79 (define @t158 () (tptp.leq tptp.n0 @t84)) % 0.38/0.79 (define @t159 () (and @t126 @t125 @t124 @t123 @t122 @t121 @t120 @t119 @t118 @t117 @t158 @t116 @t115 @t114 @t113 @t112 @t111 @t110 @t109 @t108 @t107 @t106 @t105 @t104 @t103 @t102)) % 0.38/0.79 (define @t160 () (and (=> tptp.true tptp.true) (=> tptp.true @t159) (=> @t157 @t156) (=> @t149 @t152) (=> @t146 @t146) (=> @t146 @t100) (=> @t100 tptp.true) (=> @t100 @t143) (=> @t100 @t100) (=> @t97 @t94) (=> @t91 @t92))) % 0.38/0.79 (define @t161 () (@list @t49)) % 0.38/0.79 (define @t162 () (forall @t161 @t160)) % 0.38/0.79 (define @t163 () (tptp.geq tptp.n7 tptp.n0)) % 0.38/0.79 (define @t164 () (and @t163 @t85)) % 0.38/0.79 (define @t165 () (=> @t164 @t162)) % 0.38/0.79 (define @t166 () (@list @t34)) % 0.38/0.79 (define @t167 () (forall @t166 @t165)) % 0.38/0.79 (define @t168 () (=> @t88 @t167)) % 0.38/0.79 (define @t169 () (not @t168)) % 0.38/0.79 (define @t170 () (tptp.gt tptp.n1000 tptp.n588)) % 0.38/0.79 (define @t171 () (tptp.gt tptp.n5 tptp.n4)) % 0.38/0.79 (define @t172 () (tptp.gt tptp.n7 tptp.n4)) % 0.38/0.79 (define @t173 () (tptp.gt tptp.n6 tptp.n5)) % 0.38/0.79 (define @t174 () (tptp.gt tptp.n7 tptp.n5)) % 0.38/0.79 (define @t175 () (tptp.gt tptp.n7 tptp.n6)) % 0.38/0.79 (define @t176 () (tptp.gt tptp.n4 tptp.n0)) % 0.38/0.79 (define @t177 () (tptp.gt tptp.n5 tptp.n0)) % 0.38/0.79 (define @t178 () (tptp.gt tptp.n6 tptp.n0)) % 0.38/0.79 (define @t179 () (tptp.gt tptp.n1 tptp.n0)) % 0.38/0.79 (define @t180 () (tptp.gt tptp.n2 tptp.n0)) % 0.38/0.79 (define @t181 () (tptp.gt tptp.n3 tptp.n0)) % 0.38/0.79 (define @t182 () (tptp.gt tptp.n5 tptp.n1)) % 0.38/0.79 (define @t183 () (tptp.gt tptp.n7 tptp.n1)) % 0.38/0.79 (define @t184 () (tptp.gt tptp.n3 tptp.n1)) % 0.38/0.79 (define @t185 () (tptp.gt tptp.n5 tptp.n2)) % 0.38/0.79 (define @t186 () (tptp.gt tptp.n7 tptp.n2)) % 0.38/0.79 (define @t187 () (tptp.gt tptp.n3 tptp.n2)) % 0.38/0.79 (define @t188 () (tptp.gt tptp.n4 tptp.n3)) % 0.38/0.79 (define @t189 () (tptp.gt tptp.n5 tptp.n3)) % 0.38/0.79 (define @t190 () (tptp.gt tptp.n7 tptp.n3)) % 0.38/0.79 (define @t191 () (= @t2 tptp.n4)) % 0.38/0.79 (define @t192 () (= @t2 tptp.n3)) % 0.38/0.79 (define @t193 () (= @t2 tptp.n2)) % 0.38/0.79 (define @t194 () (= @t2 tptp.n1)) % 0.38/0.79 (define @t195 () (= @t2 tptp.n0)) % 0.38/0.79 (define @t196 () (= @t2 tptp.n5)) % 0.38/0.79 (define @t197 () (tptp.succ tptp.n0)) % 0.38/0.79 (define @t198 () (tptp.succ @t197)) % 0.38/0.79 (define @t199 () (tptp.succ @t198)) % 0.38/0.79 (define @t200 () (tptp.succ @t199)) % 0.38/0.79 (define @t201 () (tptp.succ @t200)) % 0.38/0.79 (define @t202 () (tptp.succ @t201)) % 0.38/0.79 (define @t203 () (not @t98)) % 0.38/0.79 (define @t204 () (not @t99)) % 0.38/0.79 (define @t205 () (or @t204 @t203 tptp.true)) % 0.38/0.79 (define @t206 () (@list false)) % 0.38/0.79 (define @t207 () (@list tptp.true)) % 0.38/0.79 (define @t208 () (not @t93)) % 0.38/0.79 (define @t209 () (not @t95)) % 0.38/0.79 (define @t210 () (not @t96)) % 0.38/0.79 (define @t211 () (or @t210 @t209 @t208 tptp.true)) % 0.38/0.79 (define @t212 () (not @t85)) % 0.38/0.79 (define @t213 () (not @t87)) % 0.38/0.79 (define @t214 () (not @t91)) % 0.38/0.79 (define @t215 () (or @t214 @t213 @t212 tptp.true)) % 0.38/0.79 (define @t216 () (or @t204 @t203 @t100)) % 0.38/0.79 (define @t217 () (not @t204)) % 0.38/0.79 (define @t218 () (not @t203)) % 0.38/0.79 (define @t219 () (not @t100)) % 0.38/0.79 (define @t220 () (@list true false false)) % 0.38/0.79 (define @t221 () (tptp.pred tptp.n1000)) % 0.38/0.79 (define @t222 () (tptp.leq tptp.n588 @t221)) % 0.38/0.79 (define @t223 () (= @t170 @t222)) % 0.38/0.79 (define @t224 () (@list false false)) % 0.38/0.79 (define @t225 () (not @t11)) % 0.38/0.79 (define @t226 () (not @t12)) % 0.38/0.79 (define @t227 () (or @t226 @t225 @t10)) % 0.38/0.79 (define @t228 () (tptp.leq tptp.pv5 @t221)) % 0.38/0.79 (define @t229 () (not @t222)) % 0.38/0.79 (define @t230 () (or @t203 @t229 @t228)) % 0.38/0.79 (define @t231 () (not @t153)) % 0.38/0.79 (define @t232 () (not @t155)) % 0.38/0.79 (define @t233 () (or @t204 @t232 @t203 @t231 @t156)) % 0.38/0.79 (define @t234 () (or @t151 @t149)) % 0.38/0.79 (define @t235 () (or @t150 @t149)) % 0.38/0.79 (define @t236 () (and @t235 @t234)) % 0.38/0.79 (define @t237 () (not @t147)) % 0.38/0.79 (define @t238 () (not @t144)) % 0.38/0.79 (define @t239 () (not @t148)) % 0.38/0.79 (define @t240 () (not @t145)) % 0.38/0.79 (define @t241 () (or @t204 @t240 @t239 @t203 @t238 @t237 @t236)) % 0.38/0.79 (define @t242 () (or @t204 @t240 @t203 @t238 @t146)) % 0.38/0.79 (define @t243 () (or @t204 @t240 @t203 @t238 @t100)) % 0.38/0.79 (define @t244 () (or @t131 @t127)) % 0.38/0.79 (define @t245 () (or @t128 @t130)) % 0.38/0.79 (define @t246 () (and @t126 @t125 @t124 @t123 @t99 @t118 @t115 @t112 @t109 @t101 @t245 @t244)) % 0.38/0.79 (define @t247 () (or @t131 @t246)) % 0.38/0.79 (define @t248 () (and @t245 @t244)) % 0.38/0.79 (define @t249 () (or @t128 @t248)) % 0.38/0.79 (define @t250 () (and @t126 @t125 @t124 @t123 @t122 @t121 @t120 @t119 @t99 @t117 @t116 @t113 @t110 @t108 @t107 @t105 @t103 @t102 @t101 @t249 @t247)) % 0.38/0.79 (define @t251 () (or @t131 @t250)) % 0.38/0.79 (define @t252 () (and @t249 @t247)) % 0.38/0.79 (define @t253 () (or @t128 @t252)) % 0.38/0.79 (define @t254 () (and @t126 @t125 @t124 @t123 @t122 @t121 @t120 @t119 @t99 @t117 @t116 @t114 @t113 @t111 @t110 @t107 @t106 @t105 @t104 @t103 @t102 @t101 @t253 @t251)) % 0.38/0.79 (define @t255 () (or @t131 @t254)) % 0.38/0.79 (define @t256 () (and @t253 @t251)) % 0.38/0.79 (define @t257 () (or @t128 @t256)) % 0.38/0.79 (define @t258 () (and @t126 @t125 @t124 @t123 @t99 @t118 @t117 @t115 @t114 @t112 @t111 @t109 @t101 @t257 @t255)) % 0.38/0.79 (define @t259 () (or @t204 @t203 @t258)) % 0.38/0.79 (define @t260 () (not @t175)) % 0.38/0.79 (define @t261 () (or @t260 @t103)) % 0.38/0.79 (define @t262 () (tptp.pred tptp.n6)) % 0.38/0.79 (define @t263 () (tptp.leq tptp.n5 @t262)) % 0.38/0.79 (define @t264 () (= @t173 @t263)) % 0.38/0.79 (define @t265 () (not @t174)) % 0.38/0.79 (define @t266 () (or @t265 @t105)) % 0.38/0.79 (define @t267 () (tptp.leq tptp.n4 tptp.n5)) % 0.38/0.79 (define @t268 () (not @t171)) % 0.38/0.79 (define @t269 () (or @t268 @t267)) % 0.38/0.79 (define @t270 () (not @t172)) % 0.38/0.79 (define @t271 () (or @t270 @t107)) % 0.38/0.79 (define @t272 () (tptp.leq tptp.n3 tptp.n5)) % 0.38/0.79 (define @t273 () (not @t189)) % 0.38/0.79 (define @t274 () (or @t273 @t272)) % 0.38/0.79 (define @t275 () (tptp.pred tptp.n4)) % 0.38/0.79 (define @t276 () (tptp.leq tptp.n3 @t275)) % 0.38/0.79 (define @t277 () (= @t188 @t276)) % 0.38/0.79 (define @t278 () (not @t190)) % 0.38/0.79 (define @t279 () (or @t278 @t110)) % 0.38/0.79 (define @t280 () (tptp.leq tptp.n2 tptp.n5)) % 0.38/0.79 (define @t281 () (not @t185)) % 0.38/0.79 (define @t282 () (or @t281 @t280)) % 0.38/0.79 (define @t283 () (tptp.leq tptp.n2 tptp.n3)) % 0.38/0.79 (define @t284 () (not @t187)) % 0.38/0.79 (define @t285 () (or @t284 @t283)) % 0.38/0.79 (define @t286 () (not @t186)) % 0.38/0.79 (define @t287 () (or @t286 @t113)) % 0.38/0.79 (define @t288 () (tptp.leq tptp.n1 tptp.n5)) % 0.38/0.79 (define @t289 () (not @t182)) % 0.38/0.79 (define @t290 () (or @t289 @t288)) % 0.38/0.79 (define @t291 () (tptp.leq tptp.n1 tptp.n3)) % 0.38/0.79 (define @t292 () (not @t184)) % 0.38/0.79 (define @t293 () (or @t292 @t291)) % 0.38/0.79 (define @t294 () (not @t183)) % 0.38/0.79 (define @t295 () (or @t294 @t116)) % 0.38/0.79 (define @t296 () (or (not tptp.true) @t159)) % 0.38/0.79 (define @t297 () (and @t296 @t233 @t241 @t242 @t243 @t205 @t259 @t216 @t211 @t215)) % 0.38/0.79 (define @t298 () (not @t163)) % 0.38/0.79 (define @t299 () (or @t298 @t212 @t297)) % 0.38/0.79 (define @t300 () (and true @t296 @t233 @t241 @t242 @t243 @t205 @t259 @t216 @t211 @t215)) % 0.38/0.79 (define @t301 () (or @t213 @t212 tptp.true)) % 0.38/0.79 (define @t302 () (or @t204 @t203)) % 0.38/0.79 (define @t303 () (not @t131)) % 0.38/0.79 (define @t304 () (or @t204 @t240 @t203 @t238)) % 0.38/0.79 (define @t305 () (not @t146)) % 0.38/0.79 (define @t306 () (or @t204 @t240 @t239 @t203 @t238 @t237)) % 0.38/0.79 (define @t307 () (not @t149)) % 0.38/0.79 (define @t308 () (or @t204 @t232 @t203 @t231)) % 0.38/0.79 (define @t309 () (= @t85 @t158)) % 0.38/0.79 (define @t310 () (not @t177)) % 0.38/0.79 (define @t311 () (or @t310 @t121)) % 0.38/0.79 (define @t312 () (= @t87 @t118)) % 0.38/0.79 (define @t313 () (= @t163 @t119)) % 0.38/0.79 (define @t314 () (not @t178)) % 0.38/0.79 (define @t315 () (or @t314 @t120)) % 0.38/0.79 (define @t316 () (not @t176)) % 0.38/0.79 (define @t317 () (or @t316 @t122)) % 0.38/0.79 (define @t318 () (not @t181)) % 0.38/0.79 (define @t319 () (or @t318 @t123)) % 0.38/0.79 (define @t320 () (not @t180)) % 0.38/0.79 (define @t321 () (or @t320 @t124)) % 0.38/0.79 (define @t322 () (not @t179)) % 0.38/0.79 (define @t323 () (or @t322 @t125)) % 0.38/0.79 (define @t324 () (@list false false false false false false false false false false)) % 0.38/0.79 (define @t325 () (forall @t8 @t227)) % 0.38/0.79 (define @t326 () (forall @t6 (= @t4 @t16))) % 0.38/0.79 (define @t327 () (@list tptp.n1000)) % 0.38/0.79 (define @t328 () (= @t84 @t221)) % 0.38/0.79 (define @t329 () (and @t328 @t228)) % 0.38/0.79 (define @t330 () (not @t240)) % 0.38/0.79 (define @t331 () (not @t238)) % 0.38/0.79 (define @t332 () (not @t101)) % 0.38/0.79 (define @t333 () (not @t102)) % 0.38/0.79 (define @t334 () (not @t103)) % 0.38/0.79 (define @t335 () (not @t104)) % 0.38/0.79 (define @t336 () (not @t105)) % 0.38/0.79 (define @t337 () (not @t106)) % 0.38/0.79 (define @t338 () (not @t107)) % 0.38/0.79 (define @t339 () (not @t108)) % 0.38/0.79 (define @t340 () (not @t109)) % 0.38/0.79 (define @t341 () (not @t110)) % 0.38/0.79 (define @t342 () (not @t111)) % 0.38/0.79 (define @t343 () (not @t112)) % 0.38/0.79 (define @t344 () (not @t113)) % 0.38/0.79 (define @t345 () (not @t114)) % 0.38/0.79 (define @t346 () (not @t115)) % 0.38/0.79 (define @t347 () (not @t116)) % 0.38/0.79 (define @t348 () (not @t117)) % 0.38/0.79 (define @t349 () (not @t118)) % 0.38/0.79 (define @t350 () (not @t119)) % 0.38/0.79 (define @t351 () (not @t120)) % 0.38/0.79 (define @t352 () (not @t121)) % 0.38/0.79 (define @t353 () (not @t122)) % 0.38/0.79 (define @t354 () (not @t123)) % 0.38/0.79 (define @t355 () (not @t124)) % 0.38/0.79 (define @t356 () (not @t125)) % 0.38/0.79 (define @t357 () (not @t126)) % 0.38/0.79 (define @t358 () (= tptp.n5 @t201)) % 0.38/0.79 (define @t359 () (= tptp.n6 @t202)) % 0.38/0.79 (define @t360 () (= @t90 @t262)) % 0.38/0.79 (define @t361 () (tptp.pred @t202)) % 0.38/0.79 (define @t362 () (= @t201 @t361)) % 0.38/0.79 (define @t363 () (and @t153 @t358 @t359 @t360 @t362)) % 0.38/0.79 (define @t364 () (@list true)) % 0.38/0.79 (define @t365 () (@list @t98)) % 0.38/0.79 (assume @p1 (forall @t6 (or @t5 @t4 @t3))) % 0.38/0.79 (assume @p2 (forall @t8 (=> (and @t5 (tptp.gt @t1 @t7)) (tptp.gt @t2 @t7)))) % 0.38/0.80 (assume @p3 (forall @t9 (not (tptp.gt @t2 @t2)))) % 0.38/0.80 (assume @p4 (forall @t9 (tptp.leq @t2 @t2))) % 0.38/0.80 (assume @p5 @t14) % 0.38/0.80 (assume @p6 (forall @t6 (= (tptp.lt @t2 @t1) @t4))) % 0.38/0.80 (assume @p7 (forall @t6 (= (tptp.geq @t2 @t1) (tptp.leq @t1 @t2)))) % 0.38/0.80 (assume @p8 @t15) % 0.38/0.80 (assume @p9 (forall @t6 (=> (and @t12 (not @t3)) @t4))) % 0.38/0.80 (assume @p10 @t17) % 0.38/0.80 (assume @p11 (forall @t9 (tptp.gt @t18 @t2))) % 0.38/0.80 (assume @p12 (forall @t6 (=> @t12 (tptp.leq @t2 @t19)))) % 0.38/0.80 (assume @p13 (forall @t6 (= @t12 (tptp.gt @t19 @t2)))) % 0.38/0.80 (assume @p14 (forall @t23 (=> @t22 (tptp.leq @t21 @t2)))) % 0.38/0.80 (assume @p15 (forall @t23 (=> @t22 (tptp.leq tptp.n0 @t21)))) % 0.38/0.80 (assume @p16 (forall (@list @t25 @t27 @t26 @t24) (=> (and (tptp.leq @t27 @t25) @t28) (= (tptp.a_select2 (tptp.tptp_const_array1 (tptp.dim @t27 @t26) @t24) @t25) @t24)))) % 0.38/0.80 (assume @p17 (forall (@list @t25 @t33 @t32 @t29 @t31 @t30 @t24) (=> (and (tptp.leq @t33 @t25) (tptp.leq @t25 @t32) (tptp.leq @t31 @t29) (tptp.leq @t29 @t30)) (= (tptp.a_select3 (tptp.tptp_const_array2 (tptp.dim @t33 @t32) (tptp.dim @t31 @t30) @t24) @t25 @t29) @t24)))) % 0.38/0.80 (assume @p18 (forall @t44 (=> @t43 (forall @t42 (=> @t41 (= (tptp.a_select3 @t35 @t25 @t29) (tptp.a_select3 @t35 @t29 @t25))))))) % 0.38/0.80 (assume @p19 (forall @t44 (=> @t43 (forall @t42 (=> @t41 (= (tptp.a_select3 @t45 @t25 @t29) (tptp.a_select3 @t45 @t29 @t25))))))) % 0.38/0.80 (assume @p20 (forall @t44 (=> @t43 (forall (@list @t25 @t29 @t47 @t46) (=> (and @t40 @t39 @t38 @t37 (tptp.leq tptp.n0 @t47) (tptp.leq @t47 @t36)) (= (tptp.a_select3 @t48 @t25 @t29) (tptp.a_select3 @t48 @t29 @t25))))))) % 0.38/0.80 (assume @p21 (forall @t54 (=> @t53 (forall @t42 (=> @t41 (= (tptp.a_select3 @t50 @t25 @t29) (tptp.a_select3 @t50 @t29 @t25))))))) % 0.38/0.80 (assume @p22 (forall @t54 (=> @t53 (forall @t42 (=> @t41 (= (tptp.a_select3 @t55 @t25 @t29) (tptp.a_select3 @t55 @t29 @t25))))))) % 0.38/0.80 (assume @p23 (forall @t54 (=> @t52 @t57))) % 0.38/0.80 (assume @p24 (forall (@list @t34 @t49 @t36 @t58) (=> (forall @t42 (=> @t59 @t51)) @t57))) % 0.38/0.80 (assume @p25 (forall (@list @t34 @t49 @t20 @t62 @t60 @t61 @t36 @t58) (=> (and (forall @t42 (=> @t59 (= (tptp.a_select3 @t62 @t25 @t29) (tptp.a_select3 @t62 @t29 @t25)))) @t43 (forall @t42 (=> @t41 (= (tptp.a_select3 @t61 @t25 @t29) (tptp.a_select3 @t61 @t29 @t25))))) (forall @t42 (=> @t41 (= (tptp.a_select3 @t63 @t25 @t29) (tptp.a_select3 @t63 @t29 @t25))))))) % 0.38/0.80 (assume @p26 (forall @t66 (= @t65 tptp.n0))) % 0.38/0.80 (assume @p27 (forall @t66 (= tptp.tptp_float_0_0 @t65))) % 0.38/0.80 (assume @p28 (= (tptp.succ tptp.tptp_minus_1) tptp.n0)) % 0.38/0.80 (assume @p29 (forall @t9 (= (tptp.plus @t2 tptp.n1) @t18))) % 0.38/0.80 (assume @p30 (forall @t9 (= (tptp.plus tptp.n1 @t2) @t18))) % 0.38/0.80 (assume @p31 (forall @t9 (= (tptp.plus @t2 tptp.n2) @t67))) % 0.38/0.80 (assume @p32 (forall @t9 (= (tptp.plus tptp.n2 @t2) @t67))) % 0.38/0.80 (assume @p33 (forall @t9 (= (tptp.plus @t2 tptp.n3) @t68))) % 0.38/0.80 (assume @p34 (forall @t9 (= (tptp.plus tptp.n3 @t2) @t68))) % 0.38/0.80 (assume @p35 (forall @t9 (= (tptp.plus @t2 tptp.n4) @t69))) % 0.38/0.80 (assume @p36 (forall @t9 (= (tptp.plus tptp.n4 @t2) @t69))) % 0.38/0.80 (assume @p37 (forall @t9 (= (tptp.plus @t2 tptp.n5) @t70))) % 0.38/0.80 (assume @p38 (forall @t9 (= (tptp.plus tptp.n5 @t2) @t70))) % 0.38/0.80 (assume @p39 @t72) % 0.38/0.80 (assume @p40 @t74) % 0.38/0.80 (assume @p41 (forall @t9 (= (tptp.succ @t71) @t2))) % 0.38/0.80 (assume @p42 (forall @t6 (= (tptp.leq @t18 @t19) @t12))) % 0.38/0.80 (assume @p43 (forall @t6 (=> (tptp.leq @t18 @t1) @t4))) % 0.38/0.80 (assume @p44 (forall @t6 (=> (tptp.leq (tptp.minus @t2 @t1) @t2) (tptp.leq tptp.n0 @t1)))) % 0.38/0.80 (assume @p45 (forall (@list @t2 @t26 @t75 @t46) (= (tptp.a_select3 @t76 @t26 @t75) @t46))) % 0.38/0.80 (assume @p46 (forall (@list @t25 @t29 @t26 @t75 @t2 @t46 @t77) (=> (and @t78 (= @t29 @t75) (= (tptp.a_select3 @t2 @t26 @t75) @t46)) (= (tptp.a_select3 (tptp.tptp_update3 @t2 @t25 @t29 @t77) @t26 @t75) @t46)))) % 0.38/0.80 (assume @p47 (forall (@list @t25 @t29 @t26 @t75 @t2 @t46) (=> (and (forall (@list @t80 @t79) (=> (and @t82 (tptp.leq tptp.n0 @t79) @t81 (tptp.leq @t79 @t75)) (= (tptp.a_select3 @t2 @t80 @t79) @t46))) @t40 @t28 @t38 (tptp.leq @t29 @t75)) (= (tptp.a_select3 @t76 @t25 @t29) @t46)))) % 0.38/0.80 (assume @p48 (forall (@list @t2 @t26 @t46) (= (tptp.a_select2 @t83 @t26) @t46))) % 0.38/0.80 (assume @p49 (forall (@list @t25 @t26 @t2 @t46 @t77) (=> (and @t78 (= (tptp.a_select2 @t2 @t26) @t46)) (= (tptp.a_select2 (tptp.tptp_update2 @t2 @t25 @t77) @t26) @t46)))) % 0.38/0.80 (assume @p50 (forall (@list @t25 @t26 @t2 @t46) (=> (and (forall (@list @t80) (=> (and @t82 @t81) (= (tptp.a_select2 @t2 @t80) @t46))) @t40 @t28) (= (tptp.a_select2 @t83 @t25) @t46)))) % 0.38/0.80 (assume @p51 tptp.true) % 0.38/0.80 (assume @p52 (not (= tptp.def tptp.use))) % 0.38/0.80 (assume @p53 @t169) % 0.38/0.80 (assume @p54 @t170) % 0.38/0.80 (assume @p55 (tptp.gt tptp.n588 tptp.n4)) % 0.38/0.80 (assume @p56 @t171) % 0.38/0.80 (assume @p57 (tptp.gt tptp.n6 tptp.n4)) % 0.38/0.80 (assume @p58 @t172) % 0.38/0.80 (assume @p59 (tptp.gt tptp.n1000 tptp.n4)) % 0.38/0.80 (assume @p60 (tptp.gt tptp.n588 tptp.n5)) % 0.38/0.80 (assume @p61 @t173) % 0.38/0.80 (assume @p62 @t174) % 0.38/0.80 (assume @p63 (tptp.gt tptp.n1000 tptp.n5)) % 0.38/0.80 (assume @p64 (tptp.gt tptp.n588 tptp.n6)) % 0.38/0.80 (assume @p65 @t175) % 0.38/0.80 (assume @p66 (tptp.gt tptp.n1000 tptp.n6)) % 0.38/0.80 (assume @p67 (tptp.gt tptp.n588 tptp.n7)) % 0.38/0.80 (assume @p68 (tptp.gt tptp.n1000 tptp.n7)) % 0.38/0.80 (assume @p69 (tptp.gt tptp.n588 tptp.tptp_minus_1)) % 0.38/0.80 (assume @p70 (tptp.gt tptp.n4 tptp.tptp_minus_1)) % 0.38/0.80 (assume @p71 (tptp.gt tptp.n5 tptp.tptp_minus_1)) % 0.38/0.80 (assume @p72 (tptp.gt tptp.n6 tptp.tptp_minus_1)) % 0.38/0.80 (assume @p73 (tptp.gt tptp.n7 tptp.tptp_minus_1)) % 0.38/0.80 (assume @p74 (tptp.gt tptp.n0 tptp.tptp_minus_1)) % 0.38/0.80 (assume @p75 (tptp.gt tptp.n1 tptp.tptp_minus_1)) % 0.38/0.80 (assume @p76 (tptp.gt tptp.n2 tptp.tptp_minus_1)) % 0.38/0.80 (assume @p77 (tptp.gt tptp.n1000 tptp.tptp_minus_1)) % 0.38/0.80 (assume @p78 (tptp.gt tptp.n3 tptp.tptp_minus_1)) % 0.38/0.80 (assume @p79 (tptp.gt tptp.n588 tptp.n0)) % 0.38/0.80 (assume @p80 @t176) % 0.38/0.80 (assume @p81 @t177) % 0.38/0.80 (assume @p82 @t178) % 0.38/0.80 (assume @p83 (tptp.gt tptp.n7 tptp.n0)) % 0.38/0.80 (assume @p84 @t179) % 0.38/0.80 (assume @p85 @t180) % 0.38/0.80 (assume @p86 (tptp.gt tptp.n1000 tptp.n0)) % 0.38/0.80 (assume @p87 @t181) % 0.38/0.80 (assume @p88 (tptp.gt tptp.n588 tptp.n1)) % 0.38/0.80 (assume @p89 (tptp.gt tptp.n4 tptp.n1)) % 0.38/0.80 (assume @p90 @t182) % 0.38/0.80 (assume @p91 (tptp.gt tptp.n6 tptp.n1)) % 0.38/0.80 (assume @p92 @t183) % 0.38/0.80 (assume @p93 (tptp.gt tptp.n2 tptp.n1)) % 0.38/0.80 (assume @p94 (tptp.gt tptp.n1000 tptp.n1)) % 0.38/0.80 (assume @p95 @t184) % 0.38/0.80 (assume @p96 (tptp.gt tptp.n588 tptp.n2)) % 0.38/0.80 (assume @p97 (tptp.gt tptp.n4 tptp.n2)) % 0.38/0.80 (assume @p98 @t185) % 0.38/0.80 (assume @p99 (tptp.gt tptp.n6 tptp.n2)) % 0.38/0.80 (assume @p100 @t186) % 0.38/0.80 (assume @p101 (tptp.gt tptp.n1000 tptp.n2)) % 0.38/0.80 (assume @p102 @t187) % 0.38/0.80 (assume @p103 (tptp.gt tptp.n588 tptp.n3)) % 0.38/0.80 (assume @p104 @t188) % 0.38/0.80 (assume @p105 @t189) % 0.38/0.80 (assume @p106 (tptp.gt tptp.n6 tptp.n3)) % 0.38/0.80 (assume @p107 @t190) % 0.38/0.80 (assume @p108 (tptp.gt tptp.n1000 tptp.n3)) % 0.38/0.80 (assume @p109 (forall @t9 (=> (and @t22 (tptp.leq @t2 tptp.n4)) (or @t195 @t194 @t193 @t192 @t191)))) % 0.38/0.80 (assume @p110 (forall @t9 (=> (and @t22 (tptp.leq @t2 tptp.n5)) (or @t195 @t194 @t193 @t192 @t191 @t196)))) % 0.38/0.80 (assume @p111 (forall @t9 (=> (and @t22 (tptp.leq @t2 tptp.n6)) (or @t195 @t194 @t193 @t192 @t191 @t196 (= @t2 tptp.n6))))) % 0.38/0.80 (assume @p112 (forall @t9 (=> (and @t22 (tptp.leq @t2 tptp.n0)) @t195))) % 0.38/0.80 (assume @p113 (forall @t9 (=> (and @t22 (tptp.leq @t2 tptp.n1)) (or @t195 @t194)))) % 0.38/0.80 (assume @p114 (forall @t9 (=> (and @t22 (tptp.leq @t2 tptp.n2)) (or @t195 @t194 @t193)))) % 0.38/0.80 (assume @p115 (forall @t9 (=> (and @t22 (tptp.leq @t2 tptp.n3)) (or @t195 @t194 @t193 @t192)))) % 0.38/0.80 (assume @p116 (= @t200 tptp.n4)) % 0.38/0.80 (assume @p117 (= @t201 tptp.n5)) % 0.38/0.80 (assume @p118 (= @t202 tptp.n6)) % 0.38/0.80 (assume @p119 (= @t197 tptp.n1)) % 0.38/0.80 (assume @p120 (= @t198 tptp.n2)) % 0.38/0.80 (assume @p121 (= @t199 tptp.n3)) % 0.38/0.80 (assume @p122 true) % 0.38/0.80 (step @p123 :rule cnf_or_neg :args (@t205 2)) % 0.38/0.80 (step @p124 :rule chain_m_resolution :premises (@p123 @p51) :args (@t205 @t206 @t207)) % 0.38/0.80 (step @p125 :rule cnf_or_neg :args (@t211 3)) % 0.38/0.80 (step @p126 :rule chain_m_resolution :premises (@p125 @p51) :args (@t211 @t206 @t207)) % 0.38/0.80 (step @p127 :rule cnf_or_neg :args (@t215 3)) % 0.38/0.80 (step @p128 :rule chain_m_resolution :premises (@p127 @p51) :args (@t215 @t206 @t207)) % 0.38/0.80 (step @p129 :rule bool-double-not-elim :args (@t99)) % 0.38/0.80 (step @p130 :rule refl :args (@t216)) % 0.38/0.80 (step @p131 :rule nary_cong :premises (@p130 @p129) :args ((or @t216 @t217))) % 0.38/0.80 (step @p132 :rule cnf_or_neg :args (@t216 0)) % 0.38/0.80 (step @p133 :rule eq_resolve :premises (@p132 @p131)) % 0.38/0.80 (step @p134 :rule reordering :premises (@p133) :args ((or @t99 @t216))) % 0.38/0.80 (step @p135 :rule bool-double-not-elim :args (@t98)) % 0.38/0.80 (step @p136 :rule nary_cong :premises (@p130 @p135) :args ((or @t216 @t218))) % 0.38/0.80 (step @p137 :rule cnf_or_neg :args (@t216 1)) % 0.38/0.80 (step @p138 :rule eq_resolve :premises (@p137 @p136)) % 0.38/0.80 (step @p139 :rule reordering :premises (@p138) :args ((or @t98 @t216))) % 0.38/0.80 (step @p140 :rule cnf_or_neg :args (@t216 2)) % 0.38/0.80 (step @p141 :rule reordering :premises (@p140) :args ((or @t219 @t216))) % 0.38/0.80 (step @p142 :rule cnf_and_neg :args (@t100)) % 0.38/0.80 (step @p143 :rule chain_m_resolution :premises (@p142 @p141 @p139 @p134) :args (@t216 @t220 (@list @t100 @t98 @t99))) % 0.38/0.80 (step @p144 :rule eq-symm :args (@t16 @t4)) % 0.38/0.80 (step @p145 :rule cong :premises (@p144) :args (@t17)) % 0.38/0.80 (step @p146 :rule eq_resolve :premises (@p10 @p145)) % 0.38/0.80 (step @p147 :rule instantiate :premises (@p146) :args ((@list tptp.n588 tptp.n1000))) % 0.38/0.80 (step @p148 :rule cnf_equiv_pos1 :args (@t223)) % 0.38/0.80 (step @p149 :rule reordering :premises (@p148) :args ((or (not @t170) @t222 (not @t223)))) % 0.38/0.80 (step @p150 :rule chain_m_resolution :premises (@p149 @p54 @p147) :args (@t222 @t224 (@list @t170 @t223))) % 0.38/0.80 (step @p151 :rule aci_norm :args ((= (or (or @t226 @t225) @t10) @t227))) % 0.38/0.80 (step @p152 :rule refl :args (@t10)) % 0.38/0.80 (step @p153 :rule bool-and-de-morgan :args (@t12 @t11 true)) % 0.38/0.80 (step @p154 :rule nary_cong :premises (@p153 @p152) :args ((or (not @t13) @t10))) % 0.38/0.80 (step @p155 :rule trans :premises (@p154 @p151)) % 0.38/0.80 (step @p156 :rule bool-impl-elim :args (@t13 @t10)) % 0.38/0.80 (step @p157 :rule trans :premises (@p156 @p155)) % 0.38/0.80 (step @p158 :rule cong :premises (@p157) :args (@t14)) % 0.38/0.80 (step @p159 :rule eq_resolve :premises (@p5 @p158)) % 0.38/0.80 (step @p160 :rule instantiate :premises (@p159) :args ((@list tptp.pv5 tptp.n588 @t221))) % 0.38/0.80 (step @p161 :rule cnf_or_pos :args (@t230)) % 0.38/0.80 (step @p162 :rule reordering :premises (@p161) :args ((or @t203 @t229 @t228 (not @t230)))) % 0.38/0.80 (step @p163 :rule refl :args (@t233)) % 0.38/0.80 (step @p164 :rule nary_cong :premises (@p163 @p129) :args ((or @t233 @t217))) % 0.38/0.80 (step @p165 :rule cnf_or_neg :args (@t233 0)) % 0.38/0.80 (step @p166 :rule eq_resolve :premises (@p165 @p164)) % 0.38/0.80 (step @p167 :rule reordering :premises (@p166) :args ((or @t99 @t233))) % 0.38/0.80 (step @p168 :rule refl :args (@t241)) % 0.38/0.80 (step @p169 :rule nary_cong :premises (@p168 @p129) :args ((or @t241 @t217))) % 0.38/0.80 (step @p170 :rule cnf_or_neg :args (@t241 0)) % 0.38/0.80 (step @p171 :rule eq_resolve :premises (@p170 @p169)) % 0.38/0.80 (step @p172 :rule reordering :premises (@p171) :args ((or @t99 @t241))) % 0.38/0.80 (step @p173 :rule refl :args (@t242)) % 0.38/0.80 (step @p174 :rule nary_cong :premises (@p173 @p129) :args ((or @t242 @t217))) % 0.38/0.80 (step @p175 :rule cnf_or_neg :args (@t242 0)) % 0.38/0.80 (step @p176 :rule eq_resolve :premises (@p175 @p174)) % 0.38/0.80 (step @p177 :rule reordering :premises (@p176) :args ((or @t99 @t242))) % 0.38/0.80 (step @p178 :rule refl :args (@t243)) % 0.38/0.80 (step @p179 :rule nary_cong :premises (@p178 @p129) :args ((or @t243 @t217))) % 0.38/0.80 (step @p180 :rule cnf_or_neg :args (@t243 0)) % 0.38/0.80 (step @p181 :rule eq_resolve :premises (@p180 @p179)) % 0.38/0.80 (step @p182 :rule reordering :premises (@p181) :args ((or @t99 @t243))) % 0.38/0.80 (step @p183 :rule refl :args (@t259)) % 0.38/0.80 (step @p184 :rule nary_cong :premises (@p183 @p129) :args ((or @t259 @t217))) % 0.38/0.80 (step @p185 :rule cnf_or_neg :args (@t259 0)) % 0.38/0.80 (step @p186 :rule eq_resolve :premises (@p185 @p184)) % 0.38/0.80 (step @p187 :rule reordering :premises (@p186) :args ((or @t99 @t259))) % 0.38/0.80 (step @p188 :rule instantiate :premises (@p4) :args ((@list tptp.n7))) % 0.38/0.80 (step @p189 :rule bool-impl-elim :args (@t4 @t12)) % 0.38/0.80 (step @p190 :rule cong :premises (@p189) :args (@t15)) % 0.38/0.80 (step @p191 :rule eq_resolve :premises (@p8 @p190)) % 0.38/0.80 (step @p192 :rule instantiate :premises (@p191) :args ((@list tptp.n6 tptp.n7))) % 0.38/0.80 (step @p193 :rule cnf_or_pos :args (@t261)) % 0.38/0.80 (step @p194 :rule reordering :premises (@p193) :args ((or @t103 @t260 (not @t261)))) % 0.38/0.80 (step @p195 :rule chain_m_resolution :premises (@p194 @p65 @p192) :args (@t103 @t224 (@list @t175 @t261))) % 0.38/0.80 (step @p196 :rule instantiate :premises (@p146) :args ((@list tptp.n5 tptp.n6))) % 0.38/0.80 (step @p197 :rule cnf_equiv_pos1 :args (@t264)) % 0.38/0.80 (step @p198 :rule reordering :premises (@p197) :args ((or (not @t173) @t263 (not @t264)))) % 0.38/0.80 (step @p199 :rule chain_m_resolution :premises (@p198 @p61 @p196) :args (@t263 @t224 (@list @t173 @t264))) % 0.38/0.80 (step @p200 :rule true_intro :premises (@p199)) % 0.38/0.80 (step @p201 :rule instantiate :premises (@p39) :args ((@list tptp.n6))) % 0.38/0.80 (step @p202 :rule refl :args (tptp.n5)) % 0.38/0.80 (step @p203 :rule cong :premises (@p202 @p201) :args (@t104)) % 0.38/0.80 (step @p204 :rule trans :premises (@p203 @p200)) % 0.38/0.80 (step @p205 :rule true_elim :premises (@p204)) % 0.38/0.80 (step @p206 :rule instantiate :premises (@p191) :args ((@list tptp.n5 tptp.n7))) % 0.38/0.80 (step @p207 :rule cnf_or_pos :args (@t266)) % 0.38/0.80 (step @p208 :rule reordering :premises (@p207) :args ((or @t105 @t265 (not @t266)))) % 0.38/0.80 (step @p209 :rule chain_m_resolution :premises (@p208 @p62 @p206) :args (@t105 @t224 (@list @t174 @t266))) % 0.38/0.80 (step @p210 :rule instantiate :premises (@p191) :args ((@list tptp.n4 tptp.n5))) % 0.38/0.80 (step @p211 :rule cnf_or_pos :args (@t269)) % 0.38/0.80 (step @p212 :rule reordering :premises (@p211) :args ((or @t268 @t267 (not @t269)))) % 0.38/0.80 (step @p213 :rule chain_m_resolution :premises (@p212 @p56 @p210) :args (@t267 @t224 (@list @t171 @t269))) % 0.38/0.80 (step @p214 :rule true_intro :premises (@p213)) % 0.38/0.80 (step @p215 :rule refl :args (tptp.n4)) % 0.38/0.80 (step @p216 :rule cong :premises (@p215 @p117) :args ((tptp.leq tptp.n4 @t201))) % 0.38/0.80 (step @p217 :rule eq-symm :args (@t73 @t2)) % 0.38/0.80 (step @p218 :rule cong :premises (@p217) :args (@t74)) % 0.38/0.80 (step @p219 :rule eq_resolve :premises (@p40 @p218)) % 0.38/0.80 (step @p220 :rule instantiate :premises (@p219) :args ((@list @t201))) % 0.38/0.80 (step @p221 :rule symm :premises (@p220)) % 0.38/0.80 (step @p222 :rule symm :premises (@p118)) % 0.38/0.80 (step @p223 :rule cong :premises (@p222) :args (@t262)) % 0.38/0.80 (step @p224 :rule trans :premises (@p223 @p221)) % 0.38/0.80 (step @p225 :rule cong :premises (@p215 @p224) :args ((tptp.leq tptp.n4 @t262))) % 0.38/0.80 (step @p226 :rule cong :premises (@p215 @p201) :args (@t106)) % 0.38/0.80 (step @p227 :rule trans :premises (@p226 @p225 @p216 @p214)) % 0.38/0.80 (step @p228 :rule true_elim :premises (@p227)) % 0.38/0.80 (step @p229 :rule instantiate :premises (@p191) :args ((@list tptp.n4 tptp.n7))) % 0.38/0.80 (step @p230 :rule cnf_or_pos :args (@t271)) % 0.38/0.80 (step @p231 :rule reordering :premises (@p230) :args ((or @t107 @t270 (not @t271)))) % 0.38/0.80 (step @p232 :rule chain_m_resolution :premises (@p231 @p58 @p229) :args (@t107 @t224 (@list @t172 @t271))) % 0.38/0.80 (step @p233 :rule instantiate :premises (@p191) :args ((@list tptp.n3 tptp.n5))) % 0.38/0.80 (step @p234 :rule cnf_or_pos :args (@t274)) % 0.38/0.80 (step @p235 :rule reordering :premises (@p234) :args ((or @t273 @t272 (not @t274)))) % 0.38/0.80 (step @p236 :rule chain_m_resolution :premises (@p235 @p105 @p233) :args (@t272 @t224 (@list @t189 @t274))) % 0.38/0.80 (step @p237 :rule true_intro :premises (@p236)) % 0.38/0.80 (step @p238 :rule refl :args (tptp.n3)) % 0.38/0.80 (step @p239 :rule cong :premises (@p238 @p117) :args ((tptp.leq tptp.n3 @t201))) % 0.38/0.80 (step @p240 :rule cong :premises (@p238 @p224) :args ((tptp.leq tptp.n3 @t262))) % 0.38/0.80 (step @p241 :rule cong :premises (@p238 @p201) :args (@t108)) % 0.38/0.80 (step @p242 :rule trans :premises (@p241 @p240 @p239 @p237)) % 0.38/0.80 (step @p243 :rule true_elim :premises (@p242)) % 0.38/0.80 (step @p244 :rule instantiate :premises (@p146) :args ((@list tptp.n3 tptp.n4))) % 0.38/0.80 (step @p245 :rule cnf_equiv_pos1 :args (@t277)) % 0.38/0.80 (step @p246 :rule reordering :premises (@p245) :args ((or (not @t188) @t276 (not @t277)))) % 0.38/0.80 (step @p247 :rule chain_m_resolution :premises (@p246 @p104 @p244) :args (@t276 @t224 (@list @t188 @t277))) % 0.38/0.80 (step @p248 :rule true_intro :premises (@p247)) % 0.38/0.80 (step @p249 :rule instantiate :premises (@p39) :args ((@list tptp.n4))) % 0.38/0.80 (step @p250 :rule cong :premises (@p238 @p249) :args (@t109)) % 0.38/0.80 (step @p251 :rule trans :premises (@p250 @p248)) % 0.38/0.80 (step @p252 :rule true_elim :premises (@p251)) % 0.38/0.80 (step @p253 :rule instantiate :premises (@p191) :args ((@list tptp.n3 tptp.n7))) % 0.38/0.80 (step @p254 :rule cnf_or_pos :args (@t279)) % 0.38/0.80 (step @p255 :rule reordering :premises (@p254) :args ((or @t110 @t278 (not @t279)))) % 0.38/0.80 (step @p256 :rule chain_m_resolution :premises (@p255 @p107 @p253) :args (@t110 @t224 (@list @t190 @t279))) % 0.38/0.80 (step @p257 :rule instantiate :premises (@p191) :args ((@list tptp.n2 tptp.n5))) % 0.38/0.80 (step @p258 :rule cnf_or_pos :args (@t282)) % 0.38/0.80 (step @p259 :rule reordering :premises (@p258) :args ((or @t281 @t280 (not @t282)))) % 0.38/0.80 (step @p260 :rule chain_m_resolution :premises (@p259 @p98 @p257) :args (@t280 @t224 (@list @t185 @t282))) % 0.38/0.80 (step @p261 :rule true_intro :premises (@p260)) % 0.38/0.80 (step @p262 :rule refl :args (tptp.n2)) % 0.38/0.80 (step @p263 :rule cong :premises (@p262 @p117) :args ((tptp.leq tptp.n2 @t201))) % 0.38/0.80 (step @p264 :rule cong :premises (@p262 @p224) :args ((tptp.leq tptp.n2 @t262))) % 0.38/0.80 (step @p265 :rule cong :premises (@p262 @p201) :args (@t111)) % 0.38/0.80 (step @p266 :rule trans :premises (@p265 @p264 @p263 @p261)) % 0.38/0.80 (step @p267 :rule true_elim :premises (@p266)) % 0.38/0.80 (step @p268 :rule instantiate :premises (@p191) :args ((@list tptp.n2 tptp.n3))) % 0.38/0.80 (step @p269 :rule cnf_or_pos :args (@t285)) % 0.38/0.80 (step @p270 :rule reordering :premises (@p269) :args ((or @t284 @t283 (not @t285)))) % 0.38/0.80 (step @p271 :rule chain_m_resolution :premises (@p270 @p102 @p268) :args (@t283 @t224 (@list @t187 @t285))) % 0.38/0.80 (step @p272 :rule true_intro :premises (@p271)) % 0.38/0.80 (step @p273 :rule cong :premises (@p262 @p121) :args ((tptp.leq tptp.n2 @t199))) % 0.38/0.80 (step @p274 :rule instantiate :premises (@p219) :args ((@list @t199))) % 0.38/0.80 (step @p275 :rule symm :premises (@p274)) % 0.38/0.80 (step @p276 :rule symm :premises (@p116)) % 0.38/0.80 (step @p277 :rule cong :premises (@p276) :args (@t275)) % 0.38/0.80 (step @p278 :rule trans :premises (@p277 @p275)) % 0.38/0.80 (step @p279 :rule cong :premises (@p262 @p278) :args ((tptp.leq tptp.n2 @t275))) % 0.38/0.80 (step @p280 :rule cong :premises (@p262 @p249) :args (@t112)) % 0.38/0.80 (step @p281 :rule trans :premises (@p280 @p279 @p273 @p272)) % 0.38/0.80 (step @p282 :rule true_elim :premises (@p281)) % 0.38/0.80 (step @p283 :rule instantiate :premises (@p191) :args ((@list tptp.n2 tptp.n7))) % 0.38/0.80 (step @p284 :rule cnf_or_pos :args (@t287)) % 0.38/0.80 (step @p285 :rule reordering :premises (@p284) :args ((or @t113 @t286 (not @t287)))) % 0.38/0.80 (step @p286 :rule chain_m_resolution :premises (@p285 @p100 @p283) :args (@t113 @t224 (@list @t186 @t287))) % 0.38/0.80 (step @p287 :rule instantiate :premises (@p191) :args ((@list tptp.n1 tptp.n5))) % 0.38/0.80 (step @p288 :rule cnf_or_pos :args (@t290)) % 0.38/0.80 (step @p289 :rule reordering :premises (@p288) :args ((or @t289 @t288 (not @t290)))) % 0.38/0.80 (step @p290 :rule chain_m_resolution :premises (@p289 @p90 @p287) :args (@t288 @t224 (@list @t182 @t290))) % 0.38/0.80 (step @p291 :rule true_intro :premises (@p290)) % 0.38/0.80 (step @p292 :rule refl :args (tptp.n1)) % 0.38/0.80 (step @p293 :rule cong :premises (@p292 @p117) :args ((tptp.leq tptp.n1 @t201))) % 0.38/0.80 (step @p294 :rule cong :premises (@p292 @p224) :args ((tptp.leq tptp.n1 @t262))) % 0.38/0.80 (step @p295 :rule cong :premises (@p292 @p201) :args (@t114)) % 0.38/0.80 (step @p296 :rule trans :premises (@p295 @p294 @p293 @p291)) % 0.38/0.80 (step @p297 :rule true_elim :premises (@p296)) % 0.38/0.80 (step @p298 :rule instantiate :premises (@p191) :args ((@list tptp.n1 tptp.n3))) % 0.38/0.80 (step @p299 :rule cnf_or_pos :args (@t293)) % 0.38/0.80 (step @p300 :rule reordering :premises (@p299) :args ((or @t292 @t291 (not @t293)))) % 0.38/0.80 (step @p301 :rule chain_m_resolution :premises (@p300 @p95 @p298) :args (@t291 @t224 (@list @t184 @t293))) % 0.38/0.80 (step @p302 :rule true_intro :premises (@p301)) % 0.38/0.80 (step @p303 :rule cong :premises (@p292 @p121) :args ((tptp.leq tptp.n1 @t199))) % 0.38/0.80 (step @p304 :rule cong :premises (@p292 @p278) :args ((tptp.leq tptp.n1 @t275))) % 0.38/0.80 (step @p305 :rule cong :premises (@p292 @p249) :args (@t115)) % 0.38/0.80 (step @p306 :rule trans :premises (@p305 @p304 @p303 @p302)) % 0.38/0.80 (step @p307 :rule true_elim :premises (@p306)) % 0.38/0.80 (step @p308 :rule instantiate :premises (@p191) :args ((@list tptp.n1 tptp.n7))) % 0.38/0.80 (step @p309 :rule cnf_or_pos :args (@t295)) % 0.38/0.80 (step @p310 :rule reordering :premises (@p309) :args ((or @t116 @t294 (not @t295)))) % 0.38/0.80 (step @p311 :rule chain_m_resolution :premises (@p310 @p92 @p308) :args (@t116 @t224 (@list @t183 @t295))) % 0.38/0.80 (step @p312 :rule instantiate :premises (@p7) :args ((@list @t84 tptp.n0))) % 0.38/0.80 (step @p313 :rule quant-unused-vars :args ((= (forall @t166 @t299) @t299))) % 0.38/0.80 (step @p314 :rule aci_norm :args ((= (or (or @t298 @t212) @t297) @t299))) % 0.38/0.80 (step @p315 :rule refl :args (@t297)) % 0.38/0.80 (step @p316 :rule bool-and-de-morgan :args (@t163 @t85 true)) % 0.38/0.80 (step @p317 :rule nary_cong :premises (@p316 @p315) :args ((or (not @t164) @t297))) % 0.38/0.80 (step @p318 :rule trans :premises (@p317 @p314)) % 0.38/0.80 (step @p319 :rule bool-impl-elim :args (@t164 @t297)) % 0.38/0.80 (step @p320 :rule trans :premises (@p319 @p318)) % 0.38/0.80 (step @p321 :rule cong :premises (@p320) :args ((forall @t166 (=> @t164 @t297)))) % 0.38/0.80 (step @p322 :rule trans :premises (@p321 @p313)) % 0.38/0.80 (step @p323 :rule quant-unused-vars :args ((= (forall @t161 @t297) @t297))) % 0.38/0.80 (step @p324 :rule aci_norm :args ((= @t300 @t297))) % 0.38/0.80 (step @p325 :rule cong :premises (@p324) :args ((forall @t161 @t300))) % 0.38/0.80 (step @p326 :rule trans :premises (@p325 @p323)) % 0.38/0.80 (step @p327 :rule aci_norm :args ((= (or @t214 @t215) @t215))) % 0.38/0.80 (step @p328 :rule aci_norm :args ((= (or @t214 @t301) @t215))) % 0.38/0.80 (step @p329 :rule aci_norm :args ((= (or (or @t213 @t212) tptp.true) @t301))) % 0.38/0.80 (step @p330 :rule refl :args (tptp.true)) % 0.38/0.80 (step @p331 :rule bool-and-de-morgan :args (@t87 @t85 true)) % 0.38/0.80 (step @p332 :rule nary_cong :premises (@p331 @p330) :args ((or (not @t88) tptp.true))) % 0.38/0.80 (step @p333 :rule trans :premises (@p332 @p329)) % 0.38/0.80 (step @p334 :rule bool-impl-elim :args (@t88 tptp.true)) % 0.38/0.80 (step @p335 :rule trans :premises (@p334 @p333)) % 0.38/0.80 (step @p336 :rule refl :args (@t214)) % 0.38/0.80 (step @p337 :rule nary_cong :premises (@p336 @p335) :args ((or @t214 @t89))) % 0.38/0.80 (step @p338 :rule trans :premises (@p337 @p328)) % 0.38/0.80 (step @p339 :rule bool-impl-elim :args (@t91 @t89)) % 0.38/0.80 (step @p340 :rule trans :premises (@p339 @p338)) % 0.38/0.80 (step @p341 :rule nary_cong :premises (@p336 @p340) :args ((or @t214 @t92))) % 0.38/0.80 (step @p342 :rule trans :premises (@p341 @p327)) % 0.38/0.80 (step @p343 :rule bool-impl-elim :args (@t91 @t92)) % 0.38/0.80 (step @p344 :rule trans :premises (@p343 @p342)) % 0.38/0.80 (step @p345 :rule aci_norm :args ((= (or (or @t210 @t209) (or @t208 tptp.true)) @t211))) % 0.38/0.80 (step @p346 :rule bool-impl-elim :args (@t93 tptp.true)) % 0.38/0.80 (step @p347 :rule bool-and-de-morgan :args (@t96 @t95 true)) % 0.38/0.80 (step @p348 :rule nary_cong :premises (@p347 @p346) :args ((or (not @t97) @t94))) % 0.38/0.80 (step @p349 :rule trans :premises (@p348 @p345)) % 0.38/0.80 (step @p350 :rule bool-impl-elim :args (@t97 @t94)) % 0.38/0.80 (step @p351 :rule trans :premises (@p350 @p349)) % 0.38/0.80 (step @p352 :rule aci_norm :args ((= (or @t302 @t100) @t216))) % 0.38/0.80 (step @p353 :rule refl :args (@t100)) % 0.38/0.80 (step @p354 :rule bool-and-de-morgan :args (@t99 @t98 true)) % 0.38/0.80 (step @p355 :rule nary_cong :premises (@p354 @p353) :args ((or @t219 @t100))) % 0.38/0.80 (step @p356 :rule trans :premises (@p355 @p352)) % 0.38/0.80 (step @p357 :rule bool-impl-elim :args (@t100 @t100)) % 0.38/0.80 (step @p358 :rule trans :premises (@p357 @p356)) % 0.38/0.80 (step @p359 :rule aci_norm :args ((= (or @t302 @t258) @t259))) % 0.38/0.80 (step @p360 :rule bool-impl-elim :args (@t128 @t127)) % 0.38/0.80 (step @p361 :rule refl :args (@t130)) % 0.38/0.80 (step @p362 :rule bool-double-not-elim :args (@t128)) % 0.38/0.80 (step @p363 :rule nary_cong :premises (@p362 @p361) :args ((or @t303 @t130))) % 0.38/0.80 (step @p364 :rule bool-impl-elim :args (@t131 @t130)) % 0.38/0.80 (step @p365 :rule trans :premises (@p364 @p363)) % 0.38/0.80 (step @p366 :rule refl :args (@t101)) % 0.38/0.80 (step @p367 :rule refl :args (@t109)) % 0.38/0.80 (step @p368 :rule refl :args (@t112)) % 0.38/0.80 (step @p369 :rule refl :args (@t115)) % 0.38/0.80 (step @p370 :rule refl :args (@t118)) % 0.38/0.80 (step @p371 :rule refl :args (@t99)) % 0.38/0.80 (step @p372 :rule refl :args (@t123)) % 0.38/0.80 (step @p373 :rule refl :args (@t124)) % 0.38/0.80 (step @p374 :rule refl :args (@t125)) % 0.38/0.80 (step @p375 :rule refl :args (@t126)) % 0.38/0.80 (step @p376 :rule nary_cong :premises (@p375 @p374 @p373 @p372 @p371 @p370 @p369 @p368 @p367 @p366 @p365 @p360) :args (@t133)) % 0.38/0.80 (step @p377 :rule refl :args (@t131)) % 0.38/0.80 (step @p378 :rule nary_cong :premises (@p377 @p376) :args ((or @t131 @t133))) % 0.38/0.80 (step @p379 :rule bool-impl-elim :args (@t128 @t133)) % 0.38/0.80 (step @p380 :rule trans :premises (@p379 @p378)) % 0.38/0.80 (step @p381 :rule nary_cong :premises (@p365 @p360) :args (@t135)) % 0.38/0.80 (step @p382 :rule refl :args (@t128)) % 0.38/0.80 (step @p383 :rule nary_cong :premises (@p382 @p381) :args ((or @t128 @t135))) % 0.38/0.80 (step @p384 :rule refl :args (@t135)) % 0.38/0.80 (step @p385 :rule nary_cong :premises (@p362 @p384) :args ((or @t303 @t135))) % 0.38/0.80 (step @p386 :rule bool-impl-elim :args (@t131 @t135)) % 0.38/0.80 (step @p387 :rule trans :premises (@p386 @p385)) % 0.38/0.80 (step @p388 :rule trans :premises (@p387 @p383)) % 0.38/0.80 (step @p389 :rule refl :args (@t102)) % 0.38/0.80 (step @p390 :rule refl :args (@t103)) % 0.38/0.80 (step @p391 :rule refl :args (@t105)) % 0.38/0.80 (step @p392 :rule refl :args (@t107)) % 0.38/0.80 (step @p393 :rule refl :args (@t108)) % 0.38/0.80 (step @p394 :rule refl :args (@t110)) % 0.38/0.80 (step @p395 :rule refl :args (@t113)) % 0.38/0.80 (step @p396 :rule refl :args (@t116)) % 0.38/0.80 (step @p397 :rule refl :args (@t117)) % 0.38/0.80 (step @p398 :rule refl :args (@t119)) % 0.38/0.80 (step @p399 :rule refl :args (@t120)) % 0.38/0.80 (step @p400 :rule refl :args (@t121)) % 0.38/0.80 (step @p401 :rule refl :args (@t122)) % 0.38/0.80 (step @p402 :rule nary_cong :premises (@p375 @p374 @p373 @p372 @p401 @p400 @p399 @p398 @p371 @p397 @p396 @p395 @p394 @p393 @p392 @p391 @p390 @p389 @p366 @p388 @p380) :args (@t137)) % 0.38/0.80 (step @p403 :rule nary_cong :premises (@p377 @p402) :args ((or @t131 @t137))) % 0.38/0.80 (step @p404 :rule bool-impl-elim :args (@t128 @t137)) % 0.38/0.80 (step @p405 :rule trans :premises (@p404 @p403)) % 0.38/0.80 (step @p406 :rule nary_cong :premises (@p388 @p380) :args (@t139)) % 0.38/0.80 (step @p407 :rule nary_cong :premises (@p382 @p406) :args ((or @t128 @t139))) % 0.38/0.80 (step @p408 :rule refl :args (@t139)) % 0.38/0.80 (step @p409 :rule nary_cong :premises (@p362 @p408) :args ((or @t303 @t139))) % 0.38/0.80 (step @p410 :rule bool-impl-elim :args (@t131 @t139)) % 0.38/0.80 (step @p411 :rule trans :premises (@p410 @p409)) % 0.38/0.80 (step @p412 :rule trans :premises (@p411 @p407)) % 0.38/0.80 (step @p413 :rule refl :args (@t104)) % 0.38/0.80 (step @p414 :rule refl :args (@t106)) % 0.38/0.80 (step @p415 :rule refl :args (@t111)) % 0.38/0.80 (step @p416 :rule refl :args (@t114)) % 0.38/0.80 (step @p417 :rule nary_cong :premises (@p375 @p374 @p373 @p372 @p401 @p400 @p399 @p398 @p371 @p397 @p396 @p416 @p395 @p415 @p394 @p392 @p414 @p391 @p413 @p390 @p389 @p366 @p412 @p405) :args (@t141)) % 0.38/0.80 (step @p418 :rule nary_cong :premises (@p377 @p417) :args ((or @t131 @t141))) % 0.38/0.80 (step @p419 :rule bool-impl-elim :args (@t128 @t141)) % 0.38/0.80 (step @p420 :rule trans :premises (@p419 @p418)) % 0.38/0.80 (step @p421 :rule nary_cong :premises (@p412 @p405) :args (@t142)) % 0.38/0.80 (step @p422 :rule nary_cong :premises (@p382 @p421) :args ((or @t128 @t142))) % 0.38/0.80 (step @p423 :rule refl :args (@t142)) % 0.38/0.80 (step @p424 :rule nary_cong :premises (@p362 @p423) :args ((or @t303 @t142))) % 0.38/0.80 (step @p425 :rule bool-impl-elim :args (@t131 @t142)) % 0.38/0.80 (step @p426 :rule trans :premises (@p425 @p424)) % 0.38/0.80 (step @p427 :rule trans :premises (@p426 @p422)) % 0.38/0.80 (step @p428 :rule nary_cong :premises (@p375 @p374 @p373 @p372 @p371 @p370 @p397 @p369 @p416 @p368 @p415 @p367 @p366 @p427 @p420) :args (@t143)) % 0.38/0.80 (step @p429 :rule nary_cong :premises (@p354 @p428) :args ((or @t219 @t143))) % 0.38/0.80 (step @p430 :rule trans :premises (@p429 @p359)) % 0.38/0.80 (step @p431 :rule bool-impl-elim :args (@t100 @t143)) % 0.38/0.80 (step @p432 :rule trans :premises (@p431 @p430)) % 0.38/0.80 (step @p433 :rule aci_norm :args ((= (or @t302 tptp.true) @t205))) % 0.38/0.80 (step @p434 :rule nary_cong :premises (@p354 @p330) :args ((or @t219 tptp.true))) % 0.38/0.80 (step @p435 :rule trans :premises (@p434 @p433)) % 0.38/0.80 (step @p436 :rule bool-impl-elim :args (@t100 tptp.true)) % 0.38/0.80 (step @p437 :rule trans :premises (@p436 @p435)) % 0.38/0.80 (step @p438 :rule aci_norm :args ((= (or @t304 @t100) @t243))) % 0.38/0.80 (step @p439 :rule aci_norm :args ((= (or @t204 (or @t240 (or @t203 @t238))) @t304))) % 0.38/0.80 (step @p440 :rule bool-and-de-morgan :args (@t98 @t144 true)) % 0.38/0.80 (step @p441 :rule refl :args (@t240)) % 0.38/0.80 (step @p442 :rule nary_cong :premises (@p441 @p440) :args ((or @t240 (not (and @t98 @t144))))) % 0.38/0.80 (step @p443 :rule bool-and-de-morgan :args (@t145 @t98 (and @t144))) % 0.38/0.80 (step @p444 :rule trans :premises (@p443 @p442)) % 0.38/0.80 (step @p445 :rule refl :args (@t204)) % 0.38/0.80 (step @p446 :rule nary_cong :premises (@p445 @p444) :args ((or @t204 (not (and @t145 @t98 @t144))))) % 0.38/0.80 (step @p447 :rule bool-and-de-morgan :args (@t99 @t145 (and @t98 @t144))) % 0.38/0.80 (step @p448 :rule trans :premises (@p447 @p446)) % 0.38/0.80 (step @p449 :rule trans :premises (@p448 @p439)) % 0.38/0.80 (step @p450 :rule nary_cong :premises (@p449 @p353) :args ((or @t305 @t100))) % 0.38/0.80 (step @p451 :rule trans :premises (@p450 @p438)) % 0.38/0.80 (step @p452 :rule bool-impl-elim :args (@t146 @t100)) % 0.38/0.80 (step @p453 :rule trans :premises (@p452 @p451)) % 0.38/0.80 (step @p454 :rule aci_norm :args ((= (or @t304 @t146) @t242))) % 0.38/0.80 (step @p455 :rule refl :args (@t146)) % 0.38/0.80 (step @p456 :rule nary_cong :premises (@p449 @p455) :args ((or @t305 @t146))) % 0.38/0.80 (step @p457 :rule trans :premises (@p456 @p454)) % 0.38/0.80 (step @p458 :rule bool-impl-elim :args (@t146 @t146)) % 0.38/0.80 (step @p459 :rule trans :premises (@p458 @p457)) % 0.38/0.80 (step @p460 :rule aci_norm :args ((= (or @t306 @t236) @t241))) % 0.38/0.80 (step @p461 :rule bool-impl-elim :args (@t150 @t149)) % 0.38/0.80 (step @p462 :rule refl :args (@t149)) % 0.38/0.80 (step @p463 :rule bool-double-not-elim :args (@t150)) % 0.38/0.80 (step @p464 :rule nary_cong :premises (@p463 @p462) :args ((or (not @t151) @t149))) % 0.38/0.80 (step @p465 :rule bool-impl-elim :args (@t151 @t149)) % 0.38/0.80 (step @p466 :rule trans :premises (@p465 @p464)) % 0.38/0.80 (step @p467 :rule nary_cong :premises (@p466 @p461) :args (@t152)) % 0.38/0.80 (step @p468 :rule aci_norm :args ((= (or @t204 (or @t240 (or @t239 (or @t203 (or @t238 @t237))))) @t306))) % 0.38/0.80 (step @p469 :rule bool-and-de-morgan :args (@t144 @t147 true)) % 0.38/0.80 (step @p470 :rule refl :args (@t203)) % 0.38/0.80 (step @p471 :rule nary_cong :premises (@p470 @p469) :args ((or @t203 (not (and @t144 @t147))))) % 0.38/0.80 (step @p472 :rule bool-and-de-morgan :args (@t98 @t144 (and @t147))) % 0.38/0.80 (step @p473 :rule trans :premises (@p472 @p471)) % 0.38/0.80 (step @p474 :rule refl :args (@t239)) % 0.38/0.80 (step @p475 :rule nary_cong :premises (@p474 @p473) :args ((or @t239 (not (and @t98 @t144 @t147))))) % 0.38/0.80 (step @p476 :rule bool-and-de-morgan :args (@t148 @t98 (and @t144 @t147))) % 0.38/0.80 (step @p477 :rule trans :premises (@p476 @p475)) % 0.38/0.80 (step @p478 :rule nary_cong :premises (@p441 @p477) :args ((or @t240 (not (and @t148 @t98 @t144 @t147))))) % 0.38/0.80 (step @p479 :rule bool-and-de-morgan :args (@t145 @t148 (and @t98 @t144 @t147))) % 0.38/0.80 (step @p480 :rule trans :premises (@p479 @p478)) % 0.38/0.80 (step @p481 :rule nary_cong :premises (@p445 @p480) :args ((or @t204 (not (and @t145 @t148 @t98 @t144 @t147))))) % 0.38/0.80 (step @p482 :rule bool-and-de-morgan :args (@t99 @t145 (and @t148 @t98 @t144 @t147))) % 0.38/0.80 (step @p483 :rule trans :premises (@p482 @p481)) % 0.38/0.80 (step @p484 :rule trans :premises (@p483 @p468)) % 0.38/0.80 (step @p485 :rule nary_cong :premises (@p484 @p467) :args ((or @t307 @t152))) % 0.38/0.80 (step @p486 :rule trans :premises (@p485 @p460)) % 0.38/0.80 (step @p487 :rule bool-impl-elim :args (@t149 @t152)) % 0.38/0.80 (step @p488 :rule trans :premises (@p487 @p486)) % 0.38/0.80 (step @p489 :rule aci_norm :args ((= (or @t308 @t156) @t233))) % 0.38/0.80 (step @p490 :rule refl :args (@t156)) % 0.38/0.80 (step @p491 :rule aci_norm :args ((= (or @t204 (or @t232 (or @t203 @t231))) @t308))) % 0.38/0.80 (step @p492 :rule bool-and-de-morgan :args (@t98 @t153 true)) % 0.38/0.80 (step @p493 :rule refl :args (@t232)) % 0.38/0.80 (step @p494 :rule nary_cong :premises (@p493 @p492) :args ((or @t232 (not (and @t98 @t153))))) % 0.38/0.80 (step @p495 :rule bool-and-de-morgan :args (@t155 @t98 (and @t153))) % 0.38/0.80 (step @p496 :rule trans :premises (@p495 @p494)) % 0.38/0.80 (step @p497 :rule nary_cong :premises (@p445 @p496) :args ((or @t204 (not (and @t155 @t98 @t153))))) % 0.38/0.80 (step @p498 :rule bool-and-de-morgan :args (@t99 @t155 (and @t98 @t153))) % 0.38/0.80 (step @p499 :rule trans :premises (@p498 @p497)) % 0.38/0.80 (step @p500 :rule trans :premises (@p499 @p491)) % 0.38/0.80 (step @p501 :rule nary_cong :premises (@p500 @p490) :args ((or (not @t157) @t156))) % 0.38/0.80 (step @p502 :rule trans :premises (@p501 @p489)) % 0.38/0.80 (step @p503 :rule bool-impl-elim :args (@t157 @t156)) % 0.38/0.80 (step @p504 :rule trans :premises (@p503 @p502)) % 0.38/0.80 (step @p505 :rule bool-impl-elim :args (tptp.true @t159)) % 0.38/0.80 (step @p506 :rule bool-or-taut2 :args (false tptp.true false false)) % 0.38/0.80 (step @p507 :rule bool-impl-elim :args (tptp.true tptp.true)) % 0.38/0.80 (step @p508 :rule trans :premises (@p507 @p506)) % 0.38/0.80 (step @p509 :rule nary_cong :premises (@p508 @p505 @p504 @p488 @p459 @p453 @p437 @p432 @p358 @p351 @p344) :args (@t160)) % 0.38/0.80 (step @p510 :rule cong :premises (@p509) :args (@t162)) % 0.38/0.80 (step @p511 :rule trans :premises (@p510 @p326)) % 0.38/0.80 (step @p512 :rule refl :args (@t164)) % 0.38/0.80 (step @p513 :rule cong :premises (@p512 @p511) :args (@t165)) % 0.38/0.80 (step @p514 :rule cong :premises (@p513) :args (@t167)) % 0.38/0.80 (step @p515 :rule trans :premises (@p514 @p322)) % 0.38/0.80 (step @p516 :rule refl :args (@t88)) % 0.38/0.80 (step @p517 :rule cong :premises (@p516 @p515) :args (@t168)) % 0.38/0.80 (step @p518 :rule cong :premises (@p517) :args (@t169)) % 0.38/0.80 (step @p519 :rule eq_resolve :premises (@p53 @p518)) % 0.38/0.80 (step @p520 :rule not_implies_elim1 :premises (@p519)) % 0.38/0.80 (step @p521 :rule and_elim :premises (@p520) :args (1)) % 0.38/0.80 (step @p522 :rule cnf_equiv_pos1 :args (@t309)) % 0.38/0.80 (step @p523 :rule reordering :premises (@p522) :args ((or @t158 @t212 (not @t309)))) % 0.38/0.80 (step @p524 :rule chain_m_resolution :premises (@p523 @p521 @p312) :args (@t158 @t224 (@list @t85 @t309))) % 0.38/0.80 (step @p525 :rule instantiate :premises (@p191) :args ((@list tptp.n0 tptp.n5))) % 0.38/0.80 (step @p526 :rule cnf_or_pos :args (@t311)) % 0.38/0.80 (step @p527 :rule reordering :premises (@p526) :args ((or @t121 @t310 (not @t311)))) % 0.38/0.80 (step @p528 :rule chain_m_resolution :premises (@p527 @p81 @p525) :args (@t121 @t224 (@list @t177 @t311))) % 0.38/0.80 (step @p529 :rule true_intro :premises (@p528)) % 0.38/0.80 (step @p530 :rule trans :premises (@p223 @p221 @p117)) % 0.38/0.80 (step @p531 :rule refl :args (tptp.n0)) % 0.38/0.80 (step @p532 :rule cong :premises (@p531 @p530) :args ((tptp.leq tptp.n0 @t262))) % 0.38/0.80 (step @p533 :rule cong :premises (@p531 @p201) :args (@t117)) % 0.38/0.80 (step @p534 :rule trans :premises (@p533 @p532 @p529)) % 0.38/0.80 (step @p535 :rule true_elim :premises (@p534)) % 0.38/0.80 (step @p536 :rule instantiate :premises (@p7) :args ((@list @t86 tptp.n0))) % 0.38/0.80 (step @p537 :rule and_elim :premises (@p520) :args (0)) % 0.38/0.80 (step @p538 :rule cnf_equiv_pos1 :args (@t312)) % 0.38/0.80 (step @p539 :rule reordering :premises (@p538) :args ((or @t118 @t213 (not @t312)))) % 0.38/0.80 (step @p540 :rule chain_m_resolution :premises (@p539 @p537 @p536) :args (@t118 @t224 (@list @t87 @t312))) % 0.38/0.80 (step @p541 :rule instantiate :premises (@p7) :args ((@list tptp.n7 tptp.n0))) % 0.38/0.80 (step @p542 :rule not_implies_elim2 :premises (@p519)) % 0.38/0.80 (step @p543 :rule not_or_elim :premises (@p542) :args (0)) % 0.38/0.80 (step @p544 :rule not_not_elim :premises (@p543)) % 0.38/0.80 (step @p545 :rule cnf_equiv_pos1 :args (@t313)) % 0.38/0.80 (step @p546 :rule reordering :premises (@p545) :args ((or @t119 @t298 (not @t313)))) % 0.38/0.80 (step @p547 :rule chain_m_resolution :premises (@p546 @p544 @p541) :args (@t119 @t224 (@list @t163 @t313))) % 0.38/0.80 (step @p548 :rule instantiate :premises (@p191) :args ((@list tptp.n0 tptp.n6))) % 0.38/0.80 (step @p549 :rule cnf_or_pos :args (@t315)) % 0.38/0.80 (step @p550 :rule reordering :premises (@p549) :args ((or @t120 @t314 (not @t315)))) % 0.38/0.80 (step @p551 :rule chain_m_resolution :premises (@p550 @p82 @p548) :args (@t120 @t224 (@list @t178 @t315))) % 0.38/0.80 (step @p552 :rule instantiate :premises (@p191) :args ((@list tptp.n0 tptp.n4))) % 0.38/0.80 (step @p553 :rule cnf_or_pos :args (@t317)) % 0.38/0.80 (step @p554 :rule reordering :premises (@p553) :args ((or @t122 @t316 (not @t317)))) % 0.38/0.80 (step @p555 :rule chain_m_resolution :premises (@p554 @p80 @p552) :args (@t122 @t224 (@list @t176 @t317))) % 0.38/0.80 (step @p556 :rule instantiate :premises (@p191) :args ((@list tptp.n0 tptp.n3))) % 0.38/0.80 (step @p557 :rule cnf_or_pos :args (@t319)) % 0.38/0.80 (step @p558 :rule reordering :premises (@p557) :args ((or @t123 @t318 (not @t319)))) % 0.38/0.80 (step @p559 :rule chain_m_resolution :premises (@p558 @p87 @p556) :args (@t123 @t224 (@list @t181 @t319))) % 0.38/0.80 (step @p560 :rule instantiate :premises (@p191) :args ((@list tptp.n0 tptp.n2))) % 0.38/0.80 (step @p561 :rule cnf_or_pos :args (@t321)) % 0.38/0.80 (step @p562 :rule reordering :premises (@p561) :args ((or @t124 @t320 (not @t321)))) % 0.38/0.80 (step @p563 :rule chain_m_resolution :premises (@p562 @p85 @p560) :args (@t124 @t224 (@list @t180 @t321))) % 0.38/0.80 (step @p564 :rule instantiate :premises (@p191) :args ((@list tptp.n0 tptp.n1))) % 0.38/0.80 (step @p565 :rule cnf_or_pos :args (@t323)) % 0.38/0.80 (step @p566 :rule reordering :premises (@p565) :args ((or @t125 @t322 (not @t323)))) % 0.38/0.80 (step @p567 :rule chain_m_resolution :premises (@p566 @p84 @p564) :args (@t125 @t224 (@list @t179 @t323))) % 0.38/0.80 (step @p568 :rule instantiate :premises (@p4) :args ((@list tptp.n0))) % 0.38/0.80 (step @p569 :rule cnf_and_neg :args (@t159)) % 0.38/0.80 (step @p570 :rule chain_m_resolution :premises (@p569 @p568 @p567 @p563 @p559 @p555 @p528 @p551 @p547 @p540 @p535 @p524 @p311 @p307 @p297 @p286 @p282 @p267 @p256 @p252 @p243 @p232 @p228 @p209 @p205 @p195 @p188) :args (@t159 (@list 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 @t126 @t125 @t124 @t123 @t122 @t121 @t120 @t119 @t118 @t117 @t158 @t116 @t115 @t114 @t113 @t112 @t111 @t110 @t109 @t108 @t107 @t106 @t105 @t104 @t103 @t102))) % 0.38/0.80 (step @p571 :rule cnf_or_neg :args (@t296 1)) % 0.38/0.80 (step @p572 :rule chain_m_resolution :premises (@p571 @p570) :args (@t296 @t206 (@list @t159))) % 0.38/0.80 (step @p573 :rule not_or_elim :premises (@p542) :args (2)) % 0.38/0.80 (step @p574 :rule not_and :premises (@p573)) % 0.38/0.80 (step @p575 :rule chain_m_resolution :premises (@p574 @p572 @p143 @p128 @p126 @p124 @p187 @p182 @p177 @p172 @p167) :args (@t99 @t324 (@list @t296 @t216 @t215 @t211 @t205 @t259 @t243 @t242 @t241 @t233))) % 0.38/0.80 (assume-push @p761 @t325) % 0.38/0.80 (step-pop @p762 :rule scope :premises (@p160)) % 0.38/0.80 (step @p577 :rule process_scope :premises (@p762) :args (@t230)) % 0.38/0.80 (step @p579 :rule implies_elim :premises (@p577)) % 0.38/0.80 (assume-push @p763 @t326) % 0.38/0.80 (step-pop @p764 :rule scope :premises (@p147)) % 0.38/0.80 (step @p581 :rule process_scope :premises (@p764) :args (@t223)) % 0.38/0.80 (step @p583 :rule implies_elim :premises (@p581)) % 0.38/0.80 (assume-push @p765 @t72) % 0.38/0.80 (step @p585 :rule instantiate :premises (@p39) :args (@t327)) % 0.38/0.80 (step-pop @p766 :rule scope :premises (@p585)) % 0.38/0.80 (step @p586 :rule process_scope :premises (@p766) :args (@t328)) % 0.38/0.80 (step @p588 :rule implies_elim :premises (@p586)) % 0.38/0.80 (assume-push @p767 @t328) % 0.38/0.80 (assume-push @p768 @t228) % 0.38/0.80 (assume-push @p769 @t228) % 0.38/0.80 (assume-push @p770 @t328) % 0.38/0.80 (step @p593 :rule true_intro :premises (@p768)) % 0.38/0.80 (step @p585 :rule instantiate :premises (@p39) :args (@t327)) % 0.38/0.80 (step @p594 :rule refl :args (tptp.pv5)) % 0.38/0.80 (step @p595 :rule cong :premises (@p594 @p585) :args (@t101)) % 0.38/0.80 (step @p596 :rule trans :premises (@p595 @p593)) % 0.38/0.80 (step @p597 :rule true_elim :premises (@p596)) % 0.38/0.80 (step-pop @p771 :rule scope :premises (@p597)) % 0.38/0.80 (step-pop @p772 :rule scope :premises (@p771)) % 0.38/0.80 (step @p598 :rule process_scope :premises (@p772) :args (@t101)) % 0.38/0.80 (step @p585 :rule instantiate :premises (@p39) :args (@t327)) % 0.38/0.80 (step @p601 :rule and_intro :premises (@p768 @p585)) % 0.38/0.80 (step @p602 :rule modus_ponens :premises (@p601 @p598)) % 0.38/0.80 (step-pop @p773 :rule scope :premises (@p602)) % 0.38/0.80 (step-pop @p774 :rule scope :premises (@p773)) % 0.38/0.80 (step @p603 :rule process_scope :premises (@p774) :args (@t101)) % 0.38/0.80 (step @p606 :rule implies_elim :premises (@p603)) % 0.38/0.80 (step @p607 :rule cnf_and_neg :args (@t329)) % 0.38/0.80 (step @p608 :rule resolution :premises (@p607 @p606) :args (true @t329)) % 0.38/0.80 (step @p609 :rule reordering :premises (@p608) :args ((or @t101 (not @t328) (not @t228)))) % 0.38/0.80 (step @p610 :rule bool-double-not-elim :args (@t145)) % 0.38/0.80 (step @p611 :rule nary_cong :premises (@p173 @p610) :args ((or @t242 @t330))) % 0.38/0.80 (step @p612 :rule cnf_or_neg :args (@t242 1)) % 0.38/0.80 (step @p613 :rule eq_resolve :premises (@p612 @p611)) % 0.38/0.80 (step @p614 :rule reordering :premises (@p613) :args ((or @t145 @t242))) % 0.38/0.80 (step @p615 :rule bool-double-not-elim :args (@t144)) % 0.38/0.80 (step @p616 :rule nary_cong :premises (@p173 @p615) :args ((or @t242 @t331))) % 0.38/0.80 (step @p617 :rule cnf_or_neg :args (@t242 3)) % 0.38/0.80 (step @p618 :rule eq_resolve :premises (@p617 @p616)) % 0.38/0.80 (step @p619 :rule reordering :premises (@p618) :args ((or @t144 @t242))) % 0.38/0.80 (step @p620 :rule cnf_or_neg :args (@t242 4)) % 0.38/0.80 (step @p621 :rule reordering :premises (@p620) :args ((or @t305 @t242))) % 0.38/0.80 (step @p622 :rule cnf_and_neg :args (@t146)) % 0.38/0.80 (step @p623 :rule reordering :premises (@p622) :args ((or @t146 @t204 @t203 @t240 @t238))) % 0.38/0.80 (step @p624 :rule chain_m_resolution :premises (@p623 @p621 @p619 @p614) :args ((or @t204 @t203 @t242) @t220 (@list @t146 @t144 @t145))) % 0.38/0.80 (step @p625 :rule cnf_and_neg :args (@t127)) % 0.38/0.80 (step @p626 :rule reordering :premises (@p625) :args ((or @t127 @t204 @t203 @t357 @t356 @t355 @t354 @t353 @t352 @t351 @t350 @t349 @t348 @t347 @t346 @t345 @t344 @t343 @t342 @t341 @t340 @t339 @t338 @t337 @t336 @t335 @t334 @t333 @t332))) % 0.38/0.80 (step @p627 :rule cnf_and_neg :args (@t130)) % 0.38/0.80 (step @p628 :rule reordering :premises (@p627) :args ((or @t130 @t204 @t203 @t357 @t356 @t355 @t354 @t353 @t352 @t351 @t350 @t348 @t347 @t345 @t344 @t342 @t341 @t339 @t338 @t337 @t336 @t335 @t334 @t333 @t332))) % 0.38/0.80 (step @p629 :rule cnf_or_neg :args (@t243 4)) % 0.38/0.80 (step @p630 :rule reordering :premises (@p629) :args ((or @t219 @t243))) % 0.38/0.80 (step @p631 :rule cnf_or_neg :args (@t244 1)) % 0.38/0.80 (step @p632 :rule cnf_or_neg :args (@t245 1)) % 0.38/0.80 (step @p633 :rule cnf_and_neg :args (@t248)) % 0.38/0.80 (step @p634 :rule cnf_and_neg :args (@t246)) % 0.38/0.80 (step @p635 :rule reordering :premises (@p634) :args ((or @t204 @t246 @t357 @t356 @t355 @t354 @t349 @t346 @t343 @t340 @t332 (not @t245) (not @t244)))) % 0.38/0.80 (step @p636 :rule cnf_or_neg :args (@t249 1)) % 0.38/0.80 (step @p637 :rule cnf_or_neg :args (@t247 1)) % 0.38/0.80 (step @p638 :rule cnf_and_neg :args (@t252)) % 0.38/0.80 (step @p639 :rule cnf_and_neg :args (@t250)) % 0.38/0.80 (step @p640 :rule reordering :premises (@p639) :args ((or @t204 @t250 @t357 @t356 @t355 @t354 @t353 @t352 @t351 @t350 @t348 @t347 @t344 @t341 @t339 @t338 @t336 @t334 @t333 @t332 (not @t249) (not @t247)))) % 0.38/0.80 (step @p641 :rule cnf_or_neg :args (@t253 1)) % 0.38/0.80 (step @p642 :rule cnf_or_neg :args (@t251 1)) % 0.38/0.80 (step @p643 :rule cnf_and_neg :args (@t256)) % 0.38/0.80 (step @p644 :rule cnf_and_neg :args (@t254)) % 0.38/0.80 (step @p645 :rule reordering :premises (@p644) :args ((or @t204 @t254 @t357 @t356 @t355 @t354 @t353 @t352 @t351 @t350 @t348 @t347 @t345 @t344 @t342 @t341 @t338 @t337 @t336 @t335 @t334 @t333 @t332 (not @t253) (not @t251)))) % 0.38/0.80 (step @p646 :rule cnf_or_neg :args (@t257 1)) % 0.38/0.80 (step @p647 :rule cnf_or_neg :args (@t255 1)) % 0.38/0.80 (step @p648 :rule cnf_and_neg :args (@t258)) % 0.38/0.80 (step @p649 :rule reordering :premises (@p648) :args ((or @t204 @t258 @t357 @t356 @t355 @t354 @t349 @t348 @t346 @t345 @t343 @t342 @t340 @t332 (not @t257) (not @t255)))) % 0.38/0.80 (step @p650 :rule cnf_or_neg :args (@t259 2)) % 0.38/0.80 (step @p651 :rule bool-double-not-elim :args (@t155)) % 0.38/0.80 (step @p652 :rule nary_cong :premises (@p163 @p651) :args ((or @t233 (not @t232)))) % 0.38/0.80 (step @p653 :rule cnf_or_neg :args (@t233 1)) % 0.38/0.80 (step @p654 :rule eq_resolve :premises (@p653 @p652)) % 0.38/0.80 (step @p655 :rule reordering :premises (@p654) :args ((or @t155 @t233))) % 0.38/0.80 (step @p656 :rule bool-double-not-elim :args (@t153)) % 0.38/0.80 (step @p657 :rule nary_cong :premises (@p163 @p656) :args ((or @t233 (not @t231)))) % 0.38/0.80 (step @p658 :rule cnf_or_neg :args (@t233 3)) % 0.38/0.80 (step @p659 :rule eq_resolve :premises (@p658 @p657)) % 0.38/0.80 (step @p660 :rule reordering :premises (@p659) :args ((or @t153 @t233))) % 0.38/0.80 (step @p661 :rule cnf_or_neg :args (@t233 4)) % 0.38/0.80 (step @p662 :rule cnf_and_neg :args (@t156)) % 0.38/0.80 (step @p663 :rule reordering :premises (@p662) :args ((or @t156 @t204 @t203 @t232 @t231 @t357 (not @t154)))) % 0.38/0.80 (step @p664 :rule symm :premises (@p117)) % 0.38/0.80 (assume-push @p775 @t153) % 0.38/0.80 (assume-push @p776 @t358) % 0.38/0.80 (assume-push @p777 @t359) % 0.38/0.80 (assume-push @p778 @t360) % 0.38/0.80 (assume-push @p779 @t362) % 0.38/0.80 (assume-push @p780 @t153) % 0.38/0.80 (assume-push @p781 @t360) % 0.38/0.80 (assume-push @p782 @t359) % 0.38/0.80 (assume-push @p783 @t362) % 0.38/0.80 (assume-push @p784 @t358) % 0.38/0.80 (step @p675 :rule true_intro :premises (@p775)) % 0.38/0.80 (step @p676 :rule symm :premises (@p201)) % 0.38/0.80 (step @p677 :rule cong :premises (@p118) :args (@t361)) % 0.38/0.80 (step @p678 :rule trans :premises (@p664 @p220 @p677 @p676)) % 0.38/0.80 (step @p679 :rule refl :args (tptp.pv21)) % 0.38/0.80 (step @p680 :rule cong :premises (@p679 @p678) :args (@t154)) % 0.38/0.80 (step @p681 :rule trans :premises (@p680 @p675)) % 0.38/0.80 (step @p682 :rule true_elim :premises (@p681)) % 0.38/0.80 (step-pop @p785 :rule scope :premises (@p682)) % 0.38/0.80 (step-pop @p786 :rule scope :premises (@p785)) % 0.38/0.80 (step-pop @p787 :rule scope :premises (@p786)) % 0.38/0.80 (step-pop @p788 :rule scope :premises (@p787)) % 0.38/0.80 (step-pop @p789 :rule scope :premises (@p788)) % 0.38/0.80 (step @p683 :rule process_scope :premises (@p789) :args (@t154)) % 0.38/0.80 (step @p689 :rule and_intro :premises (@p775 @p201 @p222 @p220 @p664)) % 0.38/0.80 (step @p690 :rule modus_ponens :premises (@p689 @p683)) % 0.38/0.80 (step-pop @p790 :rule scope :premises (@p690)) % 0.38/0.80 (step-pop @p791 :rule scope :premises (@p790)) % 0.38/0.80 (step-pop @p792 :rule scope :premises (@p791)) % 0.38/0.80 (step-pop @p793 :rule scope :premises (@p792)) % 0.38/0.80 (step-pop @p794 :rule scope :premises (@p793)) % 0.38/0.80 (step @p691 :rule process_scope :premises (@p794) :args (@t154)) % 0.38/0.80 (step @p697 :rule implies_elim :premises (@p691)) % 0.38/0.80 (step @p698 :rule cnf_and_neg :args (@t363)) % 0.38/0.80 (step @p699 :rule resolution :premises (@p698 @p697) :args (true @t363)) % 0.38/0.80 (step @p700 :rule reordering :premises (@p699) :args ((or @t154 @t231 (not @t358) (not @t359) (not @t360) (not @t362)))) % 0.38/0.80 (step @p701 :rule chain_m_resolution :premises (@p700 @p220 @p201 @p222 @p664 @p663 @p568 @p661 @p660 @p655) :args ((or @t204 @t203 @t233) (@list false false false false true false true false false) (@list @t362 @t360 @t359 @t358 @t154 @t126 @t156 @t153 @t155))) % 0.38/0.80 (step @p702 :rule nary_cong :premises (@p168 @p615) :args ((or @t241 @t331))) % 0.38/0.80 (step @p703 :rule cnf_or_neg :args (@t241 4)) % 0.38/0.80 (step @p704 :rule eq_resolve :premises (@p703 @p702)) % 0.38/0.80 (step @p705 :rule reordering :premises (@p704) :args ((or @t144 @t241))) % 0.38/0.80 (step @p706 :rule bool-double-not-elim :args (@t148)) % 0.38/0.80 (step @p707 :rule nary_cong :premises (@p168 @p706) :args ((or @t241 (not @t239)))) % 0.38/0.80 (step @p708 :rule cnf_or_neg :args (@t241 2)) % 0.38/0.80 (step @p709 :rule eq_resolve :premises (@p708 @p707)) % 0.38/0.80 (step @p710 :rule reordering :premises (@p709) :args ((or @t148 @t241))) % 0.38/0.80 (step @p711 :rule bool-double-not-elim :args (@t147)) % 0.38/0.80 (step @p712 :rule nary_cong :premises (@p168 @p711) :args ((or @t241 (not @t237)))) % 0.38/0.80 (step @p713 :rule cnf_or_neg :args (@t241 5)) % 0.38/0.80 (step @p714 :rule eq_resolve :premises (@p713 @p712)) % 0.38/0.80 (step @p715 :rule reordering :premises (@p714) :args ((or @t147 @t241))) % 0.38/0.80 (step @p716 :rule cnf_or_neg :args (@t241 6)) % 0.38/0.80 (step @p717 :rule cnf_and_neg :args (@t149)) % 0.38/0.80 (step @p718 :rule reordering :premises (@p717) :args ((or @t149 @t204 @t203 @t240 @t238 @t239 @t237))) % 0.38/0.80 (step @p719 :rule cnf_or_neg :args (@t235 1)) % 0.38/0.80 (step @p720 :rule reordering :premises (@p719) :args ((or @t307 @t235))) % 0.38/0.80 (step @p721 :rule cnf_or_neg :args (@t234 1)) % 0.38/0.80 (step @p722 :rule reordering :premises (@p721) :args ((or @t307 @t234))) % 0.38/0.80 (step @p723 :rule cnf_and_neg :args (@t236)) % 0.38/0.80 (step @p724 :rule chain_m_resolution :premises (@p723 @p722 @p720 @p718 @p716 @p715 @p710) :args ((or @t204 @t203 @t240 @t238 @t241) (@list false false false true false false) (@list @t234 @t235 @t149 @t236 @t147 @t148))) % 0.38/0.80 (step @p725 :rule chain_m_resolution :premises (@p724 @p705 @p574 @p572 @p143 @p128 @p126 @p124 @p701 @p650 @p649 @p568 @p559 @p540 @p567 @p563 @p297 @p282 @p267 @p252 @p307 @p535 @p647 @p646 @p645 @p568 @p559 @p555 @p528 @p551 @p547 @p567 @p311 @p563 @p286 @p267 @p256 @p232 @p228 @p209 @p205 @p195 @p188 @p535 @p297 @p643 @p642 @p641 @p640 @p568 @p559 @p555 @p528 @p551 @p547 @p567 @p311 @p286 @p256 @p563 @p232 @p209 @p195 @p188 @p535 @p243 @p638 @p637 @p636 @p635 @p568 @p559 @p540 @p567 @p563 @p252 @p307 @p282 @p633 @p632 @p631 @p630 @p628 @p568 @p559 @p555 @p528 @p551 @p547 @p567 @p311 @p563 @p286 @p267 @p256 @p243 @p232 @p228 @p209 @p205 @p195 @p188 @p535 @p297 @p626 @p568 @p559 @p555 @p528 @p551 @p547 @p540 @p567 @p311 @p563 @p297 @p286 @p282 @p267 @p256 @p252 @p243 @p232 @p228 @p209 @p205 @p195 @p188 @p307 @p535 @p624 @p142 @p609 @p588 @p39 @p162 @p149 @p54 @p583 @p146 @p579 @p159) :args ((or @t204 @t203 @t240) (@list false 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 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 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 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 @t144 @t241 @t296 @t216 @t215 @t211 @t205 @t233 @t259 @t258 @t126 @t123 @t118 @t125 @t124 @t114 @t112 @t111 @t109 @t115 @t117 @t255 @t257 @t254 @t126 @t123 @t122 @t121 @t120 @t119 @t125 @t116 @t124 @t113 @t111 @t110 @t107 @t106 @t105 @t104 @t103 @t102 @t117 @t114 @t256 @t251 @t253 @t250 @t126 @t123 @t122 @t121 @t120 @t119 @t125 @t116 @t113 @t110 @t124 @t107 @t105 @t103 @t102 @t117 @t108 @t252 @t247 @t249 @t246 @t126 @t123 @t118 @t125 @t124 @t109 @t115 @t112 @t248 @t245 @t244 @t243 @t130 @t126 @t123 @t122 @t121 @t120 @t119 @t125 @t116 @t124 @t113 @t111 @t110 @t108 @t107 @t106 @t105 @t104 @t103 @t102 @t117 @t114 @t127 @t126 @t123 @t122 @t121 @t120 @t119 @t118 @t125 @t116 @t124 @t114 @t113 @t112 @t111 @t110 @t109 @t108 @t107 @t106 @t105 @t104 @t103 @t102 @t115 @t117 @t242 @t100 @t101 @t328 @t72 @t228 @t222 @t170 @t223 @t326 @t230 @t325))) % 0.38/0.80 (step @p585 :rule instantiate :premises (@p39) :args (@t327)) % 0.38/0.80 (step @p726 :rule nary_cong :premises (@p168 @p610) :args ((or @t241 @t330))) % 0.38/0.80 (step @p727 :rule cnf_or_neg :args (@t241 1)) % 0.38/0.80 (step @p728 :rule eq_resolve :premises (@p727 @p726)) % 0.38/0.80 (step @p729 :rule reordering :premises (@p728) :args ((or @t145 @t241))) % 0.38/0.80 (step @p730 :rule nary_cong :premises (@p178 @p610) :args ((or @t243 @t330))) % 0.38/0.80 (step @p731 :rule cnf_or_neg :args (@t243 1)) % 0.38/0.80 (step @p732 :rule eq_resolve :premises (@p731 @p730)) % 0.38/0.80 (step @p733 :rule reordering :premises (@p732) :args ((or @t145 @t243))) % 0.38/0.80 (step @p734 :rule chain_m_resolution :premises (@p649 @p568 @p559 @p540 @p567 @p563 @p297 @p282 @p267 @p252 @p307 @p535 @p575 @p647 @p646 @p645 @p568 @p559 @p555 @p528 @p551 @p547 @p567 @p311 @p563 @p286 @p267 @p256 @p232 @p228 @p209 @p205 @p195 @p188 @p535 @p297 @p575 @p643 @p642 @p641 @p640 @p568 @p559 @p555 @p528 @p551 @p547 @p567 @p311 @p286 @p256 @p563 @p232 @p209 @p195 @p188 @p535 @p243 @p575 @p638 @p637 @p636 @p635 @p568 @p559 @p540 @p567 @p563 @p252 @p307 @p282 @p575 @p633 @p650 @p632 @p631 @p574 @p572 @p143 @p128 @p126 @p124 @p628 @p568 @p559 @p555 @p528 @p551 @p547 @p567 @p311 @p563 @p286 @p267 @p256 @p243 @p232 @p228 @p209 @p205 @p195 @p188 @p535 @p297 @p575 @p626 @p568 @p559 @p555 @p528 @p551 @p547 @p540 @p567 @p311 @p563 @p297 @p286 @p282 @p267 @p256 @p252 @p243 @p232 @p228 @p209 @p205 @p195 @p188 @p307 @p535 @p575 @p733 @p729 @p609 @p585 @p701 @p575 @p624 @p575 @p725 @p575 @p162 @p160 @p150) :args (@t203 (@list 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 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 false false true false false 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 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 true false false false false) (@list @t126 @t123 @t118 @t125 @t124 @t114 @t112 @t111 @t109 @t115 @t117 @t99 @t255 @t257 @t254 @t126 @t123 @t122 @t121 @t120 @t119 @t125 @t116 @t124 @t113 @t111 @t110 @t107 @t106 @t105 @t104 @t103 @t102 @t117 @t114 @t99 @t256 @t251 @t253 @t250 @t126 @t123 @t122 @t121 @t120 @t119 @t125 @t116 @t113 @t110 @t124 @t107 @t105 @t103 @t102 @t117 @t108 @t99 @t252 @t247 @t249 @t246 @t126 @t123 @t118 @t125 @t124 @t109 @t115 @t112 @t99 @t248 @t258 @t245 @t244 @t259 @t296 @t216 @t215 @t211 @t205 @t130 @t126 @t123 @t122 @t121 @t120 @t119 @t125 @t116 @t124 @t113 @t111 @t110 @t108 @t107 @t106 @t105 @t104 @t103 @t102 @t117 @t114 @t99 @t127 @t126 @t123 @t122 @t121 @t120 @t119 @t118 @t125 @t116 @t124 @t114 @t113 @t112 @t111 @t110 @t109 @t108 @t107 @t106 @t105 @t104 @t103 @t102 @t115 @t117 @t99 @t243 @t241 @t101 @t328 @t233 @t99 @t242 @t99 @t145 @t99 @t228 @t230 @t222))) % 0.38/0.80 (step @p735 :rule nary_cong :premises (@p163 @p135) :args ((or @t233 @t218))) % 0.38/0.80 (step @p736 :rule cnf_or_neg :args (@t233 2)) % 0.38/0.80 (step @p737 :rule eq_resolve :premises (@p736 @p735)) % 0.38/0.80 (step @p738 :rule reordering :premises (@p737) :args ((or @t98 @t233))) % 0.38/0.80 (step @p739 :rule chain_m_resolution :premises (@p738 @p734) :args (@t233 @t364 @t365)) % 0.38/0.80 (step @p740 :rule nary_cong :premises (@p178 @p135) :args ((or @t243 @t218))) % 0.38/0.80 (step @p741 :rule cnf_or_neg :args (@t243 2)) % 0.38/0.80 (step @p742 :rule eq_resolve :premises (@p741 @p740)) % 0.38/0.80 (step @p743 :rule reordering :premises (@p742) :args ((or @t98 @t243))) % 0.38/0.80 (step @p744 :rule chain_m_resolution :premises (@p743 @p734) :args (@t243 @t364 @t365)) % 0.38/0.80 (step @p745 :rule nary_cong :premises (@p173 @p135) :args ((or @t242 @t218))) % 0.38/0.80 (step @p746 :rule cnf_or_neg :args (@t242 2)) % 0.38/0.80 (step @p747 :rule eq_resolve :premises (@p746 @p745)) % 0.38/0.80 (step @p748 :rule reordering :premises (@p747) :args ((or @t98 @t242))) % 0.38/0.80 (step @p749 :rule chain_m_resolution :premises (@p748 @p734) :args (@t242 @t364 @t365)) % 0.38/0.80 (step @p750 :rule nary_cong :premises (@p168 @p135) :args ((or @t241 @t218))) % 0.38/0.80 (step @p751 :rule cnf_or_neg :args (@t241 3)) % 0.38/0.80 (step @p752 :rule eq_resolve :premises (@p751 @p750)) % 0.38/0.80 (step @p753 :rule reordering :premises (@p752) :args ((or @t98 @t241))) % 0.38/0.80 (step @p754 :rule chain_m_resolution :premises (@p753 @p734) :args (@t241 @t364 @t365)) % 0.38/0.80 (step @p755 :rule nary_cong :premises (@p183 @p135) :args ((or @t259 @t218))) % 0.38/0.80 (step @p756 :rule cnf_or_neg :args (@t259 1)) % 0.38/0.80 (step @p757 :rule eq_resolve :premises (@p756 @p755)) % 0.38/0.80 (step @p758 :rule reordering :premises (@p757) :args ((or @t98 @t259))) % 0.38/0.80 (step @p759 :rule chain_m_resolution :premises (@p758 @p734) :args (@t259 @t364 @t365)) % 0.38/0.80 (step @p760 false :rule chain_m_resolution :premises (@p574 @p759 @p754 @p572 @p749 @p744 @p739 @p143 @p128 @p126 @p124) :args (false @t324 (@list @t259 @t241 @t296 @t242 @t243 @t233 @t216 @t215 @t211 @t205))) % 0.38/0.80 ) % 0.38/0.80 % SZS output end Proof % 0.38/0.80 % cvc5 exiting %------------------------------------------------------------------------------