MAYBE
TRS:
 {       minus(x, 0()) -> x,
  minus(x, plus(y, z)) -> minus(minus(x, y), z),
         minus(0(), y) -> 0(),
     minus(s(x), s(y)) -> minus(p(s(x)), p(s(y))),
                p(0()) -> s(s(0())),
            p(s(s(x))) -> s(p(s(x))),
          plus(0(), y) -> y,
         plus(s(x), y) -> s(plus(y, minus(s(x), s(0())))),
       div(s(x), s(y)) -> s(div(minus(x, y), s(y))),
    div(plus(x, y), z) -> plus(div(x, z), div(y, z))}
 DP:
  Strict:
   {minus#(x, plus(y, z)) -> minus#(x, y),
    minus#(x, plus(y, z)) -> minus#(minus(x, y), z),
       minus#(s(x), s(y)) -> minus#(p(s(x)), p(s(y))),
       minus#(s(x), s(y)) -> p#(s(x)),
       minus#(s(x), s(y)) -> p#(s(y)),
              p#(s(s(x))) -> p#(s(x)),
           plus#(s(x), y) -> minus#(s(x), s(0())),
           plus#(s(x), y) -> plus#(y, minus(s(x), s(0()))),
         div#(s(x), s(y)) -> minus#(x, y),
         div#(s(x), s(y)) -> div#(minus(x, y), s(y)),
      div#(plus(x, y), z) -> plus#(div(x, z), div(y, z)),
      div#(plus(x, y), z) -> div#(x, z),
      div#(plus(x, y), z) -> div#(y, z)}
  Weak:
  {       minus(x, 0()) -> x,
   minus(x, plus(y, z)) -> minus(minus(x, y), z),
          minus(0(), y) -> 0(),
      minus(s(x), s(y)) -> minus(p(s(x)), p(s(y))),
                 p(0()) -> s(s(0())),
             p(s(s(x))) -> s(p(s(x))),
           plus(0(), y) -> y,
          plus(s(x), y) -> s(plus(y, minus(s(x), s(0())))),
        div(s(x), s(y)) -> s(div(minus(x, y), s(y))),
     div(plus(x, y), z) -> plus(div(x, z), div(y, z))}
  EDG:
   {(plus#(s(x), y) -> minus#(s(x), s(0())), minus#(s(x), s(y)) -> p#(s(y)))
    (plus#(s(x), y) -> minus#(s(x), s(0())), minus#(s(x), s(y)) -> p#(s(x)))
    (plus#(s(x), y) -> minus#(s(x), s(0())), minus#(s(x), s(y)) -> minus#(p(s(x)), p(s(y))))
    (div#(plus(x, y), z) -> div#(y, z), div#(plus(x, y), z) -> div#(y, z))
    (div#(plus(x, y), z) -> div#(y, z), div#(plus(x, y), z) -> div#(x, z))
    (div#(plus(x, y), z) -> div#(y, z), div#(plus(x, y), z) -> plus#(div(x, z), div(y, z)))
    (div#(plus(x, y), z) -> div#(y, z), div#(s(x), s(y)) -> div#(minus(x, y), s(y)))
    (div#(plus(x, y), z) -> div#(y, z), div#(s(x), s(y)) -> minus#(x, y))
    (minus#(x, plus(y, z)) -> minus#(minus(x, y), z), minus#(s(x), s(y)) -> p#(s(y)))
    (minus#(x, plus(y, z)) -> minus#(minus(x, y), z), minus#(s(x), s(y)) -> p#(s(x)))
    (minus#(x, plus(y, z)) -> minus#(minus(x, y), z), minus#(s(x), s(y)) -> minus#(p(s(x)), p(s(y))))
    (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), minus#(x, plus(y, z)) -> minus#(x, y))
    (minus#(x, plus(y, z)) -> minus#(x, y), minus#(s(x), s(y)) -> p#(s(y)))
    (minus#(x, plus(y, z)) -> minus#(x, y), minus#(s(x), s(y)) -> p#(s(x)))
    (minus#(x, plus(y, z)) -> minus#(x, y), minus#(s(x), s(y)) -> minus#(p(s(x)), p(s(y))))
    (minus#(x, plus(y, z)) -> minus#(x, y), minus#(x, plus(y, z)) -> minus#(minus(x, y), z))
    (minus#(x, plus(y, z)) -> minus#(x, y), minus#(x, plus(y, z)) -> minus#(x, y))
    (div#(plus(x, y), z) -> plus#(div(x, z), div(y, z)), plus#(s(x), y) -> plus#(y, minus(s(x), s(0()))))
    (div#(plus(x, y), z) -> plus#(div(x, z), div(y, z)), plus#(s(x), y) -> minus#(s(x), s(0())))
    (minus#(s(x), s(y)) -> p#(s(x)), p#(s(s(x))) -> p#(s(x)))
    (p#(s(s(x))) -> p#(s(x)), p#(s(s(x))) -> p#(s(x)))
    (minus#(s(x), s(y)) -> p#(s(y)), p#(s(s(x))) -> p#(s(x)))
    (div#(s(x), s(y)) -> minus#(x, y), minus#(x, plus(y, z)) -> minus#(x, y))
    (div#(s(x), s(y)) -> minus#(x, y), minus#(x, plus(y, z)) -> minus#(minus(x, y), z))
    (div#(s(x), s(y)) -> minus#(x, y), minus#(s(x), s(y)) -> minus#(p(s(x)), p(s(y))))
    (div#(s(x), s(y)) -> minus#(x, y), minus#(s(x), s(y)) -> p#(s(x)))
    (div#(s(x), s(y)) -> minus#(x, y), minus#(s(x), s(y)) -> p#(s(y)))
    (div#(s(x), s(y)) -> div#(minus(x, y), s(y)), div#(s(x), s(y)) -> minus#(x, y))
    (div#(s(x), s(y)) -> div#(minus(x, y), s(y)), div#(s(x), s(y)) -> div#(minus(x, y), s(y)))
    (div#(s(x), s(y)) -> div#(minus(x, y), s(y)), div#(plus(x, y), z) -> plus#(div(x, z), div(y, z)))
    (div#(s(x), s(y)) -> div#(minus(x, y), s(y)), div#(plus(x, y), z) -> div#(x, z))
    (div#(s(x), s(y)) -> div#(minus(x, y), s(y)), div#(plus(x, y), z) -> div#(y, z))
    (plus#(s(x), y) -> plus#(y, minus(s(x), s(0()))), plus#(s(x), y) -> minus#(s(x), s(0())))
    (plus#(s(x), y) -> plus#(y, minus(s(x), s(0()))), plus#(s(x), y) -> plus#(y, minus(s(x), s(0()))))
    (div#(plus(x, y), z) -> div#(x, z), div#(s(x), s(y)) -> minus#(x, y))
    (div#(plus(x, y), z) -> div#(x, z), div#(s(x), s(y)) -> div#(minus(x, y), s(y)))
    (div#(plus(x, y), z) -> div#(x, z), div#(plus(x, y), z) -> plus#(div(x, z), div(y, z)))
    (div#(plus(x, y), z) -> div#(x, z), div#(plus(x, y), z) -> div#(x, z))
    (div#(plus(x, y), z) -> div#(x, z), div#(plus(x, y), z) -> div#(y, z))
    (minus#(s(x), s(y)) -> minus#(p(s(x)), p(s(y))), minus#(x, plus(y, z)) -> minus#(x, y))
    (minus#(s(x), s(y)) -> minus#(p(s(x)), p(s(y))), minus#(x, plus(y, z)) -> minus#(minus(x, y), z))
    (minus#(s(x), s(y)) -> minus#(p(s(x)), p(s(y))), minus#(s(x), s(y)) -> minus#(p(s(x)), p(s(y))))
    (minus#(s(x), s(y)) -> minus#(p(s(x)), p(s(y))), minus#(s(x), s(y)) -> p#(s(x)))
    (minus#(s(x), s(y)) -> minus#(p(s(x)), p(s(y))), minus#(s(x), s(y)) -> p#(s(y)))}
   SCCS:
    Scc:
     {   div#(s(x), s(y)) -> div#(minus(x, y), s(y)),
      div#(plus(x, y), z) -> div#(x, z),
      div#(plus(x, y), z) -> div#(y, z)}
    Scc:
     {plus#(s(x), y) -> plus#(y, minus(s(x), s(0())))}
    Scc:
     {p#(s(s(x))) -> p#(s(x))}
    Scc:
     {minus#(x, plus(y, z)) -> minus#(x, y),
      minus#(x, plus(y, z)) -> minus#(minus(x, y), z),
         minus#(s(x), s(y)) -> minus#(p(s(x)), p(s(y)))}
    SCC:
     Strict:
      {   div#(s(x), s(y)) -> div#(minus(x, y), s(y)),
       div#(plus(x, y), z) -> div#(x, z),
       div#(plus(x, y), z) -> div#(y, z)}
     Weak:
     {       minus(x, 0()) -> x,
      minus(x, plus(y, z)) -> minus(minus(x, y), z),
             minus(0(), y) -> 0(),
         minus(s(x), s(y)) -> minus(p(s(x)), p(s(y))),
                    p(0()) -> s(s(0())),
                p(s(s(x))) -> s(p(s(x))),
              plus(0(), y) -> y,
             plus(s(x), y) -> s(plus(y, minus(s(x), s(0())))),
           div(s(x), s(y)) -> s(div(minus(x, y), s(y))),
        div(plus(x, y), z) -> plus(div(x, z), div(y, z))}
     POLY:
      Argument Filtering:
       pi(div#) = 0, pi(div) = [], pi(plus) = [0,1], pi(s) = 0, pi(p) = [], pi(0) = [], pi(minus) = 0
      Usable Rules:
       {}
      Interpretation:
       [plus](x0, x1) = x0 + x1 + 1
      Strict:
       {div#(s(x), s(y)) -> div#(minus(x, y), s(y))}
      Weak:
       {       minus(x, 0()) -> x,
        minus(x, plus(y, z)) -> minus(minus(x, y), z),
               minus(0(), y) -> 0(),
           minus(s(x), s(y)) -> minus(p(s(x)), p(s(y))),
                      p(0()) -> s(s(0())),
                  p(s(s(x))) -> s(p(s(x))),
                plus(0(), y) -> y,
               plus(s(x), y) -> s(plus(y, minus(s(x), s(0())))),
             div(s(x), s(y)) -> s(div(minus(x, y), s(y))),
          div(plus(x, y), z) -> plus(div(x, z), div(y, z))}
      EDG:
       {(div#(s(x), s(y)) -> div#(minus(x, y), s(y)), div#(s(x), s(y)) -> div#(minus(x, y), s(y)))}
       SCCS:
        Scc:
         {div#(s(x), s(y)) -> div#(minus(x, y), s(y))}
        SCC:
         Strict:
          {div#(s(x), s(y)) -> div#(minus(x, y), s(y))}
         Weak:
         {       minus(x, 0()) -> x,
          minus(x, plus(y, z)) -> minus(minus(x, y), z),
                 minus(0(), y) -> 0(),
             minus(s(x), s(y)) -> minus(p(s(x)), p(s(y))),
                        p(0()) -> s(s(0())),
                    p(s(s(x))) -> s(p(s(x))),
                  plus(0(), y) -> y,
                 plus(s(x), y) -> s(plus(y, minus(s(x), s(0())))),
               div(s(x), s(y)) -> s(div(minus(x, y), s(y))),
            div(plus(x, y), z) -> plus(div(x, z), div(y, z))}
         Fail
    SCC:
     Strict:
      {plus#(s(x), y) -> plus#(y, minus(s(x), s(0())))}
     Weak:
     {       minus(x, 0()) -> x,
      minus(x, plus(y, z)) -> minus(minus(x, y), z),
             minus(0(), y) -> 0(),
         minus(s(x), s(y)) -> minus(p(s(x)), p(s(y))),
                    p(0()) -> s(s(0())),
                p(s(s(x))) -> s(p(s(x))),
              plus(0(), y) -> y,
             plus(s(x), y) -> s(plus(y, minus(s(x), s(0())))),
           div(s(x), s(y)) -> s(div(minus(x, y), s(y))),
        div(plus(x, y), z) -> plus(div(x, z), div(y, z))}
     Fail
    SCC:
     Strict:
      {p#(s(s(x))) -> p#(s(x))}
     Weak:
     {       minus(x, 0()) -> x,
      minus(x, plus(y, z)) -> minus(minus(x, y), z),
             minus(0(), y) -> 0(),
         minus(s(x), s(y)) -> minus(p(s(x)), p(s(y))),
                    p(0()) -> s(s(0())),
                p(s(s(x))) -> s(p(s(x))),
              plus(0(), y) -> y,
             plus(s(x), y) -> s(plus(y, minus(s(x), s(0())))),
           div(s(x), s(y)) -> s(div(minus(x, y), s(y))),
        div(plus(x, y), z) -> plus(div(x, z), div(y, z))}
     SPSC:
      Simple Projection:
       pi(p#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {minus#(x, plus(y, z)) -> minus#(x, y),
       minus#(x, plus(y, z)) -> minus#(minus(x, y), z),
          minus#(s(x), s(y)) -> minus#(p(s(x)), p(s(y)))}
     Weak:
     {       minus(x, 0()) -> x,
      minus(x, plus(y, z)) -> minus(minus(x, y), z),
             minus(0(), y) -> 0(),
         minus(s(x), s(y)) -> minus(p(s(x)), p(s(y))),
                    p(0()) -> s(s(0())),
                p(s(s(x))) -> s(p(s(x))),
              plus(0(), y) -> y,
             plus(s(x), y) -> s(plus(y, minus(s(x), s(0())))),
           div(s(x), s(y)) -> s(div(minus(x, y), s(y))),
        div(plus(x, y), z) -> plus(div(x, z), div(y, z))}
     POLY:
      Argument Filtering:
       pi(div) = [], pi(plus) = [0,1], pi(s) = [], pi(p) = [], pi(0) = [], pi(minus#) = 1, pi(minus) = []
      Usable Rules:
       {}
      Interpretation:
       [plus](x0, x1) = x0 + x1 + 1,
       [s] = 0,
       [p] = 0
      Strict:
       {minus#(s(x), s(y)) -> minus#(p(s(x)), p(s(y)))}
      Weak:
       {       minus(x, 0()) -> x,
        minus(x, plus(y, z)) -> minus(minus(x, y), z),
               minus(0(), y) -> 0(),
           minus(s(x), s(y)) -> minus(p(s(x)), p(s(y))),
                      p(0()) -> s(s(0())),
                  p(s(s(x))) -> s(p(s(x))),
                plus(0(), y) -> y,
               plus(s(x), y) -> s(plus(y, minus(s(x), s(0())))),
             div(s(x), s(y)) -> s(div(minus(x, y), s(y))),
          div(plus(x, y), z) -> plus(div(x, z), div(y, z))}
      EDG:
       {(minus#(s(x), s(y)) -> minus#(p(s(x)), p(s(y))), minus#(s(x), s(y)) -> minus#(p(s(x)), p(s(y))))}
       SCCS:
        Scc:
         {minus#(s(x), s(y)) -> minus#(p(s(x)), p(s(y)))}
        SCC:
         Strict:
          {minus#(s(x), s(y)) -> minus#(p(s(x)), p(s(y)))}
         Weak:
         {       minus(x, 0()) -> x,
          minus(x, plus(y, z)) -> minus(minus(x, y), z),
                 minus(0(), y) -> 0(),
             minus(s(x), s(y)) -> minus(p(s(x)), p(s(y))),
                        p(0()) -> s(s(0())),
                    p(s(s(x))) -> s(p(s(x))),
                  plus(0(), y) -> y,
                 plus(s(x), y) -> s(plus(y, minus(s(x), s(0())))),
               div(s(x), s(y)) -> s(div(minus(x, y), s(y))),
            div(plus(x, y), z) -> plus(div(x, z), div(y, z))}
         Fail