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