((((<>~([]~p1->[][]~p1)\/[]((<>~([]~p1->[][]~p1)\/[]((<>~([]~p1->[][]~p1)\/[]((<>~([]~p1->[][]~p1)\/[]((<>~([]~p1->[][]~p1)\/[]((<>~([]~p1->[][]~p1)\/[]((<>~([]~p1->[][]~p1)\/[]((<>~([]~p1->[][]~p1)\/[]((<>~([]~p1->[][]~p1)\/[]<>[]p0)\/[](~[]p1->[]~[]p1)))\/[](~[]p1->[]~[]p1)))\/[](~[]p1->[]~[]p1)))\/[](~[]p1->[]~[]p1)))\/[](~[]p1->[]~[]p1)))\/[](~[]p1->[]~[]p1)))\/[](~[]p1->[]~[]p1)))\/[](~[]p1->[]~[]p1)))\/[](~[]p1->[]~[]p1))\/((<>([]p1/\<><>~p1)\/<>((<>([]p1/\<><>~p1)\/<>((<>([]p1/\<><>~p1)\/<>((<>([]p1/\<><>~p1)\/<>((<>([]p1/\<><>~p1)\/<>((<>([]p1/\<><>~p1)\/<>((<>([]p1/\<><>~p1)\/<>((<>([]p1/\<><>~p1)\/<>((<>([]p1/\<><>~p1)\/<>((((([]<>p0/\[](~p0\/[]p3))\/<>([]<>[](~p0\/[]p3)/\[]<>p0))\/([]<>p0/\<><>[](~p0\/[]p3)))\/<>((<>[]<>p0/\p0)/\<>(~p0\/[]p3)))\/<>[](~p0\/[]p3)))\/<>([]<>p1/\<><>[]~p1)))\/<>([]<>p1/\<><>[]~p1)))\/<>([]<>p1/\<><>[]~p1)))\/<>([]<>p1/\<><>[]~p1)))\/<>([]<>p1/\<><>[]~p1)))\/<>([]<>p1/\<><>[]~p1)))\/<>([]<>p1/\<><>[]~p1)))\/<>([]<>p1/\<><>[]~p1)))\/<>([]<>p1/\<><>[]~p1)))\/<>p4)