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