MAYBE

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

Proof:
 DP Processor:
  DPs:
   a#(b(c(a(x1)))) -> b#(x1)
   a#(b(c(a(x1)))) -> a#(b(x1))
   a#(b(c(a(x1)))) -> b#(a(b(x1)))
   a#(b(c(a(x1)))) -> c#(b(a(b(x1))))
   a#(b(c(a(x1)))) -> a#(c(b(a(b(x1)))))
   a#(b(c(a(x1)))) -> b#(a(c(b(a(b(x1))))))
   a#(d(x1)) -> c#(x1)
   a#(f(f(x1))) -> g#(x1)
   b#(g(x1)) -> b#(x1)
   b#(g(x1)) -> g#(b(x1))
   c#(a(c(x1))) -> b#(c(x1))
   c#(a(c(x1))) -> a#(b(c(x1)))
   c#(a(c(x1))) -> c#(a(b(c(x1))))
   c#(a(c(x1))) -> b#(c(a(b(c(x1)))))
   c#(d(x1)) -> a#(x1)
   c#(d(x1)) -> a#(a(x1))
   g#(x1) -> a#(x1)
   g#(x1) -> c#(a(x1))
  TRS:
   a(b(c(a(x1)))) -> b(a(c(b(a(b(x1))))))
   a(d(x1)) -> c(x1)
   a(f(f(x1))) -> g(x1)
   b(g(x1)) -> g(b(x1))
   c(x1) -> f(f(x1))
   c(a(c(x1))) -> b(c(a(b(c(x1)))))
   c(d(x1)) -> a(a(x1))
   g(x1) -> c(a(x1))
   g(x1) -> d(d(d(d(x1))))
  TDG Processor:
   DPs:
    a#(b(c(a(x1)))) -> b#(x1)
    a#(b(c(a(x1)))) -> a#(b(x1))
    a#(b(c(a(x1)))) -> b#(a(b(x1)))
    a#(b(c(a(x1)))) -> c#(b(a(b(x1))))
    a#(b(c(a(x1)))) -> a#(c(b(a(b(x1)))))
    a#(b(c(a(x1)))) -> b#(a(c(b(a(b(x1))))))
    a#(d(x1)) -> c#(x1)
    a#(f(f(x1))) -> g#(x1)
    b#(g(x1)) -> b#(x1)
    b#(g(x1)) -> g#(b(x1))
    c#(a(c(x1))) -> b#(c(x1))
    c#(a(c(x1))) -> a#(b(c(x1)))
    c#(a(c(x1))) -> c#(a(b(c(x1))))
    c#(a(c(x1))) -> b#(c(a(b(c(x1)))))
    c#(d(x1)) -> a#(x1)
    c#(d(x1)) -> a#(a(x1))
    g#(x1) -> a#(x1)
    g#(x1) -> c#(a(x1))
   TRS:
    a(b(c(a(x1)))) -> b(a(c(b(a(b(x1))))))
    a(d(x1)) -> c(x1)
    a(f(f(x1))) -> g(x1)
    b(g(x1)) -> g(b(x1))
    c(x1) -> f(f(x1))
    c(a(c(x1))) -> b(c(a(b(c(x1)))))
    c(d(x1)) -> a(a(x1))
    g(x1) -> c(a(x1))
    g(x1) -> d(d(d(d(x1))))
   graph:
    g#(x1) -> c#(a(x1)) -> c#(d(x1)) -> a#(a(x1))
    g#(x1) -> c#(a(x1)) -> c#(d(x1)) -> a#(x1)
    g#(x1) -> c#(a(x1)) -> c#(a(c(x1))) -> b#(c(a(b(c(x1)))))
    g#(x1) -> c#(a(x1)) -> c#(a(c(x1))) -> c#(a(b(c(x1))))
    g#(x1) -> c#(a(x1)) -> c#(a(c(x1))) -> a#(b(c(x1)))
    g#(x1) -> c#(a(x1)) -> c#(a(c(x1))) -> b#(c(x1))
    g#(x1) -> a#(x1) -> a#(f(f(x1))) -> g#(x1)
    g#(x1) -> a#(x1) -> a#(d(x1)) -> c#(x1)
    g#(x1) -> a#(x1) -> a#(b(c(a(x1)))) -> b#(a(c(b(a(b(x1))))))
    g#(x1) -> a#(x1) -> a#(b(c(a(x1)))) -> a#(c(b(a(b(x1)))))
    g#(x1) -> a#(x1) -> a#(b(c(a(x1)))) -> c#(b(a(b(x1))))
    g#(x1) -> a#(x1) -> a#(b(c(a(x1)))) -> b#(a(b(x1)))
    g#(x1) -> a#(x1) -> a#(b(c(a(x1)))) -> a#(b(x1))
    g#(x1) -> a#(x1) -> a#(b(c(a(x1)))) -> b#(x1)
    c#(d(x1)) -> a#(a(x1)) -> a#(f(f(x1))) -> g#(x1)
    c#(d(x1)) -> a#(a(x1)) -> a#(d(x1)) -> c#(x1)
    c#(d(x1)) -> a#(a(x1)) -> a#(b(c(a(x1)))) -> b#(a(c(b(a(b(x1))))))
    c#(d(x1)) -> a#(a(x1)) -> a#(b(c(a(x1)))) -> a#(c(b(a(b(x1)))))
    c#(d(x1)) -> a#(a(x1)) -> a#(b(c(a(x1)))) -> c#(b(a(b(x1))))
    c#(d(x1)) -> a#(a(x1)) -> a#(b(c(a(x1)))) -> b#(a(b(x1)))
    c#(d(x1)) -> a#(a(x1)) -> a#(b(c(a(x1)))) -> a#(b(x1))
    c#(d(x1)) -> a#(a(x1)) -> a#(b(c(a(x1)))) -> b#(x1)
    c#(d(x1)) -> a#(x1) -> a#(f(f(x1))) -> g#(x1)
    c#(d(x1)) -> a#(x1) -> a#(d(x1)) -> c#(x1)
    c#(d(x1)) -> a#(x1) -> a#(b(c(a(x1)))) -> b#(a(c(b(a(b(x1))))))
    c#(d(x1)) -> a#(x1) -> a#(b(c(a(x1)))) -> a#(c(b(a(b(x1)))))
    c#(d(x1)) -> a#(x1) -> a#(b(c(a(x1)))) -> c#(b(a(b(x1))))
    c#(d(x1)) -> a#(x1) -> a#(b(c(a(x1)))) -> b#(a(b(x1)))
    c#(d(x1)) -> a#(x1) -> a#(b(c(a(x1)))) -> a#(b(x1))
    c#(d(x1)) -> a#(x1) -> a#(b(c(a(x1)))) -> b#(x1)
    c#(a(c(x1))) -> c#(a(b(c(x1)))) -> c#(d(x1)) -> a#(a(x1))
    c#(a(c(x1))) -> c#(a(b(c(x1)))) -> c#(d(x1)) -> a#(x1)
    c#(a(c(x1))) -> c#(a(b(c(x1)))) ->
    c#(a(c(x1))) -> b#(c(a(b(c(x1)))))
    c#(a(c(x1))) -> c#(a(b(c(x1)))) ->
    c#(a(c(x1))) -> c#(a(b(c(x1))))
    c#(a(c(x1))) -> c#(a(b(c(x1)))) -> c#(a(c(x1))) -> a#(b(c(x1)))
    c#(a(c(x1))) -> c#(a(b(c(x1)))) -> c#(a(c(x1))) -> b#(c(x1))
    c#(a(c(x1))) -> b#(c(a(b(c(x1))))) -> b#(g(x1)) -> g#(b(x1))
    c#(a(c(x1))) -> b#(c(a(b(c(x1))))) -> b#(g(x1)) -> b#(x1)
    c#(a(c(x1))) -> b#(c(x1)) -> b#(g(x1)) -> g#(b(x1))
    c#(a(c(x1))) -> b#(c(x1)) -> b#(g(x1)) -> b#(x1)
    c#(a(c(x1))) -> a#(b(c(x1))) -> a#(f(f(x1))) -> g#(x1)
    c#(a(c(x1))) -> a#(b(c(x1))) -> a#(d(x1)) -> c#(x1)
    c#(a(c(x1))) -> a#(b(c(x1))) ->
    a#(b(c(a(x1)))) -> b#(a(c(b(a(b(x1))))))
    c#(a(c(x1))) -> a#(b(c(x1))) ->
    a#(b(c(a(x1)))) -> a#(c(b(a(b(x1)))))
    c#(a(c(x1))) -> a#(b(c(x1))) -> a#(b(c(a(x1)))) -> c#(b(a(b(x1))))
    c#(a(c(x1))) -> a#(b(c(x1))) -> a#(b(c(a(x1)))) -> b#(a(b(x1)))
    c#(a(c(x1))) -> a#(b(c(x1))) -> a#(b(c(a(x1)))) -> a#(b(x1))
    c#(a(c(x1))) -> a#(b(c(x1))) -> a#(b(c(a(x1)))) -> b#(x1)
    b#(g(x1)) -> g#(b(x1)) -> g#(x1) -> c#(a(x1))
    b#(g(x1)) -> g#(b(x1)) -> g#(x1) -> a#(x1)
    b#(g(x1)) -> b#(x1) -> b#(g(x1)) -> g#(b(x1))
    b#(g(x1)) -> b#(x1) -> b#(g(x1)) -> b#(x1)
    a#(f(f(x1))) -> g#(x1) -> g#(x1) -> c#(a(x1))
    a#(f(f(x1))) -> g#(x1) -> g#(x1) -> a#(x1)
    a#(d(x1)) -> c#(x1) -> c#(d(x1)) -> a#(a(x1))
    a#(d(x1)) -> c#(x1) -> c#(d(x1)) -> a#(x1)
    a#(d(x1)) -> c#(x1) -> c#(a(c(x1))) -> b#(c(a(b(c(x1)))))
    a#(d(x1)) -> c#(x1) -> c#(a(c(x1))) -> c#(a(b(c(x1))))
    a#(d(x1)) -> c#(x1) -> c#(a(c(x1))) -> a#(b(c(x1)))
    a#(d(x1)) -> c#(x1) -> c#(a(c(x1))) -> b#(c(x1))
    a#(b(c(a(x1)))) -> c#(b(a(b(x1)))) -> c#(d(x1)) -> a#(a(x1))
    a#(b(c(a(x1)))) -> c#(b(a(b(x1)))) -> c#(d(x1)) -> a#(x1)
    a#(b(c(a(x1)))) -> c#(b(a(b(x1)))) ->
    c#(a(c(x1))) -> b#(c(a(b(c(x1)))))
    a#(b(c(a(x1)))) -> c#(b(a(b(x1)))) ->
    c#(a(c(x1))) -> c#(a(b(c(x1))))
    a#(b(c(a(x1)))) -> c#(b(a(b(x1)))) ->
    c#(a(c(x1))) -> a#(b(c(x1)))
    a#(b(c(a(x1)))) -> c#(b(a(b(x1)))) -> c#(a(c(x1))) -> b#(c(x1))
    a#(b(c(a(x1)))) -> b#(a(b(x1))) -> b#(g(x1)) -> g#(b(x1))
    a#(b(c(a(x1)))) -> b#(a(b(x1))) -> b#(g(x1)) -> b#(x1)
    a#(b(c(a(x1)))) -> b#(a(c(b(a(b(x1)))))) ->
    b#(g(x1)) -> g#(b(x1))
    a#(b(c(a(x1)))) -> b#(a(c(b(a(b(x1)))))) -> b#(g(x1)) -> b#(x1)
    a#(b(c(a(x1)))) -> b#(x1) -> b#(g(x1)) -> g#(b(x1))
    a#(b(c(a(x1)))) -> b#(x1) -> b#(g(x1)) -> b#(x1)
    a#(b(c(a(x1)))) -> a#(b(x1)) -> a#(f(f(x1))) -> g#(x1)
    a#(b(c(a(x1)))) -> a#(b(x1)) -> a#(d(x1)) -> c#(x1)
    a#(b(c(a(x1)))) -> a#(b(x1)) ->
    a#(b(c(a(x1)))) -> b#(a(c(b(a(b(x1))))))
    a#(b(c(a(x1)))) -> a#(b(x1)) ->
    a#(b(c(a(x1)))) -> a#(c(b(a(b(x1)))))
    a#(b(c(a(x1)))) -> a#(b(x1)) -> a#(b(c(a(x1)))) -> c#(b(a(b(x1))))
    a#(b(c(a(x1)))) -> a#(b(x1)) -> a#(b(c(a(x1)))) -> b#(a(b(x1)))
    a#(b(c(a(x1)))) -> a#(b(x1)) -> a#(b(c(a(x1)))) -> a#(b(x1))
    a#(b(c(a(x1)))) -> a#(b(x1)) -> a#(b(c(a(x1)))) -> b#(x1)
    a#(b(c(a(x1)))) -> a#(c(b(a(b(x1))))) ->
    a#(f(f(x1))) -> g#(x1)
    a#(b(c(a(x1)))) -> a#(c(b(a(b(x1))))) ->
    a#(d(x1)) -> c#(x1)
    a#(b(c(a(x1)))) -> a#(c(b(a(b(x1))))) ->
    a#(b(c(a(x1)))) -> b#(a(c(b(a(b(x1))))))
    a#(b(c(a(x1)))) -> a#(c(b(a(b(x1))))) ->
    a#(b(c(a(x1)))) -> a#(c(b(a(b(x1)))))
    a#(b(c(a(x1)))) -> a#(c(b(a(b(x1))))) ->
    a#(b(c(a(x1)))) -> c#(b(a(b(x1))))
    a#(b(c(a(x1)))) -> a#(c(b(a(b(x1))))) ->
    a#(b(c(a(x1)))) -> b#(a(b(x1)))
    a#(b(c(a(x1)))) -> a#(c(b(a(b(x1))))) ->
    a#(b(c(a(x1)))) -> a#(b(x1))
    a#(b(c(a(x1)))) -> a#(c(b(a(b(x1))))) -> a#(b(c(a(x1)))) -> b#(x1)
   Open