(p A (p->q)) -> q
(¬q A (p->q)) -> ¬p
((q->r) A (r->p)) -> (q->p)
((pVq) A ¬q) -> p
p -> (pVq)
(pVq) -> p
((p) A (q)) -> (pAq)
((pVq) A (¬pVr) -> (qVr)
