(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))))

(forall (?o1 ?o2) 
	(if	(subactivity_occurrence ?o1 ?o2)
		(and  	(activity_occurrence ?o1)
			(activity_occurrence ?o2))))

(forall (?a ?s1 ?s2)
	(if	(min_precedes ?s1 ?s2 ?a)
		(exists (?occ)
			(and	(occurrence_of ?occ ?a)
				(subactivity_occurrence ?s1 ?occ)
				(subactivity_occurrence ?s2 ?occ)))))

(forall (?a ?s)
	(if	(root ?s ?a)
		(exists (?occ)
			(and	(occurrence_of ?occ ?a)
				(subactivity_occurrence ?s ?occ)))))

(forall (?occ ?a)
	(if	(and   (occurrence_of ?occ ?a)
                       (not (atomic ?a)))
		(exists (?s)
			(and	(root ?s ?a)
				(subactivity_occurrence ?s ?occ)))))

(forall (?a ?s1 ?occ1 ?occ2)
	(if	(and	(occurrence_of ?occ1 ?a)
			(occurrence_of ?occ2 ?a)
			(not (atomic ?a))
			(not (= ?occ1 ?occ2))
			(arboreal ?s1)
			(subactivity_occurrence ?s1 ?occ1)
			(subactivity_occurrence ?s1 ?occ2))
		(exists (?s2)
			(and	(min_precedes ?s1 ?s2 ?a)
				(subactivity_occurrence ?s2 ?occ1)
				(not (subactivity_occurrence ?s2 ?occ2))))))

(forall (?a ?occ ?s1 ?s2)
	(if	(and	(occurrence_of ?occ ?a)
			(not (atomic ?a))
			(arboreal ?s1)
			(arboreal ?s2)
			(subactivity_occurrence ?s1 ?occ)
		  	(subactivity_occurrence ?s2 ?occ))
		(or	(min_precedes ?s1 ?s2 ?a)
		  	(min_precedes ?s2 ?s1 ?a)
			(= ?s1 ?s2))))

(forall (?a ?s1 ?s2 ?occ)
	(if	(and	(min_precedes ?s1 ?s2 ?a)
			(subactivity_occurrence ?s2 ?occ))
		(subactivity_occurrence ?s1 ?occ)))

(forall (?a1 ?a2 ?occ1 ?occ2)
	(if	(and	(occurrence_of ?occ1 ?a1)
			(occurrence_of ?occ2 ?a2)
			(subactivity_occurrence ?occ1 ?occ2))
		(subactivity ?a1 ?a2)))

(forall (?occ1 ?occ2 ?occ3)
        (if	(and  (subactivity_occurrence ?occ1 ?occ2)
                  	(subactivity_occurrence ?occ2 ?occ3))
		(subactivity_occurrence ?occ1 ?occ3)))

(forall (?a1 ?a2 ?occ1 ?occ2)
        (if	(and	(occurrence_of ?occ1 ?a1)
			(occurrence_of ?occ2 ?a2)
			(subactivity ?a1 ?a2)
			(not (subactivity_occurrence ?occ1 ?occ2)))
		(exists (?s)
			(and	(subactivity_occurrence ?s ?occ2)
				(not (subactivity_occurrence ?s ?occ1))))))

(forall (?occ)
	(if	(activity_occurrence ?occ)
		(= (beginof ?occ) (beginof (root_occ ?occ)))))

(forall (?s ?occ)
	(if	(leaf_occ ?s ?occ)
		(= (endof ?occ) (endof ?s))))

(forall (?s1 ?s2 ?a)
        (if	(mono ?s1 ?s2 ?a)
		(hom ?s1 ?s2 ?a)))

(forall (?s1 ?s2 ?a)
        (if	(and	(hom ?s1 ?s2 ?a)
			(not (mono ?s1 ?s2 ?a)))
		(exists (?s3)
			(or	(and	(min_precedes ?s3 ?s2 ?a)
					(mono ?s1 ?s3 ?a))
				(and	(min_precedes ?s3 ?s1 ?a)
					(mono ?s2 ?s3 ?a))))))

(forall (?s1 ?s2 ?s3 ?a)
        (if	(and	(mono ?s1 ?s2 ?a)
			(mono ?s3 ?s2 ?a))
		(not 	(or	(min_precedes ?s1 ?s3 ?a)
				(min_precedes ?s3 ?s1 ?a)))))

