[1] complete lists of combinatorial 3-spheres
  n = 5: 1 complexes, certified 3-spheres on 5 vertices: 1, pairwise non-isomorphic: True (canonical forms computed for 0), with an LC edge: 0  [0s]
  n = 6: 2 complexes, certified 3-spheres on 6 vertices: 2, pairwise non-isomorphic: True (canonical forms computed for 0), with an LC edge: 2  [0s]
  n = 7: 5 complexes, certified 3-spheres on 7 vertices: 5, pairwise non-isomorphic: True (canonical forms computed for 0), with an LC edge: 5  [0s]
  n = 8: 39 complexes, certified 3-spheres on 8 vertices: 39, pairwise non-isomorphic: True (canonical forms computed for 0), with an LC edge: 39  [0s]
  n = 9: 1296 complexes, certified 3-spheres on 9 vertices: 1296, pairwise non-isomorphic: True (canonical forms computed for 38), with an LC edge: 1296  [0s]
  n = 10: 247882 complexes, certified 3-spheres on 10 vertices: 247882, pairwise non-isomorphic: True (canonical forms computed for 8730), with an LC edge: 246562  [39s]
  n = 10: f_1 distribution [(30, 30), (31, 124), (32, 385), (33, 952), (34, 2142), (35, 4340), (36, 8106), (37, 13853), (38, 21702), (39, 30526), (40, 38553), (41, 42498), (42, 39299), (43, 28087), (44, 13745), (45, 3540)]
  n = 10: neighborly spheres: 3540; with a vertex-transitive automorphism group: 3, (|Aut|, number of LC edges) = [(20, 10), (20, 5), (10, 0)]
  n = 10: spheres without an LC edge: 1320
[2] the ten-vertex 3-spheres without an LC edge
  extension certificates verified: 1320 of 1320  [1s]
  prime (no missing tetrahedron): 1320; with a stacked vertex link (Lemma H applies): 1318; others: lines [27137, 35806]
