%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : SWW822_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 : n015.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.53s 1.01s % Output : Proof 0.86s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW822_1 : TPTP v9.2.1. Released v7.0.0. % 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.16/0.34 % Computer : n015.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Tue Jun 2 22:32:49 EDT 2026 % 0.16/0.35 % CPUTime : % 0.41/0.68 %----Proving TF0_ARI % 0.41/0.69 --- Run --finite-model-find --decision=internal at 45... % 0.53/1.01 % SZS status Unsatisfiable % 0.53/1.01 % SZS output start Proof % 0.86/1.04 ( % 0.86/1.04 (declare-sort |tptp.'S26'| 0) % 0.86/1.04 (declare-sort |tptp.'S10'| 0) % 0.86/1.04 (declare-sort |tptp.'S12'| 0) % 0.86/1.04 (declare-sort |tptp.'S4'| 0) % 0.86/1.04 (declare-sort |tptp.'S7'| 0) % 0.86/1.04 (declare-sort |tptp.'S6'| 0) % 0.86/1.04 (declare-sort |tptp.'S8'| 0) % 0.86/1.04 (declare-sort |tptp.'S5'| 0) % 0.86/1.04 (declare-sort |tptp.'S24'| 0) % 0.86/1.04 (declare-sort |tptp.'S22'| 0) % 0.86/1.04 (declare-sort |tptp.'S2'| 0) % 0.86/1.04 (declare-sort |tptp.'S1'| 0) % 0.86/1.04 (declare-sort |tptp.'S3'| 0) % 0.86/1.04 (declare-sort |tptp.'S11'| 0) % 0.86/1.04 (declare-sort |tptp.'S13'| 0) % 0.86/1.04 (declare-sort |tptp.'S9'| 0) % 0.86/1.04 (declare-sort |tptp.'S14'| 0) % 0.86/1.04 (declare-sort |tptp.'S15'| 0) % 0.86/1.04 (declare-sort |tptp.'S16'| 0) % 0.86/1.04 (declare-sort |tptp.'S17'| 0) % 0.86/1.04 (declare-sort |tptp.'S18'| 0) % 0.86/1.04 (declare-sort |tptp.'S19'| 0) % 0.86/1.04 (declare-sort |tptp.'S20'| 0) % 0.86/1.04 (declare-sort |tptp.'S21'| 0) % 0.86/1.04 (declare-sort |tptp.'S23'| 0) % 0.86/1.04 (declare-sort |tptp.'S25'| 0) % 0.86/1.04 (declare-const tptp.f66 (-> |tptp.'S26'| |tptp.'S10'| |tptp.'S9'|)) % 0.86/1.04 (declare-const tptp.f67 |tptp.'S26'|) % 0.86/1.04 (declare-const tptp.f65 |tptp.'S4'|) % 0.86/1.04 (declare-const tptp.f63 (-> |tptp.'S25'| Int |tptp.'S8'|)) % 0.86/1.04 (declare-const tptp.f64 |tptp.'S25'|) % 0.86/1.04 (declare-const tptp.f62 |tptp.'S17'|) % 0.86/1.04 (declare-const tptp.f61 |tptp.'S18'|) % 0.86/1.04 (declare-const tptp.f59 (-> |tptp.'S24'| Real |tptp.'S13'|)) % 0.86/1.04 (declare-const tptp.f29 |tptp.'S15'|) % 0.86/1.04 (declare-const tptp.f25 (-> |tptp.'S15'| |tptp.'S10'| |tptp.'S2'|)) % 0.86/1.04 (declare-const tptp.f24 |tptp.'S3'|) % 0.86/1.04 (declare-const tptp.f26 |tptp.'S15'|) % 0.86/1.04 (declare-const tptp.f13 (-> |tptp.'S9'| |tptp.'S2'| |tptp.'S10'|)) % 0.86/1.04 (declare-const tptp.f17 (-> |tptp.'S12'| Real |tptp.'S11'|)) % 0.86/1.04 (declare-const tptp.f14 |tptp.'S9'|) % 0.86/1.04 (declare-const tptp.f16 (-> |tptp.'S11'| Real |tptp.'S10'|)) % 0.86/1.04 (declare-const tptp.f9 (-> |tptp.'S7'| Int |tptp.'S6'|)) % 0.86/1.04 (declare-const tptp.f27 (-> |tptp.'S16'| |tptp.'S10'| Real)) % 0.86/1.04 (declare-const tptp.f40 |tptp.'S18'|) % 0.86/1.04 (declare-const tptp.f21 |tptp.'S6'|) % 0.86/1.04 (declare-const tptp.f23 |tptp.'S14'|) % 0.86/1.04 (declare-const tptp.f18 |tptp.'S12'|) % 0.86/1.04 (declare-const tptp.f32 |tptp.'S11'|) % 0.86/1.04 (declare-const tptp.f20 |tptp.'S13'|) % 0.86/1.04 (declare-const tptp.f2 |tptp.'S1'|) % 0.86/1.04 (declare-const tptp.f7 |tptp.'S5'|) % 0.86/1.04 (declare-const tptp.f4 (-> |tptp.'S4'| |tptp.'S2'| |tptp.'S3'|)) % 0.86/1.04 (declare-const tptp.f1 |tptp.'S1'|) % 0.86/1.04 (declare-const tptp.f12 |tptp.'S8'|) % 0.86/1.04 (declare-const tptp.f19 (-> |tptp.'S13'| |tptp.'S2'| Real)) % 0.86/1.04 (declare-const tptp.f11 (-> |tptp.'S8'| |tptp.'S2'| Int)) % 0.86/1.04 (declare-const tptp.f28 |tptp.'S16'|) % 0.86/1.04 (declare-const tptp.f57 (-> |tptp.'S21'| |tptp.'S10'| |tptp.'S1'|)) % 0.86/1.04 (declare-const tptp.f3 (-> |tptp.'S3'| |tptp.'S2'| |tptp.'S2'|)) % 0.86/1.04 (declare-const tptp.f10 |tptp.'S7'|) % 0.86/1.04 (declare-const tptp.f22 (-> |tptp.'S14'| Real Real)) % 0.86/1.04 (declare-const tptp.f6 (-> |tptp.'S5'| Int |tptp.'S2'|)) % 0.86/1.04 (declare-const tptp.f5 |tptp.'S4'|) % 0.86/1.04 (declare-const tptp.f8 (-> |tptp.'S6'| Int Int)) % 0.86/1.04 (declare-const tptp.f36 |tptp.'S16'|) % 0.86/1.04 (declare-const tptp.f15 |tptp.'S2'|) % 0.86/1.04 (declare-const tptp.f30 |tptp.'S14'|) % 0.86/1.04 (declare-const tptp.f31 |tptp.'S16'|) % 0.86/1.04 (declare-const tptp.f33 |tptp.'S14'|) % 0.86/1.04 (declare-const tptp.f35 |tptp.'S17'|) % 0.86/1.04 (declare-const tptp.f34 (-> |tptp.'S17'| |tptp.'S10'| |tptp.'S10'|)) % 0.86/1.04 (declare-const tptp.f37 (-> |tptp.'S17'| |tptp.'S1'|)) % 0.86/1.04 (declare-const tptp.f38 (-> |tptp.'S16'| |tptp.'S1'|)) % 0.86/1.04 (declare-const tptp.f39 (-> |tptp.'S18'| |tptp.'S10'| |tptp.'S17'|)) % 0.86/1.04 (declare-const tptp.f42 |tptp.'S19'|) % 0.86/1.04 (declare-const tptp.f41 (-> Int |tptp.'S19'| |tptp.'S1'|)) % 0.86/1.04 (declare-const tptp.f44 |tptp.'S20'|) % 0.86/1.04 (declare-const tptp.f43 (-> Real |tptp.'S20'| |tptp.'S1'|)) % 0.86/1.04 (declare-const tptp.f46 |tptp.'S21'|) % 0.86/1.04 (declare-const tptp.f45 (-> |tptp.'S10'| |tptp.'S21'| |tptp.'S1'|)) % 0.86/1.04 (declare-const tptp.f48 |tptp.'S22'|) % 0.86/1.04 (declare-const tptp.f47 (-> |tptp.'S2'| |tptp.'S22'| |tptp.'S1'|)) % 0.86/1.04 (declare-const tptp.f50 |tptp.'S23'|) % 0.86/1.04 (declare-const tptp.f49 (-> |tptp.'S23'| Real |tptp.'S14'|)) % 0.86/1.04 (declare-const tptp.f51 |tptp.'S10'|) % 0.86/1.04 (declare-const tptp.f52 |tptp.'S18'|) % 0.86/1.04 (declare-const tptp.f53 |tptp.'S4'|) % 0.86/1.04 (declare-const tptp.f54 |tptp.'S4'|) % 0.86/1.04 (declare-const tptp.f55 (-> |tptp.'S19'| Int |tptp.'S1'|)) % 0.86/1.04 (declare-const tptp.f56 (-> |tptp.'S20'| Real |tptp.'S1'|)) % 0.86/1.04 (declare-const tptp.f58 (-> |tptp.'S22'| |tptp.'S2'| |tptp.'S1'|)) % 0.86/1.04 (declare-const tptp.f60 |tptp.'S24'|) % 0.86/1.04 (define @t1 () (@var "A__questionmark_v1" |tptp.'S2'|)) % 0.86/1.04 (define @t2 () (tptp.f11 tptp.f12 @t1)) % 0.86/1.04 (define @t3 () (@var "A__questionmark_v0" |tptp.'S2'|)) % 0.86/1.04 (define @t4 () (tptp.f11 tptp.f12 @t3)) % 0.86/1.04 (define @t5 () (tptp.f9 tptp.f10 @t4)) % 0.86/1.04 (define @t6 () (tptp.f8 @t5 @t2)) % 0.86/1.04 (define @t7 () (tptp.f6 tptp.f7 @t6)) % 0.86/1.04 (define @t8 () (@list @t3 @t1)) % 0.86/1.04 (define @t9 () (tptp.f19 tptp.f20 tptp.f15)) % 0.86/1.04 (define @t10 () (tptp.f13 tptp.f14 tptp.f15)) % 0.86/1.04 (define @t11 () (= @t10 (tptp.f16 (tptp.f17 tptp.f18 @t9) 0/1))) % 0.86/1.04 (define @t12 () (not @t11)) % 0.86/1.04 (define @t13 () (@var "A__questionmark_v3" Real)) % 0.86/1.04 (define @t14 () (@var "A__questionmark_v1" Real)) % 0.86/1.04 (define @t15 () (= @t14 @t13)) % 0.86/1.04 (define @t16 () (@var "A__questionmark_v2" Real)) % 0.86/1.04 (define @t17 () (@var "A__questionmark_v0" Real)) % 0.86/1.04 (define @t18 () (= @t17 @t16)) % 0.86/1.04 (define @t19 () (tptp.f16 (tptp.f17 tptp.f18 @t16) @t13)) % 0.86/1.04 (define @t20 () (tptp.f17 tptp.f18 @t17)) % 0.86/1.04 (define @t21 () (tptp.f16 @t20 @t14)) % 0.86/1.04 (define @t22 () (@list @t17 @t14 @t16 @t13)) % 0.86/1.04 (define @t23 () (@var "A__questionmark_v_0_1" Int)) % 0.86/1.04 (define @t24 () (@list @t3)) % 0.86/1.04 (define @t25 () (@var "A__questionmark_v_0_2" Real)) % 0.86/1.04 (define @t26 () (tptp.f19 tptp.f20 @t3)) % 0.86/1.04 (define @t27 () (= @t3 @t1)) % 0.86/1.04 (define @t28 () (tptp.f19 tptp.f20 @t1)) % 0.86/1.04 (define @t29 () (tptp.f13 tptp.f14 @t1)) % 0.86/1.04 (define @t30 () (tptp.f13 tptp.f14 @t3)) % 0.86/1.04 (define @t31 () (tptp.f3 tptp.f24 @t1)) % 0.86/1.04 (define @t32 () (tptp.f3 tptp.f24 @t3)) % 0.86/1.04 (define @t33 () (tptp.f6 tptp.f7 0)) % 0.86/1.04 (define @t34 () (@list @t17 @t14)) % 0.86/1.04 (define @t35 () (tptp.f27 tptp.f28 @t30)) % 0.86/1.04 (define @t36 () (= @t35 @t26)) % 0.86/1.04 (define @t37 () (forall @t24 @t36)) % 0.86/1.04 (define @t38 () (tptp.f16 (tptp.f17 tptp.f18 @t14) @t16)) % 0.86/1.04 (define @t39 () (@var "A__questionmark_v0" |tptp.'S10'|)) % 0.86/1.04 (define @t40 () (@list @t14 @t16)) % 0.86/1.04 (define @t41 () (@list @t39)) % 0.86/1.04 (define @t42 () (@var "A__questionmark_v_0_3" Real)) % 0.86/1.04 (define @t43 () (@var "A__questionmark_v_0_4" Real)) % 0.86/1.04 (define @t44 () (@var "A__questionmark_v_0_5" |tptp.'S10'|)) % 0.86/1.04 (define @t45 () (tptp.f22 tptp.f30 @t17)) % 0.86/1.04 (define @t46 () (@list @t17)) % 0.86/1.04 (define @t47 () (tptp.f27 tptp.f31 @t39)) % 0.86/1.04 (define @t48 () (tptp.f27 tptp.f28 @t39)) % 0.86/1.04 (define @t49 () (tptp.f16 tptp.f32 @t17)) % 0.86/1.04 (define @t50 () (tptp.f34 tptp.f35 @t39)) % 0.86/1.04 (define @t51 () (@var "A__questionmark_v_0_6" |tptp.'S10'|)) % 0.86/1.04 (define @t52 () (@var "A__questionmark_v_0_7" Real)) % 0.86/1.04 (define @t53 () (< @t52 0/1)) % 0.86/1.04 (define @t54 () (@var "A__questionmark_v_0_8" Real)) % 0.86/1.04 (define @t55 () (< @t54 0/1)) % 0.86/1.04 (define @t56 () (tptp.f27 tptp.f31 @t49)) % 0.86/1.04 (define @t57 () (< @t17 0/1)) % 0.86/1.04 (define @t58 () (not @t57)) % 0.86/1.04 (define @t59 () (- @t17)) % 0.86/1.04 (define @t60 () (tptp.f22 tptp.f33 @t17)) % 0.86/1.04 (define @t61 () (tptp.f22 tptp.f30 @t60)) % 0.86/1.04 (define @t62 () (@var "A__questionmark_v_0_9" Real)) % 0.86/1.04 (define @t63 () (< @t62 0/1)) % 0.86/1.04 (define @t64 () (@var "A__questionmark_v1" |tptp.'S10'|)) % 0.86/1.04 (define @t65 () (= @t39 @t64)) % 0.86/1.04 (define @t66 () (tptp.f34 tptp.f35 @t64)) % 0.86/1.04 (define @t67 () (@list @t39 @t64)) % 0.86/1.04 (define @t68 () (= @t17 @t14)) % 0.86/1.04 (define @t69 () (tptp.f16 tptp.f32 @t14)) % 0.86/1.04 (define @t70 () (tptp.f22 tptp.f33 @t14)) % 0.86/1.04 (define @t71 () (tptp.f16 tptp.f32 @t16)) % 0.86/1.04 (define @t72 () (@list @t17 @t14 @t16)) % 0.86/1.04 (define @t73 () (- @t14)) % 0.86/1.04 (define @t74 () (@var "A__questionmark_v_0_10" |tptp.'S11'|)) % 0.86/1.04 (define @t75 () (tptp.f27 tptp.f36 @t39)) % 0.86/1.04 (define @t76 () (- @t75)) % 0.86/1.04 (define @t77 () (tptp.f17 tptp.f18 @t48)) % 0.86/1.04 (define @t78 () (tptp.f39 tptp.f40 @t39)) % 0.86/1.04 (define @t79 () (tptp.f16 @t77 @t75)) % 0.86/1.04 (define @t80 () (forall @t41 (= @t79 @t39))) % 0.86/1.04 (define @t81 () (tptp.f22 tptp.f30 @t14)) % 0.86/1.04 (define @t82 () (tptp.f49 tptp.f50 @t81)) % 0.86/1.04 (define @t83 () (tptp.f22 @t82 @t17)) % 0.86/1.04 (define @t84 () (@list @t14)) % 0.86/1.04 (define @t85 () (forall @t84 (<= (tptp.f27 tptp.f31 @t69) @t83))) % 0.86/1.04 (define @t86 () (forall @t84 (<= (tptp.f22 tptp.f30 @t70) @t83))) % 0.86/1.04 (define @t87 () (< 0/1 @t17)) % 0.86/1.04 (define @t88 () (<= 0/1 @t17)) % 0.86/1.04 (define @t89 () (tptp.f17 tptp.f18 0/1)) % 0.86/1.04 (define @t90 () (@var "A__questionmark_v_0_11" Real)) % 0.86/1.04 (define @t91 () (< @t90 0/1)) % 0.86/1.04 (define @t92 () (@var "A__questionmark_v_0_12" Real)) % 0.86/1.04 (define @t93 () (tptp.f27 tptp.f36 @t64)) % 0.86/1.04 (define @t94 () (+ @t75 @t93)) % 0.86/1.04 (define @t95 () (tptp.f34 @t78 @t64)) % 0.86/1.04 (define @t96 () (@var "A__questionmark_v_0_13" |tptp.'S14'|)) % 0.86/1.04 (define @t97 () (+ @t14 @t16)) % 0.86/1.04 (define @t98 () (tptp.f49 tptp.f50 @t17)) % 0.86/1.04 (define @t99 () (@var "A__questionmark_v2" |tptp.'S10'|)) % 0.86/1.04 (define @t100 () (@var "A__questionmark_v_0_14" |tptp.'S17'|)) % 0.86/1.04 (define @t101 () (tptp.f39 tptp.f40 @t64)) % 0.86/1.04 (define @t102 () (tptp.f34 @t101 @t99)) % 0.86/1.04 (define @t103 () (tptp.f39 tptp.f52 @t39)) % 0.86/1.04 (define @t104 () (@list @t39 @t64 @t99)) % 0.86/1.04 (define @t105 () (@var "A__questionmark_v_0_15" |tptp.'S14'|)) % 0.86/1.04 (define @t106 () (@var "A__questionmark_v_0_16" |tptp.'S17'|)) % 0.86/1.04 (define @t107 () (tptp.f27 tptp.f31 @t64)) % 0.86/1.04 (define @t108 () (tptp.f27 tptp.f31 @t95)) % 0.86/1.04 (define @t109 () (tptp.f49 tptp.f50 @t14)) % 0.86/1.04 (define @t110 () (tptp.f22 @t109 @t16)) % 0.86/1.04 (define @t111 () (tptp.f22 @t98 @t16)) % 0.86/1.04 (define @t112 () (+ @t17 @t14)) % 0.86/1.04 (define @t113 () (tptp.f39 tptp.f52 @t64)) % 0.86/1.04 (define @t114 () (tptp.f34 @t113 @t99)) % 0.86/1.04 (define @t115 () (tptp.f34 @t103 @t99)) % 0.86/1.04 (define @t116 () (= (tptp.f45 @t64 tptp.f46) tptp.f1)) % 0.86/1.04 (define @t117 () (= (tptp.f45 @t39 tptp.f46) tptp.f1)) % 0.86/1.04 (define @t118 () (= (tptp.f43 @t14 tptp.f44) tptp.f1)) % 0.86/1.04 (define @t119 () (= (tptp.f43 @t17 tptp.f44) tptp.f1)) % 0.86/1.04 (define @t120 () (@var "A__questionmark_v1" Int)) % 0.86/1.04 (define @t121 () (@var "A__questionmark_v0" Int)) % 0.86/1.04 (define @t122 () (+ @t121 @t120)) % 0.86/1.04 (define @t123 () (= (tptp.f41 @t120 tptp.f42) tptp.f1)) % 0.86/1.04 (define @t124 () (= (tptp.f41 @t121 tptp.f42) tptp.f1)) % 0.86/1.04 (define @t125 () (@list @t121 @t120)) % 0.86/1.04 (define @t126 () (tptp.f4 tptp.f53 @t3)) % 0.86/1.04 (define @t127 () (tptp.f3 @t126 @t1)) % 0.86/1.04 (define @t128 () (= (tptp.f47 @t1 tptp.f48) tptp.f1)) % 0.86/1.04 (define @t129 () (= (tptp.f47 @t3 tptp.f48) tptp.f1)) % 0.86/1.04 (define @t130 () (tptp.f4 tptp.f54 @t3)) % 0.86/1.04 (define @t131 () (tptp.f3 @t130 @t1)) % 0.86/1.04 (define @t132 () (tptp.f22 @t98 @t14)) % 0.86/1.04 (define @t133 () (tptp.f9 tptp.f10 @t121)) % 0.86/1.04 (define @t134 () (tptp.f8 @t133 @t120)) % 0.86/1.04 (define @t135 () (tptp.f34 @t103 @t64)) % 0.86/1.04 (define @t136 () (@var "A__questionmark_v_0_17" Int)) % 0.86/1.04 (define @t137 () (tptp.f22 @t109 @t13)) % 0.86/1.04 (define @t138 () (tptp.f22 tptp.f30 @t111)) % 0.86/1.04 (define @t139 () (tptp.f22 tptp.f30 @t16)) % 0.86/1.04 (define @t140 () (< @t139 @t13)) % 0.86/1.04 (define @t141 () (< @t45 @t14)) % 0.86/1.04 (define @t142 () (tptp.f27 tptp.f31 @t115)) % 0.86/1.04 (define @t143 () (tptp.f27 tptp.f31 @t99)) % 0.86/1.04 (define @t144 () (< @t143 @t13)) % 0.86/1.04 (define @t145 () (< @t47 @t14)) % 0.86/1.04 (define @t146 () (@list @t39 @t14 @t99 @t13)) % 0.86/1.04 (define @t147 () (tptp.f22 (tptp.f49 tptp.f50 @t45) @t81)) % 0.86/1.04 (define @t148 () (tptp.f22 tptp.f30 @t132)) % 0.86/1.04 (define @t149 () (tptp.f22 (tptp.f49 tptp.f50 @t47) @t107)) % 0.86/1.04 (define @t150 () (tptp.f27 tptp.f31 @t135)) % 0.86/1.04 (define @t151 () (tptp.f39 tptp.f52 @t49)) % 0.86/1.04 (define @t152 () (tptp.f27 tptp.f28 @t64)) % 0.86/1.04 (define @t153 () (+ @t48 @t152)) % 0.86/1.04 (define @t154 () (+ @t4 @t2)) % 0.86/1.04 (define @t155 () (tptp.f6 tptp.f7 @t154)) % 0.86/1.04 (define @t156 () (@var "A__questionmark_v_0_18" Int)) % 0.86/1.04 (define @t157 () (+ @t14 @t13)) % 0.86/1.04 (define @t158 () (tptp.f34 @t78 @t99)) % 0.86/1.04 (define @t159 () (+ @t17 @t16)) % 0.86/1.04 (define @t160 () (- @t47 @t107)) % 0.86/1.04 (define @t161 () (tptp.f22 tptp.f30 @t112)) % 0.86/1.04 (define @t162 () (- @t45 @t81)) % 0.86/1.04 (define @t163 () (+ @t47 @t107)) % 0.86/1.04 (define @t164 () (+ @t45 @t81)) % 0.86/1.04 (define @t165 () (= @t75 @t93)) % 0.86/1.04 (define @t166 () (= @t48 @t152)) % 0.86/1.04 (define @t167 () (tptp.f39 tptp.f40 @t49)) % 0.86/1.04 (define @t168 () (tptp.f17 tptp.f18 @t159)) % 0.86/1.04 (define @t169 () (tptp.f39 tptp.f40 @t21)) % 0.86/1.04 (define @t170 () (@var "A__questionmark_v1" |tptp.'S19'|)) % 0.86/1.04 (define @t171 () (= (tptp.f55 @t170 @t121) tptp.f1)) % 0.86/1.04 (define @t172 () (@list @t121 @t170)) % 0.86/1.04 (define @t173 () (@var "A__questionmark_v1" |tptp.'S20'|)) % 0.86/1.04 (define @t174 () (= (tptp.f56 @t173 @t17) tptp.f1)) % 0.86/1.04 (define @t175 () (@list @t17 @t173)) % 0.86/1.04 (define @t176 () (@var "A__questionmark_v1" |tptp.'S21'|)) % 0.86/1.04 (define @t177 () (= (tptp.f57 @t176 @t39) tptp.f1)) % 0.86/1.04 (define @t178 () (@list @t39 @t176)) % 0.86/1.04 (define @t179 () (= @t17 0/1)) % 0.86/1.04 (define @t180 () (tptp.f49 tptp.f50 @t107)) % 0.86/1.04 (define @t181 () (tptp.f22 @t180 @t17)) % 0.86/1.04 (define @t182 () (@list @t64)) % 0.86/1.04 (define @t183 () (forall @t182 (<= (tptp.f22 tptp.f30 @t93) @t181))) % 0.86/1.04 (define @t184 () (forall @t182 (<= (tptp.f22 tptp.f30 @t152) @t181))) % 0.86/1.04 (define @t185 () (forall @t182 (<= (tptp.f27 tptp.f31 @t66) @t181))) % 0.86/1.04 (define @t186 () (@var "A__questionmark_v_0_19" Int)) % 0.86/1.04 (define @t187 () (@var "A__questionmark_v_0_20" Int)) % 0.86/1.04 (define @t188 () (@var "A__questionmark_v_1_21" |tptp.'S6'|)) % 0.86/1.04 (define @t189 () (@var "A__questionmark_v_1_23" Int)) % 0.86/1.04 (define @t190 () (@var "A__questionmark_v_0_22" Int)) % 0.86/1.04 (define @t191 () (@var "A__questionmark_v_0_24" |tptp.'S2'|)) % 0.86/1.04 (define @t192 () (tptp.f6 tptp.f7 1)) % 0.86/1.04 (define @t193 () (@var "A__questionmark_v_1_25" Int)) % 0.86/1.04 (define @t194 () (@var "A__questionmark_v_0_26" Int)) % 0.86/1.04 (define @t195 () (@var "A__questionmark_v_2_29" Int)) % 0.86/1.04 (define @t196 () (@var "A__questionmark_v_1_28" |tptp.'S6'|)) % 0.86/1.04 (define @t197 () (@var "A__questionmark_v_0_27" Int)) % 0.86/1.04 (define @t198 () (@var "A__questionmark_v_2_32" Int)) % 0.86/1.04 (define @t199 () (@var "A__questionmark_v_0_30" |tptp.'S6'|)) % 0.86/1.04 (define @t200 () (@var "A__questionmark_v_1_31" Int)) % 0.86/1.04 (define @t201 () (@var "A__questionmark_v2" |tptp.'S2'|)) % 0.86/1.04 (define @t202 () (tptp.f11 tptp.f12 @t201)) % 0.86/1.04 (define @t203 () (@list @t3 @t1 @t201)) % 0.86/1.04 (define @t204 () (@var "A__questionmark_v_2_34" Int)) % 0.86/1.04 (define @t205 () (@var "A__questionmark_v_0_33" |tptp.'S6'|)) % 0.86/1.04 (define @t206 () (@var "A__questionmark_v_1_35" Int)) % 0.86/1.04 (define @t207 () (@var "A__questionmark_v_2_37" Int)) % 0.86/1.04 (define @t208 () (@var "A__questionmark_v_0_38" Int)) % 0.86/1.04 (define @t209 () (@var "A__questionmark_v_1_36" Int)) % 0.86/1.04 (define @t210 () (+ 0 1)) % 0.86/1.04 (define @t211 () (@var "A__questionmark_v_0_40" Int)) % 0.86/1.04 (define @t212 () (@var "A__questionmark_v_1_39" Int)) % 0.86/1.04 (define @t213 () (@var "A__questionmark_v_0_41" |tptp.'S2'|)) % 0.86/1.04 (define @t214 () (@var "A__questionmark_v_0_42" |tptp.'S2'|)) % 0.86/1.04 (define @t215 () (@var "A__questionmark_v_2_45" Int)) % 0.86/1.04 (define @t216 () (@var "A__questionmark_v_1_44" Int)) % 0.86/1.04 (define @t217 () (@var "A__questionmark_v_0_43" |tptp.'S6'|)) % 0.86/1.04 (define @t218 () (@var "A__questionmark_v_1_48" Int)) % 0.86/1.04 (define @t219 () (@var "A__questionmark_v_2_47" Int)) % 0.86/1.04 (define @t220 () (@var "A__questionmark_v_0_46" Int)) % 0.86/1.04 (define @t221 () (@var "A__questionmark_v_1_51" Int)) % 0.86/1.04 (define @t222 () (@var "A__questionmark_v_2_49" Int)) % 0.86/1.04 (define @t223 () (@var "A__questionmark_v_0_50" Int)) % 0.86/1.04 (define @t224 () (@var "A__questionmark_v_0_52" |tptp.'S2'|)) % 0.86/1.04 (define @t225 () (tptp.f6 tptp.f7 @t210)) % 0.86/1.04 (define @t226 () (@var "A__questionmark_v_3_55" Int)) % 0.86/1.04 (define @t227 () (@var "A__questionmark_v_2_56" Int)) % 0.86/1.04 (define @t228 () (@var "A__questionmark_v_1_53" Int)) % 0.86/1.04 (define @t229 () (@var "A__questionmark_v_0_54" |tptp.'S6'|)) % 0.86/1.04 (define @t230 () (@var "A__questionmark_v_2_57" Int)) % 0.86/1.04 (define @t231 () (@var "A__questionmark_v_1_59" Int)) % 0.86/1.04 (define @t232 () (@var "A__questionmark_v_0_58" Int)) % 0.86/1.04 (define @t233 () (@var "A__questionmark_v_3_62" Int)) % 0.86/1.04 (define @t234 () (@var "A__questionmark_v_2_63" Int)) % 0.86/1.04 (define @t235 () (@var "A__questionmark_v_1_60" Int)) % 0.86/1.04 (define @t236 () (@var "A__questionmark_v_0_61" |tptp.'S6'|)) % 0.86/1.04 (define @t237 () (@var "A__questionmark_v_2_64" Int)) % 0.86/1.04 (define @t238 () (@var "A__questionmark_v_1_66" Int)) % 0.86/1.04 (define @t239 () (@var "A__questionmark_v_0_65" Int)) % 0.86/1.04 (define @t240 () (= @t3 @t33)) % 0.86/1.04 (define @t241 () (= @t1 @t201)) % 0.86/1.04 (define @t242 () (@var "A__questionmark_v_0_67" |tptp.'S6'|)) % 0.86/1.04 (define @t243 () (= @t1 @t33)) % 0.86/1.04 (define @t244 () (= @t3 @t201)) % 0.86/1.04 (define @t245 () (@var "A__questionmark_v_0_68" Int)) % 0.86/1.04 (define @t246 () (tptp.f9 tptp.f10 @t202)) % 0.86/1.04 (define @t247 () (@var "A__questionmark_v_0_69" |tptp.'S6'|)) % 0.86/1.04 (define @t248 () (tptp.f9 tptp.f10 (+ @t4 1))) % 0.86/1.04 (define @t249 () (@var "A__questionmark_v_2_71" Int)) % 0.86/1.04 (define @t250 () (@var "A__questionmark_v_1_72" Int)) % 0.86/1.04 (define @t251 () (@var "A__questionmark_v_0_70" |tptp.'S6'|)) % 0.86/1.04 (define @t252 () (@var "A__questionmark_v_2_74" Int)) % 0.86/1.04 (define @t253 () (@var "A__questionmark_v_1_75" Int)) % 0.86/1.04 (define @t254 () (@var "A__questionmark_v_0_73" |tptp.'S6'|)) % 0.86/1.04 (define @t255 () (@var "A__questionmark_v_2_78" Int)) % 0.86/1.04 (define @t256 () (@var "A__questionmark_v_1_76" Int)) % 0.86/1.04 (define @t257 () (@var "A__questionmark_v_0_77" Int)) % 0.86/1.04 (define @t258 () (@var "A__questionmark_v_2_79" Int)) % 0.86/1.04 (define @t259 () (@var "A__questionmark_v_1_81" |tptp.'S6'|)) % 0.86/1.04 (define @t260 () (@var "A__questionmark_v_0_80" Int)) % 0.86/1.04 (define @t261 () (@var "A__questionmark_v_1_84" Int)) % 0.86/1.04 (define @t262 () (@var "A__questionmark_v_2_82" Int)) % 0.86/1.04 (define @t263 () (@var "A__questionmark_v_0_83" Int)) % 0.86/1.04 (define @t264 () (@var "A__questionmark_v_3_85" Int)) % 0.86/1.04 (define @t265 () (@var "A__questionmark_v_2_88" |tptp.'S6'|)) % 0.86/1.04 (define @t266 () (@var "A__questionmark_v_1_86" Int)) % 0.86/1.04 (define @t267 () (@var "A__questionmark_v_0_87" Int)) % 0.86/1.04 (define @t268 () (@var "A__questionmark_v_3_91" Int)) % 0.86/1.04 (define @t269 () (@var "A__questionmark_v_2_89" Int)) % 0.86/1.04 (define @t270 () (@var "A__questionmark_v_1_92" Int)) % 0.86/1.04 (define @t271 () (@var "A__questionmark_v_0_90" Int)) % 0.86/1.04 (define @t272 () (@var "A__questionmark_v3" |tptp.'S2'|)) % 0.86/1.04 (define @t273 () (@list @t3 @t1 @t201 @t272)) % 0.86/1.04 (define @t274 () (@var "A__questionmark_v_1_94" Int)) % 0.86/1.04 (define @t275 () (@var "A__questionmark_v_2_95" Int)) % 0.86/1.04 (define @t276 () (@var "A__questionmark_v_0_93" Int)) % 0.86/1.04 (define @t277 () (@var "A__questionmark_v_2_98" Int)) % 0.86/1.04 (define @t278 () (@var "A__questionmark_v_1_97" Int)) % 0.86/1.04 (define @t279 () (@var "A__questionmark_v_0_96" Int)) % 0.86/1.04 (define @t280 () (@var "A__questionmark_v_2_100" Int)) % 0.86/1.04 (define @t281 () (@var "A__questionmark_v_1_101" Int)) % 0.86/1.04 (define @t282 () (@var "A__questionmark_v_0_99" Int)) % 0.86/1.04 (define @t283 () (@var "A__questionmark_v_1_102" |tptp.'S14'|)) % 0.86/1.04 (define @t284 () (@var "A__questionmark_v_0_103" |tptp.'S14'|)) % 0.86/1.04 (define @t285 () (tptp.f39 tptp.f52 @t21)) % 0.86/1.04 (define @t286 () (tptp.f34 @t103 @t50)) % 0.86/1.04 (define @t287 () (tptp.f16 (tptp.f17 tptp.f18 @t73) @t17)) % 0.86/1.04 (define @t288 () (tptp.f39 tptp.f52 tptp.f51)) % 0.86/1.04 (define @t289 () (tptp.f49 tptp.f50 @t75)) % 0.86/1.04 (define @t290 () (tptp.f49 tptp.f50 @t48)) % 0.86/1.04 (define @t291 () (@var "A__questionmark_v_0_104" |tptp.'S14'|)) % 0.86/1.04 (define @t292 () (tptp.f16 @t89 @t17)) % 0.86/1.04 (define @t293 () (@var "A__questionmark_v_3_108" Real)) % 0.86/1.04 (define @t294 () (@var "A__questionmark_v_2_105" |tptp.'S14'|)) % 0.86/1.04 (define @t295 () (@var "A__questionmark_v_1_106" Real)) % 0.86/1.04 (define @t296 () (@var "A__questionmark_v_0_107" |tptp.'S14'|)) % 0.86/1.04 (define @t297 () (tptp.f22 (tptp.f49 tptp.f50 @t139) @t14)) % 0.86/1.04 (define @t298 () (tptp.f49 tptp.f50 @t16)) % 0.86/1.04 (define @t299 () (tptp.f22 @t298 @t17)) % 0.86/1.04 (define @t300 () (@list @t16)) % 0.86/1.04 (define @t301 () (forall @t300 (<= (tptp.f22 tptp.f30 @t299) @t297))) % 0.86/1.04 (define @t302 () (<= 0/1 @t14)) % 0.86/1.04 (define @t303 () (tptp.f22 (tptp.f49 tptp.f50 @t143) @t14)) % 0.86/1.04 (define @t304 () (tptp.f39 tptp.f52 @t99)) % 0.86/1.04 (define @t305 () (@list @t99)) % 0.86/1.04 (define @t306 () (forall @t305 (<= (tptp.f27 tptp.f31 (tptp.f34 @t304 @t39)) @t303))) % 0.86/1.04 (define @t307 () (< 0/1 @t14)) % 0.86/1.04 (define @t308 () (forall @t300 (<= @t138 @t297))) % 0.86/1.04 (define @t309 () (forall @t305 (<= @t142 @t303))) % 0.86/1.04 (define @t310 () (forall @t40 (<= (tptp.f22 tptp.f30 @t110) (tptp.f22 (tptp.f49 tptp.f50 (tptp.f22 @t82 @t139)) @t17)))) % 0.86/1.04 (define @t311 () (forall (@list @t64 @t99) (<= (tptp.f27 tptp.f31 @t114) (tptp.f22 (tptp.f49 tptp.f50 (tptp.f22 @t180 @t143)) @t17)))) % 0.86/1.04 (define @t312 () (@list @t1)) % 0.86/1.04 (define @t313 () (@list @t121)) % 0.86/1.04 (define @t314 () (@var "A__questionmark_v1" |tptp.'S22'|)) % 0.86/1.04 (define @t315 () (@list @t201)) % 0.86/1.04 (define @t316 () (@var "A__questionmark_v_0_109" |tptp.'S2'|)) % 0.86/1.04 (define @t317 () (tptp.f6 tptp.f7 (* 2 @t121))) % 0.86/1.04 (define @t318 () (<= 0 @t121)) % 0.86/1.04 (define @t319 () (tptp.f6 tptp.f7 @t121)) % 0.86/1.04 (define @t320 () (@var "A__questionmark_v_0_110" |tptp.'S10'|)) % 0.86/1.04 (define @t321 () (@var "A__questionmark_v_0_111" Real)) % 0.86/1.04 (define @t322 () (@var "A__questionmark_v_0_112" Int)) % 0.86/1.04 (define @t323 () (tptp.f11 tptp.f12 @t319)) % 0.86/1.04 (define @t324 () (@var "A__questionmark_v_1_114" |tptp.'S3'|)) % 0.86/1.04 (define @t325 () (@var "A__questionmark_v_0_113" |tptp.'S3'|)) % 0.86/1.04 (define @t326 () (tptp.f4 tptp.f54 @t201)) % 0.86/1.04 (define @t327 () (@var "A__questionmark_v3" |tptp.'S10'|)) % 0.86/1.04 (define @t328 () (@var "A__questionmark_v_1_116" |tptp.'S17'|)) % 0.86/1.04 (define @t329 () (@var "A__questionmark_v_0_115" |tptp.'S17'|)) % 0.86/1.04 (define @t330 () (@list @t39 @t64 @t99 @t327)) % 0.86/1.04 (define @t331 () (@var "A__questionmark_v_1_118" |tptp.'S14'|)) % 0.86/1.04 (define @t332 () (@var "A__questionmark_v_0_117" |tptp.'S14'|)) % 0.86/1.04 (define @t333 () (@var "A__questionmark_v3" Int)) % 0.86/1.04 (define @t334 () (@var "A__questionmark_v2" Int)) % 0.86/1.04 (define @t335 () (@var "A__questionmark_v_1_120" |tptp.'S6'|)) % 0.86/1.04 (define @t336 () (@var "A__questionmark_v_0_119" |tptp.'S6'|)) % 0.86/1.04 (define @t337 () (tptp.f9 tptp.f10 @t334)) % 0.86/1.04 (define @t338 () (@list @t121 @t120 @t334 @t333)) % 0.86/1.04 (define @t339 () (tptp.f3 (tptp.f4 tptp.f54 (tptp.f3 @t126 @t201)) @t1)) % 0.86/1.04 (define @t340 () (tptp.f3 @t326 @t1)) % 0.86/1.04 (define @t341 () (tptp.f4 tptp.f53 @t131)) % 0.86/1.04 (define @t342 () (tptp.f34 (tptp.f39 tptp.f52 @t158) @t64)) % 0.86/1.04 (define @t343 () (tptp.f34 @t304 @t64)) % 0.86/1.04 (define @t344 () (tptp.f39 tptp.f40 @t135)) % 0.86/1.04 (define @t345 () (tptp.f22 (tptp.f49 tptp.f50 @t159) @t14)) % 0.86/1.04 (define @t346 () (tptp.f22 @t298 @t14)) % 0.86/1.04 (define @t347 () (+ @t121 @t334)) % 0.86/1.04 (define @t348 () (tptp.f8 (tptp.f9 tptp.f10 @t347) @t120)) % 0.86/1.04 (define @t349 () (tptp.f8 @t337 @t120)) % 0.86/1.04 (define @t350 () (tptp.f22 tptp.f23 @t17)) % 0.86/1.04 (define @t351 () (tptp.f8 tptp.f21 @t121)) % 0.86/1.04 (define @t352 () (tptp.f4 tptp.f54 @t1)) % 0.86/1.04 (define @t353 () (tptp.f22 @t109 @t17)) % 0.86/1.04 (define @t354 () (tptp.f9 tptp.f10 @t120)) % 0.86/1.04 (define @t355 () (@var "A__questionmark_v_1_121" |tptp.'S3'|)) % 0.86/1.04 (define @t356 () (@var "A__questionmark_v_0_122" |tptp.'S3'|)) % 0.86/1.04 (define @t357 () (@var "A__questionmark_v_1_123" |tptp.'S14'|)) % 0.86/1.04 (define @t358 () (@var "A__questionmark_v_0_124" |tptp.'S14'|)) % 0.86/1.04 (define @t359 () (@var "A__questionmark_v_1_125" |tptp.'S6'|)) % 0.86/1.04 (define @t360 () (@var "A__questionmark_v_0_126" |tptp.'S6'|)) % 0.86/1.04 (define @t361 () (@list @t121 @t120 @t334)) % 0.86/1.04 (define @t362 () (@var "A__questionmark_v_1_127" |tptp.'S17'|)) % 0.86/1.04 (define @t363 () (@var "A__questionmark_v_0_128" |tptp.'S17'|)) % 0.86/1.04 (define @t364 () (@var "A__questionmark_v_0_129" |tptp.'S3'|)) % 0.86/1.04 (define @t365 () (tptp.f3 @t352 @t201)) % 0.86/1.04 (define @t366 () (@var "A__questionmark_v_0_130" |tptp.'S14'|)) % 0.86/1.04 (define @t367 () (@var "A__questionmark_v_0_131" |tptp.'S6'|)) % 0.86/1.04 (define @t368 () (tptp.f8 @t354 @t334)) % 0.86/1.04 (define @t369 () (@var "A__questionmark_v_0_132" |tptp.'S17'|)) % 0.86/1.04 (define @t370 () (tptp.f22 @t98 @t17)) % 0.86/1.04 (define @t371 () (@var "A__questionmark_v_0_133" Real)) % 0.86/1.04 (define @t372 () (tptp.f8 @t133 @t121)) % 0.86/1.04 (define @t373 () (@var "A__questionmark_v_0_134" Int)) % 0.86/1.04 (define @t374 () (@var "A__questionmark_v_0_135" |tptp.'S3'|)) % 0.86/1.04 (define @t375 () (@var "A__questionmark_v_0_136" |tptp.'S14'|)) % 0.86/1.04 (define @t376 () (@var "A__questionmark_v_0_137" |tptp.'S6'|)) % 0.86/1.04 (define @t377 () (@var "A__questionmark_v_0_138" |tptp.'S17'|)) % 0.86/1.04 (define @t378 () (@var "A__questionmark_v_0_139" |tptp.'S3'|)) % 0.86/1.04 (define @t379 () (@var "A__questionmark_v_0_140" |tptp.'S14'|)) % 0.86/1.04 (define @t380 () (@var "A__questionmark_v_0_141" |tptp.'S6'|)) % 0.86/1.04 (define @t381 () (@var "A__questionmark_v_0_142" |tptp.'S17'|)) % 0.86/1.04 (define @t382 () (@var "A__questionmark_v_1_144" |tptp.'S2'|)) % 0.86/1.04 (define @t383 () (@var "A__questionmark_v_0_143" |tptp.'S3'|)) % 0.86/1.04 (define @t384 () (tptp.f3 @t326 @t272)) % 0.86/1.04 (define @t385 () (@var "A__questionmark_v_1_146" Real)) % 0.86/1.04 (define @t386 () (@var "A__questionmark_v_0_145" |tptp.'S14'|)) % 0.86/1.04 (define @t387 () (tptp.f22 @t298 @t13)) % 0.86/1.04 (define @t388 () (@var "A__questionmark_v_1_148" Int)) % 0.86/1.04 (define @t389 () (@var "A__questionmark_v_0_147" |tptp.'S6'|)) % 0.86/1.04 (define @t390 () (tptp.f8 @t337 @t333)) % 0.86/1.04 (define @t391 () (@var "A__questionmark_v_1_150" |tptp.'S10'|)) % 0.86/1.04 (define @t392 () (@var "A__questionmark_v_0_149" |tptp.'S17'|)) % 0.86/1.04 (define @t393 () (tptp.f34 @t304 @t327)) % 0.86/1.04 (define @t394 () (@var "A__questionmark_v_1_151" |tptp.'S3'|)) % 0.86/1.04 (define @t395 () (@var "A__questionmark_v_0_152" |tptp.'S3'|)) % 0.86/1.04 (define @t396 () (@var "A__questionmark_v_1_153" |tptp.'S14'|)) % 0.86/1.04 (define @t397 () (@var "A__questionmark_v_0_154" |tptp.'S14'|)) % 0.86/1.04 (define @t398 () (@var "A__questionmark_v_1_155" |tptp.'S6'|)) % 0.86/1.04 (define @t399 () (@var "A__questionmark_v_0_156" |tptp.'S6'|)) % 0.86/1.04 (define @t400 () (@var "A__questionmark_v_1_157" |tptp.'S17'|)) % 0.86/1.04 (define @t401 () (@var "A__questionmark_v_0_158" |tptp.'S17'|)) % 0.86/1.04 (define @t402 () (@var "A__questionmark_v_0_159" |tptp.'S3'|)) % 0.86/1.04 (define @t403 () (@var "A__questionmark_v_0_160" |tptp.'S14'|)) % 0.86/1.04 (define @t404 () (@var "A__questionmark_v_0_161" |tptp.'S6'|)) % 0.86/1.04 (define @t405 () (@var "A__questionmark_v_0_162" |tptp.'S17'|)) % 0.86/1.04 (define @t406 () (@var "A__questionmark_v_1_163" |tptp.'S17'|)) % 0.86/1.04 (define @t407 () (@var "A__questionmark_v_0_164" |tptp.'S17'|)) % 0.86/1.04 (define @t408 () (+ @t17 @t97)) % 0.86/1.04 (define @t409 () (+ @t120 @t334)) % 0.86/1.04 (define @t410 () (+ @t121 @t409)) % 0.86/1.04 (define @t411 () (@var "A__questionmark_v_0_165" |tptp.'S17'|)) % 0.86/1.04 (define @t412 () (+ @t112 @t16)) % 0.86/1.04 (define @t413 () (+ @t122 @t334)) % 0.86/1.04 (define @t414 () (@var "A__questionmark_v_0_166" |tptp.'S17'|)) % 0.86/1.04 (define @t415 () (@var "A__questionmark_v_0_167" |tptp.'S17'|)) % 0.86/1.04 (define @t416 () (@var "A__questionmark_v_0_168" |tptp.'S17'|)) % 0.86/1.04 (define @t417 () (tptp.f34 (tptp.f39 tptp.f40 @t99) @t327)) % 0.86/1.04 (define @t418 () (+ @t16 @t13)) % 0.86/1.04 (define @t419 () (@var "A__questionmark_v_0_169" Int)) % 0.86/1.04 (define @t420 () (@var "A__questionmark_v_0_170" Int)) % 0.86/1.04 (define @t421 () (@var "A__questionmark_v_1_173" Int)) % 0.86/1.04 (define @t422 () (@var "A__questionmark_v_2_172" Int)) % 0.86/1.04 (define @t423 () (tptp.f6 tptp.f7 (tptp.f8 (tptp.f9 tptp.f10 @t422) @t421))) % 0.86/1.04 (define @t424 () (@var "A__questionmark_v_0_171" |tptp.'S2'|)) % 0.86/1.04 (define @t425 () (= @t3 @t424)) % 0.86/1.04 (define @t426 () (@var "A__questionmark_v_0_174" |tptp.'S3'|)) % 0.86/1.04 (define @t427 () (@var "A__questionmark_v_0_175" |tptp.'S17'|)) % 0.86/1.04 (define @t428 () (@var "A__questionmark_v_0_176" |tptp.'S14'|)) % 0.86/1.04 (define @t429 () (@var "A__questionmark_v_0_177" |tptp.'S6'|)) % 0.86/1.04 (define @t430 () (@var "A__questionmark_v_1_179" |tptp.'S3'|)) % 0.86/1.04 (define @t431 () (@var "A__questionmark_v_0_178" |tptp.'S3'|)) % 0.86/1.04 (define @t432 () (@var "A__questionmark_v_1_181" |tptp.'S17'|)) % 0.86/1.04 (define @t433 () (@var "A__questionmark_v_0_180" |tptp.'S17'|)) % 0.86/1.04 (define @t434 () (@var "A__questionmark_v_1_183" |tptp.'S14'|)) % 0.86/1.04 (define @t435 () (@var "A__questionmark_v_0_182" |tptp.'S14'|)) % 0.86/1.04 (define @t436 () (@var "A__questionmark_v_1_185" |tptp.'S6'|)) % 0.86/1.04 (define @t437 () (@var "A__questionmark_v_0_184" |tptp.'S6'|)) % 0.86/1.04 (define @t438 () (@var "A__questionmark_v_0_186" |tptp.'S2'|)) % 0.86/1.04 (define @t439 () (tptp.f6 tptp.f7 2)) % 0.86/1.04 (define @t440 () (tptp.f39 tptp.f61 @t39)) % 0.86/1.04 (define @t441 () (tptp.f34 tptp.f62 @t64)) % 0.86/1.04 (define @t442 () (tptp.f6 tptp.f7 (+ @t2 @t202))) % 0.86/1.04 (define @t443 () (@var "A__questionmark_v_0_187" |tptp.'S8'|)) % 0.86/1.04 (define @t444 () (tptp.f63 tptp.f64 @t121)) % 0.86/1.04 (define @t445 () (@list @t121 @t1 @t201)) % 0.86/1.04 (define @t446 () (@var "A__questionmark_v_0_188" |tptp.'S13'|)) % 0.86/1.04 (define @t447 () (tptp.f59 tptp.f60 @t17)) % 0.86/1.04 (define @t448 () (@list @t17 @t1 @t201)) % 0.86/1.04 (define @t449 () (@var "A__questionmark_v_0_189" |tptp.'S3'|)) % 0.86/1.04 (define @t450 () (tptp.f4 tptp.f65 @t3)) % 0.86/1.04 (define @t451 () (@var "A__questionmark_v_0_190" |tptp.'S9'|)) % 0.86/1.04 (define @t452 () (tptp.f66 tptp.f67 @t39)) % 0.86/1.04 (define @t453 () (@list @t39 @t1 @t201)) % 0.86/1.04 (define @t454 () (tptp.f63 tptp.f64 @t120)) % 0.86/1.04 (define @t455 () (tptp.f59 tptp.f60 @t14)) % 0.86/1.04 (define @t456 () (tptp.f4 tptp.f65 @t1)) % 0.86/1.04 (define @t457 () (tptp.f66 tptp.f67 @t64)) % 0.86/1.04 (define @t458 () (tptp.f6 tptp.f7 (tptp.f8 (tptp.f9 tptp.f10 @t2) @t202))) % 0.86/1.04 (define @t459 () (@var "A__questionmark_v_0_191" |tptp.'S8'|)) % 0.86/1.04 (define @t460 () (@var "A__questionmark_v_0_192" |tptp.'S13'|)) % 0.86/1.04 (define @t461 () (@var "A__questionmark_v_0_193" |tptp.'S3'|)) % 0.86/1.04 (define @t462 () (@var "A__questionmark_v_0_194" |tptp.'S9'|)) % 0.86/1.04 (define @t463 () (tptp.f6 tptp.f7 (+ @t2 1))) % 0.86/1.04 (define @t464 () (@var "A__questionmark_v_0_195" |tptp.'S8'|)) % 0.86/1.04 (define @t465 () (@list @t121 @t1)) % 0.86/1.04 (define @t466 () (@var "A__questionmark_v_0_196" |tptp.'S13'|)) % 0.86/1.04 (define @t467 () (@list @t17 @t1)) % 0.86/1.04 (define @t468 () (@var "A__questionmark_v_0_197" |tptp.'S3'|)) % 0.86/1.04 (define @t469 () (@var "A__questionmark_v_0_198" |tptp.'S9'|)) % 0.86/1.04 (define @t470 () (@list @t39 @t1)) % 0.86/1.04 (define @t471 () (@var "A__questionmark_v_0_199" |tptp.'S8'|)) % 0.86/1.04 (define @t472 () (* 2 @t2)) % 0.86/1.04 (define @t473 () (tptp.f6 tptp.f7 @t472)) % 0.86/1.04 (define @t474 () (@var "A__questionmark_v_0_200" |tptp.'S13'|)) % 0.86/1.04 (define @t475 () (@var "A__questionmark_v_0_201" |tptp.'S3'|)) % 0.86/1.04 (define @t476 () (@var "A__questionmark_v_0_202" |tptp.'S9'|)) % 0.86/1.04 (define @t477 () (@var "A__questionmark_v_0_203" |tptp.'S8'|)) % 0.86/1.04 (define @t478 () (@var "A__questionmark_v_0_204" |tptp.'S13'|)) % 0.86/1.04 (define @t479 () (@var "A__questionmark_v_0_205" |tptp.'S3'|)) % 0.86/1.04 (define @t480 () (@var "A__questionmark_v_0_206" |tptp.'S9'|)) % 0.86/1.04 (define @t481 () (tptp.f6 tptp.f7 3)) % 0.86/1.04 (define @t482 () (tptp.f3 @t130 @t3)) % 0.86/1.04 (define @t483 () (tptp.f34 @t103 @t39)) % 0.86/1.04 (define @t484 () (tptp.f11 @t444 @t439)) % 0.86/1.04 (define @t485 () (tptp.f19 @t447 @t439)) % 0.86/1.04 (define @t486 () (tptp.f3 @t450 @t439)) % 0.86/1.04 (define @t487 () (tptp.f13 @t452 @t439)) % 0.86/1.04 (define @t488 () (@var "A__questionmark_v_0_207" |tptp.'S8'|)) % 0.86/1.04 (define @t489 () (@var "A__questionmark_v_0_208" |tptp.'S13'|)) % 0.86/1.04 (define @t490 () (@var "A__questionmark_v_0_209" |tptp.'S3'|)) % 0.86/1.04 (define @t491 () (@var "A__questionmark_v_0_210" |tptp.'S9'|)) % 0.86/1.04 (define @t492 () (@var "A__questionmark_v_0_211" Int)) % 0.86/1.04 (define @t493 () (@var "A__questionmark_v_0_212" Real)) % 0.86/1.04 (define @t494 () (@var "A__questionmark_v_0_213" |tptp.'S2'|)) % 0.86/1.04 (define @t495 () (tptp.f63 tptp.f64 @t351)) % 0.86/1.04 (define @t496 () (@var "A__questionmark_v_0_214" |tptp.'S2'|)) % 0.86/1.04 (define @t497 () (tptp.f59 tptp.f60 @t350)) % 0.86/1.04 (define @t498 () (tptp.f19 @t447 @t1)) % 0.86/1.04 (define @t499 () (tptp.f19 (tptp.f59 tptp.f60 @t45) @t1)) % 0.86/1.04 (define @t500 () (tptp.f22 tptp.f30 @t498)) % 0.86/1.04 (define @t501 () (tptp.f59 tptp.f60 @t47)) % 0.86/1.04 (define @t502 () (tptp.f19 @t501 @t1)) % 0.86/1.04 (define @t503 () (tptp.f13 @t452 @t1)) % 0.86/1.04 (define @t504 () (tptp.f27 tptp.f31 @t503)) % 0.86/1.04 (define @t505 () (tptp.f34 @t440 @t64)) % 0.86/1.04 (define @t506 () (- @t14 @t13)) % 0.86/1.04 (define @t507 () (- @t17 @t16)) % 0.86/1.04 (define @t508 () (- @t17 @t14)) % 0.86/1.04 (define @t509 () (@var "A__questionmark_v_0_215" |tptp.'S2'|)) % 0.86/1.04 (define @t510 () (tptp.f22 tptp.f30 @t508)) % 0.86/1.04 (define @t511 () (tptp.f39 tptp.f61 @t64)) % 0.86/1.04 (define @t512 () (tptp.f27 tptp.f31 @t505)) % 0.86/1.04 (define @t513 () (@var "A__questionmark_v_0_216" Real)) % 0.86/1.04 (define @t514 () (< @t513 0/1)) % 0.86/1.04 (define @t515 () (@var "A__questionmark_v_0_217" Real)) % 0.86/1.04 (define @t516 () (< @t515 0/1)) % 0.86/1.04 (define @t517 () (@var "A__questionmark_v_1_219" Int)) % 0.86/1.04 (define @t518 () (@var "A__questionmark_v_0_218" Int)) % 0.86/1.04 (define @t519 () (@var "A__questionmark_v_2_222" Int)) % 0.86/1.04 (define @t520 () (@var "A__questionmark_v_0_220" Int)) % 0.86/1.04 (define @t521 () (@var "A__questionmark_v_1_221" Int)) % 0.86/1.04 (define @t522 () (@var "A__questionmark_v_1_224" Int)) % 0.86/1.04 (define @t523 () (@var "A__questionmark_v_0_223" Int)) % 0.86/1.04 (define @t524 () (tptp.f49 tptp.f50 @t508)) % 0.86/1.04 (define @t525 () (tptp.f39 tptp.f52 @t505)) % 0.86/1.04 (define @t526 () (@var "A__questionmark_v_0_225" |tptp.'S14'|)) % 0.86/1.04 (define @t527 () (- @t14 @t16)) % 0.86/1.04 (define @t528 () (@var "A__questionmark_v_0_226" |tptp.'S17'|)) % 0.86/1.04 (define @t529 () (tptp.f34 @t511 @t99)) % 0.86/1.04 (define @t530 () (@var "A__questionmark_v_0_227" |tptp.'S14'|)) % 0.86/1.04 (define @t531 () (@var "A__questionmark_v_0_228" |tptp.'S17'|)) % 0.86/1.04 (define @t532 () (@var "A__questionmark_v_2_231" |tptp.'S10'|)) % 0.86/1.04 (define @t533 () (@var "A__questionmark_v_1_229" |tptp.'S17'|)) % 0.86/1.04 (define @t534 () (@var "A__questionmark_v_0_230" |tptp.'S17'|)) % 0.86/1.04 (define @t535 () (tptp.f34 @t511 @t327)) % 0.86/1.04 (define @t536 () (tptp.f34 @t440 @t99)) % 0.86/1.04 (define @t537 () (tptp.f39 tptp.f52 @t536)) % 0.86/1.04 (define @t538 () (@var "A__questionmark_v_2_234" Real)) % 0.86/1.04 (define @t539 () (@var "A__questionmark_v_1_232" |tptp.'S14'|)) % 0.86/1.04 (define @t540 () (@var "A__questionmark_v_0_233" |tptp.'S14'|)) % 0.86/1.04 (define @t541 () (tptp.f49 tptp.f50 @t507)) % 0.86/1.04 (define @t542 () (@var "A__questionmark_v4" |tptp.'S10'|)) % 0.86/1.04 (define @t543 () (= (tptp.f34 @t344 @t99) (tptp.f34 (tptp.f39 tptp.f40 (tptp.f34 (tptp.f39 tptp.f52 @t327) @t64)) @t542))) % 0.86/1.04 (define @t544 () (@list @t39 @t64 @t99 @t327 @t542)) % 0.86/1.04 (define @t545 () (@var "A__questionmark_v4" Real)) % 0.86/1.04 (define @t546 () (= (+ @t132 @t16) (+ (tptp.f22 (tptp.f49 tptp.f50 @t13) @t14) @t545))) % 0.86/1.04 (define @t547 () (@list @t17 @t14 @t16 @t13 @t545)) % 0.86/1.04 (define @t548 () (@var "A__questionmark_v4" Int)) % 0.86/1.04 (define @t549 () (= (+ @t134 @t334) (+ (tptp.f8 (tptp.f9 tptp.f10 @t333) @t120) @t548))) % 0.86/1.04 (define @t550 () (@list @t121 @t120 @t334 @t333 @t548)) % 0.86/1.04 (define @t551 () (@var "A__questionmark_v_1_236" Int)) % 0.86/1.04 (define @t552 () (@var "A__questionmark_v_0_235" |tptp.'S8'|)) % 0.86/1.04 (define @t553 () (@var "A__questionmark_v_1_238" Real)) % 0.86/1.04 (define @t554 () (@var "A__questionmark_v_0_237" |tptp.'S13'|)) % 0.86/1.04 (define @t555 () (@var "A__questionmark_v_1_240" |tptp.'S2'|)) % 0.86/1.04 (define @t556 () (@var "A__questionmark_v_0_239" |tptp.'S3'|)) % 0.86/1.04 (define @t557 () (@var "A__questionmark_v_1_242" |tptp.'S10'|)) % 0.86/1.04 (define @t558 () (@var "A__questionmark_v_0_241" |tptp.'S9'|)) % 0.86/1.04 (define @t559 () (@var "A__questionmark_v_1_244" Int)) % 0.86/1.04 (define @t560 () (tptp.f6 tptp.f7 (+ @t472 1))) % 0.86/1.04 (define @t561 () (@var "A__questionmark_v_0_243" |tptp.'S8'|)) % 0.86/1.04 (define @t562 () (@var "A__questionmark_v_1_246" Real)) % 0.86/1.04 (define @t563 () (@var "A__questionmark_v_0_245" |tptp.'S13'|)) % 0.86/1.04 (define @t564 () (@var "A__questionmark_v_1_248" |tptp.'S2'|)) % 0.86/1.04 (define @t565 () (@var "A__questionmark_v_0_247" |tptp.'S3'|)) % 0.86/1.04 (define @t566 () (@var "A__questionmark_v_1_250" |tptp.'S10'|)) % 0.86/1.04 (define @t567 () (@var "A__questionmark_v_0_249" |tptp.'S9'|)) % 0.86/1.04 (define @t568 () (@var "A__questionmark_v_0_251" |tptp.'S8'|)) % 0.86/1.04 (define @t569 () (@var "A__questionmark_v_0_252" |tptp.'S13'|)) % 0.86/1.04 (define @t570 () (@var "A__questionmark_v_0_253" |tptp.'S3'|)) % 0.86/1.04 (define @t571 () (@var "A__questionmark_v_0_254" |tptp.'S9'|)) % 0.86/1.04 (define @t572 () (@var "A__questionmark_v_0_255" |tptp.'S2'|)) % 0.86/1.04 (define @t573 () (tptp.f6 tptp.f7 (+ @t210 1))) % 0.86/1.04 (define @t574 () (@var "A__questionmark_v_0_256" |tptp.'S2'|)) % 0.86/1.04 (define @t575 () (@var "A__questionmark_v_0_257" |tptp.'S2'|)) % 0.86/1.04 (define @t576 () (@var "A__questionmark_v_0_258" |tptp.'S17'|)) % 0.86/1.04 (define @t577 () (@var "A__questionmark_v_0_259" |tptp.'S14'|)) % 0.86/1.04 (define @t578 () (@var "A__questionmark_v_0_260" |tptp.'S6'|)) % 0.86/1.04 (define @t579 () (@var "A__questionmark_v_0_261" |tptp.'S3'|)) % 0.86/1.04 (define @t580 () (tptp.f3 @t579 @t1)) % 0.86/1.04 (define @t581 () (tptp.f22 @t109 @t14)) % 0.86/1.04 (define @t582 () (@var "A__questionmark_v_0_262" |tptp.'S14'|)) % 0.86/1.04 (define @t583 () (@var "A__questionmark_v_0_263" Real)) % 0.86/1.04 (define @t584 () (= @t14 @t16)) % 0.86/1.04 (define @t585 () (not @t179)) % 0.86/1.04 (define @t586 () (@var "A__questionmark_v_0_264" |tptp.'S14'|)) % 0.86/1.04 (define @t587 () (< @t14 @t16)) % 0.86/1.04 (define @t588 () (<= @t14 @t16)) % 0.86/1.04 (define @t589 () (@var "A__questionmark_v_0_265" |tptp.'S14'|)) % 0.86/1.04 (define @t590 () (@var "A__questionmark_v_0_266" Real)) % 0.86/1.04 (define @t591 () (@var "A__questionmark_v_0_267" |tptp.'S14'|)) % 0.86/1.04 (define @t592 () (@var "A__questionmark_v_0_268" |tptp.'S2'|)) % 0.86/1.04 (define @t593 () (@var "A__questionmark_v_1_269" Real)) % 0.86/1.04 (define @t594 () (@var "A__questionmark_v_0_270" |tptp.'S2'|)) % 0.86/1.04 (define @t595 () (@var "A__questionmark_v_1_272" |tptp.'S8'|)) % 0.86/1.04 (define @t596 () (@var "A__questionmark_v_0_271" Int)) % 0.86/1.04 (define @t597 () (@var "A__questionmark_v_1_274" |tptp.'S13'|)) % 0.86/1.04 (define @t598 () (@var "A__questionmark_v_0_273" Int)) % 0.86/1.04 (define @t599 () (@var "A__questionmark_v_1_276" |tptp.'S3'|)) % 0.86/1.04 (define @t600 () (@var "A__questionmark_v_0_275" Int)) % 0.86/1.04 (define @t601 () (@var "A__questionmark_v_1_278" |tptp.'S9'|)) % 0.86/1.04 (define @t602 () (@var "A__questionmark_v_0_277" Int)) % 0.86/1.04 (define @t603 () (@var "A__questionmark_v_0_279" |tptp.'S8'|)) % 0.86/1.04 (define @t604 () (@var "A__questionmark_v_0_280" |tptp.'S13'|)) % 0.86/1.04 (define @t605 () (@var "A__questionmark_v_0_281" |tptp.'S3'|)) % 0.86/1.04 (define @t606 () (@var "A__questionmark_v_0_282" |tptp.'S9'|)) % 0.86/1.04 (define @t607 () (tptp.f3 @t450 @t1)) % 0.86/1.04 (define @t608 () (tptp.f11 tptp.f12 @t607)) % 0.86/1.04 (define @t609 () (@var "A__questionmark_v_0_283" Int)) % 0.86/1.04 (define @t610 () (@var "A__questionmark_v_0_284" |tptp.'S3'|)) % 0.86/1.04 (define @t611 () (< 0 @t4)) % 0.86/1.04 (define @t612 () (@var "A__questionmark_v_0_285" |tptp.'S2'|)) % 0.86/1.04 (define @t613 () (@var "A__questionmark_v_0_286" |tptp.'S2'|)) % 0.86/1.04 (define @t614 () (@list tptp.f15)) % 0.86/1.04 (define @t615 () (tptp.f27 tptp.f36 @t10)) % 0.86/1.04 (define @t616 () (tptp.f27 tptp.f28 @t10)) % 0.86/1.04 (define @t617 () (tptp.f17 tptp.f18 @t616)) % 0.86/1.04 (define @t618 () (tptp.f16 @t617 @t615)) % 0.86/1.04 (define @t619 () (= @t10 @t618)) % 0.86/1.04 (define @t620 () (not @t619)) % 0.86/1.04 (define @t621 () (= @t9 @t616)) % 0.86/1.04 (define @t622 () (not @t621)) % 0.86/1.04 (define @t623 () (= @t615 0/1)) % 0.86/1.04 (define @t624 () (not @t623)) % 0.86/1.04 (define @t625 () (and @t619 @t620)) % 0.86/1.04 (assume @p1 (not (= tptp.f1 tptp.f2))) % 0.86/1.04 (assume @p2 (forall @t8 (= (tptp.f3 (tptp.f4 tptp.f5 @t3) @t1) @t7))) % 0.86/1.04 (assume @p3 @t12) % 0.86/1.04 (assume @p4 (forall @t22 (= (= @t21 @t19) (and @t18 @t15)))) % 0.86/1.04 (assume @p5 (forall @t24 (exists (@list @t23) (and (= @t23 @t4) (= (tptp.f8 tptp.f21 @t23) @t23))))) % 0.86/1.04 (assume @p6 (forall @t24 (exists (@list @t25) (and (= @t25 @t26) (= (tptp.f22 tptp.f23 @t25) @t25))))) % 0.86/1.04 (assume @p7 (forall @t8 (= (= @t4 @t2) @t27))) % 0.86/1.04 (assume @p8 (forall @t8 (= (= @t26 @t28) @t27))) % 0.86/1.04 (assume @p9 (forall @t8 (= (= @t30 @t29) @t27))) % 0.86/1.04 (assume @p10 (forall @t8 (= (= @t32 @t31) @t27))) % 0.86/1.04 (assume @p11 (forall @t34 (= (tptp.f25 tptp.f26 @t21) @t33))) % 0.86/1.04 (assume @p12 @t37) % 0.86/1.04 (assume @p13 (forall @t34 (= (tptp.f25 tptp.f29 @t21) @t33))) % 0.86/1.04 (assume @p14 (forall @t41 (=> (forall @t40 (=> (= @t39 @t38) false)) false))) % 0.86/1.04 (assume @p15 (forall @t24 (exists (@list @t42) (and (= @t42 @t26) (= (tptp.f22 tptp.f30 @t42) @t42))))) % 0.86/1.04 (assume @p16 (forall @t24 (= (tptp.f27 tptp.f31 @t30) @t26))) % 0.86/1.04 (assume @p17 (forall @t24 (= (tptp.f16 tptp.f32 @t26) @t30))) % 0.86/1.04 (assume @p18 (forall @t24 (exists (@list @t43) (and (= @t43 @t26) (= (tptp.f22 tptp.f33 @t43) @t43))))) % 0.86/1.04 (assume @p19 (forall @t24 (exists (@list @t44) (and (= @t44 @t30) (= (tptp.f34 tptp.f35 @t44) @t44))))) % 0.86/1.04 (assume @p20 (forall @t46 (not (< @t45 0/1)))) % 0.86/1.04 (assume @p21 (forall @t41 (not (< @t47 0/1)))) % 0.86/1.04 (assume @p22 (forall @t46 (<= 0/1 @t45))) % 0.86/1.04 (assume @p23 (forall @t41 (<= 0/1 @t47))) % 0.86/1.04 (assume @p24 (forall @t41 (<= @t48 @t47))) % 0.86/1.04 (assume @p25 (forall @t46 (= (tptp.f27 tptp.f28 @t49) @t17))) % 0.86/1.04 (assume @p26 (forall @t41 (= (tptp.f34 tptp.f35 @t50) @t39))) % 0.86/1.04 (assume @p27 (forall @t41 (= (tptp.f27 tptp.f28 @t50) @t48))) % 0.86/1.04 (assume @p28 (forall @t46 (exists (@list @t51) (and (= @t51 @t49) (= (tptp.f34 tptp.f35 @t51) @t51))))) % 0.86/1.04 (assume @p29 (forall @t46 (exists (@list @t52) (and (= @t52 @t45) (=> @t53 (= (- @t52) @t52)) (=> (not @t53) (= @t52 @t52)))))) % 0.86/1.04 (assume @p30 (forall @t41 (exists (@list @t54) (and (= @t54 @t47) (=> @t55 (= (- @t54) @t54)) (=> (not @t55) (= @t54 @t54)))))) % 0.86/1.04 (assume @p31 (forall @t41 (= (tptp.f27 tptp.f31 @t50) @t47))) % 0.86/1.04 (assume @p32 (forall @t46 (and (=> @t57 (= @t56 @t59)) (=> @t58 (= @t56 @t17))))) % 0.86/1.04 (assume @p33 (forall @t46 (and (=> @t57 (= @t61 @t59)) (=> @t58 (= @t61 @t17))))) % 0.86/1.04 (assume @p34 (forall @t41 (exists (@list @t62) (and (= @t62 @t48) (=> @t63 (<= (- @t62) @t47)) (=> (not @t63) (<= @t62 @t47)))))) % 0.86/1.04 (assume @p35 (forall @t67 (= (= @t50 @t66) @t65))) % 0.86/1.04 (assume @p36 (forall @t34 (= (= @t49 @t69) @t68))) % 0.86/1.04 (assume @p37 (forall @t34 (= (= @t60 @t70) @t68))) % 0.86/1.04 (assume @p38 (forall @t72 (= (= @t21 @t71) (and @t18 (= @t14 0/1))))) % 0.86/1.04 (assume @p39 (forall @t46 (= @t49 (tptp.f16 @t20 0/1)))) % 0.86/1.04 (assume @p40 (forall @t34 (= (tptp.f27 tptp.f28 @t21) @t17))) % 0.86/1.04 (assume @p41 (forall @t34 (exists (@list @t74) (and (= @t74 @t20) (= (tptp.f34 tptp.f35 (tptp.f16 @t74 @t14)) (tptp.f16 @t74 @t73)))))) % 0.86/1.04 (assume @p42 (forall @t41 (= @t50 (tptp.f16 @t77 @t76)))) % 0.86/1.04 (assume @p43 (= (tptp.f37 tptp.f35) tptp.f1)) % 0.86/1.04 (assume @p44 (= (tptp.f38 tptp.f28) tptp.f1)) % 0.86/1.04 (assume @p45 (forall @t41 (= (tptp.f34 @t78 @t50) (tptp.f16 tptp.f32 (* 2/1 @t48))))) % 0.86/1.04 (assume @p46 @t80) % 0.86/1.04 (assume @p47 (forall @t24 (= (tptp.f41 @t4 tptp.f42) tptp.f1))) % 0.86/1.04 (assume @p48 (forall @t24 (= (tptp.f43 @t26 tptp.f44) tptp.f1))) % 0.86/1.04 (assume @p49 (forall @t24 (= (tptp.f45 @t30 tptp.f46) tptp.f1))) % 0.86/1.04 (assume @p50 (forall @t24 (= (tptp.f47 @t32 tptp.f48) tptp.f1))) % 0.86/1.04 (assume @p51 (exists @t46 @t85)) % 0.86/1.04 (assume @p52 (exists @t46 @t86)) % 0.86/1.04 (assume @p53 (exists @t46 (and @t87 @t85))) % 0.86/1.04 (assume @p54 (exists @t46 (and @t87 @t86))) % 0.86/1.04 (assume @p55 (exists @t46 (and @t88 @t85))) % 0.86/1.04 (assume @p56 (exists @t46 (and @t88 @t86))) % 0.86/1.04 (assume @p57 (forall @t24 (= (tptp.f27 tptp.f36 @t30) 0/1))) % 0.86/1.04 (assume @p58 (= tptp.f51 (tptp.f16 @t89 1/1))) % 0.86/1.04 (assume @p59 (= (tptp.f38 tptp.f36) tptp.f1)) % 0.86/1.04 (assume @p60 (= (tptp.f27 tptp.f36 tptp.f51) 1/1)) % 0.86/1.04 (assume @p61 (forall @t46 (and (=> @t57 (= @t45 @t59)) (=> @t58 (= @t45 @t17))))) % 0.86/1.04 (assume @p62 (forall @t46 (= (tptp.f27 tptp.f36 @t49) 0/1))) % 0.86/1.04 (assume @p63 (forall @t41 (exists (@list @t90) (and (= @t90 @t75) (=> @t91 (<= (- @t90) @t47)) (=> (not @t91) (<= @t90 @t47)))))) % 0.86/1.04 (assume @p64 (forall @t41 (exists (@list @t92) (and (= @t92 @t47) (<= (- @t92) @t92))))) % 0.86/1.04 (assume @p65 (forall @t67 (= (tptp.f27 tptp.f36 @t95) @t94))) % 0.86/1.04 (assume @p66 (forall @t72 (exists (@list @t96) (and (= @t96 @t98) (= (tptp.f22 @t96 @t97) (+ (tptp.f22 @t96 @t14) (tptp.f22 @t96 @t16))))))) % 0.86/1.04 (assume @p67 (forall @t104 (exists (@list @t100) (and (= @t100 @t103) (= (tptp.f34 @t100 @t102) (tptp.f34 (tptp.f39 tptp.f40 (tptp.f34 @t100 @t64)) (tptp.f34 @t100 @t99))))))) % 0.86/1.04 (assume @p68 (forall @t72 (exists (@list @t105) (and (= @t105 @t98) (= (tptp.f22 @t105 @t97) (+ (tptp.f22 @t105 @t14) (tptp.f22 @t105 @t16))))))) % 0.86/1.04 (assume @p69 (forall @t104 (exists (@list @t106) (and (= @t106 @t103) (= (tptp.f34 @t106 @t102) (tptp.f34 (tptp.f39 tptp.f40 (tptp.f34 @t106 @t64)) (tptp.f34 @t106 @t99))))))) % 0.86/1.04 (assume @p70 (forall @t67 (<= (- @t108 @t47) @t107))) % 0.86/1.04 (assume @p71 (forall @t72 (= (tptp.f22 (tptp.f49 tptp.f50 @t112) @t16) (+ @t111 @t110)))) % 0.86/1.04 (assume @p72 (forall @t104 (= (tptp.f34 (tptp.f39 tptp.f52 @t95) @t99) (tptp.f34 (tptp.f39 tptp.f40 @t115) @t114)))) % 0.86/1.04 (assume @p73 (forall @t67 (=> @t117 (=> @t116 (= (tptp.f45 @t95 tptp.f46) tptp.f1))))) % 0.86/1.04 (assume @p74 (forall @t34 (=> @t119 (=> @t118 (= (tptp.f43 @t112 tptp.f44) tptp.f1))))) % 0.86/1.04 (assume @p75 (forall @t125 (=> @t124 (=> @t123 (= (tptp.f41 @t122 tptp.f42) tptp.f1))))) % 0.86/1.04 (assume @p76 (forall @t8 (=> @t129 (=> @t128 (= (tptp.f47 @t127 tptp.f48) tptp.f1))))) % 0.86/1.04 (assume @p77 (forall @t8 (=> @t129 (=> @t128 (= (tptp.f47 @t131 tptp.f48) tptp.f1))))) % 0.86/1.04 (assume @p78 (forall @t34 (=> @t119 (=> @t118 (= (tptp.f43 @t132 tptp.f44) tptp.f1))))) % 0.86/1.04 (assume @p79 (forall @t125 (=> @t124 (=> @t123 (= (tptp.f41 @t134 tptp.f42) tptp.f1))))) % 0.86/1.04 (assume @p80 (forall @t67 (=> @t117 (=> @t116 (= (tptp.f45 @t135 tptp.f46) tptp.f1))))) % 0.86/1.04 (assume @p81 (forall @t8 (= (tptp.f3 tptp.f24 @t7) (tptp.f3 (tptp.f4 tptp.f54 @t32) @t31)))) % 0.86/1.04 (assume @p82 (forall @t8 (= (tptp.f19 tptp.f20 @t7) (tptp.f22 (tptp.f49 tptp.f50 @t26) @t28)))) % 0.86/1.04 (assume @p83 (forall @t8 (exists (@list @t136) (and (= @t136 @t6) (= (tptp.f11 tptp.f12 (tptp.f6 tptp.f7 @t136)) @t136))))) % 0.86/1.04 (assume @p84 (forall @t8 (= (tptp.f13 tptp.f14 @t7) (tptp.f34 (tptp.f39 tptp.f52 @t30) @t29)))) % 0.86/1.04 (assume @p85 (forall @t22 (=> @t141 (=> @t140 (< @t138 @t137))))) % 0.86/1.04 (assume @p86 (forall @t146 (=> @t145 (=> @t144 (< @t142 @t137))))) % 0.86/1.04 (assume @p87 (forall @t34 (<= @t148 @t147))) % 0.86/1.04 (assume @p88 (forall @t67 (<= @t150 @t149))) % 0.86/1.04 (assume @p89 (forall @t34 (= @t148 @t147))) % 0.86/1.04 (assume @p90 (forall @t67 (= @t150 @t149))) % 0.86/1.04 (assume @p91 (forall @t34 (= (tptp.f22 tptp.f33 @t132) (tptp.f22 (tptp.f49 tptp.f50 @t60) @t70)))) % 0.86/1.04 (assume @p92 (forall @t34 (= (tptp.f16 tptp.f32 @t132) (tptp.f34 @t151 @t69)))) % 0.86/1.04 (assume @p93 (forall @t67 (= @t95 (tptp.f16 (tptp.f17 tptp.f18 @t153) @t94)))) % 0.86/1.04 (assume @p94 (forall @t8 (= (tptp.f3 tptp.f24 @t155) (tptp.f3 (tptp.f4 tptp.f53 @t32) @t31)))) % 0.86/1.04 (assume @p95 (forall @t8 (= (tptp.f13 tptp.f14 @t155) (tptp.f34 (tptp.f39 tptp.f40 @t30) @t29)))) % 0.86/1.04 (assume @p96 (forall @t8 (= (tptp.f19 tptp.f20 @t155) (+ @t26 @t28)))) % 0.86/1.04 (assume @p97 (forall @t8 (exists (@list @t156) (and (= @t156 @t154) (= (tptp.f11 tptp.f12 (tptp.f6 tptp.f7 @t156)) @t156))))) % 0.86/1.04 (assume @p98 (forall @t146 (=> @t145 (=> @t144 (< (tptp.f27 tptp.f31 @t158) @t157))))) % 0.86/1.04 (assume @p99 (forall @t22 (=> @t141 (=> @t140 (< (tptp.f22 tptp.f30 @t159) @t157))))) % 0.86/1.04 (assume @p100 (forall @t67 (<= @t160 @t108))) % 0.86/1.04 (assume @p101 (forall @t34 (<= @t162 @t161))) % 0.86/1.04 (assume @p102 (forall @t67 (<= @t108 @t163))) % 0.86/1.04 (assume @p103 (forall @t34 (<= @t161 @t164))) % 0.86/1.04 (assume @p104 (forall @t67 (=> @t166 (=> @t165 @t65)))) % 0.86/1.04 (assume @p105 (forall @t67 (= @t65 (and @t166 @t165)))) % 0.86/1.04 (assume @p106 (forall @t34 (= (tptp.f27 tptp.f36 @t21) @t14))) % 0.86/1.04 (assume @p107 (forall @t41 (= (tptp.f27 tptp.f36 @t50) @t76))) % 0.86/1.04 (assume @p108 (forall @t34 (= (tptp.f22 tptp.f33 @t112) (+ @t60 @t70)))) % 0.86/1.04 (assume @p109 (forall @t34 (= (tptp.f16 tptp.f32 @t112) (tptp.f34 @t167 @t69)))) % 0.86/1.04 (assume @p110 (forall @t67 (= (tptp.f27 tptp.f28 @t95) @t153))) % 0.86/1.04 (assume @p111 (forall @t22 (= (tptp.f34 @t169 @t19) (tptp.f16 @t168 @t157)))) % 0.86/1.04 (assume @p112 (forall @t72 (= (tptp.f34 @t169 @t71) (tptp.f16 @t168 @t14)))) % 0.86/1.04 (assume @p113 (forall @t72 (= (tptp.f34 @t167 @t38) (tptp.f16 (tptp.f17 tptp.f18 @t112) @t16)))) % 0.86/1.04 (assume @p114 (forall @t67 (= (tptp.f34 tptp.f35 @t95) (tptp.f34 (tptp.f39 tptp.f40 @t50) @t66)))) % 0.86/1.04 (assume @p115 (forall @t172 (= (= (tptp.f41 @t121 @t170) tptp.f1) @t171))) % 0.86/1.04 (assume @p116 (forall @t175 (= (= (tptp.f43 @t17 @t173) tptp.f1) @t174))) % 0.86/1.04 (assume @p117 (forall @t178 (= (= (tptp.f45 @t39 @t176) tptp.f1) @t177))) % 0.86/1.04 (assume @p118 (= (tptp.f27 tptp.f28 tptp.f51) 0/1)) % 0.86/1.04 (assume @p119 (forall @t34 (= (= @t21 tptp.f51) (and @t179 (= @t14 1/1))))) % 0.86/1.04 (assume @p120 (exists @t46 @t183)) % 0.86/1.04 (assume @p121 (exists @t46 (and @t87 @t183))) % 0.86/1.04 (assume @p122 (exists @t46 (and @t88 @t183))) % 0.86/1.04 (assume @p123 (exists @t46 (and @t88 @t184))) % 0.86/1.04 (assume @p124 (exists @t46 (and @t87 @t184))) % 0.86/1.04 (assume @p125 (exists @t46 @t184)) % 0.86/1.04 (assume @p126 (exists @t46 (and @t88 @t185))) % 0.86/1.04 (assume @p127 (exists @t46 (and @t87 @t185))) % 0.86/1.04 (assume @p128 (forall @t24 (exists (@list @t186) (and (= @t186 @t4) (<= @t186 (tptp.f8 (tptp.f9 tptp.f10 @t186) @t186)))))) % 0.86/1.04 (assume @p129 (forall @t24 (exists (@list @t187) (and (= @t187 @t4) (exists (@list @t188) (and (= @t188 (tptp.f9 tptp.f10 @t187)) (<= @t187 (tptp.f8 @t188 (tptp.f8 @t188 @t187))))))))) % 0.86/1.04 (assume @p130 (forall @t24 (= (tptp.f6 tptp.f7 (* 0 @t4)) @t33))) % 0.86/1.04 (assume @p131 (forall @t24 (= (tptp.f6 tptp.f7 (* 1 @t4)) @t3))) % 0.86/1.04 (assume @p132 (forall @t8 (exists (@list @t190 @t189) (and (= @t190 @t4) (= @t189 @t2) (= (< 0 (tptp.f8 (tptp.f9 tptp.f10 @t190) @t189)) (and (< 0 @t190) (< 0 @t189))))))) % 0.86/1.04 (assume @p133 (forall @t8 (exists (@list @t191) (and (= @t191 @t192) (= (= @t191 @t7) (and (= @t3 @t191) (= @t1 @t191))))))) % 0.86/1.04 (assume @p134 (forall @t24 (= (tptp.f6 tptp.f7 (* @t4 0)) @t33))) % 0.86/1.04 (assume @p135 (forall @t24 (= (tptp.f6 tptp.f7 (* @t4 1)) @t3))) % 0.86/1.04 (assume @p136 (forall @t8 (exists (@list @t193 @t194) (and (= @t193 @t4) (= @t194 @t2) (= (tptp.f6 tptp.f7 (tptp.f8 (tptp.f9 tptp.f10 @t193) @t194)) (tptp.f6 tptp.f7 (tptp.f8 (tptp.f9 tptp.f10 @t194) @t193))))))) % 0.86/1.04 (assume @p137 (forall @t8 (exists (@list @t197) (and (= @t197 @t4) (exists (@list @t196 @t195) (and (= @t196 (tptp.f9 tptp.f10 @t197)) (= @t195 @t2) (= (tptp.f6 tptp.f7 (tptp.f8 @t196 (+ @t195 1))) (tptp.f6 tptp.f7 (+ @t197 (tptp.f8 @t196 @t195)))))))))) % 0.86/1.04 (assume @p138 (forall @t203 (exists (@list @t199 @t200 @t198) (and (= @t199 @t5) (= @t200 @t2) (= @t198 @t202) (= (tptp.f6 tptp.f7 (tptp.f8 @t199 (+ @t200 @t198))) (tptp.f6 tptp.f7 (+ (tptp.f8 @t199 @t200) (tptp.f8 @t199 @t198)))))))) % 0.86/1.04 (assume @p139 (forall @t203 (exists (@list @t205 @t204 @t206) (and (= @t205 @t5) (= @t204 @t202) (= @t206 @t2) (= (tptp.f6 tptp.f7 (tptp.f8 @t205 (tptp.f11 tptp.f12 (tptp.f6 tptp.f7 (- @t206 @t204))))) (tptp.f6 tptp.f7 (- (tptp.f8 @t205 @t206) (tptp.f8 @t205 @t204)))))))) % 0.86/1.04 (assume @p140 (forall @t8 (exists (@list @t209 @t207 @t208) (and (= @t209 @t4) (= @t207 @t2) (= @t208 @t210) (= (<= @t208 (tptp.f8 (tptp.f9 tptp.f10 @t209) @t207)) (and (<= @t208 @t209) (<= @t208 @t207))))))) % 0.86/1.04 (assume @p141 (forall @t8 (exists (@list @t212 @t211) (and (= @t212 @t4) (= @t211 @t2) (= (tptp.f6 tptp.f7 (tptp.f8 (tptp.f9 tptp.f10 (+ @t212 1)) @t211)) (tptp.f6 tptp.f7 (+ @t211 (tptp.f8 (tptp.f9 tptp.f10 @t212) @t211)))))))) % 0.86/1.04 (assume @p142 (forall @t8 (exists (@list @t213) (and (= @t213 @t192) (= (= @t7 @t213) (and (= @t3 @t213) (= @t1 @t213))))))) % 0.86/1.04 (assume @p143 (forall @t8 (exists (@list @t214) (and (= @t214 @t33) (= (= @t7 @t214) (or (= @t3 @t214) (= @t1 @t214))))))) % 0.86/1.04 (assume @p144 (forall @t203 (exists (@list @t217 @t216 @t215) (and (= @t217 @t5) (= @t216 @t2) (= @t215 @t202) (= (tptp.f6 tptp.f7 (tptp.f8 (tptp.f9 tptp.f10 (tptp.f8 @t217 @t216)) @t215)) (tptp.f6 tptp.f7 (tptp.f8 @t217 (tptp.f8 (tptp.f9 tptp.f10 @t216) @t215)))))))) % 0.86/1.04 (assume @p145 (forall @t203 (exists (@list @t220 @t219 @t218) (and (= @t220 @t4) (= @t219 @t2) (= @t218 @t202) (= (tptp.f6 tptp.f7 (tptp.f8 (tptp.f9 tptp.f10 (+ @t220 @t219)) @t218)) (tptp.f6 tptp.f7 (+ (tptp.f8 (tptp.f9 tptp.f10 @t220) @t218) (tptp.f8 (tptp.f9 tptp.f10 @t219) @t218)))))))) % 0.86/1.04 (assume @p146 (forall @t203 (exists (@list @t222 @t223 @t221) (and (= @t222 @t2) (= @t223 @t4) (= @t221 @t202) (= (tptp.f6 tptp.f7 (tptp.f8 (tptp.f9 tptp.f10 (tptp.f11 tptp.f12 (tptp.f6 tptp.f7 (- @t223 @t222)))) @t221)) (tptp.f6 tptp.f7 (- (tptp.f8 (tptp.f9 tptp.f10 @t223) @t221) (tptp.f8 (tptp.f9 tptp.f10 @t222) @t221)))))))) % 0.86/1.04 (assume @p147 (forall @t8 (exists (@list @t224) (and (= @t224 @t225) (= (= @t7 @t224) (and (= @t3 @t224) (= @t1 @t224))))))) % 0.86/1.04 (assume @p148 (forall @t203 (exists (@list @t228) (and (= @t228 @t4) (exists (@list @t229 @t226 @t227) (and (= @t229 (tptp.f9 tptp.f10 @t228)) (= @t226 @t202) (= @t227 @t2) (= (< (tptp.f8 @t229 @t227) (tptp.f8 @t229 @t226)) (and (< 0 @t228) (< @t227 @t226))))))))) % 0.86/1.04 (assume @p149 (forall @t203 (exists (@list @t230 @t232 @t231) (and (= @t230 @t202) (= @t232 @t2) (= @t231 @t4) (= (< (tptp.f8 (tptp.f9 tptp.f10 @t231) @t232) (tptp.f8 (tptp.f9 tptp.f10 @t230) @t232)) (and (< 0 @t232) (< @t231 @t230))))))) % 0.86/1.04 (assume @p150 (forall @t203 (exists (@list @t235) (and (= @t235 @t4) (exists (@list @t236 @t233 @t234) (and (= @t236 (tptp.f9 tptp.f10 @t235)) (= @t233 @t202) (= @t234 @t2) (= (<= (tptp.f8 @t236 @t234) (tptp.f8 @t236 @t233)) (=> (< 0 @t235) (<= @t234 @t233))))))))) % 0.86/1.04 (assume @p151 (forall @t203 (exists (@list @t237 @t239 @t238) (and (= @t237 @t202) (= @t239 @t2) (= @t238 @t4) (= (<= (tptp.f8 (tptp.f9 tptp.f10 @t238) @t239) (tptp.f8 (tptp.f9 tptp.f10 @t237) @t239)) (=> (< 0 @t239) (<= @t238 @t237))))))) % 0.86/1.04 (assume @p152 (forall @t203 (exists (@list @t242) (and (= @t242 @t5) (= (= (tptp.f6 tptp.f7 (tptp.f8 @t242 @t2)) (tptp.f6 tptp.f7 (tptp.f8 @t242 @t202))) (or @t241 @t240)))))) % 0.86/1.04 (assume @p153 (forall @t203 (exists (@list @t245) (and (= @t245 @t2) (= (= (tptp.f6 tptp.f7 (tptp.f8 @t5 @t245)) (tptp.f6 tptp.f7 (tptp.f8 @t246 @t245))) (or @t244 @t243)))))) % 0.86/1.04 (assume @p154 (forall @t203 (exists (@list @t247) (and (= @t247 @t248) (= (= (tptp.f6 tptp.f7 (tptp.f8 @t247 @t2)) (tptp.f6 tptp.f7 (tptp.f8 @t247 @t202))) @t241))))) % 0.86/1.04 (assume @p155 (forall @t203 (exists (@list @t251 @t249 @t250) (and (= @t251 @t248) (= @t249 @t202) (= @t250 @t2) (= (< (tptp.f8 @t251 @t250) (tptp.f8 @t251 @t249)) (< @t250 @t249)))))) % 0.86/1.04 (assume @p156 (forall @t203 (exists (@list @t254 @t252 @t253) (and (= @t254 @t248) (= @t252 @t202) (= @t253 @t2) (= (<= (tptp.f8 @t254 @t253) (tptp.f8 @t254 @t252)) (<= @t253 @t252)))))) % 0.86/1.04 (assume @p157 (forall @t203 (exists (@list @t256 @t257 @t255) (and (= @t256 @t2) (= @t257 @t4) (= @t255 @t202) (=> (<= @t257 @t256) (<= (tptp.f8 (tptp.f9 tptp.f10 @t257) @t255) (tptp.f8 (tptp.f9 tptp.f10 @t256) @t255))))))) % 0.86/1.04 (assume @p158 (forall @t203 (exists (@list @t258 @t260 @t259) (and (= @t258 @t2) (= @t260 @t4) (= @t259 @t246) (=> (<= @t260 @t258) (<= (tptp.f8 @t259 @t260) (tptp.f8 @t259 @t258))))))) % 0.86/1.04 (assume @p159 (forall @t203 (exists (@list @t262 @t263 @t261) (and (= @t262 @t2) (= @t263 @t4) (= @t261 @t202) (=> (< @t263 @t262) (=> (< 0 @t261) (< (tptp.f8 (tptp.f9 tptp.f10 @t263) @t261) (tptp.f8 (tptp.f9 tptp.f10 @t262) @t261)))))))) % 0.86/1.04 (assume @p160 (forall @t203 (exists (@list @t264 @t266 @t267) (and (= @t264 @t2) (= @t266 @t4) (= @t267 @t202) (exists (@list @t265) (and (= @t265 (tptp.f9 tptp.f10 @t267)) (=> (< @t266 @t264) (=> (< 0 @t267) (< (tptp.f8 @t265 @t266) (tptp.f8 @t265 @t264)))))))))) % 0.86/1.04 (assume @p161 (forall @t273 (exists (@list @t269 @t271 @t268 @t270) (and (= @t269 @t2) (= @t271 @t4) (= @t268 (tptp.f11 tptp.f12 @t272)) (= @t270 @t202) (=> (<= @t271 @t269) (=> (<= @t270 @t268) (<= (tptp.f8 (tptp.f9 tptp.f10 @t271) @t270) (tptp.f8 (tptp.f9 tptp.f10 @t269) @t268)))))))) % 0.86/1.04 (assume @p162 (forall @t8 (=> (= @t3 @t7) (or (= @t1 @t192) @t240)))) % 0.86/1.04 (assume @p163 (forall @t8 (exists (@list @t276 @t274 @t275) (and (= @t276 @t210) (= @t274 @t4) (= @t275 @t2) (=> (< @t276 @t274) (=> (< @t276 @t275) (< @t274 (tptp.f8 (tptp.f9 tptp.f10 @t275) @t274)))))))) % 0.86/1.04 (assume @p164 (forall @t8 (exists (@list @t279 @t278 @t277) (and (= @t279 @t210) (= @t278 @t4) (= @t277 @t2) (=> (< @t279 @t278) (=> (< @t279 @t277) (< @t278 (tptp.f8 (tptp.f9 tptp.f10 @t278) @t277)))))))) % 0.86/1.04 (assume @p165 (forall @t8 (exists (@list @t282 @t280 @t281) (and (= @t282 @t210) (= @t280 @t4) (= @t281 @t2) (=> (< @t282 @t280) (=> (< @t282 @t281) (< @t282 (tptp.f8 (tptp.f9 tptp.f10 @t281) @t280)))))))) % 0.86/1.04 (assume @p166 (forall @t67 (= (tptp.f34 tptp.f35 @t135) (tptp.f34 (tptp.f39 tptp.f52 @t50) @t66)))) % 0.86/1.04 (assume @p167 (forall @t22 (exists (@list @t283 @t284) (and (= @t283 @t109) (= @t284 @t98) (= (tptp.f34 @t285 @t19) (tptp.f16 (tptp.f17 tptp.f18 (- (tptp.f22 @t284 @t16) (tptp.f22 @t283 @t13))) (+ (tptp.f22 @t284 @t13) (tptp.f22 @t283 @t16)))))))) % 0.86/1.04 (assume @p168 (forall @t41 (= (tptp.f27 tptp.f36 @t286) 0/1))) % 0.86/1.04 (assume @p169 (forall @t34 (= (tptp.f34 @t288 @t21) @t287))) % 0.86/1.04 (assume @p170 (forall @t34 (= (tptp.f34 @t285 tptp.f51) @t287))) % 0.86/1.04 (assume @p171 (= (tptp.f34 @t288 tptp.f51) (tptp.f16 tptp.f32 (- 1/1)))) % 0.86/1.04 (assume @p172 (forall @t67 (= (tptp.f27 tptp.f28 @t135) (- (tptp.f22 @t290 @t152) (tptp.f22 @t289 @t93))))) % 0.86/1.04 (assume @p173 (forall @t67 (= (tptp.f27 tptp.f36 @t135) (+ (tptp.f22 @t290 @t93) (tptp.f22 @t289 @t152))))) % 0.86/1.04 (assume @p174 (forall @t72 (exists (@list @t291) (and (= @t291 @t98) (= (tptp.f34 @t151 @t38) (tptp.f16 (tptp.f17 tptp.f18 (tptp.f22 @t291 @t14)) (tptp.f22 @t291 @t16))))))) % 0.86/1.04 (assume @p175 (forall @t72 (= (tptp.f34 @t285 @t71) (tptp.f16 (tptp.f17 tptp.f18 @t111) @t110)))) % 0.86/1.04 (assume @p176 (forall @t46 (= (tptp.f34 @t288 @t49) @t292))) % 0.86/1.04 (assume @p177 (forall @t46 (= (tptp.f34 @t151 tptp.f51) @t292))) % 0.86/1.04 (assume @p178 (forall @t67 (exists (@list @t294 @t295 @t296 @t293) (and (= @t294 @t289) (= @t295 @t93) (= @t296 @t290) (= @t293 @t152) (= @t135 (tptp.f16 (tptp.f17 tptp.f18 (- (tptp.f22 @t296 @t293) (tptp.f22 @t294 @t295))) (+ (tptp.f22 @t296 @t295) (tptp.f22 @t294 @t293)))))))) % 0.86/1.04 (assume @p179 (exists @t46 @t185)) % 0.86/1.04 (assume @p180 (forall @t46 (exists @t84 (and @t302 @t301)))) % 0.86/1.04 (assume @p181 (forall @t41 (exists @t84 (and @t302 @t306)))) % 0.86/1.04 (assume @p182 (forall @t46 (exists @t84 (and @t307 @t301)))) % 0.86/1.04 (assume @p183 (forall @t41 (exists @t84 (and @t307 @t306)))) % 0.86/1.04 (assume @p184 (forall @t46 (exists @t84 (and @t302 @t308)))) % 0.86/1.04 (assume @p185 (forall @t41 (exists @t84 (and @t302 @t309)))) % 0.86/1.04 (assume @p186 (forall @t46 (exists @t84 (and @t307 @t308)))) % 0.86/1.04 (assume @p187 (forall @t41 (exists @t84 (and @t307 @t309)))) % 0.86/1.04 (assume @p188 (exists @t46 (and @t88 @t310))) % 0.86/1.04 (assume @p189 (exists @t46 (and @t88 @t311))) % 0.86/1.04 (assume @p190 (exists @t46 @t310)) % 0.86/1.04 (assume @p191 (exists @t46 @t311)) % 0.86/1.04 (assume @p192 (forall @t46 (exists @t84 @t308))) % 0.86/1.04 (assume @p193 (forall @t41 (exists @t84 @t309))) % 0.86/1.04 (assume @p194 (forall @t46 (exists @t84 @t301))) % 0.86/1.04 (assume @p195 (forall @t41 (exists @t84 @t306))) % 0.86/1.04 (assume @p196 (exists @t46 (and @t87 @t310))) % 0.86/1.04 (assume @p197 (exists @t46 (and @t87 @t311))) % 0.86/1.04 (assume @p198 (forall @t24 (=> @t129 (=> (forall @t312 (=> (= @t3 @t31) false)) false)))) % 0.86/1.04 (assume @p199 (forall @t41 (=> @t117 (=> (forall @t312 (=> (= @t39 @t29) false)) false)))) % 0.86/1.04 (assume @p200 (forall @t46 (=> @t119 (=> (forall @t312 (=> (= @t17 @t28) false)) false)))) % 0.86/1.04 (assume @p201 (forall @t313 (=> @t124 (=> (forall @t312 (=> (= @t121 @t2) false)) false)))) % 0.86/1.04 (assume @p202 (forall (@list @t3 @t314) (=> @t129 (=> (forall @t315 (= (tptp.f58 @t314 (tptp.f3 tptp.f24 @t201)) tptp.f1)) (= (tptp.f58 @t314 @t3) tptp.f1))))) % 0.86/1.04 (assume @p203 (forall @t178 (=> @t117 (=> (forall @t315 (= (tptp.f57 @t176 (tptp.f13 tptp.f14 @t201)) tptp.f1)) @t177)))) % 0.86/1.04 (assume @p204 (forall @t175 (=> @t119 (=> (forall @t315 (= (tptp.f56 @t173 (tptp.f19 tptp.f20 @t201)) tptp.f1)) @t174)))) % 0.86/1.04 (assume @p205 (forall @t172 (=> @t124 (=> (forall @t315 (= (tptp.f55 @t170 @t202) tptp.f1)) @t171)))) % 0.86/1.04 (assume @p206 (forall @t313 (exists (@list @t316) (and (= @t316 (tptp.f3 tptp.f24 @t319)) (=> @t318 (= (tptp.f3 tptp.f24 @t317) (tptp.f3 (tptp.f4 tptp.f53 @t316) @t316))))))) % 0.86/1.04 (assume @p207 (forall @t313 (exists (@list @t320) (and (= @t320 (tptp.f13 tptp.f14 @t319)) (=> @t318 (= (tptp.f13 tptp.f14 @t317) (tptp.f34 (tptp.f39 tptp.f40 @t320) @t320))))))) % 0.86/1.04 (assume @p208 (forall @t313 (exists (@list @t321) (and (= @t321 (tptp.f19 tptp.f20 @t319)) (=> @t318 (= (tptp.f19 tptp.f20 @t317) (+ @t321 @t321))))))) % 0.86/1.04 (assume @p209 (forall @t313 (exists (@list @t322) (and (= @t322 @t323) (=> @t318 (= (tptp.f11 tptp.f12 @t317) (+ @t322 @t322))))))) % 0.86/1.04 (assume @p210 (forall @t273 (exists (@list @t325 @t324) (and (= @t325 @t130) (= @t324 @t326) (= (= (tptp.f3 (tptp.f4 tptp.f53 (tptp.f3 @t325 @t1)) (tptp.f3 @t324 @t272)) (tptp.f3 (tptp.f4 tptp.f53 (tptp.f3 @t325 @t272)) (tptp.f3 @t324 @t1))) (or @t244 (= @t1 @t272))))))) % 0.86/1.04 (assume @p211 (forall @t330 (exists (@list @t329 @t328) (and (= @t329 @t103) (= @t328 @t304) (= (= (tptp.f34 (tptp.f39 tptp.f40 (tptp.f34 @t329 @t64)) (tptp.f34 @t328 @t327)) (tptp.f34 (tptp.f39 tptp.f40 (tptp.f34 @t329 @t327)) (tptp.f34 @t328 @t64))) (or (= @t39 @t99) (= @t64 @t327))))))) % 0.86/1.04 (assume @p212 (forall @t22 (exists (@list @t332 @t331) (and (= @t332 @t98) (= @t331 @t298) (= (= (+ (tptp.f22 @t332 @t14) (tptp.f22 @t331 @t13)) (+ (tptp.f22 @t332 @t13) (tptp.f22 @t331 @t14))) (or @t18 @t15)))))) % 0.86/1.04 (assume @p213 (forall @t338 (exists (@list @t336 @t335) (and (= @t336 @t133) (= @t335 @t337) (= (= (+ (tptp.f8 @t336 @t120) (tptp.f8 @t335 @t333)) (+ (tptp.f8 @t336 @t333) (tptp.f8 @t335 @t120))) (or (= @t121 @t334) (= @t120 @t333))))))) % 0.86/1.04 (assume @p214 (forall @t273 (= (tptp.f3 @t341 (tptp.f3 (tptp.f4 tptp.f53 @t340) @t272)) (tptp.f3 (tptp.f4 tptp.f53 @t339) @t272)))) % 0.86/1.04 (assume @p215 (forall @t330 (= (tptp.f34 @t344 (tptp.f34 (tptp.f39 tptp.f40 @t343) @t327)) (tptp.f34 (tptp.f39 tptp.f40 @t342) @t327)))) % 0.86/1.04 (assume @p216 (forall @t22 (= (+ @t132 (+ @t346 @t13)) (+ @t345 @t13)))) % 0.86/1.04 (assume @p217 (forall @t338 (= (+ @t134 (+ @t349 @t333)) (+ @t348 @t333)))) % 0.86/1.04 (assume @p218 (forall @t34 (= (tptp.f22 tptp.f23 @t132) (tptp.f22 (tptp.f49 tptp.f50 @t350) (tptp.f22 tptp.f23 @t14))))) % 0.86/1.04 (assume @p219 (forall @t125 (= (tptp.f8 tptp.f21 @t134) (tptp.f8 (tptp.f9 tptp.f10 @t351) (tptp.f8 tptp.f21 @t120))))) % 0.86/1.04 (assume @p220 (forall @t8 (= @t131 (tptp.f3 @t352 @t3)))) % 0.86/1.04 (assume @p221 (forall @t34 (= @t132 @t353))) % 0.86/1.04 (assume @p222 (forall @t125 (= @t134 (tptp.f8 @t354 @t121)))) % 0.86/1.04 (assume @p223 (forall @t67 (= @t135 (tptp.f34 @t113 @t39)))) % 0.86/1.04 (assume @p224 (forall @t203 (exists (@list @t355 @t356) (and (= @t355 @t130) (= @t356 @t352) (= (tptp.f3 @t355 (tptp.f3 @t356 @t201)) (tptp.f3 @t356 (tptp.f3 @t355 @t201))))))) % 0.86/1.04 (assume @p225 (forall @t72 (exists (@list @t357 @t358) (and (= @t357 @t98) (= @t358 @t109) (= (tptp.f22 @t357 (tptp.f22 @t358 @t16)) (tptp.f22 @t358 (tptp.f22 @t357 @t16))))))) % 0.86/1.04 (assume @p226 (forall @t361 (exists (@list @t359 @t360) (and (= @t359 @t133) (= @t360 @t354) (= (tptp.f8 @t359 (tptp.f8 @t360 @t334)) (tptp.f8 @t360 (tptp.f8 @t359 @t334))))))) % 0.86/1.04 (assume @p227 (forall @t104 (exists (@list @t362 @t363) (and (= @t362 @t103) (= @t363 @t113) (= (tptp.f34 @t362 (tptp.f34 @t363 @t99)) (tptp.f34 @t363 (tptp.f34 @t362 @t99))))))) % 0.86/1.04 (assume @p228 (forall @t203 (exists (@list @t364) (and (= @t364 @t130) (= (tptp.f3 @t364 @t365) (tptp.f3 (tptp.f4 tptp.f54 (tptp.f3 @t364 @t1)) @t201)))))) % 0.86/1.04 (assume @p229 (forall @t72 (exists (@list @t366) (and (= @t366 @t98) (= (tptp.f22 @t366 @t110) (tptp.f22 (tptp.f49 tptp.f50 (tptp.f22 @t366 @t14)) @t16)))))) % 0.86/1.04 (assume @p230 (forall @t361 (exists (@list @t367) (and (= @t367 @t133) (= (tptp.f8 @t367 @t368) (tptp.f8 (tptp.f9 tptp.f10 (tptp.f8 @t367 @t120)) @t334)))))) % 0.86/1.04 (assume @p231 (forall @t104 (exists (@list @t369) (and (= @t369 @t103) (= (tptp.f34 @t369 @t114) (tptp.f34 (tptp.f39 tptp.f52 (tptp.f34 @t369 @t64)) @t99)))))) % 0.86/1.04 (assume @p232 (forall @t46 (exists (@list @t371) (and (= @t371 @t350) (= (tptp.f22 (tptp.f49 tptp.f50 @t371) @t371) @t370))))) % 0.86/1.04 (assume @p233 (forall @t313 (exists (@list @t373) (and (= @t373 @t351) (= (tptp.f8 (tptp.f9 tptp.f10 @t373) @t373) @t372))))) % 0.86/1.04 (assume @p234 (forall @t203 (exists (@list @t374) (and (= @t374 @t130) (= (tptp.f3 (tptp.f4 tptp.f54 (tptp.f3 @t374 @t1)) @t201) (tptp.f3 @t374 @t365)))))) % 0.86/1.04 (assume @p235 (forall @t72 (exists (@list @t375) (and (= @t375 @t98) (= (tptp.f22 (tptp.f49 tptp.f50 (tptp.f22 @t375 @t14)) @t16) (tptp.f22 @t375 @t110)))))) % 0.86/1.04 (assume @p236 (forall @t361 (exists (@list @t376) (and (= @t376 @t133) (= (tptp.f8 (tptp.f9 tptp.f10 (tptp.f8 @t376 @t120)) @t334) (tptp.f8 @t376 @t368)))))) % 0.86/1.04 (assume @p237 (forall @t104 (exists (@list @t377) (and (= @t377 @t103) (= (tptp.f34 (tptp.f39 tptp.f52 (tptp.f34 @t377 @t64)) @t99) (tptp.f34 @t377 @t114)))))) % 0.86/1.04 (assume @p238 (forall @t203 (exists (@list @t378) (and (= @t378 @t130) (= (tptp.f3 (tptp.f4 tptp.f54 (tptp.f3 @t378 @t1)) @t201) (tptp.f3 (tptp.f4 tptp.f54 (tptp.f3 @t378 @t201)) @t1)))))) % 0.86/1.04 (assume @p239 (forall @t72 (exists (@list @t379) (and (= @t379 @t98) (= (tptp.f22 (tptp.f49 tptp.f50 (tptp.f22 @t379 @t14)) @t16) (tptp.f22 (tptp.f49 tptp.f50 (tptp.f22 @t379 @t16)) @t14)))))) % 0.86/1.04 (assume @p240 (forall @t361 (exists (@list @t380) (and (= @t380 @t133) (= (tptp.f8 (tptp.f9 tptp.f10 (tptp.f8 @t380 @t120)) @t334) (tptp.f8 (tptp.f9 tptp.f10 (tptp.f8 @t380 @t334)) @t120)))))) % 0.86/1.04 (assume @p241 (forall @t104 (exists (@list @t381) (and (= @t381 @t103) (= (tptp.f34 (tptp.f39 tptp.f52 (tptp.f34 @t381 @t64)) @t99) (tptp.f34 (tptp.f39 tptp.f52 (tptp.f34 @t381 @t99)) @t64)))))) % 0.86/1.04 (assume @p242 (forall @t273 (exists (@list @t383 @t382) (and (= @t383 @t130) (= @t382 @t384) (= (tptp.f3 (tptp.f4 tptp.f54 (tptp.f3 @t383 @t1)) @t382) (tptp.f3 @t383 (tptp.f3 @t352 @t382))))))) % 0.86/1.04 (assume @p243 (forall @t22 (exists (@list @t386 @t385) (and (= @t386 @t98) (= @t385 @t387) (= (tptp.f22 (tptp.f49 tptp.f50 (tptp.f22 @t386 @t14)) @t385) (tptp.f22 @t386 (tptp.f22 @t109 @t385))))))) % 0.86/1.04 (assume @p244 (forall @t338 (exists (@list @t389 @t388) (and (= @t389 @t133) (= @t388 @t390) (= (tptp.f8 (tptp.f9 tptp.f10 (tptp.f8 @t389 @t120)) @t388) (tptp.f8 @t389 (tptp.f8 @t354 @t388))))))) % 0.86/1.04 (assume @p245 (forall @t330 (exists (@list @t392 @t391) (and (= @t392 @t103) (= @t391 @t393) (= (tptp.f34 (tptp.f39 tptp.f52 (tptp.f34 @t392 @t64)) @t391) (tptp.f34 @t392 (tptp.f34 @t113 @t391))))))) % 0.86/1.04 (assume @p246 (forall @t273 (exists (@list @t394 @t395) (and (= @t394 (tptp.f4 tptp.f54 @t131)) (= @t395 @t326) (= (tptp.f3 @t394 (tptp.f3 @t395 @t272)) (tptp.f3 @t395 (tptp.f3 @t394 @t272))))))) % 0.86/1.04 (assume @p247 (forall @t22 (exists (@list @t396 @t397) (and (= @t396 (tptp.f49 tptp.f50 @t132)) (= @t397 @t298) (= (tptp.f22 @t396 (tptp.f22 @t397 @t13)) (tptp.f22 @t397 (tptp.f22 @t396 @t13))))))) % 0.86/1.04 (assume @p248 (forall @t338 (exists (@list @t398 @t399) (and (= @t398 (tptp.f9 tptp.f10 @t134)) (= @t399 @t337) (= (tptp.f8 @t398 (tptp.f8 @t399 @t333)) (tptp.f8 @t399 (tptp.f8 @t398 @t333))))))) % 0.86/1.04 (assume @p249 (forall @t330 (exists (@list @t400 @t401) (and (= @t400 (tptp.f39 tptp.f52 @t135)) (= @t401 @t304) (= (tptp.f34 @t400 (tptp.f34 @t401 @t327)) (tptp.f34 @t401 (tptp.f34 @t400 @t327))))))) % 0.86/1.04 (assume @p250 (forall @t273 (exists (@list @t402) (and (= @t402 @t130) (= (tptp.f3 (tptp.f4 tptp.f54 (tptp.f3 @t402 @t1)) @t384) (tptp.f3 (tptp.f4 tptp.f54 (tptp.f3 @t402 @t201)) (tptp.f3 @t352 @t272))))))) % 0.86/1.04 (assume @p251 (forall @t22 (exists (@list @t403) (and (= @t403 @t98) (= (tptp.f22 (tptp.f49 tptp.f50 (tptp.f22 @t403 @t14)) @t387) (tptp.f22 (tptp.f49 tptp.f50 (tptp.f22 @t403 @t16)) @t137)))))) % 0.86/1.04 (assume @p252 (forall @t338 (exists (@list @t404) (and (= @t404 @t133) (= (tptp.f8 (tptp.f9 tptp.f10 (tptp.f8 @t404 @t120)) @t390) (tptp.f8 (tptp.f9 tptp.f10 (tptp.f8 @t404 @t334)) (tptp.f8 @t354 @t333))))))) % 0.86/1.04 (assume @p253 (forall @t330 (exists (@list @t405) (and (= @t405 @t103) (= (tptp.f34 (tptp.f39 tptp.f52 (tptp.f34 @t405 @t64)) @t393) (tptp.f34 (tptp.f39 tptp.f52 (tptp.f34 @t405 @t99)) (tptp.f34 @t113 @t327))))))) % 0.86/1.04 (assume @p254 (forall @t67 (= @t95 (tptp.f34 @t101 @t39)))) % 0.86/1.04 (assume @p255 (forall @t34 (= @t112 (+ @t14 @t17)))) % 0.86/1.04 (assume @p256 (forall @t125 (= @t122 (+ @t120 @t121)))) % 0.86/1.04 (assume @p257 (forall @t104 (exists (@list @t406 @t407) (and (= @t406 @t78) (= @t407 @t101) (= (tptp.f34 @t406 (tptp.f34 @t407 @t99)) (tptp.f34 @t407 (tptp.f34 @t406 @t99))))))) % 0.86/1.04 (assume @p258 (forall @t72 (= @t408 (+ @t14 @t159)))) % 0.86/1.04 (assume @p259 (forall @t361 (= @t410 (+ @t120 @t347)))) % 0.86/1.04 (assume @p260 (forall @t104 (exists (@list @t411) (and (= @t411 @t78) (= (tptp.f34 @t411 @t102) (tptp.f34 (tptp.f39 tptp.f40 (tptp.f34 @t411 @t64)) @t99)))))) % 0.86/1.04 (assume @p261 (forall @t72 (= @t408 @t412))) % 0.86/1.04 (assume @p262 (forall @t361 (= @t410 @t413))) % 0.86/1.04 (assume @p263 (forall @t104 (exists (@list @t414) (and (= @t414 @t78) (= (tptp.f34 (tptp.f39 tptp.f40 (tptp.f34 @t414 @t64)) @t99) (tptp.f34 @t414 @t102)))))) % 0.86/1.04 (assume @p264 (forall @t72 (= @t412 @t408))) % 0.86/1.04 (assume @p265 (forall @t361 (= @t413 @t410))) % 0.86/1.04 (assume @p266 (forall @t104 (exists (@list @t415) (and (= @t415 @t78) (= (tptp.f34 (tptp.f39 tptp.f40 (tptp.f34 @t415 @t64)) @t99) (tptp.f34 (tptp.f39 tptp.f40 (tptp.f34 @t415 @t99)) @t64)))))) % 0.86/1.04 (assume @p267 (forall @t72 (= @t412 (+ @t159 @t14)))) % 0.86/1.04 (assume @p268 (forall @t361 (= @t413 (+ @t347 @t120)))) % 0.86/1.04 (assume @p269 (forall @t330 (exists (@list @t416) (and (= @t416 @t78) (= (tptp.f34 (tptp.f39 tptp.f40 (tptp.f34 @t416 @t64)) @t417) (tptp.f34 (tptp.f39 tptp.f40 (tptp.f34 @t416 @t99)) (tptp.f34 @t101 @t327))))))) % 0.86/1.04 (assume @p270 (forall @t22 (= (+ @t112 @t418) (+ @t159 @t157)))) % 0.86/1.04 (assume @p271 (forall @t338 (= (+ @t122 (+ @t334 @t333)) (+ @t347 (+ @t120 @t333))))) % 0.86/1.04 (assume @p272 (forall @t24 (exists (@list @t419) (and (= @t419 @t4) (= (tptp.f6 tptp.f7 (* 2 @t419)) (tptp.f6 tptp.f7 (+ @t419 @t419))))))) % 0.86/1.04 (assume @p273 (forall @t24 (exists (@list @t420) (and (= @t420 @t4) (= (tptp.f6 tptp.f7 (* @t420 2)) (tptp.f6 tptp.f7 (+ @t420 @t420))))))) % 0.86/1.04 (assume @p274 (forall @t8 (exists (@list @t424 @t422 @t421) (and (= @t424 @t33) (= @t422 @t4) (= @t421 @t2) (=> @t425 (= @t423 @t424)) (=> (not @t425) (= @t423 (tptp.f6 tptp.f7 (+ @t421 (tptp.f8 (tptp.f9 tptp.f10 (tptp.f11 tptp.f12 (tptp.f6 tptp.f7 (- @t422 1)))) @t421))))))))) % 0.86/1.04 (assume @p275 (forall @t203 (exists (@list @t426) (and (= @t426 @t130) (= (tptp.f3 @t426 (tptp.f3 (tptp.f4 tptp.f53 @t1) @t201)) (tptp.f3 (tptp.f4 tptp.f53 (tptp.f3 @t426 @t1)) (tptp.f3 @t426 @t201))))))) % 0.86/1.04 (assume @p276 (forall @t104 (exists (@list @t427) (and (= @t427 @t103) (= (tptp.f34 @t427 @t102) (tptp.f34 (tptp.f39 tptp.f40 (tptp.f34 @t427 @t64)) (tptp.f34 @t427 @t99))))))) % 0.86/1.04 (assume @p277 (forall @t72 (exists (@list @t428) (and (= @t428 @t98) (= (tptp.f22 @t428 @t97) (+ (tptp.f22 @t428 @t14) (tptp.f22 @t428 @t16))))))) % 0.86/1.04 (assume @p278 (forall @t361 (exists (@list @t429) (and (= @t429 @t133) (= (tptp.f8 @t429 @t409) (+ (tptp.f8 @t429 @t120) (tptp.f8 @t429 @t334))))))) % 0.86/1.04 (assume @p279 (forall @t273 (exists (@list @t431 @t430) (and (= @t431 @t130) (= @t430 @t352) (= (and (not @t27) (not (= @t201 @t272))) (not (= (tptp.f3 (tptp.f4 tptp.f53 (tptp.f3 @t431 @t201)) (tptp.f3 @t430 @t272)) (tptp.f3 (tptp.f4 tptp.f53 (tptp.f3 @t431 @t272)) (tptp.f3 @t430 @t201))))))))) % 0.86/1.04 (assume @p280 (forall @t330 (exists (@list @t433 @t432) (and (= @t433 @t103) (= @t432 @t113) (= (and (not @t65) (not (= @t99 @t327))) (not (= (tptp.f34 (tptp.f39 tptp.f40 (tptp.f34 @t433 @t99)) (tptp.f34 @t432 @t327)) (tptp.f34 (tptp.f39 tptp.f40 (tptp.f34 @t433 @t327)) (tptp.f34 @t432 @t99))))))))) % 0.86/1.04 (assume @p281 (forall @t22 (exists (@list @t435 @t434) (and (= @t435 @t98) (= @t434 @t109) (= (and (not @t68) (not (= @t16 @t13))) (not (= (+ (tptp.f22 @t435 @t16) (tptp.f22 @t434 @t13)) (+ (tptp.f22 @t435 @t13) (tptp.f22 @t434 @t16))))))))) % 0.86/1.04 (assume @p282 (forall @t338 (exists (@list @t437 @t436) (and (= @t437 @t133) (= @t436 @t354) (= (and (not (= @t121 @t120)) (not (= @t334 @t333))) (not (= (+ (tptp.f8 @t437 @t334) (tptp.f8 @t436 @t333)) (+ (tptp.f8 @t437 @t333) (tptp.f8 @t436 @t334))))))))) % 0.86/1.04 (assume @p283 (forall @t203 (= (tptp.f3 (tptp.f4 tptp.f54 @t127) @t201) (tptp.f3 (tptp.f4 tptp.f53 (tptp.f3 @t130 @t201)) @t365)))) % 0.86/1.04 (assume @p284 (forall @t361 (= (tptp.f8 (tptp.f9 tptp.f10 @t122) @t334) (+ (tptp.f8 @t133 @t334) @t368)))) % 0.86/1.04 (assume @p285 (forall @t203 (= (tptp.f3 @t341 @t340) @t339))) % 0.86/1.04 (assume @p286 (forall @t104 (= (tptp.f34 @t344 @t343) @t342))) % 0.86/1.04 (assume @p287 (forall @t72 (= (+ @t132 @t346) @t345))) % 0.86/1.04 (assume @p288 (forall @t361 (= (+ @t134 @t349) @t348))) % 0.86/1.04 (assume @p289 (forall @t41 (exists (@list @t438) (and (= @t438 @t439) (= @t286 (tptp.f16 tptp.f32 (+ (tptp.f19 (tptp.f59 tptp.f60 @t48) @t438) (tptp.f19 (tptp.f59 tptp.f60 @t75) @t438)))))))) % 0.86/1.04 (assume @p290 (forall @t41 (= (tptp.f34 @t440 @t50) (tptp.f34 (tptp.f39 tptp.f52 (tptp.f16 tptp.f32 (* 2/1 @t75))) tptp.f51)))) % 0.86/1.04 (assume @p291 (forall @t67 (= (tptp.f34 tptp.f62 @t95) (tptp.f34 (tptp.f39 tptp.f52 (tptp.f34 tptp.f62 @t39)) @t441)))) % 0.86/1.04 (assume @p292 (forall @t445 (exists (@list @t443) (and (= @t443 @t444) (= (tptp.f8 (tptp.f9 tptp.f10 (tptp.f11 @t443 @t1)) (tptp.f11 @t443 @t201)) (tptp.f11 @t443 @t442)))))) % 0.86/1.04 (assume @p293 (forall @t448 (exists (@list @t446) (and (= @t446 @t447) (= (tptp.f22 (tptp.f49 tptp.f50 (tptp.f19 @t446 @t1)) (tptp.f19 @t446 @t201)) (tptp.f19 @t446 @t442)))))) % 0.86/1.04 (assume @p294 (forall @t203 (exists (@list @t449) (and (= @t449 @t450) (= (tptp.f3 (tptp.f4 tptp.f54 (tptp.f3 @t449 @t1)) (tptp.f3 @t449 @t201)) (tptp.f3 @t449 @t442)))))) % 0.86/1.04 (assume @p295 (forall @t453 (exists (@list @t451) (and (= @t451 @t452) (= (tptp.f34 (tptp.f39 tptp.f52 (tptp.f13 @t451 @t1)) (tptp.f13 @t451 @t201)) (tptp.f13 @t451 @t442)))))) % 0.86/1.04 (assume @p296 (forall (@list @t121 @t120 @t201) (= (tptp.f11 (tptp.f63 tptp.f64 @t134) @t201) (tptp.f8 (tptp.f9 tptp.f10 (tptp.f11 @t444 @t201)) (tptp.f11 @t454 @t201))))) % 0.86/1.04 (assume @p297 (forall (@list @t17 @t14 @t201) (= (tptp.f19 (tptp.f59 tptp.f60 @t132) @t201) (tptp.f22 (tptp.f49 tptp.f50 (tptp.f19 @t447 @t201)) (tptp.f19 @t455 @t201))))) % 0.86/1.04 (assume @p298 (forall @t203 (= (tptp.f3 (tptp.f4 tptp.f65 @t131) @t201) (tptp.f3 (tptp.f4 tptp.f54 (tptp.f3 @t450 @t201)) (tptp.f3 @t456 @t201))))) % 0.86/1.04 (assume @p299 (forall (@list @t39 @t64 @t201) (= (tptp.f13 (tptp.f66 tptp.f67 @t135) @t201) (tptp.f34 (tptp.f39 tptp.f52 (tptp.f13 @t452 @t201)) (tptp.f13 @t457 @t201))))) % 0.86/1.04 (assume @p300 (forall @t445 (exists (@list @t459) (and (= @t459 @t444) (= (tptp.f11 (tptp.f63 tptp.f64 (tptp.f11 @t459 @t1)) @t201) (tptp.f11 @t459 @t458)))))) % 0.86/1.04 (assume @p301 (forall @t448 (exists (@list @t460) (and (= @t460 @t447) (= (tptp.f19 (tptp.f59 tptp.f60 (tptp.f19 @t460 @t1)) @t201) (tptp.f19 @t460 @t458)))))) % 0.86/1.04 (assume @p302 (forall @t203 (exists (@list @t461) (and (= @t461 @t450) (= (tptp.f3 (tptp.f4 tptp.f65 (tptp.f3 @t461 @t1)) @t201) (tptp.f3 @t461 @t458)))))) % 0.86/1.04 (assume @p303 (forall @t453 (exists (@list @t462) (and (= @t462 @t452) (= (tptp.f13 (tptp.f66 tptp.f67 (tptp.f13 @t462 @t1)) @t201) (tptp.f13 @t462 @t458)))))) % 0.86/1.04 (assume @p304 (forall @t465 (exists (@list @t464) (and (= @t464 @t444) (= (tptp.f8 (tptp.f9 tptp.f10 (tptp.f11 @t464 @t1)) @t121) (tptp.f11 @t464 @t463)))))) % 0.86/1.04 (assume @p305 (forall @t467 (exists (@list @t466) (and (= @t466 @t447) (= (tptp.f22 (tptp.f49 tptp.f50 (tptp.f19 @t466 @t1)) @t17) (tptp.f19 @t466 @t463)))))) % 0.86/1.04 (assume @p306 (forall @t8 (exists (@list @t468) (and (= @t468 @t450) (= (tptp.f3 (tptp.f4 tptp.f54 (tptp.f3 @t468 @t1)) @t3) (tptp.f3 @t468 @t463)))))) % 0.86/1.04 (assume @p307 (forall @t470 (exists (@list @t469) (and (= @t469 @t452) (= (tptp.f34 (tptp.f39 tptp.f52 (tptp.f13 @t469 @t1)) @t39) (tptp.f13 @t469 @t463)))))) % 0.86/1.04 (assume @p308 (forall @t465 (exists (@list @t471) (and (= @t471 @t444) (= (tptp.f11 @t471 @t473) (tptp.f11 (tptp.f63 tptp.f64 (tptp.f11 @t471 @t1)) @t439)))))) % 0.86/1.04 (assume @p309 (forall @t467 (exists (@list @t474) (and (= @t474 @t447) (= (tptp.f19 @t474 @t473) (tptp.f19 (tptp.f59 tptp.f60 (tptp.f19 @t474 @t1)) @t439)))))) % 0.86/1.04 (assume @p310 (forall @t8 (exists (@list @t475) (and (= @t475 @t450) (= (tptp.f3 @t475 @t473) (tptp.f3 (tptp.f4 tptp.f65 (tptp.f3 @t475 @t1)) @t439)))))) % 0.86/1.04 (assume @p311 (forall @t470 (exists (@list @t476) (and (= @t476 @t452) (= (tptp.f13 @t476 @t473) (tptp.f13 (tptp.f66 tptp.f67 (tptp.f13 @t476 @t1)) @t439)))))) % 0.86/1.04 (assume @p312 (forall @t465 (exists (@list @t477) (and (= @t477 @t444) (= (tptp.f8 @t133 (tptp.f11 @t477 @t1)) (tptp.f11 @t477 @t463)))))) % 0.86/1.04 (assume @p313 (forall @t467 (exists (@list @t478) (and (= @t478 @t447) (= (tptp.f22 @t98 (tptp.f19 @t478 @t1)) (tptp.f19 @t478 @t463)))))) % 0.86/1.04 (assume @p314 (forall @t8 (exists (@list @t479) (and (= @t479 @t450) (= (tptp.f3 @t130 (tptp.f3 @t479 @t1)) (tptp.f3 @t479 @t463)))))) % 0.86/1.04 (assume @p315 (forall @t470 (exists (@list @t480) (and (= @t480 @t452) (= (tptp.f34 @t103 (tptp.f13 @t480 @t1)) (tptp.f13 @t480 @t463)))))) % 0.86/1.04 (assume @p316 (forall @t313 (= (tptp.f11 @t444 @t481) (tptp.f8 (tptp.f9 tptp.f10 @t372) @t121)))) % 0.86/1.04 (assume @p317 (forall @t46 (= (tptp.f19 @t447 @t481) (tptp.f22 (tptp.f49 tptp.f50 @t370) @t17)))) % 0.86/1.04 (assume @p318 (forall @t24 (= (tptp.f3 @t450 @t481) (tptp.f3 (tptp.f4 tptp.f54 @t482) @t3)))) % 0.86/1.04 (assume @p319 (forall @t41 (= (tptp.f13 @t452 @t481) (tptp.f34 (tptp.f39 tptp.f52 @t483) @t39)))) % 0.86/1.04 (assume @p320 (forall @t313 (= @t484 @t372))) % 0.86/1.04 (assume @p321 (forall @t46 (= @t485 @t370))) % 0.86/1.04 (assume @p322 (forall @t24 (= @t486 @t482))) % 0.86/1.04 (assume @p323 (forall @t41 (= @t487 @t483))) % 0.86/1.04 (assume @p324 (forall @t465 (exists (@list @t488) (and (= @t488 @t444) (= (tptp.f11 @t488 @t463) (tptp.f8 @t133 (tptp.f11 @t488 @t1))))))) % 0.86/1.04 (assume @p325 (forall @t467 (exists (@list @t489) (and (= @t489 @t447) (= (tptp.f19 @t489 @t463) (tptp.f22 @t98 (tptp.f19 @t489 @t1))))))) % 0.86/1.04 (assume @p326 (forall @t8 (exists (@list @t490) (and (= @t490 @t450) (= (tptp.f3 @t490 @t463) (tptp.f3 @t130 (tptp.f3 @t490 @t1))))))) % 0.86/1.04 (assume @p327 (forall @t470 (exists (@list @t491) (and (= @t491 @t452) (= (tptp.f13 @t491 @t463) (tptp.f34 @t103 (tptp.f13 @t491 @t1))))))) % 0.86/1.04 (assume @p328 (forall @t313 (= @t372 @t484))) % 0.86/1.04 (assume @p329 (forall @t46 (= @t370 @t485))) % 0.86/1.04 (assume @p330 (forall @t24 (= @t482 @t486))) % 0.86/1.04 (assume @p331 (forall @t41 (= @t483 @t487))) % 0.86/1.04 (assume @p332 (forall @t313 (exists (@list @t492) (and (= @t492 @t484) (= (tptp.f8 tptp.f21 @t492) @t492))))) % 0.86/1.04 (assume @p333 (forall @t46 (exists (@list @t493) (and (= @t493 @t485) (= (tptp.f22 tptp.f23 @t493) @t493))))) % 0.86/1.04 (assume @p334 (forall @t313 (= (tptp.f11 @t444 @t192) @t121))) % 0.86/1.04 (assume @p335 (forall @t46 (= (tptp.f19 @t447 @t192) @t17))) % 0.86/1.04 (assume @p336 (forall @t24 (= (tptp.f3 @t450 @t192) @t3))) % 0.86/1.04 (assume @p337 (forall @t41 (= (tptp.f13 @t452 @t192) @t39))) % 0.86/1.04 (assume @p338 (forall @t313 (exists (@list @t494) (and (= @t494 @t439) (= (tptp.f11 @t495 @t494) (tptp.f11 @t444 @t494)))))) % 0.86/1.04 (assume @p339 (forall @t46 (exists (@list @t496) (and (= @t496 @t439) (= (tptp.f19 @t497 @t496) (tptp.f19 @t447 @t496)))))) % 0.86/1.04 (assume @p340 (forall @t467 (= (tptp.f22 tptp.f33 @t498) (tptp.f19 (tptp.f59 tptp.f60 @t60) @t1)))) % 0.86/1.04 (assume @p341 (forall @t467 (= (tptp.f16 tptp.f32 @t498) (tptp.f13 (tptp.f66 tptp.f67 @t49) @t1)))) % 0.86/1.04 (assume @p342 (forall @t467 (= @t500 @t499))) % 0.86/1.04 (assume @p343 (forall @t470 (= @t504 @t502))) % 0.86/1.04 (assume @p344 (forall @t467 (<= @t500 @t499))) % 0.86/1.04 (assume @p345 (forall @t470 (<= @t504 @t502))) % 0.86/1.04 (assume @p346 (forall @t67 (= (tptp.f34 tptp.f35 @t505) (tptp.f34 (tptp.f39 tptp.f61 @t50) @t66)))) % 0.86/1.04 (assume @p347 (forall @t22 (= (tptp.f34 (tptp.f39 tptp.f61 @t21) @t19) (tptp.f16 (tptp.f17 tptp.f18 @t507) @t506)))) % 0.86/1.04 (assume @p348 (forall @t67 (= (tptp.f27 tptp.f36 @t505) (- @t75 @t93)))) % 0.86/1.04 (assume @p349 (forall @t67 (= (tptp.f27 tptp.f28 @t505) (- @t48 @t152)))) % 0.86/1.05 (assume @p350 (forall @t34 (= (tptp.f22 tptp.f33 @t508) (- @t60 @t70)))) % 0.86/1.05 (assume @p351 (forall @t34 (= (tptp.f16 tptp.f32 @t508) (tptp.f34 (tptp.f39 tptp.f61 @t49) @t69)))) % 0.86/1.05 (assume @p352 (forall @t34 (exists (@list @t509) (and (= @t509 @t439) (= (tptp.f19 (tptp.f59 tptp.f60 @t112) @t509) (+ (+ (tptp.f19 @t447 @t509) (tptp.f19 @t455 @t509)) (tptp.f22 (tptp.f49 tptp.f50 (* 2/1 @t17)) @t14))))))) % 0.86/1.05 (assume @p353 (forall @t34 (= @t510 (tptp.f22 tptp.f30 (- @t14 @t17))))) % 0.86/1.05 (assume @p354 (forall @t67 (= @t512 (tptp.f27 tptp.f31 (tptp.f34 @t511 @t39))))) % 0.86/1.05 (assume @p355 (forall @t34 (<= @t510 @t164))) % 0.86/1.05 (assume @p356 (forall @t67 (<= @t512 @t163))) % 0.86/1.05 (assume @p357 (forall @t34 (exists (@list @t513) (and (= @t513 @t162) (=> @t514 (<= (- @t513) @t510)) (=> (not @t514) (<= @t513 @t510)))))) % 0.86/1.05 (assume @p358 (forall @t67 (exists (@list @t515) (and (= @t515 @t160) (=> @t516 (<= (- @t515) @t512)) (=> (not @t516) (<= @t515 @t512)))))) % 0.86/1.05 (assume @p359 (forall @t34 (<= @t162 @t510))) % 0.86/1.05 (assume @p360 (forall @t67 (<= @t160 @t512))) % 0.86/1.05 (assume @p361 (forall @t8 (exists (@list @t518 @t517) (and (= @t518 @t2) (= @t517 @t4) (=> (<= @t517 @t518) (= (tptp.f19 tptp.f20 (tptp.f6 tptp.f7 (- @t518 @t517))) (- @t28 @t26))))))) % 0.86/1.05 (assume @p362 (forall @t8 (exists (@list @t520 @t521) (and (= @t520 @t2) (= @t521 @t4) (exists (@list @t519) (and (= @t519 (- @t520 @t521)) (=> (<= @t521 @t520) (= (tptp.f11 tptp.f12 (tptp.f6 tptp.f7 @t519)) @t519)))))))) % 0.86/1.05 (assume @p363 (forall @t8 (exists (@list @t523 @t522) (and (= @t523 @t2) (= @t522 @t4) (=> (<= @t522 @t523) (= (tptp.f13 tptp.f14 (tptp.f6 tptp.f7 (- @t523 @t522))) (tptp.f34 (tptp.f39 tptp.f61 @t29) @t30))))))) % 0.86/1.05 (assume @p364 (forall @t72 (= (tptp.f22 @t524 @t16) (- @t111 @t110)))) % 0.86/1.05 (assume @p365 (forall @t104 (= (tptp.f34 @t525 @t99) (tptp.f34 (tptp.f39 tptp.f61 @t115) @t114)))) % 0.86/1.05 (assume @p366 (forall @t72 (exists (@list @t526) (and (= @t526 @t98) (= (tptp.f22 @t526 @t527) (- (tptp.f22 @t526 @t14) (tptp.f22 @t526 @t16))))))) % 0.86/1.05 (assume @p367 (forall @t104 (exists (@list @t528) (and (= @t528 @t103) (= (tptp.f34 @t528 @t529) (tptp.f34 (tptp.f39 tptp.f61 (tptp.f34 @t528 @t64)) (tptp.f34 @t528 @t99))))))) % 0.86/1.05 (assume @p368 (forall @t72 (exists (@list @t530) (and (= @t530 @t98) (= (tptp.f22 @t530 @t527) (- (tptp.f22 @t530 @t14) (tptp.f22 @t530 @t16))))))) % 0.86/1.05 (assume @p369 (forall @t104 (exists (@list @t531) (and (= @t531 @t103) (= (tptp.f34 @t531 @t529) (tptp.f34 (tptp.f39 tptp.f61 (tptp.f34 @t531 @t64)) (tptp.f34 @t531 @t99))))))) % 0.86/1.05 (assume @p370 (forall @t330 (exists (@list @t533 @t534 @t532) (and (= @t533 @t304) (= @t534 @t537) (= @t532 @t535) (= (tptp.f34 (tptp.f39 tptp.f61 @t135) (tptp.f34 @t533 @t327)) (tptp.f34 (tptp.f39 tptp.f40 (tptp.f34 (tptp.f39 tptp.f40 (tptp.f34 @t534 @t532)) (tptp.f34 @t534 @t327))) (tptp.f34 @t533 @t532))))))) % 0.86/1.05 (assume @p371 (forall @t22 (exists (@list @t539 @t540 @t538) (and (= @t539 @t298) (= @t540 @t541) (= @t538 @t506) (= (- @t132 (tptp.f22 @t539 @t13)) (+ (+ (tptp.f22 @t540 @t538) (tptp.f22 @t540 @t13)) (tptp.f22 @t539 @t538))))))) % 0.86/1.05 (assume @p372 (forall @t544 (= @t543 (= @t99 (tptp.f34 (tptp.f39 tptp.f40 (tptp.f34 (tptp.f39 tptp.f52 (tptp.f34 (tptp.f39 tptp.f61 @t327) @t39)) @t64)) @t542))))) % 0.86/1.05 (assume @p373 (forall @t547 (= @t546 (= @t16 (+ (tptp.f22 (tptp.f49 tptp.f50 (- @t13 @t17)) @t14) @t545))))) % 0.86/1.05 (assume @p374 (forall @t550 (= @t549 (= @t334 (+ (tptp.f8 (tptp.f9 tptp.f10 (- @t333 @t121)) @t120) @t548))))) % 0.86/1.05 (assume @p375 (forall @t544 (= @t543 (= (tptp.f34 (tptp.f39 tptp.f40 (tptp.f34 (tptp.f39 tptp.f52 (tptp.f34 @t440 @t327)) @t64)) @t99) @t542)))) % 0.86/1.05 (assume @p376 (forall @t547 (= @t546 (= (+ (tptp.f22 (tptp.f49 tptp.f50 (- @t17 @t13)) @t14) @t16) @t545)))) % 0.86/1.05 (assume @p377 (forall @t550 (= @t549 (= (+ (tptp.f8 (tptp.f9 tptp.f10 (- @t121 @t333)) @t120) @t334) @t548)))) % 0.86/1.05 (assume @p378 (forall @t330 (<= (tptp.f27 tptp.f31 (tptp.f34 (tptp.f39 tptp.f61 @t95) @t417)) (+ (tptp.f27 tptp.f31 @t536) (tptp.f27 tptp.f31 @t535))))) % 0.86/1.05 (assume @p379 (forall @t22 (<= (tptp.f22 tptp.f30 (- @t112 @t418)) (+ (tptp.f22 tptp.f30 @t507) (tptp.f22 tptp.f30 @t506))))) % 0.86/1.05 (assume @p380 (forall @t465 (exists (@list @t552) (and (= @t552 @t444) (exists (@list @t551) (and (= @t551 (tptp.f11 @t552 @t1)) (= (tptp.f11 @t552 @t473) (tptp.f8 (tptp.f9 tptp.f10 @t551) @t551)))))))) % 0.86/1.05 (assume @p381 (forall @t467 (exists (@list @t554) (and (= @t554 @t447) (exists (@list @t553) (and (= @t553 (tptp.f19 @t554 @t1)) (= (tptp.f19 @t554 @t473) (tptp.f22 (tptp.f49 tptp.f50 @t553) @t553)))))))) % 0.86/1.05 (assume @p382 (forall @t8 (exists (@list @t556) (and (= @t556 @t450) (exists (@list @t555) (and (= @t555 (tptp.f3 @t556 @t1)) (= (tptp.f3 @t556 @t473) (tptp.f3 (tptp.f4 tptp.f54 @t555) @t555)))))))) % 0.86/1.05 (assume @p383 (forall @t470 (exists (@list @t558) (and (= @t558 @t452) (exists (@list @t557) (and (= @t557 (tptp.f13 @t558 @t1)) (= (tptp.f13 @t558 @t473) (tptp.f34 (tptp.f39 tptp.f52 @t557) @t557)))))))) % 0.86/1.05 (assume @p384 (forall @t465 (exists (@list @t561) (and (= @t561 @t444) (exists (@list @t559) (and (= @t559 (tptp.f11 @t561 @t1)) (= (tptp.f11 @t561 @t560) (tptp.f8 @t133 (tptp.f8 (tptp.f9 tptp.f10 @t559) @t559))))))))) % 0.86/1.05 (assume @p385 (forall @t467 (exists (@list @t563) (and (= @t563 @t447) (exists (@list @t562) (and (= @t562 (tptp.f19 @t563 @t1)) (= (tptp.f19 @t563 @t560) (tptp.f22 @t98 (tptp.f22 (tptp.f49 tptp.f50 @t562) @t562))))))))) % 0.86/1.05 (assume @p386 (forall @t8 (exists (@list @t565) (and (= @t565 @t450) (exists (@list @t564) (and (= @t564 (tptp.f3 @t565 @t1)) (= (tptp.f3 @t565 @t560) (tptp.f3 @t130 (tptp.f3 (tptp.f4 tptp.f54 @t564) @t564))))))))) % 0.86/1.05 (assume @p387 (forall @t470 (exists (@list @t567) (and (= @t567 @t452) (exists (@list @t566) (and (= @t566 (tptp.f13 @t567 @t1)) (= (tptp.f13 @t567 @t560) (tptp.f34 @t103 (tptp.f34 (tptp.f39 tptp.f52 @t566) @t566))))))))) % 0.86/1.05 (assume @p388 (forall @t465 (exists (@list @t568) (and (= @t568 @t444) (= (tptp.f11 @t568 @t560) (tptp.f8 @t133 (tptp.f11 (tptp.f63 tptp.f64 (tptp.f11 @t568 @t1)) @t439))))))) % 0.86/1.05 (assume @p389 (forall @t467 (exists (@list @t569) (and (= @t569 @t447) (= (tptp.f19 @t569 @t560) (tptp.f22 @t98 (tptp.f19 (tptp.f59 tptp.f60 (tptp.f19 @t569 @t1)) @t439))))))) % 0.86/1.05 (assume @p390 (forall @t8 (exists (@list @t570) (and (= @t570 @t450) (= (tptp.f3 @t570 @t560) (tptp.f3 @t130 (tptp.f3 (tptp.f4 tptp.f65 (tptp.f3 @t570 @t1)) @t439))))))) % 0.86/1.05 (assume @p391 (forall @t470 (exists (@list @t571) (and (= @t571 @t452) (= (tptp.f13 @t571 @t560) (tptp.f34 @t103 (tptp.f13 (tptp.f66 tptp.f67 (tptp.f13 @t571 @t1)) @t439))))))) % 0.86/1.05 (assume @p392 (forall @t41 (= (tptp.f27 tptp.f31 @t286) (tptp.f19 @t501 @t439)))) % 0.86/1.05 (assume @p393 (forall @t67 (exists (@list @t572) (and (= @t572 @t573) (= (tptp.f34 (tptp.f39 tptp.f61 (tptp.f13 @t452 @t572)) (tptp.f13 @t457 @t572)) (tptp.f34 @t525 @t95)))))) % 0.86/1.05 (assume @p394 (forall @t34 (exists (@list @t574) (and (= @t574 @t573) (= (- (tptp.f19 @t447 @t574) (tptp.f19 @t455 @t574)) (tptp.f22 @t524 @t112)))))) % 0.86/1.05 (assume @p395 (forall @t125 (exists (@list @t575) (and (= @t575 @t573) (= (- (tptp.f11 @t444 @t575) (tptp.f11 @t454 @t575)) (tptp.f8 (tptp.f9 tptp.f10 (- @t121 @t120)) @t122)))))) % 0.86/1.05 (assume @p396 (forall @t330 (exists (@list @t576) (and (= @t576 @t103) (= (tptp.f34 (tptp.f39 tptp.f61 (tptp.f34 @t576 @t64)) @t393) (tptp.f34 (tptp.f39 tptp.f40 (tptp.f34 @t576 @t535)) (tptp.f34 @t537 @t327))))))) % 0.86/1.05 (assume @p397 (forall @t22 (exists (@list @t577) (and (= @t577 @t98) (= (- (tptp.f22 @t577 @t14) @t387) (+ (tptp.f22 @t577 @t506) (tptp.f22 @t541 @t13))))))) % 0.86/1.05 (assume @p398 (forall @t338 (exists (@list @t578) (and (= @t578 @t133) (= (- (tptp.f8 @t578 @t120) @t390) (+ (tptp.f8 @t578 (- @t120 @t333)) (tptp.f8 (tptp.f9 tptp.f10 (- @t121 @t334)) @t333))))))) % 0.86/1.05 (assume @p399 (forall @t41 (exists (@list @t64 @t16) (= @t39 (tptp.f34 (tptp.f39 tptp.f52 @t71) @t441))))) % 0.86/1.05 (assume @p400 (forall @t8 (exists (@list @t579) (and (= @t579 @t450) (=> @t243 (= @t580 @t192)) (=> (not @t243) (= @t580 (tptp.f6 tptp.f7 (tptp.f8 @t5 (tptp.f11 tptp.f12 (tptp.f3 @t579 (tptp.f6 tptp.f7 (- @t2 1)))))))))))) % 0.86/1.05 (assume @p401 (forall @t470 (= (tptp.f34 tptp.f35 @t503) (tptp.f13 (tptp.f66 tptp.f67 @t50) @t1)))) % 0.86/1.05 (assume @p402 (forall @t34 (<= (- @t370) @t581))) % 0.86/1.05 (assume @p403 (forall @t72 (exists (@list @t582) (and (= @t582 @t98) (= (tptp.f22 (tptp.f49 tptp.f50 (tptp.f22 @t582 @t14)) @t16) (tptp.f22 @t582 @t110)))))) % 0.86/1.05 (assume @p404 (forall @t34 (exists (@list @t583) (and (= @t583 0/1) (= (= (+ @t370 @t581) @t583) (and (= @t17 @t583) (= @t14 @t583))))))) % 0.86/1.05 (assume @p405 (forall @t72 (=> @t585 (= (= @t353 @t299) @t584)))) % 0.86/1.05 (assume @p406 (forall @t72 (exists (@list @t586) (and (= @t586 @t98) (=> @t585 (= (= (tptp.f22 @t586 @t14) (tptp.f22 @t586 @t16)) @t584)))))) % 0.86/1.05 (assume @p407 (forall @t72 (=> @t87 (= (< @t353 @t299) @t587)))) % 0.86/1.05 (assume @p408 (forall @t72 (=> @t87 (= (<= @t353 @t299) @t588)))) % 0.86/1.05 (assume @p409 (forall @t72 (exists (@list @t589) (and (= @t589 @t98) (=> @t87 (= (<= (tptp.f22 @t589 @t14) (tptp.f22 @t589 @t16)) @t588)))))) % 0.86/1.05 (assume @p410 (forall @t34 (exists (@list @t590) (and (= @t590 0/1) (=> (< @t590 @t17) (=> (< @t590 @t14) (< @t590 @t132))))))) % 0.86/1.05 (assume @p411 (forall @t72 (exists (@list @t591) (and (= @t591 @t98) (=> @t87 (=> @t587 (< (tptp.f22 @t591 @t14) (tptp.f22 @t591 @t16)))))))) % 0.86/1.05 (assume @p412 (forall @t24 (<= 1/1 (tptp.f19 (tptp.f59 tptp.f60 2/1) @t3)))) % 0.86/1.05 (assume @p413 (forall @t34 (exists (@list @t592) (and (= @t592 @t439) (<= (- (tptp.f19 @t447 @t592)) (tptp.f19 @t455 @t592)))))) % 0.86/1.05 (assume @p414 (forall @t34 (exists (@list @t593 @t594) (and (= @t593 0/1) (= @t594 @t439) (= (= (+ (tptp.f19 @t447 @t594) (tptp.f19 @t455 @t594)) @t593) (and (= @t17 @t593) (= @t14 @t593))))))) % 0.86/1.05 (assume @p415 (forall (@list @t3 @t120) (exists (@list @t596 @t595) (and (= @t596 @t4) (= @t595 @t454) (=> (< 0 @t596) (= (tptp.f8 (tptp.f9 tptp.f10 (tptp.f11 @t595 (tptp.f6 tptp.f7 (- @t596 1)))) @t120) (tptp.f11 @t595 @t3))))))) % 0.86/1.05 (assume @p416 (forall (@list @t3 @t14) (exists (@list @t598 @t597) (and (= @t598 @t4) (= @t597 @t455) (=> (< 0 @t598) (= (tptp.f22 (tptp.f49 tptp.f50 (tptp.f19 @t597 (tptp.f6 tptp.f7 (- @t598 1)))) @t14) (tptp.f19 @t597 @t3))))))) % 0.86/1.05 (assume @p417 (forall @t8 (exists (@list @t600 @t599) (and (= @t600 @t4) (= @t599 @t456) (=> (< 0 @t600) (= (tptp.f3 (tptp.f4 tptp.f54 (tptp.f3 @t599 (tptp.f6 tptp.f7 (- @t600 1)))) @t1) (tptp.f3 @t599 @t3))))))) % 0.86/1.05 (assume @p418 (forall (@list @t3 @t64) (exists (@list @t602 @t601) (and (= @t602 @t4) (= @t601 @t457) (=> (< 0 @t602) (= (tptp.f34 (tptp.f39 tptp.f52 (tptp.f13 @t601 (tptp.f6 tptp.f7 (- @t602 1)))) @t64) (tptp.f13 @t601 @t3))))))) % 0.86/1.05 (assume @p419 (forall @t445 (exists (@list @t603) (and (= @t603 @t444) (= (tptp.f11 @t603 @t458) (tptp.f11 (tptp.f63 tptp.f64 (tptp.f11 @t603 @t1)) @t201)))))) % 0.86/1.05 (assume @p420 (forall @t448 (exists (@list @t604) (and (= @t604 @t447) (= (tptp.f19 @t604 @t458) (tptp.f19 (tptp.f59 tptp.f60 (tptp.f19 @t604 @t1)) @t201)))))) % 0.86/1.05 (assume @p421 (forall @t203 (exists (@list @t605) (and (= @t605 @t450) (= (tptp.f3 @t605 @t458) (tptp.f3 (tptp.f4 tptp.f65 (tptp.f3 @t605 @t1)) @t201)))))) % 0.86/1.05 (assume @p422 (forall @t453 (exists (@list @t606) (and (= @t606 @t452) (= (tptp.f13 @t606 @t458) (tptp.f13 (tptp.f66 tptp.f67 (tptp.f13 @t606 @t1)) @t201)))))) % 0.86/1.05 (assume @p423 (forall @t8 (= @t608 (tptp.f11 (tptp.f63 tptp.f64 @t4) @t1)))) % 0.86/1.05 (assume @p424 (forall @t8 (= (tptp.f19 tptp.f20 @t607) (tptp.f19 (tptp.f59 tptp.f60 @t26) @t1)))) % 0.86/1.05 (assume @p425 (forall @t8 (= (tptp.f3 tptp.f24 @t607) (tptp.f3 (tptp.f4 tptp.f65 @t32) @t1)))) % 0.86/1.05 (assume @p426 (forall @t8 (= (tptp.f13 tptp.f14 @t607) (tptp.f13 (tptp.f66 tptp.f67 @t30) @t1)))) % 0.86/1.05 (assume @p427 (forall @t8 (exists (@list @t609) (and (= @t609 @t210) (=> (<= @t609 @t4) (<= @t609 @t608)))))) % 0.86/1.05 (assume @p428 (forall @t203 (exists (@list @t610) (and (= @t610 @t450) (=> @t611 (=> (< (tptp.f11 tptp.f12 (tptp.f3 @t610 @t1)) (tptp.f11 tptp.f12 (tptp.f3 @t610 @t201))) (< @t2 @t202))))))) % 0.86/1.05 (assume @p429 (forall @t8 (exists (@list @t612) (and (= @t612 @t225) (= (= @t607 @t612) (or @t243 (= @t3 @t612))))))) % 0.86/1.05 (assume @p430 (forall @t24 (exists (@list @t613) (and (= @t613 @t225) (= (tptp.f3 (tptp.f4 tptp.f65 @t613) @t3) @t613))))) % 0.86/1.05 (assume @p431 (forall @t8 (= (< 0 @t608) (or @t611 @t243)))) % 0.86/1.05 (assume @p432 (forall @t465 (= (tptp.f8 tptp.f21 (tptp.f11 @t444 @t1)) (tptp.f11 @t495 @t1)))) % 0.86/1.05 (assume @p433 (forall @t467 (= (tptp.f22 tptp.f23 @t498) (tptp.f19 @t497 @t1)))) % 0.86/1.05 (assume @p434 (forall @t24 (= (tptp.f6 tptp.f7 @t4) @t3))) % 0.86/1.05 (assume @p435 (forall @t313 (=> @t318 (= @t323 @t121)))) % 0.86/1.05 (assume @p436 (forall @t313 (=> (< @t121 0) (= @t323 0)))) % 0.86/1.05 (step @p437 :rule instantiate :premises (@p57) :args (@t614)) % 0.86/1.05 (step @p438 :rule arith_poly_norm :args ((= (* 1/1 (- @t35 @t26)) (* -1/1 (- @t26 @t35))))) % 0.86/1.05 (step @p439 :rule arith_poly_norm_rel :premises (@p438) :args ((= @t36 (= @t26 @t35)))) % 0.86/1.05 (step @p440 :rule cong :premises (@p439) :args (@t37)) % 0.86/1.05 (step @p441 :rule eq_resolve :premises (@p12 @p440)) % 0.86/1.05 (step @p442 :rule instantiate :premises (@p441) :args (@t614)) % 0.86/1.05 (step @p443 :rule eq-symm :args (@t79 @t39)) % 0.86/1.05 (step @p444 :rule cong :premises (@p443) :args (@t80)) % 0.86/1.05 (step @p445 :rule eq_resolve :premises (@p46 @p444)) % 0.86/1.05 (step @p446 :rule instantiate :premises (@p445) :args ((@list @t10))) % 0.86/1.05 (step @p447 :rule refl :args (@t620)) % 0.86/1.05 (step @p448 :rule refl :args (@t622)) % 0.86/1.05 (step @p449 :rule refl :args (@t624)) % 0.86/1.05 (step @p450 :rule bool-double-not-elim :args (@t11)) % 0.86/1.05 (step @p451 :rule nary_cong :premises (@p450 @p449 @p448 @p447) :args ((or (not @t12) @t624 @t622 @t620))) % 0.86/1.05 (assume-push @p487 @t619) % 0.86/1.05 (assume-push @p488 @t620) % 0.86/1.05 (step @p454 :rule evaluate :args ((= false true))) % 0.86/1.05 (step @p455 :rule true_intro :premises (@p446)) % 0.86/1.05 (step @p456 :rule false_intro :premises (@p3)) % 0.86/1.05 (step @p457 :rule symm :premises (@p442)) % 0.86/1.05 (step @p458 :rule refl :args (tptp.f18)) % 0.86/1.05 (step @p459 :rule cong :premises (@p458 @p457) :args (@t617)) % 0.86/1.05 (step @p460 :rule cong :premises (@p459 @p437) :args (@t618)) % 0.86/1.05 (step @p461 :rule refl :args (@t10)) % 0.86/1.05 (step @p462 :rule cong :premises (@p461 @p460) :args (@t619)) % 0.86/1.05 (step @p463 :rule trans :premises (@p462 @p456)) % 0.86/1.05 (step @p464 :rule symm :premises (@p463)) % 0.86/1.05 (step @p465 :rule trans :premises (@p464 @p455)) % 0.86/1.05 (step @p466 false :rule eq_resolve :premises (@p465 @p454)) % 0.86/1.05 (step-pop @p489 :rule scope :premises (@p466)) % 0.86/1.05 (step-pop @p490 :rule scope :premises (@p489)) % 0.86/1.05 (step @p467 :rule process_scope :premises (@p490) :args (false)) % 0.86/1.05 (assume-push @p491 @t12) % 0.86/1.05 (assume-push @p492 @t623) % 0.86/1.05 (assume-push @p493 @t621) % 0.86/1.05 (assume-push @p494 @t619) % 0.86/1.05 (step @p456 :rule false_intro :premises (@p3)) % 0.86/1.05 (step @p457 :rule symm :premises (@p442)) % 0.86/1.05 (step @p458 :rule refl :args (tptp.f18)) % 0.86/1.05 (step @p459 :rule cong :premises (@p458 @p457) :args (@t617)) % 0.86/1.05 (step @p460 :rule cong :premises (@p459 @p437) :args (@t618)) % 0.86/1.05 (step @p461 :rule refl :args (@t10)) % 0.86/1.05 (step @p462 :rule cong :premises (@p461 @p460) :args (@t619)) % 0.86/1.05 (step @p474 :rule trans :premises (@p462 @p456)) % 0.86/1.05 (step @p475 :rule false_elim :premises (@p474)) % 0.86/1.05 (step @p476 :rule and_intro :premises (@p446 @p475)) % 0.86/1.05 (step-pop @p495 :rule scope :premises (@p476)) % 0.86/1.05 (step-pop @p496 :rule scope :premises (@p495)) % 0.86/1.05 (step-pop @p497 :rule scope :premises (@p496)) % 0.86/1.05 (step-pop @p498 :rule scope :premises (@p497)) % 0.86/1.05 (step @p477 :rule process_scope :premises (@p498) :args (@t625)) % 0.86/1.05 (step @p482 :rule implies_elim :premises (@p477)) % 0.86/1.05 (step @p483 :rule resolution :premises (@p482 @p467) :args (true @t625)) % 0.86/1.05 (step @p484 :rule not_and :premises (@p483)) % 0.86/1.05 (step @p485 :rule eq_resolve :premises (@p484 @p451)) % 0.86/1.05 (step @p486 false :rule chain_m_resolution :premises (@p485 @p446 @p442 @p437 @p3) :args (false (@list false false false true) (@list @t619 @t621 @t623 @t11))) % 0.86/1.05 ) % 0.86/1.05 % SZS output end Proof % 0.86/1.05 % cvc5 exiting %------------------------------------------------------------------------------