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/miplib3/normalized-mps-v2-20-10-mod010.opb
MD5SUM	ef7064a9be2b712276f7b600af28e2b0
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	1176.54
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 21191

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-04-21 23:03:30 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13650 boxname=wulflinc11 idbench=1050 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ef7064a9be2b712276f7b600af28e2b0  /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-mod010.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-mod010.opb /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-mod010.opb
IDLAUNCH: 13650
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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.028
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:        414440 kB
Buffers:         35684 kB
Cached:         562852 kB
SwapCached:          0 kB
Active:         254032 kB
Inactive:       347204 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        414188 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6820 kB
Slab:            13196 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 23:23:33 (client local time) WITH STATUS 0 IN 1200.29 SECONDS
stats: 13650 7 1200.29 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.85 0.94 0.90 2/54 13137
Raw data (stat): 13137 (runsolver) R 13136 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 490668054 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0011 s]
Raw data (loadavg): 0.88 0.94 0.90 2/54 13137
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 5613 0 0 0 985 14 0 0 25 0 1 0 490668054 23097344 4944 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5639 4944 603 41 0 5598 0
vsize: 22556
[startup+20.0024 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 13137
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 6136 0 0 0 1983 15 0 0 25 0 1 0 490668054 25251840 5467 4294967295 134512640 134672761 3221224544 3221223648 134559890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6165 5467 603 41 0 6124 0
vsize: 24660
[startup+30.0109 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 13137
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 6703 0 0 0 2982 17 0 0 25 0 1 0 490668054 27545600 6034 4294967295 134512640 134672761 3221224544 3221223648 134559927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6725 6034 603 41 0 6684 0
vsize: 26900
[startup+40.011 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 13137
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 7357 0 0 0 3980 18 0 0 25 0 1 0 490668054 30248960 6688 4294967295 134512640 134672761 3221224544 3221223668 134566098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7385 6688 603 41 0 7344 0
vsize: 29540
[startup+50.0117 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 13137
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 8133 0 0 0 4978 21 0 0 25 0 1 0 490668054 33349632 7464 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8142 7464 603 41 0 8101 0
vsize: 32568
[startup+60.012 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 13137
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 8814 0 0 0 5976 23 0 0 25 0 1 0 490668054 36188160 8145 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8835 8145 603 41 0 8794 0
vsize: 35340
[startup+70.0128 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 13137
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 9449 0 0 0 6974 25 0 0 25 0 1 0 490668054 38772736 8780 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9466 8780 603 41 0 9425 0
vsize: 37864
[startup+80.0131 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 13137
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 9912 0 0 0 7973 27 0 0 25 0 1 0 490668054 40652800 9243 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9925 9243 603 41 0 9884 0
vsize: 39700
[startup+90.0134 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 13137
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 10327 0 0 0 8972 28 0 0 25 0 1 0 490668054 42401792 9658 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10352 9658 603 41 0 10311 0
vsize: 41408
[startup+100.014 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 13137
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 10884 0 0 0 9970 30 0 0 25 0 1 0 490668054 44695552 10215 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10912 10215 603 41 0 10871 0
vsize: 43648
[startup+110.014 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 13137
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 11382 0 0 0 10969 31 0 0 25 0 1 0 490668054 46714880 10713 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11405 10713 603 41 0 11364 0
vsize: 45620
[startup+120.016 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 13137
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 11872 0 0 0 11967 33 0 0 25 0 1 0 490668054 48857088 11203 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11928 11203 603 41 0 11887 0
vsize: 47712
[startup+130.016 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 12425 0 0 0 12965 35 0 0 25 0 1 0 490668054 51007488 11756 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12453 11756 603 41 0 12412 0
vsize: 49812
[startup+140.016 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 12980 0 0 0 13963 37 0 0 25 0 1 0 490668054 53305344 12311 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13014 12311 603 41 0 12973 0
vsize: 52056
[startup+150.017 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 13666 0 0 0 14963 38 0 0 25 0 1 0 490668054 56152064 12997 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13709 12997 603 41 0 13668 0
vsize: 54836
[startup+160.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 14242 0 0 0 15960 40 0 0 25 0 1 0 490668054 58445824 13573 4294967295 134512640 134672761 3221224544 3221223648 134560492 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14269 13573 603 41 0 14228 0
vsize: 57076
[startup+170.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 14814 0 0 0 16959 42 0 0 25 0 1 0 490668054 60829696 14145 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14851 14145 603 41 0 14810 0
vsize: 59404
[startup+180.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 15373 0 0 0 17957 44 0 0 25 0 1 0 490668054 63111168 14704 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15408 14704 603 41 0 15367 0
vsize: 61632
[startup+190.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 16130 0 0 0 18954 46 0 0 25 0 1 0 490668054 66183168 15461 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16158 15461 603 41 0 16117 0
vsize: 64632
[startup+200.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 16909 0 0 0 19952 49 0 0 25 0 1 0 490668054 69369856 16240 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16936 16240 603 41 0 16895 0
vsize: 67744
[startup+210.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 17530 0 0 0 20950 51 0 0 25 0 1 0 490668054 71929856 16861 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17561 16861 603 41 0 17520 0
vsize: 70244
[startup+220.022 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 18103 0 0 0 21949 52 0 0 25 0 1 0 490668054 74215424 17434 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18119 17434 603 41 0 18078 0
vsize: 72476
[startup+230.022 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 18669 0 0 0 22947 54 0 0 25 0 1 0 490668054 76517376 18000 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18681 18000 603 41 0 18640 0
vsize: 74724
[startup+240.022 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 19102 0 0 0 23946 56 0 0 25 0 1 0 490668054 78270464 18433 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19109 18433 603 41 0 19068 0
vsize: 76436
[startup+250.023 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 19775 0 0 0 24944 57 0 0 25 0 1 0 490668054 81096704 19106 4294967295 134512640 134672761 3221224544 3221223648 134559853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19799 19106 603 41 0 19758 0
vsize: 79196
[startup+260.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 20565 0 0 0 25942 59 0 0 25 0 1 0 490668054 84357120 19896 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20595 19896 603 41 0 20554 0
vsize: 82380
[startup+270.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 21353 0 0 0 26941 61 0 0 25 0 1 0 490668054 87539712 20684 4294967295 134512640 134672761 3221224544 3221223648 134560034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21372 20684 603 41 0 21331 0
vsize: 85488
[startup+280.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 22029 0 0 0 27940 62 0 0 25 0 1 0 490668054 90247168 21360 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22033 21360 603 41 0 21992 0
vsize: 88132
[startup+290.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 22798 0 0 0 28939 64 0 0 25 0 1 0 490668054 93745152 22129 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22887 22129 603 41 0 22846 0
vsize: 91548
[startup+300.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 23494 0 0 0 29937 66 0 0 25 0 1 0 490668054 96583680 22825 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23580 22825 603 41 0 23539 0
vsize: 94320
[startup+310.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 24048 0 0 0 30935 67 0 0 25 0 1 0 490668054 98852864 23379 4294967295 134512640 134672761 3221224544 3221223648 134560373 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24134 23379 603 41 0 24093 0
vsize: 96536
[startup+320.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 24830 0 0 0 31934 69 0 0 25 0 1 0 490668054 101982208 24161 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24898 24161 603 41 0 24857 0
vsize: 99592
[startup+330.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 25458 0 0 0 32933 70 0 0 25 0 1 0 490668054 104554496 24789 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25526 24789 603 41 0 25485 0
vsize: 102104
[startup+340.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 26076 0 0 0 33932 72 0 0 25 0 1 0 490668054 107106304 25407 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26149 25407 603 41 0 26108 0
vsize: 104596
[startup+350.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 26621 0 0 0 34930 73 0 0 25 0 1 0 490668054 109264896 25952 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26676 25952 603 41 0 26635 0
vsize: 106704
[startup+360.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 27163 0 0 0 35930 73 0 0 25 0 1 0 490668054 111566848 26494 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27238 26494 603 41 0 27197 0
vsize: 108952
[startup+370.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 27665 0 0 0 36929 74 0 0 25 0 1 0 490668054 113586176 26996 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27731 26996 603 41 0 27690 0
vsize: 110924
[startup+380.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 28071 0 0 0 37928 76 0 0 25 0 1 0 490668054 115204096 27402 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28126 27402 603 41 0 28085 0
vsize: 112504
[startup+390.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 28717 0 0 0 38926 78 0 0 25 0 1 0 490668054 117907456 28048 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28786 28048 603 41 0 28745 0
vsize: 115144
[startup+400.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 29439 0 0 0 39924 80 0 0 25 0 1 0 490668054 120872960 28770 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29510 28770 603 41 0 29469 0
vsize: 118040
[startup+410.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 30102 0 0 0 40922 82 0 0 25 0 1 0 490668054 123564032 29433 4294967295 134512640 134672761 3221224544 3221223648 134560148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30167 29433 603 41 0 30126 0
vsize: 120668
[startup+420.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 30764 0 0 0 41921 84 0 0 25 0 1 0 490668054 126246912 30095 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30822 30095 603 41 0 30781 0
vsize: 123288
[startup+430.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 31239 0 0 0 42919 85 0 0 25 0 1 0 490668054 128135168 30570 4294967295 134512640 134672761 3221224544 3221223800 134562229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31283 30570 603 41 0 31242 0
vsize: 125132
[startup+440.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 31937 0 0 0 43917 88 0 0 25 0 1 0 490668054 130973696 31268 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31976 31268 603 41 0 31935 0
vsize: 127904
[startup+450.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 32209 0 0 0 44916 89 0 0 25 0 1 0 490668054 132194304 31540 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32274 31540 603 41 0 32233 0
vsize: 129096
[startup+460.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 32688 0 0 0 45915 90 0 0 25 0 1 0 490668054 134082560 32019 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32735 32019 603 41 0 32694 0
vsize: 130940
[startup+470.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 33296 0 0 0 46914 91 0 0 25 0 1 0 490668054 136503296 32627 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33326 32627 603 41 0 33285 0
vsize: 133304
[startup+480.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 33879 0 0 0 47912 93 0 0 25 0 1 0 490668054 138919936 33210 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33916 33210 603 41 0 33875 0
vsize: 135664
[startup+490.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 34486 0 0 0 48910 95 0 0 25 0 1 0 490668054 141463552 33817 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34537 33817 603 41 0 34496 0
vsize: 138148
[startup+500.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 35066 0 0 0 49910 96 0 0 25 0 1 0 490668054 143757312 34397 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35097 34397 603 41 0 35056 0
vsize: 140388
[startup+510.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 35829 0 0 0 50908 98 0 0 25 0 1 0 490668054 146862080 35160 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35855 35160 603 41 0 35814 0
vsize: 143420
[startup+520.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 36493 0 0 0 51906 100 0 0 25 0 1 0 490668054 149696512 35824 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36547 35824 603 41 0 36506 0
vsize: 146188
[startup+530.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 37183 0 0 0 52905 101 0 0 25 0 1 0 490668054 152465408 36514 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37223 36514 603 41 0 37182 0
vsize: 148892
[startup+540.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 37642 0 0 0 53904 102 0 0 25 0 1 0 490668054 154333184 36973 4294967295 134512640 134672761 3221224544 3221223648 134560250 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37679 36973 603 41 0 37638 0
vsize: 150716
[startup+550.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 38106 0 0 0 54904 103 0 0 25 0 1 0 490668054 156217344 37437 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38139 37437 603 41 0 38098 0
vsize: 152556
[startup+560.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 38582 0 0 0 55903 104 0 0 25 0 1 0 490668054 158109696 37913 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38601 37913 603 41 0 38560 0
vsize: 154404
[startup+570.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 38964 0 0 0 56902 105 0 0 25 0 1 0 490668054 159735808 38295 4294967295 134512640 134672761 3221224544 3221223648 134560051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38998 38295 603 41 0 38957 0
vsize: 155992
[startup+580.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 39615 0 0 0 57900 107 0 0 25 0 1 0 490668054 162394112 38946 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39647 38946 603 41 0 39606 0
vsize: 158588
[startup+590.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 40232 0 0 0 58899 109 0 0 25 0 1 0 490668054 164945920 39563 4294967295 134512640 134672761 3221224544 3221223648 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40270 39563 603 41 0 40229 0
vsize: 161080
[startup+600.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 40835 0 0 0 59897 110 0 0 25 0 1 0 490668054 167358464 40166 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40859 40166 603 41 0 40818 0
vsize: 163436
[startup+610.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 41481 0 0 0 60896 111 0 0 25 0 1 0 490668054 170020864 40812 4294967295 134512640 134672761 3221224544 3221223648 134559841 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41509 40812 603 41 0 41468 0
vsize: 166036
[startup+620.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 42099 0 0 0 61895 113 0 0 25 0 1 0 490668054 172564480 41430 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42130 41430 603 41 0 42089 0
vsize: 168520
[startup+630.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 42614 0 0 0 62894 114 0 0 25 0 1 0 490668054 174702592 41945 4294967295 134512640 134672761 3221224544 3221223648 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42652 41945 603 41 0 42611 0
vsize: 170608
[startup+640.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 43330 0 0 0 63892 117 0 0 25 0 1 0 490668054 177532928 42661 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43343 42661 603 41 0 43302 0
vsize: 173372
[startup+650.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 44049 0 0 0 64890 119 0 0 25 0 1 0 490668054 180498432 43380 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44067 43380 603 41 0 44026 0
vsize: 176268
[startup+660.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 44766 0 0 0 65888 121 0 0 25 0 1 0 490668054 183451648 44097 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44788 44097 603 41 0 44747 0
vsize: 179152
[startup+670.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 45441 0 0 0 66886 122 0 0 25 0 1 0 490668054 186171392 44772 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45452 44772 603 41 0 45411 0
vsize: 181808
[startup+680.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 46098 0 0 0 67885 124 0 0 25 0 1 0 490668054 188878848 45429 4294967295 134512640 134672761 3221224544 3221223648 134560287 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46113 45429 603 41 0 46072 0
vsize: 184452
[startup+690.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 46737 0 0 0 68884 125 0 0 25 0 1 0 490668054 191553536 46068 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46766 46068 603 41 0 46725 0
vsize: 187064
[startup+700.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 47341 0 0 0 69883 127 0 0 25 0 1 0 490668054 193986560 46672 4294967295 134512640 134672761 3221224544 3221223648 134559883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47360 46672 603 41 0 47319 0
vsize: 189440
[startup+710.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 47956 0 0 0 70882 128 0 0 25 0 1 0 490668054 196554752 47287 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47987 47287 603 41 0 47946 0
vsize: 191948
[startup+720.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 48588 0 0 0 71881 129 0 0 25 0 1 0 490668054 199114752 47919 4294967295 134512640 134672761 3221224544 3221223648 134560237 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48612 47919 603 41 0 48571 0
vsize: 194448
[startup+730.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 49234 0 0 0 72879 131 0 0 25 0 1 0 490668054 201695232 48565 4294967295 134512640 134672761 3221224544 3221223728 134559548 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49242 48565 603 41 0 49201 0
vsize: 196968
[startup+740.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 49850 0 0 0 73878 133 0 0 25 0 1 0 490668054 204275712 49181 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49872 49181 603 41 0 49831 0
vsize: 199488
[startup+750.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 50471 0 0 0 74877 134 0 0 25 0 1 0 490668054 206827520 49802 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50495 49802 603 41 0 50454 0
vsize: 201980
[startup+760.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 51075 0 0 0 75876 135 0 0 25 0 1 0 490668054 209272832 50406 4294967295 134512640 134672761 3221224544 3221223648 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51092 50406 603 41 0 51051 0
vsize: 204368
[startup+770.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 51675 0 0 0 76875 136 0 0 25 0 1 0 490668054 211816448 51006 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51713 51006 603 41 0 51672 0
vsize: 206852
[startup+780.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 52277 0 0 0 77873 138 0 0 25 0 1 0 490668054 214241280 51608 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52305 51608 603 41 0 52264 0
vsize: 209220
[startup+790.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 52869 0 0 0 78871 140 0 0 25 0 1 0 490668054 216686592 52200 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52902 52200 603 41 0 52861 0
vsize: 211608
[startup+800.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 53478 0 0 0 79870 141 0 0 25 0 1 0 490668054 219107328 52809 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53493 52809 603 41 0 53452 0
vsize: 213972
[startup+810.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 54079 0 0 0 80869 143 0 0 25 0 1 0 490668054 221675520 53410 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54120 53410 603 41 0 54079 0
vsize: 216480
[startup+820.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 54652 0 0 0 81866 145 0 0 25 0 1 0 490668054 224489472 53983 4294967295 134512640 134672761 3221224544 3221223648 134555225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54807 53983 603 41 0 54766 0
vsize: 219228
[startup+830.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 55383 0 0 0 82863 147 0 0 25 0 1 0 490668054 227405824 54714 4294967295 134512640 134672761 3221224544 3221223728 134559332 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55519 54714 603 41 0 55478 0
vsize: 222076
[startup+840.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 55796 0 0 0 83861 148 0 0 25 0 1 0 490668054 229150720 55127 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55945 55127 603 41 0 55904 0
vsize: 223780
[startup+850.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 56158 0 0 0 84860 150 0 0 25 0 1 0 490668054 230612992 55489 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56302 55489 603 41 0 56261 0
vsize: 225208
[startup+860.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 56387 0 0 0 85860 151 0 0 25 0 1 0 490668054 231550976 55718 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56531 55718 603 41 0 56490 0
vsize: 226124
[startup+870.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 56916 0 0 0 86859 152 0 0 25 0 1 0 490668054 233701376 56247 4294967295 134512640 134672761 3221224544 3221223712 134561266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57056 56247 603 41 0 57015 0
vsize: 228224
[startup+880.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 57568 0 0 0 87856 154 0 0 25 0 1 0 490668054 236388352 56899 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57712 56899 603 41 0 57671 0
vsize: 230848
[startup+890.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 58290 0 0 0 88854 155 0 0 25 0 1 0 490668054 239353856 57621 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58436 57621 603 41 0 58395 0
vsize: 233744
[startup+900.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 58707 0 0 0 89852 157 0 0 25 0 1 0 490668054 240988160 58038 4294967295 134512640 134672761 3221224544 3221223648 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58835 58038 603 41 0 58794 0
vsize: 235340
[startup+910.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 59003 0 0 0 90852 158 0 0 25 0 1 0 490668054 242192384 58334 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59129 58334 603 41 0 59088 0
vsize: 236516
[startup+920.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 59351 0 0 0 91851 159 0 0 25 0 1 0 490668054 243679232 58682 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59492 58682 603 41 0 59451 0
vsize: 237968
[startup+930.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 59568 0 0 0 92850 159 0 0 25 0 1 0 490668054 244625408 58899 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59723 58899 603 41 0 59682 0
vsize: 238892
[startup+940.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 60138 0 0 0 93849 161 0 0 25 0 1 0 490668054 246939648 59469 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60288 59469 603 41 0 60247 0
vsize: 241152
[startup+950.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 60472 0 0 0 94849 161 0 0 25 0 1 0 490668054 248295424 59803 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60619 59803 603 41 0 60578 0
vsize: 242476
[startup+960.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 60958 0 0 0 95848 163 0 0 25 0 1 0 490668054 250306560 60289 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61110 60289 603 41 0 61069 0
vsize: 244440
[startup+970.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 61580 0 0 0 96846 165 0 0 25 0 1 0 490668054 252854272 60911 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61732 60912 603 41 0 61691 0
vsize: 246928
[startup+980.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 62197 0 0 0 97845 166 0 0 25 0 1 0 490668054 255287296 61528 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62326 61528 603 41 0 62285 0
vsize: 249304
[startup+990.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 62591 0 0 0 98845 166 0 0 25 0 1 0 490668054 256901120 61922 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62720 61922 603 41 0 62679 0
vsize: 250880
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 62996 0 0 0 99844 167 0 0 25 0 1 0 490668054 258523136 62327 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63116 62327 603 41 0 63075 0
vsize: 252464
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 63367 0 0 0 100843 168 0 0 25 0 1 0 490668054 260132864 62698 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63509 62698 603 41 0 63468 0
vsize: 254036
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 63946 0 0 0 101841 170 0 0 25 0 1 0 490668054 262475776 63277 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64081 63277 603 41 0 64040 0
vsize: 256324
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 64536 0 0 0 102840 172 0 0 25 0 1 0 490668054 264884224 63867 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64669 63867 603 41 0 64628 0
vsize: 258676
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 65094 0 0 0 103839 173 0 0 25 0 1 0 490668054 267108352 64425 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65212 64425 603 41 0 65171 0
vsize: 260848
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 65667 0 0 0 104837 175 0 0 25 0 1 0 490668054 269496320 64998 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65795 64998 603 41 0 65754 0
vsize: 263180
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 65855 0 0 0 105837 175 0 0 25 0 1 0 490668054 270303232 65186 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65992 65186 603 41 0 65951 0
vsize: 263968
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 66094 0 0 0 106837 176 0 0 25 0 1 0 490668054 271241216 65425 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66221 65425 603 41 0 66180 0
vsize: 264884
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 66603 0 0 0 107835 178 0 0 25 0 1 0 490668054 273272832 65934 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66717 65934 603 41 0 66676 0
vsize: 266868
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 67151 0 0 0 108834 179 0 0 25 0 1 0 490668054 275554304 66482 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67274 66482 603 41 0 67233 0
vsize: 269096
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 67632 0 0 0 109833 180 0 0 25 0 1 0 490668054 277573632 66963 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67767 66963 603 41 0 67726 0
vsize: 271068
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 68114 0 0 0 110832 181 0 0 25 0 1 0 490668054 279465984 67445 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68229 67445 603 41 0 68188 0
vsize: 272916
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 68459 0 0 0 111831 182 0 0 25 0 1 0 490668054 280948736 67790 4294967295 134512640 134672761 3221224544 3221223648 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68591 67790 603 41 0 68550 0
vsize: 274364
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 68953 0 0 0 112830 184 0 0 25 0 1 0 490668054 282959872 68284 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69082 68284 603 41 0 69041 0
vsize: 276328
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 69455 0 0 0 113829 185 0 0 25 0 1 0 490668054 284958720 68786 4294967295 134512640 134672761 3221224544 3221223648 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69570 68786 603 41 0 69529 0
vsize: 278280
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 69970 0 0 0 114827 187 0 0 25 0 1 0 490668054 287092736 69301 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70091 69301 603 41 0 70050 0
vsize: 280364
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 70352 0 0 0 115826 188 0 0 25 0 1 0 490668054 288710656 69683 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70486 69683 603 41 0 70445 0
vsize: 281944
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 70728 0 0 0 116826 189 0 0 25 0 1 0 490668054 290193408 70059 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70848 70059 603 41 0 70807 0
vsize: 283392
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 70941 0 0 0 117825 189 0 0 25 0 1 0 490668054 291000320 70272 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71045 70272 603 41 0 71004 0
vsize: 284180
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 71239 0 0 0 118825 190 0 0 25 0 1 0 490668054 292212736 70570 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71341 70570 603 41 0 71300 0
vsize: 285364
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13139
Raw data (stat): 13137 (minisat+) R 13136 32461 32460 0 -1 0 71239 0 0 0 119825 190 0 0 25 0 1 0 490668054 292212736 70570 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71341 70570 603 41 0 71300 0
vsize: 285364
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.19 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 13139
Raw data (stat): 13137 (minisat+) Z 13136 32461 32460 0 -1 12 71241 0 0 0 119825 203 0 0 25 0 1 0 490668054 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.19
CPU time (s): 1200.29
CPU user time (s): 1198.25
CPU system time (s): 2.03969
CPU usage (%): 100.009
Max. virtual memory (Kb): 285364
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####