Length of proof is 140. Level of proof is 43. ---------------- PROOF ---------------- 2 [] -P(i(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)))),n(i(i(n(p),n(i(i(q,r),r))),n(i(i(q,r),r)))))) # label("KA2"). 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). 154 [hyper,5,6,6] P(i(x,i(y,i(z,y)))). 155 [hyper,5,7,7] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 157 [hyper,5,7,6] P(i(i(i(x,y),z),i(y,z))). 158 [hyper,5,7,8] P(i(i(i(i(x,y),y),z),i(i(i(y,x),x),z))). 160 [hyper,5,7,9] P(i(i(i(x,y),z),i(i(n(y),n(x)),z))). 162 [hyper,5,8,154] P(i(i(i(x,i(y,x)),z),z)). 163 [hyper,5,7,154] P(i(i(i(x,i(y,x)),z),i(u,z))). 165 [hyper,5,7,157] P(i(i(i(x,y),z),i(i(i(u,x),y),z))). 167 [hyper,5,157,9] P(i(n(x),i(x,y))). 168 [hyper,5,157,8] P(i(x,i(i(x,y),y))). 171 [hyper,5,7,167] P(i(i(i(x,y),z),i(n(x),z))). 184 [hyper,5,157,162] P(i(x,x)). 187 [hyper,5,168,184] P(i(i(i(x,x),y),y)). 188 [hyper,5,6,184] P(i(x,i(y,y))). 190 [hyper,5,7,188] P(i(i(i(x,x),y),i(z,y))). 196 [hyper,5,7,190] P(i(i(i(x,y),z),i(i(i(u,u),y),z))). 225 [hyper,5,160,187] P(i(i(n(x),n(i(y,y))),x)). 234 [hyper,5,171,225] P(i(n(n(x)),x)). 242 [hyper,5,9,234] P(i(x,n(n(x)))). 243 [hyper,5,7,234] P(i(i(x,y),i(n(n(x)),y))). 253 [hyper,5,7,242] P(i(i(n(n(x)),y),i(x,y))). 277 [hyper,5,7,243] P(i(i(i(n(n(x)),y),z),i(i(x,y),z))). 298 [hyper,5,7,253] P(i(i(i(x,y),z),i(i(n(n(x)),y),z))). 310 [hyper,5,7,165] P(i(i(i(i(i(x,y),z),u),v),i(i(i(y,z),u),v))). 365 [hyper,5,7,298] P(i(i(i(i(n(n(x)),y),z),u),i(i(i(x,y),z),u))). 392 [hyper,5,155,155] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 405 [hyper,5,155,7] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 417 [hyper,5,7,158] P(i(i(i(i(i(x,y),y),z),u),i(i(i(i(y,x),x),z),u))). 450 [hyper,5,392,168] P(i(i(x,i(y,z)),i(y,i(x,z)))). 468 [hyper,5,7,450] P(i(i(i(x,i(y,z)),u),i(i(y,i(x,z)),u))). 476 [hyper,5,450,8] P(i(i(x,y),i(i(i(y,x),x),y))). 477 [hyper,5,450,7] P(i(i(x,y),i(i(z,x),i(z,y)))). 479 [hyper,5,392,476] P(i(i(x,i(i(y,z),z)),i(i(z,y),i(x,y)))). 491 [hyper,5,7,476] P(i(i(i(i(i(x,y),y),x),z),i(i(y,x),z))). 520 [hyper,5,392,477] P(i(i(x,i(y,z)),i(i(z,u),i(x,i(y,u))))). 534 [hyper,5,477,450] P(i(i(x,i(y,i(z,u))),i(x,i(z,i(y,u))))). 540 [hyper,5,477,242] P(i(i(x,y),i(x,n(n(y))))). 541 [hyper,5,477,234] P(i(i(x,n(n(y))),i(x,y))). 555 [hyper,5,477,9] P(i(i(x,i(n(y),n(z))),i(x,i(z,y)))). 556 [hyper,5,477,8] P(i(i(x,i(i(y,z),z)),i(x,i(i(z,y),y)))). 624 [hyper,5,555,540] P(i(i(n(x),y),i(n(y),x))). 636 [hyper,5,277,624] P(i(i(x,y),i(n(y),n(x)))). 644 [hyper,5,7,624] P(i(i(i(n(x),y),z),i(i(n(y),x),z))). 650 [hyper,5,477,636] P(i(i(x,i(y,z)),i(x,i(n(z),n(y))))). 663 [hyper,5,7,636] P(i(i(i(n(x),n(y)),z),i(i(y,x),z))). 667 [hyper,5,636,541] P(i(n(i(x,y)),n(i(x,n(n(y)))))). 673 [hyper,5,636,298] P(i(n(i(i(n(n(x)),y),z)),n(i(i(x,y),z)))). 674 [hyper,5,636,277] P(i(n(i(i(x,y),z)),n(i(i(n(n(x)),y),z)))). 687 [hyper,5,636,160] P(i(n(i(i(n(x),n(y)),z)),n(i(i(y,x),z)))). 691 [hyper,5,636,9] P(i(n(i(x,y)),n(i(n(y),n(x))))). 692 [hyper,5,636,8] P(i(n(i(i(x,y),y)),n(i(i(y,x),x)))). 701 [hyper,5,7,667] P(i(i(n(i(x,n(n(y)))),z),i(n(i(x,y)),z))). 705 [hyper,5,477,691] P(i(i(x,n(i(y,z))),i(x,n(i(n(z),n(y)))))). 780 [hyper,5,636,663] P(i(n(i(i(x,y),z)),n(i(i(n(y),n(x)),z)))). 795 [hyper,5,7,663] P(i(i(i(i(x,y),z),u),i(i(i(n(y),n(x)),z),u))). 802 [hyper,5,477,692] P(i(i(x,n(i(i(y,z),z))),i(x,n(i(i(z,y),y))))). 836 [hyper,5,405,663] P(i(i(i(i(i(n(x),n(y)),z),u),v),i(i(i(i(y,x),z),u),v))). 844 [hyper,5,405,450] P(i(i(i(i(x,i(y,z)),u),v),i(i(i(y,i(x,z)),u),v))). 849 [hyper,5,405,196] P(i(i(i(i(i(x,y),z),u),v),i(i(i(i(i(w,w),y),z),u),v))). 857 [hyper,5,405,158] P(i(i(i(i(i(i(x,y),y),z),u),v),i(i(i(i(i(y,x),x),z),u),v))). 945 [hyper,5,479,160] P(i(i(n(x),n(y)),i(i(i(x,y),n(x)),n(y)))). 1012 [hyper,5,520,479] P(i(i(i(x,y),z),i(i(x,i(i(y,u),u)),i(i(u,y),z)))). 1079 [hyper,5,534,168] P(i(x,i(y,i(i(x,i(y,z)),z)))). 1088 [hyper,5,650,1079] P(i(x,i(n(i(i(x,i(y,z)),z)),n(y)))). 1177 [hyper,5,450,1088] P(i(n(i(i(x,i(y,z)),z)),i(x,n(y)))). 1250 [hyper,5,624,1177] P(i(n(i(x,n(y))),i(i(x,i(y,z)),z))). 1271 [hyper,5,450,1250] P(i(i(x,i(y,z)),i(n(i(x,n(y))),z))). 1305 [hyper,5,163,1271] P(i(x,i(n(i(y,n(z))),y))). 1404 [hyper,5,556,644] P(i(i(i(n(x),y),x),i(i(x,n(y)),n(y)))). 1440 [hyper,5,7,1404] P(i(i(i(i(x,n(y)),n(y)),z),i(i(i(n(x),y),x),z))). 1446 [hyper,5,477,673] P(i(i(x,n(i(i(n(n(y)),z),u))),i(x,n(i(i(y,z),u))))). 1458 [hyper,5,477,674] P(i(i(x,n(i(i(y,z),u))),i(x,n(i(i(n(n(y)),z),u))))). 1470 [hyper,5,477,687] P(i(i(x,n(i(i(n(y),n(z)),u))),i(x,n(i(i(z,y),u))))). 1476 [hyper,5,7,687] P(i(i(n(i(i(x,y),z)),u),i(n(i(i(n(y),n(x)),z)),u))). 1489 [hyper,5,477,701] P(i(i(x,i(n(i(y,n(n(z)))),u)),i(x,i(n(i(y,z)),u)))). 1541 [hyper,5,7,705] P(i(i(i(x,n(i(n(y),n(z)))),u),i(i(x,n(i(z,y))),u))). 1557 [hyper,5,477,780] P(i(i(x,n(i(i(y,z),u))),i(x,n(i(i(n(z),n(y)),u))))). 1568 [hyper,5,663,945] P(i(i(x,y),i(i(i(y,x),n(y)),n(x)))). 1744 [hyper,5,477,365] P(i(i(x,i(i(i(n(n(y)),z),u),v)),i(x,i(i(i(y,z),u),v)))). 1804 [hyper,5,405,795] P(i(i(i(i(i(i(x,y),z),u),v),w),i(i(i(i(i(n(y),n(x)),z),u),v),w))). 1880 [hyper,5,7,802] P(i(i(i(x,n(i(i(y,z),z))),u),i(i(x,n(i(i(z,y),y))),u))). 1902 [hyper,5,477,1440] P(i(i(x,i(i(i(y,n(z)),n(z)),u)),i(x,i(i(i(n(y),z),y),u)))). 1960 [hyper,5,405,417] P(i(i(i(i(i(i(i(x,y),y),z),u),v),w),i(i(i(i(i(i(y,x),x),z),u),v),w))). 2020 [hyper,5,405,844] P(i(i(i(i(i(i(x,i(y,z)),u),v),w),v6),i(i(i(i(i(y,i(x,z)),u),v),w),v6))). 2101 [hyper,5,158,1012] P(i(i(i(x,y),y),i(i(y,i(i(x,z),z)),i(i(z,x),x)))). 2169 [hyper,5,405,1446] P(i(i(i(i(x,n(i(i(n(n(y)),z),u))),v),w),i(i(i(x,n(i(i(y,z),u))),v),w))). 2227 [hyper,5,7,1458] P(i(i(i(x,n(i(i(n(n(y)),z),u))),v),i(i(x,n(i(i(y,z),u))),v))). 2270 [hyper,5,7,1470] P(i(i(i(x,n(i(i(y,z),u))),v),i(i(x,n(i(i(n(z),n(y)),u))),v))). 2295 [hyper,5,405,1476] P(i(i(i(i(n(i(i(x,y),z)),u),v),w),i(i(i(n(i(i(n(y),n(x)),z)),u),v),w))). 2352 [hyper,5,1489,1305] P(i(x,i(n(i(y,z)),y))). 2384 [hyper,5,477,1541] P(i(i(x,i(i(y,n(i(n(z),n(u)))),v)),i(x,i(i(y,n(i(u,z))),v)))). 2453 [hyper,5,405,1557] 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))). 2495 [hyper,5,392,2101] P(i(i(x,i(y,i(i(z,u),u))),i(i(i(z,y),y),i(x,i(i(u,z),z))))). 2525 [hyper,5,477,836] P(i(i(x,i(i(i(i(n(y),n(z)),u),v),w)),i(x,i(i(i(i(z,y),u),v),w)))). 2757 [hyper,5,477,1880] P(i(i(x,i(i(y,n(i(i(z,u),u))),v)),i(x,i(i(y,n(i(i(u,z),z))),v)))). 2904 [hyper,5,477,857] P(i(i(x,i(i(i(i(i(y,z),z),u),v),w)),i(x,i(i(i(i(i(z,y),y),u),v),w)))). 2991 [hyper,5,405,2227] P(i(i(i(i(i(x,n(i(i(n(n(y)),z),u))),v),w),v6),i(i(i(i(x,n(i(i(y,z),u))),v),w),v6))). 3221 [hyper,5,468,2495] P(i(i(x,i(y,i(i(z,u),u))),i(i(i(z,x),x),i(y,i(i(u,z),z))))). 3359 [hyper,5,3221,1012] P(i(i(i(x,i(i(y,z),z)),i(i(y,z),z)),i(i(y,i(i(z,x),x)),i(i(z,x),x)))). 3713 [hyper,5,1960,310] P(i(i(i(i(i(i(x,y),y),z),u),v),i(i(i(x,z),u),v))). 4086 [hyper,5,405,2295] P(i(i(i(i(i(i(n(i(i(x,y),z)),u),v),w),v6),v7),i(i(i(i(i(n(i(i(n(y),n(x)),z)),u),v),w),v6),v7))). 4191 [hyper,5,405,2453] P(i(i(i(i(i(i(x,n(i(i(y,z),u))),v),w),v6),v7),i(i(i(i(i(x,n(i(i(n(z),n(y)),u))),v),w),v6),v7))). 4384 [hyper,5,158,3359] P(i(i(i(i(i(x,y),y),z),z),i(i(x,i(i(y,z),z)),i(i(y,z),z)))). 4412 [hyper,5,479,4384] P(i(i(i(i(x,y),y),z),i(i(i(i(i(z,x),x),y),y),z))). 4431 [hyper,5,2904,4412] P(i(i(i(i(x,y),y),z),i(i(i(i(i(x,z),z),y),y),z))). 4587 [hyper,5,7,4431] P(i(i(i(i(i(i(i(x,y),y),z),z),y),u),i(i(i(i(x,z),z),y),u))). 4702 [hyper,5,4587,849] P(i(i(i(i(x,y),y),z),i(i(i(i(i(u,u),z),y),y),z))). 4727 [hyper,5,3713,4702] P(i(i(i(x,y),z),i(i(i(i(i(u,u),z),y),y),z))). 5197 [hyper,5,7,2352] P(i(i(i(n(i(x,y)),x),z),i(u,z))). 5230 [hyper,5,405,5197] P(i(i(i(i(i(n(i(x,y)),x),z),u),v),i(i(i(w,z),u),v))). 5315 [hyper,5,405,5230] P(i(i(i(i(i(i(i(n(i(x,y)),x),z),u),v),w),v6),i(i(i(i(i(v7,z),u),v),w),v6))). 5446 [hyper,5,5315,3713] P(i(i(i(i(i(x,y),z),u),v),i(i(i(n(i(y,w)),z),u),v))). 5508 [hyper,5,4587,5446] P(i(i(i(i(x,y),y),z),i(i(i(n(i(z,u)),y),y),z))). 5648 [hyper,5,491,5508] P(i(i(x,y),i(i(i(n(i(y,z)),x),x),y))). 5719 [hyper,5,1902,5648] P(i(i(n(x),y),i(i(i(n(n(i(y,z))),x),n(i(y,z))),y))). 5857 [hyper,5,1744,5719] P(i(i(n(x),y),i(i(i(i(y,z),x),n(i(y,z))),y))). 5911 [hyper,5,2525,5857] P(i(i(n(x),n(y)),i(i(i(i(z,y),x),n(i(n(y),n(z)))),n(y)))). 5967 [hyper,5,2384,5911] P(i(i(n(x),n(y)),i(i(i(i(z,y),x),n(i(z,y))),n(y)))). 6026 [hyper,5,663,5967] P(i(i(x,y),i(i(i(i(z,x),y),n(i(z,x))),n(x)))). 6064 [hyper,5,2904,6026] P(i(i(x,y),i(i(i(i(i(x,z),z),y),n(i(i(z,x),x))),n(x)))). 6099 [hyper,5,450,6026] P(i(i(i(i(x,y),z),n(i(x,y))),i(i(y,z),n(y)))). 6227 [hyper,5,1568,6099] P(i(i(i(i(i(x,y),n(x)),i(i(i(z,x),y),n(i(z,x)))),n(i(i(x,y),n(x)))),n(i(i(i(z,x),y),n(i(z,x)))))). 6269 [hyper,5,2757,6064] P(i(i(x,y),i(i(i(i(i(x,z),z),y),n(i(i(x,z),z))),n(x)))). 6439 [hyper,5,7,6269] P(i(i(i(i(i(i(i(x,y),y),z),n(i(i(x,y),y))),n(x)),u),i(i(x,z),u))). 6562 [hyper,5,477,6439] P(i(i(x,i(i(i(i(i(i(y,z),z),u),n(i(i(y,z),z))),n(y)),v)),i(x,i(i(y,u),v)))). 6660 [hyper,5,405,6562] P(i(i(i(i(x,i(i(i(i(i(i(y,z),z),u),n(i(i(y,z),z))),n(y)),v)),w),v6),i(i(i(x,i(i(y,u),v)),w),v6))). 6724 [hyper,5,1557,6227] P(i(i(i(i(i(x,y),n(x)),i(i(i(z,x),y),n(i(z,x)))),n(i(i(x,y),n(x)))),n(i(i(n(y),n(i(z,x))),n(i(z,x)))))). 6782 [hyper,5,405,6660] P(i(i(i(i(i(i(x,i(i(i(i(i(i(y,z),z),u),n(i(i(y,z),z))),n(y)),v)),w),v6),v7),v8),i(i(i(i(i(x,i(i(y,u),v)),w),v6),v7),v8))). 6859 [hyper,5,2270,6724] P(i(i(i(i(i(x,y),n(x)),i(i(i(z,x),y),n(i(z,x)))),n(i(i(n(y),n(x)),n(x)))),n(i(i(n(y),n(i(z,x))),n(i(z,x)))))). 7128 [hyper,5,4727,6859] P(i(i(i(i(i(x,x),n(i(i(n(y),n(i(z,u))),n(i(z,u))))),n(i(i(n(y),n(u)),n(u)))),n(i(i(n(y),n(u)),n(u)))),n(i(i(n(y),n(i(z,u))),n(i(z,u)))))). 7170 [hyper,5,2991,7128] P(i(i(i(i(i(x,x),n(i(i(y,n(i(z,u))),n(i(z,u))))),n(i(i(n(n(y)),n(u)),n(u)))),n(i(i(n(n(y)),n(u)),n(u)))),n(i(i(n(n(y)),n(i(z,u))),n(i(z,u)))))). 7174 [hyper,5,2169,7170] P(i(i(i(i(i(x,x),n(i(i(y,n(i(z,u))),n(i(z,u))))),n(i(i(y,n(u)),n(u)))),n(i(i(n(n(y)),n(u)),n(u)))),n(i(i(n(n(y)),n(i(z,u))),n(i(z,u)))))). 7177 [hyper,5,2227,7174] P(i(i(i(i(i(x,x),n(i(i(y,n(i(z,u))),n(i(z,u))))),n(i(i(y,n(u)),n(u)))),n(i(i(y,n(u)),n(u)))),n(i(i(n(n(y)),n(i(z,u))),n(i(z,u)))))). 7185 [hyper,5,1446,7177] P(i(i(i(i(i(x,x),n(i(i(y,n(i(z,u))),n(i(z,u))))),n(i(i(y,n(u)),n(u)))),n(i(i(y,n(u)),n(u)))),n(i(i(y,n(i(z,u))),n(i(z,u)))))). 7193 [hyper,5,2020,7185] P(i(i(i(i(i(x,i(i(x,y),y)),n(i(i(z,n(i(u,v))),n(i(u,v))))),n(i(i(z,n(v)),n(v)))),n(i(i(z,n(v)),n(v)))),n(i(i(z,n(i(u,v))),n(i(u,v)))))). 7209 [hyper,5,6782,7193] P(i(i(i(i(i(i(i(i(i(x,y),y),z),n(i(i(x,y),y))),i(i(x,z),n(x))),n(i(i(u,n(i(v,w))),n(i(v,w))))),n(i(i(u,n(w)),n(w)))),n(i(i(u,n(w)),n(w)))),n(i(i(u,n(i(v,w))),n(i(v,w)))))). 7212 [hyper,5,1804,7209] P(i(i(i(i(i(n(i(i(x,y),n(x))),n(i(i(i(i(x,z),z),y),n(i(i(x,z),z))))),n(i(i(u,n(i(v,w))),n(i(v,w))))),n(i(i(u,n(w)),n(w)))),n(i(i(u,n(w)),n(w)))),n(i(i(u,n(i(v,w))),n(i(v,w)))))). 7213 [hyper,5,4086,7212] P(i(i(i(i(i(n(i(i(n(x),n(y)),n(y))),n(i(i(i(i(y,z),z),x),n(i(i(y,z),z))))),n(i(i(u,n(i(v,w))),n(i(v,w))))),n(i(i(u,n(w)),n(w)))),n(i(i(u,n(w)),n(w)))),n(i(i(u,n(i(v,w))),n(i(v,w)))))). 7214 [hyper,5,4191,7213] P(i(i(i(i(i(n(i(i(n(x),n(y)),n(y))),n(i(i(n(x),n(i(i(y,z),z))),n(i(i(y,z),z))))),n(i(i(u,n(i(v,w))),n(i(v,w))))),n(i(i(u,n(w)),n(w)))),n(i(i(u,n(w)),n(w)))),n(i(i(u,n(i(v,w))),n(i(v,w)))))). 7215 [hyper,5,3713,7214] P(i(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)))),n(i(i(n(x),n(i(i(y,z),z))),n(i(i(y,z),z)))))). 7216 [binary,7215.1,2.1] $F. ------------ end of proof / derivation -------------