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