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/www.csit.fsu.edu/~burkardt/datasets/mps/normalized-mps-v2-13-7-maros.opb
MD5SUM	1ae5b04b2d0e1f5ab82e29e98b8350c0
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	43097
Optimality of the best value was proved	NO
Number of terms in the objective function	64
Biggest coefficient in the objective function	4718592
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	14745570
Number of bits of the sum of numbers in the objective function	24
Biggest number in a constraint	4718592
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	14745570
Number of bits of the biggest sum of numbers	24
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02384
Number of variables	64
Total number of constraints	6
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	6
Minimum length of a constraint	12
Maximum length of a constraint	64
Trace number 14084

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-04-20 23:10:19 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=20381 boxname=wulflinc12 idbench=1568 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  1ae5b04b2d0e1f5ab82e29e98b8350c0  /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-maros.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-maros.opb /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-maros.opb
IDLAUNCH: 20381
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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:        443304 kB
Buffers:         35808 kB
Cached:         532804 kB
SwapCached:          4 kB
Active:         233076 kB
Inactive:       338320 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        443052 kB
SwapTotal:     2097136 kB
SwapFree:      2097044 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6816 kB
Slab:            14248 kB
Committed_AS:    63584 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 23:10:42 (client local time) WITH STATUS 30 IN 23.2815 SECONDS
stats: 20381 0 23.2815 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 6 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #
c   -- Clauses(.)/Splits(s): s
c ---[   5]---> Adder-cost: 37   maxlim: 894   bits: 11/10
c ---[   3]---> Adder-cost: 120   maxlim: 34560   bits: 17/16
c ---[   2]---> Adder-cost: 76   maxlim: 24056   bits: 16/15
c ---[   1]---> Adder-cost: 72   maxlim: 11514   bits: 15/14
c ---[   0]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    2151     7912 |     717       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 53303[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 102   maxlim: 106411   bits: 18/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        63 |    2792    10232 |     930      62      563     9.1 |  0.000 % |
c |       163 |    2792    10232 |    1023     162     1904    11.8 | 15.190 % |
c ==============================================================================
c [1mFound solution: 49405[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 110309   bits: 18/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       216 |    2816    10395 |     938     215     2218    10.3 | 15.190 % |
c ==============================================================================
c [1mFound solution: 48936[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 110778   bits: 18/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       299 |    2832    10526 |     944     298     3726    12.5 | 15.190 % |
c |       399 |    2832    10526 |    1038     398     5131    12.9 | 17.452 % |
c |       549 |    2832    10526 |    1142     548     6550    12.0 | 17.452 % |
c |       774 |    2832    10526 |    1256     773    10658    13.8 | 17.452 % |
c ==============================================================================
c [1mFound solution: 47549[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 112165   bits: 18/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       859 |    2839    10598 |     946     858    11600    13.5 | 17.452 % |
c ==============================================================================
c [1mFound solution: 47507[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 112207   bits: 18/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       894 |    2841    10626 |     947     893    12114    13.6 | 17.452 % |
c ==============================================================================
c [1mFound solution: 47433[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 112281   bits: 18/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       933 |    2847    10691 |     949     932    12378    13.3 | 17.452 % |
c ==============================================================================
c [1mFound solution: 47173[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 112541   bits: 18/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       982 |    2857    10788 |     952     981    13145    13.4 | 17.452 % |
c |      1082 |    2857    10788 |    1047    1081    14543    13.5 | 19.565 % |
c |      1232 |    2857    10788 |    1151     637     6745    10.6 | 19.565 % |
c |      1458 |    2857    10788 |    1267     863    10435    12.1 | 19.565 % |
c |      1796 |    2857    10788 |    1393    1201    15969    13.3 | 19.565 % |
c ==============================================================================
c [1mFound solution: 47152[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 112562   bits: 18/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1915 |    2864    10859 |     954    1320    17782    13.5 | 19.565 % |
c ==============================================================================
c [1mFound solution: 47139[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 112575   bits: 18/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1986 |    2865    10872 |     955     731     8134    11.1 | 19.565 % |
c |      2086 |    2865    10872 |    1050     831     9984    12.0 | 20.132 % |
c |      2238 |    2865    10872 |    1155     983    11560    11.8 | 20.132 % |
c ==============================================================================
c [1mFound solution: 46568[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 113146   bits: 18/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2446 |    2879    11005 |     959    1191    15189    12.8 | 20.132 % |
c |      2547 |    2879    11005 |    1054     697     7221    10.4 | 21.129 % |
c |      2697 |    2879    11005 |    1160     847     9336    11.0 | 21.129 % |
c |      2923 |    2879    11005 |    1276    1073    12310    11.5 | 21.129 % |
c |      3261 |    2879    11005 |    1404    1411    16288    11.5 | 21.129 % |
c |      3770 |    2879    11005 |    1544    1098    12433    11.3 | 21.129 % |
c |      4529 |    2879    11005 |    1698     995    10907    11.0 | 21.129 % |
c ==============================================================================
c [1mFound solution: 45917[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 113797   bits: 18/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4564 |    2887    11069 |     962    1030    11362    11.0 | 21.129 % |
c |      4664 |    2887    11069 |    1058    1130    12740    11.3 | 21.497 % |
c |      4814 |    2887    11069 |    1164     660     5346     8.1 | 21.497 % |
c |      5041 |    2887    11069 |    1280     887     7991     9.0 | 21.497 % |
c |      5378 |    2887    11069 |    1408    1224    11949     9.8 | 21.497 % |
c |      5884 |    2887    11069 |    1549     955     8271     8.7 | 21.497 % |
c |      6643 |    2887    11069 |    1704     871     6863     7.9 | 21.497 % |
c |      7782 |    2887    11069 |    1874    1087     9426     8.7 | 21.497 % |
c ==============================================================================
c [1mFound solution: 45865[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 113849   bits: 18/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8825 |    2874    11069 |     958    1225    13206    10.8 | 21.497 % |
c |      8925 |    2874    11069 |    1053     713     5912     8.3 | 22.642 % |
c ==============================================================================
c [1mFound solution: 44451[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 115263   bits: 18/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9001 |    2880    11105 |     960     789     6897     8.7 | 22.642 % |
c |      9103 |    2835    10947 |    1056     885     8176     9.2 | 23.438 % |
c ==============================================================================
c [1mFound solution: 44383[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 18   maxlim: 78467   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9219 |    2943    11343 |     981    1001     9515     9.5 | 23.438 % |
c |      9319 |    2943    11343 |    1079    1101    10753     9.8 | 23.424 % |
c |      9469 |    2943    11343 |    1187    1251    12610    10.1 | 23.424 % |
c |      9694 |    2943    11343 |    1305     793     5829     7.4 | 23.424 % |
c |     10031 |    2938    11328 |    1436    1129     9845     8.7 | 23.574 % |
c |     10538 |    2938    11328 |    1579     831     6445     7.8 | 23.574 % |
c |     11297 |    2938    11328 |    1737    1590    16469    10.4 | 23.574 % |
c |     12437 |    2938    11328 |    1911    1776    22125    12.5 | 23.574 % |
c |     14147 |    2938    11328 |    2102    1393    12836     9.2 | 23.574 % |
c |     16710 |    2938    11328 |    2313    1666    15152     9.1 | 23.574 % |
c ==============================================================================
c [1mFound solution: 44332[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 78518   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20094 |    2946    11404 |     982    2477    30716    12.4 | 23.574 % |
c |     20197 |    2946    11404 |    1080     723     6476     9.0 | 24.036 % |
c |     20348 |    2946    11404 |    1188     874     8285     9.5 | 24.036 % |
c |     20573 |    2946    11404 |    1307    1099    10871     9.9 | 24.036 % |
c |     20910 |    2946    11404 |    1437    1436    15384    10.7 | 24.036 % |
c |     21417 |    2946    11404 |    1581    1131    10482     9.3 | 24.036 % |
c |     22176 |    2946    11404 |    1739    1890    24796    13.1 | 24.036 % |
c |     23315 |    2946    11404 |    1913    1029     8396     8.2 | 24.036 % |
c |     25023 |    2946    11404 |    2105    1686    23096    13.7 | 24.036 % |
c ==============================================================================
c [1mFound solution: 43534[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 79316   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26896 |    2957    11493 |     985    1244    12026     9.7 | 24.036 % |
c |     26996 |    2957    11493 |    1083     722     5278     7.3 | 24.672 % |
c |     27147 |    2957    11493 |    1191     873     7211     8.3 | 24.672 % |
c |     27373 |    2957    11493 |    1311    1099     9873     9.0 | 24.672 % |
c |     27711 |    2957    11493 |    1442    1437    14259     9.9 | 24.672 % |
c |     28217 |    2957    11493 |    1586    1118     9886     8.8 | 24.672 % |
c |     28977 |    2957    11493 |    1744     982     8454     8.6 | 24.672 % |
c |     30116 |    2957    11493 |    1919    1133     9837     8.7 | 24.672 % |
c |     31824 |    2957    11493 |    2111    1791    17636     9.8 | 24.672 % |
c |     34387 |    2957    11493 |    2322    1969    25505    13.0 | 24.672 % |
c |     38231 |    2957    11493 |    2554    2000    20262    10.1 | 24.672 % |
c ==============================================================================
c [1mFound solution: 43531[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 79319   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41711 |    2959    11509 |     986    2682    43157    16.1 | 24.672 % |
c |     41812 |    2959    11509 |    1084     772     7104     9.2 | 24.745 % |
c |     41963 |    2959    11509 |    1193     923     8795     9.5 | 24.745 % |
c |     42188 |    2959    11509 |    1312    1148    11243     9.8 | 24.745 % |
c |     42526 |    2959    11509 |    1443    1486    16321    11.0 | 24.745 % |
c |     43032 |    2959    11509 |    1587    1164     9705     8.3 | 24.745 % |
c |     43791 |    2959    11509 |    1746    1031     8704     8.4 | 24.745 % |
c |     44930 |    2959    11509 |    1921    1138    12061    10.6 | 24.745 % |
c |     46640 |    2959    11509 |    2113    1776    17338     9.8 | 24.745 % |
c ==============================================================================
c [1mFound solution: 43518[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 79332   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     48161 |    2965    11556 |     988    2141    23907    11.2 | 24.745 % |
c |     48261 |    2965    11556 |    1086    1171    11833    10.1 | 24.964 % |
c |     48411 |    2965    11556 |    1195     683     4589     6.7 | 24.964 % |
c |     48636 |    2965    11556 |    1315     908     7153     7.9 | 24.964 % |
c |     48975 |    2965    11556 |    1446    1247    11463     9.2 | 24.964 % |
c |     49481 |    2965    11556 |    1591     940     6780     7.2 | 24.964 % |
c |     50240 |    2965    11556 |    1750    1699    15074     8.9 | 24.965 % |
c |     51382 |    2965    11556 |    1925    1798    22135    12.3 | 24.964 % |
c |     53092 |    2965    11556 |    2117    1373    13871    10.1 | 24.964 % |
c |     55654 |    2961    11546 |    2329    1573    16154    10.3 | 25.254 % |
c |     59499 |    2961    11546 |    2562    1569    13925     8.9 | 25.253 % |
c ==============================================================================
c [1mFound solution: 43517[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 79333   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     60984 |    2963    11560 |     987    1587    16527    10.4 | 25.253 % |
c |     61084 |    2963    11560 |    1085     894     6362     7.1 | 25.324 % |
c |     61234 |    2963    11560 |    1194    1044     7902     7.6 | 25.324 % |
c |     61461 |    2963    11560 |    1313    1271    10877     8.6 | 25.325 % |
c |     61798 |    2963    11560 |    1445     838     5573     6.7 | 25.324 % |
c |     62305 |    2963    11560 |    1589    1345    12514     9.3 | 25.324 % |
c ==============================================================================
c [1mFound solution: 43493[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 79357   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     62416 |    2971    11621 |     990    1456    13925     9.6 | 25.324 % |
c |     62516 |    2971    11621 |    1089     828     6012     7.3 | 25.605 % |
c |     62667 |    2971    11621 |    1197     979     7473     7.6 | 25.606 % |
c |     62892 |    2971    11621 |    1317    1204    10535     8.8 | 25.605 % |
c |     63229 |    2971    11621 |    1449    1541    14362     9.3 | 25.605 % |
c |     63735 |    2971    11621 |    1594    1165    10734     9.2 | 25.605 % |
c |     64498 |    2971    11621 |    1753    1017     9980     9.8 | 25.605 % |
c |     65639 |    2971    11621 |    1929    1139     9893     8.7 | 25.605 % |
c |     67347 |    2971    11621 |    2122    1774    22693    12.8 | 25.605 % |
c ==============================================================================
c [1mFound solution: 43306[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 79544   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     68492 |    2982    11691 |     994    1738    18085    10.4 | 25.605 % |
c |     68592 |    2982    11691 |    1093     969     7263     7.5 | 26.052 % |
c |     68743 |    2982    11691 |    1202    1120     9029     8.1 | 26.051 % |
c ==============================================================================
c [1mFound solution: 43282[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 79568   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     68820 |    2988    11734 |     996    1197    10103     8.4 | 26.051 % |
c |     68920 |    2988    11734 |    1095     699     4306     6.2 | 26.250 % |
c |     69070 |    2988    11734 |    1205     849     6588     7.8 | 26.250 % |
c |     69295 |    2988    11734 |    1325    1074     8949     8.3 | 26.251 % |
c |     69632 |    2988    11734 |    1458    1411    13550     9.6 | 26.250 % |
c ==============================================================================
c [1mFound solution: 43217[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 79633   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     69934 |    2994    11774 |     998    1713    17357    10.1 | 26.250 % |
c |     70035 |    2994    11774 |    1097     958     7276     7.6 | 26.446 % |
c |     70185 |    2994    11774 |    1207    1108     9087     8.2 | 26.448 % |
c |     70411 |    2994    11774 |    1328    1334    12172     9.1 | 26.446 % |
c |     70748 |    2994    11774 |    1461     858     6235     7.3 | 26.448 % |
c |     71255 |    2994    11774 |    1607    1365    12467     9.1 | 26.448 % |
c |     72014 |    2994    11774 |    1768    1211    11673     9.6 | 26.446 % |
c |     73153 |    2994    11774 |    1944    1298    13329    10.3 | 26.446 % |
c |     74864 |    2994    11774 |    2139    1919    21133    11.0 | 26.446 % |
c |     77427 |    2994    11774 |    2353    2117    28219    13.3 | 26.446 % |
c ==============================================================================
c [1mFound solution: 43215[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 79635   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     81137 |    2996    11789 |     998    1903    22721    11.9 | 26.446 % |
c |     81239 |    2996    11789 |    1097    1054     8880     8.4 | 26.512 % |
c |     81389 |    2996    11789 |    1207    1204    10374     8.6 | 26.512 % |
c |     81615 |    2996    11789 |    1328    1430    12399     8.7 | 26.511 % |
c |     81952 |    2996    11789 |    1461     987     7349     7.4 | 26.511 % |
c |     82459 |    2996    11789 |    1607    1494    13472     9.0 | 26.512 % |
c |     83218 |    2996    11789 |    1768    1339    11760     8.8 | 26.512 % |
c ==============================================================================
c [1mFound solution: 43168[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 79682   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     83813 |    3001    11833 |    1000    1934    18259     9.4 | 26.512 % |
c |     83914 |    3001    11833 |    1100    1068     7887     7.4 | 26.740 % |
c |     84066 |    3001    11833 |    1210    1220     9774     8.0 | 26.740 % |
c |     84293 |    3001    11833 |    1331    1447    12119     8.4 | 26.740 % |
c |     84630 |    3001    11833 |    1464     977     7872     8.1 | 26.740 % |
c |     85136 |    3001    11833 |    1610    1483    13269     8.9 | 26.740 % |
c |     85895 |    3001    11833 |    1771    1325    12345     9.3 | 26.740 % |
c ==============================================================================
c [1mFound solution: 43167[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 79683   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86434 |    3003    11848 |    1001    1864    18896    10.1 | 26.740 % |
c |     86534 |    3003    11848 |    1101    1032     8714     8.4 | 26.803 % |
c |     86685 |    3003    11848 |    1211    1183    10441     8.8 | 26.803 % |
c |     86910 |    3003    11848 |    1332    1408    13229     9.4 | 26.803 % |
c |     87247 |    3003    11848 |    1465     962     7494     7.8 | 26.804 % |
c |     87755 |    3003    11848 |    1612    1470    14915    10.1 | 26.803 % |
c |     88516 |    3003    11848 |    1773    1307    11993     9.2 | 26.804 % |
c |     89655 |    3003    11848 |    1950    1395    14882    10.7 | 26.803 % |
c |     91364 |    3003    11848 |    2145    2001    22205    11.1 | 26.804 % |
c ==============================================================================
c [1mFound solution: 43164[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 79686   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     92356 |    3007    11881 |    1002    1804    18953    10.5 | 26.804 % |
c |     92457 |    3007    11881 |    1102    1003     7248     7.2 | 26.930 % |
c |     92607 |    3007    11881 |    1212    1153     8547     7.4 | 26.930 % |
c |     92832 |    3007    11881 |    1333    1378    12014     8.7 | 26.930 % |
c |     93170 |    3007    11881 |    1467     942     6539     6.9 | 26.929 % |
c |     93676 |    3007    11881 |    1613    1448    13859     9.6 | 26.928 % |
c |     94435 |    3007    11881 |    1775    1270    11677     9.2 | 26.930 % |
c ==============================================================================
c [1mFound solution: 43144[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 79706   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     95111 |    3015    11940 |    1005    1946    20181    10.4 | 26.930 % |
c |     95212 |    3015    11940 |    1105    1074     8001     7.4 | 27.176 % |
c |     95363 |    2933    11646 |    1216    1056     8176     7.7 | 27.711 % |
c |     95588 |    2933    11646 |    1337    1281    10885     8.5 | 27.711 % |
c |     95925 |    2933    11646 |    1471     843     5406     6.4 | 27.711 % |
c |     96434 |    2933    11646 |    1618    1352    11825     8.7 | 27.711 % |
c |     97193 |    2933    11646 |    1780    1181    10295     8.7 | 27.711 % |
c ==============================================================================
c [1mFound solution: 43141[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 32   maxlim: 69469   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     98117 |    3114    12335 |    1038    1087     9190     8.5 | 27.711 % |
c |     98218 |    3114    12335 |    1141    1188    10542     8.9 | 27.743 % |
c ==============================================================================
c [1mFound solution: 43140[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 69470   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     98323 |    3116    12353 |    1038    1293    11796     9.1 | 27.743 % |
c |     98423 |    3111    12335 |    1141     744     5004     6.7 | 28.050 % |
c |     98573 |    3111    12335 |    1255     894     7401     8.3 | 28.052 % |
c |     98799 |    3111    12335 |    1381    1120    10148     9.1 | 28.051 % |
c ==============================================================================
c [1mFound solution: 43138[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 69472   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     98982 |    3114    12361 |    1038    1303    12714     9.8 | 28.051 % |
c |     99082 |    3114    12361 |    1141     752     5024     6.7 | 28.196 % |
c |     99232 |    3114    12361 |    1255     902     6618     7.3 | 28.196 % |
c |     99457 |    3072    12098 |    1381    1073     9183     8.6 | 29.073 % |
c |     99796 |    3072    12098 |    1519    1412    12819     9.1 | 29.073 % |
c |    100303 |    3072    12098 |    1671    1029     8362     8.1 | 29.073 % |
c |    101062 |    3059    12052 |    1838    1746    19490    11.2 | 29.574 % |
c ==============================================================================
c [1mFound solution: 43134[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 69476   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    101216 |    3063    12080 |    1021    1900    21400    11.3 | 29.574 % |
c |    101317 |    3063    12080 |    1123    1051     8753     8.3 | 29.676 % |
c |    101467 |    3063    12080 |    1235    1201    10284     8.6 | 29.676 % |
c |    101692 |    3063    12080 |    1358    1426    12550     8.8 | 29.676 % |
c |    102029 |    3063    12080 |    1494     889     7289     8.2 | 29.676 % |
c |    102535 |    3063    12080 |    1644    1395    12027     8.6 | 29.676 % |
c |    103294 |    3063    12080 |    1808    1194    10058     8.4 | 29.676 % |
c |    104433 |    3063    12080 |    1989    1288    10661     8.3 | 29.676 % |
c |    106141 |    3063    12080 |    2188    1846    23922    13.0 | 29.676 % |
c |    108703 |    3063    12080 |    2407    1811    24558    13.6 | 29.676 % |
c ==============================================================================
c [1mFound solution: 43130[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 69480   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    109777 |    3067    12110 |    1022    1507    16124    10.7 | 29.676 % |
c |    109877 |    3067    12110 |    1124     854     6783     7.9 | 29.777 % |
c |    110027 |    3067    12110 |    1236    1004     8608     8.6 | 29.777 % |
c |    110252 |    3067    12110 |    1360    1229    11295     9.2 | 29.777 % |
c |    110592 |    3067    12110 |    1496    1569    14612     9.3 | 29.777 % |
c |    111098 |    3067    12110 |    1645    1199    10422     8.7 | 29.777 % |
c |    111858 |    3067    12110 |    1810    1959    22285    11.4 | 29.778 % |
c |    112997 |    3067    12110 |    1991    2055    23151    11.3 | 29.777 % |
c ==============================================================================
c [1mFound solution: 43129[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 69481   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    113790 |    3065    12109 |    1021    1559    16714    10.7 | 29.777 % |
c |    113891 |    3065    12109 |    1123     881     6587     7.5 | 29.951 % |
c |    114041 |    3065    12109 |    1235    1031     8912     8.6 | 29.951 % |
c |    114267 |    3065    12109 |    1358    1257    11248     8.9 | 29.951 % |
c |    114605 |    3065    12109 |    1494    1595    16784    10.5 | 29.951 % |
c ==============================================================================
c [1mFound solution: 43125[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 69485   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    114980 |    3069    12138 |    1023    1074     9376     8.7 | 29.951 % |
c |    115080 |    3069    12138 |    1125    1174    11041     9.4 | 30.049 % |
c |    115230 |    3069    12138 |    1237    1324    13559    10.2 | 30.049 % |
c |    115455 |    3069    12138 |    1361     786     5191     6.6 | 30.049 % |
c |    115792 |    3069    12138 |    1497    1123     8906     7.9 | 30.050 % |
c ==============================================================================
c [1mFound solution: 43120[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 69490   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    115915 |    3075    12177 |    1025    1246    10415     8.4 | 30.050 % |
c |    116015 |    3075    12177 |    1127     697     4192     6.0 | 30.196 % |
c |    116165 |    3075    12177 |    1240     847     6495     7.7 | 30.196 % |
c |    116390 |    3075    12177 |    1364    1072     8856     8.3 | 30.196 % |
c ==============================================================================
c [1mFound solution: 43114[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 69496   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    116665 |    3079    12203 |    1026    1347    12178     9.0 | 30.196 % |
c |    116765 |    3079    12203 |    1128     774     5134     6.6 | 30.292 % |
c |    116915 |    3079    12203 |    1241     924     6570     7.1 | 30.293 % |
c ==============================================================================
c [1mFound solution: 43107[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 69503   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    116948 |    3081    12212 |    1027     957     7047     7.4 | 30.293 % |
c |    117048 |    3081    12212 |    1129    1057     8302     7.9 | 30.340 % |
c |    117198 |    3081    12212 |    1242    1207     9946     8.2 | 30.340 % |
c |    117423 |    3081    12212 |    1366    1432    11932     8.3 | 30.340 % |
c ==============================================================================
c [1mFound solution: 43104[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 69506   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    117737 |    3085    12240 |    1028     921     6599     7.2 | 30.340 % |
c |    117838 |    3085    12240 |    1130    1022     7542     7.4 | 30.435 % |
c ==============================================================================
c [1mFound solution: 43103[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 69507   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    117864 |    3087    12252 |    1029    1048     7938     7.6 | 30.435 % |
c |    117964 |    3087    12252 |    1131    1148     9146     8.0 | 30.482 % |
c |    118114 |    3087    12252 |    1245    1298    10944     8.4 | 30.482 % |
c |    118339 |    3087    12252 |    1369    1523    14090     9.3 | 30.483 % |
c |    118676 |    3087    12252 |    1506    1045     7022     6.7 | 30.485 % |
c |    119182 |    3087    12252 |    1657    1551    16507    10.6 | 30.484 % |
c ==============================================================================
c [1mFound solution: 43097[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 69513   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    119553 |    3090    12277 |    1030    1922    20480    10.7 | 30.484 % |
c |    119653 |    3090    12277 |    1133    1061     8172     7.7 | 30.612 % |
c |    119804 |    3090    12277 |    1246    1212    10505     8.7 | 30.612 % |
c |    120030 |    3090    12277 |    1370    1438    13896     9.7 | 30.612 % |
c |    120367 |    3080    12239 |    1508     914     6363     7.0 | 30.732 % |
c |    120873 |    3080    12239 |    1658    1420    14233    10.0 | 30.732 % |
c |    121632 |    3080    12239 |    1824    1201     9784     8.1 | 30.732 % |
c |    122774 |    3080    12239 |    2007    1248    11579     9.3 | 30.733 % |
c |    124482 |    3080    12239 |    2207    1814    20475    11.3 | 30.732 % |
c |    127044 |    3064    12179 |    2428    1203    10272     8.5 | 30.853 % |
c ==============================================================================
c [1mOptimal solution: 43097[0m
s OPTIMUM FOUND
v -VOL1_bit_7 -VOL1_bit_6 VOL1_bit_5 VOL1_bit_4 -VOL1_bit_3 VOL1_bit_2 -VOL1_bit_1 VOL1_bit0 VOL1_bit1 -VOL1_bit2 -VOL1_bit3 -VOL1_bit4 -VOL1_bit5 -VOL1_bit6 -VOL1_bit7 -VOL1_bit8 -VOL1_bit9 -VOL1_bit10 -VOL1_bit11 -VOL1_bit12 VOL2_bit_7 -VOL2_bit_6 -VOL2_bit_5 VOL2_bit_4 -VOL2_bit_3 VOL2_bit_2 -VOL2_bit_1 VOL2_bit0 -VOL2_bit1 VOL2_bit2 VOL2_bit3 -VOL2_bit4 -VOL2_bit5 -VOL2_bit6 -VOL2_bit7 -VOL2_bit8 -VOL2_bit9 -VOL2_bit10 -VOL2_bit11 -VOL2_bit12 -VOL3_bit_7 -VOL3_bit_6 -VOL3_bit_5 -VOL3_bit_4 -VOL3_bit_3 -VOL3_bit_2 -VOL3_bit_1 -VOL3_bit0 VOL3_bit1 VOL3_bit2 VOL3_bit3 VOL3_bit4 -VOL4_bit_7 -VOL4_bit_6 -VOL4_bit_5 -VOL4_bit_4 -VOL4_bit_3 -VOL4_bit_2 -VOL4_bit_1 -VOL4_bit0 -VOL4_bit1 -VOL4_bit2 -VOL4_bit3 -VOL4_bit4
c _______________________________________________________________________________
c 
c restarts              : 229
c conflicts             : 129875         (5586 /sec)
c decisions             : 164401         (7071 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 23.2495 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.71 0.92 0.90 2/54 15693
Raw data (stat): 15693 (runsolver) R 15692 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 482066743 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+10.0006 s]
Raw data (loadavg): 0.76 0.92 0.91 2/54 15693
Raw data (stat): 15693 (minisat+) R 15692 25285 25284 0 -1 0 485 0 0 0 997 1 0 0 25 0 1 0 482066743 3608576 463 4294967295 134512640 134672761 3221224544 3221223712 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 881 463 603 41 0 840 0
vsize: 3524
[startup+20.0016 s]
Raw data (loadavg): 0.79 0.92 0.91 2/54 15693
Raw data (stat): 15693 (minisat+) R 15692 25285 25284 0 -1 0 514 0 0 0 1996 2 0 0 25 0 1 0 482066743 3608576 492 4294967295 134512640 134672761 3221224544 3221223640 1075347230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 881 492 603 41 0 840 0
vsize: 3524
[startup+23.3004 s]
Raw data (loadavg): 0.79 0.92 0.91 1/53 15693
Raw data (stat): 15693 (minisat+) R 15692 25285 25284 0 -1 0 514 0 0 0 1996 2 0 0 25 0 1 0 482066743 3608576 492 4294967295 134512640 134672761 3221224544 3221223640 1075347230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 881 492 603 41 0 840 0
vsize: 0

Child status: 30
Real time (s): 23.2995
CPU time (s): 23.2815
CPU user time (s): 23.2515
CPU system time (s): 0.029995
CPU usage (%): 99.9226
Max. virtual memory (Kb): 3524
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	43097
#### END VERIFIER DATA ####