MAYBE Time: 0.008387 TRS: { f(x, f(x, y)) -> f(f(f(x, a()), a()), a()), f(y, f(x, f(a(), x))) -> f(f(f(a(), x), f(x, a())), f(a(), y))} DP: DP: { f#(x, f(x, y)) -> f#(x, a()), f#(x, f(x, y)) -> f#(f(x, a()), a()), f#(x, f(x, y)) -> f#(f(f(x, a()), a()), a()), f#(y, f(x, f(a(), x))) -> f#(x, a()), f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y)), f#(y, f(x, f(a(), x))) -> f#(f(a(), x), f(x, a())), f#(y, f(x, f(a(), x))) -> f#(a(), y)} TRS: { f(x, f(x, y)) -> f(f(f(x, a()), a()), a()), f(y, f(x, f(a(), x))) -> f(f(f(a(), x), f(x, a())), f(a(), y))} EDG: {(f#(y, f(x, f(a(), x))) -> f#(a(), y), f#(y, f(x, f(a(), x))) -> f#(a(), y)) (f#(y, f(x, f(a(), x))) -> f#(a(), y), f#(y, f(x, f(a(), x))) -> f#(f(a(), x), f(x, a()))) (f#(y, f(x, f(a(), x))) -> f#(a(), y), f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y))) (f#(y, f(x, f(a(), x))) -> f#(a(), y), f#(y, f(x, f(a(), x))) -> f#(x, a())) (f#(y, f(x, f(a(), x))) -> f#(a(), y), f#(x, f(x, y)) -> f#(f(f(x, a()), a()), a())) (f#(y, f(x, f(a(), x))) -> f#(a(), y), f#(x, f(x, y)) -> f#(f(x, a()), a())) (f#(y, f(x, f(a(), x))) -> f#(a(), y), f#(x, f(x, y)) -> f#(x, a())) (f#(y, f(x, f(a(), x))) -> f#(f(a(), x), f(x, a())), f#(x, f(x, y)) -> f#(x, a())) (f#(y, f(x, f(a(), x))) -> f#(f(a(), x), f(x, a())), f#(x, f(x, y)) -> f#(f(x, a()), a())) (f#(y, f(x, f(a(), x))) -> f#(f(a(), x), f(x, a())), f#(x, f(x, y)) -> f#(f(f(x, a()), a()), a())) (f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y)), f#(x, f(x, y)) -> f#(x, a())) (f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y)), f#(x, f(x, y)) -> f#(f(x, a()), a())) (f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y)), f#(x, f(x, y)) -> f#(f(f(x, a()), a()), a())) (f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y)), f#(y, f(x, f(a(), x))) -> f#(x, a())) (f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y)), f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y))) (f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y)), f#(y, f(x, f(a(), x))) -> f#(f(a(), x), f(x, a()))) (f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y)), f#(y, f(x, f(a(), x))) -> f#(a(), y))} STATUS: arrows: 0.653061 SCCS (1): Scc: {f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y)), f#(y, f(x, f(a(), x))) -> f#(a(), y)} SCC (2): Strict: {f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y)), f#(y, f(x, f(a(), x))) -> f#(a(), y)} Weak: { f(x, f(x, y)) -> f(f(f(x, a()), a()), a()), f(y, f(x, f(a(), x))) -> f(f(f(a(), x), f(x, a())), f(a(), y))} Open