(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 (?s1 ?s2 ?a) (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)) (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 (?s1 ?s2 ?a) (if (min_precedes ?s1 ?s2 ?a) (exists (?a1 ?a2) (and (subactivity ?a1 ?a) (atomic ?a2) (subactivity ?a1 ?a2) (occurrence_of ?s1 ?a2))))) (forall (?s1 ?s2 ?a) (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 (?s1 ?s2 ?a) (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 (?s1 ?s2 ?a) (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 (?s1 ?s2 ?a) (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))))) (forall (?a) (iff (global_ideal ?a) (forall (?a1 ?s1 ?s2) (if (and (subactivity ?a ?a1) (poss ?a ?s1) (poss ?a ?s2)) (poss_equiv ?a1 ?s1 ?s2))))) (forall (?a) (iff (global_nonideal ?a) (forall (?a1 ?s1 ?s2) (if (and (subactivity ?a ?a1) (not (poss ?a ?s1)) (not (poss ?a ?s2))) (poss_equiv ?a1 ?s1 ?s2))))) (forall (?a) (iff (global_filter ?a) (forall (?a1 ?s1 ?s2) (if (and (subactivity ?a1 ?a) (poss ?a ?s1) (poss ?a ?s2)) (poss_equiv ?a1 ?s1 ?s2))))) (forall (?a) (iff (global_nonfilter ?a) (forall (?a1 ?s1 ?s2) (if (and (subactivity ?a1 ?a) (not (poss ?a ?s1)) (not (poss ?a ?s2))) (poss_equiv ?a1 ?s1 ?s2))))) (forall (?a) (iff (reordered ?a) (forall (?occ1 ?occ2) (if (and (occurrence_of ?occ1 ?a) (occurrence_of ?occ2 ?a)) (branch_automorphic ?occ1 ?occ2))))) (forall (?a) (iff (nondet_reordered ?a) (forall (?occ1) (if (occurrence_of ?occ1 ?a) (exists (?occ2) (and (occurrence_of ?occ2 ?a) (not (same_grove ?occ1 ?occ2)) (branch_automorphic ?occ1 ?occ2))))))) (forall (?a) (iff (partial_reordered ?a) (exists (?occ1 ?occ2 ?occ3) (and (occurrence_of ?occ1 ?a) (occurrence_of ?occ2 ?a) (not (same_grove ?occ1 ?occ2)) (branch_automorphic ?occ1 ?occ2) (occurrence_of ?occ3 ?a) (same_grove ?occ1 ?occ3) (forall (?occ4) (if (and (occurrence_of ?occ4 ?a) (not (= ?occ2 ?occ4)) (same_grove ?occ2 ?occ4)) (not (branch_automorphic ?occ2 ?occ4)))))))) (forall (?a) (iff (unorderable ?a) (forall (?occ1 ?occ2) (if (and (occurrence_of ?occ1 ?a) (occurrence_of ?occ2 ?a) (not (same_grove ?occ1 ?occ2))) (not (branch_automorphic ?occ1 ?occ2)))))) (forall (?a) (iff (compacted ?a) (exists (?occ1) (and (occurrence_of ?occ1 ?a) (forall (?occ2) (if (and (occurrence_of ?occ2 ?a) (not (same_grove ?occ1 ?occ2))) (branch_homomorphic ?occ1 ?occ2))))))) (forall (?a) (iff (nondet_compacted ?a) (forall (?occ1) (if (occurrence_of ?occ1 ?a) (exists (?occ2) (and (occurrence_of ?occ2 ?a) (not (same_grove ?occ1 ?occ2)) (branch_homomorphic ?occ1 ?occ2))))))) (forall (?a) (iff (partial_compacted ?a) (exists (?occ1 ?occ2 ?occ3) (and (occurrence_of ?occ1 ?a) (occurrence_of ?occ2 ?a) (not (same_grove ?occ1 ?occ2)) (branch_homomorphic ?occ1 ?occ2) (occurrence_of ?occ3 ?a) (same_grove ?occ3 ?occ1) (forall (?occ4) (if (and (occurrence_of ?occ4 ?a) (not (= ?occ2 ?occ4)) (same_grove ?occ2 ?occ4)) (not (branch_homomorphic ?occ2 ?occ4)))))))) (forall (?a) (if (stiff ?a) (forall (?occ1 ?occ2) (if (and (occurrence_of ?occ1 ?a) (occurrence_of ?occ2 ?a) (not (same_grove ?occ1 ?occ2))) (not (branch_homomorphic ?occ1 ?occ2)))))) (forall (?a ?s) (iff (superpose ?a ?s) (forall (?a1) (if (and (subactivity ?a1 ?a) (poss ?a ?s)) (poss ?a1 ?s))))) (forall (?a ?s) (iff (assistance ?a ?s) (forall (?a1 ?a2) (if (and (subactivity ?a1 ?a) (subactivity ?a2 ?a) (poss ?a ?s)) (poss (conc ?a1 ?a2) ?s))))) (forall (?a ?s) (iff (team ?a ?s) (exists (?a1 ?a2) (and (subactivity ?a1 ?a) (subactivity ?a2 ?a) (poss ?a ?s) (not (poss (conc ?a1 ?a2) ?s)))))) (forall (?a ?s) (iff (ghost ?a ?s) (forall (?a1) (if (and (subactivity ?a1 ?a) (poss ?a1 ?s)) (poss ?a ?s))))) (forall (?a ?s) (iff (conflict ?a ?s) (forall (?a1 ?a2) (if (and (subactivity ?a1 ?a) (subactivity ?a2 ?a) (not (poss ?a1 ?s)) (poss (conc ?a1 ?a2) ?s)) (poss ?a ?s))))) (forall (?a ?s) (iff (dysfunction ?a ?s) (exists (?a1 ?a2) (and (subactivity ?a1 ?a) (subactivity ?a2 ?a) (not (poss ?a1 ?s)) (not (poss ?a ?s)) (poss (conc ?a1 ?a2) ?s))))) (forall (?s1 ?s2 ?a) (iff (live_branch ?s1 ?s2 ?a) (exists (?occ) (and (occurrence_of ?occ ?a) (= ?s1 (root_occ ?occ)) (min_precedes ?s1 ?s2 ?a))))) (forall (?s1 ?s2 ?a) (iff (embedded ?s1 ?s2 ?a) (exists (?s3) (and (root ?s2 ?a) (min_precedes ?s2 ?s3 ?a) (precedes ?s2 ?s1) (precedes ?s1 ?s3) (not (min_precedes ?s1 ?s3 ?a)))))) (forall (?s1 ?s2 ?a) (iff (dead_branch ?s1 ?s2 ?a) (exists (?a1 ?s3) (and (root ?s1 ?a) (min_precedes ?s1 ?s3 ?a) (not (leaf ?s3 ?a)) (= ?s2 (successor ?a1 ?s3)) (not (exists (?s4) (and (precedes ?s3 ?s4) (min_precedes ?s3 ?s4 ?a)))))))) (forall (?s1 ?s2 ?a) (iff (dead_occurrence ?s1 ?s2 ?a) (exists (?s3) (and (dead_branch ?s1 ?s3 ?a) (precedes ?s1 ?s2) (precedes ?s2 ?s3))))) (forall (?s1 ?s2 ?s3 ?a) (iff (embed_tree ?s1 ?s2 ?s3 ?a) (exists (?a1 ?a2) (and (subactivity ?a1 ?a) (subactivity ?a2 ?a) (occurrence_of ?s1 ?a1) (occurrence_of ?s2 ?a2) (or (live_branch ?s3 ?s1 ?a) (dead_branch ?s3 ?s1 ?a)) (or (live_branch ?s3 ?s2 ?a) (dead_branch ?s3 ?s2 ?a)))))) (forall (?s1 ?s2 ?s3 ?a) (iff (subocc_equiv ?s1 ?s2 ?s3 ?a) (and (embed_tree ?s1 ?s2 ?s3 ?a) (iff (min_precedes ?s3 ?s1 ?a) (min_precedes ?s3 ?s2 ?a))))) (forall (?occ) (iff (unrestricted ?occ) (forall (?a ?s1 ?s2 ?s3) (if (and (occurrence_of ?occ ?a) (= ?s3 (root_occ ?occ)) (embed_tree ?s1 ?s2 ?s3 ?a)) (subocc_equiv ?s1 ?s2 ?s3 ?a))))) (forall (?occ1 ?occ2) (iff (branch_homomorphic ?occ1 ?occ2) (and (same_grove ?occ1 ?occ2) (forall (?s1 ?a) (if (and (occurrence_of ?occ1 ?a) (subactivity_occurrence ?s1 ?occ1)) (exists (?s2) (and (subactivity_occurrence ?s2 ?occ2) (hom ?s1 ?s2 ?a)))))))) (forall (?occ) (iff (folded ?occ) (exists (?occ1) (and (same_grove ?occ1 ?occ) (forall (?occ2) (if (same_grove ?occ2 ?occ) (branch_homomorphic ?occ1 ?occ2))))))) (forall (?occ) (iff (nondet_folded ?occ) (forall (?occ1) (if (same_grove ?occ1 ?occ) (exists (?occ2) (and (same_grove ?occ2 ?occ) (not (= ?occ1 ?occ2)) (branch_homomorphic ?occ1 ?occ2))))))) (forall (?occ) (iff (partial_folded ?occ) (exists (?occ1 ?occ2 ?occ3) (and (same_grove ?occ1 ?occ) (same_grove ?occ2 ?occ) (not (= ?occ1 ?occ2)) (branch_homomorphic ?occ1 ?occ2) (same_grove ?occ3 ?occ) (forall (?occ4) (if (and (same_grove ?occ4 ?occ) (not (= ?occ3 ?occ4))) (not (branch_homomorphic ?occ3 ?occ4)))))))) (forall (?occ) (iff (rigid ?occ) (forall (?occ1 ?occ2) (if (and (same_grove ?occ1 ?occ) (same_grove ?occ2 ?occ) (not (= ?occ1 ?occ2))) (not (branch_homomorphic ?occ1 ?occ2)))))) (forall (?s1 ?s2 ?a) (iff (mono_tree ?s1 ?s2 ?a) (forall (?s3 ?s4 ?s5) (if (and (min_precedes ?s1 ?s3 ?a) (min_precedes ?s2 ?s4 ?a) (mono ?s3 ?s4 ?a) (min_precedes ?s3 ?s5 ?a)) (exists (?s6) (and (mono ?s5 ?s6 ?a) (min_precedes ?s4 ?s6 ?a))))))) (forall (?s1 ?s2 ?a) (iff (order_tree ?s1 ?s2 ?a) (and (mono_tree ?s1 ?s2 ?a) (forall (?s3 ?s4 ?s5 ?s6) (if (and (min_precedes ?s1 ?s3 ?a) (min_precedes ?s2 ?s4 ?a) (cousin ?s3 ?s4 ?a) (min_precedes ?s3 ?s5 ?a) (cousin ?s5 ?s6 ?a)) (iff (iso_occ ?s3 ?s5 ?a) (iso_occ ?s4 ?s6 ?a))))))) (forall (?occ1 ?occ2) (iff (root_automorphic ?occ1 ?occ2) (exists (?a ?s1 ?s2) (and (occurrence_of ?occ1 ?a) (occurrence_of ?occ2 ?a) (subactivity_occurrence ?s1 ?occ1) (subactivity_occurrence ?s2 ?occ2) (order_tree ?s1 ?s2 ?a) (order_tree ?s2 ?s1 ?a))))) (forall (?occ1) (iff (ordered ?occ1) (forall (?occ2) (if (same_grove ?occ1 ?occ2) (root_automorphic ?occ1 ?occ2))))) (forall (?occ1) (iff (nondet_ordered ?occ1) (forall (?occ2) (if (same_grove ?occ1 ?occ2) (exists (?occ3) (and (same_grove ?occ1 ?occ3) (not (= ?occ3 ?occ2)) (root_automorphic ?occ2 ?occ3))))))) (forall (?occ1) (iff (broken_ordered ?occ1) (exists (?occ2) (and (same_grove ?occ1 ?occ2) (not (= ?occ1 ?occ2)) (root_automorphic ?occ1 ?occ2) (forall (?occ3) (if (and (same_grove ?occ3 ?occ1) (not (= ?occ3 ?occ2))) (not (root_automorphic ?occ3 ?occ2)))))))) (forall (?occ1) (iff (unordered ?occ1) (forall (?occ2) (if (and (same_grove ?occ1 ?occ2) (not (= ?occ1 ?occ2))) (not (root_automorphic ?occ1 ?occ2)))))) (forall (?occ1 ?occ2) (iff (branch_monomorphic ?occ1 ?occ2) (forall (?s1 ?a) (if (and (occurrence_of ?occ1 ?a) (subactivity_occurrence ?s1 ?occ1)) (exists (?s2) (and (subactivity_occurrence ?s2 ?occ2) (mono ?s1 ?s2 ?a))))))) (forall (?occ1 ?occ2) (iff (branch_automorphic ?occ1 ?occ2) (and (branch_monomorphic ?occ1 ?occ2) (branch_monomorphic ?occ2 ?occ1)))) (forall (?occ) (iff (permuted ?occ) (forall (?occ1 ?occ2) (if (and (same_grove ?occ1 ?occ) (same_grove ?occ2 ?occ)) (branch_automorphic ?occ1 ?occ))))) (forall (?occ) (iff (nondet_permuted ?occ) (forall (?occ1) (if (same_grove ?occ1 ?occ) (exists (?occ2) (and (same_grove ?occ1 ?occ2) (not (= ?occ1 ?occ2)) (branch_automorphic ?occ1 ?occ2))))))) (forall (?occ) (iff (partial_permuted ?occ) (exists (?occ1 ?occ2 ?occ3) (and (same_grove ?occ1 ?occ) (same_grove ?occ2 ?occ) (not (= ?occ1 ?occ2)) (branch_automorphic ?occ1 ?occ2) (same_grove ?occ3 ?occ) (forall (?occ4) (if (and (same_grove ?occ3 ?occ4) (branch_automorphic ?occ3 ?occ4)) (= ?occ3 ?occ4))))))) (forall (?occ) (iff (simple ?occ) (forall (?occ1 ?occ2) (if (and (same_grove ?occ1 ?occ) (same_grove ?occ2 ?occ) (branch_automorphic ?occ1 ?occ2)) (= ?occ1 ?occ2))))) (forall (?s1 ?s2 ?s3 ?s4 ?a) (iff (branch_mono ?s1 ?s2 ?s3 ?s4 ?a) (forall (?s5 ?s6) (if (and (min_precedes ?s1 ?s5 ?a) (min_precedes ?s6 ?s2 ?a) (next_subocc ?s5 ?s6 ?a)) (exists (?s7 ?s8) (and (min_precedes ?s3 ?s7 ?a) (min_precedes ?s8 ?s4 ?a) (next_subocc ?s7 ?s8 ?a) (iso_occ ?s5 ?s7 ?a) (iso_occ ?s6 ?s8 ?a))))))) (forall (?s ?occ) (iff (reptree ?s ?occ) (forall (?s1 ?a) (if (and (occurrence_of ?occ ?a) (subactivity_occurrence ?s1 ?occ)) (exists (?s2 ?s3 ?s4 ?occ1) (and (same_tree ?occ ?occ1) (leaf_occ ?s2 ?occ1) (min_precedes ?s3 ?s1 ?a) (min_precedes ?s1 ?s4 ?a) (branch_mono ?s3 ?s4 ?s ?s2 ?a))))))) (forall (?occ) (iff (repetitive ?occ) (exists (?s ?occ2) (and (same_tree ?occ ?occ2) (subactivity_occurrence ?s ?occ2) (forall (?occ1) (if (same_tree ?occ ?occ1) (and (reptree ?s ?occ1) (not (= ?s (root_occ ?occ1)))))))))) (forall (?occ) (iff (nondet_repetitive ?occ) (forall (?occ1) (if (same_tree ?occ ?occ1) (exists (?s ?occ2) (and (same_tree ?occ ?occ2) (subactivity_occurrence ?s ?occ2) (reptree ?s ?occ1) (not (= ?s (root_occ ?occ1))))))))) (forall (?occ) (iff (partial_repetitive ?occ) (and (exists (?occ1 ?occ2 ?s) (and (same_tree ?occ ?occ1) (same_tree ?occ ?occ2) (subactivity_occurrence ?s ?occ2) (rep_tree ?s ?occ1) (not (= ?s (root_occ ?occ1))))) (exists (?occ1) (forall (?s1) (if (reptree ?s1 ?occ1) (= ?s1 (root_occ ?occ1)))))))) (forall (?occ) (iff (amorphous ?occ) (forall (?occ1 ?s) (if (and (same_tree ?occ1 ?occ) (reptree ?s ?occ1)) (= ?s (root_occ ?occ1)))))) (forall (?occ) (iff (fused ?occ) (forall (?s1 ?s2 ?s3) (if (and (= ?s1 (root_occ ?occ)) (subactivity_occurrence ?s2 ?occ) (precedes ?s1 ?s3) (precedes ?s3 ?s2)) (subactivity_occurrence ?s3 ?occ))))) (forall (?occ) (iff (embed_occ ?occ) (forall (?a ?s ?s1 ?s2 ?s3) (if (and (occurrence_of ?occ ?a) (= ?s (root_occ ?occ)) (next_subocc ?s1 ?s2 ?occ) (precedes ?s1 ?s3) (precedes ?s3 ?s2)) (exists (?s4 ?s5 ?s6) (and (precedes ?s4 ?s5) (precedes ?s5 ?s6) (iso_occ ?s4 ?s1 ?a) (iso_occ ?s5 ?s3 ?a) (iso_occ ?s6 ?s3 ?a) (dead_branch ?s1 ?s4 ?a) (dead_branch ?s1 ?s6 ?a))))))) (forall (?occ) (iff (free ?occ) (exists (?occ1 ?occ2) (and (same_tree ?occ ?occ1) (same_tree ?occ ?occ2) (not (fused ?occ1)) (fused ?occ2))))) (forall (?occ) (iff (assisted ?occ) (forall (?occ1) (if (same_tree ?occ ?occ1) (not (fused ?occ1)))))) (forall (?occ) (iff (helpless ?occ) (forall (?s1 ?s2) (if (next_subocc ?s1 ?s2 ?occ) (exists (?s3) (and (precedes ?s1 ?s3) (precedes ?s3 ?s2) (not (subactivity_occurrence ?s3 ?occ)))))))) (forall (?occ) (iff (unbound ?occ) (forall (?occ1) (if (same_tree ?occ1 ?occ) (not (embed_occ ?occ1)))))) (forall (?occ) (iff (bound ?occ) (exists (?occ1 ?occ2) (and (same_tree ?occ1 ?occ) (not (embed_occ ?occ1)) (same_tree ?occ2 ?occ) (embed_occ ?occ2))))) (forall (?occ) (iff (strict ?occ) (forall (?occ1) (if (same_tree ?occ ?occ1) (fused ?occ1))))) (forall (?s1 ?s2 ?a) (iff (subtree_embed ?s1 ?s2 ?a) (forall (?s3) (if (min_precedes ?s1 ?s3 ?a) (exists (?s4) (and (min_precedes ?s2 ?s4 ?a) (iso_occ ?s4 ?s3 ?a))))))) (forall (?a) (iff (multiple_outcome ?a) (forall (?s1 ?s2) (if (and (root ?s1 ?a) (root ?s2 ?a)) (or (subtree_embed ?s1 ?s2 ?a) (subtree_embed ?s2 ?s1 ?a)))))) (forall (?a) (iff (weak_outcome ?a) (exists (?s1) (and (root ?s1 ?a) (forall (?s2) (if (root ?s2 ?a) (subtree_embed ?s2 ?s1 ?a))))))) (forall (?a) (iff (nondet_outcome ?a) (exists (?s1 ?s2 ?s3) (and (root ?s1 ?a) (root ?s2 ?a) (subtree_embed ?s2 ?s1 ?a) (root ?s3 ?a) (forall (?s4) (if (root ?s4 ?a) (not (or (subtree_embed ?s3 ?s4 ?a) (subtree_embed ?s4 ?s3 ?a))))))))) (forall (?a) (iff (imiscible ?a) (forall (?s1 ?s2) (if (and (root ?s1 ?a) (root ?s2 ?a)) (not (or (subtree_embed ?s1 ?s2 ?a) (subtree_embed ?s2 ?s1 ?a))))))) (forall (?a) (iff (treeordered ?a) (forall (?occ1 ?occ2) (if (and (occurrence_of ?occ1 ?a) (occurrence_of ?occ2 ?a) (not (same_grove ?occ1 ?occ2))) (root_automorphic ?occ1 ?occ2))))) (forall (?a) (iff (nondet_treeordered ?a) (forall (?occ1) (if (occurrence_of ?occ1 ?a) (exists (?occ2) (and (occurence_of ?occ2 ?a) (not (same_grove ?occ1 ?occ2)) (root_automorphic ?occ1 ?occ2))))))) (forall (?a) (iff (partial_treeordered ?a) (exists (?occ1 ?occ2) (and (occurrence_of ?occ1 ?a) (occurrence_of ?occ2 ?a) (not (same_grove ?occ1 ?occ2)) (root_automorphic ?occ1 ?occ2) (forall (?occ3) (if (and (occurrence_of ?occ3 ?a) (not (same_grove ?occ3 ?occ2))) (not (root_automorphic ?occ3 ?occ2)))))))) (forall (?a) (iff (scrambled ?a) (forall (?occ1 ?occ2) (if (and (occurrence_of ?occ1 ?a) (occurrence_of ?occ2 ?a) (not (same_grove ?occ1 ?occ2))) (not (root_automorphic ?occ1 ?occ2)))))) (forall (?a ?s) (iff (natural ?a ?s) (forall (?a1) (if (and (poss ?a ?s) (poss ?a1 ?s)) (subactivity ?a ?a1))))) (forall (?a ?s) (iff (artificial ?a ?s) (forall (?a1) (if (and (poss ?a ?s) (poss ?a1 ?s) (not (subactivity ?a1 ?a))) (poss (conc ?a ?a1) ?s))))) (forall (?a ?s) (iff (performed ?a ?s) (exists (?a1 ?a2) (and (subactivity ?a1 ?a) (subactivity ?a2 ?a) (poss ?a ?s) (not (poss (conc ?a1 ?a2) ?s)))))) (forall (?a ?s) (iff (up_ghost ?a ?s) (forall (?a1) (if (and (poss ?a1 ?s) (subactivity ?a ?a1)) (poss ?a ?s))))) (forall (?a ?s) (iff (up_conflict ?a ?s) (forall (?a1) (if (poss (conc ?a ?a1) ?s) (or (poss ?a ?s) (poss ?a1 ?s) (subactivity ?a ?a1)))))) (forall (?a ?s) (iff (quark ?a ?s) (exists (?a1) (and (atomic ?a1) (subactivity ?a ?a1) (poss ?a1 ?s) (not (poss ?a ?s)))))) (forall (?f ?occ) (iff (achieved ?f ?occ) (and (holds ?f ?occ) (not (prior ?f ?occ))))) (forall (?f ?occ) (iff (falsified ?f ?occ) (and (not (holds ?f ?occ)) (prior ?f ?occ)))) (forall (?f) (iff (irreversible ?f) (not (exists (?occ) (falsified ?f ?occ))))) (forall (?f) (iff (unachievable ?f) (not (exists (?occ) (achieved ?f ?occ))))) (forall (?f) (iff (bounded ?f) (exists (?occ1 ?occ2) (and (achieved ?f ?occ1) (falsified ?f ?occ2))))) (forall (?a ?a1 ?s) (iff (preserved_effects ?a ?a1 ?s) (forall (?a2 ?f) (if (subactivity ?a ?a2) (iff (holds ?f (successor ?a2 ?s)) (holds ?f (successor (conc ?a2 ?a1) ?s))))))) (forall (?a ?s) (iff (nonclobbering ?a ?s) (forall (?a1) (if (atomic ?a1) (preserved_effects ?a ?a1 ?s))))) (forall (?a ?s) (iff (clobbering ?a ?s) (exists (?a1) (and (atomic ?a1) (not (preserved_effects ?a ?a1 ?s)))))) (forall (?a ?s) (iff (meddling ?a ?s) (forall (?a1) (if (atomic ?a1) (not (preserved_effects ?a ?a1 ?s)))))) (forall (?a) (iff (global_clobber ?a) (forall (?a1) (if (atomic ?a1) (forall (?s1 ?s2) (iff (preserved_effects ?a ?a1 ?s1) (preserved_effects ?a ?a1 ?s2))))))) (forall (?occ ?a) (iff (profile ?occ ?a) (exists (?occ1 ?occ2 ?a1) (and (occurrence_of ?occ1 ?a) (occurrence_of ?occ ?a1) (occurrence_of ?occ2 ?a1) (= ?occ2 (root_occ ?occ1)) (forall (?occ3 ?a2) (if (and (subactivity_occurrence ?occ3 ?occ1) (occurrence_of ?occ3 ?a2)) (exists (?occ4) (and (occurrence_of ?occ4 ?a2) (precedes ?occ ?occ4))))))))) (forall (?a ?occ1 ?occ2) (iff (root_equiv ?a ?occ1 ?occ2) (if (and (profile ?occ1 ?a) (profile ?occ2 ?a)) (iff (root ?occ1 ?a) (root ?occ2 ?a))))) (forall (?a) (iff (universal ?a) (forall (?occ1 ?occ2) (if (and (profile ?occ1 ?a) (profile ?occ2 ?a)) (root_equiv ?a ?occ1 ?occ2))))) (forall (?a) (iff (restricted ?a) (and (exists (?a1) (forall (?occ1 ?occ2) (if (and (occurrence_of ?occ1 ?a1) (occurrence_of ?occ2 ?a1) (profile ?occ1 ?a) (profile ?occ2 ?a)) (root_equiv ?a ?occ1 ?occ2)))) (exists (?a2 ?occ3 ?occ4) (and (occurrence_of ?occ3 ?a2) (occurrence_of ?occ4 ?a2) (profile ?occ3 ?a) (profile ?occ4 ?a) (not (root_equiv ?a ?occ3 ?occ4))))))) (forall (?a) (iff (local ?a) (forall (?a1) (exists (?occ1 ?occ2) (and (occurrence_of ?occ1 ?a1) (occurrence_of ?occ2 ?a1) (profile ?occ1 ?a) (profile ?occ2 ?a) (not (root_equiv ?a ?occ1 ?occ2))))))) (forall (?a) (iff (state_ideal ?a) (forall (?a1 ?s1 ?s2) (if (and (subactivity ?a ?a1) (poss ?a ?s1) (poss ?a ?s2) (state_equiv ?s1 ?s2)) (poss_equiv ?a1 ?s1 ?s2))))) (forall (?a) (iff (partial_state_ideal ?a) (and (exists (?s1) (forall (?s2 ?a1) (if (and (subactivity ?a ?a1) (poss ?a ?s1) (poss ?a ?s2) (state_equiv ?s1 ?s2)) (poss_equiv ?a1 ?s1 ?s2)))) (exists (?a2 ?s3 ?s4) (and (subactivity ?a ?a2) (poss ?a ?s3) (poss ?a ?s4) (state_equiv ?s3 ?s4) (not (poss_equiv ?a2 ?s3 ?s4))))))) (forall (?a) (iff (rigid_state_ideal ?a) (forall (?s1) (exists (?a1 ?s2) (and (state_equiv ?s1 ?s2) (subactivity ?a ?a1) (poss ?a ?s1) (poss ?a ?s2) (not (poss_equiv ?a1 ?s1 ?s2))))))) (forall (?a) (iff (time_ideal ?a) (forall (?a1 ?s1 ?s2) (if (and (subactivity ?a ?a1) (poss ?a ?s1) (poss ?a ?s2) (begin_equiv ?s1 ?s2)) (poss_equiv ?a1 ?s1 ?s2))))) (forall (?a) (iff (partial_time_ideal ?a) (and (exists (?s1 ?a1) (forall (?s2) (if (and (subactivity ?a ?a1) (poss ?a ?s1) (poss ?a ?s2) (begin_equiv ?s1 ?s2)) (poss_equiv ?a1 ?s1 ?s2)))) (exists (?a2 ?s3 ?s4) (and (subactivity ?a ?a2) (poss ?a ?s3) (poss ?a ?s4) (begin_equiv ?s3 ?s4) (not (poss_equiv ?a2 ?s3 ?s4))))))) (forall (?a) (iff (rigid_time_ideal ?a) (forall (?s1) (exists (?a1 ?s2) (and (begin_equiv ?s1 ?s2) (poss ?a ?s1) (poss ?a ?s2) (not (poss_equiv ?a1 ?s1 ?s2))))))) (forall (?a) (iff (state_nonideal ?a) (forall (?a1 ?s1 ?s2) (if (and (subactivity ?a ?a1) (not (poss ?a ?s1)) (not (poss ?a ?s2)) (state_equiv ?s1 ?s2)) (poss_equiv ?a1 ?s1 ?s2))))) (forall (?a) (iff (partial_state_nonideal ?a) (and (exists (?s1) (forall (?s2 ?a1) (if (and (subactivity ?a ?a1) (not (poss ?a ?s1)) (not (poss ?a ?s2)) (state_equiv ?s1 ?s2)) (poss_equiv ?a1 ?s1 ?s2)))) (exists (?a2 ?s3 ?s4) (and (subactivity ?a ?a2) (not (poss ?a ?s3)) (not (poss ?a ?s4)) (state_equiv ?s3 ?s4) (not (poss_equiv ?a2 ?s3 ?s4))))))) (forall (?a) (iff (rigid_state_nonideal ?a) (forall (?s1) (exists (?a1 ?s2) (and (state_equiv ?s1 ?s2) (not (poss ?a ?s1)) (not (poss ?a ?s2)) (not (poss_equiv ?a1 ?s1 ?s2))))))) (forall (?a) (iff (time_nonideal ?a) (forall (?a1 ?s1 ?s2) (if (and (subactivity ?a ?a1) (not (poss ?a ?s1)) (not (poss ?a ?s2)) (begin_equiv ?s1 ?s2)) (poss_equiv ?a1 ?s1 ?s2))))) (forall (?a) (iff (partial_time_nonideal ?a) (and (exists (?s1) (forall (?s2 ?a1) (if (and (subactivity ?a ?a1) (not (poss ?a ?s1)) (not (poss ?a ?s2)) (begin_equiv ?s1 ?s2)) (poss_equiv ?a1 ?s1 ?s2)))) (exists (?a2 ?s3 ?s4) (and (subactivity ?a ?a2) (not (poss ?a ?s3)) (not (poss ?a ?s4)) (begin_equiv ?s3 ?s4) (not (poss_equiv ?a2 ?s3 ?s4))))))) (forall (?a) (iff (rigid_time_nonideal ?a) (forall (?s1) (exists (?a1 ?s2) (and (begin_equiv ?s1 ?s2) (subactivity ?a ?a1) (not (poss ?a ?s1)) (not (poss ?a ?s2)) (not (poss_equiv ?a1 ?s1 ?s2))))))) (forall (?a ?s1 ?s2) (iff (effects_equiv ?a ?s1 ?s2) (and (occurrence_of ?s1 ?a) (occurrence_of ?s2 ?a) (forall (?f) (iff (holds ?f ?s1) (holds ?f ?s2)))))) (forall (?a) (iff (context_free ?a) (forall (?s1 ?s2) (if (and (occurrence_of ?s1 ?a) (occurrence_of ?s2 ?a)) (effects_equiv ?a ?s1 ?s2))))) (forall (?a) (iff (null ?a) (forall (?s) (if (occurrence_of ?s ?a) (forall (?f) (iff (holds ?f ?s) (prior ?f ?s))))))) (forall (?a) (iff (historical ?a) (forall (?s1 ?s2) (if (and (occurrence_of ?s1 ?a) (occurrence_of ?s2 ?a) (state_equiv ?s1 ?s2) (begin_equiv ?s1 ?s2) (tree_equiv ?s1 ?s2)) (legal_equiv ?s1 ?s2))))) (forall (?a) (iff (possibly_historical ?a) (exists (?s1) (and (occurrence_of ?s1 ?a) (forall (?s2) (if (and (occurrence_of ?s2 ?a) (state_equiv ?s1 ?s2) (begin_equiv ?s1 ?s2) (tree_equiv ?s1 ?s2)) (legal_equiv ?s1 ?s2))))))) (forall (?a) (iff (nonhistorical ?a) (forall (?s1) (if (occurrence_of ?s1 ?a) (exists (?s2) (and (occurrence_of ?s2 ?a) (state_equiv ?s1 ?s2) (begin_equiv ?s1 ?s2) (tree_equiv ?s1 ?s2) (not (legal_equiv ?s1 ?s2)))))))) (forall (?a ?a1 ?s) (iff (preserved_filter ?a ?a1 ?s) (forall (?a2) (if (subactivity ?a ?a2) (iff (poss ?a2 ?s) (poss (conc ?a2 ?a1) ?s)))))) (forall (?a ?s) (iff (noninterfering ?a ?s) (forall (?a1) (if (atomic ?a1) (preserved_filter ?a ?a1 ?s))))) (forall (?a ?s) (iff (interfering ?a ?s) (exists (?a1) (and (atomic ?a1) (not (preserved_filter ?a ?a1 ?s)))))) (forall (?a ?s) (iff (imperial ?a ?s) (forall (?a1) (if (atomic ?a1) (not (preserved_filter ?a ?a1 ?s)))))) (forall (?a) (iff (global_interfere ?a) (forall (?a1) (if (atomic ?a1) (forall (?s1 ?s2) (iff (preserved_filter ?a ?a1 ?s1) (preserved_filter ?a ?a1 ?s2))))))) (forall (?a) (iff (conditional_launch ?a) (forall (?occ1 ?occ2) (if (and (profile ?occ1 ?a) (profile ?occ2 ?a) (state_equiv ?occ1 ?occ2) (begin_equiv ?occ1 ?occ2)) (root_equiv ?a ?occ1 ?occ2))))) (forall (?a) (iff (partial_conditional_launch ?a) (and (exists (?occ1) (forall (?occ2) (if (and (profile ?occ1 ?a) (profile ?occ2 ?a) (state_equiv ?occ1 ?occ2) (begin_equiv ?occ1 ?occ2)) (root_equiv ?a ?occ1 ?occ2)))) (exists (?occ3 ?occ4) (and (profile ?occ3 ?a) (profile ?occ4 ?a) (state_equiv ?occ3 ?occ4) (begin_equiv ?occ3 ?occ4) (not (root_equiv ?a ?occ3 ?occ4))))))) (forall (?a) (iff (unconditional_launch ?a) (forall (?occ1) (if (profile ?occ1 ?a) (exists (?occ2) (and (profile ?occ2 ?a) (state_equiv ?occ1 ?occ2) (begin_equiv ?occ1 ?occ2) (not (root_equiv ?a ?occ1 ?occ2)))))))) (forall (?a) (iff (mixed_precond ?a) (forall (?s1 ?s2) (if (and (state_equiv ?s1 ?s2) (begin_equiv ?s1 ?s2)) (poss_equiv ?a ?s1 ?s2))))) (forall (?a) (iff (partial_mixed ?a) (and (exists (?s1) (forall (?s2) (if (and (state_equiv ?s1 ?s2) (begin_equiv ?s1 ?s2)) (poss_equiv ?a ?s1 ?s2)))) (exists (?s3 ?s4) (and (state_equiv ?s3 ?s4) (begin_equiv ?s3 ?s4) (not (poss_equiv ?a ?s3 ?s4))))))) (forall (?a) (iff (rigid_mixed ?a) (forall (?s1) (exists (?s2) (and (state_equiv ?s1 ?s2) (begin_equiv ?s1 ?s2) (not (poss_equiv ?a ?s1 ?s2))))))) (forall (?a) (iff (mixed_conditional ?a) (forall (?occ1 ?occ2) (if (and (root ?occ1 ?a) (root ?occ2 ?a) (begin_equiv ?occ1 ?occ2) (state_equiv ?occ1 ?occ2)) (min_equiv ?occ1 ?occ2 ?a))))) (forall (?a) (iff (partial_mixed_conditional ?a) (and (exists (?occ1) (forall (?occ2) (if (and (root ?occ1 ?a) (root ?occ2 ?a) (begin_equiv ?occ1 ?occ2) (state_equiv ?occ1 ?occ2)) (min_equiv ?occ1 ?occ2 ?a)))) (exists (?occ3 ?occ4) (and (root ?occ3 ?a) (root ?occ4 ?a) (begin_equiv ?occ3 ?occ4) (state_equiv ?occ3 ?occ4) (not (min_equiv ?occ3 ?occ4 ?a))))))) (forall (?a) (iff (rigid_mixed_conditional ?a) (forall (?occ1) (exists (?occ2) (and (root ?occ1 ?a) (root ?occ2 ?a) (begin_equiv ?occ1 ?occ2) (state_equiv ?occ1 ?occ2) (not (min_equiv ?occ1 ?occ2 ?a))))))) (forall (?a) (iff (occ_effects ?a) (forall (?s1 ?s2) (if (and (occurrence_of ?s1 ?a) (occurrence_of ?s2 ?a) (tree_equiv ?s1 ?s2)) (effects_equiv ?a ?s1 ?s2))))) (forall (?a) (iff (occ_depend_effects ?a) (exists (?s1) (and (occurrence_of ?s1 ?a) (forall (?s2) (if (and (occurrence_of ?s2 ?a) (tree_equiv ?s1 ?s2)) (effects_equiv ?a ?s1 ?s2))))))) (forall (?a) (iff (nonocc_effects ?a) (forall (?s1) (if (occurrence_of ?s1 ?a) (exists (?s2) (and (occurrence_of ?s2 ?a) (tree_equiv ?s1 ?s2) (not (effects_equiv ?a ?s1 ?s2)))))))) (forall (?a ?s1 ?s2) (iff (tree_equiv (successor ?a ?s1) (successor ?a ?s2)) (and (legal_equiv ?s1 ?s2) (or (tree_equiv ?s1 ?s2) (initial ?s1) (initial ?s2))))) (forall (?a) (iff (occurrence_constrained ?a) (forall (?s1 ?s2) (if (and (occurrence_of ?s1 ?a) (occurrence_of ?s2 ?a) (tree_equiv ?s1 ?s2)) (legal_equiv ?s1 ?s2))))) (forall (?a) (iff (occurrence_dependent ?a) (exists (?s1) (and (occurrence_of ?s1 ?a) (forall (?s2) (if (and (occurrence_of ?s2 ?a) (tree_equiv ?s1 ?s2)) (legal_equiv ?s1 ?s2))))))) (forall (?a) (iff (occurrence_independent ?a) (forall (?s1) (if (occurrence_of ?s1 ?a) (exists (?s2) (and (occurrence_of ?s2 ?a) (tree_equiv ?s1 ?s2) (not (legal_equiv ?s1 ?s2)))))))) (forall (?a) (iff (periodic ?a) (forall (?s1 ?s2) (if (and (occurrence_of ?s1 ?a) (occurrence_of ?s2 ?a) (begin_equiv ?s1 ?s2) (tree_equiv ?s1 ?s2)) (legal_equiv ?s1 ?s2))))) (forall (?a) (iff (intermittent ?a) (exists (?s1) (and (occurrence_of ?s1 ?a) (forall (?s2) (if (and (occurrence_of ?s2 ?a) (begin_equiv ?s1 ?s2) (tree_equiv ?s1 ?s2)) (legal_equiv ?s1 ?s2))))))) (forall (?a) (iff (aperiodic ?a) (forall (?s1) (if (occurrence_of ?s1 ?a) (exists (?s2) (and (occurrence_of ?s2 ?a) (begin_equiv ?s1 ?s2) (tree_equiv ?s1 ?s2) (not (legal_equiv ?s1 ?s2)))))))) (forall (?s) (iff (plan ?s) (forall (?a ?s1 ?s2) (if (and (root ?s ?a) (embed_tree ?s1 ?s2 ?s ?a) (state_equiv ?s1 ?s2)) (subocc_equiv ?s1 ?s2 ?s ?a))))) (forall (?s) (iff (nondet_plan ?s) (exists (?a ?s1 ?s3 ?s4) (and (root ?s ?a) (forall (?s2) (if (and (embed_tree ?s1 ?s2 ?s ?a) (state_equiv ?s1 ?s2)) (subocc_equiv ?s1 ?s2 ?s ?a))) (state_equiv ?s3 ?s4) (embed_tree ?s3 ?s4 ?s ?a) (not (subocc_equiv ?s3 ?s4 ?s ?a)))))) (forall (?s) (iff (unplan ?s) (forall (?s1 ?a) (if (root ?s ?a) (exists (?s2) (and (embed_tree ?s1 ?s2 ?s ?a) (state_equiv ?s1 ?s2) (not (subocc_equiv ?s1 ?s2 ?s ?a)))))))) (forall (?s1 ?s2) (iff (legal_equiv ?s1 ?s2) (iff (legal ?s1) (legal ?s2)))) (forall (?a ?s1 ?s2) (iff (poss_equiv ?a ?s1 ?s2) (if (and (occurrence_of ?s1 ?a) (occurrence_of ?s2 ?a)) (legal_equiv ?s1 ?s2)))) (forall (?a) (iff (unconstrained ?a) (forall (?s1 ?s2) (if (and (activity_occurrence ?s1) (activity_occurrence ?s2)) (poss_equiv ?a ?s1 ?s2))))) (forall (?a) (iff (partial_constrained ?a) (and (exists (?a1) (forall (?s1 ?s2) (if (and (occurrence_of ?s1 ?a1) (occurrence_of ?s2 ?a1)) (poss_equiv ?a ?s1 ?s2)))) (exists (?a2 ?s3 ?s4) (and (occurrence_of ?s3 ?a2) (occurrence_of ?s4 ?a2) (not (poss_equiv ?a ?s3 ?s4))))))) (forall (?a) (iff (constrained ?a) (forall (?a1) (exists (?s1 ?s2) (and (occurrence_of ?s1 ?a1) (occurrence_of ?s2 ?a1) (not (poss_equiv ?a ?s1 ?s2))))))) (forall (?a) (iff (preventable ?a) (forall (?s1 ?s2) (if (and (occurrence_of ?s1 ?a) (occurrence_of ?s2 ?a) (state_equiv ?s1 ?s2) (tree_equiv ?s1 ?s2)) (legal_equiv ?s1 ?s2))))) (forall (?a) (iff (possibly_preventable ?a) (exists (?s1) (and (occurrence_of ?s1 ?a) (forall (?s2) (if (and (occurrence_of ?s2 ?a) (state_equiv ?s1 ?s2) (tree_equiv ?s1 ?s2)) (legal_equiv ?s1 ?s2))))))) (forall (?a) (iff (unpreventable ?a) (forall (?s1) (if (occurrence_of ?s1 ?a) (exists (?s2) (and (occurrence_of ?s2 ?a) (state_equiv ?s1 ?s2) (tree_equiv ?s1 ?s2) (not (legal_equiv ?s1 ?s2)))))))) (forall (?a) (iff (quantum ?a) (forall (?s1 ?s2) (if (and (occurrence_of ?s1 ?a) (occurrence_of ?s2 ?a) (state_equiv ?s1 ?s2) (tree_equiv ?s1 ?s2)) (effects_equiv ?a ?s1 ?s2))))) (forall (?a) (iff (semiclassical ?a) (exists (?s1) (and (occurrence_of ?s1 ?a) (forall (?s2) (if (and (occurrence_of ?s2 ?a) (state_equiv ?s1 ?s2) (tree_equiv ?s1 ?s2)) (effects_equiv ?a ?s1 ?s2))))))) (forall (?a) (iff (classical ?a) (forall (?s1) (if (occurrence_of ?s1 ?a) (exists (?s2) (and (occurrence_of ?s2 ?a) (state_equiv ?s1 ?s2) (tree_equiv ?s1 ?s2) (not (effects_equiv ?a ?s1 ?s2)))))))) (forall (?a) (iff (relativistic ?a) (forall (?s1 ?s2) (if (and (occurrence_of ?s1 ?a) (occurrence_of ?s2 ?a) (begin_equiv ?s1 ?s2) (tree_equiv ?s1 ?s2)) (effects_equiv ?a ?s1 ?s2))))) (forall (?a) (iff (seminewton ?a) (exists (?s1) (and (occurrence_of ?s1 ?a) (forall (?s2) (if (and (occurrence_of ?s2 ?a) (begin_equiv ?s1 ?s2) (tree_equiv ?s1 ?s2)) (effects_equiv ?a ?s1 ?s2))))))) (forall (?a) (iff (newtonian ?a) (forall (?s1) (if (occurrence_of ?s1 ?a) (exists (?s2) (and (occurrence_of ?s2 ?a) (begin_equiv ?s1 ?s2) (tree_equiv ?s1 ?s2) (not (effects_equiv ?a ?s1 ?s2)))))))) (forall (?occ) (iff (spread ?occ) (forall (?a ?s1 ?s2 ?s3) (if (and (occurrence_of ?occ ?a) (= ?s3 (root_occ ?occ)) (subactivity_occurrence ?s1 ?occ) (iso_occ ?s1 ?s2 ?a) (embed_tree ?s1 ?s2 ?s3 ?a) (begin_equiv ?s1 ?s2)) (subocc_equiv ?s1 ?s2 ?s3 ?a))))) (forall (?occ) (iff (partial_spread ?occ) (exists (?a ?s ?s1 ?s3 ?s4) (and (occurrence_of ?occ ?a) (= ?s (root_occ ?occ)) (subactivity_occurrence ?s1 ?occ) (forall (?s2) (if (and (iso_occ ?s1 ?s2 ?a) (embed_tree ?s1 ?s2 ?s ?a) (begin_equiv ?s1 ?s2)) (subocc_equiv ?s1 ?s2 ?s ?a))) (subactivity_occurrence ?s3 ?occ) (iso_occ ?s3 ?s4 ?a) (begin_equiv ?s3 ?s4) (embed_tree ?s3 ?s4 ?s ?a) (not (subocc_equiv ?s3 ?s4 ?s ?a)))))) (forall (?occ) (iff (tight ?occ) (forall (?s ?s1 ?a) (if (and (occurrence_of ?occ ?a) (= ?s (root_occ ?occ)) (subactivity_occurrence ?s1 ?occ)) (exists (?s2) (and (iso_occ ?s1 ?s2 ?a) (embed_tree ?s1 ?s2 ?s ?a) (begin_equiv ?s1 ?s2) (not (subocc_equiv ?s1 ?s2 ?s ?a)))))))) (forall (?a) (iff (trigger ?a) (forall (?occ1 ?occ2) (if (and (profile ?occ1 ?a) (profile ?occ2 ?a) (state_equiv ?occ1 ?occ2)) (root_equiv ?a ?occ1 ?occ2))))) (forall (?a) (iff (partial_trigger ?a) (and (exists (?occ1) (forall (?occ2) (if (and (profile ?occ1 ?a) (profile ?occ2 ?a) (state_equiv ?occ1 ?occ2)) (root_equiv ?a ?occ1 ?occ2)))) (exists (?occ3 ?occ4) (and (profile ?occ3 ?a) (profile ?occ4 ?a) (state_equiv ?occ3 ?occ4) (not (root_equiv ?a ?occ3 ?occ4))))))) (forall (?a) (iff (nontrigger ?a) (forall (?occ1) (if (profile ?occ1 ?a) (exists (?occ2) (and (profile ?occ2 ?a) (state_equiv ?occ1 ?occ2) (not (root_equiv ?a ?occ1 ?occ2)))))))) (forall (?a) (iff (markov_effects ?a) (forall (?s1 ?s2) (if (and (occurrence_of ?s1 ?a) (occurrence_of ?s2 ?a) (state_equiv ?s1 ?s2)) (effects_equiv ?a ?s1 ?s2))))) (forall (?a) (iff (partial_state_effects ?a) (and (exists (?s1) (forall (?s2) (if (state_equiv ?s1 ?s2) (effects_equiv ?a ?s1 ?s2)))) (exists (?s3 ?s4) (and (state_equiv ?s3 ?s4) (not (effects_equiv ?a ?s3 ?s4))))))) (forall (?a) (iff (rigid_state_effects ?a) (forall (?s1) (exists (?s2) (and (state_equiv ?s1 ?s2) (not (effects_equiv ?a ?s1 ?s2))))))) (forall (?s1 ?s2) (iff (state_equiv ?s1 ?s2) (forall (?f) (iff (prior ?f ?s1) (prior ?f ?s2))))) (forall (?a) (iff (markov_precond ?a) (forall (?s1 ?s2) (if (state_equiv ?s1 ?s2) (poss_equiv ?a ?s1 ?s2))))) (forall (?a) (iff (partial_state ?a) (and (exists (?s1) (forall (?s2) (if (state_equiv ?s1 ?s2) (poss_equiv ?a ?s1 ?s2)))) (exists (?s3 ?s4) (and (state_equiv ?s3 ?s4) (not (poss_equiv ?a ?s3 ?s4))))))) (forall (?a) (iff (rigid_state ?a) (forall (?s1) (exists (?s2) (and (state_equiv ?s1 ?s2) (not (poss_equiv ?a ?s1 ?s2))))))) (forall (?a) (iff (conditional ?a) (forall (?occ1 ?occ2) (if (and (root ?occ1 ?a) (root ?occ2 ?a) (state_equiv ?occ1 ?occ2)) (min_equiv ?occ1 ?occ2 ?a))))) (forall (?a) (iff (partial_conditional ?a) (and (exists (?occ1) (forall (?occ2) (if (and (root ?occ1 ?a) (root ?occ2 ?a) (state_equiv ?occ1 ?occ2)) (min_equiv ?occ1 ?occ2 ?a)))) (exists (?occ3 ?occ4) (and (root ?occ3 ?a) (root ?occ4 ?a) (state_equiv ?occ3 ?occ4) (not (min_equiv ?occ3 ?occ4 ?a))))))) (forall (?a) (iff (rigid_conditional ?a) (forall (?occ1) (exists (?occ2) (and (root ?occ1 ?a) (root ?occ2 ?a) (state_equiv ?occ1 ?occ2) (not (min_equiv ?occ1 ?occ2 ?a))))))) (forall (?a) (iff (launch ?a) (forall (?occ1 ?occ2) (if (and (profile ?occ1 ?a) (profile ?occ2 ?a) (begin_equiv ?occ1 ?occ2)) (root_equiv ?a ?occ1 ?occ2))))) (forall (?a) (iff (partial_launch ?a) (and (exists (?occ1) (forall (?occ2) (if (and (profile ?occ1 ?a) (profile ?occ2 ?a) (begin_equiv ?occ1 ?occ2)) (root_equiv ?a ?occ1 ?occ2)))) (exists (?occ3 ?occ4) (and (profile ?occ3 ?a) (profile ?occ4 ?a) (begin_equiv ?occ3 ?occ4) (not (root_equiv ?a ?occ3 ?occ4))))))) (forall (?a) (iff (rigid_launch ?a) (forall (?occ1) (if (profile ?occ1 ?a) (exists (?occ2) (and (begin_equiv ?occ1 ?occ2) (not (root_equiv ?a ?occ1 ?occ2)))))))) (forall (?a) (iff (temporal_effects ?a) (forall (?s1 ?s2) (if (and (occurrence_of ?s1 ?a) (occurrence_of ?s2 ?a) (begin_equiv ?s1 ?s2)) (effects_equiv ?a ?s1 ?s2))))) (forall (?a) (iff (partial_temporal ?a) (and (exists (?s1) (forall (?s2) (if (begin_equiv ?s1 ?s2) (effects_equiv ?a ?s1 ?s2)))) (exists (?s3 ?s4) (and (begin_equiv ?s3 ?s4) (not (effects_equiv ?a ?s3 ?s4))))))) (forall (?a) (iff (nontemporal ?a) (forall (?s1) (exists (?s2) (and (begin_equiv ?s1 ?s2) (not (effects_equiv ?a ?s1 ?s2))))))) (forall (?s1 ?s2) (iff (begin_equiv ?s1 ?s2) (= (beginof ?s1) (beginof ?s2)))) (forall (?a) (iff (time_precond ?a) (forall (?s1 ?s2) (if (begin_equiv ?s1 ?s2) (poss_equiv ?a ?s1 ?s2))))) (forall (?a) (iff (partial_time ?a) (and (exists (?s1) (forall (?s2) (if (begin_equiv ?s1 ?s2) (poss_equiv ?a ?s1 ?s2)))) (exists (?s3 ?s4) (and (begin_equiv ?s3 ?s4) (not (poss_equiv ?a ?s3 ?s4))))))) (forall (?a) (iff (rigid_time ?a) (forall (?s1) (exists (?s2) (and (begin_equiv ?s1 ?s2) (not (poss_equiv ?a ?s1 ?s2))))))) (forall (?a) (iff (time_conditional ?a) (forall (?occ1 ?occ2) (if (and (root ?occ1 ?a) (root ?occ2 ?a) (begin_equiv ?occ1 ?occ2)) (min_equiv ?occ1 ?occ2 ?a))))) (forall (?a) (iff (partial_time_conditional ?a) (and (exists (?occ1) (forall (?occ2) (if (and (root ?occ1 ?a) (root ?occ2 ?a) (begin_equiv ?occ1 ?occ2)) (min_equiv ?occ1 ?occ2 ?a)))) (exists (?occ3 ?occ4) (and (root ?occ3 ?a) (root ?occ4 ?a) (begin_equiv ?occ3 ?occ4) (not (min_equiv ?occ3 ?occ4 ?a))))))) (forall (?a) (iff (rigid_time_conditional ?a) (forall (?occ1) (exists (?occ2) (and (root ?occ1 ?a) (root ?occ2 ?a) (begin_equiv ?occ1 ?occ2) (not (min_equiv ?occ1 ?occ2 ?a))))))) (forall (?a) (iff (state_filter ?a) (forall (?a1 ?s1 ?s2) (if (and (subactivity ?a1 ?a) (poss ?a ?s1) (poss ?a ?s2) (state_equiv ?s1 ?s2)) (poss_equiv ?a1 ?s1 ?s2))))) (forall (?a) (iff (partial_state_filter ?a) (and (exists (?s1) (forall (?a1 ?s2) (if (and (subactivity ?a1 ?a) (poss ?a ?s1) (poss ?a ?s2) (state_equiv ?s1 ?s2)) (poss_equiv ?a1 ?s1 ?s2)))) (exists (?a2 ?s3 ?s4) (and (subactivity ?a2 ?a) (poss ?a ?s3) (poss ?a ?s4) (state_equiv ?s3 ?s4) (not (poss_equiv ?a2 ?s3 ?s4))))))) (forall (?a) (iff (rigid_state_filter ?a) (forall (?s1) (exists (?a1 ?s2) (and (state_equiv ?s1 ?s2) (poss ?a ?s1) (poss ?a ?s2) (not (poss_equiv ?a1 ?s1 ?s2))))))) (forall (?a) (iff (time_filter ?a) (forall (?a1 ?s1 ?s2) (if (and (subactivity ?a1 ?a) (poss ?a ?s1) (poss ?a ?s2) (begin_equiv ?s1 ?s2)) (poss_equiv ?a1 ?s1 ?s2))))) (forall (?a) (iff (partial_time_filter ?a) (and (exists (?s1) (forall (?s2 ?a1) (if (and (subactivity ?a1 ?a) (poss ?a ?s1) (poss ?a ?s2) (begin_equiv ?s1 ?s2)) (poss_equiv ?a1 ?s1 ?s2)))) (exists (?a2 ?s3 ?s4) (and (subactivity ?a2 ?a) (poss ?a ?s3) (poss ?a ?s4) (begin_equiv ?s3 ?s4) (not (poss_equiv ?a2 ?s3 ?s4))))))) (forall (?a) (iff (rigid_time_filter ?a) (forall (?s1) (exists (?a1 ?s2) (and (begin_equiv ?s1 ?s2) (poss ?a ?s1) (poss ?a ?s2) (not (poss_equiv ?a1 ?s1 ?s2))))))) (forall (?a) (iff (state_nonfilter ?a) (forall (?a1 ?s1 ?s2) (if (and (subactivity ?a1 ?a) (not (poss ?a ?s1)) (not (poss ?a ?s2)) (state_equiv ?s1 ?s2)) (poss_equiv ?a1 ?s1 ?s2))))) (forall (?a) (iff (partial_state_nonfilter ?a) (and (exists (?s1) (forall (?s2 ?a1) (if (and (subactivity ?a1 ?a) (not (poss ?a ?s1)) (not (poss ?a ?s2)) (state_equiv ?s1 ?s2)) (poss_equiv ?a1 ?s1 ?s2)))) (exists (?a2 ?s3 ?s4) (and (subactivity ?a2 ?a) (not (poss ?a ?s3)) (not (poss ?a ?s4)) (state_equiv ?s3 ?s4) (not (poss_equiv ?a2 ?s3 ?s4))))))) (forall (?a) (iff (rigid_state_nonfilter ?a) (forall (?s1) (exists (?a1 ?s2) (and (state_equiv ?s1 ?s2) (not (poss ?a ?s1)) (not (poss ?a ?s2)) (not (poss_equiv ?a1 ?s1 ?s2))))))) (forall (?a) (iff (time_nonfilter ?a) (forall (?a1 ?s1 ?s2) (if (and (subactivity ?a1 ?a) (not (poss ?a ?s1)) (not (poss ?a ?s2)) (begin_equiv ?s1 ?s2)) (poss_equiv ?a1 ?s1 ?s2))))) (forall (?a) (iff (partial_time_nonfilter ?a) (and (exists (?s1) (forall (?s2 ?a1) (if (and (subactivity ?a1 ?a) (not (poss ?a ?s1)) (not (poss ?a ?s2)) (begin_equiv ?s1 ?s2)) (poss_equiv ?a1 ?s1 ?s2)))) (exists (?a2 ?s3 ?s4) (and (subactivity ?a2 ?a) (not (poss ?a ?s3)) (not (poss ?a ?s4)) (begin_equiv ?s3 ?s4) (not (poss_equiv ?a2 ?s3 ?s4))))))) (forall (?a) (iff (rigid_time_nonfilter ?a) (forall (?s1) (exists (?a1 ?s2) (and (begin_equiv ?s1 ?s2) (not (poss ?a ?s1)) (not (poss ?a ?s2)) (not (poss_equiv ?a1 ?s1 ?s2))))))) (forall (?a) (iff (state_clobber ?a) (forall (?a1 ?s1 ?s2) (if (and (atomic ?a1) (state_equiv ?s1 ?s2)) (iff (preserved_effects ?a1 ?a ?s1) (preserved_effects ?a1 ?a ?s2)))))) (forall (?a) (iff (partial_clobber ?a) (and (exists (?s1 ?a1) (forall (?s2) (if (and (atomic ?a1) (state_equiv ?s1 ?s2)) (iff (preserved_effects ?a1 ?a ?s1) (preserved_effects ?a1 ?a ?s2))))) (exists (?a2 ?s3 ?s4) (and (atomic ?a2) (state_equiv ?s3 ?s4) (preserved_effects ?a2 ?a ?s3) (not (preserved_effects ?a2 ?a ?s4))))))) (forall (?a) (iff (unconditional_clobber ?a) (forall (?s1) (exists (?a1 ?s2) (and (atomic ?a1) (state_equiv ?s1 ?s2) (iff (preserved_effects ?a1 ?a ?s1) (not (preserved_effects ?a1 ?a ?s2)))))))) (forall (?a) (iff (time_clobber ?a) (forall (?a1 ?s1 ?s2) (if (and (atomic ?a1) (begin_equiv ?s1 ?s2)) (iff (preserved_effects ?a1 ?a ?s1) (preserved_effects ?a1 ?a ?s2)))))) (forall (?a) (iff (sometime_clobber ?a) (and (exists (?s1 ?a1) (forall (?s2) (if (and (atomic ?a1) (begin_equiv ?s1 ?s2)) (iff (preserved_effects ?a1 ?a ?s1) (preserved_effects ?a1 ?a ?s2))))) (exists (?a2 ?s3 ?s4) (and (atomic ?a2) (begin_equiv ?s3 ?s4) (preserved_effects ?a2 ?a ?s3) (not (preserved_effects ?a2 ?a ?s4))))))) (forall (?a) (iff (rigid_clobber ?a) (forall (?s1) (exists (?a1 ?s2) (and (atomic ?a1) (begin_equiv ?s1 ?s2) (iff (preserved_effects ?a1 ?a ?s1) (not (preserved_effects ?a1 ?a ?s2)))))))) (forall (?a) (iff (state_interfere ?a) (forall (?a1 ?s1 ?s2) (if (and (atomic ?a1) (state_equiv ?s1 ?s2)) (iff (preserved_filter ?a1 ?a ?s1) (preserved_filter ?a1 ?a ?s2)))))) (forall (?a) (iff (partial_interfere ?a) (and (exists (?s1 ?a1) (forall (?s2) (if (and (atomic ?a1) (state_equiv ?s1 ?s2)) (iff (preserved_filter ?a1 ?a ?s1) (preserved_filter ?a1 ?a ?s2))))) (exists (?a2 ?s3 ?s4) (and (atomic ?a2) (state_equiv ?s3 ?s4) (preserved_filter ?a2 ?a ?s3) (not (preserved_filter ?a2 ?a ?s4))))))) (forall (?a) (iff (unconditional_interfere ?a) (forall (?s1) (exists (?a1 ?s2) (and (atomic ?a1) (state_equiv ?s1 ?s2) (iff (preserved_filter ?a1 ?a ?s1) (not (preserved_filter ?a1 ?a ?s2)))))))) (forall (?a) (iff (time_interfere ?a) (forall (?a1 ?s1 ?s2) (if (and (atomic ?a1) (begin_equiv ?s1 ?s2)) (iff (preserved_filter ?a1 ?a ?s1) (preserved_filter ?a1 ?a ?s2)))))) (forall (?a) (iff (sometime_interfere ?a) (and (exists (?s1 ?a1) (forall (?s2) (if (and (atomic ?a1) (begin_equiv ?s1 ?s2)) (iff (preserved_filter ?a1 ?a ?s1) (preserved_filter ?a1 ?a ?s2))))) (exists (?a2 ?s3 ?s4) (and (atomic ?a2) (begin_equiv ?s3 ?s4) (preserved_filter ?a2 ?a ?s3) (not (preserved_filter ?a2 ?a ?s4))))))) (forall (?a) (iff (rigid_interfere ?a) (forall (?s1) (exists (?a1 ?s2) (and (atomic ?a1) (begin_equiv ?s1 ?s2) (iff (preserved_filter ?a1 ?a ?s1) (not (preserved_filter ?a1 ?a ?s2)))))))) (forall (?occ1 ?occ2 ?a) (iff (min_equiv ?occ1 ?occ2 ?a) (and (subtree_embed ?occ1 ?occ2 ?a) (subtree_embed ?occ2 ?occ1 ?a)))) (forall (?a) (iff (uniform ?a) (forall (?occ1 ?occ2) (if (and (root ?occ1 ?a) (root ?occ2 ?a)) (min_equiv ?occ1 ?occ2 ?a))))) (forall (?a) (iff (variegated ?a) (and (exists (?a1) (forall (?occ1 ?occ2) (if (and (occurrence_of ?occ1 ?a1) (occurrence_of ?occ2 ?a1) (root ?occ1 ?a) (root ?occ2 ?a)) (min_equiv ?occ1 ?occ2 ?a)))) (exists (?a2 ?occ3 ?occ4) (and (occurrence_of ?occ3 ?a2) (occurrence_of ?occ4 ?a2) (root ?occ3 ?a) (root ?occ4 ?a) (not (min_equiv ?occ3 ?occ4 ?a))))))) (forall (?a) (iff (multiform ?a) (forall (?a1 ?occ1) (if (and (root ?occ1 ?a) (occurrence_of ?occ1 ?a1)) (exists (?occ2 ?occ3) (and (occurrence_of ?occ2 ?a1) (occurrence_of ?occ3 ?a1) (root ?occ2 ?a) (root ?occ3 ?a) (not (min_equiv ?occ2 ?occ3 ?a)))))))) (forall (?occ) (= (dur ?occ) (duration (beginof ?occ) (endof ?occ)))) (forall (?occ1 ?occ2) (= (delay ?occ1 ?occ2) (duration (beginof ?occ1) (beginof ?occ2)))) (forall (?occ1 ?occ2) (iff (dur_equiv ?occ1 ?occ2) (= (dur ?occ1) (dur ?occ2)))) (forall (?occ1 ?occ2) (iff (delay_equiv ?occ1 ?occ2) (exists (?occ) (= (delay ?occ ?occ1) (delay ?occ ?occ2))))) (forall (?a) (iff (constant ?a) (forall (?occ1 ?occ2) (if (and (occurrence_of ?occ1 ?a) (occurrence_of ?occ2 ?a)) (dur_equiv ?occ1 ?occ2))))) (forall (?a) (iff (interval_duration ?a) (forall (?occ1) (if (occurrence_of ?occ1 ?a) (exists (?occ2) (and (occurrence_of ?occ2 ?a) (dur_equiv ?occ1 ?occ2))))))) (forall (?a) (iff (variable ?a) (not (exists (?occ1 ?occ2) (and (occurrence_of ?occ1 ?a) (occurrence_of ?occ2 ?a) (dur_equiv ?occ1 ?occ2)))))) (forall (?occ1 ?occ2 ?a) (iff (coo_precedes ?occ1 ?occ2 ?a) (forall (?s1 ?s2) (if (and (subactivity_occurrence ?s1 ?occ1) (subactivity_occurrence ?s2 ?occ2) (atomocc ?s1) (atomocc ?s2)) (soo_precedes ?s1 ?s2 ?a))))) (forall (?occ1 ?occ2 ?a) (iff (strong_parallel ?occ1 ?occ2 ?a) (forall (?s1 ?s2) (if (and (subactivity_occurrence ?s1 ?occ1) (subactivity_occurrence ?s2 ?occ2) (atomocc ?s1) (atomocc ?s2)) (same_bag ?s1 ?s2 ?a))))) (forall (?s) (iff (atomocc ?s) (exists (?a) (and (atomic ?a) (occurrence_of ?s ?a))))) (forall (?a) (iff (duration_effects ?a) (forall (?s1 ?s2) (if (and (occurrence_of ?s1 ?a) (occurrence_of ?s2 ?a) (dur_equiv ?s1 ?s2)) (effects_equiv ?a ?s1 ?s2))))) (forall (?a) (iff (partial_duration_effects ?a) (and (exists (?s1) (forall (?s2) (if (and (occurrence_of ?s1 ?a) (occurrence_of ?s2 ?a) (dur_equiv ?s1 ?s2)) (effects_equiv ?a ?s1 ?s2)))) (exists (?s3 ?s4) (and (occurrence_of ?s3 ?a) (occurrence_of ?s4 ?a) (dur_equiv ?s3 ?s4) (not (effects_equiv ?a ?s3 ?s4))))))) (forall (?a) (iff (nonduration_effects ?a) (forall (?s1) (if (occurrence_of ?s1 ?a) (exists (?s2) (and (occurrence_of ?s2 ?a) (dur_equiv ?s1 ?s2) (not (effects_equiv ?a ?s1 ?s2)))))))) (forall (?a) (iff (embed_duration ?a) (forall (?occ1 ?occ2) (if (and (occurrence_of ?occ1 ?a) (occurrence_of ?occ2 ?a) (same_grove ?occ1 ?occ2) (branch_automorphic ?occ1 ?occ2)) (duration_equiv ?occ1 ?occ2))))) (forall (?a) (iff (partial_embed_duration ?a) (and (exists (?occ1) (forall (?occ2) (if (and (occurrence_of ?occ1 ?a) (occurrence_of ?occ2 ?a) (same_grove ?occ1 ?occ2) (branch_automorphic ?occ1 ?occ2)) (dur_equiv ?occ1 ?occ2)))) (exists (?occ3 ?occ4) (and (occurrence_of ?occ3 ?a) (occurrence_of ?occ4 ?a) (same_grove ?occ3 ?occ4) (branch_automorphic ?occ3 ?occ4) (not (dur_equiv ?occ3 ?occ4))))))) (forall (?a) (iff (nonembed_duration ?a) (exists (?occ1 ?occ2) (and (occurrence_of ?occ1 ?a) (occurrence_of ?occ2 ?a) (same_grove ?occ1 ?occ2) (branch_automorphic ?occ1 ?occ2) (not (duration_equiv ?occ1 ?occ2)))))) (forall (?a) (iff (maintain_effects ?a) (forall (?s1 ?s2) (if (and (occurrence_of ?s1 ?a) (occurrence_of ?s2 ?a) (state_equiv ?s1 ?s2) (dur_equiv ?s1 ?s2)) (effects_equiv ?a ?s1 ?s2))))) (forall (?a) (iff (partial_maintain ?a) (and (exists (?s1) (forall (?s2) (if (and (occurrence_of ?s1 ?a) (occurrence_of ?s2 ?a) (state_equiv ?s1 ?s2) (dur_equiv ?s1 ?s2)) (effects_equiv ?a ?s1 ?s2)))) (exists (?s3 ?s4) (and (occurrence_of ?s3 ?a) (occurrence_of ?s4 ?a) (dur_equiv ?s3 ?s4) (not (effects_equiv ?a ?s3 ?s4))))))) (forall (?a) (iff (nonmaintain ?a) (forall (?s1) (if (occurrence_of ?s1 ?a) (exists (?s2) (and (occurrence_of ?s2 ?a) (dur_equiv ?s1 ?s2) (not (effects_equiv ?a ?s1 ?s2)))))))) (forall (?a) (iff (mixed_duration ?a) (forall (?occ1 ?occ2) (if (and (occurrence_of ?occ1 ?a) (occurrence_of ?occ2 ?a) (state_equiv ?occ1 ?occ2) (begin_equiv ?occ1 ?occ2)) (dur_equiv ?occ1 ?occ2))))) (forall (?a) (iff (nondet_mixed_duration ?a) (and (exists (?occ1) (forall (?occ2) (if (and (occurrence_of ?occ1 ?a) (occurrence_of ?occ2 ?a) (state_equiv ?occ1 ?occ2) (begin_equiv ?occ1 ?occ2)) (dur_equiv ?occ1 ?occ2)))) (exists (?occ3 ?occ4) (and (occurrence_of ?occ3 ?a) (occurrence_of ?occ4 ?a) (begin_equiv ?occ3 ?occ4) (state_equiv ?occ3 ?occ4) (not (dur_equiv ?occ3 ?occ4))))))) (forall (?a) (iff (rigid_mixed_duration ?a) (forall (?occ1) (if (occurrence_of ?occ1 ?a) (exists (?occ2) (and (occurrence_of ?occ2 ?a) (begin_equiv ?occ1 ?occ2) (state_equiv ?occ1 ?occ2) (not (dur_equiv ?occ1 ?occ2)))))))) (forall (?a) (iff (ordered_duration ?a) (forall (?occ1 ?occ2) (if (and (occurrence_of ?occ1 ?a) (occurrence_of ?occ2 ?a) (branch_automorphic ?occ1 ?occ2)) (duration_equiv ?occ1 ?occ2))))) (forall (?a) (iff (partial_ordered_duration ?a) (and (exists (?occ1) (forall (?occ2) (if (and (occurrence_of ?occ1 ?a) (occurrence_of ?occ2 ?a) (branch_automorphic ?occ1 ?occ2)) (dur_equiv ?occ1 ?occ2)))) (exists (?occ3 ?occ4) (and (occurrence_of ?occ3 ?a) (occurrence_of ?occ4 ?a) (branch_automorphic ?occ3 ?occ4) (not (dur_equiv ?occ3 ?occ4))))))) (forall (?a) (iff (unordered_duration ?a) (exists (?occ1 ?occ2) (and (occurrence_of ?occ1 ?a) (occurrence_of ?occ2 ?a) (branch_automorphic ?occ1 ?occ2) (not (duration_equiv ?occ1 ?occ2)))))) (forall (?occ) (iff (scheduled ?occ) (forall (?a ?s1 ?s2 ?s3) (if (and (occurrence_of ?occ ?a) (= ?s3 (root_occ ?occ)) (subactivity_occurrence ?s1 ?occ) (iso_occ ?s1 ?s2 ?a) (embed_tree ?s1 ?s2 ?s3 ?a) (delay_equiv ?s1 ?s2)) (subocc_equiv ?s1 ?s2 ?s3 ?a))))) (forall (?occ) (iff (partial_scheduled ?occ) (exists (?a ?s ?s1 ?s3 ?s4) (and (occurrence_of ?occ ?a) (= ?s (root_occ ?occ)) (subactivity_occurrence ?s1 ?occ) (forall (?s2) (if (and (iso_occ ?s1 ?s2 ?a) (embed_tree ?s1 ?s2 ?s ?a) (delay_equiv ?s1 ?s2)) (subocc_equiv ?s1 ?s2 ?s ?a))) (subactivity_occurrence ?s3 ?occ) (iso_occ ?s3 ?s4 ?a) (delay_equiv ?s3 ?s4) (embed_tree ?s3 ?s4 ?s ?a) (not (subocc_equiv ?s3 ?s4 ?s ?a)))))) (forall (?occ) (iff (unscheduled ?occ) (forall (?s ?s1 ?a) (if (and (occurrence_of ?occ ?a) (= ?s (root_occ ?occ)) (subactivity_occurrence ?s1 ?occ)) (exists (?s2) (and (iso_occ ?s1 ?s2 ?a) (embed_tree ?s1 ?s2 ?s ?a) (delay_equiv ?s1 ?s2) (not (subocc_equiv ?s1 ?s2 ?s ?a)))))))) (forall (?a) (iff (spoilage ?a) (forall (?s1 ?s2) (if (and (occurrence_of ?s1 ?a) (occurrence_of ?s2 ?a) (delay_equiv ?s1 ?s2) (tree_equiv ?s1 ?s2)) (legal_equiv ?s1 ?s2))))) (forall (?a) (iff (possible_spoilage ?a) (exists (?s1) (and (occurrence_of ?s1 ?a) (forall (?s2) (if (and (occurrence_of ?s2 ?a) (delay_equiv ?s1 ?s2) (tree_equiv ?s1 ?s2)) (legal_equiv ?s1 ?s2))))))) (forall (?a) (iff (nonspoilage ?a) (forall (?s1) (if (occurrence_of ?s1 ?a) (exists (?s2) (and (occurrence_of ?s2 ?a) (delay_equiv ?s1 ?s2) (tree_equiv ?s1 ?s2) (not (legal_equiv ?s1 ?s2)))))))) (forall (?a) (iff (conditional_duration ?a) (forall (?occ1 ?occ2) (if (and (occurrence_of ?occ1 ?a) (occurrence_of ?occ2 ?a) (state_equiv ?occ1 ?occ2)) (dur_equiv ?occ1 ?occ2))))) (forall (?a) (iff (context_duration ?a) (and (exists (?occ1) (forall (?occ2) (if (and (occurrence_of ?occ1 ?a) (occurrence_of ?occ2 ?a) (state_equiv ?occ1 ?occ2)) (dur_equiv ?occ1 ?occ2)))) (exists (?occ3 ?occ4) (and (occurrence_of ?occ3 ?a) (occurrence_of ?occ3 ?a) (state_equiv ?occ3 ?occ4) (not (dur_equiv ?occ3 ?occ4))))))) (forall (?a) (iff (unconditional_duration ?a) (forall (?occ1) (if (occurrence_of ?occ1 ?a) (exists (?occ2) (and (occurrence_of ?occ2 ?a) (state_equiv ?occ1 ?occ2) (not (dur_equiv ?occ1 ?occ2)))))))) (forall (?s1 ?s2 ?a) (iff (same_bag ?s1 ?s2 ?a) (exists (?s3 ?s4) (and (next_subocc ?s1 ?s3 ?a) (iso_occ ?s3 ?s2 ?a) (next_subocc ?s2 ?s4 ?a) (iso_occ ?s4 ?s1 ?a))))) (forall (?s ?a) (iff (rotate ?s ?a) (and (forall (?s1) (if (next_subocc ?s ?s1 ?a) (exists (?s2) (and (sibling ?s ?s2 ?a) (iso_occ ?s1 ?s2 ?a))))) (forall (?s3) (if (sibling ?s ?s3 ?a) (same_bag ?s ?s3 ?a)))))) (forall (?s ?a) (iff (reflect ?s ?a) (forall (?s1) (iff (next_subocc ?s ?s1 ?a) (next_soo (soomap ?s) (soomap ?s1) ?a))))) (forall (?s ?a) (iff (flip ?s ?a) (forall (?s1) (iff (next_subocc ?s ?s1 ?a) (or (next_soo (soomap ?s) (soomap ?s1) ?a) (exists (?s2) (and (sibling ?s ?s2 ?a) (iso_occ ?s1 ?s2 ?a)))))))) (forall (?s ?a) (iff (turn ?s ?a) (and (exists (?s5) (and (sibling ?s ?s5 ?a) (same_bag ?s ?s5 ?a))) (forall (?s1) (if (next_subocc ?s ?s1 ?a) (or (next_soo (soomap ?s) (soomap ?s1) ?a) (exists (?s2) (and (sibling ?s ?s2 ?a) (iso_occ ?s1 ?s2 ?a))))))))) (forall (?occ) (iff (bag ?occ) (forall (?a ?s ?occ1) (if (and (same_grove ?occ ?occ1) (occurrence_of ?occ ?a) (subactivity_occurrence ?s ?occ1)) (rotate ?s ?a))))) (forall (?occ) (iff (choice_poset ?occ) (forall (?a ?s ?occ1) (if (and (same_grove ?occ ?occ1) (occurrence_of ?occ ?a) (subactivity_occurrence ?s ?occ1)) (reflect ?s ?a))))) (forall (?occ) (iff (strong_poset ?occ) (forall (?a ?s ?occ1) (if (and (same_grove ?occ ?occ1) (occurrence_of ?occ ?a) (subactivity_occurrence ?s ?occ1)) (flip ?s ?a))))) (forall (?occ) (iff (complex_poset ?occ) (forall (?a ?s ?occ1) (if (and (same_grove ?occ ?occ1) (occurrence_of ?occ ?a) (subactivity_occurrence ?s ?occ1)) (turn ?s ?a))))) (forall (?a) (iff (rushhour ?a) (forall (?occ1 ?occ2) (if (and (occurrence_of ?occ1 ?a) (occurrence_of ?occ2 ?a) (begin_equiv ?occ1 ?occ2)) (dur_equiv ?occ1 ?occ2))))) (forall (?a) (iff (weekend ?a) (and (exists (?occ1) (forall (?occ2) (if (and (occurrence_of ?occ1 ?a) (occurrence_of ?occ2 ?a) (begin_equiv ?occ1 ?occ2)) (dur_equiv ?occ1 ?occ2)))) (exists (?occ3 ?occ4) (and (occurrence_of ?occ3 ?a) (occurrence_of ?occ3 ?a) (begin_equiv ?occ3 ?occ4) (not (dur_equiv ?occ3 ?occ4))))))) (forall (?a) (iff (gridlock ?a) (forall (?occ1) (if (occurrence_of ?occ1 ?a) (exists (?occ2) (and (occurrence_of ?occ2 ?a) (begin_equiv ?occ1 ?occ2) (not (dur_equiv ?occ1 ?occ2)))))))) (forall (?a ?r) (iff (exclusive_use ?a ?r) (forall (?q1 ?q2 ?occ ?occp) (if (and (do ?a ?occ ?occp) (holds (demand ?a ?r ?q1) ?occ) (holds (resource_point ?r ?q2) ?occ)) (= ?q1 ?q2))))) (forall (?a ?r) (iff (capacity_based ?a ?r) (forall (?q1 ?q2 ?occ ?occp) (if (and (do ?a ?occ ?occp) (holds (demand ?a ?r ?q1) ?occ) (holds (resource_point ?r ?q2) ?occ)) (lesser ?q1 ?q2))))) (forall (?r) (iff (unary_resource ?r) (forall (?a) (if (requires ?a ?r) (exclusive_use ?a ?r))))) (forall (?r) (iff (capacitated_resource ?r) (forall (?a) (if (requires ?a ?r) (capacity_based ?a ?r))))) (forall (?a ?r ?q) (iff (uniform_demand ?a ?r ?q) (forall (?occ) (holds (demand ?a ?r ?q) ?occ)))) (forall (?r ?a) (iff (layout ?r ?a) (forall (?q ?occ1 ?occ2 ?ap) (if (= ?occ2 (successor ?ap ?occ1)) (not (iff (holds (demand ?r ?a ?q) ?occ2) (holds (demand ?r ?a ?q) ?occ1))))))) (forall (?a ?r ?q) (iff (consumes_quantity ?a ?r ?q) (forall (?q1 ?occ1 ?occ2) (if (and (do ?a ?occ1 ?occ2) (holds (demand ?a ?r ?q) ?occ1) (holds (resource_point ?r ?q1) ?occ1)) (holds (resource_point ?r (minus ?q1 ?q)) ?occ2))))) (forall (?a ?r ?q) (iff (strict_consumes_quantity ?a ?r ?q) (and (consumes_quantity ?a ?r ?q) (nonreplenishable ?r)))) (forall (?a ?r ?q) (iff (produces_quantity ?a ?r ?q) (forall (?q1 ?q2 ?occ1 ?occ2) (if (and (do ?a ?occ1 ?occ2) (holds (resource_point ?r ?q1) ?occ1) (= ?q2 (plus ?q1 ?q))) (holds (resource_point ?r ?q2) ?occ2))))) (forall (?a ?r ?q) (iff (strict_produces_quantity ?a ?r ?q) (and (produces_quantity ?a ?r ?q) (not (exists (?a2 ?q2) (and (subactivity ?a2 ?a) (consumes_quantity ?a2 ?r ?q2))))))) (forall (?a ?r ?q) (iff (uses_quantity ?a ?r ?q) (forall (?q1 ?q2 ?occ1 ?occ2) (if (and (do ?a ?occ1 ?occ2) (holds (demand ?a ?r ?q) ?occ1) (holds (resource_point ?r ?q1) ?occ1) (holds (resource_point ?r ?q2) ?occ2)) (= ?q2 ?q1))))) (forall (?a ?r) (iff (creates ?a ?r) (exists (?q1) (and (produces_quantity ?a ?r ?q1) (forall (?q2 ?occ) (if (and (occurrence_of ?occ ?a) (prior (resource_point ?r ?q2) ?occ)) (= ?q2 0))))))) (forall (?a ?r) (iff (destroys ?a ?r) (exists (?q1) (and (consumes_quantity ?a ?r ?q1) (forall (?q2 ?occ) (if (and (occurrence_of ?occ ?a) (prior (resource_point ?r ?q2) ?occ)) (= ?q2 0))))))) (forall (?r ?q) (iff (fixed_quantity ?r ?q) (forall (?occ) (holds (resource_point ?r ?q) ?occ)))) (forall (?r) (iff (nonreplenishable ?r) (forall (?a ?q1 ?q2 ?occ1 ?occ2 ?occ3) (if (and (if (do ?a ?occ1 ?occ2) (holds (resource_point ?r ?q1) ?occ2)) (precedes ?occ2 ?occ3) (holds (resource_point ?r ?q2) ?occ3)) (lesserEq ?q2 ?q1))))) (forall (?a ?r) (iff (uses ?a ?r) (exists (?q) (uses_quantity ?a ?r ?q)))) (forall (?a ?r) (iff (consumes ?a ?r) (exists (?q) (consumes_quantity ?a ?r ?q)))) (forall (?a ?r) (iff (strict_consumes ?a ?r) (exists (?q) (strict_consumes_quantity ?a ?r ?q)))) (forall (?a ?r) (iff (produces ?a ?r) (exists (?q) (produces_quantity ?a ?r ?q)))) (forall (?a ?r) (iff (strict_produces ?a ?r) (exists (?q) (strict_produces_quantity ?a ?r ?q)))) (forall (?a ?r ?q) (iff (provides_quantity ?a ?r ?q) (and (exists (?a1) (and (subactivity ?a1 ?a) (produces_quantity ?a1 ?r ?q))) (exists (?a2) (and (subactivity ?a2 ?a) (consumes_quantity ?a2 ?r ?q)))))) (forall (?a ?r) (iff (provides ?a ?r) (exists (?q) (provides_quantity ?a ?r ?q)))) (forall (?r ?a1 ?a2 ?a ?occ2) (iff (reusable ?r ?a1) (if (and (common ?a1 ?a2 ?r) (subactivity ?a1 ?a) (subactivity ?a2 ?a) (occurrence_of ?occ2 ?a1)) (forall (?b ?occ3) (if (and (subactivity_occurrence ?occ3 ?b) (occurrence_of ?b ?a) (precedes ?occ2 ?occ3)) (poss ?a2 ?occ3)))))) (forall (?r ?a1) (iff (possibly_reusable ?r ?a1) (forall (?a2 ?occ2 ?a) (if (and (common ?a1 ?a2 ?r) (subactivity ?a1 ?a) (subactivity ?a2 ?a) (occurrence_of ?occ2 ?a1)) (exists (?b ?occ3) (and (subactivity_occurrence ?occ3 ?b) (occurrence_of ?b ?a) (precedes ?occ2 ?occ3) (poss ?a2 ?occ3))))))) (forall (?r ?a1) (iff (renewable ?r ?a1) (forall (?a ?a2 ?occ2) (if (and (common ?a1 ?a2 ?r) (subactivity ?a1 ?a) (subactivity ?a2 ?a) (occurrence_of ?occ2 ?a1)) (forall (?b) (if (occurrence_of ?b ?a) (exists (?occ3) (and (subactivity_occurrence ?occ3 ?b) (precedes ?occ2 ?occ3) (poss ?a2 ?occ3))))))))) (forall (?r ?a1) (iff (weakly_reusable ?r ?a1) (forall (?a ?a2 ?occ2) (if (and (common ?a1 ?a2 ?r) (subactivity ?a1 ?a) (subactivity ?a2 ?a) (occurrence_of ?occ2 ?a1)) (exists (?b) (and (forall (?occ3) (if (and (subactivity_occurrence ?occ3 ?b) (occurrence_of ?b ?a) (precedes ?occ2 ?occ3)) (poss ?a2 ?occ3))))))))) (forall (?r ?a1) (iff (consumable ?r ?a1) (forall (?a ?a2 ?occ2) (if (and (common ?a1 ?a2 ?r) (subactivity ?a1 ?a) (subactivity ?a2 ?a) (occurrence_of ?occ2 ?a1)) (forall (?b ?occ3) (if (and (subactivity_occurrence ?occ3 ?b) (occurrence_of ?b ?a) (precedes ?occ2 ?occ3)) (not (poss ?a2 ?occ3)))))))) (forall (?r ?a1) (iff (possibly_consumable ?r ?a1) (forall (?a ?a2 ?occ2) (if (and (common ?a1 ?a2 ?r) (subactivity ?a1 ?a) (subactivity ?a2 ?a) (occurrence_of ?occ2 ?a1)) (exists (?b ?occ3) (and (subactivity_occurrence ?occ3 ?b) (occurrence_of ?b ?a) (precedes ?occ2 ?occ3) (not (poss ?a2 ?occ3)))))))) (forall (?r ?a1) (iff (weakly_consumable ?r ?a1) (forall (?a ?a2 ?occ2) (if (and (common ?a1 ?a2 ?r) (subactivity ?a1 ?a) (subactivity ?a2 ?a) (occurrence_of ?occ2 ?a1)) (exists (?b) (and (occurrence_of ?b ?a) (forall (?occ3) (if (and (subactivity_occurrence ?occ3 ?b) (occurrence_of ?b ?a) (precedes ?occ2 ?occ3)) (not (poss ?a2 ?occ3)))))))))) (forall (?r ?a1) (iff (wearable ?r ?a1) (forall (?a ?a2 ?occ2) (if (and (common ?a1 ?a2 ?r) (subactivity ?a1 ?a) (subactivity ?a2 ?a) (occurrence_of ?occ2 ?a1)) (forall (?b) (if (occurrence_of ?b ?a) (exists (?occ3) (and (subactivity_occurrence ?occ3 ?b) (precedes ?occ2 ?occ3) (not (poss ?a2 ?occ3)))))))))) (forall (?a ?r) (iff (pile ?r ?a) (and (homogeneous_set ?r ?a) (forall (?q ?occ) (iff (holds (resource_point ?r ?q) ?occ) (exists (?i) (and (holds (resource_set ?i ?r) ?occ) (= ?q (cardinality ?i))))))))) (forall (?r ?a) (iff (stock ?r ?a) (and (homogeneous_set ?r ?a) (forall (?q ?occ) (if (holds (demand ?a ?r ?q) ?occ) (exists (?i1 ?r1) (and (= ?q (cardinality ?i1)) (holds (resource_set ?i1 ?r1) ?occ) (requires_set ?a ?r1) (forall (?q3) (if (holds (agg_demand ?r ?q3) ?occ) (= ?q3 (cardinality ?i1))))))))))) (forall (?r ?a) (iff (pool ?r ?a) (and (homogeneous_set ?r ?a) (forall (?q ?occ) (if (holds (demand ?a ?r ?q) ?occ) (exists (?i ?i1 ?r1) (and (holds (resource_set ?i ?r) ?occ) (subset ?i1 ?i) (= ?q (cardinality ?i1)) (holds (resource_set ?i1 ?r1) ?occ) (requires_set ?a ?r1)))))))) (forall (?a ?r ?q) (iff (pool_demand ?a ?r ?q) (and (pool ?r ?a) (forall (?q1 ?occ) (if (holds (demand ?a ?r ?q1) ?occ) (= ?q ?q1)))))) (forall (?a ?r ?q) (if (uses_pile ?a ?r ?q) (and (pile ?r ?a) (uses_quantity ?a ?r ?q)))) (forall (?a ?r ?q) (iff (consumes_pile ?a ?r ?q) (and (pile ?r ?a) (consumes_quantity ?a ?r ?q)))) (forall (?a ?r ?q) (iff (produces_pile ?a ?r ?q) (and (pile ?r ?a) (produces_quantity ?a ?r ?q)))) (forall (?r) (iff (inventory_resource ?r) (exists (?a) (or (input_material ?r ?a) (output_material ?r ?a))))) (forall (?r ?a) (iff (inventory_pool ?r ?a) (forall (?i ?occ) (if (holds (resource_set ?i ?r) ?occ) (and (inventory_resource ?r) (homogeneous_set ?r ?a) (forall (?q1) (if (holds (resource_point ?r ?q1) ?occ) (greaterEq ?q1 (cardinality ?i)))) (stock ?r ?a) (forall (?a1 ?q4) (if (holds (min_capacity ?a1 ?r ?q4) ?occ) (lesserEq ?q4 (cardinality ?i))))))))) (forall (?r1 ?r2 ?occ) (iff (holds (inventory_contains ?r1 ?r2) ?occ) (exists (?a ?i) (and (inventory_pool ?r2 ?a) (holds (resource_set ?i ?r2) ?occ) (holds (in ?r1 ?i) ?occ))))) (forall (?r ?a) (iff (resource_pool ?r ?a) (forall (?i ?occ) (if (holds (resource_set ?i ?r) ?occ) (and (pile ?r ?a) (pool ?r ?a) (forall (?q3) (if (holds (min_capacity ?a ?r ?q3) ?occ) (lesser ?q3 (cardinality ?i))))))))) (forall (?a ?r) (iff (conservative_pool ?a ?r) (and (resource_pool ?r ?a) (forall (?q) (iff (pool_demand ?a ?r ?q) (or (uses_pile ?a ?r ?q) (consumes_pile ?a ?r ?q))))))) (forall (?r ?a) (iff (material_pool ?r ?a) (and (resource_pool ?r ?a) (exists (?q) (provides_quantity ?a ?r ?q))))) (forall (?a1 ?r1) (iff (nondet_select ?a1 ?r1) (forall (?occ) (iff (occurrence_of ?occ ?a1) (exists (?r2 ?i ?a2 ?occ2) (and (subactivity ?a2 ?a1) (holds (resource_set ?i ?r1) (root_occ ?occ)) (holds (in ?r2 ?i) (root_occ ?occ)) (requires ?a2 ?r2) (occurrence_of ?occ2 ?a2) (subactivity_occurrence ?occ2 ?occ))))))) (forall (?a1 ?r1) (iff (nondet_set_select ?a1 ?r1) (forall (?occ) (iff (occurrence_of ?occ ?a1) (exists (?r2 ?a2 ?occ2) (and (subactivity ?a2 ?a1) (holds (resource_subset ?r2 ?r1) (root_occ ?occ)) (requires ?a2 ?r2) (occurrence_of ?occ2 ?a2) (subactivity_occurrence ?occ2 ?occ))))))) (forall (?a ?r ?q) (iff (nondet_quantity_select ?a ?r ?q) (and (nondet_set_select ?a ?r) (= ?q (cardinality ?r))))) (forall (?a ?r) (iff (requires_set ?a ?r) (forall (?occ1) (iff (occurrence_of ?occ1 ?a) (forall (?a1 ?i) (if (and (holds (resource_set ?i ?r) (root_occ ?occ1)) (subactivity ?a1 ?a)) (exists (?r1 ?occ2) (and (occurrence_of ?occ2 ?a1) (holds (in ?r1 ?i) (root_occ ?occ2)) (requires ?a1 ?r1) (subactivity_occurrence ?occ1 ?occ1))))))))) (forall (?a ?r) (iff (requires_full_set ?a ?r) (forall (?occ1) (iff (occurrence_of ?occ1 ?a) (forall (?r1) (if (holds (in_resource_set ?r1 ?r) (root_occ ?occ1)) (exists (?a1 ?occ2) (and (subactivity ?a1 ?a) (requires ?a1 ?r1) (occurrence_of ?occ2 ?a1) (subactivity_occurrence ?occ2 ?occ1))))))))) (forall (?a) (iff (nondet_res_activity ?a) (if (nondet_choice ?a) (exists (?r1) (nondet_select ?a ?r1))))) (forall (?a ?r) (iff (superpose_select ?a ?r) (forall (?a1 ?occ1) (if (and (occurrence_of ?occ1 ?a) (subactivity ?a1 ?a) (primitive ?a1)) (exists (?a2 ?r1 ?occ2) (and (subactivity ?a1 ?a2) (subactivity ?a2 ?a) (occurrence_of ?occ2 ?a2) (holds (resource_subset ?r1 ?r) (root_occ ?occ2)) (nondet_select ?a2 ?r1))))))) (forall (?a ?r) (iff (homogeneous_set ?r ?a) (exists (?a2) (and (superpose_select ?a2 ?r) (subactivity ?a ?a2))))) (forall (?a1 ?a2 ?r ?occ) (iff (occurs_over (set_contention ?r) ?occ) (if (and (subactivity ?a1 (set_contention ?r)) (subactivity ?a2 (set_contention ?r))) (and (requires_set ?a1 ?r) (requires_set ?a2 ?r) (concurrent_superpose (set_contention ?r)))))) (forall (?r ?s) (if (poss (set_contention ?r) ?s) (and (forall (?a) (if (subactivity ?a (set_contention ?a)) (homogeneous_set ?r ?a))) (holds (available ?r (set_contention ?r)) ?s)))) (forall (?a ?r) (iff (modifies ?a ?r) (exists (?f) (and (resource_fluent ?f ?r) (changes ?a ?f))))) (forall (?a) (iff (processor_activity ?a) (exists (?r1 ?r2 ?r3) (and (or (reusable ?r1 ?a) (possibly_reusable ?r1 ?a)) (or (consumable ?r2 ?a) (possibly_consumable ?r2 ?a) (modifies ?a ?r2)) (or (creates ?a ?r3) (modifies ?a ?r3)))))) (forall (?r ?a) (iff (processor_resource ?r ?a) (and (processor_activity ?a) (reusable ?r ?a) (possibly_reusable ?r ?a)))) (forall (?r ?a) (iff (input_material ?r ?a) (and (processor_activity ?a) (or (consumable ?r ?a) (possibly_consumable ?r ?a) (modifies ?a ?r))))) (forall (?r ?a) (iff (output_material ?r ?a) (and (processor_activity ?a) (or (creates ?a ?r) (modifies ?a ?r))))) (forall (?occ1 ?occ2 ?a) (iff (next_processor_path ?occ1 ?occ2 ?a) (and (next_subactivity ?occ1 ?occ2 ?a) (exists (?a1 ?a2 ?r) (and (occurrence_of ?occ1 ?a1) (occurrence_of ?occ2 ?a2) (processor_activity ?a1) (processor_activity ?a2) (output_material ?r ?a1) (input_material ?r ?a2)))))) (forall (?occ1 ?occ2 ?a) (iff (pro_precedes ?occ1 ?occ2 ?a) (and (soo_precedes ?occ1 ?occ2 ?a) (forall (?occ3) (if (and (soo_precedes ?occ1 ?occ3 ?a) (soo_precedes ?occ3 ?occ2 ?a)) (exists (?occ4 ?occ5) (and (next_processor_path ?occ4 ?occ3 ?a) (next_processor_path ?occ3 ?occ5 ?a)))))))) (forall (?a) (iff (resource_path ?a) (forall (?occ1 ?occ2) (iff (soo_precedes ?occ1 ?occ2 ?a) (pro_precedes ?occ1 ?occ2 ?a))))) (forall (?occ ?a) (iff (initial_processor_path ?occ ?a) (and (resource_path ?a) (root_soo ?occ ?a)))) (forall (?occ ?a) (iff (final_processor_path ?occ ?a) (and (resource_path ?a) (leaf_soo ?occ ?a))))