MAYBE

Problem:
 a(b(x)) -> b(a(a(x)))
 b(c(x)) -> c(b(b(x)))
 c(a(x)) -> a(c(c(x)))
 u(a(x)) -> x
 v(b(x)) -> x
 w(c(x)) -> x
 a(u(x)) -> x
 b(v(x)) -> x
 c(w(x)) -> x

Proof:
 DP Processor:
  DPs:
   a#(b(x)) -> a#(x)
   a#(b(x)) -> a#(a(x))
   a#(b(x)) -> b#(a(a(x)))
   b#(c(x)) -> b#(x)
   b#(c(x)) -> b#(b(x))
   b#(c(x)) -> c#(b(b(x)))
   c#(a(x)) -> c#(x)
   c#(a(x)) -> c#(c(x))
   c#(a(x)) -> a#(c(c(x)))
  TRS:
   a(b(x)) -> b(a(a(x)))
   b(c(x)) -> c(b(b(x)))
   c(a(x)) -> a(c(c(x)))
   u(a(x)) -> x
   v(b(x)) -> x
   w(c(x)) -> x
   a(u(x)) -> x
   b(v(x)) -> x
   c(w(x)) -> x
  Usable Rule Processor:
   DPs:
    a#(b(x)) -> a#(x)
    a#(b(x)) -> a#(a(x))
    a#(b(x)) -> b#(a(a(x)))
    b#(c(x)) -> b#(x)
    b#(c(x)) -> b#(b(x))
    b#(c(x)) -> c#(b(b(x)))
    c#(a(x)) -> c#(x)
    c#(a(x)) -> c#(c(x))
    c#(a(x)) -> a#(c(c(x)))
   TRS:
    a(b(x)) -> b(a(a(x)))
    a(u(x)) -> x
    b(c(x)) -> c(b(b(x)))
    b(v(x)) -> x
    c(a(x)) -> a(c(c(x)))
    c(w(x)) -> x
   ADG Processor:
    DPs:
     a#(b(x)) -> a#(x)
     a#(b(x)) -> a#(a(x))
     a#(b(x)) -> b#(a(a(x)))
     b#(c(x)) -> b#(x)
     b#(c(x)) -> b#(b(x))
     b#(c(x)) -> c#(b(b(x)))
     c#(a(x)) -> c#(x)
     c#(a(x)) -> c#(c(x))
     c#(a(x)) -> a#(c(c(x)))
    TRS:
     a(b(x)) -> b(a(a(x)))
     a(u(x)) -> x
     b(c(x)) -> c(b(b(x)))
     b(v(x)) -> x
     c(a(x)) -> a(c(c(x)))
     c(w(x)) -> x
    graph:
     c#(a(x)) -> c#(c(x)) -> c#(a(x)) -> c#(x)
     c#(a(x)) -> c#(c(x)) -> c#(a(x)) -> c#(c(x))
     c#(a(x)) -> c#(c(x)) -> c#(a(x)) -> a#(c(c(x)))
     c#(a(x)) -> c#(x) -> c#(a(x)) -> c#(x)
     c#(a(x)) -> c#(x) -> c#(a(x)) -> c#(c(x))
     c#(a(x)) -> c#(x) -> c#(a(x)) -> a#(c(c(x)))
     c#(a(x)) -> a#(c(c(x))) -> a#(b(x)) -> a#(x)
     c#(a(x)) -> a#(c(c(x))) -> a#(b(x)) -> a#(a(x))
     c#(a(x)) -> a#(c(c(x))) -> a#(b(x)) -> b#(a(a(x)))
     b#(c(x)) -> c#(b(b(x))) -> c#(a(x)) -> c#(x)
     b#(c(x)) -> c#(b(b(x))) -> c#(a(x)) -> c#(c(x))
     b#(c(x)) -> c#(b(b(x))) -> c#(a(x)) -> a#(c(c(x)))
     b#(c(x)) -> b#(b(x)) -> b#(c(x)) -> b#(x)
     b#(c(x)) -> b#(b(x)) -> b#(c(x)) -> b#(b(x))
     b#(c(x)) -> b#(b(x)) -> b#(c(x)) -> c#(b(b(x)))
     b#(c(x)) -> b#(x) -> b#(c(x)) -> b#(x)
     b#(c(x)) -> b#(x) -> b#(c(x)) -> b#(b(x))
     b#(c(x)) -> b#(x) -> b#(c(x)) -> c#(b(b(x)))
     a#(b(x)) -> b#(a(a(x))) -> b#(c(x)) -> b#(x)
     a#(b(x)) -> b#(a(a(x))) -> b#(c(x)) -> b#(b(x))
     a#(b(x)) -> b#(a(a(x))) -> b#(c(x)) -> c#(b(b(x)))
     a#(b(x)) -> a#(a(x)) -> a#(b(x)) -> a#(x)
     a#(b(x)) -> a#(a(x)) -> a#(b(x)) -> a#(a(x))
     a#(b(x)) -> a#(a(x)) -> a#(b(x)) -> b#(a(a(x)))
     a#(b(x)) -> a#(x) -> a#(b(x)) -> a#(x)
     a#(b(x)) -> a#(x) -> a#(b(x)) -> a#(a(x))
     a#(b(x)) -> a#(x) -> a#(b(x)) -> b#(a(a(x)))
    Restore Modifier:
     DPs:
      a#(b(x)) -> a#(x)
      a#(b(x)) -> a#(a(x))
      a#(b(x)) -> b#(a(a(x)))
      b#(c(x)) -> b#(x)
      b#(c(x)) -> b#(b(x))
      b#(c(x)) -> c#(b(b(x)))
      c#(a(x)) -> c#(x)
      c#(a(x)) -> c#(c(x))
      c#(a(x)) -> a#(c(c(x)))
     TRS:
      a(b(x)) -> b(a(a(x)))
      b(c(x)) -> c(b(b(x)))
      c(a(x)) -> a(c(c(x)))
      u(a(x)) -> x
      v(b(x)) -> x
      w(c(x)) -> x
      a(u(x)) -> x
      b(v(x)) -> x
      c(w(x)) -> x
     SCC Processor:
      #sccs: 1
      #rules: 9
      #arcs: 27/81
      DPs:
       c#(a(x)) -> c#(c(x))
       c#(a(x)) -> a#(c(c(x)))
       a#(b(x)) -> b#(a(a(x)))
       b#(c(x)) -> c#(b(b(x)))
       c#(a(x)) -> c#(x)
       b#(c(x)) -> b#(b(x))
       b#(c(x)) -> b#(x)
       a#(b(x)) -> a#(a(x))
       a#(b(x)) -> a#(x)
      TRS:
       a(b(x)) -> b(a(a(x)))
       b(c(x)) -> c(b(b(x)))
       c(a(x)) -> a(c(c(x)))
       u(a(x)) -> x
       v(b(x)) -> x
       w(c(x)) -> x
       a(u(x)) -> x
       b(v(x)) -> x
       c(w(x)) -> x
      Open