((((((((~([]((<>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)))))\/(~([]((<>p3/\[]<>p3)->p4)\/[]((p4/\[]p4)-><>p3))\/~([](((p3->[]p4)/\[](p3->[]p4))->p4)\/[]((p4/\[]p4)->(p3->[]p4)))))\/(~([]((<>p4/\[]<>p4)->p5)\/[]((p5/\[]p5)-><>p4))\/~([](((p4->[]p5)/\[](p4->[]p5))->p5)\/[]((p5/\[]p5)->(p4->[]p5)))))\/(~([]((<>p5/\[]<>p5)->p6)\/[]((p6/\[]p6)-><>p5))\/~([](((p5->[]p6)/\[](p5->[]p6))->p6)\/[]((p6/\[]p6)->(p5->[]p6)))))\/(~([]((<>p6/\[]<>p6)->p7)\/[]((p7/\[]p7)-><>p6))\/~([](((p6->[]p7)/\[](p6->[]p7))->p7)\/[]((p7/\[]p7)->(p6->[]p7)))))\/([]([]p4->p4)\/[]([]p4->p4)))\/(((((~([]((<>p8/\[]<>p8)->p9)\/[]((p9/\[]p9)-><>p8))\/~([](((p8->[]p9)/\[](p8->[]p9))->p9)\/[]((p9/\[]p9)->(p8->[]p9))))\/(~([]((<>p9/\[]<>p9)->p10)\/[]((p10/\[]p10)-><>p9))\/~([](((p9->[]p10)/\[](p9->[]p10))->p10)\/[]((p10/\[]p10)->(p9->[]p10)))))\/(~([]((<>p10/\[]<>p10)->p11)\/[]((p11/\[]p11)-><>p10))\/~([](((p10->[]p11)/\[](p10->[]p11))->p11)\/[]((p11/\[]p11)->(p10->[]p11)))))\/(~([]((<>p11/\[]<>p11)->p12)\/[]((p12/\[]p12)-><>p11))\/~([](((p11->[]p12)/\[](p11->[]p12))->p12)\/[]((p12/\[]p12)->(p11->[]p12)))))\/(~([]((<>p12/\[]<>p12)->p13)\/[]((p13/\[]p13)-><>p12))\/~([](((p12->[]p13)/\[](p12->[]p13))->p13)\/[]((p13/\[]p13)->(p12->[]p13))))))