============================== prooftrans (BV) ======================= Prover9 (64) version Aug-2007, Aug 2007. Process 24977 was started by veroff on titan, Mon Dec 3 08:50:37 2007 The command was "prover9 -f RI_rezus.in". ============================== end of head =========================== ============================== end of input ========================== ============================== PROOF ================================= % -------- Comments from original proof -------- % Proof 1 at 0.48 (+ 0.00) seconds: "Rezus". % Length of proof is 119. % Level of proof is 44. % Maximum clause weight is 98. % Given clauses 116. 1 -P(i(x,y)) | -P(x) | P(y). [assumption]. 2 P(i(i(x,y),i(i(y,z),i(x,z)))) # label("B"). [assumption]. 3 P(i(i(x,i(y,z)),i(y,i(x,z)))) # label("C"). [assumption]. 4 P(i(x,x)) # label("I"). [assumption]. 5 P(i(i(x,i(x,y)),i(x,y))) # label("W"). [assumption]. 6 -P(i(i(i(X,i(i(i(Y,Y),i(i(Z,Z),i(i(U,U),i(i(V,V),i(X,W))))),W)),i(i(i(i(i(V6,V7),i(i(V7,V8),i(V6,V8))),i(i(i(i(i(V9,i(V9,V10)),i(V9,V10)),i(i(i(V11,V12),i(i(V12,V13),i(V11,V13))),V14)),V14),V15)),V15),i(i(V16,i(i(i(V17,V17),i(i(V18,V18),i(i(V19,V19),i(i(V20,V20),i(V16,V21))))),V21)),V22))),V22)) # answer("Rezus"). [assumption]. 8 P(i(x,i(i(y,i(x,z)),i(y,z)))). [hyper(1,a,3,a,b,3,a)]. 9 P(i(i(i(x,i(y,z)),u),i(i(y,i(x,z)),u))). [hyper(1,a,2,a,b,3,a)]. 10 P(i(i(x,y),i(i(z,x),i(z,y)))). [hyper(1,a,3,a,b,2,a)]. 11 P(i(x,i(i(x,y),y))). [hyper(1,a,3,a,b,4,a)]. 12 P(i(x,i(i(x,i(x,y)),y))). [hyper(1,a,3,a,b,5,a)]. 14 P(i(i(i(x,i(i(x,y),y)),z),z)). [hyper(1,a,11,a,b,11,a)]. 15 P(i(i(i(i(x,y),y),z),i(x,z))). [hyper(1,a,2,a,b,11,a)]. 17 P(i(i(i(x,x),y),y)). [hyper(1,a,11,a,b,4,a)]. 25 P(i(i(i(x,i(i(x,i(x,y)),y)),z),z)). [hyper(1,a,11,a,b,12,a)]. 32 P(i(i(x,i(i(y,y),z)),i(x,z))). [hyper(1,a,17,a,b,8,a)]. 39 P(i(i(x,i(i(y,i(i(y,z),z)),u)),i(x,u))). [hyper(1,a,8,a,b,11,a)]. 49 P(i(i(x,y),i(x,i(i(y,z),z)))). [hyper(1,a,10,a,b,11,a)]. 52 P(i(i(x,i(y,i(z,u))),i(x,i(z,i(y,u))))). [hyper(1,a,10,a,b,3,a)]. 53 P(i(i(x,i(y,z)),i(x,i(i(z,u),i(y,u))))). [hyper(1,a,10,a,b,2,a)]. 59 P(i(x,i(i(i(i(x,y),y),z),z))). [hyper(1,a,14,a,b,15,a)]. 68 P(i(x,i(i(y,z),i(i(x,y),z)))). [hyper(1,a,15,a,b,2,a)]. 73 P(i(i(x,i(y,i(i(z,z),u))),i(x,i(y,u)))). [hyper(1,a,10,a,b,32,a)]. 79 P(i(x,i(i(x,y),i(i(y,z),z)))). [hyper(1,a,15,a,b,49,a)]. 136 P(i(i(x,y),i(i(i(z,i(i(z,u),i(i(u,w),w))),x),y))). [hyper(1,a,68,a,b,79,a)]. 141 P(i(i(i(x,i(i(x,y),i(i(y,z),z))),u),u)). [hyper(1,a,11,a,b,79,a)]. 143 P(i(i(x,i(i(y,i(i(y,z),i(i(z,u),u))),w)),i(x,w))). [hyper(1,a,8,a,b,79,a)]. 160 P(i(i(i(i(i(i(i(x,i(i(x,i(x,y)),y)),z),z),u),u),w),w)). [hyper(1,a,59,a,b,25,a)]. 172 P(i(i(x,i(i(y,i(z,u)),w)),i(x,i(i(z,i(y,u)),w)))). [hyper(1,a,10,a,b,9,a)]. 208 P(i(i(x,i(y,i(z,i(u,w)))),i(x,i(y,i(u,i(z,w)))))). [hyper(1,a,10,a,b,52,a)]. 211 P(i(i(i(x,i(y,i(z,u))),w),i(i(x,i(z,i(y,u))),w))). [hyper(1,a,2,a,b,52,a)]. 248 P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). [hyper(1,a,53,a,b,2,a)]. 262 P(i(i(x,i(y,i(z,i(i(u,u),w)))),i(x,i(y,i(z,w))))). [hyper(1,a,10,a,b,73,a)]. 264 P(i(i(i(x,i(y,z)),u),i(i(x,i(y,i(i(w,w),z))),u))). [hyper(1,a,2,a,b,73,a)]. 303 P(i(i(i(i(x,i(y,i(z,u))),w),v5),i(i(i(x,i(z,i(y,u))),w),v5))). [hyper(1,a,248,a,b,52,a)]. 312 P(i(i(i(i(i(x,i(y,z)),u),w),v5),i(i(i(i(y,i(x,z)),u),w),v5))). [hyper(1,a,248,a,b,9,a)]. 316 P(i(i(i(i(x,y),z),u),i(i(i(i(i(w,i(i(w,v5),i(i(v5,v6),v6))),x),y),z),u))). [hyper(1,a,248,a,b,136,a)]. 347 P(i(i(i(i(x,i(i(y,i(i(y,z),i(i(z,u),u))),w)),v5),v6),i(i(i(x,w),v5),v6))). [hyper(1,a,248,a,b,143,a)]. 368 P(i(i(i(i(x,i(i(y,i(z,u)),w)),v5),v6),i(i(i(x,i(i(z,i(y,u)),w)),v5),v6))). [hyper(1,a,248,a,b,172,a)]. 384 P(i(i(i(x,i(i(y,i(z,u)),w)),v5),i(i(x,i(i(z,i(y,u)),w)),v5))). [hyper(1,a,2,a,b,172,a)]. 416 P(i(i(x,i(y,i(z,i(u,i(w,v5))))),i(x,i(y,i(z,i(w,i(u,v5))))))). [hyper(1,a,10,a,b,208,a)]. 418 P(i(i(i(x,i(y,i(z,i(u,w)))),v5),i(i(x,i(y,i(u,i(z,w)))),v5))). [hyper(1,a,2,a,b,208,a)]. 436 P(i(i(i(x,i(y,i(z,u))),w),i(i(z,i(x,i(y,u))),w))). [hyper(1,a,172,a,b,211,a)]. 450 P(i(i(x,i(i(y,i(z,i(u,w))),v5)),i(x,i(i(y,i(u,i(z,w))),v5)))). [hyper(1,a,10,a,b,211,a)]. 482 P(i(i(x,i(y,i(z,i(u,i(i(w,w),v5))))),i(x,i(y,i(z,i(u,v5)))))). [hyper(1,a,10,a,b,262,a)]. 518 P(i(i(x,i(i(y,i(z,u)),w)),i(x,i(i(y,i(z,i(i(v5,v5),u))),w)))). [hyper(1,a,10,a,b,264,a)]. 580 P(i(i(i(i(i(i(i(x,i(i(x,i(x,y)),y)),z),z),u),u),w),i(i(w,v5),v5))). [hyper(1,a,141,a,b,160,a)]. 611 P(i(i(i(i(i(i(x,i(y,i(z,u))),w),v5),v6),v7),i(i(i(i(i(x,i(z,i(y,u))),w),v5),v6),v7))). [hyper(1,a,248,a,b,303,a)]. 671 P(i(i(x,i(i(i(i(y,i(z,u)),w),v5),v6)),i(x,i(i(i(i(z,i(y,u)),w),v5),v6)))). [hyper(1,a,10,a,b,312,a)]. 674 P(i(i(i(i(i(i(x,i(y,z)),u),w),v5),v6),i(i(i(i(i(y,i(x,z)),u),w),v5),v6))). [hyper(1,a,2,a,b,312,a)]. 722 P(i(i(x,i(i(y,i(i(z,i(u,w)),v5)),v6)),i(x,i(i(y,i(i(u,i(z,w)),v5)),v6)))). [hyper(1,a,10,a,b,384,a)]. 767 P(i(i(i(x,i(y,i(z,i(u,i(w,v5))))),v6),i(i(x,i(y,i(z,i(w,i(u,v5))))),v6))). [hyper(1,a,2,a,b,416,a)]. 810 P(i(i(x,i(i(y,i(z,i(u,i(w,v5)))),v6)),i(x,i(i(y,i(z,i(w,i(u,v5)))),v6)))). [hyper(1,a,10,a,b,418,a)]. 827 P(i(i(i(i(x,i(i(y,i(z,i(u,w))),v5)),v6),v7),i(i(i(x,i(i(y,i(u,i(z,w))),v5)),v6),v7))). [hyper(1,a,248,a,b,450,a)]. 846 P(i(i(i(x,i(i(y,i(z,i(u,w))),v5)),v6),i(i(x,i(i(y,i(u,i(z,w))),v5)),v6))). [hyper(1,a,2,a,b,450,a)]. 885 P(i(i(i(x,i(y,i(z,i(u,w)))),v5),i(i(x,i(y,i(z,i(u,i(i(v6,v6),w))))),v5))). [hyper(1,a,2,a,b,482,a)]. 933 P(i(i(i(x,i(i(y,i(z,i(i(u,u),w))),v5)),v6),i(i(x,i(i(y,i(z,w)),v5)),v6))). [hyper(1,a,2,a,b,518,a)]. 1073 P(i(i(i(i(i(i(i(x,i(i(x,i(x,y)),y)),i(i(z,i(i(z,u),i(i(u,w),w))),v5)),v5),v6),v6),v7),v7)). [hyper(1,a,580,a,b,347,a)]. 1168 P(i(i(x,i(i(i(y,i(i(z,i(u,w)),v5)),v6),v7)),i(x,i(i(i(y,i(i(u,i(z,w)),v5)),v6),v7)))). [hyper(1,a,10,a,b,368,a)]. 1207 P(i(i(i(i(x,i(i(i(i(y,i(z,u)),w),v5),v6)),v7),v8),i(i(i(x,i(i(i(i(z,i(y,u)),w),v5),v6)),v7),v8))). [hyper(1,a,248,a,b,671,a)]. 1255 P(i(i(i(i(i(i(x,i(y,z)),u),w),i(v5,i(v6,v7))),v8),i(i(i(i(i(y,i(x,z)),u),w),i(v6,i(v5,v7))),v8))). [hyper(1,a,450,a,b,674,a)]. 1326 P(i(i(x,i(y,i(i(z,i(i(u,i(w,v5)),v6)),v7))),i(x,i(y,i(i(z,i(i(w,i(u,v5)),v6)),v7))))). [hyper(1,a,10,a,b,722,a)]. 1367 P(i(i(x,i(i(y,i(z,i(u,i(w,i(v5,v6))))),v7)),i(x,i(i(y,i(z,i(u,i(v5,i(w,v6))))),v7)))). [hyper(1,a,10,a,b,767,a)]. 1424 P(i(i(i(x,i(i(y,i(z,i(u,i(w,v5)))),v6)),v7),i(i(x,i(i(y,i(z,i(w,i(u,v5)))),v6)),v7))). [hyper(1,a,2,a,b,810,a)]. 1480 P(i(i(x,i(i(y,i(i(z,i(u,i(w,v5))),v6)),v7)),i(x,i(i(y,i(i(z,i(w,i(u,v5))),v6)),v7)))). [hyper(1,a,10,a,b,846,a)]. 1539 P(i(i(x,i(i(y,i(z,i(u,i(w,v5)))),v6)),i(x,i(i(y,i(z,i(u,i(w,i(i(v7,v7),v5))))),v6)))). [hyper(1,a,10,a,b,885,a)]. 1650 P(i(i(i(i(i(i(x,i(y,i(z,u))),w),v5),i(v6,v7)),v8),i(i(v6,i(i(i(i(x,i(z,i(y,u))),w),v5),v7)),v8))). [hyper(1,a,172,a,b,611,a)]. 1752 P(i(i(x,i(i(i(y,i(i(z,i(u,i(w,v5))),v6)),v7),v8)),i(x,i(i(i(y,i(i(z,i(w,i(u,v5))),v6)),v7),v8)))). [hyper(1,a,10,a,b,827,a)]. 1800 P(i(i(i(i(x,i(i(i(y,i(i(z,i(u,w)),v5)),v6),v7)),v8),v9),i(i(i(x,i(i(i(y,i(i(u,i(z,w)),v5)),v6),v7)),v8),v9))). [hyper(1,a,248,a,b,1168,a)]. 1949 P(i(i(i(x,i(i(y,i(z,i(u,i(w,i(v5,v6))))),v7)),v8),i(i(x,i(i(y,i(z,i(u,i(v5,i(w,v6))))),v7)),v8))). [hyper(1,a,2,a,b,1367,a)]. 2014 P(i(i(x,i(i(y,i(i(z,i(u,i(w,i(v5,v6)))),v7)),v8)),i(x,i(i(y,i(i(z,i(u,i(v5,i(w,v6)))),v7)),v8)))). [hyper(1,a,10,a,b,1424,a)]. 2079 P(i(i(x,i(y,i(i(z,i(i(u,i(w,i(v5,v6))),v7)),v8))),i(x,i(y,i(i(z,i(i(u,i(v5,i(w,v6))),v7)),v8))))). [hyper(1,a,10,a,b,1480,a)]. 2134 P(i(i(i(x,i(i(y,i(z,i(u,i(w,i(i(v5,v5),v6))))),v7)),v8),i(i(x,i(i(y,i(z,i(u,i(w,v6)))),v7)),v8))). [hyper(1,a,2,a,b,1539,a)]. 2176 P(i(i(i(i(i(x,i(i(x,y),i(i(y,z),z))),i(i(i(i(u,i(i(u,i(u,w)),w)),i(i(v5,i(i(v5,v6),i(i(v6,v7),v7))),v8)),v8),v9)),v9),v10),v10)). [hyper(1,a,316,a,b,1073,a)]. 2264 P(i(i(i(i(i(x,i(i(i(i(y,i(z,u)),w),v5),v6)),v7),v8),v9),i(i(i(i(x,i(i(i(i(z,i(y,u)),w),v5),v6)),v7),v8),v9))). [hyper(1,a,2,a,b,1207,a)]. 2426 P(i(i(i(i(i(i(x,i(y,i(z,u))),w),v5),i(v6,i(v7,v8))),v9),i(i(v7,i(i(i(i(x,i(z,i(y,u))),w),v5),i(v6,v8))),v9))). [hyper(1,a,303,a,b,1650,a)]. 2516 P(i(i(i(i(x,i(i(i(y,i(i(z,i(u,i(w,v5))),v6)),v7),v8)),v9),v10),i(i(i(x,i(i(i(y,i(i(z,i(w,i(u,v5))),v6)),v7),v8)),v9),v10))). [hyper(1,a,248,a,b,1752,a)]. 2594 P(i(i(x,i(i(y,i(i(z,i(u,i(w,i(v5,i(v6,v7))))),v8)),v9)),i(x,i(i(y,i(i(z,i(u,i(w,i(v6,i(v5,v7))))),v8)),v9)))). [hyper(1,a,10,a,b,1949,a)]. 2651 P(i(i(x,i(y,i(i(z,i(i(u,i(w,i(v5,i(v6,v7)))),v8)),v9))),i(x,i(y,i(i(z,i(i(u,i(w,i(v6,i(v5,v7)))),v8)),v9))))). [hyper(1,a,10,a,b,2014,a)]. 2859 P(i(i(i(i(i(x,i(i(i(i(y,i(z,u)),w),v5),v6)),v7),i(v8,i(v9,v10))),v11),i(i(i(i(x,i(i(i(i(z,i(y,u)),w),v5),v6)),v7),i(v9,i(v8,v10))),v11))). [hyper(1,a,450,a,b,2264,a)]. 3002 P(i(i(x,i(y,i(i(z,i(i(u,i(w,i(v5,i(v6,i(v7,v8))))),v9)),v10))),i(x,i(y,i(i(z,i(i(u,i(w,i(v5,i(v7,i(v6,v8))))),v9)),v10))))). [hyper(1,a,10,a,b,2594,a)]. 3085 P(i(i(i(i(i(x,i(i(i(y,i(i(z,i(u,i(w,v5))),v6)),v7),v8)),v9),v10),v11),i(i(i(i(x,i(i(i(y,i(i(z,i(w,i(u,v5))),v6)),v7),v8)),v9),v10),v11))). [hyper(1,a,2,a,b,2516,a)]. 3147 P(i(i(x,i(i(i(i(y,i(i(y,z),i(i(z,u),u))),i(i(i(i(w,i(i(w,i(w,v5)),v5)),i(i(v6,i(i(v6,v7),i(i(v7,v8),v8))),v9)),v9),v10)),v10),v11)),i(x,v11))). [hyper(1,a,10,a,b,2176,a)]. 3211 P(i(i(i(x,i(i(x,y),y)),i(i(i(i(z,i(i(z,u),i(i(u,w),w))),i(i(i(i(v5,i(i(v5,i(v5,v6)),v6)),i(i(v7,i(i(v7,v8),i(i(v8,v9),v9))),v10)),v10),v11)),v11),v12)),v12)). [hyper(1,a,39,a,b,3147,a)]. 3221 P(i(i(x,i(i(y,i(i(y,z),z)),i(i(i(i(u,i(i(u,w),i(i(w,v5),v5))),i(i(i(i(v6,i(i(v6,i(v6,v7)),v7)),i(i(v8,i(i(v8,v9),i(i(v9,v10),v10))),v11)),v11),v12)),v12),v13))),i(x,v13))). [hyper(1,a,436,a,b,3211,a)]. 3224 P(i(i(i(x,i(i(x,y),y)),i(i(z,i(i(z,u),u)),i(i(i(i(w,i(i(w,v5),i(i(v5,v6),v6))),i(i(i(i(v7,i(i(v7,i(v7,v8)),v8)),i(i(v9,i(i(v9,v10),i(i(v10,v11),v11))),v12)),v12),v13)),v13),v14))),v14)). [hyper(1,a,39,a,b,3221,a)]. 3226 P(i(i(i(x,i(i(x,y),y)),i(i(z,i(i(z,i(i(u,u),w)),w)),i(i(i(i(v5,i(i(v5,v6),i(i(v6,v7),v7))),i(i(i(i(v8,i(i(v8,i(v8,v9)),v9)),i(i(v10,i(i(v10,v11),i(i(v11,v12),v12))),v13)),v13),v14)),v14),v15))),v15)). [hyper(1,a,933,a,b,3224,a)]. 3254 P(i(i(i(x,i(i(x,y),y)),i(i(z,i(i(z,i(i(u,u),i(i(w,w),v5))),v5)),i(i(i(i(v6,i(i(v6,v7),i(i(v7,v8),v8))),i(i(i(i(v9,i(i(v9,i(v9,v10)),v10)),i(i(v11,i(i(v11,v12),i(i(v12,v13),v13))),v14)),v14),v15)),v15),v16))),v16)). [hyper(1,a,933,a,b,3226,a)]. 3278 P(i(i(i(x,i(i(x,y),y)),i(i(z,i(i(z,i(i(u,u),i(i(w,w),i(i(v5,v5),v6)))),v6)),i(i(i(i(v7,i(i(v7,v8),i(i(v8,v9),v9))),i(i(i(i(v10,i(i(v10,i(v10,v11)),v11)),i(i(v12,i(i(v12,v13),i(i(v13,v14),v14))),v15)),v15),v16)),v16),v17))),v17)). [hyper(1,a,933,a,b,3254,a)]. 3286 P(i(i(i(x,i(i(x,y),y)),i(i(z,i(i(z,i(i(u,u),i(i(w,w),i(i(v5,v5),i(i(v6,v6),v7))))),v7)),i(i(i(i(v8,i(i(v8,v9),i(i(v9,v10),v10))),i(i(i(i(v11,i(i(v11,i(v11,v12)),v12)),i(i(v13,i(i(v13,v14),i(i(v14,v15),v15))),v16)),v16),v17)),v17),v18))),v18)). [hyper(1,a,933,a,b,3278,a)]. 3291 P(i(i(x,i(i(y,i(i(y,z),z)),i(i(u,i(i(u,i(i(w,w),i(i(v5,v5),i(i(v6,v6),i(i(v7,v7),v8))))),v8)),i(i(i(i(v9,i(i(v9,v10),i(i(v10,v11),v11))),i(i(i(i(v12,i(i(v12,i(v12,v13)),v13)),i(i(v14,i(i(v14,v15),i(i(v15,v16),v16))),v17)),v17),v18)),v18),v19)))),i(x,v19))). [hyper(1,a,10,a,b,3286,a)]. 3307 P(i(i(x,i(i(y,i(i(y,i(i(z,z),u)),u)),i(i(w,i(i(w,i(i(v5,v5),i(i(v6,v6),i(i(v7,v7),i(i(v8,v8),v9))))),v9)),i(i(i(i(v10,i(i(v10,v11),i(i(v11,v12),v12))),i(i(i(i(v13,i(i(v13,i(v13,v14)),v14)),i(i(v15,i(i(v15,v16),i(i(v16,v17),v17))),v18)),v18),v19)),v19),v20)))),i(x,v20))). [hyper(1,a,933,a,b,3291,a)]. 3309 P(i(i(x,i(i(y,i(i(y,i(i(z,z),i(i(u,u),w))),w)),i(i(v5,i(i(v5,i(i(v6,v6),i(i(v7,v7),i(i(v8,v8),i(i(v9,v9),v10))))),v10)),i(i(i(i(v11,i(i(v11,v12),i(i(v12,v13),v13))),i(i(i(i(v14,i(i(v14,i(v14,v15)),v15)),i(i(v16,i(i(v16,v17),i(i(v17,v18),v18))),v19)),v19),v20)),v20),v21)))),i(x,v21))). [hyper(1,a,933,a,b,3307,a)]. 3312 P(i(i(x,i(i(y,i(i(y,i(i(z,z),i(i(u,u),i(i(w,w),v5)))),v5)),i(i(v6,i(i(v6,i(i(v7,v7),i(i(v8,v8),i(i(v9,v9),i(i(v10,v10),v11))))),v11)),i(i(i(i(v12,i(i(v12,v13),i(i(v13,v14),v14))),i(i(i(i(v15,i(i(v15,i(v15,v16)),v16)),i(i(v17,i(i(v17,v18),i(i(v18,v19),v19))),v20)),v20),v21)),v21),v22)))),i(x,v22))). [hyper(1,a,933,a,b,3309,a)]. 3316 P(i(i(i(x,i(i(x,i(i(y,y),i(i(z,z),i(i(u,u),i(i(w,w),v5))))),v5)),i(i(v6,i(i(v6,i(i(v7,v7),i(i(v8,v8),i(i(v9,v9),i(i(v10,v10),v11))))),v11)),i(i(i(i(v12,i(i(v12,v13),i(i(v13,v14),v14))),i(i(i(i(v15,i(i(v15,i(v15,v16)),v16)),i(i(v17,i(i(v17,v18),i(i(v18,v19),v19))),v20)),v20),v21)),v21),v22))),v22)). [hyper(1,a,3312,a,b,2134,a)]. 3318 P(i(i(i(i(i(x,i(i(x,y),i(i(y,z),z))),i(i(i(i(u,i(i(u,i(u,w)),w)),i(i(v5,i(i(v5,v6),i(i(v6,v7),v7))),v8)),v8),v9)),v9),i(i(v10,i(i(v10,i(i(v11,v11),i(i(v12,v12),i(i(v13,v13),i(i(v14,v14),v15))))),v15)),i(i(v16,i(i(v16,i(i(v17,v17),i(i(v18,v18),i(i(v19,v19),i(i(v20,v20),v21))))),v21)),v22))),v22)). [hyper(1,a,436,a,b,3316,a)]. 3320 P(i(i(x,i(i(i(i(y,i(i(y,z),i(i(z,u),u))),i(i(i(i(w,i(i(w,i(w,v5)),v5)),i(i(v6,i(i(v6,v7),i(i(v7,v8),v8))),v9)),v9),v10)),v10),i(i(v11,i(i(v11,i(i(v12,v12),i(i(v13,v13),i(i(v14,v14),i(i(v15,v15),v16))))),v16)),i(i(v17,i(i(v17,i(i(v18,v18),i(i(v19,v19),i(i(v20,v20),i(i(v21,v21),v22))))),v22)),v23)))),i(x,v23))). [hyper(1,a,10,a,b,3318,a)]. 3324 P(i(i(i(i(i(x,i(i(x,y),i(i(y,z),z))),i(i(i(i(u,i(i(u,i(u,w)),w)),i(i(v5,i(i(v5,v6),i(i(v6,v7),v7))),v8)),v8),v9)),v9),i(i(v10,i(i(v10,i(i(v11,v11),i(i(v12,v12),i(i(v13,v13),i(i(v14,v14),v15))))),v15)),i(i(v16,i(i(i(v17,v17),i(v16,i(i(v18,v18),i(i(v19,v19),i(i(v20,v20),v21))))),v21)),v22))),v22)). [hyper(1,a,3320,a,b,1326,a)]. 3326 P(i(i(x,i(i(i(i(y,i(i(y,z),i(i(z,u),u))),i(i(i(i(w,i(i(w,i(w,v5)),v5)),i(i(v6,i(i(v6,v7),i(i(v7,v8),v8))),v9)),v9),v10)),v10),i(i(v11,i(i(v11,i(i(v12,v12),i(i(v13,v13),i(i(v14,v14),i(i(v15,v15),v16))))),v16)),i(i(v17,i(i(i(v18,v18),i(v17,i(i(v19,v19),i(i(v20,v20),i(i(v21,v21),v22))))),v22)),v23)))),i(x,v23))). [hyper(1,a,10,a,b,3324,a)]. 3332 P(i(i(i(i(i(x,i(i(x,y),i(i(y,z),z))),i(i(i(i(u,i(i(u,i(u,w)),w)),i(i(v5,i(i(v5,v6),i(i(v6,v7),v7))),v8)),v8),v9)),v9),i(i(v10,i(i(v10,i(i(v11,v11),i(i(v12,v12),i(i(v13,v13),i(i(v14,v14),v15))))),v15)),i(i(v16,i(i(i(v17,v17),i(i(v18,v18),i(v16,i(i(v19,v19),i(i(v20,v20),v21))))),v21)),v22))),v22)). [hyper(1,a,3326,a,b,2079,a)]. 3335 P(i(i(x,i(i(i(i(y,i(i(y,z),i(i(z,u),u))),i(i(i(i(w,i(i(w,i(w,v5)),v5)),i(i(v6,i(i(v6,v7),i(i(v7,v8),v8))),v9)),v9),v10)),v10),i(i(v11,i(i(v11,i(i(v12,v12),i(i(v13,v13),i(i(v14,v14),i(i(v15,v15),v16))))),v16)),i(i(v17,i(i(i(v18,v18),i(i(v19,v19),i(v17,i(i(v20,v20),i(i(v21,v21),v22))))),v22)),v23)))),i(x,v23))). [hyper(1,a,10,a,b,3332,a)]. 3340 P(i(i(i(i(i(x,i(i(x,y),i(i(y,z),z))),i(i(i(i(u,i(i(u,i(u,w)),w)),i(i(v5,i(i(v5,v6),i(i(v6,v7),v7))),v8)),v8),v9)),v9),i(i(v10,i(i(v10,i(i(v11,v11),i(i(v12,v12),i(i(v13,v13),i(i(v14,v14),v15))))),v15)),i(i(v16,i(i(i(v17,v17),i(i(v18,v18),i(i(v19,v19),i(v16,i(i(v20,v20),v21))))),v21)),v22))),v22)). [hyper(1,a,3335,a,b,2651,a)]. 3343 P(i(i(x,i(i(i(i(y,i(i(y,z),i(i(z,u),u))),i(i(i(i(w,i(i(w,i(w,v5)),v5)),i(i(v6,i(i(v6,v7),i(i(v7,v8),v8))),v9)),v9),v10)),v10),i(i(v11,i(i(v11,i(i(v12,v12),i(i(v13,v13),i(i(v14,v14),i(i(v15,v15),v16))))),v16)),i(i(v17,i(i(i(v18,v18),i(i(v19,v19),i(i(v20,v20),i(v17,i(i(v21,v21),v22))))),v22)),v23)))),i(x,v23))). [hyper(1,a,10,a,b,3340,a)]. 3349 P(i(i(i(i(i(x,i(i(x,y),i(i(y,z),z))),i(i(i(i(u,i(i(u,i(u,w)),w)),i(i(v5,i(i(v5,v6),i(i(v6,v7),v7))),v8)),v8),v9)),v9),i(i(v10,i(i(v10,i(i(v11,v11),i(i(v12,v12),i(i(v13,v13),i(i(v14,v14),v15))))),v15)),i(i(v16,i(i(i(v17,v17),i(i(v18,v18),i(i(v19,v19),i(i(v20,v20),i(v16,v21))))),v21)),v22))),v22)). [hyper(1,a,3343,a,b,3002,a)]. 3351 P(i(i(x,i(i(i(i(y,i(i(y,z),i(i(z,u),u))),i(i(i(i(w,i(i(w,i(w,v5)),v5)),i(i(v6,i(i(v6,v7),i(i(v7,v8),v8))),v9)),v9),v10)),v10),i(i(v11,i(i(v11,i(i(v12,v12),i(i(v13,v13),i(i(v14,v14),i(i(v15,v15),v16))))),v16)),i(i(v17,i(i(i(v18,v18),i(i(v19,v19),i(i(v20,v20),i(i(v21,v21),i(v17,v22))))),v22)),v23)))),i(x,v23))). [hyper(1,a,10,a,b,3349,a)]. 3357 P(i(i(i(i(i(x,i(i(x,y),i(i(y,z),z))),i(i(i(i(u,i(i(u,i(u,w)),w)),i(i(v5,i(i(v5,v6),i(i(v6,v7),v7))),v8)),v8),v9)),v9),i(i(v10,i(i(i(v11,v11),i(v10,i(i(v12,v12),i(i(v13,v13),i(i(v14,v14),v15))))),v15)),i(i(v16,i(i(i(v17,v17),i(i(v18,v18),i(i(v19,v19),i(i(v20,v20),i(v16,v21))))),v21)),v22))),v22)). [hyper(1,a,3351,a,b,722,a)]. 3359 P(i(i(x,i(i(i(i(y,i(i(y,z),i(i(z,u),u))),i(i(i(i(w,i(i(w,i(w,v5)),v5)),i(i(v6,i(i(v6,v7),i(i(v7,v8),v8))),v9)),v9),v10)),v10),i(i(v11,i(i(i(v12,v12),i(v11,i(i(v13,v13),i(i(v14,v14),i(i(v15,v15),v16))))),v16)),i(i(v17,i(i(i(v18,v18),i(i(v19,v19),i(i(v20,v20),i(i(v21,v21),i(v17,v22))))),v22)),v23)))),i(x,v23))). [hyper(1,a,10,a,b,3357,a)]. 3360 P(i(i(i(i(i(x,i(i(x,y),i(i(y,z),z))),i(i(i(i(u,i(i(u,i(u,w)),w)),i(i(v5,i(i(v5,v6),i(i(v6,v7),v7))),v8)),v8),v9)),v9),i(i(v10,i(i(i(v11,v11),i(i(v12,v12),i(v10,i(i(v13,v13),i(i(v14,v14),v15))))),v15)),i(i(v16,i(i(i(v17,v17),i(i(v18,v18),i(i(v19,v19),i(i(v20,v20),i(v16,v21))))),v21)),v22))),v22)). [hyper(1,a,3359,a,b,1480,a)]. 3361 P(i(i(x,i(i(i(i(y,i(i(y,z),i(i(z,u),u))),i(i(i(i(w,i(i(w,i(w,v5)),v5)),i(i(v6,i(i(v6,v7),i(i(v7,v8),v8))),v9)),v9),v10)),v10),i(i(v11,i(i(i(v12,v12),i(i(v13,v13),i(v11,i(i(v14,v14),i(i(v15,v15),v16))))),v16)),i(i(v17,i(i(i(v18,v18),i(i(v19,v19),i(i(v20,v20),i(i(v21,v21),i(v17,v22))))),v22)),v23)))),i(x,v23))). [hyper(1,a,10,a,b,3360,a)]. 3362 P(i(i(i(i(i(x,i(i(x,y),i(i(y,z),z))),i(i(i(i(u,i(i(u,i(u,w)),w)),i(i(v5,i(i(v5,v6),i(i(v6,v7),v7))),v8)),v8),v9)),v9),i(i(v10,i(i(i(v11,v11),i(i(v12,v12),i(i(v13,v13),i(v10,i(i(v14,v14),v15))))),v15)),i(i(v16,i(i(i(v17,v17),i(i(v18,v18),i(i(v19,v19),i(i(v20,v20),i(v16,v21))))),v21)),v22))),v22)). [hyper(1,a,3361,a,b,2014,a)]. 3365 P(i(i(x,i(i(i(i(y,i(i(y,z),i(i(z,u),u))),i(i(i(i(w,i(i(w,i(w,v5)),v5)),i(i(v6,i(i(v6,v7),i(i(v7,v8),v8))),v9)),v9),v10)),v10),i(i(v11,i(i(i(v12,v12),i(i(v13,v13),i(i(v14,v14),i(v11,i(i(v15,v15),v16))))),v16)),i(i(v17,i(i(i(v18,v18),i(i(v19,v19),i(i(v20,v20),i(i(v21,v21),i(v17,v22))))),v22)),v23)))),i(x,v23))). [hyper(1,a,10,a,b,3362,a)]. 3368 P(i(i(i(i(i(x,i(i(x,y),i(i(y,z),z))),i(i(i(i(u,i(i(u,i(u,w)),w)),i(i(v5,i(i(v5,v6),i(i(v6,v7),v7))),v8)),v8),v9)),v9),i(i(v10,i(i(i(v11,v11),i(i(v12,v12),i(i(v13,v13),i(i(v14,v14),i(v10,v15))))),v15)),i(i(v16,i(i(i(v17,v17),i(i(v18,v18),i(i(v19,v19),i(i(v20,v20),i(v16,v21))))),v21)),v22))),v22)). [hyper(1,a,3365,a,b,2594,a)]. 3370 P(i(i(x,i(i(i(i(y,i(i(y,z),i(i(z,u),u))),i(i(i(i(w,i(i(w,i(w,v5)),v5)),i(i(v6,i(i(v6,v7),i(i(v7,v8),v8))),v9)),v9),v10)),v10),i(i(v11,i(i(i(v12,v12),i(i(v13,v13),i(i(v14,v14),i(i(v15,v15),i(v11,v16))))),v16)),i(i(v17,i(i(i(v18,v18),i(i(v19,v19),i(i(v20,v20),i(i(v21,v21),i(v17,v22))))),v22)),v23)))),i(x,v23))). [hyper(1,a,10,a,b,3368,a)]. 3376 P(i(i(i(i(i(x,i(i(x,y),i(i(y,z),z))),i(i(i(i(u,i(i(u,i(u,w)),w)),i(i(i(v5,v6),i(v5,i(i(v6,v7),v7))),v8)),v8),v9)),v9),i(i(v10,i(i(i(v11,v11),i(i(v12,v12),i(i(v13,v13),i(i(v14,v14),i(v10,v15))))),v15)),i(i(v16,i(i(i(v17,v17),i(i(v18,v18),i(i(v19,v19),i(i(v20,v20),i(v16,v21))))),v21)),v22))),v22)). [hyper(1,a,3370,a,b,1800,a)]. 3377 P(i(i(i(i(i(x,i(i(x,y),i(i(y,z),z))),i(i(i(i(u,i(i(u,i(u,w)),w)),i(i(i(v5,v6),i(i(v6,v7),i(v5,v7))),v8)),v8),v9)),v9),i(i(v10,i(i(i(v11,v11),i(i(v12,v12),i(i(v13,v13),i(i(v14,v14),i(v10,v15))))),v15)),i(i(v16,i(i(i(v17,v17),i(i(v18,v18),i(i(v19,v19),i(i(v20,v20),i(v16,v21))))),v21)),v22))),v22)). [hyper(1,a,3085,a,b,3376,a)]. 3384 P(i(i(i(i(i(x,i(i(x,y),i(i(y,z),z))),i(i(i(i(i(u,i(u,w)),i(u,w)),i(i(i(v5,v6),i(i(v6,v7),i(v5,v7))),v8)),v8),v9)),v9),i(i(v10,i(i(i(v11,v11),i(i(v12,v12),i(i(v13,v13),i(i(v14,v14),i(v10,v15))))),v15)),i(i(v16,i(i(i(v17,v17),i(i(v18,v18),i(i(v19,v19),i(i(v20,v20),i(v16,v21))))),v21)),v22))),v22)). [hyper(1,a,2859,a,b,3377,a)]. 3393 P(i(i(i(i(i(i(x,y),i(x,i(i(y,z),z))),i(i(i(i(i(u,i(u,w)),i(u,w)),i(i(i(v5,v6),i(i(v6,v7),i(v5,v7))),v8)),v8),v9)),v9),i(i(v10,i(i(i(v11,v11),i(i(v12,v12),i(i(v13,v13),i(i(v14,v14),i(v10,v15))))),v15)),i(i(v16,i(i(i(v17,v17),i(i(v18,v18),i(i(v19,v19),i(i(v20,v20),i(v16,v21))))),v21)),v22))),v22)). [hyper(1,a,1255,a,b,3384,a)]. 3434 P(i(i(i(x,i(i(i(y,y),i(i(z,z),i(i(u,u),i(i(w,w),i(x,v5))))),v5)),i(i(i(i(i(v6,v7),i(i(v7,v8),i(v6,v8))),i(i(i(i(i(v9,i(v9,v10)),i(v9,v10)),i(i(i(v11,v12),i(i(v12,v13),i(v11,v13))),v14)),v14),v15)),v15),i(i(v16,i(i(i(v17,v17),i(i(v18,v18),i(i(v19,v19),i(i(v20,v20),i(v16,v21))))),v21)),v22))),v22)). [hyper(1,a,2426,a,b,3393,a)]. 3435 $F # answer("Rezus"). [resolve(3434,a,6,a)]. ============================== end of proof ==========================