MAYBE
TRS:
 {    minus(x, 0()) -> x,
  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(s(x), x) -> plus(if(gt(x, x), id(x), id(x)), s(x)),
   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,
   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:
  Strict:
   {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), 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),
       gt#(s(x), s(y)) -> gt#(x, y),
               not#(x) -> if#(x, false(), true())}
  Weak:
  {    minus(x, 0()) -> x,
   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(s(x), x) -> plus(if(gt(x, x), id(x), id(x)), s(x)),
    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,
    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}
  EDG:
   {(minus#(s(x), s(y)) -> minus#(x, y), minus#(s(x), s(y)) -> minus#(x, y))
    (gt#(s(x), s(y)) -> gt#(x, 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), 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)))
    (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), 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#(id(x), s(y)) -> gt#(s(y), y), gt#(s(x), s(y)) -> gt#(x, y))
    (plus#(s(x), x) -> gt#(x, x), gt#(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), 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), 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))
    (plus#(s(x), s(y)) -> not#(gt(x, y)), not#(x) -> if#(x, false(), true()))
    (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)))
    (plus#(s(x), s(y)) -> gt#(x, y), gt#(s(x), s(y)) -> gt#(x, y))
    (quot#(s(x), s(y)) -> minus#(x, y), minus#(s(x), s(y)) -> minus#(x, y))}
   SCCS:
    Scc:
     {gt#(s(x), s(y)) -> gt#(x, y)}
    Scc:
     {    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#(id(x), s(y)) -> plus#(x, if(gt(s(y), y), y, s(y)))}
    Scc:
     {quot#(s(x), s(y)) -> quot#(minus(x, y), s(y))}
    Scc:
     {minus#(s(x), s(y)) -> minus#(x, y)}
    SCC:
     Strict:
      {gt#(s(x), s(y)) -> gt#(x, y)}
     Weak:
     {    minus(x, 0()) -> x,
      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(s(x), x) -> plus(if(gt(x, x), id(x), id(x)), s(x)),
       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,
       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}
     SPSC:
      Simple Projection:
       pi(gt#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {    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#(id(x), s(y)) -> plus#(x, if(gt(s(y), y), y, s(y)))}
     Weak:
     {    minus(x, 0()) -> x,
      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(s(x), x) -> plus(if(gt(x, x), id(x), id(x)), s(x)),
       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,
       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}
     Fail
    SCC:
     Strict:
      {quot#(s(x), s(y)) -> quot#(minus(x, y), s(y))}
     Weak:
     {    minus(x, 0()) -> x,
      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(s(x), x) -> plus(if(gt(x, x), id(x), id(x)), s(x)),
       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,
       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}
     POLY:
      Argument Filtering:
       pi(false) = [], pi(true) = [], pi(zero) = [], pi(id) = [], pi(not) = [], pi(gt) = [], pi(if) = 2, pi(plus) = 1, pi(quot#) = 0, pi(quot) = [], pi(s) = [0], pi(0) = [], pi(minus) = 0
      Usable Rules:
       {}
      Interpretation:
       [s](x0) = x0 + 1
      Strict:
       {}
      Weak:
       {    minus(x, 0()) -> x,
        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(s(x), x) -> plus(if(gt(x, x), id(x), id(x)), s(x)),
         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,
         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}
      Qed
    SCC:
     Strict:
      {minus#(s(x), s(y)) -> minus#(x, y)}
     Weak:
     {    minus(x, 0()) -> x,
      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(s(x), x) -> plus(if(gt(x, x), id(x), id(x)), s(x)),
       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,
       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}
     SPSC:
      Simple Projection:
       pi(minus#) = 0
      Strict:
       {}
      Qed