(forall (?s1 ?s2 ?a)
    (if   (mono ?s1 ?s2 ?a)
          (mono ?s2 ?s1 ?a)))

(forall (?s1 ?s2 ?s3 ?a)
    (if   (and   (mono ?s1 ?s2 ?a)
                 (mono ?s2 ?s3 ?a))
          (mono ?s1 ?s3 ?a)))

(forall (?s1 ?s2 ?a) (iff (iso_occ ?s1 ?s2 ?a)
(exists (?a1 ?a2 ?a3)
        (and    (atomic ?a1)
		(atomic ?a2)
		(atomic ?a3)
		(subactivity ?a1 ?a)
		(occurrence_of ?s1 (conc ?a1 ?a2))
                (occurrence_of ?s2 (conc ?a1 ?a3))))))

(forall (?s1 ?s2 ?a) (iff (hom ?s1 ?s2 ?a)
(exists (?occ1 ?occ2)
	(and    (iso_occ ?s1 ?s2 ?a)
		(not (min_precedes ?s1 ?s2 ?a))
		(not (min_precedes ?s2 ?s1 ?a))
		(subactivity_occurrence ?s1 ?occ1)
		(subactivity_occurrence ?s2 ?occ2)
		(occurrence_of ?occ1 ?a)
		(occurrence_of ?occ2 ?a)))))

(forall (?s ?occ)
(if (and (activity_occurrence ?s)
         (activity_occurrence ?occ))
(iff (= ?s (root_occ ?occ))
(exists (?a)
    (and    (occurrence_of ?occ ?a)
            (subactivity_occurrence ?s ?occ)
            (root ?s ?a))))))

(forall (?s ?occ) (iff (leaf_occ ?s ?occ)
(exists (?a)
	(and	(occurrence_of ?occ ?a)
		(subactivity_occurrence ?s ?occ)
		(leaf ?s ?a)))))

(forall (?occ1 ?occ2) (iff (same_grove ?occ1 ?occ2)
(exists (?a)
	(and	(occurrence_of ?occ1 ?a)
		(occurrence_of ?occ2 ?a)
                (or     (and    (initial (root_occ ?occ1))
                                (initial (root_occ ?occ2)))
                        (exists (?s4 ?a1 ?a2)
                                (and    (= (root_occ ?occ1) (successor ?a1 ?s4))
                                        (= (root_occ ?occ2) (successor ?a2 ?s4)))))))))

(forall (?a)
	(if	(primitive ?a)
		(atomic ?a)))

(forall (?a)
	(= ?a (conc ?a ?a)))

(forall (?a1 ?a2)
	(= (conc ?a1 ?a2) (conc ?a2 ?a1)))

(forall (?a1 ?a2 ?a3)
	(= (conc ?a1 (conc ?a2 ?a3)) (conc (conc ?a1 ?a2) ?a3)))

(forall (?a1 ?a2)
	(iff	(atomic (conc ?a1 ?a2))
		(and	(atomic ?a1)
			(atomic ?a2))))

(forall (?a1 ?a2)
	(if	(and	(atomic ?a1)
			(atomic ?a2))
		(iff	(subactivity ?a1 ?a2)
			(= ?a2 (conc ?a1 ?a2)))))

(forall (?a1 ?a2)
	(if	(and	(atomic ?a2)
		  	(subactivity ?a1 ?a2)
			(not (= ?a1 ?a2)))
		(exists (?a3)
			(and	(atomic ?a3)
				(= ?a2 (conc ?a1 ?a3))
				(not (exists (?a4)
					(and	(atomic ?a4)
						(subactivity ?a4 ?a1)
						(subactivity ?a4 ?a3))))))))

(forall (?a ?b0 ?b1)
	(if	(and	(atomic ?a)
			(atomic ?b0)
			(atomic ?b1)
			(subactivity ?a (conc ?b0 ?b1))
			(not (primitive ?a)))
		(exists (?a0 ?a1)
			(and	(subactivity ?a0 ?a)
				(subactivity ?a1 ?a)
				(= ?a (conc ?a0 ?a1))))))

(forall (?a)
	(if	(generator ?a)
		(atomic ?a)))

(forall (?a)
	(if	(atomic ?a)
		(activity ?a)))

