%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : MGT064-1 : TPTP v9.3.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n005.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 8 06:04:55 AM UTC 2026 % Result : Unsatisfiable 0.37s 0.68s % Output : Proof 0.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT064-1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.10/0.36 % Computer : n005.cluster.edu % 0.10/0.36 % Model : x86_64 x86_64 % 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.36 % Memory : 8046.5625MB % 0.10/0.36 % OS : Linux 6.8.0-71-generic % 0.10/0.36 % CPULimit : 300 % 0.10/0.36 % WCLimit : 300 % 0.10/0.36 % DateTime : Mon Sep 7 13:44:50 UTC 2026 % 0.13/0.36 % CPUTime : % 0.13/0.43 %----Proving TF0_NAR, FOF, or CNF % 0.13/0.45 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 0.37/0.68 % SZS status Unsatisfiable % 0.37/0.68 % SZS output start Proof % 0.37/0.69 ( % 0.37/0.69 (declare-sort $$unsorted 0) % 0.37/0.69 (declare-const tptp.sk6 $$unsorted) % 0.37/0.69 (declare-const tptp.sk4 $$unsorted) % 0.37/0.69 (declare-const tptp.sk5 $$unsorted) % 0.37/0.69 (declare-const tptp.mod1 $$unsorted) % 0.37/0.69 (declare-const tptp.mod2 $$unsorted) % 0.37/0.69 (declare-const tptp.sk2 (-> $$unsorted $$unsorted)) % 0.37/0.69 (declare-const tptp.sk3 $$unsorted) % 0.37/0.69 (declare-const tptp.robust_position (-> $$unsorted Bool)) % 0.37/0.69 (declare-const tptp.very_low $$unsorted) % 0.37/0.69 (declare-const tptp.tau $$unsorted) % 0.37/0.69 (declare-const tptp.hazard_of_mortality (-> $$unsorted $$unsorted $$unsorted)) % 0.37/0.69 (declare-const tptp.positional_advantage (-> $$unsorted $$unsorted Bool)) % 0.37/0.69 (declare-const tptp.sigma $$unsorted) % 0.37/0.69 (declare-const tptp.smaller (-> $$unsorted $$unsorted Bool)) % 0.37/0.69 (declare-const tptp.sk7 $$unsorted) % 0.37/0.69 (declare-const tptp.eta $$unsorted) % 0.37/0.69 (declare-const tptp.smaller_or_equal (-> $$unsorted $$unsorted Bool)) % 0.37/0.69 (declare-const tptp.low $$unsorted) % 0.37/0.69 (declare-const tptp.greater (-> $$unsorted $$unsorted Bool)) % 0.37/0.69 (declare-const tptp.age (-> $$unsorted $$unsorted $$unsorted)) % 0.37/0.69 (declare-const tptp.is_aligned (-> $$unsorted $$unsorted Bool)) % 0.37/0.69 (declare-const tptp.greater_or_equal (-> $$unsorted $$unsorted Bool)) % 0.37/0.69 (declare-const tptp.organization (-> $$unsorted Bool)) % 0.37/0.69 (declare-const tptp.zero $$unsorted) % 0.37/0.69 (declare-const tptp.has_endowment (-> $$unsorted Bool)) % 0.37/0.69 (declare-const tptp.high $$unsorted) % 0.37/0.69 (declare-const tptp.has_immunity (-> $$unsorted $$unsorted Bool)) % 0.37/0.69 (declare-const tptp.sk1 (-> $$unsorted $$unsorted)) % 0.37/0.69 (declare-const tptp.dissimilar (-> $$unsorted $$unsorted $$unsorted Bool)) % 0.37/0.69 (define @t1 () (@var "B" $$unsorted)) % 0.37/0.69 (define @t2 () (@var "A" $$unsorted)) % 0.37/0.69 (define @t3 () (= @t2 @t1)) % 0.37/0.69 (define @t4 () (tptp.smaller @t2 @t1)) % 0.37/0.69 (define @t5 () (tptp.smaller_or_equal @t2 @t1)) % 0.37/0.69 (define @t6 () (@list @t2 @t1)) % 0.37/0.69 (define @t7 () (forall @t6 (or (not @t5) @t4 @t3))) % 0.37/0.69 (define @t8 () (not @t4)) % 0.37/0.69 (define @t9 () (forall @t6 (or @t8 @t5))) % 0.37/0.69 (define @t10 () (not @t3)) % 0.37/0.69 (define @t11 () (tptp.greater @t2 @t1)) % 0.37/0.69 (define @t12 () (tptp.greater_or_equal @t2 @t1)) % 0.37/0.69 (define @t13 () (not @t11)) % 0.37/0.69 (define @t14 () (tptp.greater @t1 @t2)) % 0.37/0.69 (define @t15 () (forall @t6 (or @t13 (tptp.smaller @t1 @t2)))) % 0.37/0.69 (define @t16 () (@var "C" $$unsorted)) % 0.37/0.69 (define @t17 () (@list @t2 @t1 @t16)) % 0.37/0.69 (define @t18 () (tptp.organization @t2)) % 0.37/0.69 (define @t19 () (tptp.has_endowment @t2)) % 0.37/0.69 (define @t20 () (not @t19)) % 0.37/0.69 (define @t21 () (@list @t2)) % 0.37/0.69 (define @t22 () (tptp.has_immunity @t2 @t1)) % 0.37/0.69 (define @t23 () (tptp.age @t2 @t1)) % 0.37/0.69 (define @t24 () (not @t22)) % 0.37/0.69 (define @t25 () (tptp.sk1 @t2)) % 0.37/0.69 (define @t26 () (tptp.age @t2 @t25)) % 0.37/0.69 (define @t27 () (tptp.greater @t26 tptp.eta)) % 0.37/0.69 (define @t28 () (tptp.smaller_or_equal @t26 tptp.eta)) % 0.37/0.69 (define @t29 () (not @t18)) % 0.37/0.69 (define @t30 () (tptp.has_immunity @t2 @t25)) % 0.37/0.69 (define @t31 () (not @t30)) % 0.37/0.69 (define @t32 () (forall @t6 (or @t29 @t19 @t24))) % 0.37/0.69 (define @t33 () (tptp.dissimilar @t2 @t1 @t16)) % 0.37/0.69 (define @t34 () (not @t33)) % 0.37/0.69 (define @t35 () (tptp.is_aligned @t2 @t16)) % 0.37/0.69 (define @t36 () (tptp.is_aligned @t2 @t1)) % 0.37/0.69 (define @t37 () (not @t36)) % 0.37/0.69 (define @t38 () (tptp.dissimilar @t2 @t16 @t1)) % 0.37/0.69 (define @t39 () (not (= @t23 tptp.zero))) % 0.37/0.69 (define @t40 () (forall @t6 (or @t29 @t39 @t36))) % 0.37/0.69 (define @t41 () (tptp.greater (tptp.age @t2 @t16) tptp.sigma)) % 0.37/0.69 (define @t42 () (forall @t17 (or @t29 @t39 (not @t41) @t33))) % 0.37/0.69 (define @t43 () (forall @t17 (or @t29 @t39 @t34 @t41))) % 0.37/0.69 (define @t44 () (tptp.positional_advantage @t2 @t1)) % 0.37/0.69 (define @t45 () (not @t44)) % 0.37/0.69 (define @t46 () (tptp.robust_position @t2)) % 0.37/0.69 (define @t47 () (not @t46)) % 0.37/0.69 (define @t48 () (forall @t6 (or @t47 (not (tptp.smaller_or_equal @t23 tptp.tau)) @t45))) % 0.37/0.69 (define @t49 () (tptp.sk2 @t2)) % 0.37/0.69 (define @t50 () (tptp.age @t2 @t49)) % 0.37/0.69 (define @t51 () (tptp.greater @t50 tptp.tau)) % 0.37/0.69 (define @t52 () (tptp.smaller_or_equal @t50 tptp.tau)) % 0.37/0.69 (define @t53 () (tptp.positional_advantage @t2 @t49)) % 0.37/0.69 (define @t54 () (not @t53)) % 0.37/0.69 (define @t55 () (tptp.hazard_of_mortality @t2 @t1)) % 0.37/0.69 (define @t56 () (forall @t6 (or @t29 @t22 @t37 @t45 (= @t55 tptp.low)))) % 0.37/0.69 (define @t57 () (forall @t6 (or @t29 @t22 @t36 @t45 (= @t55 tptp.mod1)))) % 0.37/0.69 (define @t58 () (forall @t6 (or @t29 @t22 @t37 @t44 (= @t55 tptp.mod2)))) % 0.37/0.69 (define @t59 () (tptp.greater tptp.mod1 tptp.low)) % 0.37/0.69 (define @t60 () (tptp.greater tptp.mod2 tptp.mod1)) % 0.37/0.69 (define @t61 () (tptp.organization tptp.sk3)) % 0.37/0.69 (define @t62 () (tptp.robust_position tptp.sk3)) % 0.37/0.69 (define @t63 () (tptp.has_endowment tptp.sk3)) % 0.37/0.69 (define @t64 () (tptp.age tptp.sk3 tptp.sk4)) % 0.37/0.69 (define @t65 () (= @t64 tptp.zero)) % 0.37/0.69 (define @t66 () (tptp.greater tptp.tau tptp.zero)) % 0.37/0.69 (define @t67 () (tptp.greater tptp.sigma tptp.tau)) % 0.37/0.69 (define @t68 () (tptp.age tptp.sk3 tptp.sk5)) % 0.37/0.69 (define @t69 () (tptp.smaller_or_equal @t68 tptp.tau)) % 0.37/0.69 (define @t70 () (tptp.age tptp.sk3 tptp.sk6)) % 0.37/0.69 (define @t71 () (tptp.greater @t70 tptp.tau)) % 0.37/0.69 (define @t72 () (tptp.smaller_or_equal @t70 tptp.sigma)) % 0.37/0.69 (define @t73 () (tptp.age tptp.sk3 tptp.sk7)) % 0.37/0.69 (define @t74 () (tptp.greater @t73 tptp.sigma)) % 0.37/0.69 (define @t75 () (tptp.hazard_of_mortality tptp.sk3 tptp.sk4)) % 0.37/0.69 (define @t76 () (tptp.hazard_of_mortality tptp.sk3 tptp.sk5)) % 0.37/0.69 (define @t77 () (= @t76 @t75)) % 0.37/0.69 (define @t78 () (tptp.hazard_of_mortality tptp.sk3 tptp.sk7)) % 0.37/0.69 (define @t79 () (tptp.smaller @t78 @t76)) % 0.37/0.69 (define @t80 () (tptp.hazard_of_mortality tptp.sk3 tptp.sk6)) % 0.37/0.69 (define @t81 () (tptp.smaller @t80 @t78)) % 0.37/0.69 (define @t82 () (tptp.greater @t68 tptp.sigma)) % 0.37/0.69 (define @t83 () (tptp.dissimilar tptp.sk3 tptp.sk4 tptp.sk5)) % 0.37/0.69 (define @t84 () (not @t83)) % 0.37/0.69 (define @t85 () (not @t65)) % 0.37/0.69 (define @t86 () (not @t61)) % 0.37/0.69 (define @t87 () (or @t86 @t85 @t84 @t82)) % 0.37/0.69 (define @t88 () (@list tptp.sk3 tptp.sk4 tptp.sk5)) % 0.37/0.69 (define @t89 () (= tptp.zero @t64)) % 0.37/0.69 (define @t90 () (not @t89)) % 0.37/0.69 (define @t91 () (or @t86 @t90 @t84 @t82)) % 0.37/0.69 (define @t92 () (@list false)) % 0.37/0.69 (define @t93 () (@list @t43)) % 0.37/0.69 (define @t94 () (tptp.is_aligned tptp.sk3 tptp.sk4)) % 0.37/0.69 (define @t95 () (or @t86 @t85 @t94)) % 0.37/0.69 (define @t96 () (@list tptp.sk3 tptp.sk4)) % 0.37/0.69 (define @t97 () (or @t86 @t90 @t94)) % 0.37/0.69 (define @t98 () (@list false false false)) % 0.37/0.69 (define @t99 () (tptp.positional_advantage tptp.sk3 tptp.sk5)) % 0.37/0.69 (define @t100 () (tptp.is_aligned tptp.sk3 tptp.sk5)) % 0.37/0.69 (define @t101 () (not @t100)) % 0.37/0.69 (define @t102 () (tptp.has_immunity tptp.sk3 tptp.sk5)) % 0.37/0.69 (define @t103 () (or @t86 @t102 @t101 @t99 (= @t76 tptp.mod2))) % 0.37/0.69 (define @t104 () (@list tptp.sk3 tptp.sk5)) % 0.37/0.69 (define @t105 () (= tptp.mod2 @t76)) % 0.37/0.70 (define @t106 () (or @t86 @t102 @t101 @t99 @t105)) % 0.37/0.70 (define @t107 () (tptp.positional_advantage tptp.sk3 tptp.sk7)) % 0.37/0.70 (define @t108 () (not @t107)) % 0.37/0.70 (define @t109 () (tptp.is_aligned tptp.sk3 tptp.sk7)) % 0.37/0.70 (define @t110 () (tptp.has_immunity tptp.sk3 tptp.sk7)) % 0.37/0.70 (define @t111 () (or @t86 @t110 @t109 @t108 (= @t78 tptp.mod1))) % 0.37/0.70 (define @t112 () (@list tptp.sk3 tptp.sk7)) % 0.37/0.70 (define @t113 () (= tptp.mod1 @t78)) % 0.37/0.70 (define @t114 () (or @t86 @t110 @t109 @t108 @t113)) % 0.37/0.70 (define @t115 () (not @t110)) % 0.37/0.70 (define @t116 () (or @t86 @t63 @t115)) % 0.37/0.70 (define @t117 () (@list true false false)) % 0.37/0.70 (define @t118 () (tptp.greater @t73 tptp.tau)) % 0.37/0.70 (define @t119 () (not @t67)) % 0.37/0.70 (define @t120 () (not @t74)) % 0.37/0.70 (define @t121 () (or @t120 @t119 @t118)) % 0.37/0.70 (define @t122 () (not @t118)) % 0.37/0.70 (define @t123 () (not @t62)) % 0.37/0.70 (define @t124 () (or @t123 @t122 @t107)) % 0.37/0.70 (define @t125 () (@list tptp.sk3 tptp.sk4 tptp.sk7)) % 0.37/0.70 (define @t126 () (tptp.dissimilar tptp.sk3 tptp.sk4 tptp.sk7)) % 0.37/0.70 (define @t127 () (or @t86 @t85 @t120 @t126)) % 0.37/0.70 (define @t128 () (or @t86 @t90 @t120 @t126)) % 0.37/0.70 (define @t129 () (@list false false false false)) % 0.37/0.70 (define @t130 () (not @t109)) % 0.37/0.70 (define @t131 () (not @t94)) % 0.37/0.70 (define @t132 () (not @t126)) % 0.37/0.70 (define @t133 () (or @t132 @t131 @t130)) % 0.37/0.70 (define @t134 () (tptp.smaller_or_equal tptp.zero tptp.tau)) % 0.37/0.70 (define @t135 () (tptp.smaller tptp.zero tptp.tau)) % 0.37/0.70 (define @t136 () (not @t135)) % 0.37/0.70 (define @t137 () (or @t136 @t134)) % 0.37/0.70 (define @t138 () (not @t66)) % 0.37/0.70 (define @t139 () (or @t138 @t135)) % 0.37/0.70 (define @t140 () (tptp.smaller_or_equal @t64 tptp.tau)) % 0.37/0.70 (define @t141 () (and @t89 @t134)) % 0.37/0.70 (define @t142 () (tptp.positional_advantage tptp.sk3 tptp.sk4)) % 0.37/0.70 (define @t143 () (not @t142)) % 0.37/0.70 (define @t144 () (not @t140)) % 0.37/0.70 (define @t145 () (or @t123 @t144 @t143)) % 0.37/0.70 (define @t146 () (tptp.has_immunity tptp.sk3 tptp.sk4)) % 0.37/0.70 (define @t147 () (not @t146)) % 0.37/0.70 (define @t148 () (or @t86 @t63 @t147)) % 0.37/0.70 (define @t149 () (or @t86 @t146 @t131 @t142 (= @t75 tptp.mod2))) % 0.37/0.70 (define @t150 () (= tptp.mod2 @t75)) % 0.37/0.70 (define @t151 () (or @t86 @t146 @t131 @t142 @t150)) % 0.37/0.70 (define @t152 () (and @t105 @t150)) % 0.37/0.70 (define @t153 () (not @t105)) % 0.37/0.70 (define @t154 () (tptp.positional_advantage tptp.sk3 tptp.sk6)) % 0.37/0.70 (define @t155 () (not @t154)) % 0.37/0.70 (define @t156 () (tptp.is_aligned tptp.sk3 tptp.sk6)) % 0.37/0.70 (define @t157 () (not @t156)) % 0.37/0.70 (define @t158 () (tptp.has_immunity tptp.sk3 tptp.sk6)) % 0.37/0.70 (define @t159 () (or @t86 @t158 @t157 @t155 (= @t80 tptp.low))) % 0.37/0.70 (define @t160 () (@list tptp.sk3 tptp.sk6)) % 0.37/0.70 (define @t161 () (= tptp.low @t80)) % 0.37/0.70 (define @t162 () (or @t86 @t158 @t157 @t155 @t161)) % 0.37/0.70 (define @t163 () (@list tptp.sk3 tptp.sk4 tptp.sk6)) % 0.37/0.70 (define @t164 () (tptp.greater @t70 tptp.sigma)) % 0.37/0.70 (define @t165 () (tptp.dissimilar tptp.sk3 tptp.sk4 tptp.sk6)) % 0.37/0.70 (define @t166 () (not @t165)) % 0.37/0.70 (define @t167 () (or @t86 @t85 @t166 @t164)) % 0.37/0.70 (define @t168 () (or @t86 @t90 @t166 @t164)) % 0.37/0.70 (define @t169 () (tptp.smaller @t70 tptp.sigma)) % 0.37/0.70 (define @t170 () (not @t72)) % 0.37/0.70 (define @t171 () (or @t170 @t169 (= @t70 tptp.sigma))) % 0.37/0.70 (define @t172 () (@list @t70 tptp.sigma)) % 0.37/0.70 (define @t173 () (= tptp.sigma @t70)) % 0.37/0.70 (define @t174 () (or @t170 @t169 @t173)) % 0.37/0.70 (define @t175 () (@list @t7)) % 0.37/0.70 (define @t176 () (@list tptp.sigma @t70)) % 0.37/0.70 (define @t177 () (tptp.greater tptp.sigma @t70)) % 0.37/0.70 (define @t178 () (not @t177)) % 0.37/0.70 (define @t179 () (or @t178 @t169)) % 0.37/0.70 (define @t180 () (and @t173 @t164)) % 0.37/0.70 (define @t181 () (not @t164)) % 0.37/0.70 (define @t182 () (or @t178 @t181)) % 0.37/0.70 (define @t183 () (not @t169)) % 0.37/0.70 (define @t184 () (or @t183 @t177)) % 0.37/0.70 (define @t185 () (@list false true false false)) % 0.37/0.70 (define @t186 () (@list false false true false)) % 0.37/0.70 (define @t187 () (or @t86 @t131 @t156 @t165)) % 0.37/0.70 (define @t188 () (not @t158)) % 0.37/0.70 (define @t189 () (or @t86 @t63 @t188)) % 0.37/0.70 (define @t190 () (not @t71)) % 0.37/0.70 (define @t191 () (or @t123 @t190 @t154)) % 0.37/0.70 (define @t192 () (not @t113)) % 0.37/0.70 (define @t193 () (not @t161)) % 0.37/0.70 (define @t194 () (tptp.greater @t78 @t80)) % 0.37/0.70 (define @t195 () (not @t59)) % 0.37/0.70 (define @t196 () (not @t194)) % 0.37/0.70 (define @t197 () (= false true)) % 0.37/0.70 (define @t198 () (and @t59 @t113 @t161 @t196)) % 0.37/0.70 (define @t199 () (or @t196 @t81)) % 0.37/0.70 (define @t200 () (tptp.greater @t76 @t78)) % 0.37/0.70 (define @t201 () (not @t200)) % 0.37/0.70 (define @t202 () (or @t201 @t79)) % 0.37/0.70 (define @t203 () (and @t60 @t113 @t105)) % 0.37/0.70 (define @t204 () (not @t102)) % 0.37/0.70 (define @t205 () (or @t86 @t63 @t204)) % 0.37/0.70 (define @t206 () (not @t99)) % 0.37/0.70 (define @t207 () (not @t69)) % 0.37/0.70 (define @t208 () (or @t123 @t207 @t206)) % 0.37/0.70 (define @t209 () (or @t86 @t131 @t100 @t83)) % 0.37/0.70 (define @t210 () (not @t82)) % 0.37/0.70 (define @t211 () (tptp.greater tptp.sigma @t68)) % 0.37/0.70 (define @t212 () (not @t211)) % 0.37/0.70 (define @t213 () (or @t212 @t210)) % 0.37/0.70 (define @t214 () (tptp.smaller @t68 tptp.tau)) % 0.37/0.70 (define @t215 () (or @t207 @t214 (= @t68 tptp.tau))) % 0.37/0.70 (define @t216 () (@list @t68 tptp.tau)) % 0.37/0.70 (define @t217 () (= tptp.tau @t68)) % 0.37/0.70 (define @t218 () (or @t207 @t214 @t217)) % 0.37/0.70 (define @t219 () (tptp.greater tptp.tau @t68)) % 0.37/0.70 (define @t220 () (not @t219)) % 0.37/0.70 (define @t221 () (or @t119 @t220 @t211)) % 0.37/0.70 (define @t222 () (@list false true false)) % 0.37/0.70 (define @t223 () (not @t214)) % 0.37/0.70 (define @t224 () (or @t223 @t219)) % 0.37/0.70 (define @t225 () (not @t217)) % 0.37/0.70 (assume @p1 @t7) % 0.37/0.70 (assume @p2 @t9) % 0.37/0.70 (assume @p3 (forall @t6 (or @t10 @t5))) % 0.37/0.70 (assume @p4 (forall @t6 (or (not @t12) @t11 @t3))) % 0.37/0.70 (assume @p5 (forall @t6 (or @t13 @t12))) % 0.37/0.70 (assume @p6 (forall @t6 (or @t10 @t12))) % 0.37/0.70 (assume @p7 (forall @t6 (or @t8 @t14))) % 0.37/0.70 (assume @p8 @t15) % 0.37/0.70 (assume @p9 (forall @t6 (or @t13 (not @t14)))) % 0.37/0.70 (assume @p10 (forall @t17 (or @t13 (not (tptp.greater @t1 @t16)) (tptp.greater @t2 @t16)))) % 0.37/0.70 (assume @p11 (forall @t6 (or @t4 @t3 @t11))) % 0.37/0.70 (assume @p12 (forall @t21 (or @t20 @t18))) % 0.37/0.70 (assume @p13 (forall @t6 (or @t20 (not (tptp.smaller_or_equal @t23 tptp.eta)) @t22))) % 0.37/0.70 (assume @p14 (forall @t6 (or @t20 (not (tptp.greater @t23 tptp.eta)) @t24))) % 0.37/0.70 (assume @p15 (forall @t21 (or @t29 @t28 @t27 @t19))) % 0.37/0.70 (assume @p16 (forall @t21 (or @t29 @t28 @t30 @t19))) % 0.37/0.70 (assume @p17 (forall @t21 (or @t29 @t31 @t27 @t19))) % 0.37/0.70 (assume @p18 (forall @t21 (or @t29 @t31 @t30 @t19))) % 0.37/0.70 (assume @p19 @t32) % 0.37/0.70 (assume @p20 (forall @t17 (or @t34 @t18))) % 0.37/0.70 (assume @p21 (forall @t17 (or @t34 @t36 @t35))) % 0.37/0.70 (assume @p22 (forall @t17 (or @t34 @t37 (not @t35)))) % 0.37/0.70 (assume @p23 (forall @t17 (or @t29 @t37 @t36 @t33))) % 0.37/0.70 (assume @p24 (forall @t17 (or @t29 @t37 @t35 @t33))) % 0.37/0.70 (assume @p25 (forall @t17 (or @t29 @t37 @t35 @t38))) % 0.37/0.70 (assume @p26 (forall @t17 (or @t29 @t37 @t36 @t38))) % 0.37/0.70 (assume @p27 @t40) % 0.37/0.70 (assume @p28 @t42) % 0.37/0.70 (assume @p29 @t43) % 0.37/0.70 (assume @p30 @t48) % 0.37/0.70 (assume @p31 (forall @t6 (or @t47 (not (tptp.greater @t23 tptp.tau)) @t44))) % 0.37/0.70 (assume @p32 (forall @t21 (or @t52 @t51 @t46))) % 0.37/0.70 (assume @p33 (forall @t21 (or @t52 @t54 @t46))) % 0.37/0.70 (assume @p34 (forall @t21 (or @t53 @t51 @t46))) % 0.37/0.70 (assume @p35 (forall @t21 (or @t53 @t54 @t46))) % 0.37/0.70 (assume @p36 (forall @t6 (or @t29 @t24 (= @t55 tptp.very_low)))) % 0.37/0.70 (assume @p37 @t56) % 0.37/0.70 (assume @p38 @t57) % 0.37/0.70 (assume @p39 @t58) % 0.37/0.70 (assume @p40 (forall @t6 (or @t29 @t22 @t36 @t44 (= @t55 tptp.high)))) % 0.37/0.70 (assume @p41 (tptp.greater tptp.high tptp.mod1)) % 0.37/0.70 (assume @p42 @t59) % 0.37/0.70 (assume @p43 (tptp.greater tptp.low tptp.very_low)) % 0.37/0.70 (assume @p44 (tptp.greater tptp.high tptp.mod2)) % 0.37/0.70 (assume @p45 (tptp.greater tptp.mod2 tptp.low)) % 0.37/0.70 (assume @p46 @t60) % 0.37/0.70 (assume @p47 @t61) % 0.37/0.70 (assume @p48 @t62) % 0.37/0.70 (assume @p49 (not @t63)) % 0.37/0.70 (assume @p50 @t65) % 0.37/0.70 (assume @p51 (tptp.greater tptp.sigma tptp.zero)) % 0.37/0.70 (assume @p52 @t66) % 0.37/0.70 (assume @p53 @t67) % 0.37/0.70 (assume @p54 @t69) % 0.37/0.70 (assume @p55 @t71) % 0.37/0.70 (assume @p56 @t72) % 0.37/0.70 (assume @p57 @t74) % 0.37/0.70 (assume @p58 (or (not @t81) (not @t79) (not @t77))) % 0.37/0.70 (step @p59 :rule instantiate :premises (@p9) :args ((@list tptp.sigma @t68))) % 0.37/0.70 (step @p60 :rule refl :args (@t82)) % 0.37/0.70 (step @p61 :rule refl :args (@t84)) % 0.37/0.70 (step @p62 :rule eq-symm :args (@t64 tptp.zero)) % 0.37/0.70 (step @p63 :rule cong :premises (@p62) :args (@t85)) % 0.37/0.70 (step @p64 :rule refl :args (@t86)) % 0.37/0.70 (step @p65 :rule nary_cong :premises (@p64 @p63 @p61 @p60) :args (@t87)) % 0.37/0.70 (step @p66 :rule refl :args (@t43)) % 0.37/0.70 (step @p67 :rule cong :premises (@p66 @p65) :args ((=> @t43 @t87))) % 0.37/0.70 (assume-push @p459 @t43) % 0.37/0.70 (step @p69 :rule instantiate :premises (@p29) :args (@t88)) % 0.37/0.70 (step-pop @p460 :rule scope :premises (@p69)) % 0.37/0.70 (step @p70 :rule process_scope :premises (@p460) :args (@t87)) % 0.37/0.70 (step @p72 :rule eq_resolve :premises (@p70 @p67)) % 0.37/0.70 (step @p73 :rule implies_elim :premises (@p72)) % 0.37/0.70 (step @p74 :rule chain_m_resolution :premises (@p73 @p29) :args (@t91 @t92 @t93)) % 0.37/0.70 (step @p75 :rule instantiate :premises (@p24) :args (@t88)) % 0.37/0.70 (step @p76 :rule refl :args (@t94)) % 0.37/0.70 (step @p77 :rule nary_cong :premises (@p64 @p63 @p76) :args (@t95)) % 0.37/0.70 (step @p78 :rule refl :args (@t40)) % 0.37/0.70 (step @p79 :rule cong :premises (@p78 @p77) :args ((=> @t40 @t95))) % 0.37/0.70 (assume-push @p461 @t40) % 0.37/0.70 (step @p81 :rule instantiate :premises (@p27) :args (@t96)) % 0.37/0.70 (step-pop @p462 :rule scope :premises (@p81)) % 0.37/0.70 (step @p82 :rule process_scope :premises (@p462) :args (@t95)) % 0.37/0.70 (step @p84 :rule eq_resolve :premises (@p82 @p79)) % 0.37/0.70 (step @p85 :rule implies_elim :premises (@p84)) % 0.37/0.70 (step @p86 :rule chain_m_resolution :premises (@p85 @p27) :args (@t97 @t92 (@list @t40))) % 0.37/0.70 (step @p87 :rule symm :premises (@p50)) % 0.37/0.70 (step @p88 :rule cnf_or_pos :args (@t97)) % 0.37/0.70 (step @p89 :rule reordering :premises (@p88) :args ((or @t86 @t90 @t94 (not @t97)))) % 0.37/0.70 (step @p90 :rule chain_m_resolution :premises (@p89 @p47 @p87 @p86) :args (@t94 @t98 (@list @t61 @t89 @t97))) % 0.37/0.70 (step @p91 :rule eq-symm :args (@t76 tptp.mod2)) % 0.37/0.70 (step @p92 :rule refl :args (@t99)) % 0.37/0.70 (step @p93 :rule refl :args (@t101)) % 0.37/0.70 (step @p94 :rule refl :args (@t102)) % 0.37/0.70 (step @p95 :rule nary_cong :premises (@p64 @p94 @p93 @p92 @p91) :args (@t103)) % 0.37/0.70 (step @p96 :rule refl :args (@t58)) % 0.37/0.70 (step @p97 :rule cong :premises (@p96 @p95) :args ((=> @t58 @t103))) % 0.37/0.70 (assume-push @p463 @t58) % 0.37/0.70 (step @p99 :rule instantiate :premises (@p39) :args (@t104)) % 0.37/0.70 (step-pop @p464 :rule scope :premises (@p99)) % 0.37/0.70 (step @p100 :rule process_scope :premises (@p464) :args (@t103)) % 0.37/0.70 (step @p102 :rule eq_resolve :premises (@p100 @p97)) % 0.37/0.70 (step @p103 :rule implies_elim :premises (@p102)) % 0.37/0.70 (step @p104 :rule chain_m_resolution :premises (@p103 @p39) :args (@t106 @t92 (@list @t58))) % 0.37/0.70 (step @p105 :rule eq-symm :args (@t78 tptp.mod1)) % 0.37/0.70 (step @p106 :rule refl :args (@t108)) % 0.37/0.70 (step @p107 :rule refl :args (@t109)) % 0.37/0.70 (step @p108 :rule refl :args (@t110)) % 0.37/0.70 (step @p109 :rule nary_cong :premises (@p64 @p108 @p107 @p106 @p105) :args (@t111)) % 0.37/0.70 (step @p110 :rule refl :args (@t57)) % 0.37/0.70 (step @p111 :rule cong :premises (@p110 @p109) :args ((=> @t57 @t111))) % 0.37/0.70 (assume-push @p465 @t57) % 0.37/0.70 (step @p113 :rule instantiate :premises (@p38) :args (@t112)) % 0.37/0.70 (step-pop @p466 :rule scope :premises (@p113)) % 0.37/0.70 (step @p114 :rule process_scope :premises (@p466) :args (@t111)) % 0.37/0.70 (step @p116 :rule eq_resolve :premises (@p114 @p111)) % 0.37/0.70 (step @p117 :rule implies_elim :premises (@p116)) % 0.37/0.70 (step @p118 :rule chain_m_resolution :premises (@p117 @p38) :args (@t114 @t92 (@list @t57))) % 0.37/0.70 (step @p119 :rule instantiate :premises (@p19) :args (@t112)) % 0.37/0.70 (step @p120 :rule cnf_or_pos :args (@t116)) % 0.37/0.70 (step @p121 :rule reordering :premises (@p120) :args ((or @t63 @t86 @t115 (not @t116)))) % 0.37/0.70 (step @p122 :rule chain_m_resolution :premises (@p121 @p49 @p47 @p119) :args (@t115 @t117 (@list @t63 @t61 @t116))) % 0.37/0.70 (step @p123 :rule instantiate :premises (@p31) :args (@t112)) % 0.37/0.70 (step @p124 :rule instantiate :premises (@p10) :args ((@list @t73 tptp.sigma tptp.tau))) % 0.37/0.70 (step @p125 :rule cnf_or_pos :args (@t121)) % 0.37/0.70 (step @p126 :rule reordering :premises (@p125) :args ((or @t119 @t120 @t118 (not @t121)))) % 0.37/0.70 (step @p127 :rule chain_m_resolution :premises (@p126 @p53 @p57 @p124) :args (@t118 @t98 (@list @t67 @t74 @t121))) % 0.37/0.70 (step @p128 :rule cnf_or_pos :args (@t124)) % 0.37/0.70 (step @p129 :rule reordering :premises (@p128) :args ((or @t123 @t107 @t122 (not @t124)))) % 0.37/0.70 (step @p130 :rule chain_m_resolution :premises (@p129 @p48 @p127 @p123) :args (@t107 @t98 (@list @t62 @t118 @t124))) % 0.37/0.70 (step @p131 :rule instantiate :premises (@p22) :args (@t125)) % 0.37/0.70 (step @p132 :rule refl :args (@t126)) % 0.37/0.70 (step @p133 :rule refl :args (@t120)) % 0.37/0.70 (step @p134 :rule nary_cong :premises (@p64 @p63 @p133 @p132) :args (@t127)) % 0.37/0.70 (step @p135 :rule refl :args (@t42)) % 0.37/0.70 (step @p136 :rule cong :premises (@p135 @p134) :args ((=> @t42 @t127))) % 0.37/0.70 (assume-push @p467 @t42) % 0.37/0.70 (step @p138 :rule instantiate :premises (@p28) :args (@t125)) % 0.37/0.70 (step-pop @p468 :rule scope :premises (@p138)) % 0.37/0.70 (step @p139 :rule process_scope :premises (@p468) :args (@t127)) % 0.37/0.70 (step @p141 :rule eq_resolve :premises (@p139 @p136)) % 0.37/0.70 (step @p142 :rule implies_elim :premises (@p141)) % 0.37/0.70 (step @p143 :rule chain_m_resolution :premises (@p142 @p28) :args (@t128 @t92 (@list @t42))) % 0.37/0.70 (step @p144 :rule cnf_or_pos :args (@t128)) % 0.37/0.70 (step @p145 :rule reordering :premises (@p144) :args ((or @t86 @t90 @t120 @t126 (not @t128)))) % 0.37/0.70 (step @p146 :rule chain_m_resolution :premises (@p145 @p47 @p87 @p57 @p143) :args (@t126 @t129 (@list @t61 @t89 @t74 @t128))) % 0.37/0.70 (step @p147 :rule cnf_or_pos :args (@t133)) % 0.37/0.70 (step @p148 :rule reordering :premises (@p147) :args ((or @t130 @t131 @t132 (not @t133)))) % 0.37/0.70 (step @p149 :rule chain_m_resolution :premises (@p148 @p90 @p146 @p131) :args (@t130 @t98 (@list @t94 @t126 @t133))) % 0.37/0.70 (step @p150 :rule cnf_or_pos :args (@t114)) % 0.37/0.70 (step @p151 :rule reordering :premises (@p150) :args ((or @t86 @t109 @t108 @t110 @t113 (not @t114)))) % 0.37/0.70 (step @p152 :rule chain_m_resolution :premises (@p151 @p47 @p149 @p130 @p122 @p118) :args (@t113 (@list false true false true false) (@list @t61 @t109 @t107 @t110 @t114))) % 0.37/0.70 (assume-push @p469 @t9) % 0.37/0.70 (step @p154 :rule instantiate :premises (@p2) :args ((@list tptp.zero tptp.tau))) % 0.37/0.70 (step-pop @p470 :rule scope :premises (@p154)) % 0.37/0.70 (step @p155 :rule process_scope :premises (@p470) :args (@t137)) % 0.37/0.70 (step @p157 :rule implies_elim :premises (@p155)) % 0.37/0.70 (assume-push @p471 @t15) % 0.37/0.70 (step @p159 :rule instantiate :premises (@p8) :args ((@list tptp.tau tptp.zero))) % 0.37/0.70 (step-pop @p472 :rule scope :premises (@p159)) % 0.37/0.70 (step @p160 :rule process_scope :premises (@p472) :args (@t139)) % 0.37/0.70 (step @p162 :rule implies_elim :premises (@p160)) % 0.37/0.70 (step @p163 :rule cnf_or_pos :args (@t139)) % 0.37/0.70 (step @p164 :rule reordering :premises (@p163) :args ((or @t138 @t135 (not @t139)))) % 0.37/0.70 (step @p165 :rule cnf_or_pos :args (@t137)) % 0.37/0.70 (step @p166 :rule reordering :premises (@p165) :args ((or @t136 @t134 (not @t137)))) % 0.37/0.70 (assume-push @p473 @t89) % 0.37/0.70 (assume-push @p474 @t134) % 0.37/0.70 (assume-push @p475 @t134) % 0.37/0.70 (assume-push @p476 @t89) % 0.37/0.70 (step @p171 :rule true_intro :premises (@p474)) % 0.37/0.70 (step @p172 :rule refl :args (tptp.tau)) % 0.37/0.70 (step @p173 :rule cong :premises (@p50 @p172) :args (@t140)) % 0.37/0.70 (step @p174 :rule trans :premises (@p173 @p171)) % 0.37/0.70 (step @p175 :rule true_elim :premises (@p174)) % 0.37/0.70 (step-pop @p477 :rule scope :premises (@p175)) % 0.37/0.70 (step-pop @p478 :rule scope :premises (@p477)) % 0.37/0.70 (step @p176 :rule process_scope :premises (@p478) :args (@t140)) % 0.37/0.70 (step @p179 :rule and_intro :premises (@p474 @p87)) % 0.37/0.70 (step @p180 :rule modus_ponens :premises (@p179 @p176)) % 0.37/0.70 (step-pop @p479 :rule scope :premises (@p180)) % 0.37/0.70 (step-pop @p480 :rule scope :premises (@p479)) % 0.37/0.70 (step @p181 :rule process_scope :premises (@p480) :args (@t140)) % 0.37/0.70 (step @p184 :rule implies_elim :premises (@p181)) % 0.37/0.70 (step @p185 :rule cnf_and_neg :args (@t141)) % 0.37/0.70 (step @p186 :rule resolution :premises (@p185 @p184) :args (true @t141)) % 0.37/0.70 (step @p187 :rule reordering :premises (@p186) :args ((or @t90 @t140 (not @t134)))) % 0.37/0.70 (assume-push @p481 @t48) % 0.37/0.70 (step @p189 :rule instantiate :premises (@p30) :args (@t96)) % 0.37/0.70 (step-pop @p482 :rule scope :premises (@p189)) % 0.37/0.70 (step @p190 :rule process_scope :premises (@p482) :args (@t145)) % 0.37/0.70 (step @p192 :rule implies_elim :premises (@p190)) % 0.37/0.70 (step @p193 :rule cnf_or_pos :args (@t145)) % 0.37/0.70 (step @p194 :rule reordering :premises (@p193) :args ((or @t123 @t144 @t143 (not @t145)))) % 0.37/0.70 (assume-push @p483 @t32) % 0.37/0.70 (step @p196 :rule instantiate :premises (@p19) :args (@t96)) % 0.37/0.70 (step-pop @p484 :rule scope :premises (@p196)) % 0.37/0.70 (step @p197 :rule process_scope :premises (@p484) :args (@t148)) % 0.37/0.70 (step @p199 :rule implies_elim :premises (@p197)) % 0.37/0.70 (step @p200 :rule cnf_or_pos :args (@t148)) % 0.37/0.70 (step @p201 :rule reordering :premises (@p200) :args ((or @t63 @t86 @t147 (not @t148)))) % 0.37/0.70 (step @p202 :rule eq-symm :args (@t75 tptp.mod2)) % 0.37/0.70 (step @p203 :rule refl :args (@t142)) % 0.37/0.70 (step @p204 :rule refl :args (@t131)) % 0.37/0.70 (step @p205 :rule refl :args (@t146)) % 0.37/0.70 (step @p206 :rule nary_cong :premises (@p64 @p205 @p204 @p203 @p202) :args (@t149)) % 0.37/0.70 (step @p207 :rule cong :premises (@p96 @p206) :args ((=> @t58 @t149))) % 0.37/0.70 (assume-push @p485 @t58) % 0.37/0.70 (step @p209 :rule instantiate :premises (@p39) :args (@t96)) % 0.37/0.70 (step-pop @p486 :rule scope :premises (@p209)) % 0.37/0.70 (step @p210 :rule process_scope :premises (@p486) :args (@t149)) % 0.37/0.70 (step @p212 :rule eq_resolve :premises (@p210 @p207)) % 0.37/0.70 (step @p213 :rule implies_elim :premises (@p212)) % 0.37/0.70 (step @p214 :rule cnf_or_pos :args (@t151)) % 0.37/0.70 (step @p215 :rule reordering :premises (@p214) :args ((or @t86 @t142 @t146 @t131 @t150 (not @t151)))) % 0.37/0.70 (assume-push @p487 @t105) % 0.37/0.70 (assume-push @p488 @t150) % 0.37/0.70 (assume-push @p489 @t150) % 0.37/0.70 (assume-push @p490 @t105) % 0.37/0.70 (step @p220 :rule symm :premises (@p487)) % 0.37/0.70 (step @p221 :rule trans :premises (@p220 @p488)) % 0.37/0.70 (step-pop @p491 :rule scope :premises (@p221)) % 0.37/0.70 (step-pop @p492 :rule scope :premises (@p491)) % 0.37/0.70 (step @p222 :rule process_scope :premises (@p492) :args (@t77)) % 0.37/0.70 (step @p225 :rule and_intro :premises (@p488 @p487)) % 0.37/0.70 (step @p226 :rule modus_ponens :premises (@p225 @p222)) % 0.37/0.70 (step-pop @p493 :rule scope :premises (@p226)) % 0.37/0.70 (step-pop @p494 :rule scope :premises (@p493)) % 0.37/0.70 (step @p227 :rule process_scope :premises (@p494) :args (@t77)) % 0.37/0.70 (step @p230 :rule implies_elim :premises (@p227)) % 0.37/0.70 (step @p231 :rule cnf_and_neg :args (@t152)) % 0.37/0.70 (step @p232 :rule resolution :premises (@p231 @p230) :args (true @t152)) % 0.37/0.70 (step @p233 :rule reordering :premises (@p232) :args ((or @t77 @t153 (not @t150)))) % 0.37/0.70 (step @p234 :rule eq-symm :args (@t80 tptp.low)) % 0.37/0.70 (step @p235 :rule refl :args (@t155)) % 0.37/0.70 (step @p236 :rule refl :args (@t157)) % 0.37/0.70 (step @p237 :rule refl :args (@t158)) % 0.37/0.70 (step @p238 :rule nary_cong :premises (@p64 @p237 @p236 @p235 @p234) :args (@t159)) % 0.37/0.70 (step @p239 :rule refl :args (@t56)) % 0.37/0.70 (step @p240 :rule cong :premises (@p239 @p238) :args ((=> @t56 @t159))) % 0.37/0.70 (assume-push @p495 @t56) % 0.37/0.70 (step @p242 :rule instantiate :premises (@p37) :args (@t160)) % 0.37/0.70 (step-pop @p496 :rule scope :premises (@p242)) % 0.37/0.70 (step @p243 :rule process_scope :premises (@p496) :args (@t159)) % 0.37/0.70 (step @p245 :rule eq_resolve :premises (@p243 @p240)) % 0.37/0.70 (step @p246 :rule implies_elim :premises (@p245)) % 0.37/0.70 (step @p247 :rule chain_m_resolution :premises (@p246 @p37) :args (@t162 @t92 (@list @t56))) % 0.37/0.70 (step @p248 :rule instantiate :premises (@p24) :args (@t163)) % 0.37/0.70 (step @p249 :rule refl :args (@t164)) % 0.37/0.70 (step @p250 :rule refl :args (@t166)) % 0.37/0.70 (step @p251 :rule nary_cong :premises (@p64 @p63 @p250 @p249) :args (@t167)) % 0.37/0.70 (step @p252 :rule cong :premises (@p66 @p251) :args ((=> @t43 @t167))) % 0.37/0.70 (assume-push @p497 @t43) % 0.37/0.70 (step @p254 :rule instantiate :premises (@p29) :args (@t163)) % 0.37/0.70 (step-pop @p498 :rule scope :premises (@p254)) % 0.37/0.70 (step @p255 :rule process_scope :premises (@p498) :args (@t167)) % 0.20/0.70 (step @p257 :rule eq_resolve :premises (@p255 @p252)) % 0.20/0.70 (step @p258 :rule implies_elim :premises (@p257)) % 0.20/0.70 (step @p259 :rule chain_m_resolution :premises (@p258 @p29) :args (@t168 @t92 @t93)) % 0.20/0.70 (step @p260 :rule eq-symm :args (@t70 tptp.sigma)) % 0.20/0.70 (step @p261 :rule refl :args (@t169)) % 0.20/0.70 (step @p262 :rule refl :args (@t170)) % 0.20/0.70 (step @p263 :rule nary_cong :premises (@p262 @p261 @p260) :args (@t171)) % 0.20/0.70 (step @p264 :rule refl :args (@t7)) % 0.20/0.70 (step @p265 :rule cong :premises (@p264 @p263) :args ((=> @t7 @t171))) % 0.20/0.70 (assume-push @p499 @t7) % 0.20/0.70 (step @p267 :rule instantiate :premises (@p1) :args (@t172)) % 0.20/0.70 (step-pop @p500 :rule scope :premises (@p267)) % 0.20/0.70 (step @p268 :rule process_scope :premises (@p500) :args (@t171)) % 0.20/0.70 (step @p270 :rule eq_resolve :premises (@p268 @p265)) % 0.20/0.70 (step @p271 :rule implies_elim :premises (@p270)) % 0.20/0.70 (step @p272 :rule chain_m_resolution :premises (@p271 @p1) :args (@t174 @t92 @t175)) % 0.20/0.70 (step @p273 :rule cnf_or_pos :args (@t174)) % 0.20/0.70 (step @p274 :rule reordering :premises (@p273) :args ((or @t170 @t169 @t173 (not @t174)))) % 0.20/0.70 (step @p275 :rule instantiate :premises (@p8) :args (@t176)) % 0.20/0.70 (step @p276 :rule cnf_or_pos :args (@t179)) % 0.20/0.70 (step @p277 :rule reordering :premises (@p276) :args ((or @t169 @t178 (not @t179)))) % 0.20/0.70 (assume-push @p501 @t173) % 0.20/0.70 (assume-push @p502 @t164) % 0.20/0.70 (assume-push @p503 @t164) % 0.20/0.70 (assume-push @p504 @t173) % 0.20/0.70 (step @p282 :rule true_intro :premises (@p502)) % 0.20/0.70 (step @p283 :rule symm :premises (@p501)) % 0.20/0.70 (step @p284 :rule cong :premises (@p501 @p283) :args (@t177)) % 0.20/0.70 (step @p285 :rule trans :premises (@p284 @p282)) % 0.20/0.70 (step @p286 :rule true_elim :premises (@p285)) % 0.20/0.70 (step-pop @p505 :rule scope :premises (@p286)) % 0.20/0.70 (step-pop @p506 :rule scope :premises (@p505)) % 0.20/0.70 (step @p287 :rule process_scope :premises (@p506) :args (@t177)) % 0.20/0.70 (step @p290 :rule and_intro :premises (@p502 @p501)) % 0.20/0.70 (step @p291 :rule modus_ponens :premises (@p290 @p287)) % 0.20/0.70 (step-pop @p507 :rule scope :premises (@p291)) % 0.20/0.70 (step-pop @p508 :rule scope :premises (@p507)) % 0.20/0.70 (step @p292 :rule process_scope :premises (@p508) :args (@t177)) % 0.20/0.70 (step @p295 :rule implies_elim :premises (@p292)) % 0.20/0.70 (step @p296 :rule cnf_and_neg :args (@t180)) % 0.20/0.70 (step @p297 :rule resolution :premises (@p296 @p295) :args (true @t180)) % 0.20/0.70 (step @p298 :rule reordering :premises (@p297) :args ((or (not @t173) @t177 @t181))) % 0.20/0.70 (step @p299 :rule chain_m_resolution :premises (@p298 @p277 @p275 @p274 @p272 @p56) :args ((or @t169 @t181) (@list true false false false false) (@list @t177 @t179 @t173 @t174 @t72))) % 0.20/0.70 (step @p300 :rule instantiate :premises (@p9) :args (@t176)) % 0.20/0.70 (step @p301 :rule cnf_or_pos :args (@t182)) % 0.20/0.70 (step @p302 :rule reordering :premises (@p301) :args ((or @t178 @t181 (not @t182)))) % 0.20/0.70 (step @p303 :rule instantiate :premises (@p7) :args (@t172)) % 0.20/0.70 (step @p304 :rule cnf_or_pos :args (@t184)) % 0.20/0.70 (step @p305 :rule reordering :premises (@p304) :args ((or @t183 @t177 (not @t184)))) % 0.20/0.70 (step @p306 :rule chain_m_resolution :premises (@p305 @p303 @p302 @p300 @p299) :args (@t181 @t185 (@list @t184 @t177 @t182 @t169))) % 0.20/0.70 (step @p307 :rule cnf_or_pos :args (@t168)) % 0.20/0.70 (step @p308 :rule reordering :premises (@p307) :args ((or @t86 @t90 @t166 @t164 (not @t168)))) % 0.20/0.70 (step @p309 :rule chain_m_resolution :premises (@p308 @p47 @p87 @p306 @p259) :args (@t166 @t186 (@list @t61 @t89 @t164 @t168))) % 0.20/0.70 (step @p310 :rule cnf_or_pos :args (@t187)) % 0.20/0.70 (step @p311 :rule reordering :premises (@p310) :args ((or @t86 @t156 @t131 @t165 (not @t187)))) % 0.20/0.70 (step @p312 :rule chain_m_resolution :premises (@p311 @p47 @p90 @p309 @p248) :args (@t156 @t186 (@list @t61 @t94 @t165 @t187))) % 0.20/0.70 (step @p313 :rule instantiate :premises (@p19) :args (@t160)) % 0.20/0.70 (step @p314 :rule cnf_or_pos :args (@t189)) % 0.20/0.70 (step @p315 :rule reordering :premises (@p314) :args ((or @t63 @t86 @t188 (not @t189)))) % 0.20/0.70 (step @p316 :rule chain_m_resolution :premises (@p315 @p49 @p47 @p313) :args (@t188 @t117 (@list @t63 @t61 @t189))) % 0.20/0.70 (step @p317 :rule instantiate :premises (@p31) :args (@t160)) % 0.20/0.70 (step @p318 :rule cnf_or_pos :args (@t191)) % 0.20/0.70 (step @p319 :rule reordering :premises (@p318) :args ((or @t123 @t190 @t154 (not @t191)))) % 0.20/0.70 (step @p320 :rule chain_m_resolution :premises (@p319 @p48 @p55 @p317) :args (@t154 @t98 (@list @t62 @t71 @t191))) % 0.20/0.70 (step @p321 :rule cnf_or_pos :args (@t162)) % 0.20/0.70 (step @p322 :rule reordering :premises (@p321) :args ((or @t86 @t155 @t158 @t157 @t161 (not @t162)))) % 0.20/0.70 (step @p323 :rule chain_m_resolution :premises (@p322 @p47 @p320 @p316 @p312 @p247) :args (@t161 (@list false false true false false) (@list @t61 @t154 @t158 @t156 @t162))) % 0.20/0.70 (step @p324 :rule refl :args (@t192)) % 0.20/0.70 (step @p325 :rule refl :args (@t193)) % 0.20/0.70 (step @p326 :rule bool-double-not-elim :args (@t194)) % 0.20/0.70 (step @p327 :rule refl :args (@t195)) % 0.20/0.70 (step @p328 :rule nary_cong :premises (@p327 @p326 @p325 @p324) :args ((or @t195 (not @t196) @t193 @t192))) % 0.20/0.70 (assume-push @p509 @t59) % 0.20/0.70 (assume-push @p510 @t113) % 0.20/0.70 (assume-push @p511 @t161) % 0.20/0.70 (assume-push @p512 @t196) % 0.20/0.70 (step @p333 :rule evaluate :args (@t197)) % 0.20/0.70 (step @p334 :rule true_intro :premises (@p42)) % 0.20/0.70 (step @p335 :rule symm :premises (@p511)) % 0.20/0.70 (step @p336 :rule symm :premises (@p152)) % 0.20/0.70 (step @p337 :rule cong :premises (@p336 @p335) :args (@t194)) % 0.20/0.70 (step @p338 :rule false_intro :premises (@p512)) % 0.20/0.70 (step @p339 :rule symm :premises (@p338)) % 0.20/0.70 (step @p340 :rule trans :premises (@p339 @p337 @p334)) % 0.20/0.70 (step @p341 false :rule eq_resolve :premises (@p340 @p333)) % 0.20/0.70 (step-pop @p513 :rule scope :premises (@p341)) % 0.20/0.70 (step-pop @p514 :rule scope :premises (@p513)) % 0.20/0.70 (step-pop @p515 :rule scope :premises (@p514)) % 0.20/0.70 (step-pop @p516 :rule scope :premises (@p515)) % 0.20/0.70 (step @p342 :rule process_scope :premises (@p516) :args (false)) % 0.20/0.70 (assume-push @p517 @t59) % 0.20/0.70 (assume-push @p518 @t196) % 0.20/0.70 (assume-push @p519 @t161) % 0.20/0.70 (assume-push @p520 @t113) % 0.20/0.70 (step @p351 :rule and_intro :premises (@p42 @p152 @p519 @p518)) % 0.20/0.70 (step-pop @p521 :rule scope :premises (@p351)) % 0.20/0.70 (step-pop @p522 :rule scope :premises (@p521)) % 0.20/0.70 (step-pop @p523 :rule scope :premises (@p522)) % 0.20/0.70 (step-pop @p524 :rule scope :premises (@p523)) % 0.20/0.70 (step @p352 :rule process_scope :premises (@p524) :args (@t198)) % 0.20/0.70 (step @p357 :rule implies_elim :premises (@p352)) % 0.20/0.70 (step @p358 :rule resolution :premises (@p357 @p342) :args (true @t198)) % 0.20/0.70 (step @p359 :rule not_and :premises (@p358)) % 0.20/0.70 (step @p360 :rule eq_resolve :premises (@p359 @p328)) % 0.20/0.70 (step @p361 :rule instantiate :premises (@p8) :args ((@list @t78 @t80))) % 0.20/0.70 (step @p362 :rule cnf_or_pos :args (@t199)) % 0.20/0.70 (step @p363 :rule reordering :premises (@p362) :args ((or @t81 @t196 (not @t199)))) % 0.20/0.70 (step @p364 :rule instantiate :premises (@p8) :args ((@list @t76 @t78))) % 0.20/0.70 (step @p365 :rule cnf_or_pos :args (@t202)) % 0.20/0.70 (step @p366 :rule reordering :premises (@p365) :args ((or @t79 @t201 (not @t202)))) % 0.20/0.70 (assume-push @p525 @t60) % 0.20/0.70 (assume-push @p526 @t113) % 0.20/0.70 (assume-push @p527 @t105) % 0.20/0.70 (assume-push @p528 @t60) % 0.20/0.70 (assume-push @p529 @t105) % 0.20/0.70 (assume-push @p530 @t113) % 0.20/0.70 (step @p373 :rule true_intro :premises (@p46)) % 0.20/0.70 (step @p336 :rule symm :premises (@p152)) % 0.20/0.70 (step @p374 :rule symm :premises (@p527)) % 0.20/0.70 (step @p375 :rule cong :premises (@p374 @p336) :args (@t200)) % 0.20/0.70 (step @p376 :rule trans :premises (@p375 @p373)) % 0.20/0.70 (step @p377 :rule true_elim :premises (@p376)) % 0.20/0.70 (step-pop @p531 :rule scope :premises (@p377)) % 0.20/0.70 (step-pop @p532 :rule scope :premises (@p531)) % 0.20/0.70 (step-pop @p533 :rule scope :premises (@p532)) % 0.20/0.70 (step @p378 :rule process_scope :premises (@p533) :args (@t200)) % 0.20/0.70 (step @p382 :rule and_intro :premises (@p46 @p527 @p152)) % 0.20/0.70 (step @p383 :rule modus_ponens :premises (@p382 @p378)) % 0.20/0.70 (step-pop @p534 :rule scope :premises (@p383)) % 0.20/0.70 (step-pop @p535 :rule scope :premises (@p534)) % 0.20/0.70 (step-pop @p536 :rule scope :premises (@p535)) % 0.20/0.70 (step @p384 :rule process_scope :premises (@p536) :args (@t200)) % 0.20/0.70 (step @p388 :rule implies_elim :premises (@p384)) % 0.20/0.70 (step @p389 :rule cnf_and_neg :args (@t203)) % 0.20/0.70 (step @p390 :rule resolution :premises (@p389 @p388) :args (true @t203)) % 0.20/0.70 (step @p391 :rule reordering :premises (@p390) :args ((or (not @t60) @t200 @t192 @t153))) % 0.20/0.70 (step @p392 :rule chain_m_resolution :premises (@p391 @p46 @p366 @p364 @p58 @p363 @p361 @p360 @p323 @p42 @p233 @p215 @p213 @p39 @p201 @p49 @p199 @p19 @p89 @p47 @p85 @p27 @p194 @p48 @p192 @p30 @p187 @p87 @p166 @p164 @p52 @p162 @p8 @p157 @p2) :args ((or @t192 @t153) (@list false true false true false false false false false false false false false true true false false false false false false true false false false false false false false false false false false false) (@list @t60 @t200 @t202 @t79 @t81 @t199 @t194 @t161 @t59 @t77 @t150 @t151 @t58 @t146 @t63 @t148 @t32 @t94 @t61 @t97 @t40 @t142 @t62 @t145 @t48 @t140 @t89 @t134 @t135 @t66 @t139 @t15 @t137 @t9))) % 0.20/0.70 (step @p393 :rule chain_m_resolution :premises (@p392 @p152) :args (@t153 @t92 (@list @t113))) % 0.20/0.70 (step @p394 :rule instantiate :premises (@p19) :args (@t104)) % 0.20/0.70 (step @p395 :rule cnf_or_pos :args (@t205)) % 0.20/0.70 (step @p396 :rule reordering :premises (@p395) :args ((or @t63 @t86 @t204 (not @t205)))) % 0.20/0.70 (step @p397 :rule chain_m_resolution :premises (@p396 @p49 @p47 @p394) :args (@t204 @t117 (@list @t63 @t61 @t205))) % 0.20/0.70 (step @p398 :rule instantiate :premises (@p30) :args (@t104)) % 0.20/0.70 (step @p399 :rule cnf_or_pos :args (@t208)) % 0.20/0.70 (step @p400 :rule reordering :premises (@p399) :args ((or @t123 @t207 @t206 (not @t208)))) % 0.20/0.70 (step @p401 :rule chain_m_resolution :premises (@p400 @p48 @p54 @p398) :args (@t206 @t98 (@list @t62 @t69 @t208))) % 0.20/0.70 (step @p402 :rule cnf_or_pos :args (@t106)) % 0.20/0.70 (step @p403 :rule reordering :premises (@p402) :args ((or @t86 @t99 @t102 @t101 @t105 (not @t106)))) % 0.20/0.70 (step @p404 :rule chain_m_resolution :premises (@p403 @p47 @p401 @p397 @p393 @p104) :args (@t101 (@list false true true true false) (@list @t61 @t99 @t102 @t105 @t106))) % 0.20/0.70 (step @p405 :rule cnf_or_pos :args (@t209)) % 0.20/0.70 (step @p406 :rule reordering :premises (@p405) :args ((or @t86 @t100 @t131 @t83 (not @t209)))) % 0.20/0.70 (step @p407 :rule chain_m_resolution :premises (@p406 @p47 @p404 @p90 @p75) :args (@t83 @t185 (@list @t61 @t100 @t94 @t209))) % 0.20/0.70 (step @p408 :rule cnf_or_pos :args (@t91)) % 0.20/0.70 (step @p409 :rule reordering :premises (@p408) :args ((or @t86 @t90 @t82 @t84 (not @t91)))) % 0.20/0.70 (step @p410 :rule chain_m_resolution :premises (@p409 @p47 @p87 @p407 @p74) :args (@t82 @t129 (@list @t61 @t89 @t83 @t91))) % 0.20/0.70 (step @p411 :rule cnf_or_pos :args (@t213)) % 0.20/0.70 (step @p412 :rule reordering :premises (@p411) :args ((or @t212 @t210 (not @t213)))) % 0.20/0.70 (step @p413 :rule chain_m_resolution :premises (@p412 @p410 @p59) :args (@t212 (@list false false) (@list @t82 @t213))) % 0.20/0.70 (step @p414 :rule eq-symm :args (@t68 tptp.tau)) % 0.20/0.70 (step @p415 :rule refl :args (@t214)) % 0.20/0.70 (step @p416 :rule refl :args (@t207)) % 0.20/0.70 (step @p417 :rule nary_cong :premises (@p416 @p415 @p414) :args (@t215)) % 0.20/0.70 (step @p418 :rule cong :premises (@p264 @p417) :args ((=> @t7 @t215))) % 0.20/0.70 (assume-push @p537 @t7) % 0.20/0.70 (step @p420 :rule instantiate :premises (@p1) :args (@t216)) % 0.20/0.70 (step-pop @p538 :rule scope :premises (@p420)) % 0.20/0.70 (step @p421 :rule process_scope :premises (@p538) :args (@t215)) % 0.20/0.70 (step @p423 :rule eq_resolve :premises (@p421 @p418)) % 0.20/0.70 (step @p424 :rule implies_elim :premises (@p423)) % 0.20/0.70 (step @p425 :rule chain_m_resolution :premises (@p424 @p1) :args (@t218 @t92 @t175)) % 0.20/0.70 (step @p426 :rule instantiate :premises (@p7) :args (@t216)) % 0.20/0.70 (step @p427 :rule instantiate :premises (@p10) :args ((@list tptp.sigma tptp.tau @t68))) % 0.20/0.70 (step @p428 :rule cnf_or_pos :args (@t221)) % 0.20/0.70 (step @p429 :rule reordering :premises (@p428) :args ((or @t119 @t220 @t211 (not @t221)))) % 0.20/0.70 (step @p430 :rule chain_m_resolution :premises (@p429 @p53 @p413 @p427) :args (@t220 @t222 (@list @t67 @t211 @t221))) % 0.20/0.70 (step @p431 :rule cnf_or_pos :args (@t224)) % 0.20/0.70 (step @p432 :rule reordering :premises (@p431) :args ((or @t223 @t219 (not @t224)))) % 0.20/0.70 (step @p433 :rule chain_m_resolution :premises (@p432 @p430 @p426) :args (@t223 (@list true false) (@list @t219 @t224))) % 0.20/0.70 (step @p434 :rule cnf_or_pos :args (@t218)) % 0.20/0.70 (step @p435 :rule reordering :premises (@p434) :args ((or @t207 @t214 @t217 (not @t218)))) % 0.20/0.70 (step @p436 :rule chain_m_resolution :premises (@p435 @p54 @p433 @p425) :args (@t217 @t222 (@list @t69 @t214 @t218))) % 0.20/0.70 (step @p437 :rule bool-double-not-elim :args (@t211)) % 0.20/0.70 (step @p438 :rule refl :args (@t225)) % 0.20/0.70 (step @p439 :rule refl :args (@t119)) % 0.20/0.70 (step @p440 :rule nary_cong :premises (@p439 @p438 @p437) :args ((or @t119 @t225 (not @t212)))) % 0.20/0.70 (assume-push @p539 @t67) % 0.20/0.70 (assume-push @p540 @t217) % 0.20/0.70 (assume-push @p541 @t212) % 0.20/0.70 (step @p333 :rule evaluate :args (@t197)) % 0.20/0.70 (step @p444 :rule true_intro :premises (@p53)) % 0.20/0.70 (step @p445 :rule symm :premises (@p540)) % 0.20/0.70 (step @p446 :rule refl :args (tptp.sigma)) % 0.20/0.70 (step @p447 :rule cong :premises (@p446 @p445) :args (@t211)) % 0.20/0.70 (step @p448 :rule false_intro :premises (@p541)) % 0.20/0.70 (step @p449 :rule symm :premises (@p448)) % 0.20/0.70 (step @p450 :rule trans :premises (@p449 @p447 @p444)) % 0.20/0.70 (step @p451 false :rule eq_resolve :premises (@p450 @p333)) % 0.20/0.70 (step-pop @p542 :rule scope :premises (@p451)) % 0.20/0.70 (step-pop @p543 :rule scope :premises (@p542)) % 0.20/0.70 (step-pop @p544 :rule scope :premises (@p543)) % 0.20/0.70 (step @p452 :rule process_scope :premises (@p544) :args (false)) % 0.20/0.70 (step @p456 :rule not_and :premises (@p452)) % 0.20/0.70 (step @p457 :rule eq_resolve :premises (@p456 @p440)) % 0.20/0.70 (step @p458 false :rule chain_m_resolution :premises (@p457 @p436 @p413 @p53) :args (false @t222 (@list @t217 @t211 @t67))) % 0.20/0.70 ) % 0.20/0.70 % SZS output end Proof % 0.20/0.70 % cvc5 exiting %------------------------------------------------------------------------------