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