formulas(sos).
Proposition(L).
-True(L,W).
all x (Object(x) -> (Actual(x) <-> (Situation(x) & (all p (Proposition(p)-> (TrueIn(p,x)->True(p,W))))))).
all x (Actual(x) -> Object(x)).
end_of_list.

formulas(goals).
exists p (Proposition(p) & all x (Situation(x)&Actual(x)-> -TrueIn(p,x))).
end_of_list.