SUCCESS 4.21 (total time) COMPLETED TRS i2(i2(x)) -> f(x, a2) i2(a2) -> a2 i2(a1) -> a2 i2(f(x, y)) -> f(i2(y), i2(x)) i1(x) -> f(i2(x), a1) f(i2(x), a2) -> i2(x) f(i2(x), f(x, y)) -> y f(a2, x) -> x f(a1, x) -> x f(f(x, y), z) -> f(x, f(y, z)) f(x, i2(x)) -> a2 f(x, f(i2(x), y)) -> y