Family Example (Contradiction)

Input:

  set(hyper_res).
  assign(stats_level,1).

  list(usable).
    Parent(anne,beth).
    Parent(anne,ken).
    Parent(jim,beth).
    Parent(jim,ken).
    Female(anne).
    Female(beth).
    Male(jim).
    Male(ken).
  end_of_list.

  list(sos).  
    -Parent(x,y) | -Female(x) | Mother(x,y).
    -Parent(x,y) | -Female(y) | Daughter(y,x).
    -Daughter(beth,anne).
  end_of_list.

Output:

  ---------------- PROOF ----------------

  1 [] Parent(anne,beth).
  6 [] Female(beth).
  10 [] -Parent(x,y)| -Female(y)|Daughter(y,x).
  11 [] -Daughter(beth,anne).
  15 [hyper,10,1,6] Daughter(beth,anne).
  16 [binary,15.1,11.1] $F.

  ------------ end of proof -------------