Time: 5.150037
TRS:
 {Cond_eval_33(true(), i, j, l, r, n) -> eval_4(i, j, l, r, n),
                  and(true(), true()) -> true(),
                 and(true(), false()) -> false(),
                 and(false(), true()) -> false(),
                and(false(), false()) -> false(),
        greatereq_int(pos x, pos 0()) -> true(),
          greatereq_int(pos x, neg y) -> true(),
      greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
      greatereq_int(pos 0(), pos s y) -> false(),
        greatereq_int(neg x, pos s y) -> false(),
      greatereq_int(neg s x, pos 0()) -> false(),
      greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y),
      greatereq_int(neg s x, neg 0()) -> false(),
      greatereq_int(neg 0(), pos 0()) -> true(),
        greatereq_int(neg 0(), neg y) -> true(),
        greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
        greater_int(pos s x, pos 0()) -> true(),
        greater_int(pos s x, neg s y) -> true(),
        greater_int(pos s x, neg 0()) -> true(),
        greater_int(pos 0(), pos s y) -> false(),
        greater_int(pos 0(), pos 0()) -> false(),
        greater_int(pos 0(), neg s y) -> true(),
        greater_int(pos 0(), neg 0()) -> false(),
        greater_int(neg s x, pos s y) -> false(),
        greater_int(neg s x, pos 0()) -> false(),
        greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
        greater_int(neg s x, neg 0()) -> false(),
        greater_int(neg 0(), pos s y) -> false(),
        greater_int(neg 0(), pos 0()) -> false(),
        greater_int(neg 0(), neg s y) -> true(),
        greater_int(neg 0(), neg 0()) -> false(),
              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_3(i, j, l, r, n) -> Cond_eval_33(and(greatereq_int(r, j), greater_int(j, minus_int(r, pos s 0()))), i, j, l, r, n),
                eval_3(i, j, l, r, n) -> Cond_eval_3(and(and(greatereq_int(r, j), greatereq_int(minus_int(r, pos s 0()), j)), greatereq_int(j, pos s 0())), i, j, l, r, n),
                eval_3(i, j, l, r, n) -> Cond_eval_34(and(greatereq_int(r, j), greatereq_int(minus_int(r, pos s 0()), j)), i, j, l, r, n),
                eval_3(i, j, l, r, n) -> Cond_eval_31(and(and(greatereq_int(r, j), greatereq_int(minus_int(r, pos s 0()), j)), greatereq_int(j, pos s 0())), i, j, l, r, n),
                eval_3(i, j, l, r, n) -> Cond_eval_35(and(greatereq_int(r, j), greatereq_int(minus_int(r, pos s 0()), j)), i, j, l, r, n),
                eval_3(i, j, l, r, n) -> Cond_eval_32(and(and(greatereq_int(r, j), greater_int(j, minus_int(r, pos s 0()))), greatereq_int(j, pos s 0())), i, j, l, r, n),
   Cond_eval_3(true(), i, j, l, r, n) -> eval_3(plus_int(pos s 0(), j), plus_int(pos s s 0(), mult_int(pos s s 0(), j)), l, r, n),
   Cond_eval_4(true(), i, j, l, r, n) -> eval_2(i, j, minus_int(l, pos s 0()), r, n),
                eval_4(i, j, l, r, n) -> Cond_eval_4(and(and(greatereq_int(l, pos s s 0()), greatereq_int(l, pos s 0())), greatereq_int(r, pos s s 0())), i, j, l, r, n),
                eval_4(i, j, l, r, n) -> Cond_eval_41(and(and(greater_int(pos s s 0(), l), greatereq_int(l, pos s 0())), greatereq_int(r, pos s s 0())), i, j, l, r, n),
               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),
               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),
  Cond_eval_34(true(), i, j, l, r, n) -> eval_4(i, plus_int(pos s 0(), j), l, r, n),
                eval_2(i, j, l, r, n) -> Cond_eval_2(greatereq_int(r, pos s s 0()), i, j, l, r, n),
  Cond_eval_41(true(), i, j, l, r, n) -> eval_2(i, j, l, minus_int(r, pos s 0()), n),
  Cond_eval_31(true(), i, j, l, r, n) -> eval_3(j, mult_int(pos s s 0(), j), l, r, n),
  Cond_eval_35(true(), i, j, l, r, n) -> eval_4(i, j, l, r, n),
  Cond_eval_32(true(), i, j, l, r, n) -> eval_3(j, mult_int(pos s s 0(), j), l, r, n),
   Cond_eval_1(true(), i, j, l, r, n) -> eval_2(i, j, minus_int(l, pos s 0()), r, n),
                eval_1(i, j, l, r, n) -> Cond_eval_1(greatereq_int(l, pos s s 0()), i, j, l, r, n),
                eval_1(i, j, l, r, n) -> Cond_eval_11(greater_int(pos s s 0(), l), i, j, l, r, n),
   Cond_eval_2(true(), i, j, l, r, n) -> eval_3(l, mult_int(pos s s 0(), l), l, r, n),
  Cond_eval_11(true(), i, j, l, r, n) -> eval_2(i, j, l, minus_int(r, pos s 0()), n),
                  minus_nat(s x, s y) -> minus_nat(x, y),
                  minus_nat(s x, 0()) -> pos s x,
                  minus_nat(0(), s y) -> neg s y,
                  minus_nat(0(), 0()) -> pos 0(),
                     plus_nat(s x, y) -> s plus_nat(x, y),
                     plus_nat(0(), x) -> x,
                   mult_nat(s x, s y) -> plus_nat(mult_nat(x, s y), s y),
                   mult_nat(s x, 0()) -> 0(),
                     mult_nat(0(), y) -> 0()}
 SRS: We consider a TRS.
  Trs:
   {Cond_eval_33(true(), i, j, l, r, n) -> eval_4(i, j, l, r, n),
                    and(true(), true()) -> true(),
                   and(true(), false()) -> false(),
                   and(false(), true()) -> false(),
                  and(false(), false()) -> false(),
          greatereq_int(pos x, pos 0()) -> true(),
            greatereq_int(pos x, neg y) -> true(),
        greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
        greatereq_int(pos 0(), pos s y) -> false(),
          greatereq_int(neg x, pos s y) -> false(),
        greatereq_int(neg s x, pos 0()) -> false(),
        greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y),
        greatereq_int(neg s x, neg 0()) -> false(),
        greatereq_int(neg 0(), pos 0()) -> true(),
          greatereq_int(neg 0(), neg y) -> true(),
          greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
          greater_int(pos s x, pos 0()) -> true(),
          greater_int(pos s x, neg s y) -> true(),
          greater_int(pos s x, neg 0()) -> true(),
          greater_int(pos 0(), pos s y) -> false(),
          greater_int(pos 0(), pos 0()) -> false(),
          greater_int(pos 0(), neg s y) -> true(),
          greater_int(pos 0(), neg 0()) -> false(),
          greater_int(neg s x, pos s y) -> false(),
          greater_int(neg s x, pos 0()) -> false(),
          greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
          greater_int(neg s x, neg 0()) -> false(),
          greater_int(neg 0(), pos s y) -> false(),
          greater_int(neg 0(), pos 0()) -> false(),
          greater_int(neg 0(), neg s y) -> true(),
          greater_int(neg 0(), neg 0()) -> false(),
                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_3(i, j, l, r, n) -> Cond_eval_33(and(greatereq_int(r, j), greater_int(j, minus_int(r, pos s 0()))), i, j, l, r, n),
                  eval_3(i, j, l, r, n) -> Cond_eval_3(and(and(greatereq_int(r, j), greatereq_int(minus_int(r, pos s 0()), j)), greatereq_int(j, pos s 0())), i, j, l, r, n),
                  eval_3(i, j, l, r, n) -> Cond_eval_34(and(greatereq_int(r, j), greatereq_int(minus_int(r, pos s 0()), j)), i, j, l, r, n),
                  eval_3(i, j, l, r, n) -> Cond_eval_31(and(and(greatereq_int(r, j), greatereq_int(minus_int(r, pos s 0()), j)), greatereq_int(j, pos s 0())), i, j, l, r, n),
                  eval_3(i, j, l, r, n) -> Cond_eval_35(and(greatereq_int(r, j), greatereq_int(minus_int(r, pos s 0()), j)), i, j, l, r, n),
                  eval_3(i, j, l, r, n) -> Cond_eval_32(and(and(greatereq_int(r, j), greater_int(j, minus_int(r, pos s 0()))), greatereq_int(j, pos s 0())), i, j, l, r, n),
     Cond_eval_3(true(), i, j, l, r, n) -> eval_3(plus_int(pos s 0(), j), plus_int(pos s s 0(), mult_int(pos s s 0(), j)), l, r, n),
     Cond_eval_4(true(), i, j, l, r, n) -> eval_2(i, j, minus_int(l, pos s 0()), r, n),
                  eval_4(i, j, l, r, n) -> Cond_eval_4(and(and(greatereq_int(l, pos s s 0()), greatereq_int(l, pos s 0())), greatereq_int(r, pos s s 0())), i, j, l, r, n),
                  eval_4(i, j, l, r, n) -> Cond_eval_41(and(and(greater_int(pos s s 0(), l), greatereq_int(l, pos s 0())), greatereq_int(r, pos s s 0())), i, j, l, r, n),
                 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),
                 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),
    Cond_eval_34(true(), i, j, l, r, n) -> eval_4(i, plus_int(pos s 0(), j), l, r, n),
                  eval_2(i, j, l, r, n) -> Cond_eval_2(greatereq_int(r, pos s s 0()), i, j, l, r, n),
    Cond_eval_41(true(), i, j, l, r, n) -> eval_2(i, j, l, minus_int(r, pos s 0()), n),
    Cond_eval_31(true(), i, j, l, r, n) -> eval_3(j, mult_int(pos s s 0(), j), l, r, n),
    Cond_eval_35(true(), i, j, l, r, n) -> eval_4(i, j, l, r, n),
    Cond_eval_32(true(), i, j, l, r, n) -> eval_3(j, mult_int(pos s s 0(), j), l, r, n),
     Cond_eval_1(true(), i, j, l, r, n) -> eval_2(i, j, minus_int(l, pos s 0()), r, n),
                  eval_1(i, j, l, r, n) -> Cond_eval_1(greatereq_int(l, pos s s 0()), i, j, l, r, n),
                  eval_1(i, j, l, r, n) -> Cond_eval_11(greater_int(pos s s 0(), l), i, j, l, r, n),
     Cond_eval_2(true(), i, j, l, r, n) -> eval_3(l, mult_int(pos s s 0(), l), l, r, n),
    Cond_eval_11(true(), i, j, l, r, n) -> eval_2(i, j, l, minus_int(r, pos s 0()), n),
                    minus_nat(s x, s y) -> minus_nat(x, y),
                    minus_nat(s x, 0()) -> pos s x,
                    minus_nat(0(), s y) -> neg s y,
                    minus_nat(0(), 0()) -> pos 0(),
                       plus_nat(s x, y) -> s plus_nat(x, y),
                       plus_nat(0(), x) -> x,
                     mult_nat(s x, s y) -> plus_nat(mult_nat(x, s y), s y),
                     mult_nat(s x, 0()) -> 0(),
                       mult_nat(0(), y) -> 0()}
  Fail