;;Proof Obligations of Module in Harvey/SMT Language
(benchmark switch1Invariant0
 :logic UNKNOWN
 :extrafuns ( (normal Int )
		(reverse Int )
		(void Int )
		(actual_pos Int ))
 :extrapreds ( (POSITION Int ))
 :extramacros ((in (lambda (?x ELEMENT) (?p (ELEMENT boolean)) . (?p ?x)))
                (emptyset (lambda (?v ELEMENT) . false))
                (omega (lambda (?x ELEMENT) . true))
                (singleton (lambda (?x ELEMENT) . (lambda (?y ELEMENT) . (= ?x ?y))))
                (intersection (lambda (?p (ELEMENT boolean)) (?q (ELEMENT boolean)) .
                                      (lambda (?x ELEMENT) . (and (?p ?x) (?q ?x)))))
                (union (lambda (?p (ELEMENT boolean)) (?q (ELEMENT boolean)) .
                               (lambda (?x ELEMENT) . (or (?p ?x) (?q ?x)))))
                (difference (lambda (?p (ELEMENT boolean)) (?q (ELEMENT boolean)) .
                                    (lambda (?x ELEMENT) .
                                            (and (?p ?x) (not (?q ?x))))))
                (symmetric_difference
		 (lambda (?p (ELEMENT boolean)) (?q (ELEMENT boolean)) .
			 (lambda (?x ELEMENT) .
				 (or (and (?p ?x) (not (?q ?x)))
				     (and (?q ?x) (not (?p ?x)))))))
                (subset (lambda (?p (ELEMENT boolean)) (?q (ELEMENT boolean)) .
                                (forall (?x ELEMENT) . (implies (?p ?x) (?q ?x))))))

 :assumption (and (in normal POSITION)(in reverse POSITION)(in void POSITION)(distinct normal reverse void )(forall (e1 Int)(implies (in e1 POSITION)(or (= e1 normal)(= e1 reverse)(= e1 void)) ) ) ) 
 :assumption (and (not (= normal reverse)) (not (= normal void)) (not (= reverse void)))
 :assumption (in actual_pos POSITION)
;;INVARIANT
 :formula (not 
	(implies ((and (not (= normal reverse)) (not (= normal void)) (not (= reverse void)))) (exists actual_pos(in actual_pos POSITION)))	
)
)