PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:

LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-bk4x3.opb
MD5SUM	c2339539ffa69702e62053614fe34ce1
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	44800
Optimality of the best value was proved	NO
Number of terms in the objective function	252
Biggest coefficient in the objective function	2621440
Number of bits for the biggest coefficient in the objective function	22
Sum of the numbers in the objective function	35682270
Number of bits of the sum of numbers in the objective function	26
Biggest number in a constraint	2621440
Number of bits of the biggest number in a constraint	22
Biggest sum of numbers in a constraint	35682270
Number of bits of the biggest sum of numbers	26
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	24.1133
Number of variables	252
Total number of constraints	19
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	19
Minimum length of a constraint	21
Maximum length of a constraint	80

Trace number 14858

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc22 THE 2005-04-21 02:10:45 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18972 boxname=wulflinc22 idbench=1460 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  c2339539ffa69702e62053614fe34ce1  /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-bk4x3.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-bk4x3.opb
IDLAUNCH: 18972
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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	: 3
cpu MHz		: 451.031
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:        815036 kB
Buffers:         19040 kB
Cached:         170452 kB
SwapCached:         24 kB
Active:          23904 kB
Inactive:       168280 kB
HighTotal:      131008 kB
HighFree:        59752 kB
LowTotal:       903652 kB
LowFree:        755284 kB
SwapTotal:     2097892 kB
SwapFree:      2097660 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6640 kB
Slab:            21904 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 02:11:13 (client local time) WITH STATUS 30 IN 27.9897 SECONDS
stats: 18972 0 27.9897 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 26 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######
c   -- Clauses(.)/Splits(s): (none)
c ---[  24]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  22]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  20]---> Sorter-cost:  275     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  18]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  16]---> Sorter-cost:  455     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  14]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  12]---> Sorter-cost:  455     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  11]---> BDD-cost:   14
c ---[  10]---> BDD-cost:   14
c ---[   9]---> BDD-cost:   15
c ---[   8]---> BDD-cost:   15
c ---[   7]---> BDD-cost:   14
c ---[   6]---> BDD-cost:   15
c ---[   5]---> BDD-cost:   16
c ---[   4]---> BDD-cost:   16
c ---[   3]---> BDD-cost:   15
c ---[   2]---> BDD-cost:   16
c ---[   1]---> BDD-cost:   16
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    5719    13584 |    1906       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 69632[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 6116     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         2 |   19981    46877 |    6660       2       15     7.5 |  0.000 % |
c |       104 |   19981    46877 |    7326     104     1142    11.0 |  4.283 % |
c ==============================================================================
c [1mFound solution: 63168[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       187 |   20028    47001 |    6676     187     2186    11.7 |  4.283 % |
c ==============================================================================
c [1mFound solution: 63040[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       244 |   20040    47036 |    6680     244     3256    13.3 |  4.283 % |
c |       344 |   20040    47036 |    7348     344     4021    11.7 |  4.288 % |
c |       494 |   20040    47036 |    8082     494     5290    10.7 |  4.288 % |
c |       720 |   20040    47036 |    8891     720     9531    13.2 |  4.288 % |
c ==============================================================================
c [1mFound solution: 62454[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       841 |   20055    47085 |    6685     841    13225    15.7 |  4.288 % |
c |       943 |   20055    47085 |    7353     943    16068    17.0 |  4.296 % |
c ==============================================================================
c [1mFound solution: 59900[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1076 |   20046    47073 |    6682    1074    18047    16.8 |  4.296 % |
c |      1176 |   20046    47073 |    7350    1174    19285    16.4 |  4.396 % |
c |      1326 |   20046    47073 |    8085    1324    27692    20.9 |  4.396 % |
c ==============================================================================
c [1mFound solution: 57622[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1418 |   20072    47141 |    6690    1416    29974    21.2 |  4.396 % |
c |      1518 |   20072    47141 |    7359    1516    31706    20.9 |  4.400 % |
c |      1668 |   20072    47141 |    8094    1666    37067    22.2 |  4.400 % |
c |      1893 |   20043    47079 |    8904    1889    42867    22.7 |  4.530 % |
c |      2230 |   20043    47079 |    9794    2226    53581    24.1 |  4.530 % |
c |      2736 |   20040    47072 |   10774    2657    77254    29.1 |  4.555 % |
c |      3497 |   20040    47072 |   11851    3418   106715    31.2 |  4.555 % |
c |      4637 |   20033    47057 |   13036    4557   137444    30.2 |  4.581 % |
c |      6345 |   20033    47057 |   14340    6265   235328    37.6 |  4.581 % |
c |      8911 |   20033    47057 |   15774    8831   324335    36.7 |  4.581 % |
c ==============================================================================
c [1mFound solution: 57620[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12119 |   20040    47080 |    6680   12038   491447    40.8 |  4.581 % |
c |     12219 |   20040    47080 |    7348    6119   242617    39.6 |  4.615 % |
c |     12372 |   20040    47080 |    8082    6272   246261    39.3 |  4.615 % |
c ==============================================================================
c [1mFound solution: 50172[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12394 |   20086    47198 |    6695    6294   246681    39.2 |  4.615 % |
c |     12494 |   20086    47198 |    7364    6394   249097    39.0 |  4.611 % |
c |     12644 |   20086    47198 |    8100    6544   254240    38.9 |  4.611 % |
c |     12869 |   20086    47198 |    8911    6769   260927    38.5 |  4.611 % |
c |     13206 |   20086    47198 |    9802    7106   271797    38.2 |  4.611 % |
c ==============================================================================
c [1mFound solution: 49620[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13637 |   20096    47227 |    6698    7537   283569    37.6 |  4.611 % |
c |     13739 |   20096    47227 |    7367    3871   118107    30.5 |  4.621 % |
c |     13889 |   20096    47227 |    8104    4021   124612    31.0 |  4.621 % |
c |     14115 |   20096    47227 |    8915    4247   129988    30.6 |  4.621 % |
c |     14452 |   20096    47227 |    9806    4584   138421    30.2 |  4.621 % |
c ==============================================================================
c [1mFound solution: 48640[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14526 |   20107    47256 |    6702    4658   139936    30.0 |  4.621 % |
c |     14627 |   20107    47256 |    7372    4759   142402    29.9 |  4.630 % |
c |     14777 |   20100    47240 |    8109    4908   146510    29.9 |  4.643 % |
c |     15003 |   20100    47240 |    8920    5134   150696    29.4 |  4.643 % |
c |     15340 |   20100    47240 |    9812    5471   156640    28.6 |  4.643 % |
c |     15846 |   20100    47240 |   10793    5977   169252    28.3 |  4.643 % |
c |     16608 |   20100    47240 |   11873    6739   187436    27.8 |  4.643 % |
c ==============================================================================
c [1mFound solution: 46080[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17676 |   20118    47292 |    6706    7806   229462    29.4 |  4.643 % |
c |     17779 |   20118    47292 |    7376    4006    91340    22.8 |  4.672 % |
c |     17929 |   20118    47292 |    8114    4156    94666    22.8 |  4.672 % |
c |     18154 |   20118    47292 |    8925    4381   101775    23.2 |  4.672 % |
c |     18493 |   20118    47292 |    9818    4720   109794    23.3 |  4.672 % |
c |     18999 |   20118    47292 |   10800    5226   127053    24.3 |  4.672 % |
c |     19759 |   20118    47292 |   11880    5986   145165    24.3 |  4.672 % |
c ==============================================================================
c [1mFound solution: 44800[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19805 |   20129    47324 |    6709    6032   146213    24.2 |  4.672 % |
c |     19905 |   20129    47324 |    7379    6132   148197    24.2 |  4.681 % |
c |     20055 |   20129    47324 |    8117    6282   150779    24.0 |  4.681 % |
c |     20281 |   20129    47324 |    8929    6508   155379    23.9 |  4.681 % |
c |     20618 |   20129    47324 |    9822    6845   161306    23.6 |  4.681 % |
c |     21124 |   20129    47324 |   10804    7351   170025    23.1 |  4.681 % |
c |     21883 |   20129    47324 |   11885    8110   184974    22.8 |  4.681 % |
c |     23022 |   19495    45902 |   13073    3587    71348    19.9 |  7.707 % |
c ==============================================================================
c [1mOptimal solution: 44800[0m
s OPTIMUM FOUND
v -X0_bit_7 -X0_bit_6 -X0_bit_5 -X0_bit_4 -X0_bit_3 -X0_bit_2 -X0_bit_1 -X0_bit0 -X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X1_bit_7 -X1_bit_6 -X1_bit_5 -X1_bit_4 -X1_bit_3 -X1_bit_2 -X1_bit_1 -X1_bit0 -X1_bit1 -X1_bit2 -X1_bit3 -X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 -X2_bit_7 -X2_bit_6 -X2_bit_5 -X2_bit_4 -X2_bit_3 -X2_bit_2 -X2_bit_1 -X2_bit0 X2_bit1 -X2_bit2 X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 -X3_bit_7 -X3_bit_6 -X3_bit_5 -X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 -X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 -X4_bit_7 -X4_bit_6 -X4_bit_5 -X4_bit_4 -X4_bit_3 -X4_bit_2 -X4_bit_1 -X4_bit0 X4_bit1 X4_bit2 X4_bit3 X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 -X5_bit_7 -X5_bit_6 -X5_bit_5 -X5_bit_4 -X5_bit_3 -X5_bit_2 -X5_bit_1 -X5_bit0 -X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X6_bit_7 -X6_bit_6 -X6_bit_5 -X6_bit_4 -X6_bit_3 -X6_bit_2 -X6_bit_1 -X6_bit0 -X6_bit1 X6_bit2 -X6_bit3 X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X7_bit_7 -X7_bit_6 -X7_bit_5 -X7_bit_4 -X7_bit_3 -X7_bit_2 -X7_bit_1 -X7_bit0 -X7_bit1 X7_bit2 -X7_bit3 X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 -X8_bit_7 -X8_bit_6 -X8_bit_5 -X8_bit_4 -X8_bit_3 -X8_bit_2 -X8_bit_1 -X8_bit0 -X8_bit1 -X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 -X9_bit_7 -X9_bit_6 -X9_bit_5 -X9_bit_4 -X9_bit_3 -X9_bit_2 -X9_bit_1 -X9_bit0 -X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 -X10_bit_7 -X10_bit_6 -X10_bit_5 -X10_bit_4 -X10_bit_3 -X10_bit_2 -X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 -X11_bit_7 -X11_bit_6 -X11_bit_5 -X11_bit_4 -X11_bit_3 -X11_bit_2 -X11_bit_1 -X11_bit0 -X11_bit1 X11_bit2 -X11_bit3 X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 -Y0_bit0 -Y1_bit0 Y2_bit0 -Y3_bit0 Y4_bit0 -Y5_bit0 Y6_bit0 Y7_bit0 -Y8_bit0 -Y9_bit0 -Y10_bit0 Y11_bit0
c _______________________________________________________________________________
c 
c restarts              : 58
c conflicts             : 23099          (827 /sec)
c decisions             : 41358          (1480 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 27.9418 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.88 0.93 0.90 2/54 25535
Raw data (stat): 25535 (runsolver) R 25534 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541372793 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.90 0.93 0.90 2/54 25535
Raw data (stat): 25535 (minisat+) R 25534 26298 26297 0 -1 0 1368 0 0 0 996 2 0 0 25 0 1 0 541372793 7262208 1344 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1773 1344 603 41 0 1732 0
vsize: 7092
[startup+19.9998 s]
Raw data (loadavg): 0.92 0.93 0.90 2/54 25535
Raw data (stat): 25535 (minisat+) R 25534 26298 26297 0 -1 0 1535 0 0 0 1995 3 0 0 25 0 1 0 541372793 7933952 1511 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1937 1511 603 41 0 1896 0
vsize: 7748
[startup+27.9999 s]
Raw data (loadavg): 0.92 0.93 0.90 1/53 25535
Raw data (stat): 25535 (minisat+) R 25534 26298 26297 0 -1 0 1535 0 0 0 1995 3 0 0 25 0 1 0 541372793 7933952 1511 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1937 1511 603 41 0 1896 0
vsize: 0

Child status: 30
Real time (s): 27.9996
CPU time (s): 27.9897
CPU user time (s): 27.9458
CPU system time (s): 0.043993
CPU usage (%): 99.9647
Max. virtual memory (Kb): 7748
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	44800
#### END VERIFIER DATA ####