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/MIPLIB/miplib/normalized-mps-v2-13-7-mod010.opb
MD5SUM	4f0cac14ed3568050c2c57bb69fdb664
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	6571
Optimality of the best value was proved	NO
Number of terms in the objective function	2655
Biggest coefficient in the objective function	266
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	489211
Number of bits of the sum of numbers in the objective function	19
Biggest number in a constraint	266
Number of bits of the biggest number in a constraint	9
Biggest sum of numbers in a constraint	489211
Number of bits of the biggest sum of numbers	19
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.78
Number of variables	2655
Total number of constraints	2801
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	2800
Number of constraints which are nor clauses,nor cardinality constraints	1
Minimum length of a constraint	1
Maximum length of a constraint	2655
Trace number 19076

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-04-21 17:46:56 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17043 boxname=wulflinc2 idbench=1311 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4f0cac14ed3568050c2c57bb69fdb664  /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-mod010.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-mod010.opb /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-mod010.opb
IDLAUNCH: 17043
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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:        904036 kB
Buffers:         19560 kB
Cached:          88228 kB
SwapCached:       3324 kB
Active:          39360 kB
Inactive:        73172 kB
HighTotal:      131008 kB
HighFree:        43960 kB
LowTotal:       903652 kB
LowFree:        860076 kB
SwapTotal:     2097136 kB
SwapFree:      2092928 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5108 kB
Slab:            12532 kB
Committed_AS:    71784 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 18:06:59 (client local time) WITH STATUS 0 IN 1200.33 SECONDS
stats: 17043 7 1200.33 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 291 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 289]---> BDD-cost:   67
c ---[ 287]---> BDD-cost:  113
c ---[ 285]---> BDD-cost:  181
c ---[ 283]---> BDD-cost:  115
c ---[ 281]---> BDD-cost:   69
c ---[ 279]---> BDD-cost:  125
c ---[ 277]---> BDD-cost:  155
c ---[ 275]---> BDD-cost:   87
c ---[ 273]---> BDD-cost:   97
c ---[ 271]---> BDD-cost:   73
c ---[ 269]---> BDD-cost:  119
c ---[ 267]---> BDD-cost:   45
c ---[ 265]---> BDD-cost:  171
c ---[ 263]---> BDD-cost:  111
c ---[ 261]---> BDD-cost:  149
c ---[ 259]---> BDD-cost:  195
c ---[ 257]---> BDD-cost:  131
c ---[ 255]---> BDD-cost:  123
c ---[ 253]---> BDD-cost:  167
c ---[ 251]---> BDD-cost:  101
c ---[ 249]---> BDD-cost:   97
c ---[ 247]---> BDD-cost:   23
c ---[ 245]---> BDD-cost:  135
c ---[ 243]---> BDD-cost:   59
c ---[ 241]---> BDD-cost:   95
c ---[ 239]---> BDD-cost:   59
c ---[ 237]---> BDD-cost:  133
c ---[ 235]---> BDD-cost:   99
c ---[ 233]---> BDD-cost:  179
c ---[ 231]---> BDD-cost:  111
c ---[ 229]---> BDD-cost:   23
c ---[ 227]---> BDD-cost:   89
c ---[ 225]---> BDD-cost:   95
c ---[ 223]---> BDD-cost:  117
c ---[ 221]---> BDD-cost:   23
c ---[ 219]---> BDD-cost:   51
c ---[ 217]---> BDD-cost:  311
c ---[ 215]---> BDD-cost:  259
c ---[ 213]---> BDD-cost:  169
c ---[ 211]---> BDD-cost:  131
c ---[ 209]---> BDD-cost:  155
c ---[ 207]---> BDD-cost:   89
c ---[ 205]---> BDD-cost:   51
c ---[ 203]---> BDD-cost:  165
c ---[ 201]---> BDD-cost:   75
c ---[ 199]---> BDD-cost:  139
c ---[ 197]---> BDD-cost:   67
c ---[ 195]---> BDD-cost:  173
c ---[ 193]---> BDD-cost:  235
c ---[ 191]---> BDD-cost:  185
c ---[ 189]---> BDD-cost:  127
c ---[ 187]---> BDD-cost:   37
c ---[ 185]---> BDD-cost:   37
c ---[ 183]---> BDD-cost:   91
c ---[ 181]---> BDD-cost:   77
c ---[ 179]---> BDD-cost:   29
c ---[ 177]---> BDD-cost:   77
c ---[ 175]---> BDD-cost:   77
c ---[ 173]---> BDD-cost:  101
c ---[ 171]---> BDD-cost:  131
c ---[ 169]---> BDD-cost:  155
c ---[ 167]---> BDD-cost:  177
c ---[ 165]---> BDD-cost:  143
c ---[ 163]---> BDD-cost:   93
c ---[ 161]---> BDD-cost:   79
c ---[ 159]---> BDD-cost:   53
c ---[ 157]---> BDD-cost:   71
c ---[ 155]---> BDD-cost:  127
c ---[ 153]---> BDD-cost:  127
c ---[ 151]---> BDD-cost:   67
c ---[ 149]---> BDD-cost:   83
c ---[ 147]---> BDD-cost:   47
c ---[ 145]---> BDD-cost:   63
c ---[ 143]---> BDD-cost:  121
c ---[ 141]---> BDD-cost:  155
c ---[ 139]---> BDD-cost:   87
c ---[ 137]---> BDD-cost:   91
c ---[ 135]---> BDD-cost:   47
c ---[ 133]---> BDD-cost:   67
c ---[ 131]---> BDD-cost:   33
c ---[ 129]---> BDD-cost:   91
c ---[ 127]---> BDD-cost:   69
c ---[ 125]---> BDD-cost:    5
c ---[ 123]---> BDD-cost:   47
c ---[ 121]---> BDD-cost:   45
c ---[ 119]---> BDD-cost:   37
c ---[ 117]---> BDD-cost:  117
c ---[ 115]---> BDD-cost:   97
c ---[ 113]---> BDD-cost:   77
c ---[ 111]---> BDD-cost:   97
c ---[ 109]---> BDD-cost:  137
c ---[ 107]---> BDD-cost:  125
c ---[ 105]---> BDD-cost:   79
c ---[ 103]---> BDD-cost:  133
c ---[ 101]---> BDD-cost:  153
c ---[  99]---> BDD-cost:  139
c ---[  97]---> BDD-cost:  125
c ---[  95]---> BDD-cost:    5
c ---[  93]---> BDD-cost:   73
c ---[  91]---> BDD-cost:  157
c ---[  89]---> BDD-cost:  127
c ---[  87]---> BDD-cost:  199
c ---[  85]---> BDD-cost:  121
c ---[  83]---> BDD-cost:  107
c ---[  81]---> BDD-cost:  169
c ---[  79]---> BDD-cost:  113
c ---[  77]---> BDD-cost:  103
c ---[  75]---> BDD-cost:   75
c ---[  73]---> BDD-cost:   97
c ---[  71]---> BDD-cost:  151
c ---[  69]---> BDD-cost:  199
c ---[  67]---> BDD-cost:  109
c ---[  65]---> BDD-cost:  131
c ---[  63]---> BDD-cost:  113
c ---[  61]---> BDD-cost:  173
c ---[  59]---> BDD-cost:  119
c ---[  57]---> BDD-cost:  173
c ---[  55]---> BDD-cost:  119
c ---[  53]---> BDD-cost:   71
c ---[  51]---> BDD-cost:  179
c ---[  49]---> BDD-cost:  241
c ---[  47]---> BDD-cost:  201
c ---[  45]---> BDD-cost:  173
c ---[  43]---> BDD-cost:  147
c ---[  41]---> BDD-cost:  157
c ---[  39]---> BDD-cost:  201
c ---[  37]---> BDD-cost:  129
c ---[  35]---> BDD-cost:  117
c ---[  33]---> BDD-cost:  177
c ---[  31]---> BDD-cost:  123
c ---[  29]---> BDD-cost:  131
c ---[  27]---> BDD-cost:  115
c ---[  25]---> BDD-cost:   51
c ---[  23]---> BDD-cost:  123
c ---[  21]---> BDD-cost:   55
c ---[  19]---> BDD-cost:    5
c ---[  17]---> BDD-cost:   99
c ---[  15]---> BDD-cost:   85
c ---[  13]---> BDD-cost:  109
c ---[  11]---> BDD-cost:  153
c ---[   9]---> BDD-cost:  201
c ---[   7]---> BDD-cost:  133
c ---[   5]---> BDD-cost:  121
c ---[   3]---> BDD-cost:  171
c ---[   1]---> Adder-cost: 5294   maxlim: 2609   bits: 12/12
c ---[   0]---> BDD-cost:  751
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  112641   342501 |   37547       0        0     nan |  0.000 % |
c |       100 |  112566   342248 |   41301      93      747     8.0 |  0.739 % |
c |       251 |  112566   342248 |   45431     244     4453    18.2 |  0.739 % |
c |       477 |  112566   342248 |   49975     470    15059    32.0 |  0.739 % |
c |       819 |  112566   342248 |   54972     812    37441    46.1 |  0.739 % |
c |      1331 |  112566   342248 |   60469    1324    71852    54.3 |  0.739 % |
c |      2095 |  112566   342248 |   66516    2088   201139    96.3 |  0.739 % |
c |      3235 |  112566   342248 |   73168    3228   326074   101.0 |  0.739 % |
c |      4943 |  112537   342164 |   80485    4914   477218    97.1 |  0.751 % |
c |      7505 |  112537   342164 |   88533    7476  1210959   162.0 |  0.751 % |
c |     11350 |  112537   342164 |   97387   11321  1873735   165.5 |  0.751 % |
c |     17116 |  112537   342164 |  107125   17087  3521450   206.1 |  0.751 % |
c |     25767 |  112512   342081 |  117838   25734  4545362   176.6 |  0.767 % |
c |     38741 |  112460   341924 |  129622   38597  6644314   172.1 |  0.783 % |
c |     58202 |  112449   341881 |  142584   58057 12905884   222.3 |  0.791 % |
c |     87396 |  112356   341607 |  156843   87217 24567040   281.7 |  0.823 % |
c |    131185 |  112327   341502 |  172527  131001 48087197   367.1 |  0.840 % |
#### 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.87 0.97 0.92 2/54 2307
Raw data (stat): 2307 (runsolver) R 2306 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488772973 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0009 s]
Raw data (loadavg): 0.89 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 5603 0 0 0 985 14 0 0 25 0 1 0 488772973 22962176 4934 4294967295 134512640 134672761 3221224544 3221223680 134565098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5606 4934 603 41 0 5565 0
vsize: 22424
[startup+20.0011 s]
Raw data (loadavg): 0.91 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 6120 0 0 0 1983 15 0 0 25 0 1 0 488772973 25116672 5451 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6132 5451 603 41 0 6091 0
vsize: 24528
[startup+30.0013 s]
Raw data (loadavg): 0.92 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 6681 0 0 0 2981 17 0 0 25 0 1 0 488772973 27410432 6012 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6692 6012 603 41 0 6651 0
vsize: 26768
[startup+40.002 s]
Raw data (loadavg): 0.93 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 7333 0 0 0 3979 19 0 0 25 0 1 0 488772973 30113792 6664 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7352 6664 603 41 0 7311 0
vsize: 29408
[startup+50.0022 s]
Raw data (loadavg): 0.94 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 8077 0 0 0 4977 22 0 0 25 0 1 0 488772973 33087488 7408 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8078 7408 603 41 0 8037 0
vsize: 32312
[startup+60.0036 s]
Raw data (loadavg): 0.95 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 8763 0 0 0 5975 24 0 0 25 0 1 0 488772973 35917824 8094 4294967295 134512640 134672761 3221224544 3221223728 134559590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8094 603 41 0 8728 0
vsize: 35076
[startup+70.0041 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 9403 0 0 0 6974 26 0 0 25 0 1 0 488772973 38637568 8734 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9433 8734 603 41 0 9392 0
vsize: 37732
[startup+80.0043 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 9880 0 0 0 7972 27 0 0 25 0 1 0 488772973 40521728 9211 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9893 9211 603 41 0 9852 0
vsize: 39572
[startup+90.0055 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 10289 0 0 0 8971 29 0 0 25 0 1 0 488772973 42266624 9620 4294967295 134512640 134672761 3221224544 3221223648 134559908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10319 9620 603 41 0 10278 0
vsize: 41276
[startup+100.006 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 10780 0 0 0 9969 30 0 0 25 0 1 0 488772973 44154880 10111 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10780 10111 603 41 0 10739 0
vsize: 43120
[startup+110.006 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 11331 0 0 0 10968 31 0 0 25 0 1 0 488772973 46444544 10662 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11339 10662 603 41 0 11298 0
vsize: 45356
[startup+120.008 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 11798 0 0 0 11967 33 0 0 25 0 1 0 488772973 48455680 11129 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11830 11129 603 41 0 11789 0
vsize: 47320
[startup+130.008 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 12358 0 0 0 12964 36 0 0 25 0 1 0 488772973 50737152 11689 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12387 11689 603 41 0 12346 0
vsize: 49548
[startup+140.008 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 12854 0 0 0 13963 37 0 0 25 0 1 0 488772973 52756480 12185 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12880 12185 603 41 0 12839 0
vsize: 51520
[startup+150.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 13543 0 0 0 14962 39 0 0 25 0 1 0 488772973 55611392 12874 4294967295 134512640 134672761 3221224544 3221223728 134558761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13577 12874 603 41 0 13536 0
vsize: 54308
[startup+160.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 14096 0 0 0 15960 41 0 0 25 0 1 0 488772973 57901056 13427 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14136 13427 603 41 0 14095 0
vsize: 56544
[startup+170.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 14691 0 0 0 16958 43 0 0 25 0 1 0 488772973 60301312 14022 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14722 14022 603 41 0 14681 0
vsize: 58888
[startup+180.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 15266 0 0 0 17956 45 0 0 25 0 1 0 488772973 62709760 14597 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15310 14597 603 41 0 15269 0
vsize: 61240
[startup+190.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 15959 0 0 0 18954 47 0 0 25 0 1 0 488772973 65523712 15290 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15997 15290 603 41 0 15956 0
vsize: 63988
[startup+200.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 16755 0 0 0 19952 49 0 0 25 0 1 0 488772973 68698112 16086 4294967295 134512640 134672761 3221224544 3221223648 134559993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16772 16086 603 41 0 16731 0
vsize: 67088
[startup+210.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 17378 0 0 0 20951 51 0 0 25 0 1 0 488772973 71258112 16709 4294967295 134512640 134672761 3221224544 3221223648 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17397 16709 603 41 0 17356 0
vsize: 69588
[startup+220.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 17996 0 0 0 21949 53 0 0 25 0 1 0 488772973 73814016 17327 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18021 17327 603 41 0 17980 0
vsize: 72084
[startup+230.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 18522 0 0 0 22947 55 0 0 25 0 1 0 488772973 75980800 17853 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18550 17853 603 41 0 18509 0
vsize: 74200
[startup+240.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 19001 0 0 0 23946 55 0 0 25 0 1 0 488772973 77869056 18332 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19011 18332 603 41 0 18970 0
vsize: 76044
[startup+250.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 19609 0 0 0 24945 57 0 0 25 0 1 0 488772973 80420864 18940 4294967295 134512640 134672761 3221224544 3221223728 134558756 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19634 18940 603 41 0 19593 0
vsize: 78536
[startup+260.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 20375 0 0 0 25943 59 0 0 25 0 1 0 488772973 83542016 19706 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20396 19706 603 41 0 20355 0
vsize: 81584
[startup+270.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 21142 0 0 0 26942 60 0 0 25 0 1 0 488772973 86626304 20473 4294967295 134512640 134672761 3221224544 3221223728 134558914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21149 20473 603 41 0 21108 0
vsize: 84596
[startup+280.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 21791 0 0 0 27941 61 0 0 25 0 1 0 488772973 89288704 21122 4294967295 134512640 134672761 3221224544 3221223712 134561266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21799 21122 603 41 0 21758 0
vsize: 87196
[startup+290.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 22617 0 0 0 28939 63 0 0 25 0 1 0 488772973 92934144 21948 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22689 21948 603 41 0 22648 0
vsize: 90756
[startup+300.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 23270 0 0 0 29938 65 0 0 25 0 1 0 488772973 95641600 22601 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23350 22601 603 41 0 23309 0
vsize: 93400
[startup+310.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 23823 0 0 0 30936 67 0 0 25 0 1 0 488772973 97910784 23154 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23904 23154 603 41 0 23863 0
vsize: 95616
[startup+320.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 24572 0 0 0 31934 69 0 0 25 0 1 0 488772973 100896768 23903 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24633 23903 603 41 0 24592 0
vsize: 98532
[startup+330.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 25336 0 0 0 32933 71 0 0 25 0 1 0 488772973 104013824 24667 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25394 24667 603 41 0 25353 0
vsize: 101576
[startup+340.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 25835 0 0 0 33931 72 0 0 25 0 1 0 488772973 106037248 25166 4294967295 134512640 134672761 3221224544 3221223648 134560293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25888 25166 603 41 0 25847 0
vsize: 103552
[startup+350.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 26486 0 0 0 34929 75 0 0 25 0 1 0 488772973 108724224 25817 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26544 25817 603 41 0 26503 0
vsize: 106176
[startup+360.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 26928 0 0 0 35928 76 0 0 25 0 1 0 488772973 110620672 26259 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27007 26259 603 41 0 26966 0
vsize: 108028
[startup+370.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 27520 0 0 0 36926 78 0 0 25 0 1 0 488772973 113045504 26851 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27599 26851 603 41 0 27558 0
vsize: 110396
[startup+380.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 27878 0 0 0 37925 79 0 0 25 0 1 0 488772973 114393088 27209 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27928 27209 603 41 0 27887 0
vsize: 111712
[startup+390.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 28370 0 0 0 38924 80 0 0 25 0 1 0 488772973 116416512 27701 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28422 27701 603 41 0 28381 0
vsize: 113688
[startup+400.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 29119 0 0 0 39922 82 0 0 25 0 1 0 488772973 119525376 28450 4294967295 134512640 134672761 3221224544 3221223648 134560128 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29181 28450 603 41 0 29140 0
vsize: 116724
[startup+410.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 29733 0 0 0 40921 84 0 0 25 0 1 0 488772973 122077184 29064 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29804 29064 603 41 0 29763 0
vsize: 119216
[startup+420.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 30478 0 0 0 41919 86 0 0 25 0 1 0 488772973 125067264 29809 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30534 29809 603 41 0 30493 0
vsize: 122136
[startup+430.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 31017 0 0 0 42916 88 0 0 25 0 1 0 488772973 127320064 30348 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31084 30348 603 41 0 31043 0
vsize: 124336
[startup+440.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 31579 0 0 0 43916 89 0 0 25 0 1 0 488772973 129499136 30910 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31616 30910 603 41 0 31575 0
vsize: 126464
[startup+450.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 32092 0 0 0 44914 91 0 0 25 0 1 0 488772973 131653632 31423 4294967295 134512640 134672761 3221224544 3221223696 134541817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32142 31423 603 41 0 32101 0
vsize: 128568
[startup+460.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 32347 0 0 0 45914 92 0 0 25 0 1 0 488772973 132734976 31678 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32406 31678 603 41 0 32365 0
vsize: 129624
[startup+470.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 32970 0 0 0 46913 93 0 0 25 0 1 0 488772973 135303168 32301 4294967295 134512640 134672761 3221224544 3221223648 134559908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33033 32301 603 41 0 32992 0
vsize: 132132
[startup+480.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 33535 0 0 0 47912 94 0 0 25 0 1 0 488772973 137580544 32866 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33589 32866 603 41 0 33548 0
vsize: 134356
[startup+490.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 34107 0 0 0 48911 95 0 0 25 0 1 0 488772973 139845632 33438 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34142 33438 603 41 0 34101 0
vsize: 136568
[startup+500.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 34715 0 0 0 49910 97 0 0 25 0 1 0 488772973 142401536 34046 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34766 34046 603 41 0 34725 0
vsize: 139064
[startup+510.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 35351 0 0 0 50907 99 0 0 25 0 1 0 488772973 144969728 34682 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35393 34682 603 41 0 35352 0
vsize: 141572
[startup+520.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 36058 0 0 0 51906 101 0 0 25 0 1 0 488772973 147804160 35389 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36085 35389 603 41 0 36044 0
vsize: 144340
[startup+530.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 36755 0 0 0 52904 103 0 0 25 0 1 0 488772973 150757376 36086 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36806 36086 603 41 0 36765 0
vsize: 147224
[startup+540.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 37371 0 0 0 53903 104 0 0 25 0 1 0 488772973 153251840 36702 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37415 36702 603 41 0 37374 0
vsize: 149660
[startup+550.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 37766 0 0 0 54901 106 0 0 25 0 1 0 488772973 154873856 37097 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37811 37097 603 41 0 37770 0
vsize: 151244
[startup+560.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 38308 0 0 0 55900 108 0 0 25 0 1 0 488772973 157032448 37639 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38338 37639 603 41 0 38297 0
vsize: 153352
[startup+570.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 38736 0 0 0 56899 109 0 0 25 0 1 0 488772973 158789632 38067 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38767 38067 603 41 0 38726 0
vsize: 155068
[startup+580.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 39179 0 0 0 57898 110 0 0 25 0 1 0 488772973 160669696 38510 4294967295 134512640 134672761 3221224544 3221223728 134559553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39226 38510 603 41 0 39185 0
vsize: 156904
[startup+590.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 39816 0 0 0 58896 112 0 0 25 0 1 0 488772973 163201024 39147 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39844 39147 603 41 0 39803 0
vsize: 159376
[startup+600.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 40438 0 0 0 59895 113 0 0 25 0 1 0 488772973 165740544 39769 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40464 39769 603 41 0 40423 0
vsize: 161856
[startup+610.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 41035 0 0 0 60894 115 0 0 25 0 1 0 488772973 168153088 40366 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41053 40366 603 41 0 41012 0
vsize: 164212
[startup+620.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 41679 0 0 0 61892 117 0 0 25 0 1 0 488772973 170831872 41010 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41707 41010 603 41 0 41666 0
vsize: 166828
[startup+630.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 42248 0 0 0 62891 118 0 0 25 0 1 0 488772973 173105152 41579 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42262 41579 603 41 0 42221 0
vsize: 169048
[startup+640.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 42807 0 0 0 63889 120 0 0 25 0 1 0 488772973 175509504 42138 4294967295 134512640 134672761 3221224544 3221223648 134560335 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42849 42139 603 41 0 42808 0
vsize: 171396
[startup+650.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 43536 0 0 0 64888 122 0 0 25 0 1 0 488772973 178470912 42867 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43572 42867 603 41 0 43531 0
vsize: 174288
[startup+660.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 44250 0 0 0 65887 123 0 0 25 0 1 0 488772973 181305344 43581 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44264 43581 603 41 0 44223 0
vsize: 177056
[startup+670.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 44952 0 0 0 66885 125 0 0 25 0 1 0 488772973 184258560 44283 4294967295 134512640 134672761 3221224544 3221223728 134559363 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44985 44283 603 41 0 44944 0
vsize: 179940
[startup+680.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 45623 0 0 0 67884 126 0 0 25 0 1 0 488772973 186978304 44954 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45649 44954 603 41 0 45608 0
vsize: 182596
[startup+690.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 46274 0 0 0 68882 128 0 0 25 0 1 0 488772973 189681664 45605 4294967295 134512640 134672761 3221224544 3221223648 134559883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46309 45605 603 41 0 46268 0
vsize: 185236
[startup+700.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 46906 0 0 0 69880 130 0 0 25 0 1 0 488772973 192233472 46237 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46932 46237 603 41 0 46891 0
vsize: 187728
[startup+710.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 47502 0 0 0 70879 132 0 0 25 0 1 0 488772973 194662400 46833 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47525 46833 603 41 0 47484 0
vsize: 190100
[startup+720.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 48118 0 0 0 71877 133 0 0 25 0 1 0 488772973 197222400 47449 4294967295 134512640 134672761 3221224544 3221223728 134559581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48150 47449 603 41 0 48109 0
vsize: 192600
[startup+730.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 48752 0 0 0 72877 134 0 0 25 0 1 0 488772973 199790592 48083 4294967295 134512640 134672761 3221224544 3221223648 134559995 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48777 48083 603 41 0 48736 0
vsize: 195108
[startup+740.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 49401 0 0 0 73876 136 0 0 25 0 1 0 488772973 202375168 48732 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49408 48732 603 41 0 49367 0
vsize: 197632
[startup+750.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 49997 0 0 0 74874 138 0 0 25 0 1 0 488772973 204931072 49328 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50032 49328 603 41 0 49991 0
vsize: 200128
[startup+760.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 50623 0 0 0 75872 139 0 0 25 0 1 0 488772973 207511552 49954 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50662 49954 603 41 0 50621 0
vsize: 202648
[startup+770.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 51222 0 0 0 76871 141 0 0 25 0 1 0 488772973 209948672 50553 4294967295 134512640 134672761 3221224544 3221223648 134560520 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51257 50553 603 41 0 51216 0
vsize: 205028
[startup+780.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2307
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 51836 0 0 0 77869 143 0 0 25 0 1 0 488772973 212492288 51167 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51878 51167 603 41 0 51837 0
vsize: 207512
[startup+790.025 s]
Raw data (loadavg): 0.99 0.97 0.92 3/57 2356
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 52413 0 0 0 78868 144 0 0 25 0 1 0 488772973 214781952 51744 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52437 51744 603 41 0 52396 0
vsize: 209748
[startup+800.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2360
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 53010 0 0 0 79866 146 0 0 25 0 1 0 488772973 217231360 52341 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53035 52341 603 41 0 52994 0
vsize: 212140
[startup+810.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2360
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 53613 0 0 0 80864 148 0 0 25 0 1 0 488772973 219648000 52944 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53625 52944 603 41 0 53584 0
vsize: 214500
[startup+820.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2360
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 54204 0 0 0 81863 149 0 0 25 0 1 0 488772973 222081024 53535 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54219 53535 603 41 0 54178 0
vsize: 216876
[startup+830.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2360
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 54812 0 0 0 82862 151 0 0 25 0 1 0 488772973 225136640 54143 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54965 54143 603 41 0 54924 0
vsize: 219860
[startup+840.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2360
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 55481 0 0 0 83860 152 0 0 25 0 1 0 488772973 227930112 54812 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55647 54812 603 41 0 55606 0
vsize: 222588
[startup+850.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2360
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 55835 0 0 0 84859 154 0 0 25 0 1 0 488772973 229285888 55166 4294967295 134512640 134672761 3221224544 3221223712 134564457 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55978 55166 603 41 0 55937 0
vsize: 223912
[startup+860.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2362
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 56223 0 0 0 85858 155 0 0 25 0 1 0 488772973 230875136 55554 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56366 55554 603 41 0 56325 0
vsize: 225464
[startup+870.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2362
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 56469 0 0 0 86857 156 0 0 25 0 1 0 488772973 231952384 55800 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56629 55800 603 41 0 56588 0
vsize: 226516
[startup+880.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2362
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 57014 0 0 0 87856 157 0 0 25 0 1 0 488772973 234106880 56345 4294967295 134512640 134672761 3221224544 3221223648 134559985 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57155 56345 603 41 0 57114 0
vsize: 228620
[startup+890.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2362
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 57672 0 0 0 88854 159 0 0 25 0 1 0 488772973 236789760 57003 4294967295 134512640 134672761 3221224544 3221223728 134559503 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57810 57003 603 41 0 57769 0
vsize: 231240
[startup+900.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2362
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 58368 0 0 0 89852 161 0 0 25 0 1 0 488772973 239632384 57699 4294967295 134512640 134672761 3221224544 3221223648 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58504 57699 603 41 0 58463 0
vsize: 234016
[startup+910.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2362
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 58764 0 0 0 90851 163 0 0 25 0 1 0 488772973 241258496 58095 4294967295 134512640 134672761 3221224544 3221223648 134560036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58901 58095 603 41 0 58860 0
vsize: 235604
[startup+920.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2362
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 59073 0 0 0 91850 164 0 0 25 0 1 0 488772973 242601984 58404 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59229 58404 603 41 0 59188 0
vsize: 236916
[startup+930.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2362
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 59351 0 0 0 92849 165 0 0 25 0 1 0 488772973 243679232 58682 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59492 58682 603 41 0 59451 0
vsize: 237968
[startup+940.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2362
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 59625 0 0 0 93848 166 0 0 25 0 1 0 488772973 244764672 58956 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59757 58956 603 41 0 59716 0
vsize: 239028
[startup+950.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2362
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 60179 0 0 0 94846 168 0 0 25 0 1 0 488772973 247070720 59510 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60320 59510 603 41 0 60279 0
vsize: 241280
[startup+960.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2362
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 60517 0 0 0 95845 169 0 0 25 0 1 0 488772973 248422400 59848 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60650 59848 603 41 0 60609 0
vsize: 242600
[startup+970.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2362
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 61020 0 0 0 96843 171 0 0 25 0 1 0 488772973 250441728 60351 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61143 60351 603 41 0 61102 0
vsize: 244572
[startup+980.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2362
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 61639 0 0 0 97842 173 0 0 25 0 1 0 488772973 252989440 60970 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61765 60970 603 41 0 61724 0
vsize: 247060
[startup+990.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2362
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 62229 0 0 0 98841 175 0 0 25 0 1 0 488772973 255422464 61560 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62359 61560 603 41 0 62318 0
vsize: 249436
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2362
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 62619 0 0 0 99840 176 0 0 25 0 1 0 488772973 257036288 61950 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62753 61950 603 41 0 62712 0
vsize: 251012
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2362
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 63015 0 0 0 100838 177 0 0 25 0 1 0 488772973 258658304 62346 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63149 62346 603 41 0 63108 0
vsize: 252596
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2362
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 63386 0 0 0 101837 179 0 0 25 0 1 0 488772973 260132864 62717 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63509 62717 603 41 0 63468 0
vsize: 254036
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2362
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 63971 0 0 0 102836 180 0 0 25 0 1 0 488772973 262610944 63302 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64114 63302 603 41 0 64073 0
vsize: 256456
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2362
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 64565 0 0 0 103834 182 0 0 25 0 1 0 488772973 265019392 63896 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64702 63896 603 41 0 64661 0
vsize: 258808
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2362
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 65119 0 0 0 104832 184 0 0 25 0 1 0 488772973 267243520 64450 4294967295 134512640 134672761 3221224544 3221223648 134559890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65245 64450 603 41 0 65204 0
vsize: 260980
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2362
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 65682 0 0 0 105831 186 0 0 25 0 1 0 488772973 269496320 65013 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65795 65013 603 41 0 65754 0
vsize: 263180
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2362
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 65855 0 0 0 106830 186 0 0 25 0 1 0 488772973 270303232 65186 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65992 65186 603 41 0 65951 0
vsize: 263968
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2362
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 66107 0 0 0 107830 187 0 0 25 0 1 0 488772973 271241216 65438 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66221 65438 603 41 0 66180 0
vsize: 264884
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2362
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 66618 0 0 0 108829 188 0 0 25 0 1 0 488772973 273403904 65949 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66749 65949 603 41 0 66708 0
vsize: 266996
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2362
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 67160 0 0 0 109827 190 0 0 25 0 1 0 488772973 275554304 66491 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67274 66491 603 41 0 67233 0
vsize: 269096
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2362
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 67639 0 0 0 110825 192 0 0 25 0 1 0 488772973 277573632 66970 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67767 66970 603 41 0 67726 0
vsize: 271068
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2362
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 68114 0 0 0 111823 194 0 0 25 0 1 0 488772973 279465984 67445 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68229 67445 603 41 0 68188 0
vsize: 272916
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2364
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 68463 0 0 0 112822 196 0 0 25 0 1 0 488772973 280948736 67794 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68591 67794 603 41 0 68550 0
vsize: 274364
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2364
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 68954 0 0 0 113820 197 0 0 25 0 1 0 488772973 282959872 68285 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69082 68285 603 41 0 69041 0
vsize: 276328
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2364
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 69454 0 0 0 114819 199 0 0 25 0 1 0 488772973 284958720 68785 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69570 68785 603 41 0 69529 0
vsize: 278280
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2364
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 69965 0 0 0 115818 200 0 0 25 0 1 0 488772973 287092736 69296 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70091 69296 603 41 0 70050 0
vsize: 280364
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2364
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 70349 0 0 0 116817 201 0 0 25 0 1 0 488772973 288710656 69680 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70486 69680 603 41 0 70445 0
vsize: 281944
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2364
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 70723 0 0 0 117815 203 0 0 25 0 1 0 488772973 290193408 70054 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70848 70054 603 41 0 70807 0
vsize: 283392
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2364
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 70931 0 0 0 118815 204 0 0 25 0 1 0 488772973 291000320 70262 4294967295 134512640 134672761 3221224544 3221223668 134566011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71045 70262 603 41 0 71004 0
vsize: 284180
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2364
Raw data (stat): 2307 (minisat+) R 2306 20937 20936 0 -1 0 71239 0 0 0 119814 205 0 0 25 0 1 0 488772973 292212736 70570 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71341 70570 603 41 0 71300 0
vsize: 285364
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.16 s]
Raw data (loadavg): 0.99 0.97 0.92 1/54 2364
Raw data (stat): 2307 (minisat+) Z 2306 20937 20936 0 -1 12 71241 0 0 0 119814 218 0 0 25 0 1 0 488772973 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.16
CPU time (s): 1200.33
CPU user time (s): 1198.14
CPU system time (s): 2.18567
CPU usage (%): 100.015
Max. virtual memory (Kb): 285364
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####