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/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-pp08a.opb
MD5SUM	962e64054cef66ff1ace4918a032c24a
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1983976
Optimality of the best value was proved	NO
Number of terms in the objective function	2304
Biggest coefficient in the objective function	1048576
Number of bits for the biggest coefficient in the objective function	21
Sum of the numbers in the objective function	178464600
Number of bits of the sum of numbers in the objective function	28
Biggest number in a constraint	1048576
Number of bits of the biggest number in a constraint	21
Biggest sum of numbers in a constraint	178464600
Number of bits of the biggest sum of numbers	28
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.01
Number of variables	3584
Total number of constraints	200
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	64
Number of constraints which are nor clauses,nor cardinality constraints	136
Minimum length of a constraint	1
Maximum length of a constraint	160
Trace number 15315

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-04-21 03:55:36 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17926 boxname=wulflinc11 idbench=1379 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  962e64054cef66ff1ace4918a032c24a  /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-pp08a.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-pp08a.opb /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-pp08a.opb
IDLAUNCH: 17926
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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	: 2
cpu MHz		: 451.028
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:        872360 kB
Buffers:         24844 kB
Cached:         116664 kB
SwapCached:          0 kB
Active:          66948 kB
Inactive:        77304 kB
HighTotal:      131008 kB
HighFree:        13916 kB
LowTotal:       903652 kB
LowFree:        858444 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           6816 kB
Slab:            12528 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 04:15:40 (client local time) WITH STATUS 0 IN 1200.43 SECONDS
stats: 17926 7 1200.43 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 200 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 198]---> BDD-cost:  158
c ---[ 196]---> BDD-cost:  566
c ---[ 195]---> BDD-cost:   21
c ---[ 194]---> BDD-cost:   21
c ---[ 193]---> BDD-cost:   21
c ---[ 192]---> BDD-cost:   21
c ---[ 191]---> BDD-cost:   23
c ---[ 190]---> BDD-cost:   18
c ---[ 189]---> BDD-cost:   18
c ---[ 188]---> BDD-cost:   18
c ---[ 187]---> BDD-cost:   18
c ---[ 186]---> BDD-cost:   18
c ---[ 184]---> BDD-cost:  576
c ---[ 183]---> BDD-cost:   18
c ---[ 182]---> BDD-cost:   18
c ---[ 181]---> BDD-cost:   18
c ---[ 180]---> BDD-cost:   24
c ---[ 179]---> BDD-cost:   24
c ---[ 178]---> BDD-cost:   24
c ---[ 177]---> BDD-cost:   21
c ---[ 176]---> BDD-cost:   21
c ---[ 175]---> BDD-cost:   21
c ---[ 174]---> BDD-cost:   21
c ---[ 172]---> BDD-cost:  576
c ---[ 171]---> BDD-cost:   21
c ---[ 170]---> BDD-cost:   19
c ---[ 169]---> BDD-cost:   19
c ---[ 168]---> BDD-cost:   19
c ---[ 167]---> BDD-cost:   19
c ---[ 166]---> BDD-cost:   19
c ---[ 165]---> BDD-cost:   19
c ---[ 164]---> BDD-cost:   19
c ---[ 163]---> BDD-cost:   19
c ---[ 162]---> BDD-cost:   19
c ---[ 160]---> BDD-cost:  576
c ---[ 159]---> BDD-cost:   19
c ---[ 158]---> BDD-cost:   19
c ---[ 157]---> BDD-cost:   19
c ---[ 156]---> BDD-cost:   19
c ---[ 155]---> BDD-cost:   19
c ---[ 154]---> BDD-cost:   19
c ---[ 153]---> BDD-cost:   19
c ---[ 151]---> BDD-cost:  529
c ---[ 149]---> BDD-cost:  566
c ---[ 147]---> BDD-cost:  181
c ---[ 145]---> BDD-cost:  180
c ---[ 143]---> BDD-cost:  585
c ---[ 141]---> BDD-cost:  537
c ---[ 139]---> BDD-cost:  585
c ---[ 137]---> BDD-cost:  580
c ---[ 135]---> BDD-cost:  575
c ---[ 133]---> BDD-cost:  570
c ---[ 131]---> BDD-cost:  585
c ---[ 129]---> BDD-cost:  174
c ---[ 127]---> BDD-cost:  158
c ---[ 125]---> BDD-cost:  580
c ---[ 123]---> BDD-cost:  580
c ---[ 121]---> BDD-cost:  585
c ---[ 119]---> BDD-cost:  565
c ---[ 117]---> BDD-cost:  585
c ---[ 115]---> BDD-cost:  585
c ---[ 113]---> BDD-cost:  580
c ---[ 111]---> BDD-cost:  183
c ---[ 109]---> BDD-cost:  181
c ---[ 107]---> BDD-cost:  529
c ---[ 105]---> BDD-cost:  571
c ---[ 103]---> BDD-cost:  566
c ---[ 101]---> BDD-cost:  576
c ---[  99]---> BDD-cost:  576
c ---[  97]---> BDD-cost:  571
c ---[  95]---> BDD-cost:  580
c ---[  93]---> BDD-cost:  181
c ---[  91]---> BDD-cost:  186
c ---[  89]---> BDD-cost:  575
c ---[  87]---> BDD-cost:  575
c ---[  85]---> BDD-cost:  575
c ---[  83]---> BDD-cost:  580
c ---[  81]---> BDD-cost:  580
c ---[  79]---> BDD-cost:  575
c ---[  77]---> BDD-cost:  186
c ---[  75]---> BDD-cost:  154
c ---[  73]---> BDD-cost:  580
c ---[  71]---> BDD-cost:  571
c ---[  69]---> BDD-cost:  576
c ---[  67]---> BDD-cost:  576
c ---[  65]---> BDD-cost:  571
c ---[  63]---> BDD-cost:  571
c ---[  61]---> BDD-cost:  566
c ---[  59]---> BDD-cost:  175
c ---[  57]---> BDD-cost:  176
c ---[  55]---> BDD-cost:  562
c ---[  53]---> BDD-cost:  521
c ---[  51]---> BDD-cost:  570
c ---[  49]---> BDD-cost:  521
c ---[  47]---> BDD-cost:  567
c ---[  45]---> BDD-cost:  567
c ---[  43]---> BDD-cost:  562
c ---[  41]---> BDD-cost:  176
c ---[  40]---> BDD-cost: 1143
c ---[  39]---> BDD-cost: 1143
c ---[  38]---> BDD-cost: 1143
c ---[  37]---> BDD-cost: 1165
c ---[  36]---> BDD-cost: 1165
c ---[  34]---> BDD-cost:  537
c ---[  33]---> BDD-cost: 1165
c ---[  32]---> BDD-cost: 1165
c ---[  31]---> BDD-cost: 1176
c ---[  30]---> BDD-cost:   24
c ---[  29]---> BDD-cost:   24
c ---[  28]---> BDD-cost:   24
c ---[  27]---> BDD-cost:   21
c ---[  26]---> BDD-cost:   21
c ---[  25]---> BDD-cost:   21
c ---[  24]---> BDD-cost:   21
c ---[  22]---> BDD-cost:  183
c ---[  21]---> BDD-cost:   23
c ---[  20]---> BDD-cost:   19
c ---[  19]---> BDD-cost:   19
c ---[  18]---> BDD-cost:   19
c ---[  17]---> BDD-cost:   19
c ---[  16]---> BDD-cost:   19
c ---[  15]---> BDD-cost:   19
c ---[  14]---> BDD-cost:   19
c ---[  13]---> BDD-cost:   19
c ---[  12]---> BDD-cost:   24
c ---[  10]---> BDD-cost:  178
c ---[   9]---> BDD-cost:   24
c ---[   8]---> BDD-cost:   24
c ---[   7]---> BDD-cost:   21
c ---[   6]---> BDD-cost:   21
c ---[   5]---> BDD-cost:   21
c ---[   4]---> BDD-cost:   21
c ---[   3]---> BDD-cost:   23
c ---[   2]---> BDD-cost:   24
c ---[   1]---> BDD-cost:   24
c ---[   0]---> BDD-cost:   24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  107271   302166 |   35757       0        0     nan |  0.000 % |
c |       103 |  107271   302166 |   39332     103     1374    13.3 |  1.022 % |
c |       253 |  107271   302166 |   43265     253     4364    17.2 |  1.022 % |
c |       479 |  107271   302166 |   47592     479     7256    15.1 |  1.022 % |
c |       816 |  107271   302166 |   52351     816    10397    12.7 |  1.022 % |
c |      1325 |  107271   302166 |   57587    1325    21682    16.4 |  1.022 % |
c |      2084 |  107271   302166 |   63345    2084    31471    15.1 |  1.022 % |
c |      3227 |  107271   302166 |   69680    3227    47723    14.8 |  1.022 % |
c |      4935 |  107271   302166 |   76648    4935   100170    20.3 |  1.022 % |
c |      7497 |  107271   302166 |   84313    7497   145741    19.4 |  1.022 % |
c |     11341 |  107271   302166 |   92744   11341   206235    18.2 |  1.022 % |
c |     17110 |  107271   302166 |  102018   17110   283737    16.6 |  1.022 % |
c |     25760 |  107271   302166 |  112220   25760   547403    21.3 |  1.022 % |
c |     38734 |  107271   302166 |  123442   38734   857257    22.1 |  1.022 % |
c |     58195 |  107271   302166 |  135787   58195  1314470    22.6 |  1.022 % |
c |     87390 |  107271   302166 |  149365   87390  1764740    20.2 |  1.022 % |
c |    131179 |  107271   302166 |  164302  131179  2767368    21.1 |  1.022 % |
c |    196865 |  107271   302166 |  180732   52122  1121108    21.5 |  1.022 % |
c |    295392 |  107271   302166 |  198805  150649  3712587    24.6 |  1.022 % |
c |    443183 |  107271   302166 |  218686  112658  3844425    34.1 |  1.022 % |
c |    664867 |  107254   302132 |  240555  134965  5198291    38.5 |  1.038 % |
c |    997392 |  107210   302041 |  264610  231653 10219770    44.1 |  1.081 % |
#### 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.80 0.95 0.98 1/54 26867
Raw data (stat): 26867 (runsolver) D 26866 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 18 0 1 0 483779693 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 3225161850 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99962 s]
Raw data (loadavg): 0.83 0.95 0.98 2/54 26867
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 4677 0 0 0 981 12 0 0 25 0 1 0 483779693 22196224 4590 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5419 4590 603 41 0 5378 0
vsize: 21676
[startup+19.9996 s]
Raw data (loadavg): 0.86 0.95 0.98 2/54 26867
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 5650 0 0 0 1978 15 0 0 25 0 1 0 483779693 26210304 5563 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6399 5563 603 41 0 6358 0
vsize: 25596
[startup+30.0002 s]
Raw data (loadavg): 0.88 0.95 0.98 2/54 26867
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 6095 0 0 0 2976 17 0 0 25 0 1 0 483779693 28221440 6008 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6890 6008 603 41 0 6849 0
vsize: 27560
[startup+40.0003 s]
Raw data (loadavg): 0.90 0.96 0.98 2/54 26867
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 6469 0 0 0 3975 18 0 0 25 0 1 0 483779693 29696000 6382 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7250 6382 603 41 0 7209 0
vsize: 29000
[startup+50.0011 s]
Raw data (loadavg): 0.91 0.96 0.98 2/54 26867
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 6932 0 0 0 4974 19 0 0 25 0 1 0 483779693 31584256 6845 4294967295 134512640 134672761 3221224544 3221223696 134565064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7711 6845 603 41 0 7670 0
vsize: 30844
[startup+60.0005 s]
Raw data (loadavg): 0.92 0.96 0.98 2/54 26867
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 7262 0 0 0 5974 20 0 0 25 0 1 0 483779693 32923648 7175 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8038 7175 603 41 0 7997 0
vsize: 32152
[startup+70.0007 s]
Raw data (loadavg): 0.94 0.96 0.98 2/54 26867
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 7814 0 0 0 6972 22 0 0 25 0 1 0 483779693 35598336 7727 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8691 7727 603 41 0 8650 0
vsize: 34764
[startup+80.0011 s]
Raw data (loadavg): 0.94 0.96 0.98 2/54 26867
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 8476 0 0 0 7970 24 0 0 25 0 1 0 483779693 38285312 8389 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9347 8389 603 41 0 9306 0
vsize: 37388
[startup+90.0008 s]
Raw data (loadavg): 0.95 0.96 0.98 2/54 26867
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 8928 0 0 0 8969 25 0 0 25 0 1 0 483779693 40030208 8841 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9773 8841 603 41 0 9732 0
vsize: 39092
[startup+100.001 s]
Raw data (loadavg): 0.96 0.96 0.98 2/54 26867
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 9231 0 0 0 9968 26 0 0 25 0 1 0 483779693 41238528 9144 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10068 9144 603 41 0 10027 0
vsize: 40272
[startup+110.002 s]
Raw data (loadavg): 0.97 0.96 0.98 2/54 26867
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 9231 0 0 0 10968 26 0 0 25 0 1 0 483779693 41238528 9144 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10068 9144 603 41 0 10027 0
vsize: 40272
[startup+120.001 s]
Raw data (loadavg): 0.97 0.96 0.98 2/54 26867
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 9231 0 0 0 11968 26 0 0 25 0 1 0 483779693 41238528 9144 4294967295 134512640 134672761 3221224544 3221223712 134561234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10068 9144 603 41 0 10027 0
vsize: 40272
[startup+130.001 s]
Raw data (loadavg): 0.97 0.96 0.98 2/54 26867
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 9231 0 0 0 12969 26 0 0 25 0 1 0 483779693 41238528 9144 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10068 9144 603 41 0 10027 0
vsize: 40272
[startup+140.001 s]
Raw data (loadavg): 0.98 0.97 0.98 3/54 26867
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 9231 0 0 0 13969 26 0 0 25 0 1 0 483779693 41238528 9144 4294967295 134512640 134672761 3221224544 3221223668 134566133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10068 9144 603 41 0 10027 0
vsize: 40272
[startup+150.002 s]
Raw data (loadavg): 0.98 0.97 0.98 2/54 26867
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 9231 0 0 0 14969 26 0 0 25 0 1 0 483779693 41238528 9144 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10068 9144 603 41 0 10027 0
vsize: 40272
[startup+160.002 s]
Raw data (loadavg): 0.98 0.97 0.98 2/54 26867
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 9231 0 0 0 15969 26 0 0 25 0 1 0 483779693 41238528 9144 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10068 9144 603 41 0 10027 0
vsize: 40272
[startup+170.001 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26867
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 9410 0 0 0 16968 27 0 0 25 0 1 0 483779693 42049536 9323 4294967295 134512640 134672761 3221224544 3221223668 134566012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10266 9323 603 41 0 10225 0
vsize: 41064
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26867
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 9949 0 0 0 17967 29 0 0 25 0 1 0 483779693 44191744 9862 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10789 9862 603 41 0 10748 0
vsize: 43156
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26867
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 10509 0 0 0 18966 30 0 0 25 0 1 0 483779693 46473216 10422 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11346 10422 603 41 0 11305 0
vsize: 45384
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26867
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 11304 0 0 0 19964 32 0 0 25 0 1 0 483779693 49676288 11217 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12128 11217 603 41 0 12087 0
vsize: 48512
[startup+210.002 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26867
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 11914 0 0 0 20963 34 0 0 25 0 1 0 483779693 52084736 11827 4294967295 134512640 134672761 3221224544 3221223648 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12716 11827 603 41 0 12675 0
vsize: 50864
[startup+220.002 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26867
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 11917 0 0 0 21963 34 0 0 25 0 1 0 483779693 52084736 11830 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12716 11830 603 41 0 12675 0
vsize: 50864
[startup+230.003 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26867
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 11919 0 0 0 22963 34 0 0 25 0 1 0 483779693 52084736 11832 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12716 11832 603 41 0 12675 0
vsize: 50864
[startup+240.003 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26867
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 11920 0 0 0 23963 34 0 0 25 0 1 0 483779693 52084736 11833 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12716 11833 603 41 0 12675 0
vsize: 50864
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26867
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 11939 0 0 0 24963 34 0 0 25 0 1 0 483779693 52322304 11852 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12774 11852 603 41 0 12733 0
vsize: 51096
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26867
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 11958 0 0 0 25963 34 0 0 25 0 1 0 483779693 52322304 11871 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12774 11871 603 41 0 12733 0
vsize: 51096
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.98 3/57 26906
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 11958 0 0 0 26964 34 0 0 25 0 1 0 483779693 52322304 11871 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12774 11871 603 41 0 12733 0
vsize: 51096
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26920
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 11958 0 0 0 27963 34 0 0 25 0 1 0 483779693 52322304 11871 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12774 11871 603 41 0 12733 0
vsize: 51096
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26920
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 11968 0 0 0 28963 34 0 0 25 0 1 0 483779693 52518912 11881 4294967295 134512640 134672761 3221224544 3221223712 134561159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12822 11881 603 41 0 12781 0
vsize: 51288
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26920
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 11994 0 0 0 29963 34 0 0 25 0 1 0 483779693 52518912 11907 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12822 11907 603 41 0 12781 0
vsize: 51288
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26920
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 12035 0 0 0 30964 34 0 0 25 0 1 0 483779693 52715520 11948 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11948 603 41 0 12829 0
vsize: 51480
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26920
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 12106 0 0 0 31964 34 0 0 25 0 1 0 483779693 53108736 12019 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12966 12019 603 41 0 12925 0
vsize: 51864
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26920
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 12148 0 0 0 32963 35 0 0 25 0 1 0 483779693 53305344 12061 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13014 12061 603 41 0 12973 0
vsize: 52056
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26920
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 12172 0 0 0 33963 35 0 0 25 0 1 0 483779693 53567488 12085 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13078 12085 603 41 0 13037 0
vsize: 52312
[startup+350.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26922
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 12217 0 0 0 34964 35 0 0 25 0 1 0 483779693 53829632 12130 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13142 12130 603 41 0 13101 0
vsize: 52568
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26922
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 12222 0 0 0 35963 35 0 0 25 0 1 0 483779693 53829632 12135 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13142 12135 603 41 0 13101 0
vsize: 52568
[startup+370.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26922
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 12222 0 0 0 36963 35 0 0 25 0 1 0 483779693 53829632 12135 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13142 12135 603 41 0 13101 0
vsize: 52568
[startup+380.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26922
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 12222 0 0 0 37963 35 0 0 25 0 1 0 483779693 53829632 12135 4294967295 134512640 134672761 3221224544 3221223728 134558914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13142 12135 603 41 0 13101 0
vsize: 52568
[startup+390.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26922
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 12635 0 0 0 38963 36 0 0 25 0 1 0 483779693 55570432 12548 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13567 12548 603 41 0 13526 0
vsize: 54268
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26922
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 12994 0 0 0 39962 37 0 0 25 0 1 0 483779693 57069568 12907 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13933 12907 603 41 0 13892 0
vsize: 55732
[startup+410.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26922
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 13295 0 0 0 40962 37 0 0 25 0 1 0 483779693 58281984 13208 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14229 13208 603 41 0 14188 0
vsize: 56916
[startup+420.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26922
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 13510 0 0 0 41962 38 0 0 25 0 1 0 483779693 59170816 13423 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14446 13423 603 41 0 14405 0
vsize: 57784
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26922
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 13833 0 0 0 42961 38 0 0 25 0 1 0 483779693 60551168 13746 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14783 13746 603 41 0 14742 0
vsize: 59132
[startup+440.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26922
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 14003 0 0 0 43961 39 0 0 25 0 1 0 483779693 61247488 13916 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14953 13916 603 41 0 14912 0
vsize: 59812
[startup+450.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26922
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 14003 0 0 0 44961 39 0 0 25 0 1 0 483779693 61247488 13916 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14953 13916 603 41 0 14912 0
vsize: 59812
[startup+460.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26922
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 14003 0 0 0 45962 39 0 0 25 0 1 0 483779693 61247488 13916 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14953 13916 603 41 0 14912 0
vsize: 59812
[startup+470.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26922
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 14004 0 0 0 46962 39 0 0 25 0 1 0 483779693 61247488 13917 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14953 13917 603 41 0 14912 0
vsize: 59812
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26922
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 14004 0 0 0 47963 39 0 0 25 0 1 0 483779693 61247488 13917 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14953 13917 603 41 0 14912 0
vsize: 59812
[startup+490.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26922
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 14030 0 0 0 48963 39 0 0 25 0 1 0 483779693 61390848 13943 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14988 13943 603 41 0 14947 0
vsize: 59952
[startup+500.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26922
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 14030 0 0 0 49963 39 0 0 25 0 1 0 483779693 61390848 13943 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14988 13943 603 41 0 14947 0
vsize: 59952
[startup+510.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26922
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 14044 0 0 0 50963 39 0 0 25 0 1 0 483779693 61554688 13957 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15028 13957 603 41 0 14987 0
vsize: 60112
[startup+520.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26922
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 14045 0 0 0 51963 39 0 0 25 0 1 0 483779693 61554688 13958 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15028 13958 603 41 0 14987 0
vsize: 60112
[startup+530.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26922
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 14051 0 0 0 52963 39 0 0 25 0 1 0 483779693 61554688 13964 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15028 13964 603 41 0 14987 0
vsize: 60112
[startup+540.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26922
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 14058 0 0 0 53964 39 0 0 25 0 1 0 483779693 61554688 13971 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15028 13971 603 41 0 14987 0
vsize: 60112
[startup+550.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26922
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 14076 0 0 0 54964 39 0 0 25 0 1 0 483779693 61718528 13989 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15068 13989 603 41 0 15027 0
vsize: 60272
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26922
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 14100 0 0 0 55964 39 0 0 25 0 1 0 483779693 61718528 14013 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15068 14013 603 41 0 15027 0
vsize: 60272
[startup+570.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26922
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 14128 0 0 0 56963 39 0 0 25 0 1 0 483779693 61865984 14041 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15104 14041 603 41 0 15063 0
vsize: 60416
[startup+580.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26922
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 14147 0 0 0 57963 39 0 0 25 0 1 0 483779693 62013440 14060 4294967295 134512640 134672761 3221224544 3221223668 134566139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15140 14060 603 41 0 15099 0
vsize: 60560
[startup+590.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26922
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 14174 0 0 0 58963 39 0 0 25 0 1 0 483779693 62160896 14087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15176 14087 603 41 0 15135 0
vsize: 60704
[startup+600.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26922
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 14561 0 0 0 59963 39 0 0 25 0 1 0 483779693 63770624 14474 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15569 14474 603 41 0 15528 0
vsize: 62276
[startup+610.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 15195 0 0 0 60961 41 0 0 25 0 1 0 483779693 66342912 15108 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16197 15108 603 41 0 16156 0
vsize: 64788
[startup+620.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 15727 0 0 0 61959 43 0 0 25 0 1 0 483779693 68669440 15640 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16765 15640 603 41 0 16724 0
vsize: 67060
[startup+630.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 16317 0 0 0 62958 45 0 0 25 0 1 0 483779693 71094272 16230 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17357 16230 603 41 0 17316 0
vsize: 69428
[startup+640.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 17260 0 0 0 63955 48 0 0 25 0 1 0 483779693 74858496 17173 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18276 17173 603 41 0 18235 0
vsize: 73104
[startup+650.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 17942 0 0 0 64952 51 0 0 25 0 1 0 483779693 77688832 17855 4294967295 134512640 134672761 3221224544 3221223604 1075346629 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18967 17855 603 41 0 18926 0
vsize: 75868
[startup+660.016 s]
Raw data (loadavg): 1.07 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 18710 0 0 0 65950 53 0 0 25 0 1 0 483779693 80785408 18623 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19723 18623 603 41 0 19682 0
vsize: 78892
[startup+670.016 s]
Raw data (loadavg): 1.06 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 19428 0 0 0 66948 56 0 0 25 0 1 0 483779693 83750912 19341 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20447 19341 603 41 0 20406 0
vsize: 81788
[startup+680.016 s]
Raw data (loadavg): 1.05 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 20103 0 0 0 67946 57 0 0 25 0 1 0 483779693 86446080 20016 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21105 20016 603 41 0 21064 0
vsize: 84420
[startup+690.016 s]
Raw data (loadavg): 1.04 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 20742 0 0 0 68944 59 0 0 25 0 1 0 483779693 89133056 20655 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21761 20655 603 41 0 21720 0
vsize: 87044
[startup+700.017 s]
Raw data (loadavg): 1.03 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21325 0 0 0 69943 61 0 0 25 0 1 0 483779693 91406336 21238 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22316 21238 603 41 0 22275 0
vsize: 89264
[startup+710.017 s]
Raw data (loadavg): 1.03 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21353 0 0 0 70944 61 0 0 25 0 1 0 483779693 91541504 21266 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22349 21266 603 41 0 22308 0
vsize: 89396
[startup+720.016 s]
Raw data (loadavg): 1.02 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21353 0 0 0 71944 61 0 0 25 0 1 0 483779693 91541504 21266 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22349 21266 603 41 0 22308 0
vsize: 89396
[startup+730.016 s]
Raw data (loadavg): 1.02 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21354 0 0 0 72944 61 0 0 25 0 1 0 483779693 91541504 21267 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22349 21267 603 41 0 22308 0
vsize: 89396
[startup+740.016 s]
Raw data (loadavg): 1.02 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21354 0 0 0 73944 61 0 0 25 0 1 0 483779693 91541504 21267 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22349 21267 603 41 0 22308 0
vsize: 89396
[startup+750.016 s]
Raw data (loadavg): 1.01 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21354 0 0 0 74944 61 0 0 25 0 1 0 483779693 91541504 21267 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22349 21267 603 41 0 22308 0
vsize: 89396
[startup+760.016 s]
Raw data (loadavg): 1.01 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21354 0 0 0 75944 61 0 0 25 0 1 0 483779693 91541504 21267 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22349 21267 603 41 0 22308 0
vsize: 89396
[startup+770.017 s]
Raw data (loadavg): 1.01 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21354 0 0 0 76945 61 0 0 25 0 1 0 483779693 91541504 21267 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22349 21267 603 41 0 22308 0
vsize: 89396
[startup+780.024 s]
Raw data (loadavg): 1.01 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21354 0 0 0 77945 61 0 0 25 0 1 0 483779693 91541504 21267 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22349 21267 603 41 0 22308 0
vsize: 89396
[startup+790.024 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21354 0 0 0 78946 61 0 0 25 0 1 0 483779693 91541504 21267 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22349 21267 603 41 0 22308 0
vsize: 89396
[startup+800.024 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21354 0 0 0 79946 61 0 0 25 0 1 0 483779693 91541504 21267 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22349 21267 603 41 0 22308 0
vsize: 89396
[startup+810.027 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21354 0 0 0 80946 61 0 0 25 0 1 0 483779693 91541504 21267 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22349 21267 603 41 0 22308 0
vsize: 89396
[startup+820.026 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21354 0 0 0 81946 61 0 0 25 0 1 0 483779693 91541504 21267 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22349 21267 603 41 0 22308 0
vsize: 89396
[startup+830.026 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21354 0 0 0 82946 61 0 0 25 0 1 0 483779693 91541504 21267 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22349 21267 603 41 0 22308 0
vsize: 89396
[startup+840.027 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21354 0 0 0 83947 61 0 0 25 0 1 0 483779693 91541504 21267 4294967295 134512640 134672761 3221224544 3221223712 134564490 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22349 21267 603 41 0 22308 0
vsize: 89396
[startup+850.027 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21354 0 0 0 84947 61 0 0 25 0 1 0 483779693 91541504 21267 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22349 21267 603 41 0 22308 0
vsize: 89396
[startup+860.027 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21354 0 0 0 85947 61 0 0 25 0 1 0 483779693 91541504 21267 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22349 21267 603 41 0 22308 0
vsize: 89396
[startup+870.027 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21354 0 0 0 86947 61 0 0 25 0 1 0 483779693 91541504 21267 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22349 21267 603 41 0 22308 0
vsize: 89396
[startup+880.029 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21354 0 0 0 87946 61 0 0 25 0 1 0 483779693 91541504 21267 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22349 21267 603 41 0 22308 0
vsize: 89396
[startup+890.029 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21354 0 0 0 88946 61 0 0 25 0 1 0 483779693 91541504 21267 4294967295 134512640 134672761 3221224544 3221223728 134559324 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22349 21267 603 41 0 22308 0
vsize: 89396
[startup+900.03 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21357 0 0 0 89946 61 0 0 25 0 1 0 483779693 92590080 21270 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22605 21270 603 41 0 22564 0
vsize: 90420
[startup+910.178 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21363 0 0 0 90961 61 0 0 25 0 1 0 483779693 92590080 21276 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22605 21276 603 41 0 22564 0
vsize: 90420
[startup+920.185 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21363 0 0 0 91962 61 0 0 25 0 1 0 483779693 92590080 21276 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22605 21276 603 41 0 22564 0
vsize: 90420
[startup+930.185 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21363 0 0 0 92962 61 0 0 25 0 1 0 483779693 92590080 21276 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22605 21276 603 41 0 22564 0
vsize: 90420
[startup+940.185 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21363 0 0 0 93962 61 0 0 25 0 1 0 483779693 92590080 21276 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22605 21276 603 41 0 22564 0
vsize: 90420
[startup+950.225 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21363 0 0 0 94966 61 0 0 25 0 1 0 483779693 92590080 21276 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22605 21276 603 41 0 22564 0
vsize: 90420
[startup+960.225 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21363 0 0 0 95967 61 0 0 25 0 1 0 483779693 92590080 21276 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22605 21276 603 41 0 22564 0
vsize: 90420
[startup+970.225 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21363 0 0 0 96967 61 0 0 25 0 1 0 483779693 92590080 21276 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22605 21276 603 41 0 22564 0
vsize: 90420
[startup+980.229 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21363 0 0 0 97967 61 0 0 25 0 1 0 483779693 92590080 21276 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22605 21276 603 41 0 22564 0
vsize: 90420
[startup+990.228 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21363 0 0 0 98967 61 0 0 25 0 1 0 483779693 92590080 21276 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22605 21276 603 41 0 22564 0
vsize: 90420
[startup+1000.23 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21363 0 0 0 99968 61 0 0 25 0 1 0 483779693 92590080 21276 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22605 21276 603 41 0 22564 0
vsize: 90420
[startup+1010.23 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21363 0 0 0 100968 61 0 0 25 0 1 0 483779693 92590080 21276 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22605 21276 603 41 0 22564 0
vsize: 90420
[startup+1020.23 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21363 0 0 0 101968 61 0 0 25 0 1 0 483779693 92590080 21276 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22605 21276 603 41 0 22564 0
vsize: 90420
[startup+1030.23 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21363 0 0 0 102969 61 0 0 25 0 1 0 483779693 92590080 21276 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22605 21276 603 41 0 22564 0
vsize: 90420
[startup+1040.23 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21363 0 0 0 103969 61 0 0 25 0 1 0 483779693 92590080 21276 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22605 21276 603 41 0 22564 0
vsize: 90420
[startup+1050.23 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21363 0 0 0 104969 61 0 0 25 0 1 0 483779693 92590080 21276 4294967295 134512640 134672761 3221224544 3221223712 134560845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22605 21276 603 41 0 22564 0
vsize: 90420
[startup+1060.24 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21363 0 0 0 105970 61 0 0 25 0 1 0 483779693 92590080 21276 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22605 21276 603 41 0 22564 0
vsize: 90420
[startup+1070.26 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21363 0 0 0 106972 61 0 0 25 0 1 0 483779693 92590080 21276 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22605 21276 603 41 0 22564 0
vsize: 90420
[startup+1080.26 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21363 0 0 0 107972 61 0 0 25 0 1 0 483779693 92590080 21276 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22605 21276 603 41 0 22564 0
vsize: 90420
[startup+1090.26 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21363 0 0 0 108972 61 0 0 25 0 1 0 483779693 92590080 21276 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22605 21276 603 41 0 22564 0
vsize: 90420
[startup+1100.26 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21363 0 0 0 109972 61 0 0 25 0 1 0 483779693 92590080 21276 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22605 21276 603 41 0 22564 0
vsize: 90420
[startup+1110.26 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21363 0 0 0 110972 61 0 0 25 0 1 0 483779693 92590080 21276 4294967295 134512640 134672761 3221224544 3221223728 134558374 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22605 21276 603 41 0 22564 0
vsize: 90420
[startup+1120.26 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21363 0 0 0 111973 61 0 0 25 0 1 0 483779693 92590080 21276 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22605 21276 603 41 0 22564 0
vsize: 90420
[startup+1130.26 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21365 0 0 0 112973 61 0 0 25 0 1 0 483779693 92590080 21278 4294967295 134512640 134672761 3221224544 3221223648 134555133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22605 21278 603 41 0 22564 0
vsize: 90420
[startup+1140.26 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21365 0 0 0 113973 61 0 0 25 0 1 0 483779693 92590080 21278 4294967295 134512640 134672761 3221224544 3221223500 1075350790 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22605 21278 603 41 0 22564 0
vsize: 90420
[startup+1150.26 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21365 0 0 0 114973 61 0 0 25 0 1 0 483779693 92590080 21278 4294967295 134512640 134672761 3221224544 3221223728 134559572 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22605 21278 603 41 0 22564 0
vsize: 90420
[startup+1160.26 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21365 0 0 0 115974 61 0 0 25 0 1 0 483779693 92590080 21278 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22605 21278 603 41 0 22564 0
vsize: 90420
[startup+1170.26 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21365 0 0 0 116974 61 0 0 25 0 1 0 483779693 92590080 21278 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22605 21278 603 41 0 22564 0
vsize: 90420
[startup+1180.26 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21365 0 0 0 117974 61 0 0 25 0 1 0 483779693 92590080 21278 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22605 21278 603 41 0 22564 0
vsize: 90420
[startup+1190.27 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21365 0 0 0 118975 61 0 0 25 0 1 0 483779693 92590080 21278 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22605 21278 603 41 0 22564 0
vsize: 90420
[startup+1200.29 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26924
Raw data (stat): 26867 (minisat+) R 26866 32461 32460 0 -1 0 21365 0 0 0 119977 61 0 0 25 0 1 0 483779693 92590080 21278 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22605 21278 603 41 0 22564 0
vsize: 90420
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.42 s]
Raw data (loadavg): 1.00 0.99 0.99 1/54 26924
Raw data (stat): 26867 (minisat+) Z 26866 32461 32460 0 -1 12 21367 0 0 0 119977 65 0 0 21 0 1 0 483779693 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.42
CPU time (s): 1200.43
CPU user time (s): 1199.77
CPU system time (s): 0.6519
CPU usage (%): 100.001
Max. virtual memory (Kb): 90420
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####