%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : SYO181^5 : TPTP v9.2.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n012.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jun 3 09:12:10 AM UTC 2026 % Result : Theorem 0.23s 0.43s % Output : Proof 0.23s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.07 % Problem : SYO181^5 : TPTP v9.2.1. Released v4.0.0. % 0.00/0.07 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.26 % Computer : n012.cluster.edu % 0.09/0.26 % Model : x86_64 x86_64 % 0.09/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.26 % Memory : 8042.1875MB % 0.09/0.26 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.26 % CPULimit : 300 % 0.09/0.26 % WCLimit : 300 % 0.09/0.26 % DateTime : Wed Jun 3 00:00:03 EDT 2026 % 0.09/0.26 % CPUTime : % 0.15/0.34 %----Proving TH0 % 0.23/0.43 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-cegqi --no-sygus-inst at 90s... % 0.23/0.43 % SZS status Theorem % 0.23/0.43 % SZS output start Proof % 0.23/0.43 ( % 0.23/0.43 (declare-const tptp.q01 Bool) % 0.23/0.43 (declare-const tptp.q02 Bool) % 0.23/0.43 (declare-const tptp.q03 Bool) % 0.23/0.43 (declare-const tptp.q04 Bool) % 0.23/0.43 (declare-const tptp.q05 Bool) % 0.23/0.43 (declare-const tptp.q06 Bool) % 0.23/0.43 (declare-const tptp.p01 Bool) % 0.23/0.43 (declare-const tptp.q10 Bool) % 0.23/0.43 (declare-const tptp.p02 Bool) % 0.23/0.43 (declare-const tptp.q11 Bool) % 0.23/0.43 (declare-const tptp.p03 Bool) % 0.23/0.43 (declare-const tptp.q12 Bool) % 0.23/0.43 (declare-const tptp.p04 Bool) % 0.23/0.43 (declare-const tptp.q13 Bool) % 0.23/0.43 (declare-const tptp.p05 Bool) % 0.23/0.43 (declare-const tptp.q14 Bool) % 0.23/0.43 (declare-const tptp.p06 Bool) % 0.23/0.43 (declare-const tptp.q15 Bool) % 0.23/0.43 (declare-const tptp.p07 Bool) % 0.23/0.43 (declare-const tptp.q16 Bool) % 0.23/0.43 (declare-const tptp.p10 Bool) % 0.23/0.43 (declare-const tptp.p11 Bool) % 0.23/0.43 (declare-const tptp.q20 Bool) % 0.23/0.43 (declare-const tptp.p12 Bool) % 0.23/0.43 (declare-const tptp.q21 Bool) % 0.23/0.43 (declare-const tptp.p13 Bool) % 0.23/0.43 (declare-const tptp.q22 Bool) % 0.23/0.43 (declare-const tptp.p14 Bool) % 0.23/0.43 (declare-const tptp.q23 Bool) % 0.23/0.43 (declare-const tptp.p15 Bool) % 0.23/0.43 (declare-const tptp.q24 Bool) % 0.23/0.43 (declare-const tptp.p16 Bool) % 0.23/0.43 (declare-const tptp.q25 Bool) % 0.23/0.43 (declare-const tptp.p17 Bool) % 0.23/0.43 (declare-const tptp.q26 Bool) % 0.23/0.43 (declare-const tptp.p20 Bool) % 0.23/0.43 (declare-const tptp.p21 Bool) % 0.23/0.43 (declare-const tptp.q30 Bool) % 0.23/0.43 (declare-const tptp.p22 Bool) % 0.23/0.43 (declare-const tptp.q31 Bool) % 0.23/0.43 (declare-const tptp.p23 Bool) % 0.23/0.43 (declare-const tptp.q32 Bool) % 0.23/0.43 (declare-const tptp.p24 Bool) % 0.23/0.43 (declare-const tptp.q33 Bool) % 0.23/0.43 (declare-const tptp.p25 Bool) % 0.23/0.43 (declare-const tptp.q34 Bool) % 0.23/0.43 (declare-const tptp.p26 Bool) % 0.23/0.43 (declare-const tptp.q35 Bool) % 0.23/0.43 (declare-const tptp.p27 Bool) % 0.23/0.43 (declare-const tptp.q56 Bool) % 0.23/0.43 (declare-const tptp.p50 Bool) % 0.23/0.43 (declare-const tptp.p51 Bool) % 0.23/0.43 (declare-const tptp.q60 Bool) % 0.23/0.43 (declare-const tptp.p52 Bool) % 0.23/0.43 (declare-const tptp.q61 Bool) % 0.23/0.43 (declare-const tptp.p53 Bool) % 0.23/0.43 (declare-const tptp.q62 Bool) % 0.23/0.43 (declare-const tptp.p54 Bool) % 0.23/0.43 (declare-const tptp.q63 Bool) % 0.23/0.43 (declare-const tptp.p55 Bool) % 0.23/0.43 (declare-const tptp.q64 Bool) % 0.23/0.43 (declare-const tptp.p56 Bool) % 0.23/0.43 (declare-const tptp.q65 Bool) % 0.23/0.43 (declare-const tptp.p57 Bool) % 0.23/0.43 (declare-const tptp.q66 Bool) % 0.23/0.43 (declare-const tptp.q75 Bool) % 0.23/0.43 (declare-const tptp.p66 Bool) % 0.23/0.43 (declare-const tptp.q74 Bool) % 0.23/0.43 (declare-const tptp.p65 Bool) % 0.23/0.43 (declare-const tptp.q73 Bool) % 0.23/0.43 (declare-const tptp.p64 Bool) % 0.23/0.43 (declare-const tptp.q72 Bool) % 0.23/0.43 (declare-const tptp.p63 Bool) % 0.23/0.43 (declare-const tptp.q71 Bool) % 0.23/0.43 (declare-const tptp.p62 Bool) % 0.23/0.43 (declare-const tptp.q70 Bool) % 0.23/0.43 (declare-const tptp.p61 Bool) % 0.23/0.43 (declare-const tptp.p60 Bool) % 0.23/0.43 (declare-const tptp.p47 Bool) % 0.23/0.43 (declare-const tptp.q55 Bool) % 0.23/0.43 (declare-const tptp.p46 Bool) % 0.23/0.43 (declare-const tptp.q54 Bool) % 0.23/0.43 (declare-const tptp.p45 Bool) % 0.23/0.43 (declare-const tptp.q53 Bool) % 0.23/0.43 (declare-const tptp.p44 Bool) % 0.23/0.43 (declare-const tptp.q52 Bool) % 0.23/0.43 (declare-const tptp.p43 Bool) % 0.23/0.43 (declare-const tptp.q51 Bool) % 0.23/0.43 (declare-const tptp.p42 Bool) % 0.23/0.43 (declare-const tptp.q50 Bool) % 0.23/0.43 (declare-const tptp.p41 Bool) % 0.23/0.43 (declare-const tptp.p40 Bool) % 0.23/0.43 (declare-const tptp.q46 Bool) % 0.23/0.43 (declare-const tptp.p37 Bool) % 0.23/0.43 (declare-const tptp.q45 Bool) % 0.23/0.43 (declare-const tptp.p36 Bool) % 0.23/0.43 (declare-const tptp.q44 Bool) % 0.23/0.43 (declare-const tptp.p35 Bool) % 0.23/0.43 (declare-const tptp.q43 Bool) % 0.23/0.43 (declare-const tptp.p34 Bool) % 0.23/0.43 (declare-const tptp.q42 Bool) % 0.23/0.43 (declare-const tptp.p33 Bool) % 0.23/0.43 (declare-const tptp.q41 Bool) % 0.23/0.43 (declare-const tptp.p32 Bool) % 0.23/0.43 (declare-const tptp.q40 Bool) % 0.23/0.43 (declare-const tptp.p31 Bool) % 0.23/0.43 (declare-const tptp.p30 Bool) % 0.23/0.43 (declare-const tptp.q36 Bool) % 0.23/0.43 (define @t1 () (not tptp.q61)) % 0.23/0.43 (define @t2 () (not tptp.q75)) % 0.23/0.43 (define @t3 () (not tptp.q65)) % 0.23/0.43 (define @t4 () (not tptp.q66)) % 0.23/0.43 (define @t5 () (and @t4 @t3 @t2)) % 0.23/0.43 (define @t6 () (not tptp.p66)) % 0.23/0.43 (define @t7 () (not tptp.q74)) % 0.23/0.43 (define @t8 () (not tptp.q64)) % 0.23/0.43 (define @t9 () (and @t3 @t8 @t7 @t2)) % 0.23/0.43 (define @t10 () (not tptp.p65)) % 0.23/0.43 (define @t11 () (not tptp.q73)) % 0.23/0.43 (define @t12 () (not tptp.q63)) % 0.23/0.43 (define @t13 () (and @t8 @t12 @t11 @t7)) % 0.23/0.43 (define @t14 () (not tptp.p64)) % 0.23/0.43 (define @t15 () (not tptp.q72)) % 0.23/0.43 (define @t16 () (not tptp.q62)) % 0.23/0.43 (define @t17 () (and @t12 @t16 @t15 @t11)) % 0.23/0.43 (define @t18 () (not tptp.p63)) % 0.23/0.43 (define @t19 () (not tptp.q71)) % 0.23/0.43 (define @t20 () (and @t16 @t1 @t19 @t15)) % 0.23/0.43 (define @t21 () (not tptp.p62)) % 0.23/0.43 (define @t22 () (not tptp.q70)) % 0.23/0.43 (define @t23 () (not tptp.q60)) % 0.23/0.43 (define @t24 () (and @t1 @t23 @t22 @t19)) % 0.23/0.43 (define @t25 () (not tptp.p61)) % 0.23/0.43 (define @t26 () (and @t23 @t22)) % 0.23/0.43 (define @t27 () (not tptp.p60)) % 0.23/0.43 (define @t28 () (not tptp.q56)) % 0.23/0.43 (define @t29 () (and @t28 @t4)) % 0.23/0.43 (define @t30 () (not tptp.p57)) % 0.23/0.43 (define @t31 () (not tptp.q55)) % 0.23/0.43 (define @t32 () (and @t28 @t31 @t3 @t4)) % 0.23/0.43 (define @t33 () (not tptp.p56)) % 0.23/0.43 (define @t34 () (not tptp.q54)) % 0.23/0.43 (define @t35 () (and @t31 @t34 @t8 @t3)) % 0.23/0.43 (define @t36 () (not tptp.p55)) % 0.23/0.43 (define @t37 () (not tptp.q53)) % 0.23/0.43 (define @t38 () (and @t34 @t37 @t12 @t8)) % 0.23/0.43 (define @t39 () (not tptp.p54)) % 0.23/0.43 (define @t40 () (not tptp.q52)) % 0.23/0.43 (define @t41 () (and @t37 @t40 @t16 @t12)) % 0.23/0.43 (define @t42 () (not tptp.p53)) % 0.23/0.43 (define @t43 () (not tptp.q51)) % 0.23/0.43 (define @t44 () (and @t40 @t43 @t1 @t16)) % 0.23/0.43 (define @t45 () (not tptp.p52)) % 0.23/0.43 (define @t46 () (not tptp.q50)) % 0.23/0.43 (define @t47 () (and @t43 @t46 @t23 @t1)) % 0.23/0.43 (define @t48 () (not tptp.p51)) % 0.23/0.43 (define @t49 () (and @t46 @t23)) % 0.23/0.43 (define @t50 () (not tptp.p50)) % 0.23/0.43 (define @t51 () (not tptp.q46)) % 0.23/0.43 (define @t52 () (and @t51 @t28)) % 0.23/0.43 (define @t53 () (not tptp.p47)) % 0.23/0.43 (define @t54 () (not tptp.q45)) % 0.23/0.43 (define @t55 () (and @t51 @t54 @t31 @t28)) % 0.23/0.43 (define @t56 () (not tptp.p46)) % 0.23/0.43 (define @t57 () (not tptp.q44)) % 0.23/0.43 (define @t58 () (and @t54 @t57 @t34 @t31)) % 0.23/0.43 (define @t59 () (not tptp.p45)) % 0.23/0.43 (define @t60 () (not tptp.q43)) % 0.23/0.43 (define @t61 () (and @t57 @t60 @t37 @t34)) % 0.23/0.43 (define @t62 () (not tptp.p44)) % 0.23/0.43 (define @t63 () (not tptp.q42)) % 0.23/0.43 (define @t64 () (and @t60 @t63 @t40 @t37)) % 0.23/0.43 (define @t65 () (not tptp.p43)) % 0.23/0.43 (define @t66 () (not tptp.q41)) % 0.23/0.43 (define @t67 () (and @t63 @t66 @t43 @t40)) % 0.23/0.43 (define @t68 () (not tptp.p42)) % 0.23/0.43 (define @t69 () (not tptp.q40)) % 0.23/0.43 (define @t70 () (and @t66 @t69 @t46 @t43)) % 0.23/0.43 (define @t71 () (not tptp.p41)) % 0.23/0.43 (define @t72 () (and @t69 @t46)) % 0.23/0.43 (define @t73 () (not tptp.p40)) % 0.23/0.43 (define @t74 () (not tptp.q36)) % 0.23/0.43 (define @t75 () (and @t74 @t51)) % 0.23/0.43 (define @t76 () (not tptp.p37)) % 0.23/0.43 (define @t77 () (not tptp.q35)) % 0.23/0.43 (define @t78 () (and @t74 @t77 @t54 @t51)) % 0.23/0.43 (define @t79 () (not tptp.p36)) % 0.23/0.43 (define @t80 () (not tptp.q34)) % 0.23/0.43 (define @t81 () (and @t77 @t80 @t57 @t54)) % 0.23/0.43 (define @t82 () (not tptp.p35)) % 0.23/0.43 (define @t83 () (not tptp.q33)) % 0.23/0.43 (define @t84 () (and @t80 @t83 @t60 @t57)) % 0.23/0.43 (define @t85 () (not tptp.p34)) % 0.23/0.43 (define @t86 () (not tptp.q32)) % 0.23/0.43 (define @t87 () (and @t83 @t86 @t63 @t60)) % 0.23/0.43 (define @t88 () (not tptp.p33)) % 0.23/0.43 (define @t89 () (not tptp.q31)) % 0.23/0.43 (define @t90 () (and @t86 @t89 @t66 @t63)) % 0.23/0.43 (define @t91 () (not tptp.p32)) % 0.23/0.43 (define @t92 () (not tptp.q30)) % 0.23/0.43 (define @t93 () (and @t89 @t92 @t69 @t66)) % 0.23/0.43 (define @t94 () (not tptp.p31)) % 0.23/0.43 (define @t95 () (and @t92 @t69)) % 0.23/0.43 (define @t96 () (not tptp.p30)) % 0.23/0.43 (define @t97 () (not tptp.q26)) % 0.23/0.43 (define @t98 () (and @t97 @t74)) % 0.23/0.43 (define @t99 () (not tptp.p27)) % 0.23/0.43 (define @t100 () (not tptp.q25)) % 0.23/0.43 (define @t101 () (and @t97 @t100 @t77 @t74)) % 0.23/0.43 (define @t102 () (not tptp.p26)) % 0.23/0.43 (define @t103 () (not tptp.q24)) % 0.23/0.43 (define @t104 () (and @t100 @t103 @t80 @t77)) % 0.23/0.43 (define @t105 () (not tptp.p25)) % 0.23/0.43 (define @t106 () (not tptp.q23)) % 0.23/0.43 (define @t107 () (and @t103 @t106 @t83 @t80)) % 0.23/0.43 (define @t108 () (not tptp.p24)) % 0.23/0.43 (define @t109 () (not tptp.q22)) % 0.23/0.43 (define @t110 () (and @t106 @t109 @t86 @t83)) % 0.23/0.43 (define @t111 () (not tptp.p23)) % 0.23/0.43 (define @t112 () (not tptp.q21)) % 0.23/0.43 (define @t113 () (and @t109 @t112 @t89 @t86)) % 0.23/0.43 (define @t114 () (not tptp.p22)) % 0.23/0.43 (define @t115 () (not tptp.q20)) % 0.23/0.43 (define @t116 () (and @t112 @t115 @t92 @t89)) % 0.23/0.43 (define @t117 () (not tptp.p21)) % 0.23/0.43 (define @t118 () (and @t115 @t92)) % 0.23/0.43 (define @t119 () (not tptp.p20)) % 0.23/0.43 (define @t120 () (not tptp.q16)) % 0.23/0.43 (define @t121 () (and @t120 @t97)) % 0.23/0.43 (define @t122 () (not tptp.p17)) % 0.23/0.43 (define @t123 () (not tptp.q15)) % 0.23/0.43 (define @t124 () (and @t120 @t123 @t100 @t97)) % 0.23/0.43 (define @t125 () (not tptp.p16)) % 0.23/0.43 (define @t126 () (not tptp.q14)) % 0.23/0.43 (define @t127 () (and @t123 @t126 @t103 @t100)) % 0.23/0.43 (define @t128 () (not tptp.p15)) % 0.23/0.43 (define @t129 () (not tptp.q13)) % 0.23/0.43 (define @t130 () (and @t126 @t129 @t106 @t103)) % 0.23/0.43 (define @t131 () (not tptp.p14)) % 0.23/0.43 (define @t132 () (not tptp.q12)) % 0.23/0.43 (define @t133 () (and @t129 @t132 @t109 @t106)) % 0.23/0.43 (define @t134 () (not tptp.p13)) % 0.23/0.43 (define @t135 () (not tptp.q11)) % 0.23/0.43 (define @t136 () (and @t132 @t135 @t112 @t109)) % 0.23/0.43 (define @t137 () (not tptp.p12)) % 0.23/0.43 (define @t138 () (not tptp.q10)) % 0.23/0.43 (define @t139 () (and @t135 @t138 @t115 @t112)) % 0.23/0.43 (define @t140 () (not tptp.p11)) % 0.23/0.43 (define @t141 () (and @t138 @t115)) % 0.23/0.43 (define @t142 () (not tptp.p10)) % 0.23/0.43 (define @t143 () (not tptp.q06)) % 0.23/0.43 (define @t144 () (and @t143 @t120)) % 0.23/0.43 (define @t145 () (not tptp.p07)) % 0.23/0.43 (define @t146 () (not tptp.q05)) % 0.23/0.43 (define @t147 () (and @t143 @t146 @t123 @t120)) % 0.23/0.43 (define @t148 () (not tptp.p06)) % 0.23/0.43 (define @t149 () (not tptp.q04)) % 0.23/0.43 (define @t150 () (and @t146 @t149 @t126 @t123)) % 0.23/0.43 (define @t151 () (not tptp.p05)) % 0.23/0.43 (define @t152 () (not tptp.q03)) % 0.23/0.43 (define @t153 () (and @t149 @t152 @t129 @t126)) % 0.23/0.43 (define @t154 () (not tptp.p04)) % 0.23/0.43 (define @t155 () (not tptp.q02)) % 0.23/0.43 (define @t156 () (and @t152 @t155 @t132 @t129)) % 0.23/0.43 (define @t157 () (not tptp.p03)) % 0.23/0.43 (define @t158 () (not tptp.q01)) % 0.23/0.43 (define @t159 () (and @t155 @t158 @t135 @t132)) % 0.23/0.43 (define @t160 () (not tptp.p02)) % 0.23/0.43 (define @t161 () (and @t158 @t138 @t135)) % 0.23/0.43 (define @t162 () (not tptp.p01)) % 0.23/0.43 (define @t163 () (and @t19 @t11)) % 0.23/0.43 (define @t164 () (and @t16 @t8)) % 0.23/0.43 (define @t165 () (and @t1 @t12)) % 0.23/0.43 (define @t166 () (and @t23 @t16)) % 0.23/0.43 (define @t167 () (and @t37 @t31)) % 0.23/0.43 (define @t168 () (and @t43 @t37)) % 0.23/0.43 (define @t169 () (and @t63 @t57)) % 0.23/0.43 (define @t170 () (and @t69 @t63)) % 0.23/0.43 (define @t171 () (and @t83 @t77)) % 0.23/0.43 (define @t172 () (and @t89 @t83)) % 0.23/0.43 (define @t173 () (and @t109 @t103)) % 0.23/0.43 (define @t174 () (and @t115 @t109)) % 0.23/0.43 (define @t175 () (and @t129 @t123)) % 0.23/0.43 (define @t176 () (and @t135 @t129)) % 0.23/0.43 (define @t177 () (and @t155 @t149)) % 0.23/0.43 (define @t178 () (and @t82 @t36)) % 0.23/0.43 (define @t179 () (and @t88 @t42)) % 0.23/0.43 (define @t180 () (and @t94 @t48)) % 0.23/0.43 (define @t181 () (and @t102 @t56)) % 0.23/0.43 (define @t182 () (and @t108 @t62)) % 0.23/0.43 (define @t183 () (and @t114 @t68)) % 0.23/0.43 (define @t184 () (and @t119 @t73)) % 0.23/0.43 (define @t185 () (and @t122 @t76)) % 0.23/0.43 (define @t186 () (and @t128 @t82)) % 0.23/0.43 (define @t187 () (and @t134 @t88)) % 0.23/0.43 (define @t188 () (and @t140 @t94)) % 0.23/0.43 (define @t189 () (and @t142 @t96)) % 0.23/0.43 (define @t190 () (and @t148 @t102)) % 0.23/0.43 (define @t191 () (and @t154 @t108)) % 0.23/0.43 (define @t192 () (and @t160 @t114)) % 0.23/0.43 (define @t193 () (and (or @t162 @t140) (or @t160 @t137) (or @t157 @t134) (or @t154 @t131) (or @t151 @t128) (or @t148 @t125) (or @t145 @t122) (or @t142 @t119) (or @t140 (and @t162 @t117)) (or @t137 @t192) (or @t134 (and @t157 @t111)) (or @t131 @t191) (or @t128 (and @t151 @t105)) (or @t125 @t190) (or @t122 (and @t145 @t99)) (or @t119 @t189) (or @t117 @t188) (or @t114 (and @t137 @t91)) (or @t111 @t187) (or @t108 (and @t131 @t85)) (or @t105 @t186) (or @t102 (and @t125 @t79)) (or @t99 @t185) (or @t96 @t184) (or @t94 (and @t117 @t71)) (or @t91 @t183) (or @t88 (and @t111 @t65)) (or @t85 @t182) (or @t82 (and @t105 @t59)) (or @t79 @t181) (or @t76 (and @t99 @t53)) (or @t73 (and @t96 @t50)) (or @t71 @t180) (or @t68 (and @t91 @t45)) (or @t65 @t179) (or @t62 (and @t85 @t39)) (or @t59 @t178) (or @t56 (and @t79 @t33)) (or @t53 (and @t76 @t30)) (or @t50 (and @t73 @t27)) (or @t48 (and @t71 @t25)) (or @t45 (and @t68 @t21)) (or @t42 (and @t65 @t18)) (or @t39 (and @t62 @t14)) (or @t36 (and @t59 @t10)) (or @t33 (and @t56 @t6)) (or @t30 @t53) (or @t27 @t50) (or @t25 @t48) (or @t21 @t45) (or @t18 @t42) (or @t14 @t39) (or @t10 @t36) (or @t6 @t33) (or @t158 @t155) (or @t155 (and @t158 @t152)) (or @t152 @t177) (or @t149 (and @t152 @t146)) (or @t146 (and @t149 @t143)) (or @t143 @t146) (or @t138 @t135) (or @t135 (and @t138 @t132)) (or @t132 @t176) (or @t129 (and @t132 @t126)) (or @t126 @t175) (or @t123 (and @t126 @t120)) (or @t120 @t123) (or @t115 @t112) (or @t112 @t174) (or @t109 (and @t112 @t106)) (or @t106 @t173) (or @t103 (and @t106 @t100)) (or @t100 (and @t103 @t97)) (or @t97 @t100) (or @t92 @t89) (or @t89 (and @t92 @t86)) (or @t86 @t172) (or @t83 (and @t86 @t80)) (or @t80 @t171) (or @t77 (and @t80 @t74)) (or @t74 @t77) (or @t69 @t66) (or @t66 @t170) (or @t63 (and @t66 @t60)) (or @t60 @t169) (or @t57 (and @t60 @t54)) (or @t54 (and @t57 @t51)) (or @t51 @t54) (or @t46 @t43) (or @t43 (and @t46 @t40)) (or @t40 @t168) (or @t37 (and @t40 @t34)) (or @t34 @t167) (or @t31 (and @t34 @t28)) (or @t28 @t31) (or @t23 @t1) (or @t1 @t166) (or @t16 @t165) (or @t12 @t164) (or @t8 (and @t12 @t3)) (or @t3 (and @t8 @t4)) (or @t4 @t3) (or @t22 @t19) (or @t19 (and @t22 @t15)) (or @t15 @t163) (or @t11 (and @t15 @t7)) (or @t7 (and @t11 @t2)) (or @t2 @t7) (or @t162 @t161) (or @t160 @t159) (or @t157 @t156) (or @t154 @t153) (or @t151 @t150) (or @t148 @t147) (or @t145 @t144) (or @t142 @t141) (or @t140 @t139) (or @t137 @t136) (or @t134 @t133) (or @t131 @t130) (or @t128 @t127) (or @t125 @t124) (or @t122 @t121) (or @t119 @t118) (or @t117 @t116) (or @t114 @t113) (or @t111 @t110) (or @t108 @t107) (or @t105 @t104) (or @t102 @t101) (or @t99 @t98) (or @t96 @t95) (or @t94 @t93) (or @t91 @t90) (or @t88 @t87) (or @t85 @t84) (or @t82 @t81) (or @t79 @t78) (or @t76 @t75) (or @t73 @t72) (or @t71 @t70) (or @t68 @t67) (or @t65 @t64) (or @t62 @t61) (or @t59 @t58) (or @t56 @t55) (or @t53 @t52) (or @t50 @t49) (or @t48 @t47) (or @t45 @t44) (or @t42 @t41) (or @t39 @t38) (or @t36 @t35) (or @t33 @t32) (or @t30 @t29) (or @t27 @t26) (or @t25 @t24) (or @t21 @t20) (or @t18 @t17) (or @t14 @t13) (or @t10 @t9) (or @t6 @t5) (or tptp.p01 tptp.q01) (or tptp.p02 tptp.q02 tptp.q01) (or tptp.p03 tptp.q03 tptp.q02) (or tptp.p04 tptp.q04 tptp.q03) (or tptp.p05 tptp.q05 tptp.q04) (or tptp.p06 tptp.q06 tptp.q05) (or tptp.p07 tptp.q06) (or tptp.p10 tptp.q10) (or tptp.p11 tptp.p01 tptp.q11 tptp.q10) (or tptp.p12 tptp.p02 tptp.q12 tptp.q11) (or tptp.p13 tptp.p03 tptp.q13 tptp.q12) (or tptp.p14 tptp.p04 tptp.q14 tptp.q13) (or tptp.p15 tptp.p05 tptp.q15 tptp.q14) (or tptp.p16 tptp.p06 tptp.q16 tptp.q15) (or tptp.p17 tptp.p07 tptp.q16) (or tptp.p20 tptp.p10 tptp.q20) (or tptp.p21 tptp.p11 tptp.q21 tptp.q20) (or tptp.p22 tptp.p12 tptp.q22 tptp.q21) (or tptp.p23 tptp.p13 tptp.q23 tptp.q22) (or tptp.p24 tptp.p14 tptp.q24 tptp.q23) (or tptp.p25 tptp.p15 tptp.q25 tptp.q24) (or tptp.p26 tptp.p16 tptp.q26 tptp.q25) (or tptp.p27 tptp.p17 tptp.q26) (or tptp.p30 tptp.p20 tptp.q30) (or tptp.p31 tptp.p21 tptp.q31 tptp.q30) (or tptp.p32 tptp.p22 tptp.q32 tptp.q31) (or tptp.p33 tptp.p23 tptp.q33 tptp.q32) (or tptp.p34 tptp.p24 tptp.q34 tptp.q33) (or tptp.p35 tptp.p25 tptp.q35 tptp.q34) (or tptp.p36 tptp.p26 tptp.q36 tptp.q35) (or tptp.p37 tptp.p27 tptp.q36) (or tptp.p40 tptp.p30 tptp.q40) (or tptp.p41 tptp.p31 tptp.q41 tptp.q40) (or tptp.p42 tptp.p32 tptp.q42 tptp.q41) (or tptp.p43 tptp.p33 tptp.q43 tptp.q42) (or tptp.p44 tptp.p34 tptp.q44 tptp.q43) (or tptp.p45 tptp.p35 tptp.q45 tptp.q44) (or tptp.p46 tptp.p36 tptp.q46 tptp.q45) (or tptp.p47 tptp.p37 tptp.q46) (or tptp.p50 tptp.p40 tptp.q50) (or tptp.p51 tptp.p41 tptp.q51 tptp.q50) (or tptp.p52 tptp.p42 tptp.q52 tptp.q51) (or tptp.p53 tptp.p43 tptp.q53 tptp.q52) (or tptp.p54 tptp.p44 tptp.q54 tptp.q53) (or tptp.p55 tptp.p45 tptp.q55 tptp.q54) (or tptp.p56 tptp.p46 tptp.q56 tptp.q55) (or tptp.p57 tptp.p47 tptp.q56) (or tptp.p60 tptp.p50 tptp.q60) (or tptp.p61 tptp.p51 tptp.q61 tptp.q60) (or tptp.p62 tptp.p52 tptp.q62 @t1) (or tptp.p63 tptp.p53 tptp.q63 tptp.q62) (or tptp.p64 tptp.p54 tptp.q64 tptp.q63) (or tptp.p65 tptp.p55 tptp.q65 tptp.q64) (or tptp.p66 tptp.p56 tptp.q66 tptp.q65) (or tptp.p57 tptp.q66) (or tptp.p60 tptp.q70) (or tptp.p61 tptp.q71 tptp.q70) (or tptp.p62 tptp.q72 tptp.q71) (or tptp.p63 tptp.q73 tptp.q72) (or tptp.p64 tptp.q74 tptp.q73) (or tptp.p65 tptp.q75 tptp.q74) (or tptp.p66 tptp.q75))) % 0.23/0.43 (define @t194 () (not (=> @t193 false))) % 0.23/0.43 (define @t195 () (not @t159)) % 0.23/0.43 (define @t196 () (not @t153)) % 0.23/0.43 (define @t197 () (not @t147)) % 0.23/0.43 (define @t198 () (not @t139)) % 0.23/0.43 (define @t199 () (not @t133)) % 0.23/0.43 (define @t200 () (not @t127)) % 0.23/0.43 (define @t201 () (not @t124)) % 0.23/0.43 (define @t202 () (not @t104)) % 0.23/0.43 (define @t203 () (not @t78)) % 0.23/0.43 (define @t204 () (not @t32)) % 0.23/0.43 (define @t205 () (not @t5)) % 0.23/0.43 (define @t206 () (not @t58)) % 0.23/0.43 (define @t207 () (not @t35)) % 0.23/0.43 (define @t208 () (not @t9)) % 0.23/0.43 (define @t209 () (@list false false true false true true)) % 0.23/0.43 (define @t210 () (not @t61)) % 0.23/0.43 (define @t211 () (not @t38)) % 0.23/0.43 (define @t212 () (not @t13)) % 0.23/0.43 (define @t213 () (not @t17)) % 0.23/0.43 (define @t214 () (not @t20)) % 0.23/0.43 (define @t215 () (not @t44)) % 0.23/0.43 (define @t216 () (not @t24)) % 0.23/0.43 (define @t217 () (not @t47)) % 0.23/0.43 (define @t218 () (not @t67)) % 0.23/0.43 (define @t219 () (not @t93)) % 0.23/0.43 (define @t220 () (not @t107)) % 0.23/0.43 (define @t221 () (not @t87)) % 0.23/0.43 (define @t222 () (not @t81)) % 0.23/0.43 (define @t223 () (not @t64)) % 0.23/0.43 (define @t224 () (not @t84)) % 0.23/0.43 (define @t225 () (not @t55)) % 0.23/0.43 (define @t226 () (not @t70)) % 0.23/0.43 (define @t227 () (not @t90)) % 0.23/0.43 (define @t228 () (@list true true true false)) % 0.23/0.43 (define @t229 () (@list tptp.p44 tptp.q44 @t61 @t169)) % 0.23/0.43 (define @t230 () (not @t113)) % 0.23/0.43 (define @t231 () (not @t110)) % 0.23/0.43 (define @t232 () (not @t116)) % 0.23/0.43 (define @t233 () (not @t130)) % 0.23/0.43 (define @t234 () (not @t101)) % 0.23/0.43 (define @t235 () (@list true true false false true false true true)) % 0.23/0.43 (define @t236 () (@list tptp.q36 tptp.p37 @t98 @t185 tptp.p26 tptp.p27 @t101 tptp.q26)) % 0.23/0.43 (define @t237 () (@list true)) % 0.23/0.43 (define @t238 () (@list tptp.p41)) % 0.23/0.43 (define @t239 () (@list true true false false false true false false)) % 0.23/0.43 (define @t240 () (@list true true true false false false true true true false)) % 0.23/0.43 (define @t241 () (@list tptp.q44 tptp.q43 tptp.p44 @t84 @t182 tptp.p34 tptp.p33 tptp.q33 @t87 @t172)) % 0.23/0.43 (define @t242 () (@list true true true true false false true false true true)) % 0.23/0.43 (define @t243 () (@list tptp.p34 tptp.q34 tptp.q36 tptp.p37 @t98 @t185 tptp.p26 tptp.p27 @t101 tptp.q26)) % 0.23/0.43 (define @t244 () (not @t136)) % 0.23/0.43 (define @t245 () (@list tptp.p24 tptp.q24 @t107 @t173)) % 0.23/0.43 (define @t246 () (@list tptp.p35 tptp.q35 @t81 @t171)) % 0.23/0.43 (define @t247 () (@list true true true false false true false true true false)) % 0.23/0.43 (define @t248 () (@list tptp.q42 tptp.q41 tptp.p42 @t90 @t183 tptp.p31 tptp.p32 @t93 tptp.q31 tptp.q30)) % 0.23/0.43 (define @t249 () (@list true true false false false true true true false false false true true true false)) % 0.23/0.43 (define @t250 () (@list tptp.q36 tptp.p37 @t98 @t185 tptp.p27 tptp.q26 tptp.q25 tptp.p26 @t124 @t190 tptp.p16 tptp.p15 tptp.q15 @t127 @t175)) % 0.23/0.43 (define @t251 () (@list tptp.p22 tptp.q22 @t113 @t174)) % 0.23/0.43 (define @t252 () (not @t150)) % 0.23/0.43 (define @t253 () (@list tptp.q35 tptp.q34 tptp.p35 @t104 @t186 tptp.p25 tptp.p24 tptp.q24 @t107 @t173)) % 0.23/0.43 (define @t254 () (@list tptp.q24 tptp.q23 tptp.p24 @t130 @t191 tptp.p14 tptp.p13 tptp.q13 @t133 @t176)) % 0.23/0.43 (define @t255 () (not @t156)) % 0.23/0.43 (define @t256 () (@list true true true false false true false true true)) % 0.23/0.43 (define @t257 () (@list tptp.q22 tptp.q21 tptp.p22 @t136 @t192 tptp.p11 tptp.p12 @t139 tptp.q11)) % 0.23/0.43 (define @t258 () (@list tptp.p15 tptp.q15 @t127 @t175)) % 0.23/0.43 (define @t259 () (@list tptp.q33 tptp.q32 tptp.p33 @t110 @t187 tptp.p23 tptp.p22 tptp.q22 @t113 @t174)) % 0.23/0.43 (define @t260 () (@list tptp.p33 tptp.q33 @t87 @t172)) % 0.23/0.43 (define @t261 () (@list false)) % 0.23/0.43 (define @t262 () (@list tptp.p01)) % 0.23/0.43 (define @t263 () (not @t161)) % 0.23/0.43 (define @t264 () (@list @t161)) % 0.23/0.43 (define @t265 () (@list tptp.p10)) % 0.23/0.43 (define @t266 () (@list true true true true true true false)) % 0.23/0.43 (define @t267 () (@list tptp.p11 tptp.p20 tptp.q20 tptp.p13 tptp.q13 @t133 @t176)) % 0.23/0.43 (define @t268 () (@list true true)) % 0.23/0.43 (define @t269 () (@list tptp.p03)) % 0.23/0.43 (define @t270 () (@list tptp.p05)) % 0.23/0.43 (assume @p1 @t194) % 0.23/0.43 (assume @p2 true) % 0.23/0.43 (step @p3 :rule bool-double-not-elim :args (@t193)) % 0.23/0.43 (step @p4 :rule bool-impl-false1 :args (@t193)) % 0.23/0.43 (step @p5 :rule cong :premises (@p4) :args (@t194)) % 0.23/0.43 (step @p6 :rule trans :premises (@p5 @p3)) % 0.23/0.43 (step @p7 :rule eq_resolve :premises (@p1 @p6)) % 0.23/0.43 (step @p8 :rule and_elim :premises (@p7) :args (54)) % 0.23/0.43 (step @p9 :rule reordering :premises (@p8) :args ((or @t155 @t158))) % 0.23/0.43 (step @p10 :rule cnf_and_pos :args (@t159 1)) % 0.23/0.43 (step @p11 :rule reordering :premises (@p10) :args ((or @t158 @t195))) % 0.23/0.43 (step @p12 :rule and_elim :premises (@p7) :args (109)) % 0.23/0.43 (step @p13 :rule and_elim :premises (@p7) :args (56)) % 0.23/0.43 (step @p14 :rule cnf_and_pos :args (@t153 1)) % 0.23/0.43 (step @p15 :rule reordering :premises (@p14) :args ((or @t152 @t196))) % 0.23/0.43 (step @p16 :rule cnf_and_pos :args (@t177 1)) % 0.23/0.43 (step @p17 :rule reordering :premises (@p16) :args ((or @t149 (not @t177)))) % 0.23/0.43 (step @p18 :rule and_elim :premises (@p7) :args (111)) % 0.23/0.43 (step @p19 :rule and_elim :premises (@p7) :args (59)) % 0.23/0.43 (step @p20 :rule cnf_and_pos :args (@t147 1)) % 0.23/0.43 (step @p21 :rule reordering :premises (@p20) :args ((or @t146 @t197))) % 0.23/0.43 (step @p22 :rule and_elim :premises (@p7) :args (168)) % 0.23/0.43 (step @p23 :rule and_elim :premises (@p7) :args (113)) % 0.23/0.43 (step @p24 :rule and_elim :premises (@p7) :args (6)) % 0.23/0.43 (step @p25 :rule reordering :premises (@p24) :args ((or @t122 @t145))) % 0.23/0.43 (step @p26 :rule and_elim :premises (@p7) :args (114)) % 0.23/0.43 (step @p27 :rule cnf_and_pos :args (@t144 1)) % 0.23/0.43 (step @p28 :rule reordering :premises (@p27) :args ((or @t120 (not @t144)))) % 0.23/0.43 (step @p29 :rule and_elim :premises (@p7) :args (60)) % 0.23/0.43 (step @p30 :rule reordering :premises (@p29) :args ((or @t135 @t138))) % 0.23/0.43 (step @p31 :rule cnf_and_pos :args (@t139 1)) % 0.23/0.43 (step @p32 :rule reordering :premises (@p31) :args ((or @t138 @t198))) % 0.23/0.43 (step @p33 :rule and_elim :premises (@p7) :args (116)) % 0.23/0.43 (step @p34 :rule and_elim :premises (@p7) :args (62)) % 0.23/0.43 (step @p35 :rule cnf_and_pos :args (@t133 1)) % 0.23/0.43 (step @p36 :rule reordering :premises (@p35) :args ((or @t132 @t199))) % 0.23/0.43 (step @p37 :rule cnf_and_pos :args (@t176 1)) % 0.23/0.43 (step @p38 :rule reordering :premises (@p37) :args ((or @t129 (not @t176)))) % 0.23/0.43 (step @p39 :rule and_elim :premises (@p7) :args (118)) % 0.23/0.43 (step @p40 :rule and_elim :premises (@p7) :args (64)) % 0.23/0.43 (step @p41 :rule cnf_and_pos :args (@t127 1)) % 0.23/0.43 (step @p42 :rule reordering :premises (@p41) :args ((or @t126 @t200))) % 0.23/0.43 (step @p43 :rule cnf_and_pos :args (@t175 1)) % 0.23/0.43 (step @p44 :rule reordering :premises (@p43) :args ((or @t123 (not @t175)))) % 0.23/0.43 (step @p45 :rule and_elim :premises (@p7) :args (120)) % 0.23/0.43 (step @p46 :rule and_elim :premises (@p7) :args (175)) % 0.23/0.43 (step @p47 :rule reordering :premises (@p46) :args ((or tptp.p16 tptp.q16 tptp.q15 tptp.p06))) % 0.23/0.43 (step @p48 :rule and_elim :premises (@p7) :args (13)) % 0.23/0.43 (step @p49 :rule and_elim :premises (@p7) :args (121)) % 0.23/0.43 (step @p50 :rule cnf_and_pos :args (@t190 1)) % 0.23/0.43 (step @p51 :rule reordering :premises (@p50) :args ((or @t102 (not @t190)))) % 0.23/0.43 (step @p52 :rule cnf_and_pos :args (@t124 2)) % 0.23/0.43 (step @p53 :rule reordering :premises (@p52) :args ((or @t100 @t201))) % 0.23/0.43 (step @p54 :rule cnf_and_pos :args (@t124 3)) % 0.23/0.43 (step @p55 :rule reordering :premises (@p54) :args ((or @t97 @t201))) % 0.23/0.43 (step @p56 :rule and_elim :premises (@p7) :args (184)) % 0.23/0.43 (step @p57 :rule reordering :premises (@p56) :args ((or tptp.p27 tptp.q26 tptp.p17))) % 0.23/0.43 (step @p58 :rule and_elim :premises (@p7) :args (22)) % 0.23/0.43 (step @p59 :rule and_elim :premises (@p7) :args (130)) % 0.23/0.43 (step @p60 :rule cnf_and_pos :args (@t185 1)) % 0.23/0.43 (step @p61 :rule reordering :premises (@p60) :args ((or @t76 (not @t185)))) % 0.23/0.43 (step @p62 :rule cnf_and_pos :args (@t98 1)) % 0.23/0.43 (step @p63 :rule reordering :premises (@p62) :args ((or @t74 (not @t98)))) % 0.23/0.43 (step @p64 :rule and_elim :premises (@p7) :args (20)) % 0.23/0.43 (step @p65 :rule and_elim :premises (@p7) :args (128)) % 0.23/0.43 (step @p66 :rule cnf_and_pos :args (@t186 1)) % 0.23/0.43 (step @p67 :rule reordering :premises (@p66) :args ((or @t82 (not @t186)))) % 0.23/0.43 (step @p68 :rule cnf_and_pos :args (@t104 3)) % 0.23/0.43 (step @p69 :rule reordering :premises (@p68) :args ((or @t77 @t202))) % 0.23/0.43 (step @p70 :rule and_elim :premises (@p7) :args (191)) % 0.23/0.43 (step @p71 :rule reordering :premises (@p70) :args ((or tptp.p36 tptp.q36 tptp.q35 tptp.p26))) % 0.23/0.43 (step @p72 :rule and_elim :premises (@p7) :args (29)) % 0.23/0.43 (step @p73 :rule and_elim :premises (@p7) :args (137)) % 0.23/0.43 (step @p74 :rule cnf_and_pos :args (@t181 1)) % 0.23/0.43 (step @p75 :rule reordering :premises (@p74) :args ((or @t56 (not @t181)))) % 0.23/0.43 (step @p76 :rule cnf_and_pos :args (@t78 2)) % 0.23/0.43 (step @p77 :rule reordering :premises (@p76) :args ((or @t54 @t203))) % 0.23/0.43 (step @p78 :rule cnf_and_pos :args (@t78 3)) % 0.23/0.43 (step @p79 :rule reordering :premises (@p78) :args ((or @t51 @t203))) % 0.23/0.43 (step @p80 :rule and_elim :premises (@p7) :args (200)) % 0.23/0.43 (step @p81 :rule reordering :premises (@p80) :args ((or tptp.p47 tptp.q46 tptp.p37))) % 0.23/0.43 (step @p82 :rule and_elim :premises (@p7) :args (46)) % 0.23/0.43 (step @p83 :rule and_elim :premises (@p7) :args (146)) % 0.23/0.43 (step @p84 :rule and_elim :premises (@p7) :args (216)) % 0.23/0.43 (step @p85 :rule reordering :premises (@p84) :args ((or tptp.q66 tptp.p57))) % 0.23/0.43 (step @p86 :rule cnf_and_pos :args (@t52 1)) % 0.23/0.43 (step @p87 :rule reordering :premises (@p86) :args ((or @t28 (not @t52)))) % 0.23/0.43 (step @p88 :rule cnf_and_pos :args (@t32 3)) % 0.23/0.43 (step @p89 :rule reordering :premises (@p88) :args ((or @t4 @t204))) % 0.23/0.43 (step @p90 :rule cnf_and_pos :args (@t5 0)) % 0.23/0.43 (step @p91 :rule reordering :premises (@p90) :args ((or @t4 @t205))) % 0.23/0.43 (step @p92 :rule and_elim :premises (@p7) :args (153)) % 0.23/0.43 (step @p93 :rule and_elim :premises (@p7) :args (161)) % 0.23/0.43 (step @p94 :rule and_elim :premises (@p7) :args (207)) % 0.23/0.43 (step @p95 :rule reordering :premises (@p94) :args ((or tptp.p56 tptp.q56 tptp.q55 tptp.p46))) % 0.23/0.43 (step @p96 :rule and_elim :premises (@p7) :args (223)) % 0.23/0.43 (step @p97 :rule reordering :premises (@p96) :args ((or tptp.q75 tptp.p66))) % 0.23/0.43 (step @p98 :rule cnf_and_pos :args (@t167 1)) % 0.23/0.43 (step @p99 :rule reordering :premises (@p98) :args ((or @t31 (not @t167)))) % 0.23/0.43 (step @p100 :rule cnf_and_pos :args (@t58 3)) % 0.23/0.43 (step @p101 :rule reordering :premises (@p100) :args ((or @t31 @t206))) % 0.23/0.43 (step @p102 :rule cnf_and_pos :args (@t35 0)) % 0.23/0.43 (step @p103 :rule reordering :premises (@p102) :args ((or @t31 @t207))) % 0.23/0.43 (step @p104 :rule and_elim :premises (@p7) :args (107)) % 0.23/0.43 (step @p105 :rule and_elim :premises (@p7) :args (92)) % 0.23/0.43 (step @p106 :rule and_elim :premises (@p7) :args (144)) % 0.23/0.43 (step @p107 :rule and_elim :premises (@p7) :args (152)) % 0.23/0.43 (step @p108 :rule and_elim :premises (@p7) :args (198)) % 0.23/0.43 (step @p109 :rule reordering :premises (@p108) :args ((or tptp.p45 tptp.q45 tptp.q44 tptp.p35))) % 0.23/0.43 (step @p110 :rule and_elim :premises (@p7) :args (101)) % 0.23/0.43 (step @p111 :rule reordering :premises (@p110) :args ((or @t3 @t4))) % 0.23/0.43 (step @p112 :rule and_elim :premises (@p7) :args (214)) % 0.23/0.43 (step @p113 :rule reordering :premises (@p112) :args ((or tptp.p65 tptp.q65 tptp.q64 tptp.p55))) % 0.23/0.43 (step @p114 :rule and_elim :premises (@p7) :args (160)) % 0.23/0.43 (step @p115 :rule cnf_and_pos :args (@t9 3)) % 0.23/0.43 (step @p116 :rule reordering :premises (@p115) :args ((or @t2 @t208))) % 0.23/0.43 (step @p117 :rule chain_m_resolution :premises (@p116 @p97 @p114 @p93 @p113 @p91 @p111) :args ((or tptp.q64 tptp.p55 @t4) @t209 (@list tptp.q75 @t9 tptp.p66 tptp.p65 @t5 tptp.q65))) % 0.23/0.43 (step @p118 :rule cnf_and_pos :args (@t61 0)) % 0.23/0.43 (step @p119 :rule reordering :premises (@p118) :args ((or @t57 @t210))) % 0.23/0.43 (step @p120 :rule cnf_and_pos :args (@t164 1)) % 0.23/0.43 (step @p121 :rule reordering :premises (@p120) :args ((or @t8 (not @t164)))) % 0.23/0.43 (step @p122 :rule cnf_and_pos :args (@t38 3)) % 0.23/0.43 (step @p123 :rule reordering :premises (@p122) :args ((or @t8 @t211))) % 0.23/0.43 (step @p124 :rule cnf_and_pos :args (@t13 0)) % 0.23/0.43 (step @p125 :rule reordering :premises (@p124) :args ((or @t8 @t212))) % 0.23/0.43 (step @p126 :rule and_elim :premises (@p7) :args (143)) % 0.23/0.43 (step @p127 :rule and_elim :premises (@p7) :args (98)) % 0.23/0.43 (step @p128 :rule and_elim :premises (@p7) :args (151)) % 0.23/0.43 (step @p129 :rule and_elim :premises (@p7) :args (159)) % 0.23/0.43 (step @p130 :rule and_elim :premises (@p7) :args (205)) % 0.23/0.43 (step @p131 :rule reordering :premises (@p130) :args ((or tptp.p54 tptp.q54 tptp.q53 tptp.p44))) % 0.23/0.43 (step @p132 :rule and_elim :premises (@p7) :args (221)) % 0.23/0.43 (step @p133 :rule reordering :premises (@p132) :args ((or tptp.q74 tptp.q73 tptp.p64))) % 0.23/0.43 (step @p134 :rule cnf_and_pos :args (@t41 0)) % 0.23/0.43 (step @p135 :rule reordering :premises (@p134) :args ((or @t37 (not @t41)))) % 0.23/0.43 (step @p136 :rule cnf_and_pos :args (@t163 1)) % 0.23/0.43 (step @p137 :rule reordering :premises (@p136) :args ((or @t11 (not @t163)))) % 0.23/0.43 (step @p138 :rule cnf_and_pos :args (@t17 3)) % 0.23/0.43 (step @p139 :rule reordering :premises (@p138) :args ((or @t11 @t213))) % 0.23/0.43 (step @p140 :rule and_elim :premises (@p7) :args (150)) % 0.23/0.43 (step @p141 :rule and_elim :premises (@p7) :args (104)) % 0.23/0.43 (step @p142 :rule and_elim :premises (@p7) :args (158)) % 0.23/0.43 (step @p143 :rule and_elim :premises (@p7) :args (212)) % 0.23/0.43 (step @p144 :rule reordering :premises (@p143) :args ((or tptp.p63 tptp.q63 tptp.q62 tptp.p53))) % 0.23/0.43 (step @p145 :rule cnf_and_pos :args (@t20 0)) % 0.23/0.43 (step @p146 :rule reordering :premises (@p145) :args ((or @t16 @t214))) % 0.23/0.43 (step @p147 :rule and_elim :premises (@p7) :args (157)) % 0.23/0.43 (step @p148 :rule and_elim :premises (@p7) :args (219)) % 0.23/0.43 (step @p149 :rule reordering :premises (@p148) :args ((or tptp.q72 tptp.q71 tptp.p62))) % 0.23/0.43 (step @p150 :rule and_elim :premises (@p7) :args (102)) % 0.23/0.43 (step @p151 :rule reordering :premises (@p150) :args ((or @t19 @t22))) % 0.23/0.43 (step @p152 :rule and_elim :premises (@p7) :args (96)) % 0.23/0.43 (step @p153 :rule cnf_and_pos :args (@t44 2)) % 0.23/0.43 (step @p154 :rule reordering :premises (@p153) :args ((or @t1 @t215))) % 0.23/0.43 (step @p155 :rule cnf_and_pos :args (@t20 1)) % 0.23/0.43 (step @p156 :rule reordering :premises (@p155) :args ((or @t1 @t214))) % 0.23/0.43 (step @p157 :rule cnf_and_pos :args (@t166 1)) % 0.23/0.43 (step @p158 :rule reordering :premises (@p157) :args ((or @t16 (not @t166)))) % 0.23/0.43 (step @p159 :rule and_elim :premises (@p7) :args (149)) % 0.23/0.43 (step @p160 :rule and_elim :premises (@p7) :args (211)) % 0.23/0.43 (step @p161 :rule reordering :premises (@p160) :args ((or tptp.p62 tptp.q62 tptp.p52 @t1))) % 0.23/0.43 (step @p162 :rule chain_m_resolution :premises (@p161 @p147 @p159 @p158 @p156 @p154 @p152) :args (@t1 (@list true true true true true false) (@list tptp.p62 tptp.p52 tptp.q62 @t20 @t44 @t166))) % 0.23/0.43 (step @p163 :rule cnf_and_pos :args (@t24 3)) % 0.23/0.43 (step @p164 :rule reordering :premises (@p163) :args ((or @t19 @t216))) % 0.23/0.43 (step @p165 :rule and_elim :premises (@p7) :args (217)) % 0.23/0.43 (step @p166 :rule reordering :premises (@p165) :args ((or tptp.q70 tptp.p60))) % 0.23/0.43 (step @p167 :rule and_elim :premises (@p7) :args (156)) % 0.23/0.43 (step @p168 :rule and_elim :premises (@p7) :args (155)) % 0.23/0.43 (step @p169 :rule and_elim :premises (@p7) :args (210)) % 0.23/0.43 (step @p170 :rule reordering :premises (@p169) :args ((or tptp.p61 tptp.q61 tptp.q60 tptp.p51))) % 0.23/0.43 (step @p171 :rule cnf_and_pos :args (@t26 0)) % 0.23/0.43 (step @p172 :rule reordering :premises (@p171) :args ((or @t23 (not @t26)))) % 0.23/0.43 (step @p173 :rule chain_m_resolution :premises (@p172 @p170 @p168 @p167 @p166 @p164 @p151) :args ((or tptp.q61 tptp.p51 @t19) @t209 (@list tptp.q60 @t26 tptp.p61 tptp.p60 @t24 tptp.q70))) % 0.23/0.43 (step @p174 :rule cnf_and_pos :args (@t180 1)) % 0.23/0.43 (step @p175 :rule reordering :premises (@p174) :args ((or @t48 (not @t180)))) % 0.23/0.43 (step @p176 :rule and_elim :premises (@p7) :args (148)) % 0.23/0.43 (step @p177 :rule and_elim :premises (@p7) :args (47)) % 0.23/0.43 (step @p178 :rule and_elim :premises (@p7) :args (32)) % 0.23/0.43 (step @p179 :rule cnf_and_pos :args (@t47 0)) % 0.23/0.43 (step @p180 :rule reordering :premises (@p179) :args ((or @t43 @t217))) % 0.23/0.43 (step @p181 :rule cnf_and_pos :args (@t47 1)) % 0.23/0.43 (step @p182 :rule reordering :premises (@p181) :args ((or @t46 @t217))) % 0.23/0.43 (step @p183 :rule cnf_and_pos :args (@t168 1)) % 0.23/0.43 (step @p184 :rule reordering :premises (@p183) :args ((or @t37 (not @t168)))) % 0.23/0.43 (step @p185 :rule and_elim :premises (@p7) :args (90)) % 0.23/0.43 (step @p186 :rule and_elim :premises (@p7) :args (203)) % 0.23/0.43 (step @p187 :rule reordering :premises (@p186) :args ((or tptp.p52 tptp.q52 tptp.q51 tptp.p42))) % 0.23/0.43 (step @p188 :rule cnf_and_pos :args (@t44 3)) % 0.23/0.43 (step @p189 :rule reordering :premises (@p188) :args ((or @t16 @t215))) % 0.23/0.43 (step @p190 :rule chain_m_resolution :premises (@p189 @p159 @p144 @p187 @p140 @p185 @p135 @p184) :args ((or tptp.p63 tptp.q63 tptp.q51 tptp.p42 @t37) (@list false false false true true true true) (@list @t44 tptp.q62 tptp.p52 tptp.p53 tptp.q52 @t41 @t168))) % 0.23/0.43 (step @p191 :rule and_elim :premises (@p7) :args (201)) % 0.23/0.43 (step @p192 :rule reordering :premises (@p191) :args ((or tptp.p50 tptp.q50 tptp.p40))) % 0.23/0.43 (step @p193 :rule and_elim :premises (@p7) :args (141)) % 0.23/0.43 (step @p194 :rule cnf_and_pos :args (@t184 1)) % 0.23/0.43 (step @p195 :rule reordering :premises (@p194) :args ((or @t73 (not @t184)))) % 0.23/0.43 (step @p196 :rule and_elim :premises (@p7) :args (139)) % 0.23/0.43 (step @p197 :rule cnf_and_pos :args (@t67 1)) % 0.23/0.43 (step @p198 :rule reordering :premises (@p197) :args ((or @t66 @t218))) % 0.23/0.43 (step @p199 :rule and_elim :premises (@p7) :args (23)) % 0.23/0.43 (step @p200 :rule cnf_and_pos :args (@t72 0)) % 0.23/0.43 (step @p201 :rule reordering :premises (@p200) :args ((or @t69 (not @t72)))) % 0.23/0.43 (step @p202 :rule and_elim :premises (@p7) :args (194)) % 0.23/0.43 (step @p203 :rule reordering :premises (@p202) :args ((or tptp.p41 tptp.q41 tptp.q40 tptp.p31))) % 0.23/0.43 (step @p204 :rule and_elim :premises (@p7) :args (185)) % 0.23/0.43 (step @p205 :rule reordering :premises (@p204) :args ((or tptp.p30 tptp.q30 tptp.p20))) % 0.23/0.43 (step @p206 :rule and_elim :premises (@p7) :args (132)) % 0.23/0.43 (step @p207 :rule cnf_and_pos :args (@t93 1)) % 0.23/0.43 (step @p208 :rule reordering :premises (@p207) :args ((or @t92 @t219))) % 0.23/0.43 (step @p209 :rule chain_m_resolution :premises (@p208 @p206 @p205 @p203 @p201 @p199 @p198 @p196 @p195 @p193 @p192 @p190 @p182 @p180 @p178 @p177 @p176 @p175 @p166 @p173 @p162 @p151 @p149 @p147 @p146 @p144 @p142 @p141 @p140 @p139 @p137 @p135 @p133 @p131 @p129 @p128 @p127 @p126 @p125 @p123 @p121 @p119 @p117 @p109 @p107 @p106 @p105 @p104 @p103 @p101 @p99 @p97 @p95 @p93 @p92 @p91 @p89 @p87 @p85 @p83 @p82 @p81 @p79 @p77 @p75 @p73 @p72 @p71 @p69 @p67 @p65 @p64) :args ((or tptp.p37 tptp.q36 tptp.p26 tptp.p20 @t105) (@list false false false true true true false true false false false true true true true false true false false true true false true true false true true true true true true false false true true true true true true true true false false true true true true true true true false false true true true true true false false true false true true true false false false true true false false) (@list @t93 tptp.q30 tptp.p31 tptp.q40 tptp.p30 tptp.q41 @t72 @t184 @t67 tptp.p40 tptp.p42 tptp.q50 tptp.q51 tptp.p41 tptp.p50 @t47 @t180 tptp.p60 tptp.p51 tptp.q61 tptp.q70 tptp.q71 tptp.p62 @t20 tptp.q62 tptp.p63 tptp.q72 tptp.p53 @t17 @t163 @t41 tptp.q73 tptp.q53 tptp.p64 tptp.p54 tptp.q63 tptp.p44 @t13 @t38 @t164 @t61 tptp.q64 tptp.q44 tptp.p55 tptp.p45 tptp.q54 tptp.q74 @t35 @t58 @t167 tptp.q75 tptp.q55 tptp.p66 tptp.p56 @t5 @t32 tptp.q56 tptp.q66 @t52 tptp.p57 tptp.p47 tptp.q46 tptp.q45 tptp.p46 @t78 @t181 tptp.p36 tptp.q35 tptp.p35 @t104 @t186))) % 0.23/0.43 (step @p210 :rule and_elim :premises (@p7) :args (182)) % 0.23/0.43 (step @p211 :rule reordering :premises (@p210) :args ((or tptp.p25 tptp.q25 tptp.q24 tptp.p15))) % 0.23/0.43 (step @p212 :rule cnf_and_pos :args (@t173 1)) % 0.23/0.43 (step @p213 :rule reordering :premises (@p212) :args ((or @t103 (not @t173)))) % 0.23/0.43 (step @p214 :rule cnf_and_pos :args (@t107 0)) % 0.23/0.43 (step @p215 :rule reordering :premises (@p214) :args ((or @t103 @t220))) % 0.23/0.43 (step @p216 :rule and_elim :premises (@p7) :args (70)) % 0.23/0.43 (step @p217 :rule and_elim :premises (@p7) :args (127)) % 0.23/0.43 (step @p218 :rule and_elim :premises (@p7) :args (74)) % 0.23/0.43 (step @p219 :rule reordering :premises (@p218) :args ((or @t89 @t92))) % 0.23/0.43 (step @p220 :rule and_elim :premises (@p7) :args (76)) % 0.23/0.43 (step @p221 :rule cnf_and_pos :args (@t87 1)) % 0.23/0.43 (step @p222 :rule reordering :premises (@p221) :args ((or @t86 @t221))) % 0.23/0.43 (step @p223 :rule cnf_and_pos :args (@t172 1)) % 0.23/0.43 (step @p224 :rule reordering :premises (@p223) :args ((or @t83 (not @t172)))) % 0.23/0.43 (step @p225 :rule and_elim :premises (@p7) :args (134)) % 0.23/0.43 (step @p226 :rule and_elim :premises (@p7) :args (78)) % 0.23/0.43 (step @p227 :rule cnf_and_pos :args (@t81 1)) % 0.23/0.43 (step @p228 :rule reordering :premises (@p227) :args ((or @t80 @t222))) % 0.23/0.43 (step @p229 :rule cnf_and_pos :args (@t171 1)) % 0.23/0.43 (step @p230 :rule reordering :premises (@p229) :args ((or @t77 (not @t171)))) % 0.23/0.43 (step @p231 :rule and_elim :premises (@p7) :args (136)) % 0.23/0.43 (step @p232 :rule cnf_and_pos :args (@t169 1)) % 0.23/0.43 (step @p233 :rule reordering :premises (@p232) :args ((or @t57 (not @t169)))) % 0.23/0.43 (step @p234 :rule and_elim :premises (@p7) :args (84)) % 0.23/0.43 (step @p235 :rule cnf_and_pos :args (@t64 3)) % 0.23/0.43 (step @p236 :rule reordering :premises (@p235) :args ((or @t37 @t223))) % 0.23/0.43 (step @p237 :rule and_elim :premises (@p7) :args (142)) % 0.23/0.43 (step @p238 :rule and_elim :premises (@p7) :args (196)) % 0.23/0.43 (step @p239 :rule reordering :premises (@p238) :args ((or tptp.p43 tptp.q43 tptp.q42 tptp.p33))) % 0.23/0.43 (step @p240 :rule cnf_and_pos :args (@t67 0)) % 0.23/0.43 (step @p241 :rule reordering :premises (@p240) :args ((or @t63 @t218))) % 0.23/0.43 (step @p242 :rule chain_m_resolution :premises (@p172 @p170 @p168 @p167 @p166 @p176 @p164 @p151 @p180 @p149 @p187 @p147 @p159 @p152 @p193 @p146 @p189 @p158 @p241 @p144 @p239 @p142 @p141 @p140 @p237 @p185 @p139 @p137 @p135 @p236 @p184 @p133 @p131 @p129 @p128 @p127 @p126 @p234 @p125 @p123 @p121 @p119 @p233 @p113 @p109 @p114 @p107 @p106 @p105 @p116 @p104 @p103 @p101 @p99 @p97 @p95 @p93 @p92 @p91 @p89 @p111 @p87 @p85 @p83 @p82 @p81 @p79 @p77 @p75 @p73 @p72 @p71 @p231 @p230 @p228 @p226) :args ((or tptp.p37 tptp.p33 tptp.q36 tptp.p26 @t80) (@list false false true false true true true true false false true true true true true true true true false false true true true true true true true true true true false false true true true true true true true true true true false false true true true true true true true true true false false true true true true true true false false true false true true true false false false true true true false) (@list tptp.q60 @t26 tptp.p61 tptp.p60 tptp.p51 @t24 tptp.q70 @t47 tptp.q71 tptp.q51 tptp.p62 tptp.p52 tptp.q61 tptp.p42 @t20 @t44 @t166 @t67 tptp.q62 tptp.q42 tptp.p63 tptp.q72 tptp.p53 tptp.p43 tptp.q52 @t17 @t163 @t41 @t64 @t168 tptp.q73 tptp.q53 tptp.p64 tptp.p54 tptp.q63 tptp.p44 tptp.q43 @t13 @t38 @t164 @t61 @t169 tptp.q64 tptp.q44 tptp.p65 tptp.p55 tptp.p45 tptp.q54 @t9 tptp.q74 @t35 @t58 @t167 tptp.q75 tptp.q55 tptp.p66 tptp.p56 @t5 @t32 tptp.q65 tptp.q56 tptp.q66 @t52 tptp.p57 tptp.p47 tptp.q46 tptp.q45 tptp.p46 @t78 @t181 tptp.p36 tptp.p35 tptp.q35 @t81 @t171))) % 0.23/0.43 (step @p243 :rule and_elim :premises (@p7) :args (189)) % 0.23/0.43 (step @p244 :rule reordering :premises (@p243) :args ((or tptp.p34 tptp.q34 tptp.q33 tptp.p24))) % 0.23/0.43 (step @p245 :rule and_elim :premises (@p7) :args (27)) % 0.23/0.43 (step @p246 :rule and_elim :premises (@p7) :args (135)) % 0.23/0.43 (step @p247 :rule cnf_and_pos :args (@t182 1)) % 0.23/0.43 (step @p248 :rule reordering :premises (@p247) :args ((or @t62 (not @t182)))) % 0.23/0.43 (step @p249 :rule cnf_and_pos :args (@t84 2)) % 0.23/0.43 (step @p250 :rule reordering :premises (@p249) :args ((or @t60 @t224))) % 0.23/0.43 (step @p251 :rule cnf_and_pos :args (@t84 3)) % 0.23/0.43 (step @p252 :rule reordering :premises (@p251) :args ((or @t57 @t224))) % 0.23/0.43 (step @p253 :rule and_elim :premises (@p7) :args (87)) % 0.23/0.43 (step @p254 :rule cnf_and_pos :args (@t55 1)) % 0.23/0.43 (step @p255 :rule reordering :premises (@p254) :args ((or @t54 @t225))) % 0.23/0.43 (step @p256 :rule and_elim :premises (@p7) :args (145)) % 0.23/0.43 (step @p257 :rule chain_m_resolution :premises (@p123 @p128 @p117 @p131 @p107 @p105 @p103 @p99 @p95 @p92 @p89 @p87 @p85 @p83 @p82 @p256 @p81 @p255 @p253) :args ((or tptp.q53 tptp.p44 tptp.p37 @t54) (@list false false false true true true true false true true true false false true true false true true) (@list @t38 tptp.q64 tptp.p54 tptp.p55 tptp.q54 @t35 @t167 tptp.q55 tptp.p56 @t32 tptp.q56 tptp.q66 @t52 tptp.p57 tptp.p46 tptp.p47 @t55 tptp.q46))) % 0.23/0.43 (step @p258 :rule and_elim :premises (@p7) :args (36)) % 0.23/0.43 (step @p259 :rule cnf_and_pos :args (@t178 1)) % 0.23/0.43 (step @p260 :rule reordering :premises (@p259) :args ((or @t36 (not @t178)))) % 0.23/0.43 (step @p261 :rule cnf_and_pos :args (@t58 2)) % 0.23/0.43 (step @p262 :rule reordering :premises (@p261) :args ((or @t34 @t206))) % 0.23/0.43 (step @p263 :rule and_elim :premises (@p7) :args (154)) % 0.23/0.43 (step @p264 :rule cnf_and_pos :args (@t29 0)) % 0.23/0.43 (step @p265 :rule reordering :premises (@p264) :args ((or @t28 (not @t29)))) % 0.23/0.43 (step @p266 :rule and_elim :premises (@p7) :args (53)) % 0.23/0.43 (step @p267 :rule cnf_and_pos :args (@t32 2)) % 0.23/0.43 (step @p268 :rule reordering :premises (@p267) :args ((or @t3 @t204))) % 0.23/0.43 (step @p269 :rule chain_m_resolution :premises (@p114 @p113 @p116 @p268 @p97 @p92 @p266 @p95 @p265 @p263 @p85 @p117) :args ((or tptp.q64 tptp.p55 tptp.q55 tptp.p46) (@list false true true false false true false true false false true) (@list tptp.p65 @t9 tptp.q65 tptp.q75 @t32 tptp.p66 tptp.p56 tptp.q56 @t29 tptp.p57 tptp.q66))) % 0.23/0.43 (step @p270 :rule cnf_and_pos :args (@t55 0)) % 0.23/0.43 (step @p271 :rule reordering :premises (@p270) :args ((or @t51 @t225))) % 0.23/0.43 (step @p272 :rule chain_m_resolution :premises (@p81 @p271 @p82 @p256 @p85 @p269 @p117 @p123 @p128 @p131 @p101 @p262 @p260 @p106 @p258 @p109 @p257) :args ((or tptp.q53 tptp.p44 tptp.p37 tptp.q44 tptp.p35) (@list true true false false false true true false false true true true false false false true) (@list tptp.q46 tptp.p47 @t55 tptp.p57 tptp.p46 tptp.q66 tptp.q64 @t38 tptp.p54 tptp.q55 tptp.q54 tptp.p55 @t58 @t178 tptp.p45 tptp.q45))) % 0.23/0.43 (step @p273 :rule cnf_and_pos :args (@t170 1)) % 0.23/0.43 (step @p274 :rule reordering :premises (@p273) :args ((or @t63 (not @t170)))) % 0.23/0.43 (step @p275 :rule and_elim :premises (@p7) :args (82)) % 0.23/0.43 (step @p276 :rule and_elim :premises (@p7) :args (193)) % 0.23/0.43 (step @p277 :rule reordering :premises (@p276) :args ((or tptp.p40 tptp.q40 tptp.p30))) % 0.23/0.43 (step @p278 :rule and_elim :premises (@p7) :args (88)) % 0.23/0.43 (step @p279 :rule reordering :premises (@p278) :args ((or @t43 @t46))) % 0.23/0.43 (step @p280 :rule chain_m_resolution :premises (@p177 @p166 @p192 @p151 @p279 @p149 @p187 @p147 @p159 @p146 @p189 @p144 @p142 @p141 @p140 @p185 @p139 @p137 @p135 @p184 @p133 @p131 @p129 @p128 @p127 @p125 @p123 @p121 @p113 @p114 @p107 @p105 @p116 @p104 @p103 @p99 @p97 @p95 @p93 @p92 @p91 @p89 @p111 @p87 @p85 @p83 @p82 @p256 @p81 @p255 @p253) :args ((or tptp.p44 tptp.p42 tptp.p40 tptp.p37 @t54) (@list false false true true false false true true true true false true true true true true true true true false false true true true true true true false true true true true true true true false false true true true true true true false false true true false true true) (@list tptp.p60 tptp.p50 tptp.q70 tptp.q50 tptp.q71 tptp.q51 tptp.p62 tptp.p52 @t20 @t44 tptp.q62 tptp.p63 tptp.q72 tptp.p53 tptp.q52 @t17 @t163 @t41 @t168 tptp.q73 tptp.q53 tptp.p64 tptp.p54 tptp.q63 @t13 @t38 @t164 tptp.q64 tptp.p65 tptp.p55 tptp.q54 @t9 tptp.q74 @t35 @t167 tptp.q75 tptp.q55 tptp.p66 tptp.p56 @t5 @t32 tptp.q65 tptp.q56 tptp.q66 @t52 tptp.p57 tptp.p46 tptp.p47 @t55 tptp.q46))) % 0.23/0.43 (step @p281 :rule and_elim :premises (@p7) :args (49)) % 0.23/0.43 (step @p282 :rule cnf_and_pos :args (@t17 2)) % 0.23/0.43 (step @p283 :rule reordering :premises (@p282) :args ((or @t15 @t213))) % 0.23/0.43 (step @p284 :rule chain_m_resolution :premises (@p172 @p170 @p168 @p167 @p166 @p164 @p151 @p149 @p283 @p142 @p144 @p189 @p154 @p159 @p281 @p176 @p187 @p182 @p279) :args ((or tptp.q63 tptp.p53 tptp.q52 tptp.p42 @t46) (@list false false true false true true false true false false true true false true true false true true) (@list tptp.q60 @t26 tptp.p61 tptp.p60 @t24 tptp.q70 tptp.q71 tptp.q72 @t17 tptp.p63 tptp.q62 tptp.q61 @t44 tptp.p62 tptp.p51 tptp.p52 @t47 tptp.q51))) % 0.23/0.43 (step @p285 :rule and_elim :premises (@p7) :args (147)) % 0.23/0.43 (step @p286 :rule cnf_and_pos :args (@t49 1)) % 0.23/0.43 (step @p287 :rule reordering :premises (@p286) :args ((or @t23 (not @t49)))) % 0.23/0.43 (step @p288 :rule cnf_and_pos :args (@t24 2)) % 0.23/0.43 (step @p289 :rule reordering :premises (@p288) :args ((or @t22 @t216))) % 0.23/0.43 (step @p290 :rule and_elim :premises (@p7) :args (202)) % 0.23/0.43 (step @p291 :rule reordering :premises (@p290) :args ((or tptp.p51 tptp.q51 tptp.q50 tptp.p41))) % 0.23/0.43 (step @p292 :rule cnf_and_pos :args (@t44 1)) % 0.23/0.43 (step @p293 :rule reordering :premises (@p292) :args ((or @t43 @t215))) % 0.23/0.43 (step @p294 :rule chain_m_resolution :premises (@p161 @p147 @p158 @p159 @p156 @p152 @p293 @p170 @p291) :args ((or tptp.p61 tptp.q60 tptp.p51 tptp.q50 tptp.p41) (@list true true true true false true false false) (@list tptp.p62 tptp.q62 tptp.p52 @t20 @t166 @t44 tptp.q61 tptp.q51))) % 0.23/0.43 (step @p295 :rule chain_m_resolution :premises (@p142 @p144 @p283 @p189 @p149 @p159 @p281 @p187 @p180 @p176 @p294 @p167 @p289 @p151 @p287 @p166 @p285 @p177 @p192 @p284 @p140 @p185 @p135 @p184 @p131 @p128 @p127 @p123 @p121) :args ((or tptp.q54 tptp.p44 tptp.p42 tptp.p41 tptp.p40 @t8) (@list false true true false false true false true false false true true true true false false true false true true true true true false true true true true) (@list tptp.p63 @t17 tptp.q62 tptp.q72 @t44 tptp.p62 tptp.p52 tptp.q51 @t47 tptp.p51 tptp.p61 @t24 tptp.q71 tptp.q60 tptp.q70 @t49 tptp.p60 tptp.p50 tptp.q50 tptp.p53 tptp.q52 @t41 @t168 tptp.q53 tptp.p54 tptp.q63 @t38 @t164))) % 0.23/0.43 (step @p296 :rule chain_m_resolution :premises (@p81 @p271 @p82 @p256 @p85 @p269 @p117 @p295 @p101 @p262 @p260 @p106 @p258 @p109 @p280) :args ((or tptp.p44 tptp.p42 tptp.p41 tptp.p40 tptp.p37 tptp.q44 tptp.p35) (@list true true false false false true true true true true false false false true) (@list tptp.q46 tptp.p47 @t55 tptp.p57 tptp.p46 tptp.q66 tptp.q64 tptp.q55 tptp.q54 tptp.p55 @t58 @t178 tptp.p45 tptp.q45))) % 0.23/0.43 (step @p297 :rule cnf_and_pos :args (@t70 1)) % 0.23/0.43 (step @p298 :rule reordering :premises (@p297) :args ((or @t69 @t226))) % 0.23/0.43 (step @p299 :rule and_elim :premises (@p7) :args (140)) % 0.23/0.43 (step @p300 :rule chain_m_resolution :premises (@p299 @p298 @p296 @p277) :args ((or tptp.p44 tptp.p42 tptp.p40 tptp.p37 tptp.q44 tptp.p35 tptp.p30) (@list true false false) (@list @t70 tptp.p41 tptp.q40))) % 0.23/0.43 (step @p301 :rule cnf_and_pos :args (@t70 3)) % 0.23/0.43 (step @p302 :rule reordering :premises (@p301) :args ((or @t43 @t226))) % 0.23/0.43 (step @p303 :rule chain_m_resolution :premises (@p139 @p142 @p133 @p144 @p129 @p127 @p125 @p121 @p117 @p107 @p104 @p103 @p97 @p95 @p93 @p92 @p91 @p89 @p87 @p85 @p83 @p82 @p256 @p81 @p255 @p253) :args ((or tptp.q62 tptp.p53 tptp.p37 @t54) (@list false false false true true true true false true true true false false true true true true true false false true true false true true) (@list @t17 tptp.q73 tptp.p63 tptp.p64 tptp.q63 @t13 @t164 tptp.q64 tptp.p55 tptp.q74 @t35 tptp.q75 tptp.q55 tptp.p66 tptp.p56 @t5 @t32 tptp.q56 tptp.q66 @t52 tptp.p57 tptp.p46 tptp.p47 @t55 tptp.q46))) % 0.23/0.43 (step @p304 :rule chain_m_resolution :premises (@p81 @p271 @p82 @p256 @p85 @p269 @p117 @p121 @p127 @p144 @p142 @p283 @p149 @p173 @p101 @p260 @p106 @p258 @p109 @p303 @p189 @p154 @p159 @p281 @p187 @p302 @p175 @p299 @p178 @p203 @p201 @p196 @p300 @p193 @p275 @p241 @p274 @p239 @p140 @p237 @p185 @p135 @p236 @p184 @p272) :args ((or tptp.p44 tptp.p37 tptp.q44 tptp.p35 tptp.q43 tptp.p33 tptp.p31 tptp.p30) (@list true true false false false true true false false true true false true true true false false false true true true false true false true true false false false true false false true true true true false true true true true true true false) (@list tptp.q46 tptp.p47 @t55 tptp.p57 tptp.p46 tptp.q66 tptp.q64 @t164 tptp.q63 tptp.p63 @t17 tptp.q72 tptp.q71 tptp.q55 tptp.p55 @t58 @t178 tptp.p45 tptp.q45 tptp.q62 tptp.q61 @t44 tptp.p62 tptp.p52 tptp.q51 tptp.p51 @t70 @t180 tptp.p41 tptp.q40 @t72 tptp.p40 tptp.p42 tptp.q41 @t67 @t170 tptp.q42 tptp.p53 tptp.p43 tptp.q52 @t41 @t64 @t168 tptp.q53))) % 0.23/0.43 (step @p305 :rule cnf_and_pos :args (@t81 0)) % 0.23/0.43 (step @p306 :rule reordering :premises (@p305) :args ((or @t77 @t222))) % 0.23/0.43 (step @p307 :rule chain_m_resolution :premises (@p176 @p173 @p180 @p149 @p187 @p147 @p159 @p152 @p193 @p146 @p189 @p158 @p241 @p144 @p239 @p142 @p141 @p140 @p237 @p185 @p139 @p137 @p135 @p236 @p184 @p133 @p131 @p129 @p128 @p127 @p125 @p123 @p121 @p117 @p107 @p105 @p104 @p103 @p99 @p97 @p95 @p93 @p92 @p91 @p89 @p87 @p85 @p83 @p82 @p81 @p79 @p75 @p73 @p72 @p71 @p306 @p231 @p304 @p252 @p250 @p248 @p246 @p245 @p244 @p242 @p225 @p224 @p222 @p220) :args ((or tptp.p37 tptp.p31 tptp.p30 tptp.q36 tptp.p26 tptp.p24 @t86) (@list false true false false true true true true true true true true false false true true true true true true true true true true false false true true true true true true false true true true true true false false true true true true true false false true false true true false false false true false false true true true false false false true true true true false) (@list tptp.p51 @t47 tptp.q71 tptp.q51 tptp.p62 tptp.p52 tptp.q61 tptp.p42 @t20 @t44 @t166 @t67 tptp.q62 tptp.q42 tptp.p63 tptp.q72 tptp.p53 tptp.p43 tptp.q52 @t17 @t163 @t41 @t64 @t168 tptp.q73 tptp.q53 tptp.p64 tptp.p54 tptp.q63 @t13 @t38 @t164 tptp.q64 tptp.p55 tptp.q54 tptp.q74 @t35 @t167 tptp.q75 tptp.q55 tptp.p66 tptp.p56 @t5 @t32 tptp.q56 tptp.q66 @t52 tptp.p57 tptp.p47 tptp.q46 tptp.p46 @t78 @t181 tptp.p36 tptp.q35 @t81 tptp.p35 tptp.q44 tptp.q43 tptp.p44 @t84 @t182 tptp.p34 tptp.q34 tptp.p33 tptp.q33 @t87 @t172))) % 0.23/0.43 (step @p308 :rule and_elim :premises (@p7) :args (187)) % 0.23/0.43 (step @p309 :rule reordering :premises (@p308) :args ((or tptp.p32 tptp.q32 tptp.q31 tptp.p22))) % 0.23/0.43 (step @p310 :rule and_elim :premises (@p7) :args (25)) % 0.23/0.43 (step @p311 :rule and_elim :premises (@p7) :args (133)) % 0.23/0.43 (step @p312 :rule cnf_and_pos :args (@t183 1)) % 0.23/0.43 (step @p313 :rule reordering :premises (@p312) :args ((or @t68 (not @t183)))) % 0.23/0.43 (step @p314 :rule cnf_and_pos :args (@t90 2)) % 0.23/0.43 (step @p315 :rule reordering :premises (@p314) :args ((or @t66 @t227))) % 0.23/0.43 (step @p316 :rule cnf_and_pos :args (@t90 3)) % 0.23/0.43 (step @p317 :rule reordering :premises (@p316) :args ((or @t63 @t227))) % 0.23/0.43 (step @p318 :rule cnf_and_pos :args (@t61 1)) % 0.23/0.43 (step @p319 :rule reordering :premises (@p318) :args ((or @t60 @t210))) % 0.23/0.43 (step @p320 :rule chain_m_resolution :premises (@p300 @p126 @p233 @p319 @p234) :args ((or tptp.p42 tptp.p40 tptp.p37 tptp.p35 tptp.p30 @t60) @t228 @t229)) % 0.23/0.43 (step @p321 :rule and_elim :premises (@p7) :args (34)) % 0.23/0.43 (step @p322 :rule cnf_and_pos :args (@t179 1)) % 0.23/0.43 (step @p323 :rule reordering :premises (@p322) :args ((or @t42 (not @t179)))) % 0.23/0.43 (step @p324 :rule cnf_and_pos :args (@t64 2)) % 0.23/0.43 (step @p325 :rule reordering :premises (@p324) :args ((or @t40 @t223))) % 0.23/0.43 (step @p326 :rule chain_m_resolution :premises (@p142 @p144 @p283 @p189 @p149 @p159 @p281 @p187 @p180 @p176 @p294 @p167 @p289 @p151 @p287 @p166 @p285 @p177 @p192 @p284) :args ((or tptp.q63 tptp.p53 tptp.q52 tptp.p42 tptp.p41 tptp.p40) (@list false true true false false true false true false false true true true true false false true false true) (@list tptp.p63 @t17 tptp.q62 tptp.q72 @t44 tptp.p62 tptp.p52 tptp.q51 @t47 tptp.p51 tptp.p61 @t24 tptp.q71 tptp.q60 tptp.q70 @t49 tptp.p60 tptp.p50 tptp.q50))) % 0.23/0.43 (step @p327 :rule cnf_and_pos :args (@t165 1)) % 0.23/0.43 (step @p328 :rule reordering :premises (@p327) :args ((or @t12 (not @t165)))) % 0.23/0.43 (step @p329 :rule and_elim :premises (@p7) :args (97)) % 0.23/0.43 (step @p330 :rule cnf_and_pos :args (@t38 2)) % 0.23/0.43 (step @p331 :rule reordering :premises (@p330) :args ((or @t12 @t211))) % 0.23/0.43 (step @p332 :rule cnf_and_pos :args (@t35 1)) % 0.23/0.43 (step @p333 :rule reordering :premises (@p332) :args ((or @t34 @t207))) % 0.23/0.43 (step @p334 :rule chain_m_resolution :premises (@p269 @p107 @p99 @p333 @p105 @p131 @p128 @p121 @p331 @p127) :args ((or tptp.p46 tptp.q53 tptp.p44 @t12) (@list true true true false false true true true false) (@list tptp.p55 tptp.q55 @t35 @t167 tptp.q54 tptp.p54 tptp.q64 @t38 @t164))) % 0.23/0.43 (step @p335 :rule chain_m_resolution :premises (@p85 @p82 @p117 @p81 @p107 @p271 @p333 @p256 @p131 @p334 @p128 @p331 @p121 @p127) :args ((or tptp.q53 tptp.p44 tptp.p37 @t12) (@list true true false true true true false false false true true true false) (@list tptp.p57 tptp.q66 tptp.p47 tptp.p55 tptp.q46 @t35 @t55 tptp.q54 tptp.p46 tptp.p54 @t38 tptp.q64 @t164))) % 0.23/0.43 (step @p336 :rule chain_m_resolution :premises (@p81 @p271 @p82 @p256 @p85 @p269 @p117 @p101 @p260 @p106 @p258 @p109 @p119 @p126 @p335 @p303 @p121 @p329 @p127 @p328 @p326 @p236 @p325 @p323 @p237 @p321 @p239 @p320 @p299 @p298 @p277) :args ((or tptp.p42 tptp.p40 tptp.p37 tptp.p35 tptp.q42 tptp.p33 tptp.p30) (@list true true false false false true true true false false false true false false true true true false true false true true true false false false true true true false) (@list tptp.q46 tptp.p47 @t55 tptp.p57 tptp.p46 tptp.q66 tptp.q55 tptp.p55 @t58 @t178 tptp.p45 tptp.q44 @t61 tptp.p44 tptp.q45 tptp.q64 tptp.q62 @t164 @t165 tptp.q63 tptp.q53 tptp.q52 tptp.p53 @t64 @t179 tptp.p43 tptp.q43 tptp.p41 @t70 tptp.q40))) % 0.23/0.43 (step @p337 :rule chain_m_resolution :premises (@p81 @p271 @p82 @p256 @p85 @p269 @p117 @p121 @p127 @p144 @p101 @p260 @p142 @p106 @p258 @p283 @p109 @p149 @p303 @p173 @p189 @p154 @p159 @p281 @p187 @p140 @p185 @p135 @p184 @p272 @p126 @p233 @p319 @p234) :args ((or tptp.p51 tptp.q51 tptp.p42 tptp.p37 tptp.p35 @t60) (@list true true false false false true true false false true true true false false true false false true true true true false true false true true true true false true true true false) (@list tptp.q46 tptp.p47 @t55 tptp.p57 tptp.p46 tptp.q66 tptp.q64 @t164 tptp.q63 tptp.q55 tptp.p55 tptp.p63 @t58 @t178 @t17 tptp.p45 tptp.q72 tptp.q45 tptp.q71 tptp.q62 tptp.q61 @t44 tptp.p62 tptp.p52 tptp.p53 tptp.q52 @t41 @t168 tptp.q53 tptp.p44 tptp.q44 @t61 @t169))) % 0.23/0.43 (step @p338 :rule cnf_and_pos :args (@t13 1)) % 0.23/0.43 (step @p339 :rule reordering :premises (@p338) :args ((or @t12 @t212))) % 0.23/0.43 (step @p340 :rule cnf_and_pos :args (@t9 2)) % 0.23/0.43 (step @p341 :rule reordering :premises (@p340) :args ((or @t7 @t208))) % 0.23/0.43 (step @p342 :rule cnf_and_pos :args (@t5 1)) % 0.23/0.43 (step @p343 :rule reordering :premises (@p342) :args ((or @t3 @t205))) % 0.23/0.43 (step @p344 :rule chain_m_resolution :premises (@p113 @p343 @p260 @p93 @p258 @p114 @p97 @p109 @p341 @p104 @p119 @p133 @p126 @p129 @p121 @p335 @p339 @p127 @p144 @p142 @p137 @p283 @p141 @p149 @p303 @p173 @p189 @p154 @p159 @p281 @p187 @p236 @p325 @p323 @p237 @p321 @p239 @p337 @p302 @p175 @p299 @p178 @p203 @p201 @p196 @p336) :args ((or tptp.p42 tptp.p37 tptp.p35 tptp.q42 tptp.p33 tptp.q41 tptp.p31 tptp.p30) (@list true true false false true false false true true true false false true true false true false false true true true false false true true true true false true false true true true false false false true true true false false false true false false) (@list tptp.q65 tptp.p55 @t5 @t178 tptp.p65 tptp.p66 tptp.p45 @t9 tptp.q75 tptp.q44 tptp.q74 @t61 tptp.p64 tptp.q64 tptp.p44 @t13 @t164 tptp.q63 tptp.p63 tptp.q73 @t17 @t163 tptp.q72 tptp.q45 tptp.q71 tptp.q62 tptp.q61 @t44 tptp.p62 tptp.p52 tptp.q53 tptp.q52 tptp.p53 @t64 @t179 tptp.p43 tptp.q43 tptp.q51 tptp.p51 @t70 @t180 tptp.p41 tptp.q40 @t72 tptp.p40))) % 0.23/0.43 (step @p345 :rule chain_m_resolution :premises (@p326 @p325 @p323 @p237 @p321 @p239 @p319 @p126 @p295 @p299 @p298 @p277 @p127 @p121) :args ((or tptp.q54 tptp.p42 tptp.p40 tptp.q42 tptp.p33 tptp.p30 @t8) (@list true true false false false true false false true true false true true) (@list tptp.q52 tptp.p53 @t64 @t179 tptp.p43 tptp.q43 @t61 tptp.p44 tptp.p41 @t70 tptp.q40 tptp.q63 @t164))) % 0.23/0.43 (step @p346 :rule chain_m_resolution :premises (@p159 @p189 @p187 @p144 @p325 @p323 @p237 @p321 @p239 @p319 @p126 @p131 @p190 @p302 @p299 @p203 @p201 @p196 @p345 @p142 @p139 @p133 @p129 @p128 @p127 @p125 @p123 @p121 @p117 @p107 @p105 @p104 @p103 @p99 @p97 @p95 @p93 @p92 @p91 @p89 @p87 @p85 @p83 @p82 @p81 @p79 @p75 @p73 @p72 @p71 @p306 @p231 @p344) :args ((or tptp.p42 tptp.p37 tptp.q42 tptp.p33 tptp.q41 tptp.p31 tptp.p30 tptp.q36 tptp.p26) (@list true false false true true false false false true false false true true false false true false false true true false true true true true true true false true true true true true false false true true true true true false false true false true true false false false true false false) (@list @t44 tptp.p52 tptp.q62 tptp.q52 tptp.p53 @t64 @t179 tptp.p43 tptp.q43 @t61 tptp.p44 tptp.q53 tptp.q51 @t70 tptp.p41 tptp.q40 @t72 tptp.p40 tptp.p63 @t17 tptp.q73 tptp.p64 tptp.p54 tptp.q63 @t13 @t38 @t164 tptp.q64 tptp.p55 tptp.q54 tptp.q74 @t35 @t167 tptp.q75 tptp.q55 tptp.p66 tptp.p56 @t5 @t32 tptp.q56 tptp.q66 @t52 tptp.p57 tptp.p47 tptp.q46 tptp.p46 @t78 @t181 tptp.p36 tptp.q35 @t81 tptp.p35))) % 0.23/0.43 (step @p347 :rule cnf_and_pos :args (@t87 0)) % 0.23/0.43 (step @p348 :rule reordering :premises (@p347) :args ((or @t83 @t221))) % 0.23/0.43 (step @p349 :rule chain_m_resolution :premises (@p149 @p173 @p176 @p147 @p152 @p180 @p146 @p158 @p190 @p144 @p142 @p141 @p140 @p139 @p137 @p135 @p133 @p131 @p129 @p128 @p127 @p126 @p125 @p123 @p121 @p119 @p117 @p109 @p107 @p106 @p105 @p104 @p103 @p101 @p99 @p97 @p95 @p93 @p92 @p91 @p89 @p87 @p85 @p83 @p82 @p81 @p79 @p77 @p75 @p73 @p72 @p71 @p231 @p230 @p228 @p226) :args ((or tptp.p42 tptp.p37 tptp.q36 tptp.p26 @t80) (@list true true true true true true true false false true true true true true true false false true true true true true true true true false false true true true true true true true false false true true true true true false false true false true true true false false false true true true false) (@list tptp.q71 tptp.p51 tptp.p62 tptp.q61 @t47 @t20 @t166 tptp.q51 tptp.q62 tptp.p63 tptp.q72 tptp.p53 @t17 @t163 @t41 tptp.q73 tptp.q53 tptp.p64 tptp.p54 tptp.q63 tptp.p44 @t13 @t38 @t164 @t61 tptp.q64 tptp.q44 tptp.p55 tptp.p45 tptp.q54 tptp.q74 @t35 @t58 @t167 tptp.q75 tptp.q55 tptp.p66 tptp.p56 @t5 @t32 tptp.q56 tptp.q66 @t52 tptp.p57 tptp.p47 tptp.q46 tptp.q45 tptp.p46 @t78 @t181 tptp.p36 tptp.p35 tptp.q35 @t81 @t171))) % 0.23/0.43 (step @p350 :rule chain_m_resolution :premises (@p81 @p82 @p271 @p85 @p256 @p117 @p269 @p121 @p127 @p190 @p101 @p260 @p142 @p106 @p258 @p283 @p109 @p149 @p303 @p173 @p189 @p154 @p159 @p281 @p187 @p302 @p175 @p299 @p178 @p203 @p201 @p140 @p185 @p196 @p135 @p184 @p300 @p272) :args ((or tptp.p44 tptp.p42 tptp.p37 tptp.q44 tptp.p35 tptp.q41 tptp.p31 tptp.p30) (@list true true false false true false true false false true true true false false true false false true true true true false true false true true false false false true true true false true true false false) (@list tptp.p47 tptp.q46 tptp.p57 @t55 tptp.q66 tptp.p46 tptp.q64 @t164 tptp.q63 tptp.q55 tptp.p55 tptp.p63 @t58 @t178 @t17 tptp.p45 tptp.q72 tptp.q45 tptp.q71 tptp.q62 tptp.q61 @t44 tptp.p62 tptp.p52 tptp.q51 tptp.p51 @t70 @t180 tptp.p41 tptp.q40 tptp.p53 tptp.q52 @t72 @t41 @t168 tptp.p40 tptp.q53))) % 0.23/0.43 (step @p351 :rule chain_m_resolution :premises (@p149 @p173 @p147 @p152 @p176 @p146 @p158 @p180 @p144 @p190 @p142 @p141 @p140 @p139 @p137 @p135 @p133 @p131 @p129 @p128 @p127 @p125 @p123 @p121 @p117 @p107 @p105 @p104 @p103 @p99 @p97 @p95 @p93 @p92 @p91 @p89 @p87 @p85 @p83 @p82 @p81 @p79 @p75 @p73 @p72 @p71 @p306 @p231 @p350 @p252 @p248 @p246 @p245 @p244 @p349 @p348 @p225 @p346 @p317 @p315 @p313 @p311 @p310 @p309 @p307 @p206 @p208 @p219 @p205) :args ((or tptp.p37 tptp.p30 tptp.q36 tptp.p26 tptp.p24 tptp.p22 tptp.p20) (@list true true true true true true true false false true true true true true true false false true true true true true true false true true true true true false false true true true true true false false true false true true false false false true false false true true false false false true true false false true true true false false false true true true true false) (@list tptp.q71 tptp.p62 tptp.q61 tptp.p51 @t20 @t166 @t47 tptp.q62 tptp.q51 tptp.p63 tptp.q72 tptp.p53 @t17 @t163 @t41 tptp.q73 tptp.q53 tptp.p64 tptp.p54 tptp.q63 @t13 @t38 @t164 tptp.q64 tptp.p55 tptp.q54 tptp.q74 @t35 @t167 tptp.q75 tptp.q55 tptp.p66 tptp.p56 @t5 @t32 tptp.q56 tptp.q66 @t52 tptp.p57 tptp.p47 tptp.q46 tptp.p46 @t78 @t181 tptp.p36 tptp.q35 @t81 tptp.p35 tptp.q44 tptp.p44 @t84 @t182 tptp.p34 tptp.q34 tptp.q33 @t87 tptp.p33 tptp.q42 tptp.q41 tptp.p42 @t90 @t183 tptp.p32 tptp.q32 tptp.p31 @t93 tptp.q31 tptp.q30))) % 0.23/0.43 (step @p352 :rule and_elim :premises (@p7) :args (131)) % 0.23/0.43 (step @p353 :rule cnf_and_pos :args (@t95 1)) % 0.23/0.43 (step @p354 :rule reordering :premises (@p353) :args ((or @t69 (not @t95)))) % 0.23/0.43 (step @p355 :rule cnf_and_pos :args (@t70 2)) % 0.23/0.43 (step @p356 :rule reordering :premises (@p355) :args ((or @t46 @t226))) % 0.23/0.43 (step @p357 :rule chain_m_resolution :premises (@p167 @p170 @p162 @p289 @p287 @p166 @p285 @p177 @p192 @p356 @p175 @p299 @p178) :args ((or tptp.p40 @t71) (@list false true true true false false true false true true false false) (@list tptp.p61 tptp.q61 @t24 tptp.q60 tptp.q70 @t49 tptp.p60 tptp.p50 tptp.q50 tptp.p51 @t70 @t180))) % 0.23/0.43 (step @p358 :rule chain_m_resolution :premises (@p296 @p126 @p233 @p319 @p234) :args ((or tptp.p42 tptp.p41 tptp.p40 tptp.p37 tptp.p35 @t60) @t228 @t229)) % 0.23/0.43 (step @p359 :rule chain_m_resolution :premises (@p81 @p271 @p82 @p256 @p85 @p269 @p117 @p101 @p260 @p106 @p258 @p109 @p119 @p303 @p126 @p121 @p329 @p335 @p127 @p328 @p326 @p236 @p325 @p323 @p237 @p321 @p239 @p358 @p193 @p274 @p198 @p275 @p203) :args ((or tptp.p41 tptp.p40 tptp.p37 tptp.p35 tptp.p33 tptp.q40 tptp.p31) (@list true true false false false true true true false false false true true false true true false false true false true true true false false false true true true true false false) (@list tptp.q46 tptp.p47 @t55 tptp.p57 tptp.p46 tptp.q66 tptp.q55 tptp.p55 @t58 @t178 tptp.p45 tptp.q44 tptp.q45 @t61 tptp.q64 tptp.q62 tptp.p44 @t164 @t165 tptp.q63 tptp.q53 tptp.q52 tptp.p53 @t64 @t179 tptp.p43 tptp.q43 tptp.p42 tptp.q42 @t67 @t170 tptp.q41))) % 0.23/0.43 (step @p360 :rule chain_m_resolution :premises (@p326 @p325 @p323 @p237 @p321 @p239 @p319 @p126 @p127 @p295 @p121 @p117 @p107 @p105 @p103 @p99 @p95 @p92 @p89 @p87 @p85 @p83 @p82 @p81 @p79 @p75 @p73 @p72 @p71 @p306 @p231 @p359 @p274 @p275 @p193 @p198 @p203 @p357) :args ((or tptp.p40 tptp.p37 tptp.p33 tptp.q40 tptp.p31 tptp.q36 tptp.p26) (@list true true false false false true false true false true false true true true true false true true true false false true false true true false false false true false false true false true true false true) (@list tptp.q52 tptp.p53 @t64 @t179 tptp.p43 tptp.q43 @t61 tptp.q63 tptp.p44 @t164 tptp.q64 tptp.p55 tptp.q54 @t35 @t167 tptp.q55 tptp.p56 @t32 tptp.q56 tptp.q66 @t52 tptp.p57 tptp.p47 tptp.q46 tptp.p46 @t78 @t181 tptp.p36 tptp.q35 @t81 tptp.p35 tptp.q42 @t170 tptp.p42 @t67 tptp.q41 tptp.p41))) % 0.23/0.43 (step @p361 :rule chain_m_resolution :premises (@p117 @p295 @p107 @p105 @p103 @p99 @p95 @p92 @p89 @p87 @p85 @p83 @p82 @p81 @p79 @p75 @p73 @p72 @p71 @p306 @p231 @p296 @p252 @p248 @p246 @p245 @p244 @p348 @p225 @p360 @p349 @p193 @p198 @p203 @p357) :args ((or tptp.p40 tptp.p37 tptp.q40 tptp.p31 tptp.q36 tptp.p26 tptp.p24) (@list true true true true true false true true true false false true false true true false false false true false false true true false false false true false false true true true false true) (@list tptp.q64 tptp.p55 tptp.q54 @t35 @t167 tptp.q55 tptp.p56 @t32 tptp.q56 tptp.q66 @t52 tptp.p57 tptp.p47 tptp.q46 tptp.p46 @t78 @t181 tptp.p36 tptp.q35 @t81 tptp.p35 tptp.q44 tptp.p44 @t84 @t182 tptp.p34 tptp.q33 @t87 tptp.p33 tptp.q34 tptp.p42 @t67 tptp.q41 tptp.p41))) % 0.23/0.43 (step @p362 :rule cnf_and_pos :args (@t93 0)) % 0.23/0.43 (step @p363 :rule reordering :premises (@p362) :args ((or @t89 @t219))) % 0.23/0.43 (step @p364 :rule chain_m_resolution :premises (@p239 @p237 @p241 @p236 @p193 @p272 @p296 @p357) :args ((or tptp.p44 tptp.p40 tptp.p37 tptp.q44 tptp.p35 tptp.q43 tptp.p33) (@list true true true false false false true) (@list tptp.p43 tptp.q42 @t64 @t67 tptp.q53 tptp.p42 tptp.p41))) % 0.23/0.43 (step @p365 :rule chain_m_resolution :premises (@p237 @p239 @p236 @p241 @p131 @p193 @p128 @p295 @p123 @p117 @p107 @p105 @p103 @p99 @p95 @p92 @p89 @p87 @p85 @p83 @p82 @p81 @p79 @p75 @p73 @p72 @p71 @p306 @p231 @p364 @p252 @p250 @p248 @p246 @p245 @p244 @p242 @p225 @p224 @p222 @p220 @p357) :args ((or tptp.p40 tptp.p37 tptp.q36 tptp.p26 tptp.p24 @t86) (@list false true true false false true false true false true true true true false true true true false false true false true true false false false true false false true true true false false false true true true true false true) (@list tptp.p43 @t64 tptp.q42 tptp.q53 @t67 tptp.p54 tptp.p42 @t38 tptp.q64 tptp.p55 tptp.q54 @t35 @t167 tptp.q55 tptp.p56 @t32 tptp.q56 tptp.q66 @t52 tptp.p57 tptp.p47 tptp.q46 tptp.p46 @t78 @t181 tptp.p36 tptp.q35 @t81 tptp.p35 tptp.q44 tptp.q43 tptp.p44 @t84 @t182 tptp.p34 tptp.q34 tptp.p33 tptp.q33 @t87 @t172 tptp.p41))) % 0.23/0.43 (step @p366 :rule chain_m_resolution :premises (@p81 @p271 @p82 @p256 @p85 @p269 @p117 @p101 @p260 @p106 @p258 @p109 @p119 @p303 @p126 @p121 @p329 @p335 @p127 @p328 @p326 @p236 @p325 @p323 @p237 @p321 @p239 @p358 @p357) :args ((or tptp.p42 tptp.p40 tptp.p37 tptp.p35 tptp.q42 tptp.p33) (@list true true false false false true true true false false false true true false true true false false true false true true true false false false true true) (@list tptp.q46 tptp.p47 @t55 tptp.p57 tptp.p46 tptp.q66 tptp.q55 tptp.p55 @t58 @t178 tptp.p45 tptp.q44 tptp.q45 @t61 tptp.q64 tptp.q62 tptp.p44 @t164 @t165 tptp.q63 tptp.q53 tptp.q52 tptp.p53 @t64 @t179 tptp.p43 tptp.q43 tptp.p41))) % 0.23/0.43 (step @p367 :rule chain_m_resolution :premises (@p326 @p325 @p323 @p237 @p321 @p239 @p319 @p126 @p127 @p295 @p121 @p117 @p107 @p105 @p103 @p99 @p95 @p92 @p89 @p87 @p85 @p83 @p82 @p81 @p79 @p75 @p73 @p72 @p71 @p306 @p231 @p366 @p357) :args ((or tptp.p42 tptp.p40 tptp.p37 tptp.q42 tptp.p33 tptp.q36 tptp.p26) (@list true true false false false true false true false true false true true true true false true true true false false true false true true false false false true false false true) (@list tptp.q52 tptp.p53 @t64 @t179 tptp.p43 tptp.q43 @t61 tptp.q63 tptp.p44 @t164 tptp.q64 tptp.p55 tptp.q54 @t35 @t167 tptp.q55 tptp.p56 @t32 tptp.q56 tptp.q66 @t52 tptp.p57 tptp.p47 tptp.q46 tptp.p46 @t78 @t181 tptp.p36 tptp.q35 @t81 tptp.p35 tptp.p41))) % 0.23/0.43 (step @p368 :rule chain_m_resolution :premises (@p117 @p295 @p107 @p105 @p103 @p99 @p95 @p92 @p89 @p87 @p85 @p83 @p82 @p81 @p79 @p75 @p73 @p72 @p71 @p306 @p231 @p296 @p252 @p248 @p246 @p245 @p244 @p348 @p225 @p367 @p349 @p317 @p313 @p311 @p310 @p309 @p365 @p363 @p206 @p361 @p357 @p354 @p195 @p352 @p199 @p351) :args ((or tptp.p37 tptp.q36 tptp.p26 tptp.p24 tptp.p22 tptp.p20) (@list true true true true true false true true true false false true false true true false false false true false false true true false false false true false false true true true false false false true true false false true true true false false false) (@list tptp.q64 tptp.p55 tptp.q54 @t35 @t167 tptp.q55 tptp.p56 @t32 tptp.q56 tptp.q66 @t52 tptp.p57 tptp.p47 tptp.q46 tptp.p46 @t78 @t181 tptp.p36 tptp.q35 @t81 tptp.p35 tptp.q44 tptp.p44 @t84 @t182 tptp.p34 tptp.q33 @t87 tptp.p33 tptp.q34 tptp.q42 tptp.p42 @t90 @t183 tptp.p32 tptp.q32 tptp.q31 @t93 tptp.p31 tptp.p41 tptp.q40 tptp.p40 @t95 @t184 tptp.p30))) % 0.23/0.43 (step @p369 :rule and_elim :premises (@p7) :args (125)) % 0.23/0.43 (step @p370 :rule cnf_and_pos :args (@t113 0)) % 0.23/0.43 (step @p371 :rule reordering :premises (@p370) :args ((or @t109 @t230))) % 0.23/0.43 (step @p372 :rule and_elim :premises (@p7) :args (180)) % 0.23/0.43 (step @p373 :rule reordering :premises (@p372) :args ((or tptp.p23 tptp.q23 tptp.q22 tptp.p13))) % 0.23/0.43 (step @p374 :rule and_elim :premises (@p7) :args (18)) % 0.23/0.43 (step @p375 :rule and_elim :premises (@p7) :args (126)) % 0.23/0.43 (step @p376 :rule cnf_and_pos :args (@t187 1)) % 0.23/0.43 (step @p377 :rule reordering :premises (@p376) :args ((or @t88 (not @t187)))) % 0.23/0.43 (step @p378 :rule cnf_and_pos :args (@t110 3)) % 0.23/0.43 (step @p379 :rule reordering :premises (@p378) :args ((or @t83 @t231))) % 0.23/0.43 (step @p380 :rule chain_m_resolution :premises (@p176 @p173 @p162 @p180 @p149 @p190 @p147 @p193 @p146 @p241 @p144 @p239 @p142 @p141 @p140 @p237 @p139 @p137 @p135 @p236 @p133 @p131 @p129 @p128 @p127 @p125 @p123 @p121 @p117 @p107 @p105 @p104 @p103 @p99 @p97 @p95 @p93 @p92 @p91 @p89 @p87 @p85 @p83 @p82 @p81 @p79 @p75 @p73 @p72) :args ((or tptp.p44 tptp.p37 tptp.q43 tptp.p33 @t79) (@list false true true false false true true true true false false true true true true true true true true false false true true true true true true false true true true true true false false true true true true true false false true false true true false false) (@list tptp.p51 tptp.q61 @t47 tptp.q71 tptp.q51 tptp.p62 tptp.p42 @t20 @t67 tptp.q62 tptp.q42 tptp.p63 tptp.q72 tptp.p53 tptp.p43 @t17 @t163 @t41 @t64 tptp.q73 tptp.q53 tptp.p64 tptp.p54 tptp.q63 @t13 @t38 @t164 tptp.q64 tptp.p55 tptp.q54 tptp.q74 @t35 @t167 tptp.q75 tptp.q55 tptp.p66 tptp.p56 @t5 @t32 tptp.q56 tptp.q66 @t52 tptp.p57 tptp.p47 tptp.q46 tptp.p46 @t78 @t181))) % 0.23/0.43 (step @p381 :rule chain_m_resolution :premises (@p206 @p208 @p304 @p205 @p199 @p195 @p364 @p231 @p306 @p71 @p380 @p252 @p250 @p248 @p246 @p245 @p244 @p242 @p379 @p377 @p375 @p374 @p373 @p371 @p369 @p368 @p217 @p216 @p215 @p213 @p211 @p209) :args ((or tptp.p37 tptp.q36 tptp.p26 tptp.p20 tptp.q25 tptp.p15 tptp.p13) (@list true false false true true false true true false true true true true false false false true true true false false false true false false true true true true false true) (@list @t93 tptp.p31 tptp.q30 tptp.p30 @t184 tptp.p40 tptp.p35 @t81 tptp.q35 tptp.p36 tptp.q44 tptp.q43 tptp.p44 @t84 @t182 tptp.p34 tptp.q34 tptp.q33 tptp.p33 @t110 @t187 tptp.p23 tptp.q22 @t113 tptp.p22 tptp.p24 tptp.q23 @t107 @t173 tptp.q24 tptp.p25))) % 0.23/0.43 (step @p382 :rule and_elim :premises (@p7) :args (15)) % 0.23/0.43 (step @p383 :rule and_elim :premises (@p7) :args (123)) % 0.23/0.43 (step @p384 :rule cnf_and_pos :args (@t189 1)) % 0.23/0.43 (step @p385 :rule reordering :premises (@p384) :args ((or @t96 (not @t189)))) % 0.23/0.43 (step @p386 :rule cnf_and_pos :args (@t118 0)) % 0.23/0.43 (step @p387 :rule reordering :premises (@p386) :args ((or @t115 (not @t118)))) % 0.23/0.43 (step @p388 :rule cnf_and_pos :args (@t107 1)) % 0.23/0.43 (step @p389 :rule reordering :premises (@p388) :args ((or @t106 @t220))) % 0.23/0.43 (step @p390 :rule cnf_and_pos :args (@t104 2)) % 0.23/0.43 (step @p391 :rule reordering :premises (@p390) :args ((or @t80 @t202))) % 0.23/0.43 (step @p392 :rule chain_m_resolution :premises (@p348 @p225 @p244 @p380 @p126 @p246 @p234 @p119 @p252 @p233 @p109 @p106 @p101 @p95 @p92 @p89 @p87 @p85 @p83 @p82 @p81 @p79 @p77 @p75 @p73 @p72 @p71 @p69 @p391 @p67 @p65 @p64 @p211 @p217 @p213 @p389 @p216) :args ((or tptp.p37 tptp.q36 tptp.p26 tptp.q25 tptp.p15 @t106) (@list false false false true true true true true true false true true false true true true false false true false true true true false false false true true true false false false true true true false) (@list @t87 tptp.q33 tptp.p33 tptp.p44 tptp.p34 tptp.q43 @t61 @t84 @t169 tptp.q44 tptp.p45 @t58 tptp.q55 tptp.p56 @t32 tptp.q56 tptp.q66 @t52 tptp.p57 tptp.p47 tptp.q46 tptp.q45 tptp.p46 @t78 @t181 tptp.p36 tptp.q35 tptp.q34 tptp.p35 @t104 @t186 tptp.p25 tptp.p24 tptp.q24 @t107 @t173))) % 0.23/0.43 (step @p393 :rule and_elim :premises (@p7) :args (68)) % 0.23/0.43 (step @p394 :rule cnf_and_pos :args (@t113 1)) % 0.23/0.43 (step @p395 :rule reordering :premises (@p394) :args ((or @t112 @t230))) % 0.23/0.43 (step @p396 :rule cnf_and_pos :args (@t174 1)) % 0.23/0.43 (step @p397 :rule reordering :premises (@p396) :args ((or @t109 (not @t174)))) % 0.23/0.43 (step @p398 :rule cnf_and_pos :args (@t110 2)) % 0.23/0.43 (step @p399 :rule reordering :premises (@p398) :args ((or @t86 @t231))) % 0.23/0.43 (step @p400 :rule chain_m_resolution :premises (@p317 @p311 @p239 @p309 @p237 @p363 @p236 @p206 @p272 @p304 @p231 @p306 @p71 @p380 @p252 @p250 @p248 @p246 @p245) :args ((or tptp.p37 tptp.p33 tptp.p30 tptp.q36 tptp.p26 tptp.q32 tptp.p22 @t85) (@list false false false true true true false false false true true false true true true true false false) (@list @t90 tptp.q42 tptp.p32 tptp.p43 tptp.q31 @t64 @t93 tptp.q53 tptp.p31 tptp.p35 @t81 tptp.q35 tptp.p36 tptp.q44 tptp.q43 tptp.p44 @t84 @t182))) % 0.23/0.43 (step @p401 :rule chain_m_resolution :premises (@p380 @p126 @p234 @p119 @p233 @p109 @p106 @p101 @p95 @p92 @p89 @p87 @p85 @p83 @p82 @p81 @p79 @p77 @p75 @p73 @p72 @p71 @p69 @p67 @p65 @p64 @p211 @p215 @p217 @p244 @p400 @p242 @p379 @p399 @p377 @p375 @p374 @p373 @p369 @p397 @p395 @p393 @p392 @p385 @p382 @p381) :args ((or tptp.p37 tptp.q36 tptp.p26 tptp.q25 tptp.p15 tptp.p13 @t112) (@list true true true true false true true false true true true false false true false true true true false false false true true false false false true false false true true true true true false false false true true true false true true false false) (@list tptp.p44 tptp.q43 @t61 @t169 tptp.q44 tptp.p45 @t58 tptp.q55 tptp.p56 @t32 tptp.q56 tptp.q66 @t52 tptp.p57 tptp.p47 tptp.q46 tptp.q45 tptp.p46 @t78 @t181 tptp.p36 tptp.q35 tptp.p35 @t104 @t186 tptp.p25 tptp.q24 @t107 tptp.p24 tptp.p34 tptp.q34 tptp.q33 tptp.q32 tptp.p33 @t110 @t187 tptp.p23 tptp.p22 tptp.q22 @t113 @t174 tptp.q23 tptp.p30 @t189 tptp.p20))) % 0.23/0.43 (step @p402 :rule and_elim :premises (@p7) :args (178)) % 0.23/0.43 (step @p403 :rule reordering :premises (@p402) :args ((or tptp.p21 tptp.q21 tptp.q20 tptp.p11))) % 0.23/0.43 (step @p404 :rule and_elim :premises (@p7) :args (16)) % 0.23/0.43 (step @p405 :rule and_elim :premises (@p7) :args (124)) % 0.23/0.43 (step @p406 :rule cnf_and_pos :args (@t188 1)) % 0.23/0.43 (step @p407 :rule reordering :premises (@p406) :args ((or @t94 (not @t188)))) % 0.23/0.43 (step @p408 :rule cnf_and_pos :args (@t116 3)) % 0.23/0.43 (step @p409 :rule reordering :premises (@p408) :args ((or @t89 @t232))) % 0.23/0.43 (step @p410 :rule chain_m_resolution :premises (@p173 @p162 @p149 @p176 @p147 @p180 @p146 @p190 @p144 @p142 @p141 @p140 @p139 @p137 @p135 @p133 @p131 @p129 @p128 @p127 @p125 @p123 @p121 @p117 @p107 @p105 @p104 @p103 @p99 @p97 @p95 @p93 @p92 @p91 @p89 @p87 @p85 @p83 @p82 @p81 @p79 @p75 @p73 @p72 @p71 @p306 @p231 @p350 @p252 @p248 @p246 @p245 @p244 @p348 @p225 @p346 @p349 @p317 @p315 @p313 @p311 @p310 @p309 @p307) :args ((or tptp.p37 tptp.p31 tptp.p30 tptp.q36 tptp.p26 tptp.p24 tptp.q31 tptp.p22) (@list true false true true true true false false true true true true true true false false true true true true true true false true true true true true false false true true true true true false false true false true true false false false true false false true true false false false true false false true true true true false false false true) (@list tptp.q61 tptp.q71 tptp.p51 tptp.p62 @t47 @t20 tptp.q51 tptp.q62 tptp.p63 tptp.q72 tptp.p53 @t17 @t163 @t41 tptp.q73 tptp.q53 tptp.p64 tptp.p54 tptp.q63 @t13 @t38 @t164 tptp.q64 tptp.p55 tptp.q54 tptp.q74 @t35 @t167 tptp.q75 tptp.q55 tptp.p66 tptp.p56 @t5 @t32 tptp.q56 tptp.q66 @t52 tptp.p57 tptp.p47 tptp.q46 tptp.p46 @t78 @t181 tptp.p36 tptp.q35 @t81 tptp.p35 tptp.q44 tptp.p44 @t84 @t182 tptp.p34 tptp.q33 @t87 tptp.p33 tptp.q34 tptp.q42 tptp.q41 tptp.p42 @t90 @t183 tptp.p32 tptp.q32))) % 0.23/0.43 (step @p411 :rule chain_m_resolution :premises (@p176 @p173 @p162 @p180 @p149 @p190 @p147 @p313 @p146 @p310 @p144 @p309 @p142 @p141 @p140 @p222 @p139 @p137 @p135 @p225 @p133 @p131 @p380 @p129 @p128 @p127 @p126 @p234 @p125 @p123 @p121 @p119 @p233 @p117 @p109 @p107 @p106 @p105 @p104 @p103 @p101 @p99 @p97 @p95 @p93 @p92 @p91 @p89 @p87 @p85 @p83 @p82 @p81 @p79 @p77 @p75 @p73 @p72 @p71 @p69 @p67 @p65 @p64 @p211 @p215 @p217 @p410) :args ((or tptp.p37 tptp.p31 tptp.p30 tptp.q36 tptp.p26 tptp.q31 tptp.p22 tptp.q25 tptp.p15) (@list false true true false false true true true false false false true true true true true true true false false false false true true true true true true true true true true false false true true true true true true true false false true true true true true false false true false true true true false false false true true false false false true false false) (@list tptp.p51 tptp.q61 @t47 tptp.q71 tptp.q51 tptp.p62 tptp.p42 @t20 @t183 tptp.q62 tptp.p32 tptp.p63 tptp.q72 tptp.p53 tptp.q32 @t17 @t163 @t41 @t87 tptp.q73 tptp.q53 tptp.p33 tptp.p64 tptp.p54 tptp.q63 tptp.p44 tptp.q43 @t13 @t38 @t164 @t61 @t169 tptp.q64 tptp.q44 tptp.p55 tptp.p45 tptp.q54 tptp.q74 @t35 @t58 @t167 tptp.q75 tptp.q55 tptp.p66 tptp.p56 @t5 @t32 tptp.q56 tptp.q66 @t52 tptp.p57 tptp.p47 tptp.q46 tptp.q45 tptp.p46 @t78 @t181 tptp.p36 tptp.q35 tptp.p35 @t104 @t186 tptp.p25 tptp.q24 @t107 tptp.p24))) % 0.23/0.43 (step @p412 :rule chain_m_resolution :premises (@p306 @p231 @p71 @p304 @p380 @p252 @p250 @p248 @p246 @p245) :args ((or tptp.p37 tptp.p33 tptp.p31 tptp.p30 tptp.q36 tptp.p26 @t85) (@list false false false true true true true false false) (@list @t81 tptp.q35 tptp.p35 tptp.p36 tptp.q44 tptp.q43 tptp.p44 @t84 @t182))) % 0.23/0.43 (step @p413 :rule chain_m_resolution :premises (@p380 @p126 @p234 @p119 @p233 @p109 @p106 @p101 @p95 @p92 @p89 @p87 @p85 @p83 @p82 @p81 @p79 @p77 @p75 @p73 @p72 @p71 @p69 @p67 @p65 @p64 @p211 @p215 @p217 @p244 @p412 @p242 @p379 @p377 @p375 @p374 @p373 @p371 @p369 @p411 @p409 @p407 @p405 @p404 @p403 @p401 @p392 @p387 @p385 @p383 @p382 @p381 @p63 @p61 @p59 @p58 @p57 @p55 @p53 @p51 @p49 @p48 @p47 @p45 @p44 @p42 @p40) :args ((or tptp.p17 tptp.p13 tptp.p11 tptp.q16 tptp.p06 @t126) (@list true true true true false true true false true true true false false true false true true true false false false true true false false false true false false true true true true false false false true false false true true false false false true true true true false false false true true false false false true true true false false false true true true false) (@list tptp.p44 tptp.q43 @t61 @t169 tptp.q44 tptp.p45 @t58 tptp.q55 tptp.p56 @t32 tptp.q56 tptp.q66 @t52 tptp.p57 tptp.p47 tptp.q46 tptp.q45 tptp.p46 @t78 @t181 tptp.p36 tptp.q35 tptp.p35 @t104 @t186 tptp.p25 tptp.q24 @t107 tptp.p24 tptp.p34 tptp.q34 tptp.q33 tptp.p33 @t110 @t187 tptp.p23 tptp.q22 @t113 tptp.p22 tptp.q31 tptp.p31 @t116 @t188 tptp.p21 tptp.q21 tptp.q23 tptp.q20 tptp.p30 @t118 @t189 tptp.p20 tptp.q36 tptp.p37 @t98 @t185 tptp.p27 tptp.q26 tptp.q25 tptp.p26 @t124 @t190 tptp.p16 tptp.p15 tptp.q15 @t127 @t175))) % 0.23/0.43 (step @p414 :rule and_elim :premises (@p7) :args (173)) % 0.23/0.43 (step @p415 :rule reordering :premises (@p414) :args ((or tptp.p14 tptp.q14 tptp.q13 tptp.p04))) % 0.23/0.43 (step @p416 :rule and_elim :premises (@p7) :args (11)) % 0.23/0.43 (step @p417 :rule and_elim :premises (@p7) :args (119)) % 0.23/0.43 (step @p418 :rule cnf_and_pos :args (@t191 1)) % 0.23/0.43 (step @p419 :rule reordering :premises (@p418) :args ((or @t108 (not @t191)))) % 0.23/0.43 (step @p420 :rule cnf_and_pos :args (@t130 2)) % 0.23/0.43 (step @p421 :rule reordering :premises (@p420) :args ((or @t106 @t233))) % 0.23/0.43 (step @p422 :rule cnf_and_pos :args (@t130 3)) % 0.23/0.43 (step @p423 :rule reordering :premises (@p422) :args ((or @t103 @t233))) % 0.23/0.43 (step @p424 :rule and_elim :premises (@p7) :args (73)) % 0.23/0.43 (step @p425 :rule cnf_and_pos :args (@t101 1)) % 0.23/0.43 (step @p426 :rule reordering :premises (@p425) :args ((or @t100 @t234))) % 0.23/0.43 (step @p427 :rule and_elim :premises (@p7) :args (129)) % 0.23/0.43 (step @p428 :rule chain_m_resolution :premises (@p368 @p63 @p61 @p59 @p58 @p427 @p57 @p426 @p424) :args ((or tptp.p24 tptp.p22 tptp.p20 tptp.p17 @t100) @t235 @t236)) % 0.23/0.43 (step @p429 :rule and_elim :premises (@p7) :args (138)) % 0.23/0.43 (step @p430 :rule cnf_and_pos :args (@t75 0)) % 0.23/0.43 (step @p431 :rule reordering :premises (@p430) :args ((or @t74 (not @t75)))) % 0.23/0.43 (step @p432 :rule chain_m_resolution :premises (@p295 @p357) :args ((or tptp.q54 tptp.p44 tptp.p42 tptp.p40 @t8) @t237 @t238)) % 0.23/0.43 (step @p433 :rule chain_m_resolution :premises (@p149 @p283 @p281 @p142 @p187 @p190 @p173 @p162 @p302 @p175 @p299 @p178 @p203 @p201 @p196 @p432 @p193 @p275 @p241 @p274 @p239 @p237 @p185 @p236 @p184 @p131 @p128 @p127 @p123 @p121 @p269 @p101 @p262 @p260 @p106 @p258 @p109 @p77 @p75 @p73 @p72 @p71 @p431 @p429 @p304 @p252 @p250 @p248 @p246 @p245 @p244 @p225 @p224 @p222 @p220) :args ((or tptp.p35 tptp.p31 tptp.p30 tptp.q35 tptp.p26 tptp.q34 tptp.p24 @t86) (@list true true false false false true true true true false false false true false false true true true true false true true true true false true true true true false true true true false false false true true false false false true false false true true true false false false true true true false) (@list tptp.q72 tptp.p62 @t17 tptp.p52 tptp.p63 tptp.q71 tptp.q61 tptp.q51 tptp.p51 @t70 @t180 tptp.p41 tptp.q40 @t72 tptp.p40 tptp.p42 tptp.q41 @t67 @t170 tptp.q42 tptp.p43 tptp.q52 @t64 @t168 tptp.q53 tptp.p54 tptp.q63 @t38 @t164 tptp.q64 tptp.q55 tptp.q54 tptp.p55 @t58 @t178 tptp.p45 tptp.q45 tptp.p46 @t78 @t181 tptp.p36 tptp.q36 @t75 tptp.p37 tptp.q44 tptp.q43 tptp.p44 @t84 @t182 tptp.p34 tptp.p33 tptp.q33 @t87 @t172))) % 0.23/0.43 (step @p434 :rule chain_m_resolution :premises (@p269 @p432 @p101 @p262 @p260 @p106 @p258 @p109 @p126 @p233 @p319 @p234) :args ((or tptp.p46 tptp.p42 tptp.p40 tptp.q45 tptp.p35 @t60) (@list true true true true false false false true true true false) (@list tptp.q64 tptp.q55 tptp.q54 tptp.p55 @t58 @t178 tptp.p45 tptp.p44 tptp.q44 @t61 @t169))) % 0.23/0.43 (step @p435 :rule chain_m_resolution :premises (@p269 @p101 @p260 @p106 @p258 @p109 @p119 @p126 @p121 @p334 @p127 @p326 @p236 @p325 @p323 @p237 @p321 @p239 @p434 @p357) :args ((or tptp.p46 tptp.p42 tptp.p40 tptp.q45 tptp.p35 tptp.q42 tptp.p33) (@list true true false false false true false true false false false true true true false false false true true) (@list tptp.q55 tptp.p55 @t58 @t178 tptp.p45 tptp.q44 @t61 tptp.q64 tptp.p44 @t164 tptp.q63 tptp.q53 tptp.q52 tptp.p53 @t64 @t179 tptp.p43 tptp.q43 tptp.p41))) % 0.23/0.43 (step @p436 :rule chain_m_resolution :premises (@p149 @p281 @p283 @p187 @p142 @p185 @p190 @p184 @p131 @p128 @p127 @p123 @p121 @p269 @p101 @p262 @p260 @p106 @p258 @p109 @p126 @p233 @p319 @p234) :args ((or tptp.q71 tptp.p46 tptp.q51 tptp.p42 tptp.q45 tptp.p35 @t60) (@list true true false false true false true false true true true true false true true true false false false true true true false) (@list tptp.p62 tptp.q72 tptp.p52 @t17 tptp.q52 tptp.p63 @t168 tptp.q53 tptp.p54 tptp.q63 @t38 @t164 tptp.q64 tptp.q55 tptp.q54 tptp.p55 @t58 @t178 tptp.p45 tptp.p44 tptp.q44 @t61 @t169))) % 0.23/0.43 (step @p437 :rule chain_m_resolution :premises (@p269 @p101 @p260 @p106 @p258 @p109 @p119 @p126 @p121 @p334 @p127 @p144 @p142 @p283 @p189 @p149 @p159 @p281 @p187 @p236 @p325 @p323 @p237 @p321 @p239 @p436 @p173 @p162 @p302 @p175 @p299 @p178 @p203 @p201 @p196 @p435 @p77 @p75 @p73 @p72 @p71 @p431 @p429 @p344) :args ((or tptp.p42 tptp.p35 tptp.q42 tptp.p33 tptp.q41 tptp.p31 tptp.p30 tptp.q35 tptp.p26) (@list true true false false false true false true false false false true true true false false true false true true true false false false true true true true true false false false true false false true true false false false true false false) (@list tptp.q55 tptp.p55 @t58 @t178 tptp.p45 tptp.q44 @t61 tptp.q64 tptp.p44 @t164 tptp.q63 tptp.p63 @t17 tptp.q62 tptp.q72 @t44 tptp.p62 tptp.p52 tptp.q53 tptp.q52 tptp.p53 @t64 @t179 tptp.p43 tptp.q43 tptp.q71 tptp.q61 tptp.q51 tptp.p51 @t70 @t180 tptp.p41 tptp.q40 @t72 tptp.p40 tptp.q45 tptp.p46 @t78 @t181 tptp.p36 tptp.q36 @t75 tptp.p37))) % 0.23/0.43 (step @p438 :rule chain_m_resolution :premises (@p149 @p283 @p281 @p142 @p187 @p190 @p173 @p162 @p302 @p175 @p299 @p178 @p185 @p203 @p184 @p201 @p131 @p196 @p128 @p127 @p432 @p123 @p121 @p269 @p101 @p262 @p260 @p106 @p258 @p109 @p77 @p75 @p73 @p72 @p71 @p431 @p429 @p350 @p252 @p248 @p246 @p245 @p244 @p348 @p225 @p437 @p317 @p315 @p313 @p311 @p310 @p309 @p433 @p206 @p208 @p219 @p205) :args ((or tptp.p35 tptp.p30 tptp.q35 tptp.p26 tptp.q34 tptp.p24 tptp.p22 tptp.p20) (@list true true false false false true true true true false false true false true true false false true true false true true false true true true false false false true true false false false true false false true true false false false true false false true true true false false false true true true true false) (@list tptp.q72 tptp.p62 @t17 tptp.p52 tptp.p63 tptp.q71 tptp.q61 tptp.q51 tptp.p51 @t70 @t180 tptp.q52 tptp.p41 @t168 tptp.q40 tptp.q53 @t72 tptp.p54 tptp.q63 tptp.p40 @t38 @t164 tptp.q64 tptp.q55 tptp.q54 tptp.p55 @t58 @t178 tptp.p45 tptp.q45 tptp.p46 @t78 @t181 tptp.p36 tptp.q36 @t75 tptp.p37 tptp.q44 tptp.p44 @t84 @t182 tptp.p34 tptp.q33 @t87 tptp.p33 tptp.q42 tptp.q41 tptp.p42 @t90 @t183 tptp.p32 tptp.q32 tptp.p31 @t93 tptp.q31 tptp.q30))) % 0.23/0.43 (step @p439 :rule chain_m_resolution :premises (@p435 @p77 @p75 @p73 @p72 @p71 @p431 @p429 @p359 @p274 @p275 @p193 @p198 @p203 @p357) :args ((or tptp.p40 tptp.p35 tptp.p33 tptp.q40 tptp.p31 tptp.q35 tptp.p26) (@list true true false false false true false false true false true true false true) (@list tptp.q45 tptp.p46 @t78 @t181 tptp.p36 tptp.q36 @t75 tptp.p37 tptp.q42 @t170 tptp.p42 @t67 tptp.q41 tptp.p41))) % 0.23/0.43 (step @p440 :rule chain_m_resolution :premises (@p269 @p432 @p101 @p262 @p260 @p106 @p258 @p109 @p77 @p75 @p73 @p72 @p71 @p431 @p429 @p296 @p252 @p248 @p246 @p245 @p244 @p348 @p225 @p439 @p193 @p198 @p203 @p357) :args ((or tptp.p40 tptp.p35 tptp.q40 tptp.p31 tptp.q35 tptp.p26 tptp.q34 tptp.p24) (@list true true true true false false false true true false false false true false false true true false false false true false false true true false true) (@list tptp.q64 tptp.q55 tptp.q54 tptp.p55 @t58 @t178 tptp.p45 tptp.q45 tptp.p46 @t78 @t181 tptp.p36 tptp.q36 @t75 tptp.p37 tptp.q44 tptp.p44 @t84 @t182 tptp.p34 tptp.q33 @t87 tptp.p33 tptp.p42 @t67 tptp.q41 tptp.p41))) % 0.23/0.43 (step @p441 :rule chain_m_resolution :premises (@p237 @p239 @p236 @p241 @p131 @p193 @p128 @p432 @p123 @p269 @p101 @p262 @p260 @p106 @p258 @p109 @p77 @p75 @p73 @p72 @p71 @p431 @p429 @p364 @p252 @p250 @p248 @p246 @p245 @p244 @p225 @p224 @p222 @p220) :args ((or tptp.p40 tptp.p35 tptp.q35 tptp.p26 tptp.q34 tptp.p24 @t86) (@list false true true false false true false true false true true true false false false true true false false false true false false true true true false false false true true true false) (@list tptp.p43 @t64 tptp.q42 tptp.q53 @t67 tptp.p54 tptp.p42 @t38 tptp.q64 tptp.q55 tptp.q54 tptp.p55 @t58 @t178 tptp.p45 tptp.q45 tptp.p46 @t78 @t181 tptp.p36 tptp.q36 @t75 tptp.p37 tptp.q44 tptp.q43 tptp.p44 @t84 @t182 tptp.p34 tptp.p33 tptp.q33 @t87 @t172))) % 0.23/0.43 (step @p442 :rule chain_m_resolution :premises (@p435 @p77 @p75 @p73 @p72 @p71 @p431 @p429 @p366) :args ((or tptp.p42 tptp.p40 tptp.p35 tptp.q42 tptp.p33 tptp.q35 tptp.p26) @t239 (@list tptp.q45 tptp.p46 @t78 @t181 tptp.p36 tptp.q36 @t75 tptp.p37))) % 0.23/0.43 (step @p443 :rule chain_m_resolution :premises (@p269 @p432 @p101 @p262 @p260 @p106 @p258 @p109 @p77 @p75 @p73 @p72 @p71 @p431 @p429 @p296 @p252 @p248 @p246 @p245 @p244 @p348 @p225 @p442 @p317 @p313 @p311 @p310 @p309 @p441 @p363 @p206 @p440 @p357 @p354 @p195 @p352 @p199 @p438) :args ((or tptp.p35 tptp.q35 tptp.p26 tptp.q34 tptp.p24 tptp.p22 tptp.p20) (@list true true true true false false false true true false false false true false false true true false false false true false false true true false false false true true false false true true true false false false) (@list tptp.q64 tptp.q55 tptp.q54 tptp.p55 @t58 @t178 tptp.p45 tptp.q45 tptp.p46 @t78 @t181 tptp.p36 tptp.q36 @t75 tptp.p37 tptp.q44 tptp.p44 @t84 @t182 tptp.p34 tptp.q33 @t87 tptp.p33 tptp.q42 tptp.p42 @t90 @t183 tptp.p32 tptp.q32 tptp.q31 @t93 tptp.p31 tptp.p41 tptp.q40 tptp.p40 @t95 @t184 tptp.p30))) % 0.23/0.43 (step @p444 :rule cnf_and_pos :args (@t101 0)) % 0.23/0.43 (step @p445 :rule reordering :premises (@p444) :args ((or @t97 @t234))) % 0.23/0.43 (step @p446 :rule chain_m_resolution :premises (@p304 @p252 @p250 @p248 @p246 @p245 @p244 @p225 @p224 @p222 @p220) :args ((or tptp.p37 tptp.p35 tptp.p31 tptp.p30 tptp.q34 tptp.p24 @t86) @t240 @t241)) % 0.23/0.43 (step @p447 :rule chain_m_resolution :premises (@p350 @p252 @p248 @p246 @p245 @p244 @p348 @p225 @p344 @p317 @p315 @p313 @p311 @p310 @p309 @p446 @p206 @p208 @p219 @p205) :args ((or tptp.p37 tptp.p35 tptp.p30 tptp.q34 tptp.p24 tptp.p22 tptp.p20) (@list true true false false false true false false true true true false false false true true true true false) (@list tptp.q44 tptp.p44 @t84 @t182 tptp.p34 tptp.q33 @t87 tptp.p33 tptp.q42 tptp.q41 tptp.p42 @t90 @t183 tptp.p32 tptp.q32 tptp.p31 @t93 tptp.q31 tptp.q30))) % 0.23/0.43 (step @p448 :rule chain_m_resolution :premises (@p296 @p252 @p248 @p246 @p245 @p244 @p193 @p348 @p198 @p225 @p203 @p359 @p357) :args ((or tptp.p40 tptp.p37 tptp.p35 tptp.q40 tptp.p31 tptp.q34 tptp.p24) (@list true true false false false true true true false false false true) (@list tptp.q44 tptp.p44 @t84 @t182 tptp.p34 tptp.p42 tptp.q33 @t67 @t87 tptp.q41 tptp.p33 tptp.p41))) % 0.23/0.43 (step @p449 :rule chain_m_resolution :premises (@p364 @p252 @p250 @p248 @p246 @p245 @p244 @p225 @p224 @p222 @p220) :args ((or tptp.p40 tptp.p37 tptp.p35 tptp.q34 tptp.p24 @t86) @t240 @t241)) % 0.23/0.43 (step @p450 :rule chain_m_resolution :premises (@p296 @p252 @p248 @p246 @p245 @p244 @p348 @p225 @p366 @p317 @p313 @p311 @p310 @p309 @p449 @p363 @p206 @p448 @p357 @p354 @p195 @p352 @p199 @p447 @p61 @p58 @p57 @p445 @p427 @p443 @p69 @p391 @p67 @p65 @p64 @p211 @p428) :args ((or tptp.p24 tptp.p22 tptp.p20 tptp.p17 tptp.q24 tptp.p15) (@list true true false false false true false false true true false false false true true false false true true true false false false true false false true false false true true true false false false true) (@list tptp.q44 tptp.p44 @t84 @t182 tptp.p34 tptp.q33 @t87 tptp.p33 tptp.q42 tptp.p42 @t90 @t183 tptp.p32 tptp.q32 tptp.q31 @t93 tptp.p31 tptp.p41 tptp.q40 tptp.p40 @t95 @t184 tptp.p30 tptp.p37 @t185 tptp.p27 tptp.q26 @t101 tptp.p26 tptp.q35 tptp.q34 tptp.p35 @t104 @t186 tptp.p25 tptp.q25))) % 0.23/0.43 (step @p451 :rule chain_m_resolution :premises (@p206 @p208 @p304 @p205 @p199 @p195 @p364 @p231 @p306 @p71 @p380 @p252 @p250 @p248 @p246 @p245 @p244 @p242 @p63 @p61 @p59 @p58 @p427 @p57 @p426 @p424) :args ((or tptp.p33 tptp.q33 tptp.p24 tptp.p20 tptp.p17 @t100) (@list true false false true true false true true false true true true true false false false true true true false false true false true true) (@list @t93 tptp.p31 tptp.q30 tptp.p30 @t184 tptp.p40 tptp.p35 @t81 tptp.q35 tptp.p36 tptp.q44 tptp.q43 tptp.p44 @t84 @t182 tptp.p34 tptp.q34 tptp.q36 tptp.p37 @t98 @t185 tptp.p26 tptp.p27 @t101 tptp.q26))) % 0.23/0.43 (step @p452 :rule chain_m_resolution :premises (@p283 @p149 @p142 @p281 @p190 @p187 @p173 @p162 @p302 @p175 @p299 @p178 @p203 @p201 @p196 @p432 @p193 @p275 @p241 @p274 @p239 @p237 @p185 @p236 @p184 @p131 @p128 @p127 @p123 @p121 @p269 @p101 @p262 @p260 @p106 @p258 @p109 @p77 @p75 @p73 @p72 @p71 @p431 @p429 @p304 @p206 @p208 @p205) :args ((or tptp.p44 tptp.q44 tptp.p35 tptp.q43 tptp.p33 tptp.p30 tptp.q35 tptp.p26 tptp.p20) (@list false false true false false true true true true false false false true false false true true true true false true true true true false true true true true false true true true false false false true true false false false true false false true true false) (@list tptp.q72 @t17 tptp.p62 tptp.p63 tptp.p52 tptp.q71 tptp.q61 tptp.q51 tptp.p51 @t70 @t180 tptp.p41 tptp.q40 @t72 tptp.p40 tptp.p42 tptp.q41 @t67 @t170 tptp.q42 tptp.p43 tptp.q52 @t64 @t168 tptp.q53 tptp.p54 tptp.q63 @t38 @t164 tptp.q64 tptp.q55 tptp.q54 tptp.p55 @t58 @t178 tptp.p45 tptp.q45 tptp.p46 @t78 @t181 tptp.p36 tptp.q36 @t75 tptp.p37 tptp.p31 @t93 tptp.q30))) % 0.23/0.43 (step @p453 :rule chain_m_resolution :premises (@p237 @p239 @p236 @p241 @p131 @p193 @p128 @p295 @p123 @p269 @p101 @p262 @p260 @p106 @p258 @p109 @p77 @p75 @p73 @p72 @p71 @p431 @p429 @p364 @p357 @p195 @p199 @p452) :args ((or tptp.p44 tptp.q44 tptp.p35 tptp.q43 tptp.p33 tptp.q35 tptp.p26 tptp.p20) (@list false true true false false true false true false true true true false false false true true false false false true false false true true false false) (@list tptp.p43 @t64 tptp.q42 tptp.q53 @t67 tptp.p54 tptp.p42 @t38 tptp.q64 tptp.q55 tptp.q54 tptp.p55 @t58 @t178 tptp.p45 tptp.q45 tptp.p46 @t78 @t181 tptp.p36 tptp.q36 @t75 tptp.p37 tptp.p41 tptp.p40 @t184 tptp.p30))) % 0.23/0.43 (step @p454 :rule chain_m_resolution :premises (@p206 @p208 @p304 @p205 @p199 @p195 @p364 @p61 @p58 @p57 @p445 @p427 @p453 @p252 @p250 @p248 @p246 @p245 @p244 @p69 @p391 @p67 @p65 @p64 @p211 @p451 @p379 @p377 @p375 @p374 @p373 @p371 @p369 @p450) :args ((or tptp.p24 tptp.p20 tptp.p17 tptp.q24 tptp.p15 tptp.q23 tptp.p13) (@list true false false true true false true false false true false false true true true false false false true true true false false false true true true false false false true false false) (@list @t93 tptp.p31 tptp.q30 tptp.p30 @t184 tptp.p40 tptp.p37 @t185 tptp.p27 tptp.q26 @t101 tptp.p26 tptp.q44 tptp.q43 tptp.p44 @t84 @t182 tptp.p34 tptp.q35 tptp.q34 tptp.p35 @t104 @t186 tptp.p25 tptp.q25 tptp.q33 tptp.p33 @t110 @t187 tptp.p23 tptp.q22 @t113 tptp.p22))) % 0.23/0.43 (step @p455 :rule chain_m_resolution :premises (@p244 @p400 @p242 @p63 @p61 @p59 @p58 @p427 @p57 @p426 @p424) :args ((or tptp.p33 tptp.p30 tptp.q33 tptp.p24 tptp.q32 tptp.p22 tptp.p17 @t100) @t242 @t243)) % 0.23/0.43 (step @p456 :rule chain_m_resolution :premises (@p283 @p149 @p142 @p281 @p190 @p187 @p173 @p162 @p302 @p175 @p299 @p178 @p203 @p201 @p196 @p432 @p193 @p275 @p241 @p274 @p239 @p237 @p185 @p236 @p184 @p131 @p128 @p127 @p123 @p121 @p269 @p101 @p262 @p260 @p106 @p258 @p109 @p77 @p75 @p73 @p72 @p71 @p431 @p429 @p304) :args ((or tptp.p44 tptp.q44 tptp.p35 tptp.q43 tptp.p33 tptp.p31 tptp.p30 tptp.q35 tptp.p26) (@list false false true false false true true true true false false false true false false true true true true false true true true true false true true true true false true true true false false false true true false false false true false false) (@list tptp.q72 @t17 tptp.p62 tptp.p63 tptp.p52 tptp.q71 tptp.q61 tptp.q51 tptp.p51 @t70 @t180 tptp.p41 tptp.q40 @t72 tptp.p40 tptp.p42 tptp.q41 @t67 @t170 tptp.q42 tptp.p43 tptp.q52 @t64 @t168 tptp.q53 tptp.p54 tptp.q63 @t38 @t164 tptp.q64 tptp.q55 tptp.q54 tptp.p55 @t58 @t178 tptp.p45 tptp.q45 tptp.p46 @t78 @t181 tptp.p36 tptp.q36 @t75 tptp.p37))) % 0.23/0.43 (step @p457 :rule chain_m_resolution :premises (@p123 @p128 @p269 @p131 @p101 @p262 @p260 @p106 @p258 @p109 @p77 @p75 @p73 @p72 @p71 @p431 @p429 @p272 @p236 @p237 @p239 @p317 @p311 @p309 @p363 @p206 @p456) :args ((or tptp.p44 tptp.q44 tptp.p35 tptp.q43 tptp.p33 tptp.p30 tptp.q35 tptp.p26 tptp.q32 tptp.p22) (@list false false false true true true false false false true true false false false true false false true false false true false false true false false) (@list @t38 tptp.q64 tptp.p54 tptp.q55 tptp.q54 tptp.p55 @t58 @t178 tptp.p45 tptp.q45 tptp.p46 @t78 @t181 tptp.p36 tptp.q36 @t75 tptp.p37 tptp.q53 @t64 tptp.p43 tptp.q42 @t90 tptp.p32 tptp.q31 @t93 tptp.p31))) % 0.23/0.43 (step @p458 :rule chain_m_resolution :premises (@p311 @p317 @p309 @p239 @p363 @p237 @p206 @p236 @p304 @p272 @p61 @p58 @p57 @p445 @p427 @p457 @p252 @p250 @p248 @p246 @p245 @p244 @p69 @p391 @p67 @p65 @p64 @p211 @p455 @p379 @p399 @p377 @p375 @p374 @p373 @p369 @p397 @p395 @p393 @p385 @p382 @p454) :args ((or tptp.p24 tptp.p17 tptp.q24 tptp.p15 tptp.q23 tptp.p13 @t112) (@list true false false true true false true false false true false false true false false true true true false false false true true true false false false true true true true false false false true true true false true false false) (@list @t90 tptp.p32 tptp.q42 tptp.q31 tptp.p43 @t93 @t64 tptp.p31 tptp.q53 tptp.p37 @t185 tptp.p27 tptp.q26 @t101 tptp.p26 tptp.q44 tptp.q43 tptp.p44 @t84 @t182 tptp.p34 tptp.q35 tptp.q34 tptp.p35 @t104 @t186 tptp.p25 tptp.q25 tptp.q33 tptp.q32 tptp.p33 @t110 @t187 tptp.p23 tptp.p22 tptp.q22 @t113 @t174 tptp.p30 @t189 tptp.p20))) % 0.23/0.43 (step @p459 :rule chain_m_resolution :premises (@p410 @p63 @p61 @p59 @p58 @p427 @p57 @p426 @p424) :args ((or tptp.p31 tptp.p30 tptp.p24 tptp.q31 tptp.p22 tptp.p17 @t100) @t235 @t236)) % 0.23/0.43 (step @p460 :rule chain_m_resolution :premises (@p283 @p149 @p142 @p281 @p190 @p187 @p173 @p162 @p302 @p175 @p299 @p178 @p185 @p203 @p184 @p201 @p131 @p196 @p128 @p127 @p432 @p123 @p121 @p269 @p101 @p262 @p260 @p106 @p258 @p109 @p77 @p75 @p73 @p72 @p71 @p431 @p429 @p350 @p252 @p248 @p246 @p245 @p244 @p348 @p225 @p437 @p317 @p315 @p313 @p311 @p310 @p309 @p433) :args ((or tptp.p35 tptp.p31 tptp.p30 tptp.q35 tptp.p26 tptp.q34 tptp.p24 tptp.q31 tptp.p22) (@list false false true false false true true true true false false true false true true false false true true false true true false true true true false false false true true false false false true false false true true false false false true false false true true true false false false true) (@list tptp.q72 @t17 tptp.p62 tptp.p63 tptp.p52 tptp.q71 tptp.q61 tptp.q51 tptp.p51 @t70 @t180 tptp.q52 tptp.p41 @t168 tptp.q40 tptp.q53 @t72 tptp.p54 tptp.q63 tptp.p40 @t38 @t164 tptp.q64 tptp.q55 tptp.q54 tptp.p55 @t58 @t178 tptp.p45 tptp.q45 tptp.p46 @t78 @t181 tptp.p36 tptp.q36 @t75 tptp.p37 tptp.q44 tptp.p44 @t84 @t182 tptp.p34 tptp.q33 @t87 tptp.p33 tptp.q42 tptp.q41 tptp.p42 @t90 @t183 tptp.p32 tptp.q32))) % 0.23/0.43 (step @p461 :rule chain_m_resolution :premises (@p350 @p252 @p248 @p246 @p245 @p244 @p348 @p225 @p344 @p317 @p315 @p313 @p311 @p310 @p309 @p446 @p61 @p58 @p57 @p445 @p427 @p460 @p69 @p391 @p67 @p65 @p64 @p211 @p459) :args ((or tptp.p31 tptp.p30 tptp.p24 tptp.q31 tptp.p22 tptp.p17 tptp.q24 tptp.p15) (@list true true false false false true false false true true true false false false true true false false true false false true true true false false false true) (@list tptp.q44 tptp.p44 @t84 @t182 tptp.p34 tptp.q33 @t87 tptp.p33 tptp.q42 tptp.q41 tptp.p42 @t90 @t183 tptp.p32 tptp.q32 tptp.p37 @t185 tptp.p27 tptp.q26 @t101 tptp.p26 tptp.q35 tptp.q34 tptp.p35 @t104 @t186 tptp.p25 tptp.q25))) % 0.23/0.43 (step @p462 :rule chain_m_resolution :premises (@p244 @p412 @p242 @p63 @p61 @p59 @p58 @p427 @p57 @p426 @p424) :args ((or tptp.p33 tptp.p31 tptp.p30 tptp.q33 tptp.p24 tptp.p17 @t100) @t242 @t243)) % 0.23/0.43 (step @p463 :rule chain_m_resolution :premises (@p57 @p58 @p445 @p61 @p427 @p304 @p456 @p252 @p250 @p248 @p246 @p245 @p244 @p69 @p391 @p67 @p65 @p64 @p211 @p462 @p379 @p377 @p375 @p374 @p373 @p371 @p369 @p461 @p409 @p407 @p405 @p404 @p403 @p458 @p387 @p385 @p383 @p382 @p454) :args ((or tptp.p24 tptp.p17 tptp.q24 tptp.p15 tptp.q23 tptp.p13 tptp.p11) (@list true true true false false false true true true false false false true true true false false false true true true false false false true false false true true false false false true true true false false false) (@list tptp.p27 tptp.q26 @t185 @t101 tptp.p37 tptp.p26 tptp.q44 tptp.q43 tptp.p44 @t84 @t182 tptp.p34 tptp.q35 tptp.q34 tptp.p35 @t104 @t186 tptp.p25 tptp.q25 tptp.q33 tptp.p33 @t110 @t187 tptp.p23 tptp.q22 @t113 tptp.p22 tptp.q31 tptp.p31 @t116 @t188 tptp.p21 tptp.q21 tptp.q20 tptp.p30 @t118 @t189 tptp.p20))) % 0.23/0.43 (step @p464 :rule cnf_and_pos :args (@t127 0)) % 0.23/0.43 (step @p465 :rule reordering :premises (@p464) :args ((or @t123 @t200))) % 0.23/0.43 (step @p466 :rule chain_m_resolution :premises (@p208 @p206 @p205 @p304 @p199 @p195 @p364 @p231 @p306 @p71 @p380 @p252 @p250 @p248 @p246 @p245 @p244 @p242 @p379 @p377 @p375 @p374 @p373 @p371 @p369 @p368) :args ((or tptp.p37 tptp.q36 tptp.p26 tptp.p24 tptp.p20 tptp.q23 tptp.p13) (@list false false false true true false true true false true true true true false false false true true true false false false true false false) (@list @t93 tptp.q30 tptp.p31 tptp.p30 @t184 tptp.p40 tptp.p35 @t81 tptp.q35 tptp.p36 tptp.q44 tptp.q43 tptp.p44 @t84 @t182 tptp.p34 tptp.q34 tptp.q33 tptp.p33 @t110 @t187 tptp.p23 tptp.q22 @t113 tptp.p22))) % 0.23/0.43 (step @p467 :rule chain_m_resolution :premises (@p244 @p400 @p242 @p379 @p399 @p377 @p375 @p374 @p373 @p369 @p397 @p395 @p393 @p385 @p382 @p466) :args ((or tptp.p37 tptp.q36 tptp.p26 tptp.p24 tptp.q23 tptp.p13 @t112) (@list true true true true true false false false true true true false true false false) (@list tptp.p34 tptp.q34 tptp.q33 tptp.q32 tptp.p33 @t110 @t187 tptp.p23 tptp.p22 tptp.q22 @t113 @t174 tptp.p30 @t189 tptp.p20))) % 0.23/0.43 (step @p468 :rule chain_m_resolution :premises (@p244 @p412 @p242 @p379 @p377 @p375 @p374 @p373 @p371 @p369 @p410 @p409 @p407 @p405 @p404 @p403 @p467 @p387 @p385 @p383 @p382 @p466 @p63 @p61 @p59 @p58 @p57 @p55 @p51 @p49 @p48 @p47 @p465 @p45 @p463 @p423 @p421 @p419 @p417 @p416 @p415 @p413 @p39 @p38 @p36 @p34) :args ((or tptp.p17 tptp.p11 tptp.q16 tptp.p06 tptp.p04 @t132) (@list true true true true false false false true false false true true false false false true true true false false false true true false false false true true false false false true false false true true true false false false true true true true false) (@list tptp.p34 tptp.q34 tptp.q33 tptp.p33 @t110 @t187 tptp.p23 tptp.q22 @t113 tptp.p22 tptp.q31 tptp.p31 @t116 @t188 tptp.p21 tptp.q21 tptp.q20 tptp.p30 @t118 @t189 tptp.p20 tptp.q36 tptp.p37 @t98 @t185 tptp.p27 tptp.q26 tptp.p26 @t124 @t190 tptp.p16 tptp.q15 @t127 tptp.p15 tptp.q24 tptp.q23 tptp.p24 @t130 @t191 tptp.p14 tptp.q14 tptp.p13 tptp.q13 @t133 @t176))) % 0.23/0.43 (step @p469 :rule and_elim :premises (@p7) :args (171)) % 0.23/0.43 (step @p470 :rule reordering :premises (@p469) :args ((or tptp.p12 tptp.q12 tptp.q11 tptp.p02))) % 0.23/0.43 (step @p471 :rule and_elim :premises (@p7) :args (9)) % 0.23/0.43 (step @p472 :rule and_elim :premises (@p7) :args (117)) % 0.23/0.43 (step @p473 :rule cnf_and_pos :args (@t192 1)) % 0.23/0.43 (step @p474 :rule reordering :premises (@p473) :args ((or @t114 (not @t192)))) % 0.23/0.43 (step @p475 :rule cnf_and_pos :args (@t136 2)) % 0.23/0.43 (step @p476 :rule reordering :premises (@p475) :args ((or @t112 @t244))) % 0.23/0.43 (step @p477 :rule cnf_and_pos :args (@t136 3)) % 0.23/0.43 (step @p478 :rule reordering :premises (@p477) :args ((or @t109 @t244))) % 0.23/0.43 (step @p479 :rule chain_m_resolution :premises (@p450 @p217 @p213 @p389 @p216) :args ((or tptp.p22 tptp.p20 tptp.p17 tptp.p15 @t106) @t228 @t245)) % 0.23/0.43 (step @p480 :rule chain_m_resolution :premises (@p437 @p231 @p230 @p228 @p226) :args ((or tptp.p42 tptp.q42 tptp.p33 tptp.q41 tptp.p31 tptp.p30 tptp.p26 @t80) @t228 @t246)) % 0.23/0.43 (step @p481 :rule chain_m_resolution :premises (@p326 @p357) :args ((or tptp.q63 tptp.p53 tptp.q52 tptp.p42 tptp.p40) @t237 @t238)) % 0.23/0.43 (step @p482 :rule chain_m_resolution :premises (@p142 @p144 @p283 @p189 @p149 @p159 @p281 @p187 @p173 @p162 @p302 @p175 @p299 @p178 @p203 @p201 @p196 @p481) :args ((or tptp.q63 tptp.p53 tptp.q52 tptp.p42 tptp.q41 tptp.p31) (@list false true true false false true false true true true true false false false true false false) (@list tptp.p63 @t17 tptp.q62 tptp.q72 @t44 tptp.p62 tptp.p52 tptp.q71 tptp.q61 tptp.q51 tptp.p51 @t70 @t180 tptp.p41 tptp.q40 @t72 tptp.p40))) % 0.23/0.43 (step @p483 :rule chain_m_resolution :premises (@p106 @p109 @p262 @p255 @p131 @p256 @p128 @p334 @p331) :args ((or tptp.q53 tptp.p44 tptp.q44 tptp.p35 @t12) (@list false true true false false true false true) (@list tptp.p45 @t58 tptp.q45 tptp.q54 @t55 tptp.p54 tptp.p46 @t38))) % 0.23/0.43 (step @p484 :rule chain_m_resolution :premises (@p71 @p306 @p72 @p431 @p231 @p75 @p429 @p483 @p334 @p335 @p482 @p236 @p325 @p323 @p237 @p321 @p239 @p252 @p250 @p248 @p246 @p245 @p244 @p480 @p317 @p315 @p313 @p311 @p310 @p206 @p309 @p208 @p219 @p205) :args ((or tptp.p33 tptp.p30 tptp.p26 tptp.q33 tptp.p24 tptp.q32 tptp.p22 tptp.p20) (@list true true true false true false false false false false true true true false false false true true true false false false true true true true false false true false true true false) (@list tptp.q35 tptp.p36 tptp.q36 @t81 @t181 @t75 tptp.p35 tptp.p46 tptp.p37 tptp.q63 tptp.q53 tptp.q52 tptp.p53 @t64 @t179 tptp.p43 tptp.q44 tptp.q43 tptp.p44 @t84 @t182 tptp.p34 tptp.q34 tptp.q42 tptp.q41 tptp.p42 @t90 @t183 tptp.p31 tptp.p32 @t93 tptp.q31 tptp.q30))) % 0.23/0.43 (step @p485 :rule chain_m_resolution :premises (@p442 @p231 @p230 @p228 @p226) :args ((or tptp.p42 tptp.p40 tptp.q42 tptp.p33 tptp.p26 @t80) @t228 @t246)) % 0.23/0.43 (step @p486 :rule chain_m_resolution :premises (@p71 @p306 @p72 @p431 @p231 @p75 @p429 @p483 @p334 @p335 @p481 @p236 @p325 @p323 @p237 @p321 @p239 @p252 @p250 @p248 @p246 @p245 @p244 @p485 @p193 @p274 @p198 @p275) :args ((or tptp.p40 tptp.p33 tptp.p26 tptp.q33 tptp.p24 @t66) (@list true true true false true false false false false false true true true false false false true true true false false false true true true true false) (@list tptp.q35 tptp.p36 tptp.q36 @t81 @t181 @t75 tptp.p35 tptp.p46 tptp.p37 tptp.q63 tptp.q53 tptp.q52 tptp.p53 @t64 @t179 tptp.p43 tptp.q44 tptp.q43 tptp.p44 @t84 @t182 tptp.p34 tptp.q34 tptp.p42 tptp.q42 @t67 @t170))) % 0.23/0.43 (step @p487 :rule chain_m_resolution :premises (@p71 @p306 @p72 @p431 @p231 @p75 @p429 @p483 @p334 @p335 @p481 @p236 @p325 @p323 @p237 @p321 @p239 @p252 @p250 @p248 @p246 @p245 @p244 @p485 @p317 @p313 @p311 @p310 @p309 @p363 @p206 @p203 @p486 @p357 @p354 @p195 @p352 @p199 @p484) :args ((or tptp.p33 tptp.p26 tptp.q33 tptp.p24 tptp.q32 tptp.p22 tptp.p20) (@list true true true false true false false false false false true true true false false false true true true false false false true true true false false false true false false true true true true false false false) (@list tptp.q35 tptp.p36 tptp.q36 @t81 @t181 @t75 tptp.p35 tptp.p46 tptp.p37 tptp.q63 tptp.q53 tptp.q52 tptp.p53 @t64 @t179 tptp.p43 tptp.q44 tptp.q43 tptp.p44 @t84 @t182 tptp.p34 tptp.q34 tptp.q42 tptp.p42 @t90 @t183 tptp.p32 tptp.q31 @t93 tptp.p31 tptp.q41 tptp.p41 tptp.q40 tptp.p40 @t95 @t184 tptp.p30))) % 0.23/0.43 (step @p488 :rule chain_m_resolution :premises (@p335 @p482 @p236 @p325 @p323 @p237 @p321 @p239 @p250 @p248 @p246 @p245 @p244 @p228 @p231 @p344 @p317 @p315 @p313 @p311 @p310 @p206 @p309 @p208 @p219 @p205) :args ((or tptp.p37 tptp.p33 tptp.p30 tptp.q33 tptp.p24 tptp.q32 tptp.p22 tptp.p20) (@list false true true true false false false true true false false false true false false true true true false false true false true true false) (@list tptp.q63 tptp.q53 tptp.q52 tptp.p53 @t64 @t179 tptp.p43 tptp.q43 tptp.p44 @t84 @t182 tptp.p34 tptp.q34 @t81 tptp.p35 tptp.q42 tptp.q41 tptp.p42 @t90 @t183 tptp.p31 tptp.p32 @t93 tptp.q31 tptp.q30))) % 0.23/0.43 (step @p489 :rule chain_m_resolution :premises (@p335 @p481 @p236 @p325 @p323 @p237 @p321 @p239 @p250 @p248 @p246 @p245 @p244 @p193 @p274 @p228 @p198 @p275 @p231 @p203 @p359 @p357) :args ((or tptp.p40 tptp.p37 tptp.p33 tptp.q40 tptp.p31 tptp.q33 tptp.p24) (@list false true true true false false false true true false false false true true true true false false false false true) (@list tptp.q63 tptp.q53 tptp.q52 tptp.p53 @t64 @t179 tptp.p43 tptp.q43 tptp.p44 @t84 @t182 tptp.p34 tptp.p42 tptp.q42 tptp.q34 @t67 @t170 @t81 tptp.q41 tptp.p35 tptp.p41))) % 0.23/0.43 (step @p490 :rule chain_m_resolution :premises (@p335 @p481 @p236 @p325 @p323 @p237 @p321 @p239 @p250 @p248 @p246 @p245 @p244 @p228 @p231 @p366 @p317 @p313 @p311 @p310 @p309 @p363 @p206 @p489 @p354 @p195 @p352 @p199 @p488 @p61 @p58 @p57 @p445 @p427 @p487) :args ((or tptp.p33 tptp.q33 tptp.p24 tptp.q32 tptp.p22 tptp.p20 tptp.p17) (@list false true true true false false false true true false false false true false false true true false false false true false false true true false false false true false false true false false) (@list tptp.q63 tptp.q53 tptp.q52 tptp.p53 @t64 @t179 tptp.p43 tptp.q43 tptp.p44 @t84 @t182 tptp.p34 tptp.q34 @t81 tptp.p35 tptp.q42 tptp.p42 @t90 @t183 tptp.p32 tptp.q31 @t93 tptp.p31 tptp.q40 tptp.p40 @t95 @t184 tptp.p30 tptp.p37 @t185 tptp.p27 tptp.q26 @t101 tptp.p26))) % 0.23/0.43 (step @p491 :rule chain_m_resolution :premises (@p346 @p317 @p315 @p313 @p311 @p310 @p206 @p309 @p208 @p219 @p205) :args ((or tptp.p37 tptp.p33 tptp.p30 tptp.q36 tptp.p26 tptp.q32 tptp.p22 tptp.p20) @t247 @t248)) % 0.23/0.43 (step @p492 :rule chain_m_resolution :premises (@p367 @p317 @p313 @p311 @p310 @p309 @p363 @p206 @p360 @p354 @p195 @p352 @p199 @p491 @p63 @p61 @p59 @p58 @p427 @p57 @p426 @p424) :args ((or tptp.p33 tptp.q32 tptp.p22 tptp.p20 tptp.p17 @t100) (@list true true false false false true false false true true false false false true true false false true false true true) (@list tptp.q42 tptp.p42 @t90 @t183 tptp.p32 tptp.q31 @t93 tptp.p31 tptp.q40 tptp.p40 @t95 @t184 tptp.p30 tptp.q36 tptp.p37 @t98 @t185 tptp.p26 tptp.p27 @t101 tptp.q26))) % 0.23/0.43 (step @p493 :rule chain_m_resolution :premises (@p437 @p317 @p315 @p313 @p311 @p310 @p206 @p309 @p208 @p219 @p205) :args ((or tptp.p35 tptp.p33 tptp.p30 tptp.q35 tptp.p26 tptp.q32 tptp.p22 tptp.p20) @t247 @t248)) % 0.23/0.43 (step @p494 :rule chain_m_resolution :premises (@p442 @p317 @p313 @p311 @p310 @p309 @p363 @p206 @p439 @p354 @p195 @p352 @p199 @p493) :args ((or tptp.p35 tptp.p33 tptp.q35 tptp.p26 tptp.q32 tptp.p22 tptp.p20) (@list true true false false false true false false true true false false false) (@list tptp.q42 tptp.p42 @t90 @t183 tptp.p32 tptp.q31 @t93 tptp.p31 tptp.q40 tptp.p40 @t95 @t184 tptp.p30))) % 0.23/0.43 (step @p495 :rule chain_m_resolution :premises (@p344 @p317 @p315 @p313 @p311 @p310 @p206 @p309 @p208 @p219 @p205) :args ((or tptp.p37 tptp.p35 tptp.p33 tptp.p30 tptp.q32 tptp.p22 tptp.p20) @t247 @t248)) % 0.23/0.43 (step @p496 :rule chain_m_resolution :premises (@p366 @p317 @p313 @p311 @p310 @p309 @p363 @p206 @p359 @p357 @p354 @p195 @p352 @p199 @p495 @p61 @p58 @p57 @p445 @p427 @p494 @p69 @p67 @p65 @p64 @p211 @p492 @p215 @p217 @p490 @p379 @p399 @p377 @p375 @p374 @p373 @p479) :args ((or tptp.p22 tptp.p20 tptp.p17 tptp.p15 tptp.q22 tptp.p13) (@list true true false false false true false false true true true false false false true false false true false false true true false false false true true false false true true true false false false true) (@list tptp.q42 tptp.p42 @t90 @t183 tptp.p32 tptp.q31 @t93 tptp.p31 tptp.p41 tptp.q40 tptp.p40 @t95 @t184 tptp.p30 tptp.p37 @t185 tptp.p27 tptp.q26 @t101 tptp.p26 tptp.q35 tptp.p35 @t104 @t186 tptp.p25 tptp.q25 tptp.q24 @t107 tptp.p24 tptp.q33 tptp.q32 tptp.p33 @t110 @t187 tptp.p23 tptp.q23))) % 0.23/0.43 (step @p497 :rule chain_m_resolution :premises (@p461 @p217 @p213 @p389 @p216) :args ((or tptp.p31 tptp.p30 tptp.q31 tptp.p22 tptp.p17 tptp.p15 @t106) @t228 @t245)) % 0.23/0.43 (step @p498 :rule chain_m_resolution :premises (@p71 @p306 @p72 @p431 @p231 @p75 @p429 @p483 @p334 @p335 @p482 @p236 @p325 @p323 @p237 @p321 @p239 @p252 @p250 @p248 @p246 @p245 @p244 @p480) :args ((or tptp.p42 tptp.q42 tptp.p33 tptp.q41 tptp.p31 tptp.p30 tptp.p26 tptp.q33 tptp.p24) (@list true true true false true false false false false false true true true false false false true true true false false false true) (@list tptp.q35 tptp.p36 tptp.q36 @t81 @t181 @t75 tptp.p35 tptp.p46 tptp.p37 tptp.q63 tptp.q53 tptp.q52 tptp.p53 @t64 @t179 tptp.p43 tptp.q44 tptp.q43 tptp.p44 @t84 @t182 tptp.p34 tptp.q34))) % 0.23/0.43 (step @p499 :rule chain_m_resolution :premises (@p335 @p482 @p236 @p325 @p323 @p237 @p321 @p239 @p250 @p248 @p246 @p245 @p244 @p228 @p231 @p344 @p61 @p58 @p57 @p445 @p427 @p498) :args ((or tptp.p42 tptp.q42 tptp.p33 tptp.q41 tptp.p31 tptp.p30 tptp.q33 tptp.p24 tptp.p17) (@list false true true true false false false true true false false false true false false true false false true false false) (@list tptp.q63 tptp.q53 tptp.q52 tptp.p53 @t64 @t179 tptp.p43 tptp.q43 tptp.p44 @t84 @t182 tptp.p34 tptp.q34 @t81 tptp.p35 tptp.p37 @t185 tptp.p27 tptp.q26 @t101 tptp.p26))) % 0.23/0.43 (step @p500 :rule chain_m_resolution :premises (@p346 @p63 @p61 @p59 @p58 @p427 @p57 @p426 @p424) :args ((or tptp.p42 tptp.q42 tptp.p33 tptp.q41 tptp.p31 tptp.p30 tptp.p17 @t100) @t235 @t236)) % 0.23/0.43 (step @p501 :rule chain_m_resolution :premises (@p57 @p445 @p58 @p427 @p61 @p437 @p344 @p69 @p67 @p65 @p64 @p211 @p500 @p215 @p217 @p499 @p317 @p315 @p313 @p311 @p310 @p309 @p379 @p399 @p377 @p375 @p374 @p373 @p497 @p409 @p407 @p405 @p404 @p403 @p387 @p385 @p383 @p382 @p496) :args ((or tptp.p22 tptp.p17 tptp.p15 tptp.q22 tptp.p13 tptp.q21 tptp.p11) (@list true true false true false false true true false false false true true false false true true true false false false true true true false false false true true true false false false true true false false false) (@list tptp.q26 tptp.p27 @t101 @t185 tptp.p26 tptp.p37 tptp.q35 tptp.p35 @t104 @t186 tptp.p25 tptp.q25 tptp.q24 @t107 tptp.p24 tptp.q42 tptp.q41 tptp.p42 @t90 @t183 tptp.p32 tptp.q33 tptp.q32 tptp.p33 @t110 @t187 tptp.p23 tptp.q23 tptp.q31 tptp.p31 @t116 @t188 tptp.p21 tptp.q20 tptp.p30 @t118 @t189 tptp.p20))) % 0.23/0.43 (step @p502 :rule chain_m_resolution :premises (@p367 @p317 @p313 @p311 @p310 @p309 @p363 @p206 @p360 @p354 @p195 @p352 @p199 @p491 @p399 @p377 @p375 @p374 @p373 @p389 @p217 @p368) :args ((or tptp.p37 tptp.q36 tptp.p26 tptp.p22 tptp.p20 tptp.q22 tptp.p13) (@list true true false false false true false false true true false false false true true false false false true false false) (@list tptp.q42 tptp.p42 @t90 @t183 tptp.p32 tptp.q31 @t93 tptp.p31 tptp.q40 tptp.p40 @t95 @t184 tptp.p30 tptp.q32 tptp.p33 @t110 @t187 tptp.p23 tptp.q23 @t107 tptp.p24))) % 0.23/0.43 (step @p503 :rule chain_m_resolution :premises (@p346 @p317 @p315 @p313 @p311 @p310 @p309 @p399 @p377 @p375 @p374 @p373 @p389 @p217 @p410 @p409 @p407 @p405 @p404 @p403 @p387 @p385 @p383 @p382 @p502 @p63 @p61 @p59 @p58 @p57 @p55 @p51 @p49 @p48 @p47 @p465 @p45 @p501) :args ((or tptp.p22 tptp.p17 tptp.q22 tptp.p13 tptp.q21 tptp.p11 tptp.q16 tptp.p06) (@list true true true false false false true true false false false true false false true true false false false true true false false false true true false false false true true false false false true false false) (@list tptp.q42 tptp.q41 tptp.p42 @t90 @t183 tptp.p32 tptp.q32 tptp.p33 @t110 @t187 tptp.p23 tptp.q23 @t107 tptp.p24 tptp.q31 tptp.p31 @t116 @t188 tptp.p21 tptp.q20 tptp.p30 @t118 @t189 tptp.p20 tptp.q36 tptp.p37 @t98 @t185 tptp.p27 tptp.q26 tptp.p26 @t124 @t190 tptp.p16 tptp.q15 @t127 tptp.p15))) % 0.23/0.43 (step @p504 :rule cnf_and_pos :args (@t133 0)) % 0.23/0.43 (step @p505 :rule reordering :premises (@p504) :args ((or @t129 @t199))) % 0.23/0.43 (step @p506 :rule chain_m_resolution :premises (@p215 @p211 @p217 @p209 @p368) :args ((or tptp.p37 tptp.q36 tptp.p26 tptp.p22 tptp.p20 tptp.q25 tptp.p15) (@list false false true false) (@list tptp.q24 @t107 tptp.p25 tptp.p24))) % 0.23/0.43 (step @p507 :rule chain_m_resolution :premises (@p411 @p409 @p407 @p405 @p404 @p403 @p387 @p385 @p383 @p382 @p506 @p63 @p61 @p59 @p58 @p57 @p55 @p53 @p51 @p49 @p48 @p47 @p45 @p44 @p42 @p40) :args ((or tptp.p22 tptp.p17 tptp.q21 tptp.p11 tptp.q16 tptp.p06 @t126) (@list true true false false false true true false false false true true false false false true true true false false false true true true false) (@list tptp.q31 tptp.p31 @t116 @t188 tptp.p21 tptp.q20 tptp.p30 @t118 @t189 tptp.p20 tptp.q36 tptp.p37 @t98 @t185 tptp.p27 tptp.q26 tptp.q25 tptp.p26 @t124 @t190 tptp.p16 tptp.p15 tptp.q15 @t127 @t175))) % 0.23/0.43 (step @p508 :rule chain_m_resolution :premises (@p461 @p409 @p407 @p405 @p404 @p403 @p387 @p385 @p383 @p382 @p450) :args ((or tptp.p24 tptp.p22 tptp.p17 tptp.q24 tptp.p15 tptp.q21 tptp.p11) (@list true true false false false true true false false false) (@list tptp.q31 tptp.p31 @t116 @t188 tptp.p21 tptp.q20 tptp.p30 @t118 @t189 tptp.p20))) % 0.23/0.43 (step @p509 :rule chain_m_resolution :premises (@p410 @p409 @p407 @p405 @p404 @p403 @p387 @p385 @p383 @p382 @p368 @p63 @p61 @p59 @p58 @p57 @p55 @p51 @p49 @p48 @p47 @p465 @p45 @p508 @p423 @p419 @p417 @p416 @p415 @p507 @p505 @p39 @p503 @p478 @p476 @p474 @p472 @p471 @p470 @p468 @p33 @p32 @p30) :args ((or tptp.p17 tptp.q16 tptp.p06 tptp.p04 tptp.p02 @t138) (@list true true false false false true true false false false true true false false false true true false false false true false false true true false false false true true false false true true true false false false true true true true) (@list tptp.q31 tptp.p31 @t116 @t188 tptp.p21 tptp.q20 tptp.p30 @t118 @t189 tptp.p20 tptp.q36 tptp.p37 @t98 @t185 tptp.p27 tptp.q26 tptp.p26 @t124 @t190 tptp.p16 tptp.q15 @t127 tptp.p15 tptp.q24 tptp.p24 @t130 @t191 tptp.p14 tptp.q14 tptp.q13 @t133 tptp.p13 tptp.q22 tptp.q21 tptp.p22 @t136 @t192 tptp.p12 tptp.q12 tptp.p11 @t139 tptp.q11))) % 0.23/0.43 (step @p510 :rule and_elim :premises (@p7) :args (169)) % 0.23/0.43 (step @p511 :rule and_elim :premises (@p7) :args (7)) % 0.23/0.43 (step @p512 :rule reordering :premises (@p511) :args ((or @t119 @t142))) % 0.23/0.43 (step @p513 :rule and_elim :premises (@p7) :args (115)) % 0.23/0.43 (step @p514 :rule chain_m_resolution :premises (@p381 @p63 @p61 @p59 @p58 @p57 @p55 @p53 @p51 @p49 @p48 @p47 @p45 @p44 @p42 @p40) :args ((or tptp.p20 tptp.p17 tptp.p13 tptp.q16 tptp.p06 @t126) @t249 @t250)) % 0.23/0.43 (step @p515 :rule chain_m_resolution :premises (@p466 @p63 @p61 @p59 @p58 @p57 @p55 @p51 @p49 @p48 @p47 @p465 @p45 @p454 @p423 @p421 @p419 @p417 @p416 @p415 @p514 @p39 @p38 @p36 @p34) :args ((or tptp.p20 tptp.p17 tptp.q16 tptp.p06 tptp.p04 @t132) (@list true true false false false true true false false false true false false true true true false false false true true true true false) (@list tptp.q36 tptp.p37 @t98 @t185 tptp.p27 tptp.q26 tptp.p26 @t124 @t190 tptp.p16 tptp.q15 @t127 tptp.p15 tptp.q24 tptp.q23 tptp.p24 @t130 @t191 tptp.p14 tptp.q14 tptp.p13 tptp.q13 @t133 @t176))) % 0.23/0.43 (step @p516 :rule cnf_and_pos :args (@t141 1)) % 0.23/0.43 (step @p517 :rule reordering :premises (@p516) :args ((or @t115 (not @t141)))) % 0.23/0.43 (step @p518 :rule chain_m_resolution :premises (@p496 @p369 @p397 @p395 @p393) :args ((or tptp.p20 tptp.p17 tptp.p15 tptp.p13 @t112) @t228 @t251)) % 0.23/0.43 (step @p519 :rule cnf_and_pos :args (@t116 2)) % 0.23/0.43 (step @p520 :rule reordering :premises (@p519) :args ((or @t92 @t232))) % 0.23/0.43 (step @p521 :rule chain_m_resolution :premises (@p57 @p445 @p58 @p427 @p61 @p486 @p489 @p203 @p357) :args ((or tptp.p40 tptp.p33 tptp.q40 tptp.p31 tptp.q33 tptp.p24 tptp.p17) (@list true true false true false false false true) (@list tptp.q26 tptp.p27 @t101 @t185 tptp.p26 tptp.p37 tptp.q41 tptp.p41))) % 0.23/0.43 (step @p522 :rule chain_m_resolution :premises (@p360 @p63 @p61 @p59 @p58 @p427 @p57 @p426 @p424) :args ((or tptp.p40 tptp.p33 tptp.q40 tptp.p31 tptp.p17 @t100) @t235 @t236)) % 0.23/0.43 (step @p523 :rule chain_m_resolution :premises (@p57 @p445 @p58 @p427 @p61 @p442 @p359 @p69 @p67 @p65 @p64 @p211 @p522 @p215 @p217 @p521 @p225 @p224 @p222 @p220 @p193 @p198 @p274 @p275 @p203 @p357) :args ((or tptp.p40 tptp.q40 tptp.p31 tptp.p17 tptp.p15 @t86) (@list true true false true false false true true false false false true true false false true true true false true true true false false true) (@list tptp.q26 tptp.p27 @t101 @t185 tptp.p26 tptp.p37 tptp.q35 tptp.p35 @t104 @t186 tptp.p25 tptp.q25 tptp.q24 @t107 tptp.p24 tptp.p33 tptp.q33 @t87 @t172 tptp.p42 @t67 tptp.q42 @t170 tptp.q41 tptp.p41))) % 0.23/0.43 (step @p524 :rule chain_m_resolution :premises (@p361 @p63 @p61 @p59 @p58 @p427 @p57 @p426 @p424) :args ((or tptp.p40 tptp.q40 tptp.p31 tptp.p24 tptp.p17 @t100) @t235 @t236)) % 0.23/0.43 (step @p525 :rule chain_m_resolution :premises (@p57 @p445 @p58 @p427 @p61 @p440 @p448 @p69 @p391 @p67 @p65 @p64 @p211 @p524 @p217 @p213 @p389 @p216) :args ((or tptp.p40 tptp.q40 tptp.p31 tptp.p17 tptp.p15 @t106) (@list true true false true false false true true true false false false true true true true false) (@list tptp.q26 tptp.p27 @t101 @t185 tptp.p26 tptp.p37 tptp.q35 tptp.q34 tptp.p35 @t104 @t186 tptp.p25 tptp.q25 tptp.p24 tptp.q24 @t107 @t173))) % 0.23/0.43 (step @p526 :rule chain_m_resolution :premises (@p57 @p445 @p58 @p427 @p61 @p439 @p359 @p69 @p67 @p65 @p64 @p211 @p215 @p217 @p521 @p522 @p379 @p377 @p375 @p374 @p373 @p525 @p371 @p369 @p309 @p523 @p311 @p315 @p203 @p357 @p354 @p195 @p352 @p199 @p205 @p409 @p520 @p407 @p405 @p404 @p403 @p518) :args ((or tptp.p20 tptp.p17 tptp.p15 tptp.p13 tptp.q20 tptp.p11) (@list true true false true false false true true false false false true false false true true true false false false true true false false true true true false true true true false false false true true true false false false true) (@list tptp.q26 tptp.p27 @t101 @t185 tptp.p26 tptp.p37 tptp.q35 tptp.p35 @t104 @t186 tptp.p25 tptp.q24 @t107 tptp.p24 tptp.q25 tptp.q33 tptp.p33 @t110 @t187 tptp.p23 tptp.q23 tptp.q22 @t113 tptp.p22 tptp.q32 tptp.p32 @t90 tptp.q41 tptp.p41 tptp.q40 tptp.p40 @t95 @t184 tptp.p30 tptp.q31 tptp.q30 tptp.p31 @t116 @t188 tptp.p21 tptp.q21))) % 0.23/0.43 (step @p527 :rule chain_m_resolution :premises (@p502 @p369 @p397 @p395 @p393) :args ((or tptp.p37 tptp.q36 tptp.p26 tptp.p20 tptp.p13 @t112) @t228 @t251)) % 0.23/0.43 (step @p528 :rule chain_m_resolution :premises (@p369 @p371 @p309 @p373 @p311 @p222 @p374 @p389 @p315 @p225 @p377 @p217 @p203 @p360 @p361 @p357 @p354 @p195 @p352 @p199 @p205 @p409 @p520 @p407 @p405 @p404 @p403 @p527 @p63 @p61 @p59 @p58 @p57 @p55 @p51 @p49 @p48 @p47 @p465 @p45 @p526) :args ((or tptp.p20 tptp.p17 tptp.p13 tptp.q20 tptp.p11 tptp.q16 tptp.p06) (@list true false false true true true true true false true false false false false true true true false false false true true true false false false true true true false false false true true false false false true false false) (@list @t113 tptp.p22 tptp.q22 tptp.p32 tptp.q32 tptp.p23 tptp.q23 @t90 @t87 @t187 @t107 tptp.q41 tptp.p33 tptp.p24 tptp.p41 tptp.q40 tptp.p40 @t95 @t184 tptp.p30 tptp.q31 tptp.q30 tptp.p31 @t116 @t188 tptp.p21 tptp.q21 tptp.q36 tptp.p37 @t98 @t185 tptp.p27 tptp.q26 tptp.p26 @t124 @t190 tptp.p16 tptp.q15 @t127 tptp.p15))) % 0.23/0.43 (step @p529 :rule chain_m_resolution :premises (@p361 @p354 @p195 @p352 @p199 @p205 @p520 @p407 @p405 @p404 @p403 @p217 @p395 @p215 @p369 @p211 @p506 @p209 @p63 @p61 @p59 @p58 @p57 @p55 @p53 @p51 @p49 @p48 @p47 @p45 @p44 @p42 @p40) :args ((or tptp.p20 tptp.p17 tptp.q20 tptp.p11 tptp.q16 tptp.p06 @t126) (@list true true false false false true true false false false true true true false false false true true true false false false true true true false false false true true true false) (@list tptp.q40 tptp.p40 @t95 @t184 tptp.p30 tptp.q30 tptp.p31 @t116 @t188 tptp.p21 tptp.p24 tptp.q21 @t107 @t113 tptp.q24 tptp.p22 tptp.p25 tptp.q36 tptp.p37 @t98 @t185 tptp.p27 tptp.q26 tptp.q25 tptp.p26 @t124 @t190 tptp.p16 tptp.p15 tptp.q15 @t127 @t175))) % 0.23/0.43 (step @p530 :rule chain_m_resolution :premises (@p57 @p445 @p58 @p427 @p61 @p440 @p448 @p69 @p391 @p67 @p65 @p64 @p211 @p524 @p354 @p195 @p352 @p199 @p205 @p520 @p407 @p405 @p404 @p403 @p395 @p369 @p450) :args ((or tptp.p24 tptp.p20 tptp.p17 tptp.q24 tptp.p15 tptp.q20 tptp.p11) (@list true true false true false false true true true false false false true true true false false false true true false false false true false false) (@list tptp.q26 tptp.p27 @t101 @t185 tptp.p26 tptp.p37 tptp.q35 tptp.q34 tptp.p35 @t104 @t186 tptp.p25 tptp.q25 tptp.q40 tptp.p40 @t95 @t184 tptp.p30 tptp.q30 tptp.p31 @t116 @t188 tptp.p21 tptp.q21 @t113 tptp.p22))) % 0.23/0.43 (step @p531 :rule chain_m_resolution :premises (@p361 @p354 @p195 @p352 @p199 @p205 @p520 @p407 @p405 @p404 @p403 @p395 @p369 @p368 @p63 @p61 @p59 @p58 @p57 @p55 @p51 @p49 @p48 @p47 @p465 @p45 @p530 @p423 @p419 @p417 @p416 @p415 @p529 @p505 @p39 @p528) :args ((or tptp.p20 tptp.p17 tptp.q20 tptp.p11 tptp.q16 tptp.p06 tptp.p04) (@list true true false false false true true false false false true false false true true false false false true true false false false true false false true true false false false true true false false) (@list tptp.q40 tptp.p40 @t95 @t184 tptp.p30 tptp.q30 tptp.p31 @t116 @t188 tptp.p21 tptp.q21 @t113 tptp.p22 tptp.q36 tptp.p37 @t98 @t185 tptp.p27 tptp.q26 tptp.p26 @t124 @t190 tptp.p16 tptp.q15 @t127 tptp.p15 tptp.q24 tptp.p24 @t130 @t191 tptp.p14 tptp.q14 tptp.q13 @t133 tptp.p13))) % 0.23/0.43 (step @p532 :rule cnf_and_pos :args (@t139 0)) % 0.23/0.43 (step @p533 :rule reordering :premises (@p532) :args ((or @t135 @t198))) % 0.23/0.43 (step @p534 :rule chain_m_resolution :premises (@p502 @p63 @p61 @p59 @p58 @p57 @p55 @p51 @p49 @p48 @p47 @p465 @p45 @p496) :args ((or tptp.p22 tptp.p20 tptp.p17 tptp.q22 tptp.p13 tptp.q16 tptp.p06) (@list true true false false false true true false false false true false false) (@list tptp.q36 tptp.p37 @t98 @t185 tptp.p27 tptp.q26 tptp.p26 @t124 @t190 tptp.p16 tptp.q15 @t127 tptp.p15))) % 0.23/0.43 (step @p535 :rule chain_m_resolution :premises (@p506 @p63 @p61 @p59 @p58 @p57 @p55 @p53 @p51 @p49 @p48 @p47 @p45 @p44 @p42 @p40) :args ((or tptp.p22 tptp.p20 tptp.p17 tptp.q16 tptp.p06 @t126) @t249 @t250)) % 0.23/0.43 (step @p536 :rule chain_m_resolution :premises (@p368 @p63 @p61 @p59 @p58 @p57 @p55 @p51 @p49 @p48 @p47 @p465 @p45 @p450 @p423 @p419 @p417 @p416 @p415 @p535 @p505 @p39 @p534 @p478 @p474 @p472 @p471 @p470 @p533 @p33 @p531 @p517 @p515 @p513 @p512 @p510 @p509 @p28 @p26 @p25 @p23 @p22 @p21 @p19) :args ((or tptp.p04 tptp.p02 @t146) (@list true true false false false true true false false false true false false true true false false false true true false false true true false false false true false false true true false true false true true false true true false true true) (@list tptp.q36 tptp.p37 @t98 @t185 tptp.p27 tptp.q26 tptp.p26 @t124 @t190 tptp.p16 tptp.q15 @t127 tptp.p15 tptp.q24 tptp.p24 @t130 @t191 tptp.p14 tptp.q14 tptp.q13 @t133 tptp.p13 tptp.q22 tptp.p22 @t136 @t192 tptp.p12 tptp.q11 @t139 tptp.p11 tptp.q20 tptp.q12 @t141 tptp.p20 tptp.p10 tptp.q10 tptp.q16 @t144 tptp.p17 tptp.p06 tptp.p07 @t147 tptp.q06))) % 0.23/0.43 (step @p537 :rule and_elim :premises (@p7) :args (166)) % 0.23/0.43 (step @p538 :rule and_elim :premises (@p7) :args (4)) % 0.23/0.43 (step @p539 :rule reordering :premises (@p538) :args ((or @t128 @t151))) % 0.23/0.43 (step @p540 :rule and_elim :premises (@p7) :args (112)) % 0.23/0.43 (step @p541 :rule cnf_and_pos :args (@t150 2)) % 0.23/0.43 (step @p542 :rule reordering :premises (@p541) :args ((or @t126 @t252))) % 0.23/0.43 (step @p543 :rule cnf_and_pos :args (@t150 3)) % 0.23/0.43 (step @p544 :rule reordering :premises (@p543) :args ((or @t123 @t252))) % 0.23/0.43 (step @p545 :rule and_elim :premises (@p7) :args (122)) % 0.23/0.43 (step @p546 :rule cnf_and_pos :args (@t121 0)) % 0.23/0.43 (step @p547 :rule reordering :premises (@p546) :args ((or @t120 (not @t121)))) % 0.23/0.43 (step @p548 :rule chain_m_resolution :premises (@p453 @p252 @p250 @p248 @p246 @p245 @p244 @p379 @p377 @p375 @p374 @p373 @p371 @p369 @p443) :args ((or tptp.p35 tptp.q35 tptp.p26 tptp.q34 tptp.p24 tptp.p20 tptp.q23 tptp.p13) (@list true true true false false false true true false false false true false false) (@list tptp.q44 tptp.q43 tptp.p44 @t84 @t182 tptp.p34 tptp.q33 tptp.p33 @t110 @t187 tptp.p23 tptp.q22 @t113 tptp.p22))) % 0.23/0.43 (step @p549 :rule chain_m_resolution :premises (@p457 @p252 @p250 @p248 @p246 @p245 @p244 @p379 @p399 @p377 @p375 @p374 @p373 @p369 @p397 @p395 @p393 @p385 @p382 @p548) :args ((or tptp.p35 tptp.q35 tptp.p26 tptp.q34 tptp.p24 tptp.q23 tptp.p13 @t112) (@list true true true false false false true true true false false false true true true false true false false) (@list tptp.q44 tptp.q43 tptp.p44 @t84 @t182 tptp.p34 tptp.q33 tptp.q32 tptp.p33 @t110 @t187 tptp.p23 tptp.p22 tptp.q22 @t113 @t174 tptp.p30 @t189 tptp.p20))) % 0.23/0.43 (step @p550 :rule chain_m_resolution :premises (@p456 @p252 @p250 @p248 @p246 @p245 @p244 @p379 @p377 @p375 @p374 @p373 @p371 @p369 @p460 @p409 @p407 @p405 @p404 @p403 @p549 @p387 @p385 @p383 @p382 @p548 @p69 @p391 @p67 @p65 @p64 @p211 @p53 @p51 @p49 @p48 @p47 @p547 @p545 @p463 @p423 @p421 @p419 @p417 @p416 @p415 @p39 @p38 @p36 @p34) :args ((or tptp.p15 tptp.p11 tptp.q15 tptp.p06 tptp.q14 tptp.p04 @t132) (@list true true true false false false true true false false false true false false true true false false false true true true false false false true true true false false false true true false false false true false false true true true false false false true true true false) (@list tptp.q44 tptp.q43 tptp.p44 @t84 @t182 tptp.p34 tptp.q33 tptp.p33 @t110 @t187 tptp.p23 tptp.q22 @t113 tptp.p22 tptp.q31 tptp.p31 @t116 @t188 tptp.p21 tptp.q21 tptp.q20 tptp.p30 @t118 @t189 tptp.p20 tptp.q35 tptp.q34 tptp.p35 @t104 @t186 tptp.p25 tptp.q25 tptp.p26 @t124 @t190 tptp.p16 tptp.q16 @t121 tptp.p17 tptp.q24 tptp.q23 tptp.p24 @t130 @t191 tptp.p14 tptp.p13 tptp.q13 @t133 @t176))) % 0.23/0.43 (step @p551 :rule chain_m_resolution :premises (@p443 @p69 @p391 @p67 @p65 @p64 @p211 @p217 @p213 @p389 @p216) :args ((or tptp.p26 tptp.p22 tptp.p20 tptp.q25 tptp.p15 @t106) @t240 @t253)) % 0.23/0.43 (step @p552 :rule chain_m_resolution :premises (@p494 @p69 @p67 @p65 @p64 @p211 @p215 @p217 @p487 @p379 @p399 @p377 @p375 @p374 @p373 @p551) :args ((or tptp.p26 tptp.p22 tptp.p20 tptp.q25 tptp.p15 tptp.q22 tptp.p13) (@list true true false false false true false false true true true false false false true) (@list tptp.q35 tptp.p35 @t104 @t186 tptp.p25 tptp.q24 @t107 tptp.p24 tptp.q33 tptp.q32 tptp.p33 @t110 @t187 tptp.p23 tptp.q23))) % 0.23/0.43 (step @p553 :rule chain_m_resolution :premises (@p460 @p69 @p391 @p67 @p65 @p64 @p211 @p217 @p213 @p389 @p216) :args ((or tptp.p31 tptp.p30 tptp.p26 tptp.q31 tptp.p22 tptp.q25 tptp.p15 @t106) @t240 @t253)) % 0.23/0.43 (step @p554 :rule chain_m_resolution :premises (@p437 @p69 @p67 @p65 @p64 @p211 @p215 @p217 @p498 @p317 @p315 @p313 @p311 @p310 @p309 @p379 @p399 @p377 @p375 @p374 @p373 @p553 @p409 @p407 @p405 @p404 @p403 @p387 @p385 @p383 @p382 @p552 @p53 @p51 @p49 @p48 @p47 @p547 @p545 @p501) :args ((or tptp.p22 tptp.p15 tptp.q22 tptp.p13 tptp.q21 tptp.p11 tptp.q15 tptp.p06) (@list true true false false false true false false true true true false false false true true true false false false true true true false false false true true false false false true true false false false true false false) (@list tptp.q35 tptp.p35 @t104 @t186 tptp.p25 tptp.q24 @t107 tptp.p24 tptp.q42 tptp.q41 tptp.p42 @t90 @t183 tptp.p32 tptp.q33 tptp.q32 tptp.p33 @t110 @t187 tptp.p23 tptp.q23 tptp.q31 tptp.p31 @t116 @t188 tptp.p21 tptp.q20 tptp.p30 @t118 @t189 tptp.p20 tptp.q25 tptp.p26 @t124 @t190 tptp.p16 tptp.q16 @t121 tptp.p17))) % 0.23/0.43 (step @p555 :rule chain_m_resolution :premises (@p460 @p409 @p407 @p405 @p404 @p403 @p387 @p385 @p383 @p382 @p443 @p69 @p391 @p67 @p65 @p64 @p211 @p53 @p51 @p49 @p48 @p47 @p547 @p545 @p508 @p423 @p419 @p417 @p416 @p415 @p505 @p39 @p554 @p478 @p476 @p474 @p472 @p471 @p470 @p550 @p33 @p32 @p30) :args ((or tptp.p15 tptp.q15 tptp.p06 tptp.q14 tptp.p04 tptp.p02 @t138) (@list true true false false false true true false false false true true true false false false true true false false false true false false true true false false false true false false true true true false false false true true true true) (@list tptp.q31 tptp.p31 @t116 @t188 tptp.p21 tptp.q20 tptp.p30 @t118 @t189 tptp.p20 tptp.q35 tptp.q34 tptp.p35 @t104 @t186 tptp.p25 tptp.q25 tptp.p26 @t124 @t190 tptp.p16 tptp.q16 @t121 tptp.p17 tptp.q24 tptp.p24 @t130 @t191 tptp.p14 tptp.q13 @t133 tptp.p13 tptp.q22 tptp.q21 tptp.p22 @t136 @t192 tptp.p12 tptp.q12 tptp.p11 @t139 tptp.q11))) % 0.23/0.43 (step @p556 :rule chain_m_resolution :premises (@p552 @p369 @p397 @p395 @p393) :args ((or tptp.p26 tptp.p20 tptp.q25 tptp.p15 tptp.p13 @t112) @t228 @t251)) % 0.23/0.43 (step @p557 :rule chain_m_resolution :premises (@p439 @p69 @p67 @p65 @p64 @p211 @p215 @p217 @p486 @p225 @p224 @p222 @p220 @p203 @p357) :args ((or tptp.p40 tptp.q40 tptp.p31 tptp.p26 tptp.q25 tptp.p15 @t86) (@list true true false false false true false false true true true false false true) (@list tptp.q35 tptp.p35 @t104 @t186 tptp.p25 tptp.q24 @t107 tptp.p24 tptp.p33 tptp.q33 @t87 @t172 tptp.q41 tptp.p41))) % 0.23/0.43 (step @p558 :rule chain_m_resolution :premises (@p440 @p69 @p391 @p67 @p65 @p64 @p211 @p217 @p213 @p389 @p216) :args ((or tptp.p40 tptp.q40 tptp.p31 tptp.p26 tptp.q25 tptp.p15 @t106) @t240 @t253)) % 0.23/0.43 (step @p559 :rule chain_m_resolution :premises (@p442 @p69 @p67 @p65 @p64 @p211 @p215 @p217 @p486 @p379 @p377 @p375 @p374 @p373 @p558 @p371 @p369 @p309 @p557 @p193 @p311 @p274 @p198 @p315 @p275 @p203 @p357 @p354 @p195 @p352 @p199 @p205 @p409 @p520 @p407 @p405 @p404 @p403 @p556 @p53 @p51 @p49 @p48 @p47 @p547 @p545 @p526) :args ((or tptp.p20 tptp.p15 tptp.p13 tptp.q20 tptp.p11 tptp.q15 tptp.p06) (@list true true false false false true false false true true false false false true true false false true true true true true true false false true true true false false false true true true false false false true true true false false false true false false) (@list tptp.q35 tptp.p35 @t104 @t186 tptp.p25 tptp.q24 @t107 tptp.p24 tptp.q33 tptp.p33 @t110 @t187 tptp.p23 tptp.q23 tptp.q22 @t113 tptp.p22 tptp.q32 tptp.p42 tptp.p32 tptp.q42 @t67 @t90 @t170 tptp.q41 tptp.p41 tptp.q40 tptp.p40 @t95 @t184 tptp.p30 tptp.q31 tptp.q30 tptp.p31 @t116 @t188 tptp.p21 tptp.q21 tptp.q25 tptp.p26 @t124 @t190 tptp.p16 tptp.q16 @t121 tptp.p17))) % 0.23/0.43 (step @p560 :rule chain_m_resolution :premises (@p440 @p354 @p195 @p352 @p199 @p205 @p520 @p407 @p405 @p404 @p403 @p395 @p369 @p443 @p69 @p391 @p67 @p65 @p64 @p211 @p53 @p51 @p49 @p48 @p47 @p547 @p545 @p530 @p423 @p419 @p417 @p416 @p415 @p505 @p39 @p559) :args ((or tptp.p20 tptp.p15 tptp.q20 tptp.p11 tptp.q15 tptp.p06 tptp.q14 tptp.p04) (@list true true false false false true true false false false true false false true true true false false false true true false false false true false false true true false false false true false false) (@list tptp.q40 tptp.p40 @t95 @t184 tptp.p30 tptp.q30 tptp.p31 @t116 @t188 tptp.p21 tptp.q21 @t113 tptp.p22 tptp.q35 tptp.q34 tptp.p35 @t104 @t186 tptp.p25 tptp.q25 tptp.p26 @t124 @t190 tptp.p16 tptp.q16 @t121 tptp.p17 tptp.q24 tptp.p24 @t130 @t191 tptp.p14 tptp.q13 @t133 tptp.p13))) % 0.23/0.43 (step @p561 :rule chain_m_resolution :premises (@p548 @p69 @p391 @p67 @p65 @p64 @p211 @p53 @p51 @p49 @p48 @p47 @p547 @p545 @p454 @p423 @p421 @p419 @p417 @p416 @p415 @p39 @p38 @p36 @p34) :args ((or tptp.p20 tptp.p15 tptp.q15 tptp.p06 tptp.q14 tptp.p04 @t132) (@list true true true false false false true true false false false true false false true true true false false false true true true false) (@list tptp.q35 tptp.q34 tptp.p35 @t104 @t186 tptp.p25 tptp.q25 tptp.p26 @t124 @t190 tptp.p16 tptp.q16 @t121 tptp.p17 tptp.q24 tptp.q23 tptp.p24 @t130 @t191 tptp.p14 tptp.p13 tptp.q13 @t133 @t176))) % 0.23/0.43 (step @p562 :rule chain_m_resolution :premises (@p552 @p53 @p51 @p49 @p48 @p47 @p547 @p545 @p496) :args ((or tptp.p22 tptp.p20 tptp.p15 tptp.q22 tptp.p13 tptp.q15 tptp.p06) @t239 (@list tptp.q25 tptp.p26 @t124 @t190 tptp.p16 tptp.q16 @t121 tptp.p17))) % 0.23/0.43 (step @p563 :rule chain_m_resolution :premises (@p443 @p69 @p391 @p67 @p65 @p64 @p211 @p53 @p51 @p49 @p48 @p47 @p547 @p545 @p450 @p423 @p419 @p417 @p416 @p415 @p505 @p39 @p562 @p478 @p474 @p472 @p471 @p470 @p561 @p533 @p33 @p560 @p517 @p513 @p512 @p510 @p555) :args ((or tptp.p15 tptp.q15 tptp.p06 tptp.q14 tptp.p04 tptp.p02) (@list true true true false false false true true false false false true false false true true false false false true false false true true false false false true true false false true false true false true) (@list tptp.q35 tptp.q34 tptp.p35 @t104 @t186 tptp.p25 tptp.q25 tptp.p26 @t124 @t190 tptp.p16 tptp.q16 @t121 tptp.p17 tptp.q24 tptp.p24 @t130 @t191 tptp.p14 tptp.q13 @t133 tptp.p13 tptp.q22 tptp.p22 @t136 @t192 tptp.p12 tptp.q12 tptp.q11 @t139 tptp.p11 tptp.q20 @t141 tptp.p20 tptp.p10 tptp.q10))) % 0.23/0.43 (step @p564 :rule cnf_and_pos :args (@t147 0)) % 0.23/0.43 (step @p565 :rule reordering :premises (@p564) :args ((or @t143 @t197))) % 0.23/0.43 (step @p566 :rule chain_m_resolution :premises (@p463 @p423 @p421 @p419 @p417 @p416 @p415 @p39 @p38 @p36 @p34) :args ((or tptp.p17 tptp.p15 tptp.p11 tptp.q14 tptp.p04 @t132) @t240 @t254)) % 0.23/0.43 (step @p567 :rule chain_m_resolution :premises (@p508 @p423 @p419 @p417 @p416 @p415 @p505 @p39 @p501 @p478 @p476 @p474 @p472 @p471 @p470 @p566 @p33 @p32 @p30) :args ((or tptp.p17 tptp.p15 tptp.q14 tptp.p04 tptp.p02 @t138) (@list true true false false false true false false true true true false false false true true true true) (@list tptp.q24 tptp.p24 @t130 @t191 tptp.p14 tptp.q13 @t133 tptp.p13 tptp.q22 tptp.q21 tptp.p22 @t136 @t192 tptp.p12 tptp.q12 tptp.p11 @t139 tptp.q11))) % 0.23/0.43 (step @p568 :rule chain_m_resolution :premises (@p530 @p423 @p419 @p417 @p416 @p415 @p505 @p39 @p526) :args ((or tptp.p20 tptp.p17 tptp.p15 tptp.q20 tptp.p11 tptp.q14 tptp.p04) @t239 (@list tptp.q24 tptp.p24 @t130 @t191 tptp.p14 tptp.q13 @t133 tptp.p13))) % 0.23/0.43 (step @p569 :rule chain_m_resolution :premises (@p454 @p423 @p421 @p419 @p417 @p416 @p415 @p39 @p38 @p36 @p34) :args ((or tptp.p20 tptp.p17 tptp.p15 tptp.q14 tptp.p04 @t132) @t240 @t254)) % 0.23/0.43 (step @p570 :rule chain_m_resolution :premises (@p450 @p423 @p419 @p417 @p416 @p415 @p505 @p39 @p496 @p478 @p474 @p472 @p471 @p470 @p569 @p533 @p33 @p568 @p517 @p513 @p512 @p510 @p567 @p25 @p22 @p565 @p23 @p563 @p544 @p542 @p540 @p539 @p537 @p536 @p18 @p17 @p15 @p13) :args ((or tptp.p02 @t152) (@list true true false false false true false false true true false false false true true false false true false true false true true false true false false true true false true false true true true true false) (@list tptp.q24 tptp.p24 @t130 @t191 tptp.p14 tptp.q13 @t133 tptp.p13 tptp.q22 tptp.p22 @t136 @t192 tptp.p12 tptp.q12 tptp.q11 @t139 tptp.p11 tptp.q20 @t141 tptp.p20 tptp.p10 tptp.q10 tptp.p17 tptp.p07 tptp.q06 @t147 tptp.p06 tptp.q15 tptp.q14 @t150 tptp.p15 tptp.p05 tptp.q05 tptp.p04 tptp.q04 @t153 @t177))) % 0.23/0.43 (step @p571 :rule and_elim :premises (@p7) :args (164)) % 0.23/0.43 (step @p572 :rule and_elim :premises (@p7) :args (2)) % 0.23/0.43 (step @p573 :rule reordering :premises (@p572) :args ((or @t134 @t157))) % 0.23/0.43 (step @p574 :rule and_elim :premises (@p7) :args (110)) % 0.23/0.43 (step @p575 :rule cnf_and_pos :args (@t156 2)) % 0.23/0.43 (step @p576 :rule reordering :premises (@p575) :args ((or @t132 @t255))) % 0.23/0.43 (step @p577 :rule cnf_and_pos :args (@t156 3)) % 0.23/0.43 (step @p578 :rule reordering :premises (@p577) :args ((or @t129 @t255))) % 0.23/0.43 (step @p579 :rule chain_m_resolution :premises (@p503 @p478 @p476 @p474 @p472 @p471 @p33 @p470 @p32 @p30) :args ((or tptp.p17 tptp.p13 tptp.q16 tptp.p06 tptp.q12 tptp.p02 @t138) @t256 @t257)) % 0.23/0.43 (step @p580 :rule chain_m_resolution :premises (@p534 @p478 @p474 @p472 @p471 @p470 @p533 @p33 @p528 @p517 @p513 @p512 @p510 @p579 @p28 @p26 @p25 @p23 @p22 @p21 @p19) :args ((or tptp.p13 tptp.q12 tptp.p02 @t146) (@list true true false false false true false false true false true false true true false true true false true true) (@list tptp.q22 tptp.p22 @t136 @t192 tptp.p12 tptp.q11 @t139 tptp.p11 tptp.q20 @t141 tptp.p20 tptp.p10 tptp.q10 tptp.q16 @t144 tptp.p17 tptp.p06 tptp.p07 @t147 tptp.q06))) % 0.23/0.43 (step @p581 :rule chain_m_resolution :premises (@p554 @p45 @p44 @p42 @p40) :args ((or tptp.p22 tptp.q22 tptp.p13 tptp.q21 tptp.p11 tptp.p06 @t126) @t228 @t258)) % 0.23/0.43 (step @p582 :rule chain_m_resolution :premises (@p483 @p482 @p236 @p325 @p323 @p237 @p321 @p239 @p317 @p315 @p313 @p311 @p310 @p206 @p309 @p208 @p219) :args ((or tptp.p44 tptp.q44 tptp.p35 tptp.q43 tptp.p33 tptp.q32 tptp.p22 @t92) (@list false true true true false false false true true true false false true false true true) (@list tptp.q63 tptp.q53 tptp.q52 tptp.p53 @t64 @t179 tptp.p43 tptp.q42 tptp.q41 tptp.p42 @t90 @t183 tptp.p31 tptp.p32 @t93 tptp.q31))) % 0.23/0.43 (step @p583 :rule chain_m_resolution :premises (@p483 @p481 @p236 @p325 @p323 @p237 @p321 @p239 @p193 @p274 @p198 @p275) :args ((or tptp.p44 tptp.p40 tptp.q44 tptp.p35 tptp.q43 tptp.p33 @t66) (@list false true true true false false false true true true false) (@list tptp.q63 tptp.q53 tptp.q52 tptp.p53 @t64 @t179 tptp.p43 tptp.p42 tptp.q42 @t67 @t170))) % 0.23/0.43 (step @p584 :rule chain_m_resolution :premises (@p483 @p481 @p236 @p325 @p323 @p237 @p321 @p239 @p317 @p313 @p311 @p310 @p309 @p363 @p206 @p203 @p583 @p357 @p354 @p195 @p352 @p199 @p205 @p582 @p252 @p250 @p248 @p246 @p245 @p244 @p391 @p67 @p65 @p64 @p211 @p426 @p427 @p487) :args ((or tptp.p33 tptp.q33 tptp.p24 tptp.q32 tptp.p22 tptp.p20 tptp.q24 tptp.p15) (@list false true true true false false false true true false false false true false false true true true true false false false true true true true false false false true true false false false true false false) (@list tptp.q63 tptp.q53 tptp.q52 tptp.p53 @t64 @t179 tptp.p43 tptp.q42 tptp.p42 @t90 @t183 tptp.p32 tptp.q31 @t93 tptp.p31 tptp.q41 tptp.p41 tptp.q40 tptp.p40 @t95 @t184 tptp.p30 tptp.q30 tptp.q44 tptp.q43 tptp.p44 @t84 @t182 tptp.p34 tptp.q34 tptp.p35 @t104 @t186 tptp.p25 tptp.q25 @t101 tptp.p26))) % 0.23/0.43 (step @p585 :rule chain_m_resolution :premises (@p483 @p482 @p236 @p325 @p323 @p237 @p321 @p239 @p252 @p250 @p248 @p246 @p245 @p244 @p391 @p67 @p65 @p64 @p211 @p426 @p427 @p498 @p317 @p315 @p313 @p311 @p310 @p309 @p409 @p407 @p405 @p404 @p403 @p387 @p385 @p383 @p382 @p584) :args ((or tptp.p33 tptp.q33 tptp.p24 tptp.q32 tptp.p22 tptp.q24 tptp.p15 tptp.q21 tptp.p11) (@list false true true true false false false true true true false false false true true false false false true false false true true true false false false true true false false false true true false false false) (@list tptp.q63 tptp.q53 tptp.q52 tptp.p53 @t64 @t179 tptp.p43 tptp.q44 tptp.q43 tptp.p44 @t84 @t182 tptp.p34 tptp.q34 tptp.p35 @t104 @t186 tptp.p25 tptp.q25 @t101 tptp.p26 tptp.q42 tptp.q41 tptp.p42 @t90 @t183 tptp.p32 tptp.q31 tptp.p31 @t116 @t188 tptp.p21 tptp.q20 tptp.p30 @t118 @t189 tptp.p20))) % 0.23/0.43 (step @p586 :rule chain_m_resolution :premises (@p499 @p317 @p315 @p313 @p311 @p310 @p309 @p409 @p407 @p405 @p404 @p403 @p387 @p385 @p383 @p382 @p490) :args ((or tptp.p33 tptp.q33 tptp.p24 tptp.q32 tptp.p22 tptp.p17 tptp.q21 tptp.p11) (@list true true true false false false true true false false false true true false false false) (@list tptp.q42 tptp.q41 tptp.p42 @t90 @t183 tptp.p32 tptp.q31 tptp.p31 @t116 @t188 tptp.p21 tptp.q20 tptp.p30 @t118 @t189 tptp.p20))) % 0.23/0.43 (step @p587 :rule chain_m_resolution :premises (@p498 @p317 @p315 @p313 @p311 @p310 @p309 @p409 @p407 @p405 @p404 @p403 @p387 @p385 @p383 @p382 @p487 @p51 @p48 @p47 @p547 @p545 @p586 @p465 @p45 @p585 @p379 @p399 @p377 @p375 @p374 @p373 @p423 @p421 @p419 @p417 @p416 @p415 @p581 @p478 @p476 @p474 @p472 @p471 @p33 @p470 @p32 @p30) :args ((or tptp.p13 tptp.p06 tptp.q13 tptp.p04 tptp.q12 tptp.p02 @t138) (@list true true true false false false true true false false false true true false false false true false false true false false true false false true true true false false false true true true false false false true true true true false false true false true true) (@list tptp.q42 tptp.q41 tptp.p42 @t90 @t183 tptp.p32 tptp.q31 tptp.p31 @t116 @t188 tptp.p21 tptp.q20 tptp.p30 @t118 @t189 tptp.p20 tptp.p26 @t190 tptp.p16 tptp.q16 @t121 tptp.p17 tptp.q15 @t127 tptp.p15 tptp.q33 tptp.q32 tptp.p33 @t110 @t187 tptp.p23 tptp.q24 tptp.q23 tptp.p24 @t130 @t191 tptp.p14 tptp.q14 tptp.q22 tptp.q21 tptp.p22 @t136 @t192 tptp.p11 tptp.p12 @t139 tptp.q11))) % 0.23/0.43 (step @p588 :rule chain_m_resolution :premises (@p559 @p45 @p44 @p42 @p40) :args ((or tptp.p20 tptp.p13 tptp.q20 tptp.p11 tptp.p06 @t126) @t228 @t258)) % 0.23/0.43 (step @p589 :rule chain_m_resolution :premises (@p584 @p379 @p399 @p377 @p375 @p374 @p373 @p369 @p397 @p395 @p393) :args ((or tptp.p24 tptp.p20 tptp.q24 tptp.p15 tptp.q23 tptp.p13 @t112) @t240 @t259)) % 0.23/0.43 (step @p590 :rule chain_m_resolution :premises (@p583 @p252 @p250 @p248 @p246 @p245 @p244 @p391 @p67 @p65 @p64 @p211 @p426 @p427 @p486 @p225 @p224 @p222 @p220) :args ((or tptp.p40 tptp.p24 tptp.q24 tptp.p15 @t66 @t86) (@list true true true false false false true true false false false true false false true true true false) (@list tptp.q44 tptp.q43 tptp.p44 @t84 @t182 tptp.p34 tptp.q34 tptp.p35 @t104 @t186 tptp.p25 tptp.q25 @t101 tptp.p26 tptp.p33 tptp.q33 @t87 @t172))) % 0.23/0.43 (step @p591 :rule chain_m_resolution :premises (@p583 @p252 @p250 @p248 @p246 @p245 @p244 @p391 @p67 @p65 @p64 @p211 @p426 @p427 @p486 @p379 @p377 @p375 @p374 @p373 @p371 @p369 @p309 @p590 @p311 @p315 @p203 @p357 @p354 @p195 @p352 @p199 @p205 @p409 @p520 @p407 @p405 @p404 @p403 @p589) :args ((or tptp.p24 tptp.p20 tptp.q24 tptp.p15 tptp.q23 tptp.p13 tptp.q20 tptp.p11) (@list true true true false false false true true false false false true false false true true false false false true false false true true true false true true true false false false true true true false false false true) (@list tptp.q44 tptp.q43 tptp.p44 @t84 @t182 tptp.p34 tptp.q34 tptp.p35 @t104 @t186 tptp.p25 tptp.q25 @t101 tptp.p26 tptp.q33 tptp.p33 @t110 @t187 tptp.p23 tptp.q22 @t113 tptp.p22 tptp.q32 tptp.p32 @t90 tptp.q41 tptp.p41 tptp.q40 tptp.p40 @t95 @t184 tptp.p30 tptp.q31 tptp.q30 tptp.p31 @t116 @t188 tptp.p21 tptp.q21))) % 0.23/0.43 (step @p592 :rule chain_m_resolution :premises (@p490 @p379 @p399 @p377 @p375 @p374 @p373 @p369 @p397 @p395 @p393) :args ((or tptp.p24 tptp.p20 tptp.p17 tptp.q23 tptp.p13 @t112) @t240 @t259)) % 0.23/0.43 (step @p593 :rule chain_m_resolution :premises (@p521 @p225 @p224 @p222 @p220) :args ((or tptp.p40 tptp.q40 tptp.p31 tptp.p24 tptp.p17 @t86) @t228 @t260)) % 0.23/0.43 (step @p594 :rule chain_m_resolution :premises (@p521 @p379 @p377 @p375 @p374 @p373 @p371 @p369 @p309 @p593 @p311 @p315 @p203 @p357 @p354 @p195 @p352 @p199 @p205 @p409 @p520 @p407 @p405 @p404 @p403 @p592) :args ((or tptp.p24 tptp.p20 tptp.p17 tptp.q23 tptp.p13 tptp.q20 tptp.p11) (@list true true false false false true false false true true true false true true true false false false true true true false false false true) (@list tptp.q33 tptp.p33 @t110 @t187 tptp.p23 tptp.q22 @t113 tptp.p22 tptp.q32 tptp.p32 @t90 tptp.q41 tptp.p41 tptp.q40 tptp.p40 @t95 @t184 tptp.p30 tptp.q31 tptp.q30 tptp.p31 @t116 @t188 tptp.p21 tptp.q21))) % 0.23/0.43 (step @p595 :rule chain_m_resolution :premises (@p487 @p379 @p399 @p377 @p375 @p374 @p373 @p369 @p397 @p395 @p393) :args ((or tptp.p26 tptp.p24 tptp.p20 tptp.q23 tptp.p13 @t112) @t240 @t259)) % 0.23/0.43 (step @p596 :rule chain_m_resolution :premises (@p486 @p225 @p224 @p222 @p220) :args ((or tptp.p40 tptp.p26 tptp.p24 @t66 @t86) @t228 @t260)) % 0.23/0.43 (step @p597 :rule chain_m_resolution :premises (@p486 @p379 @p377 @p375 @p374 @p373 @p371 @p369 @p309 @p596 @p311 @p315 @p203 @p357 @p354 @p195 @p352 @p199 @p205 @p409 @p520 @p407 @p405 @p404 @p403 @p595 @p51 @p48 @p47 @p547 @p545 @p594 @p465 @p45 @p591 @p423 @p421 @p419 @p417 @p416 @p415 @p588) :args ((or tptp.p20 tptp.p13 tptp.q20 tptp.p11 tptp.p06 tptp.q13 tptp.p04) (@list true true false false false true false false true true true false true true true false false false true true true false false false true true false false true false false true false false true true true false false false true) (@list tptp.q33 tptp.p33 @t110 @t187 tptp.p23 tptp.q22 @t113 tptp.p22 tptp.q32 tptp.p32 @t90 tptp.q41 tptp.p41 tptp.q40 tptp.p40 @t95 @t184 tptp.p30 tptp.q31 tptp.q30 tptp.p31 @t116 @t188 tptp.p21 tptp.q21 tptp.p26 @t190 tptp.p16 tptp.q16 @t121 tptp.p17 tptp.q15 @t127 tptp.p15 tptp.q24 tptp.q23 tptp.p24 @t130 @t191 tptp.p14 tptp.q14))) % 0.23/0.43 (step @p598 :rule chain_m_resolution :premises (@p562 @p45 @p44 @p42 @p40) :args ((or tptp.p22 tptp.p20 tptp.q22 tptp.p13 tptp.p06 @t126) @t228 @t258)) % 0.23/0.43 (step @p599 :rule chain_m_resolution :premises (@p47 @p48 @p465 @p547 @p51 @p45 @p545 @p487 @p584 @p490 @p379 @p399 @p377 @p375 @p374 @p373 @p423 @p421 @p419 @p417 @p416 @p415 @p598 @p478 @p474 @p472 @p471 @p470 @p533 @p33 @p597 @p517 @p513 @p512 @p510 @p587) :args ((or tptp.p13 tptp.p06 tptp.q13 tptp.p04 tptp.q12 tptp.p02) (@list true true true true false false false false false true true true false false false true true true false false false true true true false false false true false false true false true false true) (@list tptp.p16 tptp.q15 tptp.q16 @t190 @t127 @t121 tptp.p26 tptp.p15 tptp.p17 tptp.q33 tptp.q32 tptp.p33 @t110 @t187 tptp.p23 tptp.q24 tptp.q23 tptp.p24 @t130 @t191 tptp.p14 tptp.q14 tptp.q22 tptp.p22 @t136 @t192 tptp.p12 tptp.q11 @t139 tptp.p11 tptp.q20 @t141 tptp.p20 tptp.p10 tptp.q10))) % 0.23/0.43 (step @p600 :rule chain_m_resolution :premises (@p586 @p379 @p399 @p377 @p375 @p374 @p373 @p421 @p419 @p417 @p416 @p415 @p42 @p45 @p501 @p478 @p476 @p474 @p472 @p471 @p33 @p470 @p32 @p30 @p25 @p22 @p565 @p23 @p599) :args ((or tptp.p13 tptp.q13 tptp.p04 tptp.q12 tptp.p02 @t138) (@list true true true false false false true true false false false true false false true true true false false true false true true true false true false false) (@list tptp.q33 tptp.q32 tptp.p33 @t110 @t187 tptp.p23 tptp.q23 tptp.p24 @t130 @t191 tptp.p14 tptp.q14 @t127 tptp.p15 tptp.q22 tptp.q21 tptp.p22 @t136 @t192 tptp.p11 tptp.p12 @t139 tptp.q11 tptp.p17 tptp.p07 tptp.q06 @t147 tptp.p06))) % 0.23/0.43 (step @p601 :rule chain_m_resolution :premises (@p594 @p421 @p419 @p417 @p416 @p415 @p42 @p45 @p526) :args ((or tptp.p20 tptp.p17 tptp.p13 tptp.q20 tptp.p11 tptp.q13 tptp.p04) @t239 (@list tptp.q23 tptp.p24 @t130 @t191 tptp.p14 tptp.q14 @t127 tptp.p15))) % 0.23/0.43 (step @p602 :rule chain_m_resolution :premises (@p490 @p379 @p399 @p377 @p375 @p374 @p373 @p421 @p419 @p417 @p416 @p415 @p42 @p45 @p496 @p478 @p474 @p472 @p471 @p470 @p533 @p33 @p601 @p517 @p513 @p512 @p510 @p600 @p25 @p22 @p565 @p23 @p599) :args ((or tptp.p13 tptp.q13 tptp.p04 tptp.q12 tptp.p02) (@list true true true false false false true true false false false true false false true true false false false true false false true false true false true true false true false false) (@list tptp.q33 tptp.q32 tptp.p33 @t110 @t187 tptp.p23 tptp.q23 tptp.p24 @t130 @t191 tptp.p14 tptp.q14 @t127 tptp.p15 tptp.q22 tptp.p22 @t136 @t192 tptp.p12 tptp.q11 @t139 tptp.p11 tptp.q20 @t141 tptp.p20 tptp.p10 tptp.q10 tptp.p17 tptp.p07 tptp.q06 @t147 tptp.p06))) % 0.23/0.43 (step @p603 :rule cnf_and_pos :args (@t153 0)) % 0.23/0.43 (step @p604 :rule reordering :premises (@p603) :args ((or @t149 @t196))) % 0.23/0.43 (step @p605 :rule chain_m_resolution :premises (@p554 @p478 @p476 @p474 @p472 @p471 @p33 @p470 @p32 @p30) :args ((or tptp.p15 tptp.p13 tptp.q15 tptp.p06 tptp.q12 tptp.p02 @t138) @t256 @t257)) % 0.23/0.43 (step @p606 :rule chain_m_resolution :premises (@p562 @p478 @p474 @p472 @p471 @p470 @p533 @p33 @p559 @p517 @p513 @p512 @p510 @p605) :args ((or tptp.p15 tptp.p13 tptp.q15 tptp.p06 tptp.q12 tptp.p02) (@list true true false false false true false false true false true false true) (@list tptp.q22 tptp.p22 @t136 @t192 tptp.p12 tptp.q11 @t139 tptp.p11 tptp.q20 @t141 tptp.p20 tptp.p10 tptp.q10))) % 0.23/0.43 (step @p607 :rule chain_m_resolution :premises (@p501 @p478 @p476 @p474 @p472 @p471 @p33 @p470 @p32 @p30) :args ((or tptp.p17 tptp.p15 tptp.p13 tptp.q12 tptp.p02 @t138) @t256 @t257)) % 0.23/0.43 (step @p608 :rule chain_m_resolution :premises (@p496 @p478 @p474 @p472 @p471 @p470 @p533 @p33 @p526 @p517 @p513 @p512 @p510 @p607 @p25 @p22 @p565 @p23 @p606 @p544 @p540 @p539 @p537 @p604 @p18 @p602 @p580 @p578 @p576 @p574 @p573 @p571 @p570 @p12 @p11 @p9) :args (@t158 (@list true true false false false true false false true false true false true true false true false false true false true false true false false true true true false true false true true true true) (@list tptp.q22 tptp.p22 @t136 @t192 tptp.p12 tptp.q11 @t139 tptp.p11 tptp.q20 @t141 tptp.p20 tptp.p10 tptp.q10 tptp.p17 tptp.p07 tptp.q06 @t147 tptp.p06 tptp.q15 @t150 tptp.p15 tptp.p05 tptp.q04 @t153 tptp.p04 tptp.q05 tptp.q13 tptp.q12 @t156 tptp.p13 tptp.p03 tptp.q03 tptp.p02 @t159 tptp.q02))) % 0.23/0.43 (step @p609 :rule and_elim :premises (@p7) :args (162)) % 0.23/0.43 (step @p610 :rule chain_m_resolution :premises (@p609 @p608) :args (tptp.p01 @t237 (@list tptp.q01))) % 0.23/0.43 (step @p611 :rule and_elim :premises (@p7) :args (0)) % 0.23/0.43 (step @p612 :rule reordering :premises (@p611) :args ((or @t140 @t162))) % 0.23/0.43 (step @p613 :rule chain_m_resolution :premises (@p612 @p610) :args (@t140 @t261 @t262)) % 0.23/0.43 (step @p614 :rule and_elim :premises (@p7) :args (108)) % 0.23/0.43 (step @p615 :rule chain_m_resolution :premises (@p614 @p610) :args (@t161 @t261 @t262)) % 0.23/0.43 (step @p616 :rule cnf_and_pos :args (@t161 1)) % 0.23/0.43 (step @p617 :rule reordering :premises (@p616) :args ((or @t138 @t263))) % 0.23/0.43 (step @p618 :rule chain_m_resolution :premises (@p617 @p615) :args (@t138 @t261 @t264)) % 0.23/0.43 (step @p619 :rule chain_m_resolution :premises (@p510 @p618) :args (tptp.p10 @t237 (@list tptp.q10))) % 0.23/0.43 (step @p620 :rule chain_m_resolution :premises (@p513 @p619) :args (@t141 @t261 @t265)) % 0.23/0.43 (step @p621 :rule chain_m_resolution :premises (@p517 @p620) :args (@t115 @t261 (@list @t141))) % 0.23/0.43 (step @p622 :rule chain_m_resolution :premises (@p512 @p619) :args (@t119 @t261 @t265)) % 0.23/0.43 (step @p623 :rule chain_m_resolution :premises (@p597 @p613 @p622 @p621 @p39 @p38 @p36 @p34) :args ((or tptp.p06 tptp.p04 @t132) @t266 @t267)) % 0.23/0.43 (step @p624 :rule cnf_and_pos :args (@t161 2)) % 0.23/0.43 (step @p625 :rule reordering :premises (@p624) :args ((or @t135 @t263))) % 0.23/0.43 (step @p626 :rule chain_m_resolution :premises (@p625 @p615) :args (@t135 @t261 @t264)) % 0.23/0.43 (step @p627 :rule chain_m_resolution :premises (@p47 @p547 @p465 @p48 @p545 @p45 @p51 @p593 @p590 @p486 @p217 @p213 @p389 @p216 @p224 @p220 @p225 @p222 @p203 @p357) :args ((or tptp.p40 tptp.q40 tptp.p31 tptp.p06 @t86 @t106) (@list true true true false false true false false false true true true false true false true true false true) (@list tptp.q16 tptp.q15 tptp.p16 @t121 @t127 @t190 tptp.p17 tptp.p15 tptp.p26 tptp.p24 tptp.q24 @t107 @t173 tptp.q33 @t172 tptp.p33 @t87 tptp.q41 tptp.p41))) % 0.23/0.43 (step @p628 :rule chain_m_resolution :premises (@p557 @p53 @p51 @p49 @p48 @p47 @p547 @p545 @p523 @p45 @p44 @p42 @p40) :args ((or tptp.p40 tptp.q40 tptp.p31 tptp.p06 @t86 @t126) (@list true true false false false true false false true true true false) (@list tptp.q25 tptp.p26 @t124 @t190 tptp.p16 tptp.q16 @t121 tptp.p17 tptp.p15 tptp.q15 @t127 @t175))) % 0.23/0.43 (step @p629 :rule chain_m_resolution :premises (@p47 @p465 @p547 @p48 @p45 @p545 @p51 @p590 @p593 @p486 @p423 @p419 @p417 @p416 @p415 @p628 @p505 @p39 @p373 @p627 @p225 @p375 @p224 @p222 @p399 @p220 @p309 @p311 @p315 @p203 @p357 @p354 @p195 @p352 @p199 @p205 @p622 @p409 @p520 @p407 @p405 @p404 @p403 @p613 @p621 @p478 @p476 @p474 @p472 @p471 @p470 @p626 @p623) :args ((or tptp.p06 tptp.p04 tptp.p02) (@list true true true false false true false false false true true false false false true true false false true true true true true true false false true true false true true true false false false true true true true false false false true true true true true false false false true true) (@list tptp.q15 tptp.q16 tptp.p16 @t127 @t121 @t190 tptp.p15 tptp.p17 tptp.p26 tptp.q24 tptp.p24 @t130 @t191 tptp.p14 tptp.q14 tptp.q13 @t133 tptp.p13 tptp.q23 tptp.p33 tptp.p23 tptp.q33 @t87 @t110 @t172 tptp.q32 tptp.p32 @t90 tptp.q41 tptp.p41 tptp.q40 tptp.p40 @t95 @t184 tptp.p30 tptp.p20 tptp.q31 tptp.q30 tptp.p31 @t116 @t188 tptp.p21 tptp.p11 tptp.q20 tptp.q22 tptp.q21 tptp.p22 @t136 @t192 tptp.p12 tptp.q11 tptp.q12))) % 0.23/0.43 (step @p630 :rule chain_m_resolution :premises (@p601 @p613 @p622 @p621 @p39 @p38 @p36 @p34) :args ((or tptp.p17 tptp.p04 @t132) @t266 @t267)) % 0.23/0.43 (step @p631 :rule chain_m_resolution :premises (@p505 @p39 @p415 @p373 @p42 @p389 @p416 @p45 @p217 @p419 @p375 @p523 @p593 @p399 @p309 @p311 @p315 @p203 @p357 @p354 @p195 @p352 @p199 @p205 @p622 @p409 @p520 @p407 @p405 @p404 @p403 @p613 @p621 @p478 @p476 @p474 @p472 @p471 @p470 @p626 @p630 @p25 @p22 @p565 @p23 @p629) :args ((or tptp.p04 tptp.p02) (@list false false false true true true false false true true false false true false true true false true true true false false false true true true true false false false true true true true true false false false true true true false true false false) (@list @t133 tptp.q13 tptp.p13 tptp.q14 tptp.q23 tptp.p14 @t127 @t107 @t191 tptp.p23 tptp.p15 tptp.p24 @t110 tptp.q32 tptp.p32 @t90 tptp.q41 tptp.p41 tptp.q40 tptp.p40 @t95 @t184 tptp.p30 tptp.p20 tptp.q31 tptp.q30 tptp.p31 @t116 @t188 tptp.p21 tptp.p11 tptp.q20 tptp.q22 tptp.q21 tptp.p22 @t136 @t192 tptp.p12 tptp.q11 tptp.q12 tptp.p17 tptp.p07 tptp.q06 @t147 tptp.p06))) % 0.23/0.43 (step @p632 :rule chain_m_resolution :premises (@p367 @p63 @p61 @p59 @p58 @p57 @p55 @p51 @p49 @p48 @p47 @p465 @p45 @p225 @p523 @p222 @p309 @p193 @p311 @p274 @p198 @p315 @p275 @p203 @p357 @p354 @p195 @p352 @p199 @p205 @p622 @p409 @p520 @p407 @p405 @p404 @p403 @p613 @p621 @p476 @p474 @p472 @p471 @p470 @p626 @p36 @p39 @p528 @p613 @p621 @p622 @p28 @p26 @p25 @p23 @p22 @p21 @p19) :args ((or tptp.p02 @t146) (@list true true false false false true true false false false true false true false true false true true true true true false false true true true false false false true true true true false false false true true true true false false false true true false false true true true true false true true false true true) (@list tptp.q36 tptp.p37 @t98 @t185 tptp.p27 tptp.q26 tptp.p26 @t124 @t190 tptp.p16 tptp.q15 @t127 tptp.p33 tptp.p15 @t87 tptp.q32 tptp.p42 tptp.p32 tptp.q42 @t67 @t90 @t170 tptp.q41 tptp.p41 tptp.q40 tptp.p40 @t95 @t184 tptp.p30 tptp.p20 tptp.q31 tptp.q30 tptp.p31 @t116 @t188 tptp.p21 tptp.p11 tptp.q20 tptp.q21 tptp.p22 @t136 @t192 tptp.p12 tptp.q11 tptp.q12 @t133 tptp.p13 tptp.p11 tptp.q20 tptp.p20 tptp.q16 @t144 tptp.p17 tptp.p06 tptp.p07 @t147 tptp.q06))) % 0.23/0.43 (step @p633 :rule chain_m_resolution :premises (@p557 @p53 @p51 @p49 @p48 @p47 @p547 @p545 @p523 @p309 @p311 @p315 @p203 @p357 @p354 @p195 @p352 @p199 @p205 @p622 @p409 @p520 @p407 @p405 @p404 @p403 @p613 @p621 @p476 @p474 @p472 @p471 @p470 @p626 @p36 @p39 @p559 @p613 @p622 @p621 @p544 @p540 @p539 @p537 @p604 @p18 @p631 @p632) :args ((or tptp.p06 tptp.p02) (@list true true false false false true false false false true true false true true true false false false true true true true false false false true true true true false false false true true false false true true true true false true false true false false true) (@list tptp.q25 tptp.p26 @t124 @t190 tptp.p16 tptp.q16 @t121 tptp.p17 tptp.q32 tptp.p32 @t90 tptp.q41 tptp.p41 tptp.q40 tptp.p40 @t95 @t184 tptp.p30 tptp.p20 tptp.q31 tptp.q30 tptp.p31 @t116 @t188 tptp.p21 tptp.p11 tptp.q20 tptp.q21 tptp.p22 @t136 @t192 tptp.p12 tptp.q11 tptp.q12 @t133 tptp.p13 tptp.p11 tptp.p20 tptp.q20 tptp.q15 @t150 tptp.p15 tptp.p05 tptp.q04 @t153 tptp.p04 tptp.q05))) % 0.23/0.43 (step @p634 :rule chain_m_resolution :premises (@p311 @p315 @p309 @p203 @p523 @p357 @p354 @p195 @p352 @p199 @p205 @p622 @p409 @p520 @p407 @p405 @p404 @p403 @p613 @p621 @p476 @p474 @p472 @p471 @p470 @p626 @p36 @p39 @p526 @p613 @p621 @p622 @p25 @p22 @p565 @p23 @p633 @p539 @p537 @p632 @p604 @p18 @p631) :args (tptp.p02 (@list true false false true true true true false false false true true true true false false false true true true true false false false true true false false true true true true false true false false true false true true false false) (@list @t90 tptp.p32 tptp.q41 tptp.q32 tptp.p41 tptp.q40 tptp.p40 @t95 @t184 tptp.p30 tptp.p20 tptp.q31 tptp.q30 tptp.p31 @t116 @t188 tptp.p21 tptp.p11 tptp.q20 tptp.q21 tptp.p22 @t136 @t192 tptp.p12 tptp.q11 tptp.q12 @t133 tptp.p13 tptp.p11 tptp.q20 tptp.p20 tptp.p17 tptp.p07 tptp.q06 @t147 tptp.p06 tptp.p15 tptp.p05 tptp.q05 tptp.q04 @t153 tptp.p04))) % 0.23/0.43 (step @p635 :rule chain_m_resolution :premises (@p12 @p634) :args (@t159 @t261 (@list tptp.p02))) % 0.23/0.43 (step @p636 :rule cnf_and_pos :args (@t159 0)) % 0.23/0.43 (step @p637 :rule reordering :premises (@p636) :args ((or @t155 @t195))) % 0.23/0.43 (step @p638 :rule chain_m_resolution :premises (@p637 @p635) :args (@t155 @t261 (@list @t159))) % 0.23/0.43 (step @p639 :rule chain_m_resolution :premises (@p28 @p531 @p613 @p622 @p621 @p26 @p25 @p23 @p22 @p21 @p19) :args ((or tptp.p04 @t146) (@list false true true true false true true false true true) (@list tptp.q16 tptp.p11 tptp.p20 tptp.q20 @t144 tptp.p17 tptp.p06 tptp.p07 @t147 tptp.q06))) % 0.23/0.43 (step @p640 :rule chain_m_resolution :premises (@p565 @p22 @p23 @p25 @p560 @p621 @p613 @p622 @p568 @p613 @p621 @p622 @p544 @p542 @p540 @p539 @p537 @p639 @p18 @p17 @p15 @p13) :args (@t152 (@list false false true false true true true false true true true true true false true false true true true true false) (@list tptp.q06 @t147 tptp.p07 tptp.p06 tptp.q20 tptp.p11 tptp.p20 tptp.p17 tptp.p11 tptp.q20 tptp.p20 tptp.q15 tptp.q14 @t150 tptp.p15 tptp.p05 tptp.q05 tptp.p04 tptp.q04 @t153 @t177))) % 0.23/0.43 (step @p641 :rule chain_m_resolution :premises (@p571 @p640 @p638) :args (tptp.p03 @t268 (@list tptp.q03 tptp.q02))) % 0.23/0.43 (step @p642 :rule chain_m_resolution :premises (@p573 @p641) :args (@t134 @t261 @t269)) % 0.23/0.43 (step @p643 :rule chain_m_resolution :premises (@p574 @p641) :args (@t156 @t261 @t269)) % 0.23/0.43 (step @p644 :rule chain_m_resolution :premises (@p578 @p643) :args (@t129 @t261 (@list @t156))) % 0.23/0.43 (step @p645 :rule chain_m_resolution :premises (@p22 @p565 @p25 @p23 @p601 @p613 @p642 @p622 @p644 @p621 @p597 @p613 @p642 @p622 @p644 @p621) :args (tptp.p04 (@list true true false false true true true true true false true true true true true) (@list tptp.q06 tptp.p07 @t147 tptp.p17 tptp.p11 tptp.p13 tptp.p20 tptp.q13 tptp.q20 tptp.p06 tptp.p11 tptp.p13 tptp.p20 tptp.q13 tptp.q20))) % 0.23/0.43 (step @p646 :rule chain_m_resolution :premises (@p18 @p645) :args (@t153 @t261 (@list tptp.p04))) % 0.23/0.43 (step @p647 :rule chain_m_resolution :premises (@p604 @p646) :args (@t149 @t261 (@list @t153))) % 0.23/0.43 (step @p648 :rule chain_m_resolution :premises (@p28 @p528 @p613 @p621 @p642 @p622 @p26 @p25 @p23 @p22 @p21 @p19) :args (@t146 (@list false true true true true false true true false true true) (@list tptp.q16 tptp.p11 tptp.q20 tptp.p13 tptp.p20 @t144 tptp.p17 tptp.p06 tptp.p07 @t147 tptp.q06))) % 0.23/0.43 (step @p649 :rule chain_m_resolution :premises (@p537 @p648 @p647) :args (tptp.p05 @t268 (@list tptp.q05 tptp.q04))) % 0.23/0.43 (step @p650 :rule chain_m_resolution :premises (@p539 @p649) :args (@t128 @t261 @t270)) % 0.23/0.43 (step @p651 :rule chain_m_resolution :premises (@p526 @p622 @p650 @p642 @p621 @p613) :args (tptp.p17 (@list true true true true true) (@list tptp.p20 tptp.p15 tptp.p13 tptp.q20 tptp.p11))) % 0.23/0.43 (step @p652 :rule chain_m_resolution :premises (@p25 @p651) :args (@t145 @t261 (@list tptp.p17))) % 0.23/0.43 (step @p653 :rule chain_m_resolution :premises (@p22 @p652) :args (tptp.q06 @t237 (@list tptp.p07))) % 0.23/0.43 (step @p654 :rule chain_m_resolution :premises (@p540 @p649) :args (@t150 @t261 @t270)) % 0.23/0.43 (step @p655 :rule chain_m_resolution :premises (@p544 @p654) :args (@t123 @t261 (@list @t150))) % 0.23/0.43 (step @p656 :rule chain_m_resolution :premises (@p559 @p622 @p650 @p642 @p621 @p613 @p655) :args (tptp.p06 (@list true true true true true true) (@list tptp.p20 tptp.p15 tptp.p13 tptp.q20 tptp.p11 tptp.q15))) % 0.23/0.43 (step @p657 :rule chain_m_resolution :premises (@p23 @p656) :args (@t147 @t261 (@list tptp.p06))) % 0.23/0.43 (step @p658 false :rule chain_m_resolution :premises (@p565 @p657 @p653) :args (false (@list false false) (@list @t147 tptp.q06))) % 0.23/0.43 ) % 0.23/0.43 % SZS output end Proof % 0.23/0.43 % cvc5 exiting %------------------------------------------------------------------------------