a209694d7694b93e56927c6aacc3f5b9366fdb8fChristian Maeder((((<>~([]~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)\/[](~[]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)\/<>((<>([]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))))\/<>([]<>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)))\/<>p4)