;;Proof Obligations of Module in Harvey/SMT Language
(benchmark switch1Operation2
  :logic UNKNOWN  
;;OPERATIONS
  :formula ((forall POSITION normal reverse void actual_pos m1 m2 m3 
              (-> (and (in POSITION (power1 INTEGER)) 
	               (seteq POSITION {normal,reverse,void}) 
		       (and (nseteq normal reverse) (nseteq normal void) (nseteq reverse void)) 
		       (in actual_pos POSITION) 
		       (and (in m1 POSITION) (in m2 POSITION) (in m3 POSITION)))
		       
	               (and (-> (and (in normal {m1,m2,m3}) (notin reverse {m1,m2,m3}))
		       
		                (in normal POSITION)) 
		             (-> (and (in reverse {m1,m2,m3}) (notin normal {m1,m2,m3})) 
			         (in reverse POSITION)) 
				   (-> (not (or (and (in normal {m1,m2,m3}) (notin reverse {m1,m2,m3})) (and (in reverse {m1,m2,m3}) (notin normal {m1,m2,m3}))))
				       (in void POSITION)))))
	)
)