YES Time: 29.718836 TRS: { f(x, f(x, y)) -> f(f(f(x, a()), a()), a()), f(y, f(x, f(a(), x))) -> f(f(f(a(), x), f(x, a())), f(a(), y))} DP: DP: { f#(x, f(x, y)) -> f#(x, a()), f#(x, f(x, y)) -> f#(f(x, a()), a()), f#(x, f(x, y)) -> f#(f(f(x, a()), a()), a()), f#(y, f(x, f(a(), x))) -> f#(x, a()), f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y)), f#(y, f(x, f(a(), x))) -> f#(f(a(), x), f(x, a())), f#(y, f(x, f(a(), x))) -> f#(a(), y)} TRS: { f(x, f(x, y)) -> f(f(f(x, a()), a()), a()), f(y, f(x, f(a(), x))) -> f(f(f(a(), x), f(x, a())), f(a(), y))} EDG: {(f#(y, f(x, f(a(), x))) -> f#(a(), y), f#(y, f(x, f(a(), x))) -> f#(a(), y)) (f#(y, f(x, f(a(), x))) -> f#(a(), y), f#(y, f(x, f(a(), x))) -> f#(f(a(), x), f(x, a()))) (f#(y, f(x, f(a(), x))) -> f#(a(), y), f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y))) (f#(y, f(x, f(a(), x))) -> f#(a(), y), f#(y, f(x, f(a(), x))) -> f#(x, a())) (f#(y, f(x, f(a(), x))) -> f#(a(), y), f#(x, f(x, y)) -> f#(f(f(x, a()), a()), a())) (f#(y, f(x, f(a(), x))) -> f#(a(), y), f#(x, f(x, y)) -> f#(f(x, a()), a())) (f#(y, f(x, f(a(), x))) -> f#(a(), y), f#(x, f(x, y)) -> f#(x, a())) (f#(y, f(x, f(a(), x))) -> f#(f(a(), x), f(x, a())), f#(x, f(x, y)) -> f#(x, a())) (f#(y, f(x, f(a(), x))) -> f#(f(a(), x), f(x, a())), f#(x, f(x, y)) -> f#(f(x, a()), a())) (f#(y, f(x, f(a(), x))) -> f#(f(a(), x), f(x, a())), f#(x, f(x, y)) -> f#(f(f(x, a()), a()), a())) (f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y)), f#(x, f(x, y)) -> f#(x, a())) (f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y)), f#(x, f(x, y)) -> f#(f(x, a()), a())) (f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y)), f#(x, f(x, y)) -> f#(f(f(x, a()), a()), a())) (f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y)), f#(y, f(x, f(a(), x))) -> f#(x, a())) (f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y)), f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y))) (f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y)), f#(y, f(x, f(a(), x))) -> f#(f(a(), x), f(x, a()))) (f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y)), f#(y, f(x, f(a(), x))) -> f#(a(), y))} SCCS (1): Scc: {f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y)), f#(y, f(x, f(a(), x))) -> f#(a(), y)} SCC (2): Strict: {f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y)), f#(y, f(x, f(a(), x))) -> f#(a(), y)} Weak: { f(x, f(x, y)) -> f(f(f(x, a()), a()), a()), f(y, f(x, f(a(), x))) -> f(f(f(a(), x), f(x, a())), f(a(), y))} BOUND: Bound: match(-raise)-DP-bounded by 1 Automaton: { a_1() -> 9* f#_1(25, 25) -> 4* f#_1(25, 23) -> 4* f#_1(25, 22) -> 4* f#_1(25, 21) -> 4* f#_1(25, 19) -> 4* f#_1(25, 17) -> 4* f#_1(25, 14) -> 4* f#_1(24, 25) -> 4* f#_1(24, 23) -> 4* f#_1(24, 22) -> 4* f#_1(24, 21) -> 4* f#_1(24, 19) -> 4* f#_1(24, 17) -> 4* f#_1(24, 14) -> 4* f#_1(23, 25) -> 4* f#_1(23, 23) -> 4* f#_1(23, 22) -> 4* f#_1(23, 21) -> 4* f#_1(23, 19) -> 4* f#_1(23, 17) -> 4* f#_1(23, 14) -> 4* f#_1(21, 25) -> 4* f#_1(21, 23) -> 4* f#_1(21, 22) -> 4* f#_1(21, 21) -> 4* f#_1(21, 19) -> 4* f#_1(21, 17) -> 4* f#_1(21, 14) -> 4* f#_1(20, 25) -> 4* f#_1(20, 23) -> 4* f#_1(20, 22) -> 4* f#_1(20, 21) -> 4* f#_1(20, 19) -> 4* f#_1(20, 17) -> 4* f#_1(20, 14) -> 4* f#_1(18, 25) -> 4* f#_1(18, 23) -> 4* f#_1(18, 22) -> 4* f#_1(18, 21) -> 4* f#_1(18, 19) -> 4* f#_1(18, 17) -> 4* f#_1(18, 14) -> 4* f#_1(16, 25) -> 4* f#_1(16, 23) -> 4* f#_1(16, 22) -> 4* f#_1(16, 21) -> 4* f#_1(16, 19) -> 4* f#_1(16, 17) -> 4* f#_1(16, 14) -> 4* f#_1(9, 25) -> 4* f#_1(9, 24) -> 4* f#_1(9, 23) -> 4* f#_1(9, 21) -> 4* f#_1(9, 20) -> 4* f#_1(9, 18) -> 4* f#_1(9, 16) -> 4* f#_0(25, 15) -> 4* f#_0(24, 15) -> 4* f#_0(23, 15) -> 4* f#_0(21, 15) -> 4* f#_0(20, 15) -> 4* f#_0(18, 15) -> 4* f#_0(16, 15) -> 4* f_1(15, 15) -> 16* f_1(9, 25) -> 14* f_1(9, 24) -> 14* f_1(9, 23) -> 14* f_1(9, 21) -> 14* f_1(9, 20) -> 14* f_1(9, 18) -> 14* f_1(9, 16) -> 14* f_1(9, 9) -> 15* f_0(25, 25) -> 18* | 16 | 10 f_0(25, 24) -> 18* | 16 | 10 f_0(25, 23) -> 10* f_0(25, 22) -> 10* f_0(25, 21) -> 18* | 16 | 10 f_0(25, 20) -> 18* | 16 | 10 f_0(25, 19) -> 18* | 16 | 10 f_0(25, 18) -> 10* f_0(25, 17) -> 18* | 16 | 10 f_0(25, 16) -> 10* f_0(25, 15) -> 23* | 22 | 18 | 16 | 14 | 10 f_0(25, 14) -> 10* f_0(25, 12) -> 18* | 16 | 10 f_0(25, 10) -> 10* f_0(25, 9) -> 25* | 24 | 21 | 20 | 19 | 18 | 17 | 16 | 14 | 12 | 10 f_0(24, 25) -> 10* f_0(24, 24) -> 10* f_0(24, 23) -> 10* f_0(24, 22) -> 10* f_0(24, 21) -> 10* f_0(24, 20) -> 10* f_0(24, 19) -> 10* f_0(24, 18) -> 10* f_0(24, 17) -> 10* f_0(24, 16) -> 10* f_0(24, 15) -> 22* | 14 | 10 f_0(24, 14) -> 10* f_0(24, 12) -> 10* f_0(24, 10) -> 10* f_0(24, 9) -> 25* | 24 | 21 | 20 | 19 | 18 | 17 | 16 | 14 | 12 | 10 f_0(23, 25) -> 18* | 16 | 10 f_0(23, 24) -> 18* | 16 | 10 f_0(23, 23) -> 10* f_0(23, 22) -> 10* f_0(23, 21) -> 18* | 16 | 10 f_0(23, 20) -> 18* | 16 | 10 f_0(23, 19) -> 18* | 16 | 10 f_0(23, 18) -> 10* f_0(23, 17) -> 18* | 16 | 10 f_0(23, 16) -> 10* f_0(23, 15) -> 23* | 22 | 18 | 16 | 14 | 10 f_0(23, 14) -> 10* f_0(23, 12) -> 18* | 16 | 10 f_0(23, 10) -> 10* f_0(23, 9) -> 24* | 20 | 18 | 16 | 12 f_0(22, 25) -> 18* | 16 | 10 f_0(22, 24) -> 18* | 16 | 10 f_0(22, 23) -> 10* f_0(22, 22) -> 10* f_0(22, 21) -> 18* | 16 | 10 f_0(22, 20) -> 18* | 16 | 10 f_0(22, 19) -> 18* | 16 | 10 f_0(22, 18) -> 10* f_0(22, 17) -> 18* | 16 | 10 f_0(22, 16) -> 10* f_0(22, 15) -> 18* | 16 | 10 f_0(22, 14) -> 10* f_0(22, 12) -> 18* | 16 | 10 f_0(22, 10) -> 10* f_0(22, 9) -> 24* | 20 | 18 | 16 | 12 f_0(21, 25) -> 18* | 16 | 10 f_0(21, 24) -> 18* | 16 | 10 f_0(21, 23) -> 10* f_0(21, 22) -> 10* f_0(21, 21) -> 18* | 16 | 10 f_0(21, 20) -> 18* | 16 | 10 f_0(21, 19) -> 18* | 16 | 10 f_0(21, 18) -> 10* f_0(21, 17) -> 18* | 16 | 10 f_0(21, 16) -> 10* f_0(21, 15) -> 23* | 22 | 18 | 16 | 14 | 10 f_0(21, 14) -> 10* f_0(21, 12) -> 18* | 16 | 10 f_0(21, 10) -> 10* f_0(21, 9) -> 25* | 24 | 21 | 20 | 19 | 18 | 17 | 16 | 14 | 12 | 10 f_0(20, 25) -> 10* f_0(20, 24) -> 10* f_0(20, 23) -> 10* f_0(20, 22) -> 10* f_0(20, 21) -> 10* f_0(20, 20) -> 10* f_0(20, 19) -> 10* f_0(20, 18) -> 10* f_0(20, 17) -> 10* f_0(20, 16) -> 10* f_0(20, 15) -> 22* | 14 | 10 f_0(20, 14) -> 10* f_0(20, 12) -> 10* f_0(20, 10) -> 10* f_0(20, 9) -> 19* | 17 | 14 | 12 | 10 f_0(19, 25) -> 18* | 16 | 10 f_0(19, 24) -> 18* | 16 | 10 f_0(19, 23) -> 10* f_0(19, 22) -> 10* f_0(19, 21) -> 18* | 16 | 10 f_0(19, 20) -> 18* | 16 | 10 f_0(19, 19) -> 18* | 16 | 10 f_0(19, 18) -> 10* f_0(19, 17) -> 18* | 16 | 10 f_0(19, 16) -> 10* f_0(19, 15) -> 18* | 16 | 10 f_0(19, 14) -> 10* f_0(19, 12) -> 18* | 16 | 10 f_0(19, 10) -> 10* f_0(19, 9) -> 25* | 24 | 21 | 20 | 19 | 18 | 17 | 16 | 14 | 12 | 10 f_0(18, 25) -> 10* f_0(18, 24) -> 10* f_0(18, 23) -> 10* f_0(18, 22) -> 10* f_0(18, 21) -> 10* f_0(18, 20) -> 10* f_0(18, 19) -> 10* f_0(18, 18) -> 10* f_0(18, 17) -> 10* f_0(18, 16) -> 10* f_0(18, 15) -> 22* | 14 | 10 f_0(18, 14) -> 10* f_0(18, 12) -> 10* f_0(18, 10) -> 10* f_0(18, 9) -> 24* | 20 | 18 | 16 | 12 f_0(17, 25) -> 18* | 16 | 10 f_0(17, 24) -> 18* | 16 | 10 f_0(17, 23) -> 10* f_0(17, 22) -> 10* f_0(17, 21) -> 18* | 16 | 10 f_0(17, 20) -> 18* | 16 | 10 f_0(17, 19) -> 18* | 16 | 10 f_0(17, 18) -> 10* f_0(17, 17) -> 18* | 16 | 10 f_0(17, 16) -> 10* f_0(17, 15) -> 18* | 16 | 10 f_0(17, 14) -> 10* f_0(17, 12) -> 18* | 16 | 10 f_0(17, 10) -> 10* f_0(17, 9) -> 19* | 17 | 14 | 12 | 10 f_0(16, 25) -> 10* f_0(16, 24) -> 10* f_0(16, 23) -> 10* f_0(16, 22) -> 10* f_0(16, 21) -> 10* f_0(16, 20) -> 10* f_0(16, 19) -> 10* f_0(16, 18) -> 10* f_0(16, 17) -> 10* f_0(16, 16) -> 10* f_0(16, 15) -> 22* | 14 | 10 f_0(16, 14) -> 10* f_0(16, 12) -> 10* f_0(16, 10) -> 10* f_0(16, 9) -> 12* f_0(15, 25) -> 18* | 16 | 10 f_0(15, 24) -> 18* | 16 | 10 f_0(15, 23) -> 10* f_0(15, 22) -> 10* f_0(15, 21) -> 18* | 16 | 10 f_0(15, 20) -> 18* | 16 | 10 f_0(15, 19) -> 18* | 16 | 10 f_0(15, 18) -> 10* f_0(15, 17) -> 18* | 16 | 10 f_0(15, 16) -> 10* f_0(15, 14) -> 10* f_0(15, 12) -> 16* f_0(15, 10) -> 10* f_0(15, 9) -> 12* f_0(14, 25) -> 18* | 16 | 10 f_0(14, 24) -> 18* | 16 | 10 f_0(14, 23) -> 10* f_0(14, 22) -> 10* f_0(14, 21) -> 18* | 16 | 10 f_0(14, 20) -> 18* | 16 | 10 f_0(14, 19) -> 18* | 16 | 10 f_0(14, 18) -> 10* f_0(14, 17) -> 18* | 16 | 10 f_0(14, 16) -> 10* f_0(14, 15) -> 16* f_0(14, 14) -> 10* f_0(14, 12) -> 16* f_0(14, 10) -> 10* f_0(14, 9) -> 12* f_0(12, 25) -> 10* f_0(12, 24) -> 10* f_0(12, 23) -> 10* f_0(12, 22) -> 10* f_0(12, 21) -> 10* f_0(12, 20) -> 10* f_0(12, 19) -> 10* f_0(12, 18) -> 10* f_0(12, 17) -> 10* f_0(12, 16) -> 10* f_0(12, 15) -> 10* f_0(12, 14) -> 10* f_0(12, 12) -> 10* f_0(12, 10) -> 10* f_0(12, 9) -> 19* | 17 | 14 | 12 | 10 f_0(10, 25) -> 10* f_0(10, 24) -> 10* f_0(10, 23) -> 10* f_0(10, 22) -> 10* f_0(10, 21) -> 10* f_0(10, 20) -> 10* f_0(10, 19) -> 10* f_0(10, 18) -> 10* f_0(10, 17) -> 10* f_0(10, 16) -> 10* f_0(10, 15) -> 10* f_0(10, 14) -> 10* f_0(10, 12) -> 10* f_0(10, 10) -> 10* f_0(10, 9) -> 24* | 20 | 18 | 16 | 12 f_0(9, 22) -> 14* f_0(9, 19) -> 14* f_0(9, 17) -> 14* f_0(9, 15) -> 14* f_0(9, 14) -> 14* f_0(9, 12) -> 14* f_0(9, 10) -> 14*} Strict: {f#(y, f(x, f(a(), x))) -> f#(a(), y)} EDG: {(f#(y, f(x, f(a(), x))) -> f#(a(), y), f#(y, f(x, f(a(), x))) -> f#(a(), y))} SCCS (1): Scc: {f#(y, f(x, f(a(), x))) -> f#(a(), y)} SCC (1): Strict: {f#(y, f(x, f(a(), x))) -> f#(a(), y)} Weak: { f(x, f(x, y)) -> f(f(f(x, a()), a()), a()), f(y, f(x, f(a(), x))) -> f(f(f(a(), x), f(x, a())), f(a(), y))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1) = x0 + 1, [a] = 0, [f#](x0, x1) = x0 + x1 + 1 Strict: f#(y, f(x, f(a(), x))) -> f#(a(), y) 2 + 1x + 1y >= 1 + 1y Weak: Qed