%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : LCL109-6 : TPTP v9.3.1. Released v1.0.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n014.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 11:22:11 AM UTC 2026 % Result : Unsatisfiable 5.65s 6.02s % Output : Proof 5.77s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL109-6 : TPTP v9.3.1. Released v1.0.0. % 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.08/0.34 % Computer : n014.cluster.edu % 0.08/0.34 % Model : x86_64 x86_64 % 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.34 % Memory : 8046.5625MB % 0.08/0.34 % OS : Linux 6.8.0-71-generic % 0.08/0.34 % CPULimit : 300 % 0.08/0.34 % WCLimit : 300 % 0.08/0.34 % DateTime : Fri Sep 4 18:19:58 UTC 2026 % 0.08/0.35 % CPUTime : % 0.18/0.46 %----Proving TF0_NAR, FOF, or CNF % 0.18/0.49 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 5.65/6.02 % SZS status Unsatisfiable % 5.65/6.02 % SZS output start Proof % 5.77/6.08 ( % 5.77/6.08 (declare-sort $$unsorted 0) % 5.77/6.08 (declare-const tptp.b $$unsorted) % 5.77/6.08 (declare-const tptp.a $$unsorted) % 5.77/6.08 (declare-const tptp.falsehood $$unsorted) % 5.77/6.08 (declare-const tptp.implies (-> $$unsorted $$unsorted $$unsorted)) % 5.77/6.08 (declare-const tptp.not (-> $$unsorted $$unsorted)) % 5.77/6.08 (declare-const tptp.xor (-> $$unsorted $$unsorted $$unsorted)) % 5.77/6.08 (declare-const tptp.and_star (-> $$unsorted $$unsorted $$unsorted)) % 5.77/6.08 (declare-const tptp.truth $$unsorted) % 5.77/6.08 (define @t1 () (@var "X" $$unsorted)) % 5.77/6.08 (define @t2 () (tptp.xor @t1 tptp.truth)) % 5.77/6.08 (define @t3 () (@list @t1)) % 5.77/6.08 (define @t4 () (forall @t3 (= (tptp.not @t1) @t2))) % 5.77/6.08 (define @t5 () (tptp.xor @t1 tptp.falsehood)) % 5.77/6.08 (define @t6 () (forall @t3 (= @t5 @t1))) % 5.77/6.08 (define @t7 () (tptp.and_star @t1 tptp.truth)) % 5.77/6.08 (define @t8 () (forall @t3 (= @t7 @t1))) % 5.77/6.08 (define @t9 () (tptp.and_star @t1 tptp.falsehood)) % 5.77/6.08 (define @t10 () (forall @t3 (= @t9 tptp.falsehood))) % 5.77/6.08 (define @t11 () (tptp.xor tptp.truth @t1)) % 5.77/6.08 (define @t12 () (tptp.and_star @t11 @t1)) % 5.77/6.08 (define @t13 () (forall @t3 (= @t12 tptp.falsehood))) % 5.77/6.08 (define @t14 () (@var "Y" $$unsorted)) % 5.77/6.09 (define @t15 () (tptp.xor tptp.truth @t14)) % 5.77/6.09 (define @t16 () (@list @t1 @t14)) % 5.77/6.09 (define @t17 () (forall @t16 (= (tptp.xor @t1 @t15) (tptp.xor @t2 @t14)))) % 5.77/6.09 (define @t18 () (forall @t16 (= (tptp.xor @t1 @t14) (tptp.xor @t14 @t1)))) % 5.77/6.09 (define @t19 () (@var "Z" $$unsorted)) % 5.77/6.09 (define @t20 () (tptp.and_star @t1 @t14)) % 5.77/6.09 (define @t21 () (forall (@list @t1 @t14 @t19) (= (tptp.and_star @t20 @t19) (tptp.and_star @t1 (tptp.and_star @t14 @t19))))) % 5.77/6.09 (define @t22 () (forall @t16 (= @t20 (tptp.and_star @t14 @t1)))) % 5.77/6.09 (define @t23 () (tptp.not tptp.truth)) % 5.77/6.09 (define @t24 () (tptp.implies tptp.b tptp.a)) % 5.77/6.09 (define @t25 () (tptp.implies tptp.a tptp.b)) % 5.77/6.09 (define @t26 () (tptp.implies @t25 @t24)) % 5.77/6.09 (define @t27 () (tptp.implies @t26 @t24)) % 5.77/6.09 (define @t28 () (@list tptp.truth)) % 5.77/6.09 (define @t29 () (@list tptp.b tptp.a)) % 5.77/6.09 (define @t30 () (@list tptp.a)) % 5.77/6.09 (define @t31 () (@list tptp.b)) % 5.77/6.09 (define @t32 () (tptp.xor tptp.truth tptp.b)) % 5.77/6.09 (define @t33 () (tptp.and_star tptp.a @t32)) % 5.77/6.09 (define @t34 () (@list @t33)) % 5.77/6.09 (define @t35 () (tptp.xor tptp.truth tptp.a)) % 5.77/6.09 (define @t36 () (tptp.and_star tptp.b @t35)) % 5.77/6.09 (define @t37 () (@list @t36)) % 5.77/6.09 (define @t38 () (tptp.xor tptp.truth @t24)) % 5.77/6.09 (define @t39 () (tptp.and_star @t25 @t38)) % 5.77/6.09 (define @t40 () (tptp.and_star @t26 @t38)) % 5.77/6.09 (define @t41 () (@list @t40)) % 5.77/6.09 (define @t42 () (@list @t33 @t38)) % 5.77/6.09 (define @t43 () (@list tptp.truth tptp.b)) % 5.77/6.09 (define @t44 () (tptp.not @t36)) % 5.77/6.09 (define @t45 () (tptp.xor @t36 tptp.truth)) % 5.77/6.09 (define @t46 () (= @t44 @t45)) % 5.77/6.09 (define @t47 () (= @t45 @t44)) % 5.77/6.09 (define @t48 () (@list false)) % 5.77/6.09 (define @t49 () (@list @t4)) % 5.77/6.09 (define @t50 () (tptp.xor tptp.truth @t33)) % 5.77/6.09 (define @t51 () (tptp.and_star @t50 @t38)) % 5.77/6.09 (define @t52 () (tptp.not @t51)) % 5.77/6.09 (define @t53 () (tptp.xor @t51 tptp.truth)) % 5.77/6.09 (define @t54 () (= @t52 @t53)) % 5.77/6.09 (define @t55 () (@list @t51)) % 5.77/6.09 (define @t56 () (= @t53 @t52)) % 5.77/6.09 (define @t57 () (tptp.xor tptp.truth @t38)) % 5.77/6.09 (define @t58 () (tptp.and_star @t57 @t39)) % 5.77/6.09 (define @t59 () (tptp.not @t58)) % 5.77/6.09 (define @t60 () (tptp.xor @t58 tptp.truth)) % 5.77/6.09 (define @t61 () (= @t59 @t60)) % 5.77/6.09 (define @t62 () (= @t60 @t59)) % 5.77/6.09 (define @t63 () (@list @t38)) % 5.77/6.09 (define @t64 () (tptp.and_star @t57 @t33)) % 5.77/6.09 (define @t65 () (@list @t64 tptp.truth)) % 5.77/6.09 (define @t66 () (tptp.and_star @t50 tptp.a)) % 5.77/6.09 (define @t67 () (tptp.and_star @t66 @t32)) % 5.77/6.09 (define @t68 () (tptp.and_star @t50 @t33)) % 5.77/6.09 (define @t69 () (= @t67 @t68)) % 5.77/6.09 (define @t70 () (@list @t50 tptp.a @t32)) % 5.77/6.09 (define @t71 () (= @t68 @t67)) % 5.77/6.09 (define @t72 () (@list @t21)) % 5.77/6.09 (define @t73 () (tptp.xor tptp.truth @t36)) % 5.77/6.09 (define @t74 () (tptp.and_star @t73 tptp.b)) % 5.77/6.09 (define @t75 () (tptp.and_star @t74 @t35)) % 5.77/6.09 (define @t76 () (tptp.and_star @t73 @t36)) % 5.77/6.09 (define @t77 () (= @t75 @t76)) % 5.77/6.09 (define @t78 () (@list @t73 tptp.b @t35)) % 5.77/6.09 (define @t79 () (= @t76 @t75)) % 5.77/6.09 (define @t80 () (tptp.xor @t64 tptp.truth)) % 5.77/6.09 (define @t81 () (tptp.and_star @t80 tptp.a)) % 5.77/6.09 (define @t82 () (tptp.and_star @t81 @t32)) % 5.77/6.09 (define @t83 () (tptp.and_star @t80 @t33)) % 5.77/6.09 (define @t84 () (= @t82 @t83)) % 5.77/6.09 (define @t85 () (@list @t80 tptp.a @t32)) % 5.77/6.09 (define @t86 () (= @t83 @t82)) % 5.77/6.09 (define @t87 () (tptp.xor tptp.truth tptp.truth)) % 5.77/6.09 (define @t88 () (tptp.xor tptp.truth @t39)) % 5.77/6.09 (define @t89 () (tptp.and_star @t88 @t38)) % 5.77/6.09 (define @t90 () (tptp.xor @t89 tptp.truth)) % 5.77/6.09 (define @t91 () (tptp.not @t38)) % 5.77/6.09 (define @t92 () (tptp.xor @t38 tptp.truth)) % 5.77/6.09 (define @t93 () (= @t91 @t92)) % 5.77/6.09 (define @t94 () (= @t92 @t91)) % 5.77/6.09 (define @t95 () (tptp.xor tptp.truth @t40)) % 5.77/6.09 (define @t96 () (tptp.and_star @t95 @t38)) % 5.77/6.09 (define @t97 () (tptp.not @t96)) % 5.77/6.09 (define @t98 () (tptp.xor @t96 tptp.truth)) % 5.77/6.09 (define @t99 () (= @t97 @t98)) % 5.77/6.09 (define @t100 () (@list @t96)) % 5.77/6.09 (define @t101 () (= @t98 @t97)) % 5.77/6.09 (define @t102 () (@list @t25)) % 5.77/6.09 (define @t103 () (@list @t64)) % 5.77/6.09 (define @t104 () (tptp.xor tptp.truth @t87)) % 5.77/6.09 (define @t105 () (tptp.xor @t87 tptp.truth)) % 5.77/6.09 (define @t106 () (= @t104 @t105)) % 5.77/6.09 (define @t107 () (= @t105 @t104)) % 5.77/6.09 (define @t108 () (@list @t17)) % 5.77/6.09 (define @t109 () (@list tptp.truth @t25)) % 5.77/6.09 (define @t110 () (@list tptp.a @t24)) % 5.77/6.09 (define @t111 () (tptp.and_star @t90 @t38)) % 5.77/6.09 (define @t112 () (tptp.and_star @t57 @t40)) % 5.77/6.09 (define @t113 () (tptp.xor tptp.truth @t25)) % 5.77/6.09 (define @t114 () (tptp.and_star @t113 @t24)) % 5.77/6.09 (define @t115 () (tptp.and_star @t35 tptp.b)) % 5.77/6.09 (define @t116 () (tptp.xor @t115 tptp.truth)) % 5.77/6.09 (define @t117 () (tptp.and_star @t32 tptp.a)) % 5.77/6.09 (define @t118 () (tptp.xor @t117 tptp.truth)) % 5.77/6.09 (define @t119 () (tptp.and_star @t57 @t38)) % 5.77/6.09 (define @t120 () (tptp.and_star @t38 @t25)) % 5.77/6.09 (define @t121 () (tptp.xor @t120 tptp.truth)) % 5.77/6.09 (define @t122 () (tptp.and_star @t38 @t26)) % 5.77/6.09 (define @t123 () (tptp.xor @t122 tptp.truth)) % 5.77/6.09 (define @t124 () (tptp.xor @t114 tptp.truth)) % 5.77/6.09 (define @t125 () (tptp.xor tptp.truth @t26)) % 5.77/6.09 (define @t126 () (tptp.xor tptp.truth @t64)) % 5.77/6.09 (define @t127 () (tptp.and_star @t126 tptp.a)) % 5.77/6.09 (define @t128 () (tptp.not @t127)) % 5.77/6.09 (define @t129 () (tptp.xor @t127 tptp.truth)) % 5.77/6.09 (define @t130 () (= @t128 @t129)) % 5.77/6.09 (define @t131 () (@list @t127)) % 5.77/6.09 (define @t132 () (= @t129 @t128)) % 5.77/6.09 (define @t133 () (tptp.xor tptp.truth @t58)) % 5.77/6.09 (define @t134 () (tptp.and_star @t133 @t38)) % 5.77/6.09 (define @t135 () (tptp.not @t134)) % 5.77/6.09 (define @t136 () (tptp.xor @t134 tptp.truth)) % 5.77/6.09 (define @t137 () (= @t135 @t136)) % 5.77/6.09 (define @t138 () (@list @t134)) % 5.77/6.09 (define @t139 () (= @t136 @t135)) % 5.77/6.09 (define @t140 () (tptp.and_star @t113 tptp.truth)) % 5.77/6.09 (define @t141 () (tptp.xor @t140 tptp.truth)) % 5.77/6.09 (define @t142 () (tptp.and_star @t32 tptp.truth)) % 5.77/6.09 (define @t143 () (tptp.xor @t142 tptp.truth)) % 5.77/6.09 (define @t144 () (tptp.xor @t33 @t87)) % 5.77/6.09 (define @t145 () (tptp.xor @t33 tptp.truth)) % 5.77/6.09 (define @t146 () (tptp.xor @t145 tptp.truth)) % 5.77/6.09 (define @t147 () (= @t144 @t146)) % 5.77/6.09 (define @t148 () (@list @t33 tptp.truth)) % 5.77/6.09 (define @t149 () (= @t146 @t144)) % 5.77/6.09 (define @t150 () (tptp.xor @t89 @t87)) % 5.77/6.09 (define @t151 () (tptp.xor @t90 tptp.truth)) % 5.77/6.09 (define @t152 () (= @t150 @t151)) % 5.77/6.09 (define @t153 () (= @t151 @t150)) % 5.77/6.09 (define @t154 () (@list @t87 tptp.b)) % 5.77/6.09 (define @t155 () (@list @t80 tptp.truth)) % 5.77/6.09 (define @t156 () (tptp.and_star @t95 @t26)) % 5.77/6.09 (define @t157 () (tptp.and_star @t50 @t64)) % 5.77/6.09 (define @t158 () (tptp.and_star @t35 @t33)) % 5.77/6.09 (define @t159 () (@list @t127 tptp.truth)) % 5.77/6.09 (define @t160 () (tptp.and_star @t35 @t64)) % 5.77/6.09 (define @t161 () (tptp.xor tptp.truth @t90)) % 5.77/6.09 (define @t162 () (tptp.and_star @t161 @t24)) % 5.77/6.09 (define @t163 () (tptp.and_star @t38 tptp.a)) % 5.77/6.09 (define @t164 () (tptp.and_star @t35 @t24)) % 5.77/6.09 (define @t165 () (tptp.and_star @t50 @t57)) % 5.77/6.09 (define @t166 () (tptp.and_star @t165 @t33)) % 5.77/6.09 (define @t167 () (= @t166 @t157)) % 5.77/6.09 (define @t168 () (= @t157 @t166)) % 5.77/6.09 (define @t169 () (tptp.and_star @t35 tptp.a)) % 5.77/6.09 (define @t170 () (tptp.and_star @t169 @t32)) % 5.77/6.09 (define @t171 () (= @t170 @t158)) % 5.77/6.09 (define @t172 () (@list @t35 tptp.a @t32)) % 5.77/6.09 (define @t173 () (= @t158 @t170)) % 5.77/6.09 (define @t174 () (tptp.and_star @t35 @t57)) % 5.77/6.09 (define @t175 () (tptp.and_star @t174 @t33)) % 5.77/6.09 (define @t176 () (= @t175 @t160)) % 5.77/6.09 (define @t177 () (= @t160 @t175)) % 5.77/6.09 (define @t178 () (tptp.and_star @t50 @t32)) % 5.77/6.09 (define @t179 () (tptp.and_star @t32 @t50)) % 5.77/6.09 (define @t180 () (= @t178 @t179)) % 5.77/6.09 (define @t181 () (@list @t50 @t32)) % 5.77/6.09 (define @t182 () (= @t179 @t178)) % 5.77/6.09 (define @t183 () (@list @t22)) % 5.77/6.09 (define @t184 () (tptp.and_star @t25 @t57)) % 5.77/6.09 (define @t185 () (tptp.and_star @t57 @t25)) % 5.77/6.09 (define @t186 () (= @t184 @t185)) % 5.77/6.09 (define @t187 () (@list @t25 @t57)) % 5.77/6.09 (define @t188 () (= @t185 @t184)) % 5.77/6.09 (define @t189 () (@list @t32 tptp.truth)) % 5.77/6.09 (define @t190 () (tptp.xor @t158 tptp.truth)) % 5.77/6.09 (define @t191 () (tptp.xor @t162 tptp.truth)) % 5.77/6.09 (define @t192 () (tptp.and_star @t87 tptp.b)) % 5.77/6.09 (define @t193 () (tptp.xor @t192 tptp.truth)) % 5.77/6.09 (define @t194 () (tptp.xor @t163 tptp.truth)) % 5.77/6.09 (define @t195 () (tptp.and_star tptp.truth @t24)) % 5.77/6.09 (define @t196 () (tptp.and_star @t38 tptp.truth)) % 5.77/6.09 (define @t197 () (tptp.xor @t196 tptp.truth)) % 5.77/6.09 (define @t198 () (@list @t95)) % 5.77/6.09 (define @t199 () (tptp.xor tptp.truth @t35)) % 5.77/6.09 (define @t200 () (@list @t199)) % 5.77/6.09 (define @t201 () (tptp.xor tptp.truth @t179)) % 5.77/6.09 (define @t202 () (tptp.xor @t179 tptp.truth)) % 5.77/6.09 (define @t203 () (= @t201 @t202)) % 5.77/6.09 (define @t204 () (@list tptp.truth @t179)) % 5.77/6.09 (define @t205 () (= @t202 @t201)) % 5.77/6.09 (define @t206 () (@list @t18)) % 5.77/6.09 (define @t207 () (tptp.xor tptp.truth @t74)) % 5.77/6.09 (define @t208 () (tptp.and_star @t207 tptp.a)) % 5.77/6.09 (define @t209 () (tptp.xor tptp.truth @t50)) % 5.77/6.09 (define @t210 () (tptp.and_star @t209 tptp.b)) % 5.77/6.09 (define @t211 () (tptp.and_star @t125 @t24)) % 5.77/6.09 (define @t212 () (tptp.and_star @t60 @t35)) % 5.77/6.09 (define @t213 () (tptp.xor tptp.truth @t57)) % 5.77/6.09 (define @t214 () (tptp.and_star @t213 tptp.a)) % 5.77/6.09 (define @t215 () (tptp.and_star @t214 @t32)) % 5.77/6.09 (define @t216 () (tptp.and_star @t213 @t33)) % 5.77/6.09 (define @t217 () (= @t215 @t216)) % 5.77/6.09 (define @t218 () (@list @t213 tptp.a @t32)) % 5.77/6.09 (define @t219 () (= @t216 @t215)) % 5.77/6.09 (define @t220 () (tptp.xor tptp.truth @t32)) % 5.77/6.09 (define @t221 () (tptp.and_star @t220 tptp.a)) % 5.77/6.09 (define @t222 () (tptp.and_star @t221 @t32)) % 5.77/6.09 (define @t223 () (tptp.and_star @t220 @t33)) % 5.77/6.09 (define @t224 () (= @t222 @t223)) % 5.77/6.09 (define @t225 () (= @t223 @t222)) % 5.77/6.09 (define @t226 () (tptp.xor @t112 tptp.truth)) % 5.77/6.09 (define @t227 () (tptp.and_star tptp.b tptp.a)) % 5.77/6.09 (define @t228 () (tptp.xor @t210 tptp.truth)) % 5.77/6.09 (define @t229 () (tptp.and_star @t113 @t38)) % 5.77/6.09 (define @t230 () (tptp.and_star @t50 @t158)) % 5.77/6.09 (define @t231 () (tptp.not @t230)) % 5.77/6.09 (define @t232 () (tptp.xor @t230 tptp.truth)) % 5.77/6.09 (define @t233 () (= @t231 @t232)) % 5.77/6.09 (define @t234 () (@list @t230)) % 5.77/6.09 (define @t235 () (= @t232 @t231)) % 5.77/6.09 (define @t236 () (tptp.and_star @t199 @t80)) % 5.77/6.09 (define @t237 () (tptp.not @t236)) % 5.77/6.09 (define @t238 () (tptp.xor @t236 tptp.truth)) % 5.77/6.09 (define @t239 () (= @t237 @t238)) % 5.77/6.09 (define @t240 () (= @t238 @t237)) % 5.77/6.09 (define @t241 () (tptp.xor @t127 @t87)) % 5.77/6.09 (define @t242 () (tptp.xor @t129 tptp.truth)) % 5.77/6.09 (define @t243 () (= @t241 @t242)) % 5.77/6.09 (define @t244 () (= @t242 @t241)) % 5.77/6.09 (define @t245 () (tptp.and_star @t125 @t32)) % 5.77/6.09 (define @t246 () (tptp.xor tptp.truth @t245)) % 5.77/6.09 (define @t247 () (tptp.xor @t245 tptp.truth)) % 5.77/6.09 (define @t248 () (= @t246 @t247)) % 5.77/6.09 (define @t249 () (= @t247 @t246)) % 5.77/6.09 (define @t250 () (tptp.xor @t164 tptp.truth)) % 5.77/6.09 (define @t251 () (tptp.and_star @t95 tptp.truth)) % 5.77/6.09 (define @t252 () (tptp.and_star tptp.a tptp.truth)) % 5.77/6.09 (define @t253 () (tptp.xor (tptp.and_star @t220 @t26) tptp.truth)) % 5.77/6.09 (define @t254 () (tptp.and_star @t250 @t123)) % 5.77/6.09 (define @t255 () (tptp.and_star @t202 @t251)) % 5.77/6.09 (define @t256 () (= tptp.falsehood @t23)) % 5.77/6.09 (define @t257 () (= @t23 @t87)) % 5.77/6.09 (define @t258 () (= @t25 @t50)) % 5.77/6.09 (define @t259 () (= @t24 @t73)) % 5.77/6.09 (define @t260 () (= @t26 @t88)) % 5.77/6.09 (define @t261 () (= @t27 @t95)) % 5.77/6.09 (define @t262 () (tptp.and_star @t87 tptp.truth)) % 5.77/6.09 (define @t263 () (= tptp.falsehood @t262)) % 5.77/6.09 (define @t264 () (= tptp.falsehood @t169)) % 5.77/6.09 (define @t265 () (tptp.and_star @t32 tptp.b)) % 5.77/6.09 (define @t266 () (= tptp.falsehood @t265)) % 5.77/6.09 (define @t267 () (tptp.and_star @t38 @t24)) % 5.77/6.09 (define @t268 () (= tptp.falsehood @t267)) % 5.77/6.09 (define @t269 () (= tptp.falsehood @t68)) % 5.77/6.09 (define @t270 () (= tptp.falsehood @t76)) % 5.77/6.09 (define @t271 () (tptp.and_star @t88 @t39)) % 5.77/6.09 (define @t272 () (= tptp.falsehood @t271)) % 5.77/6.09 (define @t273 () (= tptp.falsehood (tptp.and_star @t95 @t40))) % 5.77/6.09 (define @t274 () (tptp.and_star @t53 @t38)) % 5.77/6.09 (define @t275 () (= @t274 @t83)) % 5.77/6.09 (define @t276 () (tptp.and_star @t60 @t39)) % 5.77/6.09 (define @t277 () (= @t111 @t276)) % 5.77/6.09 (define @t278 () (tptp.xor tptp.b tptp.truth)) % 5.77/6.09 (define @t279 () (= @t32 @t278)) % 5.77/6.09 (define @t280 () (= @t38 (tptp.xor @t24 tptp.truth))) % 5.77/6.09 (define @t281 () (= @t50 @t145)) % 5.77/6.09 (define @t282 () (= @t73 @t45)) % 5.77/6.09 (define @t283 () (tptp.xor @t39 tptp.truth)) % 5.77/6.09 (define @t284 () (= @t88 @t283)) % 5.77/6.09 (define @t285 () (tptp.xor @t40 tptp.truth)) % 5.77/6.09 (define @t286 () (= @t95 @t285)) % 5.77/6.09 (define @t287 () (= @t33 @t117)) % 5.77/6.09 (define @t288 () (= @t36 @t115)) % 5.77/6.09 (define @t289 () (= @t39 @t120)) % 5.77/6.09 (define @t290 () (= @t40 @t122)) % 5.77/6.09 (define @t291 () (= tptp.falsehood @t119)) % 5.77/6.09 (define @t292 () (tptp.xor @t45 tptp.truth)) % 5.77/6.09 (define @t293 () (= (tptp.xor @t36 @t87) @t292)) % 5.77/6.09 (define @t294 () (tptp.and_star @t116 tptp.b)) % 5.77/6.09 (define @t295 () (tptp.and_star @t118 tptp.a)) % 5.77/6.09 (define @t296 () (= @t295 @t294)) % 5.77/6.09 (define @t297 () (tptp.and_star @t124 @t24)) % 5.77/6.09 (define @t298 () (tptp.and_star @t121 @t25)) % 5.77/6.09 (define @t299 () (= @t298 @t297)) % 5.77/6.09 (define @t300 () (tptp.xor @t211 tptp.truth)) % 5.77/6.09 (define @t301 () (tptp.and_star @t123 @t26)) % 5.77/6.09 (define @t302 () (= @t301 (tptp.and_star @t300 @t24))) % 5.77/6.09 (define @t303 () (= @t57 @t92)) % 5.77/6.09 (define @t304 () (= @t80 @t126)) % 5.77/6.09 (define @t305 () (= @t60 @t133)) % 5.77/6.09 (define @t306 () (tptp.and_star @t119 @t25)) % 5.77/6.09 (define @t307 () (= @t306 (tptp.and_star @t57 @t120))) % 5.77/6.09 (define @t308 () (= @t262 (tptp.and_star tptp.truth @t87))) % 5.77/6.09 (define @t309 () (tptp.and_star @t39 @t88)) % 5.77/6.09 (define @t310 () (= @t271 @t309)) % 5.77/6.09 (define @t311 () (tptp.and_star @t38 @t90)) % 5.77/6.09 (define @t312 () (= @t111 @t311)) % 5.77/6.09 (define @t313 () (tptp.and_star tptp.b @t32)) % 5.77/6.09 (define @t314 () (= @t265 @t313)) % 5.77/6.09 (define @t315 () (tptp.and_star tptp.a @t35)) % 5.77/6.09 (define @t316 () (= @t169 @t315)) % 5.77/6.09 (define @t317 () (tptp.and_star @t24 @t38)) % 5.77/6.09 (define @t318 () (= @t267 @t317)) % 5.77/6.09 (define @t319 () (tptp.and_star @t33 @t57)) % 5.77/6.09 (define @t320 () (= @t64 @t319)) % 5.77/6.09 (define @t321 () (tptp.and_star @t33 @t80)) % 5.77/6.09 (define @t322 () (= @t83 @t321)) % 5.77/6.09 (define @t323 () (tptp.and_star @t39 @t60)) % 5.77/6.09 (define @t324 () (= @t276 @t323)) % 5.77/6.09 (define @t325 () (= tptp.truth (tptp.xor tptp.truth tptp.falsehood))) % 5.77/6.09 (define @t326 () (tptp.xor @t36 tptp.falsehood)) % 5.77/6.09 (define @t327 () (= @t36 @t326)) % 5.77/6.09 (define @t328 () (tptp.and_star @t40 tptp.truth)) % 5.77/6.09 (define @t329 () (= @t40 @t328)) % 5.77/6.09 (define @t330 () (tptp.and_star @t113 @t25)) % 5.77/6.09 (define @t331 () (= tptp.falsehood @t330)) % 5.77/6.09 (define @t332 () (= tptp.falsehood (tptp.and_star @t126 @t64))) % 5.77/6.09 (define @t333 () (tptp.xor @t87 tptp.b)) % 5.77/6.09 (define @t334 () (= @t220 @t333)) % 5.77/6.09 (define @t335 () (tptp.xor @t80 tptp.truth)) % 5.77/6.09 (define @t336 () (tptp.xor @t64 @t87)) % 5.77/6.09 (define @t337 () (= @t336 @t335)) % 5.77/6.09 (define @t338 () (tptp.xor @t60 tptp.a)) % 5.77/6.09 (define @t339 () (= (tptp.xor @t58 @t35) @t338)) % 5.77/6.09 (define @t340 () (tptp.and_star @t190 @t33)) % 5.77/6.09 (define @t341 () (= (tptp.and_star (tptp.xor @t66 tptp.truth) tptp.a) @t340)) % 5.77/6.09 (define @t342 () (tptp.and_star @t141 tptp.truth)) % 5.77/6.09 (define @t343 () (tptp.and_star @t87 @t25)) % 5.77/6.09 (define @t344 () (tptp.xor @t343 tptp.truth)) % 5.77/6.09 (define @t345 () (tptp.and_star @t344 @t25)) % 5.77/6.09 (define @t346 () (= @t345 @t342)) % 5.77/6.09 (define @t347 () (tptp.and_star @t191 @t24)) % 5.77/6.09 (define @t348 () (tptp.xor @t311 tptp.truth)) % 5.77/6.09 (define @t349 () (= (tptp.and_star @t348 @t90) @t347)) % 5.77/6.09 (define @t350 () (tptp.and_star @t143 tptp.truth)) % 5.77/6.09 (define @t351 () (tptp.and_star @t193 tptp.b)) % 5.77/6.09 (define @t352 () (= @t351 @t350)) % 5.77/6.09 (define @t353 () (tptp.and_star @t194 tptp.a)) % 5.77/6.09 (define @t354 () (tptp.and_star @t250 @t24)) % 5.77/6.09 (define @t355 () (= @t354 @t353)) % 5.77/6.09 (define @t356 () (= @t113 (tptp.xor @t25 tptp.truth))) % 5.77/6.09 (define @t357 () (tptp.xor @t26 tptp.truth)) % 5.77/6.09 (define @t358 () (= @t125 @t357)) % 5.77/6.09 (define @t359 () (tptp.xor @t111 tptp.truth)) % 5.77/6.09 (define @t360 () (= (tptp.xor tptp.truth @t111) @t359)) % 5.77/6.09 (define @t361 () (tptp.xor tptp.truth @t112)) % 5.77/6.09 (define @t362 () (= @t226 @t361)) % 5.77/6.09 (define @t363 () (tptp.xor tptp.truth @t114)) % 5.77/6.09 (define @t364 () (= @t124 @t363)) % 5.77/6.09 (define @t365 () (tptp.and_star @t294 @t32)) % 5.77/6.09 (define @t366 () (= @t365 (tptp.and_star @t116 @t313))) % 5.77/6.09 (define @t367 () (tptp.and_star @t295 @t35)) % 5.77/6.09 (define @t368 () (= @t367 (tptp.and_star @t118 @t315))) % 5.77/6.09 (define @t369 () (tptp.and_star @t25 @t88)) % 5.77/6.09 (define @t370 () (tptp.and_star @t38 @t369)) % 5.77/6.09 (define @t371 () (= (tptp.and_star @t120 @t88) @t370)) % 5.77/6.09 (define @t372 () (tptp.and_star @t25 @t60)) % 5.77/6.09 (define @t373 () (tptp.and_star @t38 @t372)) % 5.77/6.09 (define @t374 () (= (tptp.and_star @t120 @t60) @t373)) % 5.77/6.09 (define @t375 () (tptp.and_star @t64 @t80)) % 5.77/6.09 (define @t376 () (= @t375 (tptp.and_star @t57 @t321))) % 5.77/6.09 (define @t377 () (tptp.and_star tptp.truth @t317)) % 5.77/6.09 (define @t378 () (tptp.and_star @t195 @t38)) % 5.77/6.09 (define @t379 () (= @t378 @t377)) % 5.77/6.09 (define @t380 () (tptp.and_star @t25 @t119)) % 5.77/6.09 (define @t381 () (= @t306 @t380)) % 5.77/6.09 (define @t382 () (= @t298 (tptp.and_star @t25 @t121))) % 5.77/6.09 (define @t383 () (tptp.and_star @t26 @t123)) % 5.77/6.09 (define @t384 () (= @t301 @t383)) % 5.77/6.09 (define @t385 () (= @t112 (tptp.and_star @t40 @t57))) % 5.77/6.09 (define @t386 () (tptp.and_star tptp.a @t80)) % 5.77/6.09 (define @t387 () (= @t81 @t386)) % 5.77/6.09 (define @t388 () (tptp.and_star @t38 @t60)) % 5.77/6.09 (define @t389 () (= (tptp.and_star @t60 @t38) @t388)) % 5.77/6.09 (define @t390 () (tptp.and_star @t24 @t124)) % 5.77/6.09 (define @t391 () (= @t297 @t390)) % 5.77/6.09 (define @t392 () (tptp.and_star @t24 @t125)) % 5.77/6.09 (define @t393 () (= @t211 @t392)) % 5.77/6.09 (define @t394 () (tptp.implies @t113 @t36)) % 5.77/6.09 (define @t395 () (= @t394 (tptp.xor tptp.truth (tptp.and_star @t113 @t73)))) % 5.77/6.09 (define @t396 () (tptp.xor tptp.truth @t319)) % 5.77/6.09 (define @t397 () (= (tptp.implies @t33 @t38) @t396)) % 5.77/6.09 (define @t398 () (= @t64 (tptp.xor @t64 tptp.falsehood))) % 5.77/6.09 (define @t399 () (= @t25 (tptp.and_star @t25 tptp.truth))) % 5.77/6.09 (define @t400 () (= @t32 @t142)) % 5.77/6.09 (define @t401 () (= @t38 @t196)) % 5.77/6.09 (define @t402 () (tptp.and_star @t80 tptp.truth)) % 5.77/6.09 (define @t403 () (= @t80 @t402)) % 5.77/6.09 (define @t404 () (= @t113 @t140)) % 5.77/6.09 (define @t405 () (= @t141 @t342)) % 5.77/6.09 (define @t406 () (= @t143 @t350)) % 5.77/6.09 (define @t407 () (tptp.xor @t87 @t35)) % 5.77/6.09 (define @t408 () (tptp.xor tptp.truth @t199)) % 5.77/6.09 (define @t409 () (= @t408 @t407)) % 5.77/6.09 (define @t410 () (tptp.xor @t51 @t87)) % 5.77/6.09 (define @t411 () (= @t410 (tptp.xor @t53 tptp.truth))) % 5.77/6.09 (define @t412 () (tptp.xor @t87 tptp.a)) % 5.77/6.09 (define @t413 () (= @t199 @t412)) % 5.77/6.09 (define @t414 () (tptp.and_star @t228 tptp.b)) % 5.77/6.09 (define @t415 () (= (tptp.and_star @t202 @t50) @t414)) % 5.77/6.09 (define @t416 () (tptp.xor tptp.b @t87)) % 5.77/6.09 (define @t417 () (= @t333 @t416)) % 5.77/6.09 (define @t418 () (tptp.xor tptp.truth @t80)) % 5.77/6.09 (define @t419 () (= @t335 @t418)) % 5.77/6.09 (define @t420 () (tptp.xor tptp.truth @t156)) % 5.77/6.09 (define @t421 () (= (tptp.xor @t156 tptp.truth) @t420)) % 5.77/6.09 (define @t422 () (tptp.xor @t74 tptp.truth)) % 5.77/6.09 (define @t423 () (= @t422 @t207)) % 5.77/6.09 (define @t424 () (= @t161 @t151)) % 5.77/6.09 (define @t425 () (= @t220 (tptp.xor @t32 tptp.truth))) % 5.77/6.09 (define @t426 () (tptp.xor tptp.truth @t157)) % 5.77/6.09 (define @t427 () (= (tptp.xor @t157 tptp.truth) @t426)) % 5.77/6.09 (define @t428 () (tptp.xor tptp.truth @t158)) % 5.77/6.09 (define @t429 () (= @t190 @t428)) % 5.77/6.09 (define @t430 () (= @t129 (tptp.xor tptp.truth @t127))) % 5.77/6.09 (define @t431 () (tptp.xor tptp.truth @t160)) % 5.77/6.09 (define @t432 () (= (tptp.xor @t160 tptp.truth) @t431)) % 5.77/6.09 (define @t433 () (= @t141 (tptp.xor tptp.truth @t140))) % 5.77/6.09 (define @t434 () (tptp.xor tptp.truth @t162)) % 5.77/6.09 (define @t435 () (= @t191 @t434)) % 5.77/6.09 (define @t436 () (= @t194 (tptp.xor tptp.truth @t163))) % 5.77/6.09 (define @t437 () (tptp.xor tptp.truth @t164)) % 5.77/6.09 (define @t438 () (= @t250 @t437)) % 5.77/6.09 (define @t439 () (tptp.and_star tptp.b @t26)) % 5.77/6.09 (define @t440 () (tptp.and_star @t115 @t26)) % 5.77/6.09 (define @t441 () (= @t440 (tptp.and_star @t35 @t439))) % 5.77/6.09 (define @t442 () (tptp.and_star @t35 @t227)) % 5.77/6.09 (define @t443 () (tptp.and_star @t115 tptp.a)) % 5.77/6.09 (define @t444 () (= @t443 @t442)) % 5.77/6.09 (define @t445 () (tptp.and_star @t60 @t115)) % 5.77/6.09 (define @t446 () (tptp.and_star @t212 tptp.b)) % 5.77/6.09 (define @t447 () (= @t446 @t445)) % 5.77/6.09 (define @t448 () (tptp.and_star @t267 @t124)) % 5.77/6.09 (define @t449 () (= @t448 (tptp.and_star @t38 @t390))) % 5.77/6.09 (define @t450 () (tptp.and_star tptp.b @t87)) % 5.77/6.09 (define @t451 () (= @t192 @t450)) % 5.77/6.09 (define @t452 () (= @t157 (tptp.and_star @t64 @t50))) % 5.77/6.09 (define @t453 () (= @t372 (tptp.and_star @t60 @t25))) % 5.77/6.09 (define @t454 () (= @t142 (tptp.and_star tptp.truth @t32))) % 5.77/6.09 (define @t455 () (= @t158 (tptp.and_star @t33 @t35))) % 5.77/6.09 (define @t456 () (tptp.and_star @t24 @t35)) % 5.77/6.09 (define @t457 () (= @t164 @t456)) % 5.77/6.09 (define @t458 () (= @t160 (tptp.and_star @t64 @t35))) % 5.77/6.09 (define @t459 () (tptp.and_star tptp.a @t38)) % 5.77/6.09 (define @t460 () (= @t163 @t459)) % 5.77/6.09 (define @t461 () (tptp.and_star @t80 @t64)) % 5.77/6.09 (define @t462 () (= @t375 @t461)) % 5.77/6.09 (define @t463 () (tptp.and_star @t126 @t26)) % 5.77/6.09 (define @t464 () (= @t463 (tptp.and_star @t26 @t126))) % 5.77/6.09 (define @t465 () (tptp.and_star tptp.truth @t80)) % 5.77/6.09 (define @t466 () (= @t402 @t465)) % 5.77/6.09 (define @t467 () (= @t330 (tptp.and_star @t25 @t113))) % 5.77/6.09 (define @t468 () (tptp.and_star @t38 @t113)) % 5.77/6.09 (define @t469 () (= @t229 @t468)) % 5.77/6.09 (define @t470 () (tptp.and_star tptp.truth @t113)) % 5.77/6.09 (define @t471 () (= @t140 @t470)) % 5.77/6.09 (define @t472 () (= @t340 (tptp.and_star @t33 @t190))) % 5.77/6.09 (define @t473 () (tptp.and_star @t24 @t191)) % 5.77/6.09 (define @t474 () (= @t347 @t473)) % 5.77/6.09 (define @t475 () (tptp.and_star tptp.b @t193)) % 5.77/6.09 (define @t476 () (= @t351 @t475)) % 5.77/6.09 (define @t477 () (tptp.and_star tptp.truth @t143)) % 5.77/6.09 (define @t478 () (= @t350 @t477)) % 5.77/6.09 (define @t479 () (= @t353 (tptp.and_star tptp.a @t194))) % 5.77/6.09 (define @t480 () (tptp.and_star @t38 @t195)) % 5.77/6.09 (define @t481 () (= @t378 @t480)) % 5.77/6.09 (define @t482 () (tptp.implies @t161 @t36)) % 5.77/6.09 (define @t483 () (= @t482 (tptp.xor tptp.truth (tptp.and_star @t161 @t73)))) % 5.77/6.09 (define @t484 () (tptp.and_star @t40 @t73)) % 5.77/6.09 (define @t485 () (tptp.xor tptp.truth @t484)) % 5.77/6.09 (define @t486 () (= (tptp.implies @t40 @t36) @t485)) % 5.77/6.09 (define @t487 () (= tptp.b (tptp.xor tptp.b tptp.falsehood))) % 5.77/6.09 (define @t488 () (tptp.xor @t33 tptp.falsehood)) % 5.77/6.09 (define @t489 () (= @t33 @t488)) % 5.77/6.09 (define @t490 () (= @t89 (tptp.xor @t89 tptp.falsehood))) % 5.77/6.09 (define @t491 () (= @t51 (tptp.xor @t51 tptp.falsehood))) % 5.77/6.09 (define @t492 () (= @t197 (tptp.and_star @t197 tptp.truth))) % 5.77/6.09 (define @t493 () (= tptp.falsehood (tptp.and_star @t95 tptp.falsehood))) % 5.77/6.09 (define @t494 () (= tptp.falsehood (tptp.and_star @t38 tptp.falsehood))) % 5.77/6.09 (define @t495 () (tptp.and_star tptp.b tptp.falsehood)) % 5.77/6.09 (define @t496 () (= tptp.falsehood @t495)) % 5.77/6.09 (define @t497 () (tptp.and_star @t408 @t199)) % 5.77/6.09 (define @t498 () (= tptp.falsehood @t497)) % 5.77/6.09 (define @t499 () (tptp.and_star @t428 @t33)) % 5.77/6.09 (define @t500 () (tptp.xor @t499 tptp.truth)) % 5.77/6.09 (define @t501 () (tptp.and_star @t500 @t33)) % 5.77/6.09 (define @t502 () (= @t501 (tptp.and_star @t232 @t158))) % 5.77/6.09 (define @t503 () (tptp.and_star @t220 tptp.truth)) % 5.77/6.09 (define @t504 () (tptp.xor @t503 tptp.truth)) % 5.77/6.09 (define @t505 () (tptp.and_star @t504 tptp.truth)) % 5.77/6.09 (define @t506 () (= @t505 (tptp.and_star (tptp.xor (tptp.and_star @t87 @t32) tptp.truth) @t32))) % 5.77/6.09 (define @t507 () (tptp.and_star @t253 @t26)) % 5.77/6.09 (define @t508 () (tptp.and_star @t247 @t32)) % 5.77/6.09 (define @t509 () (= @t508 @t507)) % 5.77/6.09 (define @t510 () (tptp.and_star @t418 @t50)) % 5.77/6.09 (define @t511 () (tptp.xor @t510 tptp.truth)) % 5.77/6.09 (define @t512 () (tptp.and_star @t511 @t50)) % 5.77/6.09 (define @t513 () (= @t512 (tptp.and_star (tptp.xor (tptp.and_star @t209 @t80) tptp.truth) @t80))) % 5.77/6.09 (define @t514 () (tptp.and_star @t238 @t80)) % 5.77/6.09 (define @t515 () (tptp.and_star @t418 @t35)) % 5.77/6.09 (define @t516 () (tptp.xor @t515 tptp.truth)) % 5.77/6.09 (define @t517 () (tptp.and_star @t516 @t35)) % 5.77/6.09 (define @t518 () (= @t517 @t514)) % 5.77/6.09 (define @t519 () (tptp.xor tptp.a @t87)) % 5.77/6.09 (define @t520 () (= @t412 @t519)) % 5.77/6.09 (define @t521 () (tptp.xor tptp.truth @t208)) % 5.77/6.09 (define @t522 () (= (tptp.xor @t208 tptp.truth) @t521)) % 5.77/6.09 (define @t523 () (tptp.xor tptp.truth @t210)) % 5.77/6.09 (define @t524 () (= @t228 @t523)) % 5.77/6.09 (define @t525 () (tptp.and_star tptp.truth @t229)) % 5.77/6.09 (define @t526 () (= (tptp.and_star @t470 @t38) @t525)) % 5.77/6.09 (define @t527 () (tptp.and_star @t446 @t211)) % 5.77/6.09 (define @t528 () (= @t527 (tptp.and_star @t212 (tptp.and_star tptp.b @t211)))) % 5.77/6.09 (define @t529 () (tptp.and_star @t25 @t33)) % 5.77/6.09 (define @t530 () (tptp.and_star @t57 @t529)) % 5.77/6.09 (define @t531 () (= (tptp.and_star @t185 @t33) @t530)) % 5.77/6.09 (define @t532 () (tptp.and_star @t468 @t25)) % 5.77/6.09 (define @t533 () (= @t532 (tptp.and_star @t38 @t330))) % 5.77/6.09 (define @t534 () (tptp.and_star @t73 @t158)) % 5.77/6.09 (define @t535 () (tptp.and_star @t73 @t35)) % 5.77/6.09 (define @t536 () (= (tptp.and_star @t535 @t33) @t534)) % 5.77/6.09 (define @t537 () (tptp.and_star @t212 @t313)) % 5.77/6.09 (define @t538 () (= (tptp.and_star @t446 @t32) @t537)) % 5.77/6.09 (define @t539 () (tptp.and_star @t190 @t32)) % 5.77/6.09 (define @t540 () (tptp.and_star @t539 tptp.a)) % 5.77/6.09 (define @t541 () (= @t540 (tptp.and_star @t190 @t117))) % 5.77/6.09 (define @t542 () (tptp.and_star tptp.a @t465)) % 5.77/6.09 (define @t543 () (tptp.and_star @t252 @t80)) % 5.77/6.09 (define @t544 () (= @t543 @t542)) % 5.77/6.09 (define @t545 () (tptp.and_star @t199 @t212)) % 5.77/6.09 (define @t546 () (tptp.and_star @t545 tptp.b)) % 5.77/6.09 (define @t547 () (= @t546 (tptp.and_star @t199 @t446))) % 5.77/6.09 (define @t548 () (tptp.and_star @t95 @t80)) % 5.77/6.09 (define @t549 () (tptp.and_star @t32 @t548)) % 5.77/6.09 (define @t550 () (tptp.and_star @t32 @t95)) % 5.77/6.09 (define @t551 () (= (tptp.and_star @t550 @t80) @t549)) % 5.77/6.09 (define @t552 () (tptp.and_star @t226 @t32)) % 5.77/6.09 (define @t553 () (tptp.and_star @t226 @t552)) % 5.77/6.09 (define @t554 () (tptp.and_star (tptp.and_star @t226 @t226) @t32)) % 5.77/6.09 (define @t555 () (= @t554 @t553)) % 5.77/6.09 (define @t556 () (tptp.and_star @t95 @t465)) % 5.77/6.09 (define @t557 () (tptp.and_star @t251 @t80)) % 5.77/6.09 (define @t558 () (= @t557 @t556)) % 5.77/6.09 (define @t559 () (tptp.and_star tptp.truth @t477)) % 5.77/6.09 (define @t560 () (tptp.and_star (tptp.and_star tptp.truth tptp.truth) @t143)) % 5.77/6.09 (define @t561 () (= @t560 @t559)) % 5.77/6.09 (define @t562 () (tptp.and_star tptp.a tptp.b)) % 5.77/6.09 (define @t563 () (= @t227 @t562)) % 5.77/6.09 (define @t564 () (tptp.and_star @t227 @t35)) % 5.77/6.09 (define @t565 () (= @t442 @t564)) % 5.77/6.09 (define @t566 () (tptp.and_star tptp.a @t226)) % 5.77/6.09 (define @t567 () (= (tptp.and_star @t226 tptp.a) @t566)) % 5.77/6.09 (define @t568 () (tptp.and_star @t35 @t60)) % 5.77/6.09 (define @t569 () (= @t212 @t568)) % 5.77/6.09 (define @t570 () (tptp.and_star tptp.b @t209)) % 5.77/6.09 (define @t571 () (= @t210 @t570)) % 5.77/6.09 (define @t572 () (tptp.and_star @t32 @t125)) % 5.77/6.09 (define @t573 () (= @t245 @t572)) % 5.77/6.09 (define @t574 () (tptp.and_star @t199 @t36)) % 5.77/6.09 (define @t575 () (= @t574 (tptp.and_star @t36 @t199))) % 5.77/6.09 (define @t576 () (tptp.and_star tptp.b @t228)) % 5.77/6.09 (define @t577 () (= @t414 @t576)) % 5.77/6.09 (define @t578 () (= @t446 (tptp.and_star tptp.b @t212))) % 5.77/6.09 (define @t579 () (tptp.and_star @t25 @t229)) % 5.77/6.09 (define @t580 () (= (tptp.and_star @t229 @t25) @t579)) % 5.77/6.09 (define @t581 () (tptp.implies @t199 @t24)) % 5.77/6.09 (define @t582 () (= @t581 (tptp.xor tptp.truth (tptp.and_star @t199 @t38)))) % 5.77/6.09 (define @t583 () (tptp.xor tptp.truth @t459)) % 5.77/6.09 (define @t584 () (= (tptp.implies tptp.a @t24) @t583)) % 5.77/6.09 (define @t585 () (= tptp.a (tptp.xor tptp.a tptp.falsehood))) % 5.77/6.09 (define @t586 () (= tptp.a @t252)) % 5.77/6.09 (define @t587 () (= @t95 @t251)) % 5.77/6.09 (define @t588 () (tptp.and_star @t35 tptp.truth)) % 5.77/6.09 (define @t589 () (= @t35 @t588)) % 5.77/6.09 (define @t590 () (= tptp.falsehood (tptp.and_star @t199 tptp.falsehood))) % 5.77/6.09 (define @t591 () (tptp.and_star @t199 @t32)) % 5.77/6.09 (define @t592 () (tptp.xor @t591 tptp.truth)) % 5.77/6.09 (define @t593 () (tptp.and_star @t592 @t32)) % 5.77/6.09 (define @t594 () (= (tptp.and_star (tptp.xor (tptp.and_star @t220 @t35) tptp.truth) @t35) @t593)) % 5.77/6.09 (define @t595 () (= @t242 (tptp.xor tptp.truth @t129))) % 5.77/6.09 (define @t596 () (tptp.and_star @t38 @t32)) % 5.77/6.09 (define @t597 () (tptp.and_star @t90 @t596)) % 5.77/6.09 (define @t598 () (= (tptp.and_star @t111 @t32) @t597)) % 5.77/6.09 (define @t599 () (tptp.and_star tptp.a @t313)) % 5.77/6.09 (define @t600 () (= (tptp.and_star @t562 @t32) @t599)) % 5.77/6.09 (define @t601 () (tptp.and_star @t254 @t26)) % 5.77/6.09 (define @t602 () (= @t601 (tptp.and_star @t250 @t301))) % 5.77/6.09 (define @t603 () (tptp.and_star @t202 @t557)) % 5.77/6.09 (define @t604 () (tptp.and_star @t255 @t80)) % 5.77/6.09 (define @t605 () (= @t604 @t603)) % 5.77/6.09 (define @t606 () (tptp.and_star @t35 @t543)) % 5.77/6.09 (define @t607 () (= (tptp.and_star (tptp.and_star @t35 @t252) @t80) @t606)) % 5.77/6.09 (define @t608 () (tptp.and_star @t26 @t253)) % 5.77/6.09 (define @t609 () (= @t507 @t608)) % 5.77/6.09 (define @t610 () (tptp.and_star @t80 @t238)) % 5.77/6.09 (define @t611 () (= @t514 @t610)) % 5.77/6.09 (define @t612 () (= @t127 (tptp.xor @t127 tptp.falsehood))) % 5.77/6.09 (define @t613 () (tptp.and_star @t26 @t80)) % 5.77/6.09 (define @t614 () (tptp.and_star @t254 @t613)) % 5.77/6.09 (define @t615 () (= (tptp.and_star @t601 @t80) @t614)) % 5.77/6.09 (define @t616 () (tptp.and_star @t604 @t26)) % 5.77/6.09 (define @t617 () (= @t616 (tptp.and_star @t255 (tptp.and_star @t80 @t26)))) % 5.77/6.09 (define @t618 () (tptp.and_star @t38 @t73)) % 5.77/6.09 (define @t619 () (tptp.xor tptp.truth @t618)) % 5.77/6.09 (define @t620 () (tptp.xor tptp.truth @t328)) % 5.77/6.09 (define @t621 () (tptp.and_star @t620 @t40)) % 5.77/6.09 (define @t622 () (tptp.xor @t621 tptp.truth)) % 5.77/6.09 (define @t623 () (tptp.and_star @t38 @t58)) % 5.77/6.09 (define @t624 () (tptp.and_star @t119 @t50)) % 5.77/6.09 (define @t625 () (tptp.xor tptp.truth @t81)) % 5.77/6.09 (define @t626 () (tptp.xor tptp.truth @t625)) % 5.77/6.09 (define @t627 () (tptp.and_star @t626 @t32)) % 5.77/6.09 (define @t628 () (tptp.xor @t278 tptp.truth)) % 5.77/6.09 (define @t629 () (tptp.and_star @t133 @t143)) % 5.77/6.09 (define @t630 () (tptp.and_star @t33 @t428)) % 5.77/6.09 (define @t631 () (tptp.and_star tptp.truth @t35)) % 5.77/6.09 (define @t632 () (tptp.and_star @t300 @t73)) % 5.77/6.09 (define @t633 () (tptp.and_star @t220 @t212)) % 5.77/6.09 (define @t634 () (tptp.and_star @t126 @t33)) % 5.77/6.09 (define @t635 () (tptp.and_star @t33 @t212)) % 5.77/6.09 (define @t636 () (tptp.xor tptp.truth @t124)) % 5.77/6.09 (define @t637 () (tptp.and_star @t418 @t212)) % 5.77/6.09 (define @t638 () (tptp.xor @t637 tptp.truth)) % 5.77/6.09 (define @t639 () (tptp.and_star @t209 @t220)) % 5.77/6.09 (define @t640 () (tptp.and_star @t550 @t126)) % 5.77/6.09 (define @t641 () (tptp.and_star @t545 @t220)) % 5.77/6.09 (define @t642 () (tptp.and_star tptp.truth tptp.a)) % 5.77/6.09 (define @t643 () (= tptp.truth @t27)) % 5.77/6.09 (define @t644 () (and @t256 @t257 @t258 @t259 @t260 @t261 @t263 @t264 @t266 @t268 @t269 @t270 @t272 @t273 @t275 @t277 @t279 @t280 @t281 @t282 @t284 @t286 @t287 @t288 @t289 @t290 @t47 @t56 @t62 @t291 @t293 @t296 @t299 @t302 @t303 @t304 @t305 @t71 @t79 @t86 @t307 @t308 @t310 @t312 @t314 @t316 @t318 @t320 @t322 @t324 @t94 @t101 @t325 @t327 @t329 @t331 @t332 @t107 @t334 @t337 @t339 @t341 @t346 @t349 @t352 @t355 @t356 @t358 @t360 @t362 @t364 @t366 @t368 @t371 @t374 @t376 @t379 @t381 @t382 @t384 @t385 @t387 @t389 @t391 @t393 @t395 @t397 @t132 @t139 @t398 @t399 @t400 @t401 @t403 @t404 @t405 @t406 @t409 @t149 @t411 @t413 @t153 @t415 @t417 @t419 @t421 @t423 @t424 @t425 @t427 @t429 @t430 @t432 @t433 @t435 @t436 @t438 @t441 @t444 @t447 @t168 @t173 @t177 @t449 @t451 @t182 @t188 @t452 @t453 @t454 @t455 @t457 @t458 @t460 @t462 @t464 @t466 @t467 @t469 @t471 @t472 @t474 @t476 @t478 @t479 @t481 @t483 @t486 @t487 @t489 @t490 @t491 @t492 @t493 @t494 @t496 @t498 @t502 @t506 @t509 @t513 @t518 @t520 @t205 @t522 @t524 @t526 @t528 @t531 @t533 @t536 @t538 @t541 @t544 @t219 @t225 @t547 @t551 @t555 @t558 @t561 @t563 @t565 @t567 @t569 @t571 @t573 @t575 @t577 @t578 @t580 @t582 @t584 @t235 @t240 @t585 @t586 @t587 @t589 @t590 @t244 @t594 @t249 @t595 @t598 @t600 @t602 @t605 @t607 @t609 @t611 @t612 @t615 @t617)) % 5.77/6.09 (assume @p1 @t4) % 5.77/6.09 (assume @p2 @t6) % 5.77/6.09 (assume @p3 (forall @t3 (= (tptp.xor @t1 @t1) tptp.falsehood))) % 5.77/6.09 (assume @p4 @t8) % 5.77/6.09 (assume @p5 @t10) % 5.77/6.09 (assume @p6 @t13) % 5.77/6.09 (assume @p7 @t17) % 5.77/6.09 (assume @p8 (forall @t16 (= (tptp.and_star (tptp.xor (tptp.and_star @t11 @t14) tptp.truth) @t14) (tptp.and_star (tptp.xor (tptp.and_star @t15 @t1) tptp.truth) @t1)))) % 5.77/6.09 (assume @p9 @t18) % 5.77/6.09 (assume @p10 @t21) % 5.77/6.09 (assume @p11 @t22) % 5.77/6.09 (assume @p12 (= @t23 tptp.falsehood)) % 5.77/6.09 (assume @p13 (forall @t16 (= (tptp.implies @t1 @t14) (tptp.xor tptp.truth (tptp.and_star @t1 @t15))))) % 5.77/6.09 (assume @p14 (not (= @t27 tptp.truth))) % 5.77/6.09 (step @p15 :rule symm :premises (@p12)) % 5.77/6.09 (step @p16 :rule symm :premises (@p14)) % 5.77/6.09 (step @p17 :rule instantiate :premises (@p1) :args (@t28)) % 5.77/6.09 (step @p18 :rule instantiate :premises (@p13) :args ((@list tptp.a tptp.b))) % 5.77/6.09 (step @p19 :rule instantiate :premises (@p13) :args (@t29)) % 5.77/6.09 (step @p20 :rule instantiate :premises (@p13) :args ((@list @t25 @t24))) % 5.77/6.09 (step @p21 :rule instantiate :premises (@p13) :args ((@list @t26 @t24))) % 5.77/6.09 (step @p22 :rule eq-symm :args (@t12 tptp.falsehood)) % 5.77/6.09 (step @p23 :rule cong :premises (@p22) :args (@t13)) % 5.77/6.09 (step @p24 :rule eq_resolve :premises (@p6 @p23)) % 5.77/6.09 (step @p25 :rule instantiate :premises (@p24) :args (@t28)) % 5.77/6.09 (step @p26 :rule instantiate :premises (@p24) :args (@t30)) % 5.77/6.09 (step @p27 :rule instantiate :premises (@p24) :args (@t31)) % 5.77/6.09 (step @p28 :rule instantiate :premises (@p24) :args ((@list @t24))) % 5.77/6.09 (step @p29 :rule instantiate :premises (@p24) :args (@t34)) % 5.77/6.09 (step @p30 :rule instantiate :premises (@p24) :args (@t37)) % 5.77/6.09 (step @p31 :rule instantiate :premises (@p24) :args ((@list @t39))) % 5.77/6.09 (step @p32 :rule instantiate :premises (@p24) :args (@t41)) % 5.77/6.09 (step @p33 :rule instantiate :premises (@p8) :args (@t42)) % 5.77/6.09 (step @p34 :rule instantiate :premises (@p8) :args ((@list @t39 @t38))) % 5.77/6.09 (step @p35 :rule instantiate :premises (@p9) :args (@t43)) % 5.77/6.09 (step @p36 :rule instantiate :premises (@p9) :args ((@list tptp.truth @t24))) % 5.77/6.09 (step @p37 :rule instantiate :premises (@p9) :args ((@list tptp.truth @t33))) % 5.77/6.09 (step @p38 :rule instantiate :premises (@p9) :args ((@list tptp.truth @t36))) % 5.77/6.09 (step @p39 :rule instantiate :premises (@p9) :args ((@list tptp.truth @t39))) % 5.77/6.09 (step @p40 :rule instantiate :premises (@p9) :args ((@list tptp.truth @t40))) % 5.77/6.09 (step @p41 :rule instantiate :premises (@p11) :args ((@list tptp.a @t32))) % 5.77/6.09 (step @p42 :rule instantiate :premises (@p11) :args ((@list tptp.b @t35))) % 5.77/6.09 (step @p43 :rule instantiate :premises (@p11) :args ((@list @t25 @t38))) % 5.77/6.09 (step @p44 :rule instantiate :premises (@p11) :args ((@list @t26 @t38))) % 5.77/6.09 (step @p45 :rule eq-symm :args (@t44 @t45)) % 5.77/6.09 (step @p46 :rule refl :args (@t4)) % 5.77/6.09 (step @p47 :rule cong :premises (@p46 @p45) :args ((=> @t4 @t46))) % 5.77/6.09 (assume-push @p1686 @t4) % 5.77/6.09 (step @p49 :rule instantiate :premises (@p1) :args (@t37)) % 5.77/6.09 (step-pop @p1687 :rule scope :premises (@p49)) % 5.77/6.09 (step @p50 :rule process_scope :premises (@p1687) :args (@t46)) % 5.77/6.09 (step @p52 :rule eq_resolve :premises (@p50 @p47)) % 5.77/6.09 (step @p53 :rule implies_elim :premises (@p52)) % 5.77/6.09 (step @p54 :rule chain_m_resolution :premises (@p53 @p1) :args (@t47 @t48 @t49)) % 5.77/6.09 (step @p55 :rule eq-symm :args (@t52 @t53)) % 5.77/6.09 (step @p56 :rule cong :premises (@p46 @p55) :args ((=> @t4 @t54))) % 5.77/6.09 (assume-push @p1688 @t4) % 5.77/6.09 (step @p58 :rule instantiate :premises (@p1) :args (@t55)) % 5.77/6.09 (step-pop @p1689 :rule scope :premises (@p58)) % 5.77/6.09 (step @p59 :rule process_scope :premises (@p1689) :args (@t54)) % 5.77/6.09 (step @p61 :rule eq_resolve :premises (@p59 @p56)) % 5.77/6.09 (step @p62 :rule implies_elim :premises (@p61)) % 5.77/6.09 (step @p63 :rule chain_m_resolution :premises (@p62 @p1) :args (@t56 @t48 @t49)) % 5.77/6.09 (step @p64 :rule eq-symm :args (@t59 @t60)) % 5.77/6.09 (step @p65 :rule cong :premises (@p46 @p64) :args ((=> @t4 @t61))) % 5.77/6.09 (assume-push @p1690 @t4) % 5.77/6.09 (step @p67 :rule instantiate :premises (@p1) :args ((@list @t58))) % 5.77/6.09 (step-pop @p1691 :rule scope :premises (@p67)) % 5.77/6.09 (step @p68 :rule process_scope :premises (@p1691) :args (@t61)) % 5.77/6.09 (step @p70 :rule eq_resolve :premises (@p68 @p65)) % 5.77/6.09 (step @p71 :rule implies_elim :premises (@p70)) % 5.77/6.09 (step @p72 :rule chain_m_resolution :premises (@p71 @p1) :args (@t62 @t48 @t49)) % 5.77/6.09 (step @p73 :rule instantiate :premises (@p24) :args (@t63)) % 5.77/6.09 (step @p74 :rule instantiate :premises (@p7) :args ((@list @t36 tptp.truth))) % 5.77/6.09 (step @p75 :rule instantiate :premises (@p8) :args (@t29)) % 5.77/6.09 (step @p76 :rule instantiate :premises (@p8) :args ((@list @t24 @t25))) % 5.77/6.09 (step @p77 :rule instantiate :premises (@p8) :args ((@list @t24 @t26))) % 5.77/6.09 (step @p78 :rule instantiate :premises (@p9) :args ((@list tptp.truth @t38))) % 5.77/6.09 (step @p79 :rule instantiate :premises (@p9) :args (@t65)) % 5.77/6.09 (step @p80 :rule instantiate :premises (@p9) :args ((@list @t58 tptp.truth))) % 5.77/6.09 (step @p81 :rule eq-symm :args (@t67 @t68)) % 5.77/6.09 (step @p82 :rule refl :args (@t21)) % 5.77/6.09 (step @p83 :rule cong :premises (@p82 @p81) :args ((=> @t21 @t69))) % 5.77/6.09 (assume-push @p1692 @t21) % 5.77/6.09 (step @p85 :rule instantiate :premises (@p10) :args (@t70)) % 5.77/6.09 (step-pop @p1693 :rule scope :premises (@p85)) % 5.77/6.09 (step @p86 :rule process_scope :premises (@p1693) :args (@t69)) % 5.77/6.09 (step @p88 :rule eq_resolve :premises (@p86 @p83)) % 5.77/6.09 (step @p89 :rule implies_elim :premises (@p88)) % 5.77/6.09 (step @p90 :rule chain_m_resolution :premises (@p89 @p10) :args (@t71 @t48 @t72)) % 5.77/6.09 (step @p91 :rule eq-symm :args (@t75 @t76)) % 5.77/6.09 (step @p92 :rule cong :premises (@p82 @p91) :args ((=> @t21 @t77))) % 5.77/6.09 (assume-push @p1694 @t21) % 5.77/6.09 (step @p94 :rule instantiate :premises (@p10) :args (@t78)) % 5.77/6.09 (step-pop @p1695 :rule scope :premises (@p94)) % 5.77/6.09 (step @p95 :rule process_scope :premises (@p1695) :args (@t77)) % 5.77/6.09 (step @p97 :rule eq_resolve :premises (@p95 @p92)) % 5.77/6.09 (step @p98 :rule implies_elim :premises (@p97)) % 5.77/6.09 (step @p99 :rule chain_m_resolution :premises (@p98 @p10) :args (@t79 @t48 @t72)) % 5.77/6.09 (step @p100 :rule eq-symm :args (@t82 @t83)) % 5.77/6.09 (step @p101 :rule cong :premises (@p82 @p100) :args ((=> @t21 @t84))) % 5.77/6.09 (assume-push @p1696 @t21) % 5.77/6.09 (step @p103 :rule instantiate :premises (@p10) :args (@t85)) % 5.77/6.09 (step-pop @p1697 :rule scope :premises (@p103)) % 5.77/6.09 (step @p104 :rule process_scope :premises (@p1697) :args (@t84)) % 5.77/6.09 (step @p106 :rule eq_resolve :premises (@p104 @p101)) % 5.77/6.09 (step @p107 :rule implies_elim :premises (@p106)) % 5.77/6.09 (step @p108 :rule chain_m_resolution :premises (@p107 @p10) :args (@t86 @t48 @t72)) % 5.77/6.09 (step @p109 :rule instantiate :premises (@p10) :args ((@list @t57 @t38 @t25))) % 5.77/6.09 (step @p110 :rule instantiate :premises (@p11) :args ((@list @t87 tptp.truth))) % 5.77/6.09 (step @p111 :rule instantiate :premises (@p11) :args ((@list @t88 @t39))) % 5.77/6.09 (step @p112 :rule instantiate :premises (@p11) :args ((@list @t90 @t38))) % 5.77/6.09 (step @p113 :rule instantiate :premises (@p11) :args ((@list @t32 tptp.b))) % 5.77/6.09 (step @p114 :rule instantiate :premises (@p11) :args ((@list @t35 tptp.a))) % 5.77/6.09 (step @p115 :rule instantiate :premises (@p11) :args ((@list @t38 @t24))) % 5.77/6.09 (step @p116 :rule instantiate :premises (@p11) :args ((@list @t57 @t33))) % 5.77/6.09 (step @p117 :rule instantiate :premises (@p11) :args ((@list @t80 @t33))) % 5.77/6.09 (step @p118 :rule instantiate :premises (@p11) :args ((@list @t60 @t39))) % 5.77/6.09 (step @p119 :rule eq-symm :args (@t91 @t92)) % 5.77/6.09 (step @p120 :rule cong :premises (@p46 @p119) :args ((=> @t4 @t93))) % 5.77/6.09 (assume-push @p1698 @t4) % 5.77/6.09 (step @p122 :rule instantiate :premises (@p1) :args (@t63)) % 5.77/6.09 (step-pop @p1699 :rule scope :premises (@p122)) % 5.77/6.09 (step @p123 :rule process_scope :premises (@p1699) :args (@t93)) % 5.77/6.09 (step @p125 :rule eq_resolve :premises (@p123 @p120)) % 5.77/6.09 (step @p126 :rule implies_elim :premises (@p125)) % 5.77/6.09 (step @p127 :rule chain_m_resolution :premises (@p126 @p1) :args (@t94 @t48 @t49)) % 5.77/6.09 (step @p128 :rule eq-symm :args (@t97 @t98)) % 5.77/6.09 (step @p129 :rule cong :premises (@p46 @p128) :args ((=> @t4 @t99))) % 5.77/6.09 (assume-push @p1700 @t4) % 5.77/6.09 (step @p131 :rule instantiate :premises (@p1) :args (@t100)) % 5.77/6.09 (step-pop @p1701 :rule scope :premises (@p131)) % 5.77/6.09 (step @p132 :rule process_scope :premises (@p1701) :args (@t99)) % 5.77/6.09 (step @p134 :rule eq_resolve :premises (@p132 @p129)) % 5.77/6.09 (step @p135 :rule implies_elim :premises (@p134)) % 5.77/6.09 (step @p136 :rule chain_m_resolution :premises (@p135 @p1) :args (@t101 @t48 @t49)) % 5.77/6.09 (step @p137 :rule eq-symm :args (@t5 @t1)) % 5.77/6.09 (step @p138 :rule cong :premises (@p137) :args (@t6)) % 5.77/6.09 (step @p139 :rule eq_resolve :premises (@p2 @p138)) % 5.77/6.09 (step @p140 :rule instantiate :premises (@p139) :args (@t28)) % 5.77/6.09 (step @p141 :rule instantiate :premises (@p139) :args (@t37)) % 5.77/6.09 (step @p142 :rule eq-symm :args (@t7 @t1)) % 5.77/6.09 (step @p143 :rule cong :premises (@p142) :args (@t8)) % 5.77/6.09 (step @p144 :rule eq_resolve :premises (@p4 @p143)) % 5.77/6.09 (step @p145 :rule instantiate :premises (@p144) :args (@t41)) % 5.77/6.09 (step @p146 :rule instantiate :premises (@p24) :args (@t102)) % 5.77/6.09 (step @p147 :rule instantiate :premises (@p24) :args (@t103)) % 5.77/6.09 (step @p148 :rule eq-symm :args (@t104 @t105)) % 5.77/6.09 (step @p149 :rule refl :args (@t17)) % 5.77/6.09 (step @p150 :rule cong :premises (@p149 @p148) :args ((=> @t17 @t106))) % 5.77/6.09 (assume-push @p1702 @t17) % 5.77/6.09 (step @p152 :rule instantiate :premises (@p7) :args ((@list tptp.truth tptp.truth))) % 5.77/6.09 (step-pop @p1703 :rule scope :premises (@p152)) % 5.77/6.09 (step @p153 :rule process_scope :premises (@p1703) :args (@t106)) % 5.77/6.09 (step @p155 :rule eq_resolve :premises (@p153 @p150)) % 5.77/6.09 (step @p156 :rule implies_elim :premises (@p155)) % 5.77/6.09 (step @p157 :rule chain_m_resolution :premises (@p156 @p7) :args (@t107 @t48 @t108)) % 5.77/6.09 (step @p158 :rule instantiate :premises (@p7) :args (@t43)) % 5.77/6.09 (step @p159 :rule instantiate :premises (@p7) :args (@t65)) % 5.77/6.09 (step @p160 :rule instantiate :premises (@p7) :args ((@list @t58 tptp.a))) % 5.77/6.09 (step @p161 :rule instantiate :premises (@p8) :args ((@list @t33 tptp.a))) % 5.77/6.09 (step @p162 :rule instantiate :premises (@p8) :args (@t109)) % 5.77/6.09 (step @p163 :rule instantiate :premises (@p8) :args ((@list @t24 @t90))) % 5.77/6.09 (step @p164 :rule instantiate :premises (@p8) :args (@t43)) % 5.77/6.09 (step @p165 :rule instantiate :premises (@p8) :args (@t110)) % 5.77/6.09 (step @p166 :rule instantiate :premises (@p9) :args (@t109)) % 5.77/6.09 (step @p167 :rule instantiate :premises (@p9) :args ((@list tptp.truth @t26))) % 5.77/6.09 (step @p168 :rule instantiate :premises (@p9) :args ((@list tptp.truth @t111))) % 5.77/6.09 (step @p169 :rule instantiate :premises (@p9) :args ((@list @t112 tptp.truth))) % 5.77/6.09 (step @p170 :rule instantiate :premises (@p9) :args ((@list @t114 tptp.truth))) % 5.77/6.09 (step @p171 :rule instantiate :premises (@p10) :args ((@list @t116 tptp.b @t32))) % 5.77/6.09 (step @p172 :rule instantiate :premises (@p10) :args ((@list @t118 tptp.a @t35))) % 5.77/6.09 (step @p173 :rule instantiate :premises (@p10) :args ((@list @t38 @t25 @t88))) % 5.77/6.09 (step @p174 :rule instantiate :premises (@p10) :args ((@list @t38 @t25 @t60))) % 5.77/6.09 (step @p175 :rule instantiate :premises (@p10) :args ((@list @t57 @t33 @t80))) % 5.77/6.09 (step @p176 :rule instantiate :premises (@p10) :args ((@list tptp.truth @t24 @t38))) % 5.77/6.09 (step @p177 :rule instantiate :premises (@p11) :args ((@list @t119 @t25))) % 5.77/6.09 (step @p178 :rule instantiate :premises (@p11) :args ((@list @t121 @t25))) % 5.77/6.09 (step @p179 :rule instantiate :premises (@p11) :args ((@list @t123 @t26))) % 5.77/6.09 (step @p180 :rule instantiate :premises (@p11) :args ((@list @t57 @t40))) % 5.77/6.09 (step @p181 :rule instantiate :premises (@p11) :args ((@list @t80 tptp.a))) % 5.77/6.09 (step @p182 :rule instantiate :premises (@p11) :args ((@list @t60 @t38))) % 5.77/6.09 (step @p183 :rule instantiate :premises (@p11) :args ((@list @t124 @t24))) % 5.77/6.09 (step @p184 :rule instantiate :premises (@p11) :args ((@list @t125 @t24))) % 5.77/6.09 (step @p185 :rule instantiate :premises (@p13) :args ((@list @t113 @t36))) % 5.77/6.09 (step @p186 :rule instantiate :premises (@p13) :args (@t42)) % 5.77/6.09 (step @p187 :rule eq-symm :args (@t128 @t129)) % 5.77/6.09 (step @p188 :rule cong :premises (@p46 @p187) :args ((=> @t4 @t130))) % 5.77/6.09 (assume-push @p1704 @t4) % 5.77/6.09 (step @p190 :rule instantiate :premises (@p1) :args (@t131)) % 5.77/6.09 (step-pop @p1705 :rule scope :premises (@p190)) % 5.77/6.09 (step @p191 :rule process_scope :premises (@p1705) :args (@t130)) % 5.77/6.09 (step @p193 :rule eq_resolve :premises (@p191 @p188)) % 5.77/6.09 (step @p194 :rule implies_elim :premises (@p193)) % 5.77/6.09 (step @p195 :rule chain_m_resolution :premises (@p194 @p1) :args (@t132 @t48 @t49)) % 5.77/6.09 (step @p196 :rule eq-symm :args (@t135 @t136)) % 5.77/6.09 (step @p197 :rule cong :premises (@p46 @p196) :args ((=> @t4 @t137))) % 5.77/6.09 (assume-push @p1706 @t4) % 5.77/6.09 (step @p199 :rule instantiate :premises (@p1) :args (@t138)) % 5.77/6.09 (step-pop @p1707 :rule scope :premises (@p199)) % 5.77/6.09 (step @p200 :rule process_scope :premises (@p1707) :args (@t137)) % 5.77/6.09 (step @p202 :rule eq_resolve :premises (@p200 @p197)) % 5.77/6.09 (step @p203 :rule implies_elim :premises (@p202)) % 5.77/6.09 (step @p204 :rule chain_m_resolution :premises (@p203 @p1) :args (@t139 @t48 @t49)) % 5.77/6.09 (step @p205 :rule instantiate :premises (@p139) :args (@t103)) % 5.77/6.09 (step @p206 :rule instantiate :premises (@p144) :args (@t102)) % 5.77/6.09 (step @p207 :rule instantiate :premises (@p144) :args ((@list @t32))) % 5.77/6.09 (step @p208 :rule instantiate :premises (@p144) :args (@t63)) % 5.77/6.09 (step @p209 :rule instantiate :premises (@p144) :args ((@list @t80))) % 5.77/6.09 (step @p210 :rule instantiate :premises (@p144) :args ((@list @t113))) % 5.77/6.09 (step @p211 :rule instantiate :premises (@p144) :args ((@list @t141))) % 5.77/6.09 (step @p212 :rule instantiate :premises (@p144) :args ((@list @t143))) % 5.77/6.09 (step @p213 :rule instantiate :premises (@p7) :args ((@list tptp.truth @t35))) % 5.77/6.09 (step @p214 :rule eq-symm :args (@t144 @t146)) % 5.77/6.09 (step @p215 :rule cong :premises (@p149 @p214) :args ((=> @t17 @t147))) % 5.77/6.09 (assume-push @p1708 @t17) % 5.77/6.09 (step @p217 :rule instantiate :premises (@p7) :args (@t148)) % 5.77/6.09 (step-pop @p1709 :rule scope :premises (@p217)) % 5.77/6.09 (step @p218 :rule process_scope :premises (@p1709) :args (@t147)) % 5.77/6.09 (step @p220 :rule eq_resolve :premises (@p218 @p215)) % 5.77/6.09 (step @p221 :rule implies_elim :premises (@p220)) % 5.77/6.09 (step @p222 :rule chain_m_resolution :premises (@p221 @p7) :args (@t149 @t48 @t108)) % 5.77/6.09 (step @p223 :rule instantiate :premises (@p7) :args ((@list @t51 tptp.truth))) % 5.77/6.09 (step @p224 :rule instantiate :premises (@p7) :args ((@list tptp.truth tptp.a))) % 5.77/6.09 (step @p225 :rule eq-symm :args (@t150 @t151)) % 5.77/6.09 (step @p226 :rule cong :premises (@p149 @p225) :args ((=> @t17 @t152))) % 5.77/6.09 (assume-push @p1710 @t17) % 5.77/6.09 (step @p228 :rule instantiate :premises (@p7) :args ((@list @t89 tptp.truth))) % 5.77/6.09 (step-pop @p1711 :rule scope :premises (@p228)) % 5.77/6.09 (step @p229 :rule process_scope :premises (@p1711) :args (@t152)) % 5.77/6.09 (step @p231 :rule eq_resolve :premises (@p229 @p226)) % 5.77/6.09 (step @p232 :rule implies_elim :premises (@p231)) % 5.77/6.09 (step @p233 :rule chain_m_resolution :premises (@p232 @p7) :args (@t153 @t48 @t108)) % 5.77/6.09 (step @p234 :rule instantiate :premises (@p8) :args ((@list tptp.b @t50))) % 5.77/6.09 (step @p235 :rule instantiate :premises (@p9) :args (@t154)) % 5.77/6.09 (step @p236 :rule instantiate :premises (@p9) :args (@t155)) % 5.77/6.09 (step @p237 :rule instantiate :premises (@p9) :args ((@list @t156 tptp.truth))) % 5.77/6.09 (step @p238 :rule instantiate :premises (@p9) :args ((@list @t74 tptp.truth))) % 5.77/6.09 (step @p239 :rule instantiate :premises (@p9) :args ((@list tptp.truth @t90))) % 5.77/6.09 (step @p240 :rule instantiate :premises (@p9) :args ((@list tptp.truth @t32))) % 5.77/6.09 (step @p241 :rule instantiate :premises (@p9) :args ((@list @t157 tptp.truth))) % 5.77/6.09 (step @p242 :rule instantiate :premises (@p9) :args ((@list @t158 tptp.truth))) % 5.77/6.09 (step @p243 :rule instantiate :premises (@p9) :args (@t159)) % 5.77/6.09 (step @p244 :rule instantiate :premises (@p9) :args ((@list @t160 tptp.truth))) % 5.77/6.09 (step @p245 :rule instantiate :premises (@p9) :args ((@list @t140 tptp.truth))) % 5.77/6.09 (step @p246 :rule instantiate :premises (@p9) :args ((@list @t162 tptp.truth))) % 5.77/6.09 (step @p247 :rule instantiate :premises (@p9) :args ((@list @t163 tptp.truth))) % 5.77/6.09 (step @p248 :rule instantiate :premises (@p9) :args ((@list @t164 tptp.truth))) % 5.77/6.09 (step @p249 :rule instantiate :premises (@p10) :args ((@list @t35 tptp.b @t26))) % 5.77/6.09 (step @p250 :rule instantiate :premises (@p10) :args ((@list @t35 tptp.b tptp.a))) % 5.77/6.09 (step @p251 :rule instantiate :premises (@p10) :args ((@list @t60 @t35 tptp.b))) % 5.77/6.09 (step @p252 :rule eq-symm :args (@t166 @t157)) % 5.77/6.09 (step @p253 :rule cong :premises (@p82 @p252) :args ((=> @t21 @t167))) % 5.77/6.09 (assume-push @p1712 @t21) % 5.77/6.09 (step @p255 :rule instantiate :premises (@p10) :args ((@list @t50 @t57 @t33))) % 5.77/6.09 (step-pop @p1713 :rule scope :premises (@p255)) % 5.77/6.09 (step @p256 :rule process_scope :premises (@p1713) :args (@t167)) % 5.77/6.09 (step @p258 :rule eq_resolve :premises (@p256 @p253)) % 5.77/6.09 (step @p259 :rule implies_elim :premises (@p258)) % 5.77/6.09 (step @p260 :rule chain_m_resolution :premises (@p259 @p10) :args (@t168 @t48 @t72)) % 5.77/6.09 (step @p261 :rule eq-symm :args (@t170 @t158)) % 5.77/6.09 (step @p262 :rule cong :premises (@p82 @p261) :args ((=> @t21 @t171))) % 5.77/6.09 (assume-push @p1714 @t21) % 5.77/6.09 (step @p264 :rule instantiate :premises (@p10) :args (@t172)) % 5.77/6.09 (step-pop @p1715 :rule scope :premises (@p264)) % 5.77/6.09 (step @p265 :rule process_scope :premises (@p1715) :args (@t171)) % 5.77/6.09 (step @p267 :rule eq_resolve :premises (@p265 @p262)) % 5.77/6.09 (step @p268 :rule implies_elim :premises (@p267)) % 5.77/6.09 (step @p269 :rule chain_m_resolution :premises (@p268 @p10) :args (@t173 @t48 @t72)) % 5.77/6.09 (step @p270 :rule eq-symm :args (@t175 @t160)) % 5.77/6.09 (step @p271 :rule cong :premises (@p82 @p270) :args ((=> @t21 @t176))) % 5.77/6.09 (assume-push @p1716 @t21) % 5.77/6.09 (step @p273 :rule instantiate :premises (@p10) :args ((@list @t35 @t57 @t33))) % 5.77/6.09 (step-pop @p1717 :rule scope :premises (@p273)) % 5.77/6.09 (step @p274 :rule process_scope :premises (@p1717) :args (@t176)) % 5.77/6.09 (step @p276 :rule eq_resolve :premises (@p274 @p271)) % 5.77/6.09 (step @p277 :rule implies_elim :premises (@p276)) % 5.77/6.09 (step @p278 :rule chain_m_resolution :premises (@p277 @p10) :args (@t177 @t48 @t72)) % 5.77/6.09 (step @p279 :rule instantiate :premises (@p10) :args ((@list @t38 @t24 @t124))) % 5.77/6.09 (step @p280 :rule instantiate :premises (@p11) :args (@t154)) % 5.77/6.09 (step @p281 :rule eq-symm :args (@t178 @t179)) % 5.77/6.09 (step @p282 :rule refl :args (@t22)) % 5.77/6.09 (step @p283 :rule cong :premises (@p282 @p281) :args ((=> @t22 @t180))) % 5.77/6.09 (assume-push @p1718 @t22) % 5.77/6.09 (step @p285 :rule instantiate :premises (@p11) :args (@t181)) % 5.77/6.09 (step-pop @p1719 :rule scope :premises (@p285)) % 5.77/6.09 (step @p286 :rule process_scope :premises (@p1719) :args (@t180)) % 5.77/6.09 (step @p288 :rule eq_resolve :premises (@p286 @p283)) % 5.77/6.09 (step @p289 :rule implies_elim :premises (@p288)) % 5.77/6.09 (step @p290 :rule chain_m_resolution :premises (@p289 @p11) :args (@t182 @t48 @t183)) % 5.77/6.09 (step @p291 :rule eq-symm :args (@t184 @t185)) % 5.77/6.09 (step @p292 :rule cong :premises (@p282 @p291) :args ((=> @t22 @t186))) % 5.77/6.09 (assume-push @p1720 @t22) % 5.77/6.09 (step @p294 :rule instantiate :premises (@p11) :args (@t187)) % 5.77/6.09 (step-pop @p1721 :rule scope :premises (@p294)) % 5.77/6.09 (step @p295 :rule process_scope :premises (@p1721) :args (@t186)) % 5.77/6.09 (step @p297 :rule eq_resolve :premises (@p295 @p292)) % 5.77/6.09 (step @p298 :rule implies_elim :premises (@p297)) % 5.77/6.09 (step @p299 :rule chain_m_resolution :premises (@p298 @p11) :args (@t188 @t48 @t183)) % 5.77/6.09 (step @p300 :rule instantiate :premises (@p11) :args ((@list @t50 @t64))) % 5.77/6.09 (step @p301 :rule instantiate :premises (@p11) :args ((@list @t25 @t60))) % 5.77/6.09 (step @p302 :rule instantiate :premises (@p11) :args (@t189)) % 5.77/6.09 (step @p303 :rule instantiate :premises (@p11) :args ((@list @t35 @t33))) % 5.77/6.09 (step @p304 :rule instantiate :premises (@p11) :args ((@list @t35 @t24))) % 5.77/6.09 (step @p305 :rule instantiate :premises (@p11) :args ((@list @t35 @t64))) % 5.77/6.09 (step @p306 :rule instantiate :premises (@p11) :args ((@list @t38 tptp.a))) % 5.77/6.09 (step @p307 :rule instantiate :premises (@p11) :args ((@list @t64 @t80))) % 5.77/6.09 (step @p308 :rule instantiate :premises (@p11) :args ((@list @t126 @t26))) % 5.77/6.09 (step @p309 :rule instantiate :premises (@p11) :args (@t155)) % 5.77/6.09 (step @p310 :rule instantiate :premises (@p11) :args ((@list @t113 @t25))) % 5.77/6.09 (step @p311 :rule instantiate :premises (@p11) :args ((@list @t113 @t38))) % 5.77/6.09 (step @p312 :rule instantiate :premises (@p11) :args ((@list @t113 tptp.truth))) % 5.77/6.09 (step @p313 :rule instantiate :premises (@p11) :args ((@list @t190 @t33))) % 5.77/6.09 (step @p314 :rule instantiate :premises (@p11) :args ((@list @t191 @t24))) % 5.77/6.09 (step @p315 :rule instantiate :premises (@p11) :args ((@list @t193 tptp.b))) % 5.77/6.09 (step @p316 :rule instantiate :premises (@p11) :args ((@list @t143 tptp.truth))) % 5.77/6.09 (step @p317 :rule instantiate :premises (@p11) :args ((@list @t194 tptp.a))) % 5.77/6.09 (step @p318 :rule instantiate :premises (@p11) :args ((@list @t195 @t38))) % 5.77/6.09 (step @p319 :rule instantiate :premises (@p13) :args ((@list @t161 @t36))) % 5.77/6.09 (step @p320 :rule instantiate :premises (@p13) :args ((@list @t40 @t36))) % 5.77/6.09 (step @p321 :rule instantiate :premises (@p139) :args (@t31)) % 5.77/6.09 (step @p322 :rule instantiate :premises (@p139) :args (@t34)) % 5.77/6.09 (step @p323 :rule instantiate :premises (@p139) :args ((@list @t89))) % 5.77/6.09 (step @p324 :rule instantiate :premises (@p139) :args (@t55)) % 5.77/6.09 (step @p325 :rule instantiate :premises (@p144) :args ((@list @t197))) % 5.77/6.09 (step @p326 :rule eq-symm :args (@t9 tptp.falsehood)) % 5.77/6.09 (step @p327 :rule cong :premises (@p326) :args (@t10)) % 5.77/6.09 (step @p328 :rule eq_resolve :premises (@p5 @p327)) % 5.77/6.09 (step @p329 :rule instantiate :premises (@p328) :args (@t198)) % 5.77/6.09 (step @p330 :rule instantiate :premises (@p328) :args (@t63)) % 5.77/6.09 (step @p331 :rule instantiate :premises (@p328) :args (@t31)) % 5.77/6.09 (step @p332 :rule instantiate :premises (@p24) :args (@t200)) % 5.77/6.09 (step @p333 :rule instantiate :premises (@p8) :args ((@list @t158 @t33))) % 5.77/6.09 (step @p334 :rule instantiate :premises (@p8) :args (@t189)) % 5.77/6.09 (step @p335 :rule instantiate :premises (@p8) :args ((@list @t26 @t32))) % 5.77/6.09 (step @p336 :rule instantiate :premises (@p8) :args ((@list @t80 @t50))) % 5.77/6.09 (step @p337 :rule instantiate :premises (@p8) :args ((@list @t80 @t35))) % 5.77/6.09 (step @p338 :rule instantiate :premises (@p9) :args ((@list @t87 tptp.a))) % 5.77/6.09 (step @p339 :rule eq-symm :args (@t201 @t202)) % 5.77/6.09 (step @p340 :rule refl :args (@t18)) % 5.77/6.09 (step @p341 :rule cong :premises (@p340 @p339) :args ((=> @t18 @t203))) % 5.77/6.09 (assume-push @p1722 @t18) % 5.77/6.09 (step @p343 :rule instantiate :premises (@p9) :args (@t204)) % 5.77/6.09 (step-pop @p1723 :rule scope :premises (@p343)) % 5.77/6.09 (step @p344 :rule process_scope :premises (@p1723) :args (@t203)) % 5.77/6.09 (step @p346 :rule eq_resolve :premises (@p344 @p341)) % 5.77/6.09 (step @p347 :rule implies_elim :premises (@p346)) % 5.77/6.09 (step @p348 :rule chain_m_resolution :premises (@p347 @p9) :args (@t205 @t48 @t206)) % 5.77/6.09 (step @p349 :rule instantiate :premises (@p9) :args ((@list @t208 tptp.truth))) % 5.77/6.09 (step @p350 :rule instantiate :premises (@p9) :args ((@list @t210 tptp.truth))) % 5.77/6.09 (step @p351 :rule instantiate :premises (@p10) :args ((@list tptp.truth @t113 @t38))) % 5.77/6.09 (step @p352 :rule instantiate :premises (@p10) :args ((@list @t212 tptp.b @t211))) % 5.77/6.09 (step @p353 :rule instantiate :premises (@p10) :args ((@list @t57 @t25 @t33))) % 5.77/6.09 (step @p354 :rule instantiate :premises (@p10) :args ((@list @t38 @t113 @t25))) % 5.77/6.09 (step @p355 :rule instantiate :premises (@p10) :args ((@list @t73 @t35 @t33))) % 5.77/6.09 (step @p356 :rule instantiate :premises (@p10) :args ((@list @t212 tptp.b @t32))) % 5.77/6.09 (step @p357 :rule instantiate :premises (@p10) :args ((@list @t190 @t32 tptp.a))) % 5.77/6.09 (step @p358 :rule instantiate :premises (@p10) :args ((@list tptp.a tptp.truth @t80))) % 5.77/6.09 (step @p359 :rule eq-symm :args (@t215 @t216)) % 5.77/6.09 (step @p360 :rule cong :premises (@p82 @p359) :args ((=> @t21 @t217))) % 5.77/6.09 (assume-push @p1724 @t21) % 5.77/6.09 (step @p362 :rule instantiate :premises (@p10) :args (@t218)) % 5.77/6.09 (step-pop @p1725 :rule scope :premises (@p362)) % 5.77/6.09 (step @p363 :rule process_scope :premises (@p1725) :args (@t217)) % 5.77/6.09 (step @p365 :rule eq_resolve :premises (@p363 @p360)) % 5.77/6.09 (step @p366 :rule implies_elim :premises (@p365)) % 5.77/6.09 (step @p367 :rule chain_m_resolution :premises (@p366 @p10) :args (@t219 @t48 @t72)) % 5.77/6.09 (step @p368 :rule eq-symm :args (@t222 @t223)) % 5.77/6.09 (step @p369 :rule cong :premises (@p82 @p368) :args ((=> @t21 @t224))) % 5.77/6.09 (assume-push @p1726 @t21) % 5.77/6.09 (step @p371 :rule instantiate :premises (@p10) :args ((@list @t220 tptp.a @t32))) % 5.77/6.09 (step-pop @p1727 :rule scope :premises (@p371)) % 5.77/6.09 (step @p372 :rule process_scope :premises (@p1727) :args (@t224)) % 5.77/6.09 (step @p374 :rule eq_resolve :premises (@p372 @p369)) % 5.77/6.09 (step @p375 :rule implies_elim :premises (@p374)) % 5.77/6.09 (step @p376 :rule chain_m_resolution :premises (@p375 @p10) :args (@t225 @t48 @t72)) % 5.77/6.09 (step @p377 :rule instantiate :premises (@p10) :args ((@list @t199 @t212 tptp.b))) % 5.77/6.09 (step @p378 :rule instantiate :premises (@p10) :args ((@list @t32 @t95 @t80))) % 5.77/6.09 (step @p379 :rule instantiate :premises (@p10) :args ((@list @t226 @t226 @t32))) % 5.77/6.09 (step @p380 :rule instantiate :premises (@p10) :args ((@list @t95 tptp.truth @t80))) % 5.77/6.09 (step @p381 :rule instantiate :premises (@p10) :args ((@list tptp.truth tptp.truth @t143))) % 5.77/6.09 (step @p382 :rule instantiate :premises (@p11) :args (@t29)) % 5.77/6.09 (step @p383 :rule instantiate :premises (@p11) :args ((@list @t35 @t227))) % 5.77/6.09 (step @p384 :rule instantiate :premises (@p11) :args ((@list @t226 tptp.a))) % 5.77/6.09 (step @p385 :rule instantiate :premises (@p11) :args ((@list @t60 @t35))) % 5.77/6.09 (step @p386 :rule instantiate :premises (@p11) :args ((@list @t209 tptp.b))) % 5.77/6.09 (step @p387 :rule instantiate :premises (@p11) :args ((@list @t125 @t32))) % 5.77/6.09 (step @p388 :rule instantiate :premises (@p11) :args ((@list @t199 @t36))) % 5.77/6.09 (step @p389 :rule instantiate :premises (@p11) :args ((@list @t228 tptp.b))) % 5.77/6.09 (step @p390 :rule instantiate :premises (@p11) :args ((@list @t212 tptp.b))) % 5.77/6.09 (step @p391 :rule instantiate :premises (@p11) :args ((@list @t229 @t25))) % 5.77/6.09 (step @p392 :rule instantiate :premises (@p13) :args ((@list @t199 @t24))) % 5.77/6.09 (step @p393 :rule instantiate :premises (@p13) :args (@t110)) % 5.77/6.09 (step @p394 :rule eq-symm :args (@t231 @t232)) % 5.77/6.09 (step @p395 :rule cong :premises (@p46 @p394) :args ((=> @t4 @t233))) % 5.77/6.09 (assume-push @p1728 @t4) % 5.77/6.09 (step @p397 :rule instantiate :premises (@p1) :args (@t234)) % 5.77/6.09 (step-pop @p1729 :rule scope :premises (@p397)) % 5.77/6.09 (step @p398 :rule process_scope :premises (@p1729) :args (@t233)) % 5.77/6.09 (step @p400 :rule eq_resolve :premises (@p398 @p395)) % 5.77/6.09 (step @p401 :rule implies_elim :premises (@p400)) % 5.77/6.09 (step @p402 :rule chain_m_resolution :premises (@p401 @p1) :args (@t235 @t48 @t49)) % 5.77/6.09 (step @p403 :rule eq-symm :args (@t237 @t238)) % 5.77/6.09 (step @p404 :rule cong :premises (@p46 @p403) :args ((=> @t4 @t239))) % 5.77/6.09 (assume-push @p1730 @t4) % 5.77/6.09 (step @p406 :rule instantiate :premises (@p1) :args ((@list @t236))) % 5.77/6.09 (step-pop @p1731 :rule scope :premises (@p406)) % 5.77/6.09 (step @p407 :rule process_scope :premises (@p1731) :args (@t239)) % 5.77/6.09 (step @p409 :rule eq_resolve :premises (@p407 @p404)) % 5.77/6.09 (step @p410 :rule implies_elim :premises (@p409)) % 5.77/6.09 (step @p411 :rule chain_m_resolution :premises (@p410 @p1) :args (@t240 @t48 @t49)) % 5.77/6.09 (step @p412 :rule instantiate :premises (@p139) :args (@t30)) % 5.77/6.09 (step @p413 :rule instantiate :premises (@p144) :args (@t30)) % 5.77/6.09 (step @p414 :rule instantiate :premises (@p144) :args (@t198)) % 5.77/6.09 (step @p415 :rule instantiate :premises (@p144) :args ((@list @t35))) % 5.77/6.09 (step @p416 :rule instantiate :premises (@p328) :args (@t200)) % 5.77/6.09 (step @p417 :rule eq-symm :args (@t241 @t242)) % 5.77/6.09 (step @p418 :rule cong :premises (@p149 @p417) :args ((=> @t17 @t243))) % 5.77/6.09 (assume-push @p1732 @t17) % 5.77/6.09 (step @p420 :rule instantiate :premises (@p7) :args (@t159)) % 5.77/6.09 (step-pop @p1733 :rule scope :premises (@p420)) % 5.77/6.09 (step @p421 :rule process_scope :premises (@p1733) :args (@t243)) % 5.77/6.09 (step @p423 :rule eq_resolve :premises (@p421 @p418)) % 5.77/6.09 (step @p424 :rule implies_elim :premises (@p423)) % 5.77/6.09 (step @p425 :rule chain_m_resolution :premises (@p424 @p7) :args (@t244 @t48 @t108)) % 5.77/6.09 (step @p426 :rule instantiate :premises (@p8) :args ((@list @t32 @t35))) % 5.77/6.09 (step @p427 :rule eq-symm :args (@t246 @t247)) % 5.77/6.09 (step @p428 :rule cong :premises (@p340 @p427) :args ((=> @t18 @t248))) % 5.77/6.09 (assume-push @p1734 @t18) % 5.77/6.09 (step @p430 :rule instantiate :premises (@p9) :args ((@list tptp.truth @t245))) % 5.77/6.09 (step-pop @p1735 :rule scope :premises (@p430)) % 5.77/6.09 (step @p431 :rule process_scope :premises (@p1735) :args (@t248)) % 5.77/6.09 (step @p433 :rule eq_resolve :premises (@p431 @p428)) % 5.77/6.09 (step @p434 :rule implies_elim :premises (@p433)) % 5.77/6.09 (step @p435 :rule chain_m_resolution :premises (@p434 @p9) :args (@t249 @t48 @t206)) % 5.77/6.09 (step @p436 :rule instantiate :premises (@p9) :args ((@list @t129 tptp.truth))) % 5.77/6.09 (step @p437 :rule instantiate :premises (@p10) :args ((@list @t90 @t38 @t32))) % 5.77/6.09 (step @p438 :rule instantiate :premises (@p10) :args ((@list tptp.a tptp.b @t32))) % 5.77/6.09 (step @p439 :rule instantiate :premises (@p10) :args ((@list @t250 @t123 @t26))) % 5.77/6.09 (step @p440 :rule instantiate :premises (@p10) :args ((@list @t202 @t251 @t80))) % 5.77/6.09 (step @p441 :rule instantiate :premises (@p10) :args ((@list @t35 @t252 @t80))) % 5.77/6.09 (step @p442 :rule instantiate :premises (@p11) :args ((@list @t253 @t26))) % 5.77/6.09 (step @p443 :rule instantiate :premises (@p11) :args ((@list @t238 @t80))) % 5.77/6.09 (step @p444 :rule instantiate :premises (@p139) :args (@t131)) % 5.77/6.09 (step @p445 :rule instantiate :premises (@p10) :args ((@list @t254 @t26 @t80))) % 5.77/6.09 (step @p446 :rule instantiate :premises (@p10) :args ((@list @t255 @t80 @t26))) % 5.77/6.09 (assume-push @p1736 @t256) % 5.77/6.09 (assume-push @p1737 @t257) % 5.77/6.09 (assume-push @p1738 @t258) % 5.77/6.09 (assume-push @p1739 @t259) % 5.77/6.09 (assume-push @p1740 @t260) % 5.77/6.09 (assume-push @p1741 @t261) % 5.77/6.09 (assume-push @p1742 @t263) % 5.77/6.09 (assume-push @p1743 @t264) % 5.77/6.09 (assume-push @p1744 @t266) % 5.77/6.09 (assume-push @p1745 @t268) % 5.77/6.09 (assume-push @p1746 @t269) % 5.77/6.09 (assume-push @p1747 @t270) % 5.77/6.09 (assume-push @p1748 @t272) % 5.77/6.09 (assume-push @p1749 @t273) % 5.77/6.09 (assume-push @p1750 @t275) % 5.77/6.09 (assume-push @p1751 @t277) % 5.77/6.09 (assume-push @p1752 @t279) % 5.77/6.09 (assume-push @p1753 @t280) % 5.77/6.09 (assume-push @p1754 @t281) % 5.77/6.09 (assume-push @p1755 @t282) % 5.77/6.09 (assume-push @p1756 @t284) % 5.77/6.09 (assume-push @p1757 @t286) % 5.77/6.09 (assume-push @p1758 @t287) % 5.77/6.09 (assume-push @p1759 @t288) % 5.77/6.09 (assume-push @p1760 @t289) % 5.77/6.09 (assume-push @p1761 @t290) % 5.77/6.09 (assume-push @p1762 @t47) % 5.77/6.09 (assume-push @p1763 @t56) % 5.77/6.09 (assume-push @p1764 @t62) % 5.77/6.09 (assume-push @p1765 @t291) % 5.77/6.09 (assume-push @p1766 @t293) % 5.77/6.09 (assume-push @p1767 @t296) % 5.77/6.09 (assume-push @p1768 @t299) % 5.77/6.09 (assume-push @p1769 @t302) % 5.77/6.09 (assume-push @p1770 @t303) % 5.77/6.09 (assume-push @p1771 @t304) % 5.77/6.09 (assume-push @p1772 @t305) % 5.77/6.09 (assume-push @p1773 @t71) % 5.77/6.09 (assume-push @p1774 @t79) % 5.77/6.09 (assume-push @p1775 @t86) % 5.77/6.09 (assume-push @p1776 @t307) % 5.77/6.09 (assume-push @p1777 @t308) % 5.77/6.09 (assume-push @p1778 @t310) % 5.77/6.09 (assume-push @p1779 @t312) % 5.77/6.09 (assume-push @p1780 @t314) % 5.77/6.09 (assume-push @p1781 @t316) % 5.77/6.09 (assume-push @p1782 @t318) % 5.77/6.09 (assume-push @p1783 @t320) % 5.77/6.09 (assume-push @p1784 @t322) % 5.77/6.09 (assume-push @p1785 @t324) % 5.77/6.09 (assume-push @p1786 @t94) % 5.77/6.09 (assume-push @p1787 @t101) % 5.77/6.09 (assume-push @p1788 @t325) % 5.77/6.09 (assume-push @p1789 @t327) % 5.77/6.09 (assume-push @p1790 @t329) % 5.77/6.09 (assume-push @p1791 @t331) % 5.77/6.09 (assume-push @p1792 @t332) % 5.77/6.09 (assume-push @p1793 @t107) % 5.77/6.09 (assume-push @p1794 @t334) % 5.77/6.09 (assume-push @p1795 @t337) % 5.77/6.09 (assume-push @p1796 @t339) % 5.77/6.09 (assume-push @p1797 @t341) % 5.77/6.09 (assume-push @p1798 @t346) % 5.77/6.09 (assume-push @p1799 @t349) % 5.77/6.09 (assume-push @p1800 @t352) % 5.77/6.09 (assume-push @p1801 @t355) % 5.77/6.09 (assume-push @p1802 @t356) % 5.77/6.09 (assume-push @p1803 @t358) % 5.77/6.09 (assume-push @p1804 @t360) % 5.77/6.09 (assume-push @p1805 @t362) % 5.77/6.09 (assume-push @p1806 @t364) % 5.77/6.09 (assume-push @p1807 @t366) % 5.77/6.09 (assume-push @p1808 @t368) % 5.77/6.09 (assume-push @p1809 @t371) % 5.77/6.09 (assume-push @p1810 @t374) % 5.77/6.09 (assume-push @p1811 @t376) % 5.77/6.09 (assume-push @p1812 @t379) % 5.77/6.09 (assume-push @p1813 @t381) % 5.77/6.09 (assume-push @p1814 @t382) % 5.77/6.09 (assume-push @p1815 @t384) % 5.77/6.09 (assume-push @p1816 @t385) % 5.77/6.09 (assume-push @p1817 @t387) % 5.77/6.09 (assume-push @p1818 @t389) % 5.77/6.09 (assume-push @p1819 @t391) % 5.77/6.09 (assume-push @p1820 @t393) % 5.77/6.09 (assume-push @p1821 @t395) % 5.77/6.09 (assume-push @p1822 @t397) % 5.77/6.09 (assume-push @p1823 @t132) % 5.77/6.09 (assume-push @p1824 @t139) % 5.77/6.09 (assume-push @p1825 @t398) % 5.77/6.09 (assume-push @p1826 @t399) % 5.77/6.09 (assume-push @p1827 @t400) % 5.77/6.09 (assume-push @p1828 @t401) % 5.77/6.09 (assume-push @p1829 @t403) % 5.77/6.09 (assume-push @p1830 @t404) % 5.77/6.09 (assume-push @p1831 @t405) % 5.77/6.09 (assume-push @p1832 @t406) % 5.77/6.09 (assume-push @p1833 @t409) % 5.77/6.09 (assume-push @p1834 @t149) % 5.77/6.09 (assume-push @p1835 @t411) % 5.77/6.09 (assume-push @p1836 @t413) % 5.77/6.09 (assume-push @p1837 @t153) % 5.77/6.09 (assume-push @p1838 @t415) % 5.77/6.09 (assume-push @p1839 @t417) % 5.77/6.09 (assume-push @p1840 @t419) % 5.77/6.09 (assume-push @p1841 @t421) % 5.77/6.09 (assume-push @p1842 @t423) % 5.77/6.09 (assume-push @p1843 @t424) % 5.77/6.09 (assume-push @p1844 @t425) % 5.77/6.09 (assume-push @p1845 @t427) % 5.77/6.09 (assume-push @p1846 @t429) % 5.77/6.09 (assume-push @p1847 @t430) % 5.77/6.09 (assume-push @p1848 @t432) % 5.77/6.09 (assume-push @p1849 @t433) % 5.77/6.09 (assume-push @p1850 @t435) % 5.77/6.09 (assume-push @p1851 @t436) % 5.77/6.09 (assume-push @p1852 @t438) % 5.77/6.09 (assume-push @p1853 @t441) % 5.77/6.09 (assume-push @p1854 @t444) % 5.77/6.09 (assume-push @p1855 @t447) % 5.77/6.09 (assume-push @p1856 @t168) % 5.77/6.09 (assume-push @p1857 @t173) % 5.77/6.09 (assume-push @p1858 @t177) % 5.77/6.09 (assume-push @p1859 @t449) % 5.77/6.09 (assume-push @p1860 @t451) % 5.77/6.09 (assume-push @p1861 @t182) % 5.77/6.09 (assume-push @p1862 @t188) % 5.77/6.09 (assume-push @p1863 @t452) % 5.77/6.09 (assume-push @p1864 @t453) % 5.77/6.09 (assume-push @p1865 @t454) % 5.77/6.09 (assume-push @p1866 @t455) % 5.77/6.09 (assume-push @p1867 @t457) % 5.77/6.09 (assume-push @p1868 @t458) % 5.77/6.09 (assume-push @p1869 @t460) % 5.77/6.09 (assume-push @p1870 @t462) % 5.77/6.09 (assume-push @p1871 @t464) % 5.77/6.09 (assume-push @p1872 @t466) % 5.77/6.09 (assume-push @p1873 @t467) % 5.77/6.09 (assume-push @p1874 @t469) % 5.77/6.09 (assume-push @p1875 @t471) % 5.77/6.09 (assume-push @p1876 @t472) % 5.77/6.09 (assume-push @p1877 @t474) % 5.77/6.09 (assume-push @p1878 @t476) % 5.77/6.09 (assume-push @p1879 @t478) % 5.77/6.09 (assume-push @p1880 @t479) % 5.77/6.09 (assume-push @p1881 @t481) % 5.77/6.09 (assume-push @p1882 @t483) % 5.77/6.09 (assume-push @p1883 @t486) % 5.77/6.09 (assume-push @p1884 @t487) % 5.77/6.09 (assume-push @p1885 @t489) % 5.77/6.09 (assume-push @p1886 @t490) % 5.77/6.09 (assume-push @p1887 @t491) % 5.77/6.09 (assume-push @p1888 @t492) % 5.77/6.09 (assume-push @p1889 @t493) % 5.77/6.09 (assume-push @p1890 @t494) % 5.77/6.09 (assume-push @p1891 @t496) % 5.77/6.09 (assume-push @p1892 @t498) % 5.77/6.09 (assume-push @p1893 @t502) % 5.77/6.09 (assume-push @p1894 @t506) % 5.77/6.09 (assume-push @p1895 @t509) % 5.77/6.09 (assume-push @p1896 @t513) % 5.77/6.09 (assume-push @p1897 @t518) % 5.77/6.09 (assume-push @p1898 @t520) % 5.77/6.09 (assume-push @p1899 @t205) % 5.77/6.09 (assume-push @p1900 @t522) % 5.77/6.09 (assume-push @p1901 @t524) % 5.77/6.09 (assume-push @p1902 @t526) % 5.77/6.09 (assume-push @p1903 @t528) % 5.77/6.09 (assume-push @p1904 @t531) % 5.77/6.09 (assume-push @p1905 @t533) % 5.77/6.09 (assume-push @p1906 @t536) % 5.77/6.09 (assume-push @p1907 @t538) % 5.77/6.09 (assume-push @p1908 @t541) % 5.77/6.09 (assume-push @p1909 @t544) % 5.77/6.09 (assume-push @p1910 @t219) % 5.77/6.09 (assume-push @p1911 @t225) % 5.77/6.09 (assume-push @p1912 @t547) % 5.77/6.09 (assume-push @p1913 @t551) % 5.77/6.09 (assume-push @p1914 @t555) % 5.77/6.09 (assume-push @p1915 @t558) % 5.77/6.09 (assume-push @p1916 @t561) % 5.77/6.09 (assume-push @p1917 @t563) % 5.77/6.09 (assume-push @p1918 @t565) % 5.77/6.09 (assume-push @p1919 @t567) % 5.77/6.09 (assume-push @p1920 @t569) % 5.77/6.09 (assume-push @p1921 @t571) % 5.77/6.09 (assume-push @p1922 @t573) % 5.77/6.09 (assume-push @p1923 @t575) % 5.77/6.09 (assume-push @p1924 @t577) % 5.77/6.09 (assume-push @p1925 @t578) % 5.77/6.09 (assume-push @p1926 @t580) % 5.77/6.09 (assume-push @p1927 @t582) % 5.77/6.09 (assume-push @p1928 @t584) % 5.77/6.09 (assume-push @p1929 @t235) % 5.77/6.09 (assume-push @p1930 @t240) % 5.77/6.09 (assume-push @p1931 @t585) % 5.77/6.09 (assume-push @p1932 @t586) % 5.77/6.09 (assume-push @p1933 @t587) % 5.77/6.09 (assume-push @p1934 @t589) % 5.77/6.09 (assume-push @p1935 @t590) % 5.77/6.09 (assume-push @p1936 @t244) % 5.77/6.09 (assume-push @p1937 @t594) % 5.77/6.09 (assume-push @p1938 @t249) % 5.77/6.09 (assume-push @p1939 @t595) % 5.77/6.09 (assume-push @p1940 @t598) % 5.77/6.09 (assume-push @p1941 @t600) % 5.77/6.09 (assume-push @p1942 @t602) % 5.77/6.09 (assume-push @p1943 @t605) % 5.77/6.09 (assume-push @p1944 @t607) % 5.77/6.09 (assume-push @p1945 @t609) % 5.77/6.09 (assume-push @p1946 @t611) % 5.77/6.09 (assume-push @p1947 @t612) % 5.77/6.09 (assume-push @p1948 @t615) % 5.77/6.09 (assume-push @p1949 @t617) % 5.77/6.09 (step @p661 :rule symm :premises (@p21)) % 5.77/6.09 (step @p662 :rule refl :args (@t38)) % 5.77/6.09 (step @p663 :rule symm :premises (@p20)) % 5.77/6.09 (step @p664 :rule symm :premises (@p39)) % 5.77/6.09 (step @p665 :rule refl :args (tptp.truth)) % 5.77/6.09 (step @p666 :rule symm :premises (@p18)) % 5.77/6.09 (step @p667 :rule cong :premises (@p666 @p662) :args (@t51)) % 5.77/6.09 (step @p668 :rule cong :premises (@p667 @p665) :args (@t53)) % 5.77/6.09 (step @p669 :rule trans :premises (@p668 @p664 @p663)) % 5.77/6.09 (step @p670 :rule cong :premises (@p669 @p662) :args (@t274)) % 5.77/6.09 (step @p671 :rule symm :premises (@p33)) % 5.77/6.09 (step @p103 :rule instantiate :premises (@p10) :args (@t85)) % 5.77/6.09 (step @p672 :rule symm :premises (@p207)) % 5.77/6.09 (step @p673 :rule symm :premises (@p302)) % 5.77/6.09 (step @p674 :rule refl :args (@t32)) % 5.77/6.09 (step @p675 :rule symm :premises (@p140)) % 5.77/6.09 (step @p676 :rule symm :premises (@p28)) % 5.77/6.09 (step @p677 :rule symm :premises (@p19)) % 5.77/6.09 (step @p678 :rule cong :premises (@p662 @p677) :args (@t618)) % 5.77/6.09 (step @p679 :rule trans :premises (@p678 @p676)) % 5.77/6.09 (step @p680 :rule cong :premises (@p665 @p679) :args (@t619)) % 5.77/6.09 (step @p681 :rule trans :premises (@p680 @p675)) % 5.77/6.09 (step @p682 :rule symm :premises (@p678)) % 5.77/6.09 (step @p683 :rule symm :premises (@p17)) % 5.77/6.09 (step @p684 :rule trans :premises (@p683 @p12 @p28 @p682)) % 5.77/6.09 (step @p685 :rule cong :premises (@p665 @p684) :args (@t104)) % 5.77/6.09 (step @p686 :rule symm :premises (@p684)) % 5.77/6.09 (step @p687 :rule cong :premises (@p686 @p665) :args ((tptp.xor @t618 tptp.truth))) % 5.77/6.09 (step @p688 :rule symm :premises (@p32)) % 5.77/6.09 (step @p689 :rule refl :args (@t40)) % 5.77/6.09 (step @p690 :rule symm :premises (@p145)) % 5.77/6.09 (step @p691 :rule cong :premises (@p665 @p690) :args (@t620)) % 5.77/6.09 (step @p692 :rule cong :premises (@p691 @p689) :args (@t621)) % 5.77/6.09 (step @p693 :rule trans :premises (@p692 @p688 @p15 @p17)) % 5.77/6.09 (step @p694 :rule trans :premises (@p693 @p684)) % 5.77/6.09 (step @p695 :rule cong :premises (@p694 @p665) :args (@t622)) % 5.77/6.09 (step @p696 :rule trans :premises (@p695 @p687 @p157 @p685)) % 5.77/6.09 (step @p697 :rule trans :premises (@p696 @p681)) % 5.77/6.09 (step @p698 :rule cong :premises (@p697 @p674) :args ((tptp.and_star @t622 @t32))) % 5.77/6.09 (step @p699 :rule symm :premises (@p696)) % 5.77/6.09 (step @p700 :rule symm :premises (@p147)) % 5.77/6.09 (step @p701 :rule refl :args (@t64)) % 5.77/6.09 (step @p702 :rule cong :premises (@p79 @p701) :args (@t461)) % 5.77/6.09 (step @p703 :rule symm :premises (@p175)) % 5.77/6.09 (step @p704 :rule symm :premises (@p670)) % 5.77/6.09 (step @p705 :rule trans :premises (@p704 @p33 @p117)) % 5.77/6.09 (step @p706 :rule refl :args (@t57)) % 5.77/6.09 (step @p707 :rule cong :premises (@p706 @p705) :args (@t112)) % 5.77/6.09 (step @p708 :rule symm :premises (@p180)) % 5.77/6.09 (step @p709 :rule symm :premises (@p78)) % 5.77/6.09 (step @p122 :rule instantiate :premises (@p1) :args (@t63)) % 5.77/6.09 (step @p710 :rule symm :premises (@p36)) % 5.77/6.09 (step @p711 :rule symm :premises (@p38)) % 5.77/6.09 (step @p712 :rule trans :premises (@p711 @p677)) % 5.77/6.09 (step @p713 :rule cong :premises (@p712 @p665) :args (@t292)) % 5.77/6.09 (step @p714 :rule trans :premises (@p15 @p17)) % 5.77/6.09 (step @p715 :rule refl :args (@t36)) % 5.77/6.09 (step @p716 :rule cong :premises (@p715 @p714) :args (@t326)) % 5.77/6.09 (step @p717 :rule trans :premises (@p141 @p716 @p74 @p713 @p710)) % 5.77/6.09 (step @p718 :rule cong :premises (@p717) :args (@t44)) % 5.77/6.09 (step @p719 :rule trans :premises (@p38 @p54 @p718 @p122 @p709)) % 5.77/6.09 (step @p720 :rule cong :premises (@p689 @p719) :args (@t484)) % 5.77/6.09 (step @p721 :rule trans :premises (@p720 @p708 @p707 @p703 @p307 @p702 @p700 @p28 @p682)) % 5.77/6.09 (step @p722 :rule cong :premises (@p665 @p721) :args (@t485)) % 5.77/6.09 (step @p723 :rule symm :premises (@p720)) % 5.77/6.09 (step @p724 :rule trans :premises (@p180 @p723)) % 5.77/6.09 (step @p725 :rule cong :premises (@p665 @p724) :args (@t361)) % 5.77/6.09 (step @p726 :rule trans :premises (@p169 @p725 @p722)) % 5.77/6.09 (step @p727 :rule trans :premises (@p726 @p699)) % 5.77/6.09 (step @p728 :rule cong :premises (@p727 @p674) :args (@t552)) % 5.77/6.09 (step @p729 :rule trans :premises (@p728 @p698 @p673 @p672)) % 5.77/6.09 (step @p730 :rule cong :premises (@p727 @p729) :args (@t553)) % 5.77/6.09 (step @p731 :rule trans :premises (@p379 @p730 @p698 @p673 @p672)) % 5.77/6.09 (step @p732 :rule symm :premises (@p329)) % 5.77/6.09 (step @p733 :rule symm :premises (@p30)) % 5.77/6.09 (step @p94 :rule instantiate :premises (@p10) :args (@t78)) % 5.77/6.09 (step @p734 :rule refl :args (@t35)) % 5.77/6.09 (step @p735 :rule refl :args (tptp.b)) % 5.77/6.09 (step @p736 :rule symm :premises (@p42)) % 5.77/6.09 (step @p737 :rule cong :premises (@p736 @p665) :args (@t116)) % 5.77/6.09 (step @p738 :rule trans :premises (@p737 @p711)) % 5.77/6.09 (step @p739 :rule cong :premises (@p738 @p735) :args (@t294)) % 5.77/6.09 (step @p740 :rule refl :args (tptp.a)) % 5.77/6.09 (step @p741 :rule cong :premises (@p41 @p665) :args (@t145)) % 5.77/6.09 (step @p742 :rule trans :premises (@p18 @p37 @p741)) % 5.77/6.09 (step @p743 :rule trans :premises (@p666 @p742)) % 5.77/6.09 (step @p744 :rule cong :premises (@p743 @p740) :args (@t66)) % 5.77/6.09 (step @p745 :rule trans :premises (@p744 @p75 @p739)) % 5.77/6.09 (step @p746 :rule symm :premises (@p744)) % 5.77/6.09 (step @p747 :rule trans :premises (@p746 @p745)) % 5.77/6.09 (step @p748 :rule cong :premises (@p747 @p734) :args (@t367)) % 5.77/6.09 (step @p749 :rule symm :premises (@p172)) % 5.77/6.09 (step @p750 :rule symm :premises (@p73)) % 5.77/6.09 (step @p751 :rule trans :premises (@p750 @p26 @p114)) % 5.77/6.09 (step @p752 :rule cong :premises (@p742 @p751) :args (@t380)) % 5.77/6.09 (step @p753 :rule symm :premises (@p109)) % 5.77/6.09 (step @p754 :rule cong :premises (@p706 @p43) :args (@t58)) % 5.77/6.09 (step @p755 :rule trans :premises (@p754 @p753 @p177 @p752 @p749 @p748 @p94 @p733)) % 5.77/6.09 (step @p756 :rule refl :args (@t95)) % 5.77/6.09 (step @p757 :rule cong :premises (@p756 @p755) :args ((tptp.and_star @t95 @t58))) % 5.77/6.09 (step @p758 :rule symm :premises (@p754)) % 5.77/6.09 (step @p759 :rule symm :premises (@p177)) % 5.77/6.09 (step @p760 :rule symm :premises (@p752)) % 5.77/6.09 (step @p761 :rule symm :premises (@p748)) % 5.77/6.09 (step @p762 :rule symm :premises (@p330)) % 5.77/6.09 (step @p763 :rule cong :premises (@p662 @p755) :args (@t623)) % 5.77/6.09 (step @p764 :rule symm :premises (@p43)) % 5.77/6.09 (step @p765 :rule trans :premises (@p19 @p38 @p54 @p718 @p122 @p709)) % 5.77/6.09 (step @p766 :rule cong :premises (@p765 @p764) :args ((tptp.and_star @t24 @t120))) % 5.77/6.09 (step @p767 :rule symm :premises (@p206)) % 5.77/6.09 (step @p768 :rule refl :args (@t119)) % 5.77/6.09 (step @p769 :rule cong :premises (@p768 @p666) :args (@t624)) % 5.77/6.09 (step @p770 :rule trans :premises (@p769 @p177 @p752 @p749 @p748 @p94 @p733 @p28 @p682)) % 5.77/6.09 (step @p771 :rule cong :premises (@p665 @p770) :args ((tptp.xor tptp.truth @t624))) % 5.77/6.09 (step @p772 :rule symm :premises (@p769)) % 5.77/6.09 (step @p773 :rule trans :premises (@p754 @p753 @p772)) % 5.77/6.09 (step @p774 :rule cong :premises (@p665 @p773) :args (@t133)) % 5.77/6.09 (step @p775 :rule trans :premises (@p80 @p774 @p771 @p680 @p675)) % 5.77/6.09 (step @p776 :rule refl :args (@t25)) % 5.77/6.09 (step @p777 :rule cong :premises (@p776 @p775) :args (@t372)) % 5.77/6.09 (step @p778 :rule trans :premises (@p777 @p767)) % 5.77/6.09 (step @p779 :rule trans :premises (@p736 @p141 @p716 @p74 @p713 @p710)) % 5.77/6.09 (step @p780 :rule cong :premises (@p779 @p778) :args ((tptp.and_star @t115 @t372))) % 5.77/6.09 (step @p781 :rule refl :args (@t372)) % 5.77/6.09 (step @p782 :rule symm :premises (@p779)) % 5.77/6.09 (step @p783 :rule cong :premises (@p782 @p781) :args (@t373)) % 5.77/6.09 (step @p784 :rule refl :args (@t60)) % 5.77/6.09 (step @p785 :rule cong :premises (@p43 @p784) :args (@t323)) % 5.77/6.09 (step @p786 :rule trans :premises (@p34 @p118 @p785 @p174 @p783 @p780)) % 5.77/6.09 (step @p787 :rule symm :premises (@p765)) % 5.77/6.09 (step @p788 :rule cong :premises (@p787 @p786) :args ((tptp.and_star @t57 @t111))) % 5.77/6.09 (step @p789 :rule symm :premises (@p34)) % 5.77/6.09 (step @p790 :rule symm :premises (@p118)) % 5.77/6.09 (step @p791 :rule symm :premises (@p785)) % 5.77/6.09 (step @p792 :rule symm :premises (@p174)) % 5.77/6.09 (step @p793 :rule symm :premises (@p783)) % 5.77/6.09 (step @p794 :rule symm :premises (@p780)) % 5.77/6.09 (step @p795 :rule symm :premises (@p324)) % 5.77/6.09 (step @p796 :rule symm :premises (@p714)) % 5.77/6.09 (step @p797 :rule refl :args (@t51)) % 5.77/6.09 (step @p798 :rule cong :premises (@p797 @p796) :args (@t410)) % 5.77/6.09 (step @p799 :rule symm :premises (@p223)) % 5.77/6.09 (step @p800 :rule symm :premises (@p669)) % 5.77/6.09 (step @p801 :rule cong :premises (@p800 @p665) :args (@t357)) % 5.77/6.09 (step @p802 :rule trans :premises (@p167 @p801 @p799 @p798 @p795 @p667 @p43 @p794 @p793 @p792 @p791 @p790 @p789)) % 5.77/6.09 (step @p803 :rule cong :premises (@p719 @p802) :args ((tptp.and_star @t73 @t125))) % 5.77/6.09 (step @p804 :rule refl :args (@t125)) % 5.77/6.09 (step @p805 :rule cong :premises (@p19 @p804) :args (@t392)) % 5.77/6.09 (step @p806 :rule trans :premises (@p805 @p803 @p788 @p766)) % 5.77/6.09 (step @p807 :rule cong :premises (@p662 @p806) :args ((tptp.and_star @t38 @t392))) % 5.77/6.09 (step @p808 :rule cong :premises (@p662 @p184) :args ((tptp.and_star @t38 @t211))) % 5.77/6.09 (step @p809 :rule refl :args (@t211)) % 5.77/6.09 (step @p810 :rule symm :premises (@p208)) % 5.77/6.09 (step @p811 :rule cong :premises (@p662 @p775) :args (@t388)) % 5.77/6.09 (step @p812 :rule cong :premises (@p784 @p779) :args (@t445)) % 5.77/6.09 (step @p813 :rule trans :premises (@p251 @p812 @p182 @p811 @p810)) % 5.77/6.09 (step @p814 :rule cong :premises (@p813 @p809) :args (@t527)) % 5.77/6.09 (step @p815 :rule symm :premises (@p352)) % 5.77/6.09 (step @p816 :rule symm :premises (@p184)) % 5.77/6.09 (step @p817 :rule symm :premises (@p805)) % 5.77/6.09 (step @p818 :rule symm :premises (@p803)) % 5.77/6.09 (step @p819 :rule symm :premises (@p788)) % 5.77/6.09 (step @p820 :rule symm :premises (@p766)) % 5.77/6.09 (step @p821 :rule trans :premises (@p683 @p12 @p30 @p99 @p761 @p172 @p760 @p759 @p109 @p758 @p820 @p819 @p818 @p817 @p816)) % 5.77/6.09 (step @p822 :rule cong :premises (@p735 @p821) :args (@t450)) % 5.77/6.09 (step @p823 :rule cong :premises (@p735 @p714) :args (@t495)) % 5.77/6.09 (step @p824 :rule symm :premises (@p27)) % 5.77/6.09 (step @p825 :rule symm :premises (@p113)) % 5.77/6.09 (step @p826 :rule trans :premises (@p825 @p824 @p331 @p823 @p822)) % 5.77/6.09 (step @p827 :rule refl :args (@t212)) % 5.77/6.09 (step @p828 :rule cong :premises (@p827 @p826) :args (@t537)) % 5.77/6.09 (step @p829 :rule symm :premises (@p813)) % 5.77/6.09 (step @p830 :rule trans :premises (@p717 @p829)) % 5.77/6.09 (step @p831 :rule cong :premises (@p830 @p674) :args ((tptp.and_star @t36 @t32))) % 5.77/6.09 (step @p832 :rule symm :premises (@p717)) % 5.77/6.09 (step @p833 :rule cong :premises (@p832 @p674) :args (@t596)) % 5.77/6.09 (step @p834 :rule trans :premises (@p833 @p831 @p356 @p828 @p815 @p814 @p808 @p807 @p763 @p762 @p30 @p99 @p761 @p172 @p760 @p759 @p109 @p758)) % 5.77/6.09 (step @p835 :rule cong :premises (@p20 @p662) :args (@t40)) % 5.77/6.09 (step @p836 :rule cong :premises (@p835 @p665) :args (@t285)) % 5.77/6.09 (step @p837 :rule trans :premises (@p40 @p836)) % 5.77/6.09 (step @p838 :rule symm :premises (@p837)) % 5.77/6.09 (step @p839 :rule cong :premises (@p838 @p834) :args (@t597)) % 5.77/6.09 (step @p840 :rule cong :premises (@p802 @p729) :args ((tptp.and_star @t125 @t552))) % 5.77/6.09 (step @p841 :rule symm :premises (@p729)) % 5.77/6.09 (step @p842 :rule cong :premises (@p804 @p841) :args (@t245)) % 5.77/6.09 (step @p843 :rule symm :premises (@p387)) % 5.77/6.09 (step @p844 :rule trans :premises (@p843 @p842 @p840 @p437 @p839 @p757 @p732 @p28 @p682)) % 5.77/6.09 (step @p845 :rule cong :premises (@p665 @p844) :args ((tptp.xor tptp.truth @t572))) % 5.77/6.09 (step @p846 :rule cong :premises (@p665 @p387) :args (@t246)) % 5.77/6.09 (step @p847 :rule trans :premises (@p435 @p846 @p845)) % 5.77/6.09 (step @p848 :rule trans :premises (@p847 @p699)) % 5.77/6.09 (step @p849 :rule cong :premises (@p848 @p731) :args ((tptp.and_star @t247 @t554))) % 5.77/6.09 (step @p850 :rule symm :premises (@p731)) % 5.77/6.09 (step @p851 :rule refl :args (@t247)) % 5.77/6.09 (step @p852 :rule cong :premises (@p851 @p850) :args (@t508)) % 5.77/6.09 (step @p853 :rule symm :premises (@p335)) % 5.77/6.09 (step @p854 :rule symm :premises (@p442)) % 5.77/6.09 (step @p855 :rule trans :premises (@p854 @p853 @p852 @p849 @p698 @p673 @p672)) % 5.77/6.09 (step @p856 :rule symm :premises (@p79)) % 5.77/6.09 (step @p857 :rule cong :premises (@p856 @p740) :args (@t127)) % 5.77/6.09 (step @p858 :rule symm :premises (@p444)) % 5.77/6.09 (step @p859 :rule refl :args (@t127)) % 5.77/6.09 (step @p860 :rule cong :premises (@p859 @p796) :args (@t241)) % 5.77/6.09 (step @p861 :rule symm :premises (@p436)) % 5.77/6.09 (step @p862 :rule symm :premises (@p243)) % 5.77/6.09 (step @p863 :rule symm :premises (@p857)) % 5.77/6.09 (step @p864 :rule cong :premises (@p665 @p863) :args (@t625)) % 5.77/6.09 (step @p865 :rule trans :premises (@p864 @p862)) % 5.77/6.09 (step @p866 :rule cong :premises (@p665 @p865) :args (@t626)) % 5.77/6.09 (step @p867 :rule symm :premises (@p864)) % 5.77/6.09 (step @p190 :rule instantiate :premises (@p1) :args (@t131)) % 5.77/6.09 (step @p868 :rule symm :premises (@p181)) % 5.77/6.09 (step @p869 :rule symm :premises (@p412)) % 5.77/6.09 (step @p870 :rule cong :premises (@p740 @p796) :args (@t519)) % 5.77/6.09 (step @p871 :rule trans :premises (@p224 @p338 @p870 @p869)) % 5.77/6.09 (step @p872 :rule cong :premises (@p871 @p856) :args ((tptp.and_star @t199 @t126))) % 5.77/6.09 (step @p873 :rule refl :args (@t199)) % 5.77/6.09 (step @p874 :rule cong :premises (@p873 @p79) :args (@t236)) % 5.77/6.09 (step @p875 :rule trans :premises (@p874 @p872 @p868 @p863)) % 5.77/6.09 (step @p876 :rule cong :premises (@p875) :args (@t237)) % 5.77/6.09 (step @p877 :rule trans :premises (@p411 @p876 @p190 @p243 @p867)) % 5.77/6.09 (step @p878 :rule cong :premises (@p665 @p877) :args ((tptp.xor tptp.truth @t238))) % 5.77/6.09 (step @p879 :rule trans :premises (@p878 @p866 @p861 @p425 @p860 @p858 @p857)) % 5.77/6.09 (step @p880 :rule symm :premises (@p878)) % 5.77/6.09 (step @p881 :rule trans :premises (@p880 @p879)) % 5.77/6.09 (step @p882 :rule cong :premises (@p881 @p855) :args ((tptp.and_star @t626 @t608))) % 5.77/6.09 (step @p883 :rule symm :premises (@p855)) % 5.77/6.09 (step @p884 :rule refl :args (@t626)) % 5.77/6.09 (step @p885 :rule cong :premises (@p884 @p883) :args (@t627)) % 5.77/6.09 (step @p886 :rule trans :premises (@p885 @p882 @p103 @p671 @p670)) % 5.77/6.09 (step @p887 :rule cong :premises (@p665 @p886) :args ((tptp.xor tptp.truth @t627))) % 5.77/6.09 (step @p888 :rule symm :premises (@p885)) % 5.77/6.09 (step @p889 :rule symm :premises (@p882)) % 5.77/6.09 (step @p890 :rule symm :premises (@p44)) % 5.77/6.09 (step @p891 :rule refl :args (@t26)) % 5.77/6.09 (step @p892 :rule cong :premises (@p779 @p891) :args (@t440)) % 5.77/6.09 (step @p893 :rule symm :premises (@p249)) % 5.77/6.09 (step @p894 :rule refl :args (@t439)) % 5.77/6.09 (step @p895 :rule symm :premises (@p415)) % 5.77/6.09 (step @p896 :rule cong :premises (@p734 @p775) :args (@t568)) % 5.77/6.09 (step @p897 :rule trans :premises (@p385 @p896 @p895)) % 5.77/6.09 (step @p898 :rule symm :premises (@p80)) % 5.77/6.09 (step @p899 :rule symm :premises (@p774)) % 5.77/6.09 (step @p900 :rule symm :premises (@p771)) % 5.77/6.09 (step @p901 :rule trans :premises (@p900 @p899 @p898)) % 5.77/6.09 (step @p902 :rule symm :premises (@p29)) % 5.77/6.09 (step @p85 :rule instantiate :premises (@p10) :args (@t70)) % 5.77/6.09 (step @p903 :rule symm :premises (@p75)) % 5.77/6.09 (step @p904 :rule trans :premises (@p903 @p746)) % 5.77/6.09 (step @p905 :rule cong :premises (@p904 @p674) :args (@t365)) % 5.77/6.09 (step @p906 :rule symm :premises (@p171)) % 5.77/6.09 (step @p907 :rule symm :premises (@p146)) % 5.77/6.09 (step @p908 :rule symm :premises (@p310)) % 5.77/6.09 (step @p909 :rule symm :premises (@p166)) % 5.77/6.09 (step @p910 :rule symm :premises (@p37)) % 5.77/6.09 (step @p911 :rule trans :premises (@p910 @p666)) % 5.77/6.09 (step @p912 :rule cong :premises (@p911 @p665) :args (@t146)) % 5.77/6.09 (step @p217 :rule instantiate :premises (@p7) :args (@t148)) % 5.77/6.09 (step @p913 :rule refl :args (@t33)) % 5.77/6.09 (step @p914 :rule cong :premises (@p913 @p714) :args (@t488)) % 5.77/6.09 (step @p915 :rule trans :premises (@p322 @p914 @p217 @p912 @p909)) % 5.77/6.09 (step @p916 :rule symm :premises (@p301)) % 5.77/6.09 (step @p917 :rule trans :premises (@p683 @p12 @p73)) % 5.77/6.09 (step @p918 :rule cong :premises (@p917 @p776) :args (@t343)) % 5.77/6.09 (step @p919 :rule trans :premises (@p918 @p109 @p758)) % 5.77/6.09 (step @p920 :rule cong :premises (@p919 @p665) :args (@t344)) % 5.77/6.09 (step @p921 :rule cong :premises (@p920 @p776) :args (@t345)) % 5.77/6.09 (step @p922 :rule symm :premises (@p162)) % 5.77/6.09 (step @p923 :rule symm :premises (@p245)) % 5.77/6.09 (step @p924 :rule cong :premises (@p665 @p210) :args ((tptp.xor tptp.truth @t113))) % 5.77/6.09 (step @p925 :rule symm :premises (@p41)) % 5.77/6.09 (step @p926 :rule symm :premises (@p35)) % 5.77/6.09 (step @p927 :rule trans :premises (@p774 @p771 @p680 @p675)) % 5.77/6.09 (step @p928 :rule cong :premises (@p735 @p927) :args ((tptp.xor tptp.b @t133))) % 5.77/6.09 (step @p929 :rule symm :premises (@p927)) % 5.77/6.09 (step @p930 :rule symm :premises (@p321)) % 5.77/6.09 (step @p931 :rule cong :premises (@p735 @p796) :args (@t416)) % 5.77/6.09 (step @p932 :rule symm :premises (@p240)) % 5.77/6.09 (step @p933 :rule cong :premises (@p672 @p927) :args ((tptp.xor @t142 @t133))) % 5.77/6.09 (step @p934 :rule refl :args (@t142)) % 5.77/6.09 (step @p935 :rule cong :premises (@p934 @p929) :args (@t143)) % 5.77/6.09 (step @p936 :rule trans :premises (@p935 @p933 @p932 @p158 @p235 @p931 @p930)) % 5.77/6.09 (step @p937 :rule symm :premises (@p935)) % 5.77/6.09 (step @p938 :rule symm :premises (@p933)) % 5.77/6.09 (step @p939 :rule cong :premises (@p926 @p665) :args (@t628)) % 5.77/6.09 (step @p940 :rule trans :premises (@p939 @p938 @p937)) % 5.77/6.09 (step @p941 :rule trans :premises (@p940 @p936)) % 5.77/6.09 (step @p942 :rule cong :premises (@p941 @p929) :args ((tptp.xor @t628 tptp.truth))) % 5.77/6.09 (step @p943 :rule symm :premises (@p940)) % 5.77/6.09 (step @p944 :rule symm :premises (@p212)) % 5.77/6.09 (step @p945 :rule symm :premises (@p316)) % 5.77/6.09 (step @p946 :rule refl :args (@t143)) % 5.77/6.09 (step @p947 :rule cong :premises (@p927 @p946) :args (@t629)) % 5.77/6.09 (step @p948 :rule trans :premises (@p947 @p945 @p944)) % 5.77/6.09 (step @p949 :rule trans :premises (@p948 @p943)) % 5.77/6.09 (step @p950 :rule cong :premises (@p949 @p665) :args ((tptp.xor @t629 tptp.truth))) % 5.77/6.09 (step @p951 :rule trans :premises (@p950 @p942 @p928 @p926)) % 5.77/6.09 (step @p952 :rule symm :premises (@p950)) % 5.77/6.09 (step @p953 :rule cong :premises (@p946 @p927) :args ((tptp.and_star @t143 @t133))) % 5.77/6.09 (step @p954 :rule trans :premises (@p240 @p938 @p937)) % 5.77/6.09 (step @p955 :rule cong :premises (@p954 @p929) :args (@t503)) % 5.77/6.09 (step @p956 :rule trans :premises (@p955 @p953 @p944)) % 5.77/6.09 (step @p957 :rule trans :premises (@p956 @p943)) % 5.77/6.09 (step @p958 :rule cong :premises (@p957 @p665) :args (@t504)) % 5.77/6.09 (step @p959 :rule trans :premises (@p958 @p952)) % 5.77/6.09 (step @p960 :rule trans :premises (@p959 @p951)) % 5.77/6.09 (step @p961 :rule cong :premises (@p960 @p665) :args (@t505)) % 5.77/6.09 (step @p962 :rule symm :premises (@p334)) % 5.77/6.09 (step @p963 :rule symm :premises (@p26)) % 5.77/6.09 (step @p964 :rule trans :premises (@p963 @p15 @p17)) % 5.77/6.09 (step @p965 :rule cong :premises (@p964 @p674) :args (@t170)) % 5.77/6.09 (step @p966 :rule trans :premises (@p269 @p965)) % 5.77/6.09 (step @p967 :rule cong :premises (@p966 @p927) :args ((tptp.xor @t158 @t133))) % 5.77/6.09 (step @p968 :rule refl :args (@t158)) % 5.77/6.09 (step @p969 :rule cong :premises (@p968 @p929) :args (@t190)) % 5.77/6.09 (step @p970 :rule trans :premises (@p969 @p967)) % 5.77/6.09 (step @p971 :rule cong :premises (@p970 @p674) :args (@t539)) % 5.77/6.09 (step @p972 :rule trans :premises (@p971 @p962 @p961 @p672)) % 5.77/6.09 (step @p973 :rule cong :premises (@p972 @p740) :args (@t540)) % 5.77/6.09 (step @p974 :rule symm :premises (@p357)) % 5.77/6.09 (step @p975 :rule refl :args (@t190)) % 5.77/6.09 (step @p976 :rule cong :premises (@p975 @p41) :args (@t340)) % 5.77/6.09 (step @p977 :rule symm :premises (@p313)) % 5.77/6.09 (step @p978 :rule symm :premises (@p242)) % 5.77/6.09 (step @p979 :rule cong :premises (@p913 @p978) :args (@t630)) % 5.77/6.09 (step @p980 :rule trans :premises (@p979 @p977 @p976 @p974 @p973 @p925 @p322 @p914 @p217 @p912 @p909)) % 5.77/6.09 (step @p981 :rule cong :premises (@p665 @p980) :args ((tptp.xor tptp.truth @t630))) % 5.77/6.09 (step @p982 :rule symm :premises (@p979)) % 5.77/6.09 (step @p983 :rule symm :premises (@p745)) % 5.77/6.09 (step @p984 :rule cong :premises (@p983 @p665) :args (@t422)) % 5.77/6.09 (step @p985 :rule symm :premises (@p238)) % 5.77/6.09 (step @p986 :rule trans :premises (@p985 @p984)) % 5.77/6.09 (step @p987 :rule cong :premises (@p986 @p740) :args (@t208)) % 5.77/6.09 (step @p988 :rule trans :premises (@p987 @p161 @p313 @p982)) % 5.77/6.09 (step @p989 :rule cong :premises (@p665 @p988) :args (@t521)) % 5.77/6.09 (step @p990 :rule trans :premises (@p349 @p989 @p981 @p924 @p923 @p211 @p922 @p921 @p916 @p777 @p767)) % 5.77/6.09 (step @p991 :rule refl :args (@t208)) % 5.77/6.09 (step @p992 :rule cong :premises (@p991 @p927) :args ((tptp.xor @t208 @t133))) % 5.77/6.09 (step @p993 :rule symm :premises (@p987)) % 5.77/6.09 (step @p994 :rule symm :premises (@p161)) % 5.77/6.09 (step @p995 :rule cong :premises (@p978 @p913) :args (@t499)) % 5.77/6.09 (step @p996 :rule trans :premises (@p995 @p994 @p993)) % 5.77/6.09 (step @p997 :rule cong :premises (@p996 @p929) :args (@t500)) % 5.77/6.09 (step @p998 :rule trans :premises (@p997 @p992)) % 5.77/6.09 (step @p999 :rule trans :premises (@p998 @p990)) % 5.77/6.09 (step @p1000 :rule cong :premises (@p999 @p915) :args (@t501)) % 5.77/6.09 (step @p1001 :rule symm :premises (@p333)) % 5.77/6.09 (step @p264 :rule instantiate :premises (@p10) :args (@t172)) % 5.77/6.09 (step @p1002 :rule symm :premises (@p964)) % 5.77/6.09 (step @p1003 :rule symm :premises (@p331)) % 5.77/6.09 (step @p1004 :rule symm :premises (@p823)) % 5.77/6.09 (step @p1005 :rule symm :premises (@p25)) % 5.77/6.09 (step @p1006 :rule symm :premises (@p110)) % 5.77/6.09 (step @p1007 :rule symm :premises (@p115)) % 5.77/6.09 (step @p1008 :rule trans :premises (@p1007 @p676 @p15 @p17)) % 5.77/6.09 (step @p1009 :rule cong :premises (@p665 @p1008) :args (@t377)) % 5.77/6.09 (step @p1010 :rule symm :premises (@p318)) % 5.77/6.09 (step @p1011 :rule trans :premises (@p1010 @p176 @p1009 @p1006 @p1005 @p15 @p17)) % 5.77/6.09 (step @p1012 :rule cong :premises (@p1011 @p735) :args ((tptp.and_star @t480 tptp.b))) % 5.77/6.09 (step @p1013 :rule trans :premises (@p945 @p944)) % 5.77/6.09 (step @p1014 :rule cong :premises (@p665 @p1013) :args (@t559)) % 5.77/6.09 (step @p1015 :rule trans :premises (@p381 @p1014 @p945 @p944 @p935 @p933 @p932 @p158 @p235 @p931 @p930)) % 5.77/6.09 (step @p1016 :rule symm :premises (@p1011)) % 5.77/6.09 (step @p1017 :rule symm :premises (@p114)) % 5.77/6.09 (step @p1018 :rule symm :premises (@p775)) % 5.77/6.09 (step @p1019 :rule cong :premises (@p1018 @p734) :args (@t631)) % 5.77/6.09 (step @p1020 :rule trans :premises (@p1019 @p385 @p896 @p895)) % 5.77/6.09 (step @p1021 :rule cong :premises (@p740 @p1020) :args ((tptp.and_star tptp.a @t631))) % 5.77/6.09 (step @p1022 :rule symm :premises (@p1019)) % 5.77/6.09 (step @p1023 :rule cong :premises (@p740 @p1022) :args ((tptp.and_star tptp.a @t212))) % 5.77/6.09 (step @p1024 :rule symm :premises (@p385)) % 5.77/6.09 (step @p1025 :rule symm :premises (@p896)) % 5.77/6.09 (step @p1026 :rule trans :premises (@p1025 @p1024)) % 5.77/6.09 (step @p1027 :rule cong :premises (@p871 @p1026) :args ((tptp.and_star @t199 @t588))) % 5.77/6.09 (step @p1028 :rule symm :premises (@p1026)) % 5.77/6.09 (step @p1029 :rule cong :premises (@p873 @p1028) :args (@t545)) % 5.77/6.09 (step @p1030 :rule trans :premises (@p1029 @p1027 @p1023 @p1021 @p1017 @p963 @p15 @p17)) % 5.77/6.09 (step @p1031 :rule trans :premises (@p1030 @p1016)) % 5.77/6.09 (step @p1032 :rule cong :premises (@p1031 @p1015) :args ((tptp.and_star @t545 @t560))) % 5.77/6.09 (step @p1033 :rule symm :premises (@p1015)) % 5.77/6.09 (step @p1034 :rule refl :args (@t545)) % 5.77/6.09 (step @p1035 :rule cong :premises (@p1034 @p1033) :args (@t546)) % 5.77/6.09 (step @p1036 :rule symm :premises (@p377)) % 5.77/6.09 (step @p1037 :rule cong :premises (@p873 @p830) :args (@t574)) % 5.77/6.09 (step @p1038 :rule symm :premises (@p388)) % 5.77/6.09 (step @p1039 :rule cong :premises (@p832 @p873) :args ((tptp.and_star @t38 @t199))) % 5.77/6.09 (step @p1040 :rule symm :premises (@p871)) % 5.77/6.09 (step @p1041 :rule symm :premises (@p251)) % 5.77/6.09 (step @p1042 :rule symm :premises (@p812)) % 5.77/6.09 (step @p1043 :rule symm :premises (@p182)) % 5.77/6.09 (step @p1044 :rule symm :premises (@p811)) % 5.77/6.09 (step @p1045 :rule cong :premises (@p665 @p787) :args (@t213)) % 5.77/6.09 (step @p1046 :rule cong :premises (@p898 @p662) :args (@t134)) % 5.77/6.09 (step @p1047 :rule trans :premises (@p1046 @p182 @p811 @p810)) % 5.77/6.09 (step @p1048 :rule cong :premises (@p1047) :args (@t135)) % 5.77/6.09 (step @p1049 :rule refl :args (@t134)) % 5.77/6.09 (step @p1050 :rule cong :premises (@p1049 @p927) :args ((tptp.xor @t134 @t133))) % 5.77/6.09 (step @p1051 :rule symm :premises (@p1046)) % 5.77/6.09 (step @p1052 :rule trans :premises (@p1044 @p1043 @p1051)) % 5.77/6.09 (step @p1053 :rule cong :premises (@p1052 @p929) :args (@t197)) % 5.77/6.09 (step @p1054 :rule symm :premises (@p325)) % 5.77/6.09 (step @p1055 :rule symm :premises (@p1053)) % 5.77/6.09 (step @p1056 :rule symm :premises (@p1050)) % 5.77/6.09 (step @p1057 :rule trans :premises (@p1056 @p1055)) % 5.77/6.09 (step @p199 :rule instantiate :premises (@p1) :args (@t138)) % 5.77/6.09 (step @p1058 :rule symm :premises (@p1048)) % 5.77/6.09 (step @p1059 :rule trans :premises (@p78 @p127 @p1058 @p199)) % 5.77/6.09 (step @p1060 :rule trans :premises (@p765 @p1059 @p1057)) % 5.77/6.09 (step @p1061 :rule cong :premises (@p1060 @p775) :args ((tptp.and_star @t24 @t60))) % 5.77/6.09 (step @p1062 :rule symm :premises (@p835)) % 5.77/6.09 (step @p1063 :rule symm :premises (@p323)) % 5.77/6.09 (step @p1064 :rule refl :args (@t89)) % 5.77/6.09 (step @p1065 :rule cong :premises (@p1064 @p796) :args (@t150)) % 5.77/6.09 (step @p1066 :rule cong :premises (@p665 @p837) :args ((tptp.xor tptp.truth @t95))) % 5.77/6.09 (step @p1067 :rule trans :premises (@p1066 @p239 @p233 @p1065 @p1063)) % 5.77/6.09 (step @p1068 :rule symm :premises (@p1066)) % 5.77/6.09 (step @p1069 :rule trans :premises (@p1068 @p1067 @p1062)) % 5.77/6.09 (step @p1070 :rule cong :premises (@p1069 @p715) :args (@t482)) % 5.77/6.09 (step @p1071 :rule symm :premises (@p319)) % 5.77/6.09 (step @p1072 :rule refl :args (@t161)) % 5.77/6.09 (step @p1073 :rule cong :premises (@p1072 @p19) :args (@t162)) % 5.77/6.09 (step @p1074 :rule cong :premises (@p665 @p1073) :args (@t434)) % 5.77/6.09 (step @p1075 :rule trans :premises (@p246 @p1074 @p1071 @p1070 @p320 @p722 @p900 @p899 @p898)) % 5.77/6.09 (step @p1076 :rule cong :premises (@p677 @p1075) :args ((tptp.and_star @t73 @t191))) % 5.77/6.09 (step @p1077 :rule refl :args (@t191)) % 5.77/6.09 (step @p1078 :rule cong :premises (@p19 @p1077) :args (@t473)) % 5.77/6.09 (step @p1079 :rule refl :args (@t348)) % 5.77/6.09 (step @p1080 :rule cong :premises (@p1079 @p837) :args ((tptp.and_star @t348 @t95))) % 5.77/6.09 (step @p1081 :rule symm :premises (@p40)) % 5.77/6.09 (step @p1082 :rule cong :premises (@p890 @p665) :args (@t123)) % 5.77/6.09 (step @p1083 :rule trans :premises (@p1082 @p1081)) % 5.77/6.09 (step @p1084 :rule symm :premises (@p168)) % 5.77/6.09 (step @p1085 :rule cong :premises (@p837 @p662) :args (@t96)) % 5.77/6.09 (step @p1086 :rule symm :premises (@p1085)) % 5.77/6.09 (step @p1087 :rule cong :premises (@p1086 @p665) :args (@t359)) % 5.77/6.09 (step @p1088 :rule symm :premises (@p1087)) % 5.77/6.09 (step @p1089 :rule trans :premises (@p1085 @p112)) % 5.77/6.09 (step @p1090 :rule cong :premises (@p1089 @p665) :args (@t98)) % 5.77/6.09 (step @p1091 :rule symm :premises (@p1090)) % 5.77/6.09 (step @p1092 :rule trans :premises (@p1091 @p1088 @p1084)) % 5.77/6.09 (step @p1093 :rule symm :premises (@p1092)) % 5.77/6.09 (step @p131 :rule instantiate :premises (@p1) :args (@t100)) % 5.77/6.09 (step @p1094 :rule symm :premises (@p667)) % 5.77/6.09 (step @p1095 :rule trans :premises (@p1085 @p34 @p118 @p785 @p174 @p783 @p780 @p764 @p1094)) % 5.77/6.09 (step @p1096 :rule symm :premises (@p1095)) % 5.77/6.09 (step @p1097 :rule cong :premises (@p1096) :args (@t52)) % 5.77/6.09 (step @p1098 :rule symm :premises (@p668)) % 5.77/6.09 (step @p1099 :rule trans :premises (@p20 @p39 @p1098 @p63 @p1097 @p131 @p1088 @p1084)) % 5.77/6.09 (step @p1100 :rule trans :premises (@p1099 @p1093)) % 5.77/6.09 (step @p1101 :rule cong :premises (@p1100 @p1083) :args (@t383)) % 5.77/6.09 (step @p1102 :rule symm :premises (@p77)) % 5.77/6.09 (step @p1103 :rule refl :args (@t300)) % 5.77/6.09 (step @p1104 :rule cong :premises (@p1103 @p677) :args (@t632)) % 5.77/6.09 (step @p1105 :rule trans :premises (@p1104 @p1102 @p179 @p1101 @p1080 @p163 @p314 @p1078 @p1076 @p1061 @p1054 @p1053 @p1050 @p204 @p1048 @p122 @p709)) % 5.77/6.09 (step @p1106 :rule cong :premises (@p665 @p1105) :args ((tptp.xor tptp.truth @t632))) % 5.77/6.09 (step @p1107 :rule trans :premises (@p1106 @p1045 @p208 @p1044 @p1043 @p1042 @p1041)) % 5.77/6.09 (step @p1108 :rule symm :premises (@p1106)) % 5.77/6.09 (step @p1109 :rule symm :premises (@p1045)) % 5.77/6.09 (step @p1110 :rule symm :premises (@p390)) % 5.77/6.09 (step @p1111 :rule trans :premises (@p954 @p936)) % 5.77/6.09 (step @p1112 :rule cong :premises (@p1111 @p827) :args (@t633)) % 5.77/6.09 (step @p1113 :rule trans :premises (@p1112 @p1110 @p251 @p812 @p182 @p811 @p810 @p1109 @p1108)) % 5.77/6.09 (step @p1114 :rule trans :premises (@p1113 @p1107 @p813)) % 5.77/6.09 (step @p1115 :rule cong :premises (@p1114 @p1040) :args ((tptp.and_star @t633 tptp.a))) % 5.77/6.09 (step @p1116 :rule symm :premises (@p1114)) % 5.77/6.09 (step @p1117 :rule cong :premises (@p1116 @p740) :args (@t163)) % 5.77/6.09 (step @p1118 :rule cong :premises (@p779 @p740) :args (@t443)) % 5.77/6.09 (step @p1119 :rule symm :premises (@p250)) % 5.77/6.09 (step @p1120 :rule symm :premises (@p383)) % 5.77/6.09 (step @p1121 :rule trans :premises (@p1120 @p1119 @p1118 @p1117 @p1115 @p1039 @p1038 @p1037 @p1036 @p1035 @p1032 @p1012 @p280 @p1004 @p1003 @p15 @p17)) % 5.77/6.09 (step @p1122 :rule trans :premises (@p1121 @p1002)) % 5.77/6.09 (step @p1123 :rule cong :premises (@p1122 @p674) :args ((tptp.and_star @t564 @t32))) % 5.77/6.09 (step @p1124 :rule symm :premises (@p1118)) % 5.77/6.09 (step @p1125 :rule cong :premises (@p1045 @p740) :args (@t214)) % 5.77/6.09 (step @p1126 :rule trans :premises (@p1125 @p1124 @p250 @p383)) % 5.77/6.09 (step @p1127 :rule cong :premises (@p1126 @p674) :args (@t215)) % 5.77/6.09 (step @p1128 :rule trans :premises (@p813 @p1109)) % 5.77/6.09 (step @p1129 :rule cong :premises (@p1128 @p913) :args ((tptp.and_star @t446 @t33))) % 5.77/6.09 (step @p1130 :rule symm :premises (@p915)) % 5.77/6.09 (step @p1131 :rule cong :premises (@p829 @p1130) :args (@t468)) % 5.77/6.09 (step @p1132 :rule trans :premises (@p311 @p1131 @p1129 @p367 @p1127 @p1123 @p264)) % 5.77/6.09 (step @p397 :rule instantiate :premises (@p1) :args (@t234)) % 5.77/6.09 (step @p1133 :rule symm :premises (@p920)) % 5.77/6.09 (step @p1134 :rule cong :premises (@p18 @p913) :args (@t529)) % 5.77/6.09 (step @p1135 :rule trans :premises (@p1134 @p902 @p27 @p113)) % 5.77/6.09 (step @p1136 :rule symm :premises (@p738)) % 5.77/6.09 (step @p1137 :rule trans :premises (@p787 @p19 @p1136)) % 5.77/6.09 (step @p1138 :rule cong :premises (@p1137 @p1135) :args (@t530)) % 5.77/6.09 (step @p294 :rule instantiate :premises (@p11) :args (@t187)) % 5.77/6.09 (step @p1139 :rule cong :premises (@p666 @p706) :args (@t165)) % 5.77/6.09 (step @p1140 :rule trans :premises (@p1139 @p294)) % 5.77/6.09 (step @p1141 :rule cong :premises (@p1140 @p913) :args (@t166)) % 5.77/6.09 (step @p1142 :rule trans :premises (@p260 @p1141 @p353 @p1138 @p906 @p905 @p85 @p902 @p28 @p682)) % 5.77/6.09 (step @p1143 :rule cong :premises (@p775 @p1142) :args ((tptp.xor @t60 @t157))) % 5.77/6.09 (step @p1144 :rule refl :args (@t157)) % 5.77/6.09 (step @p1145 :rule cong :premises (@p1018 @p1144) :args (@t426)) % 5.77/6.09 (step @p1146 :rule trans :premises (@p241 @p1145 @p1143)) % 5.77/6.09 (step @p1147 :rule cong :premises (@p1144 @p927) :args ((tptp.xor @t157 @t133))) % 5.77/6.09 (step @p1148 :rule symm :premises (@p300)) % 5.77/6.09 (step @p1149 :rule refl :args (@t50)) % 5.77/6.09 (step @p1150 :rule symm :premises (@p205)) % 5.77/6.09 (step @p1151 :rule cong :premises (@p701 @p796) :args (@t336)) % 5.77/6.09 (step @p1152 :rule symm :premises (@p159)) % 5.77/6.09 (step @p1153 :rule symm :premises (@p236)) % 5.77/6.09 (step @p1154 :rule trans :premises (@p1153 @p1152 @p1151 @p1150)) % 5.77/6.09 (step @p1155 :rule cong :premises (@p1154 @p1149) :args (@t510)) % 5.77/6.09 (step @p1156 :rule trans :premises (@p1155 @p1148)) % 5.77/6.09 (step @p1157 :rule cong :premises (@p1156 @p929) :args (@t511)) % 5.77/6.09 (step @p1158 :rule trans :premises (@p1157 @p1147)) % 5.77/6.09 (step @p1159 :rule trans :premises (@p1158 @p1146 @p901 @p1133)) % 5.77/6.09 (step @p1160 :rule cong :premises (@p1159 @p666) :args (@t512)) % 5.77/6.09 (step @p1161 :rule symm :premises (@p336)) % 5.77/6.09 (step @p1162 :rule refl :args (@t80)) % 5.77/6.09 (step @p1163 :rule cong :premises (@p665 @p18) :args (@t113)) % 5.77/6.09 (step @p1164 :rule trans :premises (@p915 @p1163)) % 5.77/6.09 (step @p1165 :rule cong :premises (@p1164 @p856) :args ((tptp.and_star @t33 @t126))) % 5.77/6.09 (step @p1166 :rule cong :premises (@p913 @p79) :args (@t321)) % 5.77/6.09 (step @p1167 :rule trans :premises (@p1062 @p704 @p33 @p117 @p1166 @p1165)) % 5.77/6.09 (step @p1168 :rule cong :premises (@p856 @p913) :args (@t634)) % 5.77/6.09 (step @p1169 :rule trans :premises (@p1168 @p671 @p670 @p835)) % 5.77/6.09 (step @p1170 :rule trans :premises (@p1169 @p1167)) % 5.77/6.09 (step @p1171 :rule cong :premises (@p1170 @p665) :args ((tptp.xor @t634 tptp.truth))) % 5.77/6.09 (step @p1172 :rule symm :premises (@p1169)) % 5.77/6.09 (step @p1173 :rule trans :premises (@p835 @p1172)) % 5.77/6.09 (step @p1174 :rule cong :premises (@p1173 @p665) :args (@t285)) % 5.77/6.09 (step @p1175 :rule trans :premises (@p40 @p1174 @p1171)) % 5.77/6.09 (step @p1176 :rule cong :premises (@p1175 @p1162) :args (@t548)) % 5.77/6.09 (step @p1177 :rule symm :premises (@p209)) % 5.77/6.09 (step @p1178 :rule symm :premises (@p309)) % 5.77/6.09 (step @p1179 :rule trans :premises (@p1178 @p1177)) % 5.77/6.09 (step @p1180 :rule cong :premises (@p756 @p1179) :args (@t556)) % 5.77/6.09 (step @p1181 :rule trans :premises (@p380 @p1180 @p1176 @p1161 @p1160 @p921 @p916 @p777 @p767)) % 5.77/6.09 (step @p1182 :rule trans :premises (@p1181 @p18)) % 5.77/6.09 (step @p1183 :rule cong :premises (@p1182 @p968) :args ((tptp.and_star @t557 @t158))) % 5.77/6.09 (step @p1184 :rule symm :premises (@p1181)) % 5.77/6.09 (step @p1185 :rule cong :premises (@p1184 @p1132) :args (@t579)) % 5.77/6.09 (step @p1186 :rule symm :premises (@p311)) % 5.77/6.09 (step @p1187 :rule cong :premises (@p1186 @p776) :args (@t532)) % 5.77/6.09 (step @p1188 :rule symm :premises (@p354)) % 5.77/6.09 (step @p1189 :rule trans :premises (@p754 @p753 @p177 @p752 @p749 @p748 @p94 @p733 @p146)) % 5.77/6.09 (step @p1190 :rule cong :premises (@p662 @p1189) :args (@t623)) % 5.77/6.09 (step @p1191 :rule symm :premises (@p763)) % 5.77/6.09 (step @p1192 :rule trans :premises (@p754 @p753 @p177 @p752 @p749 @p748 @p94 @p733 @p330 @p1191 @p1190 @p1188 @p1187 @p391 @p1185 @p1183)) % 5.77/6.09 (step @p1193 :rule cong :premises (@p1192) :args (@t59)) % 5.77/6.09 (step @p1194 :rule trans :premises (@p900 @p899 @p898 @p72 @p1193 @p397)) % 5.77/6.09 (step @p1195 :rule symm :premises (@p681)) % 5.77/6.09 (step @p1196 :rule trans :premises (@p1195 @p1194)) % 5.77/6.09 (step @p1197 :rule cong :premises (@p1196 @p1132) :args (@t525)) % 5.77/6.09 (step @p1198 :rule trans :premises (@p210 @p312)) % 5.77/6.09 (step @p1199 :rule cong :premises (@p1198 @p662) :args (@t229)) % 5.77/6.09 (step @p1200 :rule symm :premises (@p1131)) % 5.77/6.09 (step @p1201 :rule symm :premises (@p1129)) % 5.77/6.09 (step @p362 :rule instantiate :premises (@p10) :args (@t218)) % 5.77/6.09 (step @p1202 :rule symm :premises (@p1127)) % 5.77/6.09 (step @p1203 :rule symm :premises (@p1123)) % 5.77/6.09 (step @p1204 :rule symm :premises (@p303)) % 5.77/6.09 (step @p1205 :rule cong :premises (@p1130 @p734) :args ((tptp.and_star @t113 @t35))) % 5.77/6.09 (step @p1206 :rule refl :args (@t113)) % 5.77/6.09 (step @p1207 :rule cong :premises (@p1206 @p895) :args ((tptp.and_star @t113 @t588))) % 5.77/6.09 (step @p1208 :rule cong :premises (@p1206 @p1028) :args ((tptp.and_star @t113 @t212))) % 5.77/6.09 (step @p1209 :rule cong :premises (@p915 @p827) :args (@t635)) % 5.77/6.09 (step @p1210 :rule trans :premises (@p1209 @p1208 @p1207 @p1205 @p1204 @p269 @p1203 @p1202 @p362 @p1201 @p1200 @p1186 @p1199 @p351 @p1197 @p1001 @p1000 @p908 @p907 @p27 @p113)) % 5.77/6.09 (step @p1211 :rule cong :premises (@p1137 @p1210) :args ((tptp.and_star @t57 @t635))) % 5.77/6.09 (step @p1212 :rule symm :premises (@p1209)) % 5.77/6.09 (step @p1213 :rule symm :premises (@p1208)) % 5.77/6.09 (step @p1214 :rule symm :premises (@p1207)) % 5.77/6.09 (step @p1215 :rule symm :premises (@p1205)) % 5.77/6.09 (step @p1216 :rule trans :premises (@p303 @p1215 @p1214 @p1213 @p1212)) % 5.77/6.09 (step @p1217 :rule cong :premises (@p719 @p1216) :args (@t534)) % 5.77/6.09 (step @p1218 :rule cong :premises (@p19 @p734) :args (@t456)) % 5.77/6.09 (step @p1219 :rule cong :premises (@p734 @p787) :args (@t174)) % 5.77/6.09 (step @p1220 :rule trans :premises (@p1219 @p304 @p1218)) % 5.77/6.09 (step @p1221 :rule cong :premises (@p1220 @p913) :args (@t175)) % 5.77/6.09 (step @p1222 :rule trans :premises (@p278 @p1221 @p355 @p1217 @p1211 @p906 @p905 @p85 @p902 @p28 @p682)) % 5.77/6.09 (step @p1223 :rule cong :premises (@p775 @p1222) :args ((tptp.xor @t60 @t160))) % 5.77/6.09 (step @p1224 :rule refl :args (@t160)) % 5.77/6.09 (step @p1225 :rule cong :premises (@p1018 @p1224) :args (@t431)) % 5.77/6.09 (step @p1226 :rule trans :premises (@p244 @p1225 @p1223)) % 5.77/6.09 (step @p1227 :rule cong :premises (@p1224 @p927) :args ((tptp.xor @t160 @t133))) % 5.77/6.09 (step @p1228 :rule symm :premises (@p305)) % 5.77/6.09 (step @p1229 :rule symm :premises (@p116)) % 5.77/6.09 (step @p1230 :rule cong :premises (@p665 @p1229) :args (@t396)) % 5.77/6.09 (step @p1231 :rule cong :premises (@p1130 @p717) :args (@t394)) % 5.77/6.09 (step @p1232 :rule symm :premises (@p185)) % 5.77/6.09 (step @p1233 :rule cong :premises (@p1206 @p19) :args (@t114)) % 5.77/6.09 (step @p1234 :rule cong :premises (@p665 @p1233) :args (@t363)) % 5.77/6.09 (step @p1235 :rule trans :premises (@p170 @p1234 @p1232 @p1231 @p186 @p1230 @p856)) % 5.77/6.09 (step @p1236 :rule cong :premises (@p775 @p1235) :args ((tptp.xor @t60 @t124))) % 5.77/6.09 (step @p1237 :rule refl :args (@t124)) % 5.77/6.09 (step @p1238 :rule cong :premises (@p1018 @p1237) :args (@t636)) % 5.77/6.09 (step @p1239 :rule trans :premises (@p1238 @p1236 @p1153 @p1152 @p1151 @p1150)) % 5.77/6.09 (step @p1240 :rule cong :premises (@p1239 @p895) :args ((tptp.and_star @t636 @t588))) % 5.77/6.09 (step @p1241 :rule refl :args (@t636)) % 5.77/6.09 (step @p1242 :rule cong :premises (@p1241 @p1028) :args ((tptp.and_star @t636 @t212))) % 5.77/6.09 (step @p1243 :rule symm :premises (@p1239)) % 5.77/6.09 (step @p1244 :rule trans :premises (@p1154 @p1243)) % 5.77/6.09 (step @p1245 :rule cong :premises (@p1244 @p827) :args (@t637)) % 5.77/6.09 (step @p1246 :rule trans :premises (@p1245 @p1242 @p1240 @p1228)) % 5.77/6.09 (step @p1247 :rule cong :premises (@p1246 @p929) :args (@t638)) % 5.77/6.09 (step @p1248 :rule trans :premises (@p1247 @p1227)) % 5.77/6.09 (step @p1249 :rule trans :premises (@p1248 @p1226 @p901)) % 5.77/6.09 (step @p1250 :rule cong :premises (@p1249 @p897) :args ((tptp.and_star @t638 @t212))) % 5.77/6.09 (step @p1251 :rule symm :premises (@p897)) % 5.77/6.09 (step @p1252 :rule symm :premises (@p1248)) % 5.77/6.09 (step @p1253 :rule cong :premises (@p1154 @p734) :args (@t515)) % 5.77/6.09 (step @p1254 :rule trans :premises (@p1253 @p1228)) % 5.77/6.09 (step @p1255 :rule cong :premises (@p1254 @p929) :args (@t516)) % 5.77/6.09 (step @p1256 :rule trans :premises (@p1255 @p1227)) % 5.77/6.09 (step @p1257 :rule trans :premises (@p1256 @p1252)) % 5.77/6.10 (step @p1258 :rule cong :premises (@p1257 @p1251) :args (@t517)) % 5.77/6.10 (step @p1259 :rule symm :premises (@p337)) % 5.77/6.10 (step @p1260 :rule symm :premises (@p443)) % 5.77/6.10 (step @p1261 :rule trans :premises (@p1260 @p1259 @p1258 @p1250 @p385 @p896 @p895)) % 5.77/6.10 (step @p1262 :rule cong :premises (@p1261 @p894) :args ((tptp.and_star @t610 @t439))) % 5.77/6.10 (step @p58 :rule instantiate :premises (@p1) :args (@t55)) % 5.77/6.10 (step @p1263 :rule symm :premises (@p1097)) % 5.77/6.10 (step @p1264 :rule trans :premises (@p136 @p1263 @p58 @p668 @p664 @p663)) % 5.77/6.10 (step @p1265 :rule cong :premises (@p735 @p1264) :args ((tptp.and_star tptp.b @t98))) % 5.77/6.10 (step @p1266 :rule symm :premises (@p1264)) % 5.77/6.10 (step @p1267 :rule symm :premises (@p315)) % 5.77/6.10 (step @p1268 :rule trans :premises (@p1267 @p164 @p944)) % 5.77/6.10 (step @p1269 :rule cong :premises (@p1268 @p929) :args ((tptp.and_star @t475 tptp.truth))) % 5.77/6.10 (step @p1270 :rule symm :premises (@p1268)) % 5.77/6.10 (step @p1271 :rule symm :premises (@p936)) % 5.77/6.10 (step @p1272 :rule trans :premises (@p1271 @p1270)) % 5.77/6.10 (step @p1273 :rule cong :premises (@p1272 @p665) :args ((tptp.and_star tptp.b tptp.truth))) % 5.77/6.10 (step @p1274 :rule symm :premises (@p416)) % 5.77/6.10 (step @p1275 :rule cong :premises (@p873 @p755) :args ((tptp.and_star @t199 @t58))) % 5.77/6.10 (step @p1276 :rule trans :premises (@p683 @p12 @p30 @p99 @p761 @p172 @p760 @p759 @p109 @p758)) % 5.77/6.10 (step @p1277 :rule cong :premises (@p873 @p1276) :args ((tptp.and_star @t199 @t87))) % 5.77/6.10 (step @p1278 :rule trans :premises (@p825 @p824 @p15 @p17)) % 5.77/6.10 (step @p1279 :rule cong :premises (@p1040 @p1278) :args (@t599)) % 5.77/6.10 (step @p1280 :rule cong :premises (@p1111 @p740) :args (@t221)) % 5.77/6.10 (step @p1281 :rule trans :premises (@p1280 @p382)) % 5.77/6.10 (step @p1282 :rule cong :premises (@p1281 @p674) :args (@t222)) % 5.77/6.10 (step @p1283 :rule symm :premises (@p954)) % 5.77/6.10 (step @p1284 :rule trans :premises (@p1013 @p1283)) % 5.77/6.10 (step @p1285 :rule cong :premises (@p1284 @p913) :args ((tptp.and_star @t477 @t33))) % 5.77/6.10 (step @p1286 :rule symm :premises (@p1013)) % 5.77/6.10 (step @p1287 :rule trans :premises (@p1271 @p1286)) % 5.77/6.10 (step @p1288 :rule cong :premises (@p1287 @p1130) :args ((tptp.and_star tptp.b @t113))) % 5.77/6.10 (step @p1289 :rule symm :premises (@p1163)) % 5.77/6.10 (step @p1290 :rule cong :premises (@p735 @p1289) :args (@t570)) % 5.77/6.10 (step @p1291 :rule symm :premises (@p1198)) % 5.77/6.10 (step @p1292 :rule trans :premises (@p1291 @p1163)) % 5.77/6.10 (step @p1293 :rule cong :premises (@p1292 @p735) :args ((tptp.and_star @t470 tptp.b))) % 5.77/6.10 (step @p1294 :rule symm :premises (@p1292)) % 5.77/6.10 (step @p1295 :rule cong :premises (@p1294 @p1111) :args (@t639)) % 5.77/6.10 (step @p1296 :rule trans :premises (@p1295 @p1293 @p386 @p1290 @p1288 @p1285 @p376 @p1282 @p438 @p1279 @p1277 @p1275 @p1274 @p28 @p682)) % 5.77/6.10 (step @p1297 :rule cong :premises (@p665 @p1296) :args ((tptp.xor tptp.truth @t639))) % 5.77/6.10 (step @p1298 :rule symm :premises (@p1295)) % 5.77/6.10 (step @p1299 :rule symm :premises (@p1293)) % 5.77/6.10 (step @p1300 :rule symm :premises (@p386)) % 5.77/6.10 (step @p1301 :rule symm :premises (@p1290)) % 5.77/6.10 (step @p1302 :rule symm :premises (@p1288)) % 5.77/6.10 (step @p1303 :rule symm :premises (@p1285)) % 5.77/6.10 (step @p1304 :rule trans :premises (@p1303 @p1302 @p1301 @p1300 @p1299 @p1298)) % 5.77/6.10 (step @p1305 :rule cong :premises (@p665 @p1304) :args ((tptp.xor tptp.truth @t223))) % 5.77/6.10 (step @p1306 :rule trans :premises (@p386 @p1290 @p1288 @p1285)) % 5.77/6.10 (step @p1307 :rule cong :premises (@p665 @p1306) :args (@t523)) % 5.77/6.10 (step @p1308 :rule trans :premises (@p350 @p1307 @p1305 @p1297 @p680 @p675)) % 5.77/6.10 (step @p1309 :rule cong :premises (@p1015 @p1308) :args ((tptp.and_star @t560 @t228))) % 5.77/6.10 (step @p1310 :rule refl :args (@t228)) % 5.77/6.10 (step @p1311 :rule cong :premises (@p1033 @p1310) :args (@t576)) % 5.77/6.10 (step @p1312 :rule refl :args (@t202)) % 5.77/6.10 (step @p1313 :rule cong :premises (@p1312 @p1182) :args (@t603)) % 5.77/6.10 (step @p1314 :rule trans :premises (@p440 @p1313 @p234 @p389 @p1311 @p1309 @p1273 @p1269 @p953 @p944)) % 5.77/6.10 (step @p1315 :rule trans :premises (@p1314 @p936)) % 5.77/6.10 (step @p1316 :rule cong :premises (@p1315 @p1266) :args (@t616)) % 5.77/6.10 (step @p1317 :rule symm :premises (@p446)) % 5.77/6.10 (step @p1318 :rule cong :premises (@p856 @p891) :args (@t463)) % 5.77/6.10 (step @p1319 :rule symm :premises (@p308)) % 5.77/6.10 (step @p1320 :rule cong :premises (@p891 @p79) :args (@t613)) % 5.77/6.10 (step @p1321 :rule trans :premises (@p1320 @p1319 @p1318)) % 5.77/6.10 (step @p1322 :rule trans :premises (@p1082 @p1081 @p414)) % 5.77/6.10 (step @p343 :rule instantiate :premises (@p9) :args (@t204)) % 5.77/6.10 (step @p285 :rule instantiate :premises (@p11) :args (@t181)) % 5.77/6.10 (step @p1323 :rule cong :premises (@p665 @p285) :args ((tptp.xor tptp.truth @t178))) % 5.77/6.10 (step @p1324 :rule trans :premises (@p1176 @p1161 @p1160 @p921 @p916 @p777 @p767 @p18)) % 5.77/6.10 (step @p1325 :rule cong :premises (@p674 @p1324) :args (@t549)) % 5.77/6.10 (step @p1326 :rule refl :args (@t550)) % 5.77/6.10 (step @p1327 :rule cong :premises (@p1326 @p856) :args (@t640)) % 5.77/6.10 (step @p1328 :rule trans :premises (@p1327 @p378 @p1325 @p290)) % 5.77/6.10 (step @p1329 :rule cong :premises (@p665 @p1328) :args ((tptp.xor tptp.truth @t640))) % 5.77/6.10 (step @p1330 :rule symm :premises (@p1327)) % 5.77/6.10 (step @p1331 :rule symm :premises (@p378)) % 5.77/6.10 (step @p1332 :rule symm :premises (@p1325)) % 5.77/6.10 (step @p1333 :rule symm :premises (@p741)) % 5.77/6.10 (step @p1334 :rule symm :premises (@p322)) % 5.77/6.10 (step @p1335 :rule symm :premises (@p914)) % 5.77/6.10 (step @p1336 :rule trans :premises (@p222 @p1335 @p1334)) % 5.77/6.10 (step @p1337 :rule cong :premises (@p871 @p674) :args (@t591)) % 5.77/6.10 (step @p1338 :rule trans :premises (@p1337 @p322 @p914 @p217)) % 5.77/6.10 (step @p1339 :rule trans :premises (@p1338 @p1336 @p41)) % 5.77/6.10 (step @p1340 :rule cong :premises (@p1339 @p665) :args (@t592)) % 5.77/6.10 (step @p1341 :rule trans :premises (@p1340 @p1333 @p910 @p666)) % 5.77/6.10 (step @p1342 :rule trans :premises (@p1341 @p18)) % 5.77/6.10 (step @p1343 :rule cong :premises (@p1342 @p674) :args (@t593)) % 5.77/6.10 (step @p1344 :rule symm :premises (@p1111)) % 5.77/6.10 (step @p1345 :rule cong :premises (@p1344 @p734) :args (@t36)) % 5.77/6.10 (step @p1346 :rule symm :premises (@p141)) % 5.77/6.10 (step @p1347 :rule symm :premises (@p716)) % 5.77/6.10 (step @p1348 :rule symm :premises (@p74)) % 5.77/6.10 (step @p1349 :rule symm :premises (@p713)) % 5.77/6.10 (step @p1350 :rule symm :premises (@p1104)) % 5.77/6.10 (step @p1351 :rule symm :premises (@p1083)) % 5.77/6.10 (step @p1352 :rule cong :premises (@p1351 @p891) :args (@t156)) % 5.77/6.10 (step @p1353 :rule trans :premises (@p1352 @p77 @p1350)) % 5.77/6.10 (step @p1354 :rule cong :premises (@p665 @p1353) :args (@t420)) % 5.77/6.10 (step @p1355 :rule trans :premises (@p237 @p1354 @p1106 @p1045 @p36 @p1349 @p1348 @p1347 @p1346 @p1345)) % 5.77/6.10 (step @p1356 :rule symm :premises (@p237)) % 5.77/6.10 (step @p1357 :rule symm :premises (@p1354)) % 5.77/6.10 (step @p1358 :rule cong :premises (@p775 @p740) :args (@t338)) % 5.77/6.10 (step @p1359 :rule cong :premises (@p1276 @p734) :args (@t407)) % 5.77/6.10 (step @p1360 :rule trans :premises (@p213 @p1359 @p160 @p1358)) % 5.77/6.10 (step @p1361 :rule cong :premises (@p1360 @p735) :args ((tptp.and_star @t408 tptp.b))) % 5.77/6.10 (step @p1362 :rule trans :premises (@p1361 @p736 @p141 @p716 @p74 @p713 @p710 @p1109 @p1108 @p1357 @p1356)) % 5.77/6.10 (step @p1363 :rule symm :premises (@p1361)) % 5.77/6.10 (step @p1364 :rule trans :premises (@p36 @p1349 @p1348 @p1347 @p1346 @p42 @p1363)) % 5.77/6.10 (step @p1365 :rule trans :premises (@p736 @p717 @p1364 @p1362 @p1355)) % 5.77/6.10 (step @p1366 :rule cong :premises (@p1365 @p665) :args (@t116)) % 5.77/6.10 (step @p1367 :rule symm :premises (@p737)) % 5.77/6.10 (step @p49 :rule instantiate :premises (@p1) :args (@t37)) % 5.77/6.10 (step @p1368 :rule symm :premises (@p718)) % 5.77/6.10 (step @p1369 :rule symm :premises (@p1082)) % 5.77/6.10 (step @p1370 :rule symm :premises (@p836)) % 5.77/6.10 (step @p1371 :rule trans :premises (@p1370 @p1369)) % 5.77/6.10 (step @p1372 :rule cong :premises (@p891 @p1371) :args ((tptp.and_star @t26 @t90))) % 5.77/6.10 (step @p1373 :rule trans :premises (@p1372 @p1101 @p1080 @p163 @p314 @p1078 @p1076 @p1061 @p1054 @p1053 @p1050 @p204 @p1048 @p1368 @p49 @p1367 @p1366)) % 5.77/6.10 (step @p1374 :rule trans :premises (@p1372 @p1101 @p1080 @p163 @p314 @p1078 @p1076 @p1061 @p1054 @p1053 @p1050 @p204 @p1048 @p122 @p709)) % 5.77/6.10 (step @p1375 :rule symm :premises (@p1374)) % 5.77/6.10 (step @p1376 :rule trans :premises (@p677 @p765 @p1375 @p1373)) % 5.77/6.10 (step @p1377 :rule cong :premises (@p1376 @p734) :args (@t535)) % 5.77/6.10 (step @p1378 :rule trans :premises (@p304 @p1218 @p1377 @p426 @p1343 @p285 @p1332 @p1331 @p1330)) % 5.77/6.10 (step @p1379 :rule cong :premises (@p665 @p1378) :args (@t437)) % 5.77/6.10 (step @p1380 :rule trans :premises (@p248 @p1379 @p1329 @p1323)) % 5.77/6.10 (step @p1381 :rule trans :premises (@p1380 @p343)) % 5.77/6.10 (step @p1382 :rule cong :premises (@p1381 @p1322) :args (@t254)) % 5.77/6.10 (step @p1383 :rule cong :premises (@p1382 @p1321) :args (@t614)) % 5.77/6.10 (step @p1384 :rule symm :premises (@p439)) % 5.77/6.10 (step @p1385 :rule symm :premises (@p179)) % 5.77/6.10 (step @p1386 :rule symm :premises (@p1101)) % 5.77/6.10 (step @p1387 :rule symm :premises (@p1080)) % 5.77/6.10 (step @p1388 :rule symm :premises (@p163)) % 5.77/6.10 (step @p1389 :rule symm :premises (@p314)) % 5.77/6.10 (step @p1390 :rule symm :premises (@p1078)) % 5.77/6.10 (step @p1391 :rule symm :premises (@p1076)) % 5.77/6.10 (step @p1392 :rule symm :premises (@p1061)) % 5.77/6.10 (step @p1393 :rule trans :premises (@p38 @p54 @p718 @p1058 @p199 @p1056 @p1055 @p325 @p1392 @p1391 @p1390 @p1389 @p1388 @p1387 @p1386 @p1385)) % 5.77/6.10 (step @p1394 :rule refl :args (@t250)) % 5.77/6.10 (step @p1395 :rule cong :premises (@p1394 @p1393) :args ((tptp.and_star @t250 @t73))) % 5.77/6.10 (step @p1396 :rule cong :premises (@p1394 @p19) :args (@t354)) % 5.77/6.10 (step @p1397 :rule symm :premises (@p165)) % 5.77/6.10 (step @p1398 :rule symm :premises (@p317)) % 5.77/6.10 (step @p1399 :rule symm :premises (@p247)) % 5.77/6.10 (step @p1400 :rule symm :premises (@p306)) % 5.77/6.10 (step @p1401 :rule cong :premises (@p665 @p1400) :args (@t583)) % 5.77/6.10 (step @p1402 :rule refl :args (@t24)) % 5.77/6.10 (step @p1403 :rule cong :premises (@p871 @p1402) :args (@t581)) % 5.77/6.10 (step @p1404 :rule symm :premises (@p392)) % 5.77/6.10 (step @p1405 :rule cong :premises (@p873 @p717) :args (@t574)) % 5.77/6.10 (step @p1406 :rule cong :premises (@p665 @p1405) :args ((tptp.xor tptp.truth @t574))) % 5.77/6.10 (step @p1407 :rule symm :premises (@p1037)) % 5.77/6.10 (step @p1408 :rule symm :premises (@p1035)) % 5.77/6.10 (step @p1409 :rule symm :premises (@p381)) % 5.77/6.10 (step @p1410 :rule symm :premises (@p1014)) % 5.77/6.10 (step @p1411 :rule trans :premises (@p240 @p938 @p937 @p212 @p316 @p1410 @p1409)) % 5.77/6.10 (step @p1412 :rule cong :premises (@p1034 @p1411) :args (@t641)) % 5.77/6.10 (step @p1413 :rule trans :premises (@p1412 @p1408 @p377 @p1407)) % 5.77/6.10 (step @p1414 :rule cong :premises (@p665 @p1413) :args ((tptp.xor tptp.truth @t641))) % 5.77/6.10 (step @p1415 :rule symm :premises (@p1412)) % 5.77/6.10 (step @p1416 :rule symm :premises (@p1032)) % 5.77/6.10 (step @p1417 :rule symm :premises (@p1012)) % 5.77/6.10 (step @p1418 :rule symm :premises (@p280)) % 5.77/6.10 (step @p1419 :rule trans :premises (@p678 @p676 @p331 @p823 @p1418 @p1417 @p1416 @p1415)) % 5.77/6.10 (step @p1420 :rule cong :premises (@p665 @p1419) :args (@t619)) % 5.77/6.10 (step @p1421 :rule trans :premises (@p169 @p725 @p722 @p1420 @p1414 @p1406 @p1404 @p1403 @p393 @p1401 @p1399)) % 5.77/6.10 (step @p1422 :rule cong :premises (@p740 @p1421) :args (@t566)) % 5.77/6.10 (step @p1423 :rule trans :premises (@p384 @p1422 @p1398 @p1397 @p1396 @p1395 @p1384)) % 5.77/6.10 (step @p1424 :rule symm :premises (@p384)) % 5.77/6.10 (step @p1425 :rule symm :premises (@p169)) % 5.77/6.10 (step @p1426 :rule symm :premises (@p725)) % 5.77/6.10 (step @p1427 :rule symm :premises (@p722)) % 5.77/6.10 (step @p1428 :rule symm :premises (@p680)) % 5.77/6.10 (step @p1429 :rule trans :premises (@p140 @p1428 @p1427 @p1426 @p1425)) % 5.77/6.10 (step @p1430 :rule cong :premises (@p740 @p1429) :args (@t252)) % 5.77/6.10 (step @p1431 :rule trans :premises (@p224 @p338 @p870 @p869 @p413 @p1430 @p1424)) % 5.77/6.10 (step @p1432 :rule trans :premises (@p1040 @p1431 @p1423)) % 5.77/6.10 (step @p1433 :rule cong :premises (@p1432 @p1162) :args (@t386)) % 5.77/6.10 (step @p1434 :rule trans :premises (@p181 @p1433 @p445 @p1383 @p1317 @p1316 @p1265)) % 5.77/6.10 (step @p1435 :rule symm :premises (@p1261)) % 5.77/6.10 (step @p1436 :rule cong :premises (@p1435 @p1434) :args ((tptp.and_star @t35 @t81))) % 5.77/6.10 (step @p1437 :rule cong :premises (@p740 @p1179) :args (@t542)) % 5.77/6.10 (step @p1438 :rule trans :premises (@p358 @p1437 @p868)) % 5.77/6.10 (step @p1439 :rule cong :premises (@p734 @p1438) :args (@t606)) % 5.77/6.10 (step @p1440 :rule symm :premises (@p1430)) % 5.77/6.10 (step @p1441 :rule cong :premises (@p1429 @p740) :args (@t642)) % 5.77/6.10 (step @p1442 :rule trans :premises (@p1441 @p384 @p1440)) % 5.77/6.10 (step @p1443 :rule cong :premises (@p734 @p1442) :args ((tptp.and_star @t35 @t642))) % 5.77/6.10 (step @p1444 :rule symm :premises (@p1441)) % 5.77/6.10 (step @p1445 :rule trans :premises (@p224 @p338 @p870 @p869 @p413 @p1430 @p1424 @p1444)) % 5.77/6.10 (step @p1446 :rule cong :premises (@p734 @p1445) :args ((tptp.and_star @t35 @t199))) % 5.77/6.10 (step @p1447 :rule cong :premises (@p1360 @p873) :args (@t497)) % 5.77/6.10 (step @p1448 :rule trans :premises (@p683 @p12 @p332 @p1447 @p1446 @p1443)) % 5.77/6.10 (step @p1449 :rule cong :premises (@p1448 @p1162) :args ((tptp.and_star @t87 @t80))) % 5.77/6.10 (step @p1450 :rule cong :premises (@p1011 @p1235) :args ((tptp.and_star @t480 @t124))) % 5.77/6.10 (step @p1451 :rule trans :premises (@p676 @p15 @p17)) % 5.77/6.10 (step @p1452 :rule trans :premises (@p1451 @p1016)) % 5.77/6.10 (step @p1453 :rule cong :premises (@p1452 @p1237) :args (@t448)) % 5.77/6.10 (step @p1454 :rule symm :premises (@p279)) % 5.77/6.10 (step @p1455 :rule symm :premises (@p178)) % 5.77/6.10 (step @p1456 :rule cong :premises (@p43 @p665) :args (@t283)) % 5.77/6.10 (step @p1457 :rule trans :premises (@p39 @p1456)) % 5.77/6.10 (step @p1458 :rule cong :premises (@p776 @p1457) :args (@t369)) % 5.77/6.10 (step @p1459 :rule trans :premises (@p1458 @p1455 @p76 @p183)) % 5.77/6.10 (step @p1460 :rule cong :premises (@p662 @p1459) :args (@t370)) % 5.77/6.10 (step @p1461 :rule refl :args (@t88)) % 5.77/6.10 (step @p1462 :rule cong :premises (@p43 @p1461) :args (@t309)) % 5.77/6.10 (step @p1463 :rule trans :premises (@p678 @p676 @p31 @p111 @p1462 @p173 @p1460 @p1454 @p1453 @p1450 @p1449 @p441 @p1439 @p1436 @p1262 @p893 @p892 @p890 @p704 @p33 @p108 @p889 @p888)) % 5.77/6.10 (step @p1464 :rule cong :premises (@p665 @p1463) :args (@t619)) % 5.77/6.10 (step @p1465 :rule trans :premises (@p140 @p1428 @p1464 @p887 @p661)) % 5.77/6.10 (step-pop @p1950 :rule scope :premises (@p1465)) % 5.77/6.10 (step-pop @p1951 :rule scope :premises (@p1950)) % 5.77/6.10 (step-pop @p1952 :rule scope :premises (@p1951)) % 5.77/6.10 (step-pop @p1953 :rule scope :premises (@p1952)) % 5.77/6.10 (step-pop @p1954 :rule scope :premises (@p1953)) % 5.77/6.10 (step-pop @p1955 :rule scope :premises (@p1954)) % 5.77/6.10 (step-pop @p1956 :rule scope :premises (@p1955)) % 5.77/6.10 (step-pop @p1957 :rule scope :premises (@p1956)) % 5.77/6.10 (step-pop @p1958 :rule scope :premises (@p1957)) % 5.77/6.10 (step-pop @p1959 :rule scope :premises (@p1958)) % 5.77/6.10 (step-pop @p1960 :rule scope :premises (@p1959)) % 5.77/6.10 (step-pop @p1961 :rule scope :premises (@p1960)) % 5.77/6.10 (step-pop @p1962 :rule scope :premises (@p1961)) % 5.77/6.10 (step-pop @p1963 :rule scope :premises (@p1962)) % 5.77/6.10 (step-pop @p1964 :rule scope :premises (@p1963)) % 5.77/6.10 (step-pop @p1965 :rule scope :premises (@p1964)) % 5.77/6.10 (step-pop @p1966 :rule scope :premises (@p1965)) % 5.77/6.10 (step-pop @p1967 :rule scope :premises (@p1966)) % 5.77/6.10 (step-pop @p1968 :rule scope :premises (@p1967)) % 5.77/6.10 (step-pop @p1969 :rule scope :premises (@p1968)) % 5.77/6.10 (step-pop @p1970 :rule scope :premises (@p1969)) % 5.77/6.10 (step-pop @p1971 :rule scope :premises (@p1970)) % 5.77/6.10 (step-pop @p1972 :rule scope :premises (@p1971)) % 5.77/6.10 (step-pop @p1973 :rule scope :premises (@p1972)) % 5.77/6.10 (step-pop @p1974 :rule scope :premises (@p1973)) % 5.77/6.10 (step-pop @p1975 :rule scope :premises (@p1974)) % 5.77/6.10 (step-pop @p1976 :rule scope :premises (@p1975)) % 5.77/6.10 (step-pop @p1977 :rule scope :premises (@p1976)) % 5.77/6.10 (step-pop @p1978 :rule scope :premises (@p1977)) % 5.77/6.10 (step-pop @p1979 :rule scope :premises (@p1978)) % 5.77/6.10 (step-pop @p1980 :rule scope :premises (@p1979)) % 5.77/6.10 (step-pop @p1981 :rule scope :premises (@p1980)) % 5.77/6.10 (step-pop @p1982 :rule scope :premises (@p1981)) % 5.77/6.10 (step-pop @p1983 :rule scope :premises (@p1982)) % 5.77/6.10 (step-pop @p1984 :rule scope :premises (@p1983)) % 5.77/6.10 (step-pop @p1985 :rule scope :premises (@p1984)) % 5.77/6.10 (step-pop @p1986 :rule scope :premises (@p1985)) % 5.77/6.10 (step-pop @p1987 :rule scope :premises (@p1986)) % 5.77/6.10 (step-pop @p1988 :rule scope :premises (@p1987)) % 5.77/6.10 (step-pop @p1989 :rule scope :premises (@p1988)) % 5.77/6.10 (step-pop @p1990 :rule scope :premises (@p1989)) % 5.77/6.10 (step-pop @p1991 :rule scope :premises (@p1990)) % 5.77/6.10 (step-pop @p1992 :rule scope :premises (@p1991)) % 5.77/6.10 (step-pop @p1993 :rule scope :premises (@p1992)) % 5.77/6.10 (step-pop @p1994 :rule scope :premises (@p1993)) % 5.77/6.10 (step-pop @p1995 :rule scope :premises (@p1994)) % 5.77/6.10 (step-pop @p1996 :rule scope :premises (@p1995)) % 5.77/6.10 (step-pop @p1997 :rule scope :premises (@p1996)) % 5.77/6.10 (step-pop @p1998 :rule scope :premises (@p1997)) % 5.77/6.10 (step-pop @p1999 :rule scope :premises (@p1998)) % 5.77/6.10 (step-pop @p2000 :rule scope :premises (@p1999)) % 5.77/6.10 (step-pop @p2001 :rule scope :premises (@p2000)) % 5.77/6.10 (step-pop @p2002 :rule scope :premises (@p2001)) % 5.77/6.10 (step-pop @p2003 :rule scope :premises (@p2002)) % 5.77/6.10 (step-pop @p2004 :rule scope :premises (@p2003)) % 5.77/6.10 (step-pop @p2005 :rule scope :premises (@p2004)) % 5.77/6.10 (step-pop @p2006 :rule scope :premises (@p2005)) % 5.77/6.10 (step-pop @p2007 :rule scope :premises (@p2006)) % 5.77/6.10 (step-pop @p2008 :rule scope :premises (@p2007)) % 5.77/6.10 (step-pop @p2009 :rule scope :premises (@p2008)) % 5.77/6.10 (step-pop @p2010 :rule scope :premises (@p2009)) % 5.77/6.10 (step-pop @p2011 :rule scope :premises (@p2010)) % 5.77/6.10 (step-pop @p2012 :rule scope :premises (@p2011)) % 5.77/6.10 (step-pop @p2013 :rule scope :premises (@p2012)) % 5.77/6.10 (step-pop @p2014 :rule scope :premises (@p2013)) % 5.77/6.10 (step-pop @p2015 :rule scope :premises (@p2014)) % 5.77/6.10 (step-pop @p2016 :rule scope :premises (@p2015)) % 5.77/6.10 (step-pop @p2017 :rule scope :premises (@p2016)) % 5.77/6.10 (step-pop @p2018 :rule scope :premises (@p2017)) % 5.77/6.10 (step-pop @p2019 :rule scope :premises (@p2018)) % 5.77/6.10 (step-pop @p2020 :rule scope :premises (@p2019)) % 5.77/6.10 (step-pop @p2021 :rule scope :premises (@p2020)) % 5.77/6.10 (step-pop @p2022 :rule scope :premises (@p2021)) % 5.77/6.10 (step-pop @p2023 :rule scope :premises (@p2022)) % 5.77/6.10 (step-pop @p2024 :rule scope :premises (@p2023)) % 5.77/6.10 (step-pop @p2025 :rule scope :premises (@p2024)) % 5.77/6.10 (step-pop @p2026 :rule scope :premises (@p2025)) % 5.77/6.10 (step-pop @p2027 :rule scope :premises (@p2026)) % 5.77/6.10 (step-pop @p2028 :rule scope :premises (@p2027)) % 5.77/6.10 (step-pop @p2029 :rule scope :premises (@p2028)) % 5.77/6.10 (step-pop @p2030 :rule scope :premises (@p2029)) % 5.77/6.10 (step-pop @p2031 :rule scope :premises (@p2030)) % 5.77/6.10 (step-pop @p2032 :rule scope :premises (@p2031)) % 5.77/6.10 (step-pop @p2033 :rule scope :premises (@p2032)) % 5.77/6.10 (step-pop @p2034 :rule scope :premises (@p2033)) % 5.77/6.10 (step-pop @p2035 :rule scope :premises (@p2034)) % 5.77/6.10 (step-pop @p2036 :rule scope :premises (@p2035)) % 5.77/6.10 (step-pop @p2037 :rule scope :premises (@p2036)) % 5.77/6.10 (step-pop @p2038 :rule scope :premises (@p2037)) % 5.77/6.10 (step-pop @p2039 :rule scope :premises (@p2038)) % 5.77/6.10 (step-pop @p2040 :rule scope :premises (@p2039)) % 5.77/6.10 (step-pop @p2041 :rule scope :premises (@p2040)) % 5.77/6.10 (step-pop @p2042 :rule scope :premises (@p2041)) % 5.77/6.10 (step-pop @p2043 :rule scope :premises (@p2042)) % 5.77/6.10 (step-pop @p2044 :rule scope :premises (@p2043)) % 5.77/6.10 (step-pop @p2045 :rule scope :premises (@p2044)) % 5.77/6.10 (step-pop @p2046 :rule scope :premises (@p2045)) % 5.77/6.10 (step-pop @p2047 :rule scope :premises (@p2046)) % 5.77/6.10 (step-pop @p2048 :rule scope :premises (@p2047)) % 5.77/6.10 (step-pop @p2049 :rule scope :premises (@p2048)) % 5.77/6.10 (step-pop @p2050 :rule scope :premises (@p2049)) % 5.77/6.10 (step-pop @p2051 :rule scope :premises (@p2050)) % 5.77/6.10 (step-pop @p2052 :rule scope :premises (@p2051)) % 5.77/6.10 (step-pop @p2053 :rule scope :premises (@p2052)) % 5.77/6.10 (step-pop @p2054 :rule scope :premises (@p2053)) % 5.77/6.10 (step-pop @p2055 :rule scope :premises (@p2054)) % 5.77/6.10 (step-pop @p2056 :rule scope :premises (@p2055)) % 5.77/6.10 (step-pop @p2057 :rule scope :premises (@p2056)) % 5.77/6.10 (step-pop @p2058 :rule scope :premises (@p2057)) % 5.77/6.10 (step-pop @p2059 :rule scope :premises (@p2058)) % 5.77/6.10 (step-pop @p2060 :rule scope :premises (@p2059)) % 5.77/6.10 (step-pop @p2061 :rule scope :premises (@p2060)) % 5.77/6.10 (step-pop @p2062 :rule scope :premises (@p2061)) % 5.77/6.10 (step-pop @p2063 :rule scope :premises (@p2062)) % 5.77/6.10 (step-pop @p2064 :rule scope :premises (@p2063)) % 5.77/6.10 (step-pop @p2065 :rule scope :premises (@p2064)) % 5.77/6.10 (step-pop @p2066 :rule scope :premises (@p2065)) % 5.77/6.10 (step-pop @p2067 :rule scope :premises (@p2066)) % 5.77/6.10 (step-pop @p2068 :rule scope :premises (@p2067)) % 5.77/6.10 (step-pop @p2069 :rule scope :premises (@p2068)) % 5.77/6.10 (step-pop @p2070 :rule scope :premises (@p2069)) % 5.77/6.10 (step-pop @p2071 :rule scope :premises (@p2070)) % 5.77/6.10 (step-pop @p2072 :rule scope :premises (@p2071)) % 5.77/6.10 (step-pop @p2073 :rule scope :premises (@p2072)) % 5.77/6.10 (step-pop @p2074 :rule scope :premises (@p2073)) % 5.77/6.10 (step-pop @p2075 :rule scope :premises (@p2074)) % 5.77/6.10 (step-pop @p2076 :rule scope :premises (@p2075)) % 5.77/6.10 (step-pop @p2077 :rule scope :premises (@p2076)) % 5.77/6.10 (step-pop @p2078 :rule scope :premises (@p2077)) % 5.77/6.10 (step-pop @p2079 :rule scope :premises (@p2078)) % 5.77/6.10 (step-pop @p2080 :rule scope :premises (@p2079)) % 5.77/6.10 (step-pop @p2081 :rule scope :premises (@p2080)) % 5.77/6.10 (step-pop @p2082 :rule scope :premises (@p2081)) % 5.77/6.10 (step-pop @p2083 :rule scope :premises (@p2082)) % 5.77/6.10 (step-pop @p2084 :rule scope :premises (@p2083)) % 5.77/6.10 (step-pop @p2085 :rule scope :premises (@p2084)) % 5.77/6.10 (step-pop @p2086 :rule scope :premises (@p2085)) % 5.77/6.10 (step-pop @p2087 :rule scope :premises (@p2086)) % 5.77/6.10 (step-pop @p2088 :rule scope :premises (@p2087)) % 5.77/6.10 (step-pop @p2089 :rule scope :premises (@p2088)) % 5.77/6.10 (step-pop @p2090 :rule scope :premises (@p2089)) % 5.77/6.10 (step-pop @p2091 :rule scope :premises (@p2090)) % 5.77/6.10 (step-pop @p2092 :rule scope :premises (@p2091)) % 5.77/6.10 (step-pop @p2093 :rule scope :premises (@p2092)) % 5.77/6.10 (step-pop @p2094 :rule scope :premises (@p2093)) % 5.77/6.10 (step-pop @p2095 :rule scope :premises (@p2094)) % 5.77/6.10 (step-pop @p2096 :rule scope :premises (@p2095)) % 5.77/6.10 (step-pop @p2097 :rule scope :premises (@p2096)) % 5.77/6.10 (step-pop @p2098 :rule scope :premises (@p2097)) % 5.77/6.10 (step-pop @p2099 :rule scope :premises (@p2098)) % 5.77/6.10 (step-pop @p2100 :rule scope :premises (@p2099)) % 5.77/6.10 (step-pop @p2101 :rule scope :premises (@p2100)) % 5.77/6.10 (step-pop @p2102 :rule scope :premises (@p2101)) % 5.77/6.10 (step-pop @p2103 :rule scope :premises (@p2102)) % 5.77/6.10 (step-pop @p2104 :rule scope :premises (@p2103)) % 5.77/6.10 (step-pop @p2105 :rule scope :premises (@p2104)) % 5.77/6.10 (step-pop @p2106 :rule scope :premises (@p2105)) % 5.77/6.10 (step-pop @p2107 :rule scope :premises (@p2106)) % 5.77/6.10 (step-pop @p2108 :rule scope :premises (@p2107)) % 5.77/6.10 (step-pop @p2109 :rule scope :premises (@p2108)) % 5.77/6.10 (step-pop @p2110 :rule scope :premises (@p2109)) % 5.77/6.10 (step-pop @p2111 :rule scope :premises (@p2110)) % 5.77/6.10 (step-pop @p2112 :rule scope :premises (@p2111)) % 5.77/6.10 (step-pop @p2113 :rule scope :premises (@p2112)) % 5.77/6.10 (step-pop @p2114 :rule scope :premises (@p2113)) % 5.77/6.10 (step-pop @p2115 :rule scope :premises (@p2114)) % 5.77/6.10 (step-pop @p2116 :rule scope :premises (@p2115)) % 5.77/6.10 (step-pop @p2117 :rule scope :premises (@p2116)) % 5.77/6.10 (step-pop @p2118 :rule scope :premises (@p2117)) % 5.77/6.10 (step-pop @p2119 :rule scope :premises (@p2118)) % 5.77/6.10 (step-pop @p2120 :rule scope :premises (@p2119)) % 5.77/6.10 (step-pop @p2121 :rule scope :premises (@p2120)) % 5.77/6.10 (step-pop @p2122 :rule scope :premises (@p2121)) % 5.77/6.10 (step-pop @p2123 :rule scope :premises (@p2122)) % 5.77/6.10 (step-pop @p2124 :rule scope :premises (@p2123)) % 5.77/6.10 (step-pop @p2125 :rule scope :premises (@p2124)) % 5.77/6.10 (step-pop @p2126 :rule scope :premises (@p2125)) % 5.77/6.10 (step-pop @p2127 :rule scope :premises (@p2126)) % 5.77/6.10 (step-pop @p2128 :rule scope :premises (@p2127)) % 5.77/6.10 (step-pop @p2129 :rule scope :premises (@p2128)) % 5.77/6.10 (step-pop @p2130 :rule scope :premises (@p2129)) % 5.77/6.10 (step-pop @p2131 :rule scope :premises (@p2130)) % 5.77/6.10 (step-pop @p2132 :rule scope :premises (@p2131)) % 5.77/6.10 (step-pop @p2133 :rule scope :premises (@p2132)) % 5.77/6.10 (step-pop @p2134 :rule scope :premises (@p2133)) % 5.77/6.10 (step-pop @p2135 :rule scope :premises (@p2134)) % 5.77/6.10 (step-pop @p2136 :rule scope :premises (@p2135)) % 5.77/6.10 (step-pop @p2137 :rule scope :premises (@p2136)) % 5.77/6.10 (step-pop @p2138 :rule scope :premises (@p2137)) % 5.77/6.10 (step-pop @p2139 :rule scope :premises (@p2138)) % 5.77/6.10 (step-pop @p2140 :rule scope :premises (@p2139)) % 5.77/6.10 (step-pop @p2141 :rule scope :premises (@p2140)) % 5.77/6.10 (step-pop @p2142 :rule scope :premises (@p2141)) % 5.77/6.10 (step-pop @p2143 :rule scope :premises (@p2142)) % 5.77/6.10 (step-pop @p2144 :rule scope :premises (@p2143)) % 5.77/6.10 (step-pop @p2145 :rule scope :premises (@p2144)) % 5.77/6.10 (step-pop @p2146 :rule scope :premises (@p2145)) % 5.77/6.10 (step-pop @p2147 :rule scope :premises (@p2146)) % 5.77/6.10 (step-pop @p2148 :rule scope :premises (@p2147)) % 5.77/6.10 (step-pop @p2149 :rule scope :premises (@p2148)) % 5.77/6.10 (step-pop @p2150 :rule scope :premises (@p2149)) % 5.77/6.10 (step-pop @p2151 :rule scope :premises (@p2150)) % 5.77/6.10 (step-pop @p2152 :rule scope :premises (@p2151)) % 5.77/6.10 (step-pop @p2153 :rule scope :premises (@p2152)) % 5.77/6.10 (step-pop @p2154 :rule scope :premises (@p2153)) % 5.77/6.10 (step-pop @p2155 :rule scope :premises (@p2154)) % 5.77/6.10 (step-pop @p2156 :rule scope :premises (@p2155)) % 5.77/6.10 (step-pop @p2157 :rule scope :premises (@p2156)) % 5.77/6.10 (step-pop @p2158 :rule scope :premises (@p2157)) % 5.77/6.10 (step-pop @p2159 :rule scope :premises (@p2158)) % 5.77/6.10 (step-pop @p2160 :rule scope :premises (@p2159)) % 5.77/6.10 (step-pop @p2161 :rule scope :premises (@p2160)) % 5.77/6.10 (step-pop @p2162 :rule scope :premises (@p2161)) % 5.77/6.10 (step-pop @p2163 :rule scope :premises (@p2162)) % 5.77/6.10 (step @p1466 :rule process_scope :premises (@p2163) :args (@t643)) % 5.77/6.10 (step @p1681 :rule implies_elim :premises (@p1466)) % 5.77/6.10 (step @p1682 :rule cnf_and_neg :args (@t644)) % 5.77/6.10 (step @p1683 :rule resolution :premises (@p1682 @p1681) :args (true @t644)) % 5.77/6.10 (step @p1684 :rule reordering :premises (@p1683) :args ((or @t643 (not @t256) (not @t257) (not @t258) (not @t259) (not @t260) (not @t261) (not @t263) (not @t264) (not @t266) (not @t268) (not @t269) (not @t270) (not @t272) (not @t273) (not @t275) (not @t277) (not @t279) (not @t280) (not @t281) (not @t282) (not @t284) (not @t286) (not @t287) (not @t288) (not @t289) (not @t290) (not @t47) (not @t56) (not @t62) (not @t291) (not @t293) (not @t296) (not @t299) (not @t302) (not @t303) (not @t304) (not @t305) (not @t71) (not @t79) (not @t86) (not @t307) (not @t308) (not @t310) (not @t312) (not @t314) (not @t316) (not @t318) (not @t320) (not @t322) (not @t324) (not @t94) (not @t101) (not @t325) (not @t327) (not @t329) (not @t331) (not @t332) (not @t107) (not @t334) (not @t337) (not @t339) (not @t341) (not @t346) (not @t349) (not @t352) (not @t355) (not @t356) (not @t358) (not @t360) (not @t362) (not @t364) (not @t366) (not @t368) (not @t371) (not @t374) (not @t376) (not @t379) (not @t381) (not @t382) (not @t384) (not @t385) (not @t387) (not @t389) (not @t391) (not @t393) (not @t395) (not @t397) (not @t132) (not @t139) (not @t398) (not @t399) (not @t400) (not @t401) (not @t403) (not @t404) (not @t405) (not @t406) (not @t409) (not @t149) (not @t411) (not @t413) (not @t153) (not @t415) (not @t417) (not @t419) (not @t421) (not @t423) (not @t424) (not @t425) (not @t427) (not @t429) (not @t430) (not @t432) (not @t433) (not @t435) (not @t436) (not @t438) (not @t441) (not @t444) (not @t447) (not @t168) (not @t173) (not @t177) (not @t449) (not @t451) (not @t182) (not @t188) (not @t452) (not @t453) (not @t454) (not @t455) (not @t457) (not @t458) (not @t460) (not @t462) (not @t464) (not @t466) (not @t467) (not @t469) (not @t471) (not @t472) (not @t474) (not @t476) (not @t478) (not @t479) (not @t481) (not @t483) (not @t486) (not @t487) (not @t489) (not @t490) (not @t491) (not @t492) (not @t493) (not @t494) (not @t496) (not @t498) (not @t502) (not @t506) (not @t509) (not @t513) (not @t518) (not @t520) (not @t205) (not @t522) (not @t524) (not @t526) (not @t528) (not @t531) (not @t533) (not @t536) (not @t538) (not @t541) (not @t544) (not @t219) (not @t225) (not @t547) (not @t551) (not @t555) (not @t558) (not @t561) (not @t563) (not @t565) (not @t567) (not @t569) (not @t571) (not @t573) (not @t575) (not @t577) (not @t578) (not @t580) (not @t582) (not @t584) (not @t235) (not @t240) (not @t585) (not @t586) (not @t587) (not @t589) (not @t590) (not @t244) (not @t594) (not @t249) (not @t595) (not @t598) (not @t600) (not @t602) (not @t605) (not @t607) (not @t609) (not @t611) (not @t612) (not @t615) (not @t617)))) % 5.77/6.10 (step @p1685 false :rule chain_m_resolution :premises (@p1684 @p446 @p445 @p444 @p443 @p442 @p441 @p440 @p439 @p438 @p437 @p436 @p435 @p426 @p425 @p416 @p415 @p414 @p413 @p412 @p411 @p402 @p393 @p392 @p391 @p390 @p389 @p388 @p387 @p386 @p385 @p384 @p383 @p382 @p381 @p380 @p379 @p378 @p377 @p376 @p367 @p358 @p357 @p356 @p355 @p354 @p353 @p352 @p351 @p350 @p349 @p348 @p338 @p337 @p336 @p335 @p334 @p333 @p332 @p331 @p330 @p329 @p325 @p324 @p323 @p322 @p321 @p320 @p319 @p318 @p317 @p316 @p315 @p314 @p313 @p312 @p311 @p310 @p309 @p308 @p307 @p306 @p305 @p304 @p303 @p302 @p301 @p300 @p299 @p290 @p280 @p279 @p278 @p269 @p260 @p251 @p250 @p249 @p248 @p247 @p246 @p245 @p244 @p243 @p242 @p241 @p240 @p239 @p238 @p237 @p236 @p235 @p234 @p233 @p224 @p223 @p222 @p213 @p212 @p211 @p210 @p209 @p208 @p207 @p206 @p205 @p204 @p195 @p186 @p185 @p184 @p183 @p182 @p181 @p180 @p179 @p178 @p177 @p176 @p175 @p174 @p173 @p172 @p171 @p170 @p169 @p168 @p167 @p166 @p165 @p164 @p163 @p162 @p161 @p160 @p159 @p158 @p157 @p147 @p146 @p145 @p141 @p140 @p136 @p127 @p118 @p117 @p116 @p115 @p114 @p113 @p112 @p111 @p110 @p109 @p108 @p99 @p90 @p80 @p79 @p78 @p77 @p76 @p75 @p74 @p73 @p72 @p63 @p54 @p44 @p43 @p42 @p41 @p40 @p39 @p38 @p37 @p36 @p35 @p34 @p33 @p32 @p31 @p30 @p29 @p28 @p27 @p26 @p25 @p21 @p20 @p19 @p18 @p17 @p16 @p15) :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 false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false 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) (@list @t617 @t615 @t612 @t611 @t609 @t607 @t605 @t602 @t600 @t598 @t595 @t249 @t594 @t244 @t590 @t589 @t587 @t586 @t585 @t240 @t235 @t584 @t582 @t580 @t578 @t577 @t575 @t573 @t571 @t569 @t567 @t565 @t563 @t561 @t558 @t555 @t551 @t547 @t225 @t219 @t544 @t541 @t538 @t536 @t533 @t531 @t528 @t526 @t524 @t522 @t205 @t520 @t518 @t513 @t509 @t506 @t502 @t498 @t496 @t494 @t493 @t492 @t491 @t490 @t489 @t487 @t486 @t483 @t481 @t479 @t478 @t476 @t474 @t472 @t471 @t469 @t467 @t466 @t464 @t462 @t460 @t458 @t457 @t455 @t454 @t453 @t452 @t188 @t182 @t451 @t449 @t177 @t173 @t168 @t447 @t444 @t441 @t438 @t436 @t435 @t433 @t432 @t430 @t429 @t427 @t425 @t424 @t423 @t421 @t419 @t417 @t415 @t153 @t413 @t411 @t149 @t409 @t406 @t405 @t404 @t403 @t401 @t400 @t399 @t398 @t139 @t132 @t397 @t395 @t393 @t391 @t389 @t387 @t385 @t384 @t382 @t381 @t379 @t376 @t374 @t371 @t368 @t366 @t364 @t362 @t360 @t358 @t356 @t355 @t352 @t349 @t346 @t341 @t339 @t337 @t334 @t107 @t332 @t331 @t329 @t327 @t325 @t101 @t94 @t324 @t322 @t320 @t318 @t316 @t314 @t312 @t310 @t308 @t307 @t86 @t79 @t71 @t305 @t304 @t303 @t302 @t299 @t296 @t293 @t291 @t62 @t56 @t47 @t290 @t289 @t288 @t287 @t286 @t284 @t282 @t281 @t280 @t279 @t277 @t275 @t273 @t272 @t270 @t269 @t268 @t266 @t264 @t263 @t261 @t260 @t259 @t258 @t257 @t643 @t256))) % 5.77/6.10 ) % 5.77/6.11 % SZS output end Proof % 5.77/6.11 % cvc5 exiting %------------------------------------------------------------------------------