Length of proof is 140. Level of proof is 43.
---------------- PROOF ----------------
2 [] -P(i(i(i(n(i(i(n(p),n(q)),n(q))),n(i(i(n(p),n(r)),n(r)))),n(i(i(n(p),n(r)),n(r)))),n(i(i(n(p),n(i(i(q,r),r))),n(i(i(q,r),r)))))) # label("KA2").
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).
154 [hyper,5,6,6] P(i(x,i(y,i(z,y)))).
155 [hyper,5,7,7] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))).
157 [hyper,5,7,6] P(i(i(i(x,y),z),i(y,z))).
158 [hyper,5,7,8] P(i(i(i(i(x,y),y),z),i(i(i(y,x),x),z))).
160 [hyper,5,7,9] P(i(i(i(x,y),z),i(i(n(y),n(x)),z))).
162 [hyper,5,8,154] P(i(i(i(x,i(y,x)),z),z)).
163 [hyper,5,7,154] P(i(i(i(x,i(y,x)),z),i(u,z))).
165 [hyper,5,7,157] P(i(i(i(x,y),z),i(i(i(u,x),y),z))).
167 [hyper,5,157,9] P(i(n(x),i(x,y))).
168 [hyper,5,157,8] P(i(x,i(i(x,y),y))).
171 [hyper,5,7,167] P(i(i(i(x,y),z),i(n(x),z))).
184 [hyper,5,157,162] P(i(x,x)).
187 [hyper,5,168,184] P(i(i(i(x,x),y),y)).
188 [hyper,5,6,184] P(i(x,i(y,y))).
190 [hyper,5,7,188] P(i(i(i(x,x),y),i(z,y))).
196 [hyper,5,7,190] P(i(i(i(x,y),z),i(i(i(u,u),y),z))).
225 [hyper,5,160,187] P(i(i(n(x),n(i(y,y))),x)).
234 [hyper,5,171,225] P(i(n(n(x)),x)).
242 [hyper,5,9,234] P(i(x,n(n(x)))).
243 [hyper,5,7,234] P(i(i(x,y),i(n(n(x)),y))).
253 [hyper,5,7,242] P(i(i(n(n(x)),y),i(x,y))).
277 [hyper,5,7,243] P(i(i(i(n(n(x)),y),z),i(i(x,y),z))).
298 [hyper,5,7,253] P(i(i(i(x,y),z),i(i(n(n(x)),y),z))).
310 [hyper,5,7,165] P(i(i(i(i(i(x,y),z),u),v),i(i(i(y,z),u),v))).
365 [hyper,5,7,298] P(i(i(i(i(n(n(x)),y),z),u),i(i(i(x,y),z),u))).
392 [hyper,5,155,155] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))).
405 [hyper,5,155,7] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))).
417 [hyper,5,7,158] P(i(i(i(i(i(x,y),y),z),u),i(i(i(i(y,x),x),z),u))).
450 [hyper,5,392,168] P(i(i(x,i(y,z)),i(y,i(x,z)))).
468 [hyper,5,7,450] P(i(i(i(x,i(y,z)),u),i(i(y,i(x,z)),u))).
476 [hyper,5,450,8] P(i(i(x,y),i(i(i(y,x),x),y))).
477 [hyper,5,450,7] P(i(i(x,y),i(i(z,x),i(z,y)))).
479 [hyper,5,392,476] P(i(i(x,i(i(y,z),z)),i(i(z,y),i(x,y)))).
491 [hyper,5,7,476] P(i(i(i(i(i(x,y),y),x),z),i(i(y,x),z))).
520 [hyper,5,392,477] P(i(i(x,i(y,z)),i(i(z,u),i(x,i(y,u))))).
534 [hyper,5,477,450] P(i(i(x,i(y,i(z,u))),i(x,i(z,i(y,u))))).
540 [hyper,5,477,242] P(i(i(x,y),i(x,n(n(y))))).
541 [hyper,5,477,234] P(i(i(x,n(n(y))),i(x,y))).
555 [hyper,5,477,9] P(i(i(x,i(n(y),n(z))),i(x,i(z,y)))).
556 [hyper,5,477,8] P(i(i(x,i(i(y,z),z)),i(x,i(i(z,y),y)))).
624 [hyper,5,555,540] P(i(i(n(x),y),i(n(y),x))).
636 [hyper,5,277,624] P(i(i(x,y),i(n(y),n(x)))).
644 [hyper,5,7,624] P(i(i(i(n(x),y),z),i(i(n(y),x),z))).
650 [hyper,5,477,636] P(i(i(x,i(y,z)),i(x,i(n(z),n(y))))).
663 [hyper,5,7,636] P(i(i(i(n(x),n(y)),z),i(i(y,x),z))).
667 [hyper,5,636,541] P(i(n(i(x,y)),n(i(x,n(n(y)))))).
673 [hyper,5,636,298] P(i(n(i(i(n(n(x)),y),z)),n(i(i(x,y),z)))).
674 [hyper,5,636,277] P(i(n(i(i(x,y),z)),n(i(i(n(n(x)),y),z)))).
687 [hyper,5,636,160] P(i(n(i(i(n(x),n(y)),z)),n(i(i(y,x),z)))).
691 [hyper,5,636,9] P(i(n(i(x,y)),n(i(n(y),n(x))))).
692 [hyper,5,636,8] P(i(n(i(i(x,y),y)),n(i(i(y,x),x)))).
701 [hyper,5,7,667] P(i(i(n(i(x,n(n(y)))),z),i(n(i(x,y)),z))).
705 [hyper,5,477,691] P(i(i(x,n(i(y,z))),i(x,n(i(n(z),n(y)))))).
780 [hyper,5,636,663] P(i(n(i(i(x,y),z)),n(i(i(n(y),n(x)),z)))).
795 [hyper,5,7,663] P(i(i(i(i(x,y),z),u),i(i(i(n(y),n(x)),z),u))).
802 [hyper,5,477,692] P(i(i(x,n(i(i(y,z),z))),i(x,n(i(i(z,y),y))))).
836 [hyper,5,405,663] P(i(i(i(i(i(n(x),n(y)),z),u),v),i(i(i(i(y,x),z),u),v))).
844 [hyper,5,405,450] P(i(i(i(i(x,i(y,z)),u),v),i(i(i(y,i(x,z)),u),v))).
849 [hyper,5,405,196] P(i(i(i(i(i(x,y),z),u),v),i(i(i(i(i(w,w),y),z),u),v))).
857 [hyper,5,405,158] P(i(i(i(i(i(i(x,y),y),z),u),v),i(i(i(i(i(y,x),x),z),u),v))).
945 [hyper,5,479,160] P(i(i(n(x),n(y)),i(i(i(x,y),n(x)),n(y)))).
1012 [hyper,5,520,479] P(i(i(i(x,y),z),i(i(x,i(i(y,u),u)),i(i(u,y),z)))).
1079 [hyper,5,534,168] P(i(x,i(y,i(i(x,i(y,z)),z)))).
1088 [hyper,5,650,1079] P(i(x,i(n(i(i(x,i(y,z)),z)),n(y)))).
1177 [hyper,5,450,1088] P(i(n(i(i(x,i(y,z)),z)),i(x,n(y)))).
1250 [hyper,5,624,1177] P(i(n(i(x,n(y))),i(i(x,i(y,z)),z))).
1271 [hyper,5,450,1250] P(i(i(x,i(y,z)),i(n(i(x,n(y))),z))).
1305 [hyper,5,163,1271] P(i(x,i(n(i(y,n(z))),y))).
1404 [hyper,5,556,644] P(i(i(i(n(x),y),x),i(i(x,n(y)),n(y)))).
1440 [hyper,5,7,1404] P(i(i(i(i(x,n(y)),n(y)),z),i(i(i(n(x),y),x),z))).
1446 [hyper,5,477,673] P(i(i(x,n(i(i(n(n(y)),z),u))),i(x,n(i(i(y,z),u))))).
1458 [hyper,5,477,674] P(i(i(x,n(i(i(y,z),u))),i(x,n(i(i(n(n(y)),z),u))))).
1470 [hyper,5,477,687] P(i(i(x,n(i(i(n(y),n(z)),u))),i(x,n(i(i(z,y),u))))).
1476 [hyper,5,7,687] P(i(i(n(i(i(x,y),z)),u),i(n(i(i(n(y),n(x)),z)),u))).
1489 [hyper,5,477,701] P(i(i(x,i(n(i(y,n(n(z)))),u)),i(x,i(n(i(y,z)),u)))).
1541 [hyper,5,7,705] P(i(i(i(x,n(i(n(y),n(z)))),u),i(i(x,n(i(z,y))),u))).
1557 [hyper,5,477,780] P(i(i(x,n(i(i(y,z),u))),i(x,n(i(i(n(z),n(y)),u))))).
1568 [hyper,5,663,945] P(i(i(x,y),i(i(i(y,x),n(y)),n(x)))).
1744 [hyper,5,477,365] P(i(i(x,i(i(i(n(n(y)),z),u),v)),i(x,i(i(i(y,z),u),v)))).
1804 [hyper,5,405,795] P(i(i(i(i(i(i(x,y),z),u),v),w),i(i(i(i(i(n(y),n(x)),z),u),v),w))).
1880 [hyper,5,7,802] P(i(i(i(x,n(i(i(y,z),z))),u),i(i(x,n(i(i(z,y),y))),u))).
1902 [hyper,5,477,1440] P(i(i(x,i(i(i(y,n(z)),n(z)),u)),i(x,i(i(i(n(y),z),y),u)))).
1960 [hyper,5,405,417] P(i(i(i(i(i(i(i(x,y),y),z),u),v),w),i(i(i(i(i(i(y,x),x),z),u),v),w))).
2020 [hyper,5,405,844] P(i(i(i(i(i(i(x,i(y,z)),u),v),w),v6),i(i(i(i(i(y,i(x,z)),u),v),w),v6))).
2101 [hyper,5,158,1012] P(i(i(i(x,y),y),i(i(y,i(i(x,z),z)),i(i(z,x),x)))).
2169 [hyper,5,405,1446] P(i(i(i(i(x,n(i(i(n(n(y)),z),u))),v),w),i(i(i(x,n(i(i(y,z),u))),v),w))).
2227 [hyper,5,7,1458] P(i(i(i(x,n(i(i(n(n(y)),z),u))),v),i(i(x,n(i(i(y,z),u))),v))).
2270 [hyper,5,7,1470] P(i(i(i(x,n(i(i(y,z),u))),v),i(i(x,n(i(i(n(z),n(y)),u))),v))).
2295 [hyper,5,405,1476] P(i(i(i(i(n(i(i(x,y),z)),u),v),w),i(i(i(n(i(i(n(y),n(x)),z)),u),v),w))).
2352 [hyper,5,1489,1305] P(i(x,i(n(i(y,z)),y))).
2384 [hyper,5,477,1541] P(i(i(x,i(i(y,n(i(n(z),n(u)))),v)),i(x,i(i(y,n(i(u,z))),v)))).
2453 [hyper,5,405,1557] 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))).
2495 [hyper,5,392,2101] P(i(i(x,i(y,i(i(z,u),u))),i(i(i(z,y),y),i(x,i(i(u,z),z))))).
2525 [hyper,5,477,836] P(i(i(x,i(i(i(i(n(y),n(z)),u),v),w)),i(x,i(i(i(i(z,y),u),v),w)))).
2757 [hyper,5,477,1880] P(i(i(x,i(i(y,n(i(i(z,u),u))),v)),i(x,i(i(y,n(i(i(u,z),z))),v)))).
2904 [hyper,5,477,857] P(i(i(x,i(i(i(i(i(y,z),z),u),v),w)),i(x,i(i(i(i(i(z,y),y),u),v),w)))).
2991 [hyper,5,405,2227] P(i(i(i(i(i(x,n(i(i(n(n(y)),z),u))),v),w),v6),i(i(i(i(x,n(i(i(y,z),u))),v),w),v6))).
3221 [hyper,5,468,2495] P(i(i(x,i(y,i(i(z,u),u))),i(i(i(z,x),x),i(y,i(i(u,z),z))))).
3359 [hyper,5,3221,1012] P(i(i(i(x,i(i(y,z),z)),i(i(y,z),z)),i(i(y,i(i(z,x),x)),i(i(z,x),x)))).
3713 [hyper,5,1960,310] P(i(i(i(i(i(i(x,y),y),z),u),v),i(i(i(x,z),u),v))).
4086 [hyper,5,405,2295] P(i(i(i(i(i(i(n(i(i(x,y),z)),u),v),w),v6),v7),i(i(i(i(i(n(i(i(n(y),n(x)),z)),u),v),w),v6),v7))).
4191 [hyper,5,405,2453] P(i(i(i(i(i(i(x,n(i(i(y,z),u))),v),w),v6),v7),i(i(i(i(i(x,n(i(i(n(z),n(y)),u))),v),w),v6),v7))).
4384 [hyper,5,158,3359] P(i(i(i(i(i(x,y),y),z),z),i(i(x,i(i(y,z),z)),i(i(y,z),z)))).
4412 [hyper,5,479,4384] P(i(i(i(i(x,y),y),z),i(i(i(i(i(z,x),x),y),y),z))).
4431 [hyper,5,2904,4412] P(i(i(i(i(x,y),y),z),i(i(i(i(i(x,z),z),y),y),z))).
4587 [hyper,5,7,4431] P(i(i(i(i(i(i(i(x,y),y),z),z),y),u),i(i(i(i(x,z),z),y),u))).
4702 [hyper,5,4587,849] P(i(i(i(i(x,y),y),z),i(i(i(i(i(u,u),z),y),y),z))).
4727 [hyper,5,3713,4702] P(i(i(i(x,y),z),i(i(i(i(i(u,u),z),y),y),z))).
5197 [hyper,5,7,2352] P(i(i(i(n(i(x,y)),x),z),i(u,z))).
5230 [hyper,5,405,5197] P(i(i(i(i(i(n(i(x,y)),x),z),u),v),i(i(i(w,z),u),v))).
5315 [hyper,5,405,5230] P(i(i(i(i(i(i(i(n(i(x,y)),x),z),u),v),w),v6),i(i(i(i(i(v7,z),u),v),w),v6))).
5446 [hyper,5,5315,3713] P(i(i(i(i(i(x,y),z),u),v),i(i(i(n(i(y,w)),z),u),v))).
5508 [hyper,5,4587,5446] P(i(i(i(i(x,y),y),z),i(i(i(n(i(z,u)),y),y),z))).
5648 [hyper,5,491,5508] P(i(i(x,y),i(i(i(n(i(y,z)),x),x),y))).
5719 [hyper,5,1902,5648] P(i(i(n(x),y),i(i(i(n(n(i(y,z))),x),n(i(y,z))),y))).
5857 [hyper,5,1744,5719] P(i(i(n(x),y),i(i(i(i(y,z),x),n(i(y,z))),y))).
5911 [hyper,5,2525,5857] P(i(i(n(x),n(y)),i(i(i(i(z,y),x),n(i(n(y),n(z)))),n(y)))).
5967 [hyper,5,2384,5911] P(i(i(n(x),n(y)),i(i(i(i(z,y),x),n(i(z,y))),n(y)))).
6026 [hyper,5,663,5967] P(i(i(x,y),i(i(i(i(z,x),y),n(i(z,x))),n(x)))).
6064 [hyper,5,2904,6026] P(i(i(x,y),i(i(i(i(i(x,z),z),y),n(i(i(z,x),x))),n(x)))).
6099 [hyper,5,450,6026] P(i(i(i(i(x,y),z),n(i(x,y))),i(i(y,z),n(y)))).
6227 [hyper,5,1568,6099] P(i(i(i(i(i(x,y),n(x)),i(i(i(z,x),y),n(i(z,x)))),n(i(i(x,y),n(x)))),n(i(i(i(z,x),y),n(i(z,x)))))).
6269 [hyper,5,2757,6064] P(i(i(x,y),i(i(i(i(i(x,z),z),y),n(i(i(x,z),z))),n(x)))).
6439 [hyper,5,7,6269] P(i(i(i(i(i(i(i(x,y),y),z),n(i(i(x,y),y))),n(x)),u),i(i(x,z),u))).
6562 [hyper,5,477,6439] P(i(i(x,i(i(i(i(i(i(y,z),z),u),n(i(i(y,z),z))),n(y)),v)),i(x,i(i(y,u),v)))).
6660 [hyper,5,405,6562] P(i(i(i(i(x,i(i(i(i(i(i(y,z),z),u),n(i(i(y,z),z))),n(y)),v)),w),v6),i(i(i(x,i(i(y,u),v)),w),v6))).
6724 [hyper,5,1557,6227] P(i(i(i(i(i(x,y),n(x)),i(i(i(z,x),y),n(i(z,x)))),n(i(i(x,y),n(x)))),n(i(i(n(y),n(i(z,x))),n(i(z,x)))))).
6782 [hyper,5,405,6660] P(i(i(i(i(i(i(x,i(i(i(i(i(i(y,z),z),u),n(i(i(y,z),z))),n(y)),v)),w),v6),v7),v8),i(i(i(i(i(x,i(i(y,u),v)),w),v6),v7),v8))).
6859 [hyper,5,2270,6724] P(i(i(i(i(i(x,y),n(x)),i(i(i(z,x),y),n(i(z,x)))),n(i(i(n(y),n(x)),n(x)))),n(i(i(n(y),n(i(z,x))),n(i(z,x)))))).
7128 [hyper,5,4727,6859] P(i(i(i(i(i(x,x),n(i(i(n(y),n(i(z,u))),n(i(z,u))))),n(i(i(n(y),n(u)),n(u)))),n(i(i(n(y),n(u)),n(u)))),n(i(i(n(y),n(i(z,u))),n(i(z,u)))))).
7170 [hyper,5,2991,7128] P(i(i(i(i(i(x,x),n(i(i(y,n(i(z,u))),n(i(z,u))))),n(i(i(n(n(y)),n(u)),n(u)))),n(i(i(n(n(y)),n(u)),n(u)))),n(i(i(n(n(y)),n(i(z,u))),n(i(z,u)))))).
7174 [hyper,5,2169,7170] P(i(i(i(i(i(x,x),n(i(i(y,n(i(z,u))),n(i(z,u))))),n(i(i(y,n(u)),n(u)))),n(i(i(n(n(y)),n(u)),n(u)))),n(i(i(n(n(y)),n(i(z,u))),n(i(z,u)))))).
7177 [hyper,5,2227,7174] P(i(i(i(i(i(x,x),n(i(i(y,n(i(z,u))),n(i(z,u))))),n(i(i(y,n(u)),n(u)))),n(i(i(y,n(u)),n(u)))),n(i(i(n(n(y)),n(i(z,u))),n(i(z,u)))))).
7185 [hyper,5,1446,7177] P(i(i(i(i(i(x,x),n(i(i(y,n(i(z,u))),n(i(z,u))))),n(i(i(y,n(u)),n(u)))),n(i(i(y,n(u)),n(u)))),n(i(i(y,n(i(z,u))),n(i(z,u)))))).
7193 [hyper,5,2020,7185] P(i(i(i(i(i(x,i(i(x,y),y)),n(i(i(z,n(i(u,v))),n(i(u,v))))),n(i(i(z,n(v)),n(v)))),n(i(i(z,n(v)),n(v)))),n(i(i(z,n(i(u,v))),n(i(u,v)))))).
7209 [hyper,5,6782,7193] P(i(i(i(i(i(i(i(i(i(x,y),y),z),n(i(i(x,y),y))),i(i(x,z),n(x))),n(i(i(u,n(i(v,w))),n(i(v,w))))),n(i(i(u,n(w)),n(w)))),n(i(i(u,n(w)),n(w)))),n(i(i(u,n(i(v,w))),n(i(v,w)))))).
7212 [hyper,5,1804,7209] P(i(i(i(i(i(n(i(i(x,y),n(x))),n(i(i(i(i(x,z),z),y),n(i(i(x,z),z))))),n(i(i(u,n(i(v,w))),n(i(v,w))))),n(i(i(u,n(w)),n(w)))),n(i(i(u,n(w)),n(w)))),n(i(i(u,n(i(v,w))),n(i(v,w)))))).
7213 [hyper,5,4086,7212] P(i(i(i(i(i(n(i(i(n(x),n(y)),n(y))),n(i(i(i(i(y,z),z),x),n(i(i(y,z),z))))),n(i(i(u,n(i(v,w))),n(i(v,w))))),n(i(i(u,n(w)),n(w)))),n(i(i(u,n(w)),n(w)))),n(i(i(u,n(i(v,w))),n(i(v,w)))))).
7214 [hyper,5,4191,7213] P(i(i(i(i(i(n(i(i(n(x),n(y)),n(y))),n(i(i(n(x),n(i(i(y,z),z))),n(i(i(y,z),z))))),n(i(i(u,n(i(v,w))),n(i(v,w))))),n(i(i(u,n(w)),n(w)))),n(i(i(u,n(w)),n(w)))),n(i(i(u,n(i(v,w))),n(i(v,w)))))).
7215 [hyper,5,3713,7214] P(i(i(i(n(i(i(n(x),n(y)),n(y))),n(i(i(n(x),n(z)),n(z)))),n(i(i(n(x),n(z)),n(z)))),n(i(i(n(x),n(i(i(y,z),z))),n(i(i(y,z),z)))))).
7216 [binary,7215.1,2.1] $F.
------------ end of proof / derivation -------------