This question involves formalizing the properties of mathematical groups in FOL. Recall that a set is considered to be a group relative to a binary function f and an object e if and only if f is associative;

e is an identity element for f, that is for any x, f(e, x) = f(x, e) = x; and

every element has an inverse, that is, for any x, there is an i such that f(x, i) = f(i, x) = e.

(a) Formalize these as sentences of FOL with two nonlogical symbols, a function symbol f, and a constant symbol e, and show using interpretations that the sentences logically entail the following property of groups: For every x and y, there is a z such that f(x, z) = y.

(b) Repeat the entailment proof using Resolution. To do so, you will need to treat equality as a predicate and add to the sentences of part (a) some or all of the axioms of equality (Section 4.2.4 in KRR): reflexibility, symmetry, transitivity. In addition, add the axiom of the substitution of equals for equals, that is for every x, y and z, if x = y, then f(x, z) = f(y, z) and f(z, x) = f(z, y).