logictree solves propositional formulas and tries to solve predicate formulas, using semantic tableaux.