%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ITP409_1 : TPTP v9.2.1. Released v8.1.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n013.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jun 3 08:26:30 AM UTC 2026 % Result : Theorem 0.48s 0.93s % Output : Proof 0.48s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP409_1 : TPTP v9.2.1. Released v8.1.0. % 0.00/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.17/0.34 % Computer : n013.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.34 % DateTime : Tue Jun 2 05:08:30 EDT 2026 % 0.17/0.34 % CPUTime : % 0.39/0.65 %----Proving TF0_ARI % 0.48/0.93 --- Run --finite-model-find --decision=internal at 45... % 0.48/0.93 % SZS status Theorem % 0.48/0.93 % SZS output start Proof % 0.48/0.93 ( % 0.48/0.93 (declare-sort tptp.tlbool 0) % 0.48/0.93 (declare-sort |tptp.'Int_nat_fun$'| 0) % 0.48/0.93 (declare-sort |tptp.'Nat_nat_bool_fun_fun$'| 0) % 0.48/0.93 (declare-sort |tptp.'Nat_nat_fun$'| 0) % 0.48/0.93 (declare-sort |tptp.'Nat_bool_fun$'| 0) % 0.48/0.93 (declare-sort |tptp.'Nat$'| 0) % 0.48/0.93 (declare-sort |tptp.'Int_int_fun$'| 0) % 0.48/0.93 (declare-sort |tptp.'Int_int_bool_fun_fun$'| 0) % 0.48/0.93 (declare-sort |tptp.'Int_bool_fun$'| 0) % 0.48/0.93 (declare-sort |tptp.'Nat_int_fun$'| 0) % 0.48/0.93 (declare-const tptp.tlfalse tptp.tlbool) % 0.48/0.93 (declare-const |tptp.'one$'| |tptp.'Nat$'|) % 0.48/0.93 (declare-const |tptp.'of_int$'| |tptp.'Int_int_fun$'|) % 0.48/0.93 (declare-const |tptp.'times$a'| (-> |tptp.'Nat$'| |tptp.'Nat_nat_fun$'|)) % 0.48/0.93 (declare-const |tptp.'times$'| (-> Int |tptp.'Int_int_fun$'|)) % 0.48/0.93 (declare-const |tptp.'of_nat$a'| |tptp.'Nat_nat_fun$'|) % 0.48/0.93 (declare-const |tptp.'antimono$a'| (-> |tptp.'Int_int_fun$'| Bool)) % 0.48/0.93 (declare-const |tptp.'greatest$a'| (-> |tptp.'Nat_bool_fun$'| |tptp.'Nat$'|)) % 0.48/0.93 (declare-const |tptp.'greatest$'| (-> |tptp.'Int_bool_fun$'| Int)) % 0.48/0.94 (declare-const tptp.tltrue tptp.tlbool) % 0.48/0.94 (declare-const |tptp.'less$'| |tptp.'Nat_nat_bool_fun_fun$'|) % 0.48/0.94 (declare-const |tptp.'antimono$'| (-> |tptp.'Nat_int_fun$'| Bool)) % 0.48/0.94 (declare-const |tptp.'uu$'| |tptp.'Int_int_bool_fun_fun$'|) % 0.48/0.94 (declare-const |tptp.'fun_app$a'| (-> |tptp.'Int_int_bool_fun_fun$'| Int |tptp.'Int_bool_fun$'|)) % 0.48/0.94 (declare-const |tptp.'fun_app$d'| (-> |tptp.'Nat_nat_bool_fun_fun$'| |tptp.'Nat$'| |tptp.'Nat_bool_fun$'|)) % 0.48/0.94 (declare-const |tptp.'fun_app$'| (-> |tptp.'Int_bool_fun$'| Int Bool)) % 0.48/0.94 (declare-const |tptp.'zero$'| |tptp.'Nat$'|) % 0.48/0.94 (declare-const |tptp.'p$'| |tptp.'Nat_bool_fun$'|) % 0.48/0.94 (declare-const |tptp.'fun_app$c'| (-> |tptp.'Nat_bool_fun$'| |tptp.'Nat$'| Bool)) % 0.48/0.94 (declare-const |tptp.'of_nat$'| |tptp.'Nat_int_fun$'|) % 0.48/0.94 (declare-const |tptp.'fun_app$g'| (-> |tptp.'Int_int_fun$'| Int Int)) % 0.48/0.94 (declare-const |tptp.'n_0$'| |tptp.'Nat$'|) % 0.48/0.94 (declare-const |tptp.'fun_app$b'| (-> |tptp.'Nat_int_fun$'| |tptp.'Nat$'| Int)) % 0.48/0.94 (declare-const |tptp.'fun_app$e'| (-> |tptp.'Nat_nat_fun$'| |tptp.'Nat$'| |tptp.'Nat$'|)) % 0.48/0.94 (declare-const |tptp.'less_eq$'| |tptp.'Nat_nat_bool_fun_fun$'|) % 0.48/0.94 (declare-const |tptp.'fun_app$f'| (-> |tptp.'Int_nat_fun$'| Int |tptp.'Nat$'|)) % 0.48/0.94 (declare-const |tptp.'nat$'| |tptp.'Int_nat_fun$'|) % 0.48/0.94 (define @t1 () (@var "A__questionmark_v1" Int)) % 0.48/0.94 (define @t2 () (@var "A__questionmark_v0" Int)) % 0.48/0.94 (define @t3 () (< @t2 @t1)) % 0.48/0.94 (define @t4 () (@list @t2 @t1)) % 0.48/0.94 (define @t5 () (@var "A__questionmark_v0" |tptp.'Nat$'|)) % 0.48/0.94 (define @t6 () (|tptp.'fun_app$c'| |tptp.'p$'| @t5)) % 0.48/0.94 (define @t7 () (|tptp.'fun_app$b'| |tptp.'of_nat$'| @t5)) % 0.48/0.94 (define @t8 () (|tptp.'fun_app$b'| |tptp.'of_nat$'| |tptp.'n_0$'|)) % 0.48/0.94 (define @t9 () (+ @t8 1)) % 0.48/0.94 (define @t10 () (<= @t9 @t7)) % 0.48/0.94 (define @t11 () (=> @t10 @t6)) % 0.48/0.94 (define @t12 () (@list @t5)) % 0.48/0.94 (define @t13 () (forall @t12 @t11)) % 0.48/0.94 (define @t14 () (|tptp.'fun_app$c'| |tptp.'p$'| |tptp.'n_0$'|)) % 0.48/0.94 (define @t15 () (and @t14 @t13)) % 0.48/0.94 (define @t16 () (=> (<= @t8 @t7) @t6)) % 0.48/0.94 (define @t17 () (forall @t12 @t16)) % 0.48/0.94 (define @t18 () (= @t17 @t15)) % 0.48/0.94 (define @t19 () (not @t18)) % 0.48/0.94 (define @t20 () (@var "A__questionmark_v1" |tptp.'Nat$'|)) % 0.48/0.94 (define @t21 () (|tptp.'fun_app$b'| |tptp.'of_nat$'| @t20)) % 0.48/0.94 (define @t22 () (< @t7 @t21)) % 0.48/0.94 (define @t23 () (+ @t7 1)) % 0.48/0.94 (define @t24 () (<= @t23 @t21)) % 0.48/0.94 (define @t25 () (@list @t5 @t20)) % 0.48/0.94 (define @t26 () (< @t8 @t7)) % 0.48/0.94 (define @t27 () (=> @t26 @t6)) % 0.48/0.94 (define @t28 () (forall @t12 @t27)) % 0.48/0.94 (define @t29 () (and @t14 @t28)) % 0.48/0.94 (define @t30 () (= @t7 @t8)) % 0.48/0.94 (define @t31 () (or @t30 @t26)) % 0.48/0.94 (define @t32 () (=> @t31 @t6)) % 0.48/0.94 (define @t33 () (forall @t12 @t32)) % 0.48/0.94 (define @t34 () (= @t33 @t29)) % 0.48/0.94 (define @t35 () (= @t17 @t33)) % 0.48/0.94 (define @t36 () (<= @t7 @t21)) % 0.48/0.94 (define @t37 () (+ @t21 1)) % 0.48/0.94 (define @t38 () (@var "A__questionmark_v2" |tptp.'Nat$'|)) % 0.48/0.94 (define @t39 () (@var "A__questionmark_v0" |tptp.'Nat_nat_fun$'|)) % 0.48/0.94 (define @t40 () (|tptp.'fun_app$e'| @t39 @t38)) % 0.48/0.94 (define @t41 () (|tptp.'fun_app$e'| @t39 @t20)) % 0.48/0.94 (define @t42 () (|tptp.'fun_app$b'| |tptp.'of_nat$'| @t38)) % 0.48/0.94 (define @t43 () (<= @t21 @t42)) % 0.48/0.94 (define @t44 () (@var "A__questionmark_v3" |tptp.'Nat$'|)) % 0.48/0.94 (define @t45 () (|tptp.'fun_app$b'| |tptp.'of_nat$'| @t44)) % 0.48/0.94 (define @t46 () (+ @t45 1)) % 0.48/0.94 (define @t47 () (|tptp.'fun_app$f'| |tptp.'nat$'| @t46)) % 0.48/0.94 (define @t48 () (|tptp.'fun_app$e'| @t39 @t47)) % 0.48/0.94 (define @t49 () (|tptp.'fun_app$e'| @t39 @t44)) % 0.48/0.94 (define @t50 () (@list @t44)) % 0.48/0.94 (define @t51 () (@list @t39 @t20 @t38)) % 0.48/0.94 (define @t52 () (@var "A__questionmark_v0" |tptp.'Nat_int_fun$'|)) % 0.48/0.94 (define @t53 () (|tptp.'fun_app$b'| @t52 @t38)) % 0.48/0.94 (define @t54 () (|tptp.'fun_app$b'| @t52 @t20)) % 0.48/0.94 (define @t55 () (|tptp.'fun_app$b'| @t52 @t47)) % 0.48/0.94 (define @t56 () (|tptp.'fun_app$b'| @t52 @t44)) % 0.48/0.94 (define @t57 () (@list @t52 @t20 @t38)) % 0.48/0.94 (define @t58 () (= @t7 @t21)) % 0.48/0.94 (define @t59 () (= @t23 @t37)) % 0.48/0.94 (define @t60 () (|tptp.'fun_app$d'| |tptp.'less_eq$'| @t5)) % 0.48/0.94 (define @t61 () (@list @t2)) % 0.48/0.94 (define @t62 () (= @t7 @t37)) % 0.48/0.94 (define @t63 () (=> @t62 false)) % 0.48/0.94 (define @t64 () (<= @t7 @t37)) % 0.48/0.94 (define @t65 () (+ @t42 1)) % 0.48/0.94 (define @t66 () (= @t21 @t65)) % 0.48/0.94 (define @t67 () (@list @t38)) % 0.48/0.94 (define @t68 () (< @t23 @t37)) % 0.48/0.94 (define @t69 () (< @t1 @t2)) % 0.48/0.94 (define @t70 () (@list @t1)) % 0.48/0.94 (define @t71 () (|tptp.'fun_app$d'| |tptp.'less$'| @t5)) % 0.48/0.94 (define @t72 () (|tptp.'fun_app$c'| @t71 @t20)) % 0.48/0.94 (define @t73 () (@list @t20)) % 0.48/0.94 (define @t74 () (= @t5 @t20)) % 0.48/0.94 (define @t75 () (not @t74)) % 0.48/0.94 (define @t76 () (= @t2 @t1)) % 0.48/0.94 (define @t77 () (not @t76)) % 0.48/0.94 (define @t78 () (|tptp.'fun_app$d'| |tptp.'less$'| @t20)) % 0.48/0.94 (define @t79 () (|tptp.'fun_app$c'| @t78 @t5)) % 0.48/0.94 (define @t80 () (|tptp.'fun_app$c'| @t71 @t38)) % 0.48/0.94 (define @t81 () (|tptp.'fun_app$c'| @t78 @t38)) % 0.48/0.94 (define @t82 () (@list @t5 @t20 @t38)) % 0.48/0.94 (define @t83 () (@var "A__questionmark_v2" Int)) % 0.48/0.94 (define @t84 () (< @t2 @t83)) % 0.48/0.94 (define @t85 () (< @t1 @t83)) % 0.48/0.94 (define @t86 () (@list @t2 @t1 @t83)) % 0.48/0.94 (define @t87 () (= @t20 @t38)) % 0.48/0.94 (define @t88 () (= @t1 @t83)) % 0.48/0.94 (define @t89 () (@var "A__questionmark_v0" |tptp.'Nat_bool_fun$'|)) % 0.48/0.94 (define @t90 () (|tptp.'fun_app$c'| @t89 @t20)) % 0.48/0.94 (define @t91 () (|tptp.'fun_app$c'| @t89 @t38)) % 0.48/0.94 (define @t92 () (|tptp.'fun_app$c'| @t89 @t44)) % 0.48/0.94 (define @t93 () (|tptp.'fun_app$d'| |tptp.'less$'| @t44)) % 0.48/0.94 (define @t94 () (@list @t89 @t20)) % 0.48/0.94 (define @t95 () (= @t20 @t5)) % 0.48/0.94 (define @t96 () (not @t79)) % 0.48/0.94 (define @t97 () (not @t72)) % 0.48/0.94 (define @t98 () (= @t1 @t2)) % 0.48/0.94 (define @t99 () (not @t69)) % 0.48/0.94 (define @t100 () (not @t3)) % 0.48/0.94 (define @t101 () (=> @t79 false)) % 0.48/0.94 (define @t102 () (=> @t72 false)) % 0.48/0.94 (define @t103 () (=> @t69 false)) % 0.48/0.94 (define @t104 () (=> @t3 false)) % 0.48/0.94 (define @t105 () (< @t2 @t2)) % 0.48/0.94 (define @t106 () (not @t91)) % 0.48/0.94 (define @t107 () (|tptp.'fun_app$d'| |tptp.'less$'| @t38)) % 0.48/0.94 (define @t108 () (|tptp.'fun_app$c'| @t107 @t20)) % 0.48/0.94 (define @t109 () (@var "A__questionmark_v0" |tptp.'Nat_nat_bool_fun_fun$'|)) % 0.48/0.94 (define @t110 () (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| @t109 @t20) @t38)) % 0.48/0.94 (define @t111 () (@var "A__questionmark_v4" |tptp.'Nat$'|)) % 0.48/0.94 (define @t112 () (|tptp.'fun_app$d'| @t109 @t44)) % 0.48/0.94 (define @t113 () (|tptp.'fun_app$c'| @t112 @t111)) % 0.48/0.94 (define @t114 () (@list @t44 @t111)) % 0.48/0.94 (define @t115 () (forall @t114 (=> (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| @t109 @t111) @t44) @t113))) % 0.48/0.94 (define @t116 () (@list @t109 @t20 @t38)) % 0.48/0.94 (define @t117 () (@var "A__questionmark_v0" |tptp.'Int_int_bool_fun_fun$'|)) % 0.48/0.94 (define @t118 () (|tptp.'fun_app$'| (|tptp.'fun_app$a'| @t117 @t1) @t83)) % 0.48/0.94 (define @t119 () (@var "A__questionmark_v4" Int)) % 0.48/0.94 (define @t120 () (@var "A__questionmark_v3" Int)) % 0.48/0.94 (define @t121 () (|tptp.'fun_app$a'| @t117 @t120)) % 0.48/0.94 (define @t122 () (|tptp.'fun_app$'| @t121 @t119)) % 0.48/0.94 (define @t123 () (@list @t120 @t119)) % 0.48/0.94 (define @t124 () (forall @t123 (=> (|tptp.'fun_app$'| (|tptp.'fun_app$a'| @t117 @t119) @t120) @t122))) % 0.48/0.94 (define @t125 () (@list @t120)) % 0.48/0.94 (define @t126 () (@list @t117 @t1 @t83)) % 0.48/0.94 (define @t127 () (|tptp.'fun_app$c'| @t107 @t5)) % 0.48/0.94 (define @t128 () (< @t83 @t1)) % 0.48/0.94 (define @t129 () (< @t83 @t2)) % 0.48/0.94 (define @t130 () (not @t95)) % 0.48/0.94 (define @t131 () (not @t98)) % 0.48/0.94 (define @t132 () (< @t21 @t7)) % 0.48/0.94 (define @t133 () (not @t58)) % 0.48/0.94 (define @t134 () (< @t7 @t7)) % 0.48/0.94 (define @t135 () (= @t21 @t7)) % 0.48/0.94 (define @t136 () (< @t45 @t42)) % 0.48/0.94 (define @t137 () (not @t92)) % 0.48/0.94 (define @t138 () (exists @t50 (and @t136 @t137))) % 0.48/0.94 (define @t139 () (=> @t22 false)) % 0.48/0.94 (define @t140 () (@var "A__questionmark_v1" |tptp.'Int_nat_fun$'|)) % 0.48/0.94 (define @t141 () (|tptp.'fun_app$f'| @t140 @t120)) % 0.48/0.94 (define @t142 () (|tptp.'fun_app$c'| @t71 @t141)) % 0.48/0.94 (define @t143 () (@var "A__questionmark_v5" Int)) % 0.48/0.94 (define @t144 () (|tptp.'fun_app$f'| @t140 @t143)) % 0.48/0.94 (define @t145 () (|tptp.'fun_app$f'| @t140 @t119)) % 0.48/0.94 (define @t146 () (< @t119 @t143)) % 0.48/0.94 (define @t147 () (@list @t119 @t143)) % 0.48/0.94 (define @t148 () (forall @t147 (=> @t146 (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less$'| @t145) @t144)))) % 0.48/0.94 (define @t149 () (< @t83 @t120)) % 0.48/0.94 (define @t150 () (|tptp.'fun_app$f'| @t140 @t83)) % 0.48/0.94 (define @t151 () (= @t5 @t150)) % 0.48/0.94 (define @t152 () (@list @t5 @t140 @t83 @t120)) % 0.48/0.94 (define @t153 () (@var "A__questionmark_v1" |tptp.'Nat_int_fun$'|)) % 0.48/0.94 (define @t154 () (|tptp.'fun_app$b'| @t153 @t44)) % 0.48/0.94 (define @t155 () (< @t2 @t154)) % 0.48/0.94 (define @t156 () (@var "A__questionmark_v5" |tptp.'Nat$'|)) % 0.48/0.94 (define @t157 () (|tptp.'fun_app$b'| @t153 @t156)) % 0.48/0.94 (define @t158 () (|tptp.'fun_app$b'| @t153 @t111)) % 0.48/0.94 (define @t159 () (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less$'| @t111) @t156)) % 0.48/0.94 (define @t160 () (@list @t111 @t156)) % 0.48/0.94 (define @t161 () (forall @t160 (=> @t159 (< @t158 @t157)))) % 0.48/0.94 (define @t162 () (|tptp.'fun_app$c'| @t107 @t44)) % 0.48/0.94 (define @t163 () (|tptp.'fun_app$b'| @t153 @t38)) % 0.48/0.94 (define @t164 () (= @t2 @t163)) % 0.48/0.94 (define @t165 () (@list @t2 @t153 @t38 @t44)) % 0.48/0.94 (define @t166 () (@var "A__questionmark_v1" |tptp.'Nat_nat_fun$'|)) % 0.48/0.94 (define @t167 () (|tptp.'fun_app$e'| @t166 @t44)) % 0.48/0.94 (define @t168 () (|tptp.'fun_app$c'| @t71 @t167)) % 0.48/0.94 (define @t169 () (|tptp.'fun_app$e'| @t166 @t156)) % 0.48/0.94 (define @t170 () (|tptp.'fun_app$e'| @t166 @t111)) % 0.48/0.94 (define @t171 () (forall @t160 (=> @t159 (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less$'| @t170) @t169)))) % 0.48/0.94 (define @t172 () (|tptp.'fun_app$e'| @t166 @t38)) % 0.48/0.94 (define @t173 () (= @t5 @t172)) % 0.48/0.94 (define @t174 () (@list @t5 @t166 @t38 @t44)) % 0.48/0.94 (define @t175 () (@var "A__questionmark_v1" |tptp.'Int_int_fun$'|)) % 0.48/0.94 (define @t176 () (|tptp.'fun_app$g'| @t175 @t120)) % 0.48/0.94 (define @t177 () (< @t2 @t176)) % 0.48/0.94 (define @t178 () (|tptp.'fun_app$g'| @t175 @t143)) % 0.48/0.94 (define @t179 () (|tptp.'fun_app$g'| @t175 @t119)) % 0.48/0.94 (define @t180 () (forall @t147 (=> @t146 (< @t179 @t178)))) % 0.48/0.94 (define @t181 () (|tptp.'fun_app$g'| @t175 @t83)) % 0.48/0.94 (define @t182 () (= @t2 @t181)) % 0.48/0.94 (define @t183 () (@list @t2 @t175 @t83 @t120)) % 0.48/0.94 (define @t184 () (@var "A__questionmark_v2" |tptp.'Int_nat_fun$'|)) % 0.48/0.94 (define @t185 () (|tptp.'fun_app$f'| @t184 @t2)) % 0.48/0.94 (define @t186 () (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less$'| @t185) @t44)) % 0.48/0.94 (define @t187 () (|tptp.'fun_app$f'| @t184 @t143)) % 0.48/0.94 (define @t188 () (|tptp.'fun_app$f'| @t184 @t119)) % 0.48/0.94 (define @t189 () (forall @t147 (=> @t146 (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less$'| @t188) @t187)))) % 0.48/0.94 (define @t190 () (|tptp.'fun_app$f'| @t184 @t1)) % 0.48/0.94 (define @t191 () (= @t190 @t44)) % 0.48/0.94 (define @t192 () (@list @t2 @t1 @t184 @t44)) % 0.48/0.94 (define @t193 () (@var "A__questionmark_v2" |tptp.'Nat_int_fun$'|)) % 0.48/0.94 (define @t194 () (|tptp.'fun_app$b'| @t193 @t5)) % 0.48/0.94 (define @t195 () (< @t194 @t120)) % 0.48/0.94 (define @t196 () (|tptp.'fun_app$b'| @t193 @t156)) % 0.48/0.94 (define @t197 () (|tptp.'fun_app$b'| @t193 @t111)) % 0.48/0.94 (define @t198 () (forall @t160 (=> @t159 (< @t197 @t196)))) % 0.48/0.94 (define @t199 () (|tptp.'fun_app$b'| @t193 @t20)) % 0.48/0.94 (define @t200 () (= @t199 @t120)) % 0.48/0.94 (define @t201 () (@list @t5 @t20 @t193 @t120)) % 0.48/0.94 (define @t202 () (@var "A__questionmark_v2" |tptp.'Nat_nat_fun$'|)) % 0.48/0.94 (define @t203 () (|tptp.'fun_app$e'| @t202 @t5)) % 0.48/0.94 (define @t204 () (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less$'| @t203) @t44)) % 0.48/0.94 (define @t205 () (|tptp.'fun_app$e'| @t202 @t156)) % 0.48/0.94 (define @t206 () (|tptp.'fun_app$e'| @t202 @t111)) % 0.48/0.94 (define @t207 () (forall @t160 (=> @t159 (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less$'| @t206) @t205)))) % 0.48/0.94 (define @t208 () (|tptp.'fun_app$e'| @t202 @t20)) % 0.48/0.94 (define @t209 () (= @t208 @t44)) % 0.48/0.94 (define @t210 () (@list @t5 @t20 @t202 @t44)) % 0.48/0.94 (define @t211 () (@var "A__questionmark_v2" |tptp.'Int_int_fun$'|)) % 0.48/0.94 (define @t212 () (|tptp.'fun_app$g'| @t211 @t2)) % 0.48/0.94 (define @t213 () (< @t212 @t120)) % 0.48/0.94 (define @t214 () (|tptp.'fun_app$g'| @t211 @t143)) % 0.48/0.94 (define @t215 () (|tptp.'fun_app$g'| @t211 @t119)) % 0.48/0.94 (define @t216 () (forall @t147 (=> @t146 (< @t215 @t214)))) % 0.48/0.94 (define @t217 () (|tptp.'fun_app$g'| @t211 @t1)) % 0.48/0.94 (define @t218 () (= @t217 @t120)) % 0.48/0.94 (define @t219 () (@list @t2 @t1 @t211 @t120)) % 0.48/0.94 (define @t220 () (< @t2 @t163)) % 0.48/0.94 (define @t221 () (|tptp.'fun_app$c'| @t71 @t150)) % 0.48/0.94 (define @t222 () (|tptp.'fun_app$c'| @t71 @t172)) % 0.48/0.94 (define @t223 () (< @t2 @t181)) % 0.48/0.94 (define @t224 () (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less$'| @t190) @t44)) % 0.48/0.94 (define @t225 () (< @t199 @t120)) % 0.48/0.94 (define @t226 () (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less$'| @t208) @t44)) % 0.48/0.94 (define @t227 () (< @t217 @t120)) % 0.48/0.94 (define @t228 () (@var "A__questionmark_v2" tptp.tlbool)) % 0.48/0.94 (define @t229 () (= @t228 tptp.tltrue)) % 0.48/0.94 (define @t230 () (< @t21 @t42)) % 0.48/0.94 (define @t231 () (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less$'| @t41) @t40)) % 0.48/0.94 (define @t232 () (forall @t50 (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less$'| @t49) @t48))) % 0.48/0.94 (define @t233 () (< @t54 @t53)) % 0.48/0.94 (define @t234 () (forall @t50 (< @t56 @t55))) % 0.48/0.94 (define @t235 () (or @t72 @t74)) % 0.48/0.94 (define @t236 () (|tptp.'fun_app$c'| @t60 @t20)) % 0.48/0.94 (define @t237 () (or @t3 @t76)) % 0.48/0.94 (define @t238 () (<= @t2 @t1)) % 0.48/0.94 (define @t239 () (<= @t199 @t120)) % 0.48/0.94 (define @t240 () (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less_eq$'| @t190) @t44)) % 0.48/0.94 (define @t241 () (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less_eq$'| @t208) @t44)) % 0.48/0.94 (define @t242 () (<= @t217 @t120)) % 0.48/0.94 (define @t243 () (<= @t119 @t143)) % 0.48/0.94 (define @t244 () (forall @t147 (=> @t243 (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less_eq$'| @t145) @t144)))) % 0.48/0.94 (define @t245 () (<= @t83 @t120)) % 0.48/0.94 (define @t246 () (|tptp.'fun_app$d'| |tptp.'less_eq$'| @t111)) % 0.48/0.94 (define @t247 () (|tptp.'fun_app$c'| @t246 @t156)) % 0.48/0.94 (define @t248 () (forall @t160 (=> @t247 (<= @t158 @t157)))) % 0.48/0.94 (define @t249 () (|tptp.'fun_app$d'| |tptp.'less_eq$'| @t38)) % 0.48/0.94 (define @t250 () (|tptp.'fun_app$c'| @t249 @t44)) % 0.48/0.94 (define @t251 () (forall @t160 (=> @t247 (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less_eq$'| @t170) @t169)))) % 0.48/0.94 (define @t252 () (forall @t147 (=> @t243 (<= @t179 @t178)))) % 0.48/0.94 (define @t253 () (forall @t147 (=> @t243 (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less_eq$'| @t188) @t187)))) % 0.48/0.94 (define @t254 () (forall @t160 (=> @t247 (<= @t197 @t196)))) % 0.48/0.94 (define @t255 () (forall @t160 (=> @t247 (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less_eq$'| @t206) @t205)))) % 0.48/0.94 (define @t256 () (forall @t147 (=> @t243 (<= @t215 @t214)))) % 0.48/0.94 (define @t257 () (<= @t2 @t163)) % 0.48/0.94 (define @t258 () (|tptp.'fun_app$c'| @t60 @t150)) % 0.48/0.94 (define @t259 () (|tptp.'fun_app$c'| @t60 @t172)) % 0.48/0.94 (define @t260 () (<= @t2 @t181)) % 0.48/0.94 (define @t261 () (|tptp.'fun_app$d'| |tptp.'less_eq$'| @t20)) % 0.48/0.94 (define @t262 () (|tptp.'fun_app$c'| @t261 @t38)) % 0.48/0.94 (define @t263 () (<= @t1 @t83)) % 0.48/0.94 (define @t264 () (and @t236 @t75)) % 0.48/0.94 (define @t265 () (and @t238 @t77)) % 0.48/0.94 (define @t266 () (|tptp.'fun_app$c'| @t261 @t5)) % 0.48/0.94 (define @t267 () (<= @t1 @t2)) % 0.48/0.94 (define @t268 () (not @t236)) % 0.48/0.94 (define @t269 () (not @t238)) % 0.48/0.94 (define @t270 () (not @t267)) % 0.48/0.94 (define @t271 () (|tptp.'fun_app$c'| @t249 @t5)) % 0.48/0.94 (define @t272 () (<= @t83 @t2)) % 0.48/0.94 (define @t273 () (< @t7 @t37)) % 0.48/0.94 (define @t274 () (not @t22)) % 0.48/0.94 (define @t275 () (@var "A__questionmark_v2" |tptp.'Nat_bool_fun$'|)) % 0.48/0.94 (define @t276 () (|tptp.'fun_app$c'| @t275 @t5)) % 0.48/0.94 (define @t277 () (|tptp.'fun_app$c'| @t275 @t44)) % 0.48/0.94 (define @t278 () (|tptp.'fun_app$c'| @t275 @t47)) % 0.48/0.94 (define @t279 () (< @t45 @t21)) % 0.48/0.94 (define @t280 () (@list @t5 @t20 @t275)) % 0.48/0.94 (define @t281 () (@var "A__questionmark_v2" |tptp.'Nat_nat_bool_fun_fun$'|)) % 0.48/0.94 (define @t282 () (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| @t281 @t5) @t20)) % 0.48/0.94 (define @t283 () (|tptp.'fun_app$d'| @t281 @t44)) % 0.48/0.94 (define @t284 () (|tptp.'fun_app$c'| @t283 @t156)) % 0.48/0.94 (define @t285 () (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| @t281 @t111) @t156)) % 0.48/0.94 (define @t286 () (|tptp.'fun_app$c'| @t283 @t111)) % 0.48/0.94 (define @t287 () (|tptp.'fun_app$b'| |tptp.'of_nat$'| @t111)) % 0.48/0.94 (define @t288 () (< @t45 @t287)) % 0.48/0.94 (define @t289 () (@list @t44 @t111 @t156)) % 0.48/0.94 (define @t290 () (forall @t50 (|tptp.'fun_app$c'| @t283 @t47))) % 0.48/0.94 (define @t291 () (@list @t5 @t20 @t281)) % 0.48/0.94 (define @t292 () (< @t7 @t42)) % 0.48/0.94 (define @t293 () (< @t23 @t21)) % 0.48/0.94 (define @t294 () (@var "A__questionmark_v1" |tptp.'Nat_bool_fun$'|)) % 0.48/0.94 (define @t295 () (|tptp.'fun_app$c'| @t294 @t38)) % 0.48/0.94 (define @t296 () (< @t42 @t7)) % 0.48/0.94 (define @t297 () (|tptp.'fun_app$c'| @t294 @t5)) % 0.48/0.94 (define @t298 () (< @t42 @t23)) % 0.48/0.94 (define @t299 () (forall @t67 (=> @t298 @t295))) % 0.48/0.94 (define @t300 () (@list @t5 @t294)) % 0.48/0.94 (define @t301 () (< @t21 @t23)) % 0.48/0.94 (define @t302 () (or @t22 @t58)) % 0.48/0.94 (define @t303 () (exists @t67 (and @t298 @t295))) % 0.48/0.94 (define @t304 () (forall @t67 (=> (and @t292 @t66) false))) % 0.48/0.94 (define @t305 () (and @t36 @t133)) % 0.48/0.94 (define @t306 () (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less_eq$'| @t185) @t44)) % 0.48/0.94 (define @t307 () (<= @t194 @t120)) % 0.48/0.94 (define @t308 () (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less_eq$'| @t203) @t44)) % 0.48/0.94 (define @t309 () (<= @t212 @t120)) % 0.48/0.94 (define @t310 () (|tptp.'fun_app$c'| @t60 @t141)) % 0.48/0.94 (define @t311 () (<= @t2 @t154)) % 0.48/0.94 (define @t312 () (|tptp.'fun_app$c'| @t60 @t167)) % 0.48/0.94 (define @t313 () (<= @t2 @t176)) % 0.48/0.94 (define @t314 () (and @t236 @t266)) % 0.48/0.94 (define @t315 () (and @t238 @t267)) % 0.48/0.94 (define @t316 () (|tptp.'fun_app$c'| @t249 @t20)) % 0.48/0.94 (define @t317 () (<= @t83 @t1)) % 0.48/0.94 (define @t318 () (|tptp.'fun_app$d'| |tptp.'less_eq$'| @t44)) % 0.48/0.94 (define @t319 () (|tptp.'fun_app$c'| @t60 @t38)) % 0.48/0.94 (define @t320 () (<= @t2 @t83)) % 0.48/0.94 (define @t321 () (and @t238 @t263)) % 0.48/0.94 (define @t322 () (|tptp.'fun_app$c'| @t89 @t111)) % 0.48/0.94 (define @t323 () (@list @t111)) % 0.48/0.94 (define @t324 () (<= @t45 @t42)) % 0.48/0.94 (define @t325 () (and @t90 (forall @t50 (=> @t92 @t324)))) % 0.48/0.94 (define @t326 () (@list @t89 @t20 @t38)) % 0.48/0.94 (define @t327 () (<= @t21 @t7)) % 0.48/0.94 (define @t328 () (<= @t7 @t42)) % 0.48/0.94 (define @t329 () (<= @t7 @t45)) % 0.48/0.94 (define @t330 () (|tptp.'fun_app$c'| @t275 @t20)) % 0.48/0.94 (define @t331 () (|tptp.'fun_app$c'| @t294 @t44)) % 0.48/0.94 (define @t332 () (|tptp.'fun_app$f'| |tptp.'nat$'| @t37)) % 0.48/0.94 (define @t333 () (@var "A__questionmark_v0" |tptp.'Int_bool_fun$'|)) % 0.48/0.94 (define @t334 () (|tptp.'greatest$'| @t333)) % 0.48/0.94 (define @t335 () (|tptp.'fun_app$'| @t333 @t1)) % 0.48/0.94 (define @t336 () (@list @t333 @t1)) % 0.48/0.94 (define @t337 () (|tptp.'greatest$a'| @t89)) % 0.48/0.94 (define @t338 () (@var "A__questionmark_v2" |tptp.'Int_bool_fun$'|)) % 0.48/0.94 (define @t339 () (|tptp.'fun_app$'| @t333 @t120)) % 0.48/0.94 (define @t340 () (@var "A__questionmark_v0" |tptp.'Int_int_fun$'|)) % 0.48/0.94 (define @t341 () (<= (|tptp.'fun_app$g'| @t340 @t83) (|tptp.'fun_app$g'| @t340 @t1))) % 0.48/0.94 (define @t342 () (|tptp.'antimono$a'| @t340)) % 0.48/0.94 (define @t343 () (@list @t340 @t1 @t83)) % 0.48/0.94 (define @t344 () (forall (@list @t1 @t83) (=> @t263 @t341))) % 0.48/0.94 (define @t345 () (@list @t340)) % 0.48/0.94 (define @t346 () (|tptp.'fun_app$c'| @t89 @t337)) % 0.48/0.94 (define @t347 () (<= @t42 @t21)) % 0.48/0.94 (define @t348 () (|tptp.'fun_app$f'| |tptp.'nat$'| @t65)) % 0.48/0.94 (define @t349 () (|tptp.'fun_app$c'| @t89 @t348)) % 0.48/0.94 (define @t350 () (< @t42 @t21)) % 0.48/0.94 (define @t351 () (|tptp.'fun_app$f'| |tptp.'nat$'| 0)) % 0.48/0.94 (define @t352 () (|tptp.'fun_app$c'| @t89 @t351)) % 0.48/0.94 (define @t353 () (and @t90 (not @t352))) % 0.48/0.94 (define @t354 () (< 0 @t7)) % 0.48/0.94 (define @t355 () (= @t7 0)) % 0.48/0.94 (define @t356 () (not @t355)) % 0.48/0.94 (define @t357 () (< @t7 0)) % 0.48/0.94 (define @t358 () (<= 0 @t7)) % 0.48/0.94 (define @t359 () (+ 0 1)) % 0.48/0.94 (define @t360 () (=> @t355 false)) % 0.48/0.94 (define @t361 () (exists @t73 @t62)) % 0.48/0.94 (define @t362 () (= 0 @t23)) % 0.48/0.94 (define @t363 () (= @t23 0)) % 0.48/0.94 (define @t364 () (= @t21 0)) % 0.48/0.94 (define @t365 () (< 0 @t42)) % 0.48/0.94 (define @t366 () (<= @t7 0)) % 0.48/0.94 (define @t367 () (|tptp.'fun_app$c'| @t294 @t348)) % 0.48/0.94 (define @t368 () (|tptp.'fun_app$c'| @t294 @t351)) % 0.48/0.94 (define @t369 () (= @t2 0)) % 0.48/0.94 (define @t370 () (= 0 @t2)) % 0.48/0.94 (define @t371 () (< 0 @t21)) % 0.48/0.94 (define @t372 () (|tptp.'times$'| @t42)) % 0.48/0.94 (define @t373 () (|tptp.'fun_app$g'| @t372 @t21)) % 0.48/0.94 (define @t374 () (|tptp.'times$'| @t7)) % 0.48/0.94 (define @t375 () (|tptp.'fun_app$g'| @t374 @t21)) % 0.48/0.94 (define @t376 () (= @t21 @t42)) % 0.48/0.94 (define @t377 () (|tptp.'fun_app$g'| @t374 @t42)) % 0.48/0.94 (define @t378 () (= @t375 @t377)) % 0.48/0.94 (define @t379 () (= 0 @t7)) % 0.48/0.94 (define @t380 () (|tptp.'fun_app$b'| |tptp.'of_nat$'| @t351)) % 0.48/0.94 (define @t381 () (and (= @t7 @t359) (= @t21 @t359))) % 0.48/0.94 (define @t382 () (|tptp.'fun_app$e'| |tptp.'of_nat$a'| @t5)) % 0.48/0.94 (define @t383 () (|tptp.'times$a'| @t382)) % 0.48/0.94 (define @t384 () (|tptp.'fun_app$f'| |tptp.'nat$'| @t375)) % 0.48/0.94 (define @t385 () (|tptp.'times$'| @t2)) % 0.48/0.94 (define @t386 () (|tptp.'fun_app$g'| @t385 @t83)) % 0.48/0.94 (define @t387 () (|tptp.'times$'| @t1)) % 0.48/0.94 (define @t388 () (|tptp.'fun_app$g'| @t387 @t83)) % 0.48/0.94 (define @t389 () (|tptp.'fun_app$g'| @t385 @t388)) % 0.48/0.94 (define @t390 () (|tptp.'times$a'| @t5)) % 0.48/0.94 (define @t391 () (|tptp.'fun_app$e'| @t390 @t38)) % 0.48/0.94 (define @t392 () (|tptp.'times$a'| @t20)) % 0.48/0.94 (define @t393 () (|tptp.'fun_app$e'| @t392 @t38)) % 0.48/0.94 (define @t394 () (|tptp.'fun_app$e'| @t390 @t393)) % 0.48/0.94 (define @t395 () (|tptp.'fun_app$g'| @t387 @t2)) % 0.48/0.94 (define @t396 () (|tptp.'fun_app$g'| @t385 @t1)) % 0.48/0.94 (define @t397 () (|tptp.'fun_app$e'| @t392 @t5)) % 0.48/0.94 (define @t398 () (|tptp.'fun_app$e'| @t390 @t20)) % 0.48/0.94 (define @t399 () (@list @t5 @t1)) % 0.48/0.94 (define @t400 () (|tptp.'fun_app$g'| @t374 @t7)) % 0.48/0.94 (define @t401 () (|tptp.'times$'| @t21)) % 0.48/0.94 (define @t402 () (@list @t5 @t20 @t38 @t44)) % 0.48/0.94 (define @t403 () (|tptp.'fun_app$g'| @t401 @t42)) % 0.48/0.94 (define @t404 () (|tptp.'fun_app$g'| @t372 @t7)) % 0.48/0.94 (define @t405 () (|tptp.'times$'| @t23)) % 0.48/0.94 (define @t406 () (|tptp.'fun_app$g'| @t405 @t42)) % 0.48/0.94 (define @t407 () (|tptp.'fun_app$g'| @t405 @t21)) % 0.48/0.94 (define @t408 () (|tptp.'fun_app$b'| |tptp.'of_nat$'| (|tptp.'fun_app$f'| |tptp.'nat$'| @t23))) % 0.48/0.94 (define @t409 () (and @t22 @t365)) % 0.48/0.94 (define @t410 () (< @t359 @t21)) % 0.48/0.94 (define @t411 () (and @t354 @t410)) % 0.48/0.94 (define @t412 () (|tptp.'fun_app$g'| @t401 @t7)) % 0.48/0.94 (define @t413 () (<= @t375 @t377)) % 0.48/0.94 (define @t414 () (< @t375 @t377)) % 0.48/0.94 (define @t415 () (= @t1 0)) % 0.48/0.94 (define @t416 () (|tptp.'times$'| @t83)) % 0.48/0.94 (define @t417 () (|tptp.'fun_app$g'| @t416 @t1)) % 0.48/0.94 (define @t418 () (= @t20 |tptp.'zero$'|)) % 0.48/0.94 (define @t419 () (|tptp.'times$a'| @t38)) % 0.48/0.94 (define @t420 () (|tptp.'fun_app$e'| @t419 @t20)) % 0.48/0.94 (define @t421 () (= @t396 @t386)) % 0.48/0.94 (define @t422 () (= @t5 |tptp.'zero$'|)) % 0.48/0.94 (define @t423 () (= @t398 @t391)) % 0.48/0.94 (define @t424 () (or @t369 @t415)) % 0.48/0.94 (define @t425 () (= @t396 0)) % 0.48/0.94 (define @t426 () (or @t422 @t418)) % 0.48/0.94 (define @t427 () (= @t398 |tptp.'zero$'|)) % 0.48/0.94 (define @t428 () (@var "A__questionmark_v0" tptp.tlbool)) % 0.48/0.94 (define @t429 () (= @t428 tptp.tltrue)) % 0.48/0.94 (define @t430 () (not @t429)) % 0.48/0.94 (define @t431 () (|tptp.'fun_app$g'| @t416 @t2)) % 0.48/0.94 (define @t432 () (not @t369)) % 0.48/0.94 (define @t433 () (|tptp.'fun_app$e'| @t419 @t5)) % 0.48/0.94 (define @t434 () (not @t422)) % 0.48/0.94 (define @t435 () (not @t425)) % 0.48/0.94 (define @t436 () (and @t432 (not @t415))) % 0.48/0.94 (define @t437 () (not @t427)) % 0.48/0.94 (define @t438 () (and @t434 (not @t418))) % 0.48/0.94 (define @t439 () (|tptp.'fun_app$e'| @t392 @t44)) % 0.48/0.94 (define @t440 () (|tptp.'fun_app$d'| |tptp.'less_eq$'| @t391)) % 0.48/0.94 (define @t441 () (|tptp.'fun_app$c'| @t440 @t439)) % 0.48/0.94 (define @t442 () (|tptp.'fun_app$d'| |tptp.'less_eq$'| |tptp.'zero$'|)) % 0.48/0.94 (define @t443 () (|tptp.'fun_app$c'| @t442 @t38)) % 0.48/0.94 (define @t444 () (|tptp.'fun_app$c'| @t442 @t20)) % 0.48/0.94 (define @t445 () (|tptp.'fun_app$g'| @t387 @t120)) % 0.48/0.94 (define @t446 () (<= @t386 @t445)) % 0.48/0.94 (define @t447 () (<= 0 @t83)) % 0.48/0.94 (define @t448 () (<= 0 @t1)) % 0.48/0.94 (define @t449 () (@list @t2 @t1 @t83 @t120)) % 0.48/0.94 (define @t450 () (|tptp.'fun_app$c'| @t442 @t5)) % 0.48/0.94 (define @t451 () (<= 0 @t2)) % 0.48/0.94 (define @t452 () (|tptp.'fun_app$g'| @t385 @t2)) % 0.48/0.94 (define @t453 () (<= 0 @t396)) % 0.48/0.94 (define @t454 () (<= @t1 0)) % 0.48/0.94 (define @t455 () (<= @t2 0)) % 0.48/0.94 (define @t456 () (and @t455 @t454)) % 0.48/0.94 (define @t457 () (and @t451 @t448)) % 0.48/0.94 (define @t458 () (or @t457 @t456)) % 0.48/0.94 (define @t459 () (and @t238 (<= @t83 0))) % 0.48/0.94 (define @t460 () (and @t236 @t443)) % 0.48/0.94 (define @t461 () (and @t238 @t447)) % 0.48/0.94 (define @t462 () (and @t455 @t448)) % 0.48/0.94 (define @t463 () (and @t451 @t454)) % 0.48/0.94 (define @t464 () (or @t463 @t462)) % 0.48/0.94 (define @t465 () (<= @t396 0)) % 0.48/0.94 (define @t466 () (|tptp.'fun_app$d'| |tptp.'less_eq$'| @t398)) % 0.48/0.94 (define @t467 () (|tptp.'fun_app$c'| @t466 |tptp.'zero$'|)) % 0.48/0.94 (define @t468 () (and (|tptp.'fun_app$c'| @t60 |tptp.'zero$'|) @t444)) % 0.48/0.94 (define @t469 () (and @t450 (|tptp.'fun_app$c'| @t261 |tptp.'zero$'|))) % 0.48/0.94 (define @t470 () (< 0 @t396)) % 0.48/0.94 (define @t471 () (< @t1 0)) % 0.48/0.94 (define @t472 () (< @t2 0)) % 0.48/0.94 (define @t473 () (and @t472 @t471)) % 0.48/0.94 (define @t474 () (< 0 @t1)) % 0.48/0.94 (define @t475 () (and @t472 @t474)) % 0.48/0.94 (define @t476 () (< 0 @t2)) % 0.48/0.94 (define @t477 () (and @t476 @t471)) % 0.48/0.94 (define @t478 () (< @t396 0)) % 0.48/0.94 (define @t479 () (|tptp.'fun_app$d'| |tptp.'less$'| @t398)) % 0.48/0.94 (define @t480 () (|tptp.'fun_app$c'| @t479 |tptp.'zero$'|)) % 0.48/0.94 (define @t481 () (|tptp.'fun_app$d'| |tptp.'less$'| |tptp.'zero$'|)) % 0.48/0.94 (define @t482 () (|tptp.'fun_app$c'| @t481 @t20)) % 0.48/0.94 (define @t483 () (|tptp.'fun_app$c'| @t481 @t5)) % 0.48/0.94 (define @t484 () (and @t483 (|tptp.'fun_app$c'| @t78 |tptp.'zero$'|))) % 0.48/0.94 (define @t485 () (|tptp.'fun_app$c'| @t481 @t398)) % 0.48/0.94 (define @t486 () (and @t476 @t474)) % 0.48/0.94 (define @t487 () (< @t396 @t386)) % 0.48/0.94 (define @t488 () (and @t3 (< @t83 0))) % 0.48/0.94 (define @t489 () (|tptp.'fun_app$c'| @t481 @t38)) % 0.48/0.94 (define @t490 () (and @t72 @t489)) % 0.48/0.94 (define @t491 () (< 0 @t83)) % 0.48/0.94 (define @t492 () (and @t3 @t491)) % 0.48/0.94 (define @t493 () (|tptp.'fun_app$d'| |tptp.'less$'| @t391)) % 0.48/0.94 (define @t494 () (< @t396 @t417)) % 0.48/0.94 (define @t495 () (<= @t396 @t386)) % 0.48/0.94 (define @t496 () (<= @t396 @t417)) % 0.48/0.94 (define @t497 () (|tptp.'fun_app$c'| @t493 @t439)) % 0.48/0.94 (define @t498 () (< @t386 @t445)) % 0.48/0.94 (define @t499 () (= @t2 @t21)) % 0.48/0.94 (define @t500 () (forall @t73 (=> (and @t499 @t371) false))) % 0.48/0.94 (define @t501 () (forall @t73 (=> @t499 false))) % 0.48/0.94 (define @t502 () (- @t21)) % 0.48/0.94 (define @t503 () (= @t2 @t502)) % 0.48/0.94 (define @t504 () (forall @t73 (=> (and @t503 @t371) false))) % 0.48/0.94 (define @t505 () (|tptp.'fun_app$b'| |tptp.'of_nat$'| (|tptp.'fun_app$f'| |tptp.'nat$'| @t2))) % 0.48/0.94 (define @t506 () (@list @t2 @t20)) % 0.48/0.94 (define @t507 () (- @t1)) % 0.48/0.94 (define @t508 () (- @t2)) % 0.48/0.94 (define @t509 () (= @t508 @t507)) % 0.48/0.94 (define @t510 () (- @t396)) % 0.48/0.94 (define @t511 () (|tptp.'fun_app$g'| @t385 @t507)) % 0.48/0.94 (define @t512 () (|tptp.'times$'| @t508)) % 0.48/0.94 (define @t513 () (|tptp.'fun_app$g'| @t512 @t1)) % 0.48/0.94 (define @t514 () (and @t355 @t364)) % 0.48/0.94 (define @t515 () (- @t7)) % 0.48/0.94 (define @t516 () (= @t505 0)) % 0.48/0.94 (define @t517 () (|tptp.'fun_app$f'| |tptp.'nat$'| @t1)) % 0.48/0.94 (define @t518 () (|tptp.'fun_app$b'| |tptp.'of_nat$'| @t517)) % 0.48/0.94 (define @t519 () (< @t505 @t518)) % 0.48/0.94 (define @t520 () (- @t408)) % 0.48/0.94 (define @t521 () (not @t451)) % 0.48/0.94 (define @t522 () (=> @t451 (= @t505 @t2))) % 0.48/0.94 (define @t523 () (= @t2 @t507)) % 0.48/0.94 (define @t524 () (<= @t505 @t518)) % 0.48/0.94 (define @t525 () (forall @t73 (=> @t503 false))) % 0.48/0.94 (define @t526 () (= @t2 (- (|tptp.'fun_app$b'| |tptp.'of_nat$'| @t332)))) % 0.48/0.94 (define @t527 () (|tptp.'fun_app$b'| |tptp.'of_nat$'| (|tptp.'fun_app$f'| |tptp.'nat$'| @t508))) % 0.48/0.94 (define @t528 () (|tptp.'fun_app$b'| |tptp.'of_nat$'| (|tptp.'fun_app$f'| |tptp.'nat$'| @t396))) % 0.48/0.94 (define @t529 () (= @t7 @t518)) % 0.48/0.94 (define @t530 () (< 1 @t2)) % 0.48/0.94 (define @t531 () (|tptp.'fun_app$g'| |tptp.'of_int$'| @t2)) % 0.48/0.94 (define @t532 () (= @t7 1)) % 0.48/0.94 (define @t533 () (|tptp.'fun_app$b'| |tptp.'of_nat$'| (|tptp.'fun_app$f'| |tptp.'nat$'| 1))) % 0.48/0.94 (define @t534 () (or @t369 (= @t1 1))) % 0.48/0.94 (define @t535 () (- 1)) % 0.48/0.94 (define @t536 () (|tptp.'fun_app$g'| |tptp.'of_int$'| @t1)) % 0.48/0.94 (define @t537 () (@var "B" tptp.tlbool)) % 0.48/0.94 (define @t538 () (+ @t8 (* -1 @t7))) % 0.48/0.94 (define @t539 () (>= @t538 0)) % 0.48/0.94 (define @t540 () (not @t539)) % 0.48/0.94 (define @t541 () (not @t540)) % 0.48/0.94 (define @t542 () (* 1 (- @t538 0))) % 0.48/0.94 (define @t543 () (+ 1 @t8)) % 0.48/0.94 (define @t544 () (>= @t543 @t23)) % 0.48/0.94 (define @t545 () (>= @t538 1)) % 0.48/0.94 (define @t546 () (not @t545)) % 0.48/0.94 (define @t547 () (>= @t8 @t23)) % 0.48/0.94 (define @t548 () (= @t8 @t7)) % 0.48/0.94 (define @t549 () (not @t548)) % 0.48/0.94 (define @t550 () (or @t548 @t540)) % 0.48/0.94 (define @t551 () (- @t8 @t7)) % 0.48/0.94 (define @t552 () (>= @t8 @t7)) % 0.48/0.94 (define @t553 () (forall @t12 (or (and @t549 @t539) @t6))) % 0.48/0.94 (define @t554 () (and @t14 (forall @t12 (or @t539 @t6)))) % 0.48/0.94 (define @t555 () (not @t554)) % 0.48/0.94 (define @t556 () (forall @t12 (or @t545 @t6))) % 0.48/0.94 (define @t557 () (@list @t553 @t554)) % 0.48/0.94 (define @t558 () (@list false)) % 0.48/0.94 (define @t559 () (@list @t556)) % 0.48/0.94 (assume @p1 (forall @t4 (= (|tptp.'fun_app$'| (|tptp.'fun_app$a'| |tptp.'uu$'| @t2) @t1) @t3))) % 0.48/0.94 (assume @p2 @t19) % 0.48/0.94 (assume @p3 (forall @t25 (= @t24 @t22))) % 0.48/0.94 (assume @p4 @t34) % 0.48/0.94 (assume @p5 @t35) % 0.48/0.94 (assume @p6 (forall @t25 (= (<= @t23 @t37) @t36))) % 0.48/0.94 (assume @p7 (forall @t51 (=> (and (forall @t50 (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less_eq$'| @t49) @t48)) @t43) (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less_eq$'| @t41) @t40)))) % 0.48/0.94 (assume @p8 (forall @t57 (=> (and (forall @t50 (<= @t56 @t55)) @t43) (<= @t54 @t53)))) % 0.48/0.94 (assume @p9 (forall @t51 (=> (and (forall @t50 (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less_eq$'| @t48) @t49)) @t43) (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less_eq$'| @t40) @t41)))) % 0.48/0.94 (assume @p10 (forall @t57 (=> (and (forall @t50 (<= @t55 @t56)) @t43) (<= @t53 @t54)))) % 0.48/0.94 (assume @p11 (forall @t25 (= @t59 @t58))) % 0.48/0.94 (assume @p12 (forall @t12 (|tptp.'fun_app$c'| @t60 @t5))) % 0.48/0.94 (assume @p13 (forall @t61 (<= @t2 @t2))) % 0.48/0.94 (assume @p14 (forall @t25 (=> @t24 @t36))) % 0.48/0.94 (assume @p15 (forall @t25 (=> (and @t64 (=> @t36 false) @t63) false))) % 0.48/0.94 (assume @p16 (forall @t25 (=> @t36 @t64))) % 0.48/0.94 (assume @p17 (forall @t25 (=> @t24 (exists @t67 @t66)))) % 0.48/0.94 (assume @p18 (forall @t25 (= @t68 @t22))) % 0.48/0.94 (assume @p19 (forall @t25 (=> @t22 @t68))) % 0.48/0.94 (assume @p20 (forall @t12 (< @t7 @t23))) % 0.48/0.94 (assume @p21 (forall @t61 (exists @t70 @t69))) % 0.48/0.94 (assume @p22 (forall @t12 (exists @t73 @t72))) % 0.48/0.94 (assume @p23 (forall @t61 (exists @t70 @t3))) % 0.48/0.94 (assume @p24 (forall @t25 (=> @t72 @t75))) % 0.48/0.94 (assume @p25 (forall @t4 (=> @t3 @t77))) % 0.48/0.94 (assume @p26 (forall @t25 (=> (and @t72 @t79) false))) % 0.48/0.94 (assume @p27 (forall @t4 (=> (and @t3 @t69) false))) % 0.48/0.94 (assume @p28 (forall @t82 (=> (and @t74 @t81) @t80))) % 0.48/0.94 (assume @p29 (forall @t86 (=> (and @t76 @t85) @t84))) % 0.48/0.94 (assume @p30 (forall @t82 (=> (and @t72 @t87) @t80))) % 0.48/0.94 (assume @p31 (forall @t86 (=> (and @t3 @t88) @t84))) % 0.48/0.94 (assume @p32 (forall @t94 (=> (forall @t67 (=> (forall @t50 (=> (|tptp.'fun_app$c'| @t93 @t38) @t92)) @t91)) @t90))) % 0.48/0.94 (assume @p33 (forall @t25 (=> @t97 (= @t96 @t95)))) % 0.48/0.94 (assume @p34 (forall @t4 (=> @t100 (= @t99 @t98)))) % 0.48/0.94 (assume @p35 (forall @t25 (=> (and @t102 (=> @t74 false) @t101) false))) % 0.48/0.94 (assume @p36 (forall @t4 (=> (and @t104 (=> @t76 false) @t103) false))) % 0.48/0.94 (assume @p37 (forall @t12 (not (|tptp.'fun_app$c'| @t71 @t5)))) % 0.48/0.94 (assume @p38 (forall @t61 (not @t105))) % 0.48/0.94 (assume @p39 (forall (@list @t89) (= (exists @t73 @t90) (exists @t73 (and @t90 (forall @t67 (=> @t108 @t106))))))) % 0.48/0.94 (assume @p40 (forall @t116 (=> (and (forall @t114 (=> (|tptp.'fun_app$c'| @t93 @t111) @t113)) (forall @t50 (|tptp.'fun_app$c'| @t112 @t44)) @t115) @t110))) % 0.48/0.94 (assume @p41 (forall @t126 (=> (and (forall @t123 (=> (< @t120 @t119) @t122)) (forall @t125 (|tptp.'fun_app$'| @t121 @t120)) @t124) @t118))) % 0.48/0.94 (assume @p42 (forall @t82 (=> (and @t72 @t81) @t80))) % 0.48/0.94 (assume @p43 (forall @t86 (=> (and @t3 @t85) @t84))) % 0.48/0.94 (assume @p44 (forall @t25 (= @t97 (or @t79 @t74)))) % 0.48/0.94 (assume @p45 (forall @t4 (= @t100 (or @t69 @t76)))) % 0.48/0.94 (assume @p46 (forall @t82 (=> (and @t72 @t127) @t108))) % 0.48/0.94 (assume @p47 (forall @t86 (=> (and @t3 @t129) @t128))) % 0.48/0.94 (assume @p48 (forall @t25 (=> @t72 @t130))) % 0.48/0.94 (assume @p49 (forall @t4 (=> @t3 @t131))) % 0.48/0.94 (assume @p50 (forall @t25 (= @t133 (or @t22 @t132)))) % 0.48/0.94 (assume @p51 (forall @t12 (not @t134))) % 0.48/0.94 (assume @p52 (forall @t25 (=> @t22 (not @t135)))) % 0.48/0.94 (assume @p53 (forall @t25 (=> @t22 @t133))) % 0.48/0.94 (assume @p54 (forall @t12 (=> @t134 false))) % 0.48/0.94 (assume @p55 (forall @t94 (=> (forall @t67 (=> (forall @t50 (=> @t136 @t92)) @t91)) @t90))) % 0.48/0.94 (assume @p56 (forall @t94 (=> (forall @t67 (=> @t106 @t138)) @t90))) % 0.48/0.94 (assume @p57 (forall @t25 (=> (and @t133 @t139 (=> @t132 false)) false))) % 0.48/0.94 (assume @p58 (forall @t25 (=> (and @t75 @t102 @t101) false))) % 0.48/0.94 (assume @p59 (forall @t4 (=> (and @t77 @t104 @t103) false))) % 0.48/0.94 (assume @p60 (forall @t25 (= @t75 (or @t72 @t79)))) % 0.48/0.94 (assume @p61 (forall @t4 (= @t77 (or @t3 @t69)))) % 0.48/0.94 (assume @p62 (forall @t152 (=> (and @t151 @t149 @t148) @t142))) % 0.48/0.94 (assume @p63 (forall @t165 (=> (and @t164 @t162 @t161) @t155))) % 0.48/0.94 (assume @p64 (forall @t174 (=> (and @t173 @t162 @t171) @t168))) % 0.48/0.94 (assume @p65 (forall @t183 (=> (and @t182 @t149 @t180) @t177))) % 0.48/0.94 (assume @p66 (forall @t192 (=> (and @t3 @t191 @t189) @t186))) % 0.48/0.94 (assume @p67 (forall @t201 (=> (and @t72 @t200 @t198) @t195))) % 0.48/0.94 (assume @p68 (forall @t210 (=> (and @t72 @t209 @t207) @t204))) % 0.48/0.94 (assume @p69 (forall @t219 (=> (and @t3 @t218 @t216) @t213))) % 0.48/0.94 (assume @p70 (forall @t165 (=> (and @t220 @t162 @t161) @t155))) % 0.48/0.94 (assume @p71 (forall @t152 (=> (and @t221 @t149 @t148) @t142))) % 0.48/0.94 (assume @p72 (forall @t174 (=> (and @t222 @t162 @t171) @t168))) % 0.48/0.94 (assume @p73 (forall @t183 (=> (and @t223 @t149 @t180) @t177))) % 0.48/0.94 (assume @p74 (forall @t192 (=> (and @t3 @t224 @t189) @t186))) % 0.48/0.94 (assume @p75 (forall @t201 (=> (and @t72 @t225 @t198) @t195))) % 0.48/0.94 (assume @p76 (forall @t210 (=> (and @t72 @t226 @t207) @t204))) % 0.48/0.94 (assume @p77 (forall @t219 (=> (and @t3 @t227 @t216) @t213))) % 0.48/0.94 (assume @p78 (forall @t25 (=> @t72 @t96))) % 0.48/0.94 (assume @p79 (forall @t4 (=> @t3 @t99))) % 0.48/0.94 (assume @p80 (forall (@list @t5 @t20 @t228) (=> @t72 (= (=> @t79 @t229) true)))) % 0.48/0.94 (assume @p81 (forall (@list @t2 @t1 @t228) (=> @t3 (= (=> @t69 @t229) true)))) % 0.48/0.94 (assume @p82 (forall @t25 (or @t72 @t74 @t79))) % 0.48/0.94 (assume @p83 (forall @t4 (or @t3 @t76 @t69))) % 0.48/0.94 (assume @p84 (forall @t25 (=> @t72 (= @t74 false)))) % 0.48/0.94 (assume @p85 (forall @t4 (=> @t3 (= @t76 false)))) % 0.48/0.94 (assume @p86 (forall @t25 (=> @t72 (= @t95 false)))) % 0.48/0.94 (assume @p87 (forall @t4 (=> @t3 (= @t98 false)))) % 0.48/0.94 (assume @p88 (forall @t25 (=> @t72 (= @t96 true)))) % 0.48/0.94 (assume @p89 (forall @t4 (=> @t3 (= @t99 true)))) % 0.48/0.94 (assume @p90 (forall @t51 (=> @t232 (= @t231 @t230)))) % 0.48/0.94 (assume @p91 (forall @t57 (=> @t234 (= @t233 @t230)))) % 0.48/0.94 (assume @p92 (forall @t51 (=> (and @t232 @t230) @t231))) % 0.48/0.94 (assume @p93 (forall @t57 (=> (and @t234 @t230) @t233))) % 0.48/0.94 (assume @p94 (forall @t25 (=> @t236 @t235))) % 0.48/0.94 (assume @p95 (forall @t4 (=> @t238 @t237))) % 0.48/0.94 (assume @p96 (forall @t25 (or @t236 @t79))) % 0.48/0.94 (assume @p97 (forall @t4 (or @t238 @t69))) % 0.48/0.94 (assume @p98 (forall @t201 (=> (and @t72 @t239 @t198) @t195))) % 0.48/0.94 (assume @p99 (forall @t192 (=> (and @t3 @t240 @t189) @t186))) % 0.48/0.94 (assume @p100 (forall @t210 (=> (and @t72 @t241 @t207) @t204))) % 0.48/0.94 (assume @p101 (forall @t219 (=> (and @t3 @t242 @t216) @t213))) % 0.48/0.94 (assume @p102 (forall @t152 (=> (and @t221 @t245 @t244) @t142))) % 0.48/0.94 (assume @p103 (forall @t165 (=> (and @t220 @t250 @t248) @t155))) % 0.48/0.94 (assume @p104 (forall @t174 (=> (and @t222 @t250 @t251) @t168))) % 0.48/0.94 (assume @p105 (forall @t183 (=> (and @t223 @t245 @t252) @t177))) % 0.48/0.94 (assume @p106 (forall @t192 (=> (and @t238 @t224 @t253) @t186))) % 0.48/0.94 (assume @p107 (forall @t201 (=> (and @t236 @t225 @t254) @t195))) % 0.48/0.94 (assume @p108 (forall @t210 (=> (and @t236 @t226 @t255) @t204))) % 0.48/0.94 (assume @p109 (forall @t219 (=> (and @t238 @t227 @t256) @t213))) % 0.48/0.94 (assume @p110 (forall @t165 (=> (and @t257 @t162 @t161) @t155))) % 0.48/0.94 (assume @p111 (forall @t152 (=> (and @t258 @t149 @t148) @t142))) % 0.48/0.94 (assume @p112 (forall @t174 (=> (and @t259 @t162 @t171) @t168))) % 0.48/0.94 (assume @p113 (forall @t183 (=> (and @t260 @t149 @t180) @t177))) % 0.48/0.94 (assume @p114 (forall @t82 (=> (and @t72 @t262) @t80))) % 0.48/0.94 (assume @p115 (forall @t86 (=> (and @t3 @t263) @t84))) % 0.48/0.94 (assume @p116 (forall @t82 (=> (and @t236 @t81) @t80))) % 0.48/0.94 (assume @p117 (forall @t86 (=> (and @t238 @t85) @t84))) % 0.48/0.94 (assume @p118 (forall @t25 (=> (and @t75 @t236) @t72))) % 0.48/0.94 (assume @p119 (forall @t4 (=> (and @t77 @t238) @t3))) % 0.48/0.94 (assume @p120 (forall @t25 (=> @t264 @t72))) % 0.48/0.94 (assume @p121 (forall @t4 (=> @t265 @t3))) % 0.48/0.94 (assume @p122 (forall @t25 (=> @t72 @t236))) % 0.48/0.94 (assume @p123 (forall @t4 (=> @t3 @t238))) % 0.48/0.94 (assume @p124 (forall @t25 (= @t97 @t266))) % 0.48/0.94 (assume @p125 (forall @t4 (= @t100 @t267))) % 0.48/0.94 (assume @p126 (forall @t25 (= @t268 @t79))) % 0.48/0.94 (assume @p127 (forall @t4 (= @t269 @t69))) % 0.48/0.94 (assume @p128 (forall @t25 (= @t72 @t264))) % 0.48/0.94 (assume @p129 (forall @t4 (= @t3 @t265))) % 0.48/0.94 (assume @p130 (forall @t25 (= @t236 @t235))) % 0.48/0.94 (assume @p131 (forall @t4 (= @t238 @t237))) % 0.48/0.94 (assume @p132 (forall @t25 (= @t72 (and @t236 (not @t266))))) % 0.48/0.94 (assume @p133 (forall @t4 (= @t3 (and @t238 @t270)))) % 0.48/0.94 (assume @p134 (forall @t82 (=> (and @t72 @t271) @t108))) % 0.48/0.94 (assume @p135 (forall @t86 (=> (and @t3 @t272) @t128))) % 0.48/0.94 (assume @p136 (forall @t82 (=> (and @t236 @t127) @t108))) % 0.48/0.94 (assume @p137 (forall @t86 (=> (and @t238 @t129) @t128))) % 0.48/0.94 (assume @p138 (forall @t25 (= @t72 (and @t236 @t130)))) % 0.48/0.94 (assume @p139 (forall @t4 (= @t3 (and @t238 @t131)))) % 0.48/0.94 (assume @p140 (forall @t25 (= @t236 (or @t72 @t95)))) % 0.48/0.94 (assume @p141 (forall @t4 (= @t238 (or @t3 @t98)))) % 0.48/0.94 (assume @p142 (forall @t25 (=> @t268 @t79))) % 0.48/0.94 (assume @p143 (forall @t4 (=> @t269 @t69))) % 0.48/0.94 (assume @p144 (forall @t25 (=> @t236 (= @t97 @t74)))) % 0.48/0.94 (assume @p145 (forall @t4 (=> @t238 (= @t100 @t76)))) % 0.48/0.94 (assume @p146 (forall @t25 (=> @t97 (= @t236 @t74)))) % 0.48/0.94 (assume @p147 (forall @t4 (=> @t100 (= @t238 @t76)))) % 0.48/0.94 (assume @p148 (forall @t25 (= @t97 (or @t268 @t74)))) % 0.48/0.94 (assume @p149 (forall @t4 (= @t100 (or @t269 @t76)))) % 0.48/0.94 (assume @p150 (forall @t25 (=> @t97 @t266))) % 0.48/0.94 (assume @p151 (forall @t4 (=> @t100 @t267))) % 0.48/0.94 (assume @p152 (forall @t25 (=> @t236 @t96))) % 0.48/0.94 (assume @p153 (forall @t4 (=> @t238 @t99))) % 0.48/0.94 (assume @p154 (forall @t25 (=> @t274 (= @t273 @t58)))) % 0.48/0.94 (assume @p155 (forall @t280 (=> (and @t22 (forall @t50 (=> (= @t21 @t46) @t277)) (forall @t50 (=> (and @t279 @t278) @t277))) @t276))) % 0.48/0.94 (assume @p156 (forall @t291 (=> (and @t22 @t290 (forall @t289 (=> (and @t288 (< @t287 (|tptp.'fun_app$b'| |tptp.'of_nat$'| @t156)) @t286 @t285) @t284))) @t282))) % 0.48/0.94 (assume @p157 (forall @t82 (=> (and @t22 @t230) (< @t23 @t42)))) % 0.48/0.94 (assume @p158 (forall @t25 (=> @t68 @t22))) % 0.48/0.94 (assume @p159 (forall @t25 (=> (and @t274 @t273) @t135))) % 0.48/0.94 (assume @p160 (forall @t25 (= @t293 (exists @t67 (and @t66 @t292))))) % 0.48/0.94 (assume @p161 (forall @t300 (= @t299 (and @t297 (forall @t67 (=> @t296 @t295)))))) % 0.48/0.94 (assume @p162 (forall @t25 (= @t274 @t301))) % 0.48/0.94 (assume @p163 (forall @t25 (= @t273 @t302))) % 0.48/0.94 (assume @p164 (forall @t300 (= @t303 (or @t297 (exists @t67 (and @t296 @t295)))))) % 0.48/0.94 (assume @p165 (forall @t25 (=> @t22 @t273))) % 0.48/0.94 (assume @p166 (forall @t25 (=> (and @t273 @t139 (=> @t58 false)) false))) % 0.48/0.94 (assume @p167 (forall @t25 (=> (and @t22 (not (= @t23 @t21))) @t293))) % 0.48/0.94 (assume @p168 (forall @t25 (=> (and @t293 @t304) false))) % 0.48/0.94 (assume @p169 (forall @t25 (=> @t293 @t22))) % 0.48/0.94 (assume @p170 (forall @t25 (=> (and @t22 (=> (= @t21 @t23) false) @t304) false))) % 0.48/0.94 (assume @p171 (forall @t51 (=> (and (forall @t114 (=> @t288 (< (|tptp.'fun_app$b'| |tptp.'of_nat$'| @t49) (|tptp.'fun_app$b'| |tptp.'of_nat$'| (|tptp.'fun_app$e'| @t39 @t111))))) @t43) (<= (|tptp.'fun_app$b'| |tptp.'of_nat$'| @t41) (|tptp.'fun_app$b'| |tptp.'of_nat$'| @t40))))) % 0.48/0.94 (assume @p172 (forall @t25 (=> @t305 @t22))) % 0.48/0.94 (assume @p173 (forall @t25 (=> @t302 @t36))) % 0.48/0.94 (assume @p174 (forall @t25 (= @t36 @t302))) % 0.48/0.94 (assume @p175 (forall @t25 (=> @t22 @t36))) % 0.48/0.94 (assume @p176 (forall @t25 (= @t22 @t305))) % 0.48/0.94 (assume @p177 (forall @t25 (=> @t236 (= @t266 @t95)))) % 0.48/0.94 (assume @p178 (forall @t4 (=> @t238 (= @t267 @t98)))) % 0.48/0.94 (assume @p179 (forall @t25 (=> (and (=> @t236 false) (=> @t266 false)) false))) % 0.48/0.94 (assume @p180 (forall @t4 (=> (and (=> @t238 false) (=> @t267 false)) false))) % 0.48/0.94 (assume @p181 (forall @t192 (=> (and @t238 @t191 @t253) @t306))) % 0.48/0.94 (assume @p182 (forall @t201 (=> (and @t236 @t200 @t254) @t307))) % 0.48/0.94 (assume @p183 (forall @t210 (=> (and @t236 @t209 @t255) @t308))) % 0.48/0.94 (assume @p184 (forall @t219 (=> (and @t238 @t218 @t256) @t309))) % 0.48/0.94 (assume @p185 (forall @t152 (=> (and @t151 @t245 @t244) @t310))) % 0.48/0.94 (assume @p186 (forall @t165 (=> (and @t164 @t250 @t248) @t311))) % 0.48/0.94 (assume @p187 (forall @t174 (=> (and @t173 @t250 @t251) @t312))) % 0.48/0.94 (assume @p188 (forall @t183 (=> (and @t182 @t245 @t252) @t313))) % 0.48/0.94 (assume @p189 (forall @t25 (or @t236 @t266))) % 0.48/0.94 (assume @p190 (forall @t4 (or @t238 @t267))) % 0.48/0.94 (assume @p191 (forall @t25 (=> @t74 @t236))) % 0.48/0.94 (assume @p192 (forall @t4 (=> @t76 @t238))) % 0.48/0.94 (assume @p193 (forall @t192 (=> (and @t238 @t240 @t253) @t306))) % 0.48/0.94 (assume @p194 (forall @t201 (=> (and @t236 @t239 @t254) @t307))) % 0.48/0.94 (assume @p195 (forall @t210 (=> (and @t236 @t241 @t255) @t308))) % 0.48/0.94 (assume @p196 (forall @t219 (=> (and @t238 @t242 @t256) @t309))) % 0.48/0.94 (assume @p197 (forall @t165 (=> (and @t257 @t250 @t248) @t311))) % 0.48/0.94 (assume @p198 (forall @t152 (=> (and @t258 @t245 @t244) @t310))) % 0.48/0.94 (assume @p199 (forall @t174 (=> (and @t259 @t250 @t251) @t312))) % 0.48/0.94 (assume @p200 (forall @t183 (=> (and @t260 @t245 @t252) @t313))) % 0.48/0.94 (assume @p201 (forall @t25 (= @t74 @t314))) % 0.48/0.94 (assume @p202 (forall @t4 (= @t76 @t315))) % 0.48/0.94 (assume @p203 (forall @t25 (=> @t314 @t74))) % 0.48/0.94 (assume @p204 (forall @t4 (=> @t315 @t76))) % 0.48/0.94 (assume @p205 (forall @t82 (=> (and @t236 @t271) @t316))) % 0.48/0.94 (assume @p206 (forall @t86 (=> (and @t238 @t272) @t317))) % 0.48/0.94 (assume @p207 (forall @t25 (=> @t314 @t95))) % 0.48/0.94 (assume @p208 (forall @t4 (=> @t315 @t98))) % 0.48/0.94 (assume @p209 (forall @t25 (= @t74 (and @t266 @t236)))) % 0.48/0.94 (assume @p210 (forall @t4 (= @t76 (and @t267 @t238)))) % 0.48/0.94 (assume @p211 (forall @t116 (=> (and (forall @t114 (=> (|tptp.'fun_app$c'| @t318 @t111) @t113)) @t115) @t110))) % 0.48/0.94 (assume @p212 (forall @t126 (=> (and (forall @t123 (=> (<= @t120 @t119) @t122)) @t124) @t118))) % 0.48/0.94 (assume @p213 (forall @t82 (=> (and @t236 @t262) @t319))) % 0.48/0.94 (assume @p214 (forall @t86 (=> @t321 @t320))) % 0.48/0.94 (assume @p215 (forall @t86 (=> (and @t238 @t88) @t320))) % 0.48/0.94 (assume @p216 (forall @t86 (=> (and @t76 @t263) @t320))) % 0.48/0.94 (assume @p217 (forall @t86 (=> (and (=> @t321 false) (=> (and @t267 @t320) false) (=> (and @t320 @t317) false) (=> (and @t317 @t267) false) (=> (and @t263 @t272) false) (=> (and @t272 @t238) false)) false))) % 0.48/0.94 (assume @p218 (forall @t4 (= @t269 (and @t267 @t131)))) % 0.48/0.94 (assume @p219 (forall @t12 (not (= @t7 @t23)))) % 0.48/0.94 (assume @p220 (forall @t25 (=> @t59 @t58))) % 0.48/0.94 (assume @p221 (forall @t326 (=> @t325 (exists @t50 (and @t92 (forall @t323 (=> @t322 (<= @t287 @t45)))))))) % 0.48/0.94 (assume @p222 (forall @t25 (or @t36 @t327))) % 0.48/0.94 (assume @p223 (forall @t25 (=> (and @t36 @t327) @t58))) % 0.48/0.94 (assume @p224 (forall @t25 (=> @t58 @t36))) % 0.48/0.94 (assume @p225 (forall @t82 (=> (and @t36 @t43) @t328))) % 0.48/0.94 (assume @p226 (forall @t12 (<= @t7 @t7))) % 0.48/0.94 (assume @p227 (forall @t25 (=> @t36 @t273))) % 0.48/0.94 (assume @p228 (forall @t25 (= @t22 @t24))) % 0.48/0.94 (assume @p229 (forall @t25 (= @t273 @t36))) % 0.48/0.94 (assume @p230 (forall @t25 (=> @t36 (= @t301 @t135)))) % 0.48/0.94 (assume @p231 (forall @t25 (=> @t24 @t22))) % 0.48/0.94 (assume @p232 (forall @t280 (=> (and @t36 @t330 (forall @t50 (=> (and @t329 @t279 @t278) @t277))) @t276))) % 0.48/0.94 (assume @p233 (forall @t280 (=> (and @t36 @t276 (forall @t50 (=> (and @t329 @t279 @t277) @t278))) @t330))) % 0.48/0.94 (assume @p234 (forall @t25 (=> @t22 @t24))) % 0.48/0.94 (assume @p235 (forall @t291 (=> (and @t36 (forall @t50 (|tptp.'fun_app$c'| @t283 @t44)) (forall @t289 (=> (and @t286 @t285) @t284)) @t290) @t282))) % 0.48/0.94 (assume @p236 (forall @t280 (=> (and @t36 @t276 (forall @t50 (=> (and @t329 @t277) @t278))) @t330))) % 0.48/0.94 (assume @p237 (forall @t94 (=> (forall @t67 (=> (forall @t50 (=> (<= @t46 @t42) @t92)) @t91)) @t90))) % 0.48/0.94 (assume @p238 (forall @t25 (= (not @t36) (<= @t37 @t7)))) % 0.48/0.94 (assume @p239 (forall @t12 (not (<= @t23 @t7)))) % 0.48/0.94 (assume @p240 (forall @t25 (= @t64 (or @t36 @t62)))) % 0.48/0.94 (assume @p241 (forall (@list @t5 @t294 @t38) (=> (and (forall @t50 (=> (< @t7 @t45) @t331)) (forall @t50 (=> (and (<= @t45 @t7) (forall @t323 (=> @t288 (|tptp.'fun_app$c'| @t294 @t111)))) @t331))) @t295))) % 0.48/0.94 (assume @p242 (forall (@list @t52) (= (|tptp.'antimono$'| @t52) (forall @t73 (<= (|tptp.'fun_app$b'| @t52 @t332) @t54))))) % 0.48/0.94 (assume @p243 (forall @t336 (=> (and @t335 (forall (@list @t83) (=> (|tptp.'fun_app$'| @t333 @t83) @t317))) (= @t334 @t1)))) % 0.48/0.94 (assume @p244 (forall @t94 (=> (and @t90 (forall @t67 (=> @t91 @t316))) (= @t337 @t20)))) % 0.48/0.94 (assume @p245 (forall (@list @t333 @t1 @t338) (=> (and @t335 (forall @t125 (=> @t339 (<= @t120 @t1))) (forall @t125 (=> (and @t339 (forall (@list @t119) (=> (|tptp.'fun_app$'| @t333 @t119) (<= @t119 @t120)))) (|tptp.'fun_app$'| @t338 @t120)))) (|tptp.'fun_app$'| @t338 @t334)))) % 0.48/0.94 (assume @p246 (forall (@list @t89 @t20 @t275) (=> (and @t90 (forall @t50 (=> @t92 (|tptp.'fun_app$c'| @t318 @t20))) (forall @t50 (=> (and @t92 (forall @t323 (=> @t322 (|tptp.'fun_app$c'| @t246 @t44)))) @t277))) (|tptp.'fun_app$c'| @t275 @t337)))) % 0.48/0.94 (assume @p247 (forall @t343 (=> (and @t342 @t263) @t341))) % 0.48/0.94 (assume @p248 (forall @t343 (=> (and @t342 @t263 (=> @t341 false)) false))) % 0.48/0.94 (assume @p249 (forall @t345 (=> @t344 @t342))) % 0.48/0.94 (assume @p250 (forall @t345 (= @t342 @t344))) % 0.48/0.94 (assume @p251 (forall @t326 (=> @t325 @t346))) % 0.48/0.94 (assume @p252 (forall @t326 (=> @t325 (<= @t21 (|tptp.'fun_app$b'| |tptp.'of_nat$'| @t337))))) % 0.48/0.94 (assume @p253 (forall @t94 (=> (and (exists @t67 @t91) (forall @t67 (=> @t91 @t347))) @t346))) % 0.48/0.94 (assume @p254 (forall @t4 (or @t76 @t269 @t270))) % 0.48/0.94 (assume @p255 (forall @t61 (= @t105 false))) % 0.48/0.94 (assume @p256 (forall @t94 (=> @t353 (exists @t67 (and @t350 (forall @t50 (=> @t324 @t137)) @t349))))) % 0.48/0.94 (assume @p257 (forall @t12 (= @t356 @t354))) % 0.48/0.94 (assume @p258 (forall @t12 (= @t357 false))) % 0.48/0.94 (assume @p259 (forall @t12 @t358)) % 0.48/0.94 (assume @p260 (forall @t12 (< 0 @t23))) % 0.48/0.94 (assume @p261 (forall @t12 (= (< @t7 @t359) @t355))) % 0.48/0.94 (assume @p262 (forall @t12 (=> (and @t360 (=> @t356 false)) false))) % 0.48/0.94 (assume @p263 (forall @t12 (=> @t356 @t361))) % 0.48/0.94 (assume @p264 (forall @t12 (not @t362))) % 0.48/0.94 (assume @p265 (forall @t12 (=> @t362 false))) % 0.48/0.94 (assume @p266 (forall @t12 (=> @t363 false))) % 0.48/0.94 (assume @p267 (forall @t94 (=> (and @t90 (forall @t67 (=> @t349 @t91))) @t352))) % 0.48/0.94 (assume @p268 (forall @t116 (=> (and (forall @t50 (|tptp.'fun_app$c'| @t112 @t351)) (forall @t50 (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| @t109 @t351) @t47)) (forall @t114 (=> @t113 (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| @t109 @t47) (|tptp.'fun_app$f'| |tptp.'nat$'| (+ @t287 1)))))) @t110))) % 0.48/0.94 (assume @p269 (forall @t94 (=> (and @t352 (forall @t67 (=> @t91 @t349))) @t90))) % 0.48/0.94 (assume @p270 (forall @t12 (=> (and @t360 (forall @t73 @t63)) false))) % 0.48/0.94 (assume @p271 (forall @t25 (=> @t62 @t356))) % 0.48/0.94 (assume @p272 (forall @t12 (not @t363))) % 0.48/0.94 (assume @p273 (forall @t12 (not @t357))) % 0.48/0.94 (assume @p274 (forall @t12 (=> @t360 @t354))) % 0.48/0.94 (assume @p275 (forall @t12 (= (not @t354) @t355))) % 0.48/0.94 (assume @p276 (forall @t12 (=> @t357 false))) % 0.48/0.94 (assume @p277 (forall @t25 (=> @t22 (not @t364)))) % 0.48/0.94 (assume @p278 (forall @t94 (=> (and @t352 (forall @t67 (=> (and @t365 @t106) @t138))) @t90))) % 0.48/0.94 (assume @p279 (forall @t12 (= @t366 @t355))) % 0.48/0.94 (assume @p280 (forall @t12 (=> @t366 @t355))) % 0.48/0.94 (assume @p281 (forall @t12 (= @t358 true))) % 0.48/0.94 (assume @p282 (forall @t25 (= @t273 (or @t355 (exists @t67 (and (= @t7 @t65) @t350)))))) % 0.48/0.94 (assume @p283 (forall @t12 (=> @t354 @t361))) % 0.48/0.94 (assume @p284 (forall @t300 (= @t299 (and @t368 (forall @t67 (=> @t296 @t367)))))) % 0.48/0.94 (assume @p285 (forall @t12 (= @t354 @t361))) % 0.48/0.94 (assume @p286 (forall @t300 (= @t303 (or @t368 (exists @t67 (and @t296 @t367)))))) % 0.48/0.94 (assume @p287 (forall @t94 (=> @t353 (exists @t67 (and @t347 (forall @t50 (=> @t136 @t137)) @t91))))) % 0.48/0.94 (assume @p288 (forall @t61 (= @t370 @t369))) % 0.48/0.94 (assume @p289 (not (< 0 0))) % 0.48/0.94 (assume @p290 (<= 0 0)) % 0.48/0.94 (assume @p291 (forall @t12 (= @t354 @t354))) % 0.48/0.94 (assume @p292 (forall @t82 (= (<= @t375 @t373) (=> @t371 @t328)))) % 0.48/0.94 (assume @p293 (forall @t25 (= @t58 @t58))) % 0.48/0.94 (assume @p294 (forall @t25 (= (= @t375 0) (or @t355 @t364)))) % 0.48/0.94 (assume @p295 (forall @t12 (= (* @t7 0) 0))) % 0.48/0.94 (assume @p296 (forall @t82 (= @t378 (or @t376 @t355)))) % 0.48/0.94 (assume @p297 (forall @t82 (= (= @t375 @t373) (or (= @t7 @t42) @t364)))) % 0.48/0.94 (assume @p298 (forall @t12 (= @t355 @t355))) % 0.48/0.94 (assume @p299 (forall @t12 (= @t379 @t379))) % 0.48/0.94 (assume @p300 (= @t380 0)) % 0.48/0.94 (assume @p301 (forall @t25 (= @t36 @t36))) % 0.48/0.94 (assume @p302 (forall @t25 (= @t22 @t22))) % 0.48/0.94 (assume @p303 (forall @t25 (= (= @t359 @t375) @t381))) % 0.48/0.94 (assume @p304 (forall @t25 (= (= @t375 @t359) @t381))) % 0.48/0.94 (assume @p305 (forall @t25 (= (|tptp.'fun_app$e'| |tptp.'of_nat$a'| @t384) (|tptp.'fun_app$e'| @t383 (|tptp.'fun_app$e'| |tptp.'of_nat$a'| @t20))))) % 0.48/0.94 (assume @p306 (forall @t25 (= (|tptp.'fun_app$b'| |tptp.'of_nat$'| @t384) @t375))) % 0.48/0.94 (assume @p307 (forall @t25 (= (< 0 @t375) (and @t354 @t371)))) % 0.48/0.94 (assume @p308 (forall @t82 (= (< @t375 @t373) (and @t371 @t292)))) % 0.48/0.94 (assume @p309 (forall @t25 (= (<= @t359 @t375) (and (<= @t359 @t7) (<= @t359 @t21))))) % 0.48/0.94 (assume @p310 (forall @t12 (= (* 0 @t7) 0))) % 0.48/0.94 (assume @p311 (forall @t86 (= @t389 (|tptp.'fun_app$g'| @t387 @t386)))) % 0.48/0.94 (assume @p312 (forall @t82 (= @t394 (|tptp.'fun_app$e'| @t392 @t391)))) % 0.48/0.94 (assume @p313 (forall @t4 (= @t396 @t395))) % 0.48/0.94 (assume @p314 (forall @t25 (= @t398 @t397))) % 0.48/0.94 (assume @p315 (forall @t86 (= (|tptp.'fun_app$g'| (|tptp.'times$'| @t396) @t83) @t389))) % 0.48/0.94 (assume @p316 (forall @t82 (= (|tptp.'fun_app$e'| (|tptp.'times$a'| @t398) @t38) @t394))) % 0.48/0.94 (assume @p317 (forall @t25 (= (|tptp.'fun_app$e'| @t383 @t20) (|tptp.'fun_app$e'| @t392 @t382)))) % 0.48/0.94 (assume @p318 (forall @t399 (= (|tptp.'fun_app$g'| @t374 @t1) (|tptp.'fun_app$g'| @t387 @t7)))) % 0.48/0.94 (assume @p319 (forall @t12 (<= @t7 (|tptp.'fun_app$g'| @t374 @t400)))) % 0.48/0.94 (assume @p320 (forall @t12 (<= @t7 @t400))) % 0.48/0.94 (assume @p321 (forall @t402 (=> (and @t36 (<= @t42 @t45)) (<= @t377 (|tptp.'fun_app$g'| @t401 @t45))))) % 0.48/0.94 (assume @p322 (forall @t82 (=> @t36 (<= @t377 @t403)))) % 0.48/0.94 (assume @p323 (forall @t82 (=> @t36 (<= @t404 @t373)))) % 0.48/0.94 (assume @p324 (forall @t82 (= (= @t407 @t406) @t376))) % 0.48/0.94 (assume @p325 (forall @t12 (not (= @t408 0)))) % 0.48/0.94 (assume @p326 (forall @t25 (=> @t36 @t36))) % 0.48/0.94 (assume @p327 (forall @t25 (=> @t22 @t22))) % 0.48/0.94 (assume @p328 (forall @t82 (= (< @t407 @t406) @t230))) % 0.48/0.94 (assume @p329 (forall @t82 (=> @t409 (< @t404 @t373)))) % 0.48/0.94 (assume @p330 (forall @t82 (=> @t409 (< @t377 @t403)))) % 0.48/0.94 (assume @p331 (forall @t82 (= (<= @t407 @t406) @t43))) % 0.48/0.94 (assume @p332 (forall @t25 (=> @t411 (< @t7 @t375)))) % 0.48/0.94 (assume @p333 (forall @t25 (=> @t411 (< @t7 @t412)))) % 0.48/0.94 (assume @p334 (forall @t25 (=> (and (< @t359 @t7) @t410) (< @t359 @t412)))) % 0.48/0.94 (assume @p335 (forall @t82 (= @t413 (=> @t354 @t43)))) % 0.48/0.94 (assume @p336 (forall @t82 (= @t414 (and @t354 @t230)))) % 0.48/0.94 (assume @p337 (forall @t61 (= (* 0 @t2) 0))) % 0.48/0.94 (assume @p338 (forall @t12 (= (|tptp.'fun_app$e'| (|tptp.'times$a'| |tptp.'zero$'|) @t5) |tptp.'zero$'|))) % 0.48/0.94 (assume @p339 (forall @t61 (= (* @t2 0) 0))) % 0.48/0.94 (assume @p340 (forall @t12 (= (|tptp.'fun_app$e'| @t390 |tptp.'zero$'|) |tptp.'zero$'|))) % 0.48/0.94 (assume @p341 (forall @t86 (= (= @t396 @t417) (or @t415 (= @t2 @t83))))) % 0.48/0.94 (assume @p342 (forall @t82 (= (= @t398 @t420) (or @t418 (= @t5 @t38))))) % 0.48/0.94 (assume @p343 (forall @t86 (= @t421 (or @t369 @t88)))) % 0.48/0.94 (assume @p344 (forall @t82 (= @t423 (or @t422 @t87)))) % 0.48/0.94 (assume @p345 (forall @t4 (= @t425 @t424))) % 0.48/0.94 (assume @p346 (forall @t25 (= @t427 @t426))) % 0.48/0.94 (assume @p347 (forall (@list @t428 @t20 @t38) (and (=> @t429 (and (=> @t429 (= @t21 @t21)) (=> @t430 @t376))) (=> @t430 (and (=> @t429 (= @t42 @t21)) (=> @t430 (= @t42 @t42))))))) % 0.48/0.94 (assume @p348 (forall @t86 (=> @t432 (= (= @t395 @t431) @t88)))) % 0.48/0.94 (assume @p349 (forall @t82 (=> @t434 (= (= @t397 @t433) @t87)))) % 0.48/0.94 (assume @p350 (forall @t86 (=> @t432 (= @t421 @t88)))) % 0.48/0.94 (assume @p351 (forall @t82 (=> @t434 (= @t423 @t87)))) % 0.48/0.94 (assume @p352 (forall @t4 (=> @t436 @t435))) % 0.48/0.94 (assume @p353 (forall @t25 (=> @t438 @t437))) % 0.48/0.94 (assume @p354 (forall @t4 (=> @t425 @t424))) % 0.48/0.94 (assume @p355 (forall @t25 (=> @t427 @t426))) % 0.48/0.94 (assume @p356 (forall @t4 (=> @t435 @t436))) % 0.48/0.94 (assume @p357 (forall @t25 (=> @t437 @t438))) % 0.48/0.94 (assume @p358 (forall @t82 (= @t378 (or @t355 @t376)))) % 0.48/0.94 (assume @p359 (forall @t402 (=> (and @t236 @t250 @t444 @t443) @t441))) % 0.48/0.94 (assume @p360 (forall @t449 (=> (and @t238 @t245 @t448 @t447) @t446))) % 0.48/0.94 (assume @p361 (forall @t402 (=> (and @t236 @t250 @t450 @t443) @t441))) % 0.48/0.94 (assume @p362 (forall @t449 (=> (and @t238 @t245 @t451 @t447) @t446))) % 0.48/0.94 (assume @p363 (forall @t61 (<= 0 @t452))) % 0.48/0.94 (assume @p364 (forall @t4 (=> @t458 @t453))) % 0.48/0.94 (assume @p365 (forall @t86 (=> @t459 (<= @t417 @t431)))) % 0.48/0.94 (assume @p366 (forall @t4 (=> @t456 @t453))) % 0.48/0.94 (assume @p367 (forall @t82 (=> @t460 (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less_eq$'| @t433) @t420)))) % 0.48/0.94 (assume @p368 (forall @t86 (=> @t461 (<= @t431 @t417)))) % 0.48/0.94 (assume @p369 (forall @t86 (=> @t459 (<= @t388 @t386)))) % 0.48/0.94 (assume @p370 (forall @t82 (=> @t460 (|tptp.'fun_app$c'| @t440 @t393)))) % 0.48/0.94 (assume @p371 (forall @t86 (=> @t461 (<= @t386 @t388)))) % 0.48/0.94 (assume @p372 (forall @t4 (= @t465 @t464))) % 0.48/0.94 (assume @p373 (forall @t25 (=> (or @t469 @t468) @t467))) % 0.48/0.94 (assume @p374 (forall @t4 (=> @t464 @t465))) % 0.48/0.94 (assume @p375 (forall @t25 (=> (and @t450 @t444) (|tptp.'fun_app$c'| @t442 @t398)))) % 0.48/0.94 (assume @p376 (forall @t4 (=> @t457 @t453))) % 0.48/0.94 (assume @p377 (forall @t25 (=> @t469 @t467))) % 0.48/0.94 (assume @p378 (forall @t4 (=> @t463 @t465))) % 0.48/0.94 (assume @p379 (forall @t25 (=> @t468 @t467))) % 0.48/0.94 (assume @p380 (forall @t4 (=> @t462 @t465))) % 0.48/0.94 (assume @p381 (forall @t25 (=> @t469 (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less_eq$'| @t397) |tptp.'zero$'|)))) % 0.48/0.94 (assume @p382 (forall @t4 (=> @t463 (<= @t395 0)))) % 0.48/0.94 (assume @p383 (forall @t4 (= @t453 @t458))) % 0.48/0.94 (assume @p384 (forall @t4 (=> @t473 @t470))) % 0.48/0.94 (assume @p385 (forall @t61 (not (< @t452 0)))) % 0.48/0.94 (assume @p386 (forall @t4 (= @t478 (or @t477 @t475)))) % 0.48/0.94 (assume @p387 (forall @t25 (=> (and (|tptp.'fun_app$c'| @t71 |tptp.'zero$'|) @t482) @t480))) % 0.48/0.94 (assume @p388 (forall @t4 (=> @t475 @t478))) % 0.48/0.94 (assume @p389 (forall @t25 (=> @t484 @t480))) % 0.48/0.94 (assume @p390 (forall @t4 (=> @t477 @t478))) % 0.48/0.94 (assume @p391 (forall @t25 (=> (and @t483 @t482) @t485))) % 0.48/0.94 (assume @p392 (forall @t4 (=> @t486 @t470))) % 0.48/0.94 (assume @p393 (forall @t25 (=> @t484 (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less$'| @t397) |tptp.'zero$'|)))) % 0.48/0.94 (assume @p394 (forall @t4 (=> @t477 (< @t395 0)))) % 0.48/0.94 (assume @p395 (forall @t4 (= @t470 (or @t486 @t473)))) % 0.48/0.94 (assume @p396 (forall @t25 (=> (and @t485 @t483) @t482))) % 0.48/0.94 (assume @p397 (forall @t4 (=> (and @t470 @t476) @t474))) % 0.48/0.94 (assume @p398 (forall @t25 (=> (and @t485 @t482) @t483))) % 0.48/0.94 (assume @p399 (forall @t4 (=> (and @t470 @t474) @t476))) % 0.48/0.94 (assume @p400 (forall @t86 (=> @t472 (= @t487 @t128)))) % 0.48/0.94 (assume @p401 (forall @t86 (=> @t476 (= @t487 @t85)))) % 0.48/0.94 (assume @p402 (forall @t86 (=> @t488 (< @t417 @t431)))) % 0.48/0.94 (assume @p403 (forall @t82 (=> @t490 (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less$'| @t433) @t420)))) % 0.48/0.94 (assume @p404 (forall @t86 (=> @t492 (< @t431 @t417)))) % 0.48/0.94 (assume @p405 (forall @t86 (= @t487 (or (and @t476 @t85) (and @t472 @t128))))) % 0.48/0.94 (assume @p406 (forall @t86 (=> @t488 (< @t388 @t386)))) % 0.48/0.94 (assume @p407 (forall @t82 (=> @t490 (|tptp.'fun_app$c'| @t493 @t393)))) % 0.48/0.94 (assume @p408 (forall @t86 (=> @t492 (< @t386 @t388)))) % 0.48/0.94 (assume @p409 (forall @t86 (= @t494 (or (and @t474 @t84) (and @t471 @t129))))) % 0.48/0.94 (assume @p410 (forall @t82 (=> @t354 (= @t378 @t376)))) % 0.48/0.94 (assume @p411 (forall @t82 (=> @t354 (= @t414 @t230)))) % 0.48/0.94 (assume @p412 (forall @t86 (= @t495 (and (=> @t476 @t263) (=> @t472 @t317))))) % 0.48/0.94 (assume @p413 (forall @t86 (= @t496 (and (=> @t474 @t320) (=> @t471 @t272))))) % 0.48/0.94 (assume @p414 (forall @t82 (=> (and (|tptp.'fun_app$c'| @t479 @t391) @t450) @t81))) % 0.48/0.94 (assume @p415 (forall @t86 (=> (and @t487 @t451) @t85))) % 0.48/0.94 (assume @p416 (forall @t402 (=> (and @t72 @t162 @t482 @t443) @t497))) % 0.48/0.94 (assume @p417 (forall @t449 (=> (and @t3 @t149 @t474 @t447) @t498))) % 0.48/0.94 (assume @p418 (forall @t86 (= @t487 (and (=> @t451 @t85) (=> @t455 @t128))))) % 0.48/0.94 (assume @p419 (forall @t82 (=> (and (|tptp.'fun_app$c'| @t479 @t420) @t444) @t80))) % 0.48/0.94 (assume @p420 (forall @t86 (=> (and @t494 @t448) @t84))) % 0.48/0.94 (assume @p421 (forall @t402 (=> (and @t72 @t162 @t450 @t443) @t497))) % 0.48/0.94 (assume @p422 (forall @t449 (=> (and @t3 @t149 @t451 @t447) @t498))) % 0.48/0.94 (assume @p423 (forall @t86 (= @t494 (and (=> @t448 @t84) (=> @t454 @t129))))) % 0.48/0.94 (assume @p424 (forall @t86 (=> @t472 (= @t495 @t317)))) % 0.48/0.94 (assume @p425 (forall @t86 (=> @t476 (= @t495 @t263)))) % 0.48/0.94 (assume @p426 (forall @t82 (=> (and (|tptp.'fun_app$c'| @t466 @t391) @t483) @t262))) % 0.48/0.94 (assume @p427 (forall @t86 (=> (and @t495 @t476) @t263))) % 0.48/0.94 (assume @p428 (forall @t82 (=> (and (|tptp.'fun_app$c'| @t466 @t420) @t482) @t319))) % 0.48/0.94 (assume @p429 (forall @t86 (=> (and @t496 @t474) @t320))) % 0.48/0.94 (assume @p430 (forall @t402 (=> (and @t236 @t162 @t483 @t443) @t497))) % 0.48/0.94 (assume @p431 (forall @t449 (=> (and @t238 @t149 @t476 @t447) @t498))) % 0.48/0.94 (assume @p432 (forall @t402 (=> (and @t72 @t250 @t450 @t489) @t497))) % 0.48/0.94 (assume @p433 (forall @t449 (=> (and @t3 @t245 @t451 @t491) @t498))) % 0.48/0.94 (assume @p434 (forall @t82 (=> @t354 (= @t413 @t43)))) % 0.48/0.94 (assume @p435 (forall @t61 (=> @t476 (exists @t73 (and @t371 @t499))))) % 0.48/0.94 (assume @p436 (forall @t61 (=> (and @t476 @t500) false))) % 0.48/0.94 (assume @p437 (forall (@list @t2 @t1 @t38) (=> (and @t3 @t365) (< (|tptp.'fun_app$g'| @t372 @t2) (|tptp.'fun_app$g'| @t372 @t1))))) % 0.48/0.94 (assume @p438 (forall @t61 (=> @t451 (exists @t73 @t499)))) % 0.48/0.94 (assume @p439 (forall @t61 (=> (and @t451 @t501) false))) % 0.48/0.94 (assume @p440 (forall @t86 (=> @t476 (= (<= @t395 @t431) @t263)))) % 0.48/0.94 (assume @p441 (forall @t86 (=> @t476 (= (< @t395 @t431) @t85)))) % 0.48/0.94 (assume @p442 (forall @t61 (=> (and @t472 @t504) false))) % 0.48/0.94 (assume @p443 (forall @t506 (=> @t451 (= (< @t505 @t21) (< @t2 @t21))))) % 0.48/0.94 (assume @p444 (forall @t4 (= @t509 @t76))) % 0.48/0.94 (assume @p445 (forall @t61 (= (- @t508) @t2))) % 0.48/0.94 (assume @p446 (forall @t4 (= (<= @t508 @t507) @t267))) % 0.48/0.94 (assume @p447 (forall @t61 (= (= @t508 @t2) @t369))) % 0.48/0.94 (assume @p448 (forall @t61 (= (= @t2 @t508) @t369))) % 0.48/0.94 (assume @p449 (forall @t61 (= (= @t508 0) @t369))) % 0.48/0.94 (assume @p450 (forall @t61 (= (= 0 @t508) @t370))) % 0.48/0.94 (assume @p451 (= 0 0)) % 0.48/0.94 (assume @p452 (forall @t4 (= (< @t508 @t507) @t69))) % 0.48/0.94 (assume @p453 (forall @t4 (= @t511 @t510))) % 0.48/0.94 (assume @p454 (forall @t4 (= (|tptp.'fun_app$g'| @t512 @t507) @t396))) % 0.48/0.94 (assume @p455 (forall @t4 (= @t513 @t510))) % 0.48/0.94 (assume @p456 (forall @t12 (= @t7 @t7))) % 0.48/0.94 (assume @p457 (forall @t61 (= (<= @t508 @t2) @t451))) % 0.48/0.94 (assume @p458 (forall @t61 (= (<= @t2 @t508) @t455))) % 0.48/0.94 (assume @p459 (forall @t61 (= (<= @t508 0) @t451))) % 0.48/0.94 (assume @p460 (forall @t61 (= (<= 0 @t508) @t455))) % 0.48/0.94 (assume @p461 (forall @t61 (= (< @t2 @t508) @t472))) % 0.48/0.94 (assume @p462 (forall @t61 (= (< @t508 @t2) @t476))) % 0.48/0.94 (assume @p463 (forall @t61 (= (< 0 @t508) @t472))) % 0.48/0.94 (assume @p464 (forall @t61 (= (< @t508 0) @t476))) % 0.48/0.94 (assume @p465 (forall @t25 (= (= @t515 @t21) @t514))) % 0.48/0.94 (assume @p466 (forall @t25 (<= @t515 @t21))) % 0.48/0.94 (assume @p467 (forall @t61 (= @t516 @t455))) % 0.48/0.94 (assume @p468 (forall @t61 (=> @t455 @t516))) % 0.48/0.94 (assume @p469 (forall @t4 (= @t519 (and @t474 @t3)))) % 0.48/0.94 (assume @p470 (forall @t25 (< @t520 @t21))) % 0.48/0.94 (assume @p471 (forall @t12 (= (|tptp.'fun_app$b'| |tptp.'of_nat$'| (|tptp.'fun_app$f'| |tptp.'nat$'| @t515)) 0))) % 0.48/0.94 (assume @p472 (forall @t61 (and @t522 (=> @t521 @t516)))) % 0.48/0.94 (assume @p473 (forall @t61 (= (< 0 @t505) @t476))) % 0.48/0.94 (assume @p474 (forall @t4 (=> @t3 (< @t507 @t508)))) % 0.48/0.94 (assume @p475 (forall @t4 (= (<= @t2 @t507) (<= @t1 @t508)))) % 0.48/0.94 (assume @p476 (forall @t4 (= (<= @t508 @t1) (<= @t507 @t2)))) % 0.48/0.94 (assume @p477 (forall @t4 (=> @t238 (<= @t507 @t508)))) % 0.48/0.94 (assume @p478 (forall @t4 (= (< @t2 @t507) (< @t1 @t508)))) % 0.48/0.94 (assume @p479 (forall @t4 (= (< @t508 @t1) (< @t507 @t2)))) % 0.48/0.94 (assume @p480 (forall @t4 (= (= @t508 @t1) (= @t507 @t2)))) % 0.48/0.94 (assume @p481 (forall @t4 (= @t523 (= @t1 @t508)))) % 0.48/0.94 (assume @p482 (forall @t4 (=> @t76 @t509))) % 0.48/0.94 (assume @p483 (= 0 @t380)) % 0.48/0.94 (assume @p484 (forall @t4 (=> @t238 @t524))) % 0.48/0.94 (assume @p485 (forall @t25 (not (< @t7 @t502)))) % 0.48/0.94 (assume @p486 (forall @t336 (=> (and (forall @t67 (|tptp.'fun_app$'| @t333 @t42)) (forall @t67 (|tptp.'fun_app$'| @t333 (- (|tptp.'fun_app$b'| |tptp.'of_nat$'| @t348))))) @t335))) % 0.48/0.94 (assume @p487 (forall @t61 (=> (and @t501 @t525) false))) % 0.48/0.94 (assume @p488 (forall @t61 (=> (and @t501 (forall @t73 (=> @t526 false))) false))) % 0.48/0.94 (assume @p489 (forall @t4 (= @t513 @t511))) % 0.48/0.94 (assume @p490 (forall @t4 (= (= @t452 (|tptp.'fun_app$g'| @t387 @t1)) (or @t76 @t523)))) % 0.48/0.94 (assume @p491 (forall @t4 (=> @t455 (= @t528 (|tptp.'fun_app$g'| (|tptp.'times$'| @t527) (|tptp.'fun_app$b'| |tptp.'of_nat$'| (|tptp.'fun_app$f'| |tptp.'nat$'| @t507))))))) % 0.48/0.94 (assume @p492 (forall @t4 (=> @t476 (= (< @t518 @t505) @t69)))) % 0.48/0.94 (assume @p493 (forall @t399 (= (< @t7 @t518) (< @t7 @t1)))) % 0.48/0.94 (assume @p494 (forall @t506 (= (<= @t505 @t21) (<= @t2 @t21)))) % 0.48/0.94 (assume @p495 (forall @t399 (= (= @t7 @t1) (and @t529 @t448)))) % 0.48/0.94 (assume @p496 (forall @t61 @t522)) % 0.48/0.94 (assume @p497 (forall @t61 (=> (and @t501 (forall @t73 (=> (and @t371 @t503) false))) false))) % 0.48/0.94 (assume @p498 (forall @t25 (= (<= @t7 @t502) @t514))) % 0.48/0.94 (assume @p499 (forall @t61 (=> (and @t455 @t525) false))) % 0.48/0.94 (assume @p500 (forall @t12 (<= @t515 0))) % 0.48/0.94 (assume @p501 (forall @t4 (=> @t451 (= @t519 @t3)))) % 0.48/0.94 (assume @p502 (forall @t399 (= @t529 (and (=> @t448 (= @t1 @t7)) (=> (not @t448) @t355))))) % 0.48/0.94 (assume @p503 (forall @t506 (= (= @t505 @t21) (and (=> @t451 @t499) (=> @t521 @t364))))) % 0.48/0.94 (assume @p504 (forall @t4 (=> (or @t476 @t448) (= @t524 @t238)))) % 0.48/0.94 (assume @p505 (forall (@list @t89 @t1) (= (|tptp.'fun_app$c'| @t89 @t517) (and (forall @t67 (=> (= @t1 @t42) @t91)) (=> @t471 @t352))))) % 0.48/0.94 (assume @p506 (forall @t506 (=> @t451 (= (<= @t21 @t505) (<= @t21 @t2))))) % 0.48/0.94 (assume @p507 (forall @t4 (=> @t451 (= @t528 (|tptp.'fun_app$g'| (|tptp.'times$'| @t505) @t518))))) % 0.48/0.94 (assume @p508 (forall @t61 (=> (and (=> @t369 false) @t500 @t504) false))) % 0.48/0.94 (assume @p509 (forall @t12 (not (<= 0 @t520)))) % 0.48/0.94 (assume @p510 (forall @t12 (< @t520 0))) % 0.48/0.94 (assume @p511 (forall @t61 (=> @t472 (exists @t73 @t526)))) % 0.48/0.94 (assume @p512 (forall @t61 (= (< @t359 @t505) @t530))) % 0.48/0.94 (assume @p513 (forall @t61 (and (=> @t472 (= @t531 (- @t527))) (=> (not @t472) (= @t531 @t505))))) % 0.48/0.94 (assume @p514 (forall @t61 (= (* @t2 1) @t2))) % 0.48/0.94 (assume @p515 (forall @t12 (= (|tptp.'fun_app$e'| @t390 |tptp.'one$'|) @t5))) % 0.48/0.94 (assume @p516 (forall @t61 (= (* 1 @t2) @t2))) % 0.48/0.94 (assume @p517 (forall @t12 (= (|tptp.'fun_app$e'| (|tptp.'times$a'| |tptp.'one$'|) @t5) @t5))) % 0.48/0.94 (assume @p518 (forall @t12 (= @t532 @t532))) % 0.48/0.94 (assume @p519 (forall @t12 (= (= 1 @t7) @t532))) % 0.48/0.94 (assume @p520 (= @t533 1)) % 0.48/0.94 (assume @p521 (forall @t4 (= (= @t396 @t1) (or @t415 (= @t2 1))))) % 0.48/0.94 (assume @p522 (forall @t4 (= (= @t2 @t395) @t534))) % 0.48/0.94 (assume @p523 (forall @t4 (= (= @t396 @t2) @t534))) % 0.48/0.94 (assume @p524 (forall @t4 (= (= @t2 @t396) @t534))) % 0.48/0.94 (assume @p525 (forall @t61 (= (* @t535 @t2) @t508))) % 0.48/0.94 (assume @p526 (forall @t61 (= (* @t2 @t535) @t508))) % 0.48/0.94 (assume @p527 (= (|tptp.'fun_app$g'| |tptp.'of_int$'| 0) 0)) % 0.48/0.94 (assume @p528 (forall @t61 (= (= 0 @t531) @t369))) % 0.48/0.94 (assume @p529 (forall @t61 (= (= @t531 0) @t369))) % 0.48/0.94 (assume @p530 (forall @t4 (= (<= @t531 @t536) @t238))) % 0.48/0.94 (assume @p531 (forall @t4 (= (< @t531 @t536) @t3))) % 0.48/0.94 (assume @p532 (forall @t4 (= (|tptp.'fun_app$g'| |tptp.'of_int$'| @t396) (|tptp.'fun_app$g'| (|tptp.'times$'| @t531) @t536)))) % 0.48/0.94 (assume @p533 (forall @t12 (= (|tptp.'fun_app$g'| |tptp.'of_int$'| @t7) @t7))) % 0.48/0.94 (assume @p534 (= @t533 @t359)) % 0.48/0.94 (assume @p535 (forall @t61 (= (<= @t531 0) @t455))) % 0.48/0.94 (assume @p536 (forall @t61 (= (<= 0 @t531) @t451))) % 0.48/0.94 (assume @p537 (forall @t61 (= (< @t531 0) @t472))) % 0.48/0.94 (assume @p538 (forall @t61 (= (< 0 @t531) @t476))) % 0.48/0.94 (assume @p539 (forall @t61 (= (<= 1 @t531) (<= 1 @t2)))) % 0.48/0.94 (assume @p540 (forall @t61 (= (<= @t531 1) (<= @t2 1)))) % 0.48/0.94 (assume @p541 (forall @t61 (= (< @t531 1) (< @t2 1)))) % 0.48/0.94 (assume @p542 (forall @t61 (= (< 1 @t531) @t530))) % 0.48/0.94 (assume @p543 (forall @t61 (=> @t451 (= @t505 @t531)))) % 0.48/0.94 (assume @p544 (not (= 0 @t535))) % 0.48/0.94 (assume @p545 (not (<= 1 @t535))) % 0.48/0.94 (assume @p546 (forall @t12 (= (|tptp.'fun_app$f'| |tptp.'nat$'| @t7) @t5))) % 0.48/0.94 (assume @p547 (forall (@list @t537) (or (= @t537 tptp.tltrue) (= @t537 tptp.tlfalse)))) % 0.48/0.94 (assume @p548 (not (= tptp.tltrue tptp.tlfalse))) % 0.48/0.94 (assume @p549 true) % 0.48/0.94 (step @p550 :rule refl :args (@t6)) % 0.48/0.94 (step @p551 :rule bool-double-not-elim :args (@t539)) % 0.48/0.94 (step @p552 :rule nary_cong :premises (@p551 @p550) :args ((or @t541 @t6))) % 0.48/0.94 (step @p553 :rule bool-impl-elim :args (@t540 @t6)) % 0.48/0.94 (step @p554 :rule trans :premises (@p553 @p552)) % 0.48/0.94 (step @p555 :rule cong :premises (@p554) :args ((forall @t12 (=> @t540 @t6)))) % 0.48/0.94 (step @p556 :rule refl :args (@t6)) % 0.48/0.94 (step @p557 :rule arith_poly_norm :args ((= (* 1 (- @t543 @t23)) @t542))) % 0.48/0.94 (step @p558 :rule arith_poly_norm_rel :premises (@p557) :args ((= @t544 @t539))) % 0.48/0.94 (step @p559 :rule cong :premises (@p558) :args ((not @t544))) % 0.48/0.94 (step @p560 :rule arith-leq-norm :args (@t543 @t7)) % 0.48/0.94 (step @p561 :rule trans :premises (@p560 @p559)) % 0.48/0.94 (step @p562 :rule refl :args (@t7)) % 0.48/0.94 (step @p563 :rule arith_poly_norm :args ((= @t9 @t543))) % 0.48/0.94 (step @p564 :rule cong :premises (@p563 @p562) :args (@t10)) % 0.48/0.94 (step @p565 :rule trans :premises (@p564 @p561)) % 0.48/0.94 (step @p566 :rule cong :premises (@p565 @p556) :args (@t11)) % 0.48/0.94 (step @p567 :rule cong :premises (@p566) :args (@t13)) % 0.48/0.94 (step @p568 :rule trans :premises (@p567 @p555)) % 0.48/0.94 (step @p569 :rule refl :args (@t14)) % 0.48/0.94 (step @p570 :rule nary_cong :premises (@p569 @p568) :args (@t15)) % 0.48/0.94 (step @p571 :rule bool-double-not-elim :args (@t545)) % 0.48/0.94 (step @p572 :rule nary_cong :premises (@p571 @p550) :args ((or (not @t546) @t6))) % 0.48/0.94 (step @p573 :rule bool-impl-elim :args (@t546 @t6)) % 0.48/0.94 (step @p574 :rule trans :premises (@p573 @p572)) % 0.48/0.94 (step @p575 :rule cong :premises (@p574) :args ((forall @t12 (=> @t546 @t6)))) % 0.48/0.94 (step @p576 :rule arith_poly_norm :args ((= (* -1 (- @t8 @t23)) (* -1 (- @t538 1))))) % 0.48/0.94 (step @p577 :rule arith_poly_norm_rel :premises (@p576) :args ((= @t547 @t545))) % 0.48/0.94 (step @p578 :rule cong :premises (@p577) :args ((not @t547))) % 0.48/0.94 (step @p579 :rule arith-leq-norm :args (@t8 @t7)) % 0.48/0.94 (step @p580 :rule trans :premises (@p579 @p578)) % 0.48/0.94 (step @p581 :rule cong :premises (@p580 @p556) :args (@t16)) % 0.48/0.94 (step @p582 :rule cong :premises (@p581) :args (@t17)) % 0.48/0.94 (step @p583 :rule trans :premises (@p582 @p575)) % 0.48/0.94 (step @p584 :rule cong :premises (@p583 @p570) :args (@t18)) % 0.48/0.94 (step @p585 :rule cong :premises (@p584) :args (@t19)) % 0.48/0.94 (step @p586 :rule eq_resolve :premises (@p2 @p585)) % 0.48/0.94 (step @p587 :rule not_equiv_elim1 :premises (@p586)) % 0.48/0.94 (step @p588 :rule refl :args (@t549)) % 0.48/0.94 (step @p589 :rule nary_cong :premises (@p588 @p551) :args ((and @t549 @t541))) % 0.48/0.94 (step @p590 :rule bool-or-de-morgan :args (@t548 @t540 false)) % 0.48/0.94 (step @p591 :rule trans :premises (@p590 @p589)) % 0.48/0.94 (step @p592 :rule nary_cong :premises (@p591 @p550) :args ((or (not @t550) @t6))) % 0.48/0.94 (step @p593 :rule bool-impl-elim :args (@t550 @t6)) % 0.48/0.94 (step @p594 :rule trans :premises (@p593 @p592)) % 0.48/0.94 (step @p595 :rule cong :premises (@p594) :args ((forall @t12 (=> @t550 @t6)))) % 0.48/0.94 (step @p596 :rule arith_poly_norm :args ((= (* 1 @t551) @t542))) % 0.48/0.94 (step @p597 :rule arith_poly_norm_rel :premises (@p596) :args ((= @t552 @t539))) % 0.48/0.94 (step @p598 :rule cong :premises (@p597) :args ((not @t552))) % 0.48/0.94 (step @p599 :rule arith-elim-lt :args (@t8 @t7)) % 0.48/0.94 (step @p600 :rule trans :premises (@p599 @p598)) % 0.48/0.94 (step @p601 :rule arith_poly_norm :args ((= (* 1 (- @t7 @t8)) (* -1 @t551)))) % 0.48/0.94 (step @p602 :rule arith_poly_norm_rel :premises (@p601) :args ((= @t30 @t548))) % 0.48/0.94 (step @p603 :rule nary_cong :premises (@p602 @p600) :args (@t31)) % 0.48/0.94 (step @p604 :rule cong :premises (@p603 @p556) :args (@t32)) % 0.48/0.94 (step @p605 :rule cong :premises (@p604) :args (@t33)) % 0.48/0.94 (step @p606 :rule trans :premises (@p605 @p595)) % 0.48/0.94 (step @p607 :rule cong :premises (@p583 @p606) :args (@t35)) % 0.48/0.94 (step @p608 :rule eq_resolve :premises (@p5 @p607)) % 0.48/0.94 (step @p609 :rule equiv_elim2 :premises (@p608)) % 0.48/0.94 (step @p610 :rule eq-symm :args (@t553 @t554)) % 0.48/0.94 (step @p611 :rule cong :premises (@p600 @p556) :args (@t27)) % 0.48/0.94 (step @p612 :rule cong :premises (@p611) :args (@t28)) % 0.48/0.94 (step @p613 :rule trans :premises (@p612 @p555)) % 0.48/0.94 (step @p614 :rule nary_cong :premises (@p569 @p613) :args (@t29)) % 0.48/0.94 (step @p615 :rule cong :premises (@p606 @p614) :args (@t34)) % 0.48/0.94 (step @p616 :rule trans :premises (@p615 @p610)) % 0.48/0.94 (step @p617 :rule eq_resolve :premises (@p4 @p616)) % 0.48/0.94 (step @p618 :rule equiv_elim1 :premises (@p617)) % 0.48/0.94 (step @p619 :rule reordering :premises (@p618) :args ((or @t553 @t555))) % 0.48/0.94 (step @p620 :rule chain_m_resolution :premises (@p619 @p609 @p587) :args (@t556 (@list true false) @t557)) % 0.48/0.94 (step @p621 :rule not_equiv_elim2 :premises (@p586)) % 0.48/0.94 (step @p622 :rule chain_m_resolution :premises (@p621 @p620) :args (@t555 @t558 @t559)) % 0.48/0.94 (step @p623 :rule equiv_elim1 :premises (@p608)) % 0.48/0.94 (step @p624 :rule reordering :premises (@p623) :args ((or @t553 (not @t556)))) % 0.48/0.94 (step @p625 :rule chain_m_resolution :premises (@p624 @p620) :args (@t553 @t558 @t559)) % 0.48/0.94 (step @p626 :rule equiv_elim2 :premises (@p617)) % 0.48/0.94 (step @p627 false :rule chain_m_resolution :premises (@p626 @p625 @p622) :args (false (@list false true) @t557)) % 0.48/0.94 ) % 0.48/0.94 % SZS output end Proof % 0.48/0.94 % cvc5 exiting %------------------------------------------------------------------------------