MAYBE
Time: 0.008714
TRS:
 {         minus(x, 0()) -> x,
           minus(0(), y) -> 0(),
         minus(s x, s y) -> minus(x, y),
            plus(0(), y) -> y,
            plus(s x, y) -> plus(x, s y),
                zero 0() -> true(),
                zero s x -> false(),
                   p s x -> x,
           quot(x, y, z) -> if(zero x, x, y, plus(z, s 0())),
               div(x, y) -> quot(x, y, 0()),
  if(false(), x, s y, z) -> quot(minus(x, s y), s y, z),
     if(true(), x, y, z) -> p z}
 DP:
  DP:
   {       minus#(s x, s y) -> minus#(x, y),
              plus#(s x, y) -> plus#(x, s y),
             quot#(x, y, z) -> plus#(z, s 0()),
             quot#(x, y, z) -> zero# x,
             quot#(x, y, z) -> if#(zero x, x, y, plus(z, s 0())),
                 div#(x, y) -> quot#(x, y, 0()),
    if#(false(), x, s y, z) -> minus#(x, s y),
    if#(false(), x, s y, z) -> quot#(minus(x, s y), s y, z),
       if#(true(), x, y, z) -> p# z}
  TRS:
  {         minus(x, 0()) -> x,
            minus(0(), y) -> 0(),
          minus(s x, s y) -> minus(x, y),
             plus(0(), y) -> y,
             plus(s x, y) -> plus(x, s y),
                 zero 0() -> true(),
                 zero s x -> false(),
                    p s x -> x,
            quot(x, y, z) -> if(zero x, x, y, plus(z, s 0())),
                div(x, y) -> quot(x, y, 0()),
   if(false(), x, s y, z) -> quot(minus(x, s y), s y, z),
      if(true(), x, y, z) -> p z}
  EDG:
   {(quot#(x, y, z) -> if#(zero x, x, y, plus(z, s 0())), if#(true(), x, y, z) -> p# z)
    (quot#(x, y, z) -> if#(zero x, x, y, plus(z, s 0())), if#(false(), x, s y, z) -> quot#(minus(x, s y), s y, z))
    (quot#(x, y, z) -> if#(zero x, x, y, plus(z, s 0())), if#(false(), x, s y, z) -> minus#(x, s y))
    (if#(false(), x, s y, z) -> quot#(minus(x, s y), s y, z), quot#(x, y, z) -> if#(zero x, x, y, plus(z, s 0())))
    (if#(false(), x, s y, z) -> quot#(minus(x, s y), s y, z), quot#(x, y, z) -> zero# x)
    (if#(false(), x, s y, z) -> quot#(minus(x, s y), s y, z), quot#(x, y, z) -> plus#(z, s 0()))
    (quot#(x, y, z) -> plus#(z, s 0()), plus#(s x, y) -> plus#(x, s y))
    (plus#(s x, y) -> plus#(x, s y), plus#(s x, y) -> plus#(x, s y))
    (if#(false(), x, s y, z) -> minus#(x, s y), minus#(s x, s y) -> minus#(x, y))
    (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
    (div#(x, y) -> quot#(x, y, 0()), quot#(x, y, z) -> plus#(z, s 0()))
    (div#(x, y) -> quot#(x, y, 0()), quot#(x, y, z) -> zero# x)
    (div#(x, y) -> quot#(x, y, 0()), quot#(x, y, z) -> if#(zero x, x, y, plus(z, s 0())))}
   STATUS:
    arrows: 0.839506
    SCCS (3):
     Scc:
      {         quot#(x, y, z) -> if#(zero x, x, y, plus(z, s 0())),
       if#(false(), x, s y, z) -> quot#(minus(x, s y), s y, z)}
     Scc:
      {minus#(s x, s y) -> minus#(x, y)}
     Scc:
      {plus#(s x, y) -> plus#(x, s y)}
     
     
     SCC (2):
      Strict:
       {         quot#(x, y, z) -> if#(zero x, x, y, plus(z, s 0())),
        if#(false(), x, s y, z) -> quot#(minus(x, s y), s y, z)}
      Weak:
      {         minus(x, 0()) -> x,
                minus(0(), y) -> 0(),
              minus(s x, s y) -> minus(x, y),
                 plus(0(), y) -> y,
                 plus(s x, y) -> plus(x, s y),
                     zero 0() -> true(),
                     zero s x -> false(),
                        p s x -> x,
                quot(x, y, z) -> if(zero x, x, y, plus(z, s 0())),
                    div(x, y) -> quot(x, y, 0()),
       if(false(), x, s y, z) -> quot(minus(x, s y), s y, z),
          if(true(), x, y, z) -> p z}
      Open
     
     
     SCC (1):
      Strict:
       {minus#(s x, s y) -> minus#(x, y)}
      Weak:
      {         minus(x, 0()) -> x,
                minus(0(), y) -> 0(),
              minus(s x, s y) -> minus(x, y),
                 plus(0(), y) -> y,
                 plus(s x, y) -> plus(x, s y),
                     zero 0() -> true(),
                     zero s x -> false(),
                        p s x -> x,
                quot(x, y, z) -> if(zero x, x, y, plus(z, s 0())),
                    div(x, y) -> quot(x, y, 0()),
       if(false(), x, s y, z) -> quot(minus(x, s y), s y, z),
          if(true(), x, y, z) -> p z}
      Open
     
     
     SCC (1):
      Strict:
       {plus#(s x, y) -> plus#(x, s y)}
      Weak:
      {         minus(x, 0()) -> x,
                minus(0(), y) -> 0(),
              minus(s x, s y) -> minus(x, y),
                 plus(0(), y) -> y,
                 plus(s x, y) -> plus(x, s y),
                     zero 0() -> true(),
                     zero s x -> false(),
                        p s x -> x,
                quot(x, y, z) -> if(zero x, x, y, plus(z, s 0())),
                    div(x, y) -> quot(x, y, 0()),
       if(false(), x, s y, z) -> quot(minus(x, s y), s y, z),
          if(true(), x, y, z) -> p z}
      Open