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,V,W], implies( or( Continuous(U,V,W), WeaklyContinuous(U,V,W)), and( Time(U), Time(V), History(W)))) forall([U], implies( Object(U), History(HPlace(U)))) forall([U,V,W], implies( Constant(U,V,W), and( Time(U), Time(V), History(W)))) forall([U,V,W,X], implies( or( NoExitCavity(U,V,W,X), NoEntranceCavity(U,V,W,X), PersistentCavity(U,V,W,X)), and( Time(U), Time(V), History(W), History(X)))) forall([U], implies( RigidObject(U), Object(U))) forall([U], implies( RigidHistory(U), History(U))) Object(Ob1) Object(Ox1) Time(Ta1) Time(Tb1) History(Hc1) P(Slice(Tb1,HPlace(Ox1)),Slice(Tb1,Hc1)) NoExitCavity(Ta1,Tb1,Hc1,HPlace(Ob1)) Lt(Ta1,Tb1) forall([U,V,W,X], implies( NoExitCavity(U,V,W,X), and( Lt(U,V), WeaklyContinuous(U,V,W), forall([Y], implies( Leq3(U,Y,V), Cavity(Slice(Y,W),Slice(Y,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)))) 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], equiv( CContained(U,V,W), exists([X], and( ClosedContainer(U,W,X), Object(V), P(Place(U,V),X))))) forall([U,V], equiv( Leq(U,V), and( Time(U), Time(V), or( Lt(U,V), equal(U,V))))) forall([U,V,W], equiv( Leq3(U,V,W), and( Leq(U,V), Leq(V,W)))) Conjectures: CContained(Tb1,Ox1,Singleton(Ob1))