MAYBE

Problem:
 a(d(x)) -> d(c(b(a(x))))
 b(c(x)) -> c(d(a(b(x))))
 a(c(x)) -> x
 b(d(x)) -> x

Proof:
 DP Processor:
  DPs:
   a#(d(x)) -> a#(x)
   a#(d(x)) -> b#(a(x))
   b#(c(x)) -> b#(x)
   b#(c(x)) -> a#(b(x))
  TRS:
   a(d(x)) -> d(c(b(a(x))))
   b(c(x)) -> c(d(a(b(x))))
   a(c(x)) -> x
   b(d(x)) -> x
  EDG Processor:
   DPs:
    a#(d(x)) -> a#(x)
    a#(d(x)) -> b#(a(x))
    b#(c(x)) -> b#(x)
    b#(c(x)) -> a#(b(x))
   TRS:
    a(d(x)) -> d(c(b(a(x))))
    b(c(x)) -> c(d(a(b(x))))
    a(c(x)) -> x
    b(d(x)) -> x
   graph:
    b#(c(x)) -> b#(x) -> b#(c(x)) -> b#(x)
    b#(c(x)) -> b#(x) -> b#(c(x)) -> a#(b(x))
    a#(d(x)) -> a#(x) -> a#(d(x)) -> a#(x)
    a#(d(x)) -> a#(x) -> a#(d(x)) -> b#(a(x))
   SCC Processor:
    #sccs: 2
    #rules: 2
    #arcs: 4/16
    DPs:
     a#(d(x)) -> a#(x)
    TRS:
     a(d(x)) -> d(c(b(a(x))))
     b(c(x)) -> c(d(a(b(x))))
     a(c(x)) -> x
     b(d(x)) -> x
    Open
    
    DPs:
     b#(c(x)) -> b#(x)
    TRS:
     a(d(x)) -> d(c(b(a(x))))
     b(c(x)) -> c(d(a(b(x))))
     a(c(x)) -> x
     b(d(x)) -> x
    Open