YES Time: 0.021222 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#(c(), f(a(), x)) -> 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#(b(), f(a(), 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#(b(), f(a(), x))) (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#(c(), f(a(), x)) -> f#(c(), x)) (f#(b(), f(c(), x)) -> f#(b(), x), f#(c(), f(a(), x)) -> f#(a(), f(c(), x))) (f#(b(), f(c(), x)) -> f#(b(), x), f#(a(), f(b(), x)) -> f#(a(), x)) (f#(b(), f(c(), x)) -> 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#(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#(c(), f(a(), x)) -> f#(c(), x), f#(a(), f(b(), x)) -> f#(a(), x)) (f#(c(), f(a(), x)) -> f#(c(), x), f#(a(), f(b(), x)) -> f#(b(), f(a(), x))) (f#(c(), f(a(), x)) -> f#(c(), x), f#(b(), f(c(), x)) -> f#(c(), f(b(), x))) (f#(c(), f(a(), x)) -> f#(c(), x), f#(b(), f(c(), x)) -> f#(b(), x)) (f#(a(), f(b(), x)) -> f#(a(), x), f#(b(), f(c(), x)) -> f#(b(), x)) (f#(a(), f(b(), x)) -> 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#(b(), 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#(a(), x), f#(c(), f(a(), x)) -> f#(a(), f(c(), x))) (f#(a(), f(b(), x)) -> f#(a(), x), f#(c(), f(a(), x)) -> f#(c(), x)) (f#(c(), f(a(), x)) -> f#(a(), f(c(), x)), f#(b(), f(c(), x)) -> 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#(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#(c(), f(a(), x)) -> f#(a(), f(c(), x)), f#(c(), f(a(), x)) -> f#(a(), f(c(), x))) (f#(c(), f(a(), x)) -> f#(a(), f(c(), x)), f#(c(), f(a(), x)) -> f#(c(), 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#(c(), f(b(), x)), f#(b(), f(c(), x)) -> f#(c(), f(b(), 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#(c(), f(b(), 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))} 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))} EDG: {(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))} EDG: {(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))} STATUS: arrows: 0.833333 SCCS (3): Scc: {f#(c(), f(a(), x)) -> f#(c(), x)} Scc: {f#(a(), f(b(), x)) -> f#(a(), x)} Scc: {f#(b(), f(c(), x)) -> f#(b(), x)} SCC (1): Strict: {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 Weak: f(c(), f(a(), x)) -> f(a(), f(c(), x)) 2 + 1x >= 2 + 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 Qed SCC (1): Strict: {f#(a(), f(b(), x)) -> f#(a(), 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] = 1, [a] = 1, [c] = 0, [f#](x0, x1) = x0 + x1 Strict: f#(a(), f(b(), x)) -> f#(a(), x) 2 + 1x >= 1 + 1x Weak: f(c(), f(a(), x)) -> f(a(), f(c(), x)) 1 + 1x >= 1 + 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)) 1 + 1x >= 1 + 1x Qed SCC (1): Strict: {f#(b(), f(c(), x)) -> f#(b(), 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] = 1, [a] = 0, [c] = 1, [f#](x0, x1) = x0 + x1 Strict: f#(b(), f(c(), x)) -> f#(b(), x) 2 + 1x >= 1 + 1x Weak: f(c(), f(a(), x)) -> f(a(), f(c(), 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)) 2 + 1x >= 2 + 1x Qed