MAYBE Time: 0.026333 TRS: {f(c(), f(c(), x)) -> f(b(), f(a(), x)), f(b(), f(b(), x)) -> f(a(), f(c(), x)), f(a(), f(a(), x)) -> f(c(), f(b(), x))} DP: DP: {f#(c(), f(c(), x)) -> f#(b(), f(a(), x)), f#(c(), f(c(), x)) -> f#(a(), x), f#(b(), f(b(), x)) -> f#(c(), x), f#(b(), f(b(), x)) -> f#(a(), f(c(), x)), f#(a(), f(a(), x)) -> f#(c(), f(b(), x)), f#(a(), f(a(), x)) -> f#(b(), x)} TRS: {f(c(), f(c(), x)) -> f(b(), f(a(), x)), f(b(), f(b(), x)) -> f(a(), f(c(), x)), f(a(), f(a(), x)) -> f(c(), f(b(), x))} EDG: {(f#(b(), f(b(), x)) -> f#(a(), f(c(), x)), f#(a(), f(a(), x)) -> f#(b(), x)) (f#(b(), f(b(), x)) -> f#(a(), f(c(), x)), f#(a(), f(a(), x)) -> f#(c(), f(b(), x))) (f#(b(), f(b(), x)) -> f#(a(), f(c(), x)), f#(b(), f(b(), x)) -> f#(a(), f(c(), x))) (f#(b(), f(b(), x)) -> f#(a(), f(c(), x)), f#(b(), f(b(), x)) -> f#(c(), x)) (f#(b(), f(b(), x)) -> f#(a(), f(c(), x)), f#(c(), f(c(), x)) -> f#(a(), x)) (f#(b(), f(b(), x)) -> f#(a(), f(c(), x)), f#(c(), f(c(), x)) -> f#(b(), f(a(), x))) (f#(c(), f(c(), x)) -> f#(a(), x), f#(a(), f(a(), x)) -> f#(b(), x)) (f#(c(), f(c(), x)) -> f#(a(), x), f#(a(), f(a(), x)) -> f#(c(), f(b(), x))) (f#(c(), f(c(), x)) -> f#(a(), x), f#(b(), f(b(), x)) -> f#(a(), f(c(), x))) (f#(c(), f(c(), x)) -> f#(a(), x), f#(b(), f(b(), x)) -> f#(c(), x)) (f#(c(), f(c(), x)) -> f#(a(), x), f#(c(), f(c(), x)) -> f#(a(), x)) (f#(c(), f(c(), x)) -> f#(a(), x), f#(c(), f(c(), x)) -> f#(b(), f(a(), x))) (f#(a(), f(a(), x)) -> f#(b(), x), f#(a(), f(a(), x)) -> f#(b(), x)) (f#(a(), f(a(), x)) -> f#(b(), x), f#(a(), f(a(), x)) -> f#(c(), f(b(), x))) (f#(a(), f(a(), x)) -> f#(b(), x), f#(b(), f(b(), x)) -> f#(a(), f(c(), x))) (f#(a(), f(a(), x)) -> f#(b(), x), f#(b(), f(b(), x)) -> f#(c(), x)) (f#(a(), f(a(), x)) -> f#(b(), x), f#(c(), f(c(), x)) -> f#(a(), x)) (f#(a(), f(a(), x)) -> f#(b(), x), f#(c(), f(c(), x)) -> f#(b(), f(a(), x))) (f#(b(), f(b(), x)) -> f#(c(), x), f#(c(), f(c(), x)) -> f#(b(), f(a(), x))) (f#(b(), f(b(), x)) -> f#(c(), x), f#(c(), f(c(), x)) -> f#(a(), x)) (f#(b(), f(b(), x)) -> f#(c(), x), f#(b(), f(b(), x)) -> f#(c(), x)) (f#(b(), f(b(), x)) -> f#(c(), x), f#(b(), f(b(), x)) -> f#(a(), f(c(), x))) (f#(b(), f(b(), x)) -> f#(c(), x), f#(a(), f(a(), x)) -> f#(c(), f(b(), x))) (f#(b(), f(b(), x)) -> f#(c(), x), f#(a(), f(a(), x)) -> f#(b(), x)) (f#(a(), f(a(), x)) -> f#(c(), f(b(), x)), f#(c(), f(c(), x)) -> f#(b(), f(a(), x))) (f#(a(), f(a(), x)) -> f#(c(), f(b(), x)), f#(c(), f(c(), x)) -> f#(a(), x)) (f#(a(), f(a(), x)) -> f#(c(), f(b(), x)), f#(b(), f(b(), x)) -> f#(c(), x)) (f#(a(), f(a(), x)) -> f#(c(), f(b(), x)), f#(b(), f(b(), x)) -> f#(a(), f(c(), x))) (f#(a(), f(a(), x)) -> f#(c(), f(b(), x)), f#(a(), f(a(), x)) -> f#(c(), f(b(), x))) (f#(a(), f(a(), x)) -> f#(c(), f(b(), x)), f#(a(), f(a(), x)) -> f#(b(), x)) (f#(c(), f(c(), x)) -> f#(b(), f(a(), x)), f#(c(), f(c(), x)) -> f#(b(), f(a(), x))) (f#(c(), f(c(), x)) -> f#(b(), f(a(), x)), f#(c(), f(c(), x)) -> f#(a(), x)) (f#(c(), f(c(), x)) -> f#(b(), f(a(), x)), f#(b(), f(b(), x)) -> f#(c(), x)) (f#(c(), f(c(), x)) -> f#(b(), f(a(), x)), f#(b(), f(b(), x)) -> f#(a(), f(c(), x))) (f#(c(), f(c(), x)) -> f#(b(), f(a(), x)), f#(a(), f(a(), x)) -> f#(c(), f(b(), x))) (f#(c(), f(c(), x)) -> f#(b(), f(a(), x)), f#(a(), f(a(), x)) -> f#(b(), x))} EDG: {(f#(b(), f(b(), x)) -> f#(a(), f(c(), x)), f#(a(), f(a(), x)) -> f#(b(), x)) (f#(b(), f(b(), x)) -> f#(a(), f(c(), x)), f#(a(), f(a(), x)) -> f#(c(), f(b(), x))) (f#(c(), f(c(), x)) -> f#(a(), x), f#(a(), f(a(), x)) -> f#(b(), x)) (f#(c(), f(c(), x)) -> f#(a(), x), f#(a(), f(a(), x)) -> f#(c(), f(b(), x))) (f#(a(), f(a(), x)) -> f#(b(), x), f#(b(), f(b(), x)) -> f#(a(), f(c(), x))) (f#(a(), f(a(), x)) -> f#(b(), x), f#(b(), f(b(), x)) -> f#(c(), x)) (f#(b(), f(b(), x)) -> f#(c(), x), f#(c(), f(c(), x)) -> f#(b(), f(a(), x))) (f#(b(), f(b(), x)) -> f#(c(), x), f#(c(), f(c(), x)) -> f#(a(), x)) (f#(a(), f(a(), x)) -> f#(c(), f(b(), x)), f#(c(), f(c(), x)) -> f#(b(), f(a(), x))) (f#(a(), f(a(), x)) -> f#(c(), f(b(), x)), f#(c(), f(c(), x)) -> f#(a(), x)) (f#(c(), f(c(), x)) -> f#(b(), f(a(), x)), f#(b(), f(b(), x)) -> f#(c(), x)) (f#(c(), f(c(), x)) -> f#(b(), f(a(), x)), f#(b(), f(b(), x)) -> f#(a(), f(c(), x)))} EDG: {(f#(b(), f(b(), x)) -> f#(a(), f(c(), x)), f#(a(), f(a(), x)) -> f#(b(), x)) (f#(b(), f(b(), x)) -> f#(a(), f(c(), x)), f#(a(), f(a(), x)) -> f#(c(), f(b(), x))) (f#(c(), f(c(), x)) -> f#(a(), x), f#(a(), f(a(), x)) -> f#(b(), x)) (f#(c(), f(c(), x)) -> f#(a(), x), f#(a(), f(a(), x)) -> f#(c(), f(b(), x))) (f#(a(), f(a(), x)) -> f#(b(), x), f#(b(), f(b(), x)) -> f#(a(), f(c(), x))) (f#(a(), f(a(), x)) -> f#(b(), x), f#(b(), f(b(), x)) -> f#(c(), x)) (f#(b(), f(b(), x)) -> f#(c(), x), f#(c(), f(c(), x)) -> f#(b(), f(a(), x))) (f#(b(), f(b(), x)) -> f#(c(), x), f#(c(), f(c(), x)) -> f#(a(), x)) (f#(a(), f(a(), x)) -> f#(c(), f(b(), x)), f#(c(), f(c(), x)) -> f#(b(), f(a(), x))) (f#(a(), f(a(), x)) -> f#(c(), f(b(), x)), f#(c(), f(c(), x)) -> f#(a(), x)) (f#(c(), f(c(), x)) -> f#(b(), f(a(), x)), f#(b(), f(b(), x)) -> f#(c(), x)) (f#(c(), f(c(), x)) -> f#(b(), f(a(), x)), f#(b(), f(b(), x)) -> f#(a(), f(c(), x)))} EDG: {(f#(b(), f(b(), x)) -> f#(a(), f(c(), x)), f#(a(), f(a(), x)) -> f#(b(), x)) (f#(b(), f(b(), x)) -> f#(a(), f(c(), x)), f#(a(), f(a(), x)) -> f#(c(), f(b(), x))) (f#(c(), f(c(), x)) -> f#(a(), x), f#(a(), f(a(), x)) -> f#(b(), x)) (f#(c(), f(c(), x)) -> f#(a(), x), f#(a(), f(a(), x)) -> f#(c(), f(b(), x))) (f#(a(), f(a(), x)) -> f#(b(), x), f#(b(), f(b(), x)) -> f#(a(), f(c(), x))) (f#(a(), f(a(), x)) -> f#(b(), x), f#(b(), f(b(), x)) -> f#(c(), x)) (f#(b(), f(b(), x)) -> f#(c(), x), f#(c(), f(c(), x)) -> f#(b(), f(a(), x))) (f#(b(), f(b(), x)) -> f#(c(), x), f#(c(), f(c(), x)) -> f#(a(), x)) (f#(a(), f(a(), x)) -> f#(c(), f(b(), x)), f#(c(), f(c(), x)) -> f#(b(), f(a(), x))) (f#(a(), f(a(), x)) -> f#(c(), f(b(), x)), f#(c(), f(c(), x)) -> f#(a(), x)) (f#(c(), f(c(), x)) -> f#(b(), f(a(), x)), f#(b(), f(b(), x)) -> f#(c(), x)) (f#(c(), f(c(), x)) -> f#(b(), f(a(), x)), f#(b(), f(b(), x)) -> f#(a(), f(c(), x)))} STATUS: arrows: 0.666667 SCCS (1): Scc: {f#(c(), f(c(), x)) -> f#(b(), f(a(), x)), f#(c(), f(c(), x)) -> f#(a(), x), f#(b(), f(b(), x)) -> f#(c(), x), f#(b(), f(b(), x)) -> f#(a(), f(c(), x)), f#(a(), f(a(), x)) -> f#(c(), f(b(), x)), f#(a(), f(a(), x)) -> f#(b(), x)} SCC (6): Strict: {f#(c(), f(c(), x)) -> f#(b(), f(a(), x)), f#(c(), f(c(), x)) -> f#(a(), x), f#(b(), f(b(), x)) -> f#(c(), x), f#(b(), f(b(), x)) -> f#(a(), f(c(), x)), f#(a(), f(a(), x)) -> f#(c(), f(b(), x)), f#(a(), f(a(), x)) -> f#(b(), x)} Weak: {f(c(), f(c(), x)) -> f(b(), f(a(), x)), f(b(), f(b(), x)) -> f(a(), f(c(), x)), f(a(), f(a(), x)) -> f(c(), f(b(), x))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1) = x0 + x1, [c] = 1, [b] = 1, [a] = 1, [f#](x0, x1) = x0 Strict: f#(a(), f(a(), x)) -> f#(b(), x) 1 + 1x >= 0 + 1x f#(a(), f(a(), x)) -> f#(c(), f(b(), x)) 1 + 1x >= 1 + 1x f#(b(), f(b(), x)) -> f#(a(), f(c(), x)) 1 + 1x >= 1 + 1x f#(b(), f(b(), x)) -> f#(c(), x) 1 + 1x >= 0 + 1x f#(c(), f(c(), x)) -> f#(a(), x) 1 + 1x >= 0 + 1x f#(c(), f(c(), x)) -> f#(b(), f(a(), x)) 1 + 1x >= 1 + 1x Weak: f(a(), f(a(), x)) -> f(c(), f(b(), x)) 2 + 1x >= 2 + 1x f(b(), f(b(), x)) -> f(a(), f(c(), x)) 2 + 1x >= 2 + 1x f(c(), f(c(), x)) -> f(b(), f(a(), x)) 2 + 1x >= 2 + 1x SCCS (1): Scc: {f#(c(), f(c(), x)) -> f#(b(), f(a(), x)), f#(b(), f(b(), x)) -> f#(a(), f(c(), x)), f#(a(), f(a(), x)) -> f#(c(), f(b(), x))} SCC (3): Strict: {f#(c(), f(c(), x)) -> f#(b(), f(a(), x)), f#(b(), f(b(), x)) -> f#(a(), f(c(), x)), f#(a(), f(a(), x)) -> f#(c(), f(b(), x))} Weak: {f(c(), f(c(), x)) -> f(b(), f(a(), x)), f(b(), f(b(), x)) -> f(a(), f(c(), x)), f(a(), f(a(), x)) -> f(c(), f(b(), x))} Fail