F1: (( Q or T ) or S ) iff R ( Q or S ) or (( S implies R ) or T ) not R and ((( P iff S ) or P ) or S ) ( Q and ( T implies not P )) implies T ( P implies R ) and ( T or ( P implies not S )) not ((( P implies ( P implies Q )) iff S ) implies T ) P and ((( S iff P ) and ( S implies ( Q implies P ))) or S ) not (( not S implies P ) or Q ) not ( T iff Q ) and R not ((( Q implies not S ) implies Q ) and P ) F2: T iff ( Q or ( P iff T )) ( P implies (( S or ( P implies R )) iff Q )) and (( P iff R ) implies P ) ( T iff ( P iff not S )) iff ( not ( not T iff S ) iff ( S implies P )) not S or ( R or (( T and Q ) iff S )) P iff ( R or ( P implies T )) ( not R and S ) and (( R iff S ) implies R ) (( Q implies ( P and T )) or not ( not T and P )) and ( P implies T ) (( R implies (( S or P ) and Q )) implies P ) or R ( not T and ( Q implies ( R iff ( P or Q )))) implies ( R and not S ) ( T iff S ) and ( S and not S ) F3: ( Q and not T ) and ( T and S ) (( Q implies not S ) and ( R and ( P and T ))) or S S or (( T implies P ) implies ( S or T )) ( R and ( R iff T )) iff not S not ( R iff (( Q and P ) implies not R )) ( Q implies ( S implies R )) iff ( T iff P ) not ( Q implies (( T or Q ) iff S )) ( T and not P ) iff (( S and T ) implies R ) ( P implies R ) and ( T iff ( R and ( R or S ))) not ( S or ( not P and Q )) implies R F4: ( S iff not T ) implies S ( P and T ) or ( not Q iff P ) ( not T or S ) iff not ( S and T ) ( R iff ( Q and ( S and P ))) implies Q not ( not T or P ) (( P iff S ) implies ( R or S )) and not ( T or R ) ( P iff (( T and P ) and R )) iff P R implies ( not S or R ) not ( Q and not ( P and S )) Q implies (( T or Q ) implies ( Q and P )) F5: not ( not S and R ) not ( Q and ( R iff ( not Q and P ))) (( T or ( P implies ( Q implies S ))) iff R ) iff (( S and R ) iff T ) ( S implies P ) iff ( P iff ( S or ( Q or S ))) Q or ( P implies ( not ( Q or S ) and ( T iff S ))) ( not S or Q ) implies Q ( R iff S ) implies (((( R and S ) implies S ) iff R ) implies S ) (( Q implies ( not Q implies R )) iff R ) or ( S or P ) (( S implies R ) iff R ) iff ( Q and R ) not ( S iff ( T implies Q ))