%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ALG093+1 : TPTP v9.2.1. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n025.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.35s 0.67s % Output : Proof 0.35s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ALG093+1 : TPTP v9.2.1. Released v2.7.0. % 0.11/0.13 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.15/0.34 % Computer : n025.cluster.edu % 0.15/0.34 % Model : x86_64 x86_64 % 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.34 % Memory : 8042.1875MB % 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.34 % CPULimit : 300 % 0.15/0.34 % WCLimit : 300 % 0.15/0.34 % DateTime : Wed Jun 3 01:39:31 EDT 2026 % 0.15/0.34 % CPUTime : % 0.27/0.52 %----Proving TF0_NAR, FOF, or CNF % 0.35/0.67 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 0.35/0.67 % SZS status Theorem % 0.35/0.67 % SZS output start Proof % 0.35/0.67 ( % 0.35/0.67 (declare-sort $$unsorted 0) % 0.35/0.67 (declare-const tptp.unit $$unsorted) % 0.35/0.67 (declare-const tptp.op (-> $$unsorted $$unsorted $$unsorted)) % 0.35/0.67 (declare-const tptp.e0 $$unsorted) % 0.35/0.67 (declare-const tptp.e1 $$unsorted) % 0.35/0.67 (declare-const tptp.e2 $$unsorted) % 0.35/0.67 (declare-const tptp.e3 $$unsorted) % 0.35/0.67 (declare-const tptp.e4 $$unsorted) % 0.35/0.67 (define @t1 () (tptp.op tptp.e4 tptp.e4)) % 0.35/0.67 (define @t2 () (= @t1 tptp.e2)) % 0.35/0.67 (define @t3 () (tptp.op tptp.e4 tptp.e3)) % 0.35/0.67 (define @t4 () (= @t3 tptp.e1)) % 0.35/0.67 (define @t5 () (tptp.op tptp.e4 tptp.e2)) % 0.35/0.67 (define @t6 () (= @t5 tptp.e0)) % 0.35/0.67 (define @t7 () (tptp.op tptp.e4 tptp.e1)) % 0.35/0.67 (define @t8 () (= @t7 tptp.e3)) % 0.35/0.67 (define @t9 () (tptp.op tptp.e4 tptp.e0)) % 0.35/0.67 (define @t10 () (= @t9 tptp.e4)) % 0.35/0.67 (define @t11 () (tptp.op tptp.e3 tptp.e4)) % 0.35/0.67 (define @t12 () (= @t11 tptp.e0)) % 0.35/0.67 (define @t13 () (tptp.op tptp.e3 tptp.e3)) % 0.35/0.67 (define @t14 () (= @t13 tptp.e4)) % 0.35/0.67 (define @t15 () (tptp.op tptp.e3 tptp.e2)) % 0.35/0.67 (define @t16 () (= @t15 tptp.e1)) % 0.35/0.67 (define @t17 () (tptp.op tptp.e3 tptp.e1)) % 0.35/0.67 (define @t18 () (= @t17 tptp.e2)) % 0.35/0.67 (define @t19 () (tptp.op tptp.e3 tptp.e0)) % 0.35/0.67 (define @t20 () (= @t19 tptp.e3)) % 0.35/0.67 (define @t21 () (tptp.op tptp.e2 tptp.e4)) % 0.35/0.67 (define @t22 () (= @t21 tptp.e1)) % 0.35/0.67 (define @t23 () (tptp.op tptp.e2 tptp.e3)) % 0.35/0.67 (define @t24 () (= @t23 tptp.e0)) % 0.35/0.67 (define @t25 () (tptp.op tptp.e2 tptp.e2)) % 0.35/0.67 (define @t26 () (= @t25 tptp.e3)) % 0.35/0.67 (define @t27 () (tptp.op tptp.e2 tptp.e1)) % 0.35/0.67 (define @t28 () (= @t27 tptp.e4)) % 0.35/0.67 (define @t29 () (tptp.op tptp.e2 tptp.e0)) % 0.35/0.67 (define @t30 () (= @t29 tptp.e2)) % 0.35/0.67 (define @t31 () (tptp.op tptp.e1 tptp.e4)) % 0.35/0.67 (define @t32 () (= @t31 tptp.e3)) % 0.35/0.67 (define @t33 () (tptp.op tptp.e1 tptp.e3)) % 0.35/0.67 (define @t34 () (= @t33 tptp.e2)) % 0.35/0.67 (define @t35 () (tptp.op tptp.e1 tptp.e2)) % 0.35/0.67 (define @t36 () (= @t35 tptp.e4)) % 0.35/0.67 (define @t37 () (tptp.op tptp.e1 tptp.e1)) % 0.35/0.67 (define @t38 () (= @t37 tptp.e0)) % 0.35/0.67 (define @t39 () (tptp.op tptp.e1 tptp.e0)) % 0.35/0.67 (define @t40 () (= @t39 tptp.e1)) % 0.35/0.67 (define @t41 () (tptp.op tptp.e0 tptp.e4)) % 0.35/0.67 (define @t42 () (= @t41 tptp.e4)) % 0.35/0.67 (define @t43 () (tptp.op tptp.e0 tptp.e3)) % 0.35/0.67 (define @t44 () (= @t43 tptp.e3)) % 0.35/0.67 (define @t45 () (tptp.op tptp.e0 tptp.e2)) % 0.35/0.67 (define @t46 () (= @t45 tptp.e2)) % 0.35/0.67 (define @t47 () (tptp.op tptp.e0 tptp.e1)) % 0.35/0.67 (define @t48 () (= @t47 tptp.e1)) % 0.35/0.67 (define @t49 () (tptp.op tptp.e0 tptp.e0)) % 0.35/0.67 (define @t50 () (= @t49 tptp.e0)) % 0.35/0.67 (define @t51 () (= tptp.unit tptp.e0)) % 0.35/0.67 (define @t52 () (= @t1 tptp.e4)) % 0.35/0.67 (define @t53 () (= @t11 tptp.e4)) % 0.35/0.67 (define @t54 () (= @t21 tptp.e4)) % 0.35/0.67 (define @t55 () (= @t31 tptp.e4)) % 0.35/0.67 (define @t56 () (or @t42 @t55 @t54 @t53 @t52)) % 0.35/0.67 (define @t57 () (= @t3 tptp.e4)) % 0.35/0.67 (define @t58 () (= @t5 tptp.e4)) % 0.35/0.67 (define @t59 () (= @t7 tptp.e4)) % 0.35/0.67 (define @t60 () (or @t10 @t59 @t58 @t57 @t52)) % 0.35/0.67 (define @t61 () (= @t1 tptp.e3)) % 0.35/0.67 (define @t62 () (= @t11 tptp.e3)) % 0.35/0.67 (define @t63 () (= @t21 tptp.e3)) % 0.35/0.67 (define @t64 () (= @t41 tptp.e3)) % 0.35/0.67 (define @t65 () (or @t64 @t32 @t63 @t62 @t61)) % 0.35/0.67 (define @t66 () (= @t3 tptp.e3)) % 0.35/0.67 (define @t67 () (= @t5 tptp.e3)) % 0.35/0.67 (define @t68 () (= @t9 tptp.e3)) % 0.35/0.67 (define @t69 () (or @t68 @t8 @t67 @t66 @t61)) % 0.35/0.67 (define @t70 () (= @t11 tptp.e2)) % 0.35/0.67 (define @t71 () (= @t21 tptp.e2)) % 0.35/0.67 (define @t72 () (= @t31 tptp.e2)) % 0.35/0.67 (define @t73 () (= @t41 tptp.e2)) % 0.35/0.67 (define @t74 () (or @t73 @t72 @t71 @t70 @t2)) % 0.35/0.67 (define @t75 () (= @t3 tptp.e2)) % 0.35/0.67 (define @t76 () (= @t5 tptp.e2)) % 0.35/0.67 (define @t77 () (= @t7 tptp.e2)) % 0.35/0.67 (define @t78 () (= @t9 tptp.e2)) % 0.35/0.67 (define @t79 () (or @t78 @t77 @t76 @t75 @t2)) % 0.35/0.67 (define @t80 () (= @t1 tptp.e1)) % 0.35/0.67 (define @t81 () (= @t11 tptp.e1)) % 0.35/0.67 (define @t82 () (= @t31 tptp.e1)) % 0.35/0.67 (define @t83 () (= @t41 tptp.e1)) % 0.35/0.67 (define @t84 () (or @t83 @t82 @t22 @t81 @t80)) % 0.35/0.67 (define @t85 () (= @t5 tptp.e1)) % 0.35/0.67 (define @t86 () (= @t7 tptp.e1)) % 0.35/0.67 (define @t87 () (= @t9 tptp.e1)) % 0.35/0.67 (define @t88 () (or @t87 @t86 @t85 @t4 @t80)) % 0.35/0.67 (define @t89 () (= @t1 tptp.e0)) % 0.35/0.67 (define @t90 () (= @t21 tptp.e0)) % 0.35/0.67 (define @t91 () (= @t31 tptp.e0)) % 0.35/0.67 (define @t92 () (= @t41 tptp.e0)) % 0.35/0.67 (define @t93 () (or @t92 @t91 @t90 @t12 @t89)) % 0.35/0.67 (define @t94 () (= @t3 tptp.e0)) % 0.35/0.67 (define @t95 () (= @t7 tptp.e0)) % 0.35/0.67 (define @t96 () (= @t9 tptp.e0)) % 0.35/0.67 (define @t97 () (or @t96 @t95 @t6 @t94 @t89)) % 0.35/0.67 (define @t98 () (= @t23 tptp.e4)) % 0.35/0.67 (define @t99 () (= @t33 tptp.e4)) % 0.35/0.67 (define @t100 () (= @t43 tptp.e4)) % 0.35/0.67 (define @t101 () (or @t100 @t99 @t98 @t14 @t57)) % 0.35/0.67 (define @t102 () (= @t15 tptp.e4)) % 0.35/0.67 (define @t103 () (= @t17 tptp.e4)) % 0.35/0.67 (define @t104 () (= @t19 tptp.e4)) % 0.35/0.67 (define @t105 () (or @t104 @t103 @t102 @t14 @t53)) % 0.35/0.67 (define @t106 () (= @t13 tptp.e3)) % 0.35/0.67 (define @t107 () (= @t23 tptp.e3)) % 0.35/0.67 (define @t108 () (= @t33 tptp.e3)) % 0.35/0.67 (define @t109 () (or @t44 @t108 @t107 @t106 @t66)) % 0.35/0.67 (define @t110 () (= @t15 tptp.e3)) % 0.35/0.67 (define @t111 () (= @t17 tptp.e3)) % 0.35/0.67 (define @t112 () (or @t20 @t111 @t110 @t106 @t62)) % 0.35/0.67 (define @t113 () (= @t13 tptp.e2)) % 0.35/0.67 (define @t114 () (= @t23 tptp.e2)) % 0.35/0.67 (define @t115 () (= @t43 tptp.e2)) % 0.35/0.67 (define @t116 () (or @t115 @t34 @t114 @t113 @t75)) % 0.35/0.67 (define @t117 () (= @t15 tptp.e2)) % 0.35/0.67 (define @t118 () (= @t19 tptp.e2)) % 0.35/0.67 (define @t119 () (or @t118 @t18 @t117 @t113 @t70)) % 0.35/0.67 (define @t120 () (= @t13 tptp.e1)) % 0.35/0.67 (define @t121 () (= @t23 tptp.e1)) % 0.35/0.67 (define @t122 () (= @t33 tptp.e1)) % 0.35/0.67 (define @t123 () (= @t43 tptp.e1)) % 0.35/0.67 (define @t124 () (or @t123 @t122 @t121 @t120 @t4)) % 0.35/0.67 (define @t125 () (= @t17 tptp.e1)) % 0.35/0.67 (define @t126 () (= @t19 tptp.e1)) % 0.35/0.67 (define @t127 () (or @t126 @t125 @t16 @t120 @t81)) % 0.35/0.67 (define @t128 () (= @t13 tptp.e0)) % 0.35/0.67 (define @t129 () (= @t33 tptp.e0)) % 0.35/0.67 (define @t130 () (= @t43 tptp.e0)) % 0.35/0.67 (define @t131 () (or @t130 @t129 @t24 @t128 @t94)) % 0.35/0.67 (define @t132 () (= @t15 tptp.e0)) % 0.35/0.67 (define @t133 () (= @t17 tptp.e0)) % 0.35/0.67 (define @t134 () (= @t19 tptp.e0)) % 0.35/0.67 (define @t135 () (or @t134 @t133 @t132 @t128 @t12)) % 0.35/0.67 (define @t136 () (= @t25 tptp.e4)) % 0.35/0.67 (define @t137 () (= @t45 tptp.e4)) % 0.35/0.67 (define @t138 () (or @t137 @t36 @t136 @t102 @t58)) % 0.35/0.67 (define @t139 () (= @t29 tptp.e4)) % 0.35/0.67 (define @t140 () (or @t139 @t28 @t136 @t98 @t54)) % 0.35/0.67 (define @t141 () (= @t35 tptp.e3)) % 0.35/0.67 (define @t142 () (= @t45 tptp.e3)) % 0.35/0.67 (define @t143 () (or @t142 @t141 @t26 @t110 @t67)) % 0.35/0.67 (define @t144 () (= @t27 tptp.e3)) % 0.35/0.67 (define @t145 () (= @t29 tptp.e3)) % 0.35/0.67 (define @t146 () (or @t145 @t144 @t26 @t107 @t63)) % 0.35/0.67 (define @t147 () (= @t25 tptp.e2)) % 0.35/0.67 (define @t148 () (= @t35 tptp.e2)) % 0.35/0.67 (define @t149 () (or @t46 @t148 @t147 @t117 @t76)) % 0.35/0.67 (define @t150 () (= @t27 tptp.e2)) % 0.35/0.67 (define @t151 () (or @t30 @t150 @t147 @t114 @t71)) % 0.35/0.67 (define @t152 () (= @t25 tptp.e1)) % 0.35/0.67 (define @t153 () (= @t35 tptp.e1)) % 0.35/0.67 (define @t154 () (= @t45 tptp.e1)) % 0.35/0.67 (define @t155 () (or @t154 @t153 @t152 @t16 @t85)) % 0.35/0.67 (define @t156 () (= @t27 tptp.e1)) % 0.35/0.67 (define @t157 () (= @t29 tptp.e1)) % 0.35/0.67 (define @t158 () (or @t157 @t156 @t152 @t121 @t22)) % 0.35/0.67 (define @t159 () (= @t25 tptp.e0)) % 0.35/0.67 (define @t160 () (= @t35 tptp.e0)) % 0.35/0.67 (define @t161 () (= @t45 tptp.e0)) % 0.35/0.67 (define @t162 () (or @t161 @t160 @t159 @t132 @t6)) % 0.35/0.67 (define @t163 () (= @t27 tptp.e0)) % 0.35/0.67 (define @t164 () (= @t29 tptp.e0)) % 0.35/0.67 (define @t165 () (or @t164 @t163 @t159 @t24 @t90)) % 0.35/0.67 (define @t166 () (= @t37 tptp.e4)) % 0.35/0.67 (define @t167 () (= @t47 tptp.e4)) % 0.35/0.67 (define @t168 () (or @t167 @t166 @t28 @t103 @t59)) % 0.35/0.67 (define @t169 () (= @t39 tptp.e4)) % 0.35/0.67 (define @t170 () (or @t169 @t166 @t36 @t99 @t55)) % 0.35/0.67 (define @t171 () (= @t37 tptp.e3)) % 0.35/0.67 (define @t172 () (= @t47 tptp.e3)) % 0.35/0.67 (define @t173 () (or @t172 @t171 @t144 @t111 @t8)) % 0.35/0.67 (define @t174 () (= @t39 tptp.e3)) % 0.35/0.67 (define @t175 () (or @t174 @t171 @t141 @t108 @t32)) % 0.35/0.67 (define @t176 () (= @t37 tptp.e2)) % 0.35/0.67 (define @t177 () (= @t47 tptp.e2)) % 0.35/0.67 (define @t178 () (or @t177 @t176 @t150 @t18 @t77)) % 0.35/0.67 (define @t179 () (= @t39 tptp.e2)) % 0.35/0.67 (define @t180 () (or @t179 @t176 @t148 @t34 @t72)) % 0.35/0.67 (define @t181 () (= @t37 tptp.e1)) % 0.35/0.67 (define @t182 () (or @t48 @t181 @t156 @t125 @t86)) % 0.35/0.67 (define @t183 () (or @t40 @t181 @t153 @t122 @t82)) % 0.35/0.67 (define @t184 () (= @t47 tptp.e0)) % 0.35/0.67 (define @t185 () (or @t184 @t38 @t163 @t133 @t95)) % 0.35/0.67 (define @t186 () (= @t39 tptp.e0)) % 0.35/0.67 (define @t187 () (or @t186 @t38 @t160 @t129 @t91)) % 0.35/0.67 (define @t188 () (= @t49 tptp.e4)) % 0.35/0.67 (define @t189 () (or @t188 @t169 @t139 @t104 @t10)) % 0.35/0.67 (define @t190 () (or @t188 @t167 @t137 @t100 @t42)) % 0.35/0.67 (define @t191 () (= @t49 tptp.e3)) % 0.35/0.67 (define @t192 () (or @t191 @t174 @t145 @t20 @t68)) % 0.35/0.67 (define @t193 () (or @t191 @t172 @t142 @t44 @t64)) % 0.35/0.67 (define @t194 () (= @t49 tptp.e2)) % 0.35/0.67 (define @t195 () (or @t194 @t179 @t30 @t118 @t78)) % 0.35/0.67 (define @t196 () (or @t194 @t177 @t46 @t115 @t73)) % 0.35/0.67 (define @t197 () (= @t49 tptp.e1)) % 0.35/0.67 (define @t198 () (or @t197 @t40 @t157 @t126 @t87)) % 0.35/0.67 (define @t199 () (or @t197 @t48 @t154 @t123 @t83)) % 0.35/0.67 (define @t200 () (or @t50 @t186 @t164 @t134 @t96)) % 0.35/0.67 (define @t201 () (or @t50 @t184 @t161 @t130 @t92)) % 0.35/0.67 (define @t202 () (or @t51 (= tptp.unit tptp.e1) (= tptp.unit tptp.e2) (= tptp.unit tptp.e3) (= tptp.unit tptp.e4))) % 0.35/0.67 (define @t203 () (tptp.op tptp.e4 tptp.unit)) % 0.35/0.67 (define @t204 () (tptp.op tptp.unit tptp.e4)) % 0.35/0.67 (define @t205 () (tptp.op tptp.e3 tptp.unit)) % 0.35/0.67 (define @t206 () (tptp.op tptp.unit tptp.e3)) % 0.35/0.67 (define @t207 () (tptp.op tptp.e2 tptp.unit)) % 0.35/0.67 (define @t208 () (tptp.op tptp.unit tptp.e2)) % 0.35/0.67 (define @t209 () (tptp.op tptp.e1 tptp.unit)) % 0.35/0.67 (define @t210 () (tptp.op tptp.unit tptp.e1)) % 0.35/0.67 (define @t211 () (tptp.op tptp.e0 tptp.unit)) % 0.35/0.67 (define @t212 () (tptp.op tptp.unit tptp.e0)) % 0.35/0.67 (define @t213 () (or @t89 @t80 @t2 @t61 @t52)) % 0.35/0.67 (define @t214 () (or @t94 @t4 @t75 @t66 @t57)) % 0.35/0.67 (define @t215 () (or @t6 @t85 @t76 @t67 @t58)) % 0.35/0.67 (define @t216 () (or @t95 @t86 @t77 @t8 @t59)) % 0.35/0.67 (define @t217 () (or @t96 @t87 @t78 @t68 @t10)) % 0.35/0.67 (define @t218 () (or @t12 @t81 @t70 @t62 @t53)) % 0.35/0.67 (define @t219 () (or @t128 @t120 @t113 @t106 @t14)) % 0.35/0.67 (define @t220 () (or @t132 @t16 @t117 @t110 @t102)) % 0.35/0.67 (define @t221 () (or @t133 @t125 @t18 @t111 @t103)) % 0.35/0.67 (define @t222 () (or @t134 @t126 @t118 @t20 @t104)) % 0.35/0.67 (define @t223 () (or @t90 @t22 @t71 @t63 @t54)) % 0.35/0.67 (define @t224 () (or @t24 @t121 @t114 @t107 @t98)) % 0.35/0.67 (define @t225 () (or @t159 @t152 @t147 @t26 @t136)) % 0.35/0.67 (define @t226 () (or @t163 @t156 @t150 @t144 @t28)) % 0.35/0.67 (define @t227 () (or @t164 @t157 @t30 @t145 @t139)) % 0.35/0.67 (define @t228 () (or @t91 @t82 @t72 @t32 @t55)) % 0.35/0.67 (define @t229 () (or @t129 @t122 @t34 @t108 @t99)) % 0.35/0.67 (define @t230 () (or @t160 @t153 @t148 @t141 @t36)) % 0.35/0.67 (define @t231 () (or @t38 @t181 @t176 @t171 @t166)) % 0.35/0.67 (define @t232 () (or @t186 @t40 @t179 @t174 @t169)) % 0.35/0.67 (define @t233 () (or @t92 @t83 @t73 @t64 @t42)) % 0.35/0.67 (define @t234 () (or @t130 @t123 @t115 @t44 @t100)) % 0.35/0.67 (define @t235 () (or @t161 @t154 @t46 @t142 @t137)) % 0.35/0.67 (define @t236 () (or @t184 @t48 @t177 @t172 @t167)) % 0.35/0.67 (define @t237 () (or @t50 @t197 @t194 @t191 @t188)) % 0.35/0.67 (define @t238 () (= tptp.e4 tptp.unit)) % 0.35/0.67 (define @t239 () (not @t238)) % 0.35/0.67 (define @t240 () (and @t52 @t239)) % 0.35/0.67 (define @t241 () (not @t52)) % 0.35/0.67 (define @t242 () (or @t241 @t240)) % 0.35/0.67 (define @t243 () (and @t61 @t239)) % 0.35/0.67 (define @t244 () (not @t57)) % 0.35/0.67 (define @t245 () (or @t244 @t243)) % 0.35/0.67 (define @t246 () (and @t2 @t239)) % 0.35/0.67 (define @t247 () (not @t58)) % 0.35/0.67 (define @t248 () (or @t247 @t246)) % 0.35/0.67 (define @t249 () (and @t80 @t239)) % 0.35/0.67 (define @t250 () (not @t59)) % 0.35/0.67 (define @t251 () (or @t250 @t249)) % 0.35/0.67 (define @t252 () (and @t89 @t239)) % 0.35/0.67 (define @t253 () (not @t10)) % 0.35/0.67 (define @t254 () (or @t253 @t252)) % 0.35/0.67 (define @t255 () (and @t53 @t239)) % 0.35/0.67 (define @t256 () (not @t53)) % 0.35/0.67 (define @t257 () (or @t256 @t255)) % 0.35/0.67 (define @t258 () (and @t62 @t239)) % 0.35/0.67 (define @t259 () (not @t14)) % 0.35/0.67 (define @t260 () (or @t259 @t258)) % 0.35/0.67 (define @t261 () (and @t70 @t239)) % 0.35/0.67 (define @t262 () (not @t102)) % 0.35/0.67 (define @t263 () (or @t262 @t261)) % 0.35/0.67 (define @t264 () (and @t81 @t239)) % 0.35/0.67 (define @t265 () (not @t103)) % 0.35/0.67 (define @t266 () (or @t265 @t264)) % 0.35/0.67 (define @t267 () (and @t12 @t239)) % 0.35/0.67 (define @t268 () (not @t104)) % 0.35/0.67 (define @t269 () (or @t268 @t267)) % 0.35/0.67 (define @t270 () (and @t54 @t239)) % 0.35/0.67 (define @t271 () (not @t54)) % 0.35/0.67 (define @t272 () (or @t271 @t270)) % 0.35/0.67 (define @t273 () (and @t63 @t239)) % 0.35/0.67 (define @t274 () (not @t98)) % 0.35/0.67 (define @t275 () (or @t274 @t273)) % 0.35/0.67 (define @t276 () (and @t71 @t239)) % 0.35/0.67 (define @t277 () (not @t136)) % 0.35/0.67 (define @t278 () (or @t277 @t276)) % 0.35/0.67 (define @t279 () (and @t22 @t239)) % 0.35/0.67 (define @t280 () (not @t28)) % 0.35/0.67 (define @t281 () (or @t280 @t279)) % 0.35/0.67 (define @t282 () (and @t90 @t239)) % 0.35/0.67 (define @t283 () (not @t139)) % 0.35/0.67 (define @t284 () (or @t283 @t282)) % 0.35/0.67 (define @t285 () (and @t55 @t239)) % 0.35/0.67 (define @t286 () (not @t55)) % 0.35/0.67 (define @t287 () (or @t286 @t285)) % 0.35/0.67 (define @t288 () (and @t32 @t239)) % 0.35/0.67 (define @t289 () (not @t99)) % 0.35/0.67 (define @t290 () (or @t289 @t288)) % 0.35/0.67 (define @t291 () (and @t72 @t239)) % 0.35/0.67 (define @t292 () (not @t36)) % 0.35/0.67 (define @t293 () (or @t292 @t291)) % 0.35/0.67 (define @t294 () (and @t82 @t239)) % 0.35/0.67 (define @t295 () (not @t166)) % 0.35/0.67 (define @t296 () (or @t295 @t294)) % 0.35/0.67 (define @t297 () (and @t91 @t239)) % 0.35/0.67 (define @t298 () (not @t169)) % 0.35/0.67 (define @t299 () (or @t298 @t297)) % 0.35/0.67 (define @t300 () (and @t42 @t239)) % 0.35/0.67 (define @t301 () (not @t42)) % 0.35/0.67 (define @t302 () (or @t301 @t300)) % 0.35/0.67 (define @t303 () (and @t64 @t239)) % 0.35/0.67 (define @t304 () (not @t100)) % 0.35/0.67 (define @t305 () (or @t304 @t303)) % 0.35/0.67 (define @t306 () (and @t73 @t239)) % 0.35/0.67 (define @t307 () (not @t137)) % 0.35/0.67 (define @t308 () (or @t307 @t306)) % 0.35/0.67 (define @t309 () (and @t83 @t239)) % 0.35/0.67 (define @t310 () (not @t167)) % 0.35/0.67 (define @t311 () (or @t310 @t309)) % 0.35/0.67 (define @t312 () (and @t92 @t239)) % 0.35/0.67 (define @t313 () (not @t188)) % 0.35/0.67 (define @t314 () (or @t313 @t312)) % 0.35/0.67 (define @t315 () (and @t314 @t311 @t308 @t305 @t302 @t299 @t296 @t293 @t290 @t287 @t284 @t281 @t278 @t275 @t272 @t269 @t266 @t263 @t260 @t257 @t254 @t251 @t248 @t245 @t242)) % 0.35/0.67 (define @t316 () (= tptp.e3 tptp.unit)) % 0.35/0.67 (define @t317 () (not @t316)) % 0.35/0.67 (define @t318 () (and @t57 @t317)) % 0.35/0.67 (define @t319 () (not @t61)) % 0.35/0.67 (define @t320 () (or @t319 @t318)) % 0.35/0.67 (define @t321 () (and @t66 @t317)) % 0.35/0.67 (define @t322 () (not @t66)) % 0.35/0.67 (define @t323 () (or @t322 @t321)) % 0.35/0.67 (define @t324 () (and @t75 @t317)) % 0.35/0.67 (define @t325 () (not @t67)) % 0.35/0.67 (define @t326 () (or @t325 @t324)) % 0.35/0.67 (define @t327 () (and @t4 @t317)) % 0.35/0.67 (define @t328 () (not @t8)) % 0.35/0.67 (define @t329 () (or @t328 @t327)) % 0.35/0.67 (define @t330 () (and @t94 @t317)) % 0.35/0.67 (define @t331 () (not @t68)) % 0.35/0.67 (define @t332 () (or @t331 @t330)) % 0.35/0.67 (define @t333 () (and @t14 @t317)) % 0.35/0.67 (define @t334 () (not @t62)) % 0.35/0.67 (define @t335 () (or @t334 @t333)) % 0.35/0.67 (define @t336 () (and @t106 @t317)) % 0.35/0.67 (define @t337 () (not @t106)) % 0.35/0.67 (define @t338 () (or @t337 @t336)) % 0.35/0.67 (define @t339 () (and @t113 @t317)) % 0.35/0.67 (define @t340 () (not @t110)) % 0.35/0.67 (define @t341 () (or @t340 @t339)) % 0.35/0.67 (define @t342 () (and @t120 @t317)) % 0.35/0.67 (define @t343 () (not @t111)) % 0.35/0.67 (define @t344 () (or @t343 @t342)) % 0.35/0.67 (define @t345 () (and @t128 @t317)) % 0.35/0.67 (define @t346 () (not @t20)) % 0.35/0.67 (define @t347 () (or @t346 @t345)) % 0.35/0.67 (define @t348 () (and @t98 @t317)) % 0.35/0.67 (define @t349 () (not @t63)) % 0.35/0.67 (define @t350 () (or @t349 @t348)) % 0.35/0.67 (define @t351 () (and @t107 @t317)) % 0.35/0.67 (define @t352 () (not @t107)) % 0.35/0.67 (define @t353 () (or @t352 @t351)) % 0.35/0.67 (define @t354 () (and @t114 @t317)) % 0.35/0.67 (define @t355 () (not @t26)) % 0.35/0.67 (define @t356 () (or @t355 @t354)) % 0.35/0.67 (define @t357 () (and @t121 @t317)) % 0.35/0.67 (define @t358 () (not @t144)) % 0.35/0.67 (define @t359 () (or @t358 @t357)) % 0.35/0.67 (define @t360 () (and @t24 @t317)) % 0.35/0.67 (define @t361 () (not @t145)) % 0.35/0.67 (define @t362 () (or @t361 @t360)) % 0.35/0.67 (define @t363 () (and @t99 @t317)) % 0.35/0.67 (define @t364 () (not @t32)) % 0.35/0.67 (define @t365 () (or @t364 @t363)) % 0.35/0.67 (define @t366 () (and @t108 @t317)) % 0.35/0.67 (define @t367 () (not @t108)) % 0.35/0.67 (define @t368 () (or @t367 @t366)) % 0.35/0.67 (define @t369 () (and @t34 @t317)) % 0.35/0.67 (define @t370 () (not @t141)) % 0.35/0.67 (define @t371 () (or @t370 @t369)) % 0.35/0.67 (define @t372 () (and @t122 @t317)) % 0.35/0.67 (define @t373 () (not @t171)) % 0.35/0.67 (define @t374 () (or @t373 @t372)) % 0.35/0.67 (define @t375 () (and @t129 @t317)) % 0.35/0.67 (define @t376 () (not @t174)) % 0.35/0.67 (define @t377 () (or @t376 @t375)) % 0.35/0.67 (define @t378 () (and @t100 @t317)) % 0.35/0.67 (define @t379 () (not @t64)) % 0.35/0.67 (define @t380 () (or @t379 @t378)) % 0.35/0.67 (define @t381 () (and @t44 @t317)) % 0.35/0.67 (define @t382 () (not @t44)) % 0.35/0.67 (define @t383 () (or @t382 @t381)) % 0.35/0.67 (define @t384 () (and @t115 @t317)) % 0.35/0.67 (define @t385 () (not @t142)) % 0.35/0.67 (define @t386 () (or @t385 @t384)) % 0.35/0.67 (define @t387 () (and @t123 @t317)) % 0.35/0.67 (define @t388 () (not @t172)) % 0.35/0.67 (define @t389 () (or @t388 @t387)) % 0.35/0.67 (define @t390 () (and @t130 @t317)) % 0.35/0.67 (define @t391 () (not @t191)) % 0.35/0.67 (define @t392 () (or @t391 @t390)) % 0.35/0.67 (define @t393 () (and @t392 @t389 @t386 @t383 @t380 @t377 @t374 @t371 @t368 @t365 @t362 @t359 @t356 @t353 @t350 @t347 @t344 @t341 @t338 @t335 @t332 @t329 @t326 @t323 @t320)) % 0.35/0.67 (define @t394 () (= tptp.e2 tptp.unit)) % 0.35/0.67 (define @t395 () (not @t394)) % 0.35/0.67 (define @t396 () (and @t58 @t395)) % 0.35/0.67 (define @t397 () (not @t2)) % 0.35/0.67 (define @t398 () (or @t397 @t396)) % 0.35/0.67 (define @t399 () (and @t67 @t395)) % 0.35/0.67 (define @t400 () (not @t75)) % 0.35/0.67 (define @t401 () (or @t400 @t399)) % 0.35/0.67 (define @t402 () (and @t76 @t395)) % 0.35/0.67 (define @t403 () (not @t76)) % 0.35/0.67 (define @t404 () (or @t403 @t402)) % 0.35/0.67 (define @t405 () (and @t85 @t395)) % 0.35/0.67 (define @t406 () (not @t77)) % 0.35/0.67 (define @t407 () (or @t406 @t405)) % 0.35/0.67 (define @t408 () (and @t6 @t395)) % 0.35/0.67 (define @t409 () (not @t78)) % 0.35/0.67 (define @t410 () (or @t409 @t408)) % 0.35/0.67 (define @t411 () (and @t102 @t395)) % 0.35/0.67 (define @t412 () (not @t70)) % 0.35/0.67 (define @t413 () (or @t412 @t411)) % 0.35/0.67 (define @t414 () (and @t110 @t395)) % 0.35/0.67 (define @t415 () (not @t113)) % 0.35/0.67 (define @t416 () (or @t415 @t414)) % 0.35/0.67 (define @t417 () (and @t117 @t395)) % 0.35/0.67 (define @t418 () (not @t117)) % 0.35/0.67 (define @t419 () (or @t418 @t417)) % 0.35/0.67 (define @t420 () (and @t16 @t395)) % 0.35/0.67 (define @t421 () (not @t18)) % 0.35/0.67 (define @t422 () (or @t421 @t420)) % 0.35/0.67 (define @t423 () (and @t132 @t395)) % 0.35/0.67 (define @t424 () (not @t118)) % 0.35/0.67 (define @t425 () (or @t424 @t423)) % 0.35/0.67 (define @t426 () (and @t136 @t395)) % 0.35/0.67 (define @t427 () (not @t71)) % 0.35/0.67 (define @t428 () (or @t427 @t426)) % 0.35/0.67 (define @t429 () (and @t26 @t395)) % 0.35/0.67 (define @t430 () (not @t114)) % 0.35/0.67 (define @t431 () (or @t430 @t429)) % 0.35/0.67 (define @t432 () (and @t147 @t395)) % 0.35/0.67 (define @t433 () (not @t147)) % 0.35/0.67 (define @t434 () (or @t433 @t432)) % 0.35/0.67 (define @t435 () (and @t152 @t395)) % 0.35/0.67 (define @t436 () (not @t150)) % 0.35/0.67 (define @t437 () (or @t436 @t435)) % 0.35/0.67 (define @t438 () (and @t159 @t395)) % 0.35/0.67 (define @t439 () (not @t30)) % 0.35/0.67 (define @t440 () (or @t439 @t438)) % 0.35/0.67 (define @t441 () (and @t36 @t395)) % 0.35/0.67 (define @t442 () (not @t72)) % 0.35/0.67 (define @t443 () (or @t442 @t441)) % 0.35/0.67 (define @t444 () (and @t141 @t395)) % 0.35/0.67 (define @t445 () (not @t34)) % 0.35/0.67 (define @t446 () (or @t445 @t444)) % 0.35/0.67 (define @t447 () (and @t148 @t395)) % 0.35/0.67 (define @t448 () (not @t148)) % 0.35/0.67 (define @t449 () (or @t448 @t447)) % 0.35/0.67 (define @t450 () (and @t153 @t395)) % 0.35/0.67 (define @t451 () (not @t176)) % 0.35/0.67 (define @t452 () (or @t451 @t450)) % 0.35/0.67 (define @t453 () (and @t160 @t395)) % 0.35/0.67 (define @t454 () (not @t179)) % 0.35/0.67 (define @t455 () (or @t454 @t453)) % 0.35/0.67 (define @t456 () (and @t137 @t395)) % 0.35/0.67 (define @t457 () (not @t73)) % 0.35/0.67 (define @t458 () (or @t457 @t456)) % 0.35/0.67 (define @t459 () (and @t142 @t395)) % 0.35/0.67 (define @t460 () (not @t115)) % 0.35/0.67 (define @t461 () (or @t460 @t459)) % 0.35/0.67 (define @t462 () (and @t46 @t395)) % 0.35/0.67 (define @t463 () (not @t46)) % 0.35/0.67 (define @t464 () (or @t463 @t462)) % 0.35/0.67 (define @t465 () (and @t154 @t395)) % 0.35/0.67 (define @t466 () (not @t177)) % 0.35/0.67 (define @t467 () (or @t466 @t465)) % 0.35/0.67 (define @t468 () (and @t161 @t395)) % 0.35/0.67 (define @t469 () (not @t194)) % 0.35/0.67 (define @t470 () (or @t469 @t468)) % 0.35/0.67 (define @t471 () (and @t470 @t467 @t464 @t461 @t458 @t455 @t452 @t449 @t446 @t443 @t440 @t437 @t434 @t431 @t428 @t425 @t422 @t419 @t416 @t413 @t410 @t407 @t404 @t401 @t398)) % 0.35/0.67 (define @t472 () (= tptp.e1 tptp.unit)) % 0.35/0.67 (define @t473 () (not @t472)) % 0.35/0.67 (define @t474 () (and @t59 @t473)) % 0.35/0.67 (define @t475 () (not @t80)) % 0.35/0.67 (define @t476 () (or @t475 @t474)) % 0.35/0.67 (define @t477 () (and @t8 @t473)) % 0.35/0.67 (define @t478 () (not @t4)) % 0.35/0.67 (define @t479 () (or @t478 @t477)) % 0.35/0.67 (define @t480 () (and @t77 @t473)) % 0.35/0.67 (define @t481 () (not @t85)) % 0.35/0.67 (define @t482 () (or @t481 @t480)) % 0.35/0.67 (define @t483 () (and @t86 @t473)) % 0.35/0.67 (define @t484 () (not @t86)) % 0.35/0.67 (define @t485 () (or @t484 @t483)) % 0.35/0.67 (define @t486 () (and @t95 @t473)) % 0.35/0.67 (define @t487 () (not @t87)) % 0.35/0.67 (define @t488 () (or @t487 @t486)) % 0.35/0.67 (define @t489 () (and @t103 @t473)) % 0.35/0.67 (define @t490 () (not @t81)) % 0.35/0.67 (define @t491 () (or @t490 @t489)) % 0.35/0.67 (define @t492 () (and @t111 @t473)) % 0.35/0.67 (define @t493 () (not @t120)) % 0.35/0.67 (define @t494 () (or @t493 @t492)) % 0.35/0.67 (define @t495 () (and @t18 @t473)) % 0.35/0.67 (define @t496 () (not @t16)) % 0.35/0.67 (define @t497 () (or @t496 @t495)) % 0.35/0.67 (define @t498 () (and @t125 @t473)) % 0.35/0.67 (define @t499 () (not @t125)) % 0.35/0.67 (define @t500 () (or @t499 @t498)) % 0.35/0.67 (define @t501 () (and @t133 @t473)) % 0.35/0.67 (define @t502 () (not @t126)) % 0.35/0.67 (define @t503 () (or @t502 @t501)) % 0.35/0.67 (define @t504 () (and @t28 @t473)) % 0.35/0.67 (define @t505 () (not @t22)) % 0.35/0.67 (define @t506 () (or @t505 @t504)) % 0.35/0.67 (define @t507 () (and @t144 @t473)) % 0.35/0.67 (define @t508 () (not @t121)) % 0.35/0.67 (define @t509 () (or @t508 @t507)) % 0.35/0.67 (define @t510 () (and @t150 @t473)) % 0.35/0.67 (define @t511 () (not @t152)) % 0.35/0.67 (define @t512 () (or @t511 @t510)) % 0.35/0.67 (define @t513 () (and @t156 @t473)) % 0.35/0.67 (define @t514 () (not @t156)) % 0.35/0.67 (define @t515 () (or @t514 @t513)) % 0.35/0.67 (define @t516 () (and @t163 @t473)) % 0.35/0.67 (define @t517 () (not @t157)) % 0.35/0.67 (define @t518 () (or @t517 @t516)) % 0.35/0.67 (define @t519 () (and @t166 @t473)) % 0.35/0.67 (define @t520 () (not @t82)) % 0.35/0.67 (define @t521 () (or @t520 @t519)) % 0.35/0.67 (define @t522 () (and @t171 @t473)) % 0.35/0.67 (define @t523 () (not @t122)) % 0.35/0.67 (define @t524 () (or @t523 @t522)) % 0.35/0.67 (define @t525 () (and @t176 @t473)) % 0.35/0.67 (define @t526 () (not @t153)) % 0.35/0.67 (define @t527 () (or @t526 @t525)) % 0.35/0.67 (define @t528 () (and @t181 @t473)) % 0.35/0.67 (define @t529 () (not @t181)) % 0.35/0.67 (define @t530 () (or @t529 @t528)) % 0.35/0.67 (define @t531 () (and @t38 @t473)) % 0.35/0.67 (define @t532 () (not @t40)) % 0.35/0.67 (define @t533 () (or @t532 @t531)) % 0.35/0.67 (define @t534 () (and @t167 @t473)) % 0.35/0.67 (define @t535 () (not @t83)) % 0.35/0.67 (define @t536 () (or @t535 @t534)) % 0.35/0.67 (define @t537 () (and @t172 @t473)) % 0.35/0.67 (define @t538 () (not @t123)) % 0.35/0.67 (define @t539 () (or @t538 @t537)) % 0.35/0.67 (define @t540 () (and @t177 @t473)) % 0.35/0.67 (define @t541 () (not @t154)) % 0.35/0.67 (define @t542 () (or @t541 @t540)) % 0.35/0.67 (define @t543 () (and @t48 @t473)) % 0.35/0.67 (define @t544 () (not @t48)) % 0.35/0.67 (define @t545 () (or @t544 @t543)) % 0.35/0.67 (define @t546 () (and @t184 @t473)) % 0.35/0.67 (define @t547 () (not @t197)) % 0.35/0.67 (define @t548 () (or @t547 @t546)) % 0.35/0.67 (define @t549 () (and @t548 @t545 @t542 @t539 @t536 @t533 @t530 @t527 @t524 @t521 @t518 @t515 @t512 @t509 @t506 @t503 @t500 @t497 @t494 @t491 @t488 @t485 @t482 @t479 @t476)) % 0.35/0.67 (define @t550 () (= tptp.e0 tptp.unit)) % 0.35/0.67 (define @t551 () (not @t550)) % 0.35/0.67 (define @t552 () (and @t10 @t551)) % 0.35/0.67 (define @t553 () (not @t89)) % 0.35/0.67 (define @t554 () (or @t553 @t552)) % 0.35/0.67 (define @t555 () (and @t68 @t551)) % 0.35/0.67 (define @t556 () (not @t94)) % 0.35/0.67 (define @t557 () (or @t556 @t555)) % 0.35/0.67 (define @t558 () (and @t78 @t551)) % 0.35/0.67 (define @t559 () (not @t6)) % 0.35/0.67 (define @t560 () (or @t559 @t558)) % 0.35/0.67 (define @t561 () (and @t87 @t551)) % 0.35/0.67 (define @t562 () (not @t95)) % 0.35/0.67 (define @t563 () (or @t562 @t561)) % 0.35/0.67 (define @t564 () (and @t96 @t551)) % 0.35/0.67 (define @t565 () (not @t96)) % 0.35/0.67 (define @t566 () (or @t565 @t564)) % 0.35/0.67 (define @t567 () (and @t104 @t551)) % 0.35/0.67 (define @t568 () (not @t12)) % 0.35/0.67 (define @t569 () (or @t568 @t567)) % 0.35/0.67 (define @t570 () (and @t20 @t551)) % 0.35/0.67 (define @t571 () (not @t128)) % 0.35/0.67 (define @t572 () (or @t571 @t570)) % 0.35/0.67 (define @t573 () (and @t118 @t551)) % 0.35/0.67 (define @t574 () (not @t132)) % 0.35/0.67 (define @t575 () (or @t574 @t573)) % 0.35/0.67 (define @t576 () (and @t126 @t551)) % 0.35/0.67 (define @t577 () (not @t133)) % 0.35/0.67 (define @t578 () (or @t577 @t576)) % 0.35/0.67 (define @t579 () (and @t134 @t551)) % 0.35/0.67 (define @t580 () (not @t134)) % 0.35/0.67 (define @t581 () (or @t580 @t579)) % 0.35/0.67 (define @t582 () (and @t139 @t551)) % 0.35/0.67 (define @t583 () (not @t90)) % 0.35/0.67 (define @t584 () (or @t583 @t582)) % 0.35/0.67 (define @t585 () (and @t145 @t551)) % 0.35/0.67 (define @t586 () (not @t24)) % 0.35/0.67 (define @t587 () (or @t586 @t585)) % 0.35/0.67 (define @t588 () (and @t30 @t551)) % 0.35/0.67 (define @t589 () (not @t159)) % 0.35/0.67 (define @t590 () (or @t589 @t588)) % 0.35/0.67 (define @t591 () (and @t157 @t551)) % 0.35/0.67 (define @t592 () (not @t163)) % 0.35/0.67 (define @t593 () (or @t592 @t591)) % 0.35/0.67 (define @t594 () (and @t164 @t551)) % 0.35/0.67 (define @t595 () (not @t164)) % 0.35/0.67 (define @t596 () (or @t595 @t594)) % 0.35/0.67 (define @t597 () (and @t169 @t551)) % 0.35/0.67 (define @t598 () (not @t91)) % 0.35/0.67 (define @t599 () (or @t598 @t597)) % 0.35/0.67 (define @t600 () (and @t174 @t551)) % 0.35/0.67 (define @t601 () (not @t129)) % 0.35/0.67 (define @t602 () (or @t601 @t600)) % 0.35/0.67 (define @t603 () (and @t179 @t551)) % 0.35/0.67 (define @t604 () (not @t160)) % 0.35/0.67 (define @t605 () (or @t604 @t603)) % 0.35/0.67 (define @t606 () (and @t40 @t551)) % 0.35/0.67 (define @t607 () (not @t38)) % 0.35/0.67 (define @t608 () (or @t607 @t606)) % 0.35/0.67 (define @t609 () (and @t186 @t551)) % 0.35/0.67 (define @t610 () (not @t186)) % 0.35/0.67 (define @t611 () (or @t610 @t609)) % 0.35/0.67 (define @t612 () (and @t188 @t551)) % 0.35/0.67 (define @t613 () (not @t92)) % 0.35/0.67 (define @t614 () (or @t613 @t612)) % 0.35/0.67 (define @t615 () (and @t191 @t551)) % 0.35/0.67 (define @t616 () (not @t130)) % 0.35/0.67 (define @t617 () (or @t616 @t615)) % 0.35/0.67 (define @t618 () (and @t194 @t551)) % 0.35/0.67 (define @t619 () (not @t161)) % 0.35/0.67 (define @t620 () (or @t619 @t618)) % 0.35/0.67 (define @t621 () (and @t197 @t551)) % 0.35/0.67 (define @t622 () (not @t184)) % 0.35/0.67 (define @t623 () (or @t622 @t621)) % 0.35/0.67 (define @t624 () (and @t50 @t551)) % 0.35/0.67 (define @t625 () (not @t50)) % 0.35/0.67 (define @t626 () (or @t625 @t624)) % 0.35/0.67 (define @t627 () (and @t626 @t623 @t620 @t617 @t614 @t611 @t608 @t605 @t602 @t599 @t596 @t593 @t590 @t587 @t584 @t581 @t578 @t575 @t572 @t569 @t566 @t563 @t560 @t557 @t554)) % 0.35/0.67 (define @t628 () (or @t627 @t549 @t471 @t393 @t315)) % 0.35/0.67 (define @t629 () (and @t628 @t237 @t236 @t235 @t234 @t233 @t232 @t231 @t230 @t229 @t228 @t227 @t226 @t225 @t224 @t223 @t222 @t221 @t220 @t219 @t218 @t217 @t216 @t215 @t214 @t213 (= @t212 tptp.e0) (= @t211 tptp.e0) (= @t210 tptp.e1) (= @t209 tptp.e1) (= @t208 tptp.e2) (= @t207 tptp.e2) (= @t206 tptp.e3) (= @t205 tptp.e3) (= @t204 tptp.e4) (= @t203 tptp.e4) @t202 @t201 @t200 @t199 @t198 @t196 @t195 @t193 @t192 @t190 @t189 @t187 @t185 @t183 @t182 @t180 @t178 @t175 @t173 @t170 @t168 @t165 @t162 @t158 @t155 @t151 @t149 @t146 @t143 @t140 @t138 @t135 @t131 @t127 @t124 @t119 @t116 @t112 @t109 @t105 @t101 @t97 @t93 @t88 @t84 @t79 @t74 @t69 @t65 @t60 @t56)) % 0.35/0.67 (define @t630 () (not @t629)) % 0.35/0.67 (define @t631 () (= tptp.e4 @t1)) % 0.35/0.67 (define @t632 () (= tptp.e4 @t11)) % 0.35/0.67 (define @t633 () (= tptp.e4 @t21)) % 0.35/0.67 (define @t634 () (= tptp.e4 @t31)) % 0.35/0.67 (define @t635 () (= tptp.e4 @t41)) % 0.35/0.67 (define @t636 () (or @t635 @t634 @t633 @t632 @t631)) % 0.35/0.67 (define @t637 () (not @t635)) % 0.35/0.67 (define @t638 () (@list false)) % 0.35/0.67 (define @t639 () (@list @t635)) % 0.35/0.67 (define @t640 () (= tptp.e4 @t3)) % 0.35/0.67 (define @t641 () (= tptp.e4 @t5)) % 0.35/0.67 (define @t642 () (= tptp.e4 @t7)) % 0.35/0.67 (define @t643 () (= tptp.e4 @t9)) % 0.35/0.67 (define @t644 () (or @t643 @t642 @t641 @t640 @t631)) % 0.35/0.67 (define @t645 () (not @t643)) % 0.35/0.67 (define @t646 () (@list @t643)) % 0.35/0.67 (define @t647 () (= tptp.e3 @t1)) % 0.35/0.67 (define @t648 () (= tptp.e3 @t11)) % 0.35/0.67 (define @t649 () (= tptp.e3 @t21)) % 0.35/0.67 (define @t650 () (= tptp.e3 @t31)) % 0.35/0.67 (define @t651 () (= tptp.e3 @t41)) % 0.35/0.67 (define @t652 () (or @t651 @t650 @t649 @t648 @t647)) % 0.35/0.67 (define @t653 () (not @t650)) % 0.35/0.67 (define @t654 () (@list @t650)) % 0.35/0.67 (define @t655 () (= tptp.e3 @t3)) % 0.35/0.67 (define @t656 () (= tptp.e3 @t5)) % 0.35/0.67 (define @t657 () (= tptp.e3 @t7)) % 0.35/0.67 (define @t658 () (= tptp.e3 @t9)) % 0.35/0.67 (define @t659 () (or @t658 @t657 @t656 @t655 @t647)) % 0.35/0.67 (define @t660 () (not @t657)) % 0.35/0.67 (define @t661 () (@list @t657)) % 0.35/0.67 (define @t662 () (= tptp.e2 @t1)) % 0.35/0.67 (define @t663 () (= tptp.e2 @t11)) % 0.35/0.67 (define @t664 () (= tptp.e2 @t21)) % 0.35/0.67 (define @t665 () (= tptp.e2 @t31)) % 0.35/0.67 (define @t666 () (= tptp.e2 @t41)) % 0.35/0.67 (define @t667 () (or @t666 @t665 @t664 @t663 @t662)) % 0.35/0.67 (define @t668 () (not @t662)) % 0.35/0.67 (define @t669 () (@list @t662)) % 0.35/0.67 (define @t670 () (= tptp.e2 @t3)) % 0.35/0.67 (define @t671 () (= tptp.e2 @t5)) % 0.35/0.67 (define @t672 () (= tptp.e2 @t7)) % 0.35/0.67 (define @t673 () (= tptp.e2 @t9)) % 0.35/0.67 (define @t674 () (or @t673 @t672 @t671 @t670 @t662)) % 0.35/0.67 (define @t675 () (= tptp.e1 @t1)) % 0.35/0.67 (define @t676 () (= tptp.e1 @t11)) % 0.35/0.67 (define @t677 () (= tptp.e1 @t21)) % 0.35/0.67 (define @t678 () (= tptp.e1 @t31)) % 0.35/0.67 (define @t679 () (= tptp.e1 @t41)) % 0.35/0.67 (define @t680 () (or @t679 @t678 @t677 @t676 @t675)) % 0.35/0.67 (define @t681 () (not @t677)) % 0.35/0.67 (define @t682 () (@list @t677)) % 0.35/0.67 (define @t683 () (= tptp.e1 @t3)) % 0.35/0.67 (define @t684 () (= tptp.e1 @t5)) % 0.35/0.67 (define @t685 () (= tptp.e1 @t7)) % 0.35/0.67 (define @t686 () (= tptp.e1 @t9)) % 0.35/0.67 (define @t687 () (or @t686 @t685 @t684 @t683 @t675)) % 0.35/0.67 (define @t688 () (not @t683)) % 0.35/0.67 (define @t689 () (@list @t683)) % 0.35/0.67 (define @t690 () (= tptp.e0 @t1)) % 0.35/0.67 (define @t691 () (= tptp.e0 @t11)) % 0.35/0.67 (define @t692 () (= tptp.e0 @t21)) % 0.35/0.67 (define @t693 () (= tptp.e0 @t31)) % 0.35/0.67 (define @t694 () (= tptp.e0 @t41)) % 0.35/0.67 (define @t695 () (or @t694 @t693 @t692 @t691 @t690)) % 0.35/0.67 (define @t696 () (not @t691)) % 0.35/0.67 (define @t697 () (@list @t691)) % 0.35/0.67 (define @t698 () (= tptp.e0 @t3)) % 0.35/0.67 (define @t699 () (= tptp.e0 @t5)) % 0.35/0.67 (define @t700 () (= tptp.e0 @t7)) % 0.35/0.67 (define @t701 () (= tptp.e0 @t9)) % 0.35/0.67 (define @t702 () (or @t701 @t700 @t699 @t698 @t690)) % 0.35/0.67 (define @t703 () (not @t699)) % 0.35/0.67 (define @t704 () (@list @t699)) % 0.35/0.67 (define @t705 () (= tptp.e4 @t13)) % 0.35/0.67 (define @t706 () (= tptp.e4 @t23)) % 0.35/0.67 (define @t707 () (= tptp.e4 @t33)) % 0.35/0.67 (define @t708 () (= tptp.e4 @t43)) % 0.35/0.67 (define @t709 () (or @t708 @t707 @t706 @t705 @t640)) % 0.35/0.67 (define @t710 () (not @t705)) % 0.35/0.67 (define @t711 () (@list @t705)) % 0.35/0.67 (define @t712 () (= tptp.e4 @t15)) % 0.35/0.67 (define @t713 () (= tptp.e4 @t17)) % 0.35/0.67 (define @t714 () (= tptp.e4 @t19)) % 0.35/0.67 (define @t715 () (or @t714 @t713 @t712 @t705 @t632)) % 0.35/0.67 (define @t716 () (= tptp.e3 @t13)) % 0.35/0.67 (define @t717 () (= tptp.e3 @t23)) % 0.35/0.67 (define @t718 () (= tptp.e3 @t33)) % 0.35/0.67 (define @t719 () (= tptp.e3 @t43)) % 0.35/0.67 (define @t720 () (or @t719 @t718 @t717 @t716 @t655)) % 0.35/0.67 (define @t721 () (not @t719)) % 0.35/0.67 (define @t722 () (@list @t719)) % 0.35/0.67 (define @t723 () (= tptp.e3 @t15)) % 0.35/0.67 (define @t724 () (= tptp.e3 @t17)) % 0.35/0.67 (define @t725 () (= tptp.e3 @t19)) % 0.35/0.67 (define @t726 () (or @t725 @t724 @t723 @t716 @t648)) % 0.35/0.67 (define @t727 () (not @t725)) % 0.35/0.67 (define @t728 () (@list @t725)) % 0.35/0.67 (define @t729 () (= tptp.e2 @t13)) % 0.35/0.67 (define @t730 () (= tptp.e2 @t23)) % 0.35/0.67 (define @t731 () (= tptp.e2 @t33)) % 0.35/0.67 (define @t732 () (= tptp.e2 @t43)) % 0.35/0.67 (define @t733 () (or @t732 @t731 @t730 @t729 @t670)) % 0.35/0.67 (define @t734 () (not @t731)) % 0.35/0.67 (define @t735 () (@list @t731)) % 0.35/0.67 (define @t736 () (= tptp.e2 @t15)) % 0.35/0.67 (define @t737 () (= tptp.e2 @t17)) % 0.35/0.67 (define @t738 () (= tptp.e2 @t19)) % 0.35/0.67 (define @t739 () (or @t738 @t737 @t736 @t729 @t663)) % 0.35/0.67 (define @t740 () (not @t737)) % 0.35/0.67 (define @t741 () (@list @t737)) % 0.35/0.67 (define @t742 () (= tptp.e1 @t13)) % 0.35/0.67 (define @t743 () (= tptp.e1 @t23)) % 0.35/0.67 (define @t744 () (= tptp.e1 @t33)) % 0.35/0.67 (define @t745 () (= tptp.e1 @t43)) % 0.35/0.67 (define @t746 () (or @t745 @t744 @t743 @t742 @t683)) % 0.35/0.67 (define @t747 () (= tptp.e1 @t15)) % 0.35/0.67 (define @t748 () (= tptp.e1 @t17)) % 0.35/0.67 (define @t749 () (= tptp.e1 @t19)) % 0.35/0.67 (define @t750 () (or @t749 @t748 @t747 @t742 @t676)) % 0.35/0.67 (define @t751 () (not @t747)) % 0.35/0.67 (define @t752 () (@list @t747)) % 0.35/0.67 (define @t753 () (= tptp.e0 @t13)) % 0.35/0.67 (define @t754 () (= tptp.e0 @t23)) % 0.35/0.67 (define @t755 () (= tptp.e0 @t33)) % 0.35/0.67 (define @t756 () (= tptp.e0 @t43)) % 0.35/0.67 (define @t757 () (or @t756 @t755 @t754 @t753 @t698)) % 0.35/0.67 (define @t758 () (not @t754)) % 0.35/0.67 (define @t759 () (@list @t754)) % 0.35/0.67 (define @t760 () (= tptp.e0 @t15)) % 0.35/0.67 (define @t761 () (= tptp.e0 @t17)) % 0.35/0.67 (define @t762 () (= tptp.e0 @t19)) % 0.35/0.67 (define @t763 () (or @t762 @t761 @t760 @t753 @t691)) % 0.35/0.67 (define @t764 () (= tptp.e4 @t25)) % 0.35/0.67 (define @t765 () (= tptp.e4 @t35)) % 0.35/0.67 (define @t766 () (= tptp.e4 @t45)) % 0.35/0.67 (define @t767 () (or @t766 @t765 @t764 @t712 @t641)) % 0.35/0.67 (define @t768 () (not @t765)) % 0.35/0.67 (define @t769 () (@list @t765)) % 0.35/0.67 (define @t770 () (= tptp.e4 @t27)) % 0.35/0.67 (define @t771 () (= tptp.e4 @t29)) % 0.35/0.67 (define @t772 () (or @t771 @t770 @t764 @t706 @t633)) % 0.35/0.67 (define @t773 () (not @t770)) % 0.35/0.67 (define @t774 () (@list @t770)) % 0.35/0.67 (define @t775 () (= tptp.e3 @t25)) % 0.35/0.67 (define @t776 () (= tptp.e3 @t35)) % 0.35/0.67 (define @t777 () (= tptp.e3 @t45)) % 0.35/0.67 (define @t778 () (or @t777 @t776 @t775 @t723 @t656)) % 0.35/0.67 (define @t779 () (not @t775)) % 0.35/0.67 (define @t780 () (@list @t775)) % 0.35/0.67 (define @t781 () (= tptp.e3 @t27)) % 0.35/0.67 (define @t782 () (= tptp.e3 @t29)) % 0.35/0.67 (define @t783 () (or @t782 @t781 @t775 @t717 @t649)) % 0.35/0.67 (define @t784 () (= tptp.e2 @t25)) % 0.35/0.67 (define @t785 () (= tptp.e2 @t35)) % 0.35/0.67 (define @t786 () (= tptp.e2 @t45)) % 0.35/0.67 (define @t787 () (or @t786 @t785 @t784 @t736 @t671)) % 0.35/0.67 (define @t788 () (not @t786)) % 0.35/0.67 (define @t789 () (@list @t786)) % 0.35/0.67 (define @t790 () (= tptp.e2 @t27)) % 0.35/0.67 (define @t791 () (= tptp.e2 @t29)) % 0.35/0.67 (define @t792 () (or @t791 @t790 @t784 @t730 @t664)) % 0.35/0.67 (define @t793 () (not @t791)) % 0.35/0.67 (define @t794 () (@list @t791)) % 0.35/0.67 (define @t795 () (= tptp.e1 @t25)) % 0.35/0.67 (define @t796 () (= tptp.e1 @t35)) % 0.35/0.67 (define @t797 () (= tptp.e1 @t45)) % 0.35/0.67 (define @t798 () (or @t797 @t796 @t795 @t747 @t684)) % 0.35/0.67 (define @t799 () (= tptp.e1 @t27)) % 0.35/0.67 (define @t800 () (= tptp.e1 @t29)) % 0.35/0.67 (define @t801 () (or @t800 @t799 @t795 @t743 @t677)) % 0.35/0.67 (define @t802 () (= tptp.e0 @t25)) % 0.35/0.67 (define @t803 () (= tptp.e0 @t35)) % 0.35/0.67 (define @t804 () (= tptp.e0 @t45)) % 0.35/0.67 (define @t805 () (or @t804 @t803 @t802 @t760 @t699)) % 0.35/0.67 (define @t806 () (= tptp.e0 @t27)) % 0.35/0.67 (define @t807 () (= tptp.e0 @t29)) % 0.35/0.67 (define @t808 () (or @t807 @t806 @t802 @t754 @t692)) % 0.35/0.67 (define @t809 () (= tptp.e4 @t37)) % 0.35/0.67 (define @t810 () (= tptp.e4 @t47)) % 0.35/0.67 (define @t811 () (or @t810 @t809 @t770 @t713 @t642)) % 0.35/0.67 (define @t812 () (= tptp.e4 @t39)) % 0.35/0.67 (define @t813 () (or @t812 @t809 @t765 @t707 @t634)) % 0.35/0.67 (define @t814 () (= tptp.e3 @t37)) % 0.35/0.67 (define @t815 () (= tptp.e3 @t47)) % 0.35/0.67 (define @t816 () (or @t815 @t814 @t781 @t724 @t657)) % 0.35/0.67 (define @t817 () (= tptp.e3 @t39)) % 0.35/0.67 (define @t818 () (or @t817 @t814 @t776 @t718 @t650)) % 0.35/0.67 (define @t819 () (= tptp.e2 @t37)) % 0.35/0.67 (define @t820 () (= tptp.e2 @t47)) % 0.35/0.67 (define @t821 () (or @t820 @t819 @t790 @t737 @t672)) % 0.35/0.67 (define @t822 () (= tptp.e2 @t39)) % 0.35/0.67 (define @t823 () (or @t822 @t819 @t785 @t731 @t665)) % 0.35/0.67 (define @t824 () (= tptp.e1 @t37)) % 0.35/0.67 (define @t825 () (= tptp.e1 @t47)) % 0.35/0.67 (define @t826 () (or @t825 @t824 @t799 @t748 @t685)) % 0.35/0.67 (define @t827 () (not @t825)) % 0.35/0.67 (define @t828 () (@list @t825)) % 0.35/0.67 (define @t829 () (= tptp.e1 @t39)) % 0.35/0.67 (define @t830 () (or @t829 @t824 @t796 @t744 @t678)) % 0.35/0.67 (define @t831 () (not @t829)) % 0.35/0.67 (define @t832 () (@list @t829)) % 0.35/0.67 (define @t833 () (= tptp.e0 @t37)) % 0.35/0.67 (define @t834 () (= tptp.e0 @t47)) % 0.35/0.67 (define @t835 () (or @t834 @t833 @t806 @t761 @t700)) % 0.35/0.67 (define @t836 () (not @t833)) % 0.35/0.67 (define @t837 () (@list @t833)) % 0.35/0.67 (define @t838 () (= tptp.e0 @t39)) % 0.35/0.67 (define @t839 () (or @t838 @t833 @t803 @t755 @t693)) % 0.35/0.67 (define @t840 () (= tptp.e4 @t49)) % 0.35/0.67 (define @t841 () (or @t840 @t812 @t771 @t714 @t643)) % 0.35/0.67 (define @t842 () (or @t840 @t810 @t766 @t708 @t635)) % 0.35/0.67 (define @t843 () (= tptp.e3 @t49)) % 0.35/0.67 (define @t844 () (or @t843 @t817 @t782 @t725 @t658)) % 0.35/0.67 (define @t845 () (or @t843 @t815 @t777 @t719 @t651)) % 0.35/0.67 (define @t846 () (= tptp.e2 @t49)) % 0.35/0.67 (define @t847 () (or @t846 @t822 @t791 @t738 @t673)) % 0.35/0.67 (define @t848 () (or @t846 @t820 @t786 @t732 @t666)) % 0.35/0.67 (define @t849 () (= tptp.e1 @t49)) % 0.35/0.67 (define @t850 () (or @t849 @t829 @t800 @t749 @t686)) % 0.35/0.67 (define @t851 () (or @t849 @t825 @t797 @t745 @t679)) % 0.35/0.67 (define @t852 () (= tptp.e0 @t49)) % 0.35/0.67 (define @t853 () (or @t852 @t838 @t807 @t762 @t701)) % 0.35/0.67 (define @t854 () (not @t852)) % 0.35/0.67 (define @t855 () (@list @t852)) % 0.35/0.67 (define @t856 () (or @t852 @t834 @t804 @t756 @t694)) % 0.35/0.67 (define @t857 () (or @t550 @t472 @t394 @t316 @t238)) % 0.35/0.67 (define @t858 () (or @t690 @t675 @t662 @t647 @t631)) % 0.35/0.67 (define @t859 () (or @t698 @t683 @t670 @t655 @t640)) % 0.35/0.67 (define @t860 () (or @t699 @t684 @t671 @t656 @t641)) % 0.35/0.67 (define @t861 () (or @t700 @t685 @t672 @t657 @t642)) % 0.35/0.67 (define @t862 () (or @t701 @t686 @t673 @t658 @t643)) % 0.35/0.67 (define @t863 () (or @t691 @t676 @t663 @t648 @t632)) % 0.35/0.67 (define @t864 () (or @t753 @t742 @t729 @t716 @t705)) % 0.35/0.67 (define @t865 () (or @t760 @t747 @t736 @t723 @t712)) % 0.35/0.67 (define @t866 () (or @t761 @t748 @t737 @t724 @t713)) % 0.35/0.67 (define @t867 () (or @t762 @t749 @t738 @t725 @t714)) % 0.35/0.67 (define @t868 () (or @t692 @t677 @t664 @t649 @t633)) % 0.35/0.67 (define @t869 () (or @t754 @t743 @t730 @t717 @t706)) % 0.35/0.67 (define @t870 () (or @t802 @t795 @t784 @t775 @t764)) % 0.35/0.67 (define @t871 () (or @t806 @t799 @t790 @t781 @t770)) % 0.35/0.67 (define @t872 () (or @t807 @t800 @t791 @t782 @t771)) % 0.35/0.67 (define @t873 () (or @t693 @t678 @t665 @t650 @t634)) % 0.35/0.67 (define @t874 () (or @t755 @t744 @t731 @t718 @t707)) % 0.35/0.67 (define @t875 () (or @t803 @t796 @t785 @t776 @t765)) % 0.35/0.67 (define @t876 () (or @t833 @t824 @t819 @t814 @t809)) % 0.35/0.67 (define @t877 () (or @t838 @t829 @t822 @t817 @t812)) % 0.35/0.67 (define @t878 () (or @t694 @t679 @t666 @t651 @t635)) % 0.35/0.67 (define @t879 () (or @t756 @t745 @t732 @t719 @t708)) % 0.35/0.67 (define @t880 () (or @t804 @t797 @t786 @t777 @t766)) % 0.35/0.67 (define @t881 () (or @t834 @t825 @t820 @t815 @t810)) % 0.35/0.67 (define @t882 () (or @t852 @t849 @t846 @t843 @t840)) % 0.35/0.67 (define @t883 () (not @t675)) % 0.35/0.67 (define @t884 () (or @t883 (and @t642 @t473))) % 0.35/0.67 (define @t885 () (and @t657 @t473)) % 0.35/0.67 (define @t886 () (or @t688 @t885)) % 0.35/0.67 (define @t887 () (not @t684)) % 0.35/0.67 (define @t888 () (or @t887 (and @t672 @t473))) % 0.35/0.67 (define @t889 () (not @t685)) % 0.35/0.67 (define @t890 () (or @t889 (and @t685 @t473))) % 0.35/0.67 (define @t891 () (not @t686)) % 0.35/0.67 (define @t892 () (or @t891 (and @t700 @t473))) % 0.35/0.67 (define @t893 () (not @t676)) % 0.35/0.67 (define @t894 () (or @t893 (and @t713 @t473))) % 0.35/0.67 (define @t895 () (not @t742)) % 0.35/0.67 (define @t896 () (or @t895 (and @t724 @t473))) % 0.35/0.67 (define @t897 () (and @t737 @t473)) % 0.35/0.67 (define @t898 () (or @t751 @t897)) % 0.35/0.67 (define @t899 () (not @t748)) % 0.35/0.67 (define @t900 () (or @t899 (and @t748 @t473))) % 0.35/0.67 (define @t901 () (not @t749)) % 0.35/0.67 (define @t902 () (or @t901 (and @t761 @t473))) % 0.35/0.67 (define @t903 () (and @t770 @t473)) % 0.35/0.67 (define @t904 () (or @t681 @t903)) % 0.35/0.67 (define @t905 () (not @t743)) % 0.35/0.67 (define @t906 () (or @t905 (and @t781 @t473))) % 0.35/0.67 (define @t907 () (not @t795)) % 0.35/0.67 (define @t908 () (or @t907 (and @t790 @t473))) % 0.35/0.67 (define @t909 () (not @t799)) % 0.35/0.67 (define @t910 () (or @t909 (and @t799 @t473))) % 0.35/0.67 (define @t911 () (not @t800)) % 0.35/0.67 (define @t912 () (or @t911 (and @t806 @t473))) % 0.35/0.67 (define @t913 () (not @t678)) % 0.35/0.67 (define @t914 () (or @t913 (and @t809 @t473))) % 0.35/0.67 (define @t915 () (not @t744)) % 0.35/0.67 (define @t916 () (or @t915 (and @t814 @t473))) % 0.35/0.67 (define @t917 () (not @t796)) % 0.35/0.67 (define @t918 () (or @t917 (and @t819 @t473))) % 0.35/0.67 (define @t919 () (not @t824)) % 0.35/0.67 (define @t920 () (or @t919 (and @t824 @t473))) % 0.35/0.67 (define @t921 () (and @t833 @t473)) % 0.35/0.67 (define @t922 () (or @t831 @t921)) % 0.35/0.67 (define @t923 () (not @t679)) % 0.35/0.67 (define @t924 () (or @t923 (and @t810 @t473))) % 0.35/0.67 (define @t925 () (not @t745)) % 0.35/0.67 (define @t926 () (or @t925 (and @t815 @t473))) % 0.35/0.67 (define @t927 () (not @t797)) % 0.35/0.67 (define @t928 () (or @t927 (and @t820 @t473))) % 0.35/0.67 (define @t929 () (and @t825 @t473)) % 0.35/0.67 (define @t930 () (or @t827 @t929)) % 0.35/0.67 (define @t931 () (not @t849)) % 0.35/0.67 (define @t932 () (or @t931 (and @t834 @t473))) % 0.35/0.67 (define @t933 () (and @t932 @t930 @t928 @t926 @t924 @t922 @t920 @t918 @t916 @t914 @t912 @t910 @t908 @t906 @t904 @t902 @t900 @t898 @t896 @t894 @t892 @t890 @t888 @t886 @t884)) % 0.35/0.67 (define @t934 () (or (and (or @t854 (and @t852 @t551)) (or (not @t834) (and @t849 @t551)) (or (not @t804) (and @t846 @t551)) (or (not @t756) (and @t843 @t551)) (or (not @t694) (and @t840 @t551)) (or (not @t838) (and @t838 @t551)) (or @t836 (and @t829 @t551)) (or (not @t803) (and @t822 @t551)) (or (not @t755) (and @t817 @t551)) (or (not @t693) (and @t812 @t551)) (or (not @t807) (and @t807 @t551)) (or (not @t806) (and @t800 @t551)) (or (not @t802) (and @t791 @t551)) (or @t758 (and @t782 @t551)) (or (not @t692) (and @t771 @t551)) (or (not @t762) (and @t762 @t551)) (or (not @t761) (and @t749 @t551)) (or (not @t760) (and @t738 @t551)) (or (not @t753) (and @t725 @t551)) (or @t696 (and @t714 @t551)) (or (not @t701) (and @t701 @t551)) (or (not @t700) (and @t686 @t551)) (or @t703 (and @t673 @t551)) (or (not @t698) (and @t658 @t551)) (or (not @t690) (and @t643 @t551))) @t933 (and (or (not @t846) (and @t804 @t395)) (or (not @t820) (and @t797 @t395)) (or @t788 (and @t786 @t395)) (or (not @t732) (and @t777 @t395)) (or (not @t666) (and @t766 @t395)) (or (not @t822) (and @t803 @t395)) (or (not @t819) (and @t796 @t395)) (or (not @t785) (and @t785 @t395)) (or @t734 (and @t776 @t395)) (or (not @t665) (and @t765 @t395)) (or @t793 (and @t802 @t395)) (or (not @t790) (and @t795 @t395)) (or (not @t784) (and @t784 @t395)) (or (not @t730) (and @t775 @t395)) (or (not @t664) (and @t764 @t395)) (or (not @t738) (and @t760 @t395)) (or @t740 (and @t747 @t395)) (or (not @t736) (and @t736 @t395)) (or (not @t729) (and @t723 @t395)) (or (not @t663) (and @t712 @t395)) (or (not @t673) (and @t699 @t395)) (or (not @t672) (and @t684 @t395)) (or (not @t671) (and @t671 @t395)) (or (not @t670) (and @t656 @t395)) (or @t668 (and @t641 @t395))) (and (or (not @t843) (and @t756 @t317)) (or (not @t815) (and @t745 @t317)) (or (not @t777) (and @t732 @t317)) (or @t721 (and @t719 @t317)) (or (not @t651) (and @t708 @t317)) (or (not @t817) (and @t755 @t317)) (or (not @t814) (and @t744 @t317)) (or (not @t776) (and @t731 @t317)) (or (not @t718) (and @t718 @t317)) (or @t653 (and @t707 @t317)) (or (not @t782) (and @t754 @t317)) (or (not @t781) (and @t743 @t317)) (or @t779 (and @t730 @t317)) (or (not @t717) (and @t717 @t317)) (or (not @t649) (and @t706 @t317)) (or @t727 (and @t753 @t317)) (or (not @t724) (and @t742 @t317)) (or (not @t723) (and @t729 @t317)) (or (not @t716) (and @t716 @t317)) (or (not @t648) (and @t705 @t317)) (or (not @t658) (and @t698 @t317)) (or @t660 (and @t683 @t317)) (or (not @t656) (and @t670 @t317)) (or (not @t655) (and @t655 @t317)) (or (not @t647) (and @t640 @t317))) (and (or (not @t840) (and @t694 @t239)) (or (not @t810) (and @t679 @t239)) (or (not @t766) (and @t666 @t239)) (or (not @t708) (and @t651 @t239)) (or @t637 (and @t635 @t239)) (or (not @t812) (and @t693 @t239)) (or (not @t809) (and @t678 @t239)) (or @t768 (and @t665 @t239)) (or (not @t707) (and @t650 @t239)) (or (not @t634) (and @t634 @t239)) (or (not @t771) (and @t692 @t239)) (or @t773 (and @t677 @t239)) (or (not @t764) (and @t664 @t239)) (or (not @t706) (and @t649 @t239)) (or (not @t633) (and @t633 @t239)) (or (not @t714) (and @t691 @t239)) (or (not @t713) (and @t676 @t239)) (or (not @t712) (and @t663 @t239)) (or @t710 (and @t648 @t239)) (or (not @t632) (and @t632 @t239)) (or @t645 (and @t690 @t239)) (or (not @t642) (and @t675 @t239)) (or (not @t641) (and @t662 @t239)) (or (not @t640) (and @t647 @t239)) (or (not @t631) (and @t631 @t239))))) % 0.35/0.67 (define @t935 () (@list true)) % 0.35/0.67 (define @t936 () (not @t473)) % 0.35/0.67 (define @t937 () (@list true false)) % 0.35/0.67 (assume @p1 (and (not (= tptp.e0 tptp.e1)) (not (= tptp.e0 tptp.e2)) (not (= tptp.e0 tptp.e3)) (not (= tptp.e0 tptp.e4)) (not (= tptp.e1 tptp.e2)) (not (= tptp.e1 tptp.e3)) (not (= tptp.e1 tptp.e4)) (not (= tptp.e2 tptp.e3)) (not (= tptp.e2 tptp.e4)) (not (= tptp.e3 tptp.e4)))) % 0.35/0.67 (assume @p2 (and @t50 @t48 @t46 @t44 @t42 @t40 @t38 @t36 @t34 @t32 @t30 @t28 @t26 @t24 @t22 @t20 @t18 @t16 @t14 @t12 @t10 @t8 @t6 @t4 @t2)) % 0.35/0.67 (assume @p3 @t51) % 0.35/0.67 (assume @p4 @t630) % 0.35/0.67 (assume @p5 true) % 0.35/0.67 (step @p6 :rule and_elim :premises (@p2) :args (4)) % 0.35/0.67 (step @p7 :rule symm :premises (@p6)) % 0.35/0.67 (step @p8 :rule cnf_or_neg :args (@t636 0)) % 0.35/0.67 (step @p9 :rule reordering :premises (@p8) :args ((or @t637 @t636))) % 0.35/0.67 (step @p10 :rule chain_m_resolution :premises (@p9 @p7) :args (@t636 @t638 @t639)) % 0.35/0.67 (step @p11 :rule and_elim :premises (@p2) :args (20)) % 0.35/0.67 (step @p12 :rule symm :premises (@p11)) % 0.35/0.67 (step @p13 :rule cnf_or_neg :args (@t644 0)) % 0.35/0.67 (step @p14 :rule reordering :premises (@p13) :args ((or @t645 @t644))) % 0.35/0.67 (step @p15 :rule chain_m_resolution :premises (@p14 @p12) :args (@t644 @t638 @t646)) % 0.35/0.67 (step @p16 :rule and_elim :premises (@p2) :args (9)) % 0.35/0.67 (step @p17 :rule symm :premises (@p16)) % 0.35/0.67 (step @p18 :rule cnf_or_neg :args (@t652 1)) % 0.35/0.67 (step @p19 :rule reordering :premises (@p18) :args ((or @t653 @t652))) % 0.35/0.67 (step @p20 :rule chain_m_resolution :premises (@p19 @p17) :args (@t652 @t638 @t654)) % 0.35/0.67 (step @p21 :rule and_elim :premises (@p2) :args (21)) % 0.35/0.67 (step @p22 :rule symm :premises (@p21)) % 0.35/0.67 (step @p23 :rule cnf_or_neg :args (@t659 1)) % 0.35/0.67 (step @p24 :rule reordering :premises (@p23) :args ((or @t660 @t659))) % 0.35/0.67 (step @p25 :rule chain_m_resolution :premises (@p24 @p22) :args (@t659 @t638 @t661)) % 0.35/0.67 (step @p26 :rule and_elim :premises (@p2) :args (24)) % 0.35/0.67 (step @p27 :rule symm :premises (@p26)) % 0.35/0.67 (step @p28 :rule cnf_or_neg :args (@t667 4)) % 0.35/0.67 (step @p29 :rule reordering :premises (@p28) :args ((or @t668 @t667))) % 0.35/0.67 (step @p30 :rule chain_m_resolution :premises (@p29 @p27) :args (@t667 @t638 @t669)) % 0.35/0.67 (step @p31 :rule cnf_or_neg :args (@t674 4)) % 0.35/0.67 (step @p32 :rule reordering :premises (@p31) :args ((or @t668 @t674))) % 0.35/0.67 (step @p33 :rule chain_m_resolution :premises (@p32 @p27) :args (@t674 @t638 @t669)) % 0.35/0.67 (step @p34 :rule and_elim :premises (@p2) :args (14)) % 0.35/0.67 (step @p35 :rule symm :premises (@p34)) % 0.35/0.67 (step @p36 :rule cnf_or_neg :args (@t680 2)) % 0.35/0.67 (step @p37 :rule reordering :premises (@p36) :args ((or @t681 @t680))) % 0.35/0.67 (step @p38 :rule chain_m_resolution :premises (@p37 @p35) :args (@t680 @t638 @t682)) % 0.35/0.67 (step @p39 :rule and_elim :premises (@p2) :args (23)) % 0.35/0.67 (step @p40 :rule symm :premises (@p39)) % 0.35/0.67 (step @p41 :rule cnf_or_neg :args (@t687 3)) % 0.35/0.67 (step @p42 :rule reordering :premises (@p41) :args ((or @t688 @t687))) % 0.35/0.67 (step @p43 :rule chain_m_resolution :premises (@p42 @p40) :args (@t687 @t638 @t689)) % 0.35/0.67 (step @p44 :rule and_elim :premises (@p2) :args (19)) % 0.35/0.67 (step @p45 :rule symm :premises (@p44)) % 0.35/0.67 (step @p46 :rule cnf_or_neg :args (@t695 3)) % 0.35/0.67 (step @p47 :rule reordering :premises (@p46) :args ((or @t696 @t695))) % 0.35/0.67 (step @p48 :rule chain_m_resolution :premises (@p47 @p45) :args (@t695 @t638 @t697)) % 0.35/0.67 (step @p49 :rule and_elim :premises (@p2) :args (22)) % 0.35/0.67 (step @p50 :rule symm :premises (@p49)) % 0.35/0.67 (step @p51 :rule cnf_or_neg :args (@t702 2)) % 0.35/0.67 (step @p52 :rule reordering :premises (@p51) :args ((or @t703 @t702))) % 0.35/0.67 (step @p53 :rule chain_m_resolution :premises (@p52 @p50) :args (@t702 @t638 @t704)) % 0.35/0.67 (step @p54 :rule and_elim :premises (@p2) :args (18)) % 0.35/0.67 (step @p55 :rule symm :premises (@p54)) % 0.35/0.67 (step @p56 :rule cnf_or_neg :args (@t709 3)) % 0.35/0.67 (step @p57 :rule reordering :premises (@p56) :args ((or @t710 @t709))) % 0.35/0.67 (step @p58 :rule chain_m_resolution :premises (@p57 @p55) :args (@t709 @t638 @t711)) % 0.35/0.67 (step @p59 :rule cnf_or_neg :args (@t715 3)) % 0.35/0.67 (step @p60 :rule reordering :premises (@p59) :args ((or @t710 @t715))) % 0.35/0.67 (step @p61 :rule chain_m_resolution :premises (@p60 @p55) :args (@t715 @t638 @t711)) % 0.35/0.67 (step @p62 :rule and_elim :premises (@p2) :args (3)) % 0.35/0.67 (step @p63 :rule symm :premises (@p62)) % 0.35/0.67 (step @p64 :rule cnf_or_neg :args (@t720 0)) % 0.35/0.67 (step @p65 :rule reordering :premises (@p64) :args ((or @t721 @t720))) % 0.35/0.67 (step @p66 :rule chain_m_resolution :premises (@p65 @p63) :args (@t720 @t638 @t722)) % 0.35/0.67 (step @p67 :rule and_elim :premises (@p2) :args (15)) % 0.35/0.67 (step @p68 :rule symm :premises (@p67)) % 0.35/0.67 (step @p69 :rule cnf_or_neg :args (@t726 0)) % 0.35/0.67 (step @p70 :rule reordering :premises (@p69) :args ((or @t727 @t726))) % 0.35/0.67 (step @p71 :rule chain_m_resolution :premises (@p70 @p68) :args (@t726 @t638 @t728)) % 0.35/0.67 (step @p72 :rule and_elim :premises (@p2) :args (8)) % 0.35/0.67 (step @p73 :rule symm :premises (@p72)) % 0.35/0.67 (step @p74 :rule cnf_or_neg :args (@t733 1)) % 0.35/0.67 (step @p75 :rule reordering :premises (@p74) :args ((or @t734 @t733))) % 0.35/0.67 (step @p76 :rule chain_m_resolution :premises (@p75 @p73) :args (@t733 @t638 @t735)) % 0.35/0.67 (step @p77 :rule and_elim :premises (@p2) :args (16)) % 0.35/0.67 (step @p78 :rule symm :premises (@p77)) % 0.35/0.67 (step @p79 :rule cnf_or_neg :args (@t739 1)) % 0.35/0.67 (step @p80 :rule reordering :premises (@p79) :args ((or @t740 @t739))) % 0.35/0.67 (step @p81 :rule chain_m_resolution :premises (@p80 @p78) :args (@t739 @t638 @t741)) % 0.35/0.67 (step @p82 :rule cnf_or_neg :args (@t746 4)) % 0.35/0.67 (step @p83 :rule reordering :premises (@p82) :args ((or @t688 @t746))) % 0.35/0.67 (step @p84 :rule chain_m_resolution :premises (@p83 @p40) :args (@t746 @t638 @t689)) % 0.35/0.67 (step @p85 :rule and_elim :premises (@p2) :args (17)) % 0.35/0.67 (step @p86 :rule symm :premises (@p85)) % 0.35/0.67 (step @p87 :rule cnf_or_neg :args (@t750 2)) % 0.35/0.67 (step @p88 :rule reordering :premises (@p87) :args ((or @t751 @t750))) % 0.35/0.67 (step @p89 :rule chain_m_resolution :premises (@p88 @p86) :args (@t750 @t638 @t752)) % 0.35/0.67 (step @p90 :rule and_elim :premises (@p2) :args (13)) % 0.35/0.67 (step @p91 :rule symm :premises (@p90)) % 0.35/0.67 (step @p92 :rule cnf_or_neg :args (@t757 2)) % 0.35/0.67 (step @p93 :rule reordering :premises (@p92) :args ((or @t758 @t757))) % 0.35/0.67 (step @p94 :rule chain_m_resolution :premises (@p93 @p91) :args (@t757 @t638 @t759)) % 0.35/0.67 (step @p95 :rule cnf_or_neg :args (@t763 4)) % 0.35/0.67 (step @p96 :rule reordering :premises (@p95) :args ((or @t696 @t763))) % 0.35/0.67 (step @p97 :rule chain_m_resolution :premises (@p96 @p45) :args (@t763 @t638 @t697)) % 0.35/0.67 (step @p98 :rule and_elim :premises (@p2) :args (7)) % 0.35/0.67 (step @p99 :rule symm :premises (@p98)) % 0.35/0.67 (step @p100 :rule cnf_or_neg :args (@t767 1)) % 0.35/0.67 (step @p101 :rule reordering :premises (@p100) :args ((or @t768 @t767))) % 0.35/0.67 (step @p102 :rule chain_m_resolution :premises (@p101 @p99) :args (@t767 @t638 @t769)) % 0.35/0.67 (step @p103 :rule and_elim :premises (@p2) :args (11)) % 0.35/0.67 (step @p104 :rule symm :premises (@p103)) % 0.35/0.67 (step @p105 :rule cnf_or_neg :args (@t772 1)) % 0.35/0.67 (step @p106 :rule reordering :premises (@p105) :args ((or @t773 @t772))) % 0.35/0.67 (step @p107 :rule chain_m_resolution :premises (@p106 @p104) :args (@t772 @t638 @t774)) % 0.35/0.67 (step @p108 :rule and_elim :premises (@p2) :args (12)) % 0.35/0.67 (step @p109 :rule symm :premises (@p108)) % 0.35/0.67 (step @p110 :rule cnf_or_neg :args (@t778 2)) % 0.35/0.67 (step @p111 :rule reordering :premises (@p110) :args ((or @t779 @t778))) % 0.35/0.67 (step @p112 :rule chain_m_resolution :premises (@p111 @p109) :args (@t778 @t638 @t780)) % 0.35/0.67 (step @p113 :rule cnf_or_neg :args (@t783 2)) % 0.35/0.67 (step @p114 :rule reordering :premises (@p113) :args ((or @t779 @t783))) % 0.35/0.67 (step @p115 :rule chain_m_resolution :premises (@p114 @p109) :args (@t783 @t638 @t780)) % 0.35/0.67 (step @p116 :rule and_elim :premises (@p2) :args (2)) % 0.35/0.67 (step @p117 :rule symm :premises (@p116)) % 0.35/0.67 (step @p118 :rule cnf_or_neg :args (@t787 0)) % 0.35/0.67 (step @p119 :rule reordering :premises (@p118) :args ((or @t788 @t787))) % 0.35/0.67 (step @p120 :rule chain_m_resolution :premises (@p119 @p117) :args (@t787 @t638 @t789)) % 0.35/0.67 (step @p121 :rule and_elim :premises (@p2) :args (10)) % 0.35/0.67 (step @p122 :rule symm :premises (@p121)) % 0.35/0.67 (step @p123 :rule cnf_or_neg :args (@t792 0)) % 0.35/0.67 (step @p124 :rule reordering :premises (@p123) :args ((or @t793 @t792))) % 0.35/0.67 (step @p125 :rule chain_m_resolution :premises (@p124 @p122) :args (@t792 @t638 @t794)) % 0.35/0.67 (step @p126 :rule cnf_or_neg :args (@t798 3)) % 0.35/0.67 (step @p127 :rule reordering :premises (@p126) :args ((or @t751 @t798))) % 0.35/0.67 (step @p128 :rule chain_m_resolution :premises (@p127 @p86) :args (@t798 @t638 @t752)) % 0.35/0.67 (step @p129 :rule cnf_or_neg :args (@t801 4)) % 0.35/0.67 (step @p130 :rule reordering :premises (@p129) :args ((or @t681 @t801))) % 0.35/0.67 (step @p131 :rule chain_m_resolution :premises (@p130 @p35) :args (@t801 @t638 @t682)) % 0.35/0.67 (step @p132 :rule cnf_or_neg :args (@t805 4)) % 0.35/0.67 (step @p133 :rule reordering :premises (@p132) :args ((or @t703 @t805))) % 0.35/0.67 (step @p134 :rule chain_m_resolution :premises (@p133 @p50) :args (@t805 @t638 @t704)) % 0.35/0.67 (step @p135 :rule cnf_or_neg :args (@t808 3)) % 0.35/0.67 (step @p136 :rule reordering :premises (@p135) :args ((or @t758 @t808))) % 0.35/0.67 (step @p137 :rule chain_m_resolution :premises (@p136 @p91) :args (@t808 @t638 @t759)) % 0.35/0.67 (step @p138 :rule cnf_or_neg :args (@t811 2)) % 0.35/0.67 (step @p139 :rule reordering :premises (@p138) :args ((or @t773 @t811))) % 0.35/0.67 (step @p140 :rule chain_m_resolution :premises (@p139 @p104) :args (@t811 @t638 @t774)) % 0.35/0.67 (step @p141 :rule cnf_or_neg :args (@t813 2)) % 0.35/0.67 (step @p142 :rule reordering :premises (@p141) :args ((or @t768 @t813))) % 0.35/0.67 (step @p143 :rule chain_m_resolution :premises (@p142 @p99) :args (@t813 @t638 @t769)) % 0.35/0.67 (step @p144 :rule cnf_or_neg :args (@t816 4)) % 0.35/0.67 (step @p145 :rule reordering :premises (@p144) :args ((or @t660 @t816))) % 0.35/0.67 (step @p146 :rule chain_m_resolution :premises (@p145 @p22) :args (@t816 @t638 @t661)) % 0.35/0.67 (step @p147 :rule cnf_or_neg :args (@t818 4)) % 0.35/0.67 (step @p148 :rule reordering :premises (@p147) :args ((or @t653 @t818))) % 0.35/0.67 (step @p149 :rule chain_m_resolution :premises (@p148 @p17) :args (@t818 @t638 @t654)) % 0.35/0.67 (step @p150 :rule cnf_or_neg :args (@t821 3)) % 0.35/0.67 (step @p151 :rule reordering :premises (@p150) :args ((or @t740 @t821))) % 0.35/0.67 (step @p152 :rule chain_m_resolution :premises (@p151 @p78) :args (@t821 @t638 @t741)) % 0.35/0.67 (step @p153 :rule cnf_or_neg :args (@t823 3)) % 0.35/0.67 (step @p154 :rule reordering :premises (@p153) :args ((or @t734 @t823))) % 0.35/0.67 (step @p155 :rule chain_m_resolution :premises (@p154 @p73) :args (@t823 @t638 @t735)) % 0.35/0.67 (step @p156 :rule and_elim :premises (@p2) :args (1)) % 0.35/0.67 (step @p157 :rule symm :premises (@p156)) % 0.35/0.67 (step @p158 :rule cnf_or_neg :args (@t826 0)) % 0.35/0.67 (step @p159 :rule reordering :premises (@p158) :args ((or @t827 @t826))) % 0.35/0.67 (step @p160 :rule chain_m_resolution :premises (@p159 @p157) :args (@t826 @t638 @t828)) % 0.35/0.67 (step @p161 :rule and_elim :premises (@p2) :args (5)) % 0.35/0.67 (step @p162 :rule symm :premises (@p161)) % 0.35/0.67 (step @p163 :rule cnf_or_neg :args (@t830 0)) % 0.35/0.67 (step @p164 :rule reordering :premises (@p163) :args ((or @t831 @t830))) % 0.35/0.67 (step @p165 :rule chain_m_resolution :premises (@p164 @p162) :args (@t830 @t638 @t832)) % 0.35/0.67 (step @p166 :rule and_elim :premises (@p2) :args (6)) % 0.35/0.67 (step @p167 :rule symm :premises (@p166)) % 0.35/0.67 (step @p168 :rule cnf_or_neg :args (@t835 1)) % 0.35/0.67 (step @p169 :rule reordering :premises (@p168) :args ((or @t836 @t835))) % 0.35/0.67 (step @p170 :rule chain_m_resolution :premises (@p169 @p167) :args (@t835 @t638 @t837)) % 0.35/0.67 (step @p171 :rule cnf_or_neg :args (@t839 1)) % 0.35/0.67 (step @p172 :rule reordering :premises (@p171) :args ((or @t836 @t839))) % 0.35/0.67 (step @p173 :rule chain_m_resolution :premises (@p172 @p167) :args (@t839 @t638 @t837)) % 0.35/0.67 (step @p174 :rule cnf_or_neg :args (@t841 4)) % 0.35/0.67 (step @p175 :rule reordering :premises (@p174) :args ((or @t645 @t841))) % 0.35/0.67 (step @p176 :rule chain_m_resolution :premises (@p175 @p12) :args (@t841 @t638 @t646)) % 0.35/0.67 (step @p177 :rule cnf_or_neg :args (@t842 4)) % 0.35/0.67 (step @p178 :rule reordering :premises (@p177) :args ((or @t637 @t842))) % 0.35/0.67 (step @p179 :rule chain_m_resolution :premises (@p178 @p7) :args (@t842 @t638 @t639)) % 0.35/0.67 (step @p180 :rule cnf_or_neg :args (@t844 3)) % 0.35/0.67 (step @p181 :rule reordering :premises (@p180) :args ((or @t727 @t844))) % 0.35/0.67 (step @p182 :rule chain_m_resolution :premises (@p181 @p68) :args (@t844 @t638 @t728)) % 0.35/0.67 (step @p183 :rule cnf_or_neg :args (@t845 3)) % 0.35/0.67 (step @p184 :rule reordering :premises (@p183) :args ((or @t721 @t845))) % 0.35/0.67 (step @p185 :rule chain_m_resolution :premises (@p184 @p63) :args (@t845 @t638 @t722)) % 0.35/0.67 (step @p186 :rule cnf_or_neg :args (@t847 2)) % 0.35/0.67 (step @p187 :rule reordering :premises (@p186) :args ((or @t793 @t847))) % 0.35/0.67 (step @p188 :rule chain_m_resolution :premises (@p187 @p122) :args (@t847 @t638 @t794)) % 0.35/0.67 (step @p189 :rule cnf_or_neg :args (@t848 2)) % 0.35/0.67 (step @p190 :rule reordering :premises (@p189) :args ((or @t788 @t848))) % 0.35/0.67 (step @p191 :rule chain_m_resolution :premises (@p190 @p117) :args (@t848 @t638 @t789)) % 0.35/0.67 (step @p192 :rule cnf_or_neg :args (@t850 1)) % 0.35/0.67 (step @p193 :rule reordering :premises (@p192) :args ((or @t831 @t850))) % 0.35/0.67 (step @p194 :rule chain_m_resolution :premises (@p193 @p162) :args (@t850 @t638 @t832)) % 0.35/0.67 (step @p195 :rule cnf_or_neg :args (@t851 1)) % 0.35/0.67 (step @p196 :rule reordering :premises (@p195) :args ((or @t827 @t851))) % 0.35/0.67 (step @p197 :rule chain_m_resolution :premises (@p196 @p157) :args (@t851 @t638 @t828)) % 0.35/0.67 (step @p198 :rule and_elim :premises (@p2) :args (0)) % 0.35/0.67 (step @p199 :rule symm :premises (@p198)) % 0.35/0.67 (step @p200 :rule cnf_or_neg :args (@t853 0)) % 0.35/0.67 (step @p201 :rule reordering :premises (@p200) :args ((or @t854 @t853))) % 0.35/0.67 (step @p202 :rule chain_m_resolution :premises (@p201 @p199) :args (@t853 @t638 @t855)) % 0.35/0.67 (step @p203 :rule cnf_or_neg :args (@t856 0)) % 0.35/0.67 (step @p204 :rule reordering :premises (@p203) :args ((or @t854 @t856))) % 0.35/0.67 (step @p205 :rule chain_m_resolution :premises (@p204 @p199) :args (@t856 @t638 @t855)) % 0.35/0.67 (step @p206 :rule symm :premises (@p3)) % 0.35/0.67 (step @p207 :rule cnf_or_neg :args (@t857 0)) % 0.35/0.67 (step @p208 :rule reordering :premises (@p207) :args ((or @t551 @t857))) % 0.35/0.67 (step @p209 :rule chain_m_resolution :premises (@p208 @p206) :args (@t857 @t638 (@list @t550))) % 0.35/0.67 (step @p210 :rule refl :args (tptp.e4)) % 0.35/0.67 (step @p211 :rule cong :premises (@p210 @p206) :args (@t9)) % 0.35/0.67 (step @p212 :rule trans :premises (@p12 @p211)) % 0.35/0.67 (step @p213 :rule cong :premises (@p206 @p210) :args (@t41)) % 0.35/0.67 (step @p214 :rule trans :premises (@p7 @p213)) % 0.35/0.67 (step @p215 :rule refl :args (tptp.e3)) % 0.35/0.67 (step @p216 :rule cong :premises (@p215 @p206) :args (@t19)) % 0.35/0.67 (step @p217 :rule trans :premises (@p68 @p216)) % 0.35/0.67 (step @p218 :rule cong :premises (@p206 @p215) :args (@t43)) % 0.35/0.67 (step @p219 :rule trans :premises (@p63 @p218)) % 0.35/0.67 (step @p220 :rule refl :args (tptp.e2)) % 0.35/0.67 (step @p221 :rule cong :premises (@p220 @p206) :args (@t29)) % 0.35/0.67 (step @p222 :rule trans :premises (@p122 @p221)) % 0.35/0.67 (step @p223 :rule cong :premises (@p206 @p220) :args (@t45)) % 0.35/0.67 (step @p224 :rule trans :premises (@p117 @p223)) % 0.35/0.67 (step @p225 :rule refl :args (tptp.e1)) % 0.35/0.67 (step @p226 :rule cong :premises (@p225 @p206) :args (@t39)) % 0.35/0.67 (step @p227 :rule trans :premises (@p162 @p226)) % 0.35/0.67 (step @p228 :rule cong :premises (@p206 @p225) :args (@t47)) % 0.35/0.67 (step @p229 :rule trans :premises (@p157 @p228)) % 0.35/0.67 (step @p230 :rule refl :args (tptp.e0)) % 0.35/0.67 (step @p231 :rule cong :premises (@p230 @p206) :args (@t49)) % 0.35/0.67 (step @p232 :rule trans :premises (@p199 @p231)) % 0.35/0.67 (step @p233 :rule cong :premises (@p206 @p230) :args (@t49)) % 0.35/0.67 (step @p234 :rule trans :premises (@p199 @p233)) % 0.35/0.67 (step @p235 :rule cnf_or_neg :args (@t858 2)) % 0.35/0.67 (step @p236 :rule reordering :premises (@p235) :args ((or @t668 @t858))) % 0.35/0.67 (step @p237 :rule chain_m_resolution :premises (@p236 @p27) :args (@t858 @t638 @t669)) % 0.35/0.67 (step @p238 :rule cnf_or_neg :args (@t859 1)) % 0.35/0.67 (step @p239 :rule reordering :premises (@p238) :args ((or @t688 @t859))) % 0.35/0.67 (step @p240 :rule chain_m_resolution :premises (@p239 @p40) :args (@t859 @t638 @t689)) % 0.35/0.67 (step @p241 :rule cnf_or_neg :args (@t860 0)) % 0.35/0.67 (step @p242 :rule reordering :premises (@p241) :args ((or @t703 @t860))) % 0.35/0.67 (step @p243 :rule chain_m_resolution :premises (@p242 @p50) :args (@t860 @t638 @t704)) % 0.35/0.67 (step @p244 :rule cnf_or_neg :args (@t861 3)) % 0.35/0.67 (step @p245 :rule reordering :premises (@p244) :args ((or @t660 @t861))) % 0.35/0.67 (step @p246 :rule chain_m_resolution :premises (@p245 @p22) :args (@t861 @t638 @t661)) % 0.35/0.67 (step @p247 :rule cnf_or_neg :args (@t862 4)) % 0.35/0.67 (step @p248 :rule reordering :premises (@p247) :args ((or @t645 @t862))) % 0.35/0.67 (step @p249 :rule chain_m_resolution :premises (@p248 @p12) :args (@t862 @t638 @t646)) % 0.35/0.67 (step @p250 :rule cnf_or_neg :args (@t863 0)) % 0.35/0.67 (step @p251 :rule reordering :premises (@p250) :args ((or @t696 @t863))) % 0.35/0.67 (step @p252 :rule chain_m_resolution :premises (@p251 @p45) :args (@t863 @t638 @t697)) % 0.35/0.67 (step @p253 :rule cnf_or_neg :args (@t864 4)) % 0.35/0.67 (step @p254 :rule reordering :premises (@p253) :args ((or @t710 @t864))) % 0.35/0.67 (step @p255 :rule chain_m_resolution :premises (@p254 @p55) :args (@t864 @t638 @t711)) % 0.35/0.67 (step @p256 :rule cnf_or_neg :args (@t865 1)) % 0.35/0.67 (step @p257 :rule reordering :premises (@p256) :args ((or @t751 @t865))) % 0.35/0.67 (step @p258 :rule chain_m_resolution :premises (@p257 @p86) :args (@t865 @t638 @t752)) % 0.35/0.67 (step @p259 :rule cnf_or_neg :args (@t866 2)) % 0.35/0.67 (step @p260 :rule reordering :premises (@p259) :args ((or @t740 @t866))) % 0.35/0.67 (step @p261 :rule chain_m_resolution :premises (@p260 @p78) :args (@t866 @t638 @t741)) % 0.35/0.67 (step @p262 :rule cnf_or_neg :args (@t867 3)) % 0.35/0.67 (step @p263 :rule reordering :premises (@p262) :args ((or @t727 @t867))) % 0.35/0.67 (step @p264 :rule chain_m_resolution :premises (@p263 @p68) :args (@t867 @t638 @t728)) % 0.35/0.67 (step @p265 :rule cnf_or_neg :args (@t868 1)) % 0.35/0.67 (step @p266 :rule reordering :premises (@p265) :args ((or @t681 @t868))) % 0.35/0.67 (step @p267 :rule chain_m_resolution :premises (@p266 @p35) :args (@t868 @t638 @t682)) % 0.35/0.67 (step @p268 :rule cnf_or_neg :args (@t869 0)) % 0.35/0.67 (step @p269 :rule reordering :premises (@p268) :args ((or @t758 @t869))) % 0.35/0.67 (step @p270 :rule chain_m_resolution :premises (@p269 @p91) :args (@t869 @t638 @t759)) % 0.35/0.67 (step @p271 :rule cnf_or_neg :args (@t870 3)) % 0.35/0.67 (step @p272 :rule reordering :premises (@p271) :args ((or @t779 @t870))) % 0.35/0.67 (step @p273 :rule chain_m_resolution :premises (@p272 @p109) :args (@t870 @t638 @t780)) % 0.35/0.67 (step @p274 :rule cnf_or_neg :args (@t871 4)) % 0.35/0.67 (step @p275 :rule reordering :premises (@p274) :args ((or @t773 @t871))) % 0.35/0.67 (step @p276 :rule chain_m_resolution :premises (@p275 @p104) :args (@t871 @t638 @t774)) % 0.35/0.67 (step @p277 :rule cnf_or_neg :args (@t872 2)) % 0.35/0.67 (step @p278 :rule reordering :premises (@p277) :args ((or @t793 @t872))) % 0.35/0.67 (step @p279 :rule chain_m_resolution :premises (@p278 @p122) :args (@t872 @t638 @t794)) % 0.35/0.67 (step @p280 :rule cnf_or_neg :args (@t873 3)) % 0.35/0.67 (step @p281 :rule reordering :premises (@p280) :args ((or @t653 @t873))) % 0.35/0.67 (step @p282 :rule chain_m_resolution :premises (@p281 @p17) :args (@t873 @t638 @t654)) % 0.35/0.67 (step @p283 :rule cnf_or_neg :args (@t874 2)) % 0.35/0.67 (step @p284 :rule reordering :premises (@p283) :args ((or @t734 @t874))) % 0.35/0.67 (step @p285 :rule chain_m_resolution :premises (@p284 @p73) :args (@t874 @t638 @t735)) % 0.35/0.67 (step @p286 :rule cnf_or_neg :args (@t875 4)) % 0.35/0.67 (step @p287 :rule reordering :premises (@p286) :args ((or @t768 @t875))) % 0.35/0.67 (step @p288 :rule chain_m_resolution :premises (@p287 @p99) :args (@t875 @t638 @t769)) % 0.35/0.67 (step @p289 :rule cnf_or_neg :args (@t876 0)) % 0.35/0.67 (step @p290 :rule reordering :premises (@p289) :args ((or @t836 @t876))) % 0.35/0.67 (step @p291 :rule chain_m_resolution :premises (@p290 @p167) :args (@t876 @t638 @t837)) % 0.35/0.67 (step @p292 :rule cnf_or_neg :args (@t877 1)) % 0.35/0.67 (step @p293 :rule reordering :premises (@p292) :args ((or @t831 @t877))) % 0.35/0.67 (step @p294 :rule chain_m_resolution :premises (@p293 @p162) :args (@t877 @t638 @t832)) % 0.35/0.67 (step @p295 :rule cnf_or_neg :args (@t878 4)) % 0.35/0.67 (step @p296 :rule reordering :premises (@p295) :args ((or @t637 @t878))) % 0.35/0.67 (step @p297 :rule chain_m_resolution :premises (@p296 @p7) :args (@t878 @t638 @t639)) % 0.35/0.67 (step @p298 :rule cnf_or_neg :args (@t879 3)) % 0.35/0.67 (step @p299 :rule reordering :premises (@p298) :args ((or @t721 @t879))) % 0.35/0.67 (step @p300 :rule chain_m_resolution :premises (@p299 @p63) :args (@t879 @t638 @t722)) % 0.35/0.67 (step @p301 :rule cnf_or_neg :args (@t880 2)) % 0.35/0.67 (step @p302 :rule reordering :premises (@p301) :args ((or @t788 @t880))) % 0.35/0.67 (step @p303 :rule chain_m_resolution :premises (@p302 @p117) :args (@t880 @t638 @t789)) % 0.35/0.67 (step @p304 :rule cnf_or_neg :args (@t881 1)) % 0.35/0.67 (step @p305 :rule reordering :premises (@p304) :args ((or @t827 @t881))) % 0.35/0.67 (step @p306 :rule chain_m_resolution :premises (@p305 @p157) :args (@t881 @t638 @t828)) % 0.35/0.67 (step @p307 :rule cnf_or_neg :args (@t882 0)) % 0.35/0.67 (step @p308 :rule reordering :premises (@p307) :args ((or @t854 @t882))) % 0.35/0.67 (step @p309 :rule chain_m_resolution :premises (@p308 @p199) :args (@t882 @t638 @t855)) % 0.35/0.67 (step @p310 :rule eq-symm :args (@t1 tptp.e4)) % 0.35/0.67 (step @p311 :rule eq-symm :args (@t11 tptp.e4)) % 0.35/0.67 (step @p312 :rule eq-symm :args (@t21 tptp.e4)) % 0.35/0.67 (step @p313 :rule eq-symm :args (@t31 tptp.e4)) % 0.35/0.67 (step @p314 :rule eq-symm :args (@t41 tptp.e4)) % 0.35/0.67 (step @p315 :rule nary_cong :premises (@p314 @p313 @p312 @p311 @p310) :args (@t56)) % 0.35/0.67 (step @p316 :rule eq-symm :args (@t3 tptp.e4)) % 0.35/0.67 (step @p317 :rule eq-symm :args (@t5 tptp.e4)) % 0.35/0.67 (step @p318 :rule eq-symm :args (@t7 tptp.e4)) % 0.35/0.67 (step @p319 :rule eq-symm :args (@t9 tptp.e4)) % 0.35/0.67 (step @p320 :rule nary_cong :premises (@p319 @p318 @p317 @p316 @p310) :args (@t60)) % 0.35/0.67 (step @p321 :rule eq-symm :args (@t1 tptp.e3)) % 0.35/0.67 (step @p322 :rule eq-symm :args (@t11 tptp.e3)) % 0.35/0.67 (step @p323 :rule eq-symm :args (@t21 tptp.e3)) % 0.35/0.67 (step @p324 :rule eq-symm :args (@t31 tptp.e3)) % 0.35/0.67 (step @p325 :rule eq-symm :args (@t41 tptp.e3)) % 0.35/0.67 (step @p326 :rule nary_cong :premises (@p325 @p324 @p323 @p322 @p321) :args (@t65)) % 0.35/0.67 (step @p327 :rule eq-symm :args (@t3 tptp.e3)) % 0.35/0.67 (step @p328 :rule eq-symm :args (@t5 tptp.e3)) % 0.35/0.67 (step @p329 :rule eq-symm :args (@t7 tptp.e3)) % 0.35/0.67 (step @p330 :rule eq-symm :args (@t9 tptp.e3)) % 0.35/0.67 (step @p331 :rule nary_cong :premises (@p330 @p329 @p328 @p327 @p321) :args (@t69)) % 0.35/0.67 (step @p332 :rule eq-symm :args (@t1 tptp.e2)) % 0.35/0.67 (step @p333 :rule eq-symm :args (@t11 tptp.e2)) % 0.35/0.67 (step @p334 :rule eq-symm :args (@t21 tptp.e2)) % 0.35/0.67 (step @p335 :rule eq-symm :args (@t31 tptp.e2)) % 0.35/0.67 (step @p336 :rule eq-symm :args (@t41 tptp.e2)) % 0.35/0.67 (step @p337 :rule nary_cong :premises (@p336 @p335 @p334 @p333 @p332) :args (@t74)) % 0.35/0.67 (step @p338 :rule eq-symm :args (@t3 tptp.e2)) % 0.35/0.67 (step @p339 :rule eq-symm :args (@t5 tptp.e2)) % 0.35/0.67 (step @p340 :rule eq-symm :args (@t7 tptp.e2)) % 0.35/0.67 (step @p341 :rule eq-symm :args (@t9 tptp.e2)) % 0.35/0.67 (step @p342 :rule nary_cong :premises (@p341 @p340 @p339 @p338 @p332) :args (@t79)) % 0.35/0.67 (step @p343 :rule eq-symm :args (@t1 tptp.e1)) % 0.35/0.67 (step @p344 :rule eq-symm :args (@t11 tptp.e1)) % 0.35/0.67 (step @p345 :rule eq-symm :args (@t21 tptp.e1)) % 0.35/0.67 (step @p346 :rule eq-symm :args (@t31 tptp.e1)) % 0.35/0.67 (step @p347 :rule eq-symm :args (@t41 tptp.e1)) % 0.35/0.67 (step @p348 :rule nary_cong :premises (@p347 @p346 @p345 @p344 @p343) :args (@t84)) % 0.35/0.67 (step @p349 :rule eq-symm :args (@t3 tptp.e1)) % 0.35/0.67 (step @p350 :rule eq-symm :args (@t5 tptp.e1)) % 0.35/0.67 (step @p351 :rule eq-symm :args (@t7 tptp.e1)) % 0.35/0.67 (step @p352 :rule eq-symm :args (@t9 tptp.e1)) % 0.35/0.67 (step @p353 :rule nary_cong :premises (@p352 @p351 @p350 @p349 @p343) :args (@t88)) % 0.35/0.67 (step @p354 :rule eq-symm :args (@t1 tptp.e0)) % 0.35/0.67 (step @p355 :rule eq-symm :args (@t11 tptp.e0)) % 0.35/0.67 (step @p356 :rule eq-symm :args (@t21 tptp.e0)) % 0.35/0.67 (step @p357 :rule eq-symm :args (@t31 tptp.e0)) % 0.35/0.67 (step @p358 :rule eq-symm :args (@t41 tptp.e0)) % 0.35/0.67 (step @p359 :rule nary_cong :premises (@p358 @p357 @p356 @p355 @p354) :args (@t93)) % 0.35/0.67 (step @p360 :rule eq-symm :args (@t3 tptp.e0)) % 0.35/0.67 (step @p361 :rule eq-symm :args (@t5 tptp.e0)) % 0.35/0.67 (step @p362 :rule eq-symm :args (@t7 tptp.e0)) % 0.35/0.67 (step @p363 :rule eq-symm :args (@t9 tptp.e0)) % 0.35/0.67 (step @p364 :rule nary_cong :premises (@p363 @p362 @p361 @p360 @p354) :args (@t97)) % 0.35/0.67 (step @p365 :rule eq-symm :args (@t13 tptp.e4)) % 0.35/0.67 (step @p366 :rule eq-symm :args (@t23 tptp.e4)) % 0.35/0.67 (step @p367 :rule eq-symm :args (@t33 tptp.e4)) % 0.35/0.67 (step @p368 :rule eq-symm :args (@t43 tptp.e4)) % 0.35/0.67 (step @p369 :rule nary_cong :premises (@p368 @p367 @p366 @p365 @p316) :args (@t101)) % 0.35/0.67 (step @p370 :rule eq-symm :args (@t15 tptp.e4)) % 0.35/0.67 (step @p371 :rule eq-symm :args (@t17 tptp.e4)) % 0.35/0.67 (step @p372 :rule eq-symm :args (@t19 tptp.e4)) % 0.35/0.67 (step @p373 :rule nary_cong :premises (@p372 @p371 @p370 @p365 @p311) :args (@t105)) % 0.35/0.67 (step @p374 :rule eq-symm :args (@t13 tptp.e3)) % 0.35/0.67 (step @p375 :rule eq-symm :args (@t23 tptp.e3)) % 0.35/0.67 (step @p376 :rule eq-symm :args (@t33 tptp.e3)) % 0.35/0.67 (step @p377 :rule eq-symm :args (@t43 tptp.e3)) % 0.35/0.67 (step @p378 :rule nary_cong :premises (@p377 @p376 @p375 @p374 @p327) :args (@t109)) % 0.35/0.67 (step @p379 :rule eq-symm :args (@t15 tptp.e3)) % 0.35/0.67 (step @p380 :rule eq-symm :args (@t17 tptp.e3)) % 0.35/0.67 (step @p381 :rule eq-symm :args (@t19 tptp.e3)) % 0.35/0.67 (step @p382 :rule nary_cong :premises (@p381 @p380 @p379 @p374 @p322) :args (@t112)) % 0.35/0.67 (step @p383 :rule eq-symm :args (@t13 tptp.e2)) % 0.35/0.67 (step @p384 :rule eq-symm :args (@t23 tptp.e2)) % 0.35/0.67 (step @p385 :rule eq-symm :args (@t33 tptp.e2)) % 0.35/0.67 (step @p386 :rule eq-symm :args (@t43 tptp.e2)) % 0.35/0.67 (step @p387 :rule nary_cong :premises (@p386 @p385 @p384 @p383 @p338) :args (@t116)) % 0.35/0.67 (step @p388 :rule eq-symm :args (@t15 tptp.e2)) % 0.35/0.67 (step @p389 :rule eq-symm :args (@t17 tptp.e2)) % 0.35/0.67 (step @p390 :rule eq-symm :args (@t19 tptp.e2)) % 0.35/0.67 (step @p391 :rule nary_cong :premises (@p390 @p389 @p388 @p383 @p333) :args (@t119)) % 0.35/0.67 (step @p392 :rule eq-symm :args (@t13 tptp.e1)) % 0.35/0.67 (step @p393 :rule eq-symm :args (@t23 tptp.e1)) % 0.35/0.67 (step @p394 :rule eq-symm :args (@t33 tptp.e1)) % 0.35/0.67 (step @p395 :rule eq-symm :args (@t43 tptp.e1)) % 0.35/0.67 (step @p396 :rule nary_cong :premises (@p395 @p394 @p393 @p392 @p349) :args (@t124)) % 0.35/0.67 (step @p397 :rule eq-symm :args (@t15 tptp.e1)) % 0.35/0.67 (step @p398 :rule eq-symm :args (@t17 tptp.e1)) % 0.35/0.67 (step @p399 :rule eq-symm :args (@t19 tptp.e1)) % 0.35/0.67 (step @p400 :rule nary_cong :premises (@p399 @p398 @p397 @p392 @p344) :args (@t127)) % 0.35/0.67 (step @p401 :rule eq-symm :args (@t13 tptp.e0)) % 0.35/0.67 (step @p402 :rule eq-symm :args (@t23 tptp.e0)) % 0.35/0.67 (step @p403 :rule eq-symm :args (@t33 tptp.e0)) % 0.35/0.67 (step @p404 :rule eq-symm :args (@t43 tptp.e0)) % 0.35/0.67 (step @p405 :rule nary_cong :premises (@p404 @p403 @p402 @p401 @p360) :args (@t131)) % 0.35/0.67 (step @p406 :rule eq-symm :args (@t15 tptp.e0)) % 0.35/0.67 (step @p407 :rule eq-symm :args (@t17 tptp.e0)) % 0.35/0.67 (step @p408 :rule eq-symm :args (@t19 tptp.e0)) % 0.35/0.67 (step @p409 :rule nary_cong :premises (@p408 @p407 @p406 @p401 @p355) :args (@t135)) % 0.35/0.67 (step @p410 :rule eq-symm :args (@t25 tptp.e4)) % 0.35/0.67 (step @p411 :rule eq-symm :args (@t35 tptp.e4)) % 0.35/0.67 (step @p412 :rule eq-symm :args (@t45 tptp.e4)) % 0.35/0.67 (step @p413 :rule nary_cong :premises (@p412 @p411 @p410 @p370 @p317) :args (@t138)) % 0.35/0.67 (step @p414 :rule eq-symm :args (@t27 tptp.e4)) % 0.35/0.67 (step @p415 :rule eq-symm :args (@t29 tptp.e4)) % 0.35/0.67 (step @p416 :rule nary_cong :premises (@p415 @p414 @p410 @p366 @p312) :args (@t140)) % 0.35/0.67 (step @p417 :rule eq-symm :args (@t25 tptp.e3)) % 0.35/0.67 (step @p418 :rule eq-symm :args (@t35 tptp.e3)) % 0.35/0.67 (step @p419 :rule eq-symm :args (@t45 tptp.e3)) % 0.35/0.67 (step @p420 :rule nary_cong :premises (@p419 @p418 @p417 @p379 @p328) :args (@t143)) % 0.35/0.67 (step @p421 :rule eq-symm :args (@t27 tptp.e3)) % 0.35/0.67 (step @p422 :rule eq-symm :args (@t29 tptp.e3)) % 0.35/0.67 (step @p423 :rule nary_cong :premises (@p422 @p421 @p417 @p375 @p323) :args (@t146)) % 0.35/0.67 (step @p424 :rule eq-symm :args (@t25 tptp.e2)) % 0.35/0.67 (step @p425 :rule eq-symm :args (@t35 tptp.e2)) % 0.35/0.67 (step @p426 :rule eq-symm :args (@t45 tptp.e2)) % 0.35/0.67 (step @p427 :rule nary_cong :premises (@p426 @p425 @p424 @p388 @p339) :args (@t149)) % 0.35/0.67 (step @p428 :rule eq-symm :args (@t27 tptp.e2)) % 0.35/0.67 (step @p429 :rule eq-symm :args (@t29 tptp.e2)) % 0.35/0.67 (step @p430 :rule nary_cong :premises (@p429 @p428 @p424 @p384 @p334) :args (@t151)) % 0.35/0.67 (step @p431 :rule eq-symm :args (@t25 tptp.e1)) % 0.35/0.67 (step @p432 :rule eq-symm :args (@t35 tptp.e1)) % 0.35/0.67 (step @p433 :rule eq-symm :args (@t45 tptp.e1)) % 0.35/0.67 (step @p434 :rule nary_cong :premises (@p433 @p432 @p431 @p397 @p350) :args (@t155)) % 0.35/0.67 (step @p435 :rule eq-symm :args (@t27 tptp.e1)) % 0.35/0.67 (step @p436 :rule eq-symm :args (@t29 tptp.e1)) % 0.35/0.67 (step @p437 :rule nary_cong :premises (@p436 @p435 @p431 @p393 @p345) :args (@t158)) % 0.35/0.67 (step @p438 :rule eq-symm :args (@t25 tptp.e0)) % 0.35/0.67 (step @p439 :rule eq-symm :args (@t35 tptp.e0)) % 0.35/0.67 (step @p440 :rule eq-symm :args (@t45 tptp.e0)) % 0.35/0.67 (step @p441 :rule nary_cong :premises (@p440 @p439 @p438 @p406 @p361) :args (@t162)) % 0.35/0.67 (step @p442 :rule eq-symm :args (@t27 tptp.e0)) % 0.35/0.67 (step @p443 :rule eq-symm :args (@t29 tptp.e0)) % 0.35/0.67 (step @p444 :rule nary_cong :premises (@p443 @p442 @p438 @p402 @p356) :args (@t165)) % 0.35/0.67 (step @p445 :rule eq-symm :args (@t37 tptp.e4)) % 0.35/0.67 (step @p446 :rule eq-symm :args (@t47 tptp.e4)) % 0.35/0.67 (step @p447 :rule nary_cong :premises (@p446 @p445 @p414 @p371 @p318) :args (@t168)) % 0.35/0.67 (step @p448 :rule eq-symm :args (@t39 tptp.e4)) % 0.35/0.67 (step @p449 :rule nary_cong :premises (@p448 @p445 @p411 @p367 @p313) :args (@t170)) % 0.35/0.67 (step @p450 :rule eq-symm :args (@t37 tptp.e3)) % 0.35/0.67 (step @p451 :rule eq-symm :args (@t47 tptp.e3)) % 0.35/0.67 (step @p452 :rule nary_cong :premises (@p451 @p450 @p421 @p380 @p329) :args (@t173)) % 0.35/0.67 (step @p453 :rule eq-symm :args (@t39 tptp.e3)) % 0.35/0.67 (step @p454 :rule nary_cong :premises (@p453 @p450 @p418 @p376 @p324) :args (@t175)) % 0.35/0.67 (step @p455 :rule eq-symm :args (@t37 tptp.e2)) % 0.35/0.67 (step @p456 :rule eq-symm :args (@t47 tptp.e2)) % 0.35/0.67 (step @p457 :rule nary_cong :premises (@p456 @p455 @p428 @p389 @p340) :args (@t178)) % 0.35/0.67 (step @p458 :rule eq-symm :args (@t39 tptp.e2)) % 0.35/0.67 (step @p459 :rule nary_cong :premises (@p458 @p455 @p425 @p385 @p335) :args (@t180)) % 0.35/0.67 (step @p460 :rule eq-symm :args (@t37 tptp.e1)) % 0.35/0.67 (step @p461 :rule eq-symm :args (@t47 tptp.e1)) % 0.35/0.67 (step @p462 :rule nary_cong :premises (@p461 @p460 @p435 @p398 @p351) :args (@t182)) % 0.35/0.67 (step @p463 :rule eq-symm :args (@t39 tptp.e1)) % 0.35/0.67 (step @p464 :rule nary_cong :premises (@p463 @p460 @p432 @p394 @p346) :args (@t183)) % 0.35/0.67 (step @p465 :rule eq-symm :args (@t37 tptp.e0)) % 0.35/0.67 (step @p466 :rule eq-symm :args (@t47 tptp.e0)) % 0.35/0.67 (step @p467 :rule nary_cong :premises (@p466 @p465 @p442 @p407 @p362) :args (@t185)) % 0.35/0.67 (step @p468 :rule eq-symm :args (@t39 tptp.e0)) % 0.35/0.67 (step @p469 :rule nary_cong :premises (@p468 @p465 @p439 @p403 @p357) :args (@t187)) % 0.35/0.67 (step @p470 :rule eq-symm :args (@t49 tptp.e4)) % 0.35/0.67 (step @p471 :rule nary_cong :premises (@p470 @p448 @p415 @p372 @p319) :args (@t189)) % 0.35/0.67 (step @p472 :rule nary_cong :premises (@p470 @p446 @p412 @p368 @p314) :args (@t190)) % 0.35/0.67 (step @p473 :rule eq-symm :args (@t49 tptp.e3)) % 0.35/0.67 (step @p474 :rule nary_cong :premises (@p473 @p453 @p422 @p381 @p330) :args (@t192)) % 0.35/0.67 (step @p475 :rule nary_cong :premises (@p473 @p451 @p419 @p377 @p325) :args (@t193)) % 0.35/0.67 (step @p476 :rule eq-symm :args (@t49 tptp.e2)) % 0.35/0.67 (step @p477 :rule nary_cong :premises (@p476 @p458 @p429 @p390 @p341) :args (@t195)) % 0.35/0.67 (step @p478 :rule nary_cong :premises (@p476 @p456 @p426 @p386 @p336) :args (@t196)) % 0.35/0.67 (step @p479 :rule eq-symm :args (@t49 tptp.e1)) % 0.35/0.67 (step @p480 :rule nary_cong :premises (@p479 @p463 @p436 @p399 @p352) :args (@t198)) % 0.35/0.67 (step @p481 :rule nary_cong :premises (@p479 @p461 @p433 @p395 @p347) :args (@t199)) % 0.35/0.67 (step @p482 :rule eq-symm :args (@t49 tptp.e0)) % 0.35/0.67 (step @p483 :rule nary_cong :premises (@p482 @p468 @p443 @p408 @p363) :args (@t200)) % 0.35/0.67 (step @p484 :rule nary_cong :premises (@p482 @p466 @p440 @p404 @p358) :args (@t201)) % 0.35/0.67 (step @p485 :rule eq-symm :args (tptp.unit tptp.e4)) % 0.35/0.67 (step @p486 :rule eq-symm :args (tptp.unit tptp.e3)) % 0.35/0.67 (step @p487 :rule eq-symm :args (tptp.unit tptp.e2)) % 0.35/0.67 (step @p488 :rule eq-symm :args (tptp.unit tptp.e1)) % 0.35/0.67 (step @p489 :rule eq-symm :args (tptp.unit tptp.e0)) % 0.35/0.67 (step @p490 :rule nary_cong :premises (@p489 @p488 @p487 @p486 @p485) :args (@t202)) % 0.35/0.67 (step @p491 :rule eq-symm :args (@t203 tptp.e4)) % 0.35/0.67 (step @p492 :rule eq-symm :args (@t204 tptp.e4)) % 0.35/0.67 (step @p493 :rule eq-symm :args (@t205 tptp.e3)) % 0.35/0.67 (step @p494 :rule eq-symm :args (@t206 tptp.e3)) % 0.35/0.67 (step @p495 :rule eq-symm :args (@t207 tptp.e2)) % 0.35/0.67 (step @p496 :rule eq-symm :args (@t208 tptp.e2)) % 0.35/0.67 (step @p497 :rule eq-symm :args (@t209 tptp.e1)) % 0.35/0.67 (step @p498 :rule eq-symm :args (@t210 tptp.e1)) % 0.35/0.67 (step @p499 :rule eq-symm :args (@t211 tptp.e0)) % 0.35/0.67 (step @p500 :rule eq-symm :args (@t212 tptp.e0)) % 0.35/0.67 (step @p501 :rule nary_cong :premises (@p354 @p343 @p332 @p321 @p310) :args (@t213)) % 0.35/0.67 (step @p502 :rule nary_cong :premises (@p360 @p349 @p338 @p327 @p316) :args (@t214)) % 0.35/0.67 (step @p503 :rule nary_cong :premises (@p361 @p350 @p339 @p328 @p317) :args (@t215)) % 0.35/0.67 (step @p504 :rule nary_cong :premises (@p362 @p351 @p340 @p329 @p318) :args (@t216)) % 0.35/0.67 (step @p505 :rule nary_cong :premises (@p363 @p352 @p341 @p330 @p319) :args (@t217)) % 0.35/0.67 (step @p506 :rule nary_cong :premises (@p355 @p344 @p333 @p322 @p311) :args (@t218)) % 0.35/0.67 (step @p507 :rule nary_cong :premises (@p401 @p392 @p383 @p374 @p365) :args (@t219)) % 0.35/0.67 (step @p508 :rule nary_cong :premises (@p406 @p397 @p388 @p379 @p370) :args (@t220)) % 0.35/0.67 (step @p509 :rule nary_cong :premises (@p407 @p398 @p389 @p380 @p371) :args (@t221)) % 0.35/0.67 (step @p510 :rule nary_cong :premises (@p408 @p399 @p390 @p381 @p372) :args (@t222)) % 0.35/0.67 (step @p511 :rule nary_cong :premises (@p356 @p345 @p334 @p323 @p312) :args (@t223)) % 0.35/0.67 (step @p512 :rule nary_cong :premises (@p402 @p393 @p384 @p375 @p366) :args (@t224)) % 0.35/0.67 (step @p513 :rule nary_cong :premises (@p438 @p431 @p424 @p417 @p410) :args (@t225)) % 0.35/0.67 (step @p514 :rule nary_cong :premises (@p442 @p435 @p428 @p421 @p414) :args (@t226)) % 0.35/0.67 (step @p515 :rule nary_cong :premises (@p443 @p436 @p429 @p422 @p415) :args (@t227)) % 0.35/0.67 (step @p516 :rule nary_cong :premises (@p357 @p346 @p335 @p324 @p313) :args (@t228)) % 0.35/0.67 (step @p517 :rule nary_cong :premises (@p403 @p394 @p385 @p376 @p367) :args (@t229)) % 0.35/0.67 (step @p518 :rule nary_cong :premises (@p439 @p432 @p425 @p418 @p411) :args (@t230)) % 0.35/0.67 (step @p519 :rule nary_cong :premises (@p465 @p460 @p455 @p450 @p445) :args (@t231)) % 0.35/0.67 (step @p520 :rule nary_cong :premises (@p468 @p463 @p458 @p453 @p448) :args (@t232)) % 0.35/0.67 (step @p521 :rule nary_cong :premises (@p358 @p347 @p336 @p325 @p314) :args (@t233)) % 0.35/0.67 (step @p522 :rule nary_cong :premises (@p404 @p395 @p386 @p377 @p368) :args (@t234)) % 0.35/0.67 (step @p523 :rule nary_cong :premises (@p440 @p433 @p426 @p419 @p412) :args (@t235)) % 0.35/0.67 (step @p524 :rule nary_cong :premises (@p466 @p461 @p456 @p451 @p446) :args (@t236)) % 0.35/0.67 (step @p525 :rule nary_cong :premises (@p482 @p479 @p476 @p473 @p470) :args (@t237)) % 0.35/0.67 (step @p526 :rule refl :args (@t239)) % 0.35/0.67 (step @p527 :rule nary_cong :premises (@p310 @p526) :args (@t240)) % 0.35/0.67 (step @p528 :rule cong :premises (@p310) :args (@t241)) % 0.35/0.67 (step @p529 :rule nary_cong :premises (@p528 @p527) :args (@t242)) % 0.35/0.67 (step @p530 :rule nary_cong :premises (@p321 @p526) :args (@t243)) % 0.35/0.67 (step @p531 :rule cong :premises (@p316) :args (@t244)) % 0.35/0.67 (step @p532 :rule nary_cong :premises (@p531 @p530) :args (@t245)) % 0.35/0.67 (step @p533 :rule nary_cong :premises (@p332 @p526) :args (@t246)) % 0.35/0.67 (step @p534 :rule cong :premises (@p317) :args (@t247)) % 0.35/0.67 (step @p535 :rule nary_cong :premises (@p534 @p533) :args (@t248)) % 0.35/0.67 (step @p536 :rule nary_cong :premises (@p343 @p526) :args (@t249)) % 0.35/0.67 (step @p537 :rule cong :premises (@p318) :args (@t250)) % 0.35/0.67 (step @p538 :rule nary_cong :premises (@p537 @p536) :args (@t251)) % 0.35/0.67 (step @p539 :rule nary_cong :premises (@p354 @p526) :args (@t252)) % 0.35/0.67 (step @p540 :rule cong :premises (@p319) :args (@t253)) % 0.35/0.67 (step @p541 :rule nary_cong :premises (@p540 @p539) :args (@t254)) % 0.35/0.67 (step @p542 :rule nary_cong :premises (@p311 @p526) :args (@t255)) % 0.35/0.67 (step @p543 :rule cong :premises (@p311) :args (@t256)) % 0.35/0.67 (step @p544 :rule nary_cong :premises (@p543 @p542) :args (@t257)) % 0.35/0.67 (step @p545 :rule nary_cong :premises (@p322 @p526) :args (@t258)) % 0.35/0.67 (step @p546 :rule cong :premises (@p365) :args (@t259)) % 0.35/0.67 (step @p547 :rule nary_cong :premises (@p546 @p545) :args (@t260)) % 0.35/0.67 (step @p548 :rule nary_cong :premises (@p333 @p526) :args (@t261)) % 0.35/0.67 (step @p549 :rule cong :premises (@p370) :args (@t262)) % 0.35/0.67 (step @p550 :rule nary_cong :premises (@p549 @p548) :args (@t263)) % 0.35/0.67 (step @p551 :rule nary_cong :premises (@p344 @p526) :args (@t264)) % 0.35/0.67 (step @p552 :rule cong :premises (@p371) :args (@t265)) % 0.35/0.67 (step @p553 :rule nary_cong :premises (@p552 @p551) :args (@t266)) % 0.35/0.67 (step @p554 :rule nary_cong :premises (@p355 @p526) :args (@t267)) % 0.35/0.67 (step @p555 :rule cong :premises (@p372) :args (@t268)) % 0.35/0.67 (step @p556 :rule nary_cong :premises (@p555 @p554) :args (@t269)) % 0.35/0.67 (step @p557 :rule nary_cong :premises (@p312 @p526) :args (@t270)) % 0.35/0.67 (step @p558 :rule cong :premises (@p312) :args (@t271)) % 0.35/0.67 (step @p559 :rule nary_cong :premises (@p558 @p557) :args (@t272)) % 0.35/0.67 (step @p560 :rule nary_cong :premises (@p323 @p526) :args (@t273)) % 0.35/0.67 (step @p561 :rule cong :premises (@p366) :args (@t274)) % 0.35/0.67 (step @p562 :rule nary_cong :premises (@p561 @p560) :args (@t275)) % 0.35/0.67 (step @p563 :rule nary_cong :premises (@p334 @p526) :args (@t276)) % 0.35/0.67 (step @p564 :rule cong :premises (@p410) :args (@t277)) % 0.35/0.67 (step @p565 :rule nary_cong :premises (@p564 @p563) :args (@t278)) % 0.35/0.67 (step @p566 :rule nary_cong :premises (@p345 @p526) :args (@t279)) % 0.35/0.67 (step @p567 :rule cong :premises (@p414) :args (@t280)) % 0.35/0.67 (step @p568 :rule nary_cong :premises (@p567 @p566) :args (@t281)) % 0.35/0.67 (step @p569 :rule nary_cong :premises (@p356 @p526) :args (@t282)) % 0.35/0.67 (step @p570 :rule cong :premises (@p415) :args (@t283)) % 0.35/0.67 (step @p571 :rule nary_cong :premises (@p570 @p569) :args (@t284)) % 0.35/0.67 (step @p572 :rule nary_cong :premises (@p313 @p526) :args (@t285)) % 0.35/0.67 (step @p573 :rule cong :premises (@p313) :args (@t286)) % 0.35/0.67 (step @p574 :rule nary_cong :premises (@p573 @p572) :args (@t287)) % 0.35/0.67 (step @p575 :rule nary_cong :premises (@p324 @p526) :args (@t288)) % 0.35/0.67 (step @p576 :rule cong :premises (@p367) :args (@t289)) % 0.35/0.67 (step @p577 :rule nary_cong :premises (@p576 @p575) :args (@t290)) % 0.35/0.67 (step @p578 :rule nary_cong :premises (@p335 @p526) :args (@t291)) % 0.35/0.67 (step @p579 :rule cong :premises (@p411) :args (@t292)) % 0.35/0.67 (step @p580 :rule nary_cong :premises (@p579 @p578) :args (@t293)) % 0.35/0.67 (step @p581 :rule nary_cong :premises (@p346 @p526) :args (@t294)) % 0.35/0.67 (step @p582 :rule cong :premises (@p445) :args (@t295)) % 0.35/0.67 (step @p583 :rule nary_cong :premises (@p582 @p581) :args (@t296)) % 0.35/0.67 (step @p584 :rule nary_cong :premises (@p357 @p526) :args (@t297)) % 0.35/0.67 (step @p585 :rule cong :premises (@p448) :args (@t298)) % 0.35/0.67 (step @p586 :rule nary_cong :premises (@p585 @p584) :args (@t299)) % 0.35/0.67 (step @p587 :rule nary_cong :premises (@p314 @p526) :args (@t300)) % 0.35/0.67 (step @p588 :rule cong :premises (@p314) :args (@t301)) % 0.35/0.67 (step @p589 :rule nary_cong :premises (@p588 @p587) :args (@t302)) % 0.35/0.67 (step @p590 :rule nary_cong :premises (@p325 @p526) :args (@t303)) % 0.35/0.67 (step @p591 :rule cong :premises (@p368) :args (@t304)) % 0.35/0.67 (step @p592 :rule nary_cong :premises (@p591 @p590) :args (@t305)) % 0.35/0.67 (step @p593 :rule nary_cong :premises (@p336 @p526) :args (@t306)) % 0.35/0.67 (step @p594 :rule cong :premises (@p412) :args (@t307)) % 0.35/0.67 (step @p595 :rule nary_cong :premises (@p594 @p593) :args (@t308)) % 0.35/0.67 (step @p596 :rule nary_cong :premises (@p347 @p526) :args (@t309)) % 0.35/0.67 (step @p597 :rule cong :premises (@p446) :args (@t310)) % 0.35/0.67 (step @p598 :rule nary_cong :premises (@p597 @p596) :args (@t311)) % 0.35/0.67 (step @p599 :rule nary_cong :premises (@p358 @p526) :args (@t312)) % 0.35/0.67 (step @p600 :rule cong :premises (@p470) :args (@t313)) % 0.35/0.67 (step @p601 :rule nary_cong :premises (@p600 @p599) :args (@t314)) % 0.35/0.67 (step @p602 :rule nary_cong :premises (@p601 @p598 @p595 @p592 @p589 @p586 @p583 @p580 @p577 @p574 @p571 @p568 @p565 @p562 @p559 @p556 @p553 @p550 @p547 @p544 @p541 @p538 @p535 @p532 @p529) :args (@t315)) % 0.35/0.67 (step @p603 :rule refl :args (@t317)) % 0.35/0.67 (step @p604 :rule nary_cong :premises (@p316 @p603) :args (@t318)) % 0.35/0.67 (step @p605 :rule cong :premises (@p321) :args (@t319)) % 0.35/0.67 (step @p606 :rule nary_cong :premises (@p605 @p604) :args (@t320)) % 0.35/0.67 (step @p607 :rule nary_cong :premises (@p327 @p603) :args (@t321)) % 0.35/0.67 (step @p608 :rule cong :premises (@p327) :args (@t322)) % 0.35/0.67 (step @p609 :rule nary_cong :premises (@p608 @p607) :args (@t323)) % 0.35/0.67 (step @p610 :rule nary_cong :premises (@p338 @p603) :args (@t324)) % 0.35/0.67 (step @p611 :rule cong :premises (@p328) :args (@t325)) % 0.35/0.67 (step @p612 :rule nary_cong :premises (@p611 @p610) :args (@t326)) % 0.35/0.67 (step @p613 :rule nary_cong :premises (@p349 @p603) :args (@t327)) % 0.35/0.67 (step @p614 :rule cong :premises (@p329) :args (@t328)) % 0.35/0.67 (step @p615 :rule nary_cong :premises (@p614 @p613) :args (@t329)) % 0.35/0.67 (step @p616 :rule nary_cong :premises (@p360 @p603) :args (@t330)) % 0.35/0.67 (step @p617 :rule cong :premises (@p330) :args (@t331)) % 0.35/0.67 (step @p618 :rule nary_cong :premises (@p617 @p616) :args (@t332)) % 0.35/0.67 (step @p619 :rule nary_cong :premises (@p365 @p603) :args (@t333)) % 0.35/0.67 (step @p620 :rule cong :premises (@p322) :args (@t334)) % 0.35/0.67 (step @p621 :rule nary_cong :premises (@p620 @p619) :args (@t335)) % 0.35/0.67 (step @p622 :rule nary_cong :premises (@p374 @p603) :args (@t336)) % 0.35/0.67 (step @p623 :rule cong :premises (@p374) :args (@t337)) % 0.35/0.67 (step @p624 :rule nary_cong :premises (@p623 @p622) :args (@t338)) % 0.35/0.67 (step @p625 :rule nary_cong :premises (@p383 @p603) :args (@t339)) % 0.35/0.67 (step @p626 :rule cong :premises (@p379) :args (@t340)) % 0.35/0.67 (step @p627 :rule nary_cong :premises (@p626 @p625) :args (@t341)) % 0.35/0.67 (step @p628 :rule nary_cong :premises (@p392 @p603) :args (@t342)) % 0.35/0.67 (step @p629 :rule cong :premises (@p380) :args (@t343)) % 0.35/0.67 (step @p630 :rule nary_cong :premises (@p629 @p628) :args (@t344)) % 0.35/0.67 (step @p631 :rule nary_cong :premises (@p401 @p603) :args (@t345)) % 0.35/0.67 (step @p632 :rule cong :premises (@p381) :args (@t346)) % 0.35/0.67 (step @p633 :rule nary_cong :premises (@p632 @p631) :args (@t347)) % 0.35/0.67 (step @p634 :rule nary_cong :premises (@p366 @p603) :args (@t348)) % 0.35/0.67 (step @p635 :rule cong :premises (@p323) :args (@t349)) % 0.35/0.67 (step @p636 :rule nary_cong :premises (@p635 @p634) :args (@t350)) % 0.35/0.67 (step @p637 :rule nary_cong :premises (@p375 @p603) :args (@t351)) % 0.35/0.67 (step @p638 :rule cong :premises (@p375) :args (@t352)) % 0.35/0.67 (step @p639 :rule nary_cong :premises (@p638 @p637) :args (@t353)) % 0.35/0.67 (step @p640 :rule nary_cong :premises (@p384 @p603) :args (@t354)) % 0.35/0.67 (step @p641 :rule cong :premises (@p417) :args (@t355)) % 0.35/0.67 (step @p642 :rule nary_cong :premises (@p641 @p640) :args (@t356)) % 0.35/0.67 (step @p643 :rule nary_cong :premises (@p393 @p603) :args (@t357)) % 0.35/0.67 (step @p644 :rule cong :premises (@p421) :args (@t358)) % 0.35/0.67 (step @p645 :rule nary_cong :premises (@p644 @p643) :args (@t359)) % 0.35/0.67 (step @p646 :rule nary_cong :premises (@p402 @p603) :args (@t360)) % 0.35/0.67 (step @p647 :rule cong :premises (@p422) :args (@t361)) % 0.35/0.67 (step @p648 :rule nary_cong :premises (@p647 @p646) :args (@t362)) % 0.35/0.67 (step @p649 :rule nary_cong :premises (@p367 @p603) :args (@t363)) % 0.35/0.67 (step @p650 :rule cong :premises (@p324) :args (@t364)) % 0.35/0.67 (step @p651 :rule nary_cong :premises (@p650 @p649) :args (@t365)) % 0.35/0.67 (step @p652 :rule nary_cong :premises (@p376 @p603) :args (@t366)) % 0.35/0.67 (step @p653 :rule cong :premises (@p376) :args (@t367)) % 0.35/0.67 (step @p654 :rule nary_cong :premises (@p653 @p652) :args (@t368)) % 0.35/0.67 (step @p655 :rule nary_cong :premises (@p385 @p603) :args (@t369)) % 0.35/0.67 (step @p656 :rule cong :premises (@p418) :args (@t370)) % 0.35/0.67 (step @p657 :rule nary_cong :premises (@p656 @p655) :args (@t371)) % 0.35/0.67 (step @p658 :rule nary_cong :premises (@p394 @p603) :args (@t372)) % 0.35/0.67 (step @p659 :rule cong :premises (@p450) :args (@t373)) % 0.35/0.67 (step @p660 :rule nary_cong :premises (@p659 @p658) :args (@t374)) % 0.35/0.67 (step @p661 :rule nary_cong :premises (@p403 @p603) :args (@t375)) % 0.35/0.67 (step @p662 :rule cong :premises (@p453) :args (@t376)) % 0.35/0.67 (step @p663 :rule nary_cong :premises (@p662 @p661) :args (@t377)) % 0.35/0.67 (step @p664 :rule nary_cong :premises (@p368 @p603) :args (@t378)) % 0.35/0.67 (step @p665 :rule cong :premises (@p325) :args (@t379)) % 0.35/0.67 (step @p666 :rule nary_cong :premises (@p665 @p664) :args (@t380)) % 0.35/0.67 (step @p667 :rule nary_cong :premises (@p377 @p603) :args (@t381)) % 0.35/0.67 (step @p668 :rule cong :premises (@p377) :args (@t382)) % 0.35/0.67 (step @p669 :rule nary_cong :premises (@p668 @p667) :args (@t383)) % 0.35/0.67 (step @p670 :rule nary_cong :premises (@p386 @p603) :args (@t384)) % 0.35/0.67 (step @p671 :rule cong :premises (@p419) :args (@t385)) % 0.35/0.67 (step @p672 :rule nary_cong :premises (@p671 @p670) :args (@t386)) % 0.35/0.67 (step @p673 :rule nary_cong :premises (@p395 @p603) :args (@t387)) % 0.35/0.67 (step @p674 :rule cong :premises (@p451) :args (@t388)) % 0.35/0.67 (step @p675 :rule nary_cong :premises (@p674 @p673) :args (@t389)) % 0.35/0.67 (step @p676 :rule nary_cong :premises (@p404 @p603) :args (@t390)) % 0.35/0.67 (step @p677 :rule cong :premises (@p473) :args (@t391)) % 0.35/0.67 (step @p678 :rule nary_cong :premises (@p677 @p676) :args (@t392)) % 0.35/0.67 (step @p679 :rule nary_cong :premises (@p678 @p675 @p672 @p669 @p666 @p663 @p660 @p657 @p654 @p651 @p648 @p645 @p642 @p639 @p636 @p633 @p630 @p627 @p624 @p621 @p618 @p615 @p612 @p609 @p606) :args (@t393)) % 0.35/0.67 (step @p680 :rule refl :args (@t395)) % 0.35/0.67 (step @p681 :rule nary_cong :premises (@p317 @p680) :args (@t396)) % 0.35/0.67 (step @p682 :rule cong :premises (@p332) :args (@t397)) % 0.35/0.67 (step @p683 :rule nary_cong :premises (@p682 @p681) :args (@t398)) % 0.35/0.67 (step @p684 :rule nary_cong :premises (@p328 @p680) :args (@t399)) % 0.35/0.67 (step @p685 :rule cong :premises (@p338) :args (@t400)) % 0.35/0.67 (step @p686 :rule nary_cong :premises (@p685 @p684) :args (@t401)) % 0.35/0.67 (step @p687 :rule nary_cong :premises (@p339 @p680) :args (@t402)) % 0.35/0.67 (step @p688 :rule cong :premises (@p339) :args (@t403)) % 0.35/0.67 (step @p689 :rule nary_cong :premises (@p688 @p687) :args (@t404)) % 0.35/0.67 (step @p690 :rule nary_cong :premises (@p350 @p680) :args (@t405)) % 0.35/0.67 (step @p691 :rule cong :premises (@p340) :args (@t406)) % 0.35/0.67 (step @p692 :rule nary_cong :premises (@p691 @p690) :args (@t407)) % 0.35/0.67 (step @p693 :rule nary_cong :premises (@p361 @p680) :args (@t408)) % 0.35/0.67 (step @p694 :rule cong :premises (@p341) :args (@t409)) % 0.35/0.67 (step @p695 :rule nary_cong :premises (@p694 @p693) :args (@t410)) % 0.35/0.67 (step @p696 :rule nary_cong :premises (@p370 @p680) :args (@t411)) % 0.35/0.67 (step @p697 :rule cong :premises (@p333) :args (@t412)) % 0.35/0.67 (step @p698 :rule nary_cong :premises (@p697 @p696) :args (@t413)) % 0.35/0.67 (step @p699 :rule nary_cong :premises (@p379 @p680) :args (@t414)) % 0.35/0.67 (step @p700 :rule cong :premises (@p383) :args (@t415)) % 0.35/0.67 (step @p701 :rule nary_cong :premises (@p700 @p699) :args (@t416)) % 0.35/0.67 (step @p702 :rule nary_cong :premises (@p388 @p680) :args (@t417)) % 0.35/0.67 (step @p703 :rule cong :premises (@p388) :args (@t418)) % 0.35/0.67 (step @p704 :rule nary_cong :premises (@p703 @p702) :args (@t419)) % 0.35/0.67 (step @p705 :rule nary_cong :premises (@p397 @p680) :args (@t420)) % 0.35/0.67 (step @p706 :rule cong :premises (@p389) :args (@t421)) % 0.35/0.67 (step @p707 :rule nary_cong :premises (@p706 @p705) :args (@t422)) % 0.35/0.67 (step @p708 :rule nary_cong :premises (@p406 @p680) :args (@t423)) % 0.35/0.67 (step @p709 :rule cong :premises (@p390) :args (@t424)) % 0.35/0.67 (step @p710 :rule nary_cong :premises (@p709 @p708) :args (@t425)) % 0.35/0.67 (step @p711 :rule nary_cong :premises (@p410 @p680) :args (@t426)) % 0.35/0.67 (step @p712 :rule cong :premises (@p334) :args (@t427)) % 0.35/0.67 (step @p713 :rule nary_cong :premises (@p712 @p711) :args (@t428)) % 0.35/0.67 (step @p714 :rule nary_cong :premises (@p417 @p680) :args (@t429)) % 0.35/0.67 (step @p715 :rule cong :premises (@p384) :args (@t430)) % 0.35/0.67 (step @p716 :rule nary_cong :premises (@p715 @p714) :args (@t431)) % 0.35/0.67 (step @p717 :rule nary_cong :premises (@p424 @p680) :args (@t432)) % 0.35/0.67 (step @p718 :rule cong :premises (@p424) :args (@t433)) % 0.35/0.67 (step @p719 :rule nary_cong :premises (@p718 @p717) :args (@t434)) % 0.35/0.67 (step @p720 :rule nary_cong :premises (@p431 @p680) :args (@t435)) % 0.35/0.67 (step @p721 :rule cong :premises (@p428) :args (@t436)) % 0.35/0.67 (step @p722 :rule nary_cong :premises (@p721 @p720) :args (@t437)) % 0.35/0.67 (step @p723 :rule nary_cong :premises (@p438 @p680) :args (@t438)) % 0.35/0.67 (step @p724 :rule cong :premises (@p429) :args (@t439)) % 0.35/0.67 (step @p725 :rule nary_cong :premises (@p724 @p723) :args (@t440)) % 0.35/0.67 (step @p726 :rule nary_cong :premises (@p411 @p680) :args (@t441)) % 0.35/0.67 (step @p727 :rule cong :premises (@p335) :args (@t442)) % 0.35/0.67 (step @p728 :rule nary_cong :premises (@p727 @p726) :args (@t443)) % 0.35/0.67 (step @p729 :rule nary_cong :premises (@p418 @p680) :args (@t444)) % 0.35/0.67 (step @p730 :rule cong :premises (@p385) :args (@t445)) % 0.35/0.67 (step @p731 :rule nary_cong :premises (@p730 @p729) :args (@t446)) % 0.35/0.67 (step @p732 :rule nary_cong :premises (@p425 @p680) :args (@t447)) % 0.35/0.67 (step @p733 :rule cong :premises (@p425) :args (@t448)) % 0.35/0.67 (step @p734 :rule nary_cong :premises (@p733 @p732) :args (@t449)) % 0.35/0.67 (step @p735 :rule nary_cong :premises (@p432 @p680) :args (@t450)) % 0.35/0.67 (step @p736 :rule cong :premises (@p455) :args (@t451)) % 0.35/0.67 (step @p737 :rule nary_cong :premises (@p736 @p735) :args (@t452)) % 0.35/0.67 (step @p738 :rule nary_cong :premises (@p439 @p680) :args (@t453)) % 0.35/0.67 (step @p739 :rule cong :premises (@p458) :args (@t454)) % 0.35/0.67 (step @p740 :rule nary_cong :premises (@p739 @p738) :args (@t455)) % 0.35/0.67 (step @p741 :rule nary_cong :premises (@p412 @p680) :args (@t456)) % 0.35/0.67 (step @p742 :rule cong :premises (@p336) :args (@t457)) % 0.35/0.67 (step @p743 :rule nary_cong :premises (@p742 @p741) :args (@t458)) % 0.35/0.67 (step @p744 :rule nary_cong :premises (@p419 @p680) :args (@t459)) % 0.35/0.67 (step @p745 :rule cong :premises (@p386) :args (@t460)) % 0.35/0.67 (step @p746 :rule nary_cong :premises (@p745 @p744) :args (@t461)) % 0.35/0.67 (step @p747 :rule nary_cong :premises (@p426 @p680) :args (@t462)) % 0.35/0.67 (step @p748 :rule cong :premises (@p426) :args (@t463)) % 0.35/0.67 (step @p749 :rule nary_cong :premises (@p748 @p747) :args (@t464)) % 0.35/0.67 (step @p750 :rule nary_cong :premises (@p433 @p680) :args (@t465)) % 0.35/0.67 (step @p751 :rule cong :premises (@p456) :args (@t466)) % 0.35/0.67 (step @p752 :rule nary_cong :premises (@p751 @p750) :args (@t467)) % 0.35/0.67 (step @p753 :rule nary_cong :premises (@p440 @p680) :args (@t468)) % 0.35/0.67 (step @p754 :rule cong :premises (@p476) :args (@t469)) % 0.35/0.67 (step @p755 :rule nary_cong :premises (@p754 @p753) :args (@t470)) % 0.35/0.67 (step @p756 :rule nary_cong :premises (@p755 @p752 @p749 @p746 @p743 @p740 @p737 @p734 @p731 @p728 @p725 @p722 @p719 @p716 @p713 @p710 @p707 @p704 @p701 @p698 @p695 @p692 @p689 @p686 @p683) :args (@t471)) % 0.35/0.67 (step @p757 :rule refl :args (@t473)) % 0.35/0.67 (step @p758 :rule nary_cong :premises (@p318 @p757) :args (@t474)) % 0.35/0.67 (step @p759 :rule cong :premises (@p343) :args (@t475)) % 0.35/0.67 (step @p760 :rule nary_cong :premises (@p759 @p758) :args (@t476)) % 0.35/0.67 (step @p761 :rule nary_cong :premises (@p329 @p757) :args (@t477)) % 0.35/0.67 (step @p762 :rule cong :premises (@p349) :args (@t478)) % 0.35/0.67 (step @p763 :rule nary_cong :premises (@p762 @p761) :args (@t479)) % 0.35/0.67 (step @p764 :rule nary_cong :premises (@p340 @p757) :args (@t480)) % 0.35/0.67 (step @p765 :rule cong :premises (@p350) :args (@t481)) % 0.35/0.67 (step @p766 :rule nary_cong :premises (@p765 @p764) :args (@t482)) % 0.35/0.67 (step @p767 :rule nary_cong :premises (@p351 @p757) :args (@t483)) % 0.35/0.67 (step @p768 :rule cong :premises (@p351) :args (@t484)) % 0.35/0.67 (step @p769 :rule nary_cong :premises (@p768 @p767) :args (@t485)) % 0.35/0.67 (step @p770 :rule nary_cong :premises (@p362 @p757) :args (@t486)) % 0.35/0.67 (step @p771 :rule cong :premises (@p352) :args (@t487)) % 0.35/0.67 (step @p772 :rule nary_cong :premises (@p771 @p770) :args (@t488)) % 0.35/0.67 (step @p773 :rule nary_cong :premises (@p371 @p757) :args (@t489)) % 0.35/0.67 (step @p774 :rule cong :premises (@p344) :args (@t490)) % 0.35/0.67 (step @p775 :rule nary_cong :premises (@p774 @p773) :args (@t491)) % 0.35/0.67 (step @p776 :rule nary_cong :premises (@p380 @p757) :args (@t492)) % 0.35/0.67 (step @p777 :rule cong :premises (@p392) :args (@t493)) % 0.35/0.67 (step @p778 :rule nary_cong :premises (@p777 @p776) :args (@t494)) % 0.35/0.67 (step @p779 :rule nary_cong :premises (@p389 @p757) :args (@t495)) % 0.35/0.67 (step @p780 :rule cong :premises (@p397) :args (@t496)) % 0.35/0.67 (step @p781 :rule nary_cong :premises (@p780 @p779) :args (@t497)) % 0.35/0.67 (step @p782 :rule nary_cong :premises (@p398 @p757) :args (@t498)) % 0.35/0.67 (step @p783 :rule cong :premises (@p398) :args (@t499)) % 0.35/0.67 (step @p784 :rule nary_cong :premises (@p783 @p782) :args (@t500)) % 0.35/0.67 (step @p785 :rule nary_cong :premises (@p407 @p757) :args (@t501)) % 0.35/0.67 (step @p786 :rule cong :premises (@p399) :args (@t502)) % 0.35/0.67 (step @p787 :rule nary_cong :premises (@p786 @p785) :args (@t503)) % 0.35/0.67 (step @p788 :rule nary_cong :premises (@p414 @p757) :args (@t504)) % 0.35/0.67 (step @p789 :rule cong :premises (@p345) :args (@t505)) % 0.35/0.67 (step @p790 :rule nary_cong :premises (@p789 @p788) :args (@t506)) % 0.35/0.67 (step @p791 :rule nary_cong :premises (@p421 @p757) :args (@t507)) % 0.35/0.67 (step @p792 :rule cong :premises (@p393) :args (@t508)) % 0.35/0.67 (step @p793 :rule nary_cong :premises (@p792 @p791) :args (@t509)) % 0.35/0.67 (step @p794 :rule nary_cong :premises (@p428 @p757) :args (@t510)) % 0.35/0.67 (step @p795 :rule cong :premises (@p431) :args (@t511)) % 0.35/0.67 (step @p796 :rule nary_cong :premises (@p795 @p794) :args (@t512)) % 0.35/0.67 (step @p797 :rule nary_cong :premises (@p435 @p757) :args (@t513)) % 0.35/0.67 (step @p798 :rule cong :premises (@p435) :args (@t514)) % 0.35/0.67 (step @p799 :rule nary_cong :premises (@p798 @p797) :args (@t515)) % 0.35/0.67 (step @p800 :rule nary_cong :premises (@p442 @p757) :args (@t516)) % 0.35/0.67 (step @p801 :rule cong :premises (@p436) :args (@t517)) % 0.35/0.67 (step @p802 :rule nary_cong :premises (@p801 @p800) :args (@t518)) % 0.35/0.67 (step @p803 :rule nary_cong :premises (@p445 @p757) :args (@t519)) % 0.35/0.67 (step @p804 :rule cong :premises (@p346) :args (@t520)) % 0.35/0.67 (step @p805 :rule nary_cong :premises (@p804 @p803) :args (@t521)) % 0.35/0.67 (step @p806 :rule nary_cong :premises (@p450 @p757) :args (@t522)) % 0.35/0.67 (step @p807 :rule cong :premises (@p394) :args (@t523)) % 0.35/0.67 (step @p808 :rule nary_cong :premises (@p807 @p806) :args (@t524)) % 0.35/0.67 (step @p809 :rule nary_cong :premises (@p455 @p757) :args (@t525)) % 0.35/0.67 (step @p810 :rule cong :premises (@p432) :args (@t526)) % 0.35/0.67 (step @p811 :rule nary_cong :premises (@p810 @p809) :args (@t527)) % 0.35/0.67 (step @p812 :rule nary_cong :premises (@p460 @p757) :args (@t528)) % 0.35/0.67 (step @p813 :rule cong :premises (@p460) :args (@t529)) % 0.35/0.67 (step @p814 :rule nary_cong :premises (@p813 @p812) :args (@t530)) % 0.35/0.67 (step @p815 :rule nary_cong :premises (@p465 @p757) :args (@t531)) % 0.35/0.67 (step @p816 :rule cong :premises (@p463) :args (@t532)) % 0.35/0.67 (step @p817 :rule nary_cong :premises (@p816 @p815) :args (@t533)) % 0.35/0.67 (step @p818 :rule nary_cong :premises (@p446 @p757) :args (@t534)) % 0.35/0.67 (step @p819 :rule cong :premises (@p347) :args (@t535)) % 0.35/0.67 (step @p820 :rule nary_cong :premises (@p819 @p818) :args (@t536)) % 0.35/0.67 (step @p821 :rule nary_cong :premises (@p451 @p757) :args (@t537)) % 0.35/0.68 (step @p822 :rule cong :premises (@p395) :args (@t538)) % 0.35/0.68 (step @p823 :rule nary_cong :premises (@p822 @p821) :args (@t539)) % 0.35/0.68 (step @p824 :rule nary_cong :premises (@p456 @p757) :args (@t540)) % 0.35/0.68 (step @p825 :rule cong :premises (@p433) :args (@t541)) % 0.35/0.68 (step @p826 :rule nary_cong :premises (@p825 @p824) :args (@t542)) % 0.35/0.68 (step @p827 :rule nary_cong :premises (@p461 @p757) :args (@t543)) % 0.35/0.68 (step @p828 :rule cong :premises (@p461) :args (@t544)) % 0.35/0.68 (step @p829 :rule nary_cong :premises (@p828 @p827) :args (@t545)) % 0.35/0.68 (step @p830 :rule nary_cong :premises (@p466 @p757) :args (@t546)) % 0.35/0.68 (step @p831 :rule cong :premises (@p479) :args (@t547)) % 0.35/0.68 (step @p832 :rule nary_cong :premises (@p831 @p830) :args (@t548)) % 0.35/0.68 (step @p833 :rule nary_cong :premises (@p832 @p829 @p826 @p823 @p820 @p817 @p814 @p811 @p808 @p805 @p802 @p799 @p796 @p793 @p790 @p787 @p784 @p781 @p778 @p775 @p772 @p769 @p766 @p763 @p760) :args (@t549)) % 0.35/0.68 (step @p834 :rule refl :args (@t551)) % 0.35/0.68 (step @p835 :rule nary_cong :premises (@p319 @p834) :args (@t552)) % 0.35/0.68 (step @p836 :rule cong :premises (@p354) :args (@t553)) % 0.35/0.68 (step @p837 :rule nary_cong :premises (@p836 @p835) :args (@t554)) % 0.35/0.68 (step @p838 :rule nary_cong :premises (@p330 @p834) :args (@t555)) % 0.35/0.68 (step @p839 :rule cong :premises (@p360) :args (@t556)) % 0.35/0.68 (step @p840 :rule nary_cong :premises (@p839 @p838) :args (@t557)) % 0.35/0.68 (step @p841 :rule nary_cong :premises (@p341 @p834) :args (@t558)) % 0.35/0.68 (step @p842 :rule cong :premises (@p361) :args (@t559)) % 0.35/0.68 (step @p843 :rule nary_cong :premises (@p842 @p841) :args (@t560)) % 0.35/0.68 (step @p844 :rule nary_cong :premises (@p352 @p834) :args (@t561)) % 0.35/0.68 (step @p845 :rule cong :premises (@p362) :args (@t562)) % 0.35/0.68 (step @p846 :rule nary_cong :premises (@p845 @p844) :args (@t563)) % 0.35/0.68 (step @p847 :rule nary_cong :premises (@p363 @p834) :args (@t564)) % 0.35/0.68 (step @p848 :rule cong :premises (@p363) :args (@t565)) % 0.35/0.68 (step @p849 :rule nary_cong :premises (@p848 @p847) :args (@t566)) % 0.35/0.68 (step @p850 :rule nary_cong :premises (@p372 @p834) :args (@t567)) % 0.35/0.68 (step @p851 :rule cong :premises (@p355) :args (@t568)) % 0.35/0.68 (step @p852 :rule nary_cong :premises (@p851 @p850) :args (@t569)) % 0.35/0.68 (step @p853 :rule nary_cong :premises (@p381 @p834) :args (@t570)) % 0.35/0.68 (step @p854 :rule cong :premises (@p401) :args (@t571)) % 0.35/0.68 (step @p855 :rule nary_cong :premises (@p854 @p853) :args (@t572)) % 0.35/0.68 (step @p856 :rule nary_cong :premises (@p390 @p834) :args (@t573)) % 0.35/0.68 (step @p857 :rule cong :premises (@p406) :args (@t574)) % 0.35/0.68 (step @p858 :rule nary_cong :premises (@p857 @p856) :args (@t575)) % 0.35/0.68 (step @p859 :rule nary_cong :premises (@p399 @p834) :args (@t576)) % 0.35/0.68 (step @p860 :rule cong :premises (@p407) :args (@t577)) % 0.35/0.68 (step @p861 :rule nary_cong :premises (@p860 @p859) :args (@t578)) % 0.35/0.68 (step @p862 :rule nary_cong :premises (@p408 @p834) :args (@t579)) % 0.35/0.68 (step @p863 :rule cong :premises (@p408) :args (@t580)) % 0.35/0.68 (step @p864 :rule nary_cong :premises (@p863 @p862) :args (@t581)) % 0.35/0.68 (step @p865 :rule nary_cong :premises (@p415 @p834) :args (@t582)) % 0.35/0.68 (step @p866 :rule cong :premises (@p356) :args (@t583)) % 0.35/0.68 (step @p867 :rule nary_cong :premises (@p866 @p865) :args (@t584)) % 0.35/0.68 (step @p868 :rule nary_cong :premises (@p422 @p834) :args (@t585)) % 0.35/0.68 (step @p869 :rule cong :premises (@p402) :args (@t586)) % 0.35/0.68 (step @p870 :rule nary_cong :premises (@p869 @p868) :args (@t587)) % 0.35/0.68 (step @p871 :rule nary_cong :premises (@p429 @p834) :args (@t588)) % 0.35/0.68 (step @p872 :rule cong :premises (@p438) :args (@t589)) % 0.35/0.68 (step @p873 :rule nary_cong :premises (@p872 @p871) :args (@t590)) % 0.35/0.68 (step @p874 :rule nary_cong :premises (@p436 @p834) :args (@t591)) % 0.35/0.68 (step @p875 :rule cong :premises (@p442) :args (@t592)) % 0.35/0.68 (step @p876 :rule nary_cong :premises (@p875 @p874) :args (@t593)) % 0.35/0.68 (step @p877 :rule nary_cong :premises (@p443 @p834) :args (@t594)) % 0.35/0.68 (step @p878 :rule cong :premises (@p443) :args (@t595)) % 0.35/0.68 (step @p879 :rule nary_cong :premises (@p878 @p877) :args (@t596)) % 0.35/0.68 (step @p880 :rule nary_cong :premises (@p448 @p834) :args (@t597)) % 0.35/0.68 (step @p881 :rule cong :premises (@p357) :args (@t598)) % 0.35/0.68 (step @p882 :rule nary_cong :premises (@p881 @p880) :args (@t599)) % 0.35/0.68 (step @p883 :rule nary_cong :premises (@p453 @p834) :args (@t600)) % 0.35/0.68 (step @p884 :rule cong :premises (@p403) :args (@t601)) % 0.35/0.68 (step @p885 :rule nary_cong :premises (@p884 @p883) :args (@t602)) % 0.35/0.68 (step @p886 :rule nary_cong :premises (@p458 @p834) :args (@t603)) % 0.35/0.68 (step @p887 :rule cong :premises (@p439) :args (@t604)) % 0.35/0.68 (step @p888 :rule nary_cong :premises (@p887 @p886) :args (@t605)) % 0.35/0.68 (step @p889 :rule nary_cong :premises (@p463 @p834) :args (@t606)) % 0.35/0.68 (step @p890 :rule cong :premises (@p465) :args (@t607)) % 0.35/0.68 (step @p891 :rule nary_cong :premises (@p890 @p889) :args (@t608)) % 0.35/0.68 (step @p892 :rule nary_cong :premises (@p468 @p834) :args (@t609)) % 0.35/0.68 (step @p893 :rule cong :premises (@p468) :args (@t610)) % 0.35/0.68 (step @p894 :rule nary_cong :premises (@p893 @p892) :args (@t611)) % 0.35/0.68 (step @p895 :rule nary_cong :premises (@p470 @p834) :args (@t612)) % 0.35/0.68 (step @p896 :rule cong :premises (@p358) :args (@t613)) % 0.35/0.68 (step @p897 :rule nary_cong :premises (@p896 @p895) :args (@t614)) % 0.35/0.68 (step @p898 :rule nary_cong :premises (@p473 @p834) :args (@t615)) % 0.35/0.68 (step @p899 :rule cong :premises (@p404) :args (@t616)) % 0.35/0.68 (step @p900 :rule nary_cong :premises (@p899 @p898) :args (@t617)) % 0.35/0.68 (step @p901 :rule nary_cong :premises (@p476 @p834) :args (@t618)) % 0.35/0.68 (step @p902 :rule cong :premises (@p440) :args (@t619)) % 0.35/0.68 (step @p903 :rule nary_cong :premises (@p902 @p901) :args (@t620)) % 0.35/0.68 (step @p904 :rule nary_cong :premises (@p479 @p834) :args (@t621)) % 0.35/0.68 (step @p905 :rule cong :premises (@p466) :args (@t622)) % 0.35/0.68 (step @p906 :rule nary_cong :premises (@p905 @p904) :args (@t623)) % 0.35/0.68 (step @p907 :rule nary_cong :premises (@p482 @p834) :args (@t624)) % 0.35/0.68 (step @p908 :rule cong :premises (@p482) :args (@t625)) % 0.35/0.68 (step @p909 :rule nary_cong :premises (@p908 @p907) :args (@t626)) % 0.35/0.68 (step @p910 :rule nary_cong :premises (@p909 @p906 @p903 @p900 @p897 @p894 @p891 @p888 @p885 @p882 @p879 @p876 @p873 @p870 @p867 @p864 @p861 @p858 @p855 @p852 @p849 @p846 @p843 @p840 @p837) :args (@t627)) % 0.35/0.68 (step @p911 :rule nary_cong :premises (@p910 @p833 @p756 @p679 @p602) :args (@t628)) % 0.35/0.68 (step @p912 :rule nary_cong :premises (@p911 @p525 @p524 @p523 @p522 @p521 @p520 @p519 @p518 @p517 @p516 @p515 @p514 @p513 @p512 @p511 @p510 @p509 @p508 @p507 @p506 @p505 @p504 @p503 @p502 @p501 @p500 @p499 @p498 @p497 @p496 @p495 @p494 @p493 @p492 @p491 @p490 @p484 @p483 @p481 @p480 @p478 @p477 @p475 @p474 @p472 @p471 @p469 @p467 @p464 @p462 @p459 @p457 @p454 @p452 @p449 @p447 @p444 @p441 @p437 @p434 @p430 @p427 @p423 @p420 @p416 @p413 @p409 @p405 @p400 @p396 @p391 @p387 @p382 @p378 @p373 @p369 @p364 @p359 @p353 @p348 @p342 @p337 @p331 @p326 @p320 @p315) :args (@t629)) % 0.35/0.68 (step @p913 :rule cong :premises (@p912) :args (@t630)) % 0.35/0.68 (step @p914 :rule eq_resolve :premises (@p4 @p913)) % 0.35/0.68 (step @p915 :rule not_and :premises (@p914)) % 0.35/0.68 (step @p916 :rule chain_m_resolution :premises (@p915 @p309 @p306 @p303 @p300 @p297 @p294 @p291 @p288 @p285 @p282 @p279 @p276 @p273 @p270 @p267 @p264 @p261 @p258 @p255 @p252 @p249 @p246 @p243 @p240 @p237 @p234 @p232 @p229 @p227 @p224 @p222 @p219 @p217 @p214 @p212 @p209 @p205 @p202 @p197 @p194 @p191 @p188 @p185 @p182 @p179 @p176 @p173 @p170 @p165 @p160 @p155 @p152 @p149 @p146 @p143 @p140 @p137 @p134 @p131 @p128 @p125 @p120 @p115 @p112 @p107 @p102 @p97 @p94 @p89 @p84 @p81 @p76 @p71 @p66 @p61 @p58 @p53 @p48 @p43 @p38 @p33 @p30 @p25 @p20 @p15 @p10) :args ((not @t934) (@list false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false) (@list @t882 @t881 @t880 @t879 @t878 @t877 @t876 @t875 @t874 @t873 @t872 @t871 @t870 @t869 @t868 @t867 @t866 @t865 @t864 @t863 @t862 @t861 @t860 @t859 @t858 (= tptp.e0 @t212) (= tptp.e0 @t211) (= tptp.e1 @t210) (= tptp.e1 @t209) (= tptp.e2 @t208) (= tptp.e2 @t207) (= tptp.e3 @t206) (= tptp.e3 @t205) (= tptp.e4 @t204) (= tptp.e4 @t203) @t857 @t856 @t853 @t851 @t850 @t848 @t847 @t845 @t844 @t842 @t841 @t839 @t835 @t830 @t826 @t823 @t821 @t818 @t816 @t813 @t811 @t808 @t805 @t801 @t798 @t792 @t787 @t783 @t778 @t772 @t767 @t763 @t757 @t750 @t746 @t739 @t733 @t726 @t720 @t715 @t709 @t702 @t695 @t687 @t680 @t674 @t667 @t659 @t652 @t644 @t636))) % 0.35/0.68 (step @p917 :rule cnf_or_neg :args (@t934 1)) % 0.35/0.68 (step @p918 :rule chain_m_resolution :premises (@p917 @p916) :args ((not @t933) @t935 (@list @t934))) % 0.35/0.68 (step @p919 :rule and_elim :premises (@p1) :args (4)) % 0.35/0.68 (step @p920 :rule false_intro :premises (@p919)) % 0.35/0.68 (step @p921 :rule cong :premises (@p225 @p26) :args (@t675)) % 0.35/0.68 (step @p922 :rule trans :premises (@p921 @p920)) % 0.35/0.68 (step @p923 :rule false_elim :premises (@p922)) % 0.35/0.68 (step @p924 :rule bool-double-not-elim :args (@t675)) % 0.35/0.68 (step @p925 :rule refl :args (@t884)) % 0.35/0.68 (step @p926 :rule nary_cong :premises (@p925 @p924) :args ((or @t884 (not @t883)))) % 0.35/0.68 (step @p927 :rule cnf_or_neg :args (@t884 0)) % 0.35/0.68 (step @p928 :rule eq_resolve :premises (@p927 @p926)) % 0.35/0.68 (step @p929 :rule reordering :premises (@p928) :args ((or @t675 @t884))) % 0.35/0.68 (step @p930 :rule chain_m_resolution :premises (@p929 @p923) :args (@t884 @t935 (@list @t675))) % 0.35/0.68 (step @p931 :rule and_elim :premises (@p1) :args (0)) % 0.35/0.68 (step @p932 :rule symm :premises (@p931)) % 0.35/0.68 (step @p933 :rule false_intro :premises (@p932)) % 0.35/0.68 (step @p934 :rule cong :premises (@p225 @p3) :args (@t472)) % 0.35/0.68 (step @p935 :rule trans :premises (@p934 @p933)) % 0.35/0.68 (step @p936 :rule false_elim :premises (@p935)) % 0.35/0.68 (step @p937 :rule bool-double-not-elim :args (@t472)) % 0.35/0.68 (step @p938 :rule refl :args (@t660)) % 0.35/0.68 (step @p939 :rule refl :args (@t885)) % 0.35/0.68 (step @p940 :rule nary_cong :premises (@p939 @p938 @p937) :args ((or @t885 @t660 @t936))) % 0.35/0.68 (step @p941 :rule cnf_and_neg :args (@t885)) % 0.35/0.68 (step @p942 :rule eq_resolve :premises (@p941 @p940)) % 0.35/0.68 (step @p943 :rule reordering :premises (@p942) :args ((or @t472 @t885 @t660))) % 0.35/0.68 (step @p944 :rule chain_m_resolution :premises (@p943 @p936 @p22) :args (@t885 @t937 (@list @t472 @t657))) % 0.35/0.68 (step @p945 :rule cnf_or_neg :args (@t886 1)) % 0.35/0.68 (step @p946 :rule chain_m_resolution :premises (@p945 @p944) :args (@t886 @t638 (@list @t885))) % 0.35/0.68 (step @p947 :rule cong :premises (@p225 @p49) :args (@t684)) % 0.35/0.68 (step @p948 :rule trans :premises (@p947 @p933)) % 0.35/0.68 (step @p949 :rule false_elim :premises (@p948)) % 0.35/0.68 (step @p950 :rule bool-double-not-elim :args (@t684)) % 0.35/0.68 (step @p951 :rule refl :args (@t888)) % 0.35/0.68 (step @p952 :rule nary_cong :premises (@p951 @p950) :args ((or @t888 (not @t887)))) % 0.35/0.68 (step @p953 :rule cnf_or_neg :args (@t888 0)) % 0.35/0.68 (step @p954 :rule eq_resolve :premises (@p953 @p952)) % 0.35/0.68 (step @p955 :rule reordering :premises (@p954) :args ((or @t684 @t888))) % 0.35/0.68 (step @p956 :rule chain_m_resolution :premises (@p955 @p949) :args (@t888 @t935 (@list @t684))) % 0.35/0.68 (step @p957 :rule and_elim :premises (@p1) :args (5)) % 0.35/0.68 (step @p958 :rule false_intro :premises (@p957)) % 0.35/0.68 (step @p959 :rule cong :premises (@p225 @p21) :args (@t685)) % 0.35/0.68 (step @p960 :rule trans :premises (@p959 @p958)) % 0.35/0.68 (step @p961 :rule false_elim :premises (@p960)) % 0.35/0.68 (step @p962 :rule bool-double-not-elim :args (@t685)) % 0.35/0.68 (step @p963 :rule refl :args (@t890)) % 0.35/0.68 (step @p964 :rule nary_cong :premises (@p963 @p962) :args ((or @t890 (not @t889)))) % 0.35/0.68 (step @p965 :rule cnf_or_neg :args (@t890 0)) % 0.35/0.68 (step @p966 :rule eq_resolve :premises (@p965 @p964)) % 0.35/0.68 (step @p967 :rule reordering :premises (@p966) :args ((or @t685 @t890))) % 0.35/0.68 (step @p968 :rule chain_m_resolution :premises (@p967 @p961) :args (@t890 @t935 (@list @t685))) % 0.35/0.68 (step @p969 :rule and_elim :premises (@p1) :args (6)) % 0.35/0.68 (step @p970 :rule false_intro :premises (@p969)) % 0.35/0.68 (step @p971 :rule cong :premises (@p225 @p11) :args (@t686)) % 0.35/0.68 (step @p972 :rule trans :premises (@p971 @p970)) % 0.35/0.68 (step @p973 :rule false_elim :premises (@p972)) % 0.35/0.68 (step @p974 :rule bool-double-not-elim :args (@t686)) % 0.35/0.68 (step @p975 :rule refl :args (@t892)) % 0.35/0.68 (step @p976 :rule nary_cong :premises (@p975 @p974) :args ((or @t892 (not @t891)))) % 0.35/0.68 (step @p977 :rule cnf_or_neg :args (@t892 0)) % 0.35/0.68 (step @p978 :rule eq_resolve :premises (@p977 @p976)) % 0.35/0.68 (step @p979 :rule reordering :premises (@p978) :args ((or @t686 @t892))) % 0.35/0.68 (step @p980 :rule chain_m_resolution :premises (@p979 @p973) :args (@t892 @t935 (@list @t686))) % 0.35/0.68 (step @p981 :rule cong :premises (@p225 @p44) :args (@t676)) % 0.35/0.68 (step @p982 :rule trans :premises (@p981 @p933)) % 0.35/0.68 (step @p983 :rule false_elim :premises (@p982)) % 0.35/0.68 (step @p984 :rule bool-double-not-elim :args (@t676)) % 0.35/0.68 (step @p985 :rule refl :args (@t894)) % 0.35/0.68 (step @p986 :rule nary_cong :premises (@p985 @p984) :args ((or @t894 (not @t893)))) % 0.35/0.68 (step @p987 :rule cnf_or_neg :args (@t894 0)) % 0.35/0.68 (step @p988 :rule eq_resolve :premises (@p987 @p986)) % 0.35/0.68 (step @p989 :rule reordering :premises (@p988) :args ((or @t676 @t894))) % 0.35/0.68 (step @p990 :rule chain_m_resolution :premises (@p989 @p983) :args (@t894 @t935 (@list @t676))) % 0.35/0.68 (step @p991 :rule cong :premises (@p225 @p54) :args (@t742)) % 0.35/0.68 (step @p992 :rule trans :premises (@p991 @p970)) % 0.35/0.68 (step @p993 :rule false_elim :premises (@p992)) % 0.35/0.68 (step @p994 :rule bool-double-not-elim :args (@t742)) % 0.35/0.68 (step @p995 :rule refl :args (@t896)) % 0.35/0.68 (step @p996 :rule nary_cong :premises (@p995 @p994) :args ((or @t896 (not @t895)))) % 0.35/0.68 (step @p997 :rule cnf_or_neg :args (@t896 0)) % 0.35/0.68 (step @p998 :rule eq_resolve :premises (@p997 @p996)) % 0.35/0.68 (step @p999 :rule reordering :premises (@p998) :args ((or @t742 @t896))) % 0.35/0.68 (step @p1000 :rule chain_m_resolution :premises (@p999 @p993) :args (@t896 @t935 (@list @t742))) % 0.35/0.68 (step @p1001 :rule refl :args (@t740)) % 0.35/0.68 (step @p1002 :rule refl :args (@t897)) % 0.35/0.68 (step @p1003 :rule nary_cong :premises (@p1002 @p1001 @p937) :args ((or @t897 @t740 @t936))) % 0.35/0.68 (step @p1004 :rule cnf_and_neg :args (@t897)) % 0.35/0.68 (step @p1005 :rule eq_resolve :premises (@p1004 @p1003)) % 0.35/0.68 (step @p1006 :rule reordering :premises (@p1005) :args ((or @t472 @t897 @t740))) % 0.35/0.68 (step @p1007 :rule chain_m_resolution :premises (@p1006 @p936 @p78) :args (@t897 @t937 (@list @t472 @t737))) % 0.35/0.68 (step @p1008 :rule cnf_or_neg :args (@t898 1)) % 0.35/0.68 (step @p1009 :rule chain_m_resolution :premises (@p1008 @p1007) :args (@t898 @t638 (@list @t897))) % 0.35/0.68 (step @p1010 :rule cong :premises (@p225 @p77) :args (@t748)) % 0.35/0.68 (step @p1011 :rule trans :premises (@p1010 @p920)) % 0.35/0.68 (step @p1012 :rule false_elim :premises (@p1011)) % 0.35/0.68 (step @p1013 :rule bool-double-not-elim :args (@t748)) % 0.35/0.68 (step @p1014 :rule refl :args (@t900)) % 0.35/0.68 (step @p1015 :rule nary_cong :premises (@p1014 @p1013) :args ((or @t900 (not @t899)))) % 0.35/0.68 (step @p1016 :rule cnf_or_neg :args (@t900 0)) % 0.35/0.68 (step @p1017 :rule eq_resolve :premises (@p1016 @p1015)) % 0.35/0.68 (step @p1018 :rule reordering :premises (@p1017) :args ((or @t748 @t900))) % 0.35/0.68 (step @p1019 :rule chain_m_resolution :premises (@p1018 @p1012) :args (@t900 @t935 (@list @t748))) % 0.35/0.68 (step @p1020 :rule cong :premises (@p225 @p67) :args (@t749)) % 0.35/0.68 (step @p1021 :rule trans :premises (@p1020 @p958)) % 0.35/0.68 (step @p1022 :rule false_elim :premises (@p1021)) % 0.35/0.68 (step @p1023 :rule bool-double-not-elim :args (@t749)) % 0.35/0.68 (step @p1024 :rule refl :args (@t902)) % 0.35/0.68 (step @p1025 :rule nary_cong :premises (@p1024 @p1023) :args ((or @t902 (not @t901)))) % 0.35/0.68 (step @p1026 :rule cnf_or_neg :args (@t902 0)) % 0.35/0.68 (step @p1027 :rule eq_resolve :premises (@p1026 @p1025)) % 0.35/0.68 (step @p1028 :rule reordering :premises (@p1027) :args ((or @t749 @t902))) % 0.35/0.68 (step @p1029 :rule chain_m_resolution :premises (@p1028 @p1022) :args (@t902 @t935 (@list @t749))) % 0.35/0.68 (step @p1030 :rule refl :args (@t773)) % 0.35/0.68 (step @p1031 :rule refl :args (@t903)) % 0.35/0.68 (step @p1032 :rule nary_cong :premises (@p1031 @p1030 @p937) :args ((or @t903 @t773 @t936))) % 0.35/0.68 (step @p1033 :rule cnf_and_neg :args (@t903)) % 0.35/0.68 (step @p1034 :rule eq_resolve :premises (@p1033 @p1032)) % 0.35/0.68 (step @p1035 :rule reordering :premises (@p1034) :args ((or @t472 @t903 @t773))) % 0.35/0.68 (step @p1036 :rule chain_m_resolution :premises (@p1035 @p936 @p104) :args (@t903 @t937 (@list @t472 @t770))) % 0.35/0.68 (step @p1037 :rule cnf_or_neg :args (@t904 1)) % 0.35/0.68 (step @p1038 :rule chain_m_resolution :premises (@p1037 @p1036) :args (@t904 @t638 (@list @t903))) % 0.35/0.68 (step @p1039 :rule cong :premises (@p225 @p90) :args (@t743)) % 0.35/0.68 (step @p1040 :rule trans :premises (@p1039 @p933)) % 0.35/0.68 (step @p1041 :rule false_elim :premises (@p1040)) % 0.35/0.68 (step @p1042 :rule bool-double-not-elim :args (@t743)) % 0.35/0.68 (step @p1043 :rule refl :args (@t906)) % 0.35/0.68 (step @p1044 :rule nary_cong :premises (@p1043 @p1042) :args ((or @t906 (not @t905)))) % 0.35/0.68 (step @p1045 :rule cnf_or_neg :args (@t906 0)) % 0.35/0.68 (step @p1046 :rule eq_resolve :premises (@p1045 @p1044)) % 0.35/0.68 (step @p1047 :rule reordering :premises (@p1046) :args ((or @t743 @t906))) % 0.35/0.68 (step @p1048 :rule chain_m_resolution :premises (@p1047 @p1041) :args (@t906 @t935 (@list @t743))) % 0.35/0.68 (step @p1049 :rule cong :premises (@p225 @p108) :args (@t795)) % 0.35/0.68 (step @p1050 :rule trans :premises (@p1049 @p958)) % 0.35/0.68 (step @p1051 :rule false_elim :premises (@p1050)) % 0.35/0.68 (step @p1052 :rule bool-double-not-elim :args (@t795)) % 0.35/0.68 (step @p1053 :rule refl :args (@t908)) % 0.35/0.68 (step @p1054 :rule nary_cong :premises (@p1053 @p1052) :args ((or @t908 (not @t907)))) % 0.35/0.68 (step @p1055 :rule cnf_or_neg :args (@t908 0)) % 0.35/0.68 (step @p1056 :rule eq_resolve :premises (@p1055 @p1054)) % 0.35/0.68 (step @p1057 :rule reordering :premises (@p1056) :args ((or @t795 @t908))) % 0.35/0.68 (step @p1058 :rule chain_m_resolution :premises (@p1057 @p1051) :args (@t908 @t935 (@list @t795))) % 0.35/0.68 (step @p1059 :rule cong :premises (@p225 @p103) :args (@t799)) % 0.35/0.68 (step @p1060 :rule trans :premises (@p1059 @p970)) % 0.35/0.68 (step @p1061 :rule false_elim :premises (@p1060)) % 0.35/0.68 (step @p1062 :rule bool-double-not-elim :args (@t799)) % 0.35/0.68 (step @p1063 :rule refl :args (@t910)) % 0.35/0.68 (step @p1064 :rule nary_cong :premises (@p1063 @p1062) :args ((or @t910 (not @t909)))) % 0.35/0.68 (step @p1065 :rule cnf_or_neg :args (@t910 0)) % 0.35/0.68 (step @p1066 :rule eq_resolve :premises (@p1065 @p1064)) % 0.35/0.68 (step @p1067 :rule reordering :premises (@p1066) :args ((or @t799 @t910))) % 0.35/0.68 (step @p1068 :rule chain_m_resolution :premises (@p1067 @p1061) :args (@t910 @t935 (@list @t799))) % 0.35/0.68 (step @p1069 :rule cong :premises (@p225 @p121) :args (@t800)) % 0.35/0.68 (step @p1070 :rule trans :premises (@p1069 @p920)) % 0.35/0.68 (step @p1071 :rule false_elim :premises (@p1070)) % 0.35/0.68 (step @p1072 :rule bool-double-not-elim :args (@t800)) % 0.35/0.68 (step @p1073 :rule refl :args (@t912)) % 0.35/0.68 (step @p1074 :rule nary_cong :premises (@p1073 @p1072) :args ((or @t912 (not @t911)))) % 0.35/0.68 (step @p1075 :rule cnf_or_neg :args (@t912 0)) % 0.35/0.68 (step @p1076 :rule eq_resolve :premises (@p1075 @p1074)) % 0.35/0.68 (step @p1077 :rule reordering :premises (@p1076) :args ((or @t800 @t912))) % 0.35/0.68 (step @p1078 :rule chain_m_resolution :premises (@p1077 @p1071) :args (@t912 @t935 (@list @t800))) % 0.35/0.68 (step @p1079 :rule cong :premises (@p225 @p16) :args (@t678)) % 0.35/0.68 (step @p1080 :rule trans :premises (@p1079 @p958)) % 0.35/0.68 (step @p1081 :rule false_elim :premises (@p1080)) % 0.35/0.68 (step @p1082 :rule bool-double-not-elim :args (@t678)) % 0.35/0.68 (step @p1083 :rule refl :args (@t914)) % 0.35/0.68 (step @p1084 :rule nary_cong :premises (@p1083 @p1082) :args ((or @t914 (not @t913)))) % 0.35/0.68 (step @p1085 :rule cnf_or_neg :args (@t914 0)) % 0.35/0.68 (step @p1086 :rule eq_resolve :premises (@p1085 @p1084)) % 0.35/0.68 (step @p1087 :rule reordering :premises (@p1086) :args ((or @t678 @t914))) % 0.35/0.68 (step @p1088 :rule chain_m_resolution :premises (@p1087 @p1081) :args (@t914 @t935 (@list @t678))) % 0.35/0.68 (step @p1089 :rule cong :premises (@p225 @p72) :args (@t744)) % 0.35/0.68 (step @p1090 :rule trans :premises (@p1089 @p920)) % 0.35/0.68 (step @p1091 :rule false_elim :premises (@p1090)) % 0.35/0.68 (step @p1092 :rule bool-double-not-elim :args (@t744)) % 0.35/0.68 (step @p1093 :rule refl :args (@t916)) % 0.35/0.68 (step @p1094 :rule nary_cong :premises (@p1093 @p1092) :args ((or @t916 (not @t915)))) % 0.35/0.68 (step @p1095 :rule cnf_or_neg :args (@t916 0)) % 0.35/0.68 (step @p1096 :rule eq_resolve :premises (@p1095 @p1094)) % 0.35/0.68 (step @p1097 :rule reordering :premises (@p1096) :args ((or @t744 @t916))) % 0.35/0.68 (step @p1098 :rule chain_m_resolution :premises (@p1097 @p1091) :args (@t916 @t935 (@list @t744))) % 0.35/0.68 (step @p1099 :rule cong :premises (@p225 @p98) :args (@t796)) % 0.35/0.68 (step @p1100 :rule trans :premises (@p1099 @p970)) % 0.35/0.68 (step @p1101 :rule false_elim :premises (@p1100)) % 0.35/0.68 (step @p1102 :rule bool-double-not-elim :args (@t796)) % 0.35/0.68 (step @p1103 :rule refl :args (@t918)) % 0.35/0.68 (step @p1104 :rule nary_cong :premises (@p1103 @p1102) :args ((or @t918 (not @t917)))) % 0.35/0.68 (step @p1105 :rule cnf_or_neg :args (@t918 0)) % 0.35/0.68 (step @p1106 :rule eq_resolve :premises (@p1105 @p1104)) % 0.35/0.68 (step @p1107 :rule reordering :premises (@p1106) :args ((or @t796 @t918))) % 0.35/0.68 (step @p1108 :rule chain_m_resolution :premises (@p1107 @p1101) :args (@t918 @t935 (@list @t796))) % 0.35/0.68 (step @p1109 :rule cong :premises (@p225 @p166) :args (@t824)) % 0.35/0.68 (step @p1110 :rule trans :premises (@p1109 @p933)) % 0.35/0.68 (step @p1111 :rule false_elim :premises (@p1110)) % 0.35/0.68 (step @p1112 :rule bool-double-not-elim :args (@t824)) % 0.35/0.68 (step @p1113 :rule refl :args (@t920)) % 0.35/0.68 (step @p1114 :rule nary_cong :premises (@p1113 @p1112) :args ((or @t920 (not @t919)))) % 0.35/0.68 (step @p1115 :rule cnf_or_neg :args (@t920 0)) % 0.35/0.68 (step @p1116 :rule eq_resolve :premises (@p1115 @p1114)) % 0.35/0.68 (step @p1117 :rule reordering :premises (@p1116) :args ((or @t824 @t920))) % 0.35/0.68 (step @p1118 :rule chain_m_resolution :premises (@p1117 @p1111) :args (@t920 @t935 (@list @t824))) % 0.35/0.68 (step @p1119 :rule cong :premises (@p225 @p198) :args (@t849)) % 0.35/0.68 (step @p1120 :rule trans :premises (@p1119 @p933)) % 0.35/0.68 (step @p1121 :rule false_elim :premises (@p1120)) % 0.35/0.68 (step @p1122 :rule bool-double-not-elim :args (@t849)) % 0.35/0.68 (step @p1123 :rule refl :args (@t932)) % 0.35/0.68 (step @p1124 :rule nary_cong :premises (@p1123 @p1122) :args ((or @t932 (not @t931)))) % 0.35/0.68 (step @p1125 :rule cnf_or_neg :args (@t932 0)) % 0.35/0.68 (step @p1126 :rule eq_resolve :premises (@p1125 @p1124)) % 0.35/0.68 (step @p1127 :rule reordering :premises (@p1126) :args ((or @t849 @t932))) % 0.35/0.68 (step @p1128 :rule chain_m_resolution :premises (@p1127 @p1121) :args (@t932 @t935 (@list @t849))) % 0.35/0.68 (step @p1129 :rule cong :premises (@p225 @p6) :args (@t679)) % 0.35/0.68 (step @p1130 :rule trans :premises (@p1129 @p970)) % 0.35/0.68 (step @p1131 :rule false_elim :premises (@p1130)) % 0.35/0.68 (step @p1132 :rule bool-double-not-elim :args (@t679)) % 0.35/0.68 (step @p1133 :rule refl :args (@t924)) % 0.35/0.68 (step @p1134 :rule nary_cong :premises (@p1133 @p1132) :args ((or @t924 (not @t923)))) % 0.35/0.68 (step @p1135 :rule cnf_or_neg :args (@t924 0)) % 0.35/0.68 (step @p1136 :rule eq_resolve :premises (@p1135 @p1134)) % 0.35/0.68 (step @p1137 :rule reordering :premises (@p1136) :args ((or @t679 @t924))) % 0.35/0.68 (step @p1138 :rule chain_m_resolution :premises (@p1137 @p1131) :args (@t924 @t935 (@list @t679))) % 0.35/0.68 (step @p1139 :rule cong :premises (@p225 @p62) :args (@t745)) % 0.35/0.68 (step @p1140 :rule trans :premises (@p1139 @p958)) % 0.35/0.68 (step @p1141 :rule false_elim :premises (@p1140)) % 0.35/0.68 (step @p1142 :rule bool-double-not-elim :args (@t745)) % 0.35/0.68 (step @p1143 :rule refl :args (@t926)) % 0.35/0.68 (step @p1144 :rule nary_cong :premises (@p1143 @p1142) :args ((or @t926 (not @t925)))) % 0.35/0.68 (step @p1145 :rule cnf_or_neg :args (@t926 0)) % 0.35/0.68 (step @p1146 :rule eq_resolve :premises (@p1145 @p1144)) % 0.35/0.68 (step @p1147 :rule reordering :premises (@p1146) :args ((or @t745 @t926))) % 0.35/0.68 (step @p1148 :rule chain_m_resolution :premises (@p1147 @p1141) :args (@t926 @t935 (@list @t745))) % 0.35/0.68 (step @p1149 :rule cong :premises (@p225 @p116) :args (@t797)) % 0.35/0.68 (step @p1150 :rule trans :premises (@p1149 @p920)) % 0.35/0.68 (step @p1151 :rule false_elim :premises (@p1150)) % 0.35/0.68 (step @p1152 :rule bool-double-not-elim :args (@t797)) % 0.35/0.68 (step @p1153 :rule refl :args (@t928)) % 0.35/0.68 (step @p1154 :rule nary_cong :premises (@p1153 @p1152) :args ((or @t928 (not @t927)))) % 0.35/0.68 (step @p1155 :rule cnf_or_neg :args (@t928 0)) % 0.35/0.68 (step @p1156 :rule eq_resolve :premises (@p1155 @p1154)) % 0.35/0.68 (step @p1157 :rule reordering :premises (@p1156) :args ((or @t797 @t928))) % 0.35/0.68 (step @p1158 :rule chain_m_resolution :premises (@p1157 @p1151) :args (@t928 @t935 (@list @t797))) % 0.35/0.68 (step @p1159 :rule refl :args (@t827)) % 0.35/0.68 (step @p1160 :rule refl :args (@t929)) % 0.35/0.68 (step @p1161 :rule nary_cong :premises (@p1160 @p1159 @p937) :args ((or @t929 @t827 @t936))) % 0.35/0.68 (step @p1162 :rule cnf_and_neg :args (@t929)) % 0.35/0.68 (step @p1163 :rule eq_resolve :premises (@p1162 @p1161)) % 0.35/0.68 (step @p1164 :rule reordering :premises (@p1163) :args ((or @t472 @t827 @t929))) % 0.35/0.68 (step @p1165 :rule chain_m_resolution :premises (@p1164 @p936 @p157) :args (@t929 @t937 (@list @t472 @t825))) % 0.35/0.68 (step @p1166 :rule cnf_or_neg :args (@t930 1)) % 0.35/0.68 (step @p1167 :rule chain_m_resolution :premises (@p1166 @p1165) :args (@t930 @t638 (@list @t929))) % 0.35/0.68 (step @p1168 :rule refl :args (@t836)) % 0.35/0.68 (step @p1169 :rule refl :args (@t921)) % 0.35/0.68 (step @p1170 :rule nary_cong :premises (@p1169 @p1168 @p937) :args ((or @t921 @t836 @t936))) % 0.35/0.68 (step @p1171 :rule cnf_and_neg :args (@t921)) % 0.35/0.68 (step @p1172 :rule eq_resolve :premises (@p1171 @p1170)) % 0.35/0.68 (step @p1173 :rule reordering :premises (@p1172) :args ((or @t472 @t836 @t921))) % 0.35/0.68 (step @p1174 :rule chain_m_resolution :premises (@p1173 @p936 @p167) :args (@t921 @t937 (@list @t472 @t833))) % 0.35/0.68 (step @p1175 :rule cnf_or_neg :args (@t922 1)) % 0.35/0.68 (step @p1176 :rule chain_m_resolution :premises (@p1175 @p1174) :args (@t922 @t638 (@list @t921))) % 0.35/0.68 (step @p1177 :rule cnf_and_neg :args (@t933)) % 0.35/0.68 (step @p1178 false :rule chain_m_resolution :premises (@p1177 @p1176 @p1167 @p1158 @p1148 @p1138 @p1128 @p1118 @p1108 @p1098 @p1088 @p1078 @p1068 @p1058 @p1048 @p1038 @p1029 @p1019 @p1009 @p1000 @p990 @p980 @p968 @p956 @p946 @p930 @p918) :args (false (@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 true) (@list @t922 @t930 @t928 @t926 @t924 @t932 @t920 @t918 @t916 @t914 @t912 @t910 @t908 @t906 @t904 @t902 @t900 @t898 @t896 @t894 @t892 @t890 @t888 @t886 @t884 @t933))) % 0.35/0.68 ) % 0.35/0.68 % SZS output end Proof % 0.35/0.68 % cvc5 exiting %------------------------------------------------------------------------------