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