MAYBE Time: 0.519946 TRS: { f(x, f(x, y)) -> f(f(f(x, a()), a()), a()), f(y, f(x, f(a(), x))) -> f(f(a(), 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(a(), f(x, a())), f(a(), y)), f#(y, f(x, f(a(), x))) -> f#(a(), y), f#(y, f(x, f(a(), x))) -> f#(a(), f(x, a()))} TRS: { f(x, f(x, y)) -> f(f(f(x, a()), a()), a()), f(y, f(x, f(a(), x))) -> f(f(a(), f(x, a())), f(a(), y))} EDG: {(f#(x, f(x, y)) -> f#(f(x, a()), a()), f#(y, f(x, f(a(), x))) -> f#(a(), f(x, a()))) (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#(f(x, a()), a()), f#(y, f(x, f(a(), x))) -> f#(f(a(), f(x, a())), f(a(), y))) (f#(x, f(x, y)) -> f#(f(x, a()), a()), f#(y, f(x, f(a(), x))) -> 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#(x, f(x, y)) -> f#(f(x, a()), a()), f#(x, f(x, y)) -> f#(f(x, a()), a())) (f#(x, f(x, y)) -> f#(f(x, a()), a()), f#(x, f(x, y)) -> f#(x, a())) (f#(y, f(x, f(a(), x))) -> f#(x, a()), f#(y, f(x, f(a(), x))) -> f#(a(), f(x, a()))) (f#(y, f(x, f(a(), x))) -> f#(x, a()), 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#(f(a(), f(x, a())), f(a(), y))) (f#(y, f(x, f(a(), x))) -> f#(x, a()), f#(y, f(x, f(a(), x))) -> f#(x, a())) (f#(y, f(x, 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#(x, a()), f#(x, f(x, y)) -> f#(f(x, a()), a())) (f#(y, f(x, f(a(), x))) -> f#(x, a()), f#(x, f(x, y)) -> f#(x, a())) (f#(y, f(x, f(a(), x))) -> f#(a(), y), f#(y, f(x, f(a(), x))) -> f#(a(), f(x, a()))) (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(), 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#(a(), f(x, a())), f#(x, f(x, y)) -> f#(x, a())) (f#(y, f(x, f(a(), x))) -> f#(a(), f(x, a())), f#(x, f(x, y)) -> f#(f(x, a()), a())) (f#(y, f(x, f(a(), x))) -> f#(a(), f(x, a())), f#(x, f(x, y)) -> f#(f(f(x, a()), a()), a())) (f#(y, f(x, f(a(), x))) -> f#(a(), f(x, a())), f#(y, f(x, f(a(), x))) -> f#(x, a())) (f#(y, f(x, f(a(), x))) -> f#(a(), f(x, a())), f#(y, f(x, f(a(), x))) -> f#(f(a(), f(x, a())), f(a(), y))) (f#(y, f(x, f(a(), x))) -> f#(a(), f(x, a())), f#(y, f(x, f(a(), x))) -> f#(a(), y)) (f#(y, f(x, f(a(), x))) -> f#(a(), f(x, a())), f#(y, f(x, f(a(), x))) -> f#(a(), f(x, a()))) (f#(y, f(x, f(a(), x))) -> f#(f(a(), f(x, a())), f(a(), y)), f#(x, f(x, y)) -> f#(x, a())) (f#(y, f(x, f(a(), x))) -> f#(f(a(), 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(a(), 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(a(), 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(a(), f(x, a())), f(a(), y)), f#(y, f(x, f(a(), x))) -> f#(f(a(), f(x, a())), f(a(), y))) (f#(y, f(x, f(a(), x))) -> f#(f(a(), f(x, a())), f(a(), y)), f#(y, f(x, f(a(), x))) -> f#(a(), y)) (f#(y, f(x, f(a(), x))) -> f#(f(a(), f(x, a())), f(a(), y)), f#(y, f(x, f(a(), x))) -> f#(a(), f(x, a()))) (f#(x, f(x, y)) -> f#(f(f(x, a()), a()), a()), f#(x, f(x, y)) -> f#(x, a())) (f#(x, f(x, y)) -> f#(f(f(x, a()), a()), a()), f#(x, f(x, y)) -> f#(f(x, a()), a())) (f#(x, f(x, y)) -> f#(f(f(x, a()), a()), a()), f#(x, f(x, y)) -> f#(f(f(x, a()), 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#(x, f(x, y)) -> f#(f(f(x, a()), a()), a()), f#(y, f(x, f(a(), x))) -> f#(f(a(), 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#(a(), y)) (f#(x, f(x, y)) -> f#(f(f(x, a()), a()), a()), f#(y, f(x, f(a(), x))) -> f#(a(), f(x, a()))) (f#(x, f(x, y)) -> f#(x, a()), f#(x, f(x, y)) -> f#(x, a())) (f#(x, f(x, y)) -> f#(x, a()), f#(x, f(x, y)) -> f#(f(x, a()), a())) (f#(x, f(x, y)) -> f#(x, a()), f#(x, f(x, y)) -> f#(f(f(x, a()), a()), a())) (f#(x, f(x, y)) -> f#(x, a()), f#(y, f(x, f(a(), x))) -> f#(x, a())) (f#(x, f(x, y)) -> f#(x, a()), f#(y, f(x, f(a(), x))) -> f#(f(a(), f(x, a())), f(a(), y))) (f#(x, f(x, y)) -> f#(x, 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#(a(), f(x, a())))} EDG: {(f#(y, f(x, f(a(), x))) -> f#(a(), y), f#(y, f(x, f(a(), x))) -> f#(a(), f(x, a()))) (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(), 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#(a(), f(x, a())), f#(x, f(x, y)) -> f#(x, a())) (f#(y, f(x, f(a(), x))) -> f#(a(), f(x, a())), f#(x, f(x, y)) -> f#(f(x, a()), a())) (f#(y, f(x, f(a(), x))) -> f#(a(), f(x, a())), f#(x, f(x, y)) -> f#(f(f(x, a()), a()), a())) (f#(y, f(x, f(a(), x))) -> f#(f(a(), f(x, a())), f(a(), y)), f#(x, f(x, y)) -> f#(x, a())) (f#(y, f(x, f(a(), x))) -> f#(f(a(), 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(a(), 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(a(), 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(a(), f(x, a())), f(a(), y)), f#(y, f(x, f(a(), x))) -> f#(f(a(), f(x, a())), f(a(), y))) (f#(y, f(x, f(a(), x))) -> f#(f(a(), f(x, a())), f(a(), y)), f#(y, f(x, f(a(), x))) -> f#(a(), y)) (f#(y, f(x, f(a(), x))) -> f#(f(a(), f(x, a())), f(a(), y)), f#(y, f(x, f(a(), x))) -> f#(a(), f(x, a())))} EDG: {(f#(y, f(x, f(a(), x))) -> f#(a(), y), f#(y, f(x, f(a(), x))) -> f#(a(), f(x, a()))) (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(), 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(), f(x, a())), f(a(), y)), f#(x, f(x, y)) -> f#(x, a())) (f#(y, f(x, f(a(), x))) -> f#(f(a(), 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(a(), 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(a(), 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(a(), f(x, a())), f(a(), y)), f#(y, f(x, f(a(), x))) -> f#(f(a(), f(x, a())), f(a(), y))) (f#(y, f(x, f(a(), x))) -> f#(f(a(), f(x, a())), f(a(), y)), f#(y, f(x, f(a(), x))) -> f#(a(), y)) (f#(y, f(x, f(a(), x))) -> f#(f(a(), f(x, a())), f(a(), y)), f#(y, f(x, f(a(), x))) -> f#(a(), f(x, a())))} STATUS: arrows: 0.714286 SCCS (1): Scc: {f#(y, f(x, f(a(), x))) -> f#(f(a(), 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(a(), 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(a(), f(x, a())), f(a(), y))} Open