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