Time: 5.138738
TRS:
 {                cu(true(), x) -> cu(less_int(x, exp(pos s s s s s s s s s s 0(), pos s s 0())), plus_int(pos s 0(), x)),
     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(),
                      exp(x, y) -> if(greater_int(y, pos 0()), x, y),
         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),
               if(true(), x, y) -> mult_int(x, exp(x, minus_int(y, pos s 0()))),
              if(false(), x, y) -> pos s 0(),
  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(),
         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),
        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),
            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:
   {                cu(true(), x) -> cu(less_int(x, exp(pos s s s s s s s s s s 0(), pos s s 0())), plus_int(pos s 0(), x)),
       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(),
                        exp(x, y) -> if(greater_int(y, pos 0()), x, y),
           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),
                 if(true(), x, y) -> mult_int(x, exp(x, minus_int(y, pos s 0()))),
                if(false(), x, y) -> pos s 0(),
    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(),
           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),
          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),
              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