(VAR x y z)
(RULES
f(f(x, y), z) -> f(x, f(y, z))
f(a1, y) -> y
f(a2, y) -> y
f(a3, y) -> y
f(a4, y) -> y
f(a5, y) -> y
f(a6, y) -> y
f(a7, y) -> y
f(a8, y) -> y
f(a9, y) -> y
f(a10, y) -> y
f(a11, y) -> y
f(a12, y) -> y
f(a13, y) -> y
f(a14, y) -> y
f(a15, y) -> y
f(a16, y) -> y
f(a17, y) -> y
f(a18, y) -> y
f(a19, y) -> y
f(a20, y) -> y
f(a21, y) -> y
f(a22, y) -> y
f(a23, y) -> y
f(a24, y) -> y
f(x, i1(x)) -> a1
f(x, i2(x)) -> a2
f(x, i3(x)) -> a3
f(x, i4(x)) -> a4
f(x, i5(x)) -> a5
f(x, i6(x)) -> a6
f(x, i7(x)) -> a7
f(x, i8(x)) -> a8
f(x, i9(x)) -> a9
f(x, i10(x)) -> a10
f(x, i11(x)) -> a11
f(x, i12(x)) -> a12
f(x, i13(x)) -> a13
f(x, i14(x)) -> a14
f(x, i15(x)) -> a15
f(x, i16(x)) -> a16
f(x, i17(x)) -> a17
f(x, i18(x)) -> a18
f(x, i19(x)) -> a19
f(x, i20(x)) -> a20
f(x, i21(x)) -> a21
f(x, i22(x)) -> a22
f(x, i23(x)) -> a23
f(x, i24(x)) -> a24
)
(COMMENT Example form Christian 93: Flatterms ...)