MAYBE Time: 0.129171 TRS: { *(x, *(y, z)) -> *(*(x, y), z), *(x, 1()) -> x, *(x, i x) -> 1(), *(*(x, y), i y) -> x, *(*(x, i y), y) -> x, *(*(i x, k(y, z)), x) -> k(*(*(i x, y), x), *(*(i x, z), x)), *(1(), y) -> y, *(i x, x) -> 1(), *(k(x, y), k(y, x)) -> 1(), i *(x, y) -> *(i y, i x), i 1() -> 1(), i i x -> x, k(x, x) -> 1(), k(x, 1()) -> 1(), k(*(x, i y), *(y, i x)) -> 1()} DP: DP: { *#(x, *(y, z)) -> *#(x, y), *#(x, *(y, z)) -> *#(*(x, y), z), *#(*(i x, k(y, z)), x) -> *#(*(i x, y), x), *#(*(i x, k(y, z)), x) -> *#(*(i x, z), x), *#(*(i x, k(y, z)), x) -> *#(i x, y), *#(*(i x, k(y, z)), x) -> *#(i x, z), *#(*(i x, k(y, z)), x) -> k#(*(*(i x, y), x), *(*(i x, z), x)), i# *(x, y) -> *#(i y, i x), i# *(x, y) -> i# x, i# *(x, y) -> i# y} TRS: { *(x, *(y, z)) -> *(*(x, y), z), *(x, 1()) -> x, *(x, i x) -> 1(), *(*(x, y), i y) -> x, *(*(x, i y), y) -> x, *(*(i x, k(y, z)), x) -> k(*(*(i x, y), x), *(*(i x, z), x)), *(1(), y) -> y, *(i x, x) -> 1(), *(k(x, y), k(y, x)) -> 1(), i *(x, y) -> *(i y, i x), i 1() -> 1(), i i x -> x, k(x, x) -> 1(), k(x, 1()) -> 1(), k(*(x, i y), *(y, i x)) -> 1()} UR: { *(x, *(y, z)) -> *(*(x, y), z), *(x, 1()) -> x, *(x, i x) -> 1(), *(*(x, y), i y) -> x, *(*(x, i y), y) -> x, *(*(i x, k(y, z)), x) -> k(*(*(i x, y), x), *(*(i x, z), x)), *(1(), y) -> y, *(i x, x) -> 1(), *(k(x, y), k(y, x)) -> 1(), i *(x, y) -> *(i y, i x), i 1() -> 1(), i i x -> x, k(x, x) -> 1(), k(x, 1()) -> 1(), k(*(x, i y), *(y, i x)) -> 1(), a(w, v) -> w, a(w, v) -> v} EDG: {(*#(x, *(y, z)) -> *#(x, y), *#(*(i x, k(y, z)), x) -> k#(*(*(i x, y), x), *(*(i x, z), x))) (*#(x, *(y, z)) -> *#(x, y), *#(*(i x, k(y, z)), x) -> *#(i x, z)) (*#(x, *(y, z)) -> *#(x, y), *#(*(i x, k(y, z)), x) -> *#(i x, y)) (*#(x, *(y, z)) -> *#(x, y), *#(*(i x, k(y, z)), x) -> *#(*(i x, z), x)) (*#(x, *(y, z)) -> *#(x, y), *#(*(i x, k(y, z)), x) -> *#(*(i x, y), x)) (*#(x, *(y, z)) -> *#(x, y), *#(x, *(y, z)) -> *#(*(x, y), z)) (*#(x, *(y, z)) -> *#(x, y), *#(x, *(y, z)) -> *#(x, y)) (*#(*(i x, k(y, z)), x) -> *#(i x, z), *#(*(i x, k(y, z)), x) -> k#(*(*(i x, y), x), *(*(i x, z), x))) (*#(*(i x, k(y, z)), x) -> *#(i x, z), *#(*(i x, k(y, z)), x) -> *#(i x, z)) (*#(*(i x, k(y, z)), x) -> *#(i x, z), *#(*(i x, k(y, z)), x) -> *#(i x, y)) (*#(*(i x, k(y, z)), x) -> *#(i x, z), *#(*(i x, k(y, z)), x) -> *#(*(i x, z), x)) (*#(*(i x, k(y, z)), x) -> *#(i x, z), *#(*(i x, k(y, z)), x) -> *#(*(i x, y), x)) (*#(*(i x, k(y, z)), x) -> *#(i x, z), *#(x, *(y, z)) -> *#(*(x, y), z)) (*#(*(i x, k(y, z)), x) -> *#(i x, z), *#(x, *(y, z)) -> *#(x, y)) (*#(*(i x, k(y, z)), x) -> *#(*(i x, y), x), *#(*(i x, k(y, z)), x) -> k#(*(*(i x, y), x), *(*(i x, z), x))) (*#(*(i x, k(y, z)), x) -> *#(*(i x, y), x), *#(*(i x, k(y, z)), x) -> *#(i x, z)) (*#(*(i x, k(y, z)), x) -> *#(*(i x, y), x), *#(*(i x, k(y, z)), x) -> *#(i x, y)) (*#(*(i x, k(y, z)), x) -> *#(*(i x, y), x), *#(*(i x, k(y, z)), x) -> *#(*(i x, z), x)) (*#(*(i x, k(y, z)), x) -> *#(*(i x, y), x), *#(*(i x, k(y, z)), x) -> *#(*(i x, y), x)) (*#(*(i x, k(y, z)), x) -> *#(*(i x, y), x), *#(x, *(y, z)) -> *#(*(x, y), z)) (*#(*(i x, k(y, z)), x) -> *#(*(i x, y), x), *#(x, *(y, z)) -> *#(x, y)) (i# *(x, y) -> i# x, i# *(x, y) -> i# y) (i# *(x, y) -> i# x, i# *(x, y) -> i# x) (i# *(x, y) -> i# x, i# *(x, y) -> *#(i y, i x)) (*#(*(i x, k(y, z)), x) -> *#(*(i x, z), x), *#(x, *(y, z)) -> *#(x, y)) (*#(*(i x, k(y, z)), x) -> *#(*(i x, z), x), *#(x, *(y, z)) -> *#(*(x, y), z)) (*#(*(i x, k(y, z)), x) -> *#(*(i x, z), x), *#(*(i x, k(y, z)), x) -> *#(*(i x, y), x)) (*#(*(i x, k(y, z)), x) -> *#(*(i x, z), x), *#(*(i x, k(y, z)), x) -> *#(*(i x, z), x)) (*#(*(i x, k(y, z)), x) -> *#(*(i x, z), x), *#(*(i x, k(y, z)), x) -> *#(i x, y)) (*#(*(i x, k(y, z)), x) -> *#(*(i x, z), x), *#(*(i x, k(y, z)), x) -> *#(i x, z)) (*#(*(i x, k(y, z)), x) -> *#(*(i x, z), x), *#(*(i x, k(y, z)), x) -> k#(*(*(i x, y), x), *(*(i x, z), x))) (*#(*(i x, k(y, z)), x) -> *#(i x, y), *#(x, *(y, z)) -> *#(x, y)) (*#(*(i x, k(y, z)), x) -> *#(i x, y), *#(x, *(y, z)) -> *#(*(x, y), z)) (*#(*(i x, k(y, z)), x) -> *#(i x, y), *#(*(i x, k(y, z)), x) -> *#(*(i x, y), x)) (*#(*(i x, k(y, z)), x) -> *#(i x, y), *#(*(i x, k(y, z)), x) -> *#(*(i x, z), x)) (*#(*(i x, k(y, z)), x) -> *#(i x, y), *#(*(i x, k(y, z)), x) -> *#(i x, y)) (*#(*(i x, k(y, z)), x) -> *#(i x, y), *#(*(i x, k(y, z)), x) -> *#(i x, z)) (*#(*(i x, k(y, z)), x) -> *#(i x, y), *#(*(i x, k(y, z)), x) -> k#(*(*(i x, y), x), *(*(i x, z), x))) (*#(x, *(y, z)) -> *#(*(x, y), z), *#(x, *(y, z)) -> *#(x, y)) (*#(x, *(y, z)) -> *#(*(x, y), z), *#(x, *(y, z)) -> *#(*(x, y), z)) (*#(x, *(y, z)) -> *#(*(x, y), z), *#(*(i x, k(y, z)), x) -> *#(*(i x, y), x)) (*#(x, *(y, z)) -> *#(*(x, y), z), *#(*(i x, k(y, z)), x) -> *#(*(i x, z), x)) (*#(x, *(y, z)) -> *#(*(x, y), z), *#(*(i x, k(y, z)), x) -> *#(i x, y)) (*#(x, *(y, z)) -> *#(*(x, y), z), *#(*(i x, k(y, z)), x) -> *#(i x, z)) (*#(x, *(y, z)) -> *#(*(x, y), z), *#(*(i x, k(y, z)), x) -> k#(*(*(i x, y), x), *(*(i x, z), x))) (i# *(x, y) -> *#(i y, i x), *#(x, *(y, z)) -> *#(x, y)) (i# *(x, y) -> *#(i y, i x), *#(x, *(y, z)) -> *#(*(x, y), z)) (i# *(x, y) -> *#(i y, i x), *#(*(i x, k(y, z)), x) -> *#(*(i x, y), x)) (i# *(x, y) -> *#(i y, i x), *#(*(i x, k(y, z)), x) -> *#(*(i x, z), x)) (i# *(x, y) -> *#(i y, i x), *#(*(i x, k(y, z)), x) -> *#(i x, y)) (i# *(x, y) -> *#(i y, i x), *#(*(i x, k(y, z)), x) -> *#(i x, z)) (i# *(x, y) -> *#(i y, i x), *#(*(i x, k(y, z)), x) -> k#(*(*(i x, y), x), *(*(i x, z), x))) (i# *(x, y) -> i# y, i# *(x, y) -> *#(i y, i x)) (i# *(x, y) -> i# y, i# *(x, y) -> i# x) (i# *(x, y) -> i# y, i# *(x, y) -> i# y)} STATUS: arrows: 0.450000 SCCS (2): Scc: {i# *(x, y) -> i# x, i# *(x, y) -> i# y} Scc: { *#(x, *(y, z)) -> *#(x, y), *#(x, *(y, z)) -> *#(*(x, y), z), *#(*(i x, k(y, z)), x) -> *#(*(i x, y), x), *#(*(i x, k(y, z)), x) -> *#(*(i x, z), x), *#(*(i x, k(y, z)), x) -> *#(i x, y), *#(*(i x, k(y, z)), x) -> *#(i x, z)} SCC (2): Strict: {i# *(x, y) -> i# x, i# *(x, y) -> i# y} Weak: { *(x, *(y, z)) -> *(*(x, y), z), *(x, 1()) -> x, *(x, i x) -> 1(), *(*(x, y), i y) -> x, *(*(x, i y), y) -> x, *(*(i x, k(y, z)), x) -> k(*(*(i x, y), x), *(*(i x, z), x)), *(1(), y) -> y, *(i x, x) -> 1(), *(k(x, y), k(y, x)) -> 1(), i *(x, y) -> *(i y, i x), i 1() -> 1(), i i x -> x, k(x, x) -> 1(), k(x, 1()) -> 1(), k(*(x, i y), *(y, i x)) -> 1()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [*](x0, x1) = x0 + x1 + 1, [k](x0, x1) = x0, [i](x0) = 0, [1] = 1, [i#](x0) = x0 Strict: i# *(x, y) -> i# y 1 + 1x + 1y >= 0 + 1y i# *(x, y) -> i# x 1 + 1x + 1y >= 0 + 1x Weak: k(*(x, i y), *(y, i x)) -> 1() 1 + 1x + 0y >= 1 k(x, 1()) -> 1() 0 + 1x >= 1 k(x, x) -> 1() 0 + 1x >= 1 i i x -> x 0 + 0x >= 1x i 1() -> 1() 0 >= 1 i *(x, y) -> *(i y, i x) 0 + 0x + 0y >= 1 + 0x + 0y *(k(x, y), k(y, x)) -> 1() 1 + 1x + 1y >= 1 *(i x, x) -> 1() 1 + 1x >= 1 *(1(), y) -> y 2 + 1y >= 1y *(*(i x, k(y, z)), x) -> k(*(*(i x, y), x), *(*(i x, z), x)) 2 + 1x + 1y + 0z >= 2 + 1x + 1y + 0z *(*(x, i y), y) -> x 2 + 1x + 1y >= 1x *(*(x, y), i y) -> x 2 + 1x + 1y >= 1x *(x, i x) -> 1() 1 + 1x >= 1 *(x, 1()) -> x 2 + 1x >= 1x *(x, *(y, z)) -> *(*(x, y), z) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z Qed SCC (6): Strict: { *#(x, *(y, z)) -> *#(x, y), *#(x, *(y, z)) -> *#(*(x, y), z), *#(*(i x, k(y, z)), x) -> *#(*(i x, y), x), *#(*(i x, k(y, z)), x) -> *#(*(i x, z), x), *#(*(i x, k(y, z)), x) -> *#(i x, y), *#(*(i x, k(y, z)), x) -> *#(i x, z)} Weak: { *(x, *(y, z)) -> *(*(x, y), z), *(x, 1()) -> x, *(x, i x) -> 1(), *(*(x, y), i y) -> x, *(*(x, i y), y) -> x, *(*(i x, k(y, z)), x) -> k(*(*(i x, y), x), *(*(i x, z), x)), *(1(), y) -> y, *(i x, x) -> 1(), *(k(x, y), k(y, x)) -> 1(), i *(x, y) -> *(i y, i x), i 1() -> 1(), i i x -> x, k(x, x) -> 1(), k(x, 1()) -> 1(), k(*(x, i y), *(y, i x)) -> 1()} Fail