cvc5---1.3.4.THM-Prf.s

%------------------------------------------------------------------------------
% File     : cvc5---1.3.4
% Problem  : ALG095+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 : n013.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:12 AM UTC 2026

% Result   : Theorem 0.47s 0.64s
% Output   : Proof 0.47s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12  % Problem  : ALG095+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.18/0.34  % Computer : n013.cluster.edu
% 0.18/0.34  % Model    : x86_64 x86_64
% 0.18/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.34  % Memory   : 8042.1875MB
% 0.18/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.18/0.35  % CPULimit : 300
% 0.18/0.35  % WCLimit  : 300
% 0.18/0.35  % DateTime : Wed Jun  3 01:39:15 EDT 2026
% 0.18/0.35  % CPUTime  : 
% 0.33/0.52  %----Proving TF0_NAR, FOF, or CNF
% 0.47/0.64  --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15...
% 0.47/0.64  % SZS status Theorem
% 0.47/0.64  % SZS output start Proof
% 0.47/0.64  (
% 0.47/0.64  (declare-sort $$unsorted 0)
% 0.47/0.64  (declare-const tptp.unit $$unsorted)
% 0.47/0.64  (declare-const tptp.op (-> $$unsorted $$unsorted $$unsorted))
% 0.47/0.64  (declare-const tptp.e0 $$unsorted)
% 0.47/0.64  (declare-const tptp.e1 $$unsorted)
% 0.47/0.64  (declare-const tptp.e2 $$unsorted)
% 0.47/0.64  (declare-const tptp.e3 $$unsorted)
% 0.47/0.64  (declare-const tptp.e4 $$unsorted)
% 0.47/0.64  (define @t1 () (tptp.op tptp.e4 tptp.e4))
% 0.47/0.64  (define @t2 () (= @t1 tptp.e0))
% 0.47/0.64  (define @t3 () (tptp.op tptp.e4 tptp.e3))
% 0.47/0.64  (define @t4 () (= @t3 tptp.e2))
% 0.47/0.64  (define @t5 () (tptp.op tptp.e4 tptp.e2))
% 0.47/0.64  (define @t6 () (= @t5 tptp.e1))
% 0.47/0.64  (define @t7 () (tptp.op tptp.e4 tptp.e1))
% 0.47/0.64  (define @t8 () (= @t7 tptp.e3))
% 0.47/0.64  (define @t9 () (tptp.op tptp.e4 tptp.e0))
% 0.47/0.64  (define @t10 () (= @t9 tptp.e4))
% 0.47/0.64  (define @t11 () (tptp.op tptp.e3 tptp.e4))
% 0.47/0.64  (define @t12 () (= @t11 tptp.e2))
% 0.47/0.64  (define @t13 () (tptp.op tptp.e3 tptp.e3))
% 0.47/0.64  (define @t14 () (= @t13 tptp.e1))
% 0.47/0.64  (define @t15 () (tptp.op tptp.e3 tptp.e2))
% 0.47/0.64  (define @t16 () (= @t15 tptp.e0))
% 0.47/0.64  (define @t17 () (tptp.op tptp.e3 tptp.e1))
% 0.47/0.64  (define @t18 () (= @t17 tptp.e4))
% 0.47/0.64  (define @t19 () (tptp.op tptp.e3 tptp.e0))
% 0.47/0.64  (define @t20 () (= @t19 tptp.e3))
% 0.47/0.64  (define @t21 () (tptp.op tptp.e2 tptp.e4))
% 0.47/0.64  (define @t22 () (= @t21 tptp.e1))
% 0.47/0.64  (define @t23 () (tptp.op tptp.e2 tptp.e3))
% 0.47/0.64  (define @t24 () (= @t23 tptp.e4))
% 0.47/0.64  (define @t25 () (tptp.op tptp.e2 tptp.e2))
% 0.47/0.64  (define @t26 () (= @t25 tptp.e3))
% 0.47/0.64  (define @t27 () (tptp.op tptp.e2 tptp.e1))
% 0.47/0.64  (define @t28 () (= @t27 tptp.e0))
% 0.47/0.64  (define @t29 () (tptp.op tptp.e2 tptp.e0))
% 0.47/0.64  (define @t30 () (= @t29 tptp.e2))
% 0.47/0.64  (define @t31 () (tptp.op tptp.e1 tptp.e4))
% 0.47/0.64  (define @t32 () (= @t31 tptp.e3))
% 0.47/0.64  (define @t33 () (tptp.op tptp.e1 tptp.e3))
% 0.47/0.64  (define @t34 () (= @t33 tptp.e0))
% 0.47/0.64  (define @t35 () (tptp.op tptp.e1 tptp.e2))
% 0.47/0.64  (define @t36 () (= @t35 tptp.e4))
% 0.47/0.64  (define @t37 () (tptp.op tptp.e1 tptp.e1))
% 0.47/0.64  (define @t38 () (= @t37 tptp.e2))
% 0.47/0.64  (define @t39 () (tptp.op tptp.e1 tptp.e0))
% 0.47/0.64  (define @t40 () (= @t39 tptp.e1))
% 0.47/0.64  (define @t41 () (tptp.op tptp.e0 tptp.e4))
% 0.47/0.64  (define @t42 () (= @t41 tptp.e4))
% 0.47/0.64  (define @t43 () (tptp.op tptp.e0 tptp.e3))
% 0.47/0.64  (define @t44 () (= @t43 tptp.e3))
% 0.47/0.64  (define @t45 () (tptp.op tptp.e0 tptp.e2))
% 0.47/0.64  (define @t46 () (= @t45 tptp.e2))
% 0.47/0.64  (define @t47 () (tptp.op tptp.e0 tptp.e1))
% 0.47/0.64  (define @t48 () (= @t47 tptp.e1))
% 0.47/0.64  (define @t49 () (tptp.op tptp.e0 tptp.e0))
% 0.47/0.64  (define @t50 () (= @t49 tptp.e0))
% 0.47/0.64  (define @t51 () (= tptp.unit tptp.e0))
% 0.47/0.64  (define @t52 () (= @t1 tptp.e4))
% 0.47/0.64  (define @t53 () (= @t11 tptp.e4))
% 0.47/0.64  (define @t54 () (= @t21 tptp.e4))
% 0.47/0.64  (define @t55 () (= @t31 tptp.e4))
% 0.47/0.64  (define @t56 () (or @t42 @t55 @t54 @t53 @t52))
% 0.47/0.64  (define @t57 () (= @t3 tptp.e4))
% 0.47/0.64  (define @t58 () (= @t5 tptp.e4))
% 0.47/0.64  (define @t59 () (= @t7 tptp.e4))
% 0.47/0.64  (define @t60 () (or @t10 @t59 @t58 @t57 @t52))
% 0.47/0.64  (define @t61 () (= @t1 tptp.e3))
% 0.47/0.64  (define @t62 () (= @t11 tptp.e3))
% 0.47/0.64  (define @t63 () (= @t21 tptp.e3))
% 0.47/0.64  (define @t64 () (= @t41 tptp.e3))
% 0.47/0.64  (define @t65 () (or @t64 @t32 @t63 @t62 @t61))
% 0.47/0.64  (define @t66 () (= @t3 tptp.e3))
% 0.47/0.64  (define @t67 () (= @t5 tptp.e3))
% 0.47/0.64  (define @t68 () (= @t9 tptp.e3))
% 0.47/0.64  (define @t69 () (or @t68 @t8 @t67 @t66 @t61))
% 0.47/0.64  (define @t70 () (= @t1 tptp.e2))
% 0.47/0.64  (define @t71 () (= @t21 tptp.e2))
% 0.47/0.64  (define @t72 () (= @t31 tptp.e2))
% 0.47/0.64  (define @t73 () (= @t41 tptp.e2))
% 0.47/0.64  (define @t74 () (or @t73 @t72 @t71 @t12 @t70))
% 0.47/0.64  (define @t75 () (= @t5 tptp.e2))
% 0.47/0.64  (define @t76 () (= @t7 tptp.e2))
% 0.47/0.64  (define @t77 () (= @t9 tptp.e2))
% 0.47/0.64  (define @t78 () (or @t77 @t76 @t75 @t4 @t70))
% 0.47/0.64  (define @t79 () (= @t1 tptp.e1))
% 0.47/0.64  (define @t80 () (= @t11 tptp.e1))
% 0.47/0.64  (define @t81 () (= @t31 tptp.e1))
% 0.47/0.64  (define @t82 () (= @t41 tptp.e1))
% 0.47/0.64  (define @t83 () (or @t82 @t81 @t22 @t80 @t79))
% 0.47/0.64  (define @t84 () (= @t3 tptp.e1))
% 0.47/0.64  (define @t85 () (= @t7 tptp.e1))
% 0.47/0.64  (define @t86 () (= @t9 tptp.e1))
% 0.47/0.64  (define @t87 () (or @t86 @t85 @t6 @t84 @t79))
% 0.47/0.64  (define @t88 () (= @t11 tptp.e0))
% 0.47/0.64  (define @t89 () (= @t21 tptp.e0))
% 0.47/0.64  (define @t90 () (= @t31 tptp.e0))
% 0.47/0.64  (define @t91 () (= @t41 tptp.e0))
% 0.47/0.64  (define @t92 () (or @t91 @t90 @t89 @t88 @t2))
% 0.47/0.64  (define @t93 () (= @t3 tptp.e0))
% 0.47/0.64  (define @t94 () (= @t5 tptp.e0))
% 0.47/0.64  (define @t95 () (= @t7 tptp.e0))
% 0.47/0.64  (define @t96 () (= @t9 tptp.e0))
% 0.47/0.64  (define @t97 () (or @t96 @t95 @t94 @t93 @t2))
% 0.47/0.64  (define @t98 () (= @t13 tptp.e4))
% 0.47/0.64  (define @t99 () (= @t33 tptp.e4))
% 0.47/0.64  (define @t100 () (= @t43 tptp.e4))
% 0.47/0.64  (define @t101 () (or @t100 @t99 @t24 @t98 @t57))
% 0.47/0.64  (define @t102 () (= @t15 tptp.e4))
% 0.47/0.64  (define @t103 () (= @t19 tptp.e4))
% 0.47/0.64  (define @t104 () (or @t103 @t18 @t102 @t98 @t53))
% 0.47/0.64  (define @t105 () (= @t13 tptp.e3))
% 0.47/0.64  (define @t106 () (= @t23 tptp.e3))
% 0.47/0.64  (define @t107 () (= @t33 tptp.e3))
% 0.47/0.64  (define @t108 () (or @t44 @t107 @t106 @t105 @t66))
% 0.47/0.64  (define @t109 () (= @t15 tptp.e3))
% 0.47/0.64  (define @t110 () (= @t17 tptp.e3))
% 0.47/0.64  (define @t111 () (or @t20 @t110 @t109 @t105 @t62))
% 0.47/0.64  (define @t112 () (= @t13 tptp.e2))
% 0.47/0.64  (define @t113 () (= @t23 tptp.e2))
% 0.47/0.64  (define @t114 () (= @t33 tptp.e2))
% 0.47/0.64  (define @t115 () (= @t43 tptp.e2))
% 0.47/0.64  (define @t116 () (or @t115 @t114 @t113 @t112 @t4))
% 0.47/0.64  (define @t117 () (= @t15 tptp.e2))
% 0.47/0.64  (define @t118 () (= @t17 tptp.e2))
% 0.47/0.64  (define @t119 () (= @t19 tptp.e2))
% 0.47/0.64  (define @t120 () (or @t119 @t118 @t117 @t112 @t12))
% 0.47/0.64  (define @t121 () (= @t23 tptp.e1))
% 0.47/0.64  (define @t122 () (= @t33 tptp.e1))
% 0.47/0.64  (define @t123 () (= @t43 tptp.e1))
% 0.47/0.64  (define @t124 () (or @t123 @t122 @t121 @t14 @t84))
% 0.47/0.64  (define @t125 () (= @t15 tptp.e1))
% 0.47/0.64  (define @t126 () (= @t17 tptp.e1))
% 0.47/0.64  (define @t127 () (= @t19 tptp.e1))
% 0.47/0.64  (define @t128 () (or @t127 @t126 @t125 @t14 @t80))
% 0.47/0.64  (define @t129 () (= @t13 tptp.e0))
% 0.47/0.64  (define @t130 () (= @t23 tptp.e0))
% 0.47/0.64  (define @t131 () (= @t43 tptp.e0))
% 0.47/0.64  (define @t132 () (or @t131 @t34 @t130 @t129 @t93))
% 0.47/0.64  (define @t133 () (= @t17 tptp.e0))
% 0.47/0.64  (define @t134 () (= @t19 tptp.e0))
% 0.47/0.64  (define @t135 () (or @t134 @t133 @t16 @t129 @t88))
% 0.47/0.64  (define @t136 () (= @t25 tptp.e4))
% 0.47/0.64  (define @t137 () (= @t45 tptp.e4))
% 0.47/0.64  (define @t138 () (or @t137 @t36 @t136 @t102 @t58))
% 0.47/0.64  (define @t139 () (= @t27 tptp.e4))
% 0.47/0.64  (define @t140 () (= @t29 tptp.e4))
% 0.47/0.64  (define @t141 () (or @t140 @t139 @t136 @t24 @t54))
% 0.47/0.64  (define @t142 () (= @t35 tptp.e3))
% 0.47/0.64  (define @t143 () (= @t45 tptp.e3))
% 0.47/0.64  (define @t144 () (or @t143 @t142 @t26 @t109 @t67))
% 0.47/0.64  (define @t145 () (= @t27 tptp.e3))
% 0.47/0.64  (define @t146 () (= @t29 tptp.e3))
% 0.47/0.64  (define @t147 () (or @t146 @t145 @t26 @t106 @t63))
% 0.47/0.64  (define @t148 () (= @t25 tptp.e2))
% 0.47/0.64  (define @t149 () (= @t35 tptp.e2))
% 0.47/0.64  (define @t150 () (or @t46 @t149 @t148 @t117 @t75))
% 0.47/0.64  (define @t151 () (= @t27 tptp.e2))
% 0.47/0.64  (define @t152 () (or @t30 @t151 @t148 @t113 @t71))
% 0.47/0.64  (define @t153 () (= @t25 tptp.e1))
% 0.47/0.64  (define @t154 () (= @t35 tptp.e1))
% 0.47/0.64  (define @t155 () (= @t45 tptp.e1))
% 0.47/0.64  (define @t156 () (or @t155 @t154 @t153 @t125 @t6))
% 0.47/0.64  (define @t157 () (= @t27 tptp.e1))
% 0.47/0.64  (define @t158 () (= @t29 tptp.e1))
% 0.47/0.64  (define @t159 () (or @t158 @t157 @t153 @t121 @t22))
% 0.47/0.64  (define @t160 () (= @t25 tptp.e0))
% 0.47/0.64  (define @t161 () (= @t35 tptp.e0))
% 0.47/0.64  (define @t162 () (= @t45 tptp.e0))
% 0.47/0.64  (define @t163 () (or @t162 @t161 @t160 @t16 @t94))
% 0.47/0.64  (define @t164 () (= @t29 tptp.e0))
% 0.47/0.64  (define @t165 () (or @t164 @t28 @t160 @t130 @t89))
% 0.47/0.64  (define @t166 () (= @t37 tptp.e4))
% 0.47/0.64  (define @t167 () (= @t47 tptp.e4))
% 0.47/0.64  (define @t168 () (or @t167 @t166 @t139 @t18 @t59))
% 0.47/0.64  (define @t169 () (= @t39 tptp.e4))
% 0.47/0.64  (define @t170 () (or @t169 @t166 @t36 @t99 @t55))
% 0.47/0.64  (define @t171 () (= @t37 tptp.e3))
% 0.47/0.64  (define @t172 () (= @t47 tptp.e3))
% 0.47/0.64  (define @t173 () (or @t172 @t171 @t145 @t110 @t8))
% 0.47/0.64  (define @t174 () (= @t39 tptp.e3))
% 0.47/0.64  (define @t175 () (or @t174 @t171 @t142 @t107 @t32))
% 0.47/0.64  (define @t176 () (= @t47 tptp.e2))
% 0.47/0.64  (define @t177 () (or @t176 @t38 @t151 @t118 @t76))
% 0.47/0.64  (define @t178 () (= @t39 tptp.e2))
% 0.47/0.64  (define @t179 () (or @t178 @t38 @t149 @t114 @t72))
% 0.47/0.64  (define @t180 () (= @t37 tptp.e1))
% 0.47/0.64  (define @t181 () (or @t48 @t180 @t157 @t126 @t85))
% 0.47/0.64  (define @t182 () (or @t40 @t180 @t154 @t122 @t81))
% 0.47/0.64  (define @t183 () (= @t37 tptp.e0))
% 0.47/0.64  (define @t184 () (= @t47 tptp.e0))
% 0.47/0.64  (define @t185 () (or @t184 @t183 @t28 @t133 @t95))
% 0.47/0.64  (define @t186 () (= @t39 tptp.e0))
% 0.47/0.64  (define @t187 () (or @t186 @t183 @t161 @t34 @t90))
% 0.47/0.64  (define @t188 () (= @t49 tptp.e4))
% 0.47/0.64  (define @t189 () (or @t188 @t169 @t140 @t103 @t10))
% 0.47/0.64  (define @t190 () (or @t188 @t167 @t137 @t100 @t42))
% 0.47/0.64  (define @t191 () (= @t49 tptp.e3))
% 0.47/0.64  (define @t192 () (or @t191 @t174 @t146 @t20 @t68))
% 0.47/0.64  (define @t193 () (or @t191 @t172 @t143 @t44 @t64))
% 0.47/0.64  (define @t194 () (= @t49 tptp.e2))
% 0.47/0.64  (define @t195 () (or @t194 @t178 @t30 @t119 @t77))
% 0.47/0.64  (define @t196 () (or @t194 @t176 @t46 @t115 @t73))
% 0.47/0.64  (define @t197 () (= @t49 tptp.e1))
% 0.47/0.64  (define @t198 () (or @t197 @t40 @t158 @t127 @t86))
% 0.47/0.64  (define @t199 () (or @t197 @t48 @t155 @t123 @t82))
% 0.47/0.64  (define @t200 () (or @t50 @t186 @t164 @t134 @t96))
% 0.47/0.64  (define @t201 () (or @t50 @t184 @t162 @t131 @t91))
% 0.47/0.64  (define @t202 () (or @t51 (= tptp.unit tptp.e1) (= tptp.unit tptp.e2) (= tptp.unit tptp.e3) (= tptp.unit tptp.e4)))
% 0.47/0.64  (define @t203 () (tptp.op tptp.e4 tptp.unit))
% 0.47/0.64  (define @t204 () (tptp.op tptp.unit tptp.e4))
% 0.47/0.64  (define @t205 () (tptp.op tptp.e3 tptp.unit))
% 0.47/0.64  (define @t206 () (tptp.op tptp.unit tptp.e3))
% 0.47/0.64  (define @t207 () (tptp.op tptp.e2 tptp.unit))
% 0.47/0.64  (define @t208 () (tptp.op tptp.unit tptp.e2))
% 0.47/0.64  (define @t209 () (tptp.op tptp.e1 tptp.unit))
% 0.47/0.64  (define @t210 () (tptp.op tptp.unit tptp.e1))
% 0.47/0.64  (define @t211 () (tptp.op tptp.e0 tptp.unit))
% 0.47/0.64  (define @t212 () (tptp.op tptp.unit tptp.e0))
% 0.47/0.64  (define @t213 () (or @t2 @t79 @t70 @t61 @t52))
% 0.47/0.64  (define @t214 () (or @t93 @t84 @t4 @t66 @t57))
% 0.47/0.64  (define @t215 () (or @t94 @t6 @t75 @t67 @t58))
% 0.47/0.64  (define @t216 () (or @t95 @t85 @t76 @t8 @t59))
% 0.47/0.64  (define @t217 () (or @t96 @t86 @t77 @t68 @t10))
% 0.47/0.64  (define @t218 () (or @t88 @t80 @t12 @t62 @t53))
% 0.47/0.64  (define @t219 () (or @t129 @t14 @t112 @t105 @t98))
% 0.47/0.64  (define @t220 () (or @t16 @t125 @t117 @t109 @t102))
% 0.47/0.64  (define @t221 () (or @t133 @t126 @t118 @t110 @t18))
% 0.47/0.64  (define @t222 () (or @t134 @t127 @t119 @t20 @t103))
% 0.47/0.64  (define @t223 () (or @t89 @t22 @t71 @t63 @t54))
% 0.47/0.64  (define @t224 () (or @t130 @t121 @t113 @t106 @t24))
% 0.47/0.64  (define @t225 () (or @t160 @t153 @t148 @t26 @t136))
% 0.47/0.64  (define @t226 () (or @t28 @t157 @t151 @t145 @t139))
% 0.47/0.64  (define @t227 () (or @t164 @t158 @t30 @t146 @t140))
% 0.47/0.64  (define @t228 () (or @t90 @t81 @t72 @t32 @t55))
% 0.47/0.64  (define @t229 () (or @t34 @t122 @t114 @t107 @t99))
% 0.47/0.64  (define @t230 () (or @t161 @t154 @t149 @t142 @t36))
% 0.47/0.64  (define @t231 () (or @t183 @t180 @t38 @t171 @t166))
% 0.47/0.64  (define @t232 () (or @t186 @t40 @t178 @t174 @t169))
% 0.47/0.64  (define @t233 () (or @t91 @t82 @t73 @t64 @t42))
% 0.47/0.64  (define @t234 () (or @t131 @t123 @t115 @t44 @t100))
% 0.47/0.64  (define @t235 () (or @t162 @t155 @t46 @t143 @t137))
% 0.47/0.64  (define @t236 () (or @t184 @t48 @t176 @t172 @t167))
% 0.47/0.64  (define @t237 () (or @t50 @t197 @t194 @t191 @t188))
% 0.47/0.64  (define @t238 () (tptp.op @t1 tptp.e4))
% 0.47/0.64  (define @t239 () (= @t238 tptp.e4))
% 0.47/0.64  (define @t240 () (not @t239))
% 0.47/0.64  (define @t241 () (not (= @t1 @t1)))
% 0.47/0.64  (define @t242 () (and @t241 @t239 @t240))
% 0.47/0.64  (define @t243 () (tptp.op @t3 tptp.e4))
% 0.47/0.64  (define @t244 () (not (= @t243 tptp.e3)))
% 0.47/0.64  (define @t245 () (tptp.op @t3 tptp.e3))
% 0.47/0.64  (define @t246 () (not (= @t11 @t3)))
% 0.47/0.64  (define @t247 () (and @t246 (= @t245 tptp.e4) @t244))
% 0.47/0.64  (define @t248 () (tptp.op @t5 tptp.e4))
% 0.47/0.64  (define @t249 () (not (= @t248 tptp.e2)))
% 0.47/0.64  (define @t250 () (tptp.op @t5 tptp.e2))
% 0.47/0.64  (define @t251 () (not (= @t21 @t5)))
% 0.47/0.64  (define @t252 () (and @t251 (= @t250 tptp.e4) @t249))
% 0.47/0.64  (define @t253 () (tptp.op @t7 tptp.e4))
% 0.47/0.64  (define @t254 () (not (= @t253 tptp.e1)))
% 0.47/0.64  (define @t255 () (tptp.op @t7 tptp.e1))
% 0.47/0.64  (define @t256 () (not (= @t31 @t7)))
% 0.47/0.64  (define @t257 () (and @t256 (= @t255 tptp.e4) @t254))
% 0.47/0.64  (define @t258 () (tptp.op @t9 tptp.e4))
% 0.47/0.64  (define @t259 () (not (= @t258 tptp.e0)))
% 0.47/0.64  (define @t260 () (tptp.op @t9 tptp.e0))
% 0.47/0.64  (define @t261 () (not (= @t41 @t9)))
% 0.47/0.64  (define @t262 () (and @t261 (= @t260 tptp.e4) @t259))
% 0.47/0.64  (define @t263 () (tptp.op @t11 tptp.e3))
% 0.47/0.64  (define @t264 () (not (= @t263 tptp.e4)))
% 0.47/0.64  (define @t265 () (tptp.op @t11 tptp.e4))
% 0.47/0.64  (define @t266 () (not (= @t3 @t11)))
% 0.47/0.64  (define @t267 () (and @t266 (= @t265 tptp.e3) @t264))
% 0.47/0.64  (define @t268 () (tptp.op @t13 tptp.e3))
% 0.47/0.64  (define @t269 () (= @t268 tptp.e3))
% 0.47/0.64  (define @t270 () (not @t269))
% 0.47/0.64  (define @t271 () (not (= @t13 @t13)))
% 0.47/0.64  (define @t272 () (and @t271 @t269 @t270))
% 0.47/0.64  (define @t273 () (tptp.op @t15 tptp.e3))
% 0.47/0.64  (define @t274 () (not (= @t273 tptp.e2)))
% 0.47/0.64  (define @t275 () (tptp.op @t15 tptp.e2))
% 0.47/0.64  (define @t276 () (not (= @t23 @t15)))
% 0.47/0.64  (define @t277 () (and @t276 (= @t275 tptp.e3) @t274))
% 0.47/0.64  (define @t278 () (tptp.op @t17 tptp.e3))
% 0.47/0.64  (define @t279 () (not (= @t278 tptp.e1)))
% 0.47/0.64  (define @t280 () (tptp.op @t17 tptp.e1))
% 0.47/0.64  (define @t281 () (= @t33 @t17))
% 0.47/0.64  (define @t282 () (not @t281))
% 0.47/0.64  (define @t283 () (and @t282 (= @t280 tptp.e3) @t279))
% 0.47/0.64  (define @t284 () (tptp.op @t19 tptp.e3))
% 0.47/0.64  (define @t285 () (not (= @t284 tptp.e0)))
% 0.47/0.64  (define @t286 () (tptp.op @t19 tptp.e0))
% 0.47/0.64  (define @t287 () (not (= @t43 @t19)))
% 0.47/0.64  (define @t288 () (and @t287 (= @t286 tptp.e3) @t285))
% 0.47/0.64  (define @t289 () (tptp.op @t21 tptp.e2))
% 0.47/0.64  (define @t290 () (not (= @t289 tptp.e4)))
% 0.47/0.64  (define @t291 () (tptp.op @t21 tptp.e4))
% 0.47/0.64  (define @t292 () (not (= @t5 @t21)))
% 0.47/0.64  (define @t293 () (and @t292 (= @t291 tptp.e2) @t290))
% 0.47/0.64  (define @t294 () (tptp.op @t23 tptp.e2))
% 0.47/0.64  (define @t295 () (not (= @t294 tptp.e3)))
% 0.47/0.64  (define @t296 () (tptp.op @t23 tptp.e3))
% 0.47/0.64  (define @t297 () (not (= @t15 @t23)))
% 0.47/0.64  (define @t298 () (and @t297 (= @t296 tptp.e2) @t295))
% 0.47/0.64  (define @t299 () (tptp.op @t25 tptp.e2))
% 0.47/0.64  (define @t300 () (= @t299 tptp.e2))
% 0.47/0.64  (define @t301 () (not @t300))
% 0.47/0.64  (define @t302 () (not (= @t25 @t25)))
% 0.47/0.64  (define @t303 () (and @t302 @t300 @t301))
% 0.47/0.64  (define @t304 () (tptp.op @t27 tptp.e2))
% 0.47/0.64  (define @t305 () (not (= @t304 tptp.e1)))
% 0.47/0.64  (define @t306 () (tptp.op @t27 tptp.e1))
% 0.47/0.64  (define @t307 () (not (= @t35 @t27)))
% 0.47/0.64  (define @t308 () (and @t307 (= @t306 tptp.e2) @t305))
% 0.47/0.64  (define @t309 () (tptp.op @t29 tptp.e2))
% 0.47/0.64  (define @t310 () (not (= @t309 tptp.e0)))
% 0.47/0.64  (define @t311 () (tptp.op @t29 tptp.e0))
% 0.47/0.64  (define @t312 () (not (= @t45 @t29)))
% 0.47/0.64  (define @t313 () (and @t312 (= @t311 tptp.e2) @t310))
% 0.47/0.64  (define @t314 () (tptp.op @t31 tptp.e1))
% 0.47/0.64  (define @t315 () (not (= @t314 tptp.e4)))
% 0.47/0.64  (define @t316 () (tptp.op @t31 tptp.e4))
% 0.47/0.64  (define @t317 () (not (= @t7 @t31)))
% 0.47/0.64  (define @t318 () (and @t317 (= @t316 tptp.e1) @t315))
% 0.47/0.64  (define @t319 () (tptp.op @t33 tptp.e1))
% 0.47/0.64  (define @t320 () (not (= @t319 tptp.e3)))
% 0.47/0.64  (define @t321 () (tptp.op @t33 tptp.e3))
% 0.47/0.64  (define @t322 () (not (= @t17 @t33)))
% 0.47/0.64  (define @t323 () (and @t322 (= @t321 tptp.e1) @t320))
% 0.47/0.64  (define @t324 () (tptp.op @t35 tptp.e1))
% 0.47/0.64  (define @t325 () (not (= @t324 tptp.e2)))
% 0.47/0.64  (define @t326 () (tptp.op @t35 tptp.e2))
% 0.47/0.64  (define @t327 () (not (= @t27 @t35)))
% 0.47/0.64  (define @t328 () (and @t327 (= @t326 tptp.e1) @t325))
% 0.47/0.64  (define @t329 () (tptp.op @t37 tptp.e1))
% 0.47/0.64  (define @t330 () (= @t329 tptp.e1))
% 0.47/0.64  (define @t331 () (not @t330))
% 0.47/0.64  (define @t332 () (not (= @t37 @t37)))
% 0.47/0.64  (define @t333 () (and @t332 @t330 @t331))
% 0.47/0.64  (define @t334 () (tptp.op @t39 tptp.e1))
% 0.47/0.64  (define @t335 () (not (= @t334 tptp.e0)))
% 0.47/0.64  (define @t336 () (tptp.op @t39 tptp.e0))
% 0.47/0.64  (define @t337 () (not (= @t47 @t39)))
% 0.47/0.65  (define @t338 () (and @t337 (= @t336 tptp.e1) @t335))
% 0.47/0.65  (define @t339 () (tptp.op @t41 tptp.e0))
% 0.47/0.65  (define @t340 () (not (= @t339 tptp.e4)))
% 0.47/0.65  (define @t341 () (tptp.op @t41 tptp.e4))
% 0.47/0.65  (define @t342 () (not (= @t9 @t41)))
% 0.47/0.65  (define @t343 () (and @t342 (= @t341 tptp.e0) @t340))
% 0.47/0.65  (define @t344 () (tptp.op @t43 tptp.e0))
% 0.47/0.65  (define @t345 () (not (= @t344 tptp.e3)))
% 0.47/0.65  (define @t346 () (tptp.op @t43 tptp.e3))
% 0.47/0.65  (define @t347 () (not (= @t19 @t43)))
% 0.47/0.65  (define @t348 () (and @t347 (= @t346 tptp.e0) @t345))
% 0.47/0.65  (define @t349 () (tptp.op @t45 tptp.e0))
% 0.47/0.65  (define @t350 () (not (= @t349 tptp.e2)))
% 0.47/0.65  (define @t351 () (tptp.op @t45 tptp.e2))
% 0.47/0.65  (define @t352 () (not (= @t29 @t45)))
% 0.47/0.65  (define @t353 () (and @t352 (= @t351 tptp.e0) @t350))
% 0.47/0.65  (define @t354 () (tptp.op @t47 tptp.e0))
% 0.47/0.65  (define @t355 () (not (= @t354 tptp.e1)))
% 0.47/0.65  (define @t356 () (tptp.op @t47 tptp.e1))
% 0.47/0.65  (define @t357 () (not (= @t39 @t47)))
% 0.47/0.65  (define @t358 () (and @t357 (= @t356 tptp.e0) @t355))
% 0.47/0.65  (define @t359 () (tptp.op @t49 tptp.e0))
% 0.47/0.65  (define @t360 () (= @t359 tptp.e0))
% 0.47/0.65  (define @t361 () (not @t360))
% 0.47/0.65  (define @t362 () (not (= @t49 @t49)))
% 0.47/0.65  (define @t363 () (and @t362 @t360 @t361))
% 0.47/0.65  (define @t364 () (or @t363 @t358 @t353 @t348 @t343 @t338 @t333 @t328 @t323 @t318 @t313 @t308 @t303 @t298 @t293 @t288 @t283 @t277 @t272 @t267 @t262 @t257 @t252 @t247 @t242))
% 0.47/0.65  (define @t365 () (and @t364 @t237 @t236 @t235 @t234 @t233 @t232 @t231 @t230 @t229 @t228 @t227 @t226 @t225 @t224 @t223 @t222 @t221 @t220 @t219 @t218 @t217 @t216 @t215 @t214 @t213 (= @t212 tptp.e0) (= @t211 tptp.e0) (= @t210 tptp.e1) (= @t209 tptp.e1) (= @t208 tptp.e2) (= @t207 tptp.e2) (= @t206 tptp.e3) (= @t205 tptp.e3) (= @t204 tptp.e4) (= @t203 tptp.e4) @t202 @t201 @t200 @t199 @t198 @t196 @t195 @t193 @t192 @t190 @t189 @t187 @t185 @t182 @t181 @t179 @t177 @t175 @t173 @t170 @t168 @t165 @t163 @t159 @t156 @t152 @t150 @t147 @t144 @t141 @t138 @t135 @t132 @t128 @t124 @t120 @t116 @t111 @t108 @t104 @t101 @t97 @t92 @t87 @t83 @t78 @t74 @t69 @t65 @t60 @t56))
% 0.47/0.65  (define @t366 () (not @t365))
% 0.47/0.65  (define @t367 () (= tptp.e1 @t278))
% 0.47/0.65  (define @t368 () (= tptp.e3 @t280))
% 0.47/0.65  (define @t369 () (not @t368))
% 0.47/0.65  (define @t370 () (not @t367))
% 0.47/0.65  (define @t371 () (and @t282 @t368 @t370))
% 0.47/0.65  (define @t372 () (= tptp.e4 @t1))
% 0.47/0.65  (define @t373 () (= tptp.e4 @t11))
% 0.47/0.65  (define @t374 () (= tptp.e4 @t21))
% 0.47/0.65  (define @t375 () (= tptp.e4 @t31))
% 0.47/0.65  (define @t376 () (= tptp.e4 @t41))
% 0.47/0.65  (define @t377 () (or @t376 @t375 @t374 @t373 @t372))
% 0.47/0.65  (define @t378 () (@list false))
% 0.47/0.65  (define @t379 () (@list @t376))
% 0.47/0.65  (define @t380 () (= tptp.e4 @t3))
% 0.47/0.65  (define @t381 () (= tptp.e4 @t5))
% 0.47/0.65  (define @t382 () (= tptp.e4 @t7))
% 0.47/0.65  (define @t383 () (= tptp.e4 @t9))
% 0.47/0.65  (define @t384 () (or @t383 @t382 @t381 @t380 @t372))
% 0.47/0.65  (define @t385 () (@list @t383))
% 0.47/0.65  (define @t386 () (= tptp.e3 @t1))
% 0.47/0.65  (define @t387 () (= tptp.e3 @t11))
% 0.47/0.65  (define @t388 () (= tptp.e3 @t21))
% 0.47/0.65  (define @t389 () (= tptp.e3 @t31))
% 0.47/0.65  (define @t390 () (= tptp.e3 @t41))
% 0.47/0.65  (define @t391 () (or @t390 @t389 @t388 @t387 @t386))
% 0.47/0.65  (define @t392 () (@list @t389))
% 0.47/0.65  (define @t393 () (= tptp.e3 @t3))
% 0.47/0.65  (define @t394 () (= tptp.e3 @t5))
% 0.47/0.65  (define @t395 () (= tptp.e3 @t7))
% 0.47/0.65  (define @t396 () (= tptp.e3 @t9))
% 0.47/0.65  (define @t397 () (or @t396 @t395 @t394 @t393 @t386))
% 0.47/0.65  (define @t398 () (@list @t395))
% 0.47/0.65  (define @t399 () (= tptp.e2 @t1))
% 0.47/0.65  (define @t400 () (= tptp.e2 @t11))
% 0.47/0.65  (define @t401 () (= tptp.e2 @t21))
% 0.47/0.65  (define @t402 () (= tptp.e2 @t31))
% 0.47/0.65  (define @t403 () (= tptp.e2 @t41))
% 0.47/0.65  (define @t404 () (or @t403 @t402 @t401 @t400 @t399))
% 0.47/0.65  (define @t405 () (@list @t400))
% 0.47/0.65  (define @t406 () (= tptp.e2 @t3))
% 0.47/0.65  (define @t407 () (= tptp.e2 @t5))
% 0.47/0.65  (define @t408 () (= tptp.e2 @t7))
% 0.47/0.65  (define @t409 () (= tptp.e2 @t9))
% 0.47/0.65  (define @t410 () (or @t409 @t408 @t407 @t406 @t399))
% 0.47/0.65  (define @t411 () (@list @t406))
% 0.47/0.65  (define @t412 () (= tptp.e1 @t1))
% 0.47/0.65  (define @t413 () (= tptp.e1 @t11))
% 0.47/0.65  (define @t414 () (= tptp.e1 @t21))
% 0.47/0.65  (define @t415 () (= tptp.e1 @t31))
% 0.47/0.65  (define @t416 () (= tptp.e1 @t41))
% 0.47/0.65  (define @t417 () (or @t416 @t415 @t414 @t413 @t412))
% 0.47/0.65  (define @t418 () (@list @t414))
% 0.47/0.65  (define @t419 () (= tptp.e1 @t3))
% 0.47/0.65  (define @t420 () (= tptp.e1 @t5))
% 0.47/0.65  (define @t421 () (= tptp.e1 @t7))
% 0.47/0.65  (define @t422 () (= tptp.e1 @t9))
% 0.47/0.65  (define @t423 () (or @t422 @t421 @t420 @t419 @t412))
% 0.47/0.65  (define @t424 () (@list @t420))
% 0.47/0.65  (define @t425 () (= tptp.e0 @t1))
% 0.47/0.65  (define @t426 () (= tptp.e0 @t11))
% 0.47/0.65  (define @t427 () (= tptp.e0 @t21))
% 0.47/0.65  (define @t428 () (= tptp.e0 @t31))
% 0.47/0.65  (define @t429 () (= tptp.e0 @t41))
% 0.47/0.65  (define @t430 () (or @t429 @t428 @t427 @t426 @t425))
% 0.47/0.65  (define @t431 () (@list @t425))
% 0.47/0.65  (define @t432 () (= tptp.e0 @t3))
% 0.47/0.65  (define @t433 () (= tptp.e0 @t5))
% 0.47/0.65  (define @t434 () (= tptp.e0 @t7))
% 0.47/0.65  (define @t435 () (= tptp.e0 @t9))
% 0.47/0.65  (define @t436 () (or @t435 @t434 @t433 @t432 @t425))
% 0.47/0.65  (define @t437 () (= tptp.e4 @t13))
% 0.47/0.65  (define @t438 () (= tptp.e4 @t23))
% 0.47/0.65  (define @t439 () (= tptp.e4 @t33))
% 0.47/0.65  (define @t440 () (= tptp.e4 @t43))
% 0.47/0.65  (define @t441 () (or @t440 @t439 @t438 @t437 @t380))
% 0.47/0.65  (define @t442 () (@list @t438))
% 0.47/0.65  (define @t443 () (= tptp.e4 @t15))
% 0.47/0.65  (define @t444 () (= tptp.e4 @t17))
% 0.47/0.65  (define @t445 () (= tptp.e4 @t19))
% 0.47/0.65  (define @t446 () (or @t445 @t444 @t443 @t437 @t373))
% 0.47/0.65  (define @t447 () (@list @t444))
% 0.47/0.65  (define @t448 () (= tptp.e3 @t13))
% 0.47/0.65  (define @t449 () (= tptp.e3 @t23))
% 0.47/0.65  (define @t450 () (= tptp.e3 @t33))
% 0.47/0.65  (define @t451 () (= tptp.e3 @t43))
% 0.47/0.65  (define @t452 () (or @t451 @t450 @t449 @t448 @t393))
% 0.47/0.65  (define @t453 () (@list @t451))
% 0.47/0.65  (define @t454 () (= tptp.e3 @t15))
% 0.47/0.65  (define @t455 () (= tptp.e3 @t17))
% 0.47/0.65  (define @t456 () (= tptp.e3 @t19))
% 0.47/0.65  (define @t457 () (or @t456 @t455 @t454 @t448 @t387))
% 0.47/0.65  (define @t458 () (@list @t456))
% 0.47/0.65  (define @t459 () (= tptp.e2 @t13))
% 0.47/0.65  (define @t460 () (= tptp.e2 @t23))
% 0.47/0.65  (define @t461 () (= tptp.e2 @t33))
% 0.47/0.65  (define @t462 () (= tptp.e2 @t43))
% 0.47/0.65  (define @t463 () (or @t462 @t461 @t460 @t459 @t406))
% 0.47/0.65  (define @t464 () (= tptp.e2 @t15))
% 0.47/0.65  (define @t465 () (= tptp.e2 @t17))
% 0.47/0.65  (define @t466 () (= tptp.e2 @t19))
% 0.47/0.65  (define @t467 () (or @t466 @t465 @t464 @t459 @t400))
% 0.47/0.65  (define @t468 () (= tptp.e1 @t13))
% 0.47/0.65  (define @t469 () (= tptp.e1 @t23))
% 0.47/0.65  (define @t470 () (= tptp.e1 @t33))
% 0.47/0.65  (define @t471 () (= tptp.e1 @t43))
% 0.47/0.65  (define @t472 () (or @t471 @t470 @t469 @t468 @t419))
% 0.47/0.65  (define @t473 () (@list @t468))
% 0.47/0.65  (define @t474 () (= tptp.e1 @t15))
% 0.47/0.65  (define @t475 () (= tptp.e1 @t17))
% 0.47/0.65  (define @t476 () (= tptp.e1 @t19))
% 0.47/0.65  (define @t477 () (or @t476 @t475 @t474 @t468 @t413))
% 0.47/0.65  (define @t478 () (= tptp.e0 @t13))
% 0.47/0.65  (define @t479 () (= tptp.e0 @t23))
% 0.47/0.65  (define @t480 () (= tptp.e0 @t33))
% 0.47/0.65  (define @t481 () (= tptp.e0 @t43))
% 0.47/0.65  (define @t482 () (or @t481 @t480 @t479 @t478 @t432))
% 0.47/0.65  (define @t483 () (@list @t480))
% 0.47/0.65  (define @t484 () (= tptp.e0 @t15))
% 0.47/0.65  (define @t485 () (= tptp.e0 @t17))
% 0.47/0.65  (define @t486 () (= tptp.e0 @t19))
% 0.47/0.65  (define @t487 () (or @t486 @t485 @t484 @t478 @t426))
% 0.47/0.65  (define @t488 () (@list @t484))
% 0.47/0.65  (define @t489 () (= tptp.e4 @t25))
% 0.47/0.65  (define @t490 () (= tptp.e4 @t35))
% 0.47/0.65  (define @t491 () (= tptp.e4 @t45))
% 0.47/0.65  (define @t492 () (or @t491 @t490 @t489 @t443 @t381))
% 0.47/0.65  (define @t493 () (@list @t490))
% 0.47/0.65  (define @t494 () (= tptp.e4 @t27))
% 0.47/0.65  (define @t495 () (= tptp.e4 @t29))
% 0.47/0.65  (define @t496 () (or @t495 @t494 @t489 @t438 @t374))
% 0.47/0.65  (define @t497 () (= tptp.e3 @t25))
% 0.47/0.65  (define @t498 () (= tptp.e3 @t35))
% 0.47/0.65  (define @t499 () (= tptp.e3 @t45))
% 0.47/0.65  (define @t500 () (or @t499 @t498 @t497 @t454 @t394))
% 0.47/0.65  (define @t501 () (@list @t497))
% 0.47/0.65  (define @t502 () (= tptp.e3 @t27))
% 0.47/0.65  (define @t503 () (= tptp.e3 @t29))
% 0.47/0.65  (define @t504 () (or @t503 @t502 @t497 @t449 @t388))
% 0.47/0.65  (define @t505 () (= tptp.e2 @t25))
% 0.47/0.65  (define @t506 () (= tptp.e2 @t35))
% 0.47/0.65  (define @t507 () (= tptp.e2 @t45))
% 0.47/0.65  (define @t508 () (or @t507 @t506 @t505 @t464 @t407))
% 0.47/0.65  (define @t509 () (@list @t507))
% 0.47/0.65  (define @t510 () (= tptp.e2 @t27))
% 0.47/0.65  (define @t511 () (= tptp.e2 @t29))
% 0.47/0.65  (define @t512 () (or @t511 @t510 @t505 @t460 @t401))
% 0.47/0.65  (define @t513 () (@list @t511))
% 0.47/0.65  (define @t514 () (= tptp.e1 @t25))
% 0.47/0.65  (define @t515 () (= tptp.e1 @t35))
% 0.47/0.65  (define @t516 () (= tptp.e1 @t45))
% 0.47/0.65  (define @t517 () (or @t516 @t515 @t514 @t474 @t420))
% 0.47/0.65  (define @t518 () (= tptp.e1 @t27))
% 0.47/0.65  (define @t519 () (= tptp.e1 @t29))
% 0.47/0.65  (define @t520 () (or @t519 @t518 @t514 @t469 @t414))
% 0.47/0.65  (define @t521 () (= tptp.e0 @t25))
% 0.47/0.65  (define @t522 () (= tptp.e0 @t35))
% 0.47/0.65  (define @t523 () (= tptp.e0 @t45))
% 0.47/0.65  (define @t524 () (or @t523 @t522 @t521 @t484 @t433))
% 0.47/0.65  (define @t525 () (= tptp.e0 @t27))
% 0.47/0.65  (define @t526 () (= tptp.e0 @t29))
% 0.47/0.65  (define @t527 () (or @t526 @t525 @t521 @t479 @t427))
% 0.47/0.65  (define @t528 () (@list @t525))
% 0.47/0.65  (define @t529 () (= tptp.e4 @t37))
% 0.47/0.65  (define @t530 () (= tptp.e4 @t47))
% 0.47/0.65  (define @t531 () (or @t530 @t529 @t494 @t444 @t382))
% 0.47/0.65  (define @t532 () (= tptp.e4 @t39))
% 0.47/0.65  (define @t533 () (or @t532 @t529 @t490 @t439 @t375))
% 0.47/0.65  (define @t534 () (= tptp.e3 @t37))
% 0.47/0.65  (define @t535 () (= tptp.e3 @t47))
% 0.47/0.65  (define @t536 () (or @t535 @t534 @t502 @t455 @t395))
% 0.47/0.65  (define @t537 () (= tptp.e3 @t39))
% 0.47/0.65  (define @t538 () (or @t537 @t534 @t498 @t450 @t389))
% 0.47/0.65  (define @t539 () (= tptp.e2 @t37))
% 0.47/0.65  (define @t540 () (= tptp.e2 @t47))
% 0.47/0.65  (define @t541 () (or @t540 @t539 @t510 @t465 @t408))
% 0.47/0.65  (define @t542 () (@list @t539))
% 0.47/0.65  (define @t543 () (= tptp.e2 @t39))
% 0.47/0.65  (define @t544 () (or @t543 @t539 @t506 @t461 @t402))
% 0.47/0.65  (define @t545 () (= tptp.e1 @t37))
% 0.47/0.65  (define @t546 () (= tptp.e1 @t47))
% 0.47/0.65  (define @t547 () (or @t546 @t545 @t518 @t475 @t421))
% 0.47/0.65  (define @t548 () (@list @t546))
% 0.47/0.65  (define @t549 () (= tptp.e1 @t39))
% 0.47/0.65  (define @t550 () (or @t549 @t545 @t515 @t470 @t415))
% 0.47/0.65  (define @t551 () (@list @t549))
% 0.47/0.65  (define @t552 () (= tptp.e0 @t37))
% 0.47/0.65  (define @t553 () (= tptp.e0 @t47))
% 0.47/0.65  (define @t554 () (or @t553 @t552 @t525 @t485 @t434))
% 0.47/0.65  (define @t555 () (= tptp.e0 @t39))
% 0.47/0.65  (define @t556 () (or @t555 @t552 @t522 @t480 @t428))
% 0.47/0.65  (define @t557 () (= tptp.e4 @t49))
% 0.47/0.65  (define @t558 () (or @t557 @t532 @t495 @t445 @t383))
% 0.47/0.65  (define @t559 () (or @t557 @t530 @t491 @t440 @t376))
% 0.47/0.65  (define @t560 () (= tptp.e3 @t49))
% 0.47/0.65  (define @t561 () (or @t560 @t537 @t503 @t456 @t396))
% 0.47/0.65  (define @t562 () (or @t560 @t535 @t499 @t451 @t390))
% 0.47/0.65  (define @t563 () (= tptp.e2 @t49))
% 0.47/0.65  (define @t564 () (or @t563 @t543 @t511 @t466 @t409))
% 0.47/0.65  (define @t565 () (or @t563 @t540 @t507 @t462 @t403))
% 0.47/0.65  (define @t566 () (= tptp.e1 @t49))
% 0.47/0.65  (define @t567 () (or @t566 @t549 @t519 @t476 @t422))
% 0.47/0.65  (define @t568 () (or @t566 @t546 @t516 @t471 @t416))
% 0.47/0.65  (define @t569 () (= tptp.e0 @t49))
% 0.47/0.65  (define @t570 () (or @t569 @t555 @t526 @t486 @t435))
% 0.47/0.65  (define @t571 () (@list @t569))
% 0.47/0.65  (define @t572 () (or @t569 @t553 @t523 @t481 @t429))
% 0.47/0.65  (define @t573 () (= tptp.e0 tptp.unit))
% 0.47/0.65  (define @t574 () (or @t573 (= tptp.e1 tptp.unit) (= tptp.e2 tptp.unit) (= tptp.e3 tptp.unit) (= tptp.e4 tptp.unit)))
% 0.47/0.65  (define @t575 () (or @t425 @t412 @t399 @t386 @t372))
% 0.47/0.65  (define @t576 () (or @t432 @t419 @t406 @t393 @t380))
% 0.47/0.65  (define @t577 () (or @t433 @t420 @t407 @t394 @t381))
% 0.47/0.65  (define @t578 () (or @t434 @t421 @t408 @t395 @t382))
% 0.47/0.65  (define @t579 () (or @t435 @t422 @t409 @t396 @t383))
% 0.47/0.65  (define @t580 () (or @t426 @t413 @t400 @t387 @t373))
% 0.47/0.65  (define @t581 () (or @t478 @t468 @t459 @t448 @t437))
% 0.47/0.65  (define @t582 () (or @t484 @t474 @t464 @t454 @t443))
% 0.47/0.65  (define @t583 () (or @t485 @t475 @t465 @t455 @t444))
% 0.47/0.65  (define @t584 () (or @t486 @t476 @t466 @t456 @t445))
% 0.47/0.65  (define @t585 () (or @t427 @t414 @t401 @t388 @t374))
% 0.47/0.65  (define @t586 () (or @t479 @t469 @t460 @t449 @t438))
% 0.47/0.65  (define @t587 () (or @t521 @t514 @t505 @t497 @t489))
% 0.47/0.65  (define @t588 () (or @t525 @t518 @t510 @t502 @t494))
% 0.47/0.65  (define @t589 () (or @t526 @t519 @t511 @t503 @t495))
% 0.47/0.65  (define @t590 () (or @t428 @t415 @t402 @t389 @t375))
% 0.47/0.65  (define @t591 () (or @t480 @t470 @t461 @t450 @t439))
% 0.47/0.65  (define @t592 () (or @t522 @t515 @t506 @t498 @t490))
% 0.47/0.65  (define @t593 () (or @t552 @t545 @t539 @t534 @t529))
% 0.47/0.65  (define @t594 () (or @t555 @t549 @t543 @t537 @t532))
% 0.47/0.65  (define @t595 () (or @t429 @t416 @t403 @t390 @t376))
% 0.47/0.65  (define @t596 () (or @t481 @t471 @t462 @t451 @t440))
% 0.47/0.65  (define @t597 () (or @t523 @t516 @t507 @t499 @t491))
% 0.47/0.65  (define @t598 () (or @t553 @t546 @t540 @t535 @t530))
% 0.47/0.65  (define @t599 () (or @t569 @t566 @t563 @t560 @t557))
% 0.47/0.65  (define @t600 () (and @t246 (= tptp.e4 @t245) (not (= tptp.e3 @t243))))
% 0.47/0.65  (define @t601 () (and @t251 (= tptp.e4 @t250) (not (= tptp.e2 @t248))))
% 0.47/0.65  (define @t602 () (and @t256 (= tptp.e4 @t255) (not (= tptp.e1 @t253))))
% 0.47/0.65  (define @t603 () (and @t261 (= tptp.e4 @t260) (not (= tptp.e0 @t258))))
% 0.47/0.65  (define @t604 () (and @t246 (= tptp.e3 @t265) (not (= tptp.e4 @t263))))
% 0.47/0.65  (define @t605 () (and @t276 (= tptp.e3 @t275) (not (= tptp.e2 @t273))))
% 0.47/0.65  (define @t606 () (and @t287 (= tptp.e3 @t286) (not (= tptp.e0 @t284))))
% 0.47/0.65  (define @t607 () (and @t251 (= tptp.e2 @t291) (not (= tptp.e4 @t289))))
% 0.47/0.65  (define @t608 () (and @t276 (= tptp.e2 @t296) (not (= tptp.e3 @t294))))
% 0.47/0.65  (define @t609 () (and @t307 (= tptp.e2 @t306) (not (= tptp.e1 @t304))))
% 0.47/0.65  (define @t610 () (and @t312 (= tptp.e2 @t311) (not (= tptp.e0 @t309))))
% 0.47/0.65  (define @t611 () (and @t256 (= tptp.e1 @t316) (not (= tptp.e4 @t314))))
% 0.47/0.65  (define @t612 () (and @t282 (= tptp.e1 @t321) (not (= tptp.e3 @t319))))
% 0.47/0.65  (define @t613 () (and @t307 (= tptp.e1 @t326) (not (= tptp.e2 @t324))))
% 0.47/0.65  (define @t614 () (and @t337 (= tptp.e1 @t336) (not (= tptp.e0 @t334))))
% 0.47/0.65  (define @t615 () (and @t261 (= tptp.e0 @t341) (not (= tptp.e4 @t339))))
% 0.47/0.65  (define @t616 () (and @t287 (= tptp.e0 @t346) (not (= tptp.e3 @t344))))
% 0.47/0.65  (define @t617 () (and @t312 (= tptp.e0 @t351) (not (= tptp.e2 @t349))))
% 0.47/0.65  (define @t618 () (and @t337 (= tptp.e0 @t356) (not (= tptp.e1 @t354))))
% 0.47/0.65  (define @t619 () (or @t618 @t617 @t616 @t615 @t614 @t613 @t612 @t611 @t610 @t609 @t608 @t607 @t606 @t371 @t605 @t604 @t603 @t602 @t601 @t600))
% 0.47/0.65  (define @t620 () (= tptp.e4 @t238))
% 0.47/0.65  (define @t621 () (= tptp.e3 @t268))
% 0.47/0.65  (define @t622 () (= tptp.e2 @t299))
% 0.47/0.65  (define @t623 () (= tptp.e1 @t329))
% 0.47/0.65  (define @t624 () (= tptp.e0 @t359))
% 0.47/0.65  (assume @p1 (and (not (= tptp.e0 tptp.e1)) (not (= tptp.e0 tptp.e2)) (not (= tptp.e0 tptp.e3)) (not (= tptp.e0 tptp.e4)) (not (= tptp.e1 tptp.e2)) (not (= tptp.e1 tptp.e3)) (not (= tptp.e1 tptp.e4)) (not (= tptp.e2 tptp.e3)) (not (= tptp.e2 tptp.e4)) (not (= tptp.e3 tptp.e4))))
% 0.47/0.65  (assume @p2 (and @t50 @t48 @t46 @t44 @t42 @t40 @t38 @t36 @t34 @t32 @t30 @t28 @t26 @t24 @t22 @t20 @t18 @t16 @t14 @t12 @t10 @t8 @t6 @t4 @t2))
% 0.47/0.65  (assume @p3 @t51)
% 0.47/0.65  (assume @p4 @t366)
% 0.47/0.65  (assume @p5 true)
% 0.47/0.65  (step @p6 :rule refl :args (tptp.e1))
% 0.47/0.65  (step @p7 :rule and_elim :premises (@p2) :args (16))
% 0.47/0.65  (step @p8 :rule symm :premises (@p7))
% 0.47/0.65  (step @p9 :rule cong :premises (@p8 @p6) :args (@t7))
% 0.47/0.65  (step @p10 :rule and_elim :premises (@p2) :args (21))
% 0.47/0.65  (step @p11 :rule symm :premises (@p10))
% 0.47/0.65  (step @p12 :rule trans :premises (@p11 @p9))
% 0.47/0.65  (step @p13 :rule and_elim :premises (@p1) :args (4))
% 0.47/0.65  (step @p14 :rule false_intro :premises (@p13))
% 0.47/0.65  (step @p15 :rule and_elim :premises (@p2) :args (6))
% 0.47/0.65  (step @p16 :rule symm :premises (@p15))
% 0.47/0.65  (step @p17 :rule and_elim :premises (@p2) :args (23))
% 0.47/0.65  (step @p18 :rule refl :args (tptp.e3))
% 0.47/0.65  (step @p19 :rule cong :premises (@p7 @p18) :args (@t278))
% 0.47/0.65  (step @p20 :rule trans :premises (@p19 @p17 @p16))
% 0.47/0.65  (step @p21 :rule symm :premises (@p20))
% 0.47/0.65  (step @p22 :rule trans :premises (@p16 @p21))
% 0.47/0.65  (step @p23 :rule symm :premises (@p22))
% 0.47/0.65  (step @p24 :rule cong :premises (@p6 @p23) :args (@t367))
% 0.47/0.65  (step @p25 :rule trans :premises (@p24 @p14))
% 0.47/0.65  (step @p26 :rule false_elim :premises (@p25))
% 0.47/0.65  (step @p27 :rule and_elim :premises (@p1) :args (3))
% 0.47/0.65  (step @p28 :rule false_intro :premises (@p27))
% 0.47/0.65  (step @p29 :rule and_elim :premises (@p2) :args (8))
% 0.47/0.65  (step @p30 :rule cong :premises (@p29 @p7) :args (@t281))
% 0.47/0.65  (step @p31 :rule trans :premises (@p30 @p28))
% 0.47/0.65  (step @p32 :rule false_elim :premises (@p31))
% 0.47/0.65  (step @p33 :rule bool-double-not-elim :args (@t367))
% 0.47/0.65  (step @p34 :rule refl :args (@t369))
% 0.47/0.65  (step @p35 :rule bool-double-not-elim :args (@t281))
% 0.47/0.65  (step @p36 :rule refl :args (@t371))
% 0.47/0.65  (step @p37 :rule nary_cong :premises (@p36 @p35 @p34 @p33) :args ((or @t371 (not @t282) @t369 (not @t370))))
% 0.47/0.65  (step @p38 :rule cnf_and_neg :args (@t371))
% 0.47/0.65  (step @p39 :rule eq_resolve :premises (@p38 @p37))
% 0.47/0.65  (step @p40 :rule reordering :premises (@p39) :args ((or @t281 @t367 @t371 @t369)))
% 0.47/0.65  (step @p41 :rule chain_m_resolution :premises (@p40 @p32 @p26 @p12) :args (@t371 (@list true true false) (@list @t281 @t367 @t368)))
% 0.47/0.65  (step @p42 :rule and_elim :premises (@p2) :args (4))
% 0.47/0.65  (step @p43 :rule symm :premises (@p42))
% 0.47/0.65  (step @p44 :rule cnf_or_neg :args (@t377 0))
% 0.47/0.65  (step @p45 :rule chain_m_resolution :premises (@p44 @p43) :args (@t377 @t378 @t379))
% 0.47/0.65  (step @p46 :rule and_elim :premises (@p2) :args (20))
% 0.47/0.65  (step @p47 :rule symm :premises (@p46))
% 0.47/0.65  (step @p48 :rule cnf_or_neg :args (@t384 0))
% 0.47/0.65  (step @p49 :rule chain_m_resolution :premises (@p48 @p47) :args (@t384 @t378 @t385))
% 0.47/0.65  (step @p50 :rule and_elim :premises (@p2) :args (9))
% 0.47/0.65  (step @p51 :rule symm :premises (@p50))
% 0.47/0.65  (step @p52 :rule cnf_or_neg :args (@t391 1))
% 0.47/0.65  (step @p53 :rule chain_m_resolution :premises (@p52 @p51) :args (@t391 @t378 @t392))
% 0.47/0.65  (step @p54 :rule cnf_or_neg :args (@t397 1))
% 0.47/0.65  (step @p55 :rule chain_m_resolution :premises (@p54 @p11) :args (@t397 @t378 @t398))
% 0.47/0.65  (step @p56 :rule and_elim :premises (@p2) :args (19))
% 0.47/0.65  (step @p57 :rule symm :premises (@p56))
% 0.47/0.65  (step @p58 :rule cnf_or_neg :args (@t404 3))
% 0.47/0.65  (step @p59 :rule chain_m_resolution :premises (@p58 @p57) :args (@t404 @t378 @t405))
% 0.47/0.65  (step @p60 :rule symm :premises (@p17))
% 0.47/0.65  (step @p61 :rule cnf_or_neg :args (@t410 3))
% 0.47/0.65  (step @p62 :rule chain_m_resolution :premises (@p61 @p60) :args (@t410 @t378 @t411))
% 0.47/0.65  (step @p63 :rule and_elim :premises (@p2) :args (14))
% 0.47/0.65  (step @p64 :rule symm :premises (@p63))
% 0.47/0.65  (step @p65 :rule cnf_or_neg :args (@t417 2))
% 0.47/0.65  (step @p66 :rule chain_m_resolution :premises (@p65 @p64) :args (@t417 @t378 @t418))
% 0.47/0.65  (step @p67 :rule and_elim :premises (@p2) :args (22))
% 0.47/0.65  (step @p68 :rule symm :premises (@p67))
% 0.47/0.65  (step @p69 :rule cnf_or_neg :args (@t423 2))
% 0.47/0.65  (step @p70 :rule chain_m_resolution :premises (@p69 @p68) :args (@t423 @t378 @t424))
% 0.47/0.65  (step @p71 :rule and_elim :premises (@p2) :args (24))
% 0.47/0.65  (step @p72 :rule symm :premises (@p71))
% 0.47/0.65  (step @p73 :rule cnf_or_neg :args (@t430 4))
% 0.47/0.65  (step @p74 :rule chain_m_resolution :premises (@p73 @p72) :args (@t430 @t378 @t431))
% 0.47/0.65  (step @p75 :rule cnf_or_neg :args (@t436 4))
% 0.47/0.65  (step @p76 :rule chain_m_resolution :premises (@p75 @p72) :args (@t436 @t378 @t431))
% 0.47/0.65  (step @p77 :rule and_elim :premises (@p2) :args (13))
% 0.47/0.65  (step @p78 :rule symm :premises (@p77))
% 0.47/0.65  (step @p79 :rule cnf_or_neg :args (@t441 2))
% 0.47/0.65  (step @p80 :rule chain_m_resolution :premises (@p79 @p78) :args (@t441 @t378 @t442))
% 0.47/0.65  (step @p81 :rule cnf_or_neg :args (@t446 1))
% 0.47/0.65  (step @p82 :rule chain_m_resolution :premises (@p81 @p8) :args (@t446 @t378 @t447))
% 0.47/0.65  (step @p83 :rule and_elim :premises (@p2) :args (3))
% 0.47/0.65  (step @p84 :rule symm :premises (@p83))
% 0.47/0.65  (step @p85 :rule cnf_or_neg :args (@t452 0))
% 0.47/0.65  (step @p86 :rule chain_m_resolution :premises (@p85 @p84) :args (@t452 @t378 @t453))
% 0.47/0.65  (step @p87 :rule and_elim :premises (@p2) :args (15))
% 0.47/0.65  (step @p88 :rule symm :premises (@p87))
% 0.47/0.65  (step @p89 :rule cnf_or_neg :args (@t457 0))
% 0.47/0.65  (step @p90 :rule chain_m_resolution :premises (@p89 @p88) :args (@t457 @t378 @t458))
% 0.47/0.65  (step @p91 :rule cnf_or_neg :args (@t463 4))
% 0.47/0.65  (step @p92 :rule chain_m_resolution :premises (@p91 @p60) :args (@t463 @t378 @t411))
% 0.47/0.65  (step @p93 :rule cnf_or_neg :args (@t467 4))
% 0.47/0.65  (step @p94 :rule chain_m_resolution :premises (@p93 @p57) :args (@t467 @t378 @t405))
% 0.47/0.65  (step @p95 :rule and_elim :premises (@p2) :args (18))
% 0.47/0.65  (step @p96 :rule symm :premises (@p95))
% 0.47/0.65  (step @p97 :rule cnf_or_neg :args (@t472 3))
% 0.47/0.65  (step @p98 :rule chain_m_resolution :premises (@p97 @p96) :args (@t472 @t378 @t473))
% 0.47/0.65  (step @p99 :rule cnf_or_neg :args (@t477 3))
% 0.47/0.65  (step @p100 :rule chain_m_resolution :premises (@p99 @p96) :args (@t477 @t378 @t473))
% 0.47/0.65  (step @p101 :rule symm :premises (@p29))
% 0.47/0.65  (step @p102 :rule cnf_or_neg :args (@t482 1))
% 0.47/0.65  (step @p103 :rule chain_m_resolution :premises (@p102 @p101) :args (@t482 @t378 @t483))
% 0.47/0.65  (step @p104 :rule and_elim :premises (@p2) :args (17))
% 0.47/0.65  (step @p105 :rule symm :premises (@p104))
% 0.47/0.65  (step @p106 :rule cnf_or_neg :args (@t487 2))
% 0.47/0.65  (step @p107 :rule chain_m_resolution :premises (@p106 @p105) :args (@t487 @t378 @t488))
% 0.47/0.65  (step @p108 :rule and_elim :premises (@p2) :args (7))
% 0.47/0.65  (step @p109 :rule symm :premises (@p108))
% 0.47/0.65  (step @p110 :rule cnf_or_neg :args (@t492 1))
% 0.47/0.65  (step @p111 :rule chain_m_resolution :premises (@p110 @p109) :args (@t492 @t378 @t493))
% 0.47/0.65  (step @p112 :rule cnf_or_neg :args (@t496 3))
% 0.47/0.65  (step @p113 :rule chain_m_resolution :premises (@p112 @p78) :args (@t496 @t378 @t442))
% 0.47/0.65  (step @p114 :rule and_elim :premises (@p2) :args (12))
% 0.47/0.65  (step @p115 :rule symm :premises (@p114))
% 0.47/0.65  (step @p116 :rule cnf_or_neg :args (@t500 2))
% 0.47/0.65  (step @p117 :rule chain_m_resolution :premises (@p116 @p115) :args (@t500 @t378 @t501))
% 0.47/0.65  (step @p118 :rule cnf_or_neg :args (@t504 2))
% 0.47/0.65  (step @p119 :rule chain_m_resolution :premises (@p118 @p115) :args (@t504 @t378 @t501))
% 0.47/0.65  (step @p120 :rule and_elim :premises (@p2) :args (2))
% 0.47/0.65  (step @p121 :rule symm :premises (@p120))
% 0.47/0.65  (step @p122 :rule cnf_or_neg :args (@t508 0))
% 0.47/0.65  (step @p123 :rule chain_m_resolution :premises (@p122 @p121) :args (@t508 @t378 @t509))
% 0.47/0.65  (step @p124 :rule and_elim :premises (@p2) :args (10))
% 0.47/0.65  (step @p125 :rule symm :premises (@p124))
% 0.47/0.65  (step @p126 :rule cnf_or_neg :args (@t512 0))
% 0.47/0.65  (step @p127 :rule chain_m_resolution :premises (@p126 @p125) :args (@t512 @t378 @t513))
% 0.47/0.65  (step @p128 :rule cnf_or_neg :args (@t517 4))
% 0.47/0.65  (step @p129 :rule chain_m_resolution :premises (@p128 @p68) :args (@t517 @t378 @t424))
% 0.47/0.65  (step @p130 :rule cnf_or_neg :args (@t520 4))
% 0.47/0.65  (step @p131 :rule chain_m_resolution :premises (@p130 @p64) :args (@t520 @t378 @t418))
% 0.47/0.65  (step @p132 :rule cnf_or_neg :args (@t524 3))
% 0.47/0.65  (step @p133 :rule chain_m_resolution :premises (@p132 @p105) :args (@t524 @t378 @t488))
% 0.47/0.65  (step @p134 :rule and_elim :premises (@p2) :args (11))
% 0.47/0.65  (step @p135 :rule symm :premises (@p134))
% 0.47/0.65  (step @p136 :rule cnf_or_neg :args (@t527 1))
% 0.47/0.65  (step @p137 :rule chain_m_resolution :premises (@p136 @p135) :args (@t527 @t378 @t528))
% 0.47/0.65  (step @p138 :rule cnf_or_neg :args (@t531 3))
% 0.47/0.65  (step @p139 :rule chain_m_resolution :premises (@p138 @p8) :args (@t531 @t378 @t447))
% 0.47/0.65  (step @p140 :rule cnf_or_neg :args (@t533 2))
% 0.47/0.65  (step @p141 :rule chain_m_resolution :premises (@p140 @p109) :args (@t533 @t378 @t493))
% 0.47/0.65  (step @p142 :rule cnf_or_neg :args (@t536 4))
% 0.47/0.65  (step @p143 :rule chain_m_resolution :premises (@p142 @p11) :args (@t536 @t378 @t398))
% 0.47/0.65  (step @p144 :rule cnf_or_neg :args (@t538 4))
% 0.47/0.65  (step @p145 :rule chain_m_resolution :premises (@p144 @p51) :args (@t538 @t378 @t392))
% 0.47/0.65  (step @p146 :rule cnf_or_neg :args (@t541 1))
% 0.47/0.65  (step @p147 :rule chain_m_resolution :premises (@p146 @p16) :args (@t541 @t378 @t542))
% 0.47/0.65  (step @p148 :rule cnf_or_neg :args (@t544 1))
% 0.47/0.65  (step @p149 :rule chain_m_resolution :premises (@p148 @p16) :args (@t544 @t378 @t542))
% 0.47/0.65  (step @p150 :rule and_elim :premises (@p2) :args (1))
% 0.47/0.65  (step @p151 :rule symm :premises (@p150))
% 0.47/0.65  (step @p152 :rule cnf_or_neg :args (@t547 0))
% 0.47/0.65  (step @p153 :rule chain_m_resolution :premises (@p152 @p151) :args (@t547 @t378 @t548))
% 0.47/0.65  (step @p154 :rule and_elim :premises (@p2) :args (5))
% 0.47/0.65  (step @p155 :rule symm :premises (@p154))
% 0.47/0.65  (step @p156 :rule cnf_or_neg :args (@t550 0))
% 0.47/0.65  (step @p157 :rule chain_m_resolution :premises (@p156 @p155) :args (@t550 @t378 @t551))
% 0.47/0.65  (step @p158 :rule cnf_or_neg :args (@t554 2))
% 0.47/0.65  (step @p159 :rule chain_m_resolution :premises (@p158 @p135) :args (@t554 @t378 @t528))
% 0.47/0.65  (step @p160 :rule cnf_or_neg :args (@t556 3))
% 0.47/0.65  (step @p161 :rule chain_m_resolution :premises (@p160 @p101) :args (@t556 @t378 @t483))
% 0.47/0.65  (step @p162 :rule cnf_or_neg :args (@t558 4))
% 0.47/0.65  (step @p163 :rule chain_m_resolution :premises (@p162 @p47) :args (@t558 @t378 @t385))
% 0.47/0.65  (step @p164 :rule cnf_or_neg :args (@t559 4))
% 0.47/0.65  (step @p165 :rule chain_m_resolution :premises (@p164 @p43) :args (@t559 @t378 @t379))
% 0.47/0.65  (step @p166 :rule cnf_or_neg :args (@t561 3))
% 0.47/0.65  (step @p167 :rule chain_m_resolution :premises (@p166 @p88) :args (@t561 @t378 @t458))
% 0.47/0.65  (step @p168 :rule cnf_or_neg :args (@t562 3))
% 0.47/0.65  (step @p169 :rule chain_m_resolution :premises (@p168 @p84) :args (@t562 @t378 @t453))
% 0.47/0.65  (step @p170 :rule cnf_or_neg :args (@t564 2))
% 0.47/0.65  (step @p171 :rule chain_m_resolution :premises (@p170 @p125) :args (@t564 @t378 @t513))
% 0.47/0.65  (step @p172 :rule cnf_or_neg :args (@t565 2))
% 0.47/0.65  (step @p173 :rule chain_m_resolution :premises (@p172 @p121) :args (@t565 @t378 @t509))
% 0.47/0.65  (step @p174 :rule cnf_or_neg :args (@t567 1))
% 0.47/0.65  (step @p175 :rule chain_m_resolution :premises (@p174 @p155) :args (@t567 @t378 @t551))
% 0.47/0.65  (step @p176 :rule cnf_or_neg :args (@t568 1))
% 0.47/0.65  (step @p177 :rule chain_m_resolution :premises (@p176 @p151) :args (@t568 @t378 @t548))
% 0.47/0.65  (step @p178 :rule and_elim :premises (@p2) :args (0))
% 0.47/0.65  (step @p179 :rule symm :premises (@p178))
% 0.47/0.65  (step @p180 :rule cnf_or_neg :args (@t570 0))
% 0.47/0.65  (step @p181 :rule chain_m_resolution :premises (@p180 @p179) :args (@t570 @t378 @t571))
% 0.47/0.65  (step @p182 :rule cnf_or_neg :args (@t572 0))
% 0.47/0.65  (step @p183 :rule chain_m_resolution :premises (@p182 @p179) :args (@t572 @t378 @t571))
% 0.47/0.65  (step @p184 :rule symm :premises (@p3))
% 0.47/0.65  (step @p185 :rule cnf_or_neg :args (@t574 0))
% 0.47/0.65  (step @p186 :rule chain_m_resolution :premises (@p185 @p184) :args (@t574 @t378 (@list @t573)))
% 0.47/0.65  (step @p187 :rule refl :args (tptp.e4))
% 0.47/0.65  (step @p188 :rule cong :premises (@p187 @p184) :args (@t9))
% 0.47/0.65  (step @p189 :rule trans :premises (@p47 @p188))
% 0.47/0.65  (step @p190 :rule cong :premises (@p184 @p187) :args (@t41))
% 0.47/0.65  (step @p191 :rule trans :premises (@p43 @p190))
% 0.47/0.65  (step @p192 :rule cong :premises (@p18 @p184) :args (@t19))
% 0.47/0.65  (step @p193 :rule trans :premises (@p88 @p192))
% 0.47/0.65  (step @p194 :rule cong :premises (@p184 @p18) :args (@t43))
% 0.47/0.65  (step @p195 :rule trans :premises (@p84 @p194))
% 0.47/0.65  (step @p196 :rule refl :args (tptp.e2))
% 0.47/0.65  (step @p197 :rule cong :premises (@p196 @p184) :args (@t29))
% 0.47/0.65  (step @p198 :rule trans :premises (@p125 @p197))
% 0.47/0.65  (step @p199 :rule cong :premises (@p184 @p196) :args (@t45))
% 0.47/0.65  (step @p200 :rule trans :premises (@p121 @p199))
% 0.47/0.65  (step @p201 :rule cong :premises (@p6 @p184) :args (@t39))
% 0.47/0.65  (step @p202 :rule trans :premises (@p155 @p201))
% 0.47/0.65  (step @p203 :rule cong :premises (@p184 @p6) :args (@t47))
% 0.47/0.65  (step @p204 :rule trans :premises (@p151 @p203))
% 0.47/0.65  (step @p205 :rule refl :args (tptp.e0))
% 0.47/0.65  (step @p206 :rule cong :premises (@p205 @p184) :args (@t49))
% 0.47/0.65  (step @p207 :rule trans :premises (@p179 @p206))
% 0.47/0.65  (step @p208 :rule cong :premises (@p184 @p205) :args (@t49))
% 0.47/0.65  (step @p209 :rule trans :premises (@p179 @p208))
% 0.47/0.65  (step @p210 :rule cnf_or_neg :args (@t575 0))
% 0.47/0.65  (step @p211 :rule chain_m_resolution :premises (@p210 @p72) :args (@t575 @t378 @t431))
% 0.47/0.65  (step @p212 :rule cnf_or_neg :args (@t576 2))
% 0.47/0.65  (step @p213 :rule chain_m_resolution :premises (@p212 @p60) :args (@t576 @t378 @t411))
% 0.47/0.65  (step @p214 :rule cnf_or_neg :args (@t577 1))
% 0.47/0.65  (step @p215 :rule chain_m_resolution :premises (@p214 @p68) :args (@t577 @t378 @t424))
% 0.47/0.65  (step @p216 :rule cnf_or_neg :args (@t578 3))
% 0.47/0.65  (step @p217 :rule chain_m_resolution :premises (@p216 @p11) :args (@t578 @t378 @t398))
% 0.47/0.65  (step @p218 :rule cnf_or_neg :args (@t579 4))
% 0.47/0.65  (step @p219 :rule chain_m_resolution :premises (@p218 @p47) :args (@t579 @t378 @t385))
% 0.47/0.65  (step @p220 :rule cnf_or_neg :args (@t580 2))
% 0.47/0.65  (step @p221 :rule chain_m_resolution :premises (@p220 @p57) :args (@t580 @t378 @t405))
% 0.47/0.65  (step @p222 :rule cnf_or_neg :args (@t581 1))
% 0.47/0.65  (step @p223 :rule chain_m_resolution :premises (@p222 @p96) :args (@t581 @t378 @t473))
% 0.47/0.65  (step @p224 :rule cnf_or_neg :args (@t582 0))
% 0.47/0.65  (step @p225 :rule chain_m_resolution :premises (@p224 @p105) :args (@t582 @t378 @t488))
% 0.47/0.65  (step @p226 :rule cnf_or_neg :args (@t583 4))
% 0.47/0.65  (step @p227 :rule chain_m_resolution :premises (@p226 @p8) :args (@t583 @t378 @t447))
% 0.47/0.65  (step @p228 :rule cnf_or_neg :args (@t584 3))
% 0.47/0.65  (step @p229 :rule chain_m_resolution :premises (@p228 @p88) :args (@t584 @t378 @t458))
% 0.47/0.65  (step @p230 :rule cnf_or_neg :args (@t585 1))
% 0.47/0.65  (step @p231 :rule chain_m_resolution :premises (@p230 @p64) :args (@t585 @t378 @t418))
% 0.47/0.65  (step @p232 :rule cnf_or_neg :args (@t586 4))
% 0.47/0.65  (step @p233 :rule chain_m_resolution :premises (@p232 @p78) :args (@t586 @t378 @t442))
% 0.47/0.65  (step @p234 :rule cnf_or_neg :args (@t587 3))
% 0.47/0.65  (step @p235 :rule chain_m_resolution :premises (@p234 @p115) :args (@t587 @t378 @t501))
% 0.47/0.65  (step @p236 :rule cnf_or_neg :args (@t588 0))
% 0.47/0.65  (step @p237 :rule chain_m_resolution :premises (@p236 @p135) :args (@t588 @t378 @t528))
% 0.47/0.65  (step @p238 :rule cnf_or_neg :args (@t589 2))
% 0.47/0.65  (step @p239 :rule chain_m_resolution :premises (@p238 @p125) :args (@t589 @t378 @t513))
% 0.47/0.65  (step @p240 :rule cnf_or_neg :args (@t590 3))
% 0.47/0.65  (step @p241 :rule chain_m_resolution :premises (@p240 @p51) :args (@t590 @t378 @t392))
% 0.47/0.65  (step @p242 :rule cnf_or_neg :args (@t591 0))
% 0.47/0.65  (step @p243 :rule chain_m_resolution :premises (@p242 @p101) :args (@t591 @t378 @t483))
% 0.47/0.65  (step @p244 :rule cnf_or_neg :args (@t592 4))
% 0.47/0.65  (step @p245 :rule chain_m_resolution :premises (@p244 @p109) :args (@t592 @t378 @t493))
% 0.47/0.65  (step @p246 :rule cnf_or_neg :args (@t593 2))
% 0.47/0.65  (step @p247 :rule chain_m_resolution :premises (@p246 @p16) :args (@t593 @t378 @t542))
% 0.47/0.65  (step @p248 :rule cnf_or_neg :args (@t594 1))
% 0.47/0.65  (step @p249 :rule chain_m_resolution :premises (@p248 @p155) :args (@t594 @t378 @t551))
% 0.47/0.65  (step @p250 :rule cnf_or_neg :args (@t595 4))
% 0.47/0.65  (step @p251 :rule chain_m_resolution :premises (@p250 @p43) :args (@t595 @t378 @t379))
% 0.47/0.65  (step @p252 :rule cnf_or_neg :args (@t596 3))
% 0.47/0.65  (step @p253 :rule chain_m_resolution :premises (@p252 @p84) :args (@t596 @t378 @t453))
% 0.47/0.65  (step @p254 :rule cnf_or_neg :args (@t597 2))
% 0.47/0.65  (step @p255 :rule chain_m_resolution :premises (@p254 @p121) :args (@t597 @t378 @t509))
% 0.47/0.65  (step @p256 :rule cnf_or_neg :args (@t598 1))
% 0.47/0.65  (step @p257 :rule chain_m_resolution :premises (@p256 @p151) :args (@t598 @t378 @t548))
% 0.47/0.65  (step @p258 :rule cnf_or_neg :args (@t599 0))
% 0.47/0.65  (step @p259 :rule chain_m_resolution :premises (@p258 @p179) :args (@t599 @t378 @t571))
% 0.47/0.65  (step @p260 :rule eq-symm :args (@t1 tptp.e4))
% 0.47/0.65  (step @p261 :rule eq-symm :args (@t11 tptp.e4))
% 0.47/0.65  (step @p262 :rule eq-symm :args (@t21 tptp.e4))
% 0.47/0.65  (step @p263 :rule eq-symm :args (@t31 tptp.e4))
% 0.47/0.65  (step @p264 :rule eq-symm :args (@t41 tptp.e4))
% 0.47/0.65  (step @p265 :rule nary_cong :premises (@p264 @p263 @p262 @p261 @p260) :args (@t56))
% 0.47/0.65  (step @p266 :rule eq-symm :args (@t3 tptp.e4))
% 0.47/0.65  (step @p267 :rule eq-symm :args (@t5 tptp.e4))
% 0.47/0.65  (step @p268 :rule eq-symm :args (@t7 tptp.e4))
% 0.47/0.65  (step @p269 :rule eq-symm :args (@t9 tptp.e4))
% 0.47/0.65  (step @p270 :rule nary_cong :premises (@p269 @p268 @p267 @p266 @p260) :args (@t60))
% 0.47/0.65  (step @p271 :rule eq-symm :args (@t1 tptp.e3))
% 0.47/0.65  (step @p272 :rule eq-symm :args (@t11 tptp.e3))
% 0.47/0.65  (step @p273 :rule eq-symm :args (@t21 tptp.e3))
% 0.47/0.65  (step @p274 :rule eq-symm :args (@t31 tptp.e3))
% 0.47/0.65  (step @p275 :rule eq-symm :args (@t41 tptp.e3))
% 0.47/0.65  (step @p276 :rule nary_cong :premises (@p275 @p274 @p273 @p272 @p271) :args (@t65))
% 0.47/0.65  (step @p277 :rule eq-symm :args (@t3 tptp.e3))
% 0.47/0.65  (step @p278 :rule eq-symm :args (@t5 tptp.e3))
% 0.47/0.65  (step @p279 :rule eq-symm :args (@t7 tptp.e3))
% 0.47/0.65  (step @p280 :rule eq-symm :args (@t9 tptp.e3))
% 0.47/0.65  (step @p281 :rule nary_cong :premises (@p280 @p279 @p278 @p277 @p271) :args (@t69))
% 0.47/0.65  (step @p282 :rule eq-symm :args (@t1 tptp.e2))
% 0.47/0.65  (step @p283 :rule eq-symm :args (@t11 tptp.e2))
% 0.47/0.65  (step @p284 :rule eq-symm :args (@t21 tptp.e2))
% 0.47/0.65  (step @p285 :rule eq-symm :args (@t31 tptp.e2))
% 0.47/0.65  (step @p286 :rule eq-symm :args (@t41 tptp.e2))
% 0.47/0.65  (step @p287 :rule nary_cong :premises (@p286 @p285 @p284 @p283 @p282) :args (@t74))
% 0.47/0.65  (step @p288 :rule eq-symm :args (@t3 tptp.e2))
% 0.47/0.65  (step @p289 :rule eq-symm :args (@t5 tptp.e2))
% 0.47/0.65  (step @p290 :rule eq-symm :args (@t7 tptp.e2))
% 0.47/0.65  (step @p291 :rule eq-symm :args (@t9 tptp.e2))
% 0.47/0.65  (step @p292 :rule nary_cong :premises (@p291 @p290 @p289 @p288 @p282) :args (@t78))
% 0.47/0.65  (step @p293 :rule eq-symm :args (@t1 tptp.e1))
% 0.47/0.65  (step @p294 :rule eq-symm :args (@t11 tptp.e1))
% 0.47/0.65  (step @p295 :rule eq-symm :args (@t21 tptp.e1))
% 0.47/0.65  (step @p296 :rule eq-symm :args (@t31 tptp.e1))
% 0.47/0.65  (step @p297 :rule eq-symm :args (@t41 tptp.e1))
% 0.47/0.65  (step @p298 :rule nary_cong :premises (@p297 @p296 @p295 @p294 @p293) :args (@t83))
% 0.47/0.65  (step @p299 :rule eq-symm :args (@t3 tptp.e1))
% 0.47/0.65  (step @p300 :rule eq-symm :args (@t5 tptp.e1))
% 0.47/0.65  (step @p301 :rule eq-symm :args (@t7 tptp.e1))
% 0.47/0.65  (step @p302 :rule eq-symm :args (@t9 tptp.e1))
% 0.47/0.65  (step @p303 :rule nary_cong :premises (@p302 @p301 @p300 @p299 @p293) :args (@t87))
% 0.47/0.65  (step @p304 :rule eq-symm :args (@t1 tptp.e0))
% 0.47/0.65  (step @p305 :rule eq-symm :args (@t11 tptp.e0))
% 0.47/0.65  (step @p306 :rule eq-symm :args (@t21 tptp.e0))
% 0.47/0.65  (step @p307 :rule eq-symm :args (@t31 tptp.e0))
% 0.47/0.65  (step @p308 :rule eq-symm :args (@t41 tptp.e0))
% 0.47/0.65  (step @p309 :rule nary_cong :premises (@p308 @p307 @p306 @p305 @p304) :args (@t92))
% 0.47/0.65  (step @p310 :rule eq-symm :args (@t3 tptp.e0))
% 0.47/0.65  (step @p311 :rule eq-symm :args (@t5 tptp.e0))
% 0.47/0.65  (step @p312 :rule eq-symm :args (@t7 tptp.e0))
% 0.47/0.65  (step @p313 :rule eq-symm :args (@t9 tptp.e0))
% 0.47/0.65  (step @p314 :rule nary_cong :premises (@p313 @p312 @p311 @p310 @p304) :args (@t97))
% 0.47/0.65  (step @p315 :rule eq-symm :args (@t13 tptp.e4))
% 0.47/0.65  (step @p316 :rule eq-symm :args (@t23 tptp.e4))
% 0.47/0.65  (step @p317 :rule eq-symm :args (@t33 tptp.e4))
% 0.47/0.65  (step @p318 :rule eq-symm :args (@t43 tptp.e4))
% 0.47/0.65  (step @p319 :rule nary_cong :premises (@p318 @p317 @p316 @p315 @p266) :args (@t101))
% 0.47/0.65  (step @p320 :rule eq-symm :args (@t15 tptp.e4))
% 0.47/0.65  (step @p321 :rule eq-symm :args (@t17 tptp.e4))
% 0.47/0.65  (step @p322 :rule eq-symm :args (@t19 tptp.e4))
% 0.47/0.65  (step @p323 :rule nary_cong :premises (@p322 @p321 @p320 @p315 @p261) :args (@t104))
% 0.47/0.65  (step @p324 :rule eq-symm :args (@t13 tptp.e3))
% 0.47/0.65  (step @p325 :rule eq-symm :args (@t23 tptp.e3))
% 0.47/0.65  (step @p326 :rule eq-symm :args (@t33 tptp.e3))
% 0.47/0.65  (step @p327 :rule eq-symm :args (@t43 tptp.e3))
% 0.47/0.65  (step @p328 :rule nary_cong :premises (@p327 @p326 @p325 @p324 @p277) :args (@t108))
% 0.47/0.65  (step @p329 :rule eq-symm :args (@t15 tptp.e3))
% 0.47/0.65  (step @p330 :rule eq-symm :args (@t17 tptp.e3))
% 0.47/0.65  (step @p331 :rule eq-symm :args (@t19 tptp.e3))
% 0.47/0.65  (step @p332 :rule nary_cong :premises (@p331 @p330 @p329 @p324 @p272) :args (@t111))
% 0.47/0.65  (step @p333 :rule eq-symm :args (@t13 tptp.e2))
% 0.47/0.65  (step @p334 :rule eq-symm :args (@t23 tptp.e2))
% 0.47/0.65  (step @p335 :rule eq-symm :args (@t33 tptp.e2))
% 0.47/0.65  (step @p336 :rule eq-symm :args (@t43 tptp.e2))
% 0.47/0.65  (step @p337 :rule nary_cong :premises (@p336 @p335 @p334 @p333 @p288) :args (@t116))
% 0.47/0.65  (step @p338 :rule eq-symm :args (@t15 tptp.e2))
% 0.47/0.65  (step @p339 :rule eq-symm :args (@t17 tptp.e2))
% 0.47/0.65  (step @p340 :rule eq-symm :args (@t19 tptp.e2))
% 0.47/0.65  (step @p341 :rule nary_cong :premises (@p340 @p339 @p338 @p333 @p283) :args (@t120))
% 0.47/0.65  (step @p342 :rule eq-symm :args (@t13 tptp.e1))
% 0.47/0.65  (step @p343 :rule eq-symm :args (@t23 tptp.e1))
% 0.47/0.65  (step @p344 :rule eq-symm :args (@t33 tptp.e1))
% 0.47/0.65  (step @p345 :rule eq-symm :args (@t43 tptp.e1))
% 0.47/0.65  (step @p346 :rule nary_cong :premises (@p345 @p344 @p343 @p342 @p299) :args (@t124))
% 0.47/0.65  (step @p347 :rule eq-symm :args (@t15 tptp.e1))
% 0.47/0.65  (step @p348 :rule eq-symm :args (@t17 tptp.e1))
% 0.47/0.65  (step @p349 :rule eq-symm :args (@t19 tptp.e1))
% 0.47/0.65  (step @p350 :rule nary_cong :premises (@p349 @p348 @p347 @p342 @p294) :args (@t128))
% 0.47/0.65  (step @p351 :rule eq-symm :args (@t13 tptp.e0))
% 0.47/0.65  (step @p352 :rule eq-symm :args (@t23 tptp.e0))
% 0.47/0.65  (step @p353 :rule eq-symm :args (@t33 tptp.e0))
% 0.47/0.65  (step @p354 :rule eq-symm :args (@t43 tptp.e0))
% 0.47/0.65  (step @p355 :rule nary_cong :premises (@p354 @p353 @p352 @p351 @p310) :args (@t132))
% 0.47/0.65  (step @p356 :rule eq-symm :args (@t15 tptp.e0))
% 0.47/0.65  (step @p357 :rule eq-symm :args (@t17 tptp.e0))
% 0.47/0.65  (step @p358 :rule eq-symm :args (@t19 tptp.e0))
% 0.47/0.65  (step @p359 :rule nary_cong :premises (@p358 @p357 @p356 @p351 @p305) :args (@t135))
% 0.47/0.65  (step @p360 :rule eq-symm :args (@t25 tptp.e4))
% 0.47/0.65  (step @p361 :rule eq-symm :args (@t35 tptp.e4))
% 0.47/0.65  (step @p362 :rule eq-symm :args (@t45 tptp.e4))
% 0.47/0.65  (step @p363 :rule nary_cong :premises (@p362 @p361 @p360 @p320 @p267) :args (@t138))
% 0.47/0.65  (step @p364 :rule eq-symm :args (@t27 tptp.e4))
% 0.47/0.65  (step @p365 :rule eq-symm :args (@t29 tptp.e4))
% 0.47/0.65  (step @p366 :rule nary_cong :premises (@p365 @p364 @p360 @p316 @p262) :args (@t141))
% 0.47/0.65  (step @p367 :rule eq-symm :args (@t25 tptp.e3))
% 0.47/0.65  (step @p368 :rule eq-symm :args (@t35 tptp.e3))
% 0.47/0.65  (step @p369 :rule eq-symm :args (@t45 tptp.e3))
% 0.47/0.65  (step @p370 :rule nary_cong :premises (@p369 @p368 @p367 @p329 @p278) :args (@t144))
% 0.47/0.65  (step @p371 :rule eq-symm :args (@t27 tptp.e3))
% 0.47/0.65  (step @p372 :rule eq-symm :args (@t29 tptp.e3))
% 0.47/0.65  (step @p373 :rule nary_cong :premises (@p372 @p371 @p367 @p325 @p273) :args (@t147))
% 0.47/0.65  (step @p374 :rule eq-symm :args (@t25 tptp.e2))
% 0.47/0.65  (step @p375 :rule eq-symm :args (@t35 tptp.e2))
% 0.47/0.65  (step @p376 :rule eq-symm :args (@t45 tptp.e2))
% 0.47/0.65  (step @p377 :rule nary_cong :premises (@p376 @p375 @p374 @p338 @p289) :args (@t150))
% 0.47/0.65  (step @p378 :rule eq-symm :args (@t27 tptp.e2))
% 0.47/0.65  (step @p379 :rule eq-symm :args (@t29 tptp.e2))
% 0.47/0.65  (step @p380 :rule nary_cong :premises (@p379 @p378 @p374 @p334 @p284) :args (@t152))
% 0.47/0.65  (step @p381 :rule eq-symm :args (@t25 tptp.e1))
% 0.47/0.65  (step @p382 :rule eq-symm :args (@t35 tptp.e1))
% 0.47/0.65  (step @p383 :rule eq-symm :args (@t45 tptp.e1))
% 0.47/0.65  (step @p384 :rule nary_cong :premises (@p383 @p382 @p381 @p347 @p300) :args (@t156))
% 0.47/0.65  (step @p385 :rule eq-symm :args (@t27 tptp.e1))
% 0.47/0.65  (step @p386 :rule eq-symm :args (@t29 tptp.e1))
% 0.47/0.65  (step @p387 :rule nary_cong :premises (@p386 @p385 @p381 @p343 @p295) :args (@t159))
% 0.47/0.65  (step @p388 :rule eq-symm :args (@t25 tptp.e0))
% 0.47/0.65  (step @p389 :rule eq-symm :args (@t35 tptp.e0))
% 0.47/0.65  (step @p390 :rule eq-symm :args (@t45 tptp.e0))
% 0.47/0.65  (step @p391 :rule nary_cong :premises (@p390 @p389 @p388 @p356 @p311) :args (@t163))
% 0.47/0.65  (step @p392 :rule eq-symm :args (@t27 tptp.e0))
% 0.47/0.65  (step @p393 :rule eq-symm :args (@t29 tptp.e0))
% 0.47/0.65  (step @p394 :rule nary_cong :premises (@p393 @p392 @p388 @p352 @p306) :args (@t165))
% 0.47/0.65  (step @p395 :rule eq-symm :args (@t37 tptp.e4))
% 0.47/0.65  (step @p396 :rule eq-symm :args (@t47 tptp.e4))
% 0.47/0.65  (step @p397 :rule nary_cong :premises (@p396 @p395 @p364 @p321 @p268) :args (@t168))
% 0.47/0.65  (step @p398 :rule eq-symm :args (@t39 tptp.e4))
% 0.47/0.65  (step @p399 :rule nary_cong :premises (@p398 @p395 @p361 @p317 @p263) :args (@t170))
% 0.47/0.65  (step @p400 :rule eq-symm :args (@t37 tptp.e3))
% 0.47/0.65  (step @p401 :rule eq-symm :args (@t47 tptp.e3))
% 0.47/0.65  (step @p402 :rule nary_cong :premises (@p401 @p400 @p371 @p330 @p279) :args (@t173))
% 0.47/0.65  (step @p403 :rule eq-symm :args (@t39 tptp.e3))
% 0.47/0.65  (step @p404 :rule nary_cong :premises (@p403 @p400 @p368 @p326 @p274) :args (@t175))
% 0.47/0.65  (step @p405 :rule eq-symm :args (@t37 tptp.e2))
% 0.47/0.65  (step @p406 :rule eq-symm :args (@t47 tptp.e2))
% 0.47/0.65  (step @p407 :rule nary_cong :premises (@p406 @p405 @p378 @p339 @p290) :args (@t177))
% 0.47/0.65  (step @p408 :rule eq-symm :args (@t39 tptp.e2))
% 0.47/0.65  (step @p409 :rule nary_cong :premises (@p408 @p405 @p375 @p335 @p285) :args (@t179))
% 0.47/0.65  (step @p410 :rule eq-symm :args (@t37 tptp.e1))
% 0.47/0.65  (step @p411 :rule eq-symm :args (@t47 tptp.e1))
% 0.47/0.65  (step @p412 :rule nary_cong :premises (@p411 @p410 @p385 @p348 @p301) :args (@t181))
% 0.47/0.65  (step @p413 :rule eq-symm :args (@t39 tptp.e1))
% 0.47/0.65  (step @p414 :rule nary_cong :premises (@p413 @p410 @p382 @p344 @p296) :args (@t182))
% 0.47/0.65  (step @p415 :rule eq-symm :args (@t37 tptp.e0))
% 0.47/0.65  (step @p416 :rule eq-symm :args (@t47 tptp.e0))
% 0.47/0.65  (step @p417 :rule nary_cong :premises (@p416 @p415 @p392 @p357 @p312) :args (@t185))
% 0.47/0.65  (step @p418 :rule eq-symm :args (@t39 tptp.e0))
% 0.47/0.65  (step @p419 :rule nary_cong :premises (@p418 @p415 @p389 @p353 @p307) :args (@t187))
% 0.47/0.65  (step @p420 :rule eq-symm :args (@t49 tptp.e4))
% 0.47/0.65  (step @p421 :rule nary_cong :premises (@p420 @p398 @p365 @p322 @p269) :args (@t189))
% 0.47/0.65  (step @p422 :rule nary_cong :premises (@p420 @p396 @p362 @p318 @p264) :args (@t190))
% 0.47/0.65  (step @p423 :rule eq-symm :args (@t49 tptp.e3))
% 0.47/0.65  (step @p424 :rule nary_cong :premises (@p423 @p403 @p372 @p331 @p280) :args (@t192))
% 0.47/0.65  (step @p425 :rule nary_cong :premises (@p423 @p401 @p369 @p327 @p275) :args (@t193))
% 0.47/0.65  (step @p426 :rule eq-symm :args (@t49 tptp.e2))
% 0.47/0.65  (step @p427 :rule nary_cong :premises (@p426 @p408 @p379 @p340 @p291) :args (@t195))
% 0.47/0.65  (step @p428 :rule nary_cong :premises (@p426 @p406 @p376 @p336 @p286) :args (@t196))
% 0.47/0.65  (step @p429 :rule eq-symm :args (@t49 tptp.e1))
% 0.47/0.65  (step @p430 :rule nary_cong :premises (@p429 @p413 @p386 @p349 @p302) :args (@t198))
% 0.47/0.65  (step @p431 :rule nary_cong :premises (@p429 @p411 @p383 @p345 @p297) :args (@t199))
% 0.47/0.65  (step @p432 :rule eq-symm :args (@t49 tptp.e0))
% 0.47/0.65  (step @p433 :rule nary_cong :premises (@p432 @p418 @p393 @p358 @p313) :args (@t200))
% 0.47/0.65  (step @p434 :rule nary_cong :premises (@p432 @p416 @p390 @p354 @p308) :args (@t201))
% 0.47/0.65  (step @p435 :rule eq-symm :args (tptp.unit tptp.e4))
% 0.47/0.65  (step @p436 :rule eq-symm :args (tptp.unit tptp.e3))
% 0.47/0.65  (step @p437 :rule eq-symm :args (tptp.unit tptp.e2))
% 0.47/0.65  (step @p438 :rule eq-symm :args (tptp.unit tptp.e1))
% 0.47/0.65  (step @p439 :rule eq-symm :args (tptp.unit tptp.e0))
% 0.47/0.65  (step @p440 :rule nary_cong :premises (@p439 @p438 @p437 @p436 @p435) :args (@t202))
% 0.47/0.65  (step @p441 :rule eq-symm :args (@t203 tptp.e4))
% 0.47/0.65  (step @p442 :rule eq-symm :args (@t204 tptp.e4))
% 0.47/0.65  (step @p443 :rule eq-symm :args (@t205 tptp.e3))
% 0.47/0.65  (step @p444 :rule eq-symm :args (@t206 tptp.e3))
% 0.47/0.65  (step @p445 :rule eq-symm :args (@t207 tptp.e2))
% 0.47/0.65  (step @p446 :rule eq-symm :args (@t208 tptp.e2))
% 0.47/0.65  (step @p447 :rule eq-symm :args (@t209 tptp.e1))
% 0.47/0.65  (step @p448 :rule eq-symm :args (@t210 tptp.e1))
% 0.47/0.65  (step @p449 :rule eq-symm :args (@t211 tptp.e0))
% 0.47/0.65  (step @p450 :rule eq-symm :args (@t212 tptp.e0))
% 0.47/0.65  (step @p451 :rule nary_cong :premises (@p304 @p293 @p282 @p271 @p260) :args (@t213))
% 0.47/0.65  (step @p452 :rule nary_cong :premises (@p310 @p299 @p288 @p277 @p266) :args (@t214))
% 0.47/0.65  (step @p453 :rule nary_cong :premises (@p311 @p300 @p289 @p278 @p267) :args (@t215))
% 0.47/0.65  (step @p454 :rule nary_cong :premises (@p312 @p301 @p290 @p279 @p268) :args (@t216))
% 0.47/0.65  (step @p455 :rule nary_cong :premises (@p313 @p302 @p291 @p280 @p269) :args (@t217))
% 0.47/0.65  (step @p456 :rule nary_cong :premises (@p305 @p294 @p283 @p272 @p261) :args (@t218))
% 0.47/0.65  (step @p457 :rule nary_cong :premises (@p351 @p342 @p333 @p324 @p315) :args (@t219))
% 0.47/0.65  (step @p458 :rule nary_cong :premises (@p356 @p347 @p338 @p329 @p320) :args (@t220))
% 0.47/0.65  (step @p459 :rule nary_cong :premises (@p357 @p348 @p339 @p330 @p321) :args (@t221))
% 0.47/0.65  (step @p460 :rule nary_cong :premises (@p358 @p349 @p340 @p331 @p322) :args (@t222))
% 0.47/0.65  (step @p461 :rule nary_cong :premises (@p306 @p295 @p284 @p273 @p262) :args (@t223))
% 0.47/0.65  (step @p462 :rule nary_cong :premises (@p352 @p343 @p334 @p325 @p316) :args (@t224))
% 0.47/0.65  (step @p463 :rule nary_cong :premises (@p388 @p381 @p374 @p367 @p360) :args (@t225))
% 0.47/0.65  (step @p464 :rule nary_cong :premises (@p392 @p385 @p378 @p371 @p364) :args (@t226))
% 0.47/0.65  (step @p465 :rule nary_cong :premises (@p393 @p386 @p379 @p372 @p365) :args (@t227))
% 0.47/0.65  (step @p466 :rule nary_cong :premises (@p307 @p296 @p285 @p274 @p263) :args (@t228))
% 0.47/0.65  (step @p467 :rule nary_cong :premises (@p353 @p344 @p335 @p326 @p317) :args (@t229))
% 0.47/0.65  (step @p468 :rule nary_cong :premises (@p389 @p382 @p375 @p368 @p361) :args (@t230))
% 0.47/0.65  (step @p469 :rule nary_cong :premises (@p415 @p410 @p405 @p400 @p395) :args (@t231))
% 0.47/0.65  (step @p470 :rule nary_cong :premises (@p418 @p413 @p408 @p403 @p398) :args (@t232))
% 0.47/0.65  (step @p471 :rule nary_cong :premises (@p308 @p297 @p286 @p275 @p264) :args (@t233))
% 0.47/0.65  (step @p472 :rule nary_cong :premises (@p354 @p345 @p336 @p327 @p318) :args (@t234))
% 0.47/0.65  (step @p473 :rule nary_cong :premises (@p390 @p383 @p376 @p369 @p362) :args (@t235))
% 0.47/0.65  (step @p474 :rule nary_cong :premises (@p416 @p411 @p406 @p401 @p396) :args (@t236))
% 0.47/0.65  (step @p475 :rule nary_cong :premises (@p432 @p429 @p426 @p423 @p420) :args (@t237))
% 0.47/0.65  (step @p476 :rule aci_norm :args ((= (or false @t618 @t617 @t616 @t615 @t614 false @t613 @t612 @t611 @t610 @t609 false @t608 @t607 @t606 @t371 @t605 false @t604 @t603 @t602 @t601 @t600 false) @t619)))
% 0.47/0.65  (step @p477 :rule absorb :args ((= (and false @t620 (not @t620)) false)))
% 0.47/0.65  (step @p478 :rule eq-symm :args (@t238 tptp.e4))
% 0.47/0.65  (step @p479 :rule cong :premises (@p478) :args (@t240))
% 0.47/0.65  (step @p480 :rule evaluate :args ((not true)))
% 0.47/0.65  (step @p481 :rule eq-refl :args (@t1))
% 0.47/0.65  (step @p482 :rule cong :premises (@p481) :args (@t241))
% 0.47/0.65  (step @p483 :rule trans :premises (@p482 @p480))
% 0.47/0.65  (step @p484 :rule nary_cong :premises (@p483 @p478 @p479) :args (@t242))
% 0.47/0.65  (step @p485 :rule trans :premises (@p484 @p477))
% 0.47/0.65  (step @p486 :rule eq-symm :args (@t243 tptp.e3))
% 0.47/0.65  (step @p487 :rule cong :premises (@p486) :args (@t244))
% 0.47/0.65  (step @p488 :rule eq-symm :args (@t245 tptp.e4))
% 0.47/0.65  (step @p489 :rule refl :args (@t246))
% 0.47/0.65  (step @p490 :rule nary_cong :premises (@p489 @p488 @p487) :args (@t247))
% 0.47/0.65  (step @p491 :rule eq-symm :args (@t248 tptp.e2))
% 0.47/0.65  (step @p492 :rule cong :premises (@p491) :args (@t249))
% 0.47/0.65  (step @p493 :rule eq-symm :args (@t250 tptp.e4))
% 0.47/0.65  (step @p494 :rule refl :args (@t251))
% 0.47/0.65  (step @p495 :rule nary_cong :premises (@p494 @p493 @p492) :args (@t252))
% 0.47/0.65  (step @p496 :rule eq-symm :args (@t253 tptp.e1))
% 0.47/0.65  (step @p497 :rule cong :premises (@p496) :args (@t254))
% 0.47/0.65  (step @p498 :rule eq-symm :args (@t255 tptp.e4))
% 0.47/0.65  (step @p499 :rule refl :args (@t256))
% 0.47/0.65  (step @p500 :rule nary_cong :premises (@p499 @p498 @p497) :args (@t257))
% 0.47/0.65  (step @p501 :rule eq-symm :args (@t258 tptp.e0))
% 0.47/0.65  (step @p502 :rule cong :premises (@p501) :args (@t259))
% 0.47/0.65  (step @p503 :rule eq-symm :args (@t260 tptp.e4))
% 0.47/0.65  (step @p504 :rule refl :args (@t261))
% 0.47/0.65  (step @p505 :rule nary_cong :premises (@p504 @p503 @p502) :args (@t262))
% 0.47/0.65  (step @p506 :rule eq-symm :args (@t263 tptp.e4))
% 0.47/0.65  (step @p507 :rule cong :premises (@p506) :args (@t264))
% 0.47/0.65  (step @p508 :rule eq-symm :args (@t265 tptp.e3))
% 0.47/0.65  (step @p509 :rule eq-symm :args (@t3 @t11))
% 0.47/0.65  (step @p510 :rule cong :premises (@p509) :args (@t266))
% 0.47/0.65  (step @p511 :rule nary_cong :premises (@p510 @p508 @p507) :args (@t267))
% 0.47/0.65  (step @p512 :rule absorb :args ((= (and false @t621 (not @t621)) false)))
% 0.47/0.65  (step @p513 :rule eq-symm :args (@t268 tptp.e3))
% 0.47/0.65  (step @p514 :rule cong :premises (@p513) :args (@t270))
% 0.47/0.65  (step @p515 :rule eq-refl :args (@t13))
% 0.47/0.65  (step @p516 :rule cong :premises (@p515) :args (@t271))
% 0.47/0.65  (step @p517 :rule trans :premises (@p516 @p480))
% 0.47/0.65  (step @p518 :rule nary_cong :premises (@p517 @p513 @p514) :args (@t272))
% 0.47/0.65  (step @p519 :rule trans :premises (@p518 @p512))
% 0.47/0.65  (step @p520 :rule eq-symm :args (@t273 tptp.e2))
% 0.47/0.65  (step @p521 :rule cong :premises (@p520) :args (@t274))
% 0.47/0.65  (step @p522 :rule eq-symm :args (@t275 tptp.e3))
% 0.47/0.65  (step @p523 :rule refl :args (@t276))
% 0.47/0.65  (step @p524 :rule nary_cong :premises (@p523 @p522 @p521) :args (@t277))
% 0.47/0.65  (step @p525 :rule eq-symm :args (@t278 tptp.e1))
% 0.47/0.65  (step @p526 :rule cong :premises (@p525) :args (@t279))
% 0.47/0.65  (step @p527 :rule eq-symm :args (@t280 tptp.e3))
% 0.47/0.65  (step @p528 :rule refl :args (@t282))
% 0.47/0.65  (step @p529 :rule nary_cong :premises (@p528 @p527 @p526) :args (@t283))
% 0.47/0.65  (step @p530 :rule eq-symm :args (@t284 tptp.e0))
% 0.47/0.65  (step @p531 :rule cong :premises (@p530) :args (@t285))
% 0.47/0.65  (step @p532 :rule eq-symm :args (@t286 tptp.e3))
% 0.47/0.65  (step @p533 :rule refl :args (@t287))
% 0.47/0.65  (step @p534 :rule nary_cong :premises (@p533 @p532 @p531) :args (@t288))
% 0.47/0.65  (step @p535 :rule eq-symm :args (@t289 tptp.e4))
% 0.47/0.65  (step @p536 :rule cong :premises (@p535) :args (@t290))
% 0.47/0.65  (step @p537 :rule eq-symm :args (@t291 tptp.e2))
% 0.47/0.65  (step @p538 :rule eq-symm :args (@t5 @t21))
% 0.47/0.65  (step @p539 :rule cong :premises (@p538) :args (@t292))
% 0.47/0.65  (step @p540 :rule nary_cong :premises (@p539 @p537 @p536) :args (@t293))
% 0.47/0.65  (step @p541 :rule eq-symm :args (@t294 tptp.e3))
% 0.47/0.65  (step @p542 :rule cong :premises (@p541) :args (@t295))
% 0.47/0.65  (step @p543 :rule eq-symm :args (@t296 tptp.e2))
% 0.47/0.65  (step @p544 :rule eq-symm :args (@t15 @t23))
% 0.47/0.65  (step @p545 :rule cong :premises (@p544) :args (@t297))
% 0.47/0.65  (step @p546 :rule nary_cong :premises (@p545 @p543 @p542) :args (@t298))
% 0.47/0.65  (step @p547 :rule absorb :args ((= (and false @t622 (not @t622)) false)))
% 0.47/0.65  (step @p548 :rule eq-symm :args (@t299 tptp.e2))
% 0.47/0.65  (step @p549 :rule cong :premises (@p548) :args (@t301))
% 0.47/0.65  (step @p550 :rule eq-refl :args (@t25))
% 0.47/0.65  (step @p551 :rule cong :premises (@p550) :args (@t302))
% 0.47/0.65  (step @p552 :rule trans :premises (@p551 @p480))
% 0.47/0.65  (step @p553 :rule nary_cong :premises (@p552 @p548 @p549) :args (@t303))
% 0.47/0.65  (step @p554 :rule trans :premises (@p553 @p547))
% 0.47/0.65  (step @p555 :rule eq-symm :args (@t304 tptp.e1))
% 0.47/0.65  (step @p556 :rule cong :premises (@p555) :args (@t305))
% 0.47/0.65  (step @p557 :rule eq-symm :args (@t306 tptp.e2))
% 0.47/0.65  (step @p558 :rule refl :args (@t307))
% 0.47/0.65  (step @p559 :rule nary_cong :premises (@p558 @p557 @p556) :args (@t308))
% 0.47/0.65  (step @p560 :rule eq-symm :args (@t309 tptp.e0))
% 0.47/0.65  (step @p561 :rule cong :premises (@p560) :args (@t310))
% 0.47/0.65  (step @p562 :rule eq-symm :args (@t311 tptp.e2))
% 0.47/0.65  (step @p563 :rule refl :args (@t312))
% 0.47/0.65  (step @p564 :rule nary_cong :premises (@p563 @p562 @p561) :args (@t313))
% 0.47/0.65  (step @p565 :rule eq-symm :args (@t314 tptp.e4))
% 0.47/0.65  (step @p566 :rule cong :premises (@p565) :args (@t315))
% 0.47/0.65  (step @p567 :rule eq-symm :args (@t316 tptp.e1))
% 0.47/0.65  (step @p568 :rule eq-symm :args (@t7 @t31))
% 0.47/0.65  (step @p569 :rule cong :premises (@p568) :args (@t317))
% 0.47/0.65  (step @p570 :rule nary_cong :premises (@p569 @p567 @p566) :args (@t318))
% 0.47/0.65  (step @p571 :rule eq-symm :args (@t319 tptp.e3))
% 0.47/0.65  (step @p572 :rule cong :premises (@p571) :args (@t320))
% 0.47/0.65  (step @p573 :rule eq-symm :args (@t321 tptp.e1))
% 0.47/0.65  (step @p574 :rule eq-symm :args (@t17 @t33))
% 0.47/0.65  (step @p575 :rule cong :premises (@p574) :args (@t322))
% 0.47/0.65  (step @p576 :rule nary_cong :premises (@p575 @p573 @p572) :args (@t323))
% 0.47/0.65  (step @p577 :rule eq-symm :args (@t324 tptp.e2))
% 0.47/0.65  (step @p578 :rule cong :premises (@p577) :args (@t325))
% 0.47/0.65  (step @p579 :rule eq-symm :args (@t326 tptp.e1))
% 0.47/0.65  (step @p580 :rule eq-symm :args (@t27 @t35))
% 0.47/0.65  (step @p581 :rule cong :premises (@p580) :args (@t327))
% 0.47/0.65  (step @p582 :rule nary_cong :premises (@p581 @p579 @p578) :args (@t328))
% 0.47/0.65  (step @p583 :rule absorb :args ((= (and false @t623 (not @t623)) false)))
% 0.47/0.65  (step @p584 :rule eq-symm :args (@t329 tptp.e1))
% 0.47/0.65  (step @p585 :rule cong :premises (@p584) :args (@t331))
% 0.47/0.65  (step @p586 :rule eq-refl :args (@t37))
% 0.47/0.65  (step @p587 :rule cong :premises (@p586) :args (@t332))
% 0.47/0.65  (step @p588 :rule trans :premises (@p587 @p480))
% 0.47/0.65  (step @p589 :rule nary_cong :premises (@p588 @p584 @p585) :args (@t333))
% 0.47/0.65  (step @p590 :rule trans :premises (@p589 @p583))
% 0.47/0.65  (step @p591 :rule eq-symm :args (@t334 tptp.e0))
% 0.47/0.65  (step @p592 :rule cong :premises (@p591) :args (@t335))
% 0.47/0.65  (step @p593 :rule eq-symm :args (@t336 tptp.e1))
% 0.47/0.65  (step @p594 :rule refl :args (@t337))
% 0.47/0.65  (step @p595 :rule nary_cong :premises (@p594 @p593 @p592) :args (@t338))
% 0.47/0.65  (step @p596 :rule eq-symm :args (@t339 tptp.e4))
% 0.47/0.65  (step @p597 :rule cong :premises (@p596) :args (@t340))
% 0.47/0.65  (step @p598 :rule eq-symm :args (@t341 tptp.e0))
% 0.47/0.65  (step @p599 :rule eq-symm :args (@t9 @t41))
% 0.47/0.65  (step @p600 :rule cong :premises (@p599) :args (@t342))
% 0.47/0.65  (step @p601 :rule nary_cong :premises (@p600 @p598 @p597) :args (@t343))
% 0.47/0.65  (step @p602 :rule eq-symm :args (@t344 tptp.e3))
% 0.47/0.65  (step @p603 :rule cong :premises (@p602) :args (@t345))
% 0.47/0.65  (step @p604 :rule eq-symm :args (@t346 tptp.e0))
% 0.47/0.65  (step @p605 :rule eq-symm :args (@t19 @t43))
% 0.47/0.65  (step @p606 :rule cong :premises (@p605) :args (@t347))
% 0.47/0.65  (step @p607 :rule nary_cong :premises (@p606 @p604 @p603) :args (@t348))
% 0.47/0.65  (step @p608 :rule eq-symm :args (@t349 tptp.e2))
% 0.47/0.65  (step @p609 :rule cong :premises (@p608) :args (@t350))
% 0.47/0.65  (step @p610 :rule eq-symm :args (@t351 tptp.e0))
% 0.47/0.65  (step @p611 :rule eq-symm :args (@t29 @t45))
% 0.47/0.65  (step @p612 :rule cong :premises (@p611) :args (@t352))
% 0.47/0.65  (step @p613 :rule nary_cong :premises (@p612 @p610 @p609) :args (@t353))
% 0.47/0.65  (step @p614 :rule eq-symm :args (@t354 tptp.e1))
% 0.47/0.65  (step @p615 :rule cong :premises (@p614) :args (@t355))
% 0.47/0.65  (step @p616 :rule eq-symm :args (@t356 tptp.e0))
% 0.47/0.65  (step @p617 :rule eq-symm :args (@t39 @t47))
% 0.47/0.65  (step @p618 :rule cong :premises (@p617) :args (@t357))
% 0.47/0.65  (step @p619 :rule nary_cong :premises (@p618 @p616 @p615) :args (@t358))
% 0.47/0.65  (step @p620 :rule absorb :args ((= (and false @t624 (not @t624)) false)))
% 0.47/0.65  (step @p621 :rule eq-symm :args (@t359 tptp.e0))
% 0.47/0.65  (step @p622 :rule cong :premises (@p621) :args (@t361))
% 0.47/0.65  (step @p623 :rule eq-refl :args (@t49))
% 0.47/0.65  (step @p624 :rule cong :premises (@p623) :args (@t362))
% 0.47/0.65  (step @p625 :rule trans :premises (@p624 @p480))
% 0.47/0.65  (step @p626 :rule nary_cong :premises (@p625 @p621 @p622) :args (@t363))
% 0.47/0.65  (step @p627 :rule trans :premises (@p626 @p620))
% 0.47/0.65  (step @p628 :rule nary_cong :premises (@p627 @p619 @p613 @p607 @p601 @p595 @p590 @p582 @p576 @p570 @p564 @p559 @p554 @p546 @p540 @p534 @p529 @p524 @p519 @p511 @p505 @p500 @p495 @p490 @p485) :args (@t364))
% 0.47/0.65  (step @p629 :rule trans :premises (@p628 @p476))
% 0.47/0.65  (step @p630 :rule nary_cong :premises (@p629 @p475 @p474 @p473 @p472 @p471 @p470 @p469 @p468 @p467 @p466 @p465 @p464 @p463 @p462 @p461 @p460 @p459 @p458 @p457 @p456 @p455 @p454 @p453 @p452 @p451 @p450 @p449 @p448 @p447 @p446 @p445 @p444 @p443 @p442 @p441 @p440 @p434 @p433 @p431 @p430 @p428 @p427 @p425 @p424 @p422 @p421 @p419 @p417 @p414 @p412 @p409 @p407 @p404 @p402 @p399 @p397 @p394 @p391 @p387 @p384 @p380 @p377 @p373 @p370 @p366 @p363 @p359 @p355 @p350 @p346 @p341 @p337 @p332 @p328 @p323 @p319 @p314 @p309 @p303 @p298 @p292 @p287 @p281 @p276 @p270 @p265) :args (@t365))
% 0.47/0.65  (step @p631 :rule cong :premises (@p630) :args (@t366))
% 0.47/0.65  (step @p632 :rule eq_resolve :premises (@p4 @p631))
% 0.47/0.65  (step @p633 :rule not_and :premises (@p632))
% 0.47/0.65  (step @p634 :rule chain_m_resolution :premises (@p633 @p259 @p257 @p255 @p253 @p251 @p249 @p247 @p245 @p243 @p241 @p239 @p237 @p235 @p233 @p231 @p229 @p227 @p225 @p223 @p221 @p219 @p217 @p215 @p213 @p211 @p209 @p207 @p204 @p202 @p200 @p198 @p195 @p193 @p191 @p189 @p186 @p183 @p181 @p177 @p175 @p173 @p171 @p169 @p167 @p165 @p163 @p161 @p159 @p157 @p153 @p149 @p147 @p145 @p143 @p141 @p139 @p137 @p133 @p131 @p129 @p127 @p123 @p119 @p117 @p113 @p111 @p107 @p103 @p100 @p98 @p94 @p92 @p90 @p86 @p82 @p80 @p76 @p74 @p70 @p66 @p62 @p59 @p55 @p53 @p49 @p45) :args ((not @t619) (@list false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false) (@list @t599 @t598 @t597 @t596 @t595 @t594 @t593 @t592 @t591 @t590 @t589 @t588 @t587 @t586 @t585 @t584 @t583 @t582 @t581 @t580 @t579 @t578 @t577 @t576 @t575 (= tptp.e0 @t212) (= tptp.e0 @t211) (= tptp.e1 @t210) (= tptp.e1 @t209) (= tptp.e2 @t208) (= tptp.e2 @t207) (= tptp.e3 @t206) (= tptp.e3 @t205) (= tptp.e4 @t204) (= tptp.e4 @t203) @t574 @t572 @t570 @t568 @t567 @t565 @t564 @t562 @t561 @t559 @t558 @t556 @t554 @t550 @t547 @t544 @t541 @t538 @t536 @t533 @t531 @t527 @t524 @t520 @t517 @t512 @t508 @t504 @t500 @t496 @t492 @t487 @t482 @t477 @t472 @t467 @t463 @t457 @t452 @t446 @t441 @t436 @t430 @t423 @t417 @t410 @t404 @t397 @t391 @t384 @t377)))
% 0.47/0.65  (step @p635 :rule cnf_or_neg :args (@t619 13))
% 0.47/0.65  (step @p636 false :rule chain_m_resolution :premises (@p635 @p634 @p41) :args (false (@list true false) (@list @t619 @t371)))
% 0.47/0.65  )
% 0.47/0.65  % SZS output end Proof
% 0.47/0.65  % cvc5 exiting
%------------------------------------------------------------------------------