;;Proof Obligations of Module in Harvey/SMT Language
(benchmark switch1Initialization1
  :logic UNKNOWN  
;;INITIALIZATION
  :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))) (forall actual_pos1(-> (in actual_pos1 POSITION) (in POSITION POSITION)))))
	)
)