(p1 <=> (q1 <=> (p1 /\ ~p1))) (p2 <=> (q2 <=> ((p1 /\ q1) \/ ((p1 /\ (p1 /\ ~p1)) \/ (q1 /\ (p1 /\ ~p1)))))) (p3 <=> (q3 <=> ((p2 /\ q2) \/ ((p2 /\ ((p1 /\ q1) \/ ((p1 /\ (p1 /\ ~p1)) \/ (q1 /\ (p1 /\ ~p1))))) \/ (q2 /\ ((p1 /\ q1) \/ ((p1 /\ (p1 /\ ~p1)) \/ (q1 /\ (p1 /\ ~p1))))))))) ((p3 /\ q3) \/ ((p3 /\ ((p2 /\ q2) \/ ((p2 /\ ((p1 /\ q1) \/ ((p1 /\ (p1 /\ ~p1)) \/ (q1 /\ (p1 /\ ~p1))))) \/ (q2 /\ ((p1 /\ q1) \/ ((p1 /\ (p1 /\ ~p1)) \/ (q1 /\ (p1 /\ ~p1)))))))) \/ (q3 /\ ((p2 /\ q2) \/ ((p2 /\ ((~p1 /\ q1) \/ ((p1 /\ (p1 /\ ~p1)) \/ (q1 /\ (p1 /\ ~p1))))) \/ (q2 /\ ((p1 /\ q1) \/ ((p1 /\ (p1 /\ ~p1)) \/ (q1 /\ (p1 /\ ~p1))))))))))