This program will convert propositional formulae of a given JSON input format into an equisatisfiable conjunctive normal form. There are three different algorithms implemented to do the conversion. One of them uses paths through matrices.