ARITH_RULE `(a * x + b * y + a * y) EXP 3 + (b * x) EXP 3 + (a * x + b * y + b * x) EXP 3 + (a * y) EXP 3 = (a * x + a * y + b * x) EXP 3 + (b * y) EXP 3 + (a * y + b * y + b * x) EXP 3 + (a * x) EXP 3`;;