MAYBE
Time: 0.032577
TRS:
 {                  minus(x, 0()) -> x,
            minus(minus(x, y), z) -> minus(x, plus(y, z)),
                  minus(s x, s y) -> minus(x, y),
                   quot(0(), s y) -> 0(),
                   quot(s x, s y) -> s quot(minus(x, y), s y),
                     plus(0(), y) -> y,
                     plus(s x, x) -> plus(if(gt(x, x), id x, id x), s x),
                     plus(s x, y) -> s plus(x, y),
                   plus(s x, s y) -> s s plus(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)),
                  plus(id x, s y) -> s plus(x, if(gt(s y, y), y, s y)),
                  plus(zero(), y) -> y,
                    app(l, nil()) -> l,
                    app(nil(), k) -> k,
               app(cons(x, l), k) -> cons(x, app(l, k)),
  sum app(l, cons(x, cons(y, k))) -> sum app(l, sum cons(x, cons(y, k))),
               sum cons(x, nil()) -> cons(x, nil()),
          sum cons(x, cons(y, l)) -> sum cons(plus(x, y), l),
                 if(true(), x, y) -> x,
                if(false(), x, y) -> y,
                     gt(s x, s y) -> gt(x, y),
                  gt(s x, zero()) -> true(),
                    gt(zero(), y) -> false(),
                            not x -> if(x, false(), true()),
                             id x -> x}
 DP:
  DP:
   {          minus#(minus(x, y), z) -> minus#(x, plus(y, z)),
              minus#(minus(x, y), z) -> plus#(y, z),
                    minus#(s x, s y) -> minus#(x, y),
                     quot#(s x, s y) -> minus#(x, y),
                     quot#(s x, s y) -> quot#(minus(x, y), s y),
                       plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x),
                       plus#(s x, x) -> if#(gt(x, x), id x, id x),
                       plus#(s x, x) -> gt#(x, x),
                       plus#(s x, x) -> id# x,
                       plus#(s x, y) -> plus#(x, y),
                     plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)),
                     plus#(s x, s y) -> if#(gt(x, y), x, y),
                     plus#(s x, s y) -> if#(not gt(x, y), id x, id y),
                     plus#(s x, s y) -> gt#(x, y),
                     plus#(s x, s y) -> not# gt(x, y),
                     plus#(s x, s y) -> id# x,
                     plus#(s x, s y) -> id# y,
                    plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)),
                    plus#(id x, s y) -> if#(gt(s y, y), y, s y),
                    plus#(id x, s y) -> gt#(s y, y),
                 app#(cons(x, l), k) -> app#(l, k),
    sum# app(l, cons(x, cons(y, k))) -> app#(l, sum cons(x, cons(y, k))),
    sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k))),
    sum# app(l, cons(x, cons(y, k))) -> sum# cons(x, cons(y, k)),
            sum# cons(x, cons(y, l)) -> plus#(x, y),
            sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l),
                       gt#(s x, s y) -> gt#(x, y),
                              not# x -> if#(x, false(), true())}
  TRS:
  {                  minus(x, 0()) -> x,
             minus(minus(x, y), z) -> minus(x, plus(y, z)),
                   minus(s x, s y) -> minus(x, y),
                    quot(0(), s y) -> 0(),
                    quot(s x, s y) -> s quot(minus(x, y), s y),
                      plus(0(), y) -> y,
                      plus(s x, x) -> plus(if(gt(x, x), id x, id x), s x),
                      plus(s x, y) -> s plus(x, y),
                    plus(s x, s y) -> s s plus(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)),
                   plus(id x, s y) -> s plus(x, if(gt(s y, y), y, s y)),
                   plus(zero(), y) -> y,
                     app(l, nil()) -> l,
                     app(nil(), k) -> k,
                app(cons(x, l), k) -> cons(x, app(l, k)),
   sum app(l, cons(x, cons(y, k))) -> sum app(l, sum cons(x, cons(y, k))),
                sum cons(x, nil()) -> cons(x, nil()),
           sum cons(x, cons(y, l)) -> sum cons(plus(x, y), l),
                  if(true(), x, y) -> x,
                 if(false(), x, y) -> y,
                      gt(s x, s y) -> gt(x, y),
                   gt(s x, zero()) -> true(),
                     gt(zero(), y) -> false(),
                             not x -> if(x, false(), true()),
                              id x -> x}
  UR:
   {          minus(x, 0()) -> x,
      minus(minus(x, y), z) -> minus(x, plus(y, z)),
            minus(s x, s y) -> minus(x, y),
               plus(0(), y) -> y,
               plus(s x, x) -> plus(if(gt(x, x), id x, id x), s x),
               plus(s x, y) -> s plus(x, y),
             plus(s x, s y) -> s s plus(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)),
            plus(id x, s y) -> s plus(x, if(gt(s y, y), y, s y)),
            plus(zero(), y) -> y,
              app(l, nil()) -> l,
              app(nil(), k) -> k,
         app(cons(x, l), k) -> cons(x, app(l, k)),
         sum cons(x, nil()) -> cons(x, nil()),
    sum cons(x, cons(y, l)) -> sum cons(plus(x, y), l),
           if(true(), x, y) -> x,
          if(false(), x, y) -> y,
               gt(s x, s y) -> gt(x, y),
            gt(s x, zero()) -> true(),
              gt(zero(), y) -> false(),
                      not x -> if(x, false(), true()),
                       id x -> x,
                    a(w, v) -> w,
                    a(w, v) -> v}
   EDG:
    {
     (sum# app(l, cons(x, cons(y, k))) -> app#(l, sum cons(x, cons(y, k))), app#(cons(x, l), k) -> app#(l, k))
     (quot#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
     (quot#(s x, s y) -> minus#(x, y), minus#(minus(x, y), z) -> plus#(y, z))
     (quot#(s x, s y) -> minus#(x, y), minus#(minus(x, y), z) -> minus#(x, plus(y, z)))
     (plus#(s x, s y) -> gt#(x, y), gt#(s x, s y) -> gt#(x, y))
     (sum# cons(x, cons(y, l)) -> plus#(x, y), plus#(id x, s y) -> gt#(s y, y))
     (sum# cons(x, cons(y, l)) -> plus#(x, y), plus#(id x, s y) -> if#(gt(s y, y), y, s y))
     (sum# cons(x, cons(y, l)) -> plus#(x, y), plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)))
     (sum# cons(x, cons(y, l)) -> plus#(x, y), plus#(s x, s y) -> id# y)
     (sum# cons(x, cons(y, l)) -> plus#(x, y), plus#(s x, s y) -> id# x)
     (sum# cons(x, cons(y, l)) -> plus#(x, y), plus#(s x, s y) -> not# gt(x, y))
     (sum# cons(x, cons(y, l)) -> plus#(x, y), plus#(s x, s y) -> gt#(x, y))
     (sum# cons(x, cons(y, l)) -> plus#(x, y), plus#(s x, s y) -> if#(not gt(x, y), id x, id y))
     (sum# cons(x, cons(y, l)) -> plus#(x, y), plus#(s x, s y) -> if#(gt(x, y), x, y))
     (sum# cons(x, cons(y, l)) -> plus#(x, y), plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)))
     (sum# cons(x, cons(y, l)) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))
     (sum# cons(x, cons(y, l)) -> plus#(x, y), plus#(s x, x) -> id# x)
     (sum# cons(x, cons(y, l)) -> plus#(x, y), plus#(s x, x) -> gt#(x, x))
     (sum# cons(x, cons(y, l)) -> plus#(x, y), plus#(s x, x) -> if#(gt(x, x), id x, id x))
     (sum# cons(x, cons(y, l)) -> plus#(x, y), plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x))
     (plus#(s x, s y) -> not# gt(x, y), not# x -> if#(x, false(), true()))
     (sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k))), sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l))
     (sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k))), sum# cons(x, cons(y, l)) -> plus#(x, y))
     (sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k))), sum# app(l, cons(x, cons(y, k))) -> sum# cons(x, cons(y, k)))
     (sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k))), sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k))))
     (sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k))), sum# app(l, cons(x, cons(y, k))) -> app#(l, sum cons(x, cons(y, k))))
     (plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)), plus#(id x, s y) -> gt#(s y, y))
     (plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)), plus#(id x, s y) -> if#(gt(s y, y), y, s y))
     (plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)), plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)))
     (plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)), plus#(s x, s y) -> id# y)
     (plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)), plus#(s x, s y) -> id# x)
     (plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)), plus#(s x, s y) -> not# gt(x, y))
     (plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)), plus#(s x, s y) -> gt#(x, y))
     (plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)), plus#(s x, s y) -> if#(not gt(x, y), id x, id y))
     (plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)), plus#(s x, s y) -> if#(gt(x, y), x, y))
     (plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)), plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)))
     (plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)), plus#(s x, y) -> plus#(x, y))
     (plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)), plus#(s x, x) -> id# x)
     (plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)), plus#(s x, x) -> gt#(x, x))
     (plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)), plus#(s x, x) -> if#(gt(x, x), id x, id x))
     (plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)), plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x))
     (plus#(s x, x) -> gt#(x, x), gt#(s x, s y) -> gt#(x, y))
     (plus#(id x, s y) -> gt#(s y, y), gt#(s x, s y) -> gt#(x, y))
     (plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x), plus#(id x, s y) -> gt#(s y, y))
     (plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x), plus#(id x, s y) -> if#(gt(s y, y), y, s y))
     (plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x), plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)))
     (plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x), plus#(s x, s y) -> id# y)
     (plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x), plus#(s x, s y) -> id# x)
     (plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x), plus#(s x, s y) -> not# gt(x, y))
     (plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x), plus#(s x, s y) -> gt#(x, y))
     (plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x), plus#(s x, s y) -> if#(not gt(x, y), id x, id y))
     (plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x), plus#(s x, s y) -> if#(gt(x, y), x, y))
     (plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x), plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)))
     (plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x), plus#(s x, y) -> plus#(x, y))
     (plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x), plus#(s x, x) -> id# x)
     (plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x), plus#(s x, x) -> gt#(x, x))
     (plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x), plus#(s x, x) -> if#(gt(x, x), id x, id x))
     (plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x), plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x))
     (quot#(s x, s y) -> quot#(minus(x, y), s y), quot#(s x, s y) -> minus#(x, y))
     (quot#(s x, s y) -> quot#(minus(x, y), s y), quot#(s x, s y) -> quot#(minus(x, y), s y))
     (minus#(minus(x, y), z) -> plus#(y, z), plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x))
     (minus#(minus(x, y), z) -> plus#(y, z), plus#(s x, x) -> if#(gt(x, x), id x, id x))
     (minus#(minus(x, y), z) -> plus#(y, z), plus#(s x, x) -> gt#(x, x))
     (minus#(minus(x, y), z) -> plus#(y, z), plus#(s x, x) -> id# x)
     (minus#(minus(x, y), z) -> plus#(y, z), plus#(s x, y) -> plus#(x, y))
     (minus#(minus(x, y), z) -> plus#(y, z), plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)))
     (minus#(minus(x, y), z) -> plus#(y, z), plus#(s x, s y) -> if#(gt(x, y), x, y))
     (minus#(minus(x, y), z) -> plus#(y, z), plus#(s x, s y) -> if#(not gt(x, y), id x, id y))
     (minus#(minus(x, y), z) -> plus#(y, z), plus#(s x, s y) -> gt#(x, y))
     (minus#(minus(x, y), z) -> plus#(y, z), plus#(s x, s y) -> not# gt(x, y))
     (minus#(minus(x, y), z) -> plus#(y, z), plus#(s x, s y) -> id# x)
     (minus#(minus(x, y), z) -> plus#(y, z), plus#(s x, s y) -> id# y)
     (minus#(minus(x, y), z) -> plus#(y, z), plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)))
     (minus#(minus(x, y), z) -> plus#(y, z), plus#(id x, s y) -> if#(gt(s y, y), y, s y))
     (minus#(minus(x, y), z) -> plus#(y, z), plus#(id x, s y) -> gt#(s y, y))
     (minus#(minus(x, y), z) -> minus#(x, plus(y, z)), minus#(minus(x, y), z) -> minus#(x, plus(y, z)))
     (minus#(minus(x, y), z) -> minus#(x, plus(y, z)), minus#(minus(x, y), z) -> plus#(y, z))
     (minus#(minus(x, y), z) -> minus#(x, plus(y, z)), minus#(s x, s y) -> minus#(x, y))
     (plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x))
     (plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), plus#(s x, x) -> if#(gt(x, x), id x, id x))
     (plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), plus#(s x, x) -> gt#(x, x))
     (plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), plus#(s x, x) -> id# x)
     (plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), plus#(s x, y) -> plus#(x, y))
     (plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)))
     (plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), plus#(s x, s y) -> if#(gt(x, y), x, y))
     (plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), plus#(s x, s y) -> if#(not gt(x, y), id x, id y))
     (plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), plus#(s x, s y) -> gt#(x, y))
     (plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), plus#(s x, s y) -> not# gt(x, y))
     (plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), plus#(s x, s y) -> id# x)
     (plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), plus#(s x, s y) -> id# y)
     (plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)))
     (plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), plus#(id x, s y) -> if#(gt(s y, y), y, s y))
     (plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), plus#(id x, s y) -> gt#(s y, y))
     (sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l), sum# app(l, cons(x, cons(y, k))) -> app#(l, sum cons(x, cons(y, k))))
     (sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l), sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k))))
     (sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l), sum# app(l, cons(x, cons(y, k))) -> sum# cons(x, cons(y, k)))
     (sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l), sum# cons(x, cons(y, l)) -> plus#(x, y))
     (sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l), sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l))
     (app#(cons(x, l), k) -> app#(l, k), app#(cons(x, l), k) -> app#(l, k))
     (gt#(s x, s y) -> gt#(x, y), gt#(s x, s y) -> gt#(x, y))
     (sum# app(l, cons(x, cons(y, k))) -> sum# cons(x, cons(y, k)), sum# app(l, cons(x, cons(y, k))) -> app#(l, sum cons(x, cons(y, k))))
     (sum# app(l, cons(x, cons(y, k))) -> sum# cons(x, cons(y, k)), sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k))))
     (sum# app(l, cons(x, cons(y, k))) -> sum# cons(x, cons(y, k)), sum# app(l, cons(x, cons(y, k))) -> sum# cons(x, cons(y, k)))
     (sum# app(l, cons(x, cons(y, k))) -> sum# cons(x, cons(y, k)), sum# cons(x, cons(y, l)) -> plus#(x, y))
     (sum# app(l, cons(x, cons(y, k))) -> sum# cons(x, cons(y, k)), sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l))
     (plus#(s x, y) -> plus#(x, y), plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x))
     (plus#(s x, y) -> plus#(x, y), plus#(s x, x) -> if#(gt(x, x), id x, id x))
     (plus#(s x, y) -> plus#(x, y), plus#(s x, x) -> gt#(x, x))
     (plus#(s x, y) -> plus#(x, y), plus#(s x, x) -> id# x)
     (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))
     (plus#(s x, y) -> plus#(x, y), plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)))
     (plus#(s x, y) -> plus#(x, y), plus#(s x, s y) -> if#(gt(x, y), x, y))
     (plus#(s x, y) -> plus#(x, y), plus#(s x, s y) -> if#(not gt(x, y), id x, id y))
     (plus#(s x, y) -> plus#(x, y), plus#(s x, s y) -> gt#(x, y))
     (plus#(s x, y) -> plus#(x, y), plus#(s x, s y) -> not# gt(x, y))
     (plus#(s x, y) -> plus#(x, y), plus#(s x, s y) -> id# x)
     (plus#(s x, y) -> plus#(x, y), plus#(s x, s y) -> id# y)
     (plus#(s x, y) -> plus#(x, y), plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)))
     (plus#(s x, y) -> plus#(x, y), plus#(id x, s y) -> if#(gt(s y, y), y, s y))
     (plus#(s x, y) -> plus#(x, y), plus#(id x, s y) -> gt#(s y, y))
     (minus#(s x, s y) -> minus#(x, y), minus#(minus(x, y), z) -> minus#(x, plus(y, z)))
     (minus#(s x, s y) -> minus#(x, y), minus#(minus(x, y), z) -> plus#(y, z))
     (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
    }
    STATUS:
     arrows: 0.843112
     SCCS (6):
      Scc:
       {quot#(s x, s y) -> quot#(minus(x, y), s y)}
      Scc:
       {sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k))),
        sum# app(l, cons(x, cons(y, k))) -> sum# cons(x, cons(y, k)),
                sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l)}
      Scc:
       {minus#(minus(x, y), z) -> minus#(x, plus(y, z)),
              minus#(s x, s y) -> minus#(x, y)}
      Scc:
       {   plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x),
           plus#(s x, y) -> plus#(x, y),
         plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)),
        plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y))}
      Scc:
       {gt#(s x, s y) -> gt#(x, y)}
      Scc:
       {app#(cons(x, l), k) -> app#(l, k)}
      
      SCC (1):
       Strict:
        {quot#(s x, s y) -> quot#(minus(x, y), s y)}
       Weak:
       {                  minus(x, 0()) -> x,
                  minus(minus(x, y), z) -> minus(x, plus(y, z)),
                        minus(s x, s y) -> minus(x, y),
                         quot(0(), s y) -> 0(),
                         quot(s x, s y) -> s quot(minus(x, y), s y),
                           plus(0(), y) -> y,
                           plus(s x, x) -> plus(if(gt(x, x), id x, id x), s x),
                           plus(s x, y) -> s plus(x, y),
                         plus(s x, s y) -> s s plus(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)),
                        plus(id x, s y) -> s plus(x, if(gt(s y, y), y, s y)),
                        plus(zero(), y) -> y,
                          app(l, nil()) -> l,
                          app(nil(), k) -> k,
                     app(cons(x, l), k) -> cons(x, app(l, k)),
        sum app(l, cons(x, cons(y, k))) -> sum app(l, sum cons(x, cons(y, k))),
                     sum cons(x, nil()) -> cons(x, nil()),
                sum cons(x, cons(y, l)) -> sum cons(plus(x, y), l),
                       if(true(), x, y) -> x,
                      if(false(), x, y) -> y,
                           gt(s x, s y) -> gt(x, y),
                        gt(s x, zero()) -> true(),
                          gt(zero(), y) -> false(),
                                  not x -> if(x, false(), true()),
                                   id x -> x}
       Open
      SCC (3):
       Strict:
        {sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k))),
         sum# app(l, cons(x, cons(y, k))) -> sum# cons(x, cons(y, k)),
                 sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l)}
       Weak:
       {                  minus(x, 0()) -> x,
                  minus(minus(x, y), z) -> minus(x, plus(y, z)),
                        minus(s x, s y) -> minus(x, y),
                         quot(0(), s y) -> 0(),
                         quot(s x, s y) -> s quot(minus(x, y), s y),
                           plus(0(), y) -> y,
                           plus(s x, x) -> plus(if(gt(x, x), id x, id x), s x),
                           plus(s x, y) -> s plus(x, y),
                         plus(s x, s y) -> s s plus(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)),
                        plus(id x, s y) -> s plus(x, if(gt(s y, y), y, s y)),
                        plus(zero(), y) -> y,
                          app(l, nil()) -> l,
                          app(nil(), k) -> k,
                     app(cons(x, l), k) -> cons(x, app(l, k)),
        sum app(l, cons(x, cons(y, k))) -> sum app(l, sum cons(x, cons(y, k))),
                     sum cons(x, nil()) -> cons(x, nil()),
                sum cons(x, cons(y, l)) -> sum cons(plus(x, y), l),
                       if(true(), x, y) -> x,
                      if(false(), x, y) -> y,
                           gt(s x, s y) -> gt(x, y),
                        gt(s x, zero()) -> true(),
                          gt(zero(), y) -> false(),
                                  not x -> if(x, false(), true()),
                                   id x -> x}
       Open
      
      
      SCC (2):
       Strict:
        {minus#(minus(x, y), z) -> minus#(x, plus(y, z)),
               minus#(s x, s y) -> minus#(x, y)}
       Weak:
       {                  minus(x, 0()) -> x,
                  minus(minus(x, y), z) -> minus(x, plus(y, z)),
                        minus(s x, s y) -> minus(x, y),
                         quot(0(), s y) -> 0(),
                         quot(s x, s y) -> s quot(minus(x, y), s y),
                           plus(0(), y) -> y,
                           plus(s x, x) -> plus(if(gt(x, x), id x, id x), s x),
                           plus(s x, y) -> s plus(x, y),
                         plus(s x, s y) -> s s plus(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)),
                        plus(id x, s y) -> s plus(x, if(gt(s y, y), y, s y)),
                        plus(zero(), y) -> y,
                          app(l, nil()) -> l,
                          app(nil(), k) -> k,
                     app(cons(x, l), k) -> cons(x, app(l, k)),
        sum app(l, cons(x, cons(y, k))) -> sum app(l, sum cons(x, cons(y, k))),
                     sum cons(x, nil()) -> cons(x, nil()),
                sum cons(x, cons(y, l)) -> sum cons(plus(x, y), l),
                       if(true(), x, y) -> x,
                      if(false(), x, y) -> y,
                           gt(s x, s y) -> gt(x, y),
                        gt(s x, zero()) -> true(),
                          gt(zero(), y) -> false(),
                                  not x -> if(x, false(), true()),
                                   id x -> x}
       Open
      
      SCC (4):
       Strict:
        {   plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x),
            plus#(s x, y) -> plus#(x, y),
          plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)),
         plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y))}
       Weak:
       {                  minus(x, 0()) -> x,
                  minus(minus(x, y), z) -> minus(x, plus(y, z)),
                        minus(s x, s y) -> minus(x, y),
                         quot(0(), s y) -> 0(),
                         quot(s x, s y) -> s quot(minus(x, y), s y),
                           plus(0(), y) -> y,
                           plus(s x, x) -> plus(if(gt(x, x), id x, id x), s x),
                           plus(s x, y) -> s plus(x, y),
                         plus(s x, s y) -> s s plus(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)),
                        plus(id x, s y) -> s plus(x, if(gt(s y, y), y, s y)),
                        plus(zero(), y) -> y,
                          app(l, nil()) -> l,
                          app(nil(), k) -> k,
                     app(cons(x, l), k) -> cons(x, app(l, k)),
        sum app(l, cons(x, cons(y, k))) -> sum app(l, sum cons(x, cons(y, k))),
                     sum cons(x, nil()) -> cons(x, nil()),
                sum cons(x, cons(y, l)) -> sum cons(plus(x, y), l),
                       if(true(), x, y) -> x,
                      if(false(), x, y) -> y,
                           gt(s x, s y) -> gt(x, y),
                        gt(s x, zero()) -> true(),
                          gt(zero(), y) -> false(),
                                  not x -> if(x, false(), true()),
                                   id x -> x}
       Open
      
      
      
      
      
      
      
      
      
      
      SCC (1):
       Strict:
        {gt#(s x, s y) -> gt#(x, y)}
       Weak:
       {                  minus(x, 0()) -> x,
                  minus(minus(x, y), z) -> minus(x, plus(y, z)),
                        minus(s x, s y) -> minus(x, y),
                         quot(0(), s y) -> 0(),
                         quot(s x, s y) -> s quot(minus(x, y), s y),
                           plus(0(), y) -> y,
                           plus(s x, x) -> plus(if(gt(x, x), id x, id x), s x),
                           plus(s x, y) -> s plus(x, y),
                         plus(s x, s y) -> s s plus(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)),
                        plus(id x, s y) -> s plus(x, if(gt(s y, y), y, s y)),
                        plus(zero(), y) -> y,
                          app(l, nil()) -> l,
                          app(nil(), k) -> k,
                     app(cons(x, l), k) -> cons(x, app(l, k)),
        sum app(l, cons(x, cons(y, k))) -> sum app(l, sum cons(x, cons(y, k))),
                     sum cons(x, nil()) -> cons(x, nil()),
                sum cons(x, cons(y, l)) -> sum cons(plus(x, y), l),
                       if(true(), x, y) -> x,
                      if(false(), x, y) -> y,
                           gt(s x, s y) -> gt(x, y),
                        gt(s x, zero()) -> true(),
                          gt(zero(), y) -> false(),
                                  not x -> if(x, false(), true()),
                                   id x -> x}
       Open
      
      
      SCC (1):
       Strict:
        {app#(cons(x, l), k) -> app#(l, k)}
       Weak:
       {                  minus(x, 0()) -> x,
                  minus(minus(x, y), z) -> minus(x, plus(y, z)),
                        minus(s x, s y) -> minus(x, y),
                         quot(0(), s y) -> 0(),
                         quot(s x, s y) -> s quot(minus(x, y), s y),
                           plus(0(), y) -> y,
                           plus(s x, x) -> plus(if(gt(x, x), id x, id x), s x),
                           plus(s x, y) -> s plus(x, y),
                         plus(s x, s y) -> s s plus(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)),
                        plus(id x, s y) -> s plus(x, if(gt(s y, y), y, s y)),
                        plus(zero(), y) -> y,
                          app(l, nil()) -> l,
                          app(nil(), k) -> k,
                     app(cons(x, l), k) -> cons(x, app(l, k)),
        sum app(l, cons(x, cons(y, k))) -> sum app(l, sum cons(x, cons(y, k))),
                     sum cons(x, nil()) -> cons(x, nil()),
                sum cons(x, cons(y, l)) -> sum cons(plus(x, y), l),
                       if(true(), x, y) -> x,
                      if(false(), x, y) -> y,
                           gt(s x, s y) -> gt(x, y),
                        gt(s x, zero()) -> true(),
                          gt(zero(), y) -> false(),
                                  not x -> if(x, false(), true()),
                                   id x -> x}
       Open