% % CD-derivation of the long Rezus single axiom for RI from {B,C,I,W} % % Note: This essentially is a proof checking run, since it includes % the steps from a previously found proof as hints. % clear(auto). set(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"). % A Rezus-style single axiom for RI -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. % Hints extracted from previously found proof. 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.