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