[3] combinatorial 4-spheres with at most 9 vertices (finder's lists)
  n = 6: 1 complexes, certified 4-spheres on 6 vertices: 1, pairwise non-isomorphic: True, with an LC edge: 0
  n = 7: 2 complexes, certified 4-spheres on 7 vertices: 2, pairwise non-isomorphic: True, with an LC edge: 2
  n = 8: 8 complexes, certified 4-spheres on 8 vertices: 8, pairwise non-isomorphic: True, with an LC edge: 8
  n = 9: 337 complexes, certified 4-spheres on 9 vertices: 337, pairwise non-isomorphic: True, with an LC edge: 337
[4] special spheres
  A10    {'n': 10, 'fvector': [10, 45, 70, 35], 'sphere': True, 'cyclic': True, 'neighborly': True, 'lc_edges': 0, 'stacked_links': [], 'missing_tetrahedra': 0}
  A11    {'n': 11, 'fvector': [11, 55, 88, 44], 'sphere': True, 'cyclic': True, 'neighborly': True, 'lc_edges': 0, 'stacked_links': [], 'missing_tetrahedra': 0}
  Z13_0  {'n': 13, 'fvector': [13, 78, 130, 65], 'sphere': True, 'cyclic': True, 'neighborly': True, 'lc_edges': 0, 'stacked_links': [], 'missing_tetrahedra': 0}
  Z13_1  {'n': 13, 'fvector': [13, 78, 130, 65], 'sphere': True, 'cyclic': True, 'neighborly': True, 'lc_edges': 0, 'stacked_links': [], 'missing_tetrahedra': 0}
  Z14_0  {'n': 14, 'fvector': [14, 91, 154, 77], 'sphere': True, 'cyclic': True, 'neighborly': True, 'lc_edges': 0, 'stacked_links': [], 'missing_tetrahedra': 0}
  Z14_1  {'n': 14, 'fvector': [14, 91, 154, 77], 'sphere': True, 'cyclic': True, 'neighborly': True, 'lc_edges': 0, 'stacked_links': [], 'missing_tetrahedra': 0}
  Z14_2  {'n': 14, 'fvector': [14, 91, 154, 77], 'sphere': True, 'cyclic': True, 'neighborly': True, 'lc_edges': 0, 'stacked_links': [], 'missing_tetrahedra': 0}
  Z14_3  {'n': 14, 'fvector': [14, 91, 154, 77], 'sphere': True, 'cyclic': True, 'neighborly': True, 'lc_edges': 0, 'stacked_links': [], 'missing_tetrahedra': 0}
  Z14_4  {'n': 14, 'fvector': [14, 91, 154, 77], 'sphere': True, 'cyclic': True, 'neighborly': True, 'lc_edges': 0, 'stacked_links': [], 'missing_tetrahedra': 0}
  Z14_5  {'n': 14, 'fvector': [14, 91, 154, 77], 'sphere': True, 'cyclic': True, 'neighborly': True, 'lc_edges': 0, 'stacked_links': [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13], 'missing_tetrahedra': 0}
  Z14_6  {'n': 14, 'fvector': [14, 91, 154, 77], 'sphere': True, 'cyclic': True, 'neighborly': True, 'lc_edges': 0, 'stacked_links': [], 'missing_tetrahedra': 0}
  Z14_7  {'n': 14, 'fvector': [14, 91, 154, 77], 'sphere': True, 'cyclic': True, 'neighborly': True, 'lc_edges': 0, 'stacked_links': [], 'missing_tetrahedra': 0}
  Z14_8  {'n': 14, 'fvector': [14, 91, 154, 77], 'sphere': True, 'cyclic': True, 'neighborly': True, 'lc_edges': 0, 'stacked_links': [], 'missing_tetrahedra': 0}
  neighborly, no stacked vertex link => no completable antistar: ['A10', 'A11', 'Z13_0', 'Z13_1', 'Z14_0', 'Z14_1', 'Z14_2', 'Z14_3', 'Z14_4', 'Z14_6', 'Z14_7', 'Z14_8']
  the ten-vertex spheres without LC edge and without stacked link: lines [27137, 35806] ; isomorphic to A10: [35806]
  the vertex-transitive neighborly 10-vertex sphere without LC edge is isomorphic to A10: [True]
  Prop.-B certificate for ten-vertex line 27137 (vertex 0): True
  A10    certificates (cover / kind, verified): [(None, True), ([0, 1], True), ([0, 5], True)]
  A11    certificates (cover / kind, verified): [(None, True), ([0, 1, 2], True), ([0, 1, 3], True), ([0, 1, 4], True), ([0, 1, 5], True), ([0, 1, 6], True), ([0, 1, 7], True), ([0, 1, 8], True), ([0, 2, 4], True), ([0, 2, 5], True), ([0, 2, 6], True), ([0, 2, 7], True), ([0, 2, 8], True), ([0, 3, 6], True), ([0, 3, 7], True)]
  Z13_0  certificates (cover / kind, verified): [(None, True)]
  Z13_1  certificates (cover / kind, verified): [([0, 1, 11], True)]
  Z14_0  certificates (cover / kind, verified): [(None, True)]
  Z14_1  certificates (cover / kind, verified): []
  Z14_2  certificates (cover / kind, verified): [(None, True)]
  Z14_3  certificates (cover / kind, verified): []
  Z14_4  certificates (cover / kind, verified): [(None, True)]
  Z14_5  certificates (cover / kind, verified): [('propB v=0', True)]
  Z14_6  certificates (cover / kind, verified): []
  Z14_7  certificates (cover / kind, verified): [(None, True)]
  Z14_8  certificates (cover / kind, verified): [(None, True)]
  A11: verified extensions in which every facet meets a 3-set: 14 (3-sets [[0, 1, 2], [0, 1, 3], [0, 1, 4], [0, 1, 5], [0, 1, 6], [0, 1, 7], [0, 1, 8], [0, 2, 4], [0, 2, 5], [0, 2, 6], [0, 2, 7], [0, 2, 8], [0, 3, 6], [0, 3, 7]])
  spheres with a verified extension: ['A10', 'A11', 'Z13_0', 'Z13_1', 'Z14_0', 'Z14_2', 'Z14_4', 'Z14_5', 'Z14_7', 'Z14_8']
  spheres without a known extension: ['Z14_1', 'Z14_3', 'Z14_6']
  pair form A10 {0,1}: relaxation satisfiable (CNF identical: True)
  pair form A10 {0,2}: CNF 3330 vars / 37749 clauses (identical: True); DRUP proof with 24 lemmas: True (empty clause reached) [0.1s]
  pair form A10 {0,3}: CNF 3330 vars / 37741 clauses (identical: True); DRUP proof with 286 lemmas: True (empty clause reached) [0.3s]
  pair form A10 {0,4}: CNF 3330 vars / 37737 clauses (identical: True); DRUP proof with 286 lemmas: True (empty clause reached) [0.3s]
  pair form A10 {0,5}: relaxation satisfiable (CNF identical: True)
  pair form A11 {0,1}: CNF 5985 vars / 88513 clauses (identical: True); DRUP proof with 160 lemmas: True (empty clause reached) [0.3s]
  pair form A11 {0,2}: CNF 5985 vars / 88517 clauses (identical: True); DRUP proof with 100 lemmas: True (empty clause reached) [0.2s]
  pair form A11 {0,3}: CNF 5985 vars / 88517 clauses (identical: True); DRUP proof with 130 lemmas: True (empty clause reached) [0.2s]
  pair form A11 {0,4}: CNF 5985 vars / 88505 clauses (identical: True); DRUP proof with 420 lemmas: True (empty clause reached) [0.6s]
  pair form A11 {0,5}: CNF 5985 vars / 88509 clauses (identical: True); DRUP proof with 219 lemmas: True (empty clause reached) [0.3s]
  pair form Z13_0 {0,1}: CNF 15777 vars / 380386 clauses (identical: True); DRUP proof with 1029 lemmas: True (empty clause reached) [2.8s]
  pair form Z13_0 {0,2}: CNF 15777 vars / 380378 clauses (identical: True); DRUP proof with 3161 lemmas: True (empty clause reached) [7.9s]
  pair form Z13_0 {0,3}: CNF 15777 vars / 380370 clauses (identical: True); DRUP proof with 8949 lemmas: True (empty clause reached) [24.6s]
  pair form Z13_0 {0,4}: CNF 15777 vars / 380382 clauses (identical: True); DRUP proof with 1654 lemmas: True (empty clause reached) [3.9s]
  pair form Z13_0 {0,5}: CNF 15777 vars / 380374 clauses (identical: True); DRUP proof with 2188 lemmas: True (empty clause reached) [6.2s]
  pair form Z13_0 {0,6}: CNF 15777 vars / 380378 clauses (identical: True); DRUP proof with 964 lemmas: True (empty clause reached) [2.6s]
  pair form Z13_1 {0,1}: CNF 15777 vars / 380378 clauses (identical: True); DRUP proof with 955 lemmas: True (empty clause reached) [2.3s]
  pair form Z13_1 {0,2}: CNF 15777 vars / 380370 clauses (identical: True); DRUP proof with 819 lemmas: True (empty clause reached) [2.3s]
  pair form Z13_1 {0,3}: CNF 15777 vars / 380374 clauses (identical: True); DRUP proof with 3652 lemmas: True (empty clause reached) [8.1s]
  pair form Z13_1 {0,4}: CNF 15777 vars / 380382 clauses (identical: True); DRUP proof with 1177 lemmas: True (empty clause reached) [2.9s]
  pair form Z13_1 {0,5}: CNF 15777 vars / 380382 clauses (identical: True); DRUP proof with 2055 lemmas: True (empty clause reached) [4.9s]
  pair form Z13_1 {0,6}: CNF 15777 vars / 380382 clauses (identical: True); DRUP proof with 347 lemmas: True (empty clause reached) [1.2s]
  A10: verified extensions with every facet meeting a pair: [[0, 1], [0, 5]]
  orbit search n = 10: (sphere, Z_n-invariant, neighborly, #LC edges) = [(True, True, True, 0), (True, True, True, 10)]
  orbit search n = 11: (sphere, Z_n-invariant, neighborly, #LC edges) = [(True, True, True, 0), (True, True, True, 11)]
  orbit search n = 12: (sphere, Z_n-invariant, neighborly, #LC edges) = [(True, True, True, 12)]
  orbit search n = 13: (sphere, Z_n-invariant, neighborly, #LC edges) = [(True, True, True, 0), (True, True, True, 0), (True, True, True, 13)]
  orbit search n = 14: (sphere, Z_n-invariant, neighborly, #LC edges) = [(True, True, True, 0), (True, True, True, 0), (True, True, True, 0), (True, True, True, 0), (True, True, True, 0), (True, True, True, 0), (True, True, True, 0), (True, True, True, 0), (True, True, True, 0), (True, True, True, 14)]
[5] negative controls
  neighborly closed 3-manifolds with 9 and 10 vertices that are not spheres: 138, accepted as spheres: 0
  corrupted extension certificates accepted (facet removed / false cover / wrong sphere): [False, False, False]
  proof of A10 {0,2} accepted for the satisfiable A10 {0,1} CNF: False; empty proof accepted: False
total time 144s
ALL CHECKS PASSED
