gt and succ are abbreviations for is-greater-than and is-a-successor-of.
The negation of the query (omitting the universal quantifier) is
0. ~gt(5,2)
Assuming that the sentences of the knowledge base are numbered in order beginning with 1, then
Unifying 0 and 1 by the unifying substitution {5/x, 2/z}, we get
4. ~gt(5,y) ∨ ~gt(y,2)
Unifying 4 and 2 by the unifying substitution {y/a, 2/b}, we get
5. ~gt(5,y) ∨ ~succ(y,2)
Unifying 5 and 1 by the unifying substitution {5/x, y/z}, we get
6. ~gt(5,y) ∨ ~gt(y,y) ∨ ~succ(y,2)
But now, since the middle disjunct is in the knowledge base, we cannot hope to derive a contradiction from this clause, regardless of whatever other clauses might be in the knowledge base.
(∃x) surname(chuck,x) ∧ surname(bea,x)
surname(phil,patel)surname(anne, chang)
phil is replaced by chuck. Would we still be able to find bea's surname? Why or why not?
surname(X,N) :- surname(Y,N), fatherOf(Y,X), not(wife(X)).
surname(chuck,N).
fatherOf(phil,anne) is added to the corrected Prolog facts and rules of part 1 above, Prolog will report in response to the query surname(anne,X). that Anne has the same surname as Phil. However if not(wife(X)) is replaced in the first rule by nonwife(anne) (and the translations of clauses 2 and 8 of KB use this nonwife predicate), then Prolog will not report this. Which answer is most appropriate?