This is a DPLL algorithm with a logic parser. You can create propositional logic phrases and it will test if the result is true or not.