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/primes-dimacs-cnf/normalized-jnh201.opb
MD5SUM	ba509931ad93c2223be235a06a9b3100
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	84
Optimality of the best value was proved	NO
Number of terms in the objective function	200
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	200
Number of bits of the sum of numbers in the objective function	8
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	200
Number of bits of the biggest sum of numbers	8
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.01884
Number of variables	200
Total number of constraints	900
Number of constraints which are clauses	900
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	14

Trace number 6227

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-04-14 04:07:50 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4692 boxname=wulflinc10 idbench=180 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ba509931ad93c2223be235a06a9b3100  /oldhome/oroussel/tmp/wulflinc10/normalized-jnh201.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc10/normalized-jnh201.opb /oldhome/oroussel/tmp/wulflinc10/normalized-jnh201.opb
IDLAUNCH: 4692
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        859864 kB
Buffers:         35592 kB
Cached:         119692 kB
SwapCached:        164 kB
Active:          54824 kB
Inactive:       103408 kB
HighTotal:      131008 kB
HighFree:         7784 kB
LowTotal:       903652 kB
LowFree:        852080 kB
SwapTotal:     2097136 kB
SwapFree:      2096972 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            10980 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 04:12:10 (client local time) WITH STATUS 30 IN 259.397 SECONDS
stats: 4692 0 259.397 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 900 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 |     900     4354 |     300       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 91[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 5812     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         7 |   14359    35879 |    4786       7       55     7.9 |  0.000 % |
c ==============================================================================
c [1mFound solution: 90[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        13 |   14323    35801 |    4774      13      297    22.8 |  0.000 % |
c ==============================================================================
c [1mFound solution: 89[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       110 |   14404    36009 |    4801     110     5259    47.8 |  0.000 % |
c |       211 |   14404    36009 |    5281     211     9743    46.2 |  0.236 % |
c |       361 |   14377    35949 |    5809     360    12963    36.0 |  0.387 % |
c ==============================================================================
c [1mFound solution: 88[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       510 |   14326    35831 |    4775     506    19122    37.8 |  0.387 % |
c |       610 |   14096    35161 |    5252     604    20445    33.8 |  1.847 % |
c |       760 |   14096    35161 |    5777     754    24312    32.2 |  1.847 % |
c |       985 |   14096    35161 |    6355     979    27829    28.4 |  1.847 % |
c |      1324 |   14096    35161 |    6991    1318    46010    34.9 |  1.847 % |
c |      1830 |   13917    34756 |    7690    1821    59037    32.4 |  2.921 % |
c |      2589 |   13707    34280 |    8459    2575    83671    32.5 |  4.210 % |
c |      3734 |   13658    34170 |    9305    3719   135661    36.5 |  4.488 % |
c |      5444 |   12925    32494 |   10235    5418   204408    37.7 |  9.234 % |
c |      8007 |   12273    31000 |   11259    7971   318681    40.0 | 13.528 % |
c |     11851 |   10965    28009 |   12385   11772   484704    41.2 | 22.031 % |
c ==============================================================================
c [1mFound solution: 87[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 5014     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11933 |   19570    47999 |    6523   11854   488385    41.2 | 22.031 % |
c |     12033 |   19348    47495 |    7175    6025   228417    37.9 | 22.301 % |
c |     12183 |   19348    47495 |    7892    6175   232170    37.6 | 22.301 % |
c |     12409 |   19348    47495 |    8682    6401   241317    37.7 | 22.301 % |
c |     12750 |   19348    47495 |    9550    6742   256439    38.0 | 22.301 % |
c |     13257 |   19098    46930 |   10505    7247   268888    37.1 | 23.249 % |
c |     14016 |   18962    46624 |   11555    8005   298535    37.3 | 23.740 % |
c |     15156 |   18019    44484 |   12711    9135   343130    37.6 | 27.256 % |
c |     16867 |   17607    43550 |   13982   10843   421590    38.9 | 28.803 % |
c |     19430 |   17323    42904 |   15380   13403   534698    39.9 | 29.882 % |
c |     23274 |   16552    41137 |   16918   17241   701306    40.7 | 32.810 % |
c |     29043 |   15842    39509 |   18610   12980   529774    40.8 | 35.533 % |
c ==============================================================================
c [1mFound solution: 86[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35570 |   15327    38332 |    5109   19504   881771    45.2 | 35.533 % |
c |     35672 |   15058    37712 |    5619    4976   207164    41.6 | 38.475 % |
c |     35823 |   15058    37712 |    6181    5127   213713    41.7 | 38.475 % |
c |     36050 |   14919    37390 |    6800    5353   224733    42.0 | 39.038 % |
c |     36387 |   14919    37390 |    7480    5690   234518    41.2 | 39.038 % |
c |     36896 |   14919    37390 |    8228    6199   258814    41.8 | 39.039 % |
c |     37655 |   14757    37016 |    9050    6955   289491    41.6 | 39.650 % |
c |     38794 |   14757    37016 |    9955    8094   333162    41.2 | 39.650 % |
c |     40503 |   14589    36628 |   10951    9802   396377    40.4 | 40.274 % |
c |     43065 |   14589    36628 |   12046   12364   513180    41.5 | 40.274 % |
c |     46909 |   14451    36307 |   13251   16207   682725    42.1 | 40.789 % |
c |     52676 |   14113    35529 |   14576   13279   549002    41.3 | 42.048 % |
c |     61326 |   13929    35106 |   16034   12089   486078    40.2 | 42.684 % |
c |     74300 |   12303    31353 |   17637   14400   645924    44.9 | 48.753 % |
c |     93761 |   12089    30732 |   19401   13300   556530    41.8 | 49.376 % |
c ==============================================================================
c [1mFound solution: 85[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 3768     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    117156 |   15645    38878 |    5215   24286   952744    39.2 | 49.376 % |
c |    117256 |   15645    38878 |    5736    6172   206258    33.4 | 49.293 % |
c |    117406 |   15645    38878 |    6310    6322   211570    33.5 | 49.293 % |
c |    117631 |   15645    38878 |    6941    6547   220002    33.6 | 49.293 % |
c |    117968 |   15645    38878 |    7635    6884   232999    33.8 | 49.293 % |
c |    118474 |   15645    38878 |    8398    7390   259020    35.1 | 49.293 % |
c |    119235 |   15645    38878 |    9238    8151   297873    36.5 | 49.293 % |
c |    120375 |   15406    38326 |   10162    9290   346210    37.3 | 49.931 % |
c ==============================================================================
c [1mFound solution: 84[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    121330 |   15383    38276 |    5127   10245   398692    38.9 | 49.931 % |
c |    121432 |   15383    38276 |    5639   10347   403040    39.0 | 49.986 % |
c |    121582 |   15383    38276 |    6203   10497   410252    39.1 | 49.986 % |
c |    121807 |   15383    38276 |    6824   10722   420841    39.3 | 49.986 % |
c |    122144 |   15383    38276 |    7506   11059   436809    39.5 | 49.986 % |
c |    122651 |   15383    38276 |    8257   11566   459384    39.7 | 49.986 % |
c |    123414 |   15383    38276 |    9082   12329   491997    39.9 | 49.986 % |
c |    124554 |   15383    38276 |    9991   13469   530799    39.4 | 49.986 % |
c |    126262 |   15383    38276 |   10990   15177   601683    39.6 | 49.986 % |
c |    128824 |   15383    38276 |   12089    8975   287295    32.0 | 49.986 % |
c |    132668 |   15383    38276 |   13298   12819   443058    34.6 | 49.986 % |
c |    138435 |   15383    38276 |   14627   18586   661164    35.6 | 49.986 % |
c ==============================================================================
c [1mOptimal solution: 84[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
c _______________________________________________________________________________
c 
c restarts              : 64
c conflicts             : 145267         (560 /sec)
c decisions             : 220071         (849 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 259.284 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.98 0.91 2/54 1412
Raw data (stat): 1412 (runsolver) R 1411 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423374517 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+9.99933 s]
Raw data (loadavg): 0.93 0.98 0.91 2/54 1412
Raw data (stat): 1412 (minisat+) R 1411 25347 25346 0 -1 0 1144 0 0 0 994 3 0 0 25 0 1 0 423374517 6410240 1121 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1565 1121 603 41 0 1524 0
vsize: 6260
[startup+19.9997 s]
Raw data (loadavg): 0.94 0.98 0.91 2/54 1412
Raw data (stat): 1412 (minisat+) R 1411 25347 25346 0 -1 0 1613 0 0 0 1992 5 0 0 25 0 1 0 423374517 8605696 1587 4294967295 134512640 134672761 3221224576 3221223712 134560619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2101 1587 603 41 0 2060 0
vsize: 8404
[startup+29.9997 s]
Raw data (loadavg): 0.95 0.98 0.91 2/54 1412
Raw data (stat): 1412 (minisat+) R 1411 25347 25346 0 -1 0 1739 0 0 0 2991 6 0 0 25 0 1 0 423374517 9138176 1713 4294967295 134512640 134672761 3221224576 3221223744 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2231 1713 603 41 0 2190 0
vsize: 8924
[startup+39.9997 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 1412
Raw data (stat): 1412 (minisat+) R 1411 25347 25346 0 -1 0 2033 0 0 0 3990 7 0 0 25 0 1 0 423374517 10334208 2007 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2523 2007 603 41 0 2482 0
vsize: 10092
[startup+49.9992 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 1412
Raw data (stat): 1412 (minisat+) R 1411 25347 25346 0 -1 0 2060 0 0 0 4990 7 0 0 25 0 1 0 423374517 10469376 2034 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2556 2034 603 41 0 2515 0
vsize: 10224
[startup+59.9994 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 1412
Raw data (stat): 1412 (minisat+) R 1411 25347 25346 0 -1 0 2167 0 0 0 5989 7 0 0 25 0 1 0 423374517 10870784 2141 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2654 2141 603 41 0 2613 0
vsize: 10616
[startup+69.9997 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 1412
Raw data (stat): 1412 (minisat+) R 1411 25347 25346 0 -1 0 2167 0 0 0 6989 8 0 0 25 0 1 0 423374517 10870784 2141 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2654 2141 603 41 0 2613 0
vsize: 10616
[startup+79.9999 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 1412
Raw data (stat): 1412 (minisat+) R 1411 25347 25346 0 -1 0 2170 0 0 0 7989 8 0 0 25 0 1 0 423374517 11018240 2144 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2690 2144 603 41 0 2649 0
vsize: 10760
[startup+89.9998 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 1412
Raw data (stat): 1412 (minisat+) R 1411 25347 25346 0 -1 0 2177 0 0 0 8989 8 0 0 25 0 1 0 423374517 11018240 2151 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2690 2151 603 41 0 2649 0
vsize: 10760
[startup+99.9991 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 1412
Raw data (stat): 1412 (minisat+) R 1411 25347 25346 0 -1 0 2185 0 0 0 9989 8 0 0 25 0 1 0 423374517 11018240 2159 4294967295 134512640 134672761 3221224576 3221223720 134560553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2690 2159 603 41 0 2649 0
vsize: 10760
[startup+109.999 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 1412
Raw data (stat): 1412 (minisat+) R 1411 25347 25346 0 -1 0 2195 0 0 0 10990 8 0 0 25 0 1 0 423374517 11018240 2169 4294967295 134512640 134672761 3221224576 3221223744 134559126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2690 2169 603 41 0 2649 0
vsize: 10760
[startup+119.999 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1412
Raw data (stat): 1412 (minisat+) R 1411 25347 25346 0 -1 0 2268 0 0 0 11989 8 0 0 25 0 1 0 423374517 11419648 2242 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2788 2242 603 41 0 2747 0
vsize: 11152
[startup+129.999 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1412
Raw data (stat): 1412 (minisat+) R 1411 25347 25346 0 -1 0 2271 0 0 0 12989 8 0 0 25 0 1 0 423374517 11419648 2245 4294967295 134512640 134672761 3221224576 3221223712 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2788 2245 603 41 0 2747 0
vsize: 11152
[startup+139.999 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1412
Raw data (stat): 1412 (minisat+) R 1411 25347 25346 0 -1 0 2374 0 0 0 13989 9 0 0 25 0 1 0 423374517 11816960 2348 4294967295 134512640 134672761 3221224576 3221223680 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2885 2348 603 41 0 2844 0
vsize: 11540
[startup+149.999 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1412
Raw data (stat): 1412 (minisat+) R 1411 25347 25346 0 -1 0 2380 0 0 0 14989 9 0 0 25 0 1 0 423374517 11816960 2354 4294967295 134512640 134672761 3221224576 3221223712 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2885 2354 603 41 0 2844 0
vsize: 11540
[startup+159.998 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1412
Raw data (stat): 1412 (minisat+) R 1411 25347 25346 0 -1 0 2380 0 0 0 15989 9 0 0 25 0 1 0 423374517 11816960 2354 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2885 2354 603 41 0 2844 0
vsize: 11540
[startup+169.998 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1412
Raw data (stat): 1412 (minisat+) R 1411 25347 25346 0 -1 0 2380 0 0 0 16990 9 0 0 25 0 1 0 423374517 11816960 2354 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2885 2354 603 41 0 2844 0
vsize: 11540
[startup+179.998 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1412
Raw data (stat): 1412 (minisat+) R 1411 25347 25346 0 -1 0 2411 0 0 0 17989 9 0 0 25 0 1 0 423374517 11948032 2385 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2917 2385 603 41 0 2876 0
vsize: 11668
[startup+189.998 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1412
Raw data (stat): 1412 (minisat+) R 1411 25347 25346 0 -1 0 2453 0 0 0 18990 9 0 0 25 0 1 0 423374517 12083200 2427 4294967295 134512640 134672761 3221224576 3221223776 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2950 2427 603 41 0 2909 0
vsize: 11800
[startup+199.998 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1412
Raw data (stat): 1412 (minisat+) R 1411 25347 25346 0 -1 0 2456 0 0 0 19990 9 0 0 25 0 1 0 423374517 12083200 2430 4294967295 134512640 134672761 3221224576 3221223760 134559019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2950 2430 603 41 0 2909 0
vsize: 11800
[startup+209.998 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1412
Raw data (stat): 1412 (minisat+) R 1411 25347 25346 0 -1 0 2513 0 0 0 20990 9 0 0 25 0 1 0 423374517 12275712 2487 4294967295 134512640 134672761 3221224576 3221223680 134554910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2997 2487 603 41 0 2956 0
vsize: 11988
[startup+219.998 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1412
Raw data (stat): 1412 (minisat+) R 1411 25347 25346 0 -1 0 2519 0 0 0 21990 9 0 0 25 0 1 0 423374517 12275712 2493 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2997 2493 603 41 0 2956 0
vsize: 11988
[startup+229.997 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1412
Raw data (stat): 1412 (minisat+) R 1411 25347 25346 0 -1 0 2519 0 0 0 22990 9 0 0 25 0 1 0 423374517 12275712 2493 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2997 2493 603 41 0 2956 0
vsize: 11988
[startup+239.997 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1412
Raw data (stat): 1412 (minisat+) R 1411 25347 25346 0 -1 0 2530 0 0 0 23990 10 0 0 25 0 1 0 423374517 12275712 2504 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2997 2504 603 41 0 2956 0
vsize: 11988
[startup+249.997 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1412
Raw data (stat): 1412 (minisat+) R 1411 25347 25346 0 -1 0 2531 0 0 0 24990 10 0 0 25 0 1 0 423374517 12275712 2505 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2997 2505 603 41 0 2956 0
vsize: 11988
[startup+259.384 s]
Raw data (loadavg): 0.99 0.98 0.91 1/53 1412
Raw data (stat): 1412 (minisat+) R 1411 25347 25346 0 -1 0 2531 0 0 0 24990 10 0 0 25 0 1 0 423374517 12275712 2505 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2997 2505 603 41 0 2956 0
vsize: 0

Child status: 30
Real time (s): 259.384
CPU time (s): 259.397
CPU user time (s): 259.289
CPU system time (s): 0.107983
CPU usage (%): 100.005
Max. virtual memory (Kb): 11988
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	84
#### END VERIFIER DATA ####