%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ALG091+1 : TPTP v9.2.1. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n018.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.37s 0.65s % Output : Proof 0.37s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ALG091+1 : TPTP v9.2.1. Released v2.7.0. % 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.17/0.34 % Computer : n018.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:39:20 EDT 2026 % 0.17/0.34 % CPUTime : % 0.31/0.51 %----Proving TF0_NAR, FOF, or CNF % 0.37/0.65 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 0.37/0.65 % SZS status Theorem % 0.37/0.65 % SZS output start Proof % 0.37/0.65 ( % 0.37/0.65 (declare-sort $$unsorted 0) % 0.37/0.65 (declare-const tptp.unit $$unsorted) % 0.37/0.65 (declare-const tptp.op (-> $$unsorted $$unsorted $$unsorted)) % 0.37/0.65 (declare-const tptp.e0 $$unsorted) % 0.37/0.65 (declare-const tptp.e1 $$unsorted) % 0.37/0.65 (declare-const tptp.e2 $$unsorted) % 0.37/0.65 (declare-const tptp.e3 $$unsorted) % 0.37/0.65 (declare-const tptp.e4 $$unsorted) % 0.37/0.65 (define @t1 () (= tptp.e0 tptp.e4)) % 0.37/0.65 (define @t2 () (not @t1)) % 0.37/0.65 (define @t3 () (= tptp.e0 tptp.e3)) % 0.37/0.65 (define @t4 () (not @t3)) % 0.37/0.65 (define @t5 () (= tptp.e0 tptp.e2)) % 0.37/0.65 (define @t6 () (not @t5)) % 0.37/0.65 (define @t7 () (tptp.op tptp.e4 tptp.e4)) % 0.37/0.65 (define @t8 () (= @t7 tptp.e0)) % 0.37/0.65 (define @t9 () (tptp.op tptp.e4 tptp.e3)) % 0.37/0.65 (define @t10 () (= @t9 tptp.e2)) % 0.37/0.65 (define @t11 () (tptp.op tptp.e4 tptp.e2)) % 0.37/0.65 (define @t12 () (= @t11 tptp.e1)) % 0.37/0.65 (define @t13 () (tptp.op tptp.e4 tptp.e1)) % 0.37/0.65 (define @t14 () (= @t13 tptp.e3)) % 0.37/0.65 (define @t15 () (tptp.op tptp.e4 tptp.e0)) % 0.37/0.65 (define @t16 () (= @t15 tptp.e4)) % 0.37/0.65 (define @t17 () (tptp.op tptp.e3 tptp.e4)) % 0.37/0.65 (define @t18 () (= @t17 tptp.e1)) % 0.37/0.65 (define @t19 () (tptp.op tptp.e3 tptp.e3)) % 0.37/0.65 (define @t20 () (= @t19 tptp.e0)) % 0.37/0.65 (define @t21 () (tptp.op tptp.e3 tptp.e2)) % 0.37/0.65 (define @t22 () (= @t21 tptp.e4)) % 0.37/0.65 (define @t23 () (tptp.op tptp.e3 tptp.e1)) % 0.37/0.65 (define @t24 () (= @t23 tptp.e2)) % 0.37/0.65 (define @t25 () (tptp.op tptp.e3 tptp.e0)) % 0.37/0.65 (define @t26 () (= @t25 tptp.e3)) % 0.37/0.65 (define @t27 () (tptp.op tptp.e2 tptp.e4)) % 0.37/0.65 (define @t28 () (= @t27 tptp.e3)) % 0.37/0.65 (define @t29 () (tptp.op tptp.e2 tptp.e3)) % 0.37/0.65 (define @t30 () (= @t29 tptp.e1)) % 0.37/0.65 (define @t31 () (tptp.op tptp.e2 tptp.e2)) % 0.37/0.65 (define @t32 () (= @t31 tptp.e0)) % 0.37/0.65 (define @t33 () (tptp.op tptp.e2 tptp.e1)) % 0.37/0.65 (define @t34 () (= @t33 tptp.e4)) % 0.37/0.65 (define @t35 () (tptp.op tptp.e2 tptp.e0)) % 0.37/0.65 (define @t36 () (= @t35 tptp.e2)) % 0.37/0.65 (define @t37 () (tptp.op tptp.e1 tptp.e4)) % 0.37/0.65 (define @t38 () (= @t37 tptp.e2)) % 0.37/0.65 (define @t39 () (tptp.op tptp.e1 tptp.e3)) % 0.37/0.65 (define @t40 () (= @t39 tptp.e4)) % 0.37/0.65 (define @t41 () (tptp.op tptp.e1 tptp.e2)) % 0.37/0.65 (define @t42 () (= @t41 tptp.e3)) % 0.37/0.65 (define @t43 () (tptp.op tptp.e1 tptp.e1)) % 0.37/0.65 (define @t44 () (= @t43 tptp.e0)) % 0.37/0.65 (define @t45 () (tptp.op tptp.e1 tptp.e0)) % 0.37/0.65 (define @t46 () (= @t45 tptp.e1)) % 0.37/0.65 (define @t47 () (tptp.op tptp.e0 tptp.e4)) % 0.37/0.65 (define @t48 () (= @t47 tptp.e4)) % 0.37/0.65 (define @t49 () (tptp.op tptp.e0 tptp.e3)) % 0.37/0.65 (define @t50 () (= @t49 tptp.e3)) % 0.37/0.65 (define @t51 () (tptp.op tptp.e0 tptp.e2)) % 0.37/0.65 (define @t52 () (= @t51 tptp.e2)) % 0.37/0.65 (define @t53 () (tptp.op tptp.e0 tptp.e1)) % 0.37/0.65 (define @t54 () (= @t53 tptp.e1)) % 0.37/0.65 (define @t55 () (tptp.op tptp.e0 tptp.e0)) % 0.37/0.65 (define @t56 () (= @t55 tptp.e0)) % 0.37/0.65 (define @t57 () (= tptp.unit tptp.e0)) % 0.37/0.65 (define @t58 () (= @t7 tptp.e4)) % 0.37/0.65 (define @t59 () (= @t17 tptp.e4)) % 0.37/0.65 (define @t60 () (= @t27 tptp.e4)) % 0.37/0.65 (define @t61 () (= @t37 tptp.e4)) % 0.37/0.65 (define @t62 () (or @t48 @t61 @t60 @t59 @t58)) % 0.37/0.65 (define @t63 () (= @t9 tptp.e4)) % 0.37/0.65 (define @t64 () (= @t11 tptp.e4)) % 0.37/0.65 (define @t65 () (= @t13 tptp.e4)) % 0.37/0.65 (define @t66 () (or @t16 @t65 @t64 @t63 @t58)) % 0.37/0.65 (define @t67 () (= @t7 tptp.e3)) % 0.37/0.65 (define @t68 () (= @t17 tptp.e3)) % 0.37/0.65 (define @t69 () (= @t37 tptp.e3)) % 0.37/0.65 (define @t70 () (= @t47 tptp.e3)) % 0.37/0.65 (define @t71 () (or @t70 @t69 @t28 @t68 @t67)) % 0.37/0.65 (define @t72 () (= @t9 tptp.e3)) % 0.37/0.65 (define @t73 () (= @t11 tptp.e3)) % 0.37/0.65 (define @t74 () (= @t15 tptp.e3)) % 0.37/0.65 (define @t75 () (or @t74 @t14 @t73 @t72 @t67)) % 0.37/0.65 (define @t76 () (= @t7 tptp.e2)) % 0.37/0.65 (define @t77 () (= @t17 tptp.e2)) % 0.37/0.65 (define @t78 () (= @t27 tptp.e2)) % 0.37/0.65 (define @t79 () (= @t47 tptp.e2)) % 0.37/0.65 (define @t80 () (or @t79 @t38 @t78 @t77 @t76)) % 0.37/0.65 (define @t81 () (= @t11 tptp.e2)) % 0.37/0.65 (define @t82 () (= @t13 tptp.e2)) % 0.37/0.65 (define @t83 () (= @t15 tptp.e2)) % 0.37/0.65 (define @t84 () (or @t83 @t82 @t81 @t10 @t76)) % 0.37/0.65 (define @t85 () (= @t7 tptp.e1)) % 0.37/0.65 (define @t86 () (= @t27 tptp.e1)) % 0.37/0.65 (define @t87 () (= @t37 tptp.e1)) % 0.37/0.65 (define @t88 () (= @t47 tptp.e1)) % 0.37/0.65 (define @t89 () (or @t88 @t87 @t86 @t18 @t85)) % 0.37/0.65 (define @t90 () (= @t9 tptp.e1)) % 0.37/0.65 (define @t91 () (= @t13 tptp.e1)) % 0.37/0.65 (define @t92 () (= @t15 tptp.e1)) % 0.37/0.65 (define @t93 () (or @t92 @t91 @t12 @t90 @t85)) % 0.37/0.65 (define @t94 () (= @t17 tptp.e0)) % 0.37/0.65 (define @t95 () (= @t27 tptp.e0)) % 0.37/0.65 (define @t96 () (= @t37 tptp.e0)) % 0.37/0.65 (define @t97 () (= @t47 tptp.e0)) % 0.37/0.65 (define @t98 () (or @t97 @t96 @t95 @t94 @t8)) % 0.37/0.65 (define @t99 () (= @t9 tptp.e0)) % 0.37/0.65 (define @t100 () (= @t11 tptp.e0)) % 0.37/0.65 (define @t101 () (= @t13 tptp.e0)) % 0.37/0.65 (define @t102 () (= @t15 tptp.e0)) % 0.37/0.65 (define @t103 () (or @t102 @t101 @t100 @t99 @t8)) % 0.37/0.65 (define @t104 () (= @t19 tptp.e4)) % 0.37/0.65 (define @t105 () (= @t29 tptp.e4)) % 0.37/0.65 (define @t106 () (= @t49 tptp.e4)) % 0.37/0.65 (define @t107 () (or @t106 @t40 @t105 @t104 @t63)) % 0.37/0.65 (define @t108 () (= @t23 tptp.e4)) % 0.37/0.65 (define @t109 () (= @t25 tptp.e4)) % 0.37/0.65 (define @t110 () (or @t109 @t108 @t22 @t104 @t59)) % 0.37/0.65 (define @t111 () (= @t19 tptp.e3)) % 0.37/0.65 (define @t112 () (= @t29 tptp.e3)) % 0.37/0.65 (define @t113 () (= @t39 tptp.e3)) % 0.37/0.65 (define @t114 () (or @t50 @t113 @t112 @t111 @t72)) % 0.37/0.65 (define @t115 () (= @t21 tptp.e3)) % 0.37/0.65 (define @t116 () (= @t23 tptp.e3)) % 0.37/0.65 (define @t117 () (or @t26 @t116 @t115 @t111 @t68)) % 0.37/0.65 (define @t118 () (= @t19 tptp.e2)) % 0.37/0.65 (define @t119 () (= @t29 tptp.e2)) % 0.37/0.65 (define @t120 () (= @t39 tptp.e2)) % 0.37/0.65 (define @t121 () (= @t49 tptp.e2)) % 0.37/0.65 (define @t122 () (or @t121 @t120 @t119 @t118 @t10)) % 0.37/0.65 (define @t123 () (= @t21 tptp.e2)) % 0.37/0.65 (define @t124 () (= @t25 tptp.e2)) % 0.37/0.65 (define @t125 () (or @t124 @t24 @t123 @t118 @t77)) % 0.37/0.65 (define @t126 () (= @t19 tptp.e1)) % 0.37/0.65 (define @t127 () (= @t39 tptp.e1)) % 0.37/0.65 (define @t128 () (= @t49 tptp.e1)) % 0.37/0.65 (define @t129 () (or @t128 @t127 @t30 @t126 @t90)) % 0.37/0.65 (define @t130 () (= @t21 tptp.e1)) % 0.37/0.65 (define @t131 () (= @t23 tptp.e1)) % 0.37/0.65 (define @t132 () (= @t25 tptp.e1)) % 0.37/0.65 (define @t133 () (or @t132 @t131 @t130 @t126 @t18)) % 0.37/0.65 (define @t134 () (= @t29 tptp.e0)) % 0.37/0.65 (define @t135 () (= @t39 tptp.e0)) % 0.37/0.65 (define @t136 () (= @t49 tptp.e0)) % 0.37/0.65 (define @t137 () (or @t136 @t135 @t134 @t20 @t99)) % 0.37/0.65 (define @t138 () (= @t21 tptp.e0)) % 0.37/0.65 (define @t139 () (= @t23 tptp.e0)) % 0.37/0.65 (define @t140 () (= @t25 tptp.e0)) % 0.37/0.65 (define @t141 () (or @t140 @t139 @t138 @t20 @t94)) % 0.37/0.65 (define @t142 () (= @t31 tptp.e4)) % 0.37/0.65 (define @t143 () (= @t41 tptp.e4)) % 0.37/0.65 (define @t144 () (= @t51 tptp.e4)) % 0.37/0.65 (define @t145 () (or @t144 @t143 @t142 @t22 @t64)) % 0.37/0.65 (define @t146 () (= @t35 tptp.e4)) % 0.37/0.65 (define @t147 () (or @t146 @t34 @t142 @t105 @t60)) % 0.37/0.65 (define @t148 () (= @t31 tptp.e3)) % 0.37/0.65 (define @t149 () (= @t51 tptp.e3)) % 0.37/0.65 (define @t150 () (or @t149 @t42 @t148 @t115 @t73)) % 0.37/0.65 (define @t151 () (= @t33 tptp.e3)) % 0.37/0.65 (define @t152 () (= @t35 tptp.e3)) % 0.37/0.65 (define @t153 () (or @t152 @t151 @t148 @t112 @t28)) % 0.37/0.65 (define @t154 () (= @t31 tptp.e2)) % 0.37/0.65 (define @t155 () (= @t41 tptp.e2)) % 0.37/0.65 (define @t156 () (or @t52 @t155 @t154 @t123 @t81)) % 0.37/0.65 (define @t157 () (= @t33 tptp.e2)) % 0.37/0.65 (define @t158 () (or @t36 @t157 @t154 @t119 @t78)) % 0.37/0.65 (define @t159 () (= @t31 tptp.e1)) % 0.37/0.65 (define @t160 () (= @t41 tptp.e1)) % 0.37/0.65 (define @t161 () (= @t51 tptp.e1)) % 0.37/0.65 (define @t162 () (or @t161 @t160 @t159 @t130 @t12)) % 0.37/0.65 (define @t163 () (= @t33 tptp.e1)) % 0.37/0.65 (define @t164 () (= @t35 tptp.e1)) % 0.37/0.65 (define @t165 () (or @t164 @t163 @t159 @t30 @t86)) % 0.37/0.65 (define @t166 () (= @t41 tptp.e0)) % 0.37/0.65 (define @t167 () (= @t51 tptp.e0)) % 0.37/0.65 (define @t168 () (or @t167 @t166 @t32 @t138 @t100)) % 0.37/0.65 (define @t169 () (= @t33 tptp.e0)) % 0.37/0.65 (define @t170 () (= @t35 tptp.e0)) % 0.37/0.65 (define @t171 () (or @t170 @t169 @t32 @t134 @t95)) % 0.37/0.65 (define @t172 () (= @t43 tptp.e4)) % 0.37/0.65 (define @t173 () (= @t53 tptp.e4)) % 0.37/0.65 (define @t174 () (or @t173 @t172 @t34 @t108 @t65)) % 0.37/0.65 (define @t175 () (= @t45 tptp.e4)) % 0.37/0.65 (define @t176 () (or @t175 @t172 @t143 @t40 @t61)) % 0.37/0.65 (define @t177 () (= @t43 tptp.e3)) % 0.37/0.65 (define @t178 () (= @t53 tptp.e3)) % 0.37/0.65 (define @t179 () (or @t178 @t177 @t151 @t116 @t14)) % 0.37/0.65 (define @t180 () (= @t45 tptp.e3)) % 0.37/0.65 (define @t181 () (or @t180 @t177 @t42 @t113 @t69)) % 0.37/0.65 (define @t182 () (= @t43 tptp.e2)) % 0.37/0.65 (define @t183 () (= @t53 tptp.e2)) % 0.37/0.65 (define @t184 () (or @t183 @t182 @t157 @t24 @t82)) % 0.37/0.65 (define @t185 () (= @t45 tptp.e2)) % 0.37/0.65 (define @t186 () (or @t185 @t182 @t155 @t120 @t38)) % 0.37/0.65 (define @t187 () (= @t43 tptp.e1)) % 0.37/0.65 (define @t188 () (or @t54 @t187 @t163 @t131 @t91)) % 0.37/0.65 (define @t189 () (or @t46 @t187 @t160 @t127 @t87)) % 0.37/0.65 (define @t190 () (= @t53 tptp.e0)) % 0.37/0.65 (define @t191 () (or @t190 @t44 @t169 @t139 @t101)) % 0.37/0.65 (define @t192 () (= @t45 tptp.e0)) % 0.37/0.65 (define @t193 () (or @t192 @t44 @t166 @t135 @t96)) % 0.37/0.65 (define @t194 () (= @t55 tptp.e4)) % 0.37/0.65 (define @t195 () (or @t194 @t175 @t146 @t109 @t16)) % 0.37/0.65 (define @t196 () (or @t194 @t173 @t144 @t106 @t48)) % 0.37/0.65 (define @t197 () (= @t55 tptp.e3)) % 0.37/0.65 (define @t198 () (or @t197 @t180 @t152 @t26 @t74)) % 0.37/0.65 (define @t199 () (or @t197 @t178 @t149 @t50 @t70)) % 0.37/0.65 (define @t200 () (= @t55 tptp.e2)) % 0.37/0.65 (define @t201 () (or @t200 @t185 @t36 @t124 @t83)) % 0.37/0.65 (define @t202 () (or @t200 @t183 @t52 @t121 @t79)) % 0.37/0.65 (define @t203 () (= @t55 tptp.e1)) % 0.37/0.65 (define @t204 () (or @t203 @t46 @t164 @t132 @t92)) % 0.37/0.65 (define @t205 () (or @t203 @t54 @t161 @t128 @t88)) % 0.37/0.65 (define @t206 () (or @t56 @t192 @t170 @t140 @t102)) % 0.37/0.65 (define @t207 () (or @t56 @t190 @t167 @t136 @t97)) % 0.37/0.65 (define @t208 () (or @t57 (= tptp.unit tptp.e1) (= tptp.unit tptp.e2) (= tptp.unit tptp.e3) (= tptp.unit tptp.e4))) % 0.37/0.65 (define @t209 () (tptp.op tptp.e4 tptp.unit)) % 0.37/0.65 (define @t210 () (tptp.op tptp.unit tptp.e4)) % 0.37/0.65 (define @t211 () (tptp.op tptp.e3 tptp.unit)) % 0.37/0.65 (define @t212 () (tptp.op tptp.unit tptp.e3)) % 0.37/0.65 (define @t213 () (tptp.op tptp.e2 tptp.unit)) % 0.37/0.65 (define @t214 () (tptp.op tptp.unit tptp.e2)) % 0.37/0.65 (define @t215 () (tptp.op tptp.e1 tptp.unit)) % 0.37/0.65 (define @t216 () (tptp.op tptp.unit tptp.e1)) % 0.37/0.65 (define @t217 () (tptp.op tptp.e0 tptp.unit)) % 0.37/0.65 (define @t218 () (tptp.op tptp.unit tptp.e0)) % 0.37/0.65 (define @t219 () (or @t8 @t85 @t76 @t67 @t58)) % 0.37/0.65 (define @t220 () (or @t99 @t90 @t10 @t72 @t63)) % 0.37/0.65 (define @t221 () (or @t100 @t12 @t81 @t73 @t64)) % 0.37/0.65 (define @t222 () (or @t101 @t91 @t82 @t14 @t65)) % 0.37/0.65 (define @t223 () (or @t102 @t92 @t83 @t74 @t16)) % 0.37/0.65 (define @t224 () (or @t94 @t18 @t77 @t68 @t59)) % 0.37/0.65 (define @t225 () (or @t20 @t126 @t118 @t111 @t104)) % 0.37/0.65 (define @t226 () (or @t138 @t130 @t123 @t115 @t22)) % 0.37/0.65 (define @t227 () (or @t139 @t131 @t24 @t116 @t108)) % 0.37/0.65 (define @t228 () (or @t140 @t132 @t124 @t26 @t109)) % 0.37/0.65 (define @t229 () (or @t95 @t86 @t78 @t28 @t60)) % 0.37/0.65 (define @t230 () (or @t134 @t30 @t119 @t112 @t105)) % 0.37/0.65 (define @t231 () (or @t32 @t159 @t154 @t148 @t142)) % 0.37/0.65 (define @t232 () (or @t169 @t163 @t157 @t151 @t34)) % 0.37/0.65 (define @t233 () (or @t170 @t164 @t36 @t152 @t146)) % 0.37/0.65 (define @t234 () (or @t96 @t87 @t38 @t69 @t61)) % 0.37/0.65 (define @t235 () (or @t135 @t127 @t120 @t113 @t40)) % 0.37/0.65 (define @t236 () (or @t166 @t160 @t155 @t42 @t143)) % 0.37/0.65 (define @t237 () (or @t44 @t187 @t182 @t177 @t172)) % 0.37/0.65 (define @t238 () (or @t192 @t46 @t185 @t180 @t175)) % 0.37/0.65 (define @t239 () (or @t97 @t88 @t79 @t70 @t48)) % 0.37/0.65 (define @t240 () (or @t136 @t128 @t121 @t50 @t106)) % 0.37/0.65 (define @t241 () (or @t167 @t161 @t52 @t149 @t144)) % 0.37/0.65 (define @t242 () (or @t190 @t54 @t183 @t178 @t173)) % 0.37/0.65 (define @t243 () (or @t56 @t203 @t200 @t197 @t194)) % 0.37/0.65 (define @t244 () (not @t58)) % 0.37/0.65 (define @t245 () (or @t244 @t58)) % 0.37/0.65 (define @t246 () (not @t67)) % 0.37/0.65 (define @t247 () (or @t246 @t63)) % 0.37/0.65 (define @t248 () (not @t76)) % 0.37/0.65 (define @t249 () (or @t248 @t64)) % 0.37/0.65 (define @t250 () (not @t85)) % 0.37/0.65 (define @t251 () (or @t250 @t65)) % 0.37/0.65 (define @t252 () (not @t8)) % 0.37/0.65 (define @t253 () (or @t252 @t16)) % 0.37/0.65 (define @t254 () (not @t104)) % 0.37/0.65 (define @t255 () (or @t254 @t68)) % 0.37/0.65 (define @t256 () (not @t111)) % 0.37/0.65 (define @t257 () (or @t256 @t111)) % 0.37/0.65 (define @t258 () (not @t118)) % 0.37/0.65 (define @t259 () (or @t258 @t115)) % 0.37/0.65 (define @t260 () (not @t126)) % 0.37/0.65 (define @t261 () (or @t260 @t116)) % 0.37/0.65 (define @t262 () (not @t20)) % 0.37/0.65 (define @t263 () (or @t262 @t26)) % 0.37/0.65 (define @t264 () (not @t142)) % 0.37/0.65 (define @t265 () (or @t264 @t78)) % 0.37/0.65 (define @t266 () (not @t148)) % 0.37/0.65 (define @t267 () (or @t266 @t119)) % 0.37/0.65 (define @t268 () (not @t154)) % 0.37/0.65 (define @t269 () (or @t268 @t154)) % 0.37/0.65 (define @t270 () (not @t159)) % 0.37/0.65 (define @t271 () (or @t270 @t157)) % 0.37/0.65 (define @t272 () (not @t32)) % 0.37/0.65 (define @t273 () (or @t272 @t36)) % 0.37/0.65 (define @t274 () (not @t172)) % 0.37/0.65 (define @t275 () (or @t274 @t87)) % 0.37/0.65 (define @t276 () (not @t177)) % 0.37/0.65 (define @t277 () (or @t276 @t127)) % 0.37/0.65 (define @t278 () (not @t182)) % 0.37/0.65 (define @t279 () (or @t278 @t160)) % 0.37/0.65 (define @t280 () (not @t187)) % 0.37/0.65 (define @t281 () (or @t280 @t187)) % 0.37/0.65 (define @t282 () (not @t44)) % 0.37/0.65 (define @t283 () (or @t282 @t46)) % 0.37/0.65 (define @t284 () (not @t194)) % 0.37/0.65 (define @t285 () (or @t284 @t97)) % 0.37/0.65 (define @t286 () (not @t197)) % 0.37/0.65 (define @t287 () (or @t286 @t136)) % 0.37/0.65 (define @t288 () (not @t200)) % 0.37/0.65 (define @t289 () (or @t288 @t167)) % 0.37/0.65 (define @t290 () (not @t203)) % 0.37/0.65 (define @t291 () (or @t290 @t190)) % 0.37/0.65 (define @t292 () (not @t56)) % 0.37/0.65 (define @t293 () (or @t292 @t56)) % 0.37/0.65 (define @t294 () (and @t293 @t291 @t289 @t287 @t285 @t283 @t281 @t279 @t277 @t275 @t273 @t271 @t269 @t267 @t265 @t263 @t261 @t259 @t257 @t255 @t253 @t251 @t249 @t247 @t245 @t243 @t242 @t241 @t240 @t239 @t238 @t237 @t236 @t235 @t234 @t233 @t232 @t231 @t230 @t229 @t228 @t227 @t226 @t225 @t224 @t223 @t222 @t221 @t220 @t219 (= @t218 tptp.e0) (= @t217 tptp.e0) (= @t216 tptp.e1) (= @t215 tptp.e1) (= @t214 tptp.e2) (= @t213 tptp.e2) (= @t212 tptp.e3) (= @t211 tptp.e3) (= @t210 tptp.e4) (= @t209 tptp.e4) @t208 @t207 @t206 @t205 @t204 @t202 @t201 @t199 @t198 @t196 @t195 @t193 @t191 @t189 @t188 @t186 @t184 @t181 @t179 @t176 @t174 @t171 @t168 @t165 @t162 @t158 @t156 @t153 @t150 @t147 @t145 @t141 @t137 @t133 @t129 @t125 @t122 @t117 @t114 @t110 @t107 @t103 @t98 @t93 @t89 @t84 @t80 @t75 @t71 @t66 @t62)) % 0.37/0.65 (define @t295 () (not @t294)) % 0.37/0.65 (define @t296 () (= tptp.e4 @t7)) % 0.37/0.65 (define @t297 () (= tptp.e4 @t17)) % 0.37/0.65 (define @t298 () (= tptp.e4 @t27)) % 0.37/0.65 (define @t299 () (= tptp.e4 @t37)) % 0.37/0.65 (define @t300 () (= tptp.e4 @t47)) % 0.37/0.65 (define @t301 () (or @t300 @t299 @t298 @t297 @t296)) % 0.37/0.65 (define @t302 () (@list false)) % 0.37/0.65 (define @t303 () (@list @t300)) % 0.37/0.65 (define @t304 () (= tptp.e4 @t9)) % 0.37/0.65 (define @t305 () (= tptp.e4 @t11)) % 0.37/0.65 (define @t306 () (= tptp.e4 @t13)) % 0.37/0.65 (define @t307 () (= tptp.e4 @t15)) % 0.37/0.65 (define @t308 () (or @t307 @t306 @t305 @t304 @t296)) % 0.37/0.65 (define @t309 () (@list @t307)) % 0.37/0.65 (define @t310 () (= tptp.e3 @t7)) % 0.37/0.65 (define @t311 () (= tptp.e3 @t17)) % 0.37/0.65 (define @t312 () (= tptp.e3 @t27)) % 0.37/0.65 (define @t313 () (= tptp.e3 @t37)) % 0.37/0.65 (define @t314 () (= tptp.e3 @t47)) % 0.37/0.65 (define @t315 () (or @t314 @t313 @t312 @t311 @t310)) % 0.37/0.65 (define @t316 () (@list @t312)) % 0.37/0.65 (define @t317 () (= tptp.e3 @t9)) % 0.37/0.65 (define @t318 () (= tptp.e3 @t11)) % 0.37/0.65 (define @t319 () (= tptp.e3 @t13)) % 0.37/0.65 (define @t320 () (= tptp.e3 @t15)) % 0.37/0.65 (define @t321 () (or @t320 @t319 @t318 @t317 @t310)) % 0.37/0.65 (define @t322 () (@list @t319)) % 0.37/0.65 (define @t323 () (= tptp.e2 @t7)) % 0.37/0.65 (define @t324 () (= tptp.e2 @t17)) % 0.37/0.65 (define @t325 () (= tptp.e2 @t27)) % 0.37/0.65 (define @t326 () (= tptp.e2 @t37)) % 0.37/0.65 (define @t327 () (= tptp.e2 @t47)) % 0.37/0.65 (define @t328 () (or @t327 @t326 @t325 @t324 @t323)) % 0.37/0.65 (define @t329 () (@list @t326)) % 0.37/0.65 (define @t330 () (= tptp.e2 @t9)) % 0.37/0.65 (define @t331 () (= tptp.e2 @t11)) % 0.37/0.65 (define @t332 () (= tptp.e2 @t13)) % 0.37/0.65 (define @t333 () (= tptp.e2 @t15)) % 0.37/0.65 (define @t334 () (or @t333 @t332 @t331 @t330 @t323)) % 0.37/0.65 (define @t335 () (@list @t330)) % 0.37/0.65 (define @t336 () (= tptp.e1 @t7)) % 0.37/0.65 (define @t337 () (= tptp.e1 @t17)) % 0.37/0.65 (define @t338 () (= tptp.e1 @t27)) % 0.37/0.65 (define @t339 () (= tptp.e1 @t37)) % 0.37/0.65 (define @t340 () (= tptp.e1 @t47)) % 0.37/0.65 (define @t341 () (or @t340 @t339 @t338 @t337 @t336)) % 0.37/0.65 (define @t342 () (@list @t337)) % 0.37/0.65 (define @t343 () (= tptp.e1 @t9)) % 0.37/0.65 (define @t344 () (= tptp.e1 @t11)) % 0.37/0.65 (define @t345 () (= tptp.e1 @t13)) % 0.37/0.65 (define @t346 () (= tptp.e1 @t15)) % 0.37/0.65 (define @t347 () (or @t346 @t345 @t344 @t343 @t336)) % 0.37/0.65 (define @t348 () (@list @t344)) % 0.37/0.65 (define @t349 () (= tptp.e0 @t7)) % 0.37/0.65 (define @t350 () (= tptp.e0 @t17)) % 0.37/0.65 (define @t351 () (= tptp.e0 @t27)) % 0.37/0.65 (define @t352 () (= tptp.e0 @t37)) % 0.37/0.65 (define @t353 () (= tptp.e0 @t47)) % 0.37/0.65 (define @t354 () (or @t353 @t352 @t351 @t350 @t349)) % 0.37/0.65 (define @t355 () (not @t349)) % 0.37/0.65 (define @t356 () (@list @t349)) % 0.37/0.65 (define @t357 () (= tptp.e0 @t9)) % 0.37/0.65 (define @t358 () (= tptp.e0 @t11)) % 0.37/0.65 (define @t359 () (= tptp.e0 @t13)) % 0.37/0.65 (define @t360 () (= tptp.e0 @t15)) % 0.37/0.65 (define @t361 () (or @t360 @t359 @t358 @t357 @t349)) % 0.37/0.65 (define @t362 () (= tptp.e4 @t19)) % 0.37/0.65 (define @t363 () (= tptp.e4 @t29)) % 0.37/0.65 (define @t364 () (= tptp.e4 @t39)) % 0.37/0.65 (define @t365 () (= tptp.e4 @t49)) % 0.37/0.65 (define @t366 () (or @t365 @t364 @t363 @t362 @t304)) % 0.37/0.65 (define @t367 () (@list @t364)) % 0.37/0.65 (define @t368 () (= tptp.e4 @t21)) % 0.37/0.65 (define @t369 () (= tptp.e4 @t23)) % 0.37/0.65 (define @t370 () (= tptp.e4 @t25)) % 0.37/0.65 (define @t371 () (or @t370 @t369 @t368 @t362 @t297)) % 0.37/0.65 (define @t372 () (@list @t368)) % 0.37/0.65 (define @t373 () (= tptp.e3 @t19)) % 0.37/0.65 (define @t374 () (= tptp.e3 @t29)) % 0.37/0.65 (define @t375 () (= tptp.e3 @t39)) % 0.37/0.65 (define @t376 () (= tptp.e3 @t49)) % 0.37/0.65 (define @t377 () (or @t376 @t375 @t374 @t373 @t317)) % 0.37/0.65 (define @t378 () (@list @t376)) % 0.37/0.65 (define @t379 () (= tptp.e3 @t21)) % 0.37/0.65 (define @t380 () (= tptp.e3 @t23)) % 0.37/0.65 (define @t381 () (= tptp.e3 @t25)) % 0.37/0.65 (define @t382 () (or @t381 @t380 @t379 @t373 @t311)) % 0.37/0.65 (define @t383 () (@list @t381)) % 0.37/0.65 (define @t384 () (= tptp.e2 @t19)) % 0.37/0.65 (define @t385 () (= tptp.e2 @t29)) % 0.37/0.65 (define @t386 () (= tptp.e2 @t39)) % 0.37/0.65 (define @t387 () (= tptp.e2 @t49)) % 0.37/0.65 (define @t388 () (or @t387 @t386 @t385 @t384 @t330)) % 0.37/0.65 (define @t389 () (= tptp.e2 @t21)) % 0.37/0.65 (define @t390 () (= tptp.e2 @t23)) % 0.37/0.65 (define @t391 () (= tptp.e2 @t25)) % 0.37/0.65 (define @t392 () (or @t391 @t390 @t389 @t384 @t324)) % 0.37/0.65 (define @t393 () (@list @t390)) % 0.37/0.65 (define @t394 () (= tptp.e1 @t19)) % 0.37/0.65 (define @t395 () (= tptp.e1 @t29)) % 0.37/0.65 (define @t396 () (= tptp.e1 @t39)) % 0.37/0.65 (define @t397 () (= tptp.e1 @t49)) % 0.37/0.65 (define @t398 () (or @t397 @t396 @t395 @t394 @t343)) % 0.37/0.65 (define @t399 () (@list @t395)) % 0.37/0.65 (define @t400 () (= tptp.e1 @t21)) % 0.37/0.65 (define @t401 () (= tptp.e1 @t23)) % 0.37/0.65 (define @t402 () (= tptp.e1 @t25)) % 0.37/0.65 (define @t403 () (or @t402 @t401 @t400 @t394 @t337)) % 0.37/0.65 (define @t404 () (= tptp.e0 @t19)) % 0.37/0.65 (define @t405 () (= tptp.e0 @t29)) % 0.37/0.65 (define @t406 () (= tptp.e0 @t39)) % 0.37/0.65 (define @t407 () (= tptp.e0 @t49)) % 0.37/0.65 (define @t408 () (or @t407 @t406 @t405 @t404 @t357)) % 0.37/0.65 (define @t409 () (not @t404)) % 0.37/0.65 (define @t410 () (@list @t404)) % 0.37/0.65 (define @t411 () (= tptp.e0 @t21)) % 0.37/0.65 (define @t412 () (= tptp.e0 @t23)) % 0.37/0.65 (define @t413 () (= tptp.e0 @t25)) % 0.37/0.65 (define @t414 () (or @t413 @t412 @t411 @t404 @t350)) % 0.37/0.65 (define @t415 () (= tptp.e4 @t31)) % 0.37/0.65 (define @t416 () (= tptp.e4 @t41)) % 0.37/0.65 (define @t417 () (= tptp.e4 @t51)) % 0.37/0.65 (define @t418 () (or @t417 @t416 @t415 @t368 @t305)) % 0.37/0.65 (define @t419 () (= tptp.e4 @t33)) % 0.37/0.65 (define @t420 () (= tptp.e4 @t35)) % 0.37/0.65 (define @t421 () (or @t420 @t419 @t415 @t363 @t298)) % 0.37/0.65 (define @t422 () (@list @t419)) % 0.37/0.65 (define @t423 () (= tptp.e3 @t31)) % 0.37/0.65 (define @t424 () (= tptp.e3 @t41)) % 0.37/0.65 (define @t425 () (= tptp.e3 @t51)) % 0.37/0.65 (define @t426 () (or @t425 @t424 @t423 @t379 @t318)) % 0.37/0.65 (define @t427 () (@list @t424)) % 0.37/0.65 (define @t428 () (= tptp.e3 @t33)) % 0.37/0.65 (define @t429 () (= tptp.e3 @t35)) % 0.37/0.65 (define @t430 () (or @t429 @t428 @t423 @t374 @t312)) % 0.37/0.65 (define @t431 () (= tptp.e2 @t31)) % 0.37/0.65 (define @t432 () (= tptp.e2 @t41)) % 0.37/0.65 (define @t433 () (= tptp.e2 @t51)) % 0.37/0.65 (define @t434 () (or @t433 @t432 @t431 @t389 @t331)) % 0.37/0.65 (define @t435 () (@list @t433)) % 0.37/0.65 (define @t436 () (= tptp.e2 @t33)) % 0.37/0.65 (define @t437 () (= tptp.e2 @t35)) % 0.37/0.65 (define @t438 () (or @t437 @t436 @t431 @t385 @t325)) % 0.37/0.65 (define @t439 () (@list @t437)) % 0.37/0.65 (define @t440 () (= tptp.e1 @t31)) % 0.37/0.65 (define @t441 () (= tptp.e1 @t41)) % 0.37/0.65 (define @t442 () (= tptp.e1 @t51)) % 0.37/0.65 (define @t443 () (or @t442 @t441 @t440 @t400 @t344)) % 0.37/0.65 (define @t444 () (= tptp.e1 @t33)) % 0.37/0.65 (define @t445 () (= tptp.e1 @t35)) % 0.37/0.65 (define @t446 () (or @t445 @t444 @t440 @t395 @t338)) % 0.37/0.65 (define @t447 () (= tptp.e0 @t31)) % 0.37/0.65 (define @t448 () (= tptp.e0 @t41)) % 0.37/0.65 (define @t449 () (= tptp.e0 @t51)) % 0.37/0.65 (define @t450 () (or @t449 @t448 @t447 @t411 @t358)) % 0.37/0.65 (define @t451 () (not @t447)) % 0.37/0.65 (define @t452 () (@list @t447)) % 0.37/0.65 (define @t453 () (= tptp.e0 @t33)) % 0.37/0.65 (define @t454 () (= tptp.e0 @t35)) % 0.37/0.65 (define @t455 () (or @t454 @t453 @t447 @t405 @t351)) % 0.37/0.65 (define @t456 () (= tptp.e4 @t43)) % 0.37/0.65 (define @t457 () (= tptp.e4 @t53)) % 0.37/0.65 (define @t458 () (or @t457 @t456 @t419 @t369 @t306)) % 0.37/0.65 (define @t459 () (= tptp.e4 @t45)) % 0.37/0.65 (define @t460 () (or @t459 @t456 @t416 @t364 @t299)) % 0.37/0.65 (define @t461 () (= tptp.e3 @t43)) % 0.37/0.65 (define @t462 () (= tptp.e3 @t53)) % 0.37/0.65 (define @t463 () (or @t462 @t461 @t428 @t380 @t319)) % 0.37/0.65 (define @t464 () (= tptp.e3 @t45)) % 0.37/0.65 (define @t465 () (or @t464 @t461 @t424 @t375 @t313)) % 0.37/0.65 (define @t466 () (= tptp.e2 @t43)) % 0.37/0.65 (define @t467 () (= tptp.e2 @t53)) % 0.37/0.65 (define @t468 () (or @t467 @t466 @t436 @t390 @t332)) % 0.37/0.65 (define @t469 () (= tptp.e2 @t45)) % 0.37/0.65 (define @t470 () (or @t469 @t466 @t432 @t386 @t326)) % 0.37/0.65 (define @t471 () (= tptp.e1 @t43)) % 0.37/0.65 (define @t472 () (= tptp.e1 @t53)) % 0.37/0.65 (define @t473 () (or @t472 @t471 @t444 @t401 @t345)) % 0.37/0.65 (define @t474 () (@list @t472)) % 0.37/0.65 (define @t475 () (= tptp.e1 @t45)) % 0.37/0.65 (define @t476 () (or @t475 @t471 @t441 @t396 @t339)) % 0.37/0.65 (define @t477 () (@list @t475)) % 0.37/0.65 (define @t478 () (= tptp.e0 @t43)) % 0.37/0.65 (define @t479 () (= tptp.e0 @t53)) % 0.37/0.65 (define @t480 () (or @t479 @t478 @t453 @t412 @t359)) % 0.37/0.65 (define @t481 () (not @t478)) % 0.37/0.65 (define @t482 () (@list @t478)) % 0.37/0.65 (define @t483 () (= tptp.e0 @t45)) % 0.37/0.65 (define @t484 () (or @t483 @t478 @t448 @t406 @t352)) % 0.37/0.65 (define @t485 () (= tptp.e4 @t55)) % 0.37/0.65 (define @t486 () (or @t485 @t459 @t420 @t370 @t307)) % 0.37/0.65 (define @t487 () (or @t485 @t457 @t417 @t365 @t300)) % 0.37/0.65 (define @t488 () (= tptp.e3 @t55)) % 0.37/0.65 (define @t489 () (or @t488 @t464 @t429 @t381 @t320)) % 0.37/0.65 (define @t490 () (or @t488 @t462 @t425 @t376 @t314)) % 0.37/0.65 (define @t491 () (= tptp.e2 @t55)) % 0.37/0.65 (define @t492 () (or @t491 @t469 @t437 @t391 @t333)) % 0.37/0.65 (define @t493 () (or @t491 @t467 @t433 @t387 @t327)) % 0.37/0.65 (define @t494 () (= tptp.e1 @t55)) % 0.37/0.65 (define @t495 () (or @t494 @t475 @t445 @t402 @t346)) % 0.37/0.65 (define @t496 () (or @t494 @t472 @t442 @t397 @t340)) % 0.37/0.65 (define @t497 () (= tptp.e0 @t55)) % 0.37/0.65 (define @t498 () (or @t497 @t483 @t454 @t413 @t360)) % 0.37/0.65 (define @t499 () (not @t497)) % 0.37/0.65 (define @t500 () (@list @t497)) % 0.37/0.65 (define @t501 () (or @t497 @t479 @t449 @t407 @t353)) % 0.37/0.65 (define @t502 () (= tptp.e0 tptp.unit)) % 0.37/0.65 (define @t503 () (or @t502 (= tptp.e1 tptp.unit) (= tptp.e2 tptp.unit) (= tptp.e3 tptp.unit) (= tptp.e4 tptp.unit))) % 0.37/0.65 (define @t504 () (or @t349 @t336 @t323 @t310 @t296)) % 0.37/0.65 (define @t505 () (or @t357 @t343 @t330 @t317 @t304)) % 0.37/0.65 (define @t506 () (or @t358 @t344 @t331 @t318 @t305)) % 0.37/0.65 (define @t507 () (or @t359 @t345 @t332 @t319 @t306)) % 0.37/0.65 (define @t508 () (or @t360 @t346 @t333 @t320 @t307)) % 0.37/0.65 (define @t509 () (or @t350 @t337 @t324 @t311 @t297)) % 0.37/0.65 (define @t510 () (or @t404 @t394 @t384 @t373 @t362)) % 0.37/0.65 (define @t511 () (or @t411 @t400 @t389 @t379 @t368)) % 0.37/0.65 (define @t512 () (or @t412 @t401 @t390 @t380 @t369)) % 0.37/0.65 (define @t513 () (or @t413 @t402 @t391 @t381 @t370)) % 0.37/0.65 (define @t514 () (or @t351 @t338 @t325 @t312 @t298)) % 0.37/0.65 (define @t515 () (or @t405 @t395 @t385 @t374 @t363)) % 0.37/0.65 (define @t516 () (or @t447 @t440 @t431 @t423 @t415)) % 0.37/0.65 (define @t517 () (or @t453 @t444 @t436 @t428 @t419)) % 0.37/0.65 (define @t518 () (or @t454 @t445 @t437 @t429 @t420)) % 0.37/0.65 (define @t519 () (or @t352 @t339 @t326 @t313 @t299)) % 0.37/0.65 (define @t520 () (or @t406 @t396 @t386 @t375 @t364)) % 0.37/0.65 (define @t521 () (or @t448 @t441 @t432 @t424 @t416)) % 0.37/0.65 (define @t522 () (or @t478 @t471 @t466 @t461 @t456)) % 0.37/0.65 (define @t523 () (or @t483 @t475 @t469 @t464 @t459)) % 0.37/0.65 (define @t524 () (or @t353 @t340 @t327 @t314 @t300)) % 0.37/0.65 (define @t525 () (or @t407 @t397 @t387 @t376 @t365)) % 0.37/0.65 (define @t526 () (or @t449 @t442 @t433 @t425 @t417)) % 0.37/0.65 (define @t527 () (or @t479 @t472 @t467 @t462 @t457)) % 0.37/0.65 (define @t528 () (or @t497 @t494 @t491 @t488 @t485)) % 0.37/0.65 (define @t529 () (not @t296)) % 0.37/0.65 (define @t530 () (or @t529 @t296)) % 0.37/0.65 (define @t531 () (not @t310)) % 0.37/0.65 (define @t532 () (not @t4)) % 0.37/0.65 (define @t533 () (= false true)) % 0.37/0.65 (define @t534 () (and @t497 @t349 @t310 @t4)) % 0.37/0.65 (define @t535 () (@list true false false)) % 0.37/0.65 (define @t536 () (or @t531 @t304)) % 0.37/0.65 (define @t537 () (@list true)) % 0.37/0.65 (define @t538 () (not @t323)) % 0.37/0.65 (define @t539 () (not @t6)) % 0.37/0.65 (define @t540 () (and @t497 @t349 @t323 @t6)) % 0.37/0.65 (define @t541 () (or @t538 @t305)) % 0.37/0.65 (define @t542 () (not @t336)) % 0.37/0.65 (define @t543 () (or @t542 @t306)) % 0.37/0.65 (define @t544 () (or @t355 @t307)) % 0.37/0.65 (define @t545 () (not @t362)) % 0.37/0.65 (define @t546 () (not @t2)) % 0.37/0.65 (define @t547 () (and @t497 @t404 @t362 @t2)) % 0.37/0.65 (define @t548 () (or @t545 @t311)) % 0.37/0.65 (define @t549 () (not @t373)) % 0.37/0.65 (define @t550 () (or @t549 @t373)) % 0.37/0.65 (define @t551 () (not @t384)) % 0.37/0.65 (define @t552 () (and @t497 @t404 @t384 @t6)) % 0.37/0.65 (define @t553 () (or @t551 @t379)) % 0.37/0.65 (define @t554 () (not @t394)) % 0.37/0.65 (define @t555 () (or @t554 @t380)) % 0.37/0.65 (define @t556 () (or @t409 @t381)) % 0.37/0.65 (define @t557 () (not @t415)) % 0.37/0.65 (define @t558 () (and @t497 @t447 @t415 @t2)) % 0.37/0.65 (define @t559 () (or @t557 @t325)) % 0.37/0.65 (define @t560 () (not @t423)) % 0.37/0.65 (define @t561 () (and @t497 @t447 @t423 @t4)) % 0.37/0.65 (define @t562 () (or @t560 @t385)) % 0.37/0.65 (define @t563 () (not @t440)) % 0.37/0.65 (define @t564 () (or @t563 @t436)) % 0.37/0.65 (define @t565 () (or @t451 @t437)) % 0.37/0.65 (define @t566 () (not @t456)) % 0.37/0.65 (define @t567 () (and @t497 @t478 @t456 @t2)) % 0.37/0.65 (define @t568 () (or @t566 @t339)) % 0.37/0.65 (define @t569 () (not @t461)) % 0.37/0.65 (define @t570 () (and @t497 @t478 @t461 @t4)) % 0.37/0.65 (define @t571 () (or @t569 @t396)) % 0.37/0.65 (define @t572 () (not @t466)) % 0.37/0.65 (define @t573 () (and @t497 @t478 @t466 @t6)) % 0.37/0.65 (define @t574 () (or @t572 @t441)) % 0.37/0.65 (define @t575 () (not @t471)) % 0.37/0.65 (define @t576 () (or @t575 @t471)) % 0.37/0.65 (define @t577 () (or @t481 @t475)) % 0.37/0.65 (define @t578 () (not @t485)) % 0.37/0.65 (define @t579 () (and @t497 @t485 @t2)) % 0.37/0.65 (define @t580 () (@list true false)) % 0.37/0.65 (define @t581 () (or @t578 @t353)) % 0.37/0.65 (define @t582 () (not @t488)) % 0.37/0.65 (define @t583 () (and @t497 @t488 @t4)) % 0.37/0.65 (define @t584 () (or @t582 @t407)) % 0.37/0.65 (define @t585 () (not @t491)) % 0.37/0.65 (define @t586 () (and @t497 @t491 @t6)) % 0.37/0.65 (define @t587 () (or @t585 @t449)) % 0.37/0.65 (define @t588 () (not @t494)) % 0.37/0.65 (define @t589 () (or @t588 @t479)) % 0.37/0.65 (define @t590 () (or @t499 @t497)) % 0.37/0.65 (define @t591 () (not @t431)) % 0.37/0.65 (define @t592 () (or @t591 @t431)) % 0.37/0.65 (assume @p1 (and (not (= tptp.e0 tptp.e1)) @t6 @t4 @t2 (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.37/0.65 (assume @p2 (and @t56 @t54 @t52 @t50 @t48 @t46 @t44 @t42 @t40 @t38 @t36 @t34 @t32 @t30 @t28 @t26 @t24 @t22 @t20 @t18 @t16 @t14 @t12 @t10 @t8)) % 0.37/0.65 (assume @p3 @t57) % 0.37/0.65 (assume @p4 @t295) % 0.37/0.65 (assume @p5 true) % 0.37/0.65 (step @p6 :rule and_elim :premises (@p2) :args (4)) % 0.37/0.65 (step @p7 :rule symm :premises (@p6)) % 0.37/0.65 (step @p8 :rule cnf_or_neg :args (@t301 0)) % 0.37/0.65 (step @p9 :rule chain_m_resolution :premises (@p8 @p7) :args (@t301 @t302 @t303)) % 0.37/0.65 (step @p10 :rule and_elim :premises (@p2) :args (20)) % 0.37/0.65 (step @p11 :rule symm :premises (@p10)) % 0.37/0.65 (step @p12 :rule cnf_or_neg :args (@t308 0)) % 0.37/0.65 (step @p13 :rule chain_m_resolution :premises (@p12 @p11) :args (@t308 @t302 @t309)) % 0.37/0.65 (step @p14 :rule and_elim :premises (@p2) :args (14)) % 0.37/0.65 (step @p15 :rule symm :premises (@p14)) % 0.37/0.65 (step @p16 :rule cnf_or_neg :args (@t315 2)) % 0.37/0.65 (step @p17 :rule chain_m_resolution :premises (@p16 @p15) :args (@t315 @t302 @t316)) % 0.37/0.65 (step @p18 :rule and_elim :premises (@p2) :args (21)) % 0.37/0.65 (step @p19 :rule symm :premises (@p18)) % 0.37/0.65 (step @p20 :rule cnf_or_neg :args (@t321 1)) % 0.37/0.65 (step @p21 :rule chain_m_resolution :premises (@p20 @p19) :args (@t321 @t302 @t322)) % 0.37/0.65 (step @p22 :rule and_elim :premises (@p2) :args (9)) % 0.37/0.65 (step @p23 :rule symm :premises (@p22)) % 0.37/0.65 (step @p24 :rule cnf_or_neg :args (@t328 1)) % 0.37/0.65 (step @p25 :rule chain_m_resolution :premises (@p24 @p23) :args (@t328 @t302 @t329)) % 0.37/0.65 (step @p26 :rule and_elim :premises (@p2) :args (23)) % 0.37/0.65 (step @p27 :rule symm :premises (@p26)) % 0.37/0.65 (step @p28 :rule cnf_or_neg :args (@t334 3)) % 0.37/0.65 (step @p29 :rule chain_m_resolution :premises (@p28 @p27) :args (@t334 @t302 @t335)) % 0.37/0.65 (step @p30 :rule and_elim :premises (@p2) :args (19)) % 0.37/0.65 (step @p31 :rule symm :premises (@p30)) % 0.37/0.65 (step @p32 :rule cnf_or_neg :args (@t341 3)) % 0.37/0.65 (step @p33 :rule chain_m_resolution :premises (@p32 @p31) :args (@t341 @t302 @t342)) % 0.37/0.65 (step @p34 :rule and_elim :premises (@p2) :args (22)) % 0.37/0.65 (step @p35 :rule symm :premises (@p34)) % 0.37/0.65 (step @p36 :rule cnf_or_neg :args (@t347 2)) % 0.37/0.65 (step @p37 :rule chain_m_resolution :premises (@p36 @p35) :args (@t347 @t302 @t348)) % 0.37/0.65 (step @p38 :rule and_elim :premises (@p2) :args (24)) % 0.37/0.65 (step @p39 :rule symm :premises (@p38)) % 0.37/0.65 (step @p40 :rule cnf_or_neg :args (@t354 4)) % 0.37/0.65 (step @p41 :rule reordering :premises (@p40) :args ((or @t355 @t354))) % 0.37/0.65 (step @p42 :rule chain_m_resolution :premises (@p41 @p39) :args (@t354 @t302 @t356)) % 0.37/0.65 (step @p43 :rule cnf_or_neg :args (@t361 4)) % 0.37/0.65 (step @p44 :rule reordering :premises (@p43) :args ((or @t355 @t361))) % 0.37/0.65 (step @p45 :rule chain_m_resolution :premises (@p44 @p39) :args (@t361 @t302 @t356)) % 0.37/0.65 (step @p46 :rule and_elim :premises (@p2) :args (8)) % 0.37/0.65 (step @p47 :rule symm :premises (@p46)) % 0.37/0.65 (step @p48 :rule cnf_or_neg :args (@t366 1)) % 0.37/0.65 (step @p49 :rule chain_m_resolution :premises (@p48 @p47) :args (@t366 @t302 @t367)) % 0.37/0.65 (step @p50 :rule and_elim :premises (@p2) :args (17)) % 0.37/0.65 (step @p51 :rule symm :premises (@p50)) % 0.37/0.65 (step @p52 :rule cnf_or_neg :args (@t371 2)) % 0.37/0.65 (step @p53 :rule chain_m_resolution :premises (@p52 @p51) :args (@t371 @t302 @t372)) % 0.37/0.65 (step @p54 :rule and_elim :premises (@p2) :args (3)) % 0.37/0.65 (step @p55 :rule symm :premises (@p54)) % 0.37/0.65 (step @p56 :rule cnf_or_neg :args (@t377 0)) % 0.37/0.65 (step @p57 :rule chain_m_resolution :premises (@p56 @p55) :args (@t377 @t302 @t378)) % 0.37/0.65 (step @p58 :rule and_elim :premises (@p2) :args (15)) % 0.37/0.65 (step @p59 :rule symm :premises (@p58)) % 0.37/0.65 (step @p60 :rule cnf_or_neg :args (@t382 0)) % 0.37/0.65 (step @p61 :rule chain_m_resolution :premises (@p60 @p59) :args (@t382 @t302 @t383)) % 0.37/0.65 (step @p62 :rule cnf_or_neg :args (@t388 4)) % 0.37/0.65 (step @p63 :rule chain_m_resolution :premises (@p62 @p27) :args (@t388 @t302 @t335)) % 0.37/0.65 (step @p64 :rule and_elim :premises (@p2) :args (16)) % 0.37/0.65 (step @p65 :rule symm :premises (@p64)) % 0.37/0.65 (step @p66 :rule cnf_or_neg :args (@t392 1)) % 0.37/0.65 (step @p67 :rule chain_m_resolution :premises (@p66 @p65) :args (@t392 @t302 @t393)) % 0.37/0.65 (step @p68 :rule and_elim :premises (@p2) :args (13)) % 0.37/0.65 (step @p69 :rule symm :premises (@p68)) % 0.37/0.65 (step @p70 :rule cnf_or_neg :args (@t398 2)) % 0.37/0.65 (step @p71 :rule chain_m_resolution :premises (@p70 @p69) :args (@t398 @t302 @t399)) % 0.37/0.65 (step @p72 :rule cnf_or_neg :args (@t403 4)) % 0.37/0.65 (step @p73 :rule chain_m_resolution :premises (@p72 @p31) :args (@t403 @t302 @t342)) % 0.37/0.65 (step @p74 :rule and_elim :premises (@p2) :args (18)) % 0.37/0.65 (step @p75 :rule symm :premises (@p74)) % 0.37/0.65 (step @p76 :rule cnf_or_neg :args (@t408 3)) % 0.37/0.65 (step @p77 :rule reordering :premises (@p76) :args ((or @t409 @t408))) % 0.37/0.65 (step @p78 :rule chain_m_resolution :premises (@p77 @p75) :args (@t408 @t302 @t410)) % 0.37/0.65 (step @p79 :rule cnf_or_neg :args (@t414 3)) % 0.37/0.65 (step @p80 :rule reordering :premises (@p79) :args ((or @t409 @t414))) % 0.37/0.65 (step @p81 :rule chain_m_resolution :premises (@p80 @p75) :args (@t414 @t302 @t410)) % 0.37/0.65 (step @p82 :rule cnf_or_neg :args (@t418 3)) % 0.37/0.65 (step @p83 :rule chain_m_resolution :premises (@p82 @p51) :args (@t418 @t302 @t372)) % 0.37/0.65 (step @p84 :rule and_elim :premises (@p2) :args (11)) % 0.37/0.65 (step @p85 :rule symm :premises (@p84)) % 0.37/0.65 (step @p86 :rule cnf_or_neg :args (@t421 1)) % 0.37/0.65 (step @p87 :rule chain_m_resolution :premises (@p86 @p85) :args (@t421 @t302 @t422)) % 0.37/0.65 (step @p88 :rule and_elim :premises (@p2) :args (7)) % 0.37/0.65 (step @p89 :rule symm :premises (@p88)) % 0.37/0.65 (step @p90 :rule cnf_or_neg :args (@t426 1)) % 0.37/0.65 (step @p91 :rule chain_m_resolution :premises (@p90 @p89) :args (@t426 @t302 @t427)) % 0.37/0.65 (step @p92 :rule cnf_or_neg :args (@t430 4)) % 0.37/0.65 (step @p93 :rule chain_m_resolution :premises (@p92 @p15) :args (@t430 @t302 @t316)) % 0.37/0.65 (step @p94 :rule and_elim :premises (@p2) :args (2)) % 0.37/0.65 (step @p95 :rule symm :premises (@p94)) % 0.37/0.65 (step @p96 :rule cnf_or_neg :args (@t434 0)) % 0.37/0.65 (step @p97 :rule chain_m_resolution :premises (@p96 @p95) :args (@t434 @t302 @t435)) % 0.37/0.65 (step @p98 :rule and_elim :premises (@p2) :args (10)) % 0.37/0.65 (step @p99 :rule symm :premises (@p98)) % 0.37/0.65 (step @p100 :rule cnf_or_neg :args (@t438 0)) % 0.37/0.65 (step @p101 :rule chain_m_resolution :premises (@p100 @p99) :args (@t438 @t302 @t439)) % 0.37/0.65 (step @p102 :rule cnf_or_neg :args (@t443 4)) % 0.37/0.65 (step @p103 :rule chain_m_resolution :premises (@p102 @p35) :args (@t443 @t302 @t348)) % 0.37/0.65 (step @p104 :rule cnf_or_neg :args (@t446 3)) % 0.37/0.65 (step @p105 :rule chain_m_resolution :premises (@p104 @p69) :args (@t446 @t302 @t399)) % 0.37/0.65 (step @p106 :rule and_elim :premises (@p2) :args (12)) % 0.37/0.65 (step @p107 :rule symm :premises (@p106)) % 0.37/0.65 (step @p108 :rule cnf_or_neg :args (@t450 2)) % 0.37/0.65 (step @p109 :rule reordering :premises (@p108) :args ((or @t451 @t450))) % 0.37/0.65 (step @p110 :rule chain_m_resolution :premises (@p109 @p107) :args (@t450 @t302 @t452)) % 0.37/0.65 (step @p111 :rule cnf_or_neg :args (@t455 2)) % 0.37/0.65 (step @p112 :rule reordering :premises (@p111) :args ((or @t451 @t455))) % 0.37/0.65 (step @p113 :rule chain_m_resolution :premises (@p112 @p107) :args (@t455 @t302 @t452)) % 0.37/0.65 (step @p114 :rule cnf_or_neg :args (@t458 2)) % 0.37/0.65 (step @p115 :rule chain_m_resolution :premises (@p114 @p85) :args (@t458 @t302 @t422)) % 0.37/0.65 (step @p116 :rule cnf_or_neg :args (@t460 3)) % 0.37/0.65 (step @p117 :rule chain_m_resolution :premises (@p116 @p47) :args (@t460 @t302 @t367)) % 0.37/0.65 (step @p118 :rule cnf_or_neg :args (@t463 4)) % 0.37/0.65 (step @p119 :rule chain_m_resolution :premises (@p118 @p19) :args (@t463 @t302 @t322)) % 0.37/0.65 (step @p120 :rule cnf_or_neg :args (@t465 2)) % 0.37/0.65 (step @p121 :rule chain_m_resolution :premises (@p120 @p89) :args (@t465 @t302 @t427)) % 0.37/0.65 (step @p122 :rule cnf_or_neg :args (@t468 3)) % 0.37/0.65 (step @p123 :rule chain_m_resolution :premises (@p122 @p65) :args (@t468 @t302 @t393)) % 0.37/0.65 (step @p124 :rule cnf_or_neg :args (@t470 4)) % 0.37/0.65 (step @p125 :rule chain_m_resolution :premises (@p124 @p23) :args (@t470 @t302 @t329)) % 0.37/0.65 (step @p126 :rule and_elim :premises (@p2) :args (1)) % 0.37/0.65 (step @p127 :rule symm :premises (@p126)) % 0.37/0.65 (step @p128 :rule cnf_or_neg :args (@t473 0)) % 0.37/0.65 (step @p129 :rule chain_m_resolution :premises (@p128 @p127) :args (@t473 @t302 @t474)) % 0.37/0.65 (step @p130 :rule and_elim :premises (@p2) :args (5)) % 0.37/0.65 (step @p131 :rule symm :premises (@p130)) % 0.37/0.65 (step @p132 :rule cnf_or_neg :args (@t476 0)) % 0.37/0.65 (step @p133 :rule chain_m_resolution :premises (@p132 @p131) :args (@t476 @t302 @t477)) % 0.37/0.65 (step @p134 :rule and_elim :premises (@p2) :args (6)) % 0.37/0.65 (step @p135 :rule symm :premises (@p134)) % 0.37/0.65 (step @p136 :rule cnf_or_neg :args (@t480 1)) % 0.37/0.65 (step @p137 :rule reordering :premises (@p136) :args ((or @t481 @t480))) % 0.37/0.65 (step @p138 :rule chain_m_resolution :premises (@p137 @p135) :args (@t480 @t302 @t482)) % 0.37/0.65 (step @p139 :rule cnf_or_neg :args (@t484 1)) % 0.37/0.65 (step @p140 :rule reordering :premises (@p139) :args ((or @t481 @t484))) % 0.37/0.65 (step @p141 :rule chain_m_resolution :premises (@p140 @p135) :args (@t484 @t302 @t482)) % 0.37/0.65 (step @p142 :rule cnf_or_neg :args (@t486 4)) % 0.37/0.65 (step @p143 :rule chain_m_resolution :premises (@p142 @p11) :args (@t486 @t302 @t309)) % 0.37/0.65 (step @p144 :rule cnf_or_neg :args (@t487 4)) % 0.37/0.65 (step @p145 :rule chain_m_resolution :premises (@p144 @p7) :args (@t487 @t302 @t303)) % 0.37/0.65 (step @p146 :rule cnf_or_neg :args (@t489 3)) % 0.37/0.65 (step @p147 :rule chain_m_resolution :premises (@p146 @p59) :args (@t489 @t302 @t383)) % 0.37/0.65 (step @p148 :rule cnf_or_neg :args (@t490 3)) % 0.37/0.65 (step @p149 :rule chain_m_resolution :premises (@p148 @p55) :args (@t490 @t302 @t378)) % 0.37/0.65 (step @p150 :rule cnf_or_neg :args (@t492 2)) % 0.37/0.65 (step @p151 :rule chain_m_resolution :premises (@p150 @p99) :args (@t492 @t302 @t439)) % 0.37/0.65 (step @p152 :rule cnf_or_neg :args (@t493 2)) % 0.37/0.65 (step @p153 :rule chain_m_resolution :premises (@p152 @p95) :args (@t493 @t302 @t435)) % 0.37/0.65 (step @p154 :rule cnf_or_neg :args (@t495 1)) % 0.37/0.65 (step @p155 :rule chain_m_resolution :premises (@p154 @p131) :args (@t495 @t302 @t477)) % 0.37/0.65 (step @p156 :rule cnf_or_neg :args (@t496 1)) % 0.37/0.65 (step @p157 :rule chain_m_resolution :premises (@p156 @p127) :args (@t496 @t302 @t474)) % 0.37/0.65 (step @p158 :rule and_elim :premises (@p2) :args (0)) % 0.37/0.65 (step @p159 :rule symm :premises (@p158)) % 0.37/0.65 (step @p160 :rule cnf_or_neg :args (@t498 0)) % 0.37/0.65 (step @p161 :rule reordering :premises (@p160) :args ((or @t499 @t498))) % 0.37/0.65 (step @p162 :rule chain_m_resolution :premises (@p161 @p159) :args (@t498 @t302 @t500)) % 0.37/0.65 (step @p163 :rule cnf_or_neg :args (@t501 0)) % 0.37/0.65 (step @p164 :rule reordering :premises (@p163) :args ((or @t499 @t501))) % 0.37/0.65 (step @p165 :rule chain_m_resolution :premises (@p164 @p159) :args (@t501 @t302 @t500)) % 0.37/0.65 (step @p166 :rule symm :premises (@p3)) % 0.37/0.65 (step @p167 :rule cnf_or_neg :args (@t503 0)) % 0.37/0.65 (step @p168 :rule chain_m_resolution :premises (@p167 @p166) :args (@t503 @t302 (@list @t502))) % 0.37/0.65 (step @p169 :rule refl :args (tptp.e4)) % 0.37/0.65 (step @p170 :rule cong :premises (@p169 @p166) :args (@t15)) % 0.37/0.65 (step @p171 :rule trans :premises (@p11 @p170)) % 0.37/0.65 (step @p172 :rule cong :premises (@p166 @p169) :args (@t47)) % 0.37/0.65 (step @p173 :rule trans :premises (@p7 @p172)) % 0.37/0.65 (step @p174 :rule refl :args (tptp.e3)) % 0.37/0.65 (step @p175 :rule cong :premises (@p174 @p166) :args (@t25)) % 0.37/0.65 (step @p176 :rule trans :premises (@p59 @p175)) % 0.37/0.65 (step @p177 :rule cong :premises (@p166 @p174) :args (@t49)) % 0.37/0.65 (step @p178 :rule trans :premises (@p55 @p177)) % 0.37/0.65 (step @p179 :rule refl :args (tptp.e2)) % 0.37/0.65 (step @p180 :rule cong :premises (@p179 @p166) :args (@t35)) % 0.37/0.65 (step @p181 :rule trans :premises (@p99 @p180)) % 0.37/0.65 (step @p182 :rule cong :premises (@p166 @p179) :args (@t51)) % 0.37/0.65 (step @p183 :rule trans :premises (@p95 @p182)) % 0.37/0.65 (step @p184 :rule refl :args (tptp.e1)) % 0.37/0.65 (step @p185 :rule cong :premises (@p184 @p166) :args (@t45)) % 0.37/0.65 (step @p186 :rule trans :premises (@p131 @p185)) % 0.37/0.65 (step @p187 :rule cong :premises (@p166 @p184) :args (@t53)) % 0.37/0.65 (step @p188 :rule trans :premises (@p127 @p187)) % 0.37/0.65 (step @p189 :rule refl :args (tptp.e0)) % 0.37/0.65 (step @p190 :rule cong :premises (@p189 @p166) :args (@t55)) % 0.37/0.65 (step @p191 :rule trans :premises (@p159 @p190)) % 0.37/0.65 (step @p192 :rule cong :premises (@p166 @p189) :args (@t55)) % 0.37/0.65 (step @p193 :rule trans :premises (@p159 @p192)) % 0.37/0.65 (step @p194 :rule cnf_or_neg :args (@t504 0)) % 0.37/0.65 (step @p195 :rule reordering :premises (@p194) :args ((or @t355 @t504))) % 0.37/0.65 (step @p196 :rule chain_m_resolution :premises (@p195 @p39) :args (@t504 @t302 @t356)) % 0.37/0.65 (step @p197 :rule cnf_or_neg :args (@t505 2)) % 0.37/0.65 (step @p198 :rule chain_m_resolution :premises (@p197 @p27) :args (@t505 @t302 @t335)) % 0.37/0.65 (step @p199 :rule cnf_or_neg :args (@t506 1)) % 0.37/0.65 (step @p200 :rule chain_m_resolution :premises (@p199 @p35) :args (@t506 @t302 @t348)) % 0.37/0.65 (step @p201 :rule cnf_or_neg :args (@t507 3)) % 0.37/0.65 (step @p202 :rule chain_m_resolution :premises (@p201 @p19) :args (@t507 @t302 @t322)) % 0.37/0.65 (step @p203 :rule cnf_or_neg :args (@t508 4)) % 0.37/0.65 (step @p204 :rule chain_m_resolution :premises (@p203 @p11) :args (@t508 @t302 @t309)) % 0.37/0.65 (step @p205 :rule cnf_or_neg :args (@t509 1)) % 0.37/0.65 (step @p206 :rule chain_m_resolution :premises (@p205 @p31) :args (@t509 @t302 @t342)) % 0.37/0.65 (step @p207 :rule cnf_or_neg :args (@t510 0)) % 0.37/0.65 (step @p208 :rule reordering :premises (@p207) :args ((or @t409 @t510))) % 0.37/0.65 (step @p209 :rule chain_m_resolution :premises (@p208 @p75) :args (@t510 @t302 @t410)) % 0.37/0.65 (step @p210 :rule cnf_or_neg :args (@t511 4)) % 0.37/0.65 (step @p211 :rule chain_m_resolution :premises (@p210 @p51) :args (@t511 @t302 @t372)) % 0.37/0.65 (step @p212 :rule cnf_or_neg :args (@t512 2)) % 0.37/0.65 (step @p213 :rule chain_m_resolution :premises (@p212 @p65) :args (@t512 @t302 @t393)) % 0.37/0.65 (step @p214 :rule cnf_or_neg :args (@t513 3)) % 0.37/0.65 (step @p215 :rule chain_m_resolution :premises (@p214 @p59) :args (@t513 @t302 @t383)) % 0.37/0.65 (step @p216 :rule cnf_or_neg :args (@t514 3)) % 0.37/0.65 (step @p217 :rule chain_m_resolution :premises (@p216 @p15) :args (@t514 @t302 @t316)) % 0.37/0.65 (step @p218 :rule cnf_or_neg :args (@t515 1)) % 0.37/0.65 (step @p219 :rule chain_m_resolution :premises (@p218 @p69) :args (@t515 @t302 @t399)) % 0.37/0.65 (step @p220 :rule cnf_or_neg :args (@t516 0)) % 0.37/0.65 (step @p221 :rule reordering :premises (@p220) :args ((or @t451 @t516))) % 0.37/0.65 (step @p222 :rule chain_m_resolution :premises (@p221 @p107) :args (@t516 @t302 @t452)) % 0.37/0.65 (step @p223 :rule cnf_or_neg :args (@t517 4)) % 0.37/0.65 (step @p224 :rule chain_m_resolution :premises (@p223 @p85) :args (@t517 @t302 @t422)) % 0.37/0.65 (step @p225 :rule cnf_or_neg :args (@t518 2)) % 0.37/0.65 (step @p226 :rule chain_m_resolution :premises (@p225 @p99) :args (@t518 @t302 @t439)) % 0.37/0.65 (step @p227 :rule cnf_or_neg :args (@t519 2)) % 0.37/0.65 (step @p228 :rule chain_m_resolution :premises (@p227 @p23) :args (@t519 @t302 @t329)) % 0.37/0.65 (step @p229 :rule cnf_or_neg :args (@t520 4)) % 0.37/0.65 (step @p230 :rule chain_m_resolution :premises (@p229 @p47) :args (@t520 @t302 @t367)) % 0.37/0.65 (step @p231 :rule cnf_or_neg :args (@t521 3)) % 0.37/0.65 (step @p232 :rule chain_m_resolution :premises (@p231 @p89) :args (@t521 @t302 @t427)) % 0.37/0.65 (step @p233 :rule cnf_or_neg :args (@t522 0)) % 0.37/0.65 (step @p234 :rule reordering :premises (@p233) :args ((or @t481 @t522))) % 0.37/0.65 (step @p235 :rule chain_m_resolution :premises (@p234 @p135) :args (@t522 @t302 @t482)) % 0.37/0.65 (step @p236 :rule cnf_or_neg :args (@t523 1)) % 0.37/0.65 (step @p237 :rule chain_m_resolution :premises (@p236 @p131) :args (@t523 @t302 @t477)) % 0.37/0.65 (step @p238 :rule cnf_or_neg :args (@t524 4)) % 0.37/0.65 (step @p239 :rule chain_m_resolution :premises (@p238 @p7) :args (@t524 @t302 @t303)) % 0.37/0.65 (step @p240 :rule cnf_or_neg :args (@t525 3)) % 0.37/0.65 (step @p241 :rule chain_m_resolution :premises (@p240 @p55) :args (@t525 @t302 @t378)) % 0.37/0.65 (step @p242 :rule cnf_or_neg :args (@t526 2)) % 0.37/0.65 (step @p243 :rule chain_m_resolution :premises (@p242 @p95) :args (@t526 @t302 @t435)) % 0.37/0.65 (step @p244 :rule cnf_or_neg :args (@t527 1)) % 0.37/0.65 (step @p245 :rule chain_m_resolution :premises (@p244 @p127) :args (@t527 @t302 @t474)) % 0.37/0.65 (step @p246 :rule cnf_or_neg :args (@t528 0)) % 0.37/0.65 (step @p247 :rule reordering :premises (@p246) :args ((or @t499 @t528))) % 0.37/0.65 (step @p248 :rule chain_m_resolution :premises (@p247 @p159) :args (@t528 @t302 @t500)) % 0.37/0.65 (step @p249 :rule bool-double-not-elim :args (@t296)) % 0.37/0.65 (step @p250 :rule refl :args (@t530)) % 0.37/0.65 (step @p251 :rule nary_cong :premises (@p250 @p249) :args ((or @t530 (not @t529)))) % 0.37/0.65 (step @p252 :rule cnf_or_neg :args (@t530 0)) % 0.37/0.65 (step @p253 :rule eq_resolve :premises (@p252 @p251)) % 0.37/0.65 (step @p254 :rule reordering :premises (@p253) :args ((or @t296 @t530))) % 0.37/0.65 (step @p255 :rule cnf_or_neg :args (@t530 1)) % 0.37/0.65 (step @p256 :rule reordering :premises (@p255) :args ((or @t529 @t530))) % 0.37/0.65 (step @p257 :rule chain_m_resolution :premises (@p256 @p254) :args (@t530 @t302 (@list @t296))) % 0.37/0.65 (step @p258 :rule and_elim :premises (@p1) :args (2)) % 0.37/0.65 (step @p259 :rule refl :args (@t531)) % 0.37/0.65 (step @p260 :rule refl :args (@t499)) % 0.37/0.65 (step @p261 :rule refl :args (@t355)) % 0.37/0.65 (step @p262 :rule bool-double-not-elim :args (@t3)) % 0.37/0.65 (step @p263 :rule nary_cong :premises (@p262 @p261 @p260 @p259) :args ((or @t532 @t355 @t499 @t531))) % 0.37/0.65 (assume-push @p1092 @t497) % 0.37/0.65 (assume-push @p1093 @t349) % 0.37/0.65 (assume-push @p1094 @t310) % 0.37/0.65 (assume-push @p1095 @t4) % 0.37/0.65 (step @p268 :rule evaluate :args (@t533)) % 0.37/0.65 (step @p269 :rule trans :premises (@p1094 @p38 @p159)) % 0.37/0.65 (step @p270 :rule symm :premises (@p269)) % 0.37/0.65 (step @p271 :rule trans :premises (@p159 @p270)) % 0.37/0.65 (step @p272 :rule true_intro :premises (@p271)) % 0.37/0.65 (step @p273 :rule false_intro :premises (@p258)) % 0.37/0.65 (step @p274 :rule symm :premises (@p273)) % 0.37/0.65 (step @p275 :rule trans :premises (@p274 @p272)) % 0.37/0.65 (step @p276 false :rule eq_resolve :premises (@p275 @p268)) % 0.37/0.65 (step-pop @p1096 :rule scope :premises (@p276)) % 0.37/0.65 (step-pop @p1097 :rule scope :premises (@p1096)) % 0.37/0.65 (step-pop @p1098 :rule scope :premises (@p1097)) % 0.37/0.65 (step-pop @p1099 :rule scope :premises (@p1098)) % 0.37/0.65 (step @p277 :rule process_scope :premises (@p1099) :args (false)) % 0.37/0.65 (assume-push @p1100 @t4) % 0.37/0.65 (assume-push @p1101 @t349) % 0.37/0.65 (assume-push @p1102 @t497) % 0.37/0.65 (assume-push @p1103 @t310) % 0.37/0.65 (step @p286 :rule and_intro :premises (@p159 @p39 @p1103 @p258)) % 0.37/0.65 (step-pop @p1104 :rule scope :premises (@p286)) % 0.37/0.65 (step-pop @p1105 :rule scope :premises (@p1104)) % 0.37/0.65 (step-pop @p1106 :rule scope :premises (@p1105)) % 0.37/0.65 (step-pop @p1107 :rule scope :premises (@p1106)) % 0.37/0.65 (step @p287 :rule process_scope :premises (@p1107) :args (@t534)) % 0.37/0.65 (step @p292 :rule implies_elim :premises (@p287)) % 0.37/0.65 (step @p293 :rule resolution :premises (@p292 @p277) :args (true @t534)) % 0.37/0.65 (step @p294 :rule not_and :premises (@p293)) % 0.37/0.65 (step @p295 :rule eq_resolve :premises (@p294 @p263)) % 0.37/0.65 (step @p296 :rule reordering :premises (@p295) :args ((or @t3 @t499 @t355 @t531))) % 0.37/0.65 (step @p297 :rule chain_m_resolution :premises (@p296 @p258 @p159 @p39) :args (@t531 @t535 (@list @t3 @t497 @t349))) % 0.37/0.65 (step @p298 :rule bool-double-not-elim :args (@t310)) % 0.37/0.65 (step @p299 :rule refl :args (@t536)) % 0.37/0.65 (step @p300 :rule nary_cong :premises (@p299 @p298) :args ((or @t536 (not @t531)))) % 0.37/0.65 (step @p301 :rule cnf_or_neg :args (@t536 0)) % 0.37/0.65 (step @p302 :rule eq_resolve :premises (@p301 @p300)) % 0.37/0.65 (step @p303 :rule reordering :premises (@p302) :args ((or @t310 @t536))) % 0.37/0.65 (step @p304 :rule chain_m_resolution :premises (@p303 @p297) :args (@t536 @t537 (@list @t310))) % 0.37/0.65 (step @p305 :rule and_elim :premises (@p1) :args (1)) % 0.37/0.65 (step @p306 :rule refl :args (@t538)) % 0.37/0.65 (step @p307 :rule bool-double-not-elim :args (@t5)) % 0.37/0.65 (step @p308 :rule nary_cong :premises (@p307 @p261 @p260 @p306) :args ((or @t539 @t355 @t499 @t538))) % 0.37/0.65 (assume-push @p1108 @t497) % 0.37/0.65 (assume-push @p1109 @t349) % 0.37/0.65 (assume-push @p1110 @t323) % 0.37/0.65 (assume-push @p1111 @t6) % 0.37/0.65 (step @p268 :rule evaluate :args (@t533)) % 0.37/0.65 (step @p313 :rule trans :premises (@p1110 @p38 @p159)) % 0.37/0.65 (step @p314 :rule symm :premises (@p313)) % 0.37/0.65 (step @p315 :rule trans :premises (@p159 @p314)) % 0.37/0.65 (step @p316 :rule true_intro :premises (@p315)) % 0.37/0.65 (step @p317 :rule false_intro :premises (@p305)) % 0.37/0.65 (step @p318 :rule symm :premises (@p317)) % 0.37/0.65 (step @p319 :rule trans :premises (@p318 @p316)) % 0.37/0.65 (step @p320 false :rule eq_resolve :premises (@p319 @p268)) % 0.37/0.65 (step-pop @p1112 :rule scope :premises (@p320)) % 0.37/0.65 (step-pop @p1113 :rule scope :premises (@p1112)) % 0.37/0.65 (step-pop @p1114 :rule scope :premises (@p1113)) % 0.37/0.65 (step-pop @p1115 :rule scope :premises (@p1114)) % 0.37/0.65 (step @p321 :rule process_scope :premises (@p1115) :args (false)) % 0.37/0.65 (assume-push @p1116 @t6) % 0.37/0.65 (assume-push @p1117 @t349) % 0.37/0.65 (assume-push @p1118 @t497) % 0.37/0.65 (assume-push @p1119 @t323) % 0.37/0.65 (step @p330 :rule and_intro :premises (@p159 @p39 @p1119 @p305)) % 0.37/0.65 (step-pop @p1120 :rule scope :premises (@p330)) % 0.37/0.65 (step-pop @p1121 :rule scope :premises (@p1120)) % 0.37/0.65 (step-pop @p1122 :rule scope :premises (@p1121)) % 0.37/0.65 (step-pop @p1123 :rule scope :premises (@p1122)) % 0.37/0.65 (step @p331 :rule process_scope :premises (@p1123) :args (@t540)) % 0.37/0.65 (step @p336 :rule implies_elim :premises (@p331)) % 0.37/0.65 (step @p337 :rule resolution :premises (@p336 @p321) :args (true @t540)) % 0.37/0.65 (step @p338 :rule not_and :premises (@p337)) % 0.37/0.65 (step @p339 :rule eq_resolve :premises (@p338 @p308)) % 0.37/0.65 (step @p340 :rule reordering :premises (@p339) :args ((or @t5 @t499 @t355 @t538))) % 0.37/0.65 (step @p341 :rule chain_m_resolution :premises (@p340 @p305 @p159 @p39) :args (@t538 @t535 (@list @t5 @t497 @t349))) % 0.37/0.65 (step @p342 :rule bool-double-not-elim :args (@t323)) % 0.37/0.65 (step @p343 :rule refl :args (@t541)) % 0.37/0.65 (step @p344 :rule nary_cong :premises (@p343 @p342) :args ((or @t541 (not @t538)))) % 0.37/0.65 (step @p345 :rule cnf_or_neg :args (@t541 0)) % 0.37/0.65 (step @p346 :rule eq_resolve :premises (@p345 @p344)) % 0.37/0.65 (step @p347 :rule reordering :premises (@p346) :args ((or @t323 @t541))) % 0.37/0.65 (step @p348 :rule chain_m_resolution :premises (@p347 @p341) :args (@t541 @t537 (@list @t323))) % 0.37/0.65 (step @p349 :rule and_elim :premises (@p1) :args (0)) % 0.37/0.65 (step @p350 :rule symm :premises (@p349)) % 0.37/0.65 (step @p351 :rule false_intro :premises (@p350)) % 0.37/0.65 (step @p352 :rule cong :premises (@p184 @p38) :args (@t336)) % 0.37/0.65 (step @p353 :rule trans :premises (@p352 @p351)) % 0.37/0.65 (step @p354 :rule false_elim :premises (@p353)) % 0.37/0.65 (step @p355 :rule bool-double-not-elim :args (@t336)) % 0.37/0.65 (step @p356 :rule refl :args (@t543)) % 0.37/0.65 (step @p357 :rule nary_cong :premises (@p356 @p355) :args ((or @t543 (not @t542)))) % 0.37/0.65 (step @p358 :rule cnf_or_neg :args (@t543 0)) % 0.37/0.65 (step @p359 :rule eq_resolve :premises (@p358 @p357)) % 0.37/0.65 (step @p360 :rule reordering :premises (@p359) :args ((or @t336 @t543))) % 0.37/0.65 (step @p361 :rule chain_m_resolution :premises (@p360 @p354) :args (@t543 @t537 (@list @t336))) % 0.37/0.65 (step @p362 :rule cnf_or_neg :args (@t544 1)) % 0.37/0.65 (step @p363 :rule chain_m_resolution :premises (@p362 @p11) :args (@t544 @t302 @t309)) % 0.37/0.65 (step @p364 :rule and_elim :premises (@p1) :args (3)) % 0.37/0.65 (step @p365 :rule refl :args (@t545)) % 0.37/0.65 (step @p366 :rule refl :args (@t409)) % 0.37/0.65 (step @p367 :rule bool-double-not-elim :args (@t1)) % 0.37/0.65 (step @p368 :rule nary_cong :premises (@p367 @p366 @p260 @p365) :args ((or @t546 @t409 @t499 @t545))) % 0.37/0.65 (assume-push @p1124 @t497) % 0.37/0.65 (assume-push @p1125 @t404) % 0.37/0.65 (assume-push @p1126 @t362) % 0.37/0.65 (assume-push @p1127 @t2) % 0.37/0.65 (step @p268 :rule evaluate :args (@t533)) % 0.37/0.65 (step @p373 :rule trans :premises (@p1126 @p74 @p159)) % 0.37/0.65 (step @p374 :rule symm :premises (@p373)) % 0.37/0.65 (step @p375 :rule trans :premises (@p159 @p374)) % 0.37/0.65 (step @p376 :rule true_intro :premises (@p375)) % 0.37/0.65 (step @p377 :rule false_intro :premises (@p364)) % 0.37/0.65 (step @p378 :rule symm :premises (@p377)) % 0.37/0.65 (step @p379 :rule trans :premises (@p378 @p376)) % 0.37/0.65 (step @p380 false :rule eq_resolve :premises (@p379 @p268)) % 0.37/0.65 (step-pop @p1128 :rule scope :premises (@p380)) % 0.37/0.65 (step-pop @p1129 :rule scope :premises (@p1128)) % 0.37/0.65 (step-pop @p1130 :rule scope :premises (@p1129)) % 0.37/0.65 (step-pop @p1131 :rule scope :premises (@p1130)) % 0.37/0.65 (step @p381 :rule process_scope :premises (@p1131) :args (false)) % 0.37/0.65 (assume-push @p1132 @t2) % 0.37/0.65 (assume-push @p1133 @t404) % 0.37/0.65 (assume-push @p1134 @t497) % 0.37/0.65 (assume-push @p1135 @t362) % 0.37/0.65 (step @p390 :rule and_intro :premises (@p159 @p75 @p1135 @p364)) % 0.37/0.65 (step-pop @p1136 :rule scope :premises (@p390)) % 0.37/0.65 (step-pop @p1137 :rule scope :premises (@p1136)) % 0.37/0.65 (step-pop @p1138 :rule scope :premises (@p1137)) % 0.37/0.65 (step-pop @p1139 :rule scope :premises (@p1138)) % 0.37/0.65 (step @p391 :rule process_scope :premises (@p1139) :args (@t547)) % 0.37/0.65 (step @p396 :rule implies_elim :premises (@p391)) % 0.37/0.65 (step @p397 :rule resolution :premises (@p396 @p381) :args (true @t547)) % 0.37/0.65 (step @p398 :rule not_and :premises (@p397)) % 0.37/0.65 (step @p399 :rule eq_resolve :premises (@p398 @p368)) % 0.37/0.65 (step @p400 :rule reordering :premises (@p399) :args ((or @t1 @t499 @t409 @t545))) % 0.37/0.65 (step @p401 :rule chain_m_resolution :premises (@p400 @p364 @p159 @p75) :args (@t545 @t535 (@list @t1 @t497 @t404))) % 0.37/0.65 (step @p402 :rule bool-double-not-elim :args (@t362)) % 0.37/0.65 (step @p403 :rule refl :args (@t548)) % 0.37/0.65 (step @p404 :rule nary_cong :premises (@p403 @p402) :args ((or @t548 (not @t545)))) % 0.37/0.65 (step @p405 :rule cnf_or_neg :args (@t548 0)) % 0.37/0.65 (step @p406 :rule eq_resolve :premises (@p405 @p404)) % 0.37/0.65 (step @p407 :rule reordering :premises (@p406) :args ((or @t362 @t548))) % 0.37/0.65 (step @p408 :rule chain_m_resolution :premises (@p407 @p401) :args (@t548 @t537 (@list @t362))) % 0.37/0.65 (step @p409 :rule bool-double-not-elim :args (@t373)) % 0.37/0.65 (step @p410 :rule refl :args (@t550)) % 0.37/0.65 (step @p411 :rule nary_cong :premises (@p410 @p409) :args ((or @t550 (not @t549)))) % 0.37/0.65 (step @p412 :rule cnf_or_neg :args (@t550 0)) % 0.37/0.65 (step @p413 :rule eq_resolve :premises (@p412 @p411)) % 0.37/0.65 (step @p414 :rule reordering :premises (@p413) :args ((or @t373 @t550))) % 0.37/0.65 (step @p415 :rule cnf_or_neg :args (@t550 1)) % 0.37/0.65 (step @p416 :rule reordering :premises (@p415) :args ((or @t549 @t550))) % 0.37/0.65 (step @p417 :rule chain_m_resolution :premises (@p416 @p414) :args (@t550 @t302 (@list @t373))) % 0.37/0.65 (step @p418 :rule refl :args (@t551)) % 0.37/0.65 (step @p419 :rule nary_cong :premises (@p307 @p366 @p260 @p418) :args ((or @t539 @t409 @t499 @t551))) % 0.37/0.65 (assume-push @p1140 @t497) % 0.37/0.65 (assume-push @p1141 @t404) % 0.37/0.65 (assume-push @p1142 @t384) % 0.37/0.65 (assume-push @p1143 @t6) % 0.37/0.65 (step @p268 :rule evaluate :args (@t533)) % 0.37/0.65 (step @p424 :rule trans :premises (@p1142 @p74 @p159)) % 0.37/0.65 (step @p425 :rule symm :premises (@p424)) % 0.37/0.65 (step @p426 :rule trans :premises (@p159 @p425)) % 0.37/0.65 (step @p427 :rule true_intro :premises (@p426)) % 0.37/0.65 (step @p317 :rule false_intro :premises (@p305)) % 0.37/0.65 (step @p318 :rule symm :premises (@p317)) % 0.37/0.65 (step @p428 :rule trans :premises (@p318 @p427)) % 0.37/0.65 (step @p429 false :rule eq_resolve :premises (@p428 @p268)) % 0.37/0.65 (step-pop @p1144 :rule scope :premises (@p429)) % 0.37/0.65 (step-pop @p1145 :rule scope :premises (@p1144)) % 0.37/0.65 (step-pop @p1146 :rule scope :premises (@p1145)) % 0.37/0.65 (step-pop @p1147 :rule scope :premises (@p1146)) % 0.37/0.65 (step @p430 :rule process_scope :premises (@p1147) :args (false)) % 0.37/0.65 (assume-push @p1148 @t6) % 0.37/0.65 (assume-push @p1149 @t404) % 0.37/0.65 (assume-push @p1150 @t497) % 0.37/0.65 (assume-push @p1151 @t384) % 0.37/0.65 (step @p439 :rule and_intro :premises (@p159 @p75 @p1151 @p305)) % 0.37/0.65 (step-pop @p1152 :rule scope :premises (@p439)) % 0.37/0.65 (step-pop @p1153 :rule scope :premises (@p1152)) % 0.37/0.65 (step-pop @p1154 :rule scope :premises (@p1153)) % 0.37/0.65 (step-pop @p1155 :rule scope :premises (@p1154)) % 0.37/0.65 (step @p440 :rule process_scope :premises (@p1155) :args (@t552)) % 0.37/0.65 (step @p445 :rule implies_elim :premises (@p440)) % 0.37/0.65 (step @p446 :rule resolution :premises (@p445 @p430) :args (true @t552)) % 0.37/0.65 (step @p447 :rule not_and :premises (@p446)) % 0.37/0.65 (step @p448 :rule eq_resolve :premises (@p447 @p419)) % 0.37/0.65 (step @p449 :rule reordering :premises (@p448) :args ((or @t5 @t499 @t409 @t551))) % 0.37/0.65 (step @p450 :rule chain_m_resolution :premises (@p449 @p305 @p159 @p75) :args (@t551 @t535 (@list @t5 @t497 @t404))) % 0.37/0.65 (step @p451 :rule bool-double-not-elim :args (@t384)) % 0.37/0.65 (step @p452 :rule refl :args (@t553)) % 0.37/0.65 (step @p453 :rule nary_cong :premises (@p452 @p451) :args ((or @t553 (not @t551)))) % 0.37/0.65 (step @p454 :rule cnf_or_neg :args (@t553 0)) % 0.37/0.65 (step @p455 :rule eq_resolve :premises (@p454 @p453)) % 0.37/0.65 (step @p456 :rule reordering :premises (@p455) :args ((or @t384 @t553))) % 0.37/0.65 (step @p457 :rule chain_m_resolution :premises (@p456 @p450) :args (@t553 @t537 (@list @t384))) % 0.37/0.65 (step @p458 :rule cong :premises (@p184 @p74) :args (@t394)) % 0.37/0.65 (step @p459 :rule trans :premises (@p458 @p351)) % 0.37/0.65 (step @p460 :rule false_elim :premises (@p459)) % 0.37/0.65 (step @p461 :rule bool-double-not-elim :args (@t394)) % 0.37/0.65 (step @p462 :rule refl :args (@t555)) % 0.37/0.65 (step @p463 :rule nary_cong :premises (@p462 @p461) :args ((or @t555 (not @t554)))) % 0.37/0.65 (step @p464 :rule cnf_or_neg :args (@t555 0)) % 0.37/0.65 (step @p465 :rule eq_resolve :premises (@p464 @p463)) % 0.37/0.65 (step @p466 :rule reordering :premises (@p465) :args ((or @t394 @t555))) % 0.37/0.65 (step @p467 :rule chain_m_resolution :premises (@p466 @p460) :args (@t555 @t537 (@list @t394))) % 0.37/0.65 (step @p468 :rule cnf_or_neg :args (@t556 1)) % 0.37/0.65 (step @p469 :rule chain_m_resolution :premises (@p468 @p59) :args (@t556 @t302 @t383)) % 0.37/0.65 (step @p470 :rule refl :args (@t557)) % 0.37/0.65 (step @p471 :rule refl :args (@t451)) % 0.37/0.65 (step @p472 :rule nary_cong :premises (@p367 @p471 @p260 @p470) :args ((or @t546 @t451 @t499 @t557))) % 0.37/0.65 (assume-push @p1156 @t497) % 0.37/0.65 (assume-push @p1157 @t447) % 0.37/0.65 (assume-push @p1158 @t415) % 0.37/0.65 (assume-push @p1159 @t2) % 0.37/0.65 (step @p268 :rule evaluate :args (@t533)) % 0.37/0.65 (step @p477 :rule trans :premises (@p1158 @p106 @p159)) % 0.37/0.65 (step @p478 :rule symm :premises (@p477)) % 0.37/0.65 (step @p479 :rule trans :premises (@p159 @p478)) % 0.37/0.65 (step @p480 :rule true_intro :premises (@p479)) % 0.37/0.65 (step @p377 :rule false_intro :premises (@p364)) % 0.37/0.65 (step @p378 :rule symm :premises (@p377)) % 0.37/0.65 (step @p481 :rule trans :premises (@p378 @p480)) % 0.37/0.65 (step @p482 false :rule eq_resolve :premises (@p481 @p268)) % 0.37/0.65 (step-pop @p1160 :rule scope :premises (@p482)) % 0.37/0.65 (step-pop @p1161 :rule scope :premises (@p1160)) % 0.37/0.65 (step-pop @p1162 :rule scope :premises (@p1161)) % 0.37/0.65 (step-pop @p1163 :rule scope :premises (@p1162)) % 0.37/0.65 (step @p483 :rule process_scope :premises (@p1163) :args (false)) % 0.37/0.65 (assume-push @p1164 @t2) % 0.37/0.65 (assume-push @p1165 @t447) % 0.37/0.65 (assume-push @p1166 @t497) % 0.37/0.65 (assume-push @p1167 @t415) % 0.37/0.65 (step @p492 :rule and_intro :premises (@p159 @p107 @p1167 @p364)) % 0.37/0.65 (step-pop @p1168 :rule scope :premises (@p492)) % 0.37/0.65 (step-pop @p1169 :rule scope :premises (@p1168)) % 0.37/0.65 (step-pop @p1170 :rule scope :premises (@p1169)) % 0.37/0.65 (step-pop @p1171 :rule scope :premises (@p1170)) % 0.37/0.65 (step @p493 :rule process_scope :premises (@p1171) :args (@t558)) % 0.37/0.65 (step @p498 :rule implies_elim :premises (@p493)) % 0.37/0.65 (step @p499 :rule resolution :premises (@p498 @p483) :args (true @t558)) % 0.37/0.65 (step @p500 :rule not_and :premises (@p499)) % 0.37/0.65 (step @p501 :rule eq_resolve :premises (@p500 @p472)) % 0.37/0.65 (step @p502 :rule reordering :premises (@p501) :args ((or @t1 @t499 @t451 @t557))) % 0.37/0.65 (step @p503 :rule chain_m_resolution :premises (@p502 @p364 @p159 @p107) :args (@t557 @t535 (@list @t1 @t497 @t447))) % 0.37/0.65 (step @p504 :rule bool-double-not-elim :args (@t415)) % 0.37/0.65 (step @p505 :rule refl :args (@t559)) % 0.37/0.65 (step @p506 :rule nary_cong :premises (@p505 @p504) :args ((or @t559 (not @t557)))) % 0.37/0.65 (step @p507 :rule cnf_or_neg :args (@t559 0)) % 0.37/0.65 (step @p508 :rule eq_resolve :premises (@p507 @p506)) % 0.37/0.65 (step @p509 :rule reordering :premises (@p508) :args ((or @t415 @t559))) % 0.37/0.65 (step @p510 :rule chain_m_resolution :premises (@p509 @p503) :args (@t559 @t537 (@list @t415))) % 0.37/0.65 (step @p511 :rule refl :args (@t560)) % 0.37/0.65 (step @p512 :rule nary_cong :premises (@p262 @p471 @p260 @p511) :args ((or @t532 @t451 @t499 @t560))) % 0.37/0.65 (assume-push @p1172 @t497) % 0.37/0.65 (assume-push @p1173 @t447) % 0.37/0.65 (assume-push @p1174 @t423) % 0.37/0.65 (assume-push @p1175 @t4) % 0.37/0.65 (step @p268 :rule evaluate :args (@t533)) % 0.37/0.65 (step @p517 :rule trans :premises (@p1174 @p106 @p159)) % 0.37/0.65 (step @p518 :rule symm :premises (@p517)) % 0.37/0.65 (step @p519 :rule trans :premises (@p159 @p518)) % 0.37/0.65 (step @p520 :rule true_intro :premises (@p519)) % 0.37/0.65 (step @p273 :rule false_intro :premises (@p258)) % 0.37/0.65 (step @p274 :rule symm :premises (@p273)) % 0.37/0.65 (step @p521 :rule trans :premises (@p274 @p520)) % 0.37/0.65 (step @p522 false :rule eq_resolve :premises (@p521 @p268)) % 0.37/0.65 (step-pop @p1176 :rule scope :premises (@p522)) % 0.37/0.65 (step-pop @p1177 :rule scope :premises (@p1176)) % 0.37/0.65 (step-pop @p1178 :rule scope :premises (@p1177)) % 0.37/0.65 (step-pop @p1179 :rule scope :premises (@p1178)) % 0.37/0.65 (step @p523 :rule process_scope :premises (@p1179) :args (false)) % 0.37/0.65 (assume-push @p1180 @t4) % 0.37/0.65 (assume-push @p1181 @t447) % 0.37/0.65 (assume-push @p1182 @t497) % 0.37/0.65 (assume-push @p1183 @t423) % 0.37/0.65 (step @p532 :rule and_intro :premises (@p159 @p107 @p1183 @p258)) % 0.37/0.65 (step-pop @p1184 :rule scope :premises (@p532)) % 0.37/0.65 (step-pop @p1185 :rule scope :premises (@p1184)) % 0.37/0.65 (step-pop @p1186 :rule scope :premises (@p1185)) % 0.37/0.65 (step-pop @p1187 :rule scope :premises (@p1186)) % 0.37/0.65 (step @p533 :rule process_scope :premises (@p1187) :args (@t561)) % 0.37/0.65 (step @p538 :rule implies_elim :premises (@p533)) % 0.37/0.65 (step @p539 :rule resolution :premises (@p538 @p523) :args (true @t561)) % 0.37/0.65 (step @p540 :rule not_and :premises (@p539)) % 0.37/0.65 (step @p541 :rule eq_resolve :premises (@p540 @p512)) % 0.37/0.65 (step @p542 :rule reordering :premises (@p541) :args ((or @t3 @t499 @t451 @t560))) % 0.37/0.65 (step @p543 :rule chain_m_resolution :premises (@p542 @p258 @p159 @p107) :args (@t560 @t535 (@list @t3 @t497 @t447))) % 0.37/0.65 (step @p544 :rule bool-double-not-elim :args (@t423)) % 0.37/0.65 (step @p545 :rule refl :args (@t562)) % 0.37/0.65 (step @p546 :rule nary_cong :premises (@p545 @p544) :args ((or @t562 (not @t560)))) % 0.37/0.65 (step @p547 :rule cnf_or_neg :args (@t562 0)) % 0.37/0.65 (step @p548 :rule eq_resolve :premises (@p547 @p546)) % 0.37/0.65 (step @p549 :rule reordering :premises (@p548) :args ((or @t423 @t562))) % 0.37/0.65 (step @p550 :rule chain_m_resolution :premises (@p549 @p543) :args (@t562 @t537 (@list @t423))) % 0.37/0.65 (step @p551 :rule cong :premises (@p184 @p106) :args (@t440)) % 0.37/0.65 (step @p552 :rule trans :premises (@p551 @p351)) % 0.37/0.65 (step @p553 :rule false_elim :premises (@p552)) % 0.37/0.65 (step @p554 :rule bool-double-not-elim :args (@t440)) % 0.37/0.65 (step @p555 :rule refl :args (@t564)) % 0.37/0.65 (step @p556 :rule nary_cong :premises (@p555 @p554) :args ((or @t564 (not @t563)))) % 0.37/0.65 (step @p557 :rule cnf_or_neg :args (@t564 0)) % 0.37/0.65 (step @p558 :rule eq_resolve :premises (@p557 @p556)) % 0.37/0.65 (step @p559 :rule reordering :premises (@p558) :args ((or @t440 @t564))) % 0.37/0.65 (step @p560 :rule chain_m_resolution :premises (@p559 @p553) :args (@t564 @t537 (@list @t440))) % 0.37/0.65 (step @p561 :rule cnf_or_neg :args (@t565 1)) % 0.37/0.65 (step @p562 :rule chain_m_resolution :premises (@p561 @p99) :args (@t565 @t302 @t439)) % 0.37/0.65 (step @p563 :rule refl :args (@t566)) % 0.37/0.65 (step @p564 :rule refl :args (@t481)) % 0.37/0.65 (step @p565 :rule nary_cong :premises (@p367 @p564 @p260 @p563) :args ((or @t546 @t481 @t499 @t566))) % 0.37/0.65 (assume-push @p1188 @t497) % 0.37/0.65 (assume-push @p1189 @t478) % 0.37/0.65 (assume-push @p1190 @t456) % 0.37/0.65 (assume-push @p1191 @t2) % 0.37/0.65 (step @p268 :rule evaluate :args (@t533)) % 0.37/0.65 (step @p570 :rule trans :premises (@p1190 @p134 @p159)) % 0.37/0.65 (step @p571 :rule symm :premises (@p570)) % 0.37/0.65 (step @p572 :rule trans :premises (@p159 @p571)) % 0.37/0.65 (step @p573 :rule true_intro :premises (@p572)) % 0.37/0.65 (step @p377 :rule false_intro :premises (@p364)) % 0.37/0.65 (step @p378 :rule symm :premises (@p377)) % 0.37/0.65 (step @p574 :rule trans :premises (@p378 @p573)) % 0.37/0.65 (step @p575 false :rule eq_resolve :premises (@p574 @p268)) % 0.37/0.65 (step-pop @p1192 :rule scope :premises (@p575)) % 0.37/0.65 (step-pop @p1193 :rule scope :premises (@p1192)) % 0.37/0.65 (step-pop @p1194 :rule scope :premises (@p1193)) % 0.37/0.65 (step-pop @p1195 :rule scope :premises (@p1194)) % 0.37/0.65 (step @p576 :rule process_scope :premises (@p1195) :args (false)) % 0.37/0.65 (assume-push @p1196 @t2) % 0.37/0.65 (assume-push @p1197 @t478) % 0.37/0.65 (assume-push @p1198 @t497) % 0.37/0.65 (assume-push @p1199 @t456) % 0.37/0.65 (step @p585 :rule and_intro :premises (@p159 @p135 @p1199 @p364)) % 0.37/0.65 (step-pop @p1200 :rule scope :premises (@p585)) % 0.37/0.65 (step-pop @p1201 :rule scope :premises (@p1200)) % 0.37/0.65 (step-pop @p1202 :rule scope :premises (@p1201)) % 0.37/0.65 (step-pop @p1203 :rule scope :premises (@p1202)) % 0.37/0.65 (step @p586 :rule process_scope :premises (@p1203) :args (@t567)) % 0.37/0.65 (step @p591 :rule implies_elim :premises (@p586)) % 0.37/0.65 (step @p592 :rule resolution :premises (@p591 @p576) :args (true @t567)) % 0.37/0.65 (step @p593 :rule not_and :premises (@p592)) % 0.37/0.65 (step @p594 :rule eq_resolve :premises (@p593 @p565)) % 0.37/0.65 (step @p595 :rule reordering :premises (@p594) :args ((or @t1 @t499 @t481 @t566))) % 0.37/0.65 (step @p596 :rule chain_m_resolution :premises (@p595 @p364 @p159 @p135) :args (@t566 @t535 (@list @t1 @t497 @t478))) % 0.37/0.65 (step @p597 :rule bool-double-not-elim :args (@t456)) % 0.37/0.65 (step @p598 :rule refl :args (@t568)) % 0.37/0.65 (step @p599 :rule nary_cong :premises (@p598 @p597) :args ((or @t568 (not @t566)))) % 0.37/0.65 (step @p600 :rule cnf_or_neg :args (@t568 0)) % 0.37/0.65 (step @p601 :rule eq_resolve :premises (@p600 @p599)) % 0.37/0.65 (step @p602 :rule reordering :premises (@p601) :args ((or @t456 @t568))) % 0.37/0.65 (step @p603 :rule chain_m_resolution :premises (@p602 @p596) :args (@t568 @t537 (@list @t456))) % 0.37/0.65 (step @p604 :rule refl :args (@t569)) % 0.37/0.65 (step @p605 :rule nary_cong :premises (@p262 @p564 @p260 @p604) :args ((or @t532 @t481 @t499 @t569))) % 0.37/0.65 (assume-push @p1204 @t497) % 0.37/0.65 (assume-push @p1205 @t478) % 0.37/0.65 (assume-push @p1206 @t461) % 0.37/0.65 (assume-push @p1207 @t4) % 0.37/0.65 (step @p268 :rule evaluate :args (@t533)) % 0.37/0.65 (step @p610 :rule trans :premises (@p1206 @p134 @p159)) % 0.37/0.65 (step @p611 :rule symm :premises (@p610)) % 0.37/0.65 (step @p612 :rule trans :premises (@p159 @p611)) % 0.37/0.65 (step @p613 :rule true_intro :premises (@p612)) % 0.37/0.65 (step @p273 :rule false_intro :premises (@p258)) % 0.37/0.65 (step @p274 :rule symm :premises (@p273)) % 0.37/0.65 (step @p614 :rule trans :premises (@p274 @p613)) % 0.37/0.65 (step @p615 false :rule eq_resolve :premises (@p614 @p268)) % 0.37/0.65 (step-pop @p1208 :rule scope :premises (@p615)) % 0.37/0.65 (step-pop @p1209 :rule scope :premises (@p1208)) % 0.37/0.65 (step-pop @p1210 :rule scope :premises (@p1209)) % 0.37/0.65 (step-pop @p1211 :rule scope :premises (@p1210)) % 0.37/0.65 (step @p616 :rule process_scope :premises (@p1211) :args (false)) % 0.37/0.65 (assume-push @p1212 @t4) % 0.37/0.65 (assume-push @p1213 @t478) % 0.37/0.65 (assume-push @p1214 @t497) % 0.37/0.65 (assume-push @p1215 @t461) % 0.37/0.65 (step @p625 :rule and_intro :premises (@p159 @p135 @p1215 @p258)) % 0.37/0.65 (step-pop @p1216 :rule scope :premises (@p625)) % 0.37/0.65 (step-pop @p1217 :rule scope :premises (@p1216)) % 0.37/0.65 (step-pop @p1218 :rule scope :premises (@p1217)) % 0.37/0.65 (step-pop @p1219 :rule scope :premises (@p1218)) % 0.37/0.65 (step @p626 :rule process_scope :premises (@p1219) :args (@t570)) % 0.37/0.65 (step @p631 :rule implies_elim :premises (@p626)) % 0.37/0.65 (step @p632 :rule resolution :premises (@p631 @p616) :args (true @t570)) % 0.37/0.65 (step @p633 :rule not_and :premises (@p632)) % 0.37/0.65 (step @p634 :rule eq_resolve :premises (@p633 @p605)) % 0.37/0.65 (step @p635 :rule reordering :premises (@p634) :args ((or @t3 @t499 @t481 @t569))) % 0.37/0.65 (step @p636 :rule chain_m_resolution :premises (@p635 @p258 @p159 @p135) :args (@t569 @t535 (@list @t3 @t497 @t478))) % 0.37/0.65 (step @p637 :rule bool-double-not-elim :args (@t461)) % 0.37/0.65 (step @p638 :rule refl :args (@t571)) % 0.37/0.65 (step @p639 :rule nary_cong :premises (@p638 @p637) :args ((or @t571 (not @t569)))) % 0.37/0.65 (step @p640 :rule cnf_or_neg :args (@t571 0)) % 0.37/0.65 (step @p641 :rule eq_resolve :premises (@p640 @p639)) % 0.37/0.65 (step @p642 :rule reordering :premises (@p641) :args ((or @t461 @t571))) % 0.37/0.65 (step @p643 :rule chain_m_resolution :premises (@p642 @p636) :args (@t571 @t537 (@list @t461))) % 0.37/0.65 (step @p644 :rule refl :args (@t572)) % 0.37/0.65 (step @p645 :rule nary_cong :premises (@p307 @p564 @p260 @p644) :args ((or @t539 @t481 @t499 @t572))) % 0.37/0.65 (assume-push @p1220 @t497) % 0.37/0.65 (assume-push @p1221 @t478) % 0.37/0.65 (assume-push @p1222 @t466) % 0.37/0.65 (assume-push @p1223 @t6) % 0.37/0.65 (step @p268 :rule evaluate :args (@t533)) % 0.37/0.65 (step @p650 :rule trans :premises (@p1222 @p134 @p159)) % 0.37/0.65 (step @p651 :rule symm :premises (@p650)) % 0.37/0.65 (step @p652 :rule trans :premises (@p159 @p651)) % 0.37/0.65 (step @p653 :rule true_intro :premises (@p652)) % 0.37/0.65 (step @p317 :rule false_intro :premises (@p305)) % 0.37/0.65 (step @p318 :rule symm :premises (@p317)) % 0.37/0.65 (step @p654 :rule trans :premises (@p318 @p653)) % 0.37/0.65 (step @p655 false :rule eq_resolve :premises (@p654 @p268)) % 0.37/0.65 (step-pop @p1224 :rule scope :premises (@p655)) % 0.37/0.65 (step-pop @p1225 :rule scope :premises (@p1224)) % 0.37/0.65 (step-pop @p1226 :rule scope :premises (@p1225)) % 0.37/0.65 (step-pop @p1227 :rule scope :premises (@p1226)) % 0.37/0.65 (step @p656 :rule process_scope :premises (@p1227) :args (false)) % 0.37/0.65 (assume-push @p1228 @t6) % 0.37/0.65 (assume-push @p1229 @t478) % 0.37/0.65 (assume-push @p1230 @t497) % 0.37/0.65 (assume-push @p1231 @t466) % 0.37/0.65 (step @p665 :rule and_intro :premises (@p159 @p135 @p1231 @p305)) % 0.37/0.65 (step-pop @p1232 :rule scope :premises (@p665)) % 0.37/0.65 (step-pop @p1233 :rule scope :premises (@p1232)) % 0.37/0.65 (step-pop @p1234 :rule scope :premises (@p1233)) % 0.37/0.65 (step-pop @p1235 :rule scope :premises (@p1234)) % 0.37/0.65 (step @p666 :rule process_scope :premises (@p1235) :args (@t573)) % 0.37/0.65 (step @p671 :rule implies_elim :premises (@p666)) % 0.37/0.65 (step @p672 :rule resolution :premises (@p671 @p656) :args (true @t573)) % 0.37/0.65 (step @p673 :rule not_and :premises (@p672)) % 0.37/0.65 (step @p674 :rule eq_resolve :premises (@p673 @p645)) % 0.37/0.65 (step @p675 :rule reordering :premises (@p674) :args ((or @t5 @t499 @t481 @t572))) % 0.37/0.65 (step @p676 :rule chain_m_resolution :premises (@p675 @p305 @p159 @p135) :args (@t572 @t535 (@list @t5 @t497 @t478))) % 0.37/0.65 (step @p677 :rule bool-double-not-elim :args (@t466)) % 0.37/0.65 (step @p678 :rule refl :args (@t574)) % 0.37/0.65 (step @p679 :rule nary_cong :premises (@p678 @p677) :args ((or @t574 (not @t572)))) % 0.37/0.65 (step @p680 :rule cnf_or_neg :args (@t574 0)) % 0.37/0.65 (step @p681 :rule eq_resolve :premises (@p680 @p679)) % 0.37/0.65 (step @p682 :rule reordering :premises (@p681) :args ((or @t466 @t574))) % 0.37/0.65 (step @p683 :rule chain_m_resolution :premises (@p682 @p676) :args (@t574 @t537 (@list @t466))) % 0.37/0.65 (step @p684 :rule cong :premises (@p184 @p134) :args (@t471)) % 0.37/0.65 (step @p685 :rule trans :premises (@p684 @p351)) % 0.37/0.65 (step @p686 :rule false_elim :premises (@p685)) % 0.37/0.65 (step @p687 :rule bool-double-not-elim :args (@t471)) % 0.37/0.65 (step @p688 :rule refl :args (@t576)) % 0.37/0.65 (step @p689 :rule nary_cong :premises (@p688 @p687) :args ((or @t576 (not @t575)))) % 0.37/0.65 (step @p690 :rule cnf_or_neg :args (@t576 0)) % 0.37/0.65 (step @p691 :rule eq_resolve :premises (@p690 @p689)) % 0.37/0.65 (step @p692 :rule reordering :premises (@p691) :args ((or @t471 @t576))) % 0.37/0.65 (step @p693 :rule chain_m_resolution :premises (@p692 @p686) :args (@t576 @t537 (@list @t471))) % 0.37/0.65 (step @p694 :rule cnf_or_neg :args (@t577 1)) % 0.37/0.65 (step @p695 :rule chain_m_resolution :premises (@p694 @p131) :args (@t577 @t302 @t477)) % 0.37/0.65 (step @p696 :rule refl :args (@t578)) % 0.37/0.65 (step @p697 :rule nary_cong :premises (@p367 @p260 @p696) :args ((or @t546 @t499 @t578))) % 0.37/0.65 (assume-push @p1236 @t497) % 0.37/0.65 (assume-push @p1237 @t485) % 0.37/0.65 (assume-push @p1238 @t2) % 0.37/0.65 (step @p268 :rule evaluate :args (@t533)) % 0.37/0.65 (step @p701 :rule symm :premises (@p1237)) % 0.37/0.65 (step @p702 :rule trans :premises (@p159 @p701)) % 0.37/0.65 (step @p703 :rule true_intro :premises (@p702)) % 0.37/0.65 (step @p377 :rule false_intro :premises (@p364)) % 0.37/0.65 (step @p378 :rule symm :premises (@p377)) % 0.37/0.65 (step @p704 :rule trans :premises (@p378 @p703)) % 0.37/0.65 (step @p705 false :rule eq_resolve :premises (@p704 @p268)) % 0.37/0.65 (step-pop @p1239 :rule scope :premises (@p705)) % 0.37/0.65 (step-pop @p1240 :rule scope :premises (@p1239)) % 0.37/0.65 (step-pop @p1241 :rule scope :premises (@p1240)) % 0.37/0.65 (step @p706 :rule process_scope :premises (@p1241) :args (false)) % 0.37/0.65 (assume-push @p1242 @t2) % 0.37/0.65 (assume-push @p1243 @t497) % 0.37/0.65 (assume-push @p1244 @t485) % 0.37/0.65 (step @p713 :rule and_intro :premises (@p159 @p1244 @p364)) % 0.37/0.65 (step-pop @p1245 :rule scope :premises (@p713)) % 0.37/0.65 (step-pop @p1246 :rule scope :premises (@p1245)) % 0.37/0.65 (step-pop @p1247 :rule scope :premises (@p1246)) % 0.37/0.65 (step @p714 :rule process_scope :premises (@p1247) :args (@t579)) % 0.37/0.65 (step @p718 :rule implies_elim :premises (@p714)) % 0.37/0.65 (step @p719 :rule resolution :premises (@p718 @p706) :args (true @t579)) % 0.37/0.65 (step @p720 :rule not_and :premises (@p719)) % 0.37/0.65 (step @p721 :rule eq_resolve :premises (@p720 @p697)) % 0.37/0.65 (step @p722 :rule chain_m_resolution :premises (@p721 @p364 @p159) :args (@t578 @t580 (@list @t1 @t497))) % 0.37/0.65 (step @p723 :rule bool-double-not-elim :args (@t485)) % 0.37/0.65 (step @p724 :rule refl :args (@t581)) % 0.37/0.65 (step @p725 :rule nary_cong :premises (@p724 @p723) :args ((or @t581 (not @t578)))) % 0.37/0.65 (step @p726 :rule cnf_or_neg :args (@t581 0)) % 0.37/0.65 (step @p727 :rule eq_resolve :premises (@p726 @p725)) % 0.37/0.65 (step @p728 :rule reordering :premises (@p727) :args ((or @t485 @t581))) % 0.37/0.65 (step @p729 :rule chain_m_resolution :premises (@p728 @p722) :args (@t581 @t537 (@list @t485))) % 0.37/0.65 (step @p730 :rule refl :args (@t582)) % 0.37/0.65 (step @p731 :rule nary_cong :premises (@p262 @p260 @p730) :args ((or @t532 @t499 @t582))) % 0.37/0.65 (assume-push @p1248 @t497) % 0.37/0.65 (assume-push @p1249 @t488) % 0.37/0.65 (assume-push @p1250 @t4) % 0.37/0.65 (step @p268 :rule evaluate :args (@t533)) % 0.37/0.65 (step @p735 :rule symm :premises (@p1249)) % 0.37/0.65 (step @p736 :rule trans :premises (@p159 @p735)) % 0.37/0.65 (step @p737 :rule true_intro :premises (@p736)) % 0.37/0.65 (step @p273 :rule false_intro :premises (@p258)) % 0.37/0.65 (step @p274 :rule symm :premises (@p273)) % 0.37/0.65 (step @p738 :rule trans :premises (@p274 @p737)) % 0.37/0.65 (step @p739 false :rule eq_resolve :premises (@p738 @p268)) % 0.37/0.65 (step-pop @p1251 :rule scope :premises (@p739)) % 0.37/0.65 (step-pop @p1252 :rule scope :premises (@p1251)) % 0.37/0.65 (step-pop @p1253 :rule scope :premises (@p1252)) % 0.37/0.65 (step @p740 :rule process_scope :premises (@p1253) :args (false)) % 0.37/0.65 (assume-push @p1254 @t4) % 0.37/0.65 (assume-push @p1255 @t497) % 0.37/0.65 (assume-push @p1256 @t488) % 0.37/0.65 (step @p747 :rule and_intro :premises (@p159 @p1256 @p258)) % 0.37/0.65 (step-pop @p1257 :rule scope :premises (@p747)) % 0.37/0.65 (step-pop @p1258 :rule scope :premises (@p1257)) % 0.37/0.65 (step-pop @p1259 :rule scope :premises (@p1258)) % 0.37/0.65 (step @p748 :rule process_scope :premises (@p1259) :args (@t583)) % 0.37/0.65 (step @p752 :rule implies_elim :premises (@p748)) % 0.37/0.65 (step @p753 :rule resolution :premises (@p752 @p740) :args (true @t583)) % 0.37/0.65 (step @p754 :rule not_and :premises (@p753)) % 0.37/0.65 (step @p755 :rule eq_resolve :premises (@p754 @p731)) % 0.37/0.65 (step @p756 :rule chain_m_resolution :premises (@p755 @p258 @p159) :args (@t582 @t580 (@list @t3 @t497))) % 0.37/0.65 (step @p757 :rule bool-double-not-elim :args (@t488)) % 0.37/0.65 (step @p758 :rule refl :args (@t584)) % 0.37/0.65 (step @p759 :rule nary_cong :premises (@p758 @p757) :args ((or @t584 (not @t582)))) % 0.37/0.65 (step @p760 :rule cnf_or_neg :args (@t584 0)) % 0.37/0.65 (step @p761 :rule eq_resolve :premises (@p760 @p759)) % 0.37/0.65 (step @p762 :rule reordering :premises (@p761) :args ((or @t488 @t584))) % 0.37/0.65 (step @p763 :rule chain_m_resolution :premises (@p762 @p756) :args (@t584 @t537 (@list @t488))) % 0.37/0.65 (step @p764 :rule refl :args (@t585)) % 0.37/0.65 (step @p765 :rule nary_cong :premises (@p307 @p260 @p764) :args ((or @t539 @t499 @t585))) % 0.37/0.65 (assume-push @p1260 @t497) % 0.37/0.65 (assume-push @p1261 @t491) % 0.37/0.65 (assume-push @p1262 @t6) % 0.37/0.65 (step @p268 :rule evaluate :args (@t533)) % 0.37/0.65 (step @p769 :rule symm :premises (@p1261)) % 0.37/0.65 (step @p770 :rule trans :premises (@p159 @p769)) % 0.37/0.65 (step @p771 :rule true_intro :premises (@p770)) % 0.37/0.65 (step @p317 :rule false_intro :premises (@p305)) % 0.37/0.65 (step @p318 :rule symm :premises (@p317)) % 0.37/0.65 (step @p772 :rule trans :premises (@p318 @p771)) % 0.37/0.65 (step @p773 false :rule eq_resolve :premises (@p772 @p268)) % 0.37/0.65 (step-pop @p1263 :rule scope :premises (@p773)) % 0.37/0.65 (step-pop @p1264 :rule scope :premises (@p1263)) % 0.37/0.65 (step-pop @p1265 :rule scope :premises (@p1264)) % 0.37/0.65 (step @p774 :rule process_scope :premises (@p1265) :args (false)) % 0.37/0.65 (assume-push @p1266 @t6) % 0.37/0.65 (assume-push @p1267 @t497) % 0.37/0.65 (assume-push @p1268 @t491) % 0.37/0.65 (step @p781 :rule and_intro :premises (@p159 @p1268 @p305)) % 0.37/0.65 (step-pop @p1269 :rule scope :premises (@p781)) % 0.37/0.65 (step-pop @p1270 :rule scope :premises (@p1269)) % 0.37/0.65 (step-pop @p1271 :rule scope :premises (@p1270)) % 0.37/0.65 (step @p782 :rule process_scope :premises (@p1271) :args (@t586)) % 0.37/0.65 (step @p786 :rule implies_elim :premises (@p782)) % 0.37/0.65 (step @p787 :rule resolution :premises (@p786 @p774) :args (true @t586)) % 0.37/0.65 (step @p788 :rule not_and :premises (@p787)) % 0.37/0.65 (step @p789 :rule eq_resolve :premises (@p788 @p765)) % 0.37/0.65 (step @p790 :rule chain_m_resolution :premises (@p789 @p305 @p159) :args (@t585 @t580 (@list @t5 @t497))) % 0.37/0.65 (step @p791 :rule bool-double-not-elim :args (@t491)) % 0.37/0.65 (step @p792 :rule refl :args (@t587)) % 0.37/0.65 (step @p793 :rule nary_cong :premises (@p792 @p791) :args ((or @t587 (not @t585)))) % 0.37/0.65 (step @p794 :rule cnf_or_neg :args (@t587 0)) % 0.37/0.65 (step @p795 :rule eq_resolve :premises (@p794 @p793)) % 0.37/0.65 (step @p796 :rule reordering :premises (@p795) :args ((or @t491 @t587))) % 0.37/0.65 (step @p797 :rule chain_m_resolution :premises (@p796 @p790) :args (@t587 @t537 (@list @t491))) % 0.37/0.65 (step @p798 :rule cong :premises (@p184 @p158) :args (@t494)) % 0.37/0.65 (step @p799 :rule trans :premises (@p798 @p351)) % 0.37/0.65 (step @p800 :rule false_elim :premises (@p799)) % 0.37/0.65 (step @p801 :rule bool-double-not-elim :args (@t494)) % 0.37/0.65 (step @p802 :rule refl :args (@t589)) % 0.37/0.65 (step @p803 :rule nary_cong :premises (@p802 @p801) :args ((or @t589 (not @t588)))) % 0.37/0.65 (step @p804 :rule cnf_or_neg :args (@t589 0)) % 0.37/0.65 (step @p805 :rule eq_resolve :premises (@p804 @p803)) % 0.37/0.65 (step @p806 :rule reordering :premises (@p805) :args ((or @t494 @t589))) % 0.37/0.65 (step @p807 :rule chain_m_resolution :premises (@p806 @p800) :args (@t589 @t537 (@list @t494))) % 0.37/0.65 (step @p808 :rule cnf_or_neg :args (@t590 1)) % 0.37/0.65 (step @p809 :rule reordering :premises (@p808) :args ((or @t499 @t590))) % 0.37/0.65 (step @p810 :rule chain_m_resolution :premises (@p809 @p159) :args (@t590 @t302 @t500)) % 0.37/0.65 (step @p811 :rule eq-symm :args (@t7 tptp.e4)) % 0.37/0.65 (step @p812 :rule eq-symm :args (@t17 tptp.e4)) % 0.37/0.65 (step @p813 :rule eq-symm :args (@t27 tptp.e4)) % 0.37/0.65 (step @p814 :rule eq-symm :args (@t37 tptp.e4)) % 0.37/0.65 (step @p815 :rule eq-symm :args (@t47 tptp.e4)) % 0.37/0.65 (step @p816 :rule nary_cong :premises (@p815 @p814 @p813 @p812 @p811) :args (@t62)) % 0.37/0.65 (step @p817 :rule eq-symm :args (@t9 tptp.e4)) % 0.37/0.65 (step @p818 :rule eq-symm :args (@t11 tptp.e4)) % 0.37/0.65 (step @p819 :rule eq-symm :args (@t13 tptp.e4)) % 0.37/0.65 (step @p820 :rule eq-symm :args (@t15 tptp.e4)) % 0.37/0.65 (step @p821 :rule nary_cong :premises (@p820 @p819 @p818 @p817 @p811) :args (@t66)) % 0.37/0.65 (step @p822 :rule eq-symm :args (@t7 tptp.e3)) % 0.37/0.65 (step @p823 :rule eq-symm :args (@t17 tptp.e3)) % 0.37/0.65 (step @p824 :rule eq-symm :args (@t27 tptp.e3)) % 0.37/0.65 (step @p825 :rule eq-symm :args (@t37 tptp.e3)) % 0.37/0.65 (step @p826 :rule eq-symm :args (@t47 tptp.e3)) % 0.37/0.65 (step @p827 :rule nary_cong :premises (@p826 @p825 @p824 @p823 @p822) :args (@t71)) % 0.37/0.65 (step @p828 :rule eq-symm :args (@t9 tptp.e3)) % 0.37/0.65 (step @p829 :rule eq-symm :args (@t11 tptp.e3)) % 0.37/0.65 (step @p830 :rule eq-symm :args (@t13 tptp.e3)) % 0.37/0.65 (step @p831 :rule eq-symm :args (@t15 tptp.e3)) % 0.37/0.65 (step @p832 :rule nary_cong :premises (@p831 @p830 @p829 @p828 @p822) :args (@t75)) % 0.37/0.65 (step @p833 :rule eq-symm :args (@t7 tptp.e2)) % 0.37/0.65 (step @p834 :rule eq-symm :args (@t17 tptp.e2)) % 0.37/0.65 (step @p835 :rule eq-symm :args (@t27 tptp.e2)) % 0.37/0.65 (step @p836 :rule eq-symm :args (@t37 tptp.e2)) % 0.37/0.65 (step @p837 :rule eq-symm :args (@t47 tptp.e2)) % 0.37/0.65 (step @p838 :rule nary_cong :premises (@p837 @p836 @p835 @p834 @p833) :args (@t80)) % 0.37/0.65 (step @p839 :rule eq-symm :args (@t9 tptp.e2)) % 0.37/0.65 (step @p840 :rule eq-symm :args (@t11 tptp.e2)) % 0.37/0.65 (step @p841 :rule eq-symm :args (@t13 tptp.e2)) % 0.37/0.65 (step @p842 :rule eq-symm :args (@t15 tptp.e2)) % 0.37/0.65 (step @p843 :rule nary_cong :premises (@p842 @p841 @p840 @p839 @p833) :args (@t84)) % 0.37/0.65 (step @p844 :rule eq-symm :args (@t7 tptp.e1)) % 0.37/0.65 (step @p845 :rule eq-symm :args (@t17 tptp.e1)) % 0.37/0.65 (step @p846 :rule eq-symm :args (@t27 tptp.e1)) % 0.37/0.65 (step @p847 :rule eq-symm :args (@t37 tptp.e1)) % 0.37/0.65 (step @p848 :rule eq-symm :args (@t47 tptp.e1)) % 0.37/0.65 (step @p849 :rule nary_cong :premises (@p848 @p847 @p846 @p845 @p844) :args (@t89)) % 0.37/0.65 (step @p850 :rule eq-symm :args (@t9 tptp.e1)) % 0.37/0.65 (step @p851 :rule eq-symm :args (@t11 tptp.e1)) % 0.37/0.65 (step @p852 :rule eq-symm :args (@t13 tptp.e1)) % 0.37/0.65 (step @p853 :rule eq-symm :args (@t15 tptp.e1)) % 0.37/0.65 (step @p854 :rule nary_cong :premises (@p853 @p852 @p851 @p850 @p844) :args (@t93)) % 0.37/0.65 (step @p855 :rule eq-symm :args (@t7 tptp.e0)) % 0.37/0.65 (step @p856 :rule eq-symm :args (@t17 tptp.e0)) % 0.37/0.65 (step @p857 :rule eq-symm :args (@t27 tptp.e0)) % 0.37/0.65 (step @p858 :rule eq-symm :args (@t37 tptp.e0)) % 0.37/0.65 (step @p859 :rule eq-symm :args (@t47 tptp.e0)) % 0.37/0.65 (step @p860 :rule nary_cong :premises (@p859 @p858 @p857 @p856 @p855) :args (@t98)) % 0.37/0.65 (step @p861 :rule eq-symm :args (@t9 tptp.e0)) % 0.37/0.65 (step @p862 :rule eq-symm :args (@t11 tptp.e0)) % 0.37/0.65 (step @p863 :rule eq-symm :args (@t13 tptp.e0)) % 0.37/0.65 (step @p864 :rule eq-symm :args (@t15 tptp.e0)) % 0.37/0.65 (step @p865 :rule nary_cong :premises (@p864 @p863 @p862 @p861 @p855) :args (@t103)) % 0.37/0.65 (step @p866 :rule eq-symm :args (@t19 tptp.e4)) % 0.37/0.65 (step @p867 :rule eq-symm :args (@t29 tptp.e4)) % 0.37/0.65 (step @p868 :rule eq-symm :args (@t39 tptp.e4)) % 0.37/0.65 (step @p869 :rule eq-symm :args (@t49 tptp.e4)) % 0.37/0.65 (step @p870 :rule nary_cong :premises (@p869 @p868 @p867 @p866 @p817) :args (@t107)) % 0.37/0.65 (step @p871 :rule eq-symm :args (@t21 tptp.e4)) % 0.37/0.65 (step @p872 :rule eq-symm :args (@t23 tptp.e4)) % 0.37/0.65 (step @p873 :rule eq-symm :args (@t25 tptp.e4)) % 0.37/0.65 (step @p874 :rule nary_cong :premises (@p873 @p872 @p871 @p866 @p812) :args (@t110)) % 0.37/0.65 (step @p875 :rule eq-symm :args (@t19 tptp.e3)) % 0.37/0.65 (step @p876 :rule eq-symm :args (@t29 tptp.e3)) % 0.37/0.65 (step @p877 :rule eq-symm :args (@t39 tptp.e3)) % 0.37/0.65 (step @p878 :rule eq-symm :args (@t49 tptp.e3)) % 0.37/0.65 (step @p879 :rule nary_cong :premises (@p878 @p877 @p876 @p875 @p828) :args (@t114)) % 0.37/0.65 (step @p880 :rule eq-symm :args (@t21 tptp.e3)) % 0.37/0.65 (step @p881 :rule eq-symm :args (@t23 tptp.e3)) % 0.37/0.65 (step @p882 :rule eq-symm :args (@t25 tptp.e3)) % 0.37/0.65 (step @p883 :rule nary_cong :premises (@p882 @p881 @p880 @p875 @p823) :args (@t117)) % 0.37/0.65 (step @p884 :rule eq-symm :args (@t19 tptp.e2)) % 0.37/0.65 (step @p885 :rule eq-symm :args (@t29 tptp.e2)) % 0.37/0.65 (step @p886 :rule eq-symm :args (@t39 tptp.e2)) % 0.37/0.65 (step @p887 :rule eq-symm :args (@t49 tptp.e2)) % 0.37/0.65 (step @p888 :rule nary_cong :premises (@p887 @p886 @p885 @p884 @p839) :args (@t122)) % 0.37/0.65 (step @p889 :rule eq-symm :args (@t21 tptp.e2)) % 0.37/0.65 (step @p890 :rule eq-symm :args (@t23 tptp.e2)) % 0.37/0.65 (step @p891 :rule eq-symm :args (@t25 tptp.e2)) % 0.37/0.65 (step @p892 :rule nary_cong :premises (@p891 @p890 @p889 @p884 @p834) :args (@t125)) % 0.37/0.65 (step @p893 :rule eq-symm :args (@t19 tptp.e1)) % 0.37/0.65 (step @p894 :rule eq-symm :args (@t29 tptp.e1)) % 0.37/0.65 (step @p895 :rule eq-symm :args (@t39 tptp.e1)) % 0.37/0.65 (step @p896 :rule eq-symm :args (@t49 tptp.e1)) % 0.37/0.65 (step @p897 :rule nary_cong :premises (@p896 @p895 @p894 @p893 @p850) :args (@t129)) % 0.37/0.65 (step @p898 :rule eq-symm :args (@t21 tptp.e1)) % 0.37/0.65 (step @p899 :rule eq-symm :args (@t23 tptp.e1)) % 0.37/0.65 (step @p900 :rule eq-symm :args (@t25 tptp.e1)) % 0.37/0.65 (step @p901 :rule nary_cong :premises (@p900 @p899 @p898 @p893 @p845) :args (@t133)) % 0.37/0.65 (step @p902 :rule eq-symm :args (@t19 tptp.e0)) % 0.37/0.65 (step @p903 :rule eq-symm :args (@t29 tptp.e0)) % 0.37/0.65 (step @p904 :rule eq-symm :args (@t39 tptp.e0)) % 0.37/0.65 (step @p905 :rule eq-symm :args (@t49 tptp.e0)) % 0.37/0.65 (step @p906 :rule nary_cong :premises (@p905 @p904 @p903 @p902 @p861) :args (@t137)) % 0.37/0.65 (step @p907 :rule eq-symm :args (@t21 tptp.e0)) % 0.37/0.65 (step @p908 :rule eq-symm :args (@t23 tptp.e0)) % 0.37/0.65 (step @p909 :rule eq-symm :args (@t25 tptp.e0)) % 0.37/0.65 (step @p910 :rule nary_cong :premises (@p909 @p908 @p907 @p902 @p856) :args (@t141)) % 0.37/0.65 (step @p911 :rule eq-symm :args (@t31 tptp.e4)) % 0.37/0.65 (step @p912 :rule eq-symm :args (@t41 tptp.e4)) % 0.37/0.65 (step @p913 :rule eq-symm :args (@t51 tptp.e4)) % 0.37/0.65 (step @p914 :rule nary_cong :premises (@p913 @p912 @p911 @p871 @p818) :args (@t145)) % 0.37/0.65 (step @p915 :rule eq-symm :args (@t33 tptp.e4)) % 0.37/0.65 (step @p916 :rule eq-symm :args (@t35 tptp.e4)) % 0.37/0.65 (step @p917 :rule nary_cong :premises (@p916 @p915 @p911 @p867 @p813) :args (@t147)) % 0.37/0.65 (step @p918 :rule eq-symm :args (@t31 tptp.e3)) % 0.37/0.65 (step @p919 :rule eq-symm :args (@t41 tptp.e3)) % 0.37/0.65 (step @p920 :rule eq-symm :args (@t51 tptp.e3)) % 0.37/0.65 (step @p921 :rule nary_cong :premises (@p920 @p919 @p918 @p880 @p829) :args (@t150)) % 0.37/0.65 (step @p922 :rule eq-symm :args (@t33 tptp.e3)) % 0.37/0.65 (step @p923 :rule eq-symm :args (@t35 tptp.e3)) % 0.37/0.65 (step @p924 :rule nary_cong :premises (@p923 @p922 @p918 @p876 @p824) :args (@t153)) % 0.37/0.65 (step @p925 :rule eq-symm :args (@t31 tptp.e2)) % 0.37/0.65 (step @p926 :rule eq-symm :args (@t41 tptp.e2)) % 0.37/0.65 (step @p927 :rule eq-symm :args (@t51 tptp.e2)) % 0.37/0.65 (step @p928 :rule nary_cong :premises (@p927 @p926 @p925 @p889 @p840) :args (@t156)) % 0.37/0.65 (step @p929 :rule eq-symm :args (@t33 tptp.e2)) % 0.37/0.65 (step @p930 :rule eq-symm :args (@t35 tptp.e2)) % 0.37/0.65 (step @p931 :rule nary_cong :premises (@p930 @p929 @p925 @p885 @p835) :args (@t158)) % 0.37/0.65 (step @p932 :rule eq-symm :args (@t31 tptp.e1)) % 0.37/0.65 (step @p933 :rule eq-symm :args (@t41 tptp.e1)) % 0.37/0.65 (step @p934 :rule eq-symm :args (@t51 tptp.e1)) % 0.37/0.65 (step @p935 :rule nary_cong :premises (@p934 @p933 @p932 @p898 @p851) :args (@t162)) % 0.37/0.65 (step @p936 :rule eq-symm :args (@t33 tptp.e1)) % 0.37/0.65 (step @p937 :rule eq-symm :args (@t35 tptp.e1)) % 0.37/0.65 (step @p938 :rule nary_cong :premises (@p937 @p936 @p932 @p894 @p846) :args (@t165)) % 0.37/0.65 (step @p939 :rule eq-symm :args (@t31 tptp.e0)) % 0.37/0.65 (step @p940 :rule eq-symm :args (@t41 tptp.e0)) % 0.37/0.65 (step @p941 :rule eq-symm :args (@t51 tptp.e0)) % 0.37/0.65 (step @p942 :rule nary_cong :premises (@p941 @p940 @p939 @p907 @p862) :args (@t168)) % 0.37/0.65 (step @p943 :rule eq-symm :args (@t33 tptp.e0)) % 0.37/0.65 (step @p944 :rule eq-symm :args (@t35 tptp.e0)) % 0.37/0.65 (step @p945 :rule nary_cong :premises (@p944 @p943 @p939 @p903 @p857) :args (@t171)) % 0.37/0.65 (step @p946 :rule eq-symm :args (@t43 tptp.e4)) % 0.37/0.65 (step @p947 :rule eq-symm :args (@t53 tptp.e4)) % 0.37/0.65 (step @p948 :rule nary_cong :premises (@p947 @p946 @p915 @p872 @p819) :args (@t174)) % 0.37/0.65 (step @p949 :rule eq-symm :args (@t45 tptp.e4)) % 0.37/0.65 (step @p950 :rule nary_cong :premises (@p949 @p946 @p912 @p868 @p814) :args (@t176)) % 0.37/0.65 (step @p951 :rule eq-symm :args (@t43 tptp.e3)) % 0.37/0.65 (step @p952 :rule eq-symm :args (@t53 tptp.e3)) % 0.37/0.65 (step @p953 :rule nary_cong :premises (@p952 @p951 @p922 @p881 @p830) :args (@t179)) % 0.37/0.65 (step @p954 :rule eq-symm :args (@t45 tptp.e3)) % 0.37/0.65 (step @p955 :rule nary_cong :premises (@p954 @p951 @p919 @p877 @p825) :args (@t181)) % 0.37/0.65 (step @p956 :rule eq-symm :args (@t43 tptp.e2)) % 0.37/0.65 (step @p957 :rule eq-symm :args (@t53 tptp.e2)) % 0.37/0.65 (step @p958 :rule nary_cong :premises (@p957 @p956 @p929 @p890 @p841) :args (@t184)) % 0.37/0.65 (step @p959 :rule eq-symm :args (@t45 tptp.e2)) % 0.37/0.65 (step @p960 :rule nary_cong :premises (@p959 @p956 @p926 @p886 @p836) :args (@t186)) % 0.37/0.65 (step @p961 :rule eq-symm :args (@t43 tptp.e1)) % 0.37/0.65 (step @p962 :rule eq-symm :args (@t53 tptp.e1)) % 0.37/0.65 (step @p963 :rule nary_cong :premises (@p962 @p961 @p936 @p899 @p852) :args (@t188)) % 0.37/0.65 (step @p964 :rule eq-symm :args (@t45 tptp.e1)) % 0.37/0.65 (step @p965 :rule nary_cong :premises (@p964 @p961 @p933 @p895 @p847) :args (@t189)) % 0.37/0.65 (step @p966 :rule eq-symm :args (@t43 tptp.e0)) % 0.37/0.65 (step @p967 :rule eq-symm :args (@t53 tptp.e0)) % 0.37/0.65 (step @p968 :rule nary_cong :premises (@p967 @p966 @p943 @p908 @p863) :args (@t191)) % 0.37/0.65 (step @p969 :rule eq-symm :args (@t45 tptp.e0)) % 0.37/0.65 (step @p970 :rule nary_cong :premises (@p969 @p966 @p940 @p904 @p858) :args (@t193)) % 0.37/0.65 (step @p971 :rule eq-symm :args (@t55 tptp.e4)) % 0.37/0.65 (step @p972 :rule nary_cong :premises (@p971 @p949 @p916 @p873 @p820) :args (@t195)) % 0.37/0.65 (step @p973 :rule nary_cong :premises (@p971 @p947 @p913 @p869 @p815) :args (@t196)) % 0.37/0.65 (step @p974 :rule eq-symm :args (@t55 tptp.e3)) % 0.37/0.65 (step @p975 :rule nary_cong :premises (@p974 @p954 @p923 @p882 @p831) :args (@t198)) % 0.37/0.65 (step @p976 :rule nary_cong :premises (@p974 @p952 @p920 @p878 @p826) :args (@t199)) % 0.37/0.65 (step @p977 :rule eq-symm :args (@t55 tptp.e2)) % 0.37/0.65 (step @p978 :rule nary_cong :premises (@p977 @p959 @p930 @p891 @p842) :args (@t201)) % 0.37/0.65 (step @p979 :rule nary_cong :premises (@p977 @p957 @p927 @p887 @p837) :args (@t202)) % 0.37/0.65 (step @p980 :rule eq-symm :args (@t55 tptp.e1)) % 0.37/0.65 (step @p981 :rule nary_cong :premises (@p980 @p964 @p937 @p900 @p853) :args (@t204)) % 0.37/0.65 (step @p982 :rule nary_cong :premises (@p980 @p962 @p934 @p896 @p848) :args (@t205)) % 0.37/0.65 (step @p983 :rule eq-symm :args (@t55 tptp.e0)) % 0.37/0.65 (step @p984 :rule nary_cong :premises (@p983 @p969 @p944 @p909 @p864) :args (@t206)) % 0.37/0.65 (step @p985 :rule nary_cong :premises (@p983 @p967 @p941 @p905 @p859) :args (@t207)) % 0.37/0.65 (step @p986 :rule eq-symm :args (tptp.unit tptp.e4)) % 0.37/0.65 (step @p987 :rule eq-symm :args (tptp.unit tptp.e3)) % 0.37/0.65 (step @p988 :rule eq-symm :args (tptp.unit tptp.e2)) % 0.37/0.65 (step @p989 :rule eq-symm :args (tptp.unit tptp.e1)) % 0.37/0.65 (step @p990 :rule eq-symm :args (tptp.unit tptp.e0)) % 0.37/0.65 (step @p991 :rule nary_cong :premises (@p990 @p989 @p988 @p987 @p986) :args (@t208)) % 0.37/0.65 (step @p992 :rule eq-symm :args (@t209 tptp.e4)) % 0.37/0.65 (step @p993 :rule eq-symm :args (@t210 tptp.e4)) % 0.37/0.65 (step @p994 :rule eq-symm :args (@t211 tptp.e3)) % 0.37/0.65 (step @p995 :rule eq-symm :args (@t212 tptp.e3)) % 0.37/0.65 (step @p996 :rule eq-symm :args (@t213 tptp.e2)) % 0.37/0.65 (step @p997 :rule eq-symm :args (@t214 tptp.e2)) % 0.37/0.65 (step @p998 :rule eq-symm :args (@t215 tptp.e1)) % 0.37/0.65 (step @p999 :rule eq-symm :args (@t216 tptp.e1)) % 0.37/0.65 (step @p1000 :rule eq-symm :args (@t217 tptp.e0)) % 0.37/0.65 (step @p1001 :rule eq-symm :args (@t218 tptp.e0)) % 0.37/0.65 (step @p1002 :rule nary_cong :premises (@p855 @p844 @p833 @p822 @p811) :args (@t219)) % 0.37/0.65 (step @p1003 :rule nary_cong :premises (@p861 @p850 @p839 @p828 @p817) :args (@t220)) % 0.37/0.65 (step @p1004 :rule nary_cong :premises (@p862 @p851 @p840 @p829 @p818) :args (@t221)) % 0.37/0.65 (step @p1005 :rule nary_cong :premises (@p863 @p852 @p841 @p830 @p819) :args (@t222)) % 0.37/0.65 (step @p1006 :rule nary_cong :premises (@p864 @p853 @p842 @p831 @p820) :args (@t223)) % 0.37/0.65 (step @p1007 :rule nary_cong :premises (@p856 @p845 @p834 @p823 @p812) :args (@t224)) % 0.37/0.65 (step @p1008 :rule nary_cong :premises (@p902 @p893 @p884 @p875 @p866) :args (@t225)) % 0.37/0.65 (step @p1009 :rule nary_cong :premises (@p907 @p898 @p889 @p880 @p871) :args (@t226)) % 0.37/0.65 (step @p1010 :rule nary_cong :premises (@p908 @p899 @p890 @p881 @p872) :args (@t227)) % 0.37/0.65 (step @p1011 :rule nary_cong :premises (@p909 @p900 @p891 @p882 @p873) :args (@t228)) % 0.37/0.65 (step @p1012 :rule nary_cong :premises (@p857 @p846 @p835 @p824 @p813) :args (@t229)) % 0.37/0.65 (step @p1013 :rule nary_cong :premises (@p903 @p894 @p885 @p876 @p867) :args (@t230)) % 0.37/0.65 (step @p1014 :rule nary_cong :premises (@p939 @p932 @p925 @p918 @p911) :args (@t231)) % 0.37/0.65 (step @p1015 :rule nary_cong :premises (@p943 @p936 @p929 @p922 @p915) :args (@t232)) % 0.37/0.65 (step @p1016 :rule nary_cong :premises (@p944 @p937 @p930 @p923 @p916) :args (@t233)) % 0.37/0.65 (step @p1017 :rule nary_cong :premises (@p858 @p847 @p836 @p825 @p814) :args (@t234)) % 0.37/0.65 (step @p1018 :rule nary_cong :premises (@p904 @p895 @p886 @p877 @p868) :args (@t235)) % 0.37/0.65 (step @p1019 :rule nary_cong :premises (@p940 @p933 @p926 @p919 @p912) :args (@t236)) % 0.37/0.65 (step @p1020 :rule nary_cong :premises (@p966 @p961 @p956 @p951 @p946) :args (@t237)) % 0.37/0.65 (step @p1021 :rule nary_cong :premises (@p969 @p964 @p959 @p954 @p949) :args (@t238)) % 0.37/0.65 (step @p1022 :rule nary_cong :premises (@p859 @p848 @p837 @p826 @p815) :args (@t239)) % 0.37/0.65 (step @p1023 :rule nary_cong :premises (@p905 @p896 @p887 @p878 @p869) :args (@t240)) % 0.37/0.65 (step @p1024 :rule nary_cong :premises (@p941 @p934 @p927 @p920 @p913) :args (@t241)) % 0.37/0.65 (step @p1025 :rule nary_cong :premises (@p967 @p962 @p957 @p952 @p947) :args (@t242)) % 0.37/0.65 (step @p1026 :rule nary_cong :premises (@p983 @p980 @p977 @p974 @p971) :args (@t243)) % 0.37/0.65 (step @p1027 :rule cong :premises (@p811) :args (@t244)) % 0.37/0.65 (step @p1028 :rule nary_cong :premises (@p1027 @p811) :args (@t245)) % 0.37/0.65 (step @p1029 :rule cong :premises (@p822) :args (@t246)) % 0.37/0.65 (step @p1030 :rule nary_cong :premises (@p1029 @p817) :args (@t247)) % 0.37/0.65 (step @p1031 :rule cong :premises (@p833) :args (@t248)) % 0.37/0.65 (step @p1032 :rule nary_cong :premises (@p1031 @p818) :args (@t249)) % 0.37/0.65 (step @p1033 :rule cong :premises (@p844) :args (@t250)) % 0.37/0.65 (step @p1034 :rule nary_cong :premises (@p1033 @p819) :args (@t251)) % 0.37/0.65 (step @p1035 :rule cong :premises (@p855) :args (@t252)) % 0.37/0.65 (step @p1036 :rule nary_cong :premises (@p1035 @p820) :args (@t253)) % 0.37/0.65 (step @p1037 :rule cong :premises (@p866) :args (@t254)) % 0.37/0.65 (step @p1038 :rule nary_cong :premises (@p1037 @p823) :args (@t255)) % 0.37/0.65 (step @p1039 :rule cong :premises (@p875) :args (@t256)) % 0.37/0.65 (step @p1040 :rule nary_cong :premises (@p1039 @p875) :args (@t257)) % 0.37/0.65 (step @p1041 :rule cong :premises (@p884) :args (@t258)) % 0.37/0.65 (step @p1042 :rule nary_cong :premises (@p1041 @p880) :args (@t259)) % 0.37/0.65 (step @p1043 :rule cong :premises (@p893) :args (@t260)) % 0.37/0.65 (step @p1044 :rule nary_cong :premises (@p1043 @p881) :args (@t261)) % 0.37/0.65 (step @p1045 :rule cong :premises (@p902) :args (@t262)) % 0.37/0.65 (step @p1046 :rule nary_cong :premises (@p1045 @p882) :args (@t263)) % 0.37/0.65 (step @p1047 :rule cong :premises (@p911) :args (@t264)) % 0.37/0.65 (step @p1048 :rule nary_cong :premises (@p1047 @p835) :args (@t265)) % 0.37/0.65 (step @p1049 :rule cong :premises (@p918) :args (@t266)) % 0.37/0.65 (step @p1050 :rule nary_cong :premises (@p1049 @p885) :args (@t267)) % 0.37/0.65 (step @p1051 :rule cong :premises (@p925) :args (@t268)) % 0.37/0.65 (step @p1052 :rule nary_cong :premises (@p1051 @p925) :args (@t269)) % 0.37/0.65 (step @p1053 :rule cong :premises (@p932) :args (@t270)) % 0.37/0.65 (step @p1054 :rule nary_cong :premises (@p1053 @p929) :args (@t271)) % 0.37/0.65 (step @p1055 :rule cong :premises (@p939) :args (@t272)) % 0.37/0.65 (step @p1056 :rule nary_cong :premises (@p1055 @p930) :args (@t273)) % 0.37/0.65 (step @p1057 :rule cong :premises (@p946) :args (@t274)) % 0.37/0.65 (step @p1058 :rule nary_cong :premises (@p1057 @p847) :args (@t275)) % 0.37/0.65 (step @p1059 :rule cong :premises (@p951) :args (@t276)) % 0.37/0.65 (step @p1060 :rule nary_cong :premises (@p1059 @p895) :args (@t277)) % 0.37/0.65 (step @p1061 :rule cong :premises (@p956) :args (@t278)) % 0.37/0.65 (step @p1062 :rule nary_cong :premises (@p1061 @p933) :args (@t279)) % 0.37/0.65 (step @p1063 :rule cong :premises (@p961) :args (@t280)) % 0.37/0.65 (step @p1064 :rule nary_cong :premises (@p1063 @p961) :args (@t281)) % 0.37/0.65 (step @p1065 :rule cong :premises (@p966) :args (@t282)) % 0.37/0.65 (step @p1066 :rule nary_cong :premises (@p1065 @p964) :args (@t283)) % 0.37/0.65 (step @p1067 :rule cong :premises (@p971) :args (@t284)) % 0.37/0.65 (step @p1068 :rule nary_cong :premises (@p1067 @p859) :args (@t285)) % 0.37/0.65 (step @p1069 :rule cong :premises (@p974) :args (@t286)) % 0.37/0.65 (step @p1070 :rule nary_cong :premises (@p1069 @p905) :args (@t287)) % 0.37/0.65 (step @p1071 :rule cong :premises (@p977) :args (@t288)) % 0.37/0.65 (step @p1072 :rule nary_cong :premises (@p1071 @p941) :args (@t289)) % 0.37/0.65 (step @p1073 :rule cong :premises (@p980) :args (@t290)) % 0.37/0.65 (step @p1074 :rule nary_cong :premises (@p1073 @p967) :args (@t291)) % 0.37/0.65 (step @p1075 :rule cong :premises (@p983) :args (@t292)) % 0.37/0.65 (step @p1076 :rule nary_cong :premises (@p1075 @p983) :args (@t293)) % 0.37/0.65 (step @p1077 :rule nary_cong :premises (@p1076 @p1074 @p1072 @p1070 @p1068 @p1066 @p1064 @p1062 @p1060 @p1058 @p1056 @p1054 @p1052 @p1050 @p1048 @p1046 @p1044 @p1042 @p1040 @p1038 @p1036 @p1034 @p1032 @p1030 @p1028 @p1026 @p1025 @p1024 @p1023 @p1022 @p1021 @p1020 @p1019 @p1018 @p1017 @p1016 @p1015 @p1014 @p1013 @p1012 @p1011 @p1010 @p1009 @p1008 @p1007 @p1006 @p1005 @p1004 @p1003 @p1002 @p1001 @p1000 @p999 @p998 @p997 @p996 @p995 @p994 @p993 @p992 @p991 @p985 @p984 @p982 @p981 @p979 @p978 @p976 @p975 @p973 @p972 @p970 @p968 @p965 @p963 @p960 @p958 @p955 @p953 @p950 @p948 @p945 @p942 @p938 @p935 @p931 @p928 @p924 @p921 @p917 @p914 @p910 @p906 @p901 @p897 @p892 @p888 @p883 @p879 @p874 @p870 @p865 @p860 @p854 @p849 @p843 @p838 @p832 @p827 @p821 @p816) :args (@t294)) % 0.37/0.65 (step @p1078 :rule cong :premises (@p1077) :args (@t295)) % 0.37/0.65 (step @p1079 :rule eq_resolve :premises (@p4 @p1078)) % 0.37/0.65 (step @p1080 :rule not_and :premises (@p1079)) % 0.37/0.65 (step @p1081 :rule chain_m_resolution :premises (@p1080 @p810 @p807 @p797 @p763 @p729 @p695 @p693 @p683 @p643 @p603 @p562 @p560 @p550 @p510 @p469 @p467 @p457 @p417 @p408 @p363 @p361 @p348 @p304 @p257 @p248 @p245 @p243 @p241 @p239 @p237 @p235 @p232 @p230 @p228 @p226 @p224 @p222 @p219 @p217 @p215 @p213 @p211 @p209 @p206 @p204 @p202 @p200 @p198 @p196 @p193 @p191 @p188 @p186 @p183 @p181 @p178 @p176 @p173 @p171 @p168 @p165 @p162 @p157 @p155 @p153 @p151 @p149 @p147 @p145 @p143 @p141 @p138 @p133 @p129 @p125 @p123 @p121 @p119 @p117 @p115 @p113 @p110 @p105 @p103 @p101 @p97 @p93 @p91 @p87 @p83 @p81 @p78 @p73 @p71 @p67 @p63 @p61 @p57 @p53 @p49 @p45 @p42 @p37 @p33 @p29 @p25 @p21 @p17 @p13 @p9) :args ((not @t592) (@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 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 @t590 @t589 @t587 @t584 @t581 @t577 @t576 @t574 @t571 @t568 @t565 @t564 @t562 @t559 @t556 @t555 @t553 @t550 @t548 @t544 @t543 @t541 @t536 @t530 @t528 @t527 @t526 @t525 @t524 @t523 @t522 @t521 @t520 @t519 @t518 @t517 @t516 @t515 @t514 @t513 @t512 @t511 @t510 @t509 @t508 @t507 @t506 @t505 @t504 (= tptp.e0 @t218) (= tptp.e0 @t217) (= tptp.e1 @t216) (= tptp.e1 @t215) (= tptp.e2 @t214) (= tptp.e2 @t213) (= tptp.e3 @t212) (= tptp.e3 @t211) (= tptp.e4 @t210) (= tptp.e4 @t209) @t503 @t501 @t498 @t496 @t495 @t493 @t492 @t490 @t489 @t487 @t486 @t484 @t480 @t476 @t473 @t470 @t468 @t465 @t463 @t460 @t458 @t455 @t450 @t446 @t443 @t438 @t434 @t430 @t426 @t421 @t418 @t414 @t408 @t403 @t398 @t392 @t388 @t382 @t377 @t371 @t366 @t361 @t354 @t347 @t341 @t334 @t328 @t321 @t315 @t308 @t301))) % 0.37/0.65 (step @p1082 :rule bool-double-not-elim :args (@t431)) % 0.37/0.65 (step @p1083 :rule refl :args (@t592)) % 0.37/0.65 (step @p1084 :rule nary_cong :premises (@p1083 @p1082) :args ((or @t592 (not @t591)))) % 0.37/0.65 (step @p1085 :rule cnf_or_neg :args (@t592 0)) % 0.37/0.65 (step @p1086 :rule eq_resolve :premises (@p1085 @p1084)) % 0.37/0.65 (step @p1087 :rule reordering :premises (@p1086) :args ((or @t431 @t592))) % 0.37/0.65 (step @p1088 :rule chain_m_resolution :premises (@p1087 @p1081) :args (@t431 @t537 (@list @t592))) % 0.37/0.65 (step @p1089 :rule cnf_or_neg :args (@t592 1)) % 0.37/0.65 (step @p1090 :rule reordering :premises (@p1089) :args ((or @t591 @t592))) % 0.37/0.65 (step @p1091 false :rule chain_m_resolution :premises (@p1090 @p1088 @p1081) :args (false (@list false true) (@list @t431 @t592))) % 0.37/0.65 ) % 0.37/0.65 % SZS output end Proof % 0.37/0.65 % cvc5 exiting %------------------------------------------------------------------------------