MAYBE
Time: 0.064884
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:
  DP:
   {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)}
  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))}
  EDG:
   {(minus#(s x, s y) -> minus#(p s x, p s y), minus#(s x, s y) -> 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) -> minus#(p s x, p s 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#(x, plus(y, z)) -> minus#(x, y))
    (div#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> 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) -> minus#(p s x, p s 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#(x, plus(y, z)) -> minus#(x, 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#(s x, s y) -> p# s y, p# s s x -> p# s x)
    (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)
    (div#(plus(x, y), z) -> plus#(div(x, z), div(y, z)), plus#(s x, y) -> minus#(s x, s 0()))
    (div#(plus(x, y), z) -> plus#(div(x, z), div(y, z)), plus#(s x, y) -> plus#(y, minus(s x, s 0())))
    (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))
    (plus#(s x, y) -> minus#(s x, s 0()), minus#(s x, s y) -> minus#(p s x, 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) -> p# s y)
    (minus#(x, plus(y, z)) -> minus#(x, y), minus#(x, plus(y, z)) -> minus#(x, 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#(s x, s y) -> minus#(p s x, 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) -> p# s y)}
   SCCS (4):
    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 (3):
     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:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [minus](x0, x1) = x0,
       
       [plus](x0, x1) = x0 + x1 + 1,
       
       [div](x0, x1) = 0,
       
       [p](x0) = x0,
       
       [s](x0) = x0,
       
       [0] = 0,
       
       [div#](x0, x1) = x0
      Strict:
       div#(plus(x, y), z) -> div#(y, z)
       1 + 1x + 1y + 0z >= 0 + 1y + 0z
       div#(plus(x, y), z) -> div#(x, z)
       1 + 1x + 1y + 0z >= 0 + 1x + 0z
       div#(s x, s y) -> div#(minus(x, y), s y)
       0 + 1x + 0y >= 0 + 1x + 0y
      Weak:
       
     EDG:
      {(div#(s x, s y) -> div#(minus(x, y), s y), div#(s x, s y) -> div#(minus(x, y), s y))}
      SCCS (1):
       Scc:
        {div#(s x, s y) -> div#(minus(x, y), s y)}
       SCC (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))}
        Fail
   SCC (1):
    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 (1):
    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 (3):
    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:
     Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
     Interpretation:
      [minus](x0, x1) = x0 + x1 + 1,
      
      [plus](x0, x1) = x0 + x1 + 1,
      
      [div](x0, x1) = x0 + 1,
      
      [p](x0) = 0,
      
      [s](x0) = 0,
      
      [0] = 1,
      
      [minus#](x0, x1) = x0
     Strict:
      minus#(s x, s y) -> minus#(p s x, p s y)
      0 + 0x + 0y >= 0 + 0x + 0y
      minus#(x, plus(y, z)) -> minus#(minus(x, y), z)
      1 + 0x + 1y + 1z >= 0 + 0x + 0y + 1z
      minus#(x, plus(y, z)) -> minus#(x, y)
      1 + 0x + 1y + 1z >= 0 + 0x + 1y
     Weak:
      
    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 (1):
      Scc:
       {minus#(s x, s y) -> minus#(p s x, p s y)}
      SCC (1):
       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