MAYBE

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

Proof:
 DP Processor:
  DPs:
   h#(z,e(x)) -> d#(z,x)
   h#(z,e(x)) -> h#(c(z),d(z,x))
   d#(z,g(x,y)) -> d#(z,y)
   d#(z,g(x,y)) -> g#(e(x),d(z,y))
   d#(c(z),g(g(x,y),0())) -> d#(z,g(x,y))
   d#(c(z),g(g(x,y),0())) -> d#(c(z),g(x,y))
   d#(c(z),g(g(x,y),0())) -> g#(d(c(z),g(x,y)),d(z,g(x,y)))
   g#(e(x),e(y)) -> g#(x,y)
  TRS:
   h(z,e(x)) -> h(c(z),d(z,x))
   d(z,g(0(),0())) -> e(0())
   d(z,g(x,y)) -> g(e(x),d(z,y))
   d(c(z),g(g(x,y),0())) -> g(d(c(z),g(x,y)),d(z,g(x,y)))
   g(e(x),e(y)) -> e(g(x,y))
  TDG Processor:
   DPs:
    h#(z,e(x)) -> d#(z,x)
    h#(z,e(x)) -> h#(c(z),d(z,x))
    d#(z,g(x,y)) -> d#(z,y)
    d#(z,g(x,y)) -> g#(e(x),d(z,y))
    d#(c(z),g(g(x,y),0())) -> d#(z,g(x,y))
    d#(c(z),g(g(x,y),0())) -> d#(c(z),g(x,y))
    d#(c(z),g(g(x,y),0())) -> g#(d(c(z),g(x,y)),d(z,g(x,y)))
    g#(e(x),e(y)) -> g#(x,y)
   TRS:
    h(z,e(x)) -> h(c(z),d(z,x))
    d(z,g(0(),0())) -> e(0())
    d(z,g(x,y)) -> g(e(x),d(z,y))
    d(c(z),g(g(x,y),0())) -> g(d(c(z),g(x,y)),d(z,g(x,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#(c(z),g(g(x,y),0())) -> g#(d(c(z),g(x,y)),d(z,g(x,y))) ->
    g#(e(x),e(y)) -> g#(x,y)
    d#(c(z),g(g(x,y),0())) -> d#(c(z),g(x,y)) ->
    d#(c(z),g(g(x,y),0())) -> g#(d(c(z),g(x,y)),d(z,g(x,y)))
    d#(c(z),g(g(x,y),0())) -> d#(c(z),g(x,y)) ->
    d#(c(z),g(g(x,y),0())) -> d#(c(z),g(x,y))
    d#(c(z),g(g(x,y),0())) -> d#(c(z),g(x,y)) ->
    d#(c(z),g(g(x,y),0())) -> d#(z,g(x,y))
    d#(c(z),g(g(x,y),0())) -> d#(c(z),g(x,y)) ->
    d#(z,g(x,y)) -> g#(e(x),d(z,y))
    d#(c(z),g(g(x,y),0())) -> d#(c(z),g(x,y)) ->
    d#(z,g(x,y)) -> d#(z,y)
    d#(c(z),g(g(x,y),0())) -> d#(z,g(x,y)) ->
    d#(c(z),g(g(x,y),0())) -> g#(d(c(z),g(x,y)),d(z,g(x,y)))
    d#(c(z),g(g(x,y),0())) -> d#(z,g(x,y)) ->
    d#(c(z),g(g(x,y),0())) -> d#(c(z),g(x,y))
    d#(c(z),g(g(x,y),0())) -> d#(z,g(x,y)) ->
    d#(c(z),g(g(x,y),0())) -> d#(z,g(x,y))
    d#(c(z),g(g(x,y),0())) -> d#(z,g(x,y)) ->
    d#(z,g(x,y)) -> g#(e(x),d(z,y))
    d#(c(z),g(g(x,y),0())) -> d#(z,g(x,y)) ->
    d#(z,g(x,y)) -> d#(z,y)
    d#(z,g(x,y)) -> g#(e(x),d(z,y)) -> g#(e(x),e(y)) -> g#(x,y)
    d#(z,g(x,y)) -> d#(z,y) ->
    d#(c(z),g(g(x,y),0())) -> g#(d(c(z),g(x,y)),d(z,g(x,y)))
    d#(z,g(x,y)) -> d#(z,y) -> d#(c(z),g(g(x,y),0())) -> d#(c(z),g(x,y))
    d#(z,g(x,y)) -> d#(z,y) -> d#(c(z),g(g(x,y),0())) -> d#(z,g(x,y))
    d#(z,g(x,y)) -> d#(z,y) -> d#(z,g(x,y)) -> g#(e(x),d(z,y))
    d#(z,g(x,y)) -> d#(z,y) -> d#(z,g(x,y)) -> d#(z,y)
    h#(z,e(x)) -> d#(z,x) ->
    d#(c(z),g(g(x,y),0())) -> g#(d(c(z),g(x,y)),d(z,g(x,y)))
    h#(z,e(x)) -> d#(z,x) -> d#(c(z),g(g(x,y),0())) -> d#(c(z),g(x,y))
    h#(z,e(x)) -> d#(z,x) -> d#(c(z),g(g(x,y),0())) -> d#(z,g(x,y))
    h#(z,e(x)) -> d#(z,x) -> d#(z,g(x,y)) -> g#(e(x),d(z,y))
    h#(z,e(x)) -> d#(z,x) -> d#(z,g(x,y)) -> d#(z,y)
    h#(z,e(x)) -> h#(c(z),d(z,x)) -> h#(z,e(x)) -> h#(c(z),d(z,x))
    h#(z,e(x)) -> h#(c(z),d(z,x)) -> h#(z,e(x)) -> d#(z,x)
   SCC Processor:
    #sccs: 3
    #rules: 5
    #arcs: 25/64
    DPs:
     h#(z,e(x)) -> h#(c(z),d(z,x))
    TRS:
     h(z,e(x)) -> h(c(z),d(z,x))
     d(z,g(0(),0())) -> e(0())
     d(z,g(x,y)) -> g(e(x),d(z,y))
     d(c(z),g(g(x,y),0())) -> g(d(c(z),g(x,y)),d(z,g(x,y)))
     g(e(x),e(y)) -> e(g(x,y))
    Open
    
    DPs:
     d#(c(z),g(g(x,y),0())) -> d#(c(z),g(x,y))
     d#(z,g(x,y)) -> d#(z,y)
     d#(c(z),g(g(x,y),0())) -> d#(z,g(x,y))
    TRS:
     h(z,e(x)) -> h(c(z),d(z,x))
     d(z,g(0(),0())) -> e(0())
     d(z,g(x,y)) -> g(e(x),d(z,y))
     d(c(z),g(g(x,y),0())) -> g(d(c(z),g(x,y)),d(z,g(x,y)))
     g(e(x),e(y)) -> e(g(x,y))
    Subterm Criterion Processor:
     simple projection:
      pi(d#) = 1
     problem:
      DPs:
       
      TRS:
       h(z,e(x)) -> h(c(z),d(z,x))
       d(z,g(0(),0())) -> e(0())
       d(z,g(x,y)) -> g(e(x),d(z,y))
       d(c(z),g(g(x,y),0())) -> g(d(c(z),g(x,y)),d(z,g(x,y)))
       g(e(x),e(y)) -> e(g(x,y))
     Qed
    
    DPs:
     g#(e(x),e(y)) -> g#(x,y)
    TRS:
     h(z,e(x)) -> h(c(z),d(z,x))
     d(z,g(0(),0())) -> e(0())
     d(z,g(x,y)) -> g(e(x),d(z,y))
     d(c(z),g(g(x,y),0())) -> g(d(c(z),g(x,y)),d(z,g(x,y)))
     g(e(x),e(y)) -> e(g(x,y))
    Subterm Criterion Processor:
     simple projection:
      pi(g#) = 1
     problem:
      DPs:
       
      TRS:
       h(z,e(x)) -> h(c(z),d(z,x))
       d(z,g(0(),0())) -> e(0())
       d(z,g(x,y)) -> g(e(x),d(z,y))
       d(c(z),g(g(x,y),0())) -> g(d(c(z),g(x,y)),d(z,g(x,y)))
       g(e(x),e(y)) -> e(g(x,y))
     Qed