MAYBE

Problem:
 quot(0(),s(y),s(z)) -> 0()
 quot(s(x),s(y),z) -> quot(x,y,z)
 plus(0(),y) -> y
 plus(s(x),y) -> s(plus(x,y))
 quot(x,0(),s(z)) -> s(quot(x,plus(z,s(0())),s(z)))

Proof:
 DP Processor:
  DPs:
   quot#(s(x),s(y),z) -> quot#(x,y,z)
   plus#(s(x),y) -> plus#(x,y)
   quot#(x,0(),s(z)) -> plus#(z,s(0()))
   quot#(x,0(),s(z)) -> quot#(x,plus(z,s(0())),s(z))
  TRS:
   quot(0(),s(y),s(z)) -> 0()
   quot(s(x),s(y),z) -> quot(x,y,z)
   plus(0(),y) -> y
   plus(s(x),y) -> s(plus(x,y))
   quot(x,0(),s(z)) -> s(quot(x,plus(z,s(0())),s(z)))
  Usable Rule Processor:
   DPs:
    quot#(s(x),s(y),z) -> quot#(x,y,z)
    plus#(s(x),y) -> plus#(x,y)
    quot#(x,0(),s(z)) -> plus#(z,s(0()))
    quot#(x,0(),s(z)) -> quot#(x,plus(z,s(0())),s(z))
   TRS:
    plus(0(),y) -> y
    plus(s(x),y) -> s(plus(x,y))
   EDG Processor:
    DPs:
     quot#(s(x),s(y),z) -> quot#(x,y,z)
     plus#(s(x),y) -> plus#(x,y)
     quot#(x,0(),s(z)) -> plus#(z,s(0()))
     quot#(x,0(),s(z)) -> quot#(x,plus(z,s(0())),s(z))
    TRS:
     plus(0(),y) -> y
     plus(s(x),y) -> s(plus(x,y))
    graph:
     plus#(s(x),y) -> plus#(x,y) -> plus#(s(x),y) -> plus#(x,y)
     quot#(s(x),s(y),z) -> quot#(x,y,z) ->
     quot#(s(x),s(y),z) -> quot#(x,y,z)
     quot#(s(x),s(y),z) -> quot#(x,y,z) ->
     quot#(x,0(),s(z)) -> plus#(z,s(0()))
     quot#(s(x),s(y),z) -> quot#(x,y,z) ->
     quot#(x,0(),s(z)) -> quot#(x,plus(z,s(0())),s(z))
     quot#(x,0(),s(z)) -> plus#(z,s(0())) ->
     plus#(s(x),y) -> plus#(x,y)
     quot#(x,0(),s(z)) -> quot#(x,plus(z,s(0())),s(z)) ->
     quot#(s(x),s(y),z) -> quot#(x,y,z)
     quot#(x,0(),s(z)) -> quot#(x,plus(z,s(0())),s(z)) ->
     quot#(x,0(),s(z)) -> plus#(z,s(0()))
     quot#(x,0(),s(z)) -> quot#(x,plus(z,s(0())),s(z)) ->
     quot#(x,0(),s(z)) -> quot#(x,plus(z,s(0())),s(z))
    Restore Modifier:
     DPs:
      quot#(s(x),s(y),z) -> quot#(x,y,z)
      plus#(s(x),y) -> plus#(x,y)
      quot#(x,0(),s(z)) -> plus#(z,s(0()))
      quot#(x,0(),s(z)) -> quot#(x,plus(z,s(0())),s(z))
     TRS:
      quot(0(),s(y),s(z)) -> 0()
      quot(s(x),s(y),z) -> quot(x,y,z)
      plus(0(),y) -> y
      plus(s(x),y) -> s(plus(x,y))
      quot(x,0(),s(z)) -> s(quot(x,plus(z,s(0())),s(z)))
     SCC Processor:
      #sccs: 2
      #rules: 3
      #arcs: 8/16
      DPs:
       quot#(s(x),s(y),z) -> quot#(x,y,z)
       quot#(x,0(),s(z)) -> quot#(x,plus(z,s(0())),s(z))
      TRS:
       quot(0(),s(y),s(z)) -> 0()
       quot(s(x),s(y),z) -> quot(x,y,z)
       plus(0(),y) -> y
       plus(s(x),y) -> s(plus(x,y))
       quot(x,0(),s(z)) -> s(quot(x,plus(z,s(0())),s(z)))
      Open
      
      DPs:
       plus#(s(x),y) -> plus#(x,y)
      TRS:
       quot(0(),s(y),s(z)) -> 0()
       quot(s(x),s(y),z) -> quot(x,y,z)
       plus(0(),y) -> y
       plus(s(x),y) -> s(plus(x,y))
       quot(x,0(),s(z)) -> s(quot(x,plus(z,s(0())),s(z)))
      Open