Length of proof is 74. Level of proof is 18. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 2 [] -P(i(i(i(cx,i(cy,cx)),i(i(i(i(i(i(i(i(i(cz,cu),i(i(cv,cz),i(cv,cu))),i(i(cw,i(cv6,cw)),cv7)),cv7),i(i(i(i(cv8,cv9),cv9),i(i(cv9,cv8),cv8)),cv10)),cv10),i(i(i(i(cv11,cv12),i(cv12,cv11)),i(cv12,cv11)),cv13)),cv13),i(i(cv14,i(cv15,cv14)),cv16))),cv16)). 3 [] P(i(x,i(y,x))) # label("MV 1"). 4 [] P(i(i(x,y),i(i(y,z),i(x,z)))) # label("MV 2"). 5 [] P(i(i(i(x,y),y),i(i(y,x),x))) # label("MV 3"). 6 [] P(i(i(i(x,y),i(y,x)),i(y,x))) # label("MV 5"). 81 [hyper,1,3,3] P(i(x,i(y,i(z,y)))) # label("Hint 7(88)"). 82 [hyper,1,4,4] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))) # label("Hint 8(89)"). 83 [hyper,1,4,3] P(i(i(i(x,y),z),i(y,z))) # label("Hint 9(90)"). 84 [hyper,1,83,5] P(i(x,i(i(x,y),y))) # label("Hint 10(91)"). 85 [hyper,1,5,81] P(i(i(i(x,i(y,x)),z),z)) # label("Hint 11(92)"). 86 [hyper,1,4,84] P(i(i(i(i(x,y),y),z),i(x,z))) # label("Hint 12(93)"). 87 [hyper,1,84,5] P(i(i(i(i(i(x,y),y),i(i(y,x),x)),z),z)) # label("Hint 13(94)"). 88 [hyper,1,83,85] P(i(x,x)) # label("Hint 14(95)"). 89 [hyper,1,82,85] P(i(i(x,y),i(x,i(z,y)))) # label("Hint 23(104)"). 90 [hyper,1,4,85] P(i(i(x,y),i(i(i(z,i(u,z)),x),y))) # label("Hint 15(96)"). 91 [hyper,1,84,88] P(i(i(i(x,x),y),y)) # label("Hint 16(97)"). 92 [hyper,1,84,91] P(i(i(i(i(i(x,x),y),y),z),z)) # label("Hint 17(98)"). 93 [hyper,1,4,89] P(i(i(i(x,i(y,z)),u),i(i(x,z),u))) # label("Hint 24(105)"). 94 [hyper,1,4,86] P(i(i(i(x,y),z),i(i(i(i(x,u),u),y),z))) # label("Hint 19(100)"). 95 [hyper,1,86,82] P(i(i(x,y),i(i(z,x),i(z,y)))) # label("Hint 21(102)"). 96 [hyper,1,82,92] P(i(i(x,i(i(y,y),z)),i(x,z))) # label("Hint 22(103)"). 97 [hyper,1,4,92] P(i(i(x,y),i(i(i(i(i(z,z),u),u),x),y))) # label("Hint 20(101)"). 98 [hyper,1,84,95] P(i(i(i(i(x,y),i(i(z,x),i(z,y))),u),u)) # label("Hint 25(106)"). 99 [hyper,1,95,85] P(i(i(x,i(i(y,i(z,y)),u)),i(x,u))) # label("Hint 26(107)"). 100 [hyper,1,4,96] P(i(i(i(x,y),z),i(i(x,i(i(u,u),y)),z))) # label("Hint 27(108)"). 101 [hyper,1,96,92] P(i(i(i(i(i(x,x),y),y),i(i(z,z),u)),u)) # label("Hint 28(109)"). 102 [hyper,1,95,93] P(i(i(x,i(i(y,i(z,u)),v)),i(x,i(i(y,u),v)))) # label("Hint 29(110)"). 103 [hyper,1,4,99] P(i(i(i(x,y),z),i(i(x,i(i(u,i(v,u)),y)),z))) # label("Hint 30(111)"). 104 [hyper,1,4,87] P(i(i(x,y),i(i(i(i(i(z,u),u),i(i(u,z),z)),x),y))) # label("Hint 31(112)"). 105 [hyper,1,4,94] P(i(i(i(i(i(i(x,y),y),z),u),v),i(i(i(x,z),u),v))) # label("Hint 33(114)"). 106 [hyper,1,4,97] P(i(i(i(i(i(i(i(x,x),y),y),z),u),v),i(i(z,u),v))) # label("Hint 34(115)"). 107 [hyper,1,4,98] P(i(i(x,y),i(i(i(i(z,u),i(i(v,z),i(v,u))),x),y))) # label("Hint 35(116)"). 108 [hyper,1,4,100] P(i(i(i(i(x,i(i(y,y),z)),u),v),i(i(i(x,z),u),v))) # label("Hint 36(117)"). 109 [hyper,1,95,102] P(i(i(x,i(y,i(i(z,i(u,v)),w))),i(x,i(y,i(i(z,v),w))))) # label("Hint 37(118)"). 110 [hyper,1,4,103] P(i(i(i(i(x,i(i(y,i(z,y)),u)),v),w),i(i(i(x,u),v),w))) # label("Hint 38(119)"). 111 [hyper,1,95,104] P(i(i(x,i(y,z)),i(x,i(i(i(i(i(u,v),v),i(i(v,u),u)),y),z)))) # label("Hint 39(120)"). 112 [hyper,1,4,105] P(i(i(i(i(i(x,y),z),u),v),i(i(i(i(i(i(x,w),w),y),z),u),v))) # label("Hint 41(122)"). 113 [hyper,1,4,106] P(i(i(i(i(x,y),z),u),i(i(i(i(i(i(i(v,v),w),w),x),y),z),u))) # label("Hint 42(123)"). 114 [hyper,1,4,107] P(i(i(i(i(i(i(x,y),i(i(z,x),i(z,y))),u),v),w),i(i(u,v),w))) # label("Hint 43(124)"). 115 [hyper,1,4,108] P(i(i(i(i(i(x,y),z),u),v),i(i(i(i(x,i(i(w,w),y)),z),u),v))) # label("Hint 44(125)"). 116 [hyper,1,4,109] P(i(i(i(x,i(y,i(i(z,u),v))),w),i(i(x,i(y,i(i(z,i(v6,u)),v))),w))) # label("Hint 45(126)"). 117 [hyper,1,4,110] P(i(i(i(i(i(x,y),z),u),v),i(i(i(i(x,i(i(w,i(v6,w)),y)),z),u),v))) # label("Hint 46(127)"). 118 [hyper,1,4,111] P(i(i(i(x,i(i(i(i(i(y,z),z),i(i(z,y),y)),u),v)),w),i(i(x,i(u,v)),w))) # label("Hint 47(128)"). 119 [hyper,1,4,112] P(i(i(i(i(i(i(i(i(x,y),y),z),u),v),w),v6),i(i(i(i(i(x,z),u),v),w),v6))) # label("Hint 49(130)"). 120 [hyper,1,113,101] P(i(i(i(i(i(i(i(x,x),y),y),i(i(z,z),u)),u),i(i(v,v),w)),w)) # label("Hint 50(131)"). 121 [hyper,1,4,114] P(i(i(i(i(x,y),z),u),i(i(i(i(i(i(v,w),i(i(v6,v),i(v6,w))),x),y),z),u))) # label("Hint 51(132)"). 122 [hyper,1,4,115] P(i(i(i(i(i(i(x,i(i(y,y),z)),u),v),w),v6),i(i(i(i(i(x,z),u),v),w),v6))) # label("Hint 52(133)"). 123 [hyper,1,4,117] P(i(i(i(i(i(i(x,i(i(y,i(z,y)),u)),v),w),v6),v7),i(i(i(i(i(x,u),v),w),v6),v7))) # label("Hint 53(134)"). 124 [hyper,1,4,118] P(i(i(i(i(x,i(y,z)),u),v),i(i(i(x,i(i(i(i(i(w,v6),v6),i(i(v6,w),w)),y),z)),u),v))) # label("Hint 54(135)"). 125 [hyper,1,4,119] P(i(i(i(i(i(i(i(x,y),z),u),v),w),v6),i(i(i(i(i(i(i(i(x,v7),v7),y),z),u),v),w),v6))) # label("Hint 56(137)"). 126 [hyper,1,4,121] P(i(i(i(i(i(i(i(i(x,y),i(i(z,x),i(z,y))),u),v),w),v6),v7),i(i(i(i(u,v),w),v6),v7))) # label("Hint 57(138)"). 127 [hyper,1,122,120] P(i(i(i(i(i(i(i(x,x),i(i(y,y),z)),z),i(i(u,u),v)),v),i(i(w,w),v6)),v6)) # label("Hint 58(139)"). 128 [hyper,1,4,123] P(i(i(i(i(i(i(i(x,y),z),u),v),w),v6),i(i(i(i(i(i(x,i(i(v7,i(v8,v7)),y)),z),u),v),w),v6))) # label("Hint 59(140)"). 129 [hyper,1,4,124] P(i(i(i(i(i(x,i(i(i(i(i(y,z),z),i(i(z,y),y)),u),v)),w),v6),v7),i(i(i(i(x,i(u,v)),w),v6),v7))) # label("Hint 60(141)"). 130 [hyper,1,125,127] P(i(i(i(i(i(i(i(i(i(x,x),y),y),i(i(z,z),u)),u),i(i(v,v),w)),w),i(i(v6,v6),v7)),v7)) # label("Hint 62(143)"). 131 [hyper,1,4,126] P(i(i(i(i(i(i(x,y),z),u),v),w),i(i(i(i(i(i(i(i(v6,v7),i(i(v8,v6),i(v8,v7))),x),y),z),u),v),w))) # label("Hint 63(144)"). 132 [hyper,1,90,130] P(i(i(i(x,i(y,x)),i(i(i(i(i(i(i(i(z,z),u),u),i(i(v,v),w)),w),i(i(v6,v6),v7)),v7),i(i(v8,v8),v9))),v9)) # label("Hint 64(145)"). 133 [hyper,1,4,128] P(i(i(i(i(i(i(i(i(x,i(i(y,i(z,y)),u)),v),w),v6),v7),v8),v9),i(i(i(i(i(i(i(x,u),v),w),v6),v7),v8),v9))) # label("Hint 65(146)"). 134 [hyper,1,4,129] P(i(i(i(i(i(i(x,i(y,z)),u),v),w),v6),i(i(i(i(i(x,i(i(i(i(i(v7,v8),v8),i(i(v8,v7),v7)),y),z)),u),v),w),v6))) # label("Hint 66(147)"). 135 [hyper,1,4,131] P(i(i(i(i(i(i(i(i(i(i(x,y),i(i(z,x),i(z,y))),u),v),w),v6),v7),v8),v9),i(i(i(i(i(i(u,v),w),v6),v7),v8),v9))) # label("Hint 68(149)"). 136 [hyper,1,95,133] P(i(i(x,i(i(i(i(i(i(i(y,i(i(z,i(u,z)),v)),w),v6),v7),v8),v9),v10)),i(x,i(i(i(i(i(i(i(y,v),w),v6),v7),v8),v9),v10)))) # label("Hint 69(150)"). 137 [hyper,1,95,134] P(i(i(x,i(i(i(i(i(y,i(z,u)),v),w),v6),v7)),i(x,i(i(i(i(i(y,i(i(i(i(i(v8,v9),v9),i(i(v9,v8),v8)),z),u)),v),w),v6),v7)))) # label("Hint 70(151)"). 138 [hyper,1,4,135] P(i(i(i(i(i(i(i(i(x,y),z),u),v),w),v6),v7),i(i(i(i(i(i(i(i(i(i(v8,v9),i(i(v10,v8),i(v10,v9))),x),y),z),u),v),w),v6),v7))) # label("Hint 71(152)"). 139 [hyper,1,4,136] P(i(i(i(x,i(i(i(i(i(i(i(y,z),u),v),w),v6),v7),v8)),v9),i(i(x,i(i(i(i(i(i(i(y,i(i(v10,i(v11,v10)),z)),u),v),w),v6),v7),v8)),v9))) # label("Hint 72(153)"). 140 [hyper,1,4,137] P(i(i(i(x,i(i(i(i(i(y,i(i(i(i(i(z,u),u),i(i(u,z),z)),v),w)),v6),v7),v8),v9)),v10),i(i(x,i(i(i(i(i(y,i(v,w)),v6),v7),v8),v9)),v10))) # label("Hint 73(154)"). 141 [hyper,1,95,138] P(i(i(x,i(i(i(i(i(i(i(y,z),u),v),w),v6),v7),v8)),i(x,i(i(i(i(i(i(i(i(i(i(v9,v10),i(i(v11,v9),i(v11,v10))),y),z),u),v),w),v6),v7),v8)))) # label("Hint 74(155)"). 142 [hyper,1,139,132] P(i(i(i(x,i(y,x)),i(i(i(i(i(i(i(i(z,z),i(i(u,i(v,u)),w)),w),i(i(v6,v6),v7)),v7),i(i(v8,v8),v9)),v9),i(i(v10,v10),v11))),v11)) # label("Hint 75(156)"). 143 [hyper,1,4,141] P(i(i(i(x,i(i(i(i(i(i(i(i(i(i(y,z),i(i(u,y),i(u,z))),v),w),v6),v7),v8),v9),v10),v11)),v12),i(i(x,i(i(i(i(i(i(i(v,w),v6),v7),v8),v9),v10),v11)),v12))) # label("Hint 77(158)"). 144 [hyper,1,84,6] P(i(i(i(i(i(x,y),i(y,x)),i(y,x)),z),z)) # label("Hint 18(99)"). 145 [hyper,1,4,144] P(i(i(x,y),i(i(i(i(i(z,u),i(u,z)),i(u,z)),x),y))) # label("Hint 32(113)"). 146 [hyper,1,95,145] P(i(i(x,i(y,z)),i(x,i(i(i(i(i(u,v),i(v,u)),i(v,u)),y),z)))) # label("Hint 40(121)"). 147 [hyper,1,4,146] P(i(i(i(x,i(i(i(i(i(y,z),i(z,y)),i(z,y)),u),v)),w),i(i(x,i(u,v)),w))) # label("Hint 48(129)"). 148 [hyper,1,4,147] P(i(i(i(i(x,i(y,z)),u),v),i(i(i(x,i(i(i(i(i(w,v6),i(v6,w)),i(v6,w)),y),z)),u),v))) # label("Hint 55(136)"). 149 [hyper,1,95,148] P(i(i(x,i(i(i(y,i(z,u)),v),w)),i(x,i(i(i(y,i(i(i(i(i(v6,v7),i(v7,v6)),i(v7,v6)),z),u)),v),w)))) # label("Hint 61(142)"). 150 [hyper,1,4,149] P(i(i(i(x,i(i(i(y,i(i(i(i(i(z,u),i(u,z)),i(u,z)),v),w)),v6),v7)),v8),i(i(x,i(i(i(y,i(v,w)),v6),v7)),v8))) # label("Hint 67(148)"). 151 [hyper,1,150,142] P(i(i(i(x,i(y,x)),i(i(i(i(i(i(i(i(z,z),i(i(u,i(v,u)),w)),w),i(i(v6,v6),v7)),v7),i(i(i(i(v8,v9),i(v9,v8)),i(v9,v8)),v10)),v10),i(i(v11,v11),v12))),v12)) # label("Hint 76(157)"). 152 [hyper,1,143,151] P(i(i(i(x,i(y,x)),i(i(i(i(i(i(i(i(i(z,u),i(i(v,z),i(v,u))),i(i(w,i(v6,w)),v7)),v7),i(i(v8,v8),v9)),v9),i(i(i(i(v10,v11),i(v11,v10)),i(v11,v10)),v12)),v12),i(i(v13,v13),v14))),v14)) # label("Hint 78(159)"). 153 [hyper,1,140,152] P(i(i(i(x,i(y,x)),i(i(i(i(i(i(i(i(i(z,u),i(i(v,z),i(v,u))),i(i(w,i(v6,w)),v7)),v7),i(i(i(i(v8,v9),v9),i(i(v9,v8),v8)),v10)),v10),i(i(i(i(v11,v12),i(v12,v11)),i(v12,v11)),v13)),v13),i(i(v14,v14),v15))),v15)) # label("Hint 79(160)"). 154 [hyper,1,116,153] P(i(i(i(x,i(y,x)),i(i(i(i(i(i(i(i(i(z,u),i(i(v,z),i(v,u))),i(i(w,i(v6,w)),v7)),v7),i(i(i(i(v8,v9),v9),i(i(v9,v8),v8)),v10)),v10),i(i(i(i(v11,v12),i(v12,v11)),i(v12,v11)),v13)),v13),i(i(v14,i(v15,v14)),v16))),v16)) # label("Hint 80(161)"). 155 [binary,154.1,2.1] $F. ------------ end of proof / derivation -------------