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/MIPLIB/miplib3/normalized-mps-v2-13-7-flugpl.opb
MD5SUM	1b5898327a7b85a882e36ea549878fdf
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1843200
Optimality of the best value was proved	NO
Number of terms in the objective function	195
Biggest coefficient in the objective function	47185920
Number of bits for the biggest coefficient in the objective function	26
Sum of the numbers in the objective function	103639200
Number of bits of the sum of numbers in the objective function	27
Biggest number in a constraint	78643200
Number of bits of the biggest number in a constraint	27
Biggest sum of numbers in a constraint	159755625
Number of bits of the biggest sum of numbers	28
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.181972
Number of variables	195
Total number of constraints	29
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	29
Minimum length of a constraint	5
Maximum length of a constraint	45
Trace number 18156

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-04-21 14:02:21 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18366 boxname=wulflinc7 idbench=1413 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  1b5898327a7b85a882e36ea549878fdf  /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-flugpl.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-flugpl.opb /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-flugpl.opb
IDLAUNCH: 18366
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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		: 451.050
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:        654392 kB
Buffers:         22924 kB
Cached:         335228 kB
SwapCached:          4 kB
Active:         168960 kB
Inactive:       192024 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        654140 kB
SwapTotal:     2097136 kB
SwapFree:      2097128 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6936 kB
Slab:            13724 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 14:02:27 (client local time) WITH STATUS 30 IN 6.16606 SECONDS
stats: 18366 0 6.16606 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 35 PB-constraints to clauses...
c   -- Unit propagations: pp
c   -- Detecting intervals from adjacent constraints: #####
c   -- Clauses(.)/Splits(s): (none)
c ---[  34]---> Adder-cost: 8   maxlim: 12   bits: 5/4
c ---[  33]---> Adder-cost: 8   maxlim: 12   bits: 5/4
c ---[  32]---> Adder-cost: 8   maxlim: 12   bits: 5/4
c ---[  31]---> Adder-cost: 8   maxlim: 12   bits: 5/4
c ---[  30]---> Adder-cost: 8   maxlim: 12   bits: 5/4
c ---[  29]---> Adder-cost: 8   maxlim: 12   bits: 5/4
c ---[  28]---> Adder-cost: 8   maxlim: 12   bits: 5/4
c ---[  27]---> Adder-cost: 8   maxlim: 12   bits: 5/4
c ---[  26]---> Adder-cost: 8   maxlim: 12   bits: 5/4
c ---[  25]---> Adder-cost: 8   maxlim: 12   bits: 5/4
c ---[  24]---> Adder-cost: 8   maxlim: 12   bits: 5/4
c ---[  20]---> Adder-cost: 30   maxlim: 35840   bits: 17/16
c ---[  18]---> Adder-cost: 50   maxlim: 532   bits: 10/10
c ---[  16]---> Adder-cost: 50   maxlim: 532   bits: 10/10
c ---[  14]---> Adder-cost: 50   maxlim: 532   bits: 10/10
c ---[  12]---> Adder-cost: 50   maxlim: 532   bits: 10/10
c ---[  11]---> Adder-cost: 40   maxlim: 268799   bits: 20/19
c ---[  10]---> Adder-cost: 79   maxlim: 454399   bits: 20/19
c ---[   9]---> Adder-cost: 79   maxlim: 326399   bits: 20/19
c ---[   8]---> Adder-cost: 80   maxlim: 582399   bits: 21/20
c ---[   7]---> Adder-cost: 79   maxlim: 454399   bits: 20/19
c ---[   6]---> Adder-cost: 80   maxlim: 838399   bits: 21/20
c ---[   5]---> Adder-cost: 0   maxlim: 108542   bits: 18/17
c ---[   4]---> Adder-cost: 49   maxlim: 116222   bits: 18/17
c ---[   3]---> Adder-cost: 49   maxlim: 116222   bits: 18/17
c ---[   2]---> Adder-cost: 49   maxlim: 116222   bits: 18/17
c ---[   1]---> Adder-cost: 49   maxlim: 116222   bits: 18/17
c ---[   0]---> Adder-cost: 49   maxlim: 116222   bits: 18/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    5695    20694 |    1898       0        0     nan |  0.000 % |
c |       101 |    5688    20671 |    2087     100      528     5.3 | 20.947 % |
c |       253 |    5670    20611 |    2296     251     1564     6.2 | 21.162 % |
c |       479 |    5596    20343 |    2526     313     1912     6.1 | 21.377 % |
c ==============================================================================
c [1mFound solution: 2284161[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 494   maxlim: 2949497   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       549 |    8963    32417 |    2987     383     2498     6.5 | 21.377 % |
c ==============================================================================
c [1mFound solution: 2173113[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3060545   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       595 |    8990    32600 |    2996     429     2747     6.4 | 21.377 % |
c |       695 |    8830    32017 |    3295     467     3787     8.1 | 16.894 % |
c ==============================================================================
c [1mFound solution: 2154411[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 244   maxlim: 2894927   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       775 |   10512    38066 |    3504     547     4302     7.9 | 16.894 % |
c |       875 |   10512    38066 |    3854     647     4941     7.6 | 15.299 % |
c ==============================================================================
c [1mFound solution: 2038544[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 278   maxlim: 2626794   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1022 |   11426    41419 |    3808     687     5781     8.4 | 15.299 % |
c |      1122 |   11426    41419 |    4188     787     6768     8.6 | 17.375 % |
c |      1273 |   11426    41419 |    4607     938     8896     9.5 | 17.375 % |
c |      1499 |   11275    40876 |    5068    1152    10904     9.5 | 17.664 % |
c |      1836 |   11275    40876 |    5575    1489    16435    11.0 | 17.662 % |
c ==============================================================================
c [1mFound solution: 2019067[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 170   maxlim: 2461951   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2156 |   12430    45010 |    4143    1809    19973    11.0 | 17.662 % |
c |      2257 |   12430    45010 |    4557    1910    22006    11.5 | 16.711 % |
c ==============================================================================
c [1mFound solution: 1969823[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 158   maxlim: 2326875   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2339 |   13305    48172 |    4435    1988    22651    11.4 | 16.711 % |
c |      2439 |   13305    48172 |    4878    2088    24598    11.8 | 16.278 % |
c ==============================================================================
c [1mFound solution: 1936905[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2359793   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2486 |   13318    48289 |    4439    2135    25132    11.8 | 16.278 % |
c |      2587 |   13318    48289 |    4882    2236    26403    11.8 | 16.466 % |
c |      2738 |   13318    48289 |    5371    2387    27636    11.6 | 16.464 % |
c |      2963 |   13318    48289 |    5908    2612    30208    11.6 | 16.464 % |
c ==============================================================================
c [1mFound solution: 1868543[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2428155   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3048 |   13335    48439 |    4445    2697    31248    11.6 | 16.464 % |
c |      3149 |   13335    48439 |    4889    2798    32897    11.8 | 16.696 % |
c ==============================================================================
c [1mFound solution: 1851387[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2445311   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3238 |   13339    48463 |    4446    2887    33670    11.7 | 16.696 % |
c |      3339 |   13339    48463 |    4890    2988    35248    11.8 | 16.757 % |
c |      3490 |   13339    48463 |    5379    3139    37357    11.9 | 16.755 % |
c |      3715 |   13332    48440 |    5917    3362    42260    12.6 | 16.793 % |
c ==============================================================================
c [1mFound solution: 1850381[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2446317   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3953 |   13349    48598 |    4449    3600    45406    12.6 | 16.793 % |
c |      4053 |   13349    48598 |    4893    3700    46865    12.7 | 17.009 % |
c ==============================================================================
c [1mFound solution: 1850379[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2446319   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4070 |   13317    48490 |    4439    3701    47089    12.7 | 17.009 % |
c ==============================================================================
c [1mFound solution: 1850377[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2446321   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4101 |   13319    48512 |    4439    3732    47762    12.8 | 17.009 % |
c |      4201 |   13319    48512 |    4882    3832    48689    12.7 | 17.090 % |
c ==============================================================================
c [1mFound solution: 1850375[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2446323   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4320 |   13320    48532 |    4440    3951    50663    12.8 | 17.090 % |
c |      4420 |   13320    48532 |    4884    4051    51451    12.7 | 17.120 % |
c |      4570 |   13305    48481 |    5372    4199    54227    12.9 | 17.191 % |
c ==============================================================================
c [1mFound solution: 1849212[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2447486   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4594 |   13318    48631 |    4439    4223    54638    12.9 | 17.191 % |
c |      4694 |   13318    48631 |    4882    4323    57165    13.2 | 17.395 % |
c |      4847 |   13318    48631 |    5371    4476    59498    13.3 | 17.395 % |
c |      5074 |   13318    48631 |    5908    4703    64183    13.6 | 17.395 % |
c |      5411 |   13318    48631 |    6499    5040    69989    13.9 | 17.393 % |
c |      5918 |   13318    48631 |    7149    5547    81123    14.6 | 17.395 % |
c ==============================================================================
c [1mFound solution: 1849211[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2447487   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6304 |   13320    48648 |    4440    5933    85920    14.5 | 17.395 % |
c ==============================================================================
c [1mFound solution: 1849149[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2447549   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6343 |   13328    48747 |    4442    3006    43602    14.5 | 17.395 % |
c ==============================================================================
c [1mFound solution: 1849083[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2447615   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6359 |   13330    48763 |    4443    3022    43683    14.5 | 17.395 % |
c ==============================================================================
c [1mFound solution: 1848931[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2447767   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6366 |   13335    48819 |    4445    3029    43745    14.4 | 17.395 % |
c |      6466 |   13335    48819 |    4889    3129    45782    14.6 | 17.639 % |
c ==============================================================================
c [1mFound solution: 1848915[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2447783   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6472 |   13339    48859 |    4446    3135    45940    14.7 | 17.639 % |
c ==============================================================================
c [1mFound solution: 1848883[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2447815   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6472 |   13342    48895 |    4447    3135    45940    14.7 | 17.639 % |
c ==============================================================================
c [1mFound solution: 1848851[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2447847   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6476 |   13346    48930 |    4448    3139    45952    14.6 | 17.639 % |
c ==============================================================================
c [1mFound solution: 1848847[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2447851   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6476 |   13348    48952 |    4449    3139    45952    14.6 | 17.639 % |
c ==============================================================================
c [1mFound solution: 1848843[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2447855   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6482 |   13350    48969 |    4450    3145    46016    14.6 | 17.639 % |
c ==============================================================================
c [1mFound solution: 1847163[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2449535   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6512 |   13355    49000 |    4451    3175    46708    14.7 | 17.639 % |
c |      6612 |   13355    49000 |    4896    3275    47948    14.6 | 17.879 % |
c ==============================================================================
c [1mFound solution: 1847103[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2449595   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6695 |   13363    49078 |    4454    3358    49824    14.8 | 17.879 % |
c |      6796 |   13363    49078 |    4899    3459    51027    14.8 | 17.965 % |
c ==============================================================================
c [1mFound solution: 1847099[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2449599   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6810 |   13365    49096 |    4455    3473    51276    14.8 | 17.965 % |
c |      6910 |   13365    49096 |    4900    3573    53087    14.9 | 17.987 % |
c ==============================================================================
c [1mFound solution: 1847067[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2449631   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6914 |   13367    49114 |    4455    3577    53114    14.8 | 17.987 % |
c ==============================================================================
c [1mFound solution: 1847063[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2449635   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6919 |   13368    49134 |    4456    3582    53241    14.9 | 17.987 % |
c ==============================================================================
c [1mFound solution: 1847051[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2449647   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6920 |   13370    49152 |    4456    3583    53244    14.9 | 17.987 % |
c ==============================================================================
c [1mFound solution: 1847047[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2449651   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6925 |   13372    49174 |    4457    3588    53261    14.8 | 17.987 % |
c ==============================================================================
c [1mFound solution: 1847043[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2449655   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6933 |   13374    49193 |    4458    3596    53431    14.9 | 17.987 % |
c |      7033 |   13374    49193 |    4903    3696    55614    15.0 | 18.106 % |
c |      7183 |   13374    49193 |    5394    3846    57794    15.0 | 18.103 % |
c |      7411 |   13374    49193 |    5933    4074    61002    15.0 | 18.104 % |
c ==============================================================================
c [1mFound solution: 1847041[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2449657   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7440 |   13376    49215 |    4458    4103    61561    15.0 | 18.104 % |
c ==============================================================================
c [1mFound solution: 1847040[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2449658   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7445 |   13378    49239 |    4459    4108    61588    15.0 | 18.104 % |
c |      7545 |   13378    49239 |    4904    4208    62937    15.0 | 18.149 % |
c |      7695 |   12754    47003 |    5395    1841    20132    10.9 | 19.284 % |
c |      7920 |   12754    47003 |    5934    2066    23364    11.3 | 19.284 % |
c ==============================================================================
c [1mFound solution: 1847035[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 190   maxlim: 2157823   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8238 |   14002    51460 |    4667    2384    29123    12.2 | 19.284 % |
c |      8338 |   14002    51460 |    5133    2484    30581    12.3 | 18.387 % |
c |      8488 |   13993    51429 |    5647    2630    32639    12.4 | 18.419 % |
c |      8715 |   13993    51429 |    6211    2857    34904    12.2 | 18.419 % |
c ==============================================================================
c [1mFound solution: 1846589[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2158269   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8731 |   14005    51548 |    4668    2873    35225    12.3 | 18.419 % |
c |      8831 |   14005    51548 |    5134    2973    36651    12.3 | 18.577 % |
c ==============================================================================
c [1mFound solution: 1846334[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2158524   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8869 |   14017    51672 |    4672    3011    37040    12.3 | 18.577 % |
c |      8971 |   14017    51672 |    5139    3113    40287    12.9 | 18.730 % |
c |      9121 |   14017    51672 |    5653    3263    42789    13.1 | 18.727 % |
c ==============================================================================
c [1mFound solution: 1846237[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2158621   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9167 |   14028    51766 |    4676    3309    43401    13.1 | 18.727 % |
c ==============================================================================
c [1mFound solution: 1845569[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2159289   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9197 |   14039    51863 |    4679    3339    43758    13.1 | 18.727 % |
c ==============================================================================
c [1mFound solution: 1844667[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2160191   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9292 |   14043    51903 |    4681    3434    45852    13.4 | 18.727 % |
c |      9392 |   14043    51903 |    5149    3534    47223    13.4 | 19.028 % |
c |      9542 |   14043    51903 |    5664    3684    51956    14.1 | 19.028 % |
c |      9767 |   14043    51903 |    6230    3909    53640    13.7 | 19.028 % |
c |     10104 |   14043    51903 |    6853    4246    57002    13.4 | 19.028 % |
c |     10610 |   14043    51903 |    7538    4752    66299    14.0 | 19.028 % |
c |     11369 |   14043    51903 |    8292    5511    79083    14.4 | 19.028 % |
c |     12508 |   14043    51903 |    9121    6650   102636    15.4 | 19.028 % |
c ==============================================================================
c [1mFound solution: 1844255[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2160603   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13165 |   14055    52006 |    4685    7307   114710    15.7 | 19.028 % |
c |     13266 |   14055    52006 |    5153    3755    58386    15.5 | 19.149 % |
c ==============================================================================
c [1mFound solution: 1844235[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2160623   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13307 |   14059    52038 |    4686    3796    58757    15.5 | 19.149 % |
c |     13408 |   14059    52038 |    5154    3897    59948    15.4 | 19.185 % |
c |     13558 |   14059    52038 |    5670    4047    62046    15.3 | 19.185 % |
c ==============================================================================
c [1mFound solution: 1844219[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2160639   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13710 |   14060    52048 |    4686    4199    65067    15.5 | 19.185 % |
c |     13812 |   14060    52048 |    5154    4301    66677    15.5 | 19.214 % |
c ==============================================================================
c [1mFound solution: 1843915[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2160943   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13892 |   14064    52096 |    4688    4381    67786    15.5 | 19.214 % |
c |     13992 |   14064    52096 |    5156    4481    68818    15.4 | 19.281 % |
c ==============================================================================
c [1mFound solution: 1843851[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2161007   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14066 |   14068    52143 |    4689    4555    70002    15.4 | 19.281 % |
c ==============================================================================
c [1mFound solution: 1843723[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2161135   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14085 |   14076    52207 |    4692    4574    70403    15.4 | 19.281 % |
c ==============================================================================
c [1mFound solution: 1843531[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2161327   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14129 |   14083    52264 |    4694    4618    70821    15.3 | 19.281 % |
c ==============================================================================
c [1mFound solution: 1843515[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2161343   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14154 |   14085    52281 |    4695    4643    71347    15.4 | 19.281 % |
c ==============================================================================
c [1mFound solution: 1843467[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2161391   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14172 |   14089    52315 |    4696    4661    71514    15.3 | 19.281 % |
c ==============================================================================
c [1mFound solution: 1843459[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2161399   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14186 |   14082    52302 |    4694    3936    60542    15.4 | 19.281 % |
c ==============================================================================
c [1mFound solution: 1843451[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2161407   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14192 |   14083    52315 |    4694    3942    60560    15.4 | 19.281 % |
c ==============================================================================
c [1mFound solution: 1843323[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2161535   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14206 |   14084    52328 |    4694    3956    61075    15.4 | 19.281 % |
c ==============================================================================
c [1mFound solution: 1843259[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2161599   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14284 |   14083    52334 |    4694    3975    61145    15.4 | 19.281 % |
c ==============================================================================
c [1mFound solution: 1843227[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2161631   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14293 |   14084    52346 |    4694    3984    61418    15.4 | 19.281 % |
c ==============================================================================
c [1mFound solution: 1843207[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2161651   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14300 |   14087    52374 |    4695    3991    61464    15.4 | 19.281 % |
c ==============================================================================
c [1mFound solution: 1843203[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2161655   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14300 |   14089    52391 |    4696    3991    61464    15.4 | 19.281 % |
c ==============================================================================
c [1mFound solution: 1843200[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2161658   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14323 |   14093    52428 |    4697    4014    61682    15.4 | 19.281 % |
c ==============================================================================
c [1mOptimal solution: 1843200[0m
s OPTIMUM FOUND
v -STM1_bit_7 -STM1_bit_6 -STM1_bit_5 -STM1_bit_4 -STM1_bit_3 -STM1_bit_2 -STM1_bit_1 -STM1_bit0 -STM1_bit1 STM1_bit2 STM1_bit3 STM1_bit4 STM1_bit5 -STM1_bit6 -STM1_bit7 -STM1_bit8 -STM1_bit9 -STM1_bit10 -STM1_bit11 -STM1_bit12 -ANM1_bit0 ANM1_bit1 ANM1_bit2 -ANM1_bit3 -ANM1_bit4 -UE1_bit_7 -UE1_bit_6 -UE1_bit_5 -UE1_bit_4 -UE1_bit_3 -UE1_bit_2 -UE1_bit_1 -UE1_bit0 -UE1_bit1 -UE1_bit2 -UE1_bit3 -UE1_bit4 -UE1_bit5 -UE1_bit6 -UE1_bit7 -UE1_bit8 -UE1_bit9 -UE1_bit10 -UE1_bit11 -UE1_bit12 STM2_bit0 STM2_bit1 -STM2_bit2 -STM2_bit3 -STM2_bit4 -ANM2_bit0 ANM2_bit1 ANM2_bit2 -ANM2_bit3 -ANM2_bit4 -UE2_bit_7 -UE2_bit_6 -UE2_bit_5 -UE2_bit_4 -UE2_bit_3 -UE2_bit_2 -UE2_bit_1 -UE2_bit0 -UE2_bit1 -UE2_bit2 UE2_bit3 UE2_bit4 -UE2_bit5 UE2_bit6 -UE2_bit7 -UE2_bit8 UE2_bit9 -UE2_bit10 -UE2_bit11 -UE2_bit12 STM3_bit0 STM3_bit1 -STM3_bit2 -STM3_bit3 -STM3_bit4 -ANM3_bit0 -ANM3_bit1 -ANM3_bit2 -ANM3_bit3 ANM3_bit4 -UE3_bit_7 -UE3_bit_6 -UE3_bit_5 -UE3_bit_4 -UE3_bit_3 -UE3_bit_2 -UE3_bit_1 -UE3_bit0 -UE3_bit1 -UE3_bit2 UE3_bit3 UE3_bit4 -UE3_bit5 UE3_bit6 -UE3_bit7 -UE3_bit8 UE3_bit9 -UE3_bit10 -UE3_bit11 -UE3_bit12 STM4_bit0 -STM4_bit1 STM4_bit2 STM4_bit3 -STM4_bit4 ANM4_bit0 ANM4_bit1 ANM4_bit2 -ANM4_bit3 -ANM4_bit4 -UE4_bit_7 -UE4_bit_6 -UE4_bit_5 -UE4_bit_4 -UE4_bit_3 -UE4_bit_2 -UE4_bit_1 -UE4_bit0 -UE4_bit1 -UE4_bit2 UE4_bit3 -UE4_bit4 -UE4_bit5 UE4_bit6 UE4_bit7 -UE4_bit8 -UE4_bit9 -UE4_bit10 -UE4_bit11 -UE4_bit12 STM5_bit0 -STM5_bit1 STM5_bit2 STM5_bit3 -STM5_bit4 -ANM5_bit0 -ANM5_bit1 ANM5_bit2 ANM5_bit3 -ANM5_bit4 -UE5_bit_7 -UE5_bit_6 -UE5_bit_5 -UE5_bit_4 -UE5_bit_3 -UE5_bit_2 -UE5_bit_1 -UE5_bit0 -UE5_bit1 -UE5_bit2 -UE5_bit3 -UE5_bit4 -UE5_bit5 -UE5_bit6 -UE5_bit7 -UE5_bit8 -UE5_bit9 -UE5_bit10 -UE5_bit11 -UE5_bit12 -STM6_bit0 STM6_bit1 -STM6_bit2 -STM6_bit3 STM6_bit4 -ANM6_bit0 -ANM6_bit1 -ANM6_bit2 -ANM6_bit3 -ANM6_bit4 -UE6_bit_7 -UE6_bit_6 -UE6_bit_5 -UE6_bit_4 -UE6_bit_3 -UE6_bit_2 -UE6_bit_1 -UE6_bit0 UE6_bit1 UE6_bit2 UE6_bit3 -UE6_bit4 UE6_bit5 UE6_bit6 UE6_bit7 -UE6_bit8 UE6_bit9 -UE6_bit10 -UE6_bit11 -UE6_bit12
c _______________________________________________________________________________
c 
c restarts              : 112
c conflicts             : 14356          (2345 /sec)
c decisions             : 38045          (6213 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 6.12307 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.86 0.95 0.91 2/54 7791
Raw data (stat): 7791 (runsolver) R 7790 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487428170 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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+6.18148 s]
Raw data (loadavg): 0.87 0.95 0.91 1/53 7791
Raw data (stat): 7791 (runsolver) R 7790 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487428170 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 0

Child status: 30
Real time (s): 6.18087
CPU time (s): 6.16606
CPU user time (s): 6.12707
CPU system time (s): 0.038994
CPU usage (%): 99.7604
Max. virtual memory (Kb): 1028
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	1843200
#### END VERIFIER DATA ####