(forall (?t1 ?t2)

(if (before ?t1 ?t2)

(and (timepoint ?t1)

(timepoint ?t2))))

(forall (?t1 ?t2)

(if (and (timepoint ?t1)

(timepoint ?t2))

(or (= ?t1 ?t2)

(before ?t1 ?t2)

(before ?t2 ?t1))))

(forall (?t1)

(not (before ?t1 ?t1)))

(forall (?t1 ?t2 ?t3)

(if (and (before ?t1 ?t2)

(before ?t2 ?t3))

(before ?t1 ?t3)))

(forall (?t)

(if (and (timepoint ?t)

(not (= ?t inf-)))

(before inf- ?t)))

(forall (?t)

(if (and (timepoint ?t)

(not (= ?t inf+)))

(before ?t inf+)))

(forall (?t)

(if (and (timepoint ?t)

(not (= ?t inf-)))

(exists (?u)

(between inf- ?u ?t))))

(forall (?t)

(if (and (timepoint ?t)

(not (= ?t inf+)))

(exists (?u)

(between ?t ?u inf+))))

(forall (?x)

(or (activity ?x)

(activity_occurrence ?x)

(timepoint ?x)

(object ?x)))

(forall (?x)

(and (if (activity ?x)

(not (or (activity_occurrence ?x) (object ?x) (timepoint ?x))))

(if (activity_occurrence ?x)

(not (or (object ?x) (timepoint ?x))))

(if (object ?x)

(not (timepoint ?x)))))

(forall (?a ?occ)

(if (occurrence_of ?occ ?a)

(and (activity ?a)

(activity_occurrence ?occ))))

(forall (?occ)

(if (activity_occurrence ?occ)

(exists (?a)

(and (activity ?a)

(occurrence_of ?occ ?a)))))

(forall (?occ ?a1 ?a2)

(if (and (occurrence_of ?occ ?a1)

(occurrence_of ?occ ?a2))

(= ?a1 ?a2)))

(forall (?a ?x)

(if (or (occurrence_of ?x ?a)

(object ?x))

(and (timepoint (beginof ?x))

(timepoint (endof ?x)))))

(forall (?x)

(if (or (activity_occurrence ?x)

(object ?x))

(beforeEq (beginof ?x) (endof ?x))))

(forall (?x ?occ ?t)

(if (participates_in ?x ?occ ?t)

(and (object ?x)

(activity_occurrence ?occ)

(timepoint ?t))))

(forall (?x ?occ ?t)

(if (participates_in ?x ?occ ?t)

(and (exists_at ?x ?t)

(is_occurring_at ?occ ?t))))

(forall (?t1 ?t2 ?t3) (iff (between ?t1 ?t2 ?t3)

(and (before ?t1 ?t2) (before ?t2 ?t3))))

(forall (?t1 ?t2) (iff (beforeEq ?t1 ?t2)

(and (timepoint ?t1) (timepoint ?t2)

(or (before ?t1 ?t2) (= ?t1 ?t2)))))

(forall (?t1 ?t2 ?t3) (iff (betweenEq ?t1 ?t2 ?t3)

(and (beforeEq ?t1 ?t2)

(beforeEq ?t2 ?t3))))

(forall (?x ?t) (iff (exists_at ?x ?t)

(and (object ?x)

(betweenEq (beginof ?x) ?t (endof ?x)))))

(forall (?occ ?t) (iff (is_occurring_at ?occ ?t)

(betweenEq (beginof ?occ) ?t (endof ?occ))))