Time: 5.817989
TRS:
 {
  Cond_eval_511(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_end(n, i, j, k, l, t, h, m, p, q, r, up),
                               greater_int(pos 0(), pos 0()) -> false(),
                               greater_int(pos 0(), pos s y) -> false(),
                               greater_int(pos 0(), neg 0()) -> false(),
                               greater_int(pos 0(), neg s y) -> true(),
                               greater_int(pos s x, pos 0()) -> true(),
                               greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
                               greater_int(pos s x, neg 0()) -> true(),
                               greater_int(pos s x, neg s y) -> true(),
                               greater_int(neg 0(), pos 0()) -> false(),
                               greater_int(neg 0(), pos s y) -> false(),
                               greater_int(neg 0(), neg 0()) -> false(),
                               greater_int(neg 0(), neg s y) -> true(),
                               greater_int(neg s x, pos 0()) -> false(),
                               greater_int(neg s x, pos s y) -> false(),
                               greater_int(neg s x, neg 0()) -> false(),
                               greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
                eval_51(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_511(greater_int(i, n), n, i, j, k, l, t, h, m, p, q, r, up),
                eval_51(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_51(lesseq_int(i, n), n, i, j, k, l, t, h, m, p, q, r, up),
                eval_52(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_53(n, i, j, k, l, t, h, m, p, q, r, up),
   Cond_eval_51(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_52(n, i, j, k, l, t, h, m, p, q, r, up),
                 eval_5(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_5(not up, n, i, j, k, l, t, h, m, p, q, r, up),
                 eval_5(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_52(up, n, i, j, k, l, t, h, m, p, q, r, up),
                 eval_4(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_5(n, i, j, k, l, t, h, n, p, q, r, up),
   Cond_eval_33(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_38(n, i, j, k, l, t, h, m, p, q, r, up),
                                  lesseq_int(pos x, neg s y) -> false(),
                                  lesseq_int(pos 0(), pos y) -> true(),
                                lesseq_int(pos 0(), neg 0()) -> true(),
                                lesseq_int(pos s x, pos 0()) -> false(),
                                lesseq_int(pos s x, pos s y) -> lesseq_int(pos x, pos y),
                                  lesseq_int(pos s x, neg y) -> false(),
                                    lesseq_int(neg x, pos y) -> true(),
                                  lesseq_int(neg x, neg 0()) -> true(),
                                lesseq_int(neg 0(), neg s y) -> false(),
                                lesseq_int(neg s x, neg s y) -> lesseq_int(neg x, neg y),
                eval_33(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_33(lesseq_int(r, pos 0()), n, i, j, k, l, t, h, m, p, q, r, up),
                eval_33(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_331(greater_int(r, pos 0()), n, i, j, k, l, t, h, m, p, q, r, up),
  Cond_eval_381(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_39(n, i, j, k, l, t, h, m, p, q, r, up),
                eval_38(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_381(greater_int(q, pos 0()), n, i, j, k, l, t, h, m, p, q, r, up),
                eval_38(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_38(lesseq_int(q, pos 0()), n, i, j, k, l, t, h, m, p, q, r, up),
                eval_32(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_23(n, i, j, k, l, t, h, m, p, q, minus_int(r, pos s 0()), up),
                                     minus_int(pos x, pos y) -> minus_nat(x, y),
                                     minus_int(pos x, neg y) -> pos plus_nat(x, y),
                                     minus_int(neg x, pos y) -> neg plus_nat(x, y),
                                     minus_int(neg x, neg y) -> minus_nat(y, x),
                eval_31(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_32(n, i, minus_int(j, pos s 0()), k, l, t, h, m, p, q, r, up),
  Cond_eval_231(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_24(n, i, j, k, l, t, h, m, p, q, r, up),
                                         and(true(), true()) -> true(),
                                        and(true(), false()) -> false(),
                                        and(false(), true()) -> false(),
                                       and(false(), false()) -> false(),
                eval_23(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_231(and(greater_int(q, pos 0()), greater_int(r, pos 0())), n, i, j, k, l, t, h, m, p, q, r, up),
                eval_23(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_23(or(lesseq_int(q, pos 0()), lesseq_int(r, pos 0())), n, i, j, k, l, t, h, m, p, q, r, up),
                eval_19(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_191(less_int(m, p), n, i, j, k, l, t, h, m, p, q, r, up),
                eval_19(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_19(greatereq_int(m, p), n, i, j, k, l, t, h, m, p, q, r, up),
                eval_18(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_19(n, i, j, k, l, t, h, minus_int(m, q), p, q, r, up),
                eval_13(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_14(n, i, mult_int(pos s s 0(), n), k, l, t, h, m, p, q, r, up),
                                      plus_int(pos x, pos y) -> pos plus_nat(x, y),
                                      plus_int(pos x, neg y) -> minus_nat(x, y),
                                      plus_int(neg x, pos y) -> minus_nat(y, x),
                                      plus_int(neg x, neg y) -> neg plus_nat(x, y),
                eval_12(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_13(n, plus_int(pos s 0(), n), j, k, l, t, h, m, p, q, r, up),
                eval_50(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_51(n, pos s 0(), j, k, l, t, h, m, p, q, r, up),
   Cond_eval_49(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_50(n, i, j, k, l, t, h, m, p, q, r, up),
                eval_41(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_42(n, plus_int(pos s 0(), i), j, k, l, t, h, m, p, q, r, up),
                eval_40(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_41(n, i, j, plus_int(k, h), l, t, h, m, p, q, r, up),
    Cond_eval_0(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_1(n, i, j, k, l, t, h, m, p, q, r, true()),
                 eval_0(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_0(greater_int(n, pos 0()), n, i, j, k, l, t, h, m, p, q, r, up),
  Cond_eval_461(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_14(n, i, j, k, l, t, h, m, p, q, r, up),
                eval_46(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_461(greater_int(m, pos 0()), n, i, j, k, l, t, h, m, p, q, r, up),
                eval_46(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_46(lesseq_int(m, pos 0()), n, i, j, k, l, t, h, m, p, q, r, up),
                eval_22(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_23(n, i, j, k, l, t, h, minus_int(m, r), p, q, r, up),
                eval_21(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_22(n, i, j, k, l, t, h, m, p, q, m, up),
                eval_14(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_15(n, i, j, k, l, t, h, m, p, q, r, up),
                                      mult_int(pos x, pos y) -> pos mult_nat(x, y),
                                      mult_int(pos x, neg y) -> neg mult_nat(x, y),
                                      mult_int(neg x, pos y) -> neg mult_nat(x, y),
                                      mult_int(neg x, neg y) -> pos mult_nat(x, y),
                eval_10(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_11(n, i, j, pos s 0(), l, t, h, m, p, q, r, up),
    Cond_eval_5(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_10(n, i, j, k, l, t, h, m, p, q, r, up),
                 eval_3(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_4(n, i, j, k, l, t, pos s 0(), m, p, q, r, up),
                 eval_2(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_3(n, i, j, k, l, t, h, m, p, q, r, up),
  Cond_eval_191(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_21(n, i, j, k, l, t, h, m, p, q, r, up),
                                  less_int(pos 0(), pos 0()) -> false(),
                                  less_int(pos 0(), pos s y) -> true(),
                                  less_int(pos 0(), neg 0()) -> false(),
                                  less_int(pos 0(), neg s y) -> false(),
                                  less_int(pos s x, pos 0()) -> false(),
                                  less_int(pos s x, pos s y) -> less_int(pos x, pos y),
                                  less_int(pos s x, neg 0()) -> false(),
                                  less_int(pos s x, neg s y) -> false(),
                                  less_int(neg 0(), pos 0()) -> false(),
                                  less_int(neg 0(), pos s y) -> true(),
                                  less_int(neg 0(), neg 0()) -> false(),
                                  less_int(neg 0(), neg s y) -> false(),
                                  less_int(neg s x, pos 0()) -> true(),
                                  less_int(neg s x, pos s y) -> true(),
                                  less_int(neg s x, neg 0()) -> true(),
                                  less_int(neg s x, neg s y) -> less_int(neg x, neg y),
  Cond_eval_151(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_17(n, i, j, k, l, t, h, m, p, q, r, up),
                eval_15(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_151(less_int(m, p), n, i, j, k, l, t, h, m, p, q, r, up),
                eval_15(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_15(greatereq_int(m, p), n, i, j, k, l, t, h, m, p, q, r, up),
                eval_47(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_48(n, i, j, k, l, t, h, m, p, q, r, not up),
   Cond_eval_46(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_47(n, i, j, k, t, t, h, m, p, q, r, up),
                eval_53(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_51(n, plus_int(pos s 0(), i), j, k, l, t, h, m, p, q, r, up),
  Cond_eval_491(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_end(n, i, j, k, l, t, h, m, p, q, r, up),
  Cond_eval_481(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_49(n, i, j, k, l, t, h, m, mult_int(pos s s 0(), p), q, r, up),
                               greatereq_int(pos x, pos 0()) -> true(),
                                 greatereq_int(pos x, neg y) -> true(),
                             greatereq_int(pos 0(), pos s y) -> false(),
                             greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
                               greatereq_int(neg x, pos s y) -> false(),
                             greatereq_int(neg 0(), pos 0()) -> true(),
                               greatereq_int(neg 0(), neg y) -> true(),
                             greatereq_int(neg s x, pos 0()) -> false(),
                             greatereq_int(neg s x, neg 0()) -> false(),
                             greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y),
                eval_48(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_481(greatereq_int(p, n), n, i, j, k, l, t, h, m, p, q, r, up),
                eval_48(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_48(less_int(p, n), n, i, j, k, l, t, h, m, p, q, r, up),
                eval_26(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_27(n, i, j, plus_int(k, h), l, t, h, m, p, q, r, up),
                eval_25(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_26(n, i, j, k, l, t, h, m, p, q, r, up),
                eval_37(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_33(n, i, j, k, l, t, h, m, p, q, minus_int(r, pos s 0()), up),
                                                  not true() -> false(),
                                                 not false() -> true(),
                eval_49(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_49(not up, n, i, j, k, l, t, h, m, p, q, r, up),
                eval_49(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_491(up, n, i, j, k, l, t, h, m, p, q, r, up),
   Cond_eval_23(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_33(n, i, j, k, l, t, h, m, p, q, r, up),
                                          or(true(), true()) -> true(),
                                         or(true(), false()) -> true(),
                                         or(false(), true()) -> true(),
                                        or(false(), false()) -> false(),
                 eval_9(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_14(n, i, j, k, mult_int(pos s s 0(), n), t, h, n, p, q, r, up),
                eval_30(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_31(n, i, j, plus_int(k, h), l, t, h, m, p, q, r, up),
                eval_29(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_30(n, i, j, k, l, t, h, m, p, q, r, up),
                eval_20(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_22(n, i, j, k, l, t, h, m, p, q, p, up),
   Cond_eval_19(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_20(n, i, j, k, l, t, h, m, p, q, r, up),
                eval_24(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_25(n, i, j, k, l, t, h, m, p, q, r, up),
                eval_24(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_29(n, i, j, k, l, t, h, m, p, q, r, up),
                eval_39(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_40(n, i, j, k, l, t, h, m, p, q, r, up),
                eval_36(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_37(n, i, minus_int(j, pos s 0()), k, l, t, h, m, p, q, r, up),
                eval_35(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_36(n, i, j, plus_int(k, h), l, t, h, m, p, q, r, up),
                eval_34(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_35(n, i, j, k, l, t, h, m, p, q, r, up),
  Cond_eval_331(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_34(n, i, j, k, l, t, h, m, p, q, r, up),
                 eval_1(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_2(n, i, j, k, l, t, h, m, pos s 0(), q, r, up),
                eval_28(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_23(n, i, j, k, l, t, h, m, p, minus_int(q, pos s 0()), r, up),
                eval_27(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_28(n, plus_int(pos s 0(), i), j, k, l, t, h, m, p, q, r, up),
   Cond_eval_48(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_2(n, i, j, k, l, t, h, m, p, q, r, up),
                 eval_8(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_9(n, i, j, plus_int(pos s 0(), n), l, t, h, n, p, q, r, up),
                eval_43(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_44(n, i, j, k, l, t, neg_int h, m, p, q, r, up),
   Cond_eval_38(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_43(n, i, j, k, l, t, h, m, p, q, r, up),
                eval_42(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_38(n, i, j, k, l, t, h, m, p, minus_int(q, pos s 0()), r, up),
                 eval_7(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_8(n, i, n, k, l, t, h, m, p, q, r, up),
                 eval_6(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_7(n, pos s 0(), j, k, l, t, h, m, p, q, r, up),
                eval_16(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_18(n, i, j, k, l, t, h, m, p, p, r, up),
   Cond_eval_15(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_16(n, i, j, k, l, t, h, m, p, q, r, up),
                eval_44(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_45(n, i, j, k, l, k, h, m, p, q, r, up),
                                               neg_int pos x -> neg x,
                                               neg_int neg x -> pos x,
                eval_11(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_12(n, i, j, k, n, t, h, m, p, q, r, up),
                eval_45(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_46(n, i, j, l, l, t, h, m, p, q, r, up),
   Cond_eval_52(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_6(n, i, j, k, l, t, h, m, p, q, r, up),
                eval_17(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_18(n, i, j, k, l, t, h, m, p, m, r, up),
                                         minus_nat(0(), 0()) -> pos 0(),
                                         minus_nat(0(), s y) -> neg s y,
                                         minus_nat(s x, 0()) -> pos s x,
                                         minus_nat(s x, s y) -> minus_nat(x, y),
                                            plus_nat(0(), x) -> x,
                                            plus_nat(s x, y) -> s plus_nat(x, y),
                                            mult_nat(0(), y) -> 0(),
                                          mult_nat(s x, 0()) -> 0(),
                                          mult_nat(s x, s y) -> plus_nat(mult_nat(x, s y), s y)
 }
 SRS: We consider a TRS.
  Trs:
   {
    Cond_eval_511(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_end(n, i, j, k, l, t, h, m, p, q, r, up),
                                 greater_int(pos 0(), pos 0()) -> false(),
                                 greater_int(pos 0(), pos s y) -> false(),
                                 greater_int(pos 0(), neg 0()) -> false(),
                                 greater_int(pos 0(), neg s y) -> true(),
                                 greater_int(pos s x, pos 0()) -> true(),
                                 greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
                                 greater_int(pos s x, neg 0()) -> true(),
                                 greater_int(pos s x, neg s y) -> true(),
                                 greater_int(neg 0(), pos 0()) -> false(),
                                 greater_int(neg 0(), pos s y) -> false(),
                                 greater_int(neg 0(), neg 0()) -> false(),
                                 greater_int(neg 0(), neg s y) -> true(),
                                 greater_int(neg s x, pos 0()) -> false(),
                                 greater_int(neg s x, pos s y) -> false(),
                                 greater_int(neg s x, neg 0()) -> false(),
                                 greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
                  eval_51(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_511(greater_int(i, n), n, i, j, k, l, t, h, m, p, q, r, up),
                  eval_51(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_51(lesseq_int(i, n), n, i, j, k, l, t, h, m, p, q, r, up),
                  eval_52(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_53(n, i, j, k, l, t, h, m, p, q, r, up),
     Cond_eval_51(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_52(n, i, j, k, l, t, h, m, p, q, r, up),
                   eval_5(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_5(not up, n, i, j, k, l, t, h, m, p, q, r, up),
                   eval_5(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_52(up, n, i, j, k, l, t, h, m, p, q, r, up),
                   eval_4(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_5(n, i, j, k, l, t, h, n, p, q, r, up),
     Cond_eval_33(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_38(n, i, j, k, l, t, h, m, p, q, r, up),
                                    lesseq_int(pos x, neg s y) -> false(),
                                    lesseq_int(pos 0(), pos y) -> true(),
                                  lesseq_int(pos 0(), neg 0()) -> true(),
                                  lesseq_int(pos s x, pos 0()) -> false(),
                                  lesseq_int(pos s x, pos s y) -> lesseq_int(pos x, pos y),
                                    lesseq_int(pos s x, neg y) -> false(),
                                      lesseq_int(neg x, pos y) -> true(),
                                    lesseq_int(neg x, neg 0()) -> true(),
                                  lesseq_int(neg 0(), neg s y) -> false(),
                                  lesseq_int(neg s x, neg s y) -> lesseq_int(neg x, neg y),
                  eval_33(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_33(lesseq_int(r, pos 0()), n, i, j, k, l, t, h, m, p, q, r, up),
                  eval_33(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_331(greater_int(r, pos 0()), n, i, j, k, l, t, h, m, p, q, r, up),
    Cond_eval_381(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_39(n, i, j, k, l, t, h, m, p, q, r, up),
                  eval_38(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_381(greater_int(q, pos 0()), n, i, j, k, l, t, h, m, p, q, r, up),
                  eval_38(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_38(lesseq_int(q, pos 0()), n, i, j, k, l, t, h, m, p, q, r, up),
                  eval_32(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_23(n, i, j, k, l, t, h, m, p, q, minus_int(r, pos s 0()), up),
                                       minus_int(pos x, pos y) -> minus_nat(x, y),
                                       minus_int(pos x, neg y) -> pos plus_nat(x, y),
                                       minus_int(neg x, pos y) -> neg plus_nat(x, y),
                                       minus_int(neg x, neg y) -> minus_nat(y, x),
                  eval_31(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_32(n, i, minus_int(j, pos s 0()), k, l, t, h, m, p, q, r, up),
    Cond_eval_231(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_24(n, i, j, k, l, t, h, m, p, q, r, up),
                                           and(true(), true()) -> true(),
                                          and(true(), false()) -> false(),
                                          and(false(), true()) -> false(),
                                         and(false(), false()) -> false(),
                  eval_23(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_231(and(greater_int(q, pos 0()), greater_int(r, pos 0())), n, i, j, k, l, t, h, m, p, q, r, up),
                  eval_23(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_23(or(lesseq_int(q, pos 0()), lesseq_int(r, pos 0())), n, i, j, k, l, t, h, m, p, q, r, up),
                  eval_19(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_191(less_int(m, p), n, i, j, k, l, t, h, m, p, q, r, up),
                  eval_19(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_19(greatereq_int(m, p), n, i, j, k, l, t, h, m, p, q, r, up),
                  eval_18(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_19(n, i, j, k, l, t, h, minus_int(m, q), p, q, r, up),
                  eval_13(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_14(n, i, mult_int(pos s s 0(), n), k, l, t, h, m, p, q, r, up),
                                        plus_int(pos x, pos y) -> pos plus_nat(x, y),
                                        plus_int(pos x, neg y) -> minus_nat(x, y),
                                        plus_int(neg x, pos y) -> minus_nat(y, x),
                                        plus_int(neg x, neg y) -> neg plus_nat(x, y),
                  eval_12(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_13(n, plus_int(pos s 0(), n), j, k, l, t, h, m, p, q, r, up),
                  eval_50(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_51(n, pos s 0(), j, k, l, t, h, m, p, q, r, up),
     Cond_eval_49(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_50(n, i, j, k, l, t, h, m, p, q, r, up),
                  eval_41(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_42(n, plus_int(pos s 0(), i), j, k, l, t, h, m, p, q, r, up),
                  eval_40(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_41(n, i, j, plus_int(k, h), l, t, h, m, p, q, r, up),
      Cond_eval_0(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_1(n, i, j, k, l, t, h, m, p, q, r, true()),
                   eval_0(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_0(greater_int(n, pos 0()), n, i, j, k, l, t, h, m, p, q, r, up),
    Cond_eval_461(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_14(n, i, j, k, l, t, h, m, p, q, r, up),
                  eval_46(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_461(greater_int(m, pos 0()), n, i, j, k, l, t, h, m, p, q, r, up),
                  eval_46(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_46(lesseq_int(m, pos 0()), n, i, j, k, l, t, h, m, p, q, r, up),
                  eval_22(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_23(n, i, j, k, l, t, h, minus_int(m, r), p, q, r, up),
                  eval_21(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_22(n, i, j, k, l, t, h, m, p, q, m, up),
                  eval_14(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_15(n, i, j, k, l, t, h, m, p, q, r, up),
                                        mult_int(pos x, pos y) -> pos mult_nat(x, y),
                                        mult_int(pos x, neg y) -> neg mult_nat(x, y),
                                        mult_int(neg x, pos y) -> neg mult_nat(x, y),
                                        mult_int(neg x, neg y) -> pos mult_nat(x, y),
                  eval_10(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_11(n, i, j, pos s 0(), l, t, h, m, p, q, r, up),
      Cond_eval_5(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_10(n, i, j, k, l, t, h, m, p, q, r, up),
                   eval_3(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_4(n, i, j, k, l, t, pos s 0(), m, p, q, r, up),
                   eval_2(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_3(n, i, j, k, l, t, h, m, p, q, r, up),
    Cond_eval_191(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_21(n, i, j, k, l, t, h, m, p, q, r, up),
                                    less_int(pos 0(), pos 0()) -> false(),
                                    less_int(pos 0(), pos s y) -> true(),
                                    less_int(pos 0(), neg 0()) -> false(),
                                    less_int(pos 0(), neg s y) -> false(),
                                    less_int(pos s x, pos 0()) -> false(),
                                    less_int(pos s x, pos s y) -> less_int(pos x, pos y),
                                    less_int(pos s x, neg 0()) -> false(),
                                    less_int(pos s x, neg s y) -> false(),
                                    less_int(neg 0(), pos 0()) -> false(),
                                    less_int(neg 0(), pos s y) -> true(),
                                    less_int(neg 0(), neg 0()) -> false(),
                                    less_int(neg 0(), neg s y) -> false(),
                                    less_int(neg s x, pos 0()) -> true(),
                                    less_int(neg s x, pos s y) -> true(),
                                    less_int(neg s x, neg 0()) -> true(),
                                    less_int(neg s x, neg s y) -> less_int(neg x, neg y),
    Cond_eval_151(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_17(n, i, j, k, l, t, h, m, p, q, r, up),
                  eval_15(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_151(less_int(m, p), n, i, j, k, l, t, h, m, p, q, r, up),
                  eval_15(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_15(greatereq_int(m, p), n, i, j, k, l, t, h, m, p, q, r, up),
                  eval_47(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_48(n, i, j, k, l, t, h, m, p, q, r, not up),
     Cond_eval_46(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_47(n, i, j, k, t, t, h, m, p, q, r, up),
                  eval_53(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_51(n, plus_int(pos s 0(), i), j, k, l, t, h, m, p, q, r, up),
    Cond_eval_491(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_end(n, i, j, k, l, t, h, m, p, q, r, up),
    Cond_eval_481(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_49(n, i, j, k, l, t, h, m, mult_int(pos s s 0(), p), q, r, up),
                                 greatereq_int(pos x, pos 0()) -> true(),
                                   greatereq_int(pos x, neg y) -> true(),
                               greatereq_int(pos 0(), pos s y) -> false(),
                               greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
                                 greatereq_int(neg x, pos s y) -> false(),
                               greatereq_int(neg 0(), pos 0()) -> true(),
                                 greatereq_int(neg 0(), neg y) -> true(),
                               greatereq_int(neg s x, pos 0()) -> false(),
                               greatereq_int(neg s x, neg 0()) -> false(),
                               greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y),
                  eval_48(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_481(greatereq_int(p, n), n, i, j, k, l, t, h, m, p, q, r, up),
                  eval_48(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_48(less_int(p, n), n, i, j, k, l, t, h, m, p, q, r, up),
                  eval_26(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_27(n, i, j, plus_int(k, h), l, t, h, m, p, q, r, up),
                  eval_25(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_26(n, i, j, k, l, t, h, m, p, q, r, up),
                  eval_37(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_33(n, i, j, k, l, t, h, m, p, q, minus_int(r, pos s 0()), up),
                                                    not true() -> false(),
                                                   not false() -> true(),
                  eval_49(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_49(not up, n, i, j, k, l, t, h, m, p, q, r, up),
                  eval_49(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_491(up, n, i, j, k, l, t, h, m, p, q, r, up),
     Cond_eval_23(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_33(n, i, j, k, l, t, h, m, p, q, r, up),
                                            or(true(), true()) -> true(),
                                           or(true(), false()) -> true(),
                                           or(false(), true()) -> true(),
                                          or(false(), false()) -> false(),
                   eval_9(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_14(n, i, j, k, mult_int(pos s s 0(), n), t, h, n, p, q, r, up),
                  eval_30(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_31(n, i, j, plus_int(k, h), l, t, h, m, p, q, r, up),
                  eval_29(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_30(n, i, j, k, l, t, h, m, p, q, r, up),
                  eval_20(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_22(n, i, j, k, l, t, h, m, p, q, p, up),
     Cond_eval_19(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_20(n, i, j, k, l, t, h, m, p, q, r, up),
                  eval_24(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_25(n, i, j, k, l, t, h, m, p, q, r, up),
                  eval_24(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_29(n, i, j, k, l, t, h, m, p, q, r, up),
                  eval_39(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_40(n, i, j, k, l, t, h, m, p, q, r, up),
                  eval_36(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_37(n, i, minus_int(j, pos s 0()), k, l, t, h, m, p, q, r, up),
                  eval_35(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_36(n, i, j, plus_int(k, h), l, t, h, m, p, q, r, up),
                  eval_34(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_35(n, i, j, k, l, t, h, m, p, q, r, up),
    Cond_eval_331(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_34(n, i, j, k, l, t, h, m, p, q, r, up),
                   eval_1(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_2(n, i, j, k, l, t, h, m, pos s 0(), q, r, up),
                  eval_28(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_23(n, i, j, k, l, t, h, m, p, minus_int(q, pos s 0()), r, up),
                  eval_27(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_28(n, plus_int(pos s 0(), i), j, k, l, t, h, m, p, q, r, up),
     Cond_eval_48(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_2(n, i, j, k, l, t, h, m, p, q, r, up),
                   eval_8(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_9(n, i, j, plus_int(pos s 0(), n), l, t, h, n, p, q, r, up),
                  eval_43(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_44(n, i, j, k, l, t, neg_int h, m, p, q, r, up),
     Cond_eval_38(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_43(n, i, j, k, l, t, h, m, p, q, r, up),
                  eval_42(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_38(n, i, j, k, l, t, h, m, p, minus_int(q, pos s 0()), r, up),
                   eval_7(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_8(n, i, n, k, l, t, h, m, p, q, r, up),
                   eval_6(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_7(n, pos s 0(), j, k, l, t, h, m, p, q, r, up),
                  eval_16(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_18(n, i, j, k, l, t, h, m, p, p, r, up),
     Cond_eval_15(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_16(n, i, j, k, l, t, h, m, p, q, r, up),
                  eval_44(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_45(n, i, j, k, l, k, h, m, p, q, r, up),
                                                 neg_int pos x -> neg x,
                                                 neg_int neg x -> pos x,
                  eval_11(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_12(n, i, j, k, n, t, h, m, p, q, r, up),
                  eval_45(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_46(n, i, j, l, l, t, h, m, p, q, r, up),
     Cond_eval_52(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_6(n, i, j, k, l, t, h, m, p, q, r, up),
                  eval_17(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_18(n, i, j, k, l, t, h, m, p, m, r, up),
                                           minus_nat(0(), 0()) -> pos 0(),
                                           minus_nat(0(), s y) -> neg s y,
                                           minus_nat(s x, 0()) -> pos s x,
                                           minus_nat(s x, s y) -> minus_nat(x, y),
                                              plus_nat(0(), x) -> x,
                                              plus_nat(s x, y) -> s plus_nat(x, y),
                                              mult_nat(0(), y) -> 0(),
                                            mult_nat(s x, 0()) -> 0(),
                                            mult_nat(s x, s y) -> plus_nat(mult_nat(x, s y), s y)
   }
  Fail