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-ran12x21.opb
MD5SUM	0d744fe957d41a18692933adc6be4af7
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1493203
Optimality of the best value was proved	NO
Number of terms in the objective function	5292
Biggest coefficient in the objective function	5242880
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	1511880035
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	1511880035
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	5292
Total number of constraints	285
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	285
Minimum length of a constraint	21
Maximum length of a constraint	420
Trace number 31268

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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:        828696 kB
Buffers:         31488 kB
Cached:         154468 kB
SwapCached:        500 kB
Active:          37388 kB
Inactive:       150960 kB
HighTotal:      131008 kB
HighFree:         1736 kB
LowTotal:       903652 kB
LowFree:        826960 kB
SwapTotal:     2097136 kB
SwapFree:      2096004 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5788 kB
Slab:            12200 kB
Committed_AS:    71796 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 23:59:51 (client local time) WITH STATUS 152 IN 1229.88 SECONDS
stats: 22667 7 1229.88 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 318 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 316]---> Adder-cost: 428   maxlim: 44523   bits: 16/16
c ---[ 314]---> Adder-cost: 428   maxlim: 45163   bits: 16/16
c ---[ 312]---> Adder-cost: 434   maxlim: 55787   bits: 16/16
c ---[ 310]---> Adder-cost: 428   maxlim: 44395   bits: 16/16
c ---[ 308]---> Adder-cost: 428   maxlim: 43627   bits: 16/16
c ---[ 306]---> Adder-cost: 428   maxlim: 43755   bits: 16/16
c ---[ 304]---> Adder-cost: 428   maxlim: 44267   bits: 16/16
c ---[ 302]---> Adder-cost: 412   maxlim: 29419   bits: 15/15
c ---[ 300]---> Adder-cost: 428   maxlim: 44651   bits: 16/16
c ---[ 298]---> Adder-cost: 428   maxlim: 45035   bits: 16/16
c ---[ 296]---> Adder-cost: 434   maxlim: 51819   bits: 16/16
c ---[ 294]---> Adder-cost: 412   maxlim: 29547   bits: 15/15
c ---[ 292]---> Adder-cost: 198   maxlim: 5876   bits: 13/13
c ---[ 290]---> Adder-cost: 242   maxlim: 23540   bits: 15/15
c ---[ 288]---> Adder-cost: 198   maxlim: 5748   bits: 13/13
c ---[ 286]---> Adder-cost: 262   maxlim: 42356   bits: 16/16
c ---[ 284]---> Adder-cost: 198   maxlim: 5876   bits: 13/13
c ---[ 282]---> Adder-cost: 262   maxlim: 41332   bits: 16/16
c ---[ 280]---> Adder-cost: 220   maxlim: 11636   bits: 14/14
c ---[ 278]---> Adder-cost: 266   maxlim: 46836   bits: 16/16
c ---[ 276]---> Adder-cost: 242   maxlim: 23412   bits: 15/15
c ---[ 274]---> Adder-cost: 220   maxlim: 11380   bits: 14/14
c ---[ 272]---> Adder-cost: 262   maxlim: 41588   bits: 16/16
c ---[ 270]---> Adder-cost: 220   maxlim: 11380   bits: 14/14
c ---[ 268]---> Adder-cost: 198   maxlim: 5876   bits: 13/13
c ---[ 266]---> Adder-cost: 262   maxlim: 41588   bits: 16/16
c ---[ 264]---> Adder-cost: 198   maxlim: 5748   bits: 13/13
c ---[ 262]---> Adder-cost: 262   maxlim: 42612   bits: 16/16
c ---[ 260]---> Adder-cost: 220   maxlim: 11636   bits: 14/14
c ---[ 258]---> Adder-cost: 242   maxlim: 22644   bits: 15/15
c ---[ 256]---> Adder-cost: 266   maxlim: 48372   bits: 16/16
c ---[ 254]---> Adder-cost: 266   maxlim: 49140   bits: 16/16
c ---[ 252]---> Adder-cost: 242   maxlim: 23412   bits: 15/15
c ---[ 251]---> BDD-cost:   10
c ---[ 250]---> BDD-cost:   12
c ---[ 249]---> BDD-cost:   11
c ---[ 248]---> BDD-cost:   15
c ---[ 247]---> BDD-cost:   13
c ---[ 246]---> BDD-cost:   16
c ---[ 245]---> BDD-cost:   13
c ---[ 244]---> BDD-cost:   16
c ---[ 243]---> BDD-cost:   10
c ---[ 242]---> BDD-cost:   12
c ---[ 241]---> BDD-cost:   10
c ---[ 240]---> BDD-cost:   11
c ---[ 239]---> BDD-cost:   14
c ---[ 238]---> BDD-cost:   17
c ---[ 237]---> BDD-cost:   13
c ---[ 236]---> BDD-cost:   14
c ---[ 235]---> BDD-cost:   14
c ---[ 234]---> BDD-cost:   14
c ---[ 233]---> BDD-cost:   15
c ---[ 232]---> BDD-cost:   11
c ---[ 231]---> BDD-cost:   14
c ---[ 230]---> BDD-cost:   10
c ---[ 229]---> BDD-cost:   14
c ---[ 228]---> BDD-cost:   13
c ---[ 227]---> BDD-cost:   10
c ---[ 226]---> BDD-cost:   14
c ---[ 225]---> BDD-cost:   15
c ---[ 224]---> BDD-cost:   13
c ---[ 223]---> BDD-cost:   14
c ---[ 222]---> BDD-cost:   13
c ---[ 221]---> BDD-cost:   14
c ---[ 220]---> BDD-cost:   10
c ---[ 219]---> BDD-cost:   12
c ---[ 218]---> BDD-cost:   10
c ---[ 217]---> BDD-cost:   11
c ---[ 216]---> BDD-cost:   14
c ---[ 215]---> BDD-cost:   17
c ---[ 214]---> BDD-cost:   13
c ---[ 213]---> BDD-cost:   15
c ---[ 212]---> BDD-cost:   17
c ---[ 211]---> BDD-cost:   17
c ---[ 210]---> BDD-cost:   15
c ---[ 209]---> BDD-cost:   11
c ---[ 208]---> BDD-cost:   17
c ---[ 207]---> BDD-cost:   10
c ---[ 206]---> BDD-cost:   17
c ---[ 205]---> BDD-cost:   13
c ---[ 204]---> BDD-cost:   13
c ---[ 203]---> BDD-cost:   17
c ---[ 202]---> BDD-cost:   15
c ---[ 201]---> BDD-cost:   13
c ---[ 200]---> BDD-cost:   17
c ---[ 199]---> BDD-cost:   13
c ---[ 198]---> BDD-cost:   17
c ---[ 197]---> BDD-cost:   10
c ---[ 196]---> BDD-cost:   12
c ---[ 195]---> BDD-cost:   10
c ---[ 194]---> BDD-cost:   14
c ---[ 193]---> BDD-cost:   11
c ---[ 192]---> BDD-cost:   17
c ---[ 191]---> BDD-cost:   13
c ---[ 190]---> BDD-cost:   15
c ---[ 189]---> BDD-cost:   15
c ---[ 188]---> BDD-cost:   15
c ---[ 187]---> BDD-cost:   15
c ---[ 186]---> BDD-cost:   11
c ---[ 185]---> BDD-cost:   15
c ---[ 184]---> BDD-cost:   10
c ---[ 183]---> BDD-cost:   15
c ---[ 182]---> BDD-cost:   15
c ---[ 181]---> BDD-cost:   13
c ---[ 180]---> BDD-cost:   15
c ---[ 179]---> BDD-cost:   15
c ---[ 178]---> BDD-cost:   13
c ---[ 177]---> BDD-cost:   15
c ---[ 176]---> BDD-cost:   13
c ---[ 175]---> BDD-cost:   15
c ---[ 174]---> BDD-cost:   10
c ---[ 173]---> BDD-cost:   12
c ---[ 172]---> BDD-cost:   13
c ---[ 171]---> BDD-cost:   10
c ---[ 170]---> BDD-cost:   11
c ---[ 169]---> BDD-cost:   17
c ---[ 168]---> BDD-cost:   13
c ---[ 167]---> BDD-cost:   15
c ---[ 166]---> BDD-cost:   18
c ---[ 165]---> BDD-cost:   14
c ---[ 164]---> BDD-cost:   15
c ---[ 163]---> BDD-cost:   11
c ---[ 162]---> BDD-cost:   17
c ---[ 161]---> BDD-cost:   14
c ---[ 160]---> BDD-cost:   10
c ---[ 159]---> BDD-cost:   17
c ---[ 158]---> BDD-cost:   13
c ---[ 157]---> BDD-cost:   18
c ---[ 156]---> BDD-cost:   15
c ---[ 155]---> BDD-cost:   13
c ---[ 154]---> BDD-cost:   17
c ---[ 153]---> BDD-cost:   13
c ---[ 152]---> BDD-cost:   17
c ---[ 151]---> BDD-cost:   10
c ---[ 150]---> BDD-cost:   13
c ---[ 149]---> BDD-cost:   12
c ---[ 148]---> BDD-cost:   10
c ---[ 147]---> BDD-cost:   11
c ---[ 146]---> BDD-cost:   15
c ---[ 145]---> BDD-cost:   13
c ---[ 144]---> BDD-cost:   15
c ---[ 143]---> BDD-cost:   15
c ---[ 142]---> BDD-cost:   15
c ---[ 141]---> BDD-cost:   15
c ---[ 140]---> BDD-cost:   11
c ---[ 139]---> BDD-cost:   10
c ---[ 138]---> BDD-cost:   14
c ---[ 137]---> BDD-cost:   15
c ---[ 136]---> BDD-cost:   10
c ---[ 135]---> BDD-cost:   15
c ---[ 134]---> BDD-cost:   13
c ---[ 133]---> BDD-cost:   15
c ---[ 132]---> BDD-cost:   15
c ---[ 131]---> BDD-cost:   13
c ---[ 130]---> BDD-cost:   15
c ---[ 129]---> BDD-cost:   13
c ---[ 128]---> BDD-cost:   15
c ---[ 127]---> BDD-cost:   10
c ---[ 126]---> BDD-cost:   10
c ---[ 125]---> BDD-cost:   12
c ---[ 124]---> BDD-cost:   10
c ---[ 123]---> BDD-cost:   11
c ---[ 122]---> BDD-cost:   17
c ---[ 121]---> BDD-cost:   13
c ---[ 120]---> BDD-cost:   15
c ---[ 119]---> BDD-cost:   14
c ---[ 118]---> BDD-cost:   14
c ---[ 117]---> BDD-cost:   15
c ---[ 116]---> BDD-cost:   12
c ---[ 115]---> BDD-cost:   11
c ---[ 114]---> BDD-cost:   17
c ---[ 113]---> BDD-cost:   10
c ---[ 112]---> BDD-cost:   17
c ---[ 111]---> BDD-cost:   13
c ---[ 110]---> BDD-cost:   14
c ---[ 109]---> BDD-cost:   15
c ---[ 108]---> BDD-cost:   13
c ---[ 107]---> BDD-cost:   17
c ---[ 106]---> BDD-cost:   13
c ---[ 105]---> BDD-cost:   10
c ---[ 104]---> BDD-cost:   17
c ---[ 103]---> BDD-cost:   10
c ---[ 102]---> BDD-cost:   12
c ---[ 101]---> BDD-cost:   10
c ---[ 100]---> BDD-cost:   11
c ---[  99]---> BDD-cost:   17
c ---[  98]---> BDD-cost:   13
c ---[  97]---> BDD-cost:   15
c ---[  96]---> BDD-cost:   17
c ---[  95]---> BDD-cost:   17
c ---[  94]---> BDD-cost:   11
c ---[  93]---> BDD-cost:   15
c ---[  92]---> BDD-cost:   11
c ---[  91]---> BDD-cost:   17
c ---[  90]---> BDD-cost:   10
c ---[  89]---> BDD-cost:   17
c ---[  88]---> BDD-cost:   13
c ---[  87]---> BDD-cost:   17
c ---[  86]---> BDD-cost:   15
c ---[  85]---> BDD-cost:   13
c ---[  84]---> BDD-cost:   17
c ---[  83]---> BDD-cost:   17
c ---[  82]---> BDD-cost:   13
c ---[  81]---> BDD-cost:   17
c ---[  80]---> BDD-cost:   13
c ---[  79]---> BDD-cost:   15
c ---[  78]---> BDD-cost:   17
c ---[  77]---> BDD-cost:   17
c ---[  76]---> BDD-cost:   11
c ---[  75]---> BDD-cost:   15
c ---[  74]---> BDD-cost:   11
c ---[  73]---> BDD-cost:   17
c ---[  72]---> BDD-cost:   10
c ---[  71]---> BDD-cost:   17
c ---[  70]---> BDD-cost:   13
c ---[  69]---> BDD-cost:   17
c ---[  68]---> BDD-cost:   15
c ---[  67]---> BDD-cost:   13
c ---[  66]---> BDD-cost:   17
c ---[  65]---> BDD-cost:   17
c ---[  64]---> BDD-cost:   13
c ---[  63]---> BDD-cost:   17
c ---[  62]---> BDD-cost:   10
c ---[  61]---> BDD-cost:   12
c ---[  60]---> BDD-cost:   10
c ---[  59]---> BDD-cost:   11
c ---[  58]---> BDD-cost:   17
c ---[  57]---> BDD-cost:   13
c ---[  56]---> BDD-cost:   15
c ---[  55]---> BDD-cost:   17
c ---[  54]---> BDD-cost:   13
c ---[  53]---> BDD-cost:   17
c ---[  52]---> BDD-cost:   15
c ---[  51]---> BDD-cost:   11
c ---[  50]---> BDD-cost:   17
c ---[  49]---> BDD-cost:   10
c ---[  48]---> BDD-cost:   17
c ---[  47]---> BDD-cost:   13
c ---[  46]---> BDD-cost:   17
c ---[  45]---> BDD-cost:   15
c ---[  44]---> BDD-cost:   13
c ---[  43]---> BDD-cost:   15
c ---[  42]---> BDD-cost:   17
c ---[  41]---> BDD-cost:   13
c ---[  40]---> BDD-cost:   17
c ---[  39]---> BDD-cost:   10
c ---[  38]---> BDD-cost:   12
c ---[  37]---> BDD-cost:   10
c ---[  36]---> BDD-cost:   11
c ---[  35]---> BDD-cost:   17
c ---[  34]---> BDD-cost:   13
c ---[  33]---> BDD-cost:   15
c ---[  32]---> BDD-cost:   14
c ---[  31]---> BDD-cost:   16
c ---[  30]---> BDD-cost:   16
c ---[  29]---> BDD-cost:   15
c ---[  28]---> BDD-cost:   11
c ---[  27]---> BDD-cost:   17
c ---[  26]---> BDD-cost:   10
c ---[  25]---> BDD-cost:   17
c ---[  24]---> BDD-cost:   13
c ---[  23]---> BDD-cost:   16
c ---[  22]---> BDD-cost:   15
c ---[  21]---> BDD-cost:   14
c ---[  20]---> BDD-cost:   13
c ---[  19]---> BDD-cost:   17
c ---[  18]---> BDD-cost:   13
c ---[  17]---> BDD-cost:   17
c ---[  16]---> BDD-cost:   10
c ---[  15]---> BDD-cost:   12
c ---[  14]---> BDD-cost:   10
c ---[  13]---> BDD-cost:   11
c ---[  12]---> BDD-cost:   17
c ---[  11]---> BDD-cost:   13
c ---[  10]---> BDD-cost:   15
c ---[   9]---> BDD-cost:   15
c ---[   8]---> BDD-cost:   16
c ---[   7]---> BDD-cost:   16
c ---[   6]---> BDD-cost:   15
c ---[   5]---> BDD-cost:   11
c ---[   4]---> BDD-cost:   17
c ---[   3]---> BDD-cost:   10
c ---[   2]---> BDD-cost:   16
c ---[   1]---> BDD-cost:   13
c ---[   0]---> BDD-cost:   16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   71899   250207 |   23966       0        0     nan |  0.000 % |
c |       100 |   71775   249789 |   26362      90      285     3.2 | 21.316 % |
c |       250 |   71661   249395 |   28998     222      730     3.3 | 21.427 % |
c |       475 |   71389   248441 |   31898     415     1374     3.3 | 21.702 % |
c |       812 |   71264   248026 |   35088     735     2410     3.3 | 21.825 % |
c |      1318 |   71004   247136 |   38597    1202     3888     3.2 | 22.088 % |
c |      2077 |   70497   245373 |   42457    1895     6183     3.3 | 22.586 % |
c |      3216 |   70137   244145 |   46702    2980    10121     3.4 | 22.949 % |
c |      4925 |   69876   243270 |   51373    4655    17540     3.8 | 23.212 % |
c |      7487 |   69792   242992 |   56510    7205    34484     4.8 | 23.300 % |
c |     11331 |   69708   242704 |   62161   11037    63037     5.7 | 23.388 % |
c |     17098 |   69601   242349 |   68377   16789   106394     6.3 | 23.505 % |
c |     25748 |   69551   242177 |   75215   25433   223628     8.8 | 23.551 % |
c |     38722 |   69475   241927 |   82737   38397   380709     9.9 | 23.633 % |
c |     58183 |   69343   241469 |   91010   57843  1285226    22.2 | 23.774 % |
c |     87375 |   69164   240876 |  100111   87009  2085575    24.0 | 23.967 % |
c |    131164 |   69034   240442 |  110123   45548  1563875    34.3 | 24.113 % |
c |    196848 |   68908   240028 |  121135  111213  5777081    51.9 | 24.254 % |
c |    295374 |   68811   239711 |  133248  107600 10096080    93.8 | 24.359 % |
c ==============================================================================
c [1mFound solution: 5164114[0m
c ---[   0]---> Adder-cost: 10758   maxlim: 3198225   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    427438 |  143942   508081 |   47980  119798  4552772    38.0 | 24.359 % |
c |    427538 |  143942   508081 |   52778   24290   324994    13.4 | 15.026 % |
c |    427688 |  143942   508081 |   58055   24440   325740    13.3 | 15.026 % |
c |    427913 |  143942   508081 |   63861   24665   326932    13.3 | 15.026 % |
c |    428250 |  143942   508081 |   70247   25002   328801    13.2 | 15.026 % |
c |    428756 |  143942   508081 |   77272   25508   331681    13.0 | 15.026 % |
c |    429516 |  143942   508081 |   84999   26268   336986    12.8 | 15.026 % |
c |    430655 |  143942   508081 |   93499   27407   347060    12.7 | 15.026 % |
c |    432363 |  143942   508081 |  102849   29115   361638    12.4 | 15.026 % |
c |    434925 |  143942   508081 |  113134   31677   383141    12.1 | 15.026 % |
c |    438769 |  143942   508081 |  124447   35521   424339    11.9 | 15.026 % |
c |    444535 |  143942   508081 |  136892   41287   504502    12.2 | 15.026 % |
c |    453184 |  143942   508081 |  150581   49936   608101    12.2 | 15.026 % |
c |    466158 |  143933   508052 |  165639   62909   799784    12.7 | 15.033 % |
c ==============================================================================
c [1mFound solution: 4993470[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3368869   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    476252 |  143940   508206 |   47980   72998   976904    13.4 | 15.033 % |
c |    476352 |  143940   508206 |   52778   24029   244358    10.2 | 15.081 % |
c |    476502 |  143940   508206 |   58055   24179   245061    10.1 | 15.081 % |
c |    476727 |  143924   508154 |   63861   24402   246268    10.1 | 15.092 % |
c |    477064 |  143924   508154 |   70247   24739   248093    10.0 | 15.092 % |
c |    477570 |  143924   508154 |   77272   25245   251148     9.9 | 15.092 % |
c |    478329 |  143924   508154 |   84999   26004   255844     9.8 | 15.092 % |
c |    479468 |  143924   508154 |   93499   27143   263557     9.7 | 15.092 % |
c |    481176 |  143924   508154 |  102849   28851   277168     9.6 | 15.092 % |
c |    483738 |  143924   508154 |  113134   31413   298331     9.5 | 15.092 % |
c |    487582 |  143924   508154 |  124447   35257   338015     9.6 | 15.092 % |
c |    493348 |  143924   508154 |  136892   41023   411370    10.0 | 15.092 % |
c |    501998 |  143924   508154 |  150581   49673   636684    12.8 | 15.092 % |
c |    514973 |  143924   508154 |  165639   62648  1548001    24.7 | 15.092 % |
c |    534435 |  143860   507938 |  182203   82102  2556226    31.1 | 15.135 % |
c ==============================================================================
c [1mFound solution: 4969533[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3392806   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    548957 |  143830   507947 |   47943   96618  2800047    29.0 | 15.135 % |
c |    549057 |  143830   507947 |   52737   25841   259182    10.0 | 15.189 % |
c |    549207 |  143830   507947 |   58011   25991   259927    10.0 | 15.189 % |
c |    549432 |  143821   507918 |   63812   26215   260957    10.0 | 15.196 % |
c |    549769 |  143821   507918 |   70193   26552   264038     9.9 | 15.196 % |
c |    550275 |  143821   507918 |   77212   27058   267170     9.9 | 15.196 % |
c |    551035 |  143812   507889 |   84933   27817   271481     9.8 | 15.203 % |
c |    552174 |  143812   507889 |   93427   28956   278220     9.6 | 15.203 % |
c |    553882 |  143812   507889 |  102770   30664   290985     9.5 | 15.203 % |
c |    556444 |  143812   507889 |  113047   33226   313156     9.4 | 15.203 % |
c |    560288 |  143812   507889 |  124351   37070   349921     9.4 | 15.203 % |
c |    566054 |  143806   507869 |  136786   42835   412129     9.6 | 15.207 % |
c |    574703 |  143806   507869 |  150465   51484   506204     9.8 | 15.207 % |
c |    587677 |  143806   507869 |  165512   64458   684691    10.6 | 15.207 % |
c |    607139 |  143806   507869 |  182063   83920  1024750    12.2 | 15.207 % |
c ==============================================================================
c [1mFound solution: 4948528[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3413811   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    619345 |  143802   507952 |   47934   96122  1210531    12.6 | 15.207 % |
c |    619445 |  143802   507952 |   52727   28426   249561     8.8 | 15.244 % |
c |    619596 |  143802   507952 |   58000   28577   250180     8.8 | 15.244 % |
c |    619821 |  143802   507952 |   63800   28802   251367     8.7 | 15.244 % |
c |    620158 |  143802   507952 |   70180   29139   254413     8.7 | 15.244 % |
c |    620664 |  143793   507921 |   77198   29644   257915     8.7 | 15.247 % |
c |    621423 |  143793   507921 |   84918   30403   263542     8.7 | 15.247 % |
c |    622562 |  143793   507921 |   93409   31542   270551     8.6 | 15.247 % |
c |    624270 |  143793   507921 |  102750   33250   287436     8.6 | 15.247 % |
c |    626832 |  143793   507921 |  113025   35812   307607     8.6 | 15.247 % |
c |    630676 |  143793   507921 |  124328   39656   343499     8.7 | 15.247 % |
c |    636443 |  143793   507921 |  136761   45423   403695     8.9 | 15.247 % |
c |    645093 |  143793   507921 |  150437   54073   506666     9.4 | 15.247 % |
c |    658067 |  143793   507921 |  165481   67047   772495    11.5 | 15.247 % |
c |    677528 |  143781   507881 |  182029   86504  1175225    13.6 | 15.254 % |
c |    706720 |  143781   507881 |  200232  115696  1691943    14.6 | 15.254 % |
c |    750510 |  143775   507861 |  220255  159485  2508041    15.7 | 15.258 % |
c |    816194 |  143748   507768 |  242280  225165  9373381    41.6 | 15.272 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:  6880 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 6876
Raw data (stat): 6876 (runsolver) R 6875 21152 21151 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 784676746 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.0004 s]
Raw data (loadavg): 0.94 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0007 s]
Raw data (loadavg): 0.95 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0012 s]
Raw data (loadavg): 0.95 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0018 s]
Raw data (loadavg): 0.96 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0023 s]
Raw data (loadavg): 0.97 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0025 s]
Raw data (loadavg): 0.97 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0033 s]
Raw data (loadavg): 0.97 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0039 s]
Raw data (loadavg): 0.98 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0052 s]
Raw data (loadavg): 0.98 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.007 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.007 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.007 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.01 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.01 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.011 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.01 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.011 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.012 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.013 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.017 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.018 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.019 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.019 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.019 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.021 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.021 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.022 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.022 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.022 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.022 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.022 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.024 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.024 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.024 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.024 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.025 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.025 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.026 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.026 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.027 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.028 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.028 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.028 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.029 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.031 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.031 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.031 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.037 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.037 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.038 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.038 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.039 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.042 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.042 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.042 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.043 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.043 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.044 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.044 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.043 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.044 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.044 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.045 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.045 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.045 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.77 s]
Raw data (loadavg): 0.99 0.98 0.94 1/53 6880
Raw data (stat): 6876 (minisat+_script) S 6875 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784676746 2174976 226 4294967295 134512640 135087896 3221224544 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.77
CPU time (s): 1229.88
CPU user time (s): 1229.02
CPU system time (s): 0.858869
CPU usage (%): 100.009
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####