proof (prove) goal (1 subgoal): 1. ⋀(x::real) xa xb xc xd xe xf xh xi xl xn xo xr xs xt xu xv xw xy xz ya yb yc yd ye yf yg yh yi yj yl ym yp yq yr ys yt yu yw yy yz za zb zc zd zf zg zh zi zj zk zm zn zo zp zq zr zs zt zu zw zy zz aaa aab aac aad aaf aag aah aai aak aal aam aao aaq aas aat aav aay aba abb abc abd abe abg abh abj abk abl abo abq abr abs abt abu abv abw abx aby abz aca acb acc acd acf acg ach aci acj ack acm acn aco acp acq acr acs act acu acw ada adb adc adf adg adh adi adj adk adl adn adp adq adr ads adu adv adw ady aea aeb aec aed aee. 0 ≤ yc ∧ 0 ≤ yd ∧ 0 ≤ yb ∧ 0 ≤ ya ⟹ 0 ≤ yf ∧ 0 ≤ xh ∧ 0 ≤ ye ∧ 0 ≤ yg ⟹ 0 ≤ yw ∧ 0 ≤ xs ∧ 0 ≤ yu ⟹ 0 ≤ aea ∧ 0 ≤ aee ∧ 0 ≤ aed ⟹ 0 ≤ zy ∧ 0 ≤ xz ∧ 0 ≤ zw ⟹ 0 ≤ zb ∧ 0 ≤ za ∧ 0 ≤ yy ∧ 0 ≤ yz ⟹ 0 ≤ zp ∧ 0 ≤ zo ∧ 0 ≤ yq ⟹ 0 ≤ adp ∧ 0 ≤ aeb ∧ 0 ≤ aec ⟹ 0 ≤ acm ∧ 0 ≤ aco ∧ 0 ≤ acn ⟹ 0 ≤ abl ⟹ 0 ≤ zr ∧ 0 ≤ zq ∧ 0 ≤ abh ⟹ 0 ≤ abq ∧ 0 ≤ zd ∧ 0 ≤ abo ⟹ 0 ≤ acd ∧ 0 ≤ acc ∧ 0 ≤ xi ∧ 0 ≤ acb ⟹ 0 ≤ acp ∧ 0 ≤ acr ∧ 0 ≤ acq ⟹ 0 ≤ xw ∧ 0 ≤ xr ∧ 0 ≤ xv ∧ 0 ≤ xu ⟹ 0 ≤ zc ∧ 0 ≤ acg ∧ 0 ≤ ach ⟹ 0 ≤ zt ∧ 0 ≤ zs ∧ 0 ≤ xy ⟹ 0 ≤ ady ∧ 0 ≤ adw ∧ 0 ≤ zg ⟹ 0 ≤ abd ∧ 0 ≤ abc ∧ 0 ≤ yr ∧ 0 ≤ abb ⟹ 0 ≤ adi ∧ 0 ≤ x ∧ 0 ≤ adh ∧ 0 ≤ xa ⟹ 0 ≤ aak ∧ 0 ≤ aai ∧ 0 ≤ aad ⟹ 0 ≤ aba ∧ 0 ≤ zh ∧ 0 ≤ aay ⟹ 0 ≤ abg ∧ 0 ≤ ys ∧ 0 ≤ abe ⟹ 0 ≤ abs ∧ 0 ≤ yt ∧ 0 ≤ abr ∧ 0 ≤ zu ⟹ 0 ≤ abv ∧ 0 ≤ zn ∧ 0 ≤ abw ∧ 0 ≤ zm ⟹ 0 ≤ adl ∧ 0 ≤ adn ⟹ 0 ≤ acf ∧ 0 ≤ aca ⟹ 0 ≤ ads ∧ 0 ≤ aaq ⟹ 0 ≤ ada ⟹ 0 ≤ aaf ∧ 0 ≤ aac ∧ 0 ≤ aag ⟹ 0 ≤ aal ∧ 0 ≤ acu ∧ 0 ≤ acs ∧ 0 ≤ act ⟹ 0 ≤ aas ∧ 0 ≤ xb ∧ 0 ≤ aat ⟹ 0 ≤ zk ∧ 0 ≤ zj ∧ 0 ≤ zi ⟹ 0 ≤ ack ∧ 0 ≤ acj ∧ 0 ≤ xc ∧ 0 ≤ aci ⟹ 0 ≤ aav ∧ 0 ≤ aah ∧ 0 ≤ xd ⟹ 0 ≤ abt ∧ 0 ≤ xo ∧ 0 ≤ abu ∧ 0 ≤ xn ⟹ 0 ≤ adc ∧ 0 ≤ abz ∧ 0 ≤ adc ∧ 0 ≤ abz ⟹ 0 ≤ xt ∧ 0 ≤ zz ∧ 0 ≤ aab ∧ 0 ≤ aaa ⟹ 0 ≤ adq ∧ 0 ≤ xl ∧ 0 ≤ adr ∧ 0 ≤ adb ⟹ 0 ≤ zf ∧ 0 ≤ yh ∧ 0 ≤ yi ⟹ 0 ≤ aao ∧ 0 ≤ aam ∧ 0 ≤ xe ⟹ 0 ≤ abk ∧ 0 ≤ aby ∧ 0 ≤ abj ∧ 0 ≤ abx ⟹ 0 ≤ yp ⟹ 0 ≤ yl ∧ 0 ≤ yj ∧ 0 ≤ ym ⟹ 0 ≤ acw ⟹ 0 ≤ adk ∧ 0 ≤ adg ∧ 0 ≤ adj ∧ 0 ≤ adf ⟹ 0 ≤ adv ∧ 0 ≤ xf ∧ 0 ≤ adu ⟹ yc + yd + yb + ya = 1 ⟹ yf + xh + ye + yg = 1 ⟹ yw + xs + yu = 1 ⟹ aea + aee + aed = 1 ⟹ zy + xz + zw = 1 ⟹ zb + za + yy + yz = 1 ⟹ zp + zo + yq = 1 ⟹ adp + aeb + aec = 1 ⟹ acm + aco + acn = 1 ⟹ abl + abl = 1 ⟹ zr + zq + abh = 1 ⟹ abq + zd + abo = 1 ⟹ acd + acc + xi + acb = 1 ⟹ acp + acr + acq = 1 ⟹ xw + xr + xv + xu = 1 ⟹ zc + acg + ach = 1 ⟹ zt + zs + xy = 1 ⟹ ady + adw + zg = 1 ⟹ abd + abc + yr + abb = 1 ⟹ adi + x + adh + xa = 1 ⟹ aak + aai + aad = 1 ⟹ aba + zh + aay = 1 ⟹ abg + ys + abe = 1 ⟹ abs + yt + abr + zu = 1 ⟹ abv + zn + abw + zm = 1 ⟹ adl + adn = 1 ⟹ acf + aca = 1 ⟹ ads + aaq = 1 ⟹ ada + ada = 1 ⟹ aaf + aac + aag = 1 ⟹ aal + acu + acs + act = 1 ⟹ aas + xb + aat = 1 ⟹ zk + zj + zi = 1 ⟹ ack + acj + xc + aci = 1 ⟹ aav + aah + xd = 1 ⟹ abt + xo + abu + xn = 1 ⟹ adc + abz + adc + abz = 1 ⟹ xt + zz + aab + aaa = 1 ⟹ adq + xl + adr + adb = 1 ⟹ zf + yh + yi = 1 ⟹ aao + aam + xe = 1 ⟹ abk + aby + abj + abx = 1 ⟹ yp + yp = 1 ⟹ yl + yj + ym = 1 ⟹ acw + acw + acw + acw = 1 ⟹ adk + adg + adj + adf = 1 ⟹ adv + xf + adu = 1 ⟹ yd = 0 ∨ yb = 0 ⟹ xh = 0 ∨ ye = 0 ⟹ yy = 0 ∨ za = 0 ⟹ acc = 0 ∨ xi = 0 ⟹ xv = 0 ∨ xr = 0 ⟹ yr = 0 ∨ abc = 0 ⟹ zn = 0 ∨ abw = 0 ⟹ xo = 0 ∨ abu = 0 ⟹ xl = 0 ∨ adr = 0 ⟹ (yr + abd < abl ∨ yr + (abd + abb) < 1) ∨ yr + abd = abl ∧ yr + (abd + abb) = 1 ⟹ adb + adr < xn + abu ∨ adb + adr = xn + abu ⟹ (abl < abt ∨ abl < abt + xo) ∨ abl = abt ∧ abl = abt + xo ⟹ yd + yc < abc + abd ∨ yd + yc = abc + abd ⟹ aca < abb + yr ∨ aca = abb + yr ⟹ acb + acc < xu + xv ∨ acb + acc = xu + xv ⟹ (yq < xu + xr ∨ yq + zp < xu + (xr + xw)) ∨ yq = xu + xr ∧ yq + zp = xu + (xr + xw) ⟹ (zw < xw ∨ zw < xw + xv ∨ zw + zy < xw + (xv + xu)) ∨ zw = xw ∧ zw = xw + xv ∧ zw + zy = xw + (xv + xu) ⟹ xs + yw < zs + zt ∨ xs + yw = zs + zt ⟹ aab + xt < ye + yf ∨ aab + xt = ye + yf ⟹ (ya + yb < yg + ye ∨ ya + (yb + yc) < yg + (ye + yf)) ∨ ya + yb = yg + ye ∧ ya + (yb + yc) = yg + (ye + yf) ⟹ (xu + xv < acb + acc ∨ xu + (xv + xw) < acb + (acc + acd)) ∨ xu + xv = acb + acc ∧ xu + (xv + xw) = acb + (acc + acd) ⟹ (zs < xz + zy ∨ zs + xy < xz + (zy + zw)) ∨ zs = xz + zy ∧ zs + xy = xz + (zy + zw) ⟹ (zs + zt < xz + zy ∨ zs + (zt + xy) < xz + (zy + zw)) ∨ zs + zt = xz + zy ∧ zs + (zt + xy) = xz + (zy + zw) ⟹ yg + ye < ya + yb ∨ yg + ye = ya + yb ⟹ (abd < yc ∨ abd + abc < yc + yd) ∨ abd = yc ∧ abd + abc = yc + yd ⟹ (ye + yf < adr + adq ∨ ye + (yf + yg) < adr + (adq + adb)) ∨ ye + yf = adr + adq ∧ ye + (yf + yg) = adr + (adq + adb) ⟹ yh + yi < ym + yj ∨ yh + yi = ym + yj ⟹ (abq < yl ∨ abq + abo < yl + ym) ∨ abq = yl ∧ abq + abo = yl + ym ⟹ (yp < zp ∨ yp < zp + zo ∨ 1 < zp + (zo + yq)) ∨ yp = zp ∧ yp = zp + zo ∧ 1 = zp + (zo + yq) ⟹ (abb + yr < aca ∨ abb + (yr + abd) < aca + acf) ∨ abb + yr = aca ∧ abb + (yr + abd) = aca + acf ⟹ adw + zg < abe + ys ∨ adw + zg = abe + ys ⟹ zd + abq < ys + abg ∨ zd + abq = ys + abg ⟹ yt + abs < aby + abk ∨ yt + abs = aby + abk ⟹ (yu < abx ∨ yu < abx + aby ∨ yu + yw < abx + (aby + abk)) ∨ yu = abx ∧ yu = abx + aby ∧ yu + yw = abx + (aby + abk) ⟹ aaf < adv ∨ aaf = adv ⟹ abj + abk < yy + zb ∨ abj + abk = yy + zb ⟹ (abb < yz ∨ abb + abc < yz + za ∨ abb + (abc + abd) < yz + (za + zb)) ∨ abb = yz ∧ abb + abc = yz + za ∧ abb + (abc + abd) = yz + (za + zb) ⟹ (acg + zc < zd + abq ∨ acg + (zc + ach) < zd + (abq + abo)) ∨ acg + zc = zd + abq ∧ acg + (zc + ach) = zd + (abq + abo) ⟹ zf < acm ∨ zf = acm ⟹ (zg + ady < acn + acm ∨ zg + (ady + adw) < acn + (acm + aco)) ∨ zg + ady = acn + acm ∧ zg + (ady + adw) = acn + (acm + aco) ⟹ aay + zh < zi + zj ∨ aay + zh = zi + zj ⟹ zy < zk ∨ zy = zk ⟹ (adn < zm + zn ∨ adn + adl < zm + (zn + abv)) ∨ adn = zm + zn ∧ adn + adl = zm + (zn + abv) ⟹ zo + zp < zs + zt ∨ zo + zp = zs + zt ⟹ zq + zr < zs + zt ∨ zq + zr = zs + zt ⟹ (aai < adi ∨ aai < adi + adh) ∨ aai = adi ∧ aai = adi + adh ⟹ (abr < acj ∨ abr + (abs + zu) < acj + (aci + ack)) ∨ abr = acj ∧ abr + (abs + zu) = acj + (aci + ack) ⟹ (abl < zw ∨ 1 < zw + zy) ∨ abl = zw ∧ 1 = zw + zy ⟹ (zz + aaa < act + acu ∨ zz + (aaa + aab) < act + (acu + aal)) ∨ zz + aaa = act + acu ∧ zz + (aaa + aab) = act + (acu + aal) ⟹ (aam < aac ∨ aam + aao < aac + aaf) ∨ aam = aac ∧ aam + aao = aac + aaf ⟹ (aak < aaf ∨ aak + aad < aaf + aag) ∨ aak = aaf ∧ aak + aad = aaf + aag ⟹ (aah < aai ∨ aah + aav < aai + aak) ∨ aah = aai ∧ aah + aav = aai + aak ⟹ act + (acu + aal) < aam + aao ∨ act + (acu + aal) = aam + aao ⟹ (ads < aat ∨ 1 < aat + aas) ∨ ads = aat ∧ 1 = aat + aas ⟹ (aba < aas ∨ aba + aay < aas + aat) ∨ aba = aas ∧ aba + aay = aas + aat ⟹ acm < aav ∨ acm = aav ⟹ (ada < aay ∨ 1 < aay + aba) ∨ ada = aay ∧ 1 = aay + aba ⟹ abb + (abc + abd) < abe + abg ∨ abb + (abc + abd) = abe + abg ⟹ (abh < abj ∨ abh < abj + abk) ∨ abh = abj ∧ abh = abj + abk ⟹ 1 < abo + abq ∨ 1 = abo + abq ⟹ (acj < abr ∨ acj + aci < abr + abs) ∨ acj = abr ∧ acj + aci = abr + abs ⟹ (abt < abv ∨ abt + abu < abv + abw) ∨ abt = abv ∧ abt + abu = abv + abw ⟹ (abx < adc ∨ abx + aby < adc + abz) ∨ abx = adc ∧ abx + aby = adc + abz ⟹ (acf < acd ∨ acf < acd + acc ∨ 1 < acd + (acc + acb)) ∨ acf = acd ∧ acf = acd + acc ∧ 1 = acd + (acc + acb) ⟹ acc + acd < acf ∨ acc + acd = acf ⟹ (acg < acq ∨ acg + ach < acq + acr) ∨ acg = acq ∧ acg + ach = acq + acr ⟹ aci + (acj + ack) < acr + acp ∨ aci + (acj + ack) = acr + acp ⟹ (acm < acp ∨ acm + acn < acp + acq ∨ acm + (acn + aco) < acp + (acq + acr)) ∨ acm = acp ∧ acm + acn = acp + acq ∧ acm + (acn + aco) = acp + (acq + acr) ⟹ (acs + act < acw + acw ∨ acs + (act + acu) < acw + (acw + acw)) ∨ acs + act = acw + acw ∧ acs + (act + acu) = acw + (acw + acw) ⟹ (ada < adb + adr ∨ 1 < adb + (adr + adq)) ∨ ada = adb + adr ∧ 1 = adb + (adr + adq) ⟹ (adc + adc < adf + adg ∨ adc + (adc + abz) < adf + (adg + adk)) ∨ adc + adc = adf + adg ∧ adc + (adc + abz) = adf + (adg + adk) ⟹ adh + adi < adj + adk ∨ adh + adi = adj + adk ⟹ (adl < aec ∨ 1 < aec + adp) ∨ adl = aec ∧ 1 = aec + adp ⟹ (adq < ads ∨ adq + adr < ads) ∨ adq = ads ∧ adq + adr = ads ⟹ adu + adv < aed + aea ∨ adu + adv = aed + aea ⟹ (adw < aee ∨ adw + ady < aee + aea) ∨ adw = aee ∧ adw + ady = aee + aea ⟹ (aeb < aed ∨ aeb + aec < aed + aee) ∨ aeb = aed ∧ aeb + aec = aed + aee ⟹ False