Length of proof is 98. Level of proof is 28. ---------------- PROOF ---------------- 3 [] -P(i(i(i(p,n(i(i(n(q),n(r)),n(r)))),n(i(i(n(q),n(r)),n(r)))),n(i(i(n(i(i(p,q),q)),n(i(i(p,r),r))),n(i(i(p,r),r)))))) # label("AK1"). 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). 114 [hyper,5,6,6] P(i(x,i(y,i(z,y)))). 115 [hyper,5,7,7] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 117 [hyper,5,7,6] P(i(i(i(x,y),z),i(y,z))). 118 [hyper,5,7,8] P(i(i(i(i(x,y),y),z),i(i(i(y,x),x),z))). 120 [hyper,5,7,9] P(i(i(i(x,y),z),i(i(n(y),n(x)),z))). 122 [hyper,5,8,114] P(i(i(i(x,i(y,x)),z),z)). 127 [hyper,5,117,9] P(i(n(x),i(x,y))). 128 [hyper,5,117,8] P(i(x,i(i(x,y),y))). 131 [hyper,5,7,127] P(i(i(i(x,y),z),i(n(x),z))). 133 [hyper,5,128,128] P(i(i(i(x,i(i(x,y),y)),z),z)). 135 [hyper,5,7,128] P(i(i(i(i(x,y),y),z),i(x,z))). 144 [hyper,5,117,122] P(i(x,x)). 147 [hyper,5,128,144] P(i(i(i(x,x),y),y)). 153 [hyper,5,128,131] P(i(i(i(i(i(x,y),z),i(n(x),z)),u),u)). 183 [hyper,5,120,147] P(i(i(n(x),n(i(y,y))),x)). 192 [hyper,5,131,183] P(i(n(n(x)),x)). 200 [hyper,5,9,192] P(i(x,n(n(x)))). 235 [hyper,5,135,115] P(i(i(x,y),i(i(z,x),i(z,y)))). 246 [hyper,5,115,135] P(i(i(x,i(y,z)),i(y,i(x,z)))). 247 [hyper,5,115,133] P(i(i(x,y),i(x,i(i(y,z),z)))). 250 [hyper,5,115,7] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 260 [hyper,5,235,200] P(i(i(x,y),i(x,n(n(y))))). 263 [hyper,5,235,153] P(i(i(x,i(i(i(i(y,z),u),i(n(y),u)),v)),i(x,v))). 269 [hyper,5,235,120] P(i(i(x,i(i(y,z),u)),i(x,i(i(n(z),n(y)),u)))). 272 [hyper,5,235,9] P(i(i(x,i(n(y),n(z))),i(x,i(z,y)))). 273 [hyper,5,235,8] P(i(i(x,i(i(y,z),z)),i(x,i(i(z,y),y)))). 299 [hyper,5,235,246] P(i(i(x,i(y,i(z,u))),i(x,i(z,i(y,u))))). 301 [hyper,5,135,246] P(i(x,i(y,i(i(x,i(y,z)),z)))). 304 [hyper,5,7,246] P(i(i(i(x,i(y,z)),u),i(i(y,i(x,z)),u))). 315 [hyper,5,246,247] P(i(x,i(i(x,y),i(i(y,z),z)))). 381 [hyper,5,128,315] P(i(i(i(x,i(i(x,y),i(i(y,z),z))),u),u)). 421 [hyper,5,272,260] P(i(i(n(x),y),i(n(y),x))). 488 [hyper,5,7,250] P(i(i(i(i(i(x,y),z),i(i(u,y),z)),v),i(i(x,u),v))). 496 [hyper,5,250,246] P(i(i(i(i(x,i(y,z)),u),v),i(i(i(y,i(x,z)),u),v))). 499 [hyper,5,250,192] P(i(i(i(n(n(x)),y),z),i(i(x,y),z))). 527 [hyper,5,499,421] P(i(i(x,y),i(n(y),n(x)))). 538 [hyper,5,499,9] P(i(i(x,n(y)),i(y,n(x)))). 545 [hyper,5,250,527] P(i(i(i(i(x,y),z),u),i(i(i(n(y),n(x)),z),u))). 548 [hyper,5,235,527] P(i(i(x,i(y,z)),i(x,i(n(z),n(y))))). 554 [hyper,5,122,527] P(i(n(i(x,y)),n(y))). 557 [hyper,5,7,527] P(i(i(i(n(x),n(y)),z),i(i(y,x),z))). 576 [hyper,5,527,120] P(i(n(i(i(n(x),n(y)),z)),n(i(i(y,x),z)))). 607 [hyper,5,7,538] P(i(i(i(x,n(y)),z),i(i(y,n(x)),z))). 635 [hyper,5,548,301] P(i(x,i(n(i(i(x,i(y,z)),z)),n(y)))). 654 [hyper,5,527,557] P(i(n(i(i(x,y),z)),n(i(i(n(y),n(x)),z)))). 660 [hyper,5,235,557] P(i(i(x,i(i(n(y),n(z)),u)),i(x,i(i(z,y),u)))). 723 [hyper,5,246,635] P(i(n(i(i(x,i(y,z)),z)),i(x,n(y)))). 772 [hyper,5,421,723] P(i(n(i(x,n(y))),i(i(x,i(y,z)),z))). 790 [hyper,5,246,772] P(i(i(x,i(y,z)),i(n(i(x,n(y))),z))). 805 [hyper,5,250,790] P(i(i(i(i(x,i(y,z)),u),v),i(i(i(n(i(x,n(y))),z),u),v))). 859 [hyper,5,250,273] P(i(i(i(i(x,i(i(y,z),z)),u),v),i(i(i(x,i(i(z,y),y)),u),v))). 868 [hyper,5,7,273] P(i(i(i(x,i(i(y,z),z)),u),i(i(x,i(i(z,y),y)),u))). 920 [hyper,5,299,273] P(i(i(x,i(i(y,z),z)),i(i(z,y),i(x,y)))). 1005 [hyper,5,235,576] P(i(i(x,n(i(i(n(y),n(z)),u))),i(x,n(i(i(z,y),u))))). 1017 [hyper,5,235,654] P(i(i(x,n(i(i(y,z),u))),i(x,n(i(i(n(z),n(y)),u))))). 1027 [hyper,5,304,920] P(i(i(i(x,y),i(z,y)),i(i(y,x),i(z,x)))). 1066 [hyper,5,920,120] P(i(i(n(x),n(y)),i(i(i(x,y),n(x)),n(y)))). 1084 [hyper,5,7,1027] P(i(i(i(i(x,y),i(z,y)),u),i(i(i(y,x),i(z,x)),u))). 1090 [hyper,5,557,1066] P(i(i(x,y),i(i(i(y,x),n(y)),n(x)))). 1106 [hyper,5,1066,554] P(i(i(i(i(x,y),y),n(i(x,y))),n(y))). 1116 [hyper,5,381,1090] P(i(i(i(i(i(x,y),i(i(y,z),z)),x),n(i(i(x,y),i(i(y,z),z)))),n(x))). 1123 [hyper,5,246,1090] P(i(i(i(x,y),n(x)),i(i(y,x),n(y)))). 1160 [hyper,5,7,1106] P(i(i(n(x),y),i(i(i(i(z,x),x),n(i(z,x))),y))). 1177 [hyper,5,7,1123] P(i(i(i(i(x,y),n(x)),z),i(i(i(y,x),n(y)),z))). 1203 [hyper,5,269,548] P(i(i(i(x,y),i(z,u)),i(i(n(y),n(x)),i(n(u),n(z))))). 1261 [hyper,5,545,272] P(i(i(i(n(x),n(y)),i(n(z),n(u))),i(i(y,x),i(u,z)))). 1288 [hyper,5,7,660] P(i(i(i(x,i(i(y,z),u)),v),i(i(x,i(i(n(z),n(y)),u)),v))). 1500 [hyper,5,527,868] P(i(n(i(i(x,i(i(y,z),z)),u)),n(i(i(x,i(i(z,y),y)),u)))). 1553 [hyper,5,7,1005] P(i(i(i(x,n(i(i(y,z),u))),v),i(i(x,n(i(i(n(z),n(y)),u))),v))). 1568 [hyper,5,250,1017] 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))). 1698 [hyper,5,1084,1261] P(i(i(i(n(x),n(y)),i(n(z),n(y))),i(i(x,y),i(x,z)))). 1730 [hyper,5,235,1698] P(i(i(x,i(i(n(y),n(z)),i(n(u),n(z)))),i(x,i(i(y,z),i(y,u))))). 1821 [hyper,5,235,1500] P(i(i(x,n(i(i(y,i(i(z,u),u)),v))),i(x,n(i(i(y,i(i(u,z),z)),v))))). 1833 [hyper,5,859,488] P(i(i(i(i(i(x,y),y),i(i(y,z),z)),u),i(i(x,z),u))). 1858 [hyper,5,247,1833] P(i(i(i(i(i(x,y),y),i(i(y,z),z)),u),i(i(i(i(x,z),u),v),v))). 1916 [hyper,5,1730,1203] P(i(i(i(x,y),i(x,z)),i(i(y,x),i(y,z)))). 1943 [hyper,5,263,1916] P(i(i(i(i(n(x),y),i(i(x,z),y)),i(i(n(x),y),u)),i(i(i(x,z),y),u))). 1945 [hyper,5,250,1916] P(i(i(i(i(i(x,y),i(x,z)),u),v),i(i(i(i(y,x),i(y,z)),u),v))). 1956 [hyper,5,548,1858] P(i(i(i(i(i(x,y),y),i(i(y,z),z)),u),i(n(v),n(i(i(i(x,z),u),v))))). 2012 [hyper,5,235,1116] P(i(i(x,i(i(i(i(y,z),i(i(z,u),u)),y),n(i(i(y,z),i(i(z,u),u))))),i(x,n(y)))). 2017 [hyper,5,496,1943] P(i(i(i(i(x,y),i(i(n(x),z),z)),i(i(n(x),z),u)),i(i(i(x,y),z),u))). 2020 [hyper,5,246,1956] P(i(n(x),i(i(i(i(i(y,z),z),i(i(z,u),u)),v),n(i(i(i(y,u),v),x))))). 2046 [hyper,5,269,2020] P(i(n(x),i(i(n(y),n(i(i(i(z,u),u),i(i(u,v),v)))),n(i(i(i(z,v),y),x))))). 2051 [hyper,5,1160,2046] P(i(i(i(i(x,y),y),n(i(x,y))),i(i(n(z),n(i(i(i(u,v),v),i(i(v,w),w)))),n(i(i(i(u,w),z),y))))). 2052 [hyper,5,7,2012] P(i(i(i(x,n(y)),z),i(i(x,i(i(i(i(y,u),i(i(u,v),v)),y),n(i(i(y,u),i(i(u,v),v))))),z))). 2053 [hyper,5,2052,2051] P(i(i(i(i(x,y),y),i(i(i(i(i(x,y),z),i(i(z,u),u)),i(x,y)),n(i(i(i(x,y),z),i(i(z,u),u))))),i(i(n(v),n(i(i(i(w,v6),v6),i(i(v6,v7),v7)))),n(i(i(i(w,v7),v),y))))). 2054 [hyper,5,1288,2053] P(i(i(i(i(x,y),y),i(i(n(i(x,y)),n(i(i(i(x,y),z),i(i(z,u),u)))),n(i(i(i(x,y),z),i(i(z,u),u))))),i(i(n(v),n(i(i(i(w,v6),v6),i(i(v6,v7),v7)))),n(i(i(i(w,v7),v),y))))). 2055 [hyper,5,2017,2054] P(i(i(i(i(x,y),y),n(i(i(i(x,y),y),i(i(y,z),z)))),n(i(i(i(x,z),i(x,y)),y)))). 2056 [hyper,5,607,2055] P(i(i(i(i(i(x,y),y),i(i(y,z),z)),n(i(i(x,y),y))),n(i(i(i(x,z),i(x,y)),y)))). 2058 [hyper,5,1177,2056] P(i(i(i(i(i(x,y),y),i(i(z,x),x)),n(i(i(x,y),y))),n(i(i(i(z,y),i(z,x)),x)))). 2059 [hyper,5,538,2058] P(i(i(i(i(x,y),i(x,z)),z),n(i(i(i(i(z,y),y),i(i(x,z),z)),n(i(i(z,y),y)))))). 2062 [hyper,5,1821,2059] P(i(i(i(i(x,y),i(x,z)),z),n(i(i(i(i(z,y),y),i(i(z,x),x)),n(i(i(z,y),y)))))). 2064 [hyper,5,1945,2062] P(i(i(i(i(x,y),i(x,z)),z),n(i(i(i(i(z,x),x),i(i(z,y),y)),n(i(i(z,x),x)))))). 2066 [hyper,5,805,2064] P(i(i(i(n(i(i(x,y),n(x))),z),z),n(i(i(i(i(z,x),x),i(i(z,y),y)),n(i(i(z,x),x)))))). 2067 [hyper,5,118,2066] P(i(i(i(x,n(i(i(y,z),n(y)))),n(i(i(y,z),n(y)))),n(i(i(i(i(x,y),y),i(i(x,z),z)),n(i(i(x,y),y)))))). 2068 [hyper,5,1017,2067] P(i(i(i(x,n(i(i(y,z),n(y)))),n(i(i(y,z),n(y)))),n(i(i(n(i(i(x,z),z)),n(i(i(x,y),y))),n(i(i(x,y),y)))))). 2069 [hyper,5,1553,2068] P(i(i(i(x,n(i(i(y,z),n(y)))),n(i(i(n(z),n(y)),n(y)))),n(i(i(n(i(i(x,z),z)),n(i(i(x,y),y))),n(i(i(x,y),y)))))). 2071 [hyper,5,1568,2069] P(i(i(i(x,n(i(i(n(y),n(z)),n(z)))),n(i(i(n(y),n(z)),n(z)))),n(i(i(n(i(i(x,y),y)),n(i(i(x,z),z))),n(i(i(x,z),z)))))). 2072 [binary,2071.1,3.1] $F. ------------ end of proof / derivation -------------