cvc5---1.3.4.UNS-Prf.s

%------------------------------------------------------------------------------
% File     : cvc5---1.3.4
% Problem  : ALG045+1 : TPTP v9.2.1. Released v2.7.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM

% Computer : n003.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Wed Jun  3 08:05:05 AM UTC 2026

% Result   : Unsatisfiable 0.39s 0.58s
% Output   : Proof 0.39s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12  % Problem  : ALG045+1 : TPTP v9.2.1. Released v2.7.0.
% 0.12/0.13  % Command  : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.17/0.34  % Computer : n003.cluster.edu
% 0.17/0.34  % Model    : x86_64 x86_64
% 0.17/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.34  % Memory   : 8042.1875MB
% 0.17/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.17/0.34  % CPULimit : 300
% 0.17/0.34  % WCLimit  : 300
% 0.17/0.34  % DateTime : Wed Jun  3 01:37:59 EDT 2026
% 0.17/0.34  % CPUTime  : 
% 0.29/0.50  %----Proving TF0_NAR, FOF, or CNF
% 0.29/0.52  --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15...
% 0.39/0.58  % SZS status Unsatisfiable
% 0.39/0.58  % SZS output start Proof
% 0.39/0.61  (
% 0.39/0.61  (declare-sort $$unsorted 0)
% 0.39/0.61  (declare-const tptp.unit $$unsorted)
% 0.39/0.61  (declare-const tptp.e0 $$unsorted)
% 0.39/0.61  (declare-const tptp.e1 $$unsorted)
% 0.39/0.61  (declare-const tptp.e2 $$unsorted)
% 0.39/0.61  (declare-const tptp.op (-> $$unsorted $$unsorted $$unsorted))
% 0.39/0.61  (declare-const tptp.e3 $$unsorted)
% 0.39/0.61  (define @t1 () (tptp.op tptp.e3 tptp.e3))
% 0.39/0.61  (define @t2 () (= @t1 tptp.e3))
% 0.39/0.61  (define @t3 () (= @t1 tptp.e2))
% 0.39/0.61  (define @t4 () (= @t1 tptp.e1))
% 0.39/0.61  (define @t5 () (= @t1 tptp.e0))
% 0.39/0.61  (define @t6 () (tptp.op tptp.e3 tptp.e2))
% 0.39/0.61  (define @t7 () (= @t6 tptp.e3))
% 0.39/0.61  (define @t8 () (= @t6 tptp.e2))
% 0.39/0.61  (define @t9 () (= @t6 tptp.e1))
% 0.39/0.61  (define @t10 () (= @t6 tptp.e0))
% 0.39/0.61  (define @t11 () (tptp.op tptp.e3 tptp.e1))
% 0.39/0.61  (define @t12 () (= @t11 tptp.e3))
% 0.39/0.61  (define @t13 () (= @t11 tptp.e2))
% 0.39/0.61  (define @t14 () (= @t11 tptp.e1))
% 0.39/0.61  (define @t15 () (= @t11 tptp.e0))
% 0.39/0.61  (define @t16 () (tptp.op tptp.e3 tptp.e0))
% 0.39/0.61  (define @t17 () (= @t16 tptp.e3))
% 0.39/0.61  (define @t18 () (= @t16 tptp.e2))
% 0.39/0.61  (define @t19 () (= @t16 tptp.e1))
% 0.39/0.61  (define @t20 () (= @t16 tptp.e0))
% 0.39/0.61  (define @t21 () (tptp.op tptp.e2 tptp.e3))
% 0.39/0.61  (define @t22 () (= @t21 tptp.e3))
% 0.39/0.61  (define @t23 () (= @t21 tptp.e2))
% 0.39/0.61  (define @t24 () (= @t21 tptp.e1))
% 0.39/0.61  (define @t25 () (= @t21 tptp.e0))
% 0.39/0.61  (define @t26 () (tptp.op tptp.e2 tptp.e2))
% 0.39/0.61  (define @t27 () (= @t26 tptp.e3))
% 0.39/0.61  (define @t28 () (= @t26 tptp.e2))
% 0.39/0.61  (define @t29 () (= @t26 tptp.e1))
% 0.39/0.61  (define @t30 () (= @t26 tptp.e0))
% 0.39/0.61  (define @t31 () (tptp.op tptp.e2 tptp.e1))
% 0.39/0.61  (define @t32 () (= @t31 tptp.e3))
% 0.39/0.61  (define @t33 () (= @t31 tptp.e2))
% 0.39/0.61  (define @t34 () (= @t31 tptp.e1))
% 0.39/0.61  (define @t35 () (= @t31 tptp.e0))
% 0.39/0.61  (define @t36 () (tptp.op tptp.e2 tptp.e0))
% 0.39/0.61  (define @t37 () (= @t36 tptp.e3))
% 0.39/0.61  (define @t38 () (= @t36 tptp.e2))
% 0.39/0.61  (define @t39 () (= @t36 tptp.e1))
% 0.39/0.61  (define @t40 () (= @t36 tptp.e0))
% 0.39/0.61  (define @t41 () (or @t40 @t39 @t38 @t37))
% 0.39/0.61  (define @t42 () (tptp.op tptp.e1 tptp.e3))
% 0.39/0.61  (define @t43 () (= @t42 tptp.e3))
% 0.39/0.61  (define @t44 () (= @t42 tptp.e2))
% 0.39/0.61  (define @t45 () (= @t42 tptp.e1))
% 0.39/0.61  (define @t46 () (= @t42 tptp.e0))
% 0.39/0.61  (define @t47 () (tptp.op tptp.e1 tptp.e2))
% 0.39/0.61  (define @t48 () (= @t47 tptp.e3))
% 0.39/0.61  (define @t49 () (= @t47 tptp.e2))
% 0.39/0.61  (define @t50 () (= @t47 tptp.e1))
% 0.39/0.61  (define @t51 () (= @t47 tptp.e0))
% 0.39/0.61  (define @t52 () (tptp.op tptp.e1 tptp.e1))
% 0.39/0.61  (define @t53 () (= @t52 tptp.e3))
% 0.39/0.61  (define @t54 () (= @t52 tptp.e2))
% 0.39/0.61  (define @t55 () (= @t52 tptp.e1))
% 0.39/0.61  (define @t56 () (= @t52 tptp.e0))
% 0.39/0.61  (define @t57 () (tptp.op tptp.e1 tptp.e0))
% 0.39/0.61  (define @t58 () (= @t57 tptp.e3))
% 0.39/0.61  (define @t59 () (= @t57 tptp.e2))
% 0.39/0.61  (define @t60 () (= @t57 tptp.e1))
% 0.39/0.61  (define @t61 () (= @t57 tptp.e0))
% 0.39/0.61  (define @t62 () (tptp.op tptp.e0 tptp.e3))
% 0.39/0.61  (define @t63 () (= @t62 tptp.e3))
% 0.39/0.61  (define @t64 () (= @t62 tptp.e2))
% 0.39/0.61  (define @t65 () (= @t62 tptp.e1))
% 0.39/0.61  (define @t66 () (= @t62 tptp.e0))
% 0.39/0.61  (define @t67 () (tptp.op tptp.e0 tptp.e2))
% 0.39/0.61  (define @t68 () (= @t67 tptp.e3))
% 0.39/0.61  (define @t69 () (= @t67 tptp.e2))
% 0.39/0.61  (define @t70 () (= @t67 tptp.e1))
% 0.39/0.61  (define @t71 () (= @t67 tptp.e0))
% 0.39/0.61  (define @t72 () (tptp.op tptp.e0 tptp.e1))
% 0.39/0.61  (define @t73 () (= @t72 tptp.e3))
% 0.39/0.61  (define @t74 () (= @t72 tptp.e2))
% 0.39/0.61  (define @t75 () (= @t72 tptp.e1))
% 0.39/0.61  (define @t76 () (= @t72 tptp.e0))
% 0.39/0.61  (define @t77 () (tptp.op tptp.e0 tptp.e0))
% 0.39/0.61  (define @t78 () (= @t77 tptp.e3))
% 0.39/0.61  (define @t79 () (= @t77 tptp.e2))
% 0.39/0.61  (define @t80 () (= @t77 tptp.e1))
% 0.39/0.61  (define @t81 () (= @t77 tptp.e0))
% 0.39/0.61  (define @t82 () (or (= tptp.unit tptp.e0) (= tptp.unit tptp.e1) (= tptp.unit tptp.e2) (= tptp.unit tptp.e3)))
% 0.39/0.61  (define @t83 () (tptp.op tptp.e3 tptp.unit))
% 0.39/0.61  (define @t84 () (tptp.op tptp.unit tptp.e3))
% 0.39/0.61  (define @t85 () (tptp.op tptp.e2 tptp.unit))
% 0.39/0.61  (define @t86 () (tptp.op tptp.e1 tptp.unit))
% 0.39/0.61  (define @t87 () (tptp.op tptp.unit tptp.e1))
% 0.39/0.61  (define @t88 () (tptp.op tptp.unit tptp.e0))
% 0.39/0.61  (define @t89 () (or @t73 @t53 @t32 @t12))
% 0.39/0.61  (define @t90 () (or @t78 @t73 @t68 @t63))
% 0.39/0.61  (define @t91 () (or @t80 @t60 @t39 @t19))
% 0.39/0.61  (define @t92 () (= tptp.e2 tptp.e3))
% 0.39/0.61  (define @t93 () (not @t92))
% 0.39/0.61  (define @t94 () (= tptp.e1 tptp.e3))
% 0.39/0.61  (define @t95 () (= tptp.e1 tptp.e2))
% 0.39/0.61  (define @t96 () (= tptp.e0 tptp.e3))
% 0.39/0.61  (define @t97 () (not @t96))
% 0.39/0.61  (define @t98 () (= tptp.e0 tptp.e2))
% 0.39/0.61  (define @t99 () (not @t98))
% 0.39/0.61  (define @t100 () (= tptp.e0 tptp.e1))
% 0.39/0.61  (define @t101 () (not @t100))
% 0.39/0.61  (define @t102 () (and @t78 @t53 @t27 @t2))
% 0.39/0.61  (define @t103 () (and @t79 @t54 @t28 @t3))
% 0.39/0.61  (define @t104 () (and @t80 @t55 @t29 @t4))
% 0.39/0.61  (define @t105 () (and @t81 @t56 @t30 @t5))
% 0.39/0.61  (define @t106 () (or @t105 @t104 @t103 @t102))
% 0.39/0.61  (define @t107 () (= tptp.e0 @t52))
% 0.39/0.61  (define @t108 () (= tptp.e3 @t31))
% 0.39/0.61  (define @t109 () (= tptp.e0 @t26))
% 0.39/0.61  (define @t110 () (= tptp.e0 @t1))
% 0.39/0.61  (define @t111 () (= tptp.e1 @t77))
% 0.39/0.61  (define @t112 () (= tptp.e3 @t36))
% 0.39/0.61  (define @t113 () (= tptp.e1 @t26))
% 0.39/0.61  (define @t114 () (= tptp.e3 @t67))
% 0.39/0.61  (define @t115 () (= tptp.e1 @t1))
% 0.39/0.61  (define @t116 () (= tptp.e1 @t16))
% 0.39/0.61  (define @t117 () (= tptp.e2 @t77))
% 0.39/0.61  (define @t118 () (= tptp.e2 @t52))
% 0.39/0.61  (define @t119 () (= tptp.e3 @t72))
% 0.39/0.61  (define @t120 () (= tptp.e2 @t1))
% 0.39/0.61  (define @t121 () (= tptp.e1 @t36))
% 0.39/0.61  (define @t122 () (= tptp.e3 @t77))
% 0.39/0.61  (define @t123 () (= tptp.e3 @t52))
% 0.39/0.61  (define @t124 () (= tptp.e3 @t26))
% 0.39/0.61  (define @t125 () (not @t120))
% 0.39/0.61  (define @t126 () (= tptp.e3 tptp.unit))
% 0.39/0.61  (define @t127 () (not @t126))
% 0.39/0.61  (define @t128 () (= tptp.e3 @t83))
% 0.39/0.61  (define @t129 () (not @t128))
% 0.39/0.61  (define @t130 () (= tptp.e3 @t1))
% 0.39/0.61  (define @t131 () (and @t93 @t128 @t126))
% 0.39/0.61  (define @t132 () (not @t110))
% 0.39/0.61  (define @t133 () (and @t97 @t128 @t126))
% 0.39/0.61  (define @t134 () (= tptp.e2 @t36))
% 0.39/0.61  (define @t135 () (not @t134))
% 0.39/0.61  (define @t136 () (= @t21 @t36))
% 0.39/0.61  (define @t137 () (= tptp.e2 @t85))
% 0.39/0.61  (define @t138 () (not @t137))
% 0.39/0.61  (define @t139 () (not @t136))
% 0.39/0.61  (define @t140 () (= tptp.e2 @t21))
% 0.39/0.61  (define @t141 () (and @t137 @t139 @t126))
% 0.39/0.61  (define @t142 () (= tptp.e1 @t57))
% 0.39/0.61  (define @t143 () (not @t142))
% 0.39/0.61  (define @t144 () (= @t42 @t57))
% 0.39/0.61  (define @t145 () (= tptp.e1 @t86))
% 0.39/0.61  (define @t146 () (not @t145))
% 0.39/0.61  (define @t147 () (not @t144))
% 0.39/0.61  (define @t148 () (= tptp.e1 @t42))
% 0.39/0.61  (define @t149 () (and @t145 @t147 @t126))
% 0.39/0.61  (define @t150 () (not @t116))
% 0.39/0.61  (define @t151 () (= @t11 @t16))
% 0.39/0.61  (define @t152 () (= tptp.e1 @t87))
% 0.39/0.61  (define @t153 () (not @t152))
% 0.39/0.61  (define @t154 () (not @t151))
% 0.39/0.61  (define @t155 () (not @t154))
% 0.39/0.61  (define @t156 () (= tptp.e1 @t11))
% 0.39/0.61  (define @t157 () (and @t152 @t154 @t126))
% 0.39/0.61  (define @t158 () (= tptp.e0 @t36))
% 0.39/0.61  (define @t159 () (not @t158))
% 0.39/0.61  (define @t160 () (= @t16 @t36))
% 0.39/0.61  (define @t161 () (= tptp.e0 @t88))
% 0.39/0.61  (define @t162 () (not @t161))
% 0.39/0.61  (define @t163 () (not @t160))
% 0.39/0.61  (define @t164 () (= tptp.e0 @t16))
% 0.39/0.61  (define @t165 () (and @t161 @t163 @t126))
% 0.39/0.61  (define @t166 () (= tptp.e2 @t26))
% 0.39/0.61  (define @t167 () (and @t117 @t118 @t166 @t120))
% 0.39/0.61  (define @t168 () (not @t167))
% 0.39/0.61  (define @t169 () (= tptp.e0 @t77))
% 0.39/0.61  (define @t170 () (and @t169 @t107 @t109 @t110))
% 0.39/0.61  (define @t171 () (not @t170))
% 0.39/0.61  (define @t172 () (= tptp.e1 @t52))
% 0.39/0.61  (define @t173 () (and @t111 @t172 @t113 @t115))
% 0.39/0.61  (define @t174 () (not @t173))
% 0.39/0.61  (define @t175 () (not @t113))
% 0.39/0.61  (define @t176 () (= tptp.e0 tptp.unit))
% 0.39/0.61  (define @t177 () (= @t52 @t57))
% 0.39/0.61  (define @t178 () (and @t145 @t172 @t176))
% 0.39/0.61  (define @t179 () (not @t176))
% 0.39/0.61  (define @t180 () (= tptp.e2 tptp.unit))
% 0.39/0.61  (define @t181 () (and @t113 @t137 @t180))
% 0.39/0.61  (define @t182 () (not @t180))
% 0.39/0.61  (define @t183 () (and @t115 @t128 @t126))
% 0.39/0.61  (define @t184 () (not @t122))
% 0.39/0.61  (define @t185 () (= tptp.e1 tptp.unit))
% 0.39/0.61  (define @t186 () (not @t185))
% 0.39/0.61  (define @t187 () (not @t111))
% 0.39/0.61  (define @t188 () (not @t127))
% 0.39/0.61  (define @t189 () (and @t111 @t185 @t127))
% 0.39/0.61  (define @t190 () (not @t119))
% 0.39/0.61  (define @t191 () (= @t11 @t72))
% 0.39/0.61  (define @t192 () (not @t191))
% 0.39/0.61  (define @t193 () (= tptp.e3 @t11))
% 0.39/0.61  (define @t194 () (and @t128 @t192 @t185))
% 0.39/0.61  (define @t195 () (= tptp.e3 @t62))
% 0.39/0.61  (define @t196 () (not @t195))
% 0.39/0.61  (define @t197 () (= @t42 @t62))
% 0.39/0.61  (define @t198 () (= tptp.e3 @t84))
% 0.39/0.61  (define @t199 () (not @t198))
% 0.39/0.61  (define @t200 () (not @t197))
% 0.39/0.61  (define @t201 () (= tptp.e3 @t42))
% 0.39/0.61  (define @t202 () (and @t198 @t200 @t185))
% 0.39/0.61  (define @t203 () (and @t122 @t123 @t124 @t130))
% 0.39/0.61  (define @t204 () (not @t203))
% 0.39/0.61  (define @t205 () (not @t169))
% 0.39/0.61  (define @t206 () (not @t101))
% 0.39/0.61  (define @t207 () (and @t101 @t111))
% 0.39/0.61  (define @t208 () (= @t57 @t77))
% 0.39/0.61  (define @t209 () (and @t111 @t145 @t176))
% 0.39/0.61  (define @t210 () (not @t124))
% 0.39/0.61  (define @t211 () (= @t6 @t26))
% 0.39/0.61  (define @t212 () (not @t211))
% 0.39/0.61  (define @t213 () (= tptp.e3 @t6))
% 0.39/0.61  (define @t214 () (and @t128 @t212 @t180))
% 0.39/0.61  (define @t215 () (not @t117))
% 0.39/0.61  (define @t216 () (= @t26 @t47))
% 0.39/0.61  (define @t217 () (not @t216))
% 0.39/0.61  (define @t218 () (= tptp.e1 @t47))
% 0.39/0.61  (define @t219 () (and @t111 @t137 @t145 @t217 @t180))
% 0.39/0.61  (define @t220 () (not @t109))
% 0.39/0.61  (define @t221 () (and @t99 @t137 @t180))
% 0.39/0.61  (define @t222 () (= @t47 @t57))
% 0.39/0.61  (define @t223 () (not @t222))
% 0.39/0.61  (define @t224 () (and @t145 @t223 @t180))
% 0.39/0.61  (define @t225 () (not @t121))
% 0.39/0.61  (define @t226 () (= @t31 @t36))
% 0.39/0.61  (define @t227 () (not @t226))
% 0.39/0.61  (define @t228 () (= tptp.e1 @t31))
% 0.39/0.61  (define @t229 () (and @t152 @t227 @t180))
% 0.39/0.61  (define @t230 () (= @t16 @t77))
% 0.39/0.61  (define @t231 () (not @t230))
% 0.39/0.61  (define @t232 () (= tptp.e3 @t16))
% 0.39/0.61  (define @t233 () (and @t128 @t231 @t176))
% 0.39/0.61  (define @t234 () (= @t36 @t77))
% 0.39/0.61  (define @t235 () (not @t234))
% 0.39/0.61  (define @t236 () (and @t137 @t235 @t176))
% 0.39/0.61  (define @t237 () (= @t16 @t57))
% 0.39/0.61  (define @t238 () (not @t237))
% 0.39/0.61  (define @t239 () (= tptp.e1 @t72))
% 0.39/0.61  (define @t240 () (and @t128 @t145 @t152 @t238 @t176))
% 0.39/0.61  (define @t241 () (not @t123))
% 0.39/0.61  (define @t242 () (not @t107))
% 0.39/0.61  (define @t243 () (and @t107 @t176 @t127))
% 0.39/0.61  (define @t244 () (not @t193))
% 0.39/0.61  (define @t245 () (and @t198 @t193 @t232 @t154))
% 0.39/0.61  (define @t246 () (@list true))
% 0.39/0.61  (define @t247 () (not @t118))
% 0.39/0.61  (define @t248 () (= @t31 @t52))
% 0.39/0.61  (define @t249 () (not @t248))
% 0.39/0.61  (define @t250 () (= tptp.e2 @t31))
% 0.39/0.61  (define @t251 () (and @t137 @t249 @t185))
% 0.39/0.61  (define @t252 () (@list true false false))
% 0.39/0.61  (define @t253 () (= @t11 @t52))
% 0.39/0.61  (define @t254 () (not @t253))
% 0.39/0.61  (define @t255 () (and @t128 @t254 @t185))
% 0.39/0.61  (define @t256 () (and @t101 @t145 @t185))
% 0.39/0.61  (assume @p1 (and (or @t81 @t80 @t79 @t78) (or @t76 @t75 @t74 @t73) (or @t71 @t70 @t69 @t68) (or @t66 @t65 @t64 @t63) (or @t61 @t60 @t59 @t58) (or @t56 @t55 @t54 @t53) (or @t51 @t50 @t49 @t48) (or @t46 @t45 @t44 @t43) @t41 (or @t35 @t34 @t33 @t32) (or @t30 @t29 @t28 @t27) (or @t25 @t24 @t23 @t22) (or @t20 @t19 @t18 @t17) (or @t15 @t14 @t13 @t12) (or @t10 @t9 @t8 @t7) (or @t5 @t4 @t3 @t2)))
% 0.39/0.61  (assume @p2 (and (= @t88 tptp.e0) (= (tptp.op tptp.e0 tptp.unit) tptp.e0) (= @t87 tptp.e1) (= @t86 tptp.e1) (= (tptp.op tptp.unit tptp.e2) tptp.e2) (= @t85 tptp.e2) (= @t84 tptp.e3) (= @t83 tptp.e3) @t82))
% 0.39/0.61  (assume @p3 (and (or @t81 @t76 @t71 @t66) (or @t81 @t61 @t40 @t20) (or @t80 @t75 @t70 @t65) @t91 (or @t79 @t74 @t69 @t64) (or @t79 @t59 @t38 @t18) @t90 (or @t78 @t58 @t37 @t17) (or @t61 @t56 @t51 @t46) (or @t76 @t56 @t35 @t15) (or @t60 @t55 @t50 @t45) (or @t75 @t55 @t34 @t14) (or @t59 @t54 @t49 @t44) (or @t74 @t54 @t33 @t13) (or @t58 @t53 @t48 @t43) @t89 (or @t40 @t35 @t30 @t25) (or @t71 @t51 @t30 @t10) (or @t39 @t34 @t29 @t24) (or @t70 @t50 @t29 @t9) (or @t38 @t33 @t28 @t23) (or @t69 @t49 @t28 @t8) (or @t37 @t32 @t27 @t22) (or @t68 @t48 @t27 @t7) (or @t20 @t15 @t10 @t5) (or @t66 @t46 @t25 @t5) (or @t19 @t14 @t9 @t4) (or @t65 @t45 @t24 @t4) (or @t18 @t13 @t8 @t3) (or @t64 @t44 @t23 @t3) (or @t17 @t12 @t7 @t2) (or @t63 @t43 @t22 @t2)))
% 0.39/0.61  (assume @p4 (and (not (= @t77 @t57)) (not (= @t77 @t36)) (not (= @t77 @t16)) (not (= @t57 @t36)) (not (= @t57 @t16)) (not (= @t36 @t16)) (not (= @t72 @t52)) (not (= @t72 @t31)) (not (= @t72 @t11)) (not (= @t52 @t31)) (not (= @t52 @t11)) (not (= @t31 @t11)) (not (= @t67 @t47)) (not (= @t67 @t26)) (not (= @t67 @t6)) (not (= @t47 @t26)) (not (= @t47 @t6)) (not (= @t26 @t6)) (not (= @t62 @t42)) (not (= @t62 @t21)) (not (= @t62 @t1)) (not (= @t42 @t21)) (not (= @t42 @t1)) (not (= @t21 @t1)) (not (= @t77 @t72)) (not (= @t77 @t67)) (not (= @t77 @t62)) (not (= @t72 @t67)) (not (= @t72 @t62)) (not (= @t67 @t62)) (not (= @t57 @t52)) (not (= @t57 @t47)) (not (= @t57 @t42)) (not (= @t52 @t47)) (not (= @t52 @t42)) (not (= @t47 @t42)) (not (= @t36 @t31)) (not (= @t36 @t26)) (not (= @t36 @t21)) (not (= @t31 @t26)) (not (= @t31 @t21)) (not (= @t26 @t21)) (not (= @t16 @t11)) (not (= @t16 @t6)) (not (= @t16 @t1)) (not (= @t11 @t6)) (not (= @t11 @t1)) (not (= @t6 @t1))))
% 0.39/0.61  (assume @p5 (and @t101 @t99 @t97 (not @t95) (not @t94) @t93))
% 0.39/0.61  (assume @p6 @t106)
% 0.39/0.61  (assume @p7 (not (and @t107 (= tptp.e2 @t11))))
% 0.39/0.61  (assume @p8 (not (and @t107 @t108)))
% 0.39/0.61  (assume @p9 (not (and @t109 (= tptp.e1 @t6))))
% 0.39/0.61  (assume @p10 (not (and @t109 (= tptp.e3 @t47))))
% 0.39/0.61  (assume @p11 (not (and @t110 (= tptp.e1 @t21))))
% 0.39/0.61  (assume @p12 (not (and @t110 (= tptp.e2 @t42))))
% 0.39/0.61  (assume @p13 (not (and @t111 (= tptp.e2 @t16))))
% 0.39/0.61  (assume @p14 (not (and @t111 @t112)))
% 0.39/0.61  (assume @p15 (not (and @t113 (= tptp.e0 @t6))))
% 0.39/0.61  (assume @p16 (not (and @t113 @t114)))
% 0.39/0.61  (assume @p17 (not (and @t115 (= tptp.e0 @t21))))
% 0.39/0.61  (assume @p18 (not (and @t115 (= tptp.e2 @t62))))
% 0.39/0.61  (assume @p19 (not (and @t117 @t116)))
% 0.39/0.61  (assume @p20 (not (and @t117 (= tptp.e3 @t57))))
% 0.39/0.61  (assume @p21 (not (and @t118 (= tptp.e0 @t11))))
% 0.39/0.61  (assume @p22 (not (and @t118 @t119)))
% 0.39/0.61  (assume @p23 (not (and @t120 (= tptp.e0 @t42))))
% 0.39/0.61  (assume @p24 (not (and @t120 (= tptp.e1 @t62))))
% 0.39/0.61  (assume @p25 (not (and @t122 @t121)))
% 0.39/0.61  (assume @p26 (not (and @t122 (= tptp.e2 @t57))))
% 0.39/0.61  (assume @p27 (not (and @t123 (= tptp.e0 @t31))))
% 0.39/0.61  (assume @p28 (not (and @t123 (= tptp.e2 @t72))))
% 0.39/0.61  (assume @p29 (not (and @t124 (= tptp.e0 @t47))))
% 0.39/0.61  (assume @p30 (not (and @t124 (= tptp.e1 @t67))))
% 0.39/0.61  (step @p31 :rule and_elim :premises (@p2) :args (7))
% 0.39/0.61  (step @p32 :rule symm :premises (@p31))
% 0.39/0.61  (step @p33 :rule and_elim :premises (@p5) :args (5))
% 0.39/0.61  (step @p34 :rule refl :args (@t125))
% 0.39/0.61  (step @p35 :rule refl :args (@t127))
% 0.39/0.61  (step @p36 :rule refl :args (@t129))
% 0.39/0.61  (step @p37 :rule bool-double-not-elim :args (@t92))
% 0.39/0.61  (step @p38 :rule nary_cong :premises (@p37 @p36 @p35 @p34) :args ((or (not @t93) @t129 @t127 @t125)))
% 0.39/0.61  (assume-push @p1145 @t93)
% 0.39/0.61  (assume-push @p1146 @t128)
% 0.39/0.61  (assume-push @p1147 @t126)
% 0.39/0.61  (assume-push @p1148 @t93)
% 0.39/0.61  (assume-push @p1149 @t130)
% 0.39/0.61  (step @p44 :rule false_intro :premises (@p33))
% 0.39/0.61  (step @p45 :rule symm :premises (@p1149))
% 0.39/0.61  (step @p46 :rule refl :args (tptp.e2))
% 0.39/0.61  (step @p47 :rule cong :premises (@p46 @p45) :args (@t120))
% 0.39/0.61  (step @p48 :rule trans :premises (@p47 @p44))
% 0.39/0.61  (step @p49 :rule false_elim :premises (@p48))
% 0.39/0.61  (step-pop @p1150 :rule scope :premises (@p49))
% 0.39/0.61  (step-pop @p1151 :rule scope :premises (@p1150))
% 0.39/0.61  (step @p50 :rule process_scope :premises (@p1151) :args (@t125))
% 0.39/0.61  (assume-push @p1152 @t126)
% 0.39/0.61  (assume-push @p1153 @t128)
% 0.39/0.61  (step @p55 :rule symm :premises (@p1147))
% 0.39/0.61  (step @p56 :rule refl :args (tptp.e3))
% 0.39/0.61  (step @p57 :rule cong :premises (@p56 @p55) :args (@t83))
% 0.39/0.61  (step @p58 :rule trans :premises (@p32 @p57))
% 0.39/0.61  (step-pop @p1154 :rule scope :premises (@p58))
% 0.39/0.61  (step-pop @p1155 :rule scope :premises (@p1154))
% 0.39/0.61  (step @p59 :rule process_scope :premises (@p1155) :args (@t130))
% 0.39/0.61  (step @p62 :rule and_intro :premises (@p1147 @p32))
% 0.39/0.61  (step @p63 :rule modus_ponens :premises (@p62 @p59))
% 0.39/0.61  (step @p64 :rule and_intro :premises (@p33 @p63))
% 0.39/0.61  (step @p65 :rule modus_ponens :premises (@p64 @p50))
% 0.39/0.61  (step-pop @p1156 :rule scope :premises (@p65))
% 0.39/0.61  (step-pop @p1157 :rule scope :premises (@p1156))
% 0.39/0.61  (step-pop @p1158 :rule scope :premises (@p1157))
% 0.39/0.61  (step @p66 :rule process_scope :premises (@p1158) :args (@t125))
% 0.39/0.61  (step @p70 :rule implies_elim :premises (@p66))
% 0.39/0.61  (step @p71 :rule cnf_and_neg :args (@t131))
% 0.39/0.61  (step @p72 :rule resolution :premises (@p71 @p70) :args (true @t131))
% 0.39/0.61  (step @p73 :rule eq_resolve :premises (@p72 @p38))
% 0.39/0.61  (step @p74 :rule reordering :premises (@p73) :args ((or @t92 @t125 @t129 @t127)))
% 0.39/0.61  (step @p75 :rule and_elim :premises (@p5) :args (2))
% 0.39/0.61  (step @p76 :rule refl :args (@t132))
% 0.39/0.61  (step @p77 :rule bool-double-not-elim :args (@t96))
% 0.39/0.61  (step @p78 :rule nary_cong :premises (@p77 @p36 @p35 @p76) :args ((or (not @t97) @t129 @t127 @t132)))
% 0.39/0.61  (assume-push @p1159 @t97)
% 0.39/0.61  (assume-push @p1160 @t128)
% 0.39/0.61  (assume-push @p1161 @t126)
% 0.39/0.61  (assume-push @p1162 @t97)
% 0.39/0.61  (assume-push @p1163 @t130)
% 0.39/0.61  (step @p84 :rule false_intro :premises (@p75))
% 0.39/0.61  (step @p85 :rule symm :premises (@p1163))
% 0.39/0.61  (step @p86 :rule refl :args (tptp.e0))
% 0.39/0.61  (step @p87 :rule cong :premises (@p86 @p85) :args (@t110))
% 0.39/0.61  (step @p88 :rule trans :premises (@p87 @p84))
% 0.39/0.61  (step @p89 :rule false_elim :premises (@p88))
% 0.39/0.61  (step-pop @p1164 :rule scope :premises (@p89))
% 0.39/0.61  (step-pop @p1165 :rule scope :premises (@p1164))
% 0.39/0.61  (step @p90 :rule process_scope :premises (@p1165) :args (@t132))
% 0.39/0.61  (assume-push @p1166 @t126)
% 0.39/0.61  (assume-push @p1167 @t128)
% 0.39/0.61  (step @p55 :rule symm :premises (@p1161))
% 0.39/0.61  (step @p56 :rule refl :args (tptp.e3))
% 0.39/0.61  (step @p57 :rule cong :premises (@p56 @p55) :args (@t83))
% 0.39/0.61  (step @p58 :rule trans :premises (@p32 @p57))
% 0.39/0.61  (step-pop @p1168 :rule scope :premises (@p58))
% 0.39/0.61  (step-pop @p1169 :rule scope :premises (@p1168))
% 0.39/0.61  (step @p95 :rule process_scope :premises (@p1169) :args (@t130))
% 0.39/0.61  (step @p98 :rule and_intro :premises (@p1161 @p32))
% 0.39/0.61  (step @p99 :rule modus_ponens :premises (@p98 @p95))
% 0.39/0.61  (step @p100 :rule and_intro :premises (@p75 @p99))
% 0.39/0.61  (step @p101 :rule modus_ponens :premises (@p100 @p90))
% 0.39/0.61  (step-pop @p1170 :rule scope :premises (@p101))
% 0.39/0.61  (step-pop @p1171 :rule scope :premises (@p1170))
% 0.39/0.61  (step-pop @p1172 :rule scope :premises (@p1171))
% 0.39/0.61  (step @p102 :rule process_scope :premises (@p1172) :args (@t132))
% 0.39/0.61  (step @p106 :rule implies_elim :premises (@p102))
% 0.39/0.61  (step @p107 :rule cnf_and_neg :args (@t133))
% 0.39/0.61  (step @p108 :rule resolution :premises (@p107 @p106) :args (true @t133))
% 0.39/0.61  (step @p109 :rule eq_resolve :premises (@p108 @p78))
% 0.39/0.61  (step @p110 :rule reordering :premises (@p109) :args ((or @t96 @t132 @t129 @t127)))
% 0.39/0.61  (step @p111 :rule and_elim :premises (@p2) :args (5))
% 0.39/0.61  (step @p112 :rule symm :premises (@p111))
% 0.39/0.61  (step @p113 :rule and_elim :premises (@p4) :args (38))
% 0.39/0.61  (step @p114 :rule symm :premises (@p113))
% 0.39/0.61  (step @p115 :rule refl :args (@t135))
% 0.39/0.61  (step @p116 :rule bool-double-not-elim :args (@t136))
% 0.39/0.61  (step @p117 :rule refl :args (@t138))
% 0.39/0.61  (step @p118 :rule nary_cong :premises (@p117 @p116 @p35 @p115) :args ((or @t138 (not @t139) @t127 @t135)))
% 0.39/0.61  (assume-push @p1173 @t137)
% 0.39/0.61  (assume-push @p1174 @t139)
% 0.39/0.61  (assume-push @p1175 @t126)
% 0.39/0.61  (assume-push @p1176 @t139)
% 0.39/0.61  (assume-push @p1177 @t140)
% 0.39/0.61  (step @p124 :rule false_intro :premises (@p114))
% 0.39/0.61  (step @p125 :rule refl :args (@t36))
% 0.39/0.61  (step @p126 :rule cong :premises (@p1177 @p125) :args (@t134))
% 0.39/0.61  (step @p127 :rule trans :premises (@p126 @p124))
% 0.39/0.61  (step @p128 :rule false_elim :premises (@p127))
% 0.39/0.61  (step-pop @p1178 :rule scope :premises (@p128))
% 0.39/0.61  (step-pop @p1179 :rule scope :premises (@p1178))
% 0.39/0.61  (step @p129 :rule process_scope :premises (@p1179) :args (@t135))
% 0.39/0.61  (assume-push @p1180 @t126)
% 0.39/0.61  (assume-push @p1181 @t137)
% 0.39/0.61  (step @p134 :rule symm :premises (@p1175))
% 0.39/0.61  (step @p46 :rule refl :args (tptp.e2))
% 0.39/0.61  (step @p135 :rule cong :premises (@p46 @p134) :args (@t85))
% 0.39/0.61  (step @p136 :rule trans :premises (@p112 @p135))
% 0.39/0.61  (step-pop @p1182 :rule scope :premises (@p136))
% 0.39/0.61  (step-pop @p1183 :rule scope :premises (@p1182))
% 0.39/0.61  (step @p137 :rule process_scope :premises (@p1183) :args (@t140))
% 0.39/0.61  (step @p140 :rule and_intro :premises (@p1175 @p112))
% 0.39/0.61  (step @p141 :rule modus_ponens :premises (@p140 @p137))
% 0.39/0.61  (step @p142 :rule and_intro :premises (@p114 @p141))
% 0.39/0.61  (step @p143 :rule modus_ponens :premises (@p142 @p129))
% 0.39/0.61  (step-pop @p1184 :rule scope :premises (@p143))
% 0.39/0.61  (step-pop @p1185 :rule scope :premises (@p1184))
% 0.39/0.61  (step-pop @p1186 :rule scope :premises (@p1185))
% 0.39/0.61  (step @p144 :rule process_scope :premises (@p1186) :args (@t135))
% 0.39/0.61  (step @p148 :rule implies_elim :premises (@p144))
% 0.39/0.61  (step @p149 :rule cnf_and_neg :args (@t141))
% 0.39/0.61  (step @p150 :rule resolution :premises (@p149 @p148) :args (true @t141))
% 0.39/0.61  (step @p151 :rule eq_resolve :premises (@p150 @p118))
% 0.39/0.61  (step @p152 :rule reordering :premises (@p151) :args ((or @t136 @t135 @t138 @t127)))
% 0.39/0.61  (step @p153 :rule and_elim :premises (@p2) :args (3))
% 0.39/0.61  (step @p154 :rule symm :premises (@p153))
% 0.39/0.61  (step @p155 :rule and_elim :premises (@p4) :args (32))
% 0.39/0.61  (step @p156 :rule symm :premises (@p155))
% 0.39/0.61  (step @p157 :rule refl :args (@t143))
% 0.39/0.61  (step @p158 :rule bool-double-not-elim :args (@t144))
% 0.39/0.61  (step @p159 :rule refl :args (@t146))
% 0.39/0.61  (step @p160 :rule nary_cong :premises (@p159 @p158 @p35 @p157) :args ((or @t146 (not @t147) @t127 @t143)))
% 0.39/0.61  (assume-push @p1187 @t145)
% 0.39/0.61  (assume-push @p1188 @t147)
% 0.39/0.61  (assume-push @p1189 @t126)
% 0.39/0.61  (assume-push @p1190 @t147)
% 0.39/0.61  (assume-push @p1191 @t148)
% 0.39/0.61  (step @p166 :rule false_intro :premises (@p156))
% 0.39/0.61  (step @p167 :rule refl :args (@t57))
% 0.39/0.61  (step @p168 :rule cong :premises (@p1191 @p167) :args (@t142))
% 0.39/0.61  (step @p169 :rule trans :premises (@p168 @p166))
% 0.39/0.61  (step @p170 :rule false_elim :premises (@p169))
% 0.39/0.61  (step-pop @p1192 :rule scope :premises (@p170))
% 0.39/0.61  (step-pop @p1193 :rule scope :premises (@p1192))
% 0.39/0.61  (step @p171 :rule process_scope :premises (@p1193) :args (@t143))
% 0.39/0.61  (assume-push @p1194 @t126)
% 0.39/0.61  (assume-push @p1195 @t145)
% 0.39/0.61  (step @p176 :rule symm :premises (@p1189))
% 0.39/0.61  (step @p177 :rule refl :args (tptp.e1))
% 0.39/0.61  (step @p178 :rule cong :premises (@p177 @p176) :args (@t86))
% 0.39/0.61  (step @p179 :rule trans :premises (@p154 @p178))
% 0.39/0.61  (step-pop @p1196 :rule scope :premises (@p179))
% 0.39/0.61  (step-pop @p1197 :rule scope :premises (@p1196))
% 0.39/0.61  (step @p180 :rule process_scope :premises (@p1197) :args (@t148))
% 0.39/0.61  (step @p183 :rule and_intro :premises (@p1189 @p154))
% 0.39/0.61  (step @p184 :rule modus_ponens :premises (@p183 @p180))
% 0.39/0.61  (step @p185 :rule and_intro :premises (@p156 @p184))
% 0.39/0.61  (step @p186 :rule modus_ponens :premises (@p185 @p171))
% 0.39/0.61  (step-pop @p1198 :rule scope :premises (@p186))
% 0.39/0.61  (step-pop @p1199 :rule scope :premises (@p1198))
% 0.39/0.61  (step-pop @p1200 :rule scope :premises (@p1199))
% 0.39/0.61  (step @p187 :rule process_scope :premises (@p1200) :args (@t143))
% 0.39/0.61  (step @p191 :rule implies_elim :premises (@p187))
% 0.39/0.61  (step @p192 :rule cnf_and_neg :args (@t149))
% 0.39/0.61  (step @p193 :rule resolution :premises (@p192 @p191) :args (true @t149))
% 0.39/0.61  (step @p194 :rule eq_resolve :premises (@p193 @p160))
% 0.39/0.61  (step @p195 :rule reordering :premises (@p194) :args ((or @t144 @t143 @t146 @t127)))
% 0.39/0.61  (step @p196 :rule and_elim :premises (@p2) :args (2))
% 0.39/0.61  (step @p197 :rule symm :premises (@p196))
% 0.39/0.61  (step @p198 :rule and_elim :premises (@p4) :args (42))
% 0.39/0.61  (step @p199 :rule symm :premises (@p198))
% 0.39/0.61  (step @p200 :rule refl :args (@t150))
% 0.39/0.61  (step @p201 :rule bool-double-not-elim :args (@t151))
% 0.39/0.61  (step @p202 :rule refl :args (@t153))
% 0.39/0.61  (step @p203 :rule nary_cong :premises (@p202 @p201 @p35 @p200) :args ((or @t153 @t155 @t127 @t150)))
% 0.39/0.61  (assume-push @p1201 @t152)
% 0.39/0.61  (assume-push @p1202 @t154)
% 0.39/0.61  (assume-push @p1203 @t126)
% 0.39/0.61  (assume-push @p1204 @t154)
% 0.39/0.61  (assume-push @p1205 @t156)
% 0.39/0.61  (step @p209 :rule false_intro :premises (@p199))
% 0.39/0.61  (step @p210 :rule refl :args (@t16))
% 0.39/0.61  (step @p211 :rule cong :premises (@p1205 @p210) :args (@t116))
% 0.39/0.61  (step @p212 :rule trans :premises (@p211 @p209))
% 0.39/0.61  (step @p213 :rule false_elim :premises (@p212))
% 0.39/0.61  (step-pop @p1206 :rule scope :premises (@p213))
% 0.39/0.61  (step-pop @p1207 :rule scope :premises (@p1206))
% 0.39/0.61  (step @p214 :rule process_scope :premises (@p1207) :args (@t150))
% 0.39/0.61  (assume-push @p1208 @t126)
% 0.39/0.61  (assume-push @p1209 @t152)
% 0.39/0.61  (step @p177 :rule refl :args (tptp.e1))
% 0.39/0.61  (step @p219 :rule symm :premises (@p1203))
% 0.39/0.61  (step @p220 :rule cong :premises (@p219 @p177) :args (@t87))
% 0.39/0.61  (step @p221 :rule trans :premises (@p197 @p220))
% 0.39/0.61  (step-pop @p1210 :rule scope :premises (@p221))
% 0.39/0.61  (step-pop @p1211 :rule scope :premises (@p1210))
% 0.39/0.61  (step @p222 :rule process_scope :premises (@p1211) :args (@t156))
% 0.39/0.61  (step @p225 :rule and_intro :premises (@p1203 @p197))
% 0.39/0.61  (step @p226 :rule modus_ponens :premises (@p225 @p222))
% 0.39/0.61  (step @p227 :rule and_intro :premises (@p199 @p226))
% 0.39/0.61  (step @p228 :rule modus_ponens :premises (@p227 @p214))
% 0.39/0.61  (step-pop @p1212 :rule scope :premises (@p228))
% 0.39/0.61  (step-pop @p1213 :rule scope :premises (@p1212))
% 0.39/0.61  (step-pop @p1214 :rule scope :premises (@p1213))
% 0.39/0.61  (step @p229 :rule process_scope :premises (@p1214) :args (@t150))
% 0.39/0.61  (step @p233 :rule implies_elim :premises (@p229))
% 0.39/0.61  (step @p234 :rule cnf_and_neg :args (@t157))
% 0.39/0.61  (step @p235 :rule resolution :premises (@p234 @p233) :args (true @t157))
% 0.39/0.61  (step @p236 :rule eq_resolve :premises (@p235 @p203))
% 0.39/0.61  (step @p237 :rule reordering :premises (@p236) :args ((or @t151 @t150 @t153 @t127)))
% 0.39/0.61  (step @p238 :rule and_elim :premises (@p2) :args (0))
% 0.39/0.61  (step @p239 :rule symm :premises (@p238))
% 0.39/0.61  (step @p240 :rule and_elim :premises (@p4) :args (5))
% 0.39/0.61  (step @p241 :rule symm :premises (@p240))
% 0.39/0.61  (step @p242 :rule refl :args (@t159))
% 0.39/0.61  (step @p243 :rule bool-double-not-elim :args (@t160))
% 0.39/0.61  (step @p244 :rule refl :args (@t162))
% 0.39/0.61  (step @p245 :rule nary_cong :premises (@p244 @p243 @p35 @p242) :args ((or @t162 (not @t163) @t127 @t159)))
% 0.39/0.61  (assume-push @p1215 @t161)
% 0.39/0.61  (assume-push @p1216 @t163)
% 0.39/0.61  (assume-push @p1217 @t126)
% 0.39/0.61  (assume-push @p1218 @t163)
% 0.39/0.61  (assume-push @p1219 @t164)
% 0.39/0.61  (step @p251 :rule false_intro :premises (@p241))
% 0.39/0.61  (step @p125 :rule refl :args (@t36))
% 0.39/0.61  (step @p252 :rule cong :premises (@p1219 @p125) :args (@t158))
% 0.39/0.61  (step @p253 :rule trans :premises (@p252 @p251))
% 0.39/0.61  (step @p254 :rule false_elim :premises (@p253))
% 0.39/0.61  (step-pop @p1220 :rule scope :premises (@p254))
% 0.39/0.61  (step-pop @p1221 :rule scope :premises (@p1220))
% 0.39/0.61  (step @p255 :rule process_scope :premises (@p1221) :args (@t159))
% 0.39/0.61  (assume-push @p1222 @t126)
% 0.39/0.61  (assume-push @p1223 @t161)
% 0.39/0.61  (step @p86 :rule refl :args (tptp.e0))
% 0.39/0.61  (step @p260 :rule symm :premises (@p1217))
% 0.39/0.61  (step @p261 :rule cong :premises (@p260 @p86) :args (@t88))
% 0.39/0.61  (step @p262 :rule trans :premises (@p239 @p261))
% 0.39/0.61  (step-pop @p1224 :rule scope :premises (@p262))
% 0.39/0.61  (step-pop @p1225 :rule scope :premises (@p1224))
% 0.39/0.61  (step @p263 :rule process_scope :premises (@p1225) :args (@t164))
% 0.39/0.61  (step @p266 :rule and_intro :premises (@p1217 @p239))
% 0.39/0.61  (step @p267 :rule modus_ponens :premises (@p266 @p263))
% 0.39/0.61  (step @p268 :rule and_intro :premises (@p241 @p267))
% 0.39/0.61  (step @p269 :rule modus_ponens :premises (@p268 @p255))
% 0.39/0.61  (step-pop @p1226 :rule scope :premises (@p269))
% 0.39/0.61  (step-pop @p1227 :rule scope :premises (@p1226))
% 0.39/0.61  (step-pop @p1228 :rule scope :premises (@p1227))
% 0.39/0.61  (step @p270 :rule process_scope :premises (@p1228) :args (@t159))
% 0.39/0.61  (step @p274 :rule implies_elim :premises (@p270))
% 0.39/0.61  (step @p275 :rule cnf_and_neg :args (@t165))
% 0.39/0.61  (step @p276 :rule resolution :premises (@p275 @p274) :args (true @t165))
% 0.39/0.61  (step @p277 :rule eq_resolve :premises (@p276 @p245))
% 0.39/0.61  (step @p278 :rule reordering :premises (@p277) :args ((or @t160 @t159 @t162 @t127)))
% 0.39/0.61  (step @p279 :rule cnf_and_pos :args (@t167 3))
% 0.39/0.61  (step @p280 :rule reordering :premises (@p279) :args ((or @t120 @t168)))
% 0.39/0.61  (step @p281 :rule cnf_and_pos :args (@t170 3))
% 0.39/0.61  (step @p282 :rule reordering :premises (@p281) :args ((or @t110 @t171)))
% 0.39/0.61  (step @p283 :rule cnf_and_pos :args (@t173 0))
% 0.39/0.61  (step @p284 :rule reordering :premises (@p283) :args ((or @t111 @t174)))
% 0.39/0.61  (step @p285 :rule cnf_and_pos :args (@t173 1))
% 0.39/0.61  (step @p286 :rule reordering :premises (@p285) :args ((or @t172 @t174)))
% 0.39/0.61  (step @p287 :rule cnf_and_pos :args (@t173 2))
% 0.39/0.61  (step @p288 :rule reordering :premises (@p287) :args ((or @t113 @t174)))
% 0.39/0.61  (step @p289 :rule cnf_and_pos :args (@t173 3))
% 0.39/0.61  (step @p290 :rule reordering :premises (@p289) :args ((or @t115 @t174)))
% 0.39/0.61  (step @p291 :rule not_and :premises (@p16))
% 0.39/0.61  (step @p292 :rule reordering :premises (@p291) :args ((or (not @t114) @t175)))
% 0.39/0.61  (step @p293 :rule and_elim :premises (@p4) :args (30))
% 0.39/0.61  (step @p294 :rule symm :premises (@p293))
% 0.39/0.61  (assume-push @p1229 @t145)
% 0.39/0.61  (assume-push @p1230 @t172)
% 0.39/0.61  (assume-push @p1231 @t176)
% 0.39/0.61  (assume-push @p1232 @t176)
% 0.39/0.61  (assume-push @p1233 @t145)
% 0.39/0.61  (assume-push @p1234 @t172)
% 0.39/0.61  (step @p301 :rule symm :premises (@p1231))
% 0.39/0.61  (step @p177 :rule refl :args (tptp.e1))
% 0.39/0.61  (step @p302 :rule cong :premises (@p177 @p301) :args (@t86))
% 0.39/0.61  (step @p303 :rule symm :premises (@p1230))
% 0.39/0.61  (step @p304 :rule trans :premises (@p303 @p154 @p302))
% 0.39/0.61  (step-pop @p1235 :rule scope :premises (@p304))
% 0.39/0.61  (step-pop @p1236 :rule scope :premises (@p1235))
% 0.39/0.61  (step-pop @p1237 :rule scope :premises (@p1236))
% 0.39/0.61  (step @p305 :rule process_scope :premises (@p1237) :args (@t177))
% 0.39/0.61  (step @p309 :rule and_intro :premises (@p1231 @p154 @p1230))
% 0.39/0.61  (step @p310 :rule modus_ponens :premises (@p309 @p305))
% 0.39/0.61  (step-pop @p1238 :rule scope :premises (@p310))
% 0.39/0.61  (step-pop @p1239 :rule scope :premises (@p1238))
% 0.39/0.61  (step-pop @p1240 :rule scope :premises (@p1239))
% 0.39/0.61  (step @p311 :rule process_scope :premises (@p1240) :args (@t177))
% 0.39/0.61  (step @p315 :rule implies_elim :premises (@p311))
% 0.39/0.61  (step @p316 :rule cnf_and_neg :args (@t178))
% 0.39/0.61  (step @p317 :rule resolution :premises (@p316 @p315) :args (true @t178))
% 0.39/0.61  (step @p318 :rule reordering :premises (@p317) :args ((or @t177 (not @t172) @t146 @t179)))
% 0.39/0.61  (step @p319 :rule and_elim :premises (@p5) :args (3))
% 0.39/0.61  (assume-push @p1241 @t113)
% 0.39/0.61  (assume-push @p1242 @t137)
% 0.39/0.61  (assume-push @p1243 @t180)
% 0.39/0.61  (assume-push @p1244 @t137)
% 0.39/0.61  (assume-push @p1245 @t180)
% 0.39/0.61  (assume-push @p1246 @t113)
% 0.39/0.61  (step @p46 :rule refl :args (tptp.e2))
% 0.39/0.61  (step @p326 :rule cong :premises (@p46 @p1243) :args (@t26))
% 0.39/0.61  (step @p327 :rule trans :premises (@p1241 @p326 @p111))
% 0.39/0.61  (step-pop @p1247 :rule scope :premises (@p327))
% 0.39/0.61  (step-pop @p1248 :rule scope :premises (@p1247))
% 0.39/0.61  (step-pop @p1249 :rule scope :premises (@p1248))
% 0.39/0.61  (step @p328 :rule process_scope :premises (@p1249) :args (@t95))
% 0.39/0.61  (step @p332 :rule and_intro :premises (@p112 @p1243 @p1241))
% 0.39/0.61  (step @p333 :rule modus_ponens :premises (@p332 @p328))
% 0.39/0.61  (step-pop @p1250 :rule scope :premises (@p333))
% 0.39/0.61  (step-pop @p1251 :rule scope :premises (@p1250))
% 0.39/0.61  (step-pop @p1252 :rule scope :premises (@p1251))
% 0.39/0.61  (step @p334 :rule process_scope :premises (@p1252) :args (@t95))
% 0.39/0.61  (step @p338 :rule implies_elim :premises (@p334))
% 0.39/0.61  (step @p339 :rule cnf_and_neg :args (@t181))
% 0.39/0.61  (step @p340 :rule resolution :premises (@p339 @p338) :args (true @t181))
% 0.39/0.61  (step @p341 :rule reordering :premises (@p340) :args ((or @t95 @t175 @t138 @t182)))
% 0.39/0.61  (step @p342 :rule and_elim :premises (@p5) :args (4))
% 0.39/0.61  (assume-push @p1253 @t115)
% 0.39/0.61  (assume-push @p1254 @t128)
% 0.39/0.61  (assume-push @p1255 @t126)
% 0.39/0.61  (assume-push @p1256 @t128)
% 0.39/0.61  (assume-push @p1257 @t126)
% 0.39/0.61  (assume-push @p1258 @t115)
% 0.39/0.61  (step @p56 :rule refl :args (tptp.e3))
% 0.39/0.61  (step @p349 :rule cong :premises (@p56 @p1255) :args (@t1))
% 0.39/0.61  (step @p350 :rule trans :premises (@p1253 @p349 @p31))
% 0.39/0.61  (step-pop @p1259 :rule scope :premises (@p350))
% 0.39/0.61  (step-pop @p1260 :rule scope :premises (@p1259))
% 0.39/0.61  (step-pop @p1261 :rule scope :premises (@p1260))
% 0.39/0.61  (step @p351 :rule process_scope :premises (@p1261) :args (@t94))
% 0.39/0.61  (step @p355 :rule and_intro :premises (@p32 @p1255 @p1253))
% 0.39/0.61  (step @p356 :rule modus_ponens :premises (@p355 @p351))
% 0.39/0.61  (step-pop @p1262 :rule scope :premises (@p356))
% 0.39/0.61  (step-pop @p1263 :rule scope :premises (@p1262))
% 0.39/0.61  (step-pop @p1264 :rule scope :premises (@p1263))
% 0.39/0.61  (step @p357 :rule process_scope :premises (@p1264) :args (@t94))
% 0.39/0.61  (step @p361 :rule implies_elim :premises (@p357))
% 0.39/0.61  (step @p362 :rule cnf_and_neg :args (@t183))
% 0.39/0.61  (step @p363 :rule resolution :premises (@p362 @p361) :args (true @t183))
% 0.39/0.61  (step @p364 :rule reordering :premises (@p363) :args ((or @t94 (not @t115) @t129 @t127)))
% 0.39/0.61  (step @p365 :rule refl :args (@t184))
% 0.39/0.61  (step @p366 :rule bool-double-not-elim :args (@t126))
% 0.39/0.61  (step @p367 :rule refl :args (@t186))
% 0.39/0.61  (step @p368 :rule refl :args (@t187))
% 0.39/0.61  (step @p369 :rule nary_cong :premises (@p368 @p367 @p366 @p365) :args ((or @t187 @t186 @t188 @t184)))
% 0.39/0.61  (assume-push @p1265 @t111)
% 0.39/0.61  (assume-push @p1266 @t185)
% 0.39/0.61  (assume-push @p1267 @t127)
% 0.39/0.61  (assume-push @p1268 @t127)
% 0.39/0.61  (assume-push @p1269 @t185)
% 0.39/0.61  (assume-push @p1270 @t111)
% 0.39/0.61  (step @p376 :rule false_intro :premises (@p1267))
% 0.39/0.61  (step @p377 :rule symm :premises (@p1265))
% 0.39/0.61  (step @p378 :rule trans :premises (@p377 @p1266))
% 0.39/0.61  (step @p56 :rule refl :args (tptp.e3))
% 0.39/0.61  (step @p379 :rule cong :premises (@p56 @p378) :args (@t122))
% 0.39/0.61  (step @p380 :rule trans :premises (@p379 @p376))
% 0.39/0.61  (step @p381 :rule false_elim :premises (@p380))
% 0.39/0.61  (step-pop @p1271 :rule scope :premises (@p381))
% 0.39/0.61  (step-pop @p1272 :rule scope :premises (@p1271))
% 0.39/0.61  (step-pop @p1273 :rule scope :premises (@p1272))
% 0.39/0.61  (step @p382 :rule process_scope :premises (@p1273) :args (@t184))
% 0.39/0.61  (step @p386 :rule and_intro :premises (@p1267 @p1266 @p1265))
% 0.39/0.61  (step @p387 :rule modus_ponens :premises (@p386 @p382))
% 0.39/0.61  (step-pop @p1274 :rule scope :premises (@p387))
% 0.39/0.61  (step-pop @p1275 :rule scope :premises (@p1274))
% 0.39/0.61  (step-pop @p1276 :rule scope :premises (@p1275))
% 0.39/0.61  (step @p388 :rule process_scope :premises (@p1276) :args (@t184))
% 0.39/0.61  (step @p392 :rule implies_elim :premises (@p388))
% 0.39/0.61  (step @p393 :rule cnf_and_neg :args (@t189))
% 0.39/0.61  (step @p394 :rule resolution :premises (@p393 @p392) :args (true @t189))
% 0.39/0.61  (step @p395 :rule eq_resolve :premises (@p394 @p369))
% 0.39/0.61  (step @p396 :rule reordering :premises (@p395) :args ((or @t126 @t187 @t184 @t186)))
% 0.39/0.61  (step @p397 :rule and_elim :premises (@p4) :args (8))
% 0.39/0.61  (step @p398 :rule symm :premises (@p397))
% 0.39/0.61  (step @p399 :rule refl :args (@t190))
% 0.39/0.61  (step @p400 :rule bool-double-not-elim :args (@t191))
% 0.39/0.61  (step @p401 :rule nary_cong :premises (@p36 @p400 @p367 @p399) :args ((or @t129 (not @t192) @t186 @t190)))
% 0.39/0.61  (assume-push @p1277 @t128)
% 0.39/0.61  (assume-push @p1278 @t192)
% 0.39/0.61  (assume-push @p1279 @t185)
% 0.39/0.61  (assume-push @p1280 @t192)
% 0.39/0.61  (assume-push @p1281 @t193)
% 0.39/0.61  (step @p407 :rule false_intro :premises (@p398))
% 0.39/0.61  (step @p408 :rule refl :args (@t72))
% 0.39/0.61  (step @p409 :rule cong :premises (@p1281 @p408) :args (@t119))
% 0.39/0.61  (step @p410 :rule trans :premises (@p409 @p407))
% 0.39/0.61  (step @p411 :rule false_elim :premises (@p410))
% 0.39/0.61  (step-pop @p1282 :rule scope :premises (@p411))
% 0.39/0.61  (step-pop @p1283 :rule scope :premises (@p1282))
% 0.39/0.61  (step @p412 :rule process_scope :premises (@p1283) :args (@t190))
% 0.39/0.61  (assume-push @p1284 @t185)
% 0.39/0.61  (assume-push @p1285 @t128)
% 0.39/0.61  (step @p417 :rule symm :premises (@p1279))
% 0.39/0.61  (step @p56 :rule refl :args (tptp.e3))
% 0.39/0.61  (step @p418 :rule cong :premises (@p56 @p417) :args (@t83))
% 0.39/0.61  (step @p419 :rule trans :premises (@p32 @p418))
% 0.39/0.61  (step-pop @p1286 :rule scope :premises (@p419))
% 0.39/0.61  (step-pop @p1287 :rule scope :premises (@p1286))
% 0.39/0.61  (step @p420 :rule process_scope :premises (@p1287) :args (@t193))
% 0.39/0.61  (step @p423 :rule and_intro :premises (@p1279 @p32))
% 0.39/0.61  (step @p424 :rule modus_ponens :premises (@p423 @p420))
% 0.39/0.61  (step @p425 :rule and_intro :premises (@p398 @p424))
% 0.39/0.61  (step @p426 :rule modus_ponens :premises (@p425 @p412))
% 0.39/0.61  (step-pop @p1288 :rule scope :premises (@p426))
% 0.39/0.61  (step-pop @p1289 :rule scope :premises (@p1288))
% 0.39/0.61  (step-pop @p1290 :rule scope :premises (@p1289))
% 0.39/0.61  (step @p427 :rule process_scope :premises (@p1290) :args (@t190))
% 0.39/0.61  (step @p431 :rule implies_elim :premises (@p427))
% 0.39/0.61  (step @p432 :rule cnf_and_neg :args (@t194))
% 0.39/0.61  (step @p433 :rule resolution :premises (@p432 @p431) :args (true @t194))
% 0.39/0.61  (step @p434 :rule eq_resolve :premises (@p433 @p401))
% 0.39/0.61  (step @p435 :rule reordering :premises (@p434) :args ((or @t191 @t190 @t129 @t186)))
% 0.39/0.61  (step @p436 :rule and_elim :premises (@p2) :args (6))
% 0.39/0.61  (step @p437 :rule symm :premises (@p436))
% 0.39/0.61  (step @p438 :rule and_elim :premises (@p4) :args (18))
% 0.39/0.61  (step @p439 :rule symm :premises (@p438))
% 0.39/0.61  (step @p440 :rule refl :args (@t196))
% 0.39/0.61  (step @p441 :rule bool-double-not-elim :args (@t197))
% 0.39/0.61  (step @p442 :rule refl :args (@t199))
% 0.39/0.61  (step @p443 :rule nary_cong :premises (@p442 @p441 @p367 @p440) :args ((or @t199 (not @t200) @t186 @t196)))
% 0.39/0.61  (assume-push @p1291 @t198)
% 0.39/0.61  (assume-push @p1292 @t200)
% 0.39/0.61  (assume-push @p1293 @t185)
% 0.39/0.61  (assume-push @p1294 @t200)
% 0.39/0.61  (assume-push @p1295 @t201)
% 0.39/0.61  (step @p449 :rule false_intro :premises (@p439))
% 0.39/0.61  (step @p450 :rule refl :args (@t62))
% 0.39/0.61  (step @p451 :rule cong :premises (@p1295 @p450) :args (@t195))
% 0.39/0.61  (step @p452 :rule trans :premises (@p451 @p449))
% 0.39/0.61  (step @p453 :rule false_elim :premises (@p452))
% 0.39/0.61  (step-pop @p1296 :rule scope :premises (@p453))
% 0.39/0.61  (step-pop @p1297 :rule scope :premises (@p1296))
% 0.39/0.61  (step @p454 :rule process_scope :premises (@p1297) :args (@t196))
% 0.39/0.61  (assume-push @p1298 @t185)
% 0.39/0.61  (assume-push @p1299 @t198)
% 0.39/0.61  (step @p56 :rule refl :args (tptp.e3))
% 0.39/0.61  (step @p459 :rule symm :premises (@p1293))
% 0.39/0.61  (step @p460 :rule cong :premises (@p459 @p56) :args (@t84))
% 0.39/0.61  (step @p461 :rule trans :premises (@p437 @p460))
% 0.39/0.61  (step-pop @p1300 :rule scope :premises (@p461))
% 0.39/0.61  (step-pop @p1301 :rule scope :premises (@p1300))
% 0.39/0.61  (step @p462 :rule process_scope :premises (@p1301) :args (@t201))
% 0.39/0.61  (step @p465 :rule and_intro :premises (@p1293 @p437))
% 0.39/0.61  (step @p466 :rule modus_ponens :premises (@p465 @p462))
% 0.39/0.61  (step @p467 :rule and_intro :premises (@p439 @p466))
% 0.39/0.61  (step @p468 :rule modus_ponens :premises (@p467 @p454))
% 0.39/0.61  (step-pop @p1302 :rule scope :premises (@p468))
% 0.39/0.61  (step-pop @p1303 :rule scope :premises (@p1302))
% 0.39/0.61  (step-pop @p1304 :rule scope :premises (@p1303))
% 0.39/0.61  (step @p469 :rule process_scope :premises (@p1304) :args (@t196))
% 0.39/0.61  (step @p473 :rule implies_elim :premises (@p469))
% 0.39/0.61  (step @p474 :rule cnf_and_neg :args (@t202))
% 0.39/0.61  (step @p475 :rule resolution :premises (@p474 @p473) :args (true @t202))
% 0.39/0.61  (step @p476 :rule eq_resolve :premises (@p475 @p443))
% 0.39/0.61  (step @p477 :rule reordering :premises (@p476) :args ((or @t197 @t196 @t199 @t186)))
% 0.39/0.61  (step @p478 :rule eq-symm :args (@t62 tptp.e3))
% 0.39/0.61  (step @p479 :rule eq-symm :args (@t67 tptp.e3))
% 0.39/0.61  (step @p480 :rule eq-symm :args (@t72 tptp.e3))
% 0.39/0.61  (step @p481 :rule eq-symm :args (@t77 tptp.e3))
% 0.39/0.61  (step @p482 :rule nary_cong :premises (@p481 @p480 @p479 @p478) :args (@t90))
% 0.39/0.61  (step @p483 :rule and_elim :premises (@p3) :args (6))
% 0.39/0.61  (step @p484 :rule eq_resolve :premises (@p483 @p482))
% 0.39/0.61  (step @p485 :rule reordering :premises (@p484) :args ((or @t114 @t119 @t122 @t195)))
% 0.39/0.61  (step @p486 :rule chain_m_resolution :premises (@p485 @p477 @p439 @p437 @p435 @p398 @p32 @p396) :args ((or @t114 @t126 @t187 @t186) (@list true true false true true false true) (@list @t195 @t197 @t198 @t119 @t191 @t128 @t122)))
% 0.39/0.61  (step @p487 :rule eq-symm :args (tptp.unit tptp.e3))
% 0.39/0.61  (step @p488 :rule eq-symm :args (tptp.unit tptp.e2))
% 0.39/0.61  (step @p489 :rule eq-symm :args (tptp.unit tptp.e1))
% 0.39/0.61  (step @p490 :rule eq-symm :args (tptp.unit tptp.e0))
% 0.39/0.61  (step @p491 :rule nary_cong :premises (@p490 @p489 @p488 @p487) :args (@t82))
% 0.39/0.61  (step @p492 :rule and_elim :premises (@p2) :args (8))
% 0.39/0.61  (step @p493 :rule eq_resolve :premises (@p492 @p491))
% 0.39/0.61  (step @p494 :rule chain_m_resolution :premises (@p493 @p486 @p364 @p342 @p32 @p341 @p319 @p112 @p318 @p294 @p154 @p292 @p290 @p288 @p286 @p284) :args (@t174 (@list true true true false true true false true true false true false false false false) (@list @t185 @t126 @t94 @t128 @t180 @t95 @t137 @t176 @t177 @t145 @t114 @t115 @t113 @t172 @t111)))
% 0.39/0.61  (step @p495 :rule eq-symm :args (@t1 tptp.e3))
% 0.39/0.61  (step @p496 :rule eq-symm :args (@t26 tptp.e3))
% 0.39/0.61  (step @p497 :rule eq-symm :args (@t52 tptp.e3))
% 0.39/0.61  (step @p498 :rule nary_cong :premises (@p481 @p497 @p496 @p495) :args (@t102))
% 0.39/0.61  (step @p499 :rule eq-symm :args (@t1 tptp.e2))
% 0.39/0.61  (step @p500 :rule eq-symm :args (@t26 tptp.e2))
% 0.39/0.61  (step @p501 :rule eq-symm :args (@t52 tptp.e2))
% 0.39/0.61  (step @p502 :rule eq-symm :args (@t77 tptp.e2))
% 0.39/0.61  (step @p503 :rule nary_cong :premises (@p502 @p501 @p500 @p499) :args (@t103))
% 0.39/0.61  (step @p504 :rule eq-symm :args (@t1 tptp.e1))
% 0.39/0.61  (step @p505 :rule eq-symm :args (@t26 tptp.e1))
% 0.39/0.61  (step @p506 :rule eq-symm :args (@t52 tptp.e1))
% 0.39/0.61  (step @p507 :rule eq-symm :args (@t77 tptp.e1))
% 0.39/0.61  (step @p508 :rule nary_cong :premises (@p507 @p506 @p505 @p504) :args (@t104))
% 0.39/0.61  (step @p509 :rule eq-symm :args (@t1 tptp.e0))
% 0.39/0.61  (step @p510 :rule eq-symm :args (@t26 tptp.e0))
% 0.39/0.61  (step @p511 :rule eq-symm :args (@t52 tptp.e0))
% 0.39/0.61  (step @p512 :rule eq-symm :args (@t77 tptp.e0))
% 0.39/0.61  (step @p513 :rule nary_cong :premises (@p512 @p511 @p510 @p509) :args (@t105))
% 0.39/0.61  (step @p514 :rule nary_cong :premises (@p513 @p508 @p503 @p498) :args (@t106))
% 0.39/0.61  (step @p515 :rule eq_resolve :premises (@p6 @p514))
% 0.39/0.61  (step @p516 :rule cnf_and_pos :args (@t203 0))
% 0.39/0.61  (step @p517 :rule reordering :premises (@p516) :args ((or @t122 @t204)))
% 0.39/0.61  (step @p518 :rule not_and :premises (@p25))
% 0.39/0.61  (step @p519 :rule eq-symm :args (@t16 tptp.e1))
% 0.39/0.61  (step @p520 :rule eq-symm :args (@t36 tptp.e1))
% 0.39/0.61  (step @p521 :rule eq-symm :args (@t57 tptp.e1))
% 0.39/0.61  (step @p522 :rule nary_cong :premises (@p507 @p521 @p520 @p519) :args (@t91))
% 0.39/0.61  (step @p523 :rule and_elim :premises (@p3) :args (3))
% 0.39/0.61  (step @p524 :rule eq_resolve :premises (@p523 @p522))
% 0.39/0.61  (step @p525 :rule reordering :premises (@p524) :args ((or @t111 @t116 @t121 @t142)))
% 0.39/0.61  (step @p526 :rule eq-symm :args (@t36 tptp.e3))
% 0.39/0.61  (step @p527 :rule eq-symm :args (@t36 tptp.e2))
% 0.39/0.61  (step @p528 :rule eq-symm :args (@t36 tptp.e0))
% 0.39/0.61  (step @p529 :rule nary_cong :premises (@p528 @p520 @p527 @p526) :args (@t41))
% 0.39/0.61  (step @p530 :rule and_elim :premises (@p1) :args (8))
% 0.39/0.61  (step @p531 :rule eq_resolve :premises (@p530 @p529))
% 0.39/0.61  (step @p532 :rule reordering :premises (@p531) :args ((or @t112 @t121 @t158 @t134)))
% 0.39/0.61  (step @p533 :rule not_and :premises (@p14))
% 0.39/0.61  (step @p534 :rule chain_m_resolution :premises (@p533 @p532 @p525 @p518 @p517 @p515 @p494 @p282 @p280 @p278 @p241 @p239 @p237 @p199 @p197 @p195 @p156 @p154 @p152 @p114 @p112 @p110 @p75 @p32 @p74 @p33 @p32) :args (@t127 (@list false false true false false true true true true true false true true false true true false true true false true true false true true false) (@list @t112 @t111 @t121 @t122 @t203 @t173 @t170 @t167 @t158 @t160 @t161 @t116 @t151 @t152 @t142 @t144 @t145 @t134 @t136 @t137 @t110 @t96 @t128 @t120 @t92 @t128)))
% 0.39/0.61  (step @p535 :rule and_elim :premises (@p5) :args (0))
% 0.39/0.61  (step @p536 :rule refl :args (@t205))
% 0.39/0.61  (step @p537 :rule bool-double-not-elim :args (@t100))
% 0.39/0.61  (step @p538 :rule nary_cong :premises (@p537 @p368 @p536) :args ((or @t206 @t187 @t205)))
% 0.39/0.61  (assume-push @p1305 @t101)
% 0.39/0.61  (assume-push @p1306 @t111)
% 0.39/0.61  (assume-push @p1307 @t101)
% 0.39/0.61  (assume-push @p1308 @t111)
% 0.39/0.61  (step @p543 :rule false_intro :premises (@p535))
% 0.39/0.61  (step @p544 :rule symm :premises (@p1306))
% 0.39/0.61  (step @p86 :rule refl :args (tptp.e0))
% 0.39/0.61  (step @p545 :rule cong :premises (@p86 @p544) :args (@t169))
% 0.39/0.61  (step @p546 :rule trans :premises (@p545 @p543))
% 0.39/0.61  (step @p547 :rule false_elim :premises (@p546))
% 0.39/0.61  (step-pop @p1309 :rule scope :premises (@p547))
% 0.39/0.61  (step-pop @p1310 :rule scope :premises (@p1309))
% 0.39/0.61  (step @p548 :rule process_scope :premises (@p1310) :args (@t205))
% 0.39/0.61  (step @p551 :rule and_intro :premises (@p535 @p1306))
% 0.39/0.61  (step @p552 :rule modus_ponens :premises (@p551 @p548))
% 0.39/0.61  (step-pop @p1311 :rule scope :premises (@p552))
% 0.39/0.61  (step-pop @p1312 :rule scope :premises (@p1311))
% 0.39/0.61  (step @p553 :rule process_scope :premises (@p1312) :args (@t205))
% 0.39/0.61  (step @p556 :rule implies_elim :premises (@p553))
% 0.39/0.61  (step @p557 :rule cnf_and_neg :args (@t207))
% 0.39/0.61  (step @p558 :rule resolution :premises (@p557 @p556) :args (true @t207))
% 0.39/0.61  (step @p559 :rule eq_resolve :premises (@p558 @p538))
% 0.39/0.61  (step @p560 :rule reordering :premises (@p559) :args ((or @t100 @t205 @t187)))
% 0.39/0.61  (step @p561 :rule cnf_and_pos :args (@t170 0))
% 0.39/0.61  (step @p562 :rule reordering :premises (@p561) :args ((or @t169 @t171)))
% 0.39/0.61  (step @p563 :rule and_elim :premises (@p4) :args (0))
% 0.39/0.61  (step @p564 :rule symm :premises (@p563))
% 0.39/0.61  (assume-push @p1313 @t111)
% 0.39/0.61  (assume-push @p1314 @t145)
% 0.39/0.61  (assume-push @p1315 @t176)
% 0.39/0.61  (assume-push @p1316 @t111)
% 0.39/0.61  (assume-push @p1317 @t145)
% 0.39/0.61  (assume-push @p1318 @t176)
% 0.39/0.61  (step @p177 :rule refl :args (tptp.e1))
% 0.39/0.61  (step @p571 :rule cong :premises (@p177 @p1315) :args (@t57))
% 0.39/0.61  (step @p572 :rule trans :premises (@p571 @p153 @p1313))
% 0.39/0.61  (step-pop @p1319 :rule scope :premises (@p572))
% 0.39/0.61  (step-pop @p1320 :rule scope :premises (@p1319))
% 0.39/0.61  (step-pop @p1321 :rule scope :premises (@p1320))
% 0.39/0.61  (step @p573 :rule process_scope :premises (@p1321) :args (@t208))
% 0.39/0.61  (step @p577 :rule and_intro :premises (@p1313 @p154 @p1315))
% 0.39/0.61  (step @p578 :rule modus_ponens :premises (@p577 @p573))
% 0.39/0.61  (step-pop @p1322 :rule scope :premises (@p578))
% 0.39/0.61  (step-pop @p1323 :rule scope :premises (@p1322))
% 0.39/0.61  (step-pop @p1324 :rule scope :premises (@p1323))
% 0.39/0.61  (step @p579 :rule process_scope :premises (@p1324) :args (@t208))
% 0.39/0.61  (step @p583 :rule implies_elim :premises (@p579))
% 0.39/0.61  (step @p584 :rule cnf_and_neg :args (@t209))
% 0.39/0.61  (step @p585 :rule resolution :premises (@p584 @p583) :args (true @t209))
% 0.39/0.61  (step @p586 :rule reordering :premises (@p585) :args ((or @t208 @t187 @t146 @t179)))
% 0.39/0.61  (step @p587 :rule and_elim :premises (@p4) :args (17))
% 0.39/0.61  (step @p588 :rule symm :premises (@p587))
% 0.39/0.61  (step @p589 :rule refl :args (@t210))
% 0.39/0.61  (step @p590 :rule refl :args (@t182))
% 0.39/0.61  (step @p591 :rule bool-double-not-elim :args (@t211))
% 0.39/0.61  (step @p592 :rule nary_cong :premises (@p36 @p591 @p590 @p589) :args ((or @t129 (not @t212) @t182 @t210)))
% 0.39/0.61  (assume-push @p1325 @t128)
% 0.39/0.61  (assume-push @p1326 @t212)
% 0.39/0.61  (assume-push @p1327 @t180)
% 0.39/0.61  (assume-push @p1328 @t212)
% 0.39/0.61  (assume-push @p1329 @t213)
% 0.39/0.61  (step @p598 :rule false_intro :premises (@p588))
% 0.39/0.61  (step @p599 :rule refl :args (@t26))
% 0.39/0.61  (step @p600 :rule cong :premises (@p1329 @p599) :args (@t124))
% 0.39/0.61  (step @p601 :rule trans :premises (@p600 @p598))
% 0.39/0.61  (step @p602 :rule false_elim :premises (@p601))
% 0.39/0.61  (step-pop @p1330 :rule scope :premises (@p602))
% 0.39/0.61  (step-pop @p1331 :rule scope :premises (@p1330))
% 0.39/0.61  (step @p603 :rule process_scope :premises (@p1331) :args (@t210))
% 0.39/0.61  (assume-push @p1332 @t180)
% 0.39/0.61  (assume-push @p1333 @t128)
% 0.39/0.61  (step @p608 :rule symm :premises (@p1327))
% 0.39/0.61  (step @p56 :rule refl :args (tptp.e3))
% 0.39/0.61  (step @p609 :rule cong :premises (@p56 @p608) :args (@t83))
% 0.39/0.61  (step @p610 :rule trans :premises (@p32 @p609))
% 0.39/0.61  (step-pop @p1334 :rule scope :premises (@p610))
% 0.39/0.61  (step-pop @p1335 :rule scope :premises (@p1334))
% 0.39/0.61  (step @p611 :rule process_scope :premises (@p1335) :args (@t213))
% 0.39/0.61  (step @p614 :rule and_intro :premises (@p1327 @p32))
% 0.39/0.61  (step @p615 :rule modus_ponens :premises (@p614 @p611))
% 0.39/0.61  (step @p616 :rule and_intro :premises (@p588 @p615))
% 0.39/0.61  (step @p617 :rule modus_ponens :premises (@p616 @p603))
% 0.39/0.61  (step-pop @p1336 :rule scope :premises (@p617))
% 0.39/0.61  (step-pop @p1337 :rule scope :premises (@p1336))
% 0.39/0.61  (step-pop @p1338 :rule scope :premises (@p1337))
% 0.39/0.61  (step @p618 :rule process_scope :premises (@p1338) :args (@t210))
% 0.39/0.61  (step @p622 :rule implies_elim :premises (@p618))
% 0.39/0.61  (step @p623 :rule cnf_and_neg :args (@t214))
% 0.39/0.61  (step @p624 :rule resolution :premises (@p623 @p622) :args (true @t214))
% 0.39/0.61  (step @p625 :rule eq_resolve :premises (@p624 @p592))
% 0.39/0.61  (step @p626 :rule reordering :premises (@p625) :args ((or @t211 @t210 @t129 @t182)))
% 0.39/0.61  (step @p627 :rule and_elim :premises (@p4) :args (15))
% 0.39/0.61  (step @p628 :rule symm :premises (@p627))
% 0.39/0.61  (step @p629 :rule refl :args (@t215))
% 0.39/0.61  (step @p630 :rule bool-double-not-elim :args (@t216))
% 0.39/0.61  (step @p631 :rule nary_cong :premises (@p368 @p117 @p159 @p630 @p590 @p629) :args ((or @t187 @t138 @t146 (not @t217) @t182 @t215)))
% 0.39/0.61  (assume-push @p1339 @t111)
% 0.39/0.61  (assume-push @p1340 @t137)
% 0.39/0.61  (assume-push @p1341 @t145)
% 0.39/0.61  (assume-push @p1342 @t217)
% 0.39/0.61  (assume-push @p1343 @t180)
% 0.39/0.61  (assume-push @p1344 @t217)
% 0.39/0.61  (assume-push @p1345 @t166)
% 0.39/0.61  (assume-push @p1346 @t218)
% 0.39/0.61  (assume-push @p1347 @t111)
% 0.39/0.61  (step @p641 :rule false_intro :premises (@p628))
% 0.39/0.61  (step @p642 :rule symm :premises (@p1339))
% 0.39/0.61  (step @p643 :rule trans :premises (@p642 @p1346))
% 0.39/0.61  (step @p644 :rule cong :premises (@p1345 @p643) :args (@t117))
% 0.39/0.61  (step @p645 :rule trans :premises (@p644 @p641))
% 0.39/0.61  (step @p646 :rule false_elim :premises (@p645))
% 0.39/0.61  (step-pop @p1348 :rule scope :premises (@p646))
% 0.39/0.61  (step-pop @p1349 :rule scope :premises (@p1348))
% 0.39/0.61  (step-pop @p1350 :rule scope :premises (@p1349))
% 0.39/0.61  (step-pop @p1351 :rule scope :premises (@p1350))
% 0.39/0.61  (step @p647 :rule process_scope :premises (@p1351) :args (@t215))
% 0.39/0.61  (assume-push @p1352 @t180)
% 0.39/0.61  (assume-push @p1353 @t145)
% 0.39/0.61  (step @p654 :rule symm :premises (@p1343))
% 0.39/0.61  (step @p177 :rule refl :args (tptp.e1))
% 0.39/0.61  (step @p655 :rule cong :premises (@p177 @p654) :args (@t86))
% 0.39/0.61  (step @p656 :rule trans :premises (@p154 @p655))
% 0.39/0.61  (step-pop @p1354 :rule scope :premises (@p656))
% 0.39/0.61  (step-pop @p1355 :rule scope :premises (@p1354))
% 0.39/0.61  (step @p657 :rule process_scope :premises (@p1355) :args (@t218))
% 0.39/0.61  (step @p660 :rule and_intro :premises (@p1343 @p154))
% 0.39/0.62  (step @p661 :rule modus_ponens :premises (@p660 @p657))
% 0.39/0.62  (assume-push @p1356 @t180)
% 0.39/0.62  (assume-push @p1357 @t137)
% 0.39/0.62  (step @p664 :rule symm :premises (@p1343))
% 0.39/0.62  (step @p46 :rule refl :args (tptp.e2))
% 0.39/0.62  (step @p665 :rule cong :premises (@p46 @p664) :args (@t85))
% 0.39/0.62  (step @p666 :rule trans :premises (@p112 @p665))
% 0.39/0.62  (step-pop @p1358 :rule scope :premises (@p666))
% 0.39/0.62  (step-pop @p1359 :rule scope :premises (@p1358))
% 0.39/0.62  (step @p667 :rule process_scope :premises (@p1359) :args (@t166))
% 0.39/0.62  (step @p670 :rule and_intro :premises (@p1343 @p112))
% 0.39/0.62  (step @p671 :rule modus_ponens :premises (@p670 @p667))
% 0.39/0.62  (step @p672 :rule and_intro :premises (@p628 @p671 @p661 @p1339))
% 0.39/0.62  (step @p673 :rule modus_ponens :premises (@p672 @p647))
% 0.39/0.62  (step-pop @p1360 :rule scope :premises (@p673))
% 0.39/0.62  (step-pop @p1361 :rule scope :premises (@p1360))
% 0.39/0.62  (step-pop @p1362 :rule scope :premises (@p1361))
% 0.39/0.62  (step-pop @p1363 :rule scope :premises (@p1362))
% 0.39/0.62  (step-pop @p1364 :rule scope :premises (@p1363))
% 0.39/0.62  (step @p674 :rule process_scope :premises (@p1364) :args (@t215))
% 0.39/0.62  (step @p680 :rule implies_elim :premises (@p674))
% 0.39/0.62  (step @p681 :rule cnf_and_neg :args (@t219))
% 0.39/0.62  (step @p682 :rule resolution :premises (@p681 @p680) :args (true @t219))
% 0.39/0.62  (step @p683 :rule eq_resolve :premises (@p682 @p631))
% 0.39/0.62  (step @p684 :rule reordering :premises (@p683) :args ((or @t216 @t187 @t215 @t146 @t138 @t182)))
% 0.39/0.62  (step @p685 :rule cnf_and_pos :args (@t203 2))
% 0.39/0.62  (step @p686 :rule reordering :premises (@p685) :args ((or @t124 @t204)))
% 0.39/0.62  (step @p687 :rule cnf_and_pos :args (@t167 0))
% 0.39/0.62  (step @p688 :rule reordering :premises (@p687) :args ((or @t117 @t168)))
% 0.39/0.62  (step @p689 :rule chain_m_resolution :premises (@p515 @p494 @p688 @p686 @p684 @p628 @p112 @p154 @p626 @p588 @p32 @p493 @p586 @p564 @p154 @p562 @p560 @p535) :args ((or @t185 @t126 @t187) (@list true true true true true false false true true false false true true false true true true) (@list @t173 @t167 @t203 @t117 @t216 @t137 @t145 @t124 @t211 @t128 @t180 @t176 @t208 @t145 @t170 @t169 @t100)))
% 0.39/0.62  (step @p690 :rule and_elim :premises (@p5) :args (1))
% 0.39/0.62  (step @p691 :rule refl :args (@t220))
% 0.39/0.62  (step @p692 :rule bool-double-not-elim :args (@t98))
% 0.39/0.62  (step @p693 :rule nary_cong :premises (@p692 @p117 @p590 @p691) :args ((or (not @t99) @t138 @t182 @t220)))
% 0.39/0.62  (assume-push @p1365 @t99)
% 0.39/0.62  (assume-push @p1366 @t137)
% 0.39/0.62  (assume-push @p1367 @t180)
% 0.39/0.62  (assume-push @p1368 @t99)
% 0.39/0.62  (assume-push @p1369 @t166)
% 0.39/0.62  (step @p699 :rule false_intro :premises (@p690))
% 0.39/0.62  (step @p700 :rule symm :premises (@p1369))
% 0.39/0.62  (step @p86 :rule refl :args (tptp.e0))
% 0.39/0.62  (step @p701 :rule cong :premises (@p86 @p700) :args (@t109))
% 0.39/0.62  (step @p702 :rule trans :premises (@p701 @p699))
% 0.39/0.62  (step @p703 :rule false_elim :premises (@p702))
% 0.39/0.62  (step-pop @p1370 :rule scope :premises (@p703))
% 0.39/0.62  (step-pop @p1371 :rule scope :premises (@p1370))
% 0.39/0.62  (step @p704 :rule process_scope :premises (@p1371) :args (@t220))
% 0.39/0.62  (assume-push @p1372 @t180)
% 0.39/0.62  (assume-push @p1373 @t137)
% 0.39/0.62  (step @p664 :rule symm :premises (@p1367))
% 0.39/0.62  (step @p46 :rule refl :args (tptp.e2))
% 0.39/0.62  (step @p665 :rule cong :premises (@p46 @p664) :args (@t85))
% 0.39/0.62  (step @p666 :rule trans :premises (@p112 @p665))
% 0.39/0.62  (step-pop @p1374 :rule scope :premises (@p666))
% 0.39/0.62  (step-pop @p1375 :rule scope :premises (@p1374))
% 0.39/0.62  (step @p709 :rule process_scope :premises (@p1375) :args (@t166))
% 0.39/0.62  (step @p712 :rule and_intro :premises (@p1367 @p112))
% 0.39/0.62  (step @p713 :rule modus_ponens :premises (@p712 @p709))
% 0.39/0.62  (step @p714 :rule and_intro :premises (@p690 @p713))
% 0.39/0.62  (step @p715 :rule modus_ponens :premises (@p714 @p704))
% 0.39/0.62  (step-pop @p1376 :rule scope :premises (@p715))
% 0.39/0.62  (step-pop @p1377 :rule scope :premises (@p1376))
% 0.39/0.62  (step-pop @p1378 :rule scope :premises (@p1377))
% 0.39/0.62  (step @p716 :rule process_scope :premises (@p1378) :args (@t220))
% 0.39/0.62  (step @p720 :rule implies_elim :premises (@p716))
% 0.39/0.62  (step @p721 :rule cnf_and_neg :args (@t221))
% 0.39/0.62  (step @p722 :rule resolution :premises (@p721 @p720) :args (true @t221))
% 0.39/0.62  (step @p723 :rule eq_resolve :premises (@p722 @p693))
% 0.39/0.62  (step @p724 :rule reordering :premises (@p723) :args ((or @t98 @t220 @t138 @t182)))
% 0.39/0.62  (step @p725 :rule and_elim :premises (@p4) :args (31))
% 0.39/0.62  (step @p726 :rule symm :premises (@p725))
% 0.39/0.62  (step @p727 :rule bool-double-not-elim :args (@t222))
% 0.39/0.62  (step @p728 :rule nary_cong :premises (@p159 @p727 @p590 @p157) :args ((or @t146 (not @t223) @t182 @t143)))
% 0.39/0.62  (assume-push @p1379 @t145)
% 0.39/0.62  (assume-push @p1380 @t223)
% 0.39/0.62  (assume-push @p1381 @t180)
% 0.39/0.62  (assume-push @p1382 @t223)
% 0.39/0.62  (assume-push @p1383 @t218)
% 0.39/0.62  (step @p734 :rule false_intro :premises (@p726))
% 0.39/0.62  (step @p167 :rule refl :args (@t57))
% 0.39/0.62  (step @p735 :rule cong :premises (@p1383 @p167) :args (@t142))
% 0.39/0.62  (step @p736 :rule trans :premises (@p735 @p734))
% 0.39/0.62  (step @p737 :rule false_elim :premises (@p736))
% 0.39/0.62  (step-pop @p1384 :rule scope :premises (@p737))
% 0.39/0.62  (step-pop @p1385 :rule scope :premises (@p1384))
% 0.39/0.62  (step @p738 :rule process_scope :premises (@p1385) :args (@t143))
% 0.39/0.62  (assume-push @p1386 @t180)
% 0.39/0.62  (assume-push @p1387 @t145)
% 0.39/0.62  (step @p654 :rule symm :premises (@p1381))
% 0.39/0.62  (step @p177 :rule refl :args (tptp.e1))
% 0.39/0.62  (step @p655 :rule cong :premises (@p177 @p654) :args (@t86))
% 0.39/0.62  (step @p656 :rule trans :premises (@p154 @p655))
% 0.39/0.62  (step-pop @p1388 :rule scope :premises (@p656))
% 0.39/0.62  (step-pop @p1389 :rule scope :premises (@p1388))
% 0.39/0.62  (step @p743 :rule process_scope :premises (@p1389) :args (@t218))
% 0.39/0.62  (step @p746 :rule and_intro :premises (@p1381 @p154))
% 0.39/0.62  (step @p747 :rule modus_ponens :premises (@p746 @p743))
% 0.39/0.62  (step @p748 :rule and_intro :premises (@p726 @p747))
% 0.39/0.62  (step @p749 :rule modus_ponens :premises (@p748 @p738))
% 0.39/0.62  (step-pop @p1390 :rule scope :premises (@p749))
% 0.39/0.62  (step-pop @p1391 :rule scope :premises (@p1390))
% 0.39/0.62  (step-pop @p1392 :rule scope :premises (@p1391))
% 0.39/0.62  (step @p750 :rule process_scope :premises (@p1392) :args (@t143))
% 0.39/0.62  (step @p754 :rule implies_elim :premises (@p750))
% 0.39/0.62  (step @p755 :rule cnf_and_neg :args (@t224))
% 0.39/0.62  (step @p756 :rule resolution :premises (@p755 @p754) :args (true @t224))
% 0.39/0.62  (step @p757 :rule eq_resolve :premises (@p756 @p728))
% 0.39/0.62  (step @p758 :rule reordering :premises (@p757) :args ((or @t222 @t143 @t146 @t182)))
% 0.39/0.62  (step @p759 :rule and_elim :premises (@p4) :args (36))
% 0.39/0.62  (step @p760 :rule symm :premises (@p759))
% 0.39/0.62  (step @p761 :rule refl :args (@t225))
% 0.39/0.62  (step @p762 :rule bool-double-not-elim :args (@t226))
% 0.39/0.62  (step @p763 :rule nary_cong :premises (@p202 @p762 @p590 @p761) :args ((or @t153 (not @t227) @t182 @t225)))
% 0.39/0.62  (assume-push @p1393 @t152)
% 0.39/0.62  (assume-push @p1394 @t227)
% 0.39/0.62  (assume-push @p1395 @t180)
% 0.39/0.62  (assume-push @p1396 @t227)
% 0.39/0.62  (assume-push @p1397 @t228)
% 0.39/0.62  (step @p769 :rule false_intro :premises (@p760))
% 0.39/0.62  (step @p125 :rule refl :args (@t36))
% 0.39/0.62  (step @p770 :rule cong :premises (@p1397 @p125) :args (@t121))
% 0.39/0.62  (step @p771 :rule trans :premises (@p770 @p769))
% 0.39/0.62  (step @p772 :rule false_elim :premises (@p771))
% 0.39/0.62  (step-pop @p1398 :rule scope :premises (@p772))
% 0.39/0.62  (step-pop @p1399 :rule scope :premises (@p1398))
% 0.39/0.62  (step @p773 :rule process_scope :premises (@p1399) :args (@t225))
% 0.39/0.62  (assume-push @p1400 @t180)
% 0.39/0.62  (assume-push @p1401 @t152)
% 0.39/0.62  (step @p177 :rule refl :args (tptp.e1))
% 0.39/0.62  (step @p778 :rule symm :premises (@p1395))
% 0.39/0.62  (step @p779 :rule cong :premises (@p778 @p177) :args (@t87))
% 0.39/0.62  (step @p780 :rule trans :premises (@p197 @p779))
% 0.39/0.62  (step-pop @p1402 :rule scope :premises (@p780))
% 0.39/0.62  (step-pop @p1403 :rule scope :premises (@p1402))
% 0.39/0.62  (step @p781 :rule process_scope :premises (@p1403) :args (@t228))
% 0.39/0.62  (step @p784 :rule and_intro :premises (@p1395 @p197))
% 0.39/0.62  (step @p785 :rule modus_ponens :premises (@p784 @p781))
% 0.39/0.62  (step @p786 :rule and_intro :premises (@p760 @p785))
% 0.39/0.62  (step @p787 :rule modus_ponens :premises (@p786 @p773))
% 0.39/0.62  (step-pop @p1404 :rule scope :premises (@p787))
% 0.39/0.62  (step-pop @p1405 :rule scope :premises (@p1404))
% 0.39/0.62  (step-pop @p1406 :rule scope :premises (@p1405))
% 0.39/0.62  (step @p788 :rule process_scope :premises (@p1406) :args (@t225))
% 0.39/0.62  (step @p792 :rule implies_elim :premises (@p788))
% 0.39/0.62  (step @p793 :rule cnf_and_neg :args (@t229))
% 0.39/0.62  (step @p794 :rule resolution :premises (@p793 @p792) :args (true @t229))
% 0.39/0.62  (step @p795 :rule eq_resolve :premises (@p794 @p763))
% 0.39/0.62  (step @p796 :rule reordering :premises (@p795) :args ((or @t226 @t225 @t153 @t182)))
% 0.39/0.62  (step @p797 :rule cnf_and_pos :args (@t170 2))
% 0.39/0.62  (step @p798 :rule reordering :premises (@p797) :args ((or @t109 @t171)))
% 0.39/0.62  (step @p799 :rule not_and :premises (@p19))
% 0.39/0.62  (step @p800 :rule chain_m_resolution :premises (@p688 @p799 @p515 @p494 @p525 @p798 @p796 @p760 @p197 @p758 @p726 @p154 @p724 @p690 @p112 @p686 @p626 @p588 @p32) :args ((or @t111 @t182) (@list true false true false true true true false true true false true true false true true true false) (@list @t117 @t167 @t173 @t116 @t170 @t121 @t226 @t152 @t142 @t222 @t145 @t109 @t98 @t137 @t203 @t124 @t211 @t128)))
% 0.39/0.62  (step @p801 :rule and_elim :premises (@p4) :args (2))
% 0.39/0.62  (step @p802 :rule symm :premises (@p801))
% 0.39/0.62  (step @p803 :rule refl :args (@t179))
% 0.39/0.62  (step @p804 :rule bool-double-not-elim :args (@t230))
% 0.39/0.62  (step @p805 :rule nary_cong :premises (@p36 @p804 @p803 @p365) :args ((or @t129 (not @t231) @t179 @t184)))
% 0.39/0.62  (assume-push @p1407 @t128)
% 0.39/0.62  (assume-push @p1408 @t231)
% 0.39/0.62  (assume-push @p1409 @t176)
% 0.39/0.62  (assume-push @p1410 @t231)
% 0.39/0.62  (assume-push @p1411 @t232)
% 0.39/0.62  (step @p811 :rule false_intro :premises (@p802))
% 0.39/0.62  (step @p812 :rule refl :args (@t77))
% 0.39/0.62  (step @p813 :rule cong :premises (@p1411 @p812) :args (@t122))
% 0.39/0.62  (step @p814 :rule trans :premises (@p813 @p811))
% 0.39/0.62  (step @p815 :rule false_elim :premises (@p814))
% 0.39/0.62  (step-pop @p1412 :rule scope :premises (@p815))
% 0.39/0.62  (step-pop @p1413 :rule scope :premises (@p1412))
% 0.39/0.62  (step @p816 :rule process_scope :premises (@p1413) :args (@t184))
% 0.39/0.62  (assume-push @p1414 @t176)
% 0.39/0.62  (assume-push @p1415 @t128)
% 0.39/0.62  (step @p821 :rule symm :premises (@p1409))
% 0.39/0.62  (step @p56 :rule refl :args (tptp.e3))
% 0.39/0.62  (step @p822 :rule cong :premises (@p56 @p821) :args (@t83))
% 0.39/0.62  (step @p823 :rule trans :premises (@p32 @p822))
% 0.39/0.62  (step-pop @p1416 :rule scope :premises (@p823))
% 0.39/0.62  (step-pop @p1417 :rule scope :premises (@p1416))
% 0.39/0.62  (step @p824 :rule process_scope :premises (@p1417) :args (@t232))
% 0.39/0.62  (step @p827 :rule and_intro :premises (@p1409 @p32))
% 0.39/0.62  (step @p828 :rule modus_ponens :premises (@p827 @p824))
% 0.39/0.62  (step @p829 :rule and_intro :premises (@p802 @p828))
% 0.39/0.62  (step @p830 :rule modus_ponens :premises (@p829 @p816))
% 0.39/0.62  (step-pop @p1418 :rule scope :premises (@p830))
% 0.39/0.62  (step-pop @p1419 :rule scope :premises (@p1418))
% 0.39/0.62  (step-pop @p1420 :rule scope :premises (@p1419))
% 0.39/0.62  (step @p831 :rule process_scope :premises (@p1420) :args (@t184))
% 0.39/0.62  (step @p835 :rule implies_elim :premises (@p831))
% 0.39/0.62  (step @p836 :rule cnf_and_neg :args (@t233))
% 0.39/0.62  (step @p837 :rule resolution :premises (@p836 @p835) :args (true @t233))
% 0.39/0.62  (step @p838 :rule eq_resolve :premises (@p837 @p805))
% 0.39/0.62  (step @p839 :rule reordering :premises (@p838) :args ((or @t230 @t184 @t129 @t179)))
% 0.39/0.62  (step @p840 :rule and_elim :premises (@p4) :args (1))
% 0.39/0.62  (step @p841 :rule symm :premises (@p840))
% 0.39/0.62  (step @p842 :rule bool-double-not-elim :args (@t234))
% 0.39/0.62  (step @p843 :rule nary_cong :premises (@p117 @p842 @p803 @p629) :args ((or @t138 (not @t235) @t179 @t215)))
% 0.39/0.62  (assume-push @p1421 @t137)
% 0.39/0.62  (assume-push @p1422 @t235)
% 0.39/0.62  (assume-push @p1423 @t176)
% 0.39/0.62  (assume-push @p1424 @t235)
% 0.39/0.62  (assume-push @p1425 @t134)
% 0.39/0.62  (step @p849 :rule false_intro :premises (@p841))
% 0.39/0.62  (step @p812 :rule refl :args (@t77))
% 0.39/0.62  (step @p850 :rule cong :premises (@p1425 @p812) :args (@t117))
% 0.39/0.62  (step @p851 :rule trans :premises (@p850 @p849))
% 0.39/0.62  (step @p852 :rule false_elim :premises (@p851))
% 0.39/0.62  (step-pop @p1426 :rule scope :premises (@p852))
% 0.39/0.62  (step-pop @p1427 :rule scope :premises (@p1426))
% 0.39/0.62  (step @p853 :rule process_scope :premises (@p1427) :args (@t215))
% 0.39/0.62  (assume-push @p1428 @t176)
% 0.39/0.62  (assume-push @p1429 @t137)
% 0.39/0.62  (step @p858 :rule symm :premises (@p1423))
% 0.39/0.62  (step @p46 :rule refl :args (tptp.e2))
% 0.39/0.62  (step @p859 :rule cong :premises (@p46 @p858) :args (@t85))
% 0.39/0.62  (step @p860 :rule trans :premises (@p112 @p859))
% 0.39/0.62  (step-pop @p1430 :rule scope :premises (@p860))
% 0.39/0.62  (step-pop @p1431 :rule scope :premises (@p1430))
% 0.39/0.62  (step @p861 :rule process_scope :premises (@p1431) :args (@t134))
% 0.39/0.62  (step @p864 :rule and_intro :premises (@p1423 @p112))
% 0.39/0.62  (step @p865 :rule modus_ponens :premises (@p864 @p861))
% 0.39/0.62  (step @p866 :rule and_intro :premises (@p841 @p865))
% 0.39/0.62  (step @p867 :rule modus_ponens :premises (@p866 @p853))
% 0.39/0.62  (step-pop @p1432 :rule scope :premises (@p867))
% 0.39/0.62  (step-pop @p1433 :rule scope :premises (@p1432))
% 0.39/0.62  (step-pop @p1434 :rule scope :premises (@p1433))
% 0.39/0.62  (step @p868 :rule process_scope :premises (@p1434) :args (@t215))
% 0.39/0.62  (step @p872 :rule implies_elim :premises (@p868))
% 0.39/0.62  (step @p873 :rule cnf_and_neg :args (@t236))
% 0.39/0.62  (step @p874 :rule resolution :premises (@p873 @p872) :args (true @t236))
% 0.39/0.62  (step @p875 :rule eq_resolve :premises (@p874 @p843))
% 0.39/0.62  (step @p876 :rule reordering :premises (@p875) :args ((or @t234 @t215 @t138 @t179)))
% 0.39/0.62  (step @p877 :rule and_elim :premises (@p4) :args (4))
% 0.39/0.62  (step @p878 :rule symm :premises (@p877))
% 0.39/0.62  (step @p879 :rule bool-double-not-elim :args (@t237))
% 0.39/0.62  (step @p880 :rule nary_cong :premises (@p36 @p159 @p202 @p879 @p803 @p399) :args ((or @t129 @t146 @t153 (not @t238) @t179 @t190)))
% 0.39/0.62  (assume-push @p1435 @t128)
% 0.39/0.62  (assume-push @p1436 @t145)
% 0.39/0.62  (assume-push @p1437 @t152)
% 0.39/0.62  (assume-push @p1438 @t238)
% 0.39/0.62  (assume-push @p1439 @t176)
% 0.39/0.62  (assume-push @p1440 @t238)
% 0.39/0.62  (assume-push @p1441 @t232)
% 0.39/0.62  (assume-push @p1442 @t142)
% 0.39/0.62  (assume-push @p1443 @t239)
% 0.39/0.62  (step @p890 :rule false_intro :premises (@p878))
% 0.39/0.62  (step @p891 :rule symm :premises (@p1443))
% 0.39/0.62  (step @p892 :rule trans :premises (@p891 @p1442))
% 0.39/0.62  (step @p893 :rule cong :premises (@p1441 @p892) :args (@t119))
% 0.39/0.62  (step @p894 :rule trans :premises (@p893 @p890))
% 0.39/0.62  (step @p895 :rule false_elim :premises (@p894))
% 0.39/0.62  (step-pop @p1444 :rule scope :premises (@p895))
% 0.39/0.62  (step-pop @p1445 :rule scope :premises (@p1444))
% 0.39/0.62  (step-pop @p1446 :rule scope :premises (@p1445))
% 0.39/0.62  (step-pop @p1447 :rule scope :premises (@p1446))
% 0.39/0.62  (step @p896 :rule process_scope :premises (@p1447) :args (@t190))
% 0.39/0.62  (assume-push @p1448 @t176)
% 0.39/0.62  (assume-push @p1449 @t152)
% 0.39/0.62  (step @p177 :rule refl :args (tptp.e1))
% 0.39/0.62  (step @p903 :rule symm :premises (@p1439))
% 0.39/0.62  (step @p904 :rule cong :premises (@p903 @p177) :args (@t87))
% 0.39/0.62  (step @p905 :rule trans :premises (@p197 @p904))
% 0.39/0.62  (step-pop @p1450 :rule scope :premises (@p905))
% 0.39/0.62  (step-pop @p1451 :rule scope :premises (@p1450))
% 0.39/0.62  (step @p906 :rule process_scope :premises (@p1451) :args (@t239))
% 0.39/0.62  (step @p909 :rule and_intro :premises (@p1439 @p197))
% 0.39/0.62  (step @p910 :rule modus_ponens :premises (@p909 @p906))
% 0.39/0.62  (assume-push @p1452 @t176)
% 0.39/0.62  (assume-push @p1453 @t145)
% 0.39/0.62  (step @p913 :rule symm :premises (@p1439))
% 0.39/0.62  (step @p177 :rule refl :args (tptp.e1))
% 0.39/0.62  (step @p914 :rule cong :premises (@p177 @p913) :args (@t86))
% 0.39/0.62  (step @p915 :rule trans :premises (@p154 @p914))
% 0.39/0.62  (step-pop @p1454 :rule scope :premises (@p915))
% 0.39/0.62  (step-pop @p1455 :rule scope :premises (@p1454))
% 0.39/0.62  (step @p916 :rule process_scope :premises (@p1455) :args (@t142))
% 0.39/0.62  (step @p919 :rule and_intro :premises (@p1439 @p154))
% 0.39/0.62  (step @p920 :rule modus_ponens :premises (@p919 @p916))
% 0.39/0.62  (assume-push @p1456 @t176)
% 0.39/0.62  (assume-push @p1457 @t128)
% 0.39/0.62  (step @p821 :rule symm :premises (@p1439))
% 0.39/0.62  (step @p56 :rule refl :args (tptp.e3))
% 0.39/0.62  (step @p822 :rule cong :premises (@p56 @p821) :args (@t83))
% 0.39/0.62  (step @p823 :rule trans :premises (@p32 @p822))
% 0.39/0.62  (step-pop @p1458 :rule scope :premises (@p823))
% 0.39/0.62  (step-pop @p1459 :rule scope :premises (@p1458))
% 0.39/0.62  (step @p923 :rule process_scope :premises (@p1459) :args (@t232))
% 0.39/0.62  (step @p926 :rule and_intro :premises (@p1439 @p32))
% 0.39/0.62  (step @p927 :rule modus_ponens :premises (@p926 @p923))
% 0.39/0.62  (step @p928 :rule and_intro :premises (@p878 @p927 @p920 @p910))
% 0.39/0.62  (step @p929 :rule modus_ponens :premises (@p928 @p896))
% 0.39/0.62  (step-pop @p1460 :rule scope :premises (@p929))
% 0.39/0.62  (step-pop @p1461 :rule scope :premises (@p1460))
% 0.39/0.62  (step-pop @p1462 :rule scope :premises (@p1461))
% 0.39/0.62  (step-pop @p1463 :rule scope :premises (@p1462))
% 0.39/0.62  (step-pop @p1464 :rule scope :premises (@p1463))
% 0.39/0.62  (step @p930 :rule process_scope :premises (@p1464) :args (@t190))
% 0.39/0.62  (step @p936 :rule implies_elim :premises (@p930))
% 0.39/0.62  (step @p937 :rule cnf_and_neg :args (@t240))
% 0.39/0.62  (step @p938 :rule resolution :premises (@p937 @p936) :args (true @t240))
% 0.39/0.62  (step @p939 :rule eq_resolve :premises (@p938 @p880))
% 0.39/0.62  (step @p940 :rule reordering :premises (@p939) :args ((or @t237 @t190 @t153 @t146 @t129 @t179)))
% 0.39/0.62  (step @p941 :rule cnf_and_pos :args (@t170 1))
% 0.39/0.62  (step @p942 :rule reordering :premises (@p941) :args ((or @t107 @t171)))
% 0.39/0.62  (step @p943 :rule not_and :premises (@p8))
% 0.39/0.62  (step @p944 :rule refl :args (@t241))
% 0.39/0.62  (step @p945 :rule refl :args (@t242))
% 0.39/0.62  (step @p946 :rule nary_cong :premises (@p945 @p803 @p366 @p944) :args ((or @t242 @t179 @t188 @t241)))
% 0.39/0.62  (assume-push @p1465 @t107)
% 0.39/0.62  (assume-push @p1466 @t176)
% 0.39/0.62  (assume-push @p1467 @t127)
% 0.39/0.62  (assume-push @p1468 @t127)
% 0.39/0.62  (assume-push @p1469 @t176)
% 0.39/0.62  (assume-push @p1470 @t107)
% 0.39/0.62  (step @p953 :rule false_intro :premises (@p1467))
% 0.39/0.62  (step @p954 :rule symm :premises (@p1465))
% 0.39/0.62  (step @p955 :rule trans :premises (@p954 @p1466))
% 0.39/0.62  (step @p56 :rule refl :args (tptp.e3))
% 0.39/0.62  (step @p956 :rule cong :premises (@p56 @p955) :args (@t123))
% 0.39/0.62  (step @p957 :rule trans :premises (@p956 @p953))
% 0.39/0.62  (step @p958 :rule false_elim :premises (@p957))
% 0.39/0.62  (step-pop @p1471 :rule scope :premises (@p958))
% 0.39/0.62  (step-pop @p1472 :rule scope :premises (@p1471))
% 0.39/0.62  (step-pop @p1473 :rule scope :premises (@p1472))
% 0.39/0.62  (step @p959 :rule process_scope :premises (@p1473) :args (@t241))
% 0.39/0.62  (step @p963 :rule and_intro :premises (@p1467 @p1466 @p1465))
% 0.39/0.62  (step @p964 :rule modus_ponens :premises (@p963 @p959))
% 0.39/0.62  (step-pop @p1474 :rule scope :premises (@p964))
% 0.39/0.62  (step-pop @p1475 :rule scope :premises (@p1474))
% 0.39/0.62  (step-pop @p1476 :rule scope :premises (@p1475))
% 0.39/0.62  (step @p965 :rule process_scope :premises (@p1476) :args (@t241))
% 0.39/0.62  (step @p969 :rule implies_elim :premises (@p965))
% 0.39/0.62  (step @p970 :rule cnf_and_neg :args (@t243))
% 0.39/0.62  (step @p971 :rule resolution :premises (@p970 @p969) :args (true @t243))
% 0.39/0.62  (step @p972 :rule eq_resolve :premises (@p971 @p946))
% 0.39/0.62  (step @p973 :rule reordering :premises (@p972) :args ((or @t126 @t242 @t241 @t179)))
% 0.39/0.62  (step @p974 :rule eq-symm :args (@t11 tptp.e3))
% 0.39/0.62  (step @p975 :rule eq-symm :args (@t31 tptp.e3))
% 0.39/0.62  (step @p976 :rule nary_cong :premises (@p480 @p497 @p975 @p974) :args (@t89))
% 0.39/0.62  (step @p977 :rule and_elim :premises (@p3) :args (15))
% 0.39/0.62  (step @p978 :rule eq_resolve :premises (@p977 @p976))
% 0.39/0.62  (step @p979 :rule reordering :premises (@p978) :args ((or @t108 @t119 @t123 @t193)))
% 0.39/0.62  (step @p980 :rule refl :args (@t244))
% 0.39/0.62  (step @p981 :rule nary_cong :premises (@p36 @p442 @p201 @p980 @p803) :args ((or @t129 @t199 @t155 @t244 @t179)))
% 0.39/0.62  (assume-push @p1477 @t198)
% 0.39/0.62  (assume-push @p1478 @t193)
% 0.39/0.62  (assume-push @p1479 @t232)
% 0.39/0.62  (assume-push @p1480 @t154)
% 0.39/0.62  (step @p986 :rule evaluate :args ((= false true)))
% 0.39/0.62  (step @p987 :rule symm :premises (@p1479))
% 0.39/0.62  (step @p988 :rule trans :premises (@p987 @p437))
% 0.39/0.62  (step @p989 :rule symm :premises (@p988))
% 0.39/0.62  (step @p990 :rule symm :premises (@p1478))
% 0.39/0.62  (step @p991 :rule trans :premises (@p990 @p437 @p989))
% 0.39/0.62  (step @p992 :rule true_intro :premises (@p991))
% 0.39/0.62  (step @p209 :rule false_intro :premises (@p199))
% 0.39/0.62  (step @p993 :rule symm :premises (@p209))
% 0.39/0.62  (step @p994 :rule trans :premises (@p993 @p992))
% 0.39/0.62  (step @p995 false :rule eq_resolve :premises (@p994 @p986))
% 0.39/0.62  (step-pop @p1481 :rule scope :premises (@p995))
% 0.39/0.62  (step-pop @p1482 :rule scope :premises (@p1481))
% 0.39/0.62  (step-pop @p1483 :rule scope :premises (@p1482))
% 0.39/0.62  (step-pop @p1484 :rule scope :premises (@p1483))
% 0.39/0.62  (step @p996 :rule process_scope :premises (@p1484) :args (false))
% 0.39/0.62  (assume-push @p1485 @t128)
% 0.39/0.62  (assume-push @p1486 @t198)
% 0.39/0.62  (assume-push @p1487 @t154)
% 0.39/0.62  (assume-push @p1488 @t193)
% 0.39/0.62  (assume-push @p1489 @t176)
% 0.39/0.62  (assume-push @p1490 @t176)
% 0.39/0.62  (assume-push @p1491 @t128)
% 0.39/0.62  (step @p821 :rule symm :premises (@p1489))
% 0.39/0.62  (step @p56 :rule refl :args (tptp.e3))
% 0.39/0.62  (step @p822 :rule cong :premises (@p56 @p821) :args (@t83))
% 0.39/0.62  (step @p823 :rule trans :premises (@p32 @p822))
% 0.39/0.62  (step-pop @p1492 :rule scope :premises (@p823))
% 0.39/0.62  (step-pop @p1493 :rule scope :premises (@p1492))
% 0.39/0.62  (step @p1008 :rule process_scope :premises (@p1493) :args (@t232))
% 0.39/0.62  (step @p1011 :rule and_intro :premises (@p1489 @p32))
% 0.39/0.62  (step @p1012 :rule modus_ponens :premises (@p1011 @p1008))
% 0.39/0.62  (step @p1013 :rule and_intro :premises (@p437 @p1488 @p1012 @p199))
% 0.39/0.62  (step-pop @p1494 :rule scope :premises (@p1013))
% 0.39/0.62  (step-pop @p1495 :rule scope :premises (@p1494))
% 0.39/0.62  (step-pop @p1496 :rule scope :premises (@p1495))
% 0.39/0.62  (step-pop @p1497 :rule scope :premises (@p1496))
% 0.39/0.62  (step-pop @p1498 :rule scope :premises (@p1497))
% 0.39/0.62  (step @p1014 :rule process_scope :premises (@p1498) :args (@t245))
% 0.39/0.62  (step @p1020 :rule implies_elim :premises (@p1014))
% 0.39/0.62  (step @p1021 :rule resolution :premises (@p1020 @p996) :args (true @t245))
% 0.39/0.62  (step @p1022 :rule not_and :premises (@p1021))
% 0.39/0.62  (step @p1023 :rule eq_resolve :premises (@p1022 @p981))
% 0.39/0.62  (step @p1024 :rule reordering :premises (@p1023) :args ((or @t151 @t244 @t199 @t129 @t179)))
% 0.39/0.62  (step @p1025 :rule chain_m_resolution :premises (@p1024 @p199 @p32 @p437 @p979 @p973 @p943 @p942 @p515 @p494 @p688 @p517 @p940 @p878 @p32 @p154 @p197 @p876 @p841 @p112 @p839 @p802 @p32 @p493 @p800 @p689) :args ((or @t185 @t126) (@list true false false false true true false false true true true true true false false false true true false true true false false true true) (@list @t151 @t128 @t198 @t193 @t123 @t108 @t107 @t170 @t173 @t167 @t203 @t119 @t237 @t128 @t145 @t152 @t117 @t234 @t137 @t122 @t230 @t128 @t176 @t180 @t111)))
% 0.39/0.62  (step @p1026 :rule chain_m_resolution :premises (@p1025 @p534) :args (@t185 @t246 (@list @t126)))
% 0.39/0.62  (step @p1027 :rule and_elim :premises (@p4) :args (9))
% 0.39/0.62  (step @p1028 :rule symm :premises (@p1027))
% 0.39/0.62  (step @p1029 :rule refl :args (@t247))
% 0.39/0.62  (step @p1030 :rule bool-double-not-elim :args (@t248))
% 0.39/0.62  (step @p1031 :rule nary_cong :premises (@p117 @p1030 @p367 @p1029) :args ((or @t138 (not @t249) @t186 @t247)))
% 0.39/0.62  (assume-push @p1499 @t137)
% 0.39/0.62  (assume-push @p1500 @t249)
% 0.39/0.62  (assume-push @p1501 @t185)
% 0.39/0.62  (assume-push @p1502 @t249)
% 0.39/0.62  (assume-push @p1503 @t250)
% 0.39/0.62  (step @p1037 :rule false_intro :premises (@p1028))
% 0.39/0.62  (step @p1038 :rule refl :args (@t52))
% 0.39/0.62  (step @p1039 :rule cong :premises (@p1503 @p1038) :args (@t118))
% 0.39/0.62  (step @p1040 :rule trans :premises (@p1039 @p1037))
% 0.39/0.62  (step @p1041 :rule false_elim :premises (@p1040))
% 0.39/0.62  (step-pop @p1504 :rule scope :premises (@p1041))
% 0.39/0.62  (step-pop @p1505 :rule scope :premises (@p1504))
% 0.39/0.62  (step @p1042 :rule process_scope :premises (@p1505) :args (@t247))
% 0.39/0.62  (assume-push @p1506 @t185)
% 0.39/0.62  (assume-push @p1507 @t137)
% 0.39/0.62  (step @p1047 :rule symm :premises (@p1501))
% 0.39/0.62  (step @p46 :rule refl :args (tptp.e2))
% 0.39/0.62  (step @p1048 :rule cong :premises (@p46 @p1047) :args (@t85))
% 0.39/0.62  (step @p1049 :rule trans :premises (@p112 @p1048))
% 0.39/0.62  (step-pop @p1508 :rule scope :premises (@p1049))
% 0.39/0.62  (step-pop @p1509 :rule scope :premises (@p1508))
% 0.39/0.62  (step @p1050 :rule process_scope :premises (@p1509) :args (@t250))
% 0.39/0.62  (step @p1053 :rule and_intro :premises (@p1501 @p112))
% 0.39/0.62  (step @p1054 :rule modus_ponens :premises (@p1053 @p1050))
% 0.39/0.62  (step @p1055 :rule and_intro :premises (@p1028 @p1054))
% 0.39/0.62  (step @p1056 :rule modus_ponens :premises (@p1055 @p1042))
% 0.39/0.62  (step-pop @p1510 :rule scope :premises (@p1056))
% 0.39/0.62  (step-pop @p1511 :rule scope :premises (@p1510))
% 0.39/0.62  (step-pop @p1512 :rule scope :premises (@p1511))
% 0.39/0.62  (step @p1057 :rule process_scope :premises (@p1512) :args (@t247))
% 0.39/0.62  (step @p1061 :rule implies_elim :premises (@p1057))
% 0.39/0.62  (step @p1062 :rule cnf_and_neg :args (@t251))
% 0.39/0.62  (step @p1063 :rule resolution :premises (@p1062 @p1061) :args (true @t251))
% 0.39/0.62  (step @p1064 :rule eq_resolve :premises (@p1063 @p1031))
% 0.39/0.62  (step @p1065 :rule reordering :premises (@p1064) :args ((or @t248 @t247 @t138 @t186)))
% 0.39/0.62  (step @p1066 :rule chain_m_resolution :premises (@p1065 @p1028 @p112 @p1026) :args (@t247 @t252 (@list @t248 @t137 @t185)))
% 0.39/0.62  (step @p1067 :rule cnf_and_pos :args (@t167 1))
% 0.39/0.62  (step @p1068 :rule reordering :premises (@p1067) :args ((or @t118 @t168)))
% 0.39/0.62  (step @p1069 :rule chain_m_resolution :premises (@p1068 @p1066) :args (@t168 @t246 (@list @t118)))
% 0.39/0.62  (step @p1070 :rule and_elim :premises (@p4) :args (10))
% 0.39/0.62  (step @p1071 :rule symm :premises (@p1070))
% 0.39/0.62  (step @p1072 :rule bool-double-not-elim :args (@t253))
% 0.39/0.62  (step @p1073 :rule nary_cong :premises (@p36 @p1072 @p367 @p944) :args ((or @t129 (not @t254) @t186 @t241)))
% 0.39/0.62  (assume-push @p1513 @t128)
% 0.39/0.62  (assume-push @p1514 @t254)
% 0.39/0.62  (assume-push @p1515 @t185)
% 0.39/0.62  (assume-push @p1516 @t254)
% 0.39/0.62  (assume-push @p1517 @t193)
% 0.39/0.62  (step @p1079 :rule false_intro :premises (@p1071))
% 0.39/0.62  (step @p1038 :rule refl :args (@t52))
% 0.39/0.62  (step @p1080 :rule cong :premises (@p1517 @p1038) :args (@t123))
% 0.39/0.62  (step @p1081 :rule trans :premises (@p1080 @p1079))
% 0.39/0.62  (step @p1082 :rule false_elim :premises (@p1081))
% 0.39/0.62  (step-pop @p1518 :rule scope :premises (@p1082))
% 0.39/0.62  (step-pop @p1519 :rule scope :premises (@p1518))
% 0.39/0.62  (step @p1083 :rule process_scope :premises (@p1519) :args (@t241))
% 0.39/0.62  (assume-push @p1520 @t185)
% 0.39/0.62  (assume-push @p1521 @t128)
% 0.39/0.62  (step @p417 :rule symm :premises (@p1515))
% 0.39/0.62  (step @p56 :rule refl :args (tptp.e3))
% 0.39/0.62  (step @p418 :rule cong :premises (@p56 @p417) :args (@t83))
% 0.39/0.62  (step @p419 :rule trans :premises (@p32 @p418))
% 0.39/0.62  (step-pop @p1522 :rule scope :premises (@p419))
% 0.39/0.62  (step-pop @p1523 :rule scope :premises (@p1522))
% 0.39/0.62  (step @p1088 :rule process_scope :premises (@p1523) :args (@t193))
% 0.39/0.62  (step @p1091 :rule and_intro :premises (@p1515 @p32))
% 0.39/0.62  (step @p1092 :rule modus_ponens :premises (@p1091 @p1088))
% 0.39/0.62  (step @p1093 :rule and_intro :premises (@p1071 @p1092))
% 0.39/0.62  (step @p1094 :rule modus_ponens :premises (@p1093 @p1083))
% 0.39/0.62  (step-pop @p1524 :rule scope :premises (@p1094))
% 0.39/0.62  (step-pop @p1525 :rule scope :premises (@p1524))
% 0.39/0.62  (step-pop @p1526 :rule scope :premises (@p1525))
% 0.39/0.62  (step @p1095 :rule process_scope :premises (@p1526) :args (@t241))
% 0.39/0.62  (step @p1099 :rule implies_elim :premises (@p1095))
% 0.39/0.62  (step @p1100 :rule cnf_and_neg :args (@t255))
% 0.39/0.62  (step @p1101 :rule resolution :premises (@p1100 @p1099) :args (true @t255))
% 0.39/0.62  (step @p1102 :rule eq_resolve :premises (@p1101 @p1073))
% 0.39/0.62  (step @p1103 :rule reordering :premises (@p1102) :args ((or @t253 @t241 @t129 @t186)))
% 0.39/0.62  (step @p1104 :rule chain_m_resolution :premises (@p1103 @p1071 @p32 @p1026) :args (@t241 @t252 (@list @t253 @t128 @t185)))
% 0.39/0.62  (step @p1105 :rule cnf_and_pos :args (@t203 1))
% 0.39/0.62  (step @p1106 :rule reordering :premises (@p1105) :args ((or @t123 @t204)))
% 0.39/0.62  (step @p1107 :rule chain_m_resolution :premises (@p1106 @p1104) :args (@t204 @t246 (@list @t123)))
% 0.39/0.62  (step @p1108 :rule nary_cong :premises (@p537 @p159 @p367 @p945) :args ((or @t206 @t146 @t186 @t242)))
% 0.39/0.62  (assume-push @p1527 @t101)
% 0.39/0.62  (assume-push @p1528 @t145)
% 0.39/0.62  (assume-push @p1529 @t185)
% 0.39/0.62  (assume-push @p1530 @t101)
% 0.39/0.62  (assume-push @p1531 @t172)
% 0.39/0.62  (step @p543 :rule false_intro :premises (@p535))
% 0.39/0.62  (step @p1114 :rule symm :premises (@p1531))
% 0.39/0.62  (step @p86 :rule refl :args (tptp.e0))
% 0.39/0.62  (step @p1115 :rule cong :premises (@p86 @p1114) :args (@t107))
% 0.39/0.62  (step @p1116 :rule trans :premises (@p1115 @p543))
% 0.39/0.62  (step @p1117 :rule false_elim :premises (@p1116))
% 0.39/0.62  (step-pop @p1532 :rule scope :premises (@p1117))
% 0.39/0.62  (step-pop @p1533 :rule scope :premises (@p1532))
% 0.39/0.62  (step @p1118 :rule process_scope :premises (@p1533) :args (@t242))
% 0.39/0.62  (assume-push @p1534 @t185)
% 0.39/0.62  (assume-push @p1535 @t145)
% 0.39/0.62  (step @p1123 :rule symm :premises (@p1529))
% 0.39/0.62  (step @p177 :rule refl :args (tptp.e1))
% 0.39/0.62  (step @p1124 :rule cong :premises (@p177 @p1123) :args (@t86))
% 0.39/0.62  (step @p1125 :rule trans :premises (@p154 @p1124))
% 0.39/0.62  (step-pop @p1536 :rule scope :premises (@p1125))
% 0.39/0.62  (step-pop @p1537 :rule scope :premises (@p1536))
% 0.39/0.62  (step @p1126 :rule process_scope :premises (@p1537) :args (@t172))
% 0.39/0.62  (step @p1129 :rule and_intro :premises (@p1529 @p154))
% 0.39/0.62  (step @p1130 :rule modus_ponens :premises (@p1129 @p1126))
% 0.39/0.62  (step @p1131 :rule and_intro :premises (@p535 @p1130))
% 0.39/0.62  (step @p1132 :rule modus_ponens :premises (@p1131 @p1118))
% 0.39/0.62  (step-pop @p1538 :rule scope :premises (@p1132))
% 0.39/0.62  (step-pop @p1539 :rule scope :premises (@p1538))
% 0.39/0.62  (step-pop @p1540 :rule scope :premises (@p1539))
% 0.39/0.62  (step @p1133 :rule process_scope :premises (@p1540) :args (@t242))
% 0.39/0.62  (step @p1137 :rule implies_elim :premises (@p1133))
% 0.39/0.62  (step @p1138 :rule cnf_and_neg :args (@t256))
% 0.39/0.62  (step @p1139 :rule resolution :premises (@p1138 @p1137) :args (true @t256))
% 0.39/0.62  (step @p1140 :rule eq_resolve :premises (@p1139 @p1108))
% 0.39/0.62  (step @p1141 :rule reordering :premises (@p1140) :args ((or @t100 @t242 @t146 @t186)))
% 0.39/0.62  (step @p1142 :rule chain_m_resolution :premises (@p1141 @p535 @p154 @p1026) :args (@t242 @t252 (@list @t100 @t145 @t185)))
% 0.39/0.62  (step @p1143 :rule chain_m_resolution :premises (@p942 @p1142) :args (@t171 @t246 (@list @t107)))
% 0.39/0.62  (step @p1144 false :rule chain_m_resolution :premises (@p515 @p1143 @p1107 @p494 @p1069) :args (false (@list true true true true) (@list @t170 @t203 @t173 @t167)))
% 0.39/0.62  )
% 0.39/0.62  % SZS output end Proof
% 0.39/0.62  % cvc5 exiting
%------------------------------------------------------------------------------