%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ITP056^1 : TPTP v9.2.1. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n022.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:24:55 AM UTC 2026 % Result : Theorem 0.39s 0.78s % Output : Proof 0.39s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP056^1 : TPTP v9.2.1. Released v7.5.0. % 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.16/0.33 % Computer : n022.cluster.edu % 0.16/0.33 % Model : x86_64 x86_64 % 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.33 % Memory : 8042.1875MB % 0.16/0.33 % 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 04:12:23 EDT 2026 % 0.16/0.34 % CPUTime : % 0.29/0.54 %----Proving TH0 % 0.39/0.78 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-cegqi --no-sygus-inst at 90s... % 0.39/0.78 % SZS status Theorem % 0.39/0.78 % SZS output start Proof % 0.39/0.78 ( % 0.39/0.78 (declare-sort tptp.config256849571t_unit 0) % 0.39/0.78 (declare-sort tptp.list_c1059388851t_unit 0) % 0.39/0.78 (declare-sort tptp.nat 0) % 0.39/0.78 (declare-const tptp.plus_plus_nat (-> tptp.nat tptp.nat tptp.nat)) % 0.39/0.78 (declare-const tptp.prefix1615116500t_unit (-> tptp.list_c1059388851t_unit tptp.list_c1059388851t_unit Bool)) % 0.39/0.78 (declare-const tptp.n0 tptp.nat) % 0.39/0.78 (declare-const tptp.last_c571238084t_unit (-> tptp.list_c1059388851t_unit tptp.config256849571t_unit)) % 0.39/0.78 (declare-const tptp.nth_co1649820636t_unit (-> tptp.list_c1059388851t_unit tptp.nat tptp.config256849571t_unit)) % 0.39/0.78 (declare-const tptp.minus_minus_nat (-> tptp.nat tptp.nat tptp.nat)) % 0.39/0.78 (declare-const tptp.size_s1406904903t_unit (-> tptp.list_c1059388851t_unit tptp.nat)) % 0.39/0.78 (declare-const tptp.one_one_nat tptp.nat) % 0.39/0.78 (declare-const tptp.fe (-> tptp.nat tptp.list_c1059388851t_unit)) % 0.39/0.78 (declare-const tptp.n tptp.nat) % 0.39/0.78 (declare-const tptp.nil_co1338500125t_unit tptp.list_c1059388851t_unit) % 0.39/0.78 (define tptp.ord_less_eq_nat () (let ((_let_1 (@var "C2" tptp.nat))) (let ((_let_2 (@var "A3" tptp.nat))) (let ((_let_3 (@var "B3" tptp.nat))) (lambda (@list _let_2 _let_3) (exists (@list _let_1) (= _let_3 (_ (_ tptp.plus_plus_nat _let_2) _let_1)))))))) % 0.39/0.78 (define tptp.ord_less_nat () (let ((_let_1 (@var "N2" tptp.nat))) (let ((_let_2 (@var "M2" tptp.nat))) (lambda (@list _let_2 _let_1) (and (_ (_ tptp.ord_less_eq_nat _let_2) _let_1) (not (= _let_2 _let_1))))))) % 0.39/0.78 (define @t1 () (_ tptp.fe tptp.n)) % 0.39/0.78 (define @t2 () (not (= @t1 tptp.nil_co1338500125t_unit))) % 0.39/0.78 (define @t3 () (@var "L" tptp.list_c1059388851t_unit)) % 0.39/0.78 (define @t4 () (_ tptp.size_s1406904903t_unit @t3)) % 0.39/0.78 (define @t5 () (_ (_ tptp.minus_minus_nat @t4) tptp.one_one_nat)) % 0.39/0.78 (define @t6 () (_ tptp.nth_co1649820636t_unit @t3)) % 0.39/0.78 (define @t7 () (_ @t6 @t5)) % 0.39/0.78 (define @t8 () (_ tptp.last_c571238084t_unit @t3)) % 0.39/0.78 (define @t9 () (= @t8 @t7)) % 0.39/0.78 (define @t10 () (not (= @t3 tptp.nil_co1338500125t_unit))) % 0.39/0.78 (define @t11 () (=> @t10 @t9)) % 0.39/0.78 (define @t12 () (@list @t3)) % 0.39/0.78 (define @t13 () (forall @t12 @t11)) % 0.39/0.78 (define @t14 () (_ tptp.size_s1406904903t_unit @t1)) % 0.39/0.78 (define @t15 () (_ (_ tptp.minus_minus_nat @t14) tptp.one_one_nat)) % 0.39/0.78 (define @t16 () (@var "Xs" tptp.list_c1059388851t_unit)) % 0.39/0.78 (define @t17 () (_ tptp.size_s1406904903t_unit @t16)) % 0.39/0.78 (define @t18 () (_ tptp.nth_co1649820636t_unit @t16)) % 0.39/0.78 (define @t19 () (@var "J" tptp.nat)) % 0.39/0.78 (define @t20 () (@var "K" tptp.nat)) % 0.39/0.78 (define @t21 () (@var "I" tptp.nat)) % 0.39/0.78 (define @t22 () (_ tptp.minus_minus_nat @t21)) % 0.39/0.78 (define @t23 () (_ (_ tptp.minus_minus_nat (_ @t22 @t19)) @t20)) % 0.39/0.78 (define @t24 () (@list @t21 @t19 @t20)) % 0.39/0.78 (define @t25 () (@var "N" tptp.nat)) % 0.39/0.78 (define @t26 () (@var "Xs2" tptp.list_c1059388851t_unit)) % 0.39/0.78 (define @t27 () (_ tptp.size_s1406904903t_unit @t26)) % 0.39/0.78 (define @t28 () (@list @t26)) % 0.39/0.78 (define @t29 () (@list @t25)) % 0.39/0.78 (define @t30 () (@var "Ys" tptp.list_c1059388851t_unit)) % 0.39/0.78 (define @t31 () (= @t16 @t30)) % 0.39/0.78 (define @t32 () (= @t17 (_ tptp.size_s1406904903t_unit @t30))) % 0.39/0.78 (define @t33 () (@list @t16 @t30)) % 0.39/0.78 (define @t34 () (@var "Y" tptp.list_c1059388851t_unit)) % 0.39/0.78 (define @t35 () (@var "X" tptp.list_c1059388851t_unit)) % 0.39/0.78 (define @t36 () (_ tptp.minus_minus_nat @t25)) % 0.39/0.78 (define @t37 () (_ tptp.ord_less_eq_nat @t21)) % 0.39/0.78 (define @t38 () (_ tptp.ord_less_eq_nat @t25)) % 0.39/0.78 (define @t39 () (_ tptp.ord_less_eq_nat @t19)) % 0.39/0.78 (define @t40 () (_ @t37 @t19)) % 0.39/0.78 (define @t41 () (@var "M" tptp.nat)) % 0.39/0.78 (define @t42 () (_ (_ tptp.ord_less_eq_nat @t41) @t25)) % 0.39/0.78 (define @t43 () (= @t41 @t25)) % 0.39/0.78 (define @t44 () (@list @t41 @t25)) % 0.39/0.78 (define @t45 () (_ @t38 @t41)) % 0.39/0.78 (define @t46 () (_ tptp.ord_less_nat @t25)) % 0.39/0.78 (define @t47 () (_ @t46 @t41)) % 0.39/0.78 (define @t48 () (_ tptp.ord_less_nat @t41)) % 0.39/0.78 (define @t49 () (_ @t48 @t25)) % 0.39/0.78 (define @t50 () (not @t43)) % 0.39/0.78 (define @t51 () (_ @t36 @t20)) % 0.39/0.78 (define @t52 () (_ tptp.minus_minus_nat @t41)) % 0.39/0.78 (define @t53 () (_ @t52 @t20)) % 0.39/0.78 (define @t54 () (_ tptp.ord_less_eq_nat @t20)) % 0.39/0.78 (define @t55 () (_ @t54 @t25)) % 0.39/0.78 (define @t56 () (_ @t54 @t41)) % 0.39/0.78 (define @t57 () (@list @t20 @t41 @t25)) % 0.39/0.78 (define @t58 () (@var "C" tptp.nat)) % 0.39/0.78 (define @t59 () (@var "B" tptp.nat)) % 0.39/0.78 (define @t60 () (_ tptp.minus_minus_nat @t59)) % 0.39/0.78 (define @t61 () (@var "A" tptp.nat)) % 0.39/0.78 (define @t62 () (_ tptp.minus_minus_nat @t61)) % 0.39/0.78 (define @t63 () (_ @t62 @t58)) % 0.39/0.78 (define @t64 () (_ tptp.ord_less_eq_nat @t58)) % 0.39/0.78 (define @t65 () (_ @t64 @t61)) % 0.39/0.78 (define @t66 () (_ tptp.ord_less_nat @t61)) % 0.39/0.78 (define @t67 () (_ @t66 @t59)) % 0.39/0.78 (define @t68 () (@list @t61 @t59 @t58)) % 0.39/0.78 (define @t69 () (@list @t25 @t41)) % 0.39/0.78 (define @t70 () (@var "T" tptp.nat)) % 0.39/0.78 (define @t71 () (@var "S" tptp.nat)) % 0.39/0.78 (define @t72 () (@var "P" (-> tptp.nat Bool))) % 0.39/0.78 (define @t73 () (_ @t72 @t25)) % 0.39/0.78 (define @t74 () (@var "N3" tptp.nat)) % 0.39/0.78 (define @t75 () (_ @t72 @t74)) % 0.39/0.78 (define @t76 () (@var "M3" tptp.nat)) % 0.39/0.78 (define @t77 () (_ @t72 @t76)) % 0.39/0.78 (define @t78 () (_ tptp.ord_less_nat @t76)) % 0.39/0.78 (define @t79 () (_ @t78 @t74)) % 0.39/0.78 (define @t80 () (@list @t76)) % 0.39/0.78 (define @t81 () (@list @t74)) % 0.39/0.78 (define @t82 () (@list @t72 @t25)) % 0.39/0.78 (define @t83 () (@var "N2" tptp.nat)) % 0.39/0.78 (define @t84 () (@var "M2" tptp.nat)) % 0.39/0.78 (define @t85 () (= @t84 @t83)) % 0.39/0.78 (define @t86 () (_ (_ tptp.ord_less_nat @t84) @t83)) % 0.39/0.78 (define @t87 () (@list @t84 @t83)) % 0.39/0.78 (define @t88 () (@var "X" tptp.nat)) % 0.39/0.78 (define @t89 () (@var "Y" tptp.nat)) % 0.39/0.78 (define @t90 () (_ tptp.ord_less_nat @t89)) % 0.39/0.78 (define @t91 () (_ @t90 @t88)) % 0.39/0.78 (define @t92 () (_ tptp.ord_less_nat @t88)) % 0.39/0.78 (define @t93 () (_ @t92 @t89)) % 0.39/0.78 (define @t94 () (not @t93)) % 0.39/0.78 (define @t95 () (= @t88 @t89)) % 0.39/0.78 (define @t96 () (not @t95)) % 0.39/0.78 (define @t97 () (@list @t88 @t89)) % 0.39/0.78 (define @t98 () (@var "X2" tptp.nat)) % 0.39/0.78 (define @t99 () (@var "Y3" tptp.nat)) % 0.39/0.78 (define @t100 () (_ @t72 @t99)) % 0.39/0.78 (define @t101 () (@list @t99)) % 0.39/0.78 (define @t102 () (_ @t72 @t98)) % 0.39/0.78 (define @t103 () (@list @t98)) % 0.39/0.78 (define @t104 () (@var "Y2" tptp.nat)) % 0.39/0.78 (define @t105 () (@var "F" (-> tptp.nat tptp.nat))) % 0.39/0.78 (define @t106 () (@var "J2" tptp.nat)) % 0.39/0.78 (define @t107 () (@var "I2" tptp.nat)) % 0.39/0.78 (define @t108 () (_ tptp.ord_less_nat @t107)) % 0.39/0.78 (define @t109 () (@var "P" (-> tptp.list_c1059388851t_unit Bool))) % 0.39/0.78 (define @t110 () (@var "Ys2" tptp.list_c1059388851t_unit)) % 0.39/0.78 (define @t111 () (_ tptp.minus_minus_nat @t19)) % 0.39/0.78 (define @t112 () (_ tptp.ord_less_nat @t19)) % 0.39/0.78 (define @t113 () (@var "L" tptp.nat)) % 0.39/0.78 (define @t114 () (_ tptp.minus_minus_nat @t113)) % 0.39/0.78 (define @t115 () (_ @t114 @t41)) % 0.39/0.78 (define @t116 () (_ @t114 @t25)) % 0.39/0.78 (define @t117 () (@list @t41 @t25 @t113)) % 0.39/0.78 (define @t118 () (_ tptp.ord_less_eq_nat @t59)) % 0.39/0.78 (define @t119 () (_ @t118 @t61)) % 0.39/0.78 (define @t120 () (_ tptp.minus_minus_nat @t58)) % 0.39/0.78 (define @t121 () (_ @t118 @t58)) % 0.39/0.78 (define @t122 () (_ tptp.ord_less_eq_nat @t61)) % 0.39/0.78 (define @t123 () (_ @t122 @t58)) % 0.39/0.78 (define @t124 () (@list @t61 @t58 @t59)) % 0.39/0.78 (define @t125 () (_ @t52 @t25)) % 0.39/0.78 (define @t126 () (@var "I3" tptp.nat)) % 0.39/0.78 (define @t127 () (@var "Ys3" tptp.list_c1059388851t_unit)) % 0.39/0.78 (define @t128 () (@var "Xs3" tptp.list_c1059388851t_unit)) % 0.39/0.78 (define @t129 () (_ (_ tptp.nth_co1649820636t_unit @t128) @t126)) % 0.39/0.78 (define @t130 () (_ tptp.size_s1406904903t_unit @t128)) % 0.39/0.78 (define @t131 () (_ tptp.ord_less_nat @t126)) % 0.39/0.78 (define @t132 () (@list @t126)) % 0.39/0.78 (define @t133 () (@var "Z" tptp.list_c1059388851t_unit)) % 0.39/0.78 (define @t134 () (@var "Y4" tptp.list_c1059388851t_unit)) % 0.39/0.78 (define @t135 () (@var "P" (-> tptp.nat tptp.config256849571t_unit Bool))) % 0.39/0.78 (define @t136 () (_ @t135 @t126)) % 0.39/0.78 (define @t137 () (_ @t131 @t20)) % 0.39/0.78 (define @t138 () (@var "X3" tptp.config256849571t_unit)) % 0.39/0.78 (define @t139 () (@list @t88)) % 0.39/0.78 (define @t140 () (_ @t62 @t59)) % 0.39/0.78 (define @t141 () (_ (_ tptp.minus_minus_nat @t140) @t58)) % 0.39/0.78 (define @t142 () (@var "N4" tptp.nat)) % 0.39/0.78 (define @t143 () (_ tptp.fe @t142)) % 0.39/0.78 (define @t144 () (_ tptp.ord_less_eq_nat @t88)) % 0.39/0.78 (define @t145 () (@var "K2" tptp.nat)) % 0.39/0.78 (define @t146 () (_ @t72 @t145)) % 0.39/0.78 (define @t147 () (@var "I4" tptp.nat)) % 0.39/0.78 (define @t148 () (@list @t145)) % 0.39/0.78 (define @t149 () (@var "X4" tptp.nat)) % 0.39/0.78 (define @t150 () (_ (_ tptp.ord_less_eq_nat @t70) @t149)) % 0.39/0.78 (define @t151 () (@var "Z2" tptp.nat)) % 0.39/0.78 (define @t152 () (_ tptp.ord_less_nat @t149)) % 0.39/0.78 (define @t153 () (_ @t152 @t151)) % 0.39/0.78 (define @t154 () (@list @t149)) % 0.39/0.78 (define @t155 () (@list @t151)) % 0.39/0.78 (define @t156 () (@list @t70)) % 0.39/0.78 (define @t157 () (_ (_ tptp.ord_less_eq_nat @t149) @t70)) % 0.39/0.78 (define @t158 () (_ (_ tptp.ord_less_nat @t151) @t149)) % 0.39/0.78 (define @t159 () (= @t59 @t58)) % 0.39/0.78 (define @t160 () (_ tptp.plus_plus_nat @t61)) % 0.39/0.78 (define @t161 () (_ @t160 @t58)) % 0.39/0.78 (define @t162 () (_ @t160 @t59)) % 0.39/0.78 (define @t163 () (= @t162 @t161)) % 0.39/0.78 (define @t164 () (_ tptp.plus_plus_nat @t58)) % 0.39/0.78 (define @t165 () (_ @t164 @t61)) % 0.39/0.78 (define @t166 () (_ tptp.plus_plus_nat @t59)) % 0.39/0.78 (define @t167 () (= (_ @t166 @t61) @t165)) % 0.39/0.78 (define @t168 () (@list @t59 @t61 @t58)) % 0.39/0.78 (define @t169 () (_ @t122 @t59)) % 0.39/0.78 (define @t170 () (_ @t166 @t58)) % 0.39/0.78 (define @t171 () (_ tptp.ord_less_eq_nat @t161)) % 0.39/0.78 (define @t172 () (_ @t171 @t170)) % 0.39/0.78 (define @t173 () (_ @t164 @t59)) % 0.39/0.78 (define @t174 () (_ tptp.ord_less_eq_nat @t165)) % 0.39/0.78 (define @t175 () (_ @t174 @t173)) % 0.39/0.78 (define @t176 () (@list @t58 @t61 @t59)) % 0.39/0.78 (define @t177 () (_ tptp.ord_less_nat @t161)) % 0.39/0.78 (define @t178 () (_ @t177 @t170)) % 0.39/0.78 (define @t179 () (_ (_ tptp.ord_less_nat @t165) @t173)) % 0.39/0.78 (define @t180 () (_ tptp.minus_minus_nat @t165)) % 0.39/0.78 (define @t181 () (_ tptp.minus_minus_nat @t162)) % 0.39/0.78 (define @t182 () (@list @t61 @t59)) % 0.39/0.78 (define @t183 () (_ tptp.plus_plus_nat @t20)) % 0.39/0.78 (define @t184 () (_ @t183 @t25)) % 0.39/0.78 (define @t185 () (_ @t183 @t41)) % 0.39/0.78 (define @t186 () (_ tptp.plus_plus_nat @t19)) % 0.39/0.78 (define @t187 () (_ @t186 @t20)) % 0.39/0.78 (define @t188 () (_ tptp.plus_plus_nat @t21)) % 0.39/0.78 (define @t189 () (_ @t188 @t20)) % 0.39/0.78 (define @t190 () (_ @t111 @t20)) % 0.39/0.78 (define @t191 () (_ @t54 @t19)) % 0.39/0.78 (define @t192 () (@list @t20 @t19 @t21)) % 0.39/0.78 (define @t193 () (_ @t186 @t21)) % 0.39/0.78 (define @t194 () (_ (_ tptp.minus_minus_nat @t193) @t20)) % 0.39/0.78 (define @t195 () (_ (_ tptp.plus_plus_nat @t190) @t21)) % 0.39/0.78 (define @t196 () (_ @t188 @t19)) % 0.39/0.78 (define @t197 () (_ (_ tptp.minus_minus_nat @t196) @t20)) % 0.39/0.78 (define @t198 () (_ @t188 @t190)) % 0.39/0.78 (define @t199 () (_ @t160 @t170)) % 0.39/0.78 (define @t200 () (_ @t186 @t113)) % 0.39/0.78 (define @t201 () (= @t20 @t113)) % 0.39/0.78 (define @t202 () (= @t21 @t19)) % 0.39/0.78 (define @t203 () (@list @t21 @t19 @t20 @t113)) % 0.39/0.78 (define @t204 () (_ @t183 @t162)) % 0.39/0.78 (define @t205 () (@var "A2" tptp.nat)) % 0.39/0.78 (define @t206 () (@var "B2" tptp.nat)) % 0.39/0.78 (define @t207 () (@var "A3" tptp.nat)) % 0.39/0.78 (define @t208 () (@var "B3" tptp.nat)) % 0.39/0.78 (define @t209 () (@list @t207 @t208)) % 0.39/0.78 (define @t210 () (@var "C3" tptp.nat)) % 0.39/0.78 (define @t211 () (@var "D" tptp.nat)) % 0.39/0.78 (define @t212 () (_ @t166 @t211)) % 0.39/0.78 (define @t213 () (_ @t64 @t211)) % 0.39/0.78 (define @t214 () (@list @t61 @t59 @t58 @t211)) % 0.39/0.78 (define @t215 () (_ tptp.ord_less_eq_nat @t189)) % 0.39/0.78 (define @t216 () (_ @t215 @t200)) % 0.39/0.78 (define @t217 () (_ @t54 @t113)) % 0.39/0.78 (define @t218 () (_ @t177 @t212)) % 0.39/0.78 (define @t219 () (_ tptp.ord_less_nat @t58)) % 0.39/0.78 (define @t220 () (=> (_ @t219 @t211) @t218)) % 0.39/0.78 (define @t221 () (_ tptp.ord_less_nat @t189)) % 0.39/0.78 (define @t222 () (_ @t221 @t200)) % 0.39/0.78 (define @t223 () (_ tptp.ord_less_nat @t21)) % 0.39/0.78 (define @t224 () (_ @t223 @t19)) % 0.39/0.78 (define @t225 () (_ (_ tptp.ord_less_nat @t20) @t113)) % 0.39/0.78 (define @t226 () (_ tptp.plus_plus_nat @t41)) % 0.39/0.78 (define @t227 () (_ @t226 @t19)) % 0.39/0.78 (define @t228 () (@list @t21 @t19 @t41)) % 0.39/0.78 (define @t229 () (_ @t186 @t41)) % 0.39/0.78 (define @t230 () (_ tptp.ord_less_nat @t196)) % 0.39/0.78 (define @t231 () (@var "K3" tptp.nat)) % 0.39/0.78 (define @t232 () (_ @t226 @t20)) % 0.39/0.78 (define @t233 () (_ (_ tptp.ord_less_eq_nat @t232) @t25)) % 0.39/0.78 (define @t234 () (@list @t41 @t20 @t25)) % 0.39/0.78 (define @t235 () (_ @t226 @t25)) % 0.39/0.78 (define @t236 () (_ tptp.plus_plus_nat @t25)) % 0.39/0.78 (define @t237 () (_ @t236 @t41)) % 0.39/0.78 (define @t238 () (_ @t60 @t61)) % 0.39/0.78 (define @t239 () (_ tptp.plus_plus_nat @t238)) % 0.39/0.78 (define @t240 () (_ @t239 @t58)) % 0.39/0.78 (define @t241 () (_ (_ tptp.minus_minus_nat @t170) @t61)) % 0.39/0.78 (define @t242 () (_ @t164 @t238)) % 0.39/0.78 (define @t243 () (_ (_ tptp.minus_minus_nat @t173) @t61)) % 0.39/0.78 (define @t244 () (@var "M4" tptp.nat)) % 0.39/0.78 (define @t245 () (= @t61 @t59)) % 0.39/0.78 (define @t246 () (@list @t59 @t61)) % 0.39/0.78 (define @t247 () (_ (_ tptp.ord_less_eq_nat @t207) @t208)) % 0.39/0.78 (define @t248 () (_ (_ tptp.ord_less_eq_nat @t208) @t207)) % 0.39/0.78 (define @t249 () (@var "Z" tptp.nat)) % 0.39/0.78 (define @t250 () (@var "Y4" tptp.nat)) % 0.39/0.78 (define @t251 () (lambda (@list @t250 @t249) (= @t250 @t249))) % 0.39/0.78 (define @t252 () (@var "P" (-> tptp.nat tptp.nat Bool))) % 0.39/0.78 (define @t253 () (@var "B4" tptp.nat)) % 0.39/0.78 (define @t254 () (@var "A4" tptp.nat)) % 0.39/0.78 (define @t255 () (_ @t252 @t254)) % 0.39/0.78 (define @t256 () (_ @t255 @t253)) % 0.39/0.78 (define @t257 () (@list @t254 @t253)) % 0.39/0.78 (define @t258 () (=> (forall @t257 (=> (_ (_ @t252 @t253) @t254) @t256)) (_ (_ @t252 @t61) @t59))) % 0.39/0.78 (define @t259 () (@list @t252 @t61 @t59)) % 0.39/0.78 (define @t260 () (@list @t61)) % 0.39/0.78 (define @t261 () (@var "Z3" tptp.nat)) % 0.39/0.78 (define @t262 () (_ @t144 @t261)) % 0.39/0.78 (define @t263 () (_ tptp.ord_less_eq_nat @t89)) % 0.39/0.78 (define @t264 () (_ @t263 @t261)) % 0.39/0.78 (define @t265 () (_ @t144 @t89)) % 0.39/0.78 (define @t266 () (@list @t88 @t89 @t261)) % 0.39/0.78 (define @t267 () (=> @t121 @t123)) % 0.39/0.78 (define @t268 () (_ @t263 @t88)) % 0.39/0.78 (define @t269 () (@list @t89 @t88)) % 0.39/0.78 (define @t270 () (not @t265)) % 0.39/0.78 (define @t271 () (_ tptp.ord_less_eq_nat @t261)) % 0.39/0.78 (define @t272 () (_ @t271 @t88)) % 0.39/0.78 (define @t273 () (_ @t271 @t89)) % 0.39/0.78 (define @t274 () (@var "X5" tptp.nat)) % 0.39/0.78 (define @t275 () (@var "Y5" tptp.nat)) % 0.39/0.78 (define @t276 () (_ @t105 @t61)) % 0.39/0.78 (define @t277 () (_ @t105 @t104)) % 0.39/0.78 (define @t278 () (_ @t105 @t98)) % 0.39/0.78 (define @t279 () (@list @t98 @t104)) % 0.39/0.78 (define @t280 () (forall @t279 (=> (_ (_ tptp.ord_less_eq_nat @t98) @t104) (_ (_ tptp.ord_less_eq_nat @t278) @t277)))) % 0.39/0.78 (define @t281 () (=> @t280 (_ (_ tptp.ord_less_eq_nat @t276) @t58))) % 0.39/0.78 (define @t282 () (_ @t105 @t59)) % 0.39/0.78 (define @t283 () (= @t282 @t58)) % 0.39/0.78 (define @t284 () (@list @t61 @t59 @t105 @t58)) % 0.39/0.78 (define @t285 () (_ @t105 @t58)) % 0.39/0.78 (define @t286 () (=> @t121 (=> @t280 (_ @t122 @t285)))) % 0.39/0.78 (define @t287 () (= @t61 @t282)) % 0.39/0.78 (define @t288 () (@list @t61 @t105 @t59 @t58)) % 0.39/0.78 (define @t289 () (not @t245)) % 0.39/0.78 (define @t290 () (_ tptp.ord_less_nat @t59)) % 0.39/0.78 (define @t291 () (_ @t290 @t61)) % 0.39/0.78 (define @t292 () (@var "P3" (-> tptp.nat Bool))) % 0.39/0.78 (define @t293 () (@var "X3" tptp.nat)) % 0.39/0.78 (define @t294 () (@var "P2" (-> tptp.nat Bool))) % 0.39/0.78 (define @t295 () (not @t91)) % 0.39/0.78 (define @t296 () (_ @t66 @t58)) % 0.39/0.78 (define @t297 () (_ @t290 @t58)) % 0.39/0.78 (define @t298 () (=> @t297 @t296)) % 0.39/0.78 (define @t299 () (@var "P" Bool)) % 0.39/0.78 (define @t300 () (@var "X_1" tptp.nat)) % 0.39/0.78 (define @t301 () (_ tptp.ord_less_nat @t98)) % 0.39/0.78 (define @t302 () (forall @t279 (=> (_ @t301 @t104) (_ (_ tptp.ord_less_nat @t278) @t277)))) % 0.39/0.78 (define @t303 () (=> @t302 (_ (_ tptp.ord_less_nat @t276) @t58))) % 0.39/0.78 (define @t304 () (=> @t297 (=> @t302 (_ @t66 @t285)))) % 0.39/0.78 (define @t305 () (@var "Q2" (-> tptp.nat Bool))) % 0.39/0.78 (define @t306 () (_ @t305 @t149)) % 0.39/0.78 (define @t307 () (@var "P4" (-> tptp.nat Bool))) % 0.39/0.78 (define @t308 () (_ @t307 @t149)) % 0.39/0.78 (define @t309 () (@var "Q" (-> tptp.nat Bool))) % 0.39/0.78 (define @t310 () (_ @t309 @t149)) % 0.39/0.78 (define @t311 () (_ @t72 @t149)) % 0.39/0.78 (define @t312 () (= (and @t311 @t310) (and @t308 @t306))) % 0.39/0.78 (define @t313 () (= (_ @t309 @t98) (_ @t305 @t98))) % 0.39/0.78 (define @t314 () (@var "Z4" tptp.nat)) % 0.39/0.78 (define @t315 () (_ (_ tptp.ord_less_nat @t314) @t98)) % 0.39/0.78 (define @t316 () (@list @t314)) % 0.39/0.78 (define @t317 () (exists @t316 (forall @t103 (=> @t315 @t313)))) % 0.39/0.78 (define @t318 () (= @t102 (_ @t307 @t98))) % 0.39/0.78 (define @t319 () (exists @t316 (forall @t103 (=> @t315 @t318)))) % 0.39/0.78 (define @t320 () (@list @t72 @t307 @t309 @t305)) % 0.39/0.78 (define @t321 () (= (or @t311 @t310) (or @t308 @t306))) % 0.39/0.78 (define @t322 () (not (= @t149 @t70))) % 0.39/0.78 (define @t323 () (_ @t301 @t314)) % 0.39/0.78 (define @t324 () (exists @t316 (forall @t103 (=> @t323 @t313)))) % 0.39/0.78 (define @t325 () (exists @t316 (forall @t103 (=> @t323 @t318)))) % 0.39/0.78 (define @t326 () (_ (_ tptp.nth_co1649820636t_unit @t1) @t15)) % 0.39/0.78 (define @t327 () (_ tptp.last_c571238084t_unit @t1)) % 0.39/0.78 (define @t328 () (= @t327 @t326)) % 0.39/0.78 (define @t329 () (not @t328)) % 0.39/0.78 (define @t330 () (lambda @t87 (and (_ (_ tptp.ord_less_eq_nat @t84) @t83) (not @t85)))) % 0.39/0.78 (define @t331 () (@var "C2" tptp.nat)) % 0.39/0.78 (define @t332 () (lambda @t209 (exists (@list @t331) (= @t208 (_ (_ tptp.plus_plus_nat @t207) @t331))))) % 0.39/0.78 (define @t333 () (tptp.size_s1406904903t_unit @t3)) % 0.39/0.78 (define @t334 () (tptp.minus_minus_nat @t333 tptp.one_one_nat)) % 0.39/0.78 (define @t335 () (tptp.nth_co1649820636t_unit @t3 @t334)) % 0.39/0.78 (define @t336 () (tptp.last_c571238084t_unit @t3)) % 0.39/0.78 (define @t337 () (= tptp.nil_co1338500125t_unit @t3)) % 0.39/0.78 (define @t338 () (or @t337 @t9)) % 0.39/0.78 (define @t339 () (not @t337)) % 0.39/0.78 (define @t340 () (tptp.fe tptp.n)) % 0.39/0.78 (define @t341 () (tptp.last_c571238084t_unit @t340)) % 0.39/0.78 (define @t342 () (tptp.size_s1406904903t_unit @t340)) % 0.39/0.78 (define @t343 () (tptp.minus_minus_nat @t342 tptp.one_one_nat)) % 0.39/0.78 (define @t344 () (tptp.nth_co1649820636t_unit @t340 @t343)) % 0.39/0.78 (define @t345 () (= tptp.nil_co1338500125t_unit @t1)) % 0.39/0.78 (define @t346 () (= @t344 @t341)) % 0.39/0.78 (define @t347 () (= tptp.nil_co1338500125t_unit @t340)) % 0.39/0.78 (define @t348 () (or @t347 @t346)) % 0.39/0.78 (define @t349 () (not @t348)) % 0.39/0.78 (define @t350 () (or @t347 (= @t341 @t344))) % 0.39/0.78 (define @t351 () (forall @t12 (or @t337 (= @t336 @t335)))) % 0.39/0.78 (assume @p1 @t2) % 0.39/0.78 (assume @p2 @t13) % 0.39/0.78 (assume @p3 (_ (_ tptp.ord_less_nat @t15) @t14)) % 0.39/0.78 (assume @p4 (_ (_ tptp.ord_less_nat tptp.n0) @t14)) % 0.39/0.78 (assume @p5 (forall (@list @t16) (=> (not (= @t16 tptp.nil_co1338500125t_unit)) (= (_ tptp.last_c571238084t_unit @t16) (_ @t18 (_ (_ tptp.minus_minus_nat @t17) tptp.one_one_nat)))))) % 0.39/0.78 (assume @p6 (_ (_ tptp.ord_less_eq_nat tptp.n0) @t15)) % 0.39/0.78 (assume @p7 (= tptp.one_one_nat tptp.one_one_nat)) % 0.39/0.78 (assume @p8 (forall @t24 (= @t23 (_ (_ tptp.minus_minus_nat (_ @t22 @t20)) @t19)))) % 0.39/0.78 (assume @p9 (forall @t29 (exists @t28 (= @t27 @t25)))) % 0.39/0.78 (assume @p10 (forall @t33 (=> (not @t32) (not @t31)))) % 0.39/0.78 (assume @p11 (forall (@list @t35 @t34) (=> (not (= (_ tptp.size_s1406904903t_unit @t35) (_ tptp.size_s1406904903t_unit @t34))) (not (= @t35 @t34))))) % 0.39/0.78 (assume @p12 (forall (@list @t21 @t25) (=> (_ @t37 @t25) (= (_ @t36 (_ @t36 @t21)) @t21)))) % 0.39/0.78 (assume @p13 (forall @t29 (_ @t38 @t25))) % 0.39/0.78 (assume @p14 (forall @t24 (=> @t40 (=> (_ @t39 @t20) (_ @t37 @t20))))) % 0.39/0.78 (assume @p15 (forall @t44 (=> @t43 @t42))) % 0.39/0.78 (assume @p16 (forall @t44 (=> @t42 (=> @t45 @t43)))) % 0.39/0.78 (assume @p17 (forall @t44 (= @t50 (or @t49 @t47)))) % 0.39/0.78 (assume @p18 (forall @t57 (=> @t56 (=> @t55 (= (_ (_ tptp.ord_less_nat @t53) @t51) @t49))))) % 0.39/0.78 (assume @p19 (forall @t29 (not (_ @t46 @t25)))) % 0.39/0.78 (assume @p20 (forall @t44 (or @t42 @t45))) % 0.39/0.78 (assume @p21 (forall @t68 (=> @t67 (=> @t65 (_ (_ tptp.ord_less_nat @t63) (_ @t60 @t58)))))) % 0.39/0.78 (assume @p22 (forall @t69 (=> @t47 @t50))) % 0.39/0.78 (assume @p23 (forall (@list @t71 @t70) (=> (_ (_ tptp.ord_less_nat @t71) @t70) (not (= @t71 @t70))))) % 0.39/0.78 (assume @p24 (forall @t44 (=> @t49 @t42))) % 0.39/0.78 (assume @p25 (forall @t82 (=> (forall @t81 (=> (forall @t80 (=> @t79 @t77)) @t75)) @t73))) % 0.39/0.78 (assume @p26 (forall @t82 (=> (forall @t81 (=> (not @t75) (exists @t80 (and @t79 (not @t77))))) @t73))) % 0.39/0.78 (assume @p27 (= tptp.ord_less_eq_nat (lambda @t87 (or @t86 @t85)))) % 0.39/0.78 (assume @p28 (forall @t44 (=> (or @t49 @t43) @t42))) % 0.39/0.78 (assume @p29 (forall @t97 (=> @t96 (=> @t94 @t91)))) % 0.39/0.78 (assume @p30 (forall (@list @t72 @t20 @t59) (=> (_ @t72 @t20) (=> (forall (@list @t104) (=> (_ @t72 @t104) (_ (_ tptp.ord_less_eq_nat @t104) @t59))) (exists @t103 (and @t102 (forall @t101 (=> @t100 (_ (_ tptp.ord_less_eq_nat @t99) @t98))))))))) % 0.39/0.78 (assume @p31 (forall @t44 (=> @t42 (=> @t50 @t49)))) % 0.39/0.78 (assume @p32 (forall (@list @t105 @t21 @t19) (=> (forall (@list @t107 @t106) (=> (_ @t108 @t106) (_ (_ tptp.ord_less_nat (_ @t105 @t107)) (_ @t105 @t106)))) (=> @t40 (_ (_ tptp.ord_less_eq_nat (_ @t105 @t21)) (_ @t105 @t19)))))) % 0.39/0.78 (assume @p33 (forall (@list @t109 @t16) (=> (forall @t28 (=> (forall (@list @t110) (=> (_ (_ tptp.ord_less_nat (_ tptp.size_s1406904903t_unit @t110)) @t27) (_ @t109 @t110))) (_ @t109 @t26))) (_ @t109 @t16)))) % 0.39/0.78 (assume @p34 (forall (@list @t19 @t20 @t25) (=> (_ @t112 @t20) (_ (_ tptp.ord_less_nat (_ @t111 @t25)) @t20)))) % 0.39/0.78 (assume @p35 (forall @t117 (=> @t49 (=> (_ @t48 @t113) (_ (_ tptp.ord_less_nat @t116) @t115))))) % 0.39/0.78 (assume @p36 (forall @t117 (=> @t42 (_ (_ tptp.ord_less_eq_nat @t116) @t115)))) % 0.39/0.78 (assume @p37 (forall @t124 (=> @t123 (=> @t121 (= (_ (_ tptp.ord_less_eq_nat (_ @t120 @t61)) (_ @t120 @t59)) @t119))))) % 0.39/0.78 (assume @p38 (forall @t44 (_ (_ tptp.ord_less_eq_nat @t125) @t41))) % 0.39/0.78 (assume @p39 (forall @t117 (=> @t42 (_ (_ tptp.ord_less_eq_nat (_ @t52 @t113)) (_ @t36 @t113))))) % 0.39/0.78 (assume @p40 (forall @t57 (=> @t56 (=> @t55 (= (_ (_ tptp.minus_minus_nat @t53) @t51) @t125))))) % 0.39/0.78 (assume @p41 (forall @t57 (=> @t56 (=> @t55 (= (_ (_ tptp.ord_less_eq_nat @t53) @t51) @t42))))) % 0.39/0.78 (assume @p42 (forall @t57 (=> @t56 (=> @t55 (= (= @t53 @t51) @t43))))) % 0.39/0.78 (assume @p43 (= (lambda (@list @t134 @t133) (= @t134 @t133)) (lambda (@list @t128 @t127) (and (= @t130 (_ tptp.size_s1406904903t_unit @t127)) (forall @t132 (=> (_ @t131 @t130) (= @t129 (_ (_ tptp.nth_co1649820636t_unit @t127) @t126)))))))) % 0.39/0.78 (assume @p44 (forall (@list @t20 @t135) (= (forall @t132 (=> @t137 (exists (@list @t138) (_ @t136 @t138)))) (exists (@list @t128) (and (= @t130 @t20) (forall @t132 (=> @t137 (_ @t136 @t129)))))))) % 0.39/0.78 (assume @p45 (forall @t33 (=> @t32 (=> (forall (@list @t107) (=> (_ @t108 @t17) (= (_ @t18 @t107) (_ (_ tptp.nth_co1649820636t_unit @t30) @t107)))) @t31)))) % 0.39/0.78 (assume @p46 (forall @t139 (= (= tptp.one_one_nat @t88) (= @t88 tptp.one_one_nat)))) % 0.39/0.78 (assume @p47 (forall @t124 (= (_ (_ tptp.minus_minus_nat @t63) @t59) @t141))) % 0.39/0.78 (assume @p48 (forall (@list @t142) (_ (_ tptp.ord_less_eq_nat (_ (_ tptp.plus_plus_nat @t142) tptp.one_one_nat)) (_ tptp.size_s1406904903t_unit @t143)))) % 0.39/0.78 (assume @p49 (forall (@list @t76 @t142) (=> (_ @t78 @t142) (_ (_ tptp.prefix1615116500t_unit (_ tptp.fe @t76)) @t143)))) % 0.39/0.78 (assume @p50 (forall @t139 (_ @t144 @t88))) % 0.39/0.78 (assume @p51 (forall (@list @t25 @t72 @t41) (=> (forall @t148 (=> (_ @t46 @t145) @t146)) (=> (forall @t148 (=> (_ (_ tptp.ord_less_eq_nat @t145) @t25) (=> (forall (@list @t147) (=> (_ (_ tptp.ord_less_nat @t145) @t147) (_ @t72 @t147))) @t146))) (_ @t72 @t41))))) % 0.39/0.78 (assume @p52 (not (_ (_ tptp.ord_less_nat tptp.one_one_nat) tptp.one_one_nat))) % 0.39/0.78 (assume @p53 (_ (_ tptp.ord_less_eq_nat tptp.one_one_nat) tptp.one_one_nat)) % 0.39/0.78 (assume @p54 (forall @t156 (exists @t155 (forall @t154 (=> @t153 (not @t150)))))) % 0.39/0.78 (assume @p55 (forall @t156 (exists @t155 (forall @t154 (=> @t153 @t157))))) % 0.39/0.78 (assume @p56 (forall @t156 (exists @t155 (forall @t154 (=> @t158 @t150))))) % 0.39/0.78 (assume @p57 (forall @t156 (exists @t155 (forall @t154 (=> @t158 (not @t157)))))) % 0.39/0.78 (assume @p58 (forall @t68 (= @t163 @t159))) % 0.39/0.78 (assume @p59 (forall @t168 (= @t167 @t159))) % 0.39/0.78 (assume @p60 (forall @t124 (= @t172 @t169))) % 0.39/0.78 (assume @p61 (forall @t176 (= @t175 @t169))) % 0.39/0.78 (assume @p62 (forall @t124 (= @t178 @t67))) % 0.39/0.78 (assume @p63 (forall @t176 (= @t179 @t67))) % 0.39/0.78 (assume @p64 (forall @t176 (= (_ @t180 @t173) @t140))) % 0.39/0.78 (assume @p65 (forall @t182 (= (_ @t181 @t61) @t59))) % 0.39/0.78 (assume @p66 (forall @t124 (= (_ (_ tptp.minus_minus_nat @t161) @t170) @t140))) % 0.39/0.78 (assume @p67 (forall @t182 (= (_ @t181 @t59) @t61))) % 0.39/0.78 (assume @p68 (forall @t57 (= (_ (_ tptp.ord_less_nat @t185) @t184) @t49))) % 0.39/0.78 (assume @p69 (forall @t57 (= (_ (_ tptp.ord_less_eq_nat @t185) @t184) @t42))) % 0.39/0.78 (assume @p70 (forall @t24 (= @t23 (_ @t22 @t187)))) % 0.39/0.78 (assume @p71 (forall @t192 (=> @t191 (= (_ @t22 @t190) (_ (_ tptp.minus_minus_nat @t189) @t19))))) % 0.39/0.78 (assume @p72 (forall @t192 (=> @t191 (= @t195 @t194)))) % 0.39/0.78 (assume @p73 (forall @t192 (=> @t191 (= @t198 @t197)))) % 0.39/0.78 (assume @p74 (forall @t68 (= (_ (_ tptp.plus_plus_nat @t162) @t58) @t199))) % 0.39/0.78 (assume @p75 (forall @t203 (=> (and @t202 @t201) (= @t189 @t200)))) % 0.39/0.78 (assume @p76 (forall (@list @t205 @t20 @t61 @t59) (=> (= @t205 (_ @t183 @t61)) (= (_ (_ tptp.plus_plus_nat @t205) @t59) @t204)))) % 0.39/0.78 (assume @p77 (forall (@list @t206 @t20 @t59 @t61) (=> (= @t206 (_ @t183 @t59)) (= (_ @t160 @t206) @t204)))) % 0.39/0.78 (assume @p78 (= tptp.plus_plus_nat (lambda @t209 (_ (_ tptp.plus_plus_nat @t208) @t207)))) % 0.39/0.78 (assume @p79 (forall @t168 (= (_ @t166 @t161) @t199))) % 0.39/0.78 (assume @p80 (forall @t68 (=> @t163 @t159))) % 0.39/0.78 (assume @p81 (forall @t168 (=> @t167 @t159))) % 0.39/0.78 (assume @p82 (forall @t124 (=> @t172 @t169))) % 0.39/0.78 (assume @p83 (forall @t176 (=> @t175 @t169))) % 0.39/0.78 (assume @p84 (forall @t68 (=> @t169 @t172))) % 0.39/0.78 (assume @p85 (forall @t182 (=> @t169 (not (forall (@list @t210) (not (= @t59 (_ @t160 @t210)))))))) % 0.39/0.78 (assume @p86 (forall @t68 (=> @t169 @t175))) % 0.39/0.78 (assume @p87 (forall @t214 (=> @t169 (=> @t213 (_ @t171 @t212))))) % 0.39/0.78 (assume @p88 (forall @t203 (=> (and @t40 @t217) @t216))) % 0.39/0.78 (assume @p89 (forall @t203 (=> (and @t202 @t217) @t216))) % 0.39/0.78 (assume @p90 (forall @t203 (=> (and @t40 @t201) @t216))) % 0.39/0.78 (assume @p91 (forall @t124 (=> @t178 @t67))) % 0.39/0.78 (assume @p92 (forall @t176 (=> @t179 @t67))) % 0.39/0.78 (assume @p93 (forall @t68 (=> @t67 @t178))) % 0.39/0.78 (assume @p94 (forall @t68 (=> @t67 @t179))) % 0.39/0.78 (assume @p95 (forall @t214 (=> @t67 @t220))) % 0.39/0.78 (assume @p96 (forall @t203 (=> (and @t224 @t201) @t222))) % 0.39/0.78 (assume @p97 (forall @t203 (=> (and @t202 @t225) @t222))) % 0.39/0.78 (assume @p98 (forall @t203 (=> (and @t224 @t225) @t222))) % 0.39/0.78 (assume @p99 (forall @t68 (= @t141 (_ @t62 @t170)))) % 0.39/0.78 (assume @p100 (forall (@list @t58 @t59 @t61) (=> (= @t173 @t61) (= @t58 @t140)))) % 0.39/0.78 (assume @p101 (forall (@list @t20 @t113 @t41 @t25) (=> @t225 (=> (= (_ @t226 @t113) @t184) @t49)))) % 0.39/0.78 (assume @p102 (forall @t228 (=> @t224 (_ @t223 @t227)))) % 0.39/0.78 (assume @p103 (forall @t228 (=> @t224 (_ @t223 @t229)))) % 0.39/0.78 (assume @p104 (forall @t24 (=> @t224 (_ @t221 @t187)))) % 0.39/0.78 (assume @p105 (forall (@list @t19 @t21) (not (_ (_ tptp.ord_less_nat @t193) @t21)))) % 0.39/0.78 (assume @p106 (forall (@list @t21 @t19) (not (_ @t230 @t21)))) % 0.39/0.78 (assume @p107 (forall @t203 (=> @t224 (=> @t225 @t222)))) % 0.39/0.78 (assume @p108 (forall @t24 (=> (_ @t230 @t20) (_ @t223 @t20)))) % 0.39/0.78 (assume @p109 (= tptp.ord_less_eq_nat (lambda @t87 (exists (@list @t231) (= @t83 (_ (_ tptp.plus_plus_nat @t84) @t231)))))) % 0.39/0.78 (assume @p110 (forall @t228 (=> @t40 (_ @t37 @t227)))) % 0.39/0.78 (assume @p111 (forall @t228 (=> @t40 (_ @t37 @t229)))) % 0.39/0.78 (assume @p112 (forall @t24 (=> @t40 (_ @t215 @t187)))) % 0.39/0.78 (assume @p113 (forall @t203 (=> @t40 (=> @t217 @t216)))) % 0.39/0.78 (assume @p114 (forall (@list @t20 @t113) (=> @t217 (exists @t81 (= @t113 (_ @t183 @t74)))))) % 0.39/0.78 (assume @p115 (forall @t234 (=> @t233 @t55))) % 0.39/0.78 (assume @p116 (forall @t234 (=> @t233 @t42))) % 0.39/0.78 (assume @p117 (forall @t69 (_ @t38 @t235))) % 0.39/0.78 (assume @p118 (forall @t69 (_ @t38 @t237))) % 0.39/0.78 (assume @p119 (forall @t234 (=> @t233 (not (=> @t42 (not @t55)))))) % 0.39/0.78 (assume @p120 (forall @t57 (= (_ (_ tptp.minus_minus_nat @t185) @t184) @t125))) % 0.39/0.78 (assume @p121 (forall @t234 (= (_ (_ tptp.minus_minus_nat @t232) (_ @t236 @t20)) @t125))) % 0.39/0.78 (assume @p122 (forall @t69 (= (_ (_ tptp.minus_minus_nat @t237) @t25) @t41))) % 0.39/0.78 (assume @p123 (forall @t44 (= (_ (_ tptp.minus_minus_nat @t235) @t25) @t41))) % 0.39/0.78 (assume @p124 (forall @t214 (=> @t67 (=> @t213 @t218)))) % 0.39/0.78 (assume @p125 (forall @t214 (=> @t169 @t220))) % 0.39/0.78 (assume @p126 (forall @t203 (=> (and @t224 @t217) @t222))) % 0.39/0.78 (assume @p127 (forall @t203 (=> (and @t40 @t225) @t222))) % 0.39/0.78 (assume @p128 (forall @t68 (=> @t169 (=> @t169 (= (= @t238 @t58) (= @t59 @t165)))))) % 0.39/0.78 (assume @p129 (forall @t182 (=> @t169 (= (_ @t160 @t238) @t59)))) % 0.39/0.78 (assume @p130 (forall @t68 (=> @t169 (= (_ @t120 @t238) (_ @t180 @t59))))) % 0.39/0.78 (assume @p131 (forall @t68 (=> @t169 (= @t241 @t240)))) % 0.39/0.78 (assume @p132 (forall @t68 (=> @t169 (= @t240 @t241)))) % 0.39/0.78 (assume @p133 (forall @t68 (=> @t169 (= @t243 @t242)))) % 0.39/0.78 (assume @p134 (forall @t68 (=> @t169 (= @t242 @t243)))) % 0.39/0.78 (assume @p135 (forall @t68 (=> @t169 (= (_ @t64 @t238) (_ @t174 @t59))))) % 0.39/0.78 (assume @p136 (forall @t68 (=> @t169 (_ @t64 @t241)))) % 0.39/0.78 (assume @p137 (forall @t182 (=> @t169 (= (_ @t239 @t61) @t59)))) % 0.39/0.78 (assume @p138 (forall (@list @t105 @t41 @t20) (=> (forall (@list @t244 @t74) (=> (_ (_ tptp.ord_less_nat @t244) @t74) (_ (_ tptp.ord_less_nat (_ @t105 @t244)) (_ @t105 @t74)))) (_ (_ tptp.ord_less_eq_nat (_ (_ tptp.plus_plus_nat (_ @t105 @t41)) @t20)) (_ @t105 @t232))))) % 0.39/0.78 (assume @p139 (forall @t44 (=> (not @t49) (= (_ @t236 @t125) @t41)))) % 0.39/0.78 (assume @p140 (forall @t24 (= (_ @t223 @t190) (_ @t221 @t19)))) % 0.39/0.78 (assume @p141 (forall @t24 (=> @t40 (= (= (_ @t111 @t21) @t20) (= @t19 (_ @t183 @t21)))))) % 0.39/0.78 (assume @p142 (forall @t192 (=> @t191 (= @t194 @t195)))) % 0.39/0.78 (assume @p143 (forall @t192 (=> @t191 (= @t197 @t198)))) % 0.39/0.78 (assume @p144 (forall @t192 (=> @t191 (= (_ @t37 @t190) (_ @t215 @t19))))) % 0.39/0.78 (assume @p145 (forall (@list @t19 @t20 @t21) (= (_ (_ tptp.ord_less_eq_nat @t190) @t21) (_ @t39 @t189)))) % 0.39/0.78 (assume @p146 (forall @t192 (=> @t191 (= (_ (_ tptp.ord_less_nat @t190) @t21) (_ @t112 @t189))))) % 0.39/0.78 (assume @p147 (forall @t246 (=> @t119 (=> @t169 @t245)))) % 0.39/0.78 (assume @p148 (= @t251 (lambda @t209 (and @t248 @t247)))) % 0.39/0.78 (assume @p149 (forall @t168 (=> @t119 (=> (_ @t64 @t59) @t65)))) % 0.39/0.78 (assume @p150 (forall @t259 (=> (forall @t257 (=> (_ (_ tptp.ord_less_eq_nat @t254) @t253) @t256)) @t258))) % 0.39/0.78 (assume @p151 (forall @t260 (_ @t122 @t61))) % 0.39/0.78 (assume @p152 (forall @t266 (=> @t265 (=> @t264 @t262)))) % 0.39/0.78 (assume @p153 (forall @t182 (=> @t169 (=> @t119 @t245)))) % 0.39/0.78 (assume @p154 (forall @t68 (=> @t169 (=> @t159 @t123)))) % 0.39/0.78 (assume @p155 (forall @t68 (=> @t245 @t267))) % 0.39/0.78 (assume @p156 (= @t251 (lambda @t209 (and @t247 @t248)))) % 0.39/0.78 (assume @p157 (forall @t269 (=> @t268 (= @t265 @t95)))) % 0.39/0.78 (assume @p158 (forall @t266 (=> (=> @t265 (not @t264)) (=> (=> @t268 (not @t262)) (=> (=> @t262 (not @t273)) (=> (=> @t273 (not @t268)) (=> (=> @t264 (not @t272)) (not (=> @t272 @t270))))))))) % 0.39/0.78 (assume @p159 (forall @t68 (=> @t169 @t267))) % 0.39/0.78 (assume @p160 (forall @t97 (=> @t270 @t268))) % 0.39/0.78 (assume @p161 (forall @t97 (=> @t95 @t265))) % 0.39/0.78 (assume @p162 (forall @t97 (or @t265 @t268))) % 0.39/0.78 (assume @p163 (forall @t97 (=> @t265 (=> @t268 @t95)))) % 0.39/0.78 (assume @p164 (= @t251 (lambda (@list @t274 @t275) (and (_ (_ tptp.ord_less_eq_nat @t274) @t275) (_ (_ tptp.ord_less_eq_nat @t275) @t274))))) % 0.39/0.78 (assume @p165 (forall @t284 (=> @t169 (=> @t283 @t281)))) % 0.39/0.78 (assume @p166 (forall @t288 (=> @t287 @t286))) % 0.39/0.78 (assume @p167 (forall @t284 (=> @t169 (=> (_ (_ tptp.ord_less_eq_nat @t282) @t58) @t281)))) % 0.39/0.78 (assume @p168 (forall @t288 (=> (_ @t122 @t282) @t286))) % 0.39/0.78 (assume @p169 (forall @t246 (=> @t291 @t289))) % 0.39/0.78 (assume @p170 (forall @t182 (=> @t67 @t289))) % 0.39/0.78 (assume @p171 (forall @t97 (= @t94 (or @t91 @t95)))) % 0.39/0.78 (assume @p172 (forall @t168 (=> @t291 (=> (_ @t219 @t59) (_ @t219 @t61))))) % 0.39/0.78 (assume @p173 (forall @t259 (=> (forall @t257 (=> (_ (_ tptp.ord_less_nat @t254) @t253) @t256)) (=> (forall (@list @t254) (_ @t255 @t254)) @t258)))) % 0.39/0.78 (assume @p174 (= (lambda (@list @t294) (exists (@list @t293) (_ @t294 @t293))) (lambda (@list @t292) (exists (@list @t83) (and (_ @t292 @t83) (forall (@list @t84) (=> @t86 (not (_ @t292 @t84))))))))) % 0.39/0.78 (assume @p175 (forall @t97 (=> @t93 @t295))) % 0.39/0.78 (assume @p176 (forall @t68 (=> @t67 @t298))) % 0.39/0.78 (assume @p177 (forall @t260 (not (_ @t66 @t61)))) % 0.39/0.78 (assume @p178 (forall @t97 (=> @t94 (=> @t96 @t91)))) % 0.39/0.78 (assume @p179 (forall (@list @t88 @t89 @t299) (=> @t93 (=> @t91 @t299)))) % 0.39/0.78 (assume @p180 (forall @t97 (=> @t93 (not (= @t89 @t88))))) % 0.39/0.78 (assume @p181 (forall @t269 (=> @t295 (= @t94 @t95)))) % 0.39/0.78 (assume @p182 (forall (@list @t72 @t61) (=> (forall @t103 (=> (forall @t101 (=> (_ (_ tptp.ord_less_nat @t99) @t98) @t100)) @t102)) (_ @t72 @t61)))) % 0.39/0.78 (assume @p183 (forall @t97 (=> @t93 @t96))) % 0.39/0.78 (assume @p184 (forall @t246 (=> @t291 (not @t67)))) % 0.39/0.78 (assume @p185 (forall @t68 (=> @t67 (=> @t159 @t296)))) % 0.39/0.78 (assume @p186 (forall @t68 (=> @t245 @t298))) % 0.39/0.78 (assume @p187 (forall @t139 (not (_ @t92 @t88)))) % 0.39/0.78 (assume @p188 (forall @t97 (or @t93 @t95 @t91))) % 0.39/0.78 (assume @p189 (forall @t266 (=> @t93 (=> (_ @t90 @t261) (_ @t92 @t261))))) % 0.39/0.78 (assume @p190 (forall @t182 (=> @t67 (not @t291)))) % 0.39/0.78 (assume @p191 (forall @t97 (= @t96 (or @t93 @t91)))) % 0.39/0.78 (assume @p192 (forall @t139 (exists (@list @t300) (_ @t92 @t300)))) % 0.39/0.78 (assume @p193 (forall @t284 (=> @t67 (=> (_ (_ tptp.ord_less_nat @t282) @t58) @t303)))) % 0.39/0.78 (assume @p194 (forall @t288 (=> (_ @t66 @t282) @t304))) % 0.39/0.78 (assume @p195 (forall @t284 (=> @t67 (=> @t283 @t303)))) % 0.39/0.78 (assume @p196 (forall @t288 (=> @t287 @t304))) % 0.39/0.78 (assume @p197 (forall @t320 (=> @t319 (=> @t317 (exists @t155 (forall @t154 (=> @t158 @t312))))))) % 0.39/0.78 (assume @p198 (forall @t320 (=> @t319 (=> @t317 (exists @t155 (forall @t154 (=> @t158 @t321))))))) % 0.39/0.78 (assume @p199 (forall @t156 (exists @t155 (forall @t154 (=> @t158 @t322))))) % 0.39/0.78 (assume @p200 (forall @t156 (exists @t155 (forall @t154 (=> @t158 (not (_ @t152 @t70))))))) % 0.39/0.78 (assume @p201 (forall @t156 (exists @t155 (forall @t154 (=> @t158 (_ (_ tptp.ord_less_nat @t70) @t149)))))) % 0.39/0.78 (assume @p202 (forall @t320 (=> @t325 (=> @t324 (exists @t155 (forall @t154 (=> @t153 @t312))))))) % 0.39/0.78 (assume @p203 (forall @t320 (=> @t325 (=> @t324 (exists @t155 (forall @t154 (=> @t153 @t321))))))) % 0.39/0.78 (assume @p204 (forall @t156 (exists @t155 (forall @t154 (=> @t153 @t322))))) % 0.39/0.78 (assume @p205 @t329) % 0.39/0.78 (assume @p206 true) % 0.39/0.78 (step @p207 (= tptp.ord_less_nat @t330) :rule refl :args (@t330)) % 0.39/0.78 (step @p208 (= tptp.ord_less_eq_nat @t332) :rule refl :args (@t332)) % 0.39/0.78 (step @p209 :rule refl :args ((tptp.nth_co1649820636t_unit @t3 @t5))) % 0.39/0.78 (step @p210 :rule refl :args ((tptp.minus_minus_nat @t4 tptp.one_one_nat))) % 0.39/0.78 (step @p211 :rule refl :args (tptp.one_one_nat)) % 0.39/0.78 (step @p212 :rule refl :args (@t333)) % 0.39/0.78 (step @p213 :rule cong :premises (@p212 @p211) :args (@t334)) % 0.39/0.78 (step @p214 :rule trans :premises (@p213 @p210)) % 0.39/0.78 (step @p215 :rule refl :args (@t3)) % 0.39/0.78 (step @p216 :rule cong :premises (@p215 @p214) :args (@t335)) % 0.39/0.78 (step @p217 :rule trans :premises (@p216 @p209)) % 0.39/0.78 (step @p218 :rule refl :args (@t6)) % 0.39/0.78 (step @p219 :rule ho_cong :premises (@p218 @p214)) % 0.39/0.78 (step @p220 :rule cong :premises (@p219 @p217) :args ((= (_ @t6 @t334) @t335))) % 0.39/0.78 (step @p221 :rule symm :premises (@p220)) % 0.39/0.78 (step @p222 :rule refl :args (@t7)) % 0.39/0.78 (step @p223 :rule eq_resolve :premises (@p222 @p221)) % 0.39/0.78 (step @p224 :rule refl :args (tptp.minus_minus_nat)) % 0.39/0.78 (step @p225 :rule ho_cong :premises (@p224 @p212)) % 0.39/0.78 (step @p226 :rule ho_cong :premises (@p225 @p211)) % 0.39/0.78 (step @p227 :rule cong :premises (@p226 @p214) :args ((= (_ (_ tptp.minus_minus_nat @t333) tptp.one_one_nat) @t334))) % 0.39/0.78 (step @p228 :rule symm :premises (@p227)) % 0.39/0.78 (step @p229 :rule refl :args (@t5)) % 0.39/0.78 (step @p230 :rule eq_resolve :premises (@p229 @p228)) % 0.39/0.78 (step @p231 :rule refl :args (@t4)) % 0.39/0.78 (step @p232 :rule cong :premises (@p231 @p212) :args ((= @t4 @t333))) % 0.39/0.78 (step @p233 :rule symm :premises (@p232)) % 0.39/0.78 (step @p234 :rule eq_resolve :premises (@p231 @p233)) % 0.39/0.78 (step @p235 :rule ho_cong :premises (@p224 @p234)) % 0.39/0.78 (step @p236 :rule ho_cong :premises (@p235 @p211)) % 0.39/0.78 (step @p237 :rule trans :premises (@p236 @p230)) % 0.39/0.78 (step @p238 :rule ho_cong :premises (@p218 @p237)) % 0.39/0.78 (step @p239 :rule trans :premises (@p238 @p223)) % 0.39/0.78 (step @p240 :rule refl :args (@t336)) % 0.39/0.78 (step @p241 :rule refl :args (@t8)) % 0.39/0.78 (step @p242 :rule cong :premises (@p241 @p240) :args ((= @t8 @t336))) % 0.39/0.78 (step @p243 :rule symm :premises (@p242)) % 0.39/0.78 (step @p244 :rule eq_resolve :premises (@p241 @p243)) % 0.39/0.78 (step @p245 :rule cong :premises (@p244 @p239) :args (@t9)) % 0.39/0.78 (step @p246 :rule refl :args (@t337)) % 0.39/0.78 (step @p247 :rule nary_cong :premises (@p246 @p245) :args (@t338)) % 0.39/0.78 (step @p248 :rule cong :premises (@p247) :args ((forall @t12 @t338))) % 0.39/0.78 (step @p249 :rule refl :args (@t9)) % 0.39/0.78 (step @p250 :rule bool-double-not-elim :args (@t337)) % 0.39/0.78 (step @p251 :rule nary_cong :premises (@p250 @p249) :args ((or (not @t339) @t9))) % 0.39/0.78 (step @p252 :rule bool-impl-elim :args (@t339 @t9)) % 0.39/0.78 (step @p253 :rule trans :premises (@p252 @p251)) % 0.39/0.78 (step @p254 :rule cong :premises (@p253) :args ((forall @t12 (=> @t339 @t9)))) % 0.39/0.78 (step @p255 :rule trans :premises (@p254 @p248)) % 0.39/0.78 (step @p256 :rule refl :args (@t9)) % 0.39/0.78 (step @p257 :rule eq-symm :args (@t3 tptp.nil_co1338500125t_unit)) % 0.39/0.78 (step @p258 :rule cong :premises (@p257) :args (@t10)) % 0.39/0.78 (step @p259 :rule cong :premises (@p258 @p256) :args (@t11)) % 0.39/0.78 (step @p260 :rule cong :premises (@p259) :args (@t13)) % 0.39/0.78 (step @p261 :rule trans :premises (@p260 @p255)) % 0.39/0.78 (step @p262 :rule eq_resolve :premises (@p2 @p261)) % 0.39/0.78 (step @p263 :rule eq-symm :args (@t341 @t344)) % 0.39/0.78 (step @p264 :rule refl :args ((tptp.nth_co1649820636t_unit @t1 @t15))) % 0.39/0.78 (step @p265 :rule refl :args ((tptp.minus_minus_nat @t14 tptp.one_one_nat))) % 0.39/0.78 (step @p266 :rule refl :args ((tptp.size_s1406904903t_unit @t1))) % 0.39/0.78 (step @p267 :rule refl :args (@t340)) % 0.39/0.78 (step @p268 :rule cong :premises (@p267) :args (@t342)) % 0.39/0.78 (step @p269 :rule trans :premises (@p268 @p266)) % 0.39/0.78 (step @p270 :rule cong :premises (@p269 @p211) :args (@t343)) % 0.39/0.78 (step @p271 :rule trans :premises (@p270 @p265)) % 0.39/0.78 (step @p272 :rule cong :premises (@p267 @p271) :args (@t344)) % 0.39/0.78 (step @p273 :rule trans :premises (@p272 @p264)) % 0.39/0.78 (step @p274 :rule refl :args (tptp.nth_co1649820636t_unit)) % 0.39/0.78 (step @p275 :rule ho_cong :premises (@p274 @p267)) % 0.39/0.78 (step @p276 :rule ho_cong :premises (@p275 @p271)) % 0.39/0.78 (step @p277 :rule cong :premises (@p276 @p273) :args ((= (_ (_ tptp.nth_co1649820636t_unit @t340) @t343) @t344))) % 0.39/0.78 (step @p278 :rule symm :premises (@p277)) % 0.39/0.78 (step @p279 :rule refl :args (@t326)) % 0.39/0.78 (step @p280 :rule eq_resolve :premises (@p279 @p278)) % 0.39/0.78 (step @p281 :rule ho_cong :premises (@p224 @p269)) % 0.39/0.78 (step @p282 :rule ho_cong :premises (@p281 @p211)) % 0.39/0.78 (step @p283 :rule cong :premises (@p282 @p271) :args ((= (_ (_ tptp.minus_minus_nat @t342) tptp.one_one_nat) @t343))) % 0.39/0.78 (step @p284 :rule symm :premises (@p283)) % 0.39/0.78 (step @p285 :rule refl :args (@t15)) % 0.39/0.78 (step @p286 :rule eq_resolve :premises (@p285 @p284)) % 0.39/0.78 (step @p287 :rule refl :args (tptp.one_one_nat)) % 0.39/0.78 (step @p288 :rule refl :args (tptp.size_s1406904903t_unit)) % 0.39/0.78 (step @p289 :rule ho_cong :premises (@p288 @p267)) % 0.39/0.78 (step @p290 :rule cong :premises (@p289 @p269) :args ((= (_ tptp.size_s1406904903t_unit @t340) @t342))) % 0.39/0.78 (step @p291 :rule symm :premises (@p290)) % 0.39/0.78 (step @p292 :rule refl :args (@t14)) % 0.39/0.78 (step @p293 :rule eq_resolve :premises (@p292 @p291)) % 0.39/0.78 (step @p294 :rule refl :args (@t1)) % 0.39/0.78 (step @p295 :rule cong :premises (@p294 @p267) :args ((= @t1 @t340))) % 0.39/0.78 (step @p296 :rule symm :premises (@p295)) % 0.39/0.78 (step @p297 :rule eq_resolve :premises (@p294 @p296)) % 0.39/0.78 (step @p298 :rule refl :args (tptp.size_s1406904903t_unit)) % 0.39/0.78 (step @p299 :rule ho_cong :premises (@p298 @p297)) % 0.39/0.78 (step @p300 :rule trans :premises (@p299 @p293)) % 0.39/0.78 (step @p301 :rule refl :args (tptp.minus_minus_nat)) % 0.39/0.78 (step @p302 :rule ho_cong :premises (@p301 @p300)) % 0.39/0.78 (step @p303 :rule ho_cong :premises (@p302 @p287)) % 0.39/0.78 (step @p304 :rule trans :premises (@p303 @p286)) % 0.39/0.78 (step @p305 :rule refl :args (tptp.nth_co1649820636t_unit)) % 0.39/0.78 (step @p306 :rule ho_cong :premises (@p305 @p297)) % 0.39/0.78 (step @p307 :rule ho_cong :premises (@p306 @p304)) % 0.39/0.78 (step @p308 :rule trans :premises (@p307 @p280)) % 0.39/0.78 (step @p309 :rule refl :args ((tptp.last_c571238084t_unit @t1))) % 0.39/0.78 (step @p310 :rule cong :premises (@p267) :args (@t341)) % 0.39/0.78 (step @p311 :rule trans :premises (@p310 @p309)) % 0.39/0.78 (step @p312 :rule refl :args (tptp.last_c571238084t_unit)) % 0.39/0.78 (step @p313 :rule ho_cong :premises (@p312 @p267)) % 0.39/0.78 (step @p314 :rule cong :premises (@p313 @p311) :args ((= (_ tptp.last_c571238084t_unit @t340) @t341))) % 0.39/0.78 (step @p315 :rule symm :premises (@p314)) % 0.39/0.78 (step @p316 :rule refl :args (@t327)) % 0.39/0.78 (step @p317 :rule eq_resolve :premises (@p316 @p315)) % 0.39/0.78 (step @p318 :rule refl :args (tptp.last_c571238084t_unit)) % 0.39/0.78 (step @p319 :rule ho_cong :premises (@p318 @p297)) % 0.39/0.78 (step @p320 :rule trans :premises (@p319 @p317)) % 0.39/0.78 (step @p321 :rule cong :premises (@p320 @p308) :args (@t328)) % 0.39/0.78 (step @p322 :rule trans :premises (@p321 @p263)) % 0.39/0.78 (step @p323 :rule cong :premises (@p322) :args (@t329)) % 0.39/0.78 (step @p324 :rule eq_resolve :premises (@p205 @p323)) % 0.39/0.78 (step @p325 :rule refl :args (tptp.nil_co1338500125t_unit)) % 0.39/0.78 (step @p326 :rule cong :premises (@p325 @p297) :args (@t345)) % 0.39/0.78 (step @p327 :rule cong :premises (@p326) :args ((not @t345))) % 0.39/0.78 (step @p328 :rule eq-symm :args (@t1 tptp.nil_co1338500125t_unit)) % 0.39/0.78 (step @p329 :rule cong :premises (@p328) :args (@t2)) % 0.39/0.78 (step @p330 :rule trans :premises (@p329 @p327)) % 0.39/0.78 (step @p331 :rule eq_resolve :premises (@p1 @p330)) % 0.39/0.78 (step @p332 :rule cnf_or_pos :args (@t348)) % 0.39/0.78 (step @p333 :rule reordering :premises (@p332) :args ((or @t347 @t346 @t349))) % 0.39/0.78 (step @p334 :rule chain_m_resolution :premises (@p333 @p331 @p324) :args (@t349 (@list true true) (@list @t347 @t346))) % 0.39/0.78 (step @p335 :rule refl :args (@t347)) % 0.39/0.78 (step @p336 :rule nary_cong :premises (@p335 @p263) :args (@t350)) % 0.39/0.78 (step @p337 :rule refl :args (@t351)) % 0.39/0.78 (step @p338 :rule cong :premises (@p337 @p336) :args ((=> @t351 @t350))) % 0.39/0.78 (assume-push @p346 @t351) % 0.39/0.78 (step @p340 :rule instantiate :premises (@p262) :args ((@list @t340))) % 0.39/0.78 (step-pop @p347 :rule scope :premises (@p340)) % 0.39/0.78 (step @p341 :rule process_scope :premises (@p347) :args (@t350)) % 0.39/0.78 (step @p343 :rule eq_resolve :premises (@p341 @p338)) % 0.39/0.78 (step @p344 :rule implies_elim :premises (@p343)) % 0.39/0.78 (step @p345 false :rule chain_m_resolution :premises (@p344 @p334 @p262) :args (false (@list true false) (@list @t348 @t351))) % 0.39/0.78 ) % 0.39/0.78 % SZS output end Proof % 0.39/0.78 % cvc5 exiting %------------------------------------------------------------------------------