MAYBE Time: 0.045031 TRS: {f(a(), f(b(), x)) -> f(a(), f(a(), f(a(), x))), f(b(), f(a(), x)) -> f(b(), f(b(), f(b(), x)))} DP: DP: {f#(a(), f(b(), x)) -> f#(a(), x), f#(a(), f(b(), x)) -> f#(a(), f(a(), x)), f#(a(), f(b(), x)) -> f#(a(), f(a(), f(a(), x))), f#(b(), f(a(), x)) -> f#(b(), x), f#(b(), f(a(), x)) -> f#(b(), f(b(), x)), f#(b(), f(a(), x)) -> f#(b(), f(b(), f(b(), x)))} TRS: {f(a(), f(b(), x)) -> f(a(), f(a(), f(a(), x))), f(b(), f(a(), x)) -> f(b(), f(b(), f(b(), x)))} UR: {f(a(), f(b(), x)) -> f(a(), f(a(), f(a(), x))), f(b(), f(a(), x)) -> f(b(), f(b(), f(b(), x)))} EDG: {(f#(b(), f(a(), x)) -> f#(b(), f(b(), x)), f#(b(), f(a(), x)) -> f#(b(), f(b(), f(b(), x)))) (f#(b(), f(a(), x)) -> f#(b(), f(b(), x)), f#(b(), f(a(), x)) -> f#(b(), f(b(), x))) (f#(b(), f(a(), x)) -> f#(b(), f(b(), x)), f#(b(), f(a(), x)) -> f#(b(), x)) (f#(b(), f(a(), x)) -> f#(b(), f(b(), x)), f#(a(), f(b(), x)) -> f#(a(), f(a(), f(a(), x)))) (f#(b(), f(a(), x)) -> f#(b(), f(b(), x)), f#(a(), f(b(), x)) -> f#(a(), f(a(), x))) (f#(b(), f(a(), x)) -> f#(b(), f(b(), x)), f#(a(), f(b(), x)) -> f#(a(), x)) (f#(b(), f(a(), x)) -> f#(b(), f(b(), f(b(), x))), f#(b(), f(a(), x)) -> f#(b(), f(b(), f(b(), x)))) (f#(b(), f(a(), x)) -> f#(b(), f(b(), f(b(), x))), f#(b(), f(a(), x)) -> f#(b(), f(b(), x))) (f#(b(), f(a(), x)) -> f#(b(), f(b(), f(b(), x))), f#(b(), f(a(), x)) -> f#(b(), x)) (f#(b(), f(a(), x)) -> f#(b(), f(b(), f(b(), x))), f#(a(), f(b(), x)) -> f#(a(), f(a(), f(a(), x)))) (f#(b(), f(a(), x)) -> f#(b(), f(b(), f(b(), x))), f#(a(), f(b(), x)) -> f#(a(), f(a(), x))) (f#(b(), f(a(), x)) -> f#(b(), f(b(), f(b(), x))), f#(a(), f(b(), x)) -> f#(a(), x)) (f#(b(), f(a(), x)) -> f#(b(), x), f#(b(), f(a(), x)) -> f#(b(), f(b(), f(b(), x)))) (f#(b(), f(a(), x)) -> f#(b(), x), f#(b(), f(a(), x)) -> f#(b(), f(b(), x))) (f#(b(), f(a(), x)) -> f#(b(), x), f#(b(), f(a(), x)) -> f#(b(), x)) (f#(b(), f(a(), x)) -> f#(b(), x), f#(a(), f(b(), x)) -> f#(a(), f(a(), f(a(), x)))) (f#(b(), f(a(), x)) -> f#(b(), x), f#(a(), f(b(), x)) -> f#(a(), f(a(), x))) (f#(b(), f(a(), x)) -> 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#(a(), x), f#(a(), f(b(), x)) -> f#(a(), f(a(), x))) (f#(a(), f(b(), x)) -> f#(a(), x), f#(a(), f(b(), x)) -> f#(a(), f(a(), f(a(), x)))) (f#(a(), f(b(), x)) -> f#(a(), x), f#(b(), f(a(), x)) -> f#(b(), x)) (f#(a(), f(b(), x)) -> f#(a(), x), f#(b(), f(a(), x)) -> f#(b(), f(b(), x))) (f#(a(), f(b(), x)) -> f#(a(), x), f#(b(), f(a(), x)) -> f#(b(), f(b(), f(b(), x)))) (f#(a(), f(b(), x)) -> f#(a(), f(a(), f(a(), x))), f#(a(), f(b(), x)) -> f#(a(), x)) (f#(a(), f(b(), x)) -> f#(a(), f(a(), f(a(), x))), f#(a(), f(b(), x)) -> f#(a(), f(a(), x))) (f#(a(), f(b(), x)) -> f#(a(), f(a(), f(a(), x))), f#(a(), f(b(), x)) -> f#(a(), f(a(), f(a(), x)))) (f#(a(), f(b(), x)) -> f#(a(), f(a(), f(a(), x))), f#(b(), f(a(), x)) -> f#(b(), x)) (f#(a(), f(b(), x)) -> f#(a(), f(a(), f(a(), x))), f#(b(), f(a(), x)) -> f#(b(), f(b(), x))) (f#(a(), f(b(), x)) -> f#(a(), f(a(), f(a(), x))), f#(b(), f(a(), x)) -> f#(b(), f(b(), f(b(), x)))) (f#(a(), f(b(), x)) -> f#(a(), f(a(), x)), f#(a(), f(b(), x)) -> f#(a(), x)) (f#(a(), f(b(), x)) -> f#(a(), f(a(), x)), f#(a(), f(b(), x)) -> f#(a(), f(a(), x))) (f#(a(), f(b(), x)) -> f#(a(), f(a(), x)), f#(a(), f(b(), x)) -> f#(a(), f(a(), f(a(), x)))) (f#(a(), f(b(), x)) -> f#(a(), f(a(), x)), f#(b(), f(a(), x)) -> f#(b(), x)) (f#(a(), f(b(), x)) -> f#(a(), f(a(), x)), f#(b(), f(a(), x)) -> f#(b(), f(b(), x))) (f#(a(), f(b(), x)) -> f#(a(), f(a(), x)), f#(b(), f(a(), x)) -> f#(b(), f(b(), f(b(), x))))} STATUS: arrows: 0.000000 SCCS (1): Scc: {f#(a(), f(b(), x)) -> f#(a(), x), f#(a(), f(b(), x)) -> f#(a(), f(a(), x)), f#(a(), f(b(), x)) -> f#(a(), f(a(), f(a(), x))), f#(b(), f(a(), x)) -> f#(b(), x), f#(b(), f(a(), x)) -> f#(b(), f(b(), x)), f#(b(), f(a(), x)) -> f#(b(), f(b(), f(b(), x)))} SCC (6): Strict: {f#(a(), f(b(), x)) -> f#(a(), x), f#(a(), f(b(), x)) -> f#(a(), f(a(), x)), f#(a(), f(b(), x)) -> f#(a(), f(a(), f(a(), x))), f#(b(), f(a(), x)) -> f#(b(), x), f#(b(), f(a(), x)) -> f#(b(), f(b(), x)), f#(b(), f(a(), x)) -> f#(b(), f(b(), f(b(), x)))} Weak: {f(a(), f(b(), x)) -> f(a(), f(a(), f(a(), x))), f(b(), f(a(), x)) -> f(b(), f(b(), f(b(), x)))} Fail