S11    P  -| |- ~~P    S12    P->Q, ~Q |- ~P
S13   P->~Q, Q |- ~P   S14  ~P->Q, ~Q |- P   S15   ~P->~Q, Q |- P   S16   P->Q, Q->R |- P->R   S17   P |- Q->P   S18   ~P |- P->Q    S19   P |- ~P->Q    S20    P->Q, P->~ Q |- ~P   S21 ~P v Q -| |- P -> Q   S22   P v Q -| |- ~P->Q    S23   P v Q -| |- ~Q->P   S24   P v ~Q -| |- Q->P   S25   P v Q, P->R, Q->R |- R   S26   P v Q, P->R, Q->S |- R v S   S27   P->Q, ~P->Q |- Q   S28   ~(P v Q) -| |- ~P   S29   ~(P & Q) -| |- ~P v ~Q   S30   P & Q -| |- ~(~P v ~Q)   S31   P v Q -| |- ~(~P & ~Q)   S32   ~(P->Q) -| |- P & ~Q   S33   ~(P->~Q) -| |- P & Q   S34   P->Q -| |- ~(P & ~Q)   S35   P->~Q -| |- ~(P & Q)   S36   P & Q -| |- Q & P   S37   P v Q -| |- Q v P   S38   P <-> Q -| |- Q <-> P   S39   P->Q -| |- ~Q->~P   S40   P & (Q & R) -| |- (P & Q) & R   S41   P v (Q v R) -| |- (P v Q) v R   S42   P & (Q v R) -| |- (P & Q) v (P & R)   S43   P v (Q & R) -| |- (P v Q) & (P v R)   S44   P->(Q->R) -| |- P & Q->R   S45   P <-> Q, P |- Q   S46   P <-> Q, Q |- P   S47   P <-> Q, ~P |- ~Q   S48   P <-> Q, ~Q |- ~P   S49   P <-> Q -| |- ~Q <-> ~P   S50   P <-> ~Q -| |- ~P <-> Q   S51   ~(P <-> Q) -| |- P <-> ~Q   S52   ~(P <-> Q) -| |- ~P <-> Q   S53   P <-> Q -| |- (P & Q) v (~P & ~Q)   S54   P->Q & R, R v ~Q->S & T, T <-> U |- P->U   S55   (~P v Q) & R, Q->S |- P->(R->S)   S56   Q & R, Q->P v S, ~(S & R) |- P   S57   P->R & Q, S->~R v ~Q |- S & P->T   S58   R & P, R->(S v Q), ~(Q & P) |- S   S59   P & Q, R & ~S, Q->(P->T), T->(R->S v W) |- W   S60   R->~P, Q, Q->(P v ~S) |- S->~R   S61   P->Q, P->R, P->S, T->(U->(~V->~S)), Q->T, R->(W->U), V->~W, W |- ~P   S62   P <-> ~Q & S, P & (~T->~S) |- ~Q & T   S63   P v Q <-> P & Q |- P <-> Q   S64   ~P->P -| |- P     S65   P <-> Q -| |- ~((P->Q)->~(Q->P))       S66   P <-> Q -| |- P v Q->P & Q       S67   P <-> Q -| |- ~(P v Q) v ~(~P v ~Q)     S68   P <-> Q -| |- ~(P & Q)->~(P v Q)     S69   P <-> Q -| |- ~(~(P & Q) & ~(~P & ~Q))       S70   P v Q->R & ~P , Q v R, ~R |- C       S71   ~P <-> Q, P->R, ~R |- ~Q <-> R       S72   ~((P <-> ~Q) <-> R), S->P & (Q & T), R v (P& S) |- S & K->R & Q       S73   (P & Q) v (R v S) |- ((P & Q) v R) v S       S74   P & (~Q & ~R), P->(~S->T), ~S->(T <-> R v Q)|- S       S75   P & ~Q->~R, (~S->~P) <-> ~R |- R <-> Q & (P & ~S)       S76   P v Q, (Q->R) & (~P v S), Q & R->T |- T v S       S77   P->Q v R, (~Q & S) v (T->~P), ~(~R->~P) |- ~T & Q       S78   P v Q, P->(R->~S), (~R <-> T)->~P |- S & T->Q       S79   (P <-> ~Q)->~R, (~P & S) v (Q & T), S v T->R |- Q->P       S80   ~S v (S & R), (S->R)->P |- P       S81   P v (R v Q), (R->S) & (Q->T), S v T->P v Q, ~P |- Q       S82   (P->Q)->R, S->(~Q->T) |- R v ~T->(S->R)       S83   P & Q->R v S |- (P->R) v (Q->S)       S84   (P->Q) & (R->P), (P v R) & ~(Q & R) |- (P & Q) & ~R       S85   P & Q->(R v S) & ~(R & S), R & Q->S,S->((R & Q) v (~R & ~Q)) v ~P |- P->~Q       S86   ~(P & ~Q) v ~(~R & ~S), ~S & ~Q, T->(~S->~R & P) |- ~T