The undecidable Gödel sentence

Related reading
	Newly Published The Annotated Turing: A Guided Tour Through Alan Turing's Historic Paper on Computability and the Turing Machine Charles Petzold explains the legendary 36-page paper in the context of Turing's life
	I am a strange loop Hofstadter's latest book, in which he examines the parallels between Gödel's incompleteness theorem and the the emergence of mind My Review of I am a strange loop
	A madman dreams of Turing machines Janna Levin gives a partially fictional account of the lives of two of the most prominent mathematicians of the 20^th century, Kurt Godel and Alan Turing. My Review of A madman dreams of Turing machines
	On formally undecidable propositions of Principia mathematica and related systems This is where it all began
See Gödel's incompleteness theorem - recommended reading for more information related to this subject

¬∀z33 ∀x34 ∀y34 ∀z34 ∀x35 ∀y35 ∀z35 ∀x36 ∀y36 ∀z36 ∀x37 ∀y37 ∀z31 ∀x32 ∀y32 ∀z30 ∀x31 ∀y31 ∀z29 ∀x30 ∀y30 ∀z28 ∀x29 ∀y29 ∀z27 ∀x28 ∀y28 ∀z37 ∀x38 ∀y38 ∀z32 ∀x33 ∀y33 ∀z43 ∀x44 ∀y44 ∀z42 ∀x43 ∀y43 ∀x84 ∀y84 ∀z84 ∀z41 ∀x42 ∀y42 ∀x9 ∀y9 ∀z9 ∀x8 ∀y8 ∀z8 ∀z26 ∀x27 ∀y27 ∀z40 ∀x41 ∀y41 ∀z25 ∀x26 ∀y26 ∀z24 ∀x25 ∀y25 ∀z39 ∀x40 ∀y40 ∀z23 ∀x24 ∀y24 ∀z22 ∀x23 ∀y23 ∀z21 ∀x22 ∀y22 ∀z18 ∀x19 ∀y19 ∀z20 ∀x21 ∀y21 ∀z14 ∀x15 ∀y15 ∀z13 ∀x14 ∀y14 ∀z12 ∀x13 ∀y13 ∀z19 ∀x20 ∀y20 ∀z17 ∀x18 ∀y18 ∀z38 ∀x39 ∀y39 (∀y2 ∀x2 ∀z2 (¬(¬∀x1 ¬z2+ x1'=x6⇒(¬∀x1 ¬y2+ x1'=x6⇒∀x1 ¬x2+ x1'=x6))⇒¬∀z5 ∀y5 ∀x5 ∀z4 ∀y4 ∀x4 ∀z3 (¬∀y12 (¬∀x1 ¬y12=y2+ x1'⇒(¬∀x1 ¬y9=y2+ x1*y12⇒¬y12=( z3'*z9)'))⇒(¬∀x12 (¬∀x1 ¬x12=x+ x1'⇒(¬∀x1 ¬y8=x+ x1*x12⇒¬x12=( x'*z8)'))⇒(¬∀z11 (¬∀x1 ¬z11=z5+ x1'⇒(¬∀x1 ¬y8=z5+ x1*z11⇒¬z11=( y2'*z8)'))⇒(z5=y5'⇒(¬∀y11 (¬∀x1 ¬y11=y5+ x1'⇒(¬∀x1 ¬y8=y5+ x1*y11⇒¬y11=( z3'*z8)'))⇒(¬∀x11 (¬∀x1 ¬x11=x2+ x1'⇒(¬∀x1 ¬y7=x2+ x1*x11⇒¬x11=( x4'*z7)'))⇒(¬∀z10 (¬∀x1 ¬z10=z4+ x1'⇒(¬∀x1 ¬y7=z4+ x1*z10⇒¬z10=( y4'*z7)'))⇒(¬∀y10 (¬∀x1 ¬y10=x5+ x1'⇒(¬∀x1 ¬y7=x5+ x1*y10⇒¬y10=( y4'*z7)'))⇒(x=0⇒(( y2+ z2)*( y2+ z2)+ y2+ 0'=z4⇒(( z3+ z2')*( z3+ z2')+ z3+ 0'=y4⇒(( z3+ 0)*( z3+ 0)+ z3+ 0'=x4⇒(¬∀x10 (¬∀x1 ¬x10=z3+ x1'⇒(¬∀x1 ¬y6=z3+ x1*x10⇒¬x10=( y3'*z6)'))⇒(¬∀x1 ¬x5+ x1'=x8⇒(¬∀x1 ¬z4+ x1'=x7⇒(¬∀x1 ¬y4+ x1'=x7⇒∀x1 ¬x4+ x1'=x7)))))))))))))))))⇒(∀y297 ∀x297 (¬(y297=x297⇒∀x1 ¬y297+ x1'=z33)⇒¬∀z299 ∀y299 ∀z298 ∀y298 ∀z297 (z299=z297⇒(¬∀x300 (¬∀x1 ¬x300=z299+ x1'⇒(¬∀x1 ¬y7=z299+ x1*x300⇒¬x300=( y299'*z7)'))⇒(y299=( z298+ 0)*( z298+ 0)+ z298+ 0'⇒(¬∀x299 (¬∀x1 ¬x299=z298+ x1'⇒(¬∀x1 ¬x35=z298+ x1*x299⇒¬x299=( y298'*y35)'))⇒(y298=( x297+ 0)*( x297+ 0)+ x297+ 0'⇒∀x298 (¬∀x1 ¬x298=z297+ x1'⇒(¬∀x1 ¬x34=z297+ x1*x298⇒¬x298=( y297'*y34)'))))))))⇒(∀y281 ∀x281 ∀z280 (¬(y281=( z280+ x281)*( z280+ x281)+ z280+ 0'⇒∀x1 ¬y281+ x1'=z34)⇒¬∀y286 ∀x286 ∀x285 ∀y285 ∀x284 ∀y284 ∀y283 ∀x283 ∀z281 (¬((z280=0⇒x281=z281)⇒¬(¬z280=0⇒¬((y282=0⇒y284=z281) ⇒¬(¬y282=0⇒y286=z281))))⇒(¬∀z286 (¬∀x1 ¬z286=y286+ x1'⇒(¬∀x1 ¬x35=y286+ x1*z286⇒¬z286=( x286'*y35)'))⇒(x286=( z282+ y285)*( z282+ y285)+ z282+ 0'⇒(¬∀z285 (¬∀x1 ¬z285=y285+ x1'⇒(¬∀x1 ¬y6=y285+ x1*z285⇒¬z285=( x285'*z6)'))⇒(x285=( y282+ x281)*( y282+ x281)+ y282+ 0'⇒(¬∀z284 (¬∀x1 ¬z284=y284+ x1'⇒(¬∀x1 ¬y6=y284+ x1*z284⇒¬z284=( x284'*z6)'))⇒(x284=( 0+ 0)*( 0+ 0)+ 0+ 0'⇒(( y282+ z282)*( y282+ z282)+ y282+ 0'=y283⇒(¬∀z283 (¬∀x1 ¬z283=y283+ x1'⇒(¬∀x1 ¬x36=y283+ x1*z283⇒¬z283=( x283'*y36)'))⇒(x283=( z280+ x281)*( z280+ x281)+ z280+ 0'⇒∀x282 (¬∀x1 ¬x282=z281+ x1'⇒(¬∀x1 ¬x35=z281+ x1*x282⇒¬x282=( y281'*y35)')))))))))))))⇒(∀x244 ∀z243 ∀y243 (¬(x244=( y243+ z243)*( y243+ z243)+ y243+ 0'⇒∀x1 ¬x244+ x1'=z35)⇒¬∀z246 ∀y246 ∀z245 ∀y245 ∀y244 (¬∀x258 ∀z257 ∀z250 ∀y250 ∀x249 ∀z248 ∀z247 ∀y247 ∀x247 ((¬(¬0'=x247⇒0''=x247)⇒¬∀x280 ∀z279 ∀x279 ∀z278 ∀y277 ∀x277 ∀z275 ∀y275 ∀z274 ∀y274 ∀x273 ∀z272 ∀z271 ∀y271 ∀x271 ((¬0=x271⇒( x280+ y278)*( x280+ y278)+ x280+ 0'=y244)⇒(¬∀y280 (¬∀x1 ¬y280=x280+ x1'⇒(¬∀x1 ¬x31=x280+ x1*y280⇒¬y280=( z279'*y31)'))⇒(z279=( y276+ x278)*( y276+ x278)+ y276+ 0'⇒(( x278+ y278)*( x278+ y278)+ x278+ 0'=x279⇒(¬∀y279 (¬∀x1 ¬y279=x279+ x1'⇒(¬∀x1 ¬x37=x279+ x1*y279⇒¬y279=( z278'*y37)'))⇒(z278=( z243+ z276)*( z243+ z276)+ z243+ 0'⇒(( y276+ z276)*( y276+ z276)+ y276+ 0'=y277⇒(¬∀z277 (¬∀x1 ¬z277=y277+ x1'⇒(¬∀x1 ¬x18=y277+ x1*z277⇒¬z277=( x277'*y18)'))⇒(x277=x246⇒((0=x271⇒( z275+ x274)*( z275+ x274)+ z275+ 0'=y244)⇒(¬∀x276 (¬∀x1 ¬x276=z275+ x1'⇒(¬∀x1 ¬x32=z275+ x1*x276⇒¬x276=( y275'*y32)'))⇒(y275=( x272+ z273)*( x272+ z273)+ x272+ 0'⇒(( z273+ x274)*( z273+ x274)+ z273+ 0'=z274⇒(¬∀x275 (¬∀x1 ¬x275=z274+ x1'⇒(¬∀x1 ¬x37=z274+ x1*x275⇒¬x275=( y274'*y37)'))⇒(y274=( z243+ y272)*( z243+ y272)+ z243+ 0'⇒(( x272+ y272)*( x272+ y272)+ x272+ 0'=x273⇒(¬∀y273 (¬∀x1 ¬y273=x273+ x1'⇒(¬∀x1 ¬x37=x273+ x1*y273⇒¬y273=( z272'*y37)'))⇒(z272=( z243+ x246)*( z243+ x246)+ z243+ 0'⇒(z271=x271⇒(¬∀x1 ¬z271+ x1'=0'*0'''+ 0'⇒¬x245=y271*( 0'*0'''+ 0')+ z271)))))))))))))))))))))⇒((0''=x247⇒¬∀y270 ∀x270 ∀y269 ∀x269 ∀z267 ∀y267 ∀z266 ∀y266 ∀x265 ∀z264 ∀y263 ∀x263 ∀y262 ∀x262 ∀z260 ∀y260 ∀y259 ∀x259 ∀z258 ((¬(¬0=z258⇒0'=z258)⇒( y270+ z268)*( y270+ z268)+ y270+ 0'=y244)⇒(¬∀z270 (¬∀x1 ¬z270=y270+ x1'⇒(¬∀x1 ¬x30=y270+ x1*z270⇒¬z270=( x270'*y30)'))⇒(x270=( x257+ y268)*( x257+ y268)+ x257+ 0'⇒(( y268+ z268)*( y268+ z268)+ y268+ 0'=y269⇒(¬∀z269 (¬∀x1 ¬z269=y269+ x1'⇒(¬∀x1 ¬x24=y269+ x1*z269⇒¬z269=( x269'*y24)'))⇒(x269=y257⇒((0'=z258⇒( z267+ x266)*( z267+ x266)+ z267+ 0'=y244)⇒(¬∀x268 (¬∀x1 ¬x268=z267+ x1'⇒(¬∀x1 ¬x29=z267+ x1*x268⇒¬x268=( y267'*y29)'))⇒(y267=( ( x257+ x264)*( x257+ x264)+ x257+ 0'+ z265)*( ( x257+ x264)*( x257+ x264)+ x257+ 0'+ z265)+ ( x257+ x264)*( x257+ x264)+ x257+ 0'+ 0'⇒(( z265+ x266)*( z265+ x266)+ z265+ 0'=z266⇒(¬∀x267 (¬∀x1 ¬x267=z266+ x1'⇒(¬∀x1 ¬x24=z266+ x1*x267⇒¬x267=( y266'*y24)'))⇒(y266=y264⇒(( x264+ y264)*( x264+ y264)+ x264+ 0'=x265⇒(¬∀y265 (¬∀x1 ¬y265=x265+ x1'⇒(¬∀x1 ¬x44=x265+ x1*y265⇒¬y265=( z264'*y44)'))⇒(z264=( ( ( x257+ 0)*( x257+ 0)+ x257+ 0'+ y257)*( ( x257+ 0)*( x257+ 0)+ x257+ 0'+ y257)+ ( x257+ 0)*( x257+ 0)+ x257+ 0'+ 0'+ 0)*( ( ( x257+ 0)*( x257+ 0)+ x257+ 0'+ y257)*( ( x257+ 0)*( x257+ 0)+ x257+ 0'+ y257)+ ( x257+ 0)*( x257+ 0)+ x257+ 0'+ 0'+ 0)+ ( ( x257+ 0)*( x257+ 0)+ x257+ 0'+ y257)*( ( x257+ 0)*( x257+ 0)+ x257+ 0'+ y257)+ ( x257+ 0)*( x257+ 0)+ x257+ 0'+ 0'+ 0'⇒((0=z258⇒( y263+ z261)*( y263+ z261)+ y263+ 0'=y244)⇒(¬∀z263 (¬∀x1 ¬z263=y263+ x1'⇒(¬∀x1 ¬x28=y263+ x1*z263⇒¬z263=( x263'*y28)'))⇒(x263=( ( x257+ z259)*( x257+ z259)+ x257+ 0'+ y261)*( ( x257+ z259)*( x257+ z259)+ x257+ 0'+ y261)+ ( x257+ z259)*( x257+ z259)+ x257+ 0'+ 0'⇒(( y261+ z261)*( y261+ z261)+ y261+ 0'=y262⇒(¬∀z262 (¬∀x1 ¬z262=y262+ x1'⇒(¬∀x1 ¬x24=y262+ x1*z262⇒¬z262=( x262'*y24)'))⇒(x262=x260⇒(( z259+ x260)*( z259+ x260)+ z259+ 0'=z260⇒(¬∀x261 (¬∀x1 ¬x261=z260+ x1'⇒(¬∀x1 ¬x23=z260+ x1*x261⇒¬x261=( y260'*y23)'))⇒(y260=y257⇒(y259=z258⇒(¬∀x1 ¬y259+ x1'=0'*0'''+ 0'⇒¬x245=x259*( 0'*0'''+ 0')+ y259)))))))))))))))))))))))))))⇒(( x257+ y257)*( x257+ y257)+ x257+ 0'=x258⇒(¬∀y258 (¬∀x1 ¬y258=x258+ x1'⇒(¬∀x1 ¬x18=x258+ x1*y258⇒¬y258=( z257'*y18)'))⇒(z257=x246⇒((0'=x247⇒¬∀y256 ∀x256 ∀y255 ∀x255 ∀y254 ∀x254 ∀z252 ∀y252 ∀x252 ∀z251 ∀y251 ((¬(¬0=y251⇒0'=y251)⇒( y256+ x250)*( y256+ x250)+ y256+ 0'=y244)⇒(¬∀z256 (¬∀x1 ¬z256=y256+ x1'⇒(¬∀x1 ¬x27=y256+ x1*z256⇒¬z256=( x256'*y27)'))⇒(x256=( x248+ z249)*( x248+ z249)+ x248+ 0'⇒((0'=y251⇒( y255+ z253)*( y255+ z253)+ y255+ 0'=y244)⇒(¬∀z255 (¬∀x1 ¬z255=y255+ x1'⇒(¬∀x1 ¬x26=y255+ x1*z255⇒¬z255=( x255'*y26)'))⇒(x255=( ( x248+ z249)*( x248+ z249)+ x248+ 0'+ y253)*( ( x248+ z249)*( x248+ z249)+ x248+ 0'+ y253)+ ( x248+ z249)*( x248+ z249)+ x248+ 0'+ 0'⇒(( y253+ z253)*( y253+ z253)+ y253+ 0'=y254⇒(¬∀z254 (¬∀x1 ¬z254=y254+ x1'⇒(¬∀x1 ¬x24=y254+ x1*z254⇒¬z254=( x254'*y24)'))⇒(x254=x250⇒((0=y251⇒( z252+ x250)*( z252+ x250)+ z252+ 0'=y244)⇒(¬∀x253 (¬∀x1 ¬x253=z252+ x1'⇒(¬∀x1 ¬x25=z252+ x1*x253⇒¬x253=( y252'*y25)'))⇒(y252=( x248+ z249)*( x248+ z249)+ x248+ 0'⇒(x252=y251⇒(¬∀x1 ¬x252+ x1'=0'*0'''+ 0'⇒¬x245=z251*( 0'*0'''+ 0')+ x252)))))))))))))))⇒(( z249+ x250)*( z249+ x250)+ z249+ 0'=z250⇒(¬∀x251 (¬∀x1 ¬x251=z250+ x1'⇒(¬∀x1 ¬x24=z250+ x1*x251⇒¬x251=( y250'*y24)'))⇒(y250=y248⇒(( x248+ y248)*( x248+ y248)+ x248+ 0'=x249⇒(¬∀y249 (¬∀x1 ¬y249=x249+ x1'⇒(¬∀x1 ¬x24=x249+ x1*y249⇒¬y249=( z248'*y24)'))⇒(z248=x246⇒(z247=x247⇒(¬∀x1 ¬z247+ x1'=0'*0'''+ 0'⇒¬y243=y247*( 0'*0'''+ 0')+ z247))))))))))))))⇒(¬∀x1 ¬z246+ x1'=0'*0'''+ 0'⇒(x245=y246*( 0'*0'''+ 0')+ z246⇒(¬∀x1 ¬z245+ x1'=0'*0'''+ 0'⇒(y243=y245*( 0'*0'''+ 0')+ z245⇒∀z244 (¬∀x1 ¬z244=y244+ x1'⇒(¬∀x1 ¬x36=y244+ x1*z244⇒¬z244=( x244'*y36)'))))))))⇒(∀z229 ∀y229 ∀x229 (¬(z229=( x229+ y229)*( x229+ y229)+ x229+ 0'⇒∀x1 ¬z229+ x1'=z36)⇒¬∀x238 ∀z237 ∀z235 ∀y235 ∀x235 ∀y234 ∀x234 ∀x233 ∀z232 ∀y232 ∀x232 ∀x231 ∀z230 ∀x230 (¬((x231=0⇒¬((∀x1 ¬z233+ x1'=y231⇒( z235+ z231)*( z235+ z231)+ z235+ 0'=x230)⇒¬(¬∀x1 ¬z233+ x1'=y231⇒( 0+ 0)*( 0+ 0)+ 0+ 0'=x230)))⇒¬(¬x231=0⇒( y236+ z237)*( y236+ z237)+ y236+ 0'=x230))⇒(¬∀x1 ¬x238+ x1'=( ( 0'*0'''+ 0')*0'''+ 0)*0'''+ 0'⇒(y229=z237*( ( ( 0'*0'''+ 0')*0'''+ 0)*0'''+ 0')+ x238⇒(¬∀x236 (¬∀x1 ¬x236=z235+ x1'⇒(¬∀x1 ¬y7=z235+ x1*x236⇒¬x236=( y235'*z7)'))⇒(y235=( x229+ x235)*( x229+ x235)+ x229+ 0'⇒(x235+ y231=z233⇒(¬∀z234 (¬∀x1 ¬z234=y234+ x1'⇒(¬∀x1 ¬y8=y234+ x1*z234⇒¬z234=( x234'*z8)'))⇒(x234=x229⇒(( y231+ z231)*( y231+ z231)+ y231+ 0'=x233⇒(¬∀y233 (¬∀x1 ¬y233=x233+ x1'⇒(¬∀x1 ¬x18=x233+ x1*y233⇒¬y233=( z232'*y18)'))⇒(z232=x232⇒(¬∀x1 ¬y232+ x1'=0''⇒(y229=x232*0''+ y232⇒(¬∀x1 ¬x231+ x1'=0''⇒(y229=z230*0''+ x231⇒∀y230 (¬∀x1 ¬y230=x230+ x1'⇒(¬∀x1 ¬x37=x230+ x1*y230⇒¬y230=( z229'*y37)'))))))))))))))))))⇒(∀x239 ∀z238 ∀y238 (¬(x239=( y238+ z238)*( y238+ z238)+ y238+ 0'⇒∀x1 ¬x239+ x1'=z31)⇒¬∀y242 ∀x242 ∀z241 ∀y241 ∀y240 ∀x240 ∀y239 (¬((y240=0''⇒x243=y239)⇒¬(¬y240=0''⇒0=y239))⇒(¬((z240=y238⇒x241=x243)⇒¬(¬z240=y238⇒0=x243))⇒(( z240+ x241)*( z240+ x241)+ z240+ 0'=y242⇒(¬∀z242 (¬∀x1 ¬z242=y242+ x1'⇒(¬∀x1 ¬x24=y242+ x1*z242⇒¬z242=( x242'*y24)'))⇒(x242=y241⇒(¬∀x1 ¬z241+ x1'=0'*0'''+ 0'⇒(z238=y241*( 0'*0'''+ 0')+ z241⇒(¬∀x1 ¬y240+ x1'=0'*0'''+ 0'⇒(z238=x240*( 0'*0'''+ 0')+ y240⇒∀z239 (¬∀x1 ¬z239=y239+ x1'⇒(¬∀x1 ¬x32=y239+ x1*z239⇒¬z239=( x239'*y32)'))))))))))))⇒(∀x191 ∀z190 ∀y190 (¬(x191=( y190+ z190)*( y190+ z190)+ y190+ 0'⇒∀x1 ¬x191+ x1'=z30)⇒¬∀y192 ∀x192 ∀y191 (y192=y191⇒(¬∀z192 (¬∀x1 ¬z192=y192+ x1'⇒(¬∀x1 ¬x38=y192+ x1*z192⇒¬z192=( x192'*y38)'))⇒(x192=( y190+ z190)*( y190+ z190)+ y190+ 0'⇒∀z191 (¬∀x1 ¬z191=y191+ x1'⇒(¬∀x1 ¬x31=y191+ x1*z191⇒¬z191=( x191'*y31)'))))))⇒(∀y180 ∀x180 ∀z179 (¬(y180=( z179+ x180)*( z179+ x180)+ z179+ 0'⇒∀x1 ¬y180+ x1'=z29)⇒¬∀z189 ∀y189 ∀z188 ∀y188 ∀z187 ∀y187 ∀z186 ∀y186 ∀z185 ∀y185 ∀z184 ∀y184 ∀z183 ∀y183 ∀z182 ∀y182 ∀z181 ∀y181 ∀z180 (z189=z180⇒(¬∀x190 (¬∀x1 ¬x190=z189+ x1'⇒(¬∀x1 ¬x40=z189+ x1*x190⇒¬x190=( y189'*y40)'))⇒(y189=( z181+ z188)*( z181+ z188)+ z181+ 0'⇒(¬∀x189 (¬∀x1 ¬x189=z188+ x1'⇒(¬∀x1 ¬x40=z188+ x1*x189⇒¬x189=( y188'*y40)'))⇒(y188=( z186+ z187)*( z186+ z187)+ z186+ 0'⇒(¬∀x188 (¬∀x1 ¬x188=z187+ x1'⇒(¬∀x1 ¬x38=z187+ x1*x188⇒¬x188=( y187'*y38)'))⇒(y187=( z179+ x180)*( z179+ x180)+ z179+ 0'⇒(¬∀x187 (¬∀x1 ¬x187=z186+ x1'⇒(¬∀x1 ¬x38=z186+ x1*x187⇒¬x187=( y186'*y38)'))⇒(y186=( z179+ z185)*( z179+ z185)+ z179+ 0'⇒(¬∀x186 (¬∀x1 ¬x186=z185+ x1'⇒(¬∀x1 ¬x40=z185+ x1*x186⇒¬x186=( y185'*y40)'))⇒(y185=( x180+ z184)*( x180+ z184)+ x180+ 0'⇒(¬∀x185 (¬∀x1 ¬x185=z184+ x1'⇒(¬∀x1 ¬x33=z184+ x1*x185⇒¬x185=( y184'*y33)'))⇒(y184=( ( x180+ z179)*( x180+ z179)+ x180+ 0'+ z183)*( ( x180+ z179)*( x180+ z179)+ x180+ 0'+ z183)+ ( x180+ z179)*( x180+ z179)+ x180+ 0'+ 0'⇒(¬∀x184 (¬∀x1 ¬x184=z183+ x1'⇒(¬∀x1 ¬x20=z183+ x1*x184⇒¬x184=( y183'*y20)'))⇒(y183=( 0'*0'''+ 0'+ z182)*( 0'*0'''+ 0'+ z182)+ 0'*0'''+ 0'+ 0'⇒(¬∀x183 (¬∀x1 ¬x183=z182+ x1'⇒(¬∀x1 ¬x19=z182+ x1*x183⇒¬x183=( y182'*y19)'))⇒(y182=z179⇒(¬∀x182 (¬∀x1 ¬x182=z181+ x1'⇒(¬∀x1 ¬x33=z181+ x1*x182⇒¬x182=( y181'*y33)'))⇒(y181=( ( x180+ z179)*( x180+ z179)+ x180+ 0'+ ( 0'*0'''+ 0')*0'''+ 0)*( ( x180+ z179)*( x180+ z179)+ x180+ 0'+ ( 0'*0'''+ 0')*0'''+ 0)+ ( x180+ z179)*( x180+ z179)+ x180+ 0'+ 0'⇒∀x181 (¬∀x1 ¬x181=z180+ x1'⇒(¬∀x1 ¬x30=z180+ x1*x181⇒¬x181=( y180'*y30)'))))))))))))))))))))))⇒(∀z173 ∀y173 ∀x173 ∀z172 (¬(z173=( ( z172+ x173)*( z172+ x173)+ z172+ 0'+ y173)*( ( z172+ x173)*( z172+ x173)+ z172+ 0'+ y173)+ ( z172+ x173)*( z172+ x173)+ z172+ 0'+ 0'⇒∀x1 ¬z173+ x1'=z28)⇒¬∀x179 ∀z178 ∀x178 ∀z177 ∀x177 ∀z176 ∀x176 ∀z175 ∀x175 ∀z174 ∀x174 (x179=x174⇒(¬∀y179 (¬∀x1 ¬y179=x179+ x1'⇒(¬∀x1 ¬x40=x179+ x1*y179⇒¬y179=( z178'*y40)'))⇒(z178=( x176+ x178)*( x176+ x178)+ x176+ 0'⇒(¬∀y178 (¬∀x1 ¬y178=x178+ x1'⇒(¬∀x1 ¬x40=x178+ x1*y178⇒¬y178=( z177'*y40)'))⇒(z177=( x173+ x177)*( x173+ x177)+ x173+ 0'⇒(¬∀y177 (¬∀x1 ¬y177=x177+ x1'⇒(¬∀x1 ¬x38=x177+ x1*y177⇒¬y177=( z176'*y38)'))⇒(z176=( z172+ y173)*( z172+ y173)+ z172+ 0'⇒(¬∀y176 (¬∀x1 ¬y176=x176+ x1'⇒(¬∀x1 ¬x38=x176+ x1*y176⇒¬y176=( z175'*y38)'))⇒(z175=( z172+ x175)*( z172+ x175)+ z172+ 0'⇒(¬∀y175 (¬∀x1 ¬y175=x175+ x1'⇒(¬∀x1 ¬x40=x175+ x1*y175⇒¬y175=( z174'*y40)'))⇒(z174=( x173+ y173)*( x173+ y173)+ x173+ 0'⇒∀y174 (¬∀x1 ¬y174=x174+ x1'⇒(¬∀x1 ¬x29=x174+ x1*y174⇒¬y174=( z173'*y29)'))))))))))))))⇒(∀z168 ∀y168 ∀x168 ∀z167 (¬(z168=( ( z167+ x168)*( z167+ x168)+ z167+ 0'+ y168)*( ( z167+ x168)*( z167+ x168)+ z167+ 0'+ y168)+ ( z167+ x168)*( z167+ x168)+ z167+ 0'+ 0'⇒∀x1 ¬z168+ x1'=z27)⇒¬∀x172 ∀z171 ∀x171 ∀z170 ∀x170 ∀z169 ∀x169 (x172=x169⇒(¬∀y172 (¬∀x1 ¬y172=x172+ x1'⇒(¬∀x1 ¬x40=x172+ x1*y172⇒¬y172=( z171'*y40)'))⇒(z171=( x170+ x171)*( x170+ x171)+ x170+ 0'⇒(¬∀y171 (¬∀x1 ¬y171=x171+ x1'⇒(¬∀x1 ¬x33=x171+ x1*y171⇒¬y171=( z170'*y33)'))⇒(z170=( ( y168+ z167)*( y168+ z167)+ y168+ 0'+ x168)*( ( y168+ z167)*( y168+ z167)+ y168+ 0'+ x168)+ ( y168+ z167)*( y168+ z167)+ y168+ 0'+ 0'⇒(¬∀y170 (¬∀x1 ¬y170=x170+ x1'⇒(¬∀x1 ¬x38=x170+ x1*y170⇒¬y170=( z169'*y38)'))⇒(z169=( z167+ y168)*( z167+ y168)+ z167+ 0'⇒∀y169 (¬∀x1 ¬y169=x169+ x1'⇒(¬∀x1 ¬x28=x169+ x1*y169⇒¬y169=( z168'*y28)'))))))))))⇒(∀z140 ∀y140 ∀x140 (¬(z140=( x140+ y140)*( x140+ y140)+ x140+ 0'⇒∀x1 ¬z140+ x1'=z37)⇒¬∀x143 ∀z142 ∀x142 ∀z141 ∀x141 (x143=x141⇒(¬∀y143 (¬∀x1 ¬y143=x143+ x1'⇒(¬∀x1 ¬x21=x143+ x1*y143⇒¬y143=( z142'*y21)'))⇒(z142=( ( 0'*0'''+ 0'+ x142)*( 0'*0'''+ 0'+ x142)+ 0'*0'''+ 0'+ 0'+ y140)*( ( 0'*0'''+ 0'+ x142)*( 0'*0'''+ 0'+ x142)+ 0'*0'''+ 0'+ 0'+ y140)+ ( 0'*0'''+ 0'+ x142)*( 0'*0'''+ 0'+ x142)+ 0'*0'''+ 0'+ 0'+ 0'⇒(¬∀y142 (¬∀x1 ¬y142=x142+ x1'⇒(¬∀x1 ¬x19=x142+ x1*y142⇒¬y142=( z141'*y19)'))⇒(z141=x140⇒∀y141 (¬∀x1 ¬y141=x141+ x1'⇒(¬∀x1 ¬x38=x141+ x1*y141⇒¬y141=( z140'*y38)'))))))))⇒(∀z144 ∀y144 ∀x144 ∀z143 (¬(z144=( ( z143+ x144)*( z143+ x144)+ z143+ 0'+ y144)*( ( z143+ x144)*( z143+ x144)+ z143+ 0'+ y144)+ ( z143+ x144)*( z143+ x144)+ z143+ 0'+ 0'⇒∀x1 ¬z144+ x1'=z32)⇒¬∀z146 ∀y146 ∀x145 (z145=x145⇒(( z145+ x146)*( z145+ x146)+ z145+ 0'=z146⇒(¬∀x147 (¬∀x1 ¬x147=z146+ x1'⇒(¬∀x1 ¬x44=z146+ x1*x147⇒¬x147=( y146'*y44)'))⇒(y146=( ( ( z143+ x144)*( z143+ x144)+ z143+ 0'+ y144)*( ( z143+ x144)*( z143+ x144)+ z143+ 0'+ y144)+ ( z143+ x144)*( z143+ x144)+ z143+ 0'+ 0'+ 0)*( ( ( z143+ x144)*( z143+ x144)+ z143+ 0'+ y144)*( ( z143+ x144)*( z143+ x144)+ z143+ 0'+ y144)+ ( z143+ x144)*( z143+ x144)+ z143+ 0'+ 0'+ 0)+ ( ( z143+ x144)*( z143+ x144)+ z143+ 0'+ y144)*( ( z143+ x144)*( z143+ x144)+ z143+ 0'+ y144)+ ( z143+ x144)*( z143+ x144)+ z143+ 0'+ 0'+ 0'⇒∀y145 (¬∀x1 ¬y145=x145+ x1'⇒(¬∀x1 ¬x33=x145+ x1*y145⇒¬y145=( z144'*y33)')))))))⇒(∀x112 ∀z111 ∀y111 ∀x111 ∀z110 (¬(x112=( ( ( z110+ x111)*( z110+ x111)+ z110+ 0'+ y111)*( ( z110+ x111)*( z110+ x111)+ z110+ 0'+ y111)+ ( z110+ x111)*( z110+ x111)+ z110+ 0'+ 0'+ z111)*( ( ( z110+ x111)*( z110+ x111)+ z110+ 0'+ y111)*( ( z110+ x111)*( z110+ x111)+ z110+ 0'+ y111)+ ( z110+ x111)*( z110+ x111)+ z110+ 0'+ 0'+ z111)+ ( ( z110+ x111)*( z110+ x111)+ z110+ 0'+ y111)*( ( z110+ x111)*( z110+ x111)+ z110+ 0'+ y111)+ ( z110+ x111)*( z110+ x111)+ z110+ 0'+ 0'+ 0'⇒∀x1 ¬x112+ x1'=z43)⇒¬∀z113 ∀y113 ∀y112 (¬((z110=0⇒( 0+ 0)*( 0+ 0)+ 0+ 0'=y112)⇒¬(¬z110=0⇒¬∀y134 ∀x134 ∀y133 ∀x133 ∀y132 ∀x132 ∀x131 ∀y131 ∀x130 ∀z129 ∀x128 ∀z127 ∀y126 ∀x126 ∀y125 ∀x125 ∀z123 ∀y123 ∀x122 ∀z121 ∀x121 ∀z120 ∀y120 ∀x120 ∀z118 ∀y118 ∀z117 ∀y117 ∀x116 ∀z115 ∀z114 ∀y114 ∀x114 ((0'*0'''+ 0'=x114⇒( y134+ x129)*( y134+ x129)+ y134+ 0'=y112)⇒(¬∀z134 (¬∀x1 ¬z134=y134+ x1'⇒(¬∀x1 ¬x21=y134+ x1*z134⇒¬z134=( x134'*y21)'))⇒(x134=( ( 0'*0'''+ 0'+ 0''*y133)*( 0'*0'''+ 0'+ 0''*y133)+ 0'*0'''+ 0'+ 0'+ z128)*( ( 0'*0'''+ 0'+ 0''*y133)*( 0'*0'''+ 0'+ 0''*y133)+ 0'*0'''+ 0'+ 0'+ z128)+ ( 0'*0'''+ 0'+ 0''*y133)*( 0'*0'''+ 0'+ 0''*y133)+ 0'*0'''+ 0'+ 0'+ 0'⇒(¬∀z133 (¬∀x1 ¬z133=y133+ x1'⇒(¬∀x1 ¬x19=y133+ x1*z133⇒¬z133=( x133'*y19)'))⇒(x133=x127⇒(( z128+ x129)*( z128+ x129)+ z128+ 0'=y129⇒(¬((x127=x111⇒x130=y129)⇒¬(¬x127=x111⇒y132=y129))⇒(¬∀z132 (¬∀x1 ¬z132=y132+ x1'⇒(¬∀x1 ¬x44=y132+ x1*z132⇒¬z132=( x132'*y44)'))⇒(x132=( ( ( y127+ x111)*( y127+ x111)+ y127+ 0'+ y111)*( ( y127+ x111)*( y127+ x111)+ y127+ 0'+ y111)+ ( y127+ x111)*( y127+ x111)+ y127+ 0'+ 0'+ z130)*( ( ( y127+ x111)*( y127+ x111)+ y127+ 0'+ y111)*( ( y127+ x111)*( y127+ x111)+ y127+ 0'+ y111)+ ( y127+ x111)*( y127+ x111)+ y127+ 0'+ 0'+ z130)+ ( ( y127+ x111)*( y127+ x111)+ y127+ 0'+ y111)*( ( y127+ x111)*( y127+ x111)+ y127+ 0'+ y111)+ ( y127+ x111)*( y127+ x111)+ y127+ 0'+ 0'+ 0'⇒(¬((y111=0⇒z111=z130)⇒¬(¬y111=0⇒y131=z130))⇒(¬∀z131 (¬∀x1 ¬z131=y131+ x1'⇒(¬∀x1 ¬y6=y131+ x1*z131⇒¬z131=( x131'*z6)'))⇒(x131=( x127+ z111)*( x127+ z111)+ x127+ 0'⇒(¬∀y130 (¬∀x1 ¬y130=x130+ x1'⇒(¬∀x1 ¬x24=x130+ x1*y130⇒¬y130=( z129'*y24)'))⇒(z129=y127⇒(( x127+ y127)*( x127+ y127)+ x127+ 0'=x128⇒(¬∀y128 (¬∀x1 ¬y128=x128+ x1'⇒(¬∀x1 ¬x18=x128+ x1*y128⇒¬y128=( z127'*y18)'))⇒(z127=x113⇒((0''=x114⇒( y126+ z124)*( y126+ z124)+ y126+ 0'=y112)⇒(¬∀z126 (¬∀x1 ¬z126=y126+ x1'⇒(¬∀x1 ¬x21=y126+ x1*z126⇒¬z126=( x126'*y21)'))⇒(x126=( ( 0''+ z122)*( 0''+ z122)+ 0''+ 0'+ y124)*( ( 0''+ z122)*( 0''+ z122)+ 0''+ 0'+ y124)+ ( 0''+ z122)*( 0''+ z122)+ 0''+ 0'+ 0'⇒(( y124+ z124)*( y124+ z124)+ y124+ 0'=y125⇒(¬∀z125 (¬∀x1 ¬z125=y125+ x1'⇒(¬∀x1 ¬x44=y125+ x1*z125⇒¬z125=( x125'*y44)'))⇒(x125=( ( ( x123+ x111)*( x123+ x111)+ x123+ 0'+ y111)*( ( x123+ x111)*( x123+ x111)+ x123+ 0'+ y111)+ ( x123+ x111)*( x123+ x111)+ x123+ 0'+ 0'+ z111)*( ( ( x123+ x111)*( x123+ x111)+ x123+ 0'+ y111)*( ( x123+ x111)*( x123+ x111)+ x123+ 0'+ y111)+ ( x123+ x111)*( x123+ x111)+ x123+ 0'+ 0'+ z111)+ ( ( x123+ x111)*( x123+ x111)+ x123+ 0'+ y111)*( ( x123+ x111)*( x123+ x111)+ x123+ 0'+ y111)+ ( x123+ x111)*( x123+ x111)+ x123+ 0'+ 0'+ 0'⇒(( z122+ x123)*( z122+ x123)+ z122+ 0'=z123⇒(¬∀x124 (¬∀x1 ¬x124=z123+ x1'⇒(¬∀x1 ¬x44=z123+ x1*x124⇒¬x124=( y123'*y44)'))⇒(y123=( ( ( x113+ x111)*( x113+ x111)+ x113+ 0'+ y111)*( ( x113+ x111)*( x113+ x111)+ x113+ 0'+ y111)+ ( x113+ x111)*( x113+ x111)+ x113+ 0'+ 0'+ z111)*( ( ( x113+ x111)*( x113+ x111)+ x113+ 0'+ y111)*( ( x113+ x111)*( x113+ x111)+ x113+ 0'+ y111)+ ( x113+ x111)*( x113+ x111)+ x113+ 0'+ 0'+ z111)+ ( ( x113+ x111)*( x113+ x111)+ x113+ 0'+ y111)*( ( x113+ x111)*( x113+ x111)+ x113+ 0'+ y111)+ ( x113+ x111)*( x113+ x111)+ x113+ 0'+ 0'+ 0'⇒((0'=x114⇒( x122+ z119)*( x122+ z119)+ x122+ 0'=y112)⇒(¬∀y122 (¬∀x1 ¬y122=x122+ x1'⇒(¬∀x1 ¬x20=x122+ x1*y122⇒¬y122=( z121'*y20)'))⇒(z121=( 0'+ y119)*( 0'+ y119)+ 0'+ 0'⇒(( y119+ z119)*( y119+ z119)+ y119+ 0'=x121⇒(¬∀y121 (¬∀x1 ¬y121=x121+ x1'⇒(¬∀x1 ¬x44=x121+ x1*y121⇒¬y121=( z120'*y44)'))⇒(z120=( ( ( x120+ x111)*( x120+ x111)+ x120+ 0'+ y111)*( ( x120+ x111)*( x120+ x111)+ x120+ 0'+ y111)+ ( x120+ x111)*( x120+ x111)+ x120+ 0'+ 0'+ z111)*( ( ( x120+ x111)*( x120+ x111)+ x120+ 0'+ y111)*( ( x120+ x111)*( x120+ x111)+ x120+ 0'+ y111)+ ( x120+ x111)*( x120+ x111)+ x120+ 0'+ 0'+ z111)+ ( ( x120+ x111)*( x120+ x111)+ x120+ 0'+ y111)*( ( x120+ x111)*( x120+ x111)+ x120+ 0'+ y111)+ ( x120+ x111)*( x120+ x111)+ x120+ 0'+ 0'+ 0'⇒(¬∀x1 ¬y120+ x1'=0'*0'''+ 0'⇒(z110=x120*( 0'*0'''+ 0')+ y120⇒((0=x114⇒( z118+ x117)*( z118+ x117)+ z118+ 0'=y112)⇒(¬∀x119 (¬∀x1 ¬x119=z118+ x1'⇒(¬∀x1 ¬x21=z118+ x1*x119⇒¬x119=( y118'*y21)'))⇒(y118=( ( 0+ x115)*( 0+ x115)+ 0+ 0'+ z116)*( ( 0+ x115)*( 0+ x115)+ 0+ 0'+ z116)+ ( 0+ x115)*( 0+ x115)+ 0+ 0'+ 0'⇒(( z116+ x117)*( z116+ x117)+ z116+ 0'=z117⇒(¬∀x118 (¬∀x1 ¬x118=z117+ x1'⇒(¬∀x1 ¬x43=z117+ x1*x118⇒¬x118=( y117'*y43)'))⇒(y117=( ( ( y115+ x111)*( y115+ x111)+ y115+ 0'+ y111)*( ( y115+ x111)*( y115+ x111)+ y115+ 0'+ y111)+ ( y115+ x111)*( y115+ x111)+ y115+ 0'+ 0'+ z111)*( ( ( y115+ x111)*( y115+ x111)+ y115+ 0'+ y111)*( ( y115+ x111)*( y115+ x111)+ y115+ 0'+ y111)+ ( y115+ x111)*( y115+ x111)+ y115+ 0'+ 0'+ z111)+ ( ( y115+ x111)*( y115+ x111)+ y115+ 0'+ y111)*( ( y115+ x111)*( y115+ x111)+ y115+ 0'+ y111)+ ( y115+ x111)*( y115+ x111)+ y115+ 0'+ 0'+ 0'⇒(( x115+ y115)*( x115+ y115)+ x115+ 0'=x116⇒(¬∀y116 (¬∀x1 ¬y116=x116+ x1'⇒(¬∀x1 ¬x43=x116+ x1*y116⇒¬y116=( z115'*y43)'))⇒(z115=( ( ( x113+ x111)*( x113+ x111)+ x113+ 0'+ y111)*( ( x113+ x111)*( x113+ x111)+ x113+ 0'+ y111)+ ( x113+ x111)*( x113+ x111)+ x113+ 0'+ 0'+ z111)*( ( ( x113+ x111)*( x113+ x111)+ x113+ 0'+ y111)*( ( x113+ x111)*( x113+ x111)+ x113+ 0'+ y111)+ ( x113+ x111)*( x113+ x111)+ x113+ 0'+ 0'+ z111)+ ( ( x113+ x111)*( x113+ x111)+ x113+ 0'+ y111)*( ( x113+ x111)*( x113+ x111)+ x113+ 0'+ y111)+ ( x113+ x111)*( x113+ x111)+ x113+ 0'+ 0'+ 0'⇒(z114=x114⇒(¬∀x1 ¬z114+ x1'=0'*0'''+ 0'⇒¬z110=y114*( 0'*0'''+ 0')+ z114)))))))))))))))))))))))))))))))))))))))))))))))⇒(¬∀x1 ¬z113+ x1'=0'*0'''+ 0'⇒(z110=y113*( 0'*0'''+ 0')+ z113⇒∀z112 (¬∀x1 ¬z112=y112+ x1'⇒(¬∀x1 ¬x44=y112+ x1*z112⇒¬z112=( x112'*y44)'))))))⇒(∀y96 ∀x96 ∀z95 ∀y95 ∀x95 (¬(y96=( ( ( x95+ y95)*( x95+ y95)+ x95+ 0'+ z95)*( ( x95+ y95)*( x95+ y95)+ x95+ 0'+ z95)+ ( x95+ y95)*( x95+ y95)+ x95+ 0'+ 0'+ x96)*( ( ( x95+ y95)*( x95+ y95)+ x95+ 0'+ z95)*( ( x95+ y95)*( x95+ y95)+ x95+ 0'+ z95)+ ( x95+ y95)*( x95+ y95)+ x95+ 0'+ 0'+ x96)+ ( ( x95+ y95)*( x95+ y95)+ x95+ 0'+ z95)*( ( x95+ y95)*( x95+ y95)+ x95+ 0'+ z95)+ ( x95+ y95)*( x95+ y95)+ x95+ 0'+ 0'+ 0'⇒∀x1 ¬y96+ x1'=z42)⇒¬∀x110 ∀z109 ∀x109 ∀z108 ∀x108 ∀z107 ∀y106 ∀x106 ∀y105 ∀x105 ∀x104 ∀z103 ∀x103 ∀z102 ∀z101 ∀y101 ∀z100 ∀y100 ∀z99 ∀y99 ∀x99 ∀z98 ∀z97 ∀y97 ∀z96 (¬((z97=0⇒¬((x98=y95⇒¬((z95=0⇒( 0+ 0)*( 0+ 0)+ 0+ 0'=z96)⇒¬(¬z95=0⇒¬((z100=0⇒( 0+ 0)*( 0+ 0)+ 0+ 0'=z96)⇒¬(¬z100=0⇒( z95+ y98)*( z95+ y98)+ z95+ 0'=z96)))))⇒¬(¬x98=y95⇒( 0''*z101+ y98)*( 0''*z101+ y98)+ 0''*z101+ 0'=z96)))⇒¬(¬z97=0⇒¬((y103=0'⇒( ( 0'*0'''+ 0')*0'''+ 0+ y102)*( ( 0'*0'''+ 0')*0'''+ 0+ y102)+ ( 0'*0'''+ 0')*0'''+ 0+ 0'=z96)⇒¬(¬y103=0'⇒¬((y104=0⇒( 0+ 0)*( 0+ 0)+ 0+ 0'=z96)⇒¬(¬y104=0⇒¬((y103=0'*0'''+ 0'⇒( y106+ z104)*( y106+ z104)+ y106+ 0'=z96)⇒¬(¬y103=0'*0'''+ 0'⇒¬((x107=0⇒( 0+ 0)*( 0+ 0)+ 0+ 0'=z96)⇒¬(¬x107=0⇒¬((y103=0'*0'''+ 0'⇒( x109+ y107)*( x109+ y107)+ x109+ 0'=z96)⇒¬(¬y103=0'*0'''+ 0'⇒( x110+ y107)*( x110+ y107)+ x110+ 0'=z96))))))))))))⇒(¬∀y110 (¬∀x1 ¬y110=x110+ x1'⇒(¬∀x1 ¬x21=x110+ x1*y110⇒¬y110=( z109'*y21)'))⇒(z109=( ( 0''*0'''+ 0''+ y104)*( 0''*0'''+ 0''+ y104)+ 0''*0'''+ 0''+ 0'+ x107)*( ( 0''*0'''+ 0''+ y104)*( 0''*0'''+ 0''+ y104)+ 0''*0'''+ 0''+ 0'+ x107)+ ( 0''*0'''+ 0''+ y104)*( 0''*0'''+ 0''+ y104)+ 0''*0'''+ 0''+ 0'+ 0'⇒(¬∀y109 (¬∀x1 ¬y109=x109+ x1'⇒(¬∀x1 ¬x21=x109+ x1*y109⇒¬y109=( z108'*y21)'))⇒(z108=( ( 0''*0'''+ 0''+ y104)*( 0''*0'''+ 0''+ y104)+ 0''*0'''+ 0''+ 0'+ x107)*( ( 0''*0'''+ 0''+ y104)*( 0''*0'''+ 0''+ y104)+ 0''*0'''+ 0''+ 0'+ x107)+ ( 0''*0'''+ 0''+ y104)*( 0''*0'''+ 0''+ y104)+ 0''*0'''+ 0''+ 0'+ 0'⇒(( x107+ y107)*( x107+ y107)+ x107+ 0'=x108⇒(¬∀y108 (¬∀x1 ¬y108=x108+ x1'⇒(¬∀x1 ¬x43=x108+ x1*y108⇒¬y108=( z107'*y43)'))⇒(z107=( ( ( z104+ y95)*( z104+ y95)+ z104+ 0'+ z95)*( ( z104+ y95)*( z104+ y95)+ z104+ 0'+ z95)+ ( z104+ y95)*( z104+ y95)+ z104+ 0'+ 0'+ x96)*( ( ( z104+ y95)*( z104+ y95)+ z104+ 0'+ z95)*( ( z104+ y95)*( z104+ y95)+ z104+ 0'+ z95)+ ( z104+ y95)*( z104+ y95)+ z104+ 0'+ 0'+ x96)+ ( ( z104+ y95)*( z104+ y95)+ z104+ 0'+ z95)*( ( z104+ y95)*( z104+ y95)+ z104+ 0'+ z95)+ ( z104+ y95)*( z104+ y95)+ z104+ 0'+ 0'+ 0'⇒(¬∀z106 (¬∀x1 ¬z106=y106+ x1'⇒(¬∀x1 ¬x20=y106+ x1*z106⇒¬z106=( x106'*y20)'))⇒(x106=( 0'*0'''+ 0'+ y104)*( 0'*0'''+ 0'+ y104)+ 0'*0'''+ 0'+ 0'⇒(( y104+ z104)*( y104+ z104)+ y104+ 0'=y105⇒(¬∀z105 (¬∀x1 ¬z105=y105+ x1'⇒(¬∀x1 ¬x43=y105+ x1*z105⇒¬z105=( x105'*y43)'))⇒(x105=( ( ( y102+ y95)*( y102+ y95)+ y102+ 0'+ z95)*( ( y102+ y95)*( y102+ y95)+ y102+ 0'+ z95)+ ( y102+ y95)*( y102+ y95)+ y102+ 0'+ 0'+ x96)*( ( ( y102+ y95)*( y102+ y95)+ y102+ 0'+ z95)*( ( y102+ y95)*( y102+ y95)+ y102+ 0'+ z95)+ ( y102+ y95)*( y102+ y95)+ y102+ 0'+ 0'+ x96)+ ( ( y102+ y95)*( y102+ y95)+ y102+ 0'+ z95)*( ( y102+ y95)*( y102+ y95)+ y102+ 0'+ z95)+ ( y102+ y95)*( y102+ y95)+ y102+ 0'+ 0'+ 0'⇒(¬∀x1 ¬x104+ x1'=0''*0'''+ 0''⇒(x95=z103*( 0''*0'''+ 0'')+ x104⇒(¬∀x1 ¬x103+ x1'=0''*0'''+ 0''⇒(x95=z102*( 0''*0'''+ 0'')+ x103⇒(¬∀x102 (¬∀x1 ¬x102=z101+ x1'⇒(¬∀x1 ¬x19=z101+ x1*x102⇒¬x102=( y101'*y19)'))⇒(y101=x98⇒(¬∀x101 (¬∀x1 ¬x101=z100+ x1'⇒(¬∀x1 ¬y84=z100+ x1*x101⇒¬x101=( y100'*z84)'))⇒(y100=( z95+ x96)*( z95+ x96)+ z95+ 0'⇒(( x98+ y98)*( x98+ y98)+ x98+ 0'=z99⇒(¬∀x100 (¬∀x1 ¬x100=z99+ x1'⇒(¬∀x1 ¬x18=z99+ x1*x100⇒¬x100=( y99'*y18)'))⇒(y99=z98⇒(¬∀x1 ¬x99+ x1'=0''⇒(x95=z98*0''+ x99⇒(¬∀x1 ¬z97+ x1'=0''⇒(x95=y97*0''+ z97⇒∀x97 (¬∀x1 ¬x97=z96+ x1'⇒(¬∀x1 ¬x43=z96+ x1*x97⇒¬x97=( y96'*y43)')))))))))))))))))))))))))))))))⇒(∀z85 ∀y85 ∀x85 (¬(z85=( x85+ y85)*( x85+ y85)+ x85+ 0'⇒∀x1 ¬z85+ x1'=x84)⇒¬∀y94 ∀x94 ∀y93 ∀x93 ∀y92 ∀x92 ∀y91 ∀x91 ∀x90 ∀z89 ∀x89 ∀z88 ∀y88 ∀x88 ∀x87 ∀z86 ∀x86 (¬((x85=0⇒0=x86)⇒¬(¬x85=0⇒¬((x87=0⇒¬((x90=0'⇒0=x86)⇒¬(¬x90=0'⇒z87=x86)))⇒¬(¬x87=0⇒¬((z91=0'⇒z90=x86)⇒¬(¬z91=0'⇒¬((z91=0'*0'''+ 0'⇒z92=x86)⇒¬(¬z91=0'*0'''+ 0'⇒y94=x86))))))))⇒(¬∀z94 (¬∀x1 ¬z94=y94+ x1'⇒(¬∀x1 ¬y84=y94+ x1*z94⇒¬z94=( x94'*z84)'))⇒(x94=( z92+ y85)*( z92+ y85)+ z92+ 0'⇒(¬∀z93 (¬∀x1 ¬z93=y93+ x1'⇒(¬∀x1 ¬y84=y93+ x1*z93⇒¬z93=( x93'*z84)'))⇒(x93=( z90+ y85)*( z90+ y85)+ z90+ 0'⇒(¬∀x1 ¬y92+ x1'=0''*0'''+ 0''⇒(x85=x92*( 0''*0'''+ 0'')+ y92⇒(¬∀x1 ¬y91+ x1'=0''*0'''+ 0''⇒(x85=x91*( 0''*0'''+ 0'')+ y91⇒(¬∀y90 (¬∀x1 ¬y90=x90+ x1'⇒(¬∀x1 ¬x42=x90+ x1*y90⇒¬y90=( z89'*y42)'))⇒(z89=( y87+ y85)*( y87+ y85)+ y87+ 0'⇒(( y87+ z87)*( y87+ z87)+ y87+ 0'=x89⇒(¬∀y89 (¬∀x1 ¬y89=x89+ x1'⇒(¬∀x1 ¬x18=x89+ x1*y89⇒¬y89=( z88'*y18)'))⇒(z88=x88⇒(¬∀x1 ¬y88+ x1'=0''⇒(x85=x88*0''+ y88⇒(¬∀x1 ¬x87+ x1'=0''⇒(x85=z86*0''+ x87⇒∀y86 (¬∀x1 ¬y86=x86+ x1'⇒(¬∀x1 ¬y84=x86+ x1*y86⇒¬y86=( z85'*z84)')))))))))))))))))))))⇒(∀x79 ∀z78 ∀y78 (¬(x79=( y78+ z78)*( y78+ z78)+ y78+ 0'⇒∀x1 ¬x79+ x1'=z41)⇒¬∀y83 ∀x83 ∀y82 ∀x82 ∀y81 ∀x81 ∀y80 ∀x80 ∀y79 (¬((y80=0⇒0=y79)⇒¬(¬y80=0⇒¬((y78=y81⇒0'=y79)⇒¬(¬y78=y81⇒y83=y79))))⇒(¬∀z83 (¬∀x1 ¬z83=y83+ x1'⇒(¬∀x1 ¬x42=y83+ x1*z83⇒¬z83=( x83'*y42)'))⇒(x83=( y78+ y82)*( y78+ y82)+ y78+ 0'⇒(¬∀z82 (¬∀x1 ¬z82=y82+ x1'⇒(¬∀x1 ¬y9=y82+ x1*z82⇒¬z82=( x82'*z9)'))⇒(x82=z78⇒(¬∀z81 (¬∀x1 ¬z81=y81+ x1'⇒(¬∀x1 ¬y7=y81+ x1*z81⇒¬z81=( x81'*z7)'))⇒(x81=( z78+ 0)*( z78+ 0)+ z78+ 0'⇒(¬∀z80 (¬∀x1 ¬z80=y80+ x1'⇒(¬∀x1 ¬y8=y80+ x1*z80⇒¬z80=( x80'*z8)'))⇒(x80=z78⇒∀z79 (¬∀x1 ¬z79=y79+ x1'⇒(¬∀x1 ¬x42=y79+ x1*z79⇒¬z79=( x79'*y42)'))))))))))))⇒(∀z159 ∀y159 ∀x159 (¬(z159=( x159+ y159)*( x159+ y159)+ x159+ 0'⇒∀x1 ¬z159+ x1'=z26)⇒¬∀x167 ∀z166 ∀x166 ∀z165 ∀x165 ∀z164 ∀x164 ∀z163 ∀x163 ∀z162 ∀x162 ∀z161 ∀x161 ∀z160 ∀x160 (x167=x160⇒(¬∀y167 (¬∀x1 ¬y167=x167+ x1'⇒(¬∀x1 ¬x40=x167+ x1*y167⇒¬y167=( z166'*y40)'))⇒(z166=( x163+ x166)*( x163+ x166)+ x163+ 0'⇒(¬∀y166 (¬∀x1 ¬y166=x166+ x1'⇒(¬∀x1 ¬x40=x166+ x1*y166⇒¬y166=( z165'*y40)'))⇒(z165=( x165+ y159)*( x165+ y159)+ x165+ 0'⇒(¬∀y165 (¬∀x1 ¬y165=x165+ x1'⇒(¬∀x1 ¬x40=x165+ x1*y165⇒¬y165=( z164'*y40)'))⇒(z164=( x164+ x159)*( x164+ x159)+ x164+ 0'⇒(¬∀y164 (¬∀x1 ¬y164=x164+ x1'⇒(¬∀x1 ¬x41=x164+ x1*y164⇒¬y164=( z163'*y41)'))⇒(z163=y159⇒(¬∀y163 (¬∀x1 ¬y163=x163+ x1'⇒(¬∀x1 ¬x40=x163+ x1*y163⇒¬y163=( z162'*y40)'))⇒(z162=( x161+ x162)*( x161+ x162)+ x161+ 0'⇒(¬∀y162 (¬∀x1 ¬y162=x162+ x1'⇒(¬∀x1 ¬x41=x162+ x1*y162⇒¬y162=( z161'*y41)'))⇒(z161=x159⇒(¬∀y161 (¬∀x1 ¬y161=x161+ x1'⇒(¬∀x1 ¬x41=x161+ x1*y161⇒¬y161=( z160'*y41)'))⇒(z160=y159⇒∀y160 (¬∀x1 ¬y160=x160+ x1'⇒(¬∀x1 ¬x27=x160+ x1*y160⇒¬y160=( z159'*y27)'))))))))))))))))))⇒(∀x138 ∀z137 (¬(x138=z137⇒∀x1 ¬x138+ x1'=z40)⇒¬∀y139 ∀x139 ∀y138 (y139=y138⇒(¬∀z139 (¬∀x1 ¬z139=y139+ x1'⇒(¬∀x1 ¬x20=y139+ x1*z139⇒¬z139=( x139'*y20)'))⇒(x139=( 0'+ z137)*( 0'+ z137)+ 0'+ 0'⇒∀z138 (¬∀x1 ¬z138=y138+ x1'⇒(¬∀x1 ¬x41=y138+ x1*z138⇒¬z138=( x138'*y41)'))))))⇒(∀x152 ∀z151 ∀y151 ∀x151 (¬(x152=( ( x151+ y151)*( x151+ y151)+ x151+ 0'+ z151)*( ( x151+ y151)*( x151+ y151)+ x151+ 0'+ z151)+ ( x151+ y151)*( x151+ y151)+ x151+ 0'+ 0'⇒∀x1 ¬x152+ x1'=z25)⇒¬∀y158 ∀x158 ∀y157 ∀x157 ∀y156 ∀x156 ∀y155 ∀x155 ∀y154 ∀x154 ∀y153 ∀x153 ∀y152 (y158=y152⇒(¬∀z158 (¬∀x1 ¬z158=y158+ x1'⇒(¬∀x1 ¬x40=y158+ x1*z158⇒¬z158=( x158'*y40)'))⇒(x158=( y154+ y157)*( y154+ y157)+ y154+ 0'⇒(¬∀z157 (¬∀x1 ¬z157=y157+ x1'⇒(¬∀x1 ¬x40=y157+ x1*z157⇒¬z157=( x157'*y40)'))⇒(x157=( y155+ y156)*( y155+ y156)+ y155+ 0'⇒(¬∀z156 (¬∀x1 ¬z156=y156+ x1'⇒(¬∀x1 ¬x40=y156+ x1*z156⇒¬z156=( x156'*y40)'))⇒(x156=( x151+ z151)*( x151+ z151)+ x151+ 0'⇒(¬∀z155 (¬∀x1 ¬z155=y155+ x1'⇒(¬∀x1 ¬x40=y155+ x1*z155⇒¬z155=( x155'*y40)'))⇒(x155=( x151+ y151)*( x151+ y151)+ x151+ 0'⇒(¬∀z154 (¬∀x1 ¬z154=y154+ x1'⇒(¬∀x1 ¬x40=y154+ x1*z154⇒¬z154=( x154'*y40)'))⇒(x154=( x151+ y153)*( x151+ y153)+ x151+ 0'⇒(¬∀z153 (¬∀x1 ¬z153=y153+ x1'⇒(¬∀x1 ¬x40=y153+ x1*z153⇒¬z153=( x153'*y40)'))⇒(x153=( y151+ z151)*( y151+ z151)+ y151+ 0'⇒∀z152 (¬∀x1 ¬z152=y152+ x1'⇒(¬∀x1 ¬x26=y152+ x1*z152⇒¬z152=( x152'*y26)'))))))))))))))))⇒(∀x148 ∀z147 ∀y147 (¬(x148=( y147+ z147)*( y147+ z147)+ y147+ 0'⇒∀x1 ¬x148+ x1'=z24)⇒¬∀y150 ∀x150 ∀y149 ∀x149 ∀y148 (y150=y148⇒(¬∀z150 (¬∀x1 ¬z150=y150+ x1'⇒(¬∀x1 ¬x40=y150+ x1*z150⇒¬z150=( x150'*y40)'))⇒(x150=( y147+ y149)*( y147+ y149)+ y147+ 0'⇒(¬∀z149 (¬∀x1 ¬z149=y149+ x1'⇒(¬∀x1 ¬x40=y149+ x1*z149⇒¬z149=( x149'*y40)'))⇒(x149=( z147+ y147)*( z147+ y147)+ z147+ 0'⇒∀z148 (¬∀x1 ¬z148=y148+ x1'⇒(¬∀x1 ¬x25=y148+ x1*z148⇒¬z148=( x148'*y25)'))))))))⇒(∀z135 ∀y135 ∀x135 (¬(z135=( x135+ y135)*( x135+ y135)+ x135+ 0'⇒∀x1 ¬z135+ x1'=z39)⇒¬∀x137 ∀z136 ∀x136 (x137=x136⇒(¬∀y137 (¬∀x1 ¬y137=x137+ x1'⇒(¬∀x1 ¬x21=x137+ x1*y137⇒¬y137=( z136'*y21)'))⇒(z136=( ( 0''+ x135)*( 0''+ x135)+ 0''+ 0'+ y135)*( ( 0''+ x135)*( 0''+ x135)+ 0''+ 0'+ y135)+ ( 0''+ x135)*( 0''+ x135)+ 0''+ 0'+ 0'⇒∀y136 (¬∀x1 ¬y136=x136+ x1'⇒(¬∀x1 ¬x40=x136+ x1*y136⇒¬y136=( z135'*y40)'))))))⇒(∀z208 ∀y208 (¬(z208=y208⇒∀x1 ¬z208+ x1'=z23)⇒¬∀y210 ∀x210 ∀x209 (¬∀y228 ∀x228 ∀y227 ∀x227 ∀y226 ∀x226 ∀z224 ∀y224 ∀x223 ∀z222 ∀x222 ∀z221 ∀y220 ∀x220 ∀z218 ∀y218 ∀z217 ∀y217 ∀x217 ∀z216 ∀y215 ∀x215 ∀y214 ∀x214 ∀z212 ∀y212 ∀y211 ∀x211 ∀z210 ((0'*0'''+ 0'=z210⇒( y228+ z225)*( y228+ z225)+ y228+ 0'=x209)⇒(¬∀z228 (¬∀x1 ¬z228=y228+ x1'⇒(¬∀x1 ¬x21=y228+ x1*z228⇒¬z228=( x228'*y21)'))⇒(x228=( ( 0'*0'''+ 0'+ y227)*( 0'*0'''+ 0'+ y227)+ 0'*0'''+ 0'+ 0'+ y225)*( ( 0'*0'''+ 0'+ y227)*( 0'*0'''+ 0'+ y227)+ 0'*0'''+ 0'+ 0'+ y225)+ ( 0'*0'''+ 0'+ y227)*( 0'*0'''+ 0'+ y227)+ 0'*0'''+ 0'+ 0'+ 0'⇒(¬∀z227 (¬∀x1 ¬z227=y227+ x1'⇒(¬∀x1 ¬x19=y227+ x1*z227⇒¬z227=( x227'*y19)'))⇒(x227=z223⇒(( y225+ z225)*( y225+ z225)+ y225+ 0'=y226⇒(¬∀z226 (¬∀x1 ¬z226=y226+ x1'⇒(¬∀x1 ¬x24=y226+ x1*z226⇒¬z226=( x226'*y24)'))⇒(x226=x224⇒(( z223+ x224)*( z223+ x224)+ z223+ 0'=z224⇒(¬∀x225 (¬∀x1 ¬x225=z224+ x1'⇒(¬∀x1 ¬x18=z224+ x1*x225⇒¬x225=( y224'*y18)'))⇒(y224=z209⇒((0''=z210⇒( x223+ y221)*( x223+ y221)+ x223+ 0'=x209)⇒(¬∀y223 (¬∀x1 ¬y223=x223+ x1'⇒(¬∀x1 ¬x21=x223+ x1*y223⇒¬y223=( z222'*y21)'))⇒(z222=( ( 0''+ y219)*( 0''+ y219)+ 0''+ 0'+ x221)*( ( 0''+ y219)*( 0''+ y219)+ 0''+ 0'+ x221)+ ( 0''+ y219)*( 0''+ y219)+ 0''+ 0'+ 0'⇒(( x221+ y221)*( x221+ y221)+ x221+ 0'=x222⇒(¬∀y222 (¬∀x1 ¬y222=x222+ x1'⇒(¬∀x1 ¬x24=x222+ x1*y222⇒¬y222=( z221'*y24)'))⇒(z221=z219⇒(( y219+ z219)*( y219+ z219)+ y219+ 0'=y220⇒(¬∀z220 (¬∀x1 ¬z220=y220+ x1'⇒(¬∀x1 ¬x24=y220+ x1*z220⇒¬z220=( x220'*y24)'))⇒(x220=z209⇒((0'=z210⇒( z218+ y216)*( z218+ y216)+ z218+ 0'=x209)⇒(¬∀x219 (¬∀x1 ¬x219=z218+ x1'⇒(¬∀x1 ¬x20=z218+ x1*x219⇒¬x219=( y218'*y20)'))⇒(y218=( 0'+ x216)*( 0'+ x216)+ 0'+ 0'⇒(( x216+ y216)*( x216+ y216)+ x216+ 0'=z217⇒(¬∀x218 (¬∀x1 ¬x218=z217+ x1'⇒(¬∀x1 ¬x24=z217+ x1*x218⇒¬x218=( y217'*y24)'))⇒(y217=z216⇒(¬∀x1 ¬x217+ x1'=0'*0'''+ 0'⇒(y208=z216*( 0'*0'''+ 0')+ x217⇒((0=z210⇒( y215+ z213)*( y215+ z213)+ y215+ 0'=x209)⇒(¬∀z215 (¬∀x1 ¬z215=y215+ x1'⇒(¬∀x1 ¬x21=y215+ x1*z215⇒¬z215=( x215'*y21)'))⇒(x215=( ( 0+ z211)*( 0+ z211)+ 0+ 0'+ y213)*( ( 0+ z211)*( 0+ z211)+ 0+ 0'+ y213)+ ( 0+ z211)*( 0+ z211)+ 0+ 0'+ 0'⇒(( y213+ z213)*( y213+ z213)+ y213+ 0'=y214⇒(¬∀z214 (¬∀x1 ¬z214=y214+ x1'⇒(¬∀x1 ¬x23=y214+ x1*z214⇒¬z214=( x214'*y23)'))⇒(x214=x212⇒(( z211+ x212)*( z211+ x212)+ z211+ 0'=z212⇒(¬∀x213 (¬∀x1 ¬x213=z212+ x1'⇒(¬∀x1 ¬x23=z212+ x1*x213⇒¬x213=( y212'*y23)'))⇒(y212=z209⇒(y211=z210⇒(¬∀x1 ¬y211+ x1'=0'*0'''+ 0'⇒¬y208=x211*( 0'*0'''+ 0')+ y211)))))))))))))))))))))))))))))))))))))))⇒(¬∀x1 ¬y210+ x1'=0'*0'''+ 0'⇒(y208=x210*( 0'*0'''+ 0')+ y210⇒∀y209 (¬∀x1 ¬y209=x209+ x1'⇒(¬∀x1 ¬x24=x209+ x1*y209⇒¬y209=( z208'*y24)'))))))⇒(∀z196 ∀y196 (¬(z196=y196⇒∀x1 ¬z196+ x1'=z22)⇒¬∀z203 ∀y203 ∀x202 ∀z201 ∀z200 ∀y200 ∀y199 ∀x199 ∀z198 ∀y198 ∀x198 ∀z197 ∀x197 (¬((x198=0⇒y199=x197)⇒¬(¬x198=0⇒¬∀z207 ∀y207 ∀z206 ∀y206 ∀z205 ∀y205 ∀x205 ∀z204 ∀y204 ((0''*0'''+ 0''=y204⇒( z207+ x203)*( z207+ x203)+ z207+ 0'=x197)⇒(¬∀x208 (¬∀x1 ¬x208=z207+ x1'⇒(¬∀x1 ¬x21=z207+ x1*x208⇒¬x208=( y207'*y21)'))⇒(y207=( ( 0''*0'''+ 0''+ x201)*( 0''*0'''+ 0''+ x201)+ 0''*0'''+ 0''+ 0'+ z202)*( ( 0''*0'''+ 0''+ x201)*( 0''*0'''+ 0''+ x201)+ 0''*0'''+ 0''+ 0'+ z202)+ ( 0''*0'''+ 0''+ x201)*( 0''*0'''+ 0''+ x201)+ 0''*0'''+ 0''+ 0'+ 0'⇒((0'*0'''+ 0'=y204⇒( z206+ x203)*( z206+ x203)+ z206+ 0'=x197)⇒(¬∀x207 (¬∀x1 ¬x207=z206+ x1'⇒(¬∀x1 ¬x21=z206+ x1*x207⇒¬x207=( y206'*y21)'))⇒(y206=( ( 0''*0'''+ 0''+ x201)*( 0''*0'''+ 0''+ x201)+ 0''*0'''+ 0''+ 0'+ z202)*( ( 0''*0'''+ 0''+ x201)*( 0''*0'''+ 0''+ x201)+ 0''*0'''+ 0''+ 0'+ z202)+ ( 0''*0'''+ 0''+ x201)*( 0''*0'''+ 0''+ x201)+ 0''*0'''+ 0''+ 0'+ 0'⇒((0'*0'''+ 0'=y204⇒( z205+ y201)*( z205+ y201)+ z205+ 0'=x197)⇒(¬∀x206 (¬∀x1 ¬x206=z205+ x1'⇒(¬∀x1 ¬x20=z205+ x1*x206⇒¬x206=( y205'*y20)'))⇒(y205=( 0'*0'''+ 0'+ x201)*( 0'*0'''+ 0'+ x201)+ 0'*0'''+ 0'+ 0'⇒((0'=y204⇒( ( 0'*0'''+ 0')*0'''+ 0+ x200)*( ( 0'*0'''+ 0')*0'''+ 0+ x200)+ ( 0'*0'''+ 0')*0'''+ 0+ 0'=x197)⇒(x205=y204⇒(¬∀x1 ¬x205+ x1'=0''*0'''+ 0''⇒¬y196=z204*( 0''*0'''+ 0'')+ x205))))))))))))))⇒(( z202+ x203)*( z202+ x203)+ z202+ 0'=z203⇒(¬∀x204 (¬∀x1 ¬x204=z203+ x1'⇒(¬∀x1 ¬x23=z203+ x1*x204⇒¬x204=( y203'*y23)'))⇒(y203=y201⇒(( x201+ y201)*( x201+ y201)+ x201+ 0'=x202⇒(¬∀y202 (¬∀x1 ¬y202=x202+ x1'⇒(¬∀x1 ¬x23=x202+ x1*y202⇒¬y202=( z201'*y23)'))⇒(z201=x200⇒(¬∀x1 ¬z200+ x1'=0''*0'''+ 0''⇒(y196=y200*( 0''*0'''+ 0'')+ z200⇒(¬∀z199 (¬∀x1 ¬z199=y199+ x1'⇒(¬∀x1 ¬x22=y199+ x1*z199⇒¬z199=( x199'*y22)'))⇒(x199=y198⇒(¬∀x1 ¬z198+ x1'=0''⇒(y196=y198*0''+ z198⇒(¬∀x1 ¬x198+ x1'=0''⇒(y196=z197*0''+ x198⇒∀y197 (¬∀x1 ¬y197=x197+ x1'⇒(¬∀x1 ¬x23=x197+ x1*y197⇒¬y197=( z196'*y23)'))))))))))))))))))⇒(∀y293 ∀x293 (¬(y293=x293⇒∀x1 ¬y293+ x1'=z21)⇒¬∀y296 ∀x296 ∀y295 ∀x295 ∀z293 (( 0''*y296+ z294)*( 0''*y296+ z294)+ 0''*y296+ 0'=z293⇒(¬∀z296 (¬∀x1 ¬z296=y296+ x1'⇒(¬∀x1 ¬x19=y296+ x1*z296⇒¬z296=( x296'*y19)'))⇒(x296=y294⇒(( y294+ z294)*( y294+ z294)+ y294+ 0'=y295⇒(¬∀z295 (¬∀x1 ¬z295=y295+ x1'⇒(¬∀x1 ¬x18=y295+ x1*z295⇒¬z295=( x295'*y18)'))⇒(x295=x293⇒∀x294 (¬∀x1 ¬x294=z293+ x1'⇒(¬∀x1 ¬x22=z293+ x1*x294⇒¬x294=( y293'*y22)')))))))))⇒(∀z65 ∀y65 (¬(z65=y65⇒∀x1 ¬z65+ x1'=z18)⇒¬∀y69 ∀x69 ∀z68 ∀x68 ∀z67 ∀y67 ∀x67 ∀z66 ∀x66 (¬((y65=0⇒0''*0'''+ 0''=x66)⇒¬(¬y65=0⇒( 0'*0'''+ 0')*x68+ y69=x66))⇒(¬∀x1 ¬y69+ x1'=0'*0'''+ 0'⇒(z68=x69*( 0'*0'''+ 0')+ y69⇒(z68+ 0'=y65⇒(¬∀y68 (¬∀x1 ¬y68=x68+ x1'⇒(¬∀x1 ¬x19=x68+ x1*y68⇒¬y68=( z67'*y19)'))⇒(z67=x67⇒(¬∀x1 ¬y67+ x1'=0'*0'''+ 0'⇒(z66=x67*( 0'*0'''+ 0')+ y67⇒(z66+ 0'=y65⇒∀y66 (¬∀x1 ¬y66=x66+ x1'⇒(¬∀x1 ¬x19=x66+ x1*y66⇒¬y66=( z65'*y19)'))))))))))))⇒(∀z72 ∀y72 ∀x72 ∀z71 (¬(z72=( ( z71+ x72)*( z71+ x72)+ z71+ 0'+ y72)*( ( z71+ x72)*( z71+ x72)+ z71+ 0'+ y72)+ ( z71+ x72)*( z71+ x72)+ z71+ 0'+ 0'⇒∀x1 ¬z72+ x1'=z20)⇒¬∀z77 ∀y77 ∀z76 ∀y76 ∀z75 ∀y75 ∀x75 ∀y74 ∀x74 ∀x73 (z77=x73⇒(¬∀x78 (¬∀x1 ¬x78=z77+ x1'⇒(¬∀x1 ¬x20=z77+ x1*x78⇒¬x78=( y77'*y20)'))⇒(y77=( z71+ y72*z75+ z76)*( z71+ y72*z75+ z76)+ z71+ 0'⇒(¬∀x77 (¬∀x1 ¬x77=z76+ x1'⇒(¬∀x1 ¬x15=z76+ x1*x77⇒¬x77=( y76'*y15)'))⇒(y76=( x72+ z73)*( x72+ z73)+ x72+ 0'⇒(¬∀x76 (¬∀x1 ¬x76=z75+ x1'⇒(¬∀x1 ¬x14=z75+ x1*x76⇒¬x76=( y75'*y14)'))⇒(y75=( 0'+ z73)*( 0'+ z73)+ 0'+ 0'⇒(x75+ 0'=y74⇒(¬∀z74 (¬∀x1 ¬z74=y74+ x1'⇒(¬∀x1 ¬x13=y74+ x1*z74⇒¬z74=( x74'*y13)'))⇒(x74=x72⇒∀y73 (¬∀x1 ¬y73=x73+ x1'⇒(¬∀x1 ¬x21=x73+ x1*y73⇒¬y73=( z72'*y21)')))))))))))))⇒(∀y54 ∀x54 ∀z53 (¬(y54=( z53+ x54)*( z53+ x54)+ z53+ 0'⇒∀x1 ¬y54+ x1'=z14)⇒¬∀x58 ∀z57 ∀y57 ∀x57 ∀z56 ∀x56 ∀z55 ∀z54 (¬((z57=0⇒z53=z54)⇒¬(¬z57=0⇒x58=z54))⇒(x58+ y55=z53⇒(¬∀x1 ¬z57+ x1'=0''⇒(z56=y57*0''+ z57⇒(¬∀x1 ¬x57+ x1'=y55⇒(z53=z56*y55+ x57⇒(¬∀y56 (¬∀x1 ¬y56=x56+ x1'⇒(¬∀x1 ¬x14=x56+ x1*y56⇒¬y56=( z55'*y14)'))⇒(z55=( 0'+ x54)*( 0'+ x54)+ 0'+ 0'⇒∀x55 (¬∀x1 ¬x55=z54+ x1'⇒(¬∀x1 ¬x15=z54+ x1*x55⇒¬x55=( y54'*y15)')))))))))))⇒(∀y48 ∀x48 ∀z47 (¬(y48=( z47+ x48)*( z47+ x48)+ z47+ 0'⇒∀x1 ¬y48+ x1'=z13)⇒¬∀y50 ∀z49 ∀y49 ∀z48 (¬((x48=0⇒z47=z48)⇒¬(¬x48=0⇒0''*y50=z48))⇒(y50+ 0'=z49⇒(¬∀x50 (¬∀x1 ¬x50=z49+ x1'⇒(¬∀x1 ¬x14=z49+ x1*x50⇒¬x50=( y49'*y14)'))⇒(y49=( z47+ x48)*( z47+ x48)+ z47+ 0'⇒∀x49 (¬∀x1 ¬x49=z48+ x1'⇒(¬∀x1 ¬x14=z48+ x1*x49⇒¬x49=( y48'*y14)')))))))⇒(∀x51 ∀z50 (¬(x51=z50⇒∀x1 ¬x51+ x1'=z12)⇒¬∀x53 ∀z52 ∀y52 ∀x52 ∀y51 (¬((z50=0⇒0=y51)⇒¬(¬z50=0⇒0'+ x53=y51))⇒(¬∀y53 (¬∀x1 ¬y53=x53+ x1'⇒(¬∀x1 ¬x13=x53+ x1*y53⇒¬y53=( z52'*y13)'))⇒(z52=x52⇒(¬∀x1 ¬y52+ x1'=0''⇒(z50=x52*0''+ y52⇒∀z51 (¬∀x1 ¬z51=y51+ x1'⇒(¬∀x1 ¬x13=y51+ x1*z51⇒¬z51=( x51'*y13)'))))))))⇒(∀y70 ∀x70 ∀z69 (¬(y70=( z69+ x70)*( z69+ x70)+ z69+ 0'⇒∀x1 ¬y70+ x1'=z19)⇒¬∀y71 ∀z70 (¬((¬∀x1 ¬z69+ x1'=0'*0'''+ 0'⇒x70*( 0'*0'''+ 0')+ z69=z70)⇒¬(∀x1 ¬z69+ x1'=0'*0'''+ 0'⇒y71=z70))⇒(y71+ 0''*0'''+ 0''=x70*( 0''*0'''+ 0'')+ 0''*z69⇒∀x71 (¬∀x1 ¬x71=z70+ x1'⇒(¬∀x1 ¬x20=z70+ x1*x71⇒¬x71=( y70'*y20)')))))⇒(∀y63 ∀x63 (¬(y63=x63⇒∀x1 ¬y63+ x1'=z17)⇒¬∀z64 ∀y64 ∀z63 (z64=z63⇒(¬∀x65 (¬∀x1 ¬x65=z64+ x1'⇒(¬∀x1 ¬x39=z64+ x1*x65⇒¬x65=( y64'*y39)'))⇒(y64=( 0+ x63)*( 0+ x63)+ 0+ 0'⇒∀x64 (¬∀x1 ¬x64=z63+ x1'⇒(¬∀x1 ¬x18=z63+ x1*x64⇒¬x64=( y63'*y18)'))))))⇒(∀y287 ∀x287 (¬(y287=x287⇒∀x1 ¬y287+ x1'=z38)⇒¬∀z287 (¬∀y292 ∀x292 ∀z291 ∀y291 ∀x291 ∀z290 ∀y290 ∀x290 ∀z289 ∀y289 ∀x289 ((¬0'*0'''+ 0'=x289⇒y292=z287)⇒(¬∀z292 (¬∀x1 ¬z292=y292+ x1'⇒(¬∀x1 ¬x39=y292+ x1*z292⇒¬z292=( x292'*y39)'))⇒(x292=( y288*( 0'*0'''+ 0')+ x291+ 0'+ y291)*( y288*( 0'*0'''+ 0')+ x291+ 0'+ y291)+ y288*( 0'*0'''+ 0')+ x291+ 0'+ 0'⇒(¬∀x1 ¬z291+ x1'=0'*0'''+ 0'⇒(z288=y291*( 0'*0'''+ 0')+ z291⇒(¬∀x1 ¬x291+ x1'=0'*0'''+ 0'⇒(z288=z290*( 0'*0'''+ 0')+ x291⇒((0'*0'''+ 0'=x289⇒( y288+ x290)*( y288+ x290)+ y288+ 0'=z287)⇒(¬∀x1 ¬y290+ x1'=0'*0'''+ 0'⇒(z288=x290*( 0'*0'''+ 0')+ y290⇒(z289=x289⇒(¬∀x1 ¬z289+ x1'=0'*0'''+ 0'⇒¬z288=y289*( 0'*0'''+ 0')+ z289))))))))))))⇒(( y288+ z288)*( y288+ z288)+ y288+ 0'=x287⇒∀x288 (¬∀x1 ¬x288=z287+ x1'⇒(¬∀x1 ¬x39=z287+ x1*x288⇒¬x288=( y287'*y39)')))))⇒∀z (z=( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 0''*0'''+ 0'')*0'''+ 0)*0'''+ 0'')*0'''+ 0'')*0'''+ 0'')*0'''+ 0)*0'''+ 0)*0'''+ 0'')*0'''+ 0')*0'''+ 0'')*0'''+ 0'')*0'''+ 0')*0'''+ 0)*0'''+ 0')*0'''+ 0')*0'''+ 0'')*0'''+ 0')*0'''+ 0)*0'''+ 0')*0'''+ 0'')*0'''+ 0')*0'''+ 0'')*0'''+ 0)*0'''+ 0)*0'''+ 0)*0'''+ 0)*0'''+ 0)*0'''+ 0)*0'''+ 0'')*0'''+ 0'')*0'''+ 0')*0'''+ 0)*0'''+ 0)*0'''+ 0'')*0'''+ 0'')*0'''+ 0'')*0'''+ 0)*0'''+ 0'')*0'''+ 0)*0'''+ 0')*0'''+ 0)*0'''+ 0)*0'''+ 0'')*0'''+ 0)*0'''+ 0'')*0'''+ 0)*0'''+ 0'')*0'''+ 0')*0'''+ 0)*0'''+ 0'')*0'''+ 0)*0'''+ 0)*0'''+ 0'')*0'''+ 0')*0'''+ 0)*0'''+ 0)*0'''+ 0)*0'''+ 0'')*0'''+ 0)*0'''+ 0)*0'''+ 0')*0'''+ 0')*0'''+ 0'')*0'''+ 0)*0'''+ 0)*0'''+ 0')*0'''+ 0)*0'''+ 0')*0'''+ 0'')*0'''+ 0')*0'''+ 0'')*0'''+ 0)*0'''+ 0)*0'''+ 0'')*0'''+ 0')*0'''+ 0'')*0'''+ 0)*0'''+ 0)*0'''+ 0)*0'''+ 0'')*0'''+ 0'')*0'''+ 0'')*0'''+ 0'')*0'''+ 0'')*0'''+ 0)*0'''+ 0')*0'''+ 0)*0'''+ 0'')*0'''+ 0'')*0'''+ 0)*0'''+ 0)*0'''+ 0'')*0'''+ 0')*0'''+ 0)*0'''+ 0')*0'''+ 0'')*0'''+ 0)*0'''+ 0'')*0'''+ 0'')*0'''+ 0)*0'''+ 0')*0'''+ 0')*0'''+ 0')*0'''+ 0'')*0'''+ 0)*0'''+ 0')*0'''+ 0)*0'''+ 0')*0'''+ 0)*0'''+ 0'')*0'''+ 0)*0'''+ 0'')*0'''+ 0'')*0'''+ 0')*0'''+ 0)*0'''+ 0)*0'''+ 0'')*0'''+ 0)*0'''+ 0'')*0'''+ 0)*0'''+ 0'')*0'''+ 0)*0'''+ 0'')*0'''+ 0'')*0'''+ 0')*0'''+ 0)*0'''+ 0')*0'''+ 0'')*0'''+ 0)*0'''+ 0)*0'''+ 0'')*0'''+ 0')*0'''+ 0')*0'''+ 0)*0'''+ 0')*0'''+ 0'')*0'''+ 0')*0'''+ 0')*0'''+ 0'')*0'''+ 0')*0'''+ 0')*0'''+ 0)*0'''+ 0)*0'''+ 0'')*0'''+ 0')*0'''+ 0'')*0'''+ 0'')*0'''+ 0'')*0'''+ 0')*0'''+ 0)*0'''+ 0'')*0'''+ 0')*0'''+ 0)*0'''+ 0')*0'''+ 0)*0'''+ 0')*0'''+ 0)*0'''+ 0)*0'''+ 0'')*0'''+ 0')*0'''+ 0')*0'''+ 0'')*0'''+ 0'')*0'''+ 0)*0'''+ 0'')*0'''+ 0'')*0'''+ 0)*0'''+ 0'')*0'''+ 0'')*0'''+ 0'')*0'''+ 0)*0'''+ 0'')*0'''+ 0)*0'''+ 0'')*0'''+ 0'')*0'''+ 0')*0'''+ 0'')*0'''+ 0)*0'''+ 0')*0'''+ 0'')*0'''+ 0')*0'''+ 0)*0'''+ 0')*0'''+ 0')*0'''+ 0)*0'''+ 0'')*0'''+ 0'')*0'''+ 0'')*0'''+ 0')*0'''+ 0'')*0'''+ 0')*0'''+ 0)*0'''+ 0')*0'''+ 0'')*0'''+ 0)*0'''+ 0)*0'''+ 0)*0'''+ 0')*0'''+ 0'')*0'''+ 0')*0'''+ 0)*0'''+ 0')*0'''+ 0')*0'''+ 0)*0'''+ 0'')*0'''+ 0'')*0'''+ 0)*0'''+ 0)*0'''+ 0')*0'''+ 0)*0'''+ 0'')*0'''+ 0)*0'''+ 0''⇒∀z (¬∀x317 (¬∀x1 ¬x317=z+ x1'⇒(¬∀x1 ¬x14=z+ x1*x317⇒¬x317=( x'*y14)'))⇒¬∀z ∀z316 (¬∀x1 ¬z316=z+ x1'⇒(¬∀x1 ¬x34=z+ x1*z316⇒¬z316=( x'*y34)'))))))))))))))))))))))))))))))))))))

Gödel's incompleteness theorem project

Tachyos Home Page | Chronon Critical Points | Recent Science Book Reviews