Axioms: forall([U,V], implies( Lt(U,V), and( Time(U), Time(V)))) forall([U,V], implies( Leq(U,V), and( Time(U), Time(V)))) forall([U,V], implies( Ordered(U,V), and( Time(U), Time(V)))) forall([U,V,W], implies( Leq3(U,V,W), and( Time(U), Time(V), Time(W)))) forall([U,V], implies( or( P(U,V), O(U,V), EC(U,V), DR(U,V)), and( Region(U), Region(V)))) forall([U,V], implies( and( Region(U), Region(V)), Region(RUnion(U,V)))) forall([U,V], implies( or( Cavity(U,V), Outside(U,V)), and( Region(U), Region(V)))) forall([U], implies( Object(U), ObjectSet(Singleton(U)))) forall([U,V], implies( and( Time(U), Object(V)), Region(Place(U,V)))) forall([U,V,W], implies( OSPlace(U,V,W), and( Time(U), ObjectSet(V), Region(W)))) forall([U,V,W], implies( ClosedContainer(U,V,W), and( Time(U), ObjectSet(V), Region(W)))) forall([U,V,W], implies( CContained(U,V,W), and( Time(U), Object(V), ObjectSet(W)))) forall([U,V], implies( and( Time(U), History(V)), Region(Slice(U,V)))) forall([U], implies( Object(U), History(HPlace(U)))) forall([U], implies( RigidObject(U), Object(U))) forall([U], implies( RigidHistory(U), History(U))) RigidObject(Ob1) CContained(Ta1,Ox1,Singleton(Ob1)) Lt(Ta1,Tb1) not(equal(Ox1,Ob1)) forall([U], implies( RigidObject(U), RigidHistory(HPlace(U)))) forall([U,V,W], equiv( CContained(U,V,W), exists([X], and( ClosedContainer(U,W,X), Object(V), P(Place(U,V),X))))) forall([U,V,W], equiv( ClosedContainer(U,V,W), exists([X], and( OSPlace(U,V,X), Time(U), ObjectSet(V), Cavity(W,X))))) forall([U,V], implies( and( Time(U), Object(V)), equal(Place(U,V),Slice(U,HPlace(V))))) forall([U,V,W], implies( and( Time(U), Object(V)), equiv( OSPlace(U,Singleton(V),W), equal(Place(U,V),W)))) Conjectures: exists([U], and( Cavity(U,Slice(Ta1,HPlace(Ob1))), P(Place(Ta1,Ox1),U)))