MAYBE

Problem:
 f(a()) -> f(c(a()))
 f(c(X)) -> X
 f(c(a())) -> f(d(b()))
 f(a()) -> f(d(a()))
 f(d(X)) -> X
 f(c(b())) -> f(d(a()))
 e(g(X)) -> e(X)

Proof:
 DP Processor:
  DPs:
   f#(a()) -> f#(c(a()))
   f#(c(a())) -> f#(d(b()))
   f#(a()) -> f#(d(a()))
   f#(c(b())) -> f#(d(a()))
   e#(g(X)) -> e#(X)
  TRS:
   f(a()) -> f(c(a()))
   f(c(X)) -> X
   f(c(a())) -> f(d(b()))
   f(a()) -> f(d(a()))
   f(d(X)) -> X
   f(c(b())) -> f(d(a()))
   e(g(X)) -> e(X)
  Usable Rule Processor:
   DPs:
    f#(a()) -> f#(c(a()))
    f#(c(a())) -> f#(d(b()))
    f#(a()) -> f#(d(a()))
    f#(c(b())) -> f#(d(a()))
    e#(g(X)) -> e#(X)
   TRS:
    
   TDG Processor:
    DPs:
     f#(a()) -> f#(c(a()))
     f#(c(a())) -> f#(d(b()))
     f#(a()) -> f#(d(a()))
     f#(c(b())) -> f#(d(a()))
     e#(g(X)) -> e#(X)
    TRS:
     
    graph:
     e#(g(X)) -> e#(X) -> e#(g(X)) -> e#(X)
     f#(c(b())) -> f#(d(a())) -> f#(c(b())) -> f#(d(a()))
     f#(c(b())) -> f#(d(a())) -> f#(a()) -> f#(d(a()))
     f#(c(b())) -> f#(d(a())) -> f#(c(a())) -> f#(d(b()))
     f#(c(b())) -> f#(d(a())) -> f#(a()) -> f#(c(a()))
     f#(c(a())) -> f#(d(b())) -> f#(c(b())) -> f#(d(a()))
     f#(c(a())) -> f#(d(b())) -> f#(a()) -> f#(d(a()))
     f#(c(a())) -> f#(d(b())) -> f#(c(a())) -> f#(d(b()))
     f#(c(a())) -> f#(d(b())) -> f#(a()) -> f#(c(a()))
     f#(a()) -> f#(d(a())) -> f#(c(b())) -> f#(d(a()))
     f#(a()) -> f#(d(a())) -> f#(a()) -> f#(d(a()))
     f#(a()) -> f#(d(a())) -> f#(c(a())) -> f#(d(b()))
     f#(a()) -> f#(d(a())) -> f#(a()) -> f#(c(a()))
     f#(a()) -> f#(c(a())) -> f#(c(b())) -> f#(d(a()))
     f#(a()) -> f#(c(a())) -> f#(a()) -> f#(d(a()))
     f#(a()) -> f#(c(a())) -> f#(c(a())) -> f#(d(b()))
     f#(a()) -> f#(c(a())) -> f#(a()) -> f#(c(a()))
    Restore Modifier:
     DPs:
      f#(a()) -> f#(c(a()))
      f#(c(a())) -> f#(d(b()))
      f#(a()) -> f#(d(a()))
      f#(c(b())) -> f#(d(a()))
      e#(g(X)) -> e#(X)
     TRS:
      f(a()) -> f(c(a()))
      f(c(X)) -> X
      f(c(a())) -> f(d(b()))
      f(a()) -> f(d(a()))
      f(d(X)) -> X
      f(c(b())) -> f(d(a()))
      e(g(X)) -> e(X)
     SCC Processor:
      #sccs: 2
      #rules: 5
      #arcs: 17/25
      DPs:
       f#(c(b())) -> f#(d(a()))
       f#(a()) -> f#(c(a()))
       f#(c(a())) -> f#(d(b()))
       f#(a()) -> f#(d(a()))
      TRS:
       f(a()) -> f(c(a()))
       f(c(X)) -> X
       f(c(a())) -> f(d(b()))
       f(a()) -> f(d(a()))
       f(d(X)) -> X
       f(c(b())) -> f(d(a()))
       e(g(X)) -> e(X)
      Open
      
      DPs:
       e#(g(X)) -> e#(X)
      TRS:
       f(a()) -> f(c(a()))
       f(c(X)) -> X
       f(c(a())) -> f(d(b()))
       f(a()) -> f(d(a()))
       f(d(X)) -> X
       f(c(b())) -> f(d(a()))
       e(g(X)) -> e(X)
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [e#](x0) = x0 + 1,
        
        [e](x0) = 0,
        
        [g](x0) = x0 + 1,
        
        [d](x0) = x0,
        
        [b] = 0,
        
        [c](x0) = x0,
        
        [f](x0) = x0,
        
        [a] = 0
       orientation:
        e#(g(X)) = X + 2 >= X + 1 = e#(X)
        
        f(a()) = 0 >= 0 = f(c(a()))
        
        f(c(X)) = X >= X = X
        
        f(c(a())) = 0 >= 0 = f(d(b()))
        
        f(a()) = 0 >= 0 = f(d(a()))
        
        f(d(X)) = X >= X = X
        
        f(c(b())) = 0 >= 0 = f(d(a()))
        
        e(g(X)) = 0 >= 0 = e(X)
       problem:
        DPs:
         
        TRS:
         f(a()) -> f(c(a()))
         f(c(X)) -> X
         f(c(a())) -> f(d(b()))
         f(a()) -> f(d(a()))
         f(d(X)) -> X
         f(c(b())) -> f(d(a()))
         e(g(X)) -> e(X)
       Qed