In our proofs we mostly omit sortal predicates such as Time(t), Region(r) and so on. Scenario 1: Qualitative prediction. If Ob1 is a rigid object and it is a closed container container object Ox1, then Ox1 remains inside Ob1. Given: C.1.A.A: RigidObject(Ob1). C.1.A.B: CContained(Ta1,Ox1,Singleton(Ob1)). C.1.A.C: Lt(Ta1,Tb1). C.1.A.D: Ob1 \$\neq\$ Ox1. Infer: CContained(Tb1,Ox1,Singleton(Ob1)). Proof of Scenario 1: 1.1. RigidHistory(HPlace(Ob1)) C.1.A.A + R.G.A.A 1.2. ClosedContainer(Ta1,Singleton(Ob1),Rc1) C.1.A.B + O.C.D.A 1.3. P(Place(Ta1,Ox1),Rc1). C.1.A.B + O.C.D.A. 1.4. OSPlace(Ta1,Singleton(Ob1), Rs1). 1.2 + O.R.D.A. 1.5. Cavity(Rc1,Rs1). 1.2 + O.R.D.A. 1.6. Slice(Ta1,HPlace(Ob1)) = Place(Ta1,Ob1). H.I.A.B. 1.7. Rs1 = Place(Ta1,Ob1). O.T.A.F + 1.2 1.8. Rs1 = Slice(Ta1,HPlace(Ob1)). 1.6 + 1.7. 1.9. Cavity(Rc1,Slice(Ta1,HPlace(Ob1))). 1.5 + 1.8. 1.10 Intentionally omitted 1.11. PersistentCavity(Ta1,Tb1,Hc1,HPlace(Ob1)). 1.1 + 1.9 + C.1.A.C + + R.G.A.B 1.12. Rc1 = Slice(Ta1,Hc1). 1.1 + 1.9 + C.1.A.C + R.G.A.B 1.13. NoExitCavity(Ta1,Tb1,Hc1,HPlace(Ob1)). 1.11 + H.C.D.A. 1.14. Continuous(Ta1,Tb1,HPlace(Ox1)). H.I.A.A + C.1.A.C 1.15. Slice(Ta1,HPlace(Ox1)) = Place(Ta1,Ox1). H.I.A.B. 1.16. P(Slice(Ta1,HPlace(Ox1)),Rc1). 1.3 + 1.15. 1.17. P(Slice(Ta1,HPlace(Ox1)),Slice(Ta1,Hc1)). 1.16 + 1.12. 1.18. forall(t) DR(Place(t,Ob1),Place(t,Ox1)). C.1.A.D + O.T.A.B 1.19. forall(t) not O(Place(t,Ob1),Place(t,Ox1)). 1.18 + S.B.D.B 1.20. P(Slice(Tb1,HPlace(Ox1)),Slice(Tb1,Hc1)) 1.18 + 1.17 + 1.14 + 1.13 + contrapositive of H.C.A.B. 1.21. Leq3(Ta1,Tb1,Tb1). T.I.D.C, T.I.D.A, C.1.A.C 1.22. Cavity(Slice(Tb1,Hc1),Slice(Tb1,HPlace(Ob1))). 1.21 + 1.13 + H.C.A.A 1.23. Slice(Tb1,HPlace(Ob1)) = Place(Tb1,Ob1). H.I.A.B. 1.24. OSPlace(Tb1,Singleton(Ob1),Place(Tb1,Ob1)). O.T.A.F. 1.25. ClosedContainer(Tb1,Singleton(Ob1),Slice(Tb1,Hcl)). O.R.D.A + 1.22 + 1.23 + 1.24 1.26. Slice(Tb1,HPlace(Ox1)) = Place(Tb1,Ox1). H.I.A.B. 1.27. P(Place(Tb1,Ox1),Slice(Tb1,Hc1)). 1.20 + 1.26. 1.28. CContained(Tb1,Ox1,Singleton(Ob1)). 1.25 + 1.27 + O.C.D.A