/home/nowonder/forschung/aprove/TPDB05/TRS/SK90/4.34.trs

The program

(VAR x y z)
(RULES
a(b(x)) -> b(b(a(a(x))))
)
(COMMENT Example 4.34 in \cite{SK90}) 
(COMMENT This TRS is not terminating!)