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/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-ran14x18_1.opb
MD5SUM	27cc6bcebfcedf07c5cf3ac138a419c6
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	913429
Optimality of the best value was proved	NO
Number of terms in the objective function	5292
Biggest coefficient in the objective function	5242880
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	1421968313
Number of bits of the sum of numbers in the objective function	31
Biggest number in a constraint	5242880
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	1421968313
Number of bits of the biggest sum of numbers	31
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.03
Number of variables	5292
Total number of constraints	536
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	252
Number of constraints which are nor clauses,nor cardinality constraints	284
Minimum length of a constraint	1
Maximum length of a constraint	360
Trace number 31314

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-05-26 00:04:37 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22708 boxname=wulflinc3 idbench=1524 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  27cc6bcebfcedf07c5cf3ac138a419c6  /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-ran14x18_1.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-ran14x18_1.opb
IDLAUNCH: 22708
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        884516 kB
Buffers:          8912 kB
Cached:         122112 kB
SwapCached:         12 kB
Active:          32556 kB
Inactive:       101196 kB
HighTotal:      131008 kB
HighFree:        10640 kB
LowTotal:       903652 kB
LowFree:        873876 kB
SwapTotal:     2097136 kB
SwapFree:      2096788 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6576 kB
Slab:            10812 kB
Committed_AS:    71752 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-26 00:25:07 (client local time) WITH STATUS 152 IN 1229.87 SECONDS
stats: 22708 7 1229.87 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 316 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 314]---> Adder-cost: 386   maxlim: 47470   bits: 16/16
c ---[ 312]---> Adder-cost: 386   maxlim: 47726   bits: 16/16
c ---[ 310]---> Adder-cost: 386   maxlim: 47342   bits: 16/16
c ---[ 308]---> Adder-cost: 388   maxlim: 58222   bits: 16/16
c ---[ 306]---> Adder-cost: 386   maxlim: 47342   bits: 16/16
c ---[ 304]---> Adder-cost: 386   maxlim: 46830   bits: 16/16
c ---[ 302]---> Adder-cost: 386   maxlim: 47086   bits: 16/16
c ---[ 300]---> Adder-cost: 372   maxlim: 32494   bits: 16/15
c ---[ 298]---> Adder-cost: 386   maxlim: 46702   bits: 16/16
c ---[ 296]---> Adder-cost: 386   maxlim: 46958   bits: 16/16
c ---[ 294]---> Adder-cost: 372   maxlim: 32494   bits: 16/15
c ---[ 292]---> Adder-cost: 386   maxlim: 48110   bits: 16/16
c ---[ 290]---> Adder-cost: 386   maxlim: 47982   bits: 16/16
c ---[ 288]---> Adder-cost: 388   maxlim: 57582   bits: 16/16
c ---[ 286]---> Adder-cost: 260   maxlim: 13554   bits: 14/14
c ---[ 284]---> Adder-cost: 286   maxlim: 26994   bits: 15/15
c ---[ 282]---> Adder-cost: 260   maxlim: 13426   bits: 14/14
c ---[ 280]---> Adder-cost: 310   maxlim: 50930   bits: 16/16
c ---[ 278]---> Adder-cost: 286   maxlim: 26866   bits: 15/15
c ---[ 276]---> Adder-cost: 310   maxlim: 50418   bits: 16/16
c ---[ 274]---> Adder-cost: 312   maxlim: 57202   bits: 16/16
c ---[ 272]---> Adder-cost: 312   maxlim: 55666   bits: 16/16
c ---[ 270]---> Adder-cost: 286   maxlim: 27250   bits: 15/15
c ---[ 268]---> Adder-cost: 286   maxlim: 27634   bits: 15/15
c ---[ 266]---> Adder-cost: 310   maxlim: 50546   bits: 16/16
c ---[ 264]---> Adder-cost: 286   maxlim: 27250   bits: 15/15
c ---[ 262]---> Adder-cost: 310   maxlim: 50674   bits: 16/16
c ---[ 260]---> Adder-cost: 260   maxlim: 13810   bits: 14/14
c ---[ 258]---> Adder-cost: 312   maxlim: 56946   bits: 16/16
c ---[ 256]---> Adder-cost: 286   maxlim: 26994   bits: 15/15
c ---[ 254]---> Adder-cost: 310   maxlim: 50674   bits: 16/16
c ---[ 252]---> Adder-cost: 286   maxlim: 27506   bits: 15/15
c ---[ 251]---> BDD-cost:   12
c ---[ 250]---> BDD-cost:   15
c ---[ 249]---> BDD-cost:   13
c ---[ 248]---> BDD-cost:   13
c ---[ 247]---> BDD-cost:   16
c ---[ 246]---> BDD-cost:   14
c ---[ 245]---> BDD-cost:   16
c ---[ 244]---> BDD-cost:   17
c ---[ 243]---> BDD-cost:   17
c ---[ 242]---> BDD-cost:   15
c ---[ 241]---> BDD-cost:   12
c ---[ 240]---> BDD-cost:   12
c ---[ 239]---> BDD-cost:   14
c ---[ 238]---> BDD-cost:   16
c ---[ 237]---> BDD-cost:   14
c ---[ 236]---> BDD-cost:   14
c ---[ 235]---> BDD-cost:   14
c ---[ 234]---> BDD-cost:   11
c ---[ 233]---> BDD-cost:   14
c ---[ 232]---> BDD-cost:   14
c ---[ 231]---> BDD-cost:   14
c ---[ 230]---> BDD-cost:   15
c ---[ 229]---> BDD-cost:   13
c ---[ 228]---> BDD-cost:   14
c ---[ 227]---> BDD-cost:   14
c ---[ 226]---> BDD-cost:   14
c ---[ 225]---> BDD-cost:   14
c ---[ 224]---> BDD-cost:   14
c ---[ 223]---> BDD-cost:   14
c ---[ 222]---> BDD-cost:   14
c ---[ 221]---> BDD-cost:   12
c ---[ 220]---> BDD-cost:   12
c ---[ 219]---> BDD-cost:   15
c ---[ 218]---> BDD-cost:   13
c ---[ 217]---> BDD-cost:   15
c ---[ 216]---> BDD-cost:   17
c ---[ 215]---> BDD-cost:   13
c ---[ 214]---> BDD-cost:   11
c ---[ 213]---> BDD-cost:   13
c ---[ 212]---> BDD-cost:   15
c ---[ 211]---> BDD-cost:   13
c ---[ 210]---> BDD-cost:   15
c ---[ 209]---> BDD-cost:   13
c ---[ 208]---> BDD-cost:   13
c ---[ 207]---> BDD-cost:   14
c ---[ 206]---> BDD-cost:   13
c ---[ 205]---> BDD-cost:   17
c ---[ 204]---> BDD-cost:   13
c ---[ 203]---> BDD-cost:   13
c ---[ 202]---> BDD-cost:   15
c ---[ 201]---> BDD-cost:   12
c ---[ 200]---> BDD-cost:   12
c ---[ 199]---> BDD-cost:   15
c ---[ 198]---> BDD-cost:   17
c ---[ 197]---> BDD-cost:   15
c ---[ 196]---> BDD-cost:   17
c ---[ 195]---> BDD-cost:   11
c ---[ 194]---> BDD-cost:   17
c ---[ 193]---> BDD-cost:   17
c ---[ 192]---> BDD-cost:   15
c ---[ 191]---> BDD-cost:   17
c ---[ 190]---> BDD-cost:   15
c ---[ 189]---> BDD-cost:   13
c ---[ 188]---> BDD-cost:   17
c ---[ 187]---> BDD-cost:   14
c ---[ 186]---> BDD-cost:   17
c ---[ 185]---> BDD-cost:   17
c ---[ 184]---> BDD-cost:   17
c ---[ 183]---> BDD-cost:   15
c ---[ 182]---> BDD-cost:   15
c ---[ 181]---> BDD-cost:   12
c ---[ 180]---> BDD-cost:   12
c ---[ 179]---> BDD-cost:   15
c ---[ 178]---> BDD-cost:   17
c ---[ 177]---> BDD-cost:   15
c ---[ 176]---> BDD-cost:   15
c ---[ 175]---> BDD-cost:   11
c ---[ 174]---> BDD-cost:   19
c ---[ 173]---> BDD-cost:   15
c ---[ 172]---> BDD-cost:   12
c ---[ 171]---> BDD-cost:   15
c ---[ 170]---> BDD-cost:   15
c ---[ 169]---> BDD-cost:   13
c ---[ 168]---> BDD-cost:   16
c ---[ 167]---> BDD-cost:   14
c ---[ 166]---> BDD-cost:   16
c ---[ 165]---> BDD-cost:   19
c ---[ 164]---> BDD-cost:   18
c ---[ 163]---> BDD-cost:   15
c ---[ 162]---> BDD-cost:   12
c ---[ 161]---> BDD-cost:   12
c ---[ 160]---> BDD-cost:   12
c ---[ 159]---> BDD-cost:   15
c ---[ 158]---> BDD-cost:   17
c ---[ 157]---> BDD-cost:   15
c ---[ 156]---> BDD-cost:   15
c ---[ 155]---> BDD-cost:   11
c ---[ 154]---> BDD-cost:   16
c ---[ 153]---> BDD-cost:   15
c ---[ 152]---> BDD-cost:   15
c ---[ 151]---> BDD-cost:   15
c ---[ 150]---> BDD-cost:   15
c ---[ 149]---> BDD-cost:   13
c ---[ 148]---> BDD-cost:   16
c ---[ 147]---> BDD-cost:   14
c ---[ 146]---> BDD-cost:   16
c ---[ 145]---> BDD-cost:   16
c ---[ 144]---> BDD-cost:   16
c ---[ 143]---> BDD-cost:   15
c ---[ 142]---> BDD-cost:   12
c ---[ 141]---> BDD-cost:   12
c ---[ 140]---> BDD-cost:   15
c ---[ 139]---> BDD-cost:   17
c ---[ 138]---> BDD-cost:   17
c ---[ 137]---> BDD-cost:   17
c ---[ 136]---> BDD-cost:   15
c ---[ 135]---> BDD-cost:   15
c ---[ 134]---> BDD-cost:   11
c ---[ 133]---> BDD-cost:   19
c ---[ 132]---> BDD-cost:   15
c ---[ 131]---> BDD-cost:   15
c ---[ 130]---> BDD-cost:   15
c ---[ 129]---> BDD-cost:   13
c ---[ 128]---> BDD-cost:   16
c ---[ 127]---> BDD-cost:   15
c ---[ 126]---> BDD-cost:   14
c ---[ 125]---> BDD-cost:   16
c ---[ 124]---> BDD-cost:   19
c ---[ 123]---> BDD-cost:   19
c ---[ 122]---> BDD-cost:   15
c ---[ 121]---> BDD-cost:   12
c ---[ 120]---> BDD-cost:   12
c ---[ 119]---> BDD-cost:   15
c ---[ 118]---> BDD-cost:   17
c ---[ 117]---> BDD-cost:   15
c ---[ 116]---> BDD-cost:   17
c ---[ 115]---> BDD-cost:   15
c ---[ 114]---> BDD-cost:   11
c ---[ 113]---> BDD-cost:   16
c ---[ 112]---> BDD-cost:   15
c ---[ 111]---> BDD-cost:   15
c ---[ 110]---> BDD-cost:   15
c ---[ 109]---> BDD-cost:   13
c ---[ 108]---> BDD-cost:   16
c ---[ 107]---> BDD-cost:   14
c ---[ 106]---> BDD-cost:   16
c ---[ 105]---> BDD-cost:   11
c ---[ 104]---> BDD-cost:   16
c ---[ 103]---> BDD-cost:   16
c ---[ 102]---> BDD-cost:   15
c ---[ 101]---> BDD-cost:   12
c ---[ 100]---> BDD-cost:   12
c ---[  99]---> BDD-cost:   15
c ---[  98]---> BDD-cost:   17
c ---[  97]---> BDD-cost:   15
c ---[  96]---> BDD-cost:   15
c ---[  95]---> BDD-cost:   11
c ---[  94]---> BDD-cost:   17
c ---[  93]---> BDD-cost:   16
c ---[  92]---> BDD-cost:   15
c ---[  91]---> BDD-cost:   15
c ---[  90]---> BDD-cost:   15
c ---[  89]---> BDD-cost:   13
c ---[  88]---> BDD-cost:   16
c ---[  87]---> BDD-cost:   14
c ---[  86]---> BDD-cost:   16
c ---[  85]---> BDD-cost:   16
c ---[  84]---> BDD-cost:   16
c ---[  83]---> BDD-cost:   15
c ---[  82]---> BDD-cost:   15
c ---[  81]---> BDD-cost:   12
c ---[  80]---> BDD-cost:   17
c ---[  79]---> BDD-cost:   15
c ---[  78]---> BDD-cost:   13
c ---[  77]---> BDD-cost:   16
c ---[  76]---> BDD-cost:   15
c ---[  75]---> BDD-cost:   14
c ---[  74]---> BDD-cost:   17
c ---[  73]---> BDD-cost:   17
c ---[  72]---> BDD-cost:   17
c ---[  71]---> BDD-cost:   15
c ---[  70]---> BDD-cost:   12
c ---[  69]---> BDD-cost:   12
c ---[  68]---> BDD-cost:   15
c ---[  67]---> BDD-cost:   17
c ---[  66]---> BDD-cost:   15
c ---[  65]---> BDD-cost:   15
c ---[  64]---> BDD-cost:   15
c ---[  63]---> BDD-cost:   11
c ---[  62]---> BDD-cost:   14
c ---[  61]---> BDD-cost:   15
c ---[  60]---> BDD-cost:   15
c ---[  59]---> BDD-cost:   15
c ---[  58]---> BDD-cost:   13
c ---[  57]---> BDD-cost:   16
c ---[  56]---> BDD-cost:   14
c ---[  55]---> BDD-cost:   16
c ---[  54]---> BDD-cost:   11
c ---[  53]---> BDD-cost:   14
c ---[  52]---> BDD-cost:   14
c ---[  51]---> BDD-cost:   15
c ---[  50]---> BDD-cost:   12
c ---[  49]---> BDD-cost:   12
c ---[  48]---> BDD-cost:   14
c ---[  47]---> BDD-cost:   14
c ---[  46]---> BDD-cost:   14
c ---[  45]---> BDD-cost:   14
c ---[  44]---> BDD-cost:   11
c ---[  43]---> BDD-cost:   17
c ---[  42]---> BDD-cost:   14
c ---[  41]---> BDD-cost:   14
c ---[  40]---> BDD-cost:   14
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   13
c ---[  37]---> BDD-cost:   14
c ---[  36]---> BDD-cost:   14
c ---[  35]---> BDD-cost:   14
c ---[  34]---> BDD-cost:   14
c ---[  33]---> BDD-cost:   14
c ---[  32]---> BDD-cost:   15
c ---[  31]---> BDD-cost:   14
c ---[  30]---> BDD-cost:   12
c ---[  29]---> BDD-cost:   12
c ---[  28]---> BDD-cost:   15
c ---[  27]---> BDD-cost:   17
c ---[  26]---> BDD-cost:   15
c ---[  25]---> BDD-cost:   15
c ---[  24]---> BDD-cost:   11
c ---[  23]---> BDD-cost:   17
c ---[  22]---> BDD-cost:   15
c ---[  21]---> BDD-cost:   15
c ---[  20]---> BDD-cost:   15
c ---[  19]---> BDD-cost:   15
c ---[  18]---> BDD-cost:   13
c ---[  17]---> BDD-cost:   16
c ---[  16]---> BDD-cost:   14
c ---[  15]---> BDD-cost:   16
c ---[  14]---> BDD-cost:   17
c ---[  13]---> BDD-cost:   17
c ---[  12]---> BDD-cost:   15
c ---[  11]---> BDD-cost:   12
c ---[  10]---> BDD-cost:   15
c ---[   9]---> BDD-cost:   12
c ---[   8]---> BDD-cost:   15
c ---[   7]---> BDD-cost:   17
c ---[   6]---> BDD-cost:   15
c ---[   5]---> BDD-cost:   15
c ---[   4]---> BDD-cost:   11
c ---[   3]---> BDD-cost:   17
c ---[   2]---> BDD-cost:   15
c ---[   1]---> BDD-cost:   15
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   76494   265887 |   25498       0        0     nan |  0.000 % |
c |       100 |   76455   265758 |   28047      95      301     3.2 | 19.306 % |
c |       251 |   76209   264924 |   30852     214      693     3.2 | 19.548 % |
c |       476 |   76136   264681 |   33937     431     1394     3.2 | 19.621 % |
c |       813 |   75934   264013 |   37331     750     2468     3.3 | 19.829 % |
c |      1319 |   75512   262589 |   41064    1207     4044     3.4 | 20.262 % |
c |      2078 |   75153   261368 |   45171    1925     6481     3.4 | 20.611 % |
c |      3217 |   74754   260011 |   49688    3021    10698     3.5 | 21.015 % |
c |      4925 |   74372   258711 |   54657    4687    17335     3.7 | 21.398 % |
c |      7488 |   74311   258514 |   60122    7243    31598     4.4 | 21.459 % |
c |     11332 |   74187   258090 |   66135   11070    59410     5.4 | 21.578 % |
c |     17099 |   74061   257668 |   72748   16820   132019     7.8 | 21.707 % |
c |     25749 |   73947   257284 |   80023   25449   208727     8.2 | 21.814 % |
c |     38723 |   73853   256966 |   88026   38408   360956     9.4 | 21.909 % |
c |     58184 |   73374   255339 |   96828   57793   657242    11.4 | 22.410 % |
c |     87376 |   73275   254996 |  106511   86972  2569004    29.5 | 22.516 % |
c |    131166 |   72901   253710 |  117162   47067   486316    10.3 | 22.921 % |
c |    196851 |   72787   253332 |  128878  112735  3790794    33.6 | 23.039 % |
c |    295382 |   72762   253251 |  141766   90432  8680541    96.0 | 23.067 % |
c |    443171 |   72646   252867 |  155943  113636  5564183    49.0 | 23.191 % |
c |    664855 |   72605   252732 |  171537   52849  1095405    20.7 | 23.230 % |
c ==============================================================================
c [1mFound solution: 5531627[0m
c ---[   0]---> Adder-cost: 10447   maxlim: 3457998   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    736191 |  145536   513292 |   48512  124173  2842136    22.9 | 23.230 % |
c |    736291 |  145536   513292 |   53363   24661   603902    24.5 | 14.741 % |
c |    736441 |  145536   513292 |   58699   24811   604684    24.4 | 14.741 % |
c |    736667 |  145536   513292 |   64569   25037   605778    24.2 | 14.741 % |
c |    737004 |  145536   513292 |   71026   25374   607423    23.9 | 14.741 % |
c |    737510 |  145536   513292 |   78129   25880   610341    23.6 | 14.741 % |
c |    738269 |  145536   513292 |   85941   26639   614756    23.1 | 14.741 % |
c |    739408 |  145536   513292 |   94536   27778   623035    22.4 | 14.741 % |
c |    741116 |  145536   513292 |  103989   29486   636457    21.6 | 14.741 % |
c |    743678 |  145536   513292 |  114388   32048   663341    20.7 | 14.741 % |
c |    747522 |  145536   513292 |  125827   35892   698988    19.5 | 14.741 % |
c |    753288 |  145527   513263 |  138410   41657   768271    18.4 | 14.748 % |
c |    761938 |  145476   513092 |  152251   50298   869065    17.3 | 14.780 % |
c |    774912 |  145442   512982 |  167476   63268  1017165    16.1 | 14.805 % |
c |    794373 |  145405   512861 |  184224   82722  2257727    27.3 | 14.826 % |
c |    823566 |  145258   512372 |  202646  111893  3536219    31.6 | 14.918 % |
c ==============================================================================
c [1mFound solution: 5290450[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3699175   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    849546 |  145266   512503 |   48422  137871  5124104    37.2 | 14.918 % |
c |    849646 |  145266   512503 |   53264   28631   676824    23.6 | 14.952 % |
c |    849796 |  145266   512503 |   58590   28781   677659    23.5 | 14.952 % |
c |    850021 |  145266   512503 |   64449   29006   679109    23.4 | 14.952 % |
c |    850358 |  145266   512503 |   70894   29343   680974    23.2 | 14.952 % |
c |    850864 |  145266   512503 |   77984   29849   684879    22.9 | 14.952 % |
c |    851623 |  145266   512503 |   85782   30608   690912    22.6 | 14.952 % |
c |    852763 |  145266   512503 |   94360   31748   699288    22.0 | 14.952 % |
c |    854471 |  145266   512503 |  103796   33456   713642    21.3 | 14.952 % |
c |    857033 |  145266   512503 |  114176   36018   733776    20.4 | 14.952 % |
c |    860877 |  145266   512503 |  125594   39862   769022    19.3 | 14.952 % |
c |    866643 |  145250   512451 |  138153   45625   826019    18.1 | 14.963 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:  5710 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### 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.85 0.97 0.91 2/54 5706
Raw data (stat): 5706 (runsolver) R 5705 20224 20223 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 784829296 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 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+9.99998 s]
Raw data (loadavg): 0.87 0.97 0.91 2/55 5710
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0008 s]
Raw data (loadavg): 0.89 0.97 0.91 2/55 5710
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0014 s]
Raw data (loadavg): 0.91 0.97 0.91 2/55 5710
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0015 s]
Raw data (loadavg): 0.92 0.97 0.91 2/55 5710
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0023 s]
Raw data (loadavg): 0.93 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0018 s]
Raw data (loadavg): 0.94 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0032 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.004 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0034 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.004 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.005 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.013 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.74 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 5712
Raw data (stat): 5706 (minisat+_script) S 5705 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784829296 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.74
CPU time (s): 1229.87
CPU user time (s): 1229.21
CPU system time (s): 0.659899
CPU usage (%): 100.011
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####