changed cnf implementation to handle [Form] when applying distribution laws. Result seems to be in CNF, however it contains nested conjunction and disjunctions, should be simplified i think?