MAYBE Time: 0.021250 TRS: {f(x, f(a(), y)) -> f(a(), f(f(f(a(), a()), y), x))} DP: DP: {f#(x, f(a(), y)) -> f#(f(f(a(), a()), y), x), f#(x, f(a(), y)) -> f#(f(a(), a()), y), f#(x, f(a(), y)) -> f#(a(), f(f(f(a(), a()), y), x)), f#(x, f(a(), y)) -> f#(a(), a())} TRS: {f(x, f(a(), y)) -> f(a(), f(f(f(a(), a()), y), x))} UR: {f(x, f(a(), y)) -> f(a(), f(f(f(a(), a()), y), x))} EDG: {(f#(x, f(a(), y)) -> f#(f(a(), a()), y), f#(x, f(a(), y)) -> f#(a(), a())) (f#(x, f(a(), y)) -> f#(f(a(), a()), y), f#(x, f(a(), y)) -> f#(a(), f(f(f(a(), a()), y), x))) (f#(x, f(a(), y)) -> f#(f(a(), a()), y), f#(x, f(a(), y)) -> f#(f(a(), a()), y)) (f#(x, f(a(), y)) -> f#(f(a(), a()), y), f#(x, f(a(), y)) -> f#(f(f(a(), a()), y), x)) (f#(x, f(a(), y)) -> f#(a(), f(f(f(a(), a()), y), x)), f#(x, f(a(), y)) -> f#(f(f(a(), a()), y), x)) (f#(x, f(a(), y)) -> f#(a(), f(f(f(a(), a()), y), x)), f#(x, f(a(), y)) -> f#(f(a(), a()), y)) (f#(x, f(a(), y)) -> f#(a(), f(f(f(a(), a()), y), x)), f#(x, f(a(), y)) -> f#(a(), f(f(f(a(), a()), y), x))) (f#(x, f(a(), y)) -> f#(a(), f(f(f(a(), a()), y), x)), f#(x, f(a(), y)) -> f#(a(), a())) (f#(x, f(a(), y)) -> f#(f(f(a(), a()), y), x), f#(x, f(a(), y)) -> f#(f(f(a(), a()), y), x)) (f#(x, f(a(), y)) -> f#(f(f(a(), a()), y), x), f#(x, f(a(), y)) -> f#(f(a(), a()), y)) (f#(x, f(a(), y)) -> f#(f(f(a(), a()), y), x), f#(x, f(a(), y)) -> f#(a(), f(f(f(a(), a()), y), x))) (f#(x, f(a(), y)) -> f#(f(f(a(), a()), y), x), f#(x, f(a(), y)) -> f#(a(), a()))} STATUS: arrows: 0.250000 SCCS (1): Scc: {f#(x, f(a(), y)) -> f#(f(f(a(), a()), y), x), f#(x, f(a(), y)) -> f#(f(a(), a()), y), f#(x, f(a(), y)) -> f#(a(), f(f(f(a(), a()), y), x))} SCC (3): Strict: {f#(x, f(a(), y)) -> f#(f(f(a(), a()), y), x), f#(x, f(a(), y)) -> f#(f(a(), a()), y), f#(x, f(a(), y)) -> f#(a(), f(f(f(a(), a()), y), x))} Weak: {f(x, f(a(), y)) -> f(a(), f(f(f(a(), a()), y), x))} Open