((((([]p1\/[]p2)\/[]p3)\/[]p5)\/(((((((((((((((((((((((((((((((((((((((((((((((((((((((<>(~p1/\[]p3)\/<>(~p1/\[]p5))\/F)\/(<>(~p2/\[]p1)\/F))\/((<>(~p3/\[]p3)\/<>(~p3/\[]p5))\/F))\/(F\/F))\/((<>(~p5/\[]p3)\/<>(~p5/\[]p5))\/F))\/(F\/F))\/((((<><>(~p1/\[]p1)\/<><>(~p1/\[]p3))\/<><>(~p1/\[]p6))\/<><>(~p1/\[]p5))\/F))\/(F\/(<>(~p4/\[]p2)\/<>(~p6/\[]p2))))\/(((<><>(~p3/\[]p1)\/<><>(~p3/\[]p3))\/<><>(~p3/\[]p5))\/F))\/(F\/(<>(~p4/\[]p4)\/<>(~p6/\[]p4))))\/(((<><>(~p5/\[]p1)\/<><>(~p5/\[]p3))\/<><>(~p5/\[]p5))\/F))\/(F\/(<>(~p4/\[]p6)\/<>(~p6/\[]p6))))\/((<><><>(~p1/\[]p1)\/<><><>(~p1/\[]p3))\/F))\/(F\/((<><>(~p2/\[]p2)\/<><>(~p4/\[]p2))\/<><>(~p6/\[]p2))))\/((<><><>(~p3/\[]p1)\/<><><>(~p3/\[]p3))\/F))\/(F\/((<><>(~p2/\[]p4)\/<><>(~p4/\[]p4))\/<><>(~p6/\[]p4))))\/((<><><>(~p5/\[]p1)\/<><><>(~p5/\[]p3))\/F))\/(<><><>(~p6/\[]p5)\/((<><>(~p2/\[]p6)\/<><>(~p4/\[]p6))\/<><>(~p6/\[]p6))))\/(((<><><><>(~p1/\[]p1)\/<><><><>(~p1/\[]p3))\/<><><><>(~p1/\[]p5))\/F))\/(F\/(<><><>(~p2/\[]p2)\/<><><>(~p4/\[]p2))))\/(((<><><><>(~p3/\[]p1)\/<><><><>(~p3/\[]p3))\/<><><><>(~p3/\[]p5))\/F))\/(F\/(<><><>(~p2/\[]p4)\/<><><>(~p4/\[]p4))))\/((((<><><><>(~p5/\[]p1)\/<><><><>(~p5/\[]p3))\/<><><><>(~p5/\[]p2))\/<><><><>(~p5/\[]p5))\/F))\/(F\/(<><><>(~p2/\[]p6)\/<><><>(~p4/\[]p6))))\/((<><><><><>(~p1/\[]p1)\/<><><><><>(~p1/\[]p3))\/F))\/(<><><><><>(~p2/\[]p5)\/((<><><><>(~p2/\[]p2)\/<><><><>(~p4/\[]p2))\/<><><><>(~p6/\[]p2))))\/((<><><><><>(~p3/\[]p1)\/<><><><><>(~p3/\[]p3))\/F))\/(F\/((<><><><>(~p2/\[]p4)\/<><><><>(~p4/\[]p4))\/<><><><>(~p6/\[]p4))))\/((<><><><><>(~p5/\[]p1)\/<><><><><>(~p5/\[]p3))\/F))\/(F\/((<><><><>(~p2/\[]p6)\/<><><><>(~p4/\[]p6))\/<><><><>(~p6/\[]p6))))\/(((<><><><><><>(~p1/\[]p1)\/<><><><><><>(~p1/\[]p3))\/<><><><><><>(~p1/\[]p5))\/F))\/(F\/(<><><><><>(~p4/\[]p2)\/<><><><><>(~p6/\[]p2))))\/(((<><><><><><>(~p3/\[]p1)\/<><><><><><>(~p3/\[]p3))\/<><><><><><>(~p3/\[]p5))\/F))\/(F\/(<><><><><>(~p4/\[]p4)\/<><><><><>(~p6/\[]p4))))\/((((<><><><><><>(~p5/\[]p1)\/<><><><><><>(~p5/\[]p3))\/<><><><><><>(~p5/\[]p2))\/<><><><><><>(~p5/\[]p5))\/F))\/(F\/(<><><><><>(~p4/\[]p6)\/<><><><><>(~p6/\[]p6))))\/((<><><><><><><>(~p1/\[]p1)\/<><><><><><><>(~p1/\[]p3))\/F))\/(<><><><><><><>(~p2/\[]p5)\/((<><><><><><>(~p2/\[]p2)\/<><><><><><>(~p4/\[]p2))\/<><><><><><>(~p6/\[]p2))))\/((<><><><><><><>(~p3/\[]p1)\/<><><><><><><>(~p3/\[]p3))\/F))\/(F\/((<><><><><><>(~p2/\[]p4)\/<><><><><><>(~p4/\[]p4))\/<><><><><><>(~p6/\[]p4))))\/((<><><><><><><>(~p5/\[]p1)\/<><><><><><><>(~p5/\[]p3))\/F))\/(F\/((<><><><><><>(~p2/\[]p6)\/<><><><><><>(~p4/\[]p6))\/<><><><><><>(~p6/\[]p6))))\/(((<><><><><><><><>(~p1/\[]p1)\/<><><><><><><><>(~p1/\[]p3))\/<><><><><><><><>(~p1/\[]p5))\/F))\/(F\/(<><><><><><><>(~p4/\[]p2)\/<><><><><><><>(~p6/\[]p2))))\/(((<><><><><><><><>(~p3/\[]p1)\/<><><><><><><><>(~p3/\[]p3))\/<><><><><><><><>(~p3/\[]p5))\/F))\/(F\/(<><><><><><><>(~p4/\[]p4)\/<><><><><><><>(~p6/\[]p4))))\/((((<><><><><><><><>(~p5/\[]p1)\/<><><><><><><><>(~p5/\[]p3))\/<><><><><><><><>(~p5/\[]p2))\/<><><><><><><><>(~p5/\[]p5))\/F))\/(F\/(<><><><><><><>(~p4/\[]p6)\/<><><><><><><>(~p6/\[]p6))))\/(F\/F))\/(F\/((<><><><><><><><>(~p2/\[]p2)\/<><><><><><><><>(~p4/\[]p2))\/<><><><><><><><>(~p6/\[]p2))))\/(F\/F))\/(F\/((<><><><><><><><>(~p2/\[]p4)\/<><><><><><><><>(~p4/\[]p4))\/<><><><><><><><>(~p6/\[]p4))))\/(F\/F))\/(F\/((<><><><><><><><>(~p2/\[]p6)\/<><><><><><><><>(~p4/\[]p6))\/<><><><><><><><>(~p6/\[]p6)))))\/(((<><><><><><><><><>~p2\/<><><><><><><><><>~p4)\/<><><><><><><><><>~p2)\/<><><><><><><><><>~p6))