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