API tools faq
paste
Advertisement
xamidi

w2.in - exemplary Prover9 input file

xamidi
Mar 3rd, 2024 (edited)
106
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
PostScript 26.23 KB | Science | 0 0
raw download clone embed print report
  1. clear(echo_input).
  2. clear(print_initial_clauses).
  3. clear(print_given).
  4. clear(degrade_hints).
  5. assign(max_megs, 32000).
  6. %assign(max_megs, 1907000). % 2 TB = 1907348.6328125 MiB
  7. assign(max_seconds, -1).
  8. set(hyper_resolution).
  9. %assign(backsub_check, -1).
  10.  
  11. %assign(max_proofs, 7).
  12.  
  13. %set(production).
  14. %assign(sos_limit, 2000000).
  15.  
  16. %assign(variable_weight, 0).
  17. %assign(constant_weight, 0).
  18.  
  19. %list(weights).
  20. %weight(t(x)) = weight(x).
  21. %weight(i(x,y)) = (weight(x) + weight(y)) + 1.
  22. %weight(n(n(n(n(x))))) = weight(x) + 100.
  23. %weight(n(n(n(x)))) = weight(x) + 10.
  24. %weight(n(n(x))) = weight(x) + 4.
  25. %weight(n(x)) = weight(x) + 1.
  26. %end_of_list.
  27.  
  28. formulas(assumptions).
  29.  
  30. % Modus Ponens: (|- p, |- Cpq) => q
  31. t(x) & t(i(x,y)) -> t(y) #label(MP).
  32.  
  33. % Walsh's 2nd Axiom: CpCCqCprCCNrCCNstqCsr
  34. t(i(u,i(i(v,i(u,w)),i(i(n(w),i(i(n(x),y),v)),i(x,w))))) #label(w2).
  35.  
  36. end_of_list.
  37.  
  38. formulas(goals).
  39.  
  40. % Theorems: Cpp,CpCqp,CCpCqrCCpqCpr,CCNpNqCqp
  41. t(i(p,p))                          #answer(id).
  42. t(i(p,i(q,p)))                     #answer(A1).
  43. t(i(i(p,i(q,r)),i(i(p,q),i(p,r)))) #answer(A2).
  44. t(i(i(n(p),n(q)),i(q,p)))          #answer(A3).
  45.  
  46. % Theorems: CCpqCCqrCpr,CCNppp,CpCNpq
  47. t(i(i(p,q),i(i(q,r),i(p,r)))) #answer(L1).
  48. t(i(i(n(p),p),p))             #answer(L2).
  49. t(i(p,i(n(p),q)))             #answer(L3).
  50.  
  51. end_of_list.
  52.  
  53. formulas(hints).
  54.  
  55. 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)))).
  56. 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))))))).
  57. 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)))).
  58. 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)))))).
  59. 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))))).
  60. 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)))).
  61. 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))).
  62. 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))).
  63. t(i(x0,x0)).
  64.  
  65. 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)))).
  66. 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)))).
  67. 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))))))).
  68. 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)))))).
  69. 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)))))).
  70. 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))))).
  71. 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)))))).
  72. 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)))).
  73. 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))))).
  74. 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)))).
  75. 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))))))).
  76. 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)))))).
  77. 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)))))).
  78. t(i(x0,i(x1,i(x2,i(x3,i(x4,x1)))))).
  79. t(i(x0,i(x1,i(x2,i(x3,x0))))).
  80. 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)))).
  81. 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)))).
  82. t(i(x0,i(x1,x0))).
  83.  
  84. 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)))).
  85. 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)))).
  86. 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))))))).
  87. 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)))))).
  88. 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)))))).
  89. 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))))).
  90. 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)))).
  91. 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))))).
  92. 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))))).
  93. 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)))).
  94. 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)))).
  95. t(i(x0,i(n(x0),x1))).
  96.  
  97. 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)))).
  98. 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)))).
  99. 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))))))).
  100. 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)))).
  101. 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)))))).
  102. 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)))))).
  103. 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)))).
  104. 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))))).
  105. 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)))))).
  106. 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)))))).
  107. 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)))))))).
  108. 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)))).
  109. 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)))).
  110. 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))))))).
  111. 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)))).
  112. 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)))).
  113. 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))))))))).
  114. 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)))).
  115. 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))).
  116. 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))))).
  117. 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))).
  118. 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)))).
  119. 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)))).
  120. 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)))).
  121. 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))).
  122. 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))))).
  123. 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))))).
  124. 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))))).
  125. 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))))).
  126. 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)))).
  127. 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)))).
  128. 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)))).
  129. 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)))).
  130. 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)))).
  131. 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)))).
  132. 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))))).
  133. 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))))))).
  134. 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)))).
  135. 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)))))).
  136. 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))).
  137. 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)))))))).
  138. 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)))).
  139. 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)))))))).
  140. t(i(x0,x0)).
  141. 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)))).
  142. 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))))))).
  143. t(i(n(x0),i(i(n(x1),i(i(n(x2),x3),x0)),i(x2,x1)))).
  144. t(i(i(x0,i(i(x1,x1),x2)),i(i(n(x2),i(i(n(x3),x4),x0)),i(x3,x2)))).
  145. 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)))).
  146. 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))))).
  147. 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)))))).
  148. 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)))))).
  149. 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))).
  150. 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))))).
  151. 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)))))).
  152. t(i(x0,i(x1,i(x2,i(x3,i(x4,x1)))))).
  153. 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))))).
  154. t(i(x0,i(x1,i(x2,i(x3,x0))))).
  155. 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)))).
  156. t(i(x0,i(x1,i(x2,x2)))).
  157. 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)))).
  158. 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)))))).
  159. 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)))).
  160. 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))))).
  161. 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)))).
  162. t(i(x0,i(x1,x0))).
  163. t(i(i(x0,i(i(x1,i(x2,x1)),x3)),i(i(n(x3),i(i(n(x4),x5),x0)),i(x4,x3)))).
  164. 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))))))).
  165. 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)))).
  166. 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))))).
  167. 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))))).
  168. 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))))).
  169. t(i(x0,i(x1,i(x2,i(n(i(n(x2),x3)),x4))))).
  170. 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)))))).
  171. 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)))).
  172. t(i(x0,i(x1,i(x2,x0)))).
  173. t(i(x0,i(x1,i(n(x2),i(i(n(x3),i(i(n(x4),x5),x2)),i(x4,x3)))))).
  174. 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)))).
  175. 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)))).
  176. t(i(i(n(i(x0,x1)),i(i(n(x2),x3),x1)),i(x2,i(x0,x1)))).
  177. 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)))).
  178. t(i(x0,i(x1,i(i(n(x2),i(i(n(x3),x4),x2)),i(x3,x2))))).
  179. t(i(x0,i(x1,i(n(x0),x2)))).
  180. t(i(i(n(i(n(x0),x1)),i(i(n(x2),x3),x0)),i(x2,i(n(x0),x1)))).
  181. 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))).
  182. 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)))).
  183. 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)))))).
  184. 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)))))).
  185. t(i(i(n(i(x0,x1)),i(i(n(x2),x3),i(x0,i(i(x4,x4),x1)))),i(x2,i(x0,x1)))).
  186. t(i(n(i(n(i(n(i(n(x0),x1)),x2)),x3)),i(x4,i(x5,i(x0,x6))))).
  187. t(i(n(i(x0,i(x1,n(x2)))),i(x3,i(x4,i(x5,x2))))).
  188. t(i(x0,i(i(n(x1),i(i(n(i(x2,x2)),x3),x1)),x1))).
  189. t(i(x0,i(n(i(n(i(n(x1),x2)),x3)),i(x4,i(x1,x5))))).
  190. t(i(n(i(n(i(n(x0),x1)),x2)),i(x3,i(x0,x4)))).
  191. t(i(x0,i(n(i(x1,i(x2,x3))),i(x4,n(x3))))).
  192. t(i(n(i(x0,i(x1,x2))),i(x3,n(x2)))).
  193. t(i(x0,i(i(n(x1),i(i(n(x2),x3),i(n(x1),x1))),i(x2,x1)))).
  194. t(i(i(n(x0),i(i(n(x1),x2),i(n(x0),x0))),i(x1,x0))).
  195. t(i(i(n(x0),x0),x0)).
  196.  
  197. end_of_list.
  198.  
Tags: logic CpCqp CCpCqrCCpqCpr prover9 CpCCqCprCCNrCCNstqCsr CCNppp automated theorem proving CCNpNqCqp CCpqCCqrCpr CpCNpq
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!