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,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,V,W,X], equiv( PersistentCavity(U,V,W,X), and( NoExitCavity(U,V,W,X), NoEntranceCavity(U,V,W,X)))) forall([U], implies( RigidObject(U), Object(U))) forall([U], implies( RigidHistory(U), History(U))) RigidHistory(HPlace(Ob1)) Cavity(Rc1,Slice(Ta1,HPlace(Ob1))) forall([U,V,W,X], implies( PersistentCavity(U,V,W,X), NoExitCavity(U,V,W,X))) Lt(Ta1,Tb1) forall([U,V,W,X], implies( and( RigidHistory(U), Cavity(X,Slice(V,U)), Lt(V,W)), exists([Y], and( RigidHistory(Y), PersistentCavity(V,W,Y,U), equal(X,Slice(V,Y)))))) Conjectures: exists([U], and( equal(Rc1,Slice(Ta1,U)), NoExitCavity(Ta1,Tb1,U,HPlace(Ob1))))