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