Ernest Davis
Below are links to formal proofs of the five sample inferences in section 6 of the paper Commonsense Reasoning about Manipulating Containers . The proofs are stated in a natural deduction format, though steps are combined and compressed. Axiom numbers refer to those in the main paper, though the periods separating fields have been deleted (e.g. definition T.I.D.1 is cited here as TID1).
In our proofs, we mostly omit sortal predicates, such as Time(t), Region(r), and so on. In the proofs of scenarios 4 and 5, we also omit dependence on some basic temporal definitions (e.g. the definitions of Leq and Leq3).