formulas(sos).
all p (Proposition(p)->Proposition(NEG(p))).
all d all p (Point(d)&Proposition(p)-> (True(NEG(p),d)<-> -True(p,d))).
all x (Situation(x)->Object(x)).
all x (Object(x)-> (Possible(x)<->Situation(x)& (exists y (Point(y)& (all p (Proposition(p)-> (TrueIn(p,x)->True(p,y)))))))).
all x (Object(x)-> (Consistent(x)<->Situation(x)& -(exists p (Proposition(p)&TrueIn(p,x)&TrueIn(NEG(p),x))))).
end_of_list.

formulas(goals).
all x (Possible(x)&Situation(x)->Consistent(x)).
end_of_list.
