Time: 5.177110
TRS:
 {            stNat(true(), n, l) -> cond1(member(n, l), n, l),
    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),
                         st(n, l) -> stNat(greatereq_int(n, pos 0()), n, l),
                           sort l -> st(pos 0(), l),
                if(false(), u, v) -> v,
                 if(true(), u, v) -> u,
             or(false(), false()) -> false(),
              or(false(), true()) -> true(),
              or(true(), false()) -> true(),
               or(true(), true()) -> true(),
      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),
                 member(n, nil()) -> false(),
            member(n, cons(m, l)) -> or(equal_int(n, m), member(n, l)),
    greater_int(pos 0(), pos 0()) -> false(),
    greater_int(pos 0(), pos s y) -> false(),
    greater_int(pos 0(), neg 0()) -> false(),
    greater_int(pos 0(), neg s y) -> true(),
    greater_int(pos s x, pos 0()) -> true(),
    greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
    greater_int(pos s x, neg 0()) -> true(),
    greater_int(pos s x, neg s y) -> true(),
    greater_int(neg 0(), pos 0()) -> false(),
    greater_int(neg 0(), pos s y) -> false(),
    greater_int(neg 0(), neg 0()) -> false(),
    greater_int(neg 0(), neg s y) -> true(),
    greater_int(neg s x, pos 0()) -> false(),
    greater_int(neg s x, pos s y) -> false(),
    greater_int(neg s x, neg 0()) -> false(),
    greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
                        max nil() -> pos 0(),
                   max cons(u, l) -> if(greater_int(u, max l), u, max l),
           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),
             cond1(false(), n, l) -> cond2(greater_int(n, max l), n, l),
              cond1(true(), n, l) -> cons(n, st(plus_int(pos s 0(), n), l)),
             cond2(false(), n, l) -> st(plus_int(pos s 0(), n), l),
              cond2(true(), n, l) -> nil(),
              minus_nat(0(), 0()) -> pos 0(),
              minus_nat(0(), s y) -> neg s y,
              minus_nat(s x, 0()) -> pos s x,
              minus_nat(s x, s y) -> minus_nat(x, y),
                 plus_nat(0(), x) -> x,
                 plus_nat(s x, y) -> s plus_nat(x, y)}
 SRS: We consider a TRS.
  Trs:
   {            stNat(true(), n, l) -> cond1(member(n, l), n, l),
      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),
                           st(n, l) -> stNat(greatereq_int(n, pos 0()), n, l),
                             sort l -> st(pos 0(), l),
                  if(false(), u, v) -> v,
                   if(true(), u, v) -> u,
               or(false(), false()) -> false(),
                or(false(), true()) -> true(),
                or(true(), false()) -> true(),
                 or(true(), true()) -> true(),
        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),
                   member(n, nil()) -> false(),
              member(n, cons(m, l)) -> or(equal_int(n, m), member(n, l)),
      greater_int(pos 0(), pos 0()) -> false(),
      greater_int(pos 0(), pos s y) -> false(),
      greater_int(pos 0(), neg 0()) -> false(),
      greater_int(pos 0(), neg s y) -> true(),
      greater_int(pos s x, pos 0()) -> true(),
      greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
      greater_int(pos s x, neg 0()) -> true(),
      greater_int(pos s x, neg s y) -> true(),
      greater_int(neg 0(), pos 0()) -> false(),
      greater_int(neg 0(), pos s y) -> false(),
      greater_int(neg 0(), neg 0()) -> false(),
      greater_int(neg 0(), neg s y) -> true(),
      greater_int(neg s x, pos 0()) -> false(),
      greater_int(neg s x, pos s y) -> false(),
      greater_int(neg s x, neg 0()) -> false(),
      greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
                          max nil() -> pos 0(),
                     max cons(u, l) -> if(greater_int(u, max l), u, max l),
             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),
               cond1(false(), n, l) -> cond2(greater_int(n, max l), n, l),
                cond1(true(), n, l) -> cons(n, st(plus_int(pos s 0(), n), l)),
               cond2(false(), n, l) -> st(plus_int(pos s 0(), n), l),
                cond2(true(), n, l) -> nil(),
                minus_nat(0(), 0()) -> pos 0(),
                minus_nat(0(), s y) -> neg s y,
                minus_nat(s x, 0()) -> pos s x,
                minus_nat(s x, s y) -> minus_nat(x, y),
                   plus_nat(0(), x) -> x,
                   plus_nat(s x, y) -> s plus_nat(x, y)}
  Fail