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