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-ran10x26.opb
MD5SUM	f8a5d8e99e0f063cb10208b1e5f7bf38
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1277437
Optimality of the best value was proved	NO
Number of terms in the objective function	5460
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	1567797422
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	1567797422
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.04
Number of variables	5460
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	520
Trace number 31264

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        603772 kB
Buffers:         33596 kB
Cached:         375844 kB
SwapCached:        532 kB
Active:          32252 kB
Inactive:       379516 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        603520 kB
SwapTotal:     2097136 kB
SwapFree:      2096016 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5628 kB
Slab:            13500 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 23:59:08 (client local time) WITH STATUS 152 IN 1229.87 SECONDS
stats: 22665 7 1229.87 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 332 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 330]---> Adder-cost: 538   maxlim: 57062   bits: 16/16
c ---[ 328]---> Adder-cost: 536   maxlim: 52326   bits: 16/16
c ---[ 326]---> Adder-cost: 536   maxlim: 52582   bits: 16/16
c ---[ 324]---> Adder-cost: 536   maxlim: 53094   bits: 16/16
c ---[ 322]---> Adder-cost: 536   maxlim: 53606   bits: 16/16
c ---[ 320]---> Adder-cost: 538   maxlim: 58982   bits: 16/16
c ---[ 318]---> Adder-cost: 522   maxlim: 38502   bits: 16/16
c ---[ 316]---> Adder-cost: 538   maxlim: 57574   bits: 16/16
c ---[ 314]---> Adder-cost: 536   maxlim: 53990   bits: 16/16
c ---[ 312]---> Adder-cost: 538   maxlim: 56806   bits: 16/16
c ---[ 310]---> Adder-cost: 216   maxlim: 36214   bits: 16/16
c ---[ 308]---> Sorter-cost: 2090     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 306]---> Adder-cost: 216   maxlim: 35190   bits: 16/16
c ---[ 304]---> Sorter-cost: 2404     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 302]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 300]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 298]---> Adder-cost: 216   maxlim: 35446   bits: 16/16
c ---[ 296]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 294]---> Sorter-cost: 2090     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 292]---> Sorter-cost: 2090     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 290]---> Adder-cost: 216   maxlim: 35062   bits: 16/16
c ---[ 288]---> Sorter-cost: 2090     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 286]---> Sorter-cost: 2090     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 284]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 282]---> Adder-cost: 216   maxlim: 36854   bits: 16/16
c ---[ 280]---> Sorter-cost: 2404     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 278]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 276]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 274]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 272]---> Sorter-cost: 2090     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 270]---> Sorter-cost: 2090     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 268]---> Adder-cost: 216   maxlim: 36470   bits: 16/16
c ---[ 266]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 264]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 262]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 260]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 259]---> BDD-cost:   17
c ---[ 258]---> BDD-cost:   12
c ---[ 257]---> BDD-cost:   17
c ---[ 256]---> BDD-cost:   17
c ---[ 255]---> BDD-cost:   11
c ---[ 254]---> BDD-cost:   12
c ---[ 253]---> BDD-cost:   11
c ---[ 252]---> BDD-cost:   17
c ---[ 251]---> BDD-cost:   12
c ---[ 250]---> BDD-cost:   14
c ---[ 249]---> BDD-cost:   14
c ---[ 248]---> BDD-cost:   15
c ---[ 247]---> BDD-cost:   17
c ---[ 246]---> BDD-cost:   16
c ---[ 245]---> BDD-cost:   11
c ---[ 244]---> BDD-cost:   12
c ---[ 243]---> BDD-cost:   10
c ---[ 242]---> BDD-cost:   13
c ---[ 241]---> BDD-cost:   17
c ---[ 240]---> BDD-cost:   17
c ---[ 239]---> BDD-cost:   11
c ---[ 238]---> BDD-cost:   12
c ---[ 237]---> BDD-cost:   17
c ---[ 236]---> BDD-cost:   10
c ---[ 235]---> BDD-cost:   11
c ---[ 234]---> BDD-cost:   12
c ---[ 233]---> BDD-cost:   12
c ---[ 232]---> BDD-cost:   17
c ---[ 231]---> BDD-cost:   15
c ---[ 230]---> BDD-cost:   12
c ---[ 229]---> BDD-cost:   13
c ---[ 228]---> BDD-cost:   17
c ---[ 227]---> BDD-cost:   11
c ---[ 226]---> BDD-cost:   12
c ---[ 225]---> BDD-cost:   11
c ---[ 224]---> BDD-cost:   12
c ---[ 223]---> BDD-cost:   17
c ---[ 222]---> BDD-cost:   12
c ---[ 221]---> BDD-cost:   14
c ---[ 220]---> BDD-cost:   14
c ---[ 219]---> BDD-cost:   15
c ---[ 218]---> BDD-cost:   17
c ---[ 217]---> BDD-cost:   11
c ---[ 216]---> BDD-cost:   12
c ---[ 215]---> BDD-cost:   10
c ---[ 214]---> BDD-cost:   13
c ---[ 213]---> BDD-cost:   17
c ---[ 212]---> BDD-cost:   17
c ---[ 211]---> BDD-cost:   19
c ---[ 210]---> BDD-cost:   11
c ---[ 209]---> BDD-cost:   12
c ---[ 208]---> BDD-cost:   17
c ---[ 207]---> BDD-cost:   10
c ---[ 206]---> BDD-cost:   12
c ---[ 205]---> BDD-cost:   12
c ---[ 204]---> BDD-cost:   16
c ---[ 203]---> BDD-cost:   15
c ---[ 202]---> BDD-cost:   10
c ---[ 201]---> BDD-cost:   12
c ---[ 200]---> BDD-cost:   13
c ---[ 199]---> BDD-cost:   19
c ---[ 198]---> BDD-cost:   11
c ---[ 197]---> BDD-cost:   12
c ---[ 196]---> BDD-cost:   11
c ---[ 195]---> BDD-cost:   15
c ---[ 194]---> BDD-cost:   12
c ---[ 193]---> BDD-cost:   15
c ---[ 192]---> BDD-cost:   14
c ---[ 191]---> BDD-cost:   12
c ---[ 190]---> BDD-cost:   15
c ---[ 189]---> BDD-cost:   15
c ---[ 188]---> BDD-cost:   11
c ---[ 187]---> BDD-cost:   12
c ---[ 186]---> BDD-cost:   10
c ---[ 185]---> BDD-cost:   13
c ---[ 184]---> BDD-cost:   15
c ---[ 183]---> BDD-cost:   15
c ---[ 182]---> BDD-cost:   11
c ---[ 181]---> BDD-cost:   12
c ---[ 180]---> BDD-cost:   12
c ---[ 179]---> BDD-cost:   15
c ---[ 178]---> BDD-cost:   10
c ---[ 177]---> BDD-cost:   12
c ---[ 176]---> BDD-cost:   12
c ---[ 175]---> BDD-cost:   15
c ---[ 174]---> BDD-cost:   15
c ---[ 173]---> BDD-cost:   12
c ---[ 172]---> BDD-cost:   15
c ---[ 171]---> BDD-cost:   15
c ---[ 170]---> BDD-cost:   11
c ---[ 169]---> BDD-cost:   16
c ---[ 168]---> BDD-cost:   12
c ---[ 167]---> BDD-cost:   11
c ---[ 166]---> BDD-cost:   17
c ---[ 165]---> BDD-cost:   12
c ---[ 164]---> BDD-cost:   14
c ---[ 163]---> BDD-cost:   14
c ---[ 162]---> BDD-cost:   15
c ---[ 161]---> BDD-cost:   17
c ---[ 160]---> BDD-cost:   11
c ---[ 159]---> BDD-cost:   12
c ---[ 158]---> BDD-cost:   15
c ---[ 157]---> BDD-cost:   10
c ---[ 156]---> BDD-cost:   13
c ---[ 155]---> BDD-cost:   17
c ---[ 154]---> BDD-cost:   18
c ---[ 153]---> BDD-cost:   11
c ---[ 152]---> BDD-cost:   12
c ---[ 151]---> BDD-cost:   17
c ---[ 150]---> BDD-cost:   10
c ---[ 149]---> BDD-cost:   12
c ---[ 148]---> BDD-cost:   12
c ---[ 147]---> BDD-cost:   14
c ---[ 146]---> BDD-cost:   12
c ---[ 145]---> BDD-cost:   16
c ---[ 144]---> BDD-cost:   15
c ---[ 143]---> BDD-cost:   12
c ---[ 142]---> BDD-cost:   13
c ---[ 141]---> BDD-cost:   19
c ---[ 140]---> BDD-cost:   11
c ---[ 139]---> BDD-cost:   12
c ---[ 138]---> BDD-cost:   11
c ---[ 137]---> BDD-cost:   16
c ---[ 136]---> BDD-cost:   12
c ---[ 135]---> BDD-cost:   13
c ---[ 134]---> BDD-cost:   14
c ---[ 133]---> BDD-cost:   14
c ---[ 132]---> BDD-cost:   15
c ---[ 131]---> BDD-cost:   16
c ---[ 130]---> BDD-cost:   11
c ---[ 129]---> BDD-cost:   12
c ---[ 128]---> BDD-cost:   10
c ---[ 127]---> BDD-cost:   13
c ---[ 126]---> BDD-cost:   16
c ---[ 125]---> BDD-cost:   16
c ---[ 124]---> BDD-cost:   19
c ---[ 123]---> BDD-cost:   11
c ---[ 122]---> BDD-cost:   12
c ---[ 121]---> BDD-cost:   16
c ---[ 120]---> BDD-cost:   10
c ---[ 119]---> BDD-cost:   12
c ---[ 118]---> BDD-cost:   12
c ---[ 117]---> BDD-cost:   16
c ---[ 116]---> BDD-cost:   15
c ---[ 115]---> BDD-cost:   12
c ---[ 114]---> BDD-cost:   13
c ---[ 113]---> BDD-cost:   11
c ---[ 112]---> BDD-cost:   16
c ---[ 111]---> BDD-cost:   11
c ---[ 110]---> BDD-cost:   12
c ---[ 109]---> BDD-cost:   11
c ---[ 108]---> BDD-cost:   17
c ---[ 107]---> BDD-cost:   12
c ---[ 106]---> BDD-cost:   14
c ---[ 105]---> BDD-cost:   14
c ---[ 104]---> BDD-cost:   15
c ---[ 103]---> BDD-cost:   17
c ---[ 102]---> BDD-cost:   12
c ---[ 101]---> BDD-cost:   11
c ---[ 100]---> BDD-cost:   12
c ---[  99]---> BDD-cost:   10
c ---[  98]---> BDD-cost:   13
c ---[  97]---> BDD-cost:   17
c ---[  96]---> BDD-cost:   16
c ---[  95]---> BDD-cost:   11
c ---[  94]---> BDD-cost:   12
c ---[  93]---> BDD-cost:   17
c ---[  92]---> BDD-cost:   10
c ---[  91]---> BDD-cost:   11
c ---[  90]---> BDD-cost:   12
c ---[  89]---> BDD-cost:   12
c ---[  88]---> BDD-cost:   16
c ---[  87]---> BDD-cost:   15
c ---[  86]---> BDD-cost:   12
c ---[  85]---> BDD-cost:   13
c ---[  84]---> BDD-cost:   19
c ---[  83]---> BDD-cost:   11
c ---[  82]---> BDD-cost:   12
c ---[  81]---> BDD-cost:   11
c ---[  80]---> BDD-cost:   17
c ---[  79]---> BDD-cost:   12
c ---[  78]---> BDD-cost:   14
c ---[  77]---> BDD-cost:   14
c ---[  76]---> BDD-cost:   14
c ---[  75]---> BDD-cost:   15
c ---[  74]---> BDD-cost:   17
c ---[  73]---> BDD-cost:   11
c ---[  72]---> BDD-cost:   12
c ---[  71]---> BDD-cost:   10
c ---[  70]---> BDD-cost:   13
c ---[  69]---> BDD-cost:   17
c ---[  68]---> BDD-cost:   17
c ---[  67]---> BDD-cost:   11
c ---[  66]---> BDD-cost:   12
c ---[  65]---> BDD-cost:   15
c ---[  64]---> BDD-cost:   17
c ---[  63]---> BDD-cost:   10
c ---[  62]---> BDD-cost:   12
c ---[  61]---> BDD-cost:   12
c ---[  60]---> BDD-cost:   16
c ---[  59]---> BDD-cost:   15
c ---[  58]---> BDD-cost:   12
c ---[  57]---> BDD-cost:   13
c ---[  56]---> BDD-cost:   17
c ---[  55]---> BDD-cost:   11
c ---[  54]---> BDD-cost:   17
c ---[  53]---> BDD-cost:   12
c ---[  52]---> BDD-cost:   11
c ---[  51]---> BDD-cost:   17
c ---[  50]---> BDD-cost:   12
c ---[  49]---> BDD-cost:   14
c ---[  48]---> BDD-cost:   14
c ---[  47]---> BDD-cost:   15
c ---[  46]---> BDD-cost:   17
c ---[  45]---> BDD-cost:   11
c ---[  44]---> BDD-cost:   12
c ---[  43]---> BDD-cost:   11
c ---[  42]---> BDD-cost:   10
c ---[  41]---> BDD-cost:   13
c ---[  40]---> BDD-cost:   17
c ---[  39]---> BDD-cost:   17
c ---[  38]---> BDD-cost:   11
c ---[  37]---> BDD-cost:   12
c ---[  36]---> BDD-cost:   17
c ---[  35]---> BDD-cost:   10
c ---[  34]---> BDD-cost:   12
c ---[  33]---> BDD-cost:   12
c ---[  32]---> BDD-cost:   12
c ---[  31]---> BDD-cost:   17
c ---[  30]---> BDD-cost:   15
c ---[  29]---> BDD-cost:   12
c ---[  28]---> BDD-cost:   13
c ---[  27]---> BDD-cost:   17
c ---[  26]---> BDD-cost:   11
c ---[  25]---> BDD-cost:   12
c ---[  24]---> BDD-cost:   11
c ---[  23]---> BDD-cost:   17
c ---[  22]---> BDD-cost:   12
c ---[  21]---> BDD-cost:   10
c ---[  20]---> BDD-cost:   14
c ---[  19]---> BDD-cost:   14
c ---[  18]---> BDD-cost:   15
c ---[  17]---> BDD-cost:   17
c ---[  16]---> BDD-cost:   11
c ---[  15]---> BDD-cost:   12
c ---[  14]---> BDD-cost:   10
c ---[  13]---> BDD-cost:   13
c ---[  12]---> BDD-cost:   17
c ---[  11]---> BDD-cost:   17
c ---[  10]---> BDD-cost:   13
c ---[   9]---> BDD-cost:   11
c ---[   8]---> BDD-cost:   12
c ---[   7]---> BDD-cost:   17
c ---[   6]---> BDD-cost:   10
c ---[   5]---> BDD-cost:   12
c ---[   4]---> BDD-cost:   12
c ---[   3]---> BDD-cost:   17
c ---[   2]---> BDD-cost:   15
c ---[   1]---> BDD-cost:   12
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  152043   412495 |   50681       0        0     nan |  0.000 % |
c |       100 |  151985   412363 |   55749      99      454     4.6 |  8.552 % |
c |       251 |  151452   411147 |   61324     242     1146     4.7 |  8.901 % |
c |       479 |  151326   410848 |   67456     467     2138     4.6 |  8.989 % |
c |       816 |  151047   410204 |   74202     779     3799     4.9 |  9.151 % |
c |      1322 |  150952   409981 |   81622    1281     6190     4.8 |  9.205 % |
c |      2081 |  150778   409563 |   89784    2029     9214     4.5 |  9.299 % |
c |      3220 |  150395   408694 |   98762    3135    14781     4.7 |  9.530 % |
c |      4928 |  149090   405623 |  108639    4807    22862     4.8 | 10.342 % |
c |      7490 |  147018   400642 |  119503    7225    33875     4.7 | 11.630 % |
c |     11334 |  145422   396878 |  131453   10947    51864     4.7 | 12.636 % |
c |     17100 |  144100   393799 |  144598   16612    80564     4.8 | 13.493 % |
c |     25749 |  140718   385761 |  159058   24983   124968     5.0 | 15.648 % |
c |     38723 |  138552   380590 |  174964   37683   226936     6.0 | 17.057 % |
c |     58184 |  136987   376730 |  192461   56922   493490     8.7 | 18.029 % |
c |     87376 |  135882   373976 |  211707   85967  1410936    16.4 | 18.721 % |
c ==============================================================================
c [1mFound solution: 5653457[0m
c ---[   0]---> Adder-cost: 11067   maxlim: 3057885   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     94780 |  212824   649306 |   70941   93288  1574902    16.9 | 18.721 % |
c |     94881 |  212824   649306 |   78035   29638   680215    23.0 | 15.463 % |
c |     95031 |  212824   649306 |   85838   29788   681034    22.9 | 15.463 % |
c |     95256 |  212817   649283 |   94422   30012   682109    22.7 | 15.464 % |
c |     95593 |  212672   648938 |  103864   30338   683616    22.5 | 15.540 % |
c |     96099 |  212514   648573 |  114251   30835   686134    22.3 | 15.616 % |
c |     96859 |  212370   648234 |  125676   31587   690293    21.9 | 15.701 % |
c |     97998 |  212370   648234 |  138243   32726   696215    21.3 | 15.701 % |
c |     99706 |  212123   647661 |  152068   34419   705749    20.5 | 15.831 % |
c |    102269 |  212025   647430 |  167275   36955   725239    19.6 | 15.879 % |
c |    106113 |  211608   646463 |  184002   40763   759331    18.6 | 16.107 % |
c |    111879 |  211233   645560 |  202402   46489   807359    17.4 | 16.298 % |
c |    120529 |  211016   645037 |  222643   55113   900773    16.3 | 16.423 % |
c |    133503 |  210494   643639 |  244907   67999  1091968    16.1 | 16.669 % |
c |    152964 |  210274   643078 |  269398   87434  1591805    18.2 | 16.774 % |
c ==============================================================================
c [1mFound solution: 5592336[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3119006   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    175173 |  210207   643068 |   70069  109627  2296626    20.9 | 16.774 % |
c |    175273 |  210106   642822 |   77075   27433   543505    19.8 | 16.882 % |
c |    175423 |  210106   642822 |   84783   27583   544219    19.7 | 16.882 % |
c |    175650 |  210090   642784 |   93261   27809   546369    19.6 | 16.894 % |
c |    175988 |  210090   642784 |  102588   28147   547920    19.5 | 16.894 % |
c |    176494 |  210075   642750 |  112846   28649   550356    19.2 | 16.901 % |
c |    177253 |  210075   642750 |  124131   29408   554169    18.8 | 16.901 % |
c |    178392 |  209993   642560 |  136544   30531   559925    18.3 | 16.943 % |
c |    180100 |  209924   642399 |  150199   32231   572132    17.8 | 16.984 % |
c |    182662 |  209912   642371 |  165219   34788   593461    17.1 | 16.991 % |
c |    186506 |  209894   642313 |  181740   38629   616481    16.0 | 16.997 % |
c |    192272 |  209732   641929 |  199915   44373   659292    14.9 | 17.078 % |
c |    200922 |  209643   641720 |  219906   53007   733523    13.8 | 17.131 % |
c ==============================================================================
c [1mFound solution: 5361922[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3349420   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    211689 |  209590   641708 |   69863   63762   865469    13.6 | 17.131 % |
c |    211790 |  209590   641708 |   76849   63863   866224    13.6 | 17.181 % |
c |    211944 |  209590   641708 |   84534   64017   867881    13.6 | 17.181 % |
c |    212174 |  209590   641708 |   92987   64247   870080    13.5 | 17.181 % |
c |    212514 |  209590   641708 |  102286   64587   873231    13.5 | 17.181 % |
c |    213020 |  209590   641708 |  112515   65093   881033    13.5 | 17.181 % |
c |    213779 |  209582   641682 |  123766   65851   889569    13.5 | 17.183 % |
c |    214919 |  209573   641651 |  136143   66989   915421    13.7 | 17.184 % |
c |    216630 |  209568   641639 |  149757   68699   936775    13.6 | 17.188 % |
c |    219192 |  209544   641584 |  164733   71256   970949    13.6 | 17.203 % |
c ==============================================================================
c [1mFound solution: 5352269[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3359073   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    222456 |  209553   641686 |   69851   74520  1508712    20.2 | 17.203 % |
c |    222556 |  209456   641461 |   76836   74613  1509198    20.2 | 17.266 % |
c |    222706 |  209451   641448 |   84519   74762  1509897    20.2 | 17.269 % |
c |    222931 |  209437   641416 |   92971   74984  1511401    20.2 | 17.278 % |
c |    223268 |  209437   641416 |  102268   75321  1513793    20.1 | 17.278 % |
c |    223775 |  209427   641393 |  112495   75826  1519596    20.0 | 17.284 % |
c |    224534 |  209427   641393 |  123745   76585  1532781    20.0 | 17.284 % |
c |    225673 |  209427   641393 |  136119   77724  1548920    19.9 | 17.284 % |
c |    227381 |  209400   641329 |  149731   79431  1563564    19.7 | 17.300 % |
c |    229943 |  209360   641236 |  164705   81984  1587531    19.4 | 17.320 % |
c ==============================================================================
c [1mFound solution: 5352198[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3359144   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    230983 |  209336   641250 |   69778   83022  1739314    21.0 | 17.320 % |
c |    231083 |  209336   641250 |   76755   31281   821751    26.3 | 17.345 % |
c |    231233 |  209325   641223 |   84431   31430   822530    26.2 | 17.352 % |
c |    231459 |  209239   641025 |   92874   31652   823523    26.0 | 17.403 % |
c |    231796 |  209157   640834 |  102161   31979   825082    25.8 | 17.453 % |
c |    232302 |  209157   640834 |  112378   32485   827965    25.5 | 17.453 % |
c |    233061 |  209088   640671 |  123615   33238   832485    25.0 | 17.492 % |
c |    234200 |  209056   640597 |  135977   34374   840538    24.5 | 17.511 % |
c |    235910 |  209015   640502 |  149575   36079   855970    23.7 | 17.533 % |
c |    238472 |  208912   640260 |  164532   38637   872065    22.6 | 17.595 % |
c |    242316 |  208834   640077 |  180986   42471   985740    23.2 | 17.641 % |
c |    248082 |  208796   639988 |  199084   48229  1081108    22.4 | 17.661 % |
c |    256731 |  208668   639684 |  218993   56850  1184921    20.8 | 17.729 % |
c |    269705 |  208649   639638 |  240892   69821  1875371    26.9 | 17.741 % |
c |    289166 |  208649   639638 |  264981   89282  6005413    67.3 | 17.741 % |
c ==============================================================================
c [1mFound solution: 5262230[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3449112   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    294909 |  208628   639652 |   69542   95018  6186805    65.1 | 17.741 % |
c |    295009 |  208628   639652 |   76496   30405  1874569    61.7 | 17.761 % |
c |    295159 |  208628   639652 |   84145   30555  1875209    61.4 | 17.761 % |
c |    295384 |  208617   639626 |   92560   30777  1876293    61.0 | 17.767 % |
c |    295721 |  208538   639444 |  101816   31100  1877767    60.4 | 17.805 % |
c |    296227 |  208538   639444 |  111998   31606  1880189    59.5 | 17.805 % |
c |    296986 |  208538   639444 |  123197   32365  1884173    58.2 | 17.805 % |
c |    298125 |  208538   639444 |  135517   33504  1889916    56.4 | 17.805 % |
c |    299834 |  208491   639332 |  149069   35209  1898539    53.9 | 17.832 % |
c |    302396 |  208461   639262 |  163976   37767  1912493    50.6 | 17.852 % |
c |    306240 |  208372   639054 |  180374   41603  1957200    47.0 | 17.908 % |
c |    312006 |  208250   638768 |  198411   47355  2015110    42.6 | 17.979 % |
c |    320655 |  208134   638489 |  218252   55987  2109817    37.7 | 18.043 % |
c |    333630 |  208130   638480 |  240077   68961  2385841    34.6 | 18.045 % |
c ==============================================================================
c [1mFound solution: 4826936[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3884406   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    344542 |  208127   638630 |   69375   79871  2622019    32.8 | 18.045 % |
c |    344642 |  208102   638573 |   76312   79968  2622437    32.8 | 18.088 % |
c |    344792 |  208102   638573 |   83943   80118  2623133    32.7 | 18.088 % |
c |    345017 |  208088   638540 |   92338   80341  2624263    32.7 | 18.099 % |
c |    345354 |  208076   638512 |  101571   80677  2626176    32.6 | 18.107 % |
c |    345860 |  208076   638512 |  111729   81183  2629802    32.4 | 18.107 % |
c |    346619 |  208076   638512 |  122902   81942  2635563    32.2 | 18.107 % |
c |    347758 |  208076   638512 |  135192   83081  2695345    32.4 | 18.107 % |
c |    349466 |  208072   638503 |  148711   84787  2718759    32.1 | 18.109 % |
c |    352028 |  208072   638503 |  163582   87349  2808827    32.2 | 18.109 % |
c |    355872 |  208072   638503 |  179940   91193  2889849    31.7 | 18.109 % |
c |    361638 |  208072   638503 |  197934   96959  3048539    31.4 | 18.109 % |
c |    370291 |  208072   638503 |  217728  105612  3506725    33.2 | 18.109 % |
c ==============================================================================
c [1mFound solution: 4601641[0m
c ---[   0]---> Adder-cost: 0   maxlim: 4109701   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    382820 |  208075   638620 |   69358  118140  3860139    32.7 | 18.109 % |
c |    382920 |  208075   638620 |   76293   32441   408341    12.6 | 18.129 % |
c |    383070 |  208075   638620 |   83923   32591   409079    12.6 | 18.129 % |
c |    383295 |  208075   638620 |   92315   32816   410272    12.5 | 18.129 % |
c |    383632 |  208061   638586 |  101547   33151   412162    12.4 | 18.136 % |
c |    384138 |  208051   638564 |  111701   33655   415107    12.3 | 18.141 % |
c |    384897 |  208051   638564 |  122871   34414   419159    12.2 | 18.141 % |
c |    386036 |  208051   638564 |  135159   35553   429448    12.1 | 18.141 % |
c |    387744 |  208034   638524 |  148675   37258   439665    11.8 | 18.149 % |
c |    390306 |  208029   638512 |  163542   39819   456942    11.5 | 18.152 % |
c |    394151 |  208029   638512 |  179896   43664   500534    11.5 | 18.152 % |
c |    399917 |  207963   638361 |  197886   49415   545991    11.0 | 18.188 % |
c |    408566 |  207935   638297 |  217675   58060   737670    12.7 | 18.203 % |
c |    421541 |  207919   638259 |  239442   71033  1630592    23.0 | 18.213 % |
c |    441002 |  207857   638114 |  263386   90486  2990115    33.0 | 18.249 % |
c |    470194 |  207857   638114 |  289725  119678  3981704    33.3 | 18.249 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 21580 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.93 0.98 0.94 2/54 21576
Raw data (stat): 21576 (runsolver) R 21575 5562 5561 0 -1 64 1 0 0 0 0 0 0 0 19 0 1 0 842904396 1052672 97 4294967295 134512640 135381576 3221224480 3221219852 135024794 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 97 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.94 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.0013 s]
Raw data (loadavg): 0.95 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0014 s]
Raw data (loadavg): 0.95 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.0016 s]
Raw data (loadavg): 0.96 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.0022 s]
Raw data (loadavg): 0.97 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.0033 s]
Raw data (loadavg): 0.97 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.0036 s]
Raw data (loadavg): 0.97 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.0042 s]
Raw data (loadavg): 0.98 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.0054 s]
Raw data (loadavg): 0.98 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.006 s]
Raw data (loadavg): 0.98 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.006 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.006 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.006 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.006 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.01 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.011 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.012 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.011 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.012 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.013 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.013 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.017 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.018 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.017 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.031 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.031 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.032 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.031 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.032 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.034 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.034 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.034 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.034 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.034 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.034 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.034 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.034 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.034 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.034 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.034 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.035 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.035 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.034 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.035 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.035 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.035 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.036 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.036 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.035 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.039 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.045 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.045 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.045 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.046 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.045 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.046 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.047 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.047 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.047 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.047 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.047 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.047 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.047 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.047 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.047 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.048 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.048 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.048 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 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.049 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.74 s]
Raw data (loadavg): 0.99 0.98 0.94 1/53 21580
Raw data (stat): 21576 (minisat+_script) S 21575 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842904396 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

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