added commutative formula which alphabetizes its subformulas, switched disjunction and conjunction to implement; fixes #1