clear(echo_input). clear(print_initial_clauses). clear(print_given). clear(degrade_hints). assign(max_megs, 32000). %assign(max_megs, 1907000). % 2 TB = 1907348.6328125 MiB assign(max_seconds, -1). set(hyper_resolution). %assign(backsub_check, -1). %assign(max_proofs, 7). %set(production). %assign(sos_limit, 2000000). %assign(variable_weight, 0). %assign(constant_weight, 0). %list(weights). %weight(t(x)) = weight(x). %weight(i(x,y)) = (weight(x) + weight(y)) + 1. %weight(n(n(n(n(x))))) = weight(x) + 100. %weight(n(n(n(x)))) = weight(x) + 10. %weight(n(n(x))) = weight(x) + 4. %weight(n(x)) = weight(x) + 1. %end_of_list. formulas(assumptions). % Modus Ponens: (|- p, |- Cpq) => q t(x) & t(i(x,y)) -> t(y) #label(MP). % Walsh's 2nd Axiom: CpCCqCprCCNrCCNstqCsr t(i(u,i(i(v,i(u,w)),i(i(n(w),i(i(n(x),y),v)),i(x,w))))) #label(w2). end_of_list. formulas(goals). % Theorems: Cpp,CpCqp,CCpCqrCCpqCpr,CCNpNqCqp t(i(p,p)) #answer(id). t(i(p,i(q,p))) #answer(A1). t(i(i(p,i(q,r)),i(i(p,q),i(p,r)))) #answer(A2). t(i(i(n(p),n(q)),i(q,p))) #answer(A3). % Theorems: CCpqCCqrCpr,CCNppp,CpCNpq t(i(i(p,q),i(i(q,r),i(p,r)))) #answer(L1). t(i(i(n(p),p),p)) #answer(L2). t(i(p,i(n(p),q))) #answer(L3). end_of_list. formulas(hints). t(i(i(x0,i(i(x1,i(i(x2,i(x1,x3)),i(i(n(x3),i(i(n(x4),x5),x2)),i(x4,x3)))),x6)),i(i(n(x6),i(i(n(x7),x8),x0)),i(x7,x6)))). t(i(i(n(i(i(n(i(i(n(x0),i(i(n(x1),x2),x3)),i(x1,x0))),i(i(n(x4),x5),x6)),i(x4,i(i(n(x0),i(i(n(x1),x2),x3)),i(x1,x0))))),i(i(n(x7),x8),i(x3,i(x6,x0)))),i(x7,i(i(n(i(i(n(x0),i(i(n(x1),x2),x3)),i(x1,x0))),i(i(n(x4),x5),x6)),i(x4,i(i(n(x0),i(i(n(x1),x2),x3)),i(x1,x0))))))). t(i(i(n(i(x0,x1)),i(i(n(x2),x3),i(i(i(n(x4),i(i(n(x5),x6),n(x0))),i(x5,x4)),i(i(x7,i(i(x8,i(x7,x9)),i(i(n(x9),i(i(n(x10),x11),x8)),i(x10,x9)))),x1)))),i(x2,i(x0,x1)))). t(i(x0,i(i(n(i(i(n(x1),i(i(n(x2),x3),i(n(x1),i(i(n(x4),x5),n(x0))))),i(x2,x1))),i(i(n(x6),x7),x4)),i(x6,i(i(n(x1),i(i(n(x2),x3),i(n(x1),i(i(n(x4),x5),n(x0))))),i(x2,x1)))))). t(i(i(n(i(i(n(x0),i(i(n(x1),x2),i(n(x0),i(i(n(x3),x4),n(i(x5,i(i(x6,i(x5,x7)),i(i(n(x7),i(i(n(x8),x9),x6)),i(x8,x7))))))))),i(x1,x0))),i(i(n(x10),x11),x3)),i(x10,i(i(n(x0),i(i(n(x1),x2),i(n(x0),i(i(n(x3),x4),n(i(x5,i(i(x6,i(x5,x7)),i(i(n(x7),i(i(n(x8),x9),x6)),i(x8,x7))))))))),i(x1,x0))))). t(i(x0,i(i(n(x1),i(i(n(x2),x3),i(n(x1),i(i(n(i(i(n(x4),i(i(n(x5),x6),n(x0))),i(x5,x4))),x7),n(i(x8,i(i(x9,i(x8,x10)),i(i(n(x10),i(i(n(x11),x12),x9)),i(x11,x10))))))))),i(x2,x1)))). t(i(i(i(x0,i(i(x1,i(x0,x2)),i(i(n(x2),i(i(n(x3),x4),x1)),i(x3,x2)))),x5),i(x6,x5))). t(i(i(n(x0),i(i(n(x1),x2),i(i(x3,i(i(x4,i(x3,x5)),i(i(n(x5),i(i(n(x6),x7),x4)),i(x6,x5)))),x0))),i(x1,x0))). t(i(x0,x0)). t(i(i(x0,i(i(x1,i(i(x2,i(x1,x3)),i(i(n(x3),i(i(n(x4),x5),x2)),i(x4,x3)))),x6)),i(i(n(x6),i(i(n(x7),x8),x0)),i(x7,x6)))). t(i(i(x0,i(i(i(x1,i(i(x2,i(i(x3,i(x2,x4)),i(i(n(x4),i(i(n(x5),x6),x3)),i(x5,x4)))),x7)),i(i(n(x7),i(i(n(x8),x9),x1)),i(x8,x7))),x10)),i(i(n(x10),i(i(n(x11),x12),x0)),i(x11,x10)))). t(i(i(n(i(i(n(i(i(n(x0),i(i(n(x1),x2),x3)),i(x1,x0))),i(i(n(x4),x5),x6)),i(x4,i(i(n(x0),i(i(n(x1),x2),x3)),i(x1,x0))))),i(i(n(x7),x8),i(x3,i(x6,x0)))),i(x7,i(i(n(i(i(n(x0),i(i(n(x1),x2),x3)),i(x1,x0))),i(i(n(x4),x5),x6)),i(x4,i(i(n(x0),i(i(n(x1),x2),x3)),i(x1,x0))))))). t(i(i(n(i(i(n(i(x0,x1)),i(i(n(x2),x3),i(x4,i(i(x5,i(i(x6,i(x5,x7)),i(i(n(x7),i(i(n(x8),x9),x6)),i(x8,x7)))),x1)))),i(x2,i(x0,x1)))),i(i(n(x10),x11),i(n(x1),i(i(n(x0),x12),x4)))),i(x10,i(i(n(i(x0,x1)),i(i(n(x2),x3),i(x4,i(i(x5,i(i(x6,i(x5,x7)),i(i(n(x7),i(i(n(x8),x9),x6)),i(x8,x7)))),x1)))),i(x2,i(x0,x1)))))). t(i(x0,i(i(n(i(i(n(x1),i(i(n(x2),x3),i(n(x1),i(i(n(x4),x5),n(x0))))),i(x2,x1))),i(i(n(x6),x7),x4)),i(x6,i(i(n(x1),i(i(n(x2),x3),i(n(x1),i(i(n(x4),x5),n(x0))))),i(x2,x1)))))). t(i(i(n(i(i(n(x0),i(i(n(x1),x2),i(n(x0),i(i(n(x3),x4),n(i(x5,i(i(x6,i(x5,x7)),i(i(n(x7),i(i(n(x8),x9),x6)),i(x8,x7))))))))),i(x1,x0))),i(i(n(x10),x11),x3)),i(x10,i(i(n(x0),i(i(n(x1),x2),i(n(x0),i(i(n(x3),x4),n(i(x5,i(i(x6,i(x5,x7)),i(i(n(x7),i(i(n(x8),x9),x6)),i(x8,x7))))))))),i(x1,x0))))). t(i(i(n(i(i(n(i(x0,x1)),i(i(n(x2),x3),i(x4,i(i(x5,i(i(x6,i(x5,x7)),i(i(n(x7),i(i(n(x8),x9),x6)),i(x8,x7)))),x1)))),i(x2,i(x0,x1)))),i(i(n(x10),x11),i(n(i(i(n(i(x0,x1)),i(i(n(x2),x3),i(x4,i(i(x5,i(i(x6,i(x5,x7)),i(i(n(x7),i(i(n(x8),x9),x6)),i(x8,x7)))),x1)))),i(x2,i(x0,x1)))),i(i(n(i(x12,i(i(x13,i(x12,x14)),i(i(n(x14),i(i(n(x15),x16),x13)),i(x15,x14))))),x17),i(n(x1),i(i(n(x0),x18),x4)))))),i(x10,i(i(n(i(x0,x1)),i(i(n(x2),x3),i(x4,i(i(x5,i(i(x6,i(x5,x7)),i(i(n(x7),i(i(n(x8),x9),x6)),i(x8,x7)))),x1)))),i(x2,i(x0,x1)))))). t(i(x0,i(i(n(x1),i(i(n(x2),x3),i(n(x1),i(i(n(i(i(n(x4),i(i(n(x5),x6),n(x0))),i(x5,x4))),x7),n(i(x8,i(i(x9,i(x8,x10)),i(i(n(x10),i(i(n(x11),x12),x9)),i(x11,x10))))))))),i(x2,x1)))). t(i(i(i(n(i(x0,i(i(x1,i(x0,x2)),i(i(n(x2),i(i(n(x3),x4),x1)),i(x3,x2))))),x5),i(n(x6),i(i(n(x7),x8),x9))),i(i(n(i(x7,x6)),i(i(n(x10),x11),i(x9,i(i(x12,i(i(x13,i(x12,x14)),i(i(n(x14),i(i(n(x15),x16),x13)),i(x15,x14)))),x6)))),i(x10,i(x7,x6))))). t(i(i(x0,i(i(i(i(n(i(x1,i(i(x2,i(x1,x3)),i(i(n(x3),i(i(n(x4),x5),x2)),i(x4,x3))))),x6),i(n(x7),i(i(n(x8),x9),x10))),i(i(n(i(x8,x7)),i(i(n(x11),x12),i(x10,i(i(x13,i(i(x14,i(x13,x15)),i(i(n(x15),i(i(n(x16),x17),x14)),i(x16,x15)))),x7)))),i(x11,i(x8,x7)))),x18)),i(i(n(x18),i(i(n(x19),x20),x0)),i(x19,x18)))). t(i(i(n(i(i(n(i(x0,i(x1,x2))),i(i(n(x3),x4),i(i(n(i(x5,i(i(x6,i(x5,x7)),i(i(n(x7),i(i(n(x8),x9),x6)),i(x8,x7))))),x10),i(n(x2),i(i(n(x1),x11),x12))))),i(x3,i(x0,i(x1,x2))))),i(i(n(x13),x14),i(n(i(x1,x2)),i(i(n(x0),x15),i(x12,i(i(x16,i(i(x17,i(x16,x18)),i(i(n(x18),i(i(n(x19),x20),x17)),i(x19,x18)))),x2)))))),i(x13,i(i(n(i(x0,i(x1,x2))),i(i(n(x3),x4),i(i(n(i(x5,i(i(x6,i(x5,x7)),i(i(n(x7),i(i(n(x8),x9),x6)),i(x8,x7))))),x10),i(n(x2),i(i(n(x1),x11),x12))))),i(x3,i(x0,i(x1,x2))))))). t(i(i(i(n(x0),x1),i(x2,i(i(x3,i(i(x4,i(x3,x5)),i(i(n(x5),i(i(n(x6),x7),x4)),i(x6,x5)))),x8))),i(i(n(i(x0,i(x9,x8))),i(i(n(x10),x11),i(i(n(i(x12,i(i(x13,i(x12,x14)),i(i(n(x14),i(i(n(x15),x16),x13)),i(x15,x14))))),x17),i(n(x8),i(i(n(x9),x18),x2))))),i(x10,i(x0,i(x9,x8)))))). t(i(i(n(i(x0,i(x1,i(x2,x3)))),i(i(n(x4),x5),i(i(n(i(x6,i(i(x7,i(x6,x8)),i(i(n(x8),i(i(n(x9),x10),x7)),i(x9,x8))))),x11),i(n(i(x2,x3)),i(i(n(x1),x12),i(i(i(n(x13),i(i(n(x14),x15),n(x2))),i(x14,x13)),i(i(n(x0),x16),x3))))))),i(x4,i(x0,i(x1,i(x2,x3)))))). t(i(x0,i(x1,i(x2,i(x3,i(x4,x1)))))). t(i(x0,i(x1,i(x2,i(x3,x0))))). t(i(i(x0,i(i(x1,i(x2,i(x3,i(x4,x1)))),x5)),i(i(n(x5),i(i(n(x6),x7),x0)),i(x6,x5)))). t(i(i(n(i(x0,x1)),i(i(n(x2),x3),i(i(x4,i(x5,n(x1))),i(i(x6,i(i(x7,i(x6,x8)),i(i(n(x8),i(i(n(x9),x10),x7)),i(x9,x8)))),x1)))),i(x2,i(x0,x1)))). t(i(x0,i(x1,x0))). t(i(i(x0,i(i(x1,i(i(x2,i(x1,x3)),i(i(n(x3),i(i(n(x4),x5),x2)),i(x4,x3)))),x6)),i(i(n(x6),i(i(n(x7),x8),x0)),i(x7,x6)))). t(i(i(x0,i(i(i(x1,i(i(x2,i(i(x3,i(x2,x4)),i(i(n(x4),i(i(n(x5),x6),x3)),i(x5,x4)))),x7)),i(i(n(x7),i(i(n(x8),x9),x1)),i(x8,x7))),x10)),i(i(n(x10),i(i(n(x11),x12),x0)),i(x11,x10)))). t(i(i(n(i(i(n(i(i(n(x0),i(i(n(x1),x2),x3)),i(x1,x0))),i(i(n(x4),x5),x6)),i(x4,i(i(n(x0),i(i(n(x1),x2),x3)),i(x1,x0))))),i(i(n(x7),x8),i(x3,i(x6,x0)))),i(x7,i(i(n(i(i(n(x0),i(i(n(x1),x2),x3)),i(x1,x0))),i(i(n(x4),x5),x6)),i(x4,i(i(n(x0),i(i(n(x1),x2),x3)),i(x1,x0))))))). t(i(i(n(i(i(n(i(x0,x1)),i(i(n(x2),x3),i(x4,i(i(x5,i(i(x6,i(x5,x7)),i(i(n(x7),i(i(n(x8),x9),x6)),i(x8,x7)))),x1)))),i(x2,i(x0,x1)))),i(i(n(x10),x11),i(n(x1),i(i(n(x0),x12),x4)))),i(x10,i(i(n(i(x0,x1)),i(i(n(x2),x3),i(x4,i(i(x5,i(i(x6,i(x5,x7)),i(i(n(x7),i(i(n(x8),x9),x6)),i(x8,x7)))),x1)))),i(x2,i(x0,x1)))))). t(i(x0,i(i(n(i(i(n(x1),i(i(n(x2),x3),i(n(x1),i(i(n(x4),x5),n(x0))))),i(x2,x1))),i(i(n(x6),x7),x4)),i(x6,i(i(n(x1),i(i(n(x2),x3),i(n(x1),i(i(n(x4),x5),n(x0))))),i(x2,x1)))))). t(i(i(n(i(i(n(x0),i(i(n(x1),x2),i(n(x0),i(i(n(x3),x4),n(i(x5,i(i(x6,i(x5,x7)),i(i(n(x7),i(i(n(x8),x9),x6)),i(x8,x7))))))))),i(x1,x0))),i(i(n(x10),x11),x3)),i(x10,i(i(n(x0),i(i(n(x1),x2),i(n(x0),i(i(n(x3),x4),n(i(x5,i(i(x6,i(x5,x7)),i(i(n(x7),i(i(n(x8),x9),x6)),i(x8,x7))))))))),i(x1,x0))))). t(i(x0,i(i(n(x1),i(i(n(x2),x3),i(n(x1),i(i(n(i(i(n(x4),i(i(n(x5),x6),n(x0))),i(x5,x4))),x7),n(i(x8,i(i(x9,i(x8,x10)),i(i(n(x10),i(i(n(x11),x12),x9)),i(x11,x10))))))))),i(x2,x1)))). t(i(i(i(n(x0),x1),x2),i(i(n(i(x0,x3)),i(i(n(x4),x5),i(x2,i(i(x6,i(i(x7,i(x6,x8)),i(i(n(x8),i(i(n(x9),x10),x7)),i(x9,x8)))),x3)))),i(x4,i(x0,x3))))). t(i(i(n(i(x0,i(x1,x2))),i(i(n(x3),x4),i(i(n(x1),x5),i(n(x2),i(i(n(i(x6,i(i(x7,i(x6,x8)),i(i(n(x8),i(i(n(x9),x10),x7)),i(x9,x8))))),x11),n(x0)))))),i(x3,i(x0,i(x1,x2))))). t(i(i(n(x0),i(i(n(i(x1,i(i(x2,i(x1,x3)),i(i(n(x3),i(i(n(x4),x5),x2)),i(x4,x3))))),x6),n(x7))),i(x7,i(x8,x0)))). t(i(i(n(i(x0,x1)),i(i(n(x2),x3),i(i(x4,i(x5,x0)),i(i(x6,i(i(x7,i(x6,x8)),i(i(n(x8),i(i(n(x9),x10),x7)),i(x9,x8)))),x1)))),i(x2,i(x0,x1)))). t(i(x0,i(n(x0),x1))). t(i(i(x0,i(i(x1,i(i(x2,i(x1,x3)),i(i(n(x3),i(i(n(x4),x5),x2)),i(x4,x3)))),x6)),i(i(n(x6),i(i(n(x7),x8),x0)),i(x7,x6)))). t(i(i(x0,i(i(i(x1,i(i(x2,i(i(x3,i(x2,x4)),i(i(n(x4),i(i(n(x5),x6),x3)),i(x5,x4)))),x7)),i(i(n(x7),i(i(n(x8),x9),x1)),i(x8,x7))),x10)),i(i(n(x10),i(i(n(x11),x12),x0)),i(x11,x10)))). t(i(i(n(i(i(n(i(i(n(x0),i(i(n(x1),x2),x3)),i(x1,x0))),i(i(n(x4),x5),x6)),i(x4,i(i(n(x0),i(i(n(x1),x2),x3)),i(x1,x0))))),i(i(n(x7),x8),i(x3,i(x6,x0)))),i(x7,i(i(n(i(i(n(x0),i(i(n(x1),x2),x3)),i(x1,x0))),i(i(n(x4),x5),x6)),i(x4,i(i(n(x0),i(i(n(x1),x2),x3)),i(x1,x0))))))). t(i(i(n(i(x0,x1)),i(i(n(x2),x3),i(i(i(n(x4),i(i(n(x5),x6),n(x0))),i(x5,x4)),i(i(x7,i(i(x8,i(x7,x9)),i(i(n(x9),i(i(n(x10),x11),x8)),i(x10,x9)))),x1)))),i(x2,i(x0,x1)))). t(i(i(n(i(i(n(i(x0,x1)),i(i(n(x2),x3),i(x4,i(i(x5,i(i(x6,i(x5,x7)),i(i(n(x7),i(i(n(x8),x9),x6)),i(x8,x7)))),x1)))),i(x2,i(x0,x1)))),i(i(n(x10),x11),i(n(x1),i(i(n(x0),x12),x4)))),i(x10,i(i(n(i(x0,x1)),i(i(n(x2),x3),i(x4,i(i(x5,i(i(x6,i(x5,x7)),i(i(n(x7),i(i(n(x8),x9),x6)),i(x8,x7)))),x1)))),i(x2,i(x0,x1)))))). t(i(x0,i(i(n(i(i(n(x1),i(i(n(x2),x3),i(n(x1),i(i(n(x4),x5),n(x0))))),i(x2,x1))),i(i(n(x6),x7),x4)),i(x6,i(i(n(x1),i(i(n(x2),x3),i(n(x1),i(i(n(x4),x5),n(x0))))),i(x2,x1)))))). t(i(i(x0,i(i(i(n(i(i(n(i(x1,x2)),i(i(n(x3),x4),i(x5,i(i(x6,i(i(x7,i(x6,x8)),i(i(n(x8),i(i(n(x9),x10),x7)),i(x9,x8)))),x2)))),i(x3,i(x1,x2)))),i(i(n(x11),x12),i(n(x2),i(i(n(x1),x13),x5)))),i(x11,i(i(n(i(x1,x2)),i(i(n(x3),x4),i(x5,i(i(x6,i(i(x7,i(x6,x8)),i(i(n(x8),i(i(n(x9),x10),x7)),i(x9,x8)))),x2)))),i(x3,i(x1,x2))))),x14)),i(i(n(x14),i(i(n(x15),x16),x0)),i(x15,x14)))). t(i(i(n(i(i(n(x0),i(i(n(x1),x2),i(n(x0),i(i(n(x3),x4),n(i(x5,i(i(x6,i(x5,x7)),i(i(n(x7),i(i(n(x8),x9),x6)),i(x8,x7))))))))),i(x1,x0))),i(i(n(x10),x11),x3)),i(x10,i(i(n(x0),i(i(n(x1),x2),i(n(x0),i(i(n(x3),x4),n(i(x5,i(i(x6,i(x5,x7)),i(i(n(x7),i(i(n(x8),x9),x6)),i(x8,x7))))))))),i(x1,x0))))). t(i(i(n(i(i(n(i(x0,x1)),i(i(n(x2),x3),i(x4,i(i(x5,i(i(x6,i(x5,x7)),i(i(n(x7),i(i(n(x8),x9),x6)),i(x8,x7)))),x1)))),i(x2,i(x0,x1)))),i(i(n(x10),x11),i(n(i(i(n(i(x0,x1)),i(i(n(x2),x3),i(x4,i(i(x5,i(i(x6,i(x5,x7)),i(i(n(x7),i(i(n(x8),x9),x6)),i(x8,x7)))),x1)))),i(x2,i(x0,x1)))),i(i(n(i(x12,i(i(x13,i(x12,x14)),i(i(n(x14),i(i(n(x15),x16),x13)),i(x15,x14))))),x17),i(n(x1),i(i(n(x0),x18),x4)))))),i(x10,i(i(n(i(x0,x1)),i(i(n(x2),x3),i(x4,i(i(x5,i(i(x6,i(x5,x7)),i(i(n(x7),i(i(n(x8),x9),x6)),i(x8,x7)))),x1)))),i(x2,i(x0,x1)))))). t(i(i(n(i(x0,i(i(n(x1),i(i(n(x2),x3),i(n(x1),i(i(n(i(i(n(x4),i(i(n(x5),x6),n(x0))),i(x5,x4))),x7),n(x8))))),i(x2,x1)))),i(i(n(x9),x10),x8)),i(x9,i(x0,i(i(n(x1),i(i(n(x2),x3),i(n(x1),i(i(n(i(i(n(x4),i(i(n(x5),x6),n(x0))),i(x5,x4))),x7),n(x8))))),i(x2,x1)))))). t(i(i(n(i(i(n(i(i(n(i(x0,x1)),i(i(n(x2),x3),i(x4,i(i(x5,i(i(x6,i(x5,x7)),i(i(n(x7),i(i(n(x8),x9),x6)),i(x8,x7)))),x1)))),i(x2,i(x0,x1)))),i(i(n(x10),x11),i(n(i(i(n(i(x0,x1)),i(i(n(x2),x3),i(x4,i(i(x5,i(i(x6,i(x5,x7)),i(i(n(x7),i(i(n(x8),x9),x6)),i(x8,x7)))),x1)))),i(x2,i(x0,x1)))),i(i(n(x12),x13),i(n(x1),i(i(n(x0),x14),x4)))))),i(x10,i(i(n(i(x0,x1)),i(i(n(x2),x3),i(x4,i(i(x5,i(i(x6,i(x5,x7)),i(i(n(x7),i(i(n(x8),x9),x6)),i(x8,x7)))),x1)))),i(x2,i(x0,x1)))))),i(i(n(x15),x16),x12)),i(x15,i(i(n(i(i(n(i(x0,x1)),i(i(n(x2),x3),i(x4,i(i(x5,i(i(x6,i(x5,x7)),i(i(n(x7),i(i(n(x8),x9),x6)),i(x8,x7)))),x1)))),i(x2,i(x0,x1)))),i(i(n(x10),x11),i(n(i(i(n(i(x0,x1)),i(i(n(x2),x3),i(x4,i(i(x5,i(i(x6,i(x5,x7)),i(i(n(x7),i(i(n(x8),x9),x6)),i(x8,x7)))),x1)))),i(x2,i(x0,x1)))),i(i(n(x12),x13),i(n(x1),i(i(n(x0),x14),x4)))))),i(x10,i(i(n(i(x0,x1)),i(i(n(x2),x3),i(x4,i(i(x5,i(i(x6,i(x5,x7)),i(i(n(x7),i(i(n(x8),x9),x6)),i(x8,x7)))),x1)))),i(x2,i(x0,x1)))))))). t(i(x0,i(i(n(x1),i(i(n(x2),x3),i(n(x1),i(i(n(i(i(n(x4),i(i(n(x5),x6),n(x0))),i(x5,x4))),x7),n(i(x8,i(i(x9,i(x8,x10)),i(i(n(x10),i(i(n(x11),x12),x9)),i(x11,x10))))))))),i(x2,x1)))). t(i(i(x0,i(i(x1,i(i(n(x2),i(i(n(x3),x4),i(n(x2),i(i(n(i(i(n(x5),i(i(n(x6),x7),n(x1))),i(x6,x5))),x8),n(i(x9,i(i(x10,i(x9,x11)),i(i(n(x11),i(i(n(x12),x13),x10)),i(x12,x11))))))))),i(x3,x2))),x14)),i(i(n(x14),i(i(n(x15),x16),x0)),i(x15,x14)))). t(i(x0,i(i(n(i(i(n(i(x1,x2)),i(i(n(x3),x4),i(x5,i(i(x6,i(i(x7,i(x6,x8)),i(i(n(x8),i(i(n(x9),x10),x7)),i(x9,x8)))),x2)))),i(x3,i(x1,x2)))),i(i(n(x11),x12),i(n(i(i(n(i(x1,x2)),i(i(n(x3),x4),i(x5,i(i(x6,i(i(x7,i(x6,x8)),i(i(n(x8),i(i(n(x9),x10),x7)),i(x9,x8)))),x2)))),i(x3,i(x1,x2)))),i(i(n(i(i(n(x13),i(i(n(x14),x15),n(x0))),i(x14,x13))),x16),i(n(x2),i(i(n(x1),x17),x5)))))),i(x11,i(i(n(i(x1,x2)),i(i(n(x3),x4),i(x5,i(i(x6,i(i(x7,i(x6,x8)),i(i(n(x8),i(i(n(x9),x10),x7)),i(x9,x8)))),x2)))),i(x3,i(x1,x2))))))). t(i(i(x0,i(i(x1,i(i(n(i(i(n(i(x2,x3)),i(i(n(x4),x5),i(x6,i(i(x7,i(i(x8,i(x7,x9)),i(i(n(x9),i(i(n(x10),x11),x8)),i(x10,x9)))),x3)))),i(x4,i(x2,x3)))),i(i(n(x12),x13),i(n(i(i(n(i(x2,x3)),i(i(n(x4),x5),i(x6,i(i(x7,i(i(x8,i(x7,x9)),i(i(n(x9),i(i(n(x10),x11),x8)),i(x10,x9)))),x3)))),i(x4,i(x2,x3)))),i(i(n(i(i(n(x14),i(i(n(x15),x16),n(x1))),i(x15,x14))),x17),i(n(x3),i(i(n(x2),x18),x6)))))),i(x12,i(i(n(i(x2,x3)),i(i(n(x4),x5),i(x6,i(i(x7,i(i(x8,i(x7,x9)),i(i(n(x9),i(i(n(x10),x11),x8)),i(x10,x9)))),x3)))),i(x4,i(x2,x3)))))),x19)),i(i(n(x19),i(i(n(x20),x21),x0)),i(x20,x19)))). t(i(i(n(i(x0,x1)),i(i(n(x2),x3),i(i(i(n(x4),i(i(n(x5),x6),n(x0))),i(x5,x4)),i(i(x7,i(i(n(x8),i(i(n(x9),x10),i(n(x8),i(i(n(i(i(n(x11),i(i(n(x12),x13),n(x7))),i(x12,x11))),x14),n(i(x15,i(i(x16,i(x15,x17)),i(i(n(x17),i(i(n(x18),x19),x16)),i(x18,x17))))))))),i(x9,x8))),x1)))),i(x2,i(x0,x1)))). t(i(i(n(i(i(n(i(x0,i(i(n(i(x1,x2)),i(i(n(x3),x4),i(x5,i(i(x6,i(i(x7,i(x6,x8)),i(i(n(x8),i(i(n(x9),x10),x7)),i(x9,x8)))),x2)))),i(x3,i(x1,x2))))),i(i(n(x11),x12),x13)),i(x11,i(x0,i(i(n(i(x1,x2)),i(i(n(x3),x4),i(x5,i(i(x6,i(i(x7,i(x6,x8)),i(i(n(x8),i(i(n(x9),x10),x7)),i(x9,x8)))),x2)))),i(x3,i(x1,x2))))))),i(i(n(x14),x15),i(n(i(i(n(i(x1,x2)),i(i(n(x3),x4),i(x5,i(i(x6,i(i(x7,i(x6,x8)),i(i(n(x8),i(i(n(x9),x10),x7)),i(x9,x8)))),x2)))),i(x3,i(x1,x2)))),i(i(n(x0),x16),i(n(i(i(n(i(x1,x2)),i(i(n(x3),x4),i(x5,i(i(x6,i(i(x7,i(x6,x8)),i(i(n(x8),i(i(n(x9),x10),x7)),i(x9,x8)))),x2)))),i(x3,i(x1,x2)))),i(i(n(i(i(n(x17),i(i(n(x18),x19),n(x13))),i(x18,x17))),x20),i(n(x2),i(i(n(x1),x21),x5)))))))),i(x14,i(i(n(i(x0,i(i(n(i(x1,x2)),i(i(n(x3),x4),i(x5,i(i(x6,i(i(x7,i(x6,x8)),i(i(n(x8),i(i(n(x9),x10),x7)),i(x9,x8)))),x2)))),i(x3,i(x1,x2))))),i(i(n(x11),x12),x13)),i(x11,i(x0,i(i(n(i(x1,x2)),i(i(n(x3),x4),i(x5,i(i(x6,i(i(x7,i(x6,x8)),i(i(n(x8),i(i(n(x9),x10),x7)),i(x9,x8)))),x2)))),i(x3,i(x1,x2))))))))). t(i(i(n(i(x0,x1)),i(i(n(x2),x3),i(i(x4,x0),i(i(x5,i(i(x6,i(x5,x7)),i(i(n(x7),i(i(n(x8),x9),x6)),i(x8,x7)))),x1)))),i(x2,i(x0,x1)))). t(i(i(i(x0,i(i(x1,i(x0,x2)),i(i(n(x2),i(i(n(x3),x4),x1)),i(x3,x2)))),x5),i(x6,x5))). t(i(i(i(n(x0),x1),x2),i(i(n(i(x0,x3)),i(i(n(x4),x5),i(x2,i(i(x6,i(i(x7,i(x6,x8)),i(i(n(x8),i(i(n(x9),x10),x7)),i(x9,x8)))),x3)))),i(x4,i(x0,x3))))). t(i(x0,i(i(i(n(i(x1,i(i(x2,i(x1,x3)),i(i(n(x3),i(i(n(x4),x5),x2)),i(x4,x3))))),x6),n(x0)),x7))). t(i(i(x0,i(i(i(i(x1,i(i(x2,i(x1,x3)),i(i(n(x3),i(i(n(x4),x5),x2)),i(x4,x3)))),x6),i(x7,x6)),x8)),i(i(n(x8),i(i(n(x9),x10),x0)),i(x9,x8)))). t(i(i(x0,i(i(x1,i(i(i(n(i(x2,i(i(x3,i(x2,x4)),i(i(n(x4),i(i(n(x5),x6),x3)),i(x5,x4))))),x7),n(x1)),x8)),x9)),i(i(n(x9),i(i(n(x10),x11),x0)),i(x10,x9)))). t(i(x0,i(i(n(x1),i(i(n(x2),x3),i(n(x1),i(i(n(i(x4,x0)),x5),n(i(x6,i(i(x7,i(x6,x8)),i(i(n(x8),i(i(n(x9),x10),x7)),i(x9,x8))))))))),i(x2,x1)))). t(i(i(n(x0),i(i(n(x1),x2),i(i(x3,i(i(x4,i(x3,x5)),i(i(n(x5),i(i(n(x6),x7),x4)),i(x6,x5)))),x0))),i(x1,x0))). t(i(i(n(i(x0,i(x1,x2))),i(i(n(x3),x4),i(i(n(x1),x5),i(n(x2),i(i(n(i(x6,i(i(x7,i(x6,x8)),i(i(n(x8),i(i(n(x9),x10),x7)),i(x9,x8))))),x11),n(x0)))))),i(x3,i(x0,i(x1,x2))))). t(i(i(n(i(i(n(x0),i(i(n(x1),x2),i(i(x3,i(i(x4,i(x3,x5)),i(i(n(x5),i(i(n(x6),x7),x4)),i(x6,x5)))),x0))),i(x1,x0))),i(i(n(x8),x9),x10)),i(x8,i(i(n(x0),i(i(n(x1),x2),i(i(x3,i(i(x4,i(x3,x5)),i(i(n(x5),i(i(n(x6),x7),x4)),i(x6,x5)))),x0))),i(x1,x0))))). t(i(i(n(i(i(n(x0),i(i(n(x1),x2),x3)),i(x1,x0))),i(i(n(x4),x5),i(i(n(i(x6,i(i(x7,i(x6,x8)),i(i(n(x8),i(i(n(x9),x10),x7)),i(x9,x8))))),x11),n(x3)))),i(x4,i(i(n(x0),i(i(n(x1),x2),x3)),i(x1,x0))))). t(i(i(i(n(i(x0,i(i(x1,i(x0,x2)),i(i(n(x2),i(i(n(x3),x4),x1)),i(x3,x2))))),x5),i(n(x6),i(i(n(x7),x8),x9))),i(i(n(i(x7,x6)),i(i(n(x10),x11),i(x9,i(i(x12,i(i(x13,i(x12,x14)),i(i(n(x14),i(i(n(x15),x16),x13)),i(x15,x14)))),x6)))),i(x10,i(x7,x6))))). t(i(i(x0,i(i(i(n(i(i(n(x1),i(i(n(x2),x3),x4)),i(x2,x1))),i(i(n(x5),x6),i(i(n(i(x7,i(i(x8,i(x7,x9)),i(i(n(x9),i(i(n(x10),x11),x8)),i(x10,x9))))),x12),n(x4)))),i(x5,i(i(n(x1),i(i(n(x2),x3),x4)),i(x2,x1)))),x13)),i(i(n(x13),i(i(n(x14),x15),x0)),i(x14,x13)))). t(i(i(x0,i(i(i(i(n(i(x1,i(i(x2,i(x1,x3)),i(i(n(x3),i(i(n(x4),x5),x2)),i(x4,x3))))),x6),i(n(x7),i(i(n(x8),x9),x10))),i(i(n(i(x8,x7)),i(i(n(x11),x12),i(x10,i(i(x13,i(i(x14,i(x13,x15)),i(i(n(x15),i(i(n(x16),x17),x14)),i(x16,x15)))),x7)))),i(x11,i(x8,x7)))),x18)),i(i(n(x18),i(i(n(x19),x20),x0)),i(x19,x18)))). t(i(x0,i(x1,i(i(i(n(i(x2,i(i(x3,i(x2,x4)),i(i(n(x4),i(i(n(x5),x6),x3)),i(x5,x4))))),x7),n(x1)),x8)))). t(i(x0,i(i(n(x1),i(i(n(x2),x3),i(i(x4,i(i(x5,i(x4,x6)),i(i(n(x6),i(i(n(x7),x8),x5)),i(x7,x6)))),x1))),i(x2,x1)))). t(i(i(x0,i(i(x1,i(x2,i(i(i(n(i(x3,i(i(x4,i(x3,x5)),i(i(n(x5),i(i(n(x6),x7),x4)),i(x6,x5))))),x8),n(x2)),x9))),x10)),i(i(n(x10),i(i(n(x11),x12),x0)),i(x11,x10)))). t(i(i(x0,i(i(x1,i(i(n(x2),i(i(n(x3),x4),i(i(x5,i(i(x6,i(x5,x7)),i(i(n(x7),i(i(n(x8),x9),x6)),i(x8,x7)))),x2))),i(x3,x2))),x10)),i(i(n(x10),i(i(n(x11),x12),x0)),i(x11,x10)))). t(i(i(n(i(x0,i(x1,x2))),i(i(n(x3),x4),i(n(i(x0,i(x1,x2))),i(i(n(i(x5,i(i(x6,i(x5,x7)),i(i(n(x7),i(i(n(x8),x9),x6)),i(x8,x7))))),x10),i(i(n(x1),x11),i(n(x2),i(i(n(i(x12,i(i(x13,i(x12,x14)),i(i(n(x14),i(i(n(x15),x16),x13)),i(x15,x14))))),x17),n(x0)))))))),i(x3,i(x0,i(x1,x2))))). t(i(i(n(i(i(n(i(x0,i(x1,x2))),i(i(n(x3),x4),i(i(n(i(x5,i(i(x6,i(x5,x7)),i(i(n(x7),i(i(n(x8),x9),x6)),i(x8,x7))))),x10),i(n(x2),i(i(n(x1),x11),x12))))),i(x3,i(x0,i(x1,x2))))),i(i(n(x13),x14),i(n(i(x1,x2)),i(i(n(x0),x15),i(x12,i(i(x16,i(i(x17,i(x16,x18)),i(i(n(x18),i(i(n(x19),x20),x17)),i(x19,x18)))),x2)))))),i(x13,i(i(n(i(x0,i(x1,x2))),i(i(n(x3),x4),i(i(n(i(x5,i(i(x6,i(x5,x7)),i(i(n(x7),i(i(n(x8),x9),x6)),i(x8,x7))))),x10),i(n(x2),i(i(n(x1),x11),x12))))),i(x3,i(x0,i(x1,x2))))))). t(i(i(n(i(x0,x1)),i(i(n(x2),x3),i(i(i(n(x4),i(i(n(x5),x6),n(x0))),i(x5,x4)),i(i(i(n(i(i(n(x7),i(i(n(x8),x9),x10)),i(x8,x7))),i(i(n(x11),x12),i(i(n(i(x13,i(i(x14,i(x13,x15)),i(i(n(x15),i(i(n(x16),x17),x14)),i(x16,x15))))),x18),n(x10)))),i(x11,i(i(n(x7),i(i(n(x8),x9),x10)),i(x8,x7)))),x1)))),i(x2,i(x0,x1)))). t(i(i(n(i(i(n(i(x0,x1)),i(i(n(x2),x3),x4)),i(x2,i(x0,x1)))),i(i(n(x5),x6),i(n(x1),i(i(n(x0),x7),i(i(x8,i(i(x9,i(x8,x10)),i(i(n(x10),i(i(n(x11),x12),x9)),i(x11,x10)))),x1))))),i(x5,i(i(n(i(x0,x1)),i(i(n(x2),x3),x4)),i(x2,i(x0,x1)))))). t(i(i(i(x0,i(i(n(x1),i(i(n(x2),x3),i(n(x1),i(i(n(i(i(n(x4),i(i(n(x5),x6),n(x0))),i(x5,x4))),x7),n(i(x8,i(i(x9,i(x8,x10)),i(i(n(x10),i(i(n(x11),x12),x9)),i(x11,x10))))))))),i(x2,x1))),x13),i(x14,x13))). t(i(i(i(n(x0),x1),i(n(i(i(n(i(x2,x3)),i(i(n(x4),x5),i(x6,i(i(x7,i(i(x8,i(x7,x9)),i(i(n(x9),i(i(n(x10),x11),x8)),i(x10,x9)))),x3)))),i(x4,i(x2,x3)))),i(i(n(i(i(n(x12),i(i(n(x13),x14),n(x15))),i(x13,x12))),x16),i(n(x3),i(i(n(x2),x17),x6))))),i(i(n(i(x0,i(i(n(i(x2,x3)),i(i(n(x4),x5),i(x6,i(i(x7,i(i(x8,i(x7,x9)),i(i(n(x9),i(i(n(x10),x11),x8)),i(x10,x9)))),x3)))),i(x4,i(x2,x3))))),i(i(n(x18),x19),x15)),i(x18,i(x0,i(i(n(i(x2,x3)),i(i(n(x4),x5),i(x6,i(i(x7,i(i(x8,i(x7,x9)),i(i(n(x9),i(i(n(x10),x11),x8)),i(x10,x9)))),x3)))),i(x4,i(x2,x3)))))))). t(i(i(n(i(x0,x1)),i(i(n(x2),x3),i(i(i(n(x4),i(i(n(x5),x6),n(x0))),i(x5,x4)),i(i(x7,i(x8,i(i(i(n(i(x9,i(i(x10,i(x9,x11)),i(i(n(x11),i(i(n(x12),x13),x10)),i(x12,x11))))),x14),n(x8)),x15))),x1)))),i(x2,i(x0,x1)))). t(i(i(n(i(x0,i(x1,i(i(n(i(x2,x3)),i(i(n(x4),x5),i(x6,i(i(x7,i(i(x8,i(x7,x9)),i(i(n(x9),i(i(n(x10),x11),x8)),i(x10,x9)))),x3)))),i(x4,i(x2,x3)))))),i(i(n(x12),x13),i(i(n(x1),x14),i(n(i(i(n(i(x2,x3)),i(i(n(x4),x5),i(x6,i(i(x7,i(i(x8,i(x7,x9)),i(i(n(x9),i(i(n(x10),x11),x8)),i(x10,x9)))),x3)))),i(x4,i(x2,x3)))),i(i(n(i(i(n(x15),i(i(n(x16),x17),n(i(i(n(x18),i(i(n(x19),x20),n(x0))),i(x19,x18))))),i(x16,x15))),x21),i(n(x3),i(i(n(x2),x22),x6))))))),i(x12,i(x0,i(x1,i(i(n(i(x2,x3)),i(i(n(x4),x5),i(x6,i(i(x7,i(i(x8,i(x7,x9)),i(i(n(x9),i(i(n(x10),x11),x8)),i(x10,x9)))),x3)))),i(x4,i(x2,x3)))))))). t(i(x0,x0)). t(i(i(n(x0),i(i(n(i(x1,i(i(x2,i(x1,x3)),i(i(n(x3),i(i(n(x4),x5),x2)),i(x4,x3))))),x6),n(x7))),i(x7,i(x8,x0)))). t(i(x0,i(x1,i(i(i(n(i(i(n(x2),i(i(n(x3),x4),n(i(i(n(x5),i(i(n(x6),x7),n(x1))),i(x6,x5))))),i(x3,x2))),x8),i(n(x9),i(i(n(x10),x11),x12))),i(i(n(i(x10,x9)),i(i(n(x13),x14),i(x12,i(i(x15,i(i(x16,i(x15,x17)),i(i(n(x17),i(i(n(x18),x19),x16)),i(x18,x17)))),x9)))),i(x13,i(x10,x9))))))). t(i(n(x0),i(i(n(x1),i(i(n(x2),x3),x0)),i(x2,x1)))). t(i(i(x0,i(i(x1,x1),x2)),i(i(n(x2),i(i(n(x3),x4),x0)),i(x3,x2)))). t(i(i(x0,i(i(n(x1),i(i(n(x2),i(i(n(x3),x4),x1)),i(x3,x2))),x5)),i(i(n(x5),i(i(n(x6),x7),x0)),i(x6,x5)))). t(i(i(n(i(i(n(x0),i(i(n(x1),x2),i(x3,x0))),i(x1,x0))),i(i(n(x4),x5),x3)),i(x4,i(i(n(x0),i(i(n(x1),x2),i(x3,x0))),i(x1,x0))))). t(i(i(n(i(i(n(i(x0,x1)),i(i(n(x2),x3),n(x4))),i(x2,i(x0,x1)))),i(i(n(x5),x6),i(n(x1),i(i(n(x0),x7),x4)))),i(x5,i(i(n(i(x0,x1)),i(i(n(x2),x3),n(x4))),i(x2,i(x0,x1)))))). t(i(i(i(n(x0),x1),i(x2,i(i(x3,i(i(x4,i(x3,x5)),i(i(n(x5),i(i(n(x6),x7),x4)),i(x6,x5)))),x8))),i(i(n(i(x0,i(x9,x8))),i(i(n(x10),x11),i(i(n(i(x12,i(i(x13,i(x12,x14)),i(i(n(x14),i(i(n(x15),x16),x13)),i(x15,x14))))),x17),i(n(x8),i(i(n(x9),x18),x2))))),i(x10,i(x0,i(x9,x8)))))). t(i(i(i(i(n(i(i(n(x0),i(i(n(x1),x2),x3)),i(x1,x0))),i(i(n(x4),x5),i(i(n(i(x6,i(i(x7,i(x6,x8)),i(i(n(x8),i(i(n(x9),x10),x7)),i(x9,x8))))),x11),n(x3)))),i(x4,i(i(n(x0),i(i(n(x1),x2),x3)),i(x1,x0)))),x12),i(x13,x12))). t(i(i(i(n(x0),x1),i(i(x2,i(i(x3,i(x2,x4)),i(i(n(x4),i(i(n(x5),x6),x3)),i(x5,x4)))),x7)),i(i(n(i(x0,x7)),i(i(n(x8),x9),x10)),i(x8,i(x0,x7))))). t(i(i(n(i(x0,i(x1,i(x2,x3)))),i(i(n(x4),x5),i(i(n(i(x6,i(i(x7,i(x6,x8)),i(i(n(x8),i(i(n(x9),x10),x7)),i(x9,x8))))),x11),i(n(i(x2,x3)),i(i(n(x1),x12),i(i(i(n(x13),i(i(n(x14),x15),n(x2))),i(x14,x13)),i(i(n(x0),x16),x3))))))),i(x4,i(x0,i(x1,i(x2,x3)))))). t(i(x0,i(x1,i(x2,i(x3,i(x4,x1)))))). t(i(i(n(i(x0,i(x1,x2))),i(i(n(x3),x4),i(i(n(x1),x5),i(i(x6,i(i(x7,i(x6,x8)),i(i(n(x8),i(i(n(x9),x10),x7)),i(x9,x8)))),x2)))),i(x3,i(x0,i(x1,x2))))). t(i(x0,i(x1,i(x2,i(x3,x0))))). t(i(i(x0,i(i(x1,i(x2,i(x3,i(x4,x1)))),x5)),i(i(n(x5),i(i(n(x6),x7),x0)),i(x6,x5)))). t(i(x0,i(x1,i(x2,x2)))). t(i(i(x0,i(i(i(x1,i(i(x2,i(x3,i(x4,i(x5,x2)))),x6)),i(i(n(x6),i(i(n(x7),x8),x1)),i(x7,x6))),x9)),i(i(n(x9),i(i(n(x10),x11),x0)),i(x10,x9)))). t(i(i(n(i(i(n(i(x0,x1)),i(i(n(x2),x3),i(x4,i(i(x5,i(x6,i(x7,i(x8,x5)))),x1)))),i(x2,i(x0,x1)))),i(i(n(x9),x10),i(n(x1),i(i(n(x0),x11),x4)))),i(x9,i(i(n(i(x0,x1)),i(i(n(x2),x3),i(x4,i(i(x5,i(x6,i(x7,i(x8,x5)))),x1)))),i(x2,i(x0,x1)))))). t(i(i(n(i(x0,x1)),i(i(n(x2),x3),i(i(x4,i(x5,n(x1))),i(i(x6,i(i(x7,i(x6,x8)),i(i(n(x8),i(i(n(x9),x10),x7)),i(x9,x8)))),x1)))),i(x2,i(x0,x1)))). t(i(i(i(n(x0),x1),x2),i(i(n(i(x0,x3)),i(i(n(x4),x5),n(x2))),i(x4,i(x0,x3))))). t(i(i(x0,i(i(i(i(n(x1),x2),x3),i(i(n(i(x1,x4)),i(i(n(x5),x6),n(x3))),i(x5,i(x1,x4)))),x7)),i(i(n(x7),i(i(n(x8),x9),x0)),i(x8,x7)))). t(i(x0,i(x1,x0))). t(i(i(x0,i(i(x1,i(x2,x1)),x3)),i(i(n(x3),i(i(n(x4),x5),x0)),i(x4,x3)))). t(i(i(n(i(i(n(i(x0,i(x1,x2))),i(i(n(x3),x4),i(i(n(x1),x5),x6))),i(x3,i(x0,i(x1,x2))))),i(i(n(x7),x8),i(n(i(x1,x2)),i(i(n(x0),x9),n(x6))))),i(x7,i(i(n(i(x0,i(x1,x2))),i(i(n(x3),x4),i(i(n(x1),x5),x6))),i(x3,i(x0,i(x1,x2))))))). t(i(i(n(i(x0,x1)),i(i(n(x2),x3),i(i(x4,i(x5,x0)),i(i(x6,i(i(x7,i(x6,x8)),i(i(n(x8),i(i(n(x9),x10),x7)),i(x9,x8)))),x1)))),i(x2,i(x0,x1)))). t(i(i(n(i(i(n(x0),i(i(n(x1),x2),x0)),i(x1,x0))),i(i(n(x3),x4),x5)),i(x3,i(i(n(x0),i(i(n(x1),x2),x0)),i(x1,x0))))). t(i(x0,i(x1,i(i(n(x2),i(i(n(x3),x4),i(n(x2),i(i(n(i(i(n(x5),i(i(n(x6),x7),n(x1))),i(x6,x5))),x8),n(i(x9,x9)))))),i(x3,x2))))). t(i(i(i(n(x0),x1),x2),i(i(n(i(x0,x3)),i(i(n(x4),x5),i(x2,i(i(x6,i(x7,i(x8,i(x9,x6)))),x3)))),i(x4,i(x0,x3))))). t(i(x0,i(x1,i(x2,i(n(i(n(x2),x3)),x4))))). t(i(i(i(n(x0),x1),n(x2)),i(i(n(i(x0,i(x3,x4))),i(i(n(x5),x6),i(i(n(x3),x7),x2))),i(x5,i(x0,i(x3,x4)))))). t(i(i(x0,i(i(x1,i(x2,i(x3,i(n(i(n(x3),x4)),x5)))),x6)),i(i(n(x6),i(i(n(x7),x8),x0)),i(x7,x6)))). t(i(x0,i(x1,i(x2,x0)))). t(i(x0,i(x1,i(n(x2),i(i(n(x3),i(i(n(x4),x5),x2)),i(x4,x3)))))). t(i(i(x0,i(i(x1,i(x2,i(x3,x1))),x4)),i(i(n(x4),i(i(n(x5),x6),x0)),i(x5,x4)))). t(i(i(x0,i(i(x1,i(x2,i(n(x3),i(i(n(x4),i(i(n(x5),x6),x3)),i(x5,x4))))),x7)),i(i(n(x7),i(i(n(x8),x9),x0)),i(x8,x7)))). t(i(i(n(i(x0,x1)),i(i(n(x2),x3),x1)),i(x2,i(x0,x1)))). t(i(i(n(i(x0,x1)),i(i(n(x2),x3),i(i(x4,n(x1)),i(i(x5,i(i(x6,i(x5,x7)),i(i(n(x7),i(i(n(x8),x9),x6)),i(x8,x7)))),x1)))),i(x2,i(x0,x1)))). t(i(x0,i(x1,i(i(n(x2),i(i(n(x3),x4),x2)),i(x3,x2))))). t(i(x0,i(x1,i(n(x0),x2)))). t(i(i(n(i(n(x0),x1)),i(i(n(x2),x3),x0)),i(x2,i(n(x0),x1)))). t(i(x0,i(i(n(x1),i(i(n(i(i(n(x2),i(i(n(x3),x4),n(i(n(x0),x5)))),i(x3,x2))),x6),n(i(x7,x7)))),x1))). t(i(i(x0,i(i(x1,i(i(n(x2),i(i(n(i(i(n(x3),i(i(n(x4),x5),n(i(n(x1),x6)))),i(x4,x3))),x7),n(i(x8,x8)))),x2)),x9)),i(i(n(x9),i(i(n(x10),x11),x0)),i(x10,x9)))). t(i(i(n(i(x0,i(x1,i(x2,x3)))),i(i(n(x4),x5),i(i(n(x1),x6),n(i(n(i(n(i(n(x2),x7)),x8)),x9))))),i(x4,i(x0,i(x1,i(x2,x3)))))). t(i(i(n(i(x0,i(x1,i(x2,x3)))),i(i(n(x4),x5),i(i(n(x1),x6),n(i(x7,i(x8,n(x3))))))),i(x4,i(x0,i(x1,i(x2,x3)))))). t(i(i(n(i(x0,x1)),i(i(n(x2),x3),i(x0,i(i(x4,x4),x1)))),i(x2,i(x0,x1)))). t(i(n(i(n(i(n(i(n(x0),x1)),x2)),x3)),i(x4,i(x5,i(x0,x6))))). t(i(n(i(x0,i(x1,n(x2)))),i(x3,i(x4,i(x5,x2))))). t(i(x0,i(i(n(x1),i(i(n(i(x2,x2)),x3),x1)),x1))). t(i(x0,i(n(i(n(i(n(x1),x2)),x3)),i(x4,i(x1,x5))))). t(i(n(i(n(i(n(x0),x1)),x2)),i(x3,i(x0,x4)))). t(i(x0,i(n(i(x1,i(x2,x3))),i(x4,n(x3))))). t(i(n(i(x0,i(x1,x2))),i(x3,n(x2)))). t(i(x0,i(i(n(x1),i(i(n(x2),x3),i(n(x1),x1))),i(x2,x1)))). t(i(i(n(x0),i(i(n(x1),x2),i(n(x0),x0))),i(x1,x0))). t(i(i(n(x0),x0),x0)). end_of_list.