Length of proof is 112. Level of proof is 37.
---------------- PROOF ----------------
1 [] -P(i(n(i(i(n(p),n(i(i(q,r),r))),n(i(i(q,r),r)))),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)))))) # label("KA1").
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).
128 [hyper,5,6,6] P(i(x,i(y,i(z,y)))).
129 [hyper,5,7,7] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))).
131 [hyper,5,7,6] P(i(i(i(x,y),z),i(y,z))).
132 [hyper,5,7,8] P(i(i(i(i(x,y),y),z),i(i(i(y,x),x),z))).
134 [hyper,5,7,9] P(i(i(i(x,y),z),i(i(n(y),n(x)),z))).
136 [hyper,5,8,128] P(i(i(i(x,i(y,x)),z),z)).
141 [hyper,5,131,9] P(i(n(x),i(x,y))).
142 [hyper,5,131,8] P(i(x,i(i(x,y),y))).
144 [hyper,5,131,6] P(i(x,i(y,i(z,x)))).
145 [hyper,5,7,141] P(i(i(i(x,y),z),i(n(x),z))).
149 [hyper,5,7,142] P(i(i(i(i(x,y),y),z),i(x,z))).
178 [hyper,5,7,145] P(i(i(i(n(x),y),z),i(i(i(x,u),y),z))).
196 [hyper,5,149,7] P(i(x,i(i(y,z),i(i(x,y),z)))).
203 [hyper,5,7,196] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(z,u))).
230 [hyper,5,134,136] P(i(i(n(x),n(i(y,i(z,y)))),x)).
236 [hyper,5,145,230] P(i(n(n(x)),x)).
247 [hyper,5,9,236] P(i(x,n(n(x)))).
258 [hyper,5,7,247] P(i(i(n(n(x)),y),i(x,y))).
302 [hyper,5,178,9] P(i(i(i(x,y),n(z)),i(z,x))).
315 [hyper,5,149,129] P(i(i(x,y),i(i(z,x),i(z,y)))).
321 [hyper,5,129,129] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))).
327 [hyper,5,129,149] P(i(i(x,i(y,z)),i(y,i(x,z)))).
333 [hyper,5,129,7] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))).
347 [hyper,5,315,258] P(i(i(x,i(n(n(y)),z)),i(x,i(y,z)))).
348 [hyper,5,315,247] P(i(i(x,y),i(x,n(n(y))))).
349 [hyper,5,315,236] P(i(i(x,n(n(y))),i(x,y))).
362 [hyper,5,315,9] P(i(i(x,i(n(y),n(z))),i(x,i(z,y)))).
363 [hyper,5,315,8] P(i(i(x,i(i(y,z),z)),i(x,i(i(z,y),y)))).
405 [hyper,5,315,327] P(i(i(x,i(y,i(z,u))),i(x,i(z,i(y,u))))).
413 [hyper,5,7,327] P(i(i(i(x,i(y,z)),u),i(i(y,i(x,z)),u))).
420 [hyper,5,327,8] P(i(i(x,y),i(i(i(y,x),x),y))).
490 [hyper,5,362,348] P(i(i(n(x),y),i(n(y),x))).
500 [hyper,5,315,490] P(i(i(x,i(n(y),z)),i(x,i(n(z),y)))).
587 [hyper,5,203,327] P(i(x,i(i(x,y),i(i(y,z),z)))).
668 [hyper,5,321,420] P(i(i(x,i(i(y,z),z)),i(i(z,y),i(x,y)))).
674 [hyper,5,321,315] P(i(i(x,i(y,z)),i(i(z,u),i(x,i(y,u))))).
720 [hyper,5,333,236] P(i(i(i(n(n(x)),y),z),i(i(x,y),z))).
725 [hyper,5,333,144] P(i(i(i(x,y),z),i(i(i(u,i(v,x)),y),z))).
753 [hyper,5,720,490] P(i(i(x,y),i(n(y),n(x)))).
767 [hyper,5,720,9] P(i(i(x,n(y)),i(y,n(x)))).
774 [hyper,5,333,753] P(i(i(i(i(x,y),z),u),i(i(i(n(y),n(x)),z),u))).
775 [hyper,5,327,753] P(i(n(x),i(i(y,x),n(y)))).
777 [hyper,5,315,753] P(i(i(x,i(y,z)),i(x,i(n(z),n(y))))).
785 [hyper,5,136,753] P(i(n(i(x,y)),n(y))).
788 [hyper,5,7,753] P(i(i(i(n(x),n(y)),z),i(i(y,x),z))).
803 [hyper,5,753,302] P(i(n(i(x,y)),n(i(i(y,z),n(x))))).
824 [hyper,5,420,785] P(i(i(i(n(x),n(i(y,x))),n(i(y,x))),n(x))).
847 [hyper,5,149,767] P(i(x,i(y,n(i(x,n(y)))))).
861 [hyper,5,321,775] P(i(i(x,i(y,z)),i(n(z),i(x,n(y))))).
891 [hyper,5,134,847] P(i(i(n(x),n(y)),i(z,n(i(i(y,x),n(z)))))).
942 [hyper,5,315,803] P(i(i(x,n(i(y,z))),i(x,n(i(i(z,u),n(y)))))).
973 [hyper,5,777,775] P(i(n(x),i(n(n(y)),n(i(y,x))))).
1003 [hyper,5,347,973] P(i(n(x),i(y,n(i(y,x))))).
1029 [hyper,5,142,1003] P(i(i(i(n(x),i(y,n(i(y,x)))),z),z)).
1040 [hyper,5,315,788] P(i(i(x,i(i(n(y),n(z)),u)),i(x,i(i(z,y),u)))).
1048 [hyper,5,132,788] P(i(i(i(n(x),n(y)),n(y)),i(i(x,y),n(x)))).
1064 [hyper,5,500,861] P(i(i(x,i(y,z)),i(n(i(x,n(y))),z))).
1356 [hyper,5,413,668] P(i(i(i(x,y),i(z,y)),i(i(y,x),i(z,x)))).
1435 [hyper,5,674,847] P(i(i(n(i(x,n(y))),z),i(x,i(y,z)))).
1468 [hyper,5,674,134] P(i(i(x,y),i(i(i(z,u),x),i(i(n(u),n(z)),y)))).
1503 [hyper,5,7,1435] P(i(i(i(x,i(y,z)),u),i(i(n(i(x,n(y))),z),u))).
1598 [hyper,5,315,824] P(i(i(x,i(i(n(y),n(i(z,y))),n(i(z,y)))),i(x,n(y)))).
1618 [hyper,5,333,891] P(i(i(i(i(n(x),n(y)),z),u),i(i(i(v,n(i(i(y,x),n(v)))),z),u))).
1635 [hyper,5,753,1048] P(i(n(i(i(x,y),n(x))),n(i(i(n(x),n(y)),n(y))))).
1661 [hyper,5,333,1356] P(i(i(i(i(i(x,y),i(z,y)),u),v),i(i(i(i(y,x),i(z,x)),u),v))).
1671 [hyper,5,7,1356] P(i(i(i(i(x,y),i(z,y)),u),i(i(i(y,x),i(z,x)),u))).
1757 [hyper,5,774,362] P(i(i(i(n(x),n(y)),i(n(z),n(u))),i(i(y,x),i(u,z)))).
1859 [hyper,5,1468,753] P(i(i(i(x,y),i(z,u)),i(i(n(y),n(x)),i(n(u),n(z))))).
1906 [hyper,5,315,1503] P(i(i(x,i(i(y,i(z,u)),v)),i(x,i(i(n(i(y,n(z))),u),v)))).
1956 [hyper,5,315,1635] P(i(i(x,n(i(i(y,z),n(y)))),i(x,n(i(i(n(y),n(z)),n(z)))))).
2000 [hyper,5,1598,134] P(i(i(i(i(x,y),y),n(i(x,y))),n(y))).
2013 [hyper,5,315,2000] P(i(i(x,i(i(i(y,z),z),n(i(y,z)))),i(x,n(z)))).
2066 [hyper,5,2013,132] P(i(i(i(i(x,y),y),n(i(y,x))),n(x))).
2080 [hyper,5,315,2066] P(i(i(x,i(i(i(y,z),z),n(i(z,y)))),i(x,n(y)))).
2111 [hyper,5,203,2080] P(i(i(x,y),i(i(y,n(i(y,x))),n(x)))).
2142 [hyper,5,1029,2111] P(i(i(i(x,n(i(x,y))),n(i(i(x,n(i(x,y))),n(y)))),n(n(y)))).
2250 [hyper,5,1671,1757] P(i(i(i(n(x),n(y)),i(n(z),n(y))),i(i(x,y),i(x,z)))).
2364 [hyper,5,315,2250] P(i(i(x,i(i(n(y),n(z)),i(n(u),n(z)))),i(x,i(i(y,z),i(y,u))))).
2432 [hyper,5,333,1956] P(i(i(i(i(x,n(i(i(y,z),n(y)))),u),v),i(i(i(x,n(i(i(n(y),n(z)),n(z)))),u),v))).
2447 [hyper,5,349,2142] P(i(i(i(x,n(i(x,y))),n(i(i(x,n(i(x,y))),n(y)))),y)).
2454 [hyper,5,315,2447] P(i(i(x,i(i(y,n(i(y,z))),n(i(i(y,n(i(y,z))),n(z))))),i(x,z))).
2462 [hyper,5,315,1618] P(i(i(x,i(i(i(n(y),n(z)),u),v)),i(x,i(i(i(w,n(i(i(z,y),n(w)))),u),v)))).
2493 [hyper,5,1661,1356] P(i(i(i(i(x,y),i(z,y)),i(u,i(z,x))),i(i(i(z,x),i(y,x)),i(u,i(y,x))))).
2497 [hyper,5,1661,405] P(i(i(i(i(x,y),i(z,y)),i(u,i(v,w))),i(i(i(y,x),i(z,x)),i(v,i(u,w))))).
2512 [hyper,5,2364,1859] P(i(i(i(x,y),i(x,z)),i(i(y,x),i(y,z)))).
2514 [hyper,5,2364,777] P(i(i(i(n(x),n(y)),i(y,z)),i(i(x,y),i(x,z)))).
2546 [hyper,5,321,2512] P(i(i(x,i(y,z)),i(i(i(z,y),i(z,u)),i(x,i(y,u))))).
2588 [hyper,5,7,2514] P(i(i(i(i(x,y),i(x,z)),u),i(i(i(n(x),n(y)),i(y,z)),u))).
2652 [hyper,5,2546,9] P(i(i(i(x,y),i(x,z)),i(i(n(x),n(y)),i(y,z)))).
2692 [hyper,5,315,2588] P(i(i(x,i(i(i(y,z),i(y,u)),v)),i(x,i(i(i(n(y),n(z)),i(z,u)),v)))).
2731 [hyper,5,2454,942] P(i(i(i(x,n(i(x,y))),n(i(y,x))),y)).
2763 [hyper,5,315,2731] P(i(i(x,i(i(y,n(i(y,z))),n(i(z,y)))),i(x,z))).
2796 [hyper,5,203,2763] P(i(x,i(i(n(i(x,y)),n(i(y,x))),y))).
2829 [hyper,5,1040,2796] P(i(x,i(i(i(y,x),i(x,y)),y))).
2886 [hyper,5,327,2829] P(i(i(i(x,y),i(y,x)),i(y,x))).
2925 [hyper,5,725,2886] P(i(i(i(x,i(y,i(z,u))),i(u,z)),i(u,z))).
2976 [hyper,5,8,2925] P(i(i(i(x,y),i(z,i(u,i(y,x)))),i(z,i(u,i(y,x))))).
3008 [hyper,5,315,2692] P(i(i(x,i(y,i(i(i(z,u),i(z,v)),w))),i(x,i(y,i(i(i(n(z),n(u)),i(u,v)),w))))).
3036 [hyper,5,315,2493] P(i(i(x,i(i(i(y,z),i(u,z)),i(v,i(u,y)))),i(x,i(i(i(u,y),i(z,y)),i(v,i(z,y)))))).
3070 [hyper,5,315,2432] P(i(i(x,i(i(i(y,n(i(i(z,u),n(z)))),v),w)),i(x,i(i(i(y,n(i(i(n(z),n(u)),n(u)))),v),w)))).
3074 [hyper,5,3036,587] P(i(i(x,y),i(i(i(z,x),i(y,x)),i(i(i(z,y),i(z,x)),i(y,x))))).
3076 [hyper,5,2976,3074] P(i(i(i(x,y),i(z,y)),i(i(i(x,z),i(x,y)),i(z,y)))).
3080 [hyper,5,2692,3076] P(i(i(i(x,y),i(z,y)),i(i(i(n(x),n(z)),i(z,y)),i(z,y)))).
3132 [hyper,5,2462,3080] P(i(i(i(x,y),i(z,y)),i(i(i(u,n(i(i(z,x),n(u)))),i(z,y)),i(z,y)))).
3177 [hyper,5,3070,3132] P(i(i(i(x,y),i(z,y)),i(i(i(z,n(i(i(n(z),n(x)),n(x)))),i(z,y)),i(z,y)))).
3178 [hyper,5,363,3177] P(i(i(i(x,y),i(z,y)),i(i(i(z,y),i(z,n(i(i(n(z),n(x)),n(x))))),i(z,n(i(i(n(z),n(x)),n(x))))))).
3185 [hyper,5,2497,3178] P(i(i(i(x,y),i(z,y)),i(z,i(i(i(z,x),i(z,n(i(i(n(z),n(y)),n(y))))),n(i(i(n(z),n(y)),n(y))))))).
3186 [hyper,5,413,3185] P(i(i(x,i(i(y,z),z)),i(x,i(i(i(x,y),i(x,n(i(i(n(x),n(z)),n(z))))),n(i(i(n(x),n(z)),n(z))))))).
3187 [hyper,5,2652,3186] P(i(i(n(x),n(i(i(y,z),z))),i(i(i(y,z),z),i(i(i(x,y),i(x,n(i(i(n(x),n(z)),n(z))))),n(i(i(n(x),n(z)),n(z))))))).
3188 [hyper,5,3008,3187] P(i(i(n(x),n(i(i(y,z),z))),i(i(i(y,z),z),i(i(i(n(x),n(y)),i(y,n(i(i(n(x),n(z)),n(z))))),n(i(i(n(x),n(z)),n(z))))))).
3189 [hyper,5,1064,3188] P(i(n(i(i(n(x),n(i(i(y,z),z))),n(i(i(y,z),z)))),i(i(i(n(x),n(y)),i(y,n(i(i(n(x),n(z)),n(z))))),n(i(i(n(x),n(z)),n(z)))))).
3190 [hyper,5,1906,3189] P(i(n(i(i(n(x),n(i(i(y,z),z))),n(i(i(y,z),z)))),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)))))).
3191 [binary,3190.1,1.1] $F.
------------ end of proof / derivation -------------