**Definition 1. Timepoint q is between timepoints p and r iff p is before q and q is before r.**

(defrelation Between (?p ?q ?r) := (and (Before ?p ?q) (Before ?q ?r)))

**Definition 2. Timepoint p is BeforeEq timepoint q iff p is before or equal to q.**

(defrelation BeforeEq (?p ?q) := (and (Point ?p) (Point ?q) (or (Before ?p ?q) (= ?p ?q))))

**Definition 3. Timepoint q is BetweenEq timepoints p and r iff p is before or equal to q, and q is before or equal to r.**

(defrelation BetweenEq (?p ?q ?r) := (and (BeforeEq ?p ?q) (BeforeEq ?q ?r)))

**Definition 4. An object exists-at a timepoint p iff p is BetweenEq its begin and end points.**

(defrelation Exists-at (?x ?p) := (and (Object ?x) (BetweenEq (Beginof ?x) ?p (Endof ?x))))

**Definition 5. An activity is-occurring-at a timepoint p iff p is BetweenEq the activity's begin and end points.
**

(defrelation Is-occurring-at (?a ?p) := (and (Activity ?a) (BetweenEq (Beginof ?a) ?p (Endof ?a))))

**Definition 6. a is a subactivity of b iff every object in a at a timepoint t is also in b at t, and b is occuring at every timepoint that a is.
**

(defrelation Subactivity (?a ?b) := (and (forall (?x ?t) (=> (In ?x ?a ?t) (In ?x ?b ?t)) (forall ?p (=> (Is-occurring-at ?a ?p) (Is-occurring-at ?b ?p)))))

**Definition 7. Activity a immediately precedes activity b iff a's endpoint is b's beginpoint.
**

(defrelation Imm-precedes (?a ?b) := (and (Activity ?a) (Activity ?b) (= (Endof ?a) (Beginof ?b))))

**Axiom 1. The Before relation only holds between
timepoints. **

(=> (Before ?p ?q) (and (Point ?p) (Point ?q)))

**Axiom 2. The Before relation is a total ordering.
**

(=> (and (Point ?p) (Point ?q)) (or (= ?p ?q) (Before ?p ?q) (Before ?q ?p)))

**Axiom 3. The Before relation is irreflexive. **

(not (Before ?p ?p))

**Axiom 4. The Before relation is transitive. **

(=> (and (Before ?p ?q) (Before ?q ?r) (Before ?p ?r))

**Axiom 5: The timepoint inf- is before all other timepoints.
**

(=> (and (Point ?t) (not (= ?t inf-))) (Before inf- ?t))

**Axiom 6. Every other timepoint is before inf+.**

(=> (and (Point ?t) (not (= ?t inf+))) (Before ?t inf+))

**Axiom 7. Given any timepoint t other than inf-, there is a timepoint between inf- and t.**

(=> (and (Point ?t) (not (= ?t inf-))) (exists ?u (Between inf- ?u ?t)))

**Axiom 8. Given any timepoint t other than inf+, there is a timepoint between t and inf+.**

(=> (and (Point ?t) (not (= ?t inf+))) (exists ?u (Between ?t ?u inf+)))

**Axiom 9. Everything is either an activity, object, or timepoint.**

(or (Activity ?x) (Object ?x) (Point ?x))

**Axiom 10. Objects, activities, and timepoints are all distinct kinds of things.**

(and (=> (Activity ?x) (not (or (Object ?x) (Point ?x)))) (=> (Object ?x) (not (Point ?x))))

**Axiom 11. The begin and end of an activity are timepoints.**

(=> (Activity ?a) (and (Point (Beginof ?a)) (Point (Endof ?a))))

**Axiom 12. The begin point of every activity is before or equal to its end point.**

(=> (or (Activity ?x) (Object ?x)) (BeforeEq (Beginof ?x) (Endof ?x)))

**Axiom 13. The participates-in relation only holds between objects, activities, and timepoints, respectively.**

(=> (In ?x ?a ?t) (and (Object ?x) (Activity ?a) (Point ?t)))

**Axiom 14. An object can participate in an activity only at those timepoints at which both the object exists and the activity is occurring.**

(=> (In ?x ?a ?t) (and (Exists-at ?x ?t) (Is-occurring-at ?a ?t)))

**Axiom 15. Activities that are subactivities of each other (and hence which contain the same objects at the same timepoints and which are occurring at the same timepoints) are identical.**

(=> (and (subactivity ?a ?b) (subactivity ?b ?a)) (= ?a1 ?a2))