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))))