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/primes-dimacs-cnf/normalized-ii32c1.opb
MD5SUM	8afff0cc8710524125079d5ef00fedc0
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	167
Optimality of the best value was proved	NO
Number of terms in the objective function	450
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	450
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	450
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03084
Number of variables	450
Total number of constraints	1505
Number of constraints which are clauses	1505
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	32
Trace number 6172

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc32 THE 2005-04-14 03:57:03 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4663 boxname=wulflinc32 idbench=151 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  8afff0cc8710524125079d5ef00fedc0  /oldhome/oroussel/tmp/wulflinc32/normalized-ii32c1.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc32/normalized-ii32c1.opb /oldhome/oroussel/tmp/wulflinc32/normalized-ii32c1.opb
IDLAUNCH: 4663
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.085
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.085
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:      1034724 kB
MemFree:        701892 kB
Buffers:         35316 kB
Cached:         186036 kB
SwapCached:       1212 kB
Active:         147448 kB
Inactive:       154244 kB
HighTotal:      131072 kB
HighFree:          256 kB
LowTotal:       903652 kB
LowFree:        701636 kB
SwapTotal:     2097892 kB
SwapFree:      2096680 kB
Dirty:            2340 kB
Writeback:           0 kB
Mapped:          81768 kB
Slab:            25376 kB
Committed_AS:   174000 kB
PageTables:        432 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 03:58:50 (client local time) WITH STATUS 30 IN 107.091 SECONDS
stats: 4663 0 107.091 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1505 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    1505     6531 |     501       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 216[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:16912     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         1 |   41754   100727 |   13918       1       30    30.0 |  0.000 % |
c |       101 |   41121    99297 |   15309      79      465     5.9 |  1.338 % |
c |       251 |   35740    86937 |   16840      51      314     6.2 | 13.404 % |
c |       476 |   33374    81490 |   18524     210    11516    54.8 | 18.807 % |
c ==============================================================================
c [1mFound solution: 214[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       514 |   33421    81623 |   11140     248    14258    57.5 | 18.807 % |
c ==============================================================================
c [1mFound solution: 213[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       584 |   33355    81496 |   11118     315    19424    61.7 | 18.807 % |
c ==============================================================================
c [1mFound solution: 212[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       647 |   33092    80892 |   11030     374    22518    60.2 | 18.807 % |
c ==============================================================================
c [1mFound solution: 211[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       727 |   33051    80830 |   11017     452    26613    58.9 | 18.807 % |
c ==============================================================================
c [1mFound solution: 210[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       771 |   33008    80724 |   11002     496    29200    58.9 | 18.807 % |
c ==============================================================================
c [1mFound solution: 209[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       787 |   33076    80901 |   11025     512    30094    58.8 | 18.807 % |
c ==============================================================================
c [1mFound solution: 202[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       803 |   33152    81115 |   11050     526    30403    57.8 | 18.807 % |
c |       903 |   32697    80081 |   12155     619    33973    54.9 | 21.021 % |
c |      1053 |   31960    78390 |   13370     755    36539    48.4 | 22.835 % |
c |      1279 |   30997    76163 |   14707     935    49986    53.5 | 24.887 % |
c ==============================================================================
c [1mFound solution: 201[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1387 |   30980    76142 |   10326    1042    58694    56.3 | 24.887 % |
c |      1487 |   30510    75064 |   11358    1136    62034    54.6 | 26.062 % |
c |      1639 |   30295    74568 |   12494    1253    66875    53.4 | 26.558 % |
c ==============================================================================
c [1mFound solution: 200[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1750 |   30236    74416 |   10078    1361    74725    54.9 | 26.558 % |
c |      1851 |   29499    72732 |   11085    1428    75810    53.1 | 28.222 % |
c ==============================================================================
c [1mFound solution: 199[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1900 |   29065    71750 |    9688    1470    76994    52.4 | 28.222 % |
c |      2003 |   28608    70701 |   10656    1564    79905    51.1 | 30.321 % |
c |      2153 |   28521    70502 |   11722    1713    94401    55.1 | 30.508 % |
c ==============================================================================
c [1mFound solution: 198[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2176 |   28469    70364 |    9489    1720    94231    54.8 | 30.508 % |
c |      2276 |   28469    70364 |   10437    1820   103405    56.8 | 30.611 % |
c ==============================================================================
c [1mFound solution: 197[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2283 |   28524    70505 |    9508    1827   103953    56.9 | 30.611 % |
c |      2383 |   28333    70068 |   10458    1922   110220    57.3 | 30.996 % |
c |      2534 |   28249    69875 |   11504    2072   116328    56.1 | 31.168 % |
c |      2759 |   27877    69021 |   12655    2288   126229    55.2 | 31.986 % |
c ==============================================================================
c [1mFound solution: 182[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2890 |   27752    68766 |    9250    2401   135109    56.3 | 31.986 % |
c ==============================================================================
c [1mFound solution: 181[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2943 |   27633    68507 |    9211    2451   136751    55.8 | 31.986 % |
c ==============================================================================
c [1mFound solution: 180[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2947 |   27575    68350 |    9191    2447   136407    55.7 | 31.986 % |
c |      3047 |   27314    67754 |   10110    2543   141810    55.8 | 33.632 % |
c |      3197 |   27050    67148 |   11121    2689   150243    55.9 | 34.209 % |
c |      3422 |   27050    67148 |   12233    2914   163670    56.2 | 34.209 % |
c |      3759 |   26684    66308 |   13456    3247   182657    56.3 | 35.007 % |
c ==============================================================================
c [1mFound solution: 179[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3973 |   26661    66271 |    8887    3451   193162    56.0 | 35.007 % |
c |      4073 |   25707    64064 |    9775    3528   194696    55.2 | 37.344 % |
c |      4224 |   22654    56995 |   10753    3603   195718    54.3 | 44.170 % |
c |      4449 |   22355    56302 |   11828    3821   207132    54.2 | 44.866 % |
c |      4787 |   22355    56302 |   13011    4159   228643    55.0 | 44.866 % |
c ==============================================================================
c [1mFound solution: 178[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5094 |   22305    56168 |    7435    4409   242057    54.9 | 44.866 % |
c |      5194 |   22305    56168 |    8178    4509   248662    55.1 | 44.967 % |
c |      5344 |   22305    56168 |    8996    4659   252002    54.1 | 44.967 % |
c |      5571 |   21312    53859 |    9895    4857   259001    53.3 | 47.235 % |
c |      5910 |   21208    53619 |   10885    5195   277027    53.3 | 47.462 % |
c |      6416 |   21095    53358 |   11974    5700   305084    53.5 | 47.704 % |
c |      7177 |   21095    53358 |   13171    6461   347019    53.7 | 47.704 % |
c |      8316 |   20891    52884 |   14488    7598   387444    51.0 | 48.159 % |
c |     10026 |   20674    52382 |   15937    9302   463775    49.9 | 48.877 % |
c |     12588 |   20180    51234 |   17531   11854   565194    47.7 | 49.773 % |
c |     16436 |   19301    49205 |   19284   15684   716545    45.7 | 51.735 % |
c |     22202 |   17896    45944 |   21212   21422   966048    45.1 | 54.962 % |
c ==============================================================================
c [1mFound solution: 177[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24782 |   17528    45082 |    5842   23998  1069868    44.6 | 54.962 % |
c |     24882 |   17528    45082 |    6426   12099   431322    35.6 | 55.905 % |
c |     25032 |   17528    45082 |    7068   12249   435033    35.5 | 55.905 % |
c |     25258 |   17528    45082 |    7775   12475   440485    35.3 | 55.905 % |
c |     25595 |   17528    45082 |    8553   12812   450817    35.2 | 55.905 % |
c ==============================================================================
c [1mFound solution: 174[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25856 |   17528    45073 |    5842   13062   458410    35.1 | 55.905 % |
c ==============================================================================
c [1mFound solution: 173[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25915 |   17574    45190 |    5858   13121   461116    35.1 | 55.905 % |
c |     26015 |   17478    44966 |    6443   13219   464564    35.1 | 56.136 % |
c |     26165 |   17478    44966 |    7088   13369   472188    35.3 | 56.136 % |
c |     26391 |   17052    43962 |    7796   13589   481357    35.4 | 57.142 % |
c ==============================================================================
c [1mFound solution: 172[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26479 |   16990    43797 |    5663   13527   472242    34.9 | 57.142 % |
c |     26579 |   16990    43797 |    6229   13627   475681    34.9 | 57.254 % |
c ==============================================================================
c [1mFound solution: 171[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26671 |   17042    43928 |    5680   13719   477668    34.8 | 57.254 % |
c |     26772 |   17042    43928 |    6248   13820   479557    34.7 | 57.203 % |
c |     26923 |   17042    43928 |    6872   13971   482686    34.5 | 57.203 % |
c |     27148 |   17042    43928 |    7560   14196   490682    34.6 | 57.203 % |
c |     27487 |   16841    43451 |    8316   14532   504113    34.7 | 57.698 % |
c |     27994 |   16643    42986 |    9147   15037   521691    34.7 | 58.179 % |
c |     28753 |   16340    42284 |   10062   15787   538121    34.1 | 58.880 % |
c |     29892 |   16010    41526 |   11068   16920   563637    33.3 | 59.601 % |
c |     31601 |   14999    39172 |   12175   18603   608894    32.7 | 62.028 % |
c |     34164 |   13687    36102 |   13393   21115   678427    32.1 | 65.155 % |
c ==============================================================================
c [1mFound solution: 170[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35279 |   13531    35721 |    4510   22095   701461    31.7 | 65.155 % |
c ==============================================================================
c [1mFound solution: 169[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35344 |   13576    35835 |    4525   11113   247875    22.3 | 65.155 % |
c |     35444 |   13576    35835 |    4977   11213   252806    22.5 | 65.444 % |
c |     35594 |   13576    35835 |    5475   11363   257314    22.6 | 65.444 % |
c ==============================================================================
c [1mFound solution: 168[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35669 |   13519    35679 |    4506   11418   258215    22.6 | 65.444 % |
c |     35776 |   13519    35679 |    4956   11525   261308    22.7 | 65.548 % |
c |     35927 |   13519    35679 |    5452   11676   268816    23.0 | 65.548 % |
c ==============================================================================
c [1mFound solution: 167[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36090 |   13570    35807 |    4523   11839   272066    23.0 | 65.548 % |
c |     36191 |   13570    35807 |    4975   11940   274570    23.0 | 65.486 % |
c |     36341 |   13570    35807 |    5472   12090   276546    22.9 | 65.486 % |
c |     36567 |   13570    35807 |    6020   12316   282110    22.9 | 65.486 % |
c |     36904 |   13479    35605 |    6622   10423   244251    23.4 | 65.627 % |
c |     37411 |   13479    35605 |    7284   10930   265870    24.3 | 65.627 % |
c |     38170 |   13479    35605 |    8012   11689   299668    25.6 | 65.627 % |
c ==============================================================================
c [1mOptimal solution: 167[0m
s OPTIMUM FOUND
v x1 -x2 x3 -x4 -x5 x6 x7 -x8 x9 -x10 x11 -x12 x13 -x14 x15 -x16 x17 -x18 x19 -x20 x21 -x22 x23 -x24 x25 -x26 x27 -x28 x29 -x30 x31 -x32 x33 -x34 x35 -x36 x37 -x38 x39 -x40 x41 -x42 x43 -x44 x45 -x46 x47 -x48 x49 -x50 x51 -x52 x53 -x54 x55 -x56 x57 -x58 x59 -x60 x61 -x62 x63 -x64 x65 -x66 x67 -x68 x69 -x70 x71 -x72 x73 -x74 x75 -x76 x77 -x78 -x79 x80 x81 -x82 x83 -x84 x85 -x86 x87 -x88 x89 -x90 x91 -x92 x93 -x94 x95 -x96 x97 -x98 x99 -x100 x101 -x102 x103 -x104 x105 -x106 x107 -x108 x109 -x110 x111 -x112 x113 -x114 x115 -x116 x117 -x118 x119 -x120 x121 -x122 x123 -x124 -x125 x126 x127 -x128 -x129 -x130 x131 -x132 -x133 -x134 x135 -x136 -x137 -x138 x139 -x140 x141 -x142 -x143 -x144 -x145 -x146 x147 -x148 -x149 -x150 x151 -x152 -x153 -x154 x155 -x156 x157 -x158 -x159 -x160 -x161 -x162 x163 -x164 -x165 x166 x167 -x168 x169 -x170 -x171 -x172 -x173 -x174 x175 -x176 x177 -x178 -x179 -x180 -x181 -x182 x183 -x184 -x185 -x186 x187 -x188 x189 -x190 -x191 -x192 x193 -x194 -x195 -x196 -x197 -x198 x199 -x200 -x201 -x202 x203 -x204 -x205 -x206 x207 -x208 -x209 -x210 x211 -x212 -x213 -x214 x215 -x216 x217 -x218 -x219 x220 x221 -x222 -x223 x224 -x225 -x226 x227 -x228 -x229 -x230 x231 -x232 -x233 -x234 x235 -x236 -x237 -x238 x239 -x240 x241 -x242 -x243 -x244 x245 -x246 -x247 -x248 -x249 -x250 x251 -x252 x253 -x254 -x255 -x256 x257 -x258 -x259 x260 -x261 -x262 x263 -x264 -x265 -x266 x267 -x268 x269 -x270 -x271 -x272 -x273 -x274 x275 -x276 x277 -x278 -x279 -x280 x281 -x282 -x283 -x284 x285 -x286 -x287 x288 x289 -x290 -x291 -x292 x293 -x294 -x295 -x296 x297 -x298 -x299 -x300 x301 -x302 -x303 -x304 -x305 -x306 x307 -x308 -x309 -x310 x311 -x312 -x313 -x314 x315 -x316 x317 -x318 -x319 -x320 x321 -x322 -x323 -x324 -x325 -x326 x327 -x328 -x329 -x330 x331 -x332 -x333 x334 x335 -x336 x337 -x338 -x339 -x340 x341 -x342 -x343 -x344 -x345 -x346 x347 -x348 x349 -x350 -x351 -x352 x353 -x354 -x355 -x356 -x357 -x358 x359 -x360 -x361 -x362 x363 -x364 x365 -x366 -x367 -x368 x369 -x370 -x371 -x372 x373 -x374 -x375 -x376 -x377 -x378 x379 -x380 x381 -x382 -x383 -x384 x385 -x386 -x387 x388 -x389 x390 x391 -x392 -x393 x394 -x395 x396 x397 -x398 -x399 x400 -x401 x402 x403 -x404 -x405 x406 -x407 x408 x409 -x410 -x411 x412 -x413 x414 x415 -x416 -x417 x418 -x419 x420 -x421 x422 -x423 x424 x425 -x426 -x427 x428 x429 -x430 -x431 x432 x433 -x434 -x435 x436 -x437 x438 x439 -x440 -x441 x442 -x443 x444 x445 -x446 -x447 x448 -x449 x450
c _______________________________________________________________________________
c 
c restarts              : 89
c conflicts             : 39097          (365 /sec)
c decisions             : 82909          (775 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 106.995 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.91 0.94 0.90 2/53 14959
Raw data (stat): 14959 (runsolver) R 14958 7987 7986 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481519534 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.0011 s]
Raw data (loadavg): 1.00 0.96 0.91 2/53 14959
Raw data (stat): 14959 (minisat+) R 14958 7987 7986 0 -1 0 1690 0 0 0 993 4 0 0 25 0 1 0 481519534 8773632 1652 4294967295 134512640 134672761 3221224576 3221223760 134556589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2142 1652 603 41 0 2101 0
vsize: 8568
[startup+20.0017 s]
Raw data (loadavg): 1.00 0.96 0.91 2/53 14959
Raw data (stat): 14959 (minisat+) R 14958 7987 7986 0 -1 0 1911 0 0 0 1993 4 0 0 25 0 1 0 481519534 9670656 1873 4294967295 134512640 134672761 3221224576 3221223712 134560637 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2361 1873 603 41 0 2320 0
vsize: 9444
[startup+30.0036 s]
Raw data (loadavg): 1.00 0.96 0.91 2/53 14959
Raw data (stat): 14959 (minisat+) R 14958 7987 7986 0 -1 0 2108 0 0 0 2992 6 0 0 25 0 1 0 481519534 10522624 2070 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2569 2070 603 41 0 2528 0
vsize: 10276
[startup+40.0044 s]
Raw data (loadavg): 1.00 0.96 0.91 2/53 14959
Raw data (stat): 14959 (minisat+) R 14958 7987 7986 0 -1 0 2289 0 0 0 3992 6 0 0 25 0 1 0 481519534 11321344 2251 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2764 2251 603 41 0 2723 0
vsize: 11056
[startup+50.005 s]
Raw data (loadavg): 1.00 0.96 0.91 2/53 14959
Raw data (stat): 14959 (minisat+) R 14958 7987 7986 0 -1 0 2497 0 0 0 4992 7 0 0 25 0 1 0 481519534 12218368 2459 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2983 2459 603 41 0 2942 0
vsize: 11932
[startup+60.0061 s]
Raw data (loadavg): 1.00 0.96 0.91 2/53 14959
Raw data (stat): 14959 (minisat+) R 14958 7987 7986 0 -1 0 2686 0 0 0 5991 7 0 0 25 0 1 0 481519534 13008896 2648 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3176 2648 603 41 0 3135 0
vsize: 12704
[startup+70.0063 s]
Raw data (loadavg): 1.00 0.96 0.91 2/53 14959
Raw data (stat): 14959 (minisat+) R 14958 7987 7986 0 -1 0 2806 0 0 0 6991 7 0 0 25 0 1 0 481519534 13418496 2768 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3276 2768 603 41 0 3235 0
vsize: 13104
[startup+80.0074 s]
Raw data (loadavg): 1.00 0.96 0.91 2/53 14959
Raw data (stat): 14959 (minisat+) R 14958 7987 7986 0 -1 0 2806 0 0 0 7991 7 0 0 25 0 1 0 481519534 13418496 2768 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3276 2768 603 41 0 3235 0
vsize: 13104
[startup+90.0082 s]
Raw data (loadavg): 1.00 0.96 0.91 2/53 14959
Raw data (stat): 14959 (minisat+) R 14958 7987 7986 0 -1 0 2807 0 0 0 8991 8 0 0 25 0 1 0 481519534 13418496 2769 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3276 2769 603 41 0 3235 0
vsize: 13104
[startup+100.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/53 14959
Raw data (stat): 14959 (minisat+) R 14958 7987 7986 0 -1 0 2810 0 0 0 9991 8 0 0 25 0 1 0 481519534 13418496 2772 4294967295 134512640 134672761 3221224576 3221223680 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3276 2772 603 41 0 3235 0
vsize: 13104
[startup+107.103 s]
Raw data (loadavg): 1.00 0.97 0.91 1/52 14959
Raw data (stat): 14959 (minisat+) R 14958 7987 7986 0 -1 0 2810 0 0 0 9991 8 0 0 25 0 1 0 481519534 13418496 2772 4294967295 134512640 134672761 3221224576 3221223680 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3276 2772 603 41 0 3235 0
vsize: 0

Child status: 30
Real time (s): 107.102
CPU time (s): 107.091
CPU user time (s): 107
CPU system time (s): 0.090986
CPU usage (%): 99.9895
Max. virtual memory (Kb): 13104
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	167
#### END VERIFIER DATA ####