k_t4p_n_07.in revision 027d68858fd4bbb565ca2aa7ce026dc60c8cf881
((((<>~([]~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)\/<>(((([]<>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)))\/<>p4)