MAYBE
Time: 0.005415
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(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:
  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, 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())}
  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(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}
  UR:
   {        minus(x, 0()) -> x,
    minus(minus(x, y), z) -> minus(x, plus(y, z)),
          minus(s x, s y) -> minus(x, 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,
                  a(w, v) -> w,
                  a(w, v) -> v}
   EDG:
    {(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#(s x, s y) -> not# gt(x, y), not# x -> if#(x, false(), true()))
     (plus#(s x, x) -> gt#(x, x), gt#(s x, s y) -> gt#(x, y))
     (quot#(s x, s y) -> quot#(minus(x, y), s y), quot#(s x, s y) -> quot#(minus(x, y), s y))
     (quot#(s x, s y) -> quot#(minus(x, y), s y), quot#(s x, s y) -> minus#(x, y))
     (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)))
     (gt#(s x, s y) -> gt#(x, y), gt#(s x, s y) -> gt#(x, 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, 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))
     (plus#(s x, s y) -> gt#(x, y), gt#(s x, s y) -> gt#(x, 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))
     (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#(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) -> gt#(x, x))
     (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, 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) -> 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) -> 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) -> gt#(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))
     (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) -> id# 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#(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) -> gt#(s y, y))
     (plus#(id x, s y) -> gt#(s y, y), gt#(s x, s y) -> gt#(x, 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, 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))}
    STATUS:
     arrows: 0.836735
     SCCS (4):
      Scc:
       {quot#(s x, s y) -> quot#(minus(x, y), s y)}
      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, 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 (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(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}
       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(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}
       Open
      
      SCC (3):
       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(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(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}
       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(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}
       Open