(forall (?a ?s1 ?s2)
	(if	(min_precedes ?s1 ?s2 ?a)
		(exists (?a1 ?a2)
			(and	(subactivity ?a1 ?a)
				(atomic ?a2)
				(subactivity ?a1 ?a2)
				(occurrence_of ?s1 ?a2)))))

(forall (?a ?s1 ?s2)
	(if	(min_precedes ?s1 ?s2 ?a)
		(exists (?a2 ?a3)
			(and	(subactivity ?a2 ?a)
				(atomic ?a3)
				(subactivity ?a2 ?a3)
				(occurrence_of ?s2 ?a3)))))

(forall (?a ?s)
	(if	(root ?s ?a)
		(exists (?a2 ?a3)
			(and	(subactivity ?a2 ?a3)
				(atomic ?a3)
				(subactivity ?a2 ?a)
				(occurrence_of ?s ?a3)))))

(forall (?s1 ?s2 ?a)
	(if	(min_precedes ?s1 ?s2 ?a)
		(exists (?s3)
			(and	(root ?s3 ?a)
				(or	(min_precedes ?s3 ?s1 ?a)
					(= ?s3 ?s1))))))

(forall (?s ?a)
	(if	(root ?s ?a)
		(not (exists (?s2)
			(and	(activity_occurrence ?s2)
				(min_precedes ?s2 ?s ?a))))))

(forall (?s1 ?s2 ?a)
	(if	(min_precedes ?s1 ?s2 ?a)
		(precedes ?s1 ?s2)))

(forall (?s ?a)
	(if	(root ?s ?a)
		(legal ?s)))

(forall (?a1 ?a2 ?s)
        (if	(and    (atomic ?a1)
                        (occurrence_of ?s ?a1)
                        (legal ?s)
			(subactivity ?a2 ?a1))
		(root ?s ?a2)))

(forall (?a ?s1 ?s2)
	(if	(min_precedes ?s1 ?s2 ?a)
		(exists (?s3)
			(and	(next_subocc ?s1 ?s3 ?a)
				(or	(min_precedes ?s3 ?s2 ?a)
					(= ?s3 ?s2))))))

(forall (?a ?s1 ?s2 ?s3)
	(if	(and	(min_precedes ?s1 ?s2 ?a)
			(min_precedes ?s1 ?s3 ?a)
			(precedes ?s2 ?s3))
		(min_precedes ?s2 ?s3 ?a)))

(forall (?a1 ?a2)
	(if	(subactivity ?a1 ?a2)
		(not (exists (?s)
			(and	(activity_occurrence ?s)
				(subtree ?s ?a2 ?a1))))))

(forall (?s1 ?s2 ?a)
        (if	(min_precedes ?s1 ?s2 ?a)
                (not (atomic ?a))))

(forall (?a ?s1 ?s2 ?s3)
	(if	(and	(min_precedes ?s2 ?s1 ?a)
			(min_precedes ?s3 ?s1 ?a)
			(precedes ?s2 ?s3))
		(min_precedes ?s2 ?s3 ?a)))

(forall (?s ?a) (iff (leaf ?s ?a)
(exists (?s1)
	(and	(arboreal ?s1)
		(or	(root ?s ?a)
			(min_precedes ?s1 ?s ?a))
		(not (exists (?s2)
			(min_precedes ?s ?s2 ?a)))))))

(forall (?a ?s1 ?s2) (iff (do ?a ?s1 ?s2)
(and	(root ?s1 ?a)
	(leaf ?s2 ?a)
	(or	(min_precedes ?s1 ?s2 ?a)
		(= ?s1 ?s2)))))

(forall (?s1 ?s2 ?a) (iff (next_subocc ?s1 ?s2 ?a)
(and    (min_precedes ?s1 ?s2 ?a)
        (not (exists (?s3)
                (and    (activity_occurrence ?s3)
			(min_precedes ?s1 ?s3 ?a)
                        (min_precedes ?s3 ?s2 ?a)))))))

(forall (?s1 ?a1 ?a2) (iff (subtree ?s1 ?a1 ?a2)
    (and  (root ?s1 ?a1)
          (exists (?s2 ?s3)
             (and    (root ?s2 ?a2)
                     (min_precedes ?s1 ?s2 ?a1)
                     (min_precedes ?s1 ?s3 ?a1)
                     (not (min_precedes ?s2 ?s3 ?a2)))))))

