MAYBE

Problem:
 a(a(x1)) -> b(b(b(x1)))
 a(x1) -> c(d(x1))
 b(b(x1)) -> c(c(c(x1)))
 c(c(x1)) -> d(d(d(x1)))
 e(d(x1)) -> a(b(c(d(e(x1)))))
 b(x1) -> d(d(x1))
 e(c(x1)) -> b(a(a(e(x1))))
 c(d(d(x1))) -> a(x1)

Proof:
 DP Processor:
  DPs:
   a#(a(x1)) -> b#(x1)
   a#(a(x1)) -> b#(b(x1))
   a#(a(x1)) -> b#(b(b(x1)))
   a#(x1) -> c#(d(x1))
   b#(b(x1)) -> c#(x1)
   b#(b(x1)) -> c#(c(x1))
   b#(b(x1)) -> c#(c(c(x1)))
   e#(d(x1)) -> e#(x1)
   e#(d(x1)) -> c#(d(e(x1)))
   e#(d(x1)) -> b#(c(d(e(x1))))
   e#(d(x1)) -> a#(b(c(d(e(x1)))))
   e#(c(x1)) -> e#(x1)
   e#(c(x1)) -> a#(e(x1))
   e#(c(x1)) -> a#(a(e(x1)))
   e#(c(x1)) -> b#(a(a(e(x1))))
   c#(d(d(x1))) -> a#(x1)
  TRS:
   a(a(x1)) -> b(b(b(x1)))
   a(x1) -> c(d(x1))
   b(b(x1)) -> c(c(c(x1)))
   c(c(x1)) -> d(d(d(x1)))
   e(d(x1)) -> a(b(c(d(e(x1)))))
   b(x1) -> d(d(x1))
   e(c(x1)) -> b(a(a(e(x1))))
   c(d(d(x1))) -> a(x1)
  TDG Processor:
   DPs:
    a#(a(x1)) -> b#(x1)
    a#(a(x1)) -> b#(b(x1))
    a#(a(x1)) -> b#(b(b(x1)))
    a#(x1) -> c#(d(x1))
    b#(b(x1)) -> c#(x1)
    b#(b(x1)) -> c#(c(x1))
    b#(b(x1)) -> c#(c(c(x1)))
    e#(d(x1)) -> e#(x1)
    e#(d(x1)) -> c#(d(e(x1)))
    e#(d(x1)) -> b#(c(d(e(x1))))
    e#(d(x1)) -> a#(b(c(d(e(x1)))))
    e#(c(x1)) -> e#(x1)
    e#(c(x1)) -> a#(e(x1))
    e#(c(x1)) -> a#(a(e(x1)))
    e#(c(x1)) -> b#(a(a(e(x1))))
    c#(d(d(x1))) -> a#(x1)
   TRS:
    a(a(x1)) -> b(b(b(x1)))
    a(x1) -> c(d(x1))
    b(b(x1)) -> c(c(c(x1)))
    c(c(x1)) -> d(d(d(x1)))
    e(d(x1)) -> a(b(c(d(e(x1)))))
    b(x1) -> d(d(x1))
    e(c(x1)) -> b(a(a(e(x1))))
    c(d(d(x1))) -> a(x1)
   graph:
    e#(c(x1)) -> e#(x1) -> e#(c(x1)) -> b#(a(a(e(x1))))
    e#(c(x1)) -> e#(x1) -> e#(c(x1)) -> a#(a(e(x1)))
    e#(c(x1)) -> e#(x1) -> e#(c(x1)) -> a#(e(x1))
    e#(c(x1)) -> e#(x1) -> e#(c(x1)) -> e#(x1)
    e#(c(x1)) -> e#(x1) -> e#(d(x1)) -> a#(b(c(d(e(x1)))))
    e#(c(x1)) -> e#(x1) -> e#(d(x1)) -> b#(c(d(e(x1))))
    e#(c(x1)) -> e#(x1) -> e#(d(x1)) -> c#(d(e(x1)))
    e#(c(x1)) -> e#(x1) -> e#(d(x1)) -> e#(x1)
    e#(c(x1)) -> b#(a(a(e(x1)))) -> b#(b(x1)) -> c#(c(c(x1)))
    e#(c(x1)) -> b#(a(a(e(x1)))) -> b#(b(x1)) -> c#(c(x1))
    e#(c(x1)) -> b#(a(a(e(x1)))) -> b#(b(x1)) -> c#(x1)
    e#(c(x1)) -> a#(e(x1)) -> a#(x1) -> c#(d(x1))
    e#(c(x1)) -> a#(e(x1)) -> a#(a(x1)) -> b#(b(b(x1)))
    e#(c(x1)) -> a#(e(x1)) -> a#(a(x1)) -> b#(b(x1))
    e#(c(x1)) -> a#(e(x1)) -> a#(a(x1)) -> b#(x1)
    e#(c(x1)) -> a#(a(e(x1))) -> a#(x1) -> c#(d(x1))
    e#(c(x1)) -> a#(a(e(x1))) -> a#(a(x1)) -> b#(b(b(x1)))
    e#(c(x1)) -> a#(a(e(x1))) -> a#(a(x1)) -> b#(b(x1))
    e#(c(x1)) -> a#(a(e(x1))) -> a#(a(x1)) -> b#(x1)
    e#(d(x1)) -> e#(x1) -> e#(c(x1)) -> b#(a(a(e(x1))))
    e#(d(x1)) -> e#(x1) -> e#(c(x1)) -> a#(a(e(x1)))
    e#(d(x1)) -> e#(x1) -> e#(c(x1)) -> a#(e(x1))
    e#(d(x1)) -> e#(x1) -> e#(c(x1)) -> e#(x1)
    e#(d(x1)) -> e#(x1) -> e#(d(x1)) -> a#(b(c(d(e(x1)))))
    e#(d(x1)) -> e#(x1) -> e#(d(x1)) -> b#(c(d(e(x1))))
    e#(d(x1)) -> e#(x1) -> e#(d(x1)) -> c#(d(e(x1)))
    e#(d(x1)) -> e#(x1) -> e#(d(x1)) -> e#(x1)
    e#(d(x1)) -> c#(d(e(x1))) -> c#(d(d(x1))) -> a#(x1)
    e#(d(x1)) -> b#(c(d(e(x1)))) -> b#(b(x1)) -> c#(c(c(x1)))
    e#(d(x1)) -> b#(c(d(e(x1)))) -> b#(b(x1)) -> c#(c(x1))
    e#(d(x1)) -> b#(c(d(e(x1)))) -> b#(b(x1)) -> c#(x1)
    e#(d(x1)) -> a#(b(c(d(e(x1))))) -> a#(x1) -> c#(d(x1))
    e#(d(x1)) -> a#(b(c(d(e(x1))))) -> a#(a(x1)) -> b#(b(b(x1)))
    e#(d(x1)) -> a#(b(c(d(e(x1))))) -> a#(a(x1)) -> b#(b(x1))
    e#(d(x1)) -> a#(b(c(d(e(x1))))) -> a#(a(x1)) -> b#(x1)
    c#(d(d(x1))) -> a#(x1) -> a#(x1) -> c#(d(x1))
    c#(d(d(x1))) -> a#(x1) -> a#(a(x1)) -> b#(b(b(x1)))
    c#(d(d(x1))) -> a#(x1) -> a#(a(x1)) -> b#(b(x1))
    c#(d(d(x1))) -> a#(x1) -> a#(a(x1)) -> b#(x1)
    b#(b(x1)) -> c#(c(c(x1))) -> c#(d(d(x1))) -> a#(x1)
    b#(b(x1)) -> c#(c(x1)) -> c#(d(d(x1))) -> a#(x1)
    b#(b(x1)) -> c#(x1) -> c#(d(d(x1))) -> a#(x1)
    a#(a(x1)) -> b#(b(b(x1))) -> b#(b(x1)) -> c#(c(c(x1)))
    a#(a(x1)) -> b#(b(b(x1))) -> b#(b(x1)) -> c#(c(x1))
    a#(a(x1)) -> b#(b(b(x1))) -> b#(b(x1)) -> c#(x1)
    a#(a(x1)) -> b#(b(x1)) -> b#(b(x1)) -> c#(c(c(x1)))
    a#(a(x1)) -> b#(b(x1)) -> b#(b(x1)) -> c#(c(x1))
    a#(a(x1)) -> b#(b(x1)) -> b#(b(x1)) -> c#(x1)
    a#(a(x1)) -> b#(x1) -> b#(b(x1)) -> c#(c(c(x1)))
    a#(a(x1)) -> b#(x1) -> b#(b(x1)) -> c#(c(x1))
    a#(a(x1)) -> b#(x1) -> b#(b(x1)) -> c#(x1)
    a#(x1) -> c#(d(x1)) -> c#(d(d(x1))) -> a#(x1)
   SCC Processor:
    #sccs: 2
    #rules: 10
    #arcs: 52/256
    DPs:
     e#(c(x1)) -> e#(x1)
     e#(d(x1)) -> e#(x1)
    TRS:
     a(a(x1)) -> b(b(b(x1)))
     a(x1) -> c(d(x1))
     b(b(x1)) -> c(c(c(x1)))
     c(c(x1)) -> d(d(d(x1)))
     e(d(x1)) -> a(b(c(d(e(x1)))))
     b(x1) -> d(d(x1))
     e(c(x1)) -> b(a(a(e(x1))))
     c(d(d(x1))) -> a(x1)
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [e#](x0) = 8x0 + 12,
      
      [e](x0) = 9x0 + 2,
      
      [c](x0) = x0 + 6,
      
      [d](x0) = x0 + 4,
      
      [b](x0) = x0 + 9,
      
      [a](x0) = x0 + 14
     orientation:
      e#(c(x1)) = 8x1 + 60 >= 8x1 + 12 = e#(x1)
      
      e#(d(x1)) = 8x1 + 44 >= 8x1 + 12 = e#(x1)
      
      a(a(x1)) = x1 + 28 >= x1 + 27 = b(b(b(x1)))
      
      a(x1) = x1 + 14 >= x1 + 10 = c(d(x1))
      
      b(b(x1)) = x1 + 18 >= x1 + 18 = c(c(c(x1)))
      
      c(c(x1)) = x1 + 12 >= x1 + 12 = d(d(d(x1)))
      
      e(d(x1)) = 9x1 + 38 >= 9x1 + 35 = a(b(c(d(e(x1)))))
      
      b(x1) = x1 + 9 >= x1 + 8 = d(d(x1))
      
      e(c(x1)) = 9x1 + 56 >= 9x1 + 39 = b(a(a(e(x1))))
      
      c(d(d(x1))) = x1 + 14 >= x1 + 14 = a(x1)
     problem:
      DPs:
       
      TRS:
       a(a(x1)) -> b(b(b(x1)))
       a(x1) -> c(d(x1))
       b(b(x1)) -> c(c(c(x1)))
       c(c(x1)) -> d(d(d(x1)))
       e(d(x1)) -> a(b(c(d(e(x1)))))
       b(x1) -> d(d(x1))
       e(c(x1)) -> b(a(a(e(x1))))
       c(d(d(x1))) -> a(x1)
     Qed
    
    DPs:
     c#(d(d(x1))) -> a#(x1)
     a#(a(x1)) -> b#(x1)
     b#(b(x1)) -> c#(x1)
     b#(b(x1)) -> c#(c(x1))
     b#(b(x1)) -> c#(c(c(x1)))
     a#(a(x1)) -> b#(b(x1))
     a#(a(x1)) -> b#(b(b(x1)))
     a#(x1) -> c#(d(x1))
    TRS:
     a(a(x1)) -> b(b(b(x1)))
     a(x1) -> c(d(x1))
     b(b(x1)) -> c(c(c(x1)))
     c(c(x1)) -> d(d(d(x1)))
     e(d(x1)) -> a(b(c(d(e(x1)))))
     b(x1) -> d(d(x1))
     e(c(x1)) -> b(a(a(e(x1))))
     c(d(d(x1))) -> a(x1)
    Open