SUCCESS
20.85 (total time)

COMPLETED TRS
i3(i3(i3(x))) -> i3(x)
i3(a3) -> a3
i3(a2) -> a3
i3(a1) -> a3
i3(f(x, y)) -> f(i3(y), i3(x))
i2(x) -> f(i3(x), a2)
i1(x) -> f(i3(x), a1)
f(i3(i3(x)), y) -> f(x, y)
f(i3(x), f(x, y)) -> y
f(a3, x) -> x
f(a2, x) -> x
f(a1, x) -> x
f(f(x, y), z) -> f(x, f(y, z))
f(x, i3(x)) -> a3
f(x, a3) -> i3(i3(x))
f(x, f(i3(x), y)) -> y