Implement Automatic Theorem Prover for Propositional Calculus.
Create a system which takes any propositional calculus expression as input and
outputs whether the expression is a theorem or not.

note: Show the steps involved in the proof.