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)))
  TDG 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)))
   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#(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)) -> plus#(z,s(0()))
    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())) ->
    plus#(s(x),y) -> plus#(x,y)
    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))
    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#(s(x),s(y),z) -> quot#(x,y,z)
   CDG 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)))
    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)
    SCC Processor:
     #sccs: 2
     #rules: 3
     #arcs: 6/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