%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : PUZ028-5 : TPTP v9.2.1. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n015.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:43:59 AM UTC 2026 % Result : Unsatisfiable 0.46s 0.63s % Output : Proof 0.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : PUZ028-5 : TPTP v9.2.1. Released v2.0.0. % 0.11/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.16/0.34 % Computer : n015.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Tue Jun 2 13:13:04 EDT 2026 % 0.16/0.35 % CPUTime : % 0.28/0.50 %----Proving TF0_NAR, FOF, or CNF % 0.28/0.51 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 0.46/0.63 % SZS status Unsatisfiable % 0.46/0.63 % SZS output start Proof % 0.46/0.64 ( % 0.46/0.64 (declare-sort $$unsorted 0) % 0.46/0.64 (declare-const tptp.familiar (-> $$unsorted $$unsorted Bool)) % 0.46/0.64 (declare-const tptp.after (-> $$unsorted $$unsorted Bool)) % 0.46/0.64 (declare-const tptp.six $$unsorted) % 0.46/0.64 (declare-const tptp.five $$unsorted) % 0.46/0.64 (declare-const tptp.two $$unsorted) % 0.46/0.64 (declare-const tptp.not_familiar (-> $$unsorted $$unsorted Bool)) % 0.46/0.64 (declare-const tptp.four $$unsorted) % 0.46/0.64 (declare-const tptp.person (-> $$unsorted Bool)) % 0.46/0.64 (declare-const tptp.three $$unsorted) % 0.46/0.64 (declare-const tptp.one $$unsorted) % 0.46/0.64 (define @t1 () (tptp.person tptp.one)) % 0.46/0.64 (define @t2 () (tptp.person tptp.two)) % 0.46/0.64 (define @t3 () (tptp.person tptp.three)) % 0.46/0.64 (define @t4 () (tptp.person tptp.four)) % 0.46/0.64 (define @t5 () (tptp.person tptp.five)) % 0.46/0.64 (define @t6 () (tptp.person tptp.six)) % 0.46/0.64 (define @t7 () (tptp.after tptp.one tptp.two)) % 0.46/0.64 (define @t8 () (tptp.after tptp.two tptp.three)) % 0.46/0.64 (define @t9 () (tptp.after tptp.three tptp.four)) % 0.46/0.64 (define @t10 () (tptp.after tptp.four tptp.five)) % 0.46/0.64 (define @t11 () (tptp.after tptp.five tptp.six)) % 0.46/0.64 (define @t12 () (@var "Small" $$unsorted)) % 0.46/0.64 (define @t13 () (@var "Medium" $$unsorted)) % 0.46/0.64 (define @t14 () (@var "Large" $$unsorted)) % 0.46/0.64 (define @t15 () (forall (@list @t14 @t12 @t13) (or (tptp.after @t14 @t12) (not (tptp.after @t14 @t13)) (not (tptp.after @t13 @t12))))) % 0.46/0.64 (define @t16 () (@var "Y" $$unsorted)) % 0.46/0.64 (define @t17 () (@var "X" $$unsorted)) % 0.46/0.64 (define @t18 () (forall (@list @t17 @t16) (or (tptp.familiar @t17 @t16) (tptp.not_familiar @t17 @t16) (not (tptp.person @t17)) (not (tptp.person @t16)) (not (tptp.after @t17 @t16))))) % 0.46/0.64 (define @t19 () (@var "X3" $$unsorted)) % 0.46/0.64 (define @t20 () (@var "X1" $$unsorted)) % 0.46/0.64 (define @t21 () (@var "X2" $$unsorted)) % 0.46/0.64 (define @t22 () (@list @t20 @t21 @t19)) % 0.46/0.64 (define @t23 () (forall @t22 (or (not (tptp.familiar @t20 @t21)) (not (tptp.familiar @t21 @t19)) (not (tptp.familiar @t20 @t19))))) % 0.46/0.64 (define @t24 () (forall @t22 (or (not (tptp.not_familiar @t20 @t21)) (not (tptp.not_familiar @t21 @t19)) (not (tptp.not_familiar @t20 @t19))))) % 0.46/0.64 (define @t25 () (not @t8)) % 0.46/0.64 (define @t26 () (not @t7)) % 0.46/0.64 (define @t27 () (tptp.after tptp.one tptp.three)) % 0.46/0.64 (define @t28 () (or @t27 @t26 @t25)) % 0.46/0.64 (define @t29 () (@list false false false)) % 0.46/0.64 (define @t30 () (not @t9)) % 0.46/0.64 (define @t31 () (not @t27)) % 0.46/0.64 (define @t32 () (tptp.after tptp.one tptp.four)) % 0.46/0.64 (define @t33 () (or @t32 @t31 @t30)) % 0.46/0.64 (define @t34 () (not @t11)) % 0.46/0.64 (define @t35 () (not @t10)) % 0.46/0.64 (define @t36 () (tptp.after tptp.four tptp.six)) % 0.46/0.64 (define @t37 () (or @t36 @t35 @t34)) % 0.46/0.64 (define @t38 () (not @t36)) % 0.46/0.64 (define @t39 () (tptp.after tptp.three tptp.six)) % 0.46/0.64 (define @t40 () (or @t39 @t30 @t38)) % 0.46/0.64 (define @t41 () (@list tptp.three tptp.four tptp.five)) % 0.46/0.64 (define @t42 () (tptp.after tptp.three tptp.five)) % 0.46/0.64 (define @t43 () (or @t42 @t30 @t35)) % 0.46/0.64 (define @t44 () (tptp.after tptp.two tptp.four)) % 0.46/0.64 (define @t45 () (or @t44 @t25 @t30)) % 0.46/0.64 (define @t46 () (not @t44)) % 0.46/0.64 (define @t47 () (tptp.after tptp.two tptp.five)) % 0.46/0.64 (define @t48 () (or @t47 @t46 @t35)) % 0.46/0.64 (define @t49 () (@list tptp.one tptp.three tptp.six)) % 0.46/0.64 (define @t50 () (tptp.familiar tptp.one tptp.six)) % 0.46/0.64 (define @t51 () (not @t50)) % 0.46/0.64 (define @t52 () (tptp.familiar tptp.three tptp.six)) % 0.46/0.64 (define @t53 () (not @t52)) % 0.46/0.64 (define @t54 () (tptp.familiar tptp.one tptp.three)) % 0.46/0.64 (define @t55 () (not @t54)) % 0.46/0.64 (define @t56 () (or @t55 @t53 @t51)) % 0.46/0.64 (define @t57 () (@list tptp.one tptp.six tptp.five)) % 0.46/0.64 (define @t58 () (tptp.after tptp.one tptp.five)) % 0.46/0.64 (define @t59 () (not @t58)) % 0.46/0.64 (define @t60 () (tptp.after tptp.one tptp.six)) % 0.46/0.64 (define @t61 () (or @t60 @t59 @t34)) % 0.46/0.64 (define @t62 () (@list tptp.one tptp.five tptp.four)) % 0.46/0.64 (define @t63 () (not @t32)) % 0.46/0.64 (define @t64 () (or @t58 @t63 @t35)) % 0.46/0.64 (define @t65 () (@list tptp.one tptp.six)) % 0.46/0.64 (define @t66 () (not @t60)) % 0.46/0.64 (define @t67 () (not @t6)) % 0.46/0.64 (define @t68 () (not @t1)) % 0.46/0.64 (define @t69 () (tptp.not_familiar tptp.one tptp.six)) % 0.46/0.64 (define @t70 () (or @t50 @t69 @t68 @t67 @t66)) % 0.46/0.64 (define @t71 () (@list tptp.one tptp.three tptp.five)) % 0.46/0.64 (define @t72 () (tptp.familiar tptp.one tptp.five)) % 0.46/0.64 (define @t73 () (not @t72)) % 0.46/0.64 (define @t74 () (tptp.familiar tptp.three tptp.five)) % 0.46/0.64 (define @t75 () (not @t74)) % 0.46/0.64 (define @t76 () (or @t55 @t75 @t73)) % 0.46/0.64 (define @t77 () (@list tptp.three tptp.five tptp.six)) % 0.46/0.64 (define @t78 () (tptp.familiar tptp.five tptp.six)) % 0.46/0.64 (define @t79 () (not @t78)) % 0.46/0.64 (define @t80 () (or @t75 @t79 @t53)) % 0.46/0.64 (define @t81 () (not @t5)) % 0.46/0.64 (define @t82 () (tptp.not_familiar tptp.one tptp.five)) % 0.46/0.64 (define @t83 () (or @t72 @t82 @t68 @t81 @t59)) % 0.46/0.64 (define @t84 () (tptp.not_familiar tptp.five tptp.six)) % 0.46/0.64 (define @t85 () (or @t78 @t84 @t81 @t67 @t34)) % 0.46/0.64 (define @t86 () (@list tptp.one tptp.five tptp.six)) % 0.46/0.64 (define @t87 () (not @t69)) % 0.46/0.64 (define @t88 () (not @t84)) % 0.46/0.64 (define @t89 () (not @t82)) % 0.46/0.64 (define @t90 () (or @t89 @t88 @t87)) % 0.46/0.64 (define @t91 () (@list false false false false false false false false false false false true false true false false false false false false false false false false false false false false false false false false false false true false false)) % 0.46/0.64 (define @t92 () (not @t42)) % 0.46/0.64 (define @t93 () (not @t3)) % 0.46/0.64 (define @t94 () (tptp.not_familiar tptp.three tptp.five)) % 0.46/0.64 (define @t95 () (or @t74 @t94 @t93 @t81 @t92)) % 0.46/0.64 (define @t96 () (@list tptp.two tptp.three tptp.six)) % 0.46/0.64 (define @t97 () (tptp.familiar tptp.two tptp.six)) % 0.46/0.64 (define @t98 () (not @t97)) % 0.46/0.64 (define @t99 () (tptp.familiar tptp.two tptp.three)) % 0.46/0.64 (define @t100 () (not @t99)) % 0.46/0.64 (define @t101 () (or @t100 @t53 @t98)) % 0.46/0.64 (define @t102 () (@list tptp.one tptp.two tptp.three)) % 0.46/0.64 (define @t103 () (tptp.familiar tptp.one tptp.two)) % 0.46/0.64 (define @t104 () (not @t103)) % 0.46/0.64 (define @t105 () (or @t104 @t100 @t55)) % 0.46/0.64 (define @t106 () (not @t47)) % 0.46/0.64 (define @t107 () (tptp.after tptp.two tptp.six)) % 0.46/0.64 (define @t108 () (or @t107 @t106 @t34)) % 0.46/0.64 (define @t109 () (not @t107)) % 0.46/0.64 (define @t110 () (not @t2)) % 0.46/0.64 (define @t111 () (tptp.not_familiar tptp.two tptp.six)) % 0.46/0.64 (define @t112 () (or @t97 @t111 @t110 @t67 @t109)) % 0.46/0.64 (define @t113 () (tptp.not_familiar tptp.one tptp.two)) % 0.46/0.64 (define @t114 () (or @t103 @t113 @t68 @t110 @t26)) % 0.46/0.64 (define @t115 () (@list tptp.one tptp.two tptp.six)) % 0.46/0.64 (define @t116 () (not @t111)) % 0.46/0.64 (define @t117 () (not @t113)) % 0.46/0.64 (define @t118 () (or @t117 @t116 @t87)) % 0.46/0.64 (define @t119 () (tptp.not_familiar tptp.two tptp.three)) % 0.46/0.64 (define @t120 () (or @t99 @t119 @t110 @t93 @t25)) % 0.46/0.64 (define @t121 () (@list tptp.two tptp.three tptp.five)) % 0.46/0.64 (define @t122 () (tptp.not_familiar tptp.two tptp.five)) % 0.46/0.64 (define @t123 () (not @t122)) % 0.46/0.64 (define @t124 () (not @t94)) % 0.46/0.64 (define @t125 () (not @t119)) % 0.46/0.64 (define @t126 () (or @t125 @t124 @t123)) % 0.46/0.64 (define @t127 () (tptp.familiar tptp.two tptp.five)) % 0.46/0.64 (define @t128 () (or @t127 @t122 @t110 @t81 @t106)) % 0.46/0.64 (define @t129 () (@list tptp.two tptp.four tptp.five)) % 0.46/0.64 (define @t130 () (not @t127)) % 0.46/0.64 (define @t131 () (tptp.familiar tptp.four tptp.five)) % 0.46/0.64 (define @t132 () (not @t131)) % 0.46/0.64 (define @t133 () (tptp.familiar tptp.two tptp.four)) % 0.46/0.64 (define @t134 () (not @t133)) % 0.46/0.64 (define @t135 () (or @t134 @t132 @t130)) % 0.46/0.64 (define @t136 () (not @t4)) % 0.46/0.64 (define @t137 () (tptp.not_familiar tptp.four tptp.five)) % 0.46/0.64 (define @t138 () (or @t131 @t137 @t136 @t81 @t35)) % 0.46/0.64 (define @t139 () (not @t137)) % 0.46/0.64 (define @t140 () (tptp.not_familiar tptp.three tptp.four)) % 0.46/0.64 (define @t141 () (not @t140)) % 0.46/0.64 (define @t142 () (or @t141 @t139 @t124)) % 0.46/0.64 (define @t143 () (tptp.familiar tptp.three tptp.four)) % 0.46/0.64 (define @t144 () (or @t143 @t140 @t93 @t136 @t30)) % 0.46/0.64 (define @t145 () (@list tptp.three tptp.four tptp.six)) % 0.46/0.64 (define @t146 () (tptp.familiar tptp.four tptp.six)) % 0.46/0.64 (define @t147 () (not @t146)) % 0.46/0.64 (define @t148 () (not @t143)) % 0.46/0.64 (define @t149 () (or @t148 @t147 @t53)) % 0.46/0.64 (define @t150 () (@list tptp.one tptp.three tptp.four)) % 0.46/0.64 (define @t151 () (tptp.familiar tptp.one tptp.four)) % 0.46/0.64 (define @t152 () (not @t151)) % 0.46/0.64 (define @t153 () (or @t55 @t148 @t152)) % 0.46/0.64 (define @t154 () (tptp.not_familiar tptp.four tptp.six)) % 0.46/0.64 (define @t155 () (or @t146 @t154 @t136 @t67 @t38)) % 0.46/0.64 (define @t156 () (tptp.not_familiar tptp.one tptp.four)) % 0.46/0.64 (define @t157 () (or @t151 @t156 @t68 @t136 @t63)) % 0.46/0.64 (define @t158 () (@list tptp.one tptp.four tptp.six)) % 0.46/0.64 (define @t159 () (not @t154)) % 0.46/0.64 (define @t160 () (not @t156)) % 0.46/0.64 (define @t161 () (or @t160 @t159 @t87)) % 0.46/0.64 (define @t162 () (not @t39)) % 0.46/0.64 (define @t163 () (tptp.not_familiar tptp.three tptp.six)) % 0.46/0.64 (define @t164 () (or @t52 @t163 @t93 @t67 @t162)) % 0.46/0.64 (define @t165 () (not @t163)) % 0.46/0.64 (define @t166 () (or @t125 @t165 @t116)) % 0.46/0.64 (define @t167 () (or @t141 @t159 @t165)) % 0.46/0.64 (define @t168 () (@list tptp.two tptp.four tptp.six)) % 0.46/0.64 (define @t169 () (or @t134 @t147 @t98)) % 0.46/0.64 (define @t170 () (@list false false false false false false false false false false false true false true false)) % 0.46/0.64 (define @t171 () (@list tptp.two tptp.five tptp.six)) % 0.46/0.64 (define @t172 () (or @t130 @t79 @t98)) % 0.46/0.64 (define @t173 () (@list tptp.four tptp.five tptp.six)) % 0.46/0.64 (define @t174 () (or @t139 @t88 @t159)) % 0.46/0.64 (define @t175 () (@list false false false false false false false false false false false true false true false false false false false false false false false false false true false false)) % 0.46/0.64 (define @t176 () (or @t148 @t132 @t75)) % 0.46/0.64 (define @t177 () (@list tptp.one tptp.four tptp.five)) % 0.46/0.64 (define @t178 () (or @t160 @t139 @t89)) % 0.46/0.64 (define @t179 () (@list tptp.two tptp.three tptp.four)) % 0.46/0.64 (define @t180 () (or @t100 @t148 @t134)) % 0.46/0.64 (define @t181 () (or @t152 @t147 @t51)) % 0.46/0.64 (define @t182 () (or @t132 @t79 @t147)) % 0.46/0.64 (define @t183 () (or @t123 @t88 @t116)) % 0.46/0.64 (define @t184 () (@list tptp.two tptp.four)) % 0.46/0.64 (define @t185 () (tptp.not_familiar tptp.two tptp.four)) % 0.46/0.64 (define @t186 () (or @t133 @t185 @t110 @t136 @t46)) % 0.46/0.64 (define @t187 () (@list tptp.one tptp.two tptp.four)) % 0.46/0.64 (define @t188 () (not @t185)) % 0.46/0.64 (define @t189 () (or @t117 @t188 @t160)) % 0.46/0.64 (define @t190 () (@list false false false false false false false false false false false true false true false false false false false false false false false false false false false false true false false)) % 0.46/0.64 (define @t191 () (or @t124 @t88 @t165)) % 0.46/0.64 (define @t192 () (or @t125 @t141 @t188)) % 0.46/0.64 (define @t193 () (or @t152 @t132 @t73)) % 0.46/0.64 (define @t194 () (or @t188 @t139 @t123)) % 0.46/0.64 (define @t195 () (or @t100 @t75 @t130)) % 0.46/0.64 (define @t196 () (tptp.not_familiar tptp.one tptp.three)) % 0.46/0.64 (define @t197 () (or @t54 @t196 @t68 @t93 @t31)) % 0.46/0.64 (define @t198 () (@list false false true false false)) % 0.46/0.64 (define @t199 () (not @t196)) % 0.46/0.64 (define @t200 () (or @t199 @t165 @t87)) % 0.46/0.64 (define @t201 () (or @t199 @t141 @t160)) % 0.46/0.64 (define @t202 () (or @t199 @t124 @t89)) % 0.46/0.64 (define @t203 () (or @t73 @t79 @t51)) % 0.46/0.64 (define @t204 () (or @t188 @t159 @t116)) % 0.46/0.64 (define @t205 () (or @t117 @t125 @t199)) % 0.46/0.64 (define @t206 () (@list tptp.one tptp.two tptp.five)) % 0.46/0.64 (define @t207 () (or @t104 @t130 @t73)) % 0.46/0.64 (define @t208 () (or @t117 @t123 @t89)) % 0.46/0.64 (define @t209 () (or @t104 @t98 @t51)) % 0.46/0.64 (define @t210 () (@list false false false true false)) % 0.46/0.64 (define @t211 () (or @t104 @t134 @t152)) % 0.46/0.64 (assume @p1 @t1) % 0.46/0.64 (assume @p2 @t2) % 0.46/0.64 (assume @p3 @t3) % 0.46/0.64 (assume @p4 @t4) % 0.46/0.64 (assume @p5 @t5) % 0.46/0.64 (assume @p6 @t6) % 0.46/0.64 (assume @p7 @t7) % 0.46/0.64 (assume @p8 @t8) % 0.46/0.64 (assume @p9 @t9) % 0.46/0.64 (assume @p10 @t10) % 0.46/0.64 (assume @p11 @t11) % 0.46/0.64 (assume @p12 @t15) % 0.46/0.64 (assume @p13 @t18) % 0.46/0.64 (assume @p14 @t23) % 0.46/0.64 (assume @p15 @t24) % 0.46/0.64 (step @p16 :rule instantiate :premises (@p13) :args ((@list tptp.one tptp.four))) % 0.46/0.64 (step @p17 :rule instantiate :premises (@p12) :args ((@list tptp.one tptp.four tptp.three))) % 0.46/0.64 (step @p18 :rule instantiate :premises (@p12) :args ((@list tptp.one tptp.three tptp.two))) % 0.46/0.64 (step @p19 :rule cnf_or_pos :args (@t28)) % 0.46/0.64 (step @p20 :rule reordering :premises (@p19) :args ((or @t26 @t25 @t27 (not @t28)))) % 0.46/0.64 (step @p21 :rule chain_m_resolution :premises (@p20 @p7 @p8 @p18) :args (@t27 @t29 (@list @t7 @t8 @t28))) % 0.46/0.64 (step @p22 :rule cnf_or_pos :args (@t33)) % 0.46/0.64 (step @p23 :rule reordering :premises (@p22) :args ((or @t30 @t31 @t32 (not @t33)))) % 0.46/0.64 (step @p24 :rule chain_m_resolution :premises (@p23 @p9 @p21 @p17) :args (@t32 @t29 (@list @t9 @t27 @t33))) % 0.46/0.64 (step @p25 :rule instantiate :premises (@p13) :args ((@list tptp.three tptp.six))) % 0.46/0.64 (step @p26 :rule instantiate :premises (@p12) :args ((@list tptp.three tptp.six tptp.four))) % 0.46/0.64 (step @p27 :rule instantiate :premises (@p12) :args ((@list tptp.four tptp.six tptp.five))) % 0.46/0.64 (step @p28 :rule cnf_or_pos :args (@t37)) % 0.46/0.64 (step @p29 :rule reordering :premises (@p28) :args ((or @t35 @t34 @t36 (not @t37)))) % 0.46/0.64 (step @p30 :rule chain_m_resolution :premises (@p29 @p10 @p11 @p27) :args (@t36 @t29 (@list @t10 @t11 @t37))) % 0.46/0.64 (step @p31 :rule cnf_or_pos :args (@t40)) % 0.46/0.64 (step @p32 :rule reordering :premises (@p31) :args ((or @t30 @t38 @t39 (not @t40)))) % 0.46/0.64 (step @p33 :rule chain_m_resolution :premises (@p32 @p9 @p30 @p26) :args (@t39 @t29 (@list @t9 @t36 @t40))) % 0.46/0.64 (step @p34 :rule instantiate :premises (@p13) :args ((@list tptp.three tptp.four))) % 0.46/0.64 (step @p35 :rule instantiate :premises (@p15) :args (@t41)) % 0.46/0.64 (step @p36 :rule instantiate :premises (@p13) :args ((@list tptp.three tptp.five))) % 0.46/0.64 (step @p37 :rule instantiate :premises (@p12) :args ((@list tptp.three tptp.five tptp.four))) % 0.46/0.64 (step @p38 :rule cnf_or_pos :args (@t43)) % 0.46/0.64 (step @p39 :rule reordering :premises (@p38) :args ((or @t30 @t35 @t42 (not @t43)))) % 0.46/0.64 (step @p40 :rule chain_m_resolution :premises (@p39 @p9 @p10 @p37) :args (@t42 @t29 (@list @t9 @t10 @t43))) % 0.46/0.64 (step @p41 :rule instantiate :premises (@p13) :args ((@list tptp.two tptp.five))) % 0.46/0.64 (step @p42 :rule instantiate :premises (@p12) :args ((@list tptp.two tptp.five tptp.four))) % 0.46/0.64 (step @p43 :rule instantiate :premises (@p12) :args ((@list tptp.two tptp.four tptp.three))) % 0.46/0.64 (step @p44 :rule cnf_or_pos :args (@t45)) % 0.46/0.64 (step @p45 :rule reordering :premises (@p44) :args ((or @t25 @t30 @t44 (not @t45)))) % 0.46/0.64 (step @p46 :rule chain_m_resolution :premises (@p45 @p8 @p9 @p43) :args (@t44 @t29 (@list @t8 @t9 @t45))) % 0.46/0.64 (step @p47 :rule cnf_or_pos :args (@t48)) % 0.46/0.64 (step @p48 :rule reordering :premises (@p47) :args ((or @t35 @t46 @t47 (not @t48)))) % 0.46/0.64 (step @p49 :rule chain_m_resolution :premises (@p48 @p10 @p46 @p42) :args (@t47 @t29 (@list @t10 @t44 @t48))) % 0.46/0.64 (step @p50 :rule instantiate :premises (@p13) :args ((@list tptp.four tptp.five))) % 0.46/0.64 (step @p51 :rule instantiate :premises (@p13) :args ((@list tptp.one tptp.three))) % 0.46/0.64 (step @p52 :rule instantiate :premises (@p14) :args (@t49)) % 0.46/0.64 (step @p53 :rule cnf_or_pos :args (@t56)) % 0.46/0.64 (step @p54 :rule reordering :premises (@p53) :args ((or @t55 @t53 @t51 (not @t56)))) % 0.46/0.64 (assume-push @p386 @t23) % 0.46/0.64 (step-pop @p387 :rule scope :premises (@p52)) % 0.46/0.64 (step @p56 :rule process_scope :premises (@p387) :args (@t56)) % 0.46/0.64 (step @p58 :rule implies_elim :premises (@p56)) % 0.46/0.64 (assume-push @p388 @t15) % 0.46/0.64 (step @p60 :rule instantiate :premises (@p12) :args (@t57)) % 0.46/0.64 (step-pop @p389 :rule scope :premises (@p60)) % 0.46/0.64 (step @p61 :rule process_scope :premises (@p389) :args (@t61)) % 0.46/0.64 (step @p63 :rule implies_elim :premises (@p61)) % 0.46/0.64 (assume-push @p390 @t15) % 0.46/0.64 (step @p65 :rule instantiate :premises (@p12) :args (@t62)) % 0.46/0.64 (step-pop @p391 :rule scope :premises (@p65)) % 0.46/0.64 (step @p66 :rule process_scope :premises (@p391) :args (@t64)) % 0.46/0.64 (step @p68 :rule implies_elim :premises (@p66)) % 0.46/0.64 (assume-push @p392 @t15) % 0.46/0.64 (step-pop @p393 :rule scope :premises (@p17)) % 0.46/0.64 (step @p70 :rule process_scope :premises (@p393) :args (@t33)) % 0.46/0.64 (step @p72 :rule implies_elim :premises (@p70)) % 0.46/0.64 (assume-push @p394 @t15) % 0.46/0.64 (step-pop @p395 :rule scope :premises (@p18)) % 0.46/0.64 (step @p74 :rule process_scope :premises (@p395) :args (@t28)) % 0.46/0.64 (step @p76 :rule implies_elim :premises (@p74)) % 0.46/0.64 (step @p77 :rule cnf_or_pos :args (@t64)) % 0.46/0.64 (step @p78 :rule reordering :premises (@p77) :args ((or @t35 @t63 @t58 (not @t64)))) % 0.46/0.64 (step @p79 :rule cnf_or_pos :args (@t61)) % 0.46/0.64 (step @p80 :rule reordering :premises (@p79) :args ((or @t34 @t59 @t60 (not @t61)))) % 0.46/0.64 (assume-push @p396 @t18) % 0.46/0.64 (step @p82 :rule instantiate :premises (@p13) :args (@t65)) % 0.46/0.64 (step-pop @p397 :rule scope :premises (@p82)) % 0.46/0.64 (step @p83 :rule process_scope :premises (@p397) :args (@t70)) % 0.46/0.64 (step @p85 :rule implies_elim :premises (@p83)) % 0.46/0.64 (step @p86 :rule cnf_or_pos :args (@t70)) % 0.46/0.64 (step @p87 :rule reordering :premises (@p86) :args ((or @t68 @t67 @t50 @t69 @t66 (not @t70)))) % 0.46/0.64 (step @p88 :rule instantiate :premises (@p14) :args (@t71)) % 0.46/0.64 (step @p89 :rule cnf_or_pos :args (@t76)) % 0.46/0.64 (step @p90 :rule reordering :premises (@p89) :args ((or @t75 @t55 @t73 (not @t76)))) % 0.46/0.64 (step @p91 :rule instantiate :premises (@p14) :args (@t77)) % 0.46/0.64 (step @p92 :rule cnf_or_pos :args (@t80)) % 0.46/0.64 (step @p93 :rule reordering :premises (@p92) :args ((or @t79 @t75 @t53 (not @t80)))) % 0.46/0.64 (step @p94 :rule instantiate :premises (@p13) :args ((@list tptp.one tptp.five))) % 0.46/0.64 (step @p65 :rule instantiate :premises (@p12) :args (@t62)) % 0.46/0.64 (step @p95 :rule chain_m_resolution :premises (@p78 @p10 @p24 @p65) :args (@t58 @t29 (@list @t10 @t32 @t64))) % 0.46/0.64 (step @p96 :rule cnf_or_pos :args (@t83)) % 0.46/0.64 (step @p97 :rule reordering :premises (@p96) :args ((or @t68 @t81 @t72 @t82 @t59 (not @t83)))) % 0.46/0.64 (step @p98 :rule instantiate :premises (@p13) :args ((@list tptp.five tptp.six))) % 0.46/0.64 (step @p99 :rule cnf_or_pos :args (@t85)) % 0.46/0.64 (step @p100 :rule reordering :premises (@p99) :args ((or @t81 @t67 @t34 @t78 @t84 (not @t85)))) % 0.46/0.64 (step @p101 :rule instantiate :premises (@p15) :args (@t86)) % 0.46/0.64 (step @p102 :rule cnf_or_pos :args (@t90)) % 0.46/0.64 (step @p103 :rule reordering :premises (@p102) :args ((or @t88 @t89 @t87 (not @t90)))) % 0.46/0.64 (step @p104 :rule chain_m_resolution :premises (@p103 @p101 @p100 @p98 @p11 @p6 @p5 @p97 @p95 @p94 @p5 @p1 @p93 @p91 @p90 @p88 @p87 @p1 @p6 @p85 @p13 @p80 @p11 @p78 @p10 @p23 @p9 @p20 @p7 @p8 @p76 @p72 @p68 @p63 @p12 @p54 @p58 @p14) :args ((or @t75 @t55 @t53) @t91 (@list @t90 @t84 @t85 @t11 @t6 @t5 @t82 @t58 @t83 @t5 @t1 @t78 @t80 @t72 @t76 @t69 @t1 @t6 @t70 @t18 @t60 @t11 @t58 @t10 @t32 @t9 @t27 @t7 @t8 @t28 @t33 @t64 @t61 @t15 @t50 @t56 @t23))) % 0.46/0.64 (step @p82 :rule instantiate :premises (@p13) :args (@t65)) % 0.46/0.64 (step @p60 :rule instantiate :premises (@p12) :args (@t57)) % 0.46/0.64 (step @p105 :rule chain_m_resolution :premises (@p80 @p11 @p95 @p60) :args (@t60 @t29 (@list @t11 @t58 @t61))) % 0.46/0.64 (step @p106 :rule cnf_or_pos :args (@t95)) % 0.46/0.64 (step @p107 :rule reordering :premises (@p106) :args ((or @t93 @t81 @t74 @t94 @t92 (not @t95)))) % 0.46/0.64 (step @p108 :rule instantiate :premises (@p14) :args (@t96)) % 0.46/0.64 (step @p109 :rule cnf_or_pos :args (@t101)) % 0.46/0.64 (step @p110 :rule reordering :premises (@p109) :args ((or @t100 @t53 @t98 (not @t101)))) % 0.46/0.64 (step @p111 :rule instantiate :premises (@p14) :args (@t102)) % 0.46/0.64 (step @p112 :rule cnf_or_pos :args (@t105)) % 0.46/0.64 (step @p113 :rule reordering :premises (@p112) :args ((or @t104 @t100 @t55 (not @t105)))) % 0.46/0.64 (step @p114 :rule instantiate :premises (@p13) :args ((@list tptp.two tptp.six))) % 0.46/0.64 (step @p115 :rule instantiate :premises (@p12) :args ((@list tptp.two tptp.six tptp.five))) % 0.46/0.64 (step @p116 :rule cnf_or_pos :args (@t108)) % 0.46/0.64 (step @p117 :rule reordering :premises (@p116) :args ((or @t34 @t106 @t107 (not @t108)))) % 0.46/0.64 (step @p118 :rule chain_m_resolution :premises (@p117 @p11 @p49 @p115) :args (@t107 @t29 (@list @t11 @t47 @t108))) % 0.46/0.64 (step @p119 :rule cnf_or_pos :args (@t112)) % 0.46/0.64 (step @p120 :rule reordering :premises (@p119) :args ((or @t110 @t67 @t97 @t111 @t109 (not @t112)))) % 0.46/0.64 (step @p121 :rule instantiate :premises (@p13) :args ((@list tptp.one tptp.two))) % 0.46/0.64 (step @p122 :rule cnf_or_pos :args (@t114)) % 0.46/0.64 (step @p123 :rule reordering :premises (@p122) :args ((or @t68 @t110 @t26 @t103 @t113 (not @t114)))) % 0.46/0.64 (step @p124 :rule instantiate :premises (@p15) :args (@t115)) % 0.46/0.64 (step @p125 :rule cnf_or_pos :args (@t118)) % 0.46/0.64 (step @p126 :rule reordering :premises (@p125) :args ((or @t117 @t116 @t87 (not @t118)))) % 0.46/0.64 (step @p127 :rule chain_m_resolution :premises (@p126 @p124 @p123 @p121 @p7 @p2 @p1 @p120 @p118 @p114 @p6 @p2 @p113 @p111 @p110 @p108 @p87 @p1 @p6 @p85 @p13 @p80 @p11 @p78 @p10 @p23 @p9 @p20 @p7 @p8 @p76 @p72 @p68 @p63 @p12 @p54 @p58 @p14) :args ((or @t100 @t55 @t53) @t91 (@list @t118 @t113 @t114 @t7 @t2 @t1 @t111 @t107 @t112 @t6 @t2 @t103 @t105 @t97 @t101 @t69 @t1 @t6 @t70 @t18 @t60 @t11 @t58 @t10 @t32 @t9 @t27 @t7 @t8 @t28 @t33 @t64 @t61 @t15 @t50 @t56 @t23))) % 0.46/0.64 (step @p128 :rule instantiate :premises (@p13) :args ((@list tptp.two tptp.three))) % 0.46/0.64 (step @p129 :rule cnf_or_pos :args (@t120)) % 0.46/0.64 (step @p130 :rule reordering :premises (@p129) :args ((or @t110 @t93 @t25 @t99 @t119 (not @t120)))) % 0.46/0.64 (step @p131 :rule instantiate :premises (@p15) :args (@t121)) % 0.46/0.64 (step @p132 :rule cnf_or_pos :args (@t126)) % 0.46/0.64 (step @p133 :rule reordering :premises (@p132) :args ((or @t125 @t124 @t123 (not @t126)))) % 0.46/0.64 (step @p134 :rule cnf_or_pos :args (@t128)) % 0.46/0.64 (step @p135 :rule reordering :premises (@p134) :args ((or @t110 @t81 @t127 @t122 @t106 (not @t128)))) % 0.46/0.64 (step @p136 :rule instantiate :premises (@p14) :args (@t129)) % 0.46/0.64 (step @p137 :rule cnf_or_pos :args (@t135)) % 0.46/0.64 (step @p138 :rule reordering :premises (@p137) :args ((or @t132 @t134 @t130 (not @t135)))) % 0.46/0.64 (step @p139 :rule cnf_or_pos :args (@t138)) % 0.46/0.64 (step @p140 :rule reordering :premises (@p139) :args ((or @t136 @t81 @t35 @t131 @t137 (not @t138)))) % 0.46/0.64 (step @p141 :rule cnf_or_pos :args (@t142)) % 0.46/0.64 (step @p142 :rule reordering :premises (@p141) :args ((or @t141 @t139 @t124 (not @t142)))) % 0.46/0.64 (step @p143 :rule cnf_or_pos :args (@t144)) % 0.46/0.64 (step @p144 :rule reordering :premises (@p143) :args ((or @t93 @t136 @t30 @t143 @t140 (not @t144)))) % 0.46/0.64 (step @p145 :rule instantiate :premises (@p14) :args (@t145)) % 0.46/0.64 (step @p146 :rule cnf_or_pos :args (@t149)) % 0.46/0.64 (step @p147 :rule reordering :premises (@p146) :args ((or @t148 @t147 @t53 (not @t149)))) % 0.46/0.64 (step @p148 :rule instantiate :premises (@p14) :args (@t150)) % 0.46/0.64 (step @p149 :rule cnf_or_pos :args (@t153)) % 0.46/0.64 (step @p150 :rule reordering :premises (@p149) :args ((or @t148 @t55 @t152 (not @t153)))) % 0.46/0.64 (step @p151 :rule instantiate :premises (@p13) :args ((@list tptp.four tptp.six))) % 0.46/0.64 (step @p152 :rule cnf_or_pos :args (@t155)) % 0.46/0.64 (step @p153 :rule reordering :premises (@p152) :args ((or @t136 @t67 @t146 @t154 @t38 (not @t155)))) % 0.46/0.64 (step @p154 :rule cnf_or_pos :args (@t157)) % 0.46/0.64 (step @p155 :rule reordering :premises (@p154) :args ((or @t68 @t136 @t151 @t156 @t63 (not @t157)))) % 0.46/0.64 (step @p156 :rule instantiate :premises (@p15) :args (@t158)) % 0.46/0.64 (step @p157 :rule cnf_or_pos :args (@t161)) % 0.46/0.64 (step @p158 :rule reordering :premises (@p157) :args ((or @t159 @t160 @t87 (not @t161)))) % 0.46/0.64 (step @p159 :rule chain_m_resolution :premises (@p158 @p156 @p155 @p24 @p16 @p4 @p1 @p153 @p151 @p30 @p6 @p4 @p150 @p148 @p147 @p145 @p144 @p34 @p9 @p4 @p3 @p142 @p35 @p140 @p50 @p10 @p5 @p4 @p138 @p136 @p135 @p49 @p41 @p5 @p2 @p133 @p131 @p130 @p128 @p8 @p3 @p2 @p127 @p107 @p36 @p40 @p5 @p3 @p87 @p105 @p82 @p6 @p1 @p104 @p54 @p52) :args ((or @t134 @t55 @t53) (@list false false false false false false false false false false false true false true false false false false false false true false false false false false false true false false false false false false true false false false false false false true false false false false false false false false false false true true false) (@list @t161 @t156 @t32 @t157 @t4 @t1 @t154 @t155 @t36 @t6 @t4 @t151 @t153 @t146 @t149 @t143 @t144 @t9 @t4 @t3 @t140 @t142 @t137 @t138 @t10 @t5 @t4 @t131 @t135 @t127 @t47 @t128 @t5 @t2 @t122 @t126 @t119 @t120 @t8 @t3 @t2 @t99 @t94 @t95 @t42 @t5 @t3 @t69 @t60 @t70 @t6 @t1 @t74 @t50 @t56))) % 0.46/0.64 (step @p160 :rule cnf_or_pos :args (@t164)) % 0.46/0.64 (step @p161 :rule reordering :premises (@p160) :args ((or @t93 @t67 @t52 @t163 @t162 (not @t164)))) % 0.46/0.64 (assume-push @p398 @t18) % 0.46/0.64 (step-pop @p399 :rule scope :premises (@p25)) % 0.46/0.64 (step @p163 :rule process_scope :premises (@p399) :args (@t164)) % 0.46/0.64 (step @p165 :rule implies_elim :premises (@p163)) % 0.46/0.64 (assume-push @p400 @t15) % 0.46/0.64 (step-pop @p401 :rule scope :premises (@p26)) % 0.46/0.64 (step @p167 :rule process_scope :premises (@p401) :args (@t40)) % 0.46/0.64 (step @p169 :rule implies_elim :premises (@p167)) % 0.46/0.64 (assume-push @p402 @t15) % 0.46/0.64 (step-pop @p403 :rule scope :premises (@p27)) % 0.46/0.64 (step @p171 :rule process_scope :premises (@p403) :args (@t37)) % 0.46/0.64 (step @p173 :rule implies_elim :premises (@p171)) % 0.46/0.64 (step @p174 :rule instantiate :premises (@p15) :args (@t96)) % 0.46/0.64 (step @p175 :rule cnf_or_pos :args (@t166)) % 0.46/0.64 (step @p176 :rule reordering :premises (@p175) :args ((or @t125 @t116 @t165 (not @t166)))) % 0.46/0.64 (step @p177 :rule instantiate :premises (@p15) :args (@t145)) % 0.46/0.64 (step @p178 :rule cnf_or_pos :args (@t167)) % 0.46/0.64 (step @p179 :rule reordering :premises (@p178) :args ((or @t141 @t159 @t165 (not @t167)))) % 0.46/0.64 (step @p180 :rule instantiate :premises (@p14) :args (@t168)) % 0.46/0.64 (step @p181 :rule cnf_or_pos :args (@t169)) % 0.46/0.64 (step @p182 :rule reordering :premises (@p181) :args ((or @t134 @t147 @t98 (not @t169)))) % 0.46/0.64 (step @p183 :rule chain_m_resolution :premises (@p182 @p180 @p153 @p151 @p30 @p6 @p4 @p120 @p118 @p114 @p6 @p2 @p179 @p177 @p176 @p174) :args ((or @t125 @t141 @t134 @t165) @t170 (@list @t169 @t146 @t155 @t36 @t6 @t4 @t97 @t107 @t112 @t6 @t2 @t154 @t167 @t111 @t166))) % 0.46/0.64 (assume-push @p404 @t23) % 0.46/0.64 (step-pop @p405 :rule scope :premises (@p180)) % 0.46/0.64 (step @p185 :rule process_scope :premises (@p405) :args (@t169)) % 0.46/0.64 (step @p187 :rule implies_elim :premises (@p185)) % 0.46/0.64 (assume-push @p406 @t18) % 0.46/0.64 (step-pop @p407 :rule scope :premises (@p151)) % 0.46/0.64 (step @p189 :rule process_scope :premises (@p407) :args (@t155)) % 0.46/0.64 (step @p191 :rule implies_elim :premises (@p189)) % 0.46/0.64 (step @p192 :rule instantiate :premises (@p14) :args (@t171)) % 0.46/0.64 (step @p193 :rule cnf_or_pos :args (@t172)) % 0.46/0.64 (step @p194 :rule reordering :premises (@p193) :args ((or @t79 @t130 @t98 (not @t172)))) % 0.46/0.64 (step @p195 :rule instantiate :premises (@p15) :args (@t173)) % 0.46/0.64 (step @p196 :rule cnf_or_pos :args (@t174)) % 0.46/0.64 (step @p197 :rule reordering :premises (@p196) :args ((or @t139 @t88 @t159 (not @t174)))) % 0.46/0.64 (step @p198 :rule chain_m_resolution :premises (@p197 @p195 @p100 @p98 @p11 @p6 @p5 @p140 @p50 @p10 @p5 @p4 @p194 @p192 @p138 @p136 @p153 @p4 @p6 @p29 @p10 @p11 @p173 @p12 @p191 @p13 @p182 @p187 @p14) :args ((or @t134 @t130 @t98) @t175 (@list @t174 @t84 @t85 @t11 @t6 @t5 @t137 @t138 @t10 @t5 @t4 @t78 @t172 @t131 @t135 @t154 @t4 @t6 @t36 @t10 @t11 @t37 @t15 @t155 @t18 @t146 @t169 @t23))) % 0.46/0.64 (step @p199 :rule instantiate :premises (@p14) :args (@t41)) % 0.46/0.64 (step @p200 :rule cnf_or_pos :args (@t176)) % 0.46/0.64 (step @p201 :rule reordering :premises (@p200) :args ((or @t148 @t132 @t75 (not @t176)))) % 0.46/0.64 (step @p202 :rule instantiate :premises (@p15) :args (@t177)) % 0.46/0.64 (step @p203 :rule cnf_or_pos :args (@t178)) % 0.46/0.64 (step @p204 :rule reordering :premises (@p203) :args ((or @t139 @t160 @t89 (not @t178)))) % 0.46/0.64 (step @p205 :rule chain_m_resolution :premises (@p204 @p202 @p97 @p95 @p94 @p5 @p1 @p140 @p50 @p10 @p5 @p4 @p90 @p88 @p201 @p199 @p107 @p36 @p40 @p5 @p3 @p133 @p131 @p135 @p49 @p41 @p5 @p2 @p198 @p155 @p24 @p16 @p4 @p1 @p150 @p148 @p144 @p34 @p9 @p4 @p3 @p120 @p118 @p114 @p6 @p2 @p183 @p176 @p174 @p161 @p3 @p6 @p32 @p9 @p29 @p10 @p11 @p173 @p169 @p12 @p165 @p13 @p159) :args ((or @t125 @t134 @t55) (@list false false false false false false false false false false false true false true false false false false false false true false false false false false false true false false false false false true false false false false false false false false false false false true true false false false false false false false false false false false false false false true) (@list @t178 @t82 @t58 @t83 @t5 @t1 @t137 @t138 @t10 @t5 @t4 @t72 @t76 @t131 @t176 @t74 @t95 @t42 @t5 @t3 @t94 @t126 @t122 @t47 @t128 @t5 @t2 @t127 @t156 @t32 @t157 @t4 @t1 @t151 @t153 @t143 @t144 @t9 @t4 @t3 @t97 @t107 @t112 @t6 @t2 @t140 @t111 @t166 @t163 @t3 @t6 @t39 @t9 @t36 @t10 @t11 @t37 @t40 @t15 @t164 @t18 @t52))) % 0.46/0.64 (step @p206 :rule instantiate :premises (@p14) :args (@t179)) % 0.46/0.64 (step @p207 :rule cnf_or_pos :args (@t180)) % 0.46/0.64 (step @p208 :rule reordering :premises (@p207) :args ((or @t100 @t148 @t134 (not @t180)))) % 0.46/0.64 (step @p209 :rule instantiate :premises (@p14) :args (@t158)) % 0.46/0.64 (step @p210 :rule cnf_or_pos :args (@t181)) % 0.46/0.64 (step @p211 :rule reordering :premises (@p210) :args ((or @t147 @t152 @t51 (not @t181)))) % 0.46/0.64 (step @p212 :rule chain_m_resolution :premises (@p90 @p88 @p97 @p95 @p94 @p5 @p1 @p107 @p36 @p40 @p5 @p3 @p204 @p202 @p142 @p35) :args ((or @t141 @t139 @t55 @t160) @t170 (@list @t76 @t72 @t58 @t83 @t5 @t1 @t74 @t95 @t42 @t5 @t3 @t82 @t178 @t94 @t142))) % 0.46/0.64 (step @p213 :rule instantiate :premises (@p14) :args (@t173)) % 0.46/0.64 (step @p214 :rule cnf_or_pos :args (@t182)) % 0.46/0.64 (step @p215 :rule reordering :premises (@p214) :args ((or @t132 @t79 @t147 (not @t182)))) % 0.46/0.64 (step @p216 :rule instantiate :premises (@p15) :args (@t171)) % 0.46/0.64 (step @p217 :rule cnf_or_pos :args (@t183)) % 0.46/0.64 (step @p218 :rule reordering :premises (@p217) :args ((or @t88 @t123 @t116 (not @t183)))) % 0.46/0.64 (step @p219 :rule chain_m_resolution :premises (@p218 @p216 @p100 @p98 @p11 @p6 @p5 @p135 @p49 @p41 @p5 @p2 @p215 @p213 @p138 @p136 @p140 @p50 @p10 @p5 @p4 @p212 @p155 @p24 @p16 @p4 @p1 @p211 @p209 @p87 @p105 @p82 @p6 @p1 @p126 @p124 @p120 @p118 @p114 @p6 @p2 @p182 @p180 @p153 @p151 @p30 @p6 @p4 @p179 @p177 @p123 @p121 @p7 @p2 @p1 @p144 @p34 @p9 @p4 @p3 @p113 @p111 @p208 @p206 @p130 @p128 @p8 @p3 @p2 @p205 @p161 @p25 @p33 @p6 @p3 @p159) :args ((or @t134 @t55) (@list false false false false false false false false false false false true false true false false false false false false true false false false false false true false false false false false false true false false false false false false true false false false false false false true false false false false false false false false false false false true false true false false false false false false true false false false false false true) (@list @t183 @t84 @t85 @t11 @t6 @t5 @t122 @t47 @t128 @t5 @t2 @t78 @t182 @t127 @t135 @t131 @t138 @t10 @t5 @t4 @t137 @t156 @t32 @t157 @t4 @t1 @t151 @t181 @t50 @t60 @t70 @t6 @t1 @t69 @t118 @t111 @t107 @t112 @t6 @t2 @t97 @t169 @t146 @t155 @t36 @t6 @t4 @t154 @t167 @t113 @t114 @t7 @t2 @t1 @t140 @t144 @t9 @t4 @t3 @t103 @t105 @t143 @t180 @t99 @t120 @t8 @t3 @t2 @t119 @t163 @t164 @t39 @t6 @t3 @t52))) % 0.46/0.64 (assume-push @p408 @t18) % 0.46/0.64 (step @p221 :rule instantiate :premises (@p13) :args (@t184)) % 0.46/0.64 (step-pop @p409 :rule scope :premises (@p221)) % 0.46/0.64 (step @p222 :rule process_scope :premises (@p409) :args (@t186)) % 0.46/0.64 (step @p224 :rule implies_elim :premises (@p222)) % 0.46/0.64 (assume-push @p410 @t15) % 0.46/0.64 (step-pop @p411 :rule scope :premises (@p43)) % 0.46/0.64 (step @p226 :rule process_scope :premises (@p411) :args (@t45)) % 0.46/0.64 (step @p228 :rule implies_elim :premises (@p226)) % 0.46/0.64 (step @p229 :rule cnf_or_pos :args (@t186)) % 0.46/0.64 (step @p230 :rule reordering :premises (@p229) :args ((or @t110 @t136 @t133 @t185 @t46 (not @t186)))) % 0.46/0.64 (step @p231 :rule instantiate :premises (@p15) :args (@t187)) % 0.46/0.64 (step @p232 :rule cnf_or_pos :args (@t189)) % 0.46/0.64 (step @p233 :rule reordering :premises (@p232) :args ((or @t117 @t188 @t160 (not @t189)))) % 0.46/0.64 (assume-push @p412 @t23) % 0.46/0.64 (step-pop @p413 :rule scope :premises (@p148)) % 0.46/0.64 (step @p235 :rule process_scope :premises (@p413) :args (@t153)) % 0.46/0.64 (step @p237 :rule implies_elim :premises (@p235)) % 0.46/0.64 (assume-push @p414 @t18) % 0.46/0.64 (step-pop @p415 :rule scope :premises (@p16)) % 0.46/0.64 (step @p239 :rule process_scope :premises (@p415) :args (@t157)) % 0.46/0.64 (step @p241 :rule implies_elim :premises (@p239)) % 0.46/0.64 (step @p242 :rule chain_m_resolution :premises (@p158 @p156 @p153 @p151 @p30 @p6 @p4 @p87 @p105 @p82 @p6 @p1 @p147 @p145 @p54 @p52 @p155 @p1 @p4 @p241 @p13 @p23 @p9 @p20 @p7 @p8 @p76 @p72 @p12 @p150 @p237 @p14) :args ((or @t148 @t55 @t53) @t190 (@list @t161 @t154 @t155 @t36 @t6 @t4 @t69 @t60 @t70 @t6 @t1 @t146 @t149 @t50 @t56 @t156 @t1 @t4 @t157 @t18 @t32 @t9 @t27 @t7 @t8 @t28 @t33 @t15 @t151 @t153 @t23))) % 0.46/0.64 (assume-push @p416 @t24) % 0.46/0.64 (step-pop @p417 :rule scope :premises (@p131)) % 0.46/0.64 (step @p244 :rule process_scope :premises (@p417) :args (@t126)) % 0.46/0.64 (step @p246 :rule implies_elim :premises (@p244)) % 0.46/0.64 (assume-push @p418 @t15) % 0.46/0.64 (step-pop @p419 :rule scope :premises (@p42)) % 0.46/0.64 (step @p248 :rule process_scope :premises (@p419) :args (@t48)) % 0.46/0.64 (step @p250 :rule implies_elim :premises (@p248)) % 0.46/0.64 (assume-push @p420 @t18) % 0.46/0.64 (step-pop @p421 :rule scope :premises (@p41)) % 0.46/0.64 (step @p252 :rule process_scope :premises (@p421) :args (@t128)) % 0.46/0.64 (step @p254 :rule implies_elim :premises (@p252)) % 0.46/0.64 (step @p255 :rule instantiate :premises (@p15) :args (@t77)) % 0.46/0.64 (step @p256 :rule cnf_or_pos :args (@t191)) % 0.46/0.64 (step @p257 :rule reordering :premises (@p256) :args ((or @t88 @t124 @t165 (not @t191)))) % 0.46/0.64 (step @p258 :rule chain_m_resolution :premises (@p194 @p192 @p100 @p98 @p11 @p6 @p5 @p120 @p118 @p114 @p6 @p2 @p257 @p255 @p176 @p174 @p135 @p2 @p5 @p254 @p13 @p48 @p10 @p45 @p8 @p9 @p228 @p250 @p12 @p133 @p246 @p15) :args ((or @t125 @t124 @t165) @t190 (@list @t172 @t78 @t85 @t11 @t6 @t5 @t97 @t107 @t112 @t6 @t2 @t84 @t191 @t111 @t166 @t127 @t2 @t5 @t128 @t18 @t47 @t10 @t44 @t8 @t9 @t45 @t48 @t15 @t122 @t126 @t24))) % 0.46/0.64 (step @p259 :rule chain_m_resolution :premises (@p204 @p202 @p140 @p50 @p10 @p5 @p4 @p97 @p95 @p94 @p5 @p1 @p201 @p199 @p90 @p88 @p107 @p36 @p40 @p5 @p3 @p258 @p161 @p25 @p33 @p6 @p3 @p242 @p130 @p128 @p8 @p3 @p2 @p113 @p111 @p123 @p121 @p7 @p2 @p1 @p233 @p231 @p155 @p24 @p16 @p4 @p1 @p150 @p148 @p230 @p2 @p4 @p45 @p8 @p9 @p228 @p12 @p224 @p13 @p219) :args ((or @t148 @t55) (@list false false false false false false false false false false false true false true false false false false false false true false false false false false true false false false false false true false false false false false false true false false false false false false true false false false false false false false false false false false true) (@list @t178 @t137 @t138 @t10 @t5 @t4 @t82 @t58 @t83 @t5 @t1 @t131 @t176 @t72 @t76 @t74 @t95 @t42 @t5 @t3 @t94 @t163 @t164 @t39 @t6 @t3 @t52 @t119 @t120 @t8 @t3 @t2 @t99 @t105 @t103 @t114 @t7 @t2 @t1 @t113 @t189 @t156 @t32 @t157 @t4 @t1 @t151 @t153 @t185 @t2 @t4 @t44 @t8 @t9 @t45 @t15 @t186 @t18 @t133))) % 0.46/0.64 (step @p221 :rule instantiate :premises (@p13) :args (@t184)) % 0.46/0.64 (step @p260 :rule instantiate :premises (@p15) :args (@t179)) % 0.46/0.64 (step @p261 :rule cnf_or_pos :args (@t192)) % 0.46/0.64 (step @p262 :rule reordering :premises (@p261) :args ((or @t125 @t141 @t188 (not @t192)))) % 0.46/0.64 (step @p263 :rule chain_m_resolution :premises (@p179 @p177 @p161 @p25 @p33 @p6 @p3 @p153 @p151 @p30 @p6 @p4 @p54 @p52 @p211 @p209) :args ((or @t141 @t55 @t152 @t51) @t170 (@list @t167 @t163 @t164 @t39 @t6 @t3 @t154 @t155 @t36 @t6 @t4 @t52 @t56 @t146 @t181))) % 0.46/0.64 (step @p264 :rule instantiate :premises (@p14) :args (@t177)) % 0.46/0.64 (step @p265 :rule cnf_or_pos :args (@t193)) % 0.46/0.64 (step @p266 :rule reordering :premises (@p265) :args ((or @t132 @t152 @t73 (not @t193)))) % 0.46/0.64 (step @p267 :rule chain_m_resolution :premises (@p103 @p101 @p100 @p98 @p11 @p6 @p5 @p97 @p95 @p94 @p5 @p1 @p87 @p105 @p82 @p6 @p1 @p215 @p213 @p266 @p264 @p263 @p153 @p151 @p30 @p6 @p4 @p155 @p24 @p16 @p4 @p1 @p179 @p177 @p233 @p231 @p161 @p25 @p33 @p6 @p3 @p123 @p121 @p7 @p2 @p1 @p127 @p113 @p111 @p130 @p128 @p8 @p3 @p2 @p262 @p260 @p230 @p2 @p4 @p45 @p8 @p9 @p228 @p12 @p224 @p13 @p219) :args ((or @t141 @t132 @t55) (@list false false false false false false false false false false false false false false false false true false true false true false false false false false false false false false false true false true false false false false false false false false false false false true true false false false false false false true false false false false false false false false false false false true) (@list @t90 @t84 @t85 @t11 @t6 @t5 @t82 @t58 @t83 @t5 @t1 @t69 @t60 @t70 @t6 @t1 @t78 @t182 @t72 @t193 @t50 @t146 @t155 @t36 @t6 @t4 @t151 @t32 @t157 @t4 @t1 @t154 @t167 @t156 @t189 @t163 @t164 @t39 @t6 @t3 @t113 @t114 @t7 @t2 @t1 @t52 @t103 @t105 @t99 @t120 @t8 @t3 @t2 @t119 @t192 @t185 @t2 @t4 @t44 @t8 @t9 @t45 @t15 @t186 @t18 @t133))) % 0.46/0.64 (step @p268 :rule instantiate :premises (@p15) :args (@t129)) % 0.46/0.64 (step @p269 :rule cnf_or_pos :args (@t194)) % 0.46/0.64 (step @p270 :rule reordering :premises (@p269) :args ((or @t139 @t188 @t123 (not @t194)))) % 0.46/0.64 (step @p271 :rule instantiate :premises (@p14) :args (@t121)) % 0.46/0.64 (step @p272 :rule cnf_or_pos :args (@t195)) % 0.46/0.64 (step @p273 :rule reordering :premises (@p272) :args ((or @t100 @t75 @t130 (not @t195)))) % 0.46/0.64 (step @p274 :rule chain_m_resolution :premises (@p273 @p271 @p135 @p49 @p41 @p5 @p2 @p107 @p36 @p40 @p5 @p3 @p270 @p268 @p142 @p35 @p140 @p50 @p10 @p5 @p4 @p130 @p128 @p8 @p3 @p2 @p267 @p262 @p260 @p144 @p34 @p9 @p4 @p3 @p230 @p221 @p46 @p4 @p2 @p259 @p219) :args (@t55 (@list false false false false false false false false false false false true false true false false false false false false false false false false false true true false false false false false false false false false false false true true) (@list @t195 @t127 @t47 @t128 @t5 @t2 @t74 @t95 @t42 @t5 @t3 @t122 @t194 @t94 @t142 @t137 @t138 @t10 @t5 @t4 @t99 @t120 @t8 @t3 @t2 @t131 @t119 @t192 @t140 @t144 @t9 @t4 @t3 @t185 @t186 @t44 @t4 @t2 @t143 @t133))) % 0.46/0.64 (step @p275 :rule cnf_or_pos :args (@t197)) % 0.46/0.64 (step @p276 :rule reordering :premises (@p275) :args ((or @t68 @t93 @t54 @t196 @t31 (not @t197)))) % 0.46/0.64 (step @p277 :rule chain_m_resolution :premises (@p276 @p1 @p3 @p274 @p21 @p51) :args (@t196 @t198 (@list @t1 @t3 @t54 @t27 @t197))) % 0.46/0.64 (step @p278 :rule instantiate :premises (@p15) :args (@t49)) % 0.46/0.64 (step @p279 :rule cnf_or_pos :args (@t200)) % 0.46/0.64 (step @p280 :rule reordering :premises (@p279) :args ((or @t199 @t165 @t87 (not @t200)))) % 0.46/0.64 (assume-push @p422 @t24) % 0.46/0.64 (step-pop @p423 :rule scope :premises (@p278)) % 0.46/0.64 (step @p282 :rule process_scope :premises (@p423) :args (@t200)) % 0.46/0.64 (step @p284 :rule implies_elim :premises (@p282)) % 0.46/0.64 (assume-push @p424 @t18) % 0.46/0.64 (step-pop @p425 :rule scope :premises (@p51)) % 0.46/0.64 (step @p286 :rule process_scope :premises (@p425) :args (@t197)) % 0.46/0.64 (step @p288 :rule implies_elim :premises (@p286)) % 0.46/0.64 (step @p289 :rule instantiate :premises (@p15) :args (@t150)) % 0.46/0.64 (step @p290 :rule cnf_or_pos :args (@t201)) % 0.46/0.64 (step @p291 :rule reordering :premises (@p290) :args ((or @t141 @t199 @t160 (not @t201)))) % 0.46/0.64 (step @p292 :rule chain_m_resolution :premises (@p211 @p209 @p153 @p151 @p30 @p6 @p4 @p155 @p24 @p16 @p4 @p1 @p179 @p177 @p291 @p289 @p277 @p87 @p6 @p85 @p80 @p11 @p78 @p10 @p23 @p9 @p72 @p68 @p63 @p280 @p276 @p1 @p3 @p288 @p13 @p20 @p7 @p8 @p76 @p12 @p274 @p284 @p15) :args ((or @t141 @t165) (@list false false false false false false false false false false false true false true 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 true false false) (@list @t181 @t146 @t155 @t36 @t6 @t4 @t151 @t32 @t157 @t4 @t1 @t154 @t167 @t156 @t201 @t196 @t50 @t6 @t70 @t60 @t11 @t58 @t10 @t32 @t9 @t33 @t64 @t61 @t69 @t196 @t1 @t3 @t197 @t18 @t27 @t7 @t8 @t28 @t15 @t54 @t200 @t24))) % 0.46/0.64 (step @p293 :rule instantiate :premises (@p15) :args (@t71)) % 0.46/0.64 (step @p294 :rule cnf_or_pos :args (@t202)) % 0.46/0.64 (step @p295 :rule reordering :premises (@p294) :args ((or @t124 @t199 @t89 (not @t202)))) % 0.46/0.64 (step @p296 :rule instantiate :premises (@p14) :args (@t86)) % 0.46/0.64 (step @p297 :rule cnf_or_pos :args (@t203)) % 0.46/0.64 (step @p298 :rule reordering :premises (@p297) :args ((or @t79 @t73 @t51 (not @t203)))) % 0.46/0.64 (step @p299 :rule chain_m_resolution :premises (@p298 @p296 @p100 @p98 @p11 @p6 @p5 @p97 @p95 @p94 @p5 @p1 @p257 @p255 @p295 @p293 @p277 @p107 @p36 @p40 @p5 @p3 @p201 @p199 @p144 @p34 @p9 @p4 @p3 @p87 @p105 @p82 @p6 @p1 @p292 @p280 @p278 @p277) :args ((or @t132 @t165) (@list false false false false false false false false false false false true false true false false false false false false false true false false false false false false false false false false false true true false false) (@list @t203 @t78 @t85 @t11 @t6 @t5 @t72 @t58 @t83 @t5 @t1 @t84 @t191 @t82 @t202 @t196 @t94 @t95 @t42 @t5 @t3 @t74 @t176 @t143 @t144 @t9 @t4 @t3 @t50 @t60 @t70 @t6 @t1 @t140 @t69 @t200 @t196))) % 0.46/0.64 (assume-push @p426 @t23) % 0.46/0.64 (step-pop @p427 :rule scope :premises (@p206)) % 0.46/0.64 (step @p301 :rule process_scope :premises (@p427) :args (@t180)) % 0.46/0.64 (step @p303 :rule implies_elim :premises (@p301)) % 0.46/0.64 (step @p304 :rule instantiate :premises (@p15) :args (@t168)) % 0.46/0.64 (step @p305 :rule cnf_or_pos :args (@t204)) % 0.46/0.64 (step @p306 :rule reordering :premises (@p305) :args ((or @t188 @t159 @t116 (not @t204)))) % 0.46/0.64 (step @p307 :rule chain_m_resolution :premises (@p306 @p304 @p120 @p118 @p114 @p6 @p2 @p153 @p151 @p30 @p6 @p4 @p110 @p108 @p147 @p145 @p230 @p2 @p4 @p45 @p8 @p9 @p228 @p12 @p224 @p13 @p208 @p303 @p14) :args ((or @t100 @t148 @t53) @t175 (@list @t204 @t111 @t107 @t112 @t6 @t2 @t154 @t155 @t36 @t6 @t4 @t97 @t101 @t146 @t149 @t185 @t2 @t4 @t44 @t8 @t9 @t45 @t15 @t186 @t18 @t133 @t180 @t23))) % 0.46/0.64 (step @p308 :rule instantiate :premises (@p15) :args (@t102)) % 0.46/0.64 (step @p309 :rule cnf_or_pos :args (@t205)) % 0.46/0.64 (step @p310 :rule reordering :premises (@p309) :args ((or @t117 @t125 @t199 (not @t205)))) % 0.46/0.64 (step @p311 :rule instantiate :premises (@p14) :args (@t206)) % 0.46/0.64 (step @p312 :rule cnf_or_pos :args (@t207)) % 0.46/0.64 (step @p313 :rule reordering :premises (@p312) :args ((or @t104 @t130 @t73 (not @t207)))) % 0.46/0.64 (step @p314 :rule chain_m_resolution :premises (@p313 @p311 @p135 @p49 @p41 @p5 @p2 @p123 @p121 @p7 @p2 @p1 @p97 @p95 @p94 @p5 @p1 @p133 @p131 @p310 @p308 @p277 @p295 @p293 @p277 @p130 @p128 @p8 @p3 @p2 @p107 @p36 @p40 @p5 @p3 @p307 @p201 @p199 @p161 @p3 @p6 @p32 @p9 @p29 @p10 @p11 @p173 @p169 @p12 @p165 @p13 @p299) :args ((or @t148 @t132) (@list false false false false false false false false false false false false false false false false true false true false false true false false false false false false false false false false false false true true false false false false false false false false false false false false false false true) (@list @t207 @t127 @t47 @t128 @t5 @t2 @t103 @t114 @t7 @t2 @t1 @t72 @t58 @t83 @t5 @t1 @t122 @t126 @t113 @t205 @t196 @t82 @t202 @t196 @t119 @t120 @t8 @t3 @t2 @t94 @t95 @t42 @t5 @t3 @t99 @t74 @t176 @t52 @t3 @t6 @t39 @t9 @t36 @t10 @t11 @t37 @t40 @t15 @t164 @t18 @t163))) % 0.46/0.64 (assume-push @p428 @t18) % 0.46/0.64 (step-pop @p429 :rule scope :premises (@p34)) % 0.46/0.64 (step @p316 :rule process_scope :premises (@p429) :args (@t144)) % 0.46/0.64 (step @p318 :rule implies_elim :premises (@p316)) % 0.46/0.64 (assume-push @p430 @t24) % 0.46/0.64 (step-pop @p431 :rule scope :premises (@p289)) % 0.46/0.64 (step @p320 :rule process_scope :premises (@p431) :args (@t201)) % 0.46/0.64 (step @p322 :rule implies_elim :premises (@p320)) % 0.46/0.64 (assume-push @p432 @t23) % 0.46/0.64 (step-pop @p433 :rule scope :premises (@p264)) % 0.46/0.64 (step @p324 :rule process_scope :premises (@p433) :args (@t193)) % 0.46/0.64 (step @p326 :rule implies_elim :premises (@p324)) % 0.46/0.64 (assume-push @p434 @t18) % 0.46/0.64 (step-pop @p435 :rule scope :premises (@p94)) % 0.46/0.64 (step @p328 :rule process_scope :premises (@p435) :args (@t83)) % 0.46/0.64 (step @p330 :rule implies_elim :premises (@p328)) % 0.46/0.64 (assume-push @p436 @t24) % 0.46/0.64 (step-pop @p437 :rule scope :premises (@p293)) % 0.46/0.64 (step @p332 :rule process_scope :premises (@p437) :args (@t202)) % 0.46/0.64 (step @p334 :rule implies_elim :premises (@p332)) % 0.46/0.64 (assume-push @p438 @t18) % 0.46/0.64 (step-pop @p439 :rule scope :premises (@p36)) % 0.46/0.64 (step @p336 :rule process_scope :premises (@p439) :args (@t95)) % 0.46/0.64 (step @p338 :rule implies_elim :premises (@p336)) % 0.46/0.64 (assume-push @p440 @t15) % 0.46/0.64 (step-pop @p441 :rule scope :premises (@p37)) % 0.46/0.64 (step @p340 :rule process_scope :premises (@p441) :args (@t43)) % 0.46/0.64 (step @p342 :rule implies_elim :premises (@p340)) % 0.46/0.64 (step @p343 :rule chain_m_resolution :premises (@p262 @p260 @p130 @p128 @p8 @p3 @p2 @p230 @p221 @p46 @p4 @p2 @p273 @p271 @p138 @p136 @p107 @p39 @p342 @p338 @p295 @p334 @p97 @p5 @p330 @p78 @p10 @p68 @p266 @p326 @p14 @p155 @p241 @p23 @p72 @p291 @p276 @p1 @p288 @p20 @p7 @p8 @p76 @p12 @p274 @p322 @p15 @p144 @p3 @p4 @p9 @p318 @p13 @p314) :args ((or @t132 @t130) (@list false false false false false false false false false false false true false true false false false false false true false false false false false false false true false false false false false false true false false false false false false false false true false false false false false false false false true) (@list @t192 @t119 @t120 @t8 @t3 @t2 @t185 @t186 @t44 @t4 @t2 @t99 @t195 @t133 @t135 @t74 @t42 @t43 @t95 @t94 @t202 @t82 @t5 @t83 @t58 @t10 @t64 @t72 @t193 @t23 @t151 @t157 @t32 @t33 @t156 @t196 @t1 @t197 @t27 @t7 @t8 @t28 @t15 @t54 @t201 @t24 @t140 @t3 @t4 @t9 @t144 @t18 @t143))) % 0.46/0.64 (step @p344 :rule instantiate :premises (@p15) :args (@t206)) % 0.46/0.64 (step @p345 :rule cnf_or_pos :args (@t208)) % 0.46/0.64 (step @p346 :rule reordering :premises (@p345) :args ((or @t117 @t123 @t89 (not @t208)))) % 0.46/0.64 (step @p347 :rule instantiate :premises (@p14) :args (@t115)) % 0.46/0.64 (step @p348 :rule cnf_or_pos :args (@t209)) % 0.46/0.64 (step @p349 :rule reordering :premises (@p348) :args ((or @t104 @t98 @t51 (not @t209)))) % 0.46/0.64 (step @p350 :rule chain_m_resolution :premises (@p349 @p347 @p120 @p118 @p114 @p6 @p2 @p123 @p121 @p7 @p2 @p1 @p218 @p216 @p346 @p344 @p135 @p49 @p41 @p5 @p2 @p343 @p87 @p105 @p82 @p6 @p1 @p103 @p101 @p100 @p98 @p11 @p6 @p5 @p93 @p91 @p107 @p36 @p40 @p5 @p3 @p295 @p293 @p277 @p97 @p95 @p94 @p5 @p1 @p266 @p264 @p155 @p24 @p16 @p4 @p1 @p291 @p289 @p277 @p144 @p34 @p9 @p4 @p3 @p314 @p161 @p25 @p33 @p6 @p3 @p299) :args (@t132 (@list false false false false false false false false false false false true false true false false false false false false true false false false false false true false false false false false false true false false false false false false true false false false false false false false true false false false false false false true false false false false false false false true false false false false false true) (@list @t209 @t97 @t107 @t112 @t6 @t2 @t103 @t114 @t7 @t2 @t1 @t111 @t183 @t113 @t208 @t122 @t47 @t128 @t5 @t2 @t127 @t50 @t60 @t70 @t6 @t1 @t69 @t90 @t84 @t85 @t11 @t6 @t5 @t78 @t80 @t74 @t95 @t42 @t5 @t3 @t94 @t202 @t196 @t82 @t58 @t83 @t5 @t1 @t72 @t193 @t151 @t32 @t157 @t4 @t1 @t156 @t201 @t196 @t140 @t144 @t9 @t4 @t3 @t143 @t52 @t164 @t39 @t6 @t3 @t163))) % 0.46/0.64 (step @p351 :rule chain_m_resolution :premises (@p140 @p4 @p5 @p10 @p350 @p50) :args (@t137 @t210 (@list @t4 @t5 @t10 @t131 @t138))) % 0.46/0.64 (assume-push @p442 @t24) % 0.46/0.64 (step-pop @p443 :rule scope :premises (@p268)) % 0.46/0.64 (step @p353 :rule process_scope :premises (@p443) :args (@t194)) % 0.46/0.64 (step @p355 :rule implies_elim :premises (@p353)) % 0.46/0.64 (assume-push @p444 @t18) % 0.46/0.64 (step-pop @p445 :rule scope :premises (@p50)) % 0.46/0.64 (step @p357 :rule process_scope :premises (@p445) :args (@t138)) % 0.46/0.64 (step @p359 :rule implies_elim :premises (@p357)) % 0.46/0.64 (step @p360 :rule instantiate :premises (@p14) :args (@t187)) % 0.46/0.64 (step @p361 :rule cnf_or_pos :args (@t211)) % 0.46/0.64 (step @p362 :rule reordering :premises (@p361) :args ((or @t104 @t134 @t152 (not @t211)))) % 0.46/0.64 (step @p363 :rule chain_m_resolution :premises (@p110 @p108 @p120 @p118 @p114 @p6 @p2 @p130 @p128 @p8 @p3 @p2 @p218 @p216 @p310 @p308 @p277 @p100 @p98 @p11 @p6 @p5 @p123 @p121 @p7 @p2 @p1 @p93 @p91 @p362 @p360 @p161 @p25 @p33 @p6 @p3 @p107 @p36 @p40 @p5 @p3 @p155 @p24 @p16 @p4 @p1 @p292 @p142 @p35 @p351 @p291 @p289 @p277 @p230 @p2 @p45 @p8 @p9 @p228 @p12 @p224 @p270 @p140 @p4 @p5 @p10 @p359 @p13 @p350 @p355 @p15) :args ((or @t141 @t123) (@list false false false false false false false false false false false true false true false false false false false false false false false false false false true false true false false false false false false false false false false false false false false false false true true false false true false false false false false false false false false false true false false false false false false true false false) (@list @t101 @t97 @t107 @t112 @t6 @t2 @t99 @t120 @t8 @t3 @t2 @t111 @t183 @t119 @t205 @t196 @t84 @t85 @t11 @t6 @t5 @t113 @t114 @t7 @t2 @t1 @t78 @t80 @t103 @t211 @t52 @t164 @t39 @t6 @t3 @t74 @t95 @t42 @t5 @t3 @t151 @t32 @t157 @t4 @t1 @t163 @t94 @t142 @t137 @t156 @t201 @t196 @t133 @t2 @t44 @t8 @t9 @t45 @t15 @t186 @t185 @t137 @t4 @t5 @t10 @t138 @t18 @t131 @t194 @t24))) % 0.46/0.64 (step @p364 :rule chain_m_resolution :premises (@p197 @p195 @p351 @p100 @p98 @p11 @p6 @p5 @p153 @p151 @p30 @p6 @p4 @p93 @p91 @p147 @p145) :args ((or @t148 @t75 @t53) (@list false false false false false false false false false false false false true false true false) (@list @t174 @t137 @t84 @t85 @t11 @t6 @t5 @t154 @t155 @t36 @t6 @t4 @t78 @t80 @t146 @t149))) % 0.46/0.64 (step @p365 :rule chain_m_resolution :premises (@p349 @p347 @p120 @p118 @p114 @p6 @p2 @p87 @p105 @p82 @p6 @p1 @p176 @p174 @p280 @p278 @p277 @p161 @p25 @p33 @p6 @p3 @p364 @p107 @p36 @p40 @p5 @p3 @p123 @p121 @p7 @p2 @p1 @p133 @p131 @p310 @p308 @p277 @p130 @p128 @p8 @p3 @p2 @p208 @p206 @p144 @p34 @p9 @p4 @p3 @p363 @p230 @p221 @p46 @p4 @p2 @p270 @p268 @p351) :args (@t123 (@list false false false false false false false false false false false true false true false false false false false false false true false false false false false false false false false false true false true false false false false false false false true false false false false false false true false false false false false true false false) (@list @t209 @t97 @t107 @t112 @t6 @t2 @t50 @t60 @t70 @t6 @t1 @t111 @t166 @t69 @t200 @t196 @t163 @t164 @t39 @t6 @t3 @t52 @t74 @t95 @t42 @t5 @t3 @t103 @t114 @t7 @t2 @t1 @t94 @t126 @t113 @t205 @t196 @t119 @t120 @t8 @t3 @t2 @t99 @t180 @t143 @t144 @t9 @t4 @t3 @t140 @t133 @t186 @t44 @t4 @t2 @t185 @t194 @t137))) % 0.46/0.64 (step @p366 :rule chain_m_resolution :premises (@p135 @p2 @p5 @p365 @p49 @p41) :args (@t127 @t198 (@list @t2 @t5 @t122 @t47 @t128))) % 0.46/0.64 (step @p367 :rule chain_m_resolution :premises (@p349 @p347 @p120 @p118 @p114 @p6 @p2 @p87 @p105 @p82 @p6 @p1 @p176 @p174 @p280 @p278 @p277 @p161 @p25 @p33 @p6 @p3 @p364 @p144 @p34 @p9 @p4 @p3 @p262 @p260 @p230 @p221 @p46 @p4 @p2 @p362 @p360 @p155 @p24 @p16 @p4 @p1 @p204 @p202 @p351 @p97 @p95 @p94 @p5 @p1 @p313 @p311 @p366 @p123 @p121 @p7 @p2 @p1 @p310 @p308 @p277 @p130 @p128 @p8 @p3 @p2 @p273 @p271 @p366) :args (@t75 (@list false false false false false false false false false false false true false true false false false false false false false true false false false false false true false false false false false false true false false false false false false true false false false false false false false true false false false false false false false true false false false false false false false true false false) (@list @t209 @t97 @t107 @t112 @t6 @t2 @t50 @t60 @t70 @t6 @t1 @t111 @t166 @t69 @t200 @t196 @t163 @t164 @t39 @t6 @t3 @t52 @t143 @t144 @t9 @t4 @t3 @t140 @t192 @t185 @t186 @t44 @t4 @t2 @t133 @t211 @t151 @t32 @t157 @t4 @t1 @t156 @t178 @t137 @t82 @t58 @t83 @t5 @t1 @t72 @t207 @t127 @t103 @t114 @t7 @t2 @t1 @t113 @t205 @t196 @t119 @t120 @t8 @t3 @t2 @t99 @t195 @t127))) % 0.46/0.64 (step @p368 :rule chain_m_resolution :premises (@p107 @p3 @p5 @p367 @p40 @p36) :args (@t94 @t198 (@list @t3 @t5 @t74 @t42 @t95))) % 0.46/0.64 (step @p369 :rule chain_m_resolution :premises (@p142 @p351 @p368 @p35) :args (@t141 @t29 (@list @t137 @t94 @t142))) % 0.46/0.64 (step @p370 :rule chain_m_resolution :premises (@p144 @p3 @p4 @p9 @p369 @p34) :args (@t143 @t210 (@list @t3 @t4 @t9 @t140 @t144))) % 0.46/0.64 (step @p371 :rule chain_m_resolution :premises (@p295 @p368 @p277 @p293) :args (@t89 @t29 (@list @t94 @t196 @t202))) % 0.46/0.64 (step @p372 :rule chain_m_resolution :premises (@p97 @p1 @p5 @p371 @p95 @p94) :args (@t72 @t198 (@list @t1 @t5 @t82 @t58 @t83))) % 0.46/0.64 (step @p373 :rule chain_m_resolution :premises (@p313 @p366 @p372 @p311) :args (@t104 @t29 (@list @t127 @t72 @t207))) % 0.46/0.64 (step @p374 :rule chain_m_resolution :premises (@p123 @p1 @p2 @p7 @p373 @p121) :args (@t113 @t210 (@list @t1 @t2 @t7 @t103 @t114))) % 0.46/0.64 (step @p375 :rule chain_m_resolution :premises (@p310 @p374 @p277 @p308) :args (@t125 @t29 (@list @t113 @t196 @t205))) % 0.46/0.64 (step @p376 :rule chain_m_resolution :premises (@p130 @p2 @p3 @p8 @p375 @p128) :args (@t99 @t210 (@list @t2 @t3 @t8 @t119 @t120))) % 0.46/0.64 (step @p377 :rule chain_m_resolution :premises (@p307 @p376 @p370) :args (@t53 (@list false false) (@list @t99 @t143))) % 0.46/0.64 (step @p378 :rule chain_m_resolution :premises (@p161 @p3 @p6 @p377 @p33 @p25) :args (@t163 @t198 (@list @t3 @t6 @t52 @t39 @t164))) % 0.46/0.64 (step @p379 :rule chain_m_resolution :premises (@p208 @p376 @p370 @p206) :args (@t134 @t29 (@list @t99 @t143 @t180))) % 0.46/0.64 (step @p380 :rule chain_m_resolution :premises (@p230 @p2 @p4 @p379 @p46 @p221) :args (@t185 @t198 (@list @t2 @t4 @t133 @t44 @t186))) % 0.46/0.64 (step @p381 :rule chain_m_resolution :premises (@p306 @p304 @p120 @p118 @p114 @p6 @p2 @p153 @p151 @p30 @p6 @p4 @p194 @p192 @p211 @p209 @p100 @p98 @p11 @p6 @p5 @p87 @p105 @p82 @p6 @p1 @p257 @p255 @p280 @p278 @p277) :args ((or @t188 @t124 @t152 @t130 @t165) (@list false false false false false false false false false false false true false true false false false false false false false false false false false true false true false false) (@list @t204 @t111 @t107 @t112 @t6 @t2 @t154 @t155 @t36 @t6 @t4 @t97 @t172 @t146 @t181 @t78 @t85 @t11 @t6 @t5 @t50 @t60 @t70 @t6 @t1 @t84 @t191 @t69 @t200 @t196))) % 0.46/0.64 (step @p382 :rule chain_m_resolution :premises (@p140 @p50 @p10 @p5 @p4 @p270 @p268 @p266 @p264 @p135 @p49 @p41 @p5 @p2 @p97 @p95 @p94 @p5 @p1 @p381 @p295 @p293 @p277) :args ((or @t188 @t124 @t152 @t165) (@list false false false false true false true false false false false false false false false false false false true true false false) (@list @t138 @t10 @t5 @t4 @t137 @t194 @t131 @t193 @t122 @t47 @t128 @t5 @t2 @t72 @t58 @t83 @t5 @t1 @t127 @t82 @t202 @t196))) % 0.46/0.64 (step @p383 :rule chain_m_resolution :premises (@p382 @p380 @p368 @p378) :args (@t152 @t29 (@list @t185 @t94 @t163))) % 0.46/0.64 (step @p384 :rule chain_m_resolution :premises (@p233 @p374 @p380 @p231) :args (@t160 @t29 (@list @t113 @t185 @t189))) % 0.46/0.64 (step @p385 false :rule chain_m_resolution :premises (@p155 @p384 @p383 @p24 @p16 @p4 @p1) :args (false (@list true true false false false false) (@list @t156 @t151 @t32 @t157 @t4 @t1))) % 0.46/0.64 ) % 0.46/0.64 % SZS output end Proof % 0.46/0.64 % cvc5 exiting %------------------------------------------------------------------------------