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/submitted/manquinho/logic-synthesis/normalized-clip.b.opb
MD5SUM	cddae768b283c2db142f16fe9d163db1
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	15
Optimality of the best value was proved	NO
Number of terms in the objective function	350
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	350
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	350
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.05084
Number of variables	349
Total number of constraints	715
Number of constraints which are clauses	707
Number of constraints which are cardinality constraints (but not clauses)	8
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	111
Trace number 4655

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-04-13 19:34:38 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3448 boxname=wulflinc1 idbench=64 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  cddae768b283c2db142f16fe9d163db1  /oldhome/oroussel/tmp/wulflinc1/normalized-clip.b.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc1/normalized-clip.b.opb /oldhome/oroussel/tmp/wulflinc1/normalized-clip.b.opb
IDLAUNCH: 3448
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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.053
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:        864372 kB
Buffers:         39912 kB
Cached:         105744 kB
SwapCached:          0 kB
Active:         107036 kB
Inactive:        42324 kB
HighTotal:      131008 kB
HighFree:        32312 kB
LowTotal:       903652 kB
LowFree:        832060 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           8436 kB
Slab:            15196 kB
Committed_AS:    96700 kB
PageTables:        388 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 19:50:51 (client local time) WITH STATUS 30 IN 972.248 SECONDS
stats: 3448 0 972.248 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 705 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |     705    14499 |     235       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 21[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 686   maxlim: 329   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         2 |    5451    31443 |    1817       2      131    65.5 |  0.000 % |
c |       104 |    5451    31443 |    1998     104      713     6.9 |  0.867 % |
c |       254 |    5367    31155 |    2198     242     1424     5.9 |  2.409 % |
c |       479 |    5360    31132 |    2418     466     2796     6.0 |  2.505 % |
c |       818 |    5342    31074 |    2660     803    10221    12.7 |  2.890 % |
c |      1327 |    5342    31074 |    2926    1312    32430    24.7 |  2.890 % |
c ==============================================================================
c [1mFound solution: 20[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 330   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1691 |    5349    31102 |    1783    1676    54733    32.7 |  2.890 % |
c |      1791 |    5349    31102 |    1961    1776    60375    34.0 |  2.981 % |
c |      1943 |    5349    31102 |    2157    1928    76174    39.5 |  2.981 % |
c |      2170 |    5349    31102 |    2373    2155    96834    44.9 |  2.981 % |
c |      2508 |    5349    31102 |    2610    2493   131391    52.7 |  2.981 % |
c |      3014 |    5349    31102 |    2871    2999   175088    58.4 |  2.981 % |
c |      3773 |    5349    31102 |    3158    2259   112271    49.7 |  2.981 % |
c ==============================================================================
c [1mFound solution: 19[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 331   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4186 |    5350    31106 |    1783    2672   153024    57.3 |  2.981 % |
c |      4288 |    5350    31106 |    1961    1438    53052    36.9 |  3.074 % |
c |      4439 |    5350    31106 |    2157    1589    59480    37.4 |  3.074 % |
c |      4664 |    5350    31106 |    2373    1814    67187    37.0 |  3.074 % |
c |      5001 |    5350    31106 |    2610    2151    84653    39.4 |  3.074 % |
c |      5508 |    5350    31106 |    2871    2658   133625    50.3 |  3.075 % |
c |      6269 |    5350    31106 |    3158    1847    71232    38.6 |  3.074 % |
c |      7409 |    5350    31106 |    3474    2987   145666    48.8 |  3.074 % |
c ==============================================================================
c [1mFound solution: 18[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 332   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8626 |    5355    31128 |    1785    2263    98241    43.4 |  3.074 % |
c |      8726 |    5355    31128 |    1963    1232    24293    19.7 |  3.167 % |
c |      8876 |    5355    31128 |    2159    1382    31412    22.7 |  3.168 % |
c |      9101 |    5355    31128 |    2375    1607    44777    27.9 |  3.169 % |
c |      9440 |    5355    31128 |    2613    1946    65083    33.4 |  3.167 % |
c |      9948 |    5355    31128 |    2874    2454    97664    39.8 |  3.167 % |
c |     10707 |    5355    31128 |    3162    1694    45975    27.1 |  3.167 % |
c |     11846 |    5355    31128 |    3478    2833   116386    41.1 |  3.167 % |
c ==============================================================================
c [1mFound solution: 16[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 334   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13406 |    5357    31139 |    1785    2561    93017    36.3 |  3.167 % |
c |     13507 |    5357    31139 |    1963    1382    27349    19.8 |  3.353 % |
c |     13662 |    5357    31139 |    2159    1537    35692    23.2 |  3.353 % |
c |     13887 |    5357    31139 |    2375    1762    43982    25.0 |  3.353 % |
c |     14224 |    5357    31139 |    2613    2099    60189    28.7 |  3.353 % |
c |     14731 |    5357    31139 |    2874    2606    83226    31.9 |  3.353 % |
c |     15491 |    5357    31139 |    3162    1789    40758    22.8 |  3.353 % |
c |     16632 |    5357    31139 |    3478    2930    99919    34.1 |  3.353 % |
c |     18342 |    5357    31139 |    3826    2824    95801    33.9 |  3.353 % |
c |     20904 |    5357    31139 |    4208    3412   114438    33.5 |  3.353 % |
c |     24749 |    5357    31139 |    4629    2751   106054    38.6 |  3.353 % |
c |     30517 |    5357    31139 |    5092    3717   151622    40.8 |  3.353 % |
c |     39167 |    5357    31139 |    5602    4327   216537    50.0 |  3.353 % |
c |     52141 |    5357    31139 |    6162    5577   376169    67.5 |  3.353 % |
c |     71602 |    5357    31139 |    6778    5965   292534    49.0 |  3.353 % |
c ==============================================================================
c [1mFound solution: 15[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 335   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86453 |    5275    30837 |    1758    6808   353959    52.0 |  3.353 % |
c |     86554 |    5190    30542 |    1933    1774    61931    34.9 |  6.411 % |
c |     86704 |    5181    30513 |    2127    1923    68442    35.6 |  6.412 % |
c |     86930 |    5181    30513 |    2339    2149    76880    35.8 |  6.412 % |
c |     87269 |    5181    30513 |    2573    1261    18473    14.6 |  6.412 % |
c |     87776 |    5181    30513 |    2831    1768    41009    23.2 |  6.412 % |
c |     88535 |    5181    30513 |    3114    2527    73573    29.1 |  6.412 % |
c |     89675 |    5181    30513 |    3425    2021    59474    29.4 |  6.412 % |
c |     91383 |    5181    30513 |    3768    3729   187380    50.2 |  6.412 % |
c |     93945 |    5181    30513 |    4145    2236    80244    35.9 |  6.412 % |
c |     97789 |    5181    30513 |    4559    3922   199378    50.8 |  6.412 % |
c |    103559 |    5181    30513 |    5015    2463   108172    43.9 |  6.412 % |
c |    112210 |    5181    30513 |    5517    3353   132031    39.4 |  6.412 % |
c |    125184 |    5181    30513 |    6069    5006   230674    46.1 |  6.412 % |
c |    144646 |    5181    30513 |    6676    5594   293095    52.4 |  6.412 % |
c |    173839 |    5181    30513 |    7343    3872   148858    38.4 |  6.412 % |
c |    217628 |    5181    30513 |    8077    5844   303416    51.9 |  6.412 % |
c |    283313 |    5181    30513 |    8885    5285   215316    40.7 |  6.412 % |
c |    381839 |    5181    30513 |    9774    8270   370015    44.7 |  6.412 % |
c |    529632 |    5181    30513 |   10751    6839   270304    39.5 |  6.412 % |
c |    751319 |    5181    30513 |   11826    9884   399416    40.4 |  6.412 % |
c |   1083851 |    5181    30513 |   13009   10914   415152    38.0 |  6.412 % |
c ==============================================================================
c [1mOptimal solution: 15[0m
s OPTIMUM FOUND
v -x1 -x2 -x3 -x4 -x5 -x6 -x7 -x8 -x9 -x10 -x11 -x12 -x13 -x14 -x15 -x16 -x17 -x18 -x19 -x20 x21 -x22 -x23 -x24 -x25 -x26 -x27 -x28 -x29 -x30 -x31 -x32 -x33 -x34 -x35 -x36 -x37 -x38 -x39 -x40 -x41 -x42 -x43 -x44 -x45 -x46 -x47 -x48 -x49 -x50 x51 -x52 -x53 -x54 -x55 -x56 x57 -x58 -x59 -x60 -x61 -x62 -x63 -x64 -x65 -x66 -x67 -x68 -x69 -x70 -x71 -x72 -x73 x74 -x75 -x76 -x77 -x78 -x79 -x80 -x81 x82 -x83 -x84 -x85 -x86 -x87 -x88 x89 -x90 -x91 -x92 -x93 x94 -x95 -x96 -x97 -x98 -x99 -x100 -x101 -x102 -x103 -x104 -x105 -x106 -x107 -x108 -x109 -x110 -x111 -x112 -x113 -x114 -x115 -x116 -x117 x118 -x119 -x120 -x121 -x122 -x123 -x124 -x125 -x126 -x127 -x128 -x129 -x130 -x131 -x132 -x133 -x134 -x135 -x136 -x137 -x138 -x139 -x140 -x141 -x142 -x143 -x144 -x145 -x146 -x147 -x148 -x149 -x150 -x151 -x152 -x153 -x154 -x155 -x156 -x157 -x158 -x159 -x160 -x161 -x162 -x163 -x164 -x165 -x166 -x167 -x168 -x169 -x170 -x171 -x172 -x173 -x174 -x175 -x176 -x177 -x178 -x179 -x180 -x181 -x182 -x183 -x184 -x185 -x186 -x187 -x188 -x189 -x190 -x191 -x192 -x193 -x194 -x195 -x196 -x197 -x198 x199 -x200 -x201 -x202 -x203 -x204 -x205 -x206 -x207 -x208 -x209 -x210 -x211 -x212 -x213 -x214 -x215 -x216 x217 -x218 -x219 -x220 -x221 -x222 -x223 -x224 -x225 -x226 -x227 -x228 -x229 -x230 -x231 -x232 -x233 -x234 -x235 -x236 -x237 -x238 -x239 -x240 -x241 -x242 -x243 -x244 -x245 -x246 -x247 -x248 -x249 x250 -x251 -x252 -x253 -x254 -x255 -x256 -x257 -x258 -x259 -x260 -x261 -x262 x263 -x264 -x265 -x266 -x267 -x268 x269 -x270 -x271 -x272 -x273 -x274 -x275 -x276 -x277 -x278 -x279 -x280 -x281 -x282 -x283 -x284 -x285 -x286 -x287 -x288 -x289 -x290 -x291 -x292 -x293 -x294 -x295 -x296 -x297 -x298 -x299 -x300 x301 -x302 -x303 -x304 -x305 x306 -x307 -x308 -x309 -x310 -x311 -x312 -x313 -x314 -x315 -x316 -x317 -x318 -x319 -x320 -x321 -x322 -x323 -x324 -x325 -x326 -x327 -x328 -x329 -x330 -x331 -x332 -x333 -x334 -x335 -x336 -x337 -x338 -x339 -x340 -x341 -x342 -x343 -x344 -x345 -x346 -x347 -x348 -x349 -x350
c _______________________________________________________________________________
c 
c restarts              : 67
c conflicts             : 1455809        (1498 /sec)
c decisions             : 2446193        (2516 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 972.095 s
c _______________________________________________________________________________
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.75 0.39 2/59 14670
Raw data (stat): 14670 (runsolver) R 14669 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 363433169 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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.0004 s]
Raw data (loadavg): 0.93 0.76 0.39 2/59 14670
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 748 0 0 0 997 1 0 0 25 0 1 0 363433169 4624384 726 4294967295 134512640 134672761 3221224576 3221223744 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1129 726 603 41 0 1088 0
vsize: 4516
[startup+20.0003 s]
Raw data (loadavg): 0.94 0.76 0.40 2/59 14670
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 967 0 0 0 1997 2 0 0 25 0 1 0 363433169 5431296 945 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1326 945 603 41 0 1285 0
vsize: 5304
[startup+30.0011 s]
Raw data (loadavg): 0.95 0.77 0.41 2/59 14670
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1116 0 0 0 2996 3 0 0 25 0 1 0 363433169 6103040 1094 4294967295 134512640 134672761 3221224576 3221223712 134565110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1490 1094 603 41 0 1449 0
vsize: 5960
[startup+40.0009 s]
Raw data (loadavg): 0.95 0.78 0.41 2/59 14670
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1122 0 0 0 3996 3 0 0 25 0 1 0 363433169 6103040 1100 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1490 1100 603 41 0 1449 0
vsize: 5960
[startup+50.0021 s]
Raw data (loadavg): 0.96 0.78 0.42 2/59 14670
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1143 0 0 0 4996 4 0 0 25 0 1 0 363433169 6242304 1121 4294967295 134512640 134672761 3221224576 3221223744 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1524 1121 603 41 0 1483 0
vsize: 6096
[startup+60.0025 s]
Raw data (loadavg): 0.97 0.79 0.42 2/59 14670
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1143 0 0 0 5995 4 0 0 25 0 1 0 363433169 6242304 1121 4294967295 134512640 134672761 3221224576 3221223700 134566018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1524 1121 603 41 0 1483 0
vsize: 6096
[startup+70.0022 s]
Raw data (loadavg): 0.97 0.80 0.43 2/59 14670
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1151 0 0 0 6995 4 0 0 25 0 1 0 363433169 6242304 1129 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1524 1129 603 41 0 1483 0
vsize: 6096
[startup+80.003 s]
Raw data (loadavg): 0.98 0.80 0.43 2/59 14670
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1238 0 0 0 7995 4 0 0 25 0 1 0 363433169 6639616 1216 4294967295 134512640 134672761 3221224576 3221223712 134565121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1621 1216 603 41 0 1580 0
vsize: 6484
[startup+90.0028 s]
Raw data (loadavg): 0.98 0.81 0.44 2/59 14670
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1310 0 0 0 8995 5 0 0 25 0 1 0 363433169 6914048 1288 4294967295 134512640 134672761 3221224576 3221223712 134565089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1688 1288 603 41 0 1647 0
vsize: 6752
[startup+100.004 s]
Raw data (loadavg): 0.98 0.81 0.45 2/59 14672
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1313 0 0 0 9995 5 0 0 25 0 1 0 363433169 6914048 1291 4294967295 134512640 134672761 3221224576 3221223744 134564734 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1688 1291 603 41 0 1647 0
vsize: 6752
[startup+110.005 s]
Raw data (loadavg): 0.98 0.82 0.45 2/59 14672
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1345 0 0 0 10995 5 0 0 25 0 1 0 363433169 7053312 1323 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1722 1323 603 41 0 1681 0
vsize: 6888
[startup+120.005 s]
Raw data (loadavg): 0.99 0.83 0.46 2/59 14672
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1429 0 0 0 11994 6 0 0 25 0 1 0 363433169 7319552 1407 4294967295 134512640 134672761 3221224576 3221223760 134559166 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1787 1407 603 41 0 1746 0
vsize: 7148
[startup+130.005 s]
Raw data (loadavg): 0.99 0.83 0.46 2/59 14672
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1453 0 0 0 12994 6 0 0 25 0 1 0 363433169 7454720 1431 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1820 1431 603 41 0 1779 0
vsize: 7280
[startup+140.005 s]
Raw data (loadavg): 0.99 0.84 0.47 2/59 14672
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1454 0 0 0 13994 6 0 0 25 0 1 0 363433169 7454720 1432 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1820 1432 603 41 0 1779 0
vsize: 7280
[startup+150.005 s]
Raw data (loadavg): 0.99 0.84 0.47 2/59 14672
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1454 0 0 0 14995 6 0 0 25 0 1 0 363433169 7454720 1432 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1820 1432 603 41 0 1779 0
vsize: 7280
[startup+160.005 s]
Raw data (loadavg): 0.99 0.85 0.48 2/59 14672
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1463 0 0 0 15994 6 0 0 25 0 1 0 363433169 7589888 1441 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1853 1441 603 41 0 1812 0
vsize: 7412
[startup+170.005 s]
Raw data (loadavg): 0.99 0.85 0.48 2/59 14672
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1479 0 0 0 16994 6 0 0 25 0 1 0 363433169 7589888 1457 4294967295 134512640 134672761 3221224576 3221223680 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1853 1457 603 41 0 1812 0
vsize: 7412
[startup+180.006 s]
Raw data (loadavg): 0.99 0.85 0.49 2/59 14672
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1507 0 0 0 17994 7 0 0 25 0 1 0 363433169 7725056 1485 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1886 1485 603 41 0 1845 0
vsize: 7544
[startup+190.007 s]
Raw data (loadavg): 0.99 0.86 0.49 2/59 14672
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1532 0 0 0 18994 7 0 0 25 0 1 0 363433169 7860224 1510 4294967295 134512640 134672761 3221224576 3221223760 134559182 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1919 1510 603 41 0 1878 0
vsize: 7676
[startup+200.007 s]
Raw data (loadavg): 0.99 0.86 0.50 2/59 14672
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1554 0 0 0 19994 7 0 0 25 0 1 0 363433169 7860224 1532 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1919 1532 603 41 0 1878 0
vsize: 7676
[startup+210.007 s]
Raw data (loadavg): 0.99 0.87 0.50 2/59 14672
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1557 0 0 0 20994 7 0 0 25 0 1 0 363433169 8003584 1535 4294967295 134512640 134672761 3221224576 3221223744 134560976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1954 1535 603 41 0 1913 0
vsize: 7816
[startup+220.007 s]
Raw data (loadavg): 0.99 0.87 0.51 2/59 14672
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1576 0 0 0 21994 7 0 0 25 0 1 0 363433169 8003584 1554 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1954 1554 603 41 0 1913 0
vsize: 7816
[startup+230.007 s]
Raw data (loadavg): 0.99 0.87 0.51 2/59 14672
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1588 0 0 0 22994 7 0 0 25 0 1 0 363433169 8003584 1566 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1954 1566 603 41 0 1913 0
vsize: 7816
[startup+240.006 s]
Raw data (loadavg): 0.99 0.88 0.52 2/59 14672
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1588 0 0 0 23994 7 0 0 25 0 1 0 363433169 8003584 1566 4294967295 134512640 134672761 3221224576 3221223700 134566133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1954 1566 603 41 0 1913 0
vsize: 7816
[startup+250.006 s]
Raw data (loadavg): 0.99 0.88 0.52 2/59 14672
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1690 0 0 0 24995 7 0 0 25 0 1 0 363433169 8536064 1668 4294967295 134512640 134672761 3221224576 3221223744 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2084 1668 603 41 0 2043 0
vsize: 8336
[startup+260.006 s]
Raw data (loadavg): 0.99 0.89 0.53 2/59 14672
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1698 0 0 0 25995 7 0 0 25 0 1 0 363433169 8536064 1676 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2084 1676 603 41 0 2043 0
vsize: 8336
[startup+270.006 s]
Raw data (loadavg): 0.99 0.89 0.53 2/59 14672
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1703 0 0 0 26995 7 0 0 25 0 1 0 363433169 8536064 1681 4294967295 134512640 134672761 3221224576 3221222928 134565829 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2084 1681 603 41 0 2043 0
vsize: 8336
[startup+280.005 s]
Raw data (loadavg): 0.99 0.89 0.54 2/59 14672
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1708 0 0 0 27995 7 0 0 25 0 1 0 363433169 8536064 1686 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2084 1686 603 41 0 2043 0
vsize: 8336
[startup+290.005 s]
Raw data (loadavg): 0.99 0.89 0.54 2/59 14672
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1720 0 0 0 28995 7 0 0 25 0 1 0 363433169 8683520 1698 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2120 1698 603 41 0 2079 0
vsize: 8480
[startup+300.006 s]
Raw data (loadavg): 0.99 0.90 0.55 2/59 14672
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1734 0 0 0 29995 8 0 0 25 0 1 0 363433169 8683520 1712 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2120 1712 603 41 0 2079 0
vsize: 8480
[startup+310.006 s]
Raw data (loadavg): 0.99 0.90 0.55 2/59 14672
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1735 0 0 0 30995 8 0 0 25 0 1 0 363433169 8683520 1713 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2120 1713 603 41 0 2079 0
vsize: 8480
[startup+320.005 s]
Raw data (loadavg): 0.99 0.90 0.55 2/59 14672
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1737 0 0 0 31995 8 0 0 25 0 1 0 363433169 8683520 1715 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2120 1715 603 41 0 2079 0
vsize: 8480
[startup+330.006 s]
Raw data (loadavg): 0.99 0.91 0.56 2/59 14672
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1756 0 0 0 32995 8 0 0 25 0 1 0 363433169 8818688 1734 4294967295 134512640 134672761 3221224576 3221223736 134561029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2153 1734 603 41 0 2112 0
vsize: 8612
[startup+340.006 s]
Raw data (loadavg): 0.99 0.91 0.56 2/59 14672
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1756 0 0 0 33996 8 0 0 25 0 1 0 363433169 8818688 1734 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2153 1734 603 41 0 2112 0
vsize: 8612
[startup+350.006 s]
Raw data (loadavg): 0.99 0.91 0.57 2/59 14672
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1771 0 0 0 34996 8 0 0 25 0 1 0 363433169 8818688 1749 4294967295 134512640 134672761 3221224576 3221223680 134559838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2153 1749 603 41 0 2112 0
vsize: 8612
[startup+360.007 s]
Raw data (loadavg): 0.99 0.91 0.57 2/59 14672
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1823 0 0 0 35996 8 0 0 25 0 1 0 363433169 9089024 1801 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2219 1801 603 41 0 2178 0
vsize: 8876
[startup+370.006 s]
Raw data (loadavg): 0.99 0.92 0.57 2/59 14672
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1835 0 0 0 36996 8 0 0 25 0 1 0 363433169 9089024 1813 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2219 1813 603 41 0 2178 0
vsize: 8876
[startup+380.006 s]
Raw data (loadavg): 0.99 0.92 0.58 2/59 14672
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1835 0 0 0 37996 8 0 0 25 0 1 0 363433169 9089024 1813 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2219 1813 603 41 0 2178 0
vsize: 8876
[startup+390.006 s]
Raw data (loadavg): 0.99 0.92 0.58 2/59 14672
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1835 0 0 0 38996 8 0 0 25 0 1 0 363433169 9089024 1813 4294967295 134512640 134672761 3221224576 3221223680 134559966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2219 1813 603 41 0 2178 0
vsize: 8876
[startup+400.007 s]
Raw data (loadavg): 0.99 0.92 0.58 2/59 14674
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1835 0 0 0 39996 8 0 0 25 0 1 0 363433169 9089024 1813 4294967295 134512640 134672761 3221224576 3221223712 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2219 1813 603 41 0 2178 0
vsize: 8876
[startup+410.007 s]
Raw data (loadavg): 0.99 0.92 0.59 2/59 14674
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1835 0 0 0 40996 8 0 0 25 0 1 0 363433169 9089024 1813 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2219 1813 603 41 0 2178 0
vsize: 8876
[startup+420.006 s]
Raw data (loadavg): 0.99 0.93 0.59 2/59 14674
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1839 0 0 0 41997 8 0 0 25 0 1 0 363433169 9089024 1817 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2219 1817 603 41 0 2178 0
vsize: 8876
[startup+430.007 s]
Raw data (loadavg): 0.99 0.93 0.60 2/59 14674
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1849 0 0 0 42997 8 0 0 25 0 1 0 363433169 9228288 1827 4294967295 134512640 134672761 3221224576 3221223728 134565153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2253 1827 603 41 0 2212 0
vsize: 9012
[startup+440.007 s]
Raw data (loadavg): 0.99 0.93 0.60 2/59 14674
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1854 0 0 0 43997 8 0 0 25 0 1 0 363433169 9228288 1832 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2253 1832 603 41 0 2212 0
vsize: 9012
[startup+450.007 s]
Raw data (loadavg): 0.99 0.93 0.60 2/59 14674
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1854 0 0 0 44997 8 0 0 25 0 1 0 363433169 9228288 1832 4294967295 134512640 134672761 3221224576 3221223680 134554910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2253 1832 603 41 0 2212 0
vsize: 9012
[startup+460.006 s]
Raw data (loadavg): 0.99 0.93 0.61 2/59 14674
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1858 0 0 0 45997 8 0 0 25 0 1 0 363433169 9228288 1836 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2253 1836 603 41 0 2212 0
vsize: 9012
[startup+470.007 s]
Raw data (loadavg): 0.99 0.94 0.61 2/59 14674
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1859 0 0 0 46997 8 0 0 25 0 1 0 363433169 9228288 1837 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2253 1837 603 41 0 2212 0
vsize: 9012
[startup+480.007 s]
Raw data (loadavg): 0.99 0.94 0.62 2/59 14674
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1865 0 0 0 47997 8 0 0 25 0 1 0 363433169 9228288 1843 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2253 1843 603 41 0 2212 0
vsize: 9012
[startup+490.007 s]
Raw data (loadavg): 0.99 0.94 0.62 2/59 14674
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1874 0 0 0 48997 8 0 0 25 0 1 0 363433169 9375744 1852 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2289 1852 603 41 0 2248 0
vsize: 9156
[startup+500.008 s]
Raw data (loadavg): 0.99 0.94 0.62 2/59 14674
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1875 0 0 0 49997 8 0 0 25 0 1 0 363433169 9375744 1853 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2289 1853 603 41 0 2248 0
vsize: 9156
[startup+510.007 s]
Raw data (loadavg): 0.99 0.94 0.63 2/59 14674
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1885 0 0 0 50997 9 0 0 25 0 1 0 363433169 9375744 1863 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2289 1863 603 41 0 2248 0
vsize: 9156
[startup+520.007 s]
Raw data (loadavg): 0.99 0.94 0.63 2/59 14674
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1886 0 0 0 51997 9 0 0 25 0 1 0 363433169 9375744 1864 4294967295 134512640 134672761 3221224576 3221223744 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2289 1864 603 41 0 2248 0
vsize: 9156
[startup+530.009 s]
Raw data (loadavg): 0.99 0.94 0.64 2/59 14674
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 1918 0 0 0 52997 9 0 0 25 0 1 0 363433169 9506816 1896 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2321 1896 603 41 0 2280 0
vsize: 9284
[startup+540.009 s]
Raw data (loadavg): 0.99 0.95 0.64 2/59 14674
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2000 0 0 0 53997 9 0 0 25 0 1 0 363433169 9932800 1978 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2425 1978 603 41 0 2384 0
vsize: 9700
[startup+550.01 s]
Raw data (loadavg): 0.99 0.95 0.64 2/59 14674
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2001 0 0 0 54997 10 0 0 25 0 1 0 363433169 9932800 1979 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2425 1979 603 41 0 2384 0
vsize: 9700
[startup+560.009 s]
Raw data (loadavg): 0.99 0.95 0.64 2/59 14674
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2002 0 0 0 55996 10 0 0 25 0 1 0 363433169 9932800 1980 4294967295 134512640 134672761 3221224576 3221223744 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2425 1980 603 41 0 2384 0
vsize: 9700
[startup+570.009 s]
Raw data (loadavg): 0.99 0.95 0.65 2/59 14674
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2002 0 0 0 56996 10 0 0 25 0 1 0 363433169 9932800 1980 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2425 1980 603 41 0 2384 0
vsize: 9700
[startup+580.009 s]
Raw data (loadavg): 0.99 0.95 0.65 2/59 14674
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2015 0 0 0 57996 10 0 0 25 0 1 0 363433169 9932800 1993 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2425 1993 603 41 0 2384 0
vsize: 9700
[startup+590.009 s]
Raw data (loadavg): 0.99 0.95 0.65 2/59 14674
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2015 0 0 0 58996 10 0 0 25 0 1 0 363433169 9932800 1993 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2425 1993 603 41 0 2384 0
vsize: 9700
[startup+600.01 s]
Raw data (loadavg): 0.99 0.95 0.66 2/59 14674
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2073 0 0 0 59996 10 0 0 25 0 1 0 363433169 10211328 2051 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2493 2051 603 41 0 2452 0
vsize: 9972
[startup+610.01 s]
Raw data (loadavg): 0.99 0.95 0.66 2/59 14674
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2073 0 0 0 60997 10 0 0 25 0 1 0 363433169 10211328 2051 4294967295 134512640 134672761 3221224576 3221223728 134560074 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2493 2051 603 41 0 2452 0
vsize: 9972
[startup+620.01 s]
Raw data (loadavg): 0.99 0.95 0.66 2/59 14674
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2079 0 0 0 61997 10 0 0 25 0 1 0 363433169 10211328 2057 4294967295 134512640 134672761 3221224576 3221223712 134565078 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2493 2057 603 41 0 2452 0
vsize: 9972
[startup+630.01 s]
Raw data (loadavg): 0.99 0.95 0.67 2/59 14674
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2079 0 0 0 62997 10 0 0 25 0 1 0 363433169 10211328 2057 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2493 2057 603 41 0 2452 0
vsize: 9972
[startup+640.011 s]
Raw data (loadavg): 0.99 0.95 0.67 2/59 14674
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2089 0 0 0 63997 11 0 0 25 0 1 0 363433169 10211328 2067 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2493 2067 603 41 0 2452 0
vsize: 9972
[startup+650.012 s]
Raw data (loadavg): 0.99 0.96 0.67 2/59 14674
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2095 0 0 0 64996 11 0 0 25 0 1 0 363433169 10350592 2073 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2527 2073 603 41 0 2486 0
vsize: 10108
[startup+660.012 s]
Raw data (loadavg): 0.99 0.96 0.67 2/59 14674
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2095 0 0 0 65996 12 0 0 25 0 1 0 363433169 10350592 2073 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2527 2073 603 41 0 2486 0
vsize: 10108
[startup+670.012 s]
Raw data (loadavg): 0.99 0.96 0.68 2/59 14674
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2158 0 0 0 66996 12 0 0 25 0 1 0 363433169 10481664 2136 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2559 2136 603 41 0 2518 0
vsize: 10236
[startup+680.012 s]
Raw data (loadavg): 0.99 0.96 0.68 2/59 14674
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2174 0 0 0 67996 12 0 0 25 0 1 0 363433169 10612736 2152 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2591 2152 603 41 0 2550 0
vsize: 10364
[startup+690.012 s]
Raw data (loadavg): 0.99 0.96 0.68 2/59 14674
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2180 0 0 0 68996 12 0 0 25 0 1 0 363433169 10612736 2158 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2591 2158 603 41 0 2550 0
vsize: 10364
[startup+700.012 s]
Raw data (loadavg): 0.99 0.96 0.69 2/59 14676
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2181 0 0 0 69996 13 0 0 25 0 1 0 363433169 10612736 2159 4294967295 134512640 134672761 3221224576 3221223760 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2591 2159 603 41 0 2550 0
vsize: 10364
[startup+710.014 s]
Raw data (loadavg): 0.99 0.96 0.69 2/59 14676
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2193 0 0 0 70996 13 0 0 25 0 1 0 363433169 10772480 2171 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2630 2171 603 41 0 2589 0
vsize: 10520
[startup+720.013 s]
Raw data (loadavg): 0.99 0.96 0.69 2/59 14676
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2345 0 0 0 71995 13 0 0 25 0 1 0 363433169 11300864 2323 4294967295 134512640 134672761 3221224576 3221223760 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2759 2323 603 41 0 2718 0
vsize: 11036
[startup+730.013 s]
Raw data (loadavg): 0.99 0.96 0.69 2/59 14676
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2346 0 0 0 72995 13 0 0 25 0 1 0 363433169 11300864 2324 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2759 2324 603 41 0 2718 0
vsize: 11036
[startup+740.013 s]
Raw data (loadavg): 0.99 0.96 0.70 2/59 14676
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2346 0 0 0 73995 13 0 0 25 0 1 0 363433169 11300864 2324 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2759 2324 603 41 0 2718 0
vsize: 11036
[startup+750.014 s]
Raw data (loadavg): 0.99 0.97 0.70 2/59 14676
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2346 0 0 0 74995 13 0 0 25 0 1 0 363433169 11300864 2324 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2759 2324 603 41 0 2718 0
vsize: 11036
[startup+760.014 s]
Raw data (loadavg): 0.99 0.97 0.70 2/59 14676
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2346 0 0 0 75995 13 0 0 25 0 1 0 363433169 11300864 2324 4294967295 134512640 134672761 3221224576 3221223680 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2759 2324 603 41 0 2718 0
vsize: 11036
[startup+770.014 s]
Raw data (loadavg): 0.99 0.97 0.71 2/59 14676
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2347 0 0 0 76995 14 0 0 25 0 1 0 363433169 11300864 2325 4294967295 134512640 134672761 3221224576 3221223680 134555211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2759 2325 603 41 0 2718 0
vsize: 11036
[startup+780.015 s]
Raw data (loadavg): 0.99 0.97 0.71 2/59 14676
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2347 0 0 0 77996 14 0 0 25 0 1 0 363433169 11296768 2325 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2758 2325 603 41 0 2717 0
vsize: 11032
[startup+790.014 s]
Raw data (loadavg): 0.99 0.97 0.71 2/59 14676
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2347 0 0 0 78995 14 0 0 25 0 1 0 363433169 11296768 2325 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2758 2325 603 41 0 2717 0
vsize: 11032
[startup+800.015 s]
Raw data (loadavg): 0.99 0.97 0.72 2/59 14676
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2348 0 0 0 79995 14 0 0 25 0 1 0 363433169 11296768 2326 4294967295 134512640 134672761 3221224576 3221223712 134565140 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2758 2326 603 41 0 2717 0
vsize: 11032
[startup+810.016 s]
Raw data (loadavg): 0.99 0.97 0.72 2/59 14676
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2348 0 0 0 80996 14 0 0 25 0 1 0 363433169 11296768 2326 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2758 2326 603 41 0 2717 0
vsize: 11032
[startup+820.015 s]
Raw data (loadavg): 0.99 0.97 0.72 2/59 14676
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2348 0 0 0 81996 14 0 0 25 0 1 0 363433169 11296768 2326 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2758 2326 603 41 0 2717 0
vsize: 11032
[startup+830.016 s]
Raw data (loadavg): 0.99 0.97 0.72 2/59 14676
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2348 0 0 0 82996 14 0 0 25 0 1 0 363433169 11296768 2326 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2758 2326 603 41 0 2717 0
vsize: 11032
[startup+840.015 s]
Raw data (loadavg): 0.99 0.97 0.73 2/59 14676
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2348 0 0 0 83996 14 0 0 25 0 1 0 363433169 11231232 2317 4294967295 134512640 134672761 3221224576 3221223744 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2742 2317 603 41 0 2701 0
vsize: 10968
[startup+850.016 s]
Raw data (loadavg): 0.99 0.97 0.73 2/59 14676
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2350 0 0 0 84996 14 0 0 25 0 1 0 363433169 11231232 2319 4294967295 134512640 134672761 3221224576 3221223744 134561148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2742 2319 603 41 0 2701 0
vsize: 10968
[startup+860.016 s]
Raw data (loadavg): 0.99 0.97 0.73 2/59 14676
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2350 0 0 0 85996 14 0 0 25 0 1 0 363433169 11231232 2319 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2742 2319 603 41 0 2701 0
vsize: 10968
[startup+870.015 s]
Raw data (loadavg): 0.99 0.97 0.73 2/59 14676
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2350 0 0 0 86997 14 0 0 25 0 1 0 363433169 11231232 2319 4294967295 134512640 134672761 3221224576 3221223744 134561226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2742 2319 603 41 0 2701 0
vsize: 10968
[startup+880.016 s]
Raw data (loadavg): 0.99 0.97 0.74 2/59 14676
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2352 0 0 0 87997 14 0 0 25 0 1 0 363433169 11231232 2321 4294967295 134512640 134672761 3221224576 3221223744 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2742 2321 603 41 0 2701 0
vsize: 10968
[startup+890.016 s]
Raw data (loadavg): 0.99 0.97 0.74 2/59 14676
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2352 0 0 0 88997 14 0 0 25 0 1 0 363433169 11231232 2321 4294967295 134512640 134672761 3221224576 3221223760 134559182 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2742 2321 603 41 0 2701 0
vsize: 10968
[startup+900.017 s]
Raw data (loadavg): 0.99 0.97 0.74 2/59 14676
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2352 0 0 0 89997 14 0 0 25 0 1 0 363433169 11231232 2321 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2742 2321 603 41 0 2701 0
vsize: 10968
[startup+910.016 s]
Raw data (loadavg): 0.99 0.97 0.74 2/59 14676
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2352 0 0 0 90997 14 0 0 25 0 1 0 363433169 11231232 2321 4294967295 134512640 134672761 3221224576 3221223712 134560596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2742 2321 603 41 0 2701 0
vsize: 10968
[startup+920.016 s]
Raw data (loadavg): 0.99 0.97 0.74 2/59 14676
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2352 0 0 0 91998 14 0 0 25 0 1 0 363433169 11231232 2321 4294967295 134512640 134672761 3221224576 3221223744 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2742 2321 603 41 0 2701 0
vsize: 10968
[startup+930.016 s]
Raw data (loadavg): 0.99 0.97 0.75 2/59 14676
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2352 0 0 0 92998 14 0 0 25 0 1 0 363433169 11231232 2321 4294967295 134512640 134672761 3221224576 3221223680 134554636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2742 2321 603 41 0 2701 0
vsize: 10968
[startup+940.016 s]
Raw data (loadavg): 0.99 0.97 0.75 2/59 14676
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2352 0 0 0 93998 14 0 0 25 0 1 0 363433169 11231232 2321 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2742 2321 603 41 0 2701 0
vsize: 10968
[startup+950.017 s]
Raw data (loadavg): 0.99 0.97 0.75 2/59 14676
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2352 0 0 0 94998 14 0 0 25 0 1 0 363433169 11231232 2321 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2742 2321 603 41 0 2701 0
vsize: 10968
[startup+960.016 s]
Raw data (loadavg): 0.99 0.97 0.75 2/59 14676
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2352 0 0 0 95998 14 0 0 25 0 1 0 363433169 11231232 2321 4294967295 134512640 134672761 3221224576 3221223776 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2742 2321 603 41 0 2701 0
vsize: 10968
[startup+970.016 s]
Raw data (loadavg): 0.99 0.97 0.75 2/59 14676
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2357 0 0 0 96998 14 0 0 25 0 1 0 363433169 11395072 2326 4294967295 134512640 134672761 3221224576 3221223744 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2782 2326 603 41 0 2741 0
vsize: 11128
[startup+972.132 s]
Raw data (loadavg): 0.99 0.97 0.75 1/58 14676
Raw data (stat): 14670 (minisat+) R 14669 12452 12451 0 -1 0 2357 0 0 0 96998 14 0 0 25 0 1 0 363433169 11395072 2326 4294967295 134512640 134672761 3221224576 3221223744 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2782 2326 603 41 0 2741 0
vsize: 0

Child status: 30
Real time (s): 972.132
CPU time (s): 972.248
CPU user time (s): 972.096
CPU system time (s): 0.151976
CPU usage (%): 100.012
Max. virtual memory (Kb): 11128
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	15
#### END VERIFIER DATA ####