PSLP01

Premises:

(forall (?t1 ?t2)
        (=>     (before ?t1 ?t2)
                (and    (timepoint ?t1) 
                        (timepoint ?t2))))

(forall (?t1 ?t2)
        (=>     (and    (timepoint ?t1) 
                        (timepoint ?t2))
                (or     (= ?t1 ?t2) 
                        (before ?t1 ?t2) 
                        (before ?t2 ?t1))))

(forall (?t1)
        (not (before ?t1 ?t1)))

(forall (?t1 ?t2 ?t3)
        (=>     (and    (before ?t1 ?t2) 
                        (before ?t2 ?t3))
                (before ?t1 ?t3)))

(forall (?t)
                (=>     (and    (timepoint ?t) 
                        (not (= ?t inf-)))
                (before inf- ?t)))

(forall (?t)
                (=>     (and    (timepoint ?t) 
                        (not (= ?t inf+)))
                (before ?t inf+)))

(forall (?t)
        (=>     (and    (timepoint ?t) 
                        (not (= ?t inf-)))
                (exists (?u) 
                        (between inf- ?u ?t))))

(forall (?t)
        (=>     (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 (=> (activity ?x)
                 (not (or (activity_occurrence ?x) (object ?x) (timepoint ?x))))
         (=> (activity_occurrence ?x)
                 (not (or (object ?x) (timepoint ?x))))
         (=> (object ?x)
                 (not (timepoint ?x)))))

(forall (?a ?occ)
        (=>     (occurrence_of ?occ ?a)
                (and    (activity ?a)
                        (activity_occurrence ?occ))))

(forall (?occ)
        (=>     (activity_occurrence ?occ)
                (exists (?a)
                        (and    (activity ?a)
                                (occurrence_of ?occ ?a)))))

(forall (?occ ?a1 ?a2)
                (=>     (and    (occurrence_of ?occ ?a1)
                                (occurrence_of ?occ ?a2))
                (= ?a1 ?a2)))

(forall (?a ?x)
        (=>     (or     (occurrence_of ?x ?a)
                        (object ?x))
                (and    (timepoint (beginof ?x))
                        (timepoint (endof ?x)))))

(forall (?a ?x)
        (=>     (or     (activity_occurrence ?x)
                        (object ?x))
                (beforeEq (beginof ?x) (endof ?x))))

(forall (?x ?a ?t)
        (=>     (participates_in ?x ?a ?t)
                (and    (object ?x) 
                        (activity ?a) 
                        (timepoint ?t))))

(forall (?x ?a ?t)
        (=>     (participates_in ?x ?a ?t)
                (and    (exists_at ?x ?t)
                        (is_occurring_at ?a ?t))))

(forall (?t1 ?t2 ?t) (<=> (between ?t1 ?t2 ?t3)
  (and (before ?t1 ?t2) (before ?t2 ?t3))))

(forall (?t1 ?t2) (<=> (beforeEq ?t1 ?t2)
  (and (timepoint ?t1) (timepoint ?t2)
           (or (before ?t1 ?t2) (= ?t1 ?t2)))))

(forall (?t1 ?t2 ?t3) (<=> (betweenEq ?t1 ?t2 ?t3)
  (and (beforeEq ?t1 ?t2)
           (beforeEq ?t2 ?t3))))

(forall (?x ?t) (<=> (exists_at ?x ?t)
  (and (object ?x)
           (betweenEq (beginof ?x) ?t (endof ?x)))))

(forall (?a ?t) (<=> (is_occurring_at ?a ?t)
(exists (?occ)
        (and    (occurrence_of ?occ ?a)
                (betweenEq (beginof ?occ) ?t (endof ?occ))))))

(before t1 t2)
(before t2 t3)
(activity a1)
(occurrence_of s1 a1)
(= t1 (beginof s1))
(= t3 (endof s1))

PSLP01

Premises:

Conclusion: