%
%  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.