(forall (?s1 ?s2 ?a) (iff (sibling ?s1 ?s2 ?a)
(or	(exists (?s3)
		(and	(next_subocc ?s3 ?s1 ?a)
			(next_subocc ?s3 ?s2 ?a)))
	(and	(root ?s1 ?a)
		(root ?s2 ?a)
		(or	(and	(initial ?s1)
				(initial ?s2))
			(exists (?s4 ?a1 ?a2)
				(and	(= ?s1 (successor ?a1 ?s4))
					(= ?s2 (successor ?a2 ?s4)))))))))

(forall (?f)
	(if	(state ?f)
		(object ?f)))

(forall (?f ?occ)
	(if	(holds ?f ?occ)
		(and	(state ?f)
			(arboreal ?occ))))

(forall (?f ?occ)
	(if	(prior ?f ?occ)
		(and	(state ?f)
			(arboreal ?occ))))

(forall (?occ1 ?occ2 ?f)
	(if	(and	(initial ?occ1)
			(initial ?occ2))
		(iff	(prior ?f ?occ1)
			(prior ?f ?occ2))))

(forall (?f ?a ?occ)
        (iff    (prior ?f (successor ?a ?occ))
                (and    (holds ?f ?occ)
                        (generator ?a))))

(forall (?occ1 ?f)
	(if	(holds ?f ?occ1)
		(exists (?occ2)
			(and	(earlierEq ?occ2 ?occ1)
				(holds ?f ?occ2)
				(or	(initial ?occ2)
					(not (prior ?f ?occ2)))
				(forall (?occ3)
					(if	(and	(earlier ?occ2 ?occ3)
							(earlier ?occ3 ?occ1))
						(holds ?f ?occ3)))))))

(forall (?occ1 ?f)
	(if	(and	(state ?f)
			(arboreal ?occ1)
			(not (holds ?f ?occ1)))
		(exists (?occ2)
			(and	(earlierEq ?occ2 ?occ1)
				(not (holds ?f ?occ2))
				(or	(initial ?occ2)
					(prior ?f ?occ2))
				(not (exists (?occ3)
					(and	(earlier ?occ2 ?occ3)
						(earlier ?occ3 ?occ1)
						(holds ?f ?occ3))))))))

(forall (?f ?s1)
	(if	(holds ?f ?s1)
		(exists (?s2)
			(and	(holds ?f ?s2)
				(earlierEq ?s2 ?s1)
				(forall (?s3)
					(if	(holds ?f ?s3)
						(not (earlier ?s3 ?s2))))))))

(forall (?s1 ?s2)
	(if	(earlier ?s1 ?s2)
		(and	(arboreal ?s1)
			(arboreal ?s2))))

(forall (?s1 ?s2)
	(if	(earlier ?s1 ?s2)
		(not (earlier ?s2 ?s1))))

(forall (?s1 ?s2 ?s3)
	(if	(and	(earlier ?s1 ?s2)
			(earlier ?s2 ?s3))
		(earlier ?s1 ?s3)))

(forall (?s1 ?s2 ?s3)
	(if	(and	(earlier ?s1 ?s2)
			(earlier ?s3 ?s2))
		(or	(earlier ?s1 ?s3)
			(earlier ?s3 ?s1)
			(= ?s3 ?s1))))

(forall (?s)
	(iff	(initial ?s)
		(and	(arboreal ?s)
			(not (exists (?sp)
				(earlier ?sp ?s))))))

(forall (?s1 ?s2)
	(if	(earlier ?s1 ?s2)
		(exists (?sp)
			(and	(initial ?sp)
				(earlierEq ?sp ?s1)))))

(forall (?s ?a)
        (if	(occurrence_of ?s ?a)
		(iff	(arboreal ?s)
			(generator ?a))))

(forall (?s1 ?s2 ?a)
	(if	(and	(initial ?s1)
			(initial ?s2)
			(occurrence_of ?s1 ?a)
			(occurrence_of ?s2 ?a))
		(= ?s1 ?s2)))

(forall (?a ?o)
        (iff    (occurrence_of (successor ?a ?o) ?a)
                (and    (generator ?a)
                        (arboreal ?o))))

(forall (?s1 ?s2)
        (if	(earlier ?s1 ?s2)
		(exists (?a ?s3)
                        (and    (generator ?a)
                                (= ?s2 (successor ?a ?s3))))))

