PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:20:4.5:0.95:100.opb
MD5SUM	f82b685b64af240616b701a750c82883
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	10
Optimality of the best value was proved	NO
Number of terms in the objective function	934
Biggest coefficient in the objective function	546
Number of bits for the biggest coefficient in the objective function	10
Sum of the numbers in the objective function	2594
Number of bits of the sum of numbers in the objective function	12
Biggest number in a constraint	546
Number of bits of the biggest number in a constraint	10
Biggest sum of numbers in a constraint	2594
Number of bits of the biggest sum of numbers	12
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03784
Number of variables	934
Total number of constraints	1996
Number of constraints which are clauses	879
Number of constraints which are cardinality constraints (but not clauses)	1117
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	20
Trace number 6042

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc27 THE 2005-04-14 03:13:55 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4503 boxname=wulflinc27 idbench=367 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f82b685b64af240616b701a750c82883  /oldhome/oroussel/tmp/wulflinc27/normalized-10:20:4.5:0.95:100.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc27/normalized-10:20:4.5:0.95:100.opb /oldhome/oroussel/tmp/wulflinc27/normalized-10:20:4.5:0.95:100.opb
IDLAUNCH: 4503
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        842420 kB
Buffers:         35056 kB
Cached:         120224 kB
SwapCached:       3160 kB
Active:          69628 kB
Inactive:        91632 kB
HighTotal:      131008 kB
HighFree:         7392 kB
LowTotal:       903652 kB
LowFree:        835028 kB
SwapTotal:     2097892 kB
SwapFree:      2094732 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            25308 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 03:33:57 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 4503 7 1200.23 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1062 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[ 190]---> BDD-cost:   11
c ---[ 189]---> BDD-cost:   11
c ---[ 188]---> BDD-cost:   17
c ---[ 187]---> BDD-cost:   20
c ---[ 186]---> BDD-cost:   20
c ---[ 185]---> BDD-cost:   17
c ---[ 184]---> BDD-cost:   23
c ---[ 183]---> BDD-cost:   26
c ---[ 182]---> BDD-cost:   23
c ---[ 181]---> BDD-cost:   17
c ---[ 180]---> BDD-cost:   23
c ---[ 179]---> BDD-cost:   17
c ---[ 178]---> BDD-cost:   17
c ---[ 177]---> BDD-cost:   17
c ---[ 176]---> BDD-cost:   17
c ---[ 175]---> BDD-cost:   11
c ---[ 174]---> BDD-cost:    5
c ---[ 173]---> BDD-cost:   14
c ---[ 172]---> BDD-cost:   17
c ---[ 171]---> BDD-cost:   23
c ---[ 170]---> BDD-cost:   21
c ---[ 169]---> BDD-cost:   29
c ---[ 168]---> BDD-cost:   26
c ---[ 167]---> BDD-cost:   26
c ---[ 166]---> BDD-cost:   27
c ---[ 165]---> BDD-cost:   38
c ---[ 164]---> BDD-cost:   29
c ---[ 163]---> BDD-cost:   29
c ---[ 162]---> BDD-cost:   26
c ---[ 161]---> BDD-cost:   23
c ---[ 160]---> BDD-cost:   20
c ---[ 159]---> BDD-cost:   20
c ---[ 158]---> BDD-cost:   17
c ---[ 156]---> BDD-cost:   20
c ---[ 155]---> BDD-cost:   23
c ---[ 154]---> BDD-cost:   26
c ---[ 153]---> BDD-cost:   32
c ---[ 152]---> BDD-cost:   35
c ---[ 151]---> BDD-cost:   29
c ---[ 150]---> BDD-cost:   41
c ---[ 149]---> BDD-cost:   38
c ---[ 148]---> BDD-cost:   36
c ---[ 147]---> BDD-cost:   32
c ---[ 146]---> BDD-cost:   32
c ---[ 145]---> BDD-cost:   29
c ---[ 144]---> BDD-cost:   29
c ---[ 143]---> BDD-cost:   26
c ---[ 142]---> BDD-cost:   26
c ---[ 141]---> BDD-cost:   13
c ---[ 140]---> BDD-cost:    9
c ---[ 138]---> BDD-cost:    7
c ---[ 136]---> BDD-cost:   21
c ---[ 135]---> BDD-cost:   29
c ---[ 134]---> BDD-cost:   35
c ---[ 133]---> BDD-cost:   32
c ---[ 132]---> BDD-cost:   44
c ---[ 131]---> BDD-cost:   44
c ---[ 130]---> BDD-cost:   44
c ---[ 129]---> BDD-cost:   38
c ---[ 128]---> BDD-cost:   38
c ---[ 127]---> BDD-cost:   32
c ---[ 126]---> BDD-cost:   35
c ---[ 125]---> BDD-cost:   32
c ---[ 124]---> BDD-cost:   38
c ---[ 123]---> BDD-cost:   32
c ---[ 122]---> BDD-cost:   26
c ---[ 121]---> BDD-cost:   20
c ---[ 120]---> BDD-cost:   18
c ---[ 118]---> BDD-cost:    7
c ---[ 117]---> BDD-cost:    5
c ---[ 116]---> BDD-cost:   29
c ---[ 115]---> BDD-cost:   32
c ---[ 114]---> BDD-cost:   38
c ---[ 113]---> BDD-cost:   44
c ---[ 112]---> BDD-cost:   50
c ---[ 111]---> BDD-cost:   41
c ---[ 110]---> BDD-cost:   42
c ---[ 109]---> BDD-cost:   38
c ---[ 108]---> BDD-cost:   41
c ---[ 107]---> BDD-cost:   35
c ---[ 106]---> BDD-cost:   38
c ---[ 105]---> BDD-cost:   38
c ---[ 104]---> BDD-cost:   35
c ---[ 103]---> BDD-cost:   32
c ---[ 102]---> BDD-cost:   26
c ---[ 101]---> BDD-cost:   23
c ---[ 100]---> BDD-cost:   26
c ---[  99]---> BDD-cost:   17
c ---[  98]---> BDD-cost:   17
c ---[  97]---> BDD-cost:    5
c ---[  96]---> BDD-cost:   23
c ---[  95]---> BDD-cost:   35
c ---[  94]---> BDD-cost:   41
c ---[  93]---> BDD-cost:   41
c ---[  92]---> BDD-cost:   47
c ---[  91]---> BDD-cost:   50
c ---[  90]---> BDD-cost:   53
c ---[  89]---> BDD-cost:   47
c ---[  88]---> BDD-cost:   38
c ---[  87]---> BDD-cost:   38
c ---[  86]---> BDD-cost:   35
c ---[  85]---> BDD-cost:   32
c ---[  84]---> BDD-cost:   32
c ---[  83]---> BDD-cost:   29
c ---[  82]---> BDD-cost:   32
c ---[  81]---> BDD-cost:   32
c ---[  80]---> BDD-cost:   26
c ---[  79]---> BDD-cost:   20
c ---[  78]---> BDD-cost:   14
c ---[  77]---> BDD-cost:    8
c ---[  76]---> BDD-cost:   23
c ---[  75]---> BDD-cost:   29
c ---[  74]---> BDD-cost:   32
c ---[  73]---> BDD-cost:   41
c ---[  72]---> BDD-cost:   41
c ---[  71]---> BDD-cost:   47
c ---[  70]---> BDD-cost:   44
c ---[  69]---> BDD-cost:   44
c ---[  68]---> BDD-cost:   26
c ---[  67]---> BDD-cost:   32
c ---[  66]---> BDD-cost:   32
c ---[  65]---> BDD-cost:   32
c ---[  64]---> BDD-cost:   33
c ---[  63]---> BDD-cost:   32
c ---[  62]---> BDD-cost:   26
c ---[  61]---> BDD-cost:   29
c ---[  60]---> BDD-cost:   23
c ---[  59]---> BDD-cost:   20
c ---[  58]---> BDD-cost:   14
c ---[  57]---> BDD-cost:    5
c ---[  56]---> BDD-cost:   17
c ---[  55]---> BDD-cost:   26
c ---[  54]---> BDD-cost:   23
c ---[  53]---> BDD-cost:   29
c ---[  52]---> BDD-cost:   32
c ---[  51]---> BDD-cost:   38
c ---[  50]---> BDD-cost:   32
c ---[  49]---> BDD-cost:   35
c ---[  48]---> BDD-cost:   26
c ---[  47]---> BDD-cost:   26
c ---[  46]---> BDD-cost:   26
c ---[  45]---> BDD-cost:   29
c ---[  44]---> BDD-cost:   26
c ---[  43]---> BDD-cost:   29
c ---[  42]---> BDD-cost:   20
c ---[  41]---> BDD-cost:   20
c ---[  40]---> BDD-cost:   14
c ---[  39]---> BDD-cost:   18
c ---[  36]---> BDD-cost:   11
c ---[  35]---> BDD-cost:   17
c ---[  34]---> BDD-cost:   20
c ---[  33]---> BDD-cost:   23
c ---[  32]---> BDD-cost:   26
c ---[  31]---> BDD-cost:   29
c ---[  30]---> BDD-cost:   23
c ---[  29]---> BDD-cost:   26
c ---[  28]---> BDD-cost:   20
c ---[  27]---> BDD-cost:   23
c ---[  26]---> BDD-cost:   26
c ---[  25]---> BDD-cost:   26
c ---[  24]---> BDD-cost:   14
c ---[  23]---> BDD-cost:   14
c ---[  22]---> BDD-cost:   14
c ---[  21]---> BDD-cost:   15
c ---[  20]---> BDD-cost:    9
c ---[  18]---> BDD-cost:    5
c ---[  17]---> BDD-cost:   14
c ---[  16]---> BDD-cost:   14
c ---[  15]---> BDD-cost:   23
c ---[  14]---> BDD-cost:   20
c ---[  13]---> BDD-cost:   20
c ---[  12]---> BDD-cost:   17
c ---[  11]---> BDD-cost:   20
c ---[  10]---> BDD-cost:   17
c ---[   9]---> BDD-cost:   20
c ---[   8]---> BDD-cost:   11
c ---[   7]---> BDD-cost:   17
c ---[   6]---> BDD-cost:   14
c ---[   5]---> BDD-cost:   14
c ---[   4]---> BDD-cost:   14
c ---[   3]---> BDD-cost:    7
c ---[   2]---> BDD-cost:    8
c ---[   1]---> BDD-cost:    7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   11765    33737 |    3921       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 1032[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:70091     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  134745   321365 |   44915       0        0     nan |  0.000 % |
c |       101 |  134745   321365 |   49406     101      378     3.7 |  0.289 % |
c |       254 |  134745   321365 |   54347     254     1916     7.5 |  0.289 % |
c ==============================================================================
c [1mFound solution: 418[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       475 |  138441   330391 |   46147     472     3230     6.8 |  0.289 % |
c |       578 |  137873   329108 |   50761     564     3993     7.1 |  0.705 % |
c |       728 |  137788   328915 |   55837     711     4630     6.5 |  0.743 % |
c |       953 |  137788   328915 |   61421     936     9551    10.2 |  0.743 % |
c |      1291 |  137788   328915 |   67563    1274    13069    10.3 |  0.743 % |
c |      1797 |  137676   328664 |   74320    1779    23364    13.1 |  0.816 % |
c ==============================================================================
c [1mFound solution: 307[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2138 |  137959   329532 |   45986    2119    25259    11.9 |  0.816 % |
c |      2238 |  137959   329532 |   50584    2219    25773    11.6 |  0.865 % |
c ==============================================================================
c [1mFound solution: 159[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2254 |  138434   330777 |   46144    2235    25833    11.6 |  0.865 % |
c ==============================================================================
c [1mFound solution: 152[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2288 |  138490   330942 |   46163    2269    26896    11.9 |  0.865 % |
c |      2388 |  138445   330851 |   50779    2367    29840    12.6 |  0.898 % |
c |      2540 |  138236   330378 |   55857    2515    33411    13.3 |  1.013 % |
c |      2767 |  138236   330378 |   61442    2742    36817    13.4 |  1.013 % |
c ==============================================================================
c [1mFound solution: 107[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2941 |  138428   330891 |   46142    2916    38539    13.2 |  1.013 % |
c |      3041 |  138428   330891 |   50756    3016    40777    13.5 |  1.013 % |
c |      3192 |  138396   330824 |   55831    3165    42582    13.5 |  1.036 % |
c |      3417 |  138191   330372 |   61415    3383    46110    13.6 |  1.160 % |
c |      3755 |  138191   330372 |   67556    3721    49457    13.3 |  1.160 % |
c |      4261 |  137973   329869 |   74312    4216    55318    13.1 |  1.283 % |
c |      5021 |  137973   329869 |   81743    4976    75261    15.1 |  1.283 % |
c |      6160 |  137632   329105 |   89917    6100    90791    14.9 |  1.508 % |
c |      7868 |  137539   328894 |   98909    7805   110430    14.1 |  1.548 % |
c |     10430 |  137496   328803 |  108800   10365   155438    15.0 |  1.584 % |
c |     14275 |  137222   328193 |  119680   14202   275898    19.4 |  1.783 % |
c |     20041 |  137201   328148 |  131648   19967   704798    35.3 |  1.801 % |
c |     28692 |  137197   328139 |  144813   28613   996862    34.8 |  1.802 % |
c ==============================================================================
c [1mFound solution: 88[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34974 |  137098   327977 |   45699   34729  1135011    32.7 |  1.802 % |
c |     35074 |  136972   327695 |   50268   34826  1135981    32.6 |  2.051 % |
c |     35224 |  136972   327695 |   55295   34976  1137159    32.5 |  2.051 % |
c |     35449 |  136937   327620 |   60825   35198  1138927    32.4 |  2.081 % |
c |     35786 |  136937   327620 |   66907   35535  1149633    32.4 |  2.081 % |
c |     36294 |  136937   327620 |   73598   36043  1156248    32.1 |  2.081 % |
c |     37053 |  136937   327620 |   80958   36802  1254425    34.1 |  2.081 % |
c ==============================================================================
c [1mFound solution: 82[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37832 |  136969   327715 |   45656   37581  1268442    33.8 |  2.081 % |
c |     37932 |  136969   327715 |   50221   37681  1268959    33.7 |  2.082 % |
c |     38082 |  136969   327715 |   55243   37831  1271895    33.6 |  2.082 % |
c |     38307 |  136969   327715 |   60768   38056  1273306    33.5 |  2.082 % |
c |     38645 |  136878   327506 |   66844   38390  1280523    33.4 |  2.125 % |
c |     39151 |  136707   327110 |   73529   38894  1286713    33.1 |  2.235 % |
c |     39910 |  136664   327019 |   80882   39652  1301996    32.8 |  2.270 % |
c |     41049 |  136630   326945 |   88970   40691  1321509    32.5 |  2.300 % |
c |     42758 |  136630   326945 |   97867   42400  1363954    32.2 |  2.300 % |
c |     45320 |  136630   326945 |  107654   44962  1451229    32.3 |  2.300 % |
c |     49164 |  136306   326216 |  118419   48769  1554071    31.9 |  2.484 % |
c |     54932 |  136306   326216 |  130261   54537  1926766    35.3 |  2.484 % |
c |     63582 |  136306   326216 |  143288   63187  2438273    38.6 |  2.484 % |
c ==============================================================================
c [1mFound solution: 77[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     75735 |  136126   325854 |   45375   75325  3553417    47.2 |  2.484 % |
c |     75835 |  136126   325854 |   49912   20862  1157455    55.5 |  2.637 % |
c |     75987 |  136104   325804 |   54903   21007  1158369    55.1 |  2.646 % |
c |     76212 |  136104   325804 |   60394   21232  1161236    54.7 |  2.646 % |
c |     76550 |  136104   325804 |   66433   21570  1166658    54.1 |  2.646 % |
c |     77056 |  136104   325804 |   73076   22076  1203230    54.5 |  2.646 % |
c |     77816 |  136104   325804 |   80384   22836  1215601    53.2 |  2.646 % |
c |     78955 |  136104   325804 |   88423   23975  1238001    51.6 |  2.646 % |
c |     80663 |  136104   325804 |   97265   25683  1261960    49.1 |  2.646 % |
c |     83225 |  136104   325804 |  106991   28245  1330287    47.1 |  2.646 % |
c ==============================================================================
c [1mFound solution: 74[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     83353 |  136111   325827 |   45370   28373  1332445    47.0 |  2.646 % |
c |     83455 |  136111   325827 |   49907   28475  1335456    46.9 |  2.647 % |
c |     83605 |  136111   325827 |   54897   28625  1341423    46.9 |  2.647 % |
c |     83830 |  136111   325827 |   60387   28850  1344077    46.6 |  2.647 % |
c |     84167 |  136111   325827 |   66426   29187  1349710    46.2 |  2.647 % |
c |     84678 |  136111   325827 |   73068   29698  1354687    45.6 |  2.647 % |
c |     85438 |  136111   325827 |   80375   30458  1385841    45.5 |  2.647 % |
c |     86578 |  136111   325827 |   88413   31598  1470539    46.5 |  2.647 % |
c |     88289 |  136111   325827 |   97254   33309  1509109    45.3 |  2.647 % |
c |     90851 |  136111   325827 |  106980   35871  1574590    43.9 |  2.647 % |
c |     94696 |  136101   325804 |  117678   39713  1653312    41.6 |  2.652 % |
c |    100462 |  136101   325804 |  129445   45479  2632354    57.9 |  2.652 % |
c |    109112 |  136101   325804 |  142390   54129  3093113    57.1 |  2.652 % |
c ==============================================================================
c [1mFound solution: 65[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    113671 |  136179   326029 |   45393   58688  3937613    67.1 |  2.652 % |
c |    113771 |  136179   326029 |   49932   19316  1305290    67.6 |  2.651 % |
c |    113922 |  136179   326029 |   54925   19467  1308808    67.2 |  2.651 % |
c |    114147 |  136179   326029 |   60418   19692  1327557    67.4 |  2.651 % |
c |    114487 |  136106   325864 |   66459   20031  1335002    66.6 |  2.682 % |
c |    114993 |  136106   325864 |   73105   20537  1351714    65.8 |  2.682 % |
c |    115752 |  136106   325864 |   80416   21296  1374179    64.5 |  2.682 % |
c |    116894 |  136106   325864 |   88458   22438  1418701    63.2 |  2.682 % |
c |    118602 |  136106   325864 |   97303   24146  1569573    65.0 |  2.682 % |
c |    121164 |  136034   325706 |  107034   26665  1664717    62.4 |  2.746 % |
c |    125008 |  135980   325582 |  117737   30508  1739829    57.0 |  2.773 % |
c |    130775 |  135948   325509 |  129511   36267  1862330    51.4 |  2.786 % |
c |    139426 |  135948   325509 |  142462   44918  3368859    75.0 |  2.786 % |
c |    152400 |  135893   325384 |  156708   57883  4159349    71.9 |  2.838 % |
c |    171861 |  135893   325384 |  172379   77344  5629384    72.8 |  2.838 % |
c |    201053 |  135893   325384 |  189617  106536  7633114    71.6 |  2.838 % |
c ==============================================================================
c [1mFound solution: 50[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    229232 |  135966   325588 |   45322  134715 12974184    96.3 |  2.838 % |
c |    229334 |  135966   325588 |   49854   22269  3043851   136.7 |  2.838 % |
c |    229485 |  135966   325588 |   54839   22420  3045543   135.8 |  2.838 % |
c |    229712 |  135966   325588 |   60323   22647  3049706   134.7 |  2.838 % |
c |    230052 |  135966   325588 |   66355   22987  3055255   132.9 |  2.838 % |
c |    230558 |  135966   325588 |   72991   23493  3069007   130.6 |  2.838 % |
c |    231317 |  135966   325588 |   80290   24252  3104267   128.0 |  2.838 % |
c |    232458 |  135966   325588 |   88319   25393  3151730   124.1 |  2.838 % |
c |    234166 |  135870   325356 |   97151   27098  3218727   118.8 |  2.916 % |
c |    236728 |  135870   325356 |  106866   29660  3316097   111.8 |  2.916 % |
c |    240572 |  135870   325356 |  117553   33504  3454662   103.1 |  2.916 % |
c |    246338 |  135862   325337 |  129308   39265  3778497    96.2 |  2.921 % |
c |    254987 |  135862   325337 |  142239   47914  4054928    84.6 |  2.921 % |
c |    267963 |  135862   325337 |  156463   60890  4689436    77.0 |  2.921 % |
c |    287424 |  135862   325337 |  172110   80351  5759564    71.7 |  2.921 % |
c |    316616 |  135862   325337 |  189321  109543  7019224    64.1 |  2.921 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -v853 v782 -v197 v102 v21 -v2 -v855 v103 -v1 -v785 -v384 v272 -v196 v20 -v3 -v856 -v786 -v76 -v55 v23 v4 -v383 v275 -v202 v75 -v54 -v11 -v763 v387 v276 -v200 -v56 -v24 -v5 -v762 v247 -v150 v77 -v57 -v26 -v6 -v764 -v613 v388 -v201 -v79 v58 -v39 -v27 -v7 -v765 -v612 v513 -v250 -v205 -v149 -v65 v38 -v766 -v618 -v251 -v80 v59 v40 -v773 -v617 v512 -v326 -v155 -v125 -v82 v60 v41 -v767 -v619 -v153 -v83 v61 v42 -v768 -v623 v593 -v573 v518 -v128 v49 -v769 -v622 -v577 v516 -v154 -v129 v43 v729 -v620 -v596 -v576 -v158 v44 -v621 -v597 v517 v45 -v881 v728 v521 -v852 v781 -v192 v104 -v17 -v857 -v787 -v537 -v468 v271 -v198 v22 -v14 -v541 -v71 v25 -v15 -v859 -v385 v277 -v203 -v108 v70 -v29 -v10 -v860 v389 -v28 -v790 v246 -v206 -v145 v78 -v68 -v8 -v204 -v81 -v69 -v811 -v776 -v638 -v508 v391 -v322 -v280 -v252 v151 -v85 -v64 -v777 -v642 -v614 -v392 -v84 -v772 -v615 v514 -v325 -v156 v124 -v62 -v52 -v616 -v53 -v770 -v627 v592 v519 -v255 -v159 v130 -v48 -v572 -v157 -v877 v598 -v574 v522 -v46 -v578 v520 -v880 v730 -v133 -v601 -v854 v783 -v464 v267 v105 -v13 -v858 -v379 -v191 -v16 -v12 -v862 -v788 v536 -v488 -v467 -v378 v273 -v193 v109 -v18 -v861 -v540 -v492 -v199 v107 v19 -v791 -v386 v278 -v242 -v195 -v67 v33 -v789 v390 -v207 v72 -v66 -v807 -v775 v394 -v301 -v281 v248 v73 -v9 -v774 v393 -v279 v144 v74 -v810 -v637 -v321 -v253 v146 -v120 v89 -v51 -v641 v507 v152 -v50 -v630 v588 v509 -v327 -v256 v148 v126 -v63 -v631 v515 -v254 -v160 -v771 -v626 v594 v511 v131 -v725 v523 -v876 -v724 -v709 -v624 v599 -v330 v134 -v47 -v575 v132 -v882 v731 -v602 -v586 -v600 v582 -v900 v732 v581 v904 -v733 -v851 -v779 -v463 -v422 v106 -v850 v784 -v426 v266 v110 -v866 v780 -v662 v538 -v487 -v469 v268 -v177 -v36 -v792 -v666 -v542 -v491 v380 v274 -v194 -v37 v381 -v297 v270 -v222 -v215 v32 v382 -v282 v241 -v226 -v211 -v806 v544 -v472 -v398 -v317 -v300 v243 -v210 -v92 v30 -v545 v249 -v93 -v812 -v639 -v629 -v323 v245 -v88 -v643 -v628 v257 v147 -v119 -v913 -v836 -v328 v168 -v121 -v86 -v917 v587 v510 v164 v127 -v872 -v815 -v705 v645 v589 -v531 -v347 -v331 v163 v123 v646 v595 v527 -v351 -v329 v135 -v878 -v708 -v625 v591 -v583 v526 -v726 v603 -v585 -v95 v883 v727 -v94 -v899 v884 -v737 v579 v903 v885 -v869 -v533 -v465 v421 -v173 v118 -v35 -v870 v778 -v425 -v114 -v34 -v865 v800 v661 v539 -v489 -v470 -v212 -v176 -v113 -v796 -v665 -v543 -v493 v269 -v214 -v863 -v802 -v795 v547 -v473 -v450 -v401 -v296 v290 -v221 -v91 -v633 v546 -v471 -v402 -v286 -v225 -v90 -v808 -v632 -v495 -v397 -v302 -v285 -v208 v31 -v496 -v316 v244 -v832 v813 -v752 v640 -v395 -v318 -v265 -v209 v165 -v644 -v324 v261 v167 -v912 -v835 -v816 v648 -v528 v320 -v305 -v260 -v87 -v916 -v814 v647 -v530 -v332 -v122 -v704 -v346 v161 -v143 -v871 v590 -v584 -v350 -v139 -v873 -v710 v611 v524 v162 -v138 v879 -v607 v875 v740 -v606 -v561 v525 v886 v741 -v565 -v96 -v901 -v736 -v713 v580 v97 v905 -v867 v797 -v484 -v461 v423 -v172 -v117 v799 -v532 -v466 -v427 -v213 v663 -v534 -v490 v462 -v446 -v400 -v292 -v287 -v178 -v111 -v667 v535 v494 v474 -v399 -v289 -v864 -v793 v551 v498 -v449 -v429 -v298 -v223 -v112 -v801 -v497 -v430 -v227 -v803 -v794 -v748 -v687 -v669 v303 -v283 -v262 v181 v809 v691 -v670 -v634 -v264 v166 -v831 v805 -v751 -v635 -v396 v306 -v284 -v229 -v817 v636 -v529 -v319 v304 -v230 -v914 -v837 v700 -v652 -v340 -v258 -v140 -v918 v336 -v142 -v706 -v608 -v348 v335 -v259 -v610 -v352 -v920 -v840 v739 v711 -v412 -v371 -v136 -v921 -v896 v874 v738 -v375 -v895 v894 -v714 -v604 -v560 v354 -v137 v890 -v712 -v564 -v355 v902 v889 -v734 -v605 v100 v906 v101 -v868 v798 v658 v424 -v174 -v115 -v483 v460 -v428 -v288 -v217 v664 -v554 -v485 v482 -v445 -v432 -v216 -v179 v668 -v555 v486 v478 -v431 -v291 -v672 -v550 v502 -v477 -v451 -v293 v224 v182 -v671 v299 -v263 v228 v180 -v827 -v747 -v686 -v548 v295 v232 v908 -v804 v690 v307 -v231 v907 -v833 -v825 -v753 v655 -v454 -v337 -v821 v656 -v342 -v339 -v141 -v915 v838 -v820 -v651 -v341 -v919 v699 -v609 -v923 v841 -v756 v701 -v649 -v408 -v349 v333 -v922 v839 -v707 -v353 v891 v703 -v411 -v370 v357 v334 v893 -v715 -v374 v356 -v562 v99 -v897 -v566 v98 v898 v887 -v735 #### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.93 0.98 0.92 2/54 24156
Raw data (stat): 24156 (runsolver) R 24155 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481262926 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.94 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 5655 0 0 0 983 14 0 0 25 0 1 0 481262926 29663232 5477 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7242 5477 603 41 0 7201 0
vsize: 28968
[startup+20.0011 s]
Raw data (loadavg): 0.95 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 5774 0 0 0 1982 15 0 0 25 0 1 0 481262926 30244864 5596 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7384 5596 603 41 0 7343 0
vsize: 29536
[startup+30.0021 s]
Raw data (loadavg): 0.95 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 5970 0 0 0 2980 16 0 0 25 0 1 0 481262926 31055872 5792 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7582 5792 603 41 0 7541 0
vsize: 30328
[startup+40.0019 s]
Raw data (loadavg): 0.96 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 6247 0 0 0 3980 17 0 0 25 0 1 0 481262926 32227328 6069 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7868 6069 603 41 0 7827 0
vsize: 31472
[startup+50.0024 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 6569 0 0 0 4979 18 0 0 25 0 1 0 481262926 33431552 6391 4294967295 134512640 134672761 3221224544 3221223648 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8162 6392 603 41 0 8121 0
vsize: 32648
[startup+60.0025 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 6846 0 0 0 5978 19 0 0 25 0 1 0 481262926 34627584 6668 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8454 6668 603 41 0 8413 0
vsize: 33816
[startup+70.0024 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 6993 0 0 0 6978 19 0 0 25 0 1 0 481262926 35287040 6815 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8615 6815 603 41 0 8574 0
vsize: 34460
[startup+80.0029 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 7155 0 0 0 7978 20 0 0 25 0 1 0 481262926 35958784 6977 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8779 6977 603 41 0 8738 0
vsize: 35116
[startup+90.003 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 7243 0 0 0 8978 20 0 0 25 0 1 0 481262926 36356096 7065 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8876 7065 603 41 0 8835 0
vsize: 35504
[startup+100.004 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 7420 0 0 0 9977 21 0 0 25 0 1 0 481262926 37023744 7242 4294967295 134512640 134672761 3221224544 3221223808 134562196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9039 7242 603 41 0 8998 0
vsize: 36156
[startup+110.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 7550 0 0 0 10975 22 0 0 25 0 1 0 481262926 37564416 7372 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9171 7372 603 41 0 9130 0
vsize: 36684
[startup+120.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 7752 0 0 0 11975 22 0 0 25 0 1 0 481262926 38371328 7574 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9368 7574 603 41 0 9327 0
vsize: 37472
[startup+130.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 8003 0 0 0 12974 23 0 0 25 0 1 0 481262926 39309312 7825 4294967295 134512640 134672761 3221224544 3221223712 134561027 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9597 7825 603 41 0 9556 0
vsize: 38388
[startup+140.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 8222 0 0 0 13974 24 0 0 25 0 1 0 481262926 40239104 8044 4294967295 134512640 134672761 3221224544 3221223680 134560703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9824 8044 603 41 0 9783 0
vsize: 39296
[startup+150.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 8439 0 0 0 14973 25 0 0 25 0 1 0 481262926 41050112 8261 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10022 8261 603 41 0 9981 0
vsize: 40088
[startup+160.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 8640 0 0 0 15973 26 0 0 25 0 1 0 481262926 41979904 8462 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10249 8462 603 41 0 10208 0
vsize: 40996
[startup+170.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 9100 0 0 0 16972 27 0 0 25 0 1 0 481262926 44118016 8922 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10771 8922 603 41 0 10730 0
vsize: 43084
[startup+180.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 9269 0 0 0 17971 27 0 0 25 0 1 0 481262926 44785664 9091 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10934 9091 603 41 0 10893 0
vsize: 43736
[startup+190.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 9516 0 0 0 18971 28 0 0 25 0 1 0 481262926 45727744 9338 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11164 9338 603 41 0 11123 0
vsize: 44656
[startup+200.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 9794 0 0 0 19970 29 0 0 25 0 1 0 481262926 46931968 9616 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11458 9616 603 41 0 11417 0
vsize: 45832
[startup+210.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 9812 0 0 0 20970 29 0 0 25 0 1 0 481262926 46931968 9634 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11458 9634 603 41 0 11417 0
vsize: 45832
[startup+220.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 9812 0 0 0 21970 29 0 0 25 0 1 0 481262926 46931968 9634 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11458 9634 603 41 0 11417 0
vsize: 45832
[startup+230.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 9812 0 0 0 22971 29 0 0 25 0 1 0 481262926 46931968 9634 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11458 9634 603 41 0 11417 0
vsize: 45832
[startup+240.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 9812 0 0 0 23971 29 0 0 25 0 1 0 481262926 46931968 9634 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11458 9634 603 41 0 11417 0
vsize: 45832
[startup+250.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 9812 0 0 0 24971 29 0 0 25 0 1 0 481262926 46931968 9634 4294967295 134512640 134672761 3221224544 3221223648 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11458 9634 603 41 0 11417 0
vsize: 45832
[startup+260.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 9812 0 0 0 25971 29 0 0 25 0 1 0 481262926 46931968 9634 4294967295 134512640 134672761 3221224544 3221223648 134560148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11458 9634 603 41 0 11417 0
vsize: 45832
[startup+270.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 9812 0 0 0 26971 29 0 0 25 0 1 0 481262926 46931968 9634 4294967295 134512640 134672761 3221224544 3221223648 134560051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11458 9634 603 41 0 11417 0
vsize: 45832
[startup+280.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 9812 0 0 0 27971 29 0 0 25 0 1 0 481262926 46931968 9634 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11458 9634 603 41 0 11417 0
vsize: 45832
[startup+290.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 9812 0 0 0 28971 29 0 0 25 0 1 0 481262926 46931968 9634 4294967295 134512640 134672761 3221224544 3221223712 134561266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11458 9634 603 41 0 11417 0
vsize: 45832
[startup+300.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 9812 0 0 0 29972 29 0 0 25 0 1 0 481262926 46931968 9634 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11458 9634 603 41 0 11417 0
vsize: 45832
[startup+310.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 9877 0 0 0 30971 30 0 0 25 0 1 0 481262926 47194112 9699 4294967295 134512640 134672761 3221224544 3221223680 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11522 9699 603 41 0 11481 0
vsize: 46088
[startup+320.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 10293 0 0 0 31971 30 0 0 25 0 1 0 481262926 48926720 10115 4294967295 134512640 134672761 3221224544 3221223728 134559415 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11945 10115 603 41 0 11904 0
vsize: 47780
[startup+330.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 10293 0 0 0 32971 31 0 0 25 0 1 0 481262926 48926720 10115 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11945 10115 603 41 0 11904 0
vsize: 47780
[startup+340.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 10293 0 0 0 33971 31 0 0 25 0 1 0 481262926 48926720 10115 4294967295 134512640 134672761 3221224544 3221223728 134559463 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11945 10115 603 41 0 11904 0
vsize: 47780
[startup+350.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 10293 0 0 0 34971 31 0 0 25 0 1 0 481262926 48926720 10115 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11945 10115 603 41 0 11904 0
vsize: 47780
[startup+360.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 10293 0 0 0 35972 31 0 0 25 0 1 0 481262926 48926720 10115 4294967295 134512640 134672761 3221224544 3221223688 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11945 10115 603 41 0 11904 0
vsize: 47780
[startup+370.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 10293 0 0 0 36971 31 0 0 25 0 1 0 481262926 48926720 10115 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11945 10115 603 41 0 11904 0
vsize: 47780
[startup+380.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 10293 0 0 0 37972 31 0 0 25 0 1 0 481262926 48926720 10115 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11945 10115 603 41 0 11904 0
vsize: 47780
[startup+390.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 10293 0 0 0 38972 31 0 0 25 0 1 0 481262926 48926720 10115 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11945 10115 603 41 0 11904 0
vsize: 47780
[startup+400.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 10293 0 0 0 39972 31 0 0 25 0 1 0 481262926 48926720 10115 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11945 10115 603 41 0 11904 0
vsize: 47780
[startup+410.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 10293 0 0 0 40972 31 0 0 25 0 1 0 481262926 48926720 10115 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11945 10115 603 41 0 11904 0
vsize: 47780
[startup+420.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 10293 0 0 0 41972 31 0 0 25 0 1 0 481262926 48926720 10115 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11945 10115 603 41 0 11904 0
vsize: 47780
[startup+430.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 10359 0 0 0 42972 32 0 0 25 0 1 0 481262926 49197056 10181 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12011 10181 603 41 0 11970 0
vsize: 48044
[startup+440.017 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 10519 0 0 0 43971 32 0 0 25 0 1 0 481262926 49872896 10341 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12176 10341 603 41 0 12135 0
vsize: 48704
[startup+450.017 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 10700 0 0 0 44971 33 0 0 25 0 1 0 481262926 50548736 10522 4294967295 134512640 134672761 3221224544 3221223728 134559028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12341 10522 603 41 0 12300 0
vsize: 49364
[startup+460.017 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 10998 0 0 0 45970 34 0 0 25 0 1 0 481262926 51748864 10820 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12634 10820 603 41 0 12593 0
vsize: 50536
[startup+470.017 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 11277 0 0 0 46969 35 0 0 25 0 1 0 481262926 52957184 11099 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12929 11099 603 41 0 12888 0
vsize: 51716
[startup+480.018 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 11555 0 0 0 47969 36 0 0 25 0 1 0 481262926 54038528 11377 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13193 11377 603 41 0 13152 0
vsize: 52772
[startup+490.019 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 11819 0 0 0 48967 37 0 0 25 0 1 0 481262926 55119872 11641 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13457 11641 603 41 0 13416 0
vsize: 53828
[startup+500.019 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 12071 0 0 0 49967 38 0 0 25 0 1 0 481262926 56197120 11893 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13720 11893 603 41 0 13679 0
vsize: 54880
[startup+510.019 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 12276 0 0 0 50967 38 0 0 25 0 1 0 481262926 56999936 12098 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13916 12098 603 41 0 13875 0
vsize: 55664
[startup+520.019 s]
Raw data (loadavg): 1.10 1.02 0.93 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 12490 0 0 0 51966 40 0 0 25 0 1 0 481262926 57946112 12312 4294967295 134512640 134672761 3221224544 3221223712 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14147 12312 603 41 0 14106 0
vsize: 56588
[startup+530.02 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 12769 0 0 0 52965 41 0 0 25 0 1 0 481262926 59023360 12591 4294967295 134512640 134672761 3221224544 3221223744 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14410 12591 603 41 0 14369 0
vsize: 57640
[startup+540.02 s]
Raw data (loadavg): 1.07 1.01 0.93 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 13044 0 0 0 53964 41 0 0 25 0 1 0 481262926 60096512 12866 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14672 12866 603 41 0 14631 0
vsize: 58688
[startup+550.019 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 13314 0 0 0 54964 42 0 0 25 0 1 0 481262926 61304832 13136 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14967 13136 603 41 0 14926 0
vsize: 59868
[startup+560.021 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 13598 0 0 0 55963 43 0 0 25 0 1 0 481262926 62377984 13420 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15229 13420 603 41 0 15188 0
vsize: 60916
[startup+570.02 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 13870 0 0 0 56962 45 0 0 25 0 1 0 481262926 63442944 13692 4294967295 134512640 134672761 3221224544 3221223744 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15489 13692 603 41 0 15448 0
vsize: 61956
[startup+580.021 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 14098 0 0 0 57961 45 0 0 25 0 1 0 481262926 64376832 13920 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15717 13920 603 41 0 15676 0
vsize: 62868
[startup+590.022 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 14319 0 0 0 58960 46 0 0 25 0 1 0 481262926 65318912 14141 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15947 14141 603 41 0 15906 0
vsize: 63788
[startup+600.022 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 14512 0 0 0 59960 47 0 0 25 0 1 0 481262926 66113536 14334 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16141 14334 603 41 0 16100 0
vsize: 64564
[startup+610.022 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 14667 0 0 0 60960 47 0 0 25 0 1 0 481262926 66789376 14489 4294967295 134512640 134672761 3221224544 3221223648 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16306 14489 603 41 0 16265 0
vsize: 65224
[startup+620.023 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 14953 0 0 0 61959 48 0 0 25 0 1 0 481262926 67862528 14775 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16568 14775 603 41 0 16527 0
vsize: 66272
[startup+630.023 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 15187 0 0 0 62958 49 0 0 25 0 1 0 481262926 68800512 15009 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16797 15009 603 41 0 16756 0
vsize: 67188
[startup+640.023 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 15472 0 0 0 63958 50 0 0 25 0 1 0 481262926 70000640 15294 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17090 15294 603 41 0 17049 0
vsize: 68360
[startup+650.023 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 15775 0 0 0 64957 51 0 0 25 0 1 0 481262926 71217152 15597 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17387 15597 603 41 0 17346 0
vsize: 69548
[startup+660.024 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 16117 0 0 0 65955 53 0 0 25 0 1 0 481262926 72560640 15939 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17715 15939 603 41 0 17674 0
vsize: 70860
[startup+670.023 s]
Raw data (loadavg): 1.08 1.02 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 16411 0 0 0 66955 53 0 0 25 0 1 0 481262926 73768960 16233 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18010 16234 603 41 0 17969 0
vsize: 72040
[startup+680.023 s]
Raw data (loadavg): 1.07 1.02 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 16642 0 0 0 67954 54 0 0 25 0 1 0 481262926 74715136 16464 4294967295 134512640 134672761 3221224544 3221223688 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18241 16464 603 41 0 18200 0
vsize: 72964
[startup+690.024 s]
Raw data (loadavg): 1.06 1.02 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 16944 0 0 0 68954 55 0 0 25 0 1 0 481262926 76062720 16766 4294967295 134512640 134672761 3221224544 3221223648 134559890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18570 16766 603 41 0 18529 0
vsize: 74280
[startup+700.024 s]
Raw data (loadavg): 1.05 1.02 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 17290 0 0 0 69953 56 0 0 25 0 1 0 481262926 77410304 17112 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18899 17112 603 41 0 18858 0
vsize: 75596
[startup+710.025 s]
Raw data (loadavg): 1.04 1.01 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 17656 0 0 0 70952 57 0 0 25 0 1 0 481262926 78884864 17478 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19259 17478 603 41 0 19218 0
vsize: 77036
[startup+720.025 s]
Raw data (loadavg): 1.04 1.01 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 18082 0 0 0 71951 58 0 0 25 0 1 0 481262926 80613376 17904 4294967295 134512640 134672761 3221224544 3221223604 1075346557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19681 17904 603 41 0 19640 0
vsize: 78724
[startup+730.025 s]
Raw data (loadavg): 1.03 1.01 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 18511 0 0 0 72950 60 0 0 25 0 1 0 481262926 82358272 18333 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20107 18333 603 41 0 20066 0
vsize: 80428
[startup+740.025 s]
Raw data (loadavg): 1.02 1.01 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 18826 0 0 0 73949 61 0 0 25 0 1 0 481262926 83701760 18648 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20435 18648 603 41 0 20394 0
vsize: 81740
[startup+750.025 s]
Raw data (loadavg): 1.02 1.01 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 19020 0 0 0 74949 61 0 0 25 0 1 0 481262926 84508672 18842 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20632 18842 603 41 0 20591 0
vsize: 82528
[startup+760.026 s]
Raw data (loadavg): 1.02 1.01 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 19380 0 0 0 75947 62 0 0 25 0 1 0 481262926 86507520 19202 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21120 19202 603 41 0 21079 0
vsize: 84480
[startup+770.026 s]
Raw data (loadavg): 1.01 1.01 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 19732 0 0 0 76947 63 0 0 25 0 1 0 481262926 87846912 19554 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21447 19555 603 41 0 21406 0
vsize: 85788
[startup+780.027 s]
Raw data (loadavg): 1.01 1.01 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20026 0 0 0 77947 64 0 0 25 0 1 0 481262926 89055232 19848 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21742 19848 603 41 0 21701 0
vsize: 86968
[startup+790.027 s]
Raw data (loadavg): 1.01 1.01 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 78946 64 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+800.027 s]
Raw data (loadavg): 1.01 1.01 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 79946 64 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+810.027 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 80946 64 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223448 1075351112 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+820.027 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 81946 64 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223648 134560318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+830.028 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 82946 64 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+840.028 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 83947 64 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+850.027 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 84947 64 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+860.027 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 85947 64 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+870.028 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 86947 64 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+880.029 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 87947 65 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+890.029 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 88947 65 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+900.029 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 89947 65 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223680 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+910.029 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 90948 65 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+920.029 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 91948 65 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+930.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 92948 65 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+940.031 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 93948 65 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223744 134557892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+950.031 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 94948 65 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+960.031 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 95949 65 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223680 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+970.032 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 96949 65 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+980.032 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 97949 65 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+990.032 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 98949 65 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 99949 65 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223744 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 100949 65 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223648 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 101949 65 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 102949 65 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 103950 65 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 104950 65 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 105950 65 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 106950 65 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223680 134560608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 107950 65 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 108951 65 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 109951 65 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 110951 65 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 111951 65 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+1130.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20102 0 0 0 112951 65 0 0 25 0 1 0 481262926 89411584 19924 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19924 603 41 0 21788 0
vsize: 87316
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20103 0 0 0 113951 65 0 0 25 0 1 0 481262926 89411584 19925 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19925 603 41 0 21788 0
vsize: 87316
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20105 0 0 0 114951 65 0 0 25 0 1 0 481262926 89411584 19927 4294967295 134512640 134672761 3221224544 3221223552 1075349791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19927 603 41 0 21788 0
vsize: 87316
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20107 0 0 0 115951 65 0 0 25 0 1 0 481262926 89411584 19929 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19929 603 41 0 21788 0
vsize: 87316
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20109 0 0 0 116952 65 0 0 25 0 1 0 481262926 89411584 19931 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19931 603 41 0 21788 0
vsize: 87316
[startup+1180.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20111 0 0 0 117952 66 0 0 25 0 1 0 481262926 89411584 19933 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19933 603 41 0 21788 0
vsize: 87316
[startup+1190.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20113 0 0 0 118952 66 0 0 25 0 1 0 481262926 89411584 19935 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19935 603 41 0 21788 0
vsize: 87316
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24156
Raw data (stat): 24156 (minisat+) R 24155 18865 18864 0 -1 0 20115 0 0 0 119952 66 0 0 25 0 1 0 481262926 89411584 19937 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 19937 603 41 0 21788 0
vsize: 87316
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 1.00 0.94 1/54 24156
Raw data (stat): 24156 (minisat+) Z 24155 18865 18864 0 -1 12 20118 0 0 0 119952 70 0 0 25 0 1 0 481262926 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.08
CPU time (s): 1200.23
CPU user time (s): 1199.53
CPU system time (s): 0.700893
CPU usage (%): 100.012
Max. virtual memory (Kb): 87316
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####