%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : SWW824_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 : n029.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:42 AM UTC 2026 % Result : Unsatisfiable 0.45s 0.84s % Output : Proof 0.45s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SWW824_1 : TPTP v9.2.1. Released v7.0.0. % 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.15/0.33 % Computer : n029.cluster.edu % 0.15/0.33 % Model : x86_64 x86_64 % 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.33 % Memory : 8042.1875MB % 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.33 % CPULimit : 300 % 0.15/0.33 % WCLimit : 300 % 0.15/0.33 % DateTime : Tue Jun 2 22:33:02 EDT 2026 % 0.15/0.33 % CPUTime : % 0.37/0.63 %----Proving TF0_ARI % 0.37/0.65 --- Run --finite-model-find --decision=internal at 45... % 0.45/0.84 % SZS status Unsatisfiable % 0.45/0.84 % SZS output start Proof % 0.45/0.86 ( % 0.45/0.86 (declare-sort |tptp.'S21'| 0) % 0.45/0.86 (declare-sort |tptp.'S20'| 0) % 0.45/0.86 (declare-sort |tptp.'S19'| 0) % 0.45/0.86 (declare-sort |tptp.'S18'| 0) % 0.45/0.86 (declare-sort |tptp.'S16'| 0) % 0.45/0.86 (declare-sort |tptp.'S15'| 0) % 0.45/0.86 (declare-sort |tptp.'S14'| 0) % 0.45/0.86 (declare-sort |tptp.'S13'| 0) % 0.45/0.86 (declare-sort |tptp.'S12'| 0) % 0.45/0.86 (declare-sort |tptp.'S11'| 0) % 0.45/0.86 (declare-sort |tptp.'S8'| 0) % 0.45/0.86 (declare-sort |tptp.'S1'| 0) % 0.45/0.86 (declare-sort |tptp.'S17'| 0) % 0.45/0.86 (declare-sort |tptp.'S3'| 0) % 0.45/0.86 (declare-sort |tptp.'S5'| 0) % 0.45/0.86 (declare-sort |tptp.'S4'| 0) % 0.45/0.86 (declare-sort |tptp.'S2'| 0) % 0.45/0.86 (declare-sort |tptp.'S7'| 0) % 0.45/0.86 (declare-sort |tptp.'S9'| 0) % 0.45/0.86 (declare-sort |tptp.'S6'| 0) % 0.45/0.86 (declare-sort |tptp.'S10'| 0) % 0.45/0.86 (declare-const tptp.f46 |tptp.'S21'|) % 0.45/0.86 (declare-const tptp.f42 (-> |tptp.'S20'| Real |tptp.'S10'|)) % 0.45/0.86 (declare-const tptp.f43 |tptp.'S20'|) % 0.45/0.86 (declare-const tptp.f40 (-> |tptp.'S19'| |tptp.'S9'| |tptp.'S8'|)) % 0.45/0.86 (declare-const tptp.f41 |tptp.'S19'|) % 0.45/0.86 (declare-const tptp.f38 |tptp.'S18'|) % 0.45/0.86 (declare-const tptp.f37 (-> |tptp.'S18'| |tptp.'S5'| |tptp.'S17'|)) % 0.45/0.86 (declare-const tptp.f39 |tptp.'S18'|) % 0.45/0.86 (declare-const tptp.f36 (-> |tptp.'S17'| |tptp.'S5'| |tptp.'S5'|)) % 0.45/0.86 (declare-const tptp.f34 (-> |tptp.'S16'| Int |tptp.'S6'|)) % 0.45/0.86 (declare-const tptp.f35 |tptp.'S16'|) % 0.45/0.86 (declare-const tptp.f32 (-> |tptp.'S15'| Real |tptp.'S4'|)) % 0.45/0.86 (declare-const tptp.f33 |tptp.'S15'|) % 0.45/0.86 (declare-const tptp.f44 (-> |tptp.'S21'| |tptp.'S9'| Real)) % 0.45/0.86 (declare-const tptp.f31 |tptp.'S2'|) % 0.45/0.86 (declare-const tptp.f30 |tptp.'S13'|) % 0.45/0.86 (declare-const tptp.f45 |tptp.'S21'|) % 0.45/0.86 (declare-const tptp.f12 |tptp.'S6'|) % 0.45/0.86 (declare-const tptp.f13 (-> |tptp.'S7'| Int |tptp.'S5'|)) % 0.45/0.86 (declare-const tptp.f4 |tptp.'S2'|) % 0.45/0.86 (declare-const tptp.f27 (-> |tptp.'S13'| Int Int)) % 0.45/0.86 (declare-const tptp.f3 (-> |tptp.'S2'| Real Real)) % 0.45/0.86 (declare-const tptp.f6 |tptp.'S3'|) % 0.45/0.86 (declare-const tptp.f7 Real) % 0.45/0.86 (declare-const tptp.f8 (-> |tptp.'S4'| |tptp.'S5'| Real)) % 0.45/0.86 (declare-const tptp.f9 |tptp.'S4'|) % 0.45/0.86 (declare-const tptp.f25 |tptp.'S12'|) % 0.45/0.86 (declare-const tptp.f10 |tptp.'S5'|) % 0.45/0.86 (declare-const tptp.f5 (-> |tptp.'S3'| Real |tptp.'S2'|)) % 0.45/0.86 (declare-const tptp.f1 |tptp.'S1'|) % 0.45/0.86 (declare-const tptp.f14 |tptp.'S7'|) % 0.45/0.86 (declare-const tptp.f2 |tptp.'S1'|) % 0.45/0.86 (declare-const tptp.f11 (-> |tptp.'S6'| |tptp.'S5'| Int)) % 0.45/0.86 (declare-const tptp.f18 |tptp.'S10'|) % 0.45/0.86 (declare-const tptp.f22 (-> |tptp.'S11'| |tptp.'S9'| |tptp.'S9'|)) % 0.45/0.86 (declare-const tptp.f28 (-> |tptp.'S14'| Int |tptp.'S13'|)) % 0.45/0.86 (declare-const tptp.f19 |tptp.'S2'|) % 0.45/0.86 (declare-const tptp.f16 |tptp.'S8'|) % 0.45/0.86 (declare-const tptp.f20 |tptp.'S3'|) % 0.45/0.86 (declare-const tptp.f17 (-> |tptp.'S10'| Real |tptp.'S9'|)) % 0.45/0.86 (declare-const tptp.f26 (-> |tptp.'S5'| |tptp.'S1'|)) % 0.45/0.86 (declare-const tptp.f15 (-> |tptp.'S8'| |tptp.'S5'| |tptp.'S9'|)) % 0.45/0.86 (declare-const tptp.f21 |tptp.'S2'|) % 0.45/0.86 (declare-const tptp.f24 |tptp.'S12'|) % 0.45/0.86 (declare-const tptp.f23 (-> |tptp.'S12'| |tptp.'S9'| |tptp.'S11'|)) % 0.45/0.86 (declare-const tptp.f29 |tptp.'S14'|) % 0.45/0.86 (define @t1 () (* 2/1 tptp.f7)) % 0.45/0.86 (define @t2 () (tptp.f5 tptp.f6 @t1)) % 0.45/0.86 (define @t3 () (tptp.f3 tptp.f4 (tptp.f3 @t2 (tptp.f8 tptp.f9 tptp.f10)))) % 0.45/0.86 (define @t4 () (@var "A__questionmark_v_0_1" Real)) % 0.45/0.86 (define @t5 () (= @t4 1/1)) % 0.45/0.86 (define @t6 () (< @t4 0/1)) % 0.45/0.86 (define @t7 () (not @t6)) % 0.45/0.86 (define @t8 () (=> @t7 @t5)) % 0.45/0.86 (define @t9 () (- @t4)) % 0.45/0.86 (define @t10 () (= @t9 1/1)) % 0.45/0.86 (define @t11 () (=> @t6 @t10)) % 0.45/0.86 (define @t12 () (= @t4 @t3)) % 0.45/0.86 (define @t13 () (and @t12 @t11 @t8)) % 0.45/0.86 (define @t14 () (@list @t4)) % 0.45/0.86 (define @t15 () (exists @t14 @t13)) % 0.45/0.86 (define @t16 () (tptp.f5 tptp.f6 tptp.f7)) % 0.45/0.86 (define @t17 () (tptp.f3 @t16 2/1)) % 0.45/0.86 (define @t18 () (tptp.f3 (tptp.f5 tptp.f6 1/1) 2/1)) % 0.45/0.86 (define @t19 () (@var "A__questionmark_v0" Real)) % 0.45/0.86 (define @t20 () (tptp.f3 tptp.f4 @t19)) % 0.45/0.86 (define @t21 () (@var "A__questionmark_v_0_2" Real)) % 0.45/0.86 (define @t22 () (< @t19 @t17)) % 0.45/0.86 (define @t23 () (@list @t19)) % 0.45/0.86 (define @t24 () (@var "A__questionmark_v_0_3" Real)) % 0.45/0.86 (define @t25 () (@var "A__questionmark_v_0_4" Real)) % 0.45/0.86 (define @t26 () (@var "A__questionmark_v0" |tptp.'S5'|)) % 0.45/0.86 (define @t27 () (tptp.f8 tptp.f9 @t26)) % 0.45/0.86 (define @t28 () (@list @t26)) % 0.45/0.86 (define @t29 () (- 1/1)) % 0.45/0.86 (define @t30 () (+ @t19 tptp.f7)) % 0.45/0.86 (define @t31 () (+ @t19 @t1)) % 0.45/0.86 (define @t32 () (@var "A__questionmark_v1" Real)) % 0.45/0.86 (define @t33 () (tptp.f3 tptp.f4 @t32)) % 0.45/0.86 (define @t34 () (<= @t32 tptp.f7)) % 0.45/0.86 (define @t35 () (< @t19 @t32)) % 0.45/0.86 (define @t36 () (<= 0/1 @t19)) % 0.45/0.86 (define @t37 () (@list @t19 @t32)) % 0.45/0.86 (define @t38 () (<= @t19 @t32)) % 0.45/0.86 (define @t39 () (+ @t19 @t32)) % 0.45/0.86 (define @t40 () (tptp.f5 tptp.f6 @t39)) % 0.45/0.86 (define @t41 () (tptp.f3 @t40 2/1)) % 0.45/0.86 (define @t42 () (@var "A__questionmark_v_0_5" Real)) % 0.45/0.86 (define @t43 () (tptp.f5 tptp.f6 @t19)) % 0.45/0.86 (define @t44 () (tptp.f3 @t43 @t32)) % 0.45/0.86 (define @t45 () (@var "A__questionmark_v1" |tptp.'S5'|)) % 0.45/0.86 (define @t46 () (tptp.f8 tptp.f9 @t45)) % 0.45/0.86 (define @t47 () (@var "A__questionmark_v_1_7" Int)) % 0.45/0.86 (define @t48 () (@var "A__questionmark_v_0_6" Int)) % 0.45/0.86 (define @t49 () (tptp.f11 tptp.f12 @t26)) % 0.45/0.86 (define @t50 () (tptp.f11 tptp.f12 @t45)) % 0.45/0.86 (define @t51 () (@list @t26 @t45)) % 0.45/0.86 (define @t52 () (<= @t49 @t50)) % 0.45/0.86 (define @t53 () (< @t49 @t50)) % 0.45/0.86 (define @t54 () (tptp.f13 tptp.f14 0)) % 0.45/0.86 (define @t55 () (= @t26 @t54)) % 0.45/0.86 (define @t56 () (+ @t27 1/1)) % 0.45/0.86 (define @t57 () (< 0 @t49)) % 0.45/0.86 (define @t58 () (tptp.f13 tptp.f14 (+ @t49 @t50))) % 0.45/0.86 (define @t59 () (tptp.f13 tptp.f14 (+ @t49 1))) % 0.45/0.86 (define @t60 () (tptp.f8 tptp.f9 @t59)) % 0.45/0.86 (define @t61 () (@var "A__questionmark_v_0_8" Real)) % 0.45/0.86 (define @t62 () (< @t61 0/1)) % 0.45/0.86 (define @t63 () (+ 0 1)) % 0.45/0.86 (define @t64 () (tptp.f13 tptp.f14 @t63)) % 0.45/0.86 (define @t65 () (tptp.f13 tptp.f14 1)) % 0.45/0.86 (define @t66 () (@var "A__questionmark_v_0_9" Real)) % 0.45/0.86 (define @t67 () (< 0/1 @t19)) % 0.45/0.86 (define @t68 () (tptp.f3 tptp.f4 2/1)) % 0.45/0.86 (define @t69 () (- @t19)) % 0.45/0.86 (define @t70 () (@var "A__questionmark_v_0_10" Real)) % 0.45/0.86 (define @t71 () (< @t70 0/1)) % 0.45/0.86 (define @t72 () (@var "A__questionmark_v_0_11" Real)) % 0.45/0.86 (define @t73 () (@var "A__questionmark_v_0_12" Real)) % 0.45/0.86 (define @t74 () (- @t17)) % 0.45/0.86 (define @t75 () (@var "A__questionmark_v_0_13" Real)) % 0.45/0.86 (define @t76 () (<= @t32 0/1)) % 0.45/0.86 (define @t77 () (- tptp.f7)) % 0.45/0.86 (define @t78 () (<= @t77 @t19)) % 0.45/0.86 (define @t79 () (@var "A__questionmark_v2" Real)) % 0.45/0.86 (define @t80 () (= @t79 @t32)) % 0.45/0.86 (define @t81 () (@list @t79)) % 0.45/0.86 (define @t82 () (@list @t32)) % 0.45/0.86 (define @t83 () (<= @t19 1/1)) % 0.45/0.86 (define @t84 () (<= @t29 @t19)) % 0.45/0.86 (define @t85 () (@var "A__questionmark_v_0_14" Real)) % 0.45/0.86 (define @t86 () (@var "A__questionmark_v_0_15" Real)) % 0.45/0.86 (define @t87 () (- @t19 @t32)) % 0.45/0.86 (define @t88 () (@var "A__questionmark_v_0_16" Real)) % 0.45/0.86 (define @t89 () (@var "A__questionmark_v_0_17" Real)) % 0.45/0.86 (define @t90 () (@var "A__questionmark_v_1_19" |tptp.'S2'|)) % 0.45/0.86 (define @t91 () (@var "A__questionmark_v_0_18" Real)) % 0.45/0.86 (define @t92 () (tptp.f5 tptp.f6 @t32)) % 0.45/0.86 (define @t93 () (@list @t19 @t32 @t79)) % 0.45/0.86 (define @t94 () (tptp.f3 tptp.f19 @t32)) % 0.45/0.86 (define @t95 () (tptp.f3 tptp.f19 @t19)) % 0.45/0.86 (define @t96 () (tptp.f3 (tptp.f5 tptp.f20 (* 2/1 @t27)) tptp.f7)) % 0.45/0.86 (define @t97 () (tptp.f3 (tptp.f5 tptp.f20 (tptp.f3 (tptp.f5 tptp.f6 3/1) 2/1)) tptp.f7)) % 0.45/0.86 (define @t98 () (@var "A__questionmark_v_1_20" Real)) % 0.45/0.86 (define @t99 () (@var "A__questionmark_v_0_21" Real)) % 0.45/0.86 (define @t100 () (tptp.f3 tptp.f21 @t19)) % 0.45/0.86 (define @t101 () (tptp.f5 tptp.f20 @t32)) % 0.45/0.86 (define @t102 () (tptp.f3 @t101 @t32)) % 0.45/0.86 (define @t103 () (tptp.f5 tptp.f20 @t19)) % 0.45/0.86 (define @t104 () (tptp.f3 @t103 @t19)) % 0.45/0.86 (define @t105 () (tptp.f3 @t101 @t19)) % 0.45/0.86 (define @t106 () (tptp.f3 @t103 @t32)) % 0.45/0.86 (define @t107 () (tptp.f3 @t101 @t79)) % 0.45/0.86 (define @t108 () (@var "A__questionmark_v_0_22" |tptp.'S2'|)) % 0.45/0.86 (define @t109 () (tptp.f3 @t103 @t79)) % 0.45/0.86 (define @t110 () (@var "A__questionmark_v_0_23" Real)) % 0.45/0.86 (define @t111 () (= @t32 @t79)) % 0.45/0.86 (define @t112 () (tptp.f5 tptp.f20 @t79)) % 0.45/0.86 (define @t113 () (tptp.f3 @t112 @t19)) % 0.45/0.86 (define @t114 () (not (= @t19 0/1))) % 0.45/0.86 (define @t115 () (@var "A__questionmark_v_0_24" |tptp.'S2'|)) % 0.45/0.86 (define @t116 () (< @t32 @t79)) % 0.45/0.86 (define @t117 () (<= @t32 @t79)) % 0.45/0.86 (define @t118 () (@var "A__questionmark_v_0_25" |tptp.'S2'|)) % 0.45/0.86 (define @t119 () (@var "A__questionmark_v_0_26" Real)) % 0.45/0.86 (define @t120 () (@var "A__questionmark_v_0_27" |tptp.'S2'|)) % 0.45/0.86 (define @t121 () (@var "A__questionmark_v3" Real)) % 0.45/0.86 (define @t122 () (tptp.f3 @t101 @t121)) % 0.45/0.86 (define @t123 () (@list @t19 @t32 @t79 @t121)) % 0.45/0.86 (define @t124 () (@var "A__questionmark_v3" |tptp.'S9'|)) % 0.45/0.86 (define @t125 () (@var "A__questionmark_v1" |tptp.'S9'|)) % 0.45/0.86 (define @t126 () (tptp.f23 tptp.f24 @t125)) % 0.45/0.86 (define @t127 () (tptp.f22 @t126 @t124)) % 0.45/0.86 (define @t128 () (@var "A__questionmark_v2" |tptp.'S9'|)) % 0.45/0.86 (define @t129 () (@var "A__questionmark_v0" |tptp.'S9'|)) % 0.45/0.86 (define @t130 () (tptp.f23 tptp.f24 @t129)) % 0.45/0.86 (define @t131 () (tptp.f22 (tptp.f23 tptp.f25 @t129) @t125)) % 0.45/0.86 (define @t132 () (@list @t129 @t125 @t128 @t124)) % 0.45/0.86 (define @t133 () (@var "A__questionmark_v_2_30" |tptp.'S2'|)) % 0.45/0.86 (define @t134 () (@var "A__questionmark_v_1_29" Real)) % 0.45/0.86 (define @t135 () (@var "A__questionmark_v_0_28" Real)) % 0.45/0.86 (define @t136 () (@var "A__questionmark_v0" |tptp.'S2'|)) % 0.45/0.86 (define @t137 () (@var "A__questionmark_v_1_31" Real)) % 0.45/0.86 (define @t138 () (@var "A__questionmark_v_0_32" Real)) % 0.45/0.86 (define @t139 () (@var "A__questionmark_v2" |tptp.'S5'|)) % 0.45/0.86 (define @t140 () (tptp.f5 tptp.f20 (tptp.f8 tptp.f9 @t139))) % 0.45/0.86 (define @t141 () (tptp.f3 @t140 @t19)) % 0.45/0.86 (define @t142 () (@list @t139)) % 0.45/0.86 (define @t143 () (tptp.f11 tptp.f12 @t139)) % 0.45/0.86 (define @t144 () (@var "A__questionmark_v_0_33" Real)) % 0.45/0.86 (define @t145 () (@var "A__questionmark_v_0_34" |tptp.'S2'|)) % 0.45/0.86 (define @t146 () (@var "A__questionmark_v_0_35" |tptp.'S2'|)) % 0.45/0.86 (define @t147 () (@var "A__questionmark_v_0_36" |tptp.'S11'|)) % 0.45/0.86 (define @t148 () (@list @t129 @t125 @t128)) % 0.45/0.86 (define @t149 () (* 2 @t49)) % 0.45/0.86 (define @t150 () (tptp.f8 tptp.f9 (tptp.f13 tptp.f14 (+ @t149 1)))) % 0.45/0.86 (define @t151 () (tptp.f5 tptp.f20 tptp.f7)) % 0.45/0.86 (define @t152 () (tptp.f5 tptp.f20 @t46)) % 0.45/0.86 (define @t153 () (tptp.f3 @t152 @t17)) % 0.45/0.86 (define @t154 () (= @t19 (- @t153))) % 0.45/0.86 (define @t155 () (= (tptp.f26 @t45) tptp.f1)) % 0.45/0.86 (define @t156 () (not @t155)) % 0.45/0.86 (define @t157 () (@list @t45)) % 0.45/0.86 (define @t158 () (= @t19 @t153)) % 0.45/0.86 (define @t159 () (exists @t157 (and @t156 @t158))) % 0.45/0.86 (define @t160 () (* 4 @t49)) % 0.45/0.86 (define @t161 () (tptp.f5 tptp.f20 @t27)) % 0.45/0.86 (define @t162 () (tptp.f28 tptp.f29 @t49)) % 0.45/0.86 (define @t163 () (tptp.f13 tptp.f14 (tptp.f27 @t162 @t50))) % 0.45/0.86 (define @t164 () (@var "A__questionmark_v1" Int)) % 0.45/0.86 (define @t165 () (tptp.f27 tptp.f30 @t164)) % 0.45/0.86 (define @t166 () (@var "A__questionmark_v0" Int)) % 0.45/0.86 (define @t167 () (tptp.f27 tptp.f30 @t166)) % 0.45/0.86 (define @t168 () (tptp.f28 tptp.f29 @t166)) % 0.45/0.86 (define @t169 () (tptp.f27 @t168 @t164)) % 0.45/0.86 (define @t170 () (@list @t166 @t164)) % 0.45/0.86 (define @t171 () (@var "A__questionmark_v_0_37" Real)) % 0.45/0.86 (define @t172 () (tptp.f27 @t168 @t166)) % 0.45/0.86 (define @t173 () (@var "A__questionmark_v_0_38" Int)) % 0.45/0.86 (define @t174 () (@list @t166)) % 0.45/0.86 (define @t175 () (@var "A__questionmark_v_0_39" Real)) % 0.45/0.86 (define @t176 () (@var "A__questionmark_v_0_40" Real)) % 0.45/0.86 (define @t177 () (tptp.f3 @t161 @t32)) % 0.45/0.86 (define @t178 () (tptp.f17 tptp.f18 @t32)) % 0.45/0.86 (define @t179 () (@list @t26 @t32)) % 0.45/0.86 (define @t180 () (= (tptp.f26 @t26) tptp.f1)) % 0.45/0.86 (define @t181 () (* 2 @t50)) % 0.45/0.86 (define @t182 () (tptp.f13 tptp.f14 (+ @t181 1))) % 0.45/0.86 (define @t183 () (not @t180)) % 0.45/0.86 (define @t184 () (tptp.f27 (tptp.f28 tptp.f29 (+ @t63 1)) @t50)) % 0.45/0.86 (define @t185 () (@var "A__questionmark_v_0_41" Int)) % 0.45/0.86 (define @t186 () (and @t183 @t156)) % 0.45/0.86 (define @t187 () (and @t180 @t155)) % 0.45/0.86 (define @t188 () (= (tptp.f26 @t58) tptp.f1)) % 0.45/0.86 (define @t189 () (@var "A__questionmark_v_1_44" Int)) % 0.45/0.86 (define @t190 () (@var "A__questionmark_v_0_45" Int)) % 0.45/0.86 (define @t191 () (tptp.f17 tptp.f18 @t19)) % 0.45/0.86 (define @t192 () (tptp.f13 tptp.f14 @t181)) % 0.45/0.86 (define @t193 () (exists @t157 (and @t155 @t158))) % 0.45/0.86 (define @t194 () (tptp.f3 tptp.f31 @t19)) % 0.45/0.86 (define @t195 () (= @t194 0/1)) % 0.45/0.86 (define @t196 () (< @t19 @t46)) % 0.45/0.86 (define @t197 () (tptp.f13 tptp.f14 (+ @t50 1))) % 0.45/0.86 (define @t198 () (tptp.f8 tptp.f9 @t197)) % 0.45/0.86 (define @t199 () (tptp.f13 tptp.f14 (- @t50 1))) % 0.45/0.86 (define @t200 () (tptp.f8 (tptp.f32 tptp.f33 @t29) @t26)) % 0.45/0.86 (define @t201 () (tptp.f3 @t151 @t27)) % 0.45/0.86 (define @t202 () (@var "A__questionmark_v_1_49" |tptp.'S5'|)) % 0.45/0.86 (define @t203 () (tptp.f32 tptp.f33 @t19)) % 0.45/0.86 (define @t204 () (tptp.f3 tptp.f31 @t32)) % 0.45/0.86 (define @t205 () (@var "A__questionmark_v_0_48" |tptp.'S2'|)) % 0.45/0.86 (define @t206 () (tptp.f13 tptp.f14 2)) % 0.45/0.86 (define @t207 () (* 2/1 @t19)) % 0.45/0.86 (define @t208 () (@var "A__questionmark_v_0_50" |tptp.'S5'|)) % 0.45/0.86 (define @t209 () (tptp.f32 tptp.f33 @t32)) % 0.45/0.86 (define @t210 () (tptp.f34 tptp.f35 @t164)) % 0.45/0.86 (define @t211 () (@list @t26 @t164)) % 0.45/0.86 (define @t212 () (@var "A__questionmark_v_5_51" |tptp.'S5'|)) % 0.45/0.86 (define @t213 () (@var "A__questionmark_v_4_55" Real)) % 0.45/0.86 (define @t214 () (@var "A__questionmark_v_3_52" |tptp.'S2'|)) % 0.45/0.86 (define @t215 () (@var "A__questionmark_v_2_53" Real)) % 0.45/0.86 (define @t216 () (@var "A__questionmark_v_1_54" |tptp.'S2'|)) % 0.45/0.86 (define @t217 () (@var "A__questionmark_v_0_56" Real)) % 0.45/0.86 (define @t218 () (tptp.f5 tptp.f20 @t20)) % 0.45/0.86 (define @t219 () (tptp.f5 tptp.f20 @t194)) % 0.45/0.86 (define @t220 () (@var "A__questionmark_v2" Int)) % 0.45/0.86 (define @t221 () (@var "A__questionmark_v_1_58" Int)) % 0.45/0.86 (define @t222 () (@var "A__questionmark_v_0_57" Int)) % 0.45/0.86 (define @t223 () (@var "A__questionmark_v_2_59" |tptp.'S6'|)) % 0.45/0.86 (define @t224 () (@var "A__questionmark_v_1_61" Int)) % 0.45/0.86 (define @t225 () (@var "A__questionmark_v_0_60" Int)) % 0.45/0.86 (define @t226 () (@var "A__questionmark_v_2_62" |tptp.'S4'|)) % 0.45/0.86 (define @t227 () (@var "A__questionmark_v_1_64" Int)) % 0.45/0.86 (define @t228 () (@var "A__questionmark_v_0_63" Int)) % 0.45/0.86 (define @t229 () (@var "A__questionmark_v_2_65" |tptp.'S17'|)) % 0.45/0.86 (define @t230 () (@list @t26 @t45 @t139)) % 0.45/0.86 (define @t231 () (@var "A__questionmark_v_1_67" Int)) % 0.45/0.86 (define @t232 () (@var "A__questionmark_v_0_66" Int)) % 0.45/0.86 (define @t233 () (@var "A__questionmark_v_2_68" |tptp.'S8'|)) % 0.45/0.86 (define @t234 () (@var "A__questionmark_v_1_70" |tptp.'S6'|)) % 0.45/0.86 (define @t235 () (@var "A__questionmark_v_0_69" Int)) % 0.45/0.86 (define @t236 () (@var "A__questionmark_v_1_72" |tptp.'S4'|)) % 0.45/0.86 (define @t237 () (@var "A__questionmark_v_0_71" Int)) % 0.45/0.86 (define @t238 () (@var "A__questionmark_v_1_74" |tptp.'S17'|)) % 0.45/0.86 (define @t239 () (@var "A__questionmark_v_0_73" Int)) % 0.45/0.86 (define @t240 () (tptp.f37 tptp.f38 @t45)) % 0.45/0.86 (define @t241 () (@var "A__questionmark_v_1_76" |tptp.'S8'|)) % 0.45/0.86 (define @t242 () (@var "A__questionmark_v_0_75" Int)) % 0.45/0.86 (define @t243 () (tptp.f40 tptp.f41 @t125)) % 0.45/0.86 (define @t244 () (= @t20 1/1)) % 0.45/0.86 (define @t245 () (@var "A__questionmark_v_1_78" Real)) % 0.45/0.86 (define @t246 () (@var "A__questionmark_v_0_77" Real)) % 0.45/0.86 (define @t247 () (< @t245 @t246)) % 0.45/0.86 (define @t248 () (- @t194)) % 0.45/0.86 (define @t249 () (@var "A__questionmark_v_0_79" Real)) % 0.45/0.86 (define @t250 () (@var "A__questionmark_v_0_80" Real)) % 0.45/0.86 (define @t251 () (tptp.f8 (tptp.f32 tptp.f33 2/1) @t26)) % 0.45/0.86 (define @t252 () (@var "A__questionmark_v_1_81" |tptp.'S5'|)) % 0.45/0.86 (define @t253 () (@var "A__questionmark_v_0_82" Real)) % 0.45/0.86 (define @t254 () (@var "A__questionmark_v_0_83" |tptp.'S5'|)) % 0.45/0.86 (define @t255 () (tptp.f32 tptp.f33 @t20)) % 0.45/0.86 (define @t256 () (tptp.f32 tptp.f33 @t194)) % 0.45/0.86 (define @t257 () (@var "A__questionmark_v_0_84" |tptp.'S5'|)) % 0.45/0.86 (define @t258 () (@var "A__questionmark_v_0_85" |tptp.'S5'|)) % 0.45/0.86 (define @t259 () (@var "A__questionmark_v_0_86" |tptp.'S5'|)) % 0.45/0.86 (define @t260 () (@var "A__questionmark_v_0_87" |tptp.'S5'|)) % 0.45/0.86 (define @t261 () (@var "A__questionmark_v_0_88" Real)) % 0.45/0.86 (define @t262 () (tptp.f8 @t203 @t206)) % 0.45/0.86 (define @t263 () (< @t19 0/1)) % 0.45/0.86 (define @t264 () (@var "A__questionmark_v_0_89" Real)) % 0.45/0.86 (define @t265 () (@var "A__questionmark_v_1_90" Real)) % 0.45/0.86 (define @t266 () (@var "A__questionmark_v_0_91" |tptp.'S5'|)) % 0.45/0.86 (define @t267 () (@var "A__questionmark_v_0_92" |tptp.'S5'|)) % 0.45/0.86 (define @t268 () (@var "A__questionmark_v_0_93" Real)) % 0.45/0.86 (define @t269 () (< @t268 0/1)) % 0.45/0.86 (define @t270 () (@var "A__questionmark_v_0_94" Real)) % 0.45/0.86 (define @t271 () (@var "A__questionmark_v_0_95" |tptp.'S5'|)) % 0.45/0.86 (define @t272 () (tptp.f3 @t219 @t204)) % 0.45/0.86 (define @t273 () (tptp.f3 @t218 @t33)) % 0.45/0.86 (define @t274 () (tptp.f3 tptp.f4 @t87)) % 0.45/0.86 (define @t275 () (tptp.f5 tptp.f20 @t204)) % 0.45/0.86 (define @t276 () (tptp.f5 tptp.f20 @t33)) % 0.45/0.86 (define @t277 () (tptp.f3 @t218 @t204)) % 0.45/0.86 (define @t278 () (tptp.f3 @t219 @t33)) % 0.45/0.86 (define @t279 () (tptp.f3 tptp.f31 @t87)) % 0.45/0.86 (define @t280 () (@var "A__questionmark_v_0_96" Real)) % 0.45/0.86 (define @t281 () (@var "A__questionmark_v_1_98" Real)) % 0.45/0.86 (define @t282 () (@var "A__questionmark_v_0_97" Real)) % 0.45/0.86 (define @t283 () (@var "A__questionmark_v_0_99" Real)) % 0.45/0.86 (define @t284 () (@var "A__questionmark_v_0_100" Real)) % 0.45/0.86 (define @t285 () (@var "A__questionmark_v_0_101" Real)) % 0.45/0.86 (define @t286 () (@var "A__questionmark_v_0_102" Real)) % 0.45/0.86 (define @t287 () (tptp.f3 @t161 tptp.f7)) % 0.45/0.86 (define @t288 () (- @t17 @t19)) % 0.45/0.86 (define @t289 () (@var "A__questionmark_v_0_103" Real)) % 0.45/0.86 (define @t290 () (@var "A__questionmark_v_0_105" Real)) % 0.45/0.86 (define @t291 () (@var "A__questionmark_v_1_104" Real)) % 0.45/0.86 (define @t292 () (@var "A__questionmark_v_0_106" Real)) % 0.45/0.86 (define @t293 () (@var "A__questionmark_v_0_107" Real)) % 0.45/0.86 (define @t294 () (@var "A__questionmark_v_0_108" Real)) % 0.45/0.86 (define @t295 () (tptp.f5 tptp.f6 (tptp.f3 @t152 tptp.f7))) % 0.45/0.86 (define @t296 () (tptp.f5 tptp.f6 (tptp.f3 (tptp.f5 tptp.f20 @t198) tptp.f7))) % 0.45/0.86 (define @t297 () (@list @t19 @t45)) % 0.45/0.86 (define @t298 () (@var "A__questionmark_v_0_109" Real)) % 0.45/0.86 (define @t299 () (@var "A__questionmark_v_0_110" Real)) % 0.45/0.86 (define @t300 () (- @t299)) % 0.45/0.86 (define @t301 () (tptp.f37 tptp.f38 @t26)) % 0.45/0.86 (define @t302 () (tptp.f36 @t301 @t45)) % 0.45/0.86 (define @t303 () (tptp.f8 (tptp.f32 tptp.f33 @t27) @t45)) % 0.45/0.86 (define @t304 () (tptp.f8 tptp.f9 @t302)) % 0.45/0.86 (define @t305 () (tptp.f3 @t152 @t19)) % 0.45/0.86 (define @t306 () (@var "A__questionmark_v_0_111" Int)) % 0.45/0.86 (define @t307 () (not @t55)) % 0.45/0.86 (define @t308 () (@var "A__questionmark_v_0_112" Int)) % 0.45/0.86 (define @t309 () (@var "A__questionmark_v_0_113" Int)) % 0.45/0.86 (define @t310 () (@var "A__questionmark_v_0_114" Real)) % 0.45/0.86 (define @t311 () (@var "A__questionmark_v_0_115" |tptp.'S6'|)) % 0.45/0.86 (define @t312 () (tptp.f34 tptp.f35 @t166)) % 0.45/0.86 (define @t313 () (@list @t166 @t45)) % 0.45/0.86 (define @t314 () (@var "A__questionmark_v_0_116" |tptp.'S4'|)) % 0.45/0.86 (define @t315 () (@var "A__questionmark_v_0_117" |tptp.'S17'|)) % 0.45/0.86 (define @t316 () (tptp.f37 tptp.f39 @t26)) % 0.45/0.86 (define @t317 () (@var "A__questionmark_v_0_118" |tptp.'S8'|)) % 0.45/0.86 (define @t318 () (tptp.f40 tptp.f41 @t129)) % 0.45/0.86 (define @t319 () (@list @t129 @t45)) % 0.45/0.86 (define @t320 () (= @t45 @t54)) % 0.45/0.86 (define @t321 () (tptp.f11 tptp.f12 @t302)) % 0.45/0.86 (define @t322 () (< 0 @t321)) % 0.45/0.86 (define @t323 () (@var "A__questionmark_v_0_119" Int)) % 0.45/0.86 (define @t324 () (tptp.f11 @t312 @t206)) % 0.45/0.86 (define @t325 () (@var "A__questionmark_v_0_120" Real)) % 0.45/0.86 (define @t326 () (@var "A__questionmark_v_0_121" |tptp.'S5'|)) % 0.45/0.86 (define @t327 () (tptp.f34 tptp.f35 @t167)) % 0.45/0.86 (define @t328 () (@var "A__questionmark_v_0_122" |tptp.'S5'|)) % 0.45/0.86 (define @t329 () (tptp.f32 tptp.f33 @t95)) % 0.45/0.86 (define @t330 () (@var "A__questionmark_v_0_123" Int)) % 0.45/0.86 (define @t331 () (@var "A__questionmark_v_0_124" Int)) % 0.45/0.86 (define @t332 () (@var "A__questionmark_v_1_127" Int)) % 0.45/0.86 (define @t333 () (@var "A__questionmark_v_2_126" Int)) % 0.45/0.86 (define @t334 () (tptp.f13 tptp.f14 (tptp.f27 (tptp.f28 tptp.f29 @t333) @t332))) % 0.45/0.86 (define @t335 () (@var "A__questionmark_v_0_125" |tptp.'S5'|)) % 0.45/0.86 (define @t336 () (= @t26 @t335)) % 0.45/0.86 (define @t337 () (@var "A__questionmark_v_0_128" |tptp.'S17'|)) % 0.45/0.86 (define @t338 () (tptp.f36 @t337 @t45)) % 0.45/0.86 (define @t339 () (tptp.f13 tptp.f14 3)) % 0.45/0.86 (define @t340 () (tptp.f36 @t316 @t26)) % 0.45/0.86 (define @t341 () (tptp.f22 @t130 @t129)) % 0.45/0.86 (define @t342 () (@list @t129)) % 0.45/0.86 (define @t343 () (tptp.f36 @t301 @t206)) % 0.45/0.86 (define @t344 () (tptp.f15 @t318 @t206)) % 0.45/0.86 (define @t345 () (@var "A__questionmark_v_0_129" |tptp.'S6'|)) % 0.45/0.86 (define @t346 () (@var "A__questionmark_v_0_130" |tptp.'S4'|)) % 0.45/0.86 (define @t347 () (@var "A__questionmark_v_0_131" |tptp.'S17'|)) % 0.45/0.86 (define @t348 () (@var "A__questionmark_v_0_132" |tptp.'S8'|)) % 0.45/0.86 (define @t349 () (@var "A__questionmark_v_1_134" Int)) % 0.45/0.86 (define @t350 () (@var "A__questionmark_v_0_133" |tptp.'S6'|)) % 0.45/0.86 (define @t351 () (@var "A__questionmark_v_1_136" Real)) % 0.45/0.86 (define @t352 () (@var "A__questionmark_v_0_135" |tptp.'S4'|)) % 0.45/0.86 (define @t353 () (@var "A__questionmark_v_1_138" |tptp.'S5'|)) % 0.45/0.86 (define @t354 () (@var "A__questionmark_v_0_137" |tptp.'S17'|)) % 0.45/0.86 (define @t355 () (@var "A__questionmark_v_1_140" |tptp.'S9'|)) % 0.45/0.86 (define @t356 () (@var "A__questionmark_v_0_139" |tptp.'S8'|)) % 0.45/0.86 (define @t357 () (@var "A__questionmark_v_1_142" Int)) % 0.45/0.86 (define @t358 () (@var "A__questionmark_v_0_141" |tptp.'S6'|)) % 0.45/0.86 (define @t359 () (@var "A__questionmark_v_1_144" Real)) % 0.45/0.86 (define @t360 () (@var "A__questionmark_v_0_143" |tptp.'S4'|)) % 0.45/0.86 (define @t361 () (@var "A__questionmark_v_1_146" |tptp.'S5'|)) % 0.45/0.86 (define @t362 () (@var "A__questionmark_v_0_145" |tptp.'S17'|)) % 0.45/0.86 (define @t363 () (@var "A__questionmark_v_1_148" |tptp.'S9'|)) % 0.45/0.86 (define @t364 () (@var "A__questionmark_v_0_147" |tptp.'S8'|)) % 0.45/0.86 (define @t365 () (@var "A__questionmark_v3" |tptp.'S5'|)) % 0.45/0.86 (define @t366 () (tptp.f37 tptp.f39 @t45)) % 0.45/0.86 (define @t367 () (@var "A__questionmark_v_0_149" |tptp.'S17'|)) % 0.45/0.86 (define @t368 () (tptp.f37 tptp.f39 @t139)) % 0.45/0.86 (define @t369 () (tptp.f36 @t368 @t365)) % 0.45/0.86 (define @t370 () (@list @t26 @t45 @t139 @t365)) % 0.45/0.86 (define @t371 () (@var "A__questionmark_v_0_150" |tptp.'S2'|)) % 0.45/0.86 (define @t372 () (tptp.f3 @t112 @t121)) % 0.45/0.86 (define @t373 () (@var "A__questionmark_v3" Int)) % 0.45/0.86 (define @t374 () (tptp.f28 tptp.f29 @t164)) % 0.45/0.86 (define @t375 () (@var "A__questionmark_v_0_151" |tptp.'S13'|)) % 0.45/0.86 (define @t376 () (tptp.f28 tptp.f29 @t220)) % 0.45/0.86 (define @t377 () (tptp.f27 @t376 @t373)) % 0.45/0.86 (define @t378 () (@list @t166 @t164 @t220 @t373)) % 0.45/0.86 (define @t379 () (@var "A__questionmark_v_0_152" |tptp.'S11'|)) % 0.45/0.86 (define @t380 () (tptp.f23 tptp.f24 @t128)) % 0.45/0.86 (define @t381 () (tptp.f22 @t380 @t124)) % 0.45/0.86 (define @t382 () (@var "A__questionmark_v_1_153" |tptp.'S17'|)) % 0.45/0.86 (define @t383 () (@var "A__questionmark_v_0_154" |tptp.'S17'|)) % 0.45/0.86 (define @t384 () (tptp.f36 @t316 @t45)) % 0.45/0.86 (define @t385 () (@var "A__questionmark_v_1_155" |tptp.'S2'|)) % 0.45/0.86 (define @t386 () (@var "A__questionmark_v_0_156" |tptp.'S2'|)) % 0.45/0.86 (define @t387 () (@var "A__questionmark_v_1_157" |tptp.'S13'|)) % 0.45/0.86 (define @t388 () (@var "A__questionmark_v_0_158" |tptp.'S13'|)) % 0.45/0.86 (define @t389 () (@var "A__questionmark_v_1_159" |tptp.'S11'|)) % 0.45/0.86 (define @t390 () (@var "A__questionmark_v_0_160" |tptp.'S11'|)) % 0.45/0.86 (define @t391 () (tptp.f22 @t130 @t125)) % 0.45/0.86 (define @t392 () (@var "A__questionmark_v_1_162" |tptp.'S5'|)) % 0.45/0.86 (define @t393 () (@var "A__questionmark_v_0_161" |tptp.'S17'|)) % 0.45/0.86 (define @t394 () (@var "A__questionmark_v_1_164" Real)) % 0.45/0.86 (define @t395 () (@var "A__questionmark_v_0_163" |tptp.'S2'|)) % 0.45/0.86 (define @t396 () (@var "A__questionmark_v_1_166" Int)) % 0.45/0.86 (define @t397 () (@var "A__questionmark_v_0_165" |tptp.'S13'|)) % 0.45/0.86 (define @t398 () (@var "A__questionmark_v_1_168" |tptp.'S9'|)) % 0.45/0.86 (define @t399 () (@var "A__questionmark_v_0_167" |tptp.'S11'|)) % 0.45/0.86 (define @t400 () (@var "A__questionmark_v_0_169" |tptp.'S17'|)) % 0.45/0.86 (define @t401 () (@var "A__questionmark_v_0_170" |tptp.'S2'|)) % 0.45/0.86 (define @t402 () (@var "A__questionmark_v_0_171" |tptp.'S13'|)) % 0.45/0.86 (define @t403 () (@list @t166 @t164 @t220)) % 0.45/0.86 (define @t404 () (@var "A__questionmark_v_0_172" |tptp.'S11'|)) % 0.45/0.86 (define @t405 () (tptp.f36 @t366 @t139)) % 0.45/0.86 (define @t406 () (@var "A__questionmark_v_0_173" |tptp.'S17'|)) % 0.45/0.86 (define @t407 () (@var "A__questionmark_v_0_174" |tptp.'S2'|)) % 0.45/0.86 (define @t408 () (tptp.f27 @t374 @t220)) % 0.45/0.86 (define @t409 () (@var "A__questionmark_v_0_175" |tptp.'S13'|)) % 0.45/0.86 (define @t410 () (tptp.f22 @t126 @t128)) % 0.45/0.86 (define @t411 () (@var "A__questionmark_v_0_176" |tptp.'S11'|)) % 0.45/0.86 (define @t412 () (@var "A__questionmark_v_0_177" |tptp.'S17'|)) % 0.45/0.86 (define @t413 () (@var "A__questionmark_v_0_178" |tptp.'S2'|)) % 0.45/0.86 (define @t414 () (@var "A__questionmark_v_0_179" |tptp.'S13'|)) % 0.45/0.86 (define @t415 () (@var "A__questionmark_v_0_180" |tptp.'S11'|)) % 0.45/0.86 (define @t416 () (@var "A__questionmark_v_1_181" |tptp.'S17'|)) % 0.45/0.86 (define @t417 () (@var "A__questionmark_v_0_182" |tptp.'S17'|)) % 0.45/0.86 (define @t418 () (@var "A__questionmark_v_1_183" |tptp.'S2'|)) % 0.45/0.86 (define @t419 () (@var "A__questionmark_v_0_184" |tptp.'S2'|)) % 0.45/0.86 (define @t420 () (@var "A__questionmark_v_1_185" |tptp.'S13'|)) % 0.45/0.86 (define @t421 () (@var "A__questionmark_v_0_186" |tptp.'S13'|)) % 0.45/0.86 (define @t422 () (@var "A__questionmark_v_1_187" |tptp.'S11'|)) % 0.45/0.86 (define @t423 () (@var "A__questionmark_v_0_188" |tptp.'S11'|)) % 0.45/0.86 (define @t424 () (@list @t129 @t125)) % 0.45/0.86 (define @t425 () (@var "A__questionmark_v_0_189" |tptp.'S6'|)) % 0.45/0.86 (define @t426 () (@var "A__questionmark_v_0_190" |tptp.'S4'|)) % 0.45/0.86 (define @t427 () (@var "A__questionmark_v_0_191" |tptp.'S17'|)) % 0.45/0.86 (define @t428 () (@var "A__questionmark_v_0_192" |tptp.'S8'|)) % 0.45/0.86 (define @t429 () (@var "A__questionmark_v_0_193" |tptp.'S6'|)) % 0.45/0.86 (define @t430 () (@var "A__questionmark_v_0_194" |tptp.'S4'|)) % 0.45/0.86 (define @t431 () (@var "A__questionmark_v_0_195" |tptp.'S17'|)) % 0.45/0.86 (define @t432 () (@var "A__questionmark_v_0_196" |tptp.'S8'|)) % 0.45/0.86 (define @t433 () (@var "A__questionmark_v_0_197" |tptp.'S6'|)) % 0.45/0.86 (define @t434 () (@var "A__questionmark_v_0_198" |tptp.'S4'|)) % 0.45/0.86 (define @t435 () (@var "A__questionmark_v_0_199" |tptp.'S17'|)) % 0.45/0.86 (define @t436 () (@var "A__questionmark_v_0_200" |tptp.'S8'|)) % 0.45/0.86 (define @t437 () (tptp.f8 @t209 @t139)) % 0.45/0.86 (define @t438 () (tptp.f8 @t203 @t139)) % 0.45/0.86 (define @t439 () (@list @t19 @t32 @t139)) % 0.45/0.86 (define @t440 () (tptp.f15 @t243 @t139)) % 0.45/0.86 (define @t441 () (tptp.f15 @t318 @t139)) % 0.45/0.86 (define @t442 () (@list @t129 @t125 @t139)) % 0.45/0.86 (define @t443 () (tptp.f13 tptp.f14 (+ @t50 @t143))) % 0.45/0.86 (define @t444 () (@var "A__questionmark_v_0_201" |tptp.'S6'|)) % 0.45/0.86 (define @t445 () (@list @t166 @t45 @t139)) % 0.45/0.86 (define @t446 () (@var "A__questionmark_v_0_202" |tptp.'S4'|)) % 0.45/0.86 (define @t447 () (@list @t19 @t45 @t139)) % 0.45/0.86 (define @t448 () (@var "A__questionmark_v_0_203" |tptp.'S17'|)) % 0.45/0.86 (define @t449 () (@var "A__questionmark_v_0_204" |tptp.'S8'|)) % 0.45/0.86 (define @t450 () (@list @t129 @t45 @t139)) % 0.45/0.86 (define @t451 () (tptp.f13 tptp.f14 (tptp.f27 (tptp.f28 tptp.f29 @t50) @t143))) % 0.45/0.86 (define @t452 () (@var "A__questionmark_v_0_205" |tptp.'S6'|)) % 0.45/0.86 (define @t453 () (@var "A__questionmark_v_0_206" |tptp.'S4'|)) % 0.45/0.86 (define @t454 () (@var "A__questionmark_v_0_207" |tptp.'S17'|)) % 0.45/0.86 (define @t455 () (@var "A__questionmark_v_0_208" |tptp.'S8'|)) % 0.45/0.86 (define @t456 () (@var "A__questionmark_v_0_209" |tptp.'S6'|)) % 0.45/0.86 (define @t457 () (@var "A__questionmark_v_0_210" |tptp.'S4'|)) % 0.45/0.86 (define @t458 () (@var "A__questionmark_v_0_211" |tptp.'S17'|)) % 0.45/0.86 (define @t459 () (@var "A__questionmark_v_0_212" |tptp.'S8'|)) % 0.45/0.86 (define @t460 () (tptp.f11 @t312 @t45)) % 0.45/0.86 (define @t461 () (tptp.f8 @t203 @t45)) % 0.45/0.86 (define @t462 () (@var "A__questionmark_v_0_213" |tptp.'S5'|)) % 0.45/0.86 (define @t463 () (@var "A__questionmark_v_0_214" |tptp.'S5'|)) % 0.45/0.86 (define @t464 () (@var "A__questionmark_v_0_215" |tptp.'S17'|)) % 0.45/0.86 (define @t465 () (@var "A__questionmark_v_0_216" Int)) % 0.45/0.86 (define @t466 () (@var "A__questionmark_v_0_217" Int)) % 0.45/0.86 (define @t467 () (@var "A__questionmark_v_0_218" Real)) % 0.45/0.86 (define @t468 () (@var "A__questionmark_v_0_219" |tptp.'S5'|)) % 0.45/0.86 (define @t469 () (@var "A__questionmark_v_0_220" |tptp.'S9'|)) % 0.45/0.86 (define @t470 () (@var "A__questionmark_v_0_221" |tptp.'S6'|)) % 0.45/0.86 (define @t471 () (@var "A__questionmark_v_0_222" |tptp.'S4'|)) % 0.45/0.86 (define @t472 () (@var "A__questionmark_v_0_223" |tptp.'S17'|)) % 0.45/0.86 (define @t473 () (@var "A__questionmark_v_0_224" |tptp.'S8'|)) % 0.45/0.86 (define @t474 () (@var "A__questionmark_v_0_225" |tptp.'S6'|)) % 0.45/0.86 (define @t475 () (@var "A__questionmark_v_0_226" |tptp.'S4'|)) % 0.45/0.86 (define @t476 () (@var "A__questionmark_v_0_227" |tptp.'S17'|)) % 0.45/0.86 (define @t477 () (@var "A__questionmark_v_0_228" |tptp.'S8'|)) % 0.45/0.86 (define @t478 () (@var "A__questionmark_v_0_229" |tptp.'S6'|)) % 0.45/0.86 (define @t479 () (@var "A__questionmark_v_0_230" |tptp.'S4'|)) % 0.45/0.86 (define @t480 () (@var "A__questionmark_v_0_231" |tptp.'S17'|)) % 0.45/0.86 (define @t481 () (@var "A__questionmark_v_0_232" |tptp.'S8'|)) % 0.45/0.86 (define @t482 () (tptp.f17 (tptp.f42 tptp.f43 @t19) @t32)) % 0.45/0.86 (define @t483 () (tptp.f3 tptp.f31 @t121)) % 0.45/0.86 (define @t484 () (@var "A__questionmark_v_0_233" |tptp.'S2'|)) % 0.45/0.86 (define @t485 () (tptp.f3 tptp.f4 @t121)) % 0.45/0.86 (define @t486 () (tptp.f17 (tptp.f42 tptp.f43 @t79) @t121)) % 0.45/0.86 (define @t487 () (@var "A__questionmark_v_0_234" |tptp.'S2'|)) % 0.45/0.86 (define @t488 () (@var "A__questionmark_v_0_235" |tptp.'S2'|)) % 0.45/0.86 (define @t489 () (tptp.f15 (tptp.f40 tptp.f41 @t178) @t26)) % 0.45/0.86 (define @t490 () (tptp.f44 tptp.f45 @t125)) % 0.45/0.86 (define @t491 () (tptp.f44 tptp.f45 @t129)) % 0.45/0.86 (define @t492 () (= @t491 @t490)) % 0.45/0.86 (define @t493 () (tptp.f44 tptp.f46 @t125)) % 0.45/0.86 (define @t494 () (tptp.f44 tptp.f46 @t129)) % 0.45/0.86 (define @t495 () (= @t494 @t493)) % 0.45/0.86 (define @t496 () (= @t129 @t125)) % 0.45/0.86 (define @t497 () (tptp.f5 tptp.f20 @t491)) % 0.45/0.86 (define @t498 () (tptp.f5 tptp.f20 @t494)) % 0.45/0.86 (define @t499 () (tptp.f11 tptp.f12 (tptp.f13 tptp.f14 @t166))) % 0.45/0.86 (define @t500 () (= 0/1 1/1)) % 0.45/0.86 (define @t501 () (not @t500)) % 0.45/0.86 (define @t502 () (>= 0/1 0/1)) % 0.45/0.86 (define @t503 () (and @t502 @t501)) % 0.45/0.86 (define @t504 () (= 0/1 -1/1)) % 0.45/0.86 (define @t505 () (not @t504)) % 0.45/0.86 (define @t506 () (not @t502)) % 0.45/0.86 (define @t507 () (and @t506 @t505)) % 0.45/0.86 (define @t508 () (or @t507 @t503)) % 0.45/0.86 (define @t509 () (= @t3 1/1)) % 0.45/0.86 (define @t510 () (not @t509)) % 0.45/0.86 (define @t511 () (>= @t3 0/1)) % 0.45/0.86 (define @t512 () (and @t511 @t510)) % 0.45/0.86 (define @t513 () (= @t3 -1/1)) % 0.45/0.86 (define @t514 () (not @t513)) % 0.45/0.86 (define @t515 () (not @t511)) % 0.45/0.86 (define @t516 () (and @t515 @t514)) % 0.45/0.86 (define @t517 () (or @t516 @t512)) % 0.45/0.86 (define @t518 () (not (= @t3 @t3))) % 0.45/0.86 (define @t519 () (or @t518 @t516 @t512)) % 0.45/0.86 (define @t520 () (>= @t4 0/1)) % 0.45/0.86 (define @t521 () (and @t520 (not @t5))) % 0.45/0.86 (define @t522 () (= @t4 -1/1)) % 0.45/0.86 (define @t523 () (not @t520)) % 0.45/0.86 (define @t524 () (and @t523 (not @t522))) % 0.45/0.86 (define @t525 () (not @t12)) % 0.45/0.86 (define @t526 () (or @t525 @t525 @t524 @t521)) % 0.45/0.86 (define @t527 () (or @t525 @t524 @t521)) % 0.45/0.86 (define @t528 () (=> @t520 @t5)) % 0.45/0.86 (define @t529 () (not @t528)) % 0.45/0.86 (define @t530 () (=> @t523 @t522)) % 0.45/0.86 (define @t531 () (not @t530)) % 0.45/0.86 (define @t532 () (or @t525 @t531 @t529)) % 0.45/0.86 (define @t533 () (and @t12 @t530 @t528)) % 0.45/0.86 (define @t534 () (forall @t14 (not @t533))) % 0.45/0.86 (define @t535 () (not @t534)) % 0.45/0.86 (define @t536 () (* -1/1 @t4)) % 0.45/0.86 (assume @p1 (not (= tptp.f1 tptp.f2))) % 0.45/0.86 (assume @p2 true) % 0.45/0.86 (assume @p3 (= @t3 0/1)) % 0.45/0.86 (assume @p4 @t15) % 0.45/0.86 (assume @p5 (= (tptp.f3 tptp.f4 @t17) 0/1)) % 0.45/0.86 (assume @p6 (= (tptp.f3 tptp.f4 (tptp.f3 @t16 3/1)) @t18)) % 0.45/0.86 (assume @p7 (forall @t23 (exists (@list @t21) (and (= @t21 0/1) (=> (< @t21 @t19) (=> @t22 (< @t21 @t20))))))) % 0.45/0.86 (assume @p8 (forall @t23 (exists (@list @t24) (and (= @t24 @t17) (=> (< (- @t24) @t19) (=> (< @t19 @t24) (< 0/1 @t20))))))) % 0.45/0.86 (assume @p9 (forall @t23 (exists (@list @t25) (and (= @t25 @t17) (=> (<= (- @t25) @t19) (=> (<= @t19 @t25) (<= 0/1 @t20))))))) % 0.45/0.86 (assume @p10 (forall @t28 (<= 0/1 @t27))) % 0.45/0.86 (assume @p11 (= (tptp.f3 tptp.f4 tptp.f7) @t29)) % 0.45/0.86 (assume @p12 (forall @t23 (= (tptp.f3 tptp.f4 @t30) (- @t20)))) % 0.45/0.86 (assume @p13 (forall @t23 (= (tptp.f3 tptp.f4 @t31) @t20))) % 0.45/0.86 (assume @p14 (= (tptp.f3 tptp.f4 @t1) 1/1)) % 0.45/0.86 (assume @p15 (forall @t37 (=> @t36 (=> @t35 (=> @t34 (< @t33 @t20)))))) % 0.45/0.86 (assume @p16 (forall @t37 (=> @t36 (=> @t38 (=> @t34 (<= @t33 @t20)))))) % 0.45/0.86 (assume @p17 (forall @t37 (=> @t35 (< @t41 @t32)))) % 0.45/0.86 (assume @p18 (forall @t37 (=> @t35 (< @t19 @t41)))) % 0.45/0.86 (assume @p19 (forall @t37 (exists (@list @t42) (and (= @t42 0/1) (= (<= @t42 @t44) (and (or (<= @t19 @t42) (<= @t42 @t32)) (or (<= @t42 @t19) (<= @t32 @t42)))))))) % 0.45/0.86 (assume @p20 (forall @t51 (exists (@list @t48 @t47) (and (= @t48 @t50) (= @t47 @t49) (=> (<= @t47 @t48) (= (tptp.f8 tptp.f9 (tptp.f13 tptp.f14 (- @t48 @t47))) (- @t46 @t27))))))) % 0.45/0.86 (assume @p21 (forall @t51 (= (<= @t27 @t46) @t52))) % 0.45/0.86 (assume @p22 (forall @t51 (= (< @t27 @t46) @t53))) % 0.45/0.86 (assume @p23 (forall @t51 (= (= @t27 @t46) (= @t26 @t45)))) % 0.45/0.86 (assume @p24 (forall @t28 (= (<= @t27 0/1) @t55))) % 0.45/0.86 (assume @p25 (forall @t28 (= (= @t27 0/1) @t55))) % 0.45/0.86 (assume @p26 (forall @t51 (= @t53 (<= @t56 @t46)))) % 0.45/0.86 (assume @p27 (forall @t51 (= @t52 (< @t27 (+ @t46 1/1))))) % 0.45/0.86 (assume @p28 (forall @t28 (= (< 0/1 @t27) @t57))) % 0.45/0.86 (assume @p29 (forall @t51 (= (tptp.f8 tptp.f9 @t58) (+ @t27 @t46)))) % 0.45/0.86 (assume @p30 (forall @t28 (= @t60 @t56))) % 0.45/0.86 (assume @p31 (forall @t28 (exists (@list @t61) (and (= @t61 @t27) (=> @t62 (= (- @t61) @t61)) (=> (not @t62) (= @t61 @t61)))))) % 0.45/0.86 (assume @p32 (= (tptp.f8 tptp.f9 @t64) 1/1)) % 0.45/0.86 (assume @p33 (= (tptp.f8 tptp.f9 @t54) 0/1)) % 0.45/0.86 (assume @p34 (= (tptp.f8 tptp.f9 @t65) 1/1)) % 0.45/0.86 (assume @p35 (forall @t28 (< 0/1 @t60))) % 0.45/0.86 (assume @p36 (forall @t28 (not (< @t27 0/1)))) % 0.45/0.86 (assume @p37 (forall @t23 (exists (@list @t66) (and (= @t66 2/1) (=> @t67 (=> (< @t19 @t66) (< (tptp.f3 tptp.f4 (* @t66 @t19)) 1/1))))))) % 0.45/0.86 (assume @p38 (<= @t68 0/1)) % 0.45/0.86 (assume @p39 (< @t68 0/1)) % 0.45/0.86 (assume @p40 (forall @t23 (= (tptp.f3 tptp.f4 @t69) @t20))) % 0.45/0.86 (assume @p41 (forall @t23 (exists (@list @t70) (and (= @t70 @t20) (=> @t71 (<= (- @t70) 1/1)) (=> (not @t71) (<= @t70 1/1)))))) % 0.45/0.86 (assume @p42 (forall @t23 (<= @t20 1/1))) % 0.45/0.86 (assume @p43 (forall @t23 (<= @t29 @t20))) % 0.45/0.86 (assume @p44 (= (tptp.f3 tptp.f4 0/1) 1/1)) % 0.45/0.86 (assume @p45 (not (= @t68 0/1))) % 0.45/0.86 (assume @p46 (< (- @t1) tptp.f7)) % 0.45/0.86 (assume @p47 (<= 2/1 tptp.f7)) % 0.45/0.86 (assume @p48 (< tptp.f7 4/1)) % 0.45/0.86 (assume @p49 (<= 0/1 tptp.f7)) % 0.45/0.86 (assume @p50 (< 0/1 tptp.f7)) % 0.45/0.86 (assume @p51 (not (< tptp.f7 0/1))) % 0.45/0.86 (assume @p52 (not (= tptp.f7 0/1))) % 0.45/0.86 (assume @p53 (exists (@list @t72) (and (= @t72 2/1) (<= (tptp.f3 @t16 @t72) @t72)))) % 0.45/0.86 (assume @p54 (exists (@list @t73) (and (= @t73 2/1) (< (tptp.f3 @t16 @t73) @t73)))) % 0.45/0.86 (assume @p55 (< @t74 0/1)) % 0.45/0.86 (assume @p56 (<= 0/1 @t17)) % 0.45/0.86 (assume @p57 (< 0/1 @t17)) % 0.45/0.86 (assume @p58 (exists (@list @t75) (and (= @t75 2/1) (not (= (tptp.f3 @t16 @t75) @t75))))) % 0.45/0.86 (assume @p59 (not (= @t17 0/1))) % 0.45/0.86 (assume @p60 (forall @t37 (=> @t78 (=> @t38 (=> @t76 (<= @t20 @t33)))))) % 0.45/0.86 (assume @p61 (forall @t37 (=> @t78 (=> @t35 (=> @t76 (< @t20 @t33)))))) % 0.45/0.86 (assume @p62 (forall @t23 (=> @t84 (=> @t83 (exists @t82 (and (<= 0/1 @t32) @t34 (= @t33 @t19) (forall @t81 (=> (and (<= 0/1 @t79) (<= @t79 tptp.f7) (= (tptp.f3 tptp.f4 @t79) @t19)) @t80)))))))) % 0.45/0.86 (assume @p63 (exists (@list @t19 @t85) (and (= @t85 0/1) (<= @t85 @t19) (<= @t19 2/1) (= @t20 @t85) (forall @t82 (=> (and (<= @t85 @t32) (<= @t32 2/1) (= @t33 @t85)) (= @t32 @t19)))))) % 0.45/0.86 (assume @p64 (forall @t28 (= (tptp.f15 tptp.f16 @t26) (tptp.f17 tptp.f18 (tptp.f3 @t2 @t27))))) % 0.45/0.86 (assume @p65 (forall @t37 (exists (@list @t86) (and (= @t86 2/1) (= (- (tptp.f3 @t40 @t86) @t32) (tptp.f3 (tptp.f5 tptp.f6 @t87) @t86)))))) % 0.45/0.86 (assume @p66 (forall @t37 (exists (@list @t88) (and (= @t88 2/1) (= (- (tptp.f3 @t40 @t88) @t19) (tptp.f3 (tptp.f5 tptp.f6 (- @t32 @t19)) @t88)))))) % 0.45/0.86 (assume @p67 (forall @t23 (exists (@list @t89) (and (= @t89 (tptp.f3 @t43 2/1)) (= (+ @t89 @t89) @t19))))) % 0.45/0.86 (assume @p68 (forall @t93 (exists (@list @t91 @t90) (and (= @t91 2/1) (= @t90 @t92) (= (= @t19 (tptp.f3 @t90 (* @t91 @t79))) (= (* @t91 @t19) (tptp.f3 @t90 @t79))))))) % 0.45/0.86 (assume @p69 (forall @t37 (= (tptp.f3 tptp.f19 @t44) (tptp.f3 (tptp.f5 tptp.f6 @t95) @t94)))) % 0.45/0.86 (assume @p70 (forall @t28 (= (tptp.f3 tptp.f4 @t96) 1/1))) % 0.45/0.86 (assume @p71 (= (tptp.f3 tptp.f4 @t97) 0/1)) % 0.45/0.86 (assume @p72 (forall @t23 (exists (@list @t98 @t99) (and (= @t98 @t17) (= @t99 @t100) (=> @t84 (=> @t83 (and (<= (- @t98) @t99) (<= @t99 @t98)))))))) % 0.45/0.86 (assume @p73 (forall @t37 (<= (- @t104) @t102))) % 0.45/0.86 (assume @p74 (forall @t37 (= @t106 @t105))) % 0.45/0.86 (assume @p75 (forall @t93 (exists (@list @t108) (and (= @t108 @t103) (= (tptp.f3 (tptp.f5 tptp.f20 (tptp.f3 @t108 @t32)) @t79) (tptp.f3 @t108 @t107)))))) % 0.45/0.86 (assume @p76 (forall @t93 (= (tptp.f3 (tptp.f5 tptp.f20 @t39) @t79) (+ @t109 @t107)))) % 0.45/0.86 (assume @p77 (forall @t37 (exists (@list @t110) (and (= @t110 0/1) (= (= (+ @t104 @t102) @t110) (and (= @t19 @t110) (= @t32 @t110))))))) % 0.45/0.86 (assume @p78 (forall @t93 (=> @t114 (= (= @t105 @t113) @t111)))) % 0.45/0.86 (assume @p79 (forall @t93 (exists (@list @t115) (and (= @t115 @t103) (=> @t114 (= (= (tptp.f3 @t115 @t32) (tptp.f3 @t115 @t79)) @t111)))))) % 0.45/0.86 (assume @p80 (forall @t93 (=> @t67 (= (< @t105 @t113) @t116)))) % 0.45/0.86 (assume @p81 (forall @t93 (=> @t67 (= (<= @t105 @t113) @t117)))) % 0.45/0.86 (assume @p82 (forall @t93 (exists (@list @t118) (and (= @t118 @t103) (=> @t67 (= (<= (tptp.f3 @t118 @t32) (tptp.f3 @t118 @t79)) @t117)))))) % 0.45/0.86 (assume @p83 (forall @t37 (exists (@list @t119) (and (= @t119 0/1) (=> (< @t119 @t19) (=> (< @t119 @t32) (< @t119 @t106))))))) % 0.45/0.86 (assume @p84 (forall @t93 (exists (@list @t120) (and (= @t120 @t103) (=> @t67 (=> @t116 (< (tptp.f3 @t120 @t32) (tptp.f3 @t120 @t79)))))))) % 0.45/0.86 (assume @p85 (forall @t123 (= (tptp.f3 (tptp.f5 tptp.f20 @t44) (tptp.f3 (tptp.f5 tptp.f6 @t79) @t121)) (tptp.f3 (tptp.f5 tptp.f6 @t109) @t122)))) % 0.45/0.86 (assume @p86 (forall @t132 (= (tptp.f22 (tptp.f23 tptp.f24 @t131) (tptp.f22 (tptp.f23 tptp.f25 @t128) @t124)) (tptp.f22 (tptp.f23 tptp.f25 (tptp.f22 @t130 @t128)) @t127)))) % 0.45/0.86 (assume @p87 (forall (@list @t136 @t32 @t79) (exists (@list @t135 @t134) (and (= @t135 (tptp.f3 @t136 @t32)) (= @t134 (tptp.f3 @t136 @t79)) (exists (@list @t133) (and (= @t133 (tptp.f5 tptp.f20 (tptp.f3 (tptp.f5 tptp.f6 (- @t134 @t135)) (- @t79 @t32)))) (= (- @t135 (tptp.f3 @t133 @t32)) (- @t134 (tptp.f3 @t133 @t79))))))))) % 0.45/0.86 (assume @p88 (forall @t23 (=> @t84 (=> @t83 (<= @t100 @t17))))) % 0.45/0.86 (assume @p89 (forall @t23 (=> @t84 (=> @t83 (<= @t74 @t100))))) % 0.45/0.86 (assume @p90 (forall @t23 (exists (@list @t137 @t138) (and (= @t137 @t17) (= @t138 @t100) (=> (< @t29 @t19) (=> (< @t19 1/1) (and (< (- @t137) @t138) (< @t138 @t137)))))))) % 0.45/0.86 (assume @p91 (forall @t23 (=> @t67 (forall @t82 (exists @t142 (< @t32 @t141)))))) % 0.45/0.86 (assume @p92 (forall @t37 (exists (@list @t144) (and (= @t144 0/1) (=> (< @t144 @t19) (=> (<= @t144 @t32) (exists @t142 (and (<= @t141 @t32) (< @t32 (tptp.f3 (tptp.f5 tptp.f20 (tptp.f8 tptp.f9 (tptp.f13 tptp.f14 (+ @t143 1)))) @t19)))))))))) % 0.45/0.86 (assume @p93 (forall @t37 (exists (@list @t145) (and (= @t145 @t103) (= (tptp.f3 (tptp.f5 tptp.f6 (tptp.f3 @t145 @t32)) (tptp.f3 @t145 @t19)) (tptp.f3 @t92 @t19)))))) % 0.45/0.86 (assume @p94 (forall @t93 (exists (@list @t146) (and (= @t146 @t103) (= (tptp.f3 @t146 (tptp.f3 @t92 @t79)) (tptp.f3 (tptp.f5 tptp.f6 (tptp.f3 @t146 @t32)) @t79)))))) % 0.45/0.86 (assume @p95 (forall @t148 (exists (@list @t147) (and (= @t147 @t130) (= (tptp.f22 @t147 (tptp.f22 (tptp.f23 tptp.f25 @t125) @t128)) (tptp.f22 (tptp.f23 tptp.f25 (tptp.f22 @t147 @t125)) @t128)))))) % 0.45/0.86 (assume @p96 (forall @t28 (= (tptp.f3 tptp.f4 (tptp.f3 (tptp.f5 tptp.f6 (tptp.f3 @t151 @t150)) 2/1)) 0/1))) % 0.45/0.86 (assume @p97 (forall @t23 (= (= @t20 0/1) (or @t159 (exists @t157 (and @t156 @t154)))))) % 0.45/0.86 (assume @p98 (forall @t28 (= (* @t27 4/1) (tptp.f8 tptp.f9 (tptp.f13 tptp.f14 @t160))))) % 0.45/0.86 (assume @p99 (forall @t51 (= (tptp.f8 tptp.f9 @t163) (tptp.f3 @t161 @t46)))) % 0.45/0.86 (assume @p100 (forall @t37 (= (tptp.f3 tptp.f19 @t106) (tptp.f3 (tptp.f5 tptp.f20 @t95) @t94)))) % 0.45/0.86 (assume @p101 (forall @t170 (= (tptp.f27 tptp.f30 @t169) (tptp.f27 (tptp.f28 tptp.f29 @t167) @t165)))) % 0.45/0.86 (assume @p102 (forall @t23 (exists (@list @t171) (and (= @t171 @t95) (= (tptp.f3 (tptp.f5 tptp.f20 @t171) @t171) @t104))))) % 0.45/0.86 (assume @p103 (forall @t174 (exists (@list @t173) (and (= @t173 @t167) (= (tptp.f27 (tptp.f28 tptp.f29 @t173) @t173) @t172))))) % 0.45/0.86 (assume @p104 (forall @t23 (exists (@list @t175) (and (= @t175 0/1) (= (not (< @t175 @t104)) (= @t19 @t175)))))) % 0.45/0.86 (assume @p105 (forall @t23 (exists (@list @t176) (and (= @t176 0/1) (=> (<= @t176 @t19) (=> (= @t20 @t176) @t159)))))) % 0.45/0.86 (assume @p106 (forall @t179 (= (tptp.f17 tptp.f18 (tptp.f3 (tptp.f5 tptp.f20 @t60) @t32)) (tptp.f22 (tptp.f23 tptp.f24 @t178) (tptp.f17 tptp.f18 @t177))))) % 0.45/0.86 (assume @p107 (forall @t51 (= (= (tptp.f26 @t163) tptp.f1) (or @t180 @t155)))) % 0.45/0.86 (assume @p108 (forall @t28 (= @t183 (exists @t157 (= @t26 @t182))))) % 0.45/0.86 (assume @p109 (forall @t28 (= @t183 (exists @t157 (= @t26 (tptp.f13 tptp.f14 (+ @t184 1))))))) % 0.45/0.86 (assume @p110 (forall @t28 (exists (@list @t185) (and (= @t185 @t49) (=> (< 0 @t185) (= @t180 (not (= (tptp.f26 (tptp.f13 tptp.f14 (- @t185 1))) tptp.f1)))))))) % 0.45/0.86 (assume @p111 (forall @t28 (=> @t183 @t57))) % 0.45/0.86 (assume @p112 (forall @t51 (= @t188 (or @t187 @t186)))) % 0.45/0.86 (assume @p113 (forall @t51 (exists (@list @t189 @t190) (and (= @t189 @t50) (= @t190 @t49) (= (= (tptp.f26 (tptp.f13 tptp.f14 (- @t190 @t189))) tptp.f1) (or (< @t190 @t189) @t187 @t186)))))) % 0.45/0.86 (assume @p114 (forall @t51 (= @t188 (= @t180 @t155)))) % 0.45/0.86 (assume @p115 (forall @t51 (= (not @t188) (not (= @t183 @t156))))) % 0.45/0.86 (assume @p116 (forall @t28 (= (= (tptp.f26 @t59) tptp.f1) @t183))) % 0.45/0.86 (assume @p117 (not (= (tptp.f26 @t65) tptp.f1))) % 0.45/0.86 (assume @p118 (= (tptp.f26 @t54) tptp.f1)) % 0.45/0.86 (assume @p119 (forall @t37 (= (tptp.f22 (tptp.f23 tptp.f25 @t191) @t178) (tptp.f17 tptp.f18 @t87)))) % 0.45/0.86 (assume @p120 (forall @t37 (= (tptp.f22 (tptp.f23 tptp.f24 @t191) @t178) (tptp.f17 tptp.f18 @t39)))) % 0.45/0.86 (assume @p121 (forall @t28 (= @t180 (exists @t157 (= @t26 (tptp.f13 tptp.f14 @t184)))))) % 0.45/0.86 (assume @p122 (forall @t28 (= @t180 (exists @t157 (= @t26 @t192))))) % 0.45/0.86 (assume @p123 (forall @t23 (= @t195 (or @t193 (exists @t157 (and @t155 @t154)))))) % 0.45/0.86 (assume @p124 (forall @t23 (exists @t157 @t196))) % 0.45/0.86 (assume @p125 (forall @t23 (=> @t36 (exists @t157 (and (<= @t46 @t19) (< @t19 @t198)))))) % 0.45/0.86 (assume @p126 (forall @t23 (=> @t36 (exists @t157 (and (<= (tptp.f8 tptp.f9 @t199) @t19) @t196))))) % 0.45/0.86 (assume @p127 (forall @t28 (= (tptp.f3 tptp.f4 @t201) @t200))) % 0.45/0.86 (assume @p128 (forall @t37 (exists (@list @t205 @t202) (and (= @t205 @t103) (= @t202 @t206) (= (+ (tptp.f8 (tptp.f32 tptp.f33 (tptp.f3 @t205 @t33)) @t202) (tptp.f8 (tptp.f32 tptp.f33 (tptp.f3 @t205 @t204)) @t202)) (tptp.f8 @t203 @t202)))))) % 0.45/0.86 (assume @p129 (forall @t37 (exists (@list @t208) (and (= @t208 @t206) (= (tptp.f8 (tptp.f32 tptp.f33 @t39) @t208) (+ (+ (tptp.f8 @t203 @t208) (tptp.f8 @t209 @t208)) (tptp.f3 (tptp.f5 tptp.f20 @t207) @t32))))))) % 0.45/0.86 (assume @p130 (forall @t211 (=> @t180 (= (tptp.f11 (tptp.f34 tptp.f35 @t165) @t26) (tptp.f11 @t210 @t26))))) % 0.45/0.86 (assume @p131 (forall @t179 (=> @t180 (= (tptp.f8 (tptp.f32 tptp.f33 @t94) @t26) (tptp.f8 @t209 @t26))))) % 0.45/0.86 (assume @p132 (forall @t37 (exists (@list @t212 @t214 @t215 @t216 @t213 @t217) (and (= @t212 @t206) (= @t214 @t219) (= @t215 @t33) (= @t216 @t218) (= @t213 @t204) (= @t217 @t39) (= (+ (tptp.f8 (tptp.f32 tptp.f33 (- (tptp.f3 tptp.f31 @t217) (+ (tptp.f3 @t214 @t215) (tptp.f3 @t216 @t213)))) @t212) (tptp.f8 (tptp.f32 tptp.f33 (- (tptp.f3 tptp.f4 @t217) (- (tptp.f3 @t216 @t215) (tptp.f3 @t214 @t213)))) @t212)) 0/1))))) % 0.45/0.86 (assume @p133 (forall (@list @t26 @t45 @t220) (exists (@list @t222 @t221 @t223) (and (= @t222 @t50) (= @t221 @t49) (= @t223 (tptp.f34 tptp.f35 @t220)) (=> (<= @t221 @t222) (= (tptp.f11 @t223 (tptp.f13 tptp.f14 (- (+ @t222 1) @t221))) (tptp.f27 (tptp.f28 tptp.f29 (tptp.f11 @t223 (tptp.f13 tptp.f14 (- @t222 @t221)))) @t220))))))) % 0.45/0.86 (assume @p134 (forall (@list @t26 @t45 @t79) (exists (@list @t225 @t224 @t226) (and (= @t225 @t50) (= @t224 @t49) (= @t226 (tptp.f32 tptp.f33 @t79)) (=> (<= @t224 @t225) (= (tptp.f8 @t226 (tptp.f13 tptp.f14 (- (+ @t225 1) @t224))) (tptp.f3 (tptp.f5 tptp.f20 (tptp.f8 @t226 (tptp.f13 tptp.f14 (- @t225 @t224)))) @t79))))))) % 0.45/0.86 (assume @p135 (forall @t230 (exists (@list @t228 @t227 @t229) (and (= @t228 @t50) (= @t227 @t49) (= @t229 (tptp.f37 tptp.f38 @t139)) (=> (<= @t227 @t228) (= (tptp.f36 @t229 (tptp.f13 tptp.f14 (- (+ @t228 1) @t227))) (tptp.f36 (tptp.f37 tptp.f39 (tptp.f36 @t229 (tptp.f13 tptp.f14 (- @t228 @t227)))) @t139))))))) % 0.45/0.86 (assume @p136 (forall (@list @t26 @t45 @t128) (exists (@list @t232 @t231 @t233) (and (= @t232 @t50) (= @t231 @t49) (= @t233 (tptp.f40 tptp.f41 @t128)) (=> (<= @t231 @t232) (= (tptp.f15 @t233 (tptp.f13 tptp.f14 (- (+ @t232 1) @t231))) (tptp.f22 (tptp.f23 tptp.f24 (tptp.f15 @t233 (tptp.f13 tptp.f14 (- @t232 @t231)))) @t128))))))) % 0.45/0.86 (assume @p137 (forall @t211 (exists (@list @t235 @t234) (and (= @t235 @t49) (= @t234 @t210) (=> (< 0 @t235) (= (tptp.f27 (tptp.f28 tptp.f29 (tptp.f11 @t234 (tptp.f13 tptp.f14 (- @t235 1)))) @t164) (tptp.f11 @t234 @t26))))))) % 0.45/0.86 (assume @p138 (forall @t179 (exists (@list @t237 @t236) (and (= @t237 @t49) (= @t236 @t209) (=> (< 0 @t237) (= (tptp.f3 (tptp.f5 tptp.f20 (tptp.f8 @t236 (tptp.f13 tptp.f14 (- @t237 1)))) @t32) (tptp.f8 @t236 @t26))))))) % 0.45/0.86 (assume @p139 (forall @t51 (exists (@list @t239 @t238) (and (= @t239 @t49) (= @t238 @t240) (=> (< 0 @t239) (= (tptp.f36 (tptp.f37 tptp.f39 (tptp.f36 @t238 (tptp.f13 tptp.f14 (- @t239 1)))) @t45) (tptp.f36 @t238 @t26))))))) % 0.45/0.86 (assume @p140 (forall (@list @t26 @t125) (exists (@list @t242 @t241) (and (= @t242 @t49) (= @t241 @t243) (=> (< 0 @t242) (= (tptp.f22 (tptp.f23 tptp.f24 (tptp.f15 @t241 (tptp.f13 tptp.f14 (- @t242 1)))) @t125) (tptp.f15 @t241 @t26))))))) % 0.45/0.86 (assume @p141 (forall @t23 (=> @t244 @t195))) % 0.45/0.86 (assume @p142 (forall @t23 (exists (@list @t246 @t245) (and (= @t246 0/1) (= @t245 @t20) (=> (= @t194 @t246) (and (=> @t247 (= (- @t245) 1/1)) (=> (not @t247) (= @t245 1/1)))))))) % 0.45/0.86 (assume @p143 (forall @t23 (= (tptp.f3 tptp.f31 (- @t19 tptp.f7)) @t248))) % 0.45/0.86 (assume @p144 (= (tptp.f3 tptp.f31 tptp.f7) 0/1)) % 0.45/0.86 (assume @p145 (forall @t23 (= (tptp.f3 tptp.f31 (+ tptp.f7 @t19)) @t248))) % 0.45/0.86 (assume @p146 (forall @t23 (= (tptp.f3 tptp.f31 @t30) @t248))) % 0.45/0.86 (assume @p147 (forall @t23 (= (tptp.f3 tptp.f31 @t31) @t194))) % 0.45/0.86 (assume @p148 (= (tptp.f3 tptp.f31 @t1) 0/1)) % 0.45/0.86 (assume @p149 (forall @t23 (exists (@list @t249) (and (= @t249 0/1) (=> (< @t249 @t19) (=> (< @t19 tptp.f7) (< @t249 @t194))))))) % 0.45/0.86 (assume @p150 (forall @t23 (exists (@list @t250) (and (= @t250 0/1) (=> (<= @t250 @t19) (=> (<= @t19 tptp.f7) (<= @t250 @t194))))))) % 0.45/0.86 (assume @p151 (forall @t28 (< @t27 @t251))) % 0.45/0.86 (assume @p152 (forall @t23 (exists (@list @t252 @t253) (and (= @t252 @t206) (= @t253 @t69) (= (+ (tptp.f8 (tptp.f32 tptp.f33 (+ (tptp.f3 tptp.f31 @t253) @t194)) @t252) (tptp.f8 (tptp.f32 tptp.f33 (- (tptp.f3 tptp.f4 @t253) @t20)) @t252)) 0/1))))) % 0.45/0.86 (assume @p153 (forall @t23 (exists (@list @t254) (and (= @t254 @t206) (= (+ (tptp.f8 @t256 @t254) (tptp.f8 @t255 @t254)) 1/1))))) % 0.45/0.86 (assume @p154 (forall @t23 (exists (@list @t257) (and (= @t257 @t206) (= (+ (tptp.f8 @t255 @t257) (tptp.f8 @t256 @t257)) 1/1))))) % 0.45/0.86 (assume @p155 (forall @t23 (exists (@list @t258) (and (= @t258 @t206) (= (tptp.f8 @t256 @t258) (- 1/1 (tptp.f8 @t255 @t258))))))) % 0.45/0.86 (assume @p156 (forall @t23 (exists (@list @t259) (and (= @t259 @t206) (= (tptp.f8 @t255 @t259) (- 1/1 (tptp.f8 @t256 @t259))))))) % 0.45/0.86 (assume @p157 (forall @t23 (exists (@list @t260) (and (= @t260 @t206) (= (tptp.f3 tptp.f4 @t207) (- (tptp.f8 @t255 @t260) (tptp.f8 @t256 @t260))))))) % 0.45/0.86 (assume @p158 (forall @t23 (exists (@list @t261) (and (= @t261 1/1) (=> (and (=> @t263 (< @t69 @t261)) (=> (not @t263) (< @t19 @t261))) (< @t262 @t261)))))) % 0.45/0.86 (assume @p159 (forall @t23 (exists (@list @t264) (and (= @t264 0/1) (=> (< @t264 @t19) (=> (< @t19 2/1) (< @t264 @t194))))))) % 0.45/0.86 (assume @p160 (forall @t37 (exists (@list @t265 @t266) (and (= @t265 0/1) (= @t266 @t206) (= (= (+ (tptp.f8 @t203 @t266) (tptp.f8 @t209 @t266)) @t265) (and (= @t19 @t265) (= @t32 @t265))))))) % 0.45/0.86 (assume @p161 (forall @t37 (exists (@list @t267) (and (= @t267 @t206) (<= (- (tptp.f8 @t203 @t267)) (tptp.f8 @t209 @t267)))))) % 0.45/0.86 (assume @p162 (forall @t23 (= (tptp.f3 tptp.f31 @t69) @t248))) % 0.45/0.86 (assume @p163 (forall @t23 (exists (@list @t268) (and (= @t268 @t194) (=> @t269 (<= (- @t268) 1/1)) (=> (not @t269) (<= @t268 1/1)))))) % 0.45/0.86 (assume @p164 (forall @t23 (<= @t194 1/1))) % 0.45/0.86 (assume @p165 (forall @t23 (<= @t29 @t194))) % 0.45/0.86 (assume @p166 (exists (@list @t270) (and (= @t270 0/1) (= (tptp.f3 tptp.f31 @t270) @t270)))) % 0.45/0.86 (assume @p167 (forall @t28 (<= 1/1 @t251))) % 0.45/0.86 (assume @p168 (forall @t23 (exists (@list @t271) (and (= @t271 @t206) (= (* 4/1 (tptp.f8 @t203 @t271)) (tptp.f8 (tptp.f32 tptp.f33 @t207) @t271)))))) % 0.45/0.86 (assume @p169 (forall @t23 (=> @t84 (=> @t83 (= (tptp.f3 tptp.f31 @t100) @t19))))) % 0.45/0.86 (assume @p170 (forall @t37 (= (tptp.f3 tptp.f4 @t39) (- @t273 @t272)))) % 0.45/0.86 (assume @p171 (forall @t37 (= @t274 (+ @t273 @t272)))) % 0.45/0.86 (assume @p172 (forall @t37 (= @t274 (+ (tptp.f3 @t276 @t20) (tptp.f3 @t275 @t194))))) % 0.45/0.86 (assume @p173 (forall @t37 (= (tptp.f3 tptp.f31 @t39) (+ @t278 @t277)))) % 0.45/0.86 (assume @p174 (forall @t37 (= @t279 (- (tptp.f3 @t276 @t194) (tptp.f3 @t275 @t20))))) % 0.45/0.86 (assume @p175 (forall @t37 (= @t279 (- @t278 @t277)))) % 0.45/0.86 (assume @p176 (forall @t23 (exists (@list @t280) (and (= @t280 2/1) (= (tptp.f3 tptp.f31 (* @t280 @t19)) (tptp.f3 (tptp.f5 tptp.f20 (* @t280 @t194)) @t20)))))) % 0.45/0.86 (assume @p177 (forall @t23 (exists (@list @t282 @t281) (and (= @t282 @t20) (= @t281 @t194) (= (+ (tptp.f3 (tptp.f5 tptp.f20 @t282) @t282) (tptp.f3 (tptp.f5 tptp.f20 @t281) @t281)) 1/1))))) % 0.45/0.86 (assume @p178 (forall @t23 (exists (@list @t283) (and (= @t283 0/1) (=> (< (tptp.f3 (tptp.f5 tptp.f6 @t77) 2/1) @t19) (=> (< @t19 @t283) (< @t194 @t283))))))) % 0.45/0.86 (assume @p179 (forall @t37 (exists (@list @t284) (and (= @t284 @t17) (=> (<= (- @t284) @t19) (=> @t38 (=> (<= @t32 @t284) (<= @t194 @t204)))))))) % 0.45/0.86 (assume @p180 (forall @t23 (exists (@list @t285) (and (= @t285 0/1) (=> (< @t285 @t19) (=> @t22 (< @t285 @t194))))))) % 0.45/0.86 (assume @p181 (= (tptp.f3 tptp.f31 (tptp.f3 @t16 6/1)) @t18)) % 0.45/0.86 (assume @p182 (= (tptp.f3 tptp.f31 @t17) 1/1)) % 0.45/0.86 (assume @p183 (forall @t23 (exists (@list @t286) (and (= @t286 0/1) (=> (< @t286 @t19) (=> (< @t19 @t1) (or (not (= @t194 @t286)) (not @t244)))))))) % 0.45/0.86 (assume @p184 (forall @t28 (= (tptp.f3 tptp.f31 (tptp.f3 (tptp.f5 tptp.f6 (tptp.f3 (tptp.f5 tptp.f20 @t150) tptp.f7)) 2/1)) @t200))) % 0.45/0.86 (assume @p185 (= (tptp.f3 tptp.f31 @t97) @t29)) % 0.45/0.86 (assume @p186 (forall @t28 (= (tptp.f3 tptp.f31 @t96) 0/1))) % 0.45/0.86 (assume @p187 (forall @t28 (= (tptp.f3 tptp.f31 @t287) 0/1))) % 0.45/0.86 (assume @p188 (forall @t28 (= (tptp.f3 tptp.f31 @t201) 0/1))) % 0.45/0.86 (assume @p189 (forall @t23 (= @t248 (tptp.f3 tptp.f4 (+ @t19 @t17))))) % 0.45/0.86 (assume @p190 (forall @t23 (= @t194 (tptp.f3 tptp.f4 @t288)))) % 0.45/0.86 (assume @p191 (forall @t23 (= @t20 (tptp.f3 tptp.f31 @t288)))) % 0.45/0.86 (assume @p192 (forall @t23 (exists (@list @t289) (and (= @t289 @t17) (=> (<= (- @t289) @t19) (=> (<= @t19 @t289) (= (tptp.f3 tptp.f21 @t194) @t19))))))) % 0.45/0.86 (assume @p193 (forall @t23 (exists (@list @t291 @t290) (and (= @t291 @t17) (= @t290 @t100) (=> @t84 (=> @t83 (and (<= (- @t291) @t290) (<= @t290 @t291) (= (tptp.f3 tptp.f31 @t290) @t19)))))))) % 0.45/0.86 (assume @p194 (forall @t23 (exists (@list @t292) (and (= @t292 @t100) (=> @t84 (=> @t83 (and (<= @t74 @t292) (<= @t292 tptp.f7) (= (tptp.f3 tptp.f31 @t292) @t19)))))))) % 0.45/0.86 (assume @p195 (forall @t28 (= (tptp.f3 tptp.f4 @t287) @t200))) % 0.45/0.86 (assume @p196 (forall @t23 (exists (@list @t293) (and (= @t293 0/1) (=> (<= @t293 @t19) (=> (= @t194 @t293) @t193)))))) % 0.45/0.86 (assume @p197 (forall @t297 (exists (@list @t294) (and (= @t294 2/1) (= (tptp.f3 tptp.f31 (+ @t19 (tptp.f3 @t296 @t294))) (tptp.f3 tptp.f4 (+ @t19 (tptp.f3 @t295 @t294)))))))) % 0.45/0.86 (assume @p198 (forall @t297 (exists (@list @t298) (and (= @t298 2/1) (= (tptp.f3 tptp.f4 (+ @t19 (tptp.f3 @t296 @t298))) (- (tptp.f3 tptp.f31 (+ @t19 (tptp.f3 @t295 @t298))))))))) % 0.45/0.86 (assume @p199 (forall @t23 (=> @t84 (=> @t83 (exists (@list @t32 @t299) (and (= @t299 @t17) (<= @t300 @t32) (<= @t32 @t299) (= @t204 @t19) (forall @t81 (=> (and (<= @t300 @t79) (<= @t79 @t299) (= (tptp.f3 tptp.f31 @t79) @t19)) @t80)))))))) % 0.45/0.86 (assume @p200 (forall @t51 (= (= (tptp.f26 @t302) tptp.f1) (and @t180 (< 0 @t50))))) % 0.45/0.86 (assume @p201 (forall @t51 (= @t304 @t303))) % 0.45/0.86 (assume @p202 (forall @t51 (= @t303 @t304))) % 0.45/0.86 (assume @p203 (forall @t297 (= (tptp.f15 (tptp.f40 tptp.f41 @t191) @t45) (tptp.f17 tptp.f18 @t305)))) % 0.45/0.86 (assume @p204 (forall @t28 (exists (@list @t306) (and (= @t306 @t149) (=> @t307 (= (tptp.f13 tptp.f14 (+ (+ (tptp.f11 tptp.f12 (tptp.f13 tptp.f14 (- @t306 2))) 1) 1)) (tptp.f13 tptp.f14 @t306))))))) % 0.45/0.86 (assume @p205 (forall @t28 (exists (@list @t308) (and (= @t308 @t160) (=> @t307 (= (tptp.f13 tptp.f14 (+ (+ (tptp.f11 tptp.f12 (tptp.f13 tptp.f14 (- @t308 2))) 1) 1)) (tptp.f13 tptp.f14 @t308))))))) % 0.45/0.86 (assume @p206 (forall @t28 (exists (@list @t309) (and (= @t309 @t149) (=> @t307 (= (tptp.f13 tptp.f14 (+ (tptp.f11 tptp.f12 (tptp.f13 tptp.f14 (- @t309 1))) 1)) (tptp.f13 tptp.f14 @t309))))))) % 0.45/0.86 (assume @p207 (forall @t297 (exists (@list @t310) (and (= @t310 1/1) (=> @t36 (<= (+ @t305 @t310) (tptp.f8 (tptp.f32 tptp.f33 (+ @t19 @t310)) @t45))))))) % 0.45/0.86 (assume @p208 (forall @t313 (exists (@list @t311) (and (= @t311 @t312) (= (tptp.f11 @t311 @t182) (tptp.f27 @t168 (tptp.f11 (tptp.f34 tptp.f35 (tptp.f11 @t311 @t45)) @t206))))))) % 0.45/0.86 (assume @p209 (forall @t297 (exists (@list @t314) (and (= @t314 @t203) (= (tptp.f8 @t314 @t182) (tptp.f3 @t103 (tptp.f8 (tptp.f32 tptp.f33 (tptp.f8 @t314 @t45)) @t206))))))) % 0.45/0.86 (assume @p210 (forall @t51 (exists (@list @t315) (and (= @t315 @t301) (= (tptp.f36 @t315 @t182) (tptp.f36 @t316 (tptp.f36 (tptp.f37 tptp.f38 (tptp.f36 @t315 @t45)) @t206))))))) % 0.45/0.86 (assume @p211 (forall @t319 (exists (@list @t317) (and (= @t317 @t318) (= (tptp.f15 @t317 @t182) (tptp.f22 @t130 (tptp.f15 (tptp.f40 tptp.f41 (tptp.f15 @t317 @t45)) @t206))))))) % 0.45/0.86 (assume @p212 (forall @t51 (= @t322 (or @t320 @t57)))) % 0.45/0.86 (assume @p213 (forall @t174 (exists (@list @t323) (and (= @t323 @t324) (= (tptp.f27 tptp.f30 @t323) @t323))))) % 0.45/0.86 (assume @p214 (forall @t23 (exists (@list @t325) (and (= @t325 @t262) (= (tptp.f3 tptp.f19 @t325) @t325))))) % 0.45/0.86 (assume @p215 (forall @t174 (exists (@list @t326) (and (= @t326 @t206) (= (tptp.f11 @t327 @t326) (tptp.f11 @t312 @t326)))))) % 0.45/0.86 (assume @p216 (forall @t23 (exists (@list @t328) (and (= @t328 @t206) (= (tptp.f8 @t329 @t328) (tptp.f8 @t203 @t328)))))) % 0.45/0.86 (assume @p217 (forall @t28 (exists (@list @t330) (and (= @t330 @t49) (= (tptp.f13 tptp.f14 (* 2 @t330)) (tptp.f13 tptp.f14 (+ @t330 @t330))))))) % 0.45/0.86 (assume @p218 (forall @t28 (exists (@list @t331) (and (= @t331 @t49) (= (tptp.f13 tptp.f14 (* @t331 2)) (tptp.f13 tptp.f14 (+ @t331 @t331))))))) % 0.45/0.86 (assume @p219 (forall @t51 (exists (@list @t335 @t333 @t332) (and (= @t335 @t54) (= @t333 @t49) (= @t332 @t50) (=> @t336 (= @t334 @t335)) (=> (not @t336) (= @t334 (tptp.f13 tptp.f14 (+ @t332 (tptp.f27 (tptp.f28 tptp.f29 (tptp.f11 tptp.f12 (tptp.f13 tptp.f14 (- @t333 1)))) @t332))))))))) % 0.45/0.86 (assume @p220 (forall @t51 (exists (@list @t337) (and (= @t337 @t301) (=> @t320 (= @t338 @t65)) (=> (not @t320) (= @t338 (tptp.f13 tptp.f14 (tptp.f27 @t162 (tptp.f11 tptp.f12 (tptp.f36 @t337 @t199)))))))))) % 0.45/0.86 (assume @p221 (forall @t174 (= (tptp.f11 @t312 @t339) (tptp.f27 (tptp.f28 tptp.f29 @t172) @t166)))) % 0.45/0.86 (assume @p222 (forall @t23 (= (tptp.f8 @t203 @t339) (tptp.f3 (tptp.f5 tptp.f20 @t104) @t19)))) % 0.45/0.86 (assume @p223 (forall @t28 (= (tptp.f36 @t301 @t339) (tptp.f36 (tptp.f37 tptp.f39 @t340) @t26)))) % 0.45/0.86 (assume @p224 (forall @t342 (= (tptp.f15 @t318 @t339) (tptp.f22 (tptp.f23 tptp.f24 @t341) @t129)))) % 0.45/0.86 (assume @p225 (forall @t174 (= @t324 @t172))) % 0.45/0.86 (assume @p226 (forall @t23 (= @t262 @t104))) % 0.45/0.86 (assume @p227 (forall @t28 (= @t343 @t340))) % 0.45/0.86 (assume @p228 (forall @t342 (= @t344 @t341))) % 0.45/0.86 (assume @p229 (forall @t313 (exists (@list @t345) (and (= @t345 @t312) (= (tptp.f11 @t345 @t192) (tptp.f11 (tptp.f34 tptp.f35 (tptp.f11 @t345 @t45)) @t206)))))) % 0.45/0.86 (assume @p230 (forall @t297 (exists (@list @t346) (and (= @t346 @t203) (= (tptp.f8 @t346 @t192) (tptp.f8 (tptp.f32 tptp.f33 (tptp.f8 @t346 @t45)) @t206)))))) % 0.45/0.86 (assume @p231 (forall @t51 (exists (@list @t347) (and (= @t347 @t301) (= (tptp.f36 @t347 @t192) (tptp.f36 (tptp.f37 tptp.f38 (tptp.f36 @t347 @t45)) @t206)))))) % 0.45/0.86 (assume @p232 (forall @t319 (exists (@list @t348) (and (= @t348 @t318) (= (tptp.f15 @t348 @t192) (tptp.f15 (tptp.f40 tptp.f41 (tptp.f15 @t348 @t45)) @t206)))))) % 0.45/0.86 (assume @p233 (forall @t313 (exists (@list @t350) (and (= @t350 @t312) (exists (@list @t349) (and (= @t349 (tptp.f11 @t350 @t45)) (= (tptp.f11 @t350 @t192) (tptp.f27 (tptp.f28 tptp.f29 @t349) @t349)))))))) % 0.45/0.86 (assume @p234 (forall @t297 (exists (@list @t352) (and (= @t352 @t203) (exists (@list @t351) (and (= @t351 (tptp.f8 @t352 @t45)) (= (tptp.f8 @t352 @t192) (tptp.f3 (tptp.f5 tptp.f20 @t351) @t351)))))))) % 0.45/0.86 (assume @p235 (forall @t51 (exists (@list @t354) (and (= @t354 @t301) (exists (@list @t353) (and (= @t353 (tptp.f36 @t354 @t45)) (= (tptp.f36 @t354 @t192) (tptp.f36 (tptp.f37 tptp.f39 @t353) @t353)))))))) % 0.45/0.86 (assume @p236 (forall @t319 (exists (@list @t356) (and (= @t356 @t318) (exists (@list @t355) (and (= @t355 (tptp.f15 @t356 @t45)) (= (tptp.f15 @t356 @t192) (tptp.f22 (tptp.f23 tptp.f24 @t355) @t355)))))))) % 0.45/0.86 (assume @p237 (forall @t313 (exists (@list @t358) (and (= @t358 @t312) (exists (@list @t357) (and (= @t357 (tptp.f11 @t358 @t45)) (= (tptp.f11 @t358 @t182) (tptp.f27 @t168 (tptp.f27 (tptp.f28 tptp.f29 @t357) @t357))))))))) % 0.45/0.86 (assume @p238 (forall @t297 (exists (@list @t360) (and (= @t360 @t203) (exists (@list @t359) (and (= @t359 (tptp.f8 @t360 @t45)) (= (tptp.f8 @t360 @t182) (tptp.f3 @t103 (tptp.f3 (tptp.f5 tptp.f20 @t359) @t359))))))))) % 0.45/0.86 (assume @p239 (forall @t51 (exists (@list @t362) (and (= @t362 @t301) (exists (@list @t361) (and (= @t361 (tptp.f36 @t362 @t45)) (= (tptp.f36 @t362 @t182) (tptp.f36 @t316 (tptp.f36 (tptp.f37 tptp.f39 @t361) @t361))))))))) % 0.45/0.86 (assume @p240 (forall @t319 (exists (@list @t364) (and (= @t364 @t318) (exists (@list @t363) (and (= @t363 (tptp.f15 @t364 @t45)) (= (tptp.f15 @t364 @t182) (tptp.f22 @t130 (tptp.f22 (tptp.f23 tptp.f24 @t363) @t363))))))))) % 0.45/0.86 (assume @p241 (forall @t370 (exists (@list @t367) (and (= @t367 @t316) (= (tptp.f36 (tptp.f37 tptp.f39 (tptp.f36 @t367 @t45)) @t369) (tptp.f36 (tptp.f37 tptp.f39 (tptp.f36 @t367 @t139)) (tptp.f36 @t366 @t365))))))) % 0.45/0.86 (assume @p242 (forall @t123 (exists (@list @t371) (and (= @t371 @t103) (= (tptp.f3 (tptp.f5 tptp.f20 (tptp.f3 @t371 @t32)) @t372) (tptp.f3 (tptp.f5 tptp.f20 (tptp.f3 @t371 @t79)) @t122)))))) % 0.45/0.86 (assume @p243 (forall @t378 (exists (@list @t375) (and (= @t375 @t168) (= (tptp.f27 (tptp.f28 tptp.f29 (tptp.f27 @t375 @t164)) @t377) (tptp.f27 (tptp.f28 tptp.f29 (tptp.f27 @t375 @t220)) (tptp.f27 @t374 @t373))))))) % 0.45/0.86 (assume @p244 (forall @t132 (exists (@list @t379) (and (= @t379 @t130) (= (tptp.f22 (tptp.f23 tptp.f24 (tptp.f22 @t379 @t125)) @t381) (tptp.f22 (tptp.f23 tptp.f24 (tptp.f22 @t379 @t128)) @t127)))))) % 0.45/0.86 (assume @p245 (forall @t370 (exists (@list @t382 @t383) (and (= @t382 (tptp.f37 tptp.f39 @t384)) (= @t383 @t368) (= (tptp.f36 @t382 (tptp.f36 @t383 @t365)) (tptp.f36 @t383 (tptp.f36 @t382 @t365))))))) % 0.45/0.86 (assume @p246 (forall @t123 (exists (@list @t385 @t386) (and (= @t385 (tptp.f5 tptp.f20 @t106)) (= @t386 @t112) (= (tptp.f3 @t385 (tptp.f3 @t386 @t121)) (tptp.f3 @t386 (tptp.f3 @t385 @t121))))))) % 0.45/0.86 (assume @p247 (forall @t378 (exists (@list @t387 @t388) (and (= @t387 (tptp.f28 tptp.f29 @t169)) (= @t388 @t376) (= (tptp.f27 @t387 (tptp.f27 @t388 @t373)) (tptp.f27 @t388 (tptp.f27 @t387 @t373))))))) % 0.45/0.86 (assume @p248 (forall @t132 (exists (@list @t389 @t390) (and (= @t389 (tptp.f23 tptp.f24 @t391)) (= @t390 @t380) (= (tptp.f22 @t389 (tptp.f22 @t390 @t124)) (tptp.f22 @t390 (tptp.f22 @t389 @t124))))))) % 0.45/0.86 (assume @p249 (forall @t370 (exists (@list @t393 @t392) (and (= @t393 @t316) (= @t392 @t369) (= (tptp.f36 (tptp.f37 tptp.f39 (tptp.f36 @t393 @t45)) @t392) (tptp.f36 @t393 (tptp.f36 @t366 @t392))))))) % 0.45/0.86 (assume @p250 (forall @t123 (exists (@list @t395 @t394) (and (= @t395 @t103) (= @t394 @t372) (= (tptp.f3 (tptp.f5 tptp.f20 (tptp.f3 @t395 @t32)) @t394) (tptp.f3 @t395 (tptp.f3 @t101 @t394))))))) % 0.45/0.86 (assume @p251 (forall @t378 (exists (@list @t397 @t396) (and (= @t397 @t168) (= @t396 @t377) (= (tptp.f27 (tptp.f28 tptp.f29 (tptp.f27 @t397 @t164)) @t396) (tptp.f27 @t397 (tptp.f27 @t374 @t396))))))) % 0.45/0.86 (assume @p252 (forall @t132 (exists (@list @t399 @t398) (and (= @t399 @t130) (= @t398 @t381) (= (tptp.f22 (tptp.f23 tptp.f24 (tptp.f22 @t399 @t125)) @t398) (tptp.f22 @t399 (tptp.f22 @t126 @t398))))))) % 0.45/0.86 (assume @p253 (forall @t230 (exists (@list @t400) (and (= @t400 @t316) (= (tptp.f36 (tptp.f37 tptp.f39 (tptp.f36 @t400 @t45)) @t139) (tptp.f36 (tptp.f37 tptp.f39 (tptp.f36 @t400 @t139)) @t45)))))) % 0.45/0.86 (assume @p254 (forall @t93 (exists (@list @t401) (and (= @t401 @t103) (= (tptp.f3 (tptp.f5 tptp.f20 (tptp.f3 @t401 @t32)) @t79) (tptp.f3 (tptp.f5 tptp.f20 (tptp.f3 @t401 @t79)) @t32)))))) % 0.45/0.86 (assume @p255 (forall @t403 (exists (@list @t402) (and (= @t402 @t168) (= (tptp.f27 (tptp.f28 tptp.f29 (tptp.f27 @t402 @t164)) @t220) (tptp.f27 (tptp.f28 tptp.f29 (tptp.f27 @t402 @t220)) @t164)))))) % 0.45/0.86 (assume @p256 (forall @t148 (exists (@list @t404) (and (= @t404 @t130) (= (tptp.f22 (tptp.f23 tptp.f24 (tptp.f22 @t404 @t125)) @t128) (tptp.f22 (tptp.f23 tptp.f24 (tptp.f22 @t404 @t128)) @t125)))))) % 0.45/0.86 (assume @p257 (forall @t230 (exists (@list @t406) (and (= @t406 @t316) (= (tptp.f36 (tptp.f37 tptp.f39 (tptp.f36 @t406 @t45)) @t139) (tptp.f36 @t406 @t405)))))) % 0.45/0.86 (assume @p258 (forall @t93 (exists (@list @t407) (and (= @t407 @t103) (= (tptp.f3 (tptp.f5 tptp.f20 (tptp.f3 @t407 @t32)) @t79) (tptp.f3 @t407 @t107)))))) % 0.45/0.86 (assume @p259 (forall @t403 (exists (@list @t409) (and (= @t409 @t168) (= (tptp.f27 (tptp.f28 tptp.f29 (tptp.f27 @t409 @t164)) @t220) (tptp.f27 @t409 @t408)))))) % 0.45/0.86 (assume @p260 (forall @t148 (exists (@list @t411) (and (= @t411 @t130) (= (tptp.f22 (tptp.f23 tptp.f24 (tptp.f22 @t411 @t125)) @t128) (tptp.f22 @t411 @t410)))))) % 0.45/0.86 (assume @p261 (forall @t230 (exists (@list @t412) (and (= @t412 @t316) (= (tptp.f36 @t412 @t405) (tptp.f36 (tptp.f37 tptp.f39 (tptp.f36 @t412 @t45)) @t139)))))) % 0.45/0.86 (assume @p262 (forall @t93 (exists (@list @t413) (and (= @t413 @t103) (= (tptp.f3 @t413 @t107) (tptp.f3 (tptp.f5 tptp.f20 (tptp.f3 @t413 @t32)) @t79)))))) % 0.45/0.86 (assume @p263 (forall @t403 (exists (@list @t414) (and (= @t414 @t168) (= (tptp.f27 @t414 @t408) (tptp.f27 (tptp.f28 tptp.f29 (tptp.f27 @t414 @t164)) @t220)))))) % 0.45/0.86 (assume @p264 (forall @t148 (exists (@list @t415) (and (= @t415 @t130) (= (tptp.f22 @t415 @t410) (tptp.f22 (tptp.f23 tptp.f24 (tptp.f22 @t415 @t125)) @t128)))))) % 0.45/0.86 (assume @p265 (forall @t230 (exists (@list @t416 @t417) (and (= @t416 @t316) (= @t417 @t366) (= (tptp.f36 @t416 (tptp.f36 @t417 @t139)) (tptp.f36 @t417 (tptp.f36 @t416 @t139))))))) % 0.45/0.86 (assume @p266 (forall @t93 (exists (@list @t418 @t419) (and (= @t418 @t103) (= @t419 @t101) (= (tptp.f3 @t418 (tptp.f3 @t419 @t79)) (tptp.f3 @t419 (tptp.f3 @t418 @t79))))))) % 0.45/0.86 (assume @p267 (forall @t403 (exists (@list @t420 @t421) (and (= @t420 @t168) (= @t421 @t374) (= (tptp.f27 @t420 (tptp.f27 @t421 @t220)) (tptp.f27 @t421 (tptp.f27 @t420 @t220))))))) % 0.45/0.86 (assume @p268 (forall @t148 (exists (@list @t422 @t423) (and (= @t422 @t130) (= @t423 @t126) (= (tptp.f22 @t422 (tptp.f22 @t423 @t128)) (tptp.f22 @t423 (tptp.f22 @t422 @t128))))))) % 0.45/0.86 (assume @p269 (forall @t51 (= @t384 (tptp.f36 @t366 @t26)))) % 0.45/0.86 (assume @p270 (forall @t170 (= @t169 (tptp.f27 @t374 @t166)))) % 0.45/0.86 (assume @p271 (forall @t424 (= @t391 (tptp.f22 @t126 @t129)))) % 0.45/0.86 (assume @p272 (forall @t174 (= (tptp.f11 @t312 @t65) @t166))) % 0.45/0.86 (assume @p273 (forall @t23 (= (tptp.f8 @t203 @t65) @t19))) % 0.45/0.86 (assume @p274 (forall @t28 (= (tptp.f36 @t301 @t65) @t26))) % 0.45/0.86 (assume @p275 (forall @t342 (= (tptp.f15 @t318 @t65) @t129))) % 0.45/0.86 (assume @p276 (forall @t174 (= @t172 @t324))) % 0.45/0.86 (assume @p277 (forall @t23 (= @t104 @t262))) % 0.45/0.86 (assume @p278 (forall @t28 (= @t340 @t343))) % 0.45/0.86 (assume @p279 (forall @t342 (= @t341 @t344))) % 0.45/0.86 (assume @p280 (forall @t313 (exists (@list @t425) (and (= @t425 @t312) (= (tptp.f11 @t425 @t197) (tptp.f27 @t168 (tptp.f11 @t425 @t45))))))) % 0.45/0.86 (assume @p281 (forall @t297 (exists (@list @t426) (and (= @t426 @t203) (= (tptp.f8 @t426 @t197) (tptp.f3 @t103 (tptp.f8 @t426 @t45))))))) % 0.45/0.86 (assume @p282 (forall @t51 (exists (@list @t427) (and (= @t427 @t301) (= (tptp.f36 @t427 @t197) (tptp.f36 @t316 (tptp.f36 @t427 @t45))))))) % 0.45/0.86 (assume @p283 (forall @t319 (exists (@list @t428) (and (= @t428 @t318) (= (tptp.f15 @t428 @t197) (tptp.f22 @t130 (tptp.f15 @t428 @t45))))))) % 0.45/0.86 (assume @p284 (forall @t313 (exists (@list @t429) (and (= @t429 @t312) (= (tptp.f27 @t168 (tptp.f11 @t429 @t45)) (tptp.f11 @t429 @t197)))))) % 0.45/0.86 (assume @p285 (forall @t297 (exists (@list @t430) (and (= @t430 @t203) (= (tptp.f3 @t103 (tptp.f8 @t430 @t45)) (tptp.f8 @t430 @t197)))))) % 0.45/0.86 (assume @p286 (forall @t51 (exists (@list @t431) (and (= @t431 @t301) (= (tptp.f36 @t316 (tptp.f36 @t431 @t45)) (tptp.f36 @t431 @t197)))))) % 0.45/0.86 (assume @p287 (forall @t319 (exists (@list @t432) (and (= @t432 @t318) (= (tptp.f22 @t130 (tptp.f15 @t432 @t45)) (tptp.f15 @t432 @t197)))))) % 0.45/0.86 (assume @p288 (forall @t313 (exists (@list @t433) (and (= @t433 @t312) (= (tptp.f27 (tptp.f28 tptp.f29 (tptp.f11 @t433 @t45)) @t166) (tptp.f11 @t433 @t197)))))) % 0.45/0.86 (assume @p289 (forall @t297 (exists (@list @t434) (and (= @t434 @t203) (= (tptp.f3 (tptp.f5 tptp.f20 (tptp.f8 @t434 @t45)) @t19) (tptp.f8 @t434 @t197)))))) % 0.45/0.86 (assume @p290 (forall @t51 (exists (@list @t435) (and (= @t435 @t301) (= (tptp.f36 (tptp.f37 tptp.f39 (tptp.f36 @t435 @t45)) @t26) (tptp.f36 @t435 @t197)))))) % 0.45/0.86 (assume @p291 (forall @t319 (exists (@list @t436) (and (= @t436 @t318) (= (tptp.f22 (tptp.f23 tptp.f24 (tptp.f15 @t436 @t45)) @t129) (tptp.f15 @t436 @t197)))))) % 0.45/0.86 (assume @p292 (forall (@list @t166 @t164 @t139) (= (tptp.f11 (tptp.f34 tptp.f35 @t169) @t139) (tptp.f27 (tptp.f28 tptp.f29 (tptp.f11 @t312 @t139)) (tptp.f11 @t210 @t139))))) % 0.45/0.86 (assume @p293 (forall @t439 (= (tptp.f8 (tptp.f32 tptp.f33 @t106) @t139) (tptp.f3 (tptp.f5 tptp.f20 @t438) @t437)))) % 0.45/0.86 (assume @p294 (forall @t230 (= (tptp.f36 (tptp.f37 tptp.f38 @t384) @t139) (tptp.f36 (tptp.f37 tptp.f39 (tptp.f36 @t301 @t139)) (tptp.f36 @t240 @t139))))) % 0.45/0.86 (assume @p295 (forall @t442 (= (tptp.f15 (tptp.f40 tptp.f41 @t391) @t139) (tptp.f22 (tptp.f23 tptp.f24 @t441) @t440)))) % 0.45/0.86 (assume @p296 (forall @t445 (exists (@list @t444) (and (= @t444 @t312) (= (tptp.f27 (tptp.f28 tptp.f29 (tptp.f11 @t444 @t45)) (tptp.f11 @t444 @t139)) (tptp.f11 @t444 @t443)))))) % 0.45/0.86 (assume @p297 (forall @t447 (exists (@list @t446) (and (= @t446 @t203) (= (tptp.f3 (tptp.f5 tptp.f20 (tptp.f8 @t446 @t45)) (tptp.f8 @t446 @t139)) (tptp.f8 @t446 @t443)))))) % 0.45/0.86 (assume @p298 (forall @t230 (exists (@list @t448) (and (= @t448 @t301) (= (tptp.f36 (tptp.f37 tptp.f39 (tptp.f36 @t448 @t45)) (tptp.f36 @t448 @t139)) (tptp.f36 @t448 @t443)))))) % 0.45/0.86 (assume @p299 (forall @t450 (exists (@list @t449) (and (= @t449 @t318) (= (tptp.f22 (tptp.f23 tptp.f24 (tptp.f15 @t449 @t45)) (tptp.f15 @t449 @t139)) (tptp.f15 @t449 @t443)))))) % 0.45/0.86 (assume @p300 (forall @t445 (exists (@list @t452) (and (= @t452 @t312) (= (tptp.f11 (tptp.f34 tptp.f35 (tptp.f11 @t452 @t45)) @t139) (tptp.f11 @t452 @t451)))))) % 0.45/0.86 (assume @p301 (forall @t447 (exists (@list @t453) (and (= @t453 @t203) (= (tptp.f8 (tptp.f32 tptp.f33 (tptp.f8 @t453 @t45)) @t139) (tptp.f8 @t453 @t451)))))) % 0.45/0.86 (assume @p302 (forall @t230 (exists (@list @t454) (and (= @t454 @t301) (= (tptp.f36 (tptp.f37 tptp.f38 (tptp.f36 @t454 @t45)) @t139) (tptp.f36 @t454 @t451)))))) % 0.45/0.86 (assume @p303 (forall @t450 (exists (@list @t455) (and (= @t455 @t318) (= (tptp.f15 (tptp.f40 tptp.f41 (tptp.f15 @t455 @t45)) @t139) (tptp.f15 @t455 @t451)))))) % 0.45/0.86 (assume @p304 (forall @t445 (exists (@list @t456) (and (= @t456 @t312) (= (tptp.f11 @t456 @t451) (tptp.f11 (tptp.f34 tptp.f35 (tptp.f11 @t456 @t45)) @t139)))))) % 0.45/0.86 (assume @p305 (forall @t447 (exists (@list @t457) (and (= @t457 @t203) (= (tptp.f8 @t457 @t451) (tptp.f8 (tptp.f32 tptp.f33 (tptp.f8 @t457 @t45)) @t139)))))) % 0.45/0.86 (assume @p306 (forall @t230 (exists (@list @t458) (and (= @t458 @t301) (= (tptp.f36 @t458 @t451) (tptp.f36 (tptp.f37 tptp.f38 (tptp.f36 @t458 @t45)) @t139)))))) % 0.45/0.86 (assume @p307 (forall @t450 (exists (@list @t459) (and (= @t459 @t318) (= (tptp.f15 @t459 @t451) (tptp.f15 (tptp.f40 tptp.f41 (tptp.f15 @t459 @t45)) @t139)))))) % 0.45/0.86 (assume @p308 (forall @t439 (= (tptp.f8 (tptp.f32 tptp.f33 @t44) @t139) (tptp.f3 (tptp.f5 tptp.f6 @t438) @t437)))) % 0.45/0.86 (assume @p309 (forall @t442 (= (tptp.f15 (tptp.f40 tptp.f41 @t131) @t139) (tptp.f22 (tptp.f23 tptp.f25 @t441) @t440)))) % 0.45/0.86 (assume @p310 (forall @t313 (= (tptp.f27 tptp.f30 @t460) (tptp.f11 @t327 @t45)))) % 0.45/0.86 (assume @p311 (forall @t297 (= (tptp.f3 tptp.f19 @t461) (tptp.f8 @t329 @t45)))) % 0.45/0.86 (assume @p312 (forall @t51 (= @t322 (or @t57 @t320)))) % 0.45/0.86 (assume @p313 (forall @t28 (exists (@list @t462) (and (= @t462 @t64) (= (tptp.f36 (tptp.f37 tptp.f38 @t462) @t26) @t462))))) % 0.45/0.86 (assume @p314 (forall @t51 (exists (@list @t463) (and (= @t463 @t64) (= (= @t302 @t463) (or @t320 (= @t26 @t463))))))) % 0.45/0.86 (assume @p315 (forall @t230 (exists (@list @t464) (and (= @t464 @t301) (=> @t57 (=> (< (tptp.f11 tptp.f12 (tptp.f36 @t464 @t45)) (tptp.f11 tptp.f12 (tptp.f36 @t464 @t139))) (< @t50 @t143))))))) % 0.45/0.86 (assume @p316 (forall @t51 (exists (@list @t465) (and (= @t465 @t63) (=> (<= @t465 @t49) (<= @t465 @t321)))))) % 0.45/0.87 (assume @p317 (forall @t313 (exists (@list @t466) (and (= @t466 @t460) (= (tptp.f27 (tptp.f28 tptp.f29 @t466) @t166) (tptp.f27 @t168 @t466)))))) % 0.45/0.87 (assume @p318 (forall @t297 (exists (@list @t467) (and (= @t467 @t461) (= (tptp.f3 (tptp.f5 tptp.f20 @t467) @t19) (tptp.f3 @t103 @t467)))))) % 0.45/0.87 (assume @p319 (forall @t51 (exists (@list @t468) (and (= @t468 @t302) (= (tptp.f36 (tptp.f37 tptp.f39 @t468) @t26) (tptp.f36 @t316 @t468)))))) % 0.45/0.87 (assume @p320 (forall @t319 (exists (@list @t469) (and (= @t469 (tptp.f15 @t318 @t45)) (= (tptp.f22 (tptp.f23 tptp.f24 @t469) @t129) (tptp.f22 @t130 @t469)))))) % 0.45/0.87 (assume @p321 (forall @t445 (exists (@list @t470) (and (= @t470 @t312) (= (tptp.f11 @t470 @t443) (tptp.f27 (tptp.f28 tptp.f29 (tptp.f11 @t470 @t45)) (tptp.f11 @t470 @t139))))))) % 0.45/0.87 (assume @p322 (forall @t447 (exists (@list @t471) (and (= @t471 @t203) (= (tptp.f8 @t471 @t443) (tptp.f3 (tptp.f5 tptp.f20 (tptp.f8 @t471 @t45)) (tptp.f8 @t471 @t139))))))) % 0.45/0.87 (assume @p323 (forall @t230 (exists (@list @t472) (and (= @t472 @t301) (= (tptp.f36 @t472 @t443) (tptp.f36 (tptp.f37 tptp.f39 (tptp.f36 @t472 @t45)) (tptp.f36 @t472 @t139))))))) % 0.45/0.87 (assume @p324 (forall @t450 (exists (@list @t473) (and (= @t473 @t318) (= (tptp.f15 @t473 @t443) (tptp.f22 (tptp.f23 tptp.f24 (tptp.f15 @t473 @t45)) (tptp.f15 @t473 @t139))))))) % 0.45/0.87 (assume @p325 (forall @t313 (exists (@list @t474) (and (= @t474 @t312) (= (tptp.f11 @t474 @t197) (tptp.f27 (tptp.f28 tptp.f29 (tptp.f11 @t474 @t45)) @t166)))))) % 0.45/0.87 (assume @p326 (forall @t297 (exists (@list @t475) (and (= @t475 @t203) (= (tptp.f8 @t475 @t197) (tptp.f3 (tptp.f5 tptp.f20 (tptp.f8 @t475 @t45)) @t19)))))) % 0.45/0.87 (assume @p327 (forall @t51 (exists (@list @t476) (and (= @t476 @t301) (= (tptp.f36 @t476 @t197) (tptp.f36 (tptp.f37 tptp.f39 (tptp.f36 @t476 @t45)) @t26)))))) % 0.45/0.87 (assume @p328 (forall @t319 (exists (@list @t477) (and (= @t477 @t318) (= (tptp.f15 @t477 @t197) (tptp.f22 (tptp.f23 tptp.f24 (tptp.f15 @t477 @t45)) @t129)))))) % 0.45/0.87 (assume @p329 (forall @t313 (exists (@list @t478) (and (= @t478 @t312) (= (tptp.f11 @t478 @t197) (tptp.f27 @t168 (tptp.f11 @t478 @t45))))))) % 0.45/0.87 (assume @p330 (forall @t297 (exists (@list @t479) (and (= @t479 @t203) (= (tptp.f8 @t479 @t197) (tptp.f3 @t103 (tptp.f8 @t479 @t45))))))) % 0.45/0.87 (assume @p331 (forall @t51 (exists (@list @t480) (and (= @t480 @t301) (= (tptp.f36 @t480 @t197) (tptp.f36 @t316 (tptp.f36 @t480 @t45))))))) % 0.45/0.87 (assume @p332 (forall @t319 (exists (@list @t481) (and (= @t481 @t318) (= (tptp.f15 @t481 @t197) (tptp.f22 @t130 (tptp.f15 @t481 @t45))))))) % 0.45/0.87 (assume @p333 (forall @t439 (= (tptp.f15 (tptp.f40 tptp.f41 @t482) @t139) (tptp.f17 (tptp.f42 tptp.f43 @t438) (tptp.f3 @t140 @t32))))) % 0.45/0.87 (assume @p334 (forall @t37 (=> @t263 (exists (@list @t79 @t121 @t484) (and (= @t484 @t112) (= @t32 (tptp.f3 @t484 @t485)) (= @t19 (tptp.f3 @t484 @t483))))))) % 0.45/0.87 (assume @p335 (forall @t23 (= @t191 (tptp.f17 (tptp.f42 tptp.f43 1/1) @t19)))) % 0.45/0.87 (assume @p336 (forall @t123 (= (tptp.f22 (tptp.f23 tptp.f24 @t482) @t486) (tptp.f17 (tptp.f42 tptp.f43 @t109) (+ @t32 @t121))))) % 0.45/0.87 (assume @p337 (forall @t123 (= (tptp.f22 (tptp.f23 tptp.f25 @t482) @t486) (tptp.f17 (tptp.f42 tptp.f43 (tptp.f3 @t43 @t79)) (- @t32 @t121))))) % 0.45/0.87 (assume @p338 (forall @t37 (exists (@list @t79 @t121 @t487) (and (= @t487 @t112) (= @t19 (tptp.f3 @t487 @t485)) (= @t32 (tptp.f3 @t487 @t483)))))) % 0.45/0.87 (assume @p339 (forall @t37 (=> @t67 (exists (@list @t79 @t121 @t488) (and (= @t488 @t112) (= @t32 (tptp.f3 @t488 @t485)) (= @t19 (tptp.f3 @t488 @t483))))))) % 0.45/0.87 (assume @p340 (forall @t179 (= (tptp.f3 tptp.f31 @t177) (tptp.f44 tptp.f45 @t489)))) % 0.45/0.87 (assume @p341 (forall @t179 (= (tptp.f3 tptp.f4 @t177) (tptp.f44 tptp.f46 @t489)))) % 0.45/0.87 (assume @p342 (forall @t424 (= @t496 (and @t495 @t492)))) % 0.45/0.87 (assume @p343 (forall @t424 (=> @t495 (=> @t492 @t496)))) % 0.45/0.87 (assume @p344 (forall @t424 (= (tptp.f44 tptp.f45 @t391) (+ (tptp.f3 @t498 @t490) (tptp.f3 @t497 @t493))))) % 0.45/0.87 (assume @p345 (forall @t424 (= (tptp.f44 tptp.f46 @t391) (- (tptp.f3 @t498 @t493) (tptp.f3 @t497 @t490))))) % 0.45/0.87 (assume @p346 (forall @t23 (= (tptp.f44 tptp.f45 @t191) @t194))) % 0.45/0.87 (assume @p347 (forall @t23 (= (tptp.f44 tptp.f46 @t191) @t20))) % 0.45/0.87 (assume @p348 (forall @t28 (= (tptp.f13 tptp.f14 @t49) @t26))) % 0.45/0.87 (assume @p349 (forall @t174 (=> (<= 0 @t166) (= @t499 @t166)))) % 0.45/0.87 (assume @p350 (forall @t174 (=> (< @t166 0) (= @t499 0)))) % 0.45/0.87 (step @p351 :rule evaluate :args ((not true))) % 0.45/0.87 (step @p352 :rule evaluate :args ((or false true))) % 0.45/0.87 (step @p353 :rule evaluate :args ((and true true))) % 0.45/0.87 (step @p354 :rule evaluate :args ((not false))) % 0.45/0.87 (step @p355 :rule evaluate :args (@t500)) % 0.45/0.87 (step @p356 :rule cong :premises (@p355) :args (@t501)) % 0.45/0.87 (step @p357 :rule trans :premises (@p356 @p354)) % 0.45/0.87 (step @p358 :rule evaluate :args (@t502)) % 0.45/0.87 (step @p359 :rule nary_cong :premises (@p358 @p357) :args (@t503)) % 0.45/0.87 (step @p360 :rule trans :premises (@p359 @p353)) % 0.45/0.87 (step @p361 :rule evaluate :args ((and false true))) % 0.45/0.87 (step @p362 :rule evaluate :args (@t504)) % 0.45/0.87 (step @p363 :rule cong :premises (@p362) :args (@t505)) % 0.45/0.87 (step @p364 :rule trans :premises (@p363 @p354)) % 0.45/0.87 (step @p365 :rule cong :premises (@p358) :args (@t506)) % 0.45/0.87 (step @p366 :rule trans :premises (@p365 @p351)) % 0.45/0.87 (step @p367 :rule nary_cong :premises (@p366 @p364) :args (@t507)) % 0.45/0.87 (step @p368 :rule trans :premises (@p367 @p361)) % 0.45/0.87 (step @p369 :rule nary_cong :premises (@p368 @p360) :args (@t508)) % 0.45/0.87 (step @p370 :rule trans :premises (@p369 @p352)) % 0.45/0.87 (step @p371 :rule cong :premises (@p370) :args ((not @t508))) % 0.45/0.87 (step @p372 :rule trans :premises (@p371 @p351)) % 0.45/0.87 (step @p373 :rule refl :args (1/1)) % 0.45/0.87 (step @p374 :rule cong :premises (@p3 @p373) :args (@t509)) % 0.45/0.87 (step @p375 :rule cong :premises (@p374) :args (@t510)) % 0.45/0.87 (step @p376 :rule refl :args (0/1)) % 0.45/0.87 (step @p377 :rule cong :premises (@p3 @p376) :args (@t511)) % 0.45/0.87 (step @p378 :rule nary_cong :premises (@p377 @p375) :args (@t512)) % 0.45/0.87 (step @p379 :rule refl :args (-1/1)) % 0.45/0.87 (step @p380 :rule cong :premises (@p3 @p379) :args (@t513)) % 0.45/0.87 (step @p381 :rule cong :premises (@p380) :args (@t514)) % 0.45/0.87 (step @p382 :rule cong :premises (@p377) :args (@t515)) % 0.45/0.87 (step @p383 :rule nary_cong :premises (@p382 @p381) :args (@t516)) % 0.45/0.87 (step @p384 :rule nary_cong :premises (@p383 @p378) :args (@t517)) % 0.45/0.87 (step @p385 :rule cong :premises (@p384) :args ((not @t517))) % 0.45/0.87 (step @p386 :rule trans :premises (@p385 @p372)) % 0.45/0.87 (step @p387 :rule aci_norm :args ((= (or false @t516 @t512) @t517))) % 0.45/0.87 (step @p388 :rule refl :args (@t512)) % 0.45/0.87 (step @p389 :rule refl :args (@t516)) % 0.45/0.87 (step @p390 :rule eq-refl :args (@t3)) % 0.45/0.87 (step @p391 :rule cong :premises (@p390) :args (@t518)) % 0.45/0.87 (step @p392 :rule trans :premises (@p391 @p351)) % 0.45/0.87 (step @p393 :rule nary_cong :premises (@p392 @p389 @p388) :args (@t519)) % 0.45/0.87 (step @p394 :rule trans :premises (@p393 @p387)) % 0.45/0.87 (step @p395 :rule quant-var-elim-eq :args ((= (forall @t14 @t526) @t519))) % 0.45/0.87 (step @p396 :rule aci_norm :args ((= @t527 @t526))) % 0.45/0.87 (step @p397 :rule cong :premises (@p396) :args ((forall @t14 @t527))) % 0.45/0.87 (step @p398 :rule trans :premises (@p397 @p395)) % 0.45/0.87 (step @p399 :rule trans :premises (@p398 @p394)) % 0.45/0.87 (step @p400 :rule bool-implies-de-morgan :args (@t520 @t5)) % 0.45/0.87 (step @p401 :rule bool-implies-de-morgan :args (@t523 @t522)) % 0.45/0.87 (step @p402 :rule refl :args (@t525)) % 0.45/0.87 (step @p403 :rule nary_cong :premises (@p402 @p401 @p400) :args (@t532)) % 0.45/0.87 (step @p404 :rule aci_norm :args ((= (or @t525 (or @t531 @t529)) @t532))) % 0.45/0.87 (step @p405 :rule bool-and-de-morgan :args (@t530 @t528 true)) % 0.45/0.87 (step @p406 :rule nary_cong :premises (@p402 @p405) :args ((or @t525 (not (and @t530 @t528))))) % 0.45/0.87 (step @p407 :rule bool-and-de-morgan :args (@t12 @t530 (and @t528))) % 0.45/0.87 (step @p408 :rule trans :premises (@p407 @p406)) % 0.45/0.87 (step @p409 :rule trans :premises (@p408 @p404)) % 0.45/0.87 (step @p410 :rule trans :premises (@p409 @p403)) % 0.45/0.87 (step @p411 :rule cong :premises (@p410) :args (@t534)) % 0.45/0.87 (step @p412 :rule trans :premises (@p411 @p399)) % 0.45/0.87 (step @p413 :rule cong :premises (@p412) :args (@t535)) % 0.45/0.87 (step @p414 :rule exists-elim :args ((= (exists @t14 @t533) @t535))) % 0.45/0.87 (step @p415 :rule trans :premises (@p414 @p413)) % 0.45/0.87 (step @p416 :rule refl :args (@t5)) % 0.45/0.87 (step @p417 :rule bool-double-not-elim :args (@t520)) % 0.45/0.87 (step @p418 :rule arith-elim-lt :args (@t4 0/1)) % 0.45/0.87 (step @p419 :rule cong :premises (@p418) :args (@t7)) % 0.45/0.87 (step @p420 :rule trans :premises (@p419 @p417)) % 0.45/0.87 (step @p421 :rule cong :premises (@p420 @p416) :args (@t8)) % 0.45/0.87 (step @p422 :rule arith_poly_norm :args ((= (* 1/1 (- @t536 1/1)) (* -1/1 (- @t4 -1/1))))) % 0.45/0.87 (step @p423 :rule arith_poly_norm_rel :premises (@p422) :args ((= (= @t536 1/1) @t522))) % 0.45/0.87 (step @p424 :rule arith_poly_norm :args ((= @t9 @t536))) % 0.45/0.87 (step @p425 :rule cong :premises (@p424 @p373) :args (@t10)) % 0.45/0.87 (step @p426 :rule trans :premises (@p425 @p423)) % 0.45/0.87 (step @p427 :rule cong :premises (@p418 @p426) :args (@t11)) % 0.45/0.87 (step @p428 :rule refl :args (@t12)) % 0.45/0.87 (step @p429 :rule nary_cong :premises (@p428 @p427 @p421) :args (@t13)) % 0.45/0.87 (step @p430 :rule cong :premises (@p429) :args (@t15)) % 0.45/0.87 (step @p431 :rule trans :premises (@p430 @p415)) % 0.45/0.87 (step @p432 :rule trans :premises (@p431 @p386)) % 0.45/0.87 (step @p433 false :rule eq_resolve :premises (@p4 @p432)) % 0.45/0.87 ) % 0.45/0.87 % SZS output end Proof % 0.45/0.87 % cvc5 exiting %------------------------------------------------------------------------------