;;Proof Obligations of Module in Harvey/SMT Language
(benchmark switch1Operation3
  :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 actual_pos POSITION)) (-> (and (in reverse {m1,m2,m3}) (notin normal {m1,m2,m3})) (in actual_pos 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 actual_pos POSITION)))))
	)
)