Doesn&#x27;t Prolog support only Horn clauses?  This proof system supports arbitrary propositions in conjunctive normal form.  There are also no quantifiers or predicates here: the logic is purely propositional.