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/fctp/normalized-mps-v2-13-7-ran6x43.opb
MD5SUM	795a1eda830447df9b9714fdf1d66b4e
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2795888
Optimality of the best value was proved	NO
Number of terms in the objective function	5418
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	1537450315
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	1537450315
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	1224.65
Number of variables	5418
Total number of constraints	307
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	307
Minimum length of a constraint	21
Maximum length of a constraint	860
Trace number 31277

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc22 THE 2005-05-25 23:44:18 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22673 boxname=wulflinc22 idbench=1489 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  795a1eda830447df9b9714fdf1d66b4e  /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-ran6x43.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-ran6x43.opb
IDLAUNCH: 22673
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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	: 3
cpu MHz		: 451.031
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:        591872 kB
Buffers:         35652 kB
Cached:         384732 kB
SwapCached:        400 kB
Active:          63388 kB
Inactive:       359228 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        591620 kB
SwapTotal:     2097892 kB
SwapFree:      2096804 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5580 kB
Slab:            14440 kB
Committed_AS:    63588 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-26 00:04:48 (client local time) WITH STATUS 152 IN 1229.91 SECONDS
stats: 22673 7 1229.91 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 356 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 354]---> Adder-cost: 894   maxlim: 78677   bits: 17/17
c ---[ 352]---> Adder-cost: 894   maxlim: 84309   bits: 17/17
c ---[ 350]---> Adder-cost: 886   maxlim: 78933   bits: 17/17
c ---[ 348]---> Adder-cost: 894   maxlim: 93141   bits: 17/17
c ---[ 346]---> Adder-cost: 818   maxlim: 37973   bits: 16/16
c ---[ 344]---> Adder-cost: 894   maxlim: 84437   bits: 17/17
c ---[ 342]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 340]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[ 338]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 336]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 334]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 332]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[ 330]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2
c ---[ 328]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 326]---> Sorter-cost: 1045     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 324]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 322]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2
c ---[ 320]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 318]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[ 316]---> Sorter-cost: 1045     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 314]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[ 312]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2
c ---[ 310]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 308]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[ 306]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[ 304]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2
c ---[ 302]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 300]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 298]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 296]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[ 294]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[ 292]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[ 290]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 288]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2
c ---[ 286]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 284]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2
c ---[ 282]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 280]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 278]---> Sorter-cost: 1045     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 276]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 274]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 272]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 270]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 268]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2
c ---[ 266]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 264]---> Sorter-cost: 1045     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 262]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[ 260]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[ 258]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 257]---> BDD-cost:   12
c ---[ 256]---> BDD-cost:   12
c ---[ 255]---> BDD-cost:   14
c ---[ 254]---> BDD-cost:   11
c ---[ 253]---> BDD-cost:   15
c ---[ 252]---> BDD-cost:   17
c ---[ 251]---> BDD-cost:   14
c ---[ 250]---> BDD-cost:   10
c ---[ 249]---> BDD-cost:   12
c ---[ 248]---> BDD-cost:   17
c ---[ 247]---> BDD-cost:   12
c ---[ 246]---> BDD-cost:   10
c ---[ 245]---> BDD-cost:   15
c ---[ 244]---> BDD-cost:   17
c ---[ 243]---> BDD-cost:   12
c ---[ 242]---> BDD-cost:   13
c ---[ 241]---> BDD-cost:   11
c ---[ 240]---> BDD-cost:   15
c ---[ 239]---> BDD-cost:   17
c ---[ 238]---> BDD-cost:   12
c ---[ 237]---> BDD-cost:   11
c ---[ 236]---> BDD-cost:   12
c ---[ 235]---> BDD-cost:    9
c ---[ 234]---> BDD-cost:   11
c ---[ 233]---> BDD-cost:   13
c ---[ 232]---> BDD-cost:   17
c ---[ 231]---> BDD-cost:   10
c ---[ 230]---> BDD-cost:   14
c ---[ 229]---> BDD-cost:   17
c ---[ 228]---> BDD-cost:   17
c ---[ 227]---> BDD-cost:    9
c ---[ 226]---> BDD-cost:   15
c ---[ 225]---> BDD-cost:   14
c ---[ 224]---> BDD-cost:   11
c ---[ 223]---> BDD-cost:   12
c ---[ 222]---> BDD-cost:   12
c ---[ 221]---> BDD-cost:   12
c ---[ 220]---> BDD-cost:   13
c ---[ 219]---> BDD-cost:   11
c ---[ 218]---> BDD-cost:   17
c ---[ 217]---> BDD-cost:   14
c ---[ 216]---> BDD-cost:   14
c ---[ 215]---> BDD-cost:   11
c ---[ 214]---> BDD-cost:   11
c ---[ 213]---> BDD-cost:   12
c ---[ 212]---> BDD-cost:   14
c ---[ 211]---> BDD-cost:   11
c ---[ 210]---> BDD-cost:   17
c ---[ 209]---> BDD-cost:   13
c ---[ 208]---> BDD-cost:   12
c ---[ 207]---> BDD-cost:   11
c ---[ 206]---> BDD-cost:   15
c ---[ 205]---> BDD-cost:   19
c ---[ 204]---> BDD-cost:   14
c ---[ 203]---> BDD-cost:   10
c ---[ 202]---> BDD-cost:   12
c ---[ 201]---> BDD-cost:   15
c ---[ 200]---> BDD-cost:   15
c ---[ 199]---> BDD-cost:   12
c ---[ 198]---> BDD-cost:   10
c ---[ 197]---> BDD-cost:   15
c ---[ 196]---> BDD-cost:   12
c ---[ 195]---> BDD-cost:   13
c ---[ 194]---> BDD-cost:   11
c ---[ 193]---> BDD-cost:   15
c ---[ 192]---> BDD-cost:   17
c ---[ 191]---> BDD-cost:   12
c ---[ 190]---> BDD-cost:   11
c ---[ 189]---> BDD-cost:   19
c ---[ 188]---> BDD-cost:   12
c ---[ 187]---> BDD-cost:    9
c ---[ 186]---> BDD-cost:   11
c ---[ 185]---> BDD-cost:   17
c ---[ 184]---> BDD-cost:   10
c ---[ 183]---> BDD-cost:   14
c ---[ 182]---> BDD-cost:   17
c ---[ 181]---> BDD-cost:   19
c ---[ 180]---> BDD-cost:    9
c ---[ 179]---> BDD-cost:   15
c ---[ 178]---> BDD-cost:   14
c ---[ 177]---> BDD-cost:   14
c ---[ 176]---> BDD-cost:   11
c ---[ 175]---> BDD-cost:   13
c ---[ 174]---> BDD-cost:   12
c ---[ 173]---> BDD-cost:   13
c ---[ 172]---> BDD-cost:   11
c ---[ 171]---> BDD-cost:   13
c ---[ 170]---> BDD-cost:   13
c ---[ 169]---> BDD-cost:   13
c ---[ 168]---> BDD-cost:   11
c ---[ 167]---> BDD-cost:   10
c ---[ 166]---> BDD-cost:   11
c ---[ 165]---> BDD-cost:   13
c ---[ 164]---> BDD-cost:   13
c ---[ 163]---> BDD-cost:   13
c ---[ 162]---> BDD-cost:   13
c ---[ 161]---> BDD-cost:   12
c ---[ 160]---> BDD-cost:   11
c ---[ 159]---> BDD-cost:   13
c ---[ 158]---> BDD-cost:   13
c ---[ 157]---> BDD-cost:   13
c ---[ 156]---> BDD-cost:   12
c ---[ 155]---> BDD-cost:   10
c ---[ 154]---> BDD-cost:   13
c ---[ 153]---> BDD-cost:   13
c ---[ 152]---> BDD-cost:   12
c ---[ 151]---> BDD-cost:   10
c ---[ 150]---> BDD-cost:   13
c ---[ 149]---> BDD-cost:   12
c ---[ 148]---> BDD-cost:   13
c ---[ 147]---> BDD-cost:   11
c ---[ 146]---> BDD-cost:   13
c ---[ 145]---> BDD-cost:   13
c ---[ 144]---> BDD-cost:   19
c ---[ 143]---> BDD-cost:   13
c ---[ 142]---> BDD-cost:   13
c ---[ 141]---> BDD-cost:   11
c ---[ 140]---> BDD-cost:   12
c ---[ 139]---> BDD-cost:    9
c ---[ 138]---> BDD-cost:   11
c ---[ 137]---> BDD-cost:   13
c ---[ 136]---> BDD-cost:   10
c ---[ 135]---> BDD-cost:   13
c ---[ 134]---> BDD-cost:   13
c ---[ 133]---> BDD-cost:   12
c ---[ 132]---> BDD-cost:   13
c ---[ 131]---> BDD-cost:    9
c ---[ 130]---> BDD-cost:   13
c ---[ 129]---> BDD-cost:   13
c ---[ 128]---> BDD-cost:   11
c ---[ 127]---> BDD-cost:   12
c ---[ 126]---> BDD-cost:   12
c ---[ 125]---> BDD-cost:   13
c ---[ 124]---> BDD-cost:   11
c ---[ 123]---> BDD-cost:   17
c ---[ 122]---> BDD-cost:   10
c ---[ 121]---> BDD-cost:   14
c ---[ 120]---> BDD-cost:   14
c ---[ 119]---> BDD-cost:   11
c ---[ 118]---> BDD-cost:   11
c ---[ 117]---> BDD-cost:   12
c ---[ 116]---> BDD-cost:   14
c ---[ 115]---> BDD-cost:   17
c ---[ 114]---> BDD-cost:   13
c ---[ 113]---> BDD-cost:   12
c ---[ 112]---> BDD-cost:   11
c ---[ 111]---> BDD-cost:   15
c ---[ 110]---> BDD-cost:   15
c ---[ 109]---> BDD-cost:   19
c ---[ 108]---> BDD-cost:   14
c ---[ 107]---> BDD-cost:   10
c ---[ 106]---> BDD-cost:   12
c ---[ 105]---> BDD-cost:   19
c ---[ 104]---> BDD-cost:   12
c ---[ 103]---> BDD-cost:   10
c ---[ 102]---> BDD-cost:   15
c ---[ 101]---> BDD-cost:   12
c ---[ 100]---> BDD-cost:   12
c ---[  99]---> BDD-cost:   13
c ---[  98]---> BDD-cost:   11
c ---[  97]---> BDD-cost:   15
c ---[  96]---> BDD-cost:   17
c ---[  95]---> BDD-cost:   12
c ---[  94]---> BDD-cost:   11
c ---[  93]---> BDD-cost:   12
c ---[  92]---> BDD-cost:    9
c ---[  91]---> BDD-cost:   11
c ---[  90]---> BDD-cost:   17
c ---[  89]---> BDD-cost:   13
c ---[  88]---> BDD-cost:   10
c ---[  87]---> BDD-cost:   14
c ---[  86]---> BDD-cost:   17
c ---[  85]---> BDD-cost:   19
c ---[  84]---> BDD-cost:    9
c ---[  83]---> BDD-cost:   15
c ---[  82]---> BDD-cost:   14
c ---[  81]---> BDD-cost:   11
c ---[  80]---> BDD-cost:   11
c ---[  79]---> BDD-cost:   15
c ---[  78]---> BDD-cost:   17
c ---[  77]---> BDD-cost:   12
c ---[  76]---> BDD-cost:   11
c ---[  75]---> BDD-cost:   11
c ---[  74]---> BDD-cost:   12
c ---[  73]---> BDD-cost:    9
c ---[  72]---> BDD-cost:   11
c ---[  71]---> BDD-cost:   17
c ---[  70]---> BDD-cost:   10
c ---[  69]---> BDD-cost:   14
c ---[  68]---> BDD-cost:   17
c ---[  67]---> BDD-cost:   19
c ---[  66]---> BDD-cost:    9
c ---[  65]---> BDD-cost:   17
c ---[  64]---> BDD-cost:   15
c ---[  63]---> BDD-cost:   14
c ---[  62]---> BDD-cost:   11
c ---[  61]---> BDD-cost:   12
c ---[  60]---> BDD-cost:   12
c ---[  59]---> BDD-cost:   13
c ---[  58]---> BDD-cost:   11
c ---[  57]---> BDD-cost:   17
c ---[  56]---> BDD-cost:   14
c ---[  55]---> BDD-cost:   14
c ---[  54]---> BDD-cost:   14
c ---[  53]---> BDD-cost:   11
c ---[  52]---> BDD-cost:   11
c ---[  51]---> BDD-cost:   12
c ---[  50]---> BDD-cost:   14
c ---[  49]---> BDD-cost:   17
c ---[  48]---> BDD-cost:   13
c ---[  47]---> BDD-cost:   12
c ---[  46]---> BDD-cost:   11
c ---[  45]---> BDD-cost:   15
c ---[  44]---> BDD-cost:   19
c ---[  43]---> BDD-cost:   14
c ---[  42]---> BDD-cost:   14
c ---[  41]---> BDD-cost:   10
c ---[  40]---> BDD-cost:   12
c ---[  39]---> BDD-cost:   19
c ---[  38]---> BDD-cost:   12
c ---[  37]---> BDD-cost:   10
c ---[  36]---> BDD-cost:   15
c ---[  35]---> BDD-cost:   12
c ---[  34]---> BDD-cost:   13
c ---[  33]---> BDD-cost:   11
c ---[  32]---> BDD-cost:   11
c ---[  31]---> BDD-cost:   15
c ---[  30]---> BDD-cost:   17
c ---[  29]---> BDD-cost:   12
c ---[  28]---> BDD-cost:   11
c ---[  27]---> BDD-cost:   12
c ---[  26]---> BDD-cost:    9
c ---[  25]---> BDD-cost:   11
c ---[  24]---> BDD-cost:   17
c ---[  23]---> BDD-cost:   10
c ---[  22]---> BDD-cost:   14
c ---[  21]---> BDD-cost:   11
c ---[  20]---> BDD-cost:   17
c ---[  19]---> BDD-cost:   19
c ---[  18]---> BDD-cost:    9
c ---[  17]---> BDD-cost:   15
c ---[  16]---> BDD-cost:   14
c ---[  15]---> BDD-cost:   11
c ---[  14]---> BDD-cost:   12
c ---[  13]---> BDD-cost:   12
c ---[  12]---> BDD-cost:   13
c ---[  11]---> BDD-cost:   11
c ---[  10]---> BDD-cost:   12
c ---[   9]---> BDD-cost:   17
c ---[   8]---> BDD-cost:   14
c ---[   7]---> BDD-cost:   17
c ---[   6]---> BDD-cost:   11
c ---[   5]---> BDD-cost:   11
c ---[   4]---> BDD-cost:   12
c ---[   3]---> BDD-cost:   14
c ---[   2]---> BDD-cost:   17
c ---[   1]---> BDD-cost:   13
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  130292   351692 |   43430       0        0     nan |  0.000 % |
c |       101 |  129982   350986 |   47773      86      285     3.3 | 10.876 % |
c |       251 |  129745   350445 |   52550     227      782     3.4 | 11.042 % |
c |       476 |  129592   350099 |   57805     440     1526     3.5 | 11.148 % |
c |       813 |  129191   349134 |   63585     754     2652     3.5 | 11.410 % |
c |      1319 |  128975   348574 |   69944    1248     4595     3.7 | 11.548 % |
c |      2078 |  128738   348035 |   76938    1990     7288     3.7 | 11.708 % |
c |      3217 |  128642   347807 |   84632    3122    12665     4.1 | 11.773 % |
c |      4925 |  127437   345051 |   93096    4770    19257     4.0 | 12.643 % |
c |      7487 |  126161   342093 |  102405    7233    34078     4.7 | 13.545 % |
c |     11331 |  125335   340140 |  112646   11015    52922     4.8 | 14.126 % |
c |     17097 |  124262   337580 |  123910   16676   117469     7.0 | 14.869 % |
c |     25746 |  122620   333161 |  136301   25013   205317     8.2 | 15.886 % |
c ==============================================================================
c [1mFound solution: 5546607[0m
c ---[   0]---> Adder-cost: 10631   maxlim: 2940636   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27381 |  196862   598439 |   65620   26643   226329     8.5 | 15.886 % |
c |     27481 |  196862   598439 |   72182   26743   226818     8.5 | 12.776 % |
c |     27633 |  196862   598439 |   79400   26895   228559     8.5 | 12.776 % |
c |     27858 |  196831   598367 |   87340   27115   229812     8.5 | 12.795 % |
c |     28198 |  196821   598344 |   96074   27454   234688     8.5 | 12.800 % |
c |     28704 |  196816   598332 |  105681   27959   238050     8.5 | 12.804 % |
c |     29463 |  196789   598269 |  116249   28715   244784     8.5 | 12.827 % |
c |     30602 |  196645   597933 |  127874   29837   257229     8.6 | 12.903 % |
c |     32310 |  196572   597740 |  140662   31537   288602     9.2 | 12.937 % |
c |     34872 |  196497   597566 |  154728   34085   327172     9.6 | 12.982 % |
c |     38716 |  196415   597377 |  170201   37920   408071    10.8 | 13.033 % |
c ==============================================================================
c [1mFound solution: 5464409[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3022834   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40674 |  196375   597463 |   65458   39873   440595    11.0 | 13.033 % |
c |     40774 |  196361   597431 |   72003   39971   440993    11.0 | 13.102 % |
c |     40926 |  196361   597431 |   79204   40123   441640    11.0 | 13.102 % |
c |     41151 |  196361   597431 |   87124   40348   445423    11.0 | 13.102 % |
c |     41489 |  196361   597431 |   95837   40686   449468    11.0 | 13.102 % |
c |     41995 |  196361   597431 |  105420   41192   456314    11.1 | 13.102 % |
c |     42756 |  196361   597431 |  115962   41953   468201    11.2 | 13.102 % |
c |     43896 |  196361   597431 |  127559   43093   507870    11.8 | 13.102 % |
c |     45605 |  196263   597204 |  140315   44787   538528    12.0 | 13.160 % |
c |     48167 |  196263   597204 |  154346   47349   640087    13.5 | 13.160 % |
c |     52011 |  196263   597204 |  169781   51193   740047    14.5 | 13.160 % |
c |     57777 |  196246   597165 |  186759   56958   936123    16.4 | 13.172 % |
c ==============================================================================
c [1mFound solution: 4979303[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3507940   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     58953 |  196205   597212 |   65401   58131   963072    16.6 | 13.172 % |
c |     59053 |  196176   597146 |   71941   58228   963450    16.5 | 13.245 % |
c |     59203 |  195987   596712 |   79135   58357   964531    16.5 | 13.350 % |
c |     59428 |  195979   596693 |   87048   58581   965593    16.5 | 13.355 % |
c |     59765 |  195972   596677 |   95753   58917   967368    16.4 | 13.359 % |
c |     60271 |  195962   596654 |  105328   59420   971149    16.3 | 13.367 % |
c |     61030 |  195962   596654 |  115861   60179   985365    16.4 | 13.367 % |
c |     62170 |  195962   596654 |  127448   61319  1015148    16.6 | 13.367 % |
c |     63878 |  195917   596549 |  140192   63022  1099870    17.5 | 13.395 % |
c |     66440 |  195882   596467 |  154212   65582  1154706    17.6 | 13.414 % |
c |     70284 |  195842   596376 |  169633   69423  1305384    18.8 | 13.440 % |
c |     76050 |  195759   596182 |  186596   75177  1516897    20.2 | 13.485 % |
c |     84699 |  195695   596036 |  205256   83817  2272271    27.1 | 13.524 % |
c |     97674 |  195663   595964 |  225781   96787  2891364    29.9 | 13.541 % |
c ==============================================================================
c [1mFound solution: 4309718[0m
c ---[   0]---> Adder-cost: 0   maxlim: 4177525   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    104001 |  195645   596091 |   65215  103108  3242572    31.4 | 13.541 % |
c |    104101 |  195626   596046 |   71736   19413   764607    39.4 | 13.598 % |
c |    104252 |  195591   595967 |   78910   19561   765175    39.1 | 13.617 % |
c |    104477 |  195578   595937 |   86801   19783   766247    38.7 | 13.624 % |
c |    104815 |  195578   595937 |   95481   20121   767833    38.2 | 13.624 % |
c |    105321 |  195537   595843 |  105029   20619   770380    37.4 | 13.652 % |
c |    106080 |  195457   595661 |  115532   21371   773963    36.2 | 13.699 % |
c |    107219 |  195450   595645 |  127085   22509   780010    34.7 | 13.705 % |
c |    108927 |  195320   595346 |  139794   24195   790289    32.7 | 13.787 % |
c |    111489 |  195308   595317 |  153773   26756   861791    32.2 | 13.795 % |
c |    115333 |  195166   594991 |  169150   30585   905345    29.6 | 13.881 % |
c |    121099 |  195133   594915 |  186066   36348  1124727    30.9 | 13.902 % |
c |    129749 |  195033   594688 |  204672   44987  1286747    28.6 | 13.962 % |
c |    142723 |  195005   594623 |  225139   57958  1605740    27.7 | 13.978 % |
c |    162184 |  194983   594565 |  247653   77413  2465958    31.9 | 13.992 % |
c ==============================================================================
c [1mFound solution: 4302747[0m
c ---[   0]---> Adder-cost: 0   maxlim: 4184496   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    182112 |  194984   594668 |   64994   97340  3835165    39.4 | 13.992 % |
c |    182212 |  194984   594668 |   71493   20413  1143629    56.0 | 14.006 % |
c |    182363 |  194972   594641 |   78642   20562  1144274    55.6 | 14.013 % |
c |    182589 |  194952   594594 |   86507   20786  1145506    55.1 | 14.028 % |
c |    182926 |  194930   594542 |   95157   21122  1147624    54.3 | 14.039 % |
c |    183433 |  194930   594542 |  104673   21629  1150269    53.2 | 14.039 % |
c |    184192 |  194914   594505 |  115140   22387  1153834    51.5 | 14.047 % |
c |    185331 |  194891   594453 |  126654   23522  1161557    49.4 | 14.060 % |
c |    187039 |  194879   594425 |  139320   25228  1172314    46.5 | 14.066 % |
c |    189601 |  194778   594193 |  153252   27781  1188064    42.8 | 14.124 % |
c |    193445 |  194716   594051 |  168577   31620  1248764    39.5 | 14.156 % |
c |    199212 |  194697   594006 |  185435   37385  1655594    44.3 | 14.167 % |
c |    207861 |  194678   593956 |  203979   46029  1911038    41.5 | 14.176 % |
c |    220836 |  194678   593956 |  224376   59004  3351981    56.8 | 14.176 % |
c |    240297 |  194377   593259 |  246814   78430  3748761    47.8 | 14.354 % |
c |    269490 |  194350   593196 |  271496  107620  5493226    51.0 | 14.373 % |
c |    313280 |  194330   593150 |  298645  151408 12103280    79.9 | 14.386 % |
c |    378964 |  194318   593122 |  328510  217089 24344104   112.1 | 14.394 % |
c ==============================================================================
c [1mFound solution: 3514344[0m
c ---[   0]---> Adder-cost: 2   maxlim: 4972899   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    460943 |  194338   593278 |   64779  299067 30336227   101.4 | 14.394 % |
c |    461043 |  194319   593234 |   71256   22220  1807280    81.3 | 14.422 % |
c |    461193 |  194293   593175 |   78382   22366  1808032    80.8 | 14.439 % |
c |    461419 |  194276   593133 |   86220   22589  1808886    80.1 | 14.449 % |
c |    461756 |  194276   593133 |   94842   22926  1810216    79.0 | 14.449 % |
c |    462262 |  194267   593112 |  104327   23430  1813261    77.4 | 14.456 % |
c |    463021 |  194241   593051 |  114759   24187  1817885    75.2 | 14.473 % |
c |    464161 |  194183   592916 |  126235   25321  1828387    72.2 | 14.507 % |
c |    465869 |  194146   592830 |  138859   27025  1842916    68.2 | 14.531 % |
c |    468431 |  194113   592755 |  152745   29583  1873186    63.3 | 14.552 % |
c |    472275 |  194085   592691 |  168020   33424  1911935    57.2 | 14.567 % |
c |    478041 |  194064   592642 |  184822   39186  2315555    59.1 | 14.578 % |
c |    486692 |  193964   592411 |  203304   47823  2447108    51.2 | 14.636 % |
c |    499666 |  193885   592227 |  223634   60782  2725103    44.8 | 14.683 % |
c |    519127 |  193875   592204 |  245998   80241  3589969    44.7 | 14.688 % |
c |    548319 |  193869   592190 |  270597  109432  5454617    49.8 | 14.692 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:  8886 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.92 0.97 0.91 2/54 8882
Raw data (stat): 8882 (runsolver) R 8881 23310 23309 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 842935318 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.93 0.97 0.91 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0002 s]
Raw data (loadavg): 0.94 0.97 0.91 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0014 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0015 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0022 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0023 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0017 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0024 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0022 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.005 s]
Raw data (loadavg): 1.15 1.00 0.92 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.006 s]
Raw data (loadavg): 1.12 1.00 0.92 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.006 s]
Raw data (loadavg): 1.10 1.00 0.92 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.006 s]
Raw data (loadavg): 1.09 1.00 0.92 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.008 s]
Raw data (loadavg): 1.07 1.00 0.92 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.014 s]
Raw data (loadavg): 1.06 1.00 0.92 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.015 s]
Raw data (loadavg): 1.05 1.00 0.92 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.015 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.015 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.015 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.02 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.026 s]
Raw data (loadavg): 1.10 1.02 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.026 s]
Raw data (loadavg): 1.16 1.03 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.026 s]
Raw data (loadavg): 1.13 1.03 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.025 s]
Raw data (loadavg): 1.11 1.03 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.025 s]
Raw data (loadavg): 1.10 1.03 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.025 s]
Raw data (loadavg): 1.08 1.03 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.025 s]
Raw data (loadavg): 1.07 1.03 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.026 s]
Raw data (loadavg): 1.06 1.02 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.026 s]
Raw data (loadavg): 1.05 1.02 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.026 s]
Raw data (loadavg): 1.04 1.02 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.026 s]
Raw data (loadavg): 1.03 1.02 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.027 s]
Raw data (loadavg): 1.03 1.02 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.026 s]
Raw data (loadavg): 1.02 1.02 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.026 s]
Raw data (loadavg): 1.02 1.02 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.027 s]
Raw data (loadavg): 1.02 1.02 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.026 s]
Raw data (loadavg): 1.01 1.02 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.026 s]
Raw data (loadavg): 1.01 1.02 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.026 s]
Raw data (loadavg): 1.01 1.01 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.026 s]
Raw data (loadavg): 1.01 1.01 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.026 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.026 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.027 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.026 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.026 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.027 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.026 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.026 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 8886
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.03 s]
Raw data (loadavg): 1.08 1.02 0.94 3/59 8936
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.03 s]
Raw data (loadavg): 1.21 1.05 0.95 2/55 8939
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.029 s]
Raw data (loadavg): 1.18 1.05 0.95 2/55 8939
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.03 s]
Raw data (loadavg): 1.15 1.04 0.95 2/55 8939
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.03 s]
Raw data (loadavg): 1.13 1.04 0.95 2/55 8939
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.03 s]
Raw data (loadavg): 1.11 1.04 0.95 2/55 8939
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.03 s]
Raw data (loadavg): 1.09 1.04 0.95 2/55 8939
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.03 s]
Raw data (loadavg): 1.08 1.04 0.95 2/55 8941
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.03 s]
Raw data (loadavg): 1.06 1.03 0.95 2/55 8941
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.03 s]
Raw data (loadavg): 1.05 1.03 0.95 2/55 8941
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.03 s]
Raw data (loadavg): 1.05 1.03 0.95 2/55 8941
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.03 s]
Raw data (loadavg): 1.04 1.03 0.95 2/55 8941
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.03 s]
Raw data (loadavg): 1.03 1.03 0.95 2/55 8941
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.03 s]
Raw data (loadavg): 1.03 1.03 0.95 2/55 8941
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.03 s]
Raw data (loadavg): 1.02 1.03 0.95 2/55 8941
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.03 s]
Raw data (loadavg): 1.02 1.02 0.95 2/55 8941
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.03 s]
Raw data (loadavg): 1.02 1.02 0.95 2/55 8941
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.03 s]
Raw data (loadavg): 1.01 1.02 0.95 2/55 8941
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.03 s]
Raw data (loadavg): 1.01 1.02 0.95 2/55 8941
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.03 s]
Raw data (loadavg): 1.01 1.02 0.95 2/55 8941
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.03 s]
Raw data (loadavg): 1.01 1.02 0.95 2/55 8941
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.02 0.95 2/55 8941
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.02 0.95 2/55 8941
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.02 0.95 2/55 8941
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.02 0.95 2/55 8941
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.01 0.95 2/55 8941
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.03 s]
Raw data (loadavg): 1.00 1.01 0.95 2/55 8941
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.03 s]
Raw data (loadavg): 1.00 1.01 0.95 2/55 8941
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.78 s]
Raw data (loadavg): 1.00 1.01 0.95 1/53 8941
Raw data (stat): 8882 (minisat+_script) S 8881 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842935318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

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