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-8pb.opb
MD5SUM	2bf0a3299a380a62e2f4aaf6d6f8fe18
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	36
Optimality of the best value was proved	NO
Number of terms in the objective function	432
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	432
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	3
Number of bits of the biggest number in a constraint	2
Biggest sum of numbers in a constraint	432
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	0.903861
Number of variables	432
Total number of constraints	1304
Number of constraints which are clauses	1280
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	18
Trace number 5514

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-04-14 00:36:41 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4004 boxname=wulflinc2 idbench=244 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  2bf0a3299a380a62e2f4aaf6d6f8fe18  /oldhome/oroussel/tmp/wulflinc2/normalized-s4-4-3-8pb.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc2/normalized-s4-4-3-8pb.opb /oldhome/oroussel/tmp/wulflinc2/normalized-s4-4-3-8pb.opb
IDLAUNCH: 4004
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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.191
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:        902564 kB
Buffers:         34692 kB
Cached:          76960 kB
SwapCached:          4 kB
Active:          56504 kB
Inactive:        57996 kB
HighTotal:      131008 kB
HighFree:        50288 kB
LowTotal:       903652 kB
LowFree:        852276 kB
SwapTotal:     2097136 kB
SwapFree:      2097132 kB
Dirty:              64 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11948 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:37:28 (client local time) WITH STATUS 30 IN 46.7239 SECONDS
stats: 4004 0 46.7239 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1304 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################################################
c   -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[1290]---> BDD-cost:    1
c ---[1264]---> BDD-cost:    1
c ---[1242]---> BDD-cost:    1
c ---[1232]---> BDD-cost:    1
c ---[1199]---> BDD-cost:    1
c ---[1173]---> BDD-cost:    1
c ---[1171]---> BDD-cost:    1
c ---[1161]---> BDD-cost:    1
c ---[1147]---> BDD-cost:    1
c ---[1121]---> BDD-cost:    1
c ---[1099]---> BDD-cost:    1
c ---[1089]---> BDD-cost:    1
c ---[1052]---> BDD-cost:    1
c ---[1030]---> BDD-cost:    1
c ---[1024]---> BDD-cost:    1
c ---[1018]---> BDD-cost:    1
c ---[1008]---> BDD-cost:    1
c ---[ 998]---> BDD-cost:    1
c ---[ 948]---> BDD-cost:    1
c ---[ 946]---> BDD-cost:    1
c ---[ 932]---> BDD-cost:    1
c ---[ 906]---> BDD-cost:    1
c ---[ 884]---> BDD-cost:    1
c ---[ 874]---> BDD-cost:    1
c ---[ 826]---> BDD-cost:    1
c ---[ 816]---> BDD-cost:    1
c ---[ 806]---> BDD-cost:    1
c ---[ 804]---> BDD-cost:    1
c ---[ 802]---> BDD-cost:    1
c ---[ 776]---> BDD-cost:    1
c ---[ 758]---> BDD-cost:    1
c ---[ 733]---> BDD-cost:    1
c ---[ 723]---> BDD-cost:    1
c ---[ 713]---> BDD-cost:    1
c ---[ 663]---> BDD-cost:    1
c ---[ 661]---> BDD-cost:    1
c ---[ 643]---> BDD-cost:    1
c ---[ 622]---> BDD-cost:    1
c ---[ 596]---> BDD-cost:    1
c ---[ 590]---> BDD-cost:    1
c ---[ 554]---> BDD-cost:    1
c ---[ 532]---> BDD-cost:    1
c ---[ 526]---> BDD-cost:    1
c ---[ 520]---> BDD-cost:    1
c ---[ 518]---> BDD-cost:    1
c ---[ 492]---> BDD-cost:    1
c ---[ 474]---> BDD-cost:    1
c ---[ 448]---> BDD-cost:    1
c ---[ 430]---> BDD-cost:    1
c ---[ 408]---> BDD-cost:    1
c ---[ 382]---> BDD-cost:    1
c ---[ 376]---> BDD-cost:    1
c ---[ 366]---> BDD-cost:    1
c ---[ 356]---> BDD-cost:    1
c ---[ 307]---> BDD-cost:    1
c ---[ 305]---> BDD-cost:    1
c ---[ 253]---> BDD-cost:    1
c ---[ 243]---> BDD-cost:    1
c ---[ 237]---> BDD-cost:    1
c ---[ 235]---> BDD-cost:    1
c ---[ 182]---> BDD-cost:    1
c ---[ 172]---> BDD-cost:    1
c ---[ 166]---> BDD-cost:    1
c ---[ 164]---> BDD-cost:    1
c ---[ 112]---> BDD-cost:    1
c ---[ 102]---> BDD-cost:    1
c ---[  96]---> BDD-cost:    1
c ---[  94]---> BDD-cost:    1
c ---[  62]---> BDD-cost:    1
c ---[  36]---> BDD-cost:    1
c ---[  34]---> BDD-cost:    1
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:   59
c ---[  22]---> BDD-cost:   59
c ---[  21]---> BDD-cost:   59
c ---[  20]---> BDD-cost:   59
c ---[  19]---> BDD-cost:   59
c ---[  18]---> BDD-cost:   59
c ---[  17]---> BDD-cost:   59
c ---[  16]---> BDD-cost:   59
c ---[  15]---> BDD-cost:   59
c ---[  14]---> BDD-cost:   59
c ---[  13]---> BDD-cost:   59
c ---[  12]---> BDD-cost:   59
c ---[  11]---> BDD-cost:   59
c ---[  10]---> BDD-cost:   59
c ---[   9]---> BDD-cost:   59
c ---[   8]---> BDD-cost:   59
c ---[   7]---> BDD-cost:   59
c ---[   6]---> BDD-cost:   59
c ---[   5]---> BDD-cost:   59
c ---[   4]---> BDD-cost:   59
c ---[   3]---> BDD-cost:   59
c ---[   2]---> BDD-cost:   59
c ---[   1]---> BDD-cost:   59
c ---[   0]---> BDD-cost:   59
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    5048    14568 |    1514       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1824          
c   -- var.elim.:  1824/1824          
c   -- var.elim.:  336/336          
c   -- subsuming                       
c   -- var.elim.:  216/216          
c   -- var.elim.:  264/264          
c   -- subsuming                       
c |         0 |    4904    14208 |      --       0       --      -- |     --   | -144/-144
c |         0 |    4904    14208 |    1961       0        0     nan |  0.000 % |
c |       102 |    4904    14208 |    2157     102     2135    20.9 |  5.405 % |
c |       252 |    4904    14208 |    2373     252     7269    28.8 |  5.405 % |
c |       478 |    4904    14208 |    2610     478    14106    29.5 |  5.405 % |
c |       815 |    4904    14208 |    2871     815    22708    27.9 |  5.405 % |
c |      1323 |    4904    14208 |    3159    1323    40152    30.3 |  5.405 % |
c ==============================================================================
c (current CPU-time: 0.397939 s)
c ==============================================================================
c [1mFound solution: 58[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:16194     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1406 |   23254    56961 |    6976    1406    41517    29.5 |  5.405 % |
c   -- subsuming                       
c   -- var.elim.:  1000/12400          
c   -- var.elim.:  2000/12400          
c   -- var.elim.:  3000/12400          
c   -- var.elim.:  4000/12400          
c   -- var.elim.:  5000/12400          
c   -- var.elim.:  6000/12400          
c   -- var.elim.:  7000/12400          
c   -- var.elim.:  8000/12400          
c   -- var.elim.:  9000/12400          
c   -- var.elim.:  10000/12400          
c   -- var.elim.:  11000/12400          
c   -- var.elim.:  12000/12400          
c   -- var.elim.:  12400/12400          
c   -- var.elim.:  1000/6110          
c   -- var.elim.:  2000/6110          
c   -- var.elim.:  3000/6110          
c   -- var.elim.:  4000/6110          
c   -- var.elim.:  5000/6110          
c   -- var.elim.:  6000/6110          
c   -- var.elim.:  6110/6110          
c   -- var.elim.:  1000/1961          
c   -- var.elim.:  1961/1961          
c   -- var.elim.:  1000/2797          
c   -- var.elim.:  2000/2797          
c   -- var.elim.:  2797/2797          
c   -- var.elim.:  869/869          
c   -- subsuming                       
c   -- var.elim.:  1000/5148          
c   -- var.elim.:  2000/5148          
c   -- var.elim.:  3000/5148          
c   -- var.elim.:  4000/5148          
c   -- var.elim.:  5000/5148          
c   -- var.elim.:  5148/5148          
c   -- var.elim.:  1000/2699          
c   -- var.elim.:  2000/2699          
c   -- var.elim.:  2699/2699          
c   -- var.elim.:  1000/2634          
c   -- var.elim.:  2000/2634          
c   -- var.elim.:  2634/2634          
c   -- var.elim.:  1000/2388          
c   -- var.elim.:  2000/2388          
c   -- var.elim.:  2388/2388          
c   -- var.elim.:  113/113          
c   -- subsuming                       
c   -- var.elim.:  1000/2704          
c   -- var.elim.:  2000/2704          
c   -- var.elim.:  2704/2704          
c   -- var.elim.:  978/978          
c   -- var.elim.:  355/355          
c   -- var.elim.:  201/201          
c   -- subsuming                       
c   -- var.elim.:  961/961          
c |      1406 |   16437    80035 |      --    1406       --      -- |     --   | -6807/23104
c |      1406 |   16437    80035 |    6574    1406    41517    29.5 |  5.405 % |
c |      1506 |   16437    80035 |    7232    1506    44718    29.7 |  1.511 % |
c |      1656 |   16437    80035 |    7955    1656    49391    29.8 |  1.511 % |
c |      1883 |   16437    80035 |    8751    1883    55521    29.5 |  1.511 % |
c |      2220 |   16437    80035 |    9626    2220    62331    28.1 |  1.511 % |
c |      2729 |   16437    80035 |   10588    2729    78377    28.7 |  1.511 % |
c |      3488 |   16437    80035 |   11647    3488   103845    29.8 |  1.511 % |
c |      4627 |   16437    80035 |   12812    4627   137246    29.7 |  1.511 % |
c |      6336 |   16437    80035 |   14093    6336   195556    30.9 |  1.511 % |
c |      8898 |   16437    80035 |   15503    8898   279546    31.4 |  1.511 % |
c |     12745 |   16437    80035 |   17053   12745   413146    32.4 |  1.511 % |
c |     18513 |   16437    80035 |   18758   12705   454875    35.8 |  1.511 % |
c ==============================================================================
c (current CPU-time: 27.7928 s)
c ==============================================================================
c [1mFound solution: 52[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     22233 |   16754    80868 |    5026   16425   587815    35.8 |  1.511 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1106          
c   -- var.elim.:  1106/1106          
c   -- var.elim.:  755/755          
c   -- var.elim.:  489/489          
c   -- var.elim.:  171/171          
c   -- subsuming                       
c   -- var.elim.:  64/64          
c |     22233 |   16418    79969 |      --   16425       --      -- |     --   | -275/-6
c |     22233 |   16418    79969 |    6567   16420   587465    35.8 |  1.511 % |
c |     22334 |   16418    79969 |    7223    4967   145787    29.4 |  1.686 % |
c |     22485 |   16418    79969 |    7946    5118   150536    29.4 |  1.686 % |
c |     22711 |   16418    79969 |    8740    5344   158078    29.6 |  1.686 % |
c |     23049 |   16418    79969 |    9615    5682   167897    29.5 |  1.686 % |
c |     23556 |   16418    79969 |   10576    6189   182761    29.5 |  1.686 % |
c ==============================================================================
c (current CPU-time: 29.4005 s)
c ==============================================================================
c [1mFound solution: 50[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     23770 |   16577    80395 |    4973    6403   188027    29.4 |  1.686 % |
c   -- subsuming                       
c   -- var.elim.:  329/329          
c   -- var.elim.:  145/145          
c |     23770 |   16452    80086 |      --    6403       --      -- |     --   | -111/-166
c |     23770 |   16452    80086 |    6580    6403   188027    29.4 |  1.686 % |
c |     23870 |   16452    80086 |    7238    6503   191116    29.4 |  1.754 % |
c |     24022 |   16452    80086 |    7962    6655   197418    29.7 |  1.754 % |
c |     24247 |   16452    80086 |    8759    6880   204128    29.7 |  1.754 % |
c |     24584 |   16452    80086 |    9634    7217   215143    29.8 |  1.754 % |
c ==============================================================================
c (current CPU-time: 30.3034 s)
c ==============================================================================
c [1mFound solution: 48[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     24877 |   16682    80713 |    5004    7510   223568    29.8 |  1.754 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1626          
c   -- var.elim.:  1626/1626          
c   -- var.elim.:  1000/1760          
c   -- var.elim.:  1760/1760          
c   -- var.elim.:  489/489          
c   -- var.elim.:  405/405          
c   -- subsuming                       
c   -- var.elim.:  239/239          
c |     24877 |   16053    77350 |      --    7510       --      -- |     --   | -353/85
c |     24877 |   16053    77350 |    6421    7498   222827    29.7 |  1.754 % |
c |     24977 |   15467    73366 |    6805    5071   133181    26.3 |  5.862 % |
c |     25127 |   14985    65916 |    7252    5217   135364    25.9 |  7.522 % |
c |     25352 |   14801    64728 |    7880    5420   140446    25.9 |  8.432 % |
c |     25689 |   14767    64501 |    8648    5736   146147    25.5 |  8.677 % |
c |     26196 |   14648    62192 |    9436    6230   159298    25.6 |  9.067 % |
c ==============================================================================
c (current CPU-time: 33.165 s)
c ==============================================================================
c [1mFound solution: 44[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     26574 |   19451    75409 |    5835    6599   172702    26.2 |  9.067 % |
c   -- subsuming                       
c   -- var.elim.:  1000/9060          
c   -- var.elim.:  2000/9060          
c   -- var.elim.:  3000/9060          
c   -- var.elim.:  4000/9060          
c   -- var.elim.:  5000/9060          
c   -- var.elim.:  6000/9060          
c   -- var.elim.:  7000/9060          
c   -- var.elim.:  8000/9060          
c   -- var.elim.:  9000/9060          
c   -- var.elim.:  9060/9060          
c   -- var.elim.:  1000/4899          
c   -- var.elim.:  2000/4899          
c   -- var.elim.:  3000/4899          
c   -- var.elim.:  4000/4899          
c   -- var.elim.:  4899/4899          
c   -- var.elim.:  1000/3862          
c   -- var.elim.:  2000/3862          
c   -- var.elim.:  3000/3862          
c   -- var.elim.:  3862/3862          
c   -- var.elim.:  1000/3190          
c   -- var.elim.:  2000/3190          
c   -- var.elim.:  3000/3190          
c   -- var.elim.:  3190/3190          
c   -- var.elim.:  1000/1121          
c   -- var.elim.:  1121/1121          
c   -- var.elim.:  93/93          
c   -- subsuming                       
c   -- var.elim.:  1000/1734          
c   -- var.elim.:  1734/1734          
c   -- var.elim.:  48/48          
c |     26574 |   14093    63613 |      --    6599       --      -- |     --   | -5249/-11088
c |     26574 |   14093    63613 |    5637    6599   172702    26.2 |  9.067 % |
c |     26675 |   14093    63613 |    6200    4215    94559    22.4 | 11.536 % |
c |     26825 |   14093    63613 |    6821    4365    98839    22.6 | 11.536 % |
c |     27050 |   13972    61969 |    7438    4573   105386    23.0 | 12.047 % |
c |     27387 |   13970    61950 |    8181    4909   116594    23.8 | 12.061 % |
c |     27895 |   13970    61950 |    8999    5417   131595    24.3 | 12.061 % |
c |     28655 |   13970    61950 |    9899    6177   156641    25.4 | 12.061 % |
c ==============================================================================
c (current CPU-time: 39.69 s)
c ==============================================================================
c [1mFound solution: 42[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     28889 |   20347    79211 |    6104    6411   164237    25.6 | 12.061 % |
c   -- subsuming                       
c   -- var.elim.:  1000/9561          
c   -- var.elim.:  2000/9561          
c   -- var.elim.:  3000/9561          
c   -- var.elim.:  4000/9561          
c   -- var.elim.:  5000/9561          
c   -- var.elim.:  6000/9561          
c   -- var.elim.:  7000/9561          
c   -- var.elim.:  8000/9561          
c   -- var.elim.:  9000/9561          
c   -- var.elim.:  9561/9561          
c   -- var.elim.:  1000/4783          
c   -- var.elim.:  2000/4783          
c   -- var.elim.:  3000/4783          
c   -- var.elim.:  4000/4783          
c   -- var.elim.:  4783/4783          
c   -- var.elim.:  1000/3947          
c   -- var.elim.:  2000/3947          
c   -- var.elim.:  3000/3947          
c   -- var.elim.:  3947/3947          
c   -- var.elim.:  1000/3049          
c   -- var.elim.:  2000/3049          
c   -- var.elim.:  3000/3049          
c   -- var.elim.:  3049/3049          
c   -- var.elim.:  1000/2030          
c   -- var.elim.:  2000/2030          
c   -- var.elim.:  2030/2030          
c   -- var.elim.:  1000/1394          
c   -- var.elim.:  1394/1394          
c   -- var.elim.:  685/685          
c   -- var.elim.:  201/201          
c   -- var.elim.:  8/8          
c   -- subsuming                       
c   -- var.elim.:  257/257          
c   -- var.elim.:  36/36          
c |     28889 |   13944    62029 |      --    6411       --      -- |     --   | -6369/-17062
c |     28889 |   13944    62029 |    5577    5666   125864    22.2 | 12.061 % |
c |     28989 |   13944    62029 |    6135    5766   128392    22.3 | 12.754 % |
c |     29139 |   13944    62029 |    6748    5916   133488    22.6 | 12.754 % |
c |     29366 |   13944    62029 |    7423    6143   140135    22.8 | 12.754 % |
c ==============================================================================
c (current CPU-time: 44.9072 s)
c ==============================================================================
c [1mFound solution: 36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     29520 |   19634    67839 |    5890    6296   144753    23.0 | 12.754 % |
c   -- subsuming                       
c   -- var.elim.:  1000/7609          
c   -- var.elim.:  2000/7609          
c   -- var.elim.:  3000/7609          
c   -- var.elim.:  4000/7609          
c   -- var.elim.:  5000/7609          
c   -- var.elim.:  6000/7609          
c   -- var.elim.:  7000/7609          
c   -- var.elim.:  7609/7609          
c   -- var.elim.:  1000/4211          
c   -- var.elim.:  2000/4211          
c   -- var.elim.:  3000/4211          
c   -- var.elim.:  4000/4211          
c   -- var.elim.:  4211/4211          
c   -- var.elim.:  1000/2999          
c   -- var.elim.:  2000/2999          
c   -- var.elim.:  2999/2999          
c   -- var.elim.:  1000/1607          
c   -- var.elim.:  1607/1607          
c   -- var.elim.:  635/635          
c   -- var.elim.:  6/6          
c   -- subsuming                       
c   -- var.elim.:  405/405          
c   -- var.elim.:  121/121          
c |     29520 |    9712    32542 |      --    6296       --      -- |     --   | -6606/-16387
c |     29520 |    9712    32542 |    3884    6296   144753    23.0 | 12.754 % |
c ==============================================================================
c [1mOptimal solution: 36[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
c _______________________________________________________________________________
c 
c restarts              : 47
c conflicts             : 29525          (637 /sec)
c decisions             : 59484          (1283 /sec)
c propagations          : 7087614        (152813 /sec)
c inspects              : 41518969       (895173 /sec)
c CPU time              : 46.3809 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.97 0.91 2/54 24171
Raw data (stat): 24171 (runsolver) R 24170 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422102268 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 24171
Raw data (stat): 24171 (minisat+) R 24170 20937 20936 0 -1 0 2280 0 0 0 989 9 0 0 25 0 1 0 422102268 11190272 2198 4294967295 134512640 134672761 3221224560 3221222840 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2732 2198 603 41 0 2691 0
vsize: 10928
[startup+20.0011 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 24171
Raw data (stat): 24171 (minisat+) R 24170 20937 20936 0 -1 0 2739 0 0 0 1986 11 0 0 25 0 1 0 422102268 12800000 2576 4294967295 134512640 134672761 3221224560 3221223552 134565149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3125 2576 603 41 0 3084 0
vsize: 12500
[startup+30.0006 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 24171
Raw data (stat): 24171 (minisat+) R 24170 20937 20936 0 -1 0 3922 0 0 0 2981 16 0 0 25 0 1 0 422102268 15331328 3190 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3743 3190 603 41 0 3702 0
vsize: 14972
[startup+40.0012 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 24171
Raw data (stat): 24171 (minisat+) R 24170 20937 20936 0 -1 0 5402 0 0 0 3973 24 0 0 25 0 1 0 422102268 19476480 3729 4294967295 134512640 134672761 3221224560 3221222824 1075730078 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4755 3729 603 41 0 4714 0
vsize: 19020
[startup+46.7527 s]
Raw data (loadavg): 0.96 0.97 0.91 1/53 24171
Raw data (stat): 24171 (minisat+) R 24170 20937 20936 0 -1 0 5402 0 0 0 3973 24 0 0 25 0 1 0 422102268 19476480 3729 4294967295 134512640 134672761 3221224560 3221222824 1075730078 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4755 3729 603 41 0 4714 0
vsize: 0

Child status: 30
Real time (s): 46.7524
CPU time (s): 46.7239
CPU user time (s): 46.3879
CPU system time (s): 0.335948
CPU usage (%): 99.939
Max. virtual memory (Kb): 19020
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	36
#### END VERIFIER DATA ####