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

formulas(island_of_truth).
  all x (inhabitant(x) -> knight(x) | knave(x)). 
  all x ((knight(x) -> -knave(x)) & (knave(x) -> -knight(x))).
  knight(x) ->  m(x).
  knave(x)  -> -m(x).
end_of_list.

formulas(puzzle).  
  inhabitant(a) & inhabitant(b) & inhabitant(c).
  a=0 & b=1 & c=2.                         %remove isomorphisms
  m(a) <->  (knave(a) & knave(b) & knave(c)). 
  m(b) <-> (knight(a) & knave(b) & knave(c)) |
           (knave(a) & knight(b) & knave(c)) |
           (knave(a) & knave(b) & knight(c)).
end_of_list.
