%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : TOP053-1 : TPTP v9.2.1. Released v8.1.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/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 : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jun 3 09:15:53 AM UTC 2026 % Result : Unsatisfiable 0.61s 0.87s % Output : Proof 0.61s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : TOP053-1 : TPTP v9.2.1. Released v8.1.0. % 0.12/0.14 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.18/0.35 % Computer : n014.cluster.edu % 0.18/0.35 % Model : x86_64 x86_64 % 0.18/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.18/0.35 % Memory : 8042.1875MB % 0.18/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.18/0.35 % CPULimit : 300 % 0.18/0.35 % WCLimit : 300 % 0.18/0.35 % DateTime : Wed Jun 3 01:29:43 EDT 2026 % 0.18/0.35 % CPUTime : % 0.27/0.50 %----Proving TF0_NAR, FOF, or CNF % 0.27/0.52 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 0.61/0.87 % SZS status Unsatisfiable % 0.61/0.87 % SZS output start Proof % 0.61/0.88 ( % 0.61/0.88 (declare-sort $$unsorted 0) % 0.61/0.88 (declare-const tptp.tuple (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.61/0.88 (declare-const tptp.a15 $$unsorted) % 0.61/0.88 (declare-const tptp.a14 $$unsorted) % 0.61/0.88 (declare-const tptp.a13 $$unsorted) % 0.61/0.88 (declare-const tptp.product (-> $$unsorted $$unsorted $$unsorted)) % 0.61/0.88 (declare-const tptp.a3 $$unsorted) % 0.61/0.88 (declare-const tptp.a2 $$unsorted) % 0.61/0.88 (declare-const tptp.a1 $$unsorted) % 0.61/0.88 (declare-const tptp.a8 $$unsorted) % 0.61/0.88 (declare-const tptp.a5 $$unsorted) % 0.61/0.88 (declare-const tptp.a10 $$unsorted) % 0.61/0.88 (declare-const tptp.a4 $$unsorted) % 0.61/0.88 (declare-const tptp.a7 $$unsorted) % 0.61/0.88 (declare-const tptp.a12 $$unsorted) % 0.61/0.88 (declare-const tptp.a6 $$unsorted) % 0.61/0.88 (declare-const tptp.a11 $$unsorted) % 0.61/0.88 (declare-const tptp.a9 $$unsorted) % 0.61/0.88 (define @t1 () (@var "X" $$unsorted)) % 0.61/0.88 (define @t2 () (tptp.product @t1 @t1)) % 0.61/0.88 (define @t3 () (forall (@list @t1) (= @t2 @t1))) % 0.61/0.88 (define @t4 () (@var "Y" $$unsorted)) % 0.61/0.88 (define @t5 () (tptp.product @t1 @t4)) % 0.61/0.88 (define @t6 () (tptp.product @t5 @t4)) % 0.61/0.88 (define @t7 () (forall (@list @t1 @t4) (= @t6 @t1))) % 0.61/0.88 (define @t8 () (@var "Z" $$unsorted)) % 0.61/0.88 (define @t9 () (tptp.product tptp.a1 tptp.a2)) % 0.61/0.88 (define @t10 () (tptp.product tptp.a3 tptp.a4)) % 0.61/0.88 (define @t11 () (tptp.product tptp.a5 tptp.a6)) % 0.61/0.88 (define @t12 () (tptp.product tptp.a7 tptp.a3)) % 0.61/0.88 (define @t13 () (tptp.product tptp.a8 tptp.a2)) % 0.61/0.88 (define @t14 () (tptp.product tptp.a9 tptp.a1)) % 0.61/0.88 (define @t15 () (tptp.product tptp.a10 tptp.a11)) % 0.61/0.88 (define @t16 () (tptp.product tptp.a12 tptp.a3)) % 0.61/0.88 (define @t17 () (tptp.product tptp.a13 tptp.a8)) % 0.61/0.88 (define @t18 () (tptp.product tptp.a6 tptp.a7)) % 0.61/0.88 (define @t19 () (tptp.product tptp.a2 tptp.a12)) % 0.61/0.88 (define @t20 () (tptp.product tptp.a14 tptp.a3)) % 0.61/0.88 (define @t21 () (tptp.product tptp.a15 tptp.a8)) % 0.61/0.88 (define @t22 () (tptp.product tptp.a4 tptp.a7)) % 0.61/0.88 (define @t23 () (tptp.product tptp.a11 tptp.a10)) % 0.61/0.88 (define @t24 () (tptp.tuple tptp.a1 tptp.a2 tptp.a3 tptp.a4 tptp.a5 tptp.a6 tptp.a7 tptp.a8 tptp.a9 tptp.a10 tptp.a11 tptp.a12 tptp.a13 tptp.a14)) % 0.61/0.88 (define @t25 () (= @t24 (tptp.tuple tptp.a2 tptp.a3 tptp.a4 tptp.a5 tptp.a6 tptp.a7 tptp.a8 tptp.a9 tptp.a10 tptp.a11 tptp.a12 tptp.a13 tptp.a14 tptp.a15))) % 0.61/0.88 (define @t26 () (tptp.product tptp.a12 tptp.a7)) % 0.61/0.88 (define @t27 () (tptp.product tptp.a2 tptp.a3)) % 0.61/0.88 (define @t28 () (tptp.product tptp.a14 tptp.a7)) % 0.61/0.88 (define @t29 () (tptp.product tptp.a2 tptp.a1)) % 0.61/0.88 (define @t30 () (tptp.product tptp.a8 tptp.a1)) % 0.61/0.88 (define @t31 () (tptp.product tptp.a10 tptp.a2)) % 0.61/0.88 (define @t32 () (tptp.product tptp.a11 tptp.a2)) % 0.61/0.88 (define @t33 () (tptp.product tptp.a4 tptp.a6)) % 0.61/0.88 (define @t34 () (tptp.product tptp.a3 tptp.a6)) % 0.61/0.88 (define @t35 () (tptp.product tptp.a1 tptp.a11)) % 0.61/0.88 (define @t36 () (tptp.product tptp.a3 tptp.a8)) % 0.61/0.88 (define @t37 () (tptp.product tptp.a8 tptp.a7)) % 0.61/0.88 (define @t38 () (tptp.product tptp.a7 tptp.a12)) % 0.61/0.88 (define @t39 () (tptp.product tptp.a6 tptp.a12)) % 0.61/0.88 (define @t40 () (tptp.product tptp.a7 tptp.a2)) % 0.61/0.88 (define @t41 () (tptp.product @t27 tptp.a8)) % 0.61/0.88 (define @t42 () (tptp.product @t28 @t26)) % 0.61/0.88 (define @t43 () (tptp.product @t31 tptp.a6)) % 0.61/0.88 (define @t44 () (tptp.product @t32 tptp.a6)) % 0.61/0.88 (define @t45 () (tptp.product tptp.a2 @t31)) % 0.61/0.88 (define @t46 () (tptp.product tptp.a11 @t31)) % 0.61/0.88 (define @t47 () (tptp.product tptp.a7 @t37)) % 0.61/0.88 (define @t48 () (tptp.product tptp.a13 @t37)) % 0.61/0.88 (define @t49 () (tptp.product tptp.a15 @t37)) % 0.61/0.88 (define @t50 () (tptp.product @t29 tptp.a2)) % 0.61/0.88 (define @t51 () (tptp.product @t30 tptp.a2)) % 0.61/0.88 (define @t52 () (tptp.product tptp.a6 @t33)) % 0.61/0.88 (define @t53 () (tptp.product tptp.a11 @t35)) % 0.61/0.88 (define @t54 () (tptp.product tptp.a12 @t38)) % 0.61/0.88 (define @t55 () (tptp.product tptp.a8 @t36)) % 0.61/0.88 (define @t56 () (tptp.product @t38 tptp.a7)) % 0.61/0.88 (define @t57 () (tptp.product tptp.a12 @t36)) % 0.61/0.88 (define @t58 () (tptp.product tptp.a14 @t36)) % 0.61/0.88 (define @t59 () (tptp.product tptp.a8 tptp.a3)) % 0.61/0.88 (define @t60 () (tptp.product tptp.a2 tptp.a7)) % 0.61/0.88 (define @t61 () (= tptp.a3 @t9)) % 0.61/0.88 (define @t62 () (= tptp.a5 @t10)) % 0.61/0.88 (define @t63 () (= tptp.a7 @t11)) % 0.61/0.88 (define @t64 () (= tptp.a8 @t12)) % 0.61/0.88 (define @t65 () (= tptp.a9 @t13)) % 0.61/0.88 (define @t66 () (= tptp.a10 @t14)) % 0.61/0.88 (define @t67 () (= tptp.a12 @t15)) % 0.61/0.88 (define @t68 () (= tptp.a13 @t16)) % 0.61/0.88 (define @t69 () (= tptp.a6 @t17)) % 0.61/0.88 (define @t70 () (= tptp.a2 @t18)) % 0.61/0.88 (define @t71 () (= tptp.a14 @t19)) % 0.61/0.88 (define @t72 () (= tptp.a15 @t20)) % 0.61/0.88 (define @t73 () (= tptp.a4 @t21)) % 0.61/0.88 (define @t74 () (= tptp.a11 @t22)) % 0.61/0.88 (define @t75 () (= tptp.a1 @t23)) % 0.61/0.88 (define @t76 () (tptp.product @t32 @t31)) % 0.61/0.88 (define @t77 () (tptp.product @t23 tptp.a2)) % 0.61/0.88 (define @t78 () (= @t77 @t76)) % 0.61/0.88 (define @t79 () (tptp.product @t34 @t33)) % 0.61/0.88 (define @t80 () (= (tptp.product @t10 tptp.a6) @t79)) % 0.61/0.88 (define @t81 () (tptp.product tptp.a3 tptp.a2)) % 0.61/0.88 (define @t82 () (tptp.product @t12 tptp.a2)) % 0.61/0.88 (define @t83 () (= @t82 (tptp.product @t40 @t81))) % 0.61/0.88 (define @t84 () (tptp.product @t30 @t29)) % 0.61/0.88 (define @t85 () (tptp.product @t13 tptp.a1)) % 0.61/0.88 (define @t86 () (= @t85 @t84)) % 0.61/0.88 (define @t87 () (tptp.product (tptp.product tptp.a9 tptp.a11) @t35)) % 0.61/0.88 (define @t88 () (tptp.product @t14 tptp.a11)) % 0.61/0.88 (define @t89 () (= @t88 @t87)) % 0.61/0.88 (define @t90 () (tptp.product (tptp.product tptp.a12 tptp.a8) @t36)) % 0.61/0.88 (define @t91 () (tptp.product @t16 tptp.a8)) % 0.61/0.88 (define @t92 () (= @t91 @t90)) % 0.61/0.88 (define @t93 () (tptp.product (tptp.product tptp.a13 tptp.a7) @t37)) % 0.61/0.88 (define @t94 () (tptp.product @t17 tptp.a7)) % 0.61/0.88 (define @t95 () (= @t94 @t93)) % 0.61/0.88 (define @t96 () (tptp.product @t39 @t38)) % 0.61/0.88 (define @t97 () (tptp.product @t18 tptp.a12)) % 0.61/0.88 (define @t98 () (= @t97 @t96)) % 0.61/0.88 (define @t99 () (tptp.product @t27 @t16)) % 0.61/0.88 (define @t100 () (tptp.product @t19 tptp.a3)) % 0.61/0.88 (define @t101 () (= @t100 @t99)) % 0.61/0.88 (define @t102 () (tptp.product (tptp.product tptp.a14 tptp.a8) @t36)) % 0.61/0.88 (define @t103 () (tptp.product @t20 tptp.a8)) % 0.61/0.88 (define @t104 () (= @t103 @t102)) % 0.61/0.88 (define @t105 () (tptp.product (tptp.product tptp.a15 tptp.a7) @t37)) % 0.61/0.88 (define @t106 () (tptp.product @t21 tptp.a7)) % 0.61/0.88 (define @t107 () (= @t106 @t105)) % 0.61/0.88 (define @t108 () (tptp.product @t16 @t12)) % 0.61/0.88 (define @t109 () (tptp.product @t26 tptp.a3)) % 0.61/0.88 (define @t110 () (= @t109 @t108)) % 0.61/0.88 (define @t111 () (tptp.product @t20 @t12)) % 0.61/0.88 (define @t112 () (tptp.product @t28 tptp.a3)) % 0.61/0.88 (define @t113 () (= @t112 @t111)) % 0.61/0.88 (define @t114 () (tptp.product @t109 tptp.a3)) % 0.61/0.88 (define @t115 () (= @t26 @t114)) % 0.61/0.88 (define @t116 () (= tptp.a1 (tptp.product @t9 tptp.a2))) % 0.61/0.88 (define @t117 () (tptp.product @t99 tptp.a8)) % 0.61/0.88 (define @t118 () (= @t117 (tptp.product @t41 @t91))) % 0.61/0.88 (define @t119 () (tptp.product tptp.a3 tptp.a7)) % 0.61/0.88 (define @t120 () (tptp.product @t28 tptp.a7)) % 0.61/0.88 (define @t121 () (tptp.product @t120 @t119)) % 0.61/0.88 (define @t122 () (= (tptp.product @t112 tptp.a7) @t121)) % 0.61/0.88 (define @t123 () (tptp.product @t51 @t50)) % 0.61/0.88 (define @t124 () (tptp.product @t84 tptp.a2)) % 0.61/0.88 (define @t125 () (= @t124 @t123)) % 0.61/0.88 (define @t126 () (tptp.product @t46 @t45)) % 0.61/0.88 (define @t127 () (= @t76 @t126)) % 0.61/0.88 (define @t128 () (tptp.product @t44 @t43)) % 0.61/0.88 (define @t129 () (tptp.product @t76 tptp.a6)) % 0.61/0.88 (define @t130 () (= @t129 @t128)) % 0.61/0.88 (define @t131 () (tptp.product tptp.a3 @t33)) % 0.61/0.88 (define @t132 () (tptp.product @t131 @t52)) % 0.61/0.88 (define @t133 () (= @t79 @t132)) % 0.61/0.88 (define @t134 () (tptp.product (tptp.product @t34 tptp.a2) (tptp.product @t33 tptp.a2))) % 0.61/0.88 (define @t135 () (tptp.product @t79 tptp.a2)) % 0.61/0.88 (define @t136 () (= @t135 @t134)) % 0.61/0.88 (define @t137 () (tptp.product (tptp.product tptp.a9 @t35) @t53)) % 0.61/0.88 (define @t138 () (= @t87 @t137)) % 0.61/0.88 (define @t139 () (tptp.product @t57 @t55)) % 0.61/0.88 (define @t140 () (= @t90 @t139)) % 0.61/0.88 (define @t141 () (tptp.product @t48 @t47)) % 0.61/0.88 (define @t142 () (= @t93 @t141)) % 0.61/0.88 (define @t143 () (tptp.product (tptp.product tptp.a6 @t38) @t54)) % 0.61/0.88 (define @t144 () (= @t96 @t143)) % 0.61/0.88 (define @t145 () (tptp.product @t58 @t55)) % 0.61/0.88 (define @t146 () (= @t102 @t145)) % 0.61/0.88 (define @t147 () (tptp.product @t49 @t47)) % 0.61/0.88 (define @t148 () (= @t105 @t147)) % 0.61/0.88 (define @t149 () (tptp.product (tptp.product @t39 tptp.a7) @t56)) % 0.61/0.88 (define @t150 () (tptp.product @t96 tptp.a7)) % 0.61/0.88 (define @t151 () (= @t150 @t149)) % 0.61/0.88 (define @t152 () (tptp.product @t112 @t109)) % 0.61/0.88 (define @t153 () (tptp.product @t42 tptp.a3)) % 0.61/0.88 (define @t154 () (= @t153 @t152)) % 0.61/0.88 (define @t155 () (= tptp.a3 (tptp.product tptp.a3 tptp.a3))) % 0.61/0.88 (define @t156 () (tptp.product @t40 tptp.a1)) % 0.61/0.88 (define @t157 () (tptp.product @t156 tptp.a1)) % 0.61/0.88 (define @t158 () (= @t40 @t157)) % 0.61/0.88 (define @t159 () (tptp.product @t41 tptp.a6)) % 0.61/0.88 (define @t160 () (tptp.product @t159 tptp.a6)) % 0.61/0.88 (define @t161 () (= @t41 @t160)) % 0.61/0.88 (define @t162 () (tptp.product @t153 tptp.a3)) % 0.61/0.88 (define @t163 () (= @t42 @t162)) % 0.61/0.88 (define @t164 () (tptp.product @t26 tptp.a7)) % 0.61/0.88 (define @t165 () (= tptp.a12 @t164)) % 0.61/0.88 (define @t166 () (= tptp.a14 @t120)) % 0.61/0.88 (define @t167 () (tptp.product @t128 tptp.a3)) % 0.61/0.88 (define @t168 () (= @t167 (tptp.product (tptp.product @t44 tptp.a3) (tptp.product @t43 tptp.a3)))) % 0.61/0.88 (define @t169 () (tptp.product @t45 tptp.a7)) % 0.61/0.88 (define @t170 () (tptp.product @t46 tptp.a7)) % 0.61/0.88 (define @t171 () (tptp.product @t126 tptp.a7)) % 0.61/0.88 (define @t172 () (= @t171 (tptp.product @t170 @t169))) % 0.61/0.88 (define @t173 () (tptp.product @t47 @t31)) % 0.61/0.88 (define @t174 () (tptp.product (tptp.product @t48 @t31) @t173)) % 0.61/0.88 (define @t175 () (tptp.product @t141 @t31)) % 0.61/0.88 (define @t176 () (= @t175 @t174)) % 0.61/0.88 (define @t177 () (tptp.product (tptp.product @t49 @t31) @t173)) % 0.61/0.88 (define @t178 () (tptp.product @t147 @t31)) % 0.61/0.88 (define @t179 () (= @t178 @t177)) % 0.61/0.88 (define @t180 () (tptp.product (tptp.product @t51 tptp.a6) (tptp.product @t50 tptp.a6))) % 0.61/0.88 (define @t181 () (tptp.product @t123 tptp.a6)) % 0.61/0.88 (define @t182 () (= @t181 @t180)) % 0.61/0.88 (define @t183 () (tptp.product (tptp.product @t32 @t43) (tptp.product tptp.a6 @t43))) % 0.61/0.88 (define @t184 () (= @t128 @t183)) % 0.61/0.88 (define @t185 () (tptp.product (tptp.product @t46 @t33) (tptp.product @t45 @t33))) % 0.61/0.88 (define @t186 () (tptp.product @t126 @t33)) % 0.61/0.88 (define @t187 () (= @t186 @t185)) % 0.61/0.88 (define @t188 () (tptp.product (tptp.product tptp.a3 @t52) (tptp.product @t33 @t52))) % 0.61/0.88 (define @t189 () (= @t132 @t188)) % 0.61/0.88 (define @t190 () (tptp.product (tptp.product tptp.a9 @t53) (tptp.product @t35 @t53))) % 0.61/0.88 (define @t191 () (= @t137 @t190)) % 0.61/0.88 (define @t192 () (tptp.product (tptp.product tptp.a13 @t47) (tptp.product @t37 @t47))) % 0.61/0.88 (define @t193 () (= @t141 @t192)) % 0.61/0.88 (define @t194 () (tptp.product (tptp.product tptp.a6 @t54) (tptp.product @t38 @t54))) % 0.61/0.88 (define @t195 () (= @t143 @t194)) % 0.61/0.88 (define @t196 () (tptp.product (tptp.product tptp.a14 @t55) (tptp.product @t36 @t55))) % 0.61/0.88 (define @t197 () (= @t145 @t196)) % 0.61/0.88 (define @t198 () (tptp.product (tptp.product @t39 @t56) (tptp.product tptp.a7 @t56))) % 0.61/0.88 (define @t199 () (= @t149 @t198)) % 0.61/0.88 (define @t200 () (tptp.product @t13 @t81)) % 0.61/0.88 (define @t201 () (tptp.product @t59 tptp.a2)) % 0.61/0.88 (define @t202 () (= @t201 @t200)) % 0.61/0.88 (define @t203 () (tptp.product @t145 @t139)) % 0.61/0.88 (define @t204 () (tptp.product (tptp.product @t58 @t57) @t55)) % 0.61/0.88 (define @t205 () (= @t204 @t203)) % 0.61/0.88 (define @t206 () (tptp.product @t27 @t12)) % 0.61/0.88 (define @t207 () (tptp.product @t60 tptp.a3)) % 0.61/0.88 (define @t208 () (= @t207 @t206)) % 0.61/0.88 (define @t209 () (tptp.product @t109 @t153)) % 0.61/0.88 (define @t210 () (tptp.product (tptp.product @t26 @t42) tptp.a3)) % 0.61/0.88 (define @t211 () (= @t210 @t209)) % 0.61/0.88 (define @t212 () (tptp.product @t126 @t126)) % 0.61/0.88 (define @t213 () (tptp.product @t46 @t46)) % 0.61/0.88 (define @t214 () (tptp.product @t213 @t45)) % 0.61/0.88 (define @t215 () (= @t214 @t212)) % 0.61/0.88 (define @t216 () (= @t46 @t213)) % 0.61/0.88 (define @t217 () (tptp.product @t201 tptp.a2)) % 0.61/0.88 (define @t218 () (= @t59 @t217)) % 0.61/0.88 (define @t219 () (= @t60 (tptp.product @t207 tptp.a3))) % 0.61/0.88 (define @t220 () (tptp.product @t12 tptp.a3)) % 0.61/0.88 (define @t221 () (= tptp.a7 @t220)) % 0.61/0.88 (define @t222 () (tptp.product @t22 tptp.a7)) % 0.61/0.88 (define @t223 () (= tptp.a4 @t222)) % 0.61/0.88 (define @t224 () (tptp.product @t18 tptp.a7)) % 0.61/0.88 (define @t225 () (= tptp.a6 @t224)) % 0.61/0.88 (define @t226 () (tptp.product @t46 tptp.a6)) % 0.61/0.88 (define @t227 () (tptp.product tptp.a11 @t59)) % 0.61/0.88 (define @t228 () (tptp.product @t33 tptp.a3)) % 0.61/0.88 (define @t229 () (tptp.product @t45 tptp.a3)) % 0.61/0.88 (define @t230 () (tptp.product tptp.a6 tptp.a3)) % 0.61/0.88 (define @t231 () (tptp.product @t40 tptp.a11)) % 0.61/0.88 (define @t232 () (tptp.product @t231 tptp.a7)) % 0.61/0.88 (define @t233 () (tptp.product @t11 tptp.a3)) % 0.61/0.88 (define @t234 () (tptp.product @t34 tptp.a3)) % 0.61/0.88 (define @t235 () (tptp.product @t213 tptp.a7)) % 0.61/0.88 (define @t236 () (tptp.product @t59 tptp.a3)) % 0.61/0.88 (define @t237 () (and @t61 @t62 @t63 @t64 @t65 @t66 @t67 @t68 @t69 @t70 @t71 @t72 @t73 @t74 @t75 @t78 @t80 @t83 @t86 @t89 @t92 @t95 @t98 @t101 @t104 @t107 @t110 @t113 @t115 @t116 @t118 @t122 @t125 @t127 @t130 @t133 @t136 @t138 @t140 @t142 @t144 @t146 @t148 @t151 @t154 @t155 @t158 @t161 @t163 @t165 @t166 @t168 @t172 @t176 @t179 @t182 @t184 @t187 @t189 @t191 @t193 @t195 @t197 @t199 @t202 @t205 @t208 @t211 @t215 @t216 @t218 @t219 @t221 @t223 @t225)) % 0.61/0.88 (assume @p1 @t3) % 0.61/0.88 (assume @p2 @t7) % 0.61/0.88 (assume @p3 (forall (@list @t1 @t4 @t8) (= (tptp.product @t5 @t8) (tptp.product (tptp.product @t1 @t8) (tptp.product @t4 @t8))))) % 0.61/0.88 (assume @p4 (= @t9 tptp.a3)) % 0.61/0.88 (assume @p5 (= @t10 tptp.a5)) % 0.61/0.88 (assume @p6 (= @t11 tptp.a7)) % 0.61/0.88 (assume @p7 (= @t12 tptp.a8)) % 0.61/0.88 (assume @p8 (= @t13 tptp.a9)) % 0.61/0.88 (assume @p9 (= @t14 tptp.a10)) % 0.61/0.88 (assume @p10 (= @t15 tptp.a12)) % 0.61/0.88 (assume @p11 (= @t16 tptp.a13)) % 0.61/0.88 (assume @p12 (= @t17 tptp.a6)) % 0.61/0.88 (assume @p13 (= @t18 tptp.a2)) % 0.61/0.88 (assume @p14 (= @t19 tptp.a14)) % 0.61/0.88 (assume @p15 (= @t20 tptp.a15)) % 0.61/0.88 (assume @p16 (= @t21 tptp.a4)) % 0.61/0.88 (assume @p17 (= @t22 tptp.a11)) % 0.61/0.88 (assume @p18 (= @t23 tptp.a1)) % 0.61/0.88 (assume @p19 (not @t25)) % 0.61/0.88 (step @p20 :rule symm :premises (@p4)) % 0.61/0.88 (step @p21 :rule symm :premises (@p5)) % 0.61/0.88 (step @p22 :rule symm :premises (@p6)) % 0.61/0.88 (step @p23 :rule symm :premises (@p7)) % 0.61/0.88 (step @p24 :rule symm :premises (@p8)) % 0.61/0.88 (step @p25 :rule symm :premises (@p9)) % 0.61/0.88 (step @p26 :rule symm :premises (@p10)) % 0.61/0.88 (step @p27 :rule symm :premises (@p11)) % 0.61/0.88 (step @p28 :rule symm :premises (@p12)) % 0.61/0.88 (step @p29 :rule symm :premises (@p13)) % 0.61/0.88 (step @p30 :rule symm :premises (@p14)) % 0.61/0.88 (step @p31 :rule symm :premises (@p15)) % 0.61/0.88 (step @p32 :rule symm :premises (@p16)) % 0.61/0.88 (step @p33 :rule symm :premises (@p17)) % 0.61/0.88 (step @p34 :rule symm :premises (@p18)) % 0.61/0.88 (step @p35 :rule instantiate :premises (@p3) :args ((@list tptp.a11 tptp.a10 tptp.a2))) % 0.61/0.88 (step @p36 :rule instantiate :premises (@p3) :args ((@list tptp.a3 tptp.a4 tptp.a6))) % 0.61/0.88 (step @p37 :rule instantiate :premises (@p3) :args ((@list tptp.a7 tptp.a3 tptp.a2))) % 0.61/0.88 (step @p38 :rule instantiate :premises (@p3) :args ((@list tptp.a8 tptp.a2 tptp.a1))) % 0.61/0.88 (step @p39 :rule instantiate :premises (@p3) :args ((@list tptp.a9 tptp.a1 tptp.a11))) % 0.61/0.88 (step @p40 :rule instantiate :premises (@p3) :args ((@list tptp.a12 tptp.a3 tptp.a8))) % 0.61/0.88 (step @p41 :rule instantiate :premises (@p3) :args ((@list tptp.a13 tptp.a8 tptp.a7))) % 0.61/0.88 (step @p42 :rule instantiate :premises (@p3) :args ((@list tptp.a6 tptp.a7 tptp.a12))) % 0.61/0.88 (step @p43 :rule instantiate :premises (@p3) :args ((@list tptp.a2 tptp.a12 tptp.a3))) % 0.61/0.88 (step @p44 :rule instantiate :premises (@p3) :args ((@list tptp.a14 tptp.a3 tptp.a8))) % 0.61/0.88 (step @p45 :rule instantiate :premises (@p3) :args ((@list tptp.a15 tptp.a8 tptp.a7))) % 0.61/0.88 (step @p46 :rule instantiate :premises (@p3) :args ((@list tptp.a12 tptp.a7 tptp.a3))) % 0.61/0.88 (step @p47 :rule instantiate :premises (@p3) :args ((@list tptp.a14 tptp.a7 tptp.a3))) % 0.61/0.88 (step @p48 :rule eq-symm :args (@t6 @t1)) % 0.61/0.88 (step @p49 :rule cong :premises (@p48) :args (@t7)) % 0.61/0.88 (step @p50 :rule eq_resolve :premises (@p2 @p49)) % 0.61/0.88 (step @p51 :rule instantiate :premises (@p50) :args ((@list @t26 tptp.a3))) % 0.61/0.88 (step @p52 :rule instantiate :premises (@p50) :args ((@list tptp.a1 tptp.a2))) % 0.61/0.88 (step @p53 :rule instantiate :premises (@p3) :args ((@list @t27 @t16 tptp.a8))) % 0.61/0.88 (step @p54 :rule instantiate :premises (@p3) :args ((@list @t28 tptp.a3 tptp.a7))) % 0.61/0.88 (step @p55 :rule instantiate :premises (@p3) :args ((@list @t30 @t29 tptp.a2))) % 0.61/0.88 (step @p56 :rule instantiate :premises (@p3) :args ((@list tptp.a11 tptp.a2 @t31))) % 0.61/0.88 (step @p57 :rule instantiate :premises (@p3) :args ((@list @t32 @t31 tptp.a6))) % 0.61/0.88 (step @p58 :rule instantiate :premises (@p3) :args ((@list tptp.a3 tptp.a6 @t33))) % 0.61/0.88 (step @p59 :rule instantiate :premises (@p3) :args ((@list @t34 @t33 tptp.a2))) % 0.61/0.88 (step @p60 :rule instantiate :premises (@p3) :args ((@list tptp.a9 tptp.a11 @t35))) % 0.61/0.88 (step @p61 :rule instantiate :premises (@p3) :args ((@list tptp.a12 tptp.a8 @t36))) % 0.61/0.88 (step @p62 :rule instantiate :premises (@p3) :args ((@list tptp.a13 tptp.a7 @t37))) % 0.61/0.88 (step @p63 :rule instantiate :premises (@p3) :args ((@list tptp.a6 tptp.a12 @t38))) % 0.61/0.88 (step @p64 :rule instantiate :premises (@p3) :args ((@list tptp.a14 tptp.a8 @t36))) % 0.61/0.88 (step @p65 :rule instantiate :premises (@p3) :args ((@list tptp.a15 tptp.a7 @t37))) % 0.61/0.88 (step @p66 :rule instantiate :premises (@p3) :args ((@list @t39 @t38 tptp.a7))) % 0.61/0.88 (step @p67 :rule instantiate :premises (@p3) :args ((@list @t28 @t26 tptp.a3))) % 0.61/0.88 (step @p68 :rule eq-symm :args (@t2 @t1)) % 0.61/0.88 (step @p69 :rule cong :premises (@p68) :args (@t3)) % 0.61/0.88 (step @p70 :rule eq_resolve :premises (@p1 @p69)) % 0.61/0.88 (step @p71 :rule instantiate :premises (@p70) :args ((@list tptp.a3))) % 0.61/0.88 (step @p72 :rule instantiate :premises (@p50) :args ((@list @t40 tptp.a1))) % 0.61/0.88 (step @p73 :rule instantiate :premises (@p50) :args ((@list @t41 tptp.a6))) % 0.61/0.88 (step @p74 :rule instantiate :premises (@p50) :args ((@list @t42 tptp.a3))) % 0.61/0.88 (step @p75 :rule instantiate :premises (@p50) :args ((@list tptp.a12 tptp.a7))) % 0.61/0.88 (step @p76 :rule instantiate :premises (@p50) :args ((@list tptp.a14 tptp.a7))) % 0.61/0.88 (step @p77 :rule instantiate :premises (@p3) :args ((@list @t44 @t43 tptp.a3))) % 0.61/0.88 (step @p78 :rule instantiate :premises (@p3) :args ((@list @t46 @t45 tptp.a7))) % 0.61/0.88 (step @p79 :rule instantiate :premises (@p3) :args ((@list @t48 @t47 @t31))) % 0.61/0.88 (step @p80 :rule instantiate :premises (@p3) :args ((@list @t49 @t47 @t31))) % 0.61/0.88 (step @p81 :rule instantiate :premises (@p3) :args ((@list @t51 @t50 tptp.a6))) % 0.61/0.88 (step @p82 :rule instantiate :premises (@p3) :args ((@list @t32 tptp.a6 @t43))) % 0.61/0.88 (step @p83 :rule instantiate :premises (@p3) :args ((@list @t46 @t45 @t33))) % 0.61/0.88 (step @p84 :rule instantiate :premises (@p3) :args ((@list tptp.a3 @t33 @t52))) % 0.61/0.88 (step @p85 :rule instantiate :premises (@p3) :args ((@list tptp.a9 @t35 @t53))) % 0.61/0.88 (step @p86 :rule instantiate :premises (@p3) :args ((@list tptp.a13 @t37 @t47))) % 0.61/0.88 (step @p87 :rule instantiate :premises (@p3) :args ((@list tptp.a6 @t38 @t54))) % 0.61/0.88 (step @p88 :rule instantiate :premises (@p3) :args ((@list tptp.a14 @t36 @t55))) % 0.61/0.88 (step @p89 :rule instantiate :premises (@p3) :args ((@list @t39 tptp.a7 @t56))) % 0.61/0.88 (step @p90 :rule instantiate :premises (@p3) :args ((@list tptp.a8 tptp.a3 tptp.a2))) % 0.61/0.88 (step @p91 :rule instantiate :premises (@p3) :args ((@list @t58 @t57 @t55))) % 0.61/0.88 (step @p92 :rule instantiate :premises (@p3) :args ((@list tptp.a2 tptp.a7 tptp.a3))) % 0.61/0.88 (step @p93 :rule instantiate :premises (@p3) :args ((@list @t26 @t42 tptp.a3))) % 0.61/0.88 (step @p94 :rule instantiate :premises (@p3) :args ((@list @t46 @t46 @t45))) % 0.61/0.88 (step @p95 :rule instantiate :premises (@p70) :args ((@list @t46))) % 0.61/0.88 (step @p96 :rule instantiate :premises (@p50) :args ((@list @t59 tptp.a2))) % 0.61/0.88 (step @p97 :rule instantiate :premises (@p50) :args ((@list @t60 tptp.a3))) % 0.61/0.88 (step @p98 :rule instantiate :premises (@p50) :args ((@list tptp.a7 tptp.a3))) % 0.61/0.88 (step @p99 :rule instantiate :premises (@p50) :args ((@list tptp.a4 tptp.a7))) % 0.61/0.88 (step @p100 :rule instantiate :premises (@p50) :args ((@list tptp.a6 tptp.a7))) % 0.61/0.88 (assume-push @p680 @t61) % 0.61/0.88 (assume-push @p681 @t62) % 0.61/0.88 (assume-push @p682 @t63) % 0.61/0.88 (assume-push @p683 @t64) % 0.61/0.88 (assume-push @p684 @t65) % 0.61/0.88 (assume-push @p685 @t66) % 0.61/0.88 (assume-push @p686 @t67) % 0.61/0.88 (assume-push @p687 @t68) % 0.61/0.88 (assume-push @p688 @t69) % 0.61/0.88 (assume-push @p689 @t70) % 0.61/0.88 (assume-push @p690 @t71) % 0.61/0.88 (assume-push @p691 @t72) % 0.61/0.88 (assume-push @p692 @t73) % 0.61/0.88 (assume-push @p693 @t74) % 0.61/0.88 (assume-push @p694 @t75) % 0.61/0.88 (assume-push @p695 @t78) % 0.61/0.88 (assume-push @p696 @t80) % 0.61/0.88 (assume-push @p697 @t83) % 0.61/0.88 (assume-push @p698 @t86) % 0.61/0.88 (assume-push @p699 @t89) % 0.61/0.88 (assume-push @p700 @t92) % 0.61/0.88 (assume-push @p701 @t95) % 0.61/0.88 (assume-push @p702 @t98) % 0.61/0.88 (assume-push @p703 @t101) % 0.61/0.88 (assume-push @p704 @t104) % 0.61/0.88 (assume-push @p705 @t107) % 0.61/0.88 (assume-push @p706 @t110) % 0.61/0.88 (assume-push @p707 @t113) % 0.61/0.88 (assume-push @p708 @t115) % 0.61/0.88 (assume-push @p709 @t116) % 0.61/0.88 (assume-push @p710 @t118) % 0.61/0.88 (assume-push @p711 @t122) % 0.61/0.88 (assume-push @p712 @t125) % 0.61/0.88 (assume-push @p713 @t127) % 0.61/0.88 (assume-push @p714 @t130) % 0.61/0.88 (assume-push @p715 @t133) % 0.61/0.88 (assume-push @p716 @t136) % 0.61/0.88 (assume-push @p717 @t138) % 0.61/0.88 (assume-push @p718 @t140) % 0.61/0.88 (assume-push @p719 @t142) % 0.61/0.88 (assume-push @p720 @t144) % 0.61/0.88 (assume-push @p721 @t146) % 0.61/0.88 (assume-push @p722 @t148) % 0.61/0.88 (assume-push @p723 @t151) % 0.61/0.88 (assume-push @p724 @t154) % 0.61/0.88 (assume-push @p725 @t155) % 0.61/0.88 (assume-push @p726 @t158) % 0.61/0.88 (assume-push @p727 @t161) % 0.61/0.88 (assume-push @p728 @t163) % 0.61/0.88 (assume-push @p729 @t165) % 0.61/0.88 (assume-push @p730 @t166) % 0.61/0.88 (assume-push @p731 @t168) % 0.61/0.88 (assume-push @p732 @t172) % 0.61/0.88 (assume-push @p733 @t176) % 0.61/0.88 (assume-push @p734 @t179) % 0.61/0.88 (assume-push @p735 @t182) % 0.61/0.88 (assume-push @p736 @t184) % 0.61/0.88 (assume-push @p737 @t187) % 0.61/0.88 (assume-push @p738 @t189) % 0.61/0.88 (assume-push @p739 @t191) % 0.61/0.88 (assume-push @p740 @t193) % 0.61/0.88 (assume-push @p741 @t195) % 0.61/0.88 (assume-push @p742 @t197) % 0.61/0.88 (assume-push @p743 @t199) % 0.61/0.88 (assume-push @p744 @t202) % 0.61/0.88 (assume-push @p745 @t205) % 0.61/0.88 (assume-push @p746 @t208) % 0.61/0.88 (assume-push @p747 @t211) % 0.61/0.88 (assume-push @p748 @t215) % 0.61/0.88 (assume-push @p749 @t216) % 0.61/0.88 (assume-push @p750 @t218) % 0.61/0.88 (assume-push @p751 @t219) % 0.61/0.88 (assume-push @p752 @t221) % 0.61/0.88 (assume-push @p753 @t223) % 0.61/0.88 (assume-push @p754 @t225) % 0.61/0.88 (step @p176 :rule refl :args (tptp.a3)) % 0.61/0.88 (step @p177 :rule cong :premises (@p14 @p176) :args (@t100)) % 0.61/0.88 (step @p178 :rule symm :premises (@p71)) % 0.61/0.88 (step @p179 :rule refl :args (tptp.a2)) % 0.61/0.88 (step @p180 :rule cong :premises (@p18 @p179) :args (@t77)) % 0.61/0.88 (step @p181 :rule symm :premises (@p35)) % 0.61/0.88 (step @p182 :rule symm :premises (@p56)) % 0.61/0.88 (step @p183 :rule refl :args (@t31)) % 0.61/0.88 (step @p184 :rule refl :args (tptp.a7)) % 0.61/0.88 (step @p185 :rule cong :premises (@p12 @p184) :args (@t94)) % 0.61/0.88 (step @p186 :rule symm :premises (@p41)) % 0.61/0.88 (step @p187 :rule symm :premises (@p62)) % 0.61/0.88 (step @p188 :rule trans :premises (@p187 @p186 @p185 @p13)) % 0.61/0.88 (step @p189 :rule cong :premises (@p188 @p183) :args (@t175)) % 0.61/0.88 (step @p190 :rule symm :premises (@p79)) % 0.61/0.88 (step @p191 :rule trans :premises (@p190 @p189)) % 0.61/0.88 (step @p192 :rule cong :premises (@p16 @p184) :args (@t106)) % 0.61/0.88 (step @p193 :rule symm :premises (@p45)) % 0.61/0.88 (step @p194 :rule symm :premises (@p65)) % 0.61/0.88 (step @p195 :rule trans :premises (@p194 @p193 @p192 @p17)) % 0.61/0.88 (step @p196 :rule cong :premises (@p195 @p183) :args (@t178)) % 0.61/0.88 (step @p197 :rule symm :premises (@p80)) % 0.61/0.88 (step @p198 :rule trans :premises (@p197 @p196)) % 0.61/0.88 (step @p199 :rule cong :premises (@p198 @p191) :args ((tptp.product @t177 @t174))) % 0.61/0.88 (step @p200 :rule symm :premises (@p189)) % 0.61/0.88 (step @p201 :rule symm :premises (@p86)) % 0.61/0.88 (step @p202 :rule trans :premises (@p201 @p187 @p186 @p185 @p13)) % 0.61/0.88 (step @p203 :rule cong :premises (@p202 @p183) :args ((tptp.product @t192 @t31))) % 0.61/0.88 (step @p204 :rule refl :args (tptp.a1)) % 0.61/0.88 (step @p205 :rule cong :premises (@p8 @p204) :args (@t85)) % 0.61/0.88 (step @p206 :rule symm :premises (@p52)) % 0.61/0.88 (step @p207 :rule cong :premises (@p20 @p179) :args (@t81)) % 0.61/0.88 (step @p208 :rule trans :premises (@p207 @p206)) % 0.61/0.88 (step @p209 :rule refl :args (@t13)) % 0.61/0.88 (step @p210 :rule cong :premises (@p209 @p208) :args (@t200)) % 0.61/0.88 (step @p211 :rule trans :premises (@p90 @p210 @p205 @p9)) % 0.61/0.88 (step @p212 :rule cong :premises (@p211 @p179) :args (@t217)) % 0.61/0.88 (step @p213 :rule cong :premises (@p7 @p176) :args (@t220)) % 0.61/0.88 (step @p214 :rule trans :premises (@p98 @p213 @p96 @p212)) % 0.61/0.88 (step @p215 :rule symm :premises (@p202)) % 0.61/0.88 (step @p216 :rule cong :premises (@p215 @p214) :args (@t60)) % 0.61/0.88 (step @p217 :rule cong :premises (@p13 @p184) :args (@t224)) % 0.61/0.88 (step @p218 :rule trans :premises (@p100 @p217 @p216 @p203 @p200 @p79)) % 0.61/0.88 (step @p219 :rule symm :premises (@p198)) % 0.61/0.88 (step @p220 :rule cong :premises (@p219 @p218) :args (@t226)) % 0.61/0.88 (step @p221 :rule refl :args (tptp.a6)) % 0.61/0.88 (step @p222 :rule trans :premises (@p96 @p212)) % 0.61/0.88 (step @p223 :rule refl :args (tptp.a11)) % 0.61/0.88 (step @p224 :rule cong :premises (@p223 @p222) :args (@t227)) % 0.61/0.88 (step @p225 :rule trans :premises (@p98 @p213)) % 0.61/0.88 (step @p226 :rule cong :premises (@p223 @p225) :args ((tptp.product tptp.a11 tptp.a7))) % 0.61/0.88 (step @p227 :rule trans :premises (@p226 @p224)) % 0.61/0.88 (step @p228 :rule cong :premises (@p17 @p184) :args (@t222)) % 0.61/0.88 (step @p229 :rule trans :premises (@p99 @p228)) % 0.61/0.88 (step @p230 :rule trans :premises (@p229 @p227)) % 0.61/0.88 (step @p231 :rule cong :premises (@p230 @p221) :args (@t33)) % 0.61/0.88 (step @p232 :rule refl :args (tptp.a8)) % 0.61/0.88 (step @p233 :rule cong :premises (@p15 @p232) :args (@t103)) % 0.61/0.88 (step @p234 :rule symm :premises (@p43)) % 0.61/0.88 (step @p235 :rule trans :premises (@p234 @p177 @p15)) % 0.61/0.88 (step @p236 :rule trans :premises (@p235 @p31)) % 0.61/0.88 (step @p237 :rule cong :premises (@p236 @p232) :args (@t117)) % 0.61/0.88 (step @p238 :rule symm :premises (@p53)) % 0.61/0.88 (step @p239 :rule cong :premises (@p27 @p232) :args (@t17)) % 0.61/0.88 (step @p240 :rule trans :premises (@p28 @p239)) % 0.61/0.88 (step @p241 :rule refl :args (@t41)) % 0.61/0.88 (step @p242 :rule cong :premises (@p241 @p240) :args (@t159)) % 0.61/0.88 (step @p243 :rule trans :premises (@p242 @p238 @p237 @p233 @p16)) % 0.61/0.88 (step @p244 :rule cong :premises (@p243 @p221) :args (@t160)) % 0.61/0.88 (step @p245 :rule refl :args (@t27)) % 0.61/0.88 (step @p246 :rule cong :premises (@p245 @p7) :args (@t206)) % 0.61/0.88 (step @p247 :rule symm :premises (@p97)) % 0.61/0.88 (step @p248 :rule symm :premises (@p92)) % 0.61/0.88 (step @p249 :rule symm :premises (@p246)) % 0.61/0.88 (step @p250 :rule symm :premises (@p73)) % 0.61/0.88 (step @p251 :rule symm :premises (@p244)) % 0.61/0.88 (step @p252 :rule trans :premises (@p251 @p250 @p249 @p248)) % 0.61/0.88 (step @p253 :rule cong :premises (@p252 @p176) :args (@t228)) % 0.61/0.88 (step @p254 :rule symm :premises (@p239)) % 0.61/0.88 (step @p255 :rule refl :args (@t16)) % 0.61/0.88 (step @p256 :rule cong :premises (@p255 @p7) :args (@t108)) % 0.61/0.88 (step @p257 :rule trans :premises (@p46 @p256 @p254 @p12)) % 0.61/0.88 (step @p258 :rule refl :args (@t20)) % 0.61/0.88 (step @p259 :rule cong :premises (@p258 @p7) :args (@t111)) % 0.61/0.88 (step @p260 :rule trans :premises (@p47 @p259 @p233 @p16)) % 0.61/0.88 (step @p261 :rule cong :premises (@p260 @p257) :args (@t152)) % 0.61/0.88 (step @p262 :rule trans :premises (@p67 @p261)) % 0.61/0.88 (step @p263 :rule cong :premises (@p262 @p176) :args (@t162)) % 0.61/0.88 (step @p264 :rule trans :premises (@p74 @p263 @p253 @p247)) % 0.61/0.88 (step @p265 :rule symm :premises (@p74)) % 0.61/0.88 (step @p266 :rule symm :premises (@p263)) % 0.61/0.88 (step @p267 :rule symm :premises (@p253)) % 0.61/0.88 (step @p268 :rule symm :premises (@p216)) % 0.61/0.88 (step @p269 :rule symm :premises (@p203)) % 0.61/0.88 (step @p270 :rule trans :premises (@p190 @p189 @p269 @p268 @p97 @p267 @p266 @p265)) % 0.61/0.88 (step @p271 :rule symm :premises (@p191)) % 0.61/0.88 (step @p272 :rule trans :premises (@p271 @p270 @p264)) % 0.61/0.88 (step @p273 :rule cong :premises (@p272 @p176) :args (@t229)) % 0.61/0.88 (step @p274 :rule trans :premises (@p273 @p92 @p246 @p73 @p244 @p231 @p220 @p199 @p182 @p181 @p180 @p4)) % 0.61/0.88 (step @p275 :rule cong :premises (@p176 @p274) :args ((tptp.product tptp.a3 @t229))) % 0.61/0.88 (step @p276 :rule symm :premises (@p273)) % 0.61/0.88 (step @p277 :rule trans :premises (@p251 @p250 @p249 @p248 @p276)) % 0.61/0.88 (step @p278 :rule cong :premises (@p176 @p277) :args (@t131)) % 0.61/0.88 (step @p279 :rule refl :args (@t33)) % 0.61/0.88 (step @p280 :rule trans :premises (@p182 @p181 @p180 @p4)) % 0.61/0.88 (step @p281 :rule cong :premises (@p280 @p279) :args (@t186)) % 0.61/0.88 (step @p282 :rule symm :premises (@p83)) % 0.61/0.88 (step @p283 :rule trans :premises (@p282 @p281 @p278 @p275 @p178)) % 0.61/0.88 (step @p284 :rule symm :premises (@p281)) % 0.61/0.88 (step @p285 :rule trans :premises (@p284 @p83)) % 0.61/0.88 (step @p286 :rule trans :premises (@p285 @p283)) % 0.61/0.88 (step @p287 :rule cong :premises (@p286 @p176) :args ((tptp.product @t131 tptp.a3))) % 0.61/0.88 (step @p288 :rule trans :premises (@p218 @p191)) % 0.61/0.88 (step @p289 :rule cong :premises (@p288 @p176) :args (@t230)) % 0.61/0.88 (step @p290 :rule symm :premises (@p40)) % 0.61/0.88 (step @p291 :rule symm :premises (@p61)) % 0.61/0.88 (step @p292 :rule trans :premises (@p291 @p290 @p254 @p12)) % 0.61/0.88 (step @p293 :rule symm :premises (@p44)) % 0.61/0.88 (step @p294 :rule symm :premises (@p64)) % 0.61/0.88 (step @p295 :rule trans :premises (@p294 @p293 @p233 @p16)) % 0.61/0.88 (step @p296 :rule cong :premises (@p295 @p292) :args (@t203)) % 0.61/0.88 (step @p297 :rule trans :premises (@p91 @p296 @p231 @p220 @p199 @p182 @p181 @p180 @p4)) % 0.61/0.88 (step @p298 :rule cong :premises (@p292 @p297) :args ((tptp.product @t139 @t204))) % 0.61/0.88 (step @p299 :rule symm :premises (@p91)) % 0.61/0.88 (step @p300 :rule symm :premises (@p296)) % 0.61/0.88 (step @p301 :rule trans :premises (@p300 @p299)) % 0.61/0.88 (step @p302 :rule symm :premises (@p292)) % 0.61/0.88 (step @p303 :rule cong :premises (@p302 @p301) :args (@t52)) % 0.61/0.88 (step @p304 :rule trans :premises (@p303 @p298 @p289 @p273 @p92 @p246 @p73 @p244 @p231 @p220 @p199 @p182 @p181 @p180 @p4)) % 0.61/0.88 (step @p305 :rule symm :premises (@p285)) % 0.61/0.88 (step @p306 :rule cong :premises (@p305 @p304) :args ((tptp.product @t185 @t52))) % 0.61/0.88 (step @p307 :rule refl :args (@t52)) % 0.61/0.88 (step @p308 :rule cong :premises (@p285 @p307) :args (@t132)) % 0.61/0.88 (step @p309 :rule cong :premises (@p21 @p221) :args (@t11)) % 0.61/0.88 (step @p310 :rule trans :premises (@p22 @p309 @p36 @p58 @p308 @p306 @p287 @p178)) % 0.61/0.88 (step @p311 :rule cong :premises (@p297 @p176) :args ((tptp.product @t204 tptp.a3))) % 0.61/0.88 (step @p312 :rule cong :premises (@p301 @p176) :args (@t228)) % 0.61/0.88 (step @p313 :rule trans :premises (@p100 @p217 @p97 @p267 @p312 @p311 @p178)) % 0.61/0.88 (step @p314 :rule symm :premises (@p218)) % 0.61/0.88 (step @p315 :rule symm :premises (@p270)) % 0.61/0.88 (step @p316 :rule trans :premises (@p315 @p314 @p313)) % 0.61/0.88 (step @p317 :rule cong :premises (@p316 @p310) :args ((tptp.product @t42 tptp.a7))) % 0.61/0.88 (step @p318 :rule trans :premises (@p271 @p270)) % 0.61/0.88 (step @p319 :rule cong :premises (@p318 @p184) :args (@t169)) % 0.61/0.88 (step @p320 :rule symm :premises (@p240)) % 0.61/0.88 (step @p321 :rule trans :premises (@p320 @p218 @p191)) % 0.61/0.88 (step @p322 :rule cong :premises (@p321 @p184) :args ((tptp.product @t91 tptp.a7))) % 0.61/0.88 (step @p323 :rule symm :premises (@p313)) % 0.61/0.88 (step @p324 :rule trans :premises (@p323 @p240)) % 0.61/0.88 (step @p325 :rule cong :premises (@p324 @p184) :args (@t119)) % 0.61/0.88 (step @p326 :rule cong :premises (@p257 @p262) :args (@t209)) % 0.61/0.88 (step @p327 :rule trans :premises (@p93 @p326 @p303 @p298 @p289 @p273 @p92 @p246 @p73 @p244 @p231 @p220 @p199 @p182 @p181 @p180 @p4)) % 0.61/0.88 (step @p328 :rule symm :premises (@p93)) % 0.61/0.88 (step @p329 :rule symm :premises (@p326)) % 0.61/0.88 (step @p330 :rule symm :premises (@p303)) % 0.61/0.88 (step @p331 :rule symm :premises (@p298)) % 0.61/0.88 (step @p332 :rule cong :premises (@p257 @p176) :args (@t114)) % 0.61/0.88 (step @p333 :rule trans :premises (@p51 @p332 @p331 @p330 @p329 @p328)) % 0.61/0.88 (step @p334 :rule cong :premises (@p7 @p179) :args (@t82)) % 0.61/0.88 (step @p335 :rule symm :premises (@p37)) % 0.61/0.88 (step @p336 :rule symm :premises (@p208)) % 0.61/0.88 (step @p337 :rule refl :args (@t40)) % 0.61/0.88 (step @p338 :rule cong :premises (@p337 @p336) :args (@t156)) % 0.61/0.88 (step @p339 :rule trans :premises (@p338 @p335 @p334 @p8)) % 0.61/0.88 (step @p340 :rule trans :premises (@p339 @p24)) % 0.61/0.88 (step @p341 :rule cong :premises (@p340 @p204) :args (@t157)) % 0.61/0.88 (step @p342 :rule symm :premises (@p309)) % 0.61/0.88 (step @p343 :rule symm :premises (@p36)) % 0.61/0.88 (step @p344 :rule trans :premises (@p343 @p342 @p6)) % 0.61/0.88 (step @p345 :rule cong :premises (@p344 @p179) :args (@t135)) % 0.61/0.88 (step @p346 :rule symm :premises (@p59)) % 0.61/0.88 (step @p347 :rule trans :premises (@p346 @p345 @p72 @p341 @p205 @p9)) % 0.61/0.88 (step @p348 :rule cong :premises (@p347 @p223) :args ((tptp.product @t134 tptp.a11))) % 0.61/0.88 (step @p349 :rule symm :premises (@p345)) % 0.61/0.88 (step @p350 :rule trans :premises (@p349 @p59)) % 0.61/0.88 (step @p351 :rule cong :premises (@p350 @p223) :args (@t231)) % 0.61/0.88 (step @p352 :rule trans :premises (@p351 @p348 @p10)) % 0.61/0.88 (step @p353 :rule cong :premises (@p352 @p184) :args (@t232)) % 0.61/0.88 (step @p354 :rule trans :premises (@p353 @p333 @p327)) % 0.61/0.88 (step @p355 :rule cong :premises (@p354 @p184) :args ((tptp.product @t232 tptp.a7))) % 0.61/0.88 (step @p356 :rule symm :premises (@p353)) % 0.61/0.88 (step @p357 :rule symm :premises (@p51)) % 0.61/0.88 (step @p358 :rule symm :premises (@p332)) % 0.61/0.88 (step @p359 :rule trans :premises (@p358 @p357)) % 0.61/0.88 (step @p360 :rule trans :premises (@p359 @p356)) % 0.61/0.88 (step @p361 :rule cong :premises (@p360 @p184) :args ((tptp.product @t230 tptp.a7))) % 0.61/0.88 (step @p362 :rule symm :premises (@p359)) % 0.61/0.88 (step @p363 :rule cong :premises (@p362 @p184) :args (@t164)) % 0.61/0.88 (step @p364 :rule trans :premises (@p75 @p363 @p361 @p355 @p325 @p322 @p319 @p317 @p178)) % 0.61/0.88 (step @p365 :rule refl :args (tptp.a12)) % 0.61/0.88 (step @p366 :rule cong :premises (@p13 @p365) :args (@t97)) % 0.61/0.88 (step @p367 :rule symm :premises (@p42)) % 0.61/0.88 (step @p368 :rule symm :premises (@p63)) % 0.61/0.88 (step @p369 :rule symm :premises (@p87)) % 0.61/0.88 (step @p370 :rule trans :premises (@p369 @p368 @p367 @p366 @p14)) % 0.61/0.88 (step @p371 :rule trans :premises (@p370 @p30)) % 0.61/0.88 (step @p372 :rule cong :premises (@p371 @p364) :args ((tptp.product @t194 tptp.a12))) % 0.61/0.88 (step @p373 :rule symm :premises (@p370)) % 0.61/0.88 (step @p374 :rule cong :premises (@p373 @p365) :args ((tptp.product tptp.a14 tptp.a12))) % 0.61/0.88 (step @p375 :rule symm :premises (@p75)) % 0.61/0.88 (step @p376 :rule symm :premises (@p363)) % 0.61/0.88 (step @p377 :rule symm :premises (@p361)) % 0.61/0.88 (step @p378 :rule symm :premises (@p355)) % 0.61/0.88 (step @p379 :rule trans :premises (@p378 @p377 @p376 @p375)) % 0.61/0.88 (step @p380 :rule cong :premises (@p370 @p379) :args ((tptp.product @t194 @t119))) % 0.61/0.88 (step @p381 :rule refl :args (@t119)) % 0.61/0.88 (step @p382 :rule symm :premises (@p76)) % 0.61/0.88 (step @p383 :rule trans :premises (@p382 @p373)) % 0.61/0.88 (step @p384 :rule cong :premises (@p383 @p381) :args (@t121)) % 0.61/0.88 (step @p385 :rule symm :premises (@p260)) % 0.61/0.88 (step @p386 :rule cong :premises (@p385 @p184) :args (@t22)) % 0.61/0.88 (step @p387 :rule symm :premises (@p88)) % 0.61/0.88 (step @p388 :rule trans :premises (@p387 @p294 @p293 @p233 @p16)) % 0.61/0.88 (step @p389 :rule cong :premises (@p388 @p184) :args ((tptp.product @t196 tptp.a7))) % 0.61/0.88 (step @p390 :rule symm :premises (@p388)) % 0.61/0.88 (step @p391 :rule symm :premises (@p229)) % 0.61/0.88 (step @p392 :rule symm :premises (@p227)) % 0.61/0.88 (step @p393 :rule trans :premises (@p392 @p391 @p390)) % 0.61/0.88 (step @p394 :rule cong :premises (@p393 @p184) :args (@t170)) % 0.61/0.88 (step @p395 :rule cong :premises (@p198 @p184) :args ((tptp.product @t177 tptp.a7))) % 0.61/0.88 (step @p396 :rule symm :premises (@p310)) % 0.61/0.88 (step @p397 :rule cong :premises (@p219 @p396) :args ((tptp.product @t46 tptp.a3))) % 0.61/0.88 (step @p398 :rule cong :premises (@p198 @p313) :args ((tptp.product @t177 tptp.a6))) % 0.61/0.88 (step @p399 :rule cong :premises (@p219 @p221) :args (@t226)) % 0.61/0.88 (step @p400 :rule symm :premises (@p220)) % 0.61/0.88 (step @p401 :rule symm :premises (@p199)) % 0.61/0.88 (step @p402 :rule symm :premises (@p180)) % 0.61/0.88 (step @p403 :rule refl :args (@t26)) % 0.61/0.88 (step @p404 :rule trans :premises (@p367 @p366 @p14)) % 0.61/0.88 (step @p405 :rule cong :premises (@p404 @p184) :args (@t150)) % 0.61/0.88 (step @p406 :rule symm :premises (@p66)) % 0.61/0.88 (step @p407 :rule symm :premises (@p89)) % 0.61/0.88 (step @p408 :rule trans :premises (@p407 @p406 @p405)) % 0.61/0.88 (step @p409 :rule cong :premises (@p408 @p403) :args ((tptp.product @t198 @t26))) % 0.61/0.88 (step @p410 :rule symm :premises (@p289)) % 0.61/0.88 (step @p411 :rule symm :premises (@p231)) % 0.61/0.88 (step @p412 :rule trans :premises (@p20 @p402 @p35 @p56 @p401 @p400 @p411 @p251 @p250 @p249 @p248 @p276 @p410 @p358 @p357)) % 0.61/0.88 (step @p413 :rule symm :premises (@p408)) % 0.61/0.88 (step @p414 :rule cong :premises (@p413 @p412) :args (@t112)) % 0.61/0.88 (step @p415 :rule cong :premises (@p408 @p310) :args ((tptp.product @t198 tptp.a7))) % 0.61/0.88 (step @p416 :rule cong :premises (@p413 @p184) :args (@t120)) % 0.61/0.88 (step @p417 :rule trans :premises (@p76 @p416 @p415 @p414 @p409 @p74 @p263 @p312 @p311 @p178 @p20 @p402 @p35 @p56 @p401 @p400 @p399 @p398 @p397 @p395 @p394 @p389 @p386 @p54 @p384 @p380 @p374 @p372 @p177 @p15)) % 0.61/0.88 (step @p418 :rule symm :premises (@p416)) % 0.61/0.88 (step @p419 :rule symm :premises (@p415)) % 0.61/0.88 (step @p420 :rule symm :premises (@p414)) % 0.61/0.88 (step @p421 :rule symm :premises (@p409)) % 0.61/0.88 (step @p422 :rule symm :premises (@p312)) % 0.61/0.88 (step @p423 :rule symm :premises (@p311)) % 0.61/0.88 (step @p424 :rule cong :premises (@p9 @p223) :args (@t88)) % 0.61/0.88 (step @p425 :rule symm :premises (@p39)) % 0.61/0.88 (step @p426 :rule symm :premises (@p60)) % 0.61/0.88 (step @p427 :rule symm :premises (@p85)) % 0.61/0.88 (step @p428 :rule trans :premises (@p427 @p426 @p425 @p424 @p10)) % 0.61/0.88 (step @p429 :rule cong :premises (@p428 @p184) :args ((tptp.product @t190 tptp.a7))) % 0.61/0.88 (step @p430 :rule symm :premises (@p428)) % 0.61/0.88 (step @p431 :rule trans :premises (@p10 @p430)) % 0.61/0.88 (step @p432 :rule cong :premises (@p431 @p396) :args ((tptp.product @t15 tptp.a3))) % 0.61/0.88 (step @p433 :rule cong :premises (@p26 @p176) :args (@t16)) % 0.61/0.88 (step @p434 :rule trans :premises (@p27 @p433 @p432 @p429 @p51 @p332 @p289 @p273 @p92 @p246 @p73 @p244 @p231 @p220 @p199 @p182 @p181 @p180 @p4 @p71 @p423 @p422 @p266 @p265 @p421 @p420 @p419 @p418 @p382)) % 0.61/0.88 (step @p435 :rule symm :premises (@p433)) % 0.61/0.88 (step @p436 :rule symm :premises (@p432)) % 0.61/0.88 (step @p437 :rule symm :premises (@p429)) % 0.61/0.88 (step @p438 :rule trans :premises (@p75 @p363 @p361 @p355 @p325 @p322 @p319 @p317 @p178 @p20 @p402 @p35 @p56 @p401 @p400 @p411 @p251 @p250 @p249 @p248 @p276 @p410 @p358 @p357 @p437 @p436 @p435 @p11)) % 0.61/0.88 (step @p439 :rule symm :premises (@p325)) % 0.61/0.88 (step @p440 :rule symm :premises (@p322)) % 0.61/0.88 (step @p441 :rule symm :premises (@p319)) % 0.61/0.88 (step @p442 :rule symm :premises (@p317)) % 0.61/0.88 (step @p443 :rule symm :premises (@p399)) % 0.61/0.88 (step @p444 :rule symm :premises (@p398)) % 0.61/0.88 (step @p445 :rule symm :premises (@p397)) % 0.61/0.88 (step @p446 :rule symm :premises (@p395)) % 0.61/0.88 (step @p447 :rule symm :premises (@p394)) % 0.61/0.88 (step @p448 :rule symm :premises (@p389)) % 0.61/0.88 (step @p449 :rule trans :premises (@p33 @p448 @p447 @p446 @p445 @p444 @p443 @p220 @p199 @p182 @p181 @p180 @p4 @p71 @p442 @p441 @p440 @p439 @p378 @p377 @p376 @p375)) % 0.61/0.88 (step @p450 :rule trans :premises (@p6 @p310)) % 0.61/0.88 (step @p451 :rule cong :premises (@p450 @p176) :args (@t233)) % 0.61/0.88 (step @p452 :rule symm :premises (@p58)) % 0.61/0.88 (step @p453 :rule symm :premises (@p84)) % 0.61/0.88 (step @p454 :rule trans :premises (@p453 @p452 @p343 @p342 @p6)) % 0.61/0.88 (step @p455 :rule trans :premises (@p454 @p22)) % 0.61/0.88 (step @p456 :rule cong :premises (@p455 @p364) :args ((tptp.product @t188 tptp.a12))) % 0.61/0.88 (step @p457 :rule symm :premises (@p454)) % 0.61/0.88 (step @p458 :rule cong :premises (@p457 @p365) :args (@t38)) % 0.61/0.88 (step @p459 :rule cong :premises (@p240 @p184) :args (@t18)) % 0.61/0.88 (step @p460 :rule trans :premises (@p29 @p459 @p439 @p378 @p377 @p376 @p375)) % 0.61/0.88 (step @p461 :rule trans :premises (@p181 @p180 @p4)) % 0.61/0.88 (step @p462 :rule cong :premises (@p461 @p221) :args (@t129)) % 0.61/0.88 (step @p463 :rule symm :premises (@p57)) % 0.61/0.88 (step @p464 :rule symm :premises (@p82)) % 0.61/0.88 (step @p465 :rule trans :premises (@p464 @p463 @p462)) % 0.61/0.88 (step @p466 :rule cong :premises (@p465 @p279) :args ((tptp.product @t183 @t33))) % 0.61/0.88 (step @p467 :rule trans :premises (@p20 @p402 @p35 @p56 @p401 @p400 @p411)) % 0.61/0.88 (step @p468 :rule symm :premises (@p465)) % 0.61/0.88 (step @p469 :rule cong :premises (@p468 @p467) :args (@t234)) % 0.61/0.88 (step @p470 :rule trans :premises (@p463 @p462)) % 0.61/0.88 (step @p471 :rule cong :premises (@p470 @p176) :args (@t167)) % 0.61/0.88 (step @p472 :rule symm :premises (@p77)) % 0.61/0.88 (step @p473 :rule trans :premises (@p472 @p471 @p469 @p466 @p343 @p342 @p6)) % 0.61/0.88 (step @p474 :rule symm :premises (@p471)) % 0.61/0.88 (step @p475 :rule trans :premises (@p474 @p77)) % 0.61/0.88 (step @p476 :rule trans :premises (@p475 @p473)) % 0.61/0.88 (step @p477 :rule cong :premises (@p476 @p460) :args ((tptp.product @t234 tptp.a2))) % 0.61/0.88 (step @p478 :rule symm :premises (@p476)) % 0.61/0.88 (step @p479 :rule cong :premises (@p478 @p179) :args (@t40)) % 0.61/0.88 (step @p480 :rule symm :premises (@p72)) % 0.61/0.88 (step @p481 :rule symm :premises (@p341)) % 0.61/0.88 (step @p482 :rule symm :premises (@p205)) % 0.61/0.88 (step @p483 :rule trans :premises (@p25 @p482 @p481 @p480 @p479 @p477 @p458 @p456 @p451 @p178 @p20 @p402 @p35 @p56 @p401 @p400 @p399 @p398 @p397 @p395 @p394 @p389 @p17)) % 0.61/0.88 (step @p484 :rule symm :premises (@p479)) % 0.61/0.88 (step @p485 :rule symm :premises (@p477)) % 0.61/0.88 (step @p486 :rule symm :premises (@p458)) % 0.61/0.88 (step @p487 :rule symm :premises (@p456)) % 0.61/0.88 (step @p488 :rule symm :premises (@p451)) % 0.61/0.88 (step @p489 :rule symm :premises (@p98)) % 0.61/0.88 (step @p490 :rule symm :premises (@p213)) % 0.61/0.88 (step @p491 :rule cong :premises (@p6 @p176) :args (@t233)) % 0.61/0.88 (step @p492 :rule cong :premises (@p22 @p313) :args ((tptp.product tptp.a7 tptp.a6))) % 0.61/0.88 (step @p493 :rule symm :premises (@p214)) % 0.61/0.88 (step @p494 :rule cong :premises (@p493 @p221) :args (@t43)) % 0.61/0.88 (step @p495 :rule symm :premises (@p38)) % 0.61/0.88 (step @p496 :rule trans :premises (@p495 @p205 @p9)) % 0.61/0.88 (step @p497 :rule cong :premises (@p496 @p179) :args (@t124)) % 0.61/0.88 (step @p498 :rule symm :premises (@p55)) % 0.61/0.88 (step @p499 :rule trans :premises (@p498 @p497)) % 0.61/0.88 (step @p500 :rule cong :premises (@p499 @p221) :args (@t181)) % 0.61/0.88 (step @p501 :rule symm :premises (@p81)) % 0.61/0.88 (step @p502 :rule trans :premises (@p501 @p500 @p494 @p492 @p491 @p7)) % 0.61/0.88 (step @p503 :rule cong :premises (@p502 @p364) :args ((tptp.product @t180 tptp.a12))) % 0.61/0.88 (step @p504 :rule cong :premises (@p280 @p184) :args (@t171)) % 0.61/0.88 (step @p505 :rule symm :premises (@p78)) % 0.61/0.88 (step @p506 :rule refl :args (@t169)) % 0.61/0.88 (step @p507 :rule symm :premises (@p95)) % 0.61/0.88 (step @p508 :rule cong :premises (@p507 @p184) :args (@t235)) % 0.61/0.88 (step @p509 :rule cong :premises (@p508 @p506) :args ((tptp.product @t235 @t169))) % 0.61/0.88 (step @p510 :rule trans :premises (@p29 @p459 @p322)) % 0.61/0.88 (step @p511 :rule symm :premises (@p508)) % 0.61/0.88 (step @p512 :rule trans :premises (@p33 @p448 @p447 @p511)) % 0.61/0.88 (step @p513 :rule cong :premises (@p512 @p510) :args (@t32)) % 0.61/0.88 (step @p514 :rule trans :premises (@p513 @p509 @p505 @p504 @p378 @p377 @p376 @p375)) % 0.61/0.88 (step @p515 :rule symm :premises (@p502)) % 0.61/0.88 (step @p516 :rule cong :premises (@p515 @p514) :args ((tptp.product tptp.a8 @t32))) % 0.61/0.88 (step @p517 :rule symm :premises (@p513)) % 0.61/0.88 (step @p518 :rule symm :premises (@p509)) % 0.61/0.88 (step @p519 :rule symm :premises (@p504)) % 0.61/0.88 (step @p520 :rule trans :premises (@p29 @p459 @p439 @p519 @p78 @p518 @p517)) % 0.61/0.88 (step @p521 :rule symm :premises (@p225)) % 0.61/0.88 (step @p522 :rule trans :premises (@p521 @p22)) % 0.61/0.88 (step @p523 :rule cong :premises (@p522 @p176) :args (@t236)) % 0.61/0.88 (step @p524 :rule trans :premises (@p523 @p491 @p7)) % 0.61/0.88 (step @p525 :rule cong :premises (@p524 @p520) :args ((tptp.product @t236 tptp.a2))) % 0.61/0.88 (step @p526 :rule symm :premises (@p524)) % 0.61/0.88 (step @p527 :rule trans :premises (@p7 @p526)) % 0.61/0.88 (step @p528 :rule cong :premises (@p527 @p179) :args (@t82)) % 0.61/0.88 (step @p529 :rule symm :premises (@p334)) % 0.61/0.88 (step @p530 :rule trans :premises (@p24 @p529 @p528 @p525 @p516 @p503 @p490 @p489 @p22 @p309 @p36 @p58 @p308 @p306 @p287 @p488 @p487 @p486 @p485 @p484 @p72 @p341 @p205 @p9)) % 0.61/0.88 (step @p531 :rule symm :premises (@p528)) % 0.61/0.88 (step @p532 :rule symm :premises (@p525)) % 0.61/0.88 (step @p533 :rule symm :premises (@p516)) % 0.61/0.88 (step @p534 :rule symm :premises (@p503)) % 0.61/0.88 (step @p535 :rule symm :premises (@p308)) % 0.61/0.88 (step @p536 :rule symm :premises (@p306)) % 0.61/0.88 (step @p537 :rule symm :premises (@p287)) % 0.61/0.88 (step @p538 :rule symm :premises (@p491)) % 0.61/0.88 (step @p539 :rule trans :premises (@p23 @p538 @p451 @p537 @p536 @p535 @p452 @p343 @p342 @p6 @p98 @p213 @p534 @p533 @p532 @p531 @p334 @p8)) % 0.61/0.88 (step @p540 :rule trans :premises (@p22 @p309 @p36 @p58 @p308 @p306 @p287 @p488 @p491 @p7)) % 0.61/0.88 (step @p541 :rule trans :premises (@p100 @p217 @p97 @p267 @p312 @p311 @p537 @p536 @p535 @p452 @p343 @p342 @p6)) % 0.61/0.88 (step @p542 :rule symm :premises (@p100)) % 0.61/0.88 (step @p543 :rule symm :premises (@p217)) % 0.61/0.88 (step @p544 :rule symm :premises (@p47)) % 0.61/0.88 (step @p545 :rule symm :premises (@p259)) % 0.61/0.88 (step @p546 :rule symm :premises (@p233)) % 0.61/0.88 (step @p547 :rule trans :premises (@p32 @p546 @p545 @p544 @p414 @p409 @p74 @p263 @p312 @p311 @p178)) % 0.61/0.88 (step @p548 :rule cong :premises (@p280 @p280) :args (@t212)) % 0.61/0.88 (step @p549 :rule trans :premises (@p94 @p548 @p178)) % 0.61/0.88 (step @p550 :rule cong :premises (@p549 @p547) :args ((tptp.product @t214 tptp.a4))) % 0.61/0.88 (step @p551 :rule refl :args (tptp.a4)) % 0.61/0.88 (step @p552 :rule symm :premises (@p549)) % 0.61/0.88 (step @p553 :rule trans :premises (@p4 @p552)) % 0.61/0.88 (step @p554 :rule cong :premises (@p553 @p551) :args ((tptp.product @t9 tptp.a4))) % 0.61/0.88 (step @p555 :rule cong :premises (@p20 @p551) :args (@t10)) % 0.61/0.88 (step @p556 :rule trans :premises (@p21 @p555 @p554 @p550 @p423 @p422 @p253 @p247 @p543 @p542)) % 0.61/0.88 (step @p557 :rule symm :premises (@p555)) % 0.61/0.88 (step @p558 :rule symm :premises (@p554)) % 0.61/0.88 (step @p559 :rule symm :premises (@p550)) % 0.61/0.88 (step @p560 :rule trans :premises (@p32 @p546 @p545 @p544 @p414 @p409 @p74 @p263 @p312 @p311 @p559 @p558 @p557 @p5)) % 0.61/0.88 (step @p561 :rule symm :premises (@p547)) % 0.61/0.88 (step @p562 :rule trans :premises (@p29 @p459 @p322 @p319 @p317 @p178)) % 0.61/0.88 (step @p563 :rule symm :premises (@p459)) % 0.61/0.88 (step @p564 :rule cong :premises (@p354 @p364) :args ((tptp.product @t232 tptp.a12))) % 0.61/0.88 (step @p565 :rule cong :premises (@p356 @p365) :args ((tptp.product @t26 tptp.a12))) % 0.61/0.88 (step @p566 :rule symm :premises (@p333)) % 0.61/0.88 (step @p567 :rule cong :premises (@p566 @p365) :args ((tptp.product @t210 tptp.a12))) % 0.61/0.88 (step @p568 :rule symm :premises (@p327)) % 0.61/0.88 (step @p569 :rule cong :premises (@p568 @p365) :args ((tptp.product tptp.a3 tptp.a12))) % 0.61/0.88 (step @p570 :rule trans :premises (@p224 @p392 @p391 @p547)) % 0.61/0.88 (step @p571 :rule cong :premises (@p570 @p460) :args ((tptp.product @t227 tptp.a2))) % 0.61/0.88 (step @p572 :rule symm :premises (@p224)) % 0.61/0.88 (step @p573 :rule cong :premises (@p572 @p179) :args ((tptp.product @t46 tptp.a2))) % 0.61/0.88 (step @p574 :rule trans :premises (@p251 @p250)) % 0.61/0.88 (step @p575 :rule symm :premises (@p252)) % 0.61/0.88 (step @p576 :rule trans :premises (@p575 @p574)) % 0.61/0.88 (step @p577 :rule cong :premises (@p576 @p257) :args ((tptp.product @t207 @t109))) % 0.61/0.88 (step @p578 :rule symm :premises (@p257)) % 0.61/0.88 (step @p579 :rule cong :premises (@p507 @p221) :args ((tptp.product @t213 tptp.a6))) % 0.61/0.88 (step @p580 :rule symm :premises (@p579)) % 0.61/0.88 (step @p581 :rule trans :premises (@p231 @p580)) % 0.61/0.88 (step @p582 :rule symm :premises (@p581)) % 0.61/0.88 (step @p583 :rule trans :premises (@p579 @p220 @p199 @p182 @p181 @p180 @p4)) % 0.61/0.88 (step @p584 :rule symm :premises (@p583)) % 0.61/0.88 (step @p585 :rule trans :premises (@p584 @p582 @p252)) % 0.61/0.88 (step @p586 :rule cong :premises (@p585 @p578) :args (@t34)) % 0.61/0.88 (step @p587 :rule trans :premises (@p543 @p542)) % 0.61/0.88 (step @p588 :rule cong :premises (@p176 @p587) :args ((tptp.product tptp.a3 @t60))) % 0.61/0.88 (step @p589 :rule trans :premises (@p588 @p586 @p577 @p242 @p238 @p237 @p233 @p16)) % 0.61/0.88 (step @p590 :rule symm :premises (@p588)) % 0.61/0.88 (step @p591 :rule trans :premises (@p465 @p590 @p589 @p229 @p227)) % 0.61/0.88 (step @p592 :rule cong :premises (@p591 @p179) :args ((tptp.product @t183 tptp.a2))) % 0.61/0.88 (step @p593 :rule symm :premises (@p589)) % 0.61/0.88 (step @p594 :rule trans :premises (@p561 @p593 @p588 @p468)) % 0.61/0.88 (step @p595 :rule cong :premises (@p594 @p179) :args (@t81)) % 0.61/0.88 (step @p596 :rule symm :premises (@p207)) % 0.61/0.88 (step @p597 :rule trans :premises (@p52 @p596 @p595 @p592 @p573 @p571 @p569 @p567 @p565 @p564 @p442 @p441 @p440 @p563 @p13)) % 0.61/0.88 (step @p598 :rule cong :premises (@p597 @p562 @p561 @p560 @p556 @p541 @p540 @p539 @p530 @p483 @p449 @p438 @p434 @p417) :args (@t24)) % 0.61/0.88 (step-pop @p755 :rule scope :premises (@p598)) % 0.61/0.88 (step-pop @p756 :rule scope :premises (@p755)) % 0.61/0.88 (step-pop @p757 :rule scope :premises (@p756)) % 0.61/0.88 (step-pop @p758 :rule scope :premises (@p757)) % 0.61/0.88 (step-pop @p759 :rule scope :premises (@p758)) % 0.61/0.88 (step-pop @p760 :rule scope :premises (@p759)) % 0.61/0.88 (step-pop @p761 :rule scope :premises (@p760)) % 0.61/0.88 (step-pop @p762 :rule scope :premises (@p761)) % 0.61/0.88 (step-pop @p763 :rule scope :premises (@p762)) % 0.61/0.88 (step-pop @p764 :rule scope :premises (@p763)) % 0.61/0.88 (step-pop @p765 :rule scope :premises (@p764)) % 0.61/0.88 (step-pop @p766 :rule scope :premises (@p765)) % 0.61/0.88 (step-pop @p767 :rule scope :premises (@p766)) % 0.61/0.88 (step-pop @p768 :rule scope :premises (@p767)) % 0.61/0.88 (step-pop @p769 :rule scope :premises (@p768)) % 0.61/0.88 (step-pop @p770 :rule scope :premises (@p769)) % 0.61/0.88 (step-pop @p771 :rule scope :premises (@p770)) % 0.61/0.88 (step-pop @p772 :rule scope :premises (@p771)) % 0.61/0.88 (step-pop @p773 :rule scope :premises (@p772)) % 0.61/0.88 (step-pop @p774 :rule scope :premises (@p773)) % 0.61/0.88 (step-pop @p775 :rule scope :premises (@p774)) % 0.61/0.88 (step-pop @p776 :rule scope :premises (@p775)) % 0.61/0.88 (step-pop @p777 :rule scope :premises (@p776)) % 0.61/0.88 (step-pop @p778 :rule scope :premises (@p777)) % 0.61/0.88 (step-pop @p779 :rule scope :premises (@p778)) % 0.61/0.88 (step-pop @p780 :rule scope :premises (@p779)) % 0.61/0.88 (step-pop @p781 :rule scope :premises (@p780)) % 0.61/0.88 (step-pop @p782 :rule scope :premises (@p781)) % 0.61/0.88 (step-pop @p783 :rule scope :premises (@p782)) % 0.61/0.88 (step-pop @p784 :rule scope :premises (@p783)) % 0.61/0.88 (step-pop @p785 :rule scope :premises (@p784)) % 0.61/0.88 (step-pop @p786 :rule scope :premises (@p785)) % 0.61/0.88 (step-pop @p787 :rule scope :premises (@p786)) % 0.61/0.88 (step-pop @p788 :rule scope :premises (@p787)) % 0.61/0.88 (step-pop @p789 :rule scope :premises (@p788)) % 0.61/0.88 (step-pop @p790 :rule scope :premises (@p789)) % 0.61/0.88 (step-pop @p791 :rule scope :premises (@p790)) % 0.61/0.88 (step-pop @p792 :rule scope :premises (@p791)) % 0.61/0.88 (step-pop @p793 :rule scope :premises (@p792)) % 0.61/0.88 (step-pop @p794 :rule scope :premises (@p793)) % 0.61/0.88 (step-pop @p795 :rule scope :premises (@p794)) % 0.61/0.88 (step-pop @p796 :rule scope :premises (@p795)) % 0.61/0.88 (step-pop @p797 :rule scope :premises (@p796)) % 0.61/0.88 (step-pop @p798 :rule scope :premises (@p797)) % 0.61/0.88 (step-pop @p799 :rule scope :premises (@p798)) % 0.61/0.88 (step-pop @p800 :rule scope :premises (@p799)) % 0.61/0.88 (step-pop @p801 :rule scope :premises (@p800)) % 0.61/0.88 (step-pop @p802 :rule scope :premises (@p801)) % 0.61/0.88 (step-pop @p803 :rule scope :premises (@p802)) % 0.61/0.88 (step-pop @p804 :rule scope :premises (@p803)) % 0.61/0.88 (step-pop @p805 :rule scope :premises (@p804)) % 0.61/0.88 (step-pop @p806 :rule scope :premises (@p805)) % 0.61/0.88 (step-pop @p807 :rule scope :premises (@p806)) % 0.61/0.88 (step-pop @p808 :rule scope :premises (@p807)) % 0.61/0.88 (step-pop @p809 :rule scope :premises (@p808)) % 0.61/0.88 (step-pop @p810 :rule scope :premises (@p809)) % 0.61/0.88 (step-pop @p811 :rule scope :premises (@p810)) % 0.61/0.88 (step-pop @p812 :rule scope :premises (@p811)) % 0.61/0.88 (step-pop @p813 :rule scope :premises (@p812)) % 0.61/0.88 (step-pop @p814 :rule scope :premises (@p813)) % 0.61/0.88 (step-pop @p815 :rule scope :premises (@p814)) % 0.61/0.88 (step-pop @p816 :rule scope :premises (@p815)) % 0.61/0.88 (step-pop @p817 :rule scope :premises (@p816)) % 0.61/0.88 (step-pop @p818 :rule scope :premises (@p817)) % 0.61/0.88 (step-pop @p819 :rule scope :premises (@p818)) % 0.61/0.88 (step-pop @p820 :rule scope :premises (@p819)) % 0.61/0.88 (step-pop @p821 :rule scope :premises (@p820)) % 0.61/0.88 (step-pop @p822 :rule scope :premises (@p821)) % 0.61/0.88 (step-pop @p823 :rule scope :premises (@p822)) % 0.61/0.88 (step-pop @p824 :rule scope :premises (@p823)) % 0.61/0.88 (step-pop @p825 :rule scope :premises (@p824)) % 0.61/0.88 (step-pop @p826 :rule scope :premises (@p825)) % 0.61/0.88 (step-pop @p827 :rule scope :premises (@p826)) % 0.61/0.88 (step-pop @p828 :rule scope :premises (@p827)) % 0.61/0.88 (step-pop @p829 :rule scope :premises (@p828)) % 0.61/0.88 (step @p599 :rule process_scope :premises (@p829) :args (@t25)) % 0.61/0.88 (step @p675 :rule implies_elim :premises (@p599)) % 0.61/0.88 (step @p676 :rule cnf_and_neg :args (@t237)) % 0.61/0.88 (step @p677 :rule resolution :premises (@p676 @p675) :args (true @t237)) % 0.61/0.88 (step @p678 :rule reordering :premises (@p677) :args ((or @t25 (not @t61) (not @t62) (not @t63) (not @t64) (not @t65) (not @t66) (not @t67) (not @t68) (not @t69) (not @t70) (not @t71) (not @t72) (not @t73) (not @t74) (not @t75) (not @t78) (not @t80) (not @t83) (not @t86) (not @t89) (not @t92) (not @t95) (not @t98) (not @t101) (not @t104) (not @t107) (not @t110) (not @t113) (not @t115) (not @t116) (not @t118) (not @t122) (not @t125) (not @t127) (not @t130) (not @t133) (not @t136) (not @t138) (not @t140) (not @t142) (not @t144) (not @t146) (not @t148) (not @t151) (not @t154) (not @t155) (not @t158) (not @t161) (not @t163) (not @t165) (not @t166) (not @t168) (not @t172) (not @t176) (not @t179) (not @t182) (not @t184) (not @t187) (not @t189) (not @t191) (not @t193) (not @t195) (not @t197) (not @t199) (not @t202) (not @t205) (not @t208) (not @t211) (not @t215) (not @t216) (not @t218) (not @t219) (not @t221) (not @t223) (not @t225)))) % 0.61/0.88 (step @p679 false :rule chain_m_resolution :premises (@p678 @p100 @p99 @p98 @p97 @p96 @p95 @p94 @p93 @p92 @p91 @p90 @p89 @p88 @p87 @p86 @p85 @p84 @p83 @p82 @p81 @p80 @p79 @p78 @p77 @p76 @p75 @p74 @p73 @p72 @p71 @p67 @p66 @p65 @p64 @p63 @p62 @p61 @p60 @p59 @p58 @p57 @p56 @p55 @p54 @p53 @p52 @p51 @p47 @p46 @p45 @p44 @p43 @p42 @p41 @p40 @p39 @p38 @p37 @p36 @p35 @p19 @p34 @p33 @p32 @p31 @p30 @p29 @p28 @p27 @p26 @p25 @p24 @p23 @p22 @p21 @p20) :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 true false false false false false false false false false false false false false false false) (@list @t225 @t223 @t221 @t219 @t218 @t216 @t215 @t211 @t208 @t205 @t202 @t199 @t197 @t195 @t193 @t191 @t189 @t187 @t184 @t182 @t179 @t176 @t172 @t168 @t166 @t165 @t163 @t161 @t158 @t155 @t154 @t151 @t148 @t146 @t144 @t142 @t140 @t138 @t136 @t133 @t130 @t127 @t125 @t122 @t118 @t116 @t115 @t113 @t110 @t107 @t104 @t101 @t98 @t95 @t92 @t89 @t86 @t83 @t80 @t78 @t25 @t75 @t74 @t73 @t72 @t71 @t70 @t69 @t68 @t67 @t66 @t65 @t64 @t63 @t62 @t61))) % 0.61/0.88 ) % 0.61/0.88 % SZS output end Proof % 0.61/0.89 % cvc5 exiting %------------------------------------------------------------------------------