%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ALG198+1 : TPTP v9.2.1. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n005.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jun 3 08:05:29 AM UTC 2026 % Result : Theorem 0.42s 0.69s % Output : Proof 0.42s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.13 % Problem : ALG198+1 : TPTP v9.2.1. Released v2.7.0. % 0.12/0.14 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.16/0.35 % Computer : n005.cluster.edu % 0.16/0.35 % Model : x86_64 x86_64 % 0.16/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.35 % Memory : 8042.1875MB % 0.16/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.35 % CPULimit : 300 % 0.16/0.35 % WCLimit : 300 % 0.16/0.35 % DateTime : Wed Jun 3 01:41:03 EDT 2026 % 0.16/0.35 % CPUTime : % 0.39/0.57 %----Proving TF0_NAR, FOF, or CNF % 0.42/0.69 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 0.42/0.69 % SZS status Theorem % 0.42/0.69 % SZS output start Proof % 0.42/0.69 ( % 0.42/0.69 (declare-sort $$unsorted 0) % 0.42/0.69 (declare-const tptp.e0 $$unsorted) % 0.42/0.69 (declare-const tptp.e1 $$unsorted) % 0.42/0.69 (declare-const tptp.e2 $$unsorted) % 0.42/0.69 (declare-const tptp.e3 $$unsorted) % 0.42/0.69 (declare-const tptp.e4 $$unsorted) % 0.42/0.69 (declare-const tptp.e5 $$unsorted) % 0.42/0.69 (declare-const tptp.op (-> $$unsorted $$unsorted $$unsorted)) % 0.42/0.69 (declare-const tptp.e6 $$unsorted) % 0.42/0.69 (define @t1 () (tptp.op tptp.e6 tptp.e6)) % 0.42/0.69 (define @t2 () (= @t1 tptp.e6)) % 0.42/0.69 (define @t3 () (= @t1 tptp.e5)) % 0.42/0.69 (define @t4 () (= @t1 tptp.e4)) % 0.42/0.69 (define @t5 () (= @t1 tptp.e3)) % 0.42/0.69 (define @t6 () (= @t1 tptp.e2)) % 0.42/0.69 (define @t7 () (= @t1 tptp.e1)) % 0.42/0.69 (define @t8 () (= @t1 tptp.e0)) % 0.42/0.69 (define @t9 () (tptp.op tptp.e6 tptp.e5)) % 0.42/0.69 (define @t10 () (= @t9 tptp.e6)) % 0.42/0.69 (define @t11 () (= @t9 tptp.e5)) % 0.42/0.69 (define @t12 () (= @t9 tptp.e4)) % 0.42/0.69 (define @t13 () (= @t9 tptp.e3)) % 0.42/0.69 (define @t14 () (= @t9 tptp.e2)) % 0.42/0.69 (define @t15 () (= @t9 tptp.e1)) % 0.42/0.69 (define @t16 () (= @t9 tptp.e0)) % 0.42/0.69 (define @t17 () (tptp.op tptp.e6 tptp.e4)) % 0.42/0.69 (define @t18 () (= @t17 tptp.e6)) % 0.42/0.69 (define @t19 () (= @t17 tptp.e5)) % 0.42/0.69 (define @t20 () (= @t17 tptp.e4)) % 0.42/0.69 (define @t21 () (= @t17 tptp.e3)) % 0.42/0.69 (define @t22 () (= @t17 tptp.e2)) % 0.42/0.69 (define @t23 () (= @t17 tptp.e1)) % 0.42/0.69 (define @t24 () (= @t17 tptp.e0)) % 0.42/0.69 (define @t25 () (tptp.op tptp.e6 tptp.e3)) % 0.42/0.69 (define @t26 () (= @t25 tptp.e6)) % 0.42/0.69 (define @t27 () (= @t25 tptp.e5)) % 0.42/0.69 (define @t28 () (= @t25 tptp.e4)) % 0.42/0.69 (define @t29 () (= @t25 tptp.e3)) % 0.42/0.69 (define @t30 () (= @t25 tptp.e2)) % 0.42/0.69 (define @t31 () (= @t25 tptp.e1)) % 0.42/0.69 (define @t32 () (= @t25 tptp.e0)) % 0.42/0.69 (define @t33 () (tptp.op tptp.e6 tptp.e2)) % 0.42/0.69 (define @t34 () (= @t33 tptp.e6)) % 0.42/0.69 (define @t35 () (= @t33 tptp.e5)) % 0.42/0.69 (define @t36 () (= @t33 tptp.e4)) % 0.42/0.69 (define @t37 () (= @t33 tptp.e3)) % 0.42/0.69 (define @t38 () (= @t33 tptp.e2)) % 0.42/0.69 (define @t39 () (= @t33 tptp.e1)) % 0.42/0.69 (define @t40 () (= @t33 tptp.e0)) % 0.42/0.69 (define @t41 () (tptp.op tptp.e6 tptp.e1)) % 0.42/0.69 (define @t42 () (= @t41 tptp.e6)) % 0.42/0.69 (define @t43 () (= @t41 tptp.e5)) % 0.42/0.69 (define @t44 () (= @t41 tptp.e4)) % 0.42/0.69 (define @t45 () (= @t41 tptp.e3)) % 0.42/0.69 (define @t46 () (= @t41 tptp.e2)) % 0.42/0.69 (define @t47 () (= @t41 tptp.e1)) % 0.42/0.69 (define @t48 () (= @t41 tptp.e0)) % 0.42/0.69 (define @t49 () (tptp.op tptp.e6 tptp.e0)) % 0.42/0.69 (define @t50 () (= @t49 tptp.e6)) % 0.42/0.69 (define @t51 () (= @t49 tptp.e5)) % 0.42/0.69 (define @t52 () (= @t49 tptp.e4)) % 0.42/0.69 (define @t53 () (= @t49 tptp.e3)) % 0.42/0.69 (define @t54 () (= @t49 tptp.e2)) % 0.42/0.69 (define @t55 () (= @t49 tptp.e1)) % 0.42/0.69 (define @t56 () (= @t49 tptp.e0)) % 0.42/0.69 (define @t57 () (tptp.op tptp.e5 tptp.e6)) % 0.42/0.69 (define @t58 () (= @t57 tptp.e6)) % 0.42/0.69 (define @t59 () (= @t57 tptp.e5)) % 0.42/0.69 (define @t60 () (= @t57 tptp.e4)) % 0.42/0.69 (define @t61 () (= @t57 tptp.e3)) % 0.42/0.69 (define @t62 () (= @t57 tptp.e2)) % 0.42/0.69 (define @t63 () (= @t57 tptp.e1)) % 0.42/0.69 (define @t64 () (= @t57 tptp.e0)) % 0.42/0.69 (define @t65 () (tptp.op tptp.e5 tptp.e5)) % 0.42/0.69 (define @t66 () (= @t65 tptp.e6)) % 0.42/0.69 (define @t67 () (= @t65 tptp.e5)) % 0.42/0.69 (define @t68 () (= @t65 tptp.e4)) % 0.42/0.69 (define @t69 () (= @t65 tptp.e3)) % 0.42/0.69 (define @t70 () (= @t65 tptp.e2)) % 0.42/0.69 (define @t71 () (= @t65 tptp.e1)) % 0.42/0.69 (define @t72 () (= @t65 tptp.e0)) % 0.42/0.69 (define @t73 () (tptp.op tptp.e5 tptp.e4)) % 0.42/0.69 (define @t74 () (= @t73 tptp.e6)) % 0.42/0.69 (define @t75 () (= @t73 tptp.e5)) % 0.42/0.69 (define @t76 () (= @t73 tptp.e4)) % 0.42/0.69 (define @t77 () (= @t73 tptp.e3)) % 0.42/0.69 (define @t78 () (= @t73 tptp.e2)) % 0.42/0.69 (define @t79 () (= @t73 tptp.e1)) % 0.42/0.69 (define @t80 () (= @t73 tptp.e0)) % 0.42/0.69 (define @t81 () (tptp.op tptp.e5 tptp.e3)) % 0.42/0.69 (define @t82 () (= @t81 tptp.e6)) % 0.42/0.69 (define @t83 () (= @t81 tptp.e5)) % 0.42/0.69 (define @t84 () (= @t81 tptp.e4)) % 0.42/0.69 (define @t85 () (= @t81 tptp.e3)) % 0.42/0.69 (define @t86 () (= @t81 tptp.e2)) % 0.42/0.69 (define @t87 () (= @t81 tptp.e1)) % 0.42/0.69 (define @t88 () (= @t81 tptp.e0)) % 0.42/0.69 (define @t89 () (tptp.op tptp.e5 tptp.e2)) % 0.42/0.69 (define @t90 () (= @t89 tptp.e6)) % 0.42/0.69 (define @t91 () (= @t89 tptp.e5)) % 0.42/0.69 (define @t92 () (= @t89 tptp.e4)) % 0.42/0.69 (define @t93 () (= @t89 tptp.e3)) % 0.42/0.69 (define @t94 () (= @t89 tptp.e2)) % 0.42/0.69 (define @t95 () (= @t89 tptp.e1)) % 0.42/0.69 (define @t96 () (= @t89 tptp.e0)) % 0.42/0.69 (define @t97 () (tptp.op tptp.e5 tptp.e1)) % 0.42/0.69 (define @t98 () (= @t97 tptp.e6)) % 0.42/0.69 (define @t99 () (= @t97 tptp.e5)) % 0.42/0.69 (define @t100 () (= @t97 tptp.e4)) % 0.42/0.69 (define @t101 () (= @t97 tptp.e3)) % 0.42/0.69 (define @t102 () (= @t97 tptp.e2)) % 0.42/0.69 (define @t103 () (= @t97 tptp.e1)) % 0.42/0.69 (define @t104 () (= @t97 tptp.e0)) % 0.42/0.69 (define @t105 () (tptp.op tptp.e5 tptp.e0)) % 0.42/0.69 (define @t106 () (= @t105 tptp.e6)) % 0.42/0.69 (define @t107 () (= @t105 tptp.e5)) % 0.42/0.69 (define @t108 () (= @t105 tptp.e4)) % 0.42/0.69 (define @t109 () (= @t105 tptp.e3)) % 0.42/0.69 (define @t110 () (= @t105 tptp.e2)) % 0.42/0.69 (define @t111 () (= @t105 tptp.e1)) % 0.42/0.69 (define @t112 () (= @t105 tptp.e0)) % 0.42/0.69 (define @t113 () (tptp.op tptp.e4 tptp.e6)) % 0.42/0.69 (define @t114 () (= @t113 tptp.e6)) % 0.42/0.69 (define @t115 () (= @t113 tptp.e5)) % 0.42/0.69 (define @t116 () (= @t113 tptp.e4)) % 0.42/0.69 (define @t117 () (= @t113 tptp.e3)) % 0.42/0.69 (define @t118 () (= @t113 tptp.e2)) % 0.42/0.69 (define @t119 () (= @t113 tptp.e1)) % 0.42/0.69 (define @t120 () (= @t113 tptp.e0)) % 0.42/0.69 (define @t121 () (tptp.op tptp.e4 tptp.e5)) % 0.42/0.69 (define @t122 () (= @t121 tptp.e6)) % 0.42/0.69 (define @t123 () (= @t121 tptp.e5)) % 0.42/0.69 (define @t124 () (= @t121 tptp.e4)) % 0.42/0.69 (define @t125 () (= @t121 tptp.e3)) % 0.42/0.69 (define @t126 () (= @t121 tptp.e2)) % 0.42/0.69 (define @t127 () (= @t121 tptp.e1)) % 0.42/0.69 (define @t128 () (= @t121 tptp.e0)) % 0.42/0.69 (define @t129 () (tptp.op tptp.e4 tptp.e4)) % 0.42/0.69 (define @t130 () (= @t129 tptp.e6)) % 0.42/0.69 (define @t131 () (= @t129 tptp.e5)) % 0.42/0.69 (define @t132 () (= @t129 tptp.e4)) % 0.42/0.69 (define @t133 () (= @t129 tptp.e3)) % 0.42/0.69 (define @t134 () (= @t129 tptp.e2)) % 0.42/0.69 (define @t135 () (= @t129 tptp.e1)) % 0.42/0.69 (define @t136 () (= @t129 tptp.e0)) % 0.42/0.69 (define @t137 () (tptp.op tptp.e4 tptp.e3)) % 0.42/0.69 (define @t138 () (= @t137 tptp.e6)) % 0.42/0.69 (define @t139 () (= @t137 tptp.e5)) % 0.42/0.69 (define @t140 () (= @t137 tptp.e4)) % 0.42/0.69 (define @t141 () (= @t137 tptp.e3)) % 0.42/0.69 (define @t142 () (= @t137 tptp.e2)) % 0.42/0.69 (define @t143 () (= @t137 tptp.e1)) % 0.42/0.69 (define @t144 () (= @t137 tptp.e0)) % 0.42/0.69 (define @t145 () (tptp.op tptp.e4 tptp.e2)) % 0.42/0.69 (define @t146 () (= @t145 tptp.e6)) % 0.42/0.69 (define @t147 () (= @t145 tptp.e5)) % 0.42/0.69 (define @t148 () (= @t145 tptp.e4)) % 0.42/0.69 (define @t149 () (= @t145 tptp.e3)) % 0.42/0.69 (define @t150 () (= @t145 tptp.e2)) % 0.42/0.69 (define @t151 () (= @t145 tptp.e1)) % 0.42/0.69 (define @t152 () (= @t145 tptp.e0)) % 0.42/0.69 (define @t153 () (tptp.op tptp.e4 tptp.e1)) % 0.42/0.69 (define @t154 () (= @t153 tptp.e6)) % 0.42/0.69 (define @t155 () (= @t153 tptp.e5)) % 0.42/0.69 (define @t156 () (= @t153 tptp.e4)) % 0.42/0.69 (define @t157 () (= @t153 tptp.e3)) % 0.42/0.69 (define @t158 () (= @t153 tptp.e2)) % 0.42/0.69 (define @t159 () (= @t153 tptp.e1)) % 0.42/0.69 (define @t160 () (= @t153 tptp.e0)) % 0.42/0.69 (define @t161 () (tptp.op tptp.e4 tptp.e0)) % 0.42/0.69 (define @t162 () (= @t161 tptp.e6)) % 0.42/0.69 (define @t163 () (= @t161 tptp.e5)) % 0.42/0.69 (define @t164 () (= @t161 tptp.e4)) % 0.42/0.69 (define @t165 () (= @t161 tptp.e3)) % 0.42/0.69 (define @t166 () (= @t161 tptp.e2)) % 0.42/0.69 (define @t167 () (= @t161 tptp.e1)) % 0.42/0.69 (define @t168 () (= @t161 tptp.e0)) % 0.42/0.69 (define @t169 () (tptp.op tptp.e3 tptp.e6)) % 0.42/0.69 (define @t170 () (= @t169 tptp.e6)) % 0.42/0.69 (define @t171 () (= @t169 tptp.e5)) % 0.42/0.69 (define @t172 () (= @t169 tptp.e4)) % 0.42/0.69 (define @t173 () (= @t169 tptp.e3)) % 0.42/0.69 (define @t174 () (= @t169 tptp.e2)) % 0.42/0.69 (define @t175 () (= @t169 tptp.e1)) % 0.42/0.69 (define @t176 () (= @t169 tptp.e0)) % 0.42/0.69 (define @t177 () (tptp.op tptp.e3 tptp.e5)) % 0.42/0.69 (define @t178 () (= @t177 tptp.e6)) % 0.42/0.69 (define @t179 () (= @t177 tptp.e5)) % 0.42/0.69 (define @t180 () (= @t177 tptp.e4)) % 0.42/0.69 (define @t181 () (= @t177 tptp.e3)) % 0.42/0.69 (define @t182 () (= @t177 tptp.e2)) % 0.42/0.69 (define @t183 () (= @t177 tptp.e1)) % 0.42/0.69 (define @t184 () (= @t177 tptp.e0)) % 0.42/0.69 (define @t185 () (tptp.op tptp.e3 tptp.e4)) % 0.42/0.69 (define @t186 () (= @t185 tptp.e6)) % 0.42/0.69 (define @t187 () (= @t185 tptp.e5)) % 0.42/0.69 (define @t188 () (= @t185 tptp.e4)) % 0.42/0.69 (define @t189 () (= @t185 tptp.e3)) % 0.42/0.69 (define @t190 () (= @t185 tptp.e2)) % 0.42/0.69 (define @t191 () (= @t185 tptp.e1)) % 0.42/0.69 (define @t192 () (= @t185 tptp.e0)) % 0.42/0.69 (define @t193 () (tptp.op tptp.e3 tptp.e3)) % 0.42/0.69 (define @t194 () (= @t193 tptp.e6)) % 0.42/0.69 (define @t195 () (= @t193 tptp.e5)) % 0.42/0.69 (define @t196 () (= @t193 tptp.e4)) % 0.42/0.69 (define @t197 () (= @t193 tptp.e3)) % 0.42/0.69 (define @t198 () (= @t193 tptp.e2)) % 0.42/0.69 (define @t199 () (= @t193 tptp.e1)) % 0.42/0.69 (define @t200 () (= @t193 tptp.e0)) % 0.42/0.69 (define @t201 () (tptp.op tptp.e3 tptp.e2)) % 0.42/0.69 (define @t202 () (= @t201 tptp.e6)) % 0.42/0.69 (define @t203 () (= @t201 tptp.e5)) % 0.42/0.69 (define @t204 () (= @t201 tptp.e4)) % 0.42/0.69 (define @t205 () (= @t201 tptp.e3)) % 0.42/0.69 (define @t206 () (= @t201 tptp.e2)) % 0.42/0.69 (define @t207 () (= @t201 tptp.e1)) % 0.42/0.69 (define @t208 () (= @t201 tptp.e0)) % 0.42/0.69 (define @t209 () (tptp.op tptp.e3 tptp.e1)) % 0.42/0.69 (define @t210 () (= @t209 tptp.e6)) % 0.42/0.69 (define @t211 () (= @t209 tptp.e5)) % 0.42/0.69 (define @t212 () (= @t209 tptp.e4)) % 0.42/0.69 (define @t213 () (= @t209 tptp.e3)) % 0.42/0.69 (define @t214 () (= @t209 tptp.e2)) % 0.42/0.69 (define @t215 () (= @t209 tptp.e1)) % 0.42/0.69 (define @t216 () (= @t209 tptp.e0)) % 0.42/0.69 (define @t217 () (tptp.op tptp.e3 tptp.e0)) % 0.42/0.69 (define @t218 () (= @t217 tptp.e6)) % 0.42/0.69 (define @t219 () (= @t217 tptp.e5)) % 0.42/0.69 (define @t220 () (= @t217 tptp.e4)) % 0.42/0.69 (define @t221 () (= @t217 tptp.e3)) % 0.42/0.69 (define @t222 () (= @t217 tptp.e2)) % 0.42/0.69 (define @t223 () (= @t217 tptp.e1)) % 0.42/0.69 (define @t224 () (= @t217 tptp.e0)) % 0.42/0.69 (define @t225 () (tptp.op tptp.e2 tptp.e6)) % 0.42/0.69 (define @t226 () (= @t225 tptp.e6)) % 0.42/0.69 (define @t227 () (= @t225 tptp.e5)) % 0.42/0.69 (define @t228 () (= @t225 tptp.e4)) % 0.42/0.69 (define @t229 () (= @t225 tptp.e3)) % 0.42/0.69 (define @t230 () (= @t225 tptp.e2)) % 0.42/0.69 (define @t231 () (= @t225 tptp.e1)) % 0.42/0.69 (define @t232 () (= @t225 tptp.e0)) % 0.42/0.69 (define @t233 () (tptp.op tptp.e2 tptp.e5)) % 0.42/0.69 (define @t234 () (= @t233 tptp.e6)) % 0.42/0.69 (define @t235 () (= @t233 tptp.e5)) % 0.42/0.69 (define @t236 () (= @t233 tptp.e4)) % 0.42/0.69 (define @t237 () (= @t233 tptp.e3)) % 0.42/0.69 (define @t238 () (= @t233 tptp.e2)) % 0.42/0.69 (define @t239 () (= @t233 tptp.e1)) % 0.42/0.69 (define @t240 () (= @t233 tptp.e0)) % 0.42/0.69 (define @t241 () (tptp.op tptp.e2 tptp.e4)) % 0.42/0.69 (define @t242 () (= @t241 tptp.e6)) % 0.42/0.69 (define @t243 () (= @t241 tptp.e5)) % 0.42/0.69 (define @t244 () (= @t241 tptp.e4)) % 0.42/0.69 (define @t245 () (= @t241 tptp.e3)) % 0.42/0.69 (define @t246 () (= @t241 tptp.e2)) % 0.42/0.69 (define @t247 () (= @t241 tptp.e1)) % 0.42/0.69 (define @t248 () (= @t241 tptp.e0)) % 0.42/0.69 (define @t249 () (tptp.op tptp.e2 tptp.e3)) % 0.42/0.69 (define @t250 () (= @t249 tptp.e6)) % 0.42/0.69 (define @t251 () (= @t249 tptp.e5)) % 0.42/0.69 (define @t252 () (= @t249 tptp.e4)) % 0.42/0.69 (define @t253 () (= @t249 tptp.e3)) % 0.42/0.69 (define @t254 () (= @t249 tptp.e2)) % 0.42/0.69 (define @t255 () (= @t249 tptp.e1)) % 0.42/0.69 (define @t256 () (= @t249 tptp.e0)) % 0.42/0.69 (define @t257 () (tptp.op tptp.e2 tptp.e2)) % 0.42/0.69 (define @t258 () (= @t257 tptp.e6)) % 0.42/0.69 (define @t259 () (= @t257 tptp.e5)) % 0.42/0.69 (define @t260 () (= @t257 tptp.e4)) % 0.42/0.69 (define @t261 () (= @t257 tptp.e3)) % 0.42/0.69 (define @t262 () (= @t257 tptp.e2)) % 0.42/0.69 (define @t263 () (= @t257 tptp.e1)) % 0.42/0.69 (define @t264 () (= @t257 tptp.e0)) % 0.42/0.69 (define @t265 () (tptp.op tptp.e2 tptp.e1)) % 0.42/0.69 (define @t266 () (= @t265 tptp.e6)) % 0.42/0.69 (define @t267 () (= @t265 tptp.e5)) % 0.42/0.69 (define @t268 () (= @t265 tptp.e4)) % 0.42/0.69 (define @t269 () (= @t265 tptp.e3)) % 0.42/0.69 (define @t270 () (= @t265 tptp.e2)) % 0.42/0.69 (define @t271 () (= @t265 tptp.e1)) % 0.42/0.69 (define @t272 () (= @t265 tptp.e0)) % 0.42/0.69 (define @t273 () (tptp.op tptp.e2 tptp.e0)) % 0.42/0.69 (define @t274 () (= @t273 tptp.e6)) % 0.42/0.69 (define @t275 () (= @t273 tptp.e5)) % 0.42/0.69 (define @t276 () (= @t273 tptp.e4)) % 0.42/0.69 (define @t277 () (= @t273 tptp.e3)) % 0.42/0.69 (define @t278 () (= @t273 tptp.e2)) % 0.42/0.69 (define @t279 () (= @t273 tptp.e1)) % 0.42/0.69 (define @t280 () (= @t273 tptp.e0)) % 0.42/0.69 (define @t281 () (tptp.op tptp.e1 tptp.e6)) % 0.42/0.69 (define @t282 () (= @t281 tptp.e6)) % 0.42/0.69 (define @t283 () (= @t281 tptp.e5)) % 0.42/0.69 (define @t284 () (= @t281 tptp.e4)) % 0.42/0.69 (define @t285 () (= @t281 tptp.e3)) % 0.42/0.69 (define @t286 () (= @t281 tptp.e2)) % 0.42/0.69 (define @t287 () (= @t281 tptp.e1)) % 0.42/0.69 (define @t288 () (= @t281 tptp.e0)) % 0.42/0.69 (define @t289 () (tptp.op tptp.e1 tptp.e5)) % 0.42/0.69 (define @t290 () (= @t289 tptp.e6)) % 0.42/0.69 (define @t291 () (= @t289 tptp.e5)) % 0.42/0.69 (define @t292 () (= @t289 tptp.e4)) % 0.42/0.69 (define @t293 () (= @t289 tptp.e3)) % 0.42/0.69 (define @t294 () (= @t289 tptp.e2)) % 0.42/0.69 (define @t295 () (= @t289 tptp.e1)) % 0.42/0.69 (define @t296 () (= @t289 tptp.e0)) % 0.42/0.69 (define @t297 () (tptp.op tptp.e1 tptp.e4)) % 0.42/0.69 (define @t298 () (= @t297 tptp.e6)) % 0.42/0.69 (define @t299 () (= @t297 tptp.e5)) % 0.42/0.69 (define @t300 () (= @t297 tptp.e4)) % 0.42/0.69 (define @t301 () (= @t297 tptp.e3)) % 0.42/0.69 (define @t302 () (= @t297 tptp.e2)) % 0.42/0.69 (define @t303 () (= @t297 tptp.e1)) % 0.42/0.69 (define @t304 () (= @t297 tptp.e0)) % 0.42/0.69 (define @t305 () (tptp.op tptp.e1 tptp.e3)) % 0.42/0.69 (define @t306 () (= @t305 tptp.e6)) % 0.42/0.69 (define @t307 () (= @t305 tptp.e5)) % 0.42/0.69 (define @t308 () (= @t305 tptp.e4)) % 0.42/0.69 (define @t309 () (= @t305 tptp.e3)) % 0.42/0.69 (define @t310 () (= @t305 tptp.e2)) % 0.42/0.69 (define @t311 () (= @t305 tptp.e1)) % 0.42/0.69 (define @t312 () (= @t305 tptp.e0)) % 0.42/0.69 (define @t313 () (tptp.op tptp.e1 tptp.e2)) % 0.42/0.69 (define @t314 () (= @t313 tptp.e6)) % 0.42/0.69 (define @t315 () (= @t313 tptp.e5)) % 0.42/0.69 (define @t316 () (= @t313 tptp.e4)) % 0.42/0.69 (define @t317 () (= @t313 tptp.e3)) % 0.42/0.69 (define @t318 () (= @t313 tptp.e2)) % 0.42/0.69 (define @t319 () (= @t313 tptp.e1)) % 0.42/0.69 (define @t320 () (= @t313 tptp.e0)) % 0.42/0.69 (define @t321 () (tptp.op tptp.e1 tptp.e1)) % 0.42/0.69 (define @t322 () (= @t321 tptp.e6)) % 0.42/0.69 (define @t323 () (= @t321 tptp.e5)) % 0.42/0.69 (define @t324 () (= @t321 tptp.e4)) % 0.42/0.69 (define @t325 () (= @t321 tptp.e3)) % 0.42/0.69 (define @t326 () (= @t321 tptp.e2)) % 0.42/0.69 (define @t327 () (= @t321 tptp.e1)) % 0.42/0.69 (define @t328 () (= @t321 tptp.e0)) % 0.42/0.69 (define @t329 () (tptp.op tptp.e1 tptp.e0)) % 0.42/0.69 (define @t330 () (= @t329 tptp.e6)) % 0.42/0.69 (define @t331 () (= @t329 tptp.e5)) % 0.42/0.69 (define @t332 () (= @t329 tptp.e4)) % 0.42/0.69 (define @t333 () (= @t329 tptp.e3)) % 0.42/0.69 (define @t334 () (= @t329 tptp.e2)) % 0.42/0.69 (define @t335 () (= @t329 tptp.e1)) % 0.42/0.69 (define @t336 () (= @t329 tptp.e0)) % 0.42/0.69 (define @t337 () (tptp.op tptp.e0 tptp.e6)) % 0.42/0.69 (define @t338 () (= @t337 tptp.e6)) % 0.42/0.69 (define @t339 () (= @t337 tptp.e5)) % 0.42/0.69 (define @t340 () (= @t337 tptp.e4)) % 0.42/0.69 (define @t341 () (= @t337 tptp.e3)) % 0.42/0.69 (define @t342 () (= @t337 tptp.e2)) % 0.42/0.69 (define @t343 () (= @t337 tptp.e1)) % 0.42/0.69 (define @t344 () (= @t337 tptp.e0)) % 0.42/0.69 (define @t345 () (tptp.op tptp.e0 tptp.e5)) % 0.42/0.69 (define @t346 () (= @t345 tptp.e6)) % 0.42/0.69 (define @t347 () (= @t345 tptp.e5)) % 0.42/0.69 (define @t348 () (= @t345 tptp.e4)) % 0.42/0.69 (define @t349 () (= @t345 tptp.e3)) % 0.42/0.69 (define @t350 () (= @t345 tptp.e2)) % 0.42/0.69 (define @t351 () (= @t345 tptp.e1)) % 0.42/0.69 (define @t352 () (= @t345 tptp.e0)) % 0.42/0.69 (define @t353 () (tptp.op tptp.e0 tptp.e4)) % 0.42/0.69 (define @t354 () (= @t353 tptp.e6)) % 0.42/0.69 (define @t355 () (= @t353 tptp.e5)) % 0.42/0.69 (define @t356 () (= @t353 tptp.e4)) % 0.42/0.69 (define @t357 () (= @t353 tptp.e3)) % 0.42/0.69 (define @t358 () (= @t353 tptp.e2)) % 0.42/0.69 (define @t359 () (= @t353 tptp.e1)) % 0.42/0.69 (define @t360 () (= @t353 tptp.e0)) % 0.42/0.69 (define @t361 () (tptp.op tptp.e0 tptp.e3)) % 0.42/0.69 (define @t362 () (= @t361 tptp.e6)) % 0.42/0.69 (define @t363 () (= @t361 tptp.e5)) % 0.42/0.69 (define @t364 () (= @t361 tptp.e4)) % 0.42/0.69 (define @t365 () (= @t361 tptp.e3)) % 0.42/0.69 (define @t366 () (= @t361 tptp.e2)) % 0.42/0.69 (define @t367 () (= @t361 tptp.e1)) % 0.42/0.69 (define @t368 () (= @t361 tptp.e0)) % 0.42/0.69 (define @t369 () (tptp.op tptp.e0 tptp.e2)) % 0.42/0.69 (define @t370 () (= @t369 tptp.e6)) % 0.42/0.69 (define @t371 () (= @t369 tptp.e5)) % 0.42/0.69 (define @t372 () (= @t369 tptp.e4)) % 0.42/0.69 (define @t373 () (= @t369 tptp.e3)) % 0.42/0.69 (define @t374 () (= @t369 tptp.e2)) % 0.42/0.69 (define @t375 () (= @t369 tptp.e1)) % 0.42/0.69 (define @t376 () (= @t369 tptp.e0)) % 0.42/0.69 (define @t377 () (tptp.op tptp.e0 tptp.e1)) % 0.42/0.69 (define @t378 () (= @t377 tptp.e6)) % 0.42/0.69 (define @t379 () (= @t377 tptp.e5)) % 0.42/0.69 (define @t380 () (= @t377 tptp.e4)) % 0.42/0.69 (define @t381 () (= @t377 tptp.e3)) % 0.42/0.69 (define @t382 () (= @t377 tptp.e2)) % 0.42/0.69 (define @t383 () (= @t377 tptp.e1)) % 0.42/0.69 (define @t384 () (= @t377 tptp.e0)) % 0.42/0.69 (define @t385 () (tptp.op tptp.e0 tptp.e0)) % 0.42/0.69 (define @t386 () (= @t385 tptp.e6)) % 0.42/0.69 (define @t387 () (= @t385 tptp.e5)) % 0.42/0.69 (define @t388 () (= @t385 tptp.e4)) % 0.42/0.69 (define @t389 () (= @t385 tptp.e3)) % 0.42/0.69 (define @t390 () (= @t385 tptp.e2)) % 0.42/0.69 (define @t391 () (= @t385 tptp.e1)) % 0.42/0.69 (define @t392 () (= @t385 tptp.e0)) % 0.42/0.69 (define @t393 () (tptp.op tptp.e5 @t65)) % 0.42/0.69 (define @t394 () (tptp.op @t393 @t393)) % 0.42/0.69 (define @t395 () (tptp.op @t394 tptp.e5)) % 0.42/0.69 (define @t396 () (not @t2)) % 0.42/0.69 (define @t397 () (not @t67)) % 0.42/0.69 (define @t398 () (not @t132)) % 0.42/0.69 (define @t399 () (not @t197)) % 0.42/0.69 (define @t400 () (not @t262)) % 0.42/0.69 (define @t401 () (not @t327)) % 0.42/0.69 (define @t402 () (not @t392)) % 0.42/0.69 (define @t403 () (and @t402 @t401 @t400 @t399 @t398 @t397 @t396 @t392 @t327 @t262 @t197 @t132 @t67 @t2)) % 0.42/0.69 (assume @p1 (and (or @t392 @t391 @t390 @t389 @t388 @t387 @t386) (or @t384 @t383 @t382 @t381 @t380 @t379 @t378) (or @t376 @t375 @t374 @t373 @t372 @t371 @t370) (or @t368 @t367 @t366 @t365 @t364 @t363 @t362) (or @t360 @t359 @t358 @t357 @t356 @t355 @t354) (or @t352 @t351 @t350 @t349 @t348 @t347 @t346) (or @t344 @t343 @t342 @t341 @t340 @t339 @t338) (or @t336 @t335 @t334 @t333 @t332 @t331 @t330) (or @t328 @t327 @t326 @t325 @t324 @t323 @t322) (or @t320 @t319 @t318 @t317 @t316 @t315 @t314) (or @t312 @t311 @t310 @t309 @t308 @t307 @t306) (or @t304 @t303 @t302 @t301 @t300 @t299 @t298) (or @t296 @t295 @t294 @t293 @t292 @t291 @t290) (or @t288 @t287 @t286 @t285 @t284 @t283 @t282) (or @t280 @t279 @t278 @t277 @t276 @t275 @t274) (or @t272 @t271 @t270 @t269 @t268 @t267 @t266) (or @t264 @t263 @t262 @t261 @t260 @t259 @t258) (or @t256 @t255 @t254 @t253 @t252 @t251 @t250) (or @t248 @t247 @t246 @t245 @t244 @t243 @t242) (or @t240 @t239 @t238 @t237 @t236 @t235 @t234) (or @t232 @t231 @t230 @t229 @t228 @t227 @t226) (or @t224 @t223 @t222 @t221 @t220 @t219 @t218) (or @t216 @t215 @t214 @t213 @t212 @t211 @t210) (or @t208 @t207 @t206 @t205 @t204 @t203 @t202) (or @t200 @t199 @t198 @t197 @t196 @t195 @t194) (or @t192 @t191 @t190 @t189 @t188 @t187 @t186) (or @t184 @t183 @t182 @t181 @t180 @t179 @t178) (or @t176 @t175 @t174 @t173 @t172 @t171 @t170) (or @t168 @t167 @t166 @t165 @t164 @t163 @t162) (or @t160 @t159 @t158 @t157 @t156 @t155 @t154) (or @t152 @t151 @t150 @t149 @t148 @t147 @t146) (or @t144 @t143 @t142 @t141 @t140 @t139 @t138) (or @t136 @t135 @t134 @t133 @t132 @t131 @t130) (or @t128 @t127 @t126 @t125 @t124 @t123 @t122) (or @t120 @t119 @t118 @t117 @t116 @t115 @t114) (or @t112 @t111 @t110 @t109 @t108 @t107 @t106) (or @t104 @t103 @t102 @t101 @t100 @t99 @t98) (or @t96 @t95 @t94 @t93 @t92 @t91 @t90) (or @t88 @t87 @t86 @t85 @t84 @t83 @t82) (or @t80 @t79 @t78 @t77 @t76 @t75 @t74) (or @t72 @t71 @t70 @t69 @t68 @t67 @t66) (or @t64 @t63 @t62 @t61 @t60 @t59 @t58) (or @t56 @t55 @t54 @t53 @t52 @t51 @t50) (or @t48 @t47 @t46 @t45 @t44 @t43 @t42) (or @t40 @t39 @t38 @t37 @t36 @t35 @t34) (or @t32 @t31 @t30 @t29 @t28 @t27 @t26) (or @t24 @t23 @t22 @t21 @t20 @t19 @t18) (or @t16 @t15 @t14 @t13 @t12 @t11 @t10) (or @t8 @t7 @t6 @t5 @t4 @t3 @t2))) % 0.42/0.69 (assume @p2 (and (or @t392 @t384 @t376 @t368 @t360 @t352 @t344) (or @t392 @t336 @t280 @t224 @t168 @t112 @t56) (or @t391 @t383 @t375 @t367 @t359 @t351 @t343) (or @t391 @t335 @t279 @t223 @t167 @t111 @t55) (or @t390 @t382 @t374 @t366 @t358 @t350 @t342) (or @t390 @t334 @t278 @t222 @t166 @t110 @t54) (or @t389 @t381 @t373 @t365 @t357 @t349 @t341) (or @t389 @t333 @t277 @t221 @t165 @t109 @t53) (or @t388 @t380 @t372 @t364 @t356 @t348 @t340) (or @t388 @t332 @t276 @t220 @t164 @t108 @t52) (or @t387 @t379 @t371 @t363 @t355 @t347 @t339) (or @t387 @t331 @t275 @t219 @t163 @t107 @t51) (or @t386 @t378 @t370 @t362 @t354 @t346 @t338) (or @t386 @t330 @t274 @t218 @t162 @t106 @t50) (or @t336 @t328 @t320 @t312 @t304 @t296 @t288) (or @t384 @t328 @t272 @t216 @t160 @t104 @t48) (or @t335 @t327 @t319 @t311 @t303 @t295 @t287) (or @t383 @t327 @t271 @t215 @t159 @t103 @t47) (or @t334 @t326 @t318 @t310 @t302 @t294 @t286) (or @t382 @t326 @t270 @t214 @t158 @t102 @t46) (or @t333 @t325 @t317 @t309 @t301 @t293 @t285) (or @t381 @t325 @t269 @t213 @t157 @t101 @t45) (or @t332 @t324 @t316 @t308 @t300 @t292 @t284) (or @t380 @t324 @t268 @t212 @t156 @t100 @t44) (or @t331 @t323 @t315 @t307 @t299 @t291 @t283) (or @t379 @t323 @t267 @t211 @t155 @t99 @t43) (or @t330 @t322 @t314 @t306 @t298 @t290 @t282) (or @t378 @t322 @t266 @t210 @t154 @t98 @t42) (or @t280 @t272 @t264 @t256 @t248 @t240 @t232) (or @t376 @t320 @t264 @t208 @t152 @t96 @t40) (or @t279 @t271 @t263 @t255 @t247 @t239 @t231) (or @t375 @t319 @t263 @t207 @t151 @t95 @t39) (or @t278 @t270 @t262 @t254 @t246 @t238 @t230) (or @t374 @t318 @t262 @t206 @t150 @t94 @t38) (or @t277 @t269 @t261 @t253 @t245 @t237 @t229) (or @t373 @t317 @t261 @t205 @t149 @t93 @t37) (or @t276 @t268 @t260 @t252 @t244 @t236 @t228) (or @t372 @t316 @t260 @t204 @t148 @t92 @t36) (or @t275 @t267 @t259 @t251 @t243 @t235 @t227) (or @t371 @t315 @t259 @t203 @t147 @t91 @t35) (or @t274 @t266 @t258 @t250 @t242 @t234 @t226) (or @t370 @t314 @t258 @t202 @t146 @t90 @t34) (or @t224 @t216 @t208 @t200 @t192 @t184 @t176) (or @t368 @t312 @t256 @t200 @t144 @t88 @t32) (or @t223 @t215 @t207 @t199 @t191 @t183 @t175) (or @t367 @t311 @t255 @t199 @t143 @t87 @t31) (or @t222 @t214 @t206 @t198 @t190 @t182 @t174) (or @t366 @t310 @t254 @t198 @t142 @t86 @t30) (or @t221 @t213 @t205 @t197 @t189 @t181 @t173) (or @t365 @t309 @t253 @t197 @t141 @t85 @t29) (or @t220 @t212 @t204 @t196 @t188 @t180 @t172) (or @t364 @t308 @t252 @t196 @t140 @t84 @t28) (or @t219 @t211 @t203 @t195 @t187 @t179 @t171) (or @t363 @t307 @t251 @t195 @t139 @t83 @t27) (or @t218 @t210 @t202 @t194 @t186 @t178 @t170) (or @t362 @t306 @t250 @t194 @t138 @t82 @t26) (or @t168 @t160 @t152 @t144 @t136 @t128 @t120) (or @t360 @t304 @t248 @t192 @t136 @t80 @t24) (or @t167 @t159 @t151 @t143 @t135 @t127 @t119) (or @t359 @t303 @t247 @t191 @t135 @t79 @t23) (or @t166 @t158 @t150 @t142 @t134 @t126 @t118) (or @t358 @t302 @t246 @t190 @t134 @t78 @t22) (or @t165 @t157 @t149 @t141 @t133 @t125 @t117) (or @t357 @t301 @t245 @t189 @t133 @t77 @t21) (or @t164 @t156 @t148 @t140 @t132 @t124 @t116) (or @t356 @t300 @t244 @t188 @t132 @t76 @t20) (or @t163 @t155 @t147 @t139 @t131 @t123 @t115) (or @t355 @t299 @t243 @t187 @t131 @t75 @t19) (or @t162 @t154 @t146 @t138 @t130 @t122 @t114) (or @t354 @t298 @t242 @t186 @t130 @t74 @t18) (or @t112 @t104 @t96 @t88 @t80 @t72 @t64) (or @t352 @t296 @t240 @t184 @t128 @t72 @t16) (or @t111 @t103 @t95 @t87 @t79 @t71 @t63) (or @t351 @t295 @t239 @t183 @t127 @t71 @t15) (or @t110 @t102 @t94 @t86 @t78 @t70 @t62) (or @t350 @t294 @t238 @t182 @t126 @t70 @t14) (or @t109 @t101 @t93 @t85 @t77 @t69 @t61) (or @t349 @t293 @t237 @t181 @t125 @t69 @t13) (or @t108 @t100 @t92 @t84 @t76 @t68 @t60) (or @t348 @t292 @t236 @t180 @t124 @t68 @t12) (or @t107 @t99 @t91 @t83 @t75 @t67 @t59) (or @t347 @t291 @t235 @t179 @t123 @t67 @t11) (or @t106 @t98 @t90 @t82 @t74 @t66 @t58) (or @t346 @t290 @t234 @t178 @t122 @t66 @t10) (or @t56 @t48 @t40 @t32 @t24 @t16 @t8) (or @t344 @t288 @t232 @t176 @t120 @t64 @t8) (or @t55 @t47 @t39 @t31 @t23 @t15 @t7) (or @t343 @t287 @t231 @t175 @t119 @t63 @t7) (or @t54 @t46 @t38 @t30 @t22 @t14 @t6) (or @t342 @t286 @t230 @t174 @t118 @t62 @t6) (or @t53 @t45 @t37 @t29 @t21 @t13 @t5) (or @t341 @t285 @t229 @t173 @t117 @t61 @t5) (or @t52 @t44 @t36 @t28 @t20 @t12 @t4) (or @t340 @t284 @t228 @t172 @t116 @t60 @t4) (or @t51 @t43 @t35 @t27 @t19 @t11 @t3) (or @t339 @t283 @t227 @t171 @t115 @t59 @t3) (or @t50 @t42 @t34 @t26 @t18 @t10 @t2) (or @t338 @t282 @t226 @t170 @t114 @t58 @t2))) % 0.42/0.69 (assume @p3 (and (= (tptp.op (tptp.op @t385 tptp.e0) tptp.e0) tptp.e0) (= (tptp.op (tptp.op @t329 tptp.e1) tptp.e1) tptp.e0) (= (tptp.op (tptp.op @t273 tptp.e2) tptp.e2) tptp.e0) (= (tptp.op (tptp.op @t217 tptp.e3) tptp.e3) tptp.e0) (= (tptp.op (tptp.op @t161 tptp.e4) tptp.e4) tptp.e0) (= (tptp.op (tptp.op @t105 tptp.e5) tptp.e5) tptp.e0) (= (tptp.op (tptp.op @t49 tptp.e6) tptp.e6) tptp.e0) (= (tptp.op (tptp.op @t377 tptp.e0) tptp.e0) tptp.e1) (= (tptp.op (tptp.op @t321 tptp.e1) tptp.e1) tptp.e1) (= (tptp.op (tptp.op @t265 tptp.e2) tptp.e2) tptp.e1) (= (tptp.op (tptp.op @t209 tptp.e3) tptp.e3) tptp.e1) (= (tptp.op (tptp.op @t153 tptp.e4) tptp.e4) tptp.e1) (= (tptp.op (tptp.op @t97 tptp.e5) tptp.e5) tptp.e1) (= (tptp.op (tptp.op @t41 tptp.e6) tptp.e6) tptp.e1) (= (tptp.op (tptp.op @t369 tptp.e0) tptp.e0) tptp.e2) (= (tptp.op (tptp.op @t313 tptp.e1) tptp.e1) tptp.e2) (= (tptp.op (tptp.op @t257 tptp.e2) tptp.e2) tptp.e2) (= (tptp.op (tptp.op @t201 tptp.e3) tptp.e3) tptp.e2) (= (tptp.op (tptp.op @t145 tptp.e4) tptp.e4) tptp.e2) (= (tptp.op (tptp.op @t89 tptp.e5) tptp.e5) tptp.e2) (= (tptp.op (tptp.op @t33 tptp.e6) tptp.e6) tptp.e2) (= (tptp.op (tptp.op @t361 tptp.e0) tptp.e0) tptp.e3) (= (tptp.op (tptp.op @t305 tptp.e1) tptp.e1) tptp.e3) (= (tptp.op (tptp.op @t249 tptp.e2) tptp.e2) tptp.e3) (= (tptp.op (tptp.op @t193 tptp.e3) tptp.e3) tptp.e3) (= (tptp.op (tptp.op @t137 tptp.e4) tptp.e4) tptp.e3) (= (tptp.op (tptp.op @t81 tptp.e5) tptp.e5) tptp.e3) (= (tptp.op (tptp.op @t25 tptp.e6) tptp.e6) tptp.e3) (= (tptp.op (tptp.op @t353 tptp.e0) tptp.e0) tptp.e4) (= (tptp.op (tptp.op @t297 tptp.e1) tptp.e1) tptp.e4) (= (tptp.op (tptp.op @t241 tptp.e2) tptp.e2) tptp.e4) (= (tptp.op (tptp.op @t185 tptp.e3) tptp.e3) tptp.e4) (= (tptp.op (tptp.op @t129 tptp.e4) tptp.e4) tptp.e4) (= (tptp.op (tptp.op @t73 tptp.e5) tptp.e5) tptp.e4) (= (tptp.op (tptp.op @t17 tptp.e6) tptp.e6) tptp.e4) (= (tptp.op (tptp.op @t345 tptp.e0) tptp.e0) tptp.e5) (= (tptp.op (tptp.op @t289 tptp.e1) tptp.e1) tptp.e5) (= (tptp.op (tptp.op @t233 tptp.e2) tptp.e2) tptp.e5) (= (tptp.op (tptp.op @t177 tptp.e3) tptp.e3) tptp.e5) (= (tptp.op (tptp.op @t121 tptp.e4) tptp.e4) tptp.e5) (= (tptp.op (tptp.op @t65 tptp.e5) tptp.e5) tptp.e5) (= (tptp.op (tptp.op @t9 tptp.e6) tptp.e6) tptp.e5) (= (tptp.op (tptp.op @t337 tptp.e0) tptp.e0) tptp.e6) (= (tptp.op (tptp.op @t281 tptp.e1) tptp.e1) tptp.e6) (= (tptp.op (tptp.op @t225 tptp.e2) tptp.e2) tptp.e6) (= (tptp.op (tptp.op @t169 tptp.e3) tptp.e3) tptp.e6) (= (tptp.op (tptp.op @t113 tptp.e4) tptp.e4) tptp.e6) (= (tptp.op (tptp.op @t57 tptp.e5) tptp.e5) tptp.e6) (= (tptp.op (tptp.op @t1 tptp.e6) tptp.e6) tptp.e6))) % 0.42/0.69 (assume @p4 (and (not (= @t385 @t329)) (not (= @t385 @t273)) (not (= @t385 @t217)) (not (= @t385 @t161)) (not (= @t385 @t105)) (not (= @t385 @t49)) (not (= @t329 @t273)) (not (= @t329 @t217)) (not (= @t329 @t161)) (not (= @t329 @t105)) (not (= @t329 @t49)) (not (= @t273 @t217)) (not (= @t273 @t161)) (not (= @t273 @t105)) (not (= @t273 @t49)) (not (= @t217 @t161)) (not (= @t217 @t105)) (not (= @t217 @t49)) (not (= @t161 @t105)) (not (= @t161 @t49)) (not (= @t105 @t49)) (not (= @t377 @t321)) (not (= @t377 @t265)) (not (= @t377 @t209)) (not (= @t377 @t153)) (not (= @t377 @t97)) (not (= @t377 @t41)) (not (= @t321 @t265)) (not (= @t321 @t209)) (not (= @t321 @t153)) (not (= @t321 @t97)) (not (= @t321 @t41)) (not (= @t265 @t209)) (not (= @t265 @t153)) (not (= @t265 @t97)) (not (= @t265 @t41)) (not (= @t209 @t153)) (not (= @t209 @t97)) (not (= @t209 @t41)) (not (= @t153 @t97)) (not (= @t153 @t41)) (not (= @t97 @t41)) (not (= @t369 @t313)) (not (= @t369 @t257)) (not (= @t369 @t201)) (not (= @t369 @t145)) (not (= @t369 @t89)) (not (= @t369 @t33)) (not (= @t313 @t257)) (not (= @t313 @t201)) (not (= @t313 @t145)) (not (= @t313 @t89)) (not (= @t313 @t33)) (not (= @t257 @t201)) (not (= @t257 @t145)) (not (= @t257 @t89)) (not (= @t257 @t33)) (not (= @t201 @t145)) (not (= @t201 @t89)) (not (= @t201 @t33)) (not (= @t145 @t89)) (not (= @t145 @t33)) (not (= @t89 @t33)) (not (= @t361 @t305)) (not (= @t361 @t249)) (not (= @t361 @t193)) (not (= @t361 @t137)) (not (= @t361 @t81)) (not (= @t361 @t25)) (not (= @t305 @t249)) (not (= @t305 @t193)) (not (= @t305 @t137)) (not (= @t305 @t81)) (not (= @t305 @t25)) (not (= @t249 @t193)) (not (= @t249 @t137)) (not (= @t249 @t81)) (not (= @t249 @t25)) (not (= @t193 @t137)) (not (= @t193 @t81)) (not (= @t193 @t25)) (not (= @t137 @t81)) (not (= @t137 @t25)) (not (= @t81 @t25)) (not (= @t353 @t297)) (not (= @t353 @t241)) (not (= @t353 @t185)) (not (= @t353 @t129)) (not (= @t353 @t73)) (not (= @t353 @t17)) (not (= @t297 @t241)) (not (= @t297 @t185)) (not (= @t297 @t129)) (not (= @t297 @t73)) (not (= @t297 @t17)) (not (= @t241 @t185)) (not (= @t241 @t129)) (not (= @t241 @t73)) (not (= @t241 @t17)) (not (= @t185 @t129)) (not (= @t185 @t73)) (not (= @t185 @t17)) (not (= @t129 @t73)) (not (= @t129 @t17)) (not (= @t73 @t17)) (not (= @t345 @t289)) (not (= @t345 @t233)) (not (= @t345 @t177)) (not (= @t345 @t121)) (not (= @t345 @t65)) (not (= @t345 @t9)) (not (= @t289 @t233)) (not (= @t289 @t177)) (not (= @t289 @t121)) (not (= @t289 @t65)) (not (= @t289 @t9)) (not (= @t233 @t177)) (not (= @t233 @t121)) (not (= @t233 @t65)) (not (= @t233 @t9)) (not (= @t177 @t121)) (not (= @t177 @t65)) (not (= @t177 @t9)) (not (= @t121 @t65)) (not (= @t121 @t9)) (not (= @t65 @t9)) (not (= @t337 @t281)) (not (= @t337 @t225)) (not (= @t337 @t169)) (not (= @t337 @t113)) (not (= @t337 @t57)) (not (= @t337 @t1)) (not (= @t281 @t225)) (not (= @t281 @t169)) (not (= @t281 @t113)) (not (= @t281 @t57)) (not (= @t281 @t1)) (not (= @t225 @t169)) (not (= @t225 @t113)) (not (= @t225 @t57)) (not (= @t225 @t1)) (not (= @t169 @t113)) (not (= @t169 @t57)) (not (= @t169 @t1)) (not (= @t113 @t57)) (not (= @t113 @t1)) (not (= @t57 @t1)) (not (= @t385 @t377)) (not (= @t385 @t369)) (not (= @t385 @t361)) (not (= @t385 @t353)) (not (= @t385 @t345)) (not (= @t385 @t337)) (not (= @t377 @t369)) (not (= @t377 @t361)) (not (= @t377 @t353)) (not (= @t377 @t345)) (not (= @t377 @t337)) (not (= @t369 @t361)) (not (= @t369 @t353)) (not (= @t369 @t345)) (not (= @t369 @t337)) (not (= @t361 @t353)) (not (= @t361 @t345)) (not (= @t361 @t337)) (not (= @t353 @t345)) (not (= @t353 @t337)) (not (= @t345 @t337)) (not (= @t329 @t321)) (not (= @t329 @t313)) (not (= @t329 @t305)) (not (= @t329 @t297)) (not (= @t329 @t289)) (not (= @t329 @t281)) (not (= @t321 @t313)) (not (= @t321 @t305)) (not (= @t321 @t297)) (not (= @t321 @t289)) (not (= @t321 @t281)) (not (= @t313 @t305)) (not (= @t313 @t297)) (not (= @t313 @t289)) (not (= @t313 @t281)) (not (= @t305 @t297)) (not (= @t305 @t289)) (not (= @t305 @t281)) (not (= @t297 @t289)) (not (= @t297 @t281)) (not (= @t289 @t281)) (not (= @t273 @t265)) (not (= @t273 @t257)) (not (= @t273 @t249)) (not (= @t273 @t241)) (not (= @t273 @t233)) (not (= @t273 @t225)) (not (= @t265 @t257)) (not (= @t265 @t249)) (not (= @t265 @t241)) (not (= @t265 @t233)) (not (= @t265 @t225)) (not (= @t257 @t249)) (not (= @t257 @t241)) (not (= @t257 @t233)) (not (= @t257 @t225)) (not (= @t249 @t241)) (not (= @t249 @t233)) (not (= @t249 @t225)) (not (= @t241 @t233)) (not (= @t241 @t225)) (not (= @t233 @t225)) (not (= @t217 @t209)) (not (= @t217 @t201)) (not (= @t217 @t193)) (not (= @t217 @t185)) (not (= @t217 @t177)) (not (= @t217 @t169)) (not (= @t209 @t201)) (not (= @t209 @t193)) (not (= @t209 @t185)) (not (= @t209 @t177)) (not (= @t209 @t169)) (not (= @t201 @t193)) (not (= @t201 @t185)) (not (= @t201 @t177)) (not (= @t201 @t169)) (not (= @t193 @t185)) (not (= @t193 @t177)) (not (= @t193 @t169)) (not (= @t185 @t177)) (not (= @t185 @t169)) (not (= @t177 @t169)) (not (= @t161 @t153)) (not (= @t161 @t145)) (not (= @t161 @t137)) (not (= @t161 @t129)) (not (= @t161 @t121)) (not (= @t161 @t113)) (not (= @t153 @t145)) (not (= @t153 @t137)) (not (= @t153 @t129)) (not (= @t153 @t121)) (not (= @t153 @t113)) (not (= @t145 @t137)) (not (= @t145 @t129)) (not (= @t145 @t121)) (not (= @t145 @t113)) (not (= @t137 @t129)) (not (= @t137 @t121)) (not (= @t137 @t113)) (not (= @t129 @t121)) (not (= @t129 @t113)) (not (= @t121 @t113)) (not (= @t105 @t97)) (not (= @t105 @t89)) (not (= @t105 @t81)) (not (= @t105 @t73)) (not (= @t105 @t65)) (not (= @t105 @t57)) (not (= @t97 @t89)) (not (= @t97 @t81)) (not (= @t97 @t73)) (not (= @t97 @t65)) (not (= @t97 @t57)) (not (= @t89 @t81)) (not (= @t89 @t73)) (not (= @t89 @t65)) (not (= @t89 @t57)) (not (= @t81 @t73)) (not (= @t81 @t65)) (not (= @t81 @t57)) (not (= @t73 @t65)) (not (= @t73 @t57)) (not (= @t65 @t57)) (not (= @t49 @t41)) (not (= @t49 @t33)) (not (= @t49 @t25)) (not (= @t49 @t17)) (not (= @t49 @t9)) (not (= @t49 @t1)) (not (= @t41 @t33)) (not (= @t41 @t25)) (not (= @t41 @t17)) (not (= @t41 @t9)) (not (= @t41 @t1)) (not (= @t33 @t25)) (not (= @t33 @t17)) (not (= @t33 @t9)) (not (= @t33 @t1)) (not (= @t25 @t17)) (not (= @t25 @t9)) (not (= @t25 @t1)) (not (= @t17 @t9)) (not (= @t17 @t1)) (not (= @t9 @t1)))) % 0.42/0.69 (assume @p5 (and (not (= tptp.e0 tptp.e1)) (not (= tptp.e0 tptp.e2)) (not (= tptp.e0 tptp.e3)) (not (= tptp.e0 tptp.e4)) (not (= tptp.e0 tptp.e5)) (not (= tptp.e0 tptp.e6)) (not (= tptp.e1 tptp.e2)) (not (= tptp.e1 tptp.e3)) (not (= tptp.e1 tptp.e4)) (not (= tptp.e1 tptp.e5)) (not (= tptp.e1 tptp.e6)) (not (= tptp.e2 tptp.e3)) (not (= tptp.e2 tptp.e4)) (not (= tptp.e2 tptp.e5)) (not (= tptp.e2 tptp.e6)) (not (= tptp.e3 tptp.e4)) (not (= tptp.e3 tptp.e5)) (not (= tptp.e3 tptp.e6)) (not (= tptp.e4 tptp.e5)) (not (= tptp.e4 tptp.e6)) (not (= tptp.e5 tptp.e6)))) % 0.42/0.69 (assume @p6 (and (= tptp.e0 (tptp.op @t394 @t393)) (= tptp.e1 @t65) (= tptp.e2 @t394) (= tptp.e3 @t395) (= tptp.e4 @t393) (= tptp.e6 (tptp.op @t395 @t393)))) % 0.42/0.69 (assume @p7 (not (not @t403))) % 0.42/0.69 (assume @p8 true) % 0.42/0.69 (step @p9 :rule eq-symm :args (@t1 tptp.e6)) % 0.42/0.69 (step @p10 :rule eq-symm :args (@t65 tptp.e5)) % 0.42/0.69 (step @p11 :rule eq-symm :args (@t129 tptp.e4)) % 0.42/0.69 (step @p12 :rule eq-symm :args (@t193 tptp.e3)) % 0.42/0.69 (step @p13 :rule eq-symm :args (@t257 tptp.e2)) % 0.42/0.69 (step @p14 :rule eq-symm :args (@t321 tptp.e1)) % 0.42/0.69 (step @p15 :rule eq-symm :args (@t385 tptp.e0)) % 0.42/0.69 (step @p16 :rule cong :premises (@p9) :args (@t396)) % 0.42/0.69 (step @p17 :rule cong :premises (@p10) :args (@t397)) % 0.42/0.69 (step @p18 :rule cong :premises (@p11) :args (@t398)) % 0.42/0.69 (step @p19 :rule cong :premises (@p12) :args (@t399)) % 0.42/0.69 (step @p20 :rule cong :premises (@p13) :args (@t400)) % 0.42/0.69 (step @p21 :rule cong :premises (@p14) :args (@t401)) % 0.42/0.69 (step @p22 :rule cong :premises (@p15) :args (@t402)) % 0.42/0.69 (step @p23 :rule nary_cong :premises (@p22 @p21 @p20 @p19 @p18 @p17 @p16 @p15 @p14 @p13 @p12 @p11 @p10 @p9) :args (@t403)) % 0.42/0.69 (step @p24 :rule bool-double-not-elim :args (@t403)) % 0.42/0.69 (step @p25 :rule trans :premises (@p24 @p23)) % 0.42/0.69 (step @p26 :rule eq_resolve :premises (@p7 @p25)) % 0.42/0.69 (step @p27 :rule and_elim :premises (@p26) :args (0)) % 0.42/0.69 (step @p28 :rule and_elim :premises (@p26) :args (7)) % 0.42/0.69 (step @p29 false :rule chain_m_resolution :premises (@p28 @p27) :args (false (@list true) (@list (= tptp.e0 @t385)))) % 0.42/0.69 ) % 0.42/0.69 % SZS output end Proof % 0.42/0.69 % cvc5 exiting %------------------------------------------------------------------------------