MAYBE

Problem:
 minus(minus(x,y),z) -> minus(x,plus(y,z))
 minus(0(),y) -> 0()
 minus(x,0()) -> x
 minus(s(x),s(y)) -> minus(x,y)
 plus(0(),y) -> y
 plus(s(x),y) -> plus(x,s(y))
 plus(s(x),y) -> s(plus(y,x))
 zero(s(x)) -> false()
 zero(0()) -> true()
 p(s(x)) -> x
 p(0()) -> 0()
 div(x,y) -> quot(x,y,0())
 quot(s(x),s(y),z) -> quot(minus(p(ack(0(),x)),y),s(y),s(z))
 quot(0(),s(y),z) -> z
 ack(0(),x) -> s(x)
 ack(0(),x) -> plus(x,s(0()))
 ack(s(x),0()) -> ack(x,s(0()))
 ack(s(x),s(y)) -> ack(x,ack(s(x),y))

Proof:
 DP Processor:
  DPs:
   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),y) -> plus#(x,s(y))
   plus#(s(x),y) -> plus#(y,x)
   div#(x,y) -> quot#(x,y,0())
   quot#(s(x),s(y),z) -> ack#(0(),x)
   quot#(s(x),s(y),z) -> p#(ack(0(),x))
   quot#(s(x),s(y),z) -> minus#(p(ack(0(),x)),y)
   quot#(s(x),s(y),z) -> quot#(minus(p(ack(0(),x)),y),s(y),s(z))
   ack#(0(),x) -> plus#(x,s(0()))
   ack#(s(x),0()) -> ack#(x,s(0()))
   ack#(s(x),s(y)) -> ack#(s(x),y)
   ack#(s(x),s(y)) -> ack#(x,ack(s(x),y))
  TRS:
   minus(minus(x,y),z) -> minus(x,plus(y,z))
   minus(0(),y) -> 0()
   minus(x,0()) -> x
   minus(s(x),s(y)) -> minus(x,y)
   plus(0(),y) -> y
   plus(s(x),y) -> plus(x,s(y))
   plus(s(x),y) -> s(plus(y,x))
   zero(s(x)) -> false()
   zero(0()) -> true()
   p(s(x)) -> x
   p(0()) -> 0()
   div(x,y) -> quot(x,y,0())
   quot(s(x),s(y),z) -> quot(minus(p(ack(0(),x)),y),s(y),s(z))
   quot(0(),s(y),z) -> z
   ack(0(),x) -> s(x)
   ack(0(),x) -> plus(x,s(0()))
   ack(s(x),0()) -> ack(x,s(0()))
   ack(s(x),s(y)) -> ack(x,ack(s(x),y))
  Usable Rule Processor:
   DPs:
    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),y) -> plus#(x,s(y))
    plus#(s(x),y) -> plus#(y,x)
    div#(x,y) -> quot#(x,y,0())
    quot#(s(x),s(y),z) -> ack#(0(),x)
    quot#(s(x),s(y),z) -> p#(ack(0(),x))
    quot#(s(x),s(y),z) -> minus#(p(ack(0(),x)),y)
    quot#(s(x),s(y),z) -> quot#(minus(p(ack(0(),x)),y),s(y),s(z))
    ack#(0(),x) -> plus#(x,s(0()))
    ack#(s(x),0()) -> ack#(x,s(0()))
    ack#(s(x),s(y)) -> ack#(s(x),y)
    ack#(s(x),s(y)) -> ack#(x,ack(s(x),y))
   TRS:
    f18(x,y) -> x
    f18(x,y) -> y
    plus(0(),y) -> y
    plus(s(x),y) -> plus(x,s(y))
    plus(s(x),y) -> s(plus(y,x))
    ack(0(),x) -> s(x)
    ack(0(),x) -> plus(x,s(0()))
    p(s(x)) -> x
    p(0()) -> 0()
    minus(minus(x,y),z) -> minus(x,plus(y,z))
    minus(0(),y) -> 0()
    minus(x,0()) -> x
    minus(s(x),s(y)) -> minus(x,y)
    ack(s(x),0()) -> ack(x,s(0()))
    ack(s(x),s(y)) -> ack(x,ack(s(x),y))
   TDG Processor:
    DPs:
     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),y) -> plus#(x,s(y))
     plus#(s(x),y) -> plus#(y,x)
     div#(x,y) -> quot#(x,y,0())
     quot#(s(x),s(y),z) -> ack#(0(),x)
     quot#(s(x),s(y),z) -> p#(ack(0(),x))
     quot#(s(x),s(y),z) -> minus#(p(ack(0(),x)),y)
     quot#(s(x),s(y),z) -> quot#(minus(p(ack(0(),x)),y),s(y),s(z))
     ack#(0(),x) -> plus#(x,s(0()))
     ack#(s(x),0()) -> ack#(x,s(0()))
     ack#(s(x),s(y)) -> ack#(s(x),y)
     ack#(s(x),s(y)) -> ack#(x,ack(s(x),y))
    TRS:
     f18(x,y) -> x
     f18(x,y) -> y
     plus(0(),y) -> y
     plus(s(x),y) -> plus(x,s(y))
     plus(s(x),y) -> s(plus(y,x))
     ack(0(),x) -> s(x)
     ack(0(),x) -> plus(x,s(0()))
     p(s(x)) -> x
     p(0()) -> 0()
     minus(minus(x,y),z) -> minus(x,plus(y,z))
     minus(0(),y) -> 0()
     minus(x,0()) -> x
     minus(s(x),s(y)) -> minus(x,y)
     ack(s(x),0()) -> ack(x,s(0()))
     ack(s(x),s(y)) -> ack(x,ack(s(x),y))
    graph:
     ack#(s(x),s(y)) -> ack#(s(x),y) ->
     ack#(s(x),s(y)) -> ack#(x,ack(s(x),y))
     ack#(s(x),s(y)) -> ack#(s(x),y) ->
     ack#(s(x),s(y)) -> ack#(s(x),y)
     ack#(s(x),s(y)) -> ack#(s(x),y) ->
     ack#(s(x),0()) -> ack#(x,s(0()))
     ack#(s(x),s(y)) -> ack#(s(x),y) ->
     ack#(0(),x) -> plus#(x,s(0()))
     ack#(s(x),s(y)) -> ack#(x,ack(s(x),y)) ->
     ack#(s(x),s(y)) -> ack#(x,ack(s(x),y))
     ack#(s(x),s(y)) -> ack#(x,ack(s(x),y)) ->
     ack#(s(x),s(y)) -> ack#(s(x),y)
     ack#(s(x),s(y)) -> ack#(x,ack(s(x),y)) ->
     ack#(s(x),0()) -> ack#(x,s(0()))
     ack#(s(x),s(y)) -> ack#(x,ack(s(x),y)) ->
     ack#(0(),x) -> plus#(x,s(0()))
     ack#(s(x),0()) -> ack#(x,s(0())) ->
     ack#(s(x),s(y)) -> ack#(x,ack(s(x),y))
     ack#(s(x),0()) -> ack#(x,s(0())) ->
     ack#(s(x),s(y)) -> ack#(s(x),y)
     ack#(s(x),0()) -> ack#(x,s(0())) ->
     ack#(s(x),0()) -> ack#(x,s(0()))
     ack#(s(x),0()) -> ack#(x,s(0())) ->
     ack#(0(),x) -> plus#(x,s(0()))
     ack#(0(),x) -> plus#(x,s(0())) -> plus#(s(x),y) -> plus#(y,x)
     ack#(0(),x) -> plus#(x,s(0())) ->
     plus#(s(x),y) -> plus#(x,s(y))
     quot#(s(x),s(y),z) -> ack#(0(),x) ->
     ack#(s(x),s(y)) -> ack#(x,ack(s(x),y))
     quot#(s(x),s(y),z) -> ack#(0(),x) ->
     ack#(s(x),s(y)) -> ack#(s(x),y)
     quot#(s(x),s(y),z) -> ack#(0(),x) ->
     ack#(s(x),0()) -> ack#(x,s(0()))
     quot#(s(x),s(y),z) -> ack#(0(),x) ->
     ack#(0(),x) -> plus#(x,s(0()))
     quot#(s(x),s(y),z) -> quot#(minus(p(ack(0(),x)),y),s(y),s(z)) ->
     quot#(s(x),s(y),z) -> quot#(minus(p(ack(0(),x)),y),s(y),s(z))
     quot#(s(x),s(y),z) -> quot#(minus(p(ack(0(),x)),y),s(y),s(z)) ->
     quot#(s(x),s(y),z) -> minus#(p(ack(0(),x)),y)
     quot#(s(x),s(y),z) -> quot#(minus(p(ack(0(),x)),y),s(y),s(z)) ->
     quot#(s(x),s(y),z) -> p#(ack(0(),x))
     quot#(s(x),s(y),z) -> quot#(minus(p(ack(0(),x)),y),s(y),s(z)) ->
     quot#(s(x),s(y),z) -> ack#(0(),x)
     quot#(s(x),s(y),z) -> minus#(p(ack(0(),x)),y) ->
     minus#(s(x),s(y)) -> minus#(x,y)
     quot#(s(x),s(y),z) -> minus#(p(ack(0(),x)),y) ->
     minus#(minus(x,y),z) -> minus#(x,plus(y,z))
     quot#(s(x),s(y),z) -> minus#(p(ack(0(),x)),y) ->
     minus#(minus(x,y),z) -> plus#(y,z)
     div#(x,y) -> quot#(x,y,0()) ->
     quot#(s(x),s(y),z) -> quot#(minus(p(ack(0(),x)),y),s(y),s(z))
     div#(x,y) -> quot#(x,y,0()) ->
     quot#(s(x),s(y),z) -> minus#(p(ack(0(),x)),y)
     div#(x,y) -> quot#(x,y,0()) -> quot#(s(x),s(y),z) -> p#(ack(0(),x))
     div#(x,y) -> quot#(x,y,0()) -> quot#(s(x),s(y),z) -> ack#(0(),x)
     plus#(s(x),y) -> plus#(y,x) -> plus#(s(x),y) -> plus#(y,x)
     plus#(s(x),y) -> plus#(y,x) -> plus#(s(x),y) -> plus#(x,s(y))
     plus#(s(x),y) -> plus#(x,s(y)) -> plus#(s(x),y) -> plus#(y,x)
     plus#(s(x),y) -> plus#(x,s(y)) ->
     plus#(s(x),y) -> plus#(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) ->
     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#(minus(x,y),z) -> plus#(y,z) ->
     plus#(s(x),y) -> plus#(y,x)
     minus#(minus(x,y),z) -> plus#(y,z) ->
     plus#(s(x),y) -> plus#(x,s(y))
     minus#(minus(x,y),z) -> minus#(x,plus(y,z)) ->
     minus#(s(x),s(y)) -> minus#(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)
    Restore Modifier:
     DPs:
      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),y) -> plus#(x,s(y))
      plus#(s(x),y) -> plus#(y,x)
      div#(x,y) -> quot#(x,y,0())
      quot#(s(x),s(y),z) -> ack#(0(),x)
      quot#(s(x),s(y),z) -> p#(ack(0(),x))
      quot#(s(x),s(y),z) -> minus#(p(ack(0(),x)),y)
      quot#(s(x),s(y),z) -> quot#(minus(p(ack(0(),x)),y),s(y),s(z))
      ack#(0(),x) -> plus#(x,s(0()))
      ack#(s(x),0()) -> ack#(x,s(0()))
      ack#(s(x),s(y)) -> ack#(s(x),y)
      ack#(s(x),s(y)) -> ack#(x,ack(s(x),y))
     TRS:
      minus(minus(x,y),z) -> minus(x,plus(y,z))
      minus(0(),y) -> 0()
      minus(x,0()) -> x
      minus(s(x),s(y)) -> minus(x,y)
      plus(0(),y) -> y
      plus(s(x),y) -> plus(x,s(y))
      plus(s(x),y) -> s(plus(y,x))
      zero(s(x)) -> false()
      zero(0()) -> true()
      p(s(x)) -> x
      p(0()) -> 0()
      div(x,y) -> quot(x,y,0())
      quot(s(x),s(y),z) -> quot(minus(p(ack(0(),x)),y),s(y),s(z))
      quot(0(),s(y),z) -> z
      ack(0(),x) -> s(x)
      ack(0(),x) -> plus(x,s(0()))
      ack(s(x),0()) -> ack(x,s(0()))
      ack(s(x),s(y)) -> ack(x,ack(s(x),y))
     SCC Processor:
      #sccs: 4
      #rules: 8
      #arcs: 41/196
      DPs:
       quot#(s(x),s(y),z) -> quot#(minus(p(ack(0(),x)),y),s(y),s(z))
      TRS:
       minus(minus(x,y),z) -> minus(x,plus(y,z))
       minus(0(),y) -> 0()
       minus(x,0()) -> x
       minus(s(x),s(y)) -> minus(x,y)
       plus(0(),y) -> y
       plus(s(x),y) -> plus(x,s(y))
       plus(s(x),y) -> s(plus(y,x))
       zero(s(x)) -> false()
       zero(0()) -> true()
       p(s(x)) -> x
       p(0()) -> 0()
       div(x,y) -> quot(x,y,0())
       quot(s(x),s(y),z) -> quot(minus(p(ack(0(),x)),y),s(y),s(z))
       quot(0(),s(y),z) -> z
       ack(0(),x) -> s(x)
       ack(0(),x) -> plus(x,s(0()))
       ack(s(x),0()) -> ack(x,s(0()))
       ack(s(x),s(y)) -> ack(x,ack(s(x),y))
      Open
      
      DPs:
       minus#(minus(x,y),z) -> minus#(x,plus(y,z))
       minus#(s(x),s(y)) -> minus#(x,y)
      TRS:
       minus(minus(x,y),z) -> minus(x,plus(y,z))
       minus(0(),y) -> 0()
       minus(x,0()) -> x
       minus(s(x),s(y)) -> minus(x,y)
       plus(0(),y) -> y
       plus(s(x),y) -> plus(x,s(y))
       plus(s(x),y) -> s(plus(y,x))
       zero(s(x)) -> false()
       zero(0()) -> true()
       p(s(x)) -> x
       p(0()) -> 0()
       div(x,y) -> quot(x,y,0())
       quot(s(x),s(y),z) -> quot(minus(p(ack(0(),x)),y),s(y),s(z))
       quot(0(),s(y),z) -> z
       ack(0(),x) -> s(x)
       ack(0(),x) -> plus(x,s(0()))
       ack(s(x),0()) -> ack(x,s(0()))
       ack(s(x),s(y)) -> ack(x,ack(s(x),y))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [minus#](x0, x1) = x0 + 1,
        
        [ack](x0, x1) = x1,
        
        [quot](x0, x1, x2) = x1 + x2 + 1,
        
        [div](x0, x1) = x1 + 1,
        
        [p](x0) = x0,
        
        [true] = 0,
        
        [false] = 0,
        
        [zero](x0) = 0,
        
        [s](x0) = x0,
        
        [0] = 0,
        
        [plus](x0, x1) = x0 + x1,
        
        [minus](x0, x1) = x0 + x1 + 1
       orientation:
        minus#(minus(x,y),z) = x + y + 2 >= x + 1 = minus#(x,plus(y,z))
        
        minus#(s(x),s(y)) = x + 1 >= x + 1 = minus#(x,y)
        
        minus(minus(x,y),z) = x + y + z + 2 >= x + y + z + 1 = minus(x,plus(y,z))
        
        minus(0(),y) = y + 1 >= 0 = 0()
        
        minus(x,0()) = x + 1 >= x = x
        
        minus(s(x),s(y)) = x + y + 1 >= x + y + 1 = minus(x,y)
        
        plus(0(),y) = y >= y = y
        
        plus(s(x),y) = x + y >= x + y = plus(x,s(y))
        
        plus(s(x),y) = x + y >= x + y = s(plus(y,x))
        
        zero(s(x)) = 0 >= 0 = false()
        
        zero(0()) = 0 >= 0 = true()
        
        p(s(x)) = x >= x = x
        
        p(0()) = 0 >= 0 = 0()
        
        div(x,y) = y + 1 >= y + 1 = quot(x,y,0())
        
        quot(s(x),s(y),z) = y + z + 1 >= y + z + 1 = quot(minus(p(ack(0(),x)),y),s(y),s(z))
        
        quot(0(),s(y),z) = y + z + 1 >= z = z
        
        ack(0(),x) = x >= x = s(x)
        
        ack(0(),x) = x >= x = plus(x,s(0()))
        
        ack(s(x),0()) = 0 >= 0 = ack(x,s(0()))
        
        ack(s(x),s(y)) = y >= y = ack(x,ack(s(x),y))
       problem:
        DPs:
         minus#(s(x),s(y)) -> minus#(x,y)
        TRS:
         minus(minus(x,y),z) -> minus(x,plus(y,z))
         minus(0(),y) -> 0()
         minus(x,0()) -> x
         minus(s(x),s(y)) -> minus(x,y)
         plus(0(),y) -> y
         plus(s(x),y) -> plus(x,s(y))
         plus(s(x),y) -> s(plus(y,x))
         zero(s(x)) -> false()
         zero(0()) -> true()
         p(s(x)) -> x
         p(0()) -> 0()
         div(x,y) -> quot(x,y,0())
         quot(s(x),s(y),z) -> quot(minus(p(ack(0(),x)),y),s(y),s(z))
         quot(0(),s(y),z) -> z
         ack(0(),x) -> s(x)
         ack(0(),x) -> plus(x,s(0()))
         ack(s(x),0()) -> ack(x,s(0()))
         ack(s(x),s(y)) -> ack(x,ack(s(x),y))
       Open
      
      DPs:
       ack#(s(x),s(y)) -> ack#(s(x),y)
       ack#(s(x),0()) -> ack#(x,s(0()))
       ack#(s(x),s(y)) -> ack#(x,ack(s(x),y))
      TRS:
       minus(minus(x,y),z) -> minus(x,plus(y,z))
       minus(0(),y) -> 0()
       minus(x,0()) -> x
       minus(s(x),s(y)) -> minus(x,y)
       plus(0(),y) -> y
       plus(s(x),y) -> plus(x,s(y))
       plus(s(x),y) -> s(plus(y,x))
       zero(s(x)) -> false()
       zero(0()) -> true()
       p(s(x)) -> x
       p(0()) -> 0()
       div(x,y) -> quot(x,y,0())
       quot(s(x),s(y),z) -> quot(minus(p(ack(0(),x)),y),s(y),s(z))
       quot(0(),s(y),z) -> z
       ack(0(),x) -> s(x)
       ack(0(),x) -> plus(x,s(0()))
       ack(s(x),0()) -> ack(x,s(0()))
       ack(s(x),s(y)) -> ack(x,ack(s(x),y))
      Open
      
      DPs:
       plus#(s(x),y) -> plus#(x,s(y))
       plus#(s(x),y) -> plus#(y,x)
      TRS:
       minus(minus(x,y),z) -> minus(x,plus(y,z))
       minus(0(),y) -> 0()
       minus(x,0()) -> x
       minus(s(x),s(y)) -> minus(x,y)
       plus(0(),y) -> y
       plus(s(x),y) -> plus(x,s(y))
       plus(s(x),y) -> s(plus(y,x))
       zero(s(x)) -> false()
       zero(0()) -> true()
       p(s(x)) -> x
       p(0()) -> 0()
       div(x,y) -> quot(x,y,0())
       quot(s(x),s(y),z) -> quot(minus(p(ack(0(),x)),y),s(y),s(z))
       quot(0(),s(y),z) -> z
       ack(0(),x) -> s(x)
       ack(0(),x) -> plus(x,s(0()))
       ack(s(x),0()) -> ack(x,s(0()))
       ack(s(x),s(y)) -> ack(x,ack(s(x),y))
      Open