Time: 5.291959
TRS:
 {Cond_eval2(true(), an, bn, cn, i, j) -> eval(an, bn, plus_int(pos s 0(), cn), plus_int(pos s 0(), i), j),
                   and(true(), true()) -> true(),
                  and(true(), false()) -> false(),
                  and(false(), true()) -> false(),
                 and(false(), false()) -> false(),
            less_int(pos s x, pos s y) -> less_int(pos x, pos y),
            less_int(pos s x, pos 0()) -> false(),
            less_int(pos s x, neg s y) -> false(),
            less_int(pos s x, neg 0()) -> false(),
            less_int(pos 0(), pos s y) -> true(),
            less_int(pos 0(), pos 0()) -> false(),
            less_int(pos 0(), neg s y) -> false(),
            less_int(pos 0(), neg 0()) -> false(),
            less_int(neg s x, pos s y) -> true(),
            less_int(neg s x, pos 0()) -> true(),
            less_int(neg s x, neg s y) -> less_int(neg x, neg y),
            less_int(neg s x, neg 0()) -> true(),
            less_int(neg 0(), pos s y) -> true(),
            less_int(neg 0(), pos 0()) -> false(),
            less_int(neg 0(), neg s y) -> false(),
            less_int(neg 0(), neg 0()) -> false(),
                eval(an, bn, cn, i, j) -> Cond_eval2(and(less_int(j, bn), less_int(i, an)), an, bn, cn, i, j),
                eval(an, bn, cn, i, j) -> Cond_eval(and(less_int(j, bn), greatereq_int(i, an)), an, bn, cn, i, j),
                eval(an, bn, cn, i, j) -> Cond_eval1(and(greatereq_int(j, bn), less_int(i, an)), an, bn, cn, i, j),
                eval(an, bn, cn, i, j) -> Cond_eval3(and(less_int(j, bn), less_int(i, an)), an, bn, cn, i, j),
   Cond_eval(true(), an, bn, cn, i, j) -> eval(an, bn, plus_int(pos s 0(), cn), i, plus_int(pos s 0(), j)),
         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(),
  Cond_eval1(true(), an, bn, cn, i, j) -> eval(an, bn, plus_int(pos s 0(), cn), plus_int(pos s 0(), i), j),
  Cond_eval3(true(), an, bn, cn, i, j) -> eval(an, bn, plus_int(pos s 0(), cn), i, plus_int(pos s 0(), j)),
                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_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_eval2(true(), an, bn, cn, i, j) -> eval(an, bn, plus_int(pos s 0(), cn), plus_int(pos s 0(), i), j),
                     and(true(), true()) -> true(),
                    and(true(), false()) -> false(),
                    and(false(), true()) -> false(),
                   and(false(), false()) -> false(),
              less_int(pos s x, pos s y) -> less_int(pos x, pos y),
              less_int(pos s x, pos 0()) -> false(),
              less_int(pos s x, neg s y) -> false(),
              less_int(pos s x, neg 0()) -> false(),
              less_int(pos 0(), pos s y) -> true(),
              less_int(pos 0(), pos 0()) -> false(),
              less_int(pos 0(), neg s y) -> false(),
              less_int(pos 0(), neg 0()) -> false(),
              less_int(neg s x, pos s y) -> true(),
              less_int(neg s x, pos 0()) -> true(),
              less_int(neg s x, neg s y) -> less_int(neg x, neg y),
              less_int(neg s x, neg 0()) -> true(),
              less_int(neg 0(), pos s y) -> true(),
              less_int(neg 0(), pos 0()) -> false(),
              less_int(neg 0(), neg s y) -> false(),
              less_int(neg 0(), neg 0()) -> false(),
                  eval(an, bn, cn, i, j) -> Cond_eval2(and(less_int(j, bn), less_int(i, an)), an, bn, cn, i, j),
                  eval(an, bn, cn, i, j) -> Cond_eval(and(less_int(j, bn), greatereq_int(i, an)), an, bn, cn, i, j),
                  eval(an, bn, cn, i, j) -> Cond_eval1(and(greatereq_int(j, bn), less_int(i, an)), an, bn, cn, i, j),
                  eval(an, bn, cn, i, j) -> Cond_eval3(and(less_int(j, bn), less_int(i, an)), an, bn, cn, i, j),
     Cond_eval(true(), an, bn, cn, i, j) -> eval(an, bn, plus_int(pos s 0(), cn), i, plus_int(pos s 0(), j)),
           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(),
    Cond_eval1(true(), an, bn, cn, i, j) -> eval(an, bn, plus_int(pos s 0(), cn), plus_int(pos s 0(), i), j),
    Cond_eval3(true(), an, bn, cn, i, j) -> eval(an, bn, plus_int(pos s 0(), cn), i, plus_int(pos s 0(), j)),
                  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_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