%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : SWW834_1 : TPTP v9.2.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n012.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jun 3 09:05:43 AM UTC 2026 % Result : Unsatisfiable 0.23s 0.52s % Output : Proof 0.33s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.06 % Problem : SWW834_1 : TPTP v9.2.1. Released v7.0.0. % 0.00/0.07 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.07/0.25 % Computer : n012.cluster.edu % 0.07/0.25 % Model : x86_64 x86_64 % 0.07/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.25 % Memory : 8042.1875MB % 0.07/0.25 % OS : Linux 3.10.0-693.el7.x86_64 % 0.07/0.25 % CPULimit : 300 % 0.07/0.25 % WCLimit : 300 % 0.07/0.25 % DateTime : Tue Jun 2 22:32:48 EDT 2026 % 0.07/0.25 % CPUTime : % 0.15/0.37 %----Proving TF0_ARI % 0.15/0.38 --- Run --finite-model-find --decision=internal at 45... % 0.23/0.52 % SZS status Unsatisfiable % 0.23/0.52 % SZS output start Proof % 0.33/0.55 ( % 0.33/0.55 (declare-sort |tptp.'S9'| 0) % 0.33/0.55 (declare-sort |tptp.'S8'| 0) % 0.33/0.55 (declare-sort |tptp.'S7'| 0) % 0.33/0.55 (declare-sort |tptp.'S5'| 0) % 0.33/0.55 (declare-sort |tptp.'S3'| 0) % 0.33/0.55 (declare-sort |tptp.'S6'| 0) % 0.33/0.55 (declare-sort |tptp.'S4'| 0) % 0.33/0.55 (declare-sort |tptp.'S2'| 0) % 0.33/0.55 (declare-sort |tptp.'S1'| 0) % 0.33/0.55 (declare-const tptp.f26 |tptp.'S2'|) % 0.33/0.55 (declare-const tptp.f24 |tptp.'S2'|) % 0.33/0.55 (declare-const tptp.f23 |tptp.'S9'|) % 0.33/0.55 (declare-const tptp.f21 |tptp.'S2'|) % 0.33/0.55 (declare-const tptp.f19 (-> |tptp.'S8'| |tptp.'S4'| Int)) % 0.33/0.55 (declare-const tptp.f20 |tptp.'S8'|) % 0.33/0.55 (declare-const tptp.f17 (-> |tptp.'S7'| Int Real)) % 0.33/0.55 (declare-const tptp.f18 |tptp.'S7'|) % 0.33/0.55 (declare-const tptp.f12 (-> |tptp.'S3'| |tptp.'S4'| Real)) % 0.33/0.55 (declare-const tptp.f13 (-> |tptp.'S5'| Real |tptp.'S3'|)) % 0.33/0.55 (declare-const tptp.f22 (-> |tptp.'S9'| Int Int)) % 0.33/0.55 (declare-const tptp.f14 |tptp.'S5'|) % 0.33/0.55 (declare-const tptp.f2 |tptp.'S1'|) % 0.33/0.55 (declare-const tptp.f9 |tptp.'S2'|) % 0.33/0.55 (declare-const tptp.f1 |tptp.'S1'|) % 0.33/0.55 (declare-const tptp.f4 |tptp.'S2'|) % 0.33/0.55 (declare-const tptp.f5 Real) % 0.33/0.55 (declare-const tptp.f6 |tptp.'S2'|) % 0.33/0.55 (declare-const tptp.f3 (-> |tptp.'S2'| Real Real)) % 0.33/0.55 (declare-const tptp.f16 |tptp.'S6'|) % 0.33/0.55 (declare-const tptp.f7 Real) % 0.33/0.55 (declare-const tptp.f8 |tptp.'S2'|) % 0.33/0.55 (declare-const tptp.f25 (-> |tptp.'S2'| Real Real |tptp.'S1'|)) % 0.33/0.55 (declare-const tptp.f11 |tptp.'S2'|) % 0.33/0.55 (declare-const tptp.f10 |tptp.'S2'|) % 0.33/0.55 (declare-const tptp.f15 (-> |tptp.'S6'| Int |tptp.'S4'|)) % 0.33/0.55 (define @t1 () (= (tptp.f3 tptp.f6 tptp.f5) 1/1)) % 0.33/0.55 (define @t2 () (not @t1)) % 0.33/0.55 (define @t3 () (tptp.f3 tptp.f4 tptp.f5)) % 0.33/0.55 (define @t4 () (= @t3 0/1)) % 0.33/0.55 (define @t5 () (not @t4)) % 0.33/0.55 (define @t6 () (@var "A__questionmark_v_0_1" Real)) % 0.33/0.55 (define @t7 () (= @t3 @t6)) % 0.33/0.55 (define @t8 () (not @t7)) % 0.33/0.55 (define @t9 () (< tptp.f5 tptp.f7)) % 0.33/0.55 (define @t10 () (=> @t9 @t8)) % 0.33/0.55 (define @t11 () (=> (< @t6 tptp.f5) @t10)) % 0.33/0.55 (define @t12 () (= @t6 0/1)) % 0.33/0.55 (define @t13 () (and @t12 @t11)) % 0.33/0.55 (define @t14 () (@list @t6)) % 0.33/0.55 (define @t15 () (exists @t14 @t13)) % 0.33/0.55 (define @t16 () (= tptp.f5 tptp.f7)) % 0.33/0.55 (define @t17 () (=> @t16 @t2)) % 0.33/0.55 (define @t18 () (* 2/1 tptp.f7)) % 0.33/0.55 (define @t19 () (< tptp.f5 @t18)) % 0.33/0.55 (define @t20 () (=> @t19 @t5)) % 0.33/0.55 (define @t21 () (=> (< tptp.f7 tptp.f5) @t20)) % 0.33/0.55 (define @t22 () (@var "A__questionmark_v_0_2" Real)) % 0.33/0.55 (define @t23 () (@var "A__questionmark_v1" Real)) % 0.33/0.55 (define @t24 () (tptp.f3 tptp.f4 @t23)) % 0.33/0.55 (define @t25 () (@var "A__questionmark_v0" Real)) % 0.33/0.55 (define @t26 () (tptp.f3 tptp.f4 @t25)) % 0.33/0.55 (define @t27 () (* @t26 @t24)) % 0.33/0.55 (define @t28 () (tptp.f3 tptp.f6 @t23)) % 0.33/0.55 (define @t29 () (tptp.f3 tptp.f6 @t25)) % 0.33/0.55 (define @t30 () (* @t29 @t28)) % 0.33/0.55 (define @t31 () (+ @t25 @t23)) % 0.33/0.55 (define @t32 () (tptp.f3 tptp.f6 @t31)) % 0.33/0.55 (define @t33 () (@list @t25 @t23)) % 0.33/0.55 (define @t34 () (- @t25 @t23)) % 0.33/0.55 (define @t35 () (tptp.f3 tptp.f6 @t34)) % 0.33/0.55 (define @t36 () (* @t29 @t24)) % 0.33/0.55 (define @t37 () (* @t26 @t28)) % 0.33/0.55 (define @t38 () (tptp.f3 tptp.f4 @t31)) % 0.33/0.55 (define @t39 () (tptp.f3 tptp.f4 @t34)) % 0.33/0.55 (define @t40 () (@var "A__questionmark_v_0_3" Real)) % 0.33/0.55 (define @t41 () (@list @t25)) % 0.33/0.55 (define @t42 () (@var "A__questionmark_v_1_5" Real)) % 0.33/0.55 (define @t43 () (@var "A__questionmark_v_0_4" Real)) % 0.33/0.55 (define @t44 () (@var "A__questionmark_v_1_7" Real)) % 0.33/0.55 (define @t45 () (@var "A__questionmark_v_0_6" Real)) % 0.33/0.55 (define @t46 () (< @t44 @t45)) % 0.33/0.55 (define @t47 () (- @t26)) % 0.33/0.55 (define @t48 () (/ tptp.f7 2/1)) % 0.33/0.55 (define @t49 () (- @t48 @t25)) % 0.33/0.55 (define @t50 () (@var "A__questionmark_v_0_8" Real)) % 0.33/0.55 (define @t51 () (- @t48)) % 0.33/0.55 (define @t52 () (@var "A__questionmark_v_0_9" Real)) % 0.33/0.55 (define @t53 () (@var "A__questionmark_v_0_10" Real)) % 0.33/0.55 (define @t54 () (@var "A__questionmark_v_0_11" Real)) % 0.33/0.55 (define @t55 () (@var "A__questionmark_v_0_12" Real)) % 0.33/0.55 (define @t56 () (<= @t23 0/1)) % 0.33/0.55 (define @t57 () (<= @t25 @t23)) % 0.33/0.55 (define @t58 () (- tptp.f7)) % 0.33/0.55 (define @t59 () (<= @t58 @t25)) % 0.33/0.55 (define @t60 () (< @t25 @t23)) % 0.33/0.55 (define @t61 () (@var "A__questionmark_v_0_13" Real)) % 0.33/0.55 (define @t62 () (< @t25 @t48)) % 0.33/0.55 (define @t63 () (<= @t23 tptp.f7)) % 0.33/0.55 (define @t64 () (<= 0/1 @t25)) % 0.33/0.55 (define @t65 () (* (/ 3/1 2/1) tptp.f7)) % 0.33/0.55 (define @t66 () (+ @t25 @t18)) % 0.33/0.55 (define @t67 () (+ @t25 tptp.f7)) % 0.33/0.55 (define @t68 () (/ 1/1 2/1)) % 0.33/0.55 (define @t69 () (- 1/1)) % 0.33/0.55 (define @t70 () (@var "A__questionmark_v_0_14" Real)) % 0.33/0.55 (define @t71 () (< (/ @t58 2/1) @t25)) % 0.33/0.55 (define @t72 () (@var "A__questionmark_v_0_15" Real)) % 0.33/0.55 (define @t73 () (@var "A__questionmark_v_0_16" Real)) % 0.33/0.55 (define @t74 () (@var "A__questionmark_v_0_17" Real)) % 0.33/0.55 (define @t75 () (<= @t25 tptp.f7)) % 0.33/0.55 (define @t76 () (@var "A__questionmark_v_0_18" Real)) % 0.33/0.55 (define @t77 () (/ tptp.f7 6/1)) % 0.33/0.55 (define @t78 () (@var "A__questionmark_v_0_19" Real)) % 0.33/0.55 (define @t79 () (< 0/1 @t25)) % 0.33/0.55 (define @t80 () (tptp.f3 tptp.f6 2/1)) % 0.33/0.55 (define @t81 () (- @t25)) % 0.33/0.55 (define @t82 () (@var "A__questionmark_v_0_20" Real)) % 0.33/0.55 (define @t83 () (< @t82 0/1)) % 0.33/0.55 (define @t84 () (@var "A__questionmark_v_0_21" Real)) % 0.33/0.55 (define @t85 () (@var "A__questionmark_v_0_22" Real)) % 0.33/0.55 (define @t86 () (< @t85 0/1)) % 0.33/0.55 (define @t87 () (@var "A__questionmark_v_0_23" Real)) % 0.33/0.55 (define @t88 () (@var "A__questionmark_v2" Real)) % 0.33/0.55 (define @t89 () (= @t88 @t23)) % 0.33/0.55 (define @t90 () (@var "A__questionmark_v_0_24" Real)) % 0.33/0.55 (define @t91 () (- @t90)) % 0.33/0.55 (define @t92 () (@list @t88)) % 0.33/0.55 (define @t93 () (<= @t25 1/1)) % 0.33/0.55 (define @t94 () (<= @t69 @t25)) % 0.33/0.55 (define @t95 () (<= 0/1 @t23)) % 0.33/0.55 (define @t96 () (@list @t23)) % 0.33/0.55 (define @t97 () (@var "A__questionmark_v_0_25" Real)) % 0.33/0.55 (define @t98 () (@var "A__questionmark_v3" Real)) % 0.33/0.55 (define @t99 () (* @t88 (tptp.f3 tptp.f4 @t98))) % 0.33/0.55 (define @t100 () (* @t88 (tptp.f3 tptp.f6 @t98))) % 0.33/0.55 (define @t101 () (@list @t88 @t98)) % 0.33/0.55 (define @t102 () (exists @t101 (and (= @t23 @t100) (= @t25 @t99)))) % 0.33/0.55 (define @t103 () (< @t25 0/1)) % 0.33/0.55 (define @t104 () (@var "A__questionmark_v_2_28" Real)) % 0.33/0.55 (define @t105 () (tptp.f3 tptp.f8 @t25)) % 0.33/0.55 (define @t106 () (@var "A__questionmark_v_0_27" Real)) % 0.33/0.55 (define @t107 () (@var "A__questionmark_v_1_26" Real)) % 0.33/0.55 (define @t108 () (@var "A__questionmark_v_0_29" Real)) % 0.33/0.55 (define @t109 () (@var "A__questionmark_v_0_31" Real)) % 0.33/0.55 (define @t110 () (@var "A__questionmark_v_1_30" Real)) % 0.33/0.55 (define @t111 () (tptp.f3 tptp.f9 @t25)) % 0.33/0.55 (define @t112 () (@var "A__questionmark_v_0_32" Real)) % 0.33/0.55 (define @t113 () (@var "A__questionmark_v_0_33" Real)) % 0.33/0.55 (define @t114 () (@var "A__questionmark_v_2_36" Real)) % 0.33/0.55 (define @t115 () (@var "A__questionmark_v_1_35" Real)) % 0.33/0.55 (define @t116 () (tptp.f3 tptp.f8 @t23)) % 0.33/0.55 (define @t117 () (@var "A__questionmark_v_0_34" Real)) % 0.33/0.55 (define @t118 () (@var "A__questionmark_v_3_40" Real)) % 0.33/0.55 (define @t119 () (@var "A__questionmark_v_2_39" Real)) % 0.33/0.55 (define @t120 () (@var "A__questionmark_v_1_38" Real)) % 0.33/0.55 (define @t121 () (@var "A__questionmark_v_0_37" Real)) % 0.33/0.55 (define @t122 () (@var "A__questionmark_v_0_41" Real)) % 0.33/0.55 (define @t123 () (< @t105 @t116)) % 0.33/0.55 (define @t124 () (@var "A__questionmark_v_0_42" Real)) % 0.33/0.55 (define @t125 () (@var "A__questionmark_v_1_43" Real)) % 0.33/0.55 (define @t126 () (@var "A__questionmark_v_0_44" Real)) % 0.33/0.55 (define @t127 () (@var "A__questionmark_v_0_45" Real)) % 0.33/0.55 (define @t128 () (/ tptp.f7 4/1)) % 0.33/0.55 (define @t129 () (@var "A__questionmark_v_1_46" Real)) % 0.33/0.55 (define @t130 () (@var "A__questionmark_v_0_47" Real)) % 0.33/0.55 (define @t131 () (@var "A__questionmark_v_1_48" Real)) % 0.33/0.55 (define @t132 () (@var "A__questionmark_v_0_49" Real)) % 0.33/0.55 (define @t133 () (< @t25 1/1)) % 0.33/0.55 (define @t134 () (< @t69 @t25)) % 0.33/0.55 (define @t135 () (@var "A__questionmark_v_2_52" Real)) % 0.33/0.55 (define @t136 () (@var "A__questionmark_v_1_51" Real)) % 0.33/0.55 (define @t137 () (@var "A__questionmark_v_0_50" Real)) % 0.33/0.55 (define @t138 () (= @t116 @t25)) % 0.33/0.55 (define @t139 () (@var "A__questionmark_v_0_53" Real)) % 0.33/0.55 (define @t140 () (not @t103)) % 0.33/0.55 (define @t141 () (< @t23 @t48)) % 0.33/0.55 (define @t142 () (< 0/1 @t23)) % 0.33/0.55 (define @t143 () (@var "A__questionmark_v_0_54" Real)) % 0.33/0.55 (define @t144 () (- @t143)) % 0.33/0.55 (define @t145 () (@var "A__questionmark_v_0_55" Real)) % 0.33/0.55 (define @t146 () (tptp.f3 tptp.f10 @t29)) % 0.33/0.55 (define @t147 () (tptp.f3 tptp.f10 @t25)) % 0.33/0.55 (define @t148 () (= (tptp.f3 tptp.f6 @t147) @t25)) % 0.33/0.55 (define @t149 () (@var "A__questionmark_v_0_56" Real)) % 0.33/0.55 (define @t150 () (@var "A__questionmark_v_0_57" Real)) % 0.33/0.55 (define @t151 () (@var "A__questionmark_v_0_58" Real)) % 0.33/0.55 (define @t152 () (@var "A__questionmark_v_0_60" Real)) % 0.33/0.55 (define @t153 () (@var "A__questionmark_v_1_59" Real)) % 0.33/0.55 (define @t154 () (tptp.f3 tptp.f11 @t25)) % 0.33/0.55 (define @t155 () (@var "A__questionmark_v_0_61" Real)) % 0.33/0.55 (define @t156 () (tptp.f15 tptp.f16 2)) % 0.33/0.55 (define @t157 () (@var "A__questionmark_v_3_65" Real)) % 0.33/0.55 (define @t158 () (@var "A__questionmark_v_2_63" Real)) % 0.33/0.55 (define @t159 () (@var "A__questionmark_v_1_64" Real)) % 0.33/0.55 (define @t160 () (@var "A__questionmark_v_0_62" Real)) % 0.33/0.55 (define @t161 () (@var "A__questionmark_v1" Int)) % 0.33/0.55 (define @t162 () (tptp.f17 tptp.f18 @t161)) % 0.33/0.55 (define @t163 () (@var "A__questionmark_v_0_66" Real)) % 0.33/0.55 (define @t164 () (tptp.f3 tptp.f11 @t23)) % 0.33/0.55 (define @t165 () (@var "A__questionmark_v_0_67" Real)) % 0.33/0.55 (define @t166 () (tptp.f13 tptp.f14 @t25)) % 0.33/0.55 (define @t167 () (tptp.f12 @t166 @t156)) % 0.33/0.55 (define @t168 () (* @t25 @t23)) % 0.33/0.55 (define @t169 () (@var "A__questionmark_v_1_69" Real)) % 0.33/0.55 (define @t170 () (@var "A__questionmark_v_0_68" Real)) % 0.33/0.55 (define @t171 () (< @t23 @t170)) % 0.33/0.55 (define @t172 () (< @t25 @t170)) % 0.33/0.55 (define @t173 () (@var "A__questionmark_v_1_70" Real)) % 0.33/0.55 (define @t174 () (@var "A__questionmark_v_0_71" Real)) % 0.33/0.55 (define @t175 () (/ 1/1 239/1)) % 0.33/0.55 (define @t176 () (tptp.f3 tptp.f11 @t175)) % 0.33/0.55 (define @t177 () (/ 1/1 5/1)) % 0.33/0.55 (define @t178 () (tptp.f3 tptp.f11 @t177)) % 0.33/0.55 (define @t179 () (@var "A__questionmark_v_0_72" Real)) % 0.33/0.55 (define @t180 () (* @t179 @t178)) % 0.33/0.55 (define @t181 () (- @t180 @t176)) % 0.33/0.55 (define @t182 () (/ tptp.f7 @t179)) % 0.33/0.55 (define @t183 () (= @t182 @t181)) % 0.33/0.55 (define @t184 () (= @t179 4/1)) % 0.33/0.55 (define @t185 () (and @t184 @t183)) % 0.33/0.55 (define @t186 () (@list @t179)) % 0.33/0.55 (define @t187 () (exists @t186 @t185)) % 0.33/0.55 (define @t188 () (@var "A__questionmark_v_0_73" |tptp.'S4'|)) % 0.33/0.55 (define @t189 () (tptp.f13 tptp.f14 @t26)) % 0.33/0.55 (define @t190 () (tptp.f13 tptp.f14 @t29)) % 0.33/0.55 (define @t191 () (* 2/1 @t25)) % 0.33/0.55 (define @t192 () (@var "A__questionmark_v_0_74" |tptp.'S4'|)) % 0.33/0.55 (define @t193 () (@var "A__questionmark_v_0_75" |tptp.'S4'|)) % 0.33/0.55 (define @t194 () (@var "A__questionmark_v_0_76" |tptp.'S4'|)) % 0.33/0.55 (define @t195 () (@var "A__questionmark_v_0_77" |tptp.'S4'|)) % 0.33/0.55 (define @t196 () (@var "A__questionmark_v_1_78" |tptp.'S4'|)) % 0.33/0.55 (define @t197 () (@var "A__questionmark_v_0_79" Real)) % 0.33/0.55 (define @t198 () (@var "A__questionmark_v_5_80" |tptp.'S4'|)) % 0.33/0.55 (define @t199 () (@var "A__questionmark_v_4_84" Real)) % 0.33/0.55 (define @t200 () (@var "A__questionmark_v_3_81" Real)) % 0.33/0.55 (define @t201 () (@var "A__questionmark_v_2_82" Real)) % 0.33/0.55 (define @t202 () (@var "A__questionmark_v_1_83" Real)) % 0.33/0.55 (define @t203 () (@var "A__questionmark_v_0_85" Real)) % 0.33/0.55 (define @t204 () (@var "A__questionmark_v_0_86" |tptp.'S4'|)) % 0.33/0.55 (define @t205 () (@var "A__questionmark_v_1_87" Real)) % 0.33/0.55 (define @t206 () (@var "A__questionmark_v_0_88" |tptp.'S4'|)) % 0.33/0.55 (define @t207 () (tptp.f13 tptp.f14 @t23)) % 0.33/0.55 (define @t208 () (@var "A__questionmark_v_0_89" |tptp.'S4'|)) % 0.33/0.55 (define @t209 () (tptp.f13 tptp.f14 @t31)) % 0.33/0.55 (define @t210 () (@var "A__questionmark_v_0_90" |tptp.'S4'|)) % 0.33/0.55 (define @t211 () (@var "A__questionmark_v0" |tptp.'S4'|)) % 0.33/0.55 (define @t212 () (@list @t211)) % 0.33/0.55 (define @t213 () (@var "A__questionmark_v_0_91" |tptp.'S4'|)) % 0.33/0.55 (define @t214 () (@var "A__questionmark_v1" |tptp.'S4'|)) % 0.33/0.55 (define @t215 () (tptp.f13 tptp.f14 @t88)) % 0.33/0.55 (define @t216 () (< 0/1 @t88)) % 0.33/0.55 (define @t217 () (@list @t25 @t214)) % 0.33/0.55 (define @t218 () (= (tptp.f12 @t215 @t211) @t23)) % 0.33/0.55 (define @t219 () (tptp.f19 tptp.f20 @t211)) % 0.33/0.55 (define @t220 () (< 0 @t219)) % 0.33/0.55 (define @t221 () (@list @t211 @t23)) % 0.33/0.55 (define @t222 () (tptp.f13 tptp.f14 @t98)) % 0.33/0.55 (define @t223 () (@list @t98)) % 0.33/0.55 (define @t224 () (@var "A__questionmark_v_0_92" |tptp.'S4'|)) % 0.33/0.55 (define @t225 () (tptp.f13 tptp.f14 (tptp.f3 tptp.f21 @t25))) % 0.33/0.55 (define @t226 () (tptp.f12 @t166 @t214)) % 0.33/0.55 (define @t227 () (@var "A__questionmark_v_0_93" Real)) % 0.33/0.55 (define @t228 () (@var "A__questionmark_v_0_94" Real)) % 0.33/0.55 (define @t229 () (@var "A__questionmark_v0" Int)) % 0.33/0.55 (define @t230 () (tptp.f17 tptp.f18 @t229)) % 0.33/0.55 (define @t231 () (@var "A__questionmark_v_0_95" Int)) % 0.33/0.55 (define @t232 () (tptp.f22 tptp.f23 @t229)) % 0.33/0.55 (define @t233 () (@list @t229 @t161)) % 0.33/0.55 (define @t234 () (= @t229 @t161)) % 0.33/0.55 (define @t235 () (@var "A__questionmark_v_1_96" |tptp.'S4'|)) % 0.33/0.55 (define @t236 () (@var "A__questionmark_v_0_97" Real)) % 0.33/0.55 (define @t237 () (tptp.f3 tptp.f24 @t25)) % 0.33/0.55 (define @t238 () (@var "A__questionmark_v_0_98" Real)) % 0.33/0.55 (define @t239 () (tptp.f3 tptp.f24 @t23)) % 0.33/0.55 (define @t240 () (/ @t25 @t23)) % 0.33/0.55 (define @t241 () (= @t25 0/1)) % 0.33/0.55 (define @t242 () (< (* @t23 @t88) (* @t25 @t98))) % 0.33/0.55 (define @t243 () (@var "A__questionmark_v_0_99" Real)) % 0.33/0.55 (define @t244 () (@list @t25 @t23 @t88 @t98)) % 0.33/0.55 (define @t245 () (@var "A__questionmark_v_0_100" Real)) % 0.33/0.55 (define @t246 () (@var "A__questionmark_v_0_101" Real)) % 0.33/0.55 (define @t247 () (= @t25 @t23)) % 0.33/0.55 (define @t248 () (= @t237 @t239)) % 0.33/0.55 (define @t249 () (@var "A__questionmark_v_0_102" Real)) % 0.33/0.55 (define @t250 () (@var "A__questionmark_v_0_103" Real)) % 0.33/0.55 (define @t251 () (@var "A__questionmark_v0" |tptp.'S2'|)) % 0.33/0.55 (define @t252 () (= (tptp.f25 @t251 @t23 @t98) tptp.f1)) % 0.33/0.55 (define @t253 () (= @t88 @t98)) % 0.33/0.55 (define @t254 () (= (tptp.f25 @t251 @t23 @t88) tptp.f1)) % 0.33/0.55 (define @t255 () (@list @t251 @t23 @t88 @t98)) % 0.33/0.55 (define @t256 () (tptp.f3 tptp.f26 @t25)) % 0.33/0.55 (define @t257 () (tptp.f3 tptp.f24 @t256)) % 0.33/0.55 (define @t258 () (@var "A__questionmark_v_0_104" Real)) % 0.33/0.55 (define @t259 () (tptp.f3 tptp.f26 3/1)) % 0.33/0.55 (define @t260 () (@var "A__questionmark_v_0_105" Real)) % 0.33/0.55 (define @t261 () (@var "A__questionmark_v_0_106" Real)) % 0.33/0.55 (define @t262 () (@var "A__questionmark_v_0_107" Real)) % 0.33/0.55 (define @t263 () (@var "A__questionmark_v_1_109" Real)) % 0.33/0.55 (define @t264 () (< @t263 0/1)) % 0.33/0.55 (define @t265 () (@var "A__questionmark_v_0_108" |tptp.'S4'|)) % 0.33/0.55 (define @t266 () (@var "A__questionmark_v_0_110" |tptp.'S4'|)) % 0.33/0.55 (define @t267 () (@var "A__questionmark_v_0_111" |tptp.'S4'|)) % 0.33/0.55 (define @t268 () (@var "A__questionmark_v_0_112" |tptp.'S4'|)) % 0.33/0.55 (define @t269 () (@var "A__questionmark_v_0_113" |tptp.'S4'|)) % 0.33/0.55 (define @t270 () (@var "A__questionmark_v_0_114" |tptp.'S4'|)) % 0.33/0.55 (define @t271 () (tptp.f3 tptp.f26 (+ (tptp.f12 @t166 @t270) (tptp.f12 @t207 @t270)))) % 0.33/0.55 (define @t272 () (@var "A__questionmark_v_0_115" |tptp.'S4'|)) % 0.33/0.55 (define @t273 () (tptp.f3 tptp.f26 (+ (tptp.f12 @t207 @t272) (tptp.f12 @t166 @t272)))) % 0.33/0.55 (define @t274 () (tptp.f13 tptp.f14 @t256)) % 0.33/0.55 (define @t275 () (tptp.f3 tptp.f26 @t167)) % 0.33/0.55 (define @t276 () (@var "A__questionmark_v_0_116" |tptp.'S4'|)) % 0.33/0.55 (define @t277 () (@var "A__questionmark_v_1_118" Real)) % 0.33/0.55 (define @t278 () (@var "A__questionmark_v_0_117" |tptp.'S4'|)) % 0.33/0.55 (define @t279 () (tptp.f12 @t274 @t156)) % 0.33/0.55 (define @t280 () (= @t279 @t25)) % 0.33/0.55 (define @t281 () (@var "A__questionmark_v_0_119" Real)) % 0.33/0.55 (define @t282 () (@var "A__questionmark_v_2_121" |tptp.'S4'|)) % 0.33/0.55 (define @t283 () (@var "A__questionmark_v_1_120" Real)) % 0.33/0.55 (define @t284 () (@var "A__questionmark_v_0_122" Real)) % 0.33/0.55 (define @t285 () (@list @t25 @t23 @t88)) % 0.33/0.55 (define @t286 () (@var "A__questionmark_v_2_124" |tptp.'S4'|)) % 0.33/0.55 (define @t287 () (@var "A__questionmark_v_1_125" Real)) % 0.33/0.55 (define @t288 () (@var "A__questionmark_v_0_123" Real)) % 0.33/0.55 (define @t289 () (< @t88 @t288)) % 0.33/0.55 (define @t290 () (< @t25 @t288)) % 0.33/0.55 (define @t291 () (tptp.f3 tptp.f26 2/1)) % 0.33/0.55 (define @t292 () (@var "A__questionmark_v_0_126" |tptp.'S4'|)) % 0.33/0.55 (define @t293 () (@var "A__questionmark_v_0_127" |tptp.'S4'|)) % 0.33/0.55 (define @t294 () (tptp.f3 tptp.f26 @t23)) % 0.33/0.55 (define @t295 () (* @t25 @t25)) % 0.33/0.55 (define @t296 () (tptp.f3 tptp.f26 (+ @t295 (* @t23 @t23)))) % 0.33/0.55 (define @t297 () (@var "A__questionmark_v_0_128" Real)) % 0.33/0.55 (define @t298 () (@var "A__questionmark_v_0_129" Real)) % 0.33/0.55 (define @t299 () (tptp.f3 tptp.f26 @t295)) % 0.33/0.55 (define @t300 () (@var "A__questionmark_v_0_130" Real)) % 0.33/0.55 (define @t301 () (@var "A__questionmark_v_0_131" Real)) % 0.33/0.55 (define @t302 () (@var "A__questionmark_v_0_132" Real)) % 0.33/0.55 (define @t303 () (@var "A__questionmark_v_0_133" Real)) % 0.33/0.55 (define @t304 () (@var "A__questionmark_v_0_134" Real)) % 0.33/0.55 (define @t305 () (@var "A__questionmark_v_0_135" Real)) % 0.33/0.55 (define @t306 () (@var "A__questionmark_v_0_136" Real)) % 0.33/0.55 (define @t307 () (@var "A__questionmark_v_0_137" Real)) % 0.33/0.55 (define @t308 () (@var "A__questionmark_v_0_138" Real)) % 0.33/0.55 (define @t309 () (@var "A__questionmark_v_0_139" Real)) % 0.33/0.55 (define @t310 () (< @t256 @t294)) % 0.33/0.55 (define @t311 () (<= @t256 @t294)) % 0.33/0.55 (define @t312 () (@var "A__questionmark_v_0_140" Real)) % 0.33/0.55 (define @t313 () (@var "A__questionmark_v_0_141" Real)) % 0.33/0.55 (define @t314 () (@var "A__questionmark_v_0_142" Real)) % 0.33/0.55 (define @t315 () (@var "A__questionmark_v_0_143" Real)) % 0.33/0.55 (define @t316 () (@var "A__questionmark_v_0_144" Real)) % 0.33/0.55 (define @t317 () (@var "A__questionmark_v_0_145" Real)) % 0.33/0.55 (define @t318 () (@var "A__questionmark_v_2_147" Real)) % 0.33/0.55 (define @t319 () (@var "A__questionmark_v_1_148" Real)) % 0.33/0.55 (define @t320 () (@var "A__questionmark_v_0_146" Real)) % 0.33/0.55 (define @t321 () (@var "A__questionmark_v_0_149" Real)) % 0.33/0.55 (define @t322 () (@var "A__questionmark_v_1_151" Real)) % 0.33/0.55 (define @t323 () (@var "A__questionmark_v_0_150" |tptp.'S4'|)) % 0.33/0.55 (define @t324 () (@var "A__questionmark_v_0_152" Real)) % 0.33/0.55 (define @t325 () (tptp.f3 tptp.f4 @t147)) % 0.33/0.55 (define @t326 () (@var "A__questionmark_v_0_153" Real)) % 0.33/0.55 (define @t327 () (@var "A__questionmark_v_0_154" |tptp.'S4'|)) % 0.33/0.55 (define @t328 () (@var "A__questionmark_v_1_155" Real)) % 0.33/0.55 (define @t329 () (@var "A__questionmark_v_0_156" Real)) % 0.33/0.55 (define @t330 () (@var "A__questionmark_v_0_157" Real)) % 0.33/0.55 (define @t331 () (@var "A__questionmark_v2" |tptp.'S2'|)) % 0.33/0.55 (define @t332 () (@var "A__questionmark_v4" Real)) % 0.33/0.55 (define @t333 () (tptp.f19 tptp.f20 (tptp.f15 tptp.f16 @t229))) % 0.33/0.55 (define @t334 () (@list @t229)) % 0.33/0.55 (define @t335 () (tptp.f3 tptp.f11 1/239)) % 0.33/0.55 (define @t336 () (* 4/1 @t335)) % 0.33/0.55 (define @t337 () (tptp.f3 tptp.f11 1/5)) % 0.33/0.55 (define @t338 () (* -16/1 @t337)) % 0.33/0.55 (define @t339 () (+ tptp.f5 @t338 @t336)) % 0.33/0.55 (define @t340 () (>= 0/1 @t339)) % 0.33/0.55 (define @t341 () (* -1/1 tptp.f5)) % 0.33/0.55 (define @t342 () (>= @t341 0/1)) % 0.33/0.55 (define @t343 () (>= 0/1 tptp.f5)) % 0.33/0.55 (define @t344 () (>= @t339 0/1)) % 0.33/0.55 (define @t345 () (not @t344)) % 0.33/0.55 (define @t346 () (not @t342)) % 0.33/0.55 (define @t347 () (= 0/1 0/1)) % 0.33/0.55 (define @t348 () (and @t346 @t345 @t347)) % 0.33/0.55 (define @t349 () (and @t346 @t345 @t4)) % 0.33/0.55 (define @t350 () (+ @t338 @t336)) % 0.33/0.55 (define @t351 () (* -4/1 @t335)) % 0.33/0.55 (define @t352 () (* 16/1 @t337)) % 0.33/0.55 (define @t353 () (+ @t352 @t351)) % 0.33/0.55 (define @t354 () (* -1/1 @t353)) % 0.33/0.55 (define @t355 () (+ tptp.f5 @t354)) % 0.33/0.55 (define @t356 () (>= @t355 0/1)) % 0.33/0.55 (define @t357 () (not @t356)) % 0.33/0.55 (define @t358 () (and @t346 @t357 @t4)) % 0.33/0.55 (define @t359 () (= tptp.f7 @t353)) % 0.33/0.55 (define @t360 () (not @t359)) % 0.33/0.55 (define @t361 () (* -1/1 @t335)) % 0.33/0.55 (define @t362 () (* 4/1 @t337)) % 0.33/0.55 (define @t363 () (+ @t362 @t361)) % 0.33/0.55 (define @t364 () (* 1/4 tptp.f7)) % 0.33/0.55 (define @t365 () (* 4/1 @t337)) % 0.33/0.55 (define @t366 () (+ @t365 @t361)) % 0.33/0.55 (define @t367 () (* tptp.f7 1/4)) % 0.33/0.55 (define @t368 () (= @t128 @t366)) % 0.33/0.55 (define @t369 () (not @t368)) % 0.33/0.55 (define @t370 () (= 4/1 4/1)) % 0.33/0.55 (define @t371 () (not @t370)) % 0.33/0.55 (define @t372 () (or @t371 @t369)) % 0.33/0.55 (define @t373 () (* @t179 @t337)) % 0.33/0.55 (define @t374 () (= @t182 (+ @t373 @t361))) % 0.33/0.55 (define @t375 () (not @t374)) % 0.33/0.55 (define @t376 () (not @t184)) % 0.33/0.55 (define @t377 () (or @t376 @t376 @t375)) % 0.33/0.55 (define @t378 () (or @t376 @t375)) % 0.33/0.55 (define @t379 () (and @t184 @t374)) % 0.33/0.55 (define @t380 () (forall @t186 (not @t379))) % 0.33/0.55 (define @t381 () (not @t380)) % 0.33/0.55 (define @t382 () (* -1/1 @t176)) % 0.33/0.55 (define @t383 () (+ @t180 @t382)) % 0.33/0.55 (define @t384 () (* -1/1 tptp.f7)) % 0.33/0.55 (define @t385 () (+ tptp.f5 @t384)) % 0.33/0.55 (define @t386 () (>= @t385 0/1)) % 0.33/0.55 (define @t387 () (not @t386)) % 0.33/0.55 (define @t388 () (and @t346 @t387 @t4)) % 0.33/0.55 (define @t389 () (= 0/1 @t3)) % 0.33/0.55 (define @t390 () (+ @t341 0/1)) % 0.33/0.55 (define @t391 () (>= @t390 0/1)) % 0.33/0.55 (define @t392 () (not @t391)) % 0.33/0.55 (define @t393 () (and @t392 @t387 @t389)) % 0.33/0.55 (define @t394 () (not @t347)) % 0.33/0.55 (define @t395 () (or @t394 @t393)) % 0.33/0.55 (define @t396 () (= @t6 @t3)) % 0.33/0.55 (define @t397 () (+ @t341 @t6)) % 0.33/0.55 (define @t398 () (>= @t397 0/1)) % 0.33/0.55 (define @t399 () (not @t398)) % 0.33/0.55 (define @t400 () (and @t399 @t387 @t396)) % 0.33/0.55 (define @t401 () (not @t12)) % 0.33/0.55 (define @t402 () (or @t401 @t401 @t400)) % 0.33/0.55 (define @t403 () (or @t401 @t400)) % 0.33/0.55 (define @t404 () (not @t396)) % 0.33/0.55 (define @t405 () (=> @t387 @t404)) % 0.33/0.55 (define @t406 () (=> @t399 @t405)) % 0.33/0.55 (define @t407 () (and @t12 @t406)) % 0.33/0.55 (define @t408 () (forall @t14 (not @t407))) % 0.33/0.55 (define @t409 () (not @t408)) % 0.33/0.55 (define @t410 () (>= tptp.f5 tptp.f7)) % 0.33/0.55 (define @t411 () (>= @t6 tptp.f5)) % 0.33/0.55 (define @t412 () (@list true)) % 0.33/0.55 (define @t413 () (= tptp.f5 @t353)) % 0.33/0.55 (define @t414 () (= @t339 0/1)) % 0.33/0.55 (define @t415 () (= 1/1 1/1)) % 0.33/0.55 (define @t416 () (not @t415)) % 0.33/0.55 (define @t417 () (+ @t341 @t352 @t351)) % 0.33/0.55 (define @t418 () (>= @t417 0/1)) % 0.33/0.55 (define @t419 () (* 8/1 @t335)) % 0.33/0.55 (define @t420 () (* -32/1 @t337)) % 0.33/0.55 (define @t421 () (+ tptp.f5 @t420 @t419)) % 0.33/0.55 (define @t422 () (+ @t420 @t419)) % 0.33/0.55 (define @t423 () (* -2/1 @t353)) % 0.33/0.55 (define @t424 () (+ tptp.f5 @t423)) % 0.33/0.55 (define @t425 () (>= @t424 0/1)) % 0.33/0.55 (define @t426 () (not @t425)) % 0.33/0.55 (define @t427 () (* -2/1 tptp.f7)) % 0.33/0.55 (define @t428 () (+ tptp.f5 @t427)) % 0.33/0.55 (define @t429 () (>= @t428 0/1)) % 0.33/0.55 (define @t430 () (not @t429)) % 0.33/0.55 (define @t431 () (>= tptp.f5 @t18)) % 0.33/0.55 (define @t432 () (>= @t421 0/1)) % 0.33/0.55 (define @t433 () (not @t418)) % 0.33/0.55 (define @t434 () (not @t432)) % 0.33/0.55 (define @t435 () (=> @t434 @t394)) % 0.33/0.55 (define @t436 () (=> @t434 @t5)) % 0.33/0.55 (define @t437 () (=> @t426 @t5)) % 0.33/0.55 (define @t438 () (+ @t351 @t352 @t341)) % 0.33/0.55 (define @t439 () (+ @t341 @t353)) % 0.33/0.55 (define @t440 () (>= @t439 0/1)) % 0.33/0.55 (define @t441 () (not @t440)) % 0.33/0.55 (define @t442 () (=> @t430 @t5)) % 0.33/0.55 (define @t443 () (+ @t341 tptp.f7)) % 0.33/0.55 (define @t444 () (>= @t443 0/1)) % 0.33/0.55 (define @t445 () (not @t444)) % 0.33/0.55 (define @t446 () (>= tptp.f7 tptp.f5)) % 0.33/0.55 (assume @p1 (not (= tptp.f1 tptp.f2))) % 0.33/0.55 (assume @p2 (not (or @t5 @t2))) % 0.33/0.55 (assume @p3 @t15) % 0.33/0.55 (assume @p4 @t17) % 0.33/0.55 (assume @p5 @t21) % 0.33/0.55 (assume @p6 (< 0/1 tptp.f5)) % 0.33/0.55 (assume @p7 @t19) % 0.33/0.55 (assume @p8 (exists (@list @t22) (and (= @t22 0/1) (=> (< @t22 tptp.f5) (=> @t9 (not (= @t3 @t22))))))) % 0.33/0.55 (assume @p9 (forall @t33 (= @t32 (- @t30 @t27)))) % 0.33/0.55 (assume @p10 (forall @t33 (= @t35 (+ @t30 @t27)))) % 0.33/0.55 (assume @p11 (forall @t33 (= @t35 (+ (* @t28 @t29) (* @t24 @t26))))) % 0.33/0.55 (assume @p12 (forall @t33 (= @t38 (+ @t37 @t36)))) % 0.33/0.55 (assume @p13 (forall @t33 (= @t39 (- (* @t28 @t26) (* @t24 @t29))))) % 0.33/0.55 (assume @p14 (forall @t33 (= @t39 (- @t37 @t36)))) % 0.33/0.55 (assume @p15 (forall @t41 (exists (@list @t40) (and (= @t40 2/1) (= (tptp.f3 tptp.f4 (* @t40 @t25)) (* (* @t40 @t26) @t29)))))) % 0.33/0.55 (assume @p16 (forall @t41 (exists (@list @t43 @t42) (and (= @t43 @t29) (= @t42 @t26) (= (+ (* @t43 @t43) (* @t42 @t42)) 1/1))))) % 0.33/0.55 (assume @p17 (forall @t41 (=> (= @t29 1/1) (= @t26 0/1)))) % 0.33/0.55 (assume @p18 (forall @t41 (exists (@list @t45 @t44) (and (= @t45 0/1) (= @t44 @t29) (=> (= @t26 @t45) (and (=> @t46 (= (- @t44) 1/1)) (=> (not @t46) (= @t44 1/1)))))))) % 0.33/0.55 (assume @p19 (forall @t41 (= (tptp.f3 tptp.f4 (- @t25 tptp.f7)) @t47))) % 0.33/0.55 (assume @p20 (forall @t41 (= @t29 (tptp.f3 tptp.f4 @t49)))) % 0.33/0.55 (assume @p21 (not (= tptp.f7 0/1))) % 0.33/0.55 (assume @p22 (not (< tptp.f7 0/1))) % 0.33/0.55 (assume @p23 (not (= @t48 0/1))) % 0.33/0.55 (assume @p24 (exists (@list @t50) (and (= @t50 2/1) (not (= (/ tptp.f7 @t50) @t50))))) % 0.33/0.55 (assume @p25 (< 0/1 tptp.f7)) % 0.33/0.55 (assume @p26 (<= 0/1 tptp.f7)) % 0.33/0.55 (assume @p27 (< tptp.f7 4/1)) % 0.33/0.55 (assume @p28 (< 0/1 @t48)) % 0.33/0.55 (assume @p29 (<= 0/1 @t48)) % 0.33/0.55 (assume @p30 (<= 2/1 tptp.f7)) % 0.33/0.55 (assume @p31 (< @t51 0/1)) % 0.33/0.55 (assume @p32 (< (- @t18) tptp.f7)) % 0.33/0.55 (assume @p33 (exists (@list @t52) (and (= @t52 2/1) (< (/ tptp.f7 @t52) @t52)))) % 0.33/0.55 (assume @p34 (exists (@list @t53) (and (= @t53 2/1) (<= (/ tptp.f7 @t53) @t53)))) % 0.33/0.55 (assume @p35 (forall @t41 (exists (@list @t54) (and (= @t54 @t48) (=> (<= (- @t54) @t25) (=> (<= @t25 @t54) (<= 0/1 @t29))))))) % 0.33/0.55 (assume @p36 (forall @t41 (exists (@list @t55) (and (= @t55 @t48) (=> (< (- @t55) @t25) (=> (< @t25 @t55) (< 0/1 @t29))))))) % 0.33/0.55 (assume @p37 (forall @t33 (=> @t59 (=> @t57 (=> @t56 (<= @t29 @t28)))))) % 0.33/0.55 (assume @p38 (forall @t33 (=> @t59 (=> @t60 (=> @t56 (< @t29 @t28)))))) % 0.33/0.55 (assume @p39 (forall @t41 (exists (@list @t61) (and (= @t61 0/1) (=> (< @t61 @t25) (=> @t62 (< @t61 @t29))))))) % 0.33/0.55 (assume @p40 (forall @t33 (=> @t64 (=> @t57 (=> @t63 (<= @t28 @t29)))))) % 0.33/0.55 (assume @p41 (forall @t33 (=> @t64 (=> @t60 (=> @t63 (< @t28 @t29)))))) % 0.33/0.55 (assume @p42 (= (tptp.f3 tptp.f6 @t65) 0/1)) % 0.33/0.55 (assume @p43 (= (tptp.f3 tptp.f6 @t18) 1/1)) % 0.33/0.55 (assume @p44 (forall @t41 (= (tptp.f3 tptp.f6 @t66) @t29))) % 0.33/0.55 (assume @p45 (forall @t41 (= (tptp.f3 tptp.f6 @t67) (- @t29)))) % 0.33/0.55 (assume @p46 (= (tptp.f3 tptp.f6 (/ tptp.f7 3/1)) @t68)) % 0.33/0.55 (assume @p47 (= (tptp.f3 tptp.f6 @t48) 0/1)) % 0.33/0.55 (assume @p48 (= (tptp.f3 tptp.f6 tptp.f7) @t69)) % 0.33/0.55 (assume @p49 (forall @t41 (exists (@list @t70) (and (= @t70 0/1) (=> @t71 (=> (< @t25 @t70) (< @t26 @t70))))))) % 0.33/0.55 (assume @p50 (forall @t33 (exists (@list @t72) (and (= @t72 @t48) (=> (<= (- @t72) @t25) (=> @t57 (=> (<= @t23 @t72) (<= @t26 @t24)))))))) % 0.33/0.55 (assume @p51 (forall @t41 (exists (@list @t73) (and (= @t73 0/1) (=> (< @t73 @t25) (=> @t62 (< @t73 @t26))))))) % 0.33/0.55 (assume @p52 (forall @t41 (exists (@list @t74) (and (= @t74 0/1) (=> (<= @t74 @t25) (=> @t75 (<= @t74 @t26))))))) % 0.33/0.55 (assume @p53 (forall @t41 (exists (@list @t76) (and (= @t76 0/1) (=> (< @t76 @t25) (=> (< @t25 tptp.f7) (< @t76 @t26))))))) % 0.33/0.55 (assume @p54 (= (tptp.f3 tptp.f4 @t65) @t69)) % 0.33/0.55 (assume @p55 (= (tptp.f3 tptp.f4 @t18) 0/1)) % 0.33/0.55 (assume @p56 (forall @t41 (= (tptp.f3 tptp.f4 @t66) @t26))) % 0.33/0.55 (assume @p57 (forall @t41 (= (tptp.f3 tptp.f4 @t67) @t47))) % 0.33/0.55 (assume @p58 (= (tptp.f3 tptp.f4 @t77) @t68)) % 0.33/0.55 (assume @p59 (= (tptp.f3 tptp.f4 @t48) 1/1)) % 0.33/0.55 (assume @p60 (forall @t41 (= (tptp.f3 tptp.f4 (+ tptp.f7 @t25)) @t47))) % 0.33/0.55 (assume @p61 (= (tptp.f3 tptp.f4 tptp.f7) 0/1)) % 0.33/0.55 (assume @p62 (forall @t41 (exists (@list @t78) (and (= @t78 2/1) (=> @t79 (=> (< @t25 @t78) (< (tptp.f3 tptp.f6 (* @t78 @t25)) 1/1))))))) % 0.33/0.55 (assume @p63 (<= @t80 0/1)) % 0.33/0.55 (assume @p64 (< @t80 0/1)) % 0.33/0.55 (assume @p65 (forall @t41 (= (tptp.f3 tptp.f6 @t81) @t29))) % 0.33/0.55 (assume @p66 (forall @t41 (exists (@list @t82) (and (= @t82 @t29) (=> @t83 (<= (- @t82) 1/1)) (=> (not @t83) (<= @t82 1/1)))))) % 0.33/0.55 (assume @p67 (forall @t41 (<= @t29 1/1))) % 0.33/0.55 (assume @p68 (forall @t41 (<= @t69 @t29))) % 0.33/0.55 (assume @p69 (= (tptp.f3 tptp.f6 0/1) 1/1)) % 0.33/0.55 (assume @p70 (not (= @t80 0/1))) % 0.33/0.55 (assume @p71 (forall @t41 (exists (@list @t84) (and (= @t84 0/1) (=> (< @t84 @t25) (=> (< @t25 2/1) (< @t84 @t26))))))) % 0.33/0.55 (assume @p72 (forall @t41 (= (tptp.f3 tptp.f4 @t81) @t47))) % 0.33/0.55 (assume @p73 (forall @t41 (exists (@list @t85) (and (= @t85 @t26) (=> @t86 (<= (- @t85) 1/1)) (=> (not @t86) (<= @t85 1/1)))))) % 0.33/0.55 (assume @p74 (forall @t41 (<= @t26 1/1))) % 0.33/0.55 (assume @p75 (forall @t41 (<= @t69 @t26))) % 0.33/0.55 (assume @p76 (exists (@list @t87) (and (= @t87 0/1) (= (tptp.f3 tptp.f4 @t87) @t87)))) % 0.33/0.55 (assume @p77 (forall @t41 (= @t47 (tptp.f3 tptp.f6 (+ @t25 @t48))))) % 0.33/0.55 (assume @p78 (forall @t41 (= @t26 (tptp.f3 tptp.f6 @t49)))) % 0.33/0.55 (assume @p79 (forall @t41 (=> @t94 (=> @t93 (exists (@list @t23 @t90) (and (= @t90 @t48) (<= @t91 @t23) (<= @t23 @t90) (= @t24 @t25) (forall @t92 (=> (and (<= @t91 @t88) (<= @t88 @t90) (= (tptp.f3 tptp.f4 @t88) @t25)) @t89)))))))) % 0.33/0.55 (assume @p80 (forall @t41 (=> @t94 (=> @t93 (exists @t96 (and @t95 @t63 (= @t28 @t25) (forall @t92 (=> (and (<= 0/1 @t88) (<= @t88 tptp.f7) (= (tptp.f3 tptp.f6 @t88) @t25)) @t89)))))))) % 0.33/0.55 (assume @p81 (exists (@list @t25 @t97) (and (= @t97 0/1) (<= @t97 @t25) (<= @t25 2/1) (= @t29 @t97) (forall @t96 (=> (and (<= @t97 @t23) (<= @t23 2/1) (= @t28 @t97)) (= @t23 @t25)))))) % 0.33/0.55 (assume @p82 (forall @t33 (=> @t103 @t102))) % 0.33/0.55 (assume @p83 (forall @t33 (=> @t79 @t102))) % 0.33/0.55 (assume @p84 (forall @t33 (exists @t101 (and (= @t25 @t100) (= @t23 @t99))))) % 0.33/0.55 (assume @p85 (forall @t41 (exists (@list @t107) (and (= @t107 2/1) (exists (@list @t106 @t104) (and (= @t106 (/ tptp.f7 @t107)) (= @t104 (* @t107 @t25)) (=> (< (- @t106) @t25) (=> (< @t25 @t106) (= @t105 (/ (tptp.f3 tptp.f4 @t104) (+ (tptp.f3 tptp.f6 @t104) 1/1))))))))))) % 0.33/0.55 (assume @p86 (forall @t41 (exists (@list @t108) (and (= @t108 @t48) (=> (<= (- @t108) @t25) (=> (<= @t25 @t108) (= (tptp.f3 tptp.f9 @t26) @t25))))))) % 0.33/0.55 (assume @p87 (forall @t41 (exists (@list @t110 @t109) (and (= @t110 @t48) (= @t109 @t111) (=> @t94 (=> @t93 (and (<= (- @t110) @t109) (<= @t109 @t110) (= (tptp.f3 tptp.f4 @t109) @t25)))))))) % 0.33/0.55 (assume @p88 (forall @t41 (exists (@list @t112) (and (= @t112 @t111) (=> @t94 (=> @t93 (and (<= @t51 @t112) (<= @t112 tptp.f7) (= (tptp.f3 tptp.f4 @t112) @t25)))))))) % 0.33/0.55 (assume @p89 (exists (@list @t113) (and (= @t113 0/1) (= (tptp.f3 tptp.f8 @t113) @t113)))) % 0.33/0.55 (assume @p90 (forall @t41 (= (tptp.f3 tptp.f8 @t81) (- @t105)))) % 0.33/0.55 (assume @p91 (forall @t33 (exists (@list @t117 @t115 @t114) (and (= @t117 0/1) (= @t115 @t29) (= @t114 @t28) (=> (not (= @t115 @t117)) (=> (not (= @t114 @t117)) (= (- 1/1 (* @t105 @t116)) (/ @t32 (* @t115 @t114))))))))) % 0.33/0.55 (assume @p92 (forall @t33 (exists (@list @t121 @t120 @t119 @t118) (and (= @t121 0/1) (= @t120 @t31) (= @t119 @t105) (= @t118 @t116) (=> (not (= @t29 @t121)) (=> (not (= @t28 @t121)) (=> (not (= (tptp.f3 tptp.f6 @t120) @t121)) (= (tptp.f3 tptp.f8 @t120) (/ (+ @t119 @t118) (- 1/1 (* @t119 @t118))))))))))) % 0.33/0.55 (assume @p93 (forall @t41 (exists (@list @t122) (and (= @t122 0/1) (=> @t71 (=> (< @t25 @t122) (< @t105 @t122))))))) % 0.33/0.55 (assume @p94 (forall @t33 (exists (@list @t124) (and (= @t124 @t48) (exists (@list @t125) (and (= @t125 (- @t124)) (=> (< @t125 @t25) (=> (< @t25 @t124) (=> (< @t125 @t23) (=> (< @t23 @t124) (= @t60 @t123))))))))))) % 0.33/0.55 (assume @p95 (forall @t33 (exists (@list @t126) (and (= @t126 @t48) (=> (< (- @t126) @t25) (=> @t60 (=> (< @t23 @t126) @t123))))))) % 0.33/0.55 (assume @p96 (forall @t41 (exists (@list @t127) (and (= @t127 0/1) (=> (< @t127 @t25) (=> @t62 (< @t127 @t105))))))) % 0.33/0.55 (assume @p97 (forall @t41 (= (/ 1/1 @t105) (tptp.f3 tptp.f8 @t49)))) % 0.33/0.55 (assume @p98 (forall @t41 (= (tptp.f3 tptp.f8 @t66) @t105))) % 0.33/0.55 (assume @p99 (forall @t41 (= (tptp.f3 tptp.f8 @t67) @t105))) % 0.33/0.55 (assume @p100 (= (tptp.f3 tptp.f8 @t128) 1/1)) % 0.33/0.55 (assume @p101 (= (tptp.f3 tptp.f8 tptp.f7) 0/1)) % 0.33/0.55 (assume @p102 (forall @t41 (exists (@list @t129 @t130) (and (= @t129 @t48) (= @t130 @t111) (=> @t94 (=> @t93 (and (<= (- @t129) @t130) (<= @t130 @t129)))))))) % 0.33/0.55 (assume @p103 (forall @t41 (exists (@list @t131 @t132) (and (= @t131 @t48) (= @t132 @t111) (=> @t134 (=> @t133 (and (< (- @t131) @t132) (< @t132 @t131)))))))) % 0.33/0.55 (assume @p104 (forall @t41 (=> @t94 (=> @t93 (<= @t51 @t111))))) % 0.33/0.55 (assume @p105 (forall @t41 (=> @t94 (=> @t93 (<= @t111 @t48))))) % 0.33/0.55 (assume @p106 (forall @t41 (=> @t94 (=> @t93 (= (tptp.f3 tptp.f4 @t111) @t25))))) % 0.33/0.55 (assume @p107 (forall @t41 (= @t105 (/ @t26 @t29)))) % 0.33/0.55 (assume @p108 (forall @t33 (exists (@list @t137 @t136 @t135) (and (= @t137 0/1) (= @t136 @t29) (= @t135 @t28) (=> (not (= @t136 @t137)) (=> (not (= @t135 @t137)) (= (+ @t105 @t116) (/ @t38 (* @t136 @t135))))))))) % 0.33/0.55 (assume @p109 (forall @t41 (=> (and (=> @t103 (< @t81 1/1)) (=> @t140 @t133)) (exists (@list @t23 @t139) (and (= @t139 @t128) (< (- @t139) @t23) (< @t23 @t139) @t138))))) % 0.33/0.55 (assume @p110 (forall @t41 (=> @t64 (exists @t96 (and @t95 @t141 @t138))))) % 0.33/0.55 (assume @p111 (forall @t41 (=> @t79 (exists @t96 (and @t142 @t141 (< @t25 @t116)))))) % 0.33/0.55 (assume @p112 (forall @t41 (exists (@list @t23 @t143) (and (= @t143 @t48) (< @t144 @t23) (< @t23 @t143) @t138 (forall @t92 (=> (and (< @t144 @t88) (< @t88 @t143) (= (tptp.f3 tptp.f8 @t88) @t25)) @t89)))))) % 0.33/0.55 (assume @p113 (forall @t41 (exists (@list @t23 @t145) (and (= @t145 @t48) (< (- @t145) @t23) (< @t23 @t145) @t138)))) % 0.33/0.55 (assume @p114 (forall @t41 (=> @t64 (=> @t75 (= @t146 @t25))))) % 0.33/0.55 (assume @p115 (forall @t41 (=> @t94 (=> @t93 (<= 0/1 @t147))))) % 0.33/0.55 (assume @p116 (forall @t41 (=> (and (=> @t103 (<= @t81 1/1)) (=> @t140 @t93)) @t148))) % 0.33/0.55 (assume @p117 (forall @t41 (=> @t94 (=> @t93 @t148)))) % 0.33/0.55 (assume @p118 (forall @t41 (=> @t94 (=> @t93 (<= @t147 tptp.f7))))) % 0.33/0.55 (assume @p119 (forall @t41 (exists (@list @t149) (and (= @t149 @t147) (=> @t134 (=> @t133 (and (< 0/1 @t149) (< @t149 tptp.f7)))))))) % 0.33/0.55 (assume @p120 (forall @t41 (exists (@list @t150) (and (= @t150 @t147) (=> @t94 (=> @t93 (and (<= 0/1 @t150) (<= @t150 tptp.f7)))))))) % 0.33/0.55 (assume @p121 (forall @t41 (exists (@list @t151) (and (= @t151 @t147) (=> @t94 (=> @t93 (and (<= 0/1 @t151) (<= @t151 tptp.f7) (= (tptp.f3 tptp.f6 @t151) @t25)))))))) % 0.33/0.55 (assume @p122 (forall @t41 (=> (<= @t25 0/1) (=> @t59 (= @t146 @t81))))) % 0.33/0.55 (assume @p123 (forall @t41 (exists (@list @t153 @t152) (and (= @t153 @t48) (= @t152 @t154) (< (- @t153) @t152) (< @t152 @t153) (= (tptp.f3 tptp.f8 @t152) @t25))))) % 0.33/0.55 (assume @p124 (forall @t41 (exists (@list @t155) (and (= @t155 @t48) (=> (< (- @t155) @t25) (=> (< @t25 @t155) (= (tptp.f3 tptp.f11 @t105) @t25))))))) % 0.33/0.55 (assume @p125 (forall @t41 (exists (@list @t160 @t158) (and (= @t160 0/1) (= @t158 2/1) (exists (@list @t159 @t157) (and (= @t159 (* @t158 @t25)) (= @t157 @t105) (=> (not (= @t29 @t160)) (=> (not (= (tptp.f3 tptp.f6 @t159) @t160)) (= (tptp.f3 tptp.f8 @t159) (/ (* @t158 @t157) (- 1/1 (tptp.f12 (tptp.f13 tptp.f14 @t157) @t156)))))))))))) % 0.33/0.55 (assume @p126 (forall (@list @t25 @t161) (= (tptp.f3 tptp.f8 (+ @t25 (* @t162 tptp.f7))) @t105))) % 0.33/0.55 (assume @p127 (exists (@list @t163) (and (= @t163 0/1) (= (tptp.f3 tptp.f11 @t163) @t163)))) % 0.33/0.55 (assume @p128 (forall @t41 (= (tptp.f3 tptp.f11 @t81) (- @t154)))) % 0.33/0.55 (assume @p129 (forall @t33 (=> @t60 (< @t154 @t164)))) % 0.33/0.55 (assume @p130 (forall @t33 (=> @t57 (<= @t154 @t164)))) % 0.33/0.55 (assume @p131 (forall @t41 (exists (@list @t165) (and (= @t165 1/1) (=> (and (=> @t103 (< @t81 @t165)) (=> @t140 (< @t25 @t165))) (< @t167 @t165)))))) % 0.33/0.55 (assume @p132 (forall @t33 (exists (@list @t170 @t169) (and (= @t170 0/1) (= @t169 1/1) (=> (and (=> @t172 (<= @t81 @t169)) (=> (not @t172) (<= @t25 @t169))) (=> (and (=> @t171 (< (- @t23) @t169)) (=> (not @t171) (< @t23 @t169))) (= (+ @t154 @t164) (tptp.f3 tptp.f11 (/ @t31 (- @t169 @t168)))))))))) % 0.33/0.55 (assume @p133 (forall @t41 (not (= (tptp.f3 tptp.f6 @t154) 0/1)))) % 0.33/0.55 (assume @p134 (forall @t41 (exists (@list @t173 @t174) (and (= @t173 @t48) (= @t174 @t154) (< (- @t173) @t174) (< @t174 @t173))))) % 0.33/0.55 (assume @p135 @t187) % 0.33/0.55 (assume @p136 (forall @t41 (< @t51 @t154))) % 0.33/0.55 (assume @p137 (forall @t41 (< @t154 @t48))) % 0.33/0.55 (assume @p138 (= (tptp.f3 tptp.f11 1/1) @t128)) % 0.33/0.55 (assume @p139 (forall @t41 (= (tptp.f3 tptp.f8 @t154) @t25))) % 0.33/0.55 (assume @p140 (forall @t41 (exists (@list @t188) (and (= @t188 @t156) (= (tptp.f3 tptp.f6 @t191) (- (tptp.f12 @t190 @t188) (tptp.f12 @t189 @t188))))))) % 0.33/0.55 (assume @p141 (forall @t41 (exists (@list @t192) (and (= @t192 @t156) (= (tptp.f12 @t190 @t192) (- 1/1 (tptp.f12 @t189 @t192))))))) % 0.33/0.55 (assume @p142 (forall @t41 (exists (@list @t193) (and (= @t193 @t156) (= (tptp.f12 @t189 @t193) (- 1/1 (tptp.f12 @t190 @t193))))))) % 0.33/0.55 (assume @p143 (forall @t41 (exists (@list @t194) (and (= @t194 @t156) (= (+ (tptp.f12 @t190 @t194) (tptp.f12 @t189 @t194)) 1/1))))) % 0.33/0.55 (assume @p144 (forall @t41 (exists (@list @t195) (and (= @t195 @t156) (= (+ (tptp.f12 @t189 @t195) (tptp.f12 @t190 @t195)) 1/1))))) % 0.33/0.55 (assume @p145 (forall @t41 (exists (@list @t196 @t197) (and (= @t196 @t156) (= @t197 @t81) (= (+ (tptp.f12 (tptp.f13 tptp.f14 (+ (tptp.f3 tptp.f4 @t197) @t26)) @t196) (tptp.f12 (tptp.f13 tptp.f14 (- (tptp.f3 tptp.f6 @t197) @t29)) @t196)) 0/1))))) % 0.33/0.55 (assume @p146 (forall @t33 (exists (@list @t198 @t200 @t201 @t202 @t199 @t203) (and (= @t198 @t156) (= @t200 @t26) (= @t201 @t28) (= @t202 @t29) (= @t199 @t24) (= @t203 @t31) (= (+ (tptp.f12 (tptp.f13 tptp.f14 (- (tptp.f3 tptp.f4 @t203) (+ (* @t200 @t201) (* @t202 @t199)))) @t198) (tptp.f12 (tptp.f13 tptp.f14 (- (tptp.f3 tptp.f6 @t203) (- (* @t202 @t201) (* @t200 @t199)))) @t198)) 0/1))))) % 0.33/0.55 (assume @p147 (forall @t33 (exists (@list @t204) (and (= @t204 @t156) (= (+ (tptp.f12 (tptp.f13 tptp.f14 (* @t25 @t28)) @t204) (tptp.f12 (tptp.f13 tptp.f14 (* @t25 @t24)) @t204)) (tptp.f12 @t166 @t204)))))) % 0.33/0.55 (assume @p148 (forall @t33 (exists (@list @t205 @t206) (and (= @t205 0/1) (= @t206 @t156) (= (= (+ (tptp.f12 @t166 @t206) (tptp.f12 @t207 @t206)) @t205) (and (= @t25 @t205) (= @t23 @t205))))))) % 0.33/0.55 (assume @p149 (forall @t33 (exists (@list @t208) (and (= @t208 @t156) (= (tptp.f12 @t209 @t208) (+ (+ (tptp.f12 @t166 @t208) (tptp.f12 @t207 @t208)) (* @t191 @t23))))))) % 0.33/0.55 (assume @p150 (forall @t41 (exists (@list @t210) (and (= @t210 @t156) (= (* 4/1 (tptp.f12 @t166 @t210)) (tptp.f12 (tptp.f13 tptp.f14 @t191) @t210)))))) % 0.33/0.55 (assume @p151 (forall @t212 (<= 1/1 (tptp.f12 (tptp.f13 tptp.f14 2/1) @t211)))) % 0.33/0.55 (assume @p152 (forall @t33 (exists (@list @t213) (and (= @t213 @t156) (<= (- (tptp.f12 @t166 @t213)) (tptp.f12 @t207 @t213)))))) % 0.33/0.55 (assume @p153 (forall @t217 (=> @t79 (exists @t92 (and @t216 (= (tptp.f12 @t215 (tptp.f15 tptp.f16 (+ (tptp.f19 tptp.f20 @t214) 1))) @t25)))))) % 0.33/0.55 (assume @p154 (forall @t221 (=> @t220 (=> @t142 (exists @t92 (and @t216 @t218)))))) % 0.33/0.55 (assume @p155 (forall @t221 (=> @t220 (=> @t142 (exists @t92 (and @t216 @t218 (forall @t223 (=> (and (< 0/1 @t98) (= (tptp.f12 @t222 @t211) @t23)) (= @t98 @t88))))))))) % 0.33/0.55 (assume @p156 (forall @t41 (exists (@list @t224) (and (= @t224 @t156) (= (tptp.f12 @t225 @t224) (tptp.f12 @t166 @t224)))))) % 0.33/0.55 (assume @p157 (forall @t41 (= (tptp.f12 @t166 (tptp.f15 tptp.f16 1)) @t25))) % 0.33/0.55 (assume @p158 (forall @t217 (= (tptp.f3 tptp.f21 @t226) (tptp.f12 @t225 @t214)))) % 0.33/0.55 (assume @p159 (forall @t41 (exists (@list @t227) (and (= @t227 @t167) (= (tptp.f3 tptp.f21 @t227) @t227))))) % 0.33/0.55 (assume @p160 (forall (@list @t229 @t23) (exists (@list @t228) (and (= @t228 @t230) (= (= @t228 @t23) (= @t23 @t228)))))) % 0.33/0.55 (assume @p161 (forall @t233 (exists (@list @t231) (and (= @t231 @t232) (= (= @t231 @t161) (= @t161 @t231)))))) % 0.33/0.55 (assume @p162 (forall @t233 (= (= @t230 @t162) @t234))) % 0.33/0.55 (assume @p163 (forall @t233 (= (= @t232 (tptp.f22 tptp.f23 @t161)) @t234))) % 0.33/0.55 (assume @p164 (forall @t41 (exists (@list @t235 @t236) (and (= @t235 @t156) (= @t236 @t29) (=> (not (= @t236 0/1)) (= (+ 1/1 (tptp.f12 (tptp.f13 tptp.f14 @t105) @t235)) (tptp.f12 (tptp.f13 tptp.f14 (tptp.f3 tptp.f24 @t236)) @t235))))))) % 0.33/0.55 (assume @p165 (forall @t217 (= (tptp.f3 tptp.f24 @t226) (tptp.f12 (tptp.f13 tptp.f14 @t237) @t214)))) % 0.33/0.55 (assume @p166 (exists (@list @t238) (and (= @t238 0/1) (= (tptp.f3 tptp.f24 @t238) @t238)))) % 0.33/0.55 (assume @p167 (forall @t33 (= @t240 (* @t25 @t239)))) % 0.33/0.55 (assume @p168 (forall @t41 (=> (not @t241) (= (* @t237 @t25) 1/1)))) % 0.33/0.55 (assume @p169 (forall @t244 (exists (@list @t243) (and (= @t243 0/1) (=> (< @t243 @t25) (=> (< @t243 @t23) (=> @t242 (< (* @t88 @t237) (* @t98 @t239))))))))) % 0.33/0.55 (assume @p170 (forall @t244 (exists (@list @t245) (and (= @t245 0/1) (=> (< @t245 @t25) (=> (< @t245 @t23) (=> @t242 (< (* @t237 @t88) (* @t239 @t98))))))))) % 0.33/0.55 (assume @p171 (forall @t41 (exists (@list @t246) (and (= @t246 @t29) (=> (not (= @t246 0/1)) (= (tptp.f25 tptp.f8 @t25 (tptp.f3 tptp.f24 (tptp.f12 (tptp.f13 tptp.f14 @t246) @t156))) tptp.f1)))))) % 0.33/0.55 (assume @p172 (forall @t33 (=> @t248 @t247))) % 0.33/0.55 (assume @p173 (forall @t33 (= @t248 @t247))) % 0.33/0.55 (assume @p174 (forall @t41 (= (tptp.f25 tptp.f6 @t25 @t47) tptp.f1))) % 0.33/0.55 (assume @p175 (forall @t41 (= (tptp.f25 tptp.f4 @t25 @t29) tptp.f1))) % 0.33/0.55 (assume @p176 (forall @t41 (= (tptp.f25 tptp.f11 @t25 (tptp.f3 tptp.f24 (+ 1/1 @t167))) tptp.f1))) % 0.33/0.55 (assume @p177 (forall @t41 (= (tptp.f3 tptp.f24 @t237) @t25))) % 0.33/0.55 (assume @p178 (forall @t41 (exists (@list @t249) (and (= @t249 1/1) (=> @t134 (=> (< @t25 @t249) (= (tptp.f25 tptp.f9 @t25 (tptp.f3 tptp.f24 (tptp.f3 tptp.f26 (- @t249 @t167)))) tptp.f1))))))) % 0.33/0.55 (assume @p179 (forall @t41 (exists (@list @t250) (and (= @t250 1/1) (=> @t134 (=> (< @t25 @t250) (= (tptp.f25 tptp.f10 @t25 (tptp.f3 tptp.f24 (- (tptp.f3 tptp.f26 (- @t250 @t167))))) tptp.f1))))))) % 0.33/0.55 (assume @p180 (forall @t255 (=> @t254 (=> @t253 @t252)))) % 0.33/0.55 (assume @p181 (forall @t41 (= (tptp.f3 tptp.f26 @t237) @t257))) % 0.33/0.55 (assume @p182 (forall @t41 (exists (@list @t258) (and (= @t258 @t256) (=> @t64 (= (/ @t258 @t25) (tptp.f3 tptp.f24 @t258))))))) % 0.33/0.55 (assume @p183 (= (tptp.f3 tptp.f6 @t77) (/ @t259 2/1))) % 0.33/0.55 (assume @p184 (exists (@list @t260) (and (= @t260 2/1) (= (tptp.f3 tptp.f6 @t128) (/ (tptp.f3 tptp.f26 @t260) @t260))))) % 0.33/0.55 (assume @p185 (exists (@list @t261) (and (= @t261 2/1) (= (tptp.f3 tptp.f4 @t128) (/ (tptp.f3 tptp.f26 @t261) @t261))))) % 0.33/0.55 (assume @p186 (exists (@list @t262) (and (= @t262 3/1) (= (tptp.f3 tptp.f4 (/ tptp.f7 @t262)) (/ (tptp.f3 tptp.f26 @t262) 2/1))))) % 0.33/0.55 (assume @p187 (forall @t41 (=> @t79 (= (tptp.f12 (tptp.f13 tptp.f14 @t257) @t156) @t237)))) % 0.33/0.55 (assume @p188 (forall @t33 (exists (@list @t265) (and (= @t265 @t156) (exists (@list @t263) (and (= @t263 (/ @t25 (tptp.f3 tptp.f26 (+ (tptp.f12 @t166 @t265) (tptp.f12 @t207 @t265))))) (=> @t264 (<= (- @t263) 1/1)) (=> (not @t264) (<= @t263 1/1)))))))) % 0.33/0.55 (assume @p189 (forall @t33 (exists (@list @t266) (and (= @t266 @t156) (<= 0/1 (tptp.f3 tptp.f26 (+ (tptp.f12 @t166 @t266) (tptp.f12 @t207 @t266)))))))) % 0.33/0.55 (assume @p190 (forall @t244 (exists (@list @t267) (and (= @t267 @t156) (<= 0/1 (tptp.f3 tptp.f26 (* (+ (tptp.f12 @t166 @t267) (tptp.f12 @t207 @t267)) (+ (tptp.f12 @t215 @t267) (tptp.f12 @t222 @t267))))))))) % 0.33/0.55 (assume @p191 (forall @t33 (exists (@list @t268) (and (= @t268 @t156) (<= @t25 (tptp.f3 tptp.f26 (+ (tptp.f12 @t166 @t268) (tptp.f12 @t207 @t268)))))))) % 0.33/0.55 (assume @p192 (forall @t33 (exists (@list @t269) (and (= @t269 @t156) (<= @t25 (tptp.f3 tptp.f26 (+ (tptp.f12 @t207 @t269) (tptp.f12 @t166 @t269)))))))) % 0.33/0.55 (assume @p193 (forall @t33 (exists (@list @t270) (and (= @t270 @t156) (=> @t103 (<= @t81 @t271)) (=> @t140 (<= @t25 @t271)))))) % 0.33/0.55 (assume @p194 (forall @t33 (exists (@list @t272) (and (= @t272 @t156) (=> @t103 (<= @t81 @t273)) (=> @t140 (<= @t25 @t273)))))) % 0.33/0.55 (assume @p195 (forall @t217 (= (tptp.f3 tptp.f26 @t226) (tptp.f12 @t274 @t214)))) % 0.33/0.55 (assume @p196 (forall @t41 (and (=> @t103 (= @t275 @t81)) (=> @t140 (= @t275 @t25))))) % 0.33/0.55 (assume @p197 (forall @t244 (exists (@list @t276) (and (= @t276 @t156) (<= (tptp.f3 tptp.f26 (+ (tptp.f12 @t209 @t276) (tptp.f12 (tptp.f13 tptp.f14 (+ @t88 @t98)) @t276))) (+ (tptp.f3 tptp.f26 (+ (tptp.f12 @t166 @t276) (tptp.f12 @t215 @t276))) (tptp.f3 tptp.f26 (+ (tptp.f12 @t207 @t276) (tptp.f12 @t222 @t276))))))))) % 0.33/0.55 (assume @p198 (forall @t244 (exists (@list @t278) (and (= @t278 @t156) (exists (@list @t277) (and (= @t277 (* (+ (tptp.f12 @t166 @t278) (tptp.f12 @t207 @t278)) (+ (tptp.f12 @t215 @t278) (tptp.f12 @t222 @t278)))) (= (tptp.f12 (tptp.f13 tptp.f14 (tptp.f3 tptp.f26 @t277)) @t278) @t277))))))) % 0.33/0.55 (assume @p199 (forall @t41 (= @t280 @t64))) % 0.33/0.55 (assume @p200 (forall @t41 (exists (@list @t281) (and (= @t281 0/1) (=> (< @t281 @t25) (< @t281 @t279)))))) % 0.33/0.55 (assume @p201 (forall @t41 (=> @t64 @t280))) % 0.33/0.55 (assume @p202 (forall @t285 (exists (@list @t283 @t282 @t284) (and (= @t283 0/1) (= @t282 @t156) (= @t284 (/ @t25 2/1)) (=> (< @t283 @t25) (=> (< @t23 @t284) (=> (< @t88 @t284) (=> (<= @t283 @t23) (=> (<= @t283 @t88) (< (tptp.f3 tptp.f26 (+ (tptp.f12 @t207 @t282) (tptp.f12 @t215 @t282))) @t25)))))))))) % 0.33/0.55 (assume @p203 (forall @t285 (exists (@list @t288 @t286 @t287) (and (= @t288 0/1) (= @t286 @t156) (= @t287 (/ @t23 @t291)) (=> (and (=> @t290 (< @t81 @t287)) (=> (not @t290) (< @t25 @t287))) (=> (and (=> @t289 (< (- @t88) @t287)) (=> (not @t289) (< @t88 @t287))) (< (tptp.f3 tptp.f26 (+ (tptp.f12 @t166 @t286) (tptp.f12 @t215 @t286))) @t23))))))) % 0.33/0.55 (assume @p204 (forall @t33 (exists (@list @t292) (and (= @t292 @t156) (=> (= (tptp.f3 tptp.f26 (+ (tptp.f12 @t166 @t292) (tptp.f12 @t207 @t292))) @t25) (= @t23 0/1)))))) % 0.33/0.55 (assume @p205 (forall @t33 (exists (@list @t293) (and (= @t293 @t156) (=> (= (tptp.f3 tptp.f26 (+ (tptp.f12 @t166 @t293) (tptp.f12 @t207 @t293))) @t23) @t241))))) % 0.33/0.55 (assume @p206 (forall @t33 (=> (= @t167 @t23) (=> @t64 (= @t294 @t25))))) % 0.33/0.55 (assume @p207 (< 1/1 @t291)) % 0.33/0.55 (assume @p208 (< 0/1 @t291)) % 0.33/0.55 (assume @p209 (<= 0/1 @t291)) % 0.33/0.55 (assume @p210 (forall @t33 (<= 0/1 @t296))) % 0.33/0.55 (assume @p211 (forall @t33 (<= @t25 @t296))) % 0.33/0.55 (assume @p212 (exists (@list @t297) (and (= @t297 1/1) (= (tptp.f3 tptp.f26 @t297) @t297)))) % 0.33/0.55 (assume @p213 (exists (@list @t298) (and (= @t298 0/1) (= (tptp.f3 tptp.f26 @t298) @t298)))) % 0.33/0.55 (assume @p214 (forall @t41 (= (tptp.f3 tptp.f26 @t81) (- @t256)))) % 0.33/0.55 (assume @p215 (forall @t41 (and (=> @t103 (= @t299 @t81)) (=> @t140 (= @t299 @t25))))) % 0.33/0.55 (assume @p216 (forall @t33 (= (tptp.f3 tptp.f26 @t168) (* @t256 @t294)))) % 0.33/0.55 (assume @p217 (forall @t33 (= (tptp.f3 tptp.f26 @t240) (/ @t256 @t294)))) % 0.33/0.55 (assume @p218 (forall @t41 (exists (@list @t300) (and (= @t300 1/1) (= (< @t300 @t256) (< @t300 @t25)))))) % 0.33/0.55 (assume @p219 (forall @t41 (exists (@list @t301) (and (= @t301 0/1) (= (< @t301 @t256) (< @t301 @t25)))))) % 0.33/0.55 (assume @p220 (forall @t41 (exists (@list @t302) (and (= @t302 1/1) (= (<= @t302 @t256) (<= @t302 @t25)))))) % 0.33/0.55 (assume @p221 (forall @t41 (exists (@list @t303) (and (= @t303 0/1) (= (<= @t303 @t256) (<= @t303 @t25)))))) % 0.33/0.55 (assume @p222 (forall @t41 (exists (@list @t304) (and (= @t304 1/1) (= (= @t256 @t304) (= @t25 @t304)))))) % 0.33/0.55 (assume @p223 (forall @t41 (exists (@list @t305) (and (= @t305 0/1) (= (= @t256 @t305) (= @t25 @t305)))))) % 0.33/0.55 (assume @p224 (forall @t41 (exists (@list @t306) (and (= @t306 1/1) (= (< @t256 @t306) (< @t25 @t306)))))) % 0.33/0.55 (assume @p225 (forall @t41 (exists (@list @t307) (and (= @t307 0/1) (= (< @t256 @t307) (< @t25 @t307)))))) % 0.33/0.55 (assume @p226 (forall @t41 (exists (@list @t308) (and (= @t308 1/1) (= (<= @t256 @t308) (<= @t25 @t308)))))) % 0.33/0.55 (assume @p227 (forall @t41 (exists (@list @t309) (and (= @t309 0/1) (= (<= @t256 @t309) (<= @t25 @t309)))))) % 0.33/0.55 (assume @p228 (forall @t33 (= (= @t256 @t294) @t247))) % 0.33/0.55 (assume @p229 (forall @t33 (= @t310 @t60))) % 0.33/0.55 (assume @p230 (forall @t33 (= @t311 @t57))) % 0.33/0.55 (assume @p231 (forall @t41 (exists (@list @t312) (and (= @t312 0/1) (=> (< @t312 @t25) (not (= @t256 @t312))))))) % 0.33/0.55 (assume @p232 (forall @t41 (exists (@list @t313) (and (= @t313 0/1) (=> (< @t313 @t25) (< @t313 @t256)))))) % 0.33/0.55 (assume @p233 (forall @t41 (exists (@list @t314) (and (= @t314 1/1) (=> (<= @t314 @t25) (<= @t314 @t256)))))) % 0.33/0.55 (assume @p234 (forall @t41 (exists (@list @t315) (and (= @t315 0/1) (=> (<= @t315 @t25) (<= @t315 @t256)))))) % 0.33/0.55 (assume @p235 (forall @t41 (=> @t79 (< (/ @t25 @t291) @t25)))) % 0.33/0.55 (assume @p236 (forall @t41 (exists (@list @t316) (and (= @t316 0/1) (=> (<= @t316 @t25) (=> (= @t256 @t316) (= @t25 @t316))))))) % 0.33/0.55 (assume @p237 (forall @t33 (=> @t60 @t310))) % 0.33/0.55 (assume @p238 (forall @t33 (=> @t57 @t311))) % 0.33/0.55 (assume @p239 (= (tptp.f3 tptp.f8 @t77) (/ 1/1 @t259))) % 0.33/0.55 (assume @p240 (exists (@list @t317) (and (= @t317 3/1) (= (tptp.f3 tptp.f8 (/ tptp.f7 @t317)) (tptp.f3 tptp.f26 @t317))))) % 0.33/0.55 (assume @p241 (forall @t41 (=> @t79 (= (tptp.f25 tptp.f26 @t25 (/ @t257 2/1)) tptp.f1)))) % 0.33/0.55 (assume @p242 (forall @t33 (exists (@list @t320 @t318 @t319) (and (= @t320 0/1) (= @t318 2/1) (= @t319 @t257) (=> (not (= @t25 @t320)) (=> (=> (< @t320 @t25) (= @t23 (/ @t319 @t318))) (=> (=> (< @t25 @t320) (= @t23 (/ (- @t319) @t318))) (= (tptp.f25 tptp.f26 @t25 @t23) tptp.f1)))))))) % 0.33/0.55 (assume @p243 (forall @t41 (exists (@list @t321) (and (= @t321 1/1) (= @t154 (* 2/1 (tptp.f3 tptp.f11 (/ @t25 (+ @t321 (tptp.f3 tptp.f26 (+ @t321 @t167))))))))))) % 0.33/0.55 (assume @p244 (forall @t33 (exists (@list @t323) (and (= @t323 @t156) (exists (@list @t322) (and (= @t322 (/ @t25 (tptp.f3 tptp.f26 (+ (tptp.f12 @t166 @t323) (tptp.f12 @t207 @t323))))) (= (tptp.f3 tptp.f6 (tptp.f3 tptp.f10 @t322)) @t322))))))) % 0.33/0.55 (assume @p245 (forall @t41 (exists (@list @t324) (and (= @t324 1/1) (=> (and (=> @t103 (<= @t81 @t324)) (=> @t140 (<= @t25 @t324))) (= @t325 (tptp.f3 tptp.f26 (- @t324 @t167)))))))) % 0.33/0.55 (assume @p246 (forall @t41 (exists (@list @t326) (and (= @t326 1/1) (=> @t94 (=> (<= @t25 @t326) (= @t325 (tptp.f3 tptp.f26 (- @t326 @t167))))))))) % 0.33/0.55 (assume @p247 (forall @t33 (exists (@list @t327) (and (= @t327 @t156) (exists (@list @t328) (and (= @t328 (/ @t25 (tptp.f3 tptp.f26 (+ (tptp.f12 @t166 @t327) (tptp.f12 @t207 @t327))))) (= (tptp.f3 tptp.f4 (tptp.f3 tptp.f10 @t328)) (tptp.f3 tptp.f26 (- 1/1 (tptp.f12 (tptp.f13 tptp.f14 @t328) @t327)))))))))) % 0.33/0.55 (assume @p248 (forall @t41 (exists (@list @t329) (and (= @t329 1/1) (=> @t94 (=> (<= @t25 @t329) (= (tptp.f3 tptp.f6 @t111) (tptp.f3 tptp.f26 (- @t329 @t167))))))))) % 0.33/0.55 (assume @p249 (forall @t255 (=> @t254 (=> @t252 @t253)))) % 0.33/0.55 (assume @p250 (forall (@list @t251 @t23 @t88) (=> (forall @t223 (= (tptp.f25 @t251 @t98 0/1) tptp.f1)) (= (tptp.f3 @t251 @t23) (tptp.f3 @t251 @t88))))) % 0.33/0.55 (assume @p251 (forall (@list @t25 @t23 @t331 @t98) (exists (@list @t330) (and (= @t330 2/1) (=> (not @t247) (=> (forall (@list @t332) (= (tptp.f25 @t331 @t332 @t98) tptp.f1)) (= (tptp.f3 @t331 (/ @t31 @t330)) (/ (+ (tptp.f3 @t331 @t25) (tptp.f3 @t331 @t23)) @t330)))))))) % 0.33/0.55 (assume @p252 (forall @t212 (= (tptp.f15 tptp.f16 @t219) @t211))) % 0.33/0.55 (assume @p253 (forall @t334 (=> (<= 0 @t229) (= @t333 @t229)))) % 0.33/0.55 (assume @p254 (forall @t334 (=> (< @t229 0) (= @t333 0)))) % 0.33/0.55 (step @p255 :rule arith-elim-leq :args (@t339 0/1)) % 0.33/0.55 (step @p256 :rule symm :premises (@p255)) % 0.33/0.55 (step @p257 :rule cong :premises (@p256) :args ((not @t340))) % 0.33/0.55 (step @p258 :rule arith-elim-gt :args (@t339 0/1)) % 0.33/0.55 (step @p259 :rule trans :premises (@p258 @p257)) % 0.33/0.55 (step @p260 :rule arith_poly_norm :args ((= (* -1/1 (- 0/1 tptp.f5)) (* -1/1 (- @t341 0/1))))) % 0.33/0.55 (step @p261 :rule arith_poly_norm_rel :premises (@p260) :args ((= @t343 @t342))) % 0.33/0.55 (step @p262 :rule cong :premises (@p261) :args ((not @t343))) % 0.33/0.55 (step @p263 :rule arith-elim-lt :args (0/1 tptp.f5)) % 0.33/0.55 (step @p264 :rule trans :premises (@p263 @p262)) % 0.33/0.55 (step @p265 :rule eq_resolve :premises (@p6 @p264)) % 0.33/0.55 (step @p266 :rule bool-double-not-elim :args (@t344)) % 0.33/0.55 (step @p267 :rule bool-double-not-elim :args (@t342)) % 0.33/0.55 (step @p268 :rule nary_cong :premises (@p267 @p266) :args ((or (not @t346) (not @t345)))) % 0.33/0.55 (step @p269 :rule aci_norm :args ((= (and @t346 @t345 true) (and @t346 @t345)))) % 0.33/0.55 (step @p270 :rule evaluate :args (@t347)) % 0.33/0.55 (step @p271 :rule refl :args (@t345)) % 0.33/0.55 (step @p272 :rule refl :args (@t346)) % 0.33/0.55 (step @p273 :rule nary_cong :premises (@p272 @p271 @p270) :args (@t348)) % 0.33/0.55 (step @p274 :rule trans :premises (@p273 @p269)) % 0.33/0.55 (step @p275 :rule cong :premises (@p274) :args ((not @t348))) % 0.33/0.55 (step @p276 :rule refl :args (0/1)) % 0.33/0.55 (step @p277 :rule not_or_elim :premises (@p2) :args (0)) % 0.33/0.55 (step @p278 :rule not_not_elim :premises (@p277)) % 0.33/0.55 (step @p279 :rule cong :premises (@p278 @p276) :args (@t4)) % 0.33/0.55 (step @p280 :rule nary_cong :premises (@p272 @p271 @p279) :args (@t349)) % 0.33/0.55 (step @p281 :rule cong :premises (@p280) :args ((not @t349))) % 0.33/0.55 (step @p282 :rule trans :premises (@p281 @p275)) % 0.33/0.55 (step @p283 :rule refl :args (@t4)) % 0.33/0.55 (step @p284 :rule refl :args (0/1)) % 0.33/0.55 (step @p285 :rule arith_poly_norm :args ((= (+ tptp.f5 @t350) @t339))) % 0.33/0.55 (step @p286 :rule arith_poly_norm :args ((= @t354 @t350))) % 0.33/0.55 (step @p287 :rule refl :args (tptp.f5)) % 0.33/0.55 (step @p288 :rule nary_cong :premises (@p287 @p286) :args (@t355)) % 0.33/0.55 (step @p289 :rule trans :premises (@p288 @p285)) % 0.33/0.55 (step @p290 :rule cong :premises (@p289 @p284) :args (@t356)) % 0.33/0.55 (step @p291 :rule cong :premises (@p290) :args (@t357)) % 0.33/0.55 (step @p292 :rule nary_cong :premises (@p272 @p291 @p283) :args (@t358)) % 0.33/0.55 (step @p293 :rule cong :premises (@p292) :args ((not @t358))) % 0.33/0.55 (step @p294 :rule refl :args (0/1)) % 0.33/0.55 (step @p295 :rule bool-double-not-elim :args (@t359)) % 0.33/0.55 (step @p296 :rule aci_norm :args ((= (or false @t360) @t360))) % 0.33/0.55 (step @p297 :rule arith_poly_norm :args ((= (* 1/1 (- @t364 @t363)) (* 1/4 (- tptp.f7 @t353))))) % 0.33/0.55 (step @p298 :rule arith_poly_norm_rel :premises (@p297) :args ((= (= @t364 @t363) @t359))) % 0.33/0.55 (step @p299 :rule refl :args (@t361)) % 0.33/0.55 (step @p300 :rule arith_poly_norm :args ((= @t365 @t362))) % 0.33/0.55 (step @p301 :rule nary_cong :premises (@p300 @p299) :args (@t366)) % 0.33/0.55 (step @p302 :rule arith_poly_norm :args ((= @t367 @t364))) % 0.33/0.55 (step @p303 :rule arith_poly_norm :args ((= @t128 @t367))) % 0.33/0.55 (step @p304 :rule trans :premises (@p303 @p302)) % 0.33/0.55 (step @p305 :rule cong :premises (@p304 @p301) :args (@t368)) % 0.33/0.55 (step @p306 :rule trans :premises (@p305 @p298)) % 0.33/0.55 (step @p307 :rule cong :premises (@p306) :args (@t369)) % 0.33/0.55 (step @p308 :rule evaluate :args ((not true))) % 0.33/0.55 (step @p309 :rule evaluate :args (@t370)) % 0.33/0.55 (step @p310 :rule cong :premises (@p309) :args (@t371)) % 0.33/0.55 (step @p311 :rule trans :premises (@p310 @p308)) % 0.33/0.55 (step @p312 :rule nary_cong :premises (@p311 @p307) :args (@t372)) % 0.33/0.55 (step @p313 :rule trans :premises (@p312 @p296)) % 0.33/0.55 (step @p314 :rule quant-var-elim-eq :args ((= (forall @t186 @t377) @t372))) % 0.33/0.55 (step @p315 :rule aci_norm :args ((= @t378 @t377))) % 0.33/0.55 (step @p316 :rule cong :premises (@p315) :args ((forall @t186 @t378))) % 0.33/0.55 (step @p317 :rule trans :premises (@p316 @p314)) % 0.33/0.55 (step @p318 :rule trans :premises (@p317 @p313)) % 0.33/0.55 (step @p319 :rule bool-and-de-morgan :args (@t184 @t374 true)) % 0.33/0.55 (step @p320 :rule cong :premises (@p319) :args (@t380)) % 0.33/0.55 (step @p321 :rule trans :premises (@p320 @p318)) % 0.33/0.55 (step @p322 :rule cong :premises (@p321) :args (@t381)) % 0.33/0.55 (step @p323 :rule trans :premises (@p322 @p295)) % 0.33/0.55 (step @p324 :rule exists-elim :args ((= (exists @t186 @t379) @t381))) % 0.33/0.55 (step @p325 :rule trans :premises (@p324 @p323)) % 0.33/0.55 (step @p326 :rule evaluate :args (@t175)) % 0.33/0.55 (step @p327 :rule refl :args (tptp.f11)) % 0.33/0.55 (step @p328 :rule cong :premises (@p327 @p326) :args (@t176)) % 0.33/0.55 (step @p329 :rule refl :args (-1/1)) % 0.33/0.55 (step @p330 :rule nary_cong :premises (@p329 @p328) :args (@t382)) % 0.33/0.55 (step @p331 :rule arith_poly_norm :args ((= (* @t179 @t337) @t373))) % 0.33/0.55 (step @p332 :rule evaluate :args (@t177)) % 0.33/0.55 (step @p333 :rule cong :premises (@p327 @p332) :args (@t178)) % 0.33/0.55 (step @p334 :rule refl :args (@t179)) % 0.33/0.55 (step @p335 :rule nary_cong :premises (@p334 @p333) :args (@t180)) % 0.33/0.55 (step @p336 :rule trans :premises (@p335 @p331)) % 0.33/0.55 (step @p337 :rule nary_cong :premises (@p336 @p330) :args (@t383)) % 0.33/0.55 (step @p338 :rule arith_poly_norm :args ((= @t181 @t383))) % 0.33/0.55 (step @p339 :rule trans :premises (@p338 @p337)) % 0.33/0.55 (step @p340 :rule refl :args (@t182)) % 0.33/0.55 (step @p341 :rule cong :premises (@p340 @p339) :args (@t183)) % 0.33/0.55 (step @p342 :rule refl :args (@t184)) % 0.33/0.55 (step @p343 :rule nary_cong :premises (@p342 @p341) :args (@t185)) % 0.33/0.55 (step @p344 :rule cong :premises (@p343) :args (@t187)) % 0.33/0.55 (step @p345 :rule trans :premises (@p344 @p325)) % 0.33/0.55 (step @p346 :rule eq_resolve :premises (@p135 @p345)) % 0.33/0.55 (step @p347 :rule refl :args (-1/1)) % 0.33/0.55 (step @p348 :rule nary_cong :premises (@p347 @p346) :args (@t384)) % 0.33/0.55 (step @p349 :rule nary_cong :premises (@p287 @p348) :args (@t385)) % 0.33/0.55 (step @p350 :rule cong :premises (@p349 @p294) :args (@t386)) % 0.33/0.55 (step @p351 :rule cong :premises (@p350) :args (@t387)) % 0.33/0.55 (step @p352 :rule nary_cong :premises (@p272 @p351 @p283) :args (@t388)) % 0.33/0.55 (step @p353 :rule cong :premises (@p352) :args ((not @t388))) % 0.33/0.55 (step @p354 :rule trans :premises (@p353 @p293)) % 0.33/0.55 (step @p355 :rule aci_norm :args ((= (or false @t388) @t388))) % 0.33/0.55 (step @p356 :rule arith_poly_norm :args ((= (* 1/1 (- 0/1 @t3)) (* -1/1 (- @t3 0/1))))) % 0.33/0.55 (step @p357 :rule arith_poly_norm_rel :premises (@p356) :args ((= @t389 @t4))) % 0.33/0.55 (step @p358 :rule refl :args (@t387)) % 0.33/0.55 (step @p359 :rule refl :args (0/1)) % 0.33/0.55 (step @p360 :rule arith_poly_norm :args ((= @t390 @t341))) % 0.33/0.55 (step @p361 :rule cong :premises (@p360 @p359) :args (@t391)) % 0.33/0.55 (step @p362 :rule cong :premises (@p361) :args (@t392)) % 0.33/0.55 (step @p363 :rule nary_cong :premises (@p362 @p358 @p357) :args (@t393)) % 0.33/0.55 (step @p364 :rule cong :premises (@p270) :args (@t394)) % 0.33/0.55 (step @p365 :rule trans :premises (@p364 @p308)) % 0.33/0.55 (step @p366 :rule nary_cong :premises (@p365 @p363) :args (@t395)) % 0.33/0.55 (step @p367 :rule trans :premises (@p366 @p355)) % 0.33/0.55 (step @p368 :rule quant-var-elim-eq :args ((= (forall @t14 @t402) @t395))) % 0.33/0.55 (step @p369 :rule aci_norm :args ((= @t403 @t402))) % 0.33/0.55 (step @p370 :rule cong :premises (@p369) :args ((forall @t14 @t403))) % 0.33/0.55 (step @p371 :rule trans :premises (@p370 @p368)) % 0.33/0.55 (step @p372 :rule trans :premises (@p371 @p367)) % 0.33/0.55 (step @p373 :rule aci_norm :args ((= (and @t399 (and @t387 @t396)) @t400))) % 0.33/0.55 (step @p374 :rule bool-double-not-elim :args (@t396)) % 0.33/0.55 (step @p375 :rule refl :args (@t387)) % 0.33/0.55 (step @p376 :rule nary_cong :premises (@p375 @p374) :args ((and @t387 (not @t404)))) % 0.33/0.55 (step @p377 :rule bool-implies-de-morgan :args (@t387 @t404)) % 0.33/0.55 (step @p378 :rule trans :premises (@p377 @p376)) % 0.33/0.55 (step @p379 :rule refl :args (@t399)) % 0.33/0.55 (step @p380 :rule nary_cong :premises (@p379 @p378) :args ((and @t399 (not @t405)))) % 0.33/0.55 (step @p381 :rule trans :premises (@p380 @p373)) % 0.33/0.55 (step @p382 :rule bool-implies-de-morgan :args (@t399 @t405)) % 0.33/0.55 (step @p383 :rule trans :premises (@p382 @p381)) % 0.33/0.55 (step @p384 :rule refl :args (@t401)) % 0.33/0.55 (step @p385 :rule nary_cong :premises (@p384 @p383) :args ((or @t401 (not @t406)))) % 0.33/0.55 (step @p386 :rule bool-and-de-morgan :args (@t12 @t406 true)) % 0.33/0.55 (step @p387 :rule trans :premises (@p386 @p385)) % 0.33/0.55 (step @p388 :rule cong :premises (@p387) :args (@t408)) % 0.33/0.55 (step @p389 :rule trans :premises (@p388 @p372)) % 0.33/0.55 (step @p390 :rule cong :premises (@p389) :args (@t409)) % 0.33/0.55 (step @p391 :rule exists-elim :args ((= (exists @t14 @t407) @t409))) % 0.33/0.55 (step @p392 :rule trans :premises (@p391 @p390)) % 0.33/0.55 (step @p393 :rule arith_poly_norm :args ((= (* -1/1 (- @t3 @t6)) (* 1/1 (- @t6 @t3))))) % 0.33/0.55 (step @p394 :rule arith_poly_norm_rel :premises (@p393) :args ((= @t7 @t396))) % 0.33/0.55 (step @p395 :rule cong :premises (@p394) :args (@t8)) % 0.33/0.55 (step @p396 :rule arith_poly_norm :args ((= (* 1/1 (- tptp.f5 tptp.f7)) (* 1/1 (- @t385 0/1))))) % 0.33/0.55 (step @p397 :rule arith_poly_norm_rel :premises (@p396) :args ((= @t410 @t386))) % 0.33/0.55 (step @p398 :rule cong :premises (@p397) :args ((not @t410))) % 0.33/0.55 (step @p399 :rule arith-elim-lt :args (tptp.f5 tptp.f7)) % 0.33/0.55 (step @p400 :rule trans :premises (@p399 @p398)) % 0.33/0.55 (step @p401 :rule cong :premises (@p400 @p395) :args (@t10)) % 0.33/0.55 (step @p402 :rule arith_poly_norm :args ((= (* -1/1 (- @t6 tptp.f5)) (* -1/1 (- @t397 0/1))))) % 0.33/0.55 (step @p403 :rule arith_poly_norm_rel :premises (@p402) :args ((= @t411 @t398))) % 0.33/0.55 (step @p404 :rule cong :premises (@p403) :args ((not @t411))) % 0.33/0.55 (step @p405 :rule arith-elim-lt :args (@t6 tptp.f5)) % 0.33/0.55 (step @p406 :rule trans :premises (@p405 @p404)) % 0.33/0.55 (step @p407 :rule cong :premises (@p406 @p401) :args (@t11)) % 0.33/0.55 (step @p408 :rule refl :args (@t12)) % 0.33/0.55 (step @p409 :rule nary_cong :premises (@p408 @p407) :args (@t13)) % 0.33/0.55 (step @p410 :rule cong :premises (@p409) :args (@t15)) % 0.33/0.55 (step @p411 :rule trans :premises (@p410 @p392)) % 0.33/0.55 (step @p412 :rule trans :premises (@p411 @p354 @p282)) % 0.33/0.55 (step @p413 :rule eq_resolve :premises (@p3 @p412)) % 0.33/0.55 (step @p414 :rule not_and :premises (@p413)) % 0.33/0.55 (step @p415 :rule eq_resolve :premises (@p414 @p268)) % 0.33/0.55 (step @p416 :rule chain_m_resolution :premises (@p415 @p265) :args (@t344 @t412 (@list @t342))) % 0.33/0.55 (step @p417 :rule arith_poly_norm :args ((= (* 1/1 (- @t339 0/1)) (* 1/1 (- tptp.f5 @t353))))) % 0.33/0.55 (step @p418 :rule arith_poly_norm_rel :premises (@p417) :args ((= @t414 @t413))) % 0.33/0.55 (step @p419 :rule cong :premises (@p418) :args ((not @t414))) % 0.33/0.55 (step @p420 :rule symm :premises (@p419)) % 0.33/0.55 (step @p421 :rule bool-impl-false1 :args (@t413)) % 0.33/0.55 (step @p422 :rule evaluate :args (@t415)) % 0.33/0.55 (step @p423 :rule cong :premises (@p422) :args (@t416)) % 0.33/0.55 (step @p424 :rule trans :premises (@p423 @p308)) % 0.33/0.55 (step @p425 :rule refl :args (@t413)) % 0.33/0.55 (step @p426 :rule cong :premises (@p425 @p424) :args ((=> @t413 @t416))) % 0.33/0.55 (step @p427 :rule trans :premises (@p426 @p421)) % 0.33/0.55 (step @p428 :rule refl :args (1/1)) % 0.33/0.55 (step @p429 :rule not_or_elim :premises (@p2) :args (1)) % 0.33/0.55 (step @p430 :rule not_not_elim :premises (@p429)) % 0.33/0.55 (step @p431 :rule cong :premises (@p430 @p428) :args (@t1)) % 0.33/0.55 (step @p432 :rule cong :premises (@p431) :args (@t2)) % 0.33/0.55 (step @p433 :rule cong :premises (@p425 @p432) :args ((=> @t413 @t2))) % 0.33/0.55 (step @p434 :rule trans :premises (@p433 @p427)) % 0.33/0.55 (step @p435 :rule refl :args (@t2)) % 0.33/0.55 (step @p436 :rule cong :premises (@p287 @p346) :args (@t16)) % 0.33/0.55 (step @p437 :rule cong :premises (@p436 @p435) :args (@t17)) % 0.33/0.55 (step @p438 :rule trans :premises (@p437 @p434)) % 0.33/0.55 (step @p439 :rule eq_resolve :premises (@p4 @p438)) % 0.33/0.55 (step @p440 :rule eq_resolve :premises (@p439 @p420)) % 0.33/0.55 (step @p441 :rule arith_trichotomy :premises (@p440 @p416)) % 0.33/0.55 (step @p442 :rule eq_resolve :premises (@p441 @p259)) % 0.33/0.55 (step @p443 :rule arith_poly_norm :args ((= (* -1/1 (- 0/1 @t339)) (* -1/1 (- @t417 0/1))))) % 0.33/0.55 (step @p444 :rule arith_poly_norm_rel :premises (@p443) :args ((= @t340 @t418))) % 0.33/0.55 (step @p445 :rule trans :premises (@p255 @p444)) % 0.33/0.55 (step @p446 :rule symm :premises (@p445)) % 0.33/0.55 (step @p447 :rule refl :args (0/1)) % 0.33/0.55 (step @p448 :rule arith_poly_norm :args ((= (+ tptp.f5 @t422) @t421))) % 0.33/0.55 (step @p449 :rule arith_poly_norm :args ((= @t423 @t422))) % 0.33/0.55 (step @p450 :rule nary_cong :premises (@p287 @p449) :args (@t424)) % 0.33/0.55 (step @p451 :rule trans :premises (@p450 @p448)) % 0.33/0.55 (step @p452 :rule cong :premises (@p451 @p447) :args (@t425)) % 0.33/0.55 (step @p453 :rule cong :premises (@p452) :args (@t426)) % 0.33/0.55 (step @p454 :rule refl :args (0/1)) % 0.33/0.55 (step @p455 :rule refl :args (-2/1)) % 0.33/0.55 (step @p456 :rule nary_cong :premises (@p455 @p346) :args (@t427)) % 0.33/0.55 (step @p457 :rule nary_cong :premises (@p287 @p456) :args (@t428)) % 0.33/0.55 (step @p458 :rule cong :premises (@p457 @p454) :args (@t429)) % 0.33/0.55 (step @p459 :rule cong :premises (@p458) :args (@t430)) % 0.33/0.55 (step @p460 :rule trans :premises (@p459 @p453)) % 0.33/0.55 (step @p461 :rule arith_poly_norm :args ((= (* 1/1 (- tptp.f5 @t18)) (* 1/1 (- @t428 0/1))))) % 0.33/0.55 (step @p462 :rule arith_poly_norm_rel :premises (@p461) :args ((= @t431 @t429))) % 0.33/0.55 (step @p463 :rule cong :premises (@p462) :args ((not @t431))) % 0.33/0.55 (step @p464 :rule arith-elim-lt :args (tptp.f5 @t18)) % 0.33/0.55 (step @p465 :rule trans :premises (@p464 @p463)) % 0.33/0.55 (step @p466 :rule trans :premises (@p465 @p460)) % 0.33/0.55 (step @p467 :rule eq_resolve :premises (@p7 @p466)) % 0.33/0.55 (step @p468 :rule refl :args (@t432)) % 0.33/0.55 (step @p469 :rule bool-double-not-elim :args (@t418)) % 0.33/0.55 (step @p470 :rule nary_cong :premises (@p469 @p468) :args ((or (not @t433) @t432))) % 0.33/0.55 (step @p471 :rule bool-double-not-elim :args (@t432)) % 0.33/0.55 (step @p472 :rule bool-impl-false1 :args (@t434)) % 0.33/0.55 (step @p473 :rule trans :premises (@p472 @p471)) % 0.33/0.55 (step @p474 :rule refl :args (@t434)) % 0.33/0.55 (step @p475 :rule cong :premises (@p474 @p365) :args (@t435)) % 0.33/0.55 (step @p476 :rule trans :premises (@p475 @p473)) % 0.33/0.55 (step @p477 :rule refl :args (@t433)) % 0.33/0.55 (step @p478 :rule cong :premises (@p477 @p476) :args ((=> @t433 @t435))) % 0.33/0.55 (step @p479 :rule cong :premises (@p279) :args (@t5)) % 0.33/0.55 (step @p480 :rule cong :premises (@p474 @p479) :args (@t436)) % 0.33/0.55 (step @p481 :rule cong :premises (@p477 @p480) :args ((=> @t433 @t436))) % 0.33/0.55 (step @p482 :rule trans :premises (@p481 @p478)) % 0.33/0.55 (step @p483 :rule refl :args (@t5)) % 0.33/0.55 (step @p484 :rule cong :premises (@p453 @p483) :args (@t437)) % 0.33/0.55 (step @p485 :rule refl :args (0/1)) % 0.33/0.55 (step @p486 :rule arith_poly_norm :args ((= @t438 @t417))) % 0.33/0.55 (step @p487 :rule arith_poly_norm :args ((= @t439 @t438))) % 0.33/0.55 (step @p488 :rule trans :premises (@p487 @p486)) % 0.33/0.55 (step @p489 :rule cong :premises (@p488 @p485) :args (@t440)) % 0.33/0.55 (step @p490 :rule cong :premises (@p489) :args (@t441)) % 0.33/0.55 (step @p491 :rule cong :premises (@p490 @p484) :args ((=> @t441 @t437))) % 0.33/0.55 (step @p492 :rule cong :premises (@p459 @p483) :args (@t442)) % 0.33/0.55 (step @p493 :rule refl :args (0/1)) % 0.33/0.55 (step @p494 :rule refl :args (@t341)) % 0.33/0.55 (step @p495 :rule nary_cong :premises (@p494 @p346) :args (@t443)) % 0.33/0.55 (step @p496 :rule cong :premises (@p495 @p493) :args (@t444)) % 0.33/0.55 (step @p497 :rule cong :premises (@p496) :args (@t445)) % 0.33/0.55 (step @p498 :rule cong :premises (@p497 @p492) :args ((=> @t445 @t442))) % 0.33/0.55 (step @p499 :rule trans :premises (@p498 @p491)) % 0.33/0.55 (step @p500 :rule cong :premises (@p465 @p483) :args (@t20)) % 0.33/0.55 (step @p501 :rule arith_poly_norm :args ((= (* -1/1 (- tptp.f7 tptp.f5)) (* -1/1 (- @t443 0/1))))) % 0.33/0.55 (step @p502 :rule arith_poly_norm_rel :premises (@p501) :args ((= @t446 @t444))) % 0.33/0.55 (step @p503 :rule cong :premises (@p502) :args ((not @t446))) % 0.33/0.55 (step @p504 :rule arith-elim-lt :args (tptp.f7 tptp.f5)) % 0.33/0.55 (step @p505 :rule trans :premises (@p504 @p503)) % 0.33/0.55 (step @p506 :rule cong :premises (@p505 @p500) :args (@t21)) % 0.33/0.55 (step @p507 :rule trans :premises (@p506 @p499 @p482)) % 0.33/0.55 (step @p508 :rule eq_resolve :premises (@p5 @p507)) % 0.33/0.55 (step @p509 :rule implies_elim :premises (@p508)) % 0.33/0.55 (step @p510 :rule eq_resolve :premises (@p509 @p470)) % 0.33/0.55 (step @p511 :rule reordering :premises (@p510) :args ((or @t432 @t418))) % 0.33/0.55 (step @p512 :rule chain_m_resolution :premises (@p511 @p467) :args (@t418 @t412 (@list @t432))) % 0.33/0.55 (step @p513 :rule eq_resolve :premises (@p512 @p446)) % 0.33/0.55 (step @p514 false :rule contra :premises (@p513 @p442)) % 0.33/0.55 ) % 0.33/0.55 % SZS output end Proof % 0.33/0.55 % cvc5 exiting %------------------------------------------------------------------------------