set(auto2).
clear(fof_reduction).

formulas(usable).

% 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: 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))))).

% 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))).

end_of_list.

formulas(sos).
% Denial Corollary to L2 - Rigidity of TrueIn
-(all x all p ((Object(x) & Proposition(p)) -> ((exists d (Point(d) & TrueInAt(p,x,d))) -> (all d (Point(d) -> TrueInAt(p,x,d)))))).
end_of_list.

