Time: 5.164084
TRS:
 {     Cond_eval_21(true(), i, j) -> eval_2(i, plus_int(pos s 0(), j)),
       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_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_2(i, j) -> Cond_eval_21(lesseq_int(j, minus_int(i, pos s 0())), i, j),
                     eval_2(i, j) -> Cond_eval_2(greater_int(j, minus_int(i, pos s 0())), i, j),
                     eval_1(i, j) -> Cond_eval_1(greatereq_int(i, pos 0()), i, j),
        Cond_eval_2(true(), i, j) -> eval_1(minus_int(i, pos s 0()), j),
    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(),
           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),
        Cond_eval_1(true(), i, j) -> eval_2(i, pos 0()),
    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(),
              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:
   {     Cond_eval_21(true(), i, j) -> eval_2(i, plus_int(pos s 0(), j)),
         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_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_2(i, j) -> Cond_eval_21(lesseq_int(j, minus_int(i, pos s 0())), i, j),
                       eval_2(i, j) -> Cond_eval_2(greater_int(j, minus_int(i, pos s 0())), i, j),
                       eval_1(i, j) -> Cond_eval_1(greatereq_int(i, pos 0()), i, j),
          Cond_eval_2(true(), i, j) -> eval_1(minus_int(i, pos s 0()), j),
      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(),
             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),
          Cond_eval_1(true(), i, j) -> eval_2(i, pos 0()),
      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(),
                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