%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : PUZ010-1 : TPTP v9.2.1. Bugfixed v1.0.1. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n015.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jun 3 08:43:56 AM UTC 2026 % Result : Unsatisfiable 0.38s 0.85s % Output : Proof 0.38s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : PUZ010-1 : TPTP v9.2.1. Bugfixed v1.0.1. % 0.12/0.14 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.18/0.35 % Computer : n015.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:34 EDT 2026 % 0.18/0.36 % CPUTime : % 0.27/0.53 %----Proving TF0_NAR, FOF, or CNF % 0.27/0.54 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 0.38/0.85 % SZS status Unsatisfiable % 0.38/0.85 % SZS output start Proof % 0.38/0.88 ( % 0.38/0.88 (declare-sort $$unsorted 0) % 0.38/0.88 (declare-const tptp.yellow $$unsorted) % 0.38/0.88 (declare-const tptp.blue $$unsorted) % 0.38/0.88 (declare-const tptp.green $$unsorted) % 0.38/0.88 (declare-const tptp.ivory $$unsorted) % 0.38/0.88 (declare-const tptp.color (-> $$unsorted Bool)) % 0.38/0.88 (declare-const tptp.dog $$unsorted) % 0.38/0.88 (declare-const tptp.snails $$unsorted) % 0.38/0.88 (declare-const tptp.horse $$unsorted) % 0.38/0.88 (declare-const tptp.red $$unsorted) % 0.38/0.88 (declare-const tptp.english $$unsorted) % 0.38/0.88 (declare-const tptp.saab $$unsorted) % 0.38/0.88 (declare-const tptp.person (-> $$unsorted Bool)) % 0.38/0.88 (declare-const tptp.water $$unsorted) % 0.38/0.88 (declare-const tptp.norwegian $$unsorted) % 0.38/0.88 (declare-const tptp.coffee $$unsorted) % 0.38/0.88 (declare-const tptp.house (-> $$unsorted Bool)) % 0.38/0.88 (declare-const tptp.next_to (-> $$unsorted $$unsorted Bool)) % 0.38/0.88 (declare-const tptp.drives (-> $$unsorted $$unsorted Bool)) % 0.38/0.88 (declare-const tptp.house_1 $$unsorted) % 0.38/0.88 (declare-const tptp.owns (-> $$unsorted $$unsorted Bool)) % 0.38/0.88 (declare-const tptp.house_2 $$unsorted) % 0.38/0.88 (declare-const tptp.house_3 $$unsorted) % 0.38/0.88 (declare-const tptp.zebra $$unsorted) % 0.38/0.88 (declare-const tptp.fox $$unsorted) % 0.38/0.88 (declare-const tptp.ukranian $$unsorted) % 0.38/0.88 (declare-const tptp.house_4 $$unsorted) % 0.38/0.88 (declare-const tptp.is_color (-> $$unsorted $$unsorted Bool)) % 0.38/0.88 (declare-const tptp.spaniard $$unsorted) % 0.38/0.88 (declare-const tptp.left_of (-> $$unsorted $$unsorted Bool)) % 0.38/0.88 (declare-const tptp.porsche $$unsorted) % 0.38/0.88 (declare-const tptp.japanese $$unsorted) % 0.38/0.88 (declare-const tptp.lives (-> $$unsorted $$unsorted Bool)) % 0.38/0.88 (declare-const tptp.drinks (-> $$unsorted $$unsorted Bool)) % 0.38/0.88 (declare-const tptp.milk $$unsorted) % 0.38/0.88 (declare-const tptp.tea $$unsorted) % 0.38/0.88 (declare-const tptp.car (-> $$unsorted Bool)) % 0.38/0.88 (declare-const tptp.orange $$unsorted) % 0.38/0.88 (declare-const tptp.drink (-> $$unsorted Bool)) % 0.38/0.88 (declare-const tptp.jaguar $$unsorted) % 0.38/0.88 (declare-const tptp.honda $$unsorted) % 0.38/0.88 (declare-const tptp.animal (-> $$unsorted Bool)) % 0.38/0.88 (declare-const tptp.house_5 $$unsorted) % 0.38/0.88 (declare-const tptp.masserati $$unsorted) % 0.38/0.88 (define @t1 () (@var "Person" $$unsorted)) % 0.38/0.88 (define @t2 () (not (tptp.person @t1))) % 0.38/0.88 (define @t3 () (@list @t1)) % 0.38/0.88 (define @t4 () (@var "H" $$unsorted)) % 0.38/0.88 (define @t5 () (not (tptp.lives tptp.spaniard @t4))) % 0.38/0.88 (define @t6 () (not (tptp.lives tptp.english @t4))) % 0.38/0.88 (define @t7 () (not (tptp.house @t4))) % 0.38/0.88 (define @t8 () (@list @t4)) % 0.38/0.88 (define @t9 () (not (tptp.lives tptp.norwegian @t4))) % 0.38/0.88 (define @t10 () (not (tptp.lives tptp.ukranian @t4))) % 0.38/0.88 (define @t11 () (forall @t8 (or @t7 @t6 @t10))) % 0.38/0.88 (define @t12 () (not (tptp.lives tptp.japanese @t4))) % 0.38/0.88 (define @t13 () (forall @t8 (or @t7 @t6 @t12))) % 0.38/0.88 (define @t14 () (forall @t8 (or @t7 @t5 @t12))) % 0.38/0.88 (define @t15 () (forall @t8 (or @t7 @t10 @t12))) % 0.38/0.88 (define @t16 () (forall @t3 (or @t2 (tptp.drinks @t1 tptp.orange) (tptp.drinks @t1 tptp.coffee) (tptp.drinks @t1 tptp.tea) (tptp.drinks @t1 tptp.milk) (tptp.drinks @t1 tptp.water)))) % 0.38/0.88 (define @t17 () (not (tptp.drinks tptp.spaniard @t4))) % 0.38/0.88 (define @t18 () (not (tptp.drinks tptp.english @t4))) % 0.38/0.88 (define @t19 () (not (tptp.drink @t4))) % 0.38/0.88 (define @t20 () (forall @t8 (or @t19 @t18 @t17))) % 0.38/0.88 (define @t21 () (not (tptp.drinks tptp.norwegian @t4))) % 0.38/0.88 (define @t22 () (forall @t8 (or @t19 @t18 @t21))) % 0.38/0.88 (define @t23 () (not (tptp.drinks tptp.ukranian @t4))) % 0.38/0.88 (define @t24 () (forall @t8 (or @t19 @t18 @t23))) % 0.38/0.88 (define @t25 () (not (tptp.drinks tptp.japanese @t4))) % 0.38/0.88 (define @t26 () (forall @t8 (or @t19 @t18 @t25))) % 0.38/0.88 (define @t27 () (forall @t8 (or @t19 @t17 @t21))) % 0.38/0.88 (define @t28 () (forall @t8 (or @t19 @t17 @t23))) % 0.38/0.88 (define @t29 () (forall @t8 (or @t19 @t17 @t25))) % 0.38/0.88 (define @t30 () (forall @t8 (or @t19 @t21 @t25))) % 0.38/0.88 (define @t31 () (forall @t8 (or @t19 @t23 @t25))) % 0.38/0.88 (define @t32 () (tptp.drives @t1 tptp.masserati)) % 0.38/0.88 (define @t33 () (forall @t3 (or @t2 @t32 (tptp.drives @t1 tptp.saab) (tptp.drives @t1 tptp.porsche) (tptp.drives @t1 tptp.honda) (tptp.drives @t1 tptp.jaguar)))) % 0.38/0.88 (define @t34 () (not (tptp.drives tptp.spaniard @t4))) % 0.38/0.88 (define @t35 () (not (tptp.drives tptp.english @t4))) % 0.38/0.88 (define @t36 () (not (tptp.car @t4))) % 0.38/0.88 (define @t37 () (forall @t8 (or @t36 @t35 @t34))) % 0.38/0.88 (define @t38 () (not (tptp.drives tptp.norwegian @t4))) % 0.38/0.88 (define @t39 () (forall @t8 (or @t36 @t35 @t38))) % 0.38/0.88 (define @t40 () (not (tptp.drives tptp.ukranian @t4))) % 0.38/0.88 (define @t41 () (forall @t8 (or @t36 @t35 @t40))) % 0.38/0.88 (define @t42 () (not (tptp.drives tptp.japanese @t4))) % 0.38/0.88 (define @t43 () (forall @t8 (or @t36 @t35 @t42))) % 0.38/0.88 (define @t44 () (forall @t8 (or @t36 @t34 @t38))) % 0.38/0.88 (define @t45 () (forall @t8 (or @t36 @t34 @t40))) % 0.38/0.88 (define @t46 () (forall @t8 (or @t36 @t34 @t42))) % 0.38/0.88 (define @t47 () (forall @t8 (or @t36 @t38 @t40))) % 0.38/0.88 (define @t48 () (forall @t8 (or @t36 @t38 @t42))) % 0.38/0.88 (define @t49 () (forall @t8 (or @t36 @t40 @t42))) % 0.38/0.88 (define @t50 () (not (tptp.owns tptp.spaniard @t4))) % 0.38/0.88 (define @t51 () (not (tptp.owns tptp.english @t4))) % 0.38/0.88 (define @t52 () (not (tptp.animal @t4))) % 0.38/0.88 (define @t53 () (not (tptp.owns tptp.norwegian @t4))) % 0.38/0.88 (define @t54 () (forall @t8 (or @t52 @t51 @t53))) % 0.38/0.88 (define @t55 () (not (tptp.owns tptp.ukranian @t4))) % 0.38/0.88 (define @t56 () (forall @t8 (or @t52 @t51 @t55))) % 0.38/0.88 (define @t57 () (not (tptp.owns tptp.japanese @t4))) % 0.38/0.88 (define @t58 () (forall @t8 (or @t52 @t53 @t55))) % 0.38/0.88 (define @t59 () (forall @t8 (or @t52 @t53 @t57))) % 0.38/0.88 (define @t60 () (forall @t8 (or @t52 @t55 @t57))) % 0.38/0.88 (define @t61 () (tptp.is_color @t4 tptp.green)) % 0.38/0.88 (define @t62 () (tptp.is_color @t4 tptp.yellow)) % 0.38/0.88 (define @t63 () (tptp.is_color @t4 tptp.red)) % 0.38/0.88 (define @t64 () (forall @t8 (or @t7 @t63 @t62 (tptp.is_color @t4 tptp.blue) @t61 (tptp.is_color @t4 tptp.ivory)))) % 0.38/0.88 (define @t65 () (not (tptp.is_color tptp.house_2 @t4))) % 0.38/0.88 (define @t66 () (not (tptp.is_color tptp.house_1 @t4))) % 0.38/0.88 (define @t67 () (not (tptp.color @t4))) % 0.38/0.88 (define @t68 () (forall @t8 (or @t67 @t66 @t65))) % 0.38/0.88 (define @t69 () (not (tptp.is_color tptp.house_3 @t4))) % 0.38/0.88 (define @t70 () (not (tptp.is_color tptp.house_4 @t4))) % 0.38/0.88 (define @t71 () (forall @t8 (or @t67 @t66 @t70))) % 0.38/0.88 (define @t72 () (not (tptp.is_color tptp.house_5 @t4))) % 0.38/0.88 (define @t73 () (forall @t8 (or @t67 @t70 @t72))) % 0.38/0.88 (define @t74 () (tptp.person tptp.english)) % 0.38/0.88 (define @t75 () (tptp.person tptp.spaniard)) % 0.38/0.88 (define @t76 () (tptp.person tptp.norwegian)) % 0.38/0.88 (define @t77 () (tptp.person tptp.ukranian)) % 0.38/0.88 (define @t78 () (tptp.person tptp.japanese)) % 0.38/0.88 (define @t79 () (tptp.house tptp.house_1)) % 0.38/0.88 (define @t80 () (tptp.house tptp.house_2)) % 0.38/0.88 (define @t81 () (tptp.house tptp.house_3)) % 0.38/0.88 (define @t82 () (tptp.house tptp.house_4)) % 0.38/0.88 (define @t83 () (tptp.house tptp.house_5)) % 0.38/0.88 (define @t84 () (tptp.color tptp.red)) % 0.38/0.88 (define @t85 () (tptp.color tptp.green)) % 0.38/0.88 (define @t86 () (tptp.color tptp.yellow)) % 0.38/0.88 (define @t87 () (tptp.color tptp.ivory)) % 0.38/0.88 (define @t88 () (tptp.color tptp.blue)) % 0.38/0.88 (define @t89 () (tptp.car tptp.jaguar)) % 0.38/0.88 (define @t90 () (tptp.car tptp.honda)) % 0.38/0.88 (define @t91 () (tptp.car tptp.masserati)) % 0.38/0.88 (define @t92 () (tptp.car tptp.porsche)) % 0.38/0.88 (define @t93 () (tptp.car tptp.saab)) % 0.38/0.88 (define @t94 () (tptp.drink tptp.tea)) % 0.38/0.88 (define @t95 () (tptp.drink tptp.orange)) % 0.38/0.88 (define @t96 () (tptp.drink tptp.water)) % 0.38/0.88 (define @t97 () (tptp.drink tptp.coffee)) % 0.38/0.88 (define @t98 () (tptp.animal tptp.dog)) % 0.38/0.88 (define @t99 () (tptp.animal tptp.zebra)) % 0.38/0.88 (define @t100 () (tptp.animal tptp.snails)) % 0.38/0.88 (define @t101 () (tptp.animal tptp.horse)) % 0.38/0.88 (define @t102 () (tptp.animal tptp.fox)) % 0.38/0.88 (define @t103 () (forall @t8 (or @t63 @t7 @t6))) % 0.38/0.88 (define @t104 () (tptp.owns tptp.spaniard tptp.dog)) % 0.38/0.88 (define @t105 () (tptp.lives tptp.norwegian tptp.house_1)) % 0.38/0.88 (define @t106 () (forall (@list @t4 @t1) (or @t62 @t2 (not @t32) @t7 (not (tptp.lives @t1 @t4))))) % 0.38/0.88 (define @t107 () (@var "House_2" $$unsorted)) % 0.38/0.88 (define @t108 () (@var "Person_2" $$unsorted)) % 0.38/0.88 (define @t109 () (not (tptp.lives @t108 @t107))) % 0.38/0.88 (define @t110 () (not (tptp.house @t107))) % 0.38/0.88 (define @t111 () (not (tptp.person @t108))) % 0.38/0.88 (define @t112 () (@var "House_1" $$unsorted)) % 0.38/0.88 (define @t113 () (@var "Person_1" $$unsorted)) % 0.38/0.88 (define @t114 () (not (tptp.lives @t113 @t112))) % 0.38/0.88 (define @t115 () (not (tptp.house @t112))) % 0.38/0.88 (define @t116 () (not (tptp.person @t113))) % 0.38/0.88 (define @t117 () (tptp.next_to @t112 @t107)) % 0.38/0.88 (define @t118 () (@list @t112 @t107 @t113 @t108)) % 0.38/0.88 (define @t119 () (forall @t118 (or @t117 @t116 (not (tptp.owns @t113 tptp.fox)) @t115 @t114 @t111 (not (tptp.drives @t108 tptp.saab)) @t110 @t109))) % 0.38/0.88 (define @t120 () (@list @t107 @t112)) % 0.38/0.88 (define @t121 () (forall @t120 (or (tptp.is_color @t107 tptp.blue) @t115 (not (tptp.lives tptp.norwegian @t112)) @t110 (not @t117)))) % 0.38/0.88 (define @t122 () (@var "P" $$unsorted)) % 0.38/0.88 (define @t123 () (not (tptp.person @t122))) % 0.38/0.88 (define @t124 () (@list @t122)) % 0.38/0.88 (define @t125 () (forall @t124 (or (tptp.owns @t122 tptp.snails) @t123 (not (tptp.drives @t122 tptp.porsche))))) % 0.38/0.88 (define @t126 () (forall @t124 (or (tptp.drinks @t122 tptp.orange) @t123 (not (tptp.drives @t122 tptp.honda))))) % 0.38/0.88 (define @t127 () (tptp.drinks tptp.ukranian tptp.tea)) % 0.38/0.88 (define @t128 () (tptp.drives tptp.japanese tptp.jaguar)) % 0.38/0.88 (define @t129 () (forall @t118 (or @t117 @t116 (not (tptp.drives @t113 tptp.masserati)) @t115 @t114 @t111 (not (tptp.owns @t108 tptp.horse)) @t110 @t109))) % 0.38/0.88 (define @t130 () (forall (@list @t4 @t122) (or @t61 @t123 (not (tptp.drinks @t122 tptp.coffee)) @t7 (not (tptp.lives @t122 @t4))))) % 0.38/0.88 (define @t131 () (forall @t124 (or (tptp.lives @t122 tptp.house_3) @t123 (not (tptp.drinks @t122 tptp.milk))))) % 0.38/0.88 (define @t132 () (@var "Y" $$unsorted)) % 0.38/0.88 (define @t133 () (@var "X" $$unsorted)) % 0.38/0.88 (define @t134 () (tptp.left_of @t133 @t132)) % 0.38/0.88 (define @t135 () (tptp.next_to @t133 @t132)) % 0.38/0.88 (define @t136 () (@list @t133 @t132)) % 0.38/0.88 (define @t137 () (forall @t136 (or @t135 (not @t134)))) % 0.38/0.88 (define @t138 () (tptp.left_of @t132 @t133)) % 0.38/0.88 (define @t139 () (forall @t136 (or @t134 (not @t135) @t138))) % 0.38/0.88 (define @t140 () (tptp.left_of tptp.house_1 tptp.house_2)) % 0.38/0.88 (define @t141 () (tptp.left_of tptp.house_3 tptp.house_4)) % 0.38/0.88 (define @t142 () (tptp.left_of tptp.house_1 tptp.house_1)) % 0.38/0.88 (define @t143 () (tptp.left_of tptp.house_3 tptp.house_1)) % 0.38/0.88 (define @t144 () (tptp.left_of tptp.house_4 tptp.house_1)) % 0.38/0.88 (define @t145 () (tptp.left_of tptp.house_5 tptp.house_1)) % 0.38/0.88 (define @t146 () (tptp.left_of tptp.house_3 tptp.house_2)) % 0.38/0.88 (define @t147 () (tptp.left_of tptp.house_4 tptp.house_2)) % 0.38/0.88 (define @t148 () (tptp.left_of tptp.house_5 tptp.house_2)) % 0.38/0.88 (define @t149 () (tptp.left_of tptp.house_1 tptp.house_3)) % 0.38/0.88 (define @t150 () (tptp.left_of tptp.house_3 tptp.house_3)) % 0.38/0.88 (define @t151 () (tptp.left_of tptp.house_5 tptp.house_3)) % 0.38/0.88 (define @t152 () (tptp.left_of tptp.house_1 tptp.house_4)) % 0.38/0.88 (define @t153 () (tptp.left_of tptp.house_5 tptp.house_4)) % 0.38/0.88 (define @t154 () (tptp.left_of tptp.house_1 tptp.house_5)) % 0.38/0.88 (define @t155 () (tptp.left_of tptp.house_2 tptp.house_5)) % 0.38/0.88 (define @t156 () (tptp.left_of tptp.house_3 tptp.house_5)) % 0.38/0.88 (define @t157 () (tptp.is_color tptp.house_5 tptp.green)) % 0.38/0.88 (define @t158 () (not @t157)) % 0.38/0.88 (define @t159 () (tptp.is_color tptp.house_4 tptp.ivory)) % 0.38/0.88 (define @t160 () (not @t159)) % 0.38/0.88 (define @t161 () (tptp.is_color tptp.house_3 tptp.red)) % 0.38/0.88 (define @t162 () (not @t161)) % 0.38/0.88 (define @t163 () (tptp.is_color tptp.house_2 tptp.blue)) % 0.38/0.88 (define @t164 () (not @t163)) % 0.38/0.88 (define @t165 () (tptp.is_color tptp.house_1 tptp.yellow)) % 0.38/0.88 (define @t166 () (not @t165)) % 0.38/0.88 (define @t167 () (tptp.lives tptp.spaniard tptp.house_4)) % 0.38/0.88 (define @t168 () (not @t167)) % 0.38/0.88 (define @t169 () (tptp.lives tptp.english tptp.house_3)) % 0.38/0.88 (define @t170 () (not @t169)) % 0.38/0.88 (define @t171 () (tptp.lives tptp.japanese tptp.house_5)) % 0.38/0.88 (define @t172 () (not @t171)) % 0.38/0.88 (define @t173 () (tptp.lives tptp.ukranian tptp.house_2)) % 0.38/0.88 (define @t174 () (not @t173)) % 0.38/0.88 (define @t175 () (not @t105)) % 0.38/0.88 (define @t176 () (tptp.drives tptp.spaniard tptp.honda)) % 0.38/0.88 (define @t177 () (not @t176)) % 0.38/0.88 (define @t178 () (tptp.drives tptp.english tptp.porsche)) % 0.38/0.88 (define @t179 () (not @t178)) % 0.38/0.88 (define @t180 () (not @t128)) % 0.38/0.88 (define @t181 () (tptp.drives tptp.ukranian tptp.saab)) % 0.38/0.88 (define @t182 () (not @t181)) % 0.38/0.88 (define @t183 () (tptp.drives tptp.norwegian tptp.masserati)) % 0.38/0.88 (define @t184 () (not @t183)) % 0.38/0.88 (define @t185 () (not @t104)) % 0.38/0.88 (define @t186 () (tptp.owns tptp.english tptp.snails)) % 0.38/0.88 (define @t187 () (not @t186)) % 0.38/0.88 (define @t188 () (tptp.owns tptp.japanese tptp.zebra)) % 0.38/0.88 (define @t189 () (not @t188)) % 0.38/0.88 (define @t190 () (tptp.owns tptp.ukranian tptp.horse)) % 0.38/0.88 (define @t191 () (not @t190)) % 0.38/0.88 (define @t192 () (tptp.owns tptp.norwegian tptp.fox)) % 0.38/0.88 (define @t193 () (not @t192)) % 0.38/0.88 (define @t194 () (tptp.drinks tptp.spaniard tptp.orange)) % 0.38/0.88 (define @t195 () (not @t194)) % 0.38/0.88 (define @t196 () (tptp.drinks tptp.english tptp.milk)) % 0.38/0.88 (define @t197 () (not @t196)) % 0.38/0.88 (define @t198 () (tptp.drinks tptp.japanese tptp.coffee)) % 0.38/0.88 (define @t199 () (not @t198)) % 0.38/0.88 (define @t200 () (not @t127)) % 0.38/0.88 (define @t201 () (tptp.drinks tptp.norwegian tptp.water)) % 0.38/0.88 (define @t202 () (not @t201)) % 0.38/0.88 (define @t203 () (@list tptp.red)) % 0.38/0.88 (define @t204 () (@list tptp.house_3)) % 0.38/0.88 (define @t205 () (not @t81)) % 0.38/0.88 (define @t206 () (or @t161 @t205 @t170)) % 0.38/0.88 (define @t207 () (@list tptp.yellow)) % 0.38/0.88 (define @t208 () (tptp.is_color tptp.house_5 tptp.red)) % 0.38/0.88 (define @t209 () (not @t208)) % 0.38/0.88 (define @t210 () (tptp.is_color tptp.house_1 tptp.red)) % 0.38/0.88 (define @t211 () (not @t210)) % 0.38/0.88 (define @t212 () (not @t84)) % 0.38/0.88 (define @t213 () (or @t212 @t211 @t209)) % 0.38/0.88 (define @t214 () (or @t212 @t211 @t162)) % 0.38/0.88 (define @t215 () (@list tptp.ivory)) % 0.38/0.88 (define @t216 () (tptp.is_color tptp.house_5 tptp.ivory)) % 0.38/0.88 (define @t217 () (not @t216)) % 0.38/0.88 (define @t218 () (tptp.is_color tptp.house_1 tptp.ivory)) % 0.38/0.88 (define @t219 () (not @t218)) % 0.38/0.88 (define @t220 () (not @t87)) % 0.38/0.88 (define @t221 () (or @t220 @t219 @t217)) % 0.38/0.88 (define @t222 () (@list tptp.house_1 tptp.house_5)) % 0.38/0.88 (define @t223 () (not @t79)) % 0.38/0.88 (define @t224 () (not @t83)) % 0.38/0.88 (define @t225 () (or @t154 @t224 @t158 @t223 @t219)) % 0.38/0.88 (define @t226 () (@list tptp.house_5)) % 0.38/0.88 (define @t227 () (@list tptp.blue)) % 0.38/0.88 (define @t228 () (not @t140)) % 0.38/0.88 (define @t229 () (tptp.next_to tptp.house_1 tptp.house_2)) % 0.38/0.88 (define @t230 () (or @t229 @t228)) % 0.38/0.88 (define @t231 () (@list false false)) % 0.38/0.88 (define @t232 () (not @t229)) % 0.38/0.88 (define @t233 () (not @t80)) % 0.38/0.88 (define @t234 () (or @t163 @t223 @t175 @t233 @t232)) % 0.38/0.88 (define @t235 () (tptp.is_color tptp.house_5 tptp.blue)) % 0.38/0.88 (define @t236 () (not @t235)) % 0.38/0.88 (define @t237 () (not @t88)) % 0.38/0.88 (define @t238 () (or @t237 @t164 @t236)) % 0.38/0.88 (define @t239 () (@list false false false)) % 0.38/0.88 (define @t240 () (tptp.is_color tptp.house_5 tptp.yellow)) % 0.38/0.88 (define @t241 () (or @t224 @t208 @t240 @t235 @t157 @t216)) % 0.38/0.88 (define @t242 () (@list true false false true false true false false true false false)) % 0.38/0.88 (define @t243 () (tptp.is_color tptp.house_1 tptp.green)) % 0.38/0.88 (define @t244 () (not @t243)) % 0.38/0.88 (define @t245 () (or @t145 @t223 @t244 @t224 @t217)) % 0.38/0.88 (define @t246 () (@list tptp.green)) % 0.38/0.88 (define @t247 () (not @t85)) % 0.38/0.88 (define @t248 () (or @t247 @t244 @t158)) % 0.38/0.88 (define @t249 () (@list true false false true false false true false true false false)) % 0.38/0.88 (define @t250 () (tptp.is_color tptp.house_3 tptp.green)) % 0.38/0.88 (define @t251 () (not @t250)) % 0.38/0.88 (define @t252 () (or @t151 @t205 @t251 @t224 @t217)) % 0.38/0.88 (define @t253 () (or @t247 @t251 @t158)) % 0.38/0.88 (define @t254 () (tptp.is_color tptp.house_3 tptp.blue)) % 0.38/0.88 (define @t255 () (not @t254)) % 0.38/0.88 (define @t256 () (or @t237 @t164 @t255)) % 0.38/0.88 (define @t257 () (tptp.is_color tptp.house_3 tptp.ivory)) % 0.38/0.88 (define @t258 () (tptp.is_color tptp.house_3 tptp.yellow)) % 0.38/0.88 (define @t259 () (or @t205 @t161 @t258 @t254 @t250 @t257)) % 0.38/0.88 (define @t260 () (not @t257)) % 0.38/0.88 (define @t261 () (or @t220 @t260 @t217)) % 0.38/0.88 (define @t262 () (or @t156 @t224 @t158 @t205 @t260)) % 0.38/0.88 (define @t263 () (tptp.is_color tptp.house_2 tptp.red)) % 0.38/0.88 (define @t264 () (not @t263)) % 0.38/0.88 (define @t265 () (or @t212 @t211 @t264)) % 0.38/0.88 (define @t266 () (tptp.is_color tptp.house_4 tptp.red)) % 0.38/0.88 (define @t267 () (not @t266)) % 0.38/0.88 (define @t268 () (or @t212 @t211 @t267)) % 0.38/0.88 (define @t269 () (@list tptp.house_2)) % 0.38/0.88 (define @t270 () (tptp.lives tptp.english tptp.house_2)) % 0.38/0.88 (define @t271 () (not @t270)) % 0.38/0.88 (define @t272 () (or @t263 @t233 @t271)) % 0.38/0.88 (define @t273 () (@list tptp.house_4)) % 0.38/0.88 (define @t274 () (tptp.lives tptp.english tptp.house_4)) % 0.38/0.88 (define @t275 () (not @t274)) % 0.38/0.88 (define @t276 () (not @t82)) % 0.38/0.88 (define @t277 () (or @t266 @t276 @t275)) % 0.38/0.88 (define @t278 () (tptp.lives tptp.english tptp.house_5)) % 0.38/0.88 (define @t279 () (not @t278)) % 0.38/0.88 (define @t280 () (or @t208 @t224 @t279)) % 0.38/0.88 (define @t281 () (@list tptp.english)) % 0.38/0.88 (define @t282 () (@list tptp.house_1)) % 0.38/0.88 (define @t283 () (tptp.lives tptp.english tptp.house_1)) % 0.38/0.88 (define @t284 () (not @t283)) % 0.38/0.88 (define @t285 () (or @t223 @t284 @t175)) % 0.38/0.88 (define @t286 () (not @t74)) % 0.38/0.88 (define @t287 () (or @t286 @t283 @t270 @t169 @t274 @t278)) % 0.38/0.88 (define @t288 () (not @t258)) % 0.38/0.88 (define @t289 () (not @t86)) % 0.38/0.88 (define @t290 () (or @t289 @t166 @t288)) % 0.38/0.88 (define @t291 () (tptp.is_color tptp.house_1 tptp.blue)) % 0.38/0.88 (define @t292 () (not @t291)) % 0.38/0.88 (define @t293 () (or @t237 @t292 @t164)) % 0.38/0.88 (define @t294 () (or @t223 @t210 @t165 @t291 @t243 @t218)) % 0.38/0.88 (define @t295 () (@list true false false true false false)) % 0.38/0.88 (define @t296 () (tptp.is_color tptp.house_2 tptp.yellow)) % 0.38/0.88 (define @t297 () (not @t296)) % 0.38/0.88 (define @t298 () (or @t289 @t297 @t288)) % 0.38/0.88 (define @t299 () (or @t289 @t166 @t297)) % 0.38/0.88 (define @t300 () (or @t220 @t219 @t260)) % 0.38/0.88 (define @t301 () (@list tptp.house_1 tptp.house_3)) % 0.38/0.88 (define @t302 () (or @t149 @t205 @t251 @t223 @t219)) % 0.38/0.88 (define @t303 () (or @t247 @t244 @t251)) % 0.38/0.88 (define @t304 () (or @t143 @t223 @t244 @t205 @t260)) % 0.38/0.88 (define @t305 () (or @t169 @t286 @t197)) % 0.38/0.88 (define @t306 () (or @t212 @t264 @t209)) % 0.38/0.88 (define @t307 () (or @t212 @t267 @t209)) % 0.38/0.88 (define @t308 () (or @t224 @t279 @t172)) % 0.38/0.88 (define @t309 () (@list tptp.house_5 tptp.english)) % 0.38/0.88 (define @t310 () (tptp.drives tptp.english tptp.masserati)) % 0.38/0.88 (define @t311 () (not @t310)) % 0.38/0.88 (define @t312 () (or @t240 @t286 @t311 @t224 @t279)) % 0.38/0.88 (define @t313 () (tptp.is_color tptp.house_4 tptp.yellow)) % 0.38/0.88 (define @t314 () (not @t313)) % 0.38/0.88 (define @t315 () (or @t289 @t288 @t314)) % 0.38/0.88 (define @t316 () (tptp.is_color tptp.house_4 tptp.blue)) % 0.38/0.88 (define @t317 () (not @t316)) % 0.38/0.88 (define @t318 () (or @t237 @t164 @t317)) % 0.38/0.88 (define @t319 () (tptp.is_color tptp.house_4 tptp.green)) % 0.38/0.88 (define @t320 () (or @t276 @t266 @t313 @t316 @t319 @t159)) % 0.38/0.88 (define @t321 () (or @t144 @t223 @t244 @t276 @t160)) % 0.38/0.88 (define @t322 () (or @t220 @t219 @t160)) % 0.38/0.88 (define @t323 () (not @t319)) % 0.38/0.88 (define @t324 () (or @t247 @t244 @t323)) % 0.38/0.88 (define @t325 () (@list tptp.house_1 tptp.house_4)) % 0.38/0.88 (define @t326 () (or @t152 @t276 @t323 @t223 @t219)) % 0.38/0.88 (define @t327 () (tptp.is_color tptp.house_2 tptp.green)) % 0.38/0.88 (define @t328 () (not @t327)) % 0.38/0.88 (define @t329 () (or @t247 @t328 @t251)) % 0.38/0.88 (define @t330 () (or @t146 @t233 @t328 @t205 @t260)) % 0.38/0.88 (define @t331 () (tptp.lives tptp.spaniard tptp.house_3)) % 0.38/0.88 (define @t332 () (not @t331)) % 0.38/0.88 (define @t333 () (tptp.drives tptp.spaniard tptp.masserati)) % 0.38/0.88 (define @t334 () (not @t333)) % 0.38/0.88 (define @t335 () (not @t75)) % 0.38/0.88 (define @t336 () (or @t258 @t335 @t334 @t205 @t332)) % 0.38/0.88 (define @t337 () (or @t313 @t335 @t334 @t276 @t168)) % 0.38/0.88 (define @t338 () (@list tptp.house_2 tptp.spaniard)) % 0.38/0.88 (define @t339 () (tptp.lives tptp.spaniard tptp.house_2)) % 0.38/0.88 (define @t340 () (not @t339)) % 0.38/0.88 (define @t341 () (or @t296 @t335 @t334 @t233 @t340)) % 0.38/0.88 (define @t342 () (tptp.lives tptp.spaniard tptp.house_5)) % 0.38/0.88 (define @t343 () (not @t342)) % 0.38/0.88 (define @t344 () (or @t240 @t335 @t334 @t224 @t343)) % 0.38/0.88 (define @t345 () (@list tptp.spaniard)) % 0.38/0.88 (define @t346 () (tptp.lives tptp.spaniard tptp.house_1)) % 0.38/0.88 (define @t347 () (not @t346)) % 0.38/0.88 (define @t348 () (or @t223 @t347 @t175)) % 0.38/0.88 (define @t349 () (or @t335 @t346 @t339 @t331 @t167 @t342)) % 0.38/0.88 (define @t350 () (or @t289 @t166 @t314)) % 0.38/0.88 (define @t351 () (tptp.drinks tptp.norwegian tptp.coffee)) % 0.38/0.88 (define @t352 () (not @t351)) % 0.38/0.88 (define @t353 () (not @t76)) % 0.38/0.88 (define @t354 () (or @t243 @t353 @t352 @t223 @t175)) % 0.38/0.88 (define @t355 () (tptp.drinks tptp.english tptp.coffee)) % 0.38/0.88 (define @t356 () (not @t355)) % 0.38/0.88 (define @t357 () (or @t157 @t286 @t356 @t224 @t279)) % 0.38/0.88 (define @t358 () (@list tptp.orange)) % 0.38/0.88 (define @t359 () (tptp.drinks tptp.ukranian tptp.orange)) % 0.38/0.88 (define @t360 () (not @t359)) % 0.38/0.88 (define @t361 () (tptp.drinks tptp.english tptp.orange)) % 0.38/0.88 (define @t362 () (not @t361)) % 0.38/0.88 (define @t363 () (not @t95)) % 0.38/0.88 (define @t364 () (or @t363 @t362 @t360)) % 0.38/0.88 (define @t365 () (tptp.drinks tptp.norwegian tptp.orange)) % 0.38/0.88 (define @t366 () (not @t365)) % 0.38/0.88 (define @t367 () (or @t363 @t366 @t360)) % 0.38/0.88 (define @t368 () (@list tptp.tea)) % 0.38/0.88 (define @t369 () (tptp.drinks tptp.english tptp.tea)) % 0.38/0.88 (define @t370 () (not @t369)) % 0.38/0.88 (define @t371 () (not @t94)) % 0.38/0.88 (define @t372 () (or @t371 @t370 @t200)) % 0.38/0.88 (define @t373 () (tptp.drinks tptp.english tptp.water)) % 0.38/0.88 (define @t374 () (or @t286 @t361 @t355 @t369 @t196 @t373)) % 0.38/0.88 (define @t375 () (@list tptp.norwegian)) % 0.38/0.88 (define @t376 () (not @t141)) % 0.38/0.88 (define @t377 () (tptp.next_to tptp.house_3 tptp.house_4)) % 0.38/0.88 (define @t378 () (or @t377 @t376)) % 0.38/0.88 (define @t379 () (not @t377)) % 0.38/0.88 (define @t380 () (tptp.lives tptp.norwegian tptp.house_3)) % 0.38/0.88 (define @t381 () (not @t380)) % 0.38/0.88 (define @t382 () (or @t316 @t205 @t381 @t276 @t379)) % 0.38/0.88 (define @t383 () (tptp.drinks tptp.norwegian tptp.milk)) % 0.38/0.88 (define @t384 () (not @t383)) % 0.38/0.88 (define @t385 () (or @t380 @t353 @t384)) % 0.38/0.88 (define @t386 () (@list false true false)) % 0.38/0.88 (define @t387 () (tptp.drinks tptp.norwegian tptp.tea)) % 0.38/0.88 (define @t388 () (not @t387)) % 0.38/0.88 (define @t389 () (or @t371 @t388 @t200)) % 0.38/0.88 (define @t390 () (or @t353 @t365 @t351 @t387 @t383 @t201)) % 0.38/0.88 (define @t391 () (@list tptp.water)) % 0.38/0.88 (define @t392 () (not @t373)) % 0.38/0.88 (define @t393 () (not @t96)) % 0.38/0.88 (define @t394 () (or @t393 @t392 @t202)) % 0.38/0.88 (define @t395 () (or @t363 @t195 @t366)) % 0.38/0.88 (define @t396 () (or @t363 @t362 @t195)) % 0.38/0.88 (define @t397 () (@list tptp.ukranian)) % 0.38/0.88 (define @t398 () (tptp.drives tptp.ukranian tptp.honda)) % 0.38/0.88 (define @t399 () (not @t398)) % 0.38/0.88 (define @t400 () (not @t77)) % 0.38/0.88 (define @t401 () (or @t359 @t400 @t399)) % 0.38/0.88 (define @t402 () (or @t194 @t335 @t177)) % 0.38/0.88 (define @t403 () (@list tptp.jaguar)) % 0.38/0.88 (define @t404 () (tptp.drives tptp.spaniard tptp.jaguar)) % 0.38/0.88 (define @t405 () (not @t404)) % 0.38/0.88 (define @t406 () (not @t89)) % 0.38/0.88 (define @t407 () (or @t406 @t405 @t180)) % 0.38/0.88 (define @t408 () (@list tptp.snails)) % 0.38/0.88 (define @t409 () (tptp.owns tptp.norwegian tptp.snails)) % 0.38/0.88 (define @t410 () (not @t409)) % 0.38/0.88 (define @t411 () (tptp.owns tptp.spaniard tptp.snails)) % 0.38/0.88 (define @t412 () (not @t411)) % 0.38/0.88 (define @t413 () (not @t100)) % 0.38/0.88 (define @t414 () (or @t413 @t412 @t410)) % 0.38/0.88 (define @t415 () (tptp.owns tptp.ukranian tptp.snails)) % 0.38/0.88 (define @t416 () (not @t415)) % 0.38/0.88 (define @t417 () (or @t413 @t412 @t416)) % 0.38/0.88 (define @t418 () (tptp.owns tptp.japanese tptp.snails)) % 0.38/0.88 (define @t419 () (not @t418)) % 0.38/0.88 (define @t420 () (or @t413 @t412 @t419)) % 0.38/0.88 (define @t421 () (or @t413 @t187 @t412)) % 0.38/0.88 (define @t422 () (@list tptp.fox)) % 0.38/0.88 (define @t423 () (tptp.owns tptp.ukranian tptp.fox)) % 0.38/0.88 (define @t424 () (not @t423)) % 0.38/0.88 (define @t425 () (tptp.owns tptp.english tptp.fox)) % 0.38/0.88 (define @t426 () (not @t425)) % 0.38/0.88 (define @t427 () (not @t102)) % 0.38/0.88 (define @t428 () (or @t427 @t426 @t424)) % 0.38/0.88 (define @t429 () (tptp.owns tptp.japanese tptp.fox)) % 0.38/0.88 (define @t430 () (not @t429)) % 0.38/0.88 (define @t431 () (or @t427 @t426 @t430)) % 0.38/0.88 (define @t432 () (or @t427 @t426 @t193)) % 0.38/0.88 (define @t433 () (@list tptp.horse)) % 0.38/0.88 (define @t434 () (tptp.owns tptp.norwegian tptp.horse)) % 0.38/0.88 (define @t435 () (not @t434)) % 0.38/0.88 (define @t436 () (not @t101)) % 0.38/0.88 (define @t437 () (or @t436 @t435 @t191)) % 0.38/0.88 (define @t438 () (tptp.owns tptp.japanese tptp.horse)) % 0.38/0.88 (define @t439 () (not @t438)) % 0.38/0.88 (define @t440 () (or @t436 @t191 @t439)) % 0.38/0.88 (define @t441 () (@list tptp.dog)) % 0.38/0.88 (define @t442 () (tptp.owns tptp.norwegian tptp.dog)) % 0.38/0.88 (define @t443 () (not @t442)) % 0.38/0.88 (define @t444 () (not @t98)) % 0.38/0.88 (define @t445 () (or @t444 @t185 @t443)) % 0.38/0.88 (define @t446 () (tptp.owns tptp.norwegian tptp.zebra)) % 0.38/0.88 (define @t447 () (or @t353 @t442 @t409 @t434 @t192 @t446)) % 0.38/0.88 (define @t448 () (@list tptp.japanese)) % 0.38/0.88 (define @t449 () (tptp.owns tptp.japanese tptp.dog)) % 0.38/0.88 (define @t450 () (not @t449)) % 0.38/0.88 (define @t451 () (or @t444 @t185 @t450)) % 0.38/0.88 (define @t452 () (not @t78)) % 0.38/0.88 (define @t453 () (or @t452 @t449 @t418 @t438 @t429 @t188)) % 0.38/0.88 (define @t454 () (@list tptp.zebra)) % 0.38/0.88 (define @t455 () (not @t446)) % 0.38/0.88 (define @t456 () (not @t99)) % 0.38/0.88 (define @t457 () (or @t456 @t455 @t189)) % 0.38/0.88 (define @t458 () (@list false false false true false false false true false false true false false true false false)) % 0.38/0.88 (define @t459 () (tptp.owns tptp.ukranian tptp.dog)) % 0.38/0.88 (define @t460 () (not @t459)) % 0.38/0.88 (define @t461 () (or @t444 @t185 @t460)) % 0.38/0.88 (define @t462 () (tptp.owns tptp.ukranian tptp.zebra)) % 0.38/0.88 (define @t463 () (or @t400 @t459 @t415 @t190 @t423 @t462)) % 0.38/0.88 (define @t464 () (not @t462)) % 0.38/0.88 (define @t465 () (or @t456 @t455 @t464)) % 0.38/0.88 (define @t466 () (or @t456 @t464 @t189)) % 0.38/0.88 (define @t467 () (or @t436 @t435 @t439)) % 0.38/0.88 (define @t468 () (tptp.owns tptp.english tptp.horse)) % 0.38/0.88 (define @t469 () (not @t468)) % 0.38/0.88 (define @t470 () (or @t436 @t469 @t439)) % 0.38/0.88 (define @t471 () (tptp.owns tptp.english tptp.dog)) % 0.38/0.88 (define @t472 () (not @t471)) % 0.38/0.88 (define @t473 () (or @t444 @t472 @t185)) % 0.38/0.88 (define @t474 () (tptp.owns tptp.english tptp.zebra)) % 0.38/0.88 (define @t475 () (or @t286 @t471 @t186 @t468 @t425 @t474)) % 0.38/0.88 (define @t476 () (not @t474)) % 0.38/0.88 (define @t477 () (or @t456 @t476 @t455)) % 0.38/0.88 (define @t478 () (or @t427 @t424 @t430)) % 0.38/0.88 (define @t479 () (or @t427 @t193 @t430)) % 0.38/0.88 (define @t480 () (or @t436 @t469 @t191)) % 0.38/0.88 (define @t481 () (or @t436 @t469 @t435)) % 0.38/0.88 (define @t482 () (or @t456 @t476 @t464)) % 0.38/0.88 (define @t483 () (or @t456 @t476 @t189)) % 0.38/0.88 (define @t484 () (or @t427 @t193 @t424)) % 0.38/0.88 (define @t485 () (tptp.drives tptp.spaniard tptp.porsche)) % 0.38/0.88 (define @t486 () (not @t485)) % 0.38/0.88 (define @t487 () (or @t411 @t335 @t486)) % 0.38/0.88 (define @t488 () (tptp.drives tptp.spaniard tptp.saab)) % 0.38/0.88 (define @t489 () (or @t335 @t333 @t488 @t485 @t176 @t404)) % 0.38/0.88 (define @t490 () (@list tptp.saab)) % 0.38/0.88 (define @t491 () (not @t488)) % 0.38/0.88 (define @t492 () (tptp.drives tptp.english tptp.saab)) % 0.38/0.88 (define @t493 () (not @t492)) % 0.38/0.88 (define @t494 () (not @t93)) % 0.38/0.88 (define @t495 () (or @t494 @t493 @t491)) % 0.38/0.88 (define @t496 () (tptp.drives tptp.norwegian tptp.saab)) % 0.38/0.88 (define @t497 () (not @t496)) % 0.38/0.88 (define @t498 () (or @t494 @t491 @t497)) % 0.38/0.88 (define @t499 () (or @t494 @t491 @t182)) % 0.38/0.88 (define @t500 () (tptp.lives tptp.ukranian tptp.house_3)) % 0.38/0.88 (define @t501 () (not @t500)) % 0.38/0.88 (define @t502 () (tptp.drives tptp.ukranian tptp.masserati)) % 0.38/0.88 (define @t503 () (not @t502)) % 0.38/0.88 (define @t504 () (or @t258 @t400 @t503 @t205 @t501)) % 0.38/0.88 (define @t505 () (tptp.lives tptp.ukranian tptp.house_4)) % 0.38/0.88 (define @t506 () (not @t505)) % 0.38/0.88 (define @t507 () (or @t313 @t400 @t503 @t276 @t506)) % 0.38/0.88 (define @t508 () (tptp.lives tptp.ukranian tptp.house_5)) % 0.38/0.88 (define @t509 () (not @t508)) % 0.38/0.88 (define @t510 () (or @t240 @t400 @t503 @t224 @t509)) % 0.38/0.88 (define @t511 () (tptp.lives tptp.ukranian tptp.house_1)) % 0.38/0.88 (define @t512 () (not @t511)) % 0.38/0.88 (define @t513 () (or @t223 @t175 @t512)) % 0.38/0.88 (define @t514 () (or @t400 @t511 @t173 @t500 @t505 @t508)) % 0.38/0.88 (define @t515 () (or @t296 @t400 @t503 @t233 @t174)) % 0.38/0.88 (define @t516 () (tptp.drives tptp.ukranian tptp.jaguar)) % 0.38/0.88 (define @t517 () (not @t516)) % 0.38/0.88 (define @t518 () (or @t406 @t517 @t180)) % 0.38/0.88 (define @t519 () (tptp.drives tptp.ukranian tptp.porsche)) % 0.38/0.88 (define @t520 () (or @t400 @t502 @t181 @t519 @t398 @t516)) % 0.38/0.88 (define @t521 () (@list tptp.porsche)) % 0.38/0.88 (define @t522 () (not @t519)) % 0.38/0.88 (define @t523 () (tptp.drives tptp.norwegian tptp.porsche)) % 0.38/0.88 (define @t524 () (not @t523)) % 0.38/0.88 (define @t525 () (not @t92)) % 0.38/0.88 (define @t526 () (or @t525 @t524 @t522)) % 0.38/0.88 (define @t527 () (or @t525 @t179 @t522)) % 0.38/0.88 (define @t528 () (tptp.drives tptp.english tptp.jaguar)) % 0.38/0.88 (define @t529 () (not @t528)) % 0.38/0.88 (define @t530 () (or @t406 @t529 @t180)) % 0.38/0.88 (define @t531 () (tptp.drives tptp.english tptp.honda)) % 0.38/0.88 (define @t532 () (or @t286 @t310 @t492 @t178 @t531 @t528)) % 0.38/0.88 (define @t533 () (tptp.drives tptp.norwegian tptp.honda)) % 0.38/0.88 (define @t534 () (not @t533)) % 0.38/0.88 (define @t535 () (not @t531)) % 0.38/0.88 (define @t536 () (not @t90)) % 0.38/0.88 (define @t537 () (or @t536 @t535 @t534)) % 0.38/0.88 (define @t538 () (or @t361 @t286 @t535)) % 0.38/0.88 (define @t539 () (tptp.drives tptp.norwegian tptp.jaguar)) % 0.38/0.88 (define @t540 () (not @t539)) % 0.38/0.88 (define @t541 () (or @t406 @t540 @t180)) % 0.38/0.88 (define @t542 () (or @t353 @t183 @t496 @t523 @t533 @t539)) % 0.38/0.88 (define @t543 () (or @t363 @t362 @t366)) % 0.38/0.88 (define @t544 () (tptp.drinks tptp.japanese tptp.orange)) % 0.38/0.88 (define @t545 () (not @t544)) % 0.38/0.88 (define @t546 () (or @t363 @t362 @t545)) % 0.38/0.88 (define @t547 () (tptp.drinks tptp.japanese tptp.water)) % 0.38/0.88 (define @t548 () (not @t547)) % 0.38/0.88 (define @t549 () (or @t393 @t202 @t548)) % 0.38/0.88 (define @t550 () (or @t415 @t400 @t522)) % 0.38/0.88 (define @t551 () (or @t413 @t416 @t419)) % 0.38/0.88 (define @t552 () (or @t413 @t187 @t416)) % 0.38/0.88 (define @t553 () (@list tptp.house_1 tptp.house_5 tptp.norwegian tptp.english)) % 0.38/0.88 (define @t554 () (tptp.next_to tptp.house_1 tptp.house_5)) % 0.38/0.88 (define @t555 () (or @t554 @t353 @t184 @t223 @t175 @t286 @t469 @t224 @t279)) % 0.38/0.88 (define @t556 () (not @t554)) % 0.38/0.88 (define @t557 () (or @t154 @t556 @t145)) % 0.38/0.88 (define @t558 () (or @t413 @t410 @t416)) % 0.38/0.88 (define @t559 () (@list tptp.house_1 tptp.house_1 tptp.norwegian tptp.norwegian)) % 0.38/0.88 (define @t560 () (tptp.next_to tptp.house_1 tptp.house_1)) % 0.38/0.88 (define @t561 () (or @t560 @t353 @t184 @t223 @t175 @t353 @t435 @t223 @t175)) % 0.38/0.88 (define @t562 () (@list tptp.house_1 tptp.house_1)) % 0.38/0.88 (define @t563 () (not @t560)) % 0.38/0.88 (define @t564 () (or @t142 @t563 @t142)) % 0.38/0.88 (define @t565 () (tptp.drinks tptp.spaniard tptp.milk)) % 0.38/0.88 (define @t566 () (not @t565)) % 0.38/0.88 (define @t567 () (or @t331 @t335 @t566)) % 0.38/0.88 (define @t568 () (or @t153 @t276 @t323 @t224 @t217)) % 0.38/0.88 (define @t569 () (or @t247 @t323 @t158)) % 0.38/0.88 (define @t570 () (or @t212 @t162 @t267)) % 0.38/0.88 (define @t571 () (or @t212 @t264 @t162)) % 0.38/0.88 (define @t572 () (or @t220 @t160 @t217)) % 0.38/0.88 (define @t573 () (or @t147 @t233 @t328 @t276 @t160)) % 0.38/0.88 (define @t574 () (or @t205 @t170 @t501)) % 0.38/0.88 (define @t575 () (tptp.lives tptp.japanese tptp.house_3)) % 0.38/0.88 (define @t576 () (not @t575)) % 0.38/0.88 (define @t577 () (or @t205 @t170 @t576)) % 0.38/0.88 (define @t578 () (or @t258 @t286 @t311 @t205 @t170)) % 0.38/0.88 (define @t579 () (tptp.next_to tptp.house_1 tptp.house_4)) % 0.38/0.88 (define @t580 () (not @t579)) % 0.38/0.88 (define @t581 () (or @t152 @t580 @t144)) % 0.38/0.88 (define @t582 () (@list true true false)) % 0.38/0.88 (define @t583 () (or @t579 @t353 @t193 @t223 @t175 @t335 @t491 @t276 @t168)) % 0.38/0.88 (define @t584 () (or @t554 @t353 @t193 @t223 @t175 @t335 @t491 @t224 @t343)) % 0.38/0.88 (define @t585 () (tptp.drinks tptp.spaniard tptp.coffee)) % 0.38/0.88 (define @t586 () (not @t585)) % 0.38/0.88 (define @t587 () (or @t327 @t335 @t586 @t233 @t340)) % 0.38/0.88 (define @t588 () (tptp.drinks tptp.spaniard tptp.tea)) % 0.38/0.88 (define @t589 () (not @t588)) % 0.38/0.88 (define @t590 () (or @t371 @t589 @t200)) % 0.38/0.88 (define @t591 () (tptp.drinks tptp.spaniard tptp.water)) % 0.38/0.88 (define @t592 () (or @t335 @t194 @t585 @t588 @t565 @t591)) % 0.38/0.88 (define @t593 () (not @t591)) % 0.38/0.88 (define @t594 () (or @t393 @t593 @t202)) % 0.38/0.88 (define @t595 () (or @t233 @t340 @t174)) % 0.38/0.88 (define @t596 () (tptp.drinks tptp.japanese tptp.milk)) % 0.38/0.88 (define @t597 () (not @t596)) % 0.38/0.88 (define @t598 () (or @t575 @t452 @t597)) % 0.38/0.88 (define @t599 () (or @t363 @t195 @t360)) % 0.38/0.88 (define @t600 () (or @t363 @t195 @t545)) % 0.38/0.88 (define @t601 () (or @t365 @t353 @t534)) % 0.38/0.88 (define @t602 () (tptp.drinks tptp.japanese tptp.tea)) % 0.38/0.88 (define @t603 () (not @t602)) % 0.38/0.88 (define @t604 () (or @t371 @t200 @t603)) % 0.38/0.88 (define @t605 () (or @t452 @t544 @t198 @t602 @t596 @t547)) % 0.38/0.88 (define @t606 () (tptp.lives tptp.japanese tptp.house_2)) % 0.38/0.88 (define @t607 () (not @t606)) % 0.38/0.88 (define @t608 () (or @t327 @t452 @t199 @t233 @t607)) % 0.38/0.88 (define @t609 () (tptp.lives tptp.japanese tptp.house_4)) % 0.38/0.88 (define @t610 () (not @t609)) % 0.38/0.88 (define @t611 () (or @t319 @t452 @t199 @t276 @t610)) % 0.38/0.88 (define @t612 () (tptp.lives tptp.japanese tptp.house_1)) % 0.38/0.88 (define @t613 () (not @t612)) % 0.38/0.88 (define @t614 () (or @t223 @t175 @t613)) % 0.38/0.88 (define @t615 () (or @t452 @t612 @t606 @t575 @t609 @t171)) % 0.38/0.88 (define @t616 () (or @t224 @t343 @t172)) % 0.38/0.88 (define @t617 () (@list tptp.coffee)) % 0.38/0.88 (define @t618 () (not @t97)) % 0.38/0.88 (define @t619 () (or @t618 @t356 @t199)) % 0.38/0.88 (define @t620 () (or @t224 @t509 @t172)) % 0.38/0.88 (define @t621 () (or @t560 @t353 @t193 @t223 @t175 @t353 @t497 @t223 @t175)) % 0.38/0.88 (define @t622 () (or @t186 @t286 @t179)) % 0.38/0.88 (define @t623 () (or @t413 @t187 @t410)) % 0.38/0.88 (define @t624 () (or @t413 @t187 @t419)) % 0.38/0.88 (define @t625 () (or @t409 @t353 @t524)) % 0.38/0.88 (define @t626 () (not @t91)) % 0.38/0.88 (define @t627 () (or @t626 @t184 @t503)) % 0.38/0.88 (define @t628 () (or @t579 @t353 @t184 @t223 @t175 @t400 @t191 @t276 @t506)) % 0.38/0.88 (define @t629 () (or @t494 @t493 @t182)) % 0.38/0.88 (define @t630 () (tptp.next_to tptp.house_1 tptp.house_3)) % 0.38/0.88 (define @t631 () (not @t630)) % 0.38/0.88 (define @t632 () (or @t149 @t631 @t143)) % 0.38/0.88 (define @t633 () (or @t630 @t353 @t184 @t223 @t175 @t286 @t469 @t205 @t170)) % 0.38/0.88 (define @t634 () (or @t494 @t497 @t182)) % 0.38/0.88 (define @t635 () (or @t494 @t493 @t497)) % 0.38/0.88 (define @t636 () (or @t212 @t162 @t209)) % 0.38/0.88 (define @t637 () (or @t224 @t279 @t343)) % 0.38/0.88 (define @t638 () (or @t393 @t392 @t593)) % 0.38/0.88 (define @t639 () (or @t205 @t332 @t501)) % 0.38/0.88 (define @t640 () (or @t205 @t332 @t576)) % 0.38/0.88 (define @t641 () (or @t224 @t279 @t509)) % 0.38/0.88 (define @t642 () (or @t276 @t506 @t610)) % 0.38/0.88 (define @t643 () (or @t554 @t353 @t193 @t223 @t175 @t286 @t493 @t224 @t279)) % 0.38/0.88 (define @t644 () (or @t579 @t353 @t184 @t223 @t175 @t452 @t439 @t276 @t610)) % 0.38/0.88 (define @t645 () (or @t630 @t353 @t184 @t223 @t175 @t452 @t439 @t205 @t576)) % 0.38/0.88 (define @t646 () (or @t205 @t170 @t332)) % 0.38/0.88 (define @t647 () (or @t618 @t586 @t199)) % 0.38/0.88 (define @t648 () (or @t363 @t360 @t545)) % 0.38/0.88 (define @t649 () (or @t554 @t353 @t184 @t223 @t175 @t452 @t439 @t224 @t172)) % 0.38/0.88 (define @t650 () (@list true false)) % 0.38/0.88 (define @t651 () (tptp.next_to tptp.house_5 tptp.house_2)) % 0.38/0.88 (define @t652 () (not @t651)) % 0.38/0.88 (define @t653 () (or @t148 @t652 @t155)) % 0.38/0.88 (define @t654 () (or @t651 @t452 @t430 @t224 @t172 @t400 @t182 @t233 @t174)) % 0.38/0.88 (define @t655 () (tptp.next_to tptp.house_3 tptp.house_3)) % 0.38/0.88 (define @t656 () (not @t655)) % 0.38/0.88 (define @t657 () (or @t150 @t656 @t150)) % 0.38/0.88 (define @t658 () (or @t655 @t286 @t426 @t205 @t170 @t286 @t493 @t205 @t170)) % 0.38/0.88 (define @t659 () (not @t240)) % 0.38/0.88 (define @t660 () (or @t289 @t288 @t659)) % 0.38/0.88 (define @t661 () (or @t289 @t166 @t659)) % 0.38/0.88 (define @t662 () (or @t289 @t314 @t659)) % 0.38/0.88 (assume @p1 (forall @t3 (or @t2 (tptp.lives @t1 tptp.house_1) (tptp.lives @t1 tptp.house_2) (tptp.lives @t1 tptp.house_3) (tptp.lives @t1 tptp.house_4) (tptp.lives @t1 tptp.house_5)))) % 0.38/0.88 (assume @p2 (forall @t8 (or @t7 @t6 @t5))) % 0.38/0.88 (assume @p3 (forall @t8 (or @t7 @t6 @t9))) % 0.38/0.88 (assume @p4 @t11) % 0.38/0.88 (assume @p5 @t13) % 0.38/0.88 (assume @p6 (forall @t8 (or @t7 @t5 @t9))) % 0.38/0.88 (assume @p7 (forall @t8 (or @t7 @t5 @t10))) % 0.38/0.88 (assume @p8 @t14) % 0.38/0.88 (assume @p9 (forall @t8 (or @t7 @t9 @t10))) % 0.38/0.88 (assume @p10 (forall @t8 (or @t7 @t9 @t12))) % 0.38/0.88 (assume @p11 @t15) % 0.38/0.88 (assume @p12 @t16) % 0.38/0.88 (assume @p13 @t20) % 0.38/0.88 (assume @p14 @t22) % 0.38/0.88 (assume @p15 @t24) % 0.38/0.88 (assume @p16 @t26) % 0.38/0.88 (assume @p17 @t27) % 0.38/0.88 (assume @p18 @t28) % 0.38/0.88 (assume @p19 @t29) % 0.38/0.88 (assume @p20 (forall @t8 (or @t19 @t21 @t23))) % 0.38/0.88 (assume @p21 @t30) % 0.38/0.88 (assume @p22 @t31) % 0.38/0.88 (assume @p23 @t33) % 0.38/0.88 (assume @p24 @t37) % 0.38/0.88 (assume @p25 @t39) % 0.38/0.88 (assume @p26 @t41) % 0.38/0.88 (assume @p27 @t43) % 0.38/0.88 (assume @p28 @t44) % 0.38/0.88 (assume @p29 @t45) % 0.38/0.88 (assume @p30 @t46) % 0.38/0.88 (assume @p31 @t47) % 0.38/0.88 (assume @p32 @t48) % 0.38/0.88 (assume @p33 @t49) % 0.38/0.88 (assume @p34 (forall @t3 (or @t2 (tptp.owns @t1 tptp.dog) (tptp.owns @t1 tptp.snails) (tptp.owns @t1 tptp.horse) (tptp.owns @t1 tptp.fox) (tptp.owns @t1 tptp.zebra)))) % 0.38/0.88 (assume @p35 (forall @t8 (or @t52 @t51 @t50))) % 0.38/0.88 (assume @p36 @t54) % 0.38/0.88 (assume @p37 @t56) % 0.38/0.88 (assume @p38 (forall @t8 (or @t52 @t51 @t57))) % 0.38/0.88 (assume @p39 (forall @t8 (or @t52 @t50 @t53))) % 0.38/0.88 (assume @p40 (forall @t8 (or @t52 @t50 @t55))) % 0.38/0.88 (assume @p41 (forall @t8 (or @t52 @t50 @t57))) % 0.38/0.88 (assume @p42 @t58) % 0.38/0.88 (assume @p43 @t59) % 0.38/0.88 (assume @p44 @t60) % 0.38/0.88 (assume @p45 @t64) % 0.38/0.88 (assume @p46 @t68) % 0.38/0.88 (assume @p47 (forall @t8 (or @t67 @t66 @t69))) % 0.38/0.88 (assume @p48 @t71) % 0.38/0.88 (assume @p49 (forall @t8 (or @t67 @t66 @t72))) % 0.38/0.88 (assume @p50 (forall @t8 (or @t67 @t65 @t69))) % 0.38/0.88 (assume @p51 (forall @t8 (or @t67 @t65 @t70))) % 0.38/0.88 (assume @p52 (forall @t8 (or @t67 @t65 @t72))) % 0.38/0.88 (assume @p53 (forall @t8 (or @t67 @t69 @t70))) % 0.38/0.88 (assume @p54 (forall @t8 (or @t67 @t69 @t72))) % 0.38/0.88 (assume @p55 @t73) % 0.38/0.88 (assume @p56 @t74) % 0.38/0.88 (assume @p57 @t75) % 0.38/0.88 (assume @p58 @t76) % 0.38/0.88 (assume @p59 @t77) % 0.38/0.88 (assume @p60 @t78) % 0.38/0.88 (assume @p61 @t79) % 0.38/0.88 (assume @p62 @t80) % 0.38/0.88 (assume @p63 @t81) % 0.38/0.88 (assume @p64 @t82) % 0.38/0.88 (assume @p65 @t83) % 0.38/0.88 (assume @p66 @t84) % 0.38/0.88 (assume @p67 @t85) % 0.38/0.88 (assume @p68 @t86) % 0.38/0.88 (assume @p69 @t87) % 0.38/0.88 (assume @p70 @t88) % 0.38/0.88 (assume @p71 @t89) % 0.38/0.88 (assume @p72 @t90) % 0.38/0.88 (assume @p73 @t91) % 0.38/0.88 (assume @p74 @t92) % 0.38/0.88 (assume @p75 @t93) % 0.38/0.88 (assume @p76 @t94) % 0.38/0.88 (assume @p77 @t95) % 0.38/0.88 (assume @p78 @t96) % 0.38/0.88 (assume @p79 (tptp.drink tptp.milk)) % 0.38/0.88 (assume @p80 @t97) % 0.38/0.88 (assume @p81 @t98) % 0.38/0.88 (assume @p82 @t99) % 0.38/0.88 (assume @p83 @t100) % 0.38/0.88 (assume @p84 @t101) % 0.38/0.88 (assume @p85 @t102) % 0.38/0.88 (assume @p86 @t103) % 0.38/0.88 (assume @p87 @t104) % 0.38/0.88 (assume @p88 @t105) % 0.38/0.88 (assume @p89 @t106) % 0.38/0.88 (assume @p90 @t119) % 0.38/0.88 (assume @p91 @t121) % 0.38/0.88 (assume @p92 @t125) % 0.38/0.88 (assume @p93 @t126) % 0.38/0.88 (assume @p94 @t127) % 0.38/0.88 (assume @p95 @t128) % 0.38/0.88 (assume @p96 @t129) % 0.38/0.88 (assume @p97 @t130) % 0.38/0.88 (assume @p98 (forall @t120 (or (tptp.left_of @t107 @t112) @t115 (not (tptp.is_color @t112 tptp.green)) @t110 (not (tptp.is_color @t107 tptp.ivory))))) % 0.38/0.88 (assume @p99 @t131) % 0.38/0.88 (assume @p100 @t137) % 0.38/0.88 (assume @p101 (forall @t136 (or @t135 (not @t138)))) % 0.38/0.88 (assume @p102 @t139) % 0.38/0.88 (assume @p103 @t140) % 0.38/0.88 (assume @p104 (tptp.left_of tptp.house_2 tptp.house_3)) % 0.38/0.88 (assume @p105 @t141) % 0.38/0.88 (assume @p106 (tptp.left_of tptp.house_4 tptp.house_5)) % 0.38/0.88 (assume @p107 (not @t142)) % 0.38/0.88 (assume @p108 (not (tptp.left_of tptp.house_2 tptp.house_1))) % 0.38/0.88 (assume @p109 (not @t143)) % 0.38/0.88 (assume @p110 (not @t144)) % 0.38/0.88 (assume @p111 (not @t145)) % 0.38/0.88 (assume @p112 (not (tptp.left_of tptp.house_2 tptp.house_2))) % 0.38/0.88 (assume @p113 (not @t146)) % 0.38/0.88 (assume @p114 (not @t147)) % 0.38/0.88 (assume @p115 (not @t148)) % 0.38/0.88 (assume @p116 (not @t149)) % 0.38/0.88 (assume @p117 (not @t150)) % 0.38/0.88 (assume @p118 (not (tptp.left_of tptp.house_4 tptp.house_3))) % 0.38/0.88 (assume @p119 (not @t151)) % 0.38/0.88 (assume @p120 (not @t152)) % 0.38/0.88 (assume @p121 (not (tptp.left_of tptp.house_2 tptp.house_4))) % 0.38/0.88 (assume @p122 (not (tptp.left_of tptp.house_4 tptp.house_4))) % 0.38/0.88 (assume @p123 (not @t153)) % 0.38/0.88 (assume @p124 (not @t154)) % 0.38/0.88 (assume @p125 (not @t155)) % 0.38/0.88 (assume @p126 (not @t156)) % 0.38/0.88 (assume @p127 (not (tptp.left_of tptp.house_5 tptp.house_5))) % 0.38/0.88 (assume @p128 (or @t202 @t200 @t199 @t197 @t195 @t193 @t191 @t189 @t187 @t185 @t184 @t182 @t180 @t179 @t177 @t175 @t174 @t172 @t170 @t168 @t166 @t164 @t162 @t160 @t158)) % 0.38/0.88 (step @p129 :rule instantiate :premises (@p53) :args (@t203)) % 0.38/0.88 (step @p130 :rule instantiate :premises (@p86) :args (@t204)) % 0.38/0.88 (step @p131 :rule cnf_or_pos :args (@t206)) % 0.38/0.88 (step @p132 :rule reordering :premises (@p131) :args ((or @t170 @t161 @t205 (not @t206)))) % 0.38/0.88 (step @p133 :rule instantiate :premises (@p54) :args (@t207)) % 0.38/0.88 (step @p134 :rule instantiate :premises (@p49) :args (@t203)) % 0.38/0.88 (step @p135 :rule cnf_or_pos :args (@t213)) % 0.38/0.88 (step @p136 :rule reordering :premises (@p135) :args ((or @t212 @t211 @t209 (not @t213)))) % 0.38/0.88 (step @p137 :rule instantiate :premises (@p47) :args (@t203)) % 0.38/0.88 (step @p138 :rule cnf_or_pos :args (@t214)) % 0.38/0.88 (step @p139 :rule reordering :premises (@p138) :args ((or @t162 @t212 @t211 (not @t214)))) % 0.38/0.88 (step @p140 :rule instantiate :premises (@p49) :args (@t215)) % 0.38/0.88 (step @p141 :rule cnf_or_pos :args (@t221)) % 0.38/0.88 (step @p142 :rule reordering :premises (@p141) :args ((or @t220 @t219 @t217 (not @t221)))) % 0.38/0.88 (step @p143 :rule instantiate :premises (@p98) :args (@t222)) % 0.38/0.88 (step @p144 :rule cnf_or_pos :args (@t225)) % 0.38/0.88 (step @p145 :rule reordering :premises (@p144) :args ((or @t154 @t158 @t223 @t224 @t219 (not @t225)))) % 0.38/0.88 (step @p146 :rule instantiate :premises (@p45) :args (@t226)) % 0.38/0.88 (step @p147 :rule instantiate :premises (@p52) :args (@t227)) % 0.38/0.88 (step @p148 :rule instantiate :premises (@p91) :args ((@list tptp.house_2 tptp.house_1))) % 0.38/0.88 (step @p149 :rule instantiate :premises (@p100) :args ((@list tptp.house_1 tptp.house_2))) % 0.38/0.88 (step @p150 :rule cnf_or_pos :args (@t230)) % 0.38/0.88 (step @p151 :rule reordering :premises (@p150) :args ((or @t228 @t229 (not @t230)))) % 0.38/0.88 (step @p152 :rule chain_m_resolution :premises (@p151 @p103 @p149) :args (@t229 @t231 (@list @t140 @t230))) % 0.38/0.88 (step @p153 :rule cnf_or_pos :args (@t234)) % 0.38/0.88 (step @p154 :rule reordering :premises (@p153) :args ((or @t175 @t163 @t223 @t233 @t232 (not @t234)))) % 0.38/0.88 (step @p155 :rule chain_m_resolution :premises (@p154 @p88 @p61 @p62 @p152 @p148) :args (@t163 (@list false false false false false) (@list @t105 @t79 @t80 @t229 @t234))) % 0.38/0.88 (step @p156 :rule cnf_or_pos :args (@t238)) % 0.38/0.88 (step @p157 :rule reordering :premises (@p156) :args ((or @t164 @t237 @t236 (not @t238)))) % 0.38/0.88 (step @p158 :rule chain_m_resolution :premises (@p157 @p155 @p70 @p147) :args (@t236 @t239 (@list @t163 @t88 @t238))) % 0.38/0.88 (step @p159 :rule cnf_or_pos :args (@t241)) % 0.38/0.88 (step @p160 :rule reordering :premises (@p159) :args ((or @t157 @t224 @t208 @t240 @t235 @t216 (not @t241)))) % 0.38/0.88 (step @p161 :rule chain_m_resolution :premises (@p160 @p158 @p146 @p65 @p145 @p143 @p124 @p65 @p61 @p142 @p140 @p69) :args ((or @t208 @t240 @t219) @t242 (@list @t235 @t241 @t83 @t157 @t225 @t154 @t83 @t79 @t216 @t221 @t87))) % 0.38/0.88 (step @p162 :rule instantiate :premises (@p98) :args ((@list tptp.house_5 tptp.house_1))) % 0.38/0.88 (step @p163 :rule cnf_or_pos :args (@t245)) % 0.38/0.88 (step @p164 :rule reordering :premises (@p163) :args ((or @t145 @t223 @t224 @t244 @t217 (not @t245)))) % 0.38/0.88 (step @p165 :rule instantiate :premises (@p49) :args (@t246)) % 0.38/0.88 (step @p166 :rule cnf_or_pos :args (@t248)) % 0.38/0.88 (step @p167 :rule reordering :premises (@p166) :args ((or @t158 @t247 @t244 (not @t248)))) % 0.38/0.88 (step @p168 :rule chain_m_resolution :premises (@p160 @p158 @p146 @p65 @p167 @p165 @p67 @p164 @p162 @p111 @p65 @p61) :args ((or @t208 @t240 @t244) @t249 (@list @t235 @t241 @t83 @t157 @t248 @t85 @t216 @t245 @t145 @t83 @t79))) % 0.38/0.88 (step @p169 :rule instantiate :premises (@p98) :args ((@list tptp.house_5 tptp.house_3))) % 0.38/0.88 (step @p170 :rule cnf_or_pos :args (@t252)) % 0.38/0.88 (step @p171 :rule reordering :premises (@p170) :args ((or @t151 @t205 @t224 @t251 @t217 (not @t252)))) % 0.38/0.88 (step @p172 :rule instantiate :premises (@p54) :args (@t246)) % 0.38/0.88 (step @p173 :rule cnf_or_pos :args (@t253)) % 0.38/0.88 (step @p174 :rule reordering :premises (@p173) :args ((or @t158 @t247 @t251 (not @t253)))) % 0.38/0.88 (step @p175 :rule chain_m_resolution :premises (@p160 @p158 @p146 @p65 @p174 @p172 @p67 @p171 @p169 @p119 @p65 @p63) :args ((or @t208 @t240 @t251) @t249 (@list @t235 @t241 @t83 @t157 @t253 @t85 @t216 @t252 @t151 @t83 @t81))) % 0.38/0.88 (step @p176 :rule instantiate :premises (@p45) :args (@t204)) % 0.38/0.88 (step @p177 :rule instantiate :premises (@p50) :args (@t227)) % 0.38/0.88 (step @p178 :rule cnf_or_pos :args (@t256)) % 0.38/0.88 (step @p179 :rule reordering :premises (@p178) :args ((or @t164 @t237 @t255 (not @t256)))) % 0.38/0.88 (step @p180 :rule chain_m_resolution :premises (@p179 @p155 @p70 @p177) :args (@t255 @t239 (@list @t163 @t88 @t256))) % 0.38/0.88 (step @p181 :rule cnf_or_pos :args (@t259)) % 0.38/0.88 (step @p182 :rule reordering :premises (@p181) :args ((or @t161 @t205 @t258 @t254 @t250 @t257 (not @t259)))) % 0.38/0.88 (step @p183 :rule instantiate :premises (@p54) :args (@t215)) % 0.38/0.88 (step @p184 :rule cnf_or_pos :args (@t261)) % 0.38/0.88 (step @p185 :rule reordering :premises (@p184) :args ((or @t220 @t260 @t217 (not @t261)))) % 0.38/0.88 (step @p186 :rule instantiate :premises (@p98) :args ((@list tptp.house_3 tptp.house_5))) % 0.38/0.88 (step @p187 :rule cnf_or_pos :args (@t262)) % 0.38/0.88 (step @p188 :rule reordering :premises (@p187) :args ((or @t156 @t158 @t205 @t224 @t260 (not @t262)))) % 0.38/0.88 (step @p189 :rule chain_m_resolution :premises (@p160 @p158 @p146 @p65 @p188 @p186 @p126 @p65 @p63 @p185 @p183 @p69 @p182 @p180 @p176 @p63 @p175) :args ((or @t161 @t258 @t208 @t240) (@list true false false true false true false false true false false false true false false true) (@list @t235 @t241 @t83 @t157 @t262 @t156 @t83 @t81 @t216 @t261 @t87 @t257 @t254 @t259 @t81 @t250))) % 0.38/0.88 (step @p190 :rule instantiate :premises (@p46) :args (@t203)) % 0.38/0.88 (step @p191 :rule cnf_or_pos :args (@t265)) % 0.38/0.88 (step @p192 :rule reordering :premises (@p191) :args ((or @t212 @t211 @t264 (not @t265)))) % 0.38/0.88 (step @p193 :rule instantiate :premises (@p48) :args (@t203)) % 0.38/0.88 (step @p194 :rule cnf_or_pos :args (@t268)) % 0.38/0.88 (step @p195 :rule reordering :premises (@p194) :args ((or @t212 @t211 @t267 (not @t268)))) % 0.38/0.88 (step @p196 :rule instantiate :premises (@p86) :args (@t269)) % 0.38/0.88 (step @p197 :rule cnf_or_pos :args (@t272)) % 0.38/0.88 (step @p198 :rule reordering :premises (@p197) :args ((or @t233 @t271 @t263 (not @t272)))) % 0.38/0.88 (step @p199 :rule instantiate :premises (@p86) :args (@t273)) % 0.38/0.88 (step @p200 :rule cnf_or_pos :args (@t277)) % 0.38/0.88 (step @p201 :rule reordering :premises (@p200) :args ((or @t276 @t275 @t266 (not @t277)))) % 0.38/0.88 (step @p202 :rule instantiate :premises (@p86) :args (@t226)) % 0.38/0.88 (step @p203 :rule cnf_or_pos :args (@t280)) % 0.38/0.88 (step @p204 :rule reordering :premises (@p203) :args ((or @t224 @t279 @t208 (not @t280)))) % 0.38/0.88 (step @p205 :rule instantiate :premises (@p1) :args (@t281)) % 0.38/0.88 (step @p206 :rule instantiate :premises (@p3) :args (@t282)) % 0.38/0.88 (step @p207 :rule cnf_or_pos :args (@t285)) % 0.38/0.88 (step @p208 :rule reordering :premises (@p207) :args ((or @t175 @t223 @t284 (not @t285)))) % 0.38/0.88 (step @p209 :rule chain_m_resolution :premises (@p208 @p88 @p61 @p206) :args (@t284 @t239 (@list @t105 @t79 @t285))) % 0.38/0.88 (step @p210 :rule cnf_or_pos :args (@t287)) % 0.38/0.88 (step @p211 :rule reordering :premises (@p210) :args ((or @t169 @t286 @t283 @t270 @t274 @t278 (not @t287)))) % 0.38/0.88 (step @p212 :rule chain_m_resolution :premises (@p211 @p209 @p205 @p56 @p204 @p202 @p65 @p201 @p199 @p64 @p198 @p196 @p62 @p136 @p134 @p66 @p195 @p193 @p66 @p192 @p190 @p66) :args ((or @t169 @t211) (@list true false false true false false true false false true false false true false false true false false true false false) (@list @t283 @t287 @t74 @t278 @t280 @t83 @t274 @t277 @t82 @t270 @t272 @t80 @t208 @t213 @t84 @t266 @t268 @t84 @t263 @t265 @t84))) % 0.38/0.88 (step @p213 :rule instantiate :premises (@p47) :args (@t207)) % 0.38/0.88 (step @p214 :rule cnf_or_pos :args (@t290)) % 0.38/0.88 (step @p215 :rule reordering :premises (@p214) :args ((or @t166 @t289 @t288 (not @t290)))) % 0.38/0.88 (step @p216 :rule instantiate :premises (@p45) :args (@t282)) % 0.38/0.88 (step @p217 :rule instantiate :premises (@p46) :args (@t227)) % 0.38/0.88 (step @p218 :rule cnf_or_pos :args (@t293)) % 0.38/0.88 (step @p219 :rule reordering :premises (@p218) :args ((or @t164 @t237 @t292 (not @t293)))) % 0.38/0.88 (step @p220 :rule chain_m_resolution :premises (@p219 @p155 @p70 @p217) :args (@t292 @t239 (@list @t163 @t88 @t293))) % 0.38/0.88 (step @p221 :rule cnf_or_pos :args (@t294)) % 0.38/0.88 (step @p222 :rule reordering :premises (@p221) :args ((or @t165 @t223 @t210 @t291 @t243 @t218 (not @t294)))) % 0.38/0.88 (step @p223 :rule chain_m_resolution :premises (@p222 @p220 @p216 @p61 @p215 @p213 @p68 @p212 @p189 @p132 @p130 @p63 @p168 @p161) :args ((or @t161 @t208 @t240) (@list true false false true false false true false true false false true true) (@list @t291 @t294 @t79 @t165 @t290 @t86 @t210 @t258 @t169 @t206 @t81 @t243 @t218))) % 0.38/0.88 (step @p224 :rule chain_m_resolution :premises (@p223 @p139 @p137 @p66 @p136 @p134 @p66) :args ((or @t240 @t211) @t295 (@list @t161 @t214 @t84 @t208 @t213 @t84))) % 0.38/0.88 (step @p225 :rule instantiate :premises (@p50) :args (@t207)) % 0.38/0.88 (step @p226 :rule cnf_or_pos :args (@t298)) % 0.38/0.88 (step @p227 :rule reordering :premises (@p226) :args ((or @t289 @t297 @t288 (not @t298)))) % 0.38/0.88 (step @p228 :rule instantiate :premises (@p46) :args (@t207)) % 0.38/0.88 (step @p229 :rule cnf_or_pos :args (@t299)) % 0.38/0.88 (step @p230 :rule reordering :premises (@p229) :args ((or @t166 @t289 @t297 (not @t299)))) % 0.38/0.88 (step @p231 :rule instantiate :premises (@p47) :args (@t215)) % 0.38/0.88 (step @p232 :rule cnf_or_pos :args (@t300)) % 0.38/0.88 (step @p233 :rule reordering :premises (@p232) :args ((or @t220 @t219 @t260 (not @t300)))) % 0.38/0.88 (step @p234 :rule instantiate :premises (@p98) :args (@t301)) % 0.38/0.88 (step @p235 :rule cnf_or_pos :args (@t302)) % 0.38/0.88 (step @p236 :rule reordering :premises (@p235) :args ((or @t149 @t223 @t205 @t219 @t251 (not @t302)))) % 0.38/0.88 (step @p237 :rule chain_m_resolution :premises (@p182 @p180 @p176 @p63 @p236 @p234 @p116 @p63 @p61 @p233 @p231 @p69) :args ((or @t161 @t258 @t219) @t242 (@list @t254 @t259 @t81 @t250 @t302 @t149 @t81 @t79 @t257 @t300 @t87))) % 0.38/0.88 (step @p238 :rule instantiate :premises (@p47) :args (@t246)) % 0.38/0.88 (step @p239 :rule cnf_or_pos :args (@t303)) % 0.38/0.88 (step @p240 :rule reordering :premises (@p239) :args ((or @t247 @t244 @t251 (not @t303)))) % 0.38/0.88 (step @p241 :rule instantiate :premises (@p98) :args ((@list tptp.house_3 tptp.house_1))) % 0.38/0.88 (step @p242 :rule cnf_or_pos :args (@t304)) % 0.38/0.88 (step @p243 :rule reordering :premises (@p242) :args ((or @t143 @t223 @t205 @t244 @t260 (not @t304)))) % 0.38/0.88 (step @p244 :rule chain_m_resolution :premises (@p182 @p180 @p176 @p63 @p243 @p241 @p109 @p63 @p61 @p240 @p238 @p67 @p222 @p220 @p216 @p61 @p237 @p230 @p228 @p68 @p227 @p225 @p68) :args ((or @t161 @t210 @t297) (@list true false false true false true false false true false false false true false false true true false false true false false) (@list @t254 @t259 @t81 @t257 @t304 @t143 @t81 @t79 @t250 @t303 @t85 @t243 @t291 @t294 @t79 @t218 @t165 @t299 @t86 @t258 @t298 @t86))) % 0.38/0.88 (step @p245 :rule instantiate :premises (@p99) :args (@t281)) % 0.38/0.88 (step @p246 :rule cnf_or_pos :args (@t305)) % 0.38/0.88 (step @p247 :rule reordering :premises (@p246) :args ((or @t197 @t169 @t286 (not @t305)))) % 0.38/0.88 (step @p248 :rule instantiate :premises (@p52) :args (@t203)) % 0.38/0.88 (step @p249 :rule cnf_or_pos :args (@t306)) % 0.38/0.88 (step @p250 :rule reordering :premises (@p249) :args ((or @t212 @t264 @t209 (not @t306)))) % 0.38/0.88 (step @p251 :rule instantiate :premises (@p55) :args (@t203)) % 0.38/0.88 (step @p252 :rule cnf_or_pos :args (@t307)) % 0.38/0.88 (step @p253 :rule reordering :premises (@p252) :args ((or @t212 @t267 @t209 (not @t307)))) % 0.38/0.88 (step @p254 :rule chain_m_resolution :premises (@p211 @p209 @p205 @p56 @p201 @p199 @p64 @p198 @p196 @p62 @p253 @p251 @p66 @p250 @p248 @p66) :args ((or @t169 @t278 @t209) (@list true false false true false false true false false true false false true false false) (@list @t283 @t287 @t74 @t274 @t277 @t82 @t270 @t272 @t80 @t266 @t307 @t84 @t263 @t306 @t84))) % 0.38/0.88 (step @p255 :rule instantiate :premises (@p5) :args (@t226)) % 0.38/0.88 (step @p256 :rule cnf_or_pos :args (@t308)) % 0.38/0.88 (step @p257 :rule reordering :premises (@p256) :args ((or @t172 @t224 @t279 (not @t308)))) % 0.38/0.88 (step @p258 :rule instantiate :premises (@p89) :args (@t309)) % 0.38/0.88 (step @p259 :rule cnf_or_pos :args (@t312)) % 0.38/0.88 (step @p260 :rule reordering :premises (@p259) :args ((or @t286 @t224 @t279 @t311 @t240 (not @t312)))) % 0.38/0.88 (step @p261 :rule instantiate :premises (@p53) :args (@t207)) % 0.38/0.88 (step @p262 :rule cnf_or_pos :args (@t315)) % 0.38/0.88 (step @p263 :rule reordering :premises (@p262) :args ((or @t289 @t288 @t314 (not @t315)))) % 0.38/0.88 (step @p264 :rule instantiate :premises (@p45) :args (@t273)) % 0.38/0.88 (step @p265 :rule instantiate :premises (@p51) :args (@t227)) % 0.38/0.88 (step @p266 :rule cnf_or_pos :args (@t318)) % 0.38/0.88 (step @p267 :rule reordering :premises (@p266) :args ((or @t164 @t237 @t317 (not @t318)))) % 0.38/0.88 (step @p268 :rule chain_m_resolution :premises (@p267 @p155 @p70 @p265) :args (@t317 @t239 (@list @t163 @t88 @t318))) % 0.38/0.88 (step @p269 :rule cnf_or_pos :args (@t320)) % 0.38/0.88 (step @p270 :rule reordering :premises (@p269) :args ((or @t159 @t276 @t266 @t313 @t316 @t319 (not @t320)))) % 0.38/0.88 (step @p271 :rule instantiate :premises (@p98) :args ((@list tptp.house_4 tptp.house_1))) % 0.38/0.88 (step @p272 :rule cnf_or_pos :args (@t321)) % 0.38/0.88 (step @p273 :rule reordering :premises (@p272) :args ((or @t144 @t160 @t223 @t276 @t244 (not @t321)))) % 0.38/0.88 (step @p274 :rule instantiate :premises (@p48) :args (@t215)) % 0.38/0.88 (step @p275 :rule cnf_or_pos :args (@t322)) % 0.38/0.88 (step @p276 :rule reordering :premises (@p275) :args ((or @t160 @t220 @t219 (not @t322)))) % 0.38/0.88 (step @p277 :rule chain_m_resolution :premises (@p222 @p220 @p216 @p61 @p276 @p274 @p69 @p273 @p271 @p110 @p64 @p61 @p270 @p268 @p264 @p64 @p215 @p213 @p68 @p263 @p261 @p68) :args ((or @t210 @t266 @t319 @t288) (@list true false false true false false true false true false false false true false false true false false true false false) (@list @t291 @t294 @t79 @t218 @t322 @t87 @t243 @t321 @t144 @t82 @t79 @t159 @t316 @t320 @t82 @t165 @t290 @t86 @t313 @t315 @t86))) % 0.38/0.88 (step @p278 :rule instantiate :premises (@p48) :args (@t246)) % 0.38/0.88 (step @p279 :rule cnf_or_pos :args (@t324)) % 0.38/0.88 (step @p280 :rule reordering :premises (@p279) :args ((or @t247 @t244 @t323 (not @t324)))) % 0.38/0.88 (step @p281 :rule instantiate :premises (@p98) :args (@t325)) % 0.38/0.88 (step @p282 :rule cnf_or_pos :args (@t326)) % 0.38/0.88 (step @p283 :rule reordering :premises (@p282) :args ((or @t152 @t223 @t276 @t219 @t323 (not @t326)))) % 0.38/0.88 (step @p284 :rule chain_m_resolution :premises (@p222 @p220 @p216 @p61 @p283 @p281 @p120 @p64 @p61 @p280 @p278 @p67 @p277 @p215 @p213 @p68) :args ((or @t210 @t266 @t288) (@list true false false true false true false false true false false false true false false) (@list @t291 @t294 @t79 @t218 @t326 @t152 @t82 @t79 @t243 @t324 @t85 @t319 @t165 @t290 @t86))) % 0.38/0.88 (step @p285 :rule chain_m_resolution :premises (@p182 @p180 @p176 @p63 @p243 @p241 @p109 @p63 @p61 @p240 @p238 @p67) :args ((or @t161 @t258 @t244) @t242 (@list @t254 @t259 @t81 @t257 @t304 @t143 @t81 @t79 @t250 @t303 @t85))) % 0.38/0.88 (step @p286 :rule chain_m_resolution :premises (@p182 @p180 @p176 @p63 @p188 @p186 @p126 @p65 @p63 @p174 @p172 @p67) :args ((or @t161 @t158 @t258) @t242 (@list @t254 @t259 @t81 @t257 @t262 @t156 @t83 @t81 @t250 @t253 @t85))) % 0.38/0.88 (step @p287 :rule instantiate :premises (@p50) :args (@t246)) % 0.38/0.88 (step @p288 :rule cnf_or_pos :args (@t329)) % 0.38/0.88 (step @p289 :rule reordering :premises (@p288) :args ((or @t247 @t328 @t251 (not @t329)))) % 0.38/0.88 (step @p290 :rule instantiate :premises (@p98) :args ((@list tptp.house_3 tptp.house_2))) % 0.38/0.88 (step @p291 :rule cnf_or_pos :args (@t330)) % 0.38/0.88 (step @p292 :rule reordering :premises (@p291) :args ((or @t146 @t233 @t205 @t328 @t260 (not @t330)))) % 0.38/0.88 (step @p293 :rule chain_m_resolution :premises (@p182 @p180 @p176 @p63 @p292 @p290 @p113 @p63 @p62 @p289 @p287 @p67) :args ((or @t161 @t258 @t328) @t242 (@list @t254 @t259 @t81 @t257 @t330 @t146 @t81 @t80 @t250 @t329 @t85))) % 0.38/0.88 (assume-push @p1066 @t103) % 0.38/0.88 (step-pop @p1067 :rule scope :premises (@p130)) % 0.38/0.88 (step @p295 :rule process_scope :premises (@p1067) :args (@t206)) % 0.38/0.88 (step @p297 :rule implies_elim :premises (@p295)) % 0.38/0.88 (step @p298 :rule instantiate :premises (@p89) :args ((@list tptp.house_3 tptp.spaniard))) % 0.38/0.88 (step @p299 :rule cnf_or_pos :args (@t336)) % 0.38/0.88 (step @p300 :rule reordering :premises (@p299) :args ((or @t335 @t205 @t332 @t334 @t258 (not @t336)))) % 0.38/0.88 (step @p301 :rule instantiate :premises (@p89) :args ((@list tptp.house_4 tptp.spaniard))) % 0.38/0.88 (step @p302 :rule cnf_or_pos :args (@t337)) % 0.38/0.88 (step @p303 :rule reordering :premises (@p302) :args ((or @t168 @t335 @t276 @t334 @t313 (not @t337)))) % 0.38/0.88 (step @p304 :rule instantiate :premises (@p89) :args (@t338)) % 0.38/0.88 (step @p305 :rule cnf_or_pos :args (@t341)) % 0.38/0.88 (step @p306 :rule reordering :premises (@p305) :args ((or @t335 @t233 @t340 @t334 @t296 (not @t341)))) % 0.38/0.88 (step @p307 :rule instantiate :premises (@p89) :args ((@list tptp.house_5 tptp.spaniard))) % 0.38/0.88 (step @p308 :rule cnf_or_pos :args (@t344)) % 0.38/0.88 (step @p309 :rule reordering :premises (@p308) :args ((or @t335 @t224 @t343 @t334 @t240 (not @t344)))) % 0.38/0.88 (step @p310 :rule instantiate :premises (@p1) :args (@t345)) % 0.38/0.88 (step @p311 :rule instantiate :premises (@p6) :args (@t282)) % 0.38/0.88 (step @p312 :rule cnf_or_pos :args (@t348)) % 0.38/0.88 (step @p313 :rule reordering :premises (@p312) :args ((or @t175 @t223 @t347 (not @t348)))) % 0.38/0.88 (step @p314 :rule chain_m_resolution :premises (@p313 @p88 @p61 @p311) :args (@t347 @t239 (@list @t105 @t79 @t348))) % 0.38/0.88 (step @p315 :rule cnf_or_pos :args (@t349)) % 0.38/0.88 (step @p316 :rule reordering :premises (@p315) :args ((or @t167 @t335 @t346 @t339 @t331 @t342 (not @t349)))) % 0.38/0.88 (step @p317 :rule chain_m_resolution :premises (@p316 @p314 @p310 @p57 @p309 @p307 @p65 @p57 @p306 @p304 @p62 @p57 @p303 @p301 @p64 @p57) :args ((or @t331 @t334 @t296 @t313 @t240) (@list true false false true false false false true false false false true false false false) (@list @t346 @t349 @t75 @t342 @t344 @t83 @t75 @t339 @t341 @t80 @t75 @t167 @t337 @t82 @t75))) % 0.38/0.88 (step @p318 :rule instantiate :premises (@p48) :args (@t207)) % 0.38/0.88 (step @p319 :rule cnf_or_pos :args (@t350)) % 0.38/0.88 (step @p320 :rule reordering :premises (@p319) :args ((or @t166 @t289 @t314 (not @t350)))) % 0.38/0.88 (step @p321 :rule chain_m_resolution :premises (@p320 @p318 @p68 @p317 @p222 @p220 @p216 @p61 @p244) :args ((or @t161 @t331 @t334 @t210 @t243 @t218 @t240) (@list false false false false true false false true) (@list @t350 @t86 @t313 @t165 @t291 @t294 @t79 @t296))) % 0.38/0.88 (step @p322 :rule chain_m_resolution :premises (@p321 @p300 @p298 @p63 @p57 @p285 @p237 @p212 @p132 @p63 @p297 @p86) :args ((or @t161 @t334 @t258 @t240) (@list true false false false true true true true false false false) (@list @t331 @t336 @t81 @t75 @t243 @t218 @t210 @t169 @t81 @t206 @t103))) % 0.38/0.88 (step @p323 :rule instantiate :premises (@p97) :args ((@list tptp.house_1 tptp.norwegian))) % 0.38/0.88 (step @p324 :rule cnf_or_pos :args (@t354)) % 0.38/0.88 (step @p325 :rule reordering :premises (@p324) :args ((or @t175 @t353 @t223 @t352 @t243 (not @t354)))) % 0.38/0.88 (step @p326 :rule instantiate :premises (@p97) :args (@t309)) % 0.38/0.88 (step @p327 :rule cnf_or_pos :args (@t357)) % 0.38/0.88 (step @p328 :rule reordering :premises (@p327) :args ((or @t157 @t286 @t224 @t279 @t356 (not @t357)))) % 0.38/0.88 (step @p329 :rule instantiate :premises (@p15) :args (@t358)) % 0.38/0.88 (step @p330 :rule cnf_or_pos :args (@t364)) % 0.38/0.88 (step @p331 :rule reordering :premises (@p330) :args ((or @t363 @t362 @t360 (not @t364)))) % 0.38/0.88 (step @p332 :rule instantiate :premises (@p20) :args (@t358)) % 0.38/0.88 (step @p333 :rule cnf_or_pos :args (@t367)) % 0.38/0.88 (step @p334 :rule reordering :premises (@p333) :args ((or @t363 @t366 @t360 (not @t367)))) % 0.38/0.88 (step @p335 :rule instantiate :premises (@p12) :args (@t281)) % 0.38/0.88 (step @p336 :rule instantiate :premises (@p15) :args (@t368)) % 0.38/0.88 (step @p337 :rule cnf_or_pos :args (@t372)) % 0.38/0.88 (step @p338 :rule reordering :premises (@p337) :args ((or @t200 @t371 @t370 (not @t372)))) % 0.38/0.88 (step @p339 :rule chain_m_resolution :premises (@p338 @p94 @p76 @p336) :args (@t370 @t239 (@list @t127 @t94 @t372))) % 0.38/0.88 (step @p340 :rule cnf_or_pos :args (@t374)) % 0.38/0.88 (step @p341 :rule reordering :premises (@p340) :args ((or @t196 @t286 @t361 @t355 @t369 @t373 (not @t374)))) % 0.38/0.88 (step @p342 :rule instantiate :premises (@p99) :args (@t375)) % 0.38/0.88 (step @p343 :rule instantiate :premises (@p91) :args ((@list tptp.house_4 tptp.house_3))) % 0.38/0.88 (step @p344 :rule instantiate :premises (@p100) :args ((@list tptp.house_3 tptp.house_4))) % 0.38/0.88 (step @p345 :rule cnf_or_pos :args (@t378)) % 0.38/0.88 (step @p346 :rule reordering :premises (@p345) :args ((or @t376 @t377 (not @t378)))) % 0.38/0.88 (step @p347 :rule chain_m_resolution :premises (@p346 @p105 @p344) :args (@t377 @t231 (@list @t141 @t378))) % 0.38/0.88 (step @p348 :rule cnf_or_pos :args (@t382)) % 0.38/0.88 (step @p349 :rule reordering :premises (@p348) :args ((or @t205 @t276 @t381 @t316 @t379 (not @t382)))) % 0.38/0.88 (step @p350 :rule chain_m_resolution :premises (@p349 @p63 @p64 @p268 @p347 @p343) :args (@t381 (@list false false true false false) (@list @t81 @t82 @t316 @t377 @t382))) % 0.38/0.88 (step @p351 :rule cnf_or_pos :args (@t385)) % 0.38/0.88 (step @p352 :rule reordering :premises (@p351) :args ((or @t353 @t380 @t384 (not @t385)))) % 0.38/0.88 (step @p353 :rule chain_m_resolution :premises (@p352 @p58 @p350 @p342) :args (@t384 @t386 (@list @t76 @t380 @t385))) % 0.38/0.88 (step @p354 :rule instantiate :premises (@p12) :args (@t375)) % 0.38/0.88 (step @p355 :rule instantiate :premises (@p20) :args (@t368)) % 0.38/0.88 (step @p356 :rule cnf_or_pos :args (@t389)) % 0.38/0.88 (step @p357 :rule reordering :premises (@p356) :args ((or @t200 @t371 @t388 (not @t389)))) % 0.38/0.88 (step @p358 :rule chain_m_resolution :premises (@p357 @p94 @p76 @p355) :args (@t388 @t239 (@list @t127 @t94 @t389))) % 0.38/0.88 (step @p359 :rule cnf_or_pos :args (@t390)) % 0.38/0.88 (step @p360 :rule reordering :premises (@p359) :args ((or @t201 @t353 @t365 @t351 @t387 @t383 (not @t390)))) % 0.38/0.88 (step @p361 :rule instantiate :premises (@p14) :args (@t391)) % 0.38/0.88 (step @p362 :rule cnf_or_pos :args (@t394)) % 0.38/0.88 (step @p363 :rule reordering :premises (@p362) :args ((or @t202 @t393 @t392 (not @t394)))) % 0.38/0.88 (step @p364 :rule chain_m_resolution :premises (@p363 @p361 @p78 @p360 @p358 @p354 @p353 @p58 @p341 @p339 @p335 @p56 @p334 @p332 @p77 @p331 @p329 @p77) :args ((or @t196 @t355 @t351 @t360) (@list false false false true false true false false true false false true false false true false false) (@list @t394 @t96 @t201 @t387 @t390 @t383 @t76 @t373 @t369 @t374 @t74 @t365 @t367 @t95 @t361 @t364 @t95))) % 0.38/0.88 (step @p365 :rule instantiate :premises (@p17) :args (@t358)) % 0.38/0.88 (step @p366 :rule cnf_or_pos :args (@t395)) % 0.38/0.88 (step @p367 :rule reordering :premises (@p366) :args ((or @t195 @t363 @t366 (not @t395)))) % 0.38/0.88 (step @p368 :rule instantiate :premises (@p13) :args (@t358)) % 0.38/0.88 (step @p369 :rule cnf_or_pos :args (@t396)) % 0.38/0.88 (step @p370 :rule reordering :premises (@p369) :args ((or @t195 @t363 @t362 (not @t396)))) % 0.38/0.88 (step @p371 :rule chain_m_resolution :premises (@p363 @p361 @p78 @p341 @p339 @p335 @p56 @p360 @p358 @p354 @p353 @p58 @p370 @p368 @p77 @p367 @p365 @p77) :args ((or @t196 @t195 @t355 @t351) (@list false false false true false false false true false true false true false false true false false) (@list @t394 @t96 @t373 @t369 @t374 @t74 @t201 @t387 @t390 @t383 @t76 @t361 @t396 @t95 @t365 @t395 @t95))) % 0.38/0.88 (step @p372 :rule instantiate :premises (@p93) :args (@t397)) % 0.38/0.88 (step @p373 :rule cnf_or_pos :args (@t401)) % 0.38/0.88 (step @p374 :rule reordering :premises (@p373) :args ((or @t400 @t359 @t399 (not @t401)))) % 0.38/0.88 (step @p375 :rule instantiate :premises (@p93) :args (@t345)) % 0.38/0.88 (step @p376 :rule cnf_or_pos :args (@t402)) % 0.38/0.88 (step @p377 :rule reordering :premises (@p376) :args ((or @t194 @t177 @t335 (not @t402)))) % 0.38/0.88 (step @p378 :rule instantiate :premises (@p23) :args (@t345)) % 0.38/0.88 (step @p379 :rule instantiate :premises (@p30) :args (@t403)) % 0.38/0.88 (step @p380 :rule cnf_or_pos :args (@t407)) % 0.38/0.88 (step @p381 :rule reordering :premises (@p380) :args ((or @t180 @t406 @t405 (not @t407)))) % 0.38/0.88 (step @p382 :rule chain_m_resolution :premises (@p381 @p95 @p71 @p379) :args (@t405 @t239 (@list @t128 @t89 @t407))) % 0.38/0.88 (step @p383 :rule instantiate :premises (@p92) :args (@t345)) % 0.38/0.88 (step @p384 :rule instantiate :premises (@p39) :args (@t408)) % 0.38/0.88 (step @p385 :rule cnf_or_pos :args (@t414)) % 0.38/0.88 (step @p386 :rule reordering :premises (@p385) :args ((or @t413 @t412 @t410 (not @t414)))) % 0.38/0.88 (step @p387 :rule instantiate :premises (@p40) :args (@t408)) % 0.38/0.88 (step @p388 :rule cnf_or_pos :args (@t417)) % 0.38/0.88 (step @p389 :rule reordering :premises (@p388) :args ((or @t413 @t412 @t416 (not @t417)))) % 0.38/0.88 (step @p390 :rule instantiate :premises (@p41) :args (@t408)) % 0.38/0.88 (step @p391 :rule cnf_or_pos :args (@t420)) % 0.38/0.88 (step @p392 :rule reordering :premises (@p391) :args ((or @t413 @t412 @t419 (not @t420)))) % 0.38/0.88 (step @p393 :rule instantiate :premises (@p35) :args (@t408)) % 0.38/0.88 (step @p394 :rule cnf_or_pos :args (@t421)) % 0.38/0.88 (step @p395 :rule reordering :premises (@p394) :args ((or @t187 @t413 @t412 (not @t421)))) % 0.38/0.88 (step @p396 :rule instantiate :premises (@p37) :args (@t422)) % 0.38/0.88 (step @p397 :rule cnf_or_pos :args (@t428)) % 0.38/0.88 (step @p398 :rule reordering :premises (@p397) :args ((or @t427 @t426 @t424 (not @t428)))) % 0.38/0.88 (step @p399 :rule instantiate :premises (@p38) :args (@t422)) % 0.38/0.88 (step @p400 :rule cnf_or_pos :args (@t431)) % 0.38/0.88 (step @p401 :rule reordering :premises (@p400) :args ((or @t427 @t426 @t430 (not @t431)))) % 0.38/0.88 (step @p402 :rule instantiate :premises (@p36) :args (@t422)) % 0.38/0.88 (step @p403 :rule cnf_or_pos :args (@t432)) % 0.38/0.88 (step @p404 :rule reordering :premises (@p403) :args ((or @t193 @t427 @t426 (not @t432)))) % 0.38/0.88 (step @p405 :rule instantiate :premises (@p42) :args (@t433)) % 0.38/0.88 (step @p406 :rule cnf_or_pos :args (@t437)) % 0.38/0.88 (step @p407 :rule reordering :premises (@p406) :args ((or @t191 @t436 @t435 (not @t437)))) % 0.38/0.88 (step @p408 :rule instantiate :premises (@p44) :args (@t433)) % 0.38/0.88 (step @p409 :rule cnf_or_pos :args (@t440)) % 0.38/0.88 (step @p410 :rule reordering :premises (@p409) :args ((or @t191 @t436 @t439 (not @t440)))) % 0.38/0.88 (step @p411 :rule instantiate :premises (@p34) :args (@t375)) % 0.38/0.88 (step @p412 :rule instantiate :premises (@p39) :args (@t441)) % 0.38/0.88 (step @p413 :rule cnf_or_pos :args (@t445)) % 0.38/0.88 (step @p414 :rule reordering :premises (@p413) :args ((or @t185 @t444 @t443 (not @t445)))) % 0.38/0.88 (step @p415 :rule chain_m_resolution :premises (@p414 @p87 @p81 @p412) :args (@t443 @t239 (@list @t104 @t98 @t445))) % 0.38/0.88 (step @p416 :rule cnf_or_pos :args (@t447)) % 0.38/0.88 (step @p417 :rule reordering :premises (@p416) :args ((or @t192 @t353 @t442 @t409 @t434 @t446 (not @t447)))) % 0.38/0.88 (step @p418 :rule instantiate :premises (@p34) :args (@t448)) % 0.38/0.88 (step @p419 :rule instantiate :premises (@p41) :args (@t441)) % 0.38/0.88 (step @p420 :rule cnf_or_pos :args (@t451)) % 0.38/0.88 (step @p421 :rule reordering :premises (@p420) :args ((or @t185 @t444 @t450 (not @t451)))) % 0.38/0.88 (step @p422 :rule chain_m_resolution :premises (@p421 @p87 @p81 @p419) :args (@t450 @t239 (@list @t104 @t98 @t451))) % 0.38/0.88 (step @p423 :rule cnf_or_pos :args (@t453)) % 0.38/0.88 (step @p424 :rule reordering :premises (@p423) :args ((or @t188 @t452 @t449 @t418 @t438 @t429 (not @t453)))) % 0.38/0.88 (step @p425 :rule instantiate :premises (@p43) :args (@t454)) % 0.38/0.88 (step @p426 :rule cnf_or_pos :args (@t457)) % 0.38/0.88 (step @p427 :rule reordering :premises (@p426) :args ((or @t189 @t456 @t455 (not @t457)))) % 0.38/0.88 (step @p428 :rule chain_m_resolution :premises (@p427 @p425 @p82 @p424 @p422 @p418 @p60 @p417 @p415 @p411 @p58 @p410 @p408 @p84 @p407 @p405 @p84) :args ((or @t192 @t191 @t409 @t418 @t429) @t458 (@list @t457 @t99 @t188 @t449 @t453 @t78 @t446 @t442 @t447 @t76 @t438 @t440 @t101 @t434 @t437 @t101))) % 0.38/0.88 (step @p429 :rule instantiate :premises (@p34) :args (@t397)) % 0.38/0.88 (step @p430 :rule instantiate :premises (@p40) :args (@t441)) % 0.38/0.88 (step @p431 :rule cnf_or_pos :args (@t461)) % 0.38/0.88 (step @p432 :rule reordering :premises (@p431) :args ((or @t185 @t444 @t460 (not @t461)))) % 0.38/0.88 (step @p433 :rule chain_m_resolution :premises (@p432 @p87 @p81 @p430) :args (@t460 @t239 (@list @t104 @t98 @t461))) % 0.38/0.88 (step @p434 :rule cnf_or_pos :args (@t463)) % 0.38/0.88 (step @p435 :rule reordering :premises (@p434) :args ((or @t190 @t400 @t459 @t415 @t423 @t462 (not @t463)))) % 0.38/0.88 (step @p436 :rule instantiate :premises (@p42) :args (@t454)) % 0.38/0.88 (step @p437 :rule cnf_or_pos :args (@t465)) % 0.38/0.88 (step @p438 :rule reordering :premises (@p437) :args ((or @t456 @t455 @t464 (not @t465)))) % 0.38/0.88 (step @p439 :rule instantiate :premises (@p44) :args (@t454)) % 0.38/0.88 (step @p440 :rule cnf_or_pos :args (@t466)) % 0.38/0.88 (step @p441 :rule reordering :premises (@p440) :args ((or @t189 @t456 @t464 (not @t466)))) % 0.38/0.88 (step @p442 :rule instantiate :premises (@p43) :args (@t433)) % 0.38/0.88 (step @p443 :rule cnf_or_pos :args (@t467)) % 0.38/0.88 (step @p444 :rule reordering :premises (@p443) :args ((or @t436 @t435 @t439 (not @t467)))) % 0.38/0.88 (step @p445 :rule chain_m_resolution :premises (@p444 @p442 @p84 @p424 @p422 @p418 @p60 @p417 @p415 @p411 @p58 @p441 @p439 @p82 @p438 @p436 @p82 @p435 @p433 @p429 @p59 @p428 @p404 @p402 @p85 @p401 @p399 @p85 @p398 @p396 @p85) :args ((or @t409 @t415 @t418 @t426) (@list false false false true false false false true false false true false false true false false false true false false true true false false true false false true false false) (@list @t467 @t101 @t438 @t449 @t453 @t78 @t434 @t442 @t447 @t76 @t188 @t466 @t99 @t446 @t465 @t99 @t462 @t459 @t463 @t77 @t190 @t192 @t432 @t102 @t429 @t431 @t102 @t423 @t428 @t102))) % 0.38/0.88 (step @p446 :rule instantiate :premises (@p38) :args (@t433)) % 0.38/0.88 (step @p447 :rule cnf_or_pos :args (@t470)) % 0.38/0.88 (step @p448 :rule reordering :premises (@p447) :args ((or @t436 @t469 @t439 (not @t470)))) % 0.38/0.88 (step @p449 :rule instantiate :premises (@p34) :args (@t281)) % 0.38/0.88 (step @p450 :rule instantiate :premises (@p35) :args (@t441)) % 0.38/0.88 (step @p451 :rule cnf_or_pos :args (@t473)) % 0.38/0.88 (step @p452 :rule reordering :premises (@p451) :args ((or @t185 @t444 @t472 (not @t473)))) % 0.38/0.88 (step @p453 :rule chain_m_resolution :premises (@p452 @p87 @p81 @p450) :args (@t472 @t239 (@list @t104 @t98 @t473))) % 0.38/0.88 (step @p454 :rule cnf_or_pos :args (@t475)) % 0.38/0.88 (step @p455 :rule reordering :premises (@p454) :args ((or @t186 @t286 @t471 @t468 @t425 @t474 (not @t475)))) % 0.38/0.88 (step @p456 :rule instantiate :premises (@p36) :args (@t454)) % 0.38/0.88 (step @p457 :rule cnf_or_pos :args (@t477)) % 0.38/0.88 (step @p458 :rule reordering :premises (@p457) :args ((or @t456 @t476 @t455 (not @t477)))) % 0.38/0.88 (step @p459 :rule chain_m_resolution :premises (@p458 @p456 @p82 @p417 @p415 @p411 @p58 @p455 @p453 @p449 @p56 @p444 @p442 @p84 @p448 @p446 @p84) :args ((or @t192 @t186 @t425 @t409 @t439) @t458 (@list @t477 @t99 @t446 @t442 @t447 @t76 @t474 @t471 @t475 @t74 @t434 @t467 @t101 @t468 @t470 @t101))) % 0.38/0.88 (step @p460 :rule instantiate :premises (@p44) :args (@t422)) % 0.38/0.88 (step @p461 :rule cnf_or_pos :args (@t478)) % 0.38/0.88 (step @p462 :rule reordering :premises (@p461) :args ((or @t427 @t424 @t430 (not @t478)))) % 0.38/0.88 (step @p463 :rule instantiate :premises (@p43) :args (@t422)) % 0.38/0.88 (step @p464 :rule cnf_or_pos :args (@t479)) % 0.38/0.88 (step @p465 :rule reordering :premises (@p464) :args ((or @t193 @t427 @t430 (not @t479)))) % 0.38/0.88 (step @p466 :rule instantiate :premises (@p37) :args (@t433)) % 0.38/0.88 (step @p467 :rule cnf_or_pos :args (@t480)) % 0.38/0.88 (step @p468 :rule reordering :premises (@p467) :args ((or @t191 @t436 @t469 (not @t480)))) % 0.38/0.88 (step @p469 :rule chain_m_resolution :premises (@p468 @p466 @p84 @p435 @p433 @p429 @p59 @p455 @p453 @p449 @p56 @p438 @p436 @p82 @p458 @p456 @p82 @p417 @p415 @p411 @p58 @p465 @p463 @p85 @p462 @p460 @p85 @p401 @p399 @p85) :args ((or @t186 @t409 @t434 @t415 @t430) (@list false false false true false false false true false false true false false true false false false true false false true false false true false false true false false) (@list @t480 @t101 @t190 @t459 @t463 @t77 @t468 @t471 @t475 @t74 @t462 @t465 @t99 @t474 @t477 @t99 @t446 @t442 @t447 @t76 @t192 @t479 @t102 @t423 @t478 @t102 @t425 @t431 @t102))) % 0.38/0.88 (step @p470 :rule chain_m_resolution :premises (@p427 @p425 @p82 @p424 @p422 @p418 @p60 @p417 @p415 @p411 @p58 @p469 @p459 @p445) :args ((or @t192 @t186 @t409 @t434 @t415 @t418) (@list false false false true false false false true false false true true true) (@list @t457 @t99 @t188 @t449 @t453 @t78 @t446 @t442 @t447 @t76 @t429 @t438 @t425))) % 0.38/0.88 (step @p471 :rule instantiate :premises (@p36) :args (@t433)) % 0.38/0.88 (step @p472 :rule cnf_or_pos :args (@t481)) % 0.38/0.88 (step @p473 :rule reordering :premises (@p472) :args ((or @t436 @t469 @t435 (not @t481)))) % 0.38/0.88 (step @p474 :rule instantiate :premises (@p37) :args (@t454)) % 0.38/0.88 (step @p475 :rule cnf_or_pos :args (@t482)) % 0.38/0.88 (step @p476 :rule reordering :premises (@p475) :args ((or @t456 @t476 @t464 (not @t482)))) % 0.38/0.88 (step @p477 :rule instantiate :premises (@p38) :args (@t454)) % 0.38/0.88 (step @p478 :rule cnf_or_pos :args (@t483)) % 0.38/0.88 (step @p479 :rule reordering :premises (@p478) :args ((or @t189 @t456 @t476 (not @t483)))) % 0.38/0.88 (step @p480 :rule chain_m_resolution :premises (@p462 @p460 @p85 @p424 @p422 @p418 @p60 @p435 @p433 @p429 @p59 @p479 @p477 @p82 @p476 @p474 @p82 @p455 @p453 @p449 @p56 @p407 @p405 @p84 @p473 @p471 @p84 @p470 @p459 @p445) :args ((or @t192 @t186 @t409 @t415 @t418) (@list false false false true false false false true false false true false false true false false false true false false true false false true false false false true true) (@list @t478 @t102 @t429 @t449 @t453 @t78 @t423 @t459 @t463 @t77 @t188 @t483 @t99 @t462 @t482 @t99 @t474 @t471 @t475 @t74 @t190 @t437 @t101 @t468 @t481 @t101 @t434 @t438 @t425))) % 0.38/0.88 (step @p481 :rule instantiate :premises (@p42) :args (@t422)) % 0.38/0.88 (step @p482 :rule cnf_or_pos :args (@t484)) % 0.38/0.88 (step @p483 :rule reordering :premises (@p482) :args ((or @t193 @t427 @t424 (not @t484)))) % 0.38/0.88 (step @p484 :rule chain_m_resolution :premises (@p468 @p466 @p84 @p435 @p433 @p429 @p59 @p455 @p453 @p449 @p56 @p483 @p481 @p85 @p404 @p402 @p85) :args ((or @t193 @t186 @t474 @t415 @t462) @t458 (@list @t480 @t101 @t190 @t459 @t463 @t77 @t468 @t471 @t475 @t74 @t423 @t484 @t102 @t425 @t432 @t102))) % 0.38/0.88 (step @p485 :rule chain_m_resolution :premises (@p484 @p479 @p477 @p82 @p441 @p439 @p82) :args ((or @t193 @t189 @t186 @t415) @t295 (@list @t474 @t483 @t99 @t462 @t466 @t99))) % 0.38/0.88 (step @p486 :rule chain_m_resolution :premises (@p476 @p474 @p82 @p435 @p433 @p429 @p59 @p455 @p453 @p449 @p56 @p410 @p408 @p84 @p448 @p446 @p84 @p424 @p422 @p418 @p60 @p485 @p483 @p481 @p85 @p465 @p463 @p85 @p480 @p445 @p395 @p393 @p83 @p392 @p390 @p83 @p389 @p387 @p83 @p386 @p384 @p83) :args (@t412 (@list false false false true false false false true false false true false false true false false false true false false true true false false true false false false true true false false true false false true false false true false false) (@list @t482 @t99 @t462 @t459 @t463 @t77 @t474 @t471 @t475 @t74 @t190 @t440 @t101 @t468 @t470 @t101 @t438 @t449 @t453 @t78 @t188 @t423 @t484 @t102 @t429 @t479 @t102 @t192 @t425 @t186 @t421 @t100 @t418 @t420 @t100 @t415 @t417 @t100 @t409 @t414 @t100))) % 0.38/0.88 (step @p487 :rule cnf_or_pos :args (@t487)) % 0.38/0.88 (step @p488 :rule reordering :premises (@p487) :args ((or @t335 @t486 @t411 (not @t487)))) % 0.38/0.88 (step @p489 :rule chain_m_resolution :premises (@p488 @p57 @p486 @p383) :args (@t486 @t386 (@list @t75 @t411 @t487))) % 0.38/0.88 (step @p490 :rule cnf_or_pos :args (@t489)) % 0.38/0.88 (step @p491 :rule reordering :premises (@p490) :args ((or @t176 @t335 @t333 @t488 @t485 @t404 (not @t489)))) % 0.38/0.88 (step @p492 :rule instantiate :premises (@p24) :args (@t490)) % 0.38/0.88 (step @p493 :rule cnf_or_pos :args (@t495)) % 0.38/0.88 (step @p494 :rule reordering :premises (@p493) :args ((or @t494 @t493 @t491 (not @t495)))) % 0.38/0.88 (step @p495 :rule instantiate :premises (@p28) :args (@t490)) % 0.38/0.88 (step @p496 :rule cnf_or_pos :args (@t498)) % 0.38/0.88 (step @p497 :rule reordering :premises (@p496) :args ((or @t494 @t491 @t497 (not @t498)))) % 0.38/0.88 (step @p498 :rule instantiate :premises (@p29) :args (@t490)) % 0.38/0.88 (step @p499 :rule cnf_or_pos :args (@t499)) % 0.38/0.88 (step @p500 :rule reordering :premises (@p499) :args ((or @t182 @t494 @t491 (not @t499)))) % 0.38/0.88 (step @p501 :rule instantiate :premises (@p89) :args ((@list tptp.house_3 tptp.ukranian))) % 0.38/0.88 (step @p502 :rule cnf_or_pos :args (@t504)) % 0.38/0.88 (step @p503 :rule reordering :premises (@p502) :args ((or @t400 @t205 @t501 @t503 @t258 (not @t504)))) % 0.38/0.88 (step @p504 :rule instantiate :premises (@p89) :args ((@list tptp.house_4 tptp.ukranian))) % 0.38/0.88 (step @p505 :rule cnf_or_pos :args (@t507)) % 0.38/0.88 (step @p506 :rule reordering :premises (@p505) :args ((or @t400 @t276 @t506 @t503 @t313 (not @t507)))) % 0.38/0.88 (step @p507 :rule instantiate :premises (@p89) :args ((@list tptp.house_5 tptp.ukranian))) % 0.38/0.88 (step @p508 :rule cnf_or_pos :args (@t510)) % 0.38/0.88 (step @p509 :rule reordering :premises (@p508) :args ((or @t400 @t224 @t509 @t503 @t240 (not @t510)))) % 0.38/0.88 (step @p510 :rule instantiate :premises (@p1) :args (@t397)) % 0.38/0.88 (step @p511 :rule instantiate :premises (@p9) :args (@t282)) % 0.38/0.88 (step @p512 :rule cnf_or_pos :args (@t513)) % 0.38/0.88 (step @p513 :rule reordering :premises (@p512) :args ((or @t175 @t223 @t512 (not @t513)))) % 0.38/0.88 (step @p514 :rule chain_m_resolution :premises (@p513 @p88 @p61 @p511) :args (@t512 @t239 (@list @t105 @t79 @t513))) % 0.38/0.88 (step @p515 :rule cnf_or_pos :args (@t514)) % 0.38/0.88 (step @p516 :rule reordering :premises (@p515) :args ((or @t173 @t400 @t511 @t500 @t505 @t508 (not @t514)))) % 0.38/0.88 (step @p517 :rule chain_m_resolution :premises (@p516 @p514 @p510 @p59 @p509 @p507 @p65 @p59 @p506 @p504 @p64 @p59) :args ((or @t173 @t500 @t503 @t313 @t240) (@list true false false true false false false true false false false) (@list @t511 @t514 @t77 @t508 @t510 @t83 @t77 @t505 @t507 @t82 @t77))) % 0.38/0.88 (step @p518 :rule instantiate :premises (@p89) :args ((@list tptp.house_2 tptp.ukranian))) % 0.38/0.88 (step @p519 :rule cnf_or_pos :args (@t515)) % 0.38/0.88 (step @p520 :rule reordering :premises (@p519) :args ((or @t174 @t400 @t233 @t503 @t296 (not @t515)))) % 0.38/0.88 (step @p521 :rule chain_m_resolution :premises (@p520 @p518 @p62 @p59 @p517 @p503 @p501 @p63 @p59) :args ((or @t503 @t296 @t258 @t313 @t240) (@list false false false false true false false false) (@list @t515 @t80 @t77 @t173 @t500 @t504 @t81 @t77))) % 0.38/0.88 (step @p522 :rule instantiate :premises (@p23) :args (@t397)) % 0.38/0.88 (step @p523 :rule instantiate :premises (@p33) :args (@t403)) % 0.38/0.88 (step @p524 :rule cnf_or_pos :args (@t518)) % 0.38/0.88 (step @p525 :rule reordering :premises (@p524) :args ((or @t180 @t406 @t517 (not @t518)))) % 0.38/0.88 (step @p526 :rule chain_m_resolution :premises (@p525 @p95 @p71 @p523) :args (@t517 @t239 (@list @t128 @t89 @t518))) % 0.38/0.88 (step @p527 :rule cnf_or_pos :args (@t520)) % 0.38/0.88 (step @p528 :rule reordering :premises (@p527) :args ((or @t181 @t400 @t502 @t519 @t398 @t516 (not @t520)))) % 0.38/0.88 (step @p529 :rule instantiate :premises (@p31) :args (@t521)) % 0.38/0.88 (step @p530 :rule cnf_or_pos :args (@t526)) % 0.38/0.88 (step @p531 :rule reordering :premises (@p530) :args ((or @t525 @t524 @t522 (not @t526)))) % 0.38/0.88 (step @p532 :rule instantiate :premises (@p26) :args (@t521)) % 0.38/0.88 (step @p533 :rule cnf_or_pos :args (@t527)) % 0.38/0.88 (step @p534 :rule reordering :premises (@p533) :args ((or @t179 @t525 @t522 (not @t527)))) % 0.38/0.88 (step @p535 :rule instantiate :premises (@p23) :args (@t281)) % 0.38/0.88 (step @p536 :rule instantiate :premises (@p27) :args (@t403)) % 0.38/0.88 (step @p537 :rule cnf_or_pos :args (@t530)) % 0.38/0.88 (step @p538 :rule reordering :premises (@p537) :args ((or @t180 @t406 @t529 (not @t530)))) % 0.38/0.88 (step @p539 :rule chain_m_resolution :premises (@p538 @p95 @p71 @p536) :args (@t529 @t239 (@list @t128 @t89 @t530))) % 0.38/0.88 (step @p540 :rule cnf_or_pos :args (@t532)) % 0.38/0.88 (step @p541 :rule reordering :premises (@p540) :args ((or @t178 @t286 @t310 @t492 @t531 @t528 (not @t532)))) % 0.38/0.88 (step @p542 :rule instantiate :premises (@p25) :args ((@list tptp.honda))) % 0.38/0.88 (step @p543 :rule cnf_or_pos :args (@t537)) % 0.38/0.88 (step @p544 :rule reordering :premises (@p543) :args ((or @t536 @t535 @t534 (not @t537)))) % 0.38/0.88 (step @p545 :rule instantiate :premises (@p93) :args (@t281)) % 0.38/0.88 (step @p546 :rule cnf_or_pos :args (@t538)) % 0.38/0.88 (step @p547 :rule reordering :premises (@p546) :args ((or @t286 @t361 @t535 (not @t538)))) % 0.38/0.88 (step @p548 :rule instantiate :premises (@p23) :args (@t375)) % 0.38/0.88 (step @p549 :rule instantiate :premises (@p32) :args (@t403)) % 0.38/0.88 (step @p550 :rule cnf_or_pos :args (@t541)) % 0.38/0.88 (step @p551 :rule reordering :premises (@p550) :args ((or @t180 @t406 @t540 (not @t541)))) % 0.38/0.88 (step @p552 :rule chain_m_resolution :premises (@p551 @p95 @p71 @p549) :args (@t540 @t239 (@list @t128 @t89 @t541))) % 0.38/0.88 (step @p553 :rule cnf_or_pos :args (@t542)) % 0.38/0.88 (step @p554 :rule reordering :premises (@p553) :args ((or @t183 @t353 @t496 @t523 @t533 @t539 (not @t542)))) % 0.38/0.88 (step @p555 :rule instantiate :premises (@p14) :args (@t358)) % 0.38/0.88 (step @p556 :rule cnf_or_pos :args (@t543)) % 0.38/0.88 (step @p557 :rule reordering :premises (@p556) :args ((or @t363 @t362 @t366 (not @t543)))) % 0.38/0.88 (step @p558 :rule instantiate :premises (@p16) :args (@t358)) % 0.38/0.88 (step @p559 :rule cnf_or_pos :args (@t546)) % 0.38/0.88 (step @p560 :rule reordering :premises (@p559) :args ((or @t363 @t362 @t545 (not @t546)))) % 0.38/0.88 (step @p561 :rule instantiate :premises (@p21) :args (@t391)) % 0.38/0.88 (step @p562 :rule cnf_or_pos :args (@t549)) % 0.38/0.88 (step @p563 :rule reordering :premises (@p562) :args ((or @t202 @t393 @t548 (not @t549)))) % 0.38/0.88 (assume-push @p1068 @t73) % 0.38/0.88 (step-pop @p1069 :rule scope :premises (@p251)) % 0.38/0.88 (step @p565 :rule process_scope :premises (@p1069) :args (@t307)) % 0.38/0.88 (step @p567 :rule implies_elim :premises (@p565)) % 0.38/0.88 (assume-push @p1070 @t68) % 0.38/0.88 (step-pop @p1071 :rule scope :premises (@p217)) % 0.38/0.88 (step @p569 :rule process_scope :premises (@p1071) :args (@t293)) % 0.38/0.88 (step @p571 :rule implies_elim :premises (@p569)) % 0.38/0.88 (assume-push @p1072 @t121) % 0.38/0.88 (step-pop @p1073 :rule scope :premises (@p148)) % 0.38/0.88 (step @p573 :rule process_scope :premises (@p1073) :args (@t234)) % 0.38/0.88 (step @p575 :rule implies_elim :premises (@p573)) % 0.38/0.88 (assume-push @p1074 @t137) % 0.38/0.88 (step-pop @p1075 :rule scope :premises (@p149)) % 0.38/0.88 (step @p577 :rule process_scope :premises (@p1075) :args (@t230)) % 0.38/0.88 (step @p579 :rule implies_elim :premises (@p577)) % 0.38/0.88 (assume-push @p1076 @t64) % 0.38/0.88 (step-pop @p1077 :rule scope :premises (@p216)) % 0.38/0.88 (step @p581 :rule process_scope :premises (@p1077) :args (@t294)) % 0.38/0.88 (step @p583 :rule implies_elim :premises (@p581)) % 0.38/0.88 (assume-push @p1078 @t71) % 0.38/0.88 (step-pop @p1079 :rule scope :premises (@p318)) % 0.38/0.88 (step @p585 :rule process_scope :premises (@p1079) :args (@t350)) % 0.38/0.88 (step @p587 :rule implies_elim :premises (@p585)) % 0.38/0.88 (assume-push @p1080 @t130) % 0.38/0.88 (step-pop @p1081 :rule scope :premises (@p326)) % 0.38/0.88 (step @p589 :rule process_scope :premises (@p1081) :args (@t357)) % 0.38/0.88 (step @p591 :rule implies_elim :premises (@p589)) % 0.38/0.88 (assume-push @p1082 @t131) % 0.38/0.88 (step-pop @p1083 :rule scope :premises (@p245)) % 0.38/0.88 (step @p593 :rule process_scope :premises (@p1083) :args (@t305)) % 0.38/0.88 (step @p595 :rule implies_elim :premises (@p593)) % 0.38/0.88 (assume-push @p1084 @t130) % 0.38/0.88 (step-pop @p1085 :rule scope :premises (@p323)) % 0.38/0.88 (step @p597 :rule process_scope :premises (@p1085) :args (@t354)) % 0.38/0.88 (step @p599 :rule implies_elim :premises (@p597)) % 0.38/0.88 (assume-push @p1086 @t126) % 0.38/0.88 (step-pop @p1087 :rule scope :premises (@p375)) % 0.38/0.88 (step @p601 :rule process_scope :premises (@p1087) :args (@t402)) % 0.38/0.88 (step @p603 :rule implies_elim :premises (@p601)) % 0.38/0.88 (assume-push @p1088 @t125) % 0.38/0.88 (step-pop @p1089 :rule scope :premises (@p383)) % 0.38/0.88 (step @p605 :rule process_scope :premises (@p1089) :args (@t487)) % 0.38/0.88 (step @p607 :rule implies_elim :premises (@p605)) % 0.38/0.88 (assume-push @p1090 @t46) % 0.38/0.88 (step-pop @p1091 :rule scope :premises (@p379)) % 0.38/0.88 (step @p609 :rule process_scope :premises (@p1091) :args (@t407)) % 0.38/0.88 (step @p611 :rule implies_elim :premises (@p609)) % 0.38/0.88 (assume-push @p1092 @t33) % 0.38/0.88 (step-pop @p1093 :rule scope :premises (@p378)) % 0.38/0.88 (step @p613 :rule process_scope :premises (@p1093) :args (@t489)) % 0.38/0.88 (step @p615 :rule implies_elim :premises (@p613)) % 0.38/0.88 (assume-push @p1094 @t45) % 0.38/0.88 (step-pop @p1095 :rule scope :premises (@p498)) % 0.38/0.88 (step @p617 :rule process_scope :premises (@p1095) :args (@t499)) % 0.38/0.88 (step @p619 :rule implies_elim :premises (@p617)) % 0.38/0.88 (assume-push @p1096 @t49) % 0.38/0.88 (step-pop @p1097 :rule scope :premises (@p523)) % 0.38/0.88 (step @p621 :rule process_scope :premises (@p1097) :args (@t518)) % 0.38/0.88 (step @p623 :rule implies_elim :premises (@p621)) % 0.38/0.88 (assume-push @p1098 @t33) % 0.38/0.88 (step-pop @p1099 :rule scope :premises (@p522)) % 0.38/0.88 (step @p625 :rule process_scope :premises (@p1099) :args (@t520)) % 0.38/0.88 (step @p627 :rule implies_elim :premises (@p625)) % 0.38/0.88 (assume-push @p1100 @t126) % 0.38/0.88 (step-pop @p1101 :rule scope :premises (@p372)) % 0.38/0.88 (step @p629 :rule process_scope :premises (@p1101) :args (@t401)) % 0.38/0.88 (step @p631 :rule implies_elim :premises (@p629)) % 0.38/0.88 (assume-push @p1102 @t125) % 0.38/0.88 (step @p633 :rule instantiate :premises (@p92) :args (@t397)) % 0.38/0.88 (step-pop @p1103 :rule scope :premises (@p633)) % 0.38/0.88 (step @p634 :rule process_scope :premises (@p1103) :args (@t550)) % 0.38/0.88 (step @p636 :rule implies_elim :premises (@p634)) % 0.38/0.88 (step @p637 :rule cnf_or_pos :args (@t550)) % 0.38/0.88 (step @p638 :rule reordering :premises (@p637) :args ((or @t400 @t522 @t415 (not @t550)))) % 0.38/0.88 (assume-push @p1104 @t60) % 0.38/0.88 (step @p640 :rule instantiate :premises (@p44) :args (@t408)) % 0.38/0.88 (step-pop @p1105 :rule scope :premises (@p640)) % 0.38/0.88 (step @p641 :rule process_scope :premises (@p1105) :args (@t551)) % 0.38/0.88 (step @p643 :rule implies_elim :premises (@p641)) % 0.38/0.88 (step @p644 :rule cnf_or_pos :args (@t551)) % 0.38/0.88 (step @p645 :rule reordering :premises (@p644) :args ((or @t413 @t416 @t419 (not @t551)))) % 0.38/0.88 (assume-push @p1106 @t56) % 0.38/0.88 (step @p647 :rule instantiate :premises (@p37) :args (@t408)) % 0.38/0.88 (step-pop @p1107 :rule scope :premises (@p647)) % 0.38/0.88 (step @p648 :rule process_scope :premises (@p1107) :args (@t552)) % 0.38/0.88 (step @p650 :rule implies_elim :premises (@p648)) % 0.38/0.88 (step @p651 :rule cnf_or_pos :args (@t552)) % 0.38/0.88 (step @p652 :rule reordering :premises (@p651) :args ((or @t187 @t413 @t416 (not @t552)))) % 0.38/0.88 (assume-push @p1108 @t41) % 0.38/0.88 (step-pop @p1109 :rule scope :premises (@p532)) % 0.38/0.88 (step @p654 :rule process_scope :premises (@p1109) :args (@t527)) % 0.38/0.88 (step @p656 :rule implies_elim :premises (@p654)) % 0.38/0.88 (assume-push @p1110 @t106) % 0.38/0.88 (step-pop @p1111 :rule scope :premises (@p258)) % 0.38/0.88 (step @p658 :rule process_scope :premises (@p1111) :args (@t312)) % 0.38/0.88 (step @p660 :rule implies_elim :premises (@p658)) % 0.38/0.88 (assume-push @p1112 @t43) % 0.38/0.88 (step-pop @p1113 :rule scope :premises (@p536)) % 0.38/0.88 (step @p662 :rule process_scope :premises (@p1113) :args (@t530)) % 0.38/0.88 (step @p664 :rule implies_elim :premises (@p662)) % 0.38/0.88 (assume-push @p1114 @t33) % 0.38/0.88 (step-pop @p1115 :rule scope :premises (@p535)) % 0.38/0.88 (step @p666 :rule process_scope :premises (@p1115) :args (@t532)) % 0.38/0.88 (step @p668 :rule implies_elim :premises (@p666)) % 0.38/0.88 (assume-push @p1116 @t37) % 0.38/0.88 (step-pop @p1117 :rule scope :premises (@p492)) % 0.38/0.88 (step @p670 :rule process_scope :premises (@p1117) :args (@t495)) % 0.38/0.88 (step @p672 :rule implies_elim :premises (@p670)) % 0.38/0.88 (assume-push @p1118 @t39) % 0.38/0.88 (step-pop @p1119 :rule scope :premises (@p542)) % 0.38/0.88 (step @p674 :rule process_scope :premises (@p1119) :args (@t537)) % 0.38/0.88 (step @p676 :rule implies_elim :premises (@p674)) % 0.38/0.88 (assume-push @p1120 @t47) % 0.38/0.88 (step-pop @p1121 :rule scope :premises (@p529)) % 0.38/0.88 (step @p678 :rule process_scope :premises (@p1121) :args (@t526)) % 0.38/0.88 (step @p680 :rule implies_elim :premises (@p678)) % 0.38/0.88 (assume-push @p1122 @t48) % 0.38/0.88 (step-pop @p1123 :rule scope :premises (@p549)) % 0.38/0.88 (step @p682 :rule process_scope :premises (@p1123) :args (@t541)) % 0.38/0.88 (step @p684 :rule implies_elim :premises (@p682)) % 0.38/0.88 (assume-push @p1124 @t33) % 0.38/0.88 (step-pop @p1125 :rule scope :premises (@p548)) % 0.38/0.88 (step @p686 :rule process_scope :premises (@p1125) :args (@t542)) % 0.38/0.88 (step @p688 :rule implies_elim :premises (@p686)) % 0.38/0.88 (assume-push @p1126 @t44) % 0.38/0.88 (step-pop @p1127 :rule scope :premises (@p495)) % 0.38/0.88 (step @p690 :rule process_scope :premises (@p1127) :args (@t498)) % 0.38/0.88 (step @p692 :rule implies_elim :premises (@p690)) % 0.38/0.88 (assume-push @p1128 @t129) % 0.38/0.88 (step @p694 :rule instantiate :premises (@p96) :args (@t553)) % 0.38/0.88 (step-pop @p1129 :rule scope :premises (@p694)) % 0.38/0.88 (step @p695 :rule process_scope :premises (@p1129) :args (@t555)) % 0.38/0.88 (step @p697 :rule implies_elim :premises (@p695)) % 0.38/0.88 (assume-push @p1130 @t139) % 0.38/0.88 (step @p699 :rule instantiate :premises (@p102) :args (@t222)) % 0.38/0.88 (step-pop @p1131 :rule scope :premises (@p699)) % 0.38/0.88 (step @p700 :rule process_scope :premises (@p1131) :args (@t557)) % 0.38/0.88 (step @p702 :rule implies_elim :premises (@p700)) % 0.38/0.88 (step @p703 :rule cnf_or_pos :args (@t557)) % 0.38/0.88 (step @p704 :rule reordering :premises (@p703) :args ((or @t145 @t154 @t556 (not @t557)))) % 0.38/0.88 (step @p705 :rule cnf_or_pos :args (@t555)) % 0.38/0.88 (step @p706 :rule reordering :premises (@p705) :args ((or @t184 @t175 @t286 @t353 @t223 @t224 @t279 @t469 @t554 (not @t555)))) % 0.38/0.88 (assume-push @p1132 @t58) % 0.38/0.88 (step @p708 :rule instantiate :premises (@p42) :args (@t408)) % 0.38/0.88 (step-pop @p1133 :rule scope :premises (@p708)) % 0.38/0.88 (step @p709 :rule process_scope :premises (@p1133) :args (@t558)) % 0.38/0.88 (step @p711 :rule implies_elim :premises (@p709)) % 0.38/0.88 (step @p712 :rule cnf_or_pos :args (@t558)) % 0.38/0.88 (step @p713 :rule reordering :premises (@p712) :args ((or @t413 @t410 @t416 (not @t558)))) % 0.38/0.88 (assume-push @p1134 @t129) % 0.38/0.88 (step @p715 :rule instantiate :premises (@p96) :args (@t559)) % 0.38/0.88 (step-pop @p1135 :rule scope :premises (@p715)) % 0.38/0.88 (step @p716 :rule process_scope :premises (@p1135) :args (@t561)) % 0.38/0.88 (step @p718 :rule implies_elim :premises (@p716)) % 0.38/0.88 (assume-push @p1136 @t139) % 0.38/0.88 (step @p720 :rule instantiate :premises (@p102) :args (@t562)) % 0.38/0.88 (step-pop @p1137 :rule scope :premises (@p720)) % 0.38/0.88 (step @p721 :rule process_scope :premises (@p1137) :args (@t564)) % 0.38/0.88 (step @p723 :rule implies_elim :premises (@p721)) % 0.38/0.88 (step @p724 :rule cnf_or_pos :args (@t564)) % 0.38/0.88 (step @p725 :rule factoring :premises (@p724)) % 0.38/0.88 (step @p726 :rule reordering :premises (@p725) :args ((or @t142 @t563 (not @t564)))) % 0.38/0.88 (step @p727 :rule cnf_or_pos :args (@t561)) % 0.38/0.88 (step @p728 :rule factoring :premises (@p727)) % 0.38/0.88 (step @p729 :rule reordering :premises (@p728) :args ((or @t184 @t175 @t353 @t223 @t435 @t560 (not @t561)))) % 0.38/0.88 (assume-push @p1138 @t59) % 0.38/0.88 (step-pop @p1139 :rule scope :premises (@p463)) % 0.38/0.88 (step @p731 :rule process_scope :premises (@p1139) :args (@t479)) % 0.38/0.88 (step @p733 :rule implies_elim :premises (@p731)) % 0.38/0.88 (assume-push @p1140 @t54) % 0.38/0.88 (step-pop @p1141 :rule scope :premises (@p402)) % 0.38/0.88 (step @p735 :rule process_scope :premises (@p1141) :args (@t432)) % 0.38/0.88 (step @p737 :rule implies_elim :premises (@p735)) % 0.38/0.88 (assume-push @p1142 @t131) % 0.38/0.88 (step @p739 :rule instantiate :premises (@p99) :args (@t345)) % 0.38/0.88 (step-pop @p1143 :rule scope :premises (@p739)) % 0.38/0.88 (step @p740 :rule process_scope :premises (@p1143) :args (@t567)) % 0.38/0.88 (step @p742 :rule implies_elim :premises (@p740)) % 0.38/0.88 (step @p743 :rule cnf_or_pos :args (@t567)) % 0.38/0.88 (step @p744 :rule reordering :premises (@p743) :args ((or @t335 @t331 @t566 (not @t567)))) % 0.38/0.88 (step @p745 :rule instantiate :premises (@p98) :args ((@list tptp.house_5 tptp.house_4))) % 0.38/0.88 (step @p746 :rule cnf_or_pos :args (@t568)) % 0.38/0.88 (step @p747 :rule reordering :premises (@p746) :args ((or @t153 @t276 @t224 @t323 @t217 (not @t568)))) % 0.38/0.88 (step @p748 :rule instantiate :premises (@p55) :args (@t246)) % 0.38/0.88 (step @p749 :rule cnf_or_pos :args (@t569)) % 0.38/0.88 (step @p750 :rule reordering :premises (@p749) :args ((or @t158 @t247 @t323 (not @t569)))) % 0.38/0.88 (step @p751 :rule chain_m_resolution :premises (@p160 @p146 @p65 @p750 @p748 @p67 @p747 @p745 @p123 @p65 @p64) :args ((or @t208 @t240 @t235 @t323) (@list false false true false false true false true false false) (@list @t241 @t83 @t157 @t569 @t85 @t216 @t568 @t153 @t83 @t82))) % 0.38/0.88 (step @p752 :rule cnf_or_pos :args (@t570)) % 0.38/0.88 (step @p753 :rule reordering :premises (@p752) :args ((or @t162 @t212 @t267 (not @t570)))) % 0.38/0.88 (step @p754 :rule instantiate :premises (@p50) :args (@t203)) % 0.38/0.88 (step @p755 :rule cnf_or_pos :args (@t571)) % 0.38/0.88 (step @p756 :rule reordering :premises (@p755) :args ((or @t162 @t212 @t264 (not @t571)))) % 0.38/0.88 (step @p757 :rule instantiate :premises (@p55) :args (@t215)) % 0.38/0.88 (step @p758 :rule cnf_or_pos :args (@t572)) % 0.38/0.88 (step @p759 :rule reordering :premises (@p758) :args ((or @t160 @t220 @t217 (not @t572)))) % 0.38/0.88 (step @p760 :rule instantiate :premises (@p98) :args ((@list tptp.house_4 tptp.house_2))) % 0.38/0.88 (step @p761 :rule cnf_or_pos :args (@t573)) % 0.38/0.88 (step @p762 :rule reordering :premises (@p761) :args ((or @t147 @t160 @t233 @t276 @t328 (not @t573)))) % 0.38/0.88 (step @p763 :rule chain_m_resolution :premises (@p317 @p320 @p318 @p68 @p230 @p228 @p68) :args ((or @t166 @t331 @t334 @t240) @t295 (@list @t313 @t350 @t86 @t296 @t299 @t86))) % 0.38/0.88 (step @p764 :rule instantiate :premises (@p4) :args (@t204)) % 0.38/0.88 (step @p765 :rule cnf_or_pos :args (@t574)) % 0.38/0.88 (step @p766 :rule reordering :premises (@p765) :args ((or @t170 @t205 @t501 (not @t574)))) % 0.38/0.88 (step @p767 :rule instantiate :premises (@p5) :args (@t204)) % 0.38/0.88 (step @p768 :rule cnf_or_pos :args (@t577)) % 0.38/0.88 (step @p769 :rule reordering :premises (@p768) :args ((or @t170 @t205 @t576 (not @t577)))) % 0.38/0.88 (step @p770 :rule instantiate :premises (@p89) :args ((@list tptp.house_3 tptp.english))) % 0.38/0.88 (step @p771 :rule cnf_or_pos :args (@t578)) % 0.38/0.88 (step @p772 :rule reordering :premises (@p771) :args ((or @t170 @t286 @t205 @t311 @t258 (not @t578)))) % 0.38/0.88 (step @p773 :rule instantiate :premises (@p102) :args (@t325)) % 0.38/0.88 (step @p774 :rule cnf_or_pos :args (@t581)) % 0.38/0.88 (step @p775 :rule reordering :premises (@p774) :args ((or @t144 @t152 @t580 (not @t581)))) % 0.38/0.88 (step @p776 :rule chain_m_resolution :premises (@p775 @p110 @p120 @p773) :args (@t580 @t582 (@list @t144 @t152 @t581))) % 0.38/0.88 (step @p777 :rule instantiate :premises (@p90) :args ((@list tptp.house_1 tptp.house_4 tptp.norwegian tptp.spaniard))) % 0.38/0.88 (step @p778 :rule cnf_or_pos :args (@t583)) % 0.38/0.88 (step @p779 :rule reordering :premises (@p778) :args ((or @t193 @t175 @t168 @t335 @t353 @t223 @t276 @t491 @t579 (not @t583)))) % 0.38/0.88 (step @p699 :rule instantiate :premises (@p102) :args (@t222)) % 0.38/0.88 (step @p780 :rule chain_m_resolution :premises (@p704 @p111 @p124 @p699) :args (@t556 @t582 (@list @t145 @t154 @t557))) % 0.38/0.88 (step @p781 :rule instantiate :premises (@p90) :args ((@list tptp.house_1 tptp.house_5 tptp.norwegian tptp.spaniard))) % 0.38/0.88 (step @p782 :rule cnf_or_pos :args (@t584)) % 0.38/0.88 (step @p783 :rule reordering :premises (@p782) :args ((or @t193 @t175 @t335 @t353 @t223 @t224 @t343 @t491 @t554 (not @t584)))) % 0.38/0.88 (step @p784 :rule instantiate :premises (@p97) :args (@t338)) % 0.38/0.88 (step @p785 :rule cnf_or_pos :args (@t587)) % 0.38/0.88 (step @p786 :rule reordering :premises (@p785) :args ((or @t335 @t233 @t340 @t586 @t327 (not @t587)))) % 0.38/0.88 (step @p787 :rule instantiate :premises (@p12) :args (@t345)) % 0.38/0.88 (step @p788 :rule instantiate :premises (@p18) :args (@t368)) % 0.38/0.88 (step @p789 :rule cnf_or_pos :args (@t590)) % 0.38/0.88 (step @p790 :rule reordering :premises (@p789) :args ((or @t200 @t371 @t589 (not @t590)))) % 0.38/0.88 (step @p791 :rule chain_m_resolution :premises (@p790 @p94 @p76 @p788) :args (@t589 @t239 (@list @t127 @t94 @t590))) % 0.38/0.88 (step @p792 :rule cnf_or_pos :args (@t592)) % 0.38/0.88 (step @p793 :rule reordering :premises (@p792) :args ((or @t194 @t335 @t585 @t588 @t565 @t591 (not @t592)))) % 0.38/0.88 (step @p794 :rule instantiate :premises (@p17) :args (@t391)) % 0.38/0.88 (step @p795 :rule cnf_or_pos :args (@t594)) % 0.38/0.88 (step @p796 :rule reordering :premises (@p795) :args ((or @t202 @t393 @t593 (not @t594)))) % 0.38/0.88 (step @p797 :rule chain_m_resolution :premises (@p796 @p794 @p78 @p360 @p358 @p354 @p353 @p58 @p793 @p791 @p787 @p57 @p557 @p555 @p77 @p786 @p784 @p62 @p57 @p547 @p545 @p56 @p316 @p314 @p310 @p57 @p541 @p539 @p535 @p56 @p779 @p777 @p776 @p88 @p64 @p61 @p58 @p57 @p494 @p492 @p75 @p491 @p489 @p382 @p378 @p57 @p377 @p375 @p57 @p744 @p57 @p742 @p99) :args ((or @t194 @t193 @t178 @t331 @t342 @t351 @t310 @t333 @t327) (@list false false false true false true false false true false false true false false true false false false false false false false true false false false true false false true false true false false false false false true false false false true true false false true false false true false false false) (@list @t594 @t96 @t201 @t387 @t390 @t383 @t76 @t591 @t588 @t592 @t75 @t365 @t543 @t95 @t585 @t587 @t80 @t75 @t361 @t538 @t74 @t339 @t346 @t349 @t75 @t531 @t528 @t532 @t74 @t167 @t583 @t579 @t105 @t82 @t79 @t76 @t75 @t492 @t495 @t93 @t488 @t485 @t404 @t489 @t75 @t176 @t402 @t75 @t565 @t75 @t567 @t131))) % 0.38/0.88 (step @p798 :rule instantiate :premises (@p7) :args (@t269)) % 0.38/0.88 (step @p799 :rule cnf_or_pos :args (@t595)) % 0.38/0.88 (step @p800 :rule reordering :premises (@p799) :args ((or @t174 @t233 @t340 (not @t595)))) % 0.38/0.88 (step @p801 :rule chain_m_resolution :premises (@p334 @p332 @p77 @p360 @p358 @p354 @p353 @p58 @p374 @p372 @p59 @p796 @p794 @p78 @p528 @p526 @p522 @p59 @p793 @p791 @p787 @p57 @p517 @p534 @p532 @p74 @p786 @p784 @p62 @p57 @p800 @p798 @p62 @p797 @p316 @p314 @p310 @p57 @p783 @p781 @p780 @p88 @p65 @p61 @p58 @p57 @p779 @p777 @p776 @p88 @p64 @p61 @p58 @p57 @p500 @p498 @p75 @p491 @p489 @p382 @p378 @p57 @p377 @p375 @p57 @p744 @p57 @p742 @p99) :args ((or @t194 @t193 @t331 @t500 @t351 @t310 @t333 @t327 @t313 @t240) (@list false false false true false true false false false false true false false false true false false false true false false true true false false true false false false true false false false false true false false true false true false false false false false true false true false false false false false true false false false true true false false true false false true false false false) (@list @t367 @t95 @t365 @t387 @t390 @t383 @t76 @t359 @t401 @t77 @t201 @t594 @t96 @t398 @t516 @t520 @t77 @t591 @t588 @t592 @t75 @t502 @t519 @t527 @t92 @t585 @t587 @t80 @t75 @t173 @t595 @t80 @t178 @t339 @t346 @t349 @t75 @t342 @t584 @t554 @t105 @t83 @t79 @t76 @t75 @t167 @t583 @t579 @t105 @t82 @t79 @t76 @t75 @t181 @t499 @t93 @t488 @t485 @t404 @t489 @t75 @t176 @t402 @t75 @t565 @t75 @t567 @t131))) % 0.38/0.88 (step @p802 :rule instantiate :premises (@p99) :args (@t448)) % 0.38/0.88 (step @p803 :rule cnf_or_pos :args (@t598)) % 0.38/0.88 (step @p804 :rule reordering :premises (@p803) :args ((or @t452 @t575 @t597 (not @t598)))) % 0.38/0.88 (step @p805 :rule instantiate :premises (@p18) :args (@t358)) % 0.38/0.88 (step @p806 :rule cnf_or_pos :args (@t599)) % 0.38/0.88 (step @p807 :rule reordering :premises (@p806) :args ((or @t195 @t363 @t360 (not @t599)))) % 0.38/0.88 (step @p808 :rule instantiate :premises (@p19) :args (@t358)) % 0.38/0.88 (step @p809 :rule cnf_or_pos :args (@t600)) % 0.38/0.88 (step @p810 :rule reordering :premises (@p809) :args ((or @t195 @t363 @t545 (not @t600)))) % 0.38/0.88 (step @p811 :rule instantiate :premises (@p93) :args (@t375)) % 0.38/0.88 (step @p812 :rule cnf_or_pos :args (@t601)) % 0.38/0.88 (step @p813 :rule reordering :premises (@p812) :args ((or @t353 @t365 @t534 (not @t601)))) % 0.38/0.88 (step @p814 :rule instantiate :premises (@p12) :args (@t448)) % 0.38/0.88 (step @p815 :rule instantiate :premises (@p22) :args (@t368)) % 0.38/0.88 (step @p816 :rule cnf_or_pos :args (@t604)) % 0.38/0.88 (step @p817 :rule reordering :premises (@p816) :args ((or @t200 @t371 @t603 (not @t604)))) % 0.38/0.88 (step @p818 :rule chain_m_resolution :premises (@p817 @p94 @p76 @p815) :args (@t603 @t239 (@list @t127 @t94 @t604))) % 0.38/0.88 (step @p819 :rule cnf_or_pos :args (@t605)) % 0.38/0.88 (step @p820 :rule reordering :premises (@p819) :args ((or @t198 @t452 @t544 @t602 @t596 @t547 (not @t605)))) % 0.38/0.88 (step @p821 :rule instantiate :premises (@p97) :args ((@list tptp.house_2 tptp.japanese))) % 0.38/0.88 (step @p822 :rule cnf_or_pos :args (@t608)) % 0.38/0.88 (step @p823 :rule reordering :premises (@p822) :args ((or @t199 @t452 @t233 @t607 @t327 (not @t608)))) % 0.38/0.88 (step @p824 :rule instantiate :premises (@p97) :args ((@list tptp.house_4 tptp.japanese))) % 0.38/0.88 (step @p825 :rule cnf_or_pos :args (@t611)) % 0.38/0.88 (step @p826 :rule reordering :premises (@p825) :args ((or @t199 @t452 @t276 @t610 @t319 (not @t611)))) % 0.38/0.88 (step @p827 :rule instantiate :premises (@p1) :args (@t448)) % 0.38/0.88 (step @p828 :rule instantiate :premises (@p10) :args (@t282)) % 0.38/0.88 (step @p829 :rule cnf_or_pos :args (@t614)) % 0.38/0.88 (step @p830 :rule reordering :premises (@p829) :args ((or @t175 @t223 @t613 (not @t614)))) % 0.38/0.88 (step @p831 :rule chain_m_resolution :premises (@p830 @p88 @p61 @p828) :args (@t613 @t239 (@list @t105 @t79 @t614))) % 0.38/0.88 (step @p832 :rule cnf_or_pos :args (@t615)) % 0.38/0.88 (step @p833 :rule reordering :premises (@p832) :args ((or @t171 @t452 @t612 @t606 @t575 @t609 (not @t615)))) % 0.38/0.88 (assume-push @p1144 @t14) % 0.38/0.88 (step @p835 :rule instantiate :premises (@p8) :args (@t226)) % 0.38/0.88 (step-pop @p1145 :rule scope :premises (@p835)) % 0.38/0.88 (step @p836 :rule process_scope :premises (@p1145) :args (@t616)) % 0.38/0.88 (step @p838 :rule implies_elim :premises (@p836)) % 0.38/0.88 (step @p839 :rule cnf_or_pos :args (@t616)) % 0.38/0.88 (step @p840 :rule reordering :premises (@p839) :args ((or @t172 @t224 @t343 (not @t616)))) % 0.38/0.88 (assume-push @p1146 @t30) % 0.38/0.88 (step-pop @p1147 :rule scope :premises (@p561)) % 0.38/0.88 (step @p842 :rule process_scope :premises (@p1147) :args (@t549)) % 0.38/0.88 (step @p844 :rule implies_elim :premises (@p842)) % 0.38/0.88 (assume-push @p1148 @t31) % 0.38/0.88 (step-pop @p1149 :rule scope :premises (@p815)) % 0.38/0.88 (step @p846 :rule process_scope :premises (@p1149) :args (@t604)) % 0.38/0.88 (step @p848 :rule implies_elim :premises (@p846)) % 0.38/0.88 (assume-push @p1150 @t29) % 0.38/0.88 (step-pop @p1151 :rule scope :premises (@p808)) % 0.38/0.88 (step @p850 :rule process_scope :premises (@p1151) :args (@t600)) % 0.38/0.88 (step @p852 :rule implies_elim :premises (@p850)) % 0.38/0.88 (assume-push @p1152 @t16) % 0.38/0.88 (step-pop @p1153 :rule scope :premises (@p814)) % 0.38/0.88 (step @p854 :rule process_scope :premises (@p1153) :args (@t605)) % 0.38/0.88 (step @p856 :rule implies_elim :premises (@p854)) % 0.38/0.88 (assume-push @p1154 @t13) % 0.38/0.88 (step-pop @p1155 :rule scope :premises (@p767)) % 0.38/0.88 (step @p858 :rule process_scope :premises (@p1155) :args (@t577)) % 0.38/0.88 (step @p860 :rule implies_elim :premises (@p858)) % 0.38/0.88 (assume-push @p1156 @t131) % 0.38/0.88 (step-pop @p1157 :rule scope :premises (@p802)) % 0.38/0.88 (step @p862 :rule process_scope :premises (@p1157) :args (@t598)) % 0.38/0.88 (step @p864 :rule implies_elim :premises (@p862)) % 0.38/0.88 (assume-push @p1158 @t26) % 0.38/0.88 (step @p866 :rule instantiate :premises (@p16) :args (@t617)) % 0.38/0.88 (step-pop @p1159 :rule scope :premises (@p866)) % 0.38/0.88 (step @p867 :rule process_scope :premises (@p1159) :args (@t619)) % 0.38/0.88 (step @p869 :rule implies_elim :premises (@p867)) % 0.38/0.88 (step @p870 :rule cnf_or_pos :args (@t619)) % 0.38/0.88 (step @p871 :rule reordering :premises (@p870) :args ((or @t199 @t618 @t356 (not @t619)))) % 0.38/0.88 (assume-push @p1160 @t24) % 0.38/0.88 (step-pop @p1161 :rule scope :premises (@p336)) % 0.38/0.88 (step @p873 :rule process_scope :premises (@p1161) :args (@t372)) % 0.38/0.88 (step @p875 :rule implies_elim :premises (@p873)) % 0.38/0.88 (assume-push @p1162 @t22) % 0.38/0.88 (step-pop @p1163 :rule scope :premises (@p361)) % 0.38/0.88 (step @p877 :rule process_scope :premises (@p1163) :args (@t394)) % 0.38/0.88 (step @p879 :rule implies_elim :premises (@p877)) % 0.38/0.88 (assume-push @p1164 @t16) % 0.38/0.88 (step-pop @p1165 :rule scope :premises (@p335)) % 0.38/0.88 (step @p881 :rule process_scope :premises (@p1165) :args (@t374)) % 0.38/0.88 (step @p883 :rule implies_elim :premises (@p881)) % 0.38/0.88 (assume-push @p1166 @t20) % 0.38/0.88 (step-pop @p1167 :rule scope :premises (@p368)) % 0.38/0.88 (step @p885 :rule process_scope :premises (@p1167) :args (@t396)) % 0.38/0.88 (step @p887 :rule implies_elim :premises (@p885)) % 0.38/0.88 (assume-push @p1168 @t11) % 0.38/0.88 (step-pop @p1169 :rule scope :premises (@p764)) % 0.38/0.88 (step @p889 :rule process_scope :premises (@p1169) :args (@t574)) % 0.38/0.88 (step @p891 :rule implies_elim :premises (@p889)) % 0.38/0.88 (assume-push @p1170 @t15) % 0.38/0.88 (step @p893 :rule instantiate :premises (@p11) :args (@t226)) % 0.38/0.88 (step-pop @p1171 :rule scope :premises (@p893)) % 0.38/0.88 (step @p894 :rule process_scope :premises (@p1171) :args (@t620)) % 0.38/0.88 (step @p896 :rule implies_elim :premises (@p894)) % 0.38/0.88 (step @p897 :rule cnf_or_pos :args (@t620)) % 0.38/0.88 (step @p898 :rule reordering :premises (@p897) :args ((or @t172 @t224 @t509 (not @t620)))) % 0.38/0.88 (assume-push @p1172 @t28) % 0.38/0.88 (step-pop @p1173 :rule scope :premises (@p805)) % 0.38/0.88 (step @p900 :rule process_scope :premises (@p1173) :args (@t599)) % 0.38/0.88 (step @p902 :rule implies_elim :premises (@p900)) % 0.38/0.88 (assume-push @p1174 @t58) % 0.38/0.88 (step-pop @p1175 :rule scope :premises (@p481)) % 0.38/0.88 (step @p904 :rule process_scope :premises (@p1175) :args (@t484)) % 0.38/0.88 (step @p906 :rule implies_elim :premises (@p904)) % 0.38/0.88 (assume-push @p1176 @t27) % 0.38/0.88 (step-pop @p1177 :rule scope :premises (@p365)) % 0.38/0.88 (step @p908 :rule process_scope :premises (@p1177) :args (@t395)) % 0.38/0.88 (step @p910 :rule implies_elim :premises (@p908)) % 0.38/0.88 (assume-push @p1178 @t126) % 0.38/0.88 (step-pop @p1179 :rule scope :premises (@p811)) % 0.38/0.88 (step @p912 :rule process_scope :premises (@p1179) :args (@t601)) % 0.38/0.88 (step @p914 :rule implies_elim :premises (@p912)) % 0.38/0.88 (assume-push @p1180 @t119) % 0.38/0.88 (step @p916 :rule instantiate :premises (@p90) :args (@t559)) % 0.38/0.88 (step-pop @p1181 :rule scope :premises (@p916)) % 0.38/0.88 (step @p917 :rule process_scope :premises (@p1181) :args (@t621)) % 0.38/0.88 (step @p919 :rule implies_elim :premises (@p917)) % 0.38/0.88 (step @p920 :rule cnf_or_pos :args (@t621)) % 0.38/0.88 (step @p921 :rule factoring :premises (@p920)) % 0.38/0.88 (step @p922 :rule reordering :premises (@p921) :args ((or @t193 @t175 @t353 @t223 @t497 @t560 (not @t621)))) % 0.38/0.88 (step @p923 :rule instantiate :premises (@p92) :args (@t281)) % 0.38/0.88 (step @p924 :rule cnf_or_pos :args (@t622)) % 0.38/0.88 (step @p925 :rule reordering :premises (@p924) :args ((or @t186 @t179 @t286 (not @t622)))) % 0.38/0.88 (step @p926 :rule chain_m_resolution :premises (@p800 @p798 @p62 @p517 @p316 @p314 @p310 @p57 @p528 @p526 @p522 @p59 @p779 @p777 @p776 @p88 @p64 @p61 @p58 @p57 @p500 @p498 @p75) :args ((or @t193 @t331 @t342 @t500 @t519 @t398 @t491 @t313 @t240) (@list false false false false true false false false true false false true false true false false false false false true false false) (@list @t595 @t80 @t173 @t339 @t346 @t349 @t75 @t502 @t516 @t520 @t77 @t167 @t583 @t579 @t105 @t82 @t79 @t76 @t75 @t181 @t499 @t93))) % 0.38/0.88 (step @p647 :rule instantiate :premises (@p37) :args (@t408)) % 0.38/0.88 (step @p927 :rule instantiate :premises (@p36) :args (@t408)) % 0.38/0.88 (step @p928 :rule cnf_or_pos :args (@t623)) % 0.38/0.88 (step @p929 :rule reordering :premises (@p928) :args ((or @t187 @t413 @t410 (not @t623)))) % 0.38/0.88 (step @p930 :rule instantiate :premises (@p38) :args (@t408)) % 0.38/0.88 (step @p931 :rule cnf_or_pos :args (@t624)) % 0.38/0.88 (step @p932 :rule reordering :premises (@p931) :args ((or @t187 @t413 @t419 (not @t624)))) % 0.38/0.88 (step @p933 :rule instantiate :premises (@p92) :args (@t375)) % 0.38/0.88 (step @p934 :rule cnf_or_pos :args (@t625)) % 0.38/0.88 (step @p935 :rule reordering :premises (@p934) :args ((or @t353 @t524 @t409 (not @t625)))) % 0.38/0.88 (step @p936 :rule instantiate :premises (@p31) :args ((@list tptp.masserati))) % 0.38/0.88 (step @p937 :rule cnf_or_pos :args (@t627)) % 0.38/0.88 (step @p938 :rule reordering :premises (@p937) :args ((or @t184 @t626 @t503 (not @t627)))) % 0.38/0.88 (step @p939 :rule instantiate :premises (@p96) :args ((@list tptp.house_1 tptp.house_4 tptp.norwegian tptp.ukranian))) % 0.38/0.88 (step @p940 :rule cnf_or_pos :args (@t628)) % 0.38/0.88 (step @p941 :rule reordering :premises (@p940) :args ((or @t191 @t184 @t175 @t353 @t400 @t223 @t276 @t506 @t579 (not @t628)))) % 0.38/0.88 (step @p942 :rule chain_m_resolution :premises (@p316 @p314 @p310 @p57 @p128 @p155 @p95 @p94 @p88 @p87 @p800 @p798 @p62 @p516 @p514 @p510 @p59 @p941 @p939 @p776 @p88 @p64 @p61 @p59 @p58 @p528 @p526 @p522 @p59 @p435 @p433 @p429 @p59 @p938 @p936 @p73 @p441 @p439 @p82 @p554 @p552 @p548 @p58 @p424 @p422 @p418 @p60 @p935 @p933 @p58 @p491 @p489 @p382 @p378 @p57 @p932 @p930 @p83 @p929 @p927 @p83 @p652 @p647 @p83 @p926 @p925 @p923 @p56 @p534 @p532 @p74 @p763 @p465 @p733 @p43 @p922 @p61 @p88 @p726 @p107 @p723 @p102 @p919 @p90 @p813 @p58 @p914 @p367 @p910 @p17 @p483 @p85 @p906 @p42 @p374 @p59 @p631 @p93 @p807 @p902 @p18 @p898 @p896 @p11 @p766 @p891 @p4 @p341 @p56 @p370 @p887 @p13 @p883 @p363 @p879 @p14 @p338 @p875 @p15 @p871 @p80 @p869 @p16 @p820 @p804 @p60 @p864 @p99 @p769 @p63 @p860 @p5 @p856 @p12 @p810 @p77 @p852 @p19 @p817 @p76 @p94 @p848 @p22 @p563 @p78 @p844 @p21 @p840 @p65 @p838 @p8) :args ((or @t202 @t195 @t193 @t179 @t172 @t170 @t166 @t162 @t160 @t158 @t331 @t438 @t313 @t240) (@list true false false true false false false false false true false false false true false false true false true false false false false false false true false false false true false false true false false true false false false true false false false true false false true false false false true true false false true false false true false false true false false true false false false true false false true true false false true false false true true false false false false true false false true false false true false false false true false false false true false false true false false true false false false false true false false false true false false true false false true false false false false true false false false true false false false false false true false false false true false false false false true false false false true false false false) (@list @t346 @t349 @t75 @t167 @t163 @t128 @t127 @t105 @t104 @t339 @t595 @t80 @t173 @t511 @t514 @t77 @t505 @t628 @t579 @t105 @t82 @t79 @t77 @t76 @t181 @t516 @t520 @t77 @t190 @t459 @t463 @t77 @t502 @t627 @t91 @t462 @t466 @t99 @t183 @t539 @t542 @t76 @t188 @t449 @t453 @t78 @t523 @t625 @t76 @t176 @t485 @t404 @t489 @t75 @t418 @t624 @t100 @t409 @t623 @t100 @t415 @t552 @t100 @t488 @t186 @t622 @t74 @t519 @t527 @t92 @t333 @t429 @t479 @t59 @t496 @t79 @t105 @t560 @t142 @t564 @t139 @t621 @t119 @t533 @t76 @t601 @t365 @t395 @t27 @t423 @t102 @t484 @t58 @t398 @t77 @t401 @t126 @t359 @t599 @t28 @t508 @t620 @t15 @t500 @t574 @t11 @t196 @t74 @t361 @t396 @t20 @t374 @t373 @t394 @t22 @t369 @t372 @t24 @t355 @t97 @t619 @t26 @t198 @t596 @t78 @t598 @t131 @t575 @t81 @t577 @t13 @t605 @t16 @t544 @t95 @t600 @t29 @t602 @t94 @t127 @t604 @t31 @t547 @t96 @t549 @t30 @t342 @t83 @t616 @t14))) % 0.38/0.88 (step @p943 :rule instantiate :premises (@p26) :args (@t490)) % 0.38/0.88 (step @p944 :rule cnf_or_pos :args (@t629)) % 0.38/0.88 (step @p945 :rule reordering :premises (@p944) :args ((or @t182 @t494 @t493 (not @t629)))) % 0.38/0.88 (step @p946 :rule instantiate :premises (@p102) :args (@t301)) % 0.38/0.88 (step @p947 :rule cnf_or_pos :args (@t632)) % 0.38/0.88 (step @p948 :rule reordering :premises (@p947) :args ((or @t143 @t149 @t631 (not @t632)))) % 0.38/0.88 (step @p949 :rule chain_m_resolution :premises (@p948 @p109 @p116 @p946) :args (@t631 @t582 (@list @t143 @t149 @t632))) % 0.38/0.88 (step @p950 :rule instantiate :premises (@p96) :args ((@list tptp.house_1 tptp.house_3 tptp.norwegian tptp.english))) % 0.38/0.88 (step @p951 :rule cnf_or_pos :args (@t633)) % 0.38/0.88 (step @p952 :rule reordering :premises (@p951) :args ((or @t184 @t175 @t170 @t286 @t353 @t223 @t205 @t469 @t630 (not @t633)))) % 0.38/0.88 (step @p633 :rule instantiate :premises (@p92) :args (@t397)) % 0.38/0.88 (step @p640 :rule instantiate :premises (@p44) :args (@t408)) % 0.38/0.88 (step @p953 :rule chain_m_resolution :premises (@p479 @p477 @p82 @p455 @p453 @p449 @p56 @p424 @p422 @p418 @p60 @p652 @p647 @p83 @p645 @p640 @p83 @p638 @p633 @p59 @p528 @p526 @p522 @p59 @p938 @p936 @p73 @p952 @p950 @p949 @p88 @p63 @p61 @p58 @p56) :args ((or @t184 @t181 @t170 @t398 @t425 @t438 @t429) (@list false false false true false false false true false false true false false true false false false false false false true false false true false false true false true false false false false false) (@list @t483 @t99 @t474 @t471 @t475 @t74 @t188 @t449 @t453 @t78 @t186 @t552 @t100 @t418 @t551 @t100 @t415 @t550 @t77 @t519 @t516 @t520 @t77 @t502 @t627 @t91 @t468 @t633 @t630 @t105 @t81 @t79 @t76 @t74))) % 0.38/0.88 (step @p954 :rule instantiate :premises (@p31) :args (@t490)) % 0.38/0.88 (step @p955 :rule cnf_or_pos :args (@t634)) % 0.38/0.88 (step @p956 :rule reordering :premises (@p955) :args ((or @t182 @t494 @t497 (not @t634)))) % 0.38/0.88 (step @p957 :rule chain_m_resolution :premises (@p929 @p927 @p83 @p925 @p923 @p56 @p935 @p933 @p58 @p541 @p539 @p535 @p56 @p554 @p552 @p548 @p58 @p945 @p943 @p75 @p956 @p954 @p75) :args ((or @t183 @t182 @t310 @t531 @t533) (@list false false false false false false false false false true false false false true false false true false false true false false) (@list @t623 @t100 @t186 @t622 @t74 @t409 @t625 @t76 @t178 @t528 @t532 @t74 @t523 @t539 @t542 @t76 @t492 @t629 @t93 @t496 @t634 @t93))) % 0.38/0.88 (step @p958 :rule instantiate :premises (@p25) :args (@t490)) % 0.38/0.88 (step @p959 :rule cnf_or_pos :args (@t635)) % 0.38/0.88 (step @p960 :rule reordering :premises (@p959) :args ((or @t494 @t493 @t497 (not @t635)))) % 0.38/0.88 (step @p961 :rule chain_m_resolution :premises (@p960 @p958 @p75 @p541 @p539 @p535 @p56 @p554 @p552 @p548 @p58 @p534 @p532 @p74 @p531 @p529 @p74 @p528 @p526 @p522 @p59 @p957 @p547 @p545 @p56 @p374 @p372 @p59 @p370 @p368 @p77 @p807 @p805 @p77) :args ((or @t195 @t183 @t310 @t533 @t502) (@list false false false true false false false true false false true false false true false false false true false false true true false false true false false true false false true false false) (@list @t635 @t93 @t492 @t528 @t532 @t74 @t496 @t539 @t542 @t76 @t178 @t527 @t92 @t523 @t526 @t92 @t519 @t516 @t520 @t77 @t181 @t531 @t538 @t74 @t398 @t401 @t77 @t361 @t396 @t95 @t359 @t599 @t95))) % 0.38/0.88 (step @p962 :rule chain_m_resolution :premises (@p520 @p518 @p62 @p59 @p517 @p961 @p953 @p945 @p943 @p75 @p541 @p539 @p535 @p56 @p942 @p833 @p831 @p827 @p60 @p826 @p824 @p64 @p60 @p823 @p821 @p62 @p60 @p820 @p818 @p814 @p60 @p563 @p561 @p78 @p547 @p545 @p56 @p374 @p372 @p59 @p360 @p358 @p354 @p353 @p58 @p813 @p811 @p58 @p810 @p808 @p77 @p370 @p368 @p77 @p807 @p805 @p77 @p367 @p365 @p77 @p804 @p802 @p60 @p801 @p772 @p770 @p63 @p56 @p769 @p767 @p63 @p766 @p764 @p63 @p160 @p158 @p146 @p65 @p763 @p230 @p228 @p68 @p211 @p209 @p205 @p56 @p762 @p760 @p114 @p64 @p62 @p759 @p757 @p69 @p222 @p220 @p216 @p61 @p277 @p198 @p196 @p62 @p270 @p268 @p264 @p64 @p201 @p199 @p64 @p139 @p137 @p66 @p756 @p754 @p66 @p753 @p129 @p66 @p223 @p751 @p158 @p204 @p202 @p65 @p325 @p58 @p61 @p88 @p599 @p97 @p404 @p737 @p36 @p465 @p85 @p733 @p43) :args ((or @t193 @t331 @t438 @t243 @t218 @t313 @t208 @t240) (@list false false false false false true true false false false true false false true false true false false true false false false true false false false false true false false true false false true false false true false false false true false true false true false false true false false true false false true false false true false false true false false false true false false false true false false true false false false true false false true true false false false true false false true false true false false true false false false true false false true true false false false true false false true false false true false false true false false true false false false true true true false false true false false false false false true false false true false false false) (@list @t515 @t80 @t77 @t173 @t502 @t183 @t181 @t629 @t93 @t492 @t528 @t532 @t74 @t178 @t171 @t612 @t615 @t78 @t609 @t611 @t82 @t78 @t606 @t608 @t80 @t78 @t198 @t602 @t605 @t78 @t547 @t549 @t96 @t531 @t538 @t74 @t398 @t401 @t77 @t201 @t387 @t390 @t383 @t76 @t533 @t601 @t76 @t544 @t600 @t95 @t361 @t396 @t95 @t359 @t599 @t95 @t365 @t395 @t95 @t596 @t598 @t78 @t194 @t310 @t578 @t81 @t74 @t575 @t577 @t81 @t500 @t574 @t81 @t157 @t235 @t241 @t83 @t333 @t296 @t299 @t86 @t169 @t283 @t287 @t74 @t327 @t573 @t147 @t82 @t80 @t216 @t572 @t87 @t165 @t291 @t294 @t79 @t258 @t270 @t272 @t80 @t159 @t316 @t320 @t82 @t274 @t277 @t82 @t210 @t214 @t84 @t263 @t571 @t84 @t266 @t570 @t84 @t161 @t319 @t235 @t278 @t280 @t83 @t351 @t76 @t79 @t105 @t354 @t130 @t425 @t432 @t54 @t429 @t102 @t479 @t59))) % 0.38/0.88 (step @p963 :rule instantiate :premises (@p54) :args (@t203)) % 0.38/0.88 (step @p964 :rule cnf_or_pos :args (@t636)) % 0.38/0.88 (step @p965 :rule reordering :premises (@p964) :args ((or @t162 @t212 @t209 (not @t636)))) % 0.38/0.88 (step @p966 :rule instantiate :premises (@p2) :args (@t226)) % 0.38/0.88 (step @p967 :rule cnf_or_pos :args (@t637)) % 0.38/0.88 (step @p968 :rule reordering :premises (@p967) :args ((or @t224 @t279 @t343 (not @t637)))) % 0.38/0.88 (step @p969 :rule instantiate :premises (@p13) :args (@t391)) % 0.38/0.88 (step @p970 :rule cnf_or_pos :args (@t638)) % 0.38/0.88 (step @p971 :rule reordering :premises (@p970) :args ((or @t393 @t392 @t593 (not @t638)))) % 0.38/0.88 (step @p972 :rule chain_m_resolution :premises (@p331 @p329 @p77 @p341 @p339 @p335 @p56 @p374 @p372 @p59 @p971 @p969 @p78 @p528 @p526 @p522 @p59 @p793 @p791 @p787 @p57 @p534 @p532 @p74 @p503 @p501 @p63 @p59 @p786 @p784 @p62 @p57 @p797 @p801 @p293 @p316 @p314 @p310 @p57 @p779 @p777 @p776 @p88 @p64 @p61 @p58 @p57 @p500 @p498 @p75 @p491 @p489 @p382 @p378 @p57 @p377 @p375 @p57 @p371 @p328 @p326 @p65 @p56 @p286 @p260 @p258 @p65 @p56 @p968 @p966 @p65 @p254 @p247 @p245 @p56 @p215 @p213 @p68 @p321 @p132 @p130 @p63 @p222 @p220 @p216 @p61 @p965 @p963 @p66 @p136 @p134 @p66 @p962 @p325 @p58 @p61 @p88 @p599 @p97 @p744 @p57 @p742 @p99) :args ((or @t193 @t331 @t438 @t243 @t218 @t313 @t240) (@list false false false true false false false false false true false false false true false false false true false false true false false true false false false true false false false false false true false true false false true false true false false false false false true false false false true true false false true false false true true false false false true true false false false true false false false true false false true false false true true false false false true false false true false false true false false false true false false false false false true false false false) (@list @t364 @t95 @t361 @t369 @t374 @t74 @t359 @t401 @t77 @t373 @t638 @t96 @t398 @t516 @t520 @t77 @t591 @t588 @t592 @t75 @t519 @t527 @t92 @t502 @t504 @t81 @t77 @t585 @t587 @t80 @t75 @t178 @t500 @t327 @t339 @t346 @t349 @t75 @t167 @t583 @t579 @t105 @t82 @t79 @t76 @t75 @t181 @t499 @t93 @t488 @t485 @t404 @t489 @t75 @t176 @t402 @t75 @t194 @t355 @t357 @t83 @t74 @t157 @t310 @t312 @t83 @t74 @t342 @t637 @t83 @t278 @t196 @t305 @t74 @t258 @t290 @t86 @t333 @t169 @t206 @t81 @t165 @t291 @t294 @t79 @t161 @t636 @t84 @t210 @t213 @t84 @t208 @t351 @t76 @t79 @t105 @t354 @t130 @t565 @t75 @t567 @t131))) % 0.38/0.88 (step @p973 :rule instantiate :premises (@p7) :args (@t204)) % 0.38/0.88 (step @p974 :rule cnf_or_pos :args (@t639)) % 0.38/0.88 (step @p975 :rule reordering :premises (@p974) :args ((or @t205 @t332 @t501 (not @t639)))) % 0.38/0.88 (step @p976 :rule instantiate :premises (@p8) :args (@t204)) % 0.38/0.88 (step @p977 :rule cnf_or_pos :args (@t640)) % 0.38/0.88 (step @p978 :rule reordering :premises (@p977) :args ((or @t205 @t332 @t576 (not @t640)))) % 0.38/0.88 (assume-push @p1182 @t11) % 0.38/0.88 (step @p980 :rule instantiate :premises (@p4) :args (@t226)) % 0.38/0.88 (step-pop @p1183 :rule scope :premises (@p980)) % 0.38/0.88 (step @p981 :rule process_scope :premises (@p1183) :args (@t641)) % 0.38/0.88 (step @p983 :rule implies_elim :premises (@p981)) % 0.38/0.88 (step @p984 :rule cnf_or_pos :args (@t641)) % 0.38/0.88 (step @p985 :rule reordering :premises (@p984) :args ((or @t224 @t279 @t509 (not @t641)))) % 0.38/0.88 (assume-push @p1184 @t13) % 0.38/0.88 (step-pop @p1185 :rule scope :premises (@p255)) % 0.38/0.88 (step @p987 :rule process_scope :premises (@p1185) :args (@t308)) % 0.38/0.88 (step @p989 :rule implies_elim :premises (@p987)) % 0.38/0.88 (step @p990 :rule instantiate :premises (@p11) :args (@t273)) % 0.38/0.88 (step @p991 :rule cnf_or_pos :args (@t642)) % 0.38/0.88 (step @p992 :rule reordering :premises (@p991) :args ((or @t276 @t506 @t610 (not @t642)))) % 0.38/0.88 (step @p993 :rule chain_m_resolution :premises (@p531 @p529 @p74 @p528 @p526 @p522 @p59 @p554 @p552 @p548 @p58 @p500 @p498 @p75 @p497 @p495 @p75) :args ((or @t183 @t533 @t502 @t398 @t491) @t458 (@list @t526 @t92 @t519 @t516 @t520 @t77 @t523 @t539 @t542 @t76 @t181 @t499 @t93 @t496 @t498 @t93))) % 0.38/0.88 (step @p694 :rule instantiate :premises (@p96) :args (@t553)) % 0.38/0.88 (step @p994 :rule chain_m_resolution :premises (@p479 @p477 @p82 @p455 @p453 @p449 @p56 @p424 @p422 @p418 @p60 @p652 @p647 @p83 @p645 @p640 @p83 @p706 @p694 @p780 @p88 @p65 @p61 @p58 @p56 @p638 @p633 @p59 @p993 @p528 @p526 @p522 @p59 @p520 @p518 @p62 @p59 @p516 @p514 @p510 @p59 @p992 @p990 @p64 @p833 @p831 @p827 @p60 @p823 @p821 @p62 @p60 @p820 @p818 @p814 @p60 @p813 @p811 @p58 @p560 @p558 @p77 @p557 @p555 @p77 @p341 @p339 @p335 @p56 @p363 @p361 @p78 @p563 @p561 @p78 @p804 @p60 @p864 @p99 @p257 @p989 @p5 @p985 @p65 @p983 @p4 @p500 @p75 @p619 @p29) :args ((or @t202 @t196 @t500 @t575 @t279 @t355 @t398 @t491 @t425 @t438 @t429 @t296 @t327) (@list false false false true false false false true false false true false false true false false true false true false false false false false false false false false false true false false true false false false false true false false true false false false true false false true false false false false true false false true false false true false false true false false false true false false true false false true false false true false false false true false false true false false false true false false false) (@list @t483 @t99 @t474 @t471 @t475 @t74 @t188 @t449 @t453 @t78 @t186 @t552 @t100 @t418 @t551 @t100 @t468 @t555 @t554 @t105 @t83 @t79 @t76 @t74 @t415 @t550 @t77 @t183 @t519 @t516 @t520 @t77 @t502 @t515 @t80 @t77 @t173 @t511 @t514 @t77 @t505 @t642 @t82 @t609 @t612 @t615 @t78 @t606 @t608 @t80 @t78 @t198 @t602 @t605 @t78 @t533 @t601 @t76 @t544 @t546 @t95 @t365 @t543 @t95 @t361 @t369 @t374 @t74 @t373 @t394 @t96 @t547 @t549 @t96 @t596 @t78 @t598 @t131 @t171 @t308 @t13 @t508 @t83 @t641 @t11 @t181 @t93 @t499 @t45))) % 0.38/0.88 (step @p995 :rule instantiate :premises (@p90) :args (@t553)) % 0.38/0.88 (step @p996 :rule cnf_or_pos :args (@t643)) % 0.38/0.88 (step @p997 :rule reordering :premises (@p996) :args ((or @t193 @t175 @t286 @t353 @t223 @t224 @t279 @t493 @t554 (not @t643)))) % 0.38/0.88 (step @p998 :rule chain_m_resolution :premises (@p541 @p539 @p535 @p56 @p997 @p995 @p780 @p88 @p65 @p61 @p58 @p56 @p260 @p258 @p65 @p56) :args ((or @t193 @t178 @t279 @t531 @t240) (@list true false false true false true false false false false false true false false false) (@list @t528 @t532 @t74 @t492 @t643 @t554 @t105 @t83 @t79 @t76 @t74 @t310 @t312 @t83 @t74))) % 0.38/0.88 (step @p999 :rule chain_m_resolution :premises (@p520 @p518 @p62 @p59 @p517 @p528 @p526 @p522 @p59 @p534 @p532 @p74 @p998 @p547 @p545 @p56 @p557 @p555 @p77 @p360 @p358 @p354 @p353 @p58 @p994 @p374 @p372 @p59 @p364 @p500 @p498 @p75 @p491 @p489 @p382 @p378 @p57 @p978 @p976 @p63 @p975 @p973 @p63 @p377 @p375 @p57 @p972 @p371 @p320 @p318 @p68 @p328 @p326 @p65 @p56 @p325 @p323 @p88 @p61 @p58 @p222 @p220 @p216 @p61 @p322 @p293 @p286 @p285 @p237 @p247 @p56 @p595 @p99 @p404 @p737 @p36 @p465 @p85 @p733 @p43 @p254 @p223 @p132 @p63 @p297 @p86 @p244 @p224) :args ((or @t193 @t161 @t438 @t258 @t240) (@list false false false false false true false false true false false false true false false true false false false true false true false true true false false true true false false false true true false false true false false true false false true false false false true true false false true false false false true false false false false false true false false true true true true true true false false false true false false true false false false false false true false false false true true) (@list @t515 @t80 @t77 @t173 @t502 @t516 @t520 @t77 @t519 @t527 @t92 @t178 @t531 @t538 @t74 @t361 @t543 @t95 @t365 @t387 @t390 @t383 @t76 @t201 @t398 @t401 @t77 @t359 @t181 @t499 @t93 @t488 @t485 @t404 @t489 @t75 @t575 @t640 @t81 @t500 @t639 @t81 @t176 @t402 @t75 @t331 @t194 @t313 @t350 @t86 @t355 @t357 @t83 @t74 @t351 @t354 @t105 @t79 @t76 @t165 @t291 @t294 @t79 @t333 @t327 @t157 @t243 @t218 @t196 @t74 @t305 @t131 @t425 @t432 @t54 @t429 @t102 @t479 @t59 @t278 @t208 @t169 @t81 @t206 @t103 @t296 @t210))) % 0.38/0.88 (step @p1000 :rule chain_m_resolution :premises (@p401 @p399 @p85 @p424 @p422 @p418 @p60 @p455 @p453 @p449 @p56 @p427 @p425 @p82 @p458 @p456 @p82 @p417 @p415 @p411 @p58 @p999 @p729 @p726 @p107 @p723 @p718 @p713 @p711 @p42 @p706 @p704 @p111 @p124 @p702 @p102 @p697 @p96 @p554 @p497 @p692 @p28 @p688 @p551 @p684 @p32 @p531 @p680 @p31 @p544 @p72 @p676 @p25 @p541 @p494 @p672 @p24 @p668 @p538 @p664 @p27 @p260 @p660 @p89 @p534 @p74 @p656 @p26 @p652 @p650 @p37 @p645 @p83 @p643 @p44 @p638 @p636 @p528 @p374 @p59 @p631 @p364 @p627 @p525 @p623 @p33 @p500 @p75 @p619 @p29 @p491 @p322 @p615 @p23 @p381 @p71 @p95 @p611 @p30 @p488 @p607 @p92 @p486 @p377 @p57 @p603 @p93 @p371 @p325 @p58 @p599 @p247 @p595 @p99 @p328 @p56 @p65 @p254 @p132 @p63 @p297 @p86 @p591 @p97 @p286 @p521 @p320 @p68 @p587 @p48 @p222 @p237 @p583 @p45 @p219 @p70 @p154 @p61 @p62 @p88 @p151 @p103 @p579 @p100 @p575 @p91 @p571 @p46 @p285 @p284 @p253 @p66 @p567 @p55 @p223 @p244 @p224) :args ((or @t161 @t438 @t240) (@list false false false true false false false true false false true false false true false false false true false false true true true true false false true false false true true true true false false false false false true false false false true false false true false false true false false false false true false false false true false false true false false true false false false true false false true false false false false false false true false false true false true false false true false false false false true false false true false false false false true false false true true false false false true true false false true false false true false false false true false false false false false true true true false false false false true false false true false false false false false false false false false false false false false true true true false false false false true true) (@list @t431 @t102 @t429 @t449 @t453 @t78 @t425 @t471 @t475 @t74 @t188 @t457 @t99 @t474 @t477 @t99 @t446 @t442 @t447 @t76 @t192 @t434 @t560 @t142 @t564 @t561 @t409 @t558 @t58 @t468 @t554 @t145 @t154 @t557 @t139 @t555 @t129 @t183 @t496 @t498 @t44 @t542 @t539 @t541 @t48 @t523 @t526 @t47 @t533 @t90 @t537 @t39 @t531 @t492 @t495 @t37 @t532 @t528 @t530 @t43 @t310 @t312 @t106 @t178 @t92 @t527 @t41 @t186 @t552 @t56 @t418 @t100 @t551 @t60 @t415 @t550 @t519 @t398 @t77 @t401 @t359 @t520 @t516 @t518 @t49 @t181 @t93 @t499 @t45 @t488 @t333 @t489 @t33 @t404 @t89 @t128 @t407 @t46 @t485 @t487 @t125 @t411 @t176 @t75 @t402 @t126 @t194 @t351 @t76 @t354 @t196 @t305 @t131 @t355 @t74 @t83 @t278 @t169 @t81 @t206 @t103 @t357 @t130 @t157 @t502 @t313 @t86 @t350 @t71 @t165 @t218 @t294 @t64 @t291 @t88 @t163 @t79 @t80 @t105 @t229 @t140 @t230 @t137 @t234 @t121 @t293 @t68 @t243 @t258 @t266 @t84 @t307 @t73 @t208 @t296 @t210))) % 0.38/0.88 (step @p1001 :rule instantiate :premises (@p96) :args ((@list tptp.house_1 tptp.house_4 tptp.norwegian tptp.japanese))) % 0.38/0.88 (step @p1002 :rule cnf_or_pos :args (@t644)) % 0.38/0.88 (step @p1003 :rule reordering :premises (@p1002) :args ((or @t184 @t175 @t353 @t452 @t223 @t276 @t610 @t439 @t579 (not @t644)))) % 0.38/0.88 (step @p1004 :rule instantiate :premises (@p96) :args ((@list tptp.house_1 tptp.house_3 tptp.norwegian tptp.japanese))) % 0.38/0.88 (step @p1005 :rule cnf_or_pos :args (@t645)) % 0.38/0.88 (step @p1006 :rule reordering :premises (@p1005) :args ((or @t184 @t175 @t353 @t452 @t223 @t205 @t576 @t439 @t630 (not @t645)))) % 0.38/0.88 (step @p1007 :rule chain_m_resolution :premises (@p820 @p818 @p814 @p60 @p823 @p821 @p62 @p60 @p804 @p802 @p60 @p833 @p831 @p827 @p60 @p1006 @p1004 @p949 @p88 @p63 @p61 @p60 @p58 @p1003 @p1001 @p776 @p88 @p64 @p61 @p60 @p58 @p1000 @p563 @p561 @p78 @p360 @p358 @p354 @p353 @p58 @p560 @p558 @p77 @p557 @p555 @p77 @p554 @p552 @p548 @p58 @p547 @p545 @p56 @p544 @p542 @p72 @p541 @p539 @p535 @p56 @p534 @p532 @p74 @p531 @p529 @p74 @p528 @p526 @p522 @p59 @p521 @p500 @p498 @p75 @p497 @p495 @p75 @p494 @p492 @p75 @p491 @p489 @p382 @p378 @p57 @p377 @p375 @p57 @p374 @p372 @p59 @p371 @p320 @p318 @p68 @p364 @p328 @p326 @p65 @p56 @p222 @p220 @p216 @p61 @p325 @p323 @p88 @p61 @p58 @p322 @p293 @p286 @p285 @p237 @p284 @p260 @p258 @p65 @p56 @p257 @p255 @p65 @p253 @p251 @p66 @p254 @p247 @p245 @p56 @p244 @p223 @p132 @p130 @p63 @p224) :args ((or @t161 @t240) (@list true false false true false false false true false false false true false false true false true false false false false false true false true false false false false false false true false false false true false true false true false false true false false false true false false false false false true false false false true false false true false false true false false false true false false true true false false true false false true false false false true true false false true false false true false false true true false false true true false false false false true false false true false false false false true true true true true true true false false false true false false true false false false true false false true false true false false true) (@list @t602 @t605 @t78 @t198 @t608 @t80 @t78 @t596 @t598 @t78 @t606 @t612 @t615 @t78 @t575 @t645 @t630 @t105 @t81 @t79 @t78 @t76 @t609 @t644 @t579 @t105 @t82 @t79 @t78 @t76 @t438 @t547 @t549 @t96 @t201 @t387 @t390 @t383 @t76 @t544 @t546 @t95 @t365 @t543 @t95 @t183 @t539 @t542 @t76 @t361 @t538 @t74 @t533 @t537 @t90 @t531 @t528 @t532 @t74 @t178 @t527 @t92 @t523 @t526 @t92 @t519 @t516 @t520 @t77 @t502 @t181 @t499 @t93 @t496 @t498 @t93 @t492 @t495 @t93 @t488 @t485 @t404 @t489 @t75 @t176 @t402 @t75 @t398 @t401 @t77 @t194 @t313 @t350 @t86 @t359 @t355 @t357 @t83 @t74 @t165 @t291 @t294 @t79 @t351 @t354 @t105 @t79 @t76 @t333 @t327 @t157 @t243 @t218 @t258 @t310 @t312 @t83 @t74 @t171 @t308 @t83 @t266 @t307 @t84 @t278 @t196 @t305 @t74 @t296 @t208 @t169 @t206 @t81 @t210))) % 0.38/0.88 (step @p1008 :rule instantiate :premises (@p2) :args (@t204)) % 0.38/0.88 (step @p1009 :rule cnf_or_pos :args (@t646)) % 0.38/0.88 (step @p1010 :rule reordering :premises (@p1009) :args ((or @t170 @t205 @t332 (not @t646)))) % 0.38/0.88 (step @p739 :rule instantiate :premises (@p99) :args (@t345)) % 0.38/0.88 (step @p1011 :rule chain_m_resolution :premises (@p534 @p532 @p74 @p528 @p526 @p522 @p59 @p541 @p539 @p535 @p56 @p500 @p498 @p75 @p494 @p492 @p75 @p491 @p489 @p382 @p378 @p57 @p377 @p375 @p57 @p374 @p372 @p59 @p547 @p545 @p56 @p367 @p365 @p77 @p334 @p332 @p77 @p557 @p555 @p77) :args ((or @t366 @t310 @t333 @t502) (@list false false false true false false false true false false true false false true false false false true true false false true false false true false false true false false true false false true false false true false false) (@list @t527 @t92 @t519 @t516 @t520 @t77 @t178 @t528 @t532 @t74 @t181 @t499 @t93 @t492 @t495 @t93 @t488 @t485 @t404 @t489 @t75 @t176 @t402 @t75 @t398 @t401 @t77 @t531 @t538 @t74 @t194 @t395 @t95 @t359 @t367 @t95 @t361 @t543 @t95))) % 0.38/0.88 (step @p1012 :rule instantiate :premises (@p19) :args (@t617)) % 0.38/0.88 (step @p1013 :rule cnf_or_pos :args (@t647)) % 0.38/0.88 (step @p1014 :rule reordering :premises (@p1013) :args ((or @t199 @t618 @t586 (not @t647)))) % 0.38/0.88 (step @p1015 :rule instantiate :premises (@p22) :args (@t358)) % 0.38/0.88 (step @p1016 :rule cnf_or_pos :args (@t648)) % 0.38/0.88 (step @p1017 :rule reordering :premises (@p1016) :args ((or @t363 @t360 @t545 (not @t648)))) % 0.38/0.88 (step @p1018 :rule chain_m_resolution :premises (@p960 @p958 @p75 @p541 @p539 @p535 @p56 @p554 @p552 @p548 @p58 @p534 @p532 @p74 @p531 @p529 @p74 @p528 @p526 @p522 @p59 @p957 @p374 @p372 @p59 @p547 @p545 @p56 @p1017 @p1015 @p77 @p560 @p558 @p77 @p820 @p818 @p814 @p60 @p1014 @p1012 @p80 @p793 @p791 @p787 @p57 @p961 @p563 @p561 @p78 @p796 @p794 @p78 @p360 @p358 @p354 @p58 @p813 @p811 @p58) :args ((or @t183 @t565 @t365 @t351 @t383 @t596 @t310 @t502) (@list false false false true false false false true false false true false false true false false false true false false true true false false true false false true false false true false false false true false false true false false false true false false true true false false true false false false true false false true false false) (@list @t635 @t93 @t492 @t528 @t532 @t74 @t496 @t539 @t542 @t76 @t178 @t527 @t92 @t523 @t526 @t92 @t519 @t516 @t520 @t77 @t181 @t398 @t401 @t77 @t531 @t538 @t74 @t359 @t648 @t95 @t361 @t546 @t95 @t544 @t602 @t605 @t78 @t198 @t647 @t97 @t585 @t588 @t592 @t75 @t194 @t547 @t549 @t96 @t591 @t594 @t96 @t201 @t387 @t390 @t76 @t533 @t601 @t76))) % 0.38/0.88 (step @p1019 :rule instantiate :premises (@p96) :args ((@list tptp.house_1 tptp.house_5 tptp.norwegian tptp.japanese))) % 0.38/0.88 (step @p1020 :rule cnf_or_pos :args (@t649)) % 0.38/0.88 (step @p1021 :rule reordering :premises (@p1020) :args ((or @t184 @t175 @t172 @t353 @t452 @t223 @t224 @t439 @t554 (not @t649)))) % 0.38/0.88 (step @p1022 :rule chain_m_resolution :premises (@p833 @p831 @p827 @p60 @p823 @p821 @p62 @p60 @p1003 @p1001 @p776 @p88 @p64 @p61 @p60 @p58 @p1021 @p1019 @p780 @p88 @p65 @p61 @p60 @p58 @p820 @p818 @p814 @p60 @p1018 @p353 @p810 @p808 @p77 @p367 @p365 @p77 @p804 @p60 @p864 @p99) :args ((or @t195 @t575 @t565 @t351 @t547 @t310 @t502 @t439 @t327) (@list true false false true false false false true false true false false false false false true false true false false false false false false true false false false true true false false true false false true false false false) (@list @t612 @t615 @t78 @t606 @t608 @t80 @t78 @t609 @t644 @t579 @t105 @t82 @t79 @t78 @t76 @t171 @t649 @t554 @t105 @t83 @t79 @t78 @t76 @t198 @t602 @t605 @t78 @t183 @t383 @t544 @t600 @t95 @t365 @t395 @t95 @t596 @t78 @t598 @t131))) % 0.38/0.88 (step @p1023 :rule chain_m_resolution :premises (@p1014 @p1012 @p80 @p820 @p818 @p814 @p60 @p793 @p791 @p787 @p57 @p563 @p561 @p78 @p796 @p794 @p78) :args ((or @t202 @t194 @t565 @t544 @t596) @t458 (@list @t647 @t97 @t198 @t602 @t605 @t78 @t585 @t588 @t592 @t75 @t547 @t549 @t96 @t591 @t594 @t96))) % 0.38/0.88 (step @p1024 :rule chain_m_resolution :premises (@p534 @p532 @p74 @p528 @p526 @p522 @p59 @p541 @p539 @p535 @p56 @p374 @p372 @p59 @p547 @p545 @p56 @p494 @p492 @p75 @p1017 @p1015 @p77 @p560 @p558 @p77 @p491 @p489 @p382 @p378 @p57 @p1023 @p377 @p375 @p57) :args ((or @t202 @t194 @t181 @t565 @t596 @t310 @t333 @t502) (@list false false false true false false false true false false true false false true false false true false false true false false true false false false true true false false false true false false) (@list @t527 @t92 @t519 @t516 @t520 @t77 @t178 @t528 @t532 @t74 @t398 @t401 @t77 @t531 @t538 @t74 @t492 @t495 @t93 @t359 @t648 @t95 @t361 @t546 @t95 @t488 @t485 @t404 @t489 @t75 @t544 @t176 @t402 @t75))) % 0.38/0.88 (step @p1025 :rule chain_m_resolution :premises (@p500 @p498 @p75 @p491 @p489 @p382 @p378 @p57 @p1024 @p377 @p375 @p57 @p1022 @p563 @p561 @p78 @p804 @p60 @p864 @p99) :args ((or @t202 @t575 @t565 @t351 @t310 @t333 @t502 @t439 @t327) (@list false false false true true false false false true false false true true false false true false false false) (@list @t499 @t93 @t488 @t485 @t404 @t489 @t75 @t181 @t176 @t402 @t75 @t194 @t547 @t549 @t96 @t596 @t78 @t598 @t131))) % 0.38/0.88 (step @p720 :rule instantiate :premises (@p102) :args (@t562)) % 0.38/0.88 (step @p1026 :rule chain_m_resolution :premises (@p726 @p107 @p720) :args (@t563 @t650 (@list @t142 @t564))) % 0.38/0.88 (step @p715 :rule instantiate :premises (@p96) :args (@t559)) % 0.38/0.88 (step @p1027 :rule chain_m_resolution :premises (@p500 @p498 @p75 @p491 @p489 @p382 @p378 @p57 @p1024 @p377 @p375 @p57) :args ((or @t202 @t194 @t565 @t596 @t310 @t333 @t502) (@list false false false true true false false false true false false) (@list @t499 @t93 @t488 @t485 @t404 @t489 @t75 @t181 @t176 @t402 @t75))) % 0.38/0.88 (step @p1028 :rule chain_m_resolution :premises (@p370 @p368 @p77 @p547 @p545 @p56 @p377 @p375 @p57 @p541 @p539 @p535 @p56 @p491 @p382 @p378 @p57 @p925 @p923 @p56 @p488 @p383 @p57 @p929 @p927 @p83 @p386 @p384 @p83) :args ((or @t310 @t492 @t333 @t488 @t410) (@list false false false false false false false false false true false false false true false false true false false true false false true false false true false false) (@list @t396 @t95 @t361 @t538 @t74 @t194 @t402 @t75 @t531 @t528 @t532 @t74 @t176 @t404 @t489 @t75 @t178 @t622 @t74 @t485 @t487 @t75 @t186 @t623 @t100 @t411 @t414 @t100))) % 0.38/0.88 (step @p1029 :rule instantiate :premises (@p102) :args ((@list tptp.house_5 tptp.house_2))) % 0.38/0.88 (step @p1030 :rule cnf_or_pos :args (@t653)) % 0.38/0.88 (step @p1031 :rule reordering :premises (@p1030) :args ((or @t148 @t155 @t652 (not @t653)))) % 0.38/0.88 (step @p1032 :rule chain_m_resolution :premises (@p1031 @p115 @p125 @p1029) :args (@t652 @t582 (@list @t148 @t155 @t653))) % 0.38/0.88 (step @p1033 :rule instantiate :premises (@p90) :args ((@list tptp.house_5 tptp.house_2 tptp.japanese tptp.ukranian))) % 0.38/0.88 (step @p1034 :rule cnf_or_pos :args (@t654)) % 0.38/0.88 (step @p1035 :rule reordering :premises (@p1034) :args ((or @t182 @t174 @t172 @t400 @t452 @t233 @t224 @t430 @t651 (not @t654)))) % 0.38/0.88 (step @p1036 :rule chain_m_resolution :premises (@p941 @p939 @p776 @p88 @p64 @p61 @p59 @p58 @p516 @p514 @p510 @p59 @p435 @p433 @p429 @p59 @p1035 @p1033 @p1032 @p65 @p62 @p60 @p59 @p462 @p460 @p85 @p424 @p422 @p418 @p60 @p932 @p930 @p83 @p652 @p647 @p83 @p427 @p425 @p82 @p438 @p436 @p82 @p925 @p923 @p56 @p417 @p415 @p411 @p58 @p541 @p539 @p535 @p56 @p1028 @p945 @p943 @p75 @p500 @p498 @p75 @p729 @p58 @p61 @p88 @p726 @p107 @p723 @p102 @p718 @p96 @p898 @p65 @p896 @p11) :args ((or @t192 @t184 @t182 @t172 @t500 @t310 @t531 @t333 @t438) (@list false true false false false false false false true false false false true false false true false true false false false false true false false false true false false true false false true false false true false false true false false false false false false true false false false true false false true true false false true false false true false false false true true false false false false true false false false) (@list @t628 @t579 @t105 @t82 @t79 @t77 @t76 @t505 @t511 @t514 @t77 @t190 @t459 @t463 @t77 @t173 @t654 @t651 @t83 @t80 @t78 @t77 @t423 @t478 @t102 @t429 @t449 @t453 @t78 @t418 @t624 @t100 @t415 @t552 @t100 @t188 @t457 @t99 @t462 @t465 @t99 @t186 @t622 @t74 @t446 @t442 @t447 @t76 @t178 @t528 @t532 @t74 @t409 @t492 @t629 @t93 @t488 @t499 @t93 @t434 @t76 @t79 @t105 @t560 @t142 @t564 @t139 @t561 @t129 @t508 @t83 @t620 @t15))) % 0.38/0.88 (step @p708 :rule instantiate :premises (@p42) :args (@t408)) % 0.38/0.88 (step @p1037 :rule instantiate :premises (@p102) :args ((@list tptp.house_3 tptp.house_3))) % 0.38/0.88 (step @p1038 :rule cnf_or_pos :args (@t657)) % 0.38/0.88 (step @p1039 :rule factoring :premises (@p1038)) % 0.38/0.88 (step @p1040 :rule reordering :premises (@p1039) :args ((or @t150 @t656 (not @t657)))) % 0.38/0.88 (step @p1041 :rule chain_m_resolution :premises (@p1040 @p117 @p1037) :args (@t656 @t650 (@list @t150 @t657))) % 0.38/0.88 (step @p1042 :rule instantiate :premises (@p90) :args ((@list tptp.house_3 tptp.house_3 tptp.english tptp.english))) % 0.38/0.88 (step @p1043 :rule cnf_or_pos :args (@t658)) % 0.38/0.88 (step @p1044 :rule factoring :premises (@p1043)) % 0.38/0.88 (step @p1045 :rule reordering :premises (@p1044) :args ((or @t170 @t286 @t205 @t493 @t426 @t655 (not @t658)))) % 0.38/0.88 (step @p1046 :rule chain_m_resolution :premises (@p455 @p453 @p449 @p56 @p458 @p456 @p82 @p1045 @p1042 @p1041 @p63 @p56 @p417 @p415 @p411 @p58 @p541 @p539 @p535 @p56 @p652 @p647 @p83 @p713 @p708 @p83 @p534 @p532 @p74 @p638 @p633 @p59 @p528 @p526 @p522 @p59 @p1036 @p833 @p831 @p827 @p60 @p826 @p824 @p64 @p60 @p823 @p821 @p62 @p60 @p820 @p818 @p814 @p60 @p547 @p545 @p56 @p374 @p372 @p59 @p810 @p808 @p77 @p370 @p368 @p77 @p807 @p805 @p77 @p1027 @p962 @p952 @p950 @p949 @p88 @p63 @p61 @p58 @p56 @p729 @p715 @p1026 @p88 @p61 @p58 @p1025 @p563 @p561 @p78 @p1018 @p353 @p360 @p358 @p354 @p353 @p58 @p1011 @p762 @p760 @p114 @p64 @p62 @p270 @p268 @p264 @p64 @p521 @p804 @p802 @p60 @p744 @p739 @p57 @p763 @p320 @p318 @p68 @p230 @p228 @p68 @p772 @p770 @p63 @p56 @p769 @p767 @p63 @p766 @p764 @p63 @p1010 @p1008 @p63 @p222 @p220 @p216 @p61 @p325 @p323 @p88 @p61 @p58 @p211 @p209 @p205 @p56 @p198 @p196 @p62 @p284 @p201 @p199 @p64 @p168 @p161 @p751 @p158 @p204 @p202 @p65 @p756 @p754 @p66 @p753 @p129 @p66 @p965 @p963 @p66 @p1007 @p224) :args (@t240 (@list true false false true false false true false true false false false true false false false true false false true false false true false false true false false false false false false true false false true false true false false true false false false true false false false false true false false true false false true false false true false false true false false true false false false true true false true false false false false false true false true false false false true true false false false true false true false true false true true false true false false false true false false true true false false true false false true true false false true false false true false false false true false false true false false true false false false true false false true false false false false false true false false true false false true true false false true true true true true false false true false false true false false true false false false true) (@list @t471 @t475 @t74 @t474 @t477 @t99 @t425 @t658 @t655 @t81 @t74 @t446 @t442 @t447 @t76 @t492 @t528 @t532 @t74 @t186 @t552 @t100 @t409 @t558 @t100 @t178 @t527 @t92 @t415 @t550 @t77 @t519 @t516 @t520 @t77 @t181 @t171 @t612 @t615 @t78 @t609 @t611 @t82 @t78 @t606 @t608 @t80 @t78 @t198 @t602 @t605 @t78 @t531 @t538 @t74 @t398 @t401 @t77 @t544 @t600 @t95 @t361 @t396 @t95 @t359 @t599 @t95 @t194 @t192 @t468 @t633 @t630 @t105 @t81 @t79 @t76 @t74 @t434 @t561 @t560 @t105 @t79 @t76 @t438 @t547 @t549 @t96 @t183 @t383 @t201 @t387 @t390 @t383 @t76 @t365 @t327 @t573 @t147 @t82 @t80 @t159 @t316 @t320 @t82 @t502 @t596 @t598 @t78 @t565 @t567 @t75 @t333 @t313 @t350 @t86 @t296 @t299 @t86 @t310 @t578 @t81 @t74 @t575 @t577 @t81 @t500 @t574 @t81 @t331 @t646 @t81 @t165 @t291 @t294 @t79 @t351 @t354 @t105 @t79 @t76 @t169 @t283 @t287 @t74 @t270 @t272 @t80 @t258 @t274 @t277 @t82 @t243 @t218 @t319 @t235 @t278 @t280 @t83 @t263 @t571 @t84 @t266 @t570 @t84 @t208 @t636 @t84 @t161 @t210))) % 0.38/0.88 (step @p1047 :rule cnf_or_pos :args (@t660)) % 0.38/0.88 (step @p1048 :rule reordering :premises (@p1047) :args ((or @t289 @t288 @t659 (not @t660)))) % 0.38/0.88 (step @p1049 :rule chain_m_resolution :premises (@p1048 @p68 @p1046 @p133) :args (@t288 @t239 (@list @t86 @t240 @t660))) % 0.38/0.88 (step @p1050 :rule instantiate :premises (@p49) :args (@t207)) % 0.38/0.88 (step @p1051 :rule cnf_or_pos :args (@t661)) % 0.38/0.88 (step @p1052 :rule reordering :premises (@p1051) :args ((or @t166 @t289 @t659 (not @t661)))) % 0.38/0.88 (step @p1053 :rule chain_m_resolution :premises (@p1052 @p68 @p1046 @p1050) :args (@t166 @t239 (@list @t86 @t240 @t661))) % 0.38/0.88 (step @p1054 :rule chain_m_resolution :premises (@p222 @p220 @p1053 @p216 @p61 @p212 @p285 @p1049 @p237 @p1049 @p132 @p130 @p63) :args (@t161 (@list true true false false true true true true true true false false) (@list @t291 @t165 @t294 @t79 @t210 @t243 @t258 @t218 @t258 @t169 @t206 @t81))) % 0.38/0.88 (step @p1055 :rule chain_m_resolution :premises (@p753 @p1054 @p66 @p129) :args (@t267 @t239 (@list @t161 @t84 @t570))) % 0.38/0.88 (step @p1056 :rule instantiate :premises (@p55) :args (@t207)) % 0.38/0.88 (step @p1057 :rule cnf_or_pos :args (@t662)) % 0.38/0.88 (step @p1058 :rule reordering :premises (@p1057) :args ((or @t289 @t314 @t659 (not @t662)))) % 0.38/0.88 (step @p1059 :rule chain_m_resolution :premises (@p1058 @p68 @p1046 @p1056) :args (@t314 @t239 (@list @t86 @t240 @t662))) % 0.38/0.88 (step @p1060 :rule chain_m_resolution :premises (@p270 @p268 @p1059 @p264 @p1055 @p64 @p273 @p271 @p110 @p64 @p61 @p280 @p278 @p67) :args (@t244 (@list true true false true false true false true false false true false false) (@list @t316 @t313 @t320 @t266 @t82 @t159 @t321 @t144 @t82 @t79 @t319 @t324 @t85))) % 0.38/0.88 (step @p1061 :rule chain_m_resolution :premises (@p139 @p1054 @p66 @p137) :args (@t211 @t239 (@list @t161 @t84 @t214))) % 0.38/0.88 (step @p1062 :rule chain_m_resolution :premises (@p222 @p1053 @p61 @p1061 @p220 @p1060 @p216) :args (@t218 (@list true false true true true false) (@list @t165 @t79 @t210 @t291 @t243 @t294))) % 0.38/0.88 (step @p1063 :rule chain_m_resolution :premises (@p283 @p120 @p61 @p64 @p1062 @p281) :args (@t323 (@list true false false false false) (@list @t152 @t79 @t82 @t218 @t326))) % 0.38/0.88 (step @p1064 :rule chain_m_resolution :premises (@p276 @p69 @p1062 @p274) :args (@t160 @t239 (@list @t87 @t218 @t322))) % 0.38/0.88 (step @p1065 false :rule chain_m_resolution :premises (@p270 @p1064 @p1063 @p268 @p1059 @p264 @p1055 @p64) :args (false (@list true true true true false true false) (@list @t159 @t319 @t316 @t313 @t320 @t266 @t82))) % 0.38/0.88 ) % 0.38/0.88 % SZS output end Proof % 0.38/0.88 % cvc5 exiting %------------------------------------------------------------------------------