formulas(sos).

% Logical Axiom: Ex1At(A,x,d) is rigid
all x (Object(x) -> ((exists d (Point(d) & Ex1At(A,x,d))) -> (all d (Point(d) -> Ex1At(A,x,d))))). 

% Logical Axiom: EncAt(x,F,d) is rigid
all x all F ((Object(x) & Property(F)) -> ((exists d (Point(d) & EncAt(x,F,d))) -> (all d (Point(d) -> EncAt(x,F,d))))).

% Definition: WorldAt(x,d)
all x all d ((Object(x) & Point(d)) -> (WorldAt(x,d) <-> (SituationAt(x,d) & (exists d2 (Point(d2) & (all p (Proposition(p) -> (TrueInAt(p,x,d2) <-> True(p,d2))))))))).

% Definition: TrueInAt(p,x,d)
all p all x all d ((Object(x) & Proposition(p) & Point(d)) -> (TrueInAt(p,x,d) <-> EncpAt(x,p,d))).

% Definition: SituationAt(x,d)
all x all d ((Object(x) & Point(d)) -> (SituationAt(x,d) <-> (Ex1At(A,x,d) & (all F (Property(F) -> (EncAt(x,F,d) -> (exists p (Proposition(p) & F=VAC(p))))))))).

% Definition: EncpAt(x,p,d)
all x all p all d ((Object(x) & Proposition(p) & Point(d)) -> (EncpAt(x,p,d) <-> (exists F (Property(F) & F=VAC(p) & EncAt(x,F,d))))).

end_of_list.

formulas(goals).

% Logical Theorem (Lemma 1): WorldAt(x,d) is rigid.
all x (Object(x) -> ((exists d (Point(d) & WorldAt(x,d))) -> (all d (Point(d) -> WorldAt(x,d))))).

end_of_list.
