MAYBE Time: 0.002800 TRS: { f(x, f(y, z)) -> f(f(x, y), z), f(f(a(), b()), x) -> f(b(), f(a(), f(c(), f(b(), f(a(), x)))))} DP: DP: { f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), b()), x) -> f#(b(), f(a(), x)), f#(f(a(), b()), x) -> f#(b(), f(a(), f(c(), f(b(), f(a(), x))))), f#(f(a(), b()), x) -> f#(a(), x), f#(f(a(), b()), x) -> f#(a(), f(c(), f(b(), f(a(), x)))), f#(f(a(), b()), x) -> f#(c(), f(b(), f(a(), x)))} TRS: { f(x, f(y, z)) -> f(f(x, y), z), f(f(a(), b()), x) -> f(b(), f(a(), f(c(), f(b(), f(a(), x)))))} UR: { f(x, f(y, z)) -> f(f(x, y), z), f(f(a(), b()), x) -> f(b(), f(a(), f(c(), f(b(), f(a(), x)))))} EDG: {(f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), b()), x) -> f#(c(), f(b(), f(a(), x)))) (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), b()), x) -> f#(a(), f(c(), f(b(), f(a(), x))))) (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), b()), x) -> f#(a(), x)) (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), b()), x) -> f#(b(), f(a(), f(c(), f(b(), f(a(), x)))))) (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), b()), x) -> f#(b(), f(a(), x))) (f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(f(x, y), z)) (f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(x, y)) (f#(f(a(), b()), x) -> f#(b(), f(a(), f(c(), f(b(), f(a(), x))))), f#(f(a(), b()), x) -> f#(c(), f(b(), f(a(), x)))) (f#(f(a(), b()), x) -> f#(b(), f(a(), f(c(), f(b(), f(a(), x))))), f#(f(a(), b()), x) -> f#(a(), f(c(), f(b(), f(a(), x))))) (f#(f(a(), b()), x) -> f#(b(), f(a(), f(c(), f(b(), f(a(), x))))), f#(f(a(), b()), x) -> f#(a(), x)) (f#(f(a(), b()), x) -> f#(b(), f(a(), f(c(), f(b(), f(a(), x))))), f#(f(a(), b()), x) -> f#(b(), f(a(), f(c(), f(b(), f(a(), x)))))) (f#(f(a(), b()), x) -> f#(b(), f(a(), f(c(), f(b(), f(a(), x))))), f#(f(a(), b()), x) -> f#(b(), f(a(), x))) (f#(f(a(), b()), x) -> f#(b(), f(a(), f(c(), f(b(), f(a(), x))))), f#(x, f(y, z)) -> f#(f(x, y), z)) (f#(f(a(), b()), x) -> f#(b(), f(a(), f(c(), f(b(), f(a(), x))))), f#(x, f(y, z)) -> f#(x, y)) (f#(f(a(), b()), x) -> f#(a(), f(c(), f(b(), f(a(), x)))), f#(f(a(), b()), x) -> f#(c(), f(b(), f(a(), x)))) (f#(f(a(), b()), x) -> f#(a(), f(c(), f(b(), f(a(), x)))), f#(f(a(), b()), x) -> f#(a(), f(c(), f(b(), f(a(), x))))) (f#(f(a(), b()), x) -> f#(a(), f(c(), f(b(), f(a(), x)))), f#(f(a(), b()), x) -> f#(a(), x)) (f#(f(a(), b()), x) -> f#(a(), f(c(), f(b(), f(a(), x)))), f#(f(a(), b()), x) -> f#(b(), f(a(), f(c(), f(b(), f(a(), x)))))) (f#(f(a(), b()), x) -> f#(a(), f(c(), f(b(), f(a(), x)))), f#(f(a(), b()), x) -> f#(b(), f(a(), x))) (f#(f(a(), b()), x) -> f#(a(), f(c(), f(b(), f(a(), x)))), f#(x, f(y, z)) -> f#(f(x, y), z)) (f#(f(a(), b()), x) -> f#(a(), f(c(), f(b(), f(a(), x)))), f#(x, f(y, z)) -> f#(x, y)) (f#(f(a(), b()), x) -> f#(c(), f(b(), f(a(), x))), f#(x, f(y, z)) -> f#(x, y)) (f#(f(a(), b()), x) -> f#(c(), f(b(), f(a(), x))), f#(x, f(y, z)) -> f#(f(x, y), z)) (f#(f(a(), b()), x) -> f#(c(), f(b(), f(a(), x))), f#(f(a(), b()), x) -> f#(b(), f(a(), x))) (f#(f(a(), b()), x) -> f#(c(), f(b(), f(a(), x))), f#(f(a(), b()), x) -> f#(b(), f(a(), f(c(), f(b(), f(a(), x)))))) (f#(f(a(), b()), x) -> f#(c(), f(b(), f(a(), x))), f#(f(a(), b()), x) -> f#(a(), x)) (f#(f(a(), b()), x) -> f#(c(), f(b(), f(a(), x))), f#(f(a(), b()), x) -> f#(a(), f(c(), f(b(), f(a(), x))))) (f#(f(a(), b()), x) -> f#(c(), f(b(), f(a(), x))), f#(f(a(), b()), x) -> f#(c(), f(b(), f(a(), x)))) (f#(f(a(), b()), x) -> f#(a(), x), f#(x, f(y, z)) -> f#(x, y)) (f#(f(a(), b()), x) -> f#(a(), x), f#(x, f(y, z)) -> f#(f(x, y), z)) (f#(f(a(), b()), x) -> f#(a(), x), f#(f(a(), b()), x) -> f#(b(), f(a(), x))) (f#(f(a(), b()), x) -> f#(a(), x), f#(f(a(), b()), x) -> f#(b(), f(a(), f(c(), f(b(), f(a(), x)))))) (f#(f(a(), b()), x) -> f#(a(), x), f#(f(a(), b()), x) -> f#(a(), x)) (f#(f(a(), b()), x) -> f#(a(), x), f#(f(a(), b()), x) -> f#(a(), f(c(), f(b(), f(a(), x))))) (f#(f(a(), b()), x) -> f#(a(), x), f#(f(a(), b()), x) -> f#(c(), f(b(), f(a(), x)))) (f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(x, y)) (f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z)) (f#(x, f(y, z)) -> f#(x, y), f#(f(a(), b()), x) -> f#(b(), f(a(), x))) (f#(x, f(y, z)) -> f#(x, y), f#(f(a(), b()), x) -> f#(b(), f(a(), f(c(), f(b(), f(a(), x)))))) (f#(x, f(y, z)) -> f#(x, y), f#(f(a(), b()), x) -> f#(a(), x)) (f#(x, f(y, z)) -> f#(x, y), f#(f(a(), b()), x) -> f#(a(), f(c(), f(b(), f(a(), x))))) (f#(x, f(y, z)) -> f#(x, y), f#(f(a(), b()), x) -> f#(c(), f(b(), f(a(), x)))) (f#(f(a(), b()), x) -> f#(b(), f(a(), x)), f#(x, f(y, z)) -> f#(x, y)) (f#(f(a(), b()), x) -> f#(b(), f(a(), x)), f#(x, f(y, z)) -> f#(f(x, y), z)) (f#(f(a(), b()), x) -> f#(b(), f(a(), x)), f#(f(a(), b()), x) -> f#(b(), f(a(), x))) (f#(f(a(), b()), x) -> f#(b(), f(a(), x)), f#(f(a(), b()), x) -> f#(b(), f(a(), f(c(), f(b(), f(a(), x)))))) (f#(f(a(), b()), x) -> f#(b(), f(a(), x)), f#(f(a(), b()), x) -> f#(a(), x)) (f#(f(a(), b()), x) -> f#(b(), f(a(), x)), f#(f(a(), b()), x) -> f#(a(), f(c(), f(b(), f(a(), x))))) (f#(f(a(), b()), x) -> f#(b(), f(a(), x)), f#(f(a(), b()), x) -> f#(c(), f(b(), f(a(), x))))} STATUS: arrows: 0.000000 SCCS (1): Scc: { f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), b()), x) -> f#(b(), f(a(), x)), f#(f(a(), b()), x) -> f#(b(), f(a(), f(c(), f(b(), f(a(), x))))), f#(f(a(), b()), x) -> f#(a(), x), f#(f(a(), b()), x) -> f#(a(), f(c(), f(b(), f(a(), x)))), f#(f(a(), b()), x) -> f#(c(), f(b(), f(a(), x)))} SCC (7): Strict: { f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), b()), x) -> f#(b(), f(a(), x)), f#(f(a(), b()), x) -> f#(b(), f(a(), f(c(), f(b(), f(a(), x))))), f#(f(a(), b()), x) -> f#(a(), x), f#(f(a(), b()), x) -> f#(a(), f(c(), f(b(), f(a(), x)))), f#(f(a(), b()), x) -> f#(c(), f(b(), f(a(), x)))} Weak: { f(x, f(y, z)) -> f(f(x, y), z), f(f(a(), b()), x) -> f(b(), f(a(), f(c(), f(b(), f(a(), x)))))} Open