(forall (?a ?s1 ?s2)
        (if	(generator ?a)
		(iff	(earlier ?s1 (successor ?a ?s2))
			(earlierEq ?s1 ?s2))))

(forall (?s)
	(if	(legal ?s)
		(arboreal ?s)))

(forall (?s1 ?s2)
	(if	(and	(legal ?s1)
			(earlier ?s2 ?s1))
		(legal ?s2)))

(forall (?s1 ?s2)
	(if	(earlier ?s1 ?s2)
		(before (endof ?s1) (beginof ?s2))))

(forall (?s1 ?s2) (iff (precedes ?s1 ?s2)
(and	(earlier ?s1 ?s2)
	(legal ?s2))))

(forall (?s1 ?s2) (iff (earlierEq ?s1 ?s2)
(and	(arboreal ?s1)
	(arboreal ?s2)
	(or	(earlier ?s1 ?s2)
		(= ?s1 ?s2)))))

(forall (?a ?s) (iff (poss ?a ?s)
(legal (successor ?a ?s))))

(forall (?a) (iff  (generator ?a)
(exists (?s)
        (and    (initial ?s)
                (occurrence_of ?s ?a)))))

(forall (?s) (iff  (arboreal ?s)
(exists (?sp)
        (earlier ?s ?sp))))

(forall (?a1 ?a2)
	(if	(subactivity ?a1 ?a2)
		(and	(activity ?a1)
			(activity ?a2))))

(forall (?a)
	(if	(activity ?a)
		(subactivity ?a ?a)))

(forall (?a1 ?a2)
	(if	(and	(subactivity ?a1 ?a2)
			(subactivity ?a2 ?a1))
		(= ?a1 ?a2)))

(forall (?a1 ?a2 ?a3)
	(if	(and	(subactivity ?a1 ?a2)
			(subactivity ?a2 ?a3))
		(subactivity ?a1 ?a3)))

(forall (?a1 ?a2)
	(if	(and	(subactivity ?a1 ?a2)
			(not (= ?a1 ?a2)))
		(exists (?a3)
			(and	(subactivity ?a1 ?a3)
				(subactivity ?a3 ?a2)
				(not (= ?a3 ?a1))
				(forall (?a4)
					(if	(and	(subactivity ?a1 ?a4)
							(subactivity ?a4 ?a3))
						(or	(= ?a4 ?a1)
							(= ?a4 ?a3))))))))
(forall (?a1 ?a2)
	(if	(and	(subactivity ?a1 ?a2)
			(not (= ?a1 ?a2)))
		(exists (?a3)
			(and	(subactivity ?a1 ?a3)
				(subactivity ?a3 ?a2)
				(not (= ?a3 ?a2))
				(forall (?a4)
					(if	(and	(subactivity ?a3 ?a4)
							(subactivity ?a4 ?a2))
						(or	(= ?a4 ?a2)
							(= ?a4 ?a3))))))))

(forall (?a) (iff (primitive ?a)
(and    (activity ?a)
	(forall (?a1)
		(if	(subactivity ?a1 ?a)
			(= ?a1 ?a))))))

(and	(timeduration zero)
	(timeduration max+)
	(timeduration max-))

(forall (?d1 ?d2)
(if	  (and	(timeduration ?d1)
		(timeduration ?d2))
	  (timeduration (add ?d1 ?d2))))

(forall (?d1 ?d2 ?d3)
(if	  (and	(timeduration ?d1)
		(timeduration ?d2)
		(timeduration ?d3))
          (= (add (add ?d1 ?d2) ?d3) (add ?d1 (add ?d2 ?d3)))))

(forall (?d)
(if	  (timeduration ?d)
          (= (add ?d zero) ?d)))

(forall (?d1)
(if	  (timeduration ?d1)
          (exists (?d2)
		(and 	(timeduration ?d2)
                	(= (add ?d1 ?d2) zero)))))

(forall (?d1 ?d2)
(if	  (and	(timeduration ?d1)
		(timeduration ?d2))
          (= (add ?d1 ?d2) (add ?d2 ?d1))))

(forall (?d ?r)
(if	  (timeduration ?d)
	  (timeduration (mult ?r ?d))))

(forall (?d1 ?d2 ?r)
        (= (mult ?r (add ?d1 ?d2)) (add (mult ?r ?d1) (mult ?r ?d2))))

