MAYBE

Problem:
 quot(0(),s(y),s(z)) -> 0()
 quot(s(x),s(y),z) -> quot(x,y,z)
 plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))))
 plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x))
 plus(zero(),y) -> y
 plus(id(x),s(y)) -> s(plus(x,if(gt(s(y),y),y,s(y))))
 id(x) -> x
 if(true(),x,y) -> x
 if(false(),x,y) -> y
 not(x) -> if(x,false(),true())
 gt(s(x),zero()) -> true()
 gt(zero(),y) -> false()
 gt(s(x),s(y)) -> gt(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),s(y)) -> id#(y)
   plus#(s(x),s(y)) -> id#(x)
   plus#(s(x),s(y)) -> not#(gt(x,y))
   plus#(s(x),s(y)) -> if#(not(gt(x,y)),id(x),id(y))
   plus#(s(x),s(y)) -> gt#(x,y)
   plus#(s(x),s(y)) -> if#(gt(x,y),x,y)
   plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))
   plus#(s(x),x) -> id#(x)
   plus#(s(x),x) -> gt#(x,x)
   plus#(s(x),x) -> if#(gt(x,x),id(x),id(x))
   plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x))
   plus#(id(x),s(y)) -> gt#(s(y),y)
   plus#(id(x),s(y)) -> if#(gt(s(y),y),y,s(y))
   plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y)))
   not#(x) -> if#(x,false(),true())
   gt#(s(x),s(y)) -> gt#(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(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))))
   plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x))
   plus(zero(),y) -> y
   plus(id(x),s(y)) -> s(plus(x,if(gt(s(y),y),y,s(y))))
   id(x) -> x
   if(true(),x,y) -> x
   if(false(),x,y) -> y
   not(x) -> if(x,false(),true())
   gt(s(x),zero()) -> true()
   gt(zero(),y) -> false()
   gt(s(x),s(y)) -> gt(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),s(y)) -> id#(y)
    plus#(s(x),s(y)) -> id#(x)
    plus#(s(x),s(y)) -> not#(gt(x,y))
    plus#(s(x),s(y)) -> if#(not(gt(x,y)),id(x),id(y))
    plus#(s(x),s(y)) -> gt#(x,y)
    plus#(s(x),s(y)) -> if#(gt(x,y),x,y)
    plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))
    plus#(s(x),x) -> id#(x)
    plus#(s(x),x) -> gt#(x,x)
    plus#(s(x),x) -> if#(gt(x,x),id(x),id(x))
    plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x))
    plus#(id(x),s(y)) -> gt#(s(y),y)
    plus#(id(x),s(y)) -> if#(gt(s(y),y),y,s(y))
    plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y)))
    not#(x) -> if#(x,false(),true())
    gt#(s(x),s(y)) -> gt#(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(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))))
    plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x))
    plus(zero(),y) -> y
    plus(id(x),s(y)) -> s(plus(x,if(gt(s(y),y),y,s(y))))
    id(x) -> x
    if(true(),x,y) -> x
    if(false(),x,y) -> y
    not(x) -> if(x,false(),true())
    gt(s(x),zero()) -> true()
    gt(zero(),y) -> false()
    gt(s(x),s(y)) -> gt(x,y)
    quot(x,0(),s(z)) -> s(quot(x,plus(z,s(0())),s(z)))
   graph:
    gt#(s(x),s(y)) -> gt#(x,y) -> gt#(s(x),s(y)) -> gt#(x,y)
    plus#(id(x),s(y)) -> gt#(s(y),y) ->
    gt#(s(x),s(y)) -> gt#(x,y)
    plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) ->
    plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y)))
    plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) ->
    plus#(id(x),s(y)) -> if#(gt(s(y),y),y,s(y))
    plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) ->
    plus#(id(x),s(y)) -> gt#(s(y),y)
    plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) ->
    plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x))
    plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) ->
    plus#(s(x),x) -> if#(gt(x,x),id(x),id(x))
    plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) ->
    plus#(s(x),x) -> gt#(x,x)
    plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) ->
    plus#(s(x),x) -> id#(x)
    plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) ->
    plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))
    plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) ->
    plus#(s(x),s(y)) -> if#(gt(x,y),x,y)
    plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) ->
    plus#(s(x),s(y)) -> gt#(x,y)
    plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) ->
    plus#(s(x),s(y)) -> if#(not(gt(x,y)),id(x),id(y))
    plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) ->
    plus#(s(x),s(y)) -> not#(gt(x,y))
    plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) ->
    plus#(s(x),s(y)) -> id#(x)
    plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) ->
    plus#(s(x),s(y)) -> id#(y)
    plus#(s(x),s(y)) -> gt#(x,y) -> gt#(s(x),s(y)) -> gt#(x,y)
    plus#(s(x),s(y)) -> not#(gt(x,y)) ->
    not#(x) -> if#(x,false(),true())
    plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
    plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y)))
    plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
    plus#(id(x),s(y)) -> if#(gt(s(y),y),y,s(y))
    plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
    plus#(id(x),s(y)) -> gt#(s(y),y)
    plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
    plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x))
    plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
    plus#(s(x),x) -> if#(gt(x,x),id(x),id(x))
    plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
    plus#(s(x),x) -> gt#(x,x)
    plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
    plus#(s(x),x) -> id#(x)
    plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
    plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))
    plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
    plus#(s(x),s(y)) -> if#(gt(x,y),x,y)
    plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
    plus#(s(x),s(y)) -> gt#(x,y)
    plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
    plus#(s(x),s(y)) -> if#(not(gt(x,y)),id(x),id(y))
    plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
    plus#(s(x),s(y)) -> not#(gt(x,y))
    plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
    plus#(s(x),s(y)) -> id#(x)
    plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
    plus#(s(x),s(y)) -> id#(y)
    plus#(s(x),x) -> gt#(x,x) ->
    gt#(s(x),s(y)) -> gt#(x,y)
    plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) ->
    plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y)))
    plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) ->
    plus#(id(x),s(y)) -> if#(gt(s(y),y),y,s(y))
    plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) ->
    plus#(id(x),s(y)) -> gt#(s(y),y)
    plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) ->
    plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x))
    plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) ->
    plus#(s(x),x) -> if#(gt(x,x),id(x),id(x))
    plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) ->
    plus#(s(x),x) -> gt#(x,x)
    plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) ->
    plus#(s(x),x) -> id#(x)
    plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) ->
    plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))
    plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) ->
    plus#(s(x),s(y)) -> if#(gt(x,y),x,y)
    plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) ->
    plus#(s(x),s(y)) -> gt#(x,y)
    plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) ->
    plus#(s(x),s(y)) -> if#(not(gt(x,y)),id(x),id(y))
    plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) ->
    plus#(s(x),s(y)) -> not#(gt(x,y))
    plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) ->
    plus#(s(x),s(y)) -> id#(x)
    plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) ->
    plus#(s(x),s(y)) -> id#(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#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y)))
    quot#(x,0(),s(z)) -> plus#(z,s(0())) ->
    plus#(id(x),s(y)) -> if#(gt(s(y),y),y,s(y))
    quot#(x,0(),s(z)) -> plus#(z,s(0())) ->
    plus#(id(x),s(y)) -> gt#(s(y),y)
    quot#(x,0(),s(z)) -> plus#(z,s(0())) ->
    plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x))
    quot#(x,0(),s(z)) -> plus#(z,s(0())) ->
    plus#(s(x),x) -> if#(gt(x,x),id(x),id(x))
    quot#(x,0(),s(z)) -> plus#(z,s(0())) ->
    plus#(s(x),x) -> gt#(x,x)
    quot#(x,0(),s(z)) -> plus#(z,s(0())) ->
    plus#(s(x),x) -> id#(x)
    quot#(x,0(),s(z)) -> plus#(z,s(0())) ->
    plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))
    quot#(x,0(),s(z)) -> plus#(z,s(0())) ->
    plus#(s(x),s(y)) -> if#(gt(x,y),x,y)
    quot#(x,0(),s(z)) -> plus#(z,s(0())) ->
    plus#(s(x),s(y)) -> gt#(x,y)
    quot#(x,0(),s(z)) -> plus#(z,s(0())) ->
    plus#(s(x),s(y)) -> if#(not(gt(x,y)),id(x),id(y))
    quot#(x,0(),s(z)) -> plus#(z,s(0())) ->
    plus#(s(x),s(y)) -> not#(gt(x,y))
    quot#(x,0(),s(z)) -> plus#(z,s(0())) ->
    plus#(s(x),s(y)) -> id#(x)
    quot#(x,0(),s(z)) -> plus#(z,s(0())) ->
    plus#(s(x),s(y)) -> id#(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)
   EDG Processor:
    DPs:
     quot#(s(x),s(y),z) -> quot#(x,y,z)
     plus#(s(x),s(y)) -> id#(y)
     plus#(s(x),s(y)) -> id#(x)
     plus#(s(x),s(y)) -> not#(gt(x,y))
     plus#(s(x),s(y)) -> if#(not(gt(x,y)),id(x),id(y))
     plus#(s(x),s(y)) -> gt#(x,y)
     plus#(s(x),s(y)) -> if#(gt(x,y),x,y)
     plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))
     plus#(s(x),x) -> id#(x)
     plus#(s(x),x) -> gt#(x,x)
     plus#(s(x),x) -> if#(gt(x,x),id(x),id(x))
     plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x))
     plus#(id(x),s(y)) -> gt#(s(y),y)
     plus#(id(x),s(y)) -> if#(gt(s(y),y),y,s(y))
     plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y)))
     not#(x) -> if#(x,false(),true())
     gt#(s(x),s(y)) -> gt#(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(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))))
     plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x))
     plus(zero(),y) -> y
     plus(id(x),s(y)) -> s(plus(x,if(gt(s(y),y),y,s(y))))
     id(x) -> x
     if(true(),x,y) -> x
     if(false(),x,y) -> y
     not(x) -> if(x,false(),true())
     gt(s(x),zero()) -> true()
     gt(zero(),y) -> false()
     gt(s(x),s(y)) -> gt(x,y)
     quot(x,0(),s(z)) -> s(quot(x,plus(z,s(0())),s(z)))
    graph:
     gt#(s(x),s(y)) -> gt#(x,y) -> gt#(s(x),s(y)) -> gt#(x,y)
     plus#(s(x),s(y)) -> gt#(x,y) -> gt#(s(x),s(y)) -> gt#(x,y)
     plus#(s(x),s(y)) -> not#(gt(x,y)) ->
     not#(x) -> if#(x,false(),true())
     plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
     plus#(s(x),s(y)) -> id#(y)
     plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
     plus#(s(x),s(y)) -> id#(x)
     plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
     plus#(s(x),s(y)) -> not#(gt(x,y))
     plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
     plus#(s(x),s(y)) -> if#(not(gt(x,y)),id(x),id(y))
     plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
     plus#(s(x),s(y)) -> gt#(x,y)
     plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
     plus#(s(x),s(y)) -> if#(gt(x,y),x,y)
     plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
     plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))
     plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
     plus#(s(x),x) -> id#(x)
     plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
     plus#(s(x),x) -> gt#(x,x)
     plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
     plus#(s(x),x) -> if#(gt(x,x),id(x),id(x))
     plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
     plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x))
     plus#(s(x),x) -> gt#(x,x) ->
     gt#(s(x),s(y)) -> gt#(x,y)
     plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) ->
     plus#(s(x),s(y)) -> id#(y)
     plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) ->
     plus#(s(x),s(y)) -> id#(x)
     plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) ->
     plus#(s(x),s(y)) -> not#(gt(x,y))
     plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) ->
     plus#(s(x),s(y)) -> if#(not(gt(x,y)),id(x),id(y))
     plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) ->
     plus#(s(x),s(y)) -> gt#(x,y)
     plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) ->
     plus#(s(x),s(y)) -> if#(gt(x,y),x,y)
     plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) ->
     plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))
     plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) ->
     plus#(s(x),x) -> id#(x)
     plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) ->
     plus#(s(x),x) -> gt#(x,x)
     plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) ->
     plus#(s(x),x) -> if#(gt(x,x),id(x),id(x))
     plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) ->
     plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x))
     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),s(y)) -> id#(y)
     quot#(x,0(),s(z)) -> plus#(z,s(0())) ->
     plus#(s(x),s(y)) -> id#(x)
     quot#(x,0(),s(z)) -> plus#(z,s(0())) ->
     plus#(s(x),s(y)) -> not#(gt(x,y))
     quot#(x,0(),s(z)) -> plus#(z,s(0())) ->
     plus#(s(x),s(y)) -> if#(not(gt(x,y)),id(x),id(y))
     quot#(x,0(),s(z)) -> plus#(z,s(0())) ->
     plus#(s(x),s(y)) -> gt#(x,y)
     quot#(x,0(),s(z)) -> plus#(z,s(0())) ->
     plus#(s(x),s(y)) -> if#(gt(x,y),x,y)
     quot#(x,0(),s(z)) -> plus#(z,s(0())) ->
     plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))
     quot#(x,0(),s(z)) -> plus#(z,s(0())) ->
     plus#(s(x),x) -> id#(x)
     quot#(x,0(),s(z)) -> plus#(z,s(0())) ->
     plus#(s(x),x) -> gt#(x,x)
     quot#(x,0(),s(z)) -> plus#(z,s(0())) ->
     plus#(s(x),x) -> if#(gt(x,x),id(x),id(x))
     quot#(x,0(),s(z)) -> plus#(z,s(0())) ->
     plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x))
     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))
    SCC Processor:
     #sccs: 3
     #rules: 5
     #arcs: 43/361
     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(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))))
      plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x))
      plus(zero(),y) -> y
      plus(id(x),s(y)) -> s(plus(x,if(gt(s(y),y),y,s(y))))
      id(x) -> x
      if(true(),x,y) -> x
      if(false(),x,y) -> y
      not(x) -> if(x,false(),true())
      gt(s(x),zero()) -> true()
      gt(zero(),y) -> false()
      gt(s(x),s(y)) -> gt(x,y)
      quot(x,0(),s(z)) -> s(quot(x,plus(z,s(0())),s(z)))
     Open
     
     DPs:
      plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))
      plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x))
     TRS:
      quot(0(),s(y),s(z)) -> 0()
      quot(s(x),s(y),z) -> quot(x,y,z)
      plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))))
      plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x))
      plus(zero(),y) -> y
      plus(id(x),s(y)) -> s(plus(x,if(gt(s(y),y),y,s(y))))
      id(x) -> x
      if(true(),x,y) -> x
      if(false(),x,y) -> y
      not(x) -> if(x,false(),true())
      gt(s(x),zero()) -> true()
      gt(zero(),y) -> false()
      gt(s(x),s(y)) -> gt(x,y)
      quot(x,0(),s(z)) -> s(quot(x,plus(z,s(0())),s(z)))
     Open
     
     DPs:
      gt#(s(x),s(y)) -> gt#(x,y)
     TRS:
      quot(0(),s(y),s(z)) -> 0()
      quot(s(x),s(y),z) -> quot(x,y,z)
      plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))))
      plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x))
      plus(zero(),y) -> y
      plus(id(x),s(y)) -> s(plus(x,if(gt(s(y),y),y,s(y))))
      id(x) -> x
      if(true(),x,y) -> x
      if(false(),x,y) -> y
      not(x) -> if(x,false(),true())
      gt(s(x),zero()) -> true()
      gt(zero(),y) -> false()
      gt(s(x),s(y)) -> gt(x,y)
      quot(x,0(),s(z)) -> s(quot(x,plus(z,s(0())),s(z)))
     Open