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/miplib/normalized-mps-v2-20-10-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.14
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 22140

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-22 02:18:46 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12050 boxname=wulflinc20 idbench=927 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4f0cac14ed3568050c2c57bb69fdb664  /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-mod010.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-mod010.opb /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-mod010.opb
IDLAUNCH: 12050
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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	: 3
cpu MHz		: 451.215
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        524300 kB
Buffers:         30844 kB
Cached:         456472 kB
SwapCached:        516 kB
Active:         175200 kB
Inactive:       314128 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        524048 kB
SwapTotal:     2097892 kB
SwapFree:      2096480 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5116 kB
Slab:            15460 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 02:38:48 (client local time) WITH STATUS 0 IN 1200.25 SECONDS
stats: 12050 7 1200.25 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]---> BDD-cost:122663
c ---[   0]---> BDD-cost:  751
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  407646  1200847 |  135882       0        0     nan |  0.000 % |
c |       102 |  407646  1200847 |  149470     102     8289    81.3 |  0.103 % |
c |       255 |  407646  1200847 |  164417     255    14708    57.7 |  0.103 % |
c |       481 |  407646  1200847 |  180858     481   132399   275.3 |  0.103 % |
c |       820 |  407646  1200847 |  198944     820   355047   433.0 |  0.103 % |
c |      1327 |  407646  1200847 |  218839    1327   541014   407.7 |  0.103 % |
c |      2087 |  407646  1200847 |  240723    2087   956748   458.4 |  0.103 % |
c |      3228 |  407646  1200847 |  264795    3228  1798377   557.1 |  0.103 % |
c |      4939 |  407646  1200847 |  291275    4939  3812069   771.8 |  0.103 % |
c |      7501 |  407646  1200847 |  320402    7501  6883879   917.7 |  0.103 % |
#### 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.99 2/54 17410
Raw data (stat): 17410 (runsolver) R 17409 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 550062998 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 s]
Raw data (loadavg): 0.89 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 13521 0 0 0 969 29 0 0 25 0 1 0 550062998 62861312 12547 4294967295 134512640 134672761 3221224528 3221223828 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15347 12547 603 41 0 15306 0
vsize: 61388
[startup+20.0008 s]
Raw data (loadavg): 0.91 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 13747 0 0 0 1968 31 0 0 25 0 1 0 550062998 63410176 12773 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15481 12773 603 41 0 15440 0
vsize: 61924
[startup+30.0012 s]
Raw data (loadavg): 0.92 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 13830 0 0 0 2968 31 0 0 25 0 1 0 550062998 63688704 12856 4294967295 134512640 134672761 3221224528 3221223680 134561040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15549 12856 603 41 0 15508 0
vsize: 62196
[startup+40.0022 s]
Raw data (loadavg): 0.93 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 13959 0 0 0 3967 32 0 0 25 0 1 0 550062998 64270336 12985 4294967295 134512640 134672761 3221224528 3221223632 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15691 12985 603 41 0 15650 0
vsize: 62764
[startup+50.0027 s]
Raw data (loadavg): 0.94 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 14019 0 0 0 4967 32 0 0 25 0 1 0 550062998 64409600 13045 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15725 13045 603 41 0 15684 0
vsize: 62900
[startup+60.0021 s]
Raw data (loadavg): 0.95 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 14050 0 0 0 5967 32 0 0 25 0 1 0 550062998 64532480 13076 4294967295 134512640 134672761 3221224528 3221223632 134560148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15755 13076 603 41 0 15714 0
vsize: 63020
[startup+70.0032 s]
Raw data (loadavg): 0.96 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 14179 0 0 0 6967 32 0 0 25 0 1 0 550062998 65069056 13205 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15886 13205 603 41 0 15845 0
vsize: 63544
[startup+80.004 s]
Raw data (loadavg): 0.96 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 14239 0 0 0 7967 33 0 0 25 0 1 0 550062998 65343488 13265 4294967295 134512640 134672761 3221224528 3221223696 134560822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15953 13265 603 41 0 15912 0
vsize: 63812
[startup+90.0043 s]
Raw data (loadavg): 0.97 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 14337 0 0 0 8967 33 0 0 25 0 1 0 550062998 65880064 13363 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16084 13363 603 41 0 16043 0
vsize: 64336
[startup+100.004 s]
Raw data (loadavg): 0.97 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 14494 0 0 0 9966 33 0 0 25 0 1 0 550062998 66519040 13520 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16240 13520 603 41 0 16199 0
vsize: 64960
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 14534 0 0 0 10966 33 0 0 25 0 1 0 550062998 66650112 13560 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16272 13560 603 41 0 16231 0
vsize: 65088
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 14614 0 0 0 11967 33 0 0 25 0 1 0 550062998 67039232 13640 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16367 13640 603 41 0 16326 0
vsize: 65468
[startup+130.004 s]
Raw data (loadavg): 0.98 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 14767 0 0 0 12966 34 0 0 25 0 1 0 550062998 67690496 13793 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16526 13793 603 41 0 16485 0
vsize: 66104
[startup+140.005 s]
Raw data (loadavg): 0.98 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 14806 0 0 0 13966 34 0 0 25 0 1 0 550062998 67829760 13832 4294967295 134512640 134672761 3221224528 3221223632 134560237 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16560 13832 603 41 0 16519 0
vsize: 66240
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 14879 0 0 0 14967 34 0 0 25 0 1 0 550062998 68104192 13905 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16627 13905 603 41 0 16586 0
vsize: 66508
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 14920 0 0 0 15967 34 0 0 25 0 1 0 550062998 68239360 13946 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16660 13946 603 41 0 16619 0
vsize: 66640
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 15032 0 0 0 16967 34 0 0 25 0 1 0 550062998 68775936 14058 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16791 14058 603 41 0 16750 0
vsize: 67164
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 15058 0 0 0 17967 34 0 0 25 0 1 0 550062998 68775936 14084 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16791 14084 603 41 0 16750 0
vsize: 67164
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 15071 0 0 0 18967 34 0 0 25 0 1 0 550062998 68911104 14097 4294967295 134512640 134672761 3221224528 3221223632 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16824 14097 603 41 0 16783 0
vsize: 67296
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 15092 0 0 0 19967 34 0 0 25 0 1 0 550062998 68911104 14118 4294967295 134512640 134672761 3221224528 3221223632 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16824 14118 603 41 0 16783 0
vsize: 67296
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 15136 0 0 0 20967 35 0 0 25 0 1 0 550062998 69185536 14162 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16891 14162 603 41 0 16850 0
vsize: 67564
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 15216 0 0 0 21967 35 0 0 25 0 1 0 550062998 69455872 14242 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16957 14242 603 41 0 16916 0
vsize: 67828
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 15253 0 0 0 22968 35 0 0 25 0 1 0 550062998 69595136 14279 4294967295 134512640 134672761 3221224528 3221223632 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16991 14279 603 41 0 16950 0
vsize: 67964
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 15265 0 0 0 23967 35 0 0 25 0 1 0 550062998 69730304 14291 4294967295 134512640 134672761 3221224528 3221223632 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17024 14291 603 41 0 16983 0
vsize: 68096
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 15278 0 0 0 24967 35 0 0 25 0 1 0 550062998 69730304 14304 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17024 14304 603 41 0 16983 0
vsize: 68096
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 15296 0 0 0 25967 35 0 0 25 0 1 0 550062998 69730304 14322 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17024 14322 603 41 0 16983 0
vsize: 68096
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 15357 0 0 0 26967 36 0 0 25 0 1 0 550062998 70000640 14383 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17090 14383 603 41 0 17049 0
vsize: 68360
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 15367 0 0 0 27967 36 0 0 25 0 1 0 550062998 70135808 14393 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17123 14393 603 41 0 17082 0
vsize: 68492
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 15378 0 0 0 28967 36 0 0 25 0 1 0 550062998 70135808 14404 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17123 14404 603 41 0 17082 0
vsize: 68492
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 15390 0 0 0 29967 36 0 0 25 0 1 0 550062998 70135808 14416 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17123 14416 603 41 0 17082 0
vsize: 68492
[startup+310.019 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 15405 0 0 0 30969 36 0 0 25 0 1 0 550062998 70279168 14431 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17158 14431 603 41 0 17117 0
vsize: 68632
[startup+320.023 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 15416 0 0 0 31969 36 0 0 25 0 1 0 550062998 70279168 14442 4294967295 134512640 134672761 3221224528 3221223632 134560215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17158 14442 603 41 0 17117 0
vsize: 68632
[startup+330.023 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 15428 0 0 0 32969 36 0 0 25 0 1 0 550062998 70279168 14454 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17158 14454 603 41 0 17117 0
vsize: 68632
[startup+340.023 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 15445 0 0 0 33970 36 0 0 25 0 1 0 550062998 70422528 14471 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17193 14471 603 41 0 17152 0
vsize: 68772
[startup+350.024 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 15458 0 0 0 34970 36 0 0 25 0 1 0 550062998 70422528 14484 4294967295 134512640 134672761 3221224528 3221223632 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17193 14484 603 41 0 17152 0
vsize: 68772
[startup+360.024 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 15484 0 0 0 35970 36 0 0 25 0 1 0 550062998 70529024 14510 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17219 14510 603 41 0 17178 0
vsize: 68876
[startup+370.025 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 15790 0 0 0 36968 37 0 0 25 0 1 0 550062998 71839744 14816 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17539 14816 603 41 0 17498 0
vsize: 70156
[startup+380.025 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 15961 0 0 0 37968 38 0 0 25 0 1 0 550062998 72511488 14987 4294967295 134512640 134672761 3221224528 3221223632 134560231 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17703 14987 603 41 0 17662 0
vsize: 70812
[startup+390.025 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 16132 0 0 0 38968 38 0 0 25 0 1 0 550062998 73179136 15158 4294967295 134512640 134672761 3221224528 3221223632 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17866 15158 603 41 0 17825 0
vsize: 71464
[startup+400.025 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 16245 0 0 0 39968 38 0 0 25 0 1 0 550062998 73707520 15271 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17995 15271 603 41 0 17954 0
vsize: 71980
[startup+410.025 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 16359 0 0 0 40968 38 0 0 25 0 1 0 550062998 74100736 15385 4294967295 134512640 134672761 3221224528 3221223632 134560355 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18091 15385 603 41 0 18050 0
vsize: 72364
[startup+420.025 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 16526 0 0 0 41968 39 0 0 25 0 1 0 550062998 74899456 15552 4294967295 134512640 134672761 3221224528 3221223696 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18286 15552 603 41 0 18245 0
vsize: 73144
[startup+430.025 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 16569 0 0 0 42968 39 0 0 25 0 1 0 550062998 75034624 15595 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18319 15595 603 41 0 18278 0
vsize: 73276
[startup+440.025 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 16593 0 0 0 43968 39 0 0 25 0 1 0 550062998 75034624 15619 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18319 15619 603 41 0 18278 0
vsize: 73276
[startup+450.026 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 16628 0 0 0 44968 39 0 0 25 0 1 0 550062998 75304960 15654 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18385 15654 603 41 0 18344 0
vsize: 73540
[startup+460.025 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 16666 0 0 0 45969 39 0 0 25 0 1 0 550062998 75444224 15692 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18419 15692 603 41 0 18378 0
vsize: 73676
[startup+470.025 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 16724 0 0 0 46969 39 0 0 25 0 1 0 550062998 75583488 15750 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18453 15750 603 41 0 18412 0
vsize: 73812
[startup+480.026 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 16752 0 0 0 47969 39 0 0 25 0 1 0 550062998 75722752 15778 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18487 15778 603 41 0 18446 0
vsize: 73948
[startup+490.026 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 16791 0 0 0 48969 39 0 0 25 0 1 0 550062998 75849728 15817 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18518 15817 603 41 0 18477 0
vsize: 74072
[startup+500.026 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 16810 0 0 0 49969 39 0 0 25 0 1 0 550062998 75988992 15836 4294967295 134512640 134672761 3221224528 3221223632 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18552 15836 603 41 0 18511 0
vsize: 74208
[startup+510.026 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 16840 0 0 0 50969 39 0 0 25 0 1 0 550062998 76128256 15866 4294967295 134512640 134672761 3221224528 3221223632 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18586 15866 603 41 0 18545 0
vsize: 74344
[startup+520.026 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 16881 0 0 0 51969 40 0 0 25 0 1 0 550062998 76267520 15907 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18620 15907 603 41 0 18579 0
vsize: 74480
[startup+530.026 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 16956 0 0 0 52969 40 0 0 25 0 1 0 550062998 76517376 15982 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18681 15982 603 41 0 18640 0
vsize: 74724
[startup+540.027 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 17070 0 0 0 53969 40 0 0 25 0 1 0 550062998 77070336 16096 4294967295 134512640 134672761 3221224528 3221223632 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18816 16096 603 41 0 18775 0
vsize: 75264
[startup+550.028 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 17266 0 0 0 54969 41 0 0 25 0 1 0 550062998 77864960 16292 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19010 16292 603 41 0 18969 0
vsize: 76040
[startup+560.028 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 17393 0 0 0 55969 41 0 0 25 0 1 0 550062998 78364672 16419 4294967295 134512640 134672761 3221224528 3221223632 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19132 16419 603 41 0 19091 0
vsize: 76528
[startup+570.029 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 17523 0 0 0 56968 41 0 0 25 0 1 0 550062998 78897152 16549 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19262 16549 603 41 0 19221 0
vsize: 77048
[startup+580.029 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 17690 0 0 0 57966 43 0 0 25 0 1 0 550062998 79577088 16716 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19428 16716 603 41 0 19387 0
vsize: 77712
[startup+590.03 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 17729 0 0 0 58966 43 0 0 25 0 1 0 550062998 79708160 16755 4294967295 134512640 134672761 3221224528 3221223632 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19460 16755 603 41 0 19419 0
vsize: 77840
[startup+600.03 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 17830 0 0 0 59966 44 0 0 25 0 1 0 550062998 80113664 16856 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19559 16856 603 41 0 19518 0
vsize: 78236
[startup+610.03 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 17998 0 0 0 60965 44 0 0 25 0 1 0 550062998 80785408 17024 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19723 17024 603 41 0 19682 0
vsize: 78892
[startup+620.031 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 18119 0 0 0 61965 45 0 0 25 0 1 0 550062998 81326080 17145 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19855 17145 603 41 0 19814 0
vsize: 79420
[startup+630.031 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 18210 0 0 0 62964 46 0 0 25 0 1 0 550062998 81731584 17236 4294967295 134512640 134672761 3221224528 3221223632 134560355 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19954 17236 603 41 0 19913 0
vsize: 79816
[startup+640.031 s]
Raw data (loadavg): 0.99 0.97 0.99 3/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 18234 0 0 0 63964 46 0 0 25 0 1 0 550062998 81731584 17260 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19954 17260 603 41 0 19913 0
vsize: 79816
[startup+650.032 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 18236 0 0 0 64964 46 0 0 25 0 1 0 550062998 81731584 17262 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19954 17262 603 41 0 19913 0
vsize: 79816
[startup+660.032 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 18457 0 0 0 65963 47 0 0 25 0 1 0 550062998 82681856 17483 4294967295 134512640 134672761 3221224528 3221223632 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20186 17483 603 41 0 20145 0
vsize: 80744
[startup+670.032 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 18638 0 0 0 66962 48 0 0 25 0 1 0 550062998 83488768 17664 4294967295 134512640 134672761 3221224528 3221223632 134560207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20383 17664 603 41 0 20342 0
vsize: 81532
[startup+680.032 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 18774 0 0 0 67962 49 0 0 25 0 1 0 550062998 84017152 17800 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20512 17800 603 41 0 20471 0
vsize: 82048
[startup+690.033 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 19002 0 0 0 68962 49 0 0 25 0 1 0 550062998 84955136 18028 4294967295 134512640 134672761 3221224528 3221223632 134560279 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20741 18028 603 41 0 20700 0
vsize: 82964
[startup+700.032 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 19131 0 0 0 69961 49 0 0 25 0 1 0 550062998 85499904 18157 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20874 18157 603 41 0 20833 0
vsize: 83496
[startup+710.032 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 19259 0 0 0 70961 50 0 0 25 0 1 0 550062998 86048768 18285 4294967295 134512640 134672761 3221224528 3221223632 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21008 18285 603 41 0 20967 0
vsize: 84032
[startup+720.033 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 19307 0 0 0 71961 50 0 0 25 0 1 0 550062998 86183936 18333 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21041 18333 603 41 0 21000 0
vsize: 84164
[startup+730.033 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 19422 0 0 0 72961 50 0 0 25 0 1 0 550062998 86716416 18448 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21171 18448 603 41 0 21130 0
vsize: 84684
[startup+740.033 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 19511 0 0 0 73961 51 0 0 25 0 1 0 550062998 86974464 18537 4294967295 134512640 134672761 3221224528 3221223632 134560399 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21234 18537 603 41 0 21193 0
vsize: 84936
[startup+750.033 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 19641 0 0 0 74961 51 0 0 25 0 1 0 550062998 87502848 18667 4294967295 134512640 134672761 3221224528 3221223696 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21363 18667 603 41 0 21322 0
vsize: 85452
[startup+760.033 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 19819 0 0 0 75961 51 0 0 25 0 1 0 550062998 88285184 18845 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21554 18845 603 41 0 21513 0
vsize: 86216
[startup+770.034 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 19921 0 0 0 76961 52 0 0 25 0 1 0 550062998 88694784 18947 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21654 18947 603 41 0 21613 0
vsize: 86616
[startup+780.033 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 20006 0 0 0 77960 52 0 0 25 0 1 0 550062998 88969216 19032 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21721 19032 603 41 0 21680 0
vsize: 86884
[startup+790.034 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 20115 0 0 0 78960 52 0 0 25 0 1 0 550062998 89481216 19141 4294967295 134512640 134672761 3221224528 3221223728 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21846 19141 603 41 0 21805 0
vsize: 87384
[startup+800.034 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 20238 0 0 0 79960 52 0 0 25 0 1 0 550062998 90021888 19264 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21978 19264 603 41 0 21937 0
vsize: 87912
[startup+810.034 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 20283 0 0 0 80960 52 0 0 25 0 1 0 550062998 90157056 19309 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22011 19309 603 41 0 21970 0
vsize: 88044
[startup+820.034 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 20291 0 0 0 81961 53 0 0 25 0 1 0 550062998 90157056 19317 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22011 19317 603 41 0 21970 0
vsize: 88044
[startup+830.034 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 20331 0 0 0 82961 53 0 0 25 0 1 0 550062998 90292224 19357 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22044 19357 603 41 0 22003 0
vsize: 88176
[startup+840.035 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 20366 0 0 0 83961 53 0 0 25 0 1 0 550062998 90411008 19392 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22073 19392 603 41 0 22032 0
vsize: 88292
[startup+850.035 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 20409 0 0 0 84960 54 0 0 25 0 1 0 550062998 90689536 19435 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22141 19435 603 41 0 22100 0
vsize: 88564
[startup+860.034 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 20441 0 0 0 85960 54 0 0 25 0 1 0 550062998 90824704 19467 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22174 19467 603 41 0 22133 0
vsize: 88696
[startup+870.034 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 20492 0 0 0 86960 54 0 0 25 0 1 0 550062998 90963968 19518 4294967295 134512640 134672761 3221224528 3221223696 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22208 19518 603 41 0 22167 0
vsize: 88832
[startup+880.034 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 20597 0 0 0 87959 54 0 0 25 0 1 0 550062998 91373568 19623 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22308 19623 603 41 0 22267 0
vsize: 89232
[startup+890.034 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 20699 0 0 0 88959 55 0 0 25 0 1 0 550062998 91770880 19725 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22405 19725 603 41 0 22364 0
vsize: 89620
[startup+900.034 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 20808 0 0 0 89959 55 0 0 25 0 1 0 550062998 92303360 19834 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22535 19834 603 41 0 22494 0
vsize: 90140
[startup+910.034 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 20869 0 0 0 90959 55 0 0 25 0 1 0 550062998 92561408 19895 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22598 19895 603 41 0 22557 0
vsize: 90392
[startup+920.034 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 20965 0 0 0 91959 55 0 0 25 0 1 0 550062998 92971008 19991 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22698 19991 603 41 0 22657 0
vsize: 90792
[startup+930.034 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 21124 0 0 0 92959 56 0 0 25 0 1 0 550062998 93519872 20150 4294967295 134512640 134672761 3221224528 3221223632 134560381 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22832 20150 603 41 0 22791 0
vsize: 91328
[startup+940.035 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 21325 0 0 0 93959 56 0 0 25 0 1 0 550062998 94392320 20351 4294967295 134512640 134672761 3221224528 3221223632 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23045 20351 603 41 0 23004 0
vsize: 92180
[startup+950.035 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 21497 0 0 0 94959 57 0 0 25 0 1 0 550062998 95072256 20523 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23211 20523 603 41 0 23170 0
vsize: 92844
[startup+960.035 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 21588 0 0 0 95959 57 0 0 25 0 1 0 550062998 95485952 20614 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23312 20614 603 41 0 23271 0
vsize: 93248
[startup+970.035 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 21712 0 0 0 96959 57 0 0 25 0 1 0 550062998 96014336 20738 4294967295 134512640 134672761 3221224528 3221223632 134560194 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23441 20738 603 41 0 23400 0
vsize: 93764
[startup+980.035 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 21861 0 0 0 97959 57 0 0 25 0 1 0 550062998 96559104 20887 4294967295 134512640 134672761 3221224528 3221223632 134560250 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23574 20887 603 41 0 23533 0
vsize: 94296
[startup+990.036 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 22103 0 0 0 98958 57 0 0 25 0 1 0 550062998 97636352 21129 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23837 21129 603 41 0 23796 0
vsize: 95348
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 22238 0 0 0 99958 58 0 0 25 0 1 0 550062998 98152448 21264 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23963 21264 603 41 0 23922 0
vsize: 95852
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 22454 0 0 0 100958 59 0 0 25 0 1 0 550062998 99069952 21480 4294967295 134512640 134672761 3221224528 3221223712 134559542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24187 21480 603 41 0 24146 0
vsize: 96748
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 22601 0 0 0 101957 59 0 0 25 0 1 0 550062998 99717120 21627 4294967295 134512640 134672761 3221224528 3221223632 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24345 21627 603 41 0 24304 0
vsize: 97380
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 22704 0 0 0 102957 59 0 0 25 0 1 0 550062998 100118528 21730 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24443 21730 603 41 0 24402 0
vsize: 97772
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 22766 0 0 0 103957 60 0 0 25 0 1 0 550062998 100257792 21792 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24477 21792 603 41 0 24436 0
vsize: 97908
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 22824 0 0 0 104957 60 0 0 25 0 1 0 550062998 100524032 21850 4294967295 134512640 134672761 3221224528 3221223632 134560393 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24542 21850 603 41 0 24501 0
vsize: 98168
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 22881 0 0 0 105957 60 0 0 25 0 1 0 550062998 100802560 21907 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24610 21907 603 41 0 24569 0
vsize: 98440
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 22928 0 0 0 106957 60 0 0 25 0 1 0 550062998 100937728 21954 4294967295 134512640 134672761 3221224528 3221223632 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24643 21954 603 41 0 24602 0
vsize: 98572
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 22999 0 0 0 107957 60 0 0 25 0 1 0 550062998 101343232 22025 4294967295 134512640 134672761 3221224528 3221223632 134560396 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24742 22025 603 41 0 24701 0
vsize: 98968
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 23187 0 0 0 108957 61 0 0 25 0 1 0 550062998 102010880 22213 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24905 22213 603 41 0 24864 0
vsize: 99620
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 23284 0 0 0 109957 61 0 0 25 0 1 0 550062998 102420480 22310 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25005 22310 603 41 0 24964 0
vsize: 100020
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 23416 0 0 0 110957 61 0 0 25 0 1 0 550062998 102940672 22442 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25132 22442 603 41 0 25091 0
vsize: 100528
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 23443 0 0 0 111957 62 0 0 25 0 1 0 550062998 103075840 22469 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25165 22469 603 41 0 25124 0
vsize: 100660
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 23561 0 0 0 112957 62 0 0 25 0 1 0 550062998 103620608 22587 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25298 22587 603 41 0 25257 0
vsize: 101192
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 23627 0 0 0 113957 62 0 0 25 0 1 0 550062998 103895040 22653 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25365 22653 603 41 0 25324 0
vsize: 101460
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 23672 0 0 0 114957 62 0 0 25 0 1 0 550062998 104005632 22698 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25392 22698 603 41 0 25351 0
vsize: 101568
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 23694 0 0 0 115957 62 0 0 25 0 1 0 550062998 104148992 22720 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25427 22720 603 41 0 25386 0
vsize: 101708
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 23716 0 0 0 116957 62 0 0 25 0 1 0 550062998 104148992 22742 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25427 22742 603 41 0 25386 0
vsize: 101708
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 23752 0 0 0 117957 62 0 0 25 0 1 0 550062998 104292352 22778 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25462 22778 603 41 0 25421 0
vsize: 101848
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 23812 0 0 0 118957 62 0 0 25 0 1 0 550062998 104570880 22838 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25530 22838 603 41 0 25489 0
vsize: 102120
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 17410
Raw data (stat): 17410 (minisat+) R 17409 27565 27564 0 -1 0 23874 0 0 0 119957 62 0 0 25 0 1 0 550062998 104828928 22900 4294967295 134512640 134672761 3221224528 3221223632 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25593 22900 603 41 0 25552 0
vsize: 102372
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.99 1/54 17410
Raw data (stat): 17410 (minisat+) Z 17409 27565 27564 0 -1 12 23876 0 0 0 119958 67 0 0 25 0 1 0 550062998 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.08
CPU time (s): 1200.25
CPU user time (s): 1199.58
CPU system time (s): 0.673897
CPU usage (%): 100.014
Max. virtual memory (Kb): 102372
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####