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-ran8x32.opb
MD5SUM	ff0017de67077abd1f68238274b64e50
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1695644
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	1517603678
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	1517603678
Number of bits of the biggest sum of numbers	31
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.03
Number of variables	5376
Total number of constraints	296
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	296
Minimum length of a constraint	21
Maximum length of a constraint	640
Trace number 31279

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        900232 kB
Buffers:         22040 kB
Cached:          92196 kB
SwapCached:        412 kB
Active:          17816 kB
Inactive:        98776 kB
HighTotal:      131008 kB
HighFree:       104580 kB
LowTotal:       903652 kB
LowFree:        795652 kB
SwapTotal:     2097136 kB
SwapFree:      2096060 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5948 kB
Slab:            12288 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-26 00:05:31 (client local time) WITH STATUS 152 IN 1229.88 SECONDS
stats: 22674 7 1229.88 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 336 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 334]---> Adder-cost: 646   maxlim: 45920   bits: 16/16
c ---[ 332]---> Adder-cost: 670   maxlim: 69856   bits: 17/17
c ---[ 330]---> Adder-cost: 670   maxlim: 67552   bits: 17/17
c ---[ 328]---> Adder-cost: 670   maxlim: 71392   bits: 17/17
c ---[ 326]---> Adder-cost: 670   maxlim: 71904   bits: 17/17
c ---[ 324]---> Adder-cost: 670   maxlim: 71904   bits: 17/17
c ---[ 322]---> Adder-cost: 670   maxlim: 70368   bits: 17/17
c ---[ 320]---> Adder-cost: 670   maxlim: 64608   bits: 17/16
c ---[ 318]---> Sorter-cost: 1053     Base: 2 2 2 2 2 2 2 2
c ---[ 316]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 314]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[ 312]---> Sorter-cost: 1661     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 310]---> Sorter-cost: 1525     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 308]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 306]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 304]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[ 302]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 300]---> Sorter-cost:  919     Base: 2 2 2 2 2 2 2
c ---[ 298]---> Sorter-cost: 1525     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 296]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[ 294]---> Sorter-cost: 1661     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 292]---> Sorter-cost: 1053     Base: 2 2 2 2 2 2 2 2
c ---[ 290]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[ 288]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[ 286]---> Sorter-cost: 1525     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 284]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 282]---> Sorter-cost: 1053     Base: 2 2 2 2 2 2 2 2
c ---[ 280]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[ 278]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[ 276]---> Sorter-cost: 1661     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 274]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 272]---> Sorter-cost: 1053     Base: 2 2 2 2 2 2 2 2
c ---[ 270]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 268]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 266]---> Sorter-cost: 1525     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 264]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[ 262]---> Sorter-cost: 1053     Base: 2 2 2 2 2 2 2 2
c ---[ 260]---> Sorter-cost: 1525     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 258]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 256]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 255]---> BDD-cost:   10
c ---[ 254]---> BDD-cost:   15
c ---[ 253]---> BDD-cost:   12
c ---[ 252]---> BDD-cost:   16
c ---[ 251]---> BDD-cost:   13
c ---[ 250]---> BDD-cost:   10
c ---[ 249]---> BDD-cost:   16
c ---[ 248]---> BDD-cost:   14
c ---[ 247]---> BDD-cost:   15
c ---[ 246]---> BDD-cost:   12
c ---[ 245]---> BDD-cost:   16
c ---[ 244]---> BDD-cost:   16
c ---[ 243]---> BDD-cost:   15
c ---[ 242]---> BDD-cost:   15
c ---[ 241]---> BDD-cost:   12
c ---[ 240]---> BDD-cost:   13
c ---[ 239]---> BDD-cost:   14
c ---[ 238]---> BDD-cost:    9
c ---[ 237]---> BDD-cost:   16
c ---[ 236]---> BDD-cost:   11
c ---[ 235]---> BDD-cost:   11
c ---[ 234]---> BDD-cost:   13
c ---[ 233]---> BDD-cost:   13
c ---[ 232]---> BDD-cost:   17
c ---[ 231]---> BDD-cost:   15
c ---[ 230]---> BDD-cost:   15
c ---[ 229]---> BDD-cost:   10
c ---[ 228]---> BDD-cost:   12
c ---[ 227]---> BDD-cost:   12
c ---[ 226]---> BDD-cost:   18
c ---[ 225]---> BDD-cost:   15
c ---[ 224]---> BDD-cost:   15
c ---[ 223]---> BDD-cost:   15
c ---[ 222]---> BDD-cost:   10
c ---[ 221]---> BDD-cost:   15
c ---[ 220]---> BDD-cost:   15
c ---[ 219]---> BDD-cost:   17
c ---[ 218]---> BDD-cost:   11
c ---[ 217]---> BDD-cost:   16
c ---[ 216]---> BDD-cost:   13
c ---[ 215]---> BDD-cost:   10
c ---[ 214]---> BDD-cost:   16
c ---[ 213]---> BDD-cost:   14
c ---[ 212]---> BDD-cost:   15
c ---[ 211]---> BDD-cost:   12
c ---[ 210]---> BDD-cost:   17
c ---[ 209]---> BDD-cost:   12
c ---[ 208]---> BDD-cost:   16
c ---[ 207]---> BDD-cost:   15
c ---[ 206]---> BDD-cost:   12
c ---[ 205]---> BDD-cost:   13
c ---[ 204]---> BDD-cost:   14
c ---[ 203]---> BDD-cost:    9
c ---[ 202]---> BDD-cost:   16
c ---[ 201]---> BDD-cost:   11
c ---[ 200]---> BDD-cost:   11
c ---[ 199]---> BDD-cost:   13
c ---[ 198]---> BDD-cost:   13
c ---[ 197]---> BDD-cost:   13
c ---[ 196]---> BDD-cost:   17
c ---[ 195]---> BDD-cost:   15
c ---[ 194]---> BDD-cost:   10
c ---[ 193]---> BDD-cost:   12
c ---[ 192]---> BDD-cost:   12
c ---[ 191]---> BDD-cost:   18
c ---[ 190]---> BDD-cost:   15
c ---[ 189]---> BDD-cost:   15
c ---[ 188]---> BDD-cost:   15
c ---[ 187]---> BDD-cost:   14
c ---[ 186]---> BDD-cost:   10
c ---[ 185]---> BDD-cost:   15
c ---[ 184]---> BDD-cost:   17
c ---[ 183]---> BDD-cost:   11
c ---[ 182]---> BDD-cost:   16
c ---[ 181]---> BDD-cost:   13
c ---[ 180]---> BDD-cost:   10
c ---[ 179]---> BDD-cost:   16
c ---[ 178]---> BDD-cost:   14
c ---[ 177]---> BDD-cost:   15
c ---[ 176]---> BDD-cost:    9
c ---[ 175]---> BDD-cost:   12
c ---[ 174]---> BDD-cost:   17
c ---[ 173]---> BDD-cost:   16
c ---[ 172]---> BDD-cost:   15
c ---[ 171]---> BDD-cost:   12
c ---[ 170]---> BDD-cost:   13
c ---[ 169]---> BDD-cost:   14
c ---[ 168]---> BDD-cost:    9
c ---[ 167]---> BDD-cost:   16
c ---[ 166]---> BDD-cost:   11
c ---[ 165]---> BDD-cost:   15
c ---[ 164]---> BDD-cost:   11
c ---[ 163]---> BDD-cost:   13
c ---[ 162]---> BDD-cost:   13
c ---[ 161]---> BDD-cost:   17
c ---[ 160]---> BDD-cost:   15
c ---[ 159]---> BDD-cost:   10
c ---[ 158]---> BDD-cost:   12
c ---[ 157]---> BDD-cost:   12
c ---[ 156]---> BDD-cost:   18
c ---[ 155]---> BDD-cost:   15
c ---[ 154]---> BDD-cost:   11
c ---[ 153]---> BDD-cost:   15
c ---[ 152]---> BDD-cost:   15
c ---[ 151]---> BDD-cost:   10
c ---[ 150]---> BDD-cost:   15
c ---[ 149]---> BDD-cost:   17
c ---[ 148]---> BDD-cost:   11
c ---[ 147]---> BDD-cost:   16
c ---[ 146]---> BDD-cost:   13
c ---[ 145]---> BDD-cost:   10
c ---[ 144]---> BDD-cost:   16
c ---[ 143]---> BDD-cost:   15
c ---[ 142]---> BDD-cost:   11
c ---[ 141]---> BDD-cost:   14
c ---[ 140]---> BDD-cost:   15
c ---[ 139]---> BDD-cost:   12
c ---[ 138]---> BDD-cost:   19
c ---[ 137]---> BDD-cost:   16
c ---[ 136]---> BDD-cost:   15
c ---[ 135]---> BDD-cost:   12
c ---[ 134]---> BDD-cost:   13
c ---[ 133]---> BDD-cost:   14
c ---[ 132]---> BDD-cost:    9
c ---[ 131]---> BDD-cost:   13
c ---[ 130]---> BDD-cost:   16
c ---[ 129]---> BDD-cost:   11
c ---[ 128]---> BDD-cost:   11
c ---[ 127]---> BDD-cost:   13
c ---[ 126]---> BDD-cost:   13
c ---[ 125]---> BDD-cost:   17
c ---[ 124]---> BDD-cost:   15
c ---[ 123]---> BDD-cost:   10
c ---[ 122]---> BDD-cost:   12
c ---[ 121]---> BDD-cost:   12
c ---[ 120]---> BDD-cost:   13
c ---[ 119]---> BDD-cost:   18
c ---[ 118]---> BDD-cost:   15
c ---[ 117]---> BDD-cost:   15
c ---[ 116]---> BDD-cost:   15
c ---[ 115]---> BDD-cost:   10
c ---[ 114]---> BDD-cost:   15
c ---[ 113]---> BDD-cost:   17
c ---[ 112]---> BDD-cost:   11
c ---[ 111]---> BDD-cost:   16
c ---[ 110]---> BDD-cost:   13
c ---[ 109]---> BDD-cost:   15
c ---[ 108]---> BDD-cost:   10
c ---[ 107]---> BDD-cost:   16
c ---[ 106]---> BDD-cost:   14
c ---[ 105]---> BDD-cost:   15
c ---[ 104]---> BDD-cost:   12
c ---[ 103]---> BDD-cost:   19
c ---[ 102]---> BDD-cost:   16
c ---[ 101]---> BDD-cost:   15
c ---[ 100]---> BDD-cost:   12
c ---[  99]---> BDD-cost:   13
c ---[  98]---> BDD-cost:   15
c ---[  97]---> BDD-cost:   14
c ---[  96]---> BDD-cost:    9
c ---[  95]---> BDD-cost:   16
c ---[  94]---> BDD-cost:   11
c ---[  93]---> BDD-cost:   11
c ---[  92]---> BDD-cost:   13
c ---[  91]---> BDD-cost:   13
c ---[  90]---> BDD-cost:   17
c ---[  89]---> BDD-cost:   15
c ---[  88]---> BDD-cost:   10
c ---[  87]---> BDD-cost:   10
c ---[  86]---> BDD-cost:   12
c ---[  85]---> BDD-cost:   12
c ---[  84]---> BDD-cost:   18
c ---[  83]---> BDD-cost:   15
c ---[  82]---> BDD-cost:   15
c ---[  81]---> BDD-cost:   15
c ---[  80]---> BDD-cost:   12
c ---[  79]---> BDD-cost:   12
c ---[  78]---> BDD-cost:   15
c ---[  77]---> BDD-cost:   15
c ---[  76]---> BDD-cost:   11
c ---[  75]---> BDD-cost:   15
c ---[  74]---> BDD-cost:   15
c ---[  73]---> BDD-cost:   10
c ---[  72]---> BDD-cost:   15
c ---[  71]---> BDD-cost:   17
c ---[  70]---> BDD-cost:   11
c ---[  69]---> BDD-cost:   16
c ---[  68]---> BDD-cost:   13
c ---[  67]---> BDD-cost:   10
c ---[  66]---> BDD-cost:   16
c ---[  65]---> BDD-cost:   15
c ---[  64]---> BDD-cost:   14
c ---[  63]---> BDD-cost:   15
c ---[  62]---> BDD-cost:   12
c ---[  61]---> BDD-cost:   19
c ---[  60]---> BDD-cost:   16
c ---[  59]---> BDD-cost:   15
c ---[  58]---> BDD-cost:   12
c ---[  57]---> BDD-cost:   13
c ---[  56]---> BDD-cost:   14
c ---[  55]---> BDD-cost:    9
c ---[  54]---> BDD-cost:   13
c ---[  53]---> BDD-cost:   16
c ---[  52]---> BDD-cost:   11
c ---[  51]---> BDD-cost:   11
c ---[  50]---> BDD-cost:   13
c ---[  49]---> BDD-cost:   13
c ---[  48]---> BDD-cost:   17
c ---[  47]---> BDD-cost:   15
c ---[  46]---> BDD-cost:   10
c ---[  45]---> BDD-cost:   12
c ---[  44]---> BDD-cost:   12
c ---[  43]---> BDD-cost:   10
c ---[  42]---> BDD-cost:   18
c ---[  41]---> BDD-cost:   15
c ---[  40]---> BDD-cost:   15
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   10
c ---[  37]---> BDD-cost:   15
c ---[  36]---> BDD-cost:   17
c ---[  35]---> BDD-cost:   11
c ---[  34]---> BDD-cost:   16
c ---[  33]---> BDD-cost:   13
c ---[  32]---> BDD-cost:   15
c ---[  31]---> BDD-cost:   10
c ---[  30]---> BDD-cost:   16
c ---[  29]---> BDD-cost:   14
c ---[  28]---> BDD-cost:   15
c ---[  27]---> BDD-cost:   12
c ---[  26]---> BDD-cost:   19
c ---[  25]---> BDD-cost:   16
c ---[  24]---> BDD-cost:   15
c ---[  23]---> BDD-cost:   12
c ---[  22]---> BDD-cost:   13
c ---[  21]---> BDD-cost:   14
c ---[  20]---> BDD-cost:   14
c ---[  19]---> BDD-cost:    9
c ---[  18]---> BDD-cost:   16
c ---[  17]---> BDD-cost:   11
c ---[  16]---> BDD-cost:   11
c ---[  15]---> BDD-cost:   13
c ---[  14]---> BDD-cost:   13
c ---[  13]---> BDD-cost:   17
c ---[  12]---> BDD-cost:   15
c ---[  11]---> BDD-cost:   10
c ---[  10]---> BDD-cost:   15
c ---[   9]---> BDD-cost:   12
c ---[   8]---> BDD-cost:   12
c ---[   7]---> BDD-cost:   18
c ---[   6]---> BDD-cost:   15
c ---[   5]---> BDD-cost:   15
c ---[   4]---> BDD-cost:   15
c ---[   3]---> BDD-cost:   10
c ---[   2]---> BDD-cost:   15
c ---[   1]---> BDD-cost:   16
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  144205   384224 |   48068       0        0     nan |  0.000 % |
c |       101 |  143894   383508 |   52874      66      318     4.8 |  9.453 % |
c |       251 |  143657   382969 |   58162     208      800     3.8 |  9.606 % |
c |       478 |  143324   382155 |   63978     412     1563     3.8 |  9.813 % |
c |       815 |  143107   381659 |   70376     741     2835     3.8 |  9.960 % |
c |      1321 |  142938   381226 |   77413    1229     4788     3.9 | 10.059 % |
c |      2080 |  142897   381119 |   85155    1984     7876     4.0 | 10.082 % |
c |      3219 |  142439   380071 |   93670    3082    12180     4.0 | 10.373 % |
c |      4927 |  142113   379324 |  103038    4765    18996     4.0 | 10.574 % |
c |      7489 |  141435   377773 |  113341    7272    29201     4.0 | 11.019 % |
c |     11334 |  140163   374836 |  124676   11037    46404     4.2 | 11.873 % |
c |     17100 |  137982   369803 |  137143   16603    71000     4.3 | 13.307 % |
c |     25749 |  135304   363521 |  150857   24976   111133     4.4 | 15.072 % |
c |     38723 |  133208   358577 |  165943   37669   207430     5.5 | 16.472 % |
c |     58184 |  132451   356706 |  182538   57043   681358    11.9 | 16.959 % |
c |     87376 |  131994   355630 |  200791   86176  1622302    18.8 | 17.275 % |
c ==============================================================================
c [1mFound solution: 5846672[0m
c ---[   0]---> Adder-cost: 10869   maxlim: 3059662   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88349 |  208000   627194 |   69333   87149  1680166    19.3 | 17.275 % |
c |     88449 |  208000   627194 |   76266   26294   560330    21.3 | 14.065 % |
c |     88599 |  207944   627064 |   83892   26433   560917    21.2 | 14.093 % |
c |     88826 |  207870   626885 |   92282   26650   561827    21.1 | 14.129 % |
c |     89163 |  207835   626796 |  101510   26982   563525    20.9 | 14.148 % |
c |     89670 |  207740   626571 |  111661   27478   567066    20.6 | 14.198 % |
c |     90429 |  207707   626489 |  122827   28233   575230    20.4 | 14.213 % |
c |     91572 |  207707   626489 |  135110   29376   617611    21.0 | 14.213 % |
c |     93280 |  207572   626169 |  148621   31076   628301    20.2 | 14.294 % |
c |     95842 |  207384   625733 |  163483   33617   654476    19.5 | 14.401 % |
c |     99686 |  207323   625596 |  179831   37454   694987    18.6 | 14.432 % |
c |    105452 |  207166   625231 |  197815   43205   764996    17.7 | 14.520 % |
c |    114101 |  206875   624555 |  217596   51815   935660    18.1 | 14.675 % |
c ==============================================================================
c [1mFound solution: 5547096[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3359238   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    126409 |  206349   623308 |   68783   64028  1187221    18.5 | 14.675 % |
c |    126509 |  206349   623308 |   75661   64128  1188071    18.5 | 14.962 % |
c |    126659 |  206349   623308 |   83227   64278  1189378    18.5 | 14.962 % |
c |    126884 |  206349   623308 |   91550   64503  1190920    18.5 | 14.962 % |
c |    127221 |  206299   623176 |  100705   64831  1194747    18.4 | 14.989 % |
c |    127727 |  206278   623127 |  110775   65336  1199949    18.4 | 15.003 % |
c |    128487 |  206093   622615 |  121853   66070  1207898    18.3 | 15.086 % |
c |    129626 |  206082   622588 |  134038   67207  1222047    18.2 | 15.093 % |
c |    131334 |  206038   622476 |  147442   68908  1251349    18.2 | 15.111 % |
c ==============================================================================
c [1mFound solution: 5466716[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3439618   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    131675 |  205994   622471 |   68664   69242  1255958    18.1 | 15.111 % |
c |    131775 |  205975   622425 |   75530   69340  1256530    18.1 | 15.166 % |
c |    131925 |  205913   622281 |   83083   69482  1257520    18.1 | 15.204 % |
c |    132150 |  205905   622263 |   91391   69706  1259309    18.1 | 15.209 % |
c |    132488 |  205905   622263 |  100530   70044  1263601    18.0 | 15.209 % |
c |    132995 |  205872   622186 |  110584   70546  1268344    18.0 | 15.228 % |
c ==============================================================================
c [1mFound solution: 5466530[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3439804   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    133464 |  205884   622331 |   68628   71015  1276422    18.0 | 15.228 % |
c |    133564 |  205869   622295 |   75490   71114  1276861    18.0 | 15.245 % |
c |    133714 |  205850   622252 |   83039   71262  1277529    17.9 | 15.258 % |
c |    133939 |  205835   622199 |   91343   71485  1278707    17.9 | 15.259 % |
c |    134276 |  205835   622199 |  100478   71822  1282132    17.9 | 15.259 % |
c |    134783 |  205822   622167 |  110526   72328  1287623    17.8 | 15.266 % |
c |    135543 |  205822   622167 |  121578   73088  1305319    17.9 | 15.266 % |
c |    136683 |  205800   622116 |  133736   74225  1320219    17.8 | 15.280 % |
c |    138391 |  205793   622093 |  147110   75931  1402758    18.5 | 15.282 % |
c |    140953 |  205784   622062 |  161821   78491  1488559    19.0 | 15.283 % |
c |    144798 |  205774   622033 |  178003   82333  1617844    19.7 | 15.287 % |
c |    150564 |  205758   621996 |  195803   88097  1774299    20.1 | 15.297 % |
c |    159213 |  205758   621996 |  215384   96746  3310225    34.2 | 15.297 % |
c ==============================================================================
c [1mFound solution: 3443634[0m
c ---[   0]---> Adder-cost: 2   maxlim: 5462700   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    165707 |  205778   622194 |   68592  103235  3574828    34.6 | 15.297 % |
c |    165807 |  205778   622194 |   75451   27962  1484814    53.1 | 15.317 % |
c |    165957 |  205778   622194 |   82996   28112  1485521    52.8 | 15.317 % |
c |    166182 |  205778   622194 |   91295   28337  1487056    52.5 | 15.317 % |
c |    166519 |  205778   622194 |  100425   28674  1488655    51.9 | 15.317 % |
c |    167025 |  205778   622194 |  110468   29180  1491649    51.1 | 15.317 % |
c |    167784 |  205766   622166 |  121514   29938  1496002    50.0 | 15.326 % |
c |    168923 |  205743   622113 |  133666   31074  1503179    48.4 | 15.336 % |
c |    170631 |  205717   622051 |  147033   32778  1519334    46.4 | 15.350 % |
c |    173193 |  205662   621923 |  161736   35334  1547784    43.8 | 15.383 % |
c |    177037 |  205618   621821 |  177909   39172  1572725    40.1 | 15.409 % |
c |    182804 |  205600   621780 |  195700   44937  1623079    36.1 | 15.421 % |
c |    191453 |  205569   621697 |  215271   53572  1865645    34.8 | 15.433 % |
c |    204428 |  205549   621649 |  236798   66543  2191016    32.9 | 15.445 % |
c |    223889 |  205478   621474 |  260478   85994  2764498    32.1 | 15.483 % |
c |    253081 |  205472   621460 |  286525  115184  4574051    39.7 | 15.488 % |
c ==============================================================================
c [1mFound solution: 3430223[0m
c ---[   0]---> Adder-cost: 0   maxlim: 5476111   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    271352 |  205471   621537 |   68490  133453  5946536    44.6 | 15.488 % |
c |    271452 |  205471   621537 |   75339   30935  1195186    38.6 | 15.503 % |
c |    271602 |  205471   621537 |   82872   31085  1195936    38.5 | 15.503 % |
c |    271827 |  205471   621537 |   91160   31310  1197550    38.2 | 15.503 % |
c |    272164 |  205462   621514 |  100276   31645  1199370    37.9 | 15.508 % |
c |    272670 |  205462   621514 |  110303   32151  1201983    37.4 | 15.508 % |
c |    273429 |  205458   621505 |  121334   32909  1208893    36.7 | 15.511 % |
c |    274568 |  205417   621400 |  133467   34037  1214441    35.7 | 15.535 % |
c |    276276 |  205411   621386 |  146814   35744  1224246    34.3 | 15.539 % |
c |    278838 |  205371   621294 |  161495   38301  1241197    32.4 | 15.558 % |
c |    282682 |  205345   621234 |  177645   42142  1266242    30.0 | 15.573 % |
c |    288448 |  205255   621019 |  195409   47898  1386965    29.0 | 15.621 % |
c |    297099 |  205240   620983 |  214950   56547  1799221    31.8 | 15.628 % |
c |    310073 |  205208   620910 |  236446   69515  2294825    33.0 | 15.647 % |
c |    329535 |  205133   620733 |  260090   88968  2969796    33.4 | 15.687 % |
c |    358727 |  205113   620687 |  286099  118157  4869169    41.2 | 15.699 % |
c ==============================================================================
c [1mFound solution: 3237337[0m
c ---[   0]---> Adder-cost: 0   maxlim: 5668997   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    381206 |  205124   620787 |   68374  140636  7009734    49.8 | 15.699 % |
c |    381306 |  205124   620787 |   75211   31656  1685810    53.3 | 15.706 % |
c |    381456 |  205124   620787 |   82732   31806  1686416    53.0 | 15.706 % |
c |    381682 |  205119   620775 |   91005   32031  1687321    52.7 | 15.709 % |
c |    382019 |  205119   620775 |  100106   32368  1688865    52.2 | 15.709 % |
c |    382525 |  205113   620761 |  110117   32873  1691688    51.5 | 15.713 % |
c |    383285 |  205108   620749 |  121128   33632  1696132    50.4 | 15.716 % |
c |    384425 |  205037   620584 |  133241   34763  1703888    49.0 | 15.758 % |
c |    386133 |  205017   620537 |  146565   36467  1718466    47.1 | 15.768 % |
c |    388695 |  205017   620537 |  161222   39029  1740018    44.6 | 15.768 % |
c |    392539 |  204978   620449 |  177344   42868  1772129    41.3 | 15.794 % |
c |    398305 |  204951   620386 |  195079   48629  1832259    37.7 | 15.813 % |
c |    406954 |  204922   620319 |  214586   57274  3240991    56.6 | 15.828 % |
c |    419929 |  204900   620267 |  236045   70246  3706617    52.8 | 15.842 % |
c |    439392 |  204894   620253 |  259650   89708  4551142    50.7 | 15.847 % |
c |    468585 |  204876   620213 |  285615  118896  5757279    48.4 | 15.859 % |
c |    512376 |  204828   620102 |  314176  162681  8221999    50.5 | 15.887 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 17995 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.91 2/54 17991
Raw data (stat): 17991 (runsolver) R 17990 1269 1268 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 784725659 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.93 0.95 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0017 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0023 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0017 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0017 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0023 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0027 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0037 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0034 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17995
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.036 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 18048
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.036 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 18048
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.037 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 18048
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.037 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 18048
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.037 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 18048
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.037 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 18048
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.037 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 18048
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.038 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 18050
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.038 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 18050
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.04 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 18050
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.04 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 18050
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.04 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 18050
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.04 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 18050
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.04 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 18050
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 18050
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 18050
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 18050
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 18050
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 18050
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 18050
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 18050
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 18050
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 18050
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 18050
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 18050
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 18050
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 18050
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 18050
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 18050
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 18050
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 18050
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 18050
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.81 s]
Raw data (loadavg): 1.00 0.99 0.91 1/53 18050
Raw data (stat): 17991 (minisat+_script) S 17990 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784725659 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.81
CPU time (s): 1229.88
CPU user time (s): 1228.83
CPU system time (s): 1.05584
CPU usage (%): 100.006
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####