/home/nowonder/forschung/aprove/TPDB05/TRS/Zantema/z26.trs

The program

(VAR x y)
(RULES
a(a(f(x,y))) -> f(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
f(a(x),a(y)) -> a(f(x,y))
f(b(x),b(y)) -> b(f(x,y))
)