YES Time: 0.010670 TRS: {f(a(), f(a(), x)) -> f(a(), f(f(a(), x), f(a(), a())))} DP: DP: {f#(a(), f(a(), x)) -> f#(f(a(), x), f(a(), a())), f#(a(), f(a(), x)) -> f#(a(), f(f(a(), x), f(a(), a()))), f#(a(), f(a(), x)) -> f#(a(), a())} TRS: {f(a(), f(a(), x)) -> f(a(), f(f(a(), x), f(a(), a())))} UR: {f(a(), f(a(), x)) -> f(a(), f(f(a(), x), f(a(), a())))} EDG: {} STATUS: arrows: 1.000000 SCCS (0):