Time: 5.088168
TRS:
 {                  del(x, nil()) -> nil(),
              del(x, cons(y, xs)) -> if2(equal_int(x, y), x, y, xs),
           if2(false(), x, y, xs) -> cons(y, del(x, xs)),
            if2(true(), x, y, xs) -> xs,
                        max nil() -> pos 0(),
               max cons(x, nil()) -> x,
         max cons(x, cons(y, xs)) -> if1(greatereq_int(x, y), x, y, xs),
                       sort nil() -> nil(),
                 sort cons(x, xs) -> cons(max cons(x, xs), sort del(max cons(x, xs), cons(x, xs))),
           if1(false(), x, y, xs) -> max cons(y, xs),
            if1(true(), x, y, xs) -> max cons(x, xs),
    greatereq_int(pos x, pos 0()) -> true(),
      greatereq_int(pos x, neg y) -> true(),
  greatereq_int(pos 0(), pos s y) -> false(),
  greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
    greatereq_int(neg x, pos s y) -> false(),
  greatereq_int(neg 0(), pos 0()) -> true(),
    greatereq_int(neg 0(), neg y) -> true(),
  greatereq_int(neg s x, pos 0()) -> false(),
  greatereq_int(neg s x, neg 0()) -> false(),
  greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y),
      equal_int(pos 0(), pos 0()) -> true(),
      equal_int(pos 0(), pos s y) -> false(),
      equal_int(pos 0(), neg 0()) -> true(),
      equal_int(pos 0(), neg s y) -> false(),
      equal_int(pos s x, pos 0()) -> false(),
      equal_int(pos s x, pos s y) -> equal_int(pos x, pos y),
      equal_int(pos s x, neg 0()) -> false(),
      equal_int(pos s x, neg s y) -> false(),
      equal_int(neg 0(), pos 0()) -> true(),
      equal_int(neg 0(), pos s y) -> false(),
      equal_int(neg 0(), neg 0()) -> true(),
      equal_int(neg 0(), neg s y) -> false(),
      equal_int(neg s x, pos 0()) -> false(),
      equal_int(neg s x, pos s y) -> false(),
      equal_int(neg s x, neg 0()) -> false(),
      equal_int(neg s x, neg s y) -> equal_int(neg x, neg y)}
 SRS: We consider a TRS.
  Trs:
   {                  del(x, nil()) -> nil(),
                del(x, cons(y, xs)) -> if2(equal_int(x, y), x, y, xs),
             if2(false(), x, y, xs) -> cons(y, del(x, xs)),
              if2(true(), x, y, xs) -> xs,
                          max nil() -> pos 0(),
                 max cons(x, nil()) -> x,
           max cons(x, cons(y, xs)) -> if1(greatereq_int(x, y), x, y, xs),
                         sort nil() -> nil(),
                   sort cons(x, xs) -> cons(max cons(x, xs), sort del(max cons(x, xs), cons(x, xs))),
             if1(false(), x, y, xs) -> max cons(y, xs),
              if1(true(), x, y, xs) -> max cons(x, xs),
      greatereq_int(pos x, pos 0()) -> true(),
        greatereq_int(pos x, neg y) -> true(),
    greatereq_int(pos 0(), pos s y) -> false(),
    greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
      greatereq_int(neg x, pos s y) -> false(),
    greatereq_int(neg 0(), pos 0()) -> true(),
      greatereq_int(neg 0(), neg y) -> true(),
    greatereq_int(neg s x, pos 0()) -> false(),
    greatereq_int(neg s x, neg 0()) -> false(),
    greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y),
        equal_int(pos 0(), pos 0()) -> true(),
        equal_int(pos 0(), pos s y) -> false(),
        equal_int(pos 0(), neg 0()) -> true(),
        equal_int(pos 0(), neg s y) -> false(),
        equal_int(pos s x, pos 0()) -> false(),
        equal_int(pos s x, pos s y) -> equal_int(pos x, pos y),
        equal_int(pos s x, neg 0()) -> false(),
        equal_int(pos s x, neg s y) -> false(),
        equal_int(neg 0(), pos 0()) -> true(),
        equal_int(neg 0(), pos s y) -> false(),
        equal_int(neg 0(), neg 0()) -> true(),
        equal_int(neg 0(), neg s y) -> false(),
        equal_int(neg s x, pos 0()) -> false(),
        equal_int(neg s x, pos s y) -> false(),
        equal_int(neg s x, neg 0()) -> false(),
        equal_int(neg s x, neg s y) -> equal_int(neg x, neg y)}
  Fail