%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : SYO500^1.004 : TPTP v9.2.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n022.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:13:00 AM UTC 2026 % Result : Theorem 0.38s 0.62s % Output : Proof 0.38s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYO500^1.004 : TPTP v9.2.1. Released v4.1.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 : n022.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 : Wed Jun 3 00:18:08 EDT 2026 % 0.17/0.35 % CPUTime : % 0.28/0.50 %----Proving TH0 % 0.38/0.62 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-cegqi --no-sygus-inst at 90s... % 0.38/0.62 % SZS status Theorem % 0.38/0.62 % SZS output start Proof % 0.38/0.62 ( % 0.38/0.62 (declare-const tptp.f0 (-> Bool Bool)) % 0.38/0.62 (declare-const tptp.f1 (-> Bool Bool)) % 0.38/0.62 (declare-const tptp.f2 (-> Bool Bool)) % 0.38/0.62 (declare-const tptp.f3 (-> Bool Bool)) % 0.38/0.62 (declare-const tptp.x Bool) % 0.38/0.62 (define @t1 () (_ tptp.f3 tptp.x)) % 0.38/0.62 (define @t2 () (_ tptp.f3 @t1)) % 0.38/0.62 (define @t3 () (_ tptp.f3 @t2)) % 0.38/0.62 (define @t4 () (_ tptp.f2 @t3)) % 0.38/0.62 (define @t5 () (_ tptp.f1 @t4)) % 0.38/0.62 (define @t6 () (_ tptp.f1 @t5)) % 0.38/0.62 (define @t7 () (_ tptp.f1 @t6)) % 0.38/0.62 (define @t8 () (_ tptp.f2 @t1)) % 0.38/0.62 (define @t9 () (_ tptp.f2 @t8)) % 0.38/0.62 (define @t10 () (_ tptp.f2 @t9)) % 0.38/0.62 (define @t11 () (_ tptp.f1 @t10)) % 0.38/0.62 (define @t12 () (_ tptp.f0 @t11)) % 0.38/0.62 (define @t13 () (_ tptp.f0 @t12)) % 0.38/0.62 (define @t14 () (= (_ tptp.f0 @t13) (_ tptp.f0 @t7))) % 0.38/0.62 (define @t15 () (not @t14)) % 0.38/0.62 (define @t16 () (@purify @t13)) % 0.38/0.62 (define @t17 () (tptp.f0 @t16)) % 0.38/0.62 (define @t18 () (@purify @t7)) % 0.38/0.62 (define @t19 () (tptp.f0 @t18)) % 0.38/0.62 (define @t20 () (_ tptp.f0 @t18)) % 0.38/0.62 (define @t21 () (= @t7 @t18)) % 0.38/0.62 (define @t22 () (_ tptp.f0 @t16)) % 0.38/0.62 (define @t23 () (= @t13 @t16)) % 0.38/0.62 (define @t24 () (@purify @t6)) % 0.38/0.62 (define @t25 () (tptp.f1 @t24)) % 0.38/0.62 (define @t26 () (_ tptp.f1 @t24)) % 0.38/0.62 (define @t27 () (= @t6 @t24)) % 0.38/0.62 (define @t28 () (not @t18)) % 0.38/0.62 (define @t29 () (not @t16)) % 0.38/0.62 (define @t30 () (not @t19)) % 0.38/0.62 (define @t31 () (not @t17)) % 0.38/0.62 (define @t32 () (not @t31)) % 0.38/0.62 (define @t33 () (= false true)) % 0.38/0.62 (define @t34 () (and @t19 @t18 @t16 @t31)) % 0.38/0.62 (define @t35 () (@purify @t12)) % 0.38/0.62 (define @t36 () (tptp.f0 @t35)) % 0.38/0.62 (define @t37 () (_ tptp.f0 @t35)) % 0.38/0.62 (define @t38 () (= @t12 @t35)) % 0.38/0.62 (define @t39 () (not @t35)) % 0.38/0.62 (define @t40 () (not @t36)) % 0.38/0.62 (define @t41 () (not @t40)) % 0.38/0.62 (define @t42 () (and @t19 @t18 @t35 @t40)) % 0.38/0.62 (define @t43 () (@purify @t11)) % 0.38/0.62 (define @t44 () (tptp.f0 @t43)) % 0.38/0.62 (define @t45 () (_ tptp.f0 @t43)) % 0.38/0.62 (define @t46 () (= @t11 @t43)) % 0.38/0.62 (define @t47 () (not @t43)) % 0.38/0.62 (define @t48 () (not @t44)) % 0.38/0.62 (define @t49 () (not @t48)) % 0.38/0.62 (define @t50 () (and @t19 @t18 @t43 @t48)) % 0.38/0.62 (define @t51 () (@purify @t10)) % 0.38/0.62 (define @t52 () (tptp.f1 @t51)) % 0.38/0.62 (define @t53 () (_ tptp.f1 @t51)) % 0.38/0.62 (define @t54 () (= @t10 @t51)) % 0.38/0.62 (define @t55 () (@purify @t5)) % 0.38/0.62 (define @t56 () (tptp.f1 @t55)) % 0.38/0.62 (define @t57 () (_ tptp.f1 @t55)) % 0.38/0.62 (define @t58 () (= @t5 @t55)) % 0.38/0.62 (define @t59 () (not @t24)) % 0.38/0.62 (define @t60 () (not @t51)) % 0.38/0.62 (define @t61 () (not @t25)) % 0.38/0.62 (define @t62 () (not @t52)) % 0.38/0.62 (define @t63 () (not @t62)) % 0.38/0.62 (define @t64 () (and @t25 @t24 @t51 @t62)) % 0.38/0.62 (define @t65 () (@purify @t9)) % 0.38/0.62 (define @t66 () (tptp.f2 @t65)) % 0.38/0.62 (define @t67 () (_ tptp.f2 @t65)) % 0.38/0.62 (define @t68 () (= @t9 @t65)) % 0.38/0.62 (define @t69 () (@purify @t8)) % 0.38/0.62 (define @t70 () (tptp.f2 @t69)) % 0.38/0.62 (define @t71 () (_ tptp.f2 @t69)) % 0.38/0.62 (define @t72 () (= @t8 @t69)) % 0.38/0.62 (define @t73 () (not @t65)) % 0.38/0.62 (define @t74 () (@purify @t3)) % 0.38/0.62 (define @t75 () (tptp.f2 @t74)) % 0.38/0.62 (define @t76 () (not @t75)) % 0.38/0.62 (define @t77 () (not @t74)) % 0.38/0.62 (define @t78 () (not @t66)) % 0.38/0.62 (define @t79 () (not @t78)) % 0.38/0.62 (define @t80 () (= true false)) % 0.38/0.62 (define @t81 () (and @t78 @t65 @t74 @t75)) % 0.38/0.62 (define @t82 () (not @t70)) % 0.38/0.62 (define @t83 () (not @t69)) % 0.38/0.62 (define @t84 () (and @t78 @t65 @t69 @t70)) % 0.38/0.62 (define @t85 () (@purify @t2)) % 0.38/0.62 (define @t86 () (tptp.f3 @t85)) % 0.38/0.62 (define @t87 () (_ tptp.f3 @t85)) % 0.38/0.62 (define @t88 () (= @t2 @t85)) % 0.38/0.62 (define @t89 () (= @t3 @t74)) % 0.38/0.62 (define @t90 () (@purify @t1)) % 0.38/0.62 (define @t91 () (tptp.f2 @t90)) % 0.38/0.62 (define @t92 () (_ tptp.f2 @t90)) % 0.38/0.62 (define @t93 () (= @t1 @t90)) % 0.38/0.62 (define @t94 () (@purify tptp.x)) % 0.38/0.62 (define @t95 () (tptp.f3 @t94)) % 0.38/0.62 (define @t96 () (_ tptp.f3 @t94)) % 0.38/0.62 (define @t97 () (not @t90)) % 0.38/0.62 (define @t98 () (tptp.f3 @t90)) % 0.38/0.62 (define @t99 () (_ tptp.f3 @t90)) % 0.38/0.62 (define @t100 () (not @t85)) % 0.38/0.62 (define @t101 () (not @t98)) % 0.38/0.62 (define @t102 () (not @t86)) % 0.38/0.62 (define @t103 () (not @t102)) % 0.38/0.62 (define @t104 () (and @t85 @t90 @t102)) % 0.38/0.62 (define @t105 () (@list false)) % 0.38/0.62 (define @t106 () (not @t95)) % 0.38/0.62 (define @t107 () (not @t94)) % 0.38/0.62 (define @t108 () (and @t101 @t90 @t94 @t95)) % 0.38/0.62 (define @t109 () (not @t107)) % 0.38/0.62 (define @t110 () (not @t100)) % 0.38/0.62 (define @t111 () (and @t102 @t100 @t107 @t95)) % 0.38/0.62 (define @t112 () (@list true true true false)) % 0.38/0.62 (define @t113 () (not @t97)) % 0.38/0.62 (define @t114 () (not @t91)) % 0.38/0.62 (define @t115 () (not @t114)) % 0.38/0.62 (define @t116 () (not @t83)) % 0.38/0.62 (define @t117 () (and @t70 @t83 @t97 @t114)) % 0.38/0.62 (define @t118 () (@list true true true true true false)) % 0.38/0.62 (define @t119 () (not @t82)) % 0.38/0.62 (define @t120 () (and @t75 @t74 @t69 @t82)) % 0.38/0.62 (define @t121 () (and @t75 @t74 @t90 @t114)) % 0.38/0.62 (define @t122 () (not @t106)) % 0.38/0.62 (define @t123 () (and @t86 @t85 @t94 @t106)) % 0.38/0.62 (define @t124 () (and @t98 @t97 @t107 @t106)) % 0.38/0.62 (define @t125 () (and @t86 @t100 @t97)) % 0.38/0.62 (define @t126 () (not @t73)) % 0.38/0.62 (define @t127 () (not @t77)) % 0.38/0.62 (define @t128 () (and @t78 @t73 @t77 @t75)) % 0.38/0.62 (define @t129 () (@list true true true)) % 0.38/0.62 (define @t130 () (@purify @t4)) % 0.38/0.62 (define @t131 () (_ tptp.f2 @t74)) % 0.38/0.62 (define @t132 () (= @t4 @t130)) % 0.38/0.62 (define @t133 () (not @t130)) % 0.38/0.62 (define @t134 () (tptp.f1 @t130)) % 0.38/0.62 (define @t135 () (not @t134)) % 0.38/0.62 (define @t136 () (not @t60)) % 0.38/0.62 (define @t137 () (not @t133)) % 0.38/0.62 (define @t138 () (and @t62 @t60 @t133 @t134)) % 0.38/0.62 (define @t139 () (_ tptp.f1 @t130)) % 0.38/0.62 (define @t140 () (not @t55)) % 0.38/0.62 (define @t141 () (not @t56)) % 0.38/0.62 (define @t142 () (not @t140)) % 0.38/0.62 (define @t143 () (and @t62 @t60 @t140 @t56)) % 0.38/0.62 (define @t144 () (not @t141)) % 0.38/0.62 (define @t145 () (not @t59)) % 0.38/0.62 (define @t146 () (and @t25 @t59 @t140 @t141)) % 0.38/0.62 (define @t147 () (and @t62 @t51 @t130 @t134)) % 0.38/0.62 (define @t148 () (not @t76)) % 0.38/0.62 (define @t149 () (and @t66 @t65 @t74 @t76)) % 0.38/0.62 (define @t150 () (and @t76 @t77 @t97)) % 0.38/0.62 (define @t151 () (and @t66 @t73 @t83 @t82)) % 0.38/0.62 (define @t152 () (and @t76 @t74 @t90 @t91)) % 0.38/0.62 (define @t153 () (not @t61)) % 0.38/0.62 (define @t154 () (and @t61 @t24 @t51 @t52)) % 0.38/0.62 (define @t155 () (and @t61 @t24 @t55 @t56)) % 0.38/0.62 (define @t156 () (and @t56 @t140 @t133 @t135)) % 0.38/0.62 (define @t157 () (and @t130 @t51 @t52)) % 0.38/0.62 (define @t158 () (and @t52 @t51 @t55 @t141)) % 0.38/0.62 (define @t159 () (and @t61 @t59 @t60 @t52)) % 0.38/0.62 (define @t160 () (not @t47)) % 0.38/0.62 (define @t161 () (not @t28)) % 0.38/0.62 (define @t162 () (and @t19 @t28 @t47 @t48)) % 0.38/0.62 (define @t163 () (and @t31 @t16 @t35 @t36)) % 0.38/0.62 (define @t164 () (@list @t36)) % 0.38/0.62 (define @t165 () (not @t29)) % 0.38/0.62 (define @t166 () (and @t19 @t28 @t29 @t31)) % 0.38/0.62 (define @t167 () (@list true)) % 0.38/0.62 (define @t168 () (not @t30)) % 0.38/0.62 (define @t169 () (and @t30 @t18 @t16 @t17)) % 0.38/0.62 (define @t170 () (not @t39)) % 0.38/0.62 (define @t171 () (and @t17 @t29 @t39 @t40)) % 0.38/0.62 (define @t172 () (and @t30 @t18 @t43 @t44)) % 0.38/0.62 (define @t173 () (and @t30 @t28 @t47)) % 0.38/0.62 (define @t174 () (and @t30 @t28 @t39)) % 0.38/0.62 (assume @p1 @t15) % 0.38/0.62 (assume @p2 true) % 0.38/0.62 (step @p3 :rule eq-symm :args (@t17 @t19)) % 0.38/0.62 (step @p4 :rule refl :args (@t19)) % 0.38/0.62 (step @p5 :rule refl :args (@t20)) % 0.38/0.62 (step @p6 :rule cong :premises (@p5 @p4) :args ((= @t20 @t19))) % 0.38/0.62 (step @p7 :rule symm :premises (@p6)) % 0.38/0.62 (step @p8 :rule eq_resolve :premises (@p5 @p7)) % 0.38/0.62 (step @p9 :rule eq-refl :args (@t7)) % 0.38/0.62 (step @p10 :rule skolem_intro :args (@t18)) % 0.38/0.62 (step @p11 :rule refl :args (@t7)) % 0.38/0.62 (step @p12 :rule cong :premises (@p11 @p10) :args (@t21)) % 0.38/0.62 (step @p13 :rule trans :premises (@p12 @p9)) % 0.38/0.62 (step @p14 :rule true_elim :premises (@p13)) % 0.38/0.62 (step @p15 :rule refl :args (tptp.f0)) % 0.38/0.62 (step @p16 :rule ho_cong :premises (@p15 @p14)) % 0.38/0.62 (step @p17 :rule trans :premises (@p16 @p8)) % 0.38/0.62 (step @p18 :rule refl :args (@t17)) % 0.38/0.62 (step @p19 :rule refl :args (@t22)) % 0.38/0.62 (step @p20 :rule cong :premises (@p19 @p18) :args ((= @t22 @t17))) % 0.38/0.62 (step @p21 :rule symm :premises (@p20)) % 0.38/0.62 (step @p22 :rule eq_resolve :premises (@p19 @p21)) % 0.38/0.62 (step @p23 :rule eq-refl :args (@t13)) % 0.38/0.62 (step @p24 :rule skolem_intro :args (@t16)) % 0.38/0.62 (step @p25 :rule refl :args (@t13)) % 0.38/0.62 (step @p26 :rule cong :premises (@p25 @p24) :args (@t23)) % 0.38/0.62 (step @p27 :rule trans :premises (@p26 @p23)) % 0.38/0.62 (step @p28 :rule true_elim :premises (@p27)) % 0.38/0.62 (step @p29 :rule ho_cong :premises (@p15 @p28)) % 0.38/0.62 (step @p30 :rule trans :premises (@p29 @p22)) % 0.38/0.62 (step @p31 :rule cong :premises (@p30 @p17) :args (@t14)) % 0.38/0.62 (step @p32 :rule trans :premises (@p31 @p3)) % 0.38/0.62 (step @p33 :rule cong :premises (@p32) :args (@t15)) % 0.38/0.62 (step @p34 :rule eq_resolve :premises (@p1 @p33)) % 0.38/0.62 (step @p35 :rule not_equiv_elim2 :premises (@p34)) % 0.38/0.62 (step @p36 :rule eq-symm :args (@t25 @t18)) % 0.38/0.62 (step @p37 :rule refl :args (@t18)) % 0.38/0.62 (step @p38 :rule refl :args (@t25)) % 0.38/0.62 (step @p39 :rule refl :args (@t26)) % 0.38/0.62 (step @p40 :rule cong :premises (@p39 @p38) :args ((= @t26 @t25))) % 0.38/0.62 (step @p41 :rule symm :premises (@p40)) % 0.38/0.62 (step @p42 :rule eq_resolve :premises (@p39 @p41)) % 0.38/0.62 (step @p43 :rule eq-refl :args (@t6)) % 0.38/0.62 (step @p44 :rule skolem_intro :args (@t24)) % 0.38/0.62 (step @p45 :rule refl :args (@t6)) % 0.38/0.62 (step @p46 :rule cong :premises (@p45 @p44) :args (@t27)) % 0.38/0.62 (step @p47 :rule trans :premises (@p46 @p43)) % 0.38/0.62 (step @p48 :rule true_elim :premises (@p47)) % 0.38/0.62 (step @p49 :rule refl :args (tptp.f1)) % 0.38/0.62 (step @p50 :rule ho_cong :premises (@p49 @p48)) % 0.38/0.62 (step @p51 :rule trans :premises (@p50 @p42)) % 0.38/0.62 (step @p52 :rule cong :premises (@p51 @p37) :args (@t21)) % 0.38/0.62 (step @p53 :rule trans :premises (@p52 @p36)) % 0.38/0.62 (step @p54 :rule eq-symm :args (@t18 @t7)) % 0.38/0.62 (step @p55 :rule trans :premises (@p54 @p53)) % 0.38/0.62 (step @p56 :rule eq_resolve :premises (@p10 @p55)) % 0.38/0.62 (step @p57 :rule equiv_elim1 :premises (@p56)) % 0.38/0.62 (step @p58 :rule reordering :premises (@p57) :args ((or @t25 @t28))) % 0.38/0.62 (step @p59 :rule bool-double-not-elim :args (@t17)) % 0.38/0.62 (step @p60 :rule refl :args (@t29)) % 0.38/0.62 (step @p61 :rule refl :args (@t30)) % 0.38/0.62 (step @p62 :rule refl :args (@t28)) % 0.38/0.62 (step @p63 :rule nary_cong :premises (@p62 @p61 @p60 @p59) :args ((or @t28 @t30 @t29 @t32))) % 0.38/0.62 (assume-push @p1720 @t19) % 0.38/0.62 (assume-push @p1721 @t18) % 0.38/0.62 (assume-push @p1722 @t16) % 0.38/0.62 (assume-push @p1723 @t31) % 0.38/0.62 (step @p68 :rule evaluate :args (@t33)) % 0.38/0.62 (step @p69 :rule true_intro :premises (@p1720)) % 0.38/0.62 (step @p70 :rule true_intro :premises (@p1721)) % 0.38/0.62 (step @p71 :rule symm :premises (@p70)) % 0.38/0.62 (step @p72 :rule true_intro :premises (@p1722)) % 0.38/0.62 (step @p73 :rule trans :premises (@p72 @p71)) % 0.38/0.62 (step @p74 :rule cong :premises (@p73) :args (@t17)) % 0.38/0.62 (step @p75 :rule false_intro :premises (@p1723)) % 0.38/0.62 (step @p76 :rule symm :premises (@p75)) % 0.38/0.62 (step @p77 :rule trans :premises (@p76 @p74 @p69)) % 0.38/0.62 (step @p78 false :rule eq_resolve :premises (@p77 @p68)) % 0.38/0.62 (step-pop @p1724 :rule scope :premises (@p78)) % 0.38/0.62 (step-pop @p1725 :rule scope :premises (@p1724)) % 0.38/0.62 (step-pop @p1726 :rule scope :premises (@p1725)) % 0.38/0.62 (step-pop @p1727 :rule scope :premises (@p1726)) % 0.38/0.62 (step @p79 :rule process_scope :premises (@p1727) :args (false)) % 0.38/0.62 (assume-push @p1728 @t18) % 0.38/0.62 (assume-push @p1729 @t19) % 0.38/0.62 (assume-push @p1730 @t16) % 0.38/0.62 (assume-push @p1731 @t31) % 0.38/0.62 (step @p88 :rule and_intro :premises (@p1729 @p1728 @p1730 @p1731)) % 0.38/0.62 (step-pop @p1732 :rule scope :premises (@p88)) % 0.38/0.62 (step-pop @p1733 :rule scope :premises (@p1732)) % 0.38/0.62 (step-pop @p1734 :rule scope :premises (@p1733)) % 0.38/0.62 (step-pop @p1735 :rule scope :premises (@p1734)) % 0.38/0.62 (step @p89 :rule process_scope :premises (@p1735) :args (@t34)) % 0.38/0.62 (step @p94 :rule implies_elim :premises (@p89)) % 0.38/0.62 (step @p95 :rule resolution :premises (@p94 @p79) :args (true @t34)) % 0.38/0.62 (step @p96 :rule not_and :premises (@p95)) % 0.38/0.62 (step @p97 :rule eq_resolve :premises (@p96 @p63)) % 0.38/0.62 (step @p98 :rule reordering :premises (@p97) :args ((or @t17 @t30 @t28 @t29))) % 0.38/0.62 (step @p99 :rule eq-symm :args (@t36 @t16)) % 0.38/0.62 (step @p100 :rule refl :args (@t16)) % 0.38/0.62 (step @p101 :rule refl :args (@t36)) % 0.38/0.62 (step @p102 :rule refl :args (@t37)) % 0.38/0.62 (step @p103 :rule cong :premises (@p102 @p101) :args ((= @t37 @t36))) % 0.38/0.62 (step @p104 :rule symm :premises (@p103)) % 0.38/0.62 (step @p105 :rule eq_resolve :premises (@p102 @p104)) % 0.38/0.62 (step @p106 :rule eq-refl :args (@t12)) % 0.38/0.62 (step @p107 :rule skolem_intro :args (@t35)) % 0.38/0.62 (step @p108 :rule refl :args (@t12)) % 0.38/0.62 (step @p109 :rule cong :premises (@p108 @p107) :args (@t38)) % 0.38/0.62 (step @p110 :rule trans :premises (@p109 @p106)) % 0.38/0.62 (step @p111 :rule true_elim :premises (@p110)) % 0.38/0.62 (step @p112 :rule ho_cong :premises (@p15 @p111)) % 0.38/0.62 (step @p113 :rule trans :premises (@p112 @p105)) % 0.38/0.62 (step @p114 :rule cong :premises (@p113 @p100) :args (@t23)) % 0.38/0.62 (step @p115 :rule trans :premises (@p114 @p99)) % 0.38/0.62 (step @p116 :rule eq-symm :args (@t16 @t13)) % 0.38/0.62 (step @p117 :rule trans :premises (@p116 @p115)) % 0.38/0.62 (step @p118 :rule eq_resolve :premises (@p24 @p117)) % 0.38/0.62 (step @p119 :rule equiv_elim2 :premises (@p118)) % 0.38/0.62 (step @p120 :rule bool-double-not-elim :args (@t36)) % 0.38/0.62 (step @p121 :rule refl :args (@t39)) % 0.38/0.62 (step @p122 :rule nary_cong :premises (@p62 @p61 @p121 @p120) :args ((or @t28 @t30 @t39 @t41))) % 0.38/0.62 (assume-push @p1736 @t19) % 0.38/0.62 (assume-push @p1737 @t18) % 0.38/0.62 (assume-push @p1738 @t35) % 0.38/0.62 (assume-push @p1739 @t40) % 0.38/0.62 (step @p68 :rule evaluate :args (@t33)) % 0.38/0.62 (step @p127 :rule true_intro :premises (@p1736)) % 0.38/0.62 (step @p128 :rule true_intro :premises (@p1737)) % 0.38/0.62 (step @p129 :rule symm :premises (@p128)) % 0.38/0.62 (step @p130 :rule true_intro :premises (@p1738)) % 0.38/0.62 (step @p131 :rule trans :premises (@p130 @p129)) % 0.38/0.62 (step @p132 :rule cong :premises (@p131) :args (@t36)) % 0.38/0.62 (step @p133 :rule false_intro :premises (@p1739)) % 0.38/0.62 (step @p134 :rule symm :premises (@p133)) % 0.38/0.62 (step @p135 :rule trans :premises (@p134 @p132 @p127)) % 0.38/0.62 (step @p136 false :rule eq_resolve :premises (@p135 @p68)) % 0.38/0.62 (step-pop @p1740 :rule scope :premises (@p136)) % 0.38/0.62 (step-pop @p1741 :rule scope :premises (@p1740)) % 0.38/0.62 (step-pop @p1742 :rule scope :premises (@p1741)) % 0.38/0.62 (step-pop @p1743 :rule scope :premises (@p1742)) % 0.38/0.62 (step @p137 :rule process_scope :premises (@p1743) :args (false)) % 0.38/0.62 (assume-push @p1744 @t18) % 0.38/0.62 (assume-push @p1745 @t19) % 0.38/0.62 (assume-push @p1746 @t35) % 0.38/0.62 (assume-push @p1747 @t40) % 0.38/0.62 (step @p146 :rule and_intro :premises (@p1745 @p1744 @p1746 @p1747)) % 0.38/0.62 (step-pop @p1748 :rule scope :premises (@p146)) % 0.38/0.62 (step-pop @p1749 :rule scope :premises (@p1748)) % 0.38/0.62 (step-pop @p1750 :rule scope :premises (@p1749)) % 0.38/0.62 (step-pop @p1751 :rule scope :premises (@p1750)) % 0.38/0.62 (step @p147 :rule process_scope :premises (@p1751) :args (@t42)) % 0.38/0.62 (step @p152 :rule implies_elim :premises (@p147)) % 0.38/0.62 (step @p153 :rule resolution :premises (@p152 @p137) :args (true @t42)) % 0.38/0.62 (step @p154 :rule not_and :premises (@p153)) % 0.38/0.62 (step @p155 :rule eq_resolve :premises (@p154 @p122)) % 0.38/0.62 (step @p156 :rule reordering :premises (@p155) :args ((or @t36 @t30 @t28 @t39))) % 0.38/0.62 (step @p157 :rule eq-symm :args (@t44 @t35)) % 0.38/0.62 (step @p158 :rule refl :args (@t35)) % 0.38/0.62 (step @p159 :rule refl :args (@t44)) % 0.38/0.62 (step @p160 :rule refl :args (@t45)) % 0.38/0.62 (step @p161 :rule cong :premises (@p160 @p159) :args ((= @t45 @t44))) % 0.38/0.62 (step @p162 :rule symm :premises (@p161)) % 0.38/0.62 (step @p163 :rule eq_resolve :premises (@p160 @p162)) % 0.38/0.62 (step @p164 :rule eq-refl :args (@t11)) % 0.38/0.62 (step @p165 :rule skolem_intro :args (@t43)) % 0.38/0.62 (step @p166 :rule refl :args (@t11)) % 0.38/0.62 (step @p167 :rule cong :premises (@p166 @p165) :args (@t46)) % 0.38/0.62 (step @p168 :rule trans :premises (@p167 @p164)) % 0.38/0.62 (step @p169 :rule true_elim :premises (@p168)) % 0.38/0.62 (step @p170 :rule ho_cong :premises (@p15 @p169)) % 0.38/0.62 (step @p171 :rule trans :premises (@p170 @p163)) % 0.38/0.62 (step @p172 :rule cong :premises (@p171 @p158) :args (@t38)) % 0.38/0.62 (step @p173 :rule trans :premises (@p172 @p157)) % 0.38/0.62 (step @p174 :rule eq-symm :args (@t35 @t12)) % 0.38/0.62 (step @p175 :rule trans :premises (@p174 @p173)) % 0.38/0.62 (step @p176 :rule eq_resolve :premises (@p107 @p175)) % 0.38/0.62 (step @p177 :rule equiv_elim2 :premises (@p176)) % 0.38/0.62 (step @p178 :rule bool-double-not-elim :args (@t44)) % 0.38/0.62 (step @p179 :rule refl :args (@t47)) % 0.38/0.62 (step @p180 :rule nary_cong :premises (@p62 @p61 @p179 @p178) :args ((or @t28 @t30 @t47 @t49))) % 0.38/0.62 (assume-push @p1752 @t19) % 0.38/0.62 (assume-push @p1753 @t18) % 0.38/0.62 (assume-push @p1754 @t43) % 0.38/0.62 (assume-push @p1755 @t48) % 0.38/0.62 (step @p68 :rule evaluate :args (@t33)) % 0.38/0.62 (step @p185 :rule true_intro :premises (@p1752)) % 0.38/0.62 (step @p186 :rule true_intro :premises (@p1753)) % 0.38/0.62 (step @p187 :rule symm :premises (@p186)) % 0.38/0.62 (step @p188 :rule true_intro :premises (@p1754)) % 0.38/0.62 (step @p189 :rule trans :premises (@p188 @p187)) % 0.38/0.62 (step @p190 :rule cong :premises (@p189) :args (@t44)) % 0.38/0.62 (step @p191 :rule false_intro :premises (@p1755)) % 0.38/0.62 (step @p192 :rule symm :premises (@p191)) % 0.38/0.62 (step @p193 :rule trans :premises (@p192 @p190 @p185)) % 0.38/0.62 (step @p194 false :rule eq_resolve :premises (@p193 @p68)) % 0.38/0.62 (step-pop @p1756 :rule scope :premises (@p194)) % 0.38/0.62 (step-pop @p1757 :rule scope :premises (@p1756)) % 0.38/0.62 (step-pop @p1758 :rule scope :premises (@p1757)) % 0.38/0.62 (step-pop @p1759 :rule scope :premises (@p1758)) % 0.38/0.62 (step @p195 :rule process_scope :premises (@p1759) :args (false)) % 0.38/0.62 (assume-push @p1760 @t18) % 0.38/0.62 (assume-push @p1761 @t19) % 0.38/0.62 (assume-push @p1762 @t43) % 0.38/0.62 (assume-push @p1763 @t48) % 0.38/0.62 (step @p204 :rule and_intro :premises (@p1761 @p1760 @p1762 @p1763)) % 0.38/0.62 (step-pop @p1764 :rule scope :premises (@p204)) % 0.38/0.62 (step-pop @p1765 :rule scope :premises (@p1764)) % 0.38/0.62 (step-pop @p1766 :rule scope :premises (@p1765)) % 0.38/0.62 (step-pop @p1767 :rule scope :premises (@p1766)) % 0.38/0.62 (step @p205 :rule process_scope :premises (@p1767) :args (@t50)) % 0.38/0.62 (step @p210 :rule implies_elim :premises (@p205)) % 0.38/0.62 (step @p211 :rule resolution :premises (@p210 @p195) :args (true @t50)) % 0.38/0.62 (step @p212 :rule not_and :premises (@p211)) % 0.38/0.62 (step @p213 :rule eq_resolve :premises (@p212 @p180)) % 0.38/0.62 (step @p214 :rule reordering :premises (@p213) :args ((or @t44 @t30 @t28 @t47))) % 0.38/0.62 (step @p215 :rule eq-symm :args (@t52 @t43)) % 0.38/0.62 (step @p216 :rule refl :args (@t43)) % 0.38/0.62 (step @p217 :rule refl :args (@t52)) % 0.38/0.62 (step @p218 :rule refl :args (@t53)) % 0.38/0.62 (step @p219 :rule cong :premises (@p218 @p217) :args ((= @t53 @t52))) % 0.38/0.62 (step @p220 :rule symm :premises (@p219)) % 0.38/0.62 (step @p221 :rule eq_resolve :premises (@p218 @p220)) % 0.38/0.62 (step @p222 :rule eq-refl :args (@t10)) % 0.38/0.62 (step @p223 :rule skolem_intro :args (@t51)) % 0.38/0.62 (step @p224 :rule refl :args (@t10)) % 0.38/0.62 (step @p225 :rule cong :premises (@p224 @p223) :args (@t54)) % 0.38/0.62 (step @p226 :rule trans :premises (@p225 @p222)) % 0.38/0.62 (step @p227 :rule true_elim :premises (@p226)) % 0.38/0.62 (step @p228 :rule ho_cong :premises (@p49 @p227)) % 0.38/0.62 (step @p229 :rule trans :premises (@p228 @p221)) % 0.38/0.62 (step @p230 :rule cong :premises (@p229 @p216) :args (@t46)) % 0.38/0.62 (step @p231 :rule trans :premises (@p230 @p215)) % 0.38/0.62 (step @p232 :rule eq-symm :args (@t43 @t11)) % 0.38/0.62 (step @p233 :rule trans :premises (@p232 @p231)) % 0.38/0.62 (step @p234 :rule eq_resolve :premises (@p165 @p233)) % 0.38/0.62 (step @p235 :rule equiv_elim2 :premises (@p234)) % 0.38/0.62 (step @p236 :rule eq-symm :args (@t56 @t24)) % 0.38/0.62 (step @p237 :rule refl :args (@t24)) % 0.38/0.62 (step @p238 :rule refl :args (@t56)) % 0.38/0.62 (step @p239 :rule refl :args (@t57)) % 0.38/0.62 (step @p240 :rule cong :premises (@p239 @p238) :args ((= @t57 @t56))) % 0.38/0.62 (step @p241 :rule symm :premises (@p240)) % 0.38/0.62 (step @p242 :rule eq_resolve :premises (@p239 @p241)) % 0.38/0.62 (step @p243 :rule eq-refl :args (@t5)) % 0.38/0.62 (step @p244 :rule skolem_intro :args (@t55)) % 0.38/0.62 (step @p245 :rule refl :args (@t5)) % 0.38/0.62 (step @p246 :rule cong :premises (@p245 @p244) :args (@t58)) % 0.38/0.62 (step @p247 :rule trans :premises (@p246 @p243)) % 0.38/0.62 (step @p248 :rule true_elim :premises (@p247)) % 0.38/0.62 (step @p249 :rule ho_cong :premises (@p49 @p248)) % 0.38/0.62 (step @p250 :rule trans :premises (@p249 @p242)) % 0.38/0.62 (step @p251 :rule cong :premises (@p250 @p237) :args (@t27)) % 0.38/0.62 (step @p252 :rule trans :premises (@p251 @p236)) % 0.38/0.62 (step @p253 :rule eq-symm :args (@t24 @t6)) % 0.38/0.62 (step @p254 :rule trans :premises (@p253 @p252)) % 0.38/0.62 (step @p255 :rule eq_resolve :premises (@p44 @p254)) % 0.38/0.62 (step @p256 :rule equiv_elim1 :premises (@p255)) % 0.38/0.62 (step @p257 :rule reordering :premises (@p256) :args ((or @t56 @t59))) % 0.38/0.62 (step @p258 :rule bool-double-not-elim :args (@t52)) % 0.38/0.62 (step @p259 :rule refl :args (@t60)) % 0.38/0.62 (step @p260 :rule refl :args (@t61)) % 0.38/0.62 (step @p261 :rule refl :args (@t59)) % 0.38/0.62 (step @p262 :rule nary_cong :premises (@p261 @p260 @p259 @p258) :args ((or @t59 @t61 @t60 @t63))) % 0.38/0.62 (assume-push @p1768 @t25) % 0.38/0.62 (assume-push @p1769 @t24) % 0.38/0.62 (assume-push @p1770 @t51) % 0.38/0.62 (assume-push @p1771 @t62) % 0.38/0.62 (step @p68 :rule evaluate :args (@t33)) % 0.38/0.62 (step @p267 :rule true_intro :premises (@p1768)) % 0.38/0.62 (step @p268 :rule true_intro :premises (@p1769)) % 0.38/0.62 (step @p269 :rule symm :premises (@p268)) % 0.38/0.62 (step @p270 :rule true_intro :premises (@p1770)) % 0.38/0.62 (step @p271 :rule trans :premises (@p270 @p269)) % 0.38/0.62 (step @p272 :rule cong :premises (@p271) :args (@t52)) % 0.38/0.62 (step @p273 :rule false_intro :premises (@p1771)) % 0.38/0.62 (step @p274 :rule symm :premises (@p273)) % 0.38/0.62 (step @p275 :rule trans :premises (@p274 @p272 @p267)) % 0.38/0.62 (step @p276 false :rule eq_resolve :premises (@p275 @p68)) % 0.38/0.62 (step-pop @p1772 :rule scope :premises (@p276)) % 0.38/0.62 (step-pop @p1773 :rule scope :premises (@p1772)) % 0.38/0.62 (step-pop @p1774 :rule scope :premises (@p1773)) % 0.38/0.62 (step-pop @p1775 :rule scope :premises (@p1774)) % 0.38/0.62 (step @p277 :rule process_scope :premises (@p1775) :args (false)) % 0.38/0.62 (assume-push @p1776 @t24) % 0.38/0.62 (assume-push @p1777 @t25) % 0.38/0.62 (assume-push @p1778 @t51) % 0.38/0.62 (assume-push @p1779 @t62) % 0.38/0.62 (step @p286 :rule and_intro :premises (@p1777 @p1776 @p1778 @p1779)) % 0.38/0.62 (step-pop @p1780 :rule scope :premises (@p286)) % 0.38/0.62 (step-pop @p1781 :rule scope :premises (@p1780)) % 0.38/0.62 (step-pop @p1782 :rule scope :premises (@p1781)) % 0.38/0.62 (step-pop @p1783 :rule scope :premises (@p1782)) % 0.38/0.62 (step @p287 :rule process_scope :premises (@p1783) :args (@t64)) % 0.38/0.62 (step @p292 :rule implies_elim :premises (@p287)) % 0.38/0.62 (step @p293 :rule resolution :premises (@p292 @p277) :args (true @t64)) % 0.38/0.62 (step @p294 :rule not_and :premises (@p293)) % 0.38/0.62 (step @p295 :rule eq_resolve :premises (@p294 @p262)) % 0.38/0.62 (step @p296 :rule reordering :premises (@p295) :args ((or @t52 @t61 @t59 @t60))) % 0.38/0.62 (step @p297 :rule eq-symm :args (@t66 @t51)) % 0.38/0.62 (step @p298 :rule refl :args (@t51)) % 0.38/0.62 (step @p299 :rule refl :args (@t66)) % 0.38/0.62 (step @p300 :rule refl :args (@t67)) % 0.38/0.62 (step @p301 :rule cong :premises (@p300 @p299) :args ((= @t67 @t66))) % 0.38/0.62 (step @p302 :rule symm :premises (@p301)) % 0.38/0.62 (step @p303 :rule eq_resolve :premises (@p300 @p302)) % 0.38/0.62 (step @p304 :rule eq-refl :args (@t9)) % 0.38/0.62 (step @p305 :rule skolem_intro :args (@t65)) % 0.38/0.62 (step @p306 :rule refl :args (@t9)) % 0.38/0.62 (step @p307 :rule cong :premises (@p306 @p305) :args (@t68)) % 0.38/0.62 (step @p308 :rule trans :premises (@p307 @p304)) % 0.38/0.62 (step @p309 :rule true_elim :premises (@p308)) % 0.38/0.62 (step @p310 :rule refl :args (tptp.f2)) % 0.38/0.62 (step @p311 :rule ho_cong :premises (@p310 @p309)) % 0.38/0.62 (step @p312 :rule trans :premises (@p311 @p303)) % 0.38/0.62 (step @p313 :rule cong :premises (@p312 @p298) :args (@t54)) % 0.38/0.62 (step @p314 :rule trans :premises (@p313 @p297)) % 0.38/0.62 (step @p315 :rule eq-symm :args (@t51 @t10)) % 0.38/0.62 (step @p316 :rule trans :premises (@p315 @p314)) % 0.38/0.62 (step @p317 :rule eq_resolve :premises (@p223 @p316)) % 0.38/0.62 (step @p318 :rule equiv_elim2 :premises (@p317)) % 0.38/0.62 (step @p319 :rule eq-symm :args (@t70 @t65)) % 0.38/0.62 (step @p320 :rule refl :args (@t65)) % 0.38/0.62 (step @p321 :rule refl :args (@t70)) % 0.38/0.62 (step @p322 :rule refl :args (@t71)) % 0.38/0.62 (step @p323 :rule cong :premises (@p322 @p321) :args ((= @t71 @t70))) % 0.38/0.62 (step @p324 :rule symm :premises (@p323)) % 0.38/0.62 (step @p325 :rule eq_resolve :premises (@p322 @p324)) % 0.38/0.62 (step @p326 :rule eq-refl :args (@t8)) % 0.38/0.62 (step @p327 :rule skolem_intro :args (@t69)) % 0.38/0.62 (step @p328 :rule refl :args (@t8)) % 0.38/0.62 (step @p329 :rule cong :premises (@p328 @p327) :args (@t72)) % 0.38/0.62 (step @p330 :rule trans :premises (@p329 @p326)) % 0.38/0.62 (step @p331 :rule true_elim :premises (@p330)) % 0.38/0.62 (step @p332 :rule ho_cong :premises (@p310 @p331)) % 0.38/0.62 (step @p333 :rule trans :premises (@p332 @p325)) % 0.38/0.62 (step @p334 :rule cong :premises (@p333 @p320) :args (@t68)) % 0.38/0.62 (step @p335 :rule trans :premises (@p334 @p319)) % 0.38/0.62 (step @p336 :rule eq-symm :args (@t65 @t9)) % 0.38/0.62 (step @p337 :rule trans :premises (@p336 @p335)) % 0.38/0.62 (step @p338 :rule eq_resolve :premises (@p305 @p337)) % 0.38/0.62 (step @p339 :rule equiv_elim1 :premises (@p338)) % 0.38/0.62 (step @p340 :rule reordering :premises (@p339) :args ((or @t70 @t73))) % 0.38/0.62 (step @p341 :rule bool-double-not-elim :args (@t66)) % 0.38/0.62 (step @p342 :rule refl :args (@t73)) % 0.38/0.62 (step @p343 :rule refl :args (@t76)) % 0.38/0.62 (step @p344 :rule refl :args (@t77)) % 0.38/0.62 (step @p345 :rule nary_cong :premises (@p344 @p343 @p342 @p341) :args ((or @t77 @t76 @t73 @t79))) % 0.38/0.62 (assume-push @p1784 @t78) % 0.38/0.62 (assume-push @p1785 @t65) % 0.38/0.62 (assume-push @p1786 @t74) % 0.38/0.62 (assume-push @p1787 @t75) % 0.38/0.62 (step @p350 :rule evaluate :args (@t80)) % 0.38/0.62 (step @p351 :rule false_intro :premises (@p1784)) % 0.38/0.62 (step @p352 :rule true_intro :premises (@p1785)) % 0.38/0.62 (step @p353 :rule symm :premises (@p352)) % 0.38/0.62 (step @p354 :rule true_intro :premises (@p1786)) % 0.38/0.62 (step @p355 :rule trans :premises (@p354 @p353)) % 0.38/0.62 (step @p356 :rule cong :premises (@p355) :args (@t75)) % 0.38/0.62 (step @p357 :rule true_intro :premises (@p1787)) % 0.38/0.62 (step @p358 :rule symm :premises (@p357)) % 0.38/0.62 (step @p359 :rule trans :premises (@p358 @p356 @p351)) % 0.38/0.62 (step @p360 false :rule eq_resolve :premises (@p359 @p350)) % 0.38/0.62 (step-pop @p1788 :rule scope :premises (@p360)) % 0.38/0.62 (step-pop @p1789 :rule scope :premises (@p1788)) % 0.38/0.62 (step-pop @p1790 :rule scope :premises (@p1789)) % 0.38/0.62 (step-pop @p1791 :rule scope :premises (@p1790)) % 0.38/0.62 (step @p361 :rule process_scope :premises (@p1791) :args (false)) % 0.38/0.62 (assume-push @p1792 @t74) % 0.38/0.62 (assume-push @p1793 @t75) % 0.38/0.62 (assume-push @p1794 @t65) % 0.38/0.62 (assume-push @p1795 @t78) % 0.38/0.62 (step @p370 :rule and_intro :premises (@p1795 @p1794 @p1792 @p1793)) % 0.38/0.62 (step-pop @p1796 :rule scope :premises (@p370)) % 0.38/0.62 (step-pop @p1797 :rule scope :premises (@p1796)) % 0.38/0.62 (step-pop @p1798 :rule scope :premises (@p1797)) % 0.38/0.62 (step-pop @p1799 :rule scope :premises (@p1798)) % 0.38/0.62 (step @p371 :rule process_scope :premises (@p1799) :args (@t81)) % 0.38/0.62 (step @p376 :rule implies_elim :premises (@p371)) % 0.38/0.62 (step @p377 :rule resolution :premises (@p376 @p361) :args (true @t81)) % 0.38/0.62 (step @p378 :rule not_and :premises (@p377)) % 0.38/0.62 (step @p379 :rule eq_resolve :premises (@p378 @p345)) % 0.38/0.62 (step @p380 :rule reordering :premises (@p379) :args ((or @t66 @t76 @t77 @t73))) % 0.38/0.62 (step @p381 :rule refl :args (@t82)) % 0.38/0.62 (step @p382 :rule refl :args (@t83)) % 0.38/0.62 (step @p383 :rule nary_cong :premises (@p342 @p382 @p381 @p341) :args ((or @t73 @t83 @t82 @t79))) % 0.38/0.62 (assume-push @p1800 @t78) % 0.38/0.62 (assume-push @p1801 @t65) % 0.38/0.62 (assume-push @p1802 @t69) % 0.38/0.62 (assume-push @p1803 @t70) % 0.38/0.62 (step @p350 :rule evaluate :args (@t80)) % 0.38/0.62 (step @p388 :rule false_intro :premises (@p1800)) % 0.38/0.62 (step @p389 :rule true_intro :premises (@p1801)) % 0.38/0.62 (step @p390 :rule symm :premises (@p389)) % 0.38/0.62 (step @p391 :rule true_intro :premises (@p1802)) % 0.38/0.62 (step @p392 :rule trans :premises (@p391 @p390)) % 0.38/0.62 (step @p393 :rule cong :premises (@p392) :args (@t70)) % 0.38/0.62 (step @p394 :rule true_intro :premises (@p1803)) % 0.38/0.62 (step @p395 :rule symm :premises (@p394)) % 0.38/0.62 (step @p396 :rule trans :premises (@p395 @p393 @p388)) % 0.38/0.62 (step @p397 false :rule eq_resolve :premises (@p396 @p350)) % 0.38/0.62 (step-pop @p1804 :rule scope :premises (@p397)) % 0.38/0.62 (step-pop @p1805 :rule scope :premises (@p1804)) % 0.38/0.62 (step-pop @p1806 :rule scope :premises (@p1805)) % 0.38/0.62 (step-pop @p1807 :rule scope :premises (@p1806)) % 0.38/0.62 (step @p398 :rule process_scope :premises (@p1807) :args (false)) % 0.38/0.62 (assume-push @p1808 @t65) % 0.38/0.62 (assume-push @p1809 @t69) % 0.38/0.62 (assume-push @p1810 @t70) % 0.38/0.62 (assume-push @p1811 @t78) % 0.38/0.62 (step @p407 :rule and_intro :premises (@p1811 @p1808 @p1809 @p1810)) % 0.38/0.62 (step-pop @p1812 :rule scope :premises (@p407)) % 0.38/0.62 (step-pop @p1813 :rule scope :premises (@p1812)) % 0.38/0.62 (step-pop @p1814 :rule scope :premises (@p1813)) % 0.38/0.62 (step-pop @p1815 :rule scope :premises (@p1814)) % 0.38/0.62 (step @p408 :rule process_scope :premises (@p1815) :args (@t84)) % 0.38/0.62 (step @p413 :rule implies_elim :premises (@p408)) % 0.38/0.62 (step @p414 :rule resolution :premises (@p413 @p398) :args (true @t84)) % 0.38/0.62 (step @p415 :rule not_and :premises (@p414)) % 0.38/0.62 (step @p416 :rule eq_resolve :premises (@p415 @p383)) % 0.38/0.62 (step @p417 :rule reordering :premises (@p416) :args ((or @t66 @t73 @t82 @t83))) % 0.38/0.62 (step @p418 :rule eq-symm :args (@t86 @t74)) % 0.38/0.62 (step @p419 :rule refl :args (@t74)) % 0.38/0.62 (step @p420 :rule refl :args (@t86)) % 0.38/0.62 (step @p421 :rule refl :args (@t87)) % 0.38/0.62 (step @p422 :rule cong :premises (@p421 @p420) :args ((= @t87 @t86))) % 0.38/0.62 (step @p423 :rule symm :premises (@p422)) % 0.38/0.62 (step @p424 :rule eq_resolve :premises (@p421 @p423)) % 0.38/0.62 (step @p425 :rule eq-refl :args (@t2)) % 0.38/0.62 (step @p426 :rule skolem_intro :args (@t85)) % 0.38/0.62 (step @p427 :rule refl :args (@t2)) % 0.38/0.62 (step @p428 :rule cong :premises (@p427 @p426) :args (@t88)) % 0.38/0.62 (step @p429 :rule trans :premises (@p428 @p425)) % 0.38/0.62 (step @p430 :rule true_elim :premises (@p429)) % 0.38/0.62 (step @p431 :rule refl :args (tptp.f3)) % 0.38/0.62 (step @p432 :rule ho_cong :premises (@p431 @p430)) % 0.38/0.62 (step @p433 :rule trans :premises (@p432 @p424)) % 0.38/0.62 (step @p434 :rule cong :premises (@p433 @p419) :args (@t89)) % 0.38/0.62 (step @p435 :rule trans :premises (@p434 @p418)) % 0.38/0.62 (step @p436 :rule eq-symm :args (@t74 @t3)) % 0.38/0.62 (step @p437 :rule trans :premises (@p436 @p435)) % 0.38/0.62 (step @p438 :rule skolem_intro :args (@t74)) % 0.38/0.62 (step @p439 :rule eq_resolve :premises (@p438 @p437)) % 0.38/0.62 (step @p440 :rule equiv_elim2 :premises (@p439)) % 0.38/0.62 (step @p441 :rule eq-symm :args (@t91 @t69)) % 0.38/0.62 (step @p442 :rule refl :args (@t69)) % 0.38/0.62 (step @p443 :rule refl :args (@t91)) % 0.38/0.62 (step @p444 :rule refl :args (@t92)) % 0.38/0.62 (step @p445 :rule cong :premises (@p444 @p443) :args ((= @t92 @t91))) % 0.38/0.62 (step @p446 :rule symm :premises (@p445)) % 0.38/0.62 (step @p447 :rule eq_resolve :premises (@p444 @p446)) % 0.38/0.62 (step @p448 :rule eq-refl :args (@t1)) % 0.38/0.62 (step @p449 :rule skolem_intro :args (@t90)) % 0.38/0.62 (step @p450 :rule refl :args (@t1)) % 0.38/0.62 (step @p451 :rule cong :premises (@p450 @p449) :args (@t93)) % 0.38/0.62 (step @p452 :rule trans :premises (@p451 @p448)) % 0.38/0.62 (step @p453 :rule true_elim :premises (@p452)) % 0.38/0.62 (step @p454 :rule ho_cong :premises (@p310 @p453)) % 0.38/0.62 (step @p455 :rule trans :premises (@p454 @p447)) % 0.38/0.62 (step @p456 :rule cong :premises (@p455 @p442) :args (@t72)) % 0.38/0.62 (step @p457 :rule trans :premises (@p456 @p441)) % 0.38/0.62 (step @p458 :rule eq-symm :args (@t69 @t8)) % 0.38/0.62 (step @p459 :rule trans :premises (@p458 @p457)) % 0.38/0.62 (step @p460 :rule eq_resolve :premises (@p327 @p459)) % 0.38/0.62 (step @p461 :rule equiv_elim2 :premises (@p460)) % 0.38/0.62 (step @p462 :rule eq-symm :args (@t95 @t90)) % 0.38/0.62 (step @p463 :rule refl :args (@t90)) % 0.38/0.62 (step @p464 :rule refl :args (@t95)) % 0.38/0.62 (step @p465 :rule refl :args (@t96)) % 0.38/0.62 (step @p466 :rule cong :premises (@p465 @p464) :args ((= @t96 @t95))) % 0.38/0.62 (step @p467 :rule symm :premises (@p466)) % 0.38/0.62 (step @p468 :rule eq_resolve :premises (@p465 @p467)) % 0.38/0.62 (step @p469 :rule eq-refl :args (tptp.x)) % 0.38/0.62 (step @p470 :rule skolem_intro :args (@t94)) % 0.38/0.62 (step @p471 :rule refl :args (tptp.x)) % 0.38/0.62 (step @p472 :rule cong :premises (@p471 @p470) :args ((= tptp.x @t94))) % 0.38/0.62 (step @p473 :rule trans :premises (@p472 @p469)) % 0.38/0.62 (step @p474 :rule true_elim :premises (@p473)) % 0.38/0.62 (step @p475 :rule ho_cong :premises (@p431 @p474)) % 0.38/0.62 (step @p476 :rule trans :premises (@p475 @p468)) % 0.38/0.62 (step @p477 :rule cong :premises (@p476 @p463) :args (@t93)) % 0.38/0.62 (step @p478 :rule trans :premises (@p477 @p462)) % 0.38/0.62 (step @p479 :rule eq-symm :args (@t90 @t1)) % 0.38/0.62 (step @p480 :rule trans :premises (@p479 @p478)) % 0.38/0.62 (step @p481 :rule eq_resolve :premises (@p449 @p480)) % 0.38/0.62 (step @p482 :rule equiv_elim1 :premises (@p481)) % 0.38/0.62 (step @p483 :rule reordering :premises (@p482) :args ((or @t95 @t97))) % 0.38/0.62 (step @p484 :rule eq-symm :args (@t98 @t85)) % 0.38/0.62 (step @p485 :rule refl :args (@t85)) % 0.38/0.62 (step @p486 :rule refl :args (@t98)) % 0.38/0.62 (step @p487 :rule refl :args (@t99)) % 0.38/0.62 (step @p488 :rule cong :premises (@p487 @p486) :args ((= @t99 @t98))) % 0.38/0.62 (step @p489 :rule symm :premises (@p488)) % 0.38/0.62 (step @p490 :rule eq_resolve :premises (@p487 @p489)) % 0.38/0.62 (step @p491 :rule ho_cong :premises (@p431 @p453)) % 0.38/0.62 (step @p492 :rule trans :premises (@p491 @p490)) % 0.38/0.62 (step @p493 :rule cong :premises (@p492 @p485) :args (@t88)) % 0.38/0.62 (step @p494 :rule trans :premises (@p493 @p484)) % 0.38/0.62 (step @p495 :rule eq-symm :args (@t85 @t2)) % 0.38/0.62 (step @p496 :rule trans :premises (@p495 @p494)) % 0.38/0.62 (step @p497 :rule eq_resolve :premises (@p426 @p496)) % 0.38/0.62 (step @p498 :rule equiv_elim1 :premises (@p497)) % 0.38/0.62 (step @p499 :rule reordering :premises (@p498) :args ((or @t98 @t100))) % 0.38/0.62 (step @p500 :rule refl :args (@t101)) % 0.38/0.62 (step @p501 :rule bool-double-not-elim :args (@t86)) % 0.38/0.62 (step @p502 :rule refl :args (@t97)) % 0.38/0.62 (step @p503 :rule refl :args (@t100)) % 0.38/0.62 (step @p504 :rule nary_cong :premises (@p503 @p502 @p501 @p500) :args ((or @t100 @t97 @t103 @t101))) % 0.38/0.62 (assume-push @p1816 @t85) % 0.38/0.62 (assume-push @p1817 @t90) % 0.38/0.62 (assume-push @p1818 @t102) % 0.38/0.62 (assume-push @p1819 @t102) % 0.38/0.62 (assume-push @p1820 @t85) % 0.38/0.62 (assume-push @p1821 @t90) % 0.38/0.62 (step @p511 :rule false_intro :premises (@p1818)) % 0.38/0.62 (step @p512 :rule true_intro :premises (@p1816)) % 0.38/0.62 (step @p513 :rule symm :premises (@p512)) % 0.38/0.62 (step @p514 :rule true_intro :premises (@p1817)) % 0.38/0.62 (step @p515 :rule trans :premises (@p514 @p513)) % 0.38/0.62 (step @p516 :rule cong :premises (@p515) :args (@t98)) % 0.38/0.62 (step @p517 :rule trans :premises (@p516 @p511)) % 0.38/0.62 (step @p518 :rule false_elim :premises (@p517)) % 0.38/0.62 (step-pop @p1822 :rule scope :premises (@p518)) % 0.38/0.62 (step-pop @p1823 :rule scope :premises (@p1822)) % 0.38/0.62 (step-pop @p1824 :rule scope :premises (@p1823)) % 0.38/0.62 (step @p519 :rule process_scope :premises (@p1824) :args (@t101)) % 0.38/0.62 (step @p523 :rule and_intro :premises (@p1818 @p1816 @p1817)) % 0.38/0.62 (step @p524 :rule modus_ponens :premises (@p523 @p519)) % 0.38/0.62 (step-pop @p1825 :rule scope :premises (@p524)) % 0.38/0.62 (step-pop @p1826 :rule scope :premises (@p1825)) % 0.38/0.62 (step-pop @p1827 :rule scope :premises (@p1826)) % 0.38/0.62 (step @p525 :rule process_scope :premises (@p1827) :args (@t101)) % 0.38/0.62 (step @p529 :rule implies_elim :premises (@p525)) % 0.38/0.62 (step @p530 :rule cnf_and_neg :args (@t104)) % 0.38/0.62 (step @p531 :rule resolution :premises (@p530 @p529) :args (true @t104)) % 0.38/0.62 (step @p532 :rule eq_resolve :premises (@p531 @p504)) % 0.38/0.62 (step @p533 :rule reordering :premises (@p532) :args ((or @t86 @t100 @t101 @t97))) % 0.38/0.62 (step @p534 :rule chain_m_resolution :premises (@p533 @p499) :args ((or @t86 @t100 @t97) @t105 (@list @t98))) % 0.38/0.62 (step @p535 :rule equiv_elim2 :premises (@p497)) % 0.38/0.62 (step @p536 :rule bool-double-not-elim :args (@t98)) % 0.38/0.62 (step @p537 :rule refl :args (@t106)) % 0.38/0.62 (step @p538 :rule refl :args (@t107)) % 0.38/0.62 (step @p539 :rule nary_cong :premises (@p502 @p538 @p537 @p536) :args ((or @t97 @t107 @t106 (not @t101)))) % 0.38/0.62 (assume-push @p1828 @t101) % 0.38/0.62 (assume-push @p1829 @t90) % 0.38/0.62 (assume-push @p1830 @t94) % 0.38/0.62 (assume-push @p1831 @t95) % 0.38/0.62 (step @p350 :rule evaluate :args (@t80)) % 0.38/0.62 (step @p544 :rule false_intro :premises (@p1828)) % 0.38/0.62 (step @p545 :rule true_intro :premises (@p1829)) % 0.38/0.62 (step @p546 :rule symm :premises (@p545)) % 0.38/0.62 (step @p547 :rule true_intro :premises (@p1830)) % 0.38/0.62 (step @p548 :rule trans :premises (@p547 @p546)) % 0.38/0.62 (step @p549 :rule cong :premises (@p548) :args (@t95)) % 0.38/0.62 (step @p550 :rule true_intro :premises (@p1831)) % 0.38/0.62 (step @p551 :rule symm :premises (@p550)) % 0.38/0.62 (step @p552 :rule trans :premises (@p551 @p549 @p544)) % 0.38/0.62 (step @p553 false :rule eq_resolve :premises (@p552 @p350)) % 0.38/0.62 (step-pop @p1832 :rule scope :premises (@p553)) % 0.38/0.62 (step-pop @p1833 :rule scope :premises (@p1832)) % 0.38/0.62 (step-pop @p1834 :rule scope :premises (@p1833)) % 0.38/0.62 (step-pop @p1835 :rule scope :premises (@p1834)) % 0.38/0.62 (step @p554 :rule process_scope :premises (@p1835) :args (false)) % 0.38/0.62 (assume-push @p1836 @t90) % 0.38/0.62 (assume-push @p1837 @t94) % 0.38/0.62 (assume-push @p1838 @t95) % 0.38/0.62 (assume-push @p1839 @t101) % 0.38/0.62 (step @p563 :rule and_intro :premises (@p1839 @p1836 @p1837 @p1838)) % 0.38/0.62 (step-pop @p1840 :rule scope :premises (@p563)) % 0.38/0.62 (step-pop @p1841 :rule scope :premises (@p1840)) % 0.38/0.62 (step-pop @p1842 :rule scope :premises (@p1841)) % 0.38/0.62 (step-pop @p1843 :rule scope :premises (@p1842)) % 0.38/0.62 (step @p564 :rule process_scope :premises (@p1843) :args (@t108)) % 0.38/0.62 (step @p569 :rule implies_elim :premises (@p564)) % 0.38/0.62 (step @p570 :rule resolution :premises (@p569 @p554) :args (true @t108)) % 0.38/0.62 (step @p571 :rule not_and :premises (@p570)) % 0.38/0.62 (step @p572 :rule eq_resolve :premises (@p571 @p539)) % 0.38/0.62 (step @p573 :rule reordering :premises (@p572) :args ((or @t98 @t97 @t106 @t107))) % 0.38/0.62 (step @p574 :rule bool-double-not-elim :args (@t94)) % 0.38/0.62 (step @p575 :rule bool-double-not-elim :args (@t85)) % 0.38/0.62 (step @p576 :rule nary_cong :premises (@p537 @p501 @p575 @p574) :args ((or @t106 @t103 @t110 @t109))) % 0.38/0.62 (assume-push @p1844 @t102) % 0.38/0.62 (assume-push @p1845 @t100) % 0.38/0.62 (assume-push @p1846 @t107) % 0.38/0.62 (assume-push @p1847 @t95) % 0.38/0.62 (step @p350 :rule evaluate :args (@t80)) % 0.38/0.62 (step @p581 :rule false_intro :premises (@p1844)) % 0.38/0.62 (step @p582 :rule false_intro :premises (@p1845)) % 0.38/0.62 (step @p583 :rule symm :premises (@p582)) % 0.38/0.62 (step @p584 :rule false_intro :premises (@p1846)) % 0.38/0.62 (step @p585 :rule trans :premises (@p584 @p583)) % 0.38/0.62 (step @p586 :rule cong :premises (@p585) :args (@t95)) % 0.38/0.62 (step @p587 :rule true_intro :premises (@p1847)) % 0.38/0.62 (step @p588 :rule symm :premises (@p587)) % 0.38/0.62 (step @p589 :rule trans :premises (@p588 @p586 @p581)) % 0.38/0.62 (step @p590 false :rule eq_resolve :premises (@p589 @p350)) % 0.38/0.62 (step-pop @p1848 :rule scope :premises (@p590)) % 0.38/0.62 (step-pop @p1849 :rule scope :premises (@p1848)) % 0.38/0.62 (step-pop @p1850 :rule scope :premises (@p1849)) % 0.38/0.62 (step-pop @p1851 :rule scope :premises (@p1850)) % 0.38/0.62 (step @p591 :rule process_scope :premises (@p1851) :args (false)) % 0.38/0.62 (assume-push @p1852 @t95) % 0.38/0.62 (assume-push @p1853 @t102) % 0.38/0.62 (assume-push @p1854 @t100) % 0.38/0.62 (assume-push @p1855 @t107) % 0.38/0.62 (step @p600 :rule and_intro :premises (@p1853 @p1854 @p1855 @p1852)) % 0.38/0.62 (step-pop @p1856 :rule scope :premises (@p600)) % 0.38/0.62 (step-pop @p1857 :rule scope :premises (@p1856)) % 0.38/0.62 (step-pop @p1858 :rule scope :premises (@p1857)) % 0.38/0.62 (step-pop @p1859 :rule scope :premises (@p1858)) % 0.38/0.62 (step @p601 :rule process_scope :premises (@p1859) :args (@t111)) % 0.38/0.62 (step @p606 :rule implies_elim :premises (@p601)) % 0.38/0.62 (step @p607 :rule resolution :premises (@p606 @p591) :args (true @t111)) % 0.38/0.62 (step @p608 :rule not_and :premises (@p607)) % 0.38/0.62 (step @p609 :rule eq_resolve :premises (@p608 @p576)) % 0.38/0.62 (step @p610 :rule reordering :premises (@p609) :args ((or @t85 @t86 @t94 @t106))) % 0.38/0.62 (step @p611 :rule chain_m_resolution :premises (@p610 @p573 @p535 @p534 @p483) :args ((or @t86 @t97) @t112 (@list @t94 @t98 @t85 @t95))) % 0.38/0.62 (step @p612 :rule bool-double-not-elim :args (@t90)) % 0.38/0.62 (step @p613 :rule bool-double-not-elim :args (@t91)) % 0.38/0.62 (step @p614 :rule bool-double-not-elim :args (@t69)) % 0.38/0.62 (step @p615 :rule nary_cong :premises (@p381 @p614 @p613 @p612) :args ((or @t82 @t116 @t115 @t113))) % 0.38/0.62 (assume-push @p1860 @t70) % 0.38/0.62 (assume-push @p1861 @t83) % 0.38/0.62 (assume-push @p1862 @t97) % 0.38/0.62 (assume-push @p1863 @t114) % 0.38/0.62 (step @p68 :rule evaluate :args (@t33)) % 0.38/0.62 (step @p620 :rule true_intro :premises (@p1860)) % 0.38/0.62 (step @p621 :rule false_intro :premises (@p1861)) % 0.38/0.62 (step @p622 :rule symm :premises (@p621)) % 0.38/0.62 (step @p623 :rule false_intro :premises (@p1862)) % 0.38/0.62 (step @p624 :rule trans :premises (@p623 @p622)) % 0.38/0.62 (step @p625 :rule cong :premises (@p624) :args (@t91)) % 0.38/0.62 (step @p626 :rule false_intro :premises (@p1863)) % 0.38/0.62 (step @p627 :rule symm :premises (@p626)) % 0.38/0.62 (step @p628 :rule trans :premises (@p627 @p625 @p620)) % 0.38/0.62 (step @p629 false :rule eq_resolve :premises (@p628 @p68)) % 0.38/0.62 (step-pop @p1864 :rule scope :premises (@p629)) % 0.38/0.62 (step-pop @p1865 :rule scope :premises (@p1864)) % 0.38/0.62 (step-pop @p1866 :rule scope :premises (@p1865)) % 0.38/0.62 (step-pop @p1867 :rule scope :premises (@p1866)) % 0.38/0.62 (step @p630 :rule process_scope :premises (@p1867) :args (false)) % 0.38/0.62 (assume-push @p1868 @t70) % 0.38/0.62 (assume-push @p1869 @t83) % 0.38/0.62 (assume-push @p1870 @t114) % 0.38/0.62 (assume-push @p1871 @t97) % 0.38/0.62 (step @p639 :rule and_intro :premises (@p1868 @p1869 @p1871 @p1870)) % 0.38/0.62 (step-pop @p1872 :rule scope :premises (@p639)) % 0.38/0.62 (step-pop @p1873 :rule scope :premises (@p1872)) % 0.38/0.62 (step-pop @p1874 :rule scope :premises (@p1873)) % 0.38/0.62 (step-pop @p1875 :rule scope :premises (@p1874)) % 0.38/0.62 (step @p640 :rule process_scope :premises (@p1875) :args (@t117)) % 0.38/0.62 (step @p645 :rule implies_elim :premises (@p640)) % 0.38/0.62 (step @p646 :rule resolution :premises (@p645 @p630) :args (true @t117)) % 0.38/0.62 (step @p647 :rule not_and :premises (@p646)) % 0.38/0.62 (step @p648 :rule eq_resolve :premises (@p647 @p615)) % 0.38/0.62 (step @p649 :rule reordering :premises (@p648) :args ((or @t69 @t90 @t91 @t82))) % 0.38/0.62 (step @p650 :rule chain_m_resolution :premises (@p649 @p611 @p461 @p440 @p417 @p380 @p340) :args ((or @t66 @t76 @t73) @t118 (@list @t90 @t91 @t86 @t69 @t74 @t70))) % 0.38/0.62 (step @p651 :rule equiv_elim2 :premises (@p338)) % 0.38/0.62 (step @p652 :rule equiv_elim1 :premises (@p439)) % 0.38/0.62 (step @p653 :rule reordering :premises (@p652) :args ((or @t86 @t77))) % 0.38/0.62 (step @p654 :rule bool-double-not-elim :args (@t70)) % 0.38/0.62 (step @p655 :rule nary_cong :premises (@p344 @p343 @p382 @p654) :args ((or @t77 @t76 @t83 @t119))) % 0.38/0.62 (assume-push @p1876 @t75) % 0.38/0.62 (assume-push @p1877 @t74) % 0.38/0.62 (assume-push @p1878 @t69) % 0.38/0.62 (assume-push @p1879 @t82) % 0.38/0.62 (step @p68 :rule evaluate :args (@t33)) % 0.38/0.62 (step @p660 :rule true_intro :premises (@p1876)) % 0.38/0.62 (step @p661 :rule true_intro :premises (@p1877)) % 0.38/0.62 (step @p662 :rule symm :premises (@p661)) % 0.38/0.62 (step @p663 :rule true_intro :premises (@p1878)) % 0.38/0.62 (step @p664 :rule trans :premises (@p663 @p662)) % 0.38/0.62 (step @p665 :rule cong :premises (@p664) :args (@t70)) % 0.38/0.62 (step @p666 :rule false_intro :premises (@p1879)) % 0.38/0.62 (step @p667 :rule symm :premises (@p666)) % 0.38/0.62 (step @p668 :rule trans :premises (@p667 @p665 @p660)) % 0.38/0.62 (step @p669 false :rule eq_resolve :premises (@p668 @p68)) % 0.38/0.62 (step-pop @p1880 :rule scope :premises (@p669)) % 0.38/0.62 (step-pop @p1881 :rule scope :premises (@p1880)) % 0.38/0.62 (step-pop @p1882 :rule scope :premises (@p1881)) % 0.38/0.62 (step-pop @p1883 :rule scope :premises (@p1882)) % 0.38/0.62 (step @p670 :rule process_scope :premises (@p1883) :args (false)) % 0.38/0.62 (assume-push @p1884 @t74) % 0.38/0.62 (assume-push @p1885 @t75) % 0.38/0.62 (assume-push @p1886 @t69) % 0.38/0.62 (assume-push @p1887 @t82) % 0.38/0.62 (step @p679 :rule and_intro :premises (@p1885 @p1884 @p1886 @p1887)) % 0.38/0.62 (step-pop @p1888 :rule scope :premises (@p679)) % 0.38/0.62 (step-pop @p1889 :rule scope :premises (@p1888)) % 0.38/0.62 (step-pop @p1890 :rule scope :premises (@p1889)) % 0.38/0.62 (step-pop @p1891 :rule scope :premises (@p1890)) % 0.38/0.62 (step @p680 :rule process_scope :premises (@p1891) :args (@t120)) % 0.38/0.62 (step @p685 :rule implies_elim :premises (@p680)) % 0.38/0.62 (step @p686 :rule resolution :premises (@p685 @p670) :args (true @t120)) % 0.38/0.62 (step @p687 :rule not_and :premises (@p686)) % 0.38/0.62 (step @p688 :rule eq_resolve :premises (@p687 @p655)) % 0.38/0.62 (step @p689 :rule reordering :premises (@p688) :args ((or @t70 @t76 @t77 @t83))) % 0.38/0.62 (step @p690 :rule nary_cong :premises (@p344 @p343 @p502 @p613) :args ((or @t77 @t76 @t97 @t115))) % 0.38/0.62 (assume-push @p1892 @t75) % 0.38/0.62 (assume-push @p1893 @t74) % 0.38/0.62 (assume-push @p1894 @t90) % 0.38/0.62 (assume-push @p1895 @t114) % 0.38/0.62 (step @p68 :rule evaluate :args (@t33)) % 0.38/0.62 (step @p695 :rule true_intro :premises (@p1892)) % 0.38/0.62 (step @p696 :rule true_intro :premises (@p1893)) % 0.38/0.62 (step @p697 :rule symm :premises (@p696)) % 0.38/0.62 (step @p698 :rule true_intro :premises (@p1894)) % 0.38/0.62 (step @p699 :rule trans :premises (@p698 @p697)) % 0.38/0.62 (step @p700 :rule cong :premises (@p699) :args (@t91)) % 0.38/0.62 (step @p701 :rule false_intro :premises (@p1895)) % 0.38/0.62 (step @p702 :rule symm :premises (@p701)) % 0.38/0.62 (step @p703 :rule trans :premises (@p702 @p700 @p695)) % 0.38/0.62 (step @p704 false :rule eq_resolve :premises (@p703 @p68)) % 0.38/0.62 (step-pop @p1896 :rule scope :premises (@p704)) % 0.38/0.62 (step-pop @p1897 :rule scope :premises (@p1896)) % 0.38/0.62 (step-pop @p1898 :rule scope :premises (@p1897)) % 0.38/0.62 (step-pop @p1899 :rule scope :premises (@p1898)) % 0.38/0.62 (step @p705 :rule process_scope :premises (@p1899) :args (false)) % 0.38/0.62 (assume-push @p1900 @t74) % 0.38/0.62 (assume-push @p1901 @t75) % 0.38/0.62 (assume-push @p1902 @t90) % 0.38/0.62 (assume-push @p1903 @t114) % 0.38/0.62 (step @p714 :rule and_intro :premises (@p1901 @p1900 @p1902 @p1903)) % 0.38/0.62 (step-pop @p1904 :rule scope :premises (@p714)) % 0.38/0.62 (step-pop @p1905 :rule scope :premises (@p1904)) % 0.38/0.62 (step-pop @p1906 :rule scope :premises (@p1905)) % 0.38/0.62 (step-pop @p1907 :rule scope :premises (@p1906)) % 0.38/0.62 (step @p715 :rule process_scope :premises (@p1907) :args (@t121)) % 0.38/0.62 (step @p720 :rule implies_elim :premises (@p715)) % 0.38/0.62 (step @p721 :rule resolution :premises (@p720 @p705) :args (true @t121)) % 0.38/0.62 (step @p722 :rule not_and :premises (@p721)) % 0.38/0.62 (step @p723 :rule eq_resolve :premises (@p722 @p690)) % 0.38/0.62 (step @p724 :rule reordering :premises (@p723) :args ((or @t91 @t76 @t77 @t97))) % 0.38/0.62 (step @p725 :rule equiv_elim2 :premises (@p481)) % 0.38/0.62 (step @p726 :rule bool-double-not-elim :args (@t95)) % 0.38/0.62 (step @p727 :rule refl :args (@t102)) % 0.38/0.62 (step @p728 :rule nary_cong :premises (@p503 @p727 @p538 @p726) :args ((or @t100 @t102 @t107 @t122))) % 0.38/0.62 (assume-push @p1908 @t86) % 0.38/0.62 (assume-push @p1909 @t85) % 0.38/0.62 (assume-push @p1910 @t94) % 0.38/0.62 (assume-push @p1911 @t106) % 0.38/0.62 (step @p68 :rule evaluate :args (@t33)) % 0.38/0.62 (step @p733 :rule true_intro :premises (@p1908)) % 0.38/0.62 (step @p734 :rule true_intro :premises (@p1909)) % 0.38/0.62 (step @p735 :rule symm :premises (@p734)) % 0.38/0.62 (step @p736 :rule true_intro :premises (@p1910)) % 0.38/0.62 (step @p737 :rule trans :premises (@p736 @p735)) % 0.38/0.62 (step @p738 :rule cong :premises (@p737) :args (@t95)) % 0.38/0.62 (step @p739 :rule false_intro :premises (@p1911)) % 0.38/0.62 (step @p740 :rule symm :premises (@p739)) % 0.38/0.62 (step @p741 :rule trans :premises (@p740 @p738 @p733)) % 0.38/0.62 (step @p742 false :rule eq_resolve :premises (@p741 @p68)) % 0.38/0.62 (step-pop @p1912 :rule scope :premises (@p742)) % 0.38/0.62 (step-pop @p1913 :rule scope :premises (@p1912)) % 0.38/0.62 (step-pop @p1914 :rule scope :premises (@p1913)) % 0.38/0.62 (step-pop @p1915 :rule scope :premises (@p1914)) % 0.38/0.62 (step @p743 :rule process_scope :premises (@p1915) :args (false)) % 0.38/0.62 (assume-push @p1916 @t85) % 0.38/0.62 (assume-push @p1917 @t86) % 0.38/0.62 (assume-push @p1918 @t94) % 0.38/0.62 (assume-push @p1919 @t106) % 0.38/0.62 (step @p752 :rule and_intro :premises (@p1917 @p1916 @p1918 @p1919)) % 0.38/0.62 (step-pop @p1920 :rule scope :premises (@p752)) % 0.38/0.62 (step-pop @p1921 :rule scope :premises (@p1920)) % 0.38/0.62 (step-pop @p1922 :rule scope :premises (@p1921)) % 0.38/0.62 (step-pop @p1923 :rule scope :premises (@p1922)) % 0.38/0.62 (step @p753 :rule process_scope :premises (@p1923) :args (@t123)) % 0.38/0.62 (step @p758 :rule implies_elim :premises (@p753)) % 0.38/0.62 (step @p759 :rule resolution :premises (@p758 @p743) :args (true @t123)) % 0.38/0.62 (step @p760 :rule not_and :premises (@p759)) % 0.38/0.62 (step @p761 :rule eq_resolve :premises (@p760 @p728)) % 0.38/0.62 (step @p762 :rule reordering :premises (@p761) :args ((or @t95 @t102 @t100 @t107))) % 0.38/0.62 (step @p763 :rule nary_cong :premises (@p500 @p612 @p726 @p574) :args ((or @t101 @t113 @t122 @t109))) % 0.38/0.62 (assume-push @p1924 @t98) % 0.38/0.62 (assume-push @p1925 @t97) % 0.38/0.62 (assume-push @p1926 @t107) % 0.38/0.62 (assume-push @p1927 @t106) % 0.38/0.62 (step @p68 :rule evaluate :args (@t33)) % 0.38/0.62 (step @p768 :rule true_intro :premises (@p1924)) % 0.38/0.62 (step @p769 :rule false_intro :premises (@p1925)) % 0.38/0.62 (step @p770 :rule symm :premises (@p769)) % 0.38/0.62 (step @p771 :rule false_intro :premises (@p1926)) % 0.38/0.62 (step @p772 :rule trans :premises (@p771 @p770)) % 0.38/0.62 (step @p773 :rule cong :premises (@p772) :args (@t95)) % 0.38/0.62 (step @p774 :rule false_intro :premises (@p1927)) % 0.38/0.62 (step @p775 :rule symm :premises (@p774)) % 0.38/0.62 (step @p776 :rule trans :premises (@p775 @p773 @p768)) % 0.38/0.62 (step @p777 false :rule eq_resolve :premises (@p776 @p68)) % 0.38/0.62 (step-pop @p1928 :rule scope :premises (@p777)) % 0.38/0.62 (step-pop @p1929 :rule scope :premises (@p1928)) % 0.38/0.62 (step-pop @p1930 :rule scope :premises (@p1929)) % 0.38/0.62 (step-pop @p1931 :rule scope :premises (@p1930)) % 0.38/0.62 (step @p778 :rule process_scope :premises (@p1931) :args (false)) % 0.38/0.62 (assume-push @p1932 @t98) % 0.38/0.62 (assume-push @p1933 @t97) % 0.38/0.62 (assume-push @p1934 @t106) % 0.38/0.62 (assume-push @p1935 @t107) % 0.38/0.62 (step @p787 :rule and_intro :premises (@p1932 @p1933 @p1935 @p1934)) % 0.38/0.62 (step-pop @p1936 :rule scope :premises (@p787)) % 0.38/0.62 (step-pop @p1937 :rule scope :premises (@p1936)) % 0.38/0.62 (step-pop @p1938 :rule scope :premises (@p1937)) % 0.38/0.62 (step-pop @p1939 :rule scope :premises (@p1938)) % 0.38/0.62 (step @p788 :rule process_scope :premises (@p1939) :args (@t124)) % 0.38/0.62 (step @p793 :rule implies_elim :premises (@p788)) % 0.38/0.62 (step @p794 :rule resolution :premises (@p793 @p778) :args (true @t124)) % 0.38/0.62 (step @p795 :rule not_and :premises (@p794)) % 0.38/0.62 (step @p796 :rule eq_resolve :premises (@p795 @p763)) % 0.38/0.62 (step @p797 :rule reordering :premises (@p796) :args ((or @t90 @t94 @t95 @t101))) % 0.38/0.62 (step @p798 :rule chain_m_resolution :premises (@p797 @p762 @p499 @p725) :args ((or @t90 @t102 @t100) (@list true false true) (@list @t94 @t98 @t95))) % 0.38/0.62 (step @p799 :rule refl :args (@t98)) % 0.38/0.62 (step @p800 :rule nary_cong :premises (@p727 @p575 @p612 @p799) :args ((or @t102 @t110 @t113 @t98))) % 0.38/0.62 (assume-push @p1940 @t86) % 0.38/0.62 (assume-push @p1941 @t100) % 0.38/0.62 (assume-push @p1942 @t97) % 0.38/0.62 (assume-push @p1943 @t86) % 0.38/0.62 (assume-push @p1944 @t100) % 0.38/0.62 (assume-push @p1945 @t97) % 0.38/0.62 (step @p807 :rule true_intro :premises (@p1940)) % 0.38/0.62 (step @p808 :rule false_intro :premises (@p1941)) % 0.38/0.62 (step @p809 :rule symm :premises (@p808)) % 0.38/0.62 (step @p810 :rule false_intro :premises (@p1942)) % 0.38/0.62 (step @p811 :rule trans :premises (@p810 @p809)) % 0.38/0.62 (step @p812 :rule cong :premises (@p811) :args (@t98)) % 0.38/0.62 (step @p813 :rule trans :premises (@p812 @p807)) % 0.38/0.62 (step @p814 :rule true_elim :premises (@p813)) % 0.38/0.62 (step-pop @p1946 :rule scope :premises (@p814)) % 0.38/0.62 (step-pop @p1947 :rule scope :premises (@p1946)) % 0.38/0.62 (step-pop @p1948 :rule scope :premises (@p1947)) % 0.38/0.62 (step @p815 :rule process_scope :premises (@p1948) :args (@t98)) % 0.38/0.62 (step @p819 :rule and_intro :premises (@p1940 @p1941 @p1942)) % 0.38/0.62 (step @p820 :rule modus_ponens :premises (@p819 @p815)) % 0.38/0.62 (step-pop @p1949 :rule scope :premises (@p820)) % 0.38/0.62 (step-pop @p1950 :rule scope :premises (@p1949)) % 0.38/0.62 (step-pop @p1951 :rule scope :premises (@p1950)) % 0.38/0.62 (step @p821 :rule process_scope :premises (@p1951) :args (@t98)) % 0.38/0.62 (step @p825 :rule implies_elim :premises (@p821)) % 0.38/0.62 (step @p826 :rule cnf_and_neg :args (@t125)) % 0.38/0.62 (step @p827 :rule resolution :premises (@p826 @p825) :args (true @t125)) % 0.38/0.62 (step @p828 :rule eq_resolve :premises (@p827 @p800)) % 0.38/0.62 (step @p829 :rule reordering :premises (@p828) :args ((or @t85 @t90 @t98 @t102))) % 0.38/0.62 (step @p830 :rule chain_m_resolution :premises (@p829 @p535 @p798 @p724 @p461 @p689 @p653) :args ((or @t70 @t76 @t77) @t118 (@list @t98 @t85 @t90 @t91 @t69 @t86))) % 0.38/0.62 (step @p831 :rule bool-double-not-elim :args (@t65)) % 0.38/0.62 (step @p832 :rule bool-double-not-elim :args (@t74)) % 0.38/0.62 (step @p833 :rule nary_cong :premises (@p343 @p341 @p832 @p831) :args ((or @t76 @t79 @t127 @t126))) % 0.38/0.62 (assume-push @p1952 @t78) % 0.38/0.62 (assume-push @p1953 @t73) % 0.38/0.62 (assume-push @p1954 @t77) % 0.38/0.62 (assume-push @p1955 @t75) % 0.38/0.62 (step @p350 :rule evaluate :args (@t80)) % 0.38/0.62 (step @p838 :rule false_intro :premises (@p1952)) % 0.38/0.62 (step @p839 :rule false_intro :premises (@p1953)) % 0.38/0.62 (step @p840 :rule symm :premises (@p839)) % 0.38/0.62 (step @p841 :rule false_intro :premises (@p1954)) % 0.38/0.62 (step @p842 :rule trans :premises (@p841 @p840)) % 0.38/0.62 (step @p843 :rule cong :premises (@p842) :args (@t75)) % 0.38/0.62 (step @p844 :rule true_intro :premises (@p1955)) % 0.38/0.62 (step @p845 :rule symm :premises (@p844)) % 0.38/0.62 (step @p846 :rule trans :premises (@p845 @p843 @p838)) % 0.38/0.62 (step @p847 false :rule eq_resolve :premises (@p846 @p350)) % 0.38/0.62 (step-pop @p1956 :rule scope :premises (@p847)) % 0.38/0.62 (step-pop @p1957 :rule scope :premises (@p1956)) % 0.38/0.62 (step-pop @p1958 :rule scope :premises (@p1957)) % 0.38/0.62 (step-pop @p1959 :rule scope :premises (@p1958)) % 0.38/0.62 (step @p848 :rule process_scope :premises (@p1959) :args (false)) % 0.38/0.62 (assume-push @p1960 @t75) % 0.38/0.62 (assume-push @p1961 @t78) % 0.38/0.62 (assume-push @p1962 @t77) % 0.38/0.62 (assume-push @p1963 @t73) % 0.38/0.62 (step @p857 :rule and_intro :premises (@p1961 @p1963 @p1962 @p1960)) % 0.38/0.62 (step-pop @p1964 :rule scope :premises (@p857)) % 0.38/0.62 (step-pop @p1965 :rule scope :premises (@p1964)) % 0.38/0.62 (step-pop @p1966 :rule scope :premises (@p1965)) % 0.38/0.62 (step-pop @p1967 :rule scope :premises (@p1966)) % 0.38/0.62 (step @p858 :rule process_scope :premises (@p1967) :args (@t128)) % 0.38/0.62 (step @p863 :rule implies_elim :premises (@p858)) % 0.38/0.62 (step @p864 :rule resolution :premises (@p863 @p848) :args (true @t128)) % 0.38/0.62 (step @p865 :rule not_and :premises (@p864)) % 0.38/0.62 (step @p866 :rule eq_resolve :premises (@p865 @p833)) % 0.38/0.62 (step @p867 :rule reordering :premises (@p866) :args ((or @t74 @t65 @t66 @t76))) % 0.38/0.62 (step @p868 :rule chain_m_resolution :premises (@p867 @p830 @p651 @p650) :args ((or @t66 @t76) @t129 (@list @t74 @t70 @t65))) % 0.38/0.62 (step @p869 :rule eq-symm :args (@t75 @t130)) % 0.38/0.62 (step @p870 :rule refl :args (@t130)) % 0.38/0.62 (step @p871 :rule refl :args (@t75)) % 0.38/0.62 (step @p872 :rule refl :args (@t131)) % 0.38/0.62 (step @p873 :rule cong :premises (@p872 @p871) :args ((= @t131 @t75))) % 0.38/0.62 (step @p874 :rule symm :premises (@p873)) % 0.38/0.62 (step @p875 :rule eq_resolve :premises (@p872 @p874)) % 0.38/0.62 (step @p876 :rule eq-refl :args (@t3)) % 0.38/0.62 (step @p877 :rule refl :args (@t3)) % 0.38/0.62 (step @p878 :rule cong :premises (@p877 @p438) :args (@t89)) % 0.38/0.62 (step @p879 :rule trans :premises (@p878 @p876)) % 0.38/0.62 (step @p880 :rule true_elim :premises (@p879)) % 0.38/0.62 (step @p881 :rule ho_cong :premises (@p310 @p880)) % 0.38/0.62 (step @p882 :rule trans :premises (@p881 @p875)) % 0.38/0.62 (step @p883 :rule cong :premises (@p882 @p870) :args (@t132)) % 0.38/0.62 (step @p884 :rule trans :premises (@p883 @p869)) % 0.38/0.62 (step @p885 :rule eq-symm :args (@t130 @t4)) % 0.38/0.62 (step @p886 :rule trans :premises (@p885 @p884)) % 0.38/0.62 (step @p887 :rule skolem_intro :args (@t130)) % 0.38/0.62 (step @p888 :rule eq_resolve :premises (@p887 @p886)) % 0.38/0.62 (step @p889 :rule equiv_elim1 :premises (@p888)) % 0.38/0.62 (step @p890 :rule reordering :premises (@p889) :args ((or @t75 @t133))) % 0.38/0.62 (step @p891 :rule bool-double-not-elim :args (@t51)) % 0.38/0.62 (step @p892 :rule bool-double-not-elim :args (@t130)) % 0.38/0.62 (step @p893 :rule refl :args (@t135)) % 0.38/0.62 (step @p894 :rule nary_cong :premises (@p893 @p258 @p892 @p891) :args ((or @t135 @t63 @t137 @t136))) % 0.38/0.62 (assume-push @p1968 @t62) % 0.38/0.62 (assume-push @p1969 @t60) % 0.38/0.62 (assume-push @p1970 @t133) % 0.38/0.62 (assume-push @p1971 @t134) % 0.38/0.62 (step @p350 :rule evaluate :args (@t80)) % 0.38/0.62 (step @p899 :rule false_intro :premises (@p1968)) % 0.38/0.62 (step @p900 :rule false_intro :premises (@p1969)) % 0.38/0.62 (step @p901 :rule symm :premises (@p900)) % 0.38/0.62 (step @p902 :rule false_intro :premises (@p1970)) % 0.38/0.62 (step @p903 :rule trans :premises (@p902 @p901)) % 0.38/0.62 (step @p904 :rule cong :premises (@p903) :args (@t134)) % 0.38/0.62 (step @p905 :rule true_intro :premises (@p1971)) % 0.38/0.62 (step @p906 :rule symm :premises (@p905)) % 0.38/0.62 (step @p907 :rule trans :premises (@p906 @p904 @p899)) % 0.38/0.62 (step @p908 false :rule eq_resolve :premises (@p907 @p350)) % 0.38/0.62 (step-pop @p1972 :rule scope :premises (@p908)) % 0.38/0.62 (step-pop @p1973 :rule scope :premises (@p1972)) % 0.38/0.62 (step-pop @p1974 :rule scope :premises (@p1973)) % 0.38/0.62 (step-pop @p1975 :rule scope :premises (@p1974)) % 0.38/0.62 (step @p909 :rule process_scope :premises (@p1975) :args (false)) % 0.38/0.62 (assume-push @p1976 @t134) % 0.38/0.62 (assume-push @p1977 @t62) % 0.38/0.62 (assume-push @p1978 @t133) % 0.38/0.62 (assume-push @p1979 @t60) % 0.38/0.62 (step @p918 :rule and_intro :premises (@p1977 @p1979 @p1978 @p1976)) % 0.38/0.62 (step-pop @p1980 :rule scope :premises (@p918)) % 0.38/0.62 (step-pop @p1981 :rule scope :premises (@p1980)) % 0.38/0.62 (step-pop @p1982 :rule scope :premises (@p1981)) % 0.38/0.62 (step-pop @p1983 :rule scope :premises (@p1982)) % 0.38/0.62 (step @p919 :rule process_scope :premises (@p1983) :args (@t138)) % 0.38/0.62 (step @p924 :rule implies_elim :premises (@p919)) % 0.38/0.62 (step @p925 :rule resolution :premises (@p924 @p909) :args (true @t138)) % 0.38/0.62 (step @p926 :rule not_and :premises (@p925)) % 0.38/0.62 (step @p927 :rule eq_resolve :premises (@p926 @p894)) % 0.38/0.62 (step @p928 :rule reordering :premises (@p927) :args ((or @t130 @t51 @t52 @t135))) % 0.38/0.62 (step @p929 :rule eq-symm :args (@t134 @t55)) % 0.38/0.62 (step @p930 :rule refl :args (@t55)) % 0.38/0.62 (step @p931 :rule refl :args (@t134)) % 0.38/0.62 (step @p932 :rule refl :args (@t139)) % 0.38/0.62 (step @p933 :rule cong :premises (@p932 @p931) :args ((= @t139 @t134))) % 0.38/0.62 (step @p934 :rule symm :premises (@p933)) % 0.38/0.62 (step @p935 :rule eq_resolve :premises (@p932 @p934)) % 0.38/0.62 (step @p936 :rule eq-refl :args (@t4)) % 0.38/0.62 (step @p937 :rule refl :args (@t4)) % 0.38/0.62 (step @p938 :rule cong :premises (@p937 @p887) :args (@t132)) % 0.38/0.62 (step @p939 :rule trans :premises (@p938 @p936)) % 0.38/0.62 (step @p940 :rule true_elim :premises (@p939)) % 0.38/0.62 (step @p941 :rule ho_cong :premises (@p49 @p940)) % 0.38/0.62 (step @p942 :rule trans :premises (@p941 @p935)) % 0.38/0.62 (step @p943 :rule cong :premises (@p942 @p930) :args (@t58)) % 0.38/0.62 (step @p944 :rule trans :premises (@p943 @p929)) % 0.38/0.62 (step @p945 :rule eq-symm :args (@t55 @t5)) % 0.38/0.62 (step @p946 :rule trans :premises (@p945 @p944)) % 0.38/0.62 (step @p947 :rule eq_resolve :premises (@p244 @p946)) % 0.38/0.62 (step @p948 :rule equiv_elim1 :premises (@p947)) % 0.38/0.62 (step @p949 :rule reordering :premises (@p948) :args ((or @t134 @t140))) % 0.38/0.62 (step @p950 :rule bool-double-not-elim :args (@t55)) % 0.38/0.62 (step @p951 :rule refl :args (@t141)) % 0.38/0.62 (step @p952 :rule nary_cong :premises (@p951 @p950 @p258 @p891) :args ((or @t141 @t142 @t63 @t136))) % 0.38/0.62 (assume-push @p1984 @t62) % 0.38/0.62 (assume-push @p1985 @t60) % 0.38/0.62 (assume-push @p1986 @t140) % 0.38/0.62 (assume-push @p1987 @t56) % 0.38/0.62 (step @p350 :rule evaluate :args (@t80)) % 0.38/0.62 (step @p957 :rule false_intro :premises (@p1984)) % 0.38/0.62 (step @p958 :rule false_intro :premises (@p1985)) % 0.38/0.62 (step @p959 :rule symm :premises (@p958)) % 0.38/0.62 (step @p960 :rule false_intro :premises (@p1986)) % 0.38/0.62 (step @p961 :rule trans :premises (@p960 @p959)) % 0.38/0.62 (step @p962 :rule cong :premises (@p961) :args (@t56)) % 0.38/0.62 (step @p963 :rule true_intro :premises (@p1987)) % 0.38/0.62 (step @p964 :rule symm :premises (@p963)) % 0.38/0.62 (step @p965 :rule trans :premises (@p964 @p962 @p957)) % 0.38/0.62 (step @p966 false :rule eq_resolve :premises (@p965 @p350)) % 0.38/0.62 (step-pop @p1988 :rule scope :premises (@p966)) % 0.38/0.62 (step-pop @p1989 :rule scope :premises (@p1988)) % 0.38/0.62 (step-pop @p1990 :rule scope :premises (@p1989)) % 0.38/0.62 (step-pop @p1991 :rule scope :premises (@p1990)) % 0.38/0.62 (step @p967 :rule process_scope :premises (@p1991) :args (false)) % 0.38/0.62 (assume-push @p1992 @t56) % 0.38/0.62 (assume-push @p1993 @t140) % 0.38/0.62 (assume-push @p1994 @t62) % 0.38/0.62 (assume-push @p1995 @t60) % 0.38/0.62 (step @p976 :rule and_intro :premises (@p1994 @p1995 @p1993 @p1992)) % 0.38/0.62 (step-pop @p1996 :rule scope :premises (@p976)) % 0.38/0.62 (step-pop @p1997 :rule scope :premises (@p1996)) % 0.38/0.62 (step-pop @p1998 :rule scope :premises (@p1997)) % 0.38/0.62 (step-pop @p1999 :rule scope :premises (@p1998)) % 0.38/0.62 (step @p977 :rule process_scope :premises (@p1999) :args (@t143)) % 0.38/0.62 (step @p982 :rule implies_elim :premises (@p977)) % 0.38/0.62 (step @p983 :rule resolution :premises (@p982 @p967) :args (true @t143)) % 0.38/0.62 (step @p984 :rule not_and :premises (@p983)) % 0.38/0.62 (step @p985 :rule eq_resolve :premises (@p984 @p952)) % 0.38/0.62 (step @p986 :rule reordering :premises (@p985) :args ((or @t55 @t51 @t52 @t141))) % 0.38/0.62 (step @p987 :rule chain_m_resolution :premises (@p986 @p949 @p928 @p890 @p868 @p318 @p296 @p257) :args ((or @t52 @t61 @t59) (@list true true true true true true false) (@list @t55 @t134 @t130 @t75 @t66 @t51 @t56))) % 0.38/0.62 (step @p988 :rule equiv_elim2 :premises (@p255)) % 0.38/0.62 (step @p989 :rule bool-double-not-elim :args (@t56)) % 0.38/0.62 (step @p990 :rule bool-double-not-elim :args (@t24)) % 0.38/0.62 (step @p991 :rule nary_cong :premises (@p260 @p990 @p989 @p950) :args ((or @t61 @t145 @t144 @t142))) % 0.38/0.62 (assume-push @p2000 @t25) % 0.38/0.62 (assume-push @p2001 @t59) % 0.38/0.62 (assume-push @p2002 @t140) % 0.38/0.62 (assume-push @p2003 @t141) % 0.38/0.62 (step @p68 :rule evaluate :args (@t33)) % 0.38/0.62 (step @p996 :rule true_intro :premises (@p2000)) % 0.38/0.62 (step @p997 :rule false_intro :premises (@p2001)) % 0.38/0.62 (step @p998 :rule symm :premises (@p997)) % 0.38/0.62 (step @p999 :rule false_intro :premises (@p2002)) % 0.38/0.62 (step @p1000 :rule trans :premises (@p999 @p998)) % 0.38/0.62 (step @p1001 :rule cong :premises (@p1000) :args (@t56)) % 0.38/0.62 (step @p1002 :rule false_intro :premises (@p2003)) % 0.38/0.62 (step @p1003 :rule symm :premises (@p1002)) % 0.38/0.62 (step @p1004 :rule trans :premises (@p1003 @p1001 @p996)) % 0.38/0.62 (step @p1005 false :rule eq_resolve :premises (@p1004 @p68)) % 0.38/0.62 (step-pop @p2004 :rule scope :premises (@p1005)) % 0.38/0.62 (step-pop @p2005 :rule scope :premises (@p2004)) % 0.38/0.62 (step-pop @p2006 :rule scope :premises (@p2005)) % 0.38/0.62 (step-pop @p2007 :rule scope :premises (@p2006)) % 0.38/0.62 (step @p1006 :rule process_scope :premises (@p2007) :args (false)) % 0.38/0.62 (assume-push @p2008 @t25) % 0.38/0.62 (assume-push @p2009 @t59) % 0.38/0.62 (assume-push @p2010 @t141) % 0.38/0.62 (assume-push @p2011 @t140) % 0.38/0.62 (step @p1015 :rule and_intro :premises (@p2008 @p2009 @p2011 @p2010)) % 0.38/0.62 (step-pop @p2012 :rule scope :premises (@p1015)) % 0.38/0.62 (step-pop @p2013 :rule scope :premises (@p2012)) % 0.38/0.62 (step-pop @p2014 :rule scope :premises (@p2013)) % 0.38/0.62 (step-pop @p2015 :rule scope :premises (@p2014)) % 0.38/0.62 (step @p1016 :rule process_scope :premises (@p2015) :args (@t146)) % 0.38/0.62 (step @p1021 :rule implies_elim :premises (@p1016)) % 0.38/0.62 (step @p1022 :rule resolution :premises (@p1021 @p1006) :args (true @t146)) % 0.38/0.62 (step @p1023 :rule not_and :premises (@p1022)) % 0.38/0.62 (step @p1024 :rule eq_resolve :premises (@p1023 @p991)) % 0.38/0.62 (step @p1025 :rule reordering :premises (@p1024) :args ((or @t24 @t55 @t56 @t61))) % 0.38/0.62 (step @p1026 :rule equiv_elim1 :premises (@p317)) % 0.38/0.62 (step @p1027 :rule reordering :premises (@p1026) :args ((or @t66 @t60))) % 0.38/0.62 (step @p1028 :rule refl :args (@t133)) % 0.38/0.62 (step @p1029 :rule nary_cong :premises (@p1028 @p893 @p259 @p258) :args ((or @t133 @t135 @t60 @t63))) % 0.38/0.62 (assume-push @p2016 @t62) % 0.38/0.62 (assume-push @p2017 @t51) % 0.38/0.62 (assume-push @p2018 @t130) % 0.38/0.62 (assume-push @p2019 @t134) % 0.38/0.62 (step @p350 :rule evaluate :args (@t80)) % 0.38/0.62 (step @p1034 :rule false_intro :premises (@p2016)) % 0.38/0.62 (step @p1035 :rule true_intro :premises (@p2017)) % 0.38/0.62 (step @p1036 :rule symm :premises (@p1035)) % 0.38/0.62 (step @p1037 :rule true_intro :premises (@p2018)) % 0.38/0.62 (step @p1038 :rule trans :premises (@p1037 @p1036)) % 0.38/0.62 (step @p1039 :rule cong :premises (@p1038) :args (@t134)) % 0.38/0.62 (step @p1040 :rule true_intro :premises (@p2019)) % 0.38/0.62 (step @p1041 :rule symm :premises (@p1040)) % 0.38/0.62 (step @p1042 :rule trans :premises (@p1041 @p1039 @p1034)) % 0.38/0.62 (step @p1043 false :rule eq_resolve :premises (@p1042 @p350)) % 0.38/0.62 (step-pop @p2020 :rule scope :premises (@p1043)) % 0.38/0.62 (step-pop @p2021 :rule scope :premises (@p2020)) % 0.38/0.62 (step-pop @p2022 :rule scope :premises (@p2021)) % 0.38/0.62 (step-pop @p2023 :rule scope :premises (@p2022)) % 0.38/0.62 (step @p1044 :rule process_scope :premises (@p2023) :args (false)) % 0.38/0.62 (assume-push @p2024 @t130) % 0.38/0.62 (assume-push @p2025 @t134) % 0.38/0.62 (assume-push @p2026 @t51) % 0.38/0.62 (assume-push @p2027 @t62) % 0.38/0.62 (step @p1053 :rule and_intro :premises (@p2027 @p2026 @p2024 @p2025)) % 0.38/0.62 (step-pop @p2028 :rule scope :premises (@p1053)) % 0.38/0.62 (step-pop @p2029 :rule scope :premises (@p2028)) % 0.38/0.62 (step-pop @p2030 :rule scope :premises (@p2029)) % 0.38/0.62 (step-pop @p2031 :rule scope :premises (@p2030)) % 0.38/0.62 (step @p1054 :rule process_scope :premises (@p2031) :args (@t147)) % 0.38/0.62 (step @p1059 :rule implies_elim :premises (@p1054)) % 0.38/0.62 (step @p1060 :rule resolution :premises (@p1059 @p1044) :args (true @t147)) % 0.38/0.62 (step @p1061 :rule not_and :premises (@p1060)) % 0.38/0.62 (step @p1062 :rule eq_resolve :premises (@p1061 @p1029)) % 0.38/0.62 (step @p1063 :rule reordering :premises (@p1062) :args ((or @t52 @t135 @t133 @t60))) % 0.38/0.62 (step @p1064 :rule bool-double-not-elim :args (@t75)) % 0.38/0.62 (step @p1065 :rule refl :args (@t78)) % 0.38/0.62 (step @p1066 :rule nary_cong :premises (@p344 @p342 @p1065 @p1064) :args ((or @t77 @t73 @t78 @t148))) % 0.38/0.62 (assume-push @p2032 @t66) % 0.38/0.62 (assume-push @p2033 @t65) % 0.38/0.62 (assume-push @p2034 @t74) % 0.38/0.62 (assume-push @p2035 @t76) % 0.38/0.62 (step @p68 :rule evaluate :args (@t33)) % 0.38/0.62 (step @p1071 :rule true_intro :premises (@p2032)) % 0.38/0.62 (step @p1072 :rule true_intro :premises (@p2033)) % 0.38/0.62 (step @p1073 :rule symm :premises (@p1072)) % 0.38/0.62 (step @p1074 :rule true_intro :premises (@p2034)) % 0.38/0.62 (step @p1075 :rule trans :premises (@p1074 @p1073)) % 0.38/0.62 (step @p1076 :rule cong :premises (@p1075) :args (@t75)) % 0.38/0.62 (step @p1077 :rule false_intro :premises (@p2035)) % 0.38/0.62 (step @p1078 :rule symm :premises (@p1077)) % 0.38/0.62 (step @p1079 :rule trans :premises (@p1078 @p1076 @p1071)) % 0.38/0.62 (step @p1080 false :rule eq_resolve :premises (@p1079 @p68)) % 0.38/0.62 (step-pop @p2036 :rule scope :premises (@p1080)) % 0.38/0.62 (step-pop @p2037 :rule scope :premises (@p2036)) % 0.38/0.62 (step-pop @p2038 :rule scope :premises (@p2037)) % 0.38/0.62 (step-pop @p2039 :rule scope :premises (@p2038)) % 0.38/0.62 (step @p1081 :rule process_scope :premises (@p2039) :args (false)) % 0.38/0.62 (assume-push @p2040 @t74) % 0.38/0.62 (assume-push @p2041 @t65) % 0.38/0.62 (assume-push @p2042 @t66) % 0.38/0.62 (assume-push @p2043 @t76) % 0.38/0.62 (step @p1090 :rule and_intro :premises (@p2042 @p2041 @p2040 @p2043)) % 0.38/0.62 (step-pop @p2044 :rule scope :premises (@p1090)) % 0.38/0.62 (step-pop @p2045 :rule scope :premises (@p2044)) % 0.38/0.62 (step-pop @p2046 :rule scope :premises (@p2045)) % 0.38/0.62 (step-pop @p2047 :rule scope :premises (@p2046)) % 0.38/0.62 (step @p1091 :rule process_scope :premises (@p2047) :args (@t149)) % 0.38/0.62 (step @p1096 :rule implies_elim :premises (@p1091)) % 0.38/0.62 (step @p1097 :rule resolution :premises (@p1096 @p1081) :args (true @t149)) % 0.38/0.62 (step @p1098 :rule not_and :premises (@p1097)) % 0.38/0.62 (step @p1099 :rule eq_resolve :premises (@p1098 @p1066)) % 0.38/0.62 (step @p1100 :rule reordering :premises (@p1099) :args ((or @t75 @t78 @t77 @t73))) % 0.38/0.62 (step @p1101 :rule refl :args (@t114)) % 0.38/0.62 (step @p1102 :rule nary_cong :premises (@p1064 @p832 @p612 @p1101) :args ((or @t148 @t127 @t113 @t114))) % 0.38/0.62 (assume-push @p2048 @t76) % 0.38/0.62 (assume-push @p2049 @t77) % 0.38/0.62 (assume-push @p2050 @t97) % 0.38/0.62 (assume-push @p2051 @t76) % 0.38/0.62 (assume-push @p2052 @t77) % 0.38/0.62 (assume-push @p2053 @t97) % 0.38/0.62 (step @p1109 :rule false_intro :premises (@p2048)) % 0.38/0.62 (step @p1110 :rule false_intro :premises (@p2049)) % 0.38/0.62 (step @p1111 :rule symm :premises (@p1110)) % 0.38/0.62 (step @p1112 :rule false_intro :premises (@p2050)) % 0.38/0.62 (step @p1113 :rule trans :premises (@p1112 @p1111)) % 0.38/0.62 (step @p1114 :rule cong :premises (@p1113) :args (@t91)) % 0.38/0.62 (step @p1115 :rule trans :premises (@p1114 @p1109)) % 0.38/0.62 (step @p1116 :rule false_elim :premises (@p1115)) % 0.38/0.62 (step-pop @p2054 :rule scope :premises (@p1116)) % 0.38/0.62 (step-pop @p2055 :rule scope :premises (@p2054)) % 0.38/0.62 (step-pop @p2056 :rule scope :premises (@p2055)) % 0.38/0.62 (step @p1117 :rule process_scope :premises (@p2056) :args (@t114)) % 0.38/0.62 (step @p1121 :rule and_intro :premises (@p2048 @p2049 @p2050)) % 0.38/0.62 (step @p1122 :rule modus_ponens :premises (@p1121 @p1117)) % 0.38/0.62 (step-pop @p2057 :rule scope :premises (@p1122)) % 0.38/0.62 (step-pop @p2058 :rule scope :premises (@p2057)) % 0.38/0.62 (step-pop @p2059 :rule scope :premises (@p2058)) % 0.38/0.62 (step @p1123 :rule process_scope :premises (@p2059) :args (@t114)) % 0.38/0.62 (step @p1127 :rule implies_elim :premises (@p1123)) % 0.38/0.62 (step @p1128 :rule cnf_and_neg :args (@t150)) % 0.38/0.62 (step @p1129 :rule resolution :premises (@p1128 @p1127) :args (true @t150)) % 0.38/0.62 (step @p1130 :rule eq_resolve :premises (@p1129 @p1102)) % 0.38/0.62 (step @p1131 :rule reordering :premises (@p1130) :args ((or @t74 @t75 @t90 @t114))) % 0.38/0.62 (step @p1132 :rule equiv_elim1 :premises (@p460)) % 0.38/0.62 (step @p1133 :rule reordering :premises (@p1132) :args ((or @t91 @t83))) % 0.38/0.62 (step @p1134 :rule chain_m_resolution :premises (@p649 @p1133 @p1131 @p611 @p440 @p1100 @p340) :args ((or @t75 @t78 @t73) @t118 (@list @t69 @t91 @t90 @t86 @t74 @t70))) % 0.38/0.62 (step @p1135 :rule nary_cong :premises (@p1065 @p831 @p654 @p614) :args ((or @t78 @t126 @t119 @t116))) % 0.38/0.62 (assume-push @p2060 @t66) % 0.38/0.62 (assume-push @p2061 @t73) % 0.38/0.62 (assume-push @p2062 @t83) % 0.38/0.62 (assume-push @p2063 @t82) % 0.38/0.62 (step @p68 :rule evaluate :args (@t33)) % 0.38/0.62 (step @p1140 :rule true_intro :premises (@p2060)) % 0.38/0.62 (step @p1141 :rule false_intro :premises (@p2061)) % 0.38/0.62 (step @p1142 :rule symm :premises (@p1141)) % 0.38/0.62 (step @p1143 :rule false_intro :premises (@p2062)) % 0.38/0.62 (step @p1144 :rule trans :premises (@p1143 @p1142)) % 0.38/0.62 (step @p1145 :rule cong :premises (@p1144) :args (@t70)) % 0.38/0.62 (step @p1146 :rule false_intro :premises (@p2063)) % 0.38/0.62 (step @p1147 :rule symm :premises (@p1146)) % 0.38/0.62 (step @p1148 :rule trans :premises (@p1147 @p1145 @p1140)) % 0.38/0.62 (step @p1149 false :rule eq_resolve :premises (@p1148 @p68)) % 0.38/0.62 (step-pop @p2064 :rule scope :premises (@p1149)) % 0.38/0.62 (step-pop @p2065 :rule scope :premises (@p2064)) % 0.38/0.62 (step-pop @p2066 :rule scope :premises (@p2065)) % 0.38/0.62 (step-pop @p2067 :rule scope :premises (@p2066)) % 0.38/0.62 (step @p1150 :rule process_scope :premises (@p2067) :args (false)) % 0.38/0.62 (assume-push @p2068 @t66) % 0.38/0.62 (assume-push @p2069 @t73) % 0.38/0.62 (assume-push @p2070 @t82) % 0.38/0.62 (assume-push @p2071 @t83) % 0.38/0.62 (step @p1159 :rule and_intro :premises (@p2068 @p2069 @p2071 @p2070)) % 0.38/0.62 (step-pop @p2072 :rule scope :premises (@p1159)) % 0.38/0.62 (step-pop @p2073 :rule scope :premises (@p2072)) % 0.38/0.62 (step-pop @p2074 :rule scope :premises (@p2073)) % 0.38/0.62 (step-pop @p2075 :rule scope :premises (@p2074)) % 0.38/0.62 (step @p1160 :rule process_scope :premises (@p2075) :args (@t151)) % 0.38/0.62 (step @p1165 :rule implies_elim :premises (@p1160)) % 0.38/0.62 (step @p1166 :rule resolution :premises (@p1165 @p1150) :args (true @t151)) % 0.38/0.62 (step @p1167 :rule not_and :premises (@p1166)) % 0.38/0.62 (step @p1168 :rule eq_resolve :premises (@p1167 @p1135)) % 0.38/0.62 (step @p1169 :rule reordering :premises (@p1168) :args ((or @t65 @t69 @t70 @t78))) % 0.38/0.62 (step @p1170 :rule nary_cong :premises (@p344 @p502 @p1101 @p1064) :args ((or @t77 @t97 @t114 @t148))) % 0.38/0.62 (assume-push @p2076 @t76) % 0.38/0.62 (assume-push @p2077 @t74) % 0.38/0.62 (assume-push @p2078 @t90) % 0.38/0.62 (assume-push @p2079 @t91) % 0.38/0.62 (step @p350 :rule evaluate :args (@t80)) % 0.38/0.62 (step @p1175 :rule false_intro :premises (@p2076)) % 0.38/0.62 (step @p1176 :rule true_intro :premises (@p2077)) % 0.38/0.62 (step @p1177 :rule symm :premises (@p1176)) % 0.38/0.62 (step @p1178 :rule true_intro :premises (@p2078)) % 0.38/0.62 (step @p1179 :rule trans :premises (@p1178 @p1177)) % 0.38/0.62 (step @p1180 :rule cong :premises (@p1179) :args (@t91)) % 0.38/0.62 (step @p1181 :rule true_intro :premises (@p2079)) % 0.38/0.62 (step @p1182 :rule symm :premises (@p1181)) % 0.38/0.62 (step @p1183 :rule trans :premises (@p1182 @p1180 @p1175)) % 0.38/0.62 (step @p1184 false :rule eq_resolve :premises (@p1183 @p350)) % 0.38/0.62 (step-pop @p2080 :rule scope :premises (@p1184)) % 0.38/0.62 (step-pop @p2081 :rule scope :premises (@p2080)) % 0.38/0.62 (step-pop @p2082 :rule scope :premises (@p2081)) % 0.38/0.62 (step-pop @p2083 :rule scope :premises (@p2082)) % 0.38/0.62 (step @p1185 :rule process_scope :premises (@p2083) :args (false)) % 0.38/0.62 (assume-push @p2084 @t74) % 0.38/0.62 (assume-push @p2085 @t90) % 0.38/0.62 (assume-push @p2086 @t91) % 0.38/0.62 (assume-push @p2087 @t76) % 0.38/0.62 (step @p1194 :rule and_intro :premises (@p2087 @p2084 @p2085 @p2086)) % 0.38/0.62 (step-pop @p2088 :rule scope :premises (@p1194)) % 0.38/0.62 (step-pop @p2089 :rule scope :premises (@p2088)) % 0.38/0.62 (step-pop @p2090 :rule scope :premises (@p2089)) % 0.38/0.62 (step-pop @p2091 :rule scope :premises (@p2090)) % 0.38/0.62 (step @p1195 :rule process_scope :premises (@p2091) :args (@t152)) % 0.38/0.62 (step @p1200 :rule implies_elim :premises (@p1195)) % 0.38/0.62 (step @p1201 :rule resolution :premises (@p1200 @p1185) :args (true @t152)) % 0.38/0.62 (step @p1202 :rule not_and :premises (@p1201)) % 0.38/0.62 (step @p1203 :rule eq_resolve :premises (@p1202 @p1170)) % 0.38/0.62 (step @p1204 :rule reordering :premises (@p1203) :args ((or @t75 @t77 @t114 @t97))) % 0.38/0.62 (step @p1205 :rule chain_m_resolution :premises (@p829 @p535 @p798) :args ((or @t90 @t102) (@list true true) (@list @t98 @t85))) % 0.38/0.62 (step @p1206 :rule chain_m_resolution :premises (@p1205 @p1204 @p653) :args ((or @t75 @t77 @t114) (@list true false) (@list @t90 @t86))) % 0.38/0.62 (step @p1207 :rule chain_m_resolution :premises (@p611 @p1131 @p440 @p1206 @p1133 @p1169 @p651 @p1134) :args ((or @t75 @t78) (@list false true true false false true true) (@list @t90 @t86 @t74 @t91 @t69 @t70 @t65))) % 0.38/0.62 (step @p1208 :rule equiv_elim2 :premises (@p888)) % 0.38/0.62 (step @p1209 :rule chain_m_resolution :premises (@p1208 @p1207 @p1063 @p1027) :args ((or @t52 @t135 @t60) (@list false true false) (@list @t75 @t130 @t66))) % 0.38/0.62 (step @p1210 :rule chain_m_resolution :premises (@p890 @p868 @p928 @p318 @p1209 @p949 @p1025 @p988 @p987 @p235 @p214 @p177 @p156 @p119 @p98 @p58 @p35) :args ((or @t30 @t28) (@list true false true true false false true true true true true true true true false true) (@list @t75 @t130 @t66 @t51 @t134 @t55 @t56 @t24 @t52 @t43 @t44 @t35 @t36 @t16 @t25 @t17))) % 0.38/0.62 (step @p1211 :rule equiv_elim2 :premises (@p56)) % 0.38/0.62 (step @p1212 :rule bool-double-not-elim :args (@t25)) % 0.38/0.62 (step @p1213 :rule refl :args (@t62)) % 0.38/0.62 (step @p1214 :rule nary_cong :premises (@p261 @p259 @p1213 @p1212) :args ((or @t59 @t60 @t62 @t153))) % 0.38/0.62 (assume-push @p2092 @t61) % 0.38/0.62 (assume-push @p2093 @t24) % 0.38/0.62 (assume-push @p2094 @t51) % 0.38/0.62 (assume-push @p2095 @t52) % 0.38/0.62 (step @p350 :rule evaluate :args (@t80)) % 0.38/0.62 (step @p1219 :rule false_intro :premises (@p2092)) % 0.38/0.62 (step @p1220 :rule true_intro :premises (@p2093)) % 0.38/0.62 (step @p1221 :rule symm :premises (@p1220)) % 0.38/0.62 (step @p1222 :rule true_intro :premises (@p2094)) % 0.38/0.62 (step @p1223 :rule trans :premises (@p1222 @p1221)) % 0.38/0.62 (step @p1224 :rule cong :premises (@p1223) :args (@t52)) % 0.38/0.62 (step @p1225 :rule true_intro :premises (@p2095)) % 0.38/0.62 (step @p1226 :rule symm :premises (@p1225)) % 0.38/0.62 (step @p1227 :rule trans :premises (@p1226 @p1224 @p1219)) % 0.38/0.62 (step @p1228 false :rule eq_resolve :premises (@p1227 @p350)) % 0.38/0.62 (step-pop @p2096 :rule scope :premises (@p1228)) % 0.38/0.62 (step-pop @p2097 :rule scope :premises (@p2096)) % 0.38/0.62 (step-pop @p2098 :rule scope :premises (@p2097)) % 0.38/0.62 (step-pop @p2099 :rule scope :premises (@p2098)) % 0.38/0.62 (step @p1229 :rule process_scope :premises (@p2099) :args (false)) % 0.38/0.62 (assume-push @p2100 @t24) % 0.38/0.62 (assume-push @p2101 @t51) % 0.38/0.62 (assume-push @p2102 @t52) % 0.38/0.62 (assume-push @p2103 @t61) % 0.38/0.62 (step @p1238 :rule and_intro :premises (@p2103 @p2100 @p2101 @p2102)) % 0.38/0.62 (step-pop @p2104 :rule scope :premises (@p1238)) % 0.38/0.62 (step-pop @p2105 :rule scope :premises (@p2104)) % 0.38/0.62 (step-pop @p2106 :rule scope :premises (@p2105)) % 0.38/0.62 (step-pop @p2107 :rule scope :premises (@p2106)) % 0.38/0.62 (step @p1239 :rule process_scope :premises (@p2107) :args (@t154)) % 0.38/0.62 (step @p1244 :rule implies_elim :premises (@p1239)) % 0.38/0.62 (step @p1245 :rule resolution :premises (@p1244 @p1229) :args (true @t154)) % 0.38/0.62 (step @p1246 :rule not_and :premises (@p1245)) % 0.38/0.62 (step @p1247 :rule eq_resolve :premises (@p1246 @p1214)) % 0.38/0.62 (step @p1248 :rule reordering :premises (@p1247) :args ((or @t25 @t59 @t62 @t60))) % 0.38/0.62 (step @p1249 :rule refl :args (@t140)) % 0.38/0.62 (step @p1250 :rule nary_cong :premises (@p261 @p1249 @p951 @p1212) :args ((or @t59 @t140 @t141 @t153))) % 0.38/0.62 (assume-push @p2108 @t61) % 0.38/0.62 (assume-push @p2109 @t24) % 0.38/0.62 (assume-push @p2110 @t55) % 0.38/0.62 (assume-push @p2111 @t56) % 0.38/0.62 (step @p350 :rule evaluate :args (@t80)) % 0.38/0.62 (step @p1255 :rule false_intro :premises (@p2108)) % 0.38/0.62 (step @p1256 :rule true_intro :premises (@p2109)) % 0.38/0.62 (step @p1257 :rule symm :premises (@p1256)) % 0.38/0.62 (step @p1258 :rule true_intro :premises (@p2110)) % 0.38/0.62 (step @p1259 :rule trans :premises (@p1258 @p1257)) % 0.38/0.62 (step @p1260 :rule cong :premises (@p1259) :args (@t56)) % 0.38/0.62 (step @p1261 :rule true_intro :premises (@p2111)) % 0.38/0.62 (step @p1262 :rule symm :premises (@p1261)) % 0.38/0.62 (step @p1263 :rule trans :premises (@p1262 @p1260 @p1255)) % 0.38/0.62 (step @p1264 false :rule eq_resolve :premises (@p1263 @p350)) % 0.38/0.62 (step-pop @p2112 :rule scope :premises (@p1264)) % 0.38/0.62 (step-pop @p2113 :rule scope :premises (@p2112)) % 0.38/0.62 (step-pop @p2114 :rule scope :premises (@p2113)) % 0.38/0.62 (step-pop @p2115 :rule scope :premises (@p2114)) % 0.38/0.62 (step @p1265 :rule process_scope :premises (@p2115) :args (false)) % 0.38/0.62 (assume-push @p2116 @t24) % 0.38/0.62 (assume-push @p2117 @t55) % 0.38/0.62 (assume-push @p2118 @t56) % 0.38/0.62 (assume-push @p2119 @t61) % 0.38/0.62 (step @p1274 :rule and_intro :premises (@p2119 @p2116 @p2117 @p2118)) % 0.38/0.62 (step-pop @p2120 :rule scope :premises (@p1274)) % 0.38/0.62 (step-pop @p2121 :rule scope :premises (@p2120)) % 0.38/0.62 (step-pop @p2122 :rule scope :premises (@p2121)) % 0.38/0.62 (step-pop @p2123 :rule scope :premises (@p2122)) % 0.38/0.62 (step @p1275 :rule process_scope :premises (@p2123) :args (@t155)) % 0.38/0.62 (step @p1280 :rule implies_elim :premises (@p1275)) % 0.38/0.62 (step @p1281 :rule resolution :premises (@p1280 @p1265) :args (true @t155)) % 0.38/0.62 (step @p1282 :rule not_and :premises (@p1281)) % 0.38/0.62 (step @p1283 :rule eq_resolve :premises (@p1282 @p1250)) % 0.38/0.62 (step @p1284 :rule reordering :premises (@p1283) :args ((or @t25 @t59 @t141 @t140))) % 0.38/0.62 (step @p1285 :rule equiv_elim2 :premises (@p947)) % 0.38/0.62 (step @p1286 :rule bool-double-not-elim :args (@t134)) % 0.38/0.62 (step @p1287 :rule nary_cong :premises (@p951 @p950 @p1286 @p892) :args ((or @t141 @t142 (not @t135) @t137))) % 0.38/0.62 (assume-push @p2124 @t56) % 0.38/0.62 (assume-push @p2125 @t140) % 0.38/0.62 (assume-push @p2126 @t133) % 0.38/0.62 (assume-push @p2127 @t135) % 0.38/0.62 (step @p68 :rule evaluate :args (@t33)) % 0.38/0.62 (step @p1292 :rule true_intro :premises (@p2124)) % 0.38/0.62 (step @p1293 :rule false_intro :premises (@p2125)) % 0.38/0.62 (step @p1294 :rule symm :premises (@p1293)) % 0.38/0.62 (step @p1295 :rule false_intro :premises (@p2126)) % 0.38/0.62 (step @p1296 :rule trans :premises (@p1295 @p1294)) % 0.38/0.62 (step @p1297 :rule cong :premises (@p1296) :args (@t134)) % 0.38/0.62 (step @p1298 :rule false_intro :premises (@p2127)) % 0.38/0.62 (step @p1299 :rule symm :premises (@p1298)) % 0.38/0.62 (step @p1300 :rule trans :premises (@p1299 @p1297 @p1292)) % 0.38/0.62 (step @p1301 false :rule eq_resolve :premises (@p1300 @p68)) % 0.38/0.62 (step-pop @p2128 :rule scope :premises (@p1301)) % 0.38/0.62 (step-pop @p2129 :rule scope :premises (@p2128)) % 0.38/0.62 (step-pop @p2130 :rule scope :premises (@p2129)) % 0.38/0.62 (step-pop @p2131 :rule scope :premises (@p2130)) % 0.38/0.62 (step @p1302 :rule process_scope :premises (@p2131) :args (false)) % 0.38/0.62 (assume-push @p2132 @t56) % 0.38/0.62 (assume-push @p2133 @t140) % 0.38/0.62 (assume-push @p2134 @t135) % 0.38/0.62 (assume-push @p2135 @t133) % 0.38/0.62 (step @p1311 :rule and_intro :premises (@p2132 @p2133 @p2135 @p2134)) % 0.38/0.62 (step-pop @p2136 :rule scope :premises (@p1311)) % 0.38/0.62 (step-pop @p2137 :rule scope :premises (@p2136)) % 0.38/0.62 (step-pop @p2138 :rule scope :premises (@p2137)) % 0.38/0.62 (step-pop @p2139 :rule scope :premises (@p2138)) % 0.38/0.62 (step @p1312 :rule process_scope :premises (@p2139) :args (@t156)) % 0.38/0.62 (step @p1317 :rule implies_elim :premises (@p1312)) % 0.38/0.62 (step @p1318 :rule resolution :premises (@p1317 @p1302) :args (true @t156)) % 0.38/0.62 (step @p1319 :rule not_and :premises (@p1318)) % 0.38/0.62 (step @p1320 :rule eq_resolve :premises (@p1319 @p1287)) % 0.38/0.62 (step @p1321 :rule reordering :premises (@p1320) :args ((or @t55 @t130 @t134 @t141))) % 0.38/0.62 (step @p1322 :rule chain_m_resolution :premises (@p890 @p1321 @p868 @p1285 @p318 @p1284 @p1248 @p257) :args ((or @t25 @t59 @t62) (@list false true true true true true false) (@list @t130 @t75 @t134 @t66 @t55 @t51 @t56))) % 0.38/0.62 (assume-push @p2140 @t130) % 0.38/0.62 (assume-push @p2141 @t51) % 0.38/0.62 (assume-push @p2142 @t52) % 0.38/0.62 (assume-push @p2143 @t52) % 0.38/0.62 (assume-push @p2144 @t51) % 0.38/0.62 (assume-push @p2145 @t130) % 0.38/0.62 (step @p1329 :rule true_intro :premises (@p2142)) % 0.38/0.62 (step @p1330 :rule true_intro :premises (@p2141)) % 0.38/0.62 (step @p1331 :rule symm :premises (@p1330)) % 0.38/0.62 (step @p1332 :rule true_intro :premises (@p2140)) % 0.38/0.62 (step @p1333 :rule trans :premises (@p1332 @p1331)) % 0.38/0.62 (step @p1334 :rule cong :premises (@p1333) :args (@t134)) % 0.38/0.62 (step @p1335 :rule trans :premises (@p1334 @p1329)) % 0.38/0.62 (step @p1336 :rule true_elim :premises (@p1335)) % 0.38/0.62 (step-pop @p2146 :rule scope :premises (@p1336)) % 0.38/0.62 (step-pop @p2147 :rule scope :premises (@p2146)) % 0.38/0.62 (step-pop @p2148 :rule scope :premises (@p2147)) % 0.38/0.62 (step @p1337 :rule process_scope :premises (@p2148) :args (@t134)) % 0.38/0.62 (step @p1341 :rule and_intro :premises (@p2142 @p2141 @p2140)) % 0.38/0.62 (step @p1342 :rule modus_ponens :premises (@p1341 @p1337)) % 0.38/0.62 (step-pop @p2149 :rule scope :premises (@p1342)) % 0.38/0.62 (step-pop @p2150 :rule scope :premises (@p2149)) % 0.38/0.62 (step-pop @p2151 :rule scope :premises (@p2150)) % 0.38/0.62 (step @p1343 :rule process_scope :premises (@p2151) :args (@t134)) % 0.38/0.62 (step @p1347 :rule implies_elim :premises (@p1343)) % 0.38/0.62 (step @p1348 :rule cnf_and_neg :args (@t157)) % 0.38/0.62 (step @p1349 :rule resolution :premises (@p1348 @p1347) :args (true @t157)) % 0.38/0.62 (step @p1350 :rule reordering :premises (@p1349) :args ((or @t134 @t62 @t133 @t60))) % 0.38/0.62 (step @p1351 :rule nary_cong :premises (@p1249 @p259 @p1213 @p989) :args ((or @t140 @t60 @t62 @t144))) % 0.38/0.62 (assume-push @p2152 @t52) % 0.38/0.62 (assume-push @p2153 @t51) % 0.38/0.62 (assume-push @p2154 @t55) % 0.38/0.62 (assume-push @p2155 @t141) % 0.38/0.62 (step @p68 :rule evaluate :args (@t33)) % 0.38/0.62 (step @p1356 :rule true_intro :premises (@p2152)) % 0.38/0.62 (step @p1357 :rule true_intro :premises (@p2153)) % 0.38/0.62 (step @p1358 :rule symm :premises (@p1357)) % 0.38/0.62 (step @p1359 :rule true_intro :premises (@p2154)) % 0.38/0.62 (step @p1360 :rule trans :premises (@p1359 @p1358)) % 0.38/0.62 (step @p1361 :rule cong :premises (@p1360) :args (@t56)) % 0.38/0.62 (step @p1362 :rule false_intro :premises (@p2155)) % 0.38/0.62 (step @p1363 :rule symm :premises (@p1362)) % 0.38/0.62 (step @p1364 :rule trans :premises (@p1363 @p1361 @p1356)) % 0.38/0.62 (step @p1365 false :rule eq_resolve :premises (@p1364 @p68)) % 0.38/0.62 (step-pop @p2156 :rule scope :premises (@p1365)) % 0.38/0.62 (step-pop @p2157 :rule scope :premises (@p2156)) % 0.38/0.62 (step-pop @p2158 :rule scope :premises (@p2157)) % 0.38/0.62 (step-pop @p2159 :rule scope :premises (@p2158)) % 0.38/0.62 (step @p1366 :rule process_scope :premises (@p2159) :args (false)) % 0.38/0.62 (assume-push @p2160 @t55) % 0.38/0.62 (assume-push @p2161 @t51) % 0.38/0.62 (assume-push @p2162 @t52) % 0.38/0.62 (assume-push @p2163 @t141) % 0.38/0.62 (step @p1375 :rule and_intro :premises (@p2162 @p2161 @p2160 @p2163)) % 0.38/0.62 (step-pop @p2164 :rule scope :premises (@p1375)) % 0.38/0.62 (step-pop @p2165 :rule scope :premises (@p2164)) % 0.38/0.62 (step-pop @p2166 :rule scope :premises (@p2165)) % 0.38/0.62 (step-pop @p2167 :rule scope :premises (@p2166)) % 0.38/0.62 (step @p1376 :rule process_scope :premises (@p2167) :args (@t158)) % 0.38/0.62 (step @p1381 :rule implies_elim :premises (@p1376)) % 0.38/0.62 (step @p1382 :rule resolution :premises (@p1381 @p1366) :args (true @t158)) % 0.38/0.62 (step @p1383 :rule not_and :premises (@p1382)) % 0.38/0.62 (step @p1384 :rule eq_resolve :premises (@p1383 @p1351)) % 0.38/0.62 (step @p1385 :rule reordering :premises (@p1384) :args ((or @t56 @t140 @t62 @t60))) % 0.38/0.62 (step @p1386 :rule chain_m_resolution :premises (@p1385 @p1285 @p1350 @p1208 @p1207 @p1027) :args ((or @t56 @t62 @t60) (@list false false false false false) (@list @t55 @t134 @t130 @t75 @t66))) % 0.38/0.62 (step @p1387 :rule nary_cong :premises (@p1213 @p1212 @p990 @p891) :args ((or @t62 @t153 @t145 @t136))) % 0.38/0.62 (assume-push @p2168 @t61) % 0.38/0.62 (assume-push @p2169 @t59) % 0.38/0.62 (assume-push @p2170 @t60) % 0.38/0.62 (assume-push @p2171 @t52) % 0.38/0.62 (step @p350 :rule evaluate :args (@t80)) % 0.38/0.62 (step @p1392 :rule false_intro :premises (@p2168)) % 0.38/0.62 (step @p1393 :rule false_intro :premises (@p2169)) % 0.38/0.62 (step @p1394 :rule symm :premises (@p1393)) % 0.38/0.62 (step @p1395 :rule false_intro :premises (@p2170)) % 0.38/0.62 (step @p1396 :rule trans :premises (@p1395 @p1394)) % 0.38/0.62 (step @p1397 :rule cong :premises (@p1396) :args (@t52)) % 0.38/0.62 (step @p1398 :rule true_intro :premises (@p2171)) % 0.38/0.62 (step @p1399 :rule symm :premises (@p1398)) % 0.38/0.62 (step @p1400 :rule trans :premises (@p1399 @p1397 @p1392)) % 0.38/0.62 (step @p1401 false :rule eq_resolve :premises (@p1400 @p350)) % 0.38/0.62 (step-pop @p2172 :rule scope :premises (@p1401)) % 0.38/0.62 (step-pop @p2173 :rule scope :premises (@p2172)) % 0.38/0.62 (step-pop @p2174 :rule scope :premises (@p2173)) % 0.38/0.62 (step-pop @p2175 :rule scope :premises (@p2174)) % 0.38/0.62 (step @p1402 :rule process_scope :premises (@p2175) :args (false)) % 0.38/0.62 (assume-push @p2176 @t52) % 0.38/0.62 (assume-push @p2177 @t61) % 0.38/0.62 (assume-push @p2178 @t59) % 0.38/0.62 (assume-push @p2179 @t60) % 0.38/0.62 (step @p1411 :rule and_intro :premises (@p2177 @p2178 @p2179 @p2176)) % 0.38/0.62 (step-pop @p2180 :rule scope :premises (@p1411)) % 0.38/0.62 (step-pop @p2181 :rule scope :premises (@p2180)) % 0.38/0.62 (step-pop @p2182 :rule scope :premises (@p2181)) % 0.38/0.62 (step-pop @p2183 :rule scope :premises (@p2182)) % 0.38/0.62 (step @p1412 :rule process_scope :premises (@p2183) :args (@t159)) % 0.38/0.62 (step @p1417 :rule implies_elim :premises (@p1412)) % 0.38/0.62 (step @p1418 :rule resolution :premises (@p1417 @p1402) :args (true @t159)) % 0.38/0.62 (step @p1419 :rule not_and :premises (@p1418)) % 0.38/0.62 (step @p1420 :rule eq_resolve :premises (@p1419 @p1387)) % 0.38/0.62 (step @p1421 :rule reordering :premises (@p1420) :args ((or @t24 @t25 @t51 @t62))) % 0.38/0.62 (step @p1422 :rule chain_m_resolution :premises (@p1421 @p1386 @p988 @p1322) :args ((or @t25 @t62) @t129 (@list @t51 @t56 @t24))) % 0.38/0.62 (step @p1423 :rule equiv_elim1 :premises (@p234)) % 0.38/0.62 (step @p1424 :rule reordering :premises (@p1423) :args ((or @t52 @t47))) % 0.38/0.62 (step @p1425 :rule bool-double-not-elim :args (@t43)) % 0.38/0.62 (step @p1426 :rule bool-double-not-elim :args (@t18)) % 0.38/0.62 (step @p1427 :rule nary_cong :premises (@p61 @p1426 @p178 @p1425) :args ((or @t30 @t161 @t49 @t160))) % 0.38/0.62 (assume-push @p2184 @t19) % 0.38/0.62 (assume-push @p2185 @t28) % 0.38/0.62 (assume-push @p2186 @t47) % 0.38/0.62 (assume-push @p2187 @t48) % 0.38/0.62 (step @p68 :rule evaluate :args (@t33)) % 0.38/0.62 (step @p1432 :rule true_intro :premises (@p2184)) % 0.38/0.62 (step @p1433 :rule false_intro :premises (@p2185)) % 0.38/0.62 (step @p1434 :rule symm :premises (@p1433)) % 0.38/0.62 (step @p1435 :rule false_intro :premises (@p2186)) % 0.38/0.62 (step @p1436 :rule trans :premises (@p1435 @p1434)) % 0.38/0.62 (step @p1437 :rule cong :premises (@p1436) :args (@t44)) % 0.38/0.62 (step @p1438 :rule false_intro :premises (@p2187)) % 0.38/0.62 (step @p1439 :rule symm :premises (@p1438)) % 0.38/0.62 (step @p1440 :rule trans :premises (@p1439 @p1437 @p1432)) % 0.38/0.62 (step @p1441 false :rule eq_resolve :premises (@p1440 @p68)) % 0.38/0.62 (step-pop @p2188 :rule scope :premises (@p1441)) % 0.38/0.62 (step-pop @p2189 :rule scope :premises (@p2188)) % 0.38/0.62 (step-pop @p2190 :rule scope :premises (@p2189)) % 0.38/0.62 (step-pop @p2191 :rule scope :premises (@p2190)) % 0.38/0.62 (step @p1442 :rule process_scope :premises (@p2191) :args (false)) % 0.38/0.62 (assume-push @p2192 @t19) % 0.38/0.62 (assume-push @p2193 @t28) % 0.38/0.62 (assume-push @p2194 @t48) % 0.38/0.62 (assume-push @p2195 @t47) % 0.38/0.62 (step @p1451 :rule and_intro :premises (@p2192 @p2193 @p2195 @p2194)) % 0.38/0.62 (step-pop @p2196 :rule scope :premises (@p1451)) % 0.38/0.62 (step-pop @p2197 :rule scope :premises (@p2196)) % 0.38/0.62 (step-pop @p2198 :rule scope :premises (@p2197)) % 0.38/0.62 (step-pop @p2199 :rule scope :premises (@p2198)) % 0.38/0.62 (step @p1452 :rule process_scope :premises (@p2199) :args (@t162)) % 0.38/0.62 (step @p1457 :rule implies_elim :premises (@p1452)) % 0.38/0.62 (step @p1458 :rule resolution :premises (@p1457 @p1442) :args (true @t162)) % 0.38/0.62 (step @p1459 :rule not_and :premises (@p1458)) % 0.38/0.62 (step @p1460 :rule eq_resolve :premises (@p1459 @p1427)) % 0.38/0.62 (step @p1461 :rule reordering :premises (@p1460) :args ((or @t18 @t43 @t44 @t30))) % 0.38/0.62 (step @p1462 :rule equiv_elim1 :premises (@p118)) % 0.38/0.62 (step @p1463 :rule reordering :premises (@p1462) :args ((or @t36 @t29))) % 0.38/0.62 (step @p1464 :rule refl :args (@t40)) % 0.38/0.62 (step @p1465 :rule nary_cong :premises (@p60 @p121 @p1464 @p59) :args ((or @t29 @t39 @t40 @t32))) % 0.38/0.62 (assume-push @p2200 @t31) % 0.38/0.62 (assume-push @p2201 @t16) % 0.38/0.62 (assume-push @p2202 @t35) % 0.38/0.62 (assume-push @p2203 @t36) % 0.38/0.62 (step @p350 :rule evaluate :args (@t80)) % 0.38/0.62 (step @p1470 :rule false_intro :premises (@p2200)) % 0.38/0.62 (step @p1471 :rule true_intro :premises (@p2201)) % 0.38/0.62 (step @p1472 :rule symm :premises (@p1471)) % 0.38/0.62 (step @p1473 :rule true_intro :premises (@p2202)) % 0.38/0.62 (step @p1474 :rule trans :premises (@p1473 @p1472)) % 0.38/0.62 (step @p1475 :rule cong :premises (@p1474) :args (@t36)) % 0.38/0.62 (step @p1476 :rule true_intro :premises (@p2203)) % 0.38/0.62 (step @p1477 :rule symm :premises (@p1476)) % 0.38/0.62 (step @p1478 :rule trans :premises (@p1477 @p1475 @p1470)) % 0.38/0.62 (step @p1479 false :rule eq_resolve :premises (@p1478 @p350)) % 0.38/0.62 (step-pop @p2204 :rule scope :premises (@p1479)) % 0.38/0.62 (step-pop @p2205 :rule scope :premises (@p2204)) % 0.38/0.62 (step-pop @p2206 :rule scope :premises (@p2205)) % 0.38/0.62 (step-pop @p2207 :rule scope :premises (@p2206)) % 0.38/0.62 (step @p1480 :rule process_scope :premises (@p2207) :args (false)) % 0.38/0.62 (assume-push @p2208 @t16) % 0.38/0.62 (assume-push @p2209 @t35) % 0.38/0.62 (assume-push @p2210 @t36) % 0.38/0.62 (assume-push @p2211 @t31) % 0.38/0.62 (step @p1489 :rule and_intro :premises (@p2211 @p2208 @p2209 @p2210)) % 0.38/0.63 (step-pop @p2212 :rule scope :premises (@p1489)) % 0.38/0.63 (step-pop @p2213 :rule scope :premises (@p2212)) % 0.38/0.63 (step-pop @p2214 :rule scope :premises (@p2213)) % 0.38/0.63 (step-pop @p2215 :rule scope :premises (@p2214)) % 0.38/0.63 (step @p1490 :rule process_scope :premises (@p2215) :args (@t163)) % 0.38/0.63 (step @p1495 :rule implies_elim :premises (@p1490)) % 0.38/0.63 (step @p1496 :rule resolution :premises (@p1495 @p1480) :args (true @t163)) % 0.38/0.63 (step @p1497 :rule not_and :premises (@p1496)) % 0.38/0.63 (step @p1498 :rule eq_resolve :premises (@p1497 @p1465)) % 0.38/0.63 (step @p1499 :rule reordering :premises (@p1498) :args ((or @t17 @t29 @t40 @t39))) % 0.38/0.63 (step @p1500 :rule chain_m_resolution :premises (@p1499 @p1463) :args ((or @t17 @t29 @t39) @t105 @t164)) % 0.38/0.63 (step @p1501 :rule bool-double-not-elim :args (@t16)) % 0.38/0.63 (step @p1502 :rule nary_cong :premises (@p61 @p59 @p1426 @p1501) :args ((or @t30 @t32 @t161 @t165))) % 0.38/0.63 (assume-push @p2216 @t19) % 0.38/0.63 (assume-push @p2217 @t28) % 0.38/0.63 (assume-push @p2218 @t29) % 0.38/0.63 (assume-push @p2219 @t31) % 0.38/0.63 (step @p68 :rule evaluate :args (@t33)) % 0.38/0.63 (step @p1507 :rule true_intro :premises (@p2216)) % 0.38/0.63 (step @p1508 :rule false_intro :premises (@p2217)) % 0.38/0.63 (step @p1509 :rule symm :premises (@p1508)) % 0.38/0.63 (step @p1510 :rule false_intro :premises (@p2218)) % 0.38/0.63 (step @p1511 :rule trans :premises (@p1510 @p1509)) % 0.38/0.63 (step @p1512 :rule cong :premises (@p1511) :args (@t17)) % 0.38/0.63 (step @p1513 :rule false_intro :premises (@p2219)) % 0.38/0.63 (step @p1514 :rule symm :premises (@p1513)) % 0.38/0.63 (step @p1515 :rule trans :premises (@p1514 @p1512 @p1507)) % 0.38/0.63 (step @p1516 false :rule eq_resolve :premises (@p1515 @p68)) % 0.38/0.63 (step-pop @p2220 :rule scope :premises (@p1516)) % 0.38/0.63 (step-pop @p2221 :rule scope :premises (@p2220)) % 0.38/0.63 (step-pop @p2222 :rule scope :premises (@p2221)) % 0.38/0.63 (step-pop @p2223 :rule scope :premises (@p2222)) % 0.38/0.63 (step @p1517 :rule process_scope :premises (@p2223) :args (false)) % 0.38/0.63 (assume-push @p2224 @t19) % 0.38/0.63 (assume-push @p2225 @t31) % 0.38/0.63 (assume-push @p2226 @t28) % 0.38/0.63 (assume-push @p2227 @t29) % 0.38/0.63 (step @p1526 :rule and_intro :premises (@p2224 @p2226 @p2227 @p2225)) % 0.38/0.63 (step-pop @p2228 :rule scope :premises (@p1526)) % 0.38/0.63 (step-pop @p2229 :rule scope :premises (@p2228)) % 0.38/0.63 (step-pop @p2230 :rule scope :premises (@p2229)) % 0.38/0.63 (step-pop @p2231 :rule scope :premises (@p2230)) % 0.38/0.63 (step @p1527 :rule process_scope :premises (@p2231) :args (@t166)) % 0.38/0.63 (step @p1532 :rule implies_elim :premises (@p1527)) % 0.38/0.63 (step @p1533 :rule resolution :premises (@p1532 @p1517) :args (true @t166)) % 0.38/0.63 (step @p1534 :rule not_and :premises (@p1533)) % 0.38/0.63 (step @p1535 :rule eq_resolve :premises (@p1534 @p1502)) % 0.38/0.63 (step @p1536 :rule reordering :premises (@p1535) :args ((or @t18 @t16 @t17 @t30))) % 0.38/0.63 (step @p1537 :rule chain_m_resolution :premises (@p1536 @p1500 @p177 @p1461 @p1424 @p1422 @p1211 @p1210 @p35) :args (@t30 (@list true false false true true true true true) (@list @t16 @t35 @t44 @t43 @t52 @t25 @t18 @t17))) % 0.38/0.63 (step @p1538 :rule not_equiv_elim1 :premises (@p34)) % 0.38/0.63 (step @p1539 :rule chain_m_resolution :premises (@p1538 @p1537) :args (@t17 @t167 (@list @t19))) % 0.38/0.63 (step @p1540 :rule bool-double-not-elim :args (@t19)) % 0.38/0.63 (step @p1541 :rule refl :args (@t31)) % 0.38/0.63 (step @p1542 :rule nary_cong :premises (@p62 @p60 @p1541 @p1540) :args ((or @t28 @t29 @t31 @t168))) % 0.38/0.63 (assume-push @p2232 @t30) % 0.38/0.63 (assume-push @p2233 @t18) % 0.38/0.63 (assume-push @p2234 @t16) % 0.38/0.63 (assume-push @p2235 @t17) % 0.38/0.63 (step @p350 :rule evaluate :args (@t80)) % 0.38/0.63 (step @p1547 :rule false_intro :premises (@p2232)) % 0.38/0.63 (step @p1548 :rule true_intro :premises (@p2233)) % 0.38/0.63 (step @p1549 :rule symm :premises (@p1548)) % 0.38/0.63 (step @p1550 :rule true_intro :premises (@p2234)) % 0.38/0.63 (step @p1551 :rule trans :premises (@p1550 @p1549)) % 0.38/0.63 (step @p1552 :rule cong :premises (@p1551) :args (@t17)) % 0.38/0.63 (step @p1553 :rule true_intro :premises (@p2235)) % 0.38/0.63 (step @p1554 :rule symm :premises (@p1553)) % 0.38/0.63 (step @p1555 :rule trans :premises (@p1554 @p1552 @p1547)) % 0.38/0.63 (step @p1556 false :rule eq_resolve :premises (@p1555 @p350)) % 0.38/0.63 (step-pop @p2236 :rule scope :premises (@p1556)) % 0.38/0.63 (step-pop @p2237 :rule scope :premises (@p2236)) % 0.38/0.63 (step-pop @p2238 :rule scope :premises (@p2237)) % 0.38/0.63 (step-pop @p2239 :rule scope :premises (@p2238)) % 0.38/0.63 (step @p1557 :rule process_scope :premises (@p2239) :args (false)) % 0.38/0.63 (assume-push @p2240 @t18) % 0.38/0.63 (assume-push @p2241 @t16) % 0.38/0.63 (assume-push @p2242 @t17) % 0.38/0.63 (assume-push @p2243 @t30) % 0.38/0.63 (step @p1566 :rule and_intro :premises (@p2243 @p2240 @p2241 @p2242)) % 0.38/0.63 (step-pop @p2244 :rule scope :premises (@p1566)) % 0.38/0.63 (step-pop @p2245 :rule scope :premises (@p2244)) % 0.38/0.63 (step-pop @p2246 :rule scope :premises (@p2245)) % 0.38/0.63 (step-pop @p2247 :rule scope :premises (@p2246)) % 0.38/0.63 (step @p1567 :rule process_scope :premises (@p2247) :args (@t169)) % 0.38/0.63 (step @p1572 :rule implies_elim :premises (@p1567)) % 0.38/0.63 (step @p1573 :rule resolution :premises (@p1572 @p1557) :args (true @t169)) % 0.38/0.63 (step @p1574 :rule not_and :premises (@p1573)) % 0.38/0.63 (step @p1575 :rule eq_resolve :premises (@p1574 @p1542)) % 0.38/0.63 (step @p1576 :rule reordering :premises (@p1575) :args ((or @t19 @t31 @t28 @t29))) % 0.38/0.63 (step @p1577 :rule bool-double-not-elim :args (@t35)) % 0.38/0.63 (step @p1578 :rule nary_cong :premises (@p1541 @p1501 @p120 @p1577) :args ((or @t31 @t165 @t41 @t170))) % 0.38/0.63 (assume-push @p2248 @t17) % 0.38/0.63 (assume-push @p2249 @t29) % 0.38/0.63 (assume-push @p2250 @t39) % 0.38/0.63 (assume-push @p2251 @t40) % 0.38/0.63 (step @p68 :rule evaluate :args (@t33)) % 0.38/0.63 (step @p1583 :rule true_intro :premises (@p2248)) % 0.38/0.63 (step @p1584 :rule false_intro :premises (@p2249)) % 0.38/0.63 (step @p1585 :rule symm :premises (@p1584)) % 0.38/0.63 (step @p1586 :rule false_intro :premises (@p2250)) % 0.38/0.63 (step @p1587 :rule trans :premises (@p1586 @p1585)) % 0.38/0.63 (step @p1588 :rule cong :premises (@p1587) :args (@t36)) % 0.38/0.63 (step @p1589 :rule false_intro :premises (@p2251)) % 0.38/0.63 (step @p1590 :rule symm :premises (@p1589)) % 0.38/0.63 (step @p1591 :rule trans :premises (@p1590 @p1588 @p1583)) % 0.38/0.63 (step @p1592 false :rule eq_resolve :premises (@p1591 @p68)) % 0.38/0.63 (step-pop @p2252 :rule scope :premises (@p1592)) % 0.38/0.63 (step-pop @p2253 :rule scope :premises (@p2252)) % 0.38/0.63 (step-pop @p2254 :rule scope :premises (@p2253)) % 0.38/0.63 (step-pop @p2255 :rule scope :premises (@p2254)) % 0.38/0.63 (step @p1593 :rule process_scope :premises (@p2255) :args (false)) % 0.38/0.63 (assume-push @p2256 @t17) % 0.38/0.63 (assume-push @p2257 @t29) % 0.38/0.63 (assume-push @p2258 @t40) % 0.38/0.63 (assume-push @p2259 @t39) % 0.38/0.63 (step @p1602 :rule and_intro :premises (@p2256 @p2257 @p2259 @p2258)) % 0.38/0.63 (step-pop @p2260 :rule scope :premises (@p1602)) % 0.38/0.63 (step-pop @p2261 :rule scope :premises (@p2260)) % 0.38/0.63 (step-pop @p2262 :rule scope :premises (@p2261)) % 0.38/0.63 (step-pop @p2263 :rule scope :premises (@p2262)) % 0.38/0.63 (step @p1603 :rule process_scope :premises (@p2263) :args (@t171)) % 0.38/0.63 (step @p1608 :rule implies_elim :premises (@p1603)) % 0.38/0.63 (step @p1609 :rule resolution :premises (@p1608 @p1593) :args (true @t171)) % 0.38/0.63 (step @p1610 :rule not_and :premises (@p1609)) % 0.38/0.63 (step @p1611 :rule eq_resolve :premises (@p1610 @p1578)) % 0.38/0.63 (step @p1612 :rule reordering :premises (@p1611) :args ((or @t16 @t35 @t36 @t31))) % 0.38/0.63 (step @p1613 :rule equiv_elim1 :premises (@p176)) % 0.38/0.63 (step @p1614 :rule reordering :premises (@p1613) :args ((or @t44 @t39))) % 0.38/0.63 (step @p1615 :rule refl :args (@t48)) % 0.38/0.63 (step @p1616 :rule nary_cong :premises (@p62 @p179 @p1615 @p1540) :args ((or @t28 @t47 @t48 @t168))) % 0.38/0.63 (assume-push @p2264 @t30) % 0.38/0.63 (assume-push @p2265 @t18) % 0.38/0.63 (assume-push @p2266 @t43) % 0.38/0.63 (assume-push @p2267 @t44) % 0.38/0.63 (step @p350 :rule evaluate :args (@t80)) % 0.38/0.63 (step @p1621 :rule false_intro :premises (@p2264)) % 0.38/0.63 (step @p1622 :rule true_intro :premises (@p2265)) % 0.38/0.63 (step @p1623 :rule symm :premises (@p1622)) % 0.38/0.63 (step @p1624 :rule true_intro :premises (@p2266)) % 0.38/0.63 (step @p1625 :rule trans :premises (@p1624 @p1623)) % 0.38/0.63 (step @p1626 :rule cong :premises (@p1625) :args (@t44)) % 0.38/0.63 (step @p1627 :rule true_intro :premises (@p2267)) % 0.38/0.63 (step @p1628 :rule symm :premises (@p1627)) % 0.38/0.63 (step @p1629 :rule trans :premises (@p1628 @p1626 @p1621)) % 0.38/0.63 (step @p1630 false :rule eq_resolve :premises (@p1629 @p350)) % 0.38/0.63 (step-pop @p2268 :rule scope :premises (@p1630)) % 0.38/0.63 (step-pop @p2269 :rule scope :premises (@p2268)) % 0.38/0.63 (step-pop @p2270 :rule scope :premises (@p2269)) % 0.38/0.63 (step-pop @p2271 :rule scope :premises (@p2270)) % 0.38/0.63 (step @p1631 :rule process_scope :premises (@p2271) :args (false)) % 0.38/0.63 (assume-push @p2272 @t18) % 0.38/0.63 (assume-push @p2273 @t43) % 0.38/0.63 (assume-push @p2274 @t44) % 0.38/0.63 (assume-push @p2275 @t30) % 0.38/0.63 (step @p1640 :rule and_intro :premises (@p2275 @p2272 @p2273 @p2274)) % 0.38/0.63 (step-pop @p2276 :rule scope :premises (@p1640)) % 0.38/0.63 (step-pop @p2277 :rule scope :premises (@p2276)) % 0.38/0.63 (step-pop @p2278 :rule scope :premises (@p2277)) % 0.38/0.63 (step-pop @p2279 :rule scope :premises (@p2278)) % 0.38/0.63 (step @p1641 :rule process_scope :premises (@p2279) :args (@t172)) % 0.38/0.63 (step @p1646 :rule implies_elim :premises (@p1641)) % 0.38/0.63 (step @p1647 :rule resolution :premises (@p1646 @p1631) :args (true @t172)) % 0.38/0.63 (step @p1648 :rule not_and :premises (@p1647)) % 0.38/0.63 (step @p1649 :rule eq_resolve :premises (@p1648 @p1616)) % 0.38/0.63 (step @p1650 :rule reordering :premises (@p1649) :args ((or @t19 @t28 @t48 @t47))) % 0.38/0.63 (step @p1651 :rule chain_m_resolution :premises (@p890 @p868 @p928 @p318 @p1209 @p949 @p1025 @p988 @p987 @p235 @p1650 @p1537 @p1614 @p1612 @p1539 @p119 @p1576 @p1539 @p1537 @p58) :args (@t28 (@list true false true true false false true true true true true false false false true true false true false) (@list @t75 @t130 @t66 @t51 @t134 @t55 @t56 @t24 @t52 @t43 @t19 @t44 @t35 @t17 @t36 @t16 @t17 @t19 @t25))) % 0.38/0.63 (step @p1652 :rule chain_m_resolution :premises (@p1211 @p1651) :args (@t61 @t167 (@list @t18))) % 0.38/0.63 (step @p1653 :rule chain_m_resolution :premises (@p1422 @p1652) :args (@t62 @t167 (@list @t25))) % 0.38/0.63 (step @p1654 :rule chain_m_resolution :premises (@p1424 @p1653) :args (@t47 @t167 (@list @t52))) % 0.38/0.63 (step @p1655 :rule nary_cong :premises (@p1540 @p1426 @p1425 @p1615) :args ((or @t168 @t161 @t160 @t48))) % 0.38/0.63 (assume-push @p2280 @t30) % 0.38/0.63 (assume-push @p2281 @t28) % 0.38/0.63 (assume-push @p2282 @t47) % 0.38/0.63 (assume-push @p2283 @t30) % 0.38/0.63 (assume-push @p2284 @t28) % 0.38/0.63 (assume-push @p2285 @t47) % 0.38/0.63 (step @p1662 :rule false_intro :premises (@p2280)) % 0.38/0.63 (step @p1663 :rule false_intro :premises (@p2281)) % 0.38/0.63 (step @p1664 :rule symm :premises (@p1663)) % 0.38/0.63 (step @p1665 :rule false_intro :premises (@p2282)) % 0.38/0.63 (step @p1666 :rule trans :premises (@p1665 @p1664)) % 0.38/0.63 (step @p1667 :rule cong :premises (@p1666) :args (@t44)) % 0.38/0.63 (step @p1668 :rule trans :premises (@p1667 @p1662)) % 0.38/0.63 (step @p1669 :rule false_elim :premises (@p1668)) % 0.38/0.63 (step-pop @p2286 :rule scope :premises (@p1669)) % 0.38/0.63 (step-pop @p2287 :rule scope :premises (@p2286)) % 0.38/0.63 (step-pop @p2288 :rule scope :premises (@p2287)) % 0.38/0.63 (step @p1670 :rule process_scope :premises (@p2288) :args (@t48)) % 0.38/0.63 (step @p1674 :rule and_intro :premises (@p2280 @p2281 @p2282)) % 0.38/0.63 (step @p1675 :rule modus_ponens :premises (@p1674 @p1670)) % 0.38/0.63 (step-pop @p2289 :rule scope :premises (@p1675)) % 0.38/0.63 (step-pop @p2290 :rule scope :premises (@p2289)) % 0.38/0.63 (step-pop @p2291 :rule scope :premises (@p2290)) % 0.38/0.63 (step @p1676 :rule process_scope :premises (@p2291) :args (@t48)) % 0.38/0.63 (step @p1680 :rule implies_elim :premises (@p1676)) % 0.38/0.63 (step @p1681 :rule cnf_and_neg :args (@t173)) % 0.38/0.63 (step @p1682 :rule resolution :premises (@p1681 @p1680) :args (true @t173)) % 0.38/0.63 (step @p1683 :rule eq_resolve :premises (@p1682 @p1655)) % 0.38/0.63 (step @p1684 :rule reordering :premises (@p1683) :args ((or @t18 @t19 @t43 @t48))) % 0.38/0.63 (step @p1685 :rule chain_m_resolution :premises (@p1684 @p1651 @p1537 @p1654) :args (@t48 @t129 (@list @t18 @t19 @t43))) % 0.38/0.63 (step @p1686 :rule chain_m_resolution :premises (@p1614 @p1685) :args (@t39 @t167 (@list @t44))) % 0.38/0.63 (step @p1687 :rule nary_cong :premises (@p1540 @p1426 @p1577 @p1464) :args ((or @t168 @t161 @t170 @t40))) % 0.38/0.63 (assume-push @p2292 @t30) % 0.38/0.63 (assume-push @p2293 @t28) % 0.38/0.63 (assume-push @p2294 @t39) % 0.38/0.63 (assume-push @p2295 @t30) % 0.38/0.63 (assume-push @p2296 @t28) % 0.38/0.63 (assume-push @p2297 @t39) % 0.38/0.63 (step @p1694 :rule false_intro :premises (@p2292)) % 0.38/0.63 (step @p1695 :rule false_intro :premises (@p2293)) % 0.38/0.63 (step @p1696 :rule symm :premises (@p1695)) % 0.38/0.63 (step @p1697 :rule false_intro :premises (@p2294)) % 0.38/0.63 (step @p1698 :rule trans :premises (@p1697 @p1696)) % 0.38/0.63 (step @p1699 :rule cong :premises (@p1698) :args (@t36)) % 0.38/0.63 (step @p1700 :rule trans :premises (@p1699 @p1694)) % 0.38/0.63 (step @p1701 :rule false_elim :premises (@p1700)) % 0.38/0.63 (step-pop @p2298 :rule scope :premises (@p1701)) % 0.38/0.63 (step-pop @p2299 :rule scope :premises (@p2298)) % 0.38/0.63 (step-pop @p2300 :rule scope :premises (@p2299)) % 0.38/0.63 (step @p1702 :rule process_scope :premises (@p2300) :args (@t40)) % 0.38/0.63 (step @p1706 :rule and_intro :premises (@p2292 @p2293 @p2294)) % 0.38/0.63 (step @p1707 :rule modus_ponens :premises (@p1706 @p1702)) % 0.38/0.63 (step-pop @p2301 :rule scope :premises (@p1707)) % 0.38/0.63 (step-pop @p2302 :rule scope :premises (@p2301)) % 0.38/0.63 (step-pop @p2303 :rule scope :premises (@p2302)) % 0.38/0.63 (step @p1708 :rule process_scope :premises (@p2303) :args (@t40)) % 0.38/0.63 (step @p1712 :rule implies_elim :premises (@p1708)) % 0.38/0.63 (step @p1713 :rule cnf_and_neg :args (@t174)) % 0.38/0.63 (step @p1714 :rule resolution :premises (@p1713 @p1712) :args (true @t174)) % 0.38/0.63 (step @p1715 :rule eq_resolve :premises (@p1714 @p1687)) % 0.38/0.63 (step @p1716 :rule reordering :premises (@p1715) :args ((or @t18 @t19 @t35 @t40))) % 0.38/0.63 (step @p1717 :rule chain_m_resolution :premises (@p1716 @p1651 @p1537 @p1686) :args (@t40 @t129 (@list @t18 @t19 @t35))) % 0.38/0.63 (step @p1718 :rule chain_m_resolution :premises (@p1463 @p1717) :args (@t29 @t167 @t164)) % 0.38/0.63 (step @p1719 false :rule chain_m_resolution :premises (@p1612 @p1718 @p1717 @p1686 @p1539) :args (false @t112 (@list @t16 @t36 @t35 @t17))) % 0.38/0.63 ) % 0.38/0.63 % SZS output end Proof % 0.38/0.63 % cvc5 exiting %------------------------------------------------------------------------------