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-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-rout.opb
MD5SUM	26f8714f5bbc8fb10d3a4aeb3a0f315a
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	31
Biggest coefficient in the objective function	1073741824
Number of bits for the biggest coefficient in the objective function	31
Sum of the numbers in the objective function	2147483647
Number of bits of the sum of numbers in the objective function	31
Biggest number in a constraint	26904326400
Number of bits of the biggest number in a constraint	35
Biggest sum of numbers in a constraint	81230087655
Number of bits of the biggest sum of numbers	37
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.218966
Number of variables	7561
Total number of constraints	606
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	314
Number of constraints which are nor clauses,nor cardinality constraints	292
Minimum length of a constraint	1
Maximum length of a constraint	917
Trace number 30784

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-05-25 19:30:06 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22184 boxname=wulflinc7 idbench=1000 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  26f8714f5bbc8fb10d3a4aeb3a0f315a  /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-rout.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-rout.opb
IDLAUNCH: 22184
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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.050
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:        467472 kB
Buffers:         33936 kB
Cached:         513184 kB
SwapCached:        756 kB
Active:          74620 kB
Inactive:       474676 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        467220 kB
SwapTotal:     2097136 kB
SwapFree:      2095584 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5140 kB
Slab:            12176 kB
Committed_AS:    63588 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 19:50:36 (client local time) WITH STATUS 152 IN 1229.89 SECONDS
stats: 22184 7 1229.89 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 337 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###############################
c   -- Clauses(.)/Splits(s): ...............
c ---[ 320]---> Adder-cost: 3908   maxlim: 27410865895   bits: 36/35
c ---[ 319]---> BDD-cost:   37
c ---[ 318]---> BDD-cost:   16
c ---[ 317]---> BDD-cost:   16
c ---[ 316]---> BDD-cost:   28
c ---[ 315]---> BDD-cost:   28
c ---[ 314]---> BDD-cost:   28
c ---[ 313]---> BDD-cost:   28
c ---[ 312]---> BDD-cost:   28
c ---[ 311]---> BDD-cost:   28
c ---[ 310]---> BDD-cost:   28
c ---[ 309]---> BDD-cost:   28
c ---[ 308]---> BDD-cost:   37
c ---[ 307]---> BDD-cost:   28
c ---[ 306]---> BDD-cost:   28
c ---[ 305]---> BDD-cost:   16
c ---[ 304]---> BDD-cost:   16
c ---[ 303]---> BDD-cost:   16
c ---[ 302]---> BDD-cost:   16
c ---[ 301]---> BDD-cost:   16
c ---[ 300]---> BDD-cost:   16
c ---[ 299]---> BDD-cost:   16
c ---[ 298]---> BDD-cost:   16
c ---[ 297]---> BDD-cost:   37
c ---[ 296]---> BDD-cost:   16
c ---[ 295]---> BDD-cost:   16
c ---[ 294]---> BDD-cost:   16
c ---[ 293]---> BDD-cost:   16
c ---[ 292]---> BDD-cost:   16
c ---[ 291]---> BDD-cost:   16
c ---[ 290]---> BDD-cost:   16
c ---[ 289]---> BDD-cost:   16
c ---[ 288]---> BDD-cost:   16
c ---[ 287]---> BDD-cost:   16
c ---[ 286]---> BDD-cost:   37
c ---[ 285]---> BDD-cost:   16
c ---[ 284]---> BDD-cost:   16
c ---[ 283]---> BDD-cost:   16
c ---[ 282]---> BDD-cost:   16
c ---[ 281]---> BDD-cost:   16
c ---[ 280]---> BDD-cost:   16
c ---[ 279]---> BDD-cost:   16
c ---[ 278]---> BDD-cost:   16
c ---[ 277]---> BDD-cost:   16
c ---[ 276]---> BDD-cost:   16
c ---[ 275]---> BDD-cost:   37
c ---[ 274]---> BDD-cost:   16
c ---[ 273]---> BDD-cost:   16
c ---[ 272]---> BDD-cost:   16
c ---[ 271]---> BDD-cost:   16
c ---[ 270]---> BDD-cost:   16
c ---[ 269]---> BDD-cost:   16
c ---[ 268]---> BDD-cost:   16
c ---[ 267]---> BDD-cost:   16
c ---[ 266]---> BDD-cost:   16
c ---[ 265]---> BDD-cost:   16
c ---[ 264]---> BDD-cost:   37
c ---[ 263]---> BDD-cost:   16
c ---[ 262]---> BDD-cost:   16
c ---[ 261]---> BDD-cost:   16
c ---[ 260]---> BDD-cost:   16
c ---[ 259]---> BDD-cost:   16
c ---[ 258]---> BDD-cost:   16
c ---[ 257]---> BDD-cost:   16
c ---[ 256]---> BDD-cost:   16
c ---[ 255]---> BDD-cost:   16
c ---[ 254]---> BDD-cost:   16
c ---[ 253]---> BDD-cost:   37
c ---[ 252]---> BDD-cost:   16
c ---[ 251]---> BDD-cost:   16
c ---[ 250]---> BDD-cost:   16
c ---[ 249]---> BDD-cost:   16
c ---[ 248]---> BDD-cost:   16
c ---[ 247]---> BDD-cost:   16
c ---[ 246]---> BDD-cost:   16
c ---[ 245]---> BDD-cost:   16
c ---[ 244]---> BDD-cost:   16
c ---[ 243]---> BDD-cost:   16
c ---[ 242]---> BDD-cost:   37
c ---[ 241]---> BDD-cost:   16
c ---[ 240]---> BDD-cost:   16
c ---[ 239]---> BDD-cost:   16
c ---[ 238]---> BDD-cost:   16
c ---[ 237]---> BDD-cost:   16
c ---[ 236]---> BDD-cost:   16
c ---[ 235]---> BDD-cost:   16
c ---[ 234]---> BDD-cost:   16
c ---[ 233]---> BDD-cost:   16
c ---[ 232]---> BDD-cost:   16
c ---[ 231]---> BDD-cost:   37
c ---[ 230]---> BDD-cost:   16
c ---[ 229]---> BDD-cost:   16
c ---[ 228]---> BDD-cost:   16
c ---[ 227]---> BDD-cost:   16
c ---[ 226]---> BDD-cost:   16
c ---[ 225]---> BDD-cost:   16
c ---[ 224]---> BDD-cost:   16
c ---[ 223]---> BDD-cost:   16
c ---[ 222]---> BDD-cost:   16
c ---[ 221]---> BDD-cost:   16
c ---[ 220]---> BDD-cost:   37
c ---[ 219]---> BDD-cost:   16
c ---[ 218]---> BDD-cost:   16
c ---[ 217]---> BDD-cost:   16
c ---[ 216]---> BDD-cost:   16
c ---[ 215]---> BDD-cost:   16
c ---[ 214]---> BDD-cost:   16
c ---[ 213]---> BDD-cost:   16
c ---[ 212]---> BDD-cost:   16
c ---[ 211]---> BDD-cost:   16
c ---[ 210]---> BDD-cost:   16
c ---[ 209]---> Adder-cost: 604   maxlim: 25598   bits: 15/15
c ---[ 208]---> BDD-cost:   37
c ---[ 207]---> BDD-cost:   16
c ---[ 206]---> BDD-cost:   16
c ---[ 205]---> BDD-cost:   16
c ---[ 204]---> BDD-cost:   16
c ---[ 203]---> BDD-cost:   16
c ---[ 202]---> BDD-cost:   16
c ---[ 201]---> BDD-cost:   16
c ---[ 200]---> BDD-cost:   16
c ---[ 199]---> BDD-cost:   16
c ---[ 198]---> BDD-cost:   16
c ---[ 197]---> BDD-cost:   37
c ---[ 196]---> BDD-cost:   16
c ---[ 195]---> BDD-cost:   16
c ---[ 194]---> BDD-cost:   16
c ---[ 193]---> BDD-cost:   16
c ---[ 192]---> BDD-cost:   16
c ---[ 191]---> BDD-cost:   16
c ---[ 190]---> BDD-cost:   16
c ---[ 189]---> BDD-cost:   16
c ---[ 188]---> BDD-cost:   16
c ---[ 187]---> BDD-cost:   16
c ---[ 185]---> Sorter-cost:  441     Base: 2
c ---[ 184]---> BDD-cost:   16
c ---[ 183]---> BDD-cost:   16
c ---[ 182]---> BDD-cost:   16
c ---[ 181]---> BDD-cost:   16
c ---[ 180]---> BDD-cost:   16
c ---[ 179]---> BDD-cost:   16
c ---[ 178]---> BDD-cost:   16
c ---[ 177]---> BDD-cost:   16
c ---[ 176]---> BDD-cost:   16
c ---[ 175]---> BDD-cost:   16
c ---[ 173]---> Sorter-cost:  441     Base: 2
c ---[ 172]---> BDD-cost:   16
c ---[ 171]---> BDD-cost:   16
c ---[ 170]---> BDD-cost:   16
c ---[ 169]---> BDD-cost:   16
c ---[ 168]---> BDD-cost:   16
c ---[ 167]---> BDD-cost:   16
c ---[ 166]---> BDD-cost:   16
c ---[ 165]---> BDD-cost:   16
c ---[ 164]---> BDD-cost:   16
c ---[ 163]---> BDD-cost:   16
c ---[ 161]---> Sorter-cost:  441     Base: 2
c ---[ 160]---> BDD-cost:   16
c ---[ 159]---> BDD-cost:   16
c ---[ 158]---> BDD-cost:   16
c ---[ 157]---> BDD-cost:   16
c ---[ 156]---> BDD-cost:   16
c ---[ 155]---> BDD-cost:   16
c ---[ 154]---> BDD-cost:   16
c ---[ 153]---> BDD-cost:   16
c ---[ 152]---> BDD-cost:   16
c ---[ 151]---> BDD-cost:   16
c ---[ 149]---> Sorter-cost:  441     Base: 2
c ---[ 148]---> BDD-cost:   16
c ---[ 147]---> BDD-cost:   16
c ---[ 146]---> BDD-cost:   16
c ---[ 145]---> BDD-cost:   16
c ---[ 144]---> BDD-cost:   16
c ---[ 143]---> BDD-cost:   16
c ---[ 142]---> BDD-cost:   16
c ---[ 141]---> BDD-cost:   16
c ---[ 140]---> BDD-cost:   16
c ---[ 139]---> BDD-cost:   16
c ---[ 137]---> Sorter-cost:  441     Base: 2
c ---[ 136]---> BDD-cost:   16
c ---[ 135]---> BDD-cost:   16
c ---[ 134]---> BDD-cost:   16
c ---[ 133]---> BDD-cost:   16
c ---[ 132]---> BDD-cost:   16
c ---[ 131]---> BDD-cost:   16
c ---[ 130]---> BDD-cost:   16
c ---[ 129]---> BDD-cost:   16
c ---[ 128]---> BDD-cost:   16
c ---[ 127]---> BDD-cost:   16
c ---[ 125]---> Sorter-cost:  347     Base: 2
c ---[ 124]---> BDD-cost:   16
c ---[ 123]---> BDD-cost:   16
c ---[ 122]---> BDD-cost:   16
c ---[ 121]---> BDD-cost:   16
c ---[ 120]---> BDD-cost:   16
c ---[ 119]---> BDD-cost:   16
c ---[ 118]---> BDD-cost:   16
c ---[ 117]---> BDD-cost:   16
c ---[ 116]---> BDD-cost:   16
c ---[ 115]---> BDD-cost:   16
c ---[ 113]---> Sorter-cost:  347     Base: 2
c ---[ 112]---> BDD-cost:   16
c ---[ 111]---> BDD-cost:   16
c ---[ 110]---> BDD-cost:   16
c ---[ 109]---> BDD-cost:   16
c ---[ 108]---> BDD-cost:   16
c ---[ 107]---> BDD-cost:   16
c ---[ 106]---> BDD-cost:   16
c ---[ 105]---> BDD-cost:   16
c ---[ 104]---> BDD-cost:   16
c ---[ 103]---> BDD-cost:   16
c ---[ 101]---> Sorter-cost:  347     Base: 2
c ---[ 100]---> BDD-cost:   16
c ---[  99]---> BDD-cost:   16
c ---[  98]---> Adder-cost: 604   maxlim: 25598   bits: 15/15
c ---[  96]---> Sorter-cost:  347     Base: 2
c ---[  94]---> Sorter-cost:  347     Base: 2
c ---[  92]---> Sorter-cost:  515     Base: 2
c ---[  90]---> Sorter-cost:  515     Base: 2
c ---[  88]---> Sorter-cost:  515     Base: 2
c ---[  86]---> Sorter-cost:  515     Base: 2
c ---[  84]---> Sorter-cost:  515     Base: 2
c ---[  82]---> Adder-cost: 698   maxlim: 172017   bits: 19/18
c ---[  80]---> Adder-cost: 698   maxlim: 172017   bits: 19/18
c ---[  78]---> Adder-cost: 698   maxlim: 172017   bits: 19/18
c ---[  77]---> Adder-cost: 604   maxlim: 25598   bits: 15/15
c ---[  75]---> Adder-cost: 698   maxlim: 172017   bits: 19/18
c ---[  73]---> Adder-cost: 698   maxlim: 172017   bits: 19/18
c ---[  71]---> Adder-cost: 586   maxlim: 73719   bits: 18/17
c ---[  69]---> Adder-cost: 586   maxlim: 73719   bits: 18/17
c ---[  67]---> Adder-cost: 586   maxlim: 73719   bits: 18/17
c ---[  65]---> Adder-cost: 586   maxlim: 73719   bits: 18/17
c ---[  63]---> Adder-cost: 586   maxlim: 73719   bits: 18/17
c ---[  61]---> Adder-cost: 798   maxlim: 172011   bits: 19/18
c ---[  59]---> Adder-cost: 798   maxlim: 172011   bits: 19/18
c ---[  57]---> Adder-cost: 798   maxlim: 172011   bits: 19/18
c ---[  56]---> Adder-cost: 604   maxlim: 25598   bits: 15/15
c ---[  54]---> Adder-cost: 798   maxlim: 172011   bits: 19/18
c ---[  52]---> Adder-cost: 798   maxlim: 172011   bits: 19/18
c ---[  51]---> BDD-cost:   16
c ---[  50]---> BDD-cost:   16
c ---[  49]---> BDD-cost:   16
c ---[  48]---> BDD-cost:   16
c ---[  47]---> BDD-cost:   16
c ---[  46]---> BDD-cost:   16
c ---[  45]---> BDD-cost:   16
c ---[  44]---> BDD-cost:   16
c ---[  43]---> Adder-cost: 604   maxlim: 25598   bits: 15/15
c ---[  42]---> BDD-cost:   16
c ---[  41]---> BDD-cost:   16
c ---[  40]---> BDD-cost:   16
c ---[  39]---> BDD-cost:   16
c ---[  38]---> BDD-cost:   16
c ---[  37]---> BDD-cost:   16
c ---[  36]---> BDD-cost:   16
c ---[  35]---> BDD-cost:   16
c ---[  34]---> BDD-cost:   16
c ---[  33]---> BDD-cost:   16
c ---[  32]---> BDD-cost:   37
c ---[  31]---> BDD-cost:   16
c ---[  30]---> BDD-cost:   16
c ---[  29]---> BDD-cost:   16
c ---[  28]---> BDD-cost:   16
c ---[  27]---> BDD-cost:   16
c ---[  26]---> BDD-cost:   16
c ---[  25]---> BDD-cost:   16
c ---[  24]---> BDD-cost:   16
c ---[  23]---> BDD-cost:   16
c ---[  22]---> BDD-cost:   16
c ---[  21]---> BDD-cost:   37
c ---[  20]---> BDD-cost:   16
c ---[  19]---> BDD-cost:   16
c ---[  18]---> BDD-cost:   16
c ---[  17]---> BDD-cost:   16
c ---[  16]---> BDD-cost:   16
c ---[  15]---> BDD-cost:   16
c ---[  14]---> BDD-cost:   16
c ---[  13]---> BDD-cost:   16
c ---[  12]---> BDD-cost:   16
c ---[  11]---> BDD-cost:   16
c ---[  10]---> BDD-cost:   84
c ---[   9]---> BDD-cost:   16
c ---[   8]---> BDD-cost:   16
c ---[   7]---> BDD-cost:   16
c ---[   6]---> BDD-cost:   16
c ---[   5]---> BDD-cost:   16
c ---[   4]---> BDD-cost:   16
c ---[   3]---> BDD-cost:   16
c ---[   2]---> BDD-cost:   16
c ---[   1]---> BDD-cost:   16
c ---[   0]---> BDD-cost:   16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  141334   476894 |   47111       0        0     nan |  0.000 % |
c |       100 |  141009   476121 |   51822      63      728    11.6 | 16.395 % |
c |       253 |  141009   476121 |   57004     216     8229    38.1 | 16.395 % |
c |       481 |  140993   476069 |   62704     441    13300    30.2 | 16.404 % |
c |       819 |  140984   476040 |   68975     778    21502    27.6 | 16.410 % |
c |      1326 |  140943   475948 |   75872    1284    40393    31.5 | 16.441 % |
c |      2087 |  140917   475858 |   83460    2039    66027    32.4 | 16.453 % |
c |      3230 |  140867   475704 |   91806    3178   111040    34.9 | 16.484 % |
c |      4940 |  140592   475066 |  100986    4848   191834    39.6 | 16.751 % |
c |      7505 |  140548   474936 |  111085    7406   425128    57.4 | 16.779 % |
c |     11349 |  140172   473904 |  122193   11201   566338    50.6 | 17.055 % |
c ==============================================================================
c [1mFound solution: 1075341824[0m
c ---[   0]---> BDD-cost:   21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12367 |  139910   473303 |   46636   12206   598115    49.0 | 17.055 % |
c |     12467 |  139901   473272 |   51299   12303   599071    48.7 | 17.316 % |
c |     12617 |  139700   472818 |   56429   12438   605241    48.7 | 17.494 % |
c |     12843 |  139642   472626 |   62072   12657   610887    48.3 | 17.531 % |
c |     13180 |  139642   472626 |   68279   12994   633688    48.8 | 17.531 % |
c |     13688 |  139555   472418 |   75107   13498   649237    48.1 | 17.601 % |
c |     14449 |  139555   472418 |   82618   14259   667677    46.8 | 17.601 % |
c |     15588 |  139555   472418 |   90880   15398   711516    46.2 | 17.601 % |
c |     17296 |  138935   470919 |   99968   17003   772944    45.5 | 18.127 % |
c |     19859 |  138198   469163 |  109965   19464  1106881    56.9 | 18.772 % |
c |     23704 |  138173   469080 |  120961   23305  1304092    56.0 | 18.781 % |
c |     29470 |  137919   468460 |  133057   29041  1532206    52.8 | 19.006 % |
c |     38119 |  137706   467945 |  146363   37668  2045924    54.3 | 19.202 % |
c |     51094 |  137582   467592 |  161000   50627  2567663    50.7 | 19.282 % |
c |     70557 |  136344   464117 |  177100   69937  3649132    52.2 | 20.106 % |
c |     99749 |  135236   461135 |  194810   98952  6308091    63.7 | 20.892 % |
c ==============================================================================
c [1mFound solution: 1075334656[0m
c ---[   0]---> BDD-cost:   21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    127481 |  134815   459903 |   44938  126593  8371222    66.1 | 20.892 % |
c |    127583 |  134815   459903 |   49431   22581  1453770    64.4 | 21.174 % |
c |    127734 |  134815   459903 |   54374   22732  1461037    64.3 | 21.174 % |
c |    127962 |  134815   459903 |   59812   22960  1468070    63.9 | 21.174 % |
c |    128299 |  134815   459903 |   65793   23297  1511837    64.9 | 21.174 % |
c |    128805 |  134788   459842 |   72373   23801  1523385    64.0 | 21.201 % |
c |    129565 |  134752   459750 |   79610   24508  1564010    63.8 | 21.232 % |
c |    130704 |  134752   459750 |   87571   25647  1617569    63.1 | 21.232 % |
c |    132415 |  134752   459750 |   96328   27358  2022487    73.9 | 21.232 % |
c |    134977 |  134736   459698 |  105961   29918  2096361    70.1 | 21.238 % |
c |    138823 |  134736   459698 |  116557   33764  2317105    68.6 | 21.238 % |
c |    144589 |  134334   458568 |  128213   39345  2898101    73.7 | 21.527 % |
c |    153239 |  133701   456516 |  141034   47905  3569542    74.5 | 21.800 % |
c |    166214 |  133384   455552 |  155138   60839  4622471    76.0 | 21.966 % |
c |    185675 |  133248   455084 |  170651   80281  6975445    86.9 | 22.022 % |
c ==============================================================================
c [1mFound solution: 1075313664[0m
c ---[   0]---> BDD-cost:   20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    192545 |  133244   455067 |   44414   87146  7908220    90.7 | 22.022 % |
c |    192645 |  133235   455036 |   48855   23368  1920749    82.2 | 22.033 % |
c |    192795 |  133235   455036 |   53740   23518  1925837    81.9 | 22.033 % |
c |    193021 |  133235   455036 |   59115   23744  1935700    81.5 | 22.033 % |
c |    193358 |  133235   455036 |   65026   24081  1960387    81.4 | 22.033 % |
c |    193865 |  133148   454840 |   71529   24585  1985755    80.8 | 22.113 % |
c |    194625 |  133148   454840 |   78682   25345  2088776    82.4 | 22.113 % |
c |    195764 |  133148   454840 |   86550   26484  2261862    85.4 | 22.113 % |
c |    197472 |  132865   453951 |   95205   28161  2443104    86.8 | 22.261 % |
c |    200034 |  132685   453325 |  104725   30694  2561486    83.5 | 22.319 % |
c |    203880 |  132408   452362 |  115198   34489  2833743    82.2 | 22.408 % |
c |    209647 |  132408   452362 |  126718   40256  3865213    96.0 | 22.408 % |
c |    218298 |  132347   452149 |  139390   48897  4313096    88.2 | 22.427 % |
c |    231272 |  131914   450986 |  153329   61813  6482040   104.9 | 22.780 % |
c |    250734 |  131392   449491 |  168662   81163 10001406   123.2 | 23.152 % |
c |    279929 |  131150   448748 |  185528  110034 13869512   126.0 | 23.311 % |
c |    323720 |  131029   448387 |  204081  153804 22205935   144.4 | 23.373 % |
c ==============================================================================
c [1mFound solution: 1075278336[0m
c ---[   0]---> BDD-cost:   20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    343532 |  131032   448378 |   43677  173611 25443597   146.6 | 23.373 % |
c |    343632 |  130839   447909 |   48044   26513  2165119    81.7 | 23.576 % |
c |    343784 |  130839   447909 |   52849   26665  2169624    81.4 | 23.576 % |
c |    344010 |  130839   447909 |   58134   26891  2174104    80.8 | 23.576 % |
c |    344348 |  130839   447909 |   63947   27229  2203521    80.9 | 23.576 % |
c |    344857 |  130813   447851 |   70342   27732  2211742    79.8 | 23.600 % |
c |    345617 |  130813   447851 |   77376   28492  2332919    81.9 | 23.600 % |
c |    346759 |  130813   447851 |   85114   29634  2380296    80.3 | 23.600 % |
c |    348467 |  130813   447851 |   93625   31342  2719032    86.8 | 23.600 % |
c |    351030 |  130693   447477 |  102988   33880  3064641    90.5 | 23.671 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 13934 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.97 0.91 2/54 13930
Raw data (stat): 13930 (runsolver) R 13929 24300 24299 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 783197616 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 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.0007 s]
Raw data (loadavg): 0.94 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0002 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0009 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0005 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0001 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+59.9997 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0044 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0049 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.97 0.91 1/53 13934
Raw data (stat): 13930 (minisat+_script) S 13929 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 783197616 2174976 226 4294967295 134512640 135087896 3221224544 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.89
CPU user time (s): 1228.91
CPU system time (s): 0.98485
CPU usage (%): 100.01
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####