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/web/www.ps.uni-sb.de/~walser/benchmarks/course-ass/normalized-ss97-6.opb
MD5SUM	5d90b7cbb5bac2aa14257b9c5448f25d
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	304
Optimality of the best value was proved	NO
Number of terms in the objective function	173
Biggest coefficient in the objective function	100
Number of bits for the biggest coefficient in the objective function	7
Sum of the numbers in the objective function	8448
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	100
Number of bits of the biggest number in a constraint	7
Biggest sum of numbers in a constraint	8448
Number of bits of the biggest sum of numbers	14
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.05184
Number of variables	257
Total number of constraints	353
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	353
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	44
Trace number 5243

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-13 23:13:38 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3740 boxname=wulflinc20 idbench=356 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  5d90b7cbb5bac2aa14257b9c5448f25d  /oldhome/oroussel/tmp/wulflinc20/normalized-ss97-6.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc20/normalized-ss97-6.opb /oldhome/oroussel/tmp/wulflinc20/normalized-ss97-6.opb
IDLAUNCH: 3740
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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	: 3
cpu MHz		: 451.215
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        890848 kB
Buffers:         33784 kB
Cached:          74624 kB
SwapCached:       2636 kB
Active:          47584 kB
Inactive:        66304 kB
HighTotal:      131008 kB
HighFree:        52668 kB
LowTotal:       903652 kB
LowFree:        838180 kB
SwapTotal:     2097892 kB
SwapFree:      2095256 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            24260 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:14:01 (client local time) WITH STATUS 30 IN 22.7275 SECONDS
stats: 3740 0 22.7275 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 180 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 179]---> Adder-cost: 82   maxlim: 31   bits: 6/5
c ---[ 178]---> Adder-cost: 82   maxlim: 31   bits: 6/5
c ---[ 177]---> Adder-cost: 82   maxlim: 31   bits: 6/5
c ---[ 176]---> Adder-cost: 82   maxlim: 31   bits: 6/5
c ---[ 175]---> Adder-cost: 76   maxlim: 17   bits: 6/5
c ---[ 174]---> Adder-cost: 76   maxlim: 17   bits: 6/5
c ---[ 173]---> Adder-cost: 17   maxlim: 7   bits: 4/3
c ---[ 172]---> Adder-cost: 17   maxlim: 7   bits: 4/3
c ---[ 171]---> Adder-cost: 17   maxlim: 7   bits: 4/3
c ---[ 170]---> Adder-cost: 17   maxlim: 7   bits: 4/3
c ---[ 169]---> Adder-cost: 19   maxlim: 16   bits: 6/5
c ---[ 168]---> Adder-cost: 19   maxlim: 16   bits: 6/5
c ---[ 166]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 164]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 162]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 160]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 158]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 156]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 154]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 152]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 150]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 148]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 146]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 144]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 142]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 140]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 138]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 136]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 134]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 132]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 130]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 128]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 126]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 124]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 122]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 120]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 118]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 116]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 114]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 112]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 110]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 108]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 106]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 104]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 102]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 100]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  98]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  96]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  94]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  92]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  90]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  88]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  86]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  84]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  82]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  80]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  78]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  76]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  74]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  72]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  70]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  68]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  66]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  64]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  62]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  60]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  58]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  56]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  54]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  52]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  50]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  48]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  46]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  44]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  42]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  40]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  38]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  36]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  34]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  32]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  30]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  28]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  26]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  24]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  22]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  20]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  18]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  16]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  14]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  12]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  10]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[   8]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[   6]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[   4]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[   2]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[   0]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    4480    15490 |    1493       0        0     nan |  0.000 % |
c |       100 |    4480    15490 |    1642     100      390     3.9 | 28.449 % |
c |       250 |    4464    15446 |    1806     248     1013     4.1 | 28.761 % |
c |       478 |    4464    15446 |    1987     476     4341     9.1 | 28.761 % |
c ==============================================================================
c [1mFound solution: 1725[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 508   maxlim: 6634   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       684 |    7929    27824 |    2643     680     6354     9.3 | 28.761 % |
c |       785 |    7929    27824 |    2907     781     7679     9.8 | 21.222 % |
c |       937 |    7929    27824 |    3198     933     9860    10.6 | 21.222 % |
c |      1162 |    7929    27824 |    3517    1158    14835    12.8 | 21.222 % |
c |      1499 |    7883    27692 |    3869    1490    17954    12.0 | 21.778 % |
c ==============================================================================
c [1mFound solution: 1723[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 6636   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1513 |    7889    27736 |    2629    1504    18406    12.2 | 21.778 % |
c |      1613 |    7889    27736 |    2891    1604    18795    11.7 | 21.865 % |
c |      1764 |    7853    27610 |    3181    1745    20955    12.0 | 22.031 % |
c |      1989 |    7853    27610 |    3499    1970    23892    12.1 | 22.031 % |
c |      2326 |    7824    27518 |    3849    2302    26426    11.5 | 22.253 % |
c |      2832 |    7824    27518 |    4234    2808    37703    13.4 | 22.253 % |
c |      3593 |    7795    27415 |    4657    3481    53069    15.2 | 22.420 % |
c |      4732 |    7763    27309 |    5123    4601    77423    16.8 | 22.642 % |
c |      6441 |    7763    27309 |    5635    3494    65939    18.9 | 22.642 % |
c ==============================================================================
c [1mFound solution: 1221[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7138   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7941 |    7767    27368 |    2589    4993   106543    21.3 | 22.642 % |
c |      8042 |    7751    27324 |    2847    2596    45304    17.5 | 23.234 % |
c |      8193 |    7751    27324 |    3132    2747    47003    17.1 | 23.234 % |
c |      8422 |    7743    27302 |    3445    2975    50282    16.9 | 23.344 % |
c |      8759 |    7743    27302 |    3790    3312    59456    18.0 | 23.344 % |
c |      9265 |    7743    27302 |    4169    3818    66970    17.5 | 23.344 % |
c ==============================================================================
c [1mFound solution: 1116[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7243   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9807 |    7750    27349 |    2583    4360    76289    17.5 | 23.344 % |
c |      9909 |    7750    27349 |    2841    2282    26206    11.5 | 23.500 % |
c |     10060 |    7750    27349 |    3125    2433    29342    12.1 | 23.500 % |
c |     10287 |    7719    27251 |    3437    2650    32609    12.3 | 23.831 % |
c |     10628 |    7719    27251 |    3781    2991    39109    13.1 | 23.831 % |
c ==============================================================================
c [1mFound solution: 824[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7535   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10953 |    7723    27288 |    2574    3316    43739    13.2 | 23.831 % |
c |     11053 |    7714    27257 |    2831    1751    14942     8.5 | 24.053 % |
c |     11203 |    7714    27257 |    3114    1901    16155     8.5 | 24.053 % |
c |     11429 |    7714    27257 |    3425    2127    19824     9.3 | 24.053 % |
c |     11766 |    7714    27257 |    3768    2464    26166    10.6 | 24.053 % |
c ==============================================================================
c [1mFound solution: 816[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7543   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11992 |    7717    27275 |    2572    2690    29933    11.1 | 24.053 % |
c |     12093 |    7717    27275 |    2829    2791    31308    11.2 | 24.094 % |
c |     12243 |    7708    27244 |    3112    2916    34015    11.7 | 24.149 % |
c ==============================================================================
c [1mFound solution: 814[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7545   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12400 |    7710    27260 |    2570    3073    36254    11.8 | 24.149 % |
c |     12500 |    7710    27260 |    2827    1637    14400     8.8 | 24.178 % |
c |     12650 |    7710    27260 |    3109    1787    16556     9.3 | 24.178 % |
c |     12875 |    7710    27260 |    3420    2012    20355    10.1 | 24.178 % |
c ==============================================================================
c [1mFound solution: 813[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7546   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13031 |    7712    27276 |    2570    2168    23073    10.6 | 24.178 % |
c |     13132 |    7712    27276 |    2827    2269    24178    10.7 | 24.206 % |
c |     13282 |    7712    27276 |    3109    2419    27325    11.3 | 24.206 % |
c |     13507 |    7712    27276 |    3420    2644    30644    11.6 | 24.207 % |
c |     13846 |    7712    27276 |    3762    2983    36544    12.3 | 24.206 % |
c |     14354 |    7712    27276 |    4139    3491    47596    13.6 | 24.206 % |
c |     15114 |    7712    27276 |    4552    4251    63826    15.0 | 24.206 % |
c ==============================================================================
c [1mFound solution: 812[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7547   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15477 |    7713    27289 |    2571    4614    69468    15.1 | 24.206 % |
c |     15577 |    7713    27289 |    2828    2407    31348    13.0 | 24.247 % |
c |     15727 |    7713    27289 |    3110    2557    32763    12.8 | 24.247 % |
c |     15953 |    7713    27289 |    3422    2783    37357    13.4 | 24.248 % |
c ==============================================================================
c [1mFound solution: 811[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7548   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16189 |    7715    27306 |    2571    3019    41366    13.7 | 24.248 % |
c |     16290 |    7715    27306 |    2828    1611    13656     8.5 | 24.276 % |
c |     16440 |    7715    27306 |    3110    1761    16055     9.1 | 24.276 % |
c |     16666 |    7715    27306 |    3422    1987    19487     9.8 | 24.276 % |
c |     17003 |    7715    27306 |    3764    2324    26470    11.4 | 24.276 % |
c |     17509 |    7715    27306 |    4140    2830    36599    12.9 | 24.276 % |
c |     18268 |    7715    27306 |    4554    3589    50769    14.1 | 24.276 % |
c |     19408 |    7715    27306 |    5010    4729    80580    17.0 | 24.276 % |
c ==============================================================================
c [1mFound solution: 810[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7549   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19675 |    7716    27320 |    2572    4996    85422    17.1 | 24.276 % |
c |     19775 |    7716    27320 |    2829    2598    40614    15.6 | 24.317 % |
c |     19925 |    7716    27320 |    3112    2748    42535    15.5 | 24.317 % |
c |     20150 |    7716    27320 |    3423    2973    46904    15.8 | 24.317 % |
c ==============================================================================
c [1mFound solution: 808[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7551   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20335 |    7718    27330 |    2572    3158    50708    16.1 | 24.317 % |
c |     20436 |    7710    27308 |    2829    1679    14643     8.7 | 24.455 % |
c |     20589 |    7710    27308 |    3112    1832    17069     9.3 | 24.454 % |
c |     20814 |    7710    27308 |    3423    2057    20623    10.0 | 24.454 % |
c |     21154 |    7710    27308 |    3765    2397    27455    11.5 | 24.454 % |
c |     21662 |    7710    27308 |    4142    2905    39129    13.5 | 24.454 % |
c ==============================================================================
c [1mFound solution: 718[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7641   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22035 |    7716    27356 |    2572    3278    44757    13.7 | 24.454 % |
c |     22135 |    7716    27356 |    2829    1739    16001     9.2 | 24.592 % |
c |     22286 |    7716    27356 |    3112    1890    18646     9.9 | 24.592 % |
c |     22511 |    7716    27356 |    3423    2115    21466    10.1 | 24.592 % |
c |     22848 |    7716    27356 |    3765    2452    27028    11.0 | 24.592 % |
c ==============================================================================
c [1mFound solution: 712[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7647   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22939 |    7718    27366 |    2572    2543    27896    11.0 | 24.592 % |
c |     23042 |    7695    27287 |    2829    2637    29113    11.0 | 24.837 % |
c |     23192 |    7695    27287 |    3112    2787    31480    11.3 | 24.837 % |
c |     23418 |    7695    27287 |    3423    3013    35979    11.9 | 24.837 % |
c |     23758 |    7695    27287 |    3765    3353    41475    12.4 | 24.837 % |
c |     24264 |    7695    27287 |    4142    3859    50525    13.1 | 24.837 % |
c ==============================================================================
c [1mFound solution: 711[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7648   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24428 |    7696    27302 |    2565    4023    53802    13.4 | 24.837 % |
c |     24529 |    7696    27302 |    2821    2113    20149     9.5 | 24.878 % |
c |     24679 |    7696    27302 |    3103    2263    21927     9.7 | 24.878 % |
c |     24904 |    7696    27302 |    3414    2488    25581    10.3 | 24.878 % |
c |     25242 |    7696    27302 |    3755    2826    32210    11.4 | 24.878 % |
c |     25748 |    7690    27282 |    4130    3328    40382    12.1 | 24.932 % |
c |     26507 |    7690    27282 |    4544    4087    55675    13.6 | 24.932 % |
c ==============================================================================
c [1mFound solution: 707[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7652   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26941 |    7693    27312 |    2564    4521    64900    14.4 | 24.932 % |
c |     27041 |    7693    27312 |    2820    2361    28238    12.0 | 25.000 % |
c |     27192 |    7693    27312 |    3102    2512    31030    12.4 | 25.000 % |
c |     27417 |    7693    27312 |    3412    2737    34096    12.5 | 25.000 % |
c |     27756 |    7693    27312 |    3753    3076    41149    13.4 | 25.000 % |
c |     28262 |    7693    27312 |    4129    3582    52056    14.5 | 25.000 % |
c |     29023 |    7693    27312 |    4542    4343    65191    15.0 | 25.000 % |
c ==============================================================================
c [1mFound solution: 416[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7943   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29997 |    7697    27339 |    2565    5317    89130    16.8 | 25.000 % |
c |     30098 |    7671    27249 |    2821    2680    36675    13.7 | 25.327 % |
c |     30249 |    7621    27073 |    3103    2811    38596    13.7 | 25.812 % |
c ==============================================================================
c [1mFound solution: 414[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7945   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30449 |    7600    27009 |    2533    2986    41420    13.9 | 25.812 % |
c |     30552 |    7600    27009 |    2786    3089    42495    13.8 | 25.838 % |
c ==============================================================================
c [1mFound solution: 413[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7946   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30667 |    7602    27024 |    2534    3204    44034    13.7 | 25.838 % |
c |     30770 |    7602    27024 |    2787    1705    13338     7.8 | 25.864 % |
c |     30920 |    7602    27024 |    3066    1855    15603     8.4 | 25.864 % |
c |     31147 |    7593    26993 |    3372    2075    18992     9.2 | 25.918 % |
c |     31484 |    7593    26993 |    3710    2412    27067    11.2 | 25.918 % |
c ==============================================================================
c [1mFound solution: 412[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7947   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31971 |    7595    27007 |    2531    2899    35759    12.3 | 25.918 % |
c |     32071 |    7595    27007 |    2784    2999    37559    12.5 | 25.944 % |
c |     32221 |    7595    27007 |    3062    3149    40421    12.8 | 25.944 % |
c |     32447 |    7586    26976 |    3368    3368    45355    13.5 | 25.998 % |
c |     32784 |    7586    26976 |    3705    3705    51486    13.9 | 25.998 % |
c ==============================================================================
c [1mFound solution: 408[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7951   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32995 |    7587    26987 |    2529    3916    56562    14.4 | 25.998 % |
c |     33096 |    7587    26987 |    2781    2059    22708    11.0 | 26.038 % |
c |     33246 |    7587    26987 |    3060    2209    25097    11.4 | 26.038 % |
c |     33471 |    7557    26892 |    3366    2426    30350    12.5 | 26.415 % |
c |     33808 |    7557    26892 |    3702    2763    36132    13.1 | 26.415 % |
c |     34314 |    7557    26892 |    4072    3269    46785    14.3 | 26.415 % |
c |     35073 |    7557    26892 |    4480    4028    64040    15.9 | 26.415 % |
c |     36212 |    7551    26872 |    4928    5164   106720    20.7 | 26.469 % |
c |     37922 |    7541    26839 |    5421    4090    86760    21.2 | 26.631 % |
c ==============================================================================
c [1mFound solution: 316[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 8043   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38341 |    7549    26890 |    2516    4509    93115    20.7 | 26.631 % |
c |     38441 |    7549    26890 |    2767    2355    25824    11.0 | 26.731 % |
c |     38592 |    7549    26890 |    3044    2506    27152    10.8 | 26.731 % |
c ==============================================================================
c [1mFound solution: 315[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 8044   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38788 |    7551    26905 |    2517    2702    29255    10.8 | 26.731 % |
c |     38888 |    7551    26905 |    2768    2802    30236    10.8 | 26.756 % |
c |     39038 |    7551    26905 |    3045    2952    32111    10.9 | 26.756 % |
c |     39263 |    7543    26883 |    3350    3176    34478    10.9 | 26.863 % |
c ==============================================================================
c [1mFound solution: 312[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 8047   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39549 |    7509    26772 |    2503    3348    36795    11.0 | 26.863 % |
c |     39652 |    7509    26772 |    2753    1777    13006     7.3 | 27.102 % |
c ==============================================================================
c [1mFound solution: 311[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 8048   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39719 |    7511    26789 |    2503    1844    14037     7.6 | 27.102 % |
c |     39819 |    7511    26789 |    2753    1944    14947     7.7 | 27.127 % |
c |     39971 |    7511    26789 |    3028    2096    17583     8.4 | 27.128 % |
c ==============================================================================
c [1mFound solution: 310[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 288   maxlim: 7748   bits: 13/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40041 |    9288    33067 |    3096    2095    17501     8.4 | 27.128 % |
c |     40141 |    9288    33067 |    3405    2195    18761     8.5 | 24.503 % |
c |     40292 |    9253    32942 |    3746    2332    21025     9.0 | 24.642 % |
c |     40517 |    9253    32942 |    4120    2557    25176     9.8 | 24.642 % |
c |     40854 |    8652    30549 |    4532    2474    29212    11.8 | 27.924 % |
c ==============================================================================
c [1mFound solution: 308[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 308   maxlim: 7650   bits: 13/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40897 |   10092    35648 |    3364    2384    28372    11.9 | 27.924 % |
c |     40997 |   10092    35648 |    3700    2484    30705    12.4 | 28.197 % |
c |     41148 |   10092    35648 |    4070    2635    34508    13.1 | 28.197 % |
c |     41373 |   10053    35507 |    4477    2820    39366    14.0 | 28.358 % |
c |     41710 |   10053    35507 |    4925    3157    46383    14.7 | 28.358 % |
c ==============================================================================
c [1mFound solution: 307[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7651   bits: 13/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41760 |   10030    35432 |    3343    3202    46875    14.6 | 28.358 % |
c |     41860 |    9932    35096 |    3677    3256    47749    14.7 | 29.032 % |
c |     42011 |    9932    35096 |    4045    3407    51487    15.1 | 29.032 % |
c |     42236 |    9932    35096 |    4449    3632    59569    16.4 | 29.032 % |
c |     42574 |    9932    35096 |    4894    3970    73748    18.6 | 29.032 % |
c ==============================================================================
c [1mFound solution: 306[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7652   bits: 13/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42720 |    9937    35123 |    3312    4116    75663    18.4 | 29.032 % |
c |     42820 |    9927    35085 |    3643    2142    34805    16.2 | 29.101 % |
c |     42971 |    9676    34220 |    4007    2267    35837    15.8 | 30.230 % |
c |     43197 |    8944    31624 |    4408    2412    43701    18.1 | 33.333 % |
c |     43535 |    8448    29844 |    4849    2685    46524    17.3 | 35.026 % |
c |     44043 |    7872    27820 |    5334    3082    54103    17.6 | 37.807 % |
c ==============================================================================
c [1mFound solution: 305[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 302   maxlim: 4846   bits: 13/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     44706 |    9704    34303 |    3234    3703    61775    16.7 | 37.807 % |
c |     44806 |    9662    34151 |    3557    3802    63420    16.7 | 35.006 % |
c |     44956 |    9603    33948 |    3913    3946    66936    17.0 | 35.328 % |
c |     45181 |    8895    31471 |    4304    4051    69047    17.0 | 38.696 % |
c |     45518 |    8656    30648 |    4734    4372    72597    16.6 | 39.771 % |
c |     46025 |    8206    29044 |    5208    4705    76519    16.3 | 42.960 % |
c |     46785 |    8125    28767 |    5729    5459    84898    15.6 | 43.389 % |
c |     47924 |    7611    26963 |    6302    6515    99824    15.3 | 45.432 % |
c |     49632 |    7585    26873 |    6932    4406    57464    13.0 | 45.539 % |
c |     52194 |    7569    26813 |    7625    6864   110377    16.1 | 45.575 % |
c |     56038 |    7554    26760 |    8388    6163    84205    13.7 | 45.611 % |
c ==============================================================================
c [1mFound solution: 304[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 210   maxlim: 2243   bits: 12/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     59144 |    8892    31505 |    2964    9255   124424    13.4 | 45.611 % |
c |     59244 |    8883    31476 |    3260    2413    20244     8.4 | 42.872 % |
c |     59394 |    8883    31476 |    3586    2563    21667     8.5 | 42.871 % |
c |     59619 |    8883    31476 |    3945    2788    24275     8.7 | 42.871 % |
c |     59958 |    8883    31476 |    4339    3127    28438     9.1 | 42.871 % |
c |     60464 |    8883    31476 |    4773    3633    35052     9.6 | 42.871 % |
c |     61225 |    8883    31476 |    5250    4394    43808    10.0 | 42.871 % |
c |     62364 |    8550    30289 |    5775    5514    57390    10.4 | 44.104 % |
c |     64072 |    8550    30289 |    6353    3625    41655    11.5 | 44.104 % |
c |     66634 |    8524    30201 |    6988    6108    88211    14.4 | 44.270 % |
c |     70478 |    8492    30088 |    7687    5740    68351    11.9 | 44.504 % |
c |     76245 |    8400    29762 |    8456    6923    67517     9.8 | 44.870 % |
c ==============================================================================
c [1mOptimal solution: 304[0m
s OPTIMUM FOUND
v v133 v177 -v217 v3 v179 v7 v8 -v96 -v184 v224 -v185 v225 -v10 -v98 v142 -v186 v226 v99 v12 v13 v14 -v58 v103 -v60 -v104 v148 v229 v61 v19 -v107 -v108 v152 -v21 -v109 v153 -v110 v154 v111 -v191 v231 -v26 v70 v236 v117 -v197 v237 -v198 v238 v118 v199 -v239 v163 v120 -v201 v241 v202 -v242 -v121 -v203 v243 -v123 v167 v205 -v245 v124 v246 v37 -v125 -v169 v207 -v247 v126 v248 v39 -v171 v249 -v212 v252 v129 v213 -v253 v130 v214 -v254 v131 v215 -v255 v132 v256 -v1 -v45 -v89 -v90 -v178 -v47 -v219 -v221 -v223 -v52 -v140 -v11 -v55 -v143 -v227 -v56 -v144 -v228 -v57 -v145 -v102 -v146 -v15 -v147 -v17 -v149 -v18 v62 -v106 -v150 -v151 -v65 -v23 -v67 -v155 -v24 -v68 -v112 v156 v190 -v230 -v158 -v232 -v233 -v234 -v235 -v29 -v73 -v161 -v30 -v74 -v162 -v75 -v119 -v240 -v32 -v76 -v164 -v33 -v165 -v34 -v78 -v244 -v79 -v80 -v168 -v81 -v38 -v82 -v170 -v83 -v127 -v41 -v85 -v173 -v42 -v86 -v174 -v43 -v87 -v175 -v176 -v216 one -v2 -v4 v5 -v6 -v9 -v16 -v20 -v22 -v25 -v27 -v28 -v31 -v35 -v36 -v40 -v44 -v46 -v48 -v49 v50 -v51 v53 -v54 -v59 -v63 -v64 -v66 v69 v71 v72 v77 v84 -v88 -v91 -v92 -v93 -v94 -v95 -v97 -v100 -v101 -v105 -v113 -v114 -v115 -v116 -v122 -v128 v134 -v135 v136 -v137 -v138 -v139 -v141 -v157 -v159 -v160 v166 -v172 -v180 v181 -v182 v183 v187 v188 -v189 v192 v193 v194 v195 -v196 v200 v204 -v206 -v208 -v209 v210 v211 v218 v220 v222 -v250 -v251
c _______________________________________________________________________________
c 
c restarts              : 175
c conflicts             : 83559          (3684 /sec)
c decisions             : 189652         (8362 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 22.6816 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.93 0.97 0.91 2/54 31622
Raw data (stat): 31622 (runsolver) R 31621 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479822571 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31622
Raw data (stat): 31622 (minisat+) R 31621 27565 27564 0 -1 0 748 0 0 0 996 2 0 0 25 0 1 0 479822571 4632576 726 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1131 726 603 41 0 1090 0
vsize: 4524
[startup+20.0005 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31622
Raw data (stat): 31622 (minisat+) R 31621 27565 27564 0 -1 0 970 0 0 0 1994 3 0 0 25 0 1 0 479822571 5578752 948 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1362 948 603 41 0 1321 0
vsize: 5448
[startup+22.748 s]
Raw data (loadavg): 1.01 0.99 0.91 1/53 31622
Raw data (stat): 31622 (minisat+) R 31621 27565 27564 0 -1 0 970 0 0 0 1994 3 0 0 25 0 1 0 479822571 5578752 948 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1362 948 603 41 0 1321 0
vsize: 0

Child status: 30
Real time (s): 22.7478
CPU time (s): 22.7275
CPU user time (s): 22.6866
CPU system time (s): 0.040993
CPU usage (%): 99.9111
Max. virtual memory (Kb): 5448
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	304
#### END VERIFIER DATA ####