(A1) "Every house is owned by a manager or a NBA-player."
(A2) "Every manager owns at least one house."
(A3) "All house-owners are rich."
|-
(A) " All managers are rich."
(B) "Some NBA-player are rich."
 
Representation of (A1), (A2), (A3), ~(A), and ~(B) in predicate calculus: 
    
(A1) Vh Vo ((house(h) ^ owns(o,h)) --> (nba(o) v manager(o) ))
 
(A2) Vm (manager(m) --> ]h (house(h) ^ owns(m,h) ))
 
(A3) VxVy ((owns(x,y) ^ house(y) ) --> rich(x) )
 
~(A) ~Vz (manager(z) --> rich(z) )
 
~(B) ~]u (nba(u) ^ rich(u))
  
 
Transformation of the above expressions to clause-form:
 
notations:
  a) Capital letters represent Skolem functions
  b) Identifiers beginning with $ represent variables
  c) All other identifiers represent constants
 
(C1) ~house($h) v ~owns($o,$h) v nba($o) v manager($o)
 
(C2a) ~manager($m) v house(F($m))
 
(C2b) ~manager($m) v owns(m,F($m))

(C3)  ~owns($x,$y) v ~house($y) v rich($x)

(C4a) manager(Z) 

(C4b) ~rich(Z)

(C5)  ~nba($u) v ~rich($u)


Try to prove: a) A1,A2,A3 |- A

(A6) house(F(Z))         from (C4a) and (C2a)
(A7) owns(Z,F(Z))         "   (C4a) and (C2b)
(A8) ~owns(Z,$y) v ~house($y)  from (C4b) and (C3)
(A9) ~house(F(Z))        from (A8) and (A9)
(A10) empty clause       from (A6) and (A9)
that is, a prove for A1,A2,A3 |- A has been found

Try to prove: b) A1,A2.A3 |- B

(B6) ~rich($u) v manager($u) v ~owns($u,$h) v ~house($h)   from (C5) and (C1)
(B7) manager($u) v ~owns($u,$h) v ~house($h) v ~owns($u,$y) v ~house($y)
     from (B7) and (C3).
     Assuming $h is bound to $y, (B7) can be simplified yielding:
(B7') manager($u) v ~owns($u,$y) v ~house($y)
     that is, "every house owner is a manager". However, although further
     resolution steps are applicable, the above formula cannot be  fal-
     sified; that is A1,A2,A3 |- B cannot be proved. If "all house owners
     are managers" holds A1,A2,A3 are true, although B is not true because
     in this case no house is owned by an NBA-player. 
     
(A1) "Some dolphins eat fish."
(A2) "No vegetarian eats fish."
(A3) "Every dolphin is intelligent."
(A4) "The dolphin 'Flipper' is a vegetarian."
 
(A) "Some intelligent beings are vegetarians."
(B) "Flipper is intelligent."
(C) "All fish eaters are intelligent."
(D) "Some dolphins are no vegetarians"
       
(A1) ]x (dolphin(x) ^ eatfish(x) )
(A2) ~]v (vegetarian(v) ^ eatfish(v) )
(A3) Vd (dolphin(d) --> intelligent(d) )
(A4) dolphin(Flipper) ^ vegetarian(Flipper)
 
(~A) ~]i (intelligent(i) ^ vegetarian(i))
(~B) ~intelligent(Flipper)
(~C) ~Ve (eatfish(e) --> intelligent(e) )
(~D) ~]a (dolphin(a) ^ ~vegetarian(a))

(1a) dolphin(D)
(1b) eatfish(D)
(2) ~vegetarian($v) v ~eatfish($v) 
(3) ~dolphin($d) v intelligent($d)
(4a) dolphin(Flipper)
(4b) vegetarian(Flipper)

(5) ~intelligent($i) v ~vegetarian($i)
(6) ~intelligent(Flipper)
(7a) eatfish(E)
(7b) ~intelligent(E)
(8)  ~dolphin($a) v vegetarian($a)

            A1,A2,A3 |- A 
(x1) ~dolphin($d) v ~vegetarian($d) from (5) and (3)
(x2) ~vegetarian(Flipper)  from (x1) and (4a)
(x3) empty clause          from (x2) and (4b)

           A1,A2,A3 |- B
(y1) ~dolphin(Flipper)  from (6) and (3)
(y2) empty clause       from (y1) and (4a)

          A1,A2,A3 |- C
(z1) ~vegetarian(E)  from (7a) and (2)
(z2) ~dolphin(E)     from (7b) and (3)
     ... (no proof found).
         
         A1,A2,A3 |- D
(w1) ~eatfish($v) v ~dolphin($v) from (2) and (8)
(w2) ~eatfish(D)                 from (w1) and (1a)
(w3) empty clause                from (w2) and (1b)

(A1) "If someone is not rich, then he is not married."
(A2) "Everyone, who is rich, is not married."
(A3) "If x is married to y, then y is married to x."
(A)  "No rich person is married to a poor(non rich) person."

(A1) Vp (~rich(p) --> ]m married(p,m) )
(A2) Vz (rich(z) --> ~]w married(z,w) )
(A3) VuVv (married(u,v) --> married(v,u) )
(~A)  ~~ ]x]y (rich(x) ^ ~rich(y) ^ married(x,y) )
 
(1) rich($p) v married($p,F($p))
(2) ~rich($z) v ~married($z,$w)
(3) ~married($u,$v) v married($v,$u)
(4a) rich(X)
(4b) ~rich(Y)
(4c) married(X,Y)
 
          proof: A1,A2,A3 |- A
 
(q1) ~married(X,$w) from (4a) and (2)
(q2) married(Y,F(Y))  from (4b) and (1)
(q3) ~rich(X)         from (4c) and (2)
(q4) empty clause     from (q3) and (4a)
remark: Resolving (q1) and (4c) also generates the empty clause.


   Tranforming predicate calculus to clauses 

1) Replace --> using:  (P --> Q) = (~P v Q)
2) Move ~ inside using: 1) ~Vx Px = ]x ~Px 
                        2) ~]x Qx = Vx ~Qx
                        3) ~(P ^ Q) = ~P v ~Q
                        4) ~(P v Q) = ~P ^ ~Q
3) Standardize variables - rename variables that are used more than once
   by quantifiers.
4) remove ]; replace existential quantified variables by Skolem functions.
   Use different functions for different variables; use capital letters for
   function names; the arity of the Skolem function is determined by the 
   number of V-quantifiers enclosing the ]-quantifier.
5+6) remove V; replace all quantified variables by match variables.
7) Produce CNF using the Distributive law for v and ^  moving v inside and 
   ^ outside, for example:
   (P ^ Q) v (R ^ S) = (P v R) ^ (P v S) ^ (Q v R) ^ (Q v S)
8) Remove ^; produce clauses.
9) Rename match variables that occur more than once in clauses.