MAYBE Time: 0.046880 TRS: { f(x, f(y, z)) -> f(f(x, y), z), f(f(f(a(), b()), c()), x) -> f(b(), f(a(), f(c(), f(b(), x))))} DP: DP: { f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(f(a(), b()), c()), x) -> f#(b(), x), f#(f(f(a(), b()), c()), x) -> f#(b(), f(a(), f(c(), f(b(), x)))), f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x))), f#(f(f(a(), b()), c()), x) -> f#(c(), f(b(), x))} TRS: { f(x, f(y, z)) -> f(f(x, y), z), f(f(f(a(), b()), c()), x) -> f(b(), f(a(), f(c(), f(b(), x))))} UR: { f(x, f(y, z)) -> f(f(x, y), z), f(f(f(a(), b()), c()), x) -> f(b(), f(a(), f(c(), f(b(), x))))} EDG: {(f#(x, f(y, z)) -> f#(x, y), f#(f(f(a(), b()), c()), x) -> f#(c(), f(b(), x))) (f#(x, f(y, z)) -> f#(x, y), f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x)))) (f#(x, f(y, z)) -> f#(x, y), f#(f(f(a(), b()), c()), x) -> f#(b(), f(a(), f(c(), f(b(), x))))) (f#(x, f(y, z)) -> f#(x, y), f#(f(f(a(), b()), c()), x) -> f#(b(), x)) (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#(x, f(y, z)) -> f#(x, y)) (f#(f(f(a(), b()), c()), x) -> f#(b(), f(a(), f(c(), f(b(), x)))), f#(x, f(y, z)) -> f#(f(x, y), z)) (f#(f(f(a(), b()), c()), x) -> f#(b(), f(a(), f(c(), f(b(), x)))), f#(x, f(y, z)) -> f#(x, y)) (f#(f(f(a(), b()), c()), x) -> f#(b(), x), f#(x, f(y, z)) -> f#(f(x, y), z)) (f#(f(f(a(), b()), c()), x) -> f#(b(), x), f#(x, f(y, z)) -> f#(x, y)) (f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x))), f#(x, f(y, z)) -> f#(x, y)) (f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), 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#(x, y)) (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#(f(f(a(), b()), c()), x) -> f#(b(), x)) (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(f(a(), b()), c()), x) -> f#(b(), f(a(), f(c(), f(b(), x))))) (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x)))) (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(f(a(), b()), c()), x) -> f#(c(), f(b(), x))) (f#(f(f(a(), b()), c()), x) -> f#(c(), f(b(), x)), f#(x, f(y, z)) -> f#(x, y)) (f#(f(f(a(), b()), c()), x) -> f#(c(), f(b(), x)), f#(x, f(y, z)) -> f#(f(x, y), z))} STATUS: arrows: 0.444444 SCCS (1): Scc: { f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(f(a(), b()), c()), x) -> f#(b(), x), f#(f(f(a(), b()), c()), x) -> f#(b(), f(a(), f(c(), f(b(), x)))), f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x))), f#(f(f(a(), b()), c()), x) -> f#(c(), f(b(), x))} SCC (6): Strict: { f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(f(a(), b()), c()), x) -> f#(b(), x), f#(f(f(a(), b()), c()), x) -> f#(b(), f(a(), f(c(), f(b(), x)))), f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x))), f#(f(f(a(), b()), c()), x) -> f#(c(), f(b(), x))} Weak: { f(x, f(y, z)) -> f(f(x, y), z), f(f(f(a(), b()), c()), x) -> f(b(), f(a(), f(c(), f(b(), x))))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1) = x0, [b] = 1, [a] = 1, [c] = 0, [f#](x0, x1) = x0 Strict: f#(f(f(a(), b()), c()), x) -> f#(c(), f(b(), x)) 1 + 0x >= 0 + 0x f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x))) 1 + 0x >= 1 + 0x f#(f(f(a(), b()), c()), x) -> f#(b(), f(a(), f(c(), f(b(), x)))) 1 + 0x >= 1 + 0x f#(f(f(a(), b()), c()), x) -> f#(b(), x) 1 + 0x >= 1 + 0x f#(x, f(y, z)) -> f#(f(x, y), z) 0 + 1x + 0y + 0z >= 0 + 1x + 0y + 0z f#(x, f(y, z)) -> f#(x, y) 0 + 1x + 0y + 0z >= 0 + 1x + 0y Weak: f(f(f(a(), b()), c()), x) -> f(b(), f(a(), f(c(), f(b(), x)))) 1 + 0x >= 1 + 0x f(x, f(y, z)) -> f(f(x, y), z) 0 + 1x + 0y + 0z >= 0 + 1x + 0y + 0z SCCS (1): Scc: { f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(f(a(), b()), c()), x) -> f#(b(), x), f#(f(f(a(), b()), c()), x) -> f#(b(), f(a(), f(c(), f(b(), x)))), f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x)))} SCC (5): Strict: { f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(f(a(), b()), c()), x) -> f#(b(), x), f#(f(f(a(), b()), c()), x) -> f#(b(), f(a(), f(c(), f(b(), x)))), f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x)))} Weak: { f(x, f(y, z)) -> f(f(x, y), z), f(f(f(a(), b()), c()), x) -> f(b(), f(a(), f(c(), f(b(), x))))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1) = x0 + x1, [b] = 0, [a] = 0, [c] = 1, [f#](x0, x1) = x0 + x1 Strict: f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x))) 1 + 1x >= 1 + 1x f#(f(f(a(), b()), c()), x) -> f#(b(), f(a(), f(c(), f(b(), x)))) 1 + 1x >= 1 + 1x f#(f(f(a(), b()), c()), x) -> f#(b(), x) 1 + 1x >= 0 + 1x f#(x, f(y, z)) -> f#(f(x, y), z) 0 + 1x + 1y + 1z >= 0 + 1x + 1y + 1z f#(x, f(y, z)) -> f#(x, y) 0 + 1x + 1y + 1z >= 0 + 1x + 1y Weak: f(f(f(a(), b()), c()), x) -> f(b(), f(a(), f(c(), f(b(), x)))) 1 + 1x >= 1 + 1x f(x, f(y, z)) -> f(f(x, y), z) 0 + 1x + 1y + 1z >= 0 + 1x + 1y + 1z SCCS (1): Scc: { f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(f(a(), b()), c()), x) -> f#(b(), f(a(), f(c(), f(b(), x)))), f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x)))} SCC (4): Strict: { f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(f(a(), b()), c()), x) -> f#(b(), f(a(), f(c(), f(b(), x)))), f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x)))} Weak: { f(x, f(y, z)) -> f(f(x, y), z), f(f(f(a(), b()), c()), x) -> f(b(), f(a(), f(c(), f(b(), x))))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1) = x0, [b] = 0, [a] = 1, [c] = 0, [f#](x0, x1) = x0 Strict: f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x))) 1 + 0x >= 1 + 0x f#(f(f(a(), b()), c()), x) -> f#(b(), f(a(), f(c(), f(b(), x)))) 1 + 0x >= 0 + 0x f#(x, f(y, z)) -> f#(f(x, y), z) 0 + 1x + 0y + 0z >= 0 + 1x + 0y + 0z f#(x, f(y, z)) -> f#(x, y) 0 + 1x + 0y + 0z >= 0 + 1x + 0y Weak: f(f(f(a(), b()), c()), x) -> f(b(), f(a(), f(c(), f(b(), x)))) 1 + 0x >= 0 + 0x f(x, f(y, z)) -> f(f(x, y), z) 0 + 1x + 0y + 0z >= 0 + 1x + 0y + 0z SCCS (1): Scc: { f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x)))} SCC (3): Strict: { f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x)))} Weak: { f(x, f(y, z)) -> f(f(x, y), z), f(f(f(a(), b()), c()), x) -> f(b(), f(a(), f(c(), f(b(), x))))} Fail