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