From Coursera's Introduction to Logic, Notes Chapter 9: Equality:
-----------------------------------------------------------------

From Section 9.4:
-----------------

"Now, let's look at a couple of examples that illustrate how equational reasoning
interacts with relational reasoning. We know that Pat is the father of Quincy, 
and we know that fathers are older than their children. Our job is to prove that
Pat is older than Quincy.

Our proof is shown below. As usual, we start with our premises. The father of 
Quincy is Pat, and fathers are older than their children. Next, we use Universal
Elimination to instantiate our quantified sentence. The father of Quincy is 
older than Quincy. Next we use Equality Elimination to replace father(quincy) 
with pat and thereby derive the conclusion that Pat is older than Quincy.

1.    father(pat) = quincy    Premise 
2.    Ax.older(father(x),x)    Premise 
3.    older(father(pat),pat)    Universal Elimination 2 
4.    older(quincy,pat)    Equality Elimination 3, 1"

---

Note the mistake in the above: father(pat) = quincy is mixed up; it should be 
father(quincy) = pat. I ascribe the confusion to the impedance mismatch between 
the subject-predicate syntax of natural language and the function-argument 
syntax of relational logic.

Here's how logicagent (subbot.org/logicagent) handles this proof:

---
C:\logicagent>ruby logicbot.rb
Hello
I have loaded C:/logicagent/logicagent-api.yaml.
C:/logicagent/graph.yaml loaded.

> reset graph
Okay, I have reset the graph.

> The father of Quincy is Pat.
Okay, The father of Quincy is Pat.

> Fathers are older than their children.
Okay, Fathers are older than their children.

> Fathers includes the father of Quincy
Okay, Fathers includes the father of Quincy.

> their children includes Quincy
Okay, their children includes Quincy.

> is Pat older than Quincy?
I have no knowledge that Pat is older than Quincy.

> Pat is the father of Quincy.
Okay, Pat is the father of Quincy.

> is Pat older than Quincy?
Yes, Pat is older than Quincy.

>

---

Note that I had to say explicitly: "Pat is the father of Quincy" before the 
proof worked. This requirement is because "is" is not symmetric in my system. 
"=" is symmetric, so I could do the proof as follows:

---

> reset graph
Okay, I have reset the graph.

> The father of Quincy = Pat
Okay, The father of Quincy = Pat.

> Fathers are older than their children
Okay, Fathers are older than their children.

> Fathers include the father of Quincy
Okay, Fathers includes the father of Quincy.

> their children includes Quincy
Okay, their children includes Quincy.

> is Pat older than Quincy?
Yes, Pat is older than Quincy.

>