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-ran4x64.opb
MD5SUM	6a6f7751d9c11fcafeb386712eac2f08
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3097606
Optimality of the best value was proved	NO
Number of terms in the objective function	5376
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	1473474440
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	1473474440
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	433.74
Number of variables	5376
Total number of constraints	324
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	324
Minimum length of a constraint	21
Maximum length of a constraint	1280
Trace number 31276

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc28 THE 2005-05-25 23:44:05 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22672 boxname=wulflinc28 idbench=1488 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  6a6f7751d9c11fcafeb386712eac2f08  /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-ran4x64.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-ran4x64.opb
IDLAUNCH: 22672
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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:        808596 kB
Buffers:         31280 kB
Cached:         173808 kB
SwapCached:        748 kB
Active:          25492 kB
Inactive:       181896 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        808344 kB
SwapTotal:     2097640 kB
SwapFree:      2096192 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5444 kB
Slab:            13012 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-26 00:04:35 (client local time) WITH STATUS 152 IN 1229.9 SECONDS
stats: 22672 7 1229.9 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 392 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 390]---> Adder-cost: 1332   maxlim: 117952   bits: 18/17
c ---[ 388]---> Adder-cost: 1332   maxlim: 118336   bits: 18/17
c ---[ 386]---> Adder-cost: 1332   maxlim: 115520   bits: 18/17
c ---[ 384]---> Adder-cost: 1332   maxlim: 91584   bits: 18/17
c ---[ 382]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[ 380]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 378]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2
c ---[ 376]---> Sorter-cost:  479     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 374]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 372]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 370]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 368]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 366]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 364]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[ 362]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 360]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2
c ---[ 358]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 356]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[ 354]---> Sorter-cost:  279     Base: 2 2 2 2 2 2 2
c ---[ 352]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 350]---> Sorter-cost:  479     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 348]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2
c ---[ 346]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 344]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2
c ---[ 342]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 340]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2
c ---[ 338]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 336]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 334]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 332]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2
c ---[ 330]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 328]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 326]---> Sorter-cost:  279     Base: 2 2 2 2 2 2 2
c ---[ 324]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[ 322]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 320]---> Sorter-cost:  279     Base: 2 2 2 2 2 2 2
c ---[ 318]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[ 316]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[ 314]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 312]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[ 310]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2
c ---[ 308]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[ 306]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2
c ---[ 304]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 302]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 300]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 298]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2
c ---[ 296]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 294]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 292]---> Sorter-cost:  479     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 290]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[ 288]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[ 286]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[ 284]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 282]---> Sorter-cost:  479     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 280]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 278]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 276]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2
c ---[ 274]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[ 272]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[ 270]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2
c ---[ 268]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[ 266]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 264]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[ 262]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 260]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2
c ---[ 258]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[ 256]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2
c ---[ 255]---> BDD-cost:   12
c ---[ 254]---> BDD-cost:   12
c ---[ 253]---> BDD-cost:   11
c ---[ 252]---> BDD-cost:   12
c ---[ 251]---> BDD-cost:    9
c ---[ 250]---> BDD-cost:   12
c ---[ 249]---> BDD-cost:   11
c ---[ 248]---> BDD-cost:   12
c ---[ 247]---> BDD-cost:   10
c ---[ 246]---> BDD-cost:   13
c ---[ 245]---> BDD-cost:   11
c ---[ 244]---> BDD-cost:   15
c ---[ 243]---> BDD-cost:   16
c ---[ 242]---> BDD-cost:   19
c ---[ 241]---> BDD-cost:   17
c ---[ 240]---> BDD-cost:   10
c ---[ 239]---> BDD-cost:   15
c ---[ 238]---> BDD-cost:   13
c ---[ 237]---> BDD-cost:   13
c ---[ 236]---> BDD-cost:   11
c ---[ 235]---> BDD-cost:   13
c ---[ 234]---> BDD-cost:   15
c ---[ 233]---> BDD-cost:   19
c ---[ 232]---> BDD-cost:   17
c ---[ 231]---> BDD-cost:   16
c ---[ 230]---> BDD-cost:   15
c ---[ 229]---> BDD-cost:   11
c ---[ 228]---> BDD-cost:   13
c ---[ 227]---> BDD-cost:   11
c ---[ 226]---> BDD-cost:   11
c ---[ 225]---> BDD-cost:   17
c ---[ 224]---> BDD-cost:   13
c ---[ 223]---> BDD-cost:   15
c ---[ 222]---> BDD-cost:   12
c ---[ 221]---> BDD-cost:   12
c ---[ 220]---> BDD-cost:   12
c ---[ 219]---> BDD-cost:   12
c ---[ 218]---> BDD-cost:   16
c ---[ 217]---> BDD-cost:   14
c ---[ 216]---> BDD-cost:   14
c ---[ 215]---> BDD-cost:   10
c ---[ 214]---> BDD-cost:   10
c ---[ 213]---> BDD-cost:   13
c ---[ 212]---> BDD-cost:   10
c ---[ 211]---> BDD-cost:   11
c ---[ 210]---> BDD-cost:   19
c ---[ 209]---> BDD-cost:   14
c ---[ 208]---> BDD-cost:   16
c ---[ 207]---> BDD-cost:   12
c ---[ 206]---> BDD-cost:   14
c ---[ 205]---> BDD-cost:   12
c ---[ 204]---> BDD-cost:   17
c ---[ 203]---> BDD-cost:   11
c ---[ 202]---> BDD-cost:   15
c ---[ 201]---> BDD-cost:   11
c ---[ 200]---> BDD-cost:   11
c ---[ 199]---> BDD-cost:    9
c ---[ 198]---> BDD-cost:   12
c ---[ 197]---> BDD-cost:   14
c ---[ 196]---> BDD-cost:   17
c ---[ 195]---> BDD-cost:   11
c ---[ 194]---> BDD-cost:   12
c ---[ 193]---> BDD-cost:   11
c ---[ 192]---> BDD-cost:   15
c ---[ 191]---> BDD-cost:   11
c ---[ 190]---> BDD-cost:   15
c ---[ 189]---> BDD-cost:   15
c ---[ 188]---> BDD-cost:   10
c ---[ 187]---> BDD-cost:   17
c ---[ 186]---> BDD-cost:   17
c ---[ 185]---> BDD-cost:   12
c ---[ 184]---> BDD-cost:    9
c ---[ 183]---> BDD-cost:   11
c ---[ 182]---> BDD-cost:   12
c ---[ 181]---> BDD-cost:    9
c ---[ 180]---> BDD-cost:   12
c ---[ 179]---> BDD-cost:   11
c ---[ 178]---> BDD-cost:   12
c ---[ 177]---> BDD-cost:   10
c ---[ 176]---> BDD-cost:   11
c ---[ 175]---> BDD-cost:   13
c ---[ 174]---> BDD-cost:   11
c ---[ 173]---> BDD-cost:   15
c ---[ 172]---> BDD-cost:   16
c ---[ 171]---> BDD-cost:   17
c ---[ 170]---> BDD-cost:   10
c ---[ 169]---> BDD-cost:   15
c ---[ 168]---> BDD-cost:   13
c ---[ 167]---> BDD-cost:   13
c ---[ 166]---> BDD-cost:   11
c ---[ 165]---> BDD-cost:   15
c ---[ 164]---> BDD-cost:   13
c ---[ 163]---> BDD-cost:   15
c ---[ 162]---> BDD-cost:   19
c ---[ 161]---> BDD-cost:   17
c ---[ 160]---> BDD-cost:   15
c ---[ 159]---> BDD-cost:   11
c ---[ 158]---> BDD-cost:   13
c ---[ 157]---> BDD-cost:   11
c ---[ 156]---> BDD-cost:   11
c ---[ 155]---> BDD-cost:   17
c ---[ 154]---> BDD-cost:   11
c ---[ 153]---> BDD-cost:   13
c ---[ 152]---> BDD-cost:   15
c ---[ 151]---> BDD-cost:   12
c ---[ 150]---> BDD-cost:   12
c ---[ 149]---> BDD-cost:   12
c ---[ 148]---> BDD-cost:   16
c ---[ 147]---> BDD-cost:   14
c ---[ 146]---> BDD-cost:   14
c ---[ 145]---> BDD-cost:   10
c ---[ 144]---> BDD-cost:   10
c ---[ 143]---> BDD-cost:   12
c ---[ 142]---> BDD-cost:   11
c ---[ 141]---> BDD-cost:   13
c ---[ 140]---> BDD-cost:   10
c ---[ 139]---> BDD-cost:   11
c ---[ 138]---> BDD-cost:   19
c ---[ 137]---> BDD-cost:   16
c ---[ 136]---> BDD-cost:   12
c ---[ 135]---> BDD-cost:   14
c ---[ 134]---> BDD-cost:   12
c ---[ 133]---> BDD-cost:   17
c ---[ 132]---> BDD-cost:   11
c ---[ 131]---> BDD-cost:    9
c ---[ 130]---> BDD-cost:   15
c ---[ 129]---> BDD-cost:   11
c ---[ 128]---> BDD-cost:   11
c ---[ 127]---> BDD-cost:    9
c ---[ 126]---> BDD-cost:   14
c ---[ 125]---> BDD-cost:   17
c ---[ 124]---> BDD-cost:   11
c ---[ 123]---> BDD-cost:   12
c ---[ 122]---> BDD-cost:   11
c ---[ 121]---> BDD-cost:   15
c ---[ 120]---> BDD-cost:   14
c ---[ 119]---> BDD-cost:   11
c ---[ 118]---> BDD-cost:   15
c ---[ 117]---> BDD-cost:   15
c ---[ 116]---> BDD-cost:   10
c ---[ 115]---> BDD-cost:   17
c ---[ 114]---> BDD-cost:   12
c ---[ 113]---> BDD-cost:    9
c ---[ 112]---> BDD-cost:   11
c ---[ 111]---> BDD-cost:   12
c ---[ 110]---> BDD-cost:    9
c ---[ 109]---> BDD-cost:   17
c ---[ 108]---> BDD-cost:   12
c ---[ 107]---> BDD-cost:   11
c ---[ 106]---> BDD-cost:   12
c ---[ 105]---> BDD-cost:   10
c ---[ 104]---> BDD-cost:   13
c ---[ 103]---> BDD-cost:   11
c ---[ 102]---> BDD-cost:   15
c ---[ 101]---> BDD-cost:   16
c ---[ 100]---> BDD-cost:   17
c ---[  99]---> BDD-cost:   10
c ---[  98]---> BDD-cost:   11
c ---[  97]---> BDD-cost:   15
c ---[  96]---> BDD-cost:   13
c ---[  95]---> BDD-cost:   13
c ---[  94]---> BDD-cost:   11
c ---[  93]---> BDD-cost:   13
c ---[  92]---> BDD-cost:   15
c ---[  91]---> BDD-cost:   19
c ---[  90]---> BDD-cost:   17
c ---[  89]---> BDD-cost:   15
c ---[  88]---> BDD-cost:   11
c ---[  87]---> BDD-cost:   12
c ---[  86]---> BDD-cost:   13
c ---[  85]---> BDD-cost:   11
c ---[  84]---> BDD-cost:   11
c ---[  83]---> BDD-cost:   17
c ---[  82]---> BDD-cost:   13
c ---[  81]---> BDD-cost:   15
c ---[  80]---> BDD-cost:   11
c ---[  79]---> BDD-cost:   15
c ---[  78]---> BDD-cost:   11
c ---[  77]---> BDD-cost:   15
c ---[  76]---> BDD-cost:   16
c ---[  75]---> BDD-cost:   15
c ---[  74]---> BDD-cost:   10
c ---[  73]---> BDD-cost:   17
c ---[  72]---> BDD-cost:   12
c ---[  71]---> BDD-cost:    9
c ---[  70]---> BDD-cost:   11
c ---[  69]---> BDD-cost:   12
c ---[  68]---> BDD-cost:    9
c ---[  67]---> BDD-cost:   12
c ---[  66]---> BDD-cost:   11
c ---[  65]---> BDD-cost:   14
c ---[  64]---> BDD-cost:   12
c ---[  63]---> BDD-cost:   10
c ---[  62]---> BDD-cost:   13
c ---[  61]---> BDD-cost:   11
c ---[  60]---> BDD-cost:   15
c ---[  59]---> BDD-cost:   16
c ---[  58]---> BDD-cost:   17
c ---[  57]---> BDD-cost:   10
c ---[  56]---> BDD-cost:   15
c ---[  55]---> BDD-cost:   13
c ---[  54]---> BDD-cost:   14
c ---[  53]---> BDD-cost:   13
c ---[  52]---> BDD-cost:   11
c ---[  51]---> BDD-cost:   13
c ---[  50]---> BDD-cost:   15
c ---[  49]---> BDD-cost:   19
c ---[  48]---> BDD-cost:   17
c ---[  47]---> BDD-cost:   15
c ---[  46]---> BDD-cost:   11
c ---[  45]---> BDD-cost:   13
c ---[  44]---> BDD-cost:   11
c ---[  43]---> BDD-cost:   10
c ---[  42]---> BDD-cost:   11
c ---[  41]---> BDD-cost:   17
c ---[  40]---> BDD-cost:   13
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   12
c ---[  37]---> BDD-cost:   12
c ---[  36]---> BDD-cost:   12
c ---[  35]---> BDD-cost:   16
c ---[  34]---> BDD-cost:   14
c ---[  33]---> BDD-cost:   14
c ---[  32]---> BDD-cost:   10
c ---[  31]---> BDD-cost:   10
c ---[  30]---> BDD-cost:   10
c ---[  29]---> BDD-cost:   13
c ---[  28]---> BDD-cost:   10
c ---[  27]---> BDD-cost:   11
c ---[  26]---> BDD-cost:   19
c ---[  25]---> BDD-cost:   16
c ---[  24]---> BDD-cost:   12
c ---[  23]---> BDD-cost:   14
c ---[  22]---> BDD-cost:   12
c ---[  21]---> BDD-cost:   13
c ---[  20]---> BDD-cost:   17
c ---[  19]---> BDD-cost:   11
c ---[  18]---> BDD-cost:   15
c ---[  17]---> BDD-cost:   11
c ---[  16]---> BDD-cost:   11
c ---[  15]---> BDD-cost:    9
c ---[  14]---> BDD-cost:   14
c ---[  13]---> BDD-cost:   17
c ---[  12]---> BDD-cost:   11
c ---[  11]---> BDD-cost:   12
c ---[  10]---> BDD-cost:   10
c ---[   9]---> BDD-cost:   11
c ---[   8]---> BDD-cost:   15
c ---[   7]---> BDD-cost:   11
c ---[   6]---> BDD-cost:   15
c ---[   5]---> BDD-cost:   15
c ---[   4]---> BDD-cost:   10
c ---[   3]---> BDD-cost:   17
c ---[   2]---> BDD-cost:   12
c ---[   1]---> BDD-cost:    9
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   98034   276354 |   32678       0        0     nan |  0.000 % |
c |       100 |   97988   276250 |   35945      94      282     3.0 | 14.168 % |
c |       250 |   97957   276176 |   39540     240      741     3.1 | 14.196 % |
c |       475 |   97945   276150 |   43494     463     1397     3.0 | 14.208 % |
c |       812 |   97893   276006 |   47843     793     2406     3.0 | 14.249 % |
c |      1318 |   97773   275734 |   52628    1286     3943     3.1 | 14.365 % |
c |      2077 |   97624   275371 |   57891    2029     6233     3.1 | 14.496 % |
c |      3216 |   97348   274739 |   63680    3137    10122     3.2 | 14.756 % |
c |      4924 |   97152   274269 |   70048    4823    17855     3.7 | 14.931 % |
c |      7486 |   96815   273435 |   77053    7333    34649     4.7 | 15.222 % |
c |     11330 |   96663   273090 |   84758   11158    78997     7.1 | 15.369 % |
c |     17096 |   96583   272912 |   93234   16916   234262    13.8 | 15.451 % |
c |     25747 |   96409   272495 |  102557   25542   452504    17.7 | 15.610 % |
c |     38721 |   95946   271457 |  112813   38472   788366    20.5 | 16.067 % |
c ==============================================================================
c [1mFound solution: 5714495[0m
c ---[   0]---> Adder-cost: 10520   maxlim: 2665289   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     57714 |  169433   534035 |   56477   57453  1687223    29.4 | 16.067 % |
c |     57814 |  169433   534035 |   62124   57553  1688134    29.3 | 12.156 % |
c |     57964 |  169415   533993 |   68337   57702  1689117    29.3 | 12.170 % |
c |     58189 |  169415   533993 |   75170   57927  1691115    29.2 | 12.170 % |
c |     58526 |  169415   533993 |   82687   58264  1693714    29.1 | 12.170 % |
c |     59032 |  169415   533993 |   90956   58770  1698254    28.9 | 12.170 % |
c |     59791 |  169415   533993 |  100052   59529  1707616    28.7 | 12.170 % |
c |     60930 |  169375   533902 |  110057   60665  1721178    28.4 | 12.201 % |
c |     62639 |  169375   533902 |  121063   62374  1746745    28.0 | 12.201 % |
c |     65201 |  169375   533902 |  133169   64936  1787518    27.5 | 12.201 % |
c |     69047 |  169357   533860 |  146486   68780  1834500    26.7 | 12.213 % |
c |     74813 |  169321   533782 |  161135   74543  1917770    25.7 | 12.241 % |
c |     83464 |  169309   533756 |  177249   83193  2436978    29.3 | 12.250 % |
c |     96438 |  169273   533678 |  194973   96161  2970606    30.9 | 12.278 % |
c ==============================================================================
c [1mFound solution: 5575105[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2804679   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    111008 |  169247   533745 |   56415  110724  3832850    34.6 | 12.278 % |
c |    111108 |  169247   533745 |   62056   19323   782149    40.5 | 12.334 % |
c |    111258 |  169232   533711 |   68262   19472   782709    40.2 | 12.346 % |
c |    111483 |  169193   533621 |   75088   19693   783921    39.8 | 12.376 % |
c |    111820 |  169185   533604 |   82597   20027   785910    39.2 | 12.383 % |
c |    112326 |  169167   533562 |   90856   20532   788586    38.4 | 12.395 % |
c |    113085 |  169167   533562 |   99942   21291   794400    37.3 | 12.395 % |
c |    114224 |  169167   533562 |  109936   22430   824346    36.8 | 12.395 % |
c |    115934 |  169131   533480 |  120930   24138   854651    35.4 | 12.423 % |
c |    118496 |  169099   533407 |  133023   26697   927782    34.8 | 12.447 % |
c |    122340 |  169078   533359 |  146325   30540   992304    32.5 | 12.463 % |
c |    128106 |  168979   533132 |  160958   36295  1068377    29.4 | 12.539 % |
c |    136755 |  168961   533090 |  177054   44943  1558963    34.7 | 12.553 % |
c |    149729 |  168901   532956 |  194759   57911  1805632    31.2 | 12.600 % |
c |    169190 |  168889   532930 |  214235   77370  5438575    70.3 | 12.609 % |
c |    198383 |  168824   532783 |  235659  106556  7169408    67.3 | 12.659 % |
c |    242172 |  168767   532649 |  259225  150335  8698435    57.9 | 12.699 % |
c ==============================================================================
c [1mFound solution: 5248200[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3131584   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    266152 |  168784   532795 |   56261  174314  9698842    55.6 | 12.699 % |
c |    266252 |  168784   532795 |   61887   19110   630793    33.0 | 12.719 % |
c |    266402 |  168784   532795 |   68075   19260   631996    32.8 | 12.719 % |
c |    266627 |  168784   532795 |   74883   19485   634087    32.5 | 12.719 % |
c |    266964 |  168784   532795 |   82371   19822   636531    32.1 | 12.719 % |
c |    267470 |  168746   532709 |   90608   20322   673002    33.1 | 12.747 % |
c |    268230 |  168746   532709 |   99669   21082   678420    32.2 | 12.747 % |
c |    269369 |  168742   532700 |  109636   22219   684766    30.8 | 12.749 % |
c |    271077 |  168742   532700 |  120600   23927   695064    29.0 | 12.749 % |
c |    273640 |  168729   532670 |  132660   26488   743404    28.1 | 12.759 % |
c |    277484 |  168681   532561 |  145926   30327   773877    25.5 | 12.796 % |
c |    283250 |  168670   532536 |  160519   36090   999639    27.7 | 12.803 % |
c |    291899 |  168610   532400 |  176571   44729  1246640    27.9 | 12.846 % |
c |    304873 |  168598   532374 |  194228   57702  1921293    33.3 | 12.855 % |
c |    324334 |  168552   532271 |  213651   77158  2548581    33.0 | 12.886 % |
c |    353528 |  168522   532203 |  235016  106349  4092464    38.5 | 12.909 % |
c |    397317 |  168522   532203 |  258517  150138  9427883    62.8 | 12.909 % |
c |    463001 |  168486   532120 |  284369  215818 15896902    73.7 | 12.938 % |
c ==============================================================================
c [1mFound solution: 5026432[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3353352   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    528003 |  168481   532209 |   56160  280814 25690474    91.5 | 12.938 % |
c |    528103 |  168481   532209 |   61776   28172  1663901    59.1 | 12.971 % |
c |    528256 |  168481   532209 |   67953   28325  1666532    58.8 | 12.971 % |
c |    528481 |  168481   532209 |   74748   28550  1667970    58.4 | 12.971 % |
c |    528818 |  168477   532200 |   82223   28886  1669919    57.8 | 12.973 % |
c |    529324 |  168477   532200 |   90446   29392  1677413    57.1 | 12.973 % |
c |    530083 |  168462   532166 |   99490   30150  1710417    56.7 | 12.983 % |
c |    531222 |  168456   532152 |  109439   31288  1720961    55.0 | 12.987 % |
c |    532930 |  168456   532152 |  120383   32996  1734638    52.6 | 12.987 % |
c |    535492 |  168435   532104 |  132422   35557  1773090    49.9 | 13.004 % |
c |    539338 |  168429   532090 |  145664   39402  1934385    49.1 | 13.009 % |
c |    545105 |  168429   532090 |  160231   45169  1996888    44.2 | 13.009 % |
c |    553754 |  168429   532090 |  176254   53818  2788069    51.8 | 13.009 % |
c |    566728 |  168429   532090 |  193879   66792  3721378    55.7 | 13.009 % |
c ==============================================================================
c [1mFound solution: 4307707[0m
c ---[   0]---> Adder-cost: 0   maxlim: 4072077   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    578416 |  168443   532228 |   56147   78480  4302799    54.8 | 13.009 % |
c |    578516 |  168443   532228 |   61761   18312   634881    34.7 | 13.026 % |
c |    578666 |  168443   532228 |   67937   18462   635450    34.4 | 13.026 % |
c |    578891 |  168443   532228 |   74731   18687   636740    34.1 | 13.026 % |
c |    579229 |  168443   532228 |   82204   19025   638583    33.6 | 13.026 % |
c |    579735 |  168443   532228 |   90425   19531   641502    32.8 | 13.026 % |
c |    580494 |  168443   532228 |   99467   20290   645314    31.8 | 13.026 % |
c |    581634 |  168443   532228 |  109414   21430   652543    30.4 | 13.026 % |
c |    583342 |  168443   532228 |  120356   23138   673042    29.1 | 13.026 % |
c |    585904 |  168443   532228 |  132391   25700   693970    27.0 | 13.026 % |
c |    589750 |  168443   532228 |  145630   29546   778192    26.3 | 13.026 % |
c |    595518 |  168407   532146 |  160193   35311   885682    25.1 | 13.054 % |
c |    604168 |  168407   532146 |  176213   43961  1285145    29.2 | 13.054 % |
c |    617142 |  168385   532096 |  193834   56931  1674116    29.4 | 13.071 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 11647 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.91 0.95 0.90 2/54 11643
Raw data (stat): 11643 (runsolver) R 11642 24821 24820 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 842941265 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.0008 s]
Raw data (loadavg): 0.93 0.95 0.90 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.0006 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.001 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.0007 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.0016 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.0011 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.0008 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.0018 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.0012 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.017 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.133 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.133 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.133 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.133 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.133 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.133 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.133 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.134 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.134 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.134 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.135 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.134 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.136 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.136 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.136 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.137 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.136 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.137 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.137 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.137 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.137 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.137 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.137 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.137 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.137 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11647
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.138 s]
Raw data (loadavg): 0.99 0.97 0.91 3/58 11688
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.139 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 11700
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.139 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 11700
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.139 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 11700
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.14 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 11700
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.14 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 11700
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.14 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 11700
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.14 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 11702
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.14 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 11702
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.14 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 11702
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.14 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 11702
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.14 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 11702
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.14 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 11702
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.14 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 11702
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.14 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11702
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.14 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11702
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.14 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11702
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.14 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11702
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.14 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11702
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.14 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11702
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.14 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11702
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.14 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11702
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.14 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11702
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.14 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11702
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.14 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11702
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.14 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11702
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.14 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11702
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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 0.99 0.91 1/53 11702
Raw data (stat): 11643 (minisat+_script) S 11642 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842941265 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.9
CPU user time (s): 1228.66
CPU system time (s): 1.24581
CPU usage (%): 100.01
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####