4692b8b63985ab174478d389e20a544054e09ce8Karl Luc(forall (?t1 ?t2)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (if (before ?t1 ?t2)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (and (timepoint ?t1)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (timepoint ?t2))))
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc(forall (?t1 ?t2)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (if (and (timepoint ?t1)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (timepoint ?t2))
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (or (= ?t1 ?t2)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (before ?t1 ?t2)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (before ?t2 ?t1))))
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc(forall (?t1)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (not (before ?t1 ?t1)))
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc(forall (?t1 ?t2 ?t3)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (if (and (before ?t1 ?t2)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (before ?t2 ?t3))
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (before ?t1 ?t3)))
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc(forall (?t)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (if (and (timepoint ?t)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (not (= ?t inf-)))
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (before inf- ?t)))
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc(forall (?t)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (if (and (timepoint ?t)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (not (= ?t inf+)))
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (before ?t inf+)))
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc(forall (?t)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (if (and (timepoint ?t)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (not (= ?t inf-)))
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (exists (?u)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (between inf- ?u ?t))))
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc(forall (?t)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (if (and (timepoint ?t)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (not (= ?t inf+)))
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (exists (?u)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (between ?t ?u inf+))))
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc(forall (?x)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (or (activity ?x)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (activity_occurrence ?x)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (timepoint ?x)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (object ?x)))
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc(forall (?x)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc(and (if (activity ?x)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (not (or (activity_occurrence ?x) (object ?x) (timepoint ?x))))
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (if (activity_occurrence ?x)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (not (or (object ?x) (timepoint ?x))))
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (if (object ?x)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (not (timepoint ?x)))))
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc(forall (?a ?occ)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (if (occurrence_of ?occ ?a)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (and (activity ?a)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (activity_occurrence ?occ))))
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc(forall (?occ)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (if (activity_occurrence ?occ)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (exists (?a)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (and (activity ?a)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (occurrence_of ?occ ?a)))))
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc(forall (?occ ?a1 ?a2)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (if (and (occurrence_of ?occ ?a1)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (occurrence_of ?occ ?a2))
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (= ?a1 ?a2)))
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc(forall (?a ?x)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (if (or (occurrence_of ?x ?a)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (object ?x))
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (and (timepoint (beginof ?x))
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (timepoint (endof ?x)))))
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc(forall (?x)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (if (or (activity_occurrence ?x)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (object ?x))
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (beforeEq (beginof ?x) (endof ?x))))
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc(forall (?x ?occ ?t)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (if (participates_in ?x ?occ ?t)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (and (object ?x)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (activity_occurrence ?occ)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (timepoint ?t))))
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc(forall (?x ?occ ?t)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (if (participates_in ?x ?occ ?t)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (and (exists_at ?x ?t)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (is_occurring_at ?occ ?t))))
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc(forall (?t1 ?t2 ?t3) (iff (between ?t1 ?t2 ?t3)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (and (before ?t1 ?t2) (before ?t2 ?t3))))
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc(forall (?t1 ?t2) (iff (beforeEq ?t1 ?t2)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (and (timepoint ?t1) (timepoint ?t2)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (or (before ?t1 ?t2) (= ?t1 ?t2)))))
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc(forall (?t1 ?t2 ?t3) (iff (betweenEq ?t1 ?t2 ?t3)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (and (beforeEq ?t1 ?t2)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (beforeEq ?t2 ?t3))))
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc(forall (?x ?t) (iff (exists_at ?x ?t)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (and (object ?x)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (betweenEq (beginof ?x) ?t (endof ?x)))))
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc(forall (?occ ?t) (iff (is_occurring_at ?occ ?t)
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc (betweenEq (beginof ?occ) ?t (endof ?occ))))