S54   ~P->P -| |- P     S55   P <-> Q -| |- ~((P->Q)->~(Q->P))       S56   P <-> Q -| |- P v Q->P & Q       S57   P <-> Q -| |- ~(P v Q) v ~(~P v ~Q)     S58   P <-> Q -| |- ~(P & Q)->~(P v Q)     S59   P <-> Q -| |- ~(~(P & Q) & ~(~P & ~Q))       S60   P v Q->R & ~P , Q v R, ~R |- C       61   ~P <-> Q, P->R, ~R |- ~Q <-> R       S62   ~((P <-> ~Q) <-> R), S->P & (Q & T), R v (P& S) |- S & K->R & Q       S63   (P & Q) v (R v S) |- ((P & Q) v R) v S       S64   P & (~Q & ~R), P->(~S->T), ~S->(T <-> R v Q)|- S       S65   P & ~Q->~R, (~S->~P) <-> ~R |- R <-> Q & (P & ~S)       S66   P v Q, (Q->R) & (~P v S), Q & R->T |- T v S       S67   P->Q v R, (~Q & S) v (T->~P), ~(~R->~P) |- ~T & Q       S68   P v Q, P->(R->~S), (~R <-> T)->~P |- S & T->Q       S69   (P <-> ~Q)->~R, (~P & S) v (Q & T), S v T->R |- Q->P       S70   ~S v (S & R), (S->R)->P |- P       S71   P v (R v Q), (R->S) & (Q->T), S v T->P v Q, ~P |- Q       S72   (P->Q)->R, S->(~Q->T) |- R v ~T->(S->R)       S73   P & Q->R v S |- (P->R) v (Q->S)       S74   (P->Q) & (R->P), (P v R) & ~(Q & R) |- (P & Q) & ~R       S75   P & Q->(R v S) & ~(R & S), R & Q->S,S->((R & Q) v (~R & ~Q)) v ~P |- P->~Q       S76   ~(P & ~Q) v ~(~R & ~S), ~S & ~Q, T->(~S->~R & P) |- ~T