%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : RNG027-2 : TPTP v9.2.1. Bugfixed v1.2.1. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n021.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:45:25 AM UTC 2026 % Result : Unsatisfiable 62.22s 62.42s % Output : Proof 62.22s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : RNG027-2 : TPTP v9.2.1. Bugfixed v1.2.1. % 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.15/0.34 % Computer : n021.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 : Tue Jun 2 13:59:35 EDT 2026 % 0.15/0.34 % CPUTime : % 0.29/0.49 %----Proving TF0_NAR, FOF, or CNF % 0.29/0.50 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 15.52/15.76 --- Run --no-e-matching --full-saturate-quant at 6... % 21.52/21.79 --- Run --no-e-matching --enum-inst-sum --full-saturate-quant at 6... % 27.62/27.83 --- Run --finite-model-find --uf-ss=no-minimal at 6... % 33.63/33.86 --- Run --multi-trigger-when-single --full-saturate-quant at 30... % 62.22/62.42 % SZS status Unsatisfiable % 62.22/62.42 % SZS output start Proof % 62.22/62.44 ( % 62.22/62.44 (declare-sort $$unsorted 0) % 62.22/62.44 (declare-const tptp.cz $$unsorted) % 62.22/62.44 (declare-const tptp.associator (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 62.22/62.44 (declare-const tptp.additive_inverse (-> $$unsorted $$unsorted)) % 62.22/62.44 (declare-const tptp.cy $$unsorted) % 62.22/62.44 (declare-const tptp.multiply (-> $$unsorted $$unsorted $$unsorted)) % 62.22/62.44 (declare-const tptp.cx $$unsorted) % 62.22/62.44 (declare-const tptp.add (-> $$unsorted $$unsorted $$unsorted)) % 62.22/62.44 (declare-const tptp.additive_identity $$unsorted) % 62.22/62.44 (define @t1 () (@var "X" $$unsorted)) % 62.22/62.44 (define @t2 () (tptp.add tptp.additive_identity @t1)) % 62.22/62.44 (define @t3 () (@list @t1)) % 62.22/62.44 (define @t4 () (forall @t3 (= @t2 @t1))) % 62.22/62.44 (define @t5 () (tptp.additive_inverse @t1)) % 62.22/62.44 (define @t6 () (tptp.add @t5 @t1)) % 62.22/62.44 (define @t7 () (forall @t3 (= @t6 tptp.additive_identity))) % 62.22/62.44 (define @t8 () (@var "Y" $$unsorted)) % 62.22/62.44 (define @t9 () (tptp.additive_inverse @t8)) % 62.22/62.44 (define @t10 () (tptp.add @t1 @t8)) % 62.22/62.44 (define @t11 () (@list @t1 @t8)) % 62.22/62.44 (define @t12 () (tptp.additive_inverse @t5)) % 62.22/62.44 (define @t13 () (forall @t3 (= @t12 @t1))) % 62.22/62.44 (define @t14 () (@var "Z" $$unsorted)) % 62.22/62.44 (define @t15 () (tptp.multiply @t1 @t14)) % 62.22/62.44 (define @t16 () (tptp.multiply @t1 @t8)) % 62.22/62.44 (define @t17 () (tptp.add @t8 @t14)) % 62.22/62.44 (define @t18 () (@list @t1 @t8 @t14)) % 62.22/62.44 (define @t19 () (tptp.multiply @t8 @t14)) % 62.22/62.44 (define @t20 () (forall @t11 (= (tptp.multiply @t16 @t8) (tptp.multiply @t1 (tptp.multiply @t8 @t8))))) % 62.22/62.44 (define @t21 () (tptp.additive_inverse @t16)) % 62.22/62.44 (define @t22 () (forall @t11 (= (tptp.multiply @t5 @t8) @t21))) % 62.22/62.44 (define @t23 () (tptp.multiply @t1 @t9)) % 62.22/62.44 (define @t24 () (forall @t11 (= @t23 @t21))) % 62.22/62.44 (define @t25 () (tptp.additive_inverse tptp.additive_identity)) % 62.22/62.44 (define @t26 () (= @t1 @t8)) % 62.22/62.44 (define @t27 () (tptp.add @t1 @t14)) % 62.22/62.44 (define @t28 () (not (= @t27 @t17))) % 62.22/62.44 (define @t29 () (or @t28 @t26)) % 62.22/62.44 (define @t30 () (@list @t1 @t14 @t8)) % 62.22/62.44 (define @t31 () (forall @t30 @t29)) % 62.22/62.44 (define @t32 () (tptp.associator @t1 @t8 @t14)) % 62.22/62.44 (define @t33 () (tptp.additive_inverse @t32)) % 62.22/62.44 (define @t34 () (forall (@list @t8 @t1 @t14) (= (tptp.associator @t8 @t1 @t14) @t33))) % 62.22/62.44 (define @t35 () (tptp.associator @t14 @t8 @t1)) % 62.22/62.44 (define @t36 () (forall (@list @t14 @t8 @t1) (= @t35 @t33))) % 62.22/62.44 (define @t37 () (tptp.multiply tptp.cz tptp.cx)) % 62.22/62.44 (define @t38 () (tptp.multiply @t37 tptp.cy)) % 62.22/62.44 (define @t39 () (tptp.multiply @t38 tptp.cx)) % 62.22/62.44 (define @t40 () (tptp.multiply tptp.cy tptp.cx)) % 62.22/62.44 (define @t41 () (tptp.multiply tptp.cx @t40)) % 62.22/62.44 (define @t42 () (tptp.multiply tptp.cz @t41)) % 62.22/62.44 (define @t43 () (@list tptp.cz tptp.cx tptp.cy)) % 62.22/62.44 (define @t44 () (@list @t37 tptp.cy tptp.cx)) % 62.22/62.44 (define @t45 () (@list tptp.cz tptp.cx @t40)) % 62.22/62.44 (define @t46 () (@list @t42)) % 62.22/62.44 (define @t47 () (tptp.multiply tptp.cx tptp.cy)) % 62.22/62.44 (define @t48 () (tptp.additive_inverse tptp.cz)) % 62.22/62.44 (define @t49 () (tptp.multiply @t48 @t47)) % 62.22/62.44 (define @t50 () (tptp.additive_inverse (tptp.multiply tptp.cz @t47))) % 62.22/62.44 (define @t51 () (= @t49 @t50)) % 62.22/62.44 (define @t52 () (@list tptp.cz @t47)) % 62.22/62.44 (define @t53 () (= @t50 @t49)) % 62.22/62.44 (define @t54 () (@list false)) % 62.22/62.44 (define @t55 () (@list @t22)) % 62.22/62.44 (define @t56 () (tptp.additive_inverse @t37)) % 62.22/62.44 (define @t57 () (tptp.multiply @t56 @t40)) % 62.22/62.44 (define @t58 () (tptp.multiply @t37 @t40)) % 62.22/62.44 (define @t59 () (tptp.additive_inverse @t58)) % 62.22/62.44 (define @t60 () (= @t57 @t59)) % 62.22/62.44 (define @t61 () (@list @t37 @t40)) % 62.22/62.44 (define @t62 () (= @t59 @t57)) % 62.22/62.44 (define @t63 () (tptp.additive_inverse @t42)) % 62.22/62.44 (define @t64 () (@list tptp.cx)) % 62.22/62.44 (define @t65 () (@list @t40)) % 62.22/62.44 (define @t66 () (tptp.associator tptp.cz tptp.cx tptp.cy)) % 62.22/62.44 (define @t67 () (tptp.additive_inverse @t41)) % 62.22/62.44 (define @t68 () (tptp.multiply @t48 tptp.cx)) % 62.22/62.44 (define @t69 () (= @t68 @t56)) % 62.22/62.44 (define @t70 () (@list tptp.cz tptp.cx)) % 62.22/62.44 (define @t71 () (= @t56 @t68)) % 62.22/62.44 (define @t72 () (tptp.additive_inverse tptp.cy)) % 62.22/62.44 (define @t73 () (tptp.multiply @t72 tptp.cx)) % 62.22/62.44 (define @t74 () (tptp.additive_inverse @t40)) % 62.22/62.44 (define @t75 () (= @t73 @t74)) % 62.22/62.44 (define @t76 () (@list tptp.cy tptp.cx)) % 62.22/62.44 (define @t77 () (= @t74 @t73)) % 62.22/62.44 (define @t78 () (@list tptp.cy tptp.cz tptp.cx)) % 62.22/62.44 (define @t79 () (tptp.multiply @t56 tptp.cy)) % 62.22/62.44 (define @t80 () (tptp.additive_inverse @t38)) % 62.22/62.44 (define @t81 () (= @t79 @t80)) % 62.22/62.44 (define @t82 () (@list @t37 tptp.cy)) % 62.22/62.44 (define @t83 () (= @t80 @t79)) % 62.22/62.44 (define @t84 () (tptp.additive_inverse tptp.cx)) % 62.22/62.44 (define @t85 () (@list @t84 tptp.cx)) % 62.22/62.44 (define @t86 () (tptp.additive_inverse @t50)) % 62.22/62.44 (define @t87 () (tptp.multiply @t80 tptp.cx)) % 62.22/62.44 (define @t88 () (tptp.additive_inverse @t39)) % 62.22/62.44 (define @t89 () (= @t87 @t88)) % 62.22/62.44 (define @t90 () (@list @t38 tptp.cx)) % 62.22/62.44 (define @t91 () (= @t88 @t87)) % 62.22/62.44 (define @t92 () (tptp.multiply @t37 tptp.cx)) % 62.22/62.44 (define @t93 () (tptp.multiply @t72 @t92)) % 62.22/62.44 (define @t94 () (tptp.multiply tptp.cy @t92)) % 62.22/62.44 (define @t95 () (tptp.additive_inverse @t94)) % 62.22/62.44 (define @t96 () (= @t93 @t95)) % 62.22/62.44 (define @t97 () (@list tptp.cy @t92)) % 62.22/62.44 (define @t98 () (= @t95 @t93)) % 62.22/62.44 (define @t99 () (tptp.associator tptp.cz @t40 tptp.cx)) % 62.22/62.44 (define @t100 () (tptp.associator @t40 tptp.cz tptp.cx)) % 62.22/62.44 (define @t101 () (tptp.additive_inverse @t100)) % 62.22/62.44 (define @t102 () (= @t99 @t101)) % 62.22/62.44 (define @t103 () (@list tptp.cz @t40 tptp.cx)) % 62.22/62.44 (define @t104 () (= @t101 @t99)) % 62.22/62.44 (define @t105 () (@list @t34)) % 62.22/62.44 (define @t106 () (@list tptp.cy @t56 tptp.cx)) % 62.22/62.44 (define @t107 () (tptp.additive_inverse @t63)) % 62.22/62.44 (define @t108 () (tptp.add @t107 @t59)) % 62.22/62.44 (define @t109 () (tptp.add @t39 @t59)) % 62.22/62.44 (define @t110 () (= @t109 @t108)) % 62.22/62.44 (define @t111 () (not @t110)) % 62.22/62.44 (define @t112 () (= @t107 @t39)) % 62.22/62.44 (define @t113 () (or @t111 @t112)) % 62.22/62.44 (define @t114 () (forall @t30 (or (not (= @t17 @t27)) @t26))) % 62.22/62.44 (define @t115 () (= @t39 @t107)) % 62.22/62.44 (define @t116 () (or @t111 @t115)) % 62.22/62.44 (define @t117 () (@list @t114)) % 62.22/62.44 (define @t118 () (tptp.multiply tptp.cz @t40)) % 62.22/62.44 (define @t119 () (tptp.additive_inverse @t118)) % 62.22/62.44 (define @t120 () (tptp.multiply tptp.cz @t74)) % 62.22/62.44 (define @t121 () (forall @t11 (= @t21 @t23))) % 62.22/62.44 (define @t122 () (= @t119 @t120)) % 62.22/62.44 (define @t123 () (@list tptp.cz @t40)) % 62.22/62.44 (define @t124 () (= @t120 @t119)) % 62.22/62.44 (define @t125 () (@list @t121)) % 62.22/62.44 (define @t126 () (tptp.multiply tptp.cy @t37)) % 62.22/62.44 (define @t127 () (tptp.additive_inverse @t126)) % 62.22/62.44 (define @t128 () (tptp.multiply tptp.cy tptp.cz)) % 62.22/62.44 (define @t129 () (tptp.multiply @t128 tptp.cx)) % 62.22/62.44 (define @t130 () (tptp.multiply tptp.cx tptp.cx)) % 62.22/62.44 (define @t131 () (@list tptp.cy @t37)) % 62.22/62.44 (define @t132 () (@list tptp.cz tptp.cy)) % 62.22/62.44 (define @t133 () (tptp.multiply tptp.cz tptp.cy)) % 62.22/62.44 (define @t134 () (@list @t133 @t84)) % 62.22/62.44 (define @t135 () (tptp.additive_inverse @t130)) % 62.22/62.44 (define @t136 () (tptp.multiply tptp.cx @t84)) % 62.22/62.44 (define @t137 () (= @t135 @t136)) % 62.22/62.44 (define @t138 () (= @t136 @t135)) % 62.22/62.44 (define @t139 () (tptp.add tptp.cx @t84)) % 62.22/62.44 (define @t140 () (tptp.multiply @t48 @t40)) % 62.22/62.44 (define @t141 () (= @t140 @t119)) % 62.22/62.44 (define @t142 () (= @t119 @t140)) % 62.22/62.44 (define @t143 () (tptp.multiply @t56 tptp.cx)) % 62.22/62.44 (define @t144 () (tptp.additive_inverse @t92)) % 62.22/62.44 (define @t145 () (= @t143 @t144)) % 62.22/62.44 (define @t146 () (= @t144 @t143)) % 62.22/62.44 (define @t147 () (tptp.multiply @t72 @t37)) % 62.22/62.44 (define @t148 () (= @t147 @t127)) % 62.22/62.44 (define @t149 () (= @t127 @t147)) % 62.22/62.44 (define @t150 () (tptp.multiply @t48 tptp.cy)) % 62.22/62.44 (define @t151 () (tptp.additive_inverse @t133)) % 62.22/62.44 (define @t152 () (= @t150 @t151)) % 62.22/62.44 (define @t153 () (= @t151 @t150)) % 62.22/62.44 (define @t154 () (@list tptp.cy tptp.cz @t130)) % 62.22/62.44 (define @t155 () (@list @t126 tptp.cx)) % 62.22/62.44 (define @t156 () (@list @t128 tptp.cx)) % 62.22/62.44 (define @t157 () (tptp.additive_inverse @t140)) % 62.22/62.44 (define @t158 () (tptp.multiply @t48 @t74)) % 62.22/62.44 (define @t159 () (= @t157 @t158)) % 62.22/62.44 (define @t160 () (= @t158 @t157)) % 62.22/62.44 (define @t161 () (tptp.multiply @t127 tptp.cx)) % 62.22/62.44 (define @t162 () (tptp.additive_inverse (tptp.multiply @t126 tptp.cx))) % 62.22/62.44 (define @t163 () (= @t161 @t162)) % 62.22/62.44 (define @t164 () (= @t162 @t161)) % 62.22/62.44 (define @t165 () (tptp.multiply @t133 tptp.cx)) % 62.22/62.44 (define @t166 () (tptp.associator tptp.cx tptp.cz tptp.cy)) % 62.22/62.44 (define @t167 () (tptp.additive_inverse @t166)) % 62.22/62.44 (define @t168 () (tptp.add @t167 @t165)) % 62.22/62.44 (define @t169 () (= (tptp.add @t118 @t120) (tptp.add @t168 @t120))) % 62.22/62.44 (define @t170 () (not @t169)) % 62.22/62.44 (define @t171 () (or @t170 (= @t168 @t118))) % 62.22/62.44 (define @t172 () (= @t118 @t168)) % 62.22/62.44 (define @t173 () (or @t170 @t172)) % 62.22/62.44 (define @t174 () (@list tptp.cz tptp.cy tptp.cx)) % 62.22/62.44 (define @t175 () (tptp.associator tptp.cz tptp.cy tptp.cx)) % 62.22/62.44 (define @t176 () (tptp.associator tptp.cy tptp.cz tptp.cx)) % 62.22/62.44 (define @t177 () (tptp.additive_inverse @t176)) % 62.22/62.44 (define @t178 () (= @t175 @t177)) % 62.22/62.44 (define @t179 () (tptp.additive_inverse @t66)) % 62.22/62.44 (define @t180 () (tptp.add @t50 @t38)) % 62.22/62.44 (define @t181 () (tptp.multiply tptp.cz @t67)) % 62.22/62.44 (define @t182 () (tptp.add @t181 @t42)) % 62.22/62.44 (define @t183 () (@list tptp.cy tptp.cz)) % 62.22/62.44 (define @t184 () (tptp.multiply @t72 tptp.cz)) % 62.22/62.44 (define @t185 () (tptp.additive_inverse @t128)) % 62.22/62.44 (define @t186 () (= @t184 @t185)) % 62.22/62.44 (define @t187 () (= @t185 @t184)) % 62.22/62.44 (define @t188 () (tptp.multiply @t185 tptp.cx)) % 62.22/62.44 (define @t189 () (tptp.additive_inverse @t129)) % 62.22/62.44 (define @t190 () (= @t188 @t189)) % 62.22/62.44 (define @t191 () (= @t189 @t188)) % 62.22/62.44 (define @t192 () (tptp.multiply tptp.cz @t139)) % 62.22/62.44 (define @t193 () (tptp.multiply @t128 @t84)) % 62.22/62.44 (define @t194 () (@list tptp.cz tptp.cy @t130)) % 62.22/62.44 (define @t195 () (tptp.add @t74 @t40)) % 62.22/62.44 (define @t196 () (tptp.additive_inverse @t150)) % 62.22/62.44 (define @t197 () (tptp.multiply @t48 @t72)) % 62.22/62.44 (define @t198 () (= @t196 @t197)) % 62.22/62.44 (define @t199 () (= @t197 @t196)) % 62.22/62.44 (define @t200 () (@list @t128 @t130)) % 62.22/62.44 (define @t201 () (tptp.multiply @t185 @t130)) % 62.22/62.44 (define @t202 () (tptp.multiply @t128 @t130)) % 62.22/62.44 (define @t203 () (tptp.additive_inverse @t202)) % 62.22/62.44 (define @t204 () (= @t201 @t203)) % 62.22/62.44 (define @t205 () (= @t203 @t201)) % 62.22/62.44 (define @t206 () (tptp.additive_inverse @t193)) % 62.22/62.44 (define @t207 () (tptp.multiply @t129 tptp.cx)) % 62.22/62.44 (define @t208 () (= @t207 @t202)) % 62.22/62.44 (define @t209 () (= @t202 @t207)) % 62.22/62.44 (define @t210 () (tptp.multiply tptp.cz @t130)) % 62.22/62.44 (define @t211 () (tptp.additive_inverse (tptp.multiply tptp.cy @t210))) % 62.22/62.44 (define @t212 () (tptp.multiply @t133 @t84)) % 62.22/62.44 (define @t213 () (@list @t212 tptp.cx)) % 62.22/62.44 (define @t214 () (tptp.additive_inverse (tptp.multiply @t212 tptp.cx))) % 62.22/62.44 (define @t215 () (tptp.multiply @t212 @t84)) % 62.22/62.44 (define @t216 () (= @t214 @t215)) % 62.22/62.44 (define @t217 () (= @t215 @t214)) % 62.22/62.44 (define @t218 () (tptp.multiply @t40 tptp.cx)) % 62.22/62.44 (define @t219 () (tptp.additive_inverse (tptp.multiply tptp.cz @t218))) % 62.22/62.44 (define @t220 () (tptp.multiply @t165 tptp.cx)) % 62.22/62.44 (define @t221 () (tptp.multiply @t167 tptp.cx)) % 62.22/62.44 (define @t222 () (tptp.multiply @t72 @t210)) % 62.22/62.44 (define @t223 () (tptp.additive_inverse @t222)) % 62.22/62.44 (define @t224 () (tptp.multiply @t184 @t130)) % 62.22/62.44 (define @t225 () (tptp.add @t221 @t224)) % 62.22/62.44 (define @t226 () (tptp.add @t225 @t223)) % 62.22/62.44 (define @t227 () (tptp.add @t224 @t223)) % 62.22/62.44 (define @t228 () (tptp.add @t221 @t227)) % 62.22/62.44 (define @t229 () (= @t228 @t226)) % 62.22/62.44 (define @t230 () (not @t229)) % 62.22/62.44 (define @t231 () (tptp.multiply @t84 @t84)) % 62.22/62.44 (define @t232 () (= @t215 (tptp.multiply @t133 @t231))) % 62.22/62.44 (define @t233 () (not @t232)) % 62.22/62.44 (define @t234 () (tptp.multiply tptp.cy @t130)) % 62.22/62.44 (define @t235 () (tptp.multiply tptp.cz @t234)) % 62.22/62.44 (define @t236 () (tptp.additive_inverse @t235)) % 62.22/62.44 (define @t237 () (tptp.multiply @t133 @t130)) % 62.22/62.44 (define @t238 () (tptp.add @t237 @t236)) % 62.22/62.44 (define @t239 () (tptp.associator tptp.cz tptp.cy @t130)) % 62.22/62.44 (define @t240 () (= @t239 @t238)) % 62.22/62.44 (define @t241 () (not @t240)) % 62.22/62.44 (define @t242 () (tptp.add @t221 @t220)) % 62.22/62.44 (define @t243 () (tptp.add @t242 @t219)) % 62.22/62.44 (define @t244 () (= (tptp.add @t221 (tptp.add @t220 @t219)) @t243)) % 62.22/62.44 (define @t245 () (not @t244)) % 62.22/62.44 (define @t246 () (tptp.add @t66 @t193)) % 62.22/62.44 (define @t247 () (tptp.multiply @t246 tptp.cx)) % 62.22/62.44 (define @t248 () (= @t247 (tptp.add (tptp.multiply @t66 tptp.cx) (tptp.multiply @t193 tptp.cx)))) % 62.22/62.44 (define @t249 () (not @t248)) % 62.22/62.44 (define @t250 () (not @t217)) % 62.22/62.44 (define @t251 () (tptp.multiply @t189 tptp.cx)) % 62.22/62.44 (define @t252 () (= @t251 (tptp.additive_inverse @t207))) % 62.22/62.44 (define @t253 () (not @t252)) % 62.22/62.44 (define @t254 () (tptp.additive_inverse @t212)) % 62.22/62.44 (define @t255 () (tptp.multiply @t254 tptp.cx)) % 62.22/62.44 (define @t256 () (= @t255 @t214)) % 62.22/62.44 (define @t257 () (not @t256)) % 62.22/62.44 (define @t258 () (tptp.add @t202 @t211)) % 62.22/62.44 (define @t259 () (tptp.additive_inverse @t258)) % 62.22/62.44 (define @t260 () (= @t259 (tptp.add @t203 (tptp.additive_inverse @t211)))) % 62.22/62.44 (define @t261 () (not @t260)) % 62.22/62.44 (define @t262 () (not @t209)) % 62.22/62.44 (define @t263 () (tptp.add @t206 @t193)) % 62.22/62.44 (define @t264 () (tptp.add @t127 @t263)) % 62.22/62.44 (define @t265 () (= @t264 (tptp.add (tptp.add @t127 @t206) @t193))) % 62.22/62.44 (define @t266 () (not @t265)) % 62.22/62.44 (define @t267 () (not @t205)) % 62.22/62.44 (define @t268 () (= @t203 (tptp.multiply @t128 @t135))) % 62.22/62.44 (define @t269 () (not @t268)) % 62.22/62.44 (define @t270 () (not @t199)) % 62.22/62.44 (define @t271 () (tptp.add @t195 @t127)) % 62.22/62.44 (define @t272 () (= @t271 (tptp.add @t127 @t195))) % 62.22/62.44 (define @t273 () (not @t272)) % 62.22/62.44 (define @t274 () (tptp.associator @t130 tptp.cy tptp.cz)) % 62.22/62.44 (define @t275 () (tptp.additive_inverse @t274)) % 62.22/62.44 (define @t276 () (= @t275 @t239)) % 62.22/62.44 (define @t277 () (not @t276)) % 62.22/62.44 (define @t278 () (tptp.additive_inverse @t239)) % 62.22/62.44 (define @t279 () (tptp.associator tptp.cy tptp.cz @t130)) % 62.22/62.44 (define @t280 () (= @t279 @t278)) % 62.22/62.44 (define @t281 () (not @t280)) % 62.22/62.44 (define @t282 () (= tptp.additive_identity @t263)) % 62.22/62.44 (define @t283 () (not @t282)) % 62.22/62.44 (define @t284 () (tptp.multiply @t168 tptp.cx)) % 62.22/62.44 (define @t285 () (= @t284 @t242)) % 62.22/62.44 (define @t286 () (not @t285)) % 62.22/62.44 (define @t287 () (tptp.add @t192 @t37)) % 62.22/62.44 (define @t288 () (tptp.multiply @t72 @t287)) % 62.22/62.44 (define @t289 () (= @t288 (tptp.add (tptp.multiply @t72 @t192) @t147))) % 62.22/62.44 (define @t290 () (not @t289)) % 62.22/62.44 (define @t291 () (not @t191)) % 62.22/62.44 (define @t292 () (not @t187)) % 62.22/62.44 (define @t293 () (tptp.additive_inverse @t72)) % 62.22/62.44 (define @t294 () (tptp.multiply tptp.cz @t293)) % 62.22/62.44 (define @t295 () (tptp.multiply tptp.cz @t72)) % 62.22/62.44 (define @t296 () (= (tptp.additive_inverse @t295) @t294)) % 62.22/62.44 (define @t297 () (not @t296)) % 62.22/62.44 (define @t298 () (tptp.multiply tptp.cy @t48)) % 62.22/62.44 (define @t299 () (= @t185 @t298)) % 62.22/62.44 (define @t300 () (not @t299)) % 62.22/62.44 (define @t301 () (not @t164)) % 62.22/62.44 (define @t302 () (not @t172)) % 62.22/62.44 (define @t303 () (= tptp.cy @t293)) % 62.22/62.44 (define @t304 () (not @t303)) % 62.22/62.44 (define @t305 () (tptp.multiply @t72 @t84)) % 62.22/62.44 (define @t306 () (tptp.multiply @t72 @t139)) % 62.22/62.44 (define @t307 () (= @t306 (tptp.add @t73 @t305))) % 62.22/62.44 (define @t308 () (not @t307)) % 62.22/62.44 (define @t309 () (tptp.additive_inverse (tptp.multiply @t84 tptp.cx))) % 62.22/62.44 (define @t310 () (= @t309 @t231)) % 62.22/62.44 (define @t311 () (not @t310)) % 62.22/62.44 (define @t312 () (not @t160)) % 62.22/62.44 (define @t313 () (= @t189 @t193)) % 62.22/62.44 (define @t314 () (not @t313)) % 62.22/62.44 (define @t315 () (= @t162 (tptp.multiply @t126 @t84))) % 62.22/62.44 (define @t316 () (not @t315)) % 62.22/62.44 (define @t317 () (tptp.associator tptp.cy @t130 tptp.cz)) % 62.22/62.44 (define @t318 () (= @t274 (tptp.additive_inverse @t317))) % 62.22/62.44 (define @t319 () (not @t318)) % 62.22/62.44 (define @t320 () (= @t317 @t275)) % 62.22/62.44 (define @t321 () (not @t320)) % 62.22/62.44 (define @t322 () (= @t279 @t258)) % 62.22/62.44 (define @t323 () (not @t322)) % 62.22/62.44 (define @t324 () (tptp.multiply tptp.cy @t56)) % 62.22/62.44 (define @t325 () (tptp.associator tptp.cy @t56 tptp.cx)) % 62.22/62.44 (define @t326 () (= @t325 (tptp.add (tptp.multiply @t324 tptp.cx) (tptp.additive_inverse (tptp.multiply tptp.cy @t143))))) % 62.22/62.44 (define @t327 () (not @t326)) % 62.22/62.44 (define @t328 () (= @t99 (tptp.add (tptp.multiply @t118 tptp.cx) @t219))) % 62.22/62.44 (define @t329 () (not @t328)) % 62.22/62.44 (define @t330 () (not @t153)) % 62.22/62.44 (define @t331 () (not @t149)) % 62.22/62.44 (define @t332 () (not @t146)) % 62.22/62.44 (define @t333 () (not @t142)) % 62.22/62.44 (define @t334 () (tptp.additive_inverse @t84)) % 62.22/62.44 (define @t335 () (tptp.multiply @t334 tptp.cx)) % 62.22/62.44 (define @t336 () (= @t335 @t309)) % 62.22/62.44 (define @t337 () (not @t336)) % 62.22/62.44 (define @t338 () (tptp.add @t139 tptp.cx)) % 62.22/62.44 (define @t339 () (tptp.multiply tptp.cz @t338)) % 62.22/62.44 (define @t340 () (= @t339 @t287)) % 62.22/62.44 (define @t341 () (not @t340)) % 62.22/62.44 (define @t342 () (not @t138)) % 62.22/62.44 (define @t343 () (= @t206 (tptp.multiply @t128 @t334))) % 62.22/62.44 (define @t344 () (not @t343)) % 62.22/62.44 (define @t345 () (tptp.multiply @t133 @t334)) % 62.22/62.44 (define @t346 () (= @t254 @t345)) % 62.22/62.44 (define @t347 () (not @t346)) % 62.22/62.44 (define @t348 () (tptp.additive_inverse @t74)) % 62.22/62.44 (define @t349 () (tptp.multiply tptp.cz @t348)) % 62.22/62.44 (define @t350 () (= (tptp.additive_inverse @t120) @t349)) % 62.22/62.44 (define @t351 () (not @t350)) % 62.22/62.44 (define @t352 () (= (tptp.additive_inverse @t73) @t305)) % 62.22/62.44 (define @t353 () (not @t352)) % 62.22/62.44 (define @t354 () (= @t151 @t295)) % 62.22/62.44 (define @t355 () (not @t354)) % 62.22/62.44 (define @t356 () (= @t127 @t324)) % 62.22/62.44 (define @t357 () (not @t356)) % 62.22/62.44 (define @t358 () (tptp.additive_inverse @t210)) % 62.22/62.44 (define @t359 () (= @t358 (tptp.multiply tptp.cz @t135))) % 62.22/62.44 (define @t360 () (not @t359)) % 62.22/62.44 (define @t361 () (tptp.add @t127 @t129)) % 62.22/62.44 (define @t362 () (tptp.add @t129 @t127)) % 62.22/62.44 (define @t363 () (= @t362 @t361)) % 62.22/62.44 (define @t364 () (not @t363)) % 62.22/62.44 (define @t365 () (not @t124)) % 62.22/62.44 (define @t366 () (= tptp.cx (tptp.add tptp.additive_identity tptp.cx))) % 62.22/62.44 (define @t367 () (not @t366)) % 62.22/62.44 (define @t368 () (= tptp.cx @t334)) % 62.22/62.44 (define @t369 () (not @t368)) % 62.22/62.44 (define @t370 () (= @t40 @t348)) % 62.22/62.44 (define @t371 () (not @t370)) % 62.22/62.44 (define @t372 () (tptp.associator @t56 tptp.cy tptp.cx)) % 62.22/62.44 (define @t373 () (tptp.additive_inverse @t372)) % 62.22/62.44 (define @t374 () (= @t325 @t373)) % 62.22/62.44 (define @t375 () (not @t374)) % 62.22/62.44 (define @t376 () (not @t104)) % 62.22/62.44 (define @t377 () (= @t176 @t362)) % 62.22/62.44 (define @t378 () (not @t377)) % 62.22/62.44 (define @t379 () (tptp.multiply tptp.cy @t144)) % 62.22/62.44 (define @t380 () (= @t95 @t379)) % 62.22/62.44 (define @t381 () (not @t380)) % 62.22/62.44 (define @t382 () (= @t92 @t210)) % 62.22/62.44 (define @t383 () (not @t382)) % 62.22/62.44 (define @t384 () (not @t98)) % 62.22/62.44 (define @t385 () (tptp.additive_inverse @t109)) % 62.22/62.44 (define @t386 () (= @t385 (tptp.add @t88 (tptp.additive_inverse @t59)))) % 62.22/62.44 (define @t387 () (not @t386)) % 62.22/62.44 (define @t388 () (not @t91)) % 62.22/62.44 (define @t389 () (tptp.add @t86 @t80)) % 62.22/62.44 (define @t390 () (= @t389 (tptp.add @t80 @t86))) % 62.22/62.44 (define @t391 () (not @t390)) % 62.22/62.44 (define @t392 () (tptp.add @t84 tptp.cx)) % 62.22/62.44 (define @t393 () (= @t392 @t139)) % 62.22/62.44 (define @t394 () (not @t393)) % 62.22/62.44 (define @t395 () (not @t83)) % 62.22/62.44 (define @t396 () (= @t218 @t234)) % 62.22/62.44 (define @t397 () (not @t396)) % 62.22/62.44 (define @t398 () (tptp.additive_inverse (tptp.associator tptp.cx tptp.cz @t40))) % 62.22/62.44 (define @t399 () (= @t398 @t100)) % 62.22/62.44 (define @t400 () (not @t399)) % 62.22/62.44 (define @t401 () (= @t167 @t176)) % 62.22/62.44 (define @t402 () (not @t401)) % 62.22/62.44 (define @t403 () (tptp.additive_inverse @t57)) % 62.22/62.44 (define @t404 () (tptp.multiply @t79 tptp.cx)) % 62.22/62.44 (define @t405 () (tptp.add @t404 @t403)) % 62.22/62.44 (define @t406 () (= @t372 @t405)) % 62.22/62.44 (define @t407 () (not @t406)) % 62.22/62.44 (define @t408 () (tptp.multiply tptp.cy @t84)) % 62.22/62.44 (define @t409 () (= @t74 @t408)) % 62.22/62.44 (define @t410 () (not @t409)) % 62.22/62.44 (define @t411 () (not @t77)) % 62.22/62.44 (define @t412 () (not @t71)) % 62.22/62.44 (define @t413 () (tptp.add @t67 @t41)) % 62.22/62.44 (define @t414 () (tptp.multiply tptp.cz @t413)) % 62.22/62.44 (define @t415 () (= @t414 @t182)) % 62.22/62.44 (define @t416 () (not @t415)) % 62.22/62.44 (define @t417 () (tptp.add @t63 @t58)) % 62.22/62.44 (define @t418 () (= (tptp.additive_inverse @t417) @t108)) % 62.22/62.44 (define @t419 () (not @t418)) % 62.22/62.44 (define @t420 () (tptp.additive_inverse @t180)) % 62.22/62.44 (define @t421 () (= @t420 @t389)) % 62.22/62.44 (define @t422 () (not @t421)) % 62.22/62.44 (define @t423 () (= tptp.additive_identity (tptp.add @t179 @t66))) % 62.22/62.44 (define @t424 () (not @t423)) % 62.22/62.44 (define @t425 () (= tptp.additive_identity @t195)) % 62.22/62.44 (define @t426 () (not @t425)) % 62.22/62.44 (define @t427 () (= tptp.additive_identity @t392)) % 62.22/62.44 (define @t428 () (not @t427)) % 62.22/62.44 (define @t429 () (tptp.associator @t37 tptp.cy tptp.cx)) % 62.22/62.44 (define @t430 () (tptp.associator tptp.cy @t37 tptp.cx)) % 62.22/62.44 (define @t431 () (= @t430 (tptp.additive_inverse @t429))) % 62.22/62.44 (define @t432 () (not @t431)) % 62.22/62.44 (define @t433 () (= @t166 @t179)) % 62.22/62.44 (define @t434 () (not @t433)) % 62.22/62.44 (define @t435 () (= @t429 (tptp.additive_inverse @t430))) % 62.22/62.44 (define @t436 () (not @t435)) % 62.22/62.44 (define @t437 () (tptp.associator tptp.cz tptp.cx @t40)) % 62.22/62.44 (define @t438 () (= @t437 @t398)) % 62.22/62.44 (define @t439 () (not @t438)) % 62.22/62.44 (define @t440 () (= @t66 @t167)) % 62.22/62.44 (define @t441 () (not @t440)) % 62.22/62.44 (define @t442 () (tptp.add @t58 @t63)) % 62.22/62.44 (define @t443 () (= @t442 @t417)) % 62.22/62.44 (define @t444 () (not @t443)) % 62.22/62.44 (define @t445 () (tptp.add @t38 @t50)) % 62.22/62.44 (define @t446 () (= @t445 @t180)) % 62.22/62.44 (define @t447 () (not @t446)) % 62.22/62.44 (define @t448 () (= @t63 @t181)) % 62.22/62.44 (define @t449 () (not @t448)) % 62.22/62.44 (define @t450 () (not @t62)) % 62.22/62.44 (define @t451 () (not @t53)) % 62.22/62.44 (define @t452 () (tptp.add @t63 @t42)) % 62.22/62.44 (define @t453 () (= tptp.additive_identity @t452)) % 62.22/62.44 (define @t454 () (not @t453)) % 62.22/62.44 (define @t455 () (= tptp.additive_identity @t413)) % 62.22/62.44 (define @t456 () (not @t455)) % 62.22/62.44 (define @t457 () (= @t437 @t442)) % 62.22/62.44 (define @t458 () (not @t457)) % 62.22/62.44 (define @t459 () (= @t429 @t109)) % 62.22/62.44 (define @t460 () (not @t459)) % 62.22/62.44 (define @t461 () (= @t66 @t445)) % 62.22/62.44 (define @t462 () (not @t461)) % 62.22/62.44 (define @t463 () (= tptp.additive_identity @t25)) % 62.22/62.44 (define @t464 () (not @t463)) % 62.22/62.44 (define @t465 () (= @t226 @t228)) % 62.22/62.44 (define @t466 () (not @t465)) % 62.22/62.44 (define @t467 () (tptp.additive_inverse @t437)) % 62.22/62.44 (define @t468 () (tptp.multiply tptp.cz @t408)) % 62.22/62.44 (define @t469 () (tptp.additive_inverse @t468)) % 62.22/62.44 (define @t470 () (tptp.multiply @t158 tptp.cx)) % 62.22/62.44 (define @t471 () (tptp.multiply @t197 @t130)) % 62.22/62.44 (define @t472 () (tptp.additive_inverse @t93)) % 62.22/62.44 (define @t473 () (tptp.multiply tptp.cz @t136)) % 62.22/62.44 (define @t474 () (tptp.multiply tptp.cy @t473)) % 62.22/62.44 (define @t475 () (tptp.additive_inverse @t474)) % 62.22/62.44 (define @t476 () (tptp.multiply @t128 @t136)) % 62.22/62.44 (define @t477 () (tptp.add @t476 @t475)) % 62.22/62.44 (define @t478 () (tptp.multiply @t147 tptp.cx)) % 62.22/62.44 (define @t479 () (tptp.add @t478 @t472)) % 62.22/62.44 (define @t480 () (tptp.add @t408 @t40)) % 62.22/62.44 (define @t481 () (tptp.additive_inverse @t49)) % 62.22/62.44 (define @t482 () (tptp.multiply @t68 tptp.cy)) % 62.22/62.44 (define @t483 () (tptp.add @t482 @t481)) % 62.22/62.44 (define @t484 () (tptp.add @t483 @t66)) % 62.22/62.44 (define @t485 () (tptp.add @t166 @t66)) % 62.22/62.44 (define @t486 () (tptp.add @t127 @t485)) % 62.22/62.44 (define @t487 () (tptp.multiply @t298 tptp.cx)) % 62.22/62.44 (define @t488 () (tptp.multiply @t184 tptp.cx)) % 62.22/62.44 (define @t489 () (tptp.multiply @t488 tptp.cx)) % 62.22/62.44 (define @t490 () (tptp.multiply @t128 @t231)) % 62.22/62.44 (define @t491 () (tptp.additive_inverse @t490)) % 62.22/62.44 (define @t492 () (and @t229 @t230)) % 62.22/62.44 (assume @p1 @t4) % 62.22/62.44 (assume @p2 (forall @t3 (= (tptp.multiply tptp.additive_identity @t1) tptp.additive_identity))) % 62.22/62.44 (assume @p3 (forall @t3 (= (tptp.multiply @t1 tptp.additive_identity) tptp.additive_identity))) % 62.22/62.44 (assume @p4 @t7) % 62.22/62.44 (assume @p5 (forall @t11 (= (tptp.additive_inverse @t10) (tptp.add @t5 @t9)))) % 62.22/62.44 (assume @p6 @t13) % 62.22/62.44 (assume @p7 (forall @t18 (= (tptp.multiply @t1 @t17) (tptp.add @t16 @t15)))) % 62.22/62.44 (assume @p8 (forall @t18 (= (tptp.multiply @t10 @t14) (tptp.add @t15 @t19)))) % 62.22/62.44 (assume @p9 @t20) % 62.22/62.44 (assume @p10 (forall @t11 (= (tptp.multiply (tptp.multiply @t1 @t1) @t8) (tptp.multiply @t1 @t16)))) % 62.22/62.44 (assume @p11 @t22) % 62.22/62.44 (assume @p12 @t24) % 62.22/62.44 (assume @p13 (= @t25 tptp.additive_identity)) % 62.22/62.44 (assume @p14 (forall @t11 (= @t10 (tptp.add @t8 @t1)))) % 62.22/62.44 (assume @p15 (forall @t18 (= (tptp.add @t1 @t17) (tptp.add @t10 @t14)))) % 62.22/62.44 (assume @p16 @t31) % 62.22/62.44 (assume @p17 (forall (@list @t14 @t1 @t8) (or (not (= (tptp.add @t14 @t1) (tptp.add @t14 @t8))) @t26))) % 62.22/62.44 (assume @p18 (forall @t18 (= @t32 (tptp.add (tptp.multiply @t16 @t14) (tptp.additive_inverse (tptp.multiply @t1 @t19)))))) % 62.22/62.44 (assume @p19 (forall (@list @t8 @t1) (= (tptp.multiply (tptp.multiply @t8 @t1) @t8) (tptp.multiply @t8 @t16)))) % 62.22/62.44 (assume @p20 @t34) % 62.22/62.44 (assume @p21 @t36) % 62.22/62.44 (assume @p22 (not (= @t42 @t39))) % 62.22/62.44 (step @p23 :rule symm :premises (@p13)) % 62.22/62.44 (step @p24 :rule instantiate :premises (@p18) :args (@t43)) % 62.22/62.44 (step @p25 :rule instantiate :premises (@p18) :args (@t44)) % 62.22/62.44 (step @p26 :rule instantiate :premises (@p18) :args (@t45)) % 62.22/62.44 (step @p27 :rule eq-symm :args (@t6 tptp.additive_identity)) % 62.22/62.44 (step @p28 :rule cong :premises (@p27) :args (@t7)) % 62.22/62.44 (step @p29 :rule eq_resolve :premises (@p4 @p28)) % 62.22/62.45 (step @p30 :rule instantiate :premises (@p29) :args ((@list @t41))) % 62.22/62.45 (step @p31 :rule instantiate :premises (@p29) :args (@t46)) % 62.22/62.45 (step @p32 :rule eq-symm :args (@t49 @t50)) % 62.22/62.45 (step @p33 :rule refl :args (@t22)) % 62.22/62.45 (step @p34 :rule cong :premises (@p33 @p32) :args ((=> @t22 @t51))) % 62.22/62.45 (assume-push @p931 @t22) % 62.22/62.45 (step @p36 :rule instantiate :premises (@p11) :args (@t52)) % 62.22/62.45 (step-pop @p932 :rule scope :premises (@p36)) % 62.22/62.45 (step @p37 :rule process_scope :premises (@p932) :args (@t51)) % 62.22/62.45 (step @p39 :rule eq_resolve :premises (@p37 @p34)) % 62.22/62.45 (step @p40 :rule implies_elim :premises (@p39)) % 62.22/62.45 (step @p41 :rule chain_m_resolution :premises (@p40 @p11) :args (@t53 @t54 @t55)) % 62.22/62.45 (step @p42 :rule eq-symm :args (@t57 @t59)) % 62.22/62.45 (step @p43 :rule cong :premises (@p33 @p42) :args ((=> @t22 @t60))) % 62.22/62.45 (assume-push @p933 @t22) % 62.22/62.45 (step @p45 :rule instantiate :premises (@p11) :args (@t61)) % 62.22/62.45 (step-pop @p934 :rule scope :premises (@p45)) % 62.22/62.45 (step @p46 :rule process_scope :premises (@p934) :args (@t60)) % 62.22/62.45 (step @p48 :rule eq_resolve :premises (@p46 @p43)) % 62.22/62.45 (step @p49 :rule implies_elim :premises (@p48)) % 62.22/62.45 (step @p50 :rule chain_m_resolution :premises (@p49 @p11) :args (@t62 @t54 @t55)) % 62.22/62.45 (step @p51 :rule eq-symm :args (@t23 @t21)) % 62.22/62.45 (step @p52 :rule cong :premises (@p51) :args (@t24)) % 62.22/62.45 (step @p53 :rule eq_resolve :premises (@p12 @p52)) % 62.22/62.45 (step @p54 :rule instantiate :premises (@p53) :args ((@list tptp.cz @t41))) % 62.22/62.45 (step @p55 :rule instantiate :premises (@p14) :args ((@list @t38 @t50))) % 62.22/62.45 (step @p56 :rule instantiate :premises (@p14) :args ((@list @t58 @t63))) % 62.22/62.45 (step @p57 :rule instantiate :premises (@p20) :args (@t43)) % 62.22/62.45 (step @p58 :rule instantiate :premises (@p20) :args (@t45)) % 62.22/62.45 (step @p59 :rule instantiate :premises (@p20) :args (@t44)) % 62.22/62.45 (step @p60 :rule instantiate :premises (@p20) :args ((@list tptp.cx tptp.cz tptp.cy))) % 62.22/62.45 (step @p61 :rule instantiate :premises (@p20) :args ((@list tptp.cy @t37 tptp.cx))) % 62.22/62.45 (step @p62 :rule instantiate :premises (@p29) :args (@t64)) % 62.22/62.45 (step @p63 :rule instantiate :premises (@p29) :args (@t65)) % 62.22/62.45 (step @p64 :rule instantiate :premises (@p29) :args ((@list @t66))) % 62.22/62.45 (step @p65 :rule instantiate :premises (@p5) :args ((@list @t50 @t38))) % 62.22/62.45 (step @p66 :rule instantiate :premises (@p5) :args ((@list @t63 @t58))) % 62.22/62.45 (step @p67 :rule instantiate :premises (@p7) :args ((@list tptp.cz @t67 @t41))) % 62.22/62.45 (step @p68 :rule eq-symm :args (@t68 @t56)) % 62.22/62.45 (step @p69 :rule cong :premises (@p33 @p68) :args ((=> @t22 @t69))) % 62.22/62.45 (assume-push @p935 @t22) % 62.22/62.45 (step @p71 :rule instantiate :premises (@p11) :args (@t70)) % 62.22/62.45 (step-pop @p936 :rule scope :premises (@p71)) % 62.22/62.45 (step @p72 :rule process_scope :premises (@p936) :args (@t69)) % 62.22/62.45 (step @p74 :rule eq_resolve :premises (@p72 @p69)) % 62.22/62.45 (step @p75 :rule implies_elim :premises (@p74)) % 62.22/62.45 (step @p76 :rule chain_m_resolution :premises (@p75 @p11) :args (@t71 @t54 @t55)) % 62.22/62.45 (step @p77 :rule eq-symm :args (@t73 @t74)) % 62.22/62.45 (step @p78 :rule cong :premises (@p33 @p77) :args ((=> @t22 @t75))) % 62.22/62.45 (assume-push @p937 @t22) % 62.22/62.45 (step @p80 :rule instantiate :premises (@p11) :args (@t76)) % 62.22/62.45 (step-pop @p938 :rule scope :premises (@p80)) % 62.22/62.45 (step @p81 :rule process_scope :premises (@p938) :args (@t75)) % 62.22/62.45 (step @p83 :rule eq_resolve :premises (@p81 @p78)) % 62.22/62.45 (step @p84 :rule implies_elim :premises (@p83)) % 62.22/62.45 (step @p85 :rule chain_m_resolution :premises (@p84 @p11) :args (@t77 @t54 @t55)) % 62.22/62.45 (step @p86 :rule instantiate :premises (@p53) :args (@t76)) % 62.22/62.45 (step @p87 :rule instantiate :premises (@p18) :args ((@list @t56 tptp.cy tptp.cx))) % 62.22/62.45 (step @p88 :rule eq-symm :args (@t35 @t33)) % 62.22/62.45 (step @p89 :rule cong :premises (@p88) :args (@t36)) % 62.22/62.45 (step @p90 :rule eq_resolve :premises (@p21 @p89)) % 62.22/62.45 (step @p91 :rule instantiate :premises (@p90) :args (@t78)) % 62.22/62.45 (step @p92 :rule instantiate :premises (@p90) :args ((@list @t40 tptp.cz tptp.cx))) % 62.22/62.45 (step @p93 :rule instantiate :premises (@p9) :args (@t76)) % 62.22/62.45 (step @p94 :rule eq-symm :args (@t79 @t80)) % 62.22/62.45 (step @p95 :rule cong :premises (@p33 @p94) :args ((=> @t22 @t81))) % 62.22/62.45 (assume-push @p939 @t22) % 62.22/62.45 (step @p97 :rule instantiate :premises (@p11) :args (@t82)) % 62.22/62.45 (step-pop @p940 :rule scope :premises (@p97)) % 62.22/62.45 (step @p98 :rule process_scope :premises (@p940) :args (@t81)) % 62.22/62.45 (step @p100 :rule eq_resolve :premises (@p98 @p95)) % 62.22/62.45 (step @p101 :rule implies_elim :premises (@p100)) % 62.22/62.45 (step @p102 :rule chain_m_resolution :premises (@p101 @p11) :args (@t83 @t54 @t55)) % 62.22/62.45 (step @p103 :rule instantiate :premises (@p14) :args (@t85)) % 62.22/62.45 (step @p104 :rule instantiate :premises (@p14) :args ((@list @t86 @t80))) % 62.22/62.45 (step @p105 :rule eq-symm :args (@t87 @t88)) % 62.22/62.45 (step @p106 :rule cong :premises (@p33 @p105) :args ((=> @t22 @t89))) % 62.22/62.45 (assume-push @p941 @t22) % 62.22/62.45 (step @p108 :rule instantiate :premises (@p11) :args (@t90)) % 62.22/62.45 (step-pop @p942 :rule scope :premises (@p108)) % 62.22/62.45 (step @p109 :rule process_scope :premises (@p942) :args (@t89)) % 62.22/62.45 (step @p111 :rule eq_resolve :premises (@p109 @p106)) % 62.22/62.45 (step @p112 :rule implies_elim :premises (@p111)) % 62.22/62.45 (step @p113 :rule chain_m_resolution :premises (@p112 @p11) :args (@t91 @t54 @t55)) % 62.22/62.45 (step @p114 :rule instantiate :premises (@p5) :args ((@list @t39 @t59))) % 62.22/62.45 (step @p115 :rule eq-symm :args (@t93 @t95)) % 62.22/62.45 (step @p116 :rule cong :premises (@p33 @p115) :args ((=> @t22 @t96))) % 62.22/62.45 (assume-push @p943 @t22) % 62.22/62.45 (step @p118 :rule instantiate :premises (@p11) :args (@t97)) % 62.22/62.45 (step-pop @p944 :rule scope :premises (@p118)) % 62.22/62.45 (step @p119 :rule process_scope :premises (@p944) :args (@t96)) % 62.22/62.45 (step @p121 :rule eq_resolve :premises (@p119 @p116)) % 62.22/62.45 (step @p122 :rule implies_elim :premises (@p121)) % 62.22/62.45 (step @p123 :rule chain_m_resolution :premises (@p122 @p11) :args (@t98 @t54 @t55)) % 62.22/62.45 (step @p124 :rule instantiate :premises (@p9) :args (@t70)) % 62.22/62.45 (step @p125 :rule instantiate :premises (@p53) :args (@t97)) % 62.22/62.45 (step @p126 :rule instantiate :premises (@p18) :args (@t78)) % 62.22/62.45 (step @p127 :rule eq-symm :args (@t99 @t101)) % 62.22/62.45 (step @p128 :rule refl :args (@t34)) % 62.22/62.45 (step @p129 :rule cong :premises (@p128 @p127) :args ((=> @t34 @t102))) % 62.22/62.45 (assume-push @p945 @t34) % 62.22/62.45 (step @p131 :rule instantiate :premises (@p20) :args (@t103)) % 62.22/62.45 (step-pop @p946 :rule scope :premises (@p131)) % 62.22/62.45 (step @p132 :rule process_scope :premises (@p946) :args (@t102)) % 62.22/62.45 (step @p134 :rule eq_resolve :premises (@p132 @p129)) % 62.22/62.45 (step @p135 :rule implies_elim :premises (@p134)) % 62.22/62.45 (step @p136 :rule chain_m_resolution :premises (@p135 @p20) :args (@t104 @t54 @t105)) % 62.22/62.45 (step @p137 :rule instantiate :premises (@p20) :args (@t106)) % 62.22/62.45 (step @p138 :rule refl :args (@t26)) % 62.22/62.45 (step @p139 :rule eq-symm :args (@t27 @t17)) % 62.22/62.45 (step @p140 :rule cong :premises (@p139) :args (@t28)) % 62.22/62.45 (step @p141 :rule nary_cong :premises (@p140 @p138) :args (@t29)) % 62.22/62.45 (step @p142 :rule cong :premises (@p141) :args (@t31)) % 62.22/62.45 (step @p143 :rule eq_resolve :premises (@p16 @p142)) % 62.22/62.45 (step @p144 :rule eq-symm :args (@t107 @t39)) % 62.22/62.45 (step @p145 :rule refl :args (@t111)) % 62.22/62.45 (step @p146 :rule nary_cong :premises (@p145 @p144) :args (@t113)) % 62.22/62.45 (step @p147 :rule refl :args (@t114)) % 62.22/62.45 (step @p148 :rule cong :premises (@p147 @p146) :args ((=> @t114 @t113))) % 62.22/62.45 (assume-push @p947 @t114) % 62.22/62.45 (step @p150 :rule instantiate :premises (@p143) :args ((@list @t107 @t59 @t39))) % 62.22/62.45 (step-pop @p948 :rule scope :premises (@p150)) % 62.22/62.45 (step @p151 :rule process_scope :premises (@p948) :args (@t113)) % 62.22/62.45 (step @p153 :rule eq_resolve :premises (@p151 @p148)) % 62.22/62.45 (step @p154 :rule implies_elim :premises (@p153)) % 62.22/62.45 (step @p155 :rule chain_m_resolution :premises (@p154 @p143) :args (@t116 @t54 @t117)) % 62.22/62.45 (step @p156 :rule bool-eq-false :args (@t115)) % 62.22/62.45 (step @p157 :rule symm :premises (@p156)) % 62.22/62.45 (step @p158 :rule cong :premises (@p144) :args ((not @t112))) % 62.22/62.45 (step @p159 :rule bool-eq-false :args (@t112)) % 62.22/62.45 (step @p160 :rule trans :premises (@p159 @p158)) % 62.22/62.45 (step @p161 :rule trans :premises (@p160 @p157)) % 62.22/62.45 (step @p162 :rule false_intro :premises (@p22)) % 62.22/62.45 (step @p163 :rule refl :args (@t39)) % 62.22/62.45 (step @p164 :rule eq-symm :args (@t12 @t1)) % 62.22/62.45 (step @p165 :rule cong :premises (@p164) :args (@t13)) % 62.22/62.45 (step @p166 :rule eq_resolve :premises (@p6 @p165)) % 62.22/62.45 (step @p167 :rule instantiate :premises (@p166) :args (@t46)) % 62.22/62.45 (step @p168 :rule symm :premises (@p167)) % 62.22/62.45 (step @p169 :rule cong :premises (@p168 @p163) :args (@t112)) % 62.22/62.45 (step @p170 :rule trans :premises (@p169 @p162)) % 62.22/62.45 (step @p171 :rule eq_resolve :premises (@p170 @p161)) % 62.22/62.45 (step @p172 :rule false_elim :premises (@p171)) % 62.22/62.45 (step @p173 :rule cnf_or_pos :args (@t116)) % 62.22/62.45 (step @p174 :rule reordering :premises (@p173) :args ((or @t111 @t115 (not @t116)))) % 62.22/62.45 (step @p175 :rule chain_m_resolution :premises (@p174 @p172 @p155) :args (@t111 (@list true false) (@list @t115 @t116))) % 62.22/62.45 (step @p176 :rule instantiate :premises (@p166) :args (@t65)) % 62.22/62.45 (step @p177 :rule instantiate :premises (@p166) :args (@t64)) % 62.22/62.45 (step @p178 :rule eq-symm :args (@t2 @t1)) % 62.22/62.45 (step @p179 :rule cong :premises (@p178) :args (@t4)) % 62.22/62.45 (step @p180 :rule eq_resolve :premises (@p1 @p179)) % 62.22/62.45 (step @p181 :rule instantiate :premises (@p180) :args (@t64)) % 62.22/62.45 (step @p182 :rule eq-symm :args (@t119 @t120)) % 62.22/62.45 (step @p183 :rule refl :args (@t121)) % 62.22/62.45 (step @p184 :rule cong :premises (@p183 @p182) :args ((=> @t121 @t122))) % 62.22/62.45 (assume-push @p949 @t121) % 62.22/62.45 (step @p186 :rule instantiate :premises (@p53) :args (@t123)) % 62.22/62.45 (step-pop @p950 :rule scope :premises (@p186)) % 62.22/62.45 (step @p187 :rule process_scope :premises (@p950) :args (@t122)) % 62.22/62.45 (step @p189 :rule eq_resolve :premises (@p187 @p184)) % 62.22/62.45 (step @p190 :rule implies_elim :premises (@p189)) % 62.22/62.45 (step @p191 :rule chain_m_resolution :premises (@p190 @p53) :args (@t124 @t54 @t125)) % 62.22/62.45 (step @p192 :rule instantiate :premises (@p14) :args ((@list @t129 @t127))) % 62.22/62.45 (step @p193 :rule instantiate :premises (@p53) :args ((@list tptp.cz @t130))) % 62.22/62.45 (step @p194 :rule instantiate :premises (@p53) :args (@t131)) % 62.22/62.45 (step @p195 :rule instantiate :premises (@p53) :args (@t132)) % 62.22/62.45 (step @p196 :rule instantiate :premises (@p53) :args ((@list @t72 tptp.cx))) % 62.22/62.45 (step @p197 :rule instantiate :premises (@p53) :args ((@list tptp.cz @t74))) % 62.22/62.45 (step @p198 :rule instantiate :premises (@p53) :args (@t134)) % 62.22/62.45 (step @p199 :rule instantiate :premises (@p53) :args ((@list @t128 @t84))) % 62.22/62.45 (step @p200 :rule eq-symm :args (@t135 @t136)) % 62.22/62.45 (step @p201 :rule cong :premises (@p183 @p200) :args ((=> @t121 @t137))) % 62.22/62.45 (assume-push @p951 @t121) % 62.22/62.45 (step @p203 :rule instantiate :premises (@p53) :args ((@list tptp.cx tptp.cx))) % 62.22/62.45 (step-pop @p952 :rule scope :premises (@p203)) % 62.22/62.45 (step @p204 :rule process_scope :premises (@p952) :args (@t137)) % 62.22/62.45 (step @p206 :rule eq_resolve :premises (@p204 @p201)) % 62.22/62.45 (step @p207 :rule implies_elim :premises (@p206)) % 62.22/62.45 (step @p208 :rule chain_m_resolution :premises (@p207 @p53) :args (@t138 @t54 @t125)) % 62.22/62.45 (step @p209 :rule instantiate :premises (@p7) :args ((@list tptp.cz @t139 tptp.cx))) % 62.22/62.45 (step @p210 :rule instantiate :premises (@p11) :args (@t85)) % 62.22/62.45 (step @p211 :rule eq-symm :args (@t140 @t119)) % 62.22/62.45 (step @p212 :rule cong :premises (@p33 @p211) :args ((=> @t22 @t141))) % 62.22/62.45 (assume-push @p953 @t22) % 62.22/62.45 (step @p214 :rule instantiate :premises (@p11) :args (@t123)) % 62.22/62.45 (step-pop @p954 :rule scope :premises (@p214)) % 62.22/62.45 (step @p215 :rule process_scope :premises (@p954) :args (@t141)) % 62.22/62.45 (step @p217 :rule eq_resolve :premises (@p215 @p212)) % 62.22/62.45 (step @p218 :rule implies_elim :premises (@p217)) % 62.22/62.45 (step @p219 :rule chain_m_resolution :premises (@p218 @p11) :args (@t142 @t54 @t55)) % 62.22/62.45 (step @p220 :rule eq-symm :args (@t143 @t144)) % 62.22/62.45 (step @p221 :rule cong :premises (@p33 @p220) :args ((=> @t22 @t145))) % 62.22/62.45 (assume-push @p955 @t22) % 62.22/62.45 (step @p223 :rule instantiate :premises (@p11) :args ((@list @t37 tptp.cx))) % 62.22/62.45 (step-pop @p956 :rule scope :premises (@p223)) % 62.22/62.45 (step @p224 :rule process_scope :premises (@p956) :args (@t145)) % 62.22/62.45 (step @p226 :rule eq_resolve :premises (@p224 @p221)) % 62.22/62.45 (step @p227 :rule implies_elim :premises (@p226)) % 62.22/62.45 (step @p228 :rule chain_m_resolution :premises (@p227 @p11) :args (@t146 @t54 @t55)) % 62.22/62.45 (step @p229 :rule eq-symm :args (@t147 @t127)) % 62.22/62.45 (step @p230 :rule cong :premises (@p33 @p229) :args ((=> @t22 @t148))) % 62.22/62.45 (assume-push @p957 @t22) % 62.22/62.45 (step @p232 :rule instantiate :premises (@p11) :args (@t131)) % 62.22/62.45 (step-pop @p958 :rule scope :premises (@p232)) % 62.22/62.45 (step @p233 :rule process_scope :premises (@p958) :args (@t148)) % 62.22/62.45 (step @p235 :rule eq_resolve :premises (@p233 @p230)) % 62.22/62.45 (step @p236 :rule implies_elim :premises (@p235)) % 62.22/62.45 (step @p237 :rule chain_m_resolution :premises (@p236 @p11) :args (@t149 @t54 @t55)) % 62.22/62.45 (step @p238 :rule eq-symm :args (@t150 @t151)) % 62.22/62.45 (step @p239 :rule cong :premises (@p33 @p238) :args ((=> @t22 @t152))) % 62.22/62.45 (assume-push @p959 @t22) % 62.22/62.45 (step @p241 :rule instantiate :premises (@p11) :args (@t132)) % 62.22/62.45 (step-pop @p960 :rule scope :premises (@p241)) % 62.22/62.45 (step @p242 :rule process_scope :premises (@p960) :args (@t152)) % 62.22/62.45 (step @p244 :rule eq_resolve :premises (@p242 @p239)) % 62.22/62.45 (step @p245 :rule implies_elim :premises (@p244)) % 62.22/62.45 (step @p246 :rule chain_m_resolution :premises (@p245 @p11) :args (@t153 @t54 @t55)) % 62.22/62.45 (step @p247 :rule instantiate :premises (@p18) :args (@t103)) % 62.22/62.45 (step @p248 :rule instantiate :premises (@p18) :args (@t106)) % 62.22/62.45 (step @p249 :rule instantiate :premises (@p18) :args (@t154)) % 62.22/62.45 (step @p250 :rule instantiate :premises (@p20) :args ((@list tptp.cy @t130 tptp.cz))) % 62.22/62.45 (step @p251 :rule instantiate :premises (@p20) :args ((@list @t130 tptp.cy tptp.cz))) % 62.22/62.45 (step @p252 :rule instantiate :premises (@p53) :args (@t155)) % 62.22/62.45 (step @p253 :rule instantiate :premises (@p53) :args (@t156)) % 62.22/62.45 (step @p254 :rule eq-symm :args (@t157 @t158)) % 62.22/62.45 (step @p255 :rule cong :premises (@p183 @p254) :args ((=> @t121 @t159))) % 62.22/62.45 (assume-push @p961 @t121) % 62.22/62.45 (step @p257 :rule instantiate :premises (@p53) :args ((@list @t48 @t40))) % 62.22/62.45 (step-pop @p962 :rule scope :premises (@p257)) % 62.22/62.45 (step @p258 :rule process_scope :premises (@p962) :args (@t159)) % 62.22/62.45 (step @p260 :rule eq_resolve :premises (@p258 @p255)) % 62.22/62.45 (step @p261 :rule implies_elim :premises (@p260)) % 62.22/62.45 (step @p262 :rule chain_m_resolution :premises (@p261 @p53) :args (@t160 @t54 @t125)) % 62.22/62.45 (step @p263 :rule instantiate :premises (@p53) :args (@t85)) % 62.22/62.45 (step @p264 :rule instantiate :premises (@p7) :args ((@list @t72 tptp.cx @t84))) % 62.22/62.45 (step @p265 :rule instantiate :premises (@p166) :args ((@list tptp.cy))) % 62.22/62.45 (step @p266 :rule eq-symm :args (@t161 @t162)) % 62.22/62.45 (step @p267 :rule cong :premises (@p33 @p266) :args ((=> @t22 @t163))) % 62.22/62.45 (assume-push @p963 @t22) % 62.22/62.45 (step @p269 :rule instantiate :premises (@p11) :args (@t155)) % 62.22/62.45 (step-pop @p964 :rule scope :premises (@p269)) % 62.22/62.45 (step @p270 :rule process_scope :premises (@p964) :args (@t163)) % 62.22/62.45 (step @p272 :rule eq_resolve :premises (@p270 @p267)) % 62.22/62.45 (step @p273 :rule implies_elim :premises (@p272)) % 62.22/62.45 (step @p274 :rule chain_m_resolution :premises (@p273 @p11) :args (@t164 @t54 @t55)) % 62.22/62.45 (step @p275 :rule eq-symm :args (@t168 @t118)) % 62.22/62.45 (step @p276 :rule refl :args (@t170)) % 62.22/62.45 (step @p277 :rule nary_cong :premises (@p276 @p275) :args (@t171)) % 62.22/62.45 (step @p278 :rule cong :premises (@p147 @p277) :args ((=> @t114 @t171))) % 62.22/62.45 (assume-push @p965 @t114) % 62.22/62.45 (step @p280 :rule instantiate :premises (@p143) :args ((@list @t168 @t120 @t118))) % 62.22/62.45 (step-pop @p966 :rule scope :premises (@p280)) % 62.22/62.45 (step @p281 :rule process_scope :premises (@p966) :args (@t171)) % 62.22/62.45 (step @p283 :rule eq_resolve :premises (@p281 @p278)) % 62.22/62.45 (step @p284 :rule implies_elim :premises (@p283)) % 62.22/62.45 (step @p285 :rule chain_m_resolution :premises (@p284 @p143) :args (@t173 @t54 @t117)) % 62.22/62.45 (step @p186 :rule instantiate :premises (@p53) :args (@t123)) % 62.22/62.45 (step @p286 :rule refl :args (@t168)) % 62.22/62.45 (step @p287 :rule cong :premises (@p286 @p186) :args ((tptp.add @t168 @t119))) % 62.22/62.45 (step @p288 :rule instantiate :premises (@p15) :args ((@list @t167 @t165 @t119))) % 62.22/62.45 (step @p289 :rule instantiate :premises (@p18) :args (@t174)) % 62.22/62.45 (step @p290 :rule eq-symm :args (@t175 @t177)) % 62.22/62.45 (step @p291 :rule cong :premises (@p128 @p290) :args ((=> @t34 @t178))) % 62.22/62.45 (assume-push @p967 @t34) % 62.22/62.45 (step @p293 :rule instantiate :premises (@p20) :args (@t174)) % 62.22/62.45 (step-pop @p968 :rule scope :premises (@p293)) % 62.22/62.45 (step @p294 :rule process_scope :premises (@p968) :args (@t178)) % 62.22/62.45 (step @p296 :rule eq_resolve :premises (@p294 @p291)) % 62.22/62.45 (step @p297 :rule implies_elim :premises (@p296)) % 62.22/62.45 (step @p298 :rule chain_m_resolution :premises (@p297 @p20) :args ((= @t177 @t175) @t54 @t105)) % 62.22/62.45 (step @p299 :rule trans :premises (@p57 @p91)) % 62.22/62.45 (step @p300 :rule cong :premises (@p299) :args (@t179)) % 62.22/62.45 (step @p301 :rule trans :premises (@p60 @p300 @p298 @p289)) % 62.22/62.45 (step @p302 :rule symm :premises (@p24)) % 62.22/62.45 (step @p303 :rule symm :premises (@p55)) % 62.22/62.45 (step @p304 :rule trans :premises (@p303 @p302 @p57)) % 62.22/62.45 (step @p305 :rule cong :premises (@p304 @p301) :args ((tptp.add @t180 @t166))) % 62.22/62.45 (step @p306 :rule refl :args (@t166)) % 62.22/62.45 (step @p307 :rule symm :premises (@p304)) % 62.22/62.45 (step @p308 :rule cong :premises (@p307 @p306) :args ((tptp.add @t167 @t166))) % 62.22/62.45 (step @p309 :rule instantiate :premises (@p29) :args ((@list @t166))) % 62.22/62.45 (step @p310 :rule symm :premises (@p31)) % 62.22/62.45 (step @p311 :rule refl :args (@t42)) % 62.22/62.45 (step @p312 :rule symm :premises (@p54)) % 62.22/62.45 (step @p313 :rule cong :premises (@p312 @p311) :args (@t182)) % 62.22/62.45 (step @p314 :rule symm :premises (@p63)) % 62.22/62.45 (step @p315 :rule instantiate :premises (@p14) :args ((@list @t74 @t40))) % 62.22/62.45 (step @p316 :rule symm :premises (@p315)) % 62.22/62.45 (step @p317 :rule trans :premises (@p316 @p314 @p30)) % 62.22/62.45 (step @p318 :rule refl :args (tptp.cz)) % 62.22/62.45 (step @p319 :rule cong :premises (@p318 @p317) :args ((tptp.multiply tptp.cz (tptp.add @t40 @t74)))) % 62.22/62.45 (step @p320 :rule instantiate :premises (@p7) :args ((@list tptp.cz @t40 @t74))) % 62.22/62.45 (step @p321 :rule symm :premises (@p320)) % 62.22/62.45 (step @p322 :rule trans :premises (@p321 @p319 @p67 @p313 @p310 @p309 @p308 @p305 @p288 @p287)) % 62.22/62.45 (step @p323 :rule cnf_or_pos :args (@t173)) % 62.22/62.45 (step @p324 :rule reordering :premises (@p323) :args ((or @t172 @t170 (not @t173)))) % 62.22/62.45 (step @p325 :rule chain_m_resolution :premises (@p324 @p322 @p285) :args (@t172 (@list false false) (@list @t169 @t173))) % 62.22/62.45 (step @p326 :rule instantiate :premises (@p53) :args (@t183)) % 62.22/62.45 (step @p327 :rule instantiate :premises (@p53) :args ((@list tptp.cz @t72))) % 62.22/62.45 (step @p328 :rule eq-symm :args (@t184 @t185)) % 62.22/62.45 (step @p329 :rule cong :premises (@p33 @p328) :args ((=> @t22 @t186))) % 62.22/62.45 (assume-push @p969 @t22) % 62.22/62.45 (step @p331 :rule instantiate :premises (@p11) :args (@t183)) % 62.22/62.45 (step-pop @p970 :rule scope :premises (@p331)) % 62.22/62.45 (step @p332 :rule process_scope :premises (@p970) :args (@t186)) % 62.22/62.45 (step @p334 :rule eq_resolve :premises (@p332 @p329)) % 62.22/62.45 (step @p335 :rule implies_elim :premises (@p334)) % 62.22/62.45 (step @p336 :rule chain_m_resolution :premises (@p335 @p11) :args (@t187 @t54 @t55)) % 62.22/62.45 (step @p337 :rule eq-symm :args (@t188 @t189)) % 62.22/62.45 (step @p338 :rule cong :premises (@p33 @p337) :args ((=> @t22 @t190))) % 62.22/62.45 (assume-push @p971 @t22) % 62.22/62.45 (step @p340 :rule instantiate :premises (@p11) :args (@t156)) % 62.22/62.45 (step-pop @p972 :rule scope :premises (@p340)) % 62.22/62.45 (step @p341 :rule process_scope :premises (@p972) :args (@t190)) % 62.22/62.45 (step @p343 :rule eq_resolve :premises (@p341 @p338)) % 62.22/62.45 (step @p344 :rule implies_elim :premises (@p343)) % 62.22/62.45 (step @p345 :rule chain_m_resolution :premises (@p344 @p11) :args (@t191 @t54 @t55)) % 62.22/62.45 (step @p346 :rule instantiate :premises (@p7) :args ((@list @t72 @t192 @t37))) % 62.22/62.45 (step @p347 :rule instantiate :premises (@p8) :args ((@list @t167 @t165 tptp.cx))) % 62.22/62.45 (step @p348 :rule instantiate :premises (@p29) :args ((@list @t193))) % 62.22/62.45 (step @p349 :rule instantiate :premises (@p20) :args (@t154)) % 62.22/62.45 (step @p350 :rule instantiate :premises (@p90) :args (@t194)) % 62.22/62.45 (step @p351 :rule instantiate :premises (@p14) :args ((@list @t195 @t127))) % 62.22/62.45 (step @p352 :rule eq-symm :args (@t196 @t197)) % 62.22/62.45 (step @p353 :rule cong :premises (@p183 @p352) :args ((=> @t121 @t198))) % 62.22/62.45 (assume-push @p973 @t121) % 62.22/62.45 (step @p355 :rule instantiate :premises (@p53) :args ((@list @t48 tptp.cy))) % 62.22/62.45 (step-pop @p974 :rule scope :premises (@p355)) % 62.22/62.45 (step @p356 :rule process_scope :premises (@p974) :args (@t198)) % 62.22/62.45 (step @p358 :rule eq_resolve :premises (@p356 @p353)) % 62.22/62.45 (step @p359 :rule implies_elim :premises (@p358)) % 62.22/62.45 (step @p360 :rule chain_m_resolution :premises (@p359 @p53) :args (@t199 @t54 @t125)) % 62.22/62.45 (step @p361 :rule instantiate :premises (@p53) :args (@t200)) % 62.22/62.45 (step @p362 :rule eq-symm :args (@t201 @t203)) % 62.22/62.45 (step @p363 :rule cong :premises (@p33 @p362) :args ((=> @t22 @t204))) % 62.22/62.45 (assume-push @p975 @t22) % 62.22/62.45 (step @p365 :rule instantiate :premises (@p11) :args (@t200)) % 62.22/62.45 (step-pop @p976 :rule scope :premises (@p365)) % 62.22/62.45 (step @p366 :rule process_scope :premises (@p976) :args (@t204)) % 62.22/62.45 (step @p368 :rule eq_resolve :premises (@p366 @p363)) % 62.22/62.45 (step @p369 :rule implies_elim :premises (@p368)) % 62.22/62.45 (step @p370 :rule chain_m_resolution :premises (@p369 @p11) :args (@t205 @t54 @t55)) % 62.22/62.45 (step @p371 :rule instantiate :premises (@p15) :args ((@list @t127 @t206 @t193))) % 62.22/62.45 (step @p372 :rule eq-symm :args (@t207 @t202)) % 62.22/62.45 (step @p373 :rule refl :args (@t20)) % 62.22/62.45 (step @p374 :rule cong :premises (@p373 @p372) :args ((=> @t20 @t208))) % 62.22/62.45 (assume-push @p977 @t20) % 62.22/62.45 (step @p376 :rule instantiate :premises (@p9) :args (@t156)) % 62.22/62.45 (step-pop @p978 :rule scope :premises (@p376)) % 62.22/62.45 (step @p377 :rule process_scope :premises (@p978) :args (@t208)) % 62.22/62.45 (step @p379 :rule eq_resolve :premises (@p377 @p374)) % 62.22/62.45 (step @p380 :rule implies_elim :premises (@p379)) % 62.22/62.45 (step @p381 :rule chain_m_resolution :premises (@p380 @p9) :args (@t209 @t54 (@list @t20))) % 62.22/62.45 (step @p382 :rule instantiate :premises (@p5) :args ((@list @t202 @t211))) % 62.22/62.45 (step @p383 :rule instantiate :premises (@p11) :args (@t213)) % 62.22/62.45 (step @p384 :rule instantiate :premises (@p11) :args ((@list @t129 tptp.cx))) % 62.22/62.45 (step @p385 :rule eq-symm :args (@t214 @t215)) % 62.22/62.45 (step @p386 :rule cong :premises (@p183 @p385) :args ((=> @t121 @t216))) % 62.22/62.45 (assume-push @p979 @t121) % 62.22/62.45 (step @p388 :rule instantiate :premises (@p53) :args (@t213)) % 62.22/62.45 (step-pop @p980 :rule scope :premises (@p388)) % 62.22/62.45 (step @p389 :rule process_scope :premises (@p980) :args (@t216)) % 62.22/62.45 (step @p391 :rule eq_resolve :premises (@p389 @p386)) % 62.22/62.45 (step @p392 :rule implies_elim :premises (@p391)) % 62.22/62.45 (step @p393 :rule chain_m_resolution :premises (@p392 @p53) :args (@t217 @t54 @t125)) % 62.22/62.45 (step @p394 :rule instantiate :premises (@p8) :args ((@list @t66 @t193 tptp.cx))) % 62.22/62.45 (step @p395 :rule instantiate :premises (@p15) :args ((@list @t221 @t220 @t219))) % 62.22/62.45 (step @p396 :rule instantiate :premises (@p18) :args (@t194)) % 62.22/62.45 (step @p397 :rule instantiate :premises (@p9) :args (@t134)) % 62.22/62.45 (step @p398 :rule instantiate :premises (@p15) :args ((@list @t221 @t224 @t223))) % 62.22/62.45 (step @p399 :rule refl :args (@t230)) % 62.22/62.45 (step @p400 :rule refl :args (@t233)) % 62.22/62.45 (step @p401 :rule refl :args (@t241)) % 62.22/62.45 (step @p402 :rule refl :args (@t245)) % 62.22/62.45 (step @p403 :rule refl :args (@t249)) % 62.22/62.45 (step @p404 :rule refl :args (@t250)) % 62.22/62.45 (step @p405 :rule refl :args (@t253)) % 62.22/62.45 (step @p406 :rule refl :args (@t257)) % 62.22/62.45 (step @p407 :rule refl :args (@t261)) % 62.22/62.45 (step @p408 :rule refl :args (@t262)) % 62.22/62.45 (step @p409 :rule refl :args (@t266)) % 62.22/62.45 (step @p410 :rule refl :args (@t267)) % 62.22/62.45 (step @p411 :rule refl :args (@t269)) % 62.22/62.45 (step @p412 :rule refl :args (@t270)) % 62.22/62.45 (step @p413 :rule refl :args (@t273)) % 62.22/62.45 (step @p414 :rule refl :args (@t277)) % 62.22/62.45 (step @p415 :rule refl :args (@t281)) % 62.22/62.45 (step @p416 :rule refl :args (@t283)) % 62.22/62.45 (step @p417 :rule refl :args (@t286)) % 62.22/62.45 (step @p418 :rule refl :args (@t290)) % 62.22/62.45 (step @p419 :rule refl :args (@t291)) % 62.22/62.45 (step @p420 :rule refl :args (@t292)) % 62.22/62.45 (step @p421 :rule refl :args (@t297)) % 62.22/62.45 (step @p422 :rule refl :args (@t300)) % 62.22/62.45 (step @p423 :rule refl :args (@t301)) % 62.22/62.45 (step @p424 :rule refl :args (@t302)) % 62.22/62.45 (step @p425 :rule refl :args (@t304)) % 62.22/62.45 (step @p426 :rule refl :args (@t308)) % 62.22/62.45 (step @p427 :rule refl :args (@t311)) % 62.22/62.45 (step @p428 :rule refl :args (@t312)) % 62.22/62.45 (step @p429 :rule refl :args (@t314)) % 62.22/62.45 (step @p430 :rule refl :args (@t316)) % 62.22/62.45 (step @p431 :rule refl :args (@t319)) % 62.22/62.45 (step @p432 :rule refl :args (@t321)) % 62.22/62.45 (step @p433 :rule refl :args (@t323)) % 62.22/62.45 (step @p434 :rule refl :args (@t327)) % 62.22/62.45 (step @p435 :rule refl :args (@t329)) % 62.22/62.45 (step @p436 :rule refl :args (@t330)) % 62.22/62.45 (step @p437 :rule refl :args (@t331)) % 62.22/62.45 (step @p438 :rule refl :args (@t332)) % 62.22/62.45 (step @p439 :rule refl :args (@t333)) % 62.22/62.45 (step @p440 :rule refl :args (@t337)) % 62.22/62.45 (step @p441 :rule refl :args (@t341)) % 62.22/62.45 (step @p442 :rule refl :args (@t342)) % 62.22/62.45 (step @p443 :rule refl :args (@t344)) % 62.22/62.45 (step @p444 :rule refl :args (@t347)) % 62.22/62.45 (step @p445 :rule refl :args (@t351)) % 62.22/62.45 (step @p446 :rule refl :args (@t353)) % 62.22/62.45 (step @p447 :rule refl :args (@t355)) % 62.22/62.45 (step @p448 :rule refl :args (@t357)) % 62.22/62.45 (step @p449 :rule refl :args (@t360)) % 62.22/62.45 (step @p450 :rule refl :args (@t364)) % 62.22/62.45 (step @p451 :rule refl :args (@t365)) % 62.22/62.45 (step @p452 :rule refl :args (@t367)) % 62.22/62.45 (step @p453 :rule refl :args (@t369)) % 62.22/62.45 (step @p454 :rule refl :args (@t371)) % 62.22/62.45 (step @p455 :rule refl :args (@t375)) % 62.22/62.45 (step @p456 :rule refl :args (@t376)) % 62.22/62.45 (step @p457 :rule refl :args (@t378)) % 62.22/62.45 (step @p458 :rule refl :args (@t381)) % 62.22/62.45 (step @p459 :rule refl :args (@t383)) % 62.22/62.45 (step @p460 :rule bool-double-not-elim :args (@t110)) % 62.22/62.45 (step @p461 :rule refl :args (@t384)) % 62.22/62.45 (step @p462 :rule refl :args (@t387)) % 62.22/62.45 (step @p463 :rule refl :args (@t388)) % 62.22/62.45 (step @p464 :rule refl :args (@t391)) % 62.22/62.45 (step @p465 :rule refl :args (@t394)) % 62.22/62.45 (step @p466 :rule refl :args (@t395)) % 62.22/62.45 (step @p467 :rule refl :args (@t397)) % 62.22/62.45 (step @p468 :rule refl :args (@t400)) % 62.22/62.45 (step @p469 :rule refl :args (@t402)) % 62.22/62.45 (step @p470 :rule refl :args (@t407)) % 62.22/62.45 (step @p471 :rule refl :args (@t410)) % 62.22/62.45 (step @p472 :rule refl :args (@t411)) % 62.22/62.45 (step @p473 :rule refl :args (@t412)) % 62.22/62.45 (step @p474 :rule refl :args (@t416)) % 62.22/62.45 (step @p475 :rule refl :args (@t419)) % 62.22/62.45 (step @p476 :rule refl :args (@t422)) % 62.22/62.45 (step @p477 :rule refl :args (@t424)) % 62.22/62.45 (step @p478 :rule refl :args (@t426)) % 62.22/62.45 (step @p479 :rule refl :args (@t428)) % 62.22/62.45 (step @p480 :rule refl :args (@t432)) % 62.22/62.45 (step @p481 :rule refl :args (@t434)) % 62.22/62.45 (step @p482 :rule refl :args (@t436)) % 62.22/62.45 (step @p483 :rule refl :args (@t439)) % 62.22/62.45 (step @p484 :rule refl :args (@t441)) % 62.22/62.45 (step @p485 :rule refl :args (@t444)) % 62.22/62.45 (step @p486 :rule refl :args (@t447)) % 62.22/62.45 (step @p487 :rule refl :args (@t449)) % 62.22/62.45 (step @p488 :rule refl :args (@t450)) % 62.22/62.45 (step @p489 :rule refl :args (@t451)) % 62.22/62.45 (step @p490 :rule refl :args (@t454)) % 62.22/62.45 (step @p491 :rule refl :args (@t456)) % 62.22/62.45 (step @p492 :rule refl :args (@t458)) % 62.22/62.45 (step @p493 :rule refl :args (@t460)) % 62.22/62.45 (step @p494 :rule refl :args (@t462)) % 62.22/62.45 (step @p495 :rule refl :args (@t464)) % 62.22/62.45 (step @p496 :rule nary_cong :premises (@p495 @p494 @p493 @p492 @p491 @p490 @p489 @p488 @p487 @p486 @p485 @p484 @p483 @p482 @p481 @p480 @p479 @p478 @p477 @p476 @p475 @p474 @p473 @p472 @p471 @p470 @p469 @p468 @p467 @p466 @p465 @p464 @p463 @p462 @p461 @p460 @p459 @p458 @p457 @p456 @p455 @p454 @p453 @p452 @p451 @p450 @p449 @p448 @p447 @p446 @p445 @p444 @p443 @p442 @p441 @p440 @p439 @p438 @p437 @p436 @p435 @p434 @p433 @p432 @p431 @p430 @p429 @p428 @p427 @p426 @p425 @p424 @p423 @p422 @p421 @p420 @p419 @p418 @p417 @p416 @p415 @p414 @p413 @p412 @p411 @p410 @p409 @p408 @p407 @p406 @p405 @p404 @p403 @p402 @p401 @p400 @p399) :args ((or @t464 @t462 @t460 @t458 @t456 @t454 @t451 @t450 @t449 @t447 @t444 @t441 @t439 @t436 @t434 @t432 @t428 @t426 @t424 @t422 @t419 @t416 @t412 @t411 @t410 @t407 @t402 @t400 @t397 @t395 @t394 @t391 @t388 @t387 @t384 (not @t111) @t383 @t381 @t378 @t376 @t375 @t371 @t369 @t367 @t365 @t364 @t360 @t357 @t355 @t353 @t351 @t347 @t344 @t342 @t341 @t337 @t333 @t332 @t331 @t330 @t329 @t327 @t323 @t321 @t319 @t316 @t314 @t312 @t311 @t308 @t304 @t302 @t301 @t300 @t297 @t292 @t291 @t290 @t286 @t283 @t281 @t277 @t273 @t270 @t269 @t267 @t266 @t262 @t261 @t257 @t253 @t250 @t249 @t245 @t241 @t233 @t230))) % 62.22/62.45 (assume-push @p981 @t229) % 62.22/62.45 (assume-push @p982 @t230) % 62.22/62.45 (step @p499 :rule evaluate :args ((= false true))) % 62.22/62.45 (step @p500 :rule true_intro :premises (@p398)) % 62.22/62.45 (step @p501 :rule bool-eq-false :args (@t229)) % 62.22/62.45 (step @p502 :rule symm :premises (@p501)) % 62.22/62.45 (step @p503 :rule eq-symm :args (@t226 @t228)) % 62.22/62.45 (step @p504 :rule cong :premises (@p503) :args (@t466)) % 62.22/62.45 (step @p505 :rule bool-eq-false :args (@t465)) % 62.22/62.45 (step @p506 :rule trans :premises (@p505 @p504)) % 62.22/62.45 (step @p507 :rule trans :premises (@p506 @p502)) % 62.22/62.45 (step @p508 :rule false_intro :premises (@p175)) % 62.22/62.45 (step @p509 :rule trans :premises (@p26 @p56)) % 62.22/62.45 (step @p510 :rule cong :premises (@p509) :args (@t467)) % 62.22/62.45 (step @p511 :rule symm :premises (@p58)) % 62.22/62.45 (step @p512 :rule symm :premises (@p92)) % 62.22/62.45 (step @p513 :rule trans :premises (@p512 @p511)) % 62.22/62.45 (step @p514 :rule cong :premises (@p513) :args (@t101)) % 62.22/62.45 (step @p131 :rule instantiate :premises (@p20) :args (@t103)) % 62.22/62.45 (step @p515 :rule symm :premises (@p247)) % 62.22/62.45 (step @p516 :rule refl :args (@t219)) % 62.22/62.45 (step @p517 :rule refl :args (tptp.cx)) % 62.22/62.45 (step @p518 :rule symm :premises (@p176)) % 62.22/62.45 (step @p519 :rule cong :premises (@p318 @p518) :args (@t349)) % 62.22/62.45 (step @p520 :rule symm :premises (@p86)) % 62.22/62.45 (step @p521 :rule cong :premises (@p318 @p520) :args (@t468)) % 62.22/62.45 (step @p522 :rule cong :premises (@p521) :args (@t469)) % 62.22/62.45 (step @p523 :rule symm :premises (@p521)) % 62.22/62.45 (step @p214 :rule instantiate :premises (@p11) :args (@t123)) % 62.22/62.45 (step @p524 :rule trans :premises (@p214 @p186 @p523)) % 62.22/62.45 (step @p525 :rule cong :premises (@p524) :args (@t157)) % 62.22/62.45 (step @p526 :rule trans :premises (@p262 @p525 @p522 @p197 @p519)) % 62.22/62.45 (step @p527 :rule cong :premises (@p526 @p517) :args (@t470)) % 62.22/62.45 (step @p528 :rule symm :premises (@p526)) % 62.22/62.45 (step @p529 :rule symm :premises (@p325)) % 62.22/62.45 (step @p530 :rule trans :premises (@p529 @p528)) % 62.22/62.45 (step @p531 :rule cong :premises (@p530 @p517) :args (@t284)) % 62.22/62.45 (step @p532 :rule symm :premises (@p347)) % 62.22/62.45 (step @p533 :rule trans :premises (@p532 @p531 @p527)) % 62.22/62.45 (step @p534 :rule cong :premises (@p533 @p516) :args (@t243)) % 62.22/62.45 (step @p535 :rule symm :premises (@p93)) % 62.22/62.45 (step @p536 :rule cong :premises (@p318 @p535) :args (@t235)) % 62.22/62.45 (step @p537 :rule cong :premises (@p536) :args (@t236)) % 62.22/62.45 (step @p538 :rule symm :premises (@p177)) % 62.22/62.45 (step @p539 :rule refl :args (@t133)) % 62.22/62.45 (step @p540 :rule cong :premises (@p539 @p538) :args (@t345)) % 62.22/62.45 (step @p541 :rule trans :premises (@p198 @p540)) % 62.22/62.45 (step @p542 :rule cong :premises (@p541 @p517) :args (@t255)) % 62.22/62.45 (step @p543 :rule symm :premises (@p383)) % 62.22/62.45 (step @p544 :rule symm :premises (@p397)) % 62.22/62.45 (step @p545 :rule cong :premises (@p538 @p517) :args (@t335)) % 62.22/62.45 (step @p546 :rule symm :premises (@p210)) % 62.22/62.45 (step @p547 :rule symm :premises (@p263)) % 62.22/62.45 (step @p548 :rule trans :premises (@p547 @p546 @p545)) % 62.22/62.45 (step @p549 :rule symm :premises (@p548)) % 62.22/62.45 (step @p550 :rule cong :premises (@p539 @p549) :args (@t237)) % 62.22/62.45 (step @p551 :rule refl :args (@t130)) % 62.22/62.45 (step @p552 :rule symm :premises (@p265)) % 62.22/62.45 (step @p553 :rule cong :premises (@p318 @p552) :args (@t294)) % 62.22/62.45 (step @p241 :rule instantiate :premises (@p11) :args (@t132)) % 62.22/62.45 (step @p554 :rule trans :premises (@p241 @p195)) % 62.22/62.45 (step @p555 :rule cong :premises (@p554) :args (@t196)) % 62.22/62.45 (step @p556 :rule trans :premises (@p360 @p555 @p327 @p553)) % 62.22/62.45 (step @p557 :rule cong :premises (@p556 @p551) :args (@t471)) % 62.22/62.45 (step @p558 :rule trans :premises (@p557 @p550 @p544 @p393 @p543 @p542)) % 62.22/62.45 (step @p559 :rule symm :premises (@p557)) % 62.22/62.45 (step @p560 :rule trans :premises (@p559 @p558)) % 62.22/62.45 (step @p561 :rule cong :premises (@p560 @p537) :args (@t238)) % 62.22/62.45 (step @p562 :rule symm :premises (@p251)) % 62.22/62.45 (step @p563 :rule symm :premises (@p250)) % 62.22/62.45 (step @p564 :rule symm :premises (@p350)) % 62.22/62.45 (step @p565 :rule trans :premises (@p564 @p563)) % 62.22/62.45 (step @p566 :rule cong :premises (@p565) :args (@t278)) % 62.22/62.45 (step @p567 :rule symm :premises (@p249)) % 62.22/62.45 (step @p568 :rule trans :premises (@p567 @p349 @p566 @p562)) % 62.22/62.45 (step @p569 :rule cong :premises (@p568) :args (@t259)) % 62.22/62.45 (step @p570 :rule symm :premises (@p382)) % 62.22/62.45 (step @p571 :rule refl :args (tptp.cy)) % 62.22/62.45 (step @p572 :rule cong :premises (@p571 @p124) :args (@t94)) % 62.22/62.45 (step @p573 :rule cong :premises (@p572) :args (@t95)) % 62.22/62.45 (step @p118 :rule instantiate :premises (@p11) :args (@t97)) % 62.22/62.45 (step @p574 :rule trans :premises (@p118 @p573)) % 62.22/62.45 (step @p575 :rule cong :premises (@p574) :args (@t472)) % 62.22/62.45 (step @p576 :rule symm :premises (@p125)) % 62.22/62.45 (step @p577 :rule symm :premises (@p124)) % 62.22/62.45 (step @p578 :rule cong :premises (@p577) :args (@t358)) % 62.22/62.45 (step @p579 :rule symm :premises (@p193)) % 62.22/62.45 (step @p580 :rule cong :premises (@p318 @p208) :args (@t473)) % 62.22/62.45 (step @p581 :rule trans :premises (@p580 @p579 @p578)) % 62.22/62.45 (step @p582 :rule cong :premises (@p571 @p581) :args (@t474)) % 62.22/62.45 (step @p583 :rule trans :premises (@p582 @p576 @p123)) % 62.22/62.45 (step @p584 :rule cong :premises (@p583) :args (@t475)) % 62.22/62.45 (step @p585 :rule trans :premises (@p584 @p575)) % 62.22/62.45 (step @p586 :rule symm :premises (@p361)) % 62.22/62.45 (step @p587 :rule refl :args (@t128)) % 62.22/62.45 (step @p588 :rule cong :premises (@p587 @p208) :args (@t476)) % 62.22/62.45 (step @p589 :rule trans :premises (@p588 @p586)) % 62.22/62.45 (step @p590 :rule cong :premises (@p589 @p585) :args (@t477)) % 62.22/62.45 (step @p591 :rule symm :premises (@p584)) % 62.22/62.45 (step @p592 :rule refl :args (@t72)) % 62.22/62.45 (step @p593 :rule cong :premises (@p592 @p577) :args (@t222)) % 62.22/62.45 (step @p594 :rule cong :premises (@p593) :args (@t223)) % 62.22/62.45 (step @p595 :rule trans :premises (@p594 @p591)) % 62.22/62.45 (step @p596 :rule symm :premises (@p588)) % 62.22/62.45 (step @p365 :rule instantiate :premises (@p11) :args (@t200)) % 62.22/62.45 (step @p331 :rule instantiate :premises (@p11) :args (@t183)) % 62.22/62.45 (step @p597 :rule cong :premises (@p331 @p551) :args (@t224)) % 62.22/62.45 (step @p598 :rule trans :premises (@p597 @p365 @p361 @p596)) % 62.22/62.45 (step @p599 :rule cong :premises (@p598 @p595) :args (@t227)) % 62.22/62.45 (step @p600 :rule trans :premises (@p599 @p590 @p570 @p569 @p350 @p396 @p561)) % 62.22/62.45 (step @p601 :rule refl :args (@t221)) % 62.22/62.45 (step @p602 :rule cong :premises (@p601 @p600) :args (@t228)) % 62.22/62.45 (step @p603 :rule trans :premises (@p602 @p395 @p534 @p515 @p131 @p514 @p510 @p66)) % 62.22/62.45 (step @p604 :rule symm :premises (@p59)) % 62.22/62.45 (step @p605 :rule symm :premises (@p61)) % 62.22/62.45 (step @p606 :rule symm :premises (@p25)) % 62.22/62.45 (step @p607 :rule cong :premises (@p606) :args (@t385)) % 62.22/62.45 (step @p608 :rule symm :premises (@p114)) % 62.22/62.45 (step @p45 :rule instantiate :premises (@p11) :args (@t61)) % 62.22/62.45 (step @p609 :rule cong :premises (@p45) :args (@t403)) % 62.22/62.45 (step @p108 :rule instantiate :premises (@p11) :args (@t90)) % 62.22/62.45 (step @p97 :rule instantiate :premises (@p11) :args (@t82)) % 62.22/62.45 (step @p610 :rule cong :premises (@p97 @p517) :args (@t404)) % 62.22/62.45 (step @p611 :rule trans :premises (@p610 @p108)) % 62.22/62.45 (step @p612 :rule cong :premises (@p611 @p609) :args (@t405)) % 62.22/62.45 (step @p613 :rule trans :premises (@p87 @p612 @p608 @p607 @p605)) % 62.22/62.45 (step @p614 :rule cong :premises (@p613) :args (@t373)) % 62.22/62.45 (step @p615 :rule symm :premises (@p248)) % 62.22/62.45 (step @p616 :rule cong :premises (@p571 @p228) :args (@t379)) % 62.22/62.45 (step @p617 :rule trans :premises (@p118 @p125 @p616)) % 62.22/62.45 (step @p618 :rule cong :premises (@p617) :args (@t472)) % 62.22/62.45 (step @p232 :rule instantiate :premises (@p11) :args (@t131)) % 62.22/62.45 (step @p619 :rule trans :premises (@p232 @p194)) % 62.22/62.45 (step @p620 :rule cong :premises (@p619 @p517) :args (@t478)) % 62.22/62.45 (step @p621 :rule cong :premises (@p620 @p618) :args (@t479)) % 62.22/62.45 (step @p622 :rule symm :premises (@p620)) % 62.22/62.45 (step @p623 :rule cong :premises (@p237 @p517) :args (@t161)) % 62.22/62.45 (step @p624 :rule symm :premises (@p252)) % 62.22/62.45 (step @p625 :rule trans :premises (@p624 @p274 @p623 @p620)) % 62.22/62.45 (step @p269 :rule instantiate :premises (@p11) :args (@t155)) % 62.22/62.45 (step @p626 :rule symm :premises (@p623)) % 62.22/62.45 (step @p627 :rule symm :premises (@p619)) % 62.22/62.45 (step @p628 :rule symm :premises (@p181)) % 62.22/62.45 (step @p629 :rule symm :premises (@p62)) % 62.22/62.45 (step @p630 :rule symm :premises (@p103)) % 62.22/62.45 (step @p631 :rule trans :premises (@p630 @p629 @p23)) % 62.22/62.45 (step @p632 :rule trans :premises (@p631 @p13)) % 62.22/62.45 (step @p633 :rule cong :premises (@p632 @p517) :args (@t338)) % 62.22/62.45 (step @p634 :rule trans :premises (@p633 @p628)) % 62.22/62.45 (step @p635 :rule cong :premises (@p318 @p634) :args (@t339)) % 62.22/62.45 (step @p636 :rule symm :premises (@p209)) % 62.22/62.45 (step @p637 :rule trans :premises (@p636 @p635)) % 62.22/62.45 (step @p638 :rule cong :premises (@p592 @p637) :args (@t288)) % 62.22/62.45 (step @p639 :rule symm :premises (@p346)) % 62.22/62.45 (step @p640 :rule symm :premises (@p30)) % 62.22/62.45 (step @p641 :rule trans :premises (@p640 @p62 @p103)) % 62.22/62.45 (step @p642 :rule cong :premises (@p318 @p641) :args (@t414)) % 62.22/62.45 (step @p643 :rule symm :premises (@p67)) % 62.22/62.45 (step @p644 :rule cong :premises (@p54 @p311) :args (@t452)) % 62.22/62.45 (step @p645 :rule trans :premises (@p630 @p629 @p31 @p644 @p643 @p642)) % 62.22/62.45 (step @p646 :rule cong :premises (@p592 @p645) :args (@t306)) % 62.22/62.45 (step @p647 :rule symm :premises (@p264)) % 62.22/62.45 (step @p648 :rule cong :premises (@p85) :args (@t348)) % 62.22/62.45 (step @p649 :rule trans :premises (@p176 @p648 @p196)) % 62.22/62.45 (step @p650 :rule trans :premises (@p520 @p85)) % 62.22/62.45 (step @p651 :rule cong :premises (@p650 @p649) :args (@t480)) % 62.22/62.45 (step @p652 :rule refl :args (@t40)) % 62.22/62.45 (step @p653 :rule cong :premises (@p86 @p652) :args (@t195)) % 62.22/62.45 (step @p654 :rule trans :premises (@p13 @p63 @p653 @p651 @p647 @p646)) % 62.22/62.45 (step @p655 :rule trans :premises (@p314 @p23)) % 62.22/62.45 (step @p656 :rule trans :premises (@p655 @p654)) % 62.22/62.45 (step @p657 :rule cong :premises (@p656 @p237) :args (@t271)) % 62.22/62.45 (step @p658 :rule symm :premises (@p351)) % 62.22/62.45 (step @p659 :rule symm :premises (@p64)) % 62.22/62.45 (step @p660 :rule refl :args (@t66)) % 62.22/62.45 (step @p661 :rule trans :premises (@p303 @p302)) % 62.22/62.45 (step @p662 :rule cong :premises (@p661) :args (@t420)) % 62.22/62.45 (step @p663 :rule symm :premises (@p65)) % 62.22/62.45 (step @p664 :rule symm :premises (@p104)) % 62.22/62.45 (step @p36 :rule instantiate :premises (@p11) :args (@t52)) % 62.22/62.45 (step @p665 :rule cong :premises (@p36) :args (@t481)) % 62.22/62.45 (step @p71 :rule instantiate :premises (@p11) :args (@t70)) % 62.22/62.45 (step @p666 :rule cong :premises (@p71 @p571) :args (@t482)) % 62.22/62.45 (step @p667 :rule trans :premises (@p666 @p97)) % 62.22/62.45 (step @p668 :rule cong :premises (@p667 @p665) :args (@t483)) % 62.22/62.45 (step @p669 :rule trans :premises (@p668 @p664 @p663 @p662)) % 62.22/62.45 (step @p670 :rule cong :premises (@p669 @p660) :args (@t484)) % 62.22/62.45 (step @p671 :rule symm :premises (@p669)) % 62.22/62.45 (step @p672 :rule trans :premises (@p60 @p671)) % 62.22/62.45 (step @p673 :rule cong :premises (@p672 @p660) :args (@t485)) % 62.22/62.45 (step @p674 :rule trans :premises (@p673 @p670 @p659 @p63)) % 62.22/62.45 (step @p675 :rule refl :args (@t127)) % 62.22/62.45 (step @p676 :rule cong :premises (@p675 @p674) :args (@t486)) % 62.22/62.45 (step @p677 :rule symm :premises (@p673)) % 62.22/62.45 (step @p678 :rule symm :premises (@p670)) % 62.22/62.45 (step @p679 :rule symm :premises (@p348)) % 62.22/62.45 (step @p680 :rule trans :premises (@p679 @p64 @p678 @p677)) % 62.22/62.45 (step @p681 :rule cong :premises (@p675 @p680) :args (@t264)) % 62.22/62.45 (step @p682 :rule symm :premises (@p371)) % 62.22/62.45 (step @p683 :rule refl :args (@t193)) % 62.22/62.45 (step @p684 :rule symm :premises (@p199)) % 62.22/62.45 (step @p685 :rule cong :premises (@p587 @p177) :args (@t129)) % 62.22/62.45 (step @p686 :rule trans :premises (@p685 @p684)) % 62.22/62.45 (step @p687 :rule cong :premises (@p675 @p686) :args (@t361)) % 62.22/62.45 (step @p688 :rule trans :premises (@p91 @p126 @p192 @p687)) % 62.22/62.45 (step @p689 :rule trans :premises (@p57 @p688)) % 62.22/62.45 (step @p690 :rule cong :premises (@p689 @p683) :args (@t246)) % 62.22/62.45 (step @p691 :rule trans :premises (@p690 @p682 @p681 @p676 @p658 @p657 @p639 @p638 @p232 @p194)) % 62.22/62.45 (step @p692 :rule trans :premises (@p691 @p627)) % 62.22/62.45 (step @p693 :rule cong :premises (@p692 @p517) :args (@t247)) % 62.22/62.45 (step @p694 :rule symm :premises (@p394)) % 62.22/62.45 (step @p340 :rule instantiate :premises (@p11) :args (@t156)) % 62.22/62.45 (step @p695 :rule symm :premises (@p326)) % 62.22/62.45 (step @p696 :rule cong :premises (@p695 @p517) :args (@t487)) % 62.22/62.45 (step @p697 :rule trans :premises (@p331 @p326)) % 62.22/62.45 (step @p698 :rule cong :premises (@p697 @p517) :args (@t488)) % 62.22/62.45 (step @p699 :rule trans :premises (@p698 @p696 @p340 @p253)) % 62.22/62.45 (step @p700 :rule cong :premises (@p699 @p517) :args (@t489)) % 62.22/62.45 (step @p701 :rule symm :premises (@p699)) % 62.22/62.45 (step @p702 :rule trans :premises (@p253 @p701)) % 62.22/62.45 (step @p703 :rule cong :premises (@p702 @p517) :args (@t251)) % 62.22/62.45 (step @p704 :rule symm :premises (@p384)) % 62.22/62.45 (step @p705 :rule cong :premises (@p587 @p548) :args (@t490)) % 62.22/62.45 (step @p706 :rule trans :premises (@p705 @p381)) % 62.22/62.45 (step @p707 :rule cong :premises (@p706) :args (@t491)) % 62.22/62.45 (step @p708 :rule symm :premises (@p705)) % 62.22/62.45 (step @p709 :rule cong :premises (@p708) :args (@t203)) % 62.22/62.45 (step @p710 :rule trans :premises (@p597 @p365 @p709 @p707 @p704 @p703 @p700)) % 62.22/62.45 (step @p711 :rule symm :premises (@p57)) % 62.22/62.45 (step @p712 :rule cong :premises (@p711 @p517) :args (@t221)) % 62.22/62.45 (step @p713 :rule cong :premises (@p712 @p710) :args (@t225)) % 62.22/62.45 (step @p714 :rule trans :premises (@p713 @p694 @p693 @p626 @p269 @p252)) % 62.22/62.45 (step @p715 :rule trans :premises (@p714 @p625 @p622)) % 62.22/62.45 (step @p716 :rule cong :premises (@p715 @p594) :args (@t226)) % 62.22/62.45 (step @p717 :rule trans :premises (@p716 @p621 @p615 @p137 @p614 @p604 @p25)) % 62.22/62.45 (step @p718 :rule cong :premises (@p717 @p603) :args (@t465)) % 62.22/62.45 (step @p719 :rule trans :premises (@p718 @p508)) % 62.22/62.45 (step @p720 :rule eq_resolve :premises (@p719 @p507)) % 62.22/62.45 (step @p721 :rule symm :premises (@p720)) % 62.22/62.45 (step @p722 :rule trans :premises (@p721 @p500)) % 62.22/62.45 (step @p723 false :rule eq_resolve :premises (@p722 @p499)) % 62.22/62.45 (step-pop @p983 :rule scope :premises (@p723)) % 62.22/62.45 (step-pop @p984 :rule scope :premises (@p983)) % 62.22/62.45 (step @p724 :rule process_scope :premises (@p984) :args (false)) % 62.22/62.45 (assume-push @p985 @t463) % 62.22/62.45 (assume-push @p986 @t461) % 62.22/62.45 (assume-push @p987 @t459) % 62.22/62.45 (assume-push @p988 @t457) % 62.22/62.45 (assume-push @p989 @t455) % 62.22/62.45 (assume-push @p990 @t453) % 62.22/62.45 (assume-push @p991 @t53) % 62.22/62.45 (assume-push @p992 @t62) % 62.22/62.45 (assume-push @p993 @t448) % 62.22/62.45 (assume-push @p994 @t446) % 62.22/62.45 (assume-push @p995 @t443) % 62.22/62.45 (assume-push @p996 @t440) % 62.22/62.45 (assume-push @p997 @t438) % 62.22/62.45 (assume-push @p998 @t435) % 62.22/62.45 (assume-push @p999 @t433) % 62.22/62.45 (assume-push @p1000 @t431) % 62.22/62.45 (assume-push @p1001 @t427) % 62.22/62.45 (assume-push @p1002 @t425) % 62.22/62.45 (assume-push @p1003 @t423) % 62.22/62.45 (assume-push @p1004 @t421) % 62.22/62.45 (assume-push @p1005 @t418) % 62.22/62.45 (assume-push @p1006 @t415) % 62.22/62.45 (assume-push @p1007 @t71) % 62.22/62.45 (assume-push @p1008 @t77) % 62.22/62.45 (assume-push @p1009 @t409) % 62.22/62.45 (assume-push @p1010 @t406) % 62.22/62.45 (assume-push @p1011 @t401) % 62.22/62.45 (assume-push @p1012 @t399) % 62.22/62.45 (assume-push @p1013 @t396) % 62.22/62.45 (assume-push @p1014 @t83) % 62.22/62.45 (assume-push @p1015 @t393) % 62.22/62.45 (assume-push @p1016 @t390) % 62.22/62.45 (assume-push @p1017 @t91) % 62.22/62.45 (assume-push @p1018 @t386) % 62.22/62.45 (assume-push @p1019 @t98) % 62.22/62.45 (assume-push @p1020 @t111) % 62.22/62.45 (assume-push @p1021 @t382) % 62.22/62.45 (assume-push @p1022 @t380) % 62.22/62.45 (assume-push @p1023 @t377) % 62.22/62.45 (assume-push @p1024 @t104) % 62.22/62.45 (assume-push @p1025 @t374) % 62.22/62.45 (assume-push @p1026 @t370) % 62.22/62.45 (assume-push @p1027 @t368) % 62.22/62.45 (assume-push @p1028 @t366) % 62.22/62.45 (assume-push @p1029 @t124) % 62.22/62.45 (assume-push @p1030 @t363) % 62.22/62.45 (assume-push @p1031 @t359) % 62.22/62.45 (assume-push @p1032 @t356) % 62.22/62.45 (assume-push @p1033 @t354) % 62.22/62.45 (assume-push @p1034 @t352) % 62.22/62.45 (assume-push @p1035 @t350) % 62.22/62.45 (assume-push @p1036 @t346) % 62.22/62.45 (assume-push @p1037 @t343) % 62.22/62.45 (assume-push @p1038 @t138) % 62.22/62.45 (assume-push @p1039 @t340) % 62.22/62.45 (assume-push @p1040 @t336) % 62.22/62.45 (assume-push @p1041 @t142) % 62.22/62.45 (assume-push @p1042 @t146) % 62.22/62.45 (assume-push @p1043 @t149) % 62.22/62.45 (assume-push @p1044 @t153) % 62.22/62.45 (assume-push @p1045 @t328) % 62.22/62.45 (assume-push @p1046 @t326) % 62.22/62.45 (assume-push @p1047 @t322) % 62.22/62.45 (assume-push @p1048 @t320) % 62.22/62.45 (assume-push @p1049 @t318) % 62.22/62.45 (assume-push @p1050 @t315) % 62.22/62.45 (assume-push @p1051 @t313) % 62.22/62.45 (assume-push @p1052 @t160) % 62.22/62.45 (assume-push @p1053 @t310) % 62.22/62.45 (assume-push @p1054 @t307) % 62.22/62.45 (assume-push @p1055 @t303) % 62.22/62.45 (assume-push @p1056 @t172) % 62.22/62.45 (assume-push @p1057 @t164) % 62.22/62.45 (assume-push @p1058 @t299) % 62.22/62.45 (assume-push @p1059 @t296) % 62.22/62.45 (assume-push @p1060 @t187) % 62.22/62.45 (assume-push @p1061 @t191) % 62.22/62.45 (assume-push @p1062 @t289) % 62.22/62.45 (assume-push @p1063 @t285) % 62.22/62.45 (assume-push @p1064 @t282) % 62.22/62.45 (assume-push @p1065 @t280) % 62.22/62.45 (assume-push @p1066 @t276) % 62.22/62.45 (assume-push @p1067 @t272) % 62.22/62.45 (assume-push @p1068 @t199) % 62.22/62.45 (assume-push @p1069 @t268) % 62.22/62.45 (assume-push @p1070 @t205) % 62.22/62.45 (assume-push @p1071 @t265) % 62.22/62.45 (assume-push @p1072 @t209) % 62.22/62.45 (assume-push @p1073 @t260) % 62.22/62.45 (assume-push @p1074 @t256) % 62.22/62.45 (assume-push @p1075 @t252) % 62.22/62.45 (assume-push @p1076 @t217) % 62.22/62.45 (assume-push @p1077 @t248) % 62.22/62.45 (assume-push @p1078 @t244) % 62.22/62.45 (assume-push @p1079 @t240) % 62.22/62.45 (assume-push @p1080 @t232) % 62.22/62.45 (assume-push @p1081 @t229) % 62.22/62.45 (step @p501 :rule bool-eq-false :args (@t229)) % 62.22/62.45 (step @p502 :rule symm :premises (@p501)) % 62.22/62.45 (step @p503 :rule eq-symm :args (@t226 @t228)) % 62.22/62.45 (step @p504 :rule cong :premises (@p503) :args (@t466)) % 62.22/62.45 (step @p505 :rule bool-eq-false :args (@t465)) % 62.22/62.45 (step @p506 :rule trans :premises (@p505 @p504)) % 62.22/62.45 (step @p507 :rule trans :premises (@p506 @p502)) % 62.22/62.45 (step @p508 :rule false_intro :premises (@p175)) % 62.22/62.45 (step @p509 :rule trans :premises (@p26 @p56)) % 62.22/62.45 (step @p510 :rule cong :premises (@p509) :args (@t467)) % 62.22/62.45 (step @p511 :rule symm :premises (@p58)) % 62.22/62.45 (step @p512 :rule symm :premises (@p92)) % 62.22/62.45 (step @p513 :rule trans :premises (@p512 @p511)) % 62.22/62.45 (step @p514 :rule cong :premises (@p513) :args (@t101)) % 62.22/62.45 (step @p131 :rule instantiate :premises (@p20) :args (@t103)) % 62.22/62.45 (step @p515 :rule symm :premises (@p247)) % 62.22/62.45 (step @p516 :rule refl :args (@t219)) % 62.22/62.45 (step @p517 :rule refl :args (tptp.cx)) % 62.22/62.45 (step @p518 :rule symm :premises (@p176)) % 62.22/62.45 (step @p519 :rule cong :premises (@p318 @p518) :args (@t349)) % 62.22/62.45 (step @p520 :rule symm :premises (@p86)) % 62.22/62.45 (step @p521 :rule cong :premises (@p318 @p520) :args (@t468)) % 62.22/62.45 (step @p522 :rule cong :premises (@p521) :args (@t469)) % 62.22/62.45 (step @p523 :rule symm :premises (@p521)) % 62.22/62.45 (step @p214 :rule instantiate :premises (@p11) :args (@t123)) % 62.22/62.45 (step @p524 :rule trans :premises (@p214 @p186 @p523)) % 62.22/62.45 (step @p525 :rule cong :premises (@p524) :args (@t157)) % 62.22/62.45 (step @p526 :rule trans :premises (@p262 @p525 @p522 @p197 @p519)) % 62.22/62.45 (step @p527 :rule cong :premises (@p526 @p517) :args (@t470)) % 62.22/62.45 (step @p528 :rule symm :premises (@p526)) % 62.22/62.45 (step @p529 :rule symm :premises (@p325)) % 62.22/62.45 (step @p530 :rule trans :premises (@p529 @p528)) % 62.22/62.45 (step @p531 :rule cong :premises (@p530 @p517) :args (@t284)) % 62.22/62.45 (step @p532 :rule symm :premises (@p347)) % 62.22/62.45 (step @p533 :rule trans :premises (@p532 @p531 @p527)) % 62.22/62.45 (step @p534 :rule cong :premises (@p533 @p516) :args (@t243)) % 62.22/62.45 (step @p535 :rule symm :premises (@p93)) % 62.22/62.45 (step @p536 :rule cong :premises (@p318 @p535) :args (@t235)) % 62.22/62.45 (step @p537 :rule cong :premises (@p536) :args (@t236)) % 62.22/62.45 (step @p538 :rule symm :premises (@p177)) % 62.22/62.45 (step @p539 :rule refl :args (@t133)) % 62.22/62.45 (step @p540 :rule cong :premises (@p539 @p538) :args (@t345)) % 62.22/62.45 (step @p541 :rule trans :premises (@p198 @p540)) % 62.22/62.45 (step @p542 :rule cong :premises (@p541 @p517) :args (@t255)) % 62.22/62.45 (step @p543 :rule symm :premises (@p383)) % 62.22/62.45 (step @p544 :rule symm :premises (@p397)) % 62.22/62.45 (step @p545 :rule cong :premises (@p538 @p517) :args (@t335)) % 62.22/62.45 (step @p546 :rule symm :premises (@p210)) % 62.22/62.45 (step @p547 :rule symm :premises (@p263)) % 62.22/62.45 (step @p548 :rule trans :premises (@p547 @p546 @p545)) % 62.22/62.45 (step @p549 :rule symm :premises (@p548)) % 62.22/62.45 (step @p550 :rule cong :premises (@p539 @p549) :args (@t237)) % 62.22/62.45 (step @p551 :rule refl :args (@t130)) % 62.22/62.45 (step @p552 :rule symm :premises (@p265)) % 62.22/62.45 (step @p553 :rule cong :premises (@p318 @p552) :args (@t294)) % 62.22/62.45 (step @p241 :rule instantiate :premises (@p11) :args (@t132)) % 62.22/62.45 (step @p554 :rule trans :premises (@p241 @p195)) % 62.22/62.45 (step @p555 :rule cong :premises (@p554) :args (@t196)) % 62.22/62.45 (step @p556 :rule trans :premises (@p360 @p555 @p327 @p553)) % 62.22/62.45 (step @p557 :rule cong :premises (@p556 @p551) :args (@t471)) % 62.22/62.45 (step @p558 :rule trans :premises (@p557 @p550 @p544 @p393 @p543 @p542)) % 62.22/62.45 (step @p559 :rule symm :premises (@p557)) % 62.22/62.45 (step @p560 :rule trans :premises (@p559 @p558)) % 62.22/62.45 (step @p561 :rule cong :premises (@p560 @p537) :args (@t238)) % 62.22/62.45 (step @p562 :rule symm :premises (@p251)) % 62.22/62.45 (step @p563 :rule symm :premises (@p250)) % 62.22/62.45 (step @p564 :rule symm :premises (@p350)) % 62.22/62.45 (step @p565 :rule trans :premises (@p564 @p563)) % 62.22/62.45 (step @p566 :rule cong :premises (@p565) :args (@t278)) % 62.22/62.45 (step @p567 :rule symm :premises (@p249)) % 62.22/62.45 (step @p568 :rule trans :premises (@p567 @p349 @p566 @p562)) % 62.22/62.45 (step @p569 :rule cong :premises (@p568) :args (@t259)) % 62.22/62.45 (step @p570 :rule symm :premises (@p382)) % 62.22/62.45 (step @p571 :rule refl :args (tptp.cy)) % 62.22/62.45 (step @p572 :rule cong :premises (@p571 @p124) :args (@t94)) % 62.22/62.45 (step @p573 :rule cong :premises (@p572) :args (@t95)) % 62.22/62.45 (step @p118 :rule instantiate :premises (@p11) :args (@t97)) % 62.22/62.45 (step @p574 :rule trans :premises (@p118 @p573)) % 62.22/62.45 (step @p575 :rule cong :premises (@p574) :args (@t472)) % 62.22/62.45 (step @p576 :rule symm :premises (@p125)) % 62.22/62.45 (step @p577 :rule symm :premises (@p124)) % 62.22/62.45 (step @p578 :rule cong :premises (@p577) :args (@t358)) % 62.22/62.45 (step @p579 :rule symm :premises (@p193)) % 62.22/62.45 (step @p580 :rule cong :premises (@p318 @p208) :args (@t473)) % 62.22/62.45 (step @p581 :rule trans :premises (@p580 @p579 @p578)) % 62.22/62.45 (step @p582 :rule cong :premises (@p571 @p581) :args (@t474)) % 62.22/62.45 (step @p583 :rule trans :premises (@p582 @p576 @p123)) % 62.22/62.45 (step @p584 :rule cong :premises (@p583) :args (@t475)) % 62.22/62.45 (step @p585 :rule trans :premises (@p584 @p575)) % 62.22/62.45 (step @p586 :rule symm :premises (@p361)) % 62.22/62.45 (step @p587 :rule refl :args (@t128)) % 62.22/62.45 (step @p588 :rule cong :premises (@p587 @p208) :args (@t476)) % 62.22/62.45 (step @p589 :rule trans :premises (@p588 @p586)) % 62.22/62.45 (step @p590 :rule cong :premises (@p589 @p585) :args (@t477)) % 62.22/62.45 (step @p591 :rule symm :premises (@p584)) % 62.22/62.45 (step @p592 :rule refl :args (@t72)) % 62.22/62.45 (step @p593 :rule cong :premises (@p592 @p577) :args (@t222)) % 62.22/62.45 (step @p594 :rule cong :premises (@p593) :args (@t223)) % 62.22/62.45 (step @p595 :rule trans :premises (@p594 @p591)) % 62.22/62.45 (step @p596 :rule symm :premises (@p588)) % 62.22/62.45 (step @p365 :rule instantiate :premises (@p11) :args (@t200)) % 62.22/62.45 (step @p331 :rule instantiate :premises (@p11) :args (@t183)) % 62.22/62.45 (step @p597 :rule cong :premises (@p331 @p551) :args (@t224)) % 62.22/62.45 (step @p598 :rule trans :premises (@p597 @p365 @p361 @p596)) % 62.22/62.45 (step @p599 :rule cong :premises (@p598 @p595) :args (@t227)) % 62.22/62.45 (step @p600 :rule trans :premises (@p599 @p590 @p570 @p569 @p350 @p396 @p561)) % 62.22/62.45 (step @p601 :rule refl :args (@t221)) % 62.22/62.45 (step @p602 :rule cong :premises (@p601 @p600) :args (@t228)) % 62.22/62.45 (step @p603 :rule trans :premises (@p602 @p395 @p534 @p515 @p131 @p514 @p510 @p66)) % 62.22/62.45 (step @p604 :rule symm :premises (@p59)) % 62.22/62.45 (step @p605 :rule symm :premises (@p61)) % 62.22/62.45 (step @p606 :rule symm :premises (@p25)) % 62.22/62.45 (step @p607 :rule cong :premises (@p606) :args (@t385)) % 62.22/62.45 (step @p608 :rule symm :premises (@p114)) % 62.22/62.45 (step @p45 :rule instantiate :premises (@p11) :args (@t61)) % 62.22/62.45 (step @p609 :rule cong :premises (@p45) :args (@t403)) % 62.22/62.45 (step @p108 :rule instantiate :premises (@p11) :args (@t90)) % 62.22/62.45 (step @p97 :rule instantiate :premises (@p11) :args (@t82)) % 62.22/62.45 (step @p610 :rule cong :premises (@p97 @p517) :args (@t404)) % 62.22/62.45 (step @p611 :rule trans :premises (@p610 @p108)) % 62.22/62.45 (step @p612 :rule cong :premises (@p611 @p609) :args (@t405)) % 62.22/62.45 (step @p613 :rule trans :premises (@p87 @p612 @p608 @p607 @p605)) % 62.22/62.45 (step @p614 :rule cong :premises (@p613) :args (@t373)) % 62.22/62.45 (step @p615 :rule symm :premises (@p248)) % 62.22/62.45 (step @p616 :rule cong :premises (@p571 @p228) :args (@t379)) % 62.22/62.45 (step @p617 :rule trans :premises (@p118 @p125 @p616)) % 62.22/62.45 (step @p618 :rule cong :premises (@p617) :args (@t472)) % 62.22/62.45 (step @p232 :rule instantiate :premises (@p11) :args (@t131)) % 62.22/62.45 (step @p619 :rule trans :premises (@p232 @p194)) % 62.22/62.45 (step @p620 :rule cong :premises (@p619 @p517) :args (@t478)) % 62.22/62.45 (step @p621 :rule cong :premises (@p620 @p618) :args (@t479)) % 62.22/62.45 (step @p622 :rule symm :premises (@p620)) % 62.22/62.45 (step @p623 :rule cong :premises (@p237 @p517) :args (@t161)) % 62.22/62.45 (step @p624 :rule symm :premises (@p252)) % 62.22/62.45 (step @p625 :rule trans :premises (@p624 @p274 @p623 @p620)) % 62.22/62.45 (step @p269 :rule instantiate :premises (@p11) :args (@t155)) % 62.22/62.45 (step @p626 :rule symm :premises (@p623)) % 62.22/62.45 (step @p627 :rule symm :premises (@p619)) % 62.22/62.45 (step @p628 :rule symm :premises (@p181)) % 62.22/62.45 (step @p629 :rule symm :premises (@p62)) % 62.22/62.45 (step @p630 :rule symm :premises (@p103)) % 62.22/62.45 (step @p631 :rule trans :premises (@p630 @p629 @p23)) % 62.22/62.45 (step @p632 :rule trans :premises (@p631 @p13)) % 62.22/62.45 (step @p633 :rule cong :premises (@p632 @p517) :args (@t338)) % 62.22/62.45 (step @p634 :rule trans :premises (@p633 @p628)) % 62.22/62.45 (step @p635 :rule cong :premises (@p318 @p634) :args (@t339)) % 62.22/62.45 (step @p636 :rule symm :premises (@p209)) % 62.22/62.45 (step @p637 :rule trans :premises (@p636 @p635)) % 62.22/62.45 (step @p638 :rule cong :premises (@p592 @p637) :args (@t288)) % 62.22/62.45 (step @p639 :rule symm :premises (@p346)) % 62.22/62.45 (step @p640 :rule symm :premises (@p30)) % 62.22/62.45 (step @p641 :rule trans :premises (@p640 @p62 @p103)) % 62.22/62.45 (step @p642 :rule cong :premises (@p318 @p641) :args (@t414)) % 62.22/62.45 (step @p643 :rule symm :premises (@p67)) % 62.22/62.45 (step @p644 :rule cong :premises (@p54 @p311) :args (@t452)) % 62.22/62.45 (step @p645 :rule trans :premises (@p630 @p629 @p31 @p644 @p643 @p642)) % 62.22/62.45 (step @p646 :rule cong :premises (@p592 @p645) :args (@t306)) % 62.22/62.45 (step @p647 :rule symm :premises (@p264)) % 62.22/62.45 (step @p648 :rule cong :premises (@p85) :args (@t348)) % 62.22/62.45 (step @p649 :rule trans :premises (@p176 @p648 @p196)) % 62.22/62.45 (step @p650 :rule trans :premises (@p520 @p85)) % 62.22/62.45 (step @p651 :rule cong :premises (@p650 @p649) :args (@t480)) % 62.22/62.45 (step @p652 :rule refl :args (@t40)) % 62.22/62.45 (step @p653 :rule cong :premises (@p86 @p652) :args (@t195)) % 62.22/62.45 (step @p654 :rule trans :premises (@p13 @p63 @p653 @p651 @p647 @p646)) % 62.22/62.45 (step @p655 :rule trans :premises (@p314 @p23)) % 62.22/62.45 (step @p656 :rule trans :premises (@p655 @p654)) % 62.22/62.45 (step @p657 :rule cong :premises (@p656 @p237) :args (@t271)) % 62.22/62.45 (step @p658 :rule symm :premises (@p351)) % 62.22/62.45 (step @p659 :rule symm :premises (@p64)) % 62.22/62.45 (step @p660 :rule refl :args (@t66)) % 62.22/62.45 (step @p661 :rule trans :premises (@p303 @p302)) % 62.22/62.45 (step @p662 :rule cong :premises (@p661) :args (@t420)) % 62.22/62.45 (step @p663 :rule symm :premises (@p65)) % 62.22/62.45 (step @p664 :rule symm :premises (@p104)) % 62.22/62.45 (step @p36 :rule instantiate :premises (@p11) :args (@t52)) % 62.22/62.45 (step @p665 :rule cong :premises (@p36) :args (@t481)) % 62.22/62.45 (step @p71 :rule instantiate :premises (@p11) :args (@t70)) % 62.22/62.45 (step @p666 :rule cong :premises (@p71 @p571) :args (@t482)) % 62.22/62.45 (step @p667 :rule trans :premises (@p666 @p97)) % 62.22/62.45 (step @p668 :rule cong :premises (@p667 @p665) :args (@t483)) % 62.22/62.45 (step @p669 :rule trans :premises (@p668 @p664 @p663 @p662)) % 62.22/62.45 (step @p670 :rule cong :premises (@p669 @p660) :args (@t484)) % 62.22/62.45 (step @p671 :rule symm :premises (@p669)) % 62.22/62.45 (step @p672 :rule trans :premises (@p60 @p671)) % 62.22/62.45 (step @p673 :rule cong :premises (@p672 @p660) :args (@t485)) % 62.22/62.45 (step @p674 :rule trans :premises (@p673 @p670 @p659 @p63)) % 62.22/62.45 (step @p675 :rule refl :args (@t127)) % 62.22/62.45 (step @p676 :rule cong :premises (@p675 @p674) :args (@t486)) % 62.22/62.45 (step @p677 :rule symm :premises (@p673)) % 62.22/62.45 (step @p678 :rule symm :premises (@p670)) % 62.22/62.45 (step @p679 :rule symm :premises (@p348)) % 62.22/62.45 (step @p680 :rule trans :premises (@p679 @p64 @p678 @p677)) % 62.22/62.45 (step @p681 :rule cong :premises (@p675 @p680) :args (@t264)) % 62.22/62.45 (step @p682 :rule symm :premises (@p371)) % 62.22/62.45 (step @p683 :rule refl :args (@t193)) % 62.22/62.45 (step @p684 :rule symm :premises (@p199)) % 62.22/62.45 (step @p685 :rule cong :premises (@p587 @p177) :args (@t129)) % 62.22/62.45 (step @p686 :rule trans :premises (@p685 @p684)) % 62.22/62.45 (step @p687 :rule cong :premises (@p675 @p686) :args (@t361)) % 62.22/62.45 (step @p688 :rule trans :premises (@p91 @p126 @p192 @p687)) % 62.22/62.45 (step @p689 :rule trans :premises (@p57 @p688)) % 62.22/62.45 (step @p690 :rule cong :premises (@p689 @p683) :args (@t246)) % 62.22/62.45 (step @p691 :rule trans :premises (@p690 @p682 @p681 @p676 @p658 @p657 @p639 @p638 @p232 @p194)) % 62.22/62.45 (step @p692 :rule trans :premises (@p691 @p627)) % 62.22/62.45 (step @p693 :rule cong :premises (@p692 @p517) :args (@t247)) % 62.22/62.45 (step @p694 :rule symm :premises (@p394)) % 62.22/62.45 (step @p340 :rule instantiate :premises (@p11) :args (@t156)) % 62.22/62.45 (step @p695 :rule symm :premises (@p326)) % 62.22/62.45 (step @p696 :rule cong :premises (@p695 @p517) :args (@t487)) % 62.22/62.45 (step @p697 :rule trans :premises (@p331 @p326)) % 62.22/62.45 (step @p698 :rule cong :premises (@p697 @p517) :args (@t488)) % 62.22/62.45 (step @p699 :rule trans :premises (@p698 @p696 @p340 @p253)) % 62.22/62.45 (step @p700 :rule cong :premises (@p699 @p517) :args (@t489)) % 62.22/62.45 (step @p701 :rule symm :premises (@p699)) % 62.22/62.45 (step @p702 :rule trans :premises (@p253 @p701)) % 62.22/62.45 (step @p703 :rule cong :premises (@p702 @p517) :args (@t251)) % 62.22/62.45 (step @p704 :rule symm :premises (@p384)) % 62.22/62.45 (step @p705 :rule cong :premises (@p587 @p548) :args (@t490)) % 62.22/62.45 (step @p706 :rule trans :premises (@p705 @p381)) % 62.22/62.45 (step @p707 :rule cong :premises (@p706) :args (@t491)) % 62.22/62.45 (step @p708 :rule symm :premises (@p705)) % 62.22/62.45 (step @p709 :rule cong :premises (@p708) :args (@t203)) % 62.22/62.45 (step @p710 :rule trans :premises (@p597 @p365 @p709 @p707 @p704 @p703 @p700)) % 62.22/62.45 (step @p711 :rule symm :premises (@p57)) % 62.22/62.45 (step @p712 :rule cong :premises (@p711 @p517) :args (@t221)) % 62.22/62.45 (step @p713 :rule cong :premises (@p712 @p710) :args (@t225)) % 62.22/62.45 (step @p714 :rule trans :premises (@p713 @p694 @p693 @p626 @p269 @p252)) % 62.22/62.45 (step @p715 :rule trans :premises (@p714 @p625 @p622)) % 62.22/62.45 (step @p716 :rule cong :premises (@p715 @p594) :args (@t226)) % 62.22/62.45 (step @p717 :rule trans :premises (@p716 @p621 @p615 @p137 @p614 @p604 @p25)) % 62.22/62.45 (step @p718 :rule cong :premises (@p717 @p603) :args (@t465)) % 62.22/62.45 (step @p719 :rule trans :premises (@p718 @p508)) % 62.22/62.45 (step @p824 :rule eq_resolve :premises (@p719 @p507)) % 62.22/62.45 (step @p825 :rule false_elim :premises (@p824)) % 62.22/62.45 (step @p826 :rule and_intro :premises (@p398 @p825)) % 62.22/62.45 (step-pop @p1082 :rule scope :premises (@p826)) % 62.22/62.45 (step-pop @p1083 :rule scope :premises (@p1082)) % 62.22/62.45 (step-pop @p1084 :rule scope :premises (@p1083)) % 62.22/62.45 (step-pop @p1085 :rule scope :premises (@p1084)) % 62.22/62.45 (step-pop @p1086 :rule scope :premises (@p1085)) % 62.22/62.45 (step-pop @p1087 :rule scope :premises (@p1086)) % 62.22/62.45 (step-pop @p1088 :rule scope :premises (@p1087)) % 62.22/62.45 (step-pop @p1089 :rule scope :premises (@p1088)) % 62.22/62.45 (step-pop @p1090 :rule scope :premises (@p1089)) % 62.22/62.45 (step-pop @p1091 :rule scope :premises (@p1090)) % 62.22/62.45 (step-pop @p1092 :rule scope :premises (@p1091)) % 62.22/62.45 (step-pop @p1093 :rule scope :premises (@p1092)) % 62.22/62.45 (step-pop @p1094 :rule scope :premises (@p1093)) % 62.22/62.45 (step-pop @p1095 :rule scope :premises (@p1094)) % 62.22/62.45 (step-pop @p1096 :rule scope :premises (@p1095)) % 62.22/62.45 (step-pop @p1097 :rule scope :premises (@p1096)) % 62.22/62.45 (step-pop @p1098 :rule scope :premises (@p1097)) % 62.22/62.45 (step-pop @p1099 :rule scope :premises (@p1098)) % 62.22/62.45 (step-pop @p1100 :rule scope :premises (@p1099)) % 62.22/62.45 (step-pop @p1101 :rule scope :premises (@p1100)) % 62.22/62.45 (step-pop @p1102 :rule scope :premises (@p1101)) % 62.22/62.45 (step-pop @p1103 :rule scope :premises (@p1102)) % 62.22/62.45 (step-pop @p1104 :rule scope :premises (@p1103)) % 62.22/62.45 (step-pop @p1105 :rule scope :premises (@p1104)) % 62.22/62.45 (step-pop @p1106 :rule scope :premises (@p1105)) % 62.22/62.45 (step-pop @p1107 :rule scope :premises (@p1106)) % 62.22/62.45 (step-pop @p1108 :rule scope :premises (@p1107)) % 62.22/62.45 (step-pop @p1109 :rule scope :premises (@p1108)) % 62.22/62.45 (step-pop @p1110 :rule scope :premises (@p1109)) % 62.22/62.45 (step-pop @p1111 :rule scope :premises (@p1110)) % 62.22/62.45 (step-pop @p1112 :rule scope :premises (@p1111)) % 62.22/62.45 (step-pop @p1113 :rule scope :premises (@p1112)) % 62.22/62.45 (step-pop @p1114 :rule scope :premises (@p1113)) % 62.22/62.45 (step-pop @p1115 :rule scope :premises (@p1114)) % 62.22/62.45 (step-pop @p1116 :rule scope :premises (@p1115)) % 62.22/62.45 (step-pop @p1117 :rule scope :premises (@p1116)) % 62.22/62.45 (step-pop @p1118 :rule scope :premises (@p1117)) % 62.22/62.45 (step-pop @p1119 :rule scope :premises (@p1118)) % 62.22/62.45 (step-pop @p1120 :rule scope :premises (@p1119)) % 62.22/62.45 (step-pop @p1121 :rule scope :premises (@p1120)) % 62.22/62.45 (step-pop @p1122 :rule scope :premises (@p1121)) % 62.22/62.45 (step-pop @p1123 :rule scope :premises (@p1122)) % 62.22/62.45 (step-pop @p1124 :rule scope :premises (@p1123)) % 62.22/62.45 (step-pop @p1125 :rule scope :premises (@p1124)) % 62.22/62.45 (step-pop @p1126 :rule scope :premises (@p1125)) % 62.22/62.45 (step-pop @p1127 :rule scope :premises (@p1126)) % 62.22/62.45 (step-pop @p1128 :rule scope :premises (@p1127)) % 62.22/62.45 (step-pop @p1129 :rule scope :premises (@p1128)) % 62.22/62.45 (step-pop @p1130 :rule scope :premises (@p1129)) % 62.22/62.45 (step-pop @p1131 :rule scope :premises (@p1130)) % 62.22/62.45 (step-pop @p1132 :rule scope :premises (@p1131)) % 62.22/62.45 (step-pop @p1133 :rule scope :premises (@p1132)) % 62.22/62.45 (step-pop @p1134 :rule scope :premises (@p1133)) % 62.22/62.45 (step-pop @p1135 :rule scope :premises (@p1134)) % 62.22/62.45 (step-pop @p1136 :rule scope :premises (@p1135)) % 62.22/62.45 (step-pop @p1137 :rule scope :premises (@p1136)) % 62.22/62.45 (step-pop @p1138 :rule scope :premises (@p1137)) % 62.22/62.45 (step-pop @p1139 :rule scope :premises (@p1138)) % 62.22/62.45 (step-pop @p1140 :rule scope :premises (@p1139)) % 62.22/62.45 (step-pop @p1141 :rule scope :premises (@p1140)) % 62.22/62.45 (step-pop @p1142 :rule scope :premises (@p1141)) % 62.22/62.45 (step-pop @p1143 :rule scope :premises (@p1142)) % 62.22/62.45 (step-pop @p1144 :rule scope :premises (@p1143)) % 62.22/62.45 (step-pop @p1145 :rule scope :premises (@p1144)) % 62.22/62.45 (step-pop @p1146 :rule scope :premises (@p1145)) % 62.22/62.45 (step-pop @p1147 :rule scope :premises (@p1146)) % 62.22/62.45 (step-pop @p1148 :rule scope :premises (@p1147)) % 62.22/62.45 (step-pop @p1149 :rule scope :premises (@p1148)) % 62.22/62.45 (step-pop @p1150 :rule scope :premises (@p1149)) % 62.22/62.45 (step-pop @p1151 :rule scope :premises (@p1150)) % 62.22/62.45 (step-pop @p1152 :rule scope :premises (@p1151)) % 62.22/62.45 (step-pop @p1153 :rule scope :premises (@p1152)) % 62.22/62.45 (step-pop @p1154 :rule scope :premises (@p1153)) % 62.22/62.45 (step-pop @p1155 :rule scope :premises (@p1154)) % 62.22/62.45 (step-pop @p1156 :rule scope :premises (@p1155)) % 62.22/62.45 (step-pop @p1157 :rule scope :premises (@p1156)) % 62.22/62.45 (step-pop @p1158 :rule scope :premises (@p1157)) % 62.22/62.45 (step-pop @p1159 :rule scope :premises (@p1158)) % 62.22/62.45 (step-pop @p1160 :rule scope :premises (@p1159)) % 62.22/62.45 (step-pop @p1161 :rule scope :premises (@p1160)) % 62.22/62.45 (step-pop @p1162 :rule scope :premises (@p1161)) % 62.22/62.45 (step-pop @p1163 :rule scope :premises (@p1162)) % 62.22/62.45 (step-pop @p1164 :rule scope :premises (@p1163)) % 62.22/62.45 (step-pop @p1165 :rule scope :premises (@p1164)) % 62.22/62.45 (step-pop @p1166 :rule scope :premises (@p1165)) % 62.22/62.45 (step-pop @p1167 :rule scope :premises (@p1166)) % 62.22/62.45 (step-pop @p1168 :rule scope :premises (@p1167)) % 62.22/62.45 (step-pop @p1169 :rule scope :premises (@p1168)) % 62.22/62.45 (step-pop @p1170 :rule scope :premises (@p1169)) % 62.22/62.45 (step-pop @p1171 :rule scope :premises (@p1170)) % 62.22/62.45 (step-pop @p1172 :rule scope :premises (@p1171)) % 62.22/62.45 (step-pop @p1173 :rule scope :premises (@p1172)) % 62.22/62.45 (step-pop @p1174 :rule scope :premises (@p1173)) % 62.22/62.45 (step-pop @p1175 :rule scope :premises (@p1174)) % 62.22/62.45 (step-pop @p1176 :rule scope :premises (@p1175)) % 62.22/62.45 (step-pop @p1177 :rule scope :premises (@p1176)) % 62.22/62.45 (step-pop @p1178 :rule scope :premises (@p1177)) % 62.22/62.45 (step @p827 :rule process_scope :premises (@p1178) :args (@t492)) % 62.22/62.45 (step @p925 :rule implies_elim :premises (@p827)) % 62.22/62.45 (step @p926 :rule resolution :premises (@p925 @p724) :args (true @t492)) % 62.22/62.45 (step @p927 :rule not_and :premises (@p926)) % 62.22/62.45 (step @p928 :rule eq_resolve :premises (@p927 @p496)) % 62.22/62.45 (step @p929 :rule reordering :premises (@p928) :args ((or @t464 @t462 @t460 @t458 @t456 @t454 @t451 @t450 @t449 @t447 @t444 @t441 @t439 @t436 @t434 @t432 @t428 @t426 @t424 @t422 @t419 @t416 @t412 @t411 @t410 @t407 @t402 @t400 @t397 @t395 @t394 @t391 @t388 @t387 @t110 @t384 @t383 @t381 @t378 @t376 @t375 @t371 @t369 @t367 @t365 @t364 @t360 @t357 @t355 @t353 @t351 @t347 @t344 @t342 @t341 @t337 @t333 @t332 @t331 @t330 @t329 @t327 @t323 @t321 @t319 @t316 @t314 @t312 @t311 @t308 @t304 @t302 @t301 @t300 @t297 @t292 @t291 @t290 @t286 @t283 @t281 @t277 @t273 @t270 @t269 @t267 @t266 @t262 @t261 @t257 @t253 @t250 @t249 @t245 @t241 @t233 @t230))) % 62.22/62.45 (step @p930 false :rule chain_m_resolution :premises (@p929 @p398 @p397 @p396 @p395 @p394 @p393 @p384 @p383 @p382 @p381 @p371 @p370 @p361 @p360 @p351 @p350 @p349 @p348 @p347 @p346 @p345 @p336 @p327 @p326 @p325 @p274 @p265 @p264 @p263 @p262 @p253 @p252 @p251 @p250 @p249 @p248 @p247 @p246 @p237 @p228 @p219 @p210 @p209 @p208 @p199 @p198 @p197 @p196 @p195 @p194 @p193 @p192 @p191 @p181 @p177 @p176 @p175 @p137 @p136 @p126 @p125 @p124 @p123 @p114 @p113 @p104 @p103 @p102 @p93 @p92 @p91 @p87 @p86 @p85 @p76 @p67 @p66 @p65 @p64 @p63 @p62 @p61 @p60 @p59 @p58 @p57 @p56 @p55 @p54 @p50 @p41 @p31 @p30 @p26 @p25 @p24 @p23) :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 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 true 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 @t229 @t232 @t240 @t244 @t248 @t217 @t252 @t256 @t260 @t209 @t265 @t205 @t268 @t199 @t272 @t276 @t280 @t282 @t285 @t289 @t191 @t187 @t296 @t299 @t172 @t164 @t303 @t307 @t310 @t160 @t313 @t315 @t318 @t320 @t322 @t326 @t328 @t153 @t149 @t146 @t142 @t336 @t340 @t138 @t343 @t346 @t350 @t352 @t354 @t356 @t359 @t363 @t124 @t366 @t368 @t370 @t110 @t374 @t104 @t377 @t380 @t382 @t98 @t386 @t91 @t390 @t393 @t83 @t396 @t399 @t401 @t406 @t409 @t77 @t71 @t415 @t418 @t421 @t423 @t425 @t427 @t431 @t433 @t435 @t438 @t440 @t443 @t446 @t448 @t62 @t53 @t453 @t455 @t457 @t459 @t461 @t463))) % 62.22/62.45 ) % 62.22/62.46 % SZS output end Proof % 62.22/62.46 % cvc5 exiting %------------------------------------------------------------------------------