formulas(sos). Point(W). all p (Proposition(p)->Proposition(NEG(p))). all d all p (Point(d)&Proposition(p)-> (True(NEG(p),d)<-> -True(p,d))). 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). all x (Situation(x)&Actual(x)-> -(exists p (Proposition(p)&TrueIn(p,x)&TrueIn(NEG(p),x)))). end_of_list.