dragon_exercise.in

%------------------------------------------
%  H(x)   :=  "x is happy"
%  C(x,y) :=  "x is a child of y"
%  F(x)   :=  "x can fly"
%  G(x)   :=  "x is green"
%------------------------------------------

formulas(sos).

  % every dragon is happy if all its children can fly.
  %(all x (all y (C(y,x) -> F(y)) -> H(x))).
  C(f1(x),x) | H(x).
  -F(f1(x)) | H(x).
 
  % green dragons can fly.
  %(all x (G(x) -> F(x))).
  -G(x) | F(x).

  % a dragon is green if it is a child of at least one green dragon.
  %(all x ((exists y (G(y) & C(x,y))) -> G(x))).
  -G(y) | -C(x,y) | G(x).

  % negated goal in clausal form
  -H(c1).
  G(c1).

end_of_list.

formulas(goals).

  % all green dragons are happy.
  %(all x (G(x) -> H(x))).
  
end_of_list.