Time: 5.433701
TRS:
 {               eval(i, j, k) -> Cond_eval(and(lesseq_int(i, pos s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s 0()), lesseq_int(j, k)), i, j, k),
        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),
       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),
    Cond_eval(true(), i, j, k) -> eval(j, plus_int(pos s 0(), i), minus_int(k, pos s 0())),
           and(true(), true()) -> true(),
          and(true(), false()) -> false(),
          and(false(), true()) -> false(),
         and(false(), false()) -> false(),
    lesseq_int(pos x, neg s y) -> false(),
  lesseq_int(pos s x, pos s y) -> lesseq_int(pos x, pos y),
  lesseq_int(pos s x, pos 0()) -> false(),
    lesseq_int(pos s x, neg y) -> false(),
    lesseq_int(pos 0(), pos y) -> true(),
  lesseq_int(pos 0(), neg 0()) -> true(),
      lesseq_int(neg x, pos y) -> true(),
    lesseq_int(neg x, neg 0()) -> true(),
  lesseq_int(neg s x, neg s y) -> lesseq_int(neg x, neg y),
  lesseq_int(neg 0(), neg s y) -> false(),
           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}
 SRS: We consider a TRS.
  Trs:
   {               eval(i, j, k) -> Cond_eval(and(lesseq_int(i, pos s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s 0()), lesseq_int(j, k)), i, j, k),
          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),
         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),
      Cond_eval(true(), i, j, k) -> eval(j, plus_int(pos s 0(), i), minus_int(k, pos s 0())),
             and(true(), true()) -> true(),
            and(true(), false()) -> false(),
            and(false(), true()) -> false(),
           and(false(), false()) -> false(),
      lesseq_int(pos x, neg s y) -> false(),
    lesseq_int(pos s x, pos s y) -> lesseq_int(pos x, pos y),
    lesseq_int(pos s x, pos 0()) -> false(),
      lesseq_int(pos s x, neg y) -> false(),
      lesseq_int(pos 0(), pos y) -> true(),
    lesseq_int(pos 0(), neg 0()) -> true(),
        lesseq_int(neg x, pos y) -> true(),
      lesseq_int(neg x, neg 0()) -> true(),
    lesseq_int(neg s x, neg s y) -> lesseq_int(neg x, neg y),
    lesseq_int(neg 0(), neg s y) -> false(),
             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}
  Fail