#(P/\Q \/ !P/\!Q#) <-> R /**/
<=> (P/\Q \/ !P/\!Q) /\ R \/ !(P/\Q \/ !P/\!Q) /\ !R /**/
<=> P/\Q/\R \/ !P/\!Q/\R \/ #(!(P/\Q) /\ !(!P/\!Q)#) /\ !R /**/
<=> P/\Q/\R \/ !P/\!Q/\R \/ (!P\/!Q) /\ (P\/Q) /\ !R /**/
<=> P/\Q/\R \/ !P/\!Q/\R \/ (!P/\P \/ !P/\Q \/ !Q/\P \/ !Q/\Q) /\ !R /**/
<=> P/\Q/\R \/ !P/\!Q/\R \/ (FF \/ !P/\Q \/ !Q/\P \/ FF) /\ !R /**/
<=> P/\Q/\R \/ !P/\!Q/\R \/ (!P/\Q \/ !Q/\P) /\ !R /**/
<=> P/\Q/\R \/ !P/\!Q/\R \/ !P/\Q/\!R \/ P/\!Q/\!R /**/
<=> P /\ (Q/\R \/ !Q/\!R) \/ !P /\ (!Q/\R \/ Q/\!R) /**/
<=> P /\ #( Q<->R #) \/ !P /\ #((Q\/R) /\ (!Q\/!R)#) /**/
<=> P /\ #( Q<->R #) \/ !P /\ !(Q/\R \/ !Q/\!R) /**/
<=> P /\ #( Q<->R #) \/ !P /\ !(Q <-> R ) /**/
<=> P <-> #( Q<->R #)
prop_logic
/* Another solution to the previous problem */
#(P <-> Q#) <-> R /**/
<=> Q /\ (#(P <-> TT#) <-> R) \/ !Q /\ (#(P <-> FF#) <-> R) /**/
<=> Q /\ (P <-> R) \/ !Q /\ (!P <-> R) /**/
<=> Q /\ (P <-> R) \/ !Q /\ (P <-> !R) /**/
<=> Q /\ (P <-> #(TT <-> R#)) \/ !Q /\ (P <-> #(FF <-> R#)) /**/
<=> Q /\ (P <-> #(Q <-> R#)) \/ !Q /\ (P <-> #(Q <-> R#)) /**/
<=> P <-> #(Q <-> R#)