;;Proof Obligations of Module in Harvey/SMT Language
(benchmark switch1Operation2
 :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 (e3 Int)(implies (in e3 POSITION)(or (= e3 normal)(= e3 reverse)(= e3 void)) ) ) ) 
 :assumption (and (not (= normal reverse)) (not (= normal void)) (not (= reverse void)))
 :assumption (in actual_pos POSITION)
;;OPERATIONS
 :formula (not 
	(forall 
	(m1 Int) (m2 Int) (m3 Int) 
	 (implies ( true ) (and (implies (and (in normal (union (union (singleton m1) (singleton m2 ))(union (singleton m3) ))) (not  (in reverse (union (union (singleton m1) (singleton m2 ))(union (singleton m3) ))))) (in normal POSITION)) (implies (and (in reverse (union (union (singleton m1) (singleton m2 ))(union (singleton m3) ))) (not  (in normal (union (union (singleton m1) (singleton m2 ))(union (singleton m3) ))))) (in reverse POSITION)) (implies (not (or (and (in normal (union (union (singleton m1) (singleton m2 ))(union (singleton m3) ))) (not  (in reverse (union (union (singleton m1) (singleton m2 ))(union (singleton m3) ))))) (and (in reverse (union (union (singleton m1) (singleton m2 ))(union (singleton m3) ))) (not  (in normal (union (union (singleton m1) (singleton m2 ))(union (singleton m3) ))))))) (in void POSITION)))))	
)
)