PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/submitted/manquinho/routing/normalized-s4-4-3-9pb.opb
MD5SUM	7d64f372313e74de659e9e56ab2d9bab
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	68
Optimality of the best value was proved	NO
Number of terms in the objective function	840
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	840
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	3
Number of bits of the biggest number in a constraint	2
Biggest sum of numbers in a constraint	840
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04684
Number of variables	840
Total number of constraints	2526
Number of constraints which are clauses	2502
Number of constraints which are cardinality constraints (but not clauses)	24
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	35
Trace number 5133

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-04-13 22:24:15 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3629 boxname=wulflinc5 idbench=245 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  7d64f372313e74de659e9e56ab2d9bab  /oldhome/oroussel/tmp/wulflinc5/normalized-s4-4-3-9pb.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc5/normalized-s4-4-3-9pb.opb /oldhome/oroussel/tmp/wulflinc5/normalized-s4-4-3-9pb.opb
IDLAUNCH: 3629
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        904576 kB
Buffers:         33488 kB
Cached:          75284 kB
SwapCached:       2272 kB
Active:          52916 kB
Inactive:        61040 kB
HighTotal:      131008 kB
HighFree:        51772 kB
LowTotal:       903652 kB
LowFree:        852804 kB
SwapTotal:     2097136 kB
SwapFree:      2094864 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10604 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 22:25:45 (client local time) WITH STATUS 30 IN 89.8233 SECONDS
stats: 3629 0 89.8233 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2526 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ############################################################################################################################################
c   -- Clauses(.)/Splits(s): ..............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[2520]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2503]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2465]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2455]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2449]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2431]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2393]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2383]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2377]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2359]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2321]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2311]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2309]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2283]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2265]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2239]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2206]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2180]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2178]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2168]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2151]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2129]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2103]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2097]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2079]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2057]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2031]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2025]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2007]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1985]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1959]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1953]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1935]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1913]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1887]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1881]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1871]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1861]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1812]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1810]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1758]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1748]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1742]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1740]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1692]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1682]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1672]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1670]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1664]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1646]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1609]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1599]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1593]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1575]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1537]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1527]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1513]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1487]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1465]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1455]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1422]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1396]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1394]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1384]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1378]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1360]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1322]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1312]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1298]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1272]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1250]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1240]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1234]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1216]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1178]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1168]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1135]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1109]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1107]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1097]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1079]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1057]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1031]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1025]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1007]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 985]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 959]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 953]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 935]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 913]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 887]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 881]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 875]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 858]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 820]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 810]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 808]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 782]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 764]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 738]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 724]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 698]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 676]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 666]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 652]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 627]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 605]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 595]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 593]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 567]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 549]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 523]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 521]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 495]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 477]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 451]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 438]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 412]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 390]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 380]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 378]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 352]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 334]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 308]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 306]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 280]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 262]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 236]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 188]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 178]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 168]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 166]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 156]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 146]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  96]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  94]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  42]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  32]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  26]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  24]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  23]---> Adder-cost: 64   maxlim: 31   bits: 6/5
c ---[  22]---> Adder-cost: 64   maxlim: 31   bits: 6/5
c ---[  21]---> Adder-cost: 64   maxlim: 31   bits: 6/5
c ---[  20]---> Adder-cost: 64   maxlim: 31   bits: 6/5
c ---[  19]---> Adder-cost: 64   maxlim: 31   bits: 6/5
c ---[  18]---> Adder-cost: 64   maxlim: 31   bits: 6/5
c ---[  17]---> Adder-cost: 64   maxlim: 31   bits: 6/5
c ---[  16]---> Adder-cost: 64   maxlim: 31   bits: 6/5
c ---[  15]---> Adder-cost: 64   maxlim: 31   bits: 6/5
c ---[  14]---> Adder-cost: 64   maxlim: 31   bits: 6/5
c ---[  13]---> Adder-cost: 64   maxlim: 31   bits: 6/5
c ---[  12]---> Adder-cost: 64   maxlim: 31   bits: 6/5
c ---[  11]---> Adder-cost: 64   maxlim: 31   bits: 6/5
c ---[  10]---> Adder-cost: 64   maxlim: 31   bits: 6/5
c ---[   9]---> Adder-cost: 64   maxlim: 31   bits: 6/5
c ---[   8]---> Adder-cost: 64   maxlim: 31   bits: 6/5
c ---[   7]---> Adder-cost: 64   maxlim: 31   bits: 6/5
c ---[   6]---> Adder-cost: 64   maxlim: 31   bits: 6/5
c ---[   5]---> Adder-cost: 64   maxlim: 31   bits: 6/5
c ---[   4]---> Adder-cost: 64   maxlim: 31   bits: 6/5
c ---[   3]---> Adder-cost: 64   maxlim: 31   bits: 6/5
c ---[   2]---> Adder-cost: 64   maxlim: 31   bits: 6/5
c ---[   1]---> Adder-cost: 64   maxlim: 31   bits: 6/5
c ---[   0]---> Adder-cost: 64   maxlim: 31   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   11642    40106 |    3880       0        0     nan |  0.000 % |
c |       100 |   11642    40106 |    4268     100      402     4.0 | 20.548 % |
c |       251 |   11530    39734 |    4694     236     1060     4.5 | 21.309 % |
c |       477 |   11310    39008 |    5164     425     2377     5.6 | 22.869 % |
c |       815 |   11247    38799 |    5680     754     6028     8.0 | 23.288 % |
c |      1321 |   11207    38665 |    6248    1255    14181    11.3 | 23.554 % |
c |      2080 |   10976    37904 |    6873    1980    24285    12.3 | 25.114 % |
c |      3220 |   10758    37178 |    7561    3089    38118    12.3 | 26.636 % |
c |      4928 |   10595    36637 |    8317    4771    72404    15.2 | 27.778 % |
c |      7490 |   10355    35847 |    9148    7296   119498    16.4 | 29.528 % |
c |     11334 |   10213    35377 |   10063    6057    90144    14.9 | 30.441 % |
c |     17100 |   10064    34870 |   11070    6176   120431    19.5 | 31.279 % |
c |     25749 |    9974    34566 |   12177    8816   169376    19.2 | 31.736 % |
c |     38723 |    9939    34449 |   13394    8674   150402    17.3 | 31.887 % |
c |     58187 |    9861    34185 |   14734   13776   246001    17.9 | 32.344 % |
c ==============================================================================
c [1mFound solution: 72[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1630   maxlim: 748   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     65044 |   21202    74687 |    7067   12768   240753    18.9 | 32.344 % |
c |     65144 |   21202    74687 |    7773    6484   105126    16.2 | 20.192 % |
c |     65294 |   21202    74687 |    8551    6634   107543    16.2 | 20.192 % |
c |     65519 |   21202    74687 |    9406    6859   112733    16.4 | 20.192 % |
c |     65856 |   21202    74687 |   10346    7196   118924    16.5 | 20.192 % |
c |     66364 |   21202    74687 |   11381    7704   126833    16.5 | 20.192 % |
c |     67125 |   21202    74687 |   12519    8465   140692    16.6 | 20.192 % |
c ==============================================================================
c [1mFound solution: 70[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 750   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     67828 |   21206    74712 |    7068    9168   171267    18.7 | 20.192 % |
c |     67931 |   21206    74712 |    7774    4687    71458    15.2 | 20.230 % |
c |     68081 |   21206    74712 |    8552    4837    74317    15.4 | 20.230 % |
c |     68307 |   21206    74712 |    9407    5063    78865    15.6 | 20.230 % |
c |     68645 |   21206    74712 |   10348    5401    84960    15.7 | 20.230 % |
c |     69151 |   21206    74712 |   11383    5907    92495    15.7 | 20.230 % |
c |     69910 |   21206    74712 |   12521    6666   107208    16.1 | 20.230 % |
c |     71050 |   21206    74712 |   13773    7806   127319    16.3 | 20.230 % |
c |     72758 |   21206    74712 |   15150    9514   160842    16.9 | 20.230 % |
c |     75320 |   21197    74681 |   16665   12071   206563    17.1 | 20.253 % |
c |     79164 |   21188    74650 |   18332   15908   294591    18.5 | 20.277 % |
c |     84931 |   21110    74378 |   20165   11591   371719    32.1 | 20.417 % |
c |     93581 |   21104    74358 |   22182   20237   893173    44.1 | 20.441 % |
c ==============================================================================
c [1mFound solution: 68[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1608   maxlim: 747   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     94960 |   32308   114363 |   10769   21614  1000689    46.3 | 20.441 % |
c |     95060 |   32308   114363 |   11845   10907   443007    40.6 | 14.957 % |
c |     95210 |   32308   114363 |   13030   11057   451892    40.9 | 14.957 % |
c |     95438 |   32308   114363 |   14333   11285   455906    40.4 | 14.957 % |
c |     95776 |   32308   114363 |   15766   11623   485502    41.8 | 14.957 % |
c |     96283 |   32286   114285 |   17343   12117   531520    43.9 | 14.974 % |
c |     97044 |   32260   114195 |   19077   12872   565957    44.0 | 15.042 % |
c |     98183 |   32232   114103 |   20985   14006   661130    47.2 | 15.127 % |
c |     99891 |   32232   114103 |   23084   15714   814338    51.8 | 15.127 % |
c |    102454 |   32232   114103 |   25392   18277   927318    50.7 | 15.127 % |
c |    106299 |   32232   114103 |   27932   22122  1229521    55.6 | 15.127 % |
c |    112065 |   32223   114072 |   30725   27885  1748847    62.7 | 15.144 % |
c ==============================================================================
c [1mOptimal solution: 68[0m
s OPTIMUM FOUND
v -v1 -v2 -v3 -v4 -v5 -v6 -v7 -v8 v9 -v10 -v11 -v12 -v13 -v14 -v15 -v16 -v17 -v18 -v19 -v20 -v21 -v22 -v23 -v24 -v25 -v26 v27 -v28 -v29 -v30 v31 v32 -v33 -v34 -v35 -v36 -v37 -v38 v39 -v40 -v41 -v42 v43 -v44 -v45 -v46 -v47 -v48 -v49 -v50 -v51 -v52 -v53 -v54 -v55 -v56 -v57 -v58 -v59 -v60 -v61 -v62 -v63 -v64 v65 -v66 -v67 -v68 -v69 -v70 -v71 -v72 v73 v74 v75 -v76 -v77 -v78 -v79 -v80 -v81 -v82 -v83 -v84 -v85 -v86 -v87 -v88 -v89 -v90 -v91 -v92 -v93 -v94 -v95 -v96 -v97 -v98 -v99 -v100 -v101 -v102 -v103 -v104 v105 -v106 -v107 -v108 -v109 -v110 -v111 -v112 -v113 -v114 -v115 v116 -v117 -v118 -v119 -v120 -v121 -v122 -v123 -v124 -v125 -v126 -v127 -v128 -v129 -v130 -v131 -v132 -v133 v134 -v135 -v136 -v137 -v138 -v139 -v140 -v141 -v142 -v143 -v144 -v145 -v146 -v147 -v148 -v149 -v150 -v151 -v152 -v153 -v154 v155 v156 -v157 -v158 -v159 -v160 -v161 -v162 -v163 -v164 -v165 -v166 -v167 v168 v169 -v170 -v171 -v172 -v173 -v174 -v175 -v176 -v177 -v178 -v179 -v180 -v181 v182 -v183 -v184 -v185 v186 -v187 -v188 -v189 v190 -v191 -v192 -v193 -v194 -v195 v196 -v197 -v198 -v199 -v200 -v201 -v202 -v203 -v204 v205 -v206 -v207 -v208 -v209 v210 -v211 -v212 -v213 v214 -v215 -v216 -v217 -v218 -v219 -v220 -v221 -v222 v223 -v224 -v225 -v226 -v227 -v228 -v229 -v230 -v231 -v232 v233 -v234 -v235 -v236 -v237 -v238 -v239 -v240 -v241 -v242 -v243 -v244 -v245 -v246 -v247 -v248 -v249 -v250 -v251 -v252 -v253 -v254 -v255 -v256 -v257 v258 -v259 -v260 -v261 -v262 -v263 -v264 -v265 -v266 -v267 -v268 -v269 -v270 -v271 -v272 -v273 -v274 -v275 -v276 -v277 -v278 -v279 -v280 -v281 -v282 v283 -v284 -v285 -v286 -v287 -v288 -v289 -v290 -v291 v292 v293 -v294 -v295 -v296 -v297 -v298 -v299 -v300 -v301 -v302 -v303 -v304 v305 -v306 -v307 -v308 -v309 -v310 -v311 -v312 -v313 -v314 -v315 -v316 -v317 -v318 -v319 -v320 -v321 -v322 -v323 v324 -v325 -v326 -v327 -v328 -v329 -v330 -v331 -v332 -v333 -v334 -v335 v336 -v337 -v338 v339 -v340 -v341 -v342 -v343 -v344 -v345 -v346 -v347 -v348 -v349 -v350 -v351 -v352 -v353 -v354 -v355 -v356 -v357 -v358 -v359 -v360 -v361 -v362 -v363 -v364 -v365 -v366 -v367 -v368 -v369 -v370 -v371 -v372 -v373 -v374 v375 -v376 -v377 -v378 v379 -v380 -v381 -v382 -v383 -v384 -v385 -v386 -v387 -v388 -v389 -v390 -v391 -v392 -v393 -v394 -v395 -v396 -v397 -v398 -v399 -v400 -v401 -v402 -v403 -v404 v405 -v406 -v407 -v408 -v409 v410 -v411 -v412 -v413 v414 -v415 -v416 -v417 -v418 -v419 v420 -v421 -v422 v423 -v424 -v425 -v426 -v427 v428 -v429 -v430 -v431 v432 -v433 -v434 -v435 -v436 -v437 -v438 -v439 -v440 -v441 -v442 -v443 -v444 -v445 -v446 -v447 -v448 -v449 -v450 -v451 -v452 v453 -v454 -v455 -v456 -v457 -v458 -v459 -v460 -v461 -v462 -v463 -v464 v465 -v466 -v467 -v468 -v469 -v470 -v471 -v472 -v473 -v474 -v475 v476 -v477 -v478 -v479 -v480 -v481 -v482 -v483 v484 -v485 -v486 -v487 -v488 -v489 -v490 -v491 -v492 -v493 v494 -v495 -v496 -v497 -v498 -v499 -v500 -v501 -v502 -v503 -v504 -v505 -v506 -v507 -v508 -v509 -v510 -v511 -v512 -v513 v514 -v515 -v516 -v517 -v518 -v519 -v520 -v521 -v522 -v523 -v524 v525 -v526 -v527 -v528 -v529 -v530 -v531 -v532 -v533 -v534 -v535 -v536 -v537 -v538 v539 -v540 -v541 -v542 -v543 -v544 -v545 -v546 -v547 -v548 -v549 -v550 -v551 -v552 -v553 -v554 -v555 -v556 -v557 -v558 v559 -v560 -v561 -v562 -v563 -v564 -v565 -v566 -v567 -v568 -v569 -v570 -v571 -v572 -v573 -v574 -v575 -v576 v577 v578 -v579 -v580 -v581 -v582 -v583 -v584 -v585 -v586 -v587 -v588 -v589 -v590 -v591 -v592 -v593 -v594 -v595 -v596 -v597 -v598 -v599 -v600 -v601 -v602 -v603 -v604 -v605 -v606 -v607 v608 -v609 -v610 -v611 -v612 -v613 -v614 -v615 -v616 -v617 -v618 -v619 -v620 -v621 v622 v623 -v624 -v625 -v626 -v627 -v628 -v629 -v630 -v631 v632 -v633 -v634 -v635 -v636 -v637 -v638 -v639 -v640 -v641 -v642 -v643 -v644 -v645 -v646 v647 -v648 -v649 -v650 -v651 -v652 -v653 -v654 -v655 -v656 -v657 -v658 -v659 -v660 -v661 -v662 -v663 v664 -v665 -v666 -v667 -v668 -v669 -v670 -v671 -v672 -v673 -v674 -v675 -v676 -v677 -v678 -v679 -v680 -v681 v682 v683 -v684 -v685 -v686 -v687 -v688 -v689 -v690 -v691 -v692 -v693 -v694 -v695 -v696 -v697 -v698 -v699 -v700 -v701 -v702 -v703 -v704 -v705 -v706 -v707 -v708 -v709 -v710 -v711 -v712 -v713 -v714 -v715 -v716 -v717 -v718 v719 -v720 -v721 -v722 -v723 -v724 -v725 -v726 -v727 -v728 -v729 v730 -v731 -v732 -v733 -v734 -v735 -v736 -v737 -v738 -v739 -v740 -v741 -v742 -v743 -v744 -v745 -v746 -v747 -v748 -v749 -v750 -v751 -v752 -v753 -v754 -v755 -v756 -v757 -v758 -v759 v760 -v761 -v762 -v763 -v764 -v765 -v766 -v767 -v768 -v769 -v770 -v771 -v772 v773 -v774 -v775 -v776 -v777 -v778 -v779 -v780 -v781 -v782 -v783 -v784 -v785 -v786 -v787 -v788 -v789 -v790 -v791 -v792 -v793 -v794 -v795 -v796 -v797 -v798 -v799 -v800 -v801 -v802 -v803 -v804 -v805 -v806 -v807 v808 -v809 -v810 -v811 -v812 -v813 -v814 -v815 -v816 -v817 -v818 -v819 -v820 v821 -v822 -v823 -v824 -v825 -v826 -v827 -v828 -v829 -v830 -v831 -v832 -v833 -v834 -v835 -v836 -v837 -v838 -v839 -v840
c _______________________________________________________________________________
c 
c restarts              : 47
c conflicts             : 115983         (1293 /sec)
c decisions             : 269899         (3009 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 89.6924 s
c _______________________________________________________________________________
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.97 0.91 2/54 26733
Raw data (stat): 26733 (runsolver) R 26732 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421306011 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 26733
Raw data (stat): 26733 (minisat+) R 26732 24215 24214 0 -1 0 1010 0 0 0 996 2 0 0 25 0 1 0 421306011 5754880 988 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1405 988 603 41 0 1364 0
vsize: 5620
[startup+20.0012 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 26733
Raw data (stat): 26733 (minisat+) R 26732 24215 24214 0 -1 0 1076 0 0 0 1995 2 0 0 25 0 1 0 421306011 6045696 1054 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1476 1054 603 41 0 1435 0
vsize: 5904
[startup+30.0016 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 26733
Raw data (stat): 26733 (minisat+) R 26732 24215 24214 0 -1 0 1288 0 0 0 2994 3 0 0 25 0 1 0 421306011 6942720 1266 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1695 1266 603 41 0 1654 0
vsize: 6780
[startup+40.002 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 26733
Raw data (stat): 26733 (minisat+) R 26732 24215 24214 0 -1 0 1693 0 0 0 3992 5 0 0 25 0 1 0 421306011 8687616 1671 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2121 1671 603 41 0 2080 0
vsize: 8484
[startup+50.0024 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 26733
Raw data (stat): 26733 (minisat+) R 26732 24215 24214 0 -1 0 2332 0 0 0 4991 6 0 0 25 0 1 0 421306011 11296768 2310 4294967295 134512640 134672761 3221224560 3221223664 134554671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2758 2310 603 41 0 2717 0
vsize: 11032
[startup+60.0026 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 26733
Raw data (stat): 26733 (minisat+) R 26732 24215 24214 0 -1 0 2333 0 0 0 5991 6 0 0 25 0 1 0 421306011 11296768 2311 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2758 2311 603 41 0 2717 0
vsize: 11032
[startup+70.0036 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 26733
Raw data (stat): 26733 (minisat+) R 26732 24215 24214 0 -1 0 2685 0 0 0 6990 8 0 0 25 0 1 0 421306011 12763136 2663 4294967295 134512640 134672761 3221224560 3221223728 134560813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3116 2663 603 41 0 3075 0
vsize: 12464
[startup+80.0038 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 26733
Raw data (stat): 26733 (minisat+) R 26732 24215 24214 0 -1 0 3151 0 0 0 7987 10 0 0 25 0 1 0 421306011 14630912 3129 4294967295 134512640 134672761 3221224560 3221223664 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3572 3129 603 41 0 3531 0
vsize: 14288
[startup+89.8493 s]
Raw data (loadavg): 1.03 0.99 0.92 1/53 26733
Raw data (stat): 26733 (minisat+) R 26732 24215 24214 0 -1 0 3151 0 0 0 7987 10 0 0 25 0 1 0 421306011 14630912 3129 4294967295 134512640 134672761 3221224560 3221223664 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3572 3129 603 41 0 3531 0
vsize: 0

Child status: 30
Real time (s): 89.8487
CPU time (s): 89.8233
CPU user time (s): 89.6984
CPU system time (s): 0.124981
CPU usage (%): 99.9717
Max. virtual memory (Kb): 14288
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	68
#### END VERIFIER DATA ####