Time: 5.068087
TRS:
 {     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(x, x) -> pos 0(),
                  minus(x, y) -> cond(equal_int(min(x, y), y), x, y),
           cond(true(), x, y) -> plus_int(pos s 0(), minus(x, plus_int(pos s 0(), y))),
             if(true(), u, v) -> u,
            if(false(), u, v) -> v,
   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(),
                    min(u, v) -> if(less_int(u, v), u, v),
  equal_int(pos s x, pos s y) -> equal_int(pos x, pos y),
  equal_int(pos s x, pos 0()) -> false(),
  equal_int(pos s x, neg s y) -> false(),
  equal_int(pos s x, neg 0()) -> false(),
  equal_int(pos 0(), pos s y) -> false(),
  equal_int(pos 0(), pos 0()) -> true(),
  equal_int(pos 0(), neg s y) -> false(),
  equal_int(pos 0(), neg 0()) -> true(),
  equal_int(neg s x, pos s y) -> false(),
  equal_int(neg s x, pos 0()) -> false(),
  equal_int(neg s x, neg s y) -> equal_int(neg x, neg y),
  equal_int(neg s x, neg 0()) -> false(),
  equal_int(neg 0(), pos s y) -> false(),
  equal_int(neg 0(), pos 0()) -> true(),
  equal_int(neg 0(), neg s y) -> false(),
  equal_int(neg 0(), neg 0()) -> 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:
   {     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(x, x) -> pos 0(),
                    minus(x, y) -> cond(equal_int(min(x, y), y), x, y),
             cond(true(), x, y) -> plus_int(pos s 0(), minus(x, plus_int(pos s 0(), y))),
               if(true(), u, v) -> u,
              if(false(), u, v) -> v,
     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(),
                      min(u, v) -> if(less_int(u, v), u, v),
    equal_int(pos s x, pos s y) -> equal_int(pos x, pos y),
    equal_int(pos s x, pos 0()) -> false(),
    equal_int(pos s x, neg s y) -> false(),
    equal_int(pos s x, neg 0()) -> false(),
    equal_int(pos 0(), pos s y) -> false(),
    equal_int(pos 0(), pos 0()) -> true(),
    equal_int(pos 0(), neg s y) -> false(),
    equal_int(pos 0(), neg 0()) -> true(),
    equal_int(neg s x, pos s y) -> false(),
    equal_int(neg s x, pos 0()) -> false(),
    equal_int(neg s x, neg s y) -> equal_int(neg x, neg y),
    equal_int(neg s x, neg 0()) -> false(),
    equal_int(neg 0(), pos s y) -> false(),
    equal_int(neg 0(), pos 0()) -> true(),
    equal_int(neg 0(), neg s y) -> false(),
    equal_int(neg 0(), neg 0()) -> 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