op(300,prefix,~). set(auto2). clear(fof_reduction). formulas(sos). % axioms for theorem 18b all x all p (Object(x)&Proposition(p)-> (Encp(x,p)<-> (exists F (Property(F)&F=VAC(p)&Enc(x,F))))). all x (Object(x)-> (Situation(x)<->Ex1At(A,x,W)& (all F (Property(F)-> (Enc(x,F)-> (exists p (Proposition(p)&F=VAC(p)))))))). all p all x (Object(x)&Proposition(p)-> (TrueIn(p,x)<->Encp(x,p))). all x (Object(x)-> (Actual(x)<->Situation(x)& (all p (Proposition(p)-> (TrueIn(p,x)->True(p,W)))))). all x (Object(x)-> (Maximal1(x)<->Situation(x)& (all p (Proposition(p)->TrueIn(p,x)|TrueIn(~p,x))))). all x (World(x)->Object(x)). all x all y (Ex1At(A,x,W)&Ex1At(A,y,W)-> ((all F (Property(F)-> (Enc(x,F)<->Enc(y,F))))->x=y)). all x (World(x)->Maximal1(x)). Point(W). all p (Proposition(p)->Proposition(~p)). all d all p (Point(d)&Proposition(p)-> (True(~p,d)<-> -True(p,d))). % denial of theorem 18b -(all x all y (World(x)&World(y)&Actual(x)&Actual(y)->x=y)). end_of_list.