Marcus was a man. Marcus was a Pompeian. All Pompeians are Romans. Caesar was a ruler. All Romans are either loyal to Caesar or hated him. Everyone is loyal to someone. People only try to kill rulers they are not loyal to. Marcus tried to kill Caesar.
contains the following statements.
| No | Clause |
| 1 | man(Marcus) |
| 2 | pompeian(Marcus) |
| 3 | "x[pompeian(x)=> roman(x)] |
| 4 | ruler(Caesar) |
| 5 | "x[roman(x) => loyalto(x2,Caesar)  hate(x,Caesar)]
|
| 6 | "x$yloyalto(x,y) |
| 7 | "x"man(x) ruler(y) trykill(x,y)
=>  loyalto(x,y)
|
| 8 | trykill(Marcus,Caesar) |
The are converted to conjunctive normal form as
| No | Clause | Comment |
| 1 | man(Marcus) | |
| 2 | pompeian(Marcus) | |
| 3 | pompeian(x1)
roman(x1) |
|
| 4 | ruler(Caesar) | |
| 5 | roman(x2)
loyalto(x2,Caesar) hate(x2,Caesar)
|
|
| 6 | loyalto(x3,S1(x3)) | Skolem func. |
| 7 | man(x4)
ruler(y1)
trykill(x4,y1) loyalto(x4,y1)
|
|
| 8 | trykill(Marcus,Caesar) |
So we start with the negation that Marcus does not hate Caesar and then refute that claim by looking for conflict in the database (see examples paper). The proof proceeds like:
| Current Clause | Resolve with |
| dbase clause | |
| hate(Marcus,Caesar)
|
5 |
| ¯ | |
| roman(Marcus) loyalto(Marcus,Caesar)
|
3 |
| ¯ | |
| ¯ | |
| CONFLICT |