wang's theorem to prove theorems in propositonal calculus
  Label Sequent                 Comment
  S1:   P ? Q, Q ? R, ¬R ? ¬P   Initial sequent.
  S2:   ¬P ? Q, ¬Q ? R, ¬R ? ¬P Two applications of R5.
  S3:   ¬P ? Q, ¬Q ? R ? ¬P, R  Rl.
  S4:   ¬P, ¬Q ? R ? ¬P, R      S4 and S5 are obtained from S3 with
                                R3. Note that S4 is an axiom since P
                                appears on both sides of the sequent ar-
                                row at the top level.
  S5:   Q, ¬Q ? R ? ¬P, R       The other sequent generated by the ap-
                                plication of R3.
  S6:   Q, ¬Q ? ¬P, R           S6 and S7 are obtained from S5 using
                                R3.
  S7:   Q, R ? ¬P, R            This is an axiom.
  S8:   Q ? ¬P, R, Q            Obtained from S6 using R1. S8 is an
                                axiom. The original sequent is now
                                proved, since it has successfully been
                                transformed into a set of three axioms
                                with no unproved sequents left over.
//R1,R2,R3,R4,R5 is transformation

myhomework is so complicate as you can see and i must finish homework in 4 days i just want help ,can you show me how i should construct the algorithm or how i should take and store the input