cvc5---1.3.4.THM-Prf.s

%------------------------------------------------------------------------------
% File     : cvc5---1.3.4
% Problem  : ARI664_1 : TPTP v9.2.1. Released v6.3.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM

% Computer : n021.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:08:05 AM UTC 2026

% Result   : Theorem 0.46s 0.66s
% Output   : Proof 0.46s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12  % Problem  : ARI664_1 : TPTP v9.2.1. Released v6.3.0.
% 0.13/0.14  % Command  : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.18/0.35  % Computer : n021.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 : Wed Jun  3 02:33:05 EDT 2026
% 0.18/0.35  % CPUTime  : 
% 0.32/0.50  %----Proving TF0_ARI
% 0.46/0.66  --- Run --finite-model-find --decision=internal at 45...
% 0.46/0.66  % SZS status Theorem
% 0.46/0.66  % SZS output start Proof
% 0.46/0.66  (
% 0.46/0.66  (declare-const tptp.a Int)
% 0.46/0.66  (declare-const tptp.b Int)
% 0.46/0.66  (define @t1 () (* 11 tptp.b))
% 0.46/0.66  (define @t2 () (* 5 tptp.a))
% 0.46/0.66  (define @t3 () (+ @t2 @t1))
% 0.46/0.66  (define @t4 () (= @t3 1))
% 0.46/0.66  (define @t5 () (* tptp.a tptp.b))
% 0.46/0.66  (define @t6 () (- 36))
% 0.46/0.66  (define @t7 () (>= @t6 @t5))
% 0.46/0.66  (define @t8 () (- 2))
% 0.46/0.66  (define @t9 () (<= @t8 @t5))
% 0.46/0.66  (define @t10 () (or @t9 @t7))
% 0.46/0.66  (define @t11 () (not @t10))
% 0.46/0.66  (define @t12 () (* -11 tptp.b))
% 0.46/0.66  (define @t13 () (+ 1 @t12))
% 0.46/0.66  (define @t14 () (* -1 (- @t2 @t13)))
% 0.46/0.66  (define @t15 () (= @t2 @t13))
% 0.46/0.66  (define @t16 () (* 2 tptp.b))
% 0.46/0.66  (define @t17 () (+ tptp.a @t16))
% 0.46/0.66  (define @t18 () (>= @t17 1))
% 0.46/0.66  (define @t19 () (>= tptp.b -1))
% 0.46/0.66  (define @t20 () (* -5 1))
% 0.46/0.66  (define @t21 () (* -1 -1))
% 0.46/0.66  (define @t22 () (+ @t21 1 @t20))
% 0.46/0.66  (define @t23 () (* -5 tptp.a))
% 0.46/0.66  (define @t24 () (* -10 tptp.b))
% 0.46/0.66  (define @t25 () (* -1 tptp.b))
% 0.46/0.66  (define @t26 () (+ @t25 @t24 @t1 @t2 @t23))
% 0.46/0.66  (define @t27 () (+ @t25 @t3 (* -5 @t17)))
% 0.46/0.66  (define @t28 () (< -5 0))
% 0.46/0.66  (define @t29 () (< -1 0))
% 0.46/0.66  (define @t30 () (and @t18 @t15 @t19))
% 0.46/0.66  (define @t31 () (>= tptp.b 0))
% 0.46/0.66  (define @t32 () (not @t31))
% 0.46/0.66  (define @t33 () (not @t19))
% 0.46/0.66  (define @t34 () (< tptp.b 0))
% 0.46/0.66  (define @t35 () (* -1 0))
% 0.46/0.66  (define @t36 () (+ @t35 -2))
% 0.46/0.66  (define @t37 () (+ @t25 tptp.b))
% 0.46/0.66  (define @t38 () (not @t18))
% 0.46/0.66  (define @t39 () (and @t32 @t18))
% 0.46/0.66  (define @t40 () (not @t32))
% 0.46/0.66  (define @t41 () (not @t15))
% 0.46/0.66  (define @t42 () (and @t32 @t15))
% 0.46/0.66  (define @t43 () (* tptp.b tptp.b))
% 0.46/0.66  (define @t44 () (* -2 @t43))
% 0.46/0.66  (define @t45 () (* tptp.a tptp.b))
% 0.46/0.66  (define @t46 () (* -1 @t45))
% 0.46/0.66  (define @t47 () (+ tptp.b @t46 @t44))
% 0.46/0.66  (define @t48 () (+ tptp.b @t44))
% 0.46/0.66  (define @t49 () (>= @t47 0))
% 0.46/0.66  (define @t50 () (* -2 tptp.b))
% 0.46/0.66  (define @t51 () (+ 1 @t50))
% 0.46/0.66  (define @t52 () (* -1 (+ -1 @t16)))
% 0.46/0.66  (define @t53 () (* tptp.b @t52))
% 0.46/0.66  (define @t54 () (* tptp.b tptp.a))
% 0.46/0.66  (define @t55 () (<= @t54 @t53))
% 0.46/0.66  (define @t56 () (and @t34 @t18))
% 0.46/0.66  (define @t57 () (>= tptp.a @t52))
% 0.46/0.66  (define @t58 () (and @t34 @t57))
% 0.46/0.66  (define @t59 () (* 11 @t43))
% 0.46/0.66  (define @t60 () (* 5 @t45))
% 0.46/0.66  (define @t61 () (+ @t60 @t59))
% 0.46/0.66  (define @t62 () (- tptp.b @t61))
% 0.46/0.66  (define @t63 () (* -1 @t62))
% 0.46/0.66  (define @t64 () (* -11 @t43))
% 0.46/0.66  (define @t65 () (+ tptp.b @t64))
% 0.46/0.66  (define @t66 () (= tptp.b @t61))
% 0.46/0.66  (define @t67 () (* -1 (+ -1 @t1)))
% 0.46/0.66  (define @t68 () (* tptp.b @t67))
% 0.46/0.66  (define @t69 () (* tptp.b @t2))
% 0.46/0.66  (define @t70 () (= @t69 @t68))
% 0.46/0.66  (define @t71 () (and @t34 @t15))
% 0.46/0.66  (define @t72 () (= @t2 @t67))
% 0.46/0.66  (define @t73 () (and @t34 @t72))
% 0.46/0.66  (define @t74 () (+ @t45 1))
% 0.46/0.66  (define @t75 () (>= @t45 -35))
% 0.46/0.66  (define @t76 () (<= 0 -1))
% 0.46/0.66  (define @t77 () (* -11 0))
% 0.46/0.66  (define @t78 () (* 9 1))
% 0.46/0.66  (define @t79 () (* -45 1))
% 0.46/0.66  (define @t80 () (* 2 0))
% 0.46/0.66  (define @t81 () (* -1 -35))
% 0.46/0.66  (define @t82 () (+ @t81 @t80 @t79 @t78 @t77))
% 0.46/0.66  (define @t83 () (* 22 @t43))
% 0.46/0.66  (define @t84 () (* 11 @t45))
% 0.46/0.66  (define @t85 () (+ @t12 @t84 @t83))
% 0.46/0.66  (define @t86 () (+ (* 45 tptp.a) (* 99 tptp.b)))
% 0.46/0.66  (define @t87 () (+ (* -45 tptp.a) (* -90 tptp.b)))
% 0.46/0.66  (define @t88 () (+ @t16 (* -10 @t45) (* -22 @t43)))
% 0.46/0.66  (define @t89 () (* -11 @t47))
% 0.46/0.66  (define @t90 () (* 9 @t3))
% 0.46/0.66  (define @t91 () (* -45 @t17))
% 0.46/0.66  (define @t92 () (* -5 @t45))
% 0.46/0.66  (define @t93 () (+ tptp.b @t92 @t64))
% 0.46/0.66  (define @t94 () (* 2 @t93))
% 0.46/0.66  (define @t95 () (= @t94 @t88))
% 0.46/0.66  (define @t96 () (+ @t46 @t94 @t91 @t90 @t89))
% 0.46/0.66  (define @t97 () (= @t93 0))
% 0.46/0.66  (define @t98 () (= (* 1 (- @t93 0)) (* 1 @t62)))
% 0.46/0.66  (define @t99 () (= @t97 @t66))
% 0.46/0.66  (define @t100 () (> 2 0))
% 0.46/0.66  (define @t101 () (and @t49 @t15 @t18 @t66 @t75))
% 0.46/0.66  (define @t102 () (not @t66))
% 0.46/0.66  (define @t103 () (not @t75))
% 0.46/0.66  (define @t104 () (>= tptp.a 0))
% 0.46/0.66  (define @t105 () (not @t104))
% 0.46/0.66  (define @t106 () (not @t38))
% 0.46/0.66  (define @t107 () (+ 0 1))
% 0.46/0.66  (define @t108 () (>= @t17 @t107))
% 0.46/0.66  (define @t109 () (<= @t17 0))
% 0.46/0.66  (define @t110 () (* -1/11 0/1))
% 0.46/0.66  (define @t111 () (* -2/11 1/1))
% 0.46/0.66  (define @t112 () (+ 0/1 @t111 @t110))
% 0.46/0.66  (define @t113 () (to_real tptp.a))
% 0.46/0.66  (define @t114 () (to_real @t16))
% 0.46/0.66  (define @t115 () (* -1/11 @t113))
% 0.46/0.66  (define @t116 () (+ @t115 @t114 (to_real @t50) (* -10/11 @t113) @t113))
% 0.46/0.66  (define @t117 () (to_real @t3))
% 0.46/0.66  (define @t118 () (* -2/11 @t117))
% 0.46/0.66  (define @t119 () (to_real @t17))
% 0.46/0.66  (define @t120 () (+ @t119 @t118 @t115))
% 0.46/0.66  (define @t121 () (< -1/11 0/1))
% 0.46/0.66  (define @t122 () (to_real 0))
% 0.46/0.66  (define @t123 () (>= @t113 @t122))
% 0.46/0.66  (define @t124 () (< -2/11 0/1))
% 0.46/0.66  (define @t125 () (= @t117 1/1))
% 0.46/0.66  (define @t126 () (to_real 1))
% 0.46/0.66  (define @t127 () (<= @t119 @t122))
% 0.46/0.66  (define @t128 () (= (* 1/1 (to_real (- @t17 0))) (* 1/1 (- @t119 @t122))))
% 0.46/0.66  (define @t129 () (= @t109 @t127))
% 0.46/0.66  (define @t130 () (and @t104 @t15 @t38))
% 0.46/0.66  (define @t131 () (@list false true))
% 0.46/0.66  (define @t132 () (@list @t15 @t18))
% 0.46/0.66  (define @t133 () (and @t105 @t15))
% 0.46/0.66  (define @t134 () (not @t105))
% 0.46/0.66  (define @t135 () (* tptp.a tptp.a))
% 0.46/0.66  (define @t136 () (* 5 @t135))
% 0.46/0.66  (define @t137 () (+ @t84 @t136))
% 0.46/0.66  (define @t138 () (- tptp.a @t137))
% 0.46/0.66  (define @t139 () (* -5 @t135))
% 0.46/0.66  (define @t140 () (+ tptp.a @t139))
% 0.46/0.66  (define @t141 () (= tptp.a @t137))
% 0.46/0.66  (define @t142 () (+ 1 @t23))
% 0.46/0.66  (define @t143 () (* -1 (+ -1 @t2)))
% 0.46/0.66  (define @t144 () (* tptp.a @t143))
% 0.46/0.66  (define @t145 () (* tptp.a @t1))
% 0.46/0.66  (define @t146 () (= @t145 @t144))
% 0.46/0.66  (define @t147 () (< tptp.a 0))
% 0.46/0.66  (define @t148 () (and @t147 @t15))
% 0.46/0.66  (define @t149 () (= @t1 @t143))
% 0.46/0.66  (define @t150 () (and @t147 @t149))
% 0.46/0.66  (define @t151 () (>= tptp.b 2))
% 0.46/0.66  (define @t152 () (not @t151))
% 0.46/0.66  (define @t153 () (and @t105 @t151))
% 0.46/0.66  (define @t154 () (* 2 tptp.a))
% 0.46/0.66  (define @t155 () (+ @t154 @t46))
% 0.46/0.66  (define @t156 () (- @t155 0))
% 0.46/0.66  (define @t157 () (>= @t155 0))
% 0.46/0.66  (define @t158 () (* -1 -2))
% 0.46/0.66  (define @t159 () (* tptp.a @t158))
% 0.46/0.66  (define @t160 () (<= @t5 @t159))
% 0.46/0.66  (define @t161 () (and @t147 @t151))
% 0.46/0.66  (define @t162 () (>= tptp.b @t158))
% 0.46/0.66  (define @t163 () (and @t147 @t162))
% 0.46/0.66  (define @t164 () (* 4 @t43))
% 0.46/0.66  (define @t165 () (* 4 @t45))
% 0.46/0.66  (define @t166 () (+ @t165 @t135 @t164))
% 0.46/0.66  (define @t167 () (>= @t166 1))
% 0.46/0.66  (define @t168 () (not @t157))
% 0.46/0.66  (define @t169 () (+ (* 21 @t45) @t136 @t83))
% 0.46/0.66  (define @t170 () (>= @t169 0))
% 0.46/0.66  (define @t171 () (not @t141))
% 0.46/0.66  (define @t172 () (not @t167))
% 0.46/0.66  (define @t173 () (not @t172))
% 0.46/0.66  (define @t174 () (not @t170))
% 0.46/0.66  (define @t175 () (not @t174))
% 0.46/0.66  (define @t176 () (>= @t166 @t107))
% 0.46/0.66  (define @t177 () (<= @t166 0))
% 0.46/0.66  (define @t178 () (not true))
% 0.46/0.66  (define @t179 () (* -1/55 0/1))
% 0.46/0.66  (define @t180 () (* 1/55 0/1))
% 0.46/0.66  (define @t181 () (* 12/55 0/1))
% 0.46/0.66  (define @t182 () (* 2/5 0/1))
% 0.46/0.66  (define @t183 () (* -2/55 1/1))
% 0.46/0.66  (define @t184 () (+ 0/1 @t183 @t182 @t181 @t180 @t179))
% 0.46/0.66  (define @t185 () (to_real tptp.b))
% 0.46/0.66  (define @t186 () (* -2/5 @t185))
% 0.46/0.66  (define @t187 () (to_real @t45))
% 0.46/0.66  (define @t188 () (to_real @t135))
% 0.46/0.66  (define @t189 () (to_real @t43))
% 0.46/0.66  (define @t190 () (+ (to_real @t164) (to_real @t165) (* 2/5 @t189) (* 21/55 @t187) (to_real (* -2 @t45)) (* -12/5 @t187) (* -22/5 @t189) (* 1/11 @t188) (* -12/11 @t188) @t188 (* -2/55 @t113) (* 1/55 @t187) @t186 (* -2/11 @t113) (* 2/5 @t185) (* 12/55 @t113)))
% 0.46/0.66  (define @t191 () (to_real @t155))
% 0.46/0.66  (define @t192 () (* -1/55 @t191))
% 0.46/0.66  (define @t193 () (to_real @t169))
% 0.46/0.66  (define @t194 () (* 1/55 @t193))
% 0.46/0.66  (define @t195 () (+ tptp.a (* -11 @t45) @t139))
% 0.46/0.66  (define @t196 () (to_real @t195))
% 0.46/0.66  (define @t197 () (* 12/55 @t196))
% 0.46/0.66  (define @t198 () (to_real @t93))
% 0.46/0.66  (define @t199 () (* 2/5 @t198))
% 0.46/0.66  (define @t200 () (* -2/55 @t117))
% 0.46/0.66  (define @t201 () (to_real @t166))
% 0.46/0.66  (define @t202 () (+ @t201 @t200 @t199 @t197 @t194 @t192))
% 0.46/0.66  (define @t203 () (>= @t202 @t184))
% 0.46/0.66  (define @t204 () (< -1/55 0/1))
% 0.46/0.66  (define @t205 () (>= @t191 @t122))
% 0.46/0.66  (define @t206 () (> 1/55 0/1))
% 0.46/0.66  (define @t207 () (< @t169 0))
% 0.46/0.66  (define @t208 () (< @t193 @t122))
% 0.46/0.66  (define @t209 () (> 12/55 0/1))
% 0.46/0.66  (define @t210 () (= @t195 0))
% 0.46/0.66  (define @t211 () (= @t196 0/1))
% 0.46/0.66  (define @t212 () (= (* 1 (- @t195 0)) (* 1 @t138)))
% 0.46/0.66  (define @t213 () (= @t210 @t141))
% 0.46/0.66  (define @t214 () (> 2/5 0/1))
% 0.46/0.66  (define @t215 () (= @t198 0/1))
% 0.46/0.66  (define @t216 () (< -2/55 0/1))
% 0.46/0.66  (define @t217 () (<= @t201 @t122))
% 0.46/0.66  (define @t218 () (and @t157 @t174 @t141 @t66 @t15 @t172))
% 0.46/0.66  (define @t219 () (* -2 1))
% 0.46/0.66  (define @t220 () (* -55 1))
% 0.46/0.66  (define @t221 () (* 22 0))
% 0.46/0.66  (define @t222 () (* 10 0))
% 0.46/0.66  (define @t223 () (* 21 0))
% 0.46/0.66  (define @t224 () (+ @t81 @t223 @t222 @t221 @t220 @t219))
% 0.46/0.66  (define @t225 () (+ (* -10 tptp.a) (* -22 tptp.b)))
% 0.46/0.66  (define @t226 () (* -220 @t43))
% 0.46/0.66  (define @t227 () (* -55 @t135))
% 0.46/0.66  (define @t228 () (+ (* -220 @t45) @t227 @t226))
% 0.46/0.66  (define @t229 () (* -110 @t45))
% 0.46/0.66  (define @t230 () (* 22 tptp.b))
% 0.46/0.66  (define @t231 () (+ @t230 @t229 (* -242 @t43)))
% 0.46/0.66  (define @t232 () (+ (* 10 tptp.a) @t229 (* -50 @t135)))
% 0.46/0.66  (define @t233 () (+ (* 441 @t45) (* 105 @t135) (* 462 @t43)))
% 0.46/0.66  (define @t234 () (* -2 @t3))
% 0.46/0.66  (define @t235 () (* -55 @t166))
% 0.46/0.66  (define @t236 () (* 22 @t93))
% 0.46/0.66  (define @t237 () (* 10 @t195))
% 0.46/0.66  (define @t238 () (* 21 @t169))
% 0.46/0.66  (define @t239 () (+ @t46 @t238 @t237 @t236 @t235 @t234))
% 0.46/0.66  (define @t240 () (>= @t239 @t224))
% 0.46/0.66  (define @t241 () (and @t15 @t167 @t66 @t141 @t174 @t75))
% 0.46/0.66  (define @t242 () (* -5 0))
% 0.46/0.66  (define @t243 () (* -10 0))
% 0.46/0.66  (define @t244 () (* -1 2))
% 0.46/0.66  (define @t245 () (+ @t244 @t243 @t242 1 @t242))
% 0.46/0.66  (define @t246 () (+ (* -110 @t43) (* -105 @t45) (* 50 @t45) (* 55 @t45) (* 110 @t43) (* -25 @t135) (* 25 @t135) @t25 @t1 @t2 @t24 @t23))
% 0.46/0.66  (define @t247 () (+ @t25 (* -10 @t93) (* -5 @t195) @t3 (* -5 @t169)))
% 0.46/0.66  (define @t248 () (and @t170 @t15 @t141 @t66 @t151))
% 0.46/0.66  (define @t249 () (+ tptp.a @t16 @t45 (* 2 @t43)))
% 0.46/0.66  (define @t250 () (>= @t249 -3))
% 0.46/0.66  (define @t251 () (not @t250))
% 0.46/0.66  (define @t252 () (not @t152))
% 0.46/0.66  (define @t253 () (>= 0/1 0/1))
% 0.46/0.66  (define @t254 () (to_real @t81))
% 0.46/0.66  (define @t255 () (* 1/5 1/1))
% 0.46/0.66  (define @t256 () (* -11/5 1/1))
% 0.46/0.66  (define @t257 () (to_real @t80))
% 0.46/0.66  (define @t258 () (* 11 -3))
% 0.46/0.66  (define @t259 () (to_real @t258))
% 0.46/0.66  (define @t260 () (+ @t259 @t257 @t256 @t255 @t254))
% 0.46/0.66  (define @t261 () (to_real @t46))
% 0.46/0.66  (define @t262 () (* 1/5 @t185))
% 0.46/0.66  (define @t263 () (+ (to_real (* -11 tptp.a)) (* -121/5 @t185)))
% 0.46/0.66  (define @t264 () (* 11 tptp.a))
% 0.46/0.66  (define @t265 () (+ @t264 @t230 @t84 @t83))
% 0.46/0.66  (define @t266 () (* -11/5 @t117))
% 0.46/0.66  (define @t267 () (= @t266 @t263))
% 0.46/0.66  (define @t268 () (to_real @t94))
% 0.46/0.66  (define @t269 () (* 11 @t249))
% 0.46/0.66  (define @t270 () (to_real @t269))
% 0.46/0.66  (define @t271 () (+ @t270 @t268 @t266 @t262 @t261))
% 0.46/0.66  (define @t272 () (>= @t271 @t260))
% 0.46/0.66  (define @t273 () (> 1/5 0/1))
% 0.46/0.66  (define @t274 () (<= tptp.b 1))
% 0.46/0.66  (define @t275 () (<= @t185 1/1))
% 0.46/0.66  (define @t276 () (<= @t185 @t126))
% 0.46/0.66  (define @t277 () (= (* -1/1 (to_real (- tptp.b 1))) (* -1/1 (- @t185 @t126))))
% 0.46/0.66  (define @t278 () (= @t274 @t276))
% 0.46/0.66  (define @t279 () (< -11/5 0/1))
% 0.46/0.66  (define @t280 () (= @t266 @t256))
% 0.46/0.66  (define @t281 () (> 11 0))
% 0.46/0.66  (define @t282 () (>= tptp.b 1))
% 0.46/0.66  (define @t283 () (not @t282))
% 0.46/0.66  (define @t284 () (* -1/5 1/1))
% 0.46/0.66  (define @t285 () (+ @t255 @t284 0/1))
% 0.46/0.66  (define @t286 () (+ @t262 @t114 (* -11/5 @t185) (to_real (* -1 tptp.a)) @t113))
% 0.46/0.66  (define @t287 () (* -1/5 @t117))
% 0.46/0.66  (define @t288 () (+ @t262 @t287 @t119))
% 0.46/0.66  (define @t289 () (>= @t288 @t285))
% 0.46/0.66  (define @t290 () (< -1/5 0/1))
% 0.46/0.66  (define @t291 () (< tptp.b 1))
% 0.46/0.66  (define @t292 () (< @t185 @t126))
% 0.46/0.66  (define @t293 () (* -2/5 0/1))
% 0.46/0.66  (define @t294 () (* -1/5 0/1))
% 0.46/0.66  (define @t295 () (* 2/25 1/1))
% 0.46/0.66  (define @t296 () (* -1/5 -3/1))
% 0.46/0.66  (define @t297 () (* -2/25 1/1))
% 0.46/0.66  (define @t298 () (* -1 1))
% 0.46/0.66  (define @t299 () (to_real @t298))
% 0.46/0.66  (define @t300 () (+ @t299 @t297 @t296 @t295 @t294 @t293))
% 0.46/0.66  (define @t301 () (+ @t186 (to_real (* 2 @t45)) (* 22/5 @t189)))
% 0.46/0.66  (define @t302 () (* -1/5 @t113))
% 0.46/0.66  (define @t303 () (+ @t302 (* 11/5 @t187) @t188))
% 0.46/0.66  (define @t304 () (+ (* 2/5 @t113) (* 22/25 @t185)))
% 0.46/0.66  (define @t305 () (+ @t302 @t186 (* -1/5 @t187) (* -2/5 @t189)))
% 0.46/0.66  (define @t306 () (* -2/25 @t185))
% 0.46/0.66  (define @t307 () (+ (* -4 @t45) (* -1 @t135) (* -4 @t43)))
% 0.46/0.66  (define @t308 () (* -2/5 @t198))
% 0.46/0.66  (define @t309 () (* -1/5 @t196))
% 0.46/0.66  (define @t310 () (* 2/25 @t117))
% 0.46/0.66  (define @t311 () (to_real @t249))
% 0.46/0.66  (define @t312 () (* -1/5 @t311))
% 0.46/0.66  (define @t313 () (* -1 @t166))
% 0.46/0.66  (define @t314 () (to_real @t313))
% 0.46/0.66  (define @t315 () (+ @t314 @t306 @t312 @t310 @t309 @t308))
% 0.46/0.66  (define @t316 () (< -2/5 0/1))
% 0.46/0.66  (define @t317 () (> 2/25 0/1))
% 0.46/0.66  (define @t318 () (to_real -3))
% 0.46/0.66  (define @t319 () (>= @t311 @t318))
% 0.46/0.66  (define @t320 () (< -2/25 0/1))
% 0.46/0.66  (define @t321 () (>= @t185 @t126))
% 0.46/0.66  (define @t322 () (>= @t45 -2))
% 0.46/0.66  (define @t323 () (not @t322))
% 0.46/0.66  (define @t324 () (< @t45 -2))
% 0.46/0.66  (define @t325 () (* 55 0))
% 0.46/0.66  (define @t326 () (to_real @t325))
% 0.46/0.66  (define @t327 () (* 21/5 1/1))
% 0.46/0.66  (define @t328 () (* 20 0))
% 0.46/0.66  (define @t329 () (to_real @t328))
% 0.46/0.66  (define @t330 () (* 11 0))
% 0.46/0.66  (define @t331 () (to_real @t330))
% 0.46/0.66  (define @t332 () (+ -2/1 @t331 @t329 @t256 @t327 @t326))
% 0.46/0.66  (define @t333 () (+ (* 220 @t45) (* 55 @t135) (* 220 @t43)))
% 0.46/0.66  (define @t334 () (* 21/5 @t185))
% 0.46/0.66  (define @t335 () (+ (* 20 tptp.b) (* -100 @t45) @t226))
% 0.46/0.66  (define @t336 () (+ @t264 (* -121 @t45) @t227))
% 0.46/0.66  (define @t337 () (* 55 @t166))
% 0.46/0.66  (define @t338 () (to_real @t337))
% 0.46/0.66  (define @t339 () (* 20 @t93))
% 0.46/0.66  (define @t340 () (to_real @t339))
% 0.46/0.66  (define @t341 () (* 11 @t195))
% 0.46/0.66  (define @t342 () (to_real @t341))
% 0.46/0.66  (define @t343 () (+ @t187 @t342 @t340 @t266 @t334 @t338))
% 0.46/0.66  (define @t344 () (>= @t343 @t332))
% 0.46/0.66  (define @t345 () (> 21/5 0/1))
% 0.46/0.66  (define @t346 () (to_real -2))
% 0.46/0.66  (define @t347 () (< @t187 @t346))
% 0.46/0.66  (define @t348 () (and @t172 @t152 @t15 @t66 @t141 @t323))
% 0.46/0.66  (define @t349 () (and @t282 @t15))
% 0.46/0.66  (define @t350 () (+ tptp.b @t92))
% 0.46/0.66  (define @t351 () (* tptp.b @t143))
% 0.46/0.66  (define @t352 () (* tptp.b @t1))
% 0.46/0.66  (define @t353 () (= @t352 @t351))
% 0.46/0.66  (define @t354 () (>= tptp.b @t107))
% 0.46/0.66  (define @t355 () (> tptp.b 0))
% 0.46/0.66  (define @t356 () (and @t355 @t15))
% 0.46/0.66  (define @t357 () (and @t355 @t149))
% 0.46/0.66  (assume @p1 @t4)
% 0.46/0.66  (assume @p2 @t11)
% 0.46/0.66  (assume @p3 true)
% 0.46/0.66  (step @p4 :rule arith_poly_norm :args ((= (* -1 (- @t3 1)) @t14)))
% 0.46/0.66  (step @p5 :rule arith_poly_norm_rel :premises (@p4) :args ((= @t4 @t15)))
% 0.46/0.66  (step @p6 :rule eq_resolve :premises (@p1 @p5))
% 0.46/0.66  (assume-push @p1244 @t18)
% 0.46/0.66  (assume-push @p1245 @t15)
% 0.46/0.66  (assume-push @p1246 @t19)
% 0.46/0.66  (step @p10 :rule arith-elim-lt :args (tptp.b -1))
% 0.46/0.66  (step @p11 :rule symm :premises (@p10))
% 0.46/0.66  (assume-push @p1247 @t19)
% 0.46/0.66  (step @p13 :rule evaluate :args ((<= 0 -3)))
% 0.46/0.66  (step @p14 :rule evaluate :args ((+ 1 1 -5)))
% 0.46/0.66  (step @p15 :rule evaluate :args (@t20))
% 0.46/0.66  (step @p16 :rule refl :args (1))
% 0.46/0.66  (step @p17 :rule evaluate :args (@t21))
% 0.46/0.66  (step @p18 :rule nary_cong :premises (@p17 @p16 @p15) :args (@t22))
% 0.46/0.66  (step @p19 :rule trans :premises (@p18 @p14))
% 0.46/0.66  (step @p20 :rule arith_poly_norm :args ((= @t26 0)))
% 0.46/0.66  (step @p21 :rule arith_poly_norm :args ((= @t27 @t26)))
% 0.46/0.66  (step @p22 :rule trans :premises (@p21 @p20))
% 0.46/0.66  (step @p23 :rule cong :premises (@p22 @p19) :args ((<= @t27 @t22)))
% 0.46/0.66  (step @p24 :rule trans :premises (@p23 @p13))
% 0.46/0.66  (step @p25 :rule arith_mult_neg :args (-5 @t18))
% 0.46/0.66  (step @p26 :rule evaluate :args (@t28))
% 0.46/0.66  (step @p27 :rule true_elim :premises (@p26))
% 0.46/0.66  (step @p28 :rule and_intro :premises (@p27 @p1244))
% 0.46/0.66  (step @p29 :rule modus_ponens :premises (@p28 @p25))
% 0.46/0.66  (step @p30 :rule arith_mult_neg :args (-1 @t19))
% 0.46/0.66  (step @p31 :rule evaluate :args (@t29))
% 0.46/0.66  (step @p32 :rule true_elim :premises (@p31))
% 0.46/0.66  (step @p33 :rule and_intro :premises (@p32 @p1246))
% 0.46/0.66  (step @p34 :rule modus_ponens :premises (@p33 @p30))
% 0.46/0.66  (step @p35 :rule arith_sum_ub :premises (@p34 @p1 @p29))
% 0.46/0.66  (step @p36 false :rule eq_resolve :premises (@p35 @p24))
% 0.46/0.66  (step-pop @p1248 :rule scope :premises (@p36))
% 0.46/0.66  (step @p37 :rule process_scope :premises (@p1248) :args (false))
% 0.46/0.66  (step @p39 :rule eq_resolve :premises (@p37 @p11))
% 0.46/0.66  (step @p40 :rule eq_resolve :premises (@p39 @p10))
% 0.46/0.66  (step @p41 false :rule contra :premises (@p1246 @p40))
% 0.46/0.66  (step-pop @p1249 :rule scope :premises (@p41))
% 0.46/0.66  (step-pop @p1250 :rule scope :premises (@p1249))
% 0.46/0.66  (step-pop @p1251 :rule scope :premises (@p1250))
% 0.46/0.66  (step @p42 :rule process_scope :premises (@p1251) :args (false))
% 0.46/0.66  (assume-push @p1252 @t15)
% 0.46/0.66  (assume-push @p1253 @t18)
% 0.46/0.66  (assume-push @p1254 @t19)
% 0.46/0.66  (step @p49 :rule and_intro :premises (@p1253 @p6 @p1254))
% 0.46/0.66  (step-pop @p1255 :rule scope :premises (@p49))
% 0.46/0.66  (step-pop @p1256 :rule scope :premises (@p1255))
% 0.46/0.66  (step-pop @p1257 :rule scope :premises (@p1256))
% 0.46/0.66  (step @p50 :rule process_scope :premises (@p1257) :args (@t30))
% 0.46/0.66  (step @p54 :rule implies_elim :premises (@p50))
% 0.46/0.66  (step @p55 :rule resolution :premises (@p54 @p42) :args (true @t30))
% 0.46/0.66  (step @p56 :rule not_and :premises (@p55))
% 0.46/0.66  (step @p57 :rule bool-double-not-elim :args (@t19))
% 0.46/0.66  (step @p58 :rule refl :args (@t32))
% 0.46/0.66  (step @p59 :rule nary_cong :premises (@p58 @p57) :args ((or @t32 (not @t33))))
% 0.46/0.66  (assume-push @p1258 @t31)
% 0.46/0.66  (assume-push @p1259 @t33)
% 0.46/0.66  (step @p62 :rule bool-double-not-elim :args (@t31))
% 0.46/0.66  (step @p63 :rule arith-elim-lt :args (tptp.b 0))
% 0.46/0.66  (step @p64 :rule cong :premises (@p63) :args ((not @t34)))
% 0.46/0.66  (step @p65 :rule trans :premises (@p64 @p62))
% 0.46/0.66  (step @p66 :rule symm :premises (@p65))
% 0.46/0.66  (step @p67 :rule eq_resolve :premises (@p1258 @p66))
% 0.46/0.66  (step @p68 :rule symm :premises (@p63))
% 0.46/0.66  (assume-push @p1260 @t31)
% 0.46/0.66  (step @p70 :rule evaluate :args ((<= 0 -2)))
% 0.46/0.66  (step @p71 :rule evaluate :args ((+ 0 -2)))
% 0.46/0.66  (step @p72 :rule refl :args (-2))
% 0.46/0.66  (step @p73 :rule evaluate :args (@t35))
% 0.46/0.66  (step @p74 :rule nary_cong :premises (@p73 @p72) :args (@t36))
% 0.46/0.66  (step @p75 :rule trans :premises (@p74 @p71))
% 0.46/0.66  (step @p76 :rule arith_poly_norm :args ((= @t37 0)))
% 0.46/0.66  (step @p77 :rule cong :premises (@p76 @p75) :args ((<= @t37 @t36)))
% 0.46/0.66  (step @p78 :rule trans :premises (@p77 @p70))
% 0.46/0.66  (step @p10 :rule arith-elim-lt :args (tptp.b -1))
% 0.46/0.66  (step @p11 :rule symm :premises (@p10))
% 0.46/0.66  (step @p79 :rule eq_resolve :premises (@p1259 @p11))
% 0.46/0.66  (step @p80 :rule int_tight_ub :premises (@p79))
% 0.46/0.66  (step @p81 :rule arith_mult_neg :args (-1 @t31))
% 0.46/0.66  (step @p31 :rule evaluate :args (@t29))
% 0.46/0.66  (step @p32 :rule true_elim :premises (@p31))
% 0.46/0.66  (step @p82 :rule and_intro :premises (@p32 @p1258))
% 0.46/0.66  (step @p83 :rule modus_ponens :premises (@p82 @p81))
% 0.46/0.66  (step @p84 :rule arith_sum_ub :premises (@p83 @p80))
% 0.46/0.66  (step @p85 false :rule eq_resolve :premises (@p84 @p78))
% 0.46/0.66  (step-pop @p1261 :rule scope :premises (@p85))
% 0.46/0.66  (step @p86 :rule process_scope :premises (@p1261) :args (false))
% 0.46/0.66  (step @p88 :rule eq_resolve :premises (@p86 @p68))
% 0.46/0.66  (step @p89 false :rule contra :premises (@p88 @p67))
% 0.46/0.66  (step-pop @p1262 :rule scope :premises (@p89))
% 0.46/0.66  (step-pop @p1263 :rule scope :premises (@p1262))
% 0.46/0.66  (step @p90 :rule process_scope :premises (@p1263) :args (false))
% 0.46/0.66  (step @p93 :rule not_and :premises (@p90))
% 0.46/0.66  (step @p94 :rule eq_resolve :premises (@p93 @p59))
% 0.46/0.66  (step @p95 :rule refl :args (@t38))
% 0.46/0.66  (step @p62 :rule bool-double-not-elim :args (@t31))
% 0.46/0.66  (step @p96 :rule refl :args (@t39))
% 0.46/0.66  (step @p97 :rule nary_cong :premises (@p96 @p62 @p95) :args ((or @t39 @t40 @t38)))
% 0.46/0.66  (step @p98 :rule cnf_and_neg :args (@t39))
% 0.46/0.66  (step @p99 :rule eq_resolve :premises (@p98 @p97))
% 0.46/0.66  (step @p100 :rule reordering :premises (@p99) :args ((or @t38 @t31 @t39)))
% 0.46/0.66  (step @p101 :rule refl :args (@t41))
% 0.46/0.66  (step @p102 :rule refl :args (@t42))
% 0.46/0.66  (step @p103 :rule nary_cong :premises (@p102 @p62 @p101) :args ((or @t42 @t40 @t41)))
% 0.46/0.66  (step @p104 :rule cnf_and_neg :args (@t42))
% 0.46/0.66  (step @p105 :rule eq_resolve :premises (@p104 @p103))
% 0.46/0.66  (step @p106 :rule reordering :premises (@p105) :args ((or @t41 @t31 @t42)))
% 0.46/0.66  (step @p107 :rule arith_poly_norm :args ((= (* 1 (- @t48 @t45)) (* 1 (- @t47 0)))))
% 0.46/0.66  (step @p108 :rule arith_poly_norm_rel :premises (@p107) :args ((= (>= @t48 @t45) @t49)))
% 0.46/0.66  (step @p109 :rule arith-elim-leq :args (@t45 @t48))
% 0.46/0.66  (step @p110 :rule trans :premises (@p109 @p108))
% 0.46/0.66  (step @p111 :rule arith_poly_norm :args ((= (* tptp.b @t51) @t48)))
% 0.46/0.66  (step @p112 :rule arith_poly_norm :args ((= @t52 @t51)))
% 0.46/0.66  (step @p113 :rule refl :args (tptp.b))
% 0.46/0.66  (step @p114 :rule nary_cong :premises (@p113 @p112) :args (@t53))
% 0.46/0.66  (step @p115 :rule trans :premises (@p114 @p111))
% 0.46/0.66  (step @p116 :rule arith_poly_norm :args ((= @t54 @t45)))
% 0.46/0.66  (step @p117 :rule cong :premises (@p116 @p115) :args (@t55))
% 0.46/0.66  (step @p118 :rule trans :premises (@p117 @p110))
% 0.46/0.66  (step @p119 :rule refl :args (@t18))
% 0.46/0.66  (step @p63 :rule arith-elim-lt :args (tptp.b 0))
% 0.46/0.66  (step @p120 :rule nary_cong :premises (@p63 @p119) :args (@t56))
% 0.46/0.66  (step @p121 :rule cong :premises (@p120 @p118) :args ((=> @t56 @t55)))
% 0.46/0.66  (step @p122 :rule symm :premises (@p121))
% 0.46/0.66  (step @p123 :rule arith_poly_norm :args ((= (* -1 (- tptp.a @t51)) (* -1 (- @t17 1)))))
% 0.46/0.66  (step @p124 :rule arith_poly_norm_rel :premises (@p123) :args ((= (>= tptp.a @t51) @t18)))
% 0.46/0.66  (step @p125 :rule refl :args (tptp.a))
% 0.46/0.66  (step @p126 :rule cong :premises (@p125 @p112) :args (@t57))
% 0.46/0.66  (step @p127 :rule trans :premises (@p126 @p124))
% 0.46/0.66  (step @p128 :rule nary_cong :premises (@p63 @p127) :args (@t58))
% 0.46/0.66  (step @p129 :rule cong :premises (@p128 @p118) :args ((=> @t58 @t55)))
% 0.46/0.66  (step @p130 :rule trans :premises (@p129 @p122))
% 0.46/0.66  (step @p131 :rule arith_mult_neg :args (tptp.b @t57))
% 0.46/0.66  (step @p132 :rule eq_resolve :premises (@p131 @p130))
% 0.46/0.66  (step @p133 :rule eq_resolve :premises (@p132 @p121))
% 0.46/0.66  (step @p134 :rule implies_elim :premises (@p133))
% 0.46/0.66  (step @p135 :rule reordering :premises (@p134) :args ((or @t49 (not @t39))))
% 0.46/0.66  (step @p136 :rule arith_poly_norm :args ((= (* 1 (- @t60 @t65)) @t63)))
% 0.46/0.66  (step @p137 :rule arith_poly_norm_rel :premises (@p136) :args ((= (= @t60 @t65) @t66)))
% 0.46/0.66  (step @p138 :rule arith_poly_norm :args ((= (* tptp.b @t13) @t65)))
% 0.46/0.66  (step @p139 :rule arith_poly_norm :args ((= @t67 @t13)))
% 0.46/0.66  (step @p140 :rule nary_cong :premises (@p113 @p139) :args (@t68))
% 0.46/0.66  (step @p141 :rule trans :premises (@p140 @p138))
% 0.46/0.66  (step @p142 :rule arith_poly_norm :args ((= @t69 @t60)))
% 0.46/0.66  (step @p143 :rule cong :premises (@p142 @p141) :args (@t70))
% 0.46/0.66  (step @p144 :rule trans :premises (@p143 @p137))
% 0.46/0.66  (step @p145 :rule refl :args (@t15))
% 0.46/0.66  (step @p146 :rule nary_cong :premises (@p63 @p145) :args (@t71))
% 0.46/0.66  (step @p147 :rule cong :premises (@p146 @p144) :args ((=> @t71 @t70)))
% 0.46/0.66  (step @p148 :rule symm :premises (@p147))
% 0.46/0.66  (step @p149 :rule refl :args (@t2))
% 0.46/0.66  (step @p150 :rule cong :premises (@p149 @p139) :args (@t72))
% 0.46/0.66  (step @p151 :rule nary_cong :premises (@p63 @p150) :args (@t73))
% 0.46/0.66  (step @p152 :rule cong :premises (@p151 @p144) :args ((=> @t73 @t70)))
% 0.46/0.66  (step @p153 :rule trans :premises (@p152 @p148))
% 0.46/0.66  (step @p154 :rule arith_mult_neg :args (tptp.b @t72))
% 0.46/0.66  (step @p155 :rule eq_resolve :premises (@p154 @p153))
% 0.46/0.66  (step @p156 :rule eq_resolve :premises (@p155 @p147))
% 0.46/0.66  (step @p157 :rule implies_elim :premises (@p156))
% 0.46/0.66  (step @p158 :rule reordering :premises (@p157) :args ((or @t66 (not @t42))))
% 0.46/0.66  (step @p159 :rule arith_poly_norm :args ((= (* -36 (- -35 @t74)) (* -36 (- -36 @t45)))))
% 0.46/0.66  (step @p160 :rule arith_poly_norm_rel :premises (@p159) :args ((= (>= -35 @t74) (>= -36 @t45))))
% 0.46/0.66  (step @p161 :rule arith-geq-tighten :args (@t45 -35))
% 0.46/0.66  (step @p162 :rule trans :premises (@p161 @p160))
% 0.46/0.66  (step @p163 :rule symm :premises (@p162))
% 0.46/0.66  (step @p164 :rule arith_poly_norm :args ((= @t5 @t45)))
% 0.46/0.66  (step @p165 :rule evaluate :args (@t6))
% 0.46/0.66  (step @p166 :rule cong :premises (@p165 @p164) :args (@t7))
% 0.46/0.66  (step @p167 :rule trans :premises (@p166 @p163))
% 0.46/0.66  (step @p168 :rule arith-elim-leq :args (-2 @t45))
% 0.46/0.66  (step @p169 :rule evaluate :args (@t8))
% 0.46/0.66  (step @p170 :rule cong :premises (@p169 @p164) :args (@t9))
% 0.46/0.66  (step @p171 :rule trans :premises (@p170 @p168))
% 0.46/0.66  (step @p172 :rule nary_cong :premises (@p171 @p167) :args (@t10))
% 0.46/0.66  (step @p173 :rule cong :premises (@p172) :args (@t11))
% 0.46/0.66  (step @p174 :rule eq_resolve :premises (@p2 @p173))
% 0.46/0.66  (step @p175 :rule not_or_elim :premises (@p174) :args (1))
% 0.46/0.66  (step @p176 :rule not_not_elim :premises (@p175))
% 0.46/0.66  (assume-push @p1264 @t49)
% 0.46/0.66  (assume-push @p1265 @t15)
% 0.46/0.66  (assume-push @p1266 @t18)
% 0.46/0.66  (assume-push @p1267 @t66)
% 0.46/0.66  (assume-push @p1268 @t75)
% 0.46/0.66  (step @p182 :rule arith-elim-lt :args (@t45 -35))
% 0.46/0.66  (step @p183 :rule symm :premises (@p182))
% 0.46/0.66  (assume-push @p1269 @t75)
% 0.46/0.66  (step @p185 :rule evaluate :args (@t76))
% 0.46/0.66  (step @p186 :rule evaluate :args ((+ 35 0 -45 9 0)))
% 0.46/0.66  (step @p187 :rule evaluate :args (@t77))
% 0.46/0.66  (step @p188 :rule evaluate :args (@t78))
% 0.46/0.66  (step @p189 :rule evaluate :args (@t79))
% 0.46/0.66  (step @p190 :rule evaluate :args (@t80))
% 0.46/0.66  (step @p191 :rule evaluate :args (@t81))
% 0.46/0.66  (step @p192 :rule nary_cong :premises (@p191 @p190 @p189 @p188 @p187) :args (@t82))
% 0.46/0.66  (step @p193 :rule trans :premises (@p192 @p186))
% 0.46/0.66  (step @p194 :rule arith_poly_norm :args ((= (+ @t46 @t88 @t87 @t86 @t85) 0)))
% 0.46/0.66  (step @p195 :rule arith_poly_norm :args ((= @t89 @t85)))
% 0.46/0.66  (step @p196 :rule arith_poly_norm :args ((= @t90 @t86)))
% 0.46/0.66  (step @p197 :rule arith_poly_norm :args ((= @t91 @t87)))
% 0.46/0.66  (step @p198 :rule arith_poly_norm :args (@t95))
% 0.46/0.66  (step @p199 :rule refl :args (@t46))
% 0.46/0.66  (step @p200 :rule nary_cong :premises (@p199 @p198 @p197 @p196 @p195) :args (@t96))
% 0.46/0.66  (step @p201 :rule trans :premises (@p200 @p194))
% 0.46/0.66  (step @p202 :rule cong :premises (@p201 @p193) :args ((<= @t96 @t82)))
% 0.46/0.66  (step @p203 :rule trans :premises (@p202 @p185))
% 0.46/0.66  (step @p204 :rule arith_mult_neg :args (-11 @t49))
% 0.46/0.66  (step @p205 :rule evaluate :args ((< -11 0)))
% 0.46/0.66  (step @p206 :rule true_elim :premises (@p205))
% 0.46/0.66  (step @p207 :rule and_intro :premises (@p206 @p1264))
% 0.46/0.66  (step @p208 :rule modus_ponens :premises (@p207 @p204))
% 0.46/0.66  (step @p209 :rule arith_mult_pos :args (9 @t4))
% 0.46/0.66  (step @p210 :rule evaluate :args ((> 9 0)))
% 0.46/0.66  (step @p211 :rule true_elim :premises (@p210))
% 0.46/0.66  (step @p212 :rule and_intro :premises (@p211 @p1))
% 0.46/0.66  (step @p213 :rule modus_ponens :premises (@p212 @p209))
% 0.46/0.66  (step @p214 :rule arith_mult_neg :args (-45 @t18))
% 0.46/0.66  (step @p215 :rule evaluate :args ((< -45 0)))
% 0.46/0.66  (step @p216 :rule true_elim :premises (@p215))
% 0.46/0.66  (step @p217 :rule and_intro :premises (@p216 @p1266))
% 0.46/0.66  (step @p218 :rule modus_ponens :premises (@p217 @p214))
% 0.46/0.66  (step @p219 :rule arith_mult_pos :args (2 @t97))
% 0.46/0.66  (step @p220 :rule arith_poly_norm :args (@t98))
% 0.46/0.66  (step @p221 :rule arith_poly_norm_rel :premises (@p220) :args (@t99))
% 0.46/0.66  (step @p222 :rule symm :premises (@p221))
% 0.46/0.66  (step @p223 :rule eq_resolve :premises (@p1267 @p222))
% 0.46/0.66  (step @p224 :rule evaluate :args (@t100))
% 0.46/0.66  (step @p225 :rule true_elim :premises (@p224))
% 0.46/0.66  (step @p226 :rule and_intro :premises (@p225 @p223))
% 0.46/0.66  (step @p227 :rule modus_ponens :premises (@p226 @p219))
% 0.46/0.66  (step @p228 :rule arith_mult_neg :args (-1 @t75))
% 0.46/0.66  (step @p31 :rule evaluate :args (@t29))
% 0.46/0.66  (step @p32 :rule true_elim :premises (@p31))
% 0.46/0.66  (step @p229 :rule and_intro :premises (@p32 @p176))
% 0.46/0.66  (step @p230 :rule modus_ponens :premises (@p229 @p228))
% 0.46/0.66  (step @p231 :rule arith_sum_ub :premises (@p230 @p227 @p218 @p213 @p208))
% 0.46/0.66  (step @p232 false :rule eq_resolve :premises (@p231 @p203))
% 0.46/0.66  (step-pop @p1270 :rule scope :premises (@p232))
% 0.46/0.66  (step @p233 :rule process_scope :premises (@p1270) :args (false))
% 0.46/0.66  (step @p235 :rule eq_resolve :premises (@p233 @p183))
% 0.46/0.66  (step @p236 :rule eq_resolve :premises (@p235 @p182))
% 0.46/0.66  (step @p237 false :rule contra :premises (@p176 @p236))
% 0.46/0.66  (step-pop @p1271 :rule scope :premises (@p237))
% 0.46/0.66  (step-pop @p1272 :rule scope :premises (@p1271))
% 0.46/0.66  (step-pop @p1273 :rule scope :premises (@p1272))
% 0.46/0.66  (step-pop @p1274 :rule scope :premises (@p1273))
% 0.46/0.66  (step-pop @p1275 :rule scope :premises (@p1274))
% 0.46/0.66  (step @p238 :rule process_scope :premises (@p1275) :args (false))
% 0.46/0.66  (assume-push @p1276 @t15)
% 0.46/0.66  (assume-push @p1277 @t75)
% 0.46/0.66  (assume-push @p1278 @t18)
% 0.46/0.66  (assume-push @p1279 @t49)
% 0.46/0.66  (assume-push @p1280 @t66)
% 0.46/0.66  (step @p249 :rule and_intro :premises (@p1279 @p6 @p1278 @p1280 @p176))
% 0.46/0.66  (step-pop @p1281 :rule scope :premises (@p249))
% 0.46/0.66  (step-pop @p1282 :rule scope :premises (@p1281))
% 0.46/0.66  (step-pop @p1283 :rule scope :premises (@p1282))
% 0.46/0.66  (step-pop @p1284 :rule scope :premises (@p1283))
% 0.46/0.66  (step-pop @p1285 :rule scope :premises (@p1284))
% 0.46/0.66  (step @p250 :rule process_scope :premises (@p1285) :args (@t101))
% 0.46/0.66  (step @p256 :rule implies_elim :premises (@p250))
% 0.46/0.66  (step @p257 :rule resolution :premises (@p256 @p238) :args (true @t101))
% 0.46/0.66  (step @p258 :rule not_and :premises (@p257))
% 0.46/0.66  (step @p259 :rule reordering :premises (@p258) :args ((or @t103 @t41 @t38 (not @t49) @t102)))
% 0.46/0.66  (step @p260 :rule chain_m_resolution :premises (@p259 @p176 @p6 @p158 @p135 @p106 @p6 @p100 @p94 @p56 @p6) :args (@t38 (@list false false false false false false false true true false) (@list @t75 @t15 @t66 @t49 @t42 @t15 @t39 @t31 @t19 @t15)))
% 0.46/0.66  (step @p261 :rule bool-double-not-elim :args (@t18))
% 0.46/0.66  (step @p262 :rule refl :args (@t105))
% 0.46/0.66  (step @p263 :rule nary_cong :premises (@p101 @p262 @p261) :args ((or @t41 @t105 @t106)))
% 0.46/0.66  (assume-push @p1286 @t104)
% 0.46/0.66  (assume-push @p1287 @t15)
% 0.46/0.66  (assume-push @p1288 @t38)
% 0.46/0.66  (step @p267 :rule arith-elim-leq :args (@t17 0))
% 0.46/0.66  (step @p268 :rule symm :premises (@p267))
% 0.46/0.66  (step @p269 :rule cong :premises (@p268) :args ((not (>= 0 @t17))))
% 0.46/0.66  (step @p270 :rule arith-elim-gt :args (@t17 0))
% 0.46/0.66  (step @p271 :rule trans :premises (@p270 @p269))
% 0.46/0.66  (step @p272 :rule evaluate :args (@t107))
% 0.46/0.66  (step @p273 :rule refl :args (@t17))
% 0.46/0.66  (step @p274 :rule cong :premises (@p273 @p272) :args (@t108))
% 0.46/0.66  (step @p275 :rule cong :premises (@p274) :args ((not @t108)))
% 0.46/0.66  (step @p276 :rule arith-leq-norm :args (@t17 0))
% 0.46/0.66  (step @p277 :rule trans :premises (@p276 @p275))
% 0.46/0.66  (step @p278 :rule cong :premises (@p277) :args ((not @t109)))
% 0.46/0.66  (step @p279 :rule trans :premises (@p278 @p261))
% 0.46/0.66  (step @p280 :rule trans :premises (@p271 @p279))
% 0.46/0.66  (step @p281 :rule symm :premises (@p280))
% 0.46/0.66  (step @p282 :rule trans :premises (@p279 @p281))
% 0.46/0.66  (assume-push @p1289 @t109)
% 0.46/0.66  (step @p284 :rule evaluate :args ((<= 0/1 -2/11)))
% 0.46/0.66  (step @p285 :rule evaluate :args ((+ 0/1 -2/11 0/1)))
% 0.46/0.66  (step @p286 :rule evaluate :args (@t110))
% 0.46/0.66  (step @p287 :rule evaluate :args (@t111))
% 0.46/0.66  (step @p288 :rule refl :args (0/1))
% 0.46/0.66  (step @p289 :rule nary_cong :premises (@p288 @p287 @p286) :args (@t112))
% 0.46/0.66  (step @p290 :rule trans :premises (@p289 @p285))
% 0.46/0.66  (step @p291 :rule arith_poly_norm :args ((= @t116 0/1)))
% 0.46/0.66  (step @p292 :rule arith_poly_norm :args ((= @t120 @t116)))
% 0.46/0.66  (step @p293 :rule trans :premises (@p292 @p291))
% 0.46/0.66  (step @p294 :rule cong :premises (@p293 @p290) :args ((<= @t120 @t112)))
% 0.46/0.66  (step @p295 :rule trans :premises (@p294 @p284))
% 0.46/0.66  (assume-push @p1290 @t121)
% 0.46/0.66  (assume-push @p1291 @t104)
% 0.46/0.66  (step @p298 :rule arith_mult_neg :args (-1/11 (>= @t113 0/1)))
% 0.46/0.66  (step @p299 :rule evaluate :args (@t122))
% 0.46/0.66  (step @p300 :rule refl :args (@t113))
% 0.46/0.66  (step @p301 :rule cong :premises (@p300 @p299) :args (@t123))
% 0.46/0.66  (step @p302 :rule arith_poly_norm :args ((= (* 1/1 (to_real (- tptp.a 0))) (* 1/1 (- @t113 @t122)))))
% 0.46/0.66  (step @p303 :rule arith_poly_norm_rel :premises (@p302) :args ((= @t104 @t123)))
% 0.46/0.66  (step @p304 :rule trans :premises (@p303 @p301))
% 0.46/0.66  (step @p305 :rule eq_resolve :premises (@p1286 @p304))
% 0.46/0.66  (step @p306 :rule and_intro :premises (@p1290 @p305))
% 0.46/0.66  (step @p307 :rule modus_ponens :premises (@p306 @p298))
% 0.46/0.66  (step-pop @p1292 :rule scope :premises (@p307))
% 0.46/0.66  (step-pop @p1293 :rule scope :premises (@p1292))
% 0.46/0.66  (step @p308 :rule process_scope :premises (@p1293) :args ((<= @t115 @t110)))
% 0.46/0.66  (step @p311 :rule evaluate :args (@t121))
% 0.46/0.66  (step @p312 :rule true_elim :premises (@p311))
% 0.46/0.66  (step @p313 :rule and_intro :premises (@p312 @p1286))
% 0.46/0.66  (step @p314 :rule modus_ponens :premises (@p313 @p308))
% 0.46/0.66  (assume-push @p1294 @t124)
% 0.46/0.66  (assume-push @p1295 @t4)
% 0.46/0.66  (step @p317 :rule arith_mult_neg :args (-2/11 @t125))
% 0.46/0.66  (step @p318 :rule evaluate :args (@t126))
% 0.46/0.66  (step @p319 :rule cong :premises (@p1) :args (@t117))
% 0.46/0.66  (step @p320 :rule trans :premises (@p319 @p318))
% 0.46/0.66  (step @p321 :rule and_intro :premises (@p1294 @p320))
% 0.46/0.66  (step @p322 :rule modus_ponens :premises (@p321 @p317))
% 0.46/0.66  (step-pop @p1296 :rule scope :premises (@p322))
% 0.46/0.66  (step-pop @p1297 :rule scope :premises (@p1296))
% 0.46/0.66  (step @p323 :rule process_scope :premises (@p1297) :args ((= @t118 @t111)))
% 0.46/0.66  (step @p326 :rule evaluate :args (@t124))
% 0.46/0.66  (step @p327 :rule true_elim :premises (@p326))
% 0.46/0.66  (step @p328 :rule and_intro :premises (@p327 @p1))
% 0.46/0.66  (step @p329 :rule modus_ponens :premises (@p328 @p323))
% 0.46/0.66  (step @p330 :rule evaluate :args (@t122))
% 0.46/0.66  (step @p331 :rule refl :args (@t119))
% 0.46/0.66  (step @p332 :rule cong :premises (@p331 @p330) :args (@t127))
% 0.46/0.66  (step @p333 :rule arith_poly_norm :args (@t128))
% 0.46/0.66  (step @p334 :rule arith_poly_norm_rel :premises (@p333) :args (@t129))
% 0.46/0.66  (step @p335 :rule trans :premises (@p334 @p332))
% 0.46/0.66  (step @p336 :rule eq_resolve :premises (@p1289 @p335))
% 0.46/0.66  (step @p337 :rule arith_sum_ub :premises (@p336 @p329 @p314))
% 0.46/0.66  (step @p338 false :rule eq_resolve :premises (@p337 @p295))
% 0.46/0.66  (step-pop @p1298 :rule scope :premises (@p338))
% 0.46/0.66  (step @p339 :rule process_scope :premises (@p1298) :args (false))
% 0.46/0.66  (step @p341 :rule eq_resolve :premises (@p339 @p282))
% 0.46/0.66  (step @p342 :rule eq_resolve :premises (@p341 @p271))
% 0.46/0.66  (step @p343 :rule arith-elim-lt :args (@t17 1))
% 0.46/0.66  (step @p344 :rule symm :premises (@p343))
% 0.46/0.66  (step @p345 :rule eq_resolve :premises (@p1288 @p344))
% 0.46/0.66  (step @p346 :rule int_tight_ub :premises (@p345))
% 0.46/0.66  (step @p347 false :rule contra :premises (@p346 @p342))
% 0.46/0.66  (step-pop @p1299 :rule scope :premises (@p347))
% 0.46/0.66  (step-pop @p1300 :rule scope :premises (@p1299))
% 0.46/0.66  (step-pop @p1301 :rule scope :premises (@p1300))
% 0.46/0.66  (step @p348 :rule process_scope :premises (@p1301) :args (false))
% 0.46/0.66  (assume-push @p1302 @t15)
% 0.46/0.66  (assume-push @p1303 @t104)
% 0.46/0.66  (assume-push @p1304 @t38)
% 0.46/0.66  (step @p355 :rule and_intro :premises (@p1303 @p6 @p1304))
% 0.46/0.66  (step-pop @p1305 :rule scope :premises (@p355))
% 0.46/0.66  (step-pop @p1306 :rule scope :premises (@p1305))
% 0.46/0.66  (step-pop @p1307 :rule scope :premises (@p1306))
% 0.46/0.66  (step @p356 :rule process_scope :premises (@p1307) :args (@t130))
% 0.46/0.66  (step @p360 :rule implies_elim :premises (@p356))
% 0.46/0.66  (step @p361 :rule resolution :premises (@p360 @p348) :args (true @t130))
% 0.46/0.66  (step @p362 :rule not_and :premises (@p361))
% 0.46/0.66  (step @p363 :rule eq_resolve :premises (@p362 @p263))
% 0.46/0.66  (step @p364 :rule chain_m_resolution :premises (@p363 @p6 @p260) :args (@t105 @t131 @t132))
% 0.46/0.66  (step @p365 :rule bool-double-not-elim :args (@t104))
% 0.46/0.66  (step @p366 :rule refl :args (@t133))
% 0.46/0.66  (step @p367 :rule nary_cong :premises (@p366 @p365 @p101) :args ((or @t133 @t134 @t41)))
% 0.46/0.66  (step @p368 :rule cnf_and_neg :args (@t133))
% 0.46/0.66  (step @p369 :rule eq_resolve :premises (@p368 @p367))
% 0.46/0.66  (step @p370 :rule reordering :premises (@p369) :args ((or @t41 @t104 @t133)))
% 0.46/0.66  (step @p371 :rule chain_m_resolution :premises (@p370 @p6 @p364) :args (@t133 @t131 (@list @t15 @t104)))
% 0.46/0.66  (step @p372 :rule arith_poly_norm :args ((= (* 1 (- @t84 @t140)) (* -1 @t138))))
% 0.46/0.66  (step @p373 :rule arith_poly_norm_rel :premises (@p372) :args ((= (= @t84 @t140) @t141)))
% 0.46/0.66  (step @p374 :rule arith_poly_norm :args ((= (* tptp.a @t142) @t140)))
% 0.46/0.66  (step @p375 :rule arith_poly_norm :args ((= @t143 @t142)))
% 0.46/0.66  (step @p376 :rule nary_cong :premises (@p125 @p375) :args (@t144))
% 0.46/0.66  (step @p377 :rule trans :premises (@p376 @p374))
% 0.46/0.66  (step @p378 :rule arith_poly_norm :args ((= @t145 @t84)))
% 0.46/0.66  (step @p379 :rule cong :premises (@p378 @p377) :args (@t146))
% 0.46/0.66  (step @p380 :rule trans :premises (@p379 @p373))
% 0.46/0.66  (step @p381 :rule arith-elim-lt :args (tptp.a 0))
% 0.46/0.66  (step @p382 :rule nary_cong :premises (@p381 @p145) :args (@t148))
% 0.46/0.66  (step @p383 :rule cong :premises (@p382 @p380) :args ((=> @t148 @t146)))
% 0.46/0.66  (step @p384 :rule symm :premises (@p383))
% 0.46/0.66  (step @p385 :rule arith_poly_norm :args ((= (* -1 (- @t1 @t142)) @t14)))
% 0.46/0.66  (step @p386 :rule arith_poly_norm_rel :premises (@p385) :args ((= (= @t1 @t142) @t15)))
% 0.46/0.66  (step @p387 :rule refl :args (@t1))
% 0.46/0.66  (step @p388 :rule cong :premises (@p387 @p375) :args (@t149))
% 0.46/0.66  (step @p389 :rule trans :premises (@p388 @p386))
% 0.46/0.66  (step @p390 :rule nary_cong :premises (@p381 @p389) :args (@t150))
% 0.46/0.66  (step @p391 :rule cong :premises (@p390 @p380) :args ((=> @t150 @t146)))
% 0.46/0.66  (step @p392 :rule trans :premises (@p391 @p384))
% 0.46/0.66  (step @p393 :rule arith_mult_neg :args (tptp.a @t149))
% 0.46/0.66  (step @p394 :rule eq_resolve :premises (@p393 @p392))
% 0.46/0.66  (step @p395 :rule eq_resolve :premises (@p394 @p383))
% 0.46/0.66  (step @p396 :rule implies_elim :premises (@p395))
% 0.46/0.66  (step @p397 :rule reordering :premises (@p396) :args ((or @t141 (not @t133))))
% 0.46/0.66  (step @p398 :rule chain_m_resolution :premises (@p397 @p371) :args (@t141 (@list false) (@list @t133)))
% 0.46/0.66  (step @p399 :rule refl :args (@t152))
% 0.46/0.66  (step @p400 :rule refl :args (@t153))
% 0.46/0.66  (step @p401 :rule nary_cong :premises (@p400 @p365 @p399) :args ((or @t153 @t134 @t152)))
% 0.46/0.66  (step @p402 :rule cnf_and_neg :args (@t153))
% 0.46/0.66  (step @p403 :rule eq_resolve :premises (@p402 @p401))
% 0.46/0.66  (step @p404 :rule reordering :premises (@p403) :args ((or @t104 @t152 @t153)))
% 0.46/0.66  (step @p405 :rule arith_poly_norm :args ((= (* 2 (- @t154 @t45)) (* 2 @t156))))
% 0.46/0.66  (step @p406 :rule arith_poly_norm_rel :premises (@p405) :args ((= (>= @t154 @t45) @t157)))
% 0.46/0.66  (step @p407 :rule arith-elim-leq :args (@t45 @t154))
% 0.46/0.66  (step @p408 :rule trans :premises (@p407 @p406))
% 0.46/0.66  (step @p409 :rule arith_poly_norm :args ((= (* tptp.a 2) @t154)))
% 0.46/0.66  (step @p410 :rule evaluate :args (@t158))
% 0.46/0.66  (step @p411 :rule nary_cong :premises (@p125 @p410) :args (@t159))
% 0.46/0.66  (step @p412 :rule trans :premises (@p411 @p409))
% 0.46/0.66  (step @p413 :rule cong :premises (@p164 @p412) :args (@t160))
% 0.46/0.66  (step @p414 :rule trans :premises (@p413 @p408))
% 0.46/0.66  (step @p415 :rule refl :args (@t151))
% 0.46/0.66  (step @p416 :rule nary_cong :premises (@p381 @p415) :args (@t161))
% 0.46/0.66  (step @p417 :rule cong :premises (@p416 @p414) :args ((=> @t161 @t160)))
% 0.46/0.66  (step @p418 :rule symm :premises (@p417))
% 0.46/0.66  (step @p419 :rule cong :premises (@p113 @p410) :args (@t162))
% 0.46/0.66  (step @p420 :rule nary_cong :premises (@p381 @p419) :args (@t163))
% 0.46/0.66  (step @p421 :rule cong :premises (@p420 @p414) :args ((=> @t163 @t160)))
% 0.46/0.66  (step @p422 :rule trans :premises (@p421 @p418))
% 0.46/0.66  (step @p423 :rule arith_mult_neg :args (tptp.a @t162))
% 0.46/0.66  (step @p424 :rule eq_resolve :premises (@p423 @p422))
% 0.46/0.66  (step @p425 :rule eq_resolve :premises (@p424 @p417))
% 0.46/0.66  (step @p426 :rule implies_elim :premises (@p425))
% 0.46/0.66  (step @p427 :rule reordering :premises (@p426) :args ((or @t157 (not @t153))))
% 0.46/0.66  (step @p428 :rule bool-double-not-elim :args (@t167))
% 0.46/0.66  (step @p429 :rule refl :args (@t168))
% 0.46/0.66  (step @p430 :rule bool-double-not-elim :args (@t170))
% 0.46/0.66  (step @p431 :rule refl :args (@t102))
% 0.46/0.66  (step @p432 :rule refl :args (@t171))
% 0.46/0.66  (step @p433 :rule nary_cong :premises (@p101 @p432 @p431 @p430 @p429 @p428) :args ((or @t41 @t171 @t102 @t175 @t168 @t173)))
% 0.46/0.66  (assume-push @p1308 @t157)
% 0.46/0.66  (assume-push @p1309 @t174)
% 0.46/0.66  (assume-push @p1310 @t141)
% 0.46/0.66  (assume-push @p1311 @t66)
% 0.46/0.66  (assume-push @p1312 @t15)
% 0.46/0.66  (assume-push @p1313 @t172)
% 0.46/0.66  (step @p440 :rule arith-elim-leq :args (@t166 0))
% 0.46/0.66  (step @p441 :rule symm :premises (@p440))
% 0.46/0.66  (step @p442 :rule cong :premises (@p441) :args ((not (>= 0 @t166))))
% 0.46/0.66  (step @p443 :rule arith-elim-gt :args (@t166 0))
% 0.46/0.66  (step @p444 :rule trans :premises (@p443 @p442))
% 0.46/0.66  (step @p272 :rule evaluate :args (@t107))
% 0.46/0.66  (step @p445 :rule refl :args (@t166))
% 0.46/0.66  (step @p446 :rule cong :premises (@p445 @p272) :args (@t176))
% 0.46/0.66  (step @p447 :rule cong :premises (@p446) :args ((not @t176)))
% 0.46/0.66  (step @p448 :rule arith-leq-norm :args (@t166 0))
% 0.46/0.66  (step @p449 :rule trans :premises (@p448 @p447))
% 0.46/0.66  (step @p450 :rule cong :premises (@p449) :args ((not @t177)))
% 0.46/0.66  (step @p451 :rule trans :premises (@p450 @p428))
% 0.46/0.66  (step @p452 :rule trans :premises (@p444 @p451))
% 0.46/0.66  (step @p453 :rule symm :premises (@p452))
% 0.46/0.66  (step @p454 :rule trans :premises (@p451 @p453))
% 0.46/0.66  (assume-push @p1314 @t177)
% 0.46/0.66  (step @p456 :rule evaluate :args (@t178))
% 0.46/0.66  (step @p457 :rule evaluate :args ((>= 0/1 -2/55)))
% 0.46/0.66  (step @p458 :rule evaluate :args ((+ 0/1 -2/55 0/1 0/1 0/1 0/1)))
% 0.46/0.66  (step @p459 :rule evaluate :args (@t179))
% 0.46/0.66  (step @p460 :rule evaluate :args (@t180))
% 0.46/0.66  (step @p461 :rule evaluate :args (@t181))
% 0.46/0.66  (step @p462 :rule evaluate :args (@t182))
% 0.46/0.66  (step @p463 :rule evaluate :args (@t183))
% 0.46/0.66  (step @p464 :rule refl :args (0/1))
% 0.46/0.66  (step @p465 :rule nary_cong :premises (@p464 @p463 @p462 @p461 @p460 @p459) :args (@t184))
% 0.46/0.66  (step @p466 :rule trans :premises (@p465 @p458))
% 0.46/0.66  (step @p467 :rule arith_poly_norm :args ((= @t190 0/1)))
% 0.46/0.66  (step @p468 :rule arith_poly_norm :args ((= @t202 @t190)))
% 0.46/0.66  (step @p469 :rule trans :premises (@p468 @p467))
% 0.46/0.66  (step @p470 :rule cong :premises (@p469 @p466) :args (@t203))
% 0.46/0.66  (step @p471 :rule trans :premises (@p470 @p457))
% 0.46/0.66  (step @p472 :rule cong :premises (@p471) :args ((not @t203)))
% 0.46/0.66  (step @p473 :rule trans :premises (@p472 @p456))
% 0.46/0.66  (step @p474 :rule arith-elim-lt :args (@t202 @t184))
% 0.46/0.66  (step @p475 :rule trans :premises (@p474 @p473))
% 0.46/0.66  (assume-push @p1315 @t204)
% 0.46/0.66  (assume-push @p1316 @t157)
% 0.46/0.66  (step @p478 :rule arith_mult_neg :args (-1/55 (>= @t191 0/1)))
% 0.46/0.66  (step @p479 :rule evaluate :args (@t122))
% 0.46/0.66  (step @p480 :rule refl :args (@t191))
% 0.46/0.66  (step @p481 :rule cong :premises (@p480 @p479) :args (@t205))
% 0.46/0.66  (step @p482 :rule arith_poly_norm :args ((= (* 2/1 (to_real @t156)) (* 2/1 (- @t191 @t122)))))
% 0.46/0.66  (step @p483 :rule arith_poly_norm_rel :premises (@p482) :args ((= @t157 @t205)))
% 0.46/0.66  (step @p484 :rule trans :premises (@p483 @p481))
% 0.46/0.66  (step @p485 :rule eq_resolve :premises (@p1308 @p484))
% 0.46/0.66  (step @p486 :rule and_intro :premises (@p1315 @p485))
% 0.46/0.66  (step @p487 :rule modus_ponens :premises (@p486 @p478))
% 0.46/0.66  (step-pop @p1317 :rule scope :premises (@p487))
% 0.46/0.66  (step-pop @p1318 :rule scope :premises (@p1317))
% 0.46/0.66  (step @p488 :rule process_scope :premises (@p1318) :args ((<= @t192 @t179)))
% 0.46/0.66  (step @p491 :rule evaluate :args (@t204))
% 0.46/0.66  (step @p492 :rule true_elim :premises (@p491))
% 0.46/0.66  (step @p493 :rule and_intro :premises (@p492 @p1308))
% 0.46/0.66  (step @p494 :rule modus_ponens :premises (@p493 @p488))
% 0.46/0.66  (assume-push @p1319 @t206)
% 0.46/0.66  (assume-push @p1320 @t207)
% 0.46/0.66  (step @p497 :rule arith_mult_pos :args (1/55 (< @t193 0/1)))
% 0.46/0.66  (step @p498 :rule evaluate :args (@t122))
% 0.46/0.66  (step @p499 :rule refl :args (@t193))
% 0.46/0.66  (step @p500 :rule cong :premises (@p499 @p498) :args (@t208))
% 0.46/0.66  (step @p501 :rule arith_poly_norm :args ((= (* 22/1 (to_real (- @t169 0))) (* 22/1 (- @t193 @t122)))))
% 0.46/0.66  (step @p502 :rule arith_poly_norm_rel :premises (@p501) :args ((= @t207 @t208)))
% 0.46/0.66  (step @p503 :rule trans :premises (@p502 @p500))
% 0.46/0.66  (step @p504 :rule eq_resolve :premises (@p1320 @p503))
% 0.46/0.66  (step @p505 :rule and_intro :premises (@p1319 @p504))
% 0.46/0.66  (step @p506 :rule modus_ponens :premises (@p505 @p497))
% 0.46/0.66  (step-pop @p1321 :rule scope :premises (@p506))
% 0.46/0.66  (step-pop @p1322 :rule scope :premises (@p1321))
% 0.46/0.66  (step @p507 :rule process_scope :premises (@p1322) :args ((< @t194 @t180)))
% 0.46/0.66  (step @p510 :rule arith-elim-lt :args (@t169 0))
% 0.46/0.66  (step @p511 :rule symm :premises (@p510))
% 0.46/0.66  (step @p512 :rule eq_resolve :premises (@p1309 @p511))
% 0.46/0.66  (step @p513 :rule evaluate :args (@t206))
% 0.46/0.66  (step @p514 :rule true_elim :premises (@p513))
% 0.46/0.66  (step @p515 :rule and_intro :premises (@p514 @p512))
% 0.46/0.66  (step @p516 :rule modus_ponens :premises (@p515 @p507))
% 0.46/0.66  (assume-push @p1323 @t209)
% 0.46/0.66  (assume-push @p1324 @t210)
% 0.46/0.66  (step @p519 :rule arith_mult_pos :args (12/55 @t211))
% 0.46/0.66  (step @p520 :rule evaluate :args (@t122))
% 0.46/0.66  (step @p521 :rule cong :premises (@p1324) :args (@t196))
% 0.46/0.66  (step @p522 :rule trans :premises (@p521 @p520))
% 0.46/0.66  (step @p523 :rule and_intro :premises (@p1323 @p522))
% 0.46/0.66  (step @p524 :rule modus_ponens :premises (@p523 @p519))
% 0.46/0.66  (step-pop @p1325 :rule scope :premises (@p524))
% 0.46/0.66  (step-pop @p1326 :rule scope :premises (@p1325))
% 0.46/0.66  (step @p525 :rule process_scope :premises (@p1326) :args ((= @t197 @t181)))
% 0.46/0.66  (step @p528 :rule arith_poly_norm :args (@t212))
% 0.46/0.66  (step @p529 :rule arith_poly_norm_rel :premises (@p528) :args (@t213))
% 0.46/0.66  (step @p530 :rule symm :premises (@p529))
% 0.46/0.66  (step @p531 :rule eq_resolve :premises (@p1310 @p530))
% 0.46/0.66  (step @p532 :rule evaluate :args (@t209))
% 0.46/0.66  (step @p533 :rule true_elim :premises (@p532))
% 0.46/0.66  (step @p534 :rule and_intro :premises (@p533 @p531))
% 0.46/0.66  (step @p535 :rule modus_ponens :premises (@p534 @p525))
% 0.46/0.66  (assume-push @p1327 @t214)
% 0.46/0.66  (assume-push @p1328 @t97)
% 0.46/0.66  (step @p538 :rule arith_mult_pos :args (2/5 @t215))
% 0.46/0.66  (step @p539 :rule evaluate :args (@t122))
% 0.46/0.66  (step @p540 :rule cong :premises (@p1328) :args (@t198))
% 0.46/0.66  (step @p541 :rule trans :premises (@p540 @p539))
% 0.46/0.66  (step @p542 :rule and_intro :premises (@p1327 @p541))
% 0.46/0.66  (step @p543 :rule modus_ponens :premises (@p542 @p538))
% 0.46/0.66  (step-pop @p1329 :rule scope :premises (@p543))
% 0.46/0.66  (step-pop @p1330 :rule scope :premises (@p1329))
% 0.46/0.66  (step @p544 :rule process_scope :premises (@p1330) :args ((= @t199 @t182)))
% 0.46/0.66  (step @p220 :rule arith_poly_norm :args (@t98))
% 0.46/0.66  (step @p221 :rule arith_poly_norm_rel :premises (@p220) :args (@t99))
% 0.46/0.66  (step @p222 :rule symm :premises (@p221))
% 0.46/0.66  (step @p547 :rule eq_resolve :premises (@p1311 @p222))
% 0.46/0.66  (step @p548 :rule evaluate :args (@t214))
% 0.46/0.66  (step @p549 :rule true_elim :premises (@p548))
% 0.46/0.66  (step @p550 :rule and_intro :premises (@p549 @p547))
% 0.46/0.66  (step @p551 :rule modus_ponens :premises (@p550 @p544))
% 0.46/0.66  (assume-push @p1331 @t216)
% 0.46/0.66  (assume-push @p1332 @t4)
% 0.46/0.66  (step @p554 :rule arith_mult_neg :args (-2/55 @t125))
% 0.46/0.66  (step @p555 :rule evaluate :args (@t126))
% 0.46/0.66  (step @p556 :rule cong :premises (@p1) :args (@t117))
% 0.46/0.66  (step @p557 :rule trans :premises (@p556 @p555))
% 0.46/0.66  (step @p558 :rule and_intro :premises (@p1331 @p557))
% 0.46/0.66  (step @p559 :rule modus_ponens :premises (@p558 @p554))
% 0.46/0.66  (step-pop @p1333 :rule scope :premises (@p559))
% 0.46/0.66  (step-pop @p1334 :rule scope :premises (@p1333))
% 0.46/0.66  (step @p560 :rule process_scope :premises (@p1334) :args ((= @t200 @t183)))
% 0.46/0.66  (step @p563 :rule evaluate :args (@t216))
% 0.46/0.66  (step @p564 :rule true_elim :premises (@p563))
% 0.46/0.66  (step @p565 :rule and_intro :premises (@p564 @p1))
% 0.46/0.66  (step @p566 :rule modus_ponens :premises (@p565 @p560))
% 0.46/0.66  (step @p567 :rule evaluate :args (@t122))
% 0.46/0.66  (step @p568 :rule refl :args (@t201))
% 0.46/0.66  (step @p569 :rule cong :premises (@p568 @p567) :args (@t217))
% 0.46/0.66  (step @p570 :rule arith_poly_norm :args ((= (* 4/1 (to_real (- @t166 0))) (* 4/1 (- @t201 @t122)))))
% 0.46/0.66  (step @p571 :rule arith_poly_norm_rel :premises (@p570) :args ((= @t177 @t217)))
% 0.46/0.66  (step @p572 :rule trans :premises (@p571 @p569))
% 0.46/0.66  (step @p573 :rule eq_resolve :premises (@p1314 @p572))
% 0.46/0.66  (step @p574 :rule arith_sum_ub :premises (@p573 @p566 @p551 @p535 @p516 @p494))
% 0.46/0.66  (step @p575 false :rule eq_resolve :premises (@p574 @p475))
% 0.46/0.66  (step-pop @p1335 :rule scope :premises (@p575))
% 0.46/0.66  (step @p576 :rule process_scope :premises (@p1335) :args (false))
% 0.46/0.66  (step @p578 :rule eq_resolve :premises (@p576 @p454))
% 0.46/0.66  (step @p579 :rule eq_resolve :premises (@p578 @p444))
% 0.46/0.66  (step @p580 :rule arith-elim-lt :args (@t166 1))
% 0.46/0.66  (step @p581 :rule symm :premises (@p580))
% 0.46/0.66  (step @p582 :rule eq_resolve :premises (@p1313 @p581))
% 0.46/0.66  (step @p583 :rule int_tight_ub :premises (@p582))
% 0.46/0.66  (step @p584 false :rule contra :premises (@p583 @p579))
% 0.46/0.66  (step-pop @p1336 :rule scope :premises (@p584))
% 0.46/0.66  (step-pop @p1337 :rule scope :premises (@p1336))
% 0.46/0.66  (step-pop @p1338 :rule scope :premises (@p1337))
% 0.46/0.66  (step-pop @p1339 :rule scope :premises (@p1338))
% 0.46/0.66  (step-pop @p1340 :rule scope :premises (@p1339))
% 0.46/0.66  (step-pop @p1341 :rule scope :premises (@p1340))
% 0.46/0.66  (step @p585 :rule process_scope :premises (@p1341) :args (false))
% 0.46/0.66  (assume-push @p1342 @t15)
% 0.46/0.66  (assume-push @p1343 @t141)
% 0.46/0.66  (assume-push @p1344 @t66)
% 0.46/0.66  (assume-push @p1345 @t174)
% 0.46/0.66  (assume-push @p1346 @t157)
% 0.46/0.66  (assume-push @p1347 @t172)
% 0.46/0.66  (step @p598 :rule and_intro :premises (@p1346 @p1345 @p1343 @p1344 @p6 @p1347))
% 0.46/0.66  (step-pop @p1348 :rule scope :premises (@p598))
% 0.46/0.66  (step-pop @p1349 :rule scope :premises (@p1348))
% 0.46/0.66  (step-pop @p1350 :rule scope :premises (@p1349))
% 0.46/0.66  (step-pop @p1351 :rule scope :premises (@p1350))
% 0.46/0.66  (step-pop @p1352 :rule scope :premises (@p1351))
% 0.46/0.66  (step-pop @p1353 :rule scope :premises (@p1352))
% 0.46/0.66  (step @p599 :rule process_scope :premises (@p1353) :args (@t218))
% 0.46/0.66  (step @p606 :rule implies_elim :premises (@p599))
% 0.46/0.66  (step @p607 :rule resolution :premises (@p606 @p585) :args (true @t218))
% 0.46/0.66  (step @p608 :rule not_and :premises (@p607))
% 0.46/0.66  (step @p609 :rule eq_resolve :premises (@p608 @p433))
% 0.46/0.66  (step @p610 :rule refl :args (@t172))
% 0.46/0.66  (step @p611 :rule refl :args (@t103))
% 0.46/0.66  (step @p612 :rule nary_cong :premises (@p101 @p611 @p432 @p431 @p430 @p610) :args ((or @t41 @t103 @t171 @t102 @t175 @t172)))
% 0.46/0.66  (assume-push @p1354 @t15)
% 0.46/0.66  (assume-push @p1355 @t167)
% 0.46/0.66  (assume-push @p1356 @t66)
% 0.46/0.66  (assume-push @p1357 @t141)
% 0.46/0.66  (assume-push @p1358 @t174)
% 0.46/0.66  (assume-push @p1359 @t75)
% 0.46/0.66  (step @p182 :rule arith-elim-lt :args (@t45 -35))
% 0.46/0.66  (step @p183 :rule symm :premises (@p182))
% 0.46/0.66  (assume-push @p1360 @t75)
% 0.46/0.66  (step @p456 :rule evaluate :args (@t178))
% 0.46/0.66  (step @p620 :rule evaluate :args ((>= 0 -22)))
% 0.46/0.66  (step @p621 :rule evaluate :args ((+ 35 0 0 0 -55 -2)))
% 0.46/0.66  (step @p622 :rule evaluate :args (@t219))
% 0.46/0.66  (step @p623 :rule evaluate :args (@t220))
% 0.46/0.66  (step @p624 :rule evaluate :args (@t221))
% 0.46/0.66  (step @p625 :rule evaluate :args (@t222))
% 0.46/0.66  (step @p626 :rule evaluate :args (@t223))
% 0.46/0.66  (step @p191 :rule evaluate :args (@t81))
% 0.46/0.66  (step @p627 :rule nary_cong :premises (@p191 @p626 @p625 @p624 @p623 @p622) :args (@t224))
% 0.46/0.66  (step @p628 :rule trans :premises (@p627 @p621))
% 0.46/0.66  (step @p629 :rule arith_poly_norm :args ((= (+ @t46 @t233 @t232 @t231 @t228 @t225) 0)))
% 0.46/0.66  (step @p630 :rule arith_poly_norm :args ((= @t234 @t225)))
% 0.46/0.66  (step @p631 :rule arith_poly_norm :args ((= @t235 @t228)))
% 0.46/0.66  (step @p632 :rule arith_poly_norm :args ((= @t236 @t231)))
% 0.46/0.66  (step @p633 :rule arith_poly_norm :args ((= @t237 @t232)))
% 0.46/0.66  (step @p634 :rule arith_poly_norm :args ((= @t238 @t233)))
% 0.46/0.66  (step @p199 :rule refl :args (@t46))
% 0.46/0.66  (step @p635 :rule nary_cong :premises (@p199 @p634 @p633 @p632 @p631 @p630) :args (@t239))
% 0.46/0.66  (step @p636 :rule trans :premises (@p635 @p629))
% 0.46/0.66  (step @p637 :rule cong :premises (@p636 @p628) :args (@t240))
% 0.46/0.66  (step @p638 :rule trans :premises (@p637 @p620))
% 0.46/0.66  (step @p639 :rule cong :premises (@p638) :args ((not @t240)))
% 0.46/0.66  (step @p640 :rule trans :premises (@p639 @p456))
% 0.46/0.66  (step @p641 :rule arith-elim-lt :args (@t239 @t224))
% 0.46/0.66  (step @p642 :rule trans :premises (@p641 @p640))
% 0.46/0.66  (step @p643 :rule arith_mult_neg :args (-2 @t4))
% 0.46/0.66  (step @p644 :rule evaluate :args ((< -2 0)))
% 0.46/0.66  (step @p645 :rule true_elim :premises (@p644))
% 0.46/0.66  (step @p646 :rule and_intro :premises (@p645 @p1))
% 0.46/0.66  (step @p647 :rule modus_ponens :premises (@p646 @p643))
% 0.46/0.66  (step @p648 :rule arith_mult_neg :args (-55 @t167))
% 0.46/0.66  (step @p649 :rule evaluate :args ((< -55 0)))
% 0.46/0.66  (step @p650 :rule true_elim :premises (@p649))
% 0.46/0.66  (step @p651 :rule and_intro :premises (@p650 @p1355))
% 0.46/0.66  (step @p652 :rule modus_ponens :premises (@p651 @p648))
% 0.46/0.66  (step @p653 :rule arith_mult_pos :args (22 @t97))
% 0.46/0.66  (step @p220 :rule arith_poly_norm :args (@t98))
% 0.46/0.66  (step @p221 :rule arith_poly_norm_rel :premises (@p220) :args (@t99))
% 0.46/0.66  (step @p222 :rule symm :premises (@p221))
% 0.46/0.66  (step @p654 :rule eq_resolve :premises (@p1356 @p222))
% 0.46/0.66  (step @p655 :rule evaluate :args ((> 22 0)))
% 0.46/0.66  (step @p656 :rule true_elim :premises (@p655))
% 0.46/0.66  (step @p657 :rule and_intro :premises (@p656 @p654))
% 0.46/0.66  (step @p658 :rule modus_ponens :premises (@p657 @p653))
% 0.46/0.66  (step @p659 :rule arith_mult_pos :args (10 @t210))
% 0.46/0.66  (step @p528 :rule arith_poly_norm :args (@t212))
% 0.46/0.66  (step @p529 :rule arith_poly_norm_rel :premises (@p528) :args (@t213))
% 0.46/0.66  (step @p530 :rule symm :premises (@p529))
% 0.46/0.66  (step @p660 :rule eq_resolve :premises (@p1357 @p530))
% 0.46/0.66  (step @p661 :rule evaluate :args ((> 10 0)))
% 0.46/0.66  (step @p662 :rule true_elim :premises (@p661))
% 0.46/0.66  (step @p663 :rule and_intro :premises (@p662 @p660))
% 0.46/0.66  (step @p664 :rule modus_ponens :premises (@p663 @p659))
% 0.46/0.66  (step @p665 :rule arith_mult_pos :args (21 @t207))
% 0.46/0.66  (step @p510 :rule arith-elim-lt :args (@t169 0))
% 0.46/0.66  (step @p511 :rule symm :premises (@p510))
% 0.46/0.66  (step @p666 :rule eq_resolve :premises (@p1358 @p511))
% 0.46/0.66  (step @p667 :rule evaluate :args ((> 21 0)))
% 0.46/0.66  (step @p668 :rule true_elim :premises (@p667))
% 0.46/0.66  (step @p669 :rule and_intro :premises (@p668 @p666))
% 0.46/0.66  (step @p670 :rule modus_ponens :premises (@p669 @p665))
% 0.46/0.66  (step @p228 :rule arith_mult_neg :args (-1 @t75))
% 0.46/0.66  (step @p31 :rule evaluate :args (@t29))
% 0.46/0.66  (step @p32 :rule true_elim :premises (@p31))
% 0.46/0.66  (step @p229 :rule and_intro :premises (@p32 @p176))
% 0.46/0.66  (step @p230 :rule modus_ponens :premises (@p229 @p228))
% 0.46/0.66  (step @p671 :rule arith_sum_ub :premises (@p230 @p670 @p664 @p658 @p652 @p647))
% 0.46/0.66  (step @p672 false :rule eq_resolve :premises (@p671 @p642))
% 0.46/0.66  (step-pop @p1361 :rule scope :premises (@p672))
% 0.46/0.66  (step @p673 :rule process_scope :premises (@p1361) :args (false))
% 0.46/0.66  (step @p675 :rule eq_resolve :premises (@p673 @p183))
% 0.46/0.66  (step @p676 :rule eq_resolve :premises (@p675 @p182))
% 0.46/0.66  (step @p677 false :rule contra :premises (@p176 @p676))
% 0.46/0.66  (step-pop @p1362 :rule scope :premises (@p677))
% 0.46/0.66  (step-pop @p1363 :rule scope :premises (@p1362))
% 0.46/0.66  (step-pop @p1364 :rule scope :premises (@p1363))
% 0.46/0.66  (step-pop @p1365 :rule scope :premises (@p1364))
% 0.46/0.66  (step-pop @p1366 :rule scope :premises (@p1365))
% 0.46/0.66  (step-pop @p1367 :rule scope :premises (@p1366))
% 0.46/0.66  (step @p678 :rule process_scope :premises (@p1367) :args (false))
% 0.46/0.66  (assume-push @p1368 @t15)
% 0.46/0.66  (assume-push @p1369 @t75)
% 0.46/0.66  (assume-push @p1370 @t141)
% 0.46/0.66  (assume-push @p1371 @t66)
% 0.46/0.66  (assume-push @p1372 @t174)
% 0.46/0.66  (assume-push @p1373 @t167)
% 0.46/0.66  (step @p691 :rule and_intro :premises (@p6 @p1373 @p1371 @p1370 @p1372 @p176))
% 0.46/0.66  (step-pop @p1374 :rule scope :premises (@p691))
% 0.46/0.66  (step-pop @p1375 :rule scope :premises (@p1374))
% 0.46/0.66  (step-pop @p1376 :rule scope :premises (@p1375))
% 0.46/0.66  (step-pop @p1377 :rule scope :premises (@p1376))
% 0.46/0.66  (step-pop @p1378 :rule scope :premises (@p1377))
% 0.46/0.66  (step-pop @p1379 :rule scope :premises (@p1378))
% 0.46/0.66  (step @p692 :rule process_scope :premises (@p1379) :args (@t241))
% 0.46/0.66  (step @p699 :rule implies_elim :premises (@p692))
% 0.46/0.66  (step @p700 :rule resolution :premises (@p699 @p678) :args (true @t241))
% 0.46/0.66  (step @p701 :rule not_and :premises (@p700))
% 0.46/0.66  (step @p702 :rule eq_resolve :premises (@p701 @p612))
% 0.46/0.66  (step @p703 :rule reordering :premises (@p702) :args ((or @t103 @t41 @t171 @t102 @t170 @t172)))
% 0.46/0.66  (step @p704 :rule chain_m_resolution :premises (@p703 @p176 @p6 @p609 @p6) :args ((or @t171 @t102 @t170 @t168) (@list false false false false) (@list @t75 @t15 @t167 @t15)))
% 0.46/0.66  (assume-push @p1380 @t170)
% 0.46/0.66  (assume-push @p1381 @t15)
% 0.46/0.66  (assume-push @p1382 @t141)
% 0.46/0.66  (assume-push @p1383 @t66)
% 0.46/0.66  (assume-push @p1384 @t151)
% 0.46/0.66  (step @p710 :rule arith-elim-lt :args (tptp.b 2))
% 0.46/0.66  (step @p711 :rule symm :premises (@p710))
% 0.46/0.66  (assume-push @p1385 @t151)
% 0.46/0.66  (step @p185 :rule evaluate :args (@t76))
% 0.46/0.66  (step @p713 :rule evaluate :args ((+ -2 0 0 1 0)))
% 0.46/0.66  (step @p714 :rule evaluate :args (@t242))
% 0.46/0.66  (step @p16 :rule refl :args (1))
% 0.46/0.66  (step @p715 :rule evaluate :args (@t243))
% 0.46/0.66  (step @p716 :rule evaluate :args (@t244))
% 0.46/0.66  (step @p717 :rule nary_cong :premises (@p716 @p715 @p714 @p16 @p714) :args (@t245))
% 0.46/0.66  (step @p718 :rule trans :premises (@p717 @p713))
% 0.46/0.66  (step @p719 :rule arith_poly_norm :args ((= @t246 0)))
% 0.46/0.66  (step @p720 :rule arith_poly_norm :args ((= @t247 @t246)))
% 0.46/0.66  (step @p721 :rule trans :premises (@p720 @p719))
% 0.46/0.66  (step @p722 :rule cong :premises (@p721 @p718) :args ((<= @t247 @t245)))
% 0.46/0.66  (step @p723 :rule trans :premises (@p722 @p185))
% 0.46/0.66  (step @p724 :rule arith_mult_neg :args (-5 @t170))
% 0.46/0.66  (step @p26 :rule evaluate :args (@t28))
% 0.46/0.66  (step @p27 :rule true_elim :premises (@p26))
% 0.46/0.66  (step @p725 :rule and_intro :premises (@p27 @p1380))
% 0.46/0.66  (step @p726 :rule modus_ponens :premises (@p725 @p724))
% 0.46/0.66  (step @p727 :rule arith_mult_neg :args (-5 @t210))
% 0.46/0.66  (step @p528 :rule arith_poly_norm :args (@t212))
% 0.46/0.66  (step @p529 :rule arith_poly_norm_rel :premises (@p528) :args (@t213))
% 0.46/0.66  (step @p530 :rule symm :premises (@p529))
% 0.46/0.66  (step @p728 :rule eq_resolve :premises (@p1382 @p530))
% 0.46/0.66  (step @p729 :rule and_intro :premises (@p27 @p728))
% 0.46/0.66  (step @p730 :rule modus_ponens :premises (@p729 @p727))
% 0.46/0.66  (step @p731 :rule arith_mult_neg :args (-10 @t97))
% 0.46/0.66  (step @p220 :rule arith_poly_norm :args (@t98))
% 0.46/0.66  (step @p221 :rule arith_poly_norm_rel :premises (@p220) :args (@t99))
% 0.46/0.66  (step @p222 :rule symm :premises (@p221))
% 0.46/0.66  (step @p732 :rule eq_resolve :premises (@p1383 @p222))
% 0.46/0.66  (step @p733 :rule evaluate :args ((< -10 0)))
% 0.46/0.66  (step @p734 :rule true_elim :premises (@p733))
% 0.46/0.66  (step @p735 :rule and_intro :premises (@p734 @p732))
% 0.46/0.66  (step @p736 :rule modus_ponens :premises (@p735 @p731))
% 0.46/0.66  (step @p737 :rule arith_mult_neg :args (-1 @t151))
% 0.46/0.66  (step @p31 :rule evaluate :args (@t29))
% 0.46/0.66  (step @p32 :rule true_elim :premises (@p31))
% 0.46/0.66  (step @p738 :rule and_intro :premises (@p32 @p1384))
% 0.46/0.66  (step @p739 :rule modus_ponens :premises (@p738 @p737))
% 0.46/0.66  (step @p740 :rule arith_sum_ub :premises (@p739 @p736 @p730 @p1 @p726))
% 0.46/0.66  (step @p741 false :rule eq_resolve :premises (@p740 @p723))
% 0.46/0.66  (step-pop @p1386 :rule scope :premises (@p741))
% 0.46/0.66  (step @p742 :rule process_scope :premises (@p1386) :args (false))
% 0.46/0.66  (step @p744 :rule eq_resolve :premises (@p742 @p711))
% 0.46/0.66  (step @p745 :rule eq_resolve :premises (@p744 @p710))
% 0.46/0.66  (step @p746 false :rule contra :premises (@p1384 @p745))
% 0.46/0.66  (step-pop @p1387 :rule scope :premises (@p746))
% 0.46/0.66  (step-pop @p1388 :rule scope :premises (@p1387))
% 0.46/0.66  (step-pop @p1389 :rule scope :premises (@p1388))
% 0.46/0.66  (step-pop @p1390 :rule scope :premises (@p1389))
% 0.46/0.66  (step-pop @p1391 :rule scope :premises (@p1390))
% 0.46/0.66  (step @p747 :rule process_scope :premises (@p1391) :args (false))
% 0.46/0.66  (assume-push @p1392 @t15)
% 0.46/0.66  (assume-push @p1393 @t151)
% 0.46/0.66  (assume-push @p1394 @t141)
% 0.46/0.66  (assume-push @p1395 @t66)
% 0.46/0.66  (assume-push @p1396 @t170)
% 0.46/0.66  (step @p758 :rule and_intro :premises (@p1396 @p6 @p1394 @p1395 @p1393))
% 0.46/0.66  (step-pop @p1397 :rule scope :premises (@p758))
% 0.46/0.66  (step-pop @p1398 :rule scope :premises (@p1397))
% 0.46/0.66  (step-pop @p1399 :rule scope :premises (@p1398))
% 0.46/0.66  (step-pop @p1400 :rule scope :premises (@p1399))
% 0.46/0.66  (step-pop @p1401 :rule scope :premises (@p1400))
% 0.46/0.66  (step @p759 :rule process_scope :premises (@p1401) :args (@t248))
% 0.46/0.66  (step @p765 :rule implies_elim :premises (@p759))
% 0.46/0.66  (step @p766 :rule resolution :premises (@p765 @p747) :args (true @t248))
% 0.46/0.66  (step @p767 :rule not_and :premises (@p766))
% 0.46/0.66  (step @p768 :rule chain_m_resolution :premises (@p767 @p6 @p704 @p427 @p404 @p363 @p6 @p260) :args ((or @t152 @t171 @t102) (@list false false false false true false true) (@list @t15 @t170 @t157 @t153 @t104 @t15 @t18)))
% 0.46/0.66  (step @p769 :rule bool-double-not-elim :args (@t250))
% 0.46/0.66  (step @p770 :rule bool-double-not-elim :args (@t151))
% 0.46/0.66  (step @p771 :rule nary_cong :premises (@p431 @p101 @p770 @p611 @p769) :args ((or @t102 @t41 @t252 @t103 (not @t251))))
% 0.46/0.66  (assume-push @p1402 @t66)
% 0.46/0.66  (assume-push @p1403 @t15)
% 0.46/0.66  (assume-push @p1404 @t152)
% 0.46/0.66  (assume-push @p1405 @t75)
% 0.46/0.66  (assume-push @p1406 @t251)
% 0.46/0.66  (step @p456 :rule evaluate :args (@t178))
% 0.46/0.66  (step @p777 :rule evaluate :args (@t253))
% 0.46/0.66  (step @p778 :rule evaluate :args ((+ -33/1 0/1 -11/5 1/5 35/1)))
% 0.46/0.66  (step @p779 :rule evaluate :args ((to_real 35)))
% 0.46/0.66  (step @p191 :rule evaluate :args (@t81))
% 0.46/0.66  (step @p780 :rule cong :premises (@p191) :args (@t254))
% 0.46/0.66  (step @p781 :rule trans :premises (@p780 @p779))
% 0.46/0.66  (step @p782 :rule evaluate :args (@t255))
% 0.46/0.66  (step @p783 :rule evaluate :args (@t256))
% 0.46/0.66  (step @p784 :rule evaluate :args (@t122))
% 0.46/0.66  (step @p190 :rule evaluate :args (@t80))
% 0.46/0.66  (step @p785 :rule cong :premises (@p190) :args (@t257))
% 0.46/0.66  (step @p786 :rule trans :premises (@p785 @p784))
% 0.46/0.66  (step @p787 :rule evaluate :args ((to_real -33)))
% 0.46/0.66  (step @p788 :rule evaluate :args (@t258))
% 0.46/0.66  (step @p789 :rule cong :premises (@p788) :args (@t259))
% 0.46/0.66  (step @p790 :rule trans :premises (@p789 @p787))
% 0.46/0.66  (step @p791 :rule nary_cong :premises (@p790 @p786 @p783 @p782 @p781) :args (@t260))
% 0.46/0.66  (step @p792 :rule trans :premises (@p791 @p778))
% 0.46/0.66  (step @p793 :rule arith_poly_norm :args ((= (+ (to_real @t265) (to_real @t88) @t263 @t262 @t261) 0/1)))
% 0.46/0.66  (step @p794 :rule refl :args (@t261))
% 0.46/0.66  (step @p795 :rule refl :args (@t262))
% 0.46/0.66  (step @p796 :rule arith_poly_norm :args (@t267))
% 0.46/0.66  (step @p198 :rule arith_poly_norm :args (@t95))
% 0.46/0.66  (step @p797 :rule cong :premises (@p198) :args (@t268))
% 0.46/0.66  (step @p798 :rule arith_poly_norm :args ((= @t269 @t265)))
% 0.46/0.66  (step @p799 :rule cong :premises (@p798) :args (@t270))
% 0.46/0.66  (step @p800 :rule nary_cong :premises (@p799 @p797 @p796 @p795 @p794) :args (@t271))
% 0.46/0.66  (step @p801 :rule trans :premises (@p800 @p793))
% 0.46/0.66  (step @p802 :rule cong :premises (@p801 @p792) :args (@t272))
% 0.46/0.66  (step @p803 :rule trans :premises (@p802 @p777))
% 0.46/0.66  (step @p804 :rule cong :premises (@p803) :args ((not @t272)))
% 0.46/0.66  (step @p805 :rule trans :premises (@p804 @p456))
% 0.46/0.66  (step @p806 :rule arith-elim-lt :args (@t271 @t260))
% 0.46/0.66  (step @p807 :rule trans :premises (@p806 @p805))
% 0.46/0.66  (step @p808 :rule arith_poly_norm :args ((= (* -35/1 (to_real (- @t46 @t81))) (* -35/1 (- @t261 @t254)))))
% 0.46/0.66  (step @p809 :rule arith_poly_norm_rel :premises (@p808) :args ((= (<= @t46 @t81) (<= @t261 @t254))))
% 0.46/0.66  (step @p228 :rule arith_mult_neg :args (-1 @t75))
% 0.46/0.66  (step @p31 :rule evaluate :args (@t29))
% 0.46/0.66  (step @p32 :rule true_elim :premises (@p31))
% 0.46/0.66  (step @p229 :rule and_intro :premises (@p32 @p176))
% 0.46/0.66  (step @p230 :rule modus_ponens :premises (@p229 @p228))
% 0.46/0.66  (step @p810 :rule eq_resolve :premises (@p230 @p809))
% 0.46/0.66  (assume-push @p1407 @t273)
% 0.46/0.66  (assume-push @p1408 @t274)
% 0.46/0.66  (step @p813 :rule arith_mult_pos :args (1/5 @t275))
% 0.46/0.66  (step @p814 :rule evaluate :args (@t126))
% 0.46/0.66  (step @p815 :rule refl :args (@t185))
% 0.46/0.66  (step @p816 :rule cong :premises (@p815 @p814) :args (@t276))
% 0.46/0.66  (step @p817 :rule arith_poly_norm :args (@t277))
% 0.46/0.66  (step @p818 :rule arith_poly_norm_rel :premises (@p817) :args (@t278))
% 0.46/0.66  (step @p819 :rule trans :premises (@p818 @p816))
% 0.46/0.66  (step @p820 :rule eq_resolve :premises (@p1408 @p819))
% 0.46/0.66  (step @p821 :rule and_intro :premises (@p1407 @p820))
% 0.46/0.66  (step @p822 :rule modus_ponens :premises (@p821 @p813))
% 0.46/0.66  (step-pop @p1409 :rule scope :premises (@p822))
% 0.46/0.66  (step-pop @p1410 :rule scope :premises (@p1409))
% 0.46/0.66  (step @p823 :rule process_scope :premises (@p1410) :args ((<= @t262 @t255)))
% 0.46/0.66  (step @p710 :rule arith-elim-lt :args (tptp.b 2))
% 0.46/0.66  (step @p711 :rule symm :premises (@p710))
% 0.46/0.66  (step @p826 :rule eq_resolve :premises (@p1404 @p711))
% 0.46/0.66  (step @p827 :rule int_tight_ub :premises (@p826))
% 0.46/0.66  (step @p828 :rule evaluate :args (@t273))
% 0.46/0.66  (step @p829 :rule true_elim :premises (@p828))
% 0.46/0.66  (step @p830 :rule and_intro :premises (@p829 @p827))
% 0.46/0.66  (step @p831 :rule modus_ponens :premises (@p830 @p823))
% 0.46/0.66  (assume-push @p1411 @t279)
% 0.46/0.66  (assume-push @p1412 @t4)
% 0.46/0.66  (step @p834 :rule arith_mult_neg :args (-11/5 @t125))
% 0.46/0.66  (step @p835 :rule evaluate :args (@t126))
% 0.46/0.66  (step @p836 :rule cong :premises (@p1) :args (@t117))
% 0.46/0.66  (step @p837 :rule trans :premises (@p836 @p835))
% 0.46/0.66  (step @p838 :rule and_intro :premises (@p1411 @p837))
% 0.46/0.66  (step @p839 :rule modus_ponens :premises (@p838 @p834))
% 0.46/0.66  (step-pop @p1413 :rule scope :premises (@p839))
% 0.46/0.66  (step-pop @p1414 :rule scope :premises (@p1413))
% 0.46/0.66  (step @p840 :rule process_scope :premises (@p1414) :args (@t280))
% 0.46/0.66  (step @p843 :rule evaluate :args (@t279))
% 0.46/0.66  (step @p844 :rule true_elim :premises (@p843))
% 0.46/0.66  (step @p845 :rule and_intro :premises (@p844 @p1))
% 0.46/0.66  (step @p846 :rule modus_ponens :premises (@p845 @p840))
% 0.46/0.66  (step @p219 :rule arith_mult_pos :args (2 @t97))
% 0.46/0.66  (step @p220 :rule arith_poly_norm :args (@t98))
% 0.46/0.66  (step @p221 :rule arith_poly_norm_rel :premises (@p220) :args (@t99))
% 0.46/0.66  (step @p222 :rule symm :premises (@p221))
% 0.46/0.66  (step @p847 :rule eq_resolve :premises (@p1402 @p222))
% 0.46/0.66  (step @p224 :rule evaluate :args (@t100))
% 0.46/0.66  (step @p225 :rule true_elim :premises (@p224))
% 0.46/0.66  (step @p848 :rule and_intro :premises (@p225 @p847))
% 0.46/0.66  (step @p849 :rule modus_ponens :premises (@p848 @p219))
% 0.46/0.66  (step @p850 :rule cong :premises (@p849) :args (@t268))
% 0.46/0.66  (step @p851 :rule arith_poly_norm :args ((= (* 33/1 (to_real (- @t269 @t258))) (* 33/1 (- @t270 @t259)))))
% 0.46/0.66  (step @p852 :rule arith_poly_norm_rel :premises (@p851) :args ((= (< @t269 @t258) (< @t270 @t259))))
% 0.46/0.66  (step @p853 :rule arith_mult_pos :args (11 (< @t249 -3)))
% 0.46/0.66  (step @p854 :rule arith-elim-lt :args (@t249 -3))
% 0.46/0.66  (step @p855 :rule symm :premises (@p854))
% 0.46/0.66  (step @p856 :rule eq_resolve :premises (@p1406 @p855))
% 0.46/0.66  (step @p857 :rule evaluate :args (@t281))
% 0.46/0.66  (step @p858 :rule true_elim :premises (@p857))
% 0.46/0.66  (step @p859 :rule and_intro :premises (@p858 @p856))
% 0.46/0.66  (step @p860 :rule modus_ponens :premises (@p859 @p853))
% 0.46/0.66  (step @p861 :rule eq_resolve :premises (@p860 @p852))
% 0.46/0.66  (step @p862 :rule arith_sum_ub :premises (@p861 @p850 @p846 @p831 @p810))
% 0.46/0.66  (step @p863 false :rule eq_resolve :premises (@p862 @p807))
% 0.46/0.66  (step-pop @p1415 :rule scope :premises (@p863))
% 0.46/0.66  (step-pop @p1416 :rule scope :premises (@p1415))
% 0.46/0.66  (step-pop @p1417 :rule scope :premises (@p1416))
% 0.46/0.66  (step-pop @p1418 :rule scope :premises (@p1417))
% 0.46/0.66  (step-pop @p1419 :rule scope :premises (@p1418))
% 0.46/0.66  (step @p864 :rule process_scope :premises (@p1419) :args (false))
% 0.46/0.66  (step @p870 :rule not_and :premises (@p864))
% 0.46/0.66  (step @p871 :rule eq_resolve :premises (@p870 @p771))
% 0.46/0.66  (step @p872 :rule reordering :premises (@p871) :args ((or @t103 @t41 @t151 @t102 @t250)))
% 0.46/0.66  (step @p873 :rule bool-double-not-elim :args (@t282))
% 0.46/0.66  (step @p874 :rule nary_cong :premises (@p101 @p261 @p873) :args ((or @t41 @t106 (not @t283))))
% 0.46/0.66  (assume-push @p1420 @t15)
% 0.46/0.66  (assume-push @p1421 @t38)
% 0.46/0.66  (assume-push @p1422 @t283)
% 0.46/0.66  (step @p456 :rule evaluate :args (@t178))
% 0.46/0.66  (step @p777 :rule evaluate :args (@t253))
% 0.46/0.66  (step @p878 :rule evaluate :args ((+ 1/5 -1/5 0/1)))
% 0.46/0.66  (step @p879 :rule refl :args (0/1))
% 0.46/0.66  (step @p880 :rule evaluate :args (@t284))
% 0.46/0.66  (step @p782 :rule evaluate :args (@t255))
% 0.46/0.66  (step @p881 :rule nary_cong :premises (@p782 @p880 @p879) :args (@t285))
% 0.46/0.66  (step @p882 :rule trans :premises (@p881 @p878))
% 0.46/0.66  (step @p883 :rule arith_poly_norm :args ((= @t286 0/1)))
% 0.46/0.66  (step @p884 :rule arith_poly_norm :args ((= @t288 @t286)))
% 0.46/0.66  (step @p885 :rule trans :premises (@p884 @p883))
% 0.46/0.66  (step @p886 :rule cong :premises (@p885 @p882) :args (@t289))
% 0.46/0.66  (step @p887 :rule trans :premises (@p886 @p777))
% 0.46/0.66  (step @p888 :rule cong :premises (@p887) :args ((not @t289)))
% 0.46/0.66  (step @p889 :rule trans :premises (@p888 @p456))
% 0.46/0.66  (step @p890 :rule arith-elim-lt :args (@t288 @t285))
% 0.46/0.66  (step @p891 :rule trans :premises (@p890 @p889))
% 0.46/0.66  (step @p892 :rule evaluate :args (@t122))
% 0.46/0.66  (step @p893 :rule refl :args (@t119))
% 0.46/0.66  (step @p894 :rule cong :premises (@p893 @p892) :args (@t127))
% 0.46/0.66  (step @p333 :rule arith_poly_norm :args (@t128))
% 0.46/0.66  (step @p895 :rule arith_poly_norm_rel :premises (@p333) :args (@t129))
% 0.46/0.66  (step @p896 :rule trans :premises (@p895 @p894))
% 0.46/0.66  (step @p343 :rule arith-elim-lt :args (@t17 1))
% 0.46/0.66  (step @p344 :rule symm :premises (@p343))
% 0.46/0.66  (step @p897 :rule eq_resolve :premises (@p1421 @p344))
% 0.46/0.66  (step @p898 :rule int_tight_ub :premises (@p897))
% 0.46/0.66  (step @p899 :rule eq_resolve :premises (@p898 @p896))
% 0.46/0.66  (assume-push @p1423 @t290)
% 0.46/0.66  (assume-push @p1424 @t4)
% 0.46/0.66  (step @p902 :rule arith_mult_neg :args (-1/5 @t125))
% 0.46/0.66  (step @p903 :rule evaluate :args (@t126))
% 0.46/0.66  (step @p904 :rule cong :premises (@p1) :args (@t117))
% 0.46/0.66  (step @p905 :rule trans :premises (@p904 @p903))
% 0.46/0.66  (step @p906 :rule and_intro :premises (@p1423 @p905))
% 0.46/0.66  (step @p907 :rule modus_ponens :premises (@p906 @p902))
% 0.46/0.66  (step-pop @p1425 :rule scope :premises (@p907))
% 0.46/0.66  (step-pop @p1426 :rule scope :premises (@p1425))
% 0.46/0.66  (step @p908 :rule process_scope :premises (@p1426) :args ((= @t287 @t284)))
% 0.46/0.66  (step @p911 :rule evaluate :args (@t290))
% 0.46/0.66  (step @p912 :rule true_elim :premises (@p911))
% 0.46/0.66  (step @p913 :rule and_intro :premises (@p912 @p1))
% 0.46/0.66  (step @p914 :rule modus_ponens :premises (@p913 @p908))
% 0.46/0.66  (assume-push @p1427 @t273)
% 0.46/0.66  (assume-push @p1428 @t291)
% 0.46/0.66  (step @p917 :rule arith_mult_pos :args (1/5 (< @t185 1/1)))
% 0.46/0.66  (step @p918 :rule evaluate :args (@t126))
% 0.46/0.66  (step @p919 :rule refl :args (@t185))
% 0.46/0.66  (step @p920 :rule cong :premises (@p919 @p918) :args (@t292))
% 0.46/0.66  (step @p817 :rule arith_poly_norm :args (@t277))
% 0.46/0.66  (step @p921 :rule arith_poly_norm_rel :premises (@p817) :args ((= @t291 @t292)))
% 0.46/0.66  (step @p922 :rule trans :premises (@p921 @p920))
% 0.46/0.66  (step @p923 :rule eq_resolve :premises (@p1428 @p922))
% 0.46/0.66  (step @p924 :rule and_intro :premises (@p1427 @p923))
% 0.46/0.66  (step @p925 :rule modus_ponens :premises (@p924 @p917))
% 0.46/0.66  (step-pop @p1429 :rule scope :premises (@p925))
% 0.46/0.66  (step-pop @p1430 :rule scope :premises (@p1429))
% 0.46/0.66  (step @p926 :rule process_scope :premises (@p1430) :args ((< @t262 @t255)))
% 0.46/0.66  (step @p929 :rule arith-elim-lt :args (tptp.b 1))
% 0.46/0.66  (step @p930 :rule symm :premises (@p929))
% 0.46/0.66  (step @p931 :rule eq_resolve :premises (@p1422 @p930))
% 0.46/0.66  (step @p828 :rule evaluate :args (@t273))
% 0.46/0.66  (step @p829 :rule true_elim :premises (@p828))
% 0.46/0.66  (step @p932 :rule and_intro :premises (@p829 @p931))
% 0.46/0.66  (step @p933 :rule modus_ponens :premises (@p932 @p926))
% 0.46/0.66  (step @p934 :rule arith_sum_ub :premises (@p933 @p914 @p899))
% 0.46/0.66  (step @p935 false :rule eq_resolve :premises (@p934 @p891))
% 0.46/0.66  (step-pop @p1431 :rule scope :premises (@p935))
% 0.46/0.66  (step-pop @p1432 :rule scope :premises (@p1431))
% 0.46/0.66  (step-pop @p1433 :rule scope :premises (@p1432))
% 0.46/0.66  (step @p936 :rule process_scope :premises (@p1433) :args (false))
% 0.46/0.66  (step @p940 :rule not_and :premises (@p936))
% 0.46/0.66  (step @p941 :rule eq_resolve :premises (@p940 @p874))
% 0.46/0.66  (step @p942 :rule chain_m_resolution :premises (@p941 @p6 @p260) :args (@t282 @t131 @t132))
% 0.46/0.66  (assume-push @p1434 @t282)
% 0.46/0.66  (assume-push @p1435 @t250)
% 0.46/0.66  (assume-push @p1436 @t15)
% 0.46/0.66  (assume-push @p1437 @t141)
% 0.46/0.66  (assume-push @p1438 @t66)
% 0.46/0.66  (assume-push @p1439 @t167)
% 0.46/0.66  (step @p949 :rule evaluate :args ((<= 0/1 -2/5)))
% 0.46/0.66  (step @p950 :rule evaluate :args ((+ -1/1 -2/25 3/5 2/25 0/1 0/1)))
% 0.46/0.66  (step @p951 :rule evaluate :args (@t293))
% 0.46/0.66  (step @p952 :rule evaluate :args (@t294))
% 0.46/0.66  (step @p953 :rule evaluate :args (@t295))
% 0.46/0.66  (step @p954 :rule evaluate :args (@t296))
% 0.46/0.66  (step @p955 :rule evaluate :args (@t297))
% 0.46/0.66  (step @p956 :rule evaluate :args ((to_real -1)))
% 0.46/0.66  (step @p957 :rule evaluate :args (@t298))
% 0.46/0.66  (step @p958 :rule cong :premises (@p957) :args (@t299))
% 0.46/0.66  (step @p959 :rule trans :premises (@p958 @p956))
% 0.46/0.66  (step @p960 :rule nary_cong :premises (@p959 @p955 @p954 @p953 @p952 @p951) :args (@t300))
% 0.46/0.66  (step @p961 :rule trans :premises (@p960 @p950))
% 0.46/0.66  (step @p962 :rule arith_poly_norm :args ((= (+ (to_real @t307) @t306 @t305 @t304 @t303 @t301) 0/1)))
% 0.46/0.66  (step @p963 :rule arith_poly_norm :args ((= @t308 @t301)))
% 0.46/0.66  (step @p964 :rule arith_poly_norm :args ((= @t309 @t303)))
% 0.46/0.66  (step @p965 :rule arith_poly_norm :args ((= @t310 @t304)))
% 0.46/0.66  (step @p966 :rule arith_poly_norm :args ((= @t312 @t305)))
% 0.46/0.66  (step @p967 :rule refl :args (@t306))
% 0.46/0.66  (step @p968 :rule arith_poly_norm :args ((= @t313 @t307)))
% 0.46/0.66  (step @p969 :rule cong :premises (@p968) :args (@t314))
% 0.46/0.66  (step @p970 :rule nary_cong :premises (@p969 @p967 @p966 @p965 @p964 @p963) :args (@t315))
% 0.46/0.66  (step @p971 :rule trans :premises (@p970 @p962))
% 0.46/0.66  (step @p972 :rule cong :premises (@p971 @p961) :args ((<= @t315 @t300)))
% 0.46/0.66  (step @p973 :rule trans :premises (@p972 @p949))
% 0.46/0.66  (assume-push @p1440 @t316)
% 0.46/0.66  (assume-push @p1441 @t97)
% 0.46/0.66  (step @p976 :rule arith_mult_neg :args (-2/5 @t215))
% 0.46/0.66  (step @p977 :rule evaluate :args (@t122))
% 0.46/0.66  (step @p978 :rule cong :premises (@p1441) :args (@t198))
% 0.46/0.66  (step @p979 :rule trans :premises (@p978 @p977))
% 0.46/0.66  (step @p980 :rule and_intro :premises (@p1440 @p979))
% 0.46/0.66  (step @p981 :rule modus_ponens :premises (@p980 @p976))
% 0.46/0.66  (step-pop @p1442 :rule scope :premises (@p981))
% 0.46/0.66  (step-pop @p1443 :rule scope :premises (@p1442))
% 0.46/0.66  (step @p982 :rule process_scope :premises (@p1443) :args ((= @t308 @t293)))
% 0.46/0.66  (step @p220 :rule arith_poly_norm :args (@t98))
% 0.46/0.66  (step @p221 :rule arith_poly_norm_rel :premises (@p220) :args (@t99))
% 0.46/0.66  (step @p222 :rule symm :premises (@p221))
% 0.46/0.66  (step @p985 :rule eq_resolve :premises (@p1438 @p222))
% 0.46/0.66  (step @p986 :rule evaluate :args (@t316))
% 0.46/0.66  (step @p987 :rule true_elim :premises (@p986))
% 0.46/0.66  (step @p988 :rule and_intro :premises (@p987 @p985))
% 0.46/0.66  (step @p989 :rule modus_ponens :premises (@p988 @p982))
% 0.46/0.66  (assume-push @p1444 @t290)
% 0.46/0.66  (assume-push @p1445 @t210)
% 0.46/0.66  (step @p992 :rule arith_mult_neg :args (-1/5 @t211))
% 0.46/0.66  (step @p993 :rule evaluate :args (@t122))
% 0.46/0.66  (step @p994 :rule cong :premises (@p1445) :args (@t196))
% 0.46/0.66  (step @p995 :rule trans :premises (@p994 @p993))
% 0.46/0.66  (step @p996 :rule and_intro :premises (@p1444 @p995))
% 0.46/0.66  (step @p997 :rule modus_ponens :premises (@p996 @p992))
% 0.46/0.66  (step-pop @p1446 :rule scope :premises (@p997))
% 0.46/0.66  (step-pop @p1447 :rule scope :premises (@p1446))
% 0.46/0.66  (step @p998 :rule process_scope :premises (@p1447) :args ((= @t309 @t294)))
% 0.46/0.66  (step @p528 :rule arith_poly_norm :args (@t212))
% 0.46/0.66  (step @p529 :rule arith_poly_norm_rel :premises (@p528) :args (@t213))
% 0.46/0.66  (step @p530 :rule symm :premises (@p529))
% 0.46/0.66  (step @p1001 :rule eq_resolve :premises (@p1437 @p530))
% 0.46/0.66  (step @p911 :rule evaluate :args (@t290))
% 0.46/0.66  (step @p912 :rule true_elim :premises (@p911))
% 0.46/0.66  (step @p1002 :rule and_intro :premises (@p912 @p1001))
% 0.46/0.66  (step @p1003 :rule modus_ponens :premises (@p1002 @p998))
% 0.46/0.66  (assume-push @p1448 @t317)
% 0.46/0.66  (assume-push @p1449 @t4)
% 0.46/0.66  (step @p1006 :rule arith_mult_pos :args (2/25 @t125))
% 0.46/0.66  (step @p1007 :rule evaluate :args (@t126))
% 0.46/0.66  (step @p1008 :rule cong :premises (@p1) :args (@t117))
% 0.46/0.66  (step @p1009 :rule trans :premises (@p1008 @p1007))
% 0.46/0.66  (step @p1010 :rule and_intro :premises (@p1448 @p1009))
% 0.46/0.66  (step @p1011 :rule modus_ponens :premises (@p1010 @p1006))
% 0.46/0.66  (step-pop @p1450 :rule scope :premises (@p1011))
% 0.46/0.66  (step-pop @p1451 :rule scope :premises (@p1450))
% 0.46/0.67  (step @p1012 :rule process_scope :premises (@p1451) :args ((= @t310 @t295)))
% 0.46/0.67  (step @p1015 :rule evaluate :args (@t317))
% 0.46/0.67  (step @p1016 :rule true_elim :premises (@p1015))
% 0.46/0.67  (step @p1017 :rule and_intro :premises (@p1016 @p1))
% 0.46/0.67  (step @p1018 :rule modus_ponens :premises (@p1017 @p1012))
% 0.46/0.67  (assume-push @p1452 @t290)
% 0.46/0.67  (assume-push @p1453 @t250)
% 0.46/0.67  (step @p1021 :rule arith_mult_neg :args (-1/5 (>= @t311 -3/1)))
% 0.46/0.67  (step @p1022 :rule evaluate :args (@t318))
% 0.46/0.67  (step @p1023 :rule refl :args (@t311))
% 0.46/0.67  (step @p1024 :rule cong :premises (@p1023 @p1022) :args (@t319))
% 0.46/0.67  (step @p1025 :rule arith_poly_norm :args ((= (* 3/1 (to_real (- @t249 -3))) (* 3/1 (- @t311 @t318)))))
% 0.46/0.67  (step @p1026 :rule arith_poly_norm_rel :premises (@p1025) :args ((= @t250 @t319)))
% 0.46/0.67  (step @p1027 :rule trans :premises (@p1026 @p1024))
% 0.46/0.67  (step @p1028 :rule eq_resolve :premises (@p1435 @p1027))
% 0.46/0.67  (step @p1029 :rule and_intro :premises (@p1452 @p1028))
% 0.46/0.67  (step @p1030 :rule modus_ponens :premises (@p1029 @p1021))
% 0.46/0.67  (step-pop @p1454 :rule scope :premises (@p1030))
% 0.46/0.67  (step-pop @p1455 :rule scope :premises (@p1454))
% 0.46/0.67  (step @p1031 :rule process_scope :premises (@p1455) :args ((<= @t312 @t296)))
% 0.46/0.67  (step @p1034 :rule and_intro :premises (@p912 @p1435))
% 0.46/0.67  (step @p1035 :rule modus_ponens :premises (@p1034 @p1031))
% 0.46/0.67  (assume-push @p1456 @t320)
% 0.46/0.67  (assume-push @p1457 @t282)
% 0.46/0.67  (step @p1038 :rule arith_mult_neg :args (-2/25 (>= @t185 1/1)))
% 0.46/0.67  (step @p1039 :rule evaluate :args (@t126))
% 0.46/0.67  (step @p1040 :rule refl :args (@t185))
% 0.46/0.67  (step @p1041 :rule cong :premises (@p1040 @p1039) :args (@t321))
% 0.46/0.67  (step @p817 :rule arith_poly_norm :args (@t277))
% 0.46/0.67  (step @p1042 :rule arith_poly_norm_rel :premises (@p817) :args ((= @t282 @t321)))
% 0.46/0.67  (step @p1043 :rule trans :premises (@p1042 @p1041))
% 0.46/0.67  (step @p1044 :rule eq_resolve :premises (@p1434 @p1043))
% 0.46/0.67  (step @p1045 :rule and_intro :premises (@p1456 @p1044))
% 0.46/0.67  (step @p1046 :rule modus_ponens :premises (@p1045 @p1038))
% 0.46/0.67  (step-pop @p1458 :rule scope :premises (@p1046))
% 0.46/0.67  (step-pop @p1459 :rule scope :premises (@p1458))
% 0.46/0.67  (step @p1047 :rule process_scope :premises (@p1459) :args ((<= @t306 @t297)))
% 0.46/0.67  (step @p1050 :rule evaluate :args (@t320))
% 0.46/0.67  (step @p1051 :rule true_elim :premises (@p1050))
% 0.46/0.67  (step @p1052 :rule and_intro :premises (@p1051 @p1434))
% 0.46/0.67  (step @p1053 :rule modus_ponens :premises (@p1052 @p1047))
% 0.46/0.67  (step @p1054 :rule arith_poly_norm :args ((= (* 1/1 (to_real (- @t313 @t298))) (* 1/1 (- @t314 @t299)))))
% 0.46/0.67  (step @p1055 :rule arith_poly_norm_rel :premises (@p1054) :args ((= (<= @t313 @t298) (<= @t314 @t299))))
% 0.46/0.67  (step @p1056 :rule arith_mult_neg :args (-1 @t167))
% 0.46/0.67  (step @p31 :rule evaluate :args (@t29))
% 0.46/0.67  (step @p32 :rule true_elim :premises (@p31))
% 0.46/0.67  (step @p1057 :rule and_intro :premises (@p32 @p1439))
% 0.46/0.67  (step @p1058 :rule modus_ponens :premises (@p1057 @p1056))
% 0.46/0.67  (step @p1059 :rule eq_resolve :premises (@p1058 @p1055))
% 0.46/0.67  (step @p1060 :rule arith_sum_ub :premises (@p1059 @p1053 @p1035 @p1018 @p1003 @p989))
% 0.46/0.67  (step @p1061 false :rule eq_resolve :premises (@p1060 @p973))
% 0.46/0.67  (step-pop @p1460 :rule scope :premises (@p1061))
% 0.46/0.67  (step-pop @p1461 :rule scope :premises (@p1460))
% 0.46/0.67  (step-pop @p1462 :rule scope :premises (@p1461))
% 0.46/0.67  (step-pop @p1463 :rule scope :premises (@p1462))
% 0.46/0.67  (step-pop @p1464 :rule scope :premises (@p1463))
% 0.46/0.67  (step-pop @p1465 :rule scope :premises (@p1464))
% 0.46/0.67  (step @p1062 :rule process_scope :premises (@p1465) :args (false))
% 0.46/0.67  (step @p1069 :rule not_and :premises (@p1062))
% 0.46/0.67  (step @p1070 :rule reordering :premises (@p1069) :args ((or @t41 @t283 @t171 @t102 @t172 @t251)))
% 0.46/0.67  (step @p1071 :rule not_or_elim :premises (@p174) :args (0))
% 0.46/0.67  (step @p1072 :rule bool-double-not-elim :args (@t322))
% 0.46/0.67  (step @p1073 :rule nary_cong :premises (@p101 @p1072 @p770 @p432 @p431 @p428) :args ((or @t41 (not @t323) @t252 @t171 @t102 @t173)))
% 0.46/0.67  (assume-push @p1466 @t172)
% 0.46/0.67  (assume-push @p1467 @t152)
% 0.46/0.67  (assume-push @p1468 @t15)
% 0.46/0.67  (assume-push @p1469 @t66)
% 0.46/0.67  (assume-push @p1470 @t141)
% 0.46/0.67  (assume-push @p1471 @t323)
% 0.46/0.67  (step @p1080 :rule arith-elim-lt :args (@t45 -2))
% 0.46/0.67  (step @p1081 :rule cong :premises (@p1080) :args ((not @t324)))
% 0.46/0.67  (step @p1082 :rule trans :premises (@p1081 @p1072))
% 0.46/0.67  (step @p1083 :rule symm :premises (@p1082))
% 0.46/0.67  (assume-push @p1472 @t324)
% 0.46/0.67  (step @p456 :rule evaluate :args (@t178))
% 0.46/0.67  (step @p777 :rule evaluate :args (@t253))
% 0.46/0.67  (step @p1085 :rule evaluate :args ((+ -2/1 0/1 0/1 -11/5 21/5 0/1)))
% 0.46/0.67  (step @p1086 :rule evaluate :args (@t122))
% 0.46/0.67  (step @p1087 :rule evaluate :args (@t325))
% 0.46/0.67  (step @p1088 :rule cong :premises (@p1087) :args (@t326))
% 0.46/0.67  (step @p1089 :rule trans :premises (@p1088 @p1086))
% 0.46/0.67  (step @p1090 :rule evaluate :args (@t327))
% 0.46/0.67  (step @p783 :rule evaluate :args (@t256))
% 0.46/0.67  (step @p1091 :rule evaluate :args (@t328))
% 0.46/0.67  (step @p1092 :rule cong :premises (@p1091) :args (@t329))
% 0.46/0.67  (step @p1093 :rule trans :premises (@p1092 @p1086))
% 0.46/0.67  (step @p1094 :rule evaluate :args (@t330))
% 0.46/0.67  (step @p1095 :rule cong :premises (@p1094) :args (@t331))
% 0.46/0.67  (step @p1096 :rule trans :premises (@p1095 @p1086))
% 0.46/0.67  (step @p1097 :rule refl :args (-2/1))
% 0.46/0.67  (step @p1098 :rule nary_cong :premises (@p1097 @p1096 @p1093 @p783 @p1090 @p1089) :args (@t332))
% 0.46/0.67  (step @p1099 :rule trans :premises (@p1098 @p1085))
% 0.46/0.67  (step @p1100 :rule arith_poly_norm :args ((= (+ @t187 (to_real @t336) (to_real @t335) @t263 @t334 (to_real @t333)) 0/1)))
% 0.46/0.67  (step @p1101 :rule arith_poly_norm :args ((= @t337 @t333)))
% 0.46/0.67  (step @p1102 :rule cong :premises (@p1101) :args (@t338))
% 0.46/0.67  (step @p1103 :rule refl :args (@t334))
% 0.46/0.67  (step @p796 :rule arith_poly_norm :args (@t267))
% 0.46/0.67  (step @p1104 :rule arith_poly_norm :args ((= @t339 @t335)))
% 0.46/0.67  (step @p1105 :rule cong :premises (@p1104) :args (@t340))
% 0.46/0.67  (step @p1106 :rule arith_poly_norm :args ((= @t341 @t336)))
% 0.46/0.67  (step @p1107 :rule cong :premises (@p1106) :args (@t342))
% 0.46/0.67  (step @p1108 :rule refl :args (@t187))
% 0.46/0.67  (step @p1109 :rule nary_cong :premises (@p1108 @p1107 @p1105 @p796 @p1103 @p1102) :args (@t343))
% 0.46/0.67  (step @p1110 :rule trans :premises (@p1109 @p1100))
% 0.46/0.67  (step @p1111 :rule cong :premises (@p1110 @p1099) :args (@t344))
% 0.46/0.67  (step @p1112 :rule trans :premises (@p1111 @p777))
% 0.46/0.67  (step @p1113 :rule cong :premises (@p1112) :args ((not @t344)))
% 0.46/0.67  (step @p1114 :rule trans :premises (@p1113 @p456))
% 0.46/0.67  (step @p1115 :rule arith-elim-lt :args (@t343 @t332))
% 0.46/0.67  (step @p1116 :rule trans :premises (@p1115 @p1114))
% 0.46/0.67  (step @p1117 :rule arith_poly_norm :args ((= (* 220/1 (to_real (- @t337 @t325))) (* 220/1 (- @t338 @t326)))))
% 0.46/0.67  (step @p1118 :rule arith_poly_norm_rel :premises (@p1117) :args ((= (<= @t337 @t325) (<= @t338 @t326))))
% 0.46/0.67  (step @p1119 :rule arith_mult_pos :args (55 @t177))
% 0.46/0.67  (step @p580 :rule arith-elim-lt :args (@t166 1))
% 0.46/0.67  (step @p581 :rule symm :premises (@p580))
% 0.46/0.67  (step @p1120 :rule eq_resolve :premises (@p1466 @p581))
% 0.46/0.67  (step @p1121 :rule int_tight_ub :premises (@p1120))
% 0.46/0.67  (step @p1122 :rule evaluate :args ((> 55 0)))
% 0.46/0.67  (step @p1123 :rule true_elim :premises (@p1122))
% 0.46/0.67  (step @p1124 :rule and_intro :premises (@p1123 @p1121))
% 0.46/0.67  (step @p1125 :rule modus_ponens :premises (@p1124 @p1119))
% 0.46/0.67  (step @p1126 :rule eq_resolve :premises (@p1125 @p1118))
% 0.46/0.67  (assume-push @p1473 @t345)
% 0.46/0.67  (assume-push @p1474 @t274)
% 0.46/0.67  (step @p1129 :rule arith_mult_pos :args (21/5 @t275))
% 0.46/0.67  (step @p1130 :rule evaluate :args (@t126))
% 0.46/0.67  (step @p1131 :rule refl :args (@t185))
% 0.46/0.67  (step @p1132 :rule cong :premises (@p1131 @p1130) :args (@t276))
% 0.46/0.67  (step @p817 :rule arith_poly_norm :args (@t277))
% 0.46/0.67  (step @p1133 :rule arith_poly_norm_rel :premises (@p817) :args (@t278))
% 0.46/0.67  (step @p1134 :rule trans :premises (@p1133 @p1132))
% 0.46/0.67  (step @p1135 :rule eq_resolve :premises (@p1474 @p1134))
% 0.46/0.67  (step @p1136 :rule and_intro :premises (@p1473 @p1135))
% 0.46/0.67  (step @p1137 :rule modus_ponens :premises (@p1136 @p1129))
% 0.46/0.67  (step-pop @p1475 :rule scope :premises (@p1137))
% 0.46/0.67  (step-pop @p1476 :rule scope :premises (@p1475))
% 0.46/0.67  (step @p1138 :rule process_scope :premises (@p1476) :args ((<= @t334 @t327)))
% 0.46/0.67  (step @p710 :rule arith-elim-lt :args (tptp.b 2))
% 0.46/0.67  (step @p711 :rule symm :premises (@p710))
% 0.46/0.67  (step @p1141 :rule eq_resolve :premises (@p1467 @p711))
% 0.46/0.67  (step @p1142 :rule int_tight_ub :premises (@p1141))
% 0.46/0.67  (step @p1143 :rule evaluate :args (@t345))
% 0.46/0.67  (step @p1144 :rule true_elim :premises (@p1143))
% 0.46/0.67  (step @p1145 :rule and_intro :premises (@p1144 @p1142))
% 0.46/0.67  (step @p1146 :rule modus_ponens :premises (@p1145 @p1138))
% 0.46/0.67  (assume-push @p1477 @t279)
% 0.46/0.67  (assume-push @p1478 @t4)
% 0.46/0.67  (step @p834 :rule arith_mult_neg :args (-11/5 @t125))
% 0.46/0.67  (step @p835 :rule evaluate :args (@t126))
% 0.46/0.67  (step @p836 :rule cong :premises (@p1) :args (@t117))
% 0.46/0.67  (step @p837 :rule trans :premises (@p836 @p835))
% 0.46/0.67  (step @p838 :rule and_intro :premises (@p1477 @p837))
% 0.46/0.67  (step @p839 :rule modus_ponens :premises (@p838 @p834))
% 0.46/0.67  (step-pop @p1479 :rule scope :premises (@p839))
% 0.46/0.67  (step-pop @p1480 :rule scope :premises (@p1479))
% 0.46/0.67  (step @p840 :rule process_scope :premises (@p1480) :args (@t280))
% 0.46/0.67  (step @p843 :rule evaluate :args (@t279))
% 0.46/0.67  (step @p844 :rule true_elim :premises (@p843))
% 0.46/0.67  (step @p845 :rule and_intro :premises (@p844 @p1))
% 0.46/0.67  (step @p846 :rule modus_ponens :premises (@p845 @p840))
% 0.46/0.67  (step @p1151 :rule arith_mult_pos :args (20 @t97))
% 0.46/0.67  (step @p220 :rule arith_poly_norm :args (@t98))
% 0.46/0.67  (step @p221 :rule arith_poly_norm_rel :premises (@p220) :args (@t99))
% 0.46/0.67  (step @p222 :rule symm :premises (@p221))
% 0.46/0.67  (step @p1152 :rule eq_resolve :premises (@p1469 @p222))
% 0.46/0.67  (step @p1153 :rule evaluate :args ((> 20 0)))
% 0.46/0.67  (step @p1154 :rule true_elim :premises (@p1153))
% 0.46/0.67  (step @p1155 :rule and_intro :premises (@p1154 @p1152))
% 0.46/0.67  (step @p1156 :rule modus_ponens :premises (@p1155 @p1151))
% 0.46/0.67  (step @p1157 :rule cong :premises (@p1156) :args (@t340))
% 0.46/0.67  (step @p1158 :rule arith_mult_pos :args (11 @t210))
% 0.46/0.67  (step @p528 :rule arith_poly_norm :args (@t212))
% 0.46/0.67  (step @p529 :rule arith_poly_norm_rel :premises (@p528) :args (@t213))
% 0.46/0.67  (step @p530 :rule symm :premises (@p529))
% 0.46/0.67  (step @p1159 :rule eq_resolve :premises (@p1470 @p530))
% 0.46/0.67  (step @p857 :rule evaluate :args (@t281))
% 0.46/0.67  (step @p858 :rule true_elim :premises (@p857))
% 0.46/0.67  (step @p1160 :rule and_intro :premises (@p858 @p1159))
% 0.46/0.67  (step @p1161 :rule modus_ponens :premises (@p1160 @p1158))
% 0.46/0.67  (step @p1162 :rule cong :premises (@p1161) :args (@t342))
% 0.46/0.67  (step @p1163 :rule evaluate :args (@t346))
% 0.46/0.67  (step @p1164 :rule refl :args (@t187))
% 0.46/0.67  (step @p1165 :rule cong :premises (@p1164 @p1163) :args (@t347))
% 0.46/0.67  (step @p1166 :rule arith_poly_norm :args ((= (* 2/1 (to_real (- @t45 -2))) (* 2/1 (- @t187 @t346)))))
% 0.46/0.67  (step @p1167 :rule arith_poly_norm_rel :premises (@p1166) :args ((= @t324 @t347)))
% 0.46/0.67  (step @p1168 :rule trans :premises (@p1167 @p1165))
% 0.46/0.67  (step @p1169 :rule symm :premises (@p1080))
% 0.46/0.67  (step @p1170 :rule not_or_elim :premises (@p174) :args (0))
% 0.46/0.67  (step @p1171 :rule eq_resolve :premises (@p1170 @p1169))
% 0.46/0.67  (step @p1172 :rule eq_resolve :premises (@p1171 @p1168))
% 0.46/0.67  (step @p1173 :rule arith_sum_ub :premises (@p1172 @p1162 @p1157 @p846 @p1146 @p1126))
% 0.46/0.67  (step @p1174 false :rule eq_resolve :premises (@p1173 @p1116))
% 0.46/0.67  (step-pop @p1481 :rule scope :premises (@p1174))
% 0.46/0.67  (step @p1175 :rule process_scope :premises (@p1481) :args (false))
% 0.46/0.67  (step @p1177 :rule eq_resolve :premises (@p1175 @p1082))
% 0.46/0.67  (step @p1178 :rule eq_resolve :premises (@p1177 @p1083))
% 0.46/0.67  (step @p1169 :rule symm :premises (@p1080))
% 0.46/0.67  (step @p1179 :rule eq_resolve :premises (@p1071 @p1169))
% 0.46/0.67  (step @p1180 false :rule contra :premises (@p1179 @p1178))
% 0.46/0.67  (step-pop @p1482 :rule scope :premises (@p1180))
% 0.46/0.67  (step-pop @p1483 :rule scope :premises (@p1482))
% 0.46/0.67  (step-pop @p1484 :rule scope :premises (@p1483))
% 0.46/0.67  (step-pop @p1485 :rule scope :premises (@p1484))
% 0.46/0.67  (step-pop @p1486 :rule scope :premises (@p1485))
% 0.46/0.67  (step-pop @p1487 :rule scope :premises (@p1486))
% 0.46/0.67  (step @p1181 :rule process_scope :premises (@p1487) :args (false))
% 0.46/0.67  (assume-push @p1488 @t15)
% 0.46/0.67  (assume-push @p1489 @t323)
% 0.46/0.67  (assume-push @p1490 @t152)
% 0.46/0.67  (assume-push @p1491 @t141)
% 0.46/0.67  (assume-push @p1492 @t66)
% 0.46/0.67  (assume-push @p1493 @t172)
% 0.46/0.67  (step @p1194 :rule and_intro :premises (@p1493 @p1490 @p6 @p1492 @p1491 @p1071))
% 0.46/0.67  (step-pop @p1494 :rule scope :premises (@p1194))
% 0.46/0.67  (step-pop @p1495 :rule scope :premises (@p1494))
% 0.46/0.67  (step-pop @p1496 :rule scope :premises (@p1495))
% 0.46/0.67  (step-pop @p1497 :rule scope :premises (@p1496))
% 0.46/0.67  (step-pop @p1498 :rule scope :premises (@p1497))
% 0.46/0.67  (step-pop @p1499 :rule scope :premises (@p1498))
% 0.46/0.67  (step @p1195 :rule process_scope :premises (@p1499) :args (@t348))
% 0.46/0.67  (step @p1202 :rule implies_elim :premises (@p1195))
% 0.46/0.67  (step @p1203 :rule resolution :premises (@p1202 @p1181) :args (true @t348))
% 0.46/0.67  (step @p1204 :rule not_and :premises (@p1203))
% 0.46/0.67  (step @p1205 :rule eq_resolve :premises (@p1204 @p1073))
% 0.46/0.67  (step @p1206 :rule reordering :premises (@p1205) :args ((or @t322 @t41 @t151 @t171 @t102 @t167)))
% 0.46/0.67  (step @p1207 :rule chain_m_resolution :premises (@p1206 @p398 @p1071 @p6 @p1070 @p942 @p398 @p6 @p872 @p176 @p6 @p768 @p398) :args (@t102 (@list false true false true false false false false false false true false) (@list @t141 @t322 @t15 @t167 @t282 @t141 @t15 @t250 @t75 @t15 @t151 @t141)))
% 0.46/0.67  (step @p1208 :rule cnf_and_neg :args (@t349))
% 0.46/0.67  (step @p1209 :rule reordering :premises (@p1208) :args ((or @t41 @t283 @t349)))
% 0.46/0.67  (step @p1210 :rule chain_m_resolution :premises (@p1209 @p6 @p942) :args (@t349 (@list false false) (@list @t15 @t282)))
% 0.46/0.67  (step @p1211 :rule arith_poly_norm :args ((= (* 1 (- @t59 @t350)) @t63)))
% 0.46/0.67  (step @p1212 :rule arith_poly_norm_rel :premises (@p1211) :args ((= (= @t59 @t350) @t66)))
% 0.46/0.67  (step @p1213 :rule arith_poly_norm :args ((= (* tptp.b @t142) @t350)))
% 0.46/0.67  (step @p1214 :rule nary_cong :premises (@p113 @p375) :args (@t351))
% 0.46/0.67  (step @p1215 :rule trans :premises (@p1214 @p1213))
% 0.46/0.67  (step @p1216 :rule arith_poly_norm :args ((= @t352 @t59)))
% 0.46/0.67  (step @p1217 :rule cong :premises (@p1216 @p1215) :args (@t353))
% 0.46/0.67  (step @p1218 :rule trans :premises (@p1217 @p1212))
% 0.46/0.67  (step @p272 :rule evaluate :args (@t107))
% 0.46/0.67  (step @p1219 :rule refl :args (tptp.b))
% 0.46/0.67  (step @p1220 :rule cong :premises (@p1219 @p272) :args (@t354))
% 0.46/0.67  (step @p1221 :rule cong :premises (@p1220) :args ((not @t354)))
% 0.46/0.67  (step @p1222 :rule arith-leq-norm :args (tptp.b 0))
% 0.46/0.67  (step @p1223 :rule trans :premises (@p1222 @p1221))
% 0.46/0.67  (step @p1224 :rule cong :premises (@p1223) :args ((not (<= tptp.b 0))))
% 0.46/0.67  (step @p1225 :rule trans :premises (@p1224 @p873))
% 0.46/0.67  (step @p1226 :rule arith-elim-leq :args (tptp.b 0))
% 0.46/0.67  (step @p1227 :rule symm :premises (@p1226))
% 0.46/0.67  (step @p1228 :rule cong :premises (@p1227) :args ((not (>= 0 tptp.b))))
% 0.46/0.67  (step @p1229 :rule arith-elim-gt :args (tptp.b 0))
% 0.46/0.67  (step @p1230 :rule trans :premises (@p1229 @p1228))
% 0.46/0.67  (step @p1231 :rule trans :premises (@p1230 @p1225))
% 0.46/0.67  (step @p1232 :rule nary_cong :premises (@p1231 @p145) :args (@t356))
% 0.46/0.67  (step @p1233 :rule cong :premises (@p1232 @p1218) :args ((=> @t356 @t353)))
% 0.46/0.67  (step @p1234 :rule symm :premises (@p1233))
% 0.46/0.67  (step @p1235 :rule nary_cong :premises (@p1231 @p389) :args (@t357))
% 0.46/0.67  (step @p1236 :rule cong :premises (@p1235 @p1218) :args ((=> @t357 @t353)))
% 0.46/0.67  (step @p1237 :rule trans :premises (@p1236 @p1234))
% 0.46/0.67  (step @p1238 :rule arith_mult_pos :args (tptp.b @t149))
% 0.46/0.67  (step @p1239 :rule eq_resolve :premises (@p1238 @p1237))
% 0.46/0.67  (step @p1240 :rule eq_resolve :premises (@p1239 @p1233))
% 0.46/0.67  (step @p1241 :rule implies_elim :premises (@p1240))
% 0.46/0.67  (step @p1242 :rule reordering :premises (@p1241) :args ((or @t66 (not @t349))))
% 0.46/0.67  (step @p1243 false :rule chain_m_resolution :premises (@p1242 @p1210 @p1207) :args (false @t131 (@list @t349 @t66)))
% 0.46/0.67  )
% 0.46/0.67  % SZS output end Proof
% 0.46/0.67  % cvc5 exiting
%------------------------------------------------------------------------------