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