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 -------------