7ea448352f44eec95bc3e5dcf6f59a4b5dbc5f79Christian Maeder(((~((([]((((p1/\[]p1)/\p1)->p2)\/(~p1->~([]p2/\p2)))/\[]([](((p1/\[]p1)/\p1)->p2)\/(~p1->~([]p2/\p2))))/\[]((((p1/\[]p1)/\p1)->p2)\/[](~p1->~([]p2/\p2))))->([](((p1/\[]p1)/\p1)->p2)\/[](~p1->~([]p2/\p2))))\/~((([]((((p2/\[]p2)/\p2)->p3)\/(~p2->~([]p3/\p3)))/\[]([](((p2/\[]p2)/\p2)->p3)\/(~p2->~([]p3/\p3))))/\[]((((p2/\[]p2)/\p2)->p3)\/[](~p2->~([]p3/\p3))))->([](((p2/\[]p2)/\p2)->p3)\/[](~p2->~([]p3/\p3)))))\/([]((p8/\[]p8)->p8)\/[]((p8/\[]p8)->p8)))\/(((((~((([]((((p3/\[]p3)/\p3)->p4)\/(~p3->~([]p4/\p4)))/\[]([](((p3/\[]p3)/\p3)->p4)\/(~p3->~([]p4/\p4))))/\[]((((p3/\[]p3)/\p3)->p4)\/[](~p3->~([]p4/\p4))))->([](((p3/\[]p3)/\p3)->p4)\/[](~p3->~([]p4/\p4))))\/~((([]((((p4/\[]p4)/\p4)->p5)\/(~p4->~([]p5/\p5)))/\[]([](((p4/\[]p4)/\p4)->p5)\/(~p4->~([]p5/\p5))))/\[]((((p4/\[]p4)/\p4)->p5)\/[](~p4->~([]p5/\p5))))->([](((p4/\[]p4)/\p4)->p5)\/[](~p4->~([]p5/\p5)))))\/~((([]((((p5/\[]p5)/\p5)->p6)\/(~p5->~([]p6/\p6)))/\[]([](((p5/\[]p5)/\p5)->p6)\/(~p5->~([]p6/\p6))))/\[]((((p5/\[]p5)/\p5)->p6)\/[](~p5->~([]p6/\p6))))->([](((p5/\[]p5)/\p5)->p6)\/[](~p5->~([]p6/\p6)))))\/~((([]((((p6/\[]p6)/\p6)->p7)\/(~p6->~([]p7/\p7)))/\[]([](((p6/\[]p6)/\p6)->p7)\/(~p6->~([]p7/\p7))))/\[]((((p6/\[]p6)/\p6)->p7)\/[](~p6->~([]p7/\p7))))->([](((p6/\[]p6)/\p6)->p7)\/[](~p6->~([]p7/\p7)))))\/~((([]((((p7/\[]p7)/\p7)->p8)\/(~p7->~([]p8/\p8)))/\[]([](((p7/\[]p7)/\p7)->p8)\/(~p7->~([]p8/\p8))))/\[]((((p7/\[]p7)/\p7)->p8)\/[](~p7->~([]p8/\p8))))->([](((p7/\[]p7)/\p7)->p8)\/[](~p7->~([]p8/\p8)))))\/~((([]((((p8/\[]p8)/\p8)->p9)\/(~p8->~([]p9/\p9)))/\[]([](((p8/\[]p8)/\p8)->p9)\/(~p8->~([]p9/\p9))))/\[]((((p8/\[]p8)/\p8)->p9)\/[](~p8->~([]p9/\p9))))->([](((p8/\[]p8)/\p8)->p9)\/[](~p8->~([]p9/\p9))))))