;;Proof Obligations of Module in Harvey/SMT Language
(benchmark switch1Invariant0
  :logic UNKNOWN  
;;INVARIANT
  :formula (
(forall POSITION normal reverse void(-> (and (in POSITION (power1 INTEGER)) (seteq POSITION {normal,reverse,void}) (and (nseteq normal reverse) (nseteq normal void) (nseteq reverse void))) (exists actual_pos(in actual_pos POSITION))))
	)
)