I tried my first simple proof in first-order/predicate logic with FindEquationalProof (12.3) and the following example:

Axiom: Everyone has a father

Axiom: A grandfather is the father of a father

Hypothesis: Everyone has a grandfather

FindEquationalProof finds a proof within 22 steps, but some intermediate steps seem to be logically not correct: In the EquationalizedHypothesis the Exists-quantifier is substituted by a Skolem-function f1. But in the EquationalAxiom5 from the same form of Axiom2, the Exists-quantifier is substituted only by father [x3,x1] without a Skolem-function. This finally leads to strange propositions like: father[x0,x0]==grandfather[x3,x1] which are logically invalid.

I guess this proof is not really a valid proof. Would someone help me with some hints, what is going wrong here ? Thank you for any comments

Regards Uwe

proof = FindEquationalProof[
     ForAll[x, 
      Exists[z, 
       grandfather[z, x]]], {ForAll[{x, y, 
        z}, (father[z, y] && father[y, x] \[Implies] grandfather[z, x])],
       ForAll[x, Exists[z, father[z, x]]]}]