OAI/Combinatorics/Ramsey/CycleClique/Certificates037.lean

GitHub source file

1044 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CycleClique.certificate_1152_q line 20
  2. def OAI.CycleClique.certificate_1152_edges line 21
  3. def OAI.CycleClique.certificate_1152_part_0 line 23
  4. def OAI.CycleClique.certificate_1152_part_1 line 25
  5. def OAI.CycleClique.certificate_1152 line 27
  6. theorem OAI.CycleClique.certificate_1152_checked line 29
  7. theorem OAI.CycleClique.certificate_1152_valid line 30
  8. def OAI.CycleClique.certificate_1153_q line 32
  9. def OAI.CycleClique.certificate_1153_edges line 33
  10. def OAI.CycleClique.certificate_1153_part_0 line 35
  11. def OAI.CycleClique.certificate_1153_part_1 line 37
  12. def OAI.CycleClique.certificate_1153 line 39
  13. theorem OAI.CycleClique.certificate_1153_checked line 41
  14. theorem OAI.CycleClique.certificate_1153_valid line 42
  15. def OAI.CycleClique.certificate_1154_q line 44
  16. def OAI.CycleClique.certificate_1154_edges line 45
  17. def OAI.CycleClique.certificate_1154_part_0 line 47
  18. def OAI.CycleClique.certificate_1154_part_1 line 49
  19. def OAI.CycleClique.certificate_1154_part_2 line 51
  20. def OAI.CycleClique.certificate_1154_part_3 line 53
  21. def OAI.CycleClique.certificate_1154 line 55
  22. theorem OAI.CycleClique.certificate_1154_checked line 57
  23. theorem OAI.CycleClique.certificate_1154_valid line 58
  24. def OAI.CycleClique.certificate_1155_q line 60
  25. def OAI.CycleClique.certificate_1155_edges line 61
  26. def OAI.CycleClique.certificate_1155_part_0 line 63
  27. def OAI.CycleClique.certificate_1155_part_1 line 65
  28. def OAI.CycleClique.certificate_1155_part_2 line 67
  29. def OAI.CycleClique.certificate_1155_part_3 line 69
  30. def OAI.CycleClique.certificate_1155 line 71
  31. theorem OAI.CycleClique.certificate_1155_checked line 73
  32. theorem OAI.CycleClique.certificate_1155_valid line 74
  33. def OAI.CycleClique.certificate_1156_q line 76
  34. def OAI.CycleClique.certificate_1156_edges line 77
  35. def OAI.CycleClique.certificate_1156_part_0 line 79
  36. def OAI.CycleClique.certificate_1156_part_1 line 81
  37. def OAI.CycleClique.certificate_1156_part_2 line 83
  38. def OAI.CycleClique.certificate_1156_part_3 line 85
  39. def OAI.CycleClique.certificate_1156 line 87
  40. theorem OAI.CycleClique.certificate_1156_checked line 89
  41. theorem OAI.CycleClique.certificate_1156_valid line 90
  42. def OAI.CycleClique.certificate_1157_q line 92
  43. def OAI.CycleClique.certificate_1157_edges line 93
  44. def OAI.CycleClique.certificate_1157_part_0 line 95
  45. def OAI.CycleClique.certificate_1157_part_1 line 97
  46. def OAI.CycleClique.certificate_1157_part_2 line 99
  47. def OAI.CycleClique.certificate_1157_part_3 line 101
  48. def OAI.CycleClique.certificate_1157 line 103
  49. theorem OAI.CycleClique.certificate_1157_checked line 105
  50. theorem OAI.CycleClique.certificate_1157_valid line 106
  51. def OAI.CycleClique.certificate_1158_q line 108
  52. def OAI.CycleClique.certificate_1158_edges line 109
  53. def OAI.CycleClique.certificate_1158_part_0 line 111
  54. def OAI.CycleClique.certificate_1158_part_1 line 113
  55. def OAI.CycleClique.certificate_1158_part_2 line 115
  56. def OAI.CycleClique.certificate_1158_part_3 line 117
  57. def OAI.CycleClique.certificate_1158_part_4 line 119
  58. def OAI.CycleClique.certificate_1158 line 121
  59. theorem OAI.CycleClique.certificate_1158_checked line 123
  60. theorem OAI.CycleClique.certificate_1158_valid line 124
  61. def OAI.CycleClique.certificate_1159_q line 126
  62. def OAI.CycleClique.certificate_1159_edges line 128
  63. def OAI.CycleClique.certificate_1159_E line 130
  64. def OAI.CycleClique.certificate_1159_M line 132
  65. def OAI.CycleClique.certificate_1159_part_1_E line 134
  66. def OAI.CycleClique.certificate_1159_part_1_M line 136
  67. def OAI.CycleClique.certificate_1159_part_2_E line 138
  68. def OAI.CycleClique.certificate_1159_part_2_M line 140
  69. def OAI.CycleClique.certificate_1159_part_3_E line 142
  70. def OAI.CycleClique.certificate_1159_part_3_M line 144
  71. def OAI.CycleClique.certificate_1159_part_4_E line 146
  72. def OAI.CycleClique.certificate_1159_part_4_M line 148
  73. def OAI.CycleClique.certificate_1159_part_5_E line 150
  74. def OAI.CycleClique.certificate_1159_part_5_M line 152
  75. def OAI.CycleClique.certificate_1159_part_6_E line 154
  76. def OAI.CycleClique.certificate_1159_part_6_M line 156
  77. def OAI.CycleClique.certificate_1159_part_7_E line 158
  78. def OAI.CycleClique.certificate_1159_part_7_M line 160
  79. def OAI.CycleClique.certificate_1159_part_8_E line 162
  80. def OAI.CycleClique.certificate_1159_part_8_M line 164
  81. def OAI.CycleClique.certificate_1159_part_9_E line 166
  82. def OAI.CycleClique.certificate_1159_part_9_M line 168
  83. def OAI.CycleClique.certificate_1159_part_10_E line 170
  84. def OAI.CycleClique.certificate_1159_part_10_M line 172
  85. def OAI.CycleClique.certificate_1159_part_11_E line 174
  86. def OAI.CycleClique.certificate_1159_part_11_M line 176
  87. def OAI.CycleClique.certificate_1159_part_12_E line 178
  88. def OAI.CycleClique.certificate_1159_part_12_M line 180
  89. def OAI.CycleClique.certificate_1159_part_13_E line 182
  90. def OAI.CycleClique.certificate_1159_part_13_M line 184
  91. def OAI.CycleClique.certificate_1159_part_14_E line 186
  92. def OAI.CycleClique.certificate_1159_part_14_M line 188
  93. def OAI.CycleClique.certificate_1159_part_14 line 190
  94. theorem OAI.CycleClique.certificate_1159_part_14_checked line 192
  95. def OAI.CycleClique.certificate_1159_part_13 line 194
  96. theorem OAI.CycleClique.certificate_1159_part_13_checked line 196
  97. def OAI.CycleClique.certificate_1159_part_15_E line 198
  98. def OAI.CycleClique.certificate_1159_part_15_M line 200
  99. def OAI.CycleClique.certificate_1159_part_16_E line 202
  100. def OAI.CycleClique.certificate_1159_part_16_M line 204
  101. def OAI.CycleClique.certificate_1159_part_17_E line 206
  102. def OAI.CycleClique.certificate_1159_part_17_M line 208
  103. def OAI.CycleClique.certificate_1159_part_18_E line 210
  104. def OAI.CycleClique.certificate_1159_part_18_M line 212
  105. def OAI.CycleClique.certificate_1159_part_19_E line 214
  106. def OAI.CycleClique.certificate_1159_part_19_M line 216
  107. def OAI.CycleClique.certificate_1159_part_19 line 218
  108. theorem OAI.CycleClique.certificate_1159_part_19_checked line 220
  109. def OAI.CycleClique.certificate_1159_part_18 line 222
  110. theorem OAI.CycleClique.certificate_1159_part_18_checked line 224
  111. def OAI.CycleClique.certificate_1159_part_20_E line 226
  112. def OAI.CycleClique.certificate_1159_part_20_M line 228
  113. def OAI.CycleClique.certificate_1159_part_21_E line 230
  114. def OAI.CycleClique.certificate_1159_part_21_M line 232
  115. def OAI.CycleClique.certificate_1159_part_22_E line 234
  116. def OAI.CycleClique.certificate_1159_part_22_M line 236
  117. def OAI.CycleClique.certificate_1159_part_23_E line 238
  118. def OAI.CycleClique.certificate_1159_part_23_M line 240
  119. def OAI.CycleClique.certificate_1159_part_24_E line 242
  120. def OAI.CycleClique.certificate_1159_part_24_M line 244
  121. def OAI.CycleClique.certificate_1159_part_25_E line 246
  122. def OAI.CycleClique.certificate_1159_part_25_M line 248
  123. def OAI.CycleClique.certificate_1159_part_25 line 250
  124. theorem OAI.CycleClique.certificate_1159_part_25_checked line 252
  125. def OAI.CycleClique.certificate_1159_part_24 line 254
  126. theorem OAI.CycleClique.certificate_1159_part_24_checked line 256
  127. def OAI.CycleClique.certificate_1159_part_23 line 258
  128. theorem OAI.CycleClique.certificate_1159_part_23_checked line 260
  129. def OAI.CycleClique.certificate_1159_part_22 line 262
  130. theorem OAI.CycleClique.certificate_1159_part_22_checked line 264
  131. def OAI.CycleClique.certificate_1159_part_26_E line 266
  132. def OAI.CycleClique.certificate_1159_part_26_M line 268
  133. def OAI.CycleClique.certificate_1159_part_27_E line 270
  134. def OAI.CycleClique.certificate_1159_part_27_M line 272
  135. def OAI.CycleClique.certificate_1159_part_28_E line 274
  136. def OAI.CycleClique.certificate_1159_part_28_M line 276
  137. def OAI.CycleClique.certificate_1159_part_29_E line 278
  138. def OAI.CycleClique.certificate_1159_part_29_M line 280
  139. def OAI.CycleClique.certificate_1159_part_29 line 282
  140. theorem OAI.CycleClique.certificate_1159_part_29_checked line 284
  141. def OAI.CycleClique.certificate_1159_part_28 line 286
  142. theorem OAI.CycleClique.certificate_1159_part_28_checked line 288
  143. def OAI.CycleClique.certificate_1159_part_27 line 290
  144. theorem OAI.CycleClique.certificate_1159_part_27_checked line 292
  145. def OAI.CycleClique.certificate_1159_part_26 line 294
  146. theorem OAI.CycleClique.certificate_1159_part_26_checked line 296
  147. def OAI.CycleClique.certificate_1159_part_30_E line 298
  148. def OAI.CycleClique.certificate_1159_part_30_M line 300
  149. def OAI.CycleClique.certificate_1159_part_31_E line 302
  150. def OAI.CycleClique.certificate_1159_part_31_M line 304
  151. def OAI.CycleClique.certificate_1159_part_32_E line 306
  152. def OAI.CycleClique.certificate_1159_part_32_M line 308
  153. def OAI.CycleClique.certificate_1159_part_33_E line 310
  154. def OAI.CycleClique.certificate_1159_part_33_M line 312
  155. def OAI.CycleClique.certificate_1159_part_33 line 314
  156. theorem OAI.CycleClique.certificate_1159_part_33_checked line 316
  157. def OAI.CycleClique.certificate_1159_part_32 line 318
  158. theorem OAI.CycleClique.certificate_1159_part_32_checked line 320
  159. def OAI.CycleClique.certificate_1159_part_31 line 322
  160. theorem OAI.CycleClique.certificate_1159_part_31_checked line 324
  161. def OAI.CycleClique.certificate_1159_part_30 line 326
  162. theorem OAI.CycleClique.certificate_1159_part_30_checked line 328
  163. def OAI.CycleClique.certificate_1159_part_34_E line 330
  164. def OAI.CycleClique.certificate_1159_part_34_M line 332
  165. def OAI.CycleClique.certificate_1159_part_35_E line 334
  166. def OAI.CycleClique.certificate_1159_part_35_M line 336
  167. def OAI.CycleClique.certificate_1159_part_36_E line 338
  168. def OAI.CycleClique.certificate_1159_part_36_M line 340
  169. def OAI.CycleClique.certificate_1159_part_37_E line 342
  170. def OAI.CycleClique.certificate_1159_part_37_M line 344
  171. def OAI.CycleClique.certificate_1159_part_37 line 346
  172. theorem OAI.CycleClique.certificate_1159_part_37_checked line 348
  173. def OAI.CycleClique.certificate_1159_part_36 line 350
  174. theorem OAI.CycleClique.certificate_1159_part_36_checked line 352
  175. def OAI.CycleClique.certificate_1159_part_35 line 354
  176. theorem OAI.CycleClique.certificate_1159_part_35_checked line 356
  177. def OAI.CycleClique.certificate_1159_part_38_E line 358
  178. def OAI.CycleClique.certificate_1159_part_38_M line 360
  179. def OAI.CycleClique.certificate_1159_part_39_E line 362
  180. def OAI.CycleClique.certificate_1159_part_39_M line 364
  181. def OAI.CycleClique.certificate_1159_part_39 line 366
  182. theorem OAI.CycleClique.certificate_1159_part_39_checked line 368
  183. def OAI.CycleClique.certificate_1159_part_40_E line 370
  184. def OAI.CycleClique.certificate_1159_part_40_M line 372
  185. def OAI.CycleClique.certificate_1159_part_41_E line 374
  186. def OAI.CycleClique.certificate_1159_part_41_M line 376
  187. def OAI.CycleClique.certificate_1159_part_41 line 378
  188. theorem OAI.CycleClique.certificate_1159_part_41_checked line 380
  189. def OAI.CycleClique.certificate_1159_part_40 line 382
  190. theorem OAI.CycleClique.certificate_1159_part_40_checked line 384
  191. def OAI.CycleClique.certificate_1159_part_42_E line 386
  192. def OAI.CycleClique.certificate_1159_part_42_M line 388
  193. def OAI.CycleClique.certificate_1159_part_43_E line 390
  194. def OAI.CycleClique.certificate_1159_part_43_M line 392
  195. def OAI.CycleClique.certificate_1159_part_44_E line 394
  196. def OAI.CycleClique.certificate_1159_part_44_M line 396
  197. def OAI.CycleClique.certificate_1159_part_45_E line 398
  198. def OAI.CycleClique.certificate_1159_part_45_M line 400
  199. def OAI.CycleClique.certificate_1159_part_45 line 402
  200. theorem OAI.CycleClique.certificate_1159_part_45_checked line 404
  201. def OAI.CycleClique.certificate_1159_part_44 line 406
  202. theorem OAI.CycleClique.certificate_1159_part_44_checked line 408
  203. def OAI.CycleClique.certificate_1159_part_43 line 410
  204. theorem OAI.CycleClique.certificate_1159_part_43_checked line 412
  205. def OAI.CycleClique.certificate_1159_part_42 line 414
  206. theorem OAI.CycleClique.certificate_1159_part_42_checked line 416
  207. def OAI.CycleClique.certificate_1159_part_46_E line 418
  208. def OAI.CycleClique.certificate_1159_part_46_M line 420
  209. def OAI.CycleClique.certificate_1159_part_47_E line 422
  210. def OAI.CycleClique.certificate_1159_part_47_M line 424
  211. def OAI.CycleClique.certificate_1159_part_48_E line 426
  212. def OAI.CycleClique.certificate_1159_part_48_M line 428
  213. def OAI.CycleClique.certificate_1159_part_49_E line 430
  214. def OAI.CycleClique.certificate_1159_part_49_M line 432
  215. def OAI.CycleClique.certificate_1159_part_49 line 434
  216. theorem OAI.CycleClique.certificate_1159_part_49_checked line 436
  217. def OAI.CycleClique.certificate_1159_part_48 line 438
  218. theorem OAI.CycleClique.certificate_1159_part_48_checked line 440
  219. def OAI.CycleClique.certificate_1159_part_47 line 442
  220. theorem OAI.CycleClique.certificate_1159_part_47_checked line 444
  221. def OAI.CycleClique.certificate_1159_part_46 line 446
  222. theorem OAI.CycleClique.certificate_1159_part_46_checked line 448
  223. def OAI.CycleClique.certificate_1159_part_50_E line 450
  224. def OAI.CycleClique.certificate_1159_part_50_M line 452
  225. def OAI.CycleClique.certificate_1159_part_51_E line 454
  226. def OAI.CycleClique.certificate_1159_part_51_M line 456
  227. def OAI.CycleClique.certificate_1159_part_52_E line 458
  228. def OAI.CycleClique.certificate_1159_part_52_M line 460
  229. def OAI.CycleClique.certificate_1159_part_53_E line 462
  230. def OAI.CycleClique.certificate_1159_part_53_M line 464
  231. def OAI.CycleClique.certificate_1159_part_53 line 466
  232. theorem OAI.CycleClique.certificate_1159_part_53_checked line 468
  233. def OAI.CycleClique.certificate_1159_part_52 line 470
  234. theorem OAI.CycleClique.certificate_1159_part_52_checked line 472
  235. def OAI.CycleClique.certificate_1159_part_51 line 474
  236. theorem OAI.CycleClique.certificate_1159_part_51_checked line 476
  237. def OAI.CycleClique.certificate_1159_part_50 line 478
  238. theorem OAI.CycleClique.certificate_1159_part_50_checked line 480
  239. def OAI.CycleClique.certificate_1159_part_54_E line 482
  240. def OAI.CycleClique.certificate_1159_part_54_M line 484
  241. def OAI.CycleClique.certificate_1159_part_55_E line 486
  242. def OAI.CycleClique.certificate_1159_part_55_M line 488
  243. def OAI.CycleClique.certificate_1159_part_56_E line 490
  244. def OAI.CycleClique.certificate_1159_part_56_M line 492
  245. def OAI.CycleClique.certificate_1159_part_57_E line 494
  246. def OAI.CycleClique.certificate_1159_part_57_M line 496
  247. def OAI.CycleClique.certificate_1159_part_57 line 498
  248. theorem OAI.CycleClique.certificate_1159_part_57_checked line 500
  249. def OAI.CycleClique.certificate_1159_part_56 line 502
  250. theorem OAI.CycleClique.certificate_1159_part_56_checked line 504
  251. def OAI.CycleClique.certificate_1159_part_55 line 506
  252. theorem OAI.CycleClique.certificate_1159_part_55_checked line 508
  253. def OAI.CycleClique.certificate_1159_part_54 line 510
  254. theorem OAI.CycleClique.certificate_1159_part_54_checked line 512
  255. def OAI.CycleClique.certificate_1159_part_58_E line 514
  256. def OAI.CycleClique.certificate_1159_part_58_M line 516
  257. def OAI.CycleClique.certificate_1159_part_58 line 518
  258. theorem OAI.CycleClique.certificate_1159_part_58_checked line 520
  259. def OAI.CycleClique.certificate_1159_part_59_E line 522
  260. def OAI.CycleClique.certificate_1159_part_59_M line 524
  261. def OAI.CycleClique.certificate_1159_part_60_E line 526
  262. def OAI.CycleClique.certificate_1159_part_60_M line 528
  263. def OAI.CycleClique.certificate_1159_part_61_E line 530
  264. def OAI.CycleClique.certificate_1159_part_61_M line 532
  265. def OAI.CycleClique.certificate_1159_part_61 line 534
  266. theorem OAI.CycleClique.certificate_1159_part_61_checked line 536
  267. def OAI.CycleClique.certificate_1159_part_60 line 538
  268. theorem OAI.CycleClique.certificate_1159_part_60_checked line 540
  269. def OAI.CycleClique.certificate_1159_part_62_E line 542
  270. def OAI.CycleClique.certificate_1159_part_62_M line 544
  271. def OAI.CycleClique.certificate_1159_part_63_E line 546
  272. def OAI.CycleClique.certificate_1159_part_63_M line 548
  273. def OAI.CycleClique.certificate_1159_part_64_E line 550
  274. def OAI.CycleClique.certificate_1159_part_64_M line 552
  275. def OAI.CycleClique.certificate_1159_part_65_E line 554
  276. def OAI.CycleClique.certificate_1159_part_65_M line 556
  277. def OAI.CycleClique.certificate_1159_part_65 line 558
  278. theorem OAI.CycleClique.certificate_1159_part_65_checked line 560
  279. def OAI.CycleClique.certificate_1159_part_64 line 562
  280. theorem OAI.CycleClique.certificate_1159_part_64_checked line 564
  281. def OAI.CycleClique.certificate_1159_part_63 line 566
  282. theorem OAI.CycleClique.certificate_1159_part_63_checked line 568
  283. def OAI.CycleClique.certificate_1159_part_62 line 570
  284. theorem OAI.CycleClique.certificate_1159_part_62_checked line 572
  285. def OAI.CycleClique.certificate_1159_part_66_E line 574
  286. def OAI.CycleClique.certificate_1159_part_66_M line 576
  287. def OAI.CycleClique.certificate_1159_part_67_E line 578
  288. def OAI.CycleClique.certificate_1159_part_67_M line 580
  289. def OAI.CycleClique.certificate_1159_part_68_E line 582
  290. def OAI.CycleClique.certificate_1159_part_68_M line 584
  291. def OAI.CycleClique.certificate_1159_part_69_E line 586
  292. def OAI.CycleClique.certificate_1159_part_69_M line 588
  293. def OAI.CycleClique.certificate_1159_part_69 line 590
  294. theorem OAI.CycleClique.certificate_1159_part_69_checked line 592
  295. def OAI.CycleClique.certificate_1159_part_68 line 594
  296. theorem OAI.CycleClique.certificate_1159_part_68_checked line 596
  297. def OAI.CycleClique.certificate_1159_part_67 line 598
  298. theorem OAI.CycleClique.certificate_1159_part_67_checked line 600
  299. def OAI.CycleClique.certificate_1159_part_66 line 602
  300. theorem OAI.CycleClique.certificate_1159_part_66_checked line 604
  301. def OAI.CycleClique.certificate_1159_part_70_E line 606
  302. def OAI.CycleClique.certificate_1159_part_70_M line 608
  303. def OAI.CycleClique.certificate_1159_part_71_E line 610
  304. def OAI.CycleClique.certificate_1159_part_71_M line 612
  305. def OAI.CycleClique.certificate_1159_part_72_E line 614
  306. def OAI.CycleClique.certificate_1159_part_72_M line 616
  307. def OAI.CycleClique.certificate_1159_part_73_E line 618
  308. def OAI.CycleClique.certificate_1159_part_73_M line 620
  309. def OAI.CycleClique.certificate_1159_part_73 line 622
  310. theorem OAI.CycleClique.certificate_1159_part_73_checked line 624
  311. def OAI.CycleClique.certificate_1159_part_72 line 626
  312. theorem OAI.CycleClique.certificate_1159_part_72_checked line 628
  313. def OAI.CycleClique.certificate_1159_part_71 line 630
  314. theorem OAI.CycleClique.certificate_1159_part_71_checked line 632
  315. def OAI.CycleClique.certificate_1159_part_70 line 634
  316. theorem OAI.CycleClique.certificate_1159_part_70_checked line 636
  317. def OAI.CycleClique.certificate_1159_part_74_E line 638
  318. def OAI.CycleClique.certificate_1159_part_74_M line 640
  319. def OAI.CycleClique.certificate_1159_part_75_E line 642
  320. def OAI.CycleClique.certificate_1159_part_75_M line 644
  321. def OAI.CycleClique.certificate_1159_part_76_E line 646
  322. def OAI.CycleClique.certificate_1159_part_76_M line 648
  323. def OAI.CycleClique.certificate_1159_part_77_E line 650
  324. def OAI.CycleClique.certificate_1159_part_77_M line 652
  325. def OAI.CycleClique.certificate_1159_part_77 line 654
  326. theorem OAI.CycleClique.certificate_1159_part_77_checked line 656
  327. def OAI.CycleClique.certificate_1159_part_76 line 658
  328. theorem OAI.CycleClique.certificate_1159_part_76_checked line 660
  329. def OAI.CycleClique.certificate_1159_part_75 line 662
  330. theorem OAI.CycleClique.certificate_1159_part_75_checked line 664
  331. def OAI.CycleClique.certificate_1159_part_74 line 666
  332. theorem OAI.CycleClique.certificate_1159_part_74_checked line 668
  333. def OAI.CycleClique.certificate_1159_part_78_E line 670
  334. def OAI.CycleClique.certificate_1159_part_78_M line 672
  335. def OAI.CycleClique.certificate_1159_part_78 line 674
  336. theorem OAI.CycleClique.certificate_1159_part_78_checked line 676
  337. def OAI.CycleClique.certificate_1159_part_79_E line 678
  338. def OAI.CycleClique.certificate_1159_part_79_M line 680
  339. def OAI.CycleClique.certificate_1159_part_80_E line 682
  340. def OAI.CycleClique.certificate_1159_part_80_M line 684
  341. def OAI.CycleClique.certificate_1159_part_81_E line 686
  342. def OAI.CycleClique.certificate_1159_part_81_M line 688
  343. def OAI.CycleClique.certificate_1159_part_81 line 690
  344. theorem OAI.CycleClique.certificate_1159_part_81_checked line 692
  345. def OAI.CycleClique.certificate_1159_part_80 line 694
  346. theorem OAI.CycleClique.certificate_1159_part_80_checked line 696
  347. def OAI.CycleClique.certificate_1159_part_82_E line 698
  348. def OAI.CycleClique.certificate_1159_part_82_M line 700
  349. def OAI.CycleClique.certificate_1159_part_83_E line 702
  350. def OAI.CycleClique.certificate_1159_part_83_M line 704
  351. def OAI.CycleClique.certificate_1159_part_84_E line 706
  352. def OAI.CycleClique.certificate_1159_part_84_M line 708
  353. def OAI.CycleClique.certificate_1159_part_85_E line 710
  354. def OAI.CycleClique.certificate_1159_part_85_M line 712
  355. def OAI.CycleClique.certificate_1159_part_85 line 714
  356. theorem OAI.CycleClique.certificate_1159_part_85_checked line 716
  357. def OAI.CycleClique.certificate_1159_part_84 line 718
  358. theorem OAI.CycleClique.certificate_1159_part_84_checked line 720
  359. def OAI.CycleClique.certificate_1159_part_83 line 722
  360. theorem OAI.CycleClique.certificate_1159_part_83_checked line 724
  361. def OAI.CycleClique.certificate_1159_part_82 line 726
  362. theorem OAI.CycleClique.certificate_1159_part_82_checked line 728
  363. def OAI.CycleClique.certificate_1159_part_86_E line 730
  364. def OAI.CycleClique.certificate_1159_part_86_M line 732
  365. def OAI.CycleClique.certificate_1159_part_87_E line 734
  366. def OAI.CycleClique.certificate_1159_part_87_M line 736
  367. def OAI.CycleClique.certificate_1159_part_88_E line 738
  368. def OAI.CycleClique.certificate_1159_part_88_M line 740
  369. def OAI.CycleClique.certificate_1159_part_89_E line 742
  370. def OAI.CycleClique.certificate_1159_part_89_M line 744
  371. def OAI.CycleClique.certificate_1159_part_89 line 746
  372. theorem OAI.CycleClique.certificate_1159_part_89_checked line 748
  373. def OAI.CycleClique.certificate_1159_part_88 line 750
  374. theorem OAI.CycleClique.certificate_1159_part_88_checked line 752
  375. def OAI.CycleClique.certificate_1159_part_87 line 754
  376. theorem OAI.CycleClique.certificate_1159_part_87_checked line 756
  377. def OAI.CycleClique.certificate_1159_part_86 line 758
  378. theorem OAI.CycleClique.certificate_1159_part_86_checked line 760
  379. def OAI.CycleClique.certificate_1159_part_90_E line 762
  380. def OAI.CycleClique.certificate_1159_part_90_M line 764
  381. def OAI.CycleClique.certificate_1159_part_91_E line 766
  382. def OAI.CycleClique.certificate_1159_part_91_M line 768
  383. def OAI.CycleClique.certificate_1159_part_92_E line 770
  384. def OAI.CycleClique.certificate_1159_part_92_M line 772
  385. def OAI.CycleClique.certificate_1159_part_93_E line 774
  386. def OAI.CycleClique.certificate_1159_part_93_M line 776
  387. def OAI.CycleClique.certificate_1159_part_93 line 778
  388. theorem OAI.CycleClique.certificate_1159_part_93_checked line 780
  389. def OAI.CycleClique.certificate_1159_part_92 line 782
  390. theorem OAI.CycleClique.certificate_1159_part_92_checked line 784
  391. def OAI.CycleClique.certificate_1159_part_91 line 786
  392. theorem OAI.CycleClique.certificate_1159_part_91_checked line 788
  393. def OAI.CycleClique.certificate_1159_part_90 line 790
  394. theorem OAI.CycleClique.certificate_1159_part_90_checked line 792
  395. def OAI.CycleClique.certificate_1159_part_94_E line 794
  396. def OAI.CycleClique.certificate_1159_part_94_M line 796
  397. def OAI.CycleClique.certificate_1159_part_95_E line 798
  398. def OAI.CycleClique.certificate_1159_part_95_M line 800
  399. def OAI.CycleClique.certificate_1159_part_96_E line 802
  400. def OAI.CycleClique.certificate_1159_part_96_M line 804
  401. def OAI.CycleClique.certificate_1159_part_97_E line 806
  402. def OAI.CycleClique.certificate_1159_part_97_M line 808
  403. def OAI.CycleClique.certificate_1159_part_97 line 810
  404. theorem OAI.CycleClique.certificate_1159_part_97_checked line 812
  405. def OAI.CycleClique.certificate_1159_part_96 line 814
  406. theorem OAI.CycleClique.certificate_1159_part_96_checked line 816
  407. def OAI.CycleClique.certificate_1159_part_95 line 818
  408. theorem OAI.CycleClique.certificate_1159_part_95_checked line 820
  409. def OAI.CycleClique.certificate_1159_part_94 line 822
  410. theorem OAI.CycleClique.certificate_1159_part_94_checked line 824
  411. def OAI.CycleClique.certificate_1159_part_98_E line 826
  412. def OAI.CycleClique.certificate_1159_part_98_M line 828
  413. def OAI.CycleClique.certificate_1159_part_98 line 830
  414. theorem OAI.CycleClique.certificate_1159_part_98_checked line 832
  415. def OAI.CycleClique.certificate_1159_part_99_E line 834
  416. def OAI.CycleClique.certificate_1159_part_99_M line 836
  417. def OAI.CycleClique.certificate_1159_part_100_E line 838
  418. def OAI.CycleClique.certificate_1159_part_100_M line 840
  419. def OAI.CycleClique.certificate_1159_part_101_E line 842
  420. def OAI.CycleClique.certificate_1159_part_101_M line 844
  421. def OAI.CycleClique.certificate_1159_part_101 line 846
  422. theorem OAI.CycleClique.certificate_1159_part_101_checked line 848
  423. def OAI.CycleClique.certificate_1159_part_100 line 850
  424. theorem OAI.CycleClique.certificate_1159_part_100_checked line 852
  425. def OAI.CycleClique.certificate_1159_part_102_E line 854
  426. def OAI.CycleClique.certificate_1159_part_102_M line 856
  427. def OAI.CycleClique.certificate_1159_part_103_E line 858
  428. def OAI.CycleClique.certificate_1159_part_103_M line 860
  429. def OAI.CycleClique.certificate_1159_part_104_E line 862
  430. def OAI.CycleClique.certificate_1159_part_104_M line 864
  431. def OAI.CycleClique.certificate_1159_part_105_E line 866
  432. def OAI.CycleClique.certificate_1159_part_105_M line 868
  433. def OAI.CycleClique.certificate_1159_part_105 line 870
  434. theorem OAI.CycleClique.certificate_1159_part_105_checked line 872
  435. def OAI.CycleClique.certificate_1159_part_104 line 874
  436. theorem OAI.CycleClique.certificate_1159_part_104_checked line 876
  437. def OAI.CycleClique.certificate_1159_part_103 line 878
  438. theorem OAI.CycleClique.certificate_1159_part_103_checked line 880
  439. def OAI.CycleClique.certificate_1159_part_102 line 882
  440. theorem OAI.CycleClique.certificate_1159_part_102_checked line 884
  441. def OAI.CycleClique.certificate_1159_part_106_E line 886
  442. def OAI.CycleClique.certificate_1159_part_106_M line 888
  443. def OAI.CycleClique.certificate_1159_part_107_E line 890
  444. def OAI.CycleClique.certificate_1159_part_107_M line 892
  445. def OAI.CycleClique.certificate_1159_part_108_E line 894
  446. def OAI.CycleClique.certificate_1159_part_108_M line 896
  447. def OAI.CycleClique.certificate_1159_part_109_E line 898
  448. def OAI.CycleClique.certificate_1159_part_109_M line 900
  449. def OAI.CycleClique.certificate_1159_part_109 line 902
  450. theorem OAI.CycleClique.certificate_1159_part_109_checked line 904
  451. def OAI.CycleClique.certificate_1159_part_108 line 906
  452. theorem OAI.CycleClique.certificate_1159_part_108_checked line 908
  453. def OAI.CycleClique.certificate_1159_part_107 line 910
  454. theorem OAI.CycleClique.certificate_1159_part_107_checked line 912
  455. def OAI.CycleClique.certificate_1159_part_106 line 914
  456. theorem OAI.CycleClique.certificate_1159_part_106_checked line 916
  457. def OAI.CycleClique.certificate_1159_part_110_E line 918
  458. def OAI.CycleClique.certificate_1159_part_110_M line 920
  459. def OAI.CycleClique.certificate_1159_part_111_E line 922
  460. def OAI.CycleClique.certificate_1159_part_111_M line 924
  461. def OAI.CycleClique.certificate_1159_part_112_E line 926
  462. def OAI.CycleClique.certificate_1159_part_112_M line 928
  463. def OAI.CycleClique.certificate_1159_part_113_E line 930
  464. def OAI.CycleClique.certificate_1159_part_113_M line 932
  465. def OAI.CycleClique.certificate_1159_part_113 line 934
  466. theorem OAI.CycleClique.certificate_1159_part_113_checked line 936
  467. def OAI.CycleClique.certificate_1159_part_112 line 938
  468. theorem OAI.CycleClique.certificate_1159_part_112_checked line 940
  469. def OAI.CycleClique.certificate_1159_part_111 line 942
  470. theorem OAI.CycleClique.certificate_1159_part_111_checked line 944
  471. def OAI.CycleClique.certificate_1159_part_114_E line 946
  472. def OAI.CycleClique.certificate_1159_part_114_M line 948
  473. def OAI.CycleClique.certificate_1159_part_115_E line 950
  474. def OAI.CycleClique.certificate_1159_part_115_M line 952
  475. def OAI.CycleClique.certificate_1159_part_116_E line 954
  476. def OAI.CycleClique.certificate_1159_part_116_M line 956
  477. def OAI.CycleClique.certificate_1159_part_117_E line 958
  478. def OAI.CycleClique.certificate_1159_part_117_M line 960
  479. def OAI.CycleClique.certificate_1159_part_117 line 962
  480. theorem OAI.CycleClique.certificate_1159_part_117_checked line 964
  481. def OAI.CycleClique.certificate_1159_part_116 line 966
  482. theorem OAI.CycleClique.certificate_1159_part_116_checked line 968
  483. def OAI.CycleClique.certificate_1159_part_115 line 970
  484. theorem OAI.CycleClique.certificate_1159_part_115_checked line 972
  485. def OAI.CycleClique.certificate_1159_part_114 line 974
  486. theorem OAI.CycleClique.certificate_1159_part_114_checked line 976
  487. def OAI.CycleClique.certificate_1159_part_118_E line 978
  488. def OAI.CycleClique.certificate_1159_part_118_M line 980
  489. def OAI.CycleClique.certificate_1159_part_119_E line 982
  490. def OAI.CycleClique.certificate_1159_part_119_M line 984
  491. def OAI.CycleClique.certificate_1159_part_120_E line 986
  492. def OAI.CycleClique.certificate_1159_part_120_M line 988
  493. def OAI.CycleClique.certificate_1159_part_121_E line 990
  494. def OAI.CycleClique.certificate_1159_part_121_M line 992
  495. def OAI.CycleClique.certificate_1159_part_121 line 994
  496. theorem OAI.CycleClique.certificate_1159_part_121_checked line 996
  497. def OAI.CycleClique.certificate_1159_part_120 line 998
  498. theorem OAI.CycleClique.certificate_1159_part_120_checked line 1000
  499. def OAI.CycleClique.certificate_1159_part_119 line 1002
  500. theorem OAI.CycleClique.certificate_1159_part_119_checked line 1004
  501. def OAI.CycleClique.certificate_1159_part_122_E line 1006
  502. def OAI.CycleClique.certificate_1159_part_122_M line 1008
  503. def OAI.CycleClique.certificate_1159_part_123_E line 1010
  504. def OAI.CycleClique.certificate_1159_part_123_M line 1012
  505. def OAI.CycleClique.certificate_1159_part_124_E line 1014
  506. def OAI.CycleClique.certificate_1159_part_124_M line 1016
  507. def OAI.CycleClique.certificate_1159_part_124 line 1018
  508. theorem OAI.CycleClique.certificate_1159_part_124_checked line 1020
  509. def OAI.CycleClique.certificate_1159_part_123 line 1022
  510. theorem OAI.CycleClique.certificate_1159_part_123_checked line 1024
  511. def OAI.CycleClique.certificate_1159_part_122 line 1026
  512. theorem OAI.CycleClique.certificate_1159_part_122_checked line 1028
  513. def OAI.CycleClique.certificate_1159_part_125_E line 1030
  514. def OAI.CycleClique.certificate_1159_part_125_M line 1032
  515. def OAI.CycleClique.certificate_1159_part_126_E line 1034
  516. def OAI.CycleClique.certificate_1159_part_126_M line 1036
  517. def OAI.CycleClique.certificate_1159_part_127_E line 1038
  518. def OAI.CycleClique.certificate_1159_part_127_M line 1040
  519. def OAI.CycleClique.certificate_1159_part_127 line 1042
  520. theorem OAI.CycleClique.certificate_1159_part_127_checked line 1044
  521. def OAI.CycleClique.certificate_1159_part_126 line 1046
  522. theorem OAI.CycleClique.certificate_1159_part_126_checked line 1048
  523. def OAI.CycleClique.certificate_1159_part_125 line 1050
  524. theorem OAI.CycleClique.certificate_1159_part_125_checked line 1052
  525. def OAI.CycleClique.certificate_1159_part_128_E line 1054
  526. def OAI.CycleClique.certificate_1159_part_128_M line 1056
  527. def OAI.CycleClique.certificate_1159_part_129_E line 1058
  528. def OAI.CycleClique.certificate_1159_part_129_M line 1060
  529. def OAI.CycleClique.certificate_1159_part_130_E line 1062
  530. def OAI.CycleClique.certificate_1159_part_130_M line 1064
  531. def OAI.CycleClique.certificate_1159_part_131_E line 1066
  532. def OAI.CycleClique.certificate_1159_part_131_M line 1068
  533. def OAI.CycleClique.certificate_1159_part_132_E line 1070
  534. def OAI.CycleClique.certificate_1159_part_132_M line 1072
  535. def OAI.CycleClique.certificate_1159_part_133_E line 1074
  536. def OAI.CycleClique.certificate_1159_part_133_M line 1076
  537. def OAI.CycleClique.certificate_1159_part_134_E line 1078
  538. def OAI.CycleClique.certificate_1159_part_134_M line 1080
  539. def OAI.CycleClique.certificate_1159_part_134 line 1082
  540. theorem OAI.CycleClique.certificate_1159_part_134_checked line 1084
  541. def OAI.CycleClique.certificate_1159_part_133 line 1086
  542. theorem OAI.CycleClique.certificate_1159_part_133_checked line 1088
  543. def OAI.CycleClique.certificate_1159_part_132 line 1090
  544. theorem OAI.CycleClique.certificate_1159_part_132_checked line 1092
  545. def OAI.CycleClique.certificate_1159_part_131 line 1094
  546. theorem OAI.CycleClique.certificate_1159_part_131_checked line 1096
  547. def OAI.CycleClique.certificate_1159_part_130 line 1098
  548. theorem OAI.CycleClique.certificate_1159_part_130_checked line 1100
  549. def OAI.CycleClique.certificate_1159_part_129 line 1102
  550. theorem OAI.CycleClique.certificate_1159_part_129_checked line 1104
  551. def OAI.CycleClique.certificate_1159_part_128 line 1106
  552. theorem OAI.CycleClique.certificate_1159_part_128_checked line 1108
  553. def OAI.CycleClique.certificate_1159_part_118 line 1110
  554. theorem OAI.CycleClique.certificate_1159_part_118_checked line 1112
  555. def OAI.CycleClique.certificate_1159_part_110 line 1114
  556. theorem OAI.CycleClique.certificate_1159_part_110_checked line 1116
  557. def OAI.CycleClique.certificate_1159_part_99 line 1118
  558. theorem OAI.CycleClique.certificate_1159_part_99_checked line 1120
  559. def OAI.CycleClique.certificate_1159_part_79 line 1122
  560. theorem OAI.CycleClique.certificate_1159_part_79_checked line 1124
  561. def OAI.CycleClique.certificate_1159_part_59 line 1126
  562. theorem OAI.CycleClique.certificate_1159_part_59_checked line 1128
  563. def OAI.CycleClique.certificate_1159_part_38 line 1130
  564. theorem OAI.CycleClique.certificate_1159_part_38_checked line 1132
  565. def OAI.CycleClique.certificate_1159_part_34 line 1134
  566. theorem OAI.CycleClique.certificate_1159_part_34_checked line 1136
  567. def OAI.CycleClique.certificate_1159_part_21 line 1138
  568. theorem OAI.CycleClique.certificate_1159_part_21_checked line 1140
  569. def OAI.CycleClique.certificate_1159_part_20 line 1142
  570. theorem OAI.CycleClique.certificate_1159_part_20_checked line 1144
  571. def OAI.CycleClique.certificate_1159_part_17 line 1146
  572. theorem OAI.CycleClique.certificate_1159_part_17_checked line 1148
  573. def OAI.CycleClique.certificate_1159_part_16 line 1150
  574. theorem OAI.CycleClique.certificate_1159_part_16_checked line 1152
  575. def OAI.CycleClique.certificate_1159_part_15 line 1154
  576. theorem OAI.CycleClique.certificate_1159_part_15_checked line 1156
  577. def OAI.CycleClique.certificate_1159_part_12 line 1158
  578. theorem OAI.CycleClique.certificate_1159_part_12_checked line 1160
  579. def OAI.CycleClique.certificate_1159_part_11 line 1162
  580. theorem OAI.CycleClique.certificate_1159_part_11_checked line 1164
  581. def OAI.CycleClique.certificate_1159_part_10 line 1166
  582. theorem OAI.CycleClique.certificate_1159_part_10_checked line 1168
  583. def OAI.CycleClique.certificate_1159_part_9 line 1170
  584. theorem OAI.CycleClique.certificate_1159_part_9_checked line 1172
  585. def OAI.CycleClique.certificate_1159_part_8 line 1174
  586. theorem OAI.CycleClique.certificate_1159_part_8_checked line 1176
  587. def OAI.CycleClique.certificate_1159_part_7 line 1178
  588. theorem OAI.CycleClique.certificate_1159_part_7_checked line 1180
  589. def OAI.CycleClique.certificate_1159_part_6 line 1182
  590. theorem OAI.CycleClique.certificate_1159_part_6_checked line 1184
  591. def OAI.CycleClique.certificate_1159_part_5 line 1186
  592. theorem OAI.CycleClique.certificate_1159_part_5_checked line 1188
  593. def OAI.CycleClique.certificate_1159_part_4 line 1190
  594. theorem OAI.CycleClique.certificate_1159_part_4_checked line 1192
  595. def OAI.CycleClique.certificate_1159_part_3 line 1194
  596. theorem OAI.CycleClique.certificate_1159_part_3_checked line 1196
  597. def OAI.CycleClique.certificate_1159_part_2 line 1198
  598. theorem OAI.CycleClique.certificate_1159_part_2_checked line 1200
  599. def OAI.CycleClique.certificate_1159_part_1 line 1202
  600. theorem OAI.CycleClique.certificate_1159_part_1_checked line 1204
  601. def OAI.CycleClique.certificate_1159 line 1206
  602. theorem OAI.CycleClique.certificate_1159_checked line 1208
  603. theorem OAI.CycleClique.certificate_1159_valid line 1210
  604. def OAI.CycleClique.certificate_1160_q line 1212
  605. def OAI.CycleClique.certificate_1160_edges line 1213
  606. def OAI.CycleClique.certificate_1160_part_0 line 1215
  607. def OAI.CycleClique.certificate_1160_part_1 line 1217
  608. def OAI.CycleClique.certificate_1160 line 1219
  609. theorem OAI.CycleClique.certificate_1160_checked line 1221
  610. theorem OAI.CycleClique.certificate_1160_valid line 1222
  611. def OAI.CycleClique.certificate_1161_q line 1224
  612. def OAI.CycleClique.certificate_1161_edges line 1225
  613. def OAI.CycleClique.certificate_1161_part_0 line 1227
  614. def OAI.CycleClique.certificate_1161_part_1 line 1229
  615. def OAI.CycleClique.certificate_1161_part_2 line 1231
  616. def OAI.CycleClique.certificate_1161_part_3 line 1233
  617. def OAI.CycleClique.certificate_1161 line 1235
  618. theorem OAI.CycleClique.certificate_1161_checked line 1237
  619. theorem OAI.CycleClique.certificate_1161_valid line 1238
  620. def OAI.CycleClique.certificate_1162_q line 1240
  621. def OAI.CycleClique.certificate_1162_edges line 1241
  622. def OAI.CycleClique.certificate_1162_part_0 line 1243
  623. def OAI.CycleClique.certificate_1162_part_1 line 1245
  624. def OAI.CycleClique.certificate_1162_part_2 line 1247
  625. def OAI.CycleClique.certificate_1162_part_3 line 1249
  626. def OAI.CycleClique.certificate_1162 line 1251
  627. theorem OAI.CycleClique.certificate_1162_checked line 1253
  628. theorem OAI.CycleClique.certificate_1162_valid line 1254
  629. def OAI.CycleClique.certificate_1163_q line 1256
  630. def OAI.CycleClique.certificate_1163_edges line 1257
  631. def OAI.CycleClique.certificate_1163_part_0 line 1259
  632. def OAI.CycleClique.certificate_1163_part_1 line 1261
  633. def OAI.CycleClique.certificate_1163_part_2 line 1263
  634. def OAI.CycleClique.certificate_1163_part_3 line 1265
  635. def OAI.CycleClique.certificate_1163 line 1267
  636. theorem OAI.CycleClique.certificate_1163_checked line 1269
  637. theorem OAI.CycleClique.certificate_1163_valid line 1270
  638. def OAI.CycleClique.certificate_1164_q line 1272
  639. def OAI.CycleClique.certificate_1164_edges line 1273
  640. def OAI.CycleClique.certificate_1164_part_0 line 1275
  641. def OAI.CycleClique.certificate_1164_part_1 line 1277
  642. def OAI.CycleClique.certificate_1164_part_2 line 1279
  643. def OAI.CycleClique.certificate_1164_part_3 line 1281
  644. def OAI.CycleClique.certificate_1164 line 1283
  645. theorem OAI.CycleClique.certificate_1164_checked line 1285
  646. theorem OAI.CycleClique.certificate_1164_valid line 1286
  647. def OAI.CycleClique.certificate_1165_q line 1288
  648. def OAI.CycleClique.certificate_1165_edges line 1289
  649. def OAI.CycleClique.certificate_1165_part_0 line 1291
  650. def OAI.CycleClique.certificate_1165_part_1 line 1293
  651. def OAI.CycleClique.certificate_1165_part_2 line 1295
  652. def OAI.CycleClique.certificate_1165_part_3 line 1297
  653. def OAI.CycleClique.certificate_1165 line 1299
  654. theorem OAI.CycleClique.certificate_1165_checked line 1301
  655. theorem OAI.CycleClique.certificate_1165_valid line 1302
  656. def OAI.CycleClique.certificate_1166_q line 1304
  657. def OAI.CycleClique.certificate_1166_edges line 1305
  658. def OAI.CycleClique.certificate_1166_part_0 line 1307
  659. def OAI.CycleClique.certificate_1166_part_1 line 1309
  660. def OAI.CycleClique.certificate_1166_part_2 line 1311
  661. def OAI.CycleClique.certificate_1166_part_3 line 1313
  662. def OAI.CycleClique.certificate_1166_part_4 line 1315
  663. def OAI.CycleClique.certificate_1166 line 1317
  664. theorem OAI.CycleClique.certificate_1166_checked line 1319
  665. theorem OAI.CycleClique.certificate_1166_valid line 1320
  666. def OAI.CycleClique.certificate_1167_q line 1322
  667. def OAI.CycleClique.certificate_1167_edges line 1323
  668. def OAI.CycleClique.certificate_1167_part_0 line 1325
  669. def OAI.CycleClique.certificate_1167_part_1 line 1327
  670. def OAI.CycleClique.certificate_1167_part_2 line 1329
  671. def OAI.CycleClique.certificate_1167_part_3 line 1331
  672. def OAI.CycleClique.certificate_1167 line 1333
  673. theorem OAI.CycleClique.certificate_1167_checked line 1335
  674. theorem OAI.CycleClique.certificate_1167_valid line 1336
  675. def OAI.CycleClique.certificate_1168_q line 1338
  676. def OAI.CycleClique.certificate_1168_edges line 1339
  677. def OAI.CycleClique.certificate_1168_part_0 line 1341
  678. def OAI.CycleClique.certificate_1168_part_1 line 1343
  679. def OAI.CycleClique.certificate_1168_part_2 line 1345
  680. def OAI.CycleClique.certificate_1168_part_3 line 1347
  681. def OAI.CycleClique.certificate_1168 line 1349
  682. theorem OAI.CycleClique.certificate_1168_checked line 1351
  683. theorem OAI.CycleClique.certificate_1168_valid line 1352
  684. def OAI.CycleClique.certificate_1169_q line 1354
  685. def OAI.CycleClique.certificate_1169_edges line 1355
  686. def OAI.CycleClique.certificate_1169_part_0 line 1357
  687. def OAI.CycleClique.certificate_1169_part_1 line 1359
  688. def OAI.CycleClique.certificate_1169_part_2 line 1361
  689. def OAI.CycleClique.certificate_1169_part_3 line 1363
  690. def OAI.CycleClique.certificate_1169 line 1365
  691. theorem OAI.CycleClique.certificate_1169_checked line 1367
  692. theorem OAI.CycleClique.certificate_1169_valid line 1368
  693. def OAI.CycleClique.certificate_1170_q line 1370
  694. def OAI.CycleClique.certificate_1170_edges line 1371
  695. def OAI.CycleClique.certificate_1170_part_0 line 1373
  696. def OAI.CycleClique.certificate_1170_part_1 line 1375
  697. def OAI.CycleClique.certificate_1170_part_2 line 1377
  698. def OAI.CycleClique.certificate_1170_part_3 line 1379
  699. def OAI.CycleClique.certificate_1170 line 1381
  700. theorem OAI.CycleClique.certificate_1170_checked line 1383
  701. theorem OAI.CycleClique.certificate_1170_valid line 1384
  702. def OAI.CycleClique.certificate_1171_q line 1386
  703. def OAI.CycleClique.certificate_1171_edges line 1387
  704. def OAI.CycleClique.certificate_1171_part_0 line 1389
  705. def OAI.CycleClique.certificate_1171_part_1 line 1391
  706. def OAI.CycleClique.certificate_1171_part_2 line 1393
  707. def OAI.CycleClique.certificate_1171_part_3 line 1395
  708. def OAI.CycleClique.certificate_1171_part_4 line 1397
  709. def OAI.CycleClique.certificate_1171 line 1399
  710. theorem OAI.CycleClique.certificate_1171_checked line 1401
  711. theorem OAI.CycleClique.certificate_1171_valid line 1402
  712. def OAI.CycleClique.certificate_1172_q line 1404
  713. def OAI.CycleClique.certificate_1172_edges line 1405
  714. def OAI.CycleClique.certificate_1172_part_0 line 1407
  715. def OAI.CycleClique.certificate_1172_part_1 line 1409
  716. def OAI.CycleClique.certificate_1172_part_2 line 1411
  717. def OAI.CycleClique.certificate_1172_part_3 line 1413
  718. def OAI.CycleClique.certificate_1172 line 1415
  719. theorem OAI.CycleClique.certificate_1172_checked line 1417
  720. theorem OAI.CycleClique.certificate_1172_valid line 1418
  721. def OAI.CycleClique.certificate_1173_q line 1420
  722. def OAI.CycleClique.certificate_1173_edges line 1421
  723. def OAI.CycleClique.certificate_1173_part_0 line 1423
  724. def OAI.CycleClique.certificate_1173_part_1 line 1425
  725. def OAI.CycleClique.certificate_1173_part_2 line 1427
  726. def OAI.CycleClique.certificate_1173_part_3 line 1429
  727. def OAI.CycleClique.certificate_1173 line 1431
  728. theorem OAI.CycleClique.certificate_1173_checked line 1433
  729. theorem OAI.CycleClique.certificate_1173_valid line 1434
  730. def OAI.CycleClique.certificate_1174_q line 1436
  731. def OAI.CycleClique.certificate_1174_edges line 1437
  732. def OAI.CycleClique.certificate_1174_part_0 line 1439
  733. def OAI.CycleClique.certificate_1174_part_1 line 1441
  734. def OAI.CycleClique.certificate_1174_part_2 line 1443
  735. def OAI.CycleClique.certificate_1174_part_3 line 1445
  736. def OAI.CycleClique.certificate_1174_part_4 line 1447
  737. def OAI.CycleClique.certificate_1174 line 1449
  738. theorem OAI.CycleClique.certificate_1174_checked line 1451
  739. theorem OAI.CycleClique.certificate_1174_valid line 1452
  740. def OAI.CycleClique.certificate_1175_q line 1454
  741. def OAI.CycleClique.certificate_1175_edges line 1456
  742. def OAI.CycleClique.certificate_1175_E line 1458
  743. def OAI.CycleClique.certificate_1175_M line 1460
  744. def OAI.CycleClique.certificate_1175_part_1_E line 1462
  745. def OAI.CycleClique.certificate_1175_part_1_M line 1464
  746. def OAI.CycleClique.certificate_1175_part_2_E line 1466
  747. def OAI.CycleClique.certificate_1175_part_2_M line 1468
  748. def OAI.CycleClique.certificate_1175_part_3_E line 1470
  749. def OAI.CycleClique.certificate_1175_part_3_M line 1472
  750. def OAI.CycleClique.certificate_1175_part_4_E line 1474
  751. def OAI.CycleClique.certificate_1175_part_4_M line 1476
  752. def OAI.CycleClique.certificate_1175_part_5_E line 1478
  753. def OAI.CycleClique.certificate_1175_part_5_M line 1480
  754. def OAI.CycleClique.certificate_1175_part_6_E line 1482
  755. def OAI.CycleClique.certificate_1175_part_6_M line 1484
  756. def OAI.CycleClique.certificate_1175_part_7_E line 1486
  757. def OAI.CycleClique.certificate_1175_part_7_M line 1488
  758. def OAI.CycleClique.certificate_1175_part_8_E line 1490
  759. def OAI.CycleClique.certificate_1175_part_8_M line 1492
  760. def OAI.CycleClique.certificate_1175_part_9_E line 1494
  761. def OAI.CycleClique.certificate_1175_part_9_M line 1496
  762. def OAI.CycleClique.certificate_1175_part_10_E line 1498
  763. def OAI.CycleClique.certificate_1175_part_10_M line 1500
  764. def OAI.CycleClique.certificate_1175_part_11_E line 1502
  765. def OAI.CycleClique.certificate_1175_part_11_M line 1504
  766. def OAI.CycleClique.certificate_1175_part_12_E line 1506
  767. def OAI.CycleClique.certificate_1175_part_12_M line 1508
  768. def OAI.CycleClique.certificate_1175_part_12 line 1510
  769. theorem OAI.CycleClique.certificate_1175_part_12_checked line 1512
  770. def OAI.CycleClique.certificate_1175_part_13_E line 1514
  771. def OAI.CycleClique.certificate_1175_part_13_M line 1516
  772. def OAI.CycleClique.certificate_1175_part_14_E line 1518
  773. def OAI.CycleClique.certificate_1175_part_14_M line 1520
  774. def OAI.CycleClique.certificate_1175_part_14 line 1522
  775. theorem OAI.CycleClique.certificate_1175_part_14_checked line 1524
  776. def OAI.CycleClique.certificate_1175_part_13 line 1526
  777. theorem OAI.CycleClique.certificate_1175_part_13_checked line 1528
  778. def OAI.CycleClique.certificate_1175_part_15_E line 1530
  779. def OAI.CycleClique.certificate_1175_part_15_M line 1532
  780. def OAI.CycleClique.certificate_1175_part_16_E line 1534
  781. def OAI.CycleClique.certificate_1175_part_16_M line 1536
  782. def OAI.CycleClique.certificate_1175_part_16 line 1538
  783. theorem OAI.CycleClique.certificate_1175_part_16_checked line 1540
  784. def OAI.CycleClique.certificate_1175_part_15 line 1542
  785. theorem OAI.CycleClique.certificate_1175_part_15_checked line 1544
  786. def OAI.CycleClique.certificate_1175_part_17_E line 1546
  787. def OAI.CycleClique.certificate_1175_part_17_M line 1548
  788. def OAI.CycleClique.certificate_1175_part_18_E line 1550
  789. def OAI.CycleClique.certificate_1175_part_18_M line 1552
  790. def OAI.CycleClique.certificate_1175_part_18 line 1554
  791. theorem OAI.CycleClique.certificate_1175_part_18_checked line 1556
  792. def OAI.CycleClique.certificate_1175_part_17 line 1558
  793. theorem OAI.CycleClique.certificate_1175_part_17_checked line 1560
  794. def OAI.CycleClique.certificate_1175_part_19_E line 1562
  795. def OAI.CycleClique.certificate_1175_part_19_M line 1564
  796. def OAI.CycleClique.certificate_1175_part_20_E line 1566
  797. def OAI.CycleClique.certificate_1175_part_20_M line 1568
  798. def OAI.CycleClique.certificate_1175_part_20 line 1570
  799. theorem OAI.CycleClique.certificate_1175_part_20_checked line 1572
  800. def OAI.CycleClique.certificate_1175_part_19 line 1574
  801. theorem OAI.CycleClique.certificate_1175_part_19_checked line 1576
  802. def OAI.CycleClique.certificate_1175_part_21_E line 1578
  803. def OAI.CycleClique.certificate_1175_part_21_M line 1580
  804. def OAI.CycleClique.certificate_1175_part_22_E line 1582
  805. def OAI.CycleClique.certificate_1175_part_22_M line 1584
  806. def OAI.CycleClique.certificate_1175_part_22 line 1586
  807. theorem OAI.CycleClique.certificate_1175_part_22_checked line 1588
  808. def OAI.CycleClique.certificate_1175_part_23_E line 1590
  809. def OAI.CycleClique.certificate_1175_part_23_M line 1592
  810. def OAI.CycleClique.certificate_1175_part_24_E line 1594
  811. def OAI.CycleClique.certificate_1175_part_24_M line 1596
  812. def OAI.CycleClique.certificate_1175_part_24 line 1598
  813. theorem OAI.CycleClique.certificate_1175_part_24_checked line 1600
  814. def OAI.CycleClique.certificate_1175_part_25_E line 1602
  815. def OAI.CycleClique.certificate_1175_part_25_M line 1604
  816. def OAI.CycleClique.certificate_1175_part_25 line 1606
  817. theorem OAI.CycleClique.certificate_1175_part_25_checked line 1608
  818. def OAI.CycleClique.certificate_1175_part_26_E line 1610
  819. def OAI.CycleClique.certificate_1175_part_26_M line 1612
  820. def OAI.CycleClique.certificate_1175_part_26 line 1614
  821. theorem OAI.CycleClique.certificate_1175_part_26_checked line 1616
  822. def OAI.CycleClique.certificate_1175_part_27_E line 1618
  823. def OAI.CycleClique.certificate_1175_part_27_M line 1620
  824. def OAI.CycleClique.certificate_1175_part_27 line 1622
  825. theorem OAI.CycleClique.certificate_1175_part_27_checked line 1624
  826. def OAI.CycleClique.certificate_1175_part_28_E line 1626
  827. def OAI.CycleClique.certificate_1175_part_28_M line 1628
  828. def OAI.CycleClique.certificate_1175_part_28 line 1630
  829. theorem OAI.CycleClique.certificate_1175_part_28_checked line 1632
  830. def OAI.CycleClique.certificate_1175_part_29_E line 1634
  831. def OAI.CycleClique.certificate_1175_part_29_M line 1636
  832. def OAI.CycleClique.certificate_1175_part_29 line 1638
  833. theorem OAI.CycleClique.certificate_1175_part_29_checked line 1640
  834. def OAI.CycleClique.certificate_1175_part_30_E line 1642
  835. def OAI.CycleClique.certificate_1175_part_30_M line 1644
  836. def OAI.CycleClique.certificate_1175_part_31_E line 1646
  837. def OAI.CycleClique.certificate_1175_part_31_M line 1648
  838. def OAI.CycleClique.certificate_1175_part_31 line 1650
  839. theorem OAI.CycleClique.certificate_1175_part_31_checked line 1652
  840. def OAI.CycleClique.certificate_1175_part_32_E line 1654
  841. def OAI.CycleClique.certificate_1175_part_32_M line 1656
  842. def OAI.CycleClique.certificate_1175_part_32 line 1658
  843. theorem OAI.CycleClique.certificate_1175_part_32_checked line 1660
  844. def OAI.CycleClique.certificate_1175_part_33_E line 1662
  845. def OAI.CycleClique.certificate_1175_part_33_M line 1664
  846. def OAI.CycleClique.certificate_1175_part_33 line 1666
  847. theorem OAI.CycleClique.certificate_1175_part_33_checked line 1668
  848. def OAI.CycleClique.certificate_1175_part_34_E line 1670
  849. def OAI.CycleClique.certificate_1175_part_34_M line 1672
  850. def OAI.CycleClique.certificate_1175_part_34 line 1674
  851. theorem OAI.CycleClique.certificate_1175_part_34_checked line 1676
  852. def OAI.CycleClique.certificate_1175_part_35_E line 1678
  853. def OAI.CycleClique.certificate_1175_part_35_M line 1680
  854. def OAI.CycleClique.certificate_1175_part_35 line 1682
  855. theorem OAI.CycleClique.certificate_1175_part_35_checked line 1684
  856. def OAI.CycleClique.certificate_1175_part_36_E line 1686
  857. def OAI.CycleClique.certificate_1175_part_36_M line 1688
  858. def OAI.CycleClique.certificate_1175_part_36 line 1690
  859. theorem OAI.CycleClique.certificate_1175_part_36_checked line 1692
  860. def OAI.CycleClique.certificate_1175_part_37_E line 1694
  861. def OAI.CycleClique.certificate_1175_part_37_M line 1696
  862. def OAI.CycleClique.certificate_1175_part_38_E line 1698
  863. def OAI.CycleClique.certificate_1175_part_38_M line 1700
  864. def OAI.CycleClique.certificate_1175_part_38 line 1702
  865. theorem OAI.CycleClique.certificate_1175_part_38_checked line 1704
  866. def OAI.CycleClique.certificate_1175_part_39_E line 1706
  867. def OAI.CycleClique.certificate_1175_part_39_M line 1708
  868. def OAI.CycleClique.certificate_1175_part_39 line 1710
  869. theorem OAI.CycleClique.certificate_1175_part_39_checked line 1712
  870. def OAI.CycleClique.certificate_1175_part_40_E line 1714
  871. def OAI.CycleClique.certificate_1175_part_40_M line 1716
  872. def OAI.CycleClique.certificate_1175_part_41_E line 1718
  873. def OAI.CycleClique.certificate_1175_part_41_M line 1720
  874. def OAI.CycleClique.certificate_1175_part_42_E line 1722
  875. def OAI.CycleClique.certificate_1175_part_42_M line 1724
  876. def OAI.CycleClique.certificate_1175_part_42 line 1726
  877. theorem OAI.CycleClique.certificate_1175_part_42_checked line 1728
  878. def OAI.CycleClique.certificate_1175_part_43_E line 1730
  879. def OAI.CycleClique.certificate_1175_part_43_M line 1732
  880. def OAI.CycleClique.certificate_1175_part_44_E line 1734
  881. def OAI.CycleClique.certificate_1175_part_44_M line 1736
  882. def OAI.CycleClique.certificate_1175_part_45_E line 1738
  883. def OAI.CycleClique.certificate_1175_part_45_M line 1740
  884. def OAI.CycleClique.certificate_1175_part_46_E line 1742
  885. def OAI.CycleClique.certificate_1175_part_46_M line 1744
  886. def OAI.CycleClique.certificate_1175_part_47_E line 1746
  887. def OAI.CycleClique.certificate_1175_part_47_M line 1748
  888. def OAI.CycleClique.certificate_1175_part_47 line 1750
  889. theorem OAI.CycleClique.certificate_1175_part_47_checked line 1752
  890. def OAI.CycleClique.certificate_1175_part_48_E line 1754
  891. def OAI.CycleClique.certificate_1175_part_48_M line 1756
  892. def OAI.CycleClique.certificate_1175_part_48 line 1758
  893. theorem OAI.CycleClique.certificate_1175_part_48_checked line 1760
  894. def OAI.CycleClique.certificate_1175_part_49_E line 1762
  895. def OAI.CycleClique.certificate_1175_part_49_M line 1764
  896. def OAI.CycleClique.certificate_1175_part_49 line 1766
  897. theorem OAI.CycleClique.certificate_1175_part_49_checked line 1768
  898. def OAI.CycleClique.certificate_1175_part_50_E line 1770
  899. def OAI.CycleClique.certificate_1175_part_50_M line 1772
  900. def OAI.CycleClique.certificate_1175_part_50 line 1774
  901. theorem OAI.CycleClique.certificate_1175_part_50_checked line 1776
  902. def OAI.CycleClique.certificate_1175_part_51_E line 1778
  903. def OAI.CycleClique.certificate_1175_part_51_M line 1780
  904. def OAI.CycleClique.certificate_1175_part_51 line 1782
  905. theorem OAI.CycleClique.certificate_1175_part_51_checked line 1784
  906. def OAI.CycleClique.certificate_1175_part_52_E line 1786
  907. def OAI.CycleClique.certificate_1175_part_52_M line 1788
  908. def OAI.CycleClique.certificate_1175_part_53_E line 1790
  909. def OAI.CycleClique.certificate_1175_part_53_M line 1792
  910. def OAI.CycleClique.certificate_1175_part_53 line 1794
  911. theorem OAI.CycleClique.certificate_1175_part_53_checked line 1796
  912. def OAI.CycleClique.certificate_1175_part_54_E line 1798
  913. def OAI.CycleClique.certificate_1175_part_54_M line 1800
  914. def OAI.CycleClique.certificate_1175_part_55_E line 1802
  915. def OAI.CycleClique.certificate_1175_part_55_M line 1804
  916. def OAI.CycleClique.certificate_1175_part_55 line 1806
  917. theorem OAI.CycleClique.certificate_1175_part_55_checked line 1808
  918. def OAI.CycleClique.certificate_1175_part_54 line 1810
  919. theorem OAI.CycleClique.certificate_1175_part_54_checked line 1812
  920. def OAI.CycleClique.certificate_1175_part_56_E line 1814
  921. def OAI.CycleClique.certificate_1175_part_56_M line 1816
  922. def OAI.CycleClique.certificate_1175_part_56 line 1818
  923. theorem OAI.CycleClique.certificate_1175_part_56_checked line 1820
  924. def OAI.CycleClique.certificate_1175_part_57_E line 1822
  925. def OAI.CycleClique.certificate_1175_part_57_M line 1824
  926. def OAI.CycleClique.certificate_1175_part_57 line 1826
  927. theorem OAI.CycleClique.certificate_1175_part_57_checked line 1828
  928. def OAI.CycleClique.certificate_1175_part_52 line 1830
  929. theorem OAI.CycleClique.certificate_1175_part_52_checked line 1832
  930. def OAI.CycleClique.certificate_1175_part_46 line 1834
  931. theorem OAI.CycleClique.certificate_1175_part_46_checked line 1836
  932. def OAI.CycleClique.certificate_1175_part_45 line 1838
  933. theorem OAI.CycleClique.certificate_1175_part_45_checked line 1840
  934. def OAI.CycleClique.certificate_1175_part_44 line 1842
  935. theorem OAI.CycleClique.certificate_1175_part_44_checked line 1844
  936. def OAI.CycleClique.certificate_1175_part_43 line 1846
  937. theorem OAI.CycleClique.certificate_1175_part_43_checked line 1848
  938. def OAI.CycleClique.certificate_1175_part_41 line 1850
  939. theorem OAI.CycleClique.certificate_1175_part_41_checked line 1852
  940. def OAI.CycleClique.certificate_1175_part_40 line 1854
  941. theorem OAI.CycleClique.certificate_1175_part_40_checked line 1856
  942. def OAI.CycleClique.certificate_1175_part_37 line 1858
  943. theorem OAI.CycleClique.certificate_1175_part_37_checked line 1860
  944. def OAI.CycleClique.certificate_1175_part_30 line 1862
  945. theorem OAI.CycleClique.certificate_1175_part_30_checked line 1864
  946. def OAI.CycleClique.certificate_1175_part_23 line 1866
  947. theorem OAI.CycleClique.certificate_1175_part_23_checked line 1868
  948. def OAI.CycleClique.certificate_1175_part_21 line 1870
  949. theorem OAI.CycleClique.certificate_1175_part_21_checked line 1872
  950. def OAI.CycleClique.certificate_1175_part_11 line 1874
  951. theorem OAI.CycleClique.certificate_1175_part_11_checked line 1876
  952. def OAI.CycleClique.certificate_1175_part_10 line 1878
  953. theorem OAI.CycleClique.certificate_1175_part_10_checked line 1880
  954. def OAI.CycleClique.certificate_1175_part_9 line 1882
  955. theorem OAI.CycleClique.certificate_1175_part_9_checked line 1884
  956. def OAI.CycleClique.certificate_1175_part_8 line 1886
  957. theorem OAI.CycleClique.certificate_1175_part_8_checked line 1888
  958. def OAI.CycleClique.certificate_1175_part_7 line 1890
  959. theorem OAI.CycleClique.certificate_1175_part_7_checked line 1892
  960. def OAI.CycleClique.certificate_1175_part_6 line 1894
  961. theorem OAI.CycleClique.certificate_1175_part_6_checked line 1896
  962. def OAI.CycleClique.certificate_1175_part_5 line 1898
  963. theorem OAI.CycleClique.certificate_1175_part_5_checked line 1900
  964. def OAI.CycleClique.certificate_1175_part_4 line 1902
  965. theorem OAI.CycleClique.certificate_1175_part_4_checked line 1904
  966. def OAI.CycleClique.certificate_1175_part_3 line 1906
  967. theorem OAI.CycleClique.certificate_1175_part_3_checked line 1908
  968. def OAI.CycleClique.certificate_1175_part_2 line 1910
  969. theorem OAI.CycleClique.certificate_1175_part_2_checked line 1912
  970. def OAI.CycleClique.certificate_1175_part_1 line 1914
  971. theorem OAI.CycleClique.certificate_1175_part_1_checked line 1916
  972. def OAI.CycleClique.certificate_1175 line 1918
  973. theorem OAI.CycleClique.certificate_1175_checked line 1920
  974. theorem OAI.CycleClique.certificate_1175_valid line 1922
  975. def OAI.CycleClique.certificate_1176_q line 1924
  976. def OAI.CycleClique.certificate_1176_edges line 1925
  977. def OAI.CycleClique.certificate_1176_part_0 line 1927
  978. def OAI.CycleClique.certificate_1176_part_1 line 1929
  979. def OAI.CycleClique.certificate_1176 line 1931
  980. theorem OAI.CycleClique.certificate_1176_checked line 1933
  981. theorem OAI.CycleClique.certificate_1176_valid line 1934
  982. def OAI.CycleClique.certificate_1177_q line 1936
  983. def OAI.CycleClique.certificate_1177_edges line 1937
  984. def OAI.CycleClique.certificate_1177_part_0 line 1939
  985. def OAI.CycleClique.certificate_1177_part_1 line 1941
  986. def OAI.CycleClique.certificate_1177_part_2 line 1943
  987. def OAI.CycleClique.certificate_1177_part_3 line 1945
  988. def OAI.CycleClique.certificate_1177 line 1947
  989. theorem OAI.CycleClique.certificate_1177_checked line 1949
  990. theorem OAI.CycleClique.certificate_1177_valid line 1950
  991. def OAI.CycleClique.certificate_1178_q line 1952
  992. def OAI.CycleClique.certificate_1178_edges line 1953
  993. def OAI.CycleClique.certificate_1178_part_0 line 1955
  994. def OAI.CycleClique.certificate_1178_part_1 line 1957
  995. def OAI.CycleClique.certificate_1178_part_2 line 1959
  996. def OAI.CycleClique.certificate_1178_part_3 line 1961
  997. def OAI.CycleClique.certificate_1178 line 1963
  998. theorem OAI.CycleClique.certificate_1178_checked line 1965
  999. theorem OAI.CycleClique.certificate_1178_valid line 1966
  1000. def OAI.CycleClique.certificate_1179_q line 1968
  1001. def OAI.CycleClique.certificate_1179_edges line 1969
  1002. def OAI.CycleClique.certificate_1179_part_0 line 1971
  1003. def OAI.CycleClique.certificate_1179_part_1 line 1973
  1004. def OAI.CycleClique.certificate_1179_part_2 line 1975
  1005. def OAI.CycleClique.certificate_1179_part_3 line 1977
  1006. def OAI.CycleClique.certificate_1179 line 1979
  1007. theorem OAI.CycleClique.certificate_1179_checked line 1981
  1008. theorem OAI.CycleClique.certificate_1179_valid line 1982
  1009. def OAI.CycleClique.certificate_1180_q line 1984
  1010. def OAI.CycleClique.certificate_1180_edges line 1985
  1011. def OAI.CycleClique.certificate_1180_part_0 line 1987
  1012. def OAI.CycleClique.certificate_1180_part_1 line 1989
  1013. def OAI.CycleClique.certificate_1180_part_2 line 1991
  1014. def OAI.CycleClique.certificate_1180_part_3 line 1993
  1015. def OAI.CycleClique.certificate_1180 line 1995
  1016. theorem OAI.CycleClique.certificate_1180_checked line 1997
  1017. theorem OAI.CycleClique.certificate_1180_valid line 1998
  1018. def OAI.CycleClique.certificate_1181_q line 2000
  1019. def OAI.CycleClique.certificate_1181_edges line 2001
  1020. def OAI.CycleClique.certificate_1181_part_0 line 2003
  1021. def OAI.CycleClique.certificate_1181_part_1 line 2005
  1022. def OAI.CycleClique.certificate_1181_part_2 line 2007
  1023. def OAI.CycleClique.certificate_1181_part_3 line 2009
  1024. def OAI.CycleClique.certificate_1181 line 2011
  1025. theorem OAI.CycleClique.certificate_1181_checked line 2013
  1026. theorem OAI.CycleClique.certificate_1181_valid line 2014
  1027. def OAI.CycleClique.certificate_1182_q line 2016
  1028. def OAI.CycleClique.certificate_1182_edges line 2017
  1029. def OAI.CycleClique.certificate_1182_part_0 line 2019
  1030. def OAI.CycleClique.certificate_1182_part_1 line 2021
  1031. def OAI.CycleClique.certificate_1182_part_2 line 2023
  1032. def OAI.CycleClique.certificate_1182_part_3 line 2025
  1033. def OAI.CycleClique.certificate_1182 line 2027
  1034. theorem OAI.CycleClique.certificate_1182_checked line 2029
  1035. theorem OAI.CycleClique.certificate_1182_valid line 2030
  1036. def OAI.CycleClique.certificate_1183_q line 2032
  1037. def OAI.CycleClique.certificate_1183_edges line 2033
  1038. def OAI.CycleClique.certificate_1183_part_0 line 2035
  1039. def OAI.CycleClique.certificate_1183_part_1 line 2037
  1040. def OAI.CycleClique.certificate_1183_part_2 line 2039
  1041. def OAI.CycleClique.certificate_1183_part_3 line 2041
  1042. def OAI.CycleClique.certificate_1183 line 2043
  1043. theorem OAI.CycleClique.certificate_1183_checked line 2045
  1044. theorem OAI.CycleClique.certificate_1183_valid line 2046