============================== Prover9 =============================== 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 =========================== ============================== INPUT ================================= % Reading from file RI_rezus.in clear(auto). % clear(auto) -> clear(auto_inference). % clear(auto_inference) -> clear(predicate_elim). % clear(auto_inference) -> assign(eq_defs, pass). % clear(auto) -> clear(auto_limits). % clear(auto_limits) -> assign(max_weight, 2147483647). % clear(auto_limits) -> assign(sos_limit, -1). % clear(auto) -> clear(auto_denials). % clear(auto) -> clear(auto_process). set(hyper_resolution). % set(hyper_resolution) -> set(pos_hyper_resolution). assign(max_megs,950). assign(max_weight,50). assign(sos_limit,50000). formulas(usable). -P(i(x,y)) | -P(x) | P(y). end_of_list. formulas(sos). P(i(i(u,v),i(i(v,w),i(u,w)))) # label("B"). P(i(i(u,i(v,w)),i(v,i(u,w)))) # label("C"). P(i(u,u)) # label("I"). P(i(i(u,i(u,v)),i(u,v))) # label("W"). -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"). end_of_list. formulas(hints). P(i(x,i(i(y,i(x,z)),i(y,z)))). P(i(i(i(x,i(y,z)),u),i(i(y,i(x,z)),u))). P(i(i(x,y),i(i(z,x),i(z,y)))). P(i(x,i(i(x,y),y))). P(i(x,i(i(x,i(x,y)),y))). P(i(i(i(x,i(i(x,y),y)),z),z)). P(i(i(i(i(x,y),y),z),i(x,z))). P(i(i(i(x,x),y),y)). P(i(i(i(x,i(i(x,i(x,y)),y)),z),z)). P(i(i(x,i(i(y,y),z)),i(x,z))). P(i(i(x,i(i(y,i(i(y,z),z)),u)),i(x,u))). P(i(i(x,y),i(x,i(i(y,z),z)))). P(i(i(x,i(y,i(z,u))),i(x,i(z,i(y,u))))). P(i(i(x,i(y,z)),i(x,i(i(z,u),i(y,u))))). P(i(x,i(i(i(i(x,y),y),z),z))). P(i(x,i(i(y,z),i(i(x,y),z)))). P(i(i(x,i(y,i(i(z,z),u))),i(x,i(y,u)))). P(i(x,i(i(x,y),i(i(y,z),z)))). P(i(i(x,y),i(i(i(z,i(i(z,u),i(i(u,w),w))),x),y))). P(i(i(i(x,i(i(x,y),i(i(y,z),z))),u),u)). P(i(i(x,i(i(y,i(i(y,z),i(i(z,u),u))),w)),i(x,w))). P(i(i(i(i(i(i(i(x,i(i(x,i(x,y)),y)),z),z),u),u),w),w)). P(i(i(x,i(i(y,i(z,u)),w)),i(x,i(i(z,i(y,u)),w)))). P(i(i(x,i(y,i(z,i(u,w)))),i(x,i(y,i(u,i(z,w)))))). P(i(i(i(x,i(y,i(z,u))),w),i(i(x,i(z,i(y,u))),w))). P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). P(i(i(x,i(y,i(z,i(i(u,u),w)))),i(x,i(y,i(z,w))))). P(i(i(i(x,i(y,z)),u),i(i(x,i(y,i(i(w,w),z))),u))). P(i(i(i(i(x,i(y,i(z,u))),w),v5),i(i(i(x,i(z,i(y,u))),w),v5))). P(i(i(i(i(i(x,i(y,z)),u),w),v5),i(i(i(i(y,i(x,z)),u),w),v5))). 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))). 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))). 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))). P(i(i(i(x,i(i(y,i(z,u)),w)),v5),i(i(x,i(i(z,i(y,u)),w)),v5))). P(i(i(x,i(y,i(z,i(u,i(w,v5))))),i(x,i(y,i(z,i(w,i(u,v5))))))). P(i(i(i(x,i(y,i(z,i(u,w)))),v5),i(i(x,i(y,i(u,i(z,w)))),v5))). P(i(i(i(x,i(y,i(z,u))),w),i(i(z,i(x,i(y,u))),w))). P(i(i(x,i(i(y,i(z,i(u,w))),v5)),i(x,i(i(y,i(u,i(z,w))),v5)))). P(i(i(x,i(y,i(z,i(u,i(i(w,w),v5))))),i(x,i(y,i(z,i(u,v5)))))). P(i(i(x,i(i(y,i(z,u)),w)),i(x,i(i(y,i(z,i(i(v5,v5),u))),w)))). 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))). 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))). 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)))). 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))). 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)))). 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))). 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)))). 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))). 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))). 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))). 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))). 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)). 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)))). 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))). 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))). 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))))). 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)))). 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))). 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)))). 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)))). 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))). 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)))). 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))). 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))). 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)))). 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))))). 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))). 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)). 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))). 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))). 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))). 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)))). 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))))). 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))). 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))))). 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))). 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))). 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)). 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))). 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)). 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)). 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)). 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)). 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)). 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))). 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))). 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))). 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))). 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)). 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)). 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))). 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)). 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))). 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)). 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))). 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)). 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))). 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)). 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))). 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)). 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))). 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)). 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))). 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)). 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))). 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)). 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))). 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)). 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)). 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)). 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)). 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)). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). -P(i(x,y)) | -P(x) | P(y). [assumption]. end_of_list. formulas(sos). P(i(i(x,y),i(i(y,z),i(x,z)))) # label("B"). [assumption]. P(i(i(x,i(y,z)),i(y,i(x,z)))) # label("C"). [assumption]. P(i(x,x)) # label("I"). [assumption]. P(i(i(x,i(x,y)),i(x,y))) # label("W"). [assumption]. -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]. end_of_list. formulas(demodulators). end_of_list. % 112 hints input. Term ordering decisions: Predicate symbol precedence: predicate_order([ P ]). Function symbol precedence: function_order([ U, V, V10, V11, V12, V13, V14, V15, V16, V17, V18, V19, V20, V21, V22, V6, V7, V8, V9, W, X, Y, Z, i ]). After inverse_order: (no changes). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). 1 -P(i(x,y)) | -P(x) | P(y). [assumption]. end_of_list. formulas(sos). 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]. end_of_list. formulas(demodulators). end_of_list. % 112 hints processed (0 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.02 seconds. given #1 (I,wt=12): 2 P(i(i(x,y),i(i(y,z),i(x,z)))) # label("B"). [assumption]. given #2 (I,wt=12): 3 P(i(i(x,i(y,z)),i(y,i(x,z)))) # label("C"). [assumption]. given #3 (I,wt=4): 4 P(i(x,x)) # label("I"). [assumption]. given #4 (I,wt=10): 5 P(i(i(x,i(x,y)),i(x,y))) # label("W"). [assumption]. given #5 (I,wt=94): 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]. given #6 (H,wt=8): 11 P(i(x,i(i(x,y),y))). [hyper(1,a,3,a,b,4,a)]. given #7 (H,wt=8): 17 P(i(i(i(x,x),y),y)). [hyper(1,a,11,a,b,4,a)]. given #8 (H,wt=10): 12 P(i(x,i(i(x,i(x,y)),y))). [hyper(1,a,3,a,b,5,a)]. given #9 (H,wt=12): 8 P(i(x,i(i(y,i(x,z)),i(y,z)))). [hyper(1,a,3,a,b,3,a)]. given #10 (H,wt=12): 10 P(i(i(x,y),i(i(z,x),i(z,y)))). [hyper(1,a,3,a,b,2,a)]. given #11 (H,wt=12): 14 P(i(i(i(x,i(i(x,y),y)),z),z)). [hyper(1,a,11,a,b,11,a)]. given #12 (H,wt=12): 15 P(i(i(i(i(x,y),y),z),i(x,z))). [hyper(1,a,2,a,b,11,a)]. given #13 (H,wt=12): 32 P(i(i(x,i(i(y,y),z)),i(x,z))). [hyper(1,a,17,a,b,8,a)]. given #14 (H,wt=12): 49 P(i(i(x,y),i(x,i(i(y,z),z)))). [hyper(1,a,10,a,b,11,a)]. given #15 (H,wt=12): 59 P(i(x,i(i(i(i(x,y),y),z),z))). [hyper(1,a,14,a,b,15,a)]. given #16 (H,wt=12): 68 P(i(x,i(i(y,z),i(i(x,y),z)))). [hyper(1,a,15,a,b,2,a)]. given #17 (H,wt=12): 79 P(i(x,i(i(x,y),i(i(y,z),z)))). [hyper(1,a,15,a,b,49,a)]. given #18 (H,wt=14): 25 P(i(i(i(x,i(i(x,i(x,y)),y)),z),z)). [hyper(1,a,11,a,b,12,a)]. given #19 (H,wt=16): 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)]. given #20 (H,wt=16): 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)]. given #21 (H,wt=16): 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)]. given #22 (H,wt=16): 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)]. given #23 (H,wt=16): 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)]. given #24 (H,wt=16): 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)]. given #25 (H,wt=16): 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)]. given #26 (H,wt=20): 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)]. given #27 (H,wt=20): 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)]. given #28 (H,wt=20): 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)]. given #29 (H,wt=20): 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)]. given #30 (H,wt=20): 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)]. given #31 (H,wt=20): 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)]. given #32 (H,wt=20): 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)]. given #33 (H,wt=20): 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)]. given #34 (H,wt=22): 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)]. given #35 (H,wt=24): 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)]. given #36 (H,wt=24): 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)]. given #37 (H,wt=24): 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)]. given #38 (H,wt=24): 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)]. given #39 (H,wt=24): 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)]. given #40 (H,wt=24): 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)]. given #41 (H,wt=24): 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)]. given #42 (H,wt=24): 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)]. given #43 (H,wt=26): 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)]. given #44 (H,wt=28): 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)]. given #45 (H,wt=28): 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)]. given #46 (H,wt=28): 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)]. given #47 (H,wt=28): 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)]. given #48 (H,wt=28): 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)]. given #49 (H,wt=28): 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)]. given #50 (H,wt=28): 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)]. given #51 (H,wt=28): 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)]. given #52 (H,wt=28): 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)]. given #53 (H,wt=28): 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)]. given #54 (H,wt=28): 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)]. given #55 (H,wt=32): 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)]. given #56 (H,wt=32): 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)]. given #57 (H,wt=32): 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)]. given #58 (H,wt=32): 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)]. given #59 (H,wt=32): 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)]. given #60 (H,wt=32): 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)]. given #61 (H,wt=32): 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)]. given #62 (H,wt=32): 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)]. given #63 (H,wt=34): 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)]. given #64 (H,wt=36): 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)]. given #65 (H,wt=36): 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)]. given #66 (H,wt=36): 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)]. given #67 (H,wt=36): 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)]. given #68 (H,wt=36): 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)]. given #69 (H,wt=36): 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)]. given #70 (H,wt=36): 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)]. given #71 (H,wt=36): 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)]. given #72 (H,wt=40): 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)]. given #73 (H,wt=40): 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)]. given #74 (H,wt=40): 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)]. given #75 (H,wt=40): 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)]. given #76 (H,wt=40): 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)]. given #77 (H,wt=44): 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)]. given #78 (H,wt=44): 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)]. given #79 (H,wt=46): 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)]. given #80 (H,wt=48): 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)]. given #81 (H,wt=48): 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)]. given #82 (H,wt=50): 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)]. given #83 (H,wt=54): 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)]. given #84 (H,wt=58): 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)]. given #85 (H,wt=62): 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)]. given #86 (H,wt=66): 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)]. given #87 (H,wt=70): 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)]. given #88 (H,wt=74): 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)]. given #89 (H,wt=78): 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)]. given #90 (H,wt=82): 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)]. given #91 (H,wt=86): 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)]. given #92 (H,wt=90): 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)]. given #93 (H,wt=94): 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)]. given #94 (H,wt=94): 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)]. given #95 (H,wt=94): 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)]. given #96 (H,wt=98): 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)]. given #97 (H,wt=94): 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)]. given #98 (H,wt=98): 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)]. given #99 (H,wt=94): 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)]. given #100 (H,wt=98): 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)]. given #101 (H,wt=94): 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)]. given #102 (H,wt=98): 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)]. given #103 (H,wt=94): 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)]. given #104 (H,wt=98): 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)]. given #105 (H,wt=94): 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)]. given #106 (H,wt=98): 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)]. given #107 (H,wt=94): 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)]. given #108 (H,wt=98): 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)]. given #109 (H,wt=94): 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)]. given #110 (H,wt=98): 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)]. given #111 (H,wt=94): 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)]. given #112 (H,wt=98): 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)]. given #113 (H,wt=94): 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)]. given #114 (H,wt=94): 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)]. given #115 (H,wt=94): 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)]. given #116 (H,wt=94): 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)]. -------- Proof 1 -------- "Rezus". ============================== 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 ========================== ============================== STATISTICS ============================ Given=116. Generated=11429. Kept=3433. proofs=1. Usable=117. Sos=3313. Demods=0. Limbo=0, Disabled=8. Hints=112. Weight_deleted=5371. Literals_deleted=0. Forward_subsumed=2625. Back_subsumed=3. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=0. Demod_rewrites=0. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=6.92. User_CPU=0.48, System_CPU=0.00, Wall_clock=1. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED THEOREM PROVED Exiting with 1 proof. ------ process 24977 exit (max_proofs) ------  Process 24977 exit (max_proofs) Mon Dec 3 08:50:38 2007