%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ITP060^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 : n011.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:56 AM UTC 2026 % Result : Theorem 0.40s 0.89s % Output : Proof 0.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP060^1 : TPTP v9.2.1. Released v7.5.0. % 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.17/0.34 % Computer : n011.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.34 % DateTime : Tue Jun 2 04:12:20 EDT 2026 % 0.17/0.34 % CPUTime : % 0.38/0.57 %----Proving TH0 % 0.40/0.89 --- 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.40/0.89 % SZS status Theorem % 0.40/0.89 % SZS output start Proof % 0.40/0.89 ( % 0.40/0.89 (declare-sort tptp.list_c1059388851t_unit 0) % 0.40/0.89 (declare-sort tptp.list_message_p_v 0) % 0.40/0.89 (declare-sort tptp.message_p_v 0) % 0.40/0.89 (declare-sort tptp.nat 0) % 0.40/0.89 (declare-sort tptp.config256849571t_unit 0) % 0.40/0.89 (declare-const tptp.ord_less_eq_nat (-> tptp.nat tptp.nat Bool)) % 0.40/0.89 (declare-const tptp.firstO1414030372_p_v_s (-> tptp.list_c1059388851t_unit tptp.list_message_p_v tptp.message_p_v tptp.nat Bool)) % 0.40/0.89 (declare-const tptp.fLPThe1519354920_p_v_s (-> tptp.config256849571t_unit (-> tptp.list_c1059388851t_unit tptp.list_message_p_v tptp.list_c1059388851t_unit) (-> tptp.list_c1059388851t_unit tptp.list_message_p_v tptp.list_message_p_v) tptp.nat tptp.list_c1059388851t_unit)) % 0.40/0.89 (declare-const tptp.last_message_p_v (-> tptp.list_message_p_v tptp.message_p_v)) % 0.40/0.89 (declare-const tptp.nth_message_p_v (-> tptp.list_message_p_v tptp.nat tptp.message_p_v)) % 0.40/0.89 (declare-const tptp.n tptp.nat) % 0.40/0.89 (declare-const tptp.last_c571238084t_unit (-> tptp.list_c1059388851t_unit tptp.config256849571t_unit)) % 0.40/0.89 (declare-const tptp.msg tptp.message_p_v) % 0.40/0.89 (declare-const tptp.nil_message_p_v tptp.list_message_p_v) % 0.40/0.89 (declare-const tptp.size_s1168481041ge_p_v (-> tptp.list_message_p_v tptp.nat)) % 0.40/0.89 (declare-const tptp.prefix47729710ge_p_v (-> tptp.list_message_p_v tptp.list_message_p_v Bool)) % 0.40/0.89 (declare-const tptp.nMsg tptp.nat) % 0.40/0.89 (declare-const tptp.enabled_p_v_s (-> tptp.config256849571t_unit tptp.message_p_v Bool)) % 0.40/0.89 (declare-const tptp.n0 tptp.nat) % 0.40/0.89 (declare-const tptp.prefix1615116500t_unit (-> tptp.list_c1059388851t_unit tptp.list_c1059388851t_unit Bool)) % 0.40/0.89 (declare-const tptp.fLPThe536531371_p_v_s (-> tptp.config256849571t_unit (-> tptp.list_c1059388851t_unit tptp.list_message_p_v tptp.list_c1059388851t_unit) (-> tptp.list_c1059388851t_unit tptp.list_message_p_v tptp.list_message_p_v) tptp.nat tptp.list_message_p_v)) % 0.40/0.89 (declare-const tptp.fe (-> tptp.nat tptp.list_c1059388851t_unit)) % 0.40/0.89 (declare-const tptp.nth_co1649820636t_unit (-> tptp.list_c1059388851t_unit tptp.nat tptp.config256849571t_unit)) % 0.40/0.89 (declare-const tptp.index tptp.nat) % 0.40/0.89 (declare-const tptp.one_one_nat tptp.nat) % 0.40/0.89 (declare-const tptp.size_s1406904903t_unit (-> tptp.list_c1059388851t_unit tptp.nat)) % 0.40/0.89 (declare-const tptp.n1 tptp.nat) % 0.40/0.89 (declare-const tptp.nil_co1338500125t_unit tptp.list_c1059388851t_unit) % 0.40/0.89 (declare-const tptp.suc (-> tptp.nat tptp.nat)) % 0.40/0.89 (declare-const tptp.ft (-> tptp.nat tptp.list_message_p_v)) % 0.40/0.89 (declare-const tptp.minus_minus_nat (-> tptp.nat tptp.nat tptp.nat)) % 0.40/0.89 (declare-const tptp.msgInSet tptp.message_p_v) % 0.40/0.89 (declare-const tptp.zero_zero_nat tptp.nat) % 0.40/0.89 (define tptp.ord_less_nat () (let ((_let_1 (@var "N3" 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.40/0.89 (define @t1 () (_ tptp.fe tptp.index)) % 0.40/0.89 (define @t2 () (_ tptp.size_s1406904903t_unit @t1)) % 0.40/0.89 (define @t3 () (_ tptp.ord_less_nat tptp.n1)) % 0.40/0.89 (define @t4 () (@var "I" tptp.nat)) % 0.40/0.89 (define @t5 () (_ tptp.suc tptp.index)) % 0.40/0.89 (define @t6 () (_ tptp.fe @t5)) % 0.40/0.89 (define @t7 () (_ tptp.nth_co1649820636t_unit @t6)) % 0.40/0.89 (define @t8 () (_ @t7 @t4)) % 0.40/0.89 (define @t9 () (_ tptp.nth_co1649820636t_unit @t1)) % 0.40/0.89 (define @t10 () (_ @t9 @t4)) % 0.40/0.89 (define @t11 () (= @t10 @t8)) % 0.40/0.89 (define @t12 () (_ tptp.ord_less_nat @t4)) % 0.40/0.89 (define @t13 () (=> (_ @t12 @t2) @t11)) % 0.40/0.89 (define @t14 () (@list @t4)) % 0.40/0.89 (define @t15 () (forall @t14 @t13)) % 0.40/0.89 (define @t16 () (_ @t7 tptp.n1)) % 0.40/0.89 (define @t17 () (_ @t9 tptp.n1)) % 0.40/0.89 (define @t18 () (_ tptp.minus_minus_nat @t2)) % 0.40/0.89 (define @t19 () (_ @t18 tptp.one_one_nat)) % 0.40/0.89 (define @t20 () (_ tptp.size_s1406904903t_unit @t6)) % 0.40/0.89 (define @t21 () (_ tptp.ord_less_nat tptp.zero_zero_nat)) % 0.40/0.89 (define @t22 () (@var "N" tptp.nat)) % 0.40/0.89 (define @t23 () (_ tptp.suc @t22)) % 0.40/0.89 (define @t24 () (@list @t22)) % 0.40/0.89 (define @t25 () (@var "M" tptp.nat)) % 0.40/0.89 (define @t26 () (_ tptp.minus_minus_nat @t25)) % 0.40/0.89 (define @t27 () (_ @t26 @t22)) % 0.40/0.89 (define @t28 () (_ tptp.suc @t25)) % 0.40/0.89 (define @t29 () (_ tptp.minus_minus_nat @t28)) % 0.40/0.89 (define @t30 () (@list @t25 @t22)) % 0.40/0.89 (define @t31 () (@var "K" tptp.nat)) % 0.40/0.89 (define @t32 () (_ @t29 @t22)) % 0.40/0.89 (define @t33 () (_ tptp.suc @t4)) % 0.40/0.89 (define @t34 () (_ @t26 @t23)) % 0.40/0.89 (define @t35 () (_ tptp.minus_minus_nat tptp.n1)) % 0.40/0.89 (define @t36 () (_ @t35 tptp.one_one_nat)) % 0.40/0.89 (define @t37 () (_ @t9 @t36)) % 0.40/0.89 (define @t38 () (_ (_ tptp.minus_minus_nat @t20) tptp.one_one_nat)) % 0.40/0.89 (define @t39 () (_ tptp.ord_less_eq_nat @t19)) % 0.40/0.89 (define @t40 () (_ tptp.suc tptp.zero_zero_nat)) % 0.40/0.89 (define @t41 () (_ @t18 @t40)) % 0.40/0.89 (define @t42 () (_ @t35 @t40)) % 0.40/0.89 (define @t43 () (@var "A3" tptp.nat)) % 0.40/0.89 (define @t44 () (@var "A2" (-> tptp.list_c1059388851t_unit tptp.list_message_p_v tptp.list_message_p_v))) % 0.40/0.89 (define @t45 () (@var "A1" (-> tptp.list_c1059388851t_unit tptp.list_message_p_v tptp.list_c1059388851t_unit))) % 0.40/0.89 (define @t46 () (@var "A0" tptp.config256849571t_unit)) % 0.40/0.89 (define @t47 () (@var "P" (-> tptp.config256849571t_unit (-> tptp.list_c1059388851t_unit tptp.list_message_p_v tptp.list_c1059388851t_unit) (-> tptp.list_c1059388851t_unit tptp.list_message_p_v tptp.list_message_p_v) tptp.nat Bool))) % 0.40/0.89 (define @t48 () (@var "N2" tptp.nat)) % 0.40/0.89 (define @t49 () (_ tptp.suc @t48)) % 0.40/0.89 (define @t50 () (@var "FStepMsg" (-> tptp.list_c1059388851t_unit tptp.list_message_p_v tptp.list_message_p_v))) % 0.40/0.89 (define @t51 () (@var "FStepCfg" (-> tptp.list_c1059388851t_unit tptp.list_message_p_v tptp.list_c1059388851t_unit))) % 0.40/0.89 (define @t52 () (@var "Cfg" tptp.config256849571t_unit)) % 0.40/0.89 (define @t53 () (@var "Q" (-> tptp.config256849571t_unit (-> tptp.list_c1059388851t_unit tptp.list_message_p_v tptp.list_c1059388851t_unit) (-> tptp.list_c1059388851t_unit tptp.list_message_p_v tptp.list_message_p_v) tptp.nat Bool))) % 0.40/0.89 (define @t54 () (_ (_ (_ @t53 @t52) @t51) @t50)) % 0.40/0.89 (define @t55 () (_ @t54 @t48)) % 0.40/0.89 (define @t56 () (_ (_ (_ @t47 @t52) @t51) @t50)) % 0.40/0.89 (define @t57 () (_ @t56 @t48)) % 0.40/0.89 (define @t58 () (@list @t52 @t51 @t50 @t48)) % 0.40/0.89 (define @t59 () (forall @t58 (=> @t57 (=> @t55 (_ @t54 @t49))))) % 0.40/0.89 (define @t60 () (@list @t52 @t51 @t50)) % 0.40/0.89 (define @t61 () (forall @t60 (_ @t54 tptp.zero_zero_nat))) % 0.40/0.89 (define @t62 () (forall @t58 (=> @t57 (=> @t55 (_ @t56 @t49))))) % 0.40/0.89 (define @t63 () (forall @t60 (_ @t56 tptp.zero_zero_nat))) % 0.40/0.89 (define @t64 () (@var "A7" tptp.nat)) % 0.40/0.89 (define @t65 () (@var "A6" (-> tptp.list_c1059388851t_unit tptp.list_message_p_v tptp.list_message_p_v))) % 0.40/0.89 (define @t66 () (@var "A5" (-> tptp.list_c1059388851t_unit tptp.list_message_p_v tptp.list_c1059388851t_unit))) % 0.40/0.89 (define @t67 () (@var "A4" tptp.config256849571t_unit)) % 0.40/0.89 (define @t68 () (@var "Nat2" tptp.nat)) % 0.40/0.89 (define @t69 () (@var "Nat" tptp.nat)) % 0.40/0.89 (define @t70 () (_ tptp.suc @t68)) % 0.40/0.89 (define @t71 () (@var "Y2" tptp.nat)) % 0.40/0.89 (define @t72 () (@var "X2" tptp.nat)) % 0.40/0.89 (define @t73 () (_ tptp.suc @t72)) % 0.40/0.89 (define @t74 () (_ tptp.ord_less_eq_nat tptp.n1)) % 0.40/0.89 (define @t75 () (_ tptp.ord_less_nat @t25)) % 0.40/0.89 (define @t76 () (_ @t75 @t22)) % 0.40/0.89 (define @t77 () (_ tptp.ord_less_nat @t28)) % 0.40/0.89 (define @t78 () (_ @t77 @t23)) % 0.40/0.89 (define @t79 () (_ tptp.ord_less_nat @t22)) % 0.40/0.89 (define @t80 () (_ @t21 @t22)) % 0.40/0.89 (define @t81 () (= @t22 tptp.zero_zero_nat)) % 0.40/0.89 (define @t82 () (not @t81)) % 0.40/0.89 (define @t83 () (@var "A" tptp.nat)) % 0.40/0.89 (define @t84 () (= @t83 tptp.zero_zero_nat)) % 0.40/0.89 (define @t85 () (@list @t83)) % 0.40/0.89 (define @t86 () (_ tptp.ord_less_eq_nat @t22)) % 0.40/0.89 (define @t87 () (_ @t86 @t25)) % 0.40/0.89 (define @t88 () (_ tptp.ord_less_eq_nat @t23)) % 0.40/0.89 (define @t89 () (@list @t22 @t25)) % 0.40/0.89 (define @t90 () (_ tptp.ord_less_eq_nat tptp.zero_zero_nat)) % 0.40/0.89 (define @t91 () (@list @t25)) % 0.40/0.89 (define @t92 () (_ tptp.minus_minus_nat tptp.zero_zero_nat)) % 0.40/0.89 (define @t93 () (@var "I2" tptp.nat)) % 0.40/0.89 (define @t94 () (_ tptp.minus_minus_nat @t22)) % 0.40/0.89 (define @t95 () (_ tptp.ord_less_eq_nat @t93)) % 0.40/0.89 (define @t96 () (_ @t94 @t25)) % 0.40/0.89 (define @t97 () (_ tptp.ord_less_eq_nat @t25)) % 0.40/0.89 (define @t98 () (_ @t97 @t22)) % 0.40/0.89 (define @t99 () (= @t27 tptp.zero_zero_nat)) % 0.40/0.89 (define @t100 () (_ @t94 tptp.one_one_nat)) % 0.40/0.89 (define @t101 () (_ tptp.suc @t100)) % 0.40/0.89 (define @t102 () (_ @t95 @t31)) % 0.40/0.89 (define @t103 () (@var "J" tptp.nat)) % 0.40/0.89 (define @t104 () (_ (_ tptp.ord_less_eq_nat @t103) @t31)) % 0.40/0.89 (define @t105 () (=> @t104 @t102)) % 0.40/0.89 (define @t106 () (_ @t95 @t103)) % 0.40/0.89 (define @t107 () (@list @t93 @t103 @t31)) % 0.40/0.89 (define @t108 () (forall @t107 (=> @t106 @t105))) % 0.40/0.89 (define @t109 () (= @t25 @t22)) % 0.40/0.89 (define @t110 () (=> @t87 @t109)) % 0.40/0.89 (define @t111 () (=> @t98 @t110)) % 0.40/0.89 (define @t112 () (forall @t30 @t111)) % 0.40/0.89 (define @t113 () (_ @t79 @t25)) % 0.40/0.89 (define @t114 () (not @t109)) % 0.40/0.89 (define @t115 () (@var "T" tptp.nat)) % 0.40/0.89 (define @t116 () (@var "S" tptp.nat)) % 0.40/0.89 (define @t117 () (@var "K2" tptp.nat)) % 0.40/0.89 (define @t118 () (@var "P" (-> tptp.nat Bool))) % 0.40/0.89 (define @t119 () (not (_ @t118 @t4))) % 0.40/0.89 (define @t120 () (@list @t117)) % 0.40/0.89 (define @t121 () (_ @t118 tptp.zero_zero_nat)) % 0.40/0.89 (define @t122 () (not @t121)) % 0.40/0.89 (define @t123 () (_ @t118 @t22)) % 0.40/0.89 (define @t124 () (@list @t118 @t22)) % 0.40/0.89 (define @t125 () (_ @t118 @t48)) % 0.40/0.89 (define @t126 () (@var "M3" tptp.nat)) % 0.40/0.89 (define @t127 () (_ @t118 @t126)) % 0.40/0.89 (define @t128 () (_ (_ tptp.ord_less_nat @t126) @t48)) % 0.40/0.89 (define @t129 () (@list @t126)) % 0.40/0.89 (define @t130 () (@list @t48)) % 0.40/0.89 (define @t131 () (=> (not @t125) (exists @t129 (and @t128 (not @t127))))) % 0.40/0.89 (define @t132 () (@var "N3" tptp.nat)) % 0.40/0.89 (define @t133 () (@var "M2" tptp.nat)) % 0.40/0.89 (define @t134 () (= @t133 @t132)) % 0.40/0.89 (define @t135 () (@list @t133 @t132)) % 0.40/0.89 (define @t136 () (_ tptp.ord_less_eq_nat @t4)) % 0.40/0.89 (define @t137 () (_ @t21 @t48)) % 0.40/0.89 (define @t138 () (or @t76 @t109)) % 0.40/0.89 (define @t139 () (@var "X" tptp.nat)) % 0.40/0.89 (define @t140 () (@var "Y" tptp.nat)) % 0.40/0.89 (define @t141 () (= @t139 @t140)) % 0.40/0.89 (define @t142 () (@list @t139 @t140)) % 0.40/0.89 (define @t143 () (@var "X3" tptp.nat)) % 0.40/0.89 (define @t144 () (@var "Y4" tptp.nat)) % 0.40/0.89 (define @t145 () (@list @t143)) % 0.40/0.89 (define @t146 () (@var "B" tptp.nat)) % 0.40/0.89 (define @t147 () (@var "Y3" tptp.nat)) % 0.40/0.89 (define @t148 () (@list @t147)) % 0.40/0.89 (define @t149 () (_ @t118 @t31)) % 0.40/0.89 (define @t150 () (@var "F" (-> tptp.nat tptp.nat))) % 0.40/0.89 (define @t151 () (@var "J2" tptp.nat)) % 0.40/0.89 (define @t152 () (@var "I3" tptp.nat)) % 0.40/0.89 (define @t153 () (_ tptp.ord_less_nat @t152)) % 0.40/0.89 (define @t154 () (_ @t153 @t151)) % 0.40/0.89 (define @t155 () (@var "Y" tptp.list_c1059388851t_unit)) % 0.40/0.89 (define @t156 () (@var "X" tptp.list_c1059388851t_unit)) % 0.40/0.89 (define @t157 () (@var "Y" tptp.list_message_p_v)) % 0.40/0.89 (define @t158 () (@var "X" tptp.list_message_p_v)) % 0.40/0.89 (define @t159 () (_ tptp.ord_less_nat @t83)) % 0.40/0.89 (define @t160 () (_ tptp.ord_less_eq_nat @t83)) % 0.40/0.89 (define @t161 () (_ @t160 tptp.zero_zero_nat)) % 0.40/0.89 (define @t162 () (@var "N4" tptp.nat)) % 0.40/0.89 (define @t163 () (_ @t150 @t162)) % 0.40/0.89 (define @t164 () (_ @t150 @t22)) % 0.40/0.89 (define @t165 () (_ @t86 @t162)) % 0.40/0.89 (define @t166 () (_ @t150 @t49)) % 0.40/0.89 (define @t167 () (_ @t150 @t48)) % 0.40/0.89 (define @t168 () (@list @t150 @t22 @t162)) % 0.40/0.89 (define @t169 () (_ @t75 @t23)) % 0.40/0.89 (define @t170 () (@var "__flatten_var_0" tptp.nat)) % 0.40/0.89 (define @t171 () (= @t22 @t25)) % 0.40/0.89 (define @t172 () (_ @t79 @t28)) % 0.40/0.89 (define @t173 () (= @t172 @t171)) % 0.40/0.89 (define @t174 () (_ (_ tptp.ord_less_eq_nat @t28) @t22)) % 0.40/0.89 (define @t175 () (_ @t118 @t93)) % 0.40/0.89 (define @t176 () (_ @t118 @t49)) % 0.40/0.89 (define @t177 () (=> @t176 @t125)) % 0.40/0.89 (define @t178 () (_ tptp.ord_less_nat @t48)) % 0.40/0.89 (define @t179 () (_ @t178 @t103)) % 0.40/0.89 (define @t180 () (_ @t95 @t48)) % 0.40/0.89 (define @t181 () (_ @t118 @t103)) % 0.40/0.89 (define @t182 () (@list @t93 @t103 @t118)) % 0.40/0.89 (define @t183 () (=> @t125 @t176)) % 0.40/0.89 (define @t184 () (@var "C" tptp.nat)) % 0.40/0.89 (define @t185 () (_ tptp.minus_minus_nat @t83)) % 0.40/0.89 (define @t186 () (_ @t185 @t184)) % 0.40/0.89 (define @t187 () (_ @t94 @t31)) % 0.40/0.89 (define @t188 () (_ @t26 @t31)) % 0.40/0.89 (define @t189 () (_ tptp.ord_less_eq_nat @t31)) % 0.40/0.89 (define @t190 () (_ @t189 @t22)) % 0.40/0.89 (define @t191 () (_ @t189 @t25)) % 0.40/0.89 (define @t192 () (@list @t31 @t25 @t22)) % 0.40/0.89 (define @t193 () (@var "J3" tptp.nat)) % 0.40/0.89 (define @t194 () (@var "M4" tptp.nat)) % 0.40/0.89 (define @t195 () (_ tptp.suc @t194)) % 0.40/0.89 (define @t196 () (@list @t194)) % 0.40/0.89 (define @t197 () (exists @t196 (= @t22 @t195))) % 0.40/0.89 (define @t198 () (@var "I4" tptp.nat)) % 0.40/0.89 (define @t199 () (_ @t118 (_ tptp.suc @t198))) % 0.40/0.89 (define @t200 () (_ tptp.ord_less_nat @t198)) % 0.40/0.89 (define @t201 () (_ @t200 @t22)) % 0.40/0.89 (define @t202 () (@list @t198)) % 0.40/0.89 (define @t203 () (_ @t118 @t198)) % 0.40/0.89 (define @t204 () (_ @t200 @t23)) % 0.40/0.89 (define @t205 () (forall @t202 (=> @t204 @t203))) % 0.40/0.89 (define @t206 () (@list @t22 @t118)) % 0.40/0.89 (define @t207 () (exists @t202 (and @t204 @t203))) % 0.40/0.89 (define @t208 () (_ tptp.ord_less_nat @t27)) % 0.40/0.89 (define @t209 () (@var "R" (-> tptp.nat tptp.nat Bool))) % 0.40/0.89 (define @t210 () (@var "Z" tptp.nat)) % 0.40/0.89 (define @t211 () (_ @t209 @t143)) % 0.40/0.89 (define @t212 () (not @t98)) % 0.40/0.89 (define @t213 () (= @t25 @t23)) % 0.40/0.89 (define @t214 () (_ @t97 @t23)) % 0.40/0.89 (define @t215 () (@var "M5" tptp.nat)) % 0.40/0.89 (define @t216 () (@var "L" tptp.nat)) % 0.40/0.89 (define @t217 () (_ tptp.minus_minus_nat @t216)) % 0.40/0.89 (define @t218 () (_ @t217 @t25)) % 0.40/0.89 (define @t219 () (_ @t217 @t22)) % 0.40/0.89 (define @t220 () (@list @t25 @t22 @t216)) % 0.40/0.89 (define @t221 () (_ tptp.ord_less_eq_nat @t146)) % 0.40/0.89 (define @t222 () (_ tptp.minus_minus_nat @t184)) % 0.40/0.89 (define @t223 () (@list @t83 @t184 @t146)) % 0.40/0.89 (define @t224 () (@var "Nat3" tptp.nat)) % 0.40/0.89 (define @t225 () (_ tptp.suc @t224)) % 0.40/0.89 (define @t226 () (@list @t224)) % 0.40/0.89 (define @t227 () (forall @t130 @t177)) % 0.40/0.89 (define @t228 () (@var "P" (-> tptp.nat tptp.nat Bool))) % 0.40/0.89 (define @t229 () (_ tptp.suc @t147)) % 0.40/0.89 (define @t230 () (_ @t228 @t143)) % 0.40/0.89 (define @t231 () (@list @t68)) % 0.40/0.89 (define @t232 () (_ tptp.ord_less_nat @t164)) % 0.40/0.89 (define @t233 () (forall @t130 (_ (_ tptp.ord_less_nat @t167) @t166))) % 0.40/0.89 (define @t234 () (_ tptp.suc @t93)) % 0.40/0.89 (define @t235 () (not @t113)) % 0.40/0.89 (define @t236 () (_ @t118 @t152)) % 0.40/0.89 (define @t237 () (_ tptp.suc @t152)) % 0.40/0.89 (define @t238 () (_ @t118 @t237)) % 0.40/0.89 (define @t239 () (@list @t152)) % 0.40/0.89 (define @t240 () (_ tptp.ord_less_nat @t93)) % 0.40/0.89 (define @t241 () (_ @t240 @t103)) % 0.40/0.89 (define @t242 () (_ @t228 @t152)) % 0.40/0.89 (define @t243 () (_ (_ tptp.ord_less_nat @t234) @t31)) % 0.40/0.89 (define @t244 () (_ (_ tptp.ord_less_nat @t103) @t31)) % 0.40/0.89 (define @t245 () (@var "M6" tptp.nat)) % 0.40/0.89 (define @t246 () (not @t76)) % 0.40/0.89 (define @t247 () (_ @t77 @t22)) % 0.40/0.89 (define @t248 () (not (forall (@list @t151) (=> (_ @t240 @t151) (not (= @t31 (_ tptp.suc @t151))))))) % 0.40/0.89 (define @t249 () (@list @t93 @t31)) % 0.40/0.89 (define @t250 () (_ tptp.minus_minus_nat @t93)) % 0.40/0.89 (define @t251 () (@var "Xs" tptp.list_c1059388851t_unit)) % 0.40/0.89 (define @t252 () (= @t251 tptp.nil_co1338500125t_unit)) % 0.40/0.89 (define @t253 () (not @t252)) % 0.40/0.89 (define @t254 () (_ tptp.size_s1406904903t_unit @t251)) % 0.40/0.89 (define @t255 () (@list @t251)) % 0.40/0.89 (define @t256 () (@var "Xs" tptp.list_message_p_v)) % 0.40/0.89 (define @t257 () (= @t256 tptp.nil_message_p_v)) % 0.40/0.89 (define @t258 () (not @t257)) % 0.40/0.89 (define @t259 () (_ tptp.size_s1168481041ge_p_v @t256)) % 0.40/0.89 (define @t260 () (@list @t256)) % 0.40/0.89 (define @t261 () (_ tptp.last_c571238084t_unit @t1)) % 0.40/0.89 (define @t262 () (_ tptp.enabled_p_v_s @t261)) % 0.40/0.89 (define @t263 () (_ tptp.enabled_p_v_s (_ tptp.last_c571238084t_unit @t6))) % 0.40/0.89 (define @t264 () (_ tptp.fe tptp.n)) % 0.40/0.89 (define @t265 () (@list @t139)) % 0.40/0.89 (define @t266 () (@var "Ys" tptp.list_c1059388851t_unit)) % 0.40/0.89 (define @t267 () (= @t251 @t266)) % 0.40/0.89 (define @t268 () (= @t254 (_ tptp.size_s1406904903t_unit @t266))) % 0.40/0.89 (define @t269 () (@list @t251 @t266)) % 0.40/0.89 (define @t270 () (@var "Ys" tptp.list_message_p_v)) % 0.40/0.89 (define @t271 () (= @t256 @t270)) % 0.40/0.89 (define @t272 () (= @t259 (_ tptp.size_s1168481041ge_p_v @t270))) % 0.40/0.89 (define @t273 () (@list @t256 @t270)) % 0.40/0.89 (define @t274 () (@var "Xs2" tptp.list_c1059388851t_unit)) % 0.40/0.89 (define @t275 () (_ tptp.size_s1406904903t_unit @t274)) % 0.40/0.89 (define @t276 () (@list @t274)) % 0.40/0.89 (define @t277 () (@var "Xs2" tptp.list_message_p_v)) % 0.40/0.89 (define @t278 () (_ tptp.size_s1168481041ge_p_v @t277)) % 0.40/0.89 (define @t279 () (@list @t277)) % 0.40/0.89 (define @t280 () (_ tptp.nth_co1649820636t_unit @t251)) % 0.40/0.89 (define @t281 () (_ tptp.nth_message_p_v @t256)) % 0.40/0.89 (define @t282 () (@var "P" (-> tptp.list_c1059388851t_unit Bool))) % 0.40/0.89 (define @t283 () (@var "Ys2" tptp.list_c1059388851t_unit)) % 0.40/0.89 (define @t284 () (@var "P" (-> tptp.list_message_p_v Bool))) % 0.40/0.89 (define @t285 () (@var "Ys2" tptp.list_message_p_v)) % 0.40/0.89 (define @t286 () (_ tptp.size_s1406904903t_unit tptp.nil_co1338500125t_unit)) % 0.40/0.89 (define @t287 () (@var "Xs3" tptp.list_c1059388851t_unit)) % 0.40/0.89 (define @t288 () (_ (_ tptp.nth_co1649820636t_unit @t287) @t198)) % 0.40/0.89 (define @t289 () (@var "P" (-> tptp.nat tptp.config256849571t_unit Bool))) % 0.40/0.89 (define @t290 () (_ @t289 @t198)) % 0.40/0.89 (define @t291 () (_ @t200 @t31)) % 0.40/0.89 (define @t292 () (_ tptp.size_s1406904903t_unit @t287)) % 0.40/0.89 (define @t293 () (@var "X4" tptp.config256849571t_unit)) % 0.40/0.89 (define @t294 () (@var "Xs3" tptp.list_message_p_v)) % 0.40/0.89 (define @t295 () (_ (_ tptp.nth_message_p_v @t294) @t198)) % 0.40/0.89 (define @t296 () (@var "P" (-> tptp.nat tptp.message_p_v Bool))) % 0.40/0.89 (define @t297 () (_ @t296 @t198)) % 0.40/0.89 (define @t298 () (_ tptp.size_s1168481041ge_p_v @t294)) % 0.40/0.89 (define @t299 () (@var "X4" tptp.message_p_v)) % 0.40/0.89 (define @t300 () (@var "Ys3" tptp.list_c1059388851t_unit)) % 0.40/0.89 (define @t301 () (@var "Z2" tptp.list_c1059388851t_unit)) % 0.40/0.89 (define @t302 () (@var "Y5" tptp.list_c1059388851t_unit)) % 0.40/0.89 (define @t303 () (@var "Ys3" tptp.list_message_p_v)) % 0.40/0.89 (define @t304 () (@var "Z2" tptp.list_message_p_v)) % 0.40/0.89 (define @t305 () (@var "Y5" tptp.list_message_p_v)) % 0.40/0.89 (define @t306 () (@var "Index" tptp.nat)) % 0.40/0.89 (define @t307 () (@var "L2" tptp.list_c1059388851t_unit)) % 0.40/0.89 (define @t308 () (@var "L1" tptp.list_c1059388851t_unit)) % 0.40/0.89 (define @t309 () (_ tptp.size_s1406904903t_unit @t308)) % 0.40/0.89 (define @t310 () (_ tptp.ord_less_nat @t306)) % 0.40/0.89 (define @t311 () (@list @t306)) % 0.40/0.89 (define @t312 () (_ tptp.prefix1615116500t_unit @t308)) % 0.40/0.89 (define @t313 () (_ @t312 @t307)) % 0.40/0.89 (define @t314 () (@list @t308 @t307)) % 0.40/0.89 (define @t315 () (@var "L2" tptp.list_message_p_v)) % 0.40/0.89 (define @t316 () (@var "L1" tptp.list_message_p_v)) % 0.40/0.89 (define @t317 () (_ tptp.size_s1168481041ge_p_v @t316)) % 0.40/0.89 (define @t318 () (_ tptp.prefix47729710ge_p_v @t316)) % 0.40/0.89 (define @t319 () (_ @t318 @t315)) % 0.40/0.89 (define @t320 () (@list @t316 @t315)) % 0.40/0.89 (define @t321 () (@var "FStepMsg2" (-> tptp.list_c1059388851t_unit tptp.list_message_p_v tptp.list_message_p_v))) % 0.40/0.89 (define @t322 () (@var "FStepCfg2" (-> tptp.list_c1059388851t_unit tptp.list_message_p_v tptp.list_c1059388851t_unit))) % 0.40/0.89 (define @t323 () (@var "Cfg2" tptp.config256849571t_unit)) % 0.40/0.89 (define @t324 () (_ (_ (_ tptp.fLPThe536531371_p_v_s @t323) @t322) @t321)) % 0.40/0.89 (define @t325 () (@var "N5" tptp.nat)) % 0.40/0.89 (define @t326 () (@var "N0" tptp.nat)) % 0.40/0.89 (define @t327 () (@list @t325)) % 0.40/0.89 (define @t328 () (_ @t118 @t326)) % 0.40/0.89 (define @t329 () (@list @t326)) % 0.40/0.89 (define @t330 () (@var "X_1" tptp.nat)) % 0.40/0.89 (define @t331 () (exists (@list @t330) (_ @t118 @t330))) % 0.40/0.89 (define @t332 () (@list @t118)) % 0.40/0.89 (define @t333 () (@var "L3" tptp.list_c1059388851t_unit)) % 0.40/0.89 (define @t334 () (@var "L3" tptp.list_message_p_v)) % 0.40/0.89 (define @t335 () (@var "Q" (-> tptp.nat Bool))) % 0.40/0.89 (define @t336 () (@var "Low" tptp.nat)) % 0.40/0.89 (define @t337 () (_ tptp.ord_less_eq_nat @t336)) % 0.40/0.89 (define @t338 () (@var "Pr" (-> tptp.nat Bool))) % 0.40/0.89 (define @t339 () (@var "N22" tptp.nat)) % 0.40/0.89 (define @t340 () (@var "Xb" (-> tptp.list_c1059388851t_unit tptp.list_message_p_v tptp.list_message_p_v))) % 0.40/0.89 (define @t341 () (@var "Xa" (-> tptp.list_c1059388851t_unit tptp.list_message_p_v tptp.list_c1059388851t_unit))) % 0.40/0.89 (define @t342 () (@var "X" tptp.config256849571t_unit)) % 0.40/0.89 (define @t343 () (_ (_ (_ tptp.fLPThe536531371_p_v_s @t342) @t341) @t340)) % 0.40/0.89 (define @t344 () (@var "Xc" tptp.nat)) % 0.40/0.89 (define @t345 () (_ @t324 @t22)) % 0.40/0.89 (define @t346 () (_ (_ (_ tptp.fLPThe1519354920_p_v_s @t323) @t322) @t321)) % 0.40/0.89 (define @t347 () (_ @t346 @t22)) % 0.40/0.89 (define @t348 () (@list @t323 @t322 @t321 @t22)) % 0.40/0.89 (define @t349 () (_ tptp.ft tptp.index)) % 0.40/0.89 (define @t350 () (_ tptp.nth_message_p_v @t349)) % 0.40/0.89 (define @t351 () (@var "N02" tptp.nat)) % 0.40/0.89 (define @t352 () (_ tptp.ft @t325)) % 0.40/0.89 (define @t353 () (_ tptp.ft tptp.n)) % 0.40/0.89 (define @t354 () (_ tptp.size_s1168481041ge_p_v @t353)) % 0.40/0.89 (define @t355 () (_ tptp.ord_less_nat @t351)) % 0.40/0.89 (define @t356 () (@list @t351)) % 0.40/0.89 (define @t357 () (_ tptp.ord_less_eq_nat tptp.n)) % 0.40/0.89 (define @t358 () (_ tptp.ft @t5)) % 0.40/0.89 (define @t359 () (_ tptp.size_s1168481041ge_p_v @t358)) % 0.40/0.89 (define @t360 () (_ tptp.size_s1168481041ge_p_v @t349)) % 0.40/0.89 (define @t361 () (_ tptp.nth_message_p_v @t358)) % 0.40/0.89 (define @t362 () (_ @t361 @t4)) % 0.40/0.89 (define @t363 () (_ (_ tptp.ord_less_eq_nat @t360) @t4)) % 0.40/0.89 (define @t364 () (_ @t12 @t359)) % 0.40/0.89 (define @t365 () (_ @t361 @t325)) % 0.40/0.89 (define @t366 () (_ @t350 @t325)) % 0.40/0.89 (define @t367 () (_ tptp.ord_less_nat @t325)) % 0.40/0.89 (define @t368 () (_ @t367 @t360)) % 0.40/0.89 (define @t369 () (_ @t74 @t325)) % 0.40/0.89 (define @t370 () (_ (_ tptp.firstO1414030372_p_v_s @t6) @t358)) % 0.40/0.89 (define @t371 () (@var "Msg" tptp.message_p_v)) % 0.40/0.89 (define @t372 () (@var "N03" tptp.nat)) % 0.40/0.89 (define @t373 () (_ tptp.ft @t22)) % 0.40/0.89 (define @t374 () (_ tptp.ord_less_nat @t372)) % 0.40/0.89 (define @t375 () (@var "N1" tptp.nat)) % 0.40/0.89 (define @t376 () (_ tptp.ord_less_eq_nat @t375)) % 0.40/0.89 (define @t377 () (@list @t372)) % 0.40/0.89 (define @t378 () (_ tptp.fe @t22)) % 0.40/0.89 (define @t379 () (_ tptp.nth_co1649820636t_unit @t378)) % 0.40/0.89 (define @t380 () (@var "N6" tptp.nat)) % 0.40/0.89 (define @t381 () (_ tptp.ft @t380)) % 0.40/0.89 (define @t382 () (_ tptp.ord_less_eq_nat tptp.n0)) % 0.40/0.89 (define @t383 () (_ @t367 @t359)) % 0.40/0.89 (define @t384 () (_ @t7 @t36)) % 0.40/0.89 (define @t385 () (not (= @t384 @t37))) % 0.40/0.89 (define @t386 () (lambda @t135 (and (_ (_ tptp.ord_less_eq_nat @t133) @t132) (not @t134)))) % 0.40/0.89 (define @t387 () (tptp.ord_less_eq_nat @t22 @t25)) % 0.40/0.89 (define @t388 () (not @t87)) % 0.40/0.89 (define @t389 () (tptp.ord_less_eq_nat @t25 @t22)) % 0.40/0.89 (define @t390 () (or @t212 @t388 @t171)) % 0.40/0.89 (define @t391 () (=> @t87 @t171)) % 0.40/0.89 (define @t392 () (tptp.size_s1406904903t_unit tptp.nil_co1338500125t_unit)) % 0.40/0.89 (define @t393 () (tptp.suc @t392)) % 0.40/0.89 (define @t394 () (tptp.fe tptp.index)) % 0.40/0.89 (define @t395 () (tptp.size_s1406904903t_unit @t394)) % 0.40/0.89 (define @t396 () (tptp.minus_minus_nat @t395 @t393)) % 0.40/0.89 (define @t397 () (tptp.minus_minus_nat tptp.n1 @t393)) % 0.40/0.89 (define @t398 () (_ tptp.suc @t286)) % 0.40/0.89 (define @t399 () (_ @t18 @t398)) % 0.40/0.89 (define @t400 () (_ @t35 @t398)) % 0.40/0.89 (define @t401 () (= @t400 @t399)) % 0.40/0.89 (define @t402 () (not @t401)) % 0.40/0.89 (define @t403 () (tptp.ord_less_eq_nat @t397 @t396)) % 0.40/0.89 (define @t404 () (_ (_ tptp.ord_less_eq_nat @t400) @t399)) % 0.40/0.89 (define @t405 () (= @t42 @t41)) % 0.40/0.89 (define @t406 () (not @t405)) % 0.40/0.89 (define @t407 () (_ tptp.ord_less_eq_nat @t42)) % 0.40/0.89 (define @t408 () (and (_ @t407 @t41) @t406)) % 0.40/0.89 (define @t409 () (@list @t132)) % 0.40/0.89 (define @t410 () (lambda @t409 (and (_ @t407 @t132) (not (= @t42 @t132))))) % 0.40/0.89 (define @t411 () (= @t396 @t397)) % 0.40/0.89 (define @t412 () (not (tptp.ord_less_eq_nat @t396 @t397))) % 0.40/0.89 (define @t413 () (not @t403)) % 0.40/0.89 (define @t414 () (or @t413 @t412 @t411)) % 0.40/0.89 (define @t415 () (@list true false false)) % 0.40/0.89 (define @t416 () (tptp.suc tptp.index)) % 0.40/0.89 (define @t417 () (tptp.fe @t416)) % 0.40/0.89 (define @t418 () (tptp.nth_co1649820636t_unit @t417 @t4)) % 0.40/0.89 (define @t419 () (tptp.nth_co1649820636t_unit @t394 @t4)) % 0.40/0.89 (define @t420 () (= @t419 @t418)) % 0.40/0.89 (define @t421 () (tptp.ord_less_eq_nat @t4 @t395)) % 0.40/0.89 (define @t422 () (not @t421)) % 0.40/0.89 (define @t423 () (or @t422 (= @t395 @t4) @t420)) % 0.40/0.89 (define @t424 () (_ tptp.nth_co1649820636t_unit @t417)) % 0.40/0.89 (define @t425 () (_ tptp.nth_co1649820636t_unit @t394)) % 0.40/0.89 (define @t426 () (= @t2 @t4)) % 0.40/0.89 (define @t427 () (_ @t136 @t2)) % 0.40/0.89 (define @t428 () (not @t427)) % 0.40/0.89 (define @t429 () (or @t428 @t426 @t11)) % 0.40/0.89 (define @t430 () (not @t426)) % 0.40/0.89 (define @t431 () (and @t427 @t430)) % 0.40/0.89 (define @t432 () (not (= @t4 @t2))) % 0.40/0.89 (define @t433 () (and @t427 @t432)) % 0.40/0.89 (define @t434 () (lambda @t409 (and (_ @t136 @t132) (not (= @t4 @t132))))) % 0.40/0.89 (define @t435 () (_ @t386 @t4)) % 0.40/0.89 (define @t436 () (=> (_ @t435 @t2) @t11)) % 0.40/0.89 (define @t437 () (tptp.nth_co1649820636t_unit @t417 @t397)) % 0.40/0.89 (define @t438 () (tptp.nth_co1649820636t_unit @t394 @t397)) % 0.40/0.89 (define @t439 () (= @t438 @t437)) % 0.40/0.89 (define @t440 () (tptp.ord_less_eq_nat @t397 @t395)) % 0.40/0.89 (define @t441 () (not @t440)) % 0.40/0.89 (define @t442 () (or @t441 (= @t397 @t395) @t439)) % 0.40/0.89 (define @t443 () (forall @t14 (or @t422 (= @t4 @t395) @t420))) % 0.40/0.89 (define @t444 () (= @t395 @t397)) % 0.40/0.89 (define @t445 () (or @t441 @t444 @t439)) % 0.40/0.89 (define @t446 () (tptp.ord_less_eq_nat @t93 @t31)) % 0.40/0.89 (define @t447 () (tptp.ord_less_eq_nat @t103 @t31)) % 0.40/0.89 (define @t448 () (not @t104)) % 0.40/0.89 (define @t449 () (tptp.ord_less_eq_nat @t93 @t103)) % 0.40/0.89 (define @t450 () (not @t106)) % 0.40/0.89 (define @t451 () (or @t450 @t448 @t102)) % 0.40/0.89 (define @t452 () (= @t2 @t399)) % 0.40/0.89 (define @t453 () (not @t452)) % 0.40/0.89 (define @t454 () (tptp.ord_less_eq_nat @t396 @t395)) % 0.40/0.89 (define @t455 () (_ (_ tptp.ord_less_eq_nat @t399) @t2)) % 0.40/0.89 (define @t456 () (= @t2 @t19)) % 0.40/0.89 (define @t457 () (not @t456)) % 0.40/0.89 (define @t458 () (_ @t39 @t2)) % 0.40/0.89 (define @t459 () (not (= @t19 @t2))) % 0.40/0.89 (define @t460 () (and @t458 @t459)) % 0.40/0.89 (define @t461 () (lambda @t409 (and (_ @t39 @t132) (not (= @t19 @t132))))) % 0.40/0.89 (define @t462 () (not @t454)) % 0.40/0.89 (define @t463 () (or @t413 @t462 @t440)) % 0.40/0.89 (define @t464 () (_ @t9 @t400)) % 0.40/0.89 (define @t465 () (_ @t7 @t400)) % 0.40/0.89 (define @t466 () (= @t465 @t464)) % 0.40/0.89 (define @t467 () (= @t37 @t384)) % 0.40/0.89 (assume @p1 (_ @t3 @t2)) % 0.40/0.89 (assume @p2 @t15) % 0.40/0.89 (assume @p3 (= @t17 @t16)) % 0.40/0.89 (assume @p4 (_ (_ tptp.ord_less_nat @t19) @t2)) % 0.40/0.89 (assume @p5 (_ @t3 @t20)) % 0.40/0.89 (assume @p6 (_ @t21 tptp.n1)) % 0.40/0.89 (assume @p7 (forall @t24 (= (_ (_ tptp.minus_minus_nat @t23) tptp.one_one_nat) @t22))) % 0.40/0.89 (assume @p8 (forall @t30 (= (_ @t29 @t23) @t27))) % 0.40/0.89 (assume @p9 (forall (@list @t25 @t22 @t31) (= (_ (_ tptp.minus_minus_nat @t32) (_ tptp.suc @t31)) (_ (_ tptp.minus_minus_nat @t27) @t31)))) % 0.40/0.89 (assume @p10 (not (= @t6 tptp.nil_co1338500125t_unit))) % 0.40/0.89 (assume @p11 (forall @t14 (_ (_ tptp.prefix1615116500t_unit (_ tptp.fe @t4)) (_ tptp.fe @t33)))) % 0.40/0.89 (assume @p12 (forall @t30 (= @t34 (_ (_ tptp.minus_minus_nat (_ @t26 tptp.one_one_nat)) @t22)))) % 0.40/0.89 (assume @p13 (_ (_ tptp.enabled_p_v_s @t37) tptp.msgInSet)) % 0.40/0.89 (assume @p14 (_ @t39 @t38)) % 0.40/0.89 (assume @p15 (not (= @t1 tptp.nil_co1338500125t_unit))) % 0.40/0.89 (assume @p16 (_ (_ tptp.ord_less_nat @t42) @t41)) % 0.40/0.89 (assume @p17 (forall (@list @t47 @t53 @t46 @t45 @t44 @t43) (=> @t63 (=> @t62 (=> @t61 (=> @t59 (_ (_ (_ (_ @t47 @t46) @t45) @t44) @t43))))))) % 0.40/0.89 (assume @p18 (forall (@list @t47 @t53 @t67 @t66 @t65 @t64) (=> @t63 (=> @t62 (=> @t61 (=> @t59 (_ (_ (_ (_ @t53 @t67) @t66) @t65) @t64))))))) % 0.40/0.89 (assume @p19 (forall (@list @t69 @t68) (= (= (_ tptp.suc @t69) @t70) (= @t69 @t68)))) % 0.40/0.89 (assume @p20 (forall (@list @t72 @t71) (= (= @t73 (_ tptp.suc @t71)) (= @t72 @t71)))) % 0.40/0.89 (assume @p21 (_ @t74 tptp.nMsg)) % 0.40/0.89 (assume @p22 (_ @t21 @t2)) % 0.40/0.89 (assume @p23 (forall @t30 (= @t78 @t76))) % 0.40/0.89 (assume @p24 (forall @t30 (=> @t76 @t78))) % 0.40/0.89 (assume @p25 (forall @t24 (_ @t79 @t23))) % 0.40/0.89 (assume @p26 (forall @t24 (= @t82 @t80))) % 0.40/0.89 (assume @p27 (forall @t24 (not (_ @t79 tptp.zero_zero_nat)))) % 0.40/0.89 (assume @p28 (forall @t85 (= (not @t84) (_ @t21 @t83)))) % 0.40/0.89 (assume @p29 (forall @t89 (= (_ @t88 @t28) @t87))) % 0.40/0.89 (assume @p30 (forall @t24 (_ @t90 @t22))) % 0.40/0.89 (assume @p31 (forall @t85 (_ @t90 @t83))) % 0.40/0.89 (assume @p32 (forall @t91 (= (_ @t26 @t25) tptp.zero_zero_nat))) % 0.40/0.89 (assume @p33 (forall @t24 (= (_ @t92 @t22) tptp.zero_zero_nat))) % 0.40/0.89 (assume @p34 (forall (@list @t93 @t22) (=> (_ @t95 @t22) (= (_ @t94 (_ @t94 @t93)) @t93)))) % 0.40/0.89 (assume @p35 (_ (_ tptp.enabled_p_v_s @t17) tptp.msgInSet)) % 0.40/0.89 (assume @p36 (_ (_ tptp.enabled_p_v_s @t16) tptp.msgInSet)) % 0.40/0.89 (assume @p37 (_ (_ tptp.enabled_p_v_s (_ @t9 @t19)) tptp.msgInSet)) % 0.40/0.89 (assume @p38 (forall @t24 (_ @t21 @t23))) % 0.40/0.89 (assume @p39 (forall @t24 (= (_ @t79 @t40) @t81))) % 0.40/0.89 (assume @p40 (forall @t89 (= (_ @t21 @t96) @t76))) % 0.40/0.89 (assume @p41 (forall @t30 (= @t99 @t98))) % 0.40/0.89 (assume @p42 (forall @t30 (=> @t98 @t99))) % 0.40/0.89 (assume @p43 (forall @t24 (= (_ @t79 tptp.one_one_nat) @t81))) % 0.40/0.89 (assume @p44 (forall @t24 (=> @t80 (= (_ tptp.suc (_ @t94 @t40)) @t22)))) % 0.40/0.89 (assume @p45 (forall @t24 (=> @t80 (= @t101 @t22)))) % 0.40/0.89 (assume @p46 (forall @t24 (=> @t82 @t80))) % 0.40/0.89 (assume @p47 (forall @t24 (= (_ @t86 tptp.zero_zero_nat) @t81))) % 0.40/0.89 (assume @p48 (forall @t24 (_ @t86 @t22))) % 0.40/0.89 (assume @p49 (forall @t24 (= (not @t80) @t81))) % 0.40/0.89 (assume @p50 @t108) % 0.40/0.89 (assume @p51 (forall @t30 (=> @t109 @t98))) % 0.40/0.89 (assume @p52 @t112) % 0.40/0.89 (assume @p53 (forall @t30 (= @t114 (or @t76 @t113)))) % 0.40/0.89 (assume @p54 (forall @t24 (not (_ @t79 @t22)))) % 0.40/0.89 (assume @p55 (forall @t30 (or @t98 @t87))) % 0.40/0.89 (assume @p56 (forall @t89 (=> @t113 @t114))) % 0.40/0.89 (assume @p57 (forall (@list @t116 @t115) (=> (_ (_ tptp.ord_less_nat @t116) @t115) (not (= @t116 @t115))))) % 0.40/0.89 (assume @p58 (forall @t124 (=> @t123 (=> @t122 (exists @t120 (and (_ (_ tptp.ord_less_eq_nat @t117) @t22) (forall @t14 (=> (_ @t12 @t117) @t119)) (_ @t118 @t117))))))) % 0.40/0.89 (assume @p59 (forall @t30 (=> @t76 @t82))) % 0.40/0.89 (assume @p60 (forall @t30 (=> @t76 @t98))) % 0.40/0.89 (assume @p61 (forall @t124 (=> (forall @t130 (=> (forall @t129 (=> @t128 @t127)) @t125)) @t123))) % 0.40/0.89 (assume @p62 (forall @t124 (=> (forall @t130 @t131) @t123))) % 0.40/0.89 (assume @p63 (= tptp.ord_less_eq_nat (lambda @t135 (or (_ (_ tptp.ord_less_nat @t133) @t132) @t134)))) % 0.40/0.89 (assume @p64 (forall @t124 (=> @t123 (=> @t122 (exists @t120 (and (_ (_ tptp.ord_less_nat @t117) @t22) (forall @t14 (=> (_ @t136 @t117) @t119)) (_ @t118 (_ tptp.suc @t117)))))))) % 0.40/0.89 (assume @p65 (forall @t124 (=> @t121 (=> (forall @t130 (=> @t137 @t131)) @t123)))) % 0.40/0.89 (assume @p66 (forall @t30 (=> @t138 @t98))) % 0.40/0.89 (assume @p67 (forall @t142 (=> (not @t141) (=> (not (_ (_ tptp.ord_less_nat @t139) @t140)) (_ (_ tptp.ord_less_nat @t140) @t139))))) % 0.40/0.89 (assume @p68 (forall (@list @t118 @t31 @t146) (=> @t149 (=> (forall @t148 (=> (_ @t118 @t147) (_ (_ tptp.ord_less_eq_nat @t147) @t146))) (exists @t145 (and (_ @t118 @t143) (forall (@list @t144) (=> (_ @t118 @t144) (_ (_ tptp.ord_less_eq_nat @t144) @t143))))))))) % 0.40/0.89 (assume @p69 (forall @t30 (=> @t98 (=> @t114 @t76)))) % 0.40/0.89 (assume @p70 (forall (@list @t150 @t93 @t103) (=> (forall (@list @t152 @t151) (=> @t154 (_ (_ tptp.ord_less_nat (_ @t150 @t152)) (_ @t150 @t151)))) (=> @t106 (_ (_ tptp.ord_less_eq_nat (_ @t150 @t93)) (_ @t150 @t103)))))) % 0.40/0.89 (assume @p71 (forall (@list @t156 @t155) (=> (not (= (_ tptp.size_s1406904903t_unit @t156) (_ tptp.size_s1406904903t_unit @t155))) (not (= @t156 @t155))))) % 0.40/0.89 (assume @p72 (forall (@list @t158 @t157) (=> (not (= (_ tptp.size_s1168481041ge_p_v @t158) (_ tptp.size_s1168481041ge_p_v @t157))) (not (= @t158 @t157))))) % 0.40/0.89 (assume @p73 (forall @t85 (not (_ @t159 tptp.zero_zero_nat)))) % 0.40/0.89 (assume @p74 (forall @t85 (= @t161 @t84))) % 0.40/0.89 (assume @p75 (forall @t85 (=> @t161 @t84))) % 0.40/0.89 (assume @p76 (forall @t168 (=> (forall @t130 (_ (_ tptp.ord_less_eq_nat @t167) @t166)) (=> @t165 (_ (_ tptp.ord_less_eq_nat @t164) @t163))))) % 0.40/0.89 (assume @p77 (forall @t168 (=> (forall @t130 (_ (_ tptp.ord_less_eq_nat @t166) @t167)) (=> @t165 (_ (_ tptp.ord_less_eq_nat @t163) @t164))))) % 0.40/0.89 (assume @p78 (forall @t30 (=> @t98 @t169))) % 0.40/0.89 (assume @p79 (= tptp.ord_less_nat (lambda (@list @t132 @t170) (_ (_ tptp.ord_less_eq_nat (_ tptp.suc @t132)) @t170)))) % 0.40/0.89 (assume @p80 (forall @t30 (= @t169 @t98))) % 0.40/0.89 (assume @p81 (forall @t30 (=> @t98 @t173))) % 0.40/0.89 (assume @p82 (forall @t30 (=> @t174 @t76))) % 0.40/0.89 (assume @p83 (forall @t182 (=> @t106 (=> @t181 (=> (forall @t130 (=> @t180 (=> @t179 @t177))) @t175))))) % 0.40/0.89 (assume @p84 (forall @t182 (=> @t106 (=> @t175 (=> (forall @t130 (=> @t180 (=> @t179 @t183))) @t181))))) % 0.40/0.89 (assume @p85 (forall @t30 (= @t174 @t76))) % 0.40/0.89 (assume @p86 (forall @t30 (=> @t76 @t174))) % 0.40/0.89 (assume @p87 (forall (@list @t83 @t146 @t184) (=> (_ @t159 @t146) (=> (_ (_ tptp.ord_less_eq_nat @t184) @t83) (_ (_ tptp.ord_less_nat @t186) (_ (_ tptp.minus_minus_nat @t146) @t184)))))) % 0.40/0.89 (assume @p88 (forall @t192 (=> @t191 (=> @t190 (= (_ (_ tptp.ord_less_nat @t188) @t187) @t76))))) % 0.40/0.89 (assume @p89 (forall @t30 (= @t169 (or (= @t25 tptp.zero_zero_nat) (exists (@list @t193) (and (= @t25 (_ tptp.suc @t193)) (_ (_ tptp.ord_less_nat @t193) @t22))))))) % 0.40/0.89 (assume @p90 (forall @t24 (=> @t80 @t197))) % 0.40/0.89 (assume @p91 (forall @t206 (= @t205 (and @t121 (forall @t202 (=> @t201 @t199)))))) % 0.40/0.89 (assume @p92 (forall @t24 (= @t80 (exists (@list @t133) (= @t22 (_ tptp.suc @t133)))))) % 0.40/0.89 (assume @p93 (forall @t206 (= @t207 (or @t121 (exists @t202 (and @t201 @t199)))))) % 0.40/0.89 (assume @p94 (forall @t89 (=> @t80 (=> (_ @t21 @t25) (_ @t208 @t25))))) % 0.40/0.89 (assume @p95 (forall (@list @t25 @t22 @t209) (=> @t98 (=> (forall @t145 (_ @t211 @t143)) (=> (forall (@list @t143 @t147 @t210) (=> (_ @t211 @t147) (=> (_ (_ @t209 @t147) @t210) (_ @t211 @t210)))) (=> (forall @t130 (_ (_ @t209 @t48) @t49)) (_ (_ @t209 @t25) @t22))))))) % 0.40/0.89 (assume @p96 (forall (@list @t25 @t22 @t118) (=> @t98 (=> (_ @t118 @t25) (=> (forall @t130 (=> (_ @t97 @t48) @t183)) @t123))))) % 0.40/0.89 (assume @p97 (forall @t124 (=> (forall @t130 (=> (forall @t129 (=> (_ (_ tptp.ord_less_eq_nat (_ tptp.suc @t126)) @t48) @t127)) @t125)) @t123))) % 0.40/0.89 (assume @p98 (forall @t30 (= @t212 (_ @t88 @t25)))) % 0.40/0.89 (assume @p99 (forall @t24 (not (_ @t88 @t22)))) % 0.40/0.89 (assume @p100 (forall @t30 (= @t214 (or @t98 @t213)))) % 0.40/0.89 (assume @p101 (forall (@list @t22 @t215) (=> (_ @t88 @t215) (exists @t196 (= @t215 @t195))))) % 0.40/0.89 (assume @p102 (forall @t30 (=> @t98 @t214))) % 0.40/0.89 (assume @p103 (forall @t30 (=> @t214 (=> @t212 @t213)))) % 0.40/0.89 (assume @p104 (forall @t30 (=> @t174 @t98))) % 0.40/0.89 (assume @p105 (forall @t220 (=> @t98 (_ (_ tptp.ord_less_eq_nat @t219) @t218)))) % 0.40/0.89 (assume @p106 (forall @t223 (=> (_ @t160 @t184) (=> (_ @t221 @t184) (= (_ (_ tptp.ord_less_eq_nat (_ @t222 @t83)) (_ @t222 @t146)) (_ @t221 @t83)))))) % 0.40/0.89 (assume @p107 (forall @t30 (_ (_ tptp.ord_less_eq_nat @t27) @t25))) % 0.40/0.89 (assume @p108 (forall @t220 (=> @t98 (_ (_ tptp.ord_less_eq_nat (_ @t26 @t216)) (_ @t94 @t216))))) % 0.40/0.89 (assume @p109 (forall @t192 (=> @t191 (=> @t190 (= (_ (_ tptp.minus_minus_nat @t188) @t187) @t27))))) % 0.40/0.89 (assume @p110 (forall @t192 (=> @t191 (=> @t190 (= (_ (_ tptp.ord_less_eq_nat @t188) @t187) @t98))))) % 0.40/0.89 (assume @p111 (forall @t192 (=> @t191 (=> @t190 (= (= @t188 @t187) @t109))))) % 0.40/0.89 (assume @p112 (forall @t24 (=> @t82 @t197))) % 0.40/0.89 (assume @p113 (forall (@list @t118 @t69) (=> @t121 (=> (forall @t226 (=> (_ @t118 @t224) (_ @t118 @t225))) (_ @t118 @t69))))) % 0.40/0.89 (assume @p114 (forall (@list @t140) (=> (not (= @t140 tptp.zero_zero_nat)) (not (forall @t226 (not (= @t140 @t225))))))) % 0.40/0.89 (assume @p115 (forall @t91 (not (= tptp.zero_zero_nat @t28)))) % 0.40/0.89 (assume @p116 (forall @t91 (not (= @t28 tptp.zero_zero_nat)))) % 0.40/0.89 (assume @p117 (forall (@list @t118 @t31) (=> @t149 (=> @t227 @t121)))) % 0.40/0.89 (assume @p118 (forall (@list @t228 @t25 @t22) (=> (forall @t145 (_ @t230 tptp.zero_zero_nat)) (=> (forall @t148 (_ (_ @t228 tptp.zero_zero_nat) @t229)) (=> (forall (@list @t143 @t147) (=> (_ @t230 @t147) (_ (_ @t228 (_ tptp.suc @t143)) @t229))) (_ (_ @t228 @t25) @t22)))))) % 0.40/0.89 (assume @p119 (forall @t124 (=> @t121 (=> (forall @t130 @t183) @t123)))) % 0.40/0.89 (assume @p120 (forall (@list @t69 @t72) (=> (= @t69 @t73) (not (= @t69 tptp.zero_zero_nat))))) % 0.40/0.89 (assume @p121 (forall @t231 (not (= tptp.zero_zero_nat @t70)))) % 0.40/0.89 (assume @p122 (forall @t231 (not (= @t70 tptp.zero_zero_nat)))) % 0.40/0.89 (assume @p123 (forall (@list @t72) (not (= tptp.zero_zero_nat @t73)))) % 0.40/0.89 (assume @p124 (forall @t91 (= (_ @t26 tptp.zero_zero_nat) @t25))) % 0.40/0.89 (assume @p125 (forall @t30 (=> @t99 (=> (= @t96 tptp.zero_zero_nat) @t109)))) % 0.40/0.89 (assume @p126 (forall (@list @t150 @t22 @t25) (=> @t233 (= (_ @t232 (_ @t150 @t25)) @t113)))) % 0.40/0.89 (assume @p127 (forall @t168 (=> @t233 (=> (_ @t79 @t162) (_ @t232 @t163))))) % 0.40/0.89 (assume @p128 (forall (@list @t22 @t93) (=> @t80 (_ (_ tptp.ord_less_nat (_ @t94 @t234)) @t22)))) % 0.40/0.89 (assume @p129 (forall @t206 (=> @t80 (=> (_ @t118 tptp.one_one_nat) (=> (forall @t130 (=> @t137 @t183)) @t123))))) % 0.40/0.89 (assume @p130 (forall @t89 (=> @t87 (= @t32 (_ tptp.suc @t27))))) % 0.40/0.89 (assume @p131 (= tptp.one_one_nat @t40)) % 0.40/0.89 (assume @p132 (forall @t89 (=> @t235 @t173))) % 0.40/0.89 (assume @p133 (forall @t182 (=> @t241 (=> (forall @t239 (=> (= @t103 @t237) @t236)) (=> (forall @t239 (=> (_ @t153 @t103) (=> @t238 @t236))) @t175))))) % 0.40/0.89 (assume @p134 (forall (@list @t93 @t103 @t228) (=> @t241 (=> (forall @t239 (_ @t242 @t237)) (=> (forall (@list @t152 @t151 @t117) (=> @t154 (=> (_ (_ tptp.ord_less_nat @t151) @t117) (=> (_ @t242 @t151) (=> (_ (_ @t228 @t151) @t117) (_ @t242 @t117)))))) (_ (_ @t228 @t93) @t103)))))) % 0.40/0.89 (assume @p135 (forall @t107 (=> @t241 (=> @t244 @t243)))) % 0.40/0.89 (assume @p136 (forall @t30 (=> @t78 @t76))) % 0.40/0.89 (assume @p137 (forall @t89 (=> @t235 (=> @t172 @t109)))) % 0.40/0.89 (assume @p138 (forall @t89 (= (_ (_ tptp.ord_less_nat @t23) @t25) (exists (@list @t245) (and (= @t25 (_ tptp.suc @t245)) (_ @t79 @t245)))))) % 0.40/0.89 (assume @p139 (forall @t206 (= @t205 (and @t123 (forall @t202 (=> @t201 @t203)))))) % 0.40/0.89 (assume @p140 (forall @t30 (= @t246 @t172))) % 0.40/0.89 (assume @p141 (forall @t30 (= @t169 @t138))) % 0.40/0.89 (assume @p142 (forall @t206 (= @t207 (or @t123 (exists @t202 (and @t201 @t203)))))) % 0.40/0.89 (assume @p143 (forall @t30 (=> @t76 @t169))) % 0.40/0.89 (assume @p144 (forall @t30 (=> @t169 (=> @t246 @t109)))) % 0.40/0.89 (assume @p145 (forall @t30 (=> @t76 (=> (not (= @t28 @t22)) @t247)))) % 0.40/0.89 (assume @p146 (forall @t249 (=> @t243 @t248))) % 0.40/0.89 (assume @p147 (forall @t30 (=> @t247 @t76))) % 0.40/0.89 (assume @p148 (forall @t249 (=> (_ @t240 @t31) (=> (not (= @t31 @t234)) @t248)))) % 0.40/0.89 (assume @p149 (forall (@list @t103 @t31 @t22) (=> @t244 (_ (_ tptp.ord_less_nat (_ (_ tptp.minus_minus_nat @t103) @t22)) @t31)))) % 0.40/0.89 (assume @p150 (forall @t220 (=> @t76 (=> (_ @t75 @t216) (_ (_ tptp.ord_less_nat @t219) @t218))))) % 0.40/0.89 (assume @p151 (forall @t89 (=> @t80 (= @t32 (_ @t26 @t100))))) % 0.40/0.89 (assume @p152 (forall @t24 (=> @t80 (= @t22 @t101)))) % 0.40/0.89 (assume @p153 (forall @t24 (not (= @t22 @t23)))) % 0.40/0.89 (assume @p154 (forall @t142 (=> (= (_ tptp.suc @t139) (_ tptp.suc @t140)) @t141))) % 0.40/0.89 (assume @p155 (forall @t107 (= (_ (_ tptp.minus_minus_nat (_ @t250 @t103)) @t31) (_ (_ tptp.minus_minus_nat (_ @t250 @t31)) @t103)))) % 0.40/0.89 (assume @p156 (forall @t30 (_ @t208 @t28))) % 0.40/0.89 (assume @p157 (forall @t89 (=> @t113 (= (_ tptp.suc @t34) @t27)))) % 0.40/0.89 (assume @p158 (forall (@list @t118 @t31 @t93) (=> @t149 (=> @t227 (_ @t118 (_ (_ tptp.minus_minus_nat @t31) @t93)))))) % 0.40/0.89 (assume @p159 (_ (_ tptp.ord_less_nat tptp.nMsg) @t20)) % 0.40/0.89 (assume @p160 (forall @t255 (= (_ @t21 @t254) @t253))) % 0.40/0.89 (assume @p161 (forall @t260 (= (_ @t21 @t259) @t258))) % 0.40/0.89 (assume @p162 (forall @t255 (= (= @t254 tptp.zero_zero_nat) @t252))) % 0.40/0.89 (assume @p163 (forall @t260 (= (= @t259 tptp.zero_zero_nat) @t257))) % 0.40/0.89 (assume @p164 (forall @t14 (=> (_ @t12 @t20) (=> (_ @t39 @t4) (_ (_ tptp.enabled_p_v_s @t8) tptp.msg))))) % 0.40/0.89 (assume @p165 (_ (_ tptp.enabled_p_v_s (_ @t7 @t38)) tptp.msg)) % 0.40/0.89 (assume @p166 (= (_ @t7 @t41) @t261)) % 0.40/0.89 (assume @p167 (forall @t85 (= (_ @t185 @t83) tptp.zero_zero_nat))) % 0.40/0.89 (assume @p168 (_ @t262 tptp.msg)) % 0.40/0.89 (assume @p169 (_ @t262 tptp.msgInSet)) % 0.40/0.89 (assume @p170 (forall @t85 (= (_ @t92 @t83) tptp.zero_zero_nat))) % 0.40/0.89 (assume @p171 (forall @t85 (= (_ @t185 tptp.zero_zero_nat) @t83))) % 0.40/0.89 (assume @p172 (_ @t263 tptp.msg)) % 0.40/0.89 (assume @p173 (_ @t263 tptp.msgInSet)) % 0.40/0.89 (assume @p174 (_ (_ tptp.enabled_p_v_s (_ @t7 tptp.nMsg)) tptp.msg)) % 0.40/0.89 (assume @p175 (_ (_ tptp.enabled_p_v_s (_ tptp.last_c571238084t_unit @t264)) tptp.msg)) % 0.40/0.89 (assume @p176 (forall @t265 (= (= tptp.zero_zero_nat @t139) (= @t139 tptp.zero_zero_nat)))) % 0.40/0.89 (assume @p177 (forall @t265 (= (= tptp.one_one_nat @t139) (= @t139 tptp.one_one_nat)))) % 0.40/0.89 (assume @p178 (forall @t223 (= (_ (_ tptp.minus_minus_nat @t186) @t146) (_ (_ tptp.minus_minus_nat (_ @t185 @t146)) @t184)))) % 0.40/0.89 (assume @p179 (forall @t269 (=> (not @t268) (not @t267)))) % 0.40/0.89 (assume @p180 (forall @t273 (=> (not @t272) (not @t271)))) % 0.40/0.89 (assume @p181 (forall @t24 (exists @t276 (= @t275 @t22)))) % 0.40/0.89 (assume @p182 (forall @t24 (exists @t279 (= @t278 @t22)))) % 0.40/0.89 (assume @p183 (forall @t255 (=> @t253 (= (_ tptp.last_c571238084t_unit @t251) (_ @t280 (_ (_ tptp.minus_minus_nat @t254) tptp.one_one_nat)))))) % 0.40/0.89 (assume @p184 (forall @t260 (=> @t258 (= (_ tptp.last_message_p_v @t256) (_ @t281 (_ (_ tptp.minus_minus_nat @t259) tptp.one_one_nat)))))) % 0.40/0.89 (assume @p185 (forall @t265 (_ @t90 @t139))) % 0.40/0.89 (assume @p186 (_ @t90 tptp.zero_zero_nat)) % 0.40/0.89 (assume @p187 (forall @t24 (= @t80 @t82))) % 0.40/0.89 (assume @p188 (not (_ @t21 tptp.zero_zero_nat))) % 0.40/0.89 (assume @p189 (_ (_ tptp.ord_less_eq_nat tptp.one_one_nat) tptp.one_one_nat)) % 0.40/0.89 (assume @p190 (not (_ (_ tptp.ord_less_nat tptp.one_one_nat) tptp.one_one_nat))) % 0.40/0.89 (assume @p191 (forall (@list @t282 @t251) (=> (forall @t276 (=> (forall (@list @t283) (=> (_ (_ tptp.ord_less_nat (_ tptp.size_s1406904903t_unit @t283)) @t275) (_ @t282 @t283))) (_ @t282 @t274))) (_ @t282 @t251)))) % 0.40/0.89 (assume @p192 (forall (@list @t284 @t256) (=> (forall @t279 (=> (forall (@list @t285) (=> (_ (_ tptp.ord_less_nat (_ tptp.size_s1168481041ge_p_v @t285)) @t278) (_ @t284 @t285))) (_ @t284 @t277))) (_ @t284 @t256)))) % 0.40/0.89 (assume @p193 (_ @t21 tptp.one_one_nat)) % 0.40/0.89 (assume @p194 (= @t286 tptp.zero_zero_nat)) % 0.40/0.89 (assume @p195 (= (_ tptp.size_s1168481041ge_p_v tptp.nil_message_p_v) tptp.zero_zero_nat)) % 0.40/0.89 (assume @p196 (forall @t269 (=> @t268 (=> (forall @t239 (=> (_ @t153 @t254) (= (_ @t280 @t152) (_ (_ tptp.nth_co1649820636t_unit @t266) @t152)))) @t267)))) % 0.40/0.89 (assume @p197 (forall @t273 (=> @t272 (=> (forall @t239 (=> (_ @t153 @t259) (= (_ @t281 @t152) (_ (_ tptp.nth_message_p_v @t270) @t152)))) @t271)))) % 0.40/0.89 (assume @p198 (forall (@list @t31 @t289) (= (forall @t202 (=> @t291 (exists (@list @t293) (_ @t290 @t293)))) (exists (@list @t287) (and (= @t292 @t31) (forall @t202 (=> @t291 (_ @t290 @t288)))))))) % 0.40/0.89 (assume @p199 (forall (@list @t31 @t296) (= (forall @t202 (=> @t291 (exists (@list @t299) (_ @t297 @t299)))) (exists (@list @t294) (and (= @t298 @t31) (forall @t202 (=> @t291 (_ @t297 @t295)))))))) % 0.40/0.89 (assume @p200 (= (lambda (@list @t302 @t301) (= @t302 @t301)) (lambda (@list @t287 @t300) (and (= @t292 (_ tptp.size_s1406904903t_unit @t300)) (forall @t202 (=> (_ @t200 @t292) (= @t288 (_ (_ tptp.nth_co1649820636t_unit @t300) @t198)))))))) % 0.40/0.89 (assume @p201 (= (lambda (@list @t305 @t304) (= @t305 @t304)) (lambda (@list @t294 @t303) (and (= @t298 (_ tptp.size_s1168481041ge_p_v @t303)) (forall @t202 (=> (_ @t200 @t298) (= @t295 (_ (_ tptp.nth_message_p_v @t303) @t198)))))))) % 0.40/0.89 (assume @p202 (forall @t314 (=> @t313 (forall @t311 (=> (_ @t310 @t309) (= (_ (_ tptp.nth_co1649820636t_unit @t308) @t306) (_ (_ tptp.nth_co1649820636t_unit @t307) @t306))))))) % 0.40/0.89 (assume @p203 (forall @t320 (=> @t319 (forall @t311 (=> (_ @t310 @t317) (= (_ (_ tptp.nth_message_p_v @t316) @t306) (_ (_ tptp.nth_message_p_v @t315) @t306))))))) % 0.40/0.89 (assume @p204 (forall (@list @t323 @t322 @t321) (= (_ @t324 tptp.zero_zero_nat) tptp.nil_message_p_v))) % 0.40/0.89 (assume @p205 (_ (_ tptp.enabled_p_v_s (_ (_ tptp.nth_co1649820636t_unit @t264) tptp.n0)) tptp.msg)) % 0.40/0.89 (assume @p206 (_ (_ tptp.ord_less_nat tptp.n0) (_ tptp.size_s1406904903t_unit @t264))) % 0.40/0.89 (assume @p207 (forall @t332 (=> @t331 (exists @t329 (and @t328 (forall @t327 (=> (_ @t118 @t325) (_ (_ tptp.ord_less_eq_nat @t326) @t325)))))))) % 0.40/0.89 (assume @p208 (forall (@list @t308 @t307 @t333) (=> @t313 (=> (_ (_ tptp.prefix1615116500t_unit @t307) @t333) (_ @t312 @t333))))) % 0.40/0.89 (assume @p209 (forall (@list @t316 @t315 @t334) (=> @t319 (=> (_ (_ tptp.prefix47729710ge_p_v @t315) @t334) (_ @t318 @t334))))) % 0.40/0.89 (assume @p210 (forall (@list @t336 @t118 @t335) (=> (forall @t239 (=> (_ @t337 @t152) (=> @t236 (and @t238 (_ @t335 @t152))))) (=> (_ @t118 @t336) (forall @t14 (=> (_ @t337 @t4) (_ @t335 @t4))))))) % 0.40/0.89 (assume @p211 (forall (@list @t339 @t338) (=> (_ @t21 @t339) (=> (_ @t338 tptp.zero_zero_nat) (=> (not (_ @t338 @t339)) (exists @t130 (and (_ @t178 @t339) (_ @t338 @t48) (not (_ @t338 @t49))))))))) % 0.40/0.89 (assume @p212 (forall @t332 (=> @t331 (exists @t329 (and @t328 (or (= @t326 tptp.zero_zero_nat) (not (_ @t118 (_ (_ tptp.minus_minus_nat @t326) tptp.one_one_nat))))))))) % 0.40/0.89 (assume @p213 (forall @t314 (=> @t313 (_ (_ tptp.ord_less_nat @t309) (_ tptp.size_s1406904903t_unit @t307))))) % 0.40/0.89 (assume @p214 (forall @t320 (=> @t319 (_ (_ tptp.ord_less_nat @t317) (_ tptp.size_s1168481041ge_p_v @t315))))) % 0.40/0.89 (assume @p215 (forall (@list @t342 @t341 @t340 @t344 @t157) (=> (= (_ @t343 @t344) @t157) (=> (=> (= @t344 tptp.zero_zero_nat) (not (= @t157 tptp.nil_message_p_v))) (not (forall @t130 (=> (= @t344 @t49) (not (= @t157 (_ (_ @t340 (_ (_ (_ (_ tptp.fLPThe1519354920_p_v_s @t342) @t341) @t340) @t48)) (_ @t343 @t48))))))))))) % 0.40/0.89 (assume @p216 (forall @t348 (= (_ @t346 @t23) (_ (_ @t322 @t347) @t345)))) % 0.40/0.89 (assume @p217 (forall @t348 (= (_ @t324 @t23) (_ (_ @t321 @t347) @t345)))) % 0.40/0.89 (assume @p218 (not (= tptp.msgInSet (_ @t350 @t36)))) % 0.40/0.89 (assume @p219 (forall @t327 (=> (_ @t357 @t325) (forall @t356 (=> (_ @t355 (_ tptp.size_s1168481041ge_p_v @t352)) (=> (_ (_ tptp.ord_less_eq_nat @t354) @t351) (not (= tptp.msg (_ (_ tptp.nth_message_p_v @t352) @t351))))))))) % 0.40/0.89 (assume @p220 (forall @t14 (_ (_ tptp.prefix47729710ge_p_v (_ tptp.ft @t4)) (_ tptp.ft @t33)))) % 0.40/0.89 (assume @p221 (_ (_ tptp.ord_less_nat @t360) @t359)) % 0.40/0.89 (assume @p222 (forall @t14 (=> (_ @t12 @t360) (= (_ @t350 @t4) @t362)))) % 0.40/0.89 (assume @p223 (_ (_ tptp.ord_less_nat @t36) @t360)) % 0.40/0.89 (assume @p224 (forall @t14 (=> @t364 (=> @t363 (not (= @t362 tptp.msg)))))) % 0.40/0.89 (assume @p225 (not (exists @t14 (and @t364 @t363 (= tptp.msg @t362))))) % 0.40/0.89 (assume @p226 (forall @t327 (=> @t369 (=> @t368 (= @t366 @t365))))) % 0.40/0.89 (assume @p227 (_ (_ @t370 tptp.msgInSet) tptp.n1)) % 0.40/0.89 (assume @p228 (forall (@list @t375 @t339 @t22 @t371) (=> (and (_ @t376 @t339) (_ (_ tptp.ord_less_nat @t339) (_ tptp.size_s1406904903t_unit @t378)) (_ (_ tptp.enabled_p_v_s (_ @t379 @t375)) @t371)) (or (_ (_ tptp.enabled_p_v_s (_ @t379 @t339)) @t371) (exists @t377 (and (_ @t376 @t372) (_ @t374 (_ tptp.size_s1168481041ge_p_v @t373)) (= (_ (_ tptp.nth_message_p_v @t373) @t372) @t371))))))) % 0.40/0.89 (assume @p229 (_ (_ @t370 tptp.msg) tptp.nMsg)) % 0.40/0.89 (assume @p230 (forall @t327 (=> @t369 (=> @t368 (not (= tptp.msgInSet @t366)))))) % 0.40/0.89 (assume @p231 (=> (exists @t356 (and (_ @t382 @t351) (_ @t355 @t354) (= (_ (_ tptp.nth_message_p_v @t353) @t351) tptp.msg))) (exists (@list @t380) (and (_ @t357 @t380) (exists @t377 (and (_ @t382 @t372) (_ @t374 (_ tptp.size_s1168481041ge_p_v @t381)) (= tptp.msg (_ (_ tptp.nth_message_p_v @t381) @t372)))))))) % 0.40/0.89 (assume @p232 (forall @t327 (=> @t369 (=> @t383 (not (= tptp.msgInSet @t365)))))) % 0.40/0.89 (assume @p233 (forall @t327 (=> (_ (_ tptp.ord_less_eq_nat tptp.nMsg) @t325) (=> @t383 (not (= tptp.msg @t365)))))) % 0.40/0.89 (assume @p234 @t385) % 0.40/0.89 (assume @p235 true) % 0.40/0.89 (step @p236 (= tptp.ord_less_nat @t386) :rule refl :args (@t386)) % 0.40/0.89 (step @p237 :rule evaluate :args ((= true false))) % 0.40/0.89 (step @p238 :rule refl :args (@t171)) % 0.40/0.89 (step @p239 :rule refl :args (@t387)) % 0.40/0.89 (step @p240 :rule refl :args (@t87)) % 0.40/0.89 (step @p241 :rule cong :premises (@p240 @p239) :args ((= @t87 @t387))) % 0.40/0.89 (step @p242 :rule symm :premises (@p241)) % 0.40/0.89 (step @p243 :rule eq_resolve :premises (@p240 @p242)) % 0.40/0.89 (step @p244 :rule cong :premises (@p243) :args (@t388)) % 0.40/0.89 (step @p245 :rule refl :args (@t389)) % 0.40/0.89 (step @p246 :rule refl :args (@t98)) % 0.40/0.89 (step @p247 :rule cong :premises (@p246 @p245) :args ((= @t98 @t389))) % 0.40/0.89 (step @p248 :rule symm :premises (@p247)) % 0.40/0.89 (step @p249 :rule eq_resolve :premises (@p246 @p248)) % 0.40/0.89 (step @p250 :rule cong :premises (@p249) :args (@t212)) % 0.40/0.89 (step @p251 :rule nary_cong :premises (@p250 @p244 @p238) :args (@t390)) % 0.40/0.89 (step @p252 :rule cong :premises (@p251) :args ((forall @t30 @t390))) % 0.40/0.89 (step @p253 :rule aci_norm :args ((= (or @t212 (or @t388 @t171)) @t390))) % 0.40/0.89 (step @p254 :rule bool-impl-elim :args (@t87 @t171)) % 0.40/0.89 (step @p255 :rule refl :args (@t212)) % 0.40/0.89 (step @p256 :rule nary_cong :premises (@p255 @p254) :args ((or @t212 @t391))) % 0.40/0.89 (step @p257 :rule trans :premises (@p256 @p253)) % 0.40/0.89 (step @p258 :rule bool-impl-elim :args (@t98 @t391)) % 0.40/0.89 (step @p259 :rule trans :premises (@p258 @p257)) % 0.40/0.89 (step @p260 :rule cong :premises (@p259) :args ((forall @t30 (=> @t98 @t391)))) % 0.40/0.89 (step @p261 :rule trans :premises (@p260 @p252)) % 0.40/0.89 (step @p262 :rule eq-symm :args (@t25 @t22)) % 0.40/0.89 (step @p263 :rule refl :args (@t87)) % 0.40/0.89 (step @p264 :rule cong :premises (@p263 @p262) :args (@t110)) % 0.40/0.89 (step @p265 :rule refl :args (@t98)) % 0.40/0.89 (step @p266 :rule cong :premises (@p265 @p264) :args (@t111)) % 0.40/0.89 (step @p267 :rule cong :premises (@p266) :args (@t112)) % 0.40/0.89 (step @p268 :rule trans :premises (@p267 @p261)) % 0.40/0.89 (step @p269 :rule eq_resolve :premises (@p52 @p268)) % 0.40/0.89 (step @p270 :rule instantiate :premises (@p269) :args ((@list @t397 @t396))) % 0.40/0.89 (step @p271 :rule eq-symm :args (@t397 @t396)) % 0.40/0.89 (step @p272 :rule refl :args ((tptp.minus_minus_nat @t2 @t398))) % 0.40/0.89 (step @p273 :rule refl :args ((tptp.suc @t286))) % 0.40/0.89 (step @p274 :rule refl :args (@t392)) % 0.40/0.89 (step @p275 :rule cong :premises (@p274) :args (@t393)) % 0.40/0.89 (step @p276 :rule trans :premises (@p275 @p273)) % 0.40/0.89 (step @p277 :rule refl :args ((tptp.size_s1406904903t_unit @t1))) % 0.40/0.89 (step @p278 :rule refl :args (@t394)) % 0.40/0.89 (step @p279 :rule cong :premises (@p278) :args (@t395)) % 0.40/0.89 (step @p280 :rule trans :premises (@p279 @p277)) % 0.40/0.89 (step @p281 :rule cong :premises (@p280 @p276) :args (@t396)) % 0.40/0.89 (step @p282 :rule trans :premises (@p281 @p272)) % 0.40/0.89 (step @p283 :rule refl :args (tptp.minus_minus_nat)) % 0.40/0.89 (step @p284 :rule ho_cong :premises (@p283 @p280)) % 0.40/0.89 (step @p285 :rule ho_cong :premises (@p284 @p276)) % 0.40/0.89 (step @p286 :rule cong :premises (@p285 @p282) :args ((= (_ (_ tptp.minus_minus_nat @t395) @t393) @t396))) % 0.40/0.89 (step @p287 :rule symm :premises (@p286)) % 0.40/0.89 (step @p288 :rule refl :args (@t399)) % 0.40/0.89 (step @p289 :rule eq_resolve :premises (@p288 @p287)) % 0.40/0.89 (step @p290 :rule refl :args (tptp.suc)) % 0.40/0.89 (step @p291 :rule ho_cong :premises (@p290 @p274)) % 0.40/0.89 (step @p292 :rule cong :premises (@p291 @p276) :args ((= (_ tptp.suc @t392) @t393))) % 0.40/0.89 (step @p293 :rule symm :premises (@p292)) % 0.40/0.89 (step @p294 :rule refl :args (@t398)) % 0.40/0.89 (step @p295 :rule eq_resolve :premises (@p294 @p293)) % 0.40/0.89 (step @p296 :rule refl :args (@t286)) % 0.40/0.89 (step @p297 :rule cong :premises (@p296 @p274) :args ((= @t286 @t392))) % 0.40/0.89 (step @p298 :rule symm :premises (@p297)) % 0.40/0.89 (step @p299 :rule eq_resolve :premises (@p296 @p298)) % 0.40/0.89 (step @p300 :rule refl :args (tptp.suc)) % 0.40/0.89 (step @p301 :rule ho_cong :premises (@p300 @p299)) % 0.40/0.89 (step @p302 :rule trans :premises (@p301 @p295)) % 0.40/0.89 (step @p303 :rule refl :args (tptp.size_s1406904903t_unit)) % 0.40/0.89 (step @p304 :rule ho_cong :premises (@p303 @p278)) % 0.40/0.89 (step @p305 :rule cong :premises (@p304 @p280) :args ((= (_ tptp.size_s1406904903t_unit @t394) @t395))) % 0.40/0.89 (step @p306 :rule symm :premises (@p305)) % 0.40/0.89 (step @p307 :rule refl :args (@t2)) % 0.40/0.89 (step @p308 :rule eq_resolve :premises (@p307 @p306)) % 0.40/0.89 (step @p309 :rule refl :args (@t1)) % 0.40/0.89 (step @p310 :rule cong :premises (@p309 @p278) :args ((= @t1 @t394))) % 0.40/0.89 (step @p311 :rule symm :premises (@p310)) % 0.40/0.89 (step @p312 :rule eq_resolve :premises (@p309 @p311)) % 0.40/0.89 (step @p313 :rule refl :args (tptp.size_s1406904903t_unit)) % 0.40/0.89 (step @p314 :rule ho_cong :premises (@p313 @p312)) % 0.40/0.89 (step @p315 :rule trans :premises (@p314 @p308)) % 0.40/0.89 (step @p316 :rule refl :args (tptp.minus_minus_nat)) % 0.40/0.89 (step @p317 :rule ho_cong :premises (@p316 @p315)) % 0.40/0.89 (step @p318 :rule ho_cong :premises (@p317 @p302)) % 0.40/0.89 (step @p319 :rule trans :premises (@p318 @p289)) % 0.40/0.89 (step @p320 :rule refl :args ((tptp.minus_minus_nat tptp.n1 @t398))) % 0.40/0.89 (step @p321 :rule refl :args (tptp.n1)) % 0.40/0.89 (step @p322 :rule cong :premises (@p321 @p276) :args (@t397)) % 0.40/0.89 (step @p323 :rule trans :premises (@p322 @p320)) % 0.40/0.89 (step @p324 :rule refl :args (@t35)) % 0.40/0.89 (step @p325 :rule ho_cong :premises (@p324 @p276)) % 0.40/0.89 (step @p326 :rule cong :premises (@p325 @p323) :args ((= (_ @t35 @t393) @t397))) % 0.40/0.89 (step @p327 :rule symm :premises (@p326)) % 0.40/0.89 (step @p328 :rule refl :args (@t400)) % 0.40/0.89 (step @p329 :rule eq_resolve :premises (@p328 @p327)) % 0.40/0.89 (step @p330 :rule refl :args (@t35)) % 0.40/0.89 (step @p331 :rule ho_cong :premises (@p330 @p302)) % 0.40/0.89 (step @p332 :rule trans :premises (@p331 @p329)) % 0.40/0.89 (step @p333 :rule cong :premises (@p332 @p319) :args (@t401)) % 0.40/0.89 (step @p334 :rule trans :premises (@p333 @p271)) % 0.40/0.89 (step @p335 :rule cong :premises (@p334) :args (@t402)) % 0.40/0.89 (step @p336 :rule refl :args ((tptp.ord_less_eq_nat @t400 @t399))) % 0.40/0.89 (step @p337 :rule cong :premises (@p323 @p282) :args (@t403)) % 0.40/0.89 (step @p338 :rule trans :premises (@p337 @p336)) % 0.40/0.89 (step @p339 :rule refl :args (tptp.ord_less_eq_nat)) % 0.40/0.89 (step @p340 :rule ho_cong :premises (@p339 @p323)) % 0.40/0.89 (step @p341 :rule ho_cong :premises (@p340 @p282)) % 0.40/0.89 (step @p342 :rule cong :premises (@p341 @p338) :args ((= (_ (_ tptp.ord_less_eq_nat @t397) @t396) @t403))) % 0.40/0.89 (step @p343 :rule symm :premises (@p342)) % 0.40/0.89 (step @p344 :rule refl :args (@t404)) % 0.40/0.89 (step @p345 :rule eq_resolve :premises (@p344 @p343)) % 0.40/0.89 (step @p346 :rule refl :args (tptp.ord_less_eq_nat)) % 0.40/0.89 (step @p347 :rule ho_cong :premises (@p346 @p332)) % 0.40/0.89 (step @p348 :rule ho_cong :premises (@p347 @p319)) % 0.40/0.89 (step @p349 :rule trans :premises (@p348 @p345)) % 0.40/0.89 (step @p350 :rule nary_cong :premises (@p349 @p335) :args ((and @t404 @t402))) % 0.40/0.89 (step @p351 :rule symm :premises (@p194)) % 0.40/0.89 (step @p352 :rule ho_cong :premises (@p300 @p351)) % 0.40/0.89 (step @p353 :rule refl :args (@t18)) % 0.40/0.89 (step @p354 :rule ho_cong :premises (@p353 @p352)) % 0.40/0.89 (step @p355 :rule ho_cong :premises (@p330 @p352)) % 0.40/0.89 (step @p356 :rule cong :premises (@p355 @p354) :args (@t405)) % 0.40/0.89 (step @p357 :rule cong :premises (@p356) :args (@t406)) % 0.40/0.89 (step @p358 :rule ho_cong :premises (@p346 @p355)) % 0.40/0.89 (step @p359 :rule ho_cong :premises (@p358 @p354)) % 0.40/0.89 (step @p360 :rule nary_cong :premises (@p359 @p357) :args (@t408)) % 0.40/0.89 (step @p361 :rule beta-reduce :args ((= (_ @t410 @t41) @t408))) % 0.40/0.89 (step @p362 :rule refl :args (@t41)) % 0.40/0.89 (step @p363 :rule beta-reduce :args ((= (_ @t386 @t42) @t410))) % 0.40/0.89 (step @p364 :rule ho_cong :premises (@p363 @p362)) % 0.40/0.89 (step @p365 :rule trans :premises (@p364 @p361)) % 0.40/0.89 (step @p366 :rule refl :args (@t42)) % 0.40/0.89 (step @p367 :rule ho_cong :premises (@p236 @p366)) % 0.40/0.89 (step @p368 :rule ho_cong :premises (@p367 @p362)) % 0.40/0.89 (step @p369 :rule trans :premises (@p368 @p365)) % 0.40/0.89 (step @p370 :rule trans :premises (@p369 @p360 @p350)) % 0.40/0.89 (step @p371 :rule eq_resolve :premises (@p16 @p370)) % 0.40/0.89 (step @p372 :rule and_elim :premises (@p371) :args (0)) % 0.40/0.89 (step @p373 :rule and_elim :premises (@p371) :args (1)) % 0.40/0.89 (step @p374 :rule cnf_or_pos :args (@t414)) % 0.40/0.89 (step @p375 :rule reordering :premises (@p374) :args ((or @t411 @t413 @t412 (not @t414)))) % 0.40/0.89 (step @p376 :rule chain_m_resolution :premises (@p375 @p373 @p372 @p270) :args (@t412 @t415 (@list @t411 @t403 @t414))) % 0.40/0.89 (step @p377 :rule false_intro :premises (@p376)) % 0.40/0.89 (step @p378 :rule refl :args (@t420)) % 0.40/0.89 (step @p379 :rule eq-symm :args (@t395 @t4)) % 0.40/0.89 (step @p380 :rule refl :args (@t422)) % 0.40/0.89 (step @p381 :rule nary_cong :premises (@p380 @p379 @p378) :args (@t423)) % 0.40/0.89 (step @p382 :rule cong :premises (@p381) :args ((forall @t14 @t423))) % 0.40/0.89 (step @p383 :rule refl :args ((tptp.nth_co1649820636t_unit @t6 @t4))) % 0.40/0.89 (step @p384 :rule refl :args (@t4)) % 0.40/0.89 (step @p385 :rule refl :args ((tptp.fe @t5))) % 0.40/0.89 (step @p386 :rule refl :args (@t416)) % 0.40/0.89 (step @p387 :rule cong :premises (@p386) :args (@t417)) % 0.40/0.89 (step @p388 :rule trans :premises (@p387 @p385)) % 0.40/0.89 (step @p389 :rule cong :premises (@p388 @p384) :args (@t418)) % 0.40/0.89 (step @p390 :rule trans :premises (@p389 @p383)) % 0.40/0.89 (step @p391 :rule refl :args (tptp.nth_co1649820636t_unit)) % 0.40/0.89 (step @p392 :rule ho_cong :premises (@p391 @p388)) % 0.40/0.89 (step @p393 :rule ho_cong :premises (@p392 @p384)) % 0.40/0.89 (step @p394 :rule cong :premises (@p393 @p390) :args ((= (_ @t424 @t4) @t418))) % 0.40/0.89 (step @p395 :rule symm :premises (@p394)) % 0.40/0.89 (step @p396 :rule refl :args (@t8)) % 0.40/0.89 (step @p397 :rule eq_resolve :premises (@p396 @p395)) % 0.40/0.89 (step @p398 :rule refl :args (tptp.fe)) % 0.40/0.89 (step @p399 :rule ho_cong :premises (@p398 @p386)) % 0.40/0.89 (step @p400 :rule cong :premises (@p399 @p388) :args ((= (_ tptp.fe @t416) @t417))) % 0.40/0.89 (step @p401 :rule symm :premises (@p400)) % 0.40/0.89 (step @p402 :rule refl :args (@t6)) % 0.40/0.89 (step @p403 :rule eq_resolve :premises (@p402 @p401)) % 0.40/0.89 (step @p404 :rule refl :args (@t5)) % 0.40/0.89 (step @p405 :rule cong :premises (@p404 @p386) :args ((= @t5 @t416))) % 0.40/0.89 (step @p406 :rule symm :premises (@p405)) % 0.40/0.89 (step @p407 :rule eq_resolve :premises (@p404 @p406)) % 0.40/0.89 (step @p408 :rule ho_cong :premises (@p398 @p407)) % 0.40/0.89 (step @p409 :rule trans :premises (@p408 @p403)) % 0.40/0.89 (step @p410 :rule ho_cong :premises (@p391 @p409)) % 0.40/0.89 (step @p411 :rule ho_cong :premises (@p410 @p384)) % 0.40/0.89 (step @p412 :rule trans :premises (@p411 @p397)) % 0.40/0.89 (step @p413 :rule refl :args ((tptp.nth_co1649820636t_unit @t1 @t4))) % 0.40/0.89 (step @p414 :rule cong :premises (@p278 @p384) :args (@t419)) % 0.40/0.89 (step @p415 :rule trans :premises (@p414 @p413)) % 0.40/0.89 (step @p416 :rule ho_cong :premises (@p391 @p278)) % 0.40/0.89 (step @p417 :rule ho_cong :premises (@p416 @p384)) % 0.40/0.89 (step @p418 :rule cong :premises (@p417 @p415) :args ((= (_ @t425 @t4) @t419))) % 0.40/0.89 (step @p419 :rule symm :premises (@p418)) % 0.40/0.89 (step @p420 :rule refl :args (@t10)) % 0.40/0.89 (step @p421 :rule eq_resolve :premises (@p420 @p419)) % 0.40/0.89 (step @p422 :rule eq_resolve :premises (@p309 @p311)) % 0.40/0.89 (step @p423 :rule ho_cong :premises (@p391 @p422)) % 0.40/0.89 (step @p424 :rule ho_cong :premises (@p423 @p384)) % 0.40/0.89 (step @p425 :rule trans :premises (@p424 @p421)) % 0.40/0.89 (step @p426 :rule cong :premises (@p425 @p412) :args (@t11)) % 0.40/0.89 (step @p427 :rule eq_resolve :premises (@p307 @p306)) % 0.40/0.89 (step @p428 :rule ho_cong :premises (@p303 @p422)) % 0.40/0.89 (step @p429 :rule trans :premises (@p428 @p427)) % 0.40/0.89 (step @p430 :rule cong :premises (@p429 @p384) :args (@t426)) % 0.40/0.89 (step @p431 :rule refl :args ((tptp.ord_less_eq_nat @t4 @t2))) % 0.40/0.89 (step @p432 :rule cong :premises (@p384 @p280) :args (@t421)) % 0.40/0.89 (step @p433 :rule trans :premises (@p432 @p431)) % 0.40/0.89 (step @p434 :rule refl :args (@t136)) % 0.40/0.89 (step @p435 :rule ho_cong :premises (@p434 @p280)) % 0.40/0.89 (step @p436 :rule cong :premises (@p435 @p433) :args ((= (_ @t136 @t395) @t421))) % 0.40/0.89 (step @p437 :rule symm :premises (@p436)) % 0.40/0.89 (step @p438 :rule refl :args (@t427)) % 0.40/0.89 (step @p439 :rule eq_resolve :premises (@p438 @p437)) % 0.40/0.89 (step @p440 :rule ho_cong :premises (@p434 @p429)) % 0.40/0.89 (step @p441 :rule trans :premises (@p440 @p439)) % 0.40/0.89 (step @p442 :rule cong :premises (@p441) :args (@t428)) % 0.40/0.89 (step @p443 :rule nary_cong :premises (@p442 @p430 @p426) :args (@t429)) % 0.40/0.89 (step @p444 :rule cong :premises (@p443) :args ((forall @t14 @t429))) % 0.40/0.89 (step @p445 :rule trans :premises (@p444 @p382)) % 0.40/0.89 (step @p446 :rule aci_norm :args ((= (or (or @t428 @t426) @t11) @t429))) % 0.40/0.89 (step @p447 :rule refl :args (@t11)) % 0.40/0.89 (step @p448 :rule bool-double-not-elim :args (@t426)) % 0.40/0.89 (step @p449 :rule refl :args (@t428)) % 0.40/0.89 (step @p450 :rule nary_cong :premises (@p449 @p448) :args ((or @t428 (not @t430)))) % 0.40/0.89 (step @p451 :rule bool-and-de-morgan :args (@t427 @t430 true)) % 0.40/0.89 (step @p452 :rule trans :premises (@p451 @p450)) % 0.40/0.89 (step @p453 :rule nary_cong :premises (@p452 @p447) :args ((or (not @t431) @t11))) % 0.40/0.89 (step @p454 :rule trans :premises (@p453 @p446)) % 0.40/0.89 (step @p455 :rule bool-impl-elim :args (@t431 @t11)) % 0.40/0.89 (step @p456 :rule trans :premises (@p455 @p454)) % 0.40/0.89 (step @p457 :rule cong :premises (@p456) :args ((forall @t14 (=> @t431 @t11)))) % 0.40/0.89 (step @p458 :rule trans :premises (@p457 @p445)) % 0.40/0.89 (step @p459 :rule refl :args (@t11)) % 0.40/0.89 (step @p460 :rule eq-symm :args (@t4 @t2)) % 0.40/0.89 (step @p461 :rule cong :premises (@p460) :args (@t432)) % 0.40/0.89 (step @p462 :rule refl :args (@t427)) % 0.40/0.89 (step @p463 :rule nary_cong :premises (@p462 @p461) :args (@t433)) % 0.40/0.89 (step @p464 :rule beta-reduce :args ((= (_ @t434 @t2) @t433))) % 0.40/0.89 (step @p465 :rule trans :premises (@p464 @p463)) % 0.40/0.89 (step @p466 :rule refl :args (@t2)) % 0.40/0.89 (step @p467 :rule beta-reduce :args ((= @t435 @t434))) % 0.40/0.89 (step @p468 :rule ho_cong :premises (@p467 @p466)) % 0.40/0.89 (step @p469 :rule trans :premises (@p468 @p465)) % 0.40/0.89 (step @p470 :rule cong :premises (@p469 @p459) :args (@t436)) % 0.40/0.89 (step @p471 :rule cong :premises (@p470) :args ((forall @t14 @t436))) % 0.40/0.89 (step @p472 :rule trans :premises (@p471 @p458)) % 0.40/0.89 (step @p473 :rule refl :args (@t4)) % 0.40/0.89 (step @p474 :rule ho_cong :premises (@p236 @p473)) % 0.40/0.89 (step @p475 :rule ho_cong :premises (@p474 @p466)) % 0.40/0.89 (step @p476 :rule cong :premises (@p475 @p459) :args (@t13)) % 0.40/0.89 (step @p477 :rule cong :premises (@p476) :args (@t15)) % 0.40/0.89 (step @p478 :rule trans :premises (@p477 @p472)) % 0.40/0.89 (step @p479 :rule eq_resolve :premises (@p2 @p478)) % 0.40/0.89 (step @p480 :rule refl :args (@t439)) % 0.40/0.89 (step @p481 :rule eq-symm :args (@t397 @t395)) % 0.40/0.89 (step @p482 :rule refl :args (@t441)) % 0.40/0.89 (step @p483 :rule nary_cong :premises (@p482 @p481 @p480) :args (@t442)) % 0.40/0.89 (step @p484 :rule refl :args (@t443)) % 0.40/0.89 (step @p485 :rule cong :premises (@p484 @p483) :args ((=> @t443 @t442))) % 0.40/0.89 (assume-push @p617 @t443) % 0.40/0.89 (step @p487 :rule instantiate :premises (@p479) :args ((@list @t397))) % 0.40/0.89 (step-pop @p618 :rule scope :premises (@p487)) % 0.40/0.89 (step @p488 :rule process_scope :premises (@p618) :args (@t442)) % 0.40/0.89 (step @p490 :rule eq_resolve :premises (@p488 @p485)) % 0.40/0.89 (step @p491 :rule implies_elim :premises (@p490)) % 0.40/0.89 (step @p492 :rule chain_m_resolution :premises (@p491 @p479) :args (@t445 (@list false) (@list @t443))) % 0.40/0.89 (step @p493 :rule refl :args (@t446)) % 0.40/0.89 (step @p494 :rule refl :args (@t102)) % 0.40/0.89 (step @p495 :rule cong :premises (@p494 @p493) :args ((= @t102 @t446))) % 0.40/0.89 (step @p496 :rule symm :premises (@p495)) % 0.40/0.89 (step @p497 :rule eq_resolve :premises (@p494 @p496)) % 0.40/0.89 (step @p498 :rule refl :args (@t447)) % 0.40/0.89 (step @p499 :rule refl :args (@t104)) % 0.40/0.89 (step @p500 :rule cong :premises (@p499 @p498) :args ((= @t104 @t447))) % 0.40/0.89 (step @p501 :rule symm :premises (@p500)) % 0.40/0.89 (step @p502 :rule eq_resolve :premises (@p499 @p501)) % 0.40/0.89 (step @p503 :rule cong :premises (@p502) :args (@t448)) % 0.40/0.89 (step @p504 :rule refl :args (@t449)) % 0.40/0.89 (step @p505 :rule refl :args (@t106)) % 0.40/0.89 (step @p506 :rule cong :premises (@p505 @p504) :args ((= @t106 @t449))) % 0.40/0.89 (step @p507 :rule symm :premises (@p506)) % 0.40/0.89 (step @p508 :rule eq_resolve :premises (@p505 @p507)) % 0.40/0.89 (step @p509 :rule cong :premises (@p508) :args (@t450)) % 0.40/0.89 (step @p510 :rule nary_cong :premises (@p509 @p503 @p497) :args (@t451)) % 0.40/0.89 (step @p511 :rule cong :premises (@p510) :args ((forall @t107 @t451))) % 0.40/0.89 (step @p512 :rule aci_norm :args ((= (or @t450 (or @t448 @t102)) @t451))) % 0.40/0.89 (step @p513 :rule bool-impl-elim :args (@t104 @t102)) % 0.40/0.89 (step @p514 :rule refl :args (@t450)) % 0.40/0.89 (step @p515 :rule nary_cong :premises (@p514 @p513) :args ((or @t450 @t105))) % 0.40/0.89 (step @p516 :rule trans :premises (@p515 @p512)) % 0.40/0.89 (step @p517 :rule bool-impl-elim :args (@t106 @t105)) % 0.40/0.89 (step @p518 :rule trans :premises (@p517 @p516)) % 0.40/0.89 (step @p519 :rule cong :premises (@p518) :args (@t108)) % 0.40/0.89 (step @p520 :rule trans :premises (@p519 @p511)) % 0.40/0.89 (step @p521 :rule eq_resolve :premises (@p50 @p520)) % 0.40/0.89 (step @p522 :rule instantiate :premises (@p521) :args ((@list @t397 @t396 @t395))) % 0.40/0.89 (step @p523 :rule cong :premises (@p315 @p319) :args (@t452)) % 0.40/0.89 (step @p524 :rule cong :premises (@p523) :args (@t453)) % 0.40/0.89 (step @p525 :rule refl :args ((tptp.ord_less_eq_nat @t399 @t2))) % 0.40/0.89 (step @p526 :rule cong :premises (@p282 @p280) :args (@t454)) % 0.40/0.89 (step @p527 :rule trans :premises (@p526 @p525)) % 0.40/0.89 (step @p528 :rule ho_cong :premises (@p339 @p282)) % 0.40/0.89 (step @p529 :rule ho_cong :premises (@p528 @p280)) % 0.40/0.89 (step @p530 :rule cong :premises (@p529 @p527) :args ((= (_ (_ tptp.ord_less_eq_nat @t396) @t395) @t454))) % 0.40/0.89 (step @p531 :rule symm :premises (@p530)) % 0.40/0.89 (step @p532 :rule refl :args (@t455)) % 0.40/0.89 (step @p533 :rule eq_resolve :premises (@p532 @p531)) % 0.40/0.89 (step @p534 :rule ho_cong :premises (@p346 @p319)) % 0.40/0.89 (step @p535 :rule ho_cong :premises (@p534 @p315)) % 0.40/0.89 (step @p536 :rule trans :premises (@p535 @p533)) % 0.40/0.89 (step @p537 :rule nary_cong :premises (@p536 @p524) :args ((and @t455 @t453))) % 0.40/0.89 (step @p538 :rule trans :premises (@p131 @p352)) % 0.40/0.89 (step @p539 :rule ho_cong :premises (@p353 @p538)) % 0.40/0.89 (step @p540 :rule cong :premises (@p466 @p539) :args (@t456)) % 0.40/0.89 (step @p541 :rule cong :premises (@p540) :args (@t457)) % 0.40/0.89 (step @p542 :rule ho_cong :premises (@p346 @p539)) % 0.40/0.89 (step @p543 :rule ho_cong :premises (@p542 @p466)) % 0.40/0.89 (step @p544 :rule nary_cong :premises (@p543 @p541) :args ((and @t458 @t457))) % 0.40/0.89 (step @p545 :rule eq-symm :args (@t19 @t2)) % 0.40/0.89 (step @p546 :rule cong :premises (@p545) :args (@t459)) % 0.40/0.89 (step @p547 :rule refl :args (@t458)) % 0.40/0.89 (step @p548 :rule nary_cong :premises (@p547 @p546) :args (@t460)) % 0.40/0.89 (step @p549 :rule beta-reduce :args ((= (_ @t461 @t2) @t460))) % 0.40/0.89 (step @p550 :rule trans :premises (@p549 @p548)) % 0.40/0.89 (step @p551 :rule beta-reduce :args ((= (_ @t386 @t19) @t461))) % 0.40/0.89 (step @p552 :rule ho_cong :premises (@p551 @p466)) % 0.40/0.89 (step @p553 :rule trans :premises (@p552 @p550)) % 0.40/0.89 (step @p554 :rule refl :args (@t19)) % 0.40/0.89 (step @p555 :rule ho_cong :premises (@p236 @p554)) % 0.40/0.89 (step @p556 :rule ho_cong :premises (@p555 @p466)) % 0.40/0.89 (step @p557 :rule trans :premises (@p556 @p553)) % 0.40/0.89 (step @p558 :rule trans :premises (@p557 @p544 @p537)) % 0.40/0.89 (step @p559 :rule eq_resolve :premises (@p4 @p558)) % 0.40/0.89 (step @p560 :rule and_elim :premises (@p559) :args (0)) % 0.40/0.89 (step @p561 :rule cnf_or_pos :args (@t463)) % 0.40/0.89 (step @p562 :rule reordering :premises (@p561) :args ((or @t462 @t413 @t440 (not @t463)))) % 0.40/0.89 (step @p563 :rule chain_m_resolution :premises (@p562 @p560 @p372 @p522) :args (@t440 (@list false false false) (@list @t454 @t403 @t463))) % 0.40/0.89 (step @p564 :rule eq-symm :args (@t437 @t438)) % 0.40/0.89 (step @p565 :rule refl :args ((tptp.nth_co1649820636t_unit @t1 @t400))) % 0.40/0.89 (step @p566 :rule cong :premises (@p278 @p323) :args (@t438)) % 0.40/0.89 (step @p567 :rule trans :premises (@p566 @p565)) % 0.40/0.89 (step @p568 :rule ho_cong :premises (@p416 @p323)) % 0.40/0.89 (step @p569 :rule cong :premises (@p568 @p567) :args ((= (_ @t425 @t397) @t438))) % 0.40/0.89 (step @p570 :rule symm :premises (@p569)) % 0.40/0.89 (step @p571 :rule refl :args (@t464)) % 0.40/0.89 (step @p572 :rule eq_resolve :premises (@p571 @p570)) % 0.40/0.89 (step @p573 :rule refl :args (tptp.nth_co1649820636t_unit)) % 0.40/0.89 (step @p574 :rule ho_cong :premises (@p573 @p312)) % 0.40/0.89 (step @p575 :rule ho_cong :premises (@p574 @p332)) % 0.40/0.89 (step @p576 :rule trans :premises (@p575 @p572)) % 0.40/0.89 (step @p577 :rule refl :args ((tptp.nth_co1649820636t_unit @t6 @t400))) % 0.40/0.89 (step @p578 :rule cong :premises (@p388 @p323) :args (@t437)) % 0.40/0.89 (step @p579 :rule trans :premises (@p578 @p577)) % 0.40/0.89 (step @p580 :rule ho_cong :premises (@p392 @p323)) % 0.40/0.89 (step @p581 :rule cong :premises (@p580 @p579) :args ((= (_ @t424 @t397) @t437))) % 0.40/0.89 (step @p582 :rule symm :premises (@p581)) % 0.40/0.89 (step @p583 :rule refl :args (@t465)) % 0.40/0.89 (step @p584 :rule eq_resolve :premises (@p583 @p582)) % 0.40/0.89 (step @p585 :rule refl :args (tptp.fe)) % 0.40/0.89 (step @p586 :rule ho_cong :premises (@p585 @p407)) % 0.40/0.89 (step @p587 :rule trans :premises (@p586 @p403)) % 0.40/0.89 (step @p588 :rule ho_cong :premises (@p573 @p587)) % 0.40/0.89 (step @p589 :rule ho_cong :premises (@p588 @p332)) % 0.40/0.89 (step @p590 :rule trans :premises (@p589 @p584)) % 0.40/0.89 (step @p591 :rule cong :premises (@p590 @p576) :args (@t466)) % 0.40/0.89 (step @p592 :rule trans :premises (@p591 @p564)) % 0.40/0.89 (step @p593 :rule cong :premises (@p592) :args ((not @t466))) % 0.40/0.89 (step @p594 :rule eq-symm :args (@t464 @t465)) % 0.40/0.89 (step @p595 :rule cong :premises (@p594) :args ((not (= @t464 @t465)))) % 0.40/0.89 (step @p596 :rule ho_cong :premises (@p330 @p538)) % 0.40/0.89 (step @p597 :rule refl :args (@t7)) % 0.40/0.89 (step @p598 :rule ho_cong :premises (@p597 @p596)) % 0.40/0.89 (step @p599 :rule refl :args (@t9)) % 0.40/0.89 (step @p600 :rule ho_cong :premises (@p599 @p596)) % 0.40/0.89 (step @p601 :rule cong :premises (@p600 @p598) :args (@t467)) % 0.40/0.89 (step @p602 :rule cong :premises (@p601) :args ((not @t467))) % 0.40/0.89 (step @p603 :rule trans :premises (@p602 @p595)) % 0.40/0.89 (step @p604 :rule eq-symm :args (@t384 @t37)) % 0.40/0.89 (step @p605 :rule cong :premises (@p604) :args (@t385)) % 0.40/0.89 (step @p606 :rule trans :premises (@p605 @p603 @p593)) % 0.40/0.89 (step @p607 :rule eq_resolve :premises (@p234 @p606)) % 0.40/0.89 (step @p608 :rule cnf_or_pos :args (@t445)) % 0.40/0.89 (step @p609 :rule reordering :premises (@p608) :args ((or @t439 @t441 @t444 (not @t445)))) % 0.40/0.89 (step @p610 :rule chain_m_resolution :premises (@p609 @p607 @p563 @p492) :args (@t444 @t415 (@list @t439 @t440 @t445))) % 0.40/0.89 (step @p611 :rule refl :args (@t396)) % 0.40/0.89 (step @p612 :rule cong :premises (@p611 @p610) :args (@t454)) % 0.40/0.89 (step @p613 :rule true_intro :premises (@p560)) % 0.40/0.89 (step @p614 :rule symm :premises (@p613)) % 0.40/0.89 (step @p615 :rule trans :premises (@p614 @p612 @p377)) % 0.40/0.89 (step @p616 false :rule eq_resolve :premises (@p615 @p237)) % 0.40/0.89 ) % 0.40/0.89 % SZS output end Proof % 0.40/0.89 % cvc5 exiting %------------------------------------------------------------------------------