formulas(assumptions).
  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).

  inhabitant(a) & inhabitant(b) & inhabitant(c).
  a != b  & b !=c  & c !=a.                         
  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.

formulas(goals).
 % knave(a) & knight(b) & knave(c). 
 % knave(a).
 % knight(b).
  knave(c). 
end_of_list.
