Knowledge Representation and Automated Reasoning with 1st Order Logic

Translate the following problem into 1st order logic:

Every Italian has an Italian lover. The father of every Italian is very protective of that person. Angelo and Antonio are Italians. If Antonio's lover is Angelo, then there is someone who is protective of Angelo.

∀X ( italian(X) => ∃Y (italian(Y) & lover(X,Y)) )
∀X ( italian(X) => protective_of(X,father_of(X)) )
italian(angelo)
italian(antonio)
lover(antonio,angelo) => ∃Y protective_of(angelo,Y)

Convert the following to CNF:

    ∃X ( ∃Y (p(X,Y) & q(Y)) => ∃Z (p(Z,X) & q(Z)) )

    ∃X ( ∃Y (p(X,Y) & q(Y)) => ∃Z (p(Z,X) & q(Z)) )
    ∃X ( ~ ∃Y (p(X,Y) & q(Y)) | ∃Z (p(Z,X) & q(Z)) )
    ∃X ( ∀Y (~p(X,Y) | ~q(Y)) | ∃Z (p(Z,X) & q(Z)) )
    ∃X ∀Y ∃Z ( (~p(X,Y) | ~q(Y)) | (p(Z,X) & q(Z)) )
    ( (~p(x,Y) | ~q(Y)) | (p(z(Y),x) & q(z(Y))) )

    ~p(x,Y) | ~q(Y) | p(z(Y),x)
    ~p(x,Y) | ~q(Y) | q(z(Y))

List all the resolvants of the following two clauses:

    p(X,f(Y),Z) | p(T,T,g(cat)) | r(X,T) | ~s(Z,T)
    ~p(f(dog),S,g(W) | s(big,rat) | ~s(small,hamster) 

    1.1 + 2.1 = p(T,T,g(cat)) | r(f(dog),T) | ~s(g(W),T) | s(big,rat) | ~s(small,hamster)
    1.2 + 2.1 = p(X,f(Y),Z) | r(X,f(dog)) | ~s(Z,f(dog)) | s(big,rat) | ~s(small,hamster)
    1.1,1.2 + 2.1 = r(f(dog),f(dog)) | ~s(Z,f(dog)) | s(big,rat) | ~s(small,hamster)
    1.4 + 2.2 = p(X,f(Y),big) | p(rat,rat,g(cat)) | r(X,rat) | ~p(f(dog),S,g(W)) | ~s(small,hamster)

Use resolution to derive the empty clause from the set

    S = { p(X) | p(f(Y)) | q(Y,b),
         t(S) | ~p(f(a)) | r(S),
         ~r(T) | ~p(T),
         ~q(a,b) | p(f(Z)),
         ~t(f(U)) }

    1 + 4 = 6 = p(X) | p(f(a)) | p(f(Z))
    2 + 3 = 7 = t(S) | ~p(f(a)) | ~p(S)
    7 + 5 = 8 = ~p(f(a)) | ~p(f(U))
    6 + 8 = 9 = false