Length of proof is 118. Level of proof is 48.
---------------- PROOF ----------------
4 [] -P(i(n(i(i(n(i(i(p,q),q)),n(i(i(p,r),r))),n(i(i(p,r),r)))),i(i(p,n(i(i(n(q),n(r)),n(r)))),n(i(i(n(q),n(r)),n(r)))))) # label("AK2").
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).
134 [hyper,5,6,6] P(i(x,i(y,i(z,y)))).
135 [hyper,5,7,7] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))).
137 [hyper,5,7,6] P(i(i(i(x,y),z),i(y,z))).
138 [hyper,5,7,8] P(i(i(i(i(x,y),y),z),i(i(i(y,x),x),z))).
140 [hyper,5,7,9] P(i(i(i(x,y),z),i(i(n(y),n(x)),z))).
142 [hyper,5,8,134] P(i(i(i(x,i(y,x)),z),z)).
147 [hyper,5,137,9] P(i(n(x),i(x,y))).
148 [hyper,5,137,8] P(i(x,i(i(x,y),y))).
151 [hyper,5,7,147] P(i(i(i(x,y),z),i(n(x),z))).
162 [hyper,5,148,7] P(i(i(i(i(x,y),i(i(y,z),i(x,z))),u),u)).
164 [hyper,5,137,142] P(i(x,x)).
165 [hyper,5,7,142] P(i(i(x,y),i(i(i(z,i(u,z)),x),y))).
167 [hyper,5,148,164] P(i(i(i(x,x),y),y)).
181 [hyper,5,151,9] P(i(n(n(x)),i(y,x))).
192 [hyper,5,140,167] P(i(i(n(x),n(i(y,y))),x)).
200 [hyper,5,151,192] P(i(n(n(x)),x)).
207 [hyper,5,148,200] P(i(i(i(n(n(x)),x),y),y)).
208 [hyper,5,9,200] P(i(x,n(n(x)))).
209 [hyper,5,7,200] P(i(i(x,y),i(n(n(x)),y))).
217 [hyper,5,7,208] P(i(i(n(n(x)),y),i(x,y))).
244 [hyper,5,7,209] P(i(i(i(n(n(x)),y),z),i(i(x,y),z))).
314 [hyper,5,135,135] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))).
320 [hyper,5,135,207] P(i(i(x,n(n(y))),i(x,y))).
368 [hyper,5,135,162] P(i(i(x,i(y,z)),i(x,i(i(z,u),i(y,u))))).
392 [hyper,5,314,148] P(i(i(x,i(y,z)),i(y,i(x,z)))).
403 [hyper,5,207,392] P(i(x,i(n(n(i(x,y))),y))).
405 [hyper,5,162,392] P(i(i(x,y),i(i(z,x),i(z,y)))).
410 [hyper,5,7,392] P(i(i(i(x,i(y,z)),u),i(i(y,i(x,z)),u))).
420 [hyper,5,392,8] P(i(i(x,y),i(i(i(y,x),x),y))).
462 [hyper,5,314,405] P(i(i(x,i(y,z)),i(i(z,u),i(x,i(y,u))))).
474 [hyper,5,405,392] P(i(i(x,i(y,i(z,u))),i(x,i(z,i(y,u))))).
478 [hyper,5,405,217] P(i(i(x,i(n(n(y)),z)),i(x,i(y,z)))).
480 [hyper,5,405,208] P(i(i(x,y),i(x,n(n(y))))).
490 [hyper,5,405,140] P(i(i(x,i(i(y,z),u)),i(x,i(i(n(z),n(y)),u)))).
492 [hyper,5,405,137] P(i(i(x,i(i(y,z),u)),i(x,i(z,u)))).
494 [hyper,5,405,9] P(i(i(x,i(n(y),n(z))),i(x,i(z,y)))).
495 [hyper,5,405,8] P(i(i(x,i(i(y,z),z)),i(x,i(i(z,y),y)))).
533 [hyper,5,314,420] P(i(i(x,i(i(y,z),z)),i(i(z,y),i(x,y)))).
642 [hyper,5,494,480] P(i(i(n(x),y),i(n(y),x))).
643 [hyper,5,494,403] P(i(x,i(y,n(i(x,n(y)))))).
648 [hyper,5,494,151] P(i(i(i(x,y),n(z)),i(z,x))).
656 [hyper,5,244,642] P(i(i(x,y),i(n(y),n(x)))).
665 [hyper,5,642,181] P(i(n(i(x,y)),n(y))).
669 [hyper,5,420,665] P(i(i(i(n(x),n(i(y,x))),n(i(y,x))),n(x))).
742 [hyper,5,405,656] P(i(i(x,i(y,z)),i(x,i(n(z),n(y))))).
754 [hyper,5,7,656] P(i(i(i(n(x),n(y)),z),i(i(y,x),z))).
786 [hyper,5,656,648] P(i(n(i(x,y)),n(i(i(y,z),n(x))))).
809 [hyper,5,405,786] P(i(i(x,n(i(y,z))),i(x,n(i(i(z,u),n(y)))))).
820 [hyper,5,492,742] P(i(i(i(x,y),i(z,u)),i(y,i(n(u),n(z))))).
865 [hyper,5,405,754] P(i(i(x,i(i(n(y),n(z)),u)),i(x,i(i(z,y),u)))).
876 [hyper,5,138,754] P(i(i(i(n(x),n(y)),n(y)),i(i(x,y),n(x)))).
877 [hyper,5,7,754] P(i(i(i(i(x,y),z),u),i(i(i(n(y),n(x)),z),u))).
924 [hyper,5,368,148] P(i(x,i(i(y,z),i(i(x,y),z)))).
952 [hyper,5,7,924] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(z,u))).
1070 [hyper,5,462,643] P(i(i(n(i(x,n(y))),z),i(x,i(y,z)))).
1122 [hyper,5,7,1070] P(i(i(i(x,i(y,z)),u),i(i(n(i(x,n(y))),z),u))).
1174 [hyper,5,474,148] P(i(x,i(y,i(i(x,i(y,z)),z)))).
1183 [hyper,5,742,1174] P(i(x,i(n(i(i(x,i(y,z)),z)),n(y)))).
1271 [hyper,5,392,1183] P(i(n(i(i(x,i(y,z)),z)),i(x,n(y)))).
1344 [hyper,5,642,1271] P(i(n(i(x,n(y))),i(i(x,i(y,z)),z))).
1372 [hyper,5,392,1344] P(i(i(x,i(y,z)),i(n(i(x,n(y))),z))).
1393 [hyper,5,405,1372] P(i(i(x,i(y,i(z,u))),i(x,i(n(i(y,n(z))),u)))).
1480 [hyper,5,7,495] P(i(i(i(x,i(i(y,z),z)),u),i(i(x,i(i(z,y),y)),u))).
1516 [hyper,5,410,533] P(i(i(i(x,y),i(z,y)),i(i(y,x),i(z,x)))).
1570 [hyper,5,405,669] P(i(i(x,i(i(n(y),n(i(z,y))),n(i(z,y)))),i(x,n(y)))).
1632 [hyper,5,820,876] P(i(n(x),i(n(n(y)),n(i(y,x))))).
1663 [hyper,5,478,1632] P(i(n(x),i(y,n(i(y,x))))).
1697 [hyper,5,148,1663] P(i(i(i(n(x),i(y,n(i(y,x)))),z),z)).
1796 [hyper,5,405,1516] P(i(i(x,i(i(y,z),i(u,z))),i(x,i(i(z,y),i(u,y))))).
1807 [hyper,5,7,1516] P(i(i(i(i(x,y),i(z,y)),u),i(i(i(y,x),i(z,x)),u))).
1870 [hyper,5,405,490] P(i(i(x,i(y,i(i(z,u),v))),i(x,i(y,i(i(n(u),n(z)),v))))).
1894 [hyper,5,490,742] P(i(i(i(x,y),i(z,u)),i(i(n(y),n(x)),i(n(u),n(z))))).
1969 [hyper,5,865,494] P(i(i(i(n(x),n(y)),i(n(z),n(u))),i(i(y,x),i(u,z)))).
2005 [hyper,5,405,877] P(i(i(x,i(i(i(y,z),u),v)),i(x,i(i(i(n(z),n(y)),u),v)))).
2060 [hyper,5,405,1122] P(i(i(x,i(i(y,i(z,u)),v)),i(x,i(i(n(i(y,n(z))),u),v)))).
2306 [hyper,5,1570,140] P(i(i(i(i(x,y),y),n(i(x,y))),n(y))).
2317 [hyper,5,405,2306] P(i(i(x,i(i(i(y,z),z),n(i(y,z)))),i(x,n(z)))).
2383 [hyper,5,2317,138] P(i(i(i(i(x,y),y),n(i(y,x))),n(x))).
2395 [hyper,5,405,2383] P(i(i(x,i(i(i(y,z),z),n(i(z,y)))),i(x,n(y)))).
2412 [hyper,5,952,2395] P(i(i(x,y),i(i(y,n(i(y,x))),n(x)))).
2466 [hyper,5,1697,2412] P(i(i(i(x,n(i(x,y))),n(i(i(x,n(i(x,y))),n(y)))),n(n(y)))).
2807 [hyper,5,1807,1969] P(i(i(i(n(x),n(y)),i(n(z),n(y))),i(i(x,y),i(x,z)))).
2862 [hyper,5,405,2807] P(i(i(x,i(i(n(y),n(z)),i(n(u),n(z)))),i(x,i(i(y,z),i(y,u))))).
3140 [hyper,5,320,2466] P(i(i(i(x,n(i(x,y))),n(i(i(x,n(i(x,y))),n(y)))),y)).
3177 [hyper,5,405,3140] P(i(i(x,i(i(y,n(i(y,z))),n(i(i(y,n(i(y,z))),n(z))))),i(x,z))).
3236 [hyper,5,2862,1894] P(i(i(i(x,y),i(x,z)),i(i(y,x),i(y,z)))).
3279 [hyper,5,462,3236] P(i(i(i(x,y),z),i(i(i(u,x),i(u,y)),i(i(x,u),z)))).
3293 [hyper,5,7,3236] P(i(i(i(i(x,y),i(x,z)),u),i(i(i(y,x),i(y,z)),u))).
3306 [hyper,5,1796,3279] P(i(i(i(x,y),i(z,y)),i(i(i(z,y),i(z,x)),i(i(x,z),i(z,x))))).
3447 [hyper,5,405,3293] P(i(i(x,i(i(i(y,z),i(y,u)),v)),i(x,i(i(i(z,y),i(z,u)),v)))).
3547 [hyper,5,3177,809] P(i(i(i(x,n(i(x,y))),n(i(y,x))),y)).
3595 [hyper,5,405,3547] P(i(i(x,i(i(y,n(i(y,z))),n(i(z,y)))),i(x,z))).
3629 [hyper,5,952,3595] P(i(x,i(i(n(i(x,y)),n(i(y,x))),y))).
3707 [hyper,5,865,3629] P(i(x,i(i(i(y,x),i(x,y)),y))).
3859 [hyper,5,392,3707] P(i(i(i(x,y),i(y,x)),i(y,x))).
4001 [hyper,5,405,3859] P(i(i(x,i(i(y,z),i(z,y))),i(x,i(z,y)))).
4043 [hyper,5,405,4001] P(i(i(x,i(y,i(i(z,u),i(u,z)))),i(x,i(y,i(u,z))))).
4195 [hyper,5,4043,3306] P(i(i(i(x,y),i(z,y)),i(i(i(z,y),i(z,x)),i(z,x)))).
4357 [hyper,5,3447,4195] P(i(i(i(x,y),i(z,y)),i(i(i(y,z),i(y,x)),i(z,x)))).
4422 [hyper,5,1807,4357] P(i(i(i(x,y),i(z,y)),i(i(i(x,z),i(x,y)),i(z,y)))).
4503 [hyper,5,165,4422] P(i(i(i(x,i(y,x)),i(i(z,u),i(v,u))),i(i(i(z,v),i(z,u)),i(v,u)))).
4540 [hyper,5,1807,4503] P(i(i(i(i(x,y),y),i(i(z,y),y)),i(i(i(z,x),i(z,y)),i(x,y)))).
4589 [hyper,5,1480,4540] P(i(i(i(i(x,y),y),i(i(y,z),z)),i(i(i(z,x),i(z,y)),i(x,y)))).
4648 [hyper,5,368,4589] P(i(i(i(i(x,y),y),i(i(y,z),z)),i(i(i(x,y),u),i(i(i(z,x),i(z,y)),u)))).
4662 [hyper,5,3236,4648] P(i(i(i(i(x,y),y),i(i(z,x),x)),i(i(i(x,y),y),i(i(i(y,z),i(y,x)),x)))).
4708 [hyper,5,1480,4662] P(i(i(i(i(x,y),y),i(i(x,z),z)),i(i(i(x,y),y),i(i(i(y,z),i(y,x)),x)))).
4748 [hyper,5,3236,4708] P(i(i(i(i(x,y),y),i(i(x,z),z)),i(i(i(x,y),y),i(i(i(z,y),i(z,x)),x)))).
4812 [hyper,5,392,4748] P(i(i(i(x,y),y),i(i(i(i(x,y),y),i(i(x,z),z)),i(i(i(z,y),i(z,x)),x)))).
4847 [hyper,5,474,4812] P(i(i(i(x,y),y),i(i(i(z,y),i(z,x)),i(i(i(i(x,y),y),i(i(x,z),z)),x)))).
4875 [hyper,5,1870,4847] P(i(i(i(x,y),y),i(i(i(z,y),i(z,x)),i(i(n(i(i(x,z),z)),n(i(i(x,y),y))),x)))).
4912 [hyper,5,3447,4875] P(i(i(i(x,y),y),i(i(i(y,z),i(y,x)),i(i(n(i(i(x,z),z)),n(i(i(x,y),y))),x)))).
4959 [hyper,5,2005,4912] P(i(i(i(x,y),y),i(i(i(n(z),n(y)),i(y,x)),i(i(n(i(i(x,z),z)),n(i(i(x,y),y))),x)))).
5021 [hyper,5,392,4959] P(i(i(i(n(x),n(y)),i(y,z)),i(i(i(z,y),y),i(i(n(i(i(z,x),x)),n(i(i(z,y),y))),z)))).
5061 [hyper,5,474,5021] P(i(i(i(n(x),n(y)),i(y,z)),i(i(n(i(i(z,x),x)),n(i(i(z,y),y))),i(i(i(z,y),y),z)))).
5092 [hyper,5,1393,5061] P(i(i(i(n(x),n(y)),i(y,z)),i(n(i(i(n(i(i(z,x),x)),n(i(i(z,y),y))),n(i(i(z,y),y)))),z))).
5154 [hyper,5,392,5092] P(i(n(i(i(n(i(i(x,y),y)),n(i(i(x,z),z))),n(i(i(x,z),z)))),i(i(i(n(y),n(z)),i(z,x)),x))).
5176 [hyper,5,2060,5154] P(i(n(i(i(n(i(i(x,y),y)),n(i(i(x,z),z))),n(i(i(x,z),z)))),i(i(n(i(i(n(y),n(z)),n(z))),x),x))).
5216 [hyper,5,495,5176] P(i(n(i(i(n(i(i(x,y),y)),n(i(i(x,z),z))),n(i(i(x,z),z)))),i(i(x,n(i(i(n(y),n(z)),n(z)))),n(i(i(n(y),n(z)),n(z)))))).
5217 [binary,5216.1,4.1] $F.
------------ end of proof / derivation -------------