%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : PUZ017-1 : TPTP v9.2.1. Released v1.0.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n027.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jun 3 08:43:57 AM UTC 2026 % Result : Unsatisfiable 0.38s 0.98s % Output : Proof 0.38s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : PUZ017-1 : TPTP v9.2.1. Released v1.0.0. % 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.18/0.35 % Computer : n027.cluster.edu % 0.18/0.35 % Model : x86_64 x86_64 % 0.18/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.18/0.35 % Memory : 8042.1875MB % 0.18/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.18/0.35 % CPULimit : 300 % 0.18/0.35 % WCLimit : 300 % 0.18/0.35 % DateTime : Tue Jun 2 13:12:36 EDT 2026 % 0.18/0.35 % CPUTime : % 0.27/0.52 %----Proving TF0_NAR, FOF, or CNF % 0.27/0.53 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 0.38/0.98 % SZS status Unsatisfiable % 0.38/0.98 % SZS output start Proof % 0.38/1.00 ( % 0.38/1.00 (declare-sort $$unsorted 0) % 0.38/1.00 (declare-const tptp.hasdrink (-> $$unsorted $$unsorted Bool)) % 0.38/1.00 (declare-const tptp.hascolor (-> $$unsorted $$unsorted Bool)) % 0.38/1.00 (declare-const tptp.hasperson (-> $$unsorted $$unsorted Bool)) % 0.38/1.00 (declare-const tptp.left (-> $$unsorted $$unsorted Bool)) % 0.38/1.00 (declare-const tptp.nextto (-> $$unsorted $$unsorted Bool)) % 0.38/1.00 (declare-const tptp.toad $$unsorted) % 0.38/1.00 (declare-const tptp.haspet (-> $$unsorted $$unsorted Bool)) % 0.38/1.00 (declare-const tptp.samepet (-> $$unsorted $$unsorted Bool)) % 0.38/1.00 (declare-const tptp.englishman $$unsorted) % 0.38/1.00 (declare-const tptp.n1 $$unsorted) % 0.38/1.00 (declare-const tptp.white $$unsorted) % 0.38/1.00 (declare-const tptp.quoits $$unsorted) % 0.38/1.00 (declare-const tptp.american $$unsorted) % 0.38/1.00 (declare-const tptp.n5 $$unsorted) % 0.38/1.00 (declare-const tptp.russian $$unsorted) % 0.38/1.00 (declare-const tptp.unknown_drink $$unsorted) % 0.38/1.00 (declare-const tptp.no_pet $$unsorted) % 0.38/1.00 (declare-const tptp.swede $$unsorted) % 0.38/1.00 (declare-const tptp.vodka $$unsorted) % 0.38/1.00 (declare-const tptp.backgammon $$unsorted) % 0.38/1.00 (declare-const tptp.samecolor (-> $$unsorted $$unsorted Bool)) % 0.38/1.00 (declare-const tptp.samehouse (-> $$unsorted $$unsorted Bool)) % 0.38/1.00 (declare-const tptp.rat $$unsorted) % 0.38/1.00 (declare-const tptp.italian $$unsorted) % 0.38/1.00 (declare-const tptp.milk $$unsorted) % 0.38/1.00 (declare-const tptp.red $$unsorted) % 0.38/1.00 (declare-const tptp.camel $$unsorted) % 0.38/1.00 (declare-const tptp.coffee $$unsorted) % 0.38/1.00 (declare-const tptp.solitaire $$unsorted) % 0.38/1.00 (declare-const tptp.n2 $$unsorted) % 0.38/1.00 (declare-const tptp.green $$unsorted) % 0.38/1.00 (declare-const tptp.hasgame (-> $$unsorted $$unsorted Bool)) % 0.38/1.00 (declare-const tptp.charades $$unsorted) % 0.38/1.00 (declare-const tptp.n3 $$unsorted) % 0.38/1.00 (declare-const tptp.yellow $$unsorted) % 0.38/1.00 (declare-const tptp.n4 $$unsorted) % 0.38/1.00 (declare-const tptp.blue $$unsorted) % 0.38/1.00 (declare-const tptp.guppy $$unsorted) % 0.38/1.00 (declare-const tptp.samedrink (-> $$unsorted $$unsorted Bool)) % 0.38/1.00 (declare-const tptp.sameperson (-> $$unsorted $$unsorted Bool)) % 0.38/1.00 (declare-const tptp.lemonade $$unsorted) % 0.38/1.00 (declare-const tptp.racquetball $$unsorted) % 0.38/1.00 (declare-const tptp.samegame (-> $$unsorted $$unsorted Bool)) % 0.38/1.00 (define @t1 () (@var "X" $$unsorted)) % 0.38/1.00 (define @t2 () (@list @t1)) % 0.38/1.00 (define @t3 () (forall @t2 (tptp.samehouse @t1 @t1))) % 0.38/1.00 (define @t4 () (tptp.samehouse tptp.n1 tptp.n2)) % 0.38/1.00 (define @t5 () (tptp.samehouse tptp.n1 tptp.n3)) % 0.38/1.00 (define @t6 () (tptp.samehouse tptp.n1 tptp.n4)) % 0.38/1.00 (define @t7 () (tptp.samehouse tptp.n2 tptp.n3)) % 0.38/1.00 (define @t8 () (tptp.samehouse tptp.n2 tptp.n4)) % 0.38/1.00 (define @t9 () (tptp.samehouse tptp.n3 tptp.n4)) % 0.38/1.00 (define @t10 () (tptp.samehouse tptp.n3 tptp.n5)) % 0.38/1.00 (define @t11 () (tptp.samehouse tptp.n4 tptp.n5)) % 0.38/1.00 (define @t12 () (tptp.sameperson tptp.englishman tptp.russian)) % 0.38/1.00 (define @t13 () (tptp.sameperson tptp.englishman tptp.american)) % 0.38/1.00 (define @t14 () (tptp.sameperson tptp.swede tptp.russian)) % 0.38/1.00 (define @t15 () (tptp.sameperson tptp.swede tptp.american)) % 0.38/1.00 (define @t16 () (tptp.samecolor tptp.red tptp.white)) % 0.38/1.00 (define @t17 () (tptp.samecolor tptp.red tptp.blue)) % 0.38/1.00 (define @t18 () (tptp.samecolor tptp.white tptp.blue)) % 0.38/1.00 (define @t19 () (tptp.samecolor tptp.green tptp.blue)) % 0.38/1.00 (define @t20 () (tptp.samedrink tptp.lemonade tptp.milk)) % 0.38/1.00 (define @t21 () (tptp.samedrink tptp.lemonade tptp.vodka)) % 0.38/1.00 (define @t22 () (tptp.samedrink tptp.coffee tptp.milk)) % 0.38/1.00 (define @t23 () (tptp.samedrink tptp.coffee tptp.vodka)) % 0.38/1.00 (define @t24 () (tptp.samedrink tptp.milk tptp.vodka)) % 0.38/1.00 (define @t25 () (tptp.samegame tptp.backgammon tptp.racquetball)) % 0.38/1.00 (define @t26 () (tptp.samegame tptp.backgammon tptp.solitaire)) % 0.38/1.00 (define @t27 () (tptp.samegame tptp.racquetball tptp.solitaire)) % 0.38/1.00 (define @t28 () (tptp.samegame tptp.solitaire tptp.charades)) % 0.38/1.00 (define @t29 () (tptp.samepet tptp.guppy tptp.toad)) % 0.38/1.00 (define @t30 () (tptp.samepet tptp.guppy tptp.rat)) % 0.38/1.00 (define @t31 () (tptp.samepet tptp.toad tptp.camel)) % 0.38/1.00 (define @t32 () (tptp.samepet tptp.toad tptp.rat)) % 0.38/1.00 (define @t33 () (tptp.samepet tptp.camel tptp.rat)) % 0.38/1.00 (define @t34 () (@var "Y" $$unsorted)) % 0.38/1.00 (define @t35 () (tptp.nextto @t1 @t34)) % 0.38/1.00 (define @t36 () (not @t35)) % 0.38/1.00 (define @t37 () (@list @t1 @t34)) % 0.38/1.00 (define @t38 () (forall @t37 (or @t36 (tptp.nextto @t34 @t1)))) % 0.38/1.00 (define @t39 () (tptp.left @t34 @t1)) % 0.38/1.00 (define @t40 () (tptp.left @t1 @t34)) % 0.38/1.00 (define @t41 () (not @t40)) % 0.38/1.00 (define @t42 () (forall @t37 (or @t41 @t35))) % 0.38/1.00 (define @t43 () (forall @t2 (not (tptp.nextto @t1 @t1)))) % 0.38/1.00 (define @t44 () (tptp.hasperson @t1 tptp.american)) % 0.38/1.00 (define @t45 () (tptp.hasperson @t1 tptp.russian)) % 0.38/1.00 (define @t46 () (tptp.hasperson @t1 tptp.swede)) % 0.38/1.00 (define @t47 () (tptp.hasperson @t1 tptp.italian)) % 0.38/1.00 (define @t48 () (tptp.hasperson @t1 tptp.englishman)) % 0.38/1.00 (define @t49 () (@list @t34)) % 0.38/1.00 (define @t50 () (tptp.hascolor @t1 tptp.blue)) % 0.38/1.00 (define @t51 () (tptp.hascolor @t1 tptp.yellow)) % 0.38/1.00 (define @t52 () (tptp.hascolor @t1 tptp.green)) % 0.38/1.00 (define @t53 () (tptp.hascolor @t1 tptp.white)) % 0.38/1.00 (define @t54 () (tptp.hascolor @t1 tptp.red)) % 0.38/1.00 (define @t55 () (forall @t2 (or @t54 @t53 @t52 @t51 @t50))) % 0.38/1.00 (define @t56 () (tptp.hasdrink @t1 tptp.vodka)) % 0.38/1.00 (define @t57 () (tptp.hasdrink @t1 tptp.coffee)) % 0.38/1.00 (define @t58 () (tptp.hasdrink @t1 tptp.lemonade)) % 0.38/1.00 (define @t59 () (forall @t2 (or @t58 @t57 (tptp.hasdrink @t1 tptp.milk) @t56 (tptp.hasdrink @t1 tptp.unknown_drink)))) % 0.38/1.00 (define @t60 () (forall @t49 (or (tptp.hasdrink tptp.n1 @t34) (tptp.hasdrink tptp.n2 @t34) (tptp.hasdrink tptp.n3 @t34) (tptp.hasdrink tptp.n4 @t34) (tptp.hasdrink tptp.n5 @t34)))) % 0.38/1.00 (define @t61 () (tptp.hasgame @t1 tptp.charades)) % 0.38/1.00 (define @t62 () (tptp.hasgame @t1 tptp.solitaire)) % 0.38/1.00 (define @t63 () (tptp.hasgame @t1 tptp.quoits)) % 0.38/1.00 (define @t64 () (tptp.hasgame @t1 tptp.racquetball)) % 0.38/1.00 (define @t65 () (tptp.hasgame @t1 tptp.backgammon)) % 0.38/1.00 (define @t66 () (forall @t2 (or @t65 @t64 @t63 @t62 @t61))) % 0.38/1.00 (define @t67 () (tptp.haspet @t1 tptp.rat)) % 0.38/1.00 (define @t68 () (tptp.haspet @t1 tptp.camel)) % 0.38/1.00 (define @t69 () (tptp.haspet @t1 tptp.toad)) % 0.38/1.00 (define @t70 () (tptp.haspet @t1 tptp.guppy)) % 0.38/1.00 (define @t71 () (@var "X2" $$unsorted)) % 0.38/1.00 (define @t72 () (@var "X1" $$unsorted)) % 0.38/1.00 (define @t73 () (tptp.samehouse @t72 @t71)) % 0.38/1.00 (define @t74 () (@list @t72 @t71 @t34)) % 0.38/1.00 (define @t75 () (forall @t74 (or @t73 (not (tptp.hasdrink @t72 @t34)) (not (tptp.hasdrink @t71 @t34))))) % 0.38/1.00 (define @t76 () (forall @t74 (or @t73 (not (tptp.hasgame @t72 @t34)) (not (tptp.hasgame @t71 @t34))))) % 0.38/1.00 (define @t77 () (forall @t74 (or (tptp.sameperson @t72 @t71) (not (tptp.hasperson @t34 @t72)) (not (tptp.hasperson @t34 @t71))))) % 0.38/1.00 (define @t78 () (forall @t74 (or (tptp.samecolor @t72 @t71) (not (tptp.hascolor @t34 @t72)) (not (tptp.hascolor @t34 @t71))))) % 0.38/1.00 (define @t79 () (forall @t74 (or (tptp.samedrink @t72 @t71) (not (tptp.hasdrink @t34 @t72)) (not (tptp.hasdrink @t34 @t71))))) % 0.38/1.00 (define @t80 () (forall @t74 (or (tptp.samepet @t72 @t71) (not (tptp.haspet @t34 @t72)) (not (tptp.haspet @t34 @t71))))) % 0.38/1.00 (define @t81 () (forall @t2 (or @t48 (not @t54)))) % 0.38/1.00 (define @t82 () (tptp.hascolor @t34 tptp.green)) % 0.38/1.00 (define @t83 () (not @t82)) % 0.38/1.00 (define @t84 () (not @t53)) % 0.38/1.00 (define @t85 () (forall @t37 (or @t84 @t82 @t41))) % 0.38/1.00 (define @t86 () (forall @t2 (or (not @t58) @t52))) % 0.38/1.00 (define @t87 () (forall @t2 (or (not @t46) @t57))) % 0.38/1.00 (define @t88 () (forall @t2 (or @t69 (not @t65)))) % 0.38/1.00 (define @t89 () (not @t64)) % 0.38/1.00 (define @t90 () (forall @t2 (or @t64 (not @t51)))) % 0.38/1.00 (define @t91 () (@var "Z" $$unsorted)) % 0.38/1.00 (define @t92 () (tptp.hasgame @t34 tptp.quoits)) % 0.38/1.00 (define @t93 () (not (tptp.nextto @t1 @t91))) % 0.38/1.00 (define @t94 () (tptp.samehouse @t34 @t91)) % 0.38/1.00 (define @t95 () (not @t68)) % 0.38/1.00 (define @t96 () (@list @t1 @t34 @t91)) % 0.38/1.00 (define @t97 () (not (tptp.samehouse tptp.n1 @t1))) % 0.38/1.00 (define @t98 () (not (tptp.samehouse @t1 tptp.n5))) % 0.38/1.00 (define @t99 () (forall @t37 (or @t95 @t35 (not @t92)))) % 0.38/1.00 (define @t100 () (tptp.haspet @t34 tptp.camel)) % 0.38/1.00 (define @t101 () (not @t63)) % 0.38/1.00 (define @t102 () (@list @t34 @t91 @t1)) % 0.38/1.00 (define @t103 () (forall @t102 (or @t94 @t36 @t93 @t101 @t100 (tptp.haspet @t91 tptp.camel)))) % 0.38/1.00 (define @t104 () (tptp.hasgame @t34 tptp.racquetball)) % 0.38/1.00 (define @t105 () (not @t67)) % 0.38/1.00 (define @t106 () (tptp.haspet @t34 tptp.rat)) % 0.38/1.00 (define @t107 () (forall @t37 (or @t36 @t97 @t89 @t106))) % 0.38/1.00 (define @t108 () (forall @t2 (or @t62 (not @t56)))) % 0.38/1.00 (define @t109 () (tptp.hascolor @t34 tptp.blue)) % 0.38/1.00 (define @t110 () (not @t45)) % 0.38/1.00 (define @t111 () (forall @t37 (or @t110 @t97 @t36 @t109))) % 0.38/1.00 (define @t112 () (forall @t37 (or @t110 @t35 (not @t109)))) % 0.38/1.00 (define @t113 () (tptp.hasperson @t34 tptp.russian)) % 0.38/1.00 (define @t114 () (not @t50)) % 0.38/1.00 (define @t115 () (tptp.left tptp.n1 tptp.n2)) % 0.38/1.00 (define @t116 () (tptp.left tptp.n2 tptp.n3)) % 0.38/1.00 (define @t117 () (tptp.left tptp.n3 tptp.n4)) % 0.38/1.00 (define @t118 () (tptp.left tptp.n4 tptp.n5)) % 0.38/1.00 (define @t119 () (tptp.nextto tptp.n1 tptp.n3)) % 0.38/1.00 (define @t120 () (tptp.nextto tptp.n1 tptp.n4)) % 0.38/1.00 (define @t121 () (tptp.nextto tptp.n1 tptp.n5)) % 0.38/1.00 (define @t122 () (tptp.nextto tptp.n2 tptp.n4)) % 0.38/1.00 (define @t123 () (tptp.nextto tptp.n2 tptp.n5)) % 0.38/1.00 (define @t124 () (tptp.nextto tptp.n3 tptp.n5)) % 0.38/1.00 (define @t125 () (tptp.hasdrink tptp.n3 tptp.milk)) % 0.38/1.00 (define @t126 () (tptp.hasperson tptp.n1 tptp.russian)) % 0.38/1.00 (define @t127 () (@var "X23" $$unsorted)) % 0.38/1.00 (define @t128 () (not (tptp.haspet tptp.n5 @t127))) % 0.38/1.00 (define @t129 () (@var "X22" $$unsorted)) % 0.38/1.00 (define @t130 () (not (tptp.haspet tptp.n4 @t129))) % 0.38/1.00 (define @t131 () (@var "X21" $$unsorted)) % 0.38/1.00 (define @t132 () (not (tptp.haspet tptp.n3 @t131))) % 0.38/1.00 (define @t133 () (@var "X20" $$unsorted)) % 0.38/1.00 (define @t134 () (not (tptp.haspet tptp.n2 @t133))) % 0.38/1.00 (define @t135 () (@var "X19" $$unsorted)) % 0.38/1.00 (define @t136 () (not (tptp.haspet tptp.n1 @t135))) % 0.38/1.00 (define @t137 () (@var "X18" $$unsorted)) % 0.38/1.00 (define @t138 () (not (tptp.hasgame tptp.n5 @t137))) % 0.38/1.00 (define @t139 () (@var "X17" $$unsorted)) % 0.38/1.00 (define @t140 () (not (tptp.hasgame tptp.n4 @t139))) % 0.38/1.00 (define @t141 () (@var "X16" $$unsorted)) % 0.38/1.00 (define @t142 () (not (tptp.hasgame tptp.n3 @t141))) % 0.38/1.00 (define @t143 () (@var "X15" $$unsorted)) % 0.38/1.00 (define @t144 () (not (tptp.hasgame tptp.n2 @t143))) % 0.38/1.00 (define @t145 () (@var "X14" $$unsorted)) % 0.38/1.00 (define @t146 () (not (tptp.hasgame tptp.n1 @t145))) % 0.38/1.00 (define @t147 () (@var "X13" $$unsorted)) % 0.38/1.00 (define @t148 () (not (tptp.hasdrink tptp.n5 @t147))) % 0.38/1.00 (define @t149 () (@var "X12" $$unsorted)) % 0.38/1.00 (define @t150 () (not (tptp.hasdrink tptp.n4 @t149))) % 0.38/1.00 (define @t151 () (@var "X11a" $$unsorted)) % 0.38/1.00 (define @t152 () (not (tptp.hasdrink tptp.n3 @t151))) % 0.38/1.00 (define @t153 () (@var "X11" $$unsorted)) % 0.38/1.00 (define @t154 () (not (tptp.hasdrink tptp.n2 @t153))) % 0.38/1.00 (define @t155 () (@var "X10" $$unsorted)) % 0.38/1.00 (define @t156 () (not (tptp.hasdrink tptp.n1 @t155))) % 0.38/1.00 (define @t157 () (@var "X9" $$unsorted)) % 0.38/1.00 (define @t158 () (not (tptp.hascolor tptp.n5 @t157))) % 0.38/1.00 (define @t159 () (@var "X8" $$unsorted)) % 0.38/1.00 (define @t160 () (not (tptp.hascolor tptp.n4 @t159))) % 0.38/1.00 (define @t161 () (@var "X7" $$unsorted)) % 0.38/1.00 (define @t162 () (not (tptp.hascolor tptp.n3 @t161))) % 0.38/1.00 (define @t163 () (@var "X6" $$unsorted)) % 0.38/1.00 (define @t164 () (not (tptp.hascolor tptp.n2 @t163))) % 0.38/1.00 (define @t165 () (@var "X5" $$unsorted)) % 0.38/1.00 (define @t166 () (not (tptp.hascolor tptp.n1 @t165))) % 0.38/1.00 (define @t167 () (@var "X4" $$unsorted)) % 0.38/1.00 (define @t168 () (not (tptp.hasperson tptp.n5 @t167))) % 0.38/1.00 (define @t169 () (@var "X3" $$unsorted)) % 0.38/1.00 (define @t170 () (not (tptp.hasperson tptp.n4 @t169))) % 0.38/1.00 (define @t171 () (not (tptp.hasperson tptp.n3 @t71))) % 0.38/1.00 (define @t172 () (not (tptp.hasperson tptp.n2 @t72))) % 0.38/1.00 (define @t173 () (@var "X0" $$unsorted)) % 0.38/1.00 (define @t174 () (not (tptp.hasperson tptp.n1 @t173))) % 0.38/1.00 (define @t175 () (forall (@list @t173 @t72 @t71 @t169 @t167 @t165 @t163 @t161 @t159 @t157 @t155 @t153 @t151 @t149 @t147 @t145 @t143 @t141 @t139 @t137 @t135 @t133 @t131 @t129 @t127) (or @t174 @t172 @t171 @t170 @t168 @t166 @t164 @t162 @t160 @t158 @t156 @t154 @t152 @t150 @t148 @t146 @t144 @t142 @t140 @t138 @t136 @t134 @t132 @t130 @t128))) % 0.38/1.00 (define @t176 () (@list tptp.n4)) % 0.38/1.00 (define @t177 () (@list tptp.n3 tptp.n4)) % 0.38/1.00 (define @t178 () (not @t117)) % 0.38/1.00 (define @t179 () (tptp.hascolor tptp.n4 tptp.green)) % 0.38/1.00 (define @t180 () (not @t179)) % 0.38/1.00 (define @t181 () (tptp.hascolor tptp.n3 tptp.white)) % 0.38/1.00 (define @t182 () (or @t181 @t180 @t178)) % 0.38/1.00 (define @t183 () (@list tptp.n4 tptp.n5)) % 0.38/1.00 (define @t184 () (tptp.left tptp.n5 tptp.n4)) % 0.38/1.00 (define @t185 () (not @t184)) % 0.38/1.00 (define @t186 () (not @t118)) % 0.38/1.00 (define @t187 () (or @t186 @t185)) % 0.38/1.00 (define @t188 () (@list false false)) % 0.38/1.00 (define @t189 () (@list tptp.n5 tptp.n4)) % 0.38/1.00 (define @t190 () (tptp.hascolor tptp.n5 tptp.white)) % 0.38/1.00 (define @t191 () (not @t190)) % 0.38/1.00 (define @t192 () (or @t191 @t180 @t184)) % 0.38/1.00 (define @t193 () (@list tptp.n2)) % 0.38/1.00 (define @t194 () (tptp.hasgame tptp.n2 tptp.charades)) % 0.38/1.00 (define @t195 () (not @t194)) % 0.38/1.00 (define @t196 () (tptp.hasgame tptp.n2 tptp.solitaire)) % 0.38/1.00 (define @t197 () (not @t196)) % 0.38/1.00 (define @t198 () (or @t28 @t197 @t195)) % 0.38/1.00 (define @t199 () (tptp.hasperson tptp.n2 tptp.american)) % 0.38/1.00 (define @t200 () (or @t199 @t195)) % 0.38/1.00 (define @t201 () (tptp.hasdrink tptp.n2 tptp.vodka)) % 0.38/1.00 (define @t202 () (not @t201)) % 0.38/1.00 (define @t203 () (or @t196 @t202)) % 0.38/1.00 (define @t204 () (not @t199)) % 0.38/1.00 (define @t205 () (tptp.hasperson tptp.n2 tptp.swede)) % 0.38/1.00 (define @t206 () (not @t205)) % 0.38/1.00 (define @t207 () (or @t15 @t206 @t204)) % 0.38/1.00 (define @t208 () (@list tptp.n5 tptp.n1)) % 0.38/1.00 (define @t209 () (tptp.nextto tptp.n5 tptp.n1)) % 0.38/1.00 (define @t210 () (not @t209)) % 0.38/1.00 (define @t211 () (or @t210 @t121)) % 0.38/1.00 (define @t212 () (@list true false)) % 0.38/1.00 (define @t213 () (tptp.left tptp.n5 tptp.n1)) % 0.38/1.00 (define @t214 () (not @t213)) % 0.38/1.00 (define @t215 () (or @t214 @t209)) % 0.38/1.00 (define @t216 () (tptp.hascolor tptp.n1 tptp.green)) % 0.38/1.00 (define @t217 () (not @t216)) % 0.38/1.00 (define @t218 () (or @t191 @t217 @t213)) % 0.38/1.00 (define @t219 () (@list tptp.n3 tptp.n1)) % 0.38/1.00 (define @t220 () (tptp.nextto tptp.n3 tptp.n1)) % 0.38/1.00 (define @t221 () (not @t220)) % 0.38/1.00 (define @t222 () (or @t221 @t119)) % 0.38/1.00 (define @t223 () (tptp.left tptp.n3 tptp.n1)) % 0.38/1.00 (define @t224 () (not @t223)) % 0.38/1.00 (define @t225 () (or @t224 @t220)) % 0.38/1.00 (define @t226 () (not @t181)) % 0.38/1.00 (define @t227 () (or @t226 @t217 @t223)) % 0.38/1.00 (define @t228 () (@list tptp.n4 tptp.n1)) % 0.38/1.00 (define @t229 () (tptp.nextto tptp.n4 tptp.n1)) % 0.38/1.00 (define @t230 () (not @t229)) % 0.38/1.00 (define @t231 () (or @t230 @t120)) % 0.38/1.00 (define @t232 () (tptp.left tptp.n4 tptp.n1)) % 0.38/1.00 (define @t233 () (not @t232)) % 0.38/1.00 (define @t234 () (or @t233 @t229)) % 0.38/1.00 (define @t235 () (tptp.hascolor tptp.n4 tptp.white)) % 0.38/1.00 (define @t236 () (not @t235)) % 0.38/1.00 (define @t237 () (or @t236 @t217 @t232)) % 0.38/1.00 (define @t238 () (@list tptp.n1 tptp.n2)) % 0.38/1.00 (define @t239 () (@list tptp.n1)) % 0.38/1.00 (define @t240 () (tptp.nextto tptp.n1 tptp.n2)) % 0.38/1.00 (define @t241 () (not @t115)) % 0.38/1.00 (define @t242 () (or @t241 @t240)) % 0.38/1.00 (define @t243 () (tptp.hascolor tptp.n2 tptp.blue)) % 0.38/1.00 (define @t244 () (not @t240)) % 0.38/1.00 (define @t245 () (tptp.samehouse tptp.n1 tptp.n1)) % 0.38/1.00 (define @t246 () (not @t245)) % 0.38/1.00 (define @t247 () (not @t126)) % 0.38/1.00 (define @t248 () (or @t247 @t246 @t244 @t243)) % 0.38/1.00 (define @t249 () (@list false false false false)) % 0.38/1.00 (define @t250 () (not @t243)) % 0.38/1.00 (define @t251 () (tptp.hascolor tptp.n2 tptp.white)) % 0.38/1.00 (define @t252 () (not @t251)) % 0.38/1.00 (define @t253 () (or @t18 @t252 @t250)) % 0.38/1.00 (define @t254 () (@list true false false)) % 0.38/1.00 (define @t255 () (tptp.hascolor tptp.n2 tptp.green)) % 0.38/1.00 (define @t256 () (not @t255)) % 0.38/1.00 (define @t257 () (or @t19 @t256 @t250)) % 0.38/1.00 (define @t258 () (tptp.hascolor tptp.n1 tptp.white)) % 0.38/1.00 (define @t259 () (not @t258)) % 0.38/1.00 (define @t260 () (or @t259 @t255 @t241)) % 0.38/1.00 (define @t261 () (@list false true false)) % 0.38/1.00 (define @t262 () (@list tptp.white)) % 0.38/1.00 (define @t263 () (or @t258 @t251 @t181 @t235 @t190)) % 0.38/1.00 (define @t264 () (tptp.hasdrink tptp.n1 tptp.lemonade)) % 0.38/1.00 (define @t265 () (not @t264)) % 0.38/1.00 (define @t266 () (or @t265 @t216)) % 0.38/1.00 (define @t267 () (tptp.hascolor tptp.n1 tptp.blue)) % 0.38/1.00 (define @t268 () (not @t267)) % 0.38/1.00 (define @t269 () (tptp.nextto tptp.n1 tptp.n1)) % 0.38/1.00 (define @t270 () (or @t247 @t269 @t268)) % 0.38/1.00 (define @t271 () (tptp.hasperson tptp.n1 tptp.englishman)) % 0.38/1.00 (define @t272 () (not @t271)) % 0.38/1.00 (define @t273 () (or @t12 @t272 @t247)) % 0.38/1.00 (define @t274 () (tptp.hascolor tptp.n1 tptp.red)) % 0.38/1.00 (define @t275 () (not @t274)) % 0.38/1.00 (define @t276 () (or @t271 @t275)) % 0.38/1.00 (define @t277 () (tptp.hascolor tptp.n1 tptp.yellow)) % 0.38/1.00 (define @t278 () (or @t274 @t258 @t216 @t277 @t267)) % 0.38/1.00 (define @t279 () (not @t125)) % 0.38/1.00 (define @t280 () (tptp.hasdrink tptp.n1 tptp.milk)) % 0.38/1.00 (define @t281 () (not @t280)) % 0.38/1.00 (define @t282 () (or @t5 @t281 @t279)) % 0.38/1.00 (define @t283 () (tptp.hasperson tptp.n1 tptp.swede)) % 0.38/1.00 (define @t284 () (not @t283)) % 0.38/1.00 (define @t285 () (or @t14 @t284 @t247)) % 0.38/1.00 (define @t286 () (tptp.hasdrink tptp.n1 tptp.coffee)) % 0.38/1.00 (define @t287 () (not @t286)) % 0.38/1.00 (define @t288 () (or @t283 @t287)) % 0.38/1.00 (define @t289 () (tptp.hasdrink tptp.n1 tptp.unknown_drink)) % 0.38/1.00 (define @t290 () (tptp.hasdrink tptp.n1 tptp.vodka)) % 0.38/1.00 (define @t291 () (or @t264 @t286 @t280 @t290 @t289)) % 0.38/1.00 (define @t292 () (not @t277)) % 0.38/1.00 (define @t293 () (tptp.hasgame tptp.n1 tptp.racquetball)) % 0.38/1.00 (define @t294 () (or @t293 @t292)) % 0.38/1.00 (define @t295 () (not @t290)) % 0.38/1.00 (define @t296 () (tptp.hasgame tptp.n1 tptp.solitaire)) % 0.38/1.00 (define @t297 () (or @t296 @t295)) % 0.38/1.00 (define @t298 () (not @t296)) % 0.38/1.00 (define @t299 () (not @t293)) % 0.38/1.00 (define @t300 () (or @t27 @t299 @t298)) % 0.38/1.00 (define @t301 () (@list true)) % 0.38/1.00 (define @t302 () (tptp.hasdrink tptp.n2 tptp.unknown_drink)) % 0.38/1.00 (define @t303 () (not @t302)) % 0.38/1.00 (define @t304 () (not @t289)) % 0.38/1.00 (define @t305 () (or @t4 @t304 @t303)) % 0.38/1.00 (define @t306 () (tptp.hasdrink tptp.n2 tptp.milk)) % 0.38/1.00 (define @t307 () (not @t306)) % 0.38/1.00 (define @t308 () (or @t7 @t307 @t279)) % 0.38/1.00 (define @t309 () (tptp.hasdrink tptp.n2 tptp.lemonade)) % 0.38/1.00 (define @t310 () (not @t309)) % 0.38/1.00 (define @t311 () (or @t310 @t255)) % 0.38/1.00 (define @t312 () (tptp.hasdrink tptp.n2 tptp.coffee)) % 0.38/1.00 (define @t313 () (or @t309 @t312 @t306 @t201 @t302)) % 0.38/1.00 (define @t314 () (not @t312)) % 0.38/1.00 (define @t315 () (or @t205 @t314)) % 0.38/1.00 (define @t316 () (or @t204 @t194)) % 0.38/1.00 (define @t317 () (@list true true true true false)) % 0.38/1.00 (define @t318 () (tptp.haspet tptp.n2 tptp.rat)) % 0.38/1.00 (define @t319 () (or @t244 @t246 @t299 @t318)) % 0.38/1.00 (define @t320 () (not @t318)) % 0.38/1.00 (define @t321 () (tptp.haspet tptp.n2 tptp.guppy)) % 0.38/1.00 (define @t322 () (not @t321)) % 0.38/1.00 (define @t323 () (or @t30 @t322 @t320)) % 0.38/1.00 (define @t324 () (tptp.hasperson tptp.n2 tptp.italian)) % 0.38/1.00 (define @t325 () (not @t324)) % 0.38/1.00 (define @t326 () (or @t325 @t321)) % 0.38/1.00 (define @t327 () (tptp.hascolor tptp.n2 tptp.red)) % 0.38/1.00 (define @t328 () (not @t327)) % 0.38/1.00 (define @t329 () (or @t17 @t328 @t250)) % 0.38/1.00 (define @t330 () (tptp.hasperson tptp.n2 tptp.englishman)) % 0.38/1.00 (define @t331 () (not @t330)) % 0.38/1.00 (define @t332 () (or @t331 @t327)) % 0.38/1.00 (define @t333 () (tptp.hasperson tptp.n2 tptp.russian)) % 0.38/1.00 (define @t334 () (not @t333)) % 0.38/1.00 (define @t335 () (or @t4 @t247 @t334)) % 0.38/1.00 (define @t336 () (or @t330 @t324 @t205 @t333 @t199)) % 0.38/1.00 (define @t337 () (or @t206 @t312)) % 0.38/1.00 (define @t338 () (or @t23 @t314 @t202)) % 0.38/1.00 (define @t339 () (or @t197 @t201)) % 0.38/1.00 (define @t340 () (@list tptp.n2 tptp.n4 tptp.coffee)) % 0.38/1.00 (define @t341 () (tptp.hasdrink tptp.n4 tptp.coffee)) % 0.38/1.00 (define @t342 () (not @t341)) % 0.38/1.00 (define @t343 () (or @t8 @t314 @t342)) % 0.38/1.00 (define @t344 () (tptp.hasperson tptp.n4 tptp.swede)) % 0.38/1.00 (define @t345 () (not @t344)) % 0.38/1.00 (define @t346 () (or @t345 @t341)) % 0.38/1.00 (define @t347 () (@list tptp.toad tptp.rat tptp.n2)) % 0.38/1.00 (define @t348 () (tptp.haspet tptp.n2 tptp.toad)) % 0.38/1.00 (define @t349 () (not @t348)) % 0.38/1.00 (define @t350 () (or @t32 @t349 @t320)) % 0.38/1.00 (define @t351 () (tptp.hasgame tptp.n2 tptp.backgammon)) % 0.38/1.00 (define @t352 () (not @t351)) % 0.38/1.00 (define @t353 () (or @t348 @t352)) % 0.38/1.00 (define @t354 () (tptp.hasgame tptp.n2 tptp.quoits)) % 0.38/1.00 (define @t355 () (tptp.hasgame tptp.n2 tptp.racquetball)) % 0.38/1.00 (define @t356 () (or @t351 @t355 @t354 @t196 @t194)) % 0.38/1.00 (define @t357 () (@list tptp.n1 tptp.n2 tptp.racquetball)) % 0.38/1.00 (define @t358 () (not @t355)) % 0.38/1.00 (define @t359 () (or @t4 @t299 @t358)) % 0.38/1.00 (define @t360 () (@list tptp.n4 tptp.n2)) % 0.38/1.00 (define @t361 () (not @t354)) % 0.38/1.00 (define @t362 () (tptp.nextto tptp.n4 tptp.n2)) % 0.38/1.00 (define @t363 () (tptp.haspet tptp.n4 tptp.camel)) % 0.38/1.00 (define @t364 () (not @t363)) % 0.38/1.00 (define @t365 () (or @t364 @t362 @t361)) % 0.38/1.00 (define @t366 () (not @t362)) % 0.38/1.00 (define @t367 () (or @t366 @t122)) % 0.38/1.00 (define @t368 () (@list tptp.n2 tptp.n4 tptp.n3)) % 0.38/1.00 (define @t369 () (tptp.haspet tptp.n2 tptp.camel)) % 0.38/1.00 (define @t370 () (tptp.hasgame tptp.n3 tptp.quoits)) % 0.38/1.00 (define @t371 () (not @t370)) % 0.38/1.00 (define @t372 () (tptp.nextto tptp.n3 tptp.n4)) % 0.38/1.00 (define @t373 () (not @t372)) % 0.38/1.00 (define @t374 () (tptp.nextto tptp.n3 tptp.n2)) % 0.38/1.00 (define @t375 () (not @t374)) % 0.38/1.00 (define @t376 () (or @t8 @t375 @t373 @t371 @t369 @t363)) % 0.38/1.00 (define @t377 () (@list tptp.camel tptp.rat tptp.n2)) % 0.38/1.00 (define @t378 () (not @t369)) % 0.38/1.00 (define @t379 () (or @t33 @t378 @t320)) % 0.38/1.00 (define @t380 () (@list tptp.n2 tptp.n3)) % 0.38/1.00 (define @t381 () (tptp.nextto tptp.n2 tptp.n3)) % 0.38/1.00 (define @t382 () (not @t381)) % 0.38/1.00 (define @t383 () (or @t382 @t374)) % 0.38/1.00 (define @t384 () (not @t116)) % 0.38/1.00 (define @t385 () (or @t384 @t381)) % 0.38/1.00 (define @t386 () (or @t178 @t372)) % 0.38/1.00 (define @t387 () (tptp.hasgame tptp.n3 tptp.racquetball)) % 0.38/1.00 (define @t388 () (not @t387)) % 0.38/1.00 (define @t389 () (or @t5 @t299 @t388)) % 0.38/1.00 (define @t390 () (@list tptp.n3)) % 0.38/1.00 (define @t391 () (tptp.hasdrink tptp.n3 tptp.vodka)) % 0.38/1.00 (define @t392 () (not @t391)) % 0.38/1.00 (define @t393 () (or @t24 @t279 @t392)) % 0.38/1.00 (define @t394 () (tptp.hasgame tptp.n3 tptp.solitaire)) % 0.38/1.00 (define @t395 () (not @t394)) % 0.38/1.00 (define @t396 () (or @t395 @t391)) % 0.38/1.00 (define @t397 () (tptp.hasgame tptp.n3 tptp.charades)) % 0.38/1.00 (define @t398 () (tptp.hasgame tptp.n3 tptp.backgammon)) % 0.38/1.00 (define @t399 () (or @t398 @t387 @t370 @t394 @t397)) % 0.38/1.00 (define @t400 () (not @t397)) % 0.38/1.00 (define @t401 () (tptp.hasperson tptp.n3 tptp.american)) % 0.38/1.00 (define @t402 () (or @t401 @t400)) % 0.38/1.00 (define @t403 () (not @t401)) % 0.38/1.00 (define @t404 () (tptp.hasperson tptp.n3 tptp.englishman)) % 0.38/1.00 (define @t405 () (not @t404)) % 0.38/1.00 (define @t406 () (or @t13 @t405 @t403)) % 0.38/1.00 (define @t407 () (tptp.hasperson tptp.n4 tptp.american)) % 0.38/1.00 (define @t408 () (not @t407)) % 0.38/1.00 (define @t409 () (or @t9 @t403 @t408)) % 0.38/1.00 (define @t410 () (tptp.hascolor tptp.n3 tptp.red)) % 0.38/1.00 (define @t411 () (not @t410)) % 0.38/1.00 (define @t412 () (or @t404 @t411)) % 0.38/1.00 (define @t413 () (tptp.hascolor tptp.n3 tptp.blue)) % 0.38/1.00 (define @t414 () (not @t413)) % 0.38/1.00 (define @t415 () (or @t247 @t119 @t414)) % 0.38/1.00 (define @t416 () (tptp.hascolor tptp.n3 tptp.yellow)) % 0.38/1.00 (define @t417 () (not @t416)) % 0.38/1.00 (define @t418 () (or @t5 @t292 @t417)) % 0.38/1.00 (define @t419 () (tptp.hascolor tptp.n3 tptp.green)) % 0.38/1.00 (define @t420 () (not @t419)) % 0.38/1.00 (define @t421 () (or @t251 @t420 @t384)) % 0.38/1.00 (define @t422 () (or @t410 @t181 @t419 @t416 @t413)) % 0.38/1.00 (define @t423 () (@list tptp.n3 tptp.n5)) % 0.38/1.00 (define @t424 () (tptp.left tptp.n3 tptp.n5)) % 0.38/1.00 (define @t425 () (not @t424)) % 0.38/1.00 (define @t426 () (or @t425 @t124)) % 0.38/1.00 (define @t427 () (tptp.hascolor tptp.n5 tptp.green)) % 0.38/1.00 (define @t428 () (not @t427)) % 0.38/1.00 (define @t429 () (or @t226 @t428 @t424)) % 0.38/1.00 (define @t430 () (@list tptp.n5)) % 0.38/1.00 (define @t431 () (tptp.hasdrink tptp.n5 tptp.lemonade)) % 0.38/1.00 (define @t432 () (not @t431)) % 0.38/1.00 (define @t433 () (or @t432 @t427)) % 0.38/1.00 (define @t434 () (tptp.hascolor tptp.n5 tptp.blue)) % 0.38/1.00 (define @t435 () (not @t434)) % 0.38/1.00 (define @t436 () (or @t247 @t121 @t435)) % 0.38/1.00 (define @t437 () (tptp.hasgame tptp.n5 tptp.racquetball)) % 0.38/1.00 (define @t438 () (not @t437)) % 0.38/1.00 (define @t439 () (or @t320 @t123 @t438)) % 0.38/1.00 (define @t440 () (tptp.hascolor tptp.n5 tptp.yellow)) % 0.38/1.00 (define @t441 () (not @t440)) % 0.38/1.00 (define @t442 () (or @t437 @t441)) % 0.38/1.00 (define @t443 () (tptp.hascolor tptp.n5 tptp.red)) % 0.38/1.00 (define @t444 () (or @t443 @t190 @t427 @t440 @t434)) % 0.38/1.00 (define @t445 () (tptp.hasdrink tptp.n3 tptp.lemonade)) % 0.38/1.00 (define @t446 () (not @t445)) % 0.38/1.00 (define @t447 () (or @t20 @t446 @t279)) % 0.38/1.00 (define @t448 () (@list tptp.lemonade)) % 0.38/1.00 (define @t449 () (tptp.hasdrink tptp.n4 tptp.lemonade)) % 0.38/1.00 (define @t450 () (or @t264 @t309 @t445 @t449 @t431)) % 0.38/1.00 (define @t451 () (not @t443)) % 0.38/1.00 (define @t452 () (tptp.hascolor tptp.n4 tptp.red)) % 0.38/1.00 (define @t453 () (not @t452)) % 0.38/1.00 (define @t454 () (or @t11 @t453 @t451)) % 0.38/1.00 (define @t455 () (tptp.hasdrink tptp.n4 tptp.vodka)) % 0.38/1.00 (define @t456 () (not @t455)) % 0.38/1.00 (define @t457 () (not @t449)) % 0.38/1.00 (define @t458 () (or @t21 @t457 @t456)) % 0.38/1.00 (define @t459 () (tptp.hasperson tptp.n4 tptp.englishman)) % 0.38/1.00 (define @t460 () (not @t459)) % 0.38/1.00 (define @t461 () (or @t460 @t452)) % 0.38/1.00 (define @t462 () (tptp.hasgame tptp.n4 tptp.solitaire)) % 0.38/1.00 (define @t463 () (not @t462)) % 0.38/1.00 (define @t464 () (or @t463 @t455)) % 0.38/1.00 (define @t465 () (tptp.hasperson tptp.n4 tptp.russian)) % 0.38/1.00 (define @t466 () (not @t465)) % 0.38/1.00 (define @t467 () (or @t6 @t247 @t466)) % 0.38/1.00 (define @t468 () (tptp.hasperson tptp.n4 tptp.italian)) % 0.38/1.00 (define @t469 () (or @t459 @t468 @t344 @t465 @t407)) % 0.38/1.00 (define @t470 () (@list tptp.solitaire)) % 0.38/1.00 (define @t471 () (tptp.hasgame tptp.n5 tptp.solitaire)) % 0.38/1.00 (define @t472 () (or @t296 @t196 @t394 @t462 @t471)) % 0.38/1.00 (define @t473 () (tptp.haspet tptp.n4 tptp.guppy)) % 0.38/1.00 (define @t474 () (not @t468)) % 0.38/1.00 (define @t475 () (or @t474 @t473)) % 0.38/1.00 (define @t476 () (not @t471)) % 0.38/1.00 (define @t477 () (tptp.hasgame tptp.n5 tptp.backgammon)) % 0.38/1.00 (define @t478 () (not @t477)) % 0.38/1.00 (define @t479 () (or @t26 @t478 @t476)) % 0.38/1.00 (define @t480 () (tptp.haspet tptp.n4 tptp.toad)) % 0.38/1.00 (define @t481 () (not @t480)) % 0.38/1.00 (define @t482 () (not @t473)) % 0.38/1.00 (define @t483 () (or @t29 @t482 @t481)) % 0.38/1.00 (define @t484 () (tptp.hasgame tptp.n1 tptp.backgammon)) % 0.38/1.00 (define @t485 () (not @t484)) % 0.38/1.00 (define @t486 () (or @t25 @t485 @t299)) % 0.38/1.00 (define @t487 () (@list tptp.backgammon)) % 0.38/1.00 (define @t488 () (tptp.hasgame tptp.n4 tptp.backgammon)) % 0.38/1.00 (define @t489 () (or @t484 @t351 @t398 @t488 @t477)) % 0.38/1.00 (define @t490 () (not @t488)) % 0.38/1.00 (define @t491 () (or @t480 @t490)) % 0.38/1.00 (define @t492 () (not @t398)) % 0.38/1.00 (define @t493 () (or @t9 @t492 @t490)) % 0.38/1.00 (define @t494 () (tptp.haspet tptp.n3 tptp.toad)) % 0.38/1.00 (define @t495 () (or @t494 @t492)) % 0.38/1.00 (define @t496 () (not @t494)) % 0.38/1.00 (define @t497 () (tptp.haspet tptp.n3 tptp.guppy)) % 0.38/1.00 (define @t498 () (not @t497)) % 0.38/1.00 (define @t499 () (or @t29 @t498 @t496)) % 0.38/1.00 (define @t500 () (tptp.haspet tptp.n3 tptp.camel)) % 0.38/1.00 (define @t501 () (not @t500)) % 0.38/1.00 (define @t502 () (or @t31 @t496 @t501)) % 0.38/1.00 (define @t503 () (tptp.hasperson tptp.n3 tptp.italian)) % 0.38/1.00 (define @t504 () (not @t503)) % 0.38/1.00 (define @t505 () (or @t504 @t497)) % 0.38/1.00 (define @t506 () (@list tptp.n5 tptp.n2)) % 0.38/1.00 (define @t507 () (tptp.nextto tptp.n5 tptp.n2)) % 0.38/1.00 (define @t508 () (not @t507)) % 0.38/1.00 (define @t509 () (or @t508 @t123)) % 0.38/1.00 (define @t510 () (tptp.haspet tptp.n5 tptp.camel)) % 0.38/1.00 (define @t511 () (not @t510)) % 0.38/1.00 (define @t512 () (or @t511 @t507 @t361)) % 0.38/1.00 (define @t513 () (@list tptp.camel)) % 0.38/1.00 (define @t514 () (tptp.haspet tptp.n1 tptp.camel)) % 0.38/1.00 (define @t515 () (or @t514 @t369 @t500 @t363 @t510)) % 0.38/1.00 (define @t516 () (or @t16 @t411 @t226)) % 0.38/1.00 (define @t517 () (or @t405 @t410)) % 0.38/1.00 (define @t518 () (tptp.hasdrink tptp.n3 tptp.coffee)) % 0.38/1.00 (define @t519 () (not @t518)) % 0.38/1.00 (define @t520 () (or @t22 @t519 @t279)) % 0.38/1.00 (define @t521 () (tptp.hasperson tptp.n3 tptp.swede)) % 0.38/1.00 (define @t522 () (not @t521)) % 0.38/1.00 (define @t523 () (or @t522 @t518)) % 0.38/1.00 (define @t524 () (tptp.hasperson tptp.n3 tptp.russian)) % 0.38/1.00 (define @t525 () (not @t524)) % 0.38/1.00 (define @t526 () (or @t5 @t247 @t525)) % 0.38/1.00 (define @t527 () (or @t404 @t503 @t521 @t524 @t401)) % 0.38/1.00 (define @t528 () (tptp.hasgame tptp.n4 tptp.charades)) % 0.38/1.00 (define @t529 () (not @t528)) % 0.38/1.00 (define @t530 () (or @t407 @t529)) % 0.38/1.00 (define @t531 () (tptp.hasgame tptp.n4 tptp.racquetball)) % 0.38/1.00 (define @t532 () (not @t531)) % 0.38/1.00 (define @t533 () (or @t320 @t122 @t532)) % 0.38/1.00 (define @t534 () (tptp.hasgame tptp.n4 tptp.quoits)) % 0.38/1.00 (define @t535 () (or @t488 @t531 @t534 @t462 @t528)) % 0.38/1.00 (define @t536 () (not @t534)) % 0.38/1.00 (define @t537 () (not @t514)) % 0.38/1.00 (define @t538 () (or @t537 @t120 @t536)) % 0.38/1.00 (define @t539 () (or @t457 @t179)) % 0.38/1.00 (define @t540 () (or @t226 @t179 @t178)) % 0.38/1.00 (define @t541 () (or @t9 @t411 @t453)) % 0.38/1.00 (define @t542 () (forall (@list @t161) @t162)) % 0.38/1.00 (define @t543 () (@list tptp.red)) % 0.38/1.00 (define @t544 () (@list false)) % 0.38/1.00 (define @t545 () (@list tptp.green)) % 0.38/1.00 (define @t546 () (or @t216 @t255 @t419 @t179 @t427)) % 0.38/1.00 (define @t547 () (or @t235 @t428 @t186)) % 0.38/1.00 (define @t548 () (forall (@list @t159) @t160)) % 0.38/1.00 (define @t549 () (forall (@list @t71) @t171)) % 0.38/1.00 (define @t550 () (forall (@list @t147) @t148)) % 0.38/1.00 (define @t551 () (forall (@list @t143) @t144)) % 0.38/1.00 (define @t552 () (forall (@list @t153) @t154)) % 0.38/1.00 (define @t553 () (tptp.nextto tptp.n4 tptp.n5)) % 0.38/1.00 (define @t554 () (or @t186 @t553)) % 0.38/1.00 (define @t555 () (tptp.nextto tptp.n5 tptp.n4)) % 0.38/1.00 (define @t556 () (not @t553)) % 0.38/1.00 (define @t557 () (or @t556 @t555)) % 0.38/1.00 (define @t558 () (tptp.hasgame tptp.n5 tptp.quoits)) % 0.38/1.00 (define @t559 () (not @t558)) % 0.38/1.00 (define @t560 () (not @t555)) % 0.38/1.00 (define @t561 () (tptp.samehouse tptp.n5 tptp.n5)) % 0.38/1.00 (define @t562 () (not @t561)) % 0.38/1.00 (define @t563 () (or @t562 @t560 @t559 @t363)) % 0.38/1.00 (define @t564 () (tptp.haspet tptp.n5 tptp.rat)) % 0.38/1.00 (define @t565 () (not @t564)) % 0.38/1.00 (define @t566 () (or @t565 @t209 @t299)) % 0.38/1.00 (define @t567 () (forall (@list @t127) @t128)) % 0.38/1.00 (define @t568 () (@list tptp.toad)) % 0.38/1.00 (define @t569 () (tptp.haspet tptp.n5 tptp.toad)) % 0.38/1.00 (define @t570 () (not @t569)) % 0.38/1.00 (define @t571 () (@list tptp.guppy)) % 0.38/1.00 (define @t572 () (tptp.haspet tptp.n5 tptp.guppy)) % 0.38/1.00 (define @t573 () (tptp.haspet tptp.n5 tptp.no_pet)) % 0.38/1.00 (define @t574 () (or @t572 @t569 @t510 @t564 @t573)) % 0.38/1.00 (define @t575 () (forall (@list @t72) @t172)) % 0.38/1.00 (define @t576 () (tptp.hasdrink tptp.n4 tptp.milk)) % 0.38/1.00 (define @t577 () (not @t576)) % 0.38/1.00 (define @t578 () (or @t9 @t279 @t577)) % 0.38/1.00 (define @t579 () (tptp.hasdrink tptp.n4 tptp.unknown_drink)) % 0.38/1.00 (define @t580 () (not @t579)) % 0.38/1.00 (define @t581 () (or @t6 @t304 @t580)) % 0.38/1.00 (define @t582 () (or @t449 @t341 @t576 @t455 @t579)) % 0.38/1.00 (define @t583 () (or @t462 @t456)) % 0.38/1.00 (define @t584 () (forall (@list @t149) @t150)) % 0.38/1.00 (define @t585 () (forall (@list @t141) @t142)) % 0.38/1.00 (define @t586 () (forall (@list @t139) @t140)) % 0.38/1.00 (define @t587 () (or @t11 @t463 @t476)) % 0.38/1.00 (define @t588 () (forall (@list @t131) @t132)) % 0.38/1.00 (define @t589 () (or @t10 @t496 @t570)) % 0.38/1.00 (define @t590 () (or @t569 @t478)) % 0.38/1.00 (define @t591 () (tptp.hasgame tptp.n5 tptp.charades)) % 0.38/1.00 (define @t592 () (or @t477 @t437 @t558 @t471 @t591)) % 0.38/1.00 (define @t593 () (forall (@list @t137) @t138)) % 0.38/1.00 (define @t594 () (not @t591)) % 0.38/1.00 (define @t595 () (tptp.hasperson tptp.n5 tptp.american)) % 0.38/1.00 (define @t596 () (or @t595 @t594)) % 0.38/1.00 (define @t597 () (forall (@list @t167) @t168)) % 0.38/1.00 (define @t598 () (not @t595)) % 0.38/1.00 (define @t599 () (or @t11 @t408 @t598)) % 0.38/1.00 (define @t600 () (forall (@list @t169) @t170)) % 0.38/1.00 (define @t601 () (forall (@list @t129) @t130)) % 0.38/1.00 (define @t602 () (forall (@list @t133) @t134)) % 0.38/1.00 (define @t603 () (forall (@list @t155) @t156)) % 0.38/1.00 (define @t604 () (forall (@list @t165) @t166)) % 0.38/1.00 (define @t605 () (forall (@list @t157) @t158)) % 0.38/1.00 (define @t606 () (not @t605)) % 0.38/1.00 (define @t607 () (forall (@list @t163) @t164)) % 0.38/1.00 (define @t608 () (forall (@list @t145) @t146)) % 0.38/1.00 (define @t609 () (forall (@list @t151) @t152)) % 0.38/1.00 (define @t610 () (not @t609)) % 0.38/1.00 (define @t611 () (forall (@list @t173) @t174)) % 0.38/1.00 (define @t612 () (not @t611)) % 0.38/1.00 (define @t613 () (forall (@list @t135) @t136)) % 0.38/1.00 (assume @p1 @t3) % 0.38/1.00 (assume @p2 (not @t4)) % 0.38/1.00 (assume @p3 (not @t5)) % 0.38/1.00 (assume @p4 (not @t6)) % 0.38/1.00 (assume @p5 (not (tptp.samehouse tptp.n1 tptp.n5))) % 0.38/1.00 (assume @p6 (not @t7)) % 0.38/1.00 (assume @p7 (not @t8)) % 0.38/1.00 (assume @p8 (not (tptp.samehouse tptp.n2 tptp.n5))) % 0.38/1.00 (assume @p9 (not @t9)) % 0.38/1.00 (assume @p10 (not @t10)) % 0.38/1.00 (assume @p11 (not @t11)) % 0.38/1.00 (assume @p12 (forall @t2 (tptp.sameperson @t1 @t1))) % 0.38/1.00 (assume @p13 (not (tptp.sameperson tptp.englishman tptp.italian))) % 0.38/1.00 (assume @p14 (not (tptp.sameperson tptp.englishman tptp.swede))) % 0.38/1.00 (assume @p15 (not @t12)) % 0.38/1.00 (assume @p16 (not @t13)) % 0.38/1.00 (assume @p17 (not (tptp.sameperson tptp.italian tptp.swede))) % 0.38/1.00 (assume @p18 (not (tptp.sameperson tptp.italian tptp.russian))) % 0.38/1.00 (assume @p19 (not (tptp.sameperson tptp.italian tptp.american))) % 0.38/1.00 (assume @p20 (not @t14)) % 0.38/1.00 (assume @p21 (not @t15)) % 0.38/1.00 (assume @p22 (not (tptp.sameperson tptp.russian tptp.american))) % 0.38/1.00 (assume @p23 (forall @t2 (tptp.samecolor @t1 @t1))) % 0.38/1.00 (assume @p24 (not @t16)) % 0.38/1.00 (assume @p25 (not (tptp.samecolor tptp.red tptp.green))) % 0.38/1.00 (assume @p26 (not (tptp.samecolor tptp.red tptp.yellow))) % 0.38/1.00 (assume @p27 (not @t17)) % 0.38/1.00 (assume @p28 (not (tptp.samecolor tptp.white tptp.green))) % 0.38/1.00 (assume @p29 (not (tptp.samecolor tptp.white tptp.yellow))) % 0.38/1.00 (assume @p30 (not @t18)) % 0.38/1.00 (assume @p31 (not (tptp.samecolor tptp.green tptp.yellow))) % 0.38/1.00 (assume @p32 (not @t19)) % 0.38/1.00 (assume @p33 (not (tptp.samecolor tptp.yellow tptp.blue))) % 0.38/1.00 (assume @p34 (forall @t2 (tptp.samedrink @t1 @t1))) % 0.38/1.00 (assume @p35 (not (tptp.samedrink tptp.lemonade tptp.coffee))) % 0.38/1.00 (assume @p36 (not @t20)) % 0.38/1.00 (assume @p37 (not @t21)) % 0.38/1.00 (assume @p38 (not (tptp.samedrink tptp.lemonade tptp.unknown_drink))) % 0.38/1.00 (assume @p39 (not @t22)) % 0.38/1.00 (assume @p40 (not @t23)) % 0.38/1.00 (assume @p41 (not (tptp.samedrink tptp.coffee tptp.unknown_drink))) % 0.38/1.00 (assume @p42 (not @t24)) % 0.38/1.00 (assume @p43 (not (tptp.samedrink tptp.milk tptp.unknown_drink))) % 0.38/1.00 (assume @p44 (not (tptp.samedrink tptp.vodka tptp.unknown_drink))) % 0.38/1.00 (assume @p45 (forall @t2 (tptp.samegame @t1 @t1))) % 0.38/1.00 (assume @p46 (not @t25)) % 0.38/1.00 (assume @p47 (not (tptp.samegame tptp.backgammon tptp.quoits))) % 0.38/1.00 (assume @p48 (not @t26)) % 0.38/1.00 (assume @p49 (not (tptp.samegame tptp.backgammon tptp.charades))) % 0.38/1.00 (assume @p50 (not (tptp.samegame tptp.racquetball tptp.quoits))) % 0.38/1.00 (assume @p51 (not @t27)) % 0.38/1.00 (assume @p52 (not (tptp.samegame tptp.racquetball tptp.charades))) % 0.38/1.00 (assume @p53 (not (tptp.samegame tptp.quoits tptp.solitaire))) % 0.38/1.00 (assume @p54 (not (tptp.samegame tptp.quoits tptp.charades))) % 0.38/1.00 (assume @p55 (not @t28)) % 0.38/1.00 (assume @p56 (forall @t2 (tptp.samepet @t1 @t1))) % 0.38/1.00 (assume @p57 (not @t29)) % 0.38/1.00 (assume @p58 (not (tptp.samepet tptp.guppy tptp.camel))) % 0.38/1.00 (assume @p59 (not @t30)) % 0.38/1.00 (assume @p60 (not (tptp.samepet tptp.guppy tptp.no_pet))) % 0.38/1.00 (assume @p61 (not @t31)) % 0.38/1.00 (assume @p62 (not @t32)) % 0.38/1.00 (assume @p63 (not (tptp.samepet tptp.toad tptp.no_pet))) % 0.38/1.00 (assume @p64 (not @t33)) % 0.38/1.00 (assume @p65 (not (tptp.samepet tptp.camel tptp.no_pet))) % 0.38/1.00 (assume @p66 (not (tptp.samepet tptp.rat tptp.no_pet))) % 0.38/1.00 (assume @p67 @t38) % 0.38/1.00 (assume @p68 (forall @t37 (or @t41 (not @t39)))) % 0.38/1.00 (assume @p69 (forall @t37 (or @t36 @t40 @t39))) % 0.38/1.00 (assume @p70 @t42) % 0.38/1.00 (assume @p71 (forall @t37 (or (not (tptp.samehouse @t1 @t34)) @t36))) % 0.38/1.00 (assume @p72 (forall @t2 (not (tptp.left @t1 @t1)))) % 0.38/1.00 (assume @p73 @t43) % 0.38/1.00 (assume @p74 (forall @t2 (or @t48 @t47 @t46 @t45 @t44))) % 0.38/1.00 (assume @p75 (forall @t49 (or (tptp.hasperson tptp.n1 @t34) (tptp.hasperson tptp.n2 @t34) (tptp.hasperson tptp.n3 @t34) (tptp.hasperson tptp.n4 @t34) (tptp.hasperson tptp.n5 @t34)))) % 0.38/1.00 (assume @p76 @t55) % 0.38/1.00 (assume @p77 (forall @t49 (or (tptp.hascolor tptp.n1 @t34) (tptp.hascolor tptp.n2 @t34) (tptp.hascolor tptp.n3 @t34) (tptp.hascolor tptp.n4 @t34) (tptp.hascolor tptp.n5 @t34)))) % 0.38/1.00 (assume @p78 @t59) % 0.38/1.00 (assume @p79 @t60) % 0.38/1.00 (assume @p80 @t66) % 0.38/1.00 (assume @p81 (forall @t49 (or (tptp.hasgame tptp.n1 @t34) (tptp.hasgame tptp.n2 @t34) (tptp.hasgame tptp.n3 @t34) (tptp.hasgame tptp.n4 @t34) (tptp.hasgame tptp.n5 @t34)))) % 0.38/1.00 (assume @p82 (forall @t2 (or @t70 @t69 @t68 @t67 (tptp.haspet @t1 tptp.no_pet)))) % 0.38/1.00 (assume @p83 (forall @t49 (or (tptp.haspet tptp.n1 @t34) (tptp.haspet tptp.n2 @t34) (tptp.haspet tptp.n3 @t34) (tptp.haspet tptp.n4 @t34) (tptp.haspet tptp.n5 @t34)))) % 0.38/1.00 (assume @p84 (forall @t74 (or @t73 (not (tptp.hascolor @t72 @t34)) (not (tptp.hascolor @t71 @t34))))) % 0.38/1.00 (assume @p85 (forall @t74 (or @t73 (not (tptp.hasperson @t72 @t34)) (not (tptp.hasperson @t71 @t34))))) % 0.38/1.00 (assume @p86 @t75) % 0.38/1.00 (assume @p87 @t76) % 0.38/1.00 (assume @p88 (forall @t74 (or @t73 (not (tptp.haspet @t72 @t34)) (not (tptp.haspet @t71 @t34))))) % 0.38/1.00 (assume @p89 @t77) % 0.38/1.00 (assume @p90 @t78) % 0.38/1.00 (assume @p91 @t79) % 0.38/1.00 (assume @p92 (forall @t74 (or (tptp.samegame @t72 @t71) (not (tptp.hasgame @t34 @t72)) (not (tptp.hasgame @t34 @t71))))) % 0.38/1.00 (assume @p93 @t80) % 0.38/1.00 (assume @p94 (forall @t2 (or (not @t48) @t54))) % 0.38/1.00 (assume @p95 @t81) % 0.38/1.00 (assume @p96 (forall @t37 (or @t84 @t83 @t40))) % 0.38/1.00 (assume @p97 @t85) % 0.38/1.00 (assume @p98 (forall @t37 (or @t53 @t83 @t41))) % 0.38/1.00 (assume @p99 (forall @t2 (or (not @t47) @t70))) % 0.38/1.00 (assume @p100 (forall @t2 (or @t47 (not @t70)))) % 0.38/1.00 (assume @p101 @t86) % 0.38/1.00 (assume @p102 (forall @t2 (or @t58 (not @t52)))) % 0.38/1.00 (assume @p103 @t87) % 0.38/1.00 (assume @p104 (forall @t2 (or @t46 (not @t57)))) % 0.38/1.00 (assume @p105 (forall @t2 (or (not @t69) @t65))) % 0.38/1.00 (assume @p106 @t88) % 0.38/1.00 (assume @p107 (forall @t2 (or @t89 @t51))) % 0.38/1.00 (assume @p108 @t90) % 0.38/1.00 (assume @p109 (forall @t96 (or @t95 @t94 @t36 @t93 @t92 (tptp.hasgame @t91 tptp.quoits)))) % 0.38/1.00 (assume @p110 (forall @t37 (or @t95 @t97 @t36 @t92))) % 0.38/1.00 (assume @p111 (forall @t37 (or @t95 @t98 @t36 @t92))) % 0.38/1.00 (assume @p112 @t99) % 0.38/1.00 (assume @p113 @t103) % 0.38/1.00 (assume @p114 (forall @t37 (or @t97 @t36 @t101 @t100))) % 0.38/1.00 (assume @p115 (forall @t37 (or @t98 @t36 @t101 @t100))) % 0.38/1.00 (assume @p116 (forall @t96 (or @t105 @t94 @t36 @t93 @t104 (tptp.hasgame @t91 tptp.racquetball)))) % 0.38/1.00 (assume @p117 (forall @t37 (or @t105 @t36 @t97 @t104))) % 0.38/1.00 (assume @p118 (forall @t37 (or @t105 @t36 @t98 @t104))) % 0.38/1.00 (assume @p119 (forall @t37 (or @t105 @t35 (not @t104)))) % 0.38/1.00 (assume @p120 (forall @t102 (or @t94 @t36 @t93 @t89 @t106 (tptp.haspet @t91 tptp.rat)))) % 0.38/1.00 (assume @p121 @t107) % 0.38/1.00 (assume @p122 (forall @t37 (or @t36 @t98 @t89 @t106))) % 0.38/1.00 (assume @p123 (forall @t2 (or (not @t62) @t56))) % 0.38/1.00 (assume @p124 @t108) % 0.38/1.00 (assume @p125 (forall @t2 (or (not @t44) @t61))) % 0.38/1.00 (assume @p126 (forall @t2 (or @t44 (not @t61)))) % 0.38/1.00 (assume @p127 (forall @t96 (or @t110 @t94 @t36 @t93 @t109 (tptp.hascolor @t91 tptp.blue)))) % 0.38/1.00 (assume @p128 @t111) % 0.38/1.00 (assume @p129 (forall @t37 (or @t110 @t98 @t36 @t109))) % 0.38/1.00 (assume @p130 @t112) % 0.38/1.00 (assume @p131 (forall @t102 (or @t94 @t36 @t93 @t114 @t113 (tptp.hasperson @t91 tptp.russian)))) % 0.38/1.00 (assume @p132 (forall @t37 (or @t36 @t114 @t97 @t113))) % 0.38/1.00 (assume @p133 (forall @t37 (or @t36 @t114 @t98 @t113))) % 0.38/1.00 (assume @p134 (forall @t2 (not (tptp.left @t1 tptp.n1)))) % 0.38/1.00 (assume @p135 (forall @t2 (not (tptp.left tptp.n5 @t1)))) % 0.38/1.00 (assume @p136 @t115) % 0.38/1.00 (assume @p137 @t116) % 0.38/1.00 (assume @p138 @t117) % 0.38/1.00 (assume @p139 @t118) % 0.38/1.00 (assume @p140 (not @t119)) % 0.38/1.00 (assume @p141 (not @t120)) % 0.38/1.00 (assume @p142 (not @t121)) % 0.38/1.00 (assume @p143 (not @t122)) % 0.38/1.00 (assume @p144 (not @t123)) % 0.38/1.00 (assume @p145 (not @t124)) % 0.38/1.00 (assume @p146 @t125) % 0.38/1.00 (assume @p147 @t126) % 0.38/1.00 (assume @p148 @t175) % 0.38/1.00 (step @p149 :rule instantiate :premises (@p101) :args (@t176)) % 0.38/1.00 (step @p150 :rule instantiate :premises (@p98) :args (@t177)) % 0.38/1.00 (step @p151 :rule cnf_or_pos :args (@t182)) % 0.38/1.00 (step @p152 :rule reordering :premises (@p151) :args ((or @t178 @t181 @t180 (not @t182)))) % 0.38/1.00 (step @p153 :rule instantiate :premises (@p68) :args (@t183)) % 0.38/1.00 (step @p154 :rule cnf_or_pos :args (@t187)) % 0.38/1.00 (step @p155 :rule reordering :premises (@p154) :args ((or @t186 @t185 (not @t187)))) % 0.38/1.00 (step @p156 :rule chain_m_resolution :premises (@p155 @p139 @p153) :args (@t185 @t188 (@list @t118 @t187))) % 0.38/1.00 (step @p157 :rule instantiate :premises (@p96) :args (@t189)) % 0.38/1.00 (step @p158 :rule cnf_or_pos :args (@t192)) % 0.38/1.00 (step @p159 :rule reordering :premises (@p158) :args ((or @t184 @t180 @t191 (not @t192)))) % 0.38/1.00 (step @p160 :rule instantiate :premises (@p123) :args (@t193)) % 0.38/1.00 (step @p161 :rule instantiate :premises (@p91) :args ((@list tptp.coffee tptp.vodka tptp.n2))) % 0.38/1.00 (step @p162 :rule instantiate :premises (@p103) :args (@t193)) % 0.38/1.00 (step @p163 :rule instantiate :premises (@p74) :args (@t193)) % 0.38/1.00 (step @p164 :rule instantiate :premises (@p125) :args (@t193)) % 0.38/1.00 (step @p165 :rule instantiate :premises (@p92) :args ((@list tptp.solitaire tptp.charades tptp.n2))) % 0.38/1.00 (step @p166 :rule cnf_or_pos :args (@t198)) % 0.38/1.00 (step @p167 :rule reordering :premises (@p166) :args ((or @t28 @t197 @t195 (not @t198)))) % 0.38/1.00 (step @p168 :rule instantiate :premises (@p126) :args (@t193)) % 0.38/1.00 (step @p169 :rule cnf_or_pos :args (@t200)) % 0.38/1.00 (step @p170 :rule reordering :premises (@p169) :args ((or @t199 @t195 (not @t200)))) % 0.38/1.00 (step @p171 :rule instantiate :premises (@p124) :args (@t193)) % 0.38/1.00 (step @p172 :rule cnf_or_pos :args (@t203)) % 0.38/1.00 (step @p173 :rule reordering :premises (@p172) :args ((or @t202 @t196 (not @t203)))) % 0.38/1.00 (step @p174 :rule instantiate :premises (@p89) :args ((@list tptp.swede tptp.american tptp.n2))) % 0.38/1.00 (step @p175 :rule cnf_or_pos :args (@t207)) % 0.38/1.00 (step @p176 :rule reordering :premises (@p175) :args ((or @t15 @t206 @t204 (not @t207)))) % 0.38/1.00 (step @p177 :rule instantiate :premises (@p86) :args ((@list tptp.n1 tptp.n2 tptp.unknown_drink))) % 0.38/1.00 (step @p178 :rule instantiate :premises (@p70) :args (@t208)) % 0.38/1.00 (step @p179 :rule instantiate :premises (@p67) :args (@t208)) % 0.38/1.00 (step @p180 :rule cnf_or_pos :args (@t211)) % 0.38/1.00 (step @p181 :rule reordering :premises (@p180) :args ((or @t121 @t210 (not @t211)))) % 0.38/1.00 (step @p182 :rule chain_m_resolution :premises (@p181 @p142 @p179) :args (@t210 @t212 (@list @t121 @t211))) % 0.38/1.00 (step @p183 :rule cnf_or_pos :args (@t215)) % 0.38/1.00 (step @p184 :rule reordering :premises (@p183) :args ((or @t209 @t214 (not @t215)))) % 0.38/1.00 (step @p185 :rule chain_m_resolution :premises (@p184 @p182 @p178) :args (@t214 @t212 (@list @t209 @t215))) % 0.38/1.00 (step @p186 :rule instantiate :premises (@p96) :args (@t208)) % 0.38/1.00 (step @p187 :rule cnf_or_pos :args (@t218)) % 0.38/1.00 (step @p188 :rule reordering :premises (@p187) :args ((or @t213 @t217 @t191 (not @t218)))) % 0.38/1.00 (step @p189 :rule instantiate :premises (@p70) :args (@t219)) % 0.38/1.00 (step @p190 :rule instantiate :premises (@p67) :args (@t219)) % 0.38/1.00 (step @p191 :rule cnf_or_pos :args (@t222)) % 0.38/1.00 (step @p192 :rule reordering :premises (@p191) :args ((or @t119 @t221 (not @t222)))) % 0.38/1.00 (step @p193 :rule chain_m_resolution :premises (@p192 @p140 @p190) :args (@t221 @t212 (@list @t119 @t222))) % 0.38/1.00 (step @p194 :rule cnf_or_pos :args (@t225)) % 0.38/1.00 (step @p195 :rule reordering :premises (@p194) :args ((or @t220 @t224 (not @t225)))) % 0.38/1.00 (step @p196 :rule chain_m_resolution :premises (@p195 @p193 @p189) :args (@t224 @t212 (@list @t220 @t225))) % 0.38/1.00 (step @p197 :rule instantiate :premises (@p96) :args (@t219)) % 0.38/1.00 (step @p198 :rule cnf_or_pos :args (@t227)) % 0.38/1.00 (step @p199 :rule reordering :premises (@p198) :args ((or @t226 @t223 @t217 (not @t227)))) % 0.38/1.00 (step @p200 :rule instantiate :premises (@p70) :args (@t228)) % 0.38/1.00 (step @p201 :rule instantiate :premises (@p67) :args (@t228)) % 0.38/1.00 (step @p202 :rule cnf_or_pos :args (@t231)) % 0.38/1.00 (step @p203 :rule reordering :premises (@p202) :args ((or @t120 @t230 (not @t231)))) % 0.38/1.00 (step @p204 :rule chain_m_resolution :premises (@p203 @p141 @p201) :args (@t230 @t212 (@list @t120 @t231))) % 0.38/1.00 (step @p205 :rule cnf_or_pos :args (@t234)) % 0.38/1.00 (step @p206 :rule reordering :premises (@p205) :args ((or @t229 @t233 (not @t234)))) % 0.38/1.00 (step @p207 :rule chain_m_resolution :premises (@p206 @p204 @p200) :args (@t233 @t212 (@list @t229 @t234))) % 0.38/1.00 (step @p208 :rule instantiate :premises (@p96) :args (@t228)) % 0.38/1.00 (step @p209 :rule cnf_or_pos :args (@t237)) % 0.38/1.00 (step @p210 :rule reordering :premises (@p209) :args ((or @t236 @t232 @t217 (not @t237)))) % 0.38/1.00 (step @p211 :rule instantiate :premises (@p90) :args ((@list tptp.white tptp.blue tptp.n2))) % 0.38/1.00 (step @p212 :rule instantiate :premises (@p128) :args (@t238)) % 0.38/1.00 (step @p213 :rule instantiate :premises (@p1) :args (@t239)) % 0.38/1.00 (step @p214 :rule instantiate :premises (@p70) :args (@t238)) % 0.38/1.00 (step @p215 :rule cnf_or_pos :args (@t242)) % 0.38/1.00 (step @p216 :rule reordering :premises (@p215) :args ((or @t241 @t240 (not @t242)))) % 0.38/1.00 (step @p217 :rule chain_m_resolution :premises (@p216 @p136 @p214) :args (@t240 @t188 (@list @t115 @t242))) % 0.38/1.00 (step @p218 :rule cnf_or_pos :args (@t248)) % 0.38/1.00 (step @p219 :rule reordering :premises (@p218) :args ((or @t247 @t244 @t243 @t246 (not @t248)))) % 0.38/1.00 (step @p220 :rule chain_m_resolution :premises (@p219 @p147 @p217 @p213 @p212) :args (@t243 @t249 (@list @t126 @t240 @t245 @t248))) % 0.38/1.00 (step @p221 :rule cnf_or_pos :args (@t253)) % 0.38/1.00 (step @p222 :rule reordering :premises (@p221) :args ((or @t18 @t252 @t250 (not @t253)))) % 0.38/1.00 (step @p223 :rule chain_m_resolution :premises (@p222 @p30 @p220 @p211) :args (@t252 @t254 (@list @t18 @t243 @t253))) % 0.38/1.00 (step @p224 :rule instantiate :premises (@p97) :args (@t238)) % 0.38/1.00 (step @p225 :rule instantiate :premises (@p90) :args ((@list tptp.green tptp.blue tptp.n2))) % 0.38/1.00 (step @p226 :rule cnf_or_pos :args (@t257)) % 0.38/1.00 (step @p227 :rule reordering :premises (@p226) :args ((or @t19 @t256 @t250 (not @t257)))) % 0.38/1.00 (step @p228 :rule chain_m_resolution :premises (@p227 @p32 @p220 @p225) :args (@t256 @t254 (@list @t19 @t243 @t257))) % 0.38/1.00 (step @p229 :rule cnf_or_pos :args (@t260)) % 0.38/1.00 (step @p230 :rule reordering :premises (@p229) :args ((or @t241 @t259 @t255 (not @t260)))) % 0.38/1.00 (step @p231 :rule chain_m_resolution :premises (@p230 @p136 @p228 @p224) :args (@t259 @t261 (@list @t115 @t255 @t260))) % 0.38/1.00 (step @p232 :rule instantiate :premises (@p77) :args (@t262)) % 0.38/1.00 (step @p233 :rule cnf_or_pos :args (@t263)) % 0.38/1.00 (step @p234 :rule reordering :premises (@p233) :args ((or @t258 @t251 @t181 @t235 @t190 (not @t263)))) % 0.38/1.00 (step @p235 :rule chain_m_resolution :premises (@p234 @p232 @p231 @p223 @p210 @p208 @p207 @p199 @p197 @p196 @p188 @p186 @p185) :args (@t217 (@list false true true true false true true false true true false true) (@list @t263 @t258 @t251 @t235 @t237 @t232 @t181 @t227 @t223 @t190 @t218 @t213))) % 0.38/1.00 (step @p236 :rule instantiate :premises (@p101) :args (@t239)) % 0.38/1.00 (step @p237 :rule cnf_or_pos :args (@t266)) % 0.38/1.00 (step @p238 :rule reordering :premises (@p237) :args ((or @t216 @t265 (not @t266)))) % 0.38/1.00 (step @p239 :rule instantiate :premises (@p130) :args ((@list tptp.n1 tptp.n1))) % 0.38/1.00 (step @p240 :rule instantiate :premises (@p73) :args (@t239)) % 0.38/1.00 (step @p241 :rule cnf_or_pos :args (@t270)) % 0.38/1.00 (step @p242 :rule reordering :premises (@p241) :args ((or @t247 @t269 @t268 (not @t270)))) % 0.38/1.00 (step @p243 :rule chain_m_resolution :premises (@p242 @p147 @p240 @p239) :args (@t268 @t261 (@list @t126 @t269 @t270))) % 0.38/1.00 (step @p244 :rule instantiate :premises (@p76) :args (@t239)) % 0.38/1.00 (step @p245 :rule instantiate :premises (@p95) :args (@t239)) % 0.38/1.00 (step @p246 :rule instantiate :premises (@p89) :args ((@list tptp.englishman tptp.russian tptp.n1))) % 0.38/1.00 (step @p247 :rule cnf_or_pos :args (@t273)) % 0.38/1.00 (step @p248 :rule reordering :premises (@p247) :args ((or @t12 @t247 @t272 (not @t273)))) % 0.38/1.00 (step @p249 :rule chain_m_resolution :premises (@p248 @p15 @p147 @p246) :args (@t272 @t254 (@list @t12 @t126 @t273))) % 0.38/1.00 (step @p250 :rule cnf_or_pos :args (@t276)) % 0.38/1.00 (step @p251 :rule reordering :premises (@p250) :args ((or @t275 @t271 (not @t276)))) % 0.38/1.00 (step @p252 :rule chain_m_resolution :premises (@p251 @p249 @p245) :args (@t275 @t212 (@list @t271 @t276))) % 0.38/1.00 (step @p253 :rule cnf_or_pos :args (@t278)) % 0.38/1.00 (step @p254 :rule reordering :premises (@p253) :args ((or @t258 @t267 @t274 @t216 @t277 (not @t278)))) % 0.38/1.00 (step @p255 :rule instantiate :premises (@p78) :args (@t239)) % 0.38/1.00 (step @p256 :rule instantiate :premises (@p86) :args ((@list tptp.n1 tptp.n3 tptp.milk))) % 0.38/1.00 (step @p257 :rule cnf_or_pos :args (@t282)) % 0.38/1.00 (step @p258 :rule reordering :premises (@p257) :args ((or @t5 @t279 @t281 (not @t282)))) % 0.38/1.00 (step @p259 :rule chain_m_resolution :premises (@p258 @p3 @p146 @p256) :args (@t281 @t254 (@list @t5 @t125 @t282))) % 0.38/1.00 (step @p260 :rule instantiate :premises (@p104) :args (@t239)) % 0.38/1.00 (step @p261 :rule instantiate :premises (@p89) :args ((@list tptp.swede tptp.russian tptp.n1))) % 0.38/1.00 (step @p262 :rule cnf_or_pos :args (@t285)) % 0.38/1.00 (step @p263 :rule reordering :premises (@p262) :args ((or @t14 @t247 @t284 (not @t285)))) % 0.38/1.00 (step @p264 :rule chain_m_resolution :premises (@p263 @p20 @p147 @p261) :args (@t284 @t254 (@list @t14 @t126 @t285))) % 0.38/1.00 (step @p265 :rule cnf_or_pos :args (@t288)) % 0.38/1.00 (step @p266 :rule reordering :premises (@p265) :args ((or @t283 @t287 (not @t288)))) % 0.38/1.00 (step @p267 :rule chain_m_resolution :premises (@p266 @p264 @p260) :args (@t287 @t212 (@list @t283 @t288))) % 0.38/1.00 (step @p268 :rule cnf_or_pos :args (@t291)) % 0.38/1.00 (step @p269 :rule reordering :premises (@p268) :args ((or @t290 @t264 @t286 @t280 @t289 (not @t291)))) % 0.38/1.00 (step @p270 :rule instantiate :premises (@p108) :args (@t239)) % 0.38/1.00 (step @p271 :rule cnf_or_pos :args (@t294)) % 0.38/1.00 (step @p272 :rule reordering :premises (@p271) :args ((or @t293 @t292 (not @t294)))) % 0.38/1.00 (step @p273 :rule instantiate :premises (@p124) :args (@t239)) % 0.38/1.00 (step @p274 :rule cnf_or_pos :args (@t297)) % 0.38/1.00 (step @p275 :rule reordering :premises (@p274) :args ((or @t295 @t296 (not @t297)))) % 0.38/1.00 (step @p276 :rule instantiate :premises (@p92) :args ((@list tptp.racquetball tptp.solitaire tptp.n1))) % 0.38/1.00 (step @p277 :rule cnf_or_pos :args (@t300)) % 0.38/1.00 (step @p278 :rule reordering :premises (@p277) :args ((or @t27 @t299 @t298 (not @t300)))) % 0.38/1.00 (step @p279 :rule chain_m_resolution :premises (@p278 @p276 @p51 @p275 @p273 @p272 @p270 @p269 @p267 @p259 @p255 @p254 @p252 @p244 @p231 @p243 @p238 @p236) :args ((or @t216 @t289) (@list false true false false false false false true true false false true false true true true false) (@list @t300 @t27 @t296 @t297 @t293 @t294 @t290 @t286 @t280 @t291 @t277 @t274 @t278 @t258 @t267 @t264 @t266))) % 0.38/1.00 (step @p280 :rule chain_m_resolution :premises (@p279 @p235) :args (@t289 @t301 (@list @t216))) % 0.38/1.00 (step @p281 :rule cnf_or_pos :args (@t305)) % 0.38/1.00 (step @p282 :rule reordering :premises (@p281) :args ((or @t4 @t303 @t304 (not @t305)))) % 0.38/1.00 (step @p283 :rule chain_m_resolution :premises (@p282 @p2 @p280 @p177) :args (@t303 @t254 (@list @t4 @t289 @t305))) % 0.38/1.00 (step @p284 :rule instantiate :premises (@p86) :args ((@list tptp.n2 tptp.n3 tptp.milk))) % 0.38/1.00 (step @p285 :rule cnf_or_pos :args (@t308)) % 0.38/1.00 (step @p286 :rule reordering :premises (@p285) :args ((or @t7 @t279 @t307 (not @t308)))) % 0.38/1.00 (step @p287 :rule chain_m_resolution :premises (@p286 @p6 @p146 @p284) :args (@t307 @t254 (@list @t7 @t125 @t308))) % 0.38/1.00 (step @p288 :rule instantiate :premises (@p78) :args (@t193)) % 0.38/1.00 (step @p289 :rule instantiate :premises (@p101) :args (@t193)) % 0.38/1.00 (step @p290 :rule cnf_or_pos :args (@t311)) % 0.38/1.00 (step @p291 :rule reordering :premises (@p290) :args ((or @t255 @t310 (not @t311)))) % 0.38/1.00 (step @p292 :rule chain_m_resolution :premises (@p291 @p228 @p289) :args (@t310 @t212 (@list @t255 @t311))) % 0.38/1.00 (step @p293 :rule cnf_or_pos :args (@t313)) % 0.38/1.00 (step @p294 :rule reordering :premises (@p293) :args ((or @t201 @t309 @t312 @t306 @t302 (not @t313)))) % 0.38/1.00 (step @p295 :rule instantiate :premises (@p104) :args (@t193)) % 0.38/1.00 (step @p296 :rule cnf_or_pos :args (@t315)) % 0.38/1.00 (step @p297 :rule reordering :premises (@p296) :args ((or @t205 @t314 (not @t315)))) % 0.38/1.00 (step @p298 :rule chain_m_resolution :premises (@p297 @p295 @p294 @p292 @p288 @p287 @p283 @p176 @p174 @p21 @p173 @p171 @p170 @p168 @p167 @p165 @p55) :args (@t195 (@list false false true false true true true false true true false false false true false true) (@list @t315 @t312 @t309 @t313 @t306 @t302 @t205 @t207 @t15 @t201 @t203 @t199 @t200 @t196 @t198 @t28))) % 0.38/1.00 (step @p299 :rule cnf_or_pos :args (@t316)) % 0.38/1.00 (step @p300 :rule reordering :premises (@p299) :args ((or @t204 @t194 (not @t316)))) % 0.38/1.00 (step @p301 :rule chain_m_resolution :premises (@p300 @p298 @p164) :args (@t204 @t212 (@list @t194 @t316))) % 0.38/1.00 (step @p302 :rule instantiate :premises (@p99) :args (@t193)) % 0.38/1.00 (step @p303 :rule instantiate :premises (@p93) :args ((@list tptp.guppy tptp.rat tptp.n2))) % 0.38/1.00 (step @p304 :rule instantiate :premises (@p121) :args (@t238)) % 0.38/1.00 (step @p305 :rule chain_m_resolution :premises (@p254 @p231 @p243 @p252 @p235 @p244) :args (@t277 @t317 (@list @t258 @t267 @t274 @t216 @t278))) % 0.38/1.00 (step @p306 :rule chain_m_resolution :premises (@p272 @p305 @p270) :args (@t293 @t188 (@list @t277 @t294))) % 0.38/1.00 (step @p307 :rule cnf_or_pos :args (@t319)) % 0.38/1.00 (step @p308 :rule reordering :premises (@p307) :args ((or @t318 @t244 @t246 @t299 (not @t319)))) % 0.38/1.00 (step @p309 :rule chain_m_resolution :premises (@p308 @p217 @p213 @p306 @p304) :args (@t318 @t249 (@list @t240 @t245 @t293 @t319))) % 0.38/1.00 (step @p310 :rule cnf_or_pos :args (@t323)) % 0.38/1.00 (step @p311 :rule reordering :premises (@p310) :args ((or @t30 @t320 @t322 (not @t323)))) % 0.38/1.00 (step @p312 :rule chain_m_resolution :premises (@p311 @p59 @p309 @p303) :args (@t322 @t254 (@list @t30 @t318 @t323))) % 0.38/1.00 (step @p313 :rule cnf_or_pos :args (@t326)) % 0.38/1.00 (step @p314 :rule reordering :premises (@p313) :args ((or @t321 @t325 (not @t326)))) % 0.38/1.00 (step @p315 :rule chain_m_resolution :premises (@p314 @p312 @p302) :args (@t325 @t212 (@list @t321 @t326))) % 0.38/1.00 (step @p316 :rule instantiate :premises (@p94) :args (@t193)) % 0.38/1.00 (step @p317 :rule instantiate :premises (@p90) :args ((@list tptp.red tptp.blue tptp.n2))) % 0.38/1.00 (step @p318 :rule cnf_or_pos :args (@t329)) % 0.38/1.00 (step @p319 :rule reordering :premises (@p318) :args ((or @t17 @t250 @t328 (not @t329)))) % 0.38/1.00 (step @p320 :rule chain_m_resolution :premises (@p319 @p27 @p220 @p317) :args (@t328 @t254 (@list @t17 @t243 @t329))) % 0.38/1.00 (step @p321 :rule cnf_or_pos :args (@t332)) % 0.38/1.00 (step @p322 :rule reordering :premises (@p321) :args ((or @t327 @t331 (not @t332)))) % 0.38/1.00 (step @p323 :rule chain_m_resolution :premises (@p322 @p320 @p316) :args (@t331 @t212 (@list @t327 @t332))) % 0.38/1.00 (step @p324 :rule instantiate :premises (@p85) :args ((@list tptp.n1 tptp.n2 tptp.russian))) % 0.38/1.00 (step @p325 :rule cnf_or_pos :args (@t335)) % 0.38/1.00 (step @p326 :rule reordering :premises (@p325) :args ((or @t4 @t247 @t334 (not @t335)))) % 0.38/1.00 (step @p327 :rule chain_m_resolution :premises (@p326 @p2 @p147 @p324) :args (@t334 @t254 (@list @t4 @t126 @t335))) % 0.38/1.00 (step @p328 :rule cnf_or_pos :args (@t336)) % 0.38/1.00 (step @p329 :rule reordering :premises (@p328) :args ((or @t333 @t330 @t324 @t205 @t199 (not @t336)))) % 0.38/1.00 (step @p330 :rule chain_m_resolution :premises (@p329 @p327 @p323 @p315 @p301 @p163) :args (@t205 @t317 (@list @t333 @t330 @t324 @t199 @t336))) % 0.38/1.00 (step @p331 :rule cnf_or_pos :args (@t337)) % 0.38/1.00 (step @p332 :rule reordering :premises (@p331) :args ((or @t206 @t312 (not @t337)))) % 0.38/1.00 (step @p333 :rule chain_m_resolution :premises (@p332 @p330 @p162) :args (@t312 @t188 (@list @t205 @t337))) % 0.38/1.00 (step @p334 :rule cnf_or_pos :args (@t338)) % 0.38/1.00 (step @p335 :rule reordering :premises (@p334) :args ((or @t23 @t202 @t314 (not @t338)))) % 0.38/1.00 (step @p336 :rule chain_m_resolution :premises (@p335 @p40 @p333 @p161) :args (@t202 @t254 (@list @t23 @t312 @t338))) % 0.38/1.00 (step @p337 :rule cnf_or_pos :args (@t339)) % 0.38/1.00 (step @p338 :rule reordering :premises (@p337) :args ((or @t201 @t197 (not @t339)))) % 0.38/1.00 (step @p339 :rule chain_m_resolution :premises (@p338 @p336 @p160) :args (@t197 @t212 (@list @t201 @t339))) % 0.38/1.00 (assume-push @p941 @t108) % 0.38/1.00 (step-pop @p942 :rule scope :premises (@p171)) % 0.38/1.00 (step @p341 :rule process_scope :premises (@p942) :args (@t203)) % 0.38/1.00 (step @p343 :rule implies_elim :premises (@p341)) % 0.38/1.00 (assume-push @p943 @t78) % 0.38/1.00 (step-pop @p944 :rule scope :premises (@p225)) % 0.38/1.00 (step @p345 :rule process_scope :premises (@p944) :args (@t257)) % 0.38/1.00 (step @p347 :rule implies_elim :premises (@p345)) % 0.38/1.00 (assume-push @p945 @t3) % 0.38/1.00 (step-pop @p946 :rule scope :premises (@p213)) % 0.38/1.00 (step @p349 :rule process_scope :premises (@p946) :args (@t245)) % 0.38/1.00 (step @p351 :rule implies_elim :premises (@p349)) % 0.38/1.00 (assume-push @p947 @t111) % 0.38/1.00 (step-pop @p948 :rule scope :premises (@p212)) % 0.38/1.00 (step @p353 :rule process_scope :premises (@p948) :args (@t248)) % 0.38/1.00 (step @p355 :rule implies_elim :premises (@p353)) % 0.38/1.00 (assume-push @p949 @t42) % 0.38/1.00 (step-pop @p950 :rule scope :premises (@p214)) % 0.38/1.00 (step @p357 :rule process_scope :premises (@p950) :args (@t242)) % 0.38/1.00 (step @p359 :rule implies_elim :premises (@p357)) % 0.38/1.00 (assume-push @p951 @t86) % 0.38/1.00 (step-pop @p952 :rule scope :premises (@p289)) % 0.38/1.00 (step @p361 :rule process_scope :premises (@p952) :args (@t311)) % 0.38/1.00 (step @p363 :rule implies_elim :premises (@p361)) % 0.38/1.00 (assume-push @p953 @t59) % 0.38/1.00 (step-pop @p954 :rule scope :premises (@p288)) % 0.38/1.00 (step @p365 :rule process_scope :premises (@p954) :args (@t313)) % 0.38/1.00 (step @p367 :rule implies_elim :premises (@p365)) % 0.38/1.00 (assume-push @p955 @t75) % 0.38/1.00 (step-pop @p956 :rule scope :premises (@p284)) % 0.38/1.00 (step @p369 :rule process_scope :premises (@p956) :args (@t308)) % 0.38/1.00 (step @p371 :rule implies_elim :premises (@p369)) % 0.38/1.00 (assume-push @p957 @t75) % 0.38/1.00 (step-pop @p958 :rule scope :premises (@p177)) % 0.38/1.00 (step @p373 :rule process_scope :premises (@p958) :args (@t305)) % 0.38/1.00 (step @p375 :rule implies_elim :premises (@p373)) % 0.38/1.00 (assume-push @p959 @t75) % 0.38/1.00 (step @p377 :rule instantiate :premises (@p86) :args (@t340)) % 0.38/1.00 (step-pop @p960 :rule scope :premises (@p377)) % 0.38/1.00 (step @p378 :rule process_scope :premises (@p960) :args (@t343)) % 0.38/1.00 (step @p380 :rule implies_elim :premises (@p378)) % 0.38/1.00 (step @p381 :rule cnf_or_pos :args (@t343)) % 0.38/1.00 (step @p382 :rule reordering :premises (@p381) :args ((or @t8 @t342 @t314 (not @t343)))) % 0.38/1.00 (assume-push @p961 @t87) % 0.38/1.00 (step @p384 :rule instantiate :premises (@p103) :args (@t176)) % 0.38/1.00 (step-pop @p962 :rule scope :premises (@p384)) % 0.38/1.00 (step @p385 :rule process_scope :premises (@p962) :args (@t346)) % 0.38/1.00 (step @p387 :rule implies_elim :premises (@p385)) % 0.38/1.00 (step @p388 :rule cnf_or_pos :args (@t346)) % 0.38/1.00 (step @p389 :rule reordering :premises (@p388) :args ((or @t341 @t345 (not @t346)))) % 0.38/1.00 (assume-push @p963 @t77) % 0.38/1.00 (step-pop @p964 :rule scope :premises (@p246)) % 0.38/1.00 (step @p391 :rule process_scope :premises (@p964) :args (@t273)) % 0.38/1.00 (step @p393 :rule implies_elim :premises (@p391)) % 0.38/1.00 (assume-push @p965 @t81) % 0.38/1.00 (step-pop @p966 :rule scope :premises (@p245)) % 0.38/1.00 (step @p395 :rule process_scope :premises (@p966) :args (@t276)) % 0.38/1.00 (step @p397 :rule implies_elim :premises (@p395)) % 0.38/1.00 (assume-push @p967 @t55) % 0.38/1.00 (step-pop @p968 :rule scope :premises (@p244)) % 0.38/1.00 (step @p399 :rule process_scope :premises (@p968) :args (@t278)) % 0.38/1.00 (step @p401 :rule implies_elim :premises (@p399)) % 0.38/1.00 (assume-push @p969 @t85) % 0.38/1.00 (step-pop @p970 :rule scope :premises (@p224)) % 0.38/1.00 (step @p403 :rule process_scope :premises (@p970) :args (@t260)) % 0.38/1.00 (step @p405 :rule implies_elim :premises (@p403)) % 0.38/1.00 (assume-push @p971 @t43) % 0.38/1.00 (step-pop @p972 :rule scope :premises (@p240)) % 0.38/1.00 (step @p407 :rule process_scope :premises (@p972) :args ((not @t269))) % 0.38/1.00 (step @p409 :rule implies_elim :premises (@p407)) % 0.38/1.00 (assume-push @p973 @t112) % 0.38/1.00 (step-pop @p974 :rule scope :premises (@p239)) % 0.38/1.00 (step @p411 :rule process_scope :premises (@p974) :args (@t270)) % 0.38/1.00 (step @p413 :rule implies_elim :premises (@p411)) % 0.38/1.00 (assume-push @p975 @t90) % 0.38/1.00 (step-pop @p976 :rule scope :premises (@p270)) % 0.38/1.00 (step @p415 :rule process_scope :premises (@p976) :args (@t294)) % 0.38/1.00 (step @p417 :rule implies_elim :premises (@p415)) % 0.38/1.00 (assume-push @p977 @t107) % 0.38/1.00 (step-pop @p978 :rule scope :premises (@p304)) % 0.38/1.00 (step @p419 :rule process_scope :premises (@p978) :args (@t319)) % 0.38/1.00 (step @p421 :rule implies_elim :premises (@p419)) % 0.38/1.00 (assume-push @p979 @t80) % 0.38/1.00 (step @p423 :rule instantiate :premises (@p93) :args (@t347)) % 0.38/1.00 (step-pop @p980 :rule scope :premises (@p423)) % 0.38/1.00 (step @p424 :rule process_scope :premises (@p980) :args (@t350)) % 0.38/1.00 (step @p426 :rule implies_elim :premises (@p424)) % 0.38/1.00 (step @p427 :rule cnf_or_pos :args (@t350)) % 0.38/1.00 (step @p428 :rule reordering :premises (@p427) :args ((or @t32 @t320 @t349 (not @t350)))) % 0.38/1.00 (assume-push @p981 @t88) % 0.38/1.00 (step @p430 :rule instantiate :premises (@p106) :args (@t193)) % 0.38/1.00 (step-pop @p982 :rule scope :premises (@p430)) % 0.38/1.00 (step @p431 :rule process_scope :premises (@p982) :args (@t353)) % 0.38/1.00 (step @p433 :rule implies_elim :premises (@p431)) % 0.38/1.00 (step @p434 :rule cnf_or_pos :args (@t353)) % 0.38/1.00 (step @p435 :rule reordering :premises (@p434) :args ((or @t348 @t352 (not @t353)))) % 0.38/1.00 (assume-push @p983 @t66) % 0.38/1.00 (step @p437 :rule instantiate :premises (@p80) :args (@t193)) % 0.38/1.00 (step-pop @p984 :rule scope :premises (@p437)) % 0.38/1.00 (step @p438 :rule process_scope :premises (@p984) :args (@t356)) % 0.38/1.00 (step @p440 :rule implies_elim :premises (@p438)) % 0.38/1.00 (assume-push @p985 @t76) % 0.38/1.00 (step @p442 :rule instantiate :premises (@p87) :args (@t357)) % 0.38/1.00 (step-pop @p986 :rule scope :premises (@p442)) % 0.38/1.00 (step @p443 :rule process_scope :premises (@p986) :args (@t359)) % 0.38/1.00 (step @p445 :rule implies_elim :premises (@p443)) % 0.38/1.00 (step @p446 :rule cnf_or_pos :args (@t359)) % 0.38/1.00 (step @p447 :rule reordering :premises (@p446) :args ((or @t4 @t299 @t358 (not @t359)))) % 0.38/1.00 (step @p448 :rule cnf_or_pos :args (@t356)) % 0.38/1.00 (step @p449 :rule reordering :premises (@p448) :args ((or @t355 @t354 @t351 @t196 @t194 (not @t356)))) % 0.38/1.00 (assume-push @p987 @t99) % 0.38/1.00 (step @p451 :rule instantiate :premises (@p112) :args (@t360)) % 0.38/1.00 (step-pop @p988 :rule scope :premises (@p451)) % 0.38/1.00 (step @p452 :rule process_scope :premises (@p988) :args (@t365)) % 0.38/1.00 (step @p454 :rule implies_elim :premises (@p452)) % 0.38/1.00 (assume-push @p989 @t38) % 0.38/1.00 (step @p456 :rule instantiate :premises (@p67) :args (@t360)) % 0.38/1.00 (step-pop @p990 :rule scope :premises (@p456)) % 0.38/1.00 (step @p457 :rule process_scope :premises (@p990) :args (@t367)) % 0.38/1.00 (step @p459 :rule implies_elim :premises (@p457)) % 0.38/1.00 (step @p460 :rule cnf_or_pos :args (@t367)) % 0.38/1.00 (step @p461 :rule reordering :premises (@p460) :args ((or @t122 @t366 (not @t367)))) % 0.38/1.00 (step @p462 :rule cnf_or_pos :args (@t365)) % 0.38/1.00 (step @p463 :rule reordering :premises (@p462) :args ((or @t362 @t364 @t361 (not @t365)))) % 0.38/1.00 (assume-push @p991 @t103) % 0.38/1.00 (step @p465 :rule instantiate :premises (@p113) :args (@t368)) % 0.38/1.00 (step-pop @p992 :rule scope :premises (@p465)) % 0.38/1.00 (step @p466 :rule process_scope :premises (@p992) :args (@t376)) % 0.38/1.00 (step @p468 :rule implies_elim :premises (@p466)) % 0.38/1.00 (assume-push @p993 @t80) % 0.38/1.00 (step @p470 :rule instantiate :premises (@p93) :args (@t377)) % 0.38/1.00 (step-pop @p994 :rule scope :premises (@p470)) % 0.38/1.00 (step @p471 :rule process_scope :premises (@p994) :args (@t379)) % 0.38/1.00 (step @p473 :rule implies_elim :premises (@p471)) % 0.38/1.00 (step @p474 :rule cnf_or_pos :args (@t379)) % 0.38/1.00 (step @p475 :rule reordering :premises (@p474) :args ((or @t33 @t378 @t320 (not @t379)))) % 0.38/1.00 (assume-push @p995 @t38) % 0.38/1.00 (step @p477 :rule instantiate :premises (@p67) :args (@t380)) % 0.38/1.00 (step-pop @p996 :rule scope :premises (@p477)) % 0.38/1.00 (step @p478 :rule process_scope :premises (@p996) :args (@t383)) % 0.38/1.00 (step @p480 :rule implies_elim :premises (@p478)) % 0.38/1.00 (assume-push @p997 @t42) % 0.38/1.00 (step @p482 :rule instantiate :premises (@p70) :args (@t380)) % 0.38/1.00 (step-pop @p998 :rule scope :premises (@p482)) % 0.38/1.00 (step @p483 :rule process_scope :premises (@p998) :args (@t385)) % 0.38/1.00 (step @p485 :rule implies_elim :premises (@p483)) % 0.38/1.00 (step @p486 :rule cnf_or_pos :args (@t385)) % 0.38/1.00 (step @p487 :rule reordering :premises (@p486) :args ((or @t384 @t381 (not @t385)))) % 0.38/1.00 (step @p488 :rule cnf_or_pos :args (@t383)) % 0.38/1.00 (step @p489 :rule reordering :premises (@p488) :args ((or @t382 @t374 (not @t383)))) % 0.38/1.00 (assume-push @p999 @t42) % 0.38/1.00 (step @p491 :rule instantiate :premises (@p70) :args (@t177)) % 0.38/1.00 (step-pop @p1000 :rule scope :premises (@p491)) % 0.38/1.00 (step @p492 :rule process_scope :premises (@p1000) :args (@t386)) % 0.38/1.00 (step @p494 :rule implies_elim :premises (@p492)) % 0.38/1.00 (step @p495 :rule cnf_or_pos :args (@t386)) % 0.38/1.00 (step @p496 :rule reordering :premises (@p495) :args ((or @t178 @t372 (not @t386)))) % 0.38/1.00 (step @p497 :rule cnf_or_pos :args (@t376)) % 0.38/1.00 (step @p498 :rule reordering :premises (@p497) :args ((or @t8 @t371 @t369 @t373 @t363 @t375 (not @t376)))) % 0.38/1.00 (step @p499 :rule instantiate :premises (@p87) :args ((@list tptp.n1 tptp.n3 tptp.racquetball))) % 0.38/1.00 (step @p500 :rule cnf_or_pos :args (@t389)) % 0.38/1.00 (step @p501 :rule reordering :premises (@p500) :args ((or @t5 @t388 @t299 (not @t389)))) % 0.38/1.00 (step @p502 :rule chain_m_resolution :premises (@p501 @p3 @p306 @p499) :args (@t388 @t254 (@list @t5 @t293 @t389))) % 0.38/1.00 (step @p503 :rule instantiate :premises (@p80) :args (@t390)) % 0.38/1.00 (step @p504 :rule instantiate :premises (@p123) :args (@t390)) % 0.38/1.00 (step @p505 :rule instantiate :premises (@p91) :args ((@list tptp.milk tptp.vodka tptp.n3))) % 0.38/1.00 (step @p506 :rule cnf_or_pos :args (@t393)) % 0.38/1.00 (step @p507 :rule reordering :premises (@p506) :args ((or @t24 @t279 @t392 (not @t393)))) % 0.38/1.00 (step @p508 :rule chain_m_resolution :premises (@p507 @p42 @p146 @p505) :args (@t392 @t254 (@list @t24 @t125 @t393))) % 0.38/1.00 (step @p509 :rule cnf_or_pos :args (@t396)) % 0.38/1.00 (step @p510 :rule reordering :premises (@p509) :args ((or @t391 @t395 (not @t396)))) % 0.38/1.00 (step @p511 :rule chain_m_resolution :premises (@p510 @p508 @p504) :args (@t395 @t212 (@list @t391 @t396))) % 0.38/1.00 (step @p512 :rule cnf_or_pos :args (@t399)) % 0.38/1.00 (step @p513 :rule reordering :premises (@p512) :args ((or @t370 @t387 @t398 @t394 @t397 (not @t399)))) % 0.38/1.00 (step @p514 :rule instantiate :premises (@p126) :args (@t390)) % 0.38/1.00 (step @p515 :rule cnf_or_pos :args (@t402)) % 0.38/1.00 (step @p516 :rule reordering :premises (@p515) :args ((or @t401 @t400 (not @t402)))) % 0.38/1.00 (step @p517 :rule instantiate :premises (@p89) :args ((@list tptp.englishman tptp.american tptp.n3))) % 0.38/1.00 (step @p518 :rule cnf_or_pos :args (@t406)) % 0.38/1.00 (step @p519 :rule reordering :premises (@p518) :args ((or @t13 @t405 @t403 (not @t406)))) % 0.38/1.00 (step @p520 :rule instantiate :premises (@p85) :args ((@list tptp.n3 tptp.n4 tptp.american))) % 0.38/1.00 (step @p521 :rule cnf_or_pos :args (@t409)) % 0.38/1.00 (step @p522 :rule reordering :premises (@p521) :args ((or @t9 @t403 @t408 (not @t409)))) % 0.38/1.00 (step @p523 :rule instantiate :premises (@p95) :args (@t390)) % 0.38/1.00 (step @p524 :rule cnf_or_pos :args (@t412)) % 0.38/1.00 (step @p525 :rule reordering :premises (@p524) :args ((or @t404 @t411 (not @t412)))) % 0.38/1.00 (step @p526 :rule instantiate :premises (@p130) :args ((@list tptp.n1 tptp.n3))) % 0.38/1.00 (step @p527 :rule cnf_or_pos :args (@t415)) % 0.38/1.00 (step @p528 :rule reordering :premises (@p527) :args ((or @t119 @t247 @t414 (not @t415)))) % 0.38/1.00 (step @p529 :rule chain_m_resolution :premises (@p528 @p140 @p147 @p526) :args (@t414 @t254 (@list @t119 @t126 @t415))) % 0.38/1.00 (step @p530 :rule instantiate :premises (@p84) :args ((@list tptp.n1 tptp.n3 tptp.yellow))) % 0.38/1.00 (step @p531 :rule cnf_or_pos :args (@t418)) % 0.38/1.00 (step @p532 :rule reordering :premises (@p531) :args ((or @t5 @t417 @t292 (not @t418)))) % 0.38/1.00 (step @p533 :rule chain_m_resolution :premises (@p532 @p3 @p305 @p530) :args (@t417 @t254 (@list @t5 @t277 @t418))) % 0.38/1.00 (step @p534 :rule instantiate :premises (@p98) :args (@t380)) % 0.38/1.00 (step @p535 :rule cnf_or_pos :args (@t421)) % 0.38/1.00 (step @p536 :rule reordering :premises (@p535) :args ((or @t384 @t251 @t420 (not @t421)))) % 0.38/1.00 (step @p537 :rule chain_m_resolution :premises (@p536 @p137 @p223 @p534) :args (@t420 @t261 (@list @t116 @t251 @t421))) % 0.38/1.00 (step @p538 :rule instantiate :premises (@p76) :args (@t390)) % 0.38/1.00 (step @p539 :rule cnf_or_pos :args (@t422)) % 0.38/1.00 (step @p540 :rule reordering :premises (@p539) :args ((or @t419 @t181 @t413 @t410 @t416 (not @t422)))) % 0.38/1.00 (step @p541 :rule instantiate :premises (@p70) :args (@t423)) % 0.38/1.00 (step @p542 :rule cnf_or_pos :args (@t426)) % 0.38/1.00 (step @p543 :rule reordering :premises (@p542) :args ((or @t124 @t425 (not @t426)))) % 0.38/1.00 (step @p544 :rule chain_m_resolution :premises (@p543 @p145 @p541) :args (@t425 @t212 (@list @t124 @t426))) % 0.38/1.00 (step @p545 :rule instantiate :premises (@p96) :args (@t423)) % 0.38/1.00 (step @p546 :rule cnf_or_pos :args (@t429)) % 0.38/1.00 (step @p547 :rule reordering :premises (@p546) :args ((or @t424 @t226 @t428 (not @t429)))) % 0.38/1.00 (step @p548 :rule instantiate :premises (@p101) :args (@t430)) % 0.38/1.00 (step @p549 :rule cnf_or_pos :args (@t433)) % 0.38/1.00 (step @p550 :rule reordering :premises (@p549) :args ((or @t427 @t432 (not @t433)))) % 0.38/1.00 (step @p551 :rule instantiate :premises (@p130) :args ((@list tptp.n1 tptp.n5))) % 0.38/1.00 (step @p552 :rule cnf_or_pos :args (@t436)) % 0.38/1.00 (step @p553 :rule reordering :premises (@p552) :args ((or @t121 @t247 @t435 (not @t436)))) % 0.38/1.00 (step @p554 :rule chain_m_resolution :premises (@p553 @p142 @p147 @p551) :args (@t435 @t254 (@list @t121 @t126 @t436))) % 0.38/1.00 (step @p555 :rule instantiate :premises (@p76) :args (@t430)) % 0.38/1.00 (step @p556 :rule instantiate :premises (@p108) :args (@t430)) % 0.38/1.00 (step @p557 :rule instantiate :premises (@p119) :args ((@list tptp.n2 tptp.n5))) % 0.38/1.00 (step @p558 :rule cnf_or_pos :args (@t439)) % 0.38/1.00 (step @p559 :rule reordering :premises (@p558) :args ((or @t123 @t438 @t320 (not @t439)))) % 0.38/1.00 (step @p560 :rule chain_m_resolution :premises (@p559 @p144 @p309 @p557) :args (@t438 @t254 (@list @t123 @t318 @t439))) % 0.38/1.00 (step @p561 :rule cnf_or_pos :args (@t442)) % 0.38/1.00 (step @p562 :rule reordering :premises (@p561) :args ((or @t437 @t441 (not @t442)))) % 0.38/1.00 (step @p563 :rule chain_m_resolution :premises (@p562 @p560 @p556) :args (@t441 @t212 (@list @t437 @t442))) % 0.38/1.00 (step @p564 :rule cnf_or_pos :args (@t444)) % 0.38/1.00 (step @p565 :rule reordering :premises (@p564) :args ((or @t427 @t434 @t443 @t190 @t440 (not @t444)))) % 0.38/1.00 (step @p566 :rule chain_m_resolution :premises (@p238 @p235 @p236) :args (@t265 @t212 (@list @t216 @t266))) % 0.38/1.00 (step @p567 :rule instantiate :premises (@p91) :args ((@list tptp.lemonade tptp.milk tptp.n3))) % 0.38/1.00 (step @p568 :rule cnf_or_pos :args (@t447)) % 0.38/1.00 (step @p569 :rule reordering :premises (@p568) :args ((or @t20 @t279 @t446 (not @t447)))) % 0.38/1.00 (step @p570 :rule chain_m_resolution :premises (@p569 @p36 @p146 @p567) :args (@t446 @t254 (@list @t20 @t125 @t447))) % 0.38/1.00 (step @p571 :rule instantiate :premises (@p79) :args (@t448)) % 0.38/1.00 (step @p572 :rule cnf_or_pos :args (@t450)) % 0.38/1.00 (step @p573 :rule reordering :premises (@p572) :args ((or @t449 @t309 @t445 @t431 @t264 (not @t450)))) % 0.38/1.00 (step @p574 :rule instantiate :premises (@p84) :args ((@list tptp.n4 tptp.n5 tptp.red))) % 0.38/1.00 (step @p575 :rule cnf_or_pos :args (@t454)) % 0.38/1.00 (step @p576 :rule reordering :premises (@p575) :args ((or @t11 @t453 @t451 (not @t454)))) % 0.38/1.00 (step @p577 :rule instantiate :premises (@p91) :args ((@list tptp.lemonade tptp.vodka tptp.n4))) % 0.38/1.00 (step @p578 :rule cnf_or_pos :args (@t458)) % 0.38/1.00 (step @p579 :rule reordering :premises (@p578) :args ((or @t21 @t457 @t456 (not @t458)))) % 0.38/1.00 (step @p580 :rule instantiate :premises (@p94) :args (@t176)) % 0.38/1.00 (step @p581 :rule cnf_or_pos :args (@t461)) % 0.38/1.00 (step @p582 :rule reordering :premises (@p581) :args ((or @t452 @t460 (not @t461)))) % 0.38/1.00 (step @p583 :rule instantiate :premises (@p123) :args (@t176)) % 0.38/1.00 (step @p584 :rule cnf_or_pos :args (@t464)) % 0.38/1.00 (step @p585 :rule reordering :premises (@p584) :args ((or @t455 @t463 (not @t464)))) % 0.38/1.00 (step @p586 :rule instantiate :premises (@p85) :args ((@list tptp.n1 tptp.n4 tptp.russian))) % 0.38/1.00 (step @p587 :rule cnf_or_pos :args (@t467)) % 0.38/1.00 (step @p588 :rule reordering :premises (@p587) :args ((or @t6 @t247 @t466 (not @t467)))) % 0.38/1.00 (step @p589 :rule chain_m_resolution :premises (@p588 @p4 @p147 @p586) :args (@t466 @t254 (@list @t6 @t126 @t467))) % 0.38/1.00 (step @p590 :rule instantiate :premises (@p74) :args (@t176)) % 0.38/1.00 (step @p591 :rule cnf_or_pos :args (@t469)) % 0.38/1.00 (step @p592 :rule reordering :premises (@p591) :args ((or @t407 @t465 @t459 @t468 @t344 (not @t469)))) % 0.38/1.00 (step @p593 :rule chain_m_resolution :premises (@p278 @p51 @p306 @p276) :args (@t298 @t254 (@list @t27 @t293 @t300))) % 0.38/1.00 (step @p594 :rule instantiate :premises (@p81) :args (@t470)) % 0.38/1.00 (step @p595 :rule cnf_or_pos :args (@t472)) % 0.38/1.00 (step @p596 :rule reordering :premises (@p595) :args ((or @t394 @t462 @t471 @t196 @t296 (not @t472)))) % 0.38/1.00 (step @p597 :rule instantiate :premises (@p99) :args (@t176)) % 0.38/1.00 (step @p598 :rule cnf_or_pos :args (@t475)) % 0.38/1.00 (step @p599 :rule reordering :premises (@p598) :args ((or @t473 @t474 (not @t475)))) % 0.38/1.00 (step @p600 :rule instantiate :premises (@p92) :args ((@list tptp.backgammon tptp.solitaire tptp.n5))) % 0.38/1.00 (step @p601 :rule cnf_or_pos :args (@t479)) % 0.38/1.00 (step @p602 :rule reordering :premises (@p601) :args ((or @t26 @t478 @t476 (not @t479)))) % 0.38/1.00 (step @p603 :rule instantiate :premises (@p93) :args ((@list tptp.guppy tptp.toad tptp.n4))) % 0.38/1.00 (step @p604 :rule cnf_or_pos :args (@t483)) % 0.38/1.00 (step @p605 :rule reordering :premises (@p604) :args ((or @t29 @t482 @t481 (not @t483)))) % 0.38/1.00 (step @p606 :rule instantiate :premises (@p92) :args ((@list tptp.backgammon tptp.racquetball tptp.n1))) % 0.38/1.00 (step @p607 :rule cnf_or_pos :args (@t486)) % 0.38/1.00 (step @p608 :rule reordering :premises (@p607) :args ((or @t25 @t299 @t485 (not @t486)))) % 0.38/1.00 (step @p609 :rule chain_m_resolution :premises (@p608 @p46 @p306 @p606) :args (@t485 @t254 (@list @t25 @t293 @t486))) % 0.38/1.00 (step @p430 :rule instantiate :premises (@p106) :args (@t193)) % 0.38/1.00 (step @p423 :rule instantiate :premises (@p93) :args (@t347)) % 0.38/1.00 (step @p610 :rule chain_m_resolution :premises (@p428 @p62 @p309 @p423) :args (@t349 @t254 (@list @t32 @t318 @t350))) % 0.38/1.00 (step @p611 :rule chain_m_resolution :premises (@p435 @p610 @p430) :args (@t352 @t212 (@list @t348 @t353))) % 0.38/1.00 (step @p612 :rule instantiate :premises (@p81) :args (@t487)) % 0.38/1.00 (step @p613 :rule cnf_or_pos :args (@t489)) % 0.38/1.00 (step @p614 :rule reordering :premises (@p613) :args ((or @t398 @t488 @t477 @t351 @t484 (not @t489)))) % 0.38/1.00 (step @p615 :rule instantiate :premises (@p106) :args (@t176)) % 0.38/1.00 (step @p616 :rule cnf_or_pos :args (@t491)) % 0.38/1.00 (step @p617 :rule reordering :premises (@p616) :args ((or @t490 @t480 (not @t491)))) % 0.38/1.00 (step @p618 :rule chain_m_resolution :premises (@p617 @p615 @p614 @p612 @p611 @p609 @p605 @p603 @p57 @p602 @p600 @p48 @p599 @p597 @p596 @p594 @p593 @p511 @p592 @p590 @p589 @p585 @p583 @p582 @p580 @p579 @p577 @p37 @p576 @p574 @p11 @p573 @p571 @p292 @p570 @p566 @p565 @p563 @p555 @p554 @p550 @p548 @p547 @p545 @p544 @p540 @p538 @p537 @p533 @p529 @p525 @p523 @p522 @p520 @p9 @p519 @p517 @p16 @p516 @p514 @p513 @p511 @p503 @p502 @p498 @p496 @p138 @p494 @p489 @p487 @p137 @p485 @p480 @p475 @p64 @p473 @p468 @p113 @p463 @p461 @p143 @p459 @p67 @p454 @p112 @p449 @p447 @p445 @p87 @p298 @p440 @p80 @p435 @p433 @p106 @p428 @p62 @p426 @p93 @p308 @p421 @p121 @p272 @p417 @p108 @p254 @p242 @p413 @p130 @p409 @p73 @p230 @p405 @p97 @p401 @p76 @p251 @p397 @p95 @p248 @p15 @p393 @p89 @p389 @p387 @p103 @p382 @p7 @p380 @p294 @p282 @p2 @p375 @p279 @p235 @p286 @p6 @p146 @p371 @p86 @p367 @p78 @p291 @p363 @p101 @p227 @p32 @p219 @p147 @p216 @p136 @p359 @p70 @p355 @p128 @p351 @p1 @p347 @p90 @p173 @p343 @p124) :args ((or @t190 @t398 @t196) (@list false false false true true true false true true false true false false false false true true false false true true false true false true false true true false true false false true true true false true false true true false true false true false false true true true true false true false true true false true false false false true false true true false false false false false false false false true true false false false true true true false false false false false true false false true false false true false false true true false false false false false false false false false true false false true false true false false false false true false false true true false false true false false true true false false true true false false true true true false false false false false true false false true true false false false false false false false false false false false false true false false) (@list @t491 @t488 @t489 @t351 @t484 @t480 @t483 @t29 @t477 @t479 @t26 @t473 @t475 @t471 @t472 @t296 @t394 @t468 @t469 @t465 @t462 @t464 @t459 @t461 @t455 @t458 @t21 @t452 @t454 @t11 @t449 @t450 @t309 @t445 @t264 @t443 @t440 @t444 @t434 @t431 @t433 @t427 @t429 @t424 @t181 @t422 @t419 @t416 @t413 @t410 @t412 @t407 @t409 @t9 @t404 @t406 @t13 @t401 @t402 @t397 @t394 @t399 @t387 @t370 @t372 @t117 @t386 @t374 @t381 @t116 @t385 @t383 @t369 @t33 @t379 @t376 @t103 @t363 @t362 @t122 @t367 @t38 @t365 @t99 @t354 @t355 @t359 @t76 @t194 @t356 @t66 @t351 @t353 @t88 @t348 @t32 @t350 @t80 @t318 @t319 @t107 @t293 @t294 @t90 @t277 @t267 @t270 @t112 @t269 @t43 @t258 @t260 @t85 @t278 @t55 @t274 @t276 @t81 @t271 @t12 @t273 @t77 @t344 @t346 @t87 @t341 @t8 @t343 @t312 @t302 @t4 @t305 @t289 @t216 @t306 @t7 @t125 @t308 @t75 @t313 @t59 @t309 @t311 @t86 @t255 @t19 @t243 @t126 @t240 @t115 @t242 @t42 @t248 @t111 @t245 @t3 @t257 @t78 @t201 @t203 @t108))) % 0.38/1.00 (step @p619 :rule instantiate :premises (@p87) :args ((@list tptp.n3 tptp.n4 tptp.backgammon))) % 0.38/1.00 (step @p620 :rule cnf_or_pos :args (@t493)) % 0.38/1.00 (step @p621 :rule reordering :premises (@p620) :args ((or @t9 @t492 @t490 (not @t493)))) % 0.38/1.00 (step @p622 :rule instantiate :premises (@p106) :args (@t390)) % 0.38/1.00 (step @p623 :rule cnf_or_pos :args (@t495)) % 0.38/1.00 (step @p624 :rule reordering :premises (@p623) :args ((or @t494 @t492 (not @t495)))) % 0.38/1.00 (step @p625 :rule instantiate :premises (@p93) :args ((@list tptp.guppy tptp.toad tptp.n3))) % 0.38/1.00 (step @p626 :rule cnf_or_pos :args (@t499)) % 0.38/1.00 (step @p627 :rule reordering :premises (@p626) :args ((or @t29 @t498 @t496 (not @t499)))) % 0.38/1.00 (step @p628 :rule instantiate :premises (@p93) :args ((@list tptp.toad tptp.camel tptp.n3))) % 0.38/1.00 (step @p629 :rule cnf_or_pos :args (@t502)) % 0.38/1.00 (step @p630 :rule reordering :premises (@p629) :args ((or @t31 @t501 @t496 (not @t502)))) % 0.38/1.00 (step @p631 :rule instantiate :premises (@p99) :args (@t390)) % 0.38/1.00 (step @p632 :rule cnf_or_pos :args (@t505)) % 0.38/1.00 (step @p633 :rule reordering :premises (@p632) :args ((or @t497 @t504 (not @t505)))) % 0.38/1.00 (step @p634 :rule instantiate :premises (@p112) :args (@t506)) % 0.38/1.00 (step @p442 :rule instantiate :premises (@p87) :args (@t357)) % 0.38/1.00 (step @p635 :rule chain_m_resolution :premises (@p447 @p2 @p306 @p442) :args (@t358 @t254 (@list @t4 @t293 @t359))) % 0.38/1.00 (step @p437 :rule instantiate :premises (@p80) :args (@t193)) % 0.38/1.00 (step @p636 :rule chain_m_resolution :premises (@p335 @p161 @p40 @p332 @p162 @p338 @p160 @p329 @p323 @p163 @p327 @p449 @p437 @p300 @p164) :args ((or @t324 @t355 @t354 @t351 @t194) (@list false true false false false false false true false true false false true false) (@list @t338 @t23 @t312 @t337 @t201 @t339 @t205 @t330 @t336 @t333 @t196 @t356 @t199 @t316))) % 0.38/1.00 (step @p637 :rule chain_m_resolution :premises (@p636 @p315 @p635 @p611 @p298) :args (@t354 (@list true true true true) (@list @t324 @t355 @t351 @t194))) % 0.38/1.00 (step @p638 :rule instantiate :premises (@p67) :args (@t506)) % 0.38/1.00 (step @p639 :rule cnf_or_pos :args (@t509)) % 0.38/1.00 (step @p640 :rule reordering :premises (@p639) :args ((or @t123 @t508 (not @t509)))) % 0.38/1.00 (step @p641 :rule chain_m_resolution :premises (@p640 @p144 @p638) :args (@t508 @t212 (@list @t123 @t509))) % 0.38/1.00 (step @p642 :rule cnf_or_pos :args (@t512)) % 0.38/1.00 (step @p643 :rule reordering :premises (@p642) :args ((or @t507 @t361 @t511 (not @t512)))) % 0.38/1.00 (step @p644 :rule chain_m_resolution :premises (@p643 @p641 @p637 @p634) :args (@t511 @t254 (@list @t507 @t354 @t512))) % 0.38/1.00 (step @p451 :rule instantiate :premises (@p112) :args (@t360)) % 0.38/1.00 (step @p456 :rule instantiate :premises (@p67) :args (@t360)) % 0.38/1.00 (step @p645 :rule chain_m_resolution :premises (@p461 @p143 @p456) :args (@t366 @t212 (@list @t122 @t367))) % 0.38/1.00 (step @p646 :rule chain_m_resolution :premises (@p463 @p645 @p637 @p451) :args (@t364 @t254 (@list @t362 @t354 @t365))) % 0.38/1.00 (step @p470 :rule instantiate :premises (@p93) :args (@t377)) % 0.38/1.00 (step @p647 :rule chain_m_resolution :premises (@p475 @p64 @p309 @p470) :args (@t378 @t254 (@list @t33 @t318 @t379))) % 0.38/1.00 (step @p648 :rule instantiate :premises (@p83) :args (@t513)) % 0.38/1.00 (step @p649 :rule cnf_or_pos :args (@t515)) % 0.38/1.00 (step @p650 :rule reordering :premises (@p649) :args ((or @t514 @t369 @t500 @t363 @t510 (not @t515)))) % 0.38/1.00 (step @p651 :rule instantiate :premises (@p90) :args ((@list tptp.red tptp.white tptp.n3))) % 0.38/1.00 (step @p652 :rule cnf_or_pos :args (@t516)) % 0.38/1.00 (step @p653 :rule reordering :premises (@p652) :args ((or @t16 @t226 @t411 (not @t516)))) % 0.38/1.00 (step @p654 :rule instantiate :premises (@p94) :args (@t390)) % 0.38/1.00 (step @p655 :rule cnf_or_pos :args (@t517)) % 0.38/1.00 (step @p656 :rule reordering :premises (@p655) :args ((or @t410 @t405 (not @t517)))) % 0.38/1.00 (step @p657 :rule instantiate :premises (@p103) :args (@t390)) % 0.38/1.00 (step @p658 :rule instantiate :premises (@p91) :args ((@list tptp.coffee tptp.milk tptp.n3))) % 0.38/1.00 (step @p659 :rule cnf_or_pos :args (@t520)) % 0.38/1.00 (step @p660 :rule reordering :premises (@p659) :args ((or @t22 @t279 @t519 (not @t520)))) % 0.38/1.00 (step @p661 :rule chain_m_resolution :premises (@p660 @p39 @p146 @p658) :args (@t519 @t254 (@list @t22 @t125 @t520))) % 0.38/1.00 (step @p662 :rule cnf_or_pos :args (@t523)) % 0.38/1.00 (step @p663 :rule reordering :premises (@p662) :args ((or @t522 @t518 (not @t523)))) % 0.38/1.00 (step @p664 :rule chain_m_resolution :premises (@p663 @p661 @p657) :args (@t522 @t212 (@list @t518 @t523))) % 0.38/1.00 (step @p665 :rule instantiate :premises (@p74) :args (@t390)) % 0.38/1.00 (step @p666 :rule instantiate :premises (@p85) :args ((@list tptp.n1 tptp.n3 tptp.russian))) % 0.38/1.00 (step @p667 :rule cnf_or_pos :args (@t526)) % 0.38/1.00 (step @p668 :rule reordering :premises (@p667) :args ((or @t5 @t247 @t525 (not @t526)))) % 0.38/1.00 (step @p669 :rule chain_m_resolution :premises (@p668 @p3 @p147 @p666) :args (@t525 @t254 (@list @t5 @t126 @t526))) % 0.38/1.00 (step @p670 :rule cnf_or_pos :args (@t527)) % 0.38/1.00 (step @p671 :rule reordering :premises (@p670) :args ((or @t524 @t404 @t503 @t521 @t401 (not @t527)))) % 0.38/1.00 (step @p672 :rule instantiate :premises (@p126) :args (@t176)) % 0.38/1.00 (step @p673 :rule cnf_or_pos :args (@t530)) % 0.38/1.00 (step @p674 :rule reordering :premises (@p673) :args ((or @t407 @t529 (not @t530)))) % 0.38/1.00 (step @p675 :rule instantiate :premises (@p119) :args ((@list tptp.n2 tptp.n4))) % 0.38/1.00 (step @p676 :rule cnf_or_pos :args (@t533)) % 0.38/1.00 (step @p677 :rule reordering :premises (@p676) :args ((or @t122 @t532 @t320 (not @t533)))) % 0.38/1.00 (step @p678 :rule chain_m_resolution :premises (@p677 @p143 @p309 @p675) :args (@t532 @t254 (@list @t122 @t318 @t533))) % 0.38/1.00 (step @p679 :rule instantiate :premises (@p80) :args (@t176)) % 0.38/1.00 (step @p680 :rule cnf_or_pos :args (@t535)) % 0.38/1.00 (step @p681 :rule reordering :premises (@p680) :args ((or @t534 @t531 @t488 @t462 @t528 (not @t535)))) % 0.38/1.00 (step @p682 :rule chain_m_resolution :premises (@p681 @p679 @p678 @p674 @p672 @p585 @p583 @p522 @p520 @p9 @p579 @p577 @p37 @p671 @p669 @p665 @p664 @p573 @p571 @p292 @p570 @p566 @p656 @p654 @p550 @p548 @p653 @p651 @p24 @p547 @p545 @p544) :args ((or @t226 @t534 @t503 @t488) (@list false true true false true false true false true true false true false true false true false false true true true true false true false true false true true false true) (@list @t535 @t531 @t528 @t530 @t462 @t464 @t407 @t409 @t9 @t455 @t458 @t21 @t401 @t524 @t527 @t521 @t449 @t450 @t309 @t445 @t264 @t404 @t517 @t431 @t433 @t410 @t516 @t16 @t427 @t429 @t424))) % 0.38/1.00 (step @p683 :rule instantiate :premises (@p112) :args ((@list tptp.n1 tptp.n4))) % 0.38/1.00 (step @p684 :rule cnf_or_pos :args (@t538)) % 0.38/1.00 (step @p685 :rule reordering :premises (@p684) :args ((or @t120 @t537 @t536 (not @t538)))) % 0.38/1.00 (step @p686 :rule chain_m_resolution :premises (@p685 @p683 @p141 @p682 @p650 @p648 @p647 @p646 @p644 @p633 @p631 @p630 @p628 @p61 @p627 @p625 @p57 @p624 @p622 @p621 @p619 @p9 @p618 @p339 @p159 @p157 @p156 @p152 @p150 @p138) :args (@t180 (@list false true false false false true true true true false true false true true false true false false true false true false true true false true false false false) (@list @t538 @t120 @t534 @t514 @t515 @t369 @t363 @t510 @t503 @t505 @t500 @t502 @t31 @t497 @t499 @t29 @t494 @t495 @t488 @t493 @t9 @t398 @t196 @t190 @t192 @t184 @t181 @t182 @t117))) % 0.38/1.00 (step @p687 :rule cnf_or_pos :args (@t539)) % 0.38/1.00 (step @p688 :rule reordering :premises (@p687) :args ((or @t179 @t457 (not @t539)))) % 0.38/1.00 (step @p689 :rule chain_m_resolution :premises (@p688 @p686 @p149) :args (@t457 @t212 (@list @t179 @t539))) % 0.38/1.00 (step @p690 :rule instantiate :premises (@p84) :args ((@list tptp.n3 tptp.n4 tptp.red))) % 0.38/1.00 (step @p691 :rule instantiate :premises (@p97) :args (@t177)) % 0.38/1.00 (step @p692 :rule cnf_or_pos :args (@t540)) % 0.38/1.00 (step @p693 :rule reordering :premises (@p692) :args ((or @t178 @t226 @t179 (not @t540)))) % 0.38/1.00 (step @p694 :rule chain_m_resolution :premises (@p693 @p138 @p686 @p691) :args (@t226 @t261 (@list @t117 @t179 @t540))) % 0.38/1.00 (step @p695 :rule chain_m_resolution :premises (@p540 @p537 @p694 @p529 @p533 @p538) :args (@t410 @t317 (@list @t419 @t181 @t413 @t416 @t422))) % 0.38/1.00 (step @p696 :rule cnf_or_pos :args (@t541)) % 0.38/1.00 (step @p697 :rule reordering :premises (@p696) :args ((or @t9 @t411 @t453 (not @t541)))) % 0.38/1.00 (step @p698 :rule chain_m_resolution :premises (@p697 @p9 @p695 @p690) :args (@t453 @t254 (@list @t9 @t410 @t541))) % 0.38/1.00 (step @p699 :rule chain_m_resolution :premises (@p582 @p698 @p580) :args (@t460 @t212 (@list @t452 @t461))) % 0.38/1.00 (assume-push @p1001 @t542) % 0.38/1.00 (step @p701 :rule instantiate :premises (@p1001) :args (@t543)) % 0.38/1.00 (step-pop @p1002 :rule scope :premises (@p701)) % 0.38/1.00 (step @p702 :rule process_scope :premises (@p1002) :args (@t411)) % 0.38/1.00 (step @p704 :rule implies_elim :premises (@p702)) % 0.38/1.00 (step @p705 :rule chain_m_resolution :premises (@p704 @p695) :args ((not @t542) @t544 (@list @t410))) % 0.38/1.00 (step @p706 :rule instantiate :premises (@p98) :args (@t183)) % 0.38/1.00 (step @p707 :rule instantiate :premises (@p77) :args (@t545)) % 0.38/1.00 (step @p708 :rule cnf_or_pos :args (@t546)) % 0.38/1.00 (step @p709 :rule reordering :premises (@p708) :args ((or @t255 @t419 @t179 @t427 @t216 (not @t546)))) % 0.38/1.00 (step @p710 :rule chain_m_resolution :premises (@p709 @p228 @p537 @p686 @p235 @p707) :args (@t427 @t317 (@list @t255 @t419 @t179 @t216 @t546))) % 0.38/1.00 (step @p711 :rule cnf_or_pos :args (@t547)) % 0.38/1.00 (step @p712 :rule reordering :premises (@p711) :args ((or @t186 @t235 @t428 (not @t547)))) % 0.38/1.00 (step @p713 :rule chain_m_resolution :premises (@p712 @p139 @p710 @p706) :args (@t235 (@list false false false) (@list @t118 @t427 @t547))) % 0.38/1.00 (assume-push @p1003 @t548) % 0.38/1.00 (step @p715 :rule instantiate :premises (@p1003) :args (@t262)) % 0.38/1.00 (step-pop @p1004 :rule scope :premises (@p715)) % 0.38/1.00 (step @p716 :rule process_scope :premises (@p1004) :args (@t236)) % 0.38/1.00 (step @p718 :rule implies_elim :premises (@p716)) % 0.38/1.00 (step @p719 :rule chain_m_resolution :premises (@p718 @p713) :args ((not @t548) @t544 (@list @t235))) % 0.38/1.00 (step @p720 :rule chain_m_resolution :premises (@p525 @p695 @p523) :args (@t404 @t188 (@list @t410 @t412))) % 0.38/1.00 (assume-push @p1005 @t549) % 0.38/1.00 (step @p722 :rule instantiate :premises (@p1005) :args ((@list tptp.englishman))) % 0.38/1.00 (step-pop @p1006 :rule scope :premises (@p722)) % 0.38/1.00 (step @p723 :rule process_scope :premises (@p1006) :args (@t405)) % 0.38/1.00 (step @p725 :rule implies_elim :premises (@p723)) % 0.38/1.00 (step @p726 :rule chain_m_resolution :premises (@p725 @p720) :args ((not @t549) @t544 (@list @t404))) % 0.38/1.00 (step @p727 :rule chain_m_resolution :premises (@p519 @p16 @p720 @p517) :args (@t403 @t254 (@list @t13 @t404 @t406))) % 0.38/1.00 (step @p728 :rule chain_m_resolution :premises (@p516 @p727 @p514) :args (@t400 @t212 (@list @t401 @t402))) % 0.38/1.00 (assume-push @p1007 @t60) % 0.38/1.00 (step-pop @p1008 :rule scope :premises (@p571)) % 0.38/1.00 (step @p730 :rule process_scope :premises (@p1008) :args (@t450)) % 0.38/1.00 (step @p732 :rule implies_elim :premises (@p730)) % 0.38/1.00 (assume-push @p1009 @t79) % 0.38/1.00 (step-pop @p1010 :rule scope :premises (@p567)) % 0.38/1.00 (step @p734 :rule process_scope :premises (@p1010) :args (@t447)) % 0.38/1.00 (step @p736 :rule implies_elim :premises (@p734)) % 0.38/1.00 (assume-push @p1011 @t86) % 0.38/1.00 (step-pop @p1012 :rule scope :premises (@p236)) % 0.38/1.00 (step @p738 :rule process_scope :premises (@p1012) :args (@t266)) % 0.38/1.00 (step @p740 :rule implies_elim :premises (@p738)) % 0.38/1.00 (assume-push @p1013 @t550) % 0.38/1.00 (step @p742 :rule instantiate :premises (@p1013) :args (@t448)) % 0.38/1.00 (step-pop @p1014 :rule scope :premises (@p742)) % 0.38/1.00 (step @p743 :rule process_scope :premises (@p1014) :args (@t432)) % 0.38/1.00 (step @p745 :rule implies_elim :premises (@p743)) % 0.38/1.00 (assume-push @p1015 @t551) % 0.38/1.00 (step @p747 :rule instantiate :premises (@p1015) :args ((@list tptp.quoits))) % 0.38/1.00 (step-pop @p1016 :rule scope :premises (@p747)) % 0.38/1.00 (step @p748 :rule process_scope :premises (@p1016) :args (@t361)) % 0.38/1.00 (step @p750 :rule implies_elim :premises (@p748)) % 0.38/1.00 (step @p377 :rule instantiate :premises (@p86) :args (@t340)) % 0.38/1.00 (assume-push @p1017 @t552) % 0.38/1.00 (step @p752 :rule instantiate :premises (@p1017) :args ((@list tptp.coffee))) % 0.38/1.00 (step-pop @p1018 :rule scope :premises (@p752)) % 0.38/1.00 (step @p753 :rule process_scope :premises (@p1018) :args (@t314)) % 0.38/1.00 (step @p755 :rule implies_elim :premises (@p753)) % 0.38/1.00 (step @p756 :rule instantiate :premises (@p67) :args (@t183)) % 0.38/1.00 (step @p757 :rule instantiate :premises (@p70) :args (@t183)) % 0.38/1.00 (step @p758 :rule cnf_or_pos :args (@t554)) % 0.38/1.00 (step @p759 :rule reordering :premises (@p758) :args ((or @t186 @t553 (not @t554)))) % 0.38/1.00 (step @p760 :rule chain_m_resolution :premises (@p759 @p139 @p757) :args (@t553 @t188 (@list @t118 @t554))) % 0.38/1.00 (step @p761 :rule cnf_or_pos :args (@t557)) % 0.38/1.00 (step @p762 :rule reordering :premises (@p761) :args ((or @t556 @t555 (not @t557)))) % 0.38/1.00 (step @p763 :rule chain_m_resolution :premises (@p762 @p760 @p756) :args (@t555 @t188 (@list @t553 @t557))) % 0.38/1.00 (step @p764 :rule instantiate :premises (@p1) :args (@t430)) % 0.38/1.00 (step @p765 :rule instantiate :premises (@p115) :args (@t189)) % 0.38/1.00 (step @p766 :rule cnf_or_pos :args (@t563)) % 0.38/1.00 (step @p767 :rule reordering :premises (@p766) :args ((or @t559 @t363 @t560 @t562 (not @t563)))) % 0.38/1.00 (step @p491 :rule instantiate :premises (@p70) :args (@t177)) % 0.38/1.00 (step @p768 :rule chain_m_resolution :premises (@p496 @p138 @p491) :args (@t372 @t188 (@list @t117 @t386))) % 0.38/1.00 (step @p477 :rule instantiate :premises (@p67) :args (@t380)) % 0.38/1.00 (step @p482 :rule instantiate :premises (@p70) :args (@t380)) % 0.38/1.00 (step @p769 :rule chain_m_resolution :premises (@p487 @p137 @p482) :args (@t381 @t188 (@list @t116 @t385))) % 0.38/1.00 (step @p770 :rule chain_m_resolution :premises (@p489 @p769 @p477) :args (@t374 @t188 (@list @t381 @t383))) % 0.38/1.00 (step @p465 :rule instantiate :premises (@p113) :args (@t368)) % 0.38/1.00 (step @p771 :rule instantiate :premises (@p119) :args (@t208)) % 0.38/1.00 (step @p772 :rule cnf_or_pos :args (@t566)) % 0.38/1.00 (step @p773 :rule reordering :premises (@p772) :args ((or @t209 @t299 @t565 (not @t566)))) % 0.38/1.00 (step @p774 :rule chain_m_resolution :premises (@p773 @p182 @p306 @p771) :args (@t565 @t254 (@list @t209 @t293 @t566))) % 0.38/1.00 (assume-push @p1019 @t567) % 0.38/1.00 (step @p776 :rule instantiate :premises (@p1019) :args (@t568)) % 0.38/1.00 (step-pop @p1020 :rule scope :premises (@p776)) % 0.38/1.00 (step @p777 :rule process_scope :premises (@p1020) :args (@t570)) % 0.38/1.00 (step @p779 :rule implies_elim :premises (@p777)) % 0.38/1.00 (assume-push @p1021 @t567) % 0.38/1.00 (step @p781 :rule instantiate :premises (@p1021) :args (@t571)) % 0.38/1.00 (step-pop @p1022 :rule scope :premises (@p781)) % 0.38/1.00 (step @p782 :rule process_scope :premises (@p1022) :args ((not @t572))) % 0.38/1.00 (step @p784 :rule implies_elim :premises (@p782)) % 0.38/1.00 (assume-push @p1023 @t567) % 0.38/1.00 (step @p786 :rule instantiate :premises (@p1023) :args ((@list tptp.no_pet))) % 0.38/1.00 (step-pop @p1024 :rule scope :premises (@p786)) % 0.38/1.00 (step @p787 :rule process_scope :premises (@p1024) :args ((not @t573))) % 0.38/1.00 (step @p789 :rule implies_elim :premises (@p787)) % 0.38/1.00 (step @p790 :rule instantiate :premises (@p82) :args (@t430)) % 0.38/1.00 (step @p791 :rule cnf_or_pos :args (@t574)) % 0.38/1.00 (step @p792 :rule reordering :premises (@p791) :args ((or @t510 @t564 @t572 @t569 @t573 (not @t574)))) % 0.38/1.00 (step @p793 :rule chain_m_resolution :premises (@p792 @p790 @p789 @p784 @p779) :args ((or (not @t567) @t510 @t564) (@list false true true true) (@list @t574 @t573 @t572 @t569))) % 0.38/1.00 (assume-push @p1025 @t575) % 0.38/1.00 (step @p795 :rule instantiate :premises (@p1025) :args ((@list tptp.swede))) % 0.38/1.00 (step-pop @p1026 :rule scope :premises (@p795)) % 0.38/1.00 (step @p796 :rule process_scope :premises (@p1026) :args (@t206)) % 0.38/1.00 (step @p798 :rule implies_elim :premises (@p796)) % 0.38/1.00 (step @p384 :rule instantiate :premises (@p103) :args (@t176)) % 0.38/1.00 (step @p799 :rule instantiate :premises (@p86) :args ((@list tptp.n3 tptp.n4 tptp.milk))) % 0.38/1.00 (step @p800 :rule cnf_or_pos :args (@t578)) % 0.38/1.00 (step @p801 :rule reordering :premises (@p800) :args ((or @t9 @t279 @t577 (not @t578)))) % 0.38/1.00 (step @p802 :rule chain_m_resolution :premises (@p801 @p9 @p146 @p799) :args (@t577 @t254 (@list @t9 @t125 @t578))) % 0.38/1.00 (step @p803 :rule instantiate :premises (@p78) :args (@t176)) % 0.38/1.00 (step @p804 :rule instantiate :premises (@p86) :args ((@list tptp.n1 tptp.n4 tptp.unknown_drink))) % 0.38/1.00 (step @p805 :rule cnf_or_pos :args (@t581)) % 0.38/1.00 (step @p806 :rule reordering :premises (@p805) :args ((or @t6 @t580 @t304 (not @t581)))) % 0.38/1.00 (step @p807 :rule chain_m_resolution :premises (@p806 @p4 @p280 @p804) :args (@t580 @t254 (@list @t6 @t289 @t581))) % 0.38/1.00 (step @p808 :rule cnf_or_pos :args (@t582)) % 0.38/1.00 (step @p809 :rule reordering :premises (@p808) :args ((or @t576 @t449 @t341 @t455 @t579 (not @t582)))) % 0.38/1.00 (step @p810 :rule instantiate :premises (@p124) :args (@t176)) % 0.38/1.00 (step @p811 :rule cnf_or_pos :args (@t583)) % 0.38/1.00 (step @p812 :rule reordering :premises (@p811) :args ((or @t462 @t456 (not @t583)))) % 0.38/1.00 (assume-push @p1027 @t584) % 0.38/1.00 (step @p814 :rule instantiate :premises (@p1027) :args ((@list tptp.vodka))) % 0.38/1.00 (step-pop @p1028 :rule scope :premises (@p814)) % 0.38/1.00 (step @p815 :rule process_scope :premises (@p1028) :args (@t456)) % 0.38/1.00 (step @p817 :rule implies_elim :premises (@p815)) % 0.38/1.00 (assume-push @p1029 @t585) % 0.38/1.00 (step @p819 :rule instantiate :premises (@p1029) :args (@t487)) % 0.38/1.00 (step-pop @p1030 :rule scope :premises (@p819)) % 0.38/1.00 (step @p820 :rule process_scope :premises (@p1030) :args (@t492)) % 0.38/1.00 (step @p822 :rule implies_elim :premises (@p820)) % 0.38/1.00 (assume-push @p1031 @t586) % 0.38/1.00 (step @p824 :rule instantiate :premises (@p1031) :args (@t470)) % 0.38/1.00 (step-pop @p1032 :rule scope :premises (@p824)) % 0.38/1.00 (step @p825 :rule process_scope :premises (@p1032) :args (@t463)) % 0.38/1.00 (step @p827 :rule implies_elim :premises (@p825)) % 0.38/1.00 (step @p828 :rule instantiate :premises (@p87) :args ((@list tptp.n4 tptp.n5 tptp.solitaire))) % 0.38/1.00 (step @p829 :rule cnf_or_pos :args (@t587)) % 0.38/1.00 (step @p830 :rule reordering :premises (@p829) :args ((or @t11 @t463 @t476 (not @t587)))) % 0.38/1.00 (assume-push @p1033 @t588) % 0.38/1.00 (step @p832 :rule instantiate :premises (@p1033) :args (@t568)) % 0.38/1.00 (step-pop @p1034 :rule scope :premises (@p832)) % 0.38/1.00 (step @p833 :rule process_scope :premises (@p1034) :args (@t496)) % 0.38/1.00 (step @p835 :rule implies_elim :premises (@p833)) % 0.38/1.00 (step @p836 :rule instantiate :premises (@p88) :args ((@list tptp.n3 tptp.n5 tptp.toad))) % 0.38/1.00 (step @p837 :rule cnf_or_pos :args (@t589)) % 0.38/1.00 (step @p838 :rule reordering :premises (@p837) :args ((or @t10 @t496 @t570 (not @t589)))) % 0.38/1.00 (step @p839 :rule instantiate :premises (@p106) :args (@t430)) % 0.38/1.00 (step @p840 :rule cnf_or_pos :args (@t590)) % 0.38/1.00 (step @p841 :rule reordering :premises (@p840) :args ((or @t478 @t569 (not @t590)))) % 0.38/1.00 (step @p842 :rule instantiate :premises (@p80) :args (@t430)) % 0.38/1.00 (step @p843 :rule cnf_or_pos :args (@t592)) % 0.38/1.00 (step @p844 :rule reordering :premises (@p843) :args ((or @t558 @t437 @t477 @t471 @t591 (not @t592)))) % 0.38/1.00 (assume-push @p1035 @t593) % 0.38/1.00 (step @p846 :rule instantiate :premises (@p1035) :args ((@list tptp.charades))) % 0.38/1.00 (step-pop @p1036 :rule scope :premises (@p846)) % 0.38/1.00 (step @p847 :rule process_scope :premises (@p1036) :args (@t594)) % 0.38/1.00 (step @p849 :rule implies_elim :premises (@p847)) % 0.38/1.00 (step @p850 :rule instantiate :premises (@p126) :args (@t430)) % 0.38/1.00 (step @p851 :rule cnf_or_pos :args (@t596)) % 0.38/1.00 (step @p852 :rule reordering :premises (@p851) :args ((or @t595 @t594 (not @t596)))) % 0.38/1.00 (assume-push @p1037 @t597) % 0.38/1.00 (step @p854 :rule instantiate :premises (@p1037) :args ((@list tptp.american))) % 0.38/1.00 (step-pop @p1038 :rule scope :premises (@p854)) % 0.38/1.00 (step @p855 :rule process_scope :premises (@p1038) :args (@t598)) % 0.38/1.00 (step @p857 :rule implies_elim :premises (@p855)) % 0.38/1.00 (step @p858 :rule instantiate :premises (@p85) :args ((@list tptp.n4 tptp.n5 tptp.american))) % 0.38/1.00 (step @p859 :rule cnf_or_pos :args (@t599)) % 0.38/1.00 (step @p860 :rule reordering :premises (@p859) :args ((or @t11 @t408 @t598 (not @t599)))) % 0.38/1.00 (assume-push @p1039 @t600) % 0.38/1.00 (step @p862 :rule instantiate :premises (@p1039) :args ((@list tptp.italian))) % 0.38/1.00 (step-pop @p1040 :rule scope :premises (@p862)) % 0.38/1.00 (step @p863 :rule process_scope :premises (@p1040) :args (@t474)) % 0.38/1.00 (step @p865 :rule implies_elim :premises (@p863)) % 0.38/1.00 (assume-push @p1041 @t601) % 0.38/1.00 (step @p867 :rule instantiate :premises (@p1041) :args (@t571)) % 0.38/1.00 (step-pop @p1042 :rule scope :premises (@p867)) % 0.38/1.00 (step @p868 :rule process_scope :premises (@p1042) :args (@t482)) % 0.38/1.00 (step @p870 :rule implies_elim :premises (@p868)) % 0.38/1.00 (assume-push @p1043 @t602) % 0.38/1.00 (step @p872 :rule instantiate :premises (@p1043) :args ((@list tptp.rat))) % 0.38/1.00 (step-pop @p1044 :rule scope :premises (@p872)) % 0.38/1.00 (step @p873 :rule process_scope :premises (@p1044) :args (@t320)) % 0.38/1.00 (step @p875 :rule implies_elim :premises (@p873)) % 0.38/1.00 (step @p876 :rule chain_m_resolution :premises (@p875 @p309) :args ((not @t602) @t544 (@list @t318))) % 0.38/1.00 (assume-push @p1045 @t603) % 0.38/1.00 (step @p878 :rule instantiate :premises (@p1045) :args ((@list tptp.unknown_drink))) % 0.38/1.00 (step-pop @p1046 :rule scope :premises (@p878)) % 0.38/1.00 (step @p879 :rule process_scope :premises (@p1046) :args (@t304)) % 0.38/1.00 (step @p881 :rule implies_elim :premises (@p879)) % 0.38/1.00 (step @p882 :rule chain_m_resolution :premises (@p881 @p280) :args ((not @t603) @t544 (@list @t289))) % 0.38/1.00 (assume-push @p1047 @t604) % 0.38/1.00 (step @p884 :rule instantiate :premises (@p1047) :args ((@list tptp.yellow))) % 0.38/1.00 (step-pop @p1048 :rule scope :premises (@p884)) % 0.38/1.00 (step @p885 :rule process_scope :premises (@p1048) :args (@t292)) % 0.38/1.00 (step @p887 :rule implies_elim :premises (@p885)) % 0.38/1.00 (step @p888 :rule chain_m_resolution :premises (@p887 @p305) :args ((not @t604) @t544 (@list @t277))) % 0.38/1.00 (assume-push @p1049 @t605) % 0.38/1.00 (step @p890 :rule instantiate :premises (@p1049) :args (@t545)) % 0.38/1.00 (step-pop @p1050 :rule scope :premises (@p890)) % 0.38/1.00 (step @p891 :rule process_scope :premises (@p1050) :args (@t428)) % 0.38/1.00 (step @p893 :rule implies_elim :premises (@p891)) % 0.38/1.00 (assume-push @p1051 @t605) % 0.38/1.00 (step @p895 :rule instantiate :premises (@p1051) :args (@t543)) % 0.38/1.00 (step-pop @p1052 :rule scope :premises (@p895)) % 0.38/1.00 (step @p896 :rule process_scope :premises (@p1052) :args (@t451)) % 0.38/1.00 (step @p898 :rule implies_elim :premises (@p896)) % 0.38/1.00 (assume-push @p1053 @t605) % 0.38/1.00 (step @p900 :rule instantiate :premises (@p1053) :args (@t262)) % 0.38/1.00 (step-pop @p1054 :rule scope :premises (@p900)) % 0.38/1.00 (step @p901 :rule process_scope :premises (@p1054) :args (@t191)) % 0.38/1.00 (step @p903 :rule implies_elim :premises (@p901)) % 0.38/1.00 (step @p904 :rule chain_m_resolution :premises (@p565 @p555 @p554 @p903 @p898 @p893) :args ((or @t606 @t440) (@list false true true true true) (@list @t444 @t434 @t190 @t443 @t427))) % 0.38/1.00 (step @p905 :rule chain_m_resolution :premises (@p904 @p563) :args (@t606 @t301 (@list @t440))) % 0.38/1.00 (assume-push @p1055 @t607) % 0.38/1.00 (step @p907 :rule instantiate :premises (@p1055) :args ((@list tptp.blue))) % 0.38/1.00 (step-pop @p1056 :rule scope :premises (@p907)) % 0.38/1.00 (step @p908 :rule process_scope :premises (@p1056) :args (@t250)) % 0.38/1.00 (step @p910 :rule implies_elim :premises (@p908)) % 0.38/1.00 (step @p911 :rule chain_m_resolution :premises (@p910 @p220) :args ((not @t607) @t544 (@list @t243))) % 0.38/1.00 (assume-push @p1057 @t608) % 0.38/1.00 (step @p913 :rule instantiate :premises (@p1057) :args ((@list tptp.racquetball))) % 0.38/1.00 (step-pop @p1058 :rule scope :premises (@p913)) % 0.38/1.00 (step @p914 :rule process_scope :premises (@p1058) :args (@t299)) % 0.38/1.00 (step @p916 :rule implies_elim :premises (@p914)) % 0.38/1.00 (step @p917 :rule chain_m_resolution :premises (@p916 @p306) :args ((not @t608) @t544 (@list @t293))) % 0.38/1.00 (assume-push @p1059 @t609) % 0.38/1.00 (step @p919 :rule instantiate :premises (@p1059) :args ((@list tptp.milk))) % 0.38/1.00 (step-pop @p1060 :rule scope :premises (@p919)) % 0.38/1.00 (step @p920 :rule process_scope :premises (@p1060) :args (@t279)) % 0.38/1.00 (step @p922 :rule implies_elim :premises (@p920)) % 0.38/1.00 (step @p923 :rule reordering :premises (@p922) :args ((or @t279 @t610))) % 0.38/1.00 (step @p924 :rule chain_m_resolution :premises (@p923 @p146) :args (@t610 @t544 (@list @t125))) % 0.38/1.00 (assume-push @p1061 @t611) % 0.38/1.00 (step @p926 :rule instantiate :premises (@p1061) :args ((@list tptp.russian))) % 0.38/1.00 (step-pop @p1062 :rule scope :premises (@p926)) % 0.38/1.00 (step @p927 :rule process_scope :premises (@p1062) :args (@t247)) % 0.38/1.00 (step @p929 :rule implies_elim :premises (@p927)) % 0.38/1.00 (step @p930 :rule reordering :premises (@p929) :args ((or @t247 @t612))) % 0.38/1.00 (step @p931 :rule chain_m_resolution :premises (@p930 @p147) :args (@t612 @t544 (@list @t126))) % 0.38/1.00 (step @p932 :rule quant-miniscope-or :args ((= @t175 (or @t611 @t575 @t549 @t600 @t597 @t604 @t607 @t542 @t548 @t605 @t603 @t552 @t609 @t584 @t550 @t608 @t551 @t585 @t586 @t593 @t613 @t602 @t588 @t601 @t567)))) % 0.38/1.00 (step @p933 :rule eq_resolve :premises (@p148 @p932)) % 0.38/1.00 (assume-push @p1063 @t613) % 0.38/1.00 (step @p935 :rule instantiate :premises (@p1063) :args (@t513)) % 0.38/1.00 (step-pop @p1064 :rule scope :premises (@p935)) % 0.38/1.00 (step @p936 :rule process_scope :premises (@p1064) :args (@t537)) % 0.38/1.00 (step @p938 :rule implies_elim :premises (@p936)) % 0.38/1.00 (step @p939 :rule chain_m_resolution :premises (@p938 @p933 @p931 @p924 @p917 @p911 @p905 @p888 @p882 @p876 @p870 @p599 @p597 @p865 @p592 @p590 @p589 @p860 @p858 @p11 @p857 @p852 @p850 @p849 @p844 @p842 @p560 @p650 @p648 @p647 @p841 @p839 @p630 @p628 @p61 @p838 @p836 @p10 @p835 @p830 @p828 @p11 @p827 @p822 @p624 @p622 @p817 @p812 @p810 @p513 @p511 @p503 @p502 @p809 @p807 @p803 @p802 @p389 @p384 @p798 @p793 @p774 @p498 @p465 @p647 @p770 @p768 @p7 @p767 @p765 @p764 @p763 @p755 @p382 @p377 @p7 @p297 @p295 @p750 @p643 @p634 @p641 @p463 @p451 @p645 @p294 @p292 @p288 @p287 @p283 @p449 @p611 @p437 @p298 @p635 @p173 @p171 @p745 @p573 @p238 @p740 @p235 @p569 @p36 @p146 @p736 @p91 @p291 @p363 @p101 @p227 @p32 @p219 @p147 @p216 @p136 @p359 @p70 @p355 @p128 @p351 @p1 @p347 @p90 @p732 @p79) :args ((or @t549 @t542 @t548 @t449 @t397 @t459 @t196) (@list false true true true true true true true true true false false true false false true true false true true false false true false false true false false true true false true false true true false true true true false true true true false false true false false false true false true false true false true true false true true true true false true false false true true false false false true true false true false false true true false true true false true false true false true true false true false true true true false true false true false true true true false false false true false false true true false false false false false false false false false false false false false false) (@list @t613 @t611 @t609 @t608 @t607 @t605 @t604 @t603 @t602 @t601 @t473 @t475 @t600 @t468 @t469 @t465 @t407 @t599 @t11 @t597 @t595 @t596 @t593 @t591 @t592 @t437 @t514 @t515 @t369 @t477 @t590 @t500 @t502 @t31 @t569 @t589 @t10 @t588 @t471 @t587 @t11 @t586 @t585 @t494 @t495 @t584 @t462 @t583 @t398 @t394 @t399 @t387 @t455 @t579 @t582 @t576 @t344 @t346 @t575 @t567 @t564 @t370 @t376 @t369 @t374 @t372 @t8 @t558 @t563 @t561 @t555 @t552 @t341 @t343 @t8 @t205 @t315 @t551 @t510 @t512 @t507 @t363 @t365 @t362 @t312 @t309 @t313 @t306 @t302 @t354 @t351 @t356 @t194 @t355 @t201 @t203 @t550 @t431 @t264 @t266 @t216 @t445 @t20 @t125 @t447 @t79 @t309 @t311 @t86 @t255 @t19 @t243 @t126 @t240 @t115 @t242 @t42 @t248 @t111 @t245 @t3 @t257 @t78 @t450 @t60))) % 0.38/1.00 (step @p940 false :rule chain_m_resolution :premises (@p939 @p728 @p726 @p339 @p719 @p705 @p699 @p689) :args (false (@list true true true true true true true) (@list @t397 @t549 @t196 @t548 @t542 @t459 @t449))) % 0.38/1.00 ) % 0.38/1.00 % SZS output end Proof % 0.38/1.00 % cvc5 exiting %------------------------------------------------------------------------------