MAYBE

Problem:
 g(s(x),s(y)) ->
 if(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))),
    g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
 n(0(),y) -> 0()
 n(x,0()) -> 0()
 n(s(x),s(y)) -> s(n(x,y))
 m(0(),y) -> y
 m(x,0()) -> x
 m(s(x),s(y)) -> s(m(x,y))
 k(0(),s(y)) -> 0()
 k(s(x),s(y)) -> s(k(minus(x,y),s(y)))
 t(x) -> p(x,x)
 p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))))
 p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x))
 p(0(),y) -> y
 p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y))))
 minus(x,0()) -> x
 minus(s(x),s(y)) -> minus(x,y)
 id(x) -> x
 if(true(),x,y) -> x
 if(false(),x,y) -> y
 not(x) -> if(x,false(),true())
 and(x,false()) -> false()
 and(true(),true()) -> true()
 f(0()) -> true()
 f(s(x)) -> h(x)
 h(0()) -> false()
 h(s(x)) -> f(x)
 gt(s(x),0()) -> true()
 gt(0(),y) -> false()
 gt(s(x),s(y)) -> gt(x,y)

Proof:
 DP Processor:
  DPs:
   g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y)))
   g#(s(x),s(y)) -> n#(s(x),s(y))
   g#(s(x),s(y)) -> k#(n(s(x),s(y)),s(s(0())))
   g#(s(x),s(y)) -> n#(x,y)
   g#(s(x),s(y)) -> m#(x,y)
   g#(s(x),s(y)) -> minus#(m(x,y),n(x,y))
   g#(s(x),s(y)) -> k#(minus(m(x,y),n(x,y)),s(s(0())))
   g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))
   g#(s(x),s(y)) -> t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
   g#(s(x),s(y)) -> f#(s(y))
   g#(s(x),s(y)) -> f#(s(x))
   g#(s(x),s(y)) -> and#(f(s(x)),f(s(y)))
   g#(s(x),s(y)) ->
   if#(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))),
       g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
   n#(s(x),s(y)) -> n#(x,y)
   m#(s(x),s(y)) -> m#(x,y)
   k#(s(x),s(y)) -> minus#(x,y)
   k#(s(x),s(y)) -> k#(minus(x,y),s(y))
   t#(x) -> p#(x,x)
   p#(s(x),s(y)) -> id#(y)
   p#(s(x),s(y)) -> id#(x)
   p#(s(x),s(y)) -> not#(gt(x,y))
   p#(s(x),s(y)) -> if#(not(gt(x,y)),id(x),id(y))
   p#(s(x),s(y)) -> gt#(x,y)
   p#(s(x),s(y)) -> if#(gt(x,y),x,y)
   p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))
   p#(s(x),x) -> id#(x)
   p#(s(x),x) -> gt#(x,x)
   p#(s(x),x) -> if#(gt(x,x),id(x),id(x))
   p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x))
   p#(id(x),s(y)) -> gt#(s(y),y)
   p#(id(x),s(y)) -> if#(gt(s(y),y),y,s(y))
   p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y)))
   minus#(s(x),s(y)) -> minus#(x,y)
   not#(x) -> if#(x,false(),true())
   f#(s(x)) -> h#(x)
   h#(s(x)) -> f#(x)
   gt#(s(x),s(y)) -> gt#(x,y)
  TRS:
   g(s(x),s(y)) ->
   if(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))),
      g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
   n(0(),y) -> 0()
   n(x,0()) -> 0()
   n(s(x),s(y)) -> s(n(x,y))
   m(0(),y) -> y
   m(x,0()) -> x
   m(s(x),s(y)) -> s(m(x,y))
   k(0(),s(y)) -> 0()
   k(s(x),s(y)) -> s(k(minus(x,y),s(y)))
   t(x) -> p(x,x)
   p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))))
   p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x))
   p(0(),y) -> y
   p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y))))
   minus(x,0()) -> x
   minus(s(x),s(y)) -> minus(x,y)
   id(x) -> x
   if(true(),x,y) -> x
   if(false(),x,y) -> y
   not(x) -> if(x,false(),true())
   and(x,false()) -> false()
   and(true(),true()) -> true()
   f(0()) -> true()
   f(s(x)) -> h(x)
   h(0()) -> false()
   h(s(x)) -> f(x)
   gt(s(x),0()) -> true()
   gt(0(),y) -> false()
   gt(s(x),s(y)) -> gt(x,y)
  EDG Processor:
   DPs:
    g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y)))
    g#(s(x),s(y)) -> n#(s(x),s(y))
    g#(s(x),s(y)) -> k#(n(s(x),s(y)),s(s(0())))
    g#(s(x),s(y)) -> n#(x,y)
    g#(s(x),s(y)) -> m#(x,y)
    g#(s(x),s(y)) -> minus#(m(x,y),n(x,y))
    g#(s(x),s(y)) -> k#(minus(m(x,y),n(x,y)),s(s(0())))
    g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))
    g#(s(x),s(y)) -> t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
    g#(s(x),s(y)) -> f#(s(y))
    g#(s(x),s(y)) -> f#(s(x))
    g#(s(x),s(y)) -> and#(f(s(x)),f(s(y)))
    g#(s(x),s(y)) ->
    if#(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))),
        g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
    n#(s(x),s(y)) -> n#(x,y)
    m#(s(x),s(y)) -> m#(x,y)
    k#(s(x),s(y)) -> minus#(x,y)
    k#(s(x),s(y)) -> k#(minus(x,y),s(y))
    t#(x) -> p#(x,x)
    p#(s(x),s(y)) -> id#(y)
    p#(s(x),s(y)) -> id#(x)
    p#(s(x),s(y)) -> not#(gt(x,y))
    p#(s(x),s(y)) -> if#(not(gt(x,y)),id(x),id(y))
    p#(s(x),s(y)) -> gt#(x,y)
    p#(s(x),s(y)) -> if#(gt(x,y),x,y)
    p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))
    p#(s(x),x) -> id#(x)
    p#(s(x),x) -> gt#(x,x)
    p#(s(x),x) -> if#(gt(x,x),id(x),id(x))
    p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x))
    p#(id(x),s(y)) -> gt#(s(y),y)
    p#(id(x),s(y)) -> if#(gt(s(y),y),y,s(y))
    p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y)))
    minus#(s(x),s(y)) -> minus#(x,y)
    not#(x) -> if#(x,false(),true())
    f#(s(x)) -> h#(x)
    h#(s(x)) -> f#(x)
    gt#(s(x),s(y)) -> gt#(x,y)
   TRS:
    g(s(x),s(y)) ->
    if(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))),
       g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
    n(0(),y) -> 0()
    n(x,0()) -> 0()
    n(s(x),s(y)) -> s(n(x,y))
    m(0(),y) -> y
    m(x,0()) -> x
    m(s(x),s(y)) -> s(m(x,y))
    k(0(),s(y)) -> 0()
    k(s(x),s(y)) -> s(k(minus(x,y),s(y)))
    t(x) -> p(x,x)
    p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))))
    p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x))
    p(0(),y) -> y
    p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y))))
    minus(x,0()) -> x
    minus(s(x),s(y)) -> minus(x,y)
    id(x) -> x
    if(true(),x,y) -> x
    if(false(),x,y) -> y
    not(x) -> if(x,false(),true())
    and(x,false()) -> false()
    and(true(),true()) -> true()
    f(0()) -> true()
    f(s(x)) -> h(x)
    h(0()) -> false()
    h(s(x)) -> f(x)
    gt(s(x),0()) -> true()
    gt(0(),y) -> false()
    gt(s(x),s(y)) -> gt(x,y)
   graph:
    h#(s(x)) -> f#(x) -> f#(s(x)) -> h#(x)
    gt#(s(x),s(y)) -> gt#(x,y) -> gt#(s(x),s(y)) -> gt#(x,y)
    p#(id(x),s(y)) -> gt#(s(y),y) ->
    gt#(s(x),s(y)) -> gt#(x,y)
    p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) ->
    p#(s(x),s(y)) -> id#(y)
    p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) ->
    p#(s(x),s(y)) -> id#(x)
    p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) ->
    p#(s(x),s(y)) -> not#(gt(x,y))
    p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) ->
    p#(s(x),s(y)) -> if#(not(gt(x,y)),id(x),id(y))
    p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) ->
    p#(s(x),s(y)) -> gt#(x,y)
    p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) ->
    p#(s(x),s(y)) -> if#(gt(x,y),x,y)
    p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) ->
    p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))
    p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) ->
    p#(s(x),x) -> id#(x)
    p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) ->
    p#(s(x),x) -> gt#(x,x)
    p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) ->
    p#(s(x),x) -> if#(gt(x,x),id(x),id(x))
    p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) ->
    p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x))
    p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) ->
    p#(id(x),s(y)) -> gt#(s(y),y)
    p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) ->
    p#(id(x),s(y)) -> if#(gt(s(y),y),y,s(y))
    p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) ->
    p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y)))
    p#(s(x),s(y)) -> gt#(x,y) -> gt#(s(x),s(y)) -> gt#(x,y)
    p#(s(x),s(y)) -> not#(gt(x,y)) ->
    not#(x) -> if#(x,false(),true())
    p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
    p#(s(x),s(y)) -> id#(y)
    p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
    p#(s(x),s(y)) -> id#(x)
    p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
    p#(s(x),s(y)) -> not#(gt(x,y))
    p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
    p#(s(x),s(y)) -> if#(not(gt(x,y)),id(x),id(y))
    p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
    p#(s(x),s(y)) -> gt#(x,y)
    p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
    p#(s(x),s(y)) -> if#(gt(x,y),x,y)
    p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
    p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))
    p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
    p#(s(x),x) -> id#(x)
    p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
    p#(s(x),x) -> gt#(x,x)
    p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
    p#(s(x),x) -> if#(gt(x,x),id(x),id(x))
    p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
    p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x))
    p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
    p#(id(x),s(y)) -> gt#(s(y),y)
    p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
    p#(id(x),s(y)) -> if#(gt(s(y),y),y,s(y))
    p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ->
    p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y)))
    p#(s(x),x) -> gt#(x,x) ->
    gt#(s(x),s(y)) -> gt#(x,y)
    p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) ->
    p#(s(x),s(y)) -> id#(y)
    p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) ->
    p#(s(x),s(y)) -> id#(x)
    p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) ->
    p#(s(x),s(y)) -> not#(gt(x,y))
    p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) ->
    p#(s(x),s(y)) -> if#(not(gt(x,y)),id(x),id(y))
    p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) ->
    p#(s(x),s(y)) -> gt#(x,y)
    p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) ->
    p#(s(x),s(y)) -> if#(gt(x,y),x,y)
    p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) ->
    p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))
    p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) ->
    p#(s(x),x) -> id#(x)
    p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) ->
    p#(s(x),x) -> gt#(x,x)
    p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) ->
    p#(s(x),x) -> if#(gt(x,x),id(x),id(x))
    p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) ->
    p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x))
    p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) ->
    p#(id(x),s(y)) -> gt#(s(y),y)
    p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) ->
    p#(id(x),s(y)) -> if#(gt(s(y),y),y,s(y))
    p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) ->
    p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y)))
    f#(s(x)) -> h#(x) -> h#(s(x)) -> f#(x)
    t#(x) -> p#(x,x) -> p#(s(x),s(y)) -> id#(y)
    t#(x) -> p#(x,x) -> p#(s(x),s(y)) -> id#(x)
    t#(x) -> p#(x,x) -> p#(s(x),s(y)) -> not#(gt(x,y))
    t#(x) -> p#(x,x) -> p#(s(x),s(y)) -> if#(not(gt(x,y)),id(x),id(y))
    t#(x) -> p#(x,x) -> p#(s(x),s(y)) -> gt#(x,y)
    t#(x) -> p#(x,x) -> p#(s(x),s(y)) -> if#(gt(x,y),x,y)
    t#(x) -> p#(x,x) ->
    p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))
    t#(x) -> p#(x,x) -> p#(s(x),x) -> id#(x)
    t#(x) -> p#(x,x) -> p#(s(x),x) -> gt#(x,x)
    t#(x) -> p#(x,x) -> p#(s(x),x) -> if#(gt(x,x),id(x),id(x))
    t#(x) -> p#(x,x) -> p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x))
    t#(x) -> p#(x,x) -> p#(id(x),s(y)) -> gt#(s(y),y)
    t#(x) -> p#(x,x) -> p#(id(x),s(y)) -> if#(gt(s(y),y),y,s(y))
    t#(x) -> p#(x,x) ->
    p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y)))
    minus#(s(x),s(y)) -> minus#(x,y) -> minus#(s(x),s(y)) -> minus#(x,y)
    m#(s(x),s(y)) -> m#(x,y) -> m#(s(x),s(y)) -> m#(x,y)
    k#(s(x),s(y)) -> minus#(x,y) ->
    minus#(s(x),s(y)) -> minus#(x,y)
    k#(s(x),s(y)) -> k#(minus(x,y),s(y)) ->
    k#(s(x),s(y)) -> minus#(x,y)
    k#(s(x),s(y)) -> k#(minus(x,y),s(y)) ->
    k#(s(x),s(y)) -> k#(minus(x,y),s(y))
    n#(s(x),s(y)) -> n#(x,y) -> n#(s(x),s(y)) -> n#(x,y)
    g#(s(x),s(y)) -> f#(s(y)) -> f#(s(x)) -> h#(x)
    g#(s(x),s(y)) -> f#(s(x)) ->
    f#(s(x)) -> h#(x)
    g#(s(x),s(y)) -> t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ->
    t#(x) -> p#(x,x)
    g#(s(x),s(y)) -> minus#(m(x,y),n(x,y)) ->
    minus#(s(x),s(y)) -> minus#(x,y)
    g#(s(x),s(y)) -> m#(x,y) ->
    m#(s(x),s(y)) -> m#(x,y)
    g#(s(x),s(y)) -> k#(minus(m(x,y),n(x,y)),s(s(0()))) ->
    k#(s(x),s(y)) -> minus#(x,y)
    g#(s(x),s(y)) -> k#(minus(m(x,y),n(x,y)),s(s(0()))) ->
    k#(s(x),s(y)) -> k#(minus(x,y),s(y))
    g#(s(x),s(y)) -> k#(n(s(x),s(y)),s(s(0()))) ->
    k#(s(x),s(y)) -> minus#(x,y)
    g#(s(x),s(y)) -> k#(n(s(x),s(y)),s(s(0()))) ->
    k#(s(x),s(y)) -> k#(minus(x,y),s(y))
    g#(s(x),s(y)) -> n#(s(x),s(y)) -> n#(s(x),s(y)) -> n#(x,y)
    g#(s(x),s(y)) -> n#(x,y) ->
    n#(s(x),s(y)) -> n#(x,y)
    g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) ->
    g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y)))
    g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) ->
    g#(s(x),s(y)) -> n#(s(x),s(y))
    g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) ->
    g#(s(x),s(y)) -> k#(n(s(x),s(y)),s(s(0())))
    g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) ->
    g#(s(x),s(y)) -> n#(x,y)
    g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) ->
    g#(s(x),s(y)) -> m#(x,y)
    g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) ->
    g#(s(x),s(y)) -> minus#(m(x,y),n(x,y))
    g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) ->
    g#(s(x),s(y)) -> k#(minus(m(x,y),n(x,y)),s(s(0())))
    g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) ->
    g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))
    g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) ->
    g#(s(x),s(y)) -> t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
    g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) ->
    g#(s(x),s(y)) -> f#(s(y))
    g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) ->
    g#(s(x),s(y)) -> f#(s(x))
    g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) ->
    g#(s(x),s(y)) -> and#(f(s(x)),f(s(y)))
    g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) ->
    g#(s(x),s(y)) ->
    if#(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))),
        g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
    g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) ->
    g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y)))
    g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) ->
    g#(s(x),s(y)) -> n#(s(x),s(y))
    g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) ->
    g#(s(x),s(y)) -> k#(n(s(x),s(y)),s(s(0())))
    g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) ->
    g#(s(x),s(y)) -> n#(x,y)
    g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) ->
    g#(s(x),s(y)) -> m#(x,y)
    g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) ->
    g#(s(x),s(y)) -> minus#(m(x,y),n(x,y))
    g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) ->
    g#(s(x),s(y)) -> k#(minus(m(x,y),n(x,y)),s(s(0())))
    g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) ->
    g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))
    g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) ->
    g#(s(x),s(y)) -> t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
    g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) ->
    g#(s(x),s(y)) -> f#(s(y))
    g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) ->
    g#(s(x),s(y)) -> f#(s(x))
    g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) ->
    g#(s(x),s(y)) -> and#(f(s(x)),f(s(y)))
    g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) ->
    g#(s(x),s(y)) ->
    if#(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))),
        g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
   SCC Processor:
    #sccs: 8
    #rules: 12
    #arcs: 106/1369
    DPs:
     g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))
     g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y)))
    TRS:
     g(s(x),s(y)) ->
     if(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))),
        g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
     n(0(),y) -> 0()
     n(x,0()) -> 0()
     n(s(x),s(y)) -> s(n(x,y))
     m(0(),y) -> y
     m(x,0()) -> x
     m(s(x),s(y)) -> s(m(x,y))
     k(0(),s(y)) -> 0()
     k(s(x),s(y)) -> s(k(minus(x,y),s(y)))
     t(x) -> p(x,x)
     p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))))
     p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x))
     p(0(),y) -> y
     p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y))))
     minus(x,0()) -> x
     minus(s(x),s(y)) -> minus(x,y)
     id(x) -> x
     if(true(),x,y) -> x
     if(false(),x,y) -> y
     not(x) -> if(x,false(),true())
     and(x,false()) -> false()
     and(true(),true()) -> true()
     f(0()) -> true()
     f(s(x)) -> h(x)
     h(0()) -> false()
     h(s(x)) -> f(x)
     gt(s(x),0()) -> true()
     gt(0(),y) -> false()
     gt(s(x),s(y)) -> gt(x,y)
    Open
    
    DPs:
     n#(s(x),s(y)) -> n#(x,y)
    TRS:
     g(s(x),s(y)) ->
     if(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))),
        g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
     n(0(),y) -> 0()
     n(x,0()) -> 0()
     n(s(x),s(y)) -> s(n(x,y))
     m(0(),y) -> y
     m(x,0()) -> x
     m(s(x),s(y)) -> s(m(x,y))
     k(0(),s(y)) -> 0()
     k(s(x),s(y)) -> s(k(minus(x,y),s(y)))
     t(x) -> p(x,x)
     p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))))
     p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x))
     p(0(),y) -> y
     p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y))))
     minus(x,0()) -> x
     minus(s(x),s(y)) -> minus(x,y)
     id(x) -> x
     if(true(),x,y) -> x
     if(false(),x,y) -> y
     not(x) -> if(x,false(),true())
     and(x,false()) -> false()
     and(true(),true()) -> true()
     f(0()) -> true()
     f(s(x)) -> h(x)
     h(0()) -> false()
     h(s(x)) -> f(x)
     gt(s(x),0()) -> true()
     gt(0(),y) -> false()
     gt(s(x),s(y)) -> gt(x,y)
    Open
    
    DPs:
     k#(s(x),s(y)) -> k#(minus(x,y),s(y))
    TRS:
     g(s(x),s(y)) ->
     if(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))),
        g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
     n(0(),y) -> 0()
     n(x,0()) -> 0()
     n(s(x),s(y)) -> s(n(x,y))
     m(0(),y) -> y
     m(x,0()) -> x
     m(s(x),s(y)) -> s(m(x,y))
     k(0(),s(y)) -> 0()
     k(s(x),s(y)) -> s(k(minus(x,y),s(y)))
     t(x) -> p(x,x)
     p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))))
     p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x))
     p(0(),y) -> y
     p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y))))
     minus(x,0()) -> x
     minus(s(x),s(y)) -> minus(x,y)
     id(x) -> x
     if(true(),x,y) -> x
     if(false(),x,y) -> y
     not(x) -> if(x,false(),true())
     and(x,false()) -> false()
     and(true(),true()) -> true()
     f(0()) -> true()
     f(s(x)) -> h(x)
     h(0()) -> false()
     h(s(x)) -> f(x)
     gt(s(x),0()) -> true()
     gt(0(),y) -> false()
     gt(s(x),s(y)) -> gt(x,y)
    Open
    
    DPs:
     m#(s(x),s(y)) -> m#(x,y)
    TRS:
     g(s(x),s(y)) ->
     if(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))),
        g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
     n(0(),y) -> 0()
     n(x,0()) -> 0()
     n(s(x),s(y)) -> s(n(x,y))
     m(0(),y) -> y
     m(x,0()) -> x
     m(s(x),s(y)) -> s(m(x,y))
     k(0(),s(y)) -> 0()
     k(s(x),s(y)) -> s(k(minus(x,y),s(y)))
     t(x) -> p(x,x)
     p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))))
     p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x))
     p(0(),y) -> y
     p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y))))
     minus(x,0()) -> x
     minus(s(x),s(y)) -> minus(x,y)
     id(x) -> x
     if(true(),x,y) -> x
     if(false(),x,y) -> y
     not(x) -> if(x,false(),true())
     and(x,false()) -> false()
     and(true(),true()) -> true()
     f(0()) -> true()
     f(s(x)) -> h(x)
     h(0()) -> false()
     h(s(x)) -> f(x)
     gt(s(x),0()) -> true()
     gt(0(),y) -> false()
     gt(s(x),s(y)) -> gt(x,y)
    Open
    
    DPs:
     minus#(s(x),s(y)) -> minus#(x,y)
    TRS:
     g(s(x),s(y)) ->
     if(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))),
        g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
     n(0(),y) -> 0()
     n(x,0()) -> 0()
     n(s(x),s(y)) -> s(n(x,y))
     m(0(),y) -> y
     m(x,0()) -> x
     m(s(x),s(y)) -> s(m(x,y))
     k(0(),s(y)) -> 0()
     k(s(x),s(y)) -> s(k(minus(x,y),s(y)))
     t(x) -> p(x,x)
     p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))))
     p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x))
     p(0(),y) -> y
     p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y))))
     minus(x,0()) -> x
     minus(s(x),s(y)) -> minus(x,y)
     id(x) -> x
     if(true(),x,y) -> x
     if(false(),x,y) -> y
     not(x) -> if(x,false(),true())
     and(x,false()) -> false()
     and(true(),true()) -> true()
     f(0()) -> true()
     f(s(x)) -> h(x)
     h(0()) -> false()
     h(s(x)) -> f(x)
     gt(s(x),0()) -> true()
     gt(0(),y) -> false()
     gt(s(x),s(y)) -> gt(x,y)
    Open
    
    DPs:
     p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y)))
     p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x))
     p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))
    TRS:
     g(s(x),s(y)) ->
     if(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))),
        g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
     n(0(),y) -> 0()
     n(x,0()) -> 0()
     n(s(x),s(y)) -> s(n(x,y))
     m(0(),y) -> y
     m(x,0()) -> x
     m(s(x),s(y)) -> s(m(x,y))
     k(0(),s(y)) -> 0()
     k(s(x),s(y)) -> s(k(minus(x,y),s(y)))
     t(x) -> p(x,x)
     p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))))
     p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x))
     p(0(),y) -> y
     p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y))))
     minus(x,0()) -> x
     minus(s(x),s(y)) -> minus(x,y)
     id(x) -> x
     if(true(),x,y) -> x
     if(false(),x,y) -> y
     not(x) -> if(x,false(),true())
     and(x,false()) -> false()
     and(true(),true()) -> true()
     f(0()) -> true()
     f(s(x)) -> h(x)
     h(0()) -> false()
     h(s(x)) -> f(x)
     gt(s(x),0()) -> true()
     gt(0(),y) -> false()
     gt(s(x),s(y)) -> gt(x,y)
    Open
    
    DPs:
     gt#(s(x),s(y)) -> gt#(x,y)
    TRS:
     g(s(x),s(y)) ->
     if(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))),
        g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
     n(0(),y) -> 0()
     n(x,0()) -> 0()
     n(s(x),s(y)) -> s(n(x,y))
     m(0(),y) -> y
     m(x,0()) -> x
     m(s(x),s(y)) -> s(m(x,y))
     k(0(),s(y)) -> 0()
     k(s(x),s(y)) -> s(k(minus(x,y),s(y)))
     t(x) -> p(x,x)
     p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))))
     p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x))
     p(0(),y) -> y
     p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y))))
     minus(x,0()) -> x
     minus(s(x),s(y)) -> minus(x,y)
     id(x) -> x
     if(true(),x,y) -> x
     if(false(),x,y) -> y
     not(x) -> if(x,false(),true())
     and(x,false()) -> false()
     and(true(),true()) -> true()
     f(0()) -> true()
     f(s(x)) -> h(x)
     h(0()) -> false()
     h(s(x)) -> f(x)
     gt(s(x),0()) -> true()
     gt(0(),y) -> false()
     gt(s(x),s(y)) -> gt(x,y)
    Open
    
    DPs:
     h#(s(x)) -> f#(x)
     f#(s(x)) -> h#(x)
    TRS:
     g(s(x),s(y)) ->
     if(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))),
        g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
     n(0(),y) -> 0()
     n(x,0()) -> 0()
     n(s(x),s(y)) -> s(n(x,y))
     m(0(),y) -> y
     m(x,0()) -> x
     m(s(x),s(y)) -> s(m(x,y))
     k(0(),s(y)) -> 0()
     k(s(x),s(y)) -> s(k(minus(x,y),s(y)))
     t(x) -> p(x,x)
     p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))))
     p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x))
     p(0(),y) -> y
     p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y))))
     minus(x,0()) -> x
     minus(s(x),s(y)) -> minus(x,y)
     id(x) -> x
     if(true(),x,y) -> x
     if(false(),x,y) -> y
     not(x) -> if(x,false(),true())
     and(x,false()) -> false()
     and(true(),true()) -> true()
     f(0()) -> true()
     f(s(x)) -> h(x)
     h(0()) -> false()
     h(s(x)) -> f(x)
     gt(s(x),0()) -> true()
     gt(0(),y) -> false()
     gt(s(x),s(y)) -> gt(x,y)
    Open