MAYBE
Time: 0.010821
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))}
  UR:
   {       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 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)),
                 a(w, v) -> w,
                 a(w, v) -> v}
   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#(x, plus(y, z)) -> minus#(x, y))
     (plus#(s x, y) -> minus#(s x, s 0()), minus#(x, plus(y, z)) -> minus#(minus(x, 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)}
    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)}
     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))
       (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)}
      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))
        (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)}
       STATUS:
        arrows: 0.745562
        SCCS (5):
         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:
          {minus#(x, plus(y, z)) -> minus#(x, y),
           minus#(x, plus(y, z)) -> minus#(minus(x, y), z)}
         Scc:
          {minus#(s x, s y) -> minus#(p s x, p s y)}
         Scc:
          {p# s s x -> p# s x}
         
         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))}
          Open
         
         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))}
          Open
         
         
         SCC (2):
          Strict:
           {minus#(x, plus(y, z)) -> minus#(x, y),
            minus#(x, plus(y, z)) -> minus#(minus(x, 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))}
          Open
         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))}
          Open
         
         
         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))}
          Open