assign(max_models, -1).
assign(domain_size,2).

formulas(minosaminos).
  all x (inhabitant(x) -> mino(x) | amino(x)). 
  all x (mino(x) -> -amino(x)).  
  mino(x)  ->  m(x).
  amino(x) -> -m(x).
  same_family(x,y) -> mino(x) & mino(y) | amino(x) & amino(y).
  brother(x,y) -> same_family(x,y).
 -brother(x,x).
  same_family(x,x).
end_of_list.

formulas(puzzle).
  inhabitant(Bahman) & inhabitant(Perviz) & (Bahman != Perviz).
  brother(Bahman,Perviz) & brother(Perviz,Bahman).
  m(Bahman) <->  married(Bahman) & married(Perviz). 
  m(Perviz) <-> -married(Perviz). 
end_of_list.
