Logichard
0:00.0

Consider the following set of propositional clauses in a resolution proof system:

  1. PQ¬RP \lor Q \lor \neg R
  2. egPS eg P \lor S
  3. egQS eg Q \lor S
  4. RR
  5. egS eg S

What is the minimum number of resolution steps required to derive the empty clause (\square)?