It is better for FOL problems to have variables that are not X, Y (because of handwriting)