(forall (?d ?r ?s)
        (= (mult (add ?r ?s) ?d) (add (mult ?r ?d) (mult ?s ?d))))

(forall (?d ?r ?s)
        (= (mult (mult ?r ?s) ?d) (mult ?r (mult ?s ?d))))

(forall (?d)
        (= ?d (mult one ?d)))

(forall (?d1 ?d2 ?d3)
(if	(and	(timeduration ?d1)
		(timeduration ?d2)
		(timeduration ?d3))
        (iff    (lesser ?d1 ?d2)
                (lesser (add ?d1 ?d3) (add ?d2 ?d3)))))

(forall (?d1 ?d2 ?d3)
(if	(and	(timeduration ?d1)
		(timeduration ?d2)
		(timeduration ?d3))
        (iff    (= ?d1 ?d2)
                (= (add ?d1 ?d3) (add ?d2 ?d3)))))

(forall (?d)
	(if	  (timeduration ?d)
		  (and	(lesser ?d max+)
			(lesser max- ?d))))

(forall (?d)
(if	  (timeduration ?d)
	  (and 	(if	  (not (= ?d max-)) (= max+ (add ?d max+)))
		(if	  (not (= ?d max+)) (= max- (add ?d max-)))
		(= zero (add max+ max-)))))

(forall (?t1 ?t2)
	(if	  (and	(timepoint ?t1)
			(timepoint ?t2))
		  (timeduration (duration ?t1 ?t2))))

(forall (?d)
	(if	  (timeduration ?d)
        	  (exists (?t1 ?t2)
			(and	(timepoint ?t1)
				(timepoint ?t2)
	                	(= ?d (duration ?t1 ?t2))))))

(forall (?t1 ?t2)
(if	  (and	(timepoint ?t1)
		(timepoint ?t2))
	  (iff	(= zero (duration ?t1 ?t2))
		(= ?t1 ?t2))))

(forall (?t1 ?t2)
(if	  (and	(timepoint ?t1)
		(timepoint ?t2))
	  (= zero (add (duration ?t1 ?t2) (duration ?t2 ?t1)))))

(forall (?t1 ?t2 ?t3)
	(if	  (and	(timepoint ?t1)
			(timepoint ?t2)
			(timepoint ?t3)
			(not (= ?t1 inf-))
			(not (= ?t2 inf+))
			(= (duration ?t1 ?t2) (duration ?t1 ?t3)))
		  (= ?t1 ?t2)))

(forall (?t)
(and 	(if	  (and	(timepoint ?t)
			(not (= ?t inf-)))
		  (= max+ (duration inf- ?t)))
	(if	  (and	(timepoint ?t)
			(not (= ?t inf+)))
		  (= max- (duration inf+ ?t)))))

(forall (?t)
(and 	(if	  (and	(timepoint ?t)
			(not (= ?t inf-)))
		  (= max- (duration ?t inf-)))
	(if	  (and	(timepoint ?t)
			(not (= ?t inf+)))
		  (= max+ (duration ?t inf+)))))

			
(forall (?t1 ?t2 ?d)
(iff	(= ?t2 (time_add ?t1 ?d))
	(and	(timepoint ?t1)
		(timepoint ?t2)
		(timeduration ?d)
		(= ?d (duration ?t2 ?t1)))))

(forall (?a1 ?s)
	(if	  (root ?s ?a1)
		  (exists (?a2)
			(envelope ?a2 ?a1 ?s))))

(forall (?a1 ?s)
	(if	  (root ?s ?a1)
		  (exists (?a2)
			(umbra ?a2 ?a1 ?s))))

(forall (?a1 ?a2 ?s ?s1)
	(if	  (and	(envelope ?a2 ?a1 ?s)
			(live_branch ?s1 ?s ?a2))
		  (not (dead_branch ?s1 ?s ?a1))))

(forall (?a1 ?a2 ?s ?s1)
	(if	  (and	(umbra ?a2 ?a1 ?s)
			(live_branch ?s1 ?s ?a2))
		  (not (live_branch ?s1 ?s ?a1))))

(forall (?a1 ?a2 ?s ?s1)
	(if	  (and	(envelope ?a2 ?a1 ?s)
			(live_branch ?s1 ?s ?a1))
		  (live_branch ?s1 ?s ?a2)))

