set(auto2). formulas(sos). % axioms for theorem 4 all x all y ((Object(x) & Object(y)) -> (PartPH(x,y) <-> (exists F (Property(F) & IsTheFormOf(y,F) & Enc(x,F))))). end_of_list.