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

(forall (?t1 ?t2)
	(=>	(and 	(timepoint ?t1) 
			(timepoint ?t2))
		(or 	(equal ?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 (equal ?t inf-)))
		(before inf- ?t)))

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

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

(forall (?t)
	(=>	(and 	(timepoint ?t) 
			(not (equal ?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))
		(equal ?a1 ?a2)))

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

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

(forall (?x ?occ ?t)
	(=>	(participates_in ?x ?occ ?t)
		(and 	(object ?x) 
			(activity_occurrence ?occ) 
			(timepoint ?t))))

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

(forall (?t1 ?t2 ?t3) (<=> (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) (equal ?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 (?occ ?t) (<=> (is_occurring_at ?occ ?t)
	(betweenEq (beginof ?occ) ?t (endof ?occ))))

(forall (?o1 ?o2) 
	(=>	(subactivity_occurrence ?o1 ?o2)
		(and  	(activity_occurrence ?o1)
			(activity_occurrence ?o2))))

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

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

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

(forall (?a ?s1 ?occ1 ?occ2)
	(=>	(and	(occurrence_of ?occ1 ?a)
			(occurrence_of ?occ2 ?a)
			(not (atomic ?a))
			(not (equal ?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)
	(=>	(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)
			(equal ?s1 ?s2))))

(forall (?a ?s1 ?s2 ?occ)
	(=>	(and	(min_precedes ?s1 ?s2 ?a)
			(subactivity_occurrence ?s2 ?occ))
		(subactivity_occurrence ?s1 ?occ)))

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

(forall (?occ1 ?occ2 ?occ3)
        (=>	(and  (subactivity_occurrence ?occ1 ?occ2)
                  	(subactivity_occurrence ?occ2 ?occ3))
		(subactivity_occurrence ?occ1 ?occ3)))

(forall (?a1 ?a2 ?occ1 ?occ2)
        (=>	(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)
	(=>	(activity_occurrence ?occ)
		(equal (beginof ?occ) (beginof (root_occ ?occ)))))

(forall (?s ?occ)
	(=>	(leaf_occ ?s ?occ)
		(equal (endof ?occ) (endof ?s))))

(forall (?s1 ?s2 ?a)
        (=>	(mono ?s1 ?s2 ?a)
		(hom ?s1 ?s2 ?a)))

(forall (?s1 ?s2 ?a)
        (=>	(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)
        (=>	(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)
    (=>   (mono ?s1 ?s2 ?a)
          (mono ?s2 ?s1 ?a)))

(forall (?s1 ?s2 ?s3 ?a)
    (=>   (and   (mono ?s1 ?s2 ?a)
                 (mono ?s2 ?s3 ?a))
          (mono ?s1 ?s3 ?a)))

(forall (?s1 ?s2 ?a) (<=> (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) (<=> (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)
(=> (and (activity_occurrence ?s)
         (activity_occurrence ?occ))
(<=> (equal ?s (root_occ ?occ))
(exists (?a)
    (and    (occurrence_of ?occ ?a)
            (subactivity_occurrence ?s ?occ)
            (root ?s ?a))))))

(forall (?s ?occ) (<=> (leaf_occ ?s ?occ)
(exists (?a)
	(and	(occurrence_of ?occ ?a)
		(subactivity_occurrence ?s ?occ)
		(leaf ?s ?a)))))

(forall (?occ1 ?occ2) (<=> (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    (equal (root_occ ?occ1) (successor ?a1 ?s4))
                                        (equal (root_occ ?occ2) (successor ?a2 ?s4)))))))))

(forall (?a)
	(=>	(primitive ?a)
		(atomic ?a)))

(forall (?a)
	(equal ?a (conc ?a ?a)))

(forall (?a1 ?a2)
	(equal (conc ?a1 ?a2) (conc ?a2 ?a1)))

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

(forall (?a1 ?a2)
	(<=>	(atomic (conc ?a1 ?a2))
		(and	(atomic ?a1)
			(atomic ?a2))))

(forall (?a1 ?a2)
	(=>	(and	(atomic ?a1)
			(atomic ?a2))
		(<=>	(subactivity ?a1 ?a2)
			(equal ?a2 (conc ?a1 ?a2)))))

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

(forall (?a ?b0 ?b1)
	(=>	(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)
				(equal ?a (conc ?a0 ?a1))))))

(forall (?a)
	(=>	(generator ?a)
		(atomic ?a)))

(forall (?a)
	(=>	(atomic ?a)
		(activity ?a)))

(forall (?a ?s1 ?s2)
	(=>	(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)
	(=>	(min_precedes ?s1 ?s2 ?a)
		(exists (?a2 ?a3)
			(and	(subactivity ?a2 ?a)
				(atomic ?a3)
				(subactivity ?a2 ?a3)
				(occurrence_of ?s2 ?a3)))))

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

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

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

(forall (?s1 ?s2 ?a)
	(=>	(min_precedes ?s1 ?s2 ?a)
		(precedes ?s1 ?s2)))

(forall (?s ?a)
	(=>	(root ?s ?a)
		(legal ?s)))

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

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

(forall (?a ?s1 ?s2 ?s3)
	(=>	(and	(min_precedes ?s1 ?s2 ?a)
			(min_precedes ?s1 ?s3 ?a)
			(precedes ?s2 ?s3))
		(min_precedes ?s2 ?s3 ?a)))

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

(forall (?s1 ?s2 ?a)
        (=>	(min_precedes ?s1 ?s2 ?a)
                (not (atomic ?a))))

(forall (?a ?s1 ?s2 ?s3)
	(=>	(and	(min_precedes ?s2 ?s1 ?a)
			(min_precedes ?s3 ?s1 ?a)
			(precedes ?s2 ?s3))
		(min_precedes ?s2 ?s3 ?a)))

(forall (?s ?a) (<=> (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) (<=> (do ?a ?s1 ?s2)
(and	(root ?s1 ?a)
	(leaf ?s2 ?a)
	(or	(min_precedes ?s1 ?s2 ?a)
		(equal ?s1 ?s2)))))

(forall (?s1 ?s2 ?a) (<=> (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) (<=> (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) (<=> (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	(equal ?s1 (successor ?a1 ?s4))
					(equal ?s2 (successor ?a2 ?s4)))))))))

(forall (?f)
	(=>	(state ?f)
		(object ?f)))

(forall (?f ?occ)
	(=>	(holds ?f ?occ)
		(and	(state ?f)
			(arboreal ?occ))))

(forall (?f ?occ)
	(=>	(prior ?f ?occ)
		(and	(state ?f)
			(arboreal ?occ))))

(forall (?occ1 ?occ2 ?f)
	(=>	(and	(initial ?occ1)
			(initial ?occ2))
		(<=>	(prior ?f ?occ1)
			(prior ?f ?occ2))))

(forall (?f ?a ?occ)
        (<=>    (prior ?f (successor ?a ?occ))
                (and    (holds ?f ?occ)
                        (generator ?a))))

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

(forall (?occ1 ?f)
	(=>	(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)
	(=>	(holds ?f ?s1)
		(exists (?s2)
			(and	(holds ?f ?s2)
				(earlierEq ?s2 ?s1)
				(forall (?s3)
					(=>	(holds ?f ?s3)
						(not (earlier ?s3 ?s2))))))))

(forall (?s1 ?s2)
	(=>	(earlier ?s1 ?s2)
		(and	(arboreal ?s1)
			(arboreal ?s2))))

(forall (?s1 ?s2)
	(=>	(earlier ?s1 ?s2)
		(not (earlier ?s2 ?s1))))

(forall (?s1 ?s2 ?s3)
	(=>	(and	(earlier ?s1 ?s2)
			(earlier ?s2 ?s3))
		(earlier ?s1 ?s3)))

(forall (?s1 ?s2 ?s3)
	(=>	(and	(earlier ?s1 ?s2)
			(earlier ?s3 ?s2))
		(or	(earlier ?s1 ?s3)
			(earlier ?s3 ?s1)
			(equal ?s3 ?s1))))

(forall (?s)
	(<=>	(initial ?s)
		(and	(arboreal ?s)
			(not (exists (?sp)
				(earlier ?sp ?s))))))

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

(forall (?s ?a)
        (=>	(occurrence_of ?s ?a)
		(<=>	(arboreal ?s)
			(generator ?a))))

(forall (?s1 ?s2 ?a)
	(=>	(and	(initial ?s1)
			(initial ?s2)
			(occurrence_of ?s1 ?a)
			(occurrence_of ?s2 ?a))
		(equal ?s1 ?s2)))

(forall (?a ?o)
        (<=>    (occurrence_of (successor ?a ?o) ?a)
                (and    (generator ?a)
                        (arboreal ?o))))

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

(forall (?a ?s1 ?s2)
        (=>	(generator ?a)
		(<=>	(earlier ?s1 (successor ?a ?s2))
			(earlierEq ?s1 ?s2))))

(forall (?s)
	(=>	(legal ?s)
		(arboreal ?s)))

(forall (?s1 ?s2)
	(=>	(and	(legal ?s1)
			(earlier ?s2 ?s1))
		(legal ?s2)))

(forall (?s1 ?s2)
	(=>	(earlier ?s1 ?s2)
		(before (endof ?s1) (beginof ?s2))))

(forall (?s1 ?s2) (<=> (precedes ?s1 ?s2)
(and	(earlier ?s1 ?s2)
	(legal ?s2))))

(forall (?s1 ?s2) (<=> (earlierEq ?s1 ?s2)
(and	(arboreal ?s1)
	(arboreal ?s2)
	(or	(earlier ?s1 ?s2)
		(equal ?s1 ?s2)))))

(forall (?a ?s) (<=> (poss ?a ?s)
(legal (successor ?a ?s))))

(forall (?a) (<=>  (generator ?a)
(exists (?s)
        (and    (initial ?s)
                (occurrence_of ?s ?a)))))

(forall (?s) (<=>  (arboreal ?s)
(exists (?sp)
        (earlier ?s ?sp))))

(forall (?a1 ?a2)
	(=>	(subactivity ?a1 ?a2)
		(and	(activity ?a1)
			(activity ?a2))))

(forall (?a)
	(=>	(activity ?a)
		(subactivity ?a ?a)))

(forall (?a1 ?a2)
	(=>	(and	(subactivity ?a1 ?a2)
			(subactivity ?a2 ?a1))
		(equal ?a1 ?a2)))

(forall (?a1 ?a2 ?a3)
	(=>	(and	(subactivity ?a1 ?a2)
			(subactivity ?a2 ?a3))
		(subactivity ?a1 ?a3)))

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

(forall (?a) (<=> (primitive ?a)
(and    (activity ?a)
	(forall (?a1)
		(=>	(subactivity ?a1 ?a)
			(equal ?a1 ?a))))))

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

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

(forall (?d1 ?d2 ?d3)
(=>	  (and	(timeduration ?d1)
		(timeduration ?d2)
		(timeduration ?d3))
          (equal (add (add ?d1 ?d2) ?d3) (add ?d1 (add ?d2 ?d3)))))

(forall (?d)
(=>	  (timeduration ?d)
          (equal (add ?d zero) ?d)))

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

(forall (?d1 ?d2)
(=>	  (and	(timeduration ?d1)
		(timeduration ?d2))
          (equal (add ?d1 ?d2) (add ?d2 ?d1))))

(forall (?d ?r)
(=>	  (timeduration ?d)
	  (timeduration (mult ?r ?d))))

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

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

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

(forall (?d)
        (equal ?d (mult one ?d)))

(forall (?d1 ?d2 ?d3)
(=>	(and	(timeduration ?d1)
		(timeduration ?d2)
		(timeduration ?d3))
        (<=>    (lesser ?d1 ?d2)
                (lesser (add ?d1 ?d3) (add ?d2 ?d3)))))

(forall (?d1 ?d2 ?d3)
(=>	(and	(timeduration ?d1)
		(timeduration ?d2)
		(timeduration ?d3))
        (<=>    (equal ?d1 ?d2)
                (equal (add ?d1 ?d3) (add ?d2 ?d3)))))

(forall (?d)
	(=>	  (timeduration ?d)
		  (and	(lesser ?d max+)
			(lesser max- ?d))))

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

(forall (?t1 ?t2)
	(=>	  (and	(timepoint ?t1)
			(timepoint ?t2))
		  (timeduration (duration ?t1 ?t2))))

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

(forall (?t1 ?t2)
(=>	  (and	(timepoint ?t1)
		(timepoint ?t2))
	  (<=>	(equal zero (duration ?t1 ?t2))
		(equal ?t1 ?t2))))

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

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

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

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

			
(forall (?t1 ?t2 ?d)
(<=>	(equal ?t2 (time_add ?t1 ?d))
	(and	(timepoint ?t1)
		(timepoint ?t2)
		(timeduration ?d)
		(equal ?d (duration ?t2 ?t1)))))

(forall (?a1 ?s)
	(=>	  (root ?s ?a1)
		  (exists (?a2)
			(envelope ?a2 ?a1 ?s))))

(forall (?a1 ?s)
	(=>	  (root ?s ?a1)
		  (exists (?a2)
			(umbra ?a2 ?a1 ?s))))

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

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

(forall (?a1 ?a2 ?s ?s1)
	(=>	  (and	(envelope ?a2 ?a1 ?s)
			(live_branch ?s1 ?s ?a1))
		  (live_branch ?s1 ?s ?a2)))

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

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

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

(forall (?a1 ?a2 ?s1 ?s2)
	(=>	  (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)
	(=>	  (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)
	(=>	  (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) (<=> (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)
	(=>	  (soo_precedes ?s1 ?s2 ?a)
		  (and	(soo ?s1 ?a)
			(soo ?s2 ?a))))

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

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

(forall (?s ?a)
	(=>	  (soo ?s ?a)
		  (equal ?s (soomap ?s))))

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

(forall (?a ?s1 ?s2)
	(=>	  (min_precedes ?s1 ?s2 ?a)
		  (<=>	(soo_precedes (soomap ?s1) (soomap ?s2) ?a)
			(not (exists (?s3 ?s4)
				(and	(min_precedes ?s4 ?s3 ?a)
					(equal (soomap ?s3) (soomap ?s1))
					(equal (soomap ?s4) (soomap ?s2))))))))

(forall (?a ?s1 ?s2)
	(=>	  (soo_precedes ?s1 ?s2 ?a)
		  (not (soo_precedes ?s2 ?s1 ?a))))

(forall (?a ?s1 ?s2 ?s3)
	(=>	  (and	(soo_precedes ?s1 ?s2 ?a)
			(soo_precedes ?s2 ?s3 ?a))
		  (soo_precedes ?s1 ?s3 ?a)))

(forall (?s ?a) (<=> (root_soo ?s ?a)
(and	(soo ?s ?a)
	(not (exists (?s1)
		(soo_precedes ?s1 ?s ?a))))))

(forall (?s ?a) (<=> (leaf_soo ?s ?a)
(and	(soo ?s ?a)
	(not (exists (?s1)
		(soo_precedes ?s ?s1 ?a))))))

(forall (?s1 ?s2 ?a) (<=> (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)
	(=>  (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)
        (<=>    (requires ?a ?r)
                (exists (?a1)
                        (and    (atomic ?a1)
                                (subactivity ?a1 ?a)
                                (requires ?a1 ?r)))))

(forall (?r ?a ?s)
	(<=>	(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)
	(=>  (prior (demand ?r ?a ?q) ?s)
		  (greater ?q zero)))

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

(forall (?r ?q ?s)
	(<=>	(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)
					(equal ?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)
					(equal ?q1 (plus ?q ?q2)))))))

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

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

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

(forall (?r1 ?r2 ?occ)
        (<=>    (holds (in_resource_set ?r1 ?r2) ?occ)
                (exists (?i)
                        (and    (set_member ?r1 ?i)
                                (holds (resource_set ?i ?r2) ?occ)))))

(forall (?r1 ?r2 ?occ)
        (<=>    (holds (resource_subset ?r1 ?r2) ?occ)
                (forall (?r ?i1 ?i2)
                   (=>  (and    (holds (resource_set ?i1 ?r1) ?occ)
                                (holds (resource_set ?i2 ?r2) ?occ)
                                (set_member ?r ?i1))
                        (set_member ?r ?i2)))))