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/een/normalized-mod008.opb
MD5SUM	18b325bb9311c83b0604c703bacc9a29
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	87
Optimality of the best value was proved	NO
Number of terms in the objective function	319
Biggest coefficient in the objective function	87
Number of bits for the biggest coefficient in the objective function	7
Sum of the numbers in the objective function	23554
Number of bits of the sum of numbers in the objective function	15
Biggest number in a constraint	7499
Number of bits of the biggest number in a constraint	13
Biggest sum of numbers in a constraint	758444
Number of bits of the biggest sum of numbers	20
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.283956
Number of variables	319
Total number of constraints	6
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	6
Minimum length of a constraint	186
Maximum length of a constraint	231
Trace number 7040

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-04-14 21:13:47 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=5140 boxname=wulflinc8 idbench=396 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  18b325bb9311c83b0604c703bacc9a29  /oldhome/oroussel/tmp/wulflinc8/normalized-mod008.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc8/normalized-mod008.opb
IDLAUNCH: 5140
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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.007
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:        860132 kB
Buffers:         38000 kB
Cached:         114864 kB
SwapCached:          0 kB
Active:          82388 kB
Inactive:        75140 kB
HighTotal:      131008 kB
HighFree:        10472 kB
LowTotal:       903652 kB
LowFree:        849660 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6932 kB
Slab:            11420 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 21:18:46 (client local time) WITH STATUS 30 IN 298.834 SECONDS
stats: 5140 0 298.834 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 6 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): sss.ss
c ---[   4]---> BDD-cost:  105
c ---[   3]---> BDD-cost:  168
c ---[   2]---> BDD-cost:  223
c ---[   1]---> Sorter-cost:  663     Base: 3
c ---[   0]---> Sorter-cost:  354     Base: 11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    2343     7303 |     781       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 5168[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:61666     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  154168   361839 |   51389       0        0     nan |  0.000 % |
c |       100 |  154168   361839 |   56527     100     2722    27.2 |  0.010 % |
c |       251 |  154168   361839 |   62180     251     3681    14.7 |  0.010 % |
c |       476 |  154168   361839 |   68398     476     5996    12.6 |  0.010 % |
c |       813 |  154168   361839 |   75238     813     9022    11.1 |  0.010 % |
c |      1320 |  154168   361839 |   82762    1320    12443     9.4 |  0.010 % |
c |      2080 |  154168   361839 |   91038    2080    19782     9.5 |  0.010 % |
c |      3219 |  154168   361839 |  100142    3219    41866    13.0 |  0.010 % |
c |      4927 |  154168   361839 |  110156    4927   112116    22.8 |  0.010 % |
c |      7490 |  154168   361839 |  121172    7490   196497    26.2 |  0.010 % |
c |     11334 |  154168   361839 |  133289   11334   343852    30.3 |  0.010 % |
c |     17100 |  154168   361839 |  146618   17100   487358    28.5 |  0.010 % |
c |     25749 |  154168   361839 |  161280   25749   739274    28.7 |  0.010 % |
c |     38723 |  154168   361839 |  177408   38723  1026536    26.5 |  0.010 % |
c ==============================================================================
c [1mFound solution: 5022[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     54752 |  154816   363656 |   51605   54752  1846349    33.7 |  0.010 % |
c |     54853 |  154816   363656 |   56765   21468   689854    32.1 |  0.012 % |
c |     55005 |  154816   363656 |   62442   21620   691245    32.0 |  0.012 % |
c |     55230 |  154816   363656 |   68686   21845   694971    31.8 |  0.012 % |
c ==============================================================================
c [1mFound solution: 2454[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     55260 |  155438   365156 |   51812   21875   695367    31.8 |  0.012 % |
c |     55360 |  155438   365156 |   56993   21975   696308    31.7 |  0.014 % |
c |     55510 |  155438   365156 |   62692   22125   697000    31.5 |  0.014 % |
c |     55736 |  155438   365156 |   68961   22351   698705    31.3 |  0.014 % |
c |     56073 |  155438   365156 |   75857   22688   702973    31.0 |  0.014 % |
c ==============================================================================
c [1mFound solution: 1174[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     56099 |  155523   365350 |   51841   22714   703251    31.0 |  0.014 % |
c |     56199 |  155523   365350 |   57025   22814   704113    30.9 |  0.015 % |
c |     56349 |  155523   365350 |   62727   22964   704965    30.7 |  0.015 % |
c ==============================================================================
c [1mFound solution: 1103[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     56382 |  155534   365379 |   51844   22997   705193    30.7 |  0.015 % |
c ==============================================================================
c [1mFound solution: 783[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     56429 |  155576   365479 |   51858   23044   706962    30.7 |  0.015 % |
c |     56529 |  155576   365479 |   57043   23144   718459    31.0 |  0.019 % |
c |     56679 |  155576   365479 |   62748   23294   719954    30.9 |  0.019 % |
c |     56904 |  155576   365479 |   69022   23519   725291    30.8 |  0.019 % |
c |     57242 |  155576   365479 |   75925   23857   736617    30.9 |  0.019 % |
c |     57748 |  155576   365479 |   83517   24363   748400    30.7 |  0.019 % |
c |     58507 |  155464   365227 |   91869   25092   767926    30.6 |  0.068 % |
c |     59648 |  155464   365227 |  101056   26233   803999    30.6 |  0.068 % |
c |     61356 |  155306   364872 |  111162   27771   850938    30.6 |  0.139 % |
c |     63918 |  155306   364872 |  122278   30333  1045528    34.5 |  0.139 % |
c ==============================================================================
c [1mFound solution: 405[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     67360 |  155339   364948 |   51779   33775  1384421    41.0 |  0.139 % |
c |     67460 |  155049   364289 |   56956   33604  1396660    41.6 |  0.274 % |
c ==============================================================================
c [1mFound solution: 340[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     67527 |  155058   364310 |   51686   33671  1398574    41.5 |  0.274 % |
c ==============================================================================
c [1mFound solution: 336[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     67534 |  155524   365446 |   51841   33678  1398617    41.5 |  0.274 % |
c ==============================================================================
c [1mFound solution: 257[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     67552 |  155543   365591 |   51847   33696  1399200    41.5 |  0.274 % |
c ==============================================================================
c [1mFound solution: 255[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     67555 |  155547   365601 |   51849   33699  1399393    41.5 |  0.274 % |
c ==============================================================================
c [1mFound solution: 229[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     67580 |  155555   365721 |   51851   33724  1405663    41.7 |  0.274 % |
c |     67681 |  155555   365721 |   57036   33825  1415943    41.9 |  0.281 % |
c ==============================================================================
c [1mFound solution: 219[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     67820 |  155560   365732 |   51853   33964  1419436    41.8 |  0.281 % |
c |     67921 |  155560   365732 |   57038   34065  1422119    41.7 |  0.283 % |
c |     68071 |  155560   365732 |   62742   34215  1426538    41.7 |  0.283 % |
c |     68296 |  154427   363155 |   69016   34180  1439202    42.1 |  0.834 % |
c ==============================================================================
c [1mFound solution: 215[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     68494 |  154240   362731 |   51413   34356  1493399    43.5 |  0.834 % |
c |     68594 |  154240   362731 |   56554   34456  1499411    43.5 |  0.933 % |
c |     68746 |  154186   362609 |   62209   34594  1502948    43.4 |  0.956 % |
c ==============================================================================
c [1mFound solution: 199[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     68835 |  154193   362626 |   51397   34683  1509788    43.5 |  0.956 % |
c ==============================================================================
c [1mFound solution: 170[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:  966
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     68873 |  156670   369375 |   52223   34721  1510739    43.5 |  0.956 % |
c ==============================================================================
c [1mFound solution: 87[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   44
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     68888 |  150465   355053 |   50155   33182  1453993    43.8 |  0.956 % |
c |     68990 |  150465   355053 |   55170   33284  1460253    43.9 |  4.207 % |
c |     69159 |  147342   347856 |   60687   32775  1500930    45.8 |  5.821 % |
c |     69384 |  147342   347856 |   66756   33000  1542408    46.7 |  5.821 % |
c |     69734 |  147267   347682 |   73431   33337  1583607    47.5 |  5.863 % |
c ==============================================================================
c [1mOptimal solution: 87[0m
s OPTIMUM FOUND
v -x0 -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
c _______________________________________________________________________________
c 
c restarts              : 60
c conflicts             : 69884          (234 /sec)
c decisions             : 242195         (811 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 298.61 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.92 0.97 0.89 2/54 5803
Raw data (stat): 5803 (runsolver) R 5802 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 415959435 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.97 0.89 2/54 5803
Raw data (stat): 5803 (minisat+) R 5802 26667 26666 0 -1 0 5231 0 0 0 987 11 0 0 25 0 1 0 415959435 23396352 5000 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5712 5000 603 41 0 5671 0
vsize: 22848
[startup+20.0005 s]
Raw data (loadavg): 0.94 0.97 0.89 2/54 5803
Raw data (stat): 5803 (minisat+) R 5802 26667 26666 0 -1 0 5355 0 0 0 1986 11 0 0 25 0 1 0 415959435 23859200 5124 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5825 5124 603 41 0 5784 0
vsize: 23300
[startup+30.0012 s]
Raw data (loadavg): 0.95 0.97 0.89 2/54 5803
Raw data (stat): 5803 (minisat+) R 5802 26667 26666 0 -1 0 5547 0 0 0 2986 12 0 0 25 0 1 0 415959435 24666112 5316 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6022 5316 603 41 0 5981 0
vsize: 24088
[startup+40.0007 s]
Raw data (loadavg): 0.96 0.97 0.90 2/54 5803
Raw data (stat): 5803 (minisat+) R 5802 26667 26666 0 -1 0 5673 0 0 0 3986 12 0 0 25 0 1 0 415959435 25174016 5442 4294967295 134512640 134672761 3221224640 3221223808 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6146 5442 603 41 0 6105 0
vsize: 24584
[startup+50.0008 s]
Raw data (loadavg): 0.96 0.97 0.90 2/54 5803
Raw data (stat): 5803 (minisat+) R 5802 26667 26666 0 -1 0 5867 0 0 0 4986 13 0 0 25 0 1 0 415959435 25964544 5636 4294967295 134512640 134672761 3221224640 3221223824 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6339 5636 603 41 0 6298 0
vsize: 25356
[startup+60.0018 s]
Raw data (loadavg): 0.97 0.97 0.90 2/54 5803
Raw data (stat): 5803 (minisat+) R 5802 26667 26666 0 -1 0 6043 0 0 0 5985 13 0 0 25 0 1 0 415959435 26632192 5812 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6502 5812 603 41 0 6461 0
vsize: 26008
[startup+70.002 s]
Raw data (loadavg): 0.97 0.97 0.90 2/54 5803
Raw data (stat): 5803 (minisat+) R 5802 26667 26666 0 -1 0 6223 0 0 0 6984 14 0 0 25 0 1 0 415959435 27566080 5992 4294967295 134512640 134672761 3221224640 3221223808 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6730 5992 603 41 0 6689 0
vsize: 26920
[startup+80.0031 s]
Raw data (loadavg): 0.98 0.97 0.90 2/54 5803
Raw data (stat): 5803 (minisat+) R 5802 26667 26666 0 -1 0 6373 0 0 0 7983 15 0 0 25 0 1 0 415959435 28102656 6142 4294967295 134512640 134672761 3221224640 3221223656 1075352688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6861 6142 603 41 0 6820 0
vsize: 27444
[startup+90.0029 s]
Raw data (loadavg): 0.98 0.97 0.90 2/54 5803
Raw data (stat): 5803 (minisat+) R 5802 26667 26666 0 -1 0 6486 0 0 0 8983 15 0 0 25 0 1 0 415959435 28639232 6255 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6992 6255 603 41 0 6951 0
vsize: 27968
[startup+100.002 s]
Raw data (loadavg): 0.98 0.97 0.90 2/54 5803
Raw data (stat): 5803 (minisat+) R 5802 26667 26666 0 -1 0 6711 0 0 0 9983 16 0 0 25 0 1 0 415959435 29446144 6480 4294967295 134512640 134672761 3221224640 3221223808 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7189 6480 603 41 0 7148 0
vsize: 28756
[startup+110.003 s]
Raw data (loadavg): 0.98 0.97 0.90 2/54 5803
Raw data (stat): 5803 (minisat+) R 5802 26667 26666 0 -1 0 6858 0 0 0 10983 16 0 0 25 0 1 0 415959435 30117888 6627 4294967295 134512640 134672761 3221224640 3221223776 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7353 6627 603 41 0 7312 0
vsize: 29412
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 5803
Raw data (stat): 5803 (minisat+) R 5802 26667 26666 0 -1 0 7178 0 0 0 11982 17 0 0 25 0 1 0 415959435 31334400 6947 4294967295 134512640 134672761 3221224640 3221223744 134560355 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7650 6947 603 41 0 7609 0
vsize: 30600
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 5803
Raw data (stat): 5803 (minisat+) R 5802 26667 26666 0 -1 0 7459 0 0 0 12982 17 0 0 25 0 1 0 415959435 33370112 7228 4294967295 134512640 134672761 3221224640 3221223940 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8147 7228 603 41 0 8106 0
vsize: 32588
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5803
Raw data (stat): 5803 (minisat+) R 5802 26667 26666 0 -1 0 7501 0 0 0 13982 17 0 0 25 0 1 0 415959435 33370112 7228 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8147 7228 603 41 0 8106 0
vsize: 32588
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5803
Raw data (stat): 5803 (minisat+) R 5802 26667 26666 0 -1 0 7501 0 0 0 14982 17 0 0 25 0 1 0 415959435 33370112 7228 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8147 7228 603 41 0 8106 0
vsize: 32588
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5803
Raw data (stat): 5803 (minisat+) R 5802 26667 26666 0 -1 0 7502 0 0 0 15982 17 0 0 25 0 1 0 415959435 33370112 7229 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8147 7229 603 41 0 8106 0
vsize: 32588
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5803
Raw data (stat): 5803 (minisat+) R 5802 26667 26666 0 -1 0 7523 0 0 0 16982 17 0 0 25 0 1 0 415959435 33570816 7250 4294967295 134512640 134672761 3221224640 3221223808 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8196 7250 603 41 0 8155 0
vsize: 32784
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5803
Raw data (stat): 5803 (minisat+) R 5802 26667 26666 0 -1 0 7523 0 0 0 17983 17 0 0 25 0 1 0 415959435 33570816 7250 4294967295 134512640 134672761 3221224640 3221223788 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8196 7250 603 41 0 8155 0
vsize: 32784
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5803
Raw data (stat): 5803 (minisat+) R 5802 26667 26666 0 -1 0 7523 0 0 0 18983 17 0 0 25 0 1 0 415959435 33570816 7250 4294967295 134512640 134672761 3221224640 3221223808 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8196 7250 603 41 0 8155 0
vsize: 32784
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5803
Raw data (stat): 5803 (minisat+) R 5802 26667 26666 0 -1 0 7523 0 0 0 19983 17 0 0 25 0 1 0 415959435 33570816 7250 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8196 7250 603 41 0 8155 0
vsize: 32784
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5803
Raw data (stat): 5803 (minisat+) R 5802 26667 26666 0 -1 0 7523 0 0 0 20982 18 0 0 25 0 1 0 415959435 33570816 7250 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8196 7250 603 41 0 8155 0
vsize: 32784
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5803
Raw data (stat): 5803 (minisat+) R 5802 26667 26666 0 -1 0 7523 0 0 0 21983 18 0 0 25 0 1 0 415959435 33570816 7250 4294967295 134512640 134672761 3221224640 3221223824 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8196 7250 603 41 0 8155 0
vsize: 32784
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5803
Raw data (stat): 5803 (minisat+) R 5802 26667 26666 0 -1 0 7523 0 0 0 22983 18 0 0 25 0 1 0 415959435 33570816 7250 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8196 7250 603 41 0 8155 0
vsize: 32784
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5803
Raw data (stat): 5803 (minisat+) R 5802 26667 26666 0 -1 0 7523 0 0 0 23983 18 0 0 25 0 1 0 415959435 33570816 7250 4294967295 134512640 134672761 3221224640 3221223808 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8196 7250 603 41 0 8155 0
vsize: 32784
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5803
Raw data (stat): 5803 (minisat+) R 5802 26667 26666 0 -1 0 7523 0 0 0 24983 18 0 0 25 0 1 0 415959435 33570816 7250 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8196 7250 603 41 0 8155 0
vsize: 32784
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5803
Raw data (stat): 5803 (minisat+) R 5802 26667 26666 0 -1 0 7693 0 0 0 25983 18 0 0 25 0 1 0 415959435 33570816 7252 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8196 7252 603 41 0 8155 0
vsize: 32784
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5803
Raw data (stat): 5803 (minisat+) R 5802 26667 26666 0 -1 0 7693 0 0 0 26983 18 0 0 25 0 1 0 415959435 33570816 7252 4294967295 134512640 134672761 3221224640 3221223808 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8196 7252 603 41 0 8155 0
vsize: 32784
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5803
Raw data (stat): 5803 (minisat+) R 5802 26667 26666 0 -1 0 7776 0 0 0 27983 18 0 0 25 0 1 0 415959435 33644544 7293 4294967295 134512640 134672761 3221224640 3221223744 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8214 7293 603 41 0 8173 0
vsize: 32856
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5803
Raw data (stat): 5803 (minisat+) R 5802 26667 26666 0 -1 0 7777 0 0 0 28983 18 0 0 25 0 1 0 415959435 33644544 7294 4294967295 134512640 134672761 3221224640 3221223808 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8214 7294 603 41 0 8173 0
vsize: 32856
[startup+298.818 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 5803
Raw data (stat): 5803 (minisat+) R 5802 26667 26666 0 -1 0 7777 0 0 0 28983 18 0 0 25 0 1 0 415959435 33644544 7294 4294967295 134512640 134672761 3221224640 3221223808 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8214 7294 603 41 0 8173 0
vsize: 0

Child status: 30
Real time (s): 298.817
CPU time (s): 298.834
CPU user time (s): 298.628
CPU system time (s): 0.205968
CPU usage (%): 100.005
Max. virtual memory (Kb): 32856
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	87
#### END VERIFIER DATA ####