| 
             
              |  | q  ¬[(p  q)  (r  t)] |   
              |  |  |  | 
             
              |  | (r  t)  ¬(p  q) |   
              |  |  |  | 
       
        | 
 | 
       
        | 
             
              |  | [q  (q  r)]  [¬(q  r)  ¬r] |   
              |  |  |  | 
             
              |  | [p  (q  r)]  [¬p  (q  r)] |   
              |  |  |  | 
       
        | 
 | 
       
        | 
             
              |  | ¬[(p  r)  (¬p  ¬¬q)] |   
              |  |  |  | 
             
              |  | {p  [(p  q)  (q  r)]}  s |   
              |  |  |  | 
       
        | 
 | 
       
        | 
             
              |  | [(p  q)  ¬r]  ¬¬[q  (q  r)] |   
              |  |  |  | 
             
              |  | ¬p  [p  (q  r)] |   
              |  |  |  | 
       
        | 
 | 
       
        | 
             
              |  | [(p  r)  (r  s)]  (p  ¬¬q) |   
              |  |  |  | 
             
              |  | [(p  q)  (p  r)]  ¬(p  s) |   
              |  |  |  | 
       
        | 
 | 
       
        | 
             
              |  | r  [q  (q  r)] |   
              |  |  |  | 
             
              |  | ¬¬q  [p  ¬(r)] |   
              |  |  |  | 
       
        | 
 | 
       
        | 
             
              |  | (r  s)  (p  r) |   
              |  |  |  | 
             
              |  | r  ¬{(p  ¬¬q)  [(p  r)  (r  s)]} |   
              |  |  |  |