Length of proof is 98. Level of proof is 28.
---------------- PROOF ----------------
3 [] -P(i(i(i(p,n(i(i(n(q),n(r)),n(r)))),n(i(i(n(q),n(r)),n(r)))),n(i(i(n(i(i(p,q),q)),n(i(i(p,r),r))),n(i(i(p,r),r)))))) # label("AK1").
5 [] -P(i(x,y))| -P(x)|P(y).
6 [] P(i(x,i(y,x))) # label(MV_1).
7 [] P(i(i(x,y),i(i(y,z),i(x,z)))) # label(MV_2).
8 [] P(i(i(i(x,y),y),i(i(y,x),x))) # label(MV_3).
9 [] P(i(i(n(x),n(y)),i(y,x))) # label(MV_4).
114 [hyper,5,6,6] P(i(x,i(y,i(z,y)))).
115 [hyper,5,7,7] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))).
117 [hyper,5,7,6] P(i(i(i(x,y),z),i(y,z))).
118 [hyper,5,7,8] P(i(i(i(i(x,y),y),z),i(i(i(y,x),x),z))).
120 [hyper,5,7,9] P(i(i(i(x,y),z),i(i(n(y),n(x)),z))).
122 [hyper,5,8,114] P(i(i(i(x,i(y,x)),z),z)).
127 [hyper,5,117,9] P(i(n(x),i(x,y))).
128 [hyper,5,117,8] P(i(x,i(i(x,y),y))).
131 [hyper,5,7,127] P(i(i(i(x,y),z),i(n(x),z))).
133 [hyper,5,128,128] P(i(i(i(x,i(i(x,y),y)),z),z)).
135 [hyper,5,7,128] P(i(i(i(i(x,y),y),z),i(x,z))).
144 [hyper,5,117,122] P(i(x,x)).
147 [hyper,5,128,144] P(i(i(i(x,x),y),y)).
153 [hyper,5,128,131] P(i(i(i(i(i(x,y),z),i(n(x),z)),u),u)).
183 [hyper,5,120,147] P(i(i(n(x),n(i(y,y))),x)).
192 [hyper,5,131,183] P(i(n(n(x)),x)).
200 [hyper,5,9,192] P(i(x,n(n(x)))).
235 [hyper,5,135,115] P(i(i(x,y),i(i(z,x),i(z,y)))).
246 [hyper,5,115,135] P(i(i(x,i(y,z)),i(y,i(x,z)))).
247 [hyper,5,115,133] P(i(i(x,y),i(x,i(i(y,z),z)))).
250 [hyper,5,115,7] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))).
260 [hyper,5,235,200] P(i(i(x,y),i(x,n(n(y))))).
263 [hyper,5,235,153] P(i(i(x,i(i(i(i(y,z),u),i(n(y),u)),v)),i(x,v))).
269 [hyper,5,235,120] P(i(i(x,i(i(y,z),u)),i(x,i(i(n(z),n(y)),u)))).
272 [hyper,5,235,9] P(i(i(x,i(n(y),n(z))),i(x,i(z,y)))).
273 [hyper,5,235,8] P(i(i(x,i(i(y,z),z)),i(x,i(i(z,y),y)))).
299 [hyper,5,235,246] P(i(i(x,i(y,i(z,u))),i(x,i(z,i(y,u))))).
301 [hyper,5,135,246] P(i(x,i(y,i(i(x,i(y,z)),z)))).
304 [hyper,5,7,246] P(i(i(i(x,i(y,z)),u),i(i(y,i(x,z)),u))).
315 [hyper,5,246,247] P(i(x,i(i(x,y),i(i(y,z),z)))).
381 [hyper,5,128,315] P(i(i(i(x,i(i(x,y),i(i(y,z),z))),u),u)).
421 [hyper,5,272,260] P(i(i(n(x),y),i(n(y),x))).
488 [hyper,5,7,250] P(i(i(i(i(i(x,y),z),i(i(u,y),z)),v),i(i(x,u),v))).
496 [hyper,5,250,246] P(i(i(i(i(x,i(y,z)),u),v),i(i(i(y,i(x,z)),u),v))).
499 [hyper,5,250,192] P(i(i(i(n(n(x)),y),z),i(i(x,y),z))).
527 [hyper,5,499,421] P(i(i(x,y),i(n(y),n(x)))).
538 [hyper,5,499,9] P(i(i(x,n(y)),i(y,n(x)))).
545 [hyper,5,250,527] P(i(i(i(i(x,y),z),u),i(i(i(n(y),n(x)),z),u))).
548 [hyper,5,235,527] P(i(i(x,i(y,z)),i(x,i(n(z),n(y))))).
554 [hyper,5,122,527] P(i(n(i(x,y)),n(y))).
557 [hyper,5,7,527] P(i(i(i(n(x),n(y)),z),i(i(y,x),z))).
576 [hyper,5,527,120] P(i(n(i(i(n(x),n(y)),z)),n(i(i(y,x),z)))).
607 [hyper,5,7,538] P(i(i(i(x,n(y)),z),i(i(y,n(x)),z))).
635 [hyper,5,548,301] P(i(x,i(n(i(i(x,i(y,z)),z)),n(y)))).
654 [hyper,5,527,557] P(i(n(i(i(x,y),z)),n(i(i(n(y),n(x)),z)))).
660 [hyper,5,235,557] P(i(i(x,i(i(n(y),n(z)),u)),i(x,i(i(z,y),u)))).
723 [hyper,5,246,635] P(i(n(i(i(x,i(y,z)),z)),i(x,n(y)))).
772 [hyper,5,421,723] P(i(n(i(x,n(y))),i(i(x,i(y,z)),z))).
790 [hyper,5,246,772] P(i(i(x,i(y,z)),i(n(i(x,n(y))),z))).
805 [hyper,5,250,790] P(i(i(i(i(x,i(y,z)),u),v),i(i(i(n(i(x,n(y))),z),u),v))).
859 [hyper,5,250,273] P(i(i(i(i(x,i(i(y,z),z)),u),v),i(i(i(x,i(i(z,y),y)),u),v))).
868 [hyper,5,7,273] P(i(i(i(x,i(i(y,z),z)),u),i(i(x,i(i(z,y),y)),u))).
920 [hyper,5,299,273] P(i(i(x,i(i(y,z),z)),i(i(z,y),i(x,y)))).
1005 [hyper,5,235,576] P(i(i(x,n(i(i(n(y),n(z)),u))),i(x,n(i(i(z,y),u))))).
1017 [hyper,5,235,654] P(i(i(x,n(i(i(y,z),u))),i(x,n(i(i(n(z),n(y)),u))))).
1027 [hyper,5,304,920] P(i(i(i(x,y),i(z,y)),i(i(y,x),i(z,x)))).
1066 [hyper,5,920,120] P(i(i(n(x),n(y)),i(i(i(x,y),n(x)),n(y)))).
1084 [hyper,5,7,1027] P(i(i(i(i(x,y),i(z,y)),u),i(i(i(y,x),i(z,x)),u))).
1090 [hyper,5,557,1066] P(i(i(x,y),i(i(i(y,x),n(y)),n(x)))).
1106 [hyper,5,1066,554] P(i(i(i(i(x,y),y),n(i(x,y))),n(y))).
1116 [hyper,5,381,1090] P(i(i(i(i(i(x,y),i(i(y,z),z)),x),n(i(i(x,y),i(i(y,z),z)))),n(x))).
1123 [hyper,5,246,1090] P(i(i(i(x,y),n(x)),i(i(y,x),n(y)))).
1160 [hyper,5,7,1106] P(i(i(n(x),y),i(i(i(i(z,x),x),n(i(z,x))),y))).
1177 [hyper,5,7,1123] P(i(i(i(i(x,y),n(x)),z),i(i(i(y,x),n(y)),z))).
1203 [hyper,5,269,548] P(i(i(i(x,y),i(z,u)),i(i(n(y),n(x)),i(n(u),n(z))))).
1261 [hyper,5,545,272] P(i(i(i(n(x),n(y)),i(n(z),n(u))),i(i(y,x),i(u,z)))).
1288 [hyper,5,7,660] P(i(i(i(x,i(i(y,z),u)),v),i(i(x,i(i(n(z),n(y)),u)),v))).
1500 [hyper,5,527,868] P(i(n(i(i(x,i(i(y,z),z)),u)),n(i(i(x,i(i(z,y),y)),u)))).
1553 [hyper,5,7,1005] P(i(i(i(x,n(i(i(y,z),u))),v),i(i(x,n(i(i(n(z),n(y)),u))),v))).
1568 [hyper,5,250,1017] P(i(i(i(i(x,n(i(i(y,z),u))),v),w),i(i(i(x,n(i(i(n(z),n(y)),u))),v),w))).
1698 [hyper,5,1084,1261] P(i(i(i(n(x),n(y)),i(n(z),n(y))),i(i(x,y),i(x,z)))).
1730 [hyper,5,235,1698] P(i(i(x,i(i(n(y),n(z)),i(n(u),n(z)))),i(x,i(i(y,z),i(y,u))))).
1821 [hyper,5,235,1500] P(i(i(x,n(i(i(y,i(i(z,u),u)),v))),i(x,n(i(i(y,i(i(u,z),z)),v))))).
1833 [hyper,5,859,488] P(i(i(i(i(i(x,y),y),i(i(y,z),z)),u),i(i(x,z),u))).
1858 [hyper,5,247,1833] P(i(i(i(i(i(x,y),y),i(i(y,z),z)),u),i(i(i(i(x,z),u),v),v))).
1916 [hyper,5,1730,1203] P(i(i(i(x,y),i(x,z)),i(i(y,x),i(y,z)))).
1943 [hyper,5,263,1916] P(i(i(i(i(n(x),y),i(i(x,z),y)),i(i(n(x),y),u)),i(i(i(x,z),y),u))).
1945 [hyper,5,250,1916] P(i(i(i(i(i(x,y),i(x,z)),u),v),i(i(i(i(y,x),i(y,z)),u),v))).
1956 [hyper,5,548,1858] P(i(i(i(i(i(x,y),y),i(i(y,z),z)),u),i(n(v),n(i(i(i(x,z),u),v))))).
2012 [hyper,5,235,1116] P(i(i(x,i(i(i(i(y,z),i(i(z,u),u)),y),n(i(i(y,z),i(i(z,u),u))))),i(x,n(y)))).
2017 [hyper,5,496,1943] P(i(i(i(i(x,y),i(i(n(x),z),z)),i(i(n(x),z),u)),i(i(i(x,y),z),u))).
2020 [hyper,5,246,1956] P(i(n(x),i(i(i(i(i(y,z),z),i(i(z,u),u)),v),n(i(i(i(y,u),v),x))))).
2046 [hyper,5,269,2020] P(i(n(x),i(i(n(y),n(i(i(i(z,u),u),i(i(u,v),v)))),n(i(i(i(z,v),y),x))))).
2051 [hyper,5,1160,2046] P(i(i(i(i(x,y),y),n(i(x,y))),i(i(n(z),n(i(i(i(u,v),v),i(i(v,w),w)))),n(i(i(i(u,w),z),y))))).
2052 [hyper,5,7,2012] P(i(i(i(x,n(y)),z),i(i(x,i(i(i(i(y,u),i(i(u,v),v)),y),n(i(i(y,u),i(i(u,v),v))))),z))).
2053 [hyper,5,2052,2051] P(i(i(i(i(x,y),y),i(i(i(i(i(x,y),z),i(i(z,u),u)),i(x,y)),n(i(i(i(x,y),z),i(i(z,u),u))))),i(i(n(v),n(i(i(i(w,v6),v6),i(i(v6,v7),v7)))),n(i(i(i(w,v7),v),y))))).
2054 [hyper,5,1288,2053] P(i(i(i(i(x,y),y),i(i(n(i(x,y)),n(i(i(i(x,y),z),i(i(z,u),u)))),n(i(i(i(x,y),z),i(i(z,u),u))))),i(i(n(v),n(i(i(i(w,v6),v6),i(i(v6,v7),v7)))),n(i(i(i(w,v7),v),y))))).
2055 [hyper,5,2017,2054] P(i(i(i(i(x,y),y),n(i(i(i(x,y),y),i(i(y,z),z)))),n(i(i(i(x,z),i(x,y)),y)))).
2056 [hyper,5,607,2055] P(i(i(i(i(i(x,y),y),i(i(y,z),z)),n(i(i(x,y),y))),n(i(i(i(x,z),i(x,y)),y)))).
2058 [hyper,5,1177,2056] P(i(i(i(i(i(x,y),y),i(i(z,x),x)),n(i(i(x,y),y))),n(i(i(i(z,y),i(z,x)),x)))).
2059 [hyper,5,538,2058] P(i(i(i(i(x,y),i(x,z)),z),n(i(i(i(i(z,y),y),i(i(x,z),z)),n(i(i(z,y),y)))))).
2062 [hyper,5,1821,2059] P(i(i(i(i(x,y),i(x,z)),z),n(i(i(i(i(z,y),y),i(i(z,x),x)),n(i(i(z,y),y)))))).
2064 [hyper,5,1945,2062] P(i(i(i(i(x,y),i(x,z)),z),n(i(i(i(i(z,x),x),i(i(z,y),y)),n(i(i(z,x),x)))))).
2066 [hyper,5,805,2064] P(i(i(i(n(i(i(x,y),n(x))),z),z),n(i(i(i(i(z,x),x),i(i(z,y),y)),n(i(i(z,x),x)))))).
2067 [hyper,5,118,2066] P(i(i(i(x,n(i(i(y,z),n(y)))),n(i(i(y,z),n(y)))),n(i(i(i(i(x,y),y),i(i(x,z),z)),n(i(i(x,y),y)))))).
2068 [hyper,5,1017,2067] P(i(i(i(x,n(i(i(y,z),n(y)))),n(i(i(y,z),n(y)))),n(i(i(n(i(i(x,z),z)),n(i(i(x,y),y))),n(i(i(x,y),y)))))).
2069 [hyper,5,1553,2068] P(i(i(i(x,n(i(i(y,z),n(y)))),n(i(i(n(z),n(y)),n(y)))),n(i(i(n(i(i(x,z),z)),n(i(i(x,y),y))),n(i(i(x,y),y)))))).
2071 [hyper,5,1568,2069] P(i(i(i(x,n(i(i(n(y),n(z)),n(z)))),n(i(i(n(y),n(z)),n(z)))),n(i(i(n(i(i(x,y),y)),n(i(i(x,z),z))),n(i(i(x,z),z)))))).
2072 [binary,2071.1,3.1] $F.
------------ end of proof / derivation -------------