2020-05-17 23:46:53 +02:00
{
"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": [
2020-05-18 20:49:46 +02:00
"100%|██████████| 35/35 [00:46<00:00, 1.32s/it]\n"
2020-05-17 23:46:53 +02:00
]
}
],
"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",
2020-05-18 20:49:46 +02:00
"execution_count": 6,
2020-05-17 23:46:53 +02:00
"metadata": {},
2020-05-18 20:49:46 +02:00
"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"
}
],
2020-05-17 23:46:53 +02:00
"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",
2020-05-18 20:49:46 +02:00
"execution_count": 7,
2020-05-17 23:46:53 +02:00
"metadata": {},
"outputs": [],
"source": [
"tm=[0]*4"
]
},
{
"cell_type": "code",
2020-05-18 20:49:46 +02:00
"execution_count": 8,
2020-05-17 23:46:53 +02:00
"metadata": {},
2020-05-18 20:49:46 +02:00
"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"
}
],
2020-05-17 23:46:53 +02:00
"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",
2020-05-18 20:49:46 +02:00
"execution_count": 9,
2020-05-17 23:46:53 +02:00
"metadata": {},
2020-05-18 20:49:46 +02:00
"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"
}
],
2020-05-17 23:46:53 +02:00
"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",
2020-05-18 20:49:46 +02:00
"execution_count": 10,
2020-05-17 23:46:53 +02:00
"metadata": {},
2020-05-18 20:49:46 +02:00
"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"
}
],
2020-05-17 23:46:53 +02:00
"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",
2020-05-18 20:49:46 +02:00
"execution_count": 11,
2020-05-17 23:46:53 +02:00
"metadata": {},
2020-05-18 20:49:46 +02:00
"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"
}
],
2020-05-17 23:46:53 +02:00
"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",
2020-05-18 20:49:46 +02:00
"execution_count": 17,
2020-05-17 23:46:53 +02:00
"metadata": {},
2020-05-18 20:49:46 +02:00
"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+KkmNMwgkqXEGgSQ1ziCQpMYZBJLUOINAkhpnEEhS4wwCSWqcQSBJjTMIJKlxBoEkNc4gkKTGGQSS1DiDQJIaZxBIUuMMAklqnEEgSY0zCCSpcQaBJDXOIJCkxhkEktQ4g0CSGmcQSFLjDAJJapxBIEmNMwgkqXEGgSQ1ziCQpMYZBJLUOINAkhpnEEhS4wwCSWqcQSBJjTMIJKlxBoEkNc4gkKTGjRIESU5KclOSbyQ
"text/plain": [
"<Figure size 432x288 with 1 Axes>"
]
},
"metadata": {},
"output_type": "display_data"
}
],
2020-05-17 23:46:53 +02:00
"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",
2020-05-18 20:49:46 +02:00
"execution_count": 13,
2020-05-17 23:46:53 +02:00
"metadata": {},
"outputs": [],
"source": [
"import pandas as pd\n",
"u=pd.DataFrame(zip(['']*len(ineqs),t,t2,t3,t4))"
]
},
{
"cell_type": "code",
2020-05-18 20:49:46 +02:00
"execution_count": 14,
2020-05-17 23:46:53 +02:00
"metadata": {},
2020-05-18 20:49:46 +02:00
"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+mGSfNDJVnQnAmQ5NnAq4GNwHX
"text/plain": [
"<Figure size 432x288 with 1 Axes>"
]
},
"metadata": {},
"output_type": "display_data"
}
],
2020-05-17 23:46:53 +02:00
"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",
2020-05-18 20:49:46 +02:00
"execution_count": 15,
2020-05-17 23:46:53 +02:00
"metadata": {},
2020-05-18 20:49:46 +02:00
"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"
}
],
2020-05-17 23:46:53 +02:00
"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",
2020-05-18 20:49:46 +02:00
"execution_count": 16,
2020-05-17 23:46:53 +02:00
"metadata": {},
2020-05-18 20:49:46 +02:00
"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"
]
}
],
2020-05-17 23:46:53 +02:00
"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
}
