/home/nowonder/forschung/aprove/TPDB05/TRS/nontermin/AG01/#4.31.trs

The program

(from AG01 4.31)
(VAR x)
(RULES
a(d(x)) -> d(c(b(a(x))))
b(c(x)) -> c(d(a(b(x))))
a(c(x)) -> x
b(d(x)) -> x
)