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) Region(Rc1) NoExitCavity(Ta1,Tb1,Hc1,HPlace(Ob1)) P(Place(Ta1,Ox1),Rc1) equal(Rc1,Slice(Ta1,Hc1)) Lt(Ta1,Tb1) not(equal(Ox1,Ob1)) forall([U,V,W], implies( and( Object(W), Lt(U,V)), Continuous(U,V,HPlace(W)))) forall([U,V], implies( and( Time(U), Object(V)), equal(Place(U,V),Slice(U,HPlace(V))))) forall([U,V,W], implies( and( Object(U), Object(V), Time(W), not(equal(U,V))), DR(Place(W,U),Place(W,V)))) forall([U,V], equiv( DR(U,V), and( Region(U), Region(V), not(O(U,V))))) forall([U,V,W,X,Y], implies( and( NoExitCavity(U,V,W,X), Continuous(U,V,Y), P(Slice(U,Y),Slice(U,W)), not(P(Slice(V,Y),Slice(V,W)))), exists([Z], and( Lt(U,Z), Lt(Z,V), O(Slice(Z,Y),Slice(Z,X)))))) Conjectures: P(Slice(Tb1,HPlace(Ox1)),Slice(Tb1,Hc1))