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-ran17x17.opb
MD5SUM	4afffa77a031423497a8b9b377dd0292
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	689314
Optimality of the best value was proved	NO
Number of terms in the objective function	6069
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	1576985250
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	1576985250
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	6069
Total number of constraints	323
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	323
Minimum length of a constraint	21
Maximum length of a constraint	340
Trace number 31275

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-05-25 23:43:59 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22671 boxname=wulflinc3 idbench=1487 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  4afffa77a031423497a8b9b377dd0292  /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-ran17x17.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-ran17x17.opb
IDLAUNCH: 22671
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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.190
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:        886656 kB
Buffers:          7212 kB
Cached:         121840 kB
SwapCached:         12 kB
Active:          32568 kB
Inactive:        99136 kB
HighTotal:      131008 kB
HighFree:        10948 kB
LowTotal:       903652 kB
LowFree:        875708 kB
SwapTotal:     2097136 kB
SwapFree:      2096788 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6576 kB
Slab:            10760 kB
Committed_AS:    71796 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-26 00:04:29 (client local time) WITH STATUS 152 IN 1229.88 SECONDS
stats: 22671 7 1229.88 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 357 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 355]---> Adder-cost: 338   maxlim: 28143   bits: 15/15
c ---[ 353]---> Adder-cost: 310   maxlim: 15599   bits: 14/14
c ---[ 351]---> Adder-cost: 338   maxlim: 27887   bits: 15/15
c ---[ 349]---> Adder-cost: 338   maxlim: 28399   bits: 15/15
c ---[ 347]---> Adder-cost: 360   maxlim: 46575   bits: 16/16
c ---[ 345]---> Adder-cost: 338   maxlim: 28527   bits: 15/15
c ---[ 343]---> Adder-cost: 338   maxlim: 28655   bits: 15/15
c ---[ 341]---> Adder-cost: 360   maxlim: 46575   bits: 16/16
c ---[ 339]---> Adder-cost: 362   maxlim: 53871   bits: 16/16
c ---[ 337]---> Adder-cost: 360   maxlim: 47215   bits: 16/16
c ---[ 335]---> Adder-cost: 360   maxlim: 46959   bits: 16/16
c ---[ 333]---> Adder-cost: 338   maxlim: 27759   bits: 15/15
c ---[ 331]---> Adder-cost: 362   maxlim: 54255   bits: 16/16
c ---[ 329]---> Adder-cost: 360   maxlim: 46703   bits: 16/16
c ---[ 327]---> Adder-cost: 360   maxlim: 47727   bits: 16/16
c ---[ 325]---> Adder-cost: 310   maxlim: 15727   bits: 14/14
c ---[ 323]---> Adder-cost: 310   maxlim: 15855   bits: 14/14
c ---[ 321]---> Adder-cost: 358   maxlim: 45935   bits: 16/16
c ---[ 319]---> Adder-cost: 320   maxlim: 16623   bits: 15/15
c ---[ 317]---> Adder-cost: 342   maxlim: 30703   bits: 15/15
c ---[ 315]---> Adder-cost: 320   maxlim: 16879   bits: 15/15
c ---[ 313]---> Adder-cost: 342   maxlim: 29807   bits: 15/15
c ---[ 311]---> Adder-cost: 358   maxlim: 46063   bits: 16/16
c ---[ 309]---> Adder-cost: 342   maxlim: 30191   bits: 15/15
c ---[ 307]---> Adder-cost: 362   maxlim: 52079   bits: 16/16
c ---[ 305]---> Adder-cost: 358   maxlim: 45679   bits: 16/16
c ---[ 303]---> Adder-cost: 288   maxlim: 8303   bits: 14/14
c ---[ 301]---> Adder-cost: 358   maxlim: 45551   bits: 16/16
c ---[ 299]---> Adder-cost: 358   maxlim: 44783   bits: 16/16
c ---[ 297]---> Adder-cost: 358   maxlim: 45167   bits: 16/16
c ---[ 295]---> Adder-cost: 362   maxlim: 51695   bits: 16/16
c ---[ 293]---> Adder-cost: 358   maxlim: 44271   bits: 16/16
c ---[ 291]---> Adder-cost: 288   maxlim: 8303   bits: 14/14
c ---[ 289]---> Adder-cost: 358   maxlim: 44399   bits: 16/16
c ---[ 288]---> BDD-cost:   13
c ---[ 287]---> BDD-cost:   12
c ---[ 286]---> BDD-cost:   12
c ---[ 285]---> BDD-cost:   14
c ---[ 284]---> BDD-cost:   17
c ---[ 283]---> BDD-cost:   17
c ---[ 282]---> BDD-cost:   12
c ---[ 281]---> BDD-cost:   11
c ---[ 280]---> BDD-cost:   15
c ---[ 279]---> BDD-cost:   16
c ---[ 278]---> BDD-cost:   17
c ---[ 277]---> BDD-cost:   17
c ---[ 276]---> BDD-cost:   17
c ---[ 275]---> BDD-cost:   11
c ---[ 274]---> BDD-cost:   11
c ---[ 273]---> BDD-cost:   17
c ---[ 272]---> BDD-cost:   12
c ---[ 271]---> BDD-cost:   11
c ---[ 270]---> BDD-cost:   15
c ---[ 269]---> BDD-cost:   13
c ---[ 268]---> BDD-cost:   13
c ---[ 267]---> BDD-cost:   17
c ---[ 266]---> BDD-cost:   17
c ---[ 265]---> BDD-cost:   17
c ---[ 264]---> BDD-cost:   13
c ---[ 263]---> BDD-cost:   12
c ---[ 262]---> BDD-cost:   11
c ---[ 261]---> BDD-cost:   17
c ---[ 260]---> BDD-cost:   17
c ---[ 259]---> BDD-cost:   17
c ---[ 258]---> BDD-cost:   17
c ---[ 257]---> BDD-cost:   17
c ---[ 256]---> BDD-cost:   11
c ---[ 255]---> BDD-cost:   17
c ---[ 254]---> BDD-cost:   12
c ---[ 253]---> BDD-cost:   13
c ---[ 252]---> BDD-cost:   11
c ---[ 251]---> BDD-cost:   15
c ---[ 250]---> BDD-cost:   13
c ---[ 249]---> BDD-cost:   13
c ---[ 248]---> BDD-cost:   17
c ---[ 247]---> BDD-cost:   17
c ---[ 246]---> BDD-cost:   13
c ---[ 245]---> BDD-cost:   13
c ---[ 244]---> BDD-cost:   11
c ---[ 243]---> BDD-cost:   13
c ---[ 242]---> BDD-cost:   13
c ---[ 241]---> BDD-cost:   13
c ---[ 240]---> BDD-cost:   13
c ---[ 239]---> BDD-cost:   13
c ---[ 238]---> BDD-cost:   13
c ---[ 237]---> BDD-cost:   11
c ---[ 236]---> BDD-cost:   13
c ---[ 235]---> BDD-cost:   13
c ---[ 234]---> BDD-cost:   11
c ---[ 233]---> BDD-cost:   13
c ---[ 232]---> BDD-cost:   13
c ---[ 231]---> BDD-cost:   13
c ---[ 230]---> BDD-cost:   13
c ---[ 229]---> BDD-cost:   13
c ---[ 228]---> BDD-cost:   13
c ---[ 227]---> BDD-cost:   11
c ---[ 226]---> BDD-cost:   11
c ---[ 225]---> BDD-cost:   11
c ---[ 224]---> BDD-cost:   11
c ---[ 223]---> BDD-cost:   11
c ---[ 222]---> BDD-cost:   11
c ---[ 221]---> BDD-cost:   11
c ---[ 220]---> BDD-cost:   13
c ---[ 219]---> BDD-cost:   11
c ---[ 218]---> BDD-cost:   11
c ---[ 217]---> BDD-cost:   11
c ---[ 216]---> BDD-cost:   11
c ---[ 215]---> BDD-cost:   11
c ---[ 214]---> BDD-cost:   11
c ---[ 213]---> BDD-cost:   11
c ---[ 212]---> BDD-cost:   11
c ---[ 211]---> BDD-cost:   11
c ---[ 210]---> BDD-cost:   11
c ---[ 209]---> BDD-cost:   12
c ---[ 208]---> BDD-cost:   14
c ---[ 207]---> BDD-cost:   12
c ---[ 206]---> BDD-cost:   11
c ---[ 205]---> BDD-cost:   14
c ---[ 204]---> BDD-cost:   14
c ---[ 203]---> BDD-cost:   14
c ---[ 202]---> BDD-cost:   14
c ---[ 201]---> BDD-cost:   14
c ---[ 200]---> BDD-cost:   11
c ---[ 199]---> BDD-cost:   14
c ---[ 198]---> BDD-cost:   12
c ---[ 197]---> BDD-cost:   12
c ---[ 196]---> BDD-cost:   11
c ---[ 195]---> BDD-cost:   14
c ---[ 194]---> BDD-cost:   14
c ---[ 193]---> BDD-cost:   13
c ---[ 192]---> BDD-cost:   14
c ---[ 191]---> BDD-cost:   14
c ---[ 190]---> BDD-cost:   14
c ---[ 189]---> BDD-cost:   12
c ---[ 188]---> BDD-cost:   11
c ---[ 187]---> BDD-cost:   11
c ---[ 186]---> BDD-cost:   14
c ---[ 185]---> BDD-cost:   14
c ---[ 184]---> BDD-cost:   14
c ---[ 183]---> BDD-cost:   14
c ---[ 182]---> BDD-cost:   14
c ---[ 181]---> BDD-cost:   11
c ---[ 180]---> BDD-cost:   14
c ---[ 179]---> BDD-cost:   12
c ---[ 178]---> BDD-cost:   11
c ---[ 177]---> BDD-cost:   14
c ---[ 176]---> BDD-cost:   11
c ---[ 175]---> BDD-cost:   12
c ---[ 174]---> BDD-cost:   14
c ---[ 173]---> BDD-cost:   14
c ---[ 172]---> BDD-cost:   14
c ---[ 171]---> BDD-cost:   14
c ---[ 170]---> BDD-cost:   17
c ---[ 169]---> BDD-cost:   12
c ---[ 168]---> BDD-cost:   11
c ---[ 167]---> BDD-cost:   15
c ---[ 166]---> BDD-cost:   16
c ---[ 165]---> BDD-cost:   17
c ---[ 164]---> BDD-cost:   12
c ---[ 163]---> BDD-cost:   15
c ---[ 162]---> BDD-cost:   15
c ---[ 161]---> BDD-cost:   11
c ---[ 160]---> BDD-cost:   15
c ---[ 159]---> BDD-cost:   12
c ---[ 158]---> BDD-cost:   11
c ---[ 157]---> BDD-cost:   15
c ---[ 156]---> BDD-cost:   13
c ---[ 155]---> BDD-cost:   13
c ---[ 154]---> BDD-cost:   15
c ---[ 153]---> BDD-cost:   12
c ---[ 152]---> BDD-cost:   17
c ---[ 151]---> BDD-cost:   15
c ---[ 150]---> BDD-cost:   12
c ---[ 149]---> BDD-cost:   11
c ---[ 148]---> BDD-cost:   15
c ---[ 147]---> BDD-cost:   15
c ---[ 146]---> BDD-cost:   15
c ---[ 145]---> BDD-cost:   15
c ---[ 144]---> BDD-cost:   15
c ---[ 143]---> BDD-cost:   11
c ---[ 142]---> BDD-cost:   12
c ---[ 141]---> BDD-cost:   15
c ---[ 140]---> BDD-cost:   12
c ---[ 139]---> BDD-cost:   11
c ---[ 138]---> BDD-cost:   15
c ---[ 137]---> BDD-cost:   15
c ---[ 136]---> BDD-cost:   15
c ---[ 135]---> BDD-cost:   15
c ---[ 134]---> BDD-cost:   15
c ---[ 133]---> BDD-cost:   12
c ---[ 132]---> BDD-cost:   12
c ---[ 131]---> BDD-cost:   12
c ---[ 130]---> BDD-cost:   11
c ---[ 129]---> BDD-cost:   12
c ---[ 128]---> BDD-cost:   12
c ---[ 127]---> BDD-cost:   12
c ---[ 126]---> BDD-cost:   12
c ---[ 125]---> BDD-cost:   12
c ---[ 124]---> BDD-cost:   11
c ---[ 123]---> BDD-cost:   12
c ---[ 122]---> BDD-cost:   12
c ---[ 121]---> BDD-cost:   11
c ---[ 120]---> BDD-cost:   11
c ---[ 119]---> BDD-cost:   12
c ---[ 118]---> BDD-cost:   12
c ---[ 117]---> BDD-cost:   12
c ---[ 116]---> BDD-cost:   12
c ---[ 115]---> BDD-cost:   12
c ---[ 114]---> BDD-cost:   17
c ---[ 113]---> BDD-cost:   12
c ---[ 112]---> BDD-cost:   11
c ---[ 111]---> BDD-cost:   15
c ---[ 110]---> BDD-cost:   16
c ---[ 109]---> BDD-cost:   12
c ---[ 108]---> BDD-cost:   17
c ---[ 107]---> BDD-cost:   15
c ---[ 106]---> BDD-cost:   15
c ---[ 105]---> BDD-cost:   11
c ---[ 104]---> BDD-cost:   15
c ---[ 103]---> BDD-cost:   12
c ---[ 102]---> BDD-cost:   11
c ---[ 101]---> BDD-cost:   15
c ---[ 100]---> BDD-cost:   13
c ---[  99]---> BDD-cost:   13
c ---[  98]---> BDD-cost:   12
c ---[  97]---> BDD-cost:   15
c ---[  96]---> BDD-cost:   17
c ---[  95]---> BDD-cost:   17
c ---[  94]---> BDD-cost:   12
c ---[  93]---> BDD-cost:   11
c ---[  92]---> BDD-cost:   15
c ---[  91]---> BDD-cost:   16
c ---[  90]---> BDD-cost:   17
c ---[  89]---> BDD-cost:   19
c ---[  88]---> BDD-cost:   16
c ---[  87]---> BDD-cost:   11
c ---[  86]---> BDD-cost:   11
c ---[  85]---> BDD-cost:   17
c ---[  84]---> BDD-cost:   12
c ---[  83]---> BDD-cost:   11
c ---[  82]---> BDD-cost:   15
c ---[  81]---> BDD-cost:   13
c ---[  80]---> BDD-cost:   13
c ---[  79]---> BDD-cost:   19
c ---[  78]---> BDD-cost:   17
c ---[  77]---> BDD-cost:   12
c ---[  76]---> BDD-cost:   13
c ---[  75]---> BDD-cost:   12
c ---[  74]---> BDD-cost:   12
c ---[  73]---> BDD-cost:   12
c ---[  72]---> BDD-cost:   12
c ---[  71]---> BDD-cost:   17
c ---[  70]---> BDD-cost:   12
c ---[  69]---> BDD-cost:   11
c ---[  68]---> BDD-cost:   15
c ---[  67]---> BDD-cost:   17
c ---[  66]---> BDD-cost:   17
c ---[  65]---> BDD-cost:   13
c ---[  64]---> BDD-cost:   17
c ---[  63]---> BDD-cost:   17
c ---[  62]---> BDD-cost:   11
c ---[  61]---> BDD-cost:   17
c ---[  60]---> BDD-cost:   12
c ---[  59]---> BDD-cost:   11
c ---[  58]---> BDD-cost:   15
c ---[  57]---> BDD-cost:   13
c ---[  56]---> BDD-cost:   13
c ---[  55]---> BDD-cost:   17
c ---[  54]---> BDD-cost:   13
c ---[  53]---> BDD-cost:   17
c ---[  52]---> BDD-cost:   17
c ---[  51]---> BDD-cost:   12
c ---[  50]---> BDD-cost:   11
c ---[  49]---> BDD-cost:   15
c ---[  48]---> BDD-cost:   17
c ---[  47]---> BDD-cost:   17
c ---[  46]---> BDD-cost:   17
c ---[  45]---> BDD-cost:   17
c ---[  44]---> BDD-cost:   11
c ---[  43]---> BDD-cost:   13
c ---[  42]---> BDD-cost:   17
c ---[  41]---> BDD-cost:   12
c ---[  40]---> BDD-cost:   11
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   13
c ---[  37]---> BDD-cost:   13
c ---[  36]---> BDD-cost:   17
c ---[  35]---> BDD-cost:   17
c ---[  34]---> BDD-cost:   15
c ---[  33]---> BDD-cost:   12
c ---[  32]---> BDD-cost:   13
c ---[  31]---> BDD-cost:   11
c ---[  30]---> BDD-cost:   15
c ---[  29]---> BDD-cost:   15
c ---[  28]---> BDD-cost:   15
c ---[  27]---> BDD-cost:   15
c ---[  26]---> BDD-cost:   15
c ---[  25]---> BDD-cost:   11
c ---[  24]---> BDD-cost:   15
c ---[  23]---> BDD-cost:   12
c ---[  22]---> BDD-cost:   11
c ---[  21]---> BDD-cost:   11
c ---[  20]---> BDD-cost:   15
c ---[  19]---> BDD-cost:   15
c ---[  18]---> BDD-cost:   13
c ---[  17]---> BDD-cost:   15
c ---[  16]---> BDD-cost:   15
c ---[  15]---> BDD-cost:   17
c ---[  14]---> BDD-cost:   12
c ---[  13]---> BDD-cost:   11
c ---[  12]---> BDD-cost:   15
c ---[  11]---> BDD-cost:   16
c ---[  10]---> BDD-cost:   13
c ---[   9]---> BDD-cost:   17
c ---[   8]---> BDD-cost:   14
c ---[   7]---> BDD-cost:   16
c ---[   6]---> BDD-cost:   11
c ---[   5]---> BDD-cost:   17
c ---[   4]---> BDD-cost:   12
c ---[   3]---> BDD-cost:   11
c ---[   2]---> BDD-cost:   15
c ---[   1]---> BDD-cost:   13
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   83813   292060 |   27937       0        0     nan |  0.000 % |
c |       101 |   83806   292037 |   30730      99      296     3.0 | 20.432 % |
c |       251 |   83718   291747 |   33803     238      721     3.0 | 20.504 % |
c |       476 |   83663   291566 |   37184     456     1409     3.1 | 20.549 % |
c |       813 |   83349   290482 |   40902     750     2332     3.1 | 20.835 % |
c |      1319 |   82809   288644 |   44992    1186     3671     3.1 | 21.310 % |
c |      2078 |   82375   287132 |   49492    1880     5986     3.2 | 21.678 % |
c |      3217 |   81934   285637 |   54441    2956     9904     3.4 | 22.071 % |
c |      4925 |   81577   284424 |   59885    4622    17053     3.7 | 22.398 % |
c |      7487 |   81485   284112 |   65873    7170    29090     4.1 | 22.480 % |
c |     11333 |   81327   283598 |   72461   10994    51248     4.7 | 22.633 % |
c |     17100 |   81318   283569 |   79707   16760   189829    11.3 | 22.643 % |
c |     25750 |   81309   283540 |   87678   25409   498287    19.6 | 22.653 % |
c |     38725 |   81271   283412 |   96446   38377   872152    22.7 | 22.684 % |
c |     58187 |   81194   283147 |  106090   57826  2217140    38.3 | 22.756 % |
c |     87379 |   80950   282301 |  116699   86988  5011094    57.6 | 22.970 % |
c |    131168 |   80810   281827 |  128369   20608  1985972    96.4 | 23.098 % |
c |    196853 |   80472   280635 |  141206   86251  5878345    68.2 | 23.419 % |
c |    295379 |   79924   278809 |  155327   62756  1646877    26.2 | 23.956 % |
c |    443168 |   79810   278439 |  170860   63691  7812906   122.7 | 24.068 % |
c ==============================================================================
c [1mFound solution: 2130074[0m
c ---[   0]---> Adder-cost: 11288   maxlim: 3337736   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    516759 |  158591   559868 |   52863  137264  9778406    71.2 | 24.068 % |
c |    516860 |  158591   559868 |   58149   25530   237369     9.3 | 15.385 % |
c |    517010 |  158591   559868 |   63964   25680   238080     9.3 | 15.385 % |
c |    517235 |  158575   559816 |   70360   25903   239262     9.2 | 15.395 % |
c |    517572 |  158575   559816 |   77396   26240   240824     9.2 | 15.395 % |
c |    518078 |  158568   559793 |   85136   26744   243334     9.1 | 15.398 % |
c |    518837 |  158558   559755 |   93650   27501   247186     9.0 | 15.401 % |
c |    519977 |  158526   559651 |  103015   28636   253178     8.8 | 15.420 % |
c |    521685 |  158485   559518 |  113316   30338   263602     8.7 | 15.446 % |
c |    524247 |  158478   559495 |  124648   32897   281696     8.6 | 15.450 % |
c |    528091 |  158478   559495 |  137113   36741   355809     9.7 | 15.450 % |
c |    533858 |  158462   559443 |  150824   42506   443278    10.4 | 15.459 % |
c |    542508 |  158462   559443 |  165906   51156  1258655    24.6 | 15.459 % |
c |    555482 |  158405   559258 |  182497   64120  1449994    22.6 | 15.495 % |
c |    574944 |  158382   559181 |  200747   83577  1737207    20.8 | 15.505 % |
c ==============================================================================
c [1mFound solution: 1732053[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3735757   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    601933 |  158312   559045 |   52770  110553  2628370    23.8 | 15.505 % |
c |    602033 |  158312   559045 |   58047   28365   281388     9.9 | 15.585 % |
c |    602183 |  158312   559045 |   63851   28515   282282     9.9 | 15.585 % |
c |    602408 |  158312   559045 |   70236   28740   283948     9.9 | 15.585 % |
c |    602745 |  158312   559045 |   77260   29077   286816     9.9 | 15.585 % |
c |    603251 |  158312   559045 |   84986   29583   291880     9.9 | 15.585 % |
c |    604010 |  158312   559045 |   93485   30342   298857     9.8 | 15.585 % |
c |    605149 |  158312   559045 |  102833   31481   310707     9.9 | 15.585 % |
c |    606857 |  158303   559016 |  113117   33188   335678    10.1 | 15.591 % |
c |    609420 |  158289   558966 |  124428   35749   369683    10.3 | 15.598 % |
c |    613264 |  158273   558914 |  136871   39590   419094    10.6 | 15.607 % |
c |    619031 |  158257   558858 |  150558   45355   518600    11.4 | 15.617 % |
c |    627680 |  158235   558786 |  165614   54001   648845    12.0 | 15.630 % |
c |    640654 |  158196   558651 |  182176   66970   904476    13.5 | 15.646 % |
c |    660115 |  157977   557916 |  200393   86392  1180406    13.7 | 15.769 % |
c |    689307 |  157951   557826 |  220433  115580  4556236    39.4 | 15.782 % |
c |    733098 |  157935   557774 |  242476  159367 12136486    76.2 | 15.792 % |
c ==============================================================================
c [1mFound solution: 1693753[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3774057   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    743166 |  157949   557927 |   52649  169435 12338940    72.8 | 15.792 % |
c |    743266 |  157949   557927 |   57913   31190  1026509    32.9 | 15.814 % |
c |    743416 |  157949   557927 |   63705   31340  1027676    32.8 | 15.814 % |
c |    743642 |  157949   557927 |   70075   31566  1028800    32.6 | 15.814 % |
c |    743979 |  157949   557927 |   77083   31903  1030672    32.3 | 15.814 % |
c |    744485 |  157949   557927 |   84791   32409  1033981    31.9 | 15.814 % |
c |    745244 |  157949   557927 |   93270   33168  1038519    31.3 | 15.814 % |
c |    746387 |  157949   557927 |  102598   34311  1044538    30.4 | 15.814 % |
c |    748095 |  157949   557927 |  112857   36019  1054044    29.3 | 15.814 % |
c |    750657 |  157949   557927 |  124143   38581  1070834    27.8 | 15.814 % |
c |    754501 |  157949   557927 |  136557   42425  1099494    25.9 | 15.814 % |
c |    760267 |  157949   557927 |  150213   48191  1165381    24.2 | 15.814 % |
c |    768918 |  157949   557927 |  165235   56842  2136791    37.6 | 15.814 % |
c |    781892 |  157883   557707 |  181758   69800  2566379    36.8 | 15.853 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:  5558 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.90 2/54 5554
Raw data (stat): 5554 (runsolver) R 5553 20224 20223 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 784705522 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.93 0.95 0.90 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0017 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0021 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0024 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0032 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0036 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0049 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0061 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0061 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.96 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.007 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 5558
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.085 s]
Raw data (loadavg): 1.15 1.00 0.92 2/55 5611
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.086 s]
Raw data (loadavg): 1.13 1.00 0.92 2/55 5611
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.086 s]
Raw data (loadavg): 1.11 1.00 0.92 2/55 5611
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.09 s]
Raw data (loadavg): 1.09 1.00 0.92 2/55 5611
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.1 s]
Raw data (loadavg): 1.08 1.00 0.92 2/55 5611
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.11 s]
Raw data (loadavg): 1.07 1.00 0.92 2/55 5611
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.11 s]
Raw data (loadavg): 1.06 1.00 0.92 2/55 5611
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.11 s]
Raw data (loadavg): 1.05 1.00 0.92 2/55 5611
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.11 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 5613
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.11 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 5613
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.11 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 5613
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.11 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 5613
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.11 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 5613
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.11 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 5613
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.11 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 5613
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.11 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 5613
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.11 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 5613
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.11 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 5613
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 5613
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 5613
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 5613
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 5613
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 5613
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 5613
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.12 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 5613
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.12 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 5613
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.82 s]
Raw data (loadavg): 1.00 1.00 0.92 1/53 5613
Raw data (stat): 5554 (minisat+_script) S 5553 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784705522 2174976 226 4294967295 134512640 135087896 3221224544 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.82
CPU time (s): 1229.88
CPU user time (s): 1228.84
CPU system time (s): 1.04284
CPU usage (%): 100.005
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####