MAYBE

Problem:
 h(e(x),y) -> h(d(x,y),s(y))
 d(g(g(0(),x),y),s(z)) -> g(e(x),d(g(g(0(),x),y),z))
 d(g(g(0(),x),y),0()) -> e(y)
 d(g(0(),x),y) -> e(x)
 d(g(x,y),z) -> g(d(x,z),e(y))
 g(e(x),e(y)) -> e(g(x,y))

Proof:
 DP Processor:
  DPs:
   h#(e(x),y) -> d#(x,y)
   h#(e(x),y) -> h#(d(x,y),s(y))
   d#(g(g(0(),x),y),s(z)) -> d#(g(g(0(),x),y),z)
   d#(g(g(0(),x),y),s(z)) -> g#(e(x),d(g(g(0(),x),y),z))
   d#(g(x,y),z) -> d#(x,z)
   d#(g(x,y),z) -> g#(d(x,z),e(y))
   g#(e(x),e(y)) -> g#(x,y)
  TRS:
   h(e(x),y) -> h(d(x,y),s(y))
   d(g(g(0(),x),y),s(z)) -> g(e(x),d(g(g(0(),x),y),z))
   d(g(g(0(),x),y),0()) -> e(y)
   d(g(0(),x),y) -> e(x)
   d(g(x,y),z) -> g(d(x,z),e(y))
   g(e(x),e(y)) -> e(g(x,y))
  Usable Rule Processor:
   DPs:
    h#(e(x),y) -> d#(x,y)
    h#(e(x),y) -> h#(d(x,y),s(y))
    d#(g(g(0(),x),y),s(z)) -> d#(g(g(0(),x),y),z)
    d#(g(g(0(),x),y),s(z)) -> g#(e(x),d(g(g(0(),x),y),z))
    d#(g(x,y),z) -> d#(x,z)
    d#(g(x,y),z) -> g#(d(x,z),e(y))
    g#(e(x),e(y)) -> g#(x,y)
   TRS:
    f9(x,y) -> x
    f9(x,y) -> y
    d(g(g(0(),x),y),s(z)) -> g(e(x),d(g(g(0(),x),y),z))
    d(g(g(0(),x),y),0()) -> e(y)
    d(g(0(),x),y) -> e(x)
    d(g(x,y),z) -> g(d(x,z),e(y))
    g(e(x),e(y)) -> e(g(x,y))
   TDG Processor:
    DPs:
     h#(e(x),y) -> d#(x,y)
     h#(e(x),y) -> h#(d(x,y),s(y))
     d#(g(g(0(),x),y),s(z)) -> d#(g(g(0(),x),y),z)
     d#(g(g(0(),x),y),s(z)) -> g#(e(x),d(g(g(0(),x),y),z))
     d#(g(x,y),z) -> d#(x,z)
     d#(g(x,y),z) -> g#(d(x,z),e(y))
     g#(e(x),e(y)) -> g#(x,y)
    TRS:
     f9(x,y) -> x
     f9(x,y) -> y
     d(g(g(0(),x),y),s(z)) -> g(e(x),d(g(g(0(),x),y),z))
     d(g(g(0(),x),y),0()) -> e(y)
     d(g(0(),x),y) -> e(x)
     d(g(x,y),z) -> g(d(x,z),e(y))
     g(e(x),e(y)) -> e(g(x,y))
    graph:
     g#(e(x),e(y)) -> g#(x,y) ->
     g#(e(x),e(y)) -> g#(x,y)
     d#(g(g(0(),x),y),s(z)) -> g#(e(x),d(g(g(0(),x),y),z)) ->
     g#(e(x),e(y)) -> g#(x,y)
     d#(g(g(0(),x),y),s(z)) -> d#(g(g(0(),x),y),z) ->
     d#(g(x,y),z) -> g#(d(x,z),e(y))
     d#(g(g(0(),x),y),s(z)) -> d#(g(g(0(),x),y),z) ->
     d#(g(x,y),z) -> d#(x,z)
     d#(g(g(0(),x),y),s(z)) -> d#(g(g(0(),x),y),z) ->
     d#(g(g(0(),x),y),s(z)) -> g#(e(x),d(g(g(0(),x),y),z))
     d#(g(g(0(),x),y),s(z)) -> d#(g(g(0(),x),y),z) ->
     d#(g(g(0(),x),y),s(z)) -> d#(g(g(0(),x),y),z)
     d#(g(x,y),z) -> g#(d(x,z),e(y)) -> g#(e(x),e(y)) -> g#(x,y)
     d#(g(x,y),z) -> d#(x,z) -> d#(g(x,y),z) -> g#(d(x,z),e(y))
     d#(g(x,y),z) -> d#(x,z) -> d#(g(x,y),z) -> d#(x,z)
     d#(g(x,y),z) -> d#(x,z) ->
     d#(g(g(0(),x),y),s(z)) -> g#(e(x),d(g(g(0(),x),y),z))
     d#(g(x,y),z) -> d#(x,z) -> d#(g(g(0(),x),y),s(z)) -> d#(g(g(0(),x),y),z)
     h#(e(x),y) -> d#(x,y) -> d#(g(x,y),z) -> g#(d(x,z),e(y))
     h#(e(x),y) -> d#(x,y) -> d#(g(x,y),z) -> d#(x,z)
     h#(e(x),y) -> d#(x,y) ->
     d#(g(g(0(),x),y),s(z)) -> g#(e(x),d(g(g(0(),x),y),z))
     h#(e(x),y) -> d#(x,y) ->
     d#(g(g(0(),x),y),s(z)) -> d#(g(g(0(),x),y),z)
     h#(e(x),y) -> h#(d(x,y),s(y)) -> h#(e(x),y) -> h#(d(x,y),s(y))
     h#(e(x),y) -> h#(d(x,y),s(y)) -> h#(e(x),y) -> d#(x,y)
    Restore Modifier:
     DPs:
      h#(e(x),y) -> d#(x,y)
      h#(e(x),y) -> h#(d(x,y),s(y))
      d#(g(g(0(),x),y),s(z)) -> d#(g(g(0(),x),y),z)
      d#(g(g(0(),x),y),s(z)) -> g#(e(x),d(g(g(0(),x),y),z))
      d#(g(x,y),z) -> d#(x,z)
      d#(g(x,y),z) -> g#(d(x,z),e(y))
      g#(e(x),e(y)) -> g#(x,y)
     TRS:
      h(e(x),y) -> h(d(x,y),s(y))
      d(g(g(0(),x),y),s(z)) -> g(e(x),d(g(g(0(),x),y),z))
      d(g(g(0(),x),y),0()) -> e(y)
      d(g(0(),x),y) -> e(x)
      d(g(x,y),z) -> g(d(x,z),e(y))
      g(e(x),e(y)) -> e(g(x,y))
     SCC Processor:
      #sccs: 3
      #rules: 4
      #arcs: 17/49
      DPs:
       h#(e(x),y) -> h#(d(x,y),s(y))
      TRS:
       h(e(x),y) -> h(d(x,y),s(y))
       d(g(g(0(),x),y),s(z)) -> g(e(x),d(g(g(0(),x),y),z))
       d(g(g(0(),x),y),0()) -> e(y)
       d(g(0(),x),y) -> e(x)
       d(g(x,y),z) -> g(d(x,z),e(y))
       g(e(x),e(y)) -> e(g(x,y))
      Open
      
      DPs:
       d#(g(g(0(),x),y),s(z)) -> d#(g(g(0(),x),y),z)
       d#(g(x,y),z) -> d#(x,z)
      TRS:
       h(e(x),y) -> h(d(x,y),s(y))
       d(g(g(0(),x),y),s(z)) -> g(e(x),d(g(g(0(),x),y),z))
       d(g(g(0(),x),y),0()) -> e(y)
       d(g(0(),x),y) -> e(x)
       d(g(x,y),z) -> g(d(x,z),e(y))
       g(e(x),e(y)) -> e(g(x,y))
      Open
      
      DPs:
       g#(e(x),e(y)) -> g#(x,y)
      TRS:
       h(e(x),y) -> h(d(x,y),s(y))
       d(g(g(0(),x),y),s(z)) -> g(e(x),d(g(g(0(),x),y),z))
       d(g(g(0(),x),y),0()) -> e(y)
       d(g(0(),x),y) -> e(x)
       d(g(x,y),z) -> g(d(x,z),e(y))
       g(e(x),e(y)) -> e(g(x,y))
      Open