w2-proof-l2_1.txt

============================== prooftrans ============================
Prover9 (64) version 2017-11A (CIIRC), November 2017.
Process 1891 was started by Samiro on Xamid,
Wed Nov 22 07:32:06 2023
The command was "/usr/bin/prover9 -f w2.in".
============================== end of head ===========================

============================== end of input ==========================

============================== PROOF =================================

% -------- Comments from original proof --------
% Proof 4 at 155737.75 (+ 7295.17) seconds: L2.
% Length of proof is 799.
% Level of proof is 125.
% Maximum clause weight is 278.000.
% Given clauses 49525 (396.200 givens/level).

1 t(x) & t(i(x,y)) -> t(y) # label(MP) # label(non_clause).  [assumption].
7 t(i(i(n(p),p),p)) # label(L2) # label(non_clause) # label(goal).  [goal].
9 -t(x) | -t(i(x,y)) | t(y) # label(MP).  [clausify(1)].
10 t(i(x,i(i(y,i(x,z)),i(i(n(z),i(i(n(u),w),y)),i(u,z))))) # label(w2).  [assumption].
16 -t(i(i(n(p),p),p)) # label(L2) # answer(L2).  [deny(7)].
18 t(i(i(x,i(i(y,i(i(z,i(y,u)),i(i(n(u),i(i(n(w),v5),z)),i(w,u)))),v6)),i(i(n(v6),i(i(n(v7),v8),x)),i(v7,v6)))).  [hyper(9,a,10,a,b,10,a)].
19 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(i(n(w),i(i(n(v5),v6),n(x))),i(v5,w)),i(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9)))),y)))),i(z,i(x,y)))).  [hyper(9,a,18,a,b,18,a)].
20 t(i(i(n(i(i(n(i(i(n(x),i(i(n(y),z),u)),i(y,x))),i(i(n(w),v5),v6)),i(w,i(i(n(x),i(i(n(y),z),u)),i(y,x))))),i(i(n(v7),v8),i(u,i(v6,x)))),i(v7,i(i(n(i(i(n(x),i(i(n(y),z),u)),i(y,x))),i(i(n(w),v5),v6)),i(w,i(i(n(x),i(i(n(y),z),u)),i(y,x))))))).  [hyper(9,a,10,a,b,18,a)].
21 t(i(i(x,i(i(i(y,i(i(z,i(i(u,i(z,w)),i(i(n(w),i(i(n(v5),v6),u)),i(v5,w)))),v7)),i(i(n(v7),i(i(n(v8),v9),y)),i(v8,v7))),v10)),i(i(n(v10),i(i(n(v11),v12),x)),i(v11,v10)))).  [hyper(9,a,18,a,b,10,a)].
22 t(i(i(n(i(x,y)),i(i(n(z),u),i(n(i(x,y)),i(i(n(i(w,i(i(v5,i(w,v6)),i(i(n(v6),i(i(n(v7),v8),v5)),i(v7,v6))))),v9),i(i(i(n(v10),i(i(n(v11),v12),n(x))),i(v11,v10)),i(i(v13,i(i(v14,i(v13,v15)),i(i(n(v15),i(i(n(v16),v17),v14)),i(v16,v15)))),y)))))),i(z,i(x,y)))).  [hyper(9,a,19,a,b,18,a)].
23 t(i(i(x,i(i(i(n(i(y,z)),i(i(n(u),w),i(i(i(n(v5),i(i(n(v6),v7),n(y))),i(v6,v5)),i(i(v8,i(i(v9,i(v8,v10)),i(i(n(v10),i(i(n(v11),v12),v9)),i(v11,v10)))),z)))),i(u,i(y,z))),v13)),i(i(n(v13),i(i(n(v14),v15),x)),i(v14,v13)))).  [hyper(9,a,19,a,b,10,a)].
24 t(i(i(n(i(i(n(i(x,y)),i(i(n(z),u),i(w,i(i(v5,i(i(v6,i(v5,v7)),i(i(n(v7),i(i(n(v8),v9),v6)),i(v8,v7)))),y)))),i(z,i(x,y)))),i(i(n(v10),v11),i(n(y),i(i(n(x),v12),w)))),i(v10,i(i(n(i(x,y)),i(i(n(z),u),i(w,i(i(v5,i(i(v6,i(v5,v7)),i(i(n(v7),i(i(n(v8),v9),v6)),i(v8,v7)))),y)))),i(z,i(x,y)))))).  [hyper(9,a,10,a,b,21,a)].
25 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(i(n(w),i(i(n(v5),v6),n(x))),i(v5,w)),i(i(i(v7,i(i(v8,i(i(v9,i(v8,v10)),i(i(n(v10),i(i(n(v11),v12),v9)),i(v11,v10)))),v13)),i(i(n(v13),i(i(n(v14),v15),v7)),i(v14,v13))),y)))),i(z,i(x,y)))).  [hyper(9,a,21,a,b,18,a)].
26 t(i(i(x,i(i(i(y,i(i(i(z,i(i(u,i(i(w,i(u,v5)),i(i(n(v5),i(i(n(v6),v7),w)),i(v6,v5)))),v8)),i(i(n(v8),i(i(n(v9),v10),z)),i(v9,v8))),v11)),i(i(n(v11),i(i(n(v12),v13),y)),i(v12,v11))),v14)),i(i(n(v14),i(i(n(v15),v16),x)),i(v15,v14)))).  [hyper(9,a,21,a,b,10,a)].
33 t(i(i(n(i(i(n(i(x,y)),i(i(n(z),u),i(w,i(i(i(v5,i(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8)))),v11)),i(i(n(v11),i(i(n(v12),v13),v5)),i(v12,v11))),y)))),i(z,i(x,y)))),i(i(n(v14),v15),i(n(y),i(i(n(x),v16),w)))),i(v14,i(i(n(i(x,y)),i(i(n(z),u),i(w,i(i(i(v5,i(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8)))),v11)),i(i(n(v11),i(i(n(v12),v13),v5)),i(v12,v11))),y)))),i(z,i(x,y)))))).  [hyper(9,a,10,a,b,26,a)].
36 t(i(x,i(i(n(i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(w),v5),n(x))))),i(z,y))),i(i(n(v6),v7),w)),i(v6,i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(w),v5),n(x))))),i(z,y)))))).  [hyper(9,a,10,a,b,20,a)].
37 t(i(i(n(i(i(n(i(i(n(x),i(i(n(y),z),u)),i(y,x))),i(i(n(w),v5),v6)),i(w,i(i(n(x),i(i(n(y),z),u)),i(y,x))))),i(i(n(v7),v8),i(n(i(i(n(i(i(n(x),i(i(n(y),z),u)),i(y,x))),i(i(n(w),v5),v6)),i(w,i(i(n(x),i(i(n(y),z),u)),i(y,x))))),i(i(n(i(i(n(i(v9,v10)),i(i(n(v11),v12),i(i(i(n(v13),i(i(n(v14),v15),n(v9))),i(v14,v13)),i(i(v16,i(i(v17,i(v16,v18)),i(i(n(v18),i(i(n(v19),v20),v17)),i(v19,v18)))),v10)))),i(v11,i(v9,v10)))),v21),i(u,i(v6,x)))))),i(v7,i(i(n(i(i(n(x),i(i(n(y),z),u)),i(y,x))),i(i(n(w),v5),v6)),i(w,i(i(n(x),i(i(n(y),z),u)),i(y,x))))))).  [hyper(9,a,20,a,b,23,a)].
39 t(i(i(n(i(i(n(i(i(n(x),i(i(n(y),z),u)),i(y,x))),i(i(n(w),v5),v6)),i(w,i(i(n(x),i(i(n(y),z),u)),i(y,x))))),i(i(n(v7),v8),i(n(i(i(n(i(i(n(x),i(i(n(y),z),u)),i(y,x))),i(i(n(w),v5),v6)),i(w,i(i(n(x),i(i(n(y),z),u)),i(y,x))))),i(i(n(i(v9,i(i(v10,i(v9,v11)),i(i(n(v11),i(i(n(v12),v13),v10)),i(v12,v11))))),v14),i(u,i(v6,x)))))),i(v7,i(i(n(i(i(n(x),i(i(n(y),z),u)),i(y,x))),i(i(n(w),v5),v6)),i(w,i(i(n(x),i(i(n(y),z),u)),i(y,x))))))).  [hyper(9,a,20,a,b,18,a)].
40 t(i(i(x,i(i(i(n(i(i(n(i(i(n(y),i(i(n(z),u),w)),i(z,y))),i(i(n(v5),v6),v7)),i(v5,i(i(n(y),i(i(n(z),u),w)),i(z,y))))),i(i(n(v8),v9),i(w,i(v7,y)))),i(v8,i(i(n(i(i(n(y),i(i(n(z),u),w)),i(z,y))),i(i(n(v5),v6),v7)),i(v5,i(i(n(y),i(i(n(z),u),w)),i(z,y)))))),v10)),i(i(n(v10),i(i(n(v11),v12),x)),i(v11,v10)))).  [hyper(9,a,20,a,b,10,a)].
41 t(i(i(n(i(i(n(x),i(i(n(y),z),i(n(x),i(i(n(u),w),n(i(i(v5,i(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8)))),v11)),i(i(n(v11),i(i(n(v12),v13),v5)),i(v12,v11)))))))),i(y,x))),i(i(n(v14),v15),u)),i(v14,i(i(n(x),i(i(n(y),z),i(n(x),i(i(n(u),w),n(i(i(v5,i(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8)))),v11)),i(i(n(v11),i(i(n(v12),v13),v5)),i(v12,v11)))))))),i(y,x))))).  [hyper(9,a,18,a,b,36,a)].
42 t(i(i(n(i(i(n(x),i(i(n(y),z),i(n(x),i(i(n(u),w),n(i(v5,i(i(v6,i(v5,v7)),i(i(n(v7),i(i(n(v8),v9),v6)),i(v8,v7))))))))),i(y,x))),i(i(n(v10),v11),u)),i(v10,i(i(n(x),i(i(n(y),z),i(n(x),i(i(n(u),w),n(i(v5,i(i(v6,i(v5,v7)),i(i(n(v7),i(i(n(v8),v9),v6)),i(v8,v7))))))))),i(y,x))))).  [hyper(9,a,10,a,b,36,a)].
43 t(i(i(n(i(x,i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(i(i(n(w),i(i(n(v5),v6),n(x))),i(v5,w))),v7),n(v8))))),i(z,y)))),i(i(n(v9),v10),v8)),i(v9,i(x,i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(i(i(n(w),i(i(n(v5),v6),n(x))),i(v5,w))),v7),n(v8))))),i(z,y)))))).  [hyper(9,a,36,a,b,18,a)].
44 t(i(i(x,i(i(y,i(i(n(i(i(n(z),i(i(n(u),w),i(n(z),i(i(n(v5),v6),n(y))))),i(u,z))),i(i(n(v7),v8),v5)),i(v7,i(i(n(z),i(i(n(u),w),i(n(z),i(i(n(v5),v6),n(y))))),i(u,z))))),v9)),i(i(n(v9),i(i(n(v10),v11),x)),i(v10,v9)))).  [hyper(9,a,36,a,b,10,a)].
48 t(i(x,i(y,i(i(n(z),i(i(n(u),w),i(n(z),i(i(n(i(i(n(v5),i(i(n(v6),v7),n(y))),i(v6,v5))),v8),n(i(i(n(v9),i(i(n(v10),v11),n(x))),i(v10,v9))))))),i(u,z))))).  [hyper(9,a,10,a,b,43,a)].
49 t(i(i(n(i(x,i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(i(i(n(w),i(i(n(v5),v6),n(x))),i(v5,w))),v7),n(v8))))),i(z,y)))),i(i(n(v9),v10),i(n(i(x,i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(i(i(n(w),i(i(n(v5),v6),n(x))),i(v5,w))),v7),n(v8))))),i(z,y)))),i(i(n(i(v11,i(i(v12,i(v11,v13)),i(i(n(v13),i(i(n(v14),v15),v12)),i(v14,v13))))),v16),v8)))),i(v9,i(x,i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(i(i(n(w),i(i(n(v5),v6),n(x))),i(v5,w))),v7),n(v8))))),i(z,y)))))).  [hyper(9,a,43,a,b,18,a)].
52 t(i(x,i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(i(i(n(w),i(i(n(v5),v6),n(x))),i(v5,w))),v7),n(i(i(n(v8),i(i(n(v9),v10),n(i(v11,i(i(v12,i(v11,v13)),i(i(n(v13),i(i(n(v14),v15),v12)),i(v14,v13))))))),i(v9,v8))))))),i(z,y)))).  [hyper(9,a,10,a,b,48,a)].
54 t(i(i(x,i(i(y,i(z,i(i(n(u),i(i(n(w),v5),i(n(u),i(i(n(i(i(n(v6),i(i(n(v7),v8),n(z))),i(v7,v6))),v9),n(i(i(n(v10),i(i(n(v11),v12),n(y))),i(v11,v10))))))),i(w,u)))),v13)),i(i(n(v13),i(i(n(v14),v15),x)),i(v14,v13)))).  [hyper(9,a,48,a,b,10,a)].
56 t(i(x,i(y,i(i(n(z),i(i(n(u),w),i(n(z),i(i(n(i(i(n(v5),i(i(n(v6),v7),n(y))),i(v6,v5))),v8),n(i(v9,x)))))),i(u,z))))).  [hyper(9,a,52,a,b,43,a)].
58 t(i(i(i(i(x,i(i(y,i(i(z,i(y,u)),i(i(n(u),i(i(n(w),v5),z)),i(w,u)))),v6)),i(i(n(v6),i(i(n(v7),v8),x)),i(v7,v6))),v9),i(v10,v9))).  [hyper(9,a,52,a,b,25,a)].
59 t(i(i(i(n(i(x,i(i(y,i(x,z)),i(i(n(z),i(i(n(u),w),y)),i(u,z))))),v5),i(i(i(n(v6),i(i(n(v7),v8),n(v9))),i(v7,v6)),i(i(v10,i(i(v11,i(v10,v12)),i(i(n(v12),i(i(n(v13),v14),v11)),i(v13,v12)))),v15))),i(v9,v15))).  [hyper(9,a,52,a,b,22,a)].
60 t(i(i(x,y),i(i(n(i(i(n(y),i(i(n(z),u),w)),i(z,y))),i(i(n(v5),v6),x)),i(v5,i(i(n(y),i(i(n(z),u),w)),i(z,y)))))).  [hyper(9,a,52,a,b,20,a)].
61 t(i(i(i(x,i(i(y,i(x,z)),i(i(n(z),i(i(n(u),w),y)),i(u,z)))),v5),i(v6,v5))).  [hyper(9,a,52,a,b,19,a)].
63 t(i(x,i(y,i(i(z,i(i(u,i(i(w,i(u,v5)),i(i(n(v5),i(i(n(v6),v7),w)),i(v6,v5)))),v8)),i(i(n(v8),i(i(n(v9),v10),z)),i(v9,v8)))))).  [hyper(9,a,61,a,b,61,a)].
70 t(i(x,i(i(y,i(i(z,i(i(u,i(z,w)),i(i(n(w),i(i(n(v5),v6),u)),i(v5,w)))),v7)),i(i(n(v7),i(i(n(v8),v9),y)),i(v8,v7))))).  [hyper(9,a,10,a,b,61,a)].
73 t(i(i(n(x),i(i(n(y),z),i(i(u,i(i(w,i(u,v5)),i(i(n(v5),i(i(n(v6),v7),w)),i(v6,v5)))),x))),i(y,x))).  [hyper(9,a,61,a,b,44,a)].
75 t(i(i(x,i(i(i(i(y,i(i(z,i(y,u)),i(i(n(u),i(i(n(w),v5),z)),i(w,u)))),v6),i(v7,v6)),v8)),i(i(n(v8),i(i(n(v9),v10),x)),i(v9,v8)))).  [hyper(9,a,61,a,b,10,a)].
76 t(i(x,x)).  [hyper(9,a,52,a,b,73,a)].
84 t(i(i(n(x),i(i(n(y),z),i(n(x),i(i(n(i(u,i(i(w,i(u,v5)),i(i(n(v5),i(i(n(v6),v7),w)),i(v6,v5))))),v8),i(i(v9,i(i(v10,i(v9,v11)),i(i(n(v11),i(i(n(v12),v13),v10)),i(v12,v11)))),x))))),i(y,x))).  [hyper(9,a,73,a,b,18,a)].
85 t(i(i(x,i(i(i(n(y),i(i(n(z),u),i(i(w,i(i(v5,i(w,v6)),i(i(n(v6),i(i(n(v7),v8),v5)),i(v7,v6)))),y))),i(z,y)),v9)),i(i(n(v9),i(i(n(v10),v11),x)),i(v10,v9)))).  [hyper(9,a,73,a,b,10,a)].
86 t(i(x,i(y,i(i(z,i(y,u)),i(i(n(u),i(i(n(w),v5),z)),i(w,u)))))).  [hyper(9,a,76,a,b,61,a)].
89 t(i(i(n(x),i(i(n(y),z),i(i(u,i(i(n(i(i(n(w),i(i(n(v5),v6),i(n(w),i(i(n(v7),v8),n(u))))),i(v5,w))),i(i(n(v9),v10),v7)),i(v9,i(i(n(w),i(i(n(v5),v6),i(n(w),i(i(n(v7),v8),n(u))))),i(v5,w))))),x))),i(y,x))).  [hyper(9,a,76,a,b,44,a)].
90 t(i(i(n(i(i(n(x),i(i(n(y),z),i(n(x),i(i(n(u),w),n(i(v5,v5)))))),i(y,x))),i(i(n(v6),v7),u)),i(v6,i(i(n(x),i(i(n(y),z),i(n(x),i(i(n(u),w),n(i(v5,v5)))))),i(y,x))))).  [hyper(9,a,76,a,b,36,a)].
94 t(i(i(x,i(i(y,y),z)),i(i(n(z),i(i(n(u),w),x)),i(u,z)))).  [hyper(9,a,76,a,b,10,a)].
95 t(i(i(n(x),i(i(n(y),z),i(i(u,u),x))),i(y,x))).  [hyper(9,a,76,a,b,94,a)].
101 t(i(i(n(i(i(n(x),i(i(n(y),z),i(u,x))),i(y,x))),i(i(n(w),v5),u)),i(w,i(i(n(x),i(i(n(y),z),i(u,x))),i(y,x))))).  [hyper(9,a,10,a,b,94,a)].
107 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(i(n(w),i(i(n(v5),v6),n(x))),i(v5,w)),i(i(v7,v7),y)))),i(z,i(x,y)))).  [hyper(9,a,94,a,b,18,a)].
116 t(i(i(x,i(i(y,i(z,i(i(u,i(z,w)),i(i(n(w),i(i(n(v5),v6),u)),i(v5,w))))),v7)),i(i(n(v7),i(i(n(v8),v9),x)),i(v8,v7)))).  [hyper(9,a,86,a,b,10,a)].
117 t(i(i(i(x,x),y),i(z,y))).  [hyper(9,a,52,a,b,107,a)].
164 t(i(i(n(i(i(n(i(i(x,i(y,z)),i(i(n(z),i(i(n(u),w),x)),i(u,z)))),i(i(n(v5),v6),v7)),i(v5,i(i(x,i(y,z)),i(i(n(z),i(i(n(u),w),x)),i(u,z)))))),i(i(n(v8),v9),y)),i(v8,i(i(n(i(i(x,i(y,z)),i(i(n(z),i(i(n(u),w),x)),i(u,z)))),i(i(n(v5),v6),v7)),i(v5,i(i(x,i(y,z)),i(i(n(z),i(i(n(u),w),x)),i(u,z)))))))).  [hyper(9,a,10,a,b,60,a)].
169 t(i(i(x,i(i(i(y,z),i(i(n(i(i(n(z),i(i(n(u),w),v5)),i(u,z))),i(i(n(v6),v7),y)),i(v6,i(i(n(z),i(i(n(u),w),v5)),i(u,z))))),v8)),i(i(n(v8),i(i(n(v9),v10),x)),i(v9,v8)))).  [hyper(9,a,60,a,b,10,a)].
184 t(i(i(x,i(i(y,i(i(z,i(i(u,i(i(w,i(u,v5)),i(i(n(v5),i(i(n(v6),v7),w)),i(v6,v5)))),v8)),i(i(n(v8),i(i(n(v9),v10),z)),i(v9,v8)))),v11)),i(i(n(v11),i(i(n(v12),v13),x)),i(v12,v11)))).  [hyper(9,a,70,a,b,10,a)].
186 t(i(x,i(i(n(y),i(i(n(z),u),i(i(i(n(w),i(i(n(v5),v6),n(x))),i(v5,w)),y))),i(z,y)))).  [hyper(9,a,70,a,b,101,a)].
216 t(i(i(n(x),i(i(n(y),z),i(i(i(n(u),i(i(n(w),v5),n(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8))))))),i(w,u)),x))),i(y,x))).  [hyper(9,a,10,a,b,186,a)].
221 t(i(i(x,i(i(y,i(i(n(z),i(i(n(u),w),i(i(i(n(v5),i(i(n(v6),v7),n(y))),i(v6,v5)),z))),i(u,z))),v8)),i(i(n(v8),i(i(n(v9),v10),x)),i(v9,v8)))).  [hyper(9,a,186,a,b,10,a)].
246 t(i(i(n(i(i(n(x),i(i(n(y),z),i(n(x),i(i(n(i(i(n(u),i(i(n(w),v5),n(i(v6,i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9)))))))),i(w,u))),v12),n(i(i(n(v13),i(i(n(v14),v15),n(v16))),i(v14,v13))))))),i(y,x))),i(i(n(v17),v18),v16)),i(v17,i(i(n(x),i(i(n(y),z),i(n(x),i(i(n(i(i(n(u),i(i(n(w),v5),n(i(v6,i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9)))))))),i(w,u))),v12),n(i(i(n(v13),i(i(n(v14),v15),n(v16))),i(v14,v13))))))),i(y,x))))).  [hyper(9,a,48,a,b,116,a)].
249 t(i(i(n(i(x,i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(i(i(w,i(i(n(x),v5),v6)),i(i(n(v6),i(i(n(v7),v8),w)),i(v7,v6)))),v9),n(v10))))),i(z,y)))),i(i(n(v11),v12),v10)),i(v11,i(x,i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(i(i(w,i(i(n(x),v5),v6)),i(i(n(v6),i(i(n(v7),v8),w)),i(v7,v6)))),v9),n(v10))))),i(z,y)))))).  [hyper(9,a,36,a,b,116,a)].
259 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(i(n(w),i(i(n(v5),v6),n(x))),i(v5,w)),i(i(v7,i(v8,i(i(v9,i(v8,v10)),i(i(n(v10),i(i(n(v11),v12),v9)),i(v11,v10))))),y)))),i(z,i(x,y)))).  [hyper(9,a,116,a,b,18,a)].
284 t(i(x,i(y,i(i(n(i(z,u)),i(i(n(w),v5),i(i(i(n(v6),i(i(n(v7),v8),n(z))),i(v7,v6)),i(i(v9,i(i(v10,i(v9,v11)),i(i(n(v11),i(i(n(v12),v13),v10)),i(v12,v11)))),u)))),i(w,i(z,u)))))).  [hyper(9,a,58,a,b,58,a)].
287 t(i(x,i(i(n(i(y,z)),i(i(n(u),w),i(i(i(n(v5),i(i(n(v6),v7),n(y))),i(v6,v5)),i(i(v8,i(i(v9,i(v8,v10)),i(i(n(v10),i(i(n(v11),v12),v9)),i(v11,v10)))),z)))),i(u,i(y,z))))).  [hyper(9,a,18,a,b,58,a)].
288 t(i(x,i(i(y,i(i(i(z,i(i(u,i(i(w,i(u,v5)),i(i(n(v5),i(i(n(v6),v7),w)),i(v6,v5)))),v8)),i(i(n(v8),i(i(n(v9),v10),z)),i(v9,v8))),v11)),i(i(n(v11),i(i(n(v12),v13),y)),i(v12,v11))))).  [hyper(9,a,10,a,b,58,a)].
300 t(i(i(n(x),i(i(n(y),z),i(i(i(i(u,i(i(w,i(u,v5)),i(i(n(v5),i(i(n(v6),v7),w)),i(v6,v5)))),v8),i(v9,v8)),x))),i(y,x))).  [hyper(9,a,76,a,b,75,a)].
310 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(i(n(w),i(i(n(v5),v6),n(x))),i(v5,w)),i(i(i(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9)))),v12),i(v13,v12)),y)))),i(z,i(x,y)))).  [hyper(9,a,75,a,b,18,a)].
311 t(i(i(x,i(i(i(y,i(i(i(i(z,i(i(u,i(z,w)),i(i(n(w),i(i(n(v5),v6),u)),i(v5,w)))),v7),i(v8,v7)),v9)),i(i(n(v9),i(i(n(v10),v11),y)),i(v10,v9))),v12)),i(i(n(v12),i(i(n(v13),v14),x)),i(v13,v12)))).  [hyper(9,a,75,a,b,10,a)].
312 t(i(x,i(i(n(y),i(i(n(z),u),i(i(w,i(i(v5,i(w,v6)),i(i(n(v6),i(i(n(v7),v8),v5)),i(v7,v6)))),y))),i(z,y)))).  [hyper(9,a,86,a,b,300,a)].
329 t(i(i(x,i(i(y,i(i(n(z),i(i(n(u),w),i(i(v5,i(i(v6,i(v5,v7)),i(i(n(v7),i(i(n(v8),v9),v6)),i(v8,v7)))),z))),i(u,z))),v10)),i(i(n(v10),i(i(n(v11),v12),x)),i(v11,v10)))).  [hyper(9,a,312,a,b,10,a)].
343 t(i(i(n(i(x,x)),i(i(n(y),z),u)),i(y,i(x,x)))).  [hyper(9,a,312,a,b,221,a)].
353 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(w,x),i(i(v5,v5),y)))),i(z,i(x,y)))).  [hyper(9,a,94,a,b,221,a)].
355 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(w,x),i(i(i(i(v5,i(i(v6,i(v5,v7)),i(i(n(v7),i(i(n(v8),v9),v6)),i(v8,v7)))),v10),i(v11,v10)),y)))),i(z,i(x,y)))).  [hyper(9,a,75,a,b,221,a)].
357 t(i(i(n(i(x,i(i(n(y),i(i(n(z),u),w)),i(z,y)))),i(i(n(v5),v6),i(i(v7,x),y))),i(v5,i(x,i(i(n(y),i(i(n(z),u),w)),i(z,y)))))).  [hyper(9,a,60,a,b,221,a)].
359 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(w,x),i(i(v5,i(i(n(i(i(n(v6),i(i(n(v7),v8),i(n(v6),i(i(n(v9),v10),n(v5))))),i(v7,v6))),i(i(n(v11),v12),v9)),i(v11,i(i(n(v6),i(i(n(v7),v8),i(n(v6),i(i(n(v9),v10),n(v5))))),i(v7,v6))))),y)))),i(z,i(x,y)))).  [hyper(9,a,44,a,b,221,a)].
360 t(i(i(n(i(x,i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(i(w,x)),v5),n(v6))))),i(z,y)))),i(i(n(v7),v8),v6)),i(v7,i(x,i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(i(w,x)),v5),n(v6))))),i(z,y)))))).  [hyper(9,a,36,a,b,221,a)].
361 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(w,x),i(i(i(v5,i(i(i(v6,i(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9)))),v12)),i(i(n(v12),i(i(n(v13),v14),v6)),i(v13,v12))),v15)),i(i(n(v15),i(i(n(v16),v17),v5)),i(v16,v15))),y)))),i(z,i(x,y)))).  [hyper(9,a,26,a,b,221,a)].
362 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(w,x),i(i(i(n(i(v5,v6)),i(i(n(v7),v8),i(i(i(n(v9),i(i(n(v10),v11),n(v5))),i(v10,v9)),i(i(v12,i(i(v13,i(v12,v14)),i(i(n(v14),i(i(n(v15),v16),v13)),i(v15,v14)))),v6)))),i(v7,i(v5,v6))),y)))),i(z,i(x,y)))).  [hyper(9,a,23,a,b,221,a)].
363 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(w,x),i(i(i(v5,i(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8)))),v11)),i(i(n(v11),i(i(n(v12),v13),v5)),i(v12,v11))),y)))),i(z,i(x,y)))).  [hyper(9,a,21,a,b,221,a)].
365 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(w,x),i(i(v5,i(i(v6,i(v5,v7)),i(i(n(v7),i(i(n(v8),v9),v6)),i(v8,v7)))),y)))),i(z,i(x,y)))).  [hyper(9,a,18,a,b,221,a)].
370 t(i(x,i(i(n(i(y,z)),i(i(n(u),w),i(i(v5,y),i(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8)))),z)))),i(u,i(y,z))))).  [hyper(9,a,221,a,b,58,a)].
375 t(i(x,i(y,y))).  [hyper(9,a,312,a,b,343,a)].
378 t(i(x,i(y,i(z,z)))).  [hyper(9,a,343,a,b,61,a)].
400 t(i(i(x,i(i(y,i(z,z)),u)),i(i(n(u),i(i(n(w),v5),x)),i(w,u)))).  [hyper(9,a,375,a,b,10,a)].
401 t(i(x,i(i(i(y,i(i(z,i(y,u)),i(i(n(u),i(i(n(w),v5),z)),i(w,u)))),v6),i(v7,v6)))).  [hyper(9,a,378,a,b,300,a)].
403 t(i(x,i(i(n(y),i(i(n(z),u),n(i(w,i(i(v5,i(w,v6)),i(i(n(v6),i(i(n(v7),v8),v5)),i(v7,v6))))))),i(z,y)))).  [hyper(9,a,378,a,b,216,a)].
414 t(i(i(x,i(i(y,i(z,i(u,u))),w)),i(i(n(w),i(i(n(v5),v6),x)),i(v5,w)))).  [hyper(9,a,378,a,b,10,a)].
415 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(n(x),w),i(i(v5,i(v6,v6)),y)))),i(z,i(x,y)))).  [hyper(9,a,400,a,b,400,a)].
425 t(i(i(n(i(i(n(x),i(i(n(y),z),i(u,x))),i(y,x))),i(i(n(w),v5),i(n(i(i(n(x),i(i(n(y),z),i(u,x))),i(y,x))),i(i(n(i(v6,i(v7,v7))),v8),u)))),i(w,i(i(n(x),i(i(n(y),z),i(u,x))),i(y,x))))).  [hyper(9,a,101,a,b,400,a)].
441 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(w,x),i(i(v5,i(v6,v6)),y)))),i(z,i(x,y)))).  [hyper(9,a,400,a,b,221,a)].
454 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(w,w),i(i(v5,i(v6,i(v7,v7))),y)))),i(z,i(x,y)))).  [hyper(9,a,414,a,b,414,a)].
456 t(i(i(n(i(x,i(y,i(z,z)))),i(i(n(u),w),v5)),i(u,i(x,i(y,i(z,z)))))).  [hyper(9,a,375,a,b,414,a)].
482 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(w,x),i(i(v5,i(v6,i(v7,v7))),y)))),i(z,i(x,y)))).  [hyper(9,a,414,a,b,221,a)].
497 t(i(x,i(y,i(z,i(u,i(w,w)))))).  [hyper(9,a,456,a,b,61,a)].
524 t(i(i(n(x),i(i(n(y),z),n(i(u,i(i(w,i(u,v5)),i(i(n(v5),i(i(n(v6),v7),w)),i(v6,v5))))))),i(y,x))).  [hyper(9,a,497,a,b,403,a)].
528 t(i(i(x,i(i(y,i(i(n(z),i(i(n(u),w),n(i(v5,i(i(v6,i(v5,v7)),i(i(n(v7),i(i(n(v8),v9),v6)),i(v8,v7))))))),i(u,z))),v10)),i(i(n(v10),i(i(n(v11),v12),x)),i(v11,v10)))).  [hyper(9,a,403,a,b,10,a)].
545 t(i(i(x,i(i(i(n(y),i(i(n(z),u),n(i(w,i(i(v5,i(w,v6)),i(i(n(v6),i(i(n(v7),v8),v5)),i(v7,v6))))))),i(z,y)),v9)),i(i(n(v9),i(i(n(v10),v11),x)),i(v10,v9)))).  [hyper(9,a,524,a,b,10,a)].
553 t(i(x,i(i(i(n(x),y),z),i(u,z)))).  [hyper(9,a,86,a,b,365,a)].
554 t(i(x,i(i(i(n(i(y,i(i(z,i(y,u)),i(i(n(u),i(i(n(w),v5),z)),i(w,u))))),v6),n(x)),v7))).  [hyper(9,a,70,a,b,365,a)].
563 t(i(x,i(y,i(i(i(n(i(z,i(i(u,i(z,w)),i(i(n(w),i(i(n(v5),v6),u)),i(v5,w))))),v7),n(y)),v8)))).  [hyper(9,a,365,a,b,61,a)].
572 t(i(i(n(i(x,y)),i(i(n(z),u),i(n(i(x,y)),i(i(n(i(w,i(i(v5,i(w,v6)),i(i(n(v6),i(i(n(v7),v8),v5)),i(v7,v6))))),v9),i(i(v10,x),i(i(v11,i(i(v12,i(v11,v13)),i(i(n(v13),i(i(n(v14),v15),v12)),i(v14,v13)))),y)))))),i(z,i(x,y)))).  [hyper(9,a,365,a,b,18,a)].
573 t(i(i(x,i(i(i(n(i(y,z)),i(i(n(u),w),i(i(v5,y),i(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8)))),z)))),i(u,i(y,z))),v11)),i(i(n(v11),i(i(n(v12),v13),x)),i(v12,v11)))).  [hyper(9,a,365,a,b,10,a)].
575 t(i(i(i(n(i(i(n(x),i(i(n(y),z),n(i(u,i(i(w,i(u,v5)),i(i(n(v5),i(i(n(v6),v7),w)),i(v6,v5))))))),i(y,x))),v8),v9),i(v10,v9))).  [hyper(9,a,524,a,b,553,a)].
622 t(i(i(i(n(i(x,i(i(y,i(x,z)),i(i(n(z),i(i(n(u),w),y)),i(u,z))))),v5),v6),i(v7,v6))).  [hyper(9,a,10,a,b,553,a)].
626 t(i(i(n(i(x,i(n(y),z))),i(i(n(u),w),y)),i(u,i(x,i(n(y),z))))).  [hyper(9,a,553,a,b,94,a)].
638 t(i(x,i(y,i(z,i(i(u,i(z,w)),i(i(n(w),i(i(n(v5),v6),u)),i(v5,w))))))).  [hyper(9,a,524,a,b,622,a)].
641 t(i(x,i(n(i(y,i(i(z,i(y,u)),i(i(n(u),i(i(n(w),v5),z)),i(w,u))))),v6))).  [hyper(9,a,76,a,b,622,a)].
645 t(i(x,i(i(y,i(i(n(i(z,i(i(u,i(z,w)),i(i(n(w),i(i(n(v5),v6),u)),i(v5,w))))),v7),v8)),i(i(n(v8),i(i(n(v9),v10),y)),i(v9,v8))))).  [hyper(9,a,10,a,b,622,a)].
647 t(i(i(n(x),i(i(n(y),z),i(i(n(i(u,i(i(w,i(u,v5)),i(i(n(v5),i(i(n(v6),v7),w)),i(v6,v5))))),v8),x))),i(y,x))).  [hyper(9,a,622,a,b,414,a)].
650 t(i(x,i(y,i(i(z,i(i(n(i(u,i(i(w,i(u,v5)),i(i(n(v5),i(i(n(v6),v7),w)),i(v6,v5))))),v8),v9)),i(i(n(v9),i(i(n(v10),v11),z)),i(v10,v9)))))).  [hyper(9,a,622,a,b,61,a)].
660 t(i(x,i(i(y,i(i(i(n(z),i(i(n(u),w),n(i(v5,i(i(v6,i(v5,v7)),i(i(n(v7),i(i(n(v8),v9),v6)),i(v8,v7))))))),i(u,z)),v10)),i(i(n(v10),i(i(n(v11),v12),y)),i(v11,v10))))).  [hyper(9,a,638,a,b,216,a)].
667 t(i(x,i(y,i(i(n(z),i(i(n(u),w),i(n(z),i(i(n(i(i(n(v5),i(i(n(v6),v7),n(y))),i(v6,v5))),v8),n(i(v9,i(i(v10,i(v9,v11)),i(i(n(v11),i(i(n(v12),v13),v10)),i(v12,v11))))))))),i(u,z))))).  [hyper(9,a,638,a,b,43,a)].
669 t(i(i(x,i(i(y,i(z,i(u,i(i(w,i(u,v5)),i(i(n(v5),i(i(n(v6),v7),w)),i(v6,v5)))))),v8)),i(i(n(v8),i(i(n(v9),v10),x)),i(v9,v8)))).  [hyper(9,a,638,a,b,10,a)].
670 t(i(n(i(x,i(i(y,i(x,z)),i(i(n(z),i(i(n(u),w),y)),i(u,z))))),v5)).  [hyper(9,a,641,a,b,641,a)].
684 t(i(i(x,i(i(n(i(y,i(i(z,i(y,u)),i(i(n(u),i(i(n(w),v5),z)),i(w,u))))),v6),v7)),i(i(n(v7),i(i(n(v8),v9),x)),i(v8,v7)))).  [hyper(9,a,670,a,b,10,a)].
761 t(i(i(i(n(i(x,i(i(y,i(x,z)),i(i(n(z),i(i(n(u),w),y)),i(u,z))))),v5),n(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8)))))),v11)).  [hyper(9,a,10,a,b,554,a)].
772 t(i(i(n(i(i(n(x),i(i(n(y),z),i(n(x),i(i(n(u),w),n(i(v5,i(i(i(n(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8))))),v11),n(v5)),v12))))))),i(y,x))),i(i(n(v13),v14),u)),i(v13,i(i(n(x),i(i(n(y),z),i(n(x),i(i(n(u),w),n(i(v5,i(i(i(n(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8))))),v11),n(v5)),v12))))))),i(y,x))))).  [hyper(9,a,554,a,b,36,a)].
773 t(i(i(x,i(i(y,i(i(i(n(i(z,i(i(u,i(z,w)),i(i(n(w),i(i(n(v5),v6),u)),i(v5,w))))),v7),n(y)),v8)),v9)),i(i(n(v9),i(i(n(v10),v11),x)),i(v10,v9)))).  [hyper(9,a,554,a,b,10,a)].
790 t(i(x,i(i(n(i(i(n(y),i(i(n(z),u),i(i(n(i(w,i(i(v5,i(w,v6)),i(i(n(v6),i(i(n(v7),v8),v5)),i(v7,v6))))),v9),n(i(n(x),v10))))),i(z,y))),i(i(n(v11),v12),v13)),i(v11,i(i(n(y),i(i(n(z),u),i(i(n(i(w,i(i(v5,i(w,v6)),i(i(n(v6),i(i(n(v7),v8),v5)),i(v7,v6))))),v9),n(i(n(x),v10))))),i(z,y)))))).  [hyper(9,a,563,a,b,20,a)].
792 t(i(i(x,i(i(y,i(z,i(i(i(n(i(u,i(i(w,i(u,v5)),i(i(n(v5),i(i(n(v6),v7),w)),i(v6,v5))))),v8),n(z)),v9))),v10)),i(i(n(v10),i(i(n(v11),v12),x)),i(v11,v10)))).  [hyper(9,a,563,a,b,10,a)].
875 t(i(x,i(y,i(z,i(u,i(i(w,i(u,v5)),i(i(n(v5),i(i(n(v6),v7),w)),i(v6,v5)))))))).  [hyper(9,a,647,a,b,61,a)].
899 t(i(i(n(i(n(i(x,i(i(y,i(x,z)),i(i(n(z),i(i(n(u),w),y)),i(u,z))))),v5)),i(i(n(v6),v7),v8)),i(v6,i(n(i(x,i(i(y,i(x,z)),i(i(n(z),i(i(n(u),w),y)),i(u,z))))),v5)))).  [hyper(9,a,375,a,b,684,a)].
920 t(i(i(x,i(i(i(y,i(i(n(i(z,i(i(u,i(z,w)),i(i(n(w),i(i(n(v5),v6),u)),i(v5,w))))),v7),v8)),i(i(n(v8),i(i(n(v9),v10),y)),i(v9,v8))),v11)),i(i(n(v11),i(i(n(v12),v13),x)),i(v12,v11)))).  [hyper(9,a,684,a,b,10,a)].
950 t(i(x,i(i(n(y),i(i(n(z),u),n(i(i(n(w),i(i(n(v5),v6),n(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9))))))),i(v5,w))))),i(z,y)))).  [hyper(9,a,684,a,b,575,a)].
957 t(i(x,i(i(y,i(i(n(i(i(n(z),i(i(n(u),w),n(i(v5,i(i(v6,i(v5,v7)),i(i(n(v7),i(i(n(v8),v9),v6)),i(v8,v7))))))),i(u,z))),v10),v11)),i(i(n(v11),i(i(n(v12),v13),y)),i(v12,v11))))).  [hyper(9,a,10,a,b,575,a)].
991 t(i(i(n(i(x,i(i(y,i(i(i(n(z),i(i(n(u),w),n(v5))),i(u,z)),v6)),i(i(n(v6),i(i(n(v7),v8),y)),i(v7,v6))))),i(i(n(v9),v10),v5)),i(v9,i(x,i(i(y,i(i(i(n(z),i(i(n(u),w),n(v5))),i(u,z)),v6)),i(i(n(v6),i(i(n(v7),v8),y)),i(v7,v6))))))).  [hyper(9,a,186,a,b,669,a)].
1004 t(i(i(n(i(x,i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(i(w,i(i(v5,i(w,v6)),i(i(n(v6),i(i(n(v7),v8),v5)),i(v7,v6))))),v9),n(v10))))),i(z,y)))),i(i(n(v11),v12),v10)),i(v11,i(x,i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(i(w,i(i(v5,i(w,v6)),i(i(n(v6),i(i(n(v7),v8),v5)),i(v7,v6))))),v9),n(v10))))),i(z,y)))))).  [hyper(9,a,36,a,b,669,a)].
1034 t(i(x,i(y,i(i(n(i(i(z,i(i(u,y),w)),i(i(n(w),i(i(n(v5),v6),z)),i(v5,w)))),i(i(n(v7),v8),v9)),i(v7,i(i(z,i(i(u,y),w)),i(i(n(w),i(i(n(v5),v6),z)),i(v5,w)))))))).  [hyper(9,a,638,a,b,357,a)].
1056 t(i(x,i(y,i(i(i(n(z),u),n(y)),i(i(n(i(z,w)),i(i(n(v5),v6),v7)),i(v5,i(z,w))))))).  [hyper(9,a,357,a,b,61,a)].
1213 t(i(i(x,i(i(y,i(z,i(i(i(n(u),w),n(z)),i(i(n(i(u,v5)),i(i(n(v6),v7),v8)),i(v6,i(u,v5)))))),v9)),i(i(n(v9),i(i(n(v10),v11),x)),i(v10,v9)))).  [hyper(9,a,1056,a,b,10,a)].
1699 t(i(i(i(i(i(x,i(i(y,i(x,z)),i(i(n(z),i(i(n(u),w),y)),i(u,z)))),v5),i(v6,v5)),v7),i(v8,v7))).  [hyper(9,a,403,a,b,355,a)].
1739 t(i(x,i(y,i(z,i(i(u,i(i(w,i(i(v5,i(w,v6)),i(i(n(v6),i(i(n(v7),v8),v5)),i(v7,v6)))),v9)),i(i(n(v9),i(i(n(v10),v11),u)),i(v10,v9))))))).  [hyper(9,a,61,a,b,1699,a)].
1902 t(i(i(n(x),i(i(n(y),z),i(i(n(i(u,i(i(w,i(u,v5)),i(i(n(v5),i(i(n(v6),v7),w)),i(v6,v5))))),v8),n(i(v9,i(i(v10,i(v9,v11)),i(i(n(v11),i(i(n(v12),v13),v10)),i(v12,v11)))))))),i(y,x))).  [hyper(9,a,761,a,b,1213,a)].
1926 t(i(i(n(x),i(i(n(y),z),i(i(u,i(i(i(n(i(w,i(i(v5,i(w,v6)),i(i(n(v6),i(i(n(v7),v8),v5)),i(v7,v6))))),v9),n(u)),v10)),x))),i(y,x))).  [hyper(9,a,76,a,b,773,a)].
1929 t(i(i(n(i(i(n(x),i(i(n(y),z),u)),i(y,x))),i(i(n(w),v5),i(i(n(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8))))),v11),n(u)))),i(w,i(i(n(x),i(i(n(y),z),u)),i(y,x))))).  [hyper(9,a,10,a,b,773,a)].
1950 t(i(i(x,i(i(i(y,i(i(z,i(i(i(n(i(u,i(i(w,i(u,v5)),i(i(n(v5),i(i(n(v6),v7),w)),i(v6,v5))))),v8),n(z)),v9)),v10)),i(i(n(v10),i(i(n(v11),v12),y)),i(v11,v10))),v13)),i(i(n(v13),i(i(n(v14),v15),x)),i(v14,v13)))).  [hyper(9,a,773,a,b,10,a)].
1951 t(i(x,i(i(y,i(i(z,i(i(i(n(i(u,i(i(w,i(u,v5)),i(i(n(v5),i(i(n(v6),v7),w)),i(v6,v5))))),v8),n(z)),v9)),v10)),i(i(n(v10),i(i(n(v11),v12),y)),i(v11,v10))))).  [hyper(9,a,638,a,b,1926,a)].
2110 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(w,x),i(i(v5,i(v6,i(i(i(n(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9))))),v12),n(v6)),v13))),y)))),i(z,i(x,y)))).  [hyper(9,a,792,a,b,221,a)].
2220 t(i(i(n(i(i(n(x),i(i(n(y),z),i(n(x),i(i(n(i(n(i(u,i(i(w,i(u,v5)),i(i(n(v5),i(i(n(v6),v7),w)),i(v6,v5))))),v8)),v9),n(i(v10,i(i(v11,i(v10,v12)),i(i(n(v12),i(i(n(v13),v14),v11)),i(v13,v12))))))))),i(y,x))),i(i(n(v15),v16),v17)),i(v15,i(i(n(x),i(i(n(y),z),i(n(x),i(i(n(i(n(i(u,i(i(w,i(u,v5)),i(i(n(v5),i(i(n(v6),v7),w)),i(v6,v5))))),v8)),v9),n(i(v10,i(i(v11,i(v10,v12)),i(i(n(v12),i(i(n(v13),v14),v11)),i(v13,v12))))))))),i(y,x))))).  [hyper(9,a,645,a,b,545,a)].
2222 t(i(i(n(i(x,i(y,z))),i(i(n(u),w),z)),i(u,i(x,i(y,z))))).  [hyper(9,a,553,a,b,545,a)].
2233 t(i(i(n(x),i(i(n(y),z),i(n(x),i(i(n(i(i(n(u),i(i(n(w),v5),n(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8))))))),i(w,u))),v11),i(i(v12,i(i(v13,i(v12,v14)),i(i(n(v14),i(i(n(v15),v16),v13)),i(v15,v14)))),x))))),i(y,x))).  [hyper(9,a,73,a,b,545,a)].
2235 t(i(i(n(i(i(n(x),i(i(n(y),z),i(n(x),i(i(n(i(i(n(u),i(i(n(w),v5),n(i(i(n(v6),i(i(n(v7),v8),n(i(v9,i(i(v10,i(v9,v11)),i(i(n(v11),i(i(n(v12),v13),v10)),i(v12,v11))))))),i(v7,v6))))),i(w,u))),v14),n(i(v15,v16)))))),i(y,x))),i(i(n(v17),v18),v16)),i(v17,i(i(n(x),i(i(n(y),z),i(n(x),i(i(n(i(i(n(u),i(i(n(w),v5),n(i(i(n(v6),i(i(n(v7),v8),n(i(v9,i(i(v10,i(v9,v11)),i(i(n(v11),i(i(n(v12),v13),v10)),i(v12,v11))))))),i(v7,v6))))),i(w,u))),v14),n(i(v15,v16)))))),i(y,x))))).  [hyper(9,a,56,a,b,545,a)].
2253 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(w,x),i(i(i(n(v5),i(i(n(v6),v7),n(i(v8,i(i(v9,i(v8,v10)),i(i(n(v10),i(i(n(v11),v12),v9)),i(v11,v10))))))),i(v6,v5)),y)))),i(z,i(x,y)))).  [hyper(9,a,545,a,b,221,a)].
2262 t(i(x,i(y,i(z,i(i(n(u),i(i(n(w),v5),n(x))),i(w,u)))))).  [hyper(9,a,1951,a,b,2222,a)].
2267 t(i(x,i(y,i(z,i(u,x))))).  [hyper(9,a,950,a,b,2222,a)].
2375 t(i(x,i(y,i(z,i(i(n(i(u,w)),i(i(n(v5),v6),i(i(v7,u),i(i(v8,i(i(v9,i(v8,v10)),i(i(n(v10),i(i(n(v11),v12),v9)),i(v11,v10)))),w)))),i(v5,i(u,w))))))).  [hyper(9,a,365,a,b,2267,a)].
2420 t(i(i(n(i(i(n(x),i(i(n(y),z),i(n(x),i(i(n(u),w),n(i(v5,i(v6,i(v7,i(v8,v5))))))))),i(y,x))),i(i(n(v9),v10),u)),i(v9,i(i(n(x),i(i(n(y),z),i(n(x),i(i(n(u),w),n(i(v5,i(v6,i(v7,i(v8,v5))))))))),i(y,x))))).  [hyper(9,a,2267,a,b,36,a)].
2421 t(i(i(x,i(i(y,i(z,i(u,i(w,y)))),v5)),i(i(n(v5),i(i(n(v6),v7),x)),i(v6,v5)))).  [hyper(9,a,2267,a,b,10,a)].
2528 t(i(i(x,i(i(y,i(z,i(u,i(i(n(w),i(i(n(v5),v6),n(y))),i(v5,w))))),v7)),i(i(n(v7),i(i(n(v8),v9),x)),i(v8,v7)))).  [hyper(9,a,2262,a,b,10,a)].
2552 t(i(i(n(i(x,i(y,i(z,i(u,i(n(w),v5)))))),i(i(n(v6),v7),w)),i(v6,i(x,i(y,i(z,i(u,i(n(w),v5)))))))).  [hyper(9,a,553,a,b,2421,a)].
2583 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(w,i(v5,n(y))),i(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8)))),y)))),i(z,i(x,y)))).  [hyper(9,a,18,a,b,2421,a)].
2598 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(w,x),i(i(v5,i(v6,i(v7,i(v8,v5)))),y)))),i(z,i(x,y)))).  [hyper(9,a,2421,a,b,221,a)].
2606 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(i(n(w),i(i(n(v5),v6),n(x))),i(v5,w)),i(i(v7,i(v8,i(v9,i(v10,v7)))),y)))),i(z,i(x,y)))).  [hyper(9,a,2421,a,b,18,a)].
2742 t(i(x,i(y,i(i(n(i(z,i(u,w))),i(i(n(v5),v6),w)),i(v5,i(z,i(u,w))))))).  [hyper(9,a,1739,a,b,2606,a)].
2745 t(i(x,i(y,i(z,y)))).  [hyper(9,a,650,a,b,2606,a)].
2784 t(i(x,i(i(n(i(y,i(z,u))),i(i(n(w),v5),u)),i(w,i(y,i(z,u)))))).  [hyper(9,a,2742,a,b,2742,a)].
2821 t(i(i(x,i(i(y,i(i(n(i(z,i(u,w))),i(i(n(v5),v6),w)),i(v5,i(z,i(u,w))))),v7)),i(i(n(v7),i(i(n(v8),v9),x)),i(v8,v7)))).  [hyper(9,a,2784,a,b,10,a)].
2913 t(i(x,i(y,x))).  [hyper(9,a,1951,a,b,2583,a)].
2955 t(i(x,i(y,i(i(n(i(z,u)),i(i(n(w),v5),i(i(v6,z),i(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9)))),u)))),i(w,i(z,u)))))).  [hyper(9,a,2821,a,b,2375,a)].
2956 t(i(x,i(y,i(z,i(i(i(n(i(u,i(i(w,i(u,v5)),i(i(n(v5),i(i(n(v6),v7),w)),i(v6,v5))))),v8),n(z)),v9))))).  [hyper(9,a,2375,a,b,2583,a)].
2984 t(i(x,i(i(n(y),i(i(n(z),u),i(i(w,i(i(i(n(i(v5,i(i(v6,i(v5,v7)),i(i(n(v7),i(i(n(v8),v9),v6)),i(v8,v7))))),v10),n(w)),v11)),y))),i(z,y)))).  [hyper(9,a,2956,a,b,101,a)].
3095 t(i(i(n(i(i(n(x),i(i(n(y),z),i(n(x),i(i(n(u),w),i(i(v5,i(i(v6,i(v5,v7)),i(i(n(v7),i(i(n(v8),v9),v6)),i(v8,v7)))),x))))),i(y,x))),i(i(n(v10),v11),u)),i(v10,i(i(n(x),i(i(n(y),z),i(n(x),i(i(n(u),w),i(i(v5,i(i(v6,i(v5,v7)),i(i(n(v7),i(i(n(v8),v9),v6)),i(v8,v7)))),x))))),i(y,x))))).  [hyper(9,a,10,a,b,85,a)].
3112 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(n(x),w),i(i(i(n(v5),i(i(n(v6),v7),i(i(v8,i(i(v9,i(v8,v10)),i(i(n(v10),i(i(n(v11),v12),v9)),i(v11,v10)))),v5))),i(v6,v5)),y)))),i(z,i(x,y)))).  [hyper(9,a,85,a,b,400,a)].
3113 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(w,x),i(i(i(n(v5),i(i(n(v6),v7),i(i(v8,i(i(v9,i(v8,v10)),i(i(n(v10),i(i(n(v11),v12),v9)),i(v11,v10)))),v5))),i(v6,v5)),y)))),i(z,i(x,y)))).  [hyper(9,a,85,a,b,221,a)].
3569 t(i(i(x,i(i(y,i(i(z,i(i(i(n(u),i(i(n(w),v5),n(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8))))))),i(w,u)),v11)),i(i(n(v11),i(i(n(v12),v13),z)),i(v12,v11)))),v14)),i(i(n(v14),i(i(n(v15),v16),x)),i(v15,v14)))).  [hyper(9,a,660,a,b,10,a)].
3791 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(w,x),i(i(v5,i(i(n(v6),i(i(n(v7),v8),i(i(v9,i(i(v10,i(v9,v11)),i(i(n(v11),i(i(n(v12),v13),v10)),i(v12,v11)))),v6))),i(v7,v6))),y)))),i(z,i(x,y)))).  [hyper(9,a,329,a,b,329,a)].
3898 t(i(i(i(x,i(y,i(i(i(n(i(z,i(i(u,i(z,w)),i(i(n(w),i(i(n(v5),v6),u)),i(v5,w))))),v7),n(y)),v8))),v9),i(v10,v9))).  [hyper(9,a,2984,a,b,2110,a)].
3950 t(i(x,i(y,i(n(i(n(y),z)),u)))).  [hyper(9,a,2110,a,b,3898,a)].
4214 t(i(x,i(y,i(i(z,i(i(u,i(w,i(i(v5,i(w,v6)),i(i(n(v6),i(i(n(v7),v8),v5)),i(v7,v6))))),v9)),i(i(n(v9),i(i(n(v10),v11),z)),i(v10,v9)))))).  [hyper(9,a,875,a,b,259,a)].
4255 t(i(x,i(i(y,i(i(z,i(u,i(i(w,i(u,v5)),i(i(n(v5),i(i(n(v6),v7),w)),i(v6,v5))))),v8)),i(i(n(v8),i(i(n(v9),v10),y)),i(v9,v8))))).  [hyper(9,a,4214,a,b,4214,a)].
4303 t(i(i(x,i(i(y,i(i(n(i(z,u)),i(i(n(w),v5),i(i(i(n(v6),i(i(n(v7),v8),n(z))),i(v7,v6)),i(i(v9,i(i(v10,i(v9,v11)),i(i(n(v11),i(i(n(v12),v13),v10)),i(v12,v11)))),u)))),i(w,i(z,u)))),v14)),i(i(n(v14),i(i(n(v15),v16),x)),i(v15,v14)))).  [hyper(9,a,287,a,b,10,a)].
4394 t(i(x,i(i(i(n(i(i(n(y),i(i(n(z),u),n(i(w,i(i(v5,i(w,v6)),i(i(n(v6),i(i(n(v7),v8),v5)),i(v7,v6))))))),i(z,y))),v9),n(x)),v10))).  [hyper(9,a,4255,a,b,2253,a)].
4401 t(i(x,i(y,i(i(n(z),i(i(n(u),w),i(n(z),i(i(n(i(v5,y)),v6),n(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9))))))))),i(u,z))))).  [hyper(9,a,638,a,b,2253,a)].
4645 t(i(i(i(n(i(i(n(x),i(i(n(y),z),n(i(u,i(i(w,i(u,v5)),i(i(n(v5),i(i(n(v6),v7),w)),i(v6,v5))))))),i(y,x))),v8),n(i(v9,i(i(v10,i(v9,v11)),i(i(n(v11),i(i(n(v12),v13),v10)),i(v12,v11)))))),v14)).  [hyper(9,a,10,a,b,4394,a)].
4669 t(i(x,i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(i(w,x)),v5),n(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8))))))))),i(z,y)))).  [hyper(9,a,4401,a,b,4401,a)].
4848 t(i(i(x,i(i(y,i(i(n(z),i(i(n(u),w),i(n(z),i(i(n(i(v5,y)),v6),n(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9))))))))),i(u,z))),v12)),i(i(n(v12),i(i(n(v13),v14),x)),i(v13,v12)))).  [hyper(9,a,4669,a,b,10,a)].
4953 t(i(i(x,i(i(n(i(i(n(y),i(i(n(z),u),n(i(w,i(i(v5,i(w,v6)),i(i(n(v6),i(i(n(v7),v8),v5)),i(v7,v6))))))),i(z,y))),v9),v10)),i(i(n(v10),i(i(n(v11),v12),x)),i(v11,v10)))).  [hyper(9,a,4669,a,b,957,a)].
5017 t(i(x,i(i(n(i(i(y,i(i(z,x),u)),i(i(n(u),i(i(n(w),v5),y)),i(w,u)))),i(i(n(v6),v7),v8)),i(v6,i(i(y,i(i(z,x),u)),i(i(n(u),i(i(n(w),v5),y)),i(w,u))))))).  [hyper(9,a,4953,a,b,1034,a)].
5054 t(i(i(n(i(x,i(i(y,i(i(z,u),w)),i(i(n(w),i(i(n(v5),v6),y)),i(v5,w))))),i(i(n(v7),v8),u)),i(v7,i(x,i(i(y,i(i(z,u),w)),i(i(n(w),i(i(n(v5),v6),y)),i(v5,w))))))).  [hyper(9,a,5017,a,b,2528,a)].
5112 t(i(i(i(i(n(x),i(i(n(y),z),i(i(u,i(i(w,i(u,v5)),i(i(n(v5),i(i(n(v6),v7),w)),i(v6,v5)))),x))),i(y,x)),v8),i(v9,v8))).  [hyper(9,a,4669,a,b,3113,a)].
5214 t(i(x,i(i(y,i(i(i(n(z),i(i(n(u),w),i(i(v5,i(i(v6,i(v5,v7)),i(i(n(v7),i(i(n(v8),v9),v6)),i(v8,v7)))),z))),i(u,z)),v10)),i(i(n(v10),i(i(n(v11),v12),y)),i(v11,v10))))).  [hyper(9,a,10,a,b,5112,a)].
5431 t(i(x,i(y,i(i(z,i(i(u,i(i(n(w),i(i(n(v5),v6),n(x))),i(v5,w))),v7)),i(i(n(v7),i(i(n(v8),v9),z)),i(v8,v7)))))).  [hyper(9,a,5214,a,b,5054,a)].
5456 t(i(x,i(y,i(i(z,i(i(u,i(i(w,i(i(v5,i(i(v6,i(v5,v7)),i(i(n(v7),i(i(n(v8),v9),v6)),i(v8,v7)))),v10)),i(i(n(v10),i(i(n(v11),v12),w)),i(v11,v10)))),v13)),i(i(n(v13),i(i(n(v14),v15),z)),i(v14,v13)))))).  [hyper(9,a,63,a,b,5054,a)].
5637 t(i(x,i(i(y,i(i(z,i(i(n(u),i(i(n(w),v5),n(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8))))))),i(w,u))),v11)),i(i(n(v11),i(i(n(v12),v13),y)),i(v12,v11))))).  [hyper(9,a,10,a,b,5431,a)].
5640 t(i(i(n(i(i(x,i(i(y,i(i(n(z),i(i(n(u),w),n(v5))),i(u,z))),v6)),i(i(n(v6),i(i(n(v7),v8),x)),i(v7,v6)))),i(i(n(v9),v10),v5)),i(v9,i(i(x,i(i(y,i(i(n(z),i(i(n(u),w),n(v5))),i(u,z))),v6)),i(i(n(v6),i(i(n(v7),v8),x)),i(v7,v6)))))).  [hyper(9,a,5431,a,b,4953,a)].
5801 t(i(x,i(i(i(n(i(y,i(i(z,i(y,u)),i(i(n(u),i(i(n(w),v5),z)),i(w,u))))),v6),i(i(i(n(v7),i(i(n(v8),v9),n(v10))),i(v8,v7)),i(i(v11,i(i(v12,i(v11,v13)),i(i(n(v13),i(i(n(v14),v15),v12)),i(v14,v13)))),v16))),i(v10,v16)))).  [hyper(9,a,284,a,b,365,a)].
6247 t(i(i(n(x),i(i(n(y),z),i(i(i(u,w),i(i(n(i(i(n(w),i(i(n(v5),v6),v7)),i(v5,w))),i(i(n(v8),v9),u)),i(v8,i(i(n(w),i(i(n(v5),v6),v7)),i(v5,w))))),x))),i(y,x))).  [hyper(9,a,76,a,b,169,a)].
6285 t(i(x,i(i(n(i(y,i(i(n(z),i(i(n(u),w),v5)),i(u,z)))),i(i(n(v6),v7),i(i(i(n(v8),i(i(n(v9),v10),n(y))),i(v9,v8)),z))),i(v6,i(y,i(i(n(z),i(i(n(u),w),v5)),i(u,z))))))).  [hyper(9,a,63,a,b,6247,a)].
6369 t(i(i(n(x),i(i(n(y),z),i(i(u,i(i(w,i(i(v5,i(i(v6,i(v5,v7)),i(i(n(v7),i(i(n(v8),v9),v6)),i(v8,v7)))),v10)),i(i(n(v10),i(i(n(v11),v12),w)),i(v11,v10)))),x))),i(y,x))).  [hyper(9,a,76,a,b,184,a)].
6392 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(w,x),i(i(v5,i(i(v6,i(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9)))),v12)),i(i(n(v12),i(i(n(v13),v14),v6)),i(v13,v12)))),y)))),i(z,i(x,y)))).  [hyper(9,a,184,a,b,528,a)].
6401 t(i(x,i(i(y,i(i(z,i(i(u,i(i(w,i(i(v5,i(w,v6)),i(i(n(v6),i(i(n(v7),v8),v5)),i(v7,v6)))),v9)),i(i(n(v9),i(i(n(v10),v11),u)),i(v10,v9)))),v12)),i(i(n(v12),i(i(n(v13),v14),y)),i(v13,v12))))).  [hyper(9,a,638,a,b,6369,a)].
6563 t(i(i(x,i(i(y,i(i(z,i(i(i(u,i(i(w,i(i(v5,i(w,v6)),i(i(n(v6),i(i(n(v7),v8),v5)),i(v7,v6)))),v9)),i(i(n(v9),i(i(n(v10),v11),u)),i(v10,v9))),v12)),i(i(n(v12),i(i(n(v13),v14),z)),i(v13,v12)))),v15)),i(i(n(v15),i(i(n(v16),v17),x)),i(v16,v15)))).  [hyper(9,a,288,a,b,10,a)].
6610 t(i(x,i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(i(i(n(w),i(i(n(v5),v6),n(x))),i(v5,w))),v7),n(i(v8,i(i(v9,i(v8,v10)),i(i(n(v10),i(i(n(v11),v12),v9)),i(v11,v10))))))))),i(z,y)))).  [hyper(9,a,6369,a,b,667,a)].
6751 t(i(i(x,i(i(y,i(i(n(z),i(i(n(u),w),i(n(z),i(i(n(i(i(n(v5),i(i(n(v6),v7),n(y))),i(v6,v5))),v8),n(i(v9,i(i(v10,i(v9,v11)),i(i(n(v11),i(i(n(v12),v13),v10)),i(v12,v11))))))))),i(u,z))),v14)),i(i(n(v14),i(i(n(v15),v16),x)),i(v15,v14)))).  [hyper(9,a,6610,a,b,10,a)].
6769 t(i(x,i(y,i(n(i(z,i(i(u,i(z,w)),i(i(n(w),i(i(n(v5),v6),u)),i(v5,w))))),v7)))).  [hyper(9,a,899,a,b,3898,a)].
6801 t(i(x,i(i(n(y),i(i(n(z),u),i(i(n(i(w,i(i(v5,i(w,v6)),i(i(n(v6),i(i(n(v7),v8),v5)),i(v7,v6))))),v9),y))),i(z,y)))).  [hyper(9,a,6769,a,b,101,a)].
6915 t(i(i(x,i(i(i(n(y),i(i(n(z),u),i(i(n(i(w,i(i(v5,i(w,v6)),i(i(n(v6),i(i(n(v7),v8),v5)),i(v7,v6))))),v9),n(i(v10,i(i(v11,i(v10,v12)),i(i(n(v12),i(i(n(v13),v14),v11)),i(v13,v12)))))))),i(z,y)),v15)),i(i(n(v15),i(i(n(v16),v17),x)),i(v16,v15)))).  [hyper(9,a,1902,a,b,10,a)].
7048 t(i(i(i(x,i(i(n(y),i(i(n(z),u),i(i(w,i(i(v5,i(w,v6)),i(i(n(v6),i(i(n(v7),v8),v5)),i(v7,v6)))),y))),i(z,y))),v9),i(v10,v9))).  [hyper(9,a,6801,a,b,3791,a)].
7053 t(i(x,i(y,i(i(i(z,i(i(u,i(z,w)),i(i(n(w),i(i(n(v5),v6),u)),i(v5,w)))),v7),i(v8,v7))))).  [hyper(9,a,2375,a,b,3791,a)].
7116 t(i(x,i(i(n(y),i(i(n(z),u),i(i(i(i(w,i(i(v5,i(w,v6)),i(i(n(v6),i(i(n(v7),v8),v5)),i(v7,v6)))),v9),i(v10,v9)),y))),i(z,y)))).  [hyper(9,a,7053,a,b,101,a)].
7137 t(i(x,i(y,i(z,i(u,i(w,y)))))).  [hyper(9,a,2222,a,b,7048,a)].
7151 t(i(x,i(i(i(y,y),z),i(u,z)))).  [hyper(9,a,107,a,b,7048,a)].
7152 t(i(x,i(y,i(i(n(z),i(i(n(u),w),i(i(v5,y),z))),i(u,z))))).  [hyper(9,a,101,a,b,7048,a)].
7153 t(i(x,i(y,i(i(n(z),i(i(n(u),w),i(n(z),i(i(n(i(v5,y)),v6),n(i(v7,v7)))))),i(u,z))))).  [hyper(9,a,90,a,b,7048,a)].
7156 t(i(x,i(y,i(z,i(i(n(u),i(i(n(w),v5),i(n(u),i(i(n(i(i(n(v6),i(i(n(v7),v8),n(z))),i(v7,v6))),v9),n(i(v10,y)))))),i(w,u)))))).  [hyper(9,a,43,a,b,7048,a)].
7272 t(i(x,i(y,i(z,i(u,i(n(x),w)))))).  [hyper(9,a,7156,a,b,2606,a)].
7768 t(i(i(x,i(i(i(n(i(y,z)),i(i(n(u),w),i(i(i(n(v5),i(i(n(v6),v7),n(y))),i(v6,v5)),i(i(i(i(v8,i(i(v9,i(v8,v10)),i(i(n(v10),i(i(n(v11),v12),v9)),i(v11,v10)))),v13),i(v14,v13)),z)))),i(u,i(y,z))),v15)),i(i(n(v15),i(i(n(v16),v17),x)),i(v16,v15)))).  [hyper(9,a,310,a,b,10,a)].
7780 t(i(i(n(i(i(x,i(i(i(y,i(i(n(i(z,i(i(u,i(z,w)),i(i(n(w),i(i(n(v5),v6),u)),i(v5,w))))),v7),v8)),i(i(n(v8),i(i(n(v9),v10),y)),i(v9,v8))),v11)),i(i(n(v11),i(i(n(v12),v13),x)),i(v12,v11)))),i(i(n(v14),v15),v16)),i(v14,i(i(x,i(i(i(y,i(i(n(i(z,i(i(u,i(z,w)),i(i(n(w),i(i(n(v5),v6),u)),i(v5,w))))),v7),v8)),i(i(n(v8),i(i(n(v9),v10),y)),i(v9,v8))),v11)),i(i(n(v11),i(i(n(v12),v13),x)),i(v12,v11)))))).  [hyper(9,a,86,a,b,920,a)].
7784 t(i(i(n(i(i(n(i(x,y)),i(i(n(z),u),i(w,i(i(n(i(v5,i(i(v6,i(v5,v7)),i(i(n(v7),i(i(n(v8),v9),v6)),i(v8,v7))))),v10),y)))),i(z,i(x,y)))),i(i(n(v11),v12),i(n(y),i(i(n(x),v13),w)))),i(v11,i(i(n(i(x,y)),i(i(n(z),u),i(w,i(i(n(i(v5,i(i(v6,i(v5,v7)),i(i(n(v7),i(i(n(v8),v9),v6)),i(v8,v7))))),v10),y)))),i(z,i(x,y)))))).  [hyper(9,a,10,a,b,920,a)].
8107 t(i(x,i(i(i(n(i(i(y,i(i(z,i(i(u,i(z,w)),i(i(n(w),i(i(n(v5),v6),u)),i(v5,w)))),v7)),i(i(n(v7),i(i(n(v8),v9),y)),i(v8,v7)))),v10),n(x)),v11))).  [hyper(9,a,5637,a,b,363,a)].
8113 t(i(x,i(i(i(n(y),z),u),i(i(n(i(y,w)),i(i(n(v5),v6),i(u,i(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9)))),w)))),i(v5,i(y,w)))))).  [hyper(9,a,638,a,b,363,a)].
8124 t(i(x,i(y,i(z,i(i(n(i(u,w)),i(i(n(v5),v6),i(i(v7,u),i(i(i(v8,i(i(v9,i(i(v10,i(v9,v11)),i(i(n(v11),i(i(n(v12),v13),v10)),i(v12,v11)))),v14)),i(i(n(v14),i(i(n(v15),v16),v8)),i(v15,v14))),w)))),i(v5,i(u,w))))))).  [hyper(9,a,363,a,b,2267,a)].
8150 t(i(i(x,i(i(i(n(i(y,z)),i(i(n(u),w),i(i(v5,y),i(i(i(v6,i(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9)))),v12)),i(i(n(v12),i(i(n(v13),v14),v6)),i(v13,v12))),z)))),i(u,i(y,z))),v15)),i(i(n(v15),i(i(n(v16),v17),x)),i(v16,v15)))).  [hyper(9,a,363,a,b,10,a)].
8315 t(i(i(x,i(i(y,i(i(i(n(i(i(z,i(i(u,i(i(w,i(u,v5)),i(i(n(v5),i(i(n(v6),v7),w)),i(v6,v5)))),v8)),i(i(n(v8),i(i(n(v9),v10),z)),i(v9,v8)))),v11),n(y)),v12)),v13)),i(i(n(v13),i(i(n(v14),v15),x)),i(v14,v13)))).  [hyper(9,a,8107,a,b,10,a)].
8316 t(i(i(i(n(x),y),z),i(i(n(i(x,u)),i(i(n(w),v5),i(z,i(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8)))),u)))),i(w,i(x,u))))).  [hyper(9,a,8113,a,b,8113,a)].
8445 t(i(i(n(i(x,i(y,i(i(n(i(i(n(z),i(i(n(u),w),v5)),i(u,z))),i(i(n(v6),v7),v8)),i(v6,i(i(n(z),i(i(n(u),w),v5)),i(u,z))))))),i(i(n(v9),v10),i(i(n(y),v11),i(v5,i(v8,z))))),i(v9,i(x,i(y,i(i(n(i(i(n(z),i(i(n(u),w),v5)),i(u,z))),i(i(n(v6),v7),v8)),i(v6,i(i(n(z),i(i(n(u),w),v5)),i(u,z))))))))).  [hyper(9,a,8316,a,b,669,a)].
8451 t(i(i(n(i(x,i(y,z))),i(i(n(u),w),i(i(n(y),v5),i(n(z),i(i(n(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8))))),v11),n(x)))))),i(u,i(x,i(y,z))))).  [hyper(9,a,8316,a,b,184,a)].
8453 t(i(i(n(i(x,i(y,i(z,u)))),i(i(n(w),v5),i(i(n(y),v6),i(i(i(n(v7),i(i(n(v8),v9),n(z))),i(v8,v7)),i(i(n(x),v10),u))))),i(w,i(x,i(y,i(z,u)))))).  [hyper(9,a,8316,a,b,116,a)].
8457 t(i(i(x,i(i(i(i(n(y),z),u),i(i(n(i(y,w)),i(i(n(v5),v6),i(u,i(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9)))),w)))),i(v5,i(y,w)))),v12)),i(i(n(v12),i(i(n(v13),v14),x)),i(v13,v12)))).  [hyper(9,a,8316,a,b,10,a)].
8458 t(i(i(i(i(n(x),i(i(n(y),z),n(u))),i(y,x)),i(i(n(w),v5),v6)),i(w,i(v7,i(u,v6))))).  [hyper(9,a,7116,a,b,8453,a)].
8459 t(i(x,i(y,i(i(i(n(y),z),u),i(w,u))))).  [hyper(9,a,5637,a,b,8453,a)].
8461 t(i(x,i(y,i(z,i(u,i(n(y),w)))))).  [hyper(9,a,497,a,b,8453,a)].
8578 t(i(i(x,i(i(y,i(z,i(i(i(n(z),u),w),i(v5,w)))),v6)),i(i(n(v6),i(i(n(v7),v8),x)),i(v7,v6)))).  [hyper(9,a,8459,a,b,10,a)].
8582 t(i(i(n(i(x,i(y,z))),i(i(n(u),w),i(i(n(y),v5),i(i(n(i(n(x),v6)),v7),z)))),i(u,i(x,i(y,z))))).  [hyper(9,a,8316,a,b,8578,a)].
8845 t(i(i(n(x),i(i(n(i(y,i(i(z,i(y,u)),i(i(n(u),i(i(n(w),v5),z)),i(w,u))))),v6),n(v7))),i(v7,i(v8,x)))).  [hyper(9,a,7116,a,b,8451,a)].
8891 t(i(i(n(i(x,i(y,z))),i(i(n(u),w),i(n(i(x,i(y,z))),i(i(n(i(v5,i(i(v6,i(v5,v7)),i(i(n(v7),i(i(n(v8),v9),v6)),i(v8,v7))))),v10),i(i(n(y),v11),i(n(z),i(i(n(i(v12,i(i(v13,i(v12,v14)),i(i(n(v14),i(i(n(v15),v16),v13)),i(v15,v14))))),v17),n(x)))))))),i(u,i(x,i(y,z))))).  [hyper(9,a,8451,a,b,18,a)].
8895 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(w,i(v5,x)),i(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8)))),y)))),i(z,i(x,y)))).  [hyper(9,a,8845,a,b,8316,a)].
8973 t(i(i(x,i(i(i(n(y),i(i(n(i(z,i(i(u,i(z,w)),i(i(n(w),i(i(n(v5),v6),u)),i(v5,w))))),v7),n(v8))),i(v8,i(v9,y))),v10)),i(i(n(v10),i(i(n(v11),v12),x)),i(v11,v10)))).  [hyper(9,a,8845,a,b,10,a)].
8991 t(i(i(n(i(x,i(y,i(z,u)))),i(i(n(w),v5),u)),i(w,i(x,i(y,i(z,u)))))).  [hyper(9,a,553,a,b,8973,a)].
9056 t(i(i(n(i(i(n(i(x,y)),i(i(n(z),u),i(n(i(x,y)),i(i(n(w),v5),i(i(v6,x),i(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9)))),y)))))),i(z,i(x,y)))),i(i(n(v12),v13),w)),i(v12,i(i(n(i(x,y)),i(i(n(z),u),i(n(i(x,y)),i(i(n(w),v5),i(i(v6,x),i(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9)))),y)))))),i(z,i(x,y)))))).  [hyper(9,a,10,a,b,573,a)].
9083 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(i(n(w),i(i(n(v5),v6),n(x))),i(v5,w)),i(i(i(n(i(v7,v8)),i(i(n(v9),v10),i(i(v11,v7),i(i(v12,i(i(v13,i(v12,v14)),i(i(n(v14),i(i(n(v15),v16),v13)),i(v15,v14)))),v8)))),i(v9,i(v7,v8))),y)))),i(z,i(x,y)))).  [hyper(9,a,573,a,b,184,a)].
9086 t(i(i(x,i(i(i(y,i(i(i(n(i(z,u)),i(i(n(w),v5),i(i(v6,z),i(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9)))),u)))),i(w,i(z,u))),v12)),i(i(n(v12),i(i(n(v13),v14),y)),i(v13,v12))),v15)),i(i(n(v15),i(i(n(v16),v17),x)),i(v16,v15)))).  [hyper(9,a,573,a,b,10,a)].
9622 t(i(i(x,i(i(i(i(n(i(i(n(y),i(i(n(z),u),n(i(w,i(i(v5,i(w,v6)),i(i(n(v6),i(i(n(v7),v8),v5)),i(v7,v6))))))),i(z,y))),v9),n(i(v10,i(i(v11,i(v10,v12)),i(i(n(v12),i(i(n(v13),v14),v11)),i(v13,v12)))))),v15),v16)),i(i(n(v16),i(i(n(v17),v18),x)),i(v17,v16)))).  [hyper(9,a,4645,a,b,10,a)].
9634 t(i(x,i(n(x),y))).  [hyper(9,a,7137,a,b,84,a)].
9837 t(i(i(n(i(i(n(i(x,y)),i(i(n(z),u),i(w,i(i(i(i(v5,i(i(v6,i(v5,v7)),i(i(n(v7),i(i(n(v8),v9),v6)),i(v8,v7)))),v10),i(v11,v10)),y)))),i(z,i(x,y)))),i(i(n(v12),v13),i(n(y),i(i(n(x),v14),w)))),i(v12,i(i(n(i(x,y)),i(i(n(z),u),i(w,i(i(i(i(v5,i(i(v6,i(v5,v7)),i(i(n(v7),i(i(n(v8),v9),v6)),i(v8,v7)))),v10),i(v11,v10)),y)))),i(z,i(x,y)))))).  [hyper(9,a,10,a,b,311,a)].
9935 t(i(x,i(y,i(i(n(z),i(i(n(u),w),i(n(z),i(i(n(i(v5,y)),v6),n(i(i(n(v7),i(i(n(v8),v9),n(x))),i(v8,v7))))))),i(u,z))))).  [hyper(9,a,6401,a,b,360,a)].
9968 t(i(x,i(y,i(i(n(z),i(i(n(u),w),i(n(z),i(i(n(i(v5,y)),v6),n(i(i(v7,i(i(v8,i(i(v9,i(v8,v10)),i(i(n(v10),i(i(n(v11),v12),v9)),i(v11,v10)))),v13)),i(i(n(v13),i(i(n(v14),v15),v7)),i(v14,v13)))))))),i(u,z))))).  [hyper(9,a,63,a,b,360,a)].
10573 t(i(x,i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(i(w,x)),v5),n(i(i(n(v6),i(i(n(v7),v8),n(i(v9,i(i(v10,i(v9,v11)),i(i(n(v11),i(i(n(v12),v13),v10)),i(v12,v11))))))),i(v7,v6))))))),i(z,y)))).  [hyper(9,a,10,a,b,9935,a)].
10605 t(i(i(n(i(i(n(x),i(i(n(y),z),i(n(x),i(i(n(i(u,i(i(n(w),i(i(n(v5),v6),n(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9))))))),i(v5,w)))),v12),n(i(i(n(v13),i(i(n(v14),v15),n(v16))),i(v14,v13))))))),i(y,x))),i(i(n(v17),v18),v16)),i(v17,i(i(n(x),i(i(n(y),z),i(n(x),i(i(n(i(u,i(i(n(w),i(i(n(v5),v6),n(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9))))))),i(v5,w)))),v12),n(i(i(n(v13),i(i(n(v14),v15),n(v16))),i(v14,v13))))))),i(y,x))))).  [hyper(9,a,9935,a,b,545,a)].
12024 t(i(n(x),i(i(n(y),i(i(n(z),u),x)),i(z,y)))).  [hyper(9,a,10573,a,b,1929,a)].
12070 t(i(i(n(i(x,y)),i(i(n(z),u),n(i(w,i(v5,n(y)))))),i(z,i(x,y)))).  [hyper(9,a,12024,a,b,2421,a)].
12095 t(i(i(x,i(i(n(y),i(i(n(z),i(i(n(u),w),y)),i(u,z))),v5)),i(i(n(v5),i(i(n(v6),v7),x)),i(v6,v5)))).  [hyper(9,a,12024,a,b,10,a)].
12271 t(i(i(n(i(i(n(i(x,y)),i(i(n(z),u),n(w))),i(z,i(x,y)))),i(i(n(v5),v6),i(n(y),i(i(n(x),v7),w)))),i(v5,i(i(n(i(x,y)),i(i(n(z),u),n(w))),i(z,i(x,y)))))).  [hyper(9,a,10,a,b,12095,a)].
13838 t(i(i(i(x,i(i(y,i(i(z,i(i(u,i(z,w)),i(i(n(w),i(i(n(v5),v6),u)),i(v5,w)))),v7)),i(i(n(v7),i(i(n(v8),v9),y)),i(v8,v7)))),v10),i(v11,v10))).  [hyper(9,a,12024,a,b,6392,a)].
15382 t(i(i(n(i(i(n(i(x,y)),i(i(n(z),u),w)),i(z,i(x,y)))),i(i(n(v5),v6),i(n(y),i(i(n(x),v7),i(n(y),i(i(n(i(v8,w)),v9),n(i(v10,i(i(v11,i(v10,v12)),i(i(n(v12),i(i(n(v13),v14),v11)),i(v13,v12))))))))))),i(v5,i(i(n(i(x,y)),i(i(n(z),u),w)),i(z,i(x,y)))))).  [hyper(9,a,10,a,b,4848,a)].
17174 t(i(i(n(x),i(i(n(y),z),i(i(i(i(n(u),w),v5),i(i(n(i(u,v6)),i(i(n(v7),v8),i(v5,i(i(v9,i(i(v10,i(v9,v11)),i(i(n(v11),i(i(n(v12),v13),v10)),i(v12,v11)))),v6)))),i(v7,i(u,v6)))),x))),i(y,x))).  [hyper(9,a,76,a,b,8457,a)].
17176 t(i(i(n(i(i(n(i(x,i(y,z))),i(i(n(u),w),i(i(n(y),v5),v6))),i(u,i(x,i(y,z))))),i(i(n(v7),v8),i(n(i(y,z)),i(i(n(x),v9),i(v6,i(i(v10,i(i(v11,i(v10,v12)),i(i(n(v12),i(i(n(v13),v14),v11)),i(v13,v12)))),z)))))),i(v7,i(i(n(i(x,i(y,z))),i(i(n(u),w),i(i(n(y),v5),v6))),i(u,i(x,i(y,z))))))).  [hyper(9,a,10,a,b,8457,a)].
17209 t(i(x,i(i(n(i(y,i(z,u))),i(i(n(w),v5),i(i(n(z),v6),i(n(u),i(i(n(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9))))),v12),n(y)))))),i(w,i(y,i(z,u)))))).  [hyper(9,a,5456,a,b,17174,a)].
17293 t(i(x,i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(i(w,x)),v5),n(i(i(v6,i(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9)))),v12)),i(i(n(v12),i(i(n(v13),v14),v6)),i(v13,v12)))))))),i(z,y)))).  [hyper(9,a,17209,a,b,9968,a)].
17379 t(i(i(x,i(i(y,i(i(n(z),i(i(n(u),w),i(n(z),i(i(n(i(v5,y)),v6),n(i(i(v7,i(i(v8,i(i(v9,i(v8,v10)),i(i(n(v10),i(i(n(v11),v12),v9)),i(v11,v10)))),v13)),i(i(n(v13),i(i(n(v14),v15),v7)),i(v14,v13)))))))),i(u,z))),v16)),i(i(n(v16),i(i(n(v17),v18),x)),i(v17,v16)))).  [hyper(9,a,17293,a,b,10,a)].
17870 t(i(i(n(x),i(i(n(y),z),i(i(i(u,i(i(w,i(i(i(n(i(v5,i(i(v6,i(v5,v7)),i(i(n(v7),i(i(n(v8),v9),v6)),i(v8,v7))))),v10),n(w)),v11)),v12)),i(i(n(v12),i(i(n(v13),v14),u)),i(v13,v12))),x))),i(y,x))).  [hyper(9,a,76,a,b,1950,a)].
18029 t(i(x,i(i(n(i(y,z)),i(i(n(u),w),i(i(v5,y),i(i(i(v6,i(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9)))),v12)),i(i(n(v12),i(i(n(v13),v14),v6)),i(v13,v12))),z)))),i(u,i(y,z))))).  [hyper(9,a,8124,a,b,17870,a)].
18143 t(i(i(n(x),i(i(n(y),z),i(i(u,i(i(i(n(i(i(w,i(i(v5,i(i(v6,i(v5,v7)),i(i(n(v7),i(i(n(v8),v9),v6)),i(v8,v7)))),v10)),i(i(n(v10),i(i(n(v11),v12),w)),i(v11,v10)))),v13),n(u)),v14)),x))),i(y,x))).  [hyper(9,a,76,a,b,8315,a)].
18180 t(i(x,i(i(y,i(i(z,i(i(i(n(i(i(u,i(i(w,i(i(v5,i(w,v6)),i(i(n(v6),i(i(n(v7),v8),v5)),i(v7,v6)))),v9)),i(i(n(v9),i(i(n(v10),v11),u)),i(v10,v9)))),v12),n(z)),v13)),v14)),i(i(n(v14),i(i(n(v15),v16),y)),i(v15,v14))))).  [hyper(9,a,638,a,b,18143,a)].
20229 t(i(i(n(x),i(i(n(y),z),i(i(u,i(w,i(i(n(v5),i(i(n(v6),v7),i(n(v5),i(i(n(i(i(n(v8),i(i(n(v9),v10),n(w))),i(v9,v8))),v11),n(i(i(n(v12),i(i(n(v13),v14),n(u))),i(v13,v12))))))),i(v6,v5)))),x))),i(y,x))).  [hyper(9,a,76,a,b,54,a)].
20265 t(i(x,i(i(y,i(i(z,i(u,i(i(n(w),i(i(n(v5),v6),i(n(w),i(i(n(i(i(n(v7),i(i(n(v8),v9),n(u))),i(v8,v7))),v10),n(i(i(n(v11),i(i(n(v12),v13),n(z))),i(v12,v11))))))),i(v5,w)))),v14)),i(i(n(v14),i(i(n(v15),v16),y)),i(v15,v14))))).  [hyper(9,a,638,a,b,20229,a)].
20998 t(i(x,i(i(n(i(y,i(i(n(z),i(i(n(u),w),i(n(z),i(i(n(i(v5,y)),v6),n(v7))))),i(u,z)))),i(i(n(v8),v9),v7)),i(v8,i(y,i(i(n(z),i(i(n(u),w),i(n(z),i(i(n(i(v5,y)),v6),n(v7))))),i(u,z))))))).  [hyper(9,a,5431,a,b,89,a)].
21139 t(i(x,i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(i(i(n(w),i(i(n(v5),v6),n(x))),i(v5,w))),v7),n(i(v8,i(v9,i(v10,i(v11,v8))))))))),i(z,y)))).  [hyper(9,a,18180,a,b,2420,a)].
22708 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(w,x),i(i(v5,i(i(v6,i(i(i(n(v7),i(i(n(v8),v9),n(i(v10,i(i(v11,i(v10,v12)),i(i(n(v12),i(i(n(v13),v14),v11)),i(v13,v12))))))),i(v8,v7)),v15)),i(i(n(v15),i(i(n(v16),v17),v6)),i(v16,v15)))),y)))),i(z,i(x,y)))).  [hyper(9,a,3569,a,b,12095,a)].
23071 t(i(i(n(i(i(n(x),i(i(n(y),z),i(i(u,i(w,i(i(n(v5),i(i(n(v6),v7),i(n(v5),i(i(n(i(i(n(v8),i(i(n(v9),v10),n(w))),i(v9,v8))),v11),n(i(i(n(v12),i(i(n(v13),v14),n(u))),i(v13,v12))))))),i(v6,v5)))),x))),i(y,x))),i(i(n(v15),v16),v17)),i(v15,i(i(n(x),i(i(n(y),z),i(i(u,i(w,i(i(n(v5),i(i(n(v6),v7),i(n(v5),i(i(n(i(i(n(v8),i(i(n(v9),v10),n(w))),i(v9,v8))),v11),n(i(i(n(v12),i(i(n(v13),v14),n(u))),i(v13,v12))))))),i(v6,v5)))),x))),i(y,x))))).  [hyper(9,a,20265,a,b,94,a)].
23140 t(i(i(i(n(i(x,i(i(y,i(x,z)),i(i(n(z),i(i(n(u),w),y)),i(u,z))))),v5),i(i(v6,v7),i(i(v8,i(i(v9,i(v8,v10)),i(i(n(v10),i(i(n(v11),v12),v9)),i(v11,v10)))),v13))),i(v7,v13))).  [hyper(9,a,21139,a,b,572,a)].
23157 t(i(i(i(n(i(x,i(i(y,i(x,z)),i(i(n(z),i(i(n(u),w),y)),i(u,z))))),v5),v6),i(v7,i(i(n(v8),i(i(n(v9),v10),i(n(v8),i(i(n(i(v11,v7)),v12),n(v6))))),i(v9,v8))))).  [hyper(9,a,20998,a,b,23140,a)].
23159 t(i(i(i(n(i(x,i(i(y,i(x,z)),i(i(n(z),i(i(n(u),w),y)),i(u,z))))),v5),i(i(v6,v7),i(i(i(v8,i(i(v9,i(i(v10,i(v9,v11)),i(i(n(v11),i(i(n(v12),v13),v10)),i(v12,v11)))),v14)),i(i(n(v14),i(i(n(v15),v16),v8)),i(v15,v14))),v17))),i(v7,v17))).  [hyper(9,a,18029,a,b,23140,a)].
23175 t(i(i(i(n(i(x,i(i(y,i(x,z)),i(i(n(z),i(i(n(u),w),y)),i(u,z))))),v5),i(i(i(n(v6),i(i(n(v7),v8),n(v9))),i(v7,v6)),v10)),i(v9,i(i(n(v10),i(i(n(v11),v12),v13)),i(v11,v10))))).  [hyper(9,a,6285,a,b,23140,a)].
23177 t(i(i(i(i(n(x),i(i(n(y),z),n(i(u,i(i(w,i(u,v5)),i(i(n(v5),i(i(n(v6),v7),w)),i(v6,v5))))))),i(y,x)),i(i(v8,i(i(v9,i(v8,v10)),i(i(n(v10),i(i(n(v11),v12),v9)),i(v11,v10)))),v13)),v13)).  [hyper(9,a,5801,a,b,23140,a)].
23400 t(i(x,i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(i(w,x)),v5),n(i(v6,i(i(i(n(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9))))),v12),n(v6)),v13))))))),i(z,y)))).  [hyper(9,a,563,a,b,23157,a)].
23403 t(i(x,i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(i(w,x)),v5),n(i(i(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8)))),v11),i(v12,v11))))))),i(z,y)))).  [hyper(9,a,401,a,b,23157,a)].
23652 t(i(i(x,i(i(y,i(i(n(z),i(i(n(u),w),i(n(z),i(i(n(i(v5,y)),v6),n(i(i(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9)))),v12),i(v13,v12))))))),i(u,z))),v14)),i(i(n(v14),i(i(n(v15),v16),x)),i(v15,v14)))).  [hyper(9,a,23403,a,b,10,a)].
23807 t(i(i(x,i(i(y,i(i(n(z),i(i(n(u),w),i(n(z),i(i(n(i(v5,y)),v6),n(i(v7,i(i(i(n(i(v8,i(i(v9,i(v8,v10)),i(i(n(v10),i(i(n(v11),v12),v9)),i(v11,v10))))),v13),n(v7)),v14))))))),i(u,z))),v15)),i(i(n(v15),i(i(n(v16),v17),x)),i(v16,v15)))).  [hyper(9,a,23400,a,b,10,a)].
23819 t(i(x,i(i(n(i(i(y,i(i(i(n(z),i(i(n(u),w),n(x))),i(u,z)),v5)),i(i(n(v5),i(i(n(v6),v7),y)),i(v6,v5)))),i(i(n(v8),v9),v10)),i(v8,i(i(y,i(i(i(n(z),i(i(n(u),w),n(x))),i(u,z)),v5)),i(i(n(v5),i(i(n(v6),v7),y)),i(v6,v5))))))).  [hyper(9,a,86,a,b,23175,a)].
26164 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(w,x),i(i(v5,i(i(n(i(v6,v7)),i(i(n(v8),v9),i(i(i(n(v10),i(i(n(v11),v12),n(v6))),i(v11,v10)),i(i(v13,i(i(v14,i(v13,v15)),i(i(n(v15),i(i(n(v16),v17),v14)),i(v16,v15)))),v7)))),i(v8,i(v6,v7)))),y)))),i(z,i(x,y)))).  [hyper(9,a,4303,a,b,23652,a)].
26758 t(i(i(i(n(i(i(x,i(i(y,i(i(z,i(y,u)),i(i(n(u),i(i(n(w),v5),z)),i(w,u)))),v6)),i(i(n(v6),i(i(n(v7),v8),x)),i(v7,v6)))),v9),i(i(v10,v11),i(i(v12,i(i(v13,i(v12,v14)),i(i(n(v14),i(i(n(v15),v16),v13)),i(v15,v14)))),v17))),i(v11,v17))).  [hyper(9,a,370,a,b,23159,a)].
27279 t(i(i(n(i(i(n(i(x,y)),i(i(n(z),u),w)),i(z,i(x,y)))),i(i(n(v5),v6),i(n(y),i(i(n(x),v7),i(n(y),i(i(n(i(i(n(v8),i(i(n(v9),v10),n(w))),i(v9,v8))),v11),n(i(v12,i(i(v13,i(v12,v14)),i(i(n(v14),i(i(n(v15),v16),v13)),i(v15,v14))))))))))),i(v5,i(i(n(i(x,y)),i(i(n(z),u),w)),i(z,i(x,y)))))).  [hyper(9,a,10,a,b,6751,a)].
27795 t(i(x,i(y,i(i(n(i(z,u)),i(i(n(w),v5),i(n(i(z,u)),i(i(n(i(v6,y)),v7),i(i(i(n(v8),i(i(n(v9),v10),n(z))),i(v9,v8)),i(i(v11,i(i(v12,i(v11,v13)),i(i(n(v13),i(i(n(v14),v15),v12)),i(v14,v13)))),u)))))),i(w,i(z,u)))))).  [hyper(9,a,638,a,b,362,a)].
27797 t(i(x,i(y,i(i(i(n(i(i(n(i(z,u)),i(i(n(w),v5),i(i(i(n(v6),i(i(n(v7),v8),n(z))),i(v7,v6)),i(i(v9,i(i(v10,i(v9,v11)),i(i(n(v11),i(i(n(v12),v13),v10)),i(v12,v11)))),u)))),i(w,i(z,u)))),v14),n(y)),v15)))).  [hyper(9,a,362,a,b,13838,a)].
27904 t(i(x,i(i(n(i(y,z)),i(i(n(u),w),i(n(i(y,z)),i(i(n(i(v5,x)),v6),i(i(i(n(v7),i(i(n(v8),v9),n(y))),i(v8,v7)),i(i(v10,i(i(v11,i(v10,v12)),i(i(n(v12),i(i(n(v13),v14),v11)),i(v13,v12)))),z)))))),i(u,i(y,z))))).  [hyper(9,a,27797,a,b,27795,a)].
27973 t(i(i(i(n(i(i(n(x),i(i(n(y),z),n(i(u,i(i(w,i(u,v5)),i(i(n(v5),i(i(n(v6),v7),w)),i(v6,v5))))))),i(y,x))),v8),i(i(v9,i(i(v10,i(v9,v11)),i(i(n(v11),i(i(n(v12),v13),v10)),i(v12,v11)))),v14)),v14)).  [hyper(9,a,27904,a,b,2233,a)].
28027 t(i(x,i(y,i(i(n(i(z,u)),i(i(n(w),v5),i(n(i(z,u)),i(i(n(i(i(n(v6),i(i(n(v7),v8),n(y))),i(v7,v6))),v9),i(i(v10,z),i(i(v11,i(i(v12,i(v11,v13)),i(i(n(v13),i(i(n(v14),v15),v12)),i(v14,v13)))),u)))))),i(w,i(z,u)))))).  [hyper(9,a,638,a,b,9083,a)].
28039 t(i(x,i(i(n(i(y,z)),i(i(n(u),w),i(n(i(y,z)),i(i(n(i(i(n(v5),i(i(n(v6),v7),n(x))),i(v6,v5))),v8),i(i(v9,y),i(i(v10,i(i(v11,i(v10,v12)),i(i(n(v12),i(i(n(v13),v14),v11)),i(v13,v12)))),z)))))),i(u,i(y,z))))).  [hyper(9,a,28027,a,b,28027,a)].
28109 t(i(i(n(i(i(i(n(i(i(n(x),i(i(n(y),z),n(u))),i(y,x))),w),i(i(v5,v6),i(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9)))),v12))),i(v6,v12))),i(i(n(v13),v14),u)),i(v13,i(i(i(n(i(i(n(x),i(i(n(y),z),n(u))),i(y,x))),w),i(i(v5,v6),i(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9)))),v12))),i(v6,v12))))).  [hyper(9,a,28039,a,b,23807,a)].
28124 t(i(i(x,i(i(y,i(i(n(i(z,u)),i(i(n(w),v5),i(n(i(z,u)),i(i(n(i(i(n(v6),i(i(n(v7),v8),n(y))),i(v7,v6))),v9),i(i(v10,z),i(i(v11,i(i(v12,i(v11,v13)),i(i(n(v13),i(i(n(v14),v15),v12)),i(v14,v13)))),u)))))),i(w,i(z,u)))),v16)),i(i(n(v16),i(i(n(v17),v18),x)),i(v17,v16)))).  [hyper(9,a,28039,a,b,10,a)].
28148 t(i(i(i(x,i(i(y,i(i(i(n(z),i(i(n(u),w),n(i(v5,i(i(v6,i(v5,v7)),i(i(n(v7),i(i(n(v8),v9),v6)),i(v8,v7))))))),i(u,z)),v10)),i(i(n(v10),i(i(n(v11),v12),y)),i(v11,v10)))),v13),i(v14,v13))).  [hyper(9,a,28039,a,b,22708,a)].
28778 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(w,x),i(i(v5,i(i(v6,i(i(i(v7,i(i(v8,i(i(v9,i(v8,v10)),i(i(n(v10),i(i(n(v11),v12),v9)),i(v11,v10)))),v13)),i(i(n(v13),i(i(n(v14),v15),v7)),i(v14,v13))),v16)),i(i(n(v16),i(i(n(v17),v18),v6)),i(v17,v16)))),y)))),i(z,i(x,y)))).  [hyper(9,a,6563,a,b,23807,a)].
28793 t(i(i(n(i(i(n(x),i(i(n(y),z),i(n(x),i(i(n(u),w),i(i(n(i(v5,i(i(v6,i(v5,v7)),i(i(n(v7),i(i(n(v8),v9),v6)),i(v8,v7))))),v10),n(i(v11,i(i(v12,i(v11,v13)),i(i(n(v13),i(i(n(v14),v15),v12)),i(v14,v13)))))))))),i(y,x))),i(i(n(v16),v17),u)),i(v16,i(i(n(x),i(i(n(y),z),i(n(x),i(i(n(u),w),i(i(n(i(v5,i(i(v6,i(v5,v7)),i(i(n(v7),i(i(n(v8),v9),v6)),i(v8,v7))))),v10),n(i(v11,i(i(v12,i(v11,v13)),i(i(n(v13),i(i(n(v14),v15),v12)),i(v14,v13)))))))))),i(y,x))))).  [hyper(9,a,10,a,b,6915,a)].
28906 t(i(x,i(i(y,i(i(i(n(z),i(i(n(u),w),n(i(i(n(v5),i(i(n(v6),v7),n(i(v8,i(i(v9,i(v8,v10)),i(i(n(v10),i(i(n(v11),v12),v9)),i(v11,v10))))))),i(v6,v5))))),i(u,z)),v13)),i(i(n(v13),i(i(n(v14),v15),y)),i(v14,v13))))).  [hyper(9,a,23819,a,b,23177,a)].
29198 t(i(i(n(i(i(n(i(x,y)),i(i(n(z),u),i(n(i(x,y)),i(i(n(w),v5),i(i(i(n(v6),i(i(n(v7),v8),n(x))),i(v7,v6)),i(i(i(i(v9,i(i(v10,i(v9,v11)),i(i(n(v11),i(i(n(v12),v13),v10)),i(v12,v11)))),v14),i(v15,v14)),y)))))),i(z,i(x,y)))),i(i(n(v16),v17),w)),i(v16,i(i(n(i(x,y)),i(i(n(z),u),i(n(i(x,y)),i(i(n(w),v5),i(i(i(n(v6),i(i(n(v7),v8),n(x))),i(v7,v6)),i(i(i(i(v9,i(i(v10,i(v9,v11)),i(i(n(v11),i(i(n(v12),v13),v10)),i(v12,v11)))),v14),i(v15,v14)),y)))))),i(z,i(x,y)))))).  [hyper(9,a,10,a,b,7768,a)].
29364 t(i(i(i(x,i(i(n(i(y,z)),i(i(n(u),w),i(i(i(n(v5),i(i(n(v6),v7),n(y))),i(v6,v5)),i(i(v8,i(i(v9,i(v8,v10)),i(i(n(v10),i(i(n(v11),v12),v9)),i(v11,v10)))),z)))),i(u,i(y,z)))),v13),i(v14,v13))).  [hyper(9,a,28039,a,b,26164,a)].
29507 t(i(x,i(i(i(n(y),z),u),i(i(n(i(y,i(i(n(w),i(i(n(v5),v6),i(n(w),i(i(n(u),v7),n(v8))))),i(v5,w)))),i(i(n(v9),v10),v8)),i(v9,i(y,i(i(n(w),i(i(n(v5),v6),i(n(w),i(i(n(u),v7),n(v8))))),i(v5,w)))))))).  [hyper(9,a,638,a,b,359,a)].
29509 t(i(x,i(i(i(y,i(i(n(i(i(n(z),i(i(n(u),w),i(n(z),i(i(n(v5),v6),n(y))))),i(u,z))),i(i(n(v7),v8),v5)),i(v7,i(i(n(z),i(i(n(u),w),i(n(z),i(i(n(v5),v6),n(y))))),i(u,z))))),v9),i(v10,v9)))).  [hyper(9,a,359,a,b,29364,a)].
29625 t(i(i(i(n(x),y),z),i(i(n(i(x,i(i(n(u),i(i(n(w),v5),i(n(u),i(i(n(z),v6),n(v7))))),i(w,u)))),i(i(n(v8),v9),v7)),i(v8,i(x,i(i(n(u),i(i(n(w),v5),i(n(u),i(i(n(z),v6),n(v7))))),i(w,u))))))).  [hyper(9,a,29509,a,b,29507,a)].
30314 t(i(i(n(i(x,i(y,i(i(n(z),i(i(n(u),w),i(n(z),i(i(n(v5),v6),n(i(v7,x)))))),i(u,z))))),i(i(n(v8),v9),i(i(n(y),v10),v5))),i(v8,i(x,i(y,i(i(n(z),i(i(n(u),w),i(n(z),i(i(n(v5),v6),n(i(v7,x)))))),i(u,z))))))).  [hyper(9,a,29625,a,b,23807,a)].
30415 t(i(x,i(y,i(z,i(i(n(u),i(i(n(w),v5),i(n(u),i(i(n(i(i(v6,i(i(n(z),v7),v8)),i(i(n(v8),i(i(n(v9),v10),v6)),i(v9,v8)))),v11),n(i(v12,y)))))),i(w,u)))))).  [hyper(9,a,638,a,b,30314,a)].
30434 t(i(x,i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(i(i(w,i(i(n(x),v5),v6)),i(i(n(v6),i(i(n(v7),v8),w)),i(v7,v6)))),v9),n(i(v10,i(v11,i(i(v12,i(v11,v13)),i(i(n(v13),i(i(n(v14),v15),v12)),i(v14,v13)))))))))),i(z,y)))).  [hyper(9,a,30415,a,b,27973,a)].
30947 t(i(x,i(i(i(n(y),z),u),i(i(n(i(y,w)),i(i(n(v5),v6),i(u,i(i(i(v7,i(i(v8,i(i(v9,i(v8,v10)),i(i(n(v10),i(i(n(v11),v12),v9)),i(v11,v10)))),v13)),i(i(n(v13),i(i(n(v14),v15),v7)),i(v14,v13))),w)))),i(v5,i(y,w)))))).  [hyper(9,a,638,a,b,361,a)].
30949 t(i(x,i(i(i(i(y,i(i(i(z,i(i(u,i(i(w,i(u,v5)),i(i(n(v5),i(i(n(v6),v7),w)),i(v6,v5)))),v8)),i(i(n(v8),i(i(n(v9),v10),z)),i(v9,v8))),v11)),i(i(n(v11),i(i(n(v12),v13),y)),i(v12,v11))),v14),i(v15,v14)))).  [hyper(9,a,361,a,b,29364,a)].
31076 t(i(i(i(n(x),y),z),i(i(n(i(x,u)),i(i(n(w),v5),i(z,i(i(i(v6,i(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9)))),v12)),i(i(n(v12),i(i(n(v13),v14),v6)),i(v13,v12))),u)))),i(w,i(x,u))))).  [hyper(9,a,30949,a,b,30947,a)].
31077 t(i(i(n(x),i(i(n(i(i(y,i(i(z,i(i(u,i(z,w)),i(i(n(w),i(i(n(v5),v6),u)),i(v5,w)))),v7)),i(i(n(v7),i(i(n(v8),v9),y)),i(v8,v7)))),v10),n(v11))),i(v11,i(v12,x)))).  [hyper(9,a,30947,a,b,26758,a)].
31154 t(i(i(x,i(i(i(n(y),i(i(n(i(i(z,i(i(u,i(i(w,i(u,v5)),i(i(n(v5),i(i(n(v6),v7),w)),i(v6,v5)))),v8)),i(i(n(v8),i(i(n(v9),v10),z)),i(v9,v8)))),v11),n(v12))),i(v12,i(v13,y))),v14)),i(i(n(v14),i(i(n(v15),v16),x)),i(v15,v14)))).  [hyper(9,a,31077,a,b,10,a)].
31206 t(i(i(x,i(i(i(i(n(y),z),u),i(i(n(i(y,w)),i(i(n(v5),v6),i(u,i(i(i(v7,i(i(v8,i(i(v9,i(v8,v10)),i(i(n(v10),i(i(n(v11),v12),v9)),i(v11,v10)))),v13)),i(i(n(v13),i(i(n(v14),v15),v7)),i(v14,v13))),w)))),i(v5,i(y,w)))),v16)),i(i(n(v16),i(i(n(v17),v18),x)),i(v17,v16)))).  [hyper(9,a,31076,a,b,10,a)].
31265 t(i(x,i(y,i(i(z,i(i(i(n(u),i(i(n(w),v5),n(i(v6,x)))),i(w,u)),v7)),i(i(n(v7),i(i(n(v8),v9),z)),i(v8,v7)))))).  [hyper(9,a,30434,a,b,991,a)].
31267 t(i(x,i(y,i(i(z,i(i(i(n(u),i(i(n(w),v5),n(i(i(n(v6),i(i(n(v7),v8),n(x))),i(v7,v6))))),i(w,u)),v9)),i(i(n(v9),i(i(n(v10),v11),z)),i(v10,v9)))))).  [hyper(9,a,28906,a,b,991,a)].
31309 t(i(x,i(y,i(i(z,i(i(i(n(u),i(i(n(w),v5),n(i(i(n(i(v6,v7)),i(i(n(v8),v9),i(i(v10,v6),i(i(v11,i(i(v12,i(v11,v13)),i(i(n(v13),i(i(n(v14),v15),v12)),i(v14,v13)))),v7)))),i(v8,i(v6,v7)))))),i(w,u)),v16)),i(i(n(v16),i(i(n(v17),v18),z)),i(v17,v16)))))).  [hyper(9,a,2955,a,b,991,a)].
31338 t(i(x,i(y,i(z,i(i(u,i(i(i(n(w),i(i(n(v5),v6),n(i(i(n(v7),i(i(n(v8),v9),n(y))),i(v8,v7))))),i(v5,w)),v10)),i(i(n(v10),i(i(n(v11),v12),u)),i(v11,v10))))))).  [hyper(9,a,991,a,b,28148,a)].
31753 t(i(x,i(i(y,i(i(i(n(z),i(i(n(u),w),n(i(v5,i(i(v6,i(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9)))),v12)),i(i(n(v12),i(i(n(v13),v14),v6)),i(v13,v12))))))),i(u,z)),v15)),i(i(n(v15),i(i(n(v16),v17),y)),i(v16,v15))))).  [hyper(9,a,18,a,b,31265,a)].
31754 t(i(x,i(i(y,i(i(i(n(z),i(i(n(u),w),n(i(v5,i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8)))))))),i(u,z)),v11)),i(i(n(v11),i(i(n(v12),v13),y)),i(v12,v11))))).  [hyper(9,a,10,a,b,31265,a)].
31755 t(i(i(n(i(i(x,i(i(i(n(y),i(i(n(z),u),n(i(w,v5)))),i(z,y)),v6)),i(i(n(v6),i(i(n(v7),v8),x)),i(v7,v6)))),i(i(n(v9),v10),v5)),i(v9,i(i(x,i(i(i(n(y),i(i(n(z),u),n(i(w,v5)))),i(z,y)),v6)),i(i(n(v6),i(i(n(v7),v8),x)),i(v7,v6)))))).  [hyper(9,a,31265,a,b,31154,a)].
32108 t(i(i(x,i(i(y,i(z,i(i(u,i(i(i(n(w),i(i(n(v5),v6),n(i(i(n(v7),i(i(n(v8),v9),n(y))),i(v8,v7))))),i(v5,w)),v10)),i(i(n(v10),i(i(n(v11),v12),u)),i(v11,v10))))),v13)),i(i(n(v13),i(i(n(v14),v15),x)),i(v14,v13)))).  [hyper(9,a,31267,a,b,10,a)].
32438 t(i(i(x,i(i(y,i(i(z,i(i(i(n(u),i(i(n(w),v5),n(i(v6,i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9)))))))),i(w,u)),v12)),i(i(n(v12),i(i(n(v13),v14),z)),i(v13,v12)))),v15)),i(i(n(v15),i(i(n(v16),v17),x)),i(v16,v15)))).  [hyper(9,a,31754,a,b,10,a)].
32947 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(w,x),i(i(v5,i(v6,i(i(v7,i(i(i(n(v8),i(i(n(v9),v10),n(i(i(n(v11),i(i(n(v12),v13),n(v5))),i(v12,v11))))),i(v9,v8)),v14)),i(i(n(v14),i(i(n(v15),v16),v7)),i(v15,v14))))),y)))),i(z,i(x,y)))).  [hyper(9,a,32108,a,b,23807,a)].
33059 t(i(i(x,i(i(i(n(y),i(i(n(z),u),n(i(w,i(i(v5,i(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8)))),v11)),i(i(n(v11),i(i(n(v12),v13),v5)),i(v12,v11))))))),i(z,y)),v14)),i(i(n(v14),i(i(n(v15),v16),x)),i(v15,v14)))).  [hyper(9,a,32947,a,b,31753,a)].
33135 t(i(x,i(i(y,i(i(i(n(z),i(i(n(u),w),n(i(i(n(i(v5,v6)),i(i(n(v7),v8),i(i(v9,v5),i(i(v10,i(i(v11,i(v10,v12)),i(i(n(v12),i(i(n(v13),v14),v11)),i(v13,v12)))),v6)))),i(v7,i(v5,v6)))))),i(u,z)),v15)),i(i(n(v15),i(i(n(v16),v17),y)),i(v16,v15))))).  [hyper(9,a,33059,a,b,31309,a)].
33184 t(i(x,i(i(y,i(i(z,i(i(n(u),i(i(n(w),v5),n(i(i(n(v6),i(i(n(v7),v8),n(x))),i(v7,v6))))),i(w,u))),v9)),i(i(n(v9),i(i(n(v10),v11),y)),i(v10,v9))))).  [hyper(9,a,33135,a,b,5640,a)].
33488 t(i(i(n(i(i(n(i(x,y)),i(i(n(z),u),i(n(i(x,y)),i(i(n(w),v5),i(i(v6,x),i(i(i(v7,i(i(v8,i(i(v9,i(v8,v10)),i(i(n(v10),i(i(n(v11),v12),v9)),i(v11,v10)))),v13)),i(i(n(v13),i(i(n(v14),v15),v7)),i(v14,v13))),y)))))),i(z,i(x,y)))),i(i(n(v16),v17),w)),i(v16,i(i(n(i(x,y)),i(i(n(z),u),i(n(i(x,y)),i(i(n(w),v5),i(i(v6,x),i(i(i(v7,i(i(v8,i(i(v9,i(v8,v10)),i(i(n(v10),i(i(n(v11),v12),v9)),i(v11,v10)))),v13)),i(i(n(v13),i(i(n(v14),v15),v7)),i(v14,v13))),y)))))),i(z,i(x,y)))))).  [hyper(9,a,10,a,b,8150,a)].
33515 t(i(i(x,i(i(i(y,i(i(i(z,i(i(i(n(i(u,w)),i(i(n(v5),v6),i(i(v7,u),i(i(v8,i(i(v9,i(v8,v10)),i(i(n(v10),i(i(n(v11),v12),v9)),i(v11,v10)))),w)))),i(v5,i(u,w))),v13)),i(i(n(v13),i(i(n(v14),v15),z)),i(v14,v13))),v16)),i(i(n(v16),i(i(n(v17),v18),y)),i(v17,v16))),v19)),i(i(n(v19),i(i(n(v20),v21),x)),i(v20,v19)))).  [hyper(9,a,9086,a,b,10,a)].
33688 t(i(x,i(i(y,i(i(i(n(z),i(i(n(u),w),n(i(v5,i(i(n(v6),i(i(n(v7),v8),n(x))),i(v7,v6)))))),i(u,z)),v9)),i(i(n(v9),i(i(n(v10),v11),y)),i(v10,v9))))).  [hyper(9,a,33184,a,b,31755,a)].
34024 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(w,x),i(i(i(i(n(i(i(n(v5),i(i(n(v6),v7),n(i(v8,i(i(v9,i(v8,v10)),i(i(n(v10),i(i(n(v11),v12),v9)),i(v11,v10))))))),i(v6,v5))),v13),n(i(v14,i(i(v15,i(v14,v16)),i(i(n(v16),i(i(n(v17),v18),v15)),i(v17,v16)))))),v19),y)))),i(z,i(x,y)))).  [hyper(9,a,9622,a,b,23807,a)].
34813 t(i(i(i(x,i(i(y,i(i(i(z,i(i(u,i(i(w,i(u,v5)),i(i(n(v5),i(i(n(v6),v7),w)),i(v6,v5)))),v8)),i(i(n(v8),i(i(n(v9),v10),z)),i(v9,v8))),v11)),i(i(n(v11),i(i(n(v12),v13),y)),i(v12,v11)))),v14),i(v15,v14))).  [hyper(9,a,30434,a,b,28778,a)].
35434 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(w,x),i(i(v5,i(i(n(v6),i(i(n(v7),v8),i(n(v6),i(i(n(i(v9,v5)),v10),n(i(i(v11,i(i(v12,i(i(v13,i(v12,v14)),i(i(n(v14),i(i(n(v15),v16),v13)),i(v15,v14)))),v17)),i(i(n(v17),i(i(n(v18),v19),v11)),i(v18,v17)))))))),i(v7,v6))),y)))),i(z,i(x,y)))).  [hyper(9,a,17379,a,b,17379,a)].
35980 t(i(i(i(n(x),y),i(n(z),i(i(n(i(u,w)),v5),n(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8)))))))),i(i(n(i(x,z)),i(i(n(v11),v12),w)),i(v11,i(x,z))))).  [hyper(9,a,30434,a,b,15382,a)].
36035 t(i(i(x,i(i(i(i(n(y),z),i(n(u),i(i(n(i(w,v5)),v6),n(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9)))))))),i(i(n(i(y,u)),i(i(n(v12),v13),v5)),i(v12,i(y,u)))),v14)),i(i(n(v14),i(i(n(v15),v16),x)),i(v15,v14)))).  [hyper(9,a,35980,a,b,10,a)].
36104 t(i(i(n(i(i(n(i(x,i(y,z))),i(i(n(u),w),i(i(n(y),v5),v6))),i(u,i(x,i(y,z))))),i(i(n(v7),v8),i(n(i(y,z)),i(i(n(x),v9),i(v6,i(i(i(v10,i(i(v11,i(i(v12,i(v11,v13)),i(i(n(v13),i(i(n(v14),v15),v12)),i(v14,v13)))),v16)),i(i(n(v16),i(i(n(v17),v18),v10)),i(v17,v16))),z)))))),i(v7,i(i(n(i(x,i(y,z))),i(i(n(u),w),i(i(n(y),v5),v6))),i(u,i(x,i(y,z))))))).  [hyper(9,a,10,a,b,31206,a)].
36219 t(i(i(i(i(i(n(i(i(n(x),i(i(n(y),z),n(i(u,i(i(w,i(u,v5)),i(i(n(v5),i(i(n(v6),v7),w)),i(v6,v5))))))),i(y,x))),v8),n(i(v9,i(i(v10,i(v9,v11)),i(i(n(v11),i(i(n(v12),v13),v10)),i(v12,v11)))))),v14),v15),i(v16,v15))).  [hyper(9,a,30434,a,b,34024,a)].
36235 t(i(x,i(i(n(y),i(i(n(z),u),i(i(n(i(i(n(w),i(i(n(v5),v6),n(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9))))))),i(v5,w))),v12),n(i(v13,i(i(v14,i(v13,v15)),i(i(n(v15),i(i(n(v16),v17),v14)),i(v16,v15)))))))),i(z,y)))).  [hyper(9,a,36035,a,b,36219,a)].
37096 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(i(n(w),i(i(n(v5),v6),n(x))),i(v5,w)),i(i(v7,i(i(n(i(v8,v9)),i(i(n(v10),v11),i(n(i(v8,v9)),i(i(n(i(i(n(v12),i(i(n(v13),v14),n(v7))),i(v13,v12))),v15),i(i(v16,v8),i(i(v17,i(i(v18,i(v17,v19)),i(i(n(v19),i(i(n(v20),v21),v18)),i(v20,v19)))),v9)))))),i(v10,i(v8,v9)))),y)))),i(z,i(x,y)))).  [hyper(9,a,28124,a,b,32438,a)].
37380 t(i(i(i(x,i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(i(w,x)),v5),n(i(i(v6,i(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9)))),v12)),i(i(n(v12),i(i(n(v13),v14),v6)),i(v13,v12)))))))),i(z,y))),v15),i(v16,v15))).  [hyper(9,a,36235,a,b,35434,a)].
37535 t(i(x,i(y,i(z,x)))).  [hyper(9,a,7137,a,b,8891,a)].
37756 t(i(x,i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(i(i(i(n(i(w,i(i(v5,i(w,v6)),i(i(n(v6),i(i(n(v7),v8),v5)),i(v7,v6))))),v9),n(i(n(x),v10))),v11)),v12),n(i(v13,i(i(v14,i(v13,v15)),i(i(n(v15),i(i(n(v16),v17),v14)),i(v16,v15))))))))),i(z,y)))).  [hyper(9,a,563,a,b,42,a)].
37764 t(i(i(x,i(i(i(n(i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(w),v5),n(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8))))))))),i(z,y))),i(i(n(v11),v12),w)),i(v11,i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(w),v5),n(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8))))))))),i(z,y)))),v13)),i(i(n(v13),i(i(n(v14),v15),x)),i(v14,v13)))).  [hyper(9,a,42,a,b,10,a)].
37842 t(i(i(i(n(x),y),i(n(z),i(i(n(i(i(n(u),i(i(n(w),v5),n(v6))),i(w,u))),v7),n(i(v8,i(i(v9,i(v8,v10)),i(i(n(v10),i(i(n(v11),v12),v9)),i(v11,v10)))))))),i(i(n(i(x,z)),i(i(n(v13),v14),v6)),i(v13,i(x,z))))).  [hyper(9,a,37756,a,b,27279,a)].
37843 t(i(i(n(i(x,i(y,z))),i(i(n(u),w),i(i(n(y),v5),i(n(z),i(i(n(i(i(n(v6),i(i(n(v7),v8),n(i(i(n(v9),i(i(n(v10),v11),n(x))),i(v10,v9))))),i(v7,v6))),v12),n(i(v13,i(i(v14,i(v13,v15)),i(i(n(v15),i(i(n(v16),v17),v14)),i(v16,v15)))))))))),i(u,i(x,i(y,z))))).  [hyper(9,a,37842,a,b,32438,a)].
37888 t(i(i(n(x),i(i(n(i(i(n(y),i(i(n(z),u),n(i(i(n(w),i(i(n(v5),v6),n(v7))),i(v5,w))))),i(z,y))),v8),n(i(v9,i(i(v10,i(v9,v11)),i(i(n(v11),i(i(n(v12),v13),v10)),i(v12,v11))))))),i(v7,i(v14,x)))).  [hyper(9,a,37756,a,b,37843,a)].
37980 t(i(i(n(i(x,i(i(n(y),i(i(n(z),u),i(i(n(i(w,i(i(v5,i(w,v6)),i(i(n(v6),i(i(n(v7),v8),v5)),i(v7,v6))))),v9),n(i(n(v10),v11))))),i(z,y)))),i(i(n(v12),v13),v10)),i(v12,i(x,i(i(n(y),i(i(n(z),u),i(i(n(i(w,i(i(v5,i(w,v6)),i(i(n(v6),i(i(n(v7),v8),v5)),i(v7,v6))))),v9),n(i(n(v10),v11))))),i(z,y)))))).  [hyper(9,a,790,a,b,32438,a)].
37986 t(i(x,i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(i(w,x)),v5),i(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8)))),y))))),i(z,y)))).  [hyper(9,a,37756,a,b,3095,a)].
37987 t(i(x,i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(i(i(n(w),i(i(n(v5),v6),n(x))),i(v5,w))),v7),i(i(v8,i(i(v9,i(v8,v10)),i(i(n(v10),i(i(n(v11),v12),v9)),i(v11,v10)))),y))))),i(z,y)))).  [hyper(9,a,33688,a,b,3095,a)].
38250 t(i(i(x,i(i(y,i(i(n(z),i(i(n(u),w),i(n(z),i(i(n(i(v5,y)),v6),i(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9)))),z))))),i(u,z))),v12)),i(i(n(v12),i(i(n(v13),v14),x)),i(v13,v12)))).  [hyper(9,a,37986,a,b,10,a)].
38418 t(i(i(i(n(x),y),i(z,i(i(u,i(i(w,i(u,v5)),i(i(n(v5),i(i(n(v6),v7),w)),i(v6,v5)))),v8))),i(i(n(i(x,i(v9,v8))),i(i(n(v10),v11),i(i(n(v9),v12),z))),i(v10,i(x,i(v9,v8)))))).  [hyper(9,a,37987,a,b,17176,a)].
38505 t(i(i(n(i(x,i(y,i(z,i(u,w))))),i(i(n(v5),v6),i(i(n(y),v7),w))),i(v5,i(x,i(y,i(z,i(u,w))))))).  [hyper(9,a,7137,a,b,38418,a)].
39017 t(i(i(n(i(i(n(i(x,y)),i(i(n(z),u),i(w,i(i(i(v5,i(i(i(n(i(v6,v7)),i(i(n(v8),v9),i(i(v10,v6),i(i(v11,i(i(v12,i(v11,v13)),i(i(n(v13),i(i(n(v14),v15),v12)),i(v14,v13)))),v7)))),i(v8,i(v6,v7))),v16)),i(i(n(v16),i(i(n(v17),v18),v5)),i(v17,v16))),y)))),i(z,i(x,y)))),i(i(n(v19),v20),i(n(y),i(i(n(x),v21),w)))),i(v19,i(i(n(i(x,y)),i(i(n(z),u),i(w,i(i(i(v5,i(i(i(n(i(v6,v7)),i(i(n(v8),v9),i(i(v10,v6),i(i(v11,i(i(v12,i(v11,v13)),i(i(n(v13),i(i(n(v14),v15),v12)),i(v14,v13)))),v7)))),i(v8,i(v6,v7))),v16)),i(i(n(v16),i(i(n(v17),v18),v5)),i(v17,v16))),y)))),i(z,i(x,y)))))).  [hyper(9,a,10,a,b,33515,a)].
39021 t(i(x,i(y,i(i(n(z),i(i(n(u),w),i(n(z),i(i(n(i(v5,i(i(v6,i(v5,v7)),i(i(n(v7),i(i(n(v8),v9),v6)),i(v8,v7))))),v10),n(i(v11,x)))))),i(u,z))))).  [hyper(9,a,37987,a,b,1004,a)].
39351 t(i(i(x,i(i(y,i(z,i(i(n(u),i(i(n(w),v5),i(n(u),i(i(n(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8))))),v11),n(i(v12,y)))))),i(w,u)))),v13)),i(i(n(v13),i(i(n(v14),v15),x)),i(v14,v13)))).  [hyper(9,a,39021,a,b,10,a)].
39903 t(i(x,i(y,i(i(n(z),i(i(n(u),w),i(i(n(i(v5,i(i(v6,i(v5,v7)),i(i(n(v7),i(i(n(v8),v9),v6)),i(v8,v7))))),v10),n(i(n(i(v11,i(i(v12,i(v11,v13)),i(i(n(v13),i(i(n(v14),v15),v12)),i(v14,v13))))),v16))))),i(u,z))))).  [hyper(9,a,638,a,b,37980,a)].
40047 t(i(x,i(i(n(y),i(i(n(z),u),i(i(n(i(w,i(i(v5,i(w,v6)),i(i(n(v6),i(i(n(v7),v8),v5)),i(v7,v6))))),v9),n(i(n(i(v10,i(i(v11,i(v10,v12)),i(i(n(v12),i(i(n(v13),v14),v11)),i(v13,v12))))),v15))))),i(z,y)))).  [hyper(9,a,39903,a,b,39903,a)].
40399 t(i(x,i(y,i(i(n(z),i(i(n(u),w),i(n(z),i(i(n(i(i(v5,i(i(n(y),v6),v7)),i(i(n(v7),i(i(n(v8),v9),v5)),i(v8,v7)))),v10),n(i(v11,i(i(v12,i(v11,v13)),i(i(n(v13),i(i(n(v14),v15),v12)),i(v14,v13))))))))),i(u,z))))).  [hyper(9,a,638,a,b,249,a)].
40511 t(i(i(i(x,i(i(n(i(y,z)),i(i(n(u),w),i(n(i(y,z)),i(i(n(i(i(n(v5),i(i(n(v6),v7),n(x))),i(v6,v5))),v8),i(i(v9,y),i(i(v10,i(i(v11,i(v10,v12)),i(i(n(v12),i(i(n(v13),v14),v11)),i(v13,v12)))),z)))))),i(u,i(y,z)))),v15),i(v16,v15))).  [hyper(9,a,40047,a,b,37096,a)].
40532 t(i(x,i(y,i(i(z,u),i(i(n(i(i(n(u),i(i(n(w),v5),v6)),i(w,u))),i(i(n(v7),v8),z)),i(v7,i(i(n(u),i(i(n(w),v5),v6)),i(w,u)))))))).  [hyper(9,a,40399,a,b,8445,a)].
40593 t(i(x,i(y,i(i(z,i(i(i(n(u),i(i(n(w),v5),n(i(i(v6,v7),i(i(n(i(i(n(v7),i(i(n(v8),v9),v10)),i(v8,v7))),i(i(n(v11),v12),v6)),i(v11,i(i(n(v7),i(i(n(v8),v9),v10)),i(v8,v7)))))))),i(w,u)),v13)),i(i(n(v13),i(i(n(v14),v15),z)),i(v14,v13)))))).  [hyper(9,a,40532,a,b,991,a)].
40607 t(i(i(x,i(i(y,i(z,i(i(u,w),i(i(n(i(i(n(w),i(i(n(v5),v6),v7)),i(v5,w))),i(i(n(v8),v9),u)),i(v8,i(i(n(w),i(i(n(v5),v6),v7)),i(v5,w))))))),v10)),i(i(n(v10),i(i(n(v11),v12),x)),i(v11,v10)))).  [hyper(9,a,40532,a,b,10,a)].
40751 t(i(x,i(i(y,i(i(i(n(z),i(i(n(u),w),n(i(i(v5,v6),i(i(n(i(i(n(v6),i(i(n(v7),v8),v9)),i(v7,v6))),i(i(n(v10),v11),v5)),i(v10,i(i(n(v6),i(i(n(v7),v8),v9)),i(v7,v6)))))))),i(u,z)),v12)),i(i(n(v12),i(i(n(v13),v14),y)),i(v13,v12))))).  [hyper(9,a,40607,a,b,40593,a)].
41162 t(i(i(n(i(i(n(i(i(n(i(i(n(x),i(i(n(y),z),u)),i(y,x))),i(i(n(w),v5),v6)),i(w,i(i(n(x),i(i(n(y),z),u)),i(y,x))))),i(i(n(v7),v8),i(n(i(i(n(i(i(n(x),i(i(n(y),z),u)),i(y,x))),i(i(n(w),v5),v6)),i(w,i(i(n(x),i(i(n(y),z),u)),i(y,x))))),i(i(n(v9),v10),i(u,i(v6,x)))))),i(v7,i(i(n(i(i(n(x),i(i(n(y),z),u)),i(y,x))),i(i(n(w),v5),v6)),i(w,i(i(n(x),i(i(n(y),z),u)),i(y,x))))))),i(i(n(v11),v12),v9)),i(v11,i(i(n(i(i(n(i(i(n(x),i(i(n(y),z),u)),i(y,x))),i(i(n(w),v5),v6)),i(w,i(i(n(x),i(i(n(y),z),u)),i(y,x))))),i(i(n(v7),v8),i(n(i(i(n(i(i(n(x),i(i(n(y),z),u)),i(y,x))),i(i(n(w),v5),v6)),i(w,i(i(n(x),i(i(n(y),z),u)),i(y,x))))),i(i(n(v9),v10),i(u,i(v6,x)))))),i(v7,i(i(n(i(i(n(x),i(i(n(y),z),u)),i(y,x))),i(i(n(w),v5),v6)),i(w,i(i(n(x),i(i(n(y),z),u)),i(y,x))))))))).  [hyper(9,a,10,a,b,40,a)].
41434 t(i(x,i(i(n(i(y,z)),i(i(n(u),w),i(i(i(n(v5),i(i(n(v6),v7),n(y))),i(v6,v5)),i(i(n(i(v8,i(i(v9,i(v8,v10)),i(i(n(v10),i(i(n(v11),v12),v9)),i(v11,v10))))),v13),z)))),i(u,i(y,z))))).  [hyper(9,a,31338,a,b,7784,a)].
41888 t(i(i(n(i(i(n(i(i(x,i(y,z)),i(i(n(z),i(i(n(u),w),x)),i(u,z)))),i(i(n(v5),v6),v7)),i(v5,i(i(x,i(y,z)),i(i(n(z),i(i(n(u),w),x)),i(u,z)))))),i(i(n(v8),v9),i(n(i(i(n(i(i(x,i(y,z)),i(i(n(z),i(i(n(u),w),x)),i(u,z)))),i(i(n(v5),v6),v7)),i(v5,i(i(x,i(y,z)),i(i(n(z),i(i(n(u),w),x)),i(u,z)))))),i(i(n(i(v10,i(i(v11,i(v10,v12)),i(i(n(v12),i(i(n(v13),v14),v11)),i(v13,v12))))),v15),y)))),i(v8,i(i(n(i(i(x,i(y,z)),i(i(n(z),i(i(n(u),w),x)),i(u,z)))),i(i(n(v5),v6),v7)),i(v5,i(i(x,i(y,z)),i(i(n(z),i(i(n(u),w),x)),i(u,z)))))))).  [hyper(9,a,164,a,b,18,a)].
42070 t(i(x,i(i(i(n(i(i(n(y),i(i(n(z),u),n(i(i(n(w),i(i(n(v5),v6),n(x))),i(v5,w))))),i(z,y))),v7),i(i(v8,v9),i(i(v10,i(i(v11,i(v10,v12)),i(i(n(v12),i(i(n(v13),v14),v11)),i(v13,v12)))),v15))),i(v9,v15)))).  [hyper(9,a,40751,a,b,28109,a)].
42168 t(i(i(i(n(i(i(n(x),i(i(n(y),z),n(i(i(n(u),i(i(n(w),v5),n(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8))))))),i(w,u))))),i(y,x))),v11),i(i(v12,v13),i(i(v14,i(i(v15,i(v14,v16)),i(i(n(v16),i(i(n(v17),v18),v15)),i(v17,v16)))),v19))),i(v13,v19))).  [hyper(9,a,10,a,b,42070,a)].
42509 t(i(i(i(n(x),y),z),i(i(n(i(x,u)),i(i(n(w),v5),i(z,i(i(i(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8)))),v11),i(v12,v11)),u)))),i(w,i(x,u))))).  [hyper(9,a,41434,a,b,9837,a)].
42517 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(w,i(v5,x)),i(i(i(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8)))),v11),i(v12,v11)),y)))),i(z,i(x,y)))).  [hyper(9,a,37888,a,b,42509,a)].
42823 t(i(i(n(i(x,y)),i(i(n(z),u),i(n(i(x,y)),i(i(n(i(i(n(i(i(n(w),i(i(n(v5),v6),i(n(w),i(i(n(v7),v8),n(i(v9,i(i(v10,i(v9,v11)),i(i(n(v11),i(i(n(v12),v13),v10)),i(v12,v11))))))))),i(v5,w))),i(i(n(v14),v15),v7)),i(v14,i(i(n(w),i(i(n(v5),v6),i(n(w),i(i(n(v7),v8),n(i(v9,i(i(v10,i(v9,v11)),i(i(n(v11),i(i(n(v12),v13),v10)),i(v12,v11))))))))),i(v5,w))))),v16),i(i(i(n(v17),i(i(n(v18),v19),n(x))),i(v18,v17)),i(i(v20,i(i(v21,i(v20,v22)),i(i(n(v22),i(i(n(v23),v24),v21)),i(v23,v22)))),y)))))),i(z,i(x,y)))).  [hyper(9,a,19,a,b,37764,a)].
42917 t(i(x,i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(i(i(n(w),i(i(n(v5),v6),n(x))),i(v5,w))),v7),n(i(v8,i(i(i(n(i(v9,i(i(v10,i(v9,v11)),i(i(n(v11),i(i(n(v12),v13),v10)),i(v12,v11))))),v14),n(v8)),v15))))))),i(z,y)))).  [hyper(9,a,40751,a,b,772,a)].
43018 t(i(i(i(n(x),y),i(z,i(i(i(u,i(i(w,i(i(v5,i(w,v6)),i(i(n(v6),i(i(n(v7),v8),v5)),i(v7,v6)))),v9)),i(i(n(v9),i(i(n(v10),v11),u)),i(v10,v9))),v12))),i(i(n(i(x,i(v13,v12))),i(i(n(v14),v15),i(i(n(v13),v16),z))),i(v14,i(x,i(v13,v12)))))).  [hyper(9,a,42917,a,b,36104,a)].
43026 t(i(i(n(i(x,i(y,i(z,u)))),i(i(n(w),v5),i(i(n(y),v6),i(i(v7,z),i(i(i(v8,i(i(v9,i(i(v10,i(v9,v11)),i(i(n(v11),i(i(n(v12),v13),v10)),i(v12,v11)))),v14)),i(i(n(v14),i(i(n(v15),v16),v8)),i(v15,v14))),u))))),i(w,i(x,i(y,i(z,u)))))).  [hyper(9,a,43018,a,b,39351,a)].
43040 t(i(i(i(x,y),i(i(i(z,i(i(u,i(i(w,i(u,v5)),i(i(n(v5),i(i(n(v6),v7),w)),i(v6,v5)))),v8)),i(i(n(v8),i(i(n(v9),v10),z)),i(v9,v8))),v11)),i(v12,i(v13,i(y,v11))))).  [hyper(9,a,42917,a,b,43026,a)].
43285 t(i(x,i(i(n(i(y,z)),i(i(n(u),w),i(n(i(y,z)),i(i(n(i(v5,x)),v6),i(i(v7,y),i(i(v8,i(i(v9,i(v8,v10)),i(i(n(v10),i(i(n(v11),v12),v9)),i(v11,v10)))),z)))))),i(u,i(y,z))))).  [hyper(9,a,42917,a,b,9056,a)].
43410 t(i(i(x,i(i(y,i(i(n(i(z,u)),i(i(n(w),v5),i(n(i(z,u)),i(i(n(i(v6,y)),v7),i(i(v8,z),i(i(v9,i(i(v10,i(v9,v11)),i(i(n(v11),i(i(n(v12),v13),v10)),i(v12,v11)))),u)))))),i(w,i(z,u)))),v14)),i(i(n(v14),i(i(n(v15),v16),x)),i(v15,v14)))).  [hyper(9,a,43285,a,b,10,a)].
45946 t(i(x,i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(i(i(n(w),i(i(n(v5),v6),n(x))),i(v5,w))),v7),n(i(i(v8,i(i(v9,i(i(v10,i(v9,v11)),i(i(n(v11),i(i(n(v12),v13),v10)),i(v12,v11)))),v14)),i(i(n(v14),i(i(n(v15),v16),v8)),i(v15,v14)))))))),i(z,y)))).  [hyper(9,a,40751,a,b,41,a)].
46001 t(i(x,i(i(y,i(i(i(z,i(i(n(i(u,i(i(w,i(u,v5)),i(i(n(v5),i(i(n(v6),v7),w)),i(v6,v5))))),v8),v9)),i(i(n(v9),i(i(n(v10),v11),z)),i(v10,v9))),v12)),i(i(n(v12),i(i(n(v13),v14),y)),i(v13,v12))))).  [hyper(9,a,45946,a,b,7780,a)].
47272 t(i(x,i(y,i(i(n(z),i(i(n(u),w),i(n(z),i(i(n(i(n(i(v5,i(i(v6,i(v5,v7)),i(i(n(v7),i(i(n(v8),v9),v6)),i(v8,v7))))),v10)),v11),n(i(v12,i(i(v13,i(v12,v14)),i(i(n(v14),i(i(n(v15),v16),v13)),i(v15,v14))))))))),i(u,z))))).  [hyper(9,a,2220,a,b,37380,a)].
47630 t(i(x,i(i(n(y),i(i(n(z),u),i(i(w,i(v5,i(i(n(v6),i(i(n(v7),v8),i(n(v6),i(i(n(i(i(n(v9),i(i(n(v10),v11),n(v5))),i(v10,v9))),v12),n(i(i(n(v13),i(i(n(v14),v15),n(w))),i(v14,v13))))))),i(v7,v6)))),y))),i(z,y)))).  [hyper(9,a,47272,a,b,23071,a)].
47735 t(i(x,i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(i(w,x)),v5),i(i(n(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8))))),v11),n(i(v12,i(i(v13,i(v12,v14)),i(i(n(v14),i(i(n(v15),v16),v13)),i(v15,v14)))))))))),i(z,y)))).  [hyper(9,a,47630,a,b,28793,a)].
47838 t(i(i(i(n(i(x,i(i(y,i(x,z)),i(i(n(z),i(i(n(u),w),y)),i(u,z))))),v5),v6),i(v7,i(i(n(v8),i(i(n(v9),v10),i(n(v8),i(i(n(i(i(n(v11),i(i(n(v12),v13),n(v7))),i(v12,v11))),v14),n(v6))))),i(v9,v8))))).  [hyper(9,a,47735,a,b,49,a)].
47948 t(i(i(n(i(i(n(x),i(i(n(y),z),i(n(x),i(i(n(i(i(n(u),i(i(n(w),v5),n(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8))))))),i(w,u))),v11),n(v12))))),i(y,x))),i(i(n(v13),v14),i(i(n(i(v15,i(i(v16,i(v15,v17)),i(i(n(v17),i(i(n(v18),v19),v16)),i(v18,v17))))),v20),v12))),i(v13,i(i(n(x),i(i(n(y),z),i(n(x),i(i(n(i(i(n(u),i(i(n(w),v5),n(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8))))))),i(w,u))),v11),n(v12))))),i(y,x))))).  [hyper(9,a,47838,a,b,18,a)].
47950 t(i(x,i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(i(i(n(w),i(i(n(v5),v6),n(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9))))))),i(v5,w))),v12),n(x))))),i(z,y)))).  [hyper(9,a,47735,a,b,47948,a)].
48052 t(i(i(n(i(x,y)),i(i(n(z),u),y)),i(z,i(x,y)))).  [hyper(9,a,47950,a,b,2421,a)].
48157 t(i(x,i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(i(i(n(w),i(i(n(v5),v6),n(i(v7,i(v8,i(i(v9,i(v8,v10)),i(i(n(v10),i(i(n(v11),v12),v9)),i(v11,v10)))))))),i(v5,w))),v13),n(i(i(n(v14),i(i(n(v15),v16),n(i(v17,x)))),i(v15,v14))))))),i(z,y)))).  [hyper(9,a,47950,a,b,246,a)].
48264 t(i(x,i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(i(i(n(w),i(i(n(v5),v6),n(i(i(n(v7),i(i(n(v8),v9),n(i(v10,i(i(v11,i(v10,v12)),i(i(n(v12),i(i(n(v13),v14),v11)),i(v13,v12))))))),i(v8,v7))))),i(v5,w))),v15),n(i(v16,i(v17,x))))))),i(z,y)))).  [hyper(9,a,48157,a,b,2235,a)].
48328 t(i(x,i(i(n(y),i(i(n(z),u),i(n(y),i(i(n(i(w,i(i(n(v5),i(i(n(v6),v7),n(i(v8,i(i(v9,i(v8,v10)),i(i(n(v10),i(i(n(v11),v12),v9)),i(v11,v10))))))),i(v6,v5)))),v13),n(i(i(n(v14),i(i(n(v15),v16),n(i(v17,x)))),i(v15,v14))))))),i(z,y)))).  [hyper(9,a,48264,a,b,10605,a)].
48377 t(i(x,i(i(n(i(y,z)),i(i(n(u),w),i(n(i(y,z)),i(i(n(i(v5,x)),v6),i(i(i(n(v7),i(i(n(v8),v9),n(y))),i(v8,v7)),i(i(i(i(v10,i(i(v11,i(v10,v12)),i(i(n(v12),i(i(n(v13),v14),v11)),i(v13,v12)))),v15),i(v16,v15)),z)))))),i(u,i(y,z))))).  [hyper(9,a,48328,a,b,29198,a)].
48537 t(i(i(i(n(i(x,i(i(y,i(x,z)),i(i(n(z),i(i(n(u),w),y)),i(u,z))))),v5),i(v6,i(v7,v8))),i(i(n(i(i(n(v8),i(i(n(v9),v10),v6)),i(v9,v8))),i(i(n(v11),v12),v7)),i(v11,i(i(n(v8),i(i(n(v9),v10),v6)),i(v9,v8)))))).  [hyper(9,a,48377,a,b,39,a)].
48539 t(i(x,i(i(i(n(i(y,i(i(z,i(y,u)),i(i(n(u),i(i(n(w),v5),z)),i(w,u))))),v6),i(v7,i(v8,v9))),i(i(n(i(i(n(v9),i(i(n(v10),v11),v7)),i(v10,v9))),i(i(n(v12),v13),v8)),i(v12,i(i(n(v9),i(i(n(v10),v11),v7)),i(v10,v9))))))).  [hyper(9,a,39,a,b,40511,a)].
48548 t(i(i(n(i(x,i(i(n(y),i(i(n(z),u),w)),i(z,y)))),i(i(n(v5),v6),i(i(n(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9))))),v12),i(w,i(i(v13,x),y))))),i(v5,i(x,i(i(n(y),i(i(n(z),u),w)),i(z,y)))))).  [hyper(9,a,48537,a,b,38250,a)].
48572 t(i(i(x,i(i(i(n(y),i(i(n(z),u),n(w))),i(z,y)),v5)),i(w,i(i(n(v5),i(i(n(v6),v7),x)),i(v6,v5))))).  [hyper(9,a,48539,a,b,42168,a)].
48838 t(i(x,i(i(n(y),i(i(n(z),u),i(i(n(i(w,i(i(v5,i(w,v6)),i(i(n(v6),i(i(n(v7),v8),v5)),i(v7,v6))))),v9),i(i(i(n(v10),i(i(n(v11),v12),n(i(i(n(v13),i(i(n(v14),v15),n(x))),i(v14,v13))))),i(v11,v10)),i(i(v16,i(i(v17,i(v16,v18)),i(i(n(v18),i(i(n(v19),v20),v17)),i(v19,v18)))),y))))),i(z,y)))).  [hyper(9,a,59,a,b,48572,a)].
48842 t(i(x,i(i(n(i(i(n(i(y,z)),i(i(n(u),w),i(v5,i(i(i(v6,i(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9)))),v12)),i(i(n(v12),i(i(n(v13),v14),v6)),i(v13,v12))),z)))),i(u,i(y,z)))),i(i(n(v15),v16),i(n(i(i(n(i(y,z)),i(i(n(u),w),i(v5,i(i(i(v6,i(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9)))),v12)),i(i(n(v12),i(i(n(v13),v14),v6)),i(v13,v12))),z)))),i(u,i(y,z)))),i(i(n(i(i(n(v17),i(i(n(v18),v19),n(x))),i(v18,v17))),v20),i(n(z),i(i(n(y),v21),v5)))))),i(v15,i(i(n(i(y,z)),i(i(n(u),w),i(v5,i(i(i(v6,i(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9)))),v12)),i(i(n(v12),i(i(n(v13),v14),v6)),i(v13,v12))),z)))),i(u,i(y,z))))))).  [hyper(9,a,33,a,b,48572,a)].
48844 t(i(x,i(i(n(i(i(n(i(y,z)),i(i(n(u),w),i(v5,i(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8)))),z)))),i(u,i(y,z)))),i(i(n(v11),v12),i(n(i(i(n(i(y,z)),i(i(n(u),w),i(v5,i(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8)))),z)))),i(u,i(y,z)))),i(i(n(i(i(n(v13),i(i(n(v14),v15),n(x))),i(v14,v13))),v16),i(n(z),i(i(n(y),v17),v5)))))),i(v11,i(i(n(i(y,z)),i(i(n(u),w),i(v5,i(i(v6,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8)))),z)))),i(u,i(y,z))))))).  [hyper(9,a,24,a,b,48572,a)].
49068 t(i(i(n(i(i(n(x),i(i(n(y),z),u)),i(y,x))),i(i(n(w),v5),i(u,i(i(i(n(v6),i(i(n(v7),v8),n(i(v9,i(i(v10,i(v9,v11)),i(i(n(v11),i(i(n(v12),v13),v10)),i(v12,v11))))))),i(v7,v6)),x)))),i(w,i(i(n(x),i(i(n(y),z),u)),i(y,x))))).  [hyper(9,a,48572,a,b,18,a)].
49313 t(i(i(x,i(i(y,z),u)),i(z,i(i(n(u),i(i(n(w),v5),x)),i(w,u))))).  [hyper(9,a,48377,a,b,48548,a)].
50228 t(i(x,i(i(n(i(y,z)),i(i(n(u),w),i(n(i(y,z)),i(i(n(i(v5,x)),v6),i(i(v7,y),i(i(i(v8,i(i(v9,i(i(v10,i(v9,v11)),i(i(n(v11),i(i(n(v12),v13),v10)),i(v12,v11)))),v14)),i(i(n(v14),i(i(n(v15),v16),v8)),i(v15,v14))),z)))))),i(u,i(y,z))))).  [hyper(9,a,48838,a,b,33488,a)].
50598 t(i(i(i(n(i(i(n(i(i(n(x),i(i(n(y),z),i(n(x),i(i(n(u),w),n(i(v5,i(i(v6,i(v5,v7)),i(i(n(v7),i(i(n(v8),v9),v6)),i(v8,v7))))))))),i(y,x))),i(i(n(v10),v11),u)),i(v10,i(i(n(x),i(i(n(y),z),i(n(x),i(i(n(u),w),n(i(v5,i(i(v6,i(v5,v7)),i(i(n(v7),i(i(n(v8),v9),v6)),i(v8,v7))))))))),i(y,x))))),v12),i(i(i(n(v13),i(i(n(v14),v15),n(v16))),i(v14,v13)),i(i(v17,i(i(v18,i(v17,v19)),i(i(n(v19),i(i(n(v20),v21),v18)),i(v20,v19)))),v22))),i(v16,v22))).  [hyper(9,a,50228,a,b,42823,a)].
50599 t(i(x,i(i(n(y),i(i(n(z),u),i(i(n(i(i(n(i(i(n(w),i(i(n(v5),v6),i(n(w),i(i(n(v7),v8),n(i(v9,i(i(v10,i(v9,v11)),i(i(n(v11),i(i(n(v12),v13),v10)),i(v12,v11))))))))),i(v5,w))),i(i(n(v14),v15),v7)),i(v14,i(i(n(w),i(i(n(v5),v6),i(n(w),i(i(n(v7),v8),n(i(v9,i(i(v10,i(v9,v11)),i(i(n(v11),i(i(n(v12),v13),v10)),i(v12,v11))))))))),i(v5,w))))),v16),i(i(i(n(v17),i(i(n(v18),v19),n(i(i(n(v20),i(i(n(v21),v22),n(x))),i(v21,v20))))),i(v18,v17)),i(i(v23,i(i(v24,i(v23,v25)),i(i(n(v25),i(i(n(v26),v27),v24)),i(v26,v25)))),y))))),i(z,y)))).  [hyper(9,a,50598,a,b,48572,a)].
50959 t(i(i(n(i(i(i(n(i(i(n(x),i(i(n(y),z),n(u))),i(y,x))),w),i(n(v5),i(i(n(v6),v7),v8))),i(i(n(i(v6,v5)),i(i(n(v9),v10),i(v8,i(i(v11,i(i(v12,i(v11,v13)),i(i(n(v13),i(i(n(v14),v15),v12)),i(v14,v13)))),v5)))),i(v9,i(v6,v5))))),i(i(n(v16),v17),u)),i(v16,i(i(i(n(i(i(n(x),i(i(n(y),z),n(u))),i(y,x))),w),i(n(v5),i(i(n(v6),v7),v8))),i(i(n(i(v6,v5)),i(i(n(v9),v10),i(v8,i(i(v11,i(i(v12,i(v11,v13)),i(i(n(v13),i(i(n(v14),v15),v12)),i(v14,v13)))),v5)))),i(v9,i(v6,v5))))))).  [hyper(9,a,48844,a,b,43410,a)].
50962 t(i(x,i(i(i(n(i(i(n(y),i(i(n(z),u),n(i(w,x)))),i(z,y))),v5),i(n(v6),i(i(n(v7),v8),v9))),i(i(n(i(v7,v6)),i(i(n(v10),v11),i(v9,i(i(v12,i(i(v13,i(v12,v14)),i(i(n(v14),i(i(n(v15),v16),v13)),i(v15,v14)))),v6)))),i(v10,i(v7,v6)))))).  [hyper(9,a,48838,a,b,50959,a)].
50979 t(i(x,i(y,i(i(i(n(i(i(n(z),i(i(n(u),w),n(i(i(n(v5),i(i(n(v6),v7),n(y))),i(v6,v5))))),i(u,z))),v8),i(n(v9),i(i(n(v10),v11),v12))),i(i(n(i(v10,v9)),i(i(n(v13),v14),i(v12,i(i(v15,i(i(v16,i(v15,v17)),i(i(n(v17),i(i(n(v18),v19),v16)),i(v18,v17)))),v9)))),i(v13,i(v10,v9))))))).  [hyper(9,a,50959,a,b,34813,a)].
51010 t(i(i(n(x),i(i(n(y),z),i(n(x),i(i(n(i(u,i(i(w,i(u,v5)),i(i(n(v5),i(i(n(v6),v7),w)),i(v6,v5))))),v8),n(v9))))),i(v9,i(y,x)))).  [hyper(9,a,50962,a,b,42168,a)].
51167 t(i(i(n(i(x,y)),i(i(n(z),u),i(n(y),i(i(n(x),w),i(n(y),i(i(n(i(v5,i(i(v6,i(v5,v7)),i(i(n(v7),i(i(n(v8),v9),v6)),i(v8,v7))))),v10),n(i(v11,i(i(v12,i(v11,v13)),i(i(n(v13),i(i(n(v14),v15),v12)),i(v14,v13))))))))))),i(z,i(x,y)))).  [hyper(9,a,51010,a,b,18,a)].
51883 t(i(i(i(n(x),y),z),i(i(n(i(x,u)),i(i(n(w),v5),i(z,i(i(i(v6,i(i(i(n(i(v7,v8)),i(i(n(v9),v10),i(i(v11,v7),i(i(v12,i(i(v13,i(v12,v14)),i(i(n(v14),i(i(n(v15),v16),v13)),i(v15,v14)))),v8)))),i(v9,i(v7,v8))),v17)),i(i(n(v17),i(i(n(v18),v19),v6)),i(v18,v17))),u)))),i(w,i(x,u))))).  [hyper(9,a,50599,a,b,39017,a)].
51897 t(i(i(n(i(x,i(y,z))),i(i(n(u),w),i(i(n(y),v5),i(n(z),i(i(n(i(i(v6,i(i(i(n(i(v7,v8)),i(i(n(v9),v10),i(i(v11,v7),i(i(v12,i(i(v13,i(v12,v14)),i(i(n(v14),i(i(n(v15),v16),v13)),i(v15,v14)))),v8)))),i(v9,i(v7,v8))),v17)),i(i(n(v17),i(i(n(v18),v19),v6)),i(v18,v17)))),v20),n(x)))))),i(u,i(x,i(y,z))))).  [hyper(9,a,51883,a,b,32438,a)].
51924 t(i(i(i(n(i(x,i(i(y,i(x,z)),i(i(n(z),i(i(n(u),w),y)),i(u,z))))),v5),v6),i(i(n(i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8)))),i(i(n(v11),v12),v13)),i(v11,i(i(v7,i(v6,v8)),i(i(n(v8),i(i(n(v9),v10),v7)),i(v9,v8))))))).  [hyper(9,a,50599,a,b,41888,a)].
51928 t(i(i(n(i(x,i(i(y,i(z,u)),i(i(n(u),i(i(n(w),v5),y)),i(w,u))))),i(i(n(v6),v7),i(i(n(i(v8,i(i(v9,i(v8,v10)),i(i(n(v10),i(i(n(v11),v12),v9)),i(v11,v10))))),v13),z))),i(v6,i(x,i(i(y,i(z,u)),i(i(n(u),i(i(n(w),v5),y)),i(w,u))))))).  [hyper(9,a,51924,a,b,40607,a)].
51935 t(i(x,i(y,i(i(z,i(x,u)),i(i(n(u),i(i(n(w),v5),z)),i(w,u)))))).  [hyper(9,a,50599,a,b,51928,a)].
51956 t(i(i(i(n(i(i(n(i(x,y)),i(i(n(z),u),i(i(i(n(w),i(i(n(v5),v6),n(x))),i(v5,w)),i(i(v7,i(i(v8,i(v7,v9)),i(i(n(v9),i(i(n(v10),v11),v8)),i(v10,v9)))),y)))),i(z,i(x,y)))),v12),i(v13,i(v14,v15))),i(i(n(i(i(n(v15),i(i(n(v16),v17),v13)),i(v16,v15))),i(i(n(v18),v19),v14)),i(v18,i(i(n(v15),i(i(n(v16),v17),v13)),i(v16,v15)))))).  [hyper(9,a,50599,a,b,37,a)].
51957 t(i(i(n(i(x,i(i(n(y),i(i(n(z),u),w)),i(z,y)))),i(i(n(v5),v6),i(i(n(i(i(n(i(v7,v8)),i(i(n(v9),v10),i(i(i(n(v11),i(i(n(v12),v13),n(v7))),i(v12,v11)),i(i(v14,i(i(v15,i(v14,v16)),i(i(n(v16),i(i(n(v17),v18),v15)),i(v17,v16)))),v8)))),i(v9,i(v7,v8)))),v19),i(w,i(i(v20,x),y))))),i(v5,i(x,i(i(n(y),i(i(n(z),u),w)),i(z,y)))))).  [hyper(9,a,51956,a,b,38250,a)].
52137 t(i(i(n(i(i(i(n(i(i(n(x),i(i(n(y),z),n(u))),i(y,x))),w),i(n(v5),i(i(n(v6),v7),v8))),i(i(n(i(v6,v5)),i(i(n(v9),v10),i(v8,i(i(i(v11,i(i(v12,i(i(v13,i(v12,v14)),i(i(n(v14),i(i(n(v15),v16),v13)),i(v15,v14)))),v17)),i(i(n(v17),i(i(n(v18),v19),v11)),i(v18,v17))),v5)))),i(v9,i(v6,v5))))),i(i(n(v20),v21),u)),i(v20,i(i(i(n(i(i(n(x),i(i(n(y),z),n(u))),i(y,x))),w),i(n(v5),i(i(n(v6),v7),v8))),i(i(n(i(v6,v5)),i(i(n(v9),v10),i(v8,i(i(i(v11,i(i(v12,i(i(v13,i(v12,v14)),i(i(n(v14),i(i(n(v15),v16),v13)),i(v15,v14)))),v17)),i(i(n(v17),i(i(n(v18),v19),v11)),i(v18,v17))),v5)))),i(v9,i(v6,v5))))))).  [hyper(9,a,48842,a,b,43410,a)].
52139 t(i(x,i(i(i(n(i(i(n(y),i(i(n(z),u),n(i(i(n(w),i(i(n(v5),v6),n(x))),i(v5,w))))),i(z,y))),v7),i(n(v8),i(i(n(v9),v10),v11))),i(i(n(i(v9,v8)),i(i(n(v12),v13),i(v11,i(i(i(v14,i(i(v15,i(i(v16,i(v15,v17)),i(i(n(v17),i(i(n(v18),v19),v16)),i(v18,v17)))),v20)),i(i(n(v20),i(i(n(v21),v22),v14)),i(v21,v20))),v8)))),i(v12,i(v9,v8)))))).  [hyper(9,a,46001,a,b,52137,a)].
52146 t(i(i(n(x),i(i(n(y),z),i(n(x),i(i(n(i(i(u,i(i(w,i(i(v5,i(w,v6)),i(i(n(v6),i(i(n(v7),v8),v5)),i(v7,v6)))),v9)),i(i(n(v9),i(i(n(v10),v11),u)),i(v10,v9)))),v12),n(v13))))),i(v13,i(y,x)))).  [hyper(9,a,52139,a,b,42168,a)].
52430 t(i(x,i(i(n(i(i(n(i(i(n(y),i(i(n(z),u),w)),i(z,y))),i(i(n(v5),v6),v7)),i(v5,i(i(n(y),i(i(n(z),u),w)),i(z,y))))),i(i(n(v8),v9),i(n(i(i(n(i(i(n(y),i(i(n(z),u),w)),i(z,y))),i(i(n(v5),v6),v7)),i(v5,i(i(n(y),i(i(n(z),u),w)),i(z,y))))),i(i(n(i(v10,x)),v11),i(w,i(v7,y)))))),i(v8,i(i(n(i(i(n(y),i(i(n(z),u),w)),i(z,y))),i(i(n(v5),v6),v7)),i(v5,i(i(n(y),i(i(n(z),u),w)),i(z,y)))))))).  [hyper(9,a,50599,a,b,41162,a)].
52434 t(i(i(x,i(i(y,i(i(n(i(i(n(i(i(n(z),i(i(n(u),w),v5)),i(u,z))),i(i(n(v6),v7),v8)),i(v6,i(i(n(z),i(i(n(u),w),v5)),i(u,z))))),i(i(n(v9),v10),i(n(i(i(n(i(i(n(z),i(i(n(u),w),v5)),i(u,z))),i(i(n(v6),v7),v8)),i(v6,i(i(n(z),i(i(n(u),w),v5)),i(u,z))))),i(i(n(i(v11,y)),v12),i(v5,i(v8,z)))))),i(v9,i(i(n(i(i(n(z),i(i(n(u),w),v5)),i(u,z))),i(i(n(v6),v7),v8)),i(v6,i(i(n(z),i(i(n(u),w),v5)),i(u,z))))))),v13)),i(i(n(v13),i(i(n(v14),v15),x)),i(v14,v13)))).  [hyper(9,a,52430,a,b,10,a)].
53149 t(i(i(n(x),i(i(n(y),z),x)),i(y,x))).  [hyper(9,a,2913,a,b,52434,a)].
54967 t(i(x,i(y,i(n(y),z)))).  [hyper(9,a,9634,a,b,2913,a)].
55318 t(i(i(n(i(x,i(y,z))),i(i(n(u),w),i(i(n(y),v5),z))),i(u,i(x,i(y,z))))).  [hyper(9,a,2745,a,b,43018,a)].
55495 t(i(x,i(y,i(z,i(u,z))))).  [hyper(9,a,2745,a,b,2913,a)].
56454 t(i(x,i(y,i(z,i(u,y))))).  [hyper(9,a,37535,a,b,2913,a)].
56903 t(i(i(n(i(i(n(x),i(i(n(y),z),u)),i(y,x))),i(i(n(w),v5),n(u))),i(w,i(i(n(x),i(i(n(y),z),u)),i(y,x))))).  [hyper(9,a,54967,a,b,51956,a)].
56917 t(i(x,i(y,i(n(x),z)))).  [hyper(9,a,54967,a,b,51167,a)].
56943 t(i(x,i(i(n(y),i(i(n(z),u),n(i(n(x),w)))),i(z,y)))).  [hyper(9,a,54967,a,b,49068,a)].
58749 t(i(i(n(i(n(x),y)),i(i(n(z),u),x)),i(z,i(n(x),y)))).  [hyper(9,a,56917,a,b,52434,a)].
59056 t(i(x,i(y,i(z,i(n(y),u))))).  [hyper(9,a,56917,a,b,2913,a)].
59688 t(i(i(x,i(i(i(i(y,y),z),i(u,z)),w)),i(i(n(w),i(i(n(v5),v6),x)),i(v5,w)))).  [hyper(9,a,117,a,b,10,a)].
60636 t(i(x,i(i(n(i(y,z)),i(i(n(u),w),n(n(z)))),i(u,i(y,z))))).  [hyper(9,a,55495,a,b,12271,a)].
61095 t(i(x,i(y,i(z,i(u,i(w,i(n(x),v5))))))).  [hyper(9,a,56454,a,b,2222,a)].
64650 t(i(i(n(i(x,i(y,i(n(z),u)))),i(i(n(w),v5),i(i(n(y),v6),z))),i(w,i(x,i(y,i(n(z),u)))))).  [hyper(9,a,59056,a,b,43018,a)].
64654 t(i(x,i(n(i(y,x)),z))).  [hyper(9,a,59056,a,b,42168,a)].
66906 t(i(x,i(y,i(n(i(n(x),z)),u)))).  [hyper(9,a,3950,a,b,51167,a)].
67191 t(i(x,i(y,i(z,i(n(i(n(i(n(x),u)),w)),v5))))).  [hyper(9,a,3950,a,b,2222,a)].
67365 t(i(i(n(i(x,i(y,z))),i(i(n(u),w),i(i(n(y),v5),i(i(v6,v6),z)))),i(u,i(x,i(y,z))))).  [hyper(9,a,7151,a,b,43018,a)].
71053 t(i(i(n(i(n(i(n(x),y)),z)),i(i(n(u),w),x)),i(u,i(n(i(n(x),y)),z)))).  [hyper(9,a,66906,a,b,52434,a)].
73016 t(i(i(n(i(x,i(y,i(n(z),u)))),i(i(n(w),v5),z)),i(w,i(x,i(y,i(n(z),u)))))).  [hyper(9,a,7272,a,b,52434,a)].
73319 t(i(x,i(y,i(z,i(u,i(w,i(n(y),v5))))))).  [hyper(9,a,7272,a,b,2913,a)].
73476 t(i(x,i(y,i(n(i(z,x)),u)))).  [hyper(9,a,8461,a,b,42168,a)].
74827 t(i(i(n(i(n(i(x,y)),z)),i(i(n(u),w),y)),i(u,i(n(i(x,y)),z)))).  [hyper(9,a,73476,a,b,52434,a)].
77696 t(i(x,i(y,i(i(n(z),i(i(n(u),w),i(i(v5,v5),z))),i(u,z))))).  [hyper(9,a,95,a,b,37535,a)].
86128 t(i(i(n(x),i(i(n(y),z),i(n(x),i(i(n(i(u,u)),w),x)))),i(y,x))).  [hyper(9,a,53149,a,b,94,a)].
109935 t(i(x,i(y,i(z,i(u,i(w,i(v5,i(n(y),v6)))))))).  [hyper(9,a,61095,a,b,2913,a)].
114155 t(i(x,i(y,i(z,i(n(i(u,x)),w))))).  [hyper(9,a,73319,a,b,42168,a)].
115777 t(i(x,i(y,i(z,i(u,i(n(i(w,y)),v5)))))).  [hyper(9,a,114155,a,b,2913,a)].
122557 t(i(x,i(y,i(n(i(z,i(u,x))),w)))).  [hyper(9,a,115777,a,b,42168,a)].
188510 t(i(x,i(y,i(z,i(u,i(n(i(n(i(n(y),w)),v5)),v6)))))).  [hyper(9,a,67191,a,b,2913,a)].
200905 t(i(x,i(y,i(z,i(u,i(n(i(w,x)),v5)))))).  [hyper(9,a,109935,a,b,42168,a)].
202723 t(i(x,i(y,i(z,i(u,i(w,i(n(i(v5,y)),v6))))))).  [hyper(9,a,200905,a,b,2913,a)].
218847 t(i(x,i(y,i(z,i(n(i(u,i(w,x))),v5))))).  [hyper(9,a,202723,a,b,42168,a)].
220607 t(i(x,i(y,i(z,i(u,i(n(i(w,i(v5,y))),v6)))))).  [hyper(9,a,218847,a,b,2913,a)].
221542 t(i(x,i(y,i(n(i(z,i(u,i(w,x)))),v5)))).  [hyper(9,a,220607,a,b,42168,a)].
423985 t(i(x,i(y,i(n(i(n(i(n(i(z,x)),u)),w)),v5)))).  [hyper(9,a,188510,a,b,42168,a)].
531786 t(i(x,i(i(n(y),i(i(n(z),u),n(w))),i(w,i(z,y))))).  [hyper(9,a,50979,a,b,441,a)].
555001 t(i(i(i(x,i(y,i(z,z))),u),i(w,u))).  [hyper(9,a,56943,a,b,454,a)].
556053 t(i(n(i(i(i(x,i(y,i(z,z))),u),i(w,u))),v5)).  [hyper(9,a,555001,a,b,9634,a)].
561529 t(i(i(n(x),i(i(n(y),z),n(u))),i(u,i(y,x)))).  [hyper(9,a,556053,a,b,531786,a)].
561645 t(i(i(i(x,y),z),i(y,i(i(n(z),i(i(n(u),w),v5)),i(u,z))))).  [hyper(9,a,531786,a,b,51957,a)].
561992 t(i(i(i(n(x),y),z),i(x,i(u,i(w,z))))).  [hyper(9,a,531786,a,b,8453,a)].
562060 t(i(x,i(i(n(y),i(i(n(z),u),i(x,y))),i(z,y)))).  [hyper(9,a,531786,a,b,425,a)].
567877 t(i(i(n(x),i(i(n(y),z),i(i(u,i(n(i(w,u)),v5)),x))),i(y,x))).  [hyper(9,a,64654,a,b,562060,a)].
568335 t(i(i(n(x),i(i(n(y),z),i(i(u,i(n(u),w)),x))),i(y,x))).  [hyper(9,a,9634,a,b,562060,a)].
569038 t(i(x,i(y,i(i(n(z),i(i(n(u),w),i(y,z))),i(u,z))))).  [hyper(9,a,562060,a,b,2913,a)].
569059 t(i(i(n(i(x,y)),i(i(n(z),u),n(x))),i(z,i(x,y)))).  [hyper(9,a,562060,a,b,400,a)].
582104 t(i(x,i(y,i(i(n(i(z,u)),i(i(n(w),v5),n(z))),i(w,i(z,u)))))).  [hyper(9,a,569059,a,b,37535,a)].
764142 t(i(x,i(i(i(n(i(y,y)),z),i(i(n(x),u),w)),w))).  [hyper(9,a,569038,a,b,353,a)].
1098520 t(i(x,i(i(i(n(i(y,y)),z),i(i(u,i(n(x),w)),v5)),v5))).  [hyper(9,a,7152,a,b,353,a)].
1101126 t(i(i(i(n(i(x,x)),y),i(i(z,i(n(i(u,u)),w)),v5)),v5)).  [hyper(9,a,76,a,b,1098520,a)].
1101460 t(i(x,i(y,i(i(i(n(i(z,z)),u),i(i(w,i(n(y),v5)),v6)),v6)))).  [hyper(9,a,1098520,a,b,2913,a)].
1103254 t(i(i(n(i(x,y)),i(i(n(z),u),n(n(y)))),i(z,i(x,y)))).  [hyper(9,a,1101126,a,b,60636,a)].
1119492 t(i(x,i(i(i(n(i(y,i(z,i(u,u)))),w),i(i(v5,v5),v6)),v6))).  [hyper(9,a,77696,a,b,482,a)].
1119496 t(i(x,i(i(i(n(i(y,i(z,z))),u),i(i(w,w),v5)),v5))).  [hyper(9,a,77696,a,b,441,a)].
1119513 t(i(x,i(i(i(n(i(y,y)),z),i(i(u,u),w)),w))).  [hyper(9,a,77696,a,b,353,a)].
1119756 t(i(i(i(n(i(x,x)),y),i(i(z,z),u)),u)).  [hyper(9,a,1119513,a,b,1119513,a)].
1120253 t(i(n(i(i(i(n(i(x,x)),y),i(i(z,z),u)),u)),w)).  [hyper(9,a,1119756,a,b,9634,a)].
1120600 t(i(i(i(n(i(x,i(y,y))),z),i(i(u,u),w)),w)).  [hyper(9,a,1120253,a,b,1119496,a)].
1121320 t(i(n(i(i(i(n(i(x,i(y,y))),z),i(i(u,u),w)),w)),v5)).  [hyper(9,a,1120600,a,b,9634,a)].
1122521 t(i(i(i(n(i(x,i(y,i(z,z)))),u),i(i(w,w),v5)),v5)).  [hyper(9,a,1121320,a,b,1119492,a)].
1422321 t(i(i(i(x,x),y),i(i(n(y),i(i(n(z),u),w)),i(z,y)))).  [hyper(9,a,1122521,a,b,561645,a)].
1423327 t(i(i(n(i(x,y)),i(i(n(z),u),i(i(w,w),y))),i(z,i(x,y)))).  [hyper(9,a,1422321,a,b,40607,a)].
1586143 t(i(x,i(i(i(y,i(n(i(n(x),z)),u)),i(i(w,w),v5)),v5))).  [hyper(9,a,1101460,a,b,353,a)].
1590267 t(i(x,i(y,i(i(i(z,i(n(i(n(y),u)),w)),i(i(v5,v5),v6)),v6)))).  [hyper(9,a,1586143,a,b,2913,a)].
2228848 t(i(x,i(i(i(n(i(y,y)),z),n(u)),i(u,w)))).  [hyper(9,a,582104,a,b,353,a)].
2228879 t(i(i(i(n(i(x,x)),y),n(z)),i(z,u))).  [hyper(9,a,2228848,a,b,2228848,a)].
2229356 t(i(n(x),i(i(n(i(x,y)),i(i(n(z),u),w)),i(z,i(x,y))))).  [hyper(9,a,2228879,a,b,561645,a)].
2234777 t(i(i(n(i(x,i(y,z))),i(i(n(u),w),n(y))),i(u,i(x,i(y,z))))).  [hyper(9,a,2229356,a,b,40607,a)].
2772644 t(i(x,i(i(n(y),i(i(n(z),u),i(z,y))),i(z,y)))).  [hyper(9,a,51935,a,b,567877,a)].
2772951 t(i(i(n(x),i(i(n(y),z),i(y,x))),i(y,x))).  [hyper(9,a,2772644,a,b,2772644,a)].
2773536 t(i(n(i(n(i(n(i(x,n(y))),z)),u)),y)).  [hyper(9,a,423985,a,b,2772951,a)].
2773556 t(i(n(i(x,i(y,i(z,n(u))))),u)).  [hyper(9,a,221542,a,b,2772951,a)].
2773562 t(i(n(i(x,i(y,n(z)))),z)).  [hyper(9,a,122557,a,b,2772951,a)].
2773567 t(i(n(i(n(n(x)),y)),x)).  [hyper(9,a,66906,a,b,2772951,a)].
2776619 t(i(x,i(n(n(i(i(n(x),y),z))),i(n(z),u)))).  [hyper(9,a,2773567,a,b,626,a)].
2777067 t(i(x,i(y,i(z,n(i(i(n(x),u),n(z))))))).  [hyper(9,a,2773562,a,b,2234777,a)].
2777436 t(i(x,i(n(y),i(z,n(i(i(n(x),u),y)))))).  [hyper(9,a,2773562,a,b,58749,a)].
2782281 t(i(x,i(y,i(n(z),i(u,n(i(i(n(x),w),z))))))).  [hyper(9,a,2773556,a,b,626,a)].
2830571 t(i(x,i(n(i(n(i(y,n(i(i(n(x),z),u)))),w)),i(v5,u)))).  [hyper(9,a,2773536,a,b,2222,a)].
2907649 t(i(x,i(y,i(n(z),i(u,n(i(i(n(y),w),z))))))).  [hyper(9,a,2777436,a,b,2913,a)].
3246804 t(i(i(i(n(n(x)),y),x),i(z,x))).  [hyper(9,a,2782281,a,b,52146,a)].
3246813 t(i(x,i(y,i(z,i(u,i(n(w),i(v5,n(i(i(n(z),v6),w))))))))).  [hyper(9,a,2782281,a,b,37535,a)].
3247375 t(i(x,i(i(n(y),i(i(n(z),u),i(i(n(n(y)),w),y))),i(z,y)))).  [hyper(9,a,3246804,a,b,49313,a)].
3396167 t(i(i(i(n(i(n(x),y)),z),u),i(x,u))).  [hyper(9,a,2907649,a,b,52146,a)].
5599485 t(i(n(i(n(i(x,n(i(i(n(i(y,y)),z),u)))),w)),i(v5,u))).  [hyper(9,a,76,a,b,2830571,a)].
6084155 t(i(x,i(i(i(y,y),i(i(z,i(u,i(w,i(v5,z)))),v6)),v6))).  [hyper(9,a,1590267,a,b,2598,a)].
6542912 t(i(x,i(n(i(y,n(i(i(n(i(z,z)),u),n(n(w)))))),w))).  [hyper(9,a,5599485,a,b,1103254,a)].
6543104 t(i(n(i(x,n(i(i(n(i(y,y)),z),n(n(u)))))),u)).  [hyper(9,a,6542912,a,b,6542912,a)].
6652897 t(i(i(i(x,x),i(i(y,i(z,i(u,i(w,y)))),v5)),v5)).  [hyper(9,a,6543104,a,b,6084155,a)].
7525676 t(i(x,i(y,i(n(z),i(u,n(i(i(n(i(n(y),w)),v5),z))))))).  [hyper(9,a,3246813,a,b,3112,a)].
7526334 t(i(i(i(n(i(n(i(n(x),y)),z)),u),w),i(x,w))).  [hyper(9,a,7525676,a,b,52146,a)].
10121568 t(i(i(i(n(i(n(x),y)),z),u),i(x,i(w,u)))).  [hyper(9,a,3247375,a,b,8582,a)].
10277255 t(i(x,i(n(y),i(y,z)))).  [hyper(9,a,582104,a,b,8895,a)].
10277262 t(i(x,i(i(n(y),i(i(n(i(z,i(n(x),u))),w),n(i(v5,v5)))),y))).  [hyper(9,a,7153,a,b,8895,a)].
10277271 t(i(n(x),i(x,y))).  [hyper(9,a,10277255,a,b,10277255,a)].
10281111 t(i(n(n(i(i(n(i(n(x),i(x,y))),z),u))),i(n(u),w))).  [hyper(9,a,10277271,a,b,2776619,a)].
10281265 t(i(i(i(n(i(x,x)),y),i(i(n(i(n(z),i(z,u))),w),v5)),v5)).  [hyper(9,a,10277271,a,b,764142,a)].
10281278 t(i(i(n(x),i(i(n(y),z),i(i(n(u),i(u,w)),x))),i(y,x))).  [hyper(9,a,10277271,a,b,562060,a)].
11778211 t(i(i(i(n(x),i(x,y)),z),z)).  [hyper(9,a,10277262,a,b,10281278,a)].
11778296 t(i(n(x),i(y,i(x,z)))).  [hyper(9,a,10277262,a,b,2234777,a)].
11778298 t(i(n(n(x)),i(y,x))).  [hyper(9,a,10277262,a,b,1103254,a)].
11778303 t(i(i(i(x,i(n(x),y)),z),z)).  [hyper(9,a,10277262,a,b,568335,a)].
11778392 t(i(n(i(x,i(y,n(z)))),i(u,z))).  [hyper(9,a,10277262,a,b,12070,a)].
11778479 t(i(i(i(x,y),i(i(z,i(u,i(w,w))),v5)),i(y,v5))).  [hyper(9,a,10277262,a,b,482,a)].
11778490 t(i(i(i(x,y),i(i(z,i(u,u)),w)),i(y,w))).  [hyper(9,a,10277262,a,b,441,a)].
11778494 t(i(i(i(n(x),y),i(i(z,i(u,u)),w)),i(x,w))).  [hyper(9,a,10277262,a,b,415,a)].
11778499 t(i(i(i(x,y),i(i(z,z),u)),i(y,u))).  [hyper(9,a,10277262,a,b,353,a)].
11780427 t(i(x,i(y,n(n(x))))).  [hyper(9,a,11778298,a,b,561529,a)].
11796295 t(i(x,i(y,i(z,n(n(i(n(i(n(x),u)),w))))))).  [hyper(9,a,11780427,a,b,10121568,a)].
11796577 t(i(x,i(y,n(n(i(n(i(n(i(n(x),z)),u)),w)))))).  [hyper(9,a,11780427,a,b,7526334,a)].
11796619 t(n(n(i(x,x)))).  [hyper(9,a,11780427,a,b,6652897,a)].
11797023 t(i(x,i(y,n(n(i(n(i(n(x),z)),u)))))).  [hyper(9,a,11780427,a,b,3396167,a)].
11798201 t(i(x,i(y,i(z,i(u,n(n(i(n(x),w)))))))).  [hyper(9,a,11780427,a,b,561992,a)].
11798558 t(i(i(n(n(n(x))),i(i(n(y),z),x)),i(y,n(n(x))))).  [hyper(9,a,11780427,a,b,52434,a)].
11798591 t(i(x,i(y,i(z,n(n(y)))))).  [hyper(9,a,11780427,a,b,2913,a)].
11798623 t(i(x,n(n(n(n(i(y,y))))))).  [hyper(9,a,11796619,a,b,11780427,a)].
11837041 t(i(x,i(y,n(n(i(n(x),z)))))).  [hyper(9,a,11798591,a,b,1423327,a)].
11837355 t(i(x,i(y,i(z,n(n(i(n(x),u))))))).  [hyper(9,a,11798591,a,b,48052,a)].
11837359 t(i(x,n(n(i(y,x))))).  [hyper(9,a,11798591,a,b,42168,a)].
11837363 t(i(x,i(y,i(z,i(u,i(w,n(n(i(n(x),v5))))))))).  [hyper(9,a,11798591,a,b,8991,a)].
11854803 t(i(x,i(y,i(z,n(n(i(u,i(n(x),w)))))))).  [hyper(9,a,11837359,a,b,561992,a)].
11855057 t(i(x,i(y,n(n(i(z,y)))))).  [hyper(9,a,11837359,a,b,2913,a)].
11874586 t(i(x,i(y,n(n(n(n(i(z,z)))))))).  [hyper(9,a,11798623,a,b,10121568,a)].
11887556 t(i(x,i(y,n(n(i(z,i(n(x),u))))))).  [hyper(9,a,11855057,a,b,48052,a)].
11887597 t(i(x,n(n(i(i(i(n(y),i(y,z)),u),u))))).  [hyper(9,a,11778211,a,b,11780427,a)].
11890041 t(i(x,n(n(i(i(i(y,i(n(y),z)),u),u))))).  [hyper(9,a,11778303,a,b,11780427,a)].
11935737 t(i(n(i(n(n(x)),y)),i(z,x))).  [hyper(9,a,11837041,a,b,561529,a)].
12020049 t(i(x,i(y,i(z,n(n(z)))))).  [hyper(9,a,11778392,a,b,2234777,a)].
12020171 t(i(x,i(y,i(z,i(u,n(n(x))))))).  [hyper(9,a,11778392,a,b,561529,a)].
12020446 t(i(x,i(y,n(n(y))))).  [hyper(9,a,12020049,a,b,12020049,a)].
12020532 t(i(x,n(n(x)))).  [hyper(9,a,12020049,a,b,10281265,a)].
12199391 t(n(n(i(x,i(y,n(n(n(n(i(z,z)))))))))).  [hyper(9,a,11874586,a,b,12020532,a)].
12594916 t(i(n(i(x,i(n(n(y)),z))),i(u,y))).  [hyper(9,a,11887556,a,b,561529,a)].
12804010 t(i(x,i(y,i(n(n(n(y))),z)))).  [hyper(9,a,12594916,a,b,569059,a)].
12806405 t(i(x,i(y,i(z,i(n(n(n(i(n(x),u)))),w))))).  [hyper(9,a,12804010,a,b,8458,a)].
12871407 t(i(x,i(y,i(z,n(n(i(u,x))))))).  [hyper(9,a,12020171,a,b,11778499,a)].
12871409 t(i(x,i(y,n(n(i(n(i(z,x)),u)))))).  [hyper(9,a,11837355,a,b,11778499,a)].
12871862 t(i(i(i(n(i(x,x)),y),z),i(n(z),u))).  [hyper(9,a,58749,a,b,11778499,a)].
12891722 t(i(x,i(y,i(z,i(u,i(w,n(n(i(v5,z))))))))).  [hyper(9,a,12871407,a,b,37535,a)].
12976312 t(i(n(i(n(i(x,n(y))),z)),i(u,y))).  [hyper(9,a,12871409,a,b,561529,a)].
13018848 t(i(x,i(n(i(y,n(n(i(z,i(u,n(w))))))),w))).  [hyper(9,a,12976312,a,b,12070,a)].
13018852 t(i(x,i(n(i(y,n(z))),i(u,i(w,z))))).  [hyper(9,a,12976312,a,b,8991,a)].
13128408 t(i(n(i(n(i(n(n(x)),y)),z)),i(u,x))).  [hyper(9,a,11797023,a,b,561529,a)].
13642630 t(i(n(i(x,n(n(n(n(i(y,y))))))),z)).  [hyper(9,a,12199391,a,b,10281111,a)].
13811303 t(i(n(i(x,n(y))),i(z,i(u,y)))).  [hyper(9,a,13642630,a,b,13018852,a)].
13873297 t(i(x,i(y,i(n(i(n(n(n(x))),z)),u)))).  [hyper(9,a,13128408,a,b,561529,a)].
13873503 t(i(x,i(n(i(n(n(y)),z)),i(u,i(w,y))))).  [hyper(9,a,13128408,a,b,8991,a)].
13950057 t(i(x,i(n(i(n(n(n(i(y,x)))),z)),u))).  [hyper(9,a,13873297,a,b,11778499,a)].
14027870 t(i(x,i(y,i(z,n(n(i(n(i(u,x)),w))))))).  [hyper(9,a,11798201,a,b,11778499,a)].
14159602 t(i(x,i(y,n(n(i(z,i(n(i(u,x)),w))))))).  [hyper(9,a,11854803,a,b,11778499,a)].
14202392 t(n(n(i(i(i(n(x),i(x,y)),z),z)))).  [hyper(9,a,13950057,a,b,11887597,a)].
14208615 t(n(n(i(i(i(x,i(n(x),y)),z),z)))).  [hyper(9,a,14202392,a,b,11890041,a)].
14834687 t(i(n(i(n(n(x)),y)),i(z,i(u,x)))).  [hyper(9,a,14208615,a,b,13873503,a)].
14910339 t(i(x,i(y,n(n(i(n(i(z,i(u,x))),w)))))).  [hyper(9,a,14027870,a,b,11778499,a)].
14921820 t(i(n(i(x,i(n(i(y,n(z))),u))),i(w,z))).  [hyper(9,a,14159602,a,b,561529,a)].
14984505 t(i(n(i(n(i(x,i(y,n(z)))),u)),i(w,z))).  [hyper(9,a,14910339,a,b,561529,a)].
15048077 t(i(x,i(n(i(y,i(z,n(i(i(u,u),w))))),w))).  [hyper(9,a,14984505,a,b,1423327,a)].
15048293 t(i(x,i(n(i(y,i(z,n(u)))),i(w,i(v5,u))))).  [hyper(9,a,14984505,a,b,8991,a)].
15824130 t(i(x,i(y,i(n(n(n(i(n(i(z,x)),u)))),w)))).  [hyper(9,a,12806405,a,b,11778499,a)].
15868845 t(i(x,i(n(i(y,i(n(z),u))),i(z,w)))).  [hyper(9,a,12891722,a,b,51897,a)].
15868855 t(i(x,i(y,i(z,n(n(i(u,i(w,i(v5,y))))))))).  [hyper(9,a,12891722,a,b,8895,a)].
15868905 t(i(n(i(n(i(x,i(n(y),z))),i(y,u))),w)).  [hyper(9,a,15868845,a,b,12871862,a)].
15893886 t(i(n(i(x,n(n(i(y,i(z,n(u))))))),u)).  [hyper(9,a,15868905,a,b,13018848,a)].
16042332 t(i(n(i(x,i(y,n(i(i(z,z),u))))),u)).  [hyper(9,a,15893886,a,b,15048077,a)].
16045189 t(i(n(i(x,i(y,n(z)))),i(u,i(w,z)))).  [hyper(9,a,16042332,a,b,15048293,a)].
16099958 t(i(n(n(n(i(n(i(x,n(y))),z)))),y)).  [hyper(9,a,15824130,a,b,2772951,a)].
16102528 t(i(x,i(n(n(n(i(n(i(y,n(z))),u)))),z))).  [hyper(9,a,16099958,a,b,2913,a)].
16105583 t(i(x,i(y,n(n(i(z,i(u,i(w,x)))))))).  [hyper(9,a,16102528,a,b,15868855,a)].
16121140 t(i(n(i(x,i(y,i(z,n(u))))),i(w,u))).  [hyper(9,a,16105583,a,b,561529,a)].
16335329 t(i(n(i(n(i(n(i(n(n(x)),y)),z)),u)),i(w,x))).  [hyper(9,a,11796577,a,b,561529,a)].
16524256 t(i(x,i(y,i(z,i(u,n(n(i(n(i(w,x)),v5)))))))).  [hyper(9,a,11837363,a,b,11778499,a)].
18009520 t(i(x,i(y,i(z,n(n(i(n(i(u,i(w,x))),v5))))))).  [hyper(9,a,16524256,a,b,11778499,a)].
18226421 t(i(x,i(y,n(n(i(n(i(z,i(u,i(w,x)))),v5)))))).  [hyper(9,a,18009520,a,b,11778499,a)].
18334992 t(i(n(i(n(i(x,i(y,i(z,n(u))))),w)),i(v5,u))).  [hyper(9,a,18226421,a,b,561529,a)].
18512067 t(i(x,i(y,n(n(i(n(i(n(i(z,x)),u)),w)))))).  [hyper(9,a,11796295,a,b,11778479,a)].
18567584 t(i(n(i(n(i(n(i(x,n(y))),z)),u)),i(w,y))).  [hyper(9,a,18512067,a,b,561529,a)].
18581687 t(i(x,i(n(i(n(i(y,n(n(z)))),u)),i(z,w)))).  [hyper(9,a,18567584,a,b,2234777,a)].
18581711 t(i(x,i(n(i(n(i(y,n(n(n(z))))),u)),z))).  [hyper(9,a,18567584,a,b,1103254,a)].
18581895 t(i(x,i(n(i(n(i(y,n(z))),u)),i(w,i(v5,z))))).  [hyper(9,a,18567584,a,b,8991,a)].
18581912 t(i(x,i(n(i(n(i(y,n(z))),u)),i(n(z),w)))).  [hyper(9,a,18567584,a,b,626,a)].
18581919 t(i(n(i(n(i(x,n(n(n(y))))),z)),y)).  [hyper(9,a,18581711,a,b,18581711,a)].
18583529 t(n(n(i(n(i(n(i(x,n(n(n(y))))),z)),y)))).  [hyper(9,a,18581919,a,b,12020532,a)].
18587586 t(i(n(i(n(i(x,n(n(y)))),z)),i(y,u))).  [hyper(9,a,18583529,a,b,18581687,a)].
18601118 t(i(n(i(n(i(x,n(y))),z)),i(n(y),u))).  [hyper(9,a,18587586,a,b,18581912,a)].
18602293 t(n(n(i(n(i(n(i(x,n(y))),z)),i(n(y),u))))).  [hyper(9,a,18601118,a,b,12020532,a)].
18634767 t(i(n(i(n(i(x,n(y))),z)),i(u,i(w,y)))).  [hyper(9,a,18602293,a,b,18581895,a)].
18636936 t(i(x,i(n(i(y,n(z))),i(u,i(w,i(v5,z)))))).  [hyper(9,a,18634767,a,b,38505,a)].
18636966 t(i(x,i(n(i(y,n(z))),i(n(i(u,z)),w)))).  [hyper(9,a,18634767,a,b,626,a)].
18636972 t(i(n(i(x,n(y))),i(n(i(z,y)),u))).  [hyper(9,a,18636966,a,b,18636966,a)].
18638590 t(n(n(i(n(i(x,n(y))),i(n(i(z,y)),u))))).  [hyper(9,a,18636972,a,b,12020532,a)].
18642593 t(i(n(i(x,n(y))),i(z,i(u,i(w,y))))).  [hyper(9,a,18638590,a,b,18636936,a)].
18841415 t(i(x,n(n(n(n(i(n(x),y))))))).  [hyper(9,a,12020446,a,b,11798558,a)].
18842468 t(i(i(i(n(i(x,i(y,y))),z),u),n(n(u)))).  [hyper(9,a,11798558,a,b,11778490,a)].
18842469 t(i(i(i(n(i(x,i(y,i(z,z)))),u),w),n(n(w)))).  [hyper(9,a,11798558,a,b,11778479,a)].
18864781 t(i(x,i(y,n(n(n(n(i(n(y),z)))))))).  [hyper(9,a,18841415,a,b,2913,a)].
18920840 t(i(x,i(y,n(n(n(n(i(n(i(n(x),z)),u)))))))).  [hyper(9,a,18864781,a,b,48052,a)].
19556234 t(i(n(n(n(i(n(i(n(n(x)),y)),z)))),i(u,x))).  [hyper(9,a,18920840,a,b,561529,a)].
19599068 t(i(x,i(y,n(n(i(n(i(n(n(n(x))),z)),u)))))).  [hyper(9,a,19556234,a,b,561529,a)].
19610048 t(i(n(i(n(i(n(n(n(n(x)))),y)),z)),i(u,x))).  [hyper(9,a,19599068,a,b,561529,a)].
19622356 t(i(x,i(n(i(n(n(n(n(i(i(y,y),z))))),u)),z))).  [hyper(9,a,19610048,a,b,1423327,a)].
19622357 t(i(x,i(n(i(n(n(n(n(n(n(y)))))),z)),y))).  [hyper(9,a,19610048,a,b,1103254,a)].
19622540 t(i(x,i(n(i(n(n(n(n(y)))),z)),i(u,i(w,y))))).  [hyper(9,a,19610048,a,b,8991,a)].
19622554 t(i(x,i(n(i(n(n(n(n(y)))),z)),i(u,y)))).  [hyper(9,a,19610048,a,b,2222,a)].
19622565 t(i(n(i(n(n(n(n(n(n(x)))))),y)),x)).  [hyper(9,a,19622357,a,b,19622357,a)].
19626442 t(i(n(i(n(n(n(n(x)))),y)),i(z,x))).  [hyper(9,a,19622565,a,b,19622554,a)].
19629940 t(i(x,i(n(n(n(n(n(n(y)))))),y))).  [hyper(9,a,19626442,a,b,1103254,a)].
19630024 t(i(x,i(y,i(n(n(n(n(n(x))))),z)))).  [hyper(9,a,19626442,a,b,561529,a)].
19630292 t(i(x,i(n(n(n(n(y)))),i(z,y)))).  [hyper(9,a,19626442,a,b,2222,a)].
19630309 t(i(n(n(n(n(n(n(x)))))),x)).  [hyper(9,a,19629940,a,b,19629940,a)].
19635005 t(i(n(n(n(n(x)))),i(y,x))).  [hyper(9,a,19630309,a,b,19630292,a)].
19639423 t(i(x,i(y,n(n(n(n(x))))))).  [hyper(9,a,19635005,a,b,561529,a)].
19659330 t(i(x,n(n(n(n(i(y,x))))))).  [hyper(9,a,19639423,a,b,11778499,a)].
19661654 t(i(x,i(y,i(z,n(n(n(n(y)))))))).  [hyper(9,a,19639423,a,b,2913,a)].
19683802 t(i(x,i(y,n(n(n(n(i(z,y)))))))).  [hyper(9,a,19659330,a,b,2913,a)].
19694215 t(i(x,i(y,n(n(n(n(i(n(x),z)))))))).  [hyper(9,a,19661654,a,b,1423327,a)].
19694529 t(i(x,i(y,i(z,n(n(n(n(i(n(x),u))))))))).  [hyper(9,a,19661654,a,b,48052,a)].
19694541 t(i(x,i(y,i(z,i(u,n(n(n(n(i(n(x),w)))))))))).  [hyper(9,a,19661654,a,b,8458,a)].
19699796 t(i(x,i(y,n(n(n(n(i(z,i(n(x),u))))))))).  [hyper(9,a,19683802,a,b,48052,a)].
19723689 t(i(x,i(y,i(z,i(n(n(n(n(n(y))))),u))))).  [hyper(9,a,19630024,a,b,2913,a)].
19751104 t(i(n(n(n(i(n(n(x)),y)))),i(z,x))).  [hyper(9,a,19694215,a,b,561529,a)].
19794935 t(i(x,i(y,n(n(i(n(n(n(x))),z)))))).  [hyper(9,a,19751104,a,b,561529,a)].
19814680 t(i(x,i(y,i(z,n(n(i(n(n(n(y))),u))))))).  [hyper(9,a,19794935,a,b,2913,a)].
19962613 t(i(x,i(y,n(n(n(n(i(n(i(z,x)),u)))))))).  [hyper(9,a,19694529,a,b,11778499,a)].
19985952 t(i(n(n(n(i(x,i(n(n(y)),z))))),i(u,y))).  [hyper(9,a,19699796,a,b,561529,a)].
19992384 t(i(x,i(y,i(n(n(n(n(n(i(n(x),z)))))),u)))).  [hyper(9,a,19723689,a,b,1423327,a)].
20007530 t(i(x,i(y,n(n(i(n(n(n(i(n(x),z)))),u)))))).  [hyper(9,a,19814680,a,b,1423327,a)].
20027297 t(i(n(n(n(i(n(i(x,n(y))),z)))),i(u,y))).  [hyper(9,a,19962613,a,b,561529,a)].
20039501 t(i(x,i(y,n(n(i(z,i(n(n(n(x))),u))))))).  [hyper(9,a,19985952,a,b,561529,a)].
20053598 t(i(x,i(y,n(n(i(n(i(z,n(n(x)))),u)))))).  [hyper(9,a,20027297,a,b,561529,a)].
20064664 t(i(n(i(x,i(n(n(n(n(y)))),z))),i(u,y))).  [hyper(9,a,20039501,a,b,561529,a)].
20075876 t(i(n(i(n(i(x,n(n(n(y))))),z)),i(u,y))).  [hyper(9,a,20053598,a,b,561529,a)].
20088370 t(i(x,i(y,i(z,i(n(n(n(n(n(x))))),u))))).  [hyper(9,a,20064664,a,b,561529,a)].
20128266 t(i(x,i(n(i(y,n(n(n(i(i(z,z),u)))))),u))).  [hyper(9,a,20075876,a,b,1423327,a)].
20128267 t(i(x,i(n(i(y,n(n(n(n(n(z))))))),z))).  [hyper(9,a,20075876,a,b,1103254,a)].
20128450 t(i(x,i(n(i(y,n(n(n(z))))),i(u,i(w,z))))).  [hyper(9,a,20075876,a,b,8991,a)].
20128464 t(i(x,i(n(i(y,n(n(n(z))))),i(u,z)))).  [hyper(9,a,20075876,a,b,2222,a)].
20128475 t(i(n(i(x,n(n(n(n(n(y))))))),y)).  [hyper(9,a,20128267,a,b,20128267,a)].
20132384 t(i(n(i(x,n(n(n(y))))),i(z,y))).  [hyper(9,a,20128475,a,b,20128464,a)].
20136005 t(i(x,i(y,i(z,n(n(n(n(x)))))))).  [hyper(9,a,20132384,a,b,561529,a)].
20183219 t(i(x,i(y,n(n(n(n(i(z,x)))))))).  [hyper(9,a,20136005,a,b,11778499,a)].
20185521 t(i(x,i(y,i(z,i(u,n(n(n(n(i(w,z)))))))))).  [hyper(9,a,20136005,a,b,43040,a)].
20185523 t(i(x,i(y,i(z,i(u,i(w,n(n(n(n(z)))))))))).  [hyper(9,a,20136005,a,b,37535,a)].
20219274 t(i(n(n(n(i(x,n(y))))),i(z,y))).  [hyper(9,a,20183219,a,b,561529,a)].
20221767 t(i(x,i(y,n(n(i(z,n(n(x)))))))).  [hyper(9,a,20219274,a,b,561529,a)].
20244251 t(i(x,i(y,i(z,n(n(i(u,n(n(y))))))))).  [hyper(9,a,20221767,a,b,2913,a)].
20331000 t(i(x,i(y,n(n(i(z,n(n(i(n(x),u))))))))).  [hyper(9,a,20244251,a,b,1423327,a)].
20331188 t(i(x,i(y,i(z,n(n(i(u,n(n(i(n(x),w)))))))))).  [hyper(9,a,20244251,a,b,48052,a)].
20345103 t(i(x,i(y,i(n(n(n(n(n(i(z,x)))))),u)))).  [hyper(9,a,20088370,a,b,11778499,a)].
20348728 t(i(x,i(n(n(i(i(n(y),z),u))),i(y,u)))).  [hyper(9,a,11935737,a,b,55318,a)].
20409232 t(i(n(i(x,n(n(i(n(n(y)),z))))),i(u,y))).  [hyper(9,a,20331000,a,b,561529,a)].
20420468 t(i(n(n(n(n(n(i(x,n(y))))))),y)).  [hyper(9,a,20345103,a,b,2772951,a)].
20423219 t(i(x,i(n(n(n(n(n(i(y,n(z))))))),z))).  [hyper(9,a,20420468,a,b,2913,a)].
20426677 t(i(n(n(i(i(n(x),y),z))),i(x,z))).  [hyper(9,a,20423219,a,b,20348728,a)].
20456017 t(i(x,i(y,i(z,n(n(i(n(n(n(x))),u))))))).  [hyper(9,a,20409232,a,b,561529,a)].
20508026 t(i(x,i(y,n(n(i(n(n(n(i(z,x)))),u)))))).  [hyper(9,a,20456017,a,b,11778499,a)].
20525906 t(i(n(i(n(n(n(i(x,n(y))))),z)),i(u,y))).  [hyper(9,a,20508026,a,b,561529,a)].
20673059 t(i(n(n(n(n(n(i(n(n(x)),y)))))),x)).  [hyper(9,a,19992384,a,b,2772951,a)].
20675481 t(i(x,i(n(n(n(n(n(i(n(n(y)),z)))))),y))).  [hyper(9,a,20673059,a,b,2913,a)].
20686627 t(i(n(i(n(n(n(i(n(n(x)),y)))),z)),i(u,x))).  [hyper(9,a,20007530,a,b,561529,a)].
20700865 t(i(n(i(x,n(n(n(i(i(y,y),z)))))),z)).  [hyper(9,a,20675481,a,b,20128266,a)].
20703237 t(i(n(i(x,n(n(n(y))))),i(z,i(u,y)))).  [hyper(9,a,20700865,a,b,20128450,a)].
20781144 t(i(x,i(y,n(n(n(n(i(z,i(u,i(w,y)))))))))).  [hyper(9,a,20185521,a,b,42517,a)].
20781959 t(i(x,i(y,i(z,n(n(n(n(i(u,i(w,y)))))))))).  [hyper(9,a,20185523,a,b,42517,a)].
20868282 t(i(x,i(n(n(n(i(n(n(n(n(y)))),z)))),y))).  [hyper(9,a,20686627,a,b,1103254,a)].
20868519 t(n(n(i(n(n(n(i(n(n(n(n(x)))),y)))),x)))).  [hyper(9,a,20868282,a,b,18842468,a)].
20885867 t(i(x,n(n(n(n(i(y,i(z,i(u,x))))))))).  [hyper(9,a,20868519,a,b,20781144,a)].
20901599 t(i(x,i(y,n(n(n(n(i(z,i(u,x))))))))).  [hyper(9,a,20885867,a,b,20781959,a)].
20917155 t(i(n(n(n(i(x,i(y,n(z)))))),i(u,z))).  [hyper(9,a,20901599,a,b,561529,a)].
20918808 t(i(x,i(y,n(n(i(z,i(u,n(n(x))))))))).  [hyper(9,a,20917155,a,b,561529,a)].
20932594 t(n(n(i(x,i(y,n(n(i(z,i(u,n(n(x))))))))))).  [hyper(9,a,20918808,a,b,12020532,a)].
20933884 t(i(n(i(x,i(y,n(n(n(z)))))),i(u,z))).  [hyper(9,a,20918808,a,b,561529,a)].
21016667 t(i(x,i(y,n(n(i(z,i(u,n(n(i(n(x),w)))))))))).  [hyper(9,a,20932594,a,b,20426677,a)].
21423488 t(i(i(i(i(i(x,x),y),i(z,y)),u),i(w,u))).  [hyper(9,a,59688,a,b,11778490,a)].
21470153 t(i(n(i(n(n(n(n(i(i(x,x),y))))),z)),y)).  [hyper(9,a,21423488,a,b,19622356,a)].
21471932 t(i(n(i(n(n(n(n(x)))),y)),i(z,i(u,x)))).  [hyper(9,a,21470153,a,b,19622540,a)].
21579491 t(i(x,i(y,i(z,n(n(n(n(i(n(i(u,x)),w))))))))).  [hyper(9,a,19694541,a,b,11778499,a)].
21875728 t(i(x,i(y,n(n(i(z,n(n(i(n(i(u,x)),w))))))))).  [hyper(9,a,20331188,a,b,11778499,a)].
21993368 t(i(n(i(x,i(y,n(n(i(n(n(z)),u)))))),i(w,z))).  [hyper(9,a,21016667,a,b,561529,a)].
22035429 t(i(x,i(y,n(n(n(n(i(n(i(z,i(u,x))),w)))))))).  [hyper(9,a,21579491,a,b,11778499,a)].
22066572 t(i(n(i(x,n(n(i(n(i(y,n(z))),u))))),i(w,z))).  [hyper(9,a,21875728,a,b,561529,a)].
22122359 t(i(x,i(y,i(z,i(u,n(n(i(n(n(n(x))),w)))))))).  [hyper(9,a,21993368,a,b,561529,a)].
22149671 t(i(n(n(n(i(n(i(x,i(y,n(z)))),u)))),i(w,z))).  [hyper(9,a,22035429,a,b,561529,a)].
22169600 t(i(x,i(y,i(z,n(n(i(n(i(u,n(n(x)))),w))))))).  [hyper(9,a,22066572,a,b,561529,a)].
22224671 t(i(x,i(y,i(z,n(n(i(n(n(n(i(u,x)))),w))))))).  [hyper(9,a,22122359,a,b,11778499,a)].
22243284 t(i(x,i(y,n(n(i(n(i(z,i(u,n(n(x))))),w)))))).  [hyper(9,a,22149671,a,b,561529,a)].
22263034 t(i(x,i(y,n(n(i(n(i(z,n(n(i(u,x))))),w)))))).  [hyper(9,a,22169600,a,b,11778499,a)].
22284151 t(i(x,i(y,n(n(i(n(n(n(i(z,i(u,x))))),w)))))).  [hyper(9,a,22224671,a,b,11778499,a)].
22327310 t(i(n(i(n(i(x,i(y,n(n(n(z)))))),u)),i(w,z))).  [hyper(9,a,22243284,a,b,561529,a)].
22344947 t(i(n(i(n(i(x,n(n(i(y,n(z)))))),u)),i(w,z))).  [hyper(9,a,22263034,a,b,561529,a)].
22388288 t(i(n(i(n(n(n(i(x,i(y,n(z)))))),u)),i(w,z))).  [hyper(9,a,22284151,a,b,561529,a)].
22431710 t(i(x,i(n(i(y,n(n(i(z,n(n(n(u)))))))),u))).  [hyper(9,a,22344947,a,b,1103254,a)].
22431839 t(i(x,i(n(i(y,n(n(i(z,n(u)))))),i(w,u)))).  [hyper(9,a,22344947,a,b,2222,a)].
22431850 t(i(n(i(x,n(n(i(y,n(n(n(z)))))))),z)).  [hyper(9,a,22431710,a,b,22431710,a)].
22434370 t(i(n(i(x,n(n(i(y,n(z)))))),i(u,z))).  [hyper(9,a,22431850,a,b,22431839,a)].
22802804 t(i(x,i(n(n(n(n(y)))),i(z,i(n(y),u))))).  [hyper(9,a,21471932,a,b,64650,a)].
22802856 t(i(x,i(n(i(y,n(z))),i(u,i(n(z),w))))).  [hyper(9,a,18634767,a,b,64650,a)].
22803462 t(i(n(n(n(n(x)))),i(y,i(n(x),z)))).  [hyper(9,a,22802804,a,b,22802804,a)].
22806860 t(i(n(i(x,n(y))),i(z,i(n(y),u)))).  [hyper(9,a,22803462,a,b,22802856,a)].
23150330 t(i(x,i(n(n(n(n(i(i(y,y),z))))),i(u,z)))).  [hyper(9,a,21471932,a,b,67365,a)].
23150338 t(i(x,i(n(i(y,n(i(i(z,z),u)))),i(w,u)))).  [hyper(9,a,18634767,a,b,67365,a)].
23150349 t(i(x,i(n(n(i(i(y,y),z))),i(u,z)))).  [hyper(9,a,14834687,a,b,67365,a)].
23150357 t(i(i(i(n(x),y),i(i(z,z),u)),i(w,i(x,u)))).  [hyper(9,a,10277262,a,b,67365,a)].
23150408 t(i(n(n(i(i(x,x),y))),i(z,y))).  [hyper(9,a,23150349,a,b,23150349,a)].
23154303 t(i(x,i(y,n(i(i(z,z),n(x)))))).  [hyper(9,a,23150408,a,b,561529,a)].
23176819 t(n(n(i(x,i(y,n(i(i(z,z),n(x)))))))).  [hyper(9,a,23154303,a,b,12020532,a)].
23286187 t(i(x,i(y,n(i(i(z,z),n(i(n(x),u))))))).  [hyper(9,a,23176819,a,b,20426677,a)].
23393820 t(i(i(i(x,x),n(i(n(n(y)),z))),i(u,y))).  [hyper(9,a,23286187,a,b,561529,a)].
23432959 t(i(n(n(n(n(i(i(x,x),y))))),i(z,y))).  [hyper(9,a,23393820,a,b,23150330,a)].
23435370 t(i(x,i(y,n(n(n(i(i(z,z),n(x)))))))).  [hyper(9,a,23432959,a,b,561529,a)].
23452554 t(i(n(n(i(i(x,x),n(n(y))))),i(z,y))).  [hyper(9,a,23435370,a,b,561529,a)].
23471656 t(i(x,i(y,n(i(i(z,z),n(n(n(x)))))))).  [hyper(9,a,23452554,a,b,561529,a)].
23487234 t(i(x,n(i(i(y,y),n(n(n(i(n(x),z)))))))).  [hyper(9,a,23471656,a,b,11778494,a)].
23541276 t(n(i(i(x,x),n(n(n(i(n(i(y,y)),z))))))).  [hyper(9,a,76,a,b,23487234,a)].
23548004 t(i(n(i(x,n(i(i(y,y),z)))),i(u,z))).  [hyper(9,a,23541276,a,b,23150338,a)].
23820481 t(i(x,i(n(i(n(y),z)),n(i(i(u,u),y))))).  [hyper(9,a,23548004,a,b,71053,a)].
23820517 t(i(x,i(n(i(n(y),z)),n(n(i(u,n(y))))))).  [hyper(9,a,22434370,a,b,71053,a)].
23820547 t(i(x,i(n(i(n(y),z)),i(u,n(n(n(y))))))).  [hyper(9,a,20933884,a,b,71053,a)].
23820553 t(i(x,i(n(i(n(i(y,z)),u)),n(n(n(z)))))).  [hyper(9,a,20703237,a,b,71053,a)].
23820591 t(i(x,i(n(i(n(y),z)),n(n(n(y)))))).  [hyper(9,a,20132384,a,b,71053,a)].
23820658 t(i(x,i(n(i(n(i(y,i(z,u))),w)),n(u)))).  [hyper(9,a,18642593,a,b,71053,a)].
23820702 t(i(x,i(n(i(n(y),z)),i(u,i(w,n(y)))))).  [hyper(9,a,16121140,a,b,71053,a)].
23820704 t(i(x,i(n(i(n(i(y,z)),u)),i(w,n(z))))).  [hyper(9,a,16045189,a,b,71053,a)].
23820780 t(i(x,i(n(i(n(i(y,z)),u)),n(z)))).  [hyper(9,a,13811303,a,b,71053,a)].
23820808 t(i(x,i(n(i(n(y),z)),i(n(n(y)),u)))).  [hyper(9,a,12594916,a,b,71053,a)].
23820927 t(i(x,i(n(i(n(y),z)),i(u,n(y))))).  [hyper(9,a,11778392,a,b,71053,a)].
23822135 t(i(n(i(n(x),y)),n(n(n(x))))).  [hyper(9,a,23820591,a,b,23820591,a)].
23825806 t(i(n(i(n(i(x,y)),z)),n(y))).  [hyper(9,a,23822135,a,b,23820780,a)].
23829477 t(i(n(i(n(x),y)),i(z,n(x)))).  [hyper(9,a,23825806,a,b,23820927,a)].
23831165 t(i(x,n(i(i(y,y),n(i(n(i(n(z),u)),i(w,n(z)))))))).  [hyper(9,a,23829477,a,b,23154303,a)].
23841151 t(n(n(i(n(i(n(x),y)),i(n(n(x)),z))))).  [hyper(9,a,23820808,a,b,18842469,a)].
23848227 t(i(n(i(n(x),y)),n(i(i(z,z),x)))).  [hyper(9,a,23841151,a,b,23820481,a)].
23850381 t(i(n(i(n(x),y)),n(n(i(z,n(x)))))).  [hyper(9,a,23848227,a,b,23820517,a)].
23852535 t(i(n(i(n(x),y)),i(z,n(n(n(x)))))).  [hyper(9,a,23850381,a,b,23820547,a)].
23854744 t(i(n(i(n(i(x,y)),z)),n(n(n(y))))).  [hyper(9,a,23852535,a,b,23820553,a)].
23856898 t(i(n(i(n(i(x,i(y,z))),u)),n(z))).  [hyper(9,a,23854744,a,b,23820658,a)].
23859054 t(i(n(i(n(x),y)),i(z,i(u,n(x))))).  [hyper(9,a,23856898,a,b,23820702,a)].
23860628 t(i(n(i(n(i(x,y)),z)),i(u,n(y)))).  [hyper(9,a,23859054,a,b,23820704,a)].
23862204 t(i(x,i(n(i(y,z)),i(u,i(w,i(v5,i(n(n(z)),v6))))))).  [hyper(9,a,23860628,a,b,2552,a)].
23923374 t(i(x,i(n(n(n(i(y,i(z,n(u)))))),i(w,i(n(u),v5))))).  [hyper(9,a,22388288,a,b,73016,a)].
23923377 t(i(x,i(n(i(y,n(n(i(z,n(u)))))),i(w,i(n(u),v5))))).  [hyper(9,a,22344947,a,b,73016,a)].
23923378 t(i(x,i(n(i(y,i(z,n(n(n(u)))))),i(w,i(n(u),v5))))).  [hyper(9,a,22327310,a,b,73016,a)].
23923391 t(i(x,i(n(n(n(n(y)))),i(z,i(n(i(u,y)),w))))).  [hyper(9,a,21471932,a,b,73016,a)].
23923413 t(i(x,i(n(n(n(i(y,n(z))))),i(u,i(n(z),w))))).  [hyper(9,a,20525906,a,b,73016,a)].
23923449 t(i(x,i(n(i(y,n(n(n(z))))),i(u,i(n(z),w))))).  [hyper(9,a,20075876,a,b,73016,a)].
23923506 t(i(x,i(n(i(y,n(z))),i(u,i(n(i(w,z)),v5))))).  [hyper(9,a,18634767,a,b,73016,a)].
23923514 t(i(x,i(n(i(y,i(z,i(u,n(w))))),i(v5,i(n(w),v6))))).  [hyper(9,a,18334992,a,b,73016,a)].
23923548 t(i(x,i(n(i(n(i(n(n(y)),z)),u)),i(w,i(n(y),v5))))).  [hyper(9,a,16335329,a,b,73016,a)].
23923581 t(i(x,i(n(i(y,i(z,n(u)))),i(w,i(n(u),v5))))).  [hyper(9,a,14984505,a,b,73016,a)].
23923626 t(i(x,i(n(i(n(n(y)),z)),i(u,i(n(y),w))))).  [hyper(9,a,13128408,a,b,73016,a)].
23993438 t(i(x,i(n(i(y,z)),n(i(i(u,u),z))))).  [hyper(9,a,23548004,a,b,74827,a)].
23993453 t(i(x,i(n(i(y,i(n(z),u))),n(z)))).  [hyper(9,a,22806860,a,b,74827,a)].
23993464 t(i(x,i(n(i(y,z)),n(n(i(u,n(z))))))).  [hyper(9,a,22434370,a,b,74827,a)].
23993493 t(i(x,i(n(i(y,z)),i(u,n(n(n(z))))))).  [hyper(9,a,20933884,a,b,74827,a)].
23993499 t(i(x,i(n(i(y,i(z,u))),n(n(n(u)))))).  [hyper(9,a,20703237,a,b,74827,a)].
23993589 t(i(x,i(n(i(y,i(z,i(u,w)))),n(w)))).  [hyper(9,a,18642593,a,b,74827,a)].
23993626 t(i(x,i(n(i(y,i(z,u))),i(w,n(u))))).  [hyper(9,a,16045189,a,b,74827,a)].
23993661 t(i(x,i(n(i(y,z)),i(n(i(u,n(z))),w)))).  [hyper(9,a,14921820,a,b,74827,a)].
23994978 t(n(n(i(n(i(x,i(n(y),z))),n(y))))).  [hyper(9,a,23993453,a,b,18842469,a)].
23999816 t(i(n(i(x,y)),n(i(i(z,z),y)))).  [hyper(9,a,23994978,a,b,23993438,a)].
24002406 t(i(n(i(x,y)),n(n(i(z,n(y)))))).  [hyper(9,a,23999816,a,b,23993464,a)].
24004631 t(i(n(i(x,y)),i(z,n(n(n(y)))))).  [hyper(9,a,24002406,a,b,23993493,a)].
24006815 t(i(n(i(x,i(y,z))),n(n(n(z))))).  [hyper(9,a,24004631,a,b,23993499,a)].
24008977 t(i(n(i(x,i(y,i(z,u)))),n(u))).  [hyper(9,a,24006815,a,b,23993589,a)].
24011147 t(i(n(i(x,i(y,z))),i(u,n(z)))).  [hyper(9,a,24008977,a,b,23993626,a)].
24013315 t(i(x,i(i(n(y),i(i(n(z),u),i(n(y),y))),i(z,y)))).  [hyper(9,a,24011147,a,b,101,a)].
24024759 t(n(n(i(n(i(x,y)),i(n(i(z,n(y))),u))))).  [hyper(9,a,23993661,a,b,18842469,a)].
24051991 t(i(n(i(n(n(x)),y)),i(z,i(n(x),u)))).  [hyper(9,a,24024759,a,b,23923626,a)].
24052800 t(i(x,i(n(n(y)),i(z,i(n(i(n(y),u)),w))))).  [hyper(9,a,24051991,a,b,73016,a)].
24073096 t(n(n(i(n(n(x)),i(y,i(n(i(n(x),z)),u)))))).  [hyper(9,a,24052800,a,b,18842469,a)].
24076842 t(i(x,i(y,i(z,n(i(i(n(i(n(y),u)),w),n(z))))))).  [hyper(9,a,2777067,a,b,23150357,a)].
24184345 t(i(n(n(n(n(x)))),i(y,i(n(i(z,x)),u)))).  [hyper(9,a,24073096,a,b,23923391,a)].
24185346 t(i(n(n(n(i(x,n(y))))),i(z,i(n(y),u)))).  [hyper(9,a,24184345,a,b,23923413,a)].
24186170 t(i(n(i(x,n(n(n(y))))),i(z,i(n(y),u)))).  [hyper(9,a,24185346,a,b,23923449,a)].
24186972 t(i(x,i(n(i(n(i(n(y),z)),u)),n(n(n(y)))))).  [hyper(9,a,24186170,a,b,71053,a)].
24189275 t(n(n(i(n(i(n(i(n(x),y)),z)),n(n(n(x))))))).  [hyper(9,a,24186972,a,b,18842469,a)].
24190962 t(i(n(i(x,n(y))),i(z,i(n(i(u,y)),w)))).  [hyper(9,a,24189275,a,b,23923506,a)].
24191764 t(i(x,i(n(i(n(i(n(i(y,z)),u)),w)),n(z)))).  [hyper(9,a,24190962,a,b,71053,a)].
24194147 t(n(n(i(n(i(n(i(n(i(x,y)),z)),u)),n(y))))).  [hyper(9,a,24191764,a,b,18842469,a)].
24195954 t(i(n(i(x,i(y,n(z)))),i(u,i(n(z),w)))).  [hyper(9,a,24194147,a,b,23923581,a)].
24196756 t(i(x,i(n(i(y,i(n(z),u))),i(w,n(z))))).  [hyper(9,a,24195954,a,b,74827,a)].
24196778 t(i(n(i(x,i(n(y),z))),i(u,n(y)))).  [hyper(9,a,24196756,a,b,24196756,a)].
24197998 t(i(x,i(i(n(y),i(i(n(n(z)),u),z)),i(n(z),y)))).  [hyper(9,a,24196778,a,b,56903,a)].
24233020 t(i(i(n(x),i(i(n(i(y,y)),z),x)),x)).  [hyper(9,a,10277262,a,b,86128,a)].
24233753 t(i(x,i(i(n(y),i(i(n(i(z,z)),u),y)),y))).  [hyper(9,a,24233020,a,b,2913,a)].
24752165 t(i(x,n(i(i(n(i(n(i(n(x),y)),z)),u),n(x))))).  [hyper(9,a,24076842,a,b,2772951,a)].
24761841 t(i(i(n(x),i(i(n(n(y)),z),y)),i(n(y),x))).  [hyper(9,a,24752165,a,b,24197998,a)].
24763566 t(i(n(i(x,y)),x)).  [hyper(9,a,11778296,a,b,24761841,a)].
24766720 t(i(x,i(i(i(n(x),y),n(z)),i(z,u)))).  [hyper(9,a,24763566,a,b,2234777,a)].
24824166 t(i(i(i(n(i(x,i(y,i(z,y)))),u),n(w)),i(w,v5))).  [hyper(9,a,2745,a,b,24766720,a)].
25474177 t(i(i(i(x,x),n(i(n(i(n(y),z)),i(u,n(y))))),w)).  [hyper(9,a,23831165,a,b,24824166,a)].
25474957 t(i(n(i(x,y)),i(z,i(u,i(w,i(n(n(y)),v5)))))).  [hyper(9,a,25474177,a,b,23862204,a)].
25477082 t(i(n(n(n(i(x,i(y,n(z)))))),i(u,i(n(z),w)))).  [hyper(9,a,25474957,a,b,23923374,a)].
25477157 t(i(n(i(x,n(n(i(y,n(z)))))),i(u,i(n(z),w)))).  [hyper(9,a,25477082,a,b,23923377,a)].
25477237 t(i(n(i(x,i(y,n(n(n(z)))))),i(u,i(n(z),w)))).  [hyper(9,a,25477157,a,b,23923378,a)].
25477503 t(i(n(i(x,i(y,i(z,n(u))))),i(w,i(n(u),v5)))).  [hyper(9,a,25477237,a,b,23923514,a)].
25477585 t(i(n(i(n(i(n(n(x)),y)),z)),i(u,i(n(x),w)))).  [hyper(9,a,25477503,a,b,23923548,a)].
25478202 t(i(i(n(x),i(i(n(y),z),i(n(x),x))),i(y,x))).  [hyper(9,a,25477585,a,b,24013315,a)].
25478228 t(i(i(n(x),x),x)).  [hyper(9,a,24233753,a,b,25478202,a)].
25478229 $F # answer(L2).  [resolve(25478228,a,16,a)].

============================== end of proof ==========================