In001
Premises:
(or (not (Q ?X)) (P ?X) (P a)) (not (P B)) (Q B)
Conclusion:
(P a)
Proof Trace