(forall (?a1 ?a2  ?s ?s1)
	(if	  (and	(umbra ?a2 ?a1 ?s)
			(dead_branch ?s1 ?s ?a1))
		  (live_branch ?s1 ?s ?a2)))

(forall (?a1 ?a2 ?s ?o)
	(if	  (and	(envelope ?a2 ?a1 ?s)
			(occurrence_of ?o ?a2)
			(= ?s (root_occ ?o)))
		  (unrestricted ?o)))

(forall (?a1 ?a2 ?s ?o)
	(if	  (and	(umbra ?a2 ?a1 ?s)
			(occurrence_of ?o ?a2)
			(= ?s (root_occ ?o)))
		  (unrestricted ?o)))

(forall (?a1 ?a2 ?s1 ?s2)
	(if	  (and	(ubiquitous ?a1 ?a2)
			(min_precedes ?s1 ?s2 ?a2))
		  (exists (?s3 ?s4 ?s5 ?s6)
			(and	(tree_equiv ?s1 ?s2)
				(tree_equiv ?s3 ?s4)
				(occurrence_of ?s5 ?a1)
				(occurrence_of ?s6 ?a1)
				(legal_equiv ?s5 ?s6)
				(end_iso ?s3 ?s4 ?s5 ?s6)))))

(forall (?a1 ?a2 ?s1 ?s2)
	(if	  (and	(ubiquitous ?a1 ?a2)
			(min_precedes ?s1 ?s2 ?a2))
		  (not (exists (?s3 ?s4)
			(and	(occurrence_of ?s3 ?a1)
				(occurrence_of ?s4 ?a1)
				(legal_equiv ?s3 ?s4)
				(end_iso ?s1 ?s2 ?s3 ?s4))))))

(forall (?a1 ?a2 ?s1 ?s2 ?s3 ?s4)
	(if	  (and	(ubiquitous ?a1 ?a2)
			(occurrence_of ?s3 ?a1)
			(occurrence_of ?s4 ?a1)
			(legal_equiv ?s3 ?s4)
			(end_iso ?s1 ?s2 ?s3 ?s4))
		  (exists (?o1 ?o2)
			(and	(occurrence_of ?o1 ?a1)
				(occurrence_of ?o2 ?a1)
				(subactivity_occurrence ?s1 ?o1)
				(subactivity_occurrence ?s2 ?o1)))))

(forall (?s1 ?s2 ?s3 ?s4) (iff (end_iso ?s1 ?s2 ?s3 ?s4)
(exists (?s5 ?s6)
	(and	(precedes ?s5 ?s1)
		(precedes ?s5 ?s3)
		(precedes ?s6 ?s2)
		(precedes ?s6 ?s4)
		(tree_equiv ?s1 ?s2)
		(tree_equiv ?s3 ?s4)
		(tree_equiv ?s5 ?s6)))))

(forall (?s1 ?s2 ?a)
	(if	  (soo_precedes ?s1 ?s2 ?a)
		  (and	(soo ?s1 ?a)
			(soo ?s2 ?a))))

(forall (?a ?s)
	(if	  (soo ?s ?a)
		  (or	(root ?s ?a)
			(exists (?s1)
				(min_precedes ?s1 ?s ?a)))))

(forall (?s ?occ ?a)
(if     (and    (occurrence_of ?occ ?a)
                (subactivity_occurrence ?s ?occ)
                (arboreal ?s))
         (soo (soomap ?s) ?a)))

(forall (?s ?a)
	(if	  (soo ?s ?a)
		  (= ?s (soomap ?s))))

(forall (?s ?a)
	(or	(mono ?s (soomap ?s) ?a)
		(= ?s (soomap ?s))))

(forall (?a ?s1 ?s2)
	(if	  (min_precedes ?s1 ?s2 ?a)
		  (iff	(soo_precedes (soomap ?s1) (soomap ?s2) ?a)
			(not (exists (?s3 ?s4)
				(and	(min_precedes ?s4 ?s3 ?a)
					(= (soomap ?s3) (soomap ?s1))
					(= (soomap ?s4) (soomap ?s2))))))))

(forall (?a ?s1 ?s2)
	(if	  (soo_precedes ?s1 ?s2 ?a)
		  (not (soo_precedes ?s2 ?s1 ?a))))

(forall (?a ?s1 ?s2 ?s3)
	(if	  (and	(soo_precedes ?s1 ?s2 ?a)
			(soo_precedes ?s2 ?s3 ?a))
		  (soo_precedes ?s1 ?s3 ?a)))

