YES Time: 0.042156 TRS: {f(b(), f(c(), x)) -> f(c(), f(b(), x)), f(a(), f(b(), x)) -> f(b(), f(a(), x)), f(c(), f(a(), x)) -> f(a(), f(c(), x))} DP: DP: {f#(b(), f(c(), x)) -> f#(b(), x), f#(b(), f(c(), x)) -> f#(c(), f(b(), x)), f#(a(), f(b(), x)) -> f#(b(), f(a(), x)), f#(a(), f(b(), x)) -> f#(a(), x), f#(c(), f(a(), x)) -> f#(a(), f(c(), x)), f#(c(), f(a(), x)) -> f#(c(), x)} TRS: {f(b(), f(c(), x)) -> f(c(), f(b(), x)), f(a(), f(b(), x)) -> f(b(), f(a(), x)), f(c(), f(a(), x)) -> f(a(), f(c(), x))} EDG: {(f#(a(), f(b(), x)) -> f#(b(), f(a(), x)), f#(b(), f(c(), x)) -> f#(c(), f(b(), x))) (f#(a(), f(b(), x)) -> f#(b(), f(a(), x)), f#(b(), f(c(), x)) -> f#(b(), x)) (f#(b(), f(c(), x)) -> f#(b(), x), f#(b(), f(c(), x)) -> f#(c(), f(b(), x))) (f#(b(), f(c(), x)) -> f#(b(), x), f#(b(), f(c(), x)) -> f#(b(), x)) (f#(c(), f(a(), x)) -> f#(c(), x), f#(c(), f(a(), x)) -> f#(c(), x)) (f#(c(), f(a(), x)) -> f#(c(), x), f#(c(), f(a(), x)) -> f#(a(), f(c(), x))) (f#(a(), f(b(), x)) -> f#(a(), x), f#(a(), f(b(), x)) -> f#(b(), f(a(), x))) (f#(a(), f(b(), x)) -> f#(a(), x), f#(a(), f(b(), x)) -> f#(a(), x)) (f#(c(), f(a(), x)) -> f#(a(), f(c(), x)), f#(a(), f(b(), x)) -> f#(b(), f(a(), x))) (f#(c(), f(a(), x)) -> f#(a(), f(c(), x)), f#(a(), f(b(), x)) -> f#(a(), x)) (f#(b(), f(c(), x)) -> f#(c(), f(b(), x)), f#(c(), f(a(), x)) -> f#(a(), f(c(), x))) (f#(b(), f(c(), x)) -> f#(c(), f(b(), x)), f#(c(), f(a(), x)) -> f#(c(), x))} SCCS (1): Scc: {f#(b(), f(c(), x)) -> f#(b(), x), f#(b(), f(c(), x)) -> f#(c(), f(b(), x)), f#(a(), f(b(), x)) -> f#(b(), f(a(), x)), f#(a(), f(b(), x)) -> f#(a(), x), f#(c(), f(a(), x)) -> f#(a(), f(c(), x)), f#(c(), f(a(), x)) -> f#(c(), x)} SCC (6): Strict: {f#(b(), f(c(), x)) -> f#(b(), x), f#(b(), f(c(), x)) -> f#(c(), f(b(), x)), f#(a(), f(b(), x)) -> f#(b(), f(a(), x)), f#(a(), f(b(), x)) -> f#(a(), x), f#(c(), f(a(), x)) -> f#(a(), f(c(), x)), f#(c(), f(a(), x)) -> f#(c(), x)} Weak: {f(b(), f(c(), x)) -> f(c(), f(b(), x)), f(a(), f(b(), x)) -> f(b(), f(a(), x)), f(c(), f(a(), x)) -> f(a(), f(c(), x))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1) = x0 + x1, [b] = 0, [a] = 1, [c] = 1, [f#](x0, x1) = x0 + x1 Strict: f#(c(), f(a(), x)) -> f#(c(), x) 2 + 1x >= 1 + 1x f#(c(), f(a(), x)) -> f#(a(), f(c(), x)) 2 + 1x >= 2 + 1x f#(a(), f(b(), x)) -> f#(a(), x) 1 + 1x >= 1 + 1x f#(a(), f(b(), x)) -> f#(b(), f(a(), x)) 1 + 1x >= 1 + 1x f#(b(), f(c(), x)) -> f#(c(), f(b(), x)) 1 + 1x >= 1 + 1x f#(b(), f(c(), x)) -> f#(b(), x) 1 + 1x >= 0 + 1x Weak: EDG: {(f#(a(), f(b(), x)) -> f#(b(), f(a(), x)), f#(b(), f(c(), x)) -> f#(c(), f(b(), x))) (f#(a(), f(b(), x)) -> f#(a(), x), f#(a(), f(b(), x)) -> f#(a(), x)) (f#(a(), f(b(), x)) -> f#(a(), x), f#(a(), f(b(), x)) -> f#(b(), f(a(), x))) (f#(c(), f(a(), x)) -> f#(a(), f(c(), x)), f#(a(), f(b(), x)) -> f#(b(), f(a(), x))) (f#(c(), f(a(), x)) -> f#(a(), f(c(), x)), f#(a(), f(b(), x)) -> f#(a(), x)) (f#(b(), f(c(), x)) -> f#(c(), f(b(), x)), f#(c(), f(a(), x)) -> f#(a(), f(c(), x)))} SCCS (1): Scc: {f#(b(), f(c(), x)) -> f#(c(), f(b(), x)), f#(a(), f(b(), x)) -> f#(b(), f(a(), x)), f#(a(), f(b(), x)) -> f#(a(), x), f#(c(), f(a(), x)) -> f#(a(), f(c(), x))} SCC (4): Strict: {f#(b(), f(c(), x)) -> f#(c(), f(b(), x)), f#(a(), f(b(), x)) -> f#(b(), f(a(), x)), f#(a(), f(b(), x)) -> f#(a(), x), f#(c(), f(a(), x)) -> f#(a(), f(c(), x))} Weak: {f(b(), f(c(), x)) -> f(c(), f(b(), x)), f(a(), f(b(), x)) -> f(b(), f(a(), x)), f(c(), f(a(), x)) -> f(a(), f(c(), x))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1) = x0 + x1 + 1, [b] = 1, [a] = 1, [c] = 1, [f#](x0, x1) = x0 Strict: f#(c(), f(a(), x)) -> f#(a(), f(c(), x)) 2 + 1x >= 2 + 1x f#(a(), f(b(), x)) -> f#(a(), x) 2 + 1x >= 0 + 1x f#(a(), f(b(), x)) -> f#(b(), f(a(), x)) 2 + 1x >= 2 + 1x f#(b(), f(c(), x)) -> f#(c(), f(b(), x)) 2 + 1x >= 2 + 1x Weak: EDG: {(f#(a(), f(b(), x)) -> f#(b(), f(a(), x)), f#(b(), f(c(), x)) -> f#(c(), f(b(), x))) (f#(c(), f(a(), x)) -> f#(a(), f(c(), x)), f#(a(), f(b(), x)) -> f#(b(), f(a(), x))) (f#(b(), f(c(), x)) -> f#(c(), f(b(), x)), f#(c(), f(a(), x)) -> f#(a(), f(c(), x)))} SCCS (1): Scc: {f#(b(), f(c(), x)) -> f#(c(), f(b(), x)), f#(a(), f(b(), x)) -> f#(b(), f(a(), x)), f#(c(), f(a(), x)) -> f#(a(), f(c(), x))} SCC (3): Strict: {f#(b(), f(c(), x)) -> f#(c(), f(b(), x)), f#(a(), f(b(), x)) -> f#(b(), f(a(), x)), f#(c(), f(a(), x)) -> f#(a(), f(c(), x))} Weak: {f(b(), f(c(), x)) -> f(c(), f(b(), x)), f(a(), f(b(), x)) -> f(b(), f(a(), x)), f(c(), f(a(), x)) -> f(a(), f(c(), x))} BOUND: Bound: match(-raise)-DP-bounded by 0 Automaton: { c_0() -> 11* a_0() -> 10* b_0() -> 9* f#_0(9, 12) -> 6* f_0(12, 12) -> 8* f_0(12, 11) -> 8* f_0(12, 10) -> 8* f_0(12, 9) -> 8* f_0(12, 8) -> 8* f_0(11, 12) -> 8* f_0(11, 11) -> 8* f_0(11, 10) -> 8* f_0(11, 9) -> 8* f_0(11, 8) -> 8* f_0(10, 12) -> 12* f_0(10, 11) -> 12* f_0(10, 10) -> 12* f_0(10, 9) -> 12* f_0(10, 8) -> 12 | 8 f_0(9, 12) -> 12 | 8 f_0(9, 11) -> 8* f_0(9, 10) -> 8* f_0(9, 9) -> 8* f_0(9, 8) -> 8* f_0(8, 12) -> 8* f_0(8, 11) -> 8* f_0(8, 10) -> 8* f_0(8, 9) -> 8* f_0(8, 8) -> 8*} Strict: {f#(b(), f(c(), x)) -> f#(c(), f(b(), x)), f#(c(), f(a(), x)) -> f#(a(), f(c(), x))} EDG: {(f#(b(), f(c(), x)) -> f#(c(), f(b(), x)), f#(c(), f(a(), x)) -> f#(a(), f(c(), x)))} SCCS (0): Qed