%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : SYN037-1 : TPTP v9.2.1. Released v1.0.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n027.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jun 3 09:07:50 AM UTC 2026 % Result : Unsatisfiable 0.39s 0.59s % Output : Proof 0.39s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYN037-1 : TPTP v9.2.1. Released v1.0.0. % 0.12/0.14 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.17/0.35 % Computer : n027.cluster.edu % 0.17/0.35 % Model : x86_64 x86_64 % 0.17/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.35 % Memory : 8042.1875MB % 0.17/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.35 % CPULimit : 300 % 0.17/0.35 % WCLimit : 300 % 0.17/0.35 % DateTime : Tue Jun 2 23:18:21 EDT 2026 % 0.17/0.35 % CPUTime : % 0.32/0.51 %----Proving TF0_NAR, FOF, or CNF % 0.32/0.52 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 0.39/0.59 % SZS status Unsatisfiable % 0.39/0.59 % SZS output start Proof % 0.39/0.61 ( % 0.39/0.61 (declare-sort $$unsorted 0) % 0.39/0.61 (declare-const tptp.s3 $$unsorted) % 0.39/0.61 (declare-const tptp.n3 Bool) % 0.39/0.61 (declare-const tptp.s2 $$unsorted) % 0.39/0.61 (declare-const tptp.s4 $$unsorted) % 0.39/0.61 (declare-const tptp.n1 (-> $$unsorted Bool)) % 0.39/0.61 (declare-const tptp.n10 Bool) % 0.39/0.61 (declare-const tptp.n9 Bool) % 0.39/0.61 (declare-const tptp.n2 Bool) % 0.39/0.61 (declare-const tptp.n8 Bool) % 0.39/0.61 (declare-const tptp.s8 $$unsorted) % 0.39/0.61 (declare-const tptp.n5 (-> $$unsorted Bool)) % 0.39/0.61 (declare-const tptp.n4 Bool) % 0.39/0.61 (declare-const tptp.q (-> $$unsorted Bool)) % 0.39/0.61 (declare-const tptp.n7 Bool) % 0.39/0.61 (declare-const tptp.p (-> $$unsorted Bool)) % 0.39/0.61 (declare-const tptp.n6 Bool) % 0.39/0.61 (declare-const tptp.s7 $$unsorted) % 0.39/0.61 (declare-const tptp.s1 (-> $$unsorted $$unsorted)) % 0.39/0.61 (declare-const tptp.s6 $$unsorted) % 0.39/0.61 (declare-const tptp.s5 (-> $$unsorted $$unsorted)) % 0.39/0.61 (define @t1 () (not tptp.n10)) % 0.39/0.61 (define @t2 () (not tptp.n6)) % 0.39/0.61 (define @t3 () (not tptp.n9)) % 0.39/0.61 (define @t4 () (not tptp.n2)) % 0.39/0.61 (define @t5 () (tptp.q tptp.s8)) % 0.39/0.61 (define @t6 () (not @t5)) % 0.39/0.61 (define @t7 () (@var "X10" $$unsorted)) % 0.39/0.61 (define @t8 () (tptp.q @t7)) % 0.39/0.61 (define @t9 () (not tptp.n8)) % 0.39/0.61 (define @t10 () (@list @t7)) % 0.39/0.61 (define @t11 () (forall @t10 (or @t9 @t8))) % 0.39/0.61 (define @t12 () (@var "X9" $$unsorted)) % 0.39/0.61 (define @t13 () (not (tptp.p @t12))) % 0.39/0.61 (define @t14 () (or @t13 tptp.n7)) % 0.39/0.61 (define @t15 () (@list @t12)) % 0.39/0.61 (define @t16 () (forall @t15 @t14)) % 0.39/0.61 (define @t17 () (tptp.p tptp.s7)) % 0.39/0.61 (define @t18 () (not tptp.n7)) % 0.39/0.61 (define @t19 () (@var "X8" $$unsorted)) % 0.39/0.61 (define @t20 () (not (tptp.n5 @t19))) % 0.39/0.61 (define @t21 () (or @t20 tptp.n6)) % 0.39/0.61 (define @t22 () (@list @t19)) % 0.39/0.61 (define @t23 () (forall @t22 @t21)) % 0.39/0.61 (define @t24 () (tptp.n5 tptp.s6)) % 0.39/0.61 (define @t25 () (@var "W" $$unsorted)) % 0.39/0.61 (define @t26 () (tptp.n5 @t25)) % 0.39/0.61 (define @t27 () (tptp.q @t25)) % 0.39/0.61 (define @t28 () (not @t27)) % 0.39/0.61 (define @t29 () (tptp.q (tptp.s5 @t25))) % 0.39/0.61 (define @t30 () (@list @t25)) % 0.39/0.61 (define @t31 () (@var "X7" $$unsorted)) % 0.39/0.61 (define @t32 () (tptp.q @t31)) % 0.39/0.61 (define @t33 () (not @t32)) % 0.39/0.61 (define @t34 () (not @t26)) % 0.39/0.61 (define @t35 () (or @t34 @t33 @t27)) % 0.39/0.61 (define @t36 () (@list @t25 @t31)) % 0.39/0.61 (define @t37 () (forall @t36 @t35)) % 0.39/0.61 (define @t38 () (or @t34 @t32 @t28)) % 0.39/0.61 (define @t39 () (forall @t36 @t38)) % 0.39/0.61 (define @t40 () (tptp.p tptp.s4)) % 0.39/0.61 (define @t41 () (not @t40)) % 0.39/0.61 (define @t42 () (@var "X6" $$unsorted)) % 0.39/0.61 (define @t43 () (tptp.p @t42)) % 0.39/0.61 (define @t44 () (not tptp.n4)) % 0.39/0.61 (define @t45 () (@list @t42)) % 0.39/0.61 (define @t46 () (forall @t45 (or @t44 @t43))) % 0.39/0.61 (define @t47 () (@var "X5" $$unsorted)) % 0.39/0.61 (define @t48 () (not (tptp.q @t47))) % 0.39/0.61 (define @t49 () (or @t48 tptp.n3)) % 0.39/0.61 (define @t50 () (@list @t47)) % 0.39/0.61 (define @t51 () (forall @t50 @t49)) % 0.39/0.61 (define @t52 () (tptp.q tptp.s3)) % 0.39/0.61 (define @t53 () (not tptp.n3)) % 0.39/0.61 (define @t54 () (@var "X4" $$unsorted)) % 0.39/0.61 (define @t55 () (not (tptp.n1 @t54))) % 0.39/0.61 (define @t56 () (or @t55 tptp.n2)) % 0.39/0.61 (define @t57 () (@list @t54)) % 0.39/0.61 (define @t58 () (forall @t57 @t56)) % 0.39/0.61 (define @t59 () (tptp.n1 tptp.s2)) % 0.39/0.61 (define @t60 () (@var "X" $$unsorted)) % 0.39/0.61 (define @t61 () (tptp.n1 @t60)) % 0.39/0.61 (define @t62 () (tptp.p (tptp.s1 @t60))) % 0.39/0.61 (define @t63 () (tptp.p @t60)) % 0.39/0.61 (define @t64 () (not @t63)) % 0.39/0.61 (define @t65 () (@list @t60)) % 0.39/0.61 (define @t66 () (forall @t65 (or @t64 (not @t62) @t61))) % 0.39/0.61 (define @t67 () (@var "X3" $$unsorted)) % 0.39/0.61 (define @t68 () (tptp.p @t67)) % 0.39/0.61 (define @t69 () (not @t61)) % 0.39/0.61 (define @t70 () (or @t69 @t64 @t68)) % 0.39/0.61 (define @t71 () (@list @t60 @t67)) % 0.39/0.61 (define @t72 () (forall @t71 @t70)) % 0.39/0.61 (define @t73 () (not @t68)) % 0.39/0.61 (define @t74 () (or @t69 @t63 @t73)) % 0.39/0.61 (define @t75 () (forall @t71 @t74)) % 0.39/0.61 (define @t76 () (forall @t15 @t13)) % 0.39/0.61 (define @t77 () (or tptp.n7 @t13)) % 0.39/0.61 (define @t78 () (@list @t67)) % 0.39/0.61 (define @t79 () (@list @t67)) % 0.39/0.61 (define @t80 () (forall @t79 @t73)) % 0.39/0.61 (define @t81 () (or @t69 @t63)) % 0.39/0.61 (define @t82 () (forall @t65 @t81)) % 0.39/0.61 (define @t83 () (or @t81 @t73)) % 0.39/0.61 (define @t84 () (forall @t57 @t55)) % 0.39/0.61 (define @t85 () (@quantifiers_skolemize @t84 0)) % 0.39/0.61 (define @t86 () (@list @t85)) % 0.39/0.61 (define @t87 () (tptp.p @t85)) % 0.39/0.61 (define @t88 () (tptp.n1 @t85)) % 0.39/0.61 (define @t89 () (not @t88)) % 0.39/0.61 (define @t90 () (or @t89 @t87)) % 0.39/0.61 (define @t91 () (@list tptp.s2)) % 0.39/0.61 (define @t92 () (not @t84)) % 0.39/0.61 (define @t93 () (not @t89)) % 0.39/0.61 (define @t94 () (not @t90)) % 0.39/0.61 (define @t95 () (not @t87)) % 0.39/0.61 (define @t96 () (or @t89 @t95)) % 0.39/0.61 (define @t97 () (or @t69 @t64)) % 0.39/0.61 (define @t98 () (forall @t65 @t97)) % 0.39/0.61 (define @t99 () (forall @t79 @t68)) % 0.39/0.61 (define @t100 () (or @t97 @t68)) % 0.39/0.61 (define @t101 () (forall @t45 @t43)) % 0.39/0.61 (define @t102 () (not @t101)) % 0.39/0.61 (define @t103 () (forall @t10 @t8)) % 0.39/0.61 (define @t104 () (not @t103)) % 0.39/0.61 (define @t105 () (@list @t31)) % 0.39/0.61 (define @t106 () (@list @t31)) % 0.39/0.61 (define @t107 () (forall @t106 @t32)) % 0.39/0.61 (define @t108 () (or @t34 @t28)) % 0.39/0.61 (define @t109 () (forall @t30 @t108)) % 0.39/0.61 (define @t110 () (or @t108 @t32)) % 0.39/0.61 (define @t111 () (@list tptp.s6)) % 0.39/0.61 (define @t112 () (tptp.q tptp.s6)) % 0.39/0.61 (define @t113 () (not @t112)) % 0.39/0.61 (define @t114 () (not @t24)) % 0.39/0.61 (define @t115 () (or @t114 @t113)) % 0.39/0.61 (define @t116 () (forall @t50 @t48)) % 0.39/0.61 (define @t117 () (or tptp.n3 @t48)) % 0.39/0.61 (define @t118 () (forall @t106 @t33)) % 0.39/0.61 (define @t119 () (or @t34 @t27)) % 0.39/0.61 (define @t120 () (forall @t30 @t119)) % 0.39/0.61 (define @t121 () (@quantifiers_skolemize @t120 0)) % 0.39/0.61 (define @t122 () (@list @t121)) % 0.39/0.61 (define @t123 () (tptp.q @t121)) % 0.39/0.61 (define @t124 () (tptp.s5 @t121)) % 0.39/0.61 (define @t125 () (tptp.q @t124)) % 0.39/0.61 (define @t126 () (forall @t22 @t20)) % 0.39/0.61 (define @t127 () (or tptp.n6 @t20)) % 0.39/0.61 (define @t128 () (tptp.n5 @t121)) % 0.39/0.61 (define @t129 () (or @t125 @t123 @t128)) % 0.39/0.61 (define @t130 () (not @t128)) % 0.39/0.61 (define @t131 () (or @t119 @t33)) % 0.39/0.61 (define @t132 () (or @t114 @t112)) % 0.39/0.61 (define @t133 () (not @t115)) % 0.39/0.61 (define @t134 () (tptp.s5 tptp.s6)) % 0.39/0.61 (define @t135 () (tptp.q @t134)) % 0.39/0.61 (define @t136 () (not @t135)) % 0.39/0.61 (define @t137 () (or @t136 @t113 @t24)) % 0.39/0.61 (define @t138 () (or tptp.n2 @t55)) % 0.39/0.61 (define @t139 () (@quantifiers_skolemize @t98 0)) % 0.39/0.61 (define @t140 () (@list @t139)) % 0.39/0.61 (define @t141 () (tptp.n1 @t139)) % 0.39/0.61 (define @t142 () (not @t141)) % 0.39/0.61 (define @t143 () (tptp.p @t139)) % 0.39/0.61 (define @t144 () (not @t143)) % 0.39/0.61 (define @t145 () (or @t142 @t144)) % 0.39/0.61 (define @t146 () (not @t145)) % 0.39/0.61 (define @t147 () (not @t98)) % 0.39/0.61 (define @t148 () (@list tptp.s7)) % 0.39/0.61 (define @t149 () (not @t17)) % 0.39/0.61 (define @t150 () (tptp.n1 tptp.s7)) % 0.39/0.61 (define @t151 () (not @t150)) % 0.39/0.61 (define @t152 () (or @t151 @t149)) % 0.39/0.61 (define @t153 () (tptp.s1 tptp.s7)) % 0.39/0.61 (define @t154 () (tptp.p @t153)) % 0.39/0.61 (define @t155 () (not @t154)) % 0.39/0.61 (define @t156 () (or @t149 @t155 @t150)) % 0.39/0.61 (define @t157 () (tptp.p tptp.s2)) % 0.39/0.61 (define @t158 () (tptp.s1 tptp.s2)) % 0.39/0.61 (define @t159 () (tptp.p @t158)) % 0.39/0.61 (define @t160 () (or @t157 @t159 @t59)) % 0.39/0.61 (define @t161 () (not @t76)) % 0.39/0.61 (define @t162 () (@quantifiers_skolemize @t76 0)) % 0.39/0.61 (define @t163 () (@list @t162)) % 0.39/0.61 (define @t164 () (tptp.p @t162)) % 0.39/0.61 (define @t165 () (not @t164)) % 0.39/0.61 (define @t166 () (tptp.n1 @t162)) % 0.39/0.61 (define @t167 () (not @t166)) % 0.39/0.61 (define @t168 () (or @t167 @t165)) % 0.39/0.61 (define @t169 () (not @t165)) % 0.39/0.61 (define @t170 () (tptp.s1 @t162)) % 0.39/0.61 (define @t171 () (tptp.p @t170)) % 0.39/0.61 (define @t172 () (not @t171)) % 0.39/0.61 (define @t173 () (or @t165 @t172 @t166)) % 0.39/0.61 (define @t174 () (or @t130 @t123)) % 0.39/0.61 (define @t175 () (not @t174)) % 0.39/0.61 (define @t176 () (not @t120)) % 0.39/0.61 (define @t177 () (@quantifiers_skolemize @t103 0)) % 0.39/0.61 (define @t178 () (@list @t177)) % 0.39/0.61 (define @t179 () (tptp.q @t177)) % 0.39/0.61 (define @t180 () (tptp.n5 @t177)) % 0.39/0.61 (define @t181 () (not @t180)) % 0.39/0.61 (define @t182 () (or @t181 @t179)) % 0.39/0.61 (define @t183 () (not @t179)) % 0.39/0.61 (define @t184 () (tptp.s5 @t177)) % 0.39/0.61 (define @t185 () (tptp.q @t184)) % 0.39/0.61 (define @t186 () (or @t185 @t179 @t180)) % 0.39/0.61 (define @t187 () (@list false)) % 0.39/0.61 (define @t188 () (@list @t76)) % 0.39/0.61 (define @t189 () (@list true)) % 0.39/0.61 (define @t190 () (@list @t84)) % 0.39/0.61 (define @t191 () (@list false false)) % 0.39/0.61 (define @t192 () (@list false true)) % 0.39/0.61 (define @t193 () (not @t82)) % 0.39/0.61 (define @t194 () (@quantifiers_skolemize @t82 0)) % 0.39/0.61 (define @t195 () (tptp.p @t194)) % 0.39/0.61 (define @t196 () (or (not (tptp.n1 @t194)) @t195)) % 0.39/0.61 (define @t197 () (not @t196)) % 0.39/0.61 (assume @p1 (or @t4 @t3 @t2 @t1)) % 0.39/0.61 (assume @p2 (or @t4 @t3 tptp.n6 tptp.n10)) % 0.39/0.61 (assume @p3 (or tptp.n2 tptp.n9 @t2 @t1)) % 0.39/0.61 (assume @p4 (or tptp.n2 tptp.n9 tptp.n6 tptp.n10)) % 0.39/0.61 (assume @p5 (or @t4 tptp.n9 @t2 tptp.n10)) % 0.39/0.61 (assume @p6 (or @t4 tptp.n9 tptp.n6 @t1)) % 0.39/0.61 (assume @p7 (or tptp.n2 @t3 @t2 tptp.n10)) % 0.39/0.61 (assume @p8 (or tptp.n2 @t3 tptp.n6 @t1)) % 0.39/0.61 (assume @p9 (or @t6 tptp.n8)) % 0.39/0.61 (assume @p10 @t11) % 0.39/0.61 (assume @p11 @t16) % 0.39/0.61 (assume @p12 (or @t18 @t17)) % 0.39/0.61 (assume @p13 @t23) % 0.39/0.61 (assume @p14 (or @t2 @t24)) % 0.39/0.61 (assume @p15 (forall @t30 (or (not @t29) @t28 @t26))) % 0.39/0.61 (assume @p16 (forall @t30 (or @t29 @t27 @t26))) % 0.39/0.61 (assume @p17 @t37) % 0.39/0.61 (assume @p18 @t39) % 0.39/0.61 (assume @p19 (or @t41 tptp.n4)) % 0.39/0.61 (assume @p20 @t46) % 0.39/0.61 (assume @p21 @t51) % 0.39/0.61 (assume @p22 (or @t53 @t52)) % 0.39/0.61 (assume @p23 @t58) % 0.39/0.61 (assume @p24 (or @t4 @t59)) % 0.39/0.61 (assume @p25 @t66) % 0.39/0.61 (assume @p26 (forall @t65 (or @t63 @t62 @t61))) % 0.39/0.61 (assume @p27 @t72) % 0.39/0.61 (assume @p28 @t75) % 0.39/0.61 (assume @p29 (or @t53 @t44 tptp.n9)) % 0.39/0.61 (assume @p30 (or tptp.n3 tptp.n4 tptp.n9)) % 0.39/0.61 (assume @p31 (or @t53 tptp.n4 @t3)) % 0.39/0.61 (assume @p32 (or tptp.n3 @t44 @t3)) % 0.39/0.61 (assume @p33 (or @t18 @t9 tptp.n10)) % 0.39/0.61 (assume @p34 (or tptp.n7 tptp.n8 tptp.n10)) % 0.39/0.61 (assume @p35 (or @t18 tptp.n8 @t1)) % 0.39/0.61 (assume @p36 (or tptp.n7 @t9 @t1)) % 0.39/0.61 (step @p37 :rule quant-miniscope-or :args ((= (forall @t15 @t77) (or tptp.n7 @t76)))) % 0.39/0.61 (step @p38 :rule aci_norm :args ((= @t14 @t77))) % 0.39/0.61 (step @p39 :rule cong :premises (@p38) :args (@t16)) % 0.39/0.61 (step @p40 :rule trans :premises (@p39 @p37)) % 0.39/0.61 (step @p41 :rule eq_resolve :premises (@p11 @p40)) % 0.39/0.61 (step @p42 :rule alpha_equiv :args (@t76 (@list @t12) @t78)) % 0.39/0.61 (step @p43 :rule equiv_elim2 :premises (@p42)) % 0.39/0.61 (step @p44 :rule quant-miniscope-or :args ((= (forall @t71 @t83) (or @t82 @t80)))) % 0.39/0.61 (step @p45 :rule aci_norm :args ((= @t74 @t83))) % 0.39/0.61 (step @p46 :rule cong :premises (@p45) :args (@t75)) % 0.39/0.61 (step @p47 :rule trans :premises (@p46 @p44)) % 0.39/0.61 (step @p48 :rule eq_resolve :premises (@p28 @p47)) % 0.39/0.61 (assume-push @p399 @t82) % 0.39/0.61 (step @p50 :rule instantiate :premises (@p399) :args (@t86)) % 0.39/0.61 (step-pop @p400 :rule scope :premises (@p50)) % 0.39/0.61 (step @p51 :rule process_scope :premises (@p400) :args (@t90)) % 0.39/0.61 (step @p53 :rule implies_elim :premises (@p51)) % 0.39/0.61 (assume-push @p401 @t84) % 0.39/0.61 (step @p55 :rule instantiate :premises (@p401) :args (@t91)) % 0.39/0.61 (step-pop @p402 :rule scope :premises (@p55)) % 0.39/0.61 (step @p56 :rule process_scope :premises (@p402) :args ((not @t59))) % 0.39/0.61 (step @p58 :rule implies_elim :premises (@p56)) % 0.39/0.61 (step @p59 :rule refl :args (@t88)) % 0.39/0.61 (step @p60 :rule bool-double-not-elim :args (@t84)) % 0.39/0.61 (step @p61 :rule nary_cong :premises (@p60 @p59) :args ((or (not @t92) @t88))) % 0.39/0.61 (step @p62 :rule bool-double-not-elim :args (@t88)) % 0.39/0.61 (step @p63 :rule refl :args (@t92)) % 0.39/0.61 (step @p64 :rule cong :premises (@p63 @p62) :args ((=> @t92 @t93))) % 0.39/0.61 (assume-push @p403 @t92) % 0.39/0.61 (step @p66 :rule skolemize :premises (@p403)) % 0.39/0.61 (step-pop @p404 :rule scope :premises (@p66)) % 0.39/0.61 (step @p67 :rule process_scope :premises (@p404) :args (@t93)) % 0.39/0.61 (step @p69 :rule eq_resolve :premises (@p67 @p64)) % 0.39/0.61 (step @p70 :rule implies_elim :premises (@p69)) % 0.39/0.61 (step @p71 :rule eq_resolve :premises (@p70 @p61)) % 0.39/0.61 (step @p72 :rule cnf_or_pos :args (@t90)) % 0.39/0.61 (step @p73 :rule reordering :premises (@p72) :args ((or @t89 @t87 @t94))) % 0.39/0.61 (step @p74 :rule cnf_or_pos :args (@t96)) % 0.39/0.61 (step @p75 :rule reordering :premises (@p74) :args ((or @t89 @t95 (not @t96)))) % 0.39/0.61 (assume-push @p405 @t98) % 0.39/0.61 (step @p77 :rule instantiate :premises (@p405) :args (@t86)) % 0.39/0.61 (step-pop @p406 :rule scope :premises (@p77)) % 0.39/0.61 (step @p78 :rule process_scope :premises (@p406) :args (@t96)) % 0.39/0.61 (step @p80 :rule implies_elim :premises (@p78)) % 0.39/0.61 (step @p81 :rule quant-miniscope-or :args ((= (forall @t71 @t100) (or @t98 @t99)))) % 0.39/0.61 (step @p82 :rule aci_norm :args ((= @t70 @t100))) % 0.39/0.61 (step @p83 :rule cong :premises (@p82) :args (@t72)) % 0.39/0.61 (step @p84 :rule trans :premises (@p83 @p81)) % 0.39/0.61 (step @p85 :rule eq_resolve :premises (@p27 @p84)) % 0.39/0.61 (step @p86 :rule alpha_equiv :args (@t101 (@list @t42) @t78)) % 0.39/0.61 (step @p87 :rule equiv_elim2 :premises (@p86)) % 0.39/0.61 (assume-push @p407 @t101) % 0.39/0.61 (step @p89 :rule instantiate :premises (@p407) :args ((@list tptp.s4))) % 0.39/0.61 (step-pop @p408 :rule scope :premises (@p89)) % 0.39/0.61 (step @p90 :rule process_scope :premises (@p408) :args (@t40)) % 0.39/0.61 (step @p92 :rule implies_elim :premises (@p90)) % 0.39/0.61 (step @p93 :rule reordering :premises (@p92) :args ((or @t40 @t102))) % 0.39/0.61 (step @p94 :rule reordering :premises (@p19) :args ((or tptp.n4 @t41))) % 0.39/0.61 (step @p95 :rule reordering :premises (@p9) :args ((or tptp.n8 @t6))) % 0.39/0.61 (step @p96 :rule reordering :premises (@p35) :args ((or @t1 tptp.n8 @t18))) % 0.39/0.61 (assume-push @p409 @t103) % 0.39/0.61 (step @p98 :rule instantiate :premises (@p409) :args ((@list tptp.s8))) % 0.39/0.61 (step-pop @p410 :rule scope :premises (@p98)) % 0.39/0.61 (step @p99 :rule process_scope :premises (@p410) :args (@t5)) % 0.39/0.61 (step @p101 :rule implies_elim :premises (@p99)) % 0.39/0.61 (step @p102 :rule reordering :premises (@p101) :args ((or @t5 @t104))) % 0.39/0.61 (step @p103 :rule alpha_equiv :args (@t103 (@list @t7) @t105)) % 0.39/0.61 (step @p104 :rule equiv_elim2 :premises (@p103)) % 0.39/0.61 (step @p105 :rule quant-miniscope-or :args ((= (forall @t36 @t110) (or @t109 @t107)))) % 0.39/0.61 (step @p106 :rule aci_norm :args ((= @t38 @t110))) % 0.39/0.61 (step @p107 :rule cong :premises (@p106) :args (@t39)) % 0.39/0.61 (step @p108 :rule trans :premises (@p107 @p105)) % 0.39/0.61 (step @p109 :rule eq_resolve :premises (@p18 @p108)) % 0.39/0.61 (assume-push @p411 @t109) % 0.39/0.61 (step @p111 :rule instantiate :premises (@p411) :args (@t111)) % 0.39/0.61 (step-pop @p412 :rule scope :premises (@p111)) % 0.39/0.61 (step @p112 :rule process_scope :premises (@p412) :args (@t115)) % 0.39/0.61 (step @p114 :rule implies_elim :premises (@p112)) % 0.39/0.61 (step @p115 :rule quant-miniscope-or :args ((= (forall @t50 @t117) (or tptp.n3 @t116)))) % 0.39/0.61 (step @p116 :rule aci_norm :args ((= @t49 @t117))) % 0.39/0.61 (step @p117 :rule cong :premises (@p116) :args (@t51)) % 0.39/0.61 (step @p118 :rule trans :premises (@p117 @p115)) % 0.39/0.61 (step @p119 :rule eq_resolve :premises (@p21 @p118)) % 0.39/0.61 (step @p120 :rule reordering :premises (@p32) :args ((or @t3 @t44 tptp.n3))) % 0.39/0.61 (step @p121 :rule alpha_equiv :args (@t118 @t105 (@list @t47))) % 0.39/0.61 (step @p122 :rule equiv_elim2 :premises (@p121)) % 0.39/0.61 (step @p123 :rule reordering :premises (@p5) :args ((or tptp.n9 tptp.n10 @t4 @t2))) % 0.39/0.61 (assume-push @p413 @t118) % 0.39/0.61 (step @p125 :rule instantiate :premises (@p413) :args (@t122)) % 0.39/0.61 (step-pop @p414 :rule scope :premises (@p125)) % 0.39/0.61 (step @p126 :rule process_scope :premises (@p414) :args ((not @t123))) % 0.39/0.61 (step @p128 :rule implies_elim :premises (@p126)) % 0.39/0.61 (assume-push @p415 @t118) % 0.39/0.61 (step @p130 :rule instantiate :premises (@p415) :args ((@list @t124))) % 0.39/0.61 (step-pop @p416 :rule scope :premises (@p130)) % 0.39/0.61 (step @p131 :rule process_scope :premises (@p416) :args ((not @t125))) % 0.39/0.61 (step @p133 :rule implies_elim :premises (@p131)) % 0.39/0.61 (step @p134 :rule quant-miniscope-or :args ((= (forall @t22 @t127) (or tptp.n6 @t126)))) % 0.39/0.61 (step @p135 :rule aci_norm :args ((= @t21 @t127))) % 0.39/0.61 (step @p136 :rule cong :premises (@p135) :args (@t23)) % 0.39/0.61 (step @p137 :rule trans :premises (@p136 @p134)) % 0.39/0.61 (step @p138 :rule eq_resolve :premises (@p13 @p137)) % 0.39/0.61 (step @p139 :rule instantiate :premises (@p16) :args (@t122)) % 0.39/0.61 (step @p140 :rule cnf_or_pos :args (@t129)) % 0.39/0.61 (step @p141 :rule reordering :premises (@p140) :args ((or @t128 @t123 @t125 (not @t129)))) % 0.39/0.61 (assume-push @p417 @t126) % 0.39/0.61 (step @p143 :rule instantiate :premises (@p417) :args (@t122)) % 0.39/0.61 (step-pop @p418 :rule scope :premises (@p143)) % 0.39/0.61 (step @p144 :rule process_scope :premises (@p418) :args (@t130)) % 0.39/0.61 (step @p146 :rule implies_elim :premises (@p144)) % 0.39/0.61 (step @p147 :rule chain_m_resolution :premises (@p146 @p141 @p139 @p138 @p133 @p128 @p123 @p122 @p120 @p119) :args ((or tptp.n10 @t4 @t44 tptp.n3) (@list false false false true true true false true false) (@list @t128 @t129 @t126 @t125 @t123 tptp.n6 @t118 tptp.n9 @t116))) % 0.39/0.61 (step @p148 :rule reordering :premises (@p29) :args ((or tptp.n9 @t44 @t53))) % 0.39/0.61 (assume-push @p419 @t118) % 0.39/0.61 (step @p150 :rule instantiate :premises (@p419) :args ((@list tptp.s3))) % 0.39/0.61 (step-pop @p420 :rule scope :premises (@p150)) % 0.39/0.61 (step @p151 :rule process_scope :premises (@p420) :args ((not @t52))) % 0.39/0.61 (step @p153 :rule implies_elim :premises (@p151)) % 0.39/0.61 (step @p154 :rule reordering :premises (@p2) :args ((or tptp.n6 tptp.n10 @t4 @t3))) % 0.39/0.61 (step @p155 :rule quant-miniscope-or :args ((= (forall @t36 @t131) (or @t120 @t118)))) % 0.39/0.61 (step @p156 :rule aci_norm :args ((= @t35 @t131))) % 0.39/0.61 (step @p157 :rule cong :premises (@p156) :args (@t37)) % 0.39/0.61 (step @p158 :rule trans :premises (@p157 @p155)) % 0.39/0.61 (step @p159 :rule eq_resolve :premises (@p17 @p158)) % 0.39/0.61 (assume-push @p421 @t120) % 0.39/0.61 (step @p161 :rule instantiate :premises (@p421) :args (@t111)) % 0.39/0.61 (step-pop @p422 :rule scope :premises (@p161)) % 0.39/0.61 (step @p162 :rule process_scope :premises (@p422) :args (@t132)) % 0.39/0.61 (step @p164 :rule implies_elim :premises (@p162)) % 0.39/0.61 (step @p165 :rule cnf_or_pos :args (@t115)) % 0.39/0.61 (step @p166 :rule reordering :premises (@p165) :args ((or @t114 @t113 @t133))) % 0.39/0.61 (step @p167 :rule cnf_or_pos :args (@t132)) % 0.39/0.61 (step @p168 :rule reordering :premises (@p167) :args ((or @t114 @t112 (not @t132)))) % 0.39/0.61 (step @p169 :rule chain_m_resolution :premises (@p168 @p166 @p164 @p14 @p159 @p154 @p153 @p148 @p22 @p147 @p114 @p109 @p104 @p102 @p96 @p95) :args ((or @t4 tptp.n8 @t18 @t44) (@list true false false false false true false false false false false true true true true) (@list @t112 @t132 @t24 @t120 tptp.n6 @t118 tptp.n9 @t52 tptp.n3 @t115 @t109 @t107 @t103 tptp.n10 @t5))) % 0.39/0.61 (step @p170 :rule quant-miniscope-or :args ((= @t11 (or @t9 @t103)))) % 0.39/0.61 (step @p171 :rule eq_resolve :premises (@p10 @p170)) % 0.39/0.61 (step @p172 :rule reordering :premises (@p33) :args ((or tptp.n10 @t9 @t18))) % 0.39/0.61 (assume-push @p423 @t103) % 0.39/0.61 (step @p174 :rule instantiate :premises (@p423) :args (@t111)) % 0.39/0.61 (step-pop @p424 :rule scope :premises (@p174)) % 0.39/0.61 (step @p175 :rule process_scope :premises (@p424) :args (@t112)) % 0.39/0.61 (step @p177 :rule implies_elim :premises (@p175)) % 0.39/0.61 (assume-push @p425 @t103) % 0.39/0.61 (step @p179 :rule instantiate :premises (@p425) :args ((@list @t134))) % 0.39/0.61 (step-pop @p426 :rule scope :premises (@p179)) % 0.39/0.61 (step @p180 :rule process_scope :premises (@p426) :args (@t135)) % 0.39/0.61 (step @p182 :rule implies_elim :premises (@p180)) % 0.39/0.61 (assume-push @p427 @t118) % 0.39/0.61 (step @p184 :rule instantiate :premises (@p427) :args (@t111)) % 0.39/0.61 (step-pop @p428 :rule scope :premises (@p184)) % 0.39/0.61 (step @p185 :rule process_scope :premises (@p428) :args (@t113)) % 0.39/0.61 (step @p187 :rule implies_elim :premises (@p185)) % 0.39/0.61 (step @p188 :rule instantiate :premises (@p15) :args (@t111)) % 0.39/0.61 (step @p189 :rule cnf_or_pos :args (@t137)) % 0.39/0.61 (step @p190 :rule reordering :premises (@p189) :args ((or @t24 @t136 @t113 (not @t137)))) % 0.39/0.61 (assume-push @p429 @t126) % 0.39/0.61 (step @p192 :rule instantiate :premises (@p429) :args (@t111)) % 0.39/0.61 (step-pop @p430 :rule scope :premises (@p192)) % 0.39/0.61 (step @p193 :rule process_scope :premises (@p430) :args (@t114)) % 0.39/0.61 (step @p195 :rule implies_elim :premises (@p193)) % 0.39/0.61 (step @p196 :rule chain_m_resolution :premises (@p1 @p148 @p138 @p119 @p195 @p122 @p190 @p188 @p187 @p182 @p177 @p172 @p171 @p169 @p94 @p93 @p87 @p85 @p80 @p75 @p73 @p71 @p58 @p24) :args ((or @t4 @t18 @t94) (@list false false false true true false false true false false false false false false false false false true true false false true false) (@list tptp.n9 tptp.n6 tptp.n3 @t126 @t116 @t24 @t137 @t118 @t135 @t112 tptp.n10 @t103 tptp.n8 tptp.n4 @t40 @t101 @t99 @t98 @t96 @t87 @t88 @t84 @t59))) % 0.39/0.61 (step @p197 :rule quant-miniscope-or :args ((= (forall @t57 @t138) (or tptp.n2 @t84)))) % 0.39/0.61 (step @p198 :rule aci_norm :args ((= @t56 @t138))) % 0.39/0.61 (step @p199 :rule cong :premises (@p198) :args (@t58)) % 0.39/0.61 (step @p200 :rule trans :premises (@p199 @p197)) % 0.39/0.61 (step @p201 :rule eq_resolve :premises (@p23 @p200)) % 0.39/0.61 (assume-push @p431 @t84) % 0.39/0.61 (step @p203 :rule instantiate :premises (@p431) :args (@t140)) % 0.39/0.61 (step-pop @p432 :rule scope :premises (@p203)) % 0.39/0.61 (step @p204 :rule process_scope :premises (@p432) :args (@t142)) % 0.39/0.61 (step @p206 :rule implies_elim :premises (@p204)) % 0.39/0.61 (step @p207 :rule bool-double-not-elim :args (@t141)) % 0.39/0.61 (step @p208 :rule refl :args (@t145)) % 0.39/0.61 (step @p209 :rule nary_cong :premises (@p208 @p207) :args ((or @t145 (not @t142)))) % 0.39/0.61 (step @p210 :rule cnf_or_neg :args (@t145 0)) % 0.39/0.61 (step @p211 :rule eq_resolve :premises (@p210 @p209)) % 0.39/0.61 (step @p212 :rule reordering :premises (@p211) :args ((or @t141 @t145))) % 0.39/0.61 (step @p213 :rule refl :args (@t146)) % 0.39/0.61 (step @p214 :rule bool-double-not-elim :args (@t98)) % 0.39/0.61 (step @p215 :rule nary_cong :premises (@p214 @p213) :args ((or (not @t147) @t146))) % 0.39/0.61 (assume-push @p433 @t147) % 0.39/0.61 (step @p217 :rule skolemize :premises (@p433)) % 0.39/0.61 (step-pop @p434 :rule scope :premises (@p217)) % 0.39/0.61 (step @p218 :rule process_scope :premises (@p434) :args (@t146)) % 0.39/0.61 (step @p220 :rule implies_elim :premises (@p218)) % 0.39/0.61 (step @p221 :rule eq_resolve :premises (@p220 @p215)) % 0.39/0.61 (assume-push @p435 @t98) % 0.39/0.61 (step @p223 :rule instantiate :premises (@p435) :args (@t148)) % 0.39/0.61 (step-pop @p436 :rule scope :premises (@p223)) % 0.39/0.61 (step @p224 :rule process_scope :premises (@p436) :args (@t152)) % 0.39/0.61 (step @p226 :rule implies_elim :premises (@p224)) % 0.39/0.61 (step @p227 :rule cnf_or_pos :args (@t152)) % 0.39/0.61 (step @p228 :rule reordering :premises (@p227) :args ((or @t149 @t151 (not @t152)))) % 0.39/0.61 (step @p229 :rule instantiate :premises (@p25) :args (@t148)) % 0.39/0.61 (step @p230 :rule cnf_or_pos :args (@t156)) % 0.39/0.61 (step @p231 :rule reordering :premises (@p230) :args ((or @t149 @t150 @t155 (not @t156)))) % 0.39/0.61 (assume-push @p437 @t101) % 0.39/0.61 (step @p233 :rule instantiate :premises (@p437) :args ((@list @t153))) % 0.39/0.61 (step-pop @p438 :rule scope :premises (@p233)) % 0.39/0.61 (step @p234 :rule process_scope :premises (@p438) :args (@t154)) % 0.39/0.61 (step @p236 :rule implies_elim :premises (@p234)) % 0.39/0.61 (step @p237 :rule quant-miniscope-or :args ((= @t46 (or @t44 @t101)))) % 0.39/0.61 (step @p238 :rule eq_resolve :premises (@p20 @p237)) % 0.39/0.61 (assume-push @p439 @t66) % 0.39/0.61 (step-pop @p440 :rule scope :premises (@p229)) % 0.39/0.61 (step @p240 :rule process_scope :premises (@p440) :args (@t156)) % 0.39/0.61 (step @p242 :rule implies_elim :premises (@p240)) % 0.39/0.61 (assume-push @p441 @t76) % 0.39/0.61 (step @p244 :rule instantiate :premises (@p441) :args (@t91)) % 0.39/0.61 (step-pop @p442 :rule scope :premises (@p244)) % 0.39/0.61 (step @p245 :rule process_scope :premises (@p442) :args ((not @t157))) % 0.39/0.61 (step @p247 :rule implies_elim :premises (@p245)) % 0.39/0.61 (assume-push @p443 @t76) % 0.39/0.61 (step @p249 :rule instantiate :premises (@p443) :args ((@list @t158))) % 0.39/0.61 (step-pop @p444 :rule scope :premises (@p249)) % 0.39/0.61 (step @p250 :rule process_scope :premises (@p444) :args ((not @t159))) % 0.39/0.61 (step @p252 :rule implies_elim :premises (@p250)) % 0.39/0.61 (step @p253 :rule instantiate :premises (@p26) :args (@t91)) % 0.39/0.61 (step @p254 :rule cnf_or_pos :args (@t160)) % 0.39/0.61 (step @p255 :rule reordering :premises (@p254) :args ((or @t59 @t157 @t159 (not @t160)))) % 0.39/0.61 (step @p256 :rule chain_m_resolution :premises (@p255 @p253 @p252 @p247) :args ((or @t59 @t161) (@list false true true) (@list @t160 @t159 @t157))) % 0.39/0.61 (assume-push @p445 @t98) % 0.39/0.61 (step @p258 :rule instantiate :premises (@p445) :args (@t163)) % 0.39/0.61 (step-pop @p446 :rule scope :premises (@p258)) % 0.39/0.61 (step @p259 :rule process_scope :premises (@p446) :args (@t168)) % 0.39/0.61 (step @p261 :rule implies_elim :premises (@p259)) % 0.39/0.61 (step @p262 :rule refl :args (@t164)) % 0.39/0.61 (step @p263 :rule bool-double-not-elim :args (@t76)) % 0.39/0.61 (step @p264 :rule nary_cong :premises (@p263 @p262) :args ((or (not @t161) @t164))) % 0.39/0.61 (step @p265 :rule bool-double-not-elim :args (@t164)) % 0.39/0.61 (step @p266 :rule refl :args (@t161)) % 0.39/0.61 (step @p267 :rule cong :premises (@p266 @p265) :args ((=> @t161 @t169))) % 0.39/0.61 (assume-push @p447 @t161) % 0.39/0.61 (step @p269 :rule skolemize :premises (@p447)) % 0.39/0.61 (step-pop @p448 :rule scope :premises (@p269)) % 0.39/0.61 (step @p270 :rule process_scope :premises (@p448) :args (@t169)) % 0.39/0.61 (step @p272 :rule eq_resolve :premises (@p270 @p267)) % 0.39/0.61 (step @p273 :rule implies_elim :premises (@p272)) % 0.39/0.61 (step @p274 :rule eq_resolve :premises (@p273 @p264)) % 0.39/0.61 (step @p275 :rule cnf_or_pos :args (@t168)) % 0.39/0.61 (step @p276 :rule reordering :premises (@p275) :args ((or @t165 @t167 (not @t168)))) % 0.39/0.61 (step @p277 :rule reordering :premises (@p7) :args ((or tptp.n2 tptp.n10 @t3 @t2))) % 0.39/0.61 (step @p278 :rule instantiate :premises (@p25) :args (@t163)) % 0.39/0.61 (step @p279 :rule cnf_or_pos :args (@t173)) % 0.39/0.61 (step @p280 :rule reordering :premises (@p279) :args ((or @t165 @t166 @t172 (not @t173)))) % 0.39/0.61 (step @p281 :rule reordering :premises (@p30) :args ((or tptp.n9 tptp.n4 tptp.n3))) % 0.39/0.61 (assume-push @p449 @t101) % 0.39/0.61 (step @p283 :rule instantiate :premises (@p449) :args ((@list @t170))) % 0.39/0.61 (step-pop @p450 :rule scope :premises (@p283)) % 0.39/0.61 (step @p284 :rule process_scope :premises (@p450) :args (@t171)) % 0.39/0.61 (step @p286 :rule implies_elim :premises (@p284)) % 0.39/0.61 (step @p287 :rule chain_m_resolution :premises (@p238 @p286 @p281 @p280 @p278 @p277 @p276 @p96 @p274 @p41 @p261 @p221 @p212 @p206 @p201) :args ((or tptp.n2 @t2 tptp.n8 tptp.n3 @t76) (@list true false true false true true true false false false false false true false) (@list @t101 tptp.n4 @t171 @t173 tptp.n9 @t166 tptp.n10 @t164 tptp.n7 @t168 @t98 @t145 @t141 @t84))) % 0.39/0.61 (step @p288 :rule chain_m_resolution :premises (@p177 @p187 @p171 @p122 @p287 @p119 @p256 @p58 @p201) :args ((or tptp.n2 @t2 tptp.n3) (@list true false false false false true true false) (@list @t112 @t103 @t118 tptp.n8 @t116 @t76 @t59 @t84))) % 0.39/0.61 (step @p289 :rule reordering :premises (@p31) :args ((or @t3 tptp.n4 @t53))) % 0.39/0.61 (step @p290 :rule chain_m_resolution :premises (@p109 @p114 @p104 @p166 @p102 @p168 @p95 @p164 @p172 @p159 @p3 @p153 @p289 @p22 @p288 @p14 @p238 @p236 @p231 @p242 @p25 @p228 @p12 @p226 @p221 @p212 @p206 @p201) :args ((or tptp.n2 @t2 @t18) (@list true true true true false true false true false true true true false false false true true true false false true false false false false true false) (@list @t109 @t107 @t115 @t103 @t112 @t5 @t132 tptp.n8 @t120 tptp.n10 @t118 tptp.n9 @t52 tptp.n3 @t24 tptp.n4 @t101 @t154 @t156 @t66 @t150 @t17 @t152 @t98 @t145 @t141 @t84))) % 0.39/0.61 (step @p291 :rule bool-double-not-elim :args (@t128)) % 0.39/0.61 (step @p292 :rule refl :args (@t174)) % 0.39/0.61 (step @p293 :rule nary_cong :premises (@p292 @p291) :args ((or @t174 (not @t130)))) % 0.39/0.61 (step @p294 :rule cnf_or_neg :args (@t174 0)) % 0.39/0.61 (step @p295 :rule eq_resolve :premises (@p294 @p293)) % 0.39/0.61 (step @p296 :rule reordering :premises (@p295) :args ((or @t128 @t174))) % 0.39/0.61 (step @p297 :rule refl :args (@t175)) % 0.39/0.61 (step @p298 :rule bool-double-not-elim :args (@t120)) % 0.39/0.61 (step @p299 :rule nary_cong :premises (@p298 @p297) :args ((or (not @t176) @t175))) % 0.39/0.61 (assume-push @p451 @t176) % 0.39/0.61 (step @p301 :rule skolemize :premises (@p451)) % 0.39/0.61 (step-pop @p452 :rule scope :premises (@p301)) % 0.39/0.61 (step @p302 :rule process_scope :premises (@p452) :args (@t175)) % 0.39/0.61 (step @p304 :rule implies_elim :premises (@p302)) % 0.39/0.61 (step @p305 :rule eq_resolve :premises (@p304 @p299)) % 0.39/0.61 (assume-push @p453 @t120) % 0.39/0.61 (step @p307 :rule instantiate :premises (@p453) :args (@t178)) % 0.39/0.61 (step-pop @p454 :rule scope :premises (@p307)) % 0.39/0.61 (step @p308 :rule process_scope :premises (@p454) :args (@t182)) % 0.39/0.61 (step @p310 :rule implies_elim :premises (@p308)) % 0.39/0.61 (step @p311 :rule chain_m_resolution :premises (@p190 @p188 @p182 @p177) :args ((or @t24 @t104) (@list false false false) (@list @t137 @t135 @t112))) % 0.39/0.61 (step @p312 :rule refl :args (@t183)) % 0.39/0.61 (step @p313 :rule bool-double-not-elim :args (@t103)) % 0.39/0.61 (step @p314 :rule nary_cong :premises (@p313 @p312) :args ((or (not @t104) @t183))) % 0.39/0.61 (assume-push @p455 @t104) % 0.39/0.61 (step @p316 :rule skolemize :premises (@p455)) % 0.39/0.61 (step-pop @p456 :rule scope :premises (@p316)) % 0.39/0.61 (step @p317 :rule process_scope :premises (@p456) :args (@t183)) % 0.39/0.61 (step @p319 :rule implies_elim :premises (@p317)) % 0.39/0.61 (step @p320 :rule eq_resolve :premises (@p319 @p314)) % 0.39/0.61 (step @p321 :rule cnf_or_pos :args (@t182)) % 0.39/0.61 (step @p322 :rule reordering :premises (@p321) :args ((or @t179 @t181 (not @t182)))) % 0.39/0.61 (step @p323 :rule instantiate :premises (@p16) :args (@t178)) % 0.39/0.61 (step @p324 :rule cnf_or_pos :args (@t186)) % 0.39/0.61 (step @p325 :rule reordering :premises (@p324) :args ((or @t179 @t180 @t185 (not @t186)))) % 0.39/0.61 (assume-push @p457 @t118) % 0.39/0.61 (step @p327 :rule instantiate :premises (@p457) :args ((@list @t184))) % 0.39/0.61 (step-pop @p458 :rule scope :premises (@p327)) % 0.39/0.61 (step @p328 :rule process_scope :premises (@p458) :args ((not @t185))) % 0.39/0.61 (step @p330 :rule implies_elim :premises (@p328)) % 0.39/0.61 (step @p331 :rule chain_m_resolution :premises (@p122 @p119 @p330 @p289 @p325 @p323 @p4 @p322 @p96 @p320 @p171 @p311 @p310 @p305 @p296 @p195 @p146 @p138 @p290 @p238 @p236 @p231 @p229 @p228 @p226 @p221 @p212 @p206 @p201 @p196 @p53 @p48 @p12 @p43 @p41) :args (@t76 (@list false true true false false false true true true true true false false false true true false true true true true false true false false false true false true false false false true false) (@list @t116 @t118 tptp.n3 @t185 @t186 tptp.n9 @t180 tptp.n10 @t179 tptp.n8 @t103 @t182 @t120 @t174 @t24 @t128 @t126 tptp.n6 tptp.n4 @t101 @t154 @t156 @t150 @t152 @t98 @t145 @t141 @t84 tptp.n2 @t90 @t82 @t17 @t80 tptp.n7))) % 0.39/0.61 (assume-push @p459 @t76) % 0.39/0.61 (step @p333 :rule instantiate :premises (@p459) :args (@t148)) % 0.39/0.61 (step-pop @p460 :rule scope :premises (@p333)) % 0.39/0.61 (step @p334 :rule process_scope :premises (@p460) :args (@t149)) % 0.39/0.61 (step @p336 :rule implies_elim :premises (@p334)) % 0.39/0.61 (step @p337 :rule chain_m_resolution :premises (@p336 @p331) :args (@t149 @t187 @t188)) % 0.39/0.61 (step @p338 :rule chain_m_resolution :premises (@p12 @p337) :args (@t18 @t189 (@list @t17))) % 0.39/0.61 (step @p339 :rule reordering :premises (@p34) :args ((or tptp.n10 tptp.n8 tptp.n7))) % 0.39/0.61 (step @p340 :rule chain_m_resolution :premises (@p256 @p331) :args (@t59 @t187 @t188)) % 0.39/0.61 (step @p341 :rule chain_m_resolution :premises (@p58 @p340) :args (@t92 @t187 (@list @t59))) % 0.39/0.61 (step @p342 :rule chain_m_resolution :premises (@p201 @p341) :args (tptp.n2 @t189 @t190)) % 0.39/0.61 (step @p343 :rule reordering :premises (@p6) :args ((or tptp.n9 tptp.n6 @t4 @t1))) % 0.39/0.61 (assume-push @p461 @t76) % 0.39/0.61 (step @p345 :rule instantiate :premises (@p461) :args (@t140)) % 0.39/0.61 (step-pop @p462 :rule scope :premises (@p345)) % 0.39/0.61 (step @p346 :rule process_scope :premises (@p462) :args (@t144)) % 0.39/0.61 (step @p348 :rule implies_elim :premises (@p346)) % 0.39/0.61 (step @p349 :rule chain_m_resolution :premises (@p348 @p331) :args (@t144 @t187 @t188)) % 0.39/0.61 (step @p350 :rule bool-double-not-elim :args (@t143)) % 0.39/0.61 (step @p351 :rule nary_cong :premises (@p208 @p350) :args ((or @t145 (not @t144)))) % 0.39/0.61 (step @p352 :rule cnf_or_neg :args (@t145 1)) % 0.39/0.61 (step @p353 :rule eq_resolve :premises (@p352 @p351)) % 0.39/0.61 (step @p354 :rule reordering :premises (@p353) :args ((or @t143 @t145))) % 0.39/0.61 (step @p355 :rule chain_m_resolution :premises (@p354 @p349) :args (@t145 @t189 (@list @t143))) % 0.39/0.61 (step @p356 :rule chain_m_resolution :premises (@p221 @p355) :args (@t98 @t187 (@list @t145))) % 0.39/0.61 (step @p357 :rule chain_m_resolution :premises (@p80 @p356) :args (@t96 @t187 (@list @t98))) % 0.39/0.61 (step @p358 :rule chain_m_resolution :premises (@p71 @p341) :args (@t88 @t189 @t190)) % 0.39/0.61 (step @p359 :rule chain_m_resolution :premises (@p75 @p358 @p357) :args (@t95 @t191 (@list @t88 @t96))) % 0.39/0.61 (step @p360 :rule chain_m_resolution :premises (@p73 @p358 @p359) :args (@t94 @t192 (@list @t88 @t87))) % 0.39/0.61 (step @p361 :rule chain_m_resolution :premises (@p53 @p360) :args (@t193 @t189 (@list @t90))) % 0.39/0.61 (step @p362 :rule refl :args (@t197)) % 0.39/0.61 (step @p363 :rule bool-double-not-elim :args (@t82)) % 0.39/0.61 (step @p364 :rule nary_cong :premises (@p363 @p362) :args ((or (not @t193) @t197))) % 0.39/0.61 (assume-push @p463 @t193) % 0.39/0.61 (step @p366 :rule skolemize :premises (@p463)) % 0.39/0.61 (step-pop @p464 :rule scope :premises (@p366)) % 0.39/0.61 (step @p367 :rule process_scope :premises (@p464) :args (@t197)) % 0.39/0.61 (step @p369 :rule implies_elim :premises (@p367)) % 0.39/0.61 (step @p370 :rule eq_resolve :premises (@p369 @p364)) % 0.39/0.61 (step @p371 :rule chain_m_resolution :premises (@p370 @p361) :args (@t197 @t189 (@list @t82))) % 0.39/0.61 (step @p372 :rule cnf_or_neg :args (@t196 1)) % 0.39/0.61 (step @p373 :rule chain_m_resolution :premises (@p372 @p371) :args ((not @t195) @t189 (@list @t196))) % 0.39/0.61 (assume-push @p465 @t101) % 0.39/0.61 (step @p375 :rule instantiate :premises (@p465) :args ((@list @t194))) % 0.39/0.61 (step-pop @p466 :rule scope :premises (@p375)) % 0.39/0.61 (step @p376 :rule process_scope :premises (@p466) :args (@t195)) % 0.39/0.61 (step @p378 :rule implies_elim :premises (@p376)) % 0.39/0.61 (step @p379 :rule chain_m_resolution :premises (@p378 @p373) :args (@t102 @t189 (@list @t195))) % 0.39/0.61 (step @p380 :rule chain_m_resolution :premises (@p238 @p379) :args (@t44 @t189 (@list @t101))) % 0.39/0.61 (step @p381 :rule chain_m_resolution :premises (@p122 @p119 @p330 @p289 @p380 @p325 @p323 @p343 @p342 @p322 @p339 @p338 @p310 @p320 @p171 @p305 @p311 @p296 @p195 @p146 @p138) :args (tptp.n6 (@list false true true true false false false false true false true false true true false true false true true false) (@list @t116 @t118 tptp.n3 tptp.n4 @t185 @t186 tptp.n9 tptp.n2 @t180 tptp.n10 tptp.n7 @t182 @t179 tptp.n8 @t120 @t103 @t174 @t24 @t128 @t126))) % 0.39/0.61 (step @p382 :rule chain_m_resolution :premises (@p171 @p177 @p339 @p338 @p187 @p1 @p381 @p342 @p122 @p281 @p380 @p119) :args (tptp.n3 (@list true false true true true false false false false true false) (@list @t103 tptp.n8 tptp.n7 @t112 tptp.n10 tptp.n6 tptp.n2 @t118 tptp.n9 tptp.n4 @t116))) % 0.39/0.61 (step @p383 :rule chain_m_resolution :premises (@p289 @p380 @p382) :args (@t3 (@list true false) (@list tptp.n4 tptp.n3))) % 0.39/0.61 (step @p384 :rule chain_m_resolution :premises (@p123 @p383 @p342 @p381) :args (tptp.n10 (@list true false false) (@list tptp.n9 tptp.n2 tptp.n6))) % 0.39/0.61 (step @p385 :rule reordering :premises (@p36) :args ((or @t1 @t9 tptp.n7))) % 0.39/0.61 (step @p386 :rule chain_m_resolution :premises (@p385 @p384 @p338) :args (@t9 @t192 (@list tptp.n10 tptp.n7))) % 0.39/0.61 (step @p387 :rule chain_m_resolution :premises (@p95 @p386) :args (@t6 @t189 (@list tptp.n8))) % 0.39/0.61 (step @p388 :rule chain_m_resolution :premises (@p102 @p387) :args (@t104 @t189 (@list @t5))) % 0.39/0.61 (step @p389 :rule chain_m_resolution :premises (@p104 @p388) :args ((not @t107) @t189 (@list @t103))) % 0.39/0.61 (step @p390 :rule chain_m_resolution :premises (@p22 @p382) :args (@t52 @t187 (@list tptp.n3))) % 0.39/0.61 (step @p391 :rule chain_m_resolution :premises (@p153 @p390) :args ((not @t118) @t187 (@list @t52))) % 0.39/0.61 (step @p392 :rule chain_m_resolution :premises (@p159 @p391) :args (@t120 @t189 (@list @t118))) % 0.39/0.61 (step @p393 :rule chain_m_resolution :premises (@p164 @p392) :args (@t132 @t187 (@list @t120))) % 0.39/0.61 (step @p394 :rule chain_m_resolution :premises (@p14 @p381) :args (@t24 @t187 (@list tptp.n6))) % 0.39/0.61 (step @p395 :rule chain_m_resolution :premises (@p168 @p394 @p393) :args (@t112 @t191 (@list @t24 @t132))) % 0.39/0.61 (step @p396 :rule chain_m_resolution :premises (@p166 @p394 @p395) :args (@t133 @t191 (@list @t24 @t112))) % 0.39/0.61 (step @p397 :rule chain_m_resolution :premises (@p114 @p396) :args ((not @t109) @t189 (@list @t115))) % 0.39/0.61 (step @p398 false :rule chain_m_resolution :premises (@p109 @p397 @p389) :args (false (@list true true) (@list @t109 @t107))) % 0.39/0.61 ) % 0.39/0.61 % SZS output end Proof % 0.39/0.61 % cvc5 exiting %------------------------------------------------------------------------------