(forall (?s ?a) (iff (root_soo ?s ?a)
(and	(soo ?s ?a)
	(not (exists (?s1)
		(soo_precedes ?s1 ?s ?a))))))

(forall (?s ?a) (iff (leaf_soo ?s ?a)
(and	(soo ?s ?a)
	(not (exists (?s1)
		(soo_precedes ?s ?s1 ?a))))))

(forall (?s1 ?s2 ?a) (iff (next_subactivity ?s1 ?s2 ?a) 
(and    (soo_precedes ?s1 ?s2 ?a)
        (not (exists (?s3)
                (and    (soo_precedes ?s1 ?s3 ?a)
                        (soo_precedes ?s3 ?s2 ?a)))))))

(forall (?a ?a1 ?r ?s)
	(if  (and	(requires ?a ?r)
			(subactivity ?a1 ?a)
			(atomic ?a1)
			(holds (available ?r ?a1) ?s))
		  (exists (?occ)
			(and	(occurrence_of ?occ ?a)
				(subactivity_occurrence (successor ?a1 ?s) ?occ)))))

(forall (?a ?r)
        (iff    (requires ?a ?r)
                (exists (?a1)
                        (and    (atomic ?a1)
                                (subactivity ?a1 ?a)
                                (requires ?a1 ?r)))))

(forall (?r ?a ?s)
	(iff	(prior (available ?r ?a) ?s)
		(exists (?q1 ?q2 ?q3)
                        (and	(prior (resource_point ?r ?q1) ?s)
                                (prior (agg_demand ?r ?q3) ?s)
                                (prior (demand ?r ?a ?q2) ?s)
                                (greater ?q1 (plus ?q2 ?q3))))))

(forall (?r ?a ?q ?s)
	(if  (prior (demand ?r ?a ?q) ?s)
		  (greater ?q zero)))

(forall (?a1 ?a2 ?r ?q ?s)
	(iff	(prior (demand (conc ?a1 ?a2) ?r ?q) ?s)
		(exists (?q1 ?q2)
                        (and    (prior (demand ?a1 ?r ?q1) ?s)
                                (prior (demand ?a2 ?r ?q2) ?s)
                                (= ?q (plus ?q1 ?q2))))))

(forall (?r ?q ?s)
	(iff	(holds (agg_demand ?r ?q) ?s)
		(or	(exists (?a1 ?q1 ?q2)
				(and	(occurrence_of ?s ?a1)
					(prior (demand ?r ?a1 ?q1) ?s)
					(prior (agg_demand ?r ?q2) ?s)
					(= ?q (plus ?q1 ?q2))))
			(exists (?a2 ?q1 ?q2)
				(and	(occurrence_of ?s ?a2)
					(prior (demand ?r ?a2 ?q1) ?s)
					(prior (agg_demand ?r ?q2) ?s)
					(= ?q1 (plus ?q ?q2)))))))

(forall (?i ?r ?occ)
        (if     (holds (resource_set ?i ?r) ?occ)
                (forall (?rp)
                        (if     (set_member ?rp ?i)
                                (exists (?a)
                                        (requires ?a ?rp))))))

(forall (?i ?r1 ?r2 ?a ?occ)
        (if     (and    (holds (resource_set ?i ?r1) ?occ)
                        (set_member ?r2 ?i)
                        (requires ?a ?r2))
                (requires ?a ?r1)))

(forall (?i1 ?i2 ?r ?occ)
        (if     (and    (holds (resource_set ?i1 ?r) ?occ)
                        (holds (resource_set ?i2 ?r) ?occ))
                (= ?i1 ?i2)))

(forall (?r1 ?r2 ?occ)
        (iff    (holds (in_resource_set ?r1 ?r2) ?occ)
                (exists (?i)
                        (and    (set_member ?r1 ?i)
                                (holds (resource_set ?i ?r2) ?occ)))))

(forall (?r1 ?r2 ?occ)
        (iff    (holds (resource_subset ?r1 ?r2) ?occ)
                (forall (?r ?i1 ?i2)
                   (if  (and    (holds (resource_set ?i1 ?r1) ?occ)
                                (holds (resource_set ?i2 ?r2) ?occ)
                                (set_member ?r ?i1))
                        (set_member ?r ?i2)))))