What does a Godel sentence actually look like?

My understanding is that Godel's first theorem says that there is a sentence that is in a sense true in a formal system F but cannot be derived in that system.

I then hear that Godel actually goes on to construct such a sentence.

My question is, what would this even look like?

For example, in Peano Arithmetic would it be something like:

5 + 3 * 15 ... = ...? Is it long? Is it short? Could it be written on a piece of paper?

If not what is wrong with my thinking?

Thanks

Here's an explicit example, due to Hagen von Eitzen (I've made this answer community wiki so I don't get rep bonus for someone else's hard work):

¬∃b:∃c:∃d:〈∃e:∃f:∃g:〈a=((((((e+ f)+ g)· ((e+ f)+ g))· ((e+ f)+ g))+ ((e+ f)· (e+ f)))+ e) ∧ ∃h:∃i:〈〈∃j:h=(j· Si) ∧ 〈∃j:h=(d+ (j· S(i· Sg))) ∧ ∃j:(d+ j)=(i· Sg)〉〉 ∧ ∀j:〈∃k:S(j+ k)=g ⇒ ∀k:∀l:〈〈〈∃m:h=(k+ (m· S(i· Sj))) ∧ ∃m:(k+ m)=(i· Sj)〉 ∧ 〈∃m:e=(l+ (m· S(f· Sj))) ∧ ∃m:(l+ m)=(f· Sj)〉〉 ⇒ 〈〈¬l=SSSSSSSSSS0 ⇒ 〈〈∃m:h=S(k+ (m· S(i· SSj))) ∧ ∃m:S(k+ m)=(i· SSj)〉 ∧ 〈∃m:b=(l+ (m· S(c· Sj))) ∧ ∃m:(l+ m)=(c· Sj)〉〉〉 ∧ 〈l=SSSSSSSSSS0 ⇒ 〈〈〈∃m:h=S((a+ k)+ (m· S(i· SSj))) ∧ ∃m:S((a+ k)+ m)=(i· SSj)〉 ∧ 〈∃m:b=SSSSSSSSS(m· S(c· S(a+ k))) ∧ ∃m:SSSSSSSSSm=(c· S(a+ k))〉〉 ∧ ∀m:〈∃n:S(m+ n)=a ⇒ 〈∃n:b=SSSSSSSS(n· S(c· S(m+ k))) ∧ ∃n:SSSSSSSSn=(c· S(m+ k))〉〉〉〉〉〉〉〉〉 ∧ ∃e:∃f:∃g:∃h:∃i:〈〈〈〈〈∃j:i=(j· Sf) ∧ ∃j:i=(j· S(f· Sg))〉 ∧ ∀j:∀k:∀l:〈〈〈∃m:S(j+ m)=g ∧ 〈∃m:i=(k+ (m· S(f· Sj))) ∧ ∃m:(k+ m)=(f· Sj)〉〉 ∧ 〈∃m:i=(l+ (m· S(f· SSj))) ∧ ∃m:(l+ m)=(f· SSj)〉〉 ⇒ 〈k=l ∨ 〈∃m:e=(m· S(f· Sj)) ∧ 〈k=Sl ∨ l=Sk〉〉〉〉〉 ∧ ∀j:〈∃k:S(j+ k)=g ⇒ ∀k:∀l:∀m:∀n:〈〈〈〈〈∃o:e=(k+ (o· S(f· Sj))) ∧ ∃o:(k+ o)=(f· Sj)〉 ∧ 〈∃o:h=(l+ (o· S(f· Sj))) ∧ ∃o:(l+ o)=(f· Sj)〉〉 ∧ 〈∃o:h=(m+ (o· S(f· SSj))) ∧ ∃o:(m+ o)=(f· SSj)〉〉 ∧ 〈∃o:h=(n+ (o· S(f· SS(m+ j)))) ∧ ∃o:(n+ o)=(f· SS(m+ j))〉〉 ⇒ 〈〈〈〈〈〈∃o:((j+ l)+ o)=g ∧ 〈∃o:SSSSSSSSSo=k ⇒ l=S0〉〉 ∧ 〈〈〈k=0 ∨ k=SSSSSSS0〉 ∨ k=SSSSSSSS0〉 ⇒ l=Sm〉〉 ∧ 〈〈〈〈〈〈k=S0 ∨ k=SS0〉 ∨ k=SSS0〉 ∨ k=SSSS0〉 ∨ k=SSSSS0〉 ∨ k=SSSSSS0〉 ⇒ 〈l=S(m+ n) ∧ ∀o:〈〈∃p:〈∃q:S(p+ q)=m ∧ 〈∃q:e=(o+ (q· S(f· SS(j+ p)))) ∧ ∃q:(o+ q)=(f· SS(j+ p))〉〉 ∧ ∃p:〈∃q:S(p+ q)=n ∧ 〈∃q:e=(o+ (q· S(f· SS((m+ j)+ p)))) ∧ ∃q:(o+ q)=(f· SS((m+ j)+ p))〉〉〉 ⇒ 〈〈∀p:¬〈〈∃q:S(p+ q)=m ∧ 〈∃q:e=SSSSSS(q· S(f· SS(j+ p))) ∧ ∃q:SSSSSSq=(f· SS(j+ p))〉〉 ∧ 〈∃q:e=(o+ (q· S(f· SSS(j+ p)))) ∧ ∃q:(o+ q)=(f· SSS(j+ p))〉〉 ∨ ∀p:¬〈〈∃q:S(p+ q)=n ∧ 〈∃q:e=SSSSSS(q· S(f· SS((m+ j)+ p))) ∧ ∃q:SSSSSSq=(f· SS((m+ j)+ p))〉〉 ∧ 〈∃q:e=(o+ (q· S(f· SSS((m+ j)+ p)))) ∧ ∃q:(o+ q)=(f· SSS((m+ j)+ p))〉〉〉 ⇒ ∀p:¬〈〈∃q:S(p+ q)=(m+ n) ∧ 〈∃q:e=SSSSSS(q· S(f· SS(j+ p))) ∧ ∃q:SSSSSSq=(f· SS(j+ p))〉〉 ∧ 〈∃q:e=(o+ (q· S(f· SSS(j+ p)))) ∧ ∃q:(o+ q)=(f· SSS(j+ p))〉〉〉〉〉〉〉 ∧ ∀o:〈〈∃p:e=(o+ (p· S(f· SSj))) ∧ ∃p:(o+ p)=(f· SSj)〉 ⇒ 〈〈〈〈〈〈k=0 ∨ k=S0〉 ∨ k=SS0〉 ∨ k=SSSSSSS0〉 ⇒ 〈〈〈〈o=S0 ∨ o=SS0〉 ∨ o=SSS0〉 ∨ o=SSSSSS0〉 ∨ o=SSSSSSS0〉〉 ∧ 〈〈〈〈k=SSS0 ∨ k=SSSS0〉 ∨ k=SSSSS0〉 ∨ k=SSSSSSSS0〉 ⇒ 〈〈o=SSSS0 ∨ o=SSSSS0〉 ∨ ∃p:SSSSSSSSp=o〉〉〉 ∧ 〈k=SSSSSS0 ⇒ ∃p:SSSSSSSSSSp=o〉〉〉〉 ∧ ∀o:〈〈∃p:e=(o+ (p· S(f· SS(m+ j)))) ∧ ∃p:(o+ p)=(f· SS(m+ j))〉 ⇒ 〈〈〈k=0 ⇒ k=o〉 ∧ 〈〈〈k=S0 ∨ k=SS0〉 ∨ k=SSSSSS0〉 ⇒ 〈〈〈〈o=S0 ∨ o=SS0〉 ∨ o=SSS0〉 ∨ o=SSSSSS0〉 ∨ o=SSSSSSS0〉〉〉 ∧ 〈〈〈k=SSS0 ∨ k=SSSS0〉 ∨ k=SSSSS0〉 ⇒ 〈〈o=SSSS0 ∨ o=SSSSS0〉 ∨ ∃p:SSSSSSSSp=o〉〉〉〉〉 ∧ 〈j=0 ⇒ k=0〉〉〉〉〉 ∧ ∃j:〈〈〈g=S(j+ d) ∧ ∃k:e=(k· S(f· Sj))〉 ∧ ∀k:¬〈〈∃l:S(k+ l)=d ∧ 〈∃l:b=SSSSSS(l· S(c· Sk)) ∧ ∃l:SSSSSSl=(c· Sk)〉〉 ∧ ∃l:b=(l· S(c· SSk))〉〉 ∧ ∀k:∀l:〈〈∃m:S(k+ m)=d ∧ 〈∃m:b=(l+ (m· S(c· Sk))) ∧ ∃m:(l+ m)=(c· Sk)〉〉 ⇒ 〈∃m:e=(l+ (m· S(f· SS(j+ k)))) ∧ ∃m:(l+ m)=(f· SS(j+ k))〉〉〉〉 ∧ ∀j:∀k:〈〈∃l:e=(l· S(f· Sj)) ∧ 〈∃l:h=(k+ (l· S(f· SSj))) ∧ ∃l:(k+ l)=(f· SSj)〉〉 ⇒ 〈〈〈〈∃l:e=SSSSSS(l· S(f· SSj)) ∧ ∃l:SSSSSSl=(f· SSj)〉 ∧ 〈∃l:e=SSSSSSSSSS(l· S(f· SSSj)) ∧ ∃l:SSSSSSSSSSl=(f· SSSj)〉〉 ∧ 〈〈〈〈〈〈∃l:e=SSSSSSS(l· S(f· SSSSj)) ∧ ∃l:e=SSS(l· S(f· SSSSSj))〉 ∧ ∃l:e=SSSSSSSS(l· S(f· SSSSSSj))〉 ∧ ∃l:e=SSSSSSSSSS(l· S(f· SSSSSSSj))〉 ∧ ∃l:e=SSSSSSSSS(l· S(f· SSSSSSSSj))〉 ∨ 〈〈〈∃l:e=SSS(l· S(f· SSSSj)) ∧ ∃l:e=SSSSSSSSSS(l· S(f· SSSSSSj))〉 ∧ ∃l:e=SSSSSSSSS(l· S(f· SSSSSSSj))〉 ∧ 〈〈∃l:e=SSSS(l· S(f· SSSSSj)) ∧ ∃l:e=SSSSSSSSSS(l· S(f· SSSSSSSSj))〉 ∨ 〈∃l:e=SSSSS(l· S(f· SSSSSj)) ∧ ∃l:e=SSSSSSSSS(l· S(f· SSSSSSSSj))〉〉〉〉 ∨ 〈〈〈〈〈〈〈〈∃l:e=SSSSSS(l· S(f· SSSSj)) ∧ ∃l:e=SSSSSSSSSSS(l· S(f· SSSSSj))〉 ∧ ∃l:e=SSS(l· S(f· SSSSSSj))〉 ∧ ∃l:e=SSSSSSSSSS(l· S(f· SSSSSSSSj))〉 ∧ ∃l:e=SSSSSSSS(l· S(f· SSSSSSSSSj))〉 ∧ ∃l:e=SSSSSSSSSSS(l· S(f· SSSSSSSSSSj))〉 ∧ ∃l:e=SSSSSSSSSS(l· S(f· SSSSSSSSSSSSSj))〉 ∧ ∃l:e=SSSSSSSSSSS(l· S(f· SSSSSSSSSSSSSSj))〉 ∧ 〈〈〈∃l:e=SSSS(l· S(f· SSSSSSSj)) ∧ ∃l:e=SSSSSSSS(l· S(f· SSSSSSSSSSSj))〉 ∧ ∃l:e=SSSS(l· S(f· SSSSSSSSSSSSj))〉 ∨ 〈〈〈∃l:e=SSSSS(l· S(f· SSSSSSSj)) ∧ ∃l:e=SSSS(l· S(f· SSSSSSSSSSSj))〉 ∧ 〈∃l:e=SSSSS(l· S(f· SSSSSSSSSSSSj)) ∧ ∃l:SSSSSl=(f· SSSSSSSSSSSSj)〉〉 ∧ ∃l:e=SSSSSSSSSS(l· S(f· SSSSSSSSSSSSSSSj))〉〉〉〉〉 ∨ ∃l:∃m:〈〈〈〈∃n:S(l+ n)=j ∧ ∃n:e=(n· S(f· Sl))〉 ∧ 〈∃n:h=(m+ (n· S(f· SSl))) ∧ ∃n:(m+ n)=(f· SSl)〉〉 ∧ ∀n:∀o:∀p:〈〈〈〈∃q:i=(n+ (q· S(f· SSl))) ∧ ∃q:(n+ q)=(f· SSl)〉 ∧ ∃q:((l+ o)+ q)=j〉 ∧ 〈∃q:i=(p+ (q· S(f· SS(l+ o)))) ∧ ∃q:(p+ q)=(f· SS(l+ o))〉〉 ⇒ ∃q:(p+ q)=n〉〉 ∧ 〈〈〈〈〈〈〈〈〈〈〈∀n:∀o:〈〈∃p:S(n+ p)=m ∧ 〈∃p:e=(o+ (p· S(f· SS(n+ j)))) ∧ ∃p:(o+ p)=(f· SS(n+ j))〉〉 ⇒ ∃p:e=(o+ (p· S(f· SS(n+ l))))〉 ∨ 〈〈〈∃n:e=SSS(n· S(f· SSj)) ∧ ∃n:SSSn=(f· SSj)〉 ∧ k=m〉 ∧ ∃n:∃o:〈〈S(n+ o)=k ∧ ∀p:∀q:〈〈∃r:S(p+ r)=o ∧ 〈∃r:e=(q+ (r· S(f· SSS(p+ j)))) ∧ ∃r:(q+ r)=(f· SSS(p+ j))〉〉 ⇒ ∃r:e=(q+ (r· S(f· SSS(p+ (l+ n)))))〉〉 ∧ ∀p:∀q:〈〈∃r:S(p+ r)=n ∧ 〈∃r:e=(q+ (r· S(f· SSS(p+ (j+ o))))) ∧ ∃r:(q+ r)=(f· SSS(p+ (j+ o)))〉〉 ⇒ ∃r:e=(q+ (r· S(f· SSS(p+ l))))〉〉〉〉 ∨ 〈〈〈∃n:e=SSSSSSS(n· S(f· SSj)) ∧ ∃n:SSSSSSSn=(f· SSj)〉 ∧ k=SSm〉 ∧ ∀n:∀o:〈〈∃p:S(n+ p)=m ∧ 〈∃p:e=(o+ (p· S(f· SSSS(n+ j)))) ∧ ∃p:(o+ p)=(f· SSSS(n+ j))〉〉 ⇒ 〈∃p:e=(o+ (p· S(f· SS(n+ l)))) ∧ ∃p:(o+ p)=(f· SS(n+ l))〉〉〉〉 ∨ 〈〈〈∃n:e=SSSSSSS(n· S(f· SSl)) ∧ ∃n:SSSSSSSn=(f· SSl)〉 ∧ m=SSk〉 ∧ ∀n:∀o:〈〈∃p:S(n+ p)=k ∧ 〈∃p:e=(o+ (p· S(f· SSSS(n+ l)))) ∧ ∃p:(o+ p)=(f· SSSS(n+ l))〉〉 ⇒ 〈∃p:e=(o+ (p· S(f· SS(n+ j)))) ∧ ∃p:(o+ p)=(f· SS(n+ j))〉〉〉〉 ∨ ∃n:∃o:〈〈〈〈〈〈∃p:h=(n+ (p· S(f· SSSl))) ∧ ∃p:(n+ p)=(f· SSSl)〉 ∧ S(n+ o)=m〉 ∧ 〈∃p:e=SSSSSSSS(p· S(f· SSSj)) ∧ ∃p:SSSSSSSSp=(f· SSSj)〉〉 ∧ 〈∃p:e=SSSSSSSS(p· S(f· SSSS(j+ n))) ∧ ∃p:SSSSSSSSp=(f· SSSS(j+ n))〉〉 ∧ ∀p:∀q:〈〈∃r:S(p+ r)=n ∧ 〈∃r:e=(q+ (r· S(f· SSSS(p+ j)))) ∧ ∃r:(q+ r)=(f· SSSS(p+ j))〉〉 ⇒ 〈∃r:e=(q+ (r· S(f· SSS(p+ l)))) ∧ ∃r:(q+ r)=(f· SSS(p+ l))〉〉〉 ∧ ∀p:∀q:〈〈∃r:S(p+ r)=o ∧ 〈∃r:e=(q+ (r· S(f· SSSSS(p+ (j+ n))))) ∧ ∃r:(q+ r)=(f· SSSSS(p+ (j+ n)))〉〉 ⇒ 〈∃r:e=(q+ (r· S(f· SSS(p+ (l+ n))))) ∧ ∃r:(q+ r)=(f· SSS(p+ (l+ n)))〉〉〉〉 ∨ ∃n:∃o:〈〈〈〈〈〈∃p:h=(n+ (p· S(f· SSSj))) ∧ ∃p:(n+ p)=(f· SSSj)〉 ∧ S(n+ o)=k〉 ∧ 〈∃p:e=SSSSSSSS(p· S(f· SSSl)) ∧ ∃p:SSSSSSSSp=(f· SSSl)〉〉 ∧ 〈∃p:e=SSSSSSSS(p· S(f· SSSS(l+ n))) ∧ ∃p:SSSSSSSSp=(f· SSSS(l+ n))〉〉 ∧ ∀p:∀q:〈〈∃r:S(p+ r)=n ∧ 〈∃r:e=(q+ (r· S(f· SSSS(p+ l)))) ∧ ∃r:(q+ r)=(f· SSSS(p+ l))〉〉 ⇒ 〈∃r:e=(q+ (r· S(f· SSS(p+ j)))) ∧ ∃r:(q+ r)=(f· SSS(p+ j))〉〉〉 ∧ ∀p:∀q:〈〈∃r:S(p+ r)=o ∧ 〈∃r:e=(q+ (r· S(f· SSSSS(p+ (l+ n))))) ∧ ∃r:(q+ r)=(f· SSSSS(p+ (l+ n)))〉〉 ⇒ 〈∃r:e=(q+ (r· S(f· SSS(p+ (j+ n))))) ∧ ∃r:(q+ r)=(f· SSS(p+ (j+ n)))〉〉〉〉 ∨ 〈〈∃n:e=SS(n· S(f· SSl)) ∧ ∃n:SSn=(f· SSl)〉 ∧ ∀n:∀o:〈〈∃p:S(n+ p)=k ∧ 〈∃p:e=(o+ (p· S(f· SS(n+ j)))) ∧ ∃p:(o+ p)=(f· SS(n+ j))〉〉 ⇒ ∃p:e=(o+ (p· S(f· SSS(n+ l))))〉〉〉 ∨ ∃n:〈〈〈∃o:h=(n+ (o· S(f· SSSl))) ∧ ∃o:(n+ o)=(f· SSSl)〉 ∧ 〈∃o:e=SS(o· S(f· SSl)) ∧ ∃o:SSo=(f· SSl)〉〉 ∧ ∀o:∀p:〈〈∃q:S(o+ q)=k ∧ 〈∃q:e=(p+ (q· S(f· SS(o+ j)))) ∧ ∃q:(p+ q)=(f· SS(o+ j))〉〉 ⇒ ∃q:e=(p+ (q· S(f· SSS(o+ (l+ n)))))〉〉〉 ∨ 〈k=SSm ∧ ∃n:∃o:〈〈〈〈S(n+ o)=m ∧ 〈∃p:e=S(p· S(f· SSj)) ∧ ∃p:Sp=(f· SSj)〉〉 ∧ 〈∃p:e=S(p· S(f· SSl)) ∧ ∃p:Sp=(f· SSl)〉〉 ∧ ∀p:∀q:〈〈∃r:S(p+ r)=o ∧ 〈∃r:e=(q+ (r· S(f· SSSSS(p+ (j+ n))))) ∧ ∃r:(q+ r)=(f· SSSSS(p+ (j+ n)))〉〉 ⇒ ∃r:e=(q+ (r· S(f· SSS(p+ l))))〉〉 ∧ ∀p:∀q:〈〈∃r:S(p+ r)=n ∧ 〈∃r:e=(q+ (r· S(f· SSSS(p+ j)))) ∧ ∃r:(q+ r)=(f· SSSS(p+ j))〉〉 ⇒ ∃r:e=(q+ (r· S(f· SSS(p+ (l+ o)))))〉〉〉〉 ∨ ∃n:∃o:∃p:∃q:〈〈〈m=SSq ∧ 〈∃r:e=SSSSSS(r· S(f· SSl)) ∧ ∃r:SSSSSSr=(f· SSl)〉〉 ∧ 〈∃r:e=(n+ (r· S(f· SSSl))) ∧ ∃r:(n+ r)=(f· SSSl)〉〉 ∧ 〈∀r:〈∃s:〈∃t:S(s+ t)=p ∧ 〈∃t:e=(r+ (t· S(f· S(o+ s)))) ∧ ∃t:(r+ t)=(f· S(o+ s))〉〉 ⇒ ∀s:¬〈〈∃t:S(s+ t)=q ∧ 〈∃t:e=SSSSSS(t· S(f· SSSS(l+ s))) ∧ ∃t:SSSSSSt=(f· SSSS(l+ s))〉〉 ∧ 〈∃t:e=(r+ (t· S(f· SSSSS(l+ s)))) ∧ ∃t:(r+ t)=(f· SSSSS(l+ s))〉〉〉 ∧ ∃r:∃s:〈〈∃t:r=(t· Ss) ∧ 〈∃t:r=(k+ (t· S(s· Sq))) ∧ ∃t:(k+ t)=(s· Sq)〉〉 ∧ ∀t:∀u:∀v:∀w:〈〈〈〈∃x:S(t+ x)=q ∧ 〈∃x:r=(u+ (x· S(s· St))) ∧ ∃x:(u+ x)=(s· St)〉〉 ∧ 〈∃x:r=(v+ (x· S(s· SSt))) ∧ ∃x:(v+ x)=(s· SSt)〉〉 ∧ 〈∃x:e=(w+ (x· S(f· SSSS(l+ t)))) ∧ ∃x:(w+ x)=(f· SSSS(l+ t))〉〉 ⇒ 〈〈¬w=n ⇒ 〈〈∃x:e=(w+ (x· S(f· SS(j+ u)))) ∧ ∃x:(w+ x)=(f· SS(j+ u))〉 ∧ v=Su〉〉 ∧ 〈w=n ⇒ 〈∀x:∀y:〈〈∃z:S(x+ z)=p ∧ 〈∃z:e=(y+ (z· S(f· S(o+ x)))) ∧ ∃z:(y+ z)=(f· S(o+ x))〉〉 ⇒ 〈∃z:e=(y+ (z· S(f· SS((x+ u)+ j)))) ∧ ∃z:(y+ z)=(f· SS((x+ u)+ j))〉〉 ∧ v=(p+ u)〉〉〉〉〉〉〉〉 ∨ ∃n:〈∀o:〈〈〈∃p:S(o+ p)=j ∧ ∃p:e=(p· S(f· So))〉 ∧ ∀p:∀q:∀r:〈〈〈〈∃s:i=(q+ (s· S(f· So))) ∧ ∃s:(q+ s)=(f· So)〉 ∧ 〈∃s:i=(r+ (s· S(f· SS(p+ o)))) ∧ ∃s:(r+ s)=(f· SS(p+ o))〉〉 ∧ ∃s:S((o+ p)+ s)=j〉 ⇒ ∃s:S(q+ s)=r〉〉 ⇒ ∀p:¬〈〈〈∃q:h=(p+ (q· S(f· So))) ∧ ∃q:(p+ q)=(f· So)〉 ∧ ∃q:〈∃r:S(q+ r)=p ∧ 〈∃r:e=(n+ (r· S(f· S(o+ q)))) ∧ ∃r:(n+ r)=(f· S(o+ q))〉〉〉 ∧ ∀q:¬〈〈∃r:S(q+ r)=p ∧ 〈∃r:e=SSSSSS(r· S(f· S(o+ q))) ∧ ∃r:SSSSSSr=(f· S(o+ q))〉〉 ∧ 〈∃r:e=(n+ (r· S(f· SS(o+ q)))) ∧ ∃r:(n+ r)=(f· SS(o+ q))〉〉〉〉 ∧ 〈〈〈∃o:e=SSSSSS(o· S(f· SSj)) ∧ ∃o:SSSSSSo=(f· SSj)〉 ∧ 〈∃o:e=(n+ (o· S(f· SSSj))) ∧ ∃o:(n+ o)=(f· SSSj)〉〉 ∧ ∀o:∀p:〈〈∃q:S(o+ q)=m ∧ 〈∃q:e=(p+ (q· S(f· SSSS(o+ j)))) ∧ ∃q:(p+ q)=(f· SSSS(o+ j))〉〉 ⇒ 〈∃q:e=(p+ (q· S(f· SS(o+ l)))) ∧ ∃q:(p+ q)=(f· SS(o+ l))〉〉〉〉〉 ∨ ∃n:∃o:〈〈〈〈∃p:S(n+ p)=j ∧ ∃p:e=(p· S(f· Sn))〉 ∧ 〈∃p:h=(o+ (p· S(f· SSn))) ∧ ∃p:(o+ p)=(f· SSn)〉〉 ∧ ∀p:∀q:∀r:〈〈〈〈∃s:i=(p+ (s· S(f· SSn))) ∧ ∃s:(p+ s)=(f· SSn)〉 ∧ ∃s:((n+ q)+ s)=j〉 ∧ 〈∃s:i=(r+ (s· S(f· SS(n+ q)))) ∧ ∃s:(r+ s)=(f· SS(n+ q))〉〉 ⇒ ∃s:(r+ s)=p〉〉 ∧ 〈〈〈〈〈〈〈∃p:e=SS(p· S(f· SSj)) ∧ ∃p:SSp=(f· SSj)〉 ∧ ∀p:∀q:〈〈∃r:S(p+ r)=m ∧ 〈∃r:e=(q+ (r· S(f· SSS(p+ j)))) ∧ ∃r:(q+ r)=(f· SSS(p+ j))〉〉 ⇒ ∃r:e=(q+ (r· S(f· SS(p+ l))))〉〉 ∧ ∀p:∀q:〈〈∃r:S(p+ r)=o ∧ 〈∃r:e=(q+ (r· S(f· SSS(p+ (j+ m))))) ∧ ∃r:(q+ r)=(f· SSS(p+ (j+ m)))〉〉 ⇒ ∃r:e=(q+ (r· S(f· SS(p+ n))))〉〉 ∨ 〈〈〈∃p:e=S(p· S(f· SSl)) ∧ ∃p:Sp=(f· SSl)〉 ∧ ∀p:∀q:〈〈∃r:S(p+ r)=o ∧ 〈∃r:e=(q+ (r· S(f· SSS(p+ l)))) ∧ ∃r:(q+ r)=(f· SSS(p+ l))〉〉 ⇒ 〈∃r:e=(q+ (r· S(f· SS(p+ n)))) ∧ ∃r:(q+ r)=(f· SS(p+ n))〉〉〉 ∧ ∀p:∀q:〈〈∃r:S(p+ r)=k ∧ 〈∃r:e=(q+ (r· S(f· SS(p+ j)))) ∧ ∃r:(q+ r)=(f· SS(p+ j))〉〉 ⇒ 〈∃r:e=(q+ (r· S(f· SSS(p+ (l+ o))))) ∧ ∃r:(q+ r)=(f· SSS(p+ (l+ o)))〉〉〉〉 ∨ 〈〈∃p:e=SSS(p· S(f· SSj)) ∧ ∃p:SSSp=(f· SSj)〉 ∧ ∃p:∃q:∃r:〈〈〈〈〈S(p+ q)=k ∧ S(p+ r)=m〉 ∧ S(r+ q)=o〉 ∧ ∀s:∀t:〈〈∃u:S(s+ u)=p ∧ 〈∃u:e=(t+ (u· S(f· SSS(s+ j)))) ∧ ∃u:(t+ u)=(f· SSS(s+ j))〉〉 ⇒ ∃u:e=(t+ (u· S(f· SSS(s+ l))))〉〉 ∧ ∀s:∀t:〈〈∃u:S(s+ u)=r ∧ 〈∃u:e=(t+ (u· S(f· SSS(s+ n)))) ∧ ∃u:(t+ u)=(f· SSS(s+ n))〉〉 ⇒ 〈∃u:e=(t+ (u· S(f· SSS(s+ (l+ p))))) ∧ ∃u:(t+ u)=(f· SSS(s+ (l+ p)))〉〉〉 ∧ ∀s:∀t:〈〈∃u:S(s+ u)=q ∧ 〈∃u:e=(t+ (u· S(f· SSS(s+ (j+ p))))) ∧ ∃u:(t+ u)=(f· SSS(s+ (j+ p)))〉〉 ⇒ ∃u:e=(t+ (u· S(f· SSS(s+ (n+ r)))))〉〉〉〉 ∨ ∃p:〈〈〈〈〈〈〈〈∃q:e=SSSSSS(q· S(f· SSj)) ∧ ∃q:SSSSSSq=(f· SSj)〉 ∧ 〈∃q:e=(p+ (q· S(f· SSSj))) ∧ ∃q:(p+ q)=(f· SSSj)〉〉 ∧ 〈∃q:e=SSSSSS(q· S(f· SSn)) ∧ ∃q:SSSSSSq=(f· SSn)〉〉 ∧ 〈∃q:e=(p+ (q· S(f· SSSn))) ∧ ∃q:(p+ q)=(f· SSSn)〉〉 ∧ 〈∃q:e=S(q· S(f· SSSSn)) ∧ ∃q:Sq=(f· SSSSn)〉〉 ∧ ∀q:∀r:〈〈∃s:S(q+ s)=m ∧ 〈∃s:e=(r+ (s· S(f· SSSS(q+ j)))) ∧ ∃s:(r+ s)=(f· SSSS(q+ j))〉〉 ⇒ 〈∃s:e=(r+ (s· S(f· SSSSS(q+ n)))) ∧ ∃s:(r+ s)=(f· SSSSS(q+ n))〉〉〉 ∧ ∀q:∀r:∀s:〈〈〈∃t:S(q+ t)=m ∧ 〈∃t:e=(r+ (t· S(f· SS(l+ q)))) ∧ ∃t:(r+ t)=(f· SS(l+ q))〉〉 ∧ 〈∃t:e=(s+ (t· S(f· SSSS(j+ q)))) ∧ ∃t:(s+ t)=(f· SSSS(j+ q))〉〉 ⇒ 〈〈s=p ⇒ r=SSSSSSSSS0〉 ∧ 〈¬s=p ⇒ r=s〉〉〉〉 ∧ ∃q:∃r:〈〈∃s:q=SSSS((m+ l)+ (s· S(r· SSSSj))) ∧ ∃s:SSSS((m+ l)+ s)=(r· SSSSj)〉 ∧ ∀s:∀t:∀u:∀v:∀w:〈〈〈〈〈∃x:S(s+ x)=m ∧ 〈∃x:q=(t+ (x· S(r· SSSS(j+ s)))) ∧ ∃x:(t+ x)=(r· SSSS(j+ s))〉〉 ∧ 〈∃x:q=(u+ (x· S(r· SSSSS(j+ s)))) ∧ ∃x:(u+ x)=(r· SSSSS(j+ s))〉〉 ∧ 〈∃x:e=(v+ (x· S(f· SSSS(j+ s)))) ∧ ∃x:(v+ x)=(f· SSSS(j+ s))〉〉 ∧ 〈∃x:e=(w+ (x· S(f· St))) ∧ ∃x:(w+ x)=(f· St)〉〉 ⇒ 〈〈v=p ⇒ 〈〈u=SSt ∧ 〈∃x:e=(p+ (x· S(f· SSt))) ∧ ∃x:(p+ x)=(f· SSt)〉〉 ∧ w=SSSSSSSS0〉〉 ∧ 〈¬v=p ⇒ 〈u=St ∧ w=v〉〉〉〉〉〉〉 ∨ 〈∃p:〈〈〈S(n+ o)=j ∧ 〈∃q:i=(p+ (q· S(f· Sl))) ∧ ∃q:(p+ q)=(f· Sl)〉〉 ∧ 〈∃q:i=(p+ (q· S(f· SSj))) ∧ ∃q:(p+ q)=(f· SSj)〉〉 ∧ ∀q:∀r:〈〈∃s:S((l+ q)+ s)=j ∧ 〈∃s:i=(r+ (s· S(f· SS(l+ q)))) ∧ ∃s:(r+ s)=(f· SS(l+ q))〉〉 ⇒ ∃s:S(p+ s)=r〉〉 ∧ 〈〈〈∃p:e=S(p· S(f· SSj)) ∧ ∃p:Sp=(f· SSj)〉 ∧ ∀p:∀q:〈〈∃r:S(p+ r)=m ∧ 〈∃r:e=(q+ (r· S(f· SSS(p+ j)))) ∧ ∃r:(q+ r)=(f· SSS(p+ j))〉〉 ⇒ 〈∃r:e=(q+ (r· S(f· SS(p+ l)))) ∧ ∃r:(q+ r)=(f· SS(p+ l))〉〉〉 ∧ ∀p:∀q:〈〈∃r:S(p+ r)=o ∧ 〈∃r:e=(q+ (r· S(f· SS(p+ n)))) ∧ ∃r:(q+ r)=(f· SS(p+ n))〉〉 ⇒ 〈∃r:e=(q+ (r· S(f· SSS(p+ (j+ m))))) ∧ ∃r:(q+ r)=(f· SSS(p+ (j+ m)))〉〉〉〉〉〉〉〉〉〉〉〉