abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder((((~([]((<>p1/\[]<>p1)->p2)\/[]((p2/\[]p2)-><>p1))\/~([](((p1->[]p2)/\[](p1->[]p2))->p2)\/[]((p2/\[]p2)->(p1->[]p2))))\/(~([]((<>p2/\[]<>p2)->p3)\/[]((p3/\[]p3)-><>p2))\/~([](((p2->[]p3)/\[](p2->[]p3))->p3)\/[]((p3/\[]p3)->(p2->[]p3)))))\/([]([]p2->p2)\/[]([]p2->p2)))\/(~([]((<>p4/\[]<>p4)->p5)\/[]((p5/\[]p5)-><>p4))\/~([](((p4->[]p5)/\[](p4->[]p5))->p5)\/[]((p5/\[]p5)->(p4->[]p5)))))