A satisfiability solver written in Racket that determines whether a logical statement is provable when entered in conjunctive normal form using DFS algorithm