{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "In this notebook several methods for proving inequalities have been compared.\n",
    "\n",
    "First of all we need a dataset. 35 inequalities were selected from https://www.imomath.com/index.php?options=592&lmm=0. Each inequality is represented by a tuple: inequality (in LaTeX), inequality constraints (for example: $a\\in [0,1]$, equality constraints (for example: $abc=1$) and a function which converts inequality to a formula which we want to prove it's nonnegativity. In most cases when this function is simply a difference between left and right-hand side, but sometimes it's better to use difference between squares of sides (to get rid of square roots). These tuples are used as parameters in `parser` function which converts them to equivalent inequalities with default constraints (i.e. all variables are positive).\n",
    "\n",
    "Some tuples have less than 4 elements. In this case `parser` use default arguments."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "from sympy import *\n",
    "import shiroindev\n",
    "from shiroindev import *\n",
    "from sympy.parsing.latex import parse_latex\n",
    "shiro.seed=1\n",
    "from IPython.display import Latex\n",
    "shiro.display=lambda x:display(Latex(x))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "`sympy` has a `parse_latex` function which converts LaTeX formula to a `sympy` one. Unfortunately it doesn't deal with missing braces in the way that LaTeX do. For example `\\frac12` generates $\\frac12$ which is the same as `\\frac{1}{2}`, but `parse_latex` accepts only the second version. So here there is a boring function which adds missing braces."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\\frac{ \\sqrt {3}}{2}\n",
      "a^2+b^2+c^2\\geq ab+bc+ca\n"
     ]
    }
   ],
   "source": [
    "def addbraces(s):\n",
    "    arg={r'\\frac':2,r'\\sqrt':1}\n",
    "    s2=''\n",
    "    p=0\n",
    "    while 1:\n",
    "        m=re.search(r\"\\\\[a-zA-Z]+\", s[p:])\n",
    "        if not m:\n",
    "            break\n",
    "        s2+=s[p:p+m.end()]\n",
    "        p+=m.end()\n",
    "        if m.group() in arg:\n",
    "            for i in range(arg[m.group()]):\n",
    "                sp=re.search('^ *',s[p:])\n",
    "                s2+=sp.group()\n",
    "                p+=sp.end()\n",
    "                if s[p]=='{':\n",
    "                    cb=re.search(r'^\\{.*?\\}',s[p:])\n",
    "                    ab=addbraces(cb.group())\n",
    "                    s2+=ab\n",
    "                    p+=cb.end()\n",
    "                else:\n",
    "                    s2+='{'+s[p]+'}'\n",
    "                    p+=1\n",
    "    s2+=s[p:]\n",
    "    return s2\n",
    "print(addbraces(r'\\frac{ \\sqrt 3}2'))\n",
    "print(addbraces(r'a^2+b^2+c^2\\geq ab+bc+ca'))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [],
   "source": [
    "#(formula,intervals,subs,function)\n",
    "dif=lambda b,s:b-s\n",
    "dif2=lambda b,s:b*b-s*s\n",
    "ineqs=[\n",
    "    (r'a^2+b^2+c^2\\geq ab+bc+ca',),\n",
    "    (r'a^2+b^2+c^2+d^2\\geq a(b+c+d)',),\n",
    "    (r'1\\leq\\frac{a^2b^2}{c^2}+\\frac{b^2c^2}{a^2}+\\frac{c^2a^2}{b^2}',\n",
    "     '[0,1-f],[0,1]','[a,sqrt(1-e-f)],[b,sqrt(e)],[c,sqrt(f)]',),\n",
    "    (r'\\frac1{1-x^2}+\\frac1{1-y^2}\\geq \\frac2{1-xy}','[0,1],[0,1]'),\n",
    "    (r'a^3+b^3\\geq a^2b+ab^2',),\n",
    "    (r'\\frac a{b+c}+\\frac b{c+a}+\\frac c{a+b}\\geq \\frac32',),\n",
    "    (r'2a^3+b^3\\geq 3a^2b',),\n",
    "    (r'a^3+b^3+c^3\\geq a^2b+b^2c+c^2a',),\n",
    "    (r'\\frac a{b+c}+\\frac b{c+d}+ \\frac c{d+a}+ \\frac d{a+b}\\geq 2',),\n",
    "    (r'\\frac{a^3}{a^2+ab+b^2}+ \\frac{b^3}{b^2+bc+c^2}+ \\frac{c^3}{c^2+ca+a^2} \\geq \\frac{a+b+c}3',),\n",
    "    (r'\\sqrt{ab}+\\sqrt{cd}+\\sqrt{ef}\\leq\\sqrt{(a+c+e)(b+d+f)}','','',dif2),\n",
    "    (r'\\frac{5a^3-ab^2}{a+b}+\\frac{5b^3-bc^2}{b+c}+\\frac{5c^3-ca^2}{c+a}\\geq 2(a^2+b^2+c^2)',),\n",
    "    #(r'\\frac{a^2}{(1+b)(1-c)}+\\frac{b^3}{(1+c)(1-d)}+\\frac{c^3}{(1+d)(1-a)}+\\frac{d^3}{(1+a)(1-b)}\\geq\\frac1{15}',\n",
    "    # '[0,1-c-d],[0,1-d],[0,1]','[a,1-b-c-d]'),\n",
    "    (r'\\frac{x^3}{(1+y)(1+z)}+\\frac{y^3}{(1+z)(1+x)}+\\frac{z^3}{(1+x)(1+y)}\\geq\\frac{3}{4}','','[z,1/(x*y)]'),\n",
    "    (r'\\frac ab+\\frac bc+\\frac ca\\geq \\frac{(a+b+c)^2}{ab+bc+ca}',),\n",
    "    (r'\\frac{a^2}b+\\frac{b^2}c+\\frac{c^2}a\\geq \\frac{a^2+b^2+c^2}{a+b+c}',),\n",
    "    (r'\\frac{a^2}b+\\frac{b^2}c+\\frac{c^2}a\\geq a+b+c+\\frac{4(a-b)^2}{a+b+c}',),\n",
    "    (r'\\frac1{a^3+b^3+abc}+ \\frac1{b^3+c^3+abc} +\\frac1{c^3+a^3+ abc} \\leq \\frac1{abc}',),\n",
    "    (r'\\frac1{a^3(b+c)}+ \\frac1{b^3(c+a)}+ \\frac1{c^3(a+b)} \\geq \\frac32','','[c,1/(a*b)]'),\n",
    "    (r'\\frac{a^3}{b^2-bc+c^2}+\\frac{b^3}{c^2-ca+a^2} + \\frac{c^3}{a^2-ab+b^2} \\geq 3 \\cdot\\frac{ab+bc+ca}{a+b+c}',),\n",
    "    (r'\\frac{x^5-x^2}{x^5+y^2+z^2}+\\frac{y^5-y^2}{y^5+z^2+x^2}+\\frac{z^5-z^2}{z^5+x^2+y^2}\\geq0','','[x,1/(y*z)]'),\n",
    "    (r'(a+b-c)(b+c-a)(c+a-b)\\leq abc',),\n",
    "    (r'\\frac1{1+xy}+\\frac1{1+yz}+\\frac1{1+zx}\\leq \\frac34','','[x,(y+z)/(y*z-1)]'),\n",
    "    (r'\\frac{x\\sqrt x}{y+z}+\\frac{y\\sqrt y}{z+x}+\\frac{z\\sqrt z}{x+y}\\geq\\frac{ \\sqrt 3}2',\n",
    "     '[0,1-z],[0,1]','[x,1-y-z]'),\n",
    "    (r'a^4+b^4+c^4+d^4\\geq 4abcd',),\n",
    "    (r'\\frac{ab}{a+b}+\\frac{bc}{b+c}+\\frac{ca}{c+a}\\leq\\frac{3(ab+bc+ca)}{2(a+b+c)}',),\n",
    "    (r'\\sqrt{a-1}+\\sqrt{b-1}+ \\sqrt{c-1} \\leq \\sqrt{c(ab+1)}','[1,oo],[1,oo],[1,oo]','',dif2),\n",
    "    (r'(x-1)(y-1)(z-1)\\geq 8','[0,1-b-c],[0,1-c],[0,1]','[x,1/a],[y,1/b],[z,1/c]'),\n",
    "    (r'ay+bz+cx\\leq s^2','[0,s],[0,s],[0,s]','[x,s-a],[y,s-b],[z,s-c]'),\n",
    "    (r'x_1^2+x_2^2+x_3^2+x_4^2+x_5^2\\geq 2 (x_1x_2+x_2x_3+x_3x_4+x_4x_5)/\\sqrt{3}',),\n",
    "    (r' xy+yz+zx - 2xyz \\leq \\frac7{27}', '[0,1-z],[0,1]','[x,1-y-z]'),\n",
    "    (r'0 \\leq xy+yz+zx - 2xyz', '[0,1-z],[0,1]','[x,1-y-z]'),\n",
    "    (r'\\sqrt{3+a+b+c}\\geq\\sqrt a+\\sqrt b+\\sqrt c','[1-z,1],[0,1]','[a,1/x-1],[b,1/y-1],[c,1/z-1],[x,2-y-z]',\n",
    "     dif2),\n",
    "    (r'\\frac{2a^3}{a^2+b^2}+\\frac{2b^3}{b^2+c^2}+\\frac{2c^3}{c^2+a^2}\\geq a+b+c',),\n",
    "    (r'\\frac{a^2}{b+c}+\\frac{b^2}{c+a}+\\frac{c^2}{a+b}\\geq \\frac12','[0,1-c],[0,1]','[a,1-b-c]'),\n",
    "    (r'\\frac{a+b}{2b+c}+\\frac{b+c}{2c+a}+\\frac{c+a}{2a+b}\\geq 2',),\n",
    "    #(r'\\frac x{5-y^2}+\\frac y{5-z^2}+\\frac z{5-x^2}\\geq \\frac34','[0,sqrt(5)],[0,sqrt(5)]','[x,1/(y*z)]')\n",
    "]\n",
    "\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [],
   "source": [
    "def parser(formula,intervals='[]',subs='[]',func=dif):\n",
    "    newproof()\n",
    "    shiro.display=lambda x:None\n",
    "    if intervals=='':\n",
    "        intervals='[]'\n",
    "    if subs=='':\n",
    "        subs='[]'\n",
    "    formula=addbraces(formula)\n",
    "    formula=Sm(str(parse_latex(formula)))\n",
    "    formula,_=fractioncancel(formula)\n",
    "    formula=formula.subs(shiroindev._smakeiterable2(subs))\n",
    "    formula=makesubs(formula,intervals)\n",
    "    b,s=formula.lhs,formula.rhs\n",
    "    if type(formula)==LessThan:\n",
    "        b,s=s,b\n",
    "    formula=func(b,s)\n",
    "    formula=simplify(formula)\n",
    "    num,den=fractioncancel(formula)\n",
    "    return num"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "100%|██████████| 35/35 [00:46<00:00,  1.32s/it]\n"
     ]
    }
   ],
   "source": [
    "from tqdm import tqdm\n",
    "ineqs2=[]\n",
    "for ineq in tqdm(ineqs):\n",
    "    ineqs2+=[parser(*ineq)]"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Now let's look at the formulas when converted to polynomials."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "0\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( a^{2} - ab - ac + b^{2} - bc + c^{2}, a, b, c, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly(a**2 - a*b - a*c + b**2 - b*c + c**2, a, b, c, domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "1\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( a^{2} - ab - ac - ad + b^{2} + c^{2} + d^{2}, a, b, c, d, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly(a**2 - a*b - a*c - a*d + b**2 + c**2 + d**2, a, b, c, d, domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "2\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( a^{4}b^{2} + a^{3}b^{2} - a^{3}b - 2 a^{2}b + a^{2} + ab^{2} - ab + b^{2}, a, b, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly(a**4*b**2 + a**3*b**2 - a**3*b - 2*a**2*b + a**2 + a*b**2 - a*b + b**2, a, b, domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "3\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( 2 a^{3}b + a^{3} - 4 a^{2}b^{2} - a^{2}b + a^{2} + 2 ab^{3} - ab^{2} - 2 ab + b^{3} + b^{2}, a, b, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly(2*a**3*b + a**3 - 4*a**2*b**2 - a**2*b + a**2 + 2*a*b**3 - a*b**2 - 2*a*b + b**3 + b**2, a, b, domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "4\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( a^{3} - a^{2}b - ab^{2} + b^{3}, a, b, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly(a**3 - a**2*b - a*b**2 + b**3, a, b, domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "5\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( 2 a^{3} - a^{2}b - a^{2}c - ab^{2} - ac^{2} + 2 b^{3} - b^{2}c - bc^{2} + 2 c^{3}, a, b, c, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly(2*a**3 - a**2*b - a**2*c - a*b**2 - a*c**2 + 2*b**3 - b**2*c - b*c**2 + 2*c**3, a, b, c, domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "6\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( 2 a^{3} - 3 a^{2}b + b^{3}, a, b, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly(2*a**3 - 3*a**2*b + b**3, a, b, domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "7\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( a^{3} - a^{2}b - ac^{2} + b^{3} - b^{2}c + c^{3}, a, b, c, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly(a**3 - a**2*b - a*c**2 + b**3 - b**2*c + c**3, a, b, c, domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "8\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( a^{3}c + a^{3}d + a^{2}b^{2} - a^{2}bd - 2 a^{2}c^{2} - a^{2}cd + a^{2}d^{2} + ab^{3} - ab^{2}c - ab^{2}d - abc^{2} + ac^{3} - acd^{2} + b^{3}d + b^{2}c^{2} - 2 b^{2}d^{2} + bc^{3} - bc^{2}d - bcd^{2} + bd^{3} + c^{2}d^{2} + cd^{3}, a, b, c, d, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly(a**3*c + a**3*d + a**2*b**2 - a**2*b*d - 2*a**2*c**2 - a**2*c*d + a**2*d**2 + a*b**3 - a*b**2*c - a*b**2*d - a*b*c**2 + a*c**3 - a*c*d**2 + b**3*d + b**2*c**2 - 2*b**2*d**2 + b*c**3 - b*c**2*d - b*c*d**2 + b*d**3 + c**2*d**2 + c*d**3, a, b, c, d, domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "9\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( 2 a^{5}b^{2} + 2 a^{5}bc + 2 a^{5}c^{2} + a^{4}b^{3} - a^{4}b^{2}c - a^{4}bc^{2} + a^{4}c^{3} + a^{3}b^{4} - 2 a^{3}b^{3}c - 4 a^{3}b^{2}c^{2} - 2 a^{3}bc^{3} + a^{3}c^{4} + 2 a^{2}b^{5} - a^{2}b^{4}c - 4 a^{2}b^{3}c^{2} - 4 a^{2}b^{2}c^{3} - a^{2}bc^{4} + 2 a^{2}c^{5} + 2 ab^{5}c - ab^{4}c^{2} - 2 ab^{3}c^{3} - ab^{2}c^{4} + 2 abc^{5} + 2 b^{5}c^{2} + b^{4}c^{3} + b^{3}c^{4} + 2 b^{2}c^{5}, a, b, c, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly(2*a**5*b**2 + 2*a**5*b*c + 2*a**5*c**2 + a**4*b**3 - a**4*b**2*c - a**4*b*c**2 + a**4*c**3 + a**3*b**4 - 2*a**3*b**3*c - 4*a**3*b**2*c**2 - 2*a**3*b*c**3 + a**3*c**4 + 2*a**2*b**5 - a**2*b**4*c - 4*a**2*b**3*c**2 - 4*a**2*b**2*c**3 - a**2*b*c**4 + 2*a**2*c**5 + 2*a*b**5*c - a*b**4*c**2 - 2*a*b**3*c**3 - a*b**2*c**4 + 2*a*b*c**5 + 2*b**5*c**2 + b**4*c**3 + b**3*c**4 + 2*b**2*c**5, a, b, c, domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "10\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( ad + af - 2 \\sqrt{a}\\sqrt{b}\\sqrt{c}\\sqrt{d} - 2 \\sqrt{a}\\sqrt{b}\\sqrt{e}\\sqrt{f} + bc + be + cf - 2 \\sqrt{c}\\sqrt{d}\\sqrt{e}\\sqrt{f} + de, \\sqrt{a}, \\sqrt{b}, \\sqrt{c}, \\sqrt{d}, \\sqrt{e}, \\sqrt{f}, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly((sqrt(a))**2*(sqrt(d))**2 + (sqrt(a))**2*(sqrt(f))**2 - 2*(sqrt(a))*(sqrt(b))*(sqrt(c))*(sqrt(d)) - 2*(sqrt(a))*(sqrt(b))*(sqrt(e))*(sqrt(f)) + (sqrt(b))**2*(sqrt(c))**2 + (sqrt(b))**2*(sqrt(e))**2 + (sqrt(c))**2*(sqrt(f))**2 - 2*(sqrt(c))*(sqrt(d))*(sqrt(e))*(sqrt(f)) + (sqrt(d))**2*(sqrt(e))**2, sqrt(a), sqrt(b), sqrt(c), sqrt(d), sqrt(e), sqrt(f), domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "11\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( 3 a^{4}b + 3 a^{4}c - 2 a^{3}b^{2} + 2 a^{3}c^{2} + 2 a^{2}b^{3} - 6 a^{2}b^{2}c - 6 a^{2}bc^{2} - 2 a^{2}c^{3} + 3 ab^{4} - 6 ab^{2}c^{2} + 3 ac^{4} + 3 b^{4}c - 2 b^{3}c^{2} + 2 b^{2}c^{3} + 3 bc^{4}, a, b, c, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly(3*a**4*b + 3*a**4*c - 2*a**3*b**2 + 2*a**3*c**2 + 2*a**2*b**3 - 6*a**2*b**2*c - 6*a**2*b*c**2 - 2*a**2*c**3 + 3*a*b**4 - 6*a*b**2*c**2 + 3*a*c**4 + 3*b**4*c - 2*b**3*c**2 + 2*b**2*c**3 + 3*b*c**4, a, b, c, domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "12\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( 4 x^{8}y^{4} + 4 x^{7}y^{4} - 3 x^{5}y^{5} - 3 x^{5}y^{4} + 4 x^{4}y^{8} + 4 x^{4}y^{7} - 3 x^{4}y^{5} - 6 x^{4}y^{4} - 3 x^{4}y^{3} - 3 x^{3}y^{4} - 3 x^{3}y^{3} + 4 xy + 4, x, y, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly(4*x**8*y**4 + 4*x**7*y**4 - 3*x**5*y**5 - 3*x**5*y**4 + 4*x**4*y**8 + 4*x**4*y**7 - 3*x**4*y**5 - 6*x**4*y**4 - 3*x**4*y**3 - 3*x**3*y**4 - 3*x**3*y**3 + 4*x*y + 4, x, y, domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "13\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( a^{3}c^{2} + a^{2}b^{3} - a^{2}b^{2}c - a^{2}bc^{2} - ab^{2}c^{2} + b^{2}c^{3}, a, b, c, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly(a**3*c**2 + a**2*b**3 - a**2*b**2*c - a**2*b*c**2 - a*b**2*c**2 + b**2*c**3, a, b, c, domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "14\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( a^{4}c + a^{3}c^{2} + a^{2}b^{3} + ab^{4} + b^{2}c^{3} + bc^{4}, a, b, c, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly(a**4*c + a**3*c**2 + a**2*b**3 + a*b**4 + b**2*c**3 + b*c**4, a, b, c, domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "15\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( a^{4}c - 4 a^{3}bc + a^{3}c^{2} + a^{2}b^{3} + 6 a^{2}b^{2}c - 2 a^{2}bc^{2} + ab^{4} - 4 ab^{3}c - 2 ab^{2}c^{2} + b^{2}c^{3} + bc^{4}, a, b, c, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly(a**4*c - 4*a**3*b*c + a**3*c**2 + a**2*b**3 + 6*a**2*b**2*c - 2*a**2*b*c**2 + a*b**4 - 4*a*b**3*c - 2*a*b**2*c**2 + b**2*c**3 + b*c**4, a, b, c, domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "16\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( a^{6}b^{3} + a^{6}c^{3} - 2 a^{5}b^{2}c^{2} + a^{3}b^{6} + a^{3}c^{6} - 2 a^{2}b^{5}c^{2} - 2 a^{2}b^{2}c^{5} + b^{6}c^{3} + b^{3}c^{6}, a, b, c, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly(a**6*b**3 + a**6*c**3 - 2*a**5*b**2*c**2 + a**3*b**6 + a**3*c**6 - 2*a**2*b**5*c**2 - 2*a**2*b**2*c**5 + b**6*c**3 + b**3*c**6, a, b, c, domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "17\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( 2 a^{8}b^{8} + 2 a^{7}b^{6} + 2 a^{6}b^{7} - 3 a^{6}b^{5} - 3 a^{5}b^{6} + 2 a^{5}b^{5} - 3 a^{5}b^{3} + 2 a^{5}b^{2} - 6 a^{4}b^{4} + 2 a^{4}b^{3} + 2 a^{4} - 3 a^{3}b^{5} + 2 a^{3}b^{4} - 3 a^{3}b^{2} + 2 a^{3}b + 2 a^{2}b^{5} - 3 a^{2}b^{3} + 2 ab^{3} + 2 b^{4}, a, b, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly(2*a**8*b**8 + 2*a**7*b**6 + 2*a**6*b**7 - 3*a**6*b**5 - 3*a**5*b**6 + 2*a**5*b**5 - 3*a**5*b**3 + 2*a**5*b**2 - 6*a**4*b**4 + 2*a**4*b**3 + 2*a**4 - 3*a**3*b**5 + 2*a**3*b**4 - 3*a**3*b**2 + 2*a**3*b + 2*a**2*b**5 - 3*a**2*b**3 + 2*a*b**3 + 2*b**4, a, b, domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "18\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( a^{8} - a^{6}bc - 2 a^{5}b^{3} + a^{5}b^{2}c + a^{5}bc^{2} - 2 a^{5}c^{3} + 3 a^{4}b^{4} - a^{4}b^{3}c + 2 a^{4}b^{2}c^{2} - a^{4}bc^{3} + 3 a^{4}c^{4} - 2 a^{3}b^{5} - a^{3}b^{4}c - a^{3}b^{3}c^{2} - a^{3}b^{2}c^{3} - a^{3}bc^{4} - 2 a^{3}c^{5} + a^{2}b^{5}c + 2 a^{2}b^{4}c^{2} - a^{2}b^{3}c^{3} + 2 a^{2}b^{2}c^{4} + a^{2}bc^{5} - ab^{6}c + ab^{5}c^{2} - ab^{4}c^{3} - ab^{3}c^{4} + ab^{2}c^{5} - abc^{6} + b^{8} - 2 b^{5}c^{3} + 3 b^{4}c^{4} - 2 b^{3}c^{5} + c^{8}, a, b, c, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly(a**8 - a**6*b*c - 2*a**5*b**3 + a**5*b**2*c + a**5*b*c**2 - 2*a**5*c**3 + 3*a**4*b**4 - a**4*b**3*c + 2*a**4*b**2*c**2 - a**4*b*c**3 + 3*a**4*c**4 - 2*a**3*b**5 - a**3*b**4*c - a**3*b**3*c**2 - a**3*b**2*c**3 - a**3*b*c**4 - 2*a**3*c**5 + a**2*b**5*c + 2*a**2*b**4*c**2 - a**2*b**3*c**3 + 2*a**2*b**2*c**4 + a**2*b*c**5 - a*b**6*c + a*b**5*c**2 - a*b**4*c**3 - a*b**3*c**4 + a*b**2*c**5 - a*b*c**6 + b**8 - 2*b**5*c**3 + 3*b**4*c**4 - 2*b**3*c**5 + c**8, a, b, c, domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "19\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( y^{18}z^{9} + 2 y^{16}z^{14} - y^{15}z^{9} + 2 y^{14}z^{16} - y^{14}z^{13} - y^{13}z^{14} - y^{13}z^{11} - y^{12}z^{12} + y^{12}z^{9} - y^{11}z^{13} - y^{11}z^{7} + 2 y^{11}z^{4} - y^{10}z^{5} + y^{9}z^{18} - y^{9}z^{15} + y^{9}z^{12} - y^{9}z^{6} - y^{8}z^{4} - y^{7}z^{11} - y^{7}z^{5} + 2 y^{7}z^{2} - y^{6}z^{9} + y^{6}z^{6} - y^{5}z^{10} - y^{5}z^{7} + 2 y^{4}z^{11} - y^{4}z^{8} - y^{3}z^{3} + 2 y^{2}z^{7} + 1, y, z, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly(y**18*z**9 + 2*y**16*z**14 - y**15*z**9 + 2*y**14*z**16 - y**14*z**13 - y**13*z**14 - y**13*z**11 - y**12*z**12 + y**12*z**9 - y**11*z**13 - y**11*z**7 + 2*y**11*z**4 - y**10*z**5 + y**9*z**18 - y**9*z**15 + y**9*z**12 - y**9*z**6 - y**8*z**4 - y**7*z**11 - y**7*z**5 + 2*y**7*z**2 - y**6*z**9 + y**6*z**6 - y**5*z**10 - y**5*z**7 + 2*y**4*z**11 - y**4*z**8 - y**3*z**3 + 2*y**2*z**7 + 1, y, z, domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "20\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( a^{3} - a^{2}b - a^{2}c - ab^{2} + 3 abc - ac^{2} + b^{3} - b^{2}c - bc^{2} + c^{3}, a, b, c, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly(a**3 - a**2*b - a**2*c - a*b**2 + 3*a*b*c - a*c**2 + b**3 - b**2*c - b*c**2 + c**3, a, b, c, domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "21\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( 2 y^{4}z^{2} - y^{3}z^{3} - 5 y^{3}z + 2 y^{2}z^{4} - 9 y^{2}z^{2} + 5 y^{2} - 5 yz^{3} + 23 yz + 5 z^{2} - 9, y, z, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly(2*y**4*z**2 - y**3*z**3 - 5*y**3*z + 2*y**2*z**4 - 9*y**2*z**2 + 5*y**2 - 5*y*z**3 + 23*y*z + 5*z**2 - 9, y, z, domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "22\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( 2 a^{\\frac{5}{2}}b\\frac{1}{\\sqrt{a b + a + b + 1}} + 2 a^{\\frac{5}{2}}\\frac{1}{\\sqrt{a b + a + b + 1}} + 2 a^{2}b^{\\frac{7}{2}}\\frac{1}{\\sqrt{b + 1}} + 2 a^{2}b^{\\frac{5}{2}}\\frac{1}{\\sqrt{b + 1}} + 2 a^{2}b^{2}\\frac{1}{a b \\sqrt{a b + a + b + 1} + a \\sqrt{a b + a + b + 1} + b \\sqrt{a b + a + b + 1} + \\sqrt{a b + a + b + 1}} - a^{2}b^{2}\\sqrt{3} + 2 a^{2}b\\frac{1}{a b \\sqrt{a b + a + b + 1} + a \\sqrt{a b + a + b + 1} + b \\sqrt{a b + a + b + 1} + \\sqrt{a b + a + b + 1}} - a^{2}b\\sqrt{3} + 2 a^{\\frac{3}{2}}b\\frac{1}{\\sqrt{a b + a + b + 1}} + 4 ab^{\\frac{7}{2}}\\frac{1}{\\sqrt{b + 1}} + 4 ab^{\\frac{5}{2}}\\frac{1}{\\sqrt{b + 1}} + 4 ab^{2}\\frac{1}{a b \\sqrt{a b + a + b + 1} + a \\sqrt{a b + a + b + 1} + b \\sqrt{a b + a + b + 1} + \\sqrt{a b + a + b + 1}} - 2 ab^{2}\\sqrt{3} + 2 ab^{\\frac{3}{2}}\\frac{1}{\\sqrt{b + 1}} + 6 ab\\frac{1}{a b \\sqrt{a b + a + b + 1} + a \\sqrt{a b + a + b + 1} + b \\sqrt{a b + a + b + 1} + \\sqrt{a b + a + b + 1}} - 2 ab\\sqrt{3} + 2 a\\frac{1}{a b \\sqrt{a b + a + b + 1} + a \\sqrt{a b + a + b + 1} + b \\sqrt{a b + a + b + 1} + \\sqrt{a b + a + b + 1}} - a\\sqrt{3} + 2 b^{\\frac{7}{2}}\\frac{1}{\\sqrt{b + 1}} + 2 b^{\\frac{5}{2}}\\frac{1}{\\sqrt{b + 1}} + 2 b^{2}\\frac{1}{a b \\sqrt{a b + a + b + 1} + a \\sqrt{a b + a + b + 1} + b \\sqrt{a b + a + b + 1} + \\sqrt{a b + a + b + 1}} - b^{2}\\sqrt{3} + 4 b\\frac{1}{a b \\sqrt{a b + a + b + 1} + a \\sqrt{a b + a + b + 1} + b \\sqrt{a b + a + b + 1} + \\sqrt{a b + a + b + 1}} - b\\sqrt{3} + 2 \\frac{1}{a b \\sqrt{a b + a + b + 1} + a \\sqrt{a b + a + b + 1} + b \\sqrt{a b + a + b + 1} + \\sqrt{a b + a + b + 1}}, \\sqrt{a}, \\sqrt{b}, \\frac{1}{a b \\sqrt{a b + a + b + 1} + a \\sqrt{a b + a + b + 1} + b \\sqrt{a b + a + b + 1} + \\sqrt{a b + a + b + 1}}, \\frac{1}{\\sqrt{a b + a + b + 1}}, \\frac{1}{\\sqrt{b + 1}}, \\sqrt{3}, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly(2*(sqrt(a))**5*(sqrt(b))**2*(1/sqrt(a*b + a + b + 1)) + 2*(sqrt(a))**5*(1/sqrt(a*b + a + b + 1)) + 2*(sqrt(a))**4*(sqrt(b))**7*(1/sqrt(b + 1)) + 2*(sqrt(a))**4*(sqrt(b))**5*(1/sqrt(b + 1)) + 2*(sqrt(a))**4*(sqrt(b))**4*(1/(a*b*sqrt(a*b + a + b + 1) + a*sqrt(a*b + a + b + 1) + b*sqrt(a*b + a + b + 1) + sqrt(a*b + a + b + 1))) - (sqrt(a))**4*(sqrt(b))**4*(sqrt(3)) + 2*(sqrt(a))**4*(sqrt(b))**2*(1/(a*b*sqrt(a*b + a + b + 1) + a*sqrt(a*b + a + b + 1) + b*sqrt(a*b + a + b + 1) + sqrt(a*b + a + b + 1))) - (sqrt(a))**4*(sqrt(b))**2*(sqrt(3)) + 2*(sqrt(a))**3*(sqrt(b))**2*(1/sqrt(a*b + a + b + 1)) + 4*(sqrt(a))**2*(sqrt(b))**7*(1/sqrt(b + 1)) + 4*(sqrt(a))**2*(sqrt(b))**5*(1/sqrt(b + 1)) + 4*(sqrt(a))**2*(sqrt(b))**4*(1/(a*b*sqrt(a*b + a + b + 1) + a*sqrt(a*b + a + b + 1) + b*sqrt(a*b + a + b + 1) + sqrt(a*b + a + b + 1))) - 2*(sqrt(a))**2*(sqrt(b))**4*(sqrt(3)) + 2*(sqrt(a))**2*(sqrt(b))**3*(1/sqrt(b + 1)) + 6*(sqrt(a))**2*(sqrt(b))**2*(1/(a*b*sqrt(a*b + a + b + 1) + a*sqrt(a*b + a + b + 1) + b*sqrt(a*b + a + b + 1) + sqrt(a*b + a + b + 1))) - 2*(sqrt(a))**2*(sqrt(b))**2*(sqrt(3)) + 2*(sqrt(a))**2*(1/(a*b*sqrt(a*b + a + b + 1) + a*sqrt(a*b + a + b + 1) + b*sqrt(a*b + a + b + 1) + sqrt(a*b + a + b + 1))) - (sqrt(a))**2*(sqrt(3)) + 2*(sqrt(b))**7*(1/sqrt(b + 1)) + 2*(sqrt(b))**5*(1/sqrt(b + 1)) + 2*(sqrt(b))**4*(1/(a*b*sqrt(a*b + a + b + 1) + a*sqrt(a*b + a + b + 1) + b*sqrt(a*b + a + b + 1) + sqrt(a*b + a + b + 1))) - (sqrt(b))**4*(sqrt(3)) + 4*(sqrt(b))**2*(1/(a*b*sqrt(a*b + a + b + 1) + a*sqrt(a*b + a + b + 1) + b*sqrt(a*b + a + b + 1) + sqrt(a*b + a + b + 1))) - (sqrt(b))**2*(sqrt(3)) + 2*(1/(a*b*sqrt(a*b + a + b + 1) + a*sqrt(a*b + a + b + 1) + b*sqrt(a*b + a + b + 1) + sqrt(a*b + a + b + 1))), sqrt(a), sqrt(b), 1/(a*b*sqrt(a*b + a + b + 1) + a*sqrt(a*b + a + b + 1) + b*sqrt(a*b + a + b + 1) + sqrt(a*b + a + b + 1)), 1/sqrt(a*b + a + b + 1), 1/sqrt(b + 1), sqrt(3), domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "23\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( a^{4} - 4 abcd + b^{4} + c^{4} + d^{4}, a, b, c, d, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly(a**4 - 4*a*b*c*d + b**4 + c**4 + d**4, a, b, c, d, domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "24\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( a^{3}b^{2} + a^{3}c^{2} + a^{2}b^{3} - 2 a^{2}b^{2}c - 2 a^{2}bc^{2} + a^{2}c^{3} - 2 ab^{2}c^{2} + b^{3}c^{2} + b^{2}c^{3}, a, b, c, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly(a**3*b**2 + a**3*c**2 + a**2*b**3 - 2*a**2*b**2*c - 2*a**2*b*c**2 + a**2*c**3 - 2*a*b**2*c**2 + b**3*c**2 + b**2*c**3, a, b, c, domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "25\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( def + de + df - 2 \\sqrt{d}\\sqrt{e} - 2 \\sqrt{d}\\sqrt{f} + ef - 2 \\sqrt{e}\\sqrt{f} + f + 2, \\sqrt{d}, \\sqrt{e}, \\sqrt{f}, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly((sqrt(d))**2*(sqrt(e))**2*(sqrt(f))**2 + (sqrt(d))**2*(sqrt(e))**2 + (sqrt(d))**2*(sqrt(f))**2 - 2*(sqrt(d))*(sqrt(e)) - 2*(sqrt(d))*(sqrt(f)) + (sqrt(e))**2*(sqrt(f))**2 - 2*(sqrt(e))*(sqrt(f)) + (sqrt(f))**2 + 2, sqrt(d), sqrt(e), sqrt(f), domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "26\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( de^{2}f^{2} + de^{2}f + 2 def^{2} - 6 def + de + df^{2} + df + e^{2}f^{2} + e^{2}f + 2 ef^{2} + 3 ef + e + f^{2} + 2 f + 1, d, e, f, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly(d*e**2*f**2 + d*e**2*f + 2*d*e*f**2 - 6*d*e*f + d*e + d*f**2 + d*f + e**2*f**2 + e**2*f + 2*e*f**2 + 3*e*f + e + f**2 + 2*f + 1, d, e, f, domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "27\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( s^{2}def + s^{2}, s, d, e, f, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly(s**2*d*e*f + s**2, s, d, e, f, domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "28\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( -2 \\sqrt{3}x_{1}x_{2} - 2 \\sqrt{3}x_{2}x_{3} - 2 \\sqrt{3}x_{3}x_{4} - 2 \\sqrt{3}x_{4}x_{5} + 3 x_{1}^{2} + 3 x_{2}^{2} + 3 x_{3}^{2} + 3 x_{4}^{2} + 3 x_{5}^{2}, \\sqrt{3}, x_{1}, x_{2}, x_{3}, x_{4}, x_{5}, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly(-2*(sqrt(3))*x_1*x_2 - 2*(sqrt(3))*x_2*x_3 - 2*(sqrt(3))*x_3*x_4 - 2*(sqrt(3))*x_4*x_5 + 3*x_1**2 + 3*x_2**2 + 3*x_3**2 + 3*x_4**2 + 3*x_5**2, sqrt(3), x_1, x_2, x_3, x_4, x_5, domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "29\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( 7 a^{2}b^{3} - 6 a^{2}b^{2} - 6 a^{2}b + 7 a^{2} + 14 ab^{3} - 12 ab^{2} + 15 ab - 13 a + 7 b^{3} - 6 b^{2} - 6 b + 7, a, b, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly(7*a**2*b**3 - 6*a**2*b**2 - 6*a**2*b + 7*a**2 + 14*a*b**3 - 12*a*b**2 + 15*a*b - 13*a + 7*b**3 - 6*b**2 - 6*b + 7, a, b, domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "30\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( a^{2}b^{2} + a^{2}b + 2 ab^{2} + ab + a + b^{2} + b, a, b, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly(a**2*b**2 + a**2*b + 2*a*b**2 + a*b + a + b**2 + b, a, b, domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "31\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( -2 \\frac{1}{\\sqrt{b}}\\sqrt{\\frac{a^{2} b^{2}}{a^{2} b + a^{2} + a b^{2} + 3 a b + 2 a + b^{2} + 2 b + 1} + \\frac{a^{2} b}{a^{2} b + a^{2} + a b^{2} + 3 a b + 2 a + b^{2} + 2 b + 1} + \\frac{a b^{2}}{a^{2} b + a^{2} + a b^{2} + 3 a b + 2 a + b^{2} + 2 b + 1} + \\frac{a b}{a^{2} b + a^{2} + a b^{2} + 3 a b + 2 a + b^{2} + 2 b + 1}} - 2 \\frac{1}{\\sqrt{b}}\\sqrt{\\frac{a b}{a^{2} b + a^{2} + a b + 2 a + 1} + \\frac{b}{a^{2} b + a^{2} + a b + 2 a + 1}} - 2 \\sqrt{\\frac{a^{2} b^{2}}{a^{2} b + a^{2} + a b^{2} + 3 a b + 2 a + b^{2} + 2 b + 1} + \\frac{a^{2} b}{a^{2} b + a^{2} + a b^{2} + 3 a b + 2 a + b^{2} + 2 b + 1} + \\frac{a b^{2}}{a^{2} b + a^{2} + a b^{2} + 3 a b + 2 a + b^{2} + 2 b + 1} + \\frac{a b}{a^{2} b + a^{2} + a b^{2} + 3 a b + 2 a + b^{2} + 2 b + 1}}\\sqrt{\\frac{a b}{a^{2} b + a^{2} + a b + 2 a + 1} + \\frac{b}{a^{2} b + a^{2} + a b + 2 a + 1}} + 3, \\frac{1}{\\sqrt{b}}, \\sqrt{\\frac{a^{2} b^{2}}{a^{2} b + a^{2} + a b^{2} + 3 a b + 2 a + b^{2} + 2 b + 1} + \\frac{a^{2} b}{a^{2} b + a^{2} + a b^{2} + 3 a b + 2 a + b^{2} + 2 b + 1} + \\frac{a b^{2}}{a^{2} b + a^{2} + a b^{2} + 3 a b + 2 a + b^{2} + 2 b + 1} + \\frac{a b}{a^{2} b + a^{2} + a b^{2} + 3 a b + 2 a + b^{2} + 2 b + 1}}, \\sqrt{\\frac{a b}{a^{2} b + a^{2} + a b + 2 a + 1} + \\frac{b}{a^{2} b + a^{2} + a b + 2 a + 1}}, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly(-2*(1/sqrt(b))*(sqrt(a**2*b**2/(a**2*b + a**2 + a*b**2 + 3*a*b + 2*a + b**2 + 2*b + 1) + a**2*b/(a**2*b + a**2 + a*b**2 + 3*a*b + 2*a + b**2 + 2*b + 1) + a*b**2/(a**2*b + a**2 + a*b**2 + 3*a*b + 2*a + b**2 + 2*b + 1) + a*b/(a**2*b + a**2 + a*b**2 + 3*a*b + 2*a + b**2 + 2*b + 1))) - 2*(1/sqrt(b))*(sqrt(a*b/(a**2*b + a**2 + a*b + 2*a + 1) + b/(a**2*b + a**2 + a*b + 2*a + 1))) - 2*(sqrt(a**2*b**2/(a**2*b + a**2 + a*b**2 + 3*a*b + 2*a + b**2 + 2*b + 1) + a**2*b/(a**2*b + a**2 + a*b**2 + 3*a*b + 2*a + b**2 + 2*b + 1) + a*b**2/(a**2*b + a**2 + a*b**2 + 3*a*b + 2*a + b**2 + 2*b + 1) + a*b/(a**2*b + a**2 + a*b**2 + 3*a*b + 2*a + b**2 + 2*b + 1)))*(sqrt(a*b/(a**2*b + a**2 + a*b + 2*a + 1) + b/(a**2*b + a**2 + a*b + 2*a + 1))) + 3, 1/sqrt(b), sqrt(a**2*b**2/(a**2*b + a**2 + a*b**2 + 3*a*b + 2*a + b**2 + 2*b + 1) + a**2*b/(a**2*b + a**2 + a*b**2 + 3*a*b + 2*a + b**2 + 2*b + 1) + a*b**2/(a**2*b + a**2 + a*b**2 + 3*a*b + 2*a + b**2 + 2*b + 1) + a*b/(a**2*b + a**2 + a*b**2 + 3*a*b + 2*a + b**2 + 2*b + 1)), sqrt(a*b/(a**2*b + a**2 + a*b + 2*a + 1) + b/(a**2*b + a**2 + a*b + 2*a + 1)), domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "32\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( a^{5}b^{2} + a^{5}c^{2} + a^{4}b^{3} - a^{4}b^{2}c - a^{4}bc^{2} - a^{4}c^{3} - a^{3}b^{4} + a^{3}c^{4} + a^{2}b^{5} - a^{2}b^{4}c - a^{2}bc^{4} + a^{2}c^{5} - ab^{4}c^{2} - ab^{2}c^{4} + b^{5}c^{2} + b^{4}c^{3} - b^{3}c^{4} + b^{2}c^{5}, a, b, c, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly(a**5*b**2 + a**5*c**2 + a**4*b**3 - a**4*b**2*c - a**4*b*c**2 - a**4*c**3 - a**3*b**4 + a**3*c**4 + a**2*b**5 - a**2*b**4*c - a**2*b*c**4 + a**2*c**5 - a*b**4*c**2 - a*b**2*c**4 + b**5*c**2 + b**4*c**3 - b**3*c**4 + b**2*c**5, a, b, c, domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "33\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( 2 a^{2}d^{3} - a^{2}d^{2} - a^{2}d + 2 a^{2} + 4 ad^{3} - 2 ad^{2} - 3 a + 2 d^{3} - d^{2} - d + 2, a, d, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly(2*a**2*d**3 - a**2*d**2 - a**2*d + 2*a**2 + 4*a*d**3 - 2*a*d**2 - 3*a + 2*d**3 - d**2 - d + 2, a, d, domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "34\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\operatorname{Poly}{\\left( 2 a^{3} - 3 a^{2}b + a^{2}c + ab^{2} - 3 ac^{2} + 2 b^{3} - 3 b^{2}c + bc^{2} + 2 c^{3}, a, b, c, domain=\\mathbb{Z} \\right)}$"
      ],
      "text/plain": [
       "Poly(2*a**3 - 3*a**2*b + a**2*c + a*b**2 - 3*a*c**2 + 2*b**3 - 3*b**2*c + b*c**2 + 2*c**3, a, b, c, domain='ZZ')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "for i,ineq in zip(range(len(ineqs2)),ineqs2):\n",
    "    print(i)\n",
    "    display(reducegens(assumeall(ineq,positive=True)))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Most formulas was converted to polynomials of independent variables. However formulas No. 22 and No. 31 were not. For this reason it's very unlikely that any method of proving these ones will succeed.\n",
    "\n",
    "Now let's try some methods of proving these inequalities. The first one would be the simple `prove`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [],
   "source": [
    "tm=[0]*4"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "0,2,2,0,0,0,0,0,2,0,0,0,0,0,0,2,0,0,2,0,2,2,2,0,0,2,2,0,2,2,0,2,0,2,0,\n",
      "20.714609994000057\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "Counter({0: 21, 2: 14})"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "from collections import Counter\n",
    "from timeit import default_timer as timer\n",
    "start=timer()\n",
    "t=[]\n",
    "for ineq in ineqs2:\n",
    "    t+=[prove(ineq)]\n",
    "    print(t[-1],end=',')\n",
    "tm[0]=timer()-start\n",
    "print('\\n',tm[0],sep='')\n",
    "Counter(t)\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Code 0 means that the proof was found, all other codes means that proof wasn't found. So this method has proved 21 inequalities.\n",
    "\n",
    "The second method uses `findvalues` function, rationalizes the result numbers and gives them as additional parameter to `prove` function."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "0,0,0,0,0,0,0,0,2,0,0,0,0,0,0,2,0,0,2,0,2,2,2,0,0,2,0,0,2,2,0,2,0,2,0,\n",
      "21.832711064998875\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "Counter({0: 24, 2: 11})"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "def cut(a):\n",
    "    if a<=0 or a>=100 or (a is None):\n",
    "        return 1\n",
    "    return a\n",
    "start=timer()\n",
    "t2=[]\n",
    "for ineq in ineqs2:\n",
    "    numvalues=findvalues(ineq,disp=0)\n",
    "    values=nsimplify(numvalues,tolerance=0.1,rational=True)\n",
    "    values=list(map(cut,values))\n",
    "    t2+=[prove(ineq,values=values)]\n",
    "    print(t2[-1],end=',')\n",
    "tm[1]=timer()-start\n",
    "print('\\n',tm[1],sep='')\n",
    "Counter(t2)\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The third method is similar to the second one, but instead of rationalize values it squares, rationalizes and makes square roots of these values."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "0,2,0,0,0,0,0,0,2,0,0,0,0,0,0,2,0,0,2,0,2,2,2,0,0,2,0,0,2,2,0,2,0,2,0,\n",
      "21.697120987002563\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "Counter({0: 23, 2: 12})"
      ]
     },
     "execution_count": 10,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "def cut(a):\n",
    "    if a<=0 or a>=1000 or (a is None):\n",
    "        return S(1)\n",
    "    return a\n",
    "    \n",
    "start=timer()\n",
    "t3=[]\n",
    "for ineq in ineqs2:\n",
    "    numvalues=findvalues(ineq,disp=0)\n",
    "    numvalues=tuple([x**2 for x in numvalues])\n",
    "    values=nsimplify(numvalues,tolerance=0.1,rational=True)\n",
    "    values=[sqrt(x) for x in values]\n",
    "    values=list(map(cut,values))\n",
    "    t3+=[prove(ineq,values=values)]\n",
    "    print(t3[-1],end=',')\n",
    "tm[2]=timer()-start\n",
    "print('\\n',tm[2],sep='')\n",
    "Counter(t3)\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Finally, the fourth method is a slight modification to the third method. It does the same \"findvalues, square, rationalize and make square roots\" thing, but then it scales the values and runs it again. It can sometimes help with uniform formulas."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "0,2,0,0,0,0,0,0,2,0,0,0,0,0,0,2,0,0,2,0,2,2,2,0,0,2,0,0,0,2,0,2,0,2,0,\n",
      "23.187820409999404\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "Counter({0: 24, 2: 11})"
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "def betw(a):\n",
    "    return a>0.001 and a<1000 and a!=None\n",
    "def cut(a):\n",
    "    if betw(a):\n",
    "        return a\n",
    "    return S(1)\n",
    "\n",
    "start=timer()\n",
    "t4=[]\n",
    "for ineq in ineqs2:\n",
    "    numvalues=findvalues(ineq,disp=0)\n",
    "    n=1\n",
    "    numvalues2=[]\n",
    "    for i in numvalues:\n",
    "        if betw(i):\n",
    "            n=1/i\n",
    "            break\n",
    "    for i in numvalues:\n",
    "        if betw(i):\n",
    "            numvalues2+=[i*n]\n",
    "        else:\n",
    "            numvalues2+=[1]\n",
    "    numvalues3=findvalues(ineq,values=numvalues2,disp=0)\n",
    "    numvalues4=tuple([x**2 for x in numvalues3])\n",
    "    values=nsimplify(numvalues4,tolerance=0.1,rational=True)\n",
    "    values=[sqrt(x) for x in values]\n",
    "    values=list(map(cut,values))\n",
    "    t4+=[prove(ineq,values=values)]\n",
    "    print(t4[-1],end=',')\n",
    "tm[3]=timer()-start\n",
    "print('\\n',tm[3],sep='')\n",
    "Counter(t4)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAYIAAAEKCAYAAAAfGVI8AAAABHNCSVQICAgIfAhkiAAAAAlwSFlzAAALEgAACxIB0t1+/AAAADl0RVh0U29mdHdhcmUAbWF0cGxvdGxpYiB2ZXJzaW9uIDIuMi40LCBodHRwOi8vbWF0cGxvdGxpYi5vcmcv7US4rQAAD8RJREFUeJzt3X2sJXV9x/H3R8CqiAHChW7B7dVWqbRBSDaIpSY+EnwCwecUNUjdpkrFaB+wGsWaptb6lJqm7aIIrUolFRQrrcV1Cda26qIIi0AwiBbZslCru0qKAt/+cWbrFXfvmX2YM3v2934lJ+fM78zD905y7+fOzG9+k6pCktSuB41dgCRpXAaBJDXOIJCkxhkEktQ4g0CSGmcQSFLjDAJJapxBIEmNMwgkqXH7jl1AH4ccckgtLi6OXYYkzZWrr776rqpamDbfXATB4uIi69evH7sMSZorSb7VZz5PDUlS4wwCSWqcQSBJjTMIJKlxBoEkNc4gkKTGGQSS1DiDQJIaZxBIUuPm4s5iSW1aPOfTY5cwulvf8ezBt+ERgSQ1ziCQpMYZBJLUOINAkhpnEEhS4wwCSWqcQSBJjTMIJKlxBoEkNc4gkKTGGQSS1DjHGtKyWh/rZRbjvEhjMwikARmkBuk88NSQJDXOIJCkxhkEktQ4g0CSGmcQSFLjDAJJapxBIEmNMwgkqXF7/Q1l3tDjDT2SlucRgSQ1ziCQpMYNFgRJHplkXZIbklyf5Oyu/eAkVyS5uXs/aKgaJEnTDXlEcC/whqp6HHA88JokRwHnAGur6jHA2m5akjSSwYKgqjZW1Ve6z1uAG4DDgVOAC7vZLgSeN1QNkqTpZnKNIMkicCzwReCwqtoIk7AADt3OMquTrE+y/s4775xFmZLUpMGDIMnDgY8Dr6uqzX2Xq6o1VbWqqlYtLCwMV6AkNW7QIEiyH5MQ+EhVXdI135FkRff9CmDTkDVIkpY3ZK+hAB8Ebqiq9yz56jLgFd3nVwCfHKoGSdJ0Q95ZfALwMuC6JNd0bX8EvAO4OMmZwLeBFw5YgyRpisGCoKr+Fch2vn7aUNuVJO0Y7yyWpMYZBJLUOINAkhpnEEhS4wwCSWqcQSBJjTMIJKlxBoEkNc4gkKTGGQSS1DiDQJIaZxBIUuMMAklqnEEgSY0zCCSpcQaBJDXOIJCkxhkEktQ4g0CSGmcQSFLjDAJJapxBIEmNMwgkqXEGgSQ1ziCQpMYZBJLUOINAkhpnEEhS4wwCSWrcvst9meQveqxjc1W9eTfVI0masWWDADgFeMuUec4BDAJJmlPTguC9VXXhcjMkOWg31iNJmrFlrxFU1fumraDPPJKkPVevi8VJ3pnkEUn2S7I2yV1JTh+6OEnS8Pr2GjqxqjYDzwFuAx4L/P5gVUmSZqZvEOzXvT8LuKiqvjttgSTnJ9mUZMOStnOTfCfJNd3rWTtRsyRpN+obBJ9KciOwClibZAH43ynLXACctI3291bVMd3r8v6lSpKG0CsIquoc4InAqqr6MXA3k66lyy1zFTD1yEGSNK5pN5Sdto22pZOX7MQ2z0rycmA98Iaq+p+dWIckaTeZdh/Bc7v3Q4FfBz7XTT8FuJIdD4K/At4OVPf+buCV25oxyWpgNcDKlSt3cDOSpL6m3UdwRlWdweQP91FV9fyqej7wqzuzsaq6o6ruq6r7gfOA45aZd01VraqqVQsLCzuzOUlSD30vFi9W1cYl03cw6UK6Q5KsWDJ5KrBhe/NKkmZj2qmhra5M8hngIiZHBy8B1i23QJKLgCcDhyS5DXgr8OQkx3TruBX47Z0rW5K0u/QKgqo6q7tw/KSuaU1VXTplmZduo/mDO1ifJGlgfY8IqKpL2LleQpKkPVjfsYZOS3Jzku8n2ZxkS5LNQxcnSRpe3yOCdwLPraobhixGkjR7fXsN3WEISNLeqe8RwfokHwM+AdyztbG7biBJmmN9g+ARTMYXOnFJW+HFY0mae327j54xdCGSpHH07TV0RJJLu+cL3JHk40mOGLo4SdLw+l4s/hBwGfALwOHAp7o2SdKc6xsEC1X1oaq6t3tdADgSnCTtBfoGwV1JTk+yT/c6HfjvIQuTJM1G3yB4JfAi4L+AjcAL2M5zBCRJ86Vvr6FvAycPXIskaQR9ew1dmOTAJdMHJTl/uLIkSbPS99TQ0VX1va0T3XOGjx2mJEnSLPUNggclOWjrRJKD2YEhrCVJe66+f8zfDfxbkn9gMrTEi4A/GawqSdLM9L1Y/LdJ1gNPBQKcVlVfH7QySdJM9D01BHAw8MOqej9wZ5JHDVSTJGmG+vYaeivwh8Abu6b9gA8PVZQkaXb6HhGcyuQ+gh8CVNXtwAFDFSVJmp2+QfCjqiomF4pJsv9wJUmSZqlvEFyc5G+AA5O8CvgscN5wZUmSZqVvr6F3JXkGsBk4EnhLVV0xaGWSpJnoFQTdqaDPVdUVSY4EjkyyX1X9eNjyJElD63tq6Crg55IczuS00BnABUMVJUmanb5BkKq6GzgNeH9VnQocNVxZkqRZ6R0ESZ4I/Cbw6a7NsYYkaS/QNwjOZnIz2aVVdX2SRwPrhitLkjQrfXsNXcXkOsHW6VuA1w5VlCRpdpY9Ikhy7rQV9JlHkrTnmnZE8FtJNi/zfYCXAOfutookSTM1LQjOY/qYQt5hLElzbNkgqKq3zaoQSdI4duR5BJKkvZBBIEmNGywIkpyfZFOSDUvaDk5yRZKbu/eDhtq+JKmfvk8oe2yStVv/qCc5Osmbpyx2AXDSA9rOAdZW1WOAtd20JGlEfY8IzmNyZ/GPAarqWibdRreruwntuw9oPgW4sPt8IfC83pVKkgbRNwgeVlVfekDbvTuxvcOqaiNA937o9mZMsjrJ+iTr77zzzp3YlCSpj75BcFeSX+Inj6p8AbBxsKqAqlpTVauqatXCwsKQm5KkpvUdQfQ1wBrgV5J8B/gmcPpObO+OJCuqamOSFcCmnViHJGk36jvo3C3A07snlT2oqrbs5PYuA14BvKN7/+ROrkeStJv0fVTlgcDLgUVg3yQAVNV2RyBNchHwZOCQJLcBb2USABcnORP4NvDCXahdkrQb9D01dDnwH8B1wP19Fqiql27nq6f13KYkaQb6BsFDqur1g1YiSRpF315Df5fkVUlWdHcHH5zk4EErkyTNRN8jgh8Bfw68ia4Laff+6CGKkiTNTt8geD3wy1V115DFSJJmr++poeuBu4csRJI0jr5HBPcB1yRZB9yztXG57qOSpPnQNwg+0b0kSXuZvncWXzh9LknSPFo2CJJcXFUvSnIdP+kt9P+q6ujBKpMkzcS0I4Kzu/fnDF2IJGkcy/Ya2vrsAODVVfWtpS/g1cOXJ0kaWt/uo8/YRtszd2chkqRxTLtG8DtM/vN/dJJrl3x1APCFIQuTJM3GtGsEHwX+CfhTfvpB81uq6oHPI5YkzaFlg6Cqvg98H9jekNKSpDnX9xqBJGkvZRBIUuMMAklqnEEgSY0zCCSpcQaBJDXOIJCkxhkEktQ4g0CSGmcQSFLjDAJJapxBIEmNMwgkqXEGgSQ1ziCQpMYZBJLUOINAkhpnEEhS4wwCSWqcQSBJjVv24fVDSXIrsAW4D7i3qlaNUYckaaQg6Dylqu4acfuSJDw1JEnNGysICviXJFcnWT1SDZIkxjs1dEJV3Z7kUOCKJDdW1VVLZ+gCYjXAypUrx6hRkpowyhFBVd3evW8CLgWO28Y8a6pqVVWtWlhYmHWJktSMmQdBkv2THLD1M3AisGHWdUiSJsY4NXQYcGmSrdv/aFX98wh1SJIYIQiq6hbg8bPeriRp2+w+KkmNMwgkqXEGgSQ1ziCQpMYZBJLUOINAkhpnEEhS4wwCSWqcQSBJjTMIJKlxBoEkNc4gkKTGGQSS1DiDQJIaZxBIUuMMAklqnEEgSY0zCCSpcQaBJDXOIJCkxhkEktQ4g0CSGmcQSFLjDAJJapxBIEmNMwgkqXEGgSQ1ziCQpMYZBJLUOINAkhpnEEhS4wwCSWqcQSBJjTMIJKlxBoEkNc4gkKTGjRIESU5KclOSbyQ5Z4waJEkTMw+CJPsAfwk8EzgKeGmSo2ZdhyRpYowjguOAb1TVLVX1I+DvgVNGqEOSxDhBcDjwn0umb+vaJEkj2HeEbWYbbfUzMyWrgdXd5A+S3DRoVcM5BLhrrI3nz8ba8m7j/ts17r9dM+r+g13eh7/YZ6YxguA24JFLpo8Abn/gTFW1Blgzq6KGkmR9Va0au4555f7bNe6/XdPK/hvj1NCXgcckeVSSBwMvAS4boQ5JEiMcEVTVvUnOAj4D7AOcX1XXz7oOSdLEGKeGqKrLgcvH2PYI5v701sjcf7vG/bdrmth/qfqZ67SSpIY4xIQkNc4gGEiS85NsSrJh7FrmUZJHJlmX5IYk1yc5e+ya5kmShyT5UpKvdfvvbWPXNI+S7JPkq0n+cexahmQQDOcC4KSxi5hj9wJvqKrHAccDr3Eokh1yD/DUqno8cAxwUpLjR65pHp0N3DB2EUMzCAZSVVcB3x27jnlVVRur6ivd5y1Mfhm9A72nmvhBN7lf9/KC4A5IcgTwbOADY9cyNINAe7wki8CxwBfHrWS+dKc1rgE2AVdUlftvx7wP+APg/rELGZpBoD1akocDHwdeV1Wbx65nnlTVfVV1DJO7949L8mtj1zQvkjwH2FRVV49dyywYBNpjJdmPSQh8pKouGbueeVVV3wOuxGtWO+IE4OQktzIZIfmpST48bknDMQi0R0oS4IPADVX1nrHrmTdJFpIc2H1+KPB04MZxq5ofVfXGqjqiqhaZDIPzuao6feSyBmMQDCTJRcC/A0cmuS3JmWPXNGdOAF7G5D+xa7rXs8Yuao6sANYluZbJ+F5XVNVe3QVSO887iyWpcR4RSFLjDAJJapxBIEmNMwgkqXEGgSQ1ziCQdlCSY5Z2ZU1ybpLf24X17dLy0q4yCKQddwzgPQ3aaxgEalKSxSQ3JvlAkg1JPpLk6Um+kOTmJMcl2b97rsSXuzHpT0nyYOCPgRd3N7m9uFvlUUmuTHJLktcu2c7ru/VvSPK6Je1vSnJTks8CR872p5d+mjeUqUndiKbfYDKq6fVM7r79GnAmcDJwBvB14OtV9eFuuIYvdfO/EFhVVWd16zoXOBF4CnAAcBPw88DRTJ5LcTwQJqOnns7kH7ALgCcweW74V4C/rqp3DfkzS9szysPrpT3EN6vqOoAk1wNrq6qSXAcsMhm18+Ql5+8fAqzczro+XVX3APck2QQcBvwGcGlV/bDbxiXAk5gEwaVVdXfXftkgP53Uk0Gglt2z5PP9S6bvZ/K7cR/w/Kq6aelCSZ4wZV33dctnmW17KK49htcIpO37DPC73UioJDm2a9/C5BTQNFcBz0vysCT7A6cCn+/aT03y0CQHAM/d/aVL/RkE0va9nckjHq9NsqGbBljH5OLw0ovFP6N71OYFTK4tfBH4QFV9tWv/GHANk+ctfH64H0GazovFktQ4jwgkqXEGgSQ1ziCQpMYZBJLUOINAkhpnEEhS4wwCSWqcQSBJjfs/ZA6/DVKt+QAAAAAASUVORK5CYII=\n",
      "text/plain": [
       "<Figure size 432x288 with 1 Axes>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "import matplotlib.pyplot as plt\n",
    "plt.bar(['1','2','3','4'],tm)\n",
    "plt.ylabel('time [seconds]')\n",
    "plt.xlabel('method')\n",
    "plt.show()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [],
   "source": [
    "import pandas as pd\n",
    "u=pd.DataFrame(zip(['']*len(ineqs),t,t2,t3,t4))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAYIAAAEKCAYAAAAfGVI8AAAABHNCSVQICAgIfAhkiAAAAAlwSFlzAAALEgAACxIB0t1+/AAAADl0RVh0U29mdHdhcmUAbWF0cGxvdGxpYiB2ZXJzaW9uIDIuMi40LCBodHRwOi8vbWF0cGxvdGxpYi5vcmcv7US4rQAAFQBJREFUeJzt3X/wXXV95/HnS34sGmEhEjAFY6DDsFLHBPsdSkXdCtLiqgR3ddGpNKOZTVuowuC2G11brXZ3cX8otrO7bQou8bcUoURFLU2hVOuACb8hsLGIkCWSKCogO7iB9/5xT8rXmO/9nm/yPffmm/N8zNw595x7frzvnSSvnPM5n/NJVSFJ6q9njbsASdJ4GQSS1HMGgST1nEEgST1nEEhSzxkEktRzBoEk9ZxBIEk9ZxBIUs/tP+4C2jj88MNr8eLF4y5DkuaUDRs2fK+qFky33pwIgsWLF7N+/fpxlyFJc0qS77RZz0tDktRznQVBkuOT3Drp9WiSC5LMT3Jtkk3N9LCuapAkTa+zIKiqe6tqaVUtBX4ReAK4ClgFrKuq44B1zbwkaUxGdWnoNOAfquo7wDJgTbN8DXDWiGqQJO3CqILgzcBnmvdHVtUWgGZ6xK42SLIyyfok67dt2zaiMiWpfzoPgiQHAmcCfzGT7apqdVVNVNXEggXT3v0kSdpNozgjeA1wc1U93Mw/nGQhQDPdOoIaJElTGEUQvIVnLgsBrAWWN++XA1ePoAZJ0hQ6DYIkzwFOB66ctPgi4PQkm5rPLuqyBknScJ32LK6qJ4Dn7bTs+wzuItIcsHjVl8Zdwljdf9Frx11Cr/nnbzR//uxZLEk9ZxBIUs8ZBJLUcwaBJPWcQSBJPWcQSFLPGQSS1HNzYoQyaa7yPnj7YcwFnhFIUs8ZBJLUcwaBJPWcQSBJPWcQSFLPGQSS1HMGgST1nEEgST1nEEhSzxkEktRzBoEk9ZxBIEk9ZxBIUs91GgRJDk1yRZJ7kmxM8stJ5ie5NsmmZnpYlzVIkobr+ozgo8BXquqfAUuAjcAqYF1VHQesa+YlSWPSWRAkOQR4JXApQFX9pKp+CCwD1jSrrQHO6qoGSdL0ujwjOBbYBvyvJLckuSTJPODIqtoC0EyP6LAGSdI0uhyhbH/gpcA7qurGJB9lBpeBkqwEVgIsWrRot4twhChHiJI0XJdnBJuBzVV1YzN/BYNgeDjJQoBmunVXG1fV6qqaqKqJBQsWdFimJPVbZ0FQVd8FHkxyfLPoNOBuYC2wvFm2HLi6qxokSdPrevD6dwCfSnIgcB/wNgbhc3mSFcADwJs6rkGSNESnQVBVtwITu/jotC6PK0lqz57FktRzBoEk9ZxBIEk9ZxBIUs8ZBJLUcwaBJPWcQSBJPWcQSFLPGQSS1HMGgST1nEEgST035bOGkvxxi+0frar3zmI9kqQRG/bQuWXAH0yz/SrAIJCkOWxYEHykqtYM+Zwkh81yPZKkEZuyjaCqLp5u4zbrSJL2bq0bi5O8PsmNSW5Ncm6XRUmSRmfKIEiyZKdF5wAnMxh3+Le7LEqSNDrD2gjOTRLgD3aMPwz8B+Bp4KFRFCdJ6t6UQVBVv9mcFfxZkvXA7wMvA54DfHBE9UmSOja0jaCqbquqZcCtwFpgYVWtraonR1KdJKlzw9oIfivJLUluBuYBZwCHJflqkleMrEJJUqeGnRGcW1UnMmgg/t2q2l5Vfwy8GXhDm50nuT/JHc2dRuubZfOTXJtkUzO1L4IkjdGwIPg/ST4I/Efgnh0Lq+oHVXXhDI7xqqpaWlUTzfwqYF1VHQesa+YlSWMyLAiWATcBfw38xiwecxmwo8fyGuCsWdy3JGmGhgXB/Kr6QlV9paqe2tUKSZ4/zf4L+KskG5KsbJYdWVVbAJrpETOuWpI0a4b1I7iGQeexYaZb55SqeijJEcC1Se4Zsu5PaYJjJcCiRYvabiZJmqFhQbAkyaNDPg8w7HOq6qFmujXJVcBJwMNJFlbVliQLga1TbLsaWA0wMTFRw44jSdp9wx46t19VHTLkdXBVHTXV9knmJTl4x3vgV4E7GfRHWN6sthy4eva+jiRppoadEeypI4GrBk+pYH/g01X1lSTfBC5PsgJ4AHhThzVIkqbRWRBU1X3Azg+uo6q+D5zW1XElSTPjmMWS1HOtzgiS7MfgUs8/rl9VD3RVlCRpdKYNgiTvAN4HPMzgEdQw6B/wkg7rkiSNSJszgvOB45tr+5KkfUybNoIHgR91XYgkaTzanBHcB1yf5EvAP45DUFUf7qwqSdLItAmCB5rXgc1LkrQPmTYIquoPYdA7uKp+3H1JkqRRmraNIMkvJ7kb2NjML0nyPzqvTJI0Em0aiy8Gfg34PgzGMQZe2WVRkqTRadWzuKoe3GnRLscnkCTNPW0aix9M8jKgkhwIvJPmMpEkae5rc0bwW8B5wFHAZmBpMy9J2ge0OSNIVf1655VIksaizRnB3yf5qyQrkhzaeUWSpJGaNgiq6jjgvcAvADcn+WKSt3ZemSRpJNreNXRTVV3IYMzhR4A1nVYlSRqZNh3KDkmyPMmXgb8HtjAIBEnSPqBNY/FtwF8CH6iqb3RcjyRpxNoEwbFVVUkOTvLcqnq886okSSPTpo3gF5LcAtwJ3J1kQ5IXd1yXJGlE2gTBauDCqnphVS0C3tUsayXJfkluSfLFZv6YJDcm2ZTkc01vZUnSmLQJgnlVdd2Omaq6Hpg3g2Ocz08/kuJDwEea21J/AKyYwb4kSbOsTRDcl+T3kyxuXu8Fvt1m50mOBl4LXNLMBzgVuKJZZQ1w1szLliTNljZB8HZgAXBl8zoceFvL/V8M/B7wdDP/POCHVbW9md/M4BlGkqQxGXrXUJL9gPdU1TtnuuMkrwO2VtWGJL+yY/EuVq0ptl8JrARYtGjRTA8vSWpp6BlBVT0F/OJu7vsU4Mwk9wOfZXBJ6GLg0CQ7Auho4KEpjr26qiaqamLBggW7WYIkaTptLg3dkmRtknOS/Msdr+k2qqp3V9XRVbUYeDPwN81TTK8D3tisthy4eneLlyTtuTYdyuYzGKby1EnLikF7we74d8Bnk/wRcAtw6W7uR5I0C6YNgqpq2zA8bB/XA9c37+/DZxVJ0l6jzUPnjk3yhSTbkmxNcnWSY0ZRnCSpe23aCD4NXA4sBH4O+AsGjb+SpH1AmyBIVX2iqrY3r08yxS2fkqS5p01j8XVJVjE4CyjgbOBLSeYDVNUjHdYnSepYmyA4u5n+5k7L384gGI6d1YokSSPV5q4hG4YlaR/WasxiSdK+yyCQpJ4zCCSp59p0KDslybzm/VuTfDjJC7svTZI0Cm3OCP4n8ESSJQzGFvgO8PFOq5IkjUybINheVQUsAz5aVR8FDu62LEnSqLTpR/BYkncD5wCvaAarOaDbsiRJo9LmjOBs4Eng7VX1XQZDS/6XTquSJI3MtEHQ/OP/eeCfNIu+B1zVZVGSpNFpc9fQvwGuAP6sWXQU8JddFiVJGp02l4bOYzD+8KMAVbUJOKLLoiRJo9MmCJ6sqp/smGkGnvcx1JK0j2gTBH+b5D3As5OczmBgmi90W5YkaVTaBMEqYBtwB4NHUV8DvLfLoiRJo9PmMdRPA3/evCRJ+5gpgyDJ5VX1r5PcwS7aBKrqJZ1WJkkaiWFnBOc309ftzo6THATcwKD/wf7AFVX1viTHMBj2cj5wM3DO5MZoSdJoTdlGUFVbmrfnVtV3Jr+Ac1vs+0ng1KpaAiwFzkhyMvAh4CNVdRzwA2DFnn0FSdKeaNNYfPoulr1muo1q4PFm9oDmVcCpDDqoAawBzmpRgySpI1MGQZLfbtoHjk9y+6TXt4Hb2+w8yX5JbgW2AtcC/wD8sKq2N6tsZtBTeVfbrkyyPsn6bdu2zeQ7SZJmYFgbwaeBLwP/icEtpDs8VlWPtNl5VT0FLE1yKIPnE71oV6tNse1qYDXAxMSEHdgkqSPDgqCq6v4k5+38QZL5bcOg2dEPk1wPnAwcmmT/5qzgaOChmRYtSZo9w9oIPt1MNwDrm+mGSfNDJVnQnAmQ5NnAq4GNwHXAG5vVlgNX71blkqRZMeUZQVW9rpkes5v7XgisaQayeRZweVV9McndwGeT/BFwC3Dpbu5fkjQLhnUoe+mwDavq5mk+vx04cRfL7wNOalugJKlbw9oI/tuQz3bcBipJmuOGXRp61SgLkSSNR5vB60nyYuAE4KAdy6rq410VJUkanWmDIMn7gF9hEATXMOhV/DXAIJCkfUCbR0y8ETgN+G5VvQ1YwjMD2UuS5rg2QfB/mzEJtic5hMHjIo7ttixJ0qi0aSNY33QM+3MGnckeB27qtCpJ0si0GaFsxyOn/zTJV4BDmj4CkqR9QJvG4lfuallV3dBNSZKkUWpzaeh3J70/iEGv4A3YoUyS9gltLg29fvJ8khcA/7mziiRJI9XmrqGdbQZePNuFSJLGo00bwZ/wzOAxz2Iw/vBtXRYlSRqdVrePTnq/HfhMVX29o3okSSPWpo1gzSgKkSSNR5tLQ3ew63GFw2A4y5fMelWSpJFpc2noy830E83014EnAM8UJGkf0CYITqmqUybNr0ry9ar6QFdFSZJGp83to/OSvHzHTJKXAfO6K0mSNEptzghWAB9L8k8ZtBX8CHh7p1VJkkamzV1DG4AlzSOoU1U/6r4sSdKoTHtpKMmRSS4FPldVP0pyQpIVLbZ7QZLrkmxMcleS85vl85Ncm2RTMz1sFr6HJGk3tWkjuAz4KvBzzfz/Bi5osd124F1V9SLgZOC8JCcAq4B1VXUcsK6ZlySNSZsgOLyqLgeeBqiq7cBT021UVVuq6ubm/WPARuAoYBnP3Hq6BjhrN+qWJM2SNkHw4yTPo+lUluRkBg3GrSVZDJwI3AgcWVVbYBAWwBFTbLMyyfok67dt2zaTw0mSZqDNXUMXAmuBn0/ydWABgwHtW0nyXODzwAVV9WiSVttV1WpgNcDExMSuejZLkmZBm7uGbk7yz4HjGTxW4t6q+n9tdp7kAAYh8KmqurJZ/HCShVW1JclCYOtu1i5JmgVtxyM4CVgCvBR4S5LfmG6DDP7rfymwsao+POmjtcDy5v1y4Or25UqSZlubh859Avh54FaeaSQu4OPTbHoKcA5wR5Jbm2XvAS4CLm9uQX0AeNNu1C1JmiVt2ggmgBOqakbX6avqawwuJe3KaTPZlySpO20uDd0JPL/rQiRJ49HmjOBw4O4kNwFP7lhYVWd2VpUkaWTaBMH7uy5CkjQ+bW4f/dtRFCJJGo8pgyDJ16rq5Uke46eHqtwxROUhnVcnSerclEFQVS9vpgePrhxJ0qi17VAmSdpHGQSS1HMGgST1nEEgST1nEEhSzxkEktRzBoEk9ZxBIEk9ZxBIUs8ZBJLUcwaBJPWcQSBJPWcQSFLPGQSS1HMGgST1XGdBkORjSbYmuXPSsvlJrk2yqZke1tXxJUntdHlGcBlwxk7LVgHrquo4YF0zL0kao86CoKpuAB7ZafEyYE3zfg1wVlfHlyS1M+o2giOragtAMz1ixMeXJO1kr20sTrIyyfok67dt2zbuciRpnzXqIHg4yUKAZrp1qhWranVVTVTVxIIFC0ZWoCT1zaiDYC2wvHm/HLh6xMeXJO2ky9tHPwN8Azg+yeYkK4CLgNOTbAJOb+YlSWO0f1c7rqq3TPHRaV0dU5I0c3ttY7EkaTQMAknqOYNAknrOIJCknjMIJKnnDAJJ6jmDQJJ6ziCQpJ4zCCSp5wwCSeo5g0CSes4gkKSeMwgkqecMAknqOYNAknrOIJCknjMIJKnnDAJJ6jmDQJJ6ziCQpJ4zCCSp58YSBEnOSHJvkm8lWTWOGiRJAyMPgiT7Af8deA1wAvCWJCeMug5J0sA4zghOAr5VVfdV1U+AzwLLxlCHJInxBMFRwIOT5jc3yyRJY7D/GI6ZXSyrn1kpWQmsbGYfT3Jvp1V153Dge+M6eD40riPPGn+/PePvt2fm+u/3wjYrjSMINgMvmDR/NPDQzitV1Wpg9aiK6kqS9VU1Me465ip/vz3j77dn+vL7jePS0DeB45Ick+RA4M3A2jHUIUliDGcEVbU9ye8AXwX2Az5WVXeNug5J0sA4Lg1RVdcA14zj2GMw5y9vjZm/357x99szvfj9UvUz7bSSpB7xEROS1HMGQUeSfCzJ1iR3jruWuSjJC5Jcl2RjkruSnD/umuaSJAcluSnJbc3v94fjrmkuSrJfkluSfHHctXTJIOjOZcAZ4y5iDtsOvKuqXgScDJzno0hm5Eng1KpaAiwFzkhy8phrmovOBzaOu4iuGQQdqaobgEfGXcdcVVVbqurm5v1jDP4y2gO9pRp4vJk9oHnZIDgDSY4GXgtcMu5aumYQaK+XZDFwInDjeCuZW5rLGrcCW4Frq8rfb2YuBn4PeHrchXTNINBeLclzgc8DF1TVo+OuZy6pqqeqaimD3vsnJXnxuGuaK5K8DthaVRvGXcsoGATaayU5gEEIfKqqrhx3PXNVVf0QuB7brGbiFODMJPczeELyqUk+Od6SumMQaK+UJMClwMaq+vC465lrkixIcmjz/tnAq4F7xlvV3FFV766qo6tqMYPH4PxNVb11zGV1xiDoSJLPAN8Ajk+yOcmKcdc0x5wCnMPgf2K3Nq9/Me6i5pCFwHVJbmfwfK9rq2qfvgVSu8+exZLUc54RSFLPGQSS1HMGgST1nEEgST1nEEhSzxkE0gwlWTr5VtYk70/yb/dgf3u0vbSnDAJp5pYC9mnQPsMgUC8lWZzkniSXJLkzyaeSvDrJ15NsSnJSknnNuBLfbJ5JvyzJgcAHgLObTm5nN7s8Icn1Se5L8s5Jx7mw2f+dSS6YtPzfJ7k3yV8Dx4/220s/zQ5l6qXmiabfYvBU07sY9L69DVgBnAm8DbgbuLuqPtk8ruGmZv03ARNV9TvNvt4P/CrwKuBg4F7g+cBLGIxLcTIQBk9PfSuD/4BdBvwSg3HDbwb+tKr+a5ffWZrKWAavl/YS366qOwCS3AWsq6pKcgewmMFTO8+cdP3+IGDRFPv6UlU9CTyZZCtwJPBy4Kqq+nFzjCuBVzAIgquq6olm+dpOvp3UkkGgPnty0vunJ80/zeDvxlPAv6qqeydvlOSXptnXU832GXJsT8W117CNQJraV4F3NE9CJcmJzfLHGFwCms4NwFlJnpNkHvAG4O+a5W9I8uwkBwOvn/3SpfYMAmlqH2QwxOPtSe5s5gGuY9A4PLmx+Gc0Q21exqBt4Ubgkqq6pVn+OeBWBuMt/F13X0Gano3FktRznhFIUs8ZBJLUcwaBJPWcQSBJPWcQSFLPGQSS1HMGgST1nEEgST33/wEm667avpkz1QAAAABJRU5ErkJggg==\n",
      "text/plain": [
       "<Figure size 432x288 with 1 Axes>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "plt.bar(['1','2','3','4'],[sum(u[i]==0)/len(ineqs2)*100 for i in range(1,5)])\n",
    "plt.ylabel('inequalities proven [%]')\n",
    "plt.xlabel('method')\n",
    "plt.show()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Down below there are contingency tables and McNemar test for every pair of methods."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th>2</th>\n",
       "      <th>False</th>\n",
       "      <th>True</th>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <th></th>\n",
       "      <th></th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>False</th>\n",
       "      <td>11</td>\n",
       "      <td>3</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>True</th>\n",
       "      <td>0</td>\n",
       "      <td>21</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "</div>"
      ],
      "text/plain": [
       "2      False  True \n",
       "1                  \n",
       "False     11      3\n",
       "True       0     21"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th>3</th>\n",
       "      <th>False</th>\n",
       "      <th>True</th>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <th></th>\n",
       "      <th></th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>False</th>\n",
       "      <td>12</td>\n",
       "      <td>2</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>True</th>\n",
       "      <td>0</td>\n",
       "      <td>21</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "</div>"
      ],
      "text/plain": [
       "3      False  True \n",
       "1                  \n",
       "False     12      2\n",
       "True       0     21"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th>4</th>\n",
       "      <th>False</th>\n",
       "      <th>True</th>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <th></th>\n",
       "      <th></th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>False</th>\n",
       "      <td>11</td>\n",
       "      <td>3</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>True</th>\n",
       "      <td>0</td>\n",
       "      <td>21</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "</div>"
      ],
      "text/plain": [
       "4      False  True \n",
       "1                  \n",
       "False     11      3\n",
       "True       0     21"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th>3</th>\n",
       "      <th>False</th>\n",
       "      <th>True</th>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <th></th>\n",
       "      <th></th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>False</th>\n",
       "      <td>11</td>\n",
       "      <td>0</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>True</th>\n",
       "      <td>1</td>\n",
       "      <td>23</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "</div>"
      ],
      "text/plain": [
       "3      False  True \n",
       "2                  \n",
       "False     11      0\n",
       "True       1     23"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th>4</th>\n",
       "      <th>False</th>\n",
       "      <th>True</th>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <th></th>\n",
       "      <th></th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>False</th>\n",
       "      <td>10</td>\n",
       "      <td>1</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>True</th>\n",
       "      <td>1</td>\n",
       "      <td>23</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "</div>"
      ],
      "text/plain": [
       "4      False  True \n",
       "2                  \n",
       "False     10      1\n",
       "True       1     23"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th>4</th>\n",
       "      <th>False</th>\n",
       "      <th>True</th>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <th></th>\n",
       "      <th></th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>False</th>\n",
       "      <td>11</td>\n",
       "      <td>1</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>True</th>\n",
       "      <td>0</td>\n",
       "      <td>23</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "</div>"
      ],
      "text/plain": [
       "4      False  True \n",
       "3                  \n",
       "False     11      1\n",
       "True       0     23"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "for i in range(4):\n",
    "    for j in range(i+1,4):\n",
    "        display(pd.crosstab(u[i+1]==0, u[j+1]==0))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "pvalue      0.25\n",
      "statistic   0.0\n",
      "pvalue      0.5\n",
      "statistic   0.0\n",
      "pvalue      0.25\n",
      "statistic   0.0\n",
      "pvalue      1.0\n",
      "statistic   0.0\n",
      "pvalue      1.0\n",
      "statistic   1.0\n",
      "pvalue      1.0\n",
      "statistic   0.0\n"
     ]
    }
   ],
   "source": [
    "from statsmodels.stats.contingency_tables import mcnemar\n",
    "for i in range(4):\n",
    "    for j in range(i+1,4):\n",
    "        print(mcnemar(pd.crosstab(u[i+1]==0, u[j+1]==0)))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "In all cases p-value is greater than 0.05, so there is no statistical difference between the methods."
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.7.3"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}