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-5pb.opb
MD5SUM	4ca29b1bc7e76812f7871e2b937d8a23
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	60
Optimality of the best value was proved	NO
Number of terms in the objective function	720
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	720
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	3
Number of bits of the biggest number in a constraint	2
Biggest sum of numbers in a constraint	720
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04084
Number of variables	720
Total number of constraints	2168
Number of constraints which are clauses	2144
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	30
Trace number 5523

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-04-14 00:34:48 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4001 boxname=wulflinc7 idbench=241 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4ca29b1bc7e76812f7871e2b937d8a23  /oldhome/oroussel/tmp/wulflinc7/normalized-s4-4-3-5pb.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc7/normalized-s4-4-3-5pb.opb /oldhome/oroussel/tmp/wulflinc7/normalized-s4-4-3-5pb.opb
IDLAUNCH: 4001
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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:        900696 kB
Buffers:         37308 kB
Cached:          77272 kB
SwapCached:          0 kB
Active:          72716 kB
Inactive:        44732 kB
HighTotal:      131008 kB
HighFree:        49868 kB
LowTotal:       903652 kB
LowFree:        850828 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10952 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:43:12 (client local time) WITH STATUS 30 IN 503.789 SECONDS
stats: 4001 0 503.789 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2168 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################################################################################################
c   -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[2119]---> BDD-cost:    1
c ---[2109]---> BDD-cost:    1
c ---[2099]---> BDD-cost:    1
c ---[2097]---> BDD-cost:    1
c ---[2083]---> BDD-cost:    1
c ---[2057]---> BDD-cost:    1
c ---[2035]---> BDD-cost:    1
c ---[2025]---> BDD-cost:    1
c ---[1976]---> BDD-cost:    1
c ---[1966]---> BDD-cost:    1
c ---[1956]---> BDD-cost:    1
c ---[1954]---> BDD-cost:    1
c ---[1940]---> BDD-cost:    1
c ---[1914]---> BDD-cost:    1
c ---[1892]---> BDD-cost:    1
c ---[1882]---> BDD-cost:    1
c ---[1864]---> BDD-cost:    1
c ---[1842]---> BDD-cost:    1
c ---[1816]---> BDD-cost:    1
c ---[1810]---> BDD-cost:    1
c ---[1808]---> BDD-cost:    1
c ---[1782]---> BDD-cost:    1
c ---[1765]---> BDD-cost:    1
c ---[1739]---> BDD-cost:    1
c ---[1733]---> BDD-cost:    1
c ---[1715]---> BDD-cost:    1
c ---[1677]---> BDD-cost:    1
c ---[1667]---> BDD-cost:    1
c ---[1630]---> BDD-cost:    1
c ---[1608]---> BDD-cost:    1
c ---[1602]---> BDD-cost:    1
c ---[1596]---> BDD-cost:    1
c ---[1563]---> BDD-cost:    1
c ---[1537]---> BDD-cost:    1
c ---[1535]---> BDD-cost:    1
c ---[1525]---> BDD-cost:    1
c ---[1488]---> BDD-cost:    1
c ---[1466]---> BDD-cost:    1
c ---[1460]---> BDD-cost:    1
c ---[1454]---> BDD-cost:    1
c ---[1452]---> BDD-cost:    1
c ---[1426]---> BDD-cost:    1
c ---[1409]---> BDD-cost:    1
c ---[1383]---> BDD-cost:    1
c ---[1377]---> BDD-cost:    1
c ---[1359]---> BDD-cost:    1
c ---[1322]---> BDD-cost:    1
c ---[1312]---> BDD-cost:    1
c ---[1298]---> BDD-cost:    1
c ---[1272]---> BDD-cost:    1
c ---[1250]---> BDD-cost:    1
c ---[1240]---> BDD-cost:    1
c ---[1222]---> BDD-cost:    1
c ---[1200]---> BDD-cost:    1
c ---[1174]---> BDD-cost:    1
c ---[1168]---> BDD-cost:    1
c ---[1158]---> BDD-cost:    1
c ---[1148]---> BDD-cost:    1
c ---[1098]---> BDD-cost:    1
c ---[1096]---> BDD-cost:    1
c ---[1047]---> BDD-cost:    1
c ---[1037]---> BDD-cost:    1
c ---[1027]---> BDD-cost:    1
c ---[1025]---> BDD-cost:    1
c ---[1023]---> BDD-cost:    1
c ---[ 997]---> BDD-cost:    1
c ---[ 979]---> BDD-cost:    1
c ---[ 953]---> BDD-cost:    1
c ---[ 935]---> BDD-cost:    1
c ---[ 914]---> BDD-cost:    1
c ---[ 888]---> BDD-cost:    1
c ---[ 882]---> BDD-cost:    1
c ---[ 864]---> BDD-cost:    1
c ---[ 842]---> BDD-cost:    1
c ---[ 816]---> BDD-cost:    1
c ---[ 810]---> BDD-cost:    1
c ---[ 804]---> BDD-cost:    1
c ---[ 786]---> BDD-cost:    1
c ---[ 749]---> BDD-cost:    1
c ---[ 739]---> BDD-cost:    1
c ---[ 721]---> BDD-cost:    1
c ---[ 700]---> BDD-cost:    1
c ---[ 674]---> BDD-cost:    1
c ---[ 668]---> BDD-cost:    1
c ---[ 654]---> BDD-cost:    1
c ---[ 629]---> BDD-cost:    1
c ---[ 607]---> BDD-cost:    1
c ---[ 597]---> BDD-cost:    1
c ---[ 564]---> BDD-cost:    1
c ---[ 538]---> BDD-cost:    1
c ---[ 536]---> BDD-cost:    1
c ---[ 526]---> BDD-cost:    1
c ---[ 477]---> BDD-cost:    1
c ---[ 467]---> BDD-cost:    1
c ---[ 457]---> BDD-cost:    1
c ---[ 455]---> BDD-cost:    1
c ---[ 437]---> BDD-cost:    1
c ---[ 415]---> BDD-cost:    1
c ---[ 389]---> BDD-cost:    1
c ---[ 383]---> BDD-cost:    1
c ---[ 381]---> BDD-cost:    1
c ---[ 355]---> BDD-cost:    1
c ---[ 337]---> BDD-cost:    1
c ---[ 311]---> BDD-cost:    1
c ---[ 305]---> BDD-cost:    1
c ---[ 287]---> BDD-cost:    1
c ---[ 249]---> BDD-cost:    1
c ---[ 239]---> BDD-cost:    1
c ---[ 186]---> BDD-cost:    1
c ---[ 176]---> BDD-cost:    1
c ---[ 170]---> BDD-cost:    1
c ---[ 168]---> BDD-cost:    1
c ---[ 154]---> BDD-cost:    1
c ---[ 128]---> BDD-cost:    1
c ---[ 106]---> BDD-cost:    1
c ---[  96]---> BDD-cost:    1
c ---[  78]---> BDD-cost:    1
c ---[  56]---> BDD-cost:    1
c ---[  30]---> BDD-cost:    1
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:  107
c ---[  22]---> BDD-cost:  107
c ---[  21]---> BDD-cost:  107
c ---[  20]---> BDD-cost:  107
c ---[  19]---> BDD-cost:  107
c ---[  18]---> BDD-cost:  107
c ---[  17]---> BDD-cost:  107
c ---[  16]---> BDD-cost:  107
c ---[  15]---> BDD-cost:  107
c ---[  14]---> BDD-cost:  107
c ---[  13]---> BDD-cost:  107
c ---[  12]---> BDD-cost:  107
c ---[  11]---> BDD-cost:  107
c ---[  10]---> BDD-cost:  107
c ---[   9]---> BDD-cost:  107
c ---[   8]---> BDD-cost:  107
c ---[   7]---> BDD-cost:  107
c ---[   6]---> BDD-cost:  107
c ---[   5]---> BDD-cost:  107
c ---[   4]---> BDD-cost:  107
c ---[   3]---> BDD-cost:  107
c ---[   2]---> BDD-cost:  107
c ---[   1]---> BDD-cost:  107
c ---[   0]---> BDD-cost:  107
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    9080    26232 |    2723       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3264          
c   -- var.elim.:  2000/3264          
c   -- var.elim.:  3000/3264          
c   -- var.elim.:  3264/3264          
c   -- var.elim.:  336/336          
c   -- subsuming                       
c   -- var.elim.:  216/216          
c   -- var.elim.:  264/264          
c   -- subsuming                       
c |         0 |    8936    25776 |      --       0       --      -- |     --   | -144/-144
c |         0 |    8936    25776 |    3574       0        0     nan |  0.000 % |
c |       101 |    8936    25776 |    3931     101     1993    19.7 |  4.412 % |
c |       255 |    8936    25776 |    4325     255     7290    28.6 |  4.412 % |
c |       482 |    8936    25776 |    4757     482    16400    34.0 |  4.412 % |
c |       819 |    8936    25776 |    5233     819    28379    34.7 |  4.412 % |
c |      1332 |    8936    25776 |    5756    1332    51485    38.7 |  4.412 % |
c |      2093 |    8936    25776 |    6332    2093    80371    38.4 |  4.412 % |
c |      3232 |    8936    25776 |    6965    3232   124280    38.5 |  4.412 % |
c |      4940 |    8936    25776 |    7662    4940   190722    38.6 |  4.412 % |
c |      7502 |    8936    25776 |    8428    7502   288577    38.5 |  4.412 % |
c |     11346 |    8936    25776 |    9271    8475   320003    37.8 |  4.412 % |
c |     17114 |    8936    25776 |   10198    7892   300938    38.1 |  4.412 % |
c |     25763 |    8936    25776 |   11217    9483   436445    46.0 |  4.412 % |
c ==============================================================================
c (current CPU-time: 19.1871 s)
c ==============================================================================
c [1mFound solution: 68[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:33028     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     36530 |   46914   114347 |   14074    8716   554162    63.6 |  4.412 % |
c   -- subsuming                       
c   -- var.elim.:  1000/25518          
c   -- var.elim.:  2000/25518          
c   -- var.elim.:  3000/25518          
c   -- var.elim.:  4000/25518          
c   -- var.elim.:  5000/25518          
c   -- var.elim.:  6000/25518          
c   -- var.elim.:  7000/25518          
c   -- var.elim.:  8000/25518          
c   -- var.elim.:  9000/25518          
c   -- var.elim.:  10000/25518          
c   -- var.elim.:  11000/25518          
c   -- var.elim.:  12000/25518          
c   -- var.elim.:  13000/25518          
c   -- var.elim.:  14000/25518          
c   -- var.elim.:  15000/25518          
c   -- var.elim.:  16000/25518          
c   -- var.elim.:  17000/25518          
c   -- var.elim.:  18000/25518          
c   -- var.elim.:  19000/25518          
c   -- var.elim.:  20000/25518          
c   -- var.elim.:  21000/25518          
c   -- var.elim.:  22000/25518          
c   -- var.elim.:  23000/25518          
c   -- var.elim.:  24000/25518          
c   -- var.elim.:  25000/25518          
c   -- var.elim.:  25518/25518          
c   -- var.elim.:  1000/12687          
c   -- var.elim.:  2000/12687          
c   -- var.elim.:  3000/12687          
c   -- var.elim.:  4000/12687          
c   -- var.elim.:  5000/12687          
c   -- var.elim.:  6000/12687          
c   -- var.elim.:  7000/12687          
c   -- var.elim.:  8000/12687          
c   -- var.elim.:  9000/12687          
c   -- var.elim.:  10000/12687          
c   -- var.elim.:  11000/12687          
c   -- var.elim.:  12000/12687          
c   -- var.elim.:  12687/12687          
c   -- var.elim.:  1000/6317          
c   -- var.elim.:  2000/6317          
c   -- var.elim.:  3000/6317          
c   -- var.elim.:  4000/6317          
c   -- var.elim.:  5000/6317          
c   -- var.elim.:  6000/6317          
c   -- var.elim.:  6317/6317          
c   -- var.elim.:  1000/5669          
c   -- var.elim.:  2000/5669          
c   -- var.elim.:  3000/5669          
c   -- var.elim.:  4000/5669          
c   -- var.elim.:  5000/5669          
c   -- var.elim.:  5669/5669          
c   -- var.elim.:  1000/4081          
c   -- var.elim.:  2000/4081          
c   -- var.elim.:  3000/4081          
c   -- var.elim.:  4000/4081          
c   -- var.elim.:  4081/4081          
c   -- var.elim.:  20/20          
c   -- subsuming                       
c   -- var.elim.:  1000/11034          
c   -- var.elim.:  2000/11034          
c   -- var.elim.:  3000/11034          
c   -- var.elim.:  4000/11034          
c   -- var.elim.:  5000/11034          
c   -- var.elim.:  6000/11034          
c   -- var.elim.:  7000/11034          
c   -- var.elim.:  8000/11034          
c   -- var.elim.:  9000/11034          
c   -- var.elim.:  10000/11034          
c   -- var.elim.:  11000/11034          
c   -- var.elim.:  11034/11034          
c   -- var.elim.:  1000/4506          
c   -- var.elim.:  2000/4506          
c   -- var.elim.:  3000/4506          
c   -- var.elim.:  4000/4506          
c   -- var.elim.:  4506/4506          
c   -- var.elim.:  1000/5352          
c   -- var.elim.:  2000/5352          
c   -- var.elim.:  3000/5352          
c   -- var.elim.:  4000/5352          
c   -- var.elim.:  5000/5352          
c   -- var.elim.:  5352/5352          
c   -- var.elim.:  1000/5709          
c   -- var.elim.:  2000/5709          
c   -- var.elim.:  3000/5709          
c   -- var.elim.:  4000/5709          
c   -- var.elim.:  5000/5709          
c   -- var.elim.:  5709/5709          
c   -- var.elim.:  1000/4141          
c   -- var.elim.:  2000/4141          
c   -- var.elim.:  3000/4141          
c   -- var.elim.:  4000/4141          
c   -- var.elim.:  4141/4141          
c   -- subsuming                       
c   -- var.elim.:  1000/6648          
c   -- var.elim.:  2000/6648          
c   -- var.elim.:  3000/6648          
c   -- var.elim.:  4000/6648          
c   -- var.elim.:  5000/6648          
c   -- var.elim.:  6000/6648          
c   -- var.elim.:  6648/6648          
c   -- var.elim.:  1000/4660          
c   -- var.elim.:  2000/4660          
c   -- var.elim.:  3000/4660          
c   -- var.elim.:  4000/4660          
c   -- var.elim.:  4660/4660          
c   -- var.elim.:  1000/2826          
c   -- var.elim.:  2000/2826          
c   -- var.elim.:  2826/2826          
c   -- var.elim.:  1000/3400          
c   -- var.elim.:  2000/3400          
c   -- var.elim.:  3000/3400          
c   -- var.elim.:  3400/3400          
c   -- subsuming                       
c   -- var.elim.:  1000/5390          
c   -- var.elim.:  2000/5390          
c   -- var.elim.:  3000/5390          
c   -- var.elim.:  4000/5390          
c   -- var.elim.:  5000/5390          
c   -- var.elim.:  5390/5390          
c   -- var.elim.:  1000/2197          
c   -- var.elim.:  2000/2197          
c   -- var.elim.:  2197/2197          
c   -- var.elim.:  1000/1768          
c   -- var.elim.:  1768/1768          
c   -- var.elim.:  1000/1841          
c   -- var.elim.:  1841/1841          
c   -- subsuming                       
c   -- var.elim.:  1000/2268          
c   -- var.elim.:  2000/2268          
c   -- var.elim.:  2268/2268          
c |     36530 |   32654   189960 |      --    8716       --      -- |     --   | -14164/75887
c |     36530 |   32654   189960 |   13061    8716   554162    63.6 |  4.412 % |
c |     36631 |   32654   189960 |   14367    8817   560616    63.6 |  1.523 % |
c |     36782 |   32654   189960 |   15804    8968   567289    63.3 |  1.523 % |
c |     37007 |   32654   189960 |   17384    9193   577325    62.8 |  1.523 % |
c |     37344 |   32654   189960 |   19123    9530   600098    63.0 |  1.523 % |
c |     37852 |   32654   189960 |   21035   10038   618374    61.6 |  1.523 % |
c |     38611 |   32654   189960 |   23139   10797   648667    60.1 |  1.523 % |
c |     39755 |   32654   189960 |   25453   11941   747901    62.6 |  1.523 % |
c |     41466 |   32654   189960 |   27998   13652   855811    62.7 |  1.523 % |
c |     44032 |   32654   189960 |   30798   16218  1099989    67.8 |  1.523 % |
c |     47878 |   32654   189960 |   33878   20064  1340387    66.8 |  1.523 % |
c |     53645 |   32654   189960 |   37266   25831  1846484    71.5 |  1.523 % |
c |     62297 |   32654   189960 |   40992   34483  2592835    75.2 |  1.523 % |
c |     75273 |   32639   189832 |   45071   19809  1418503    71.6 |  1.572 % |
c |     94737 |   32610   189619 |   49534   39272  2540051    64.7 |  1.655 % |
c |    123929 |   32347   187426 |   54048   33017  1689240    51.2 |  2.402 % |
c |    167718 |   32347   187426 |   59453   37519  1430237    38.1 |  2.402 % |
c |    233405 |   32185   186111 |   65071   48153  1801037    37.4 |  2.866 % |
c ==============================================================================
c (current CPU-time: 354.777 s)
c ==============================================================================
c [1mFound solution: 66[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 |    240003 |   38387   203411 |   11516   54747  2111570    38.6 |  2.866 % |
c   -- subsuming                       
c   -- var.elim.:  1000/13772          
c   -- var.elim.:  2000/13772          
c   -- var.elim.:  3000/13772          
c   -- var.elim.:  4000/13772          
c   -- var.elim.:  5000/13772          
c   -- var.elim.:  6000/13772          
c   -- var.elim.:  7000/13772          
c   -- var.elim.:  8000/13772          
c   -- var.elim.:  9000/13772          
c   -- var.elim.:  10000/13772          
c   -- var.elim.:  11000/13772          
c   -- var.elim.:  12000/13772          
c   -- var.elim.:  13000/13772          
c   -- var.elim.:  13772/13772          
c   -- var.elim.:  1000/5427          
c   -- var.elim.:  2000/5427          
c   -- var.elim.:  3000/5427          
c   -- var.elim.:  4000/5427          
c   -- var.elim.:  5000/5427          
c   -- var.elim.:  5427/5427          
c   -- var.elim.:  1000/2735          
c   -- var.elim.:  2000/2735          
c   -- var.elim.:  2735/2735          
c   -- var.elim.:  1000/3559          
c   -- var.elim.:  2000/3559          
c   -- var.elim.:  3000/3559          
c   -- var.elim.:  3559/3559          
c   -- var.elim.:  459/459          
c   -- subsuming                       
c   -- var.elim.:  1000/5011          
c   -- var.elim.:  2000/5011          
c   -- var.elim.:  3000/5011          
c   -- var.elim.:  4000/5011          
c   -- var.elim.:  5000/5011          
c   -- var.elim.:  5011/5011          
c   -- var.elim.:  1000/3097          
c   -- var.elim.:  2000/3097          
c   -- var.elim.:  3000/3097          
c   -- var.elim.:  3097/3097          
c   -- var.elim.:  1000/3132          
c   -- var.elim.:  2000/3132          
c   -- var.elim.:  3000/3132          
c   -- var.elim.:  3132/3132          
c   -- var.elim.:  1000/2510          
c   -- var.elim.:  2000/2510          
c   -- var.elim.:  2510/2510          
c   -- var.elim.:  1000/1779          
c   -- var.elim.:  1779/1779          
c   -- var.elim.:  1000/1510          
c   -- var.elim.:  1510/1510          
c   -- var.elim.:  507/507          
c   -- var.elim.:  42/42          
c   -- subsuming                       
c   -- var.elim.:  1000/1068          
c   -- var.elim.:  1068/1068          
c   -- var.elim.:  1000/1055          
c   -- var.elim.:  1055/1055          
c |    240003 |   32298   186917 |      --   54747       --      -- |     --   | -6080/-16372
c |    240003 |   32298   186917 |   12919   54745  2111530    38.6 |  2.866 % |
c |    240105 |   32298   186917 |   14211   10984   408938    37.2 |  3.023 % |
c |    240255 |   32298   186917 |   15632   11134   414370    37.2 |  3.023 % |
c |    240484 |   32298   186917 |   17195   11363   422006    37.1 |  3.023 % |
c |    240824 |   32256   186574 |   18890   11702   435131    37.2 |  3.134 % |
c |    241330 |   32256   186574 |   20779   12208   454579    37.2 |  3.134 % |
c |    242089 |   32256   186574 |   22857   12967   482235    37.2 |  3.134 % |
c |    243228 |   32256   186574 |   25143   14106   522015    37.0 |  3.134 % |
c |    244938 |   32235   186509 |   27639   15814   587187    37.1 |  3.175 % |
c |    247502 |   32235   186509 |   30403   18378   691951    37.7 |  3.175 % |
c |    251348 |   32185   186043 |   33391   22223   847130    38.1 |  3.327 % |
c |    257115 |   32150   185736 |   36691   27987  1089207    38.9 |  3.410 % |
c ==============================================================================
c (current CPU-time: 440.522 s)
c ==============================================================================
c [1mFound solution: 62[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 |    263916 |   37093   191518 |   11127   34689  1421732    41.0 |  3.410 % |
c   -- subsuming                       
c   -- var.elim.:  1000/14999          
c   -- var.elim.:  2000/14999          
c   -- var.elim.:  3000/14999          
c   -- var.elim.:  4000/14999          
c   -- var.elim.:  5000/14999          
c   -- var.elim.:  6000/14999          
c   -- var.elim.:  7000/14999          
c   -- var.elim.:  8000/14999          
c   -- var.elim.:  9000/14999          
c   -- var.elim.:  10000/14999          
c   -- var.elim.:  11000/14999          
c   -- var.elim.:  12000/14999          
c   -- var.elim.:  13000/14999          
c   -- var.elim.:  14000/14999          
c   -- var.elim.:  14999/14999          
c   -- var.elim.:  1000/6662          
c   -- var.elim.:  2000/6662          
c   -- var.elim.:  3000/6662          
c   -- var.elim.:  4000/6662          
c   -- var.elim.:  5000/6662          
c   -- var.elim.:  6000/6662          
c   -- var.elim.:  6662/6662          
c   -- var.elim.:  1000/4524          
c   -- var.elim.:  2000/4524          
c   -- var.elim.:  3000/4524          
c   -- var.elim.:  4000/4524          
c   -- var.elim.:  4524/4524          
c   -- var.elim.:  1000/4619          
c   -- var.elim.:  2000/4619          
c   -- var.elim.:  3000/4619          
c   -- var.elim.:  4000/4619          
c   -- var.elim.:  4619/4619          
c   -- var.elim.:  1000/2624          
c   -- var.elim.:  2000/2624          
c   -- var.elim.:  2624/2624          
c   -- var.elim.:  1000/2153          
c   -- var.elim.:  2000/2153          
c   -- var.elim.:  2153/2153          
c   -- var.elim.:  1000/1613          
c   -- var.elim.:  1613/1613          
c   -- var.elim.:  689/689          
c   -- var.elim.:  140/140          
c   -- subsuming                       
c   -- var.elim.:  221/221          
c |    263916 |   30440   171931 |      --   34689       --      -- |     --   | -6639/-19529
c |    263916 |   30440   171931 |   12176   29875  1168128    39.1 |  3.410 % |
c |    264016 |   30314   170794 |   13338    9699   325945    33.6 |  7.482 % |
c ==============================================================================
c (current CPU-time: 467.038 s)
c ==============================================================================
c [1mFound solution: 60[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 |    264052 |   37102   189499 |   11130    9734   326738    33.6 |  7.482 % |
c   -- subsuming                       
c   -- var.elim.:  1000/13183          
c   -- var.elim.:  2000/13183          
c   -- var.elim.:  3000/13183          
c   -- var.elim.:  4000/13183          
c   -- var.elim.:  5000/13183          
c   -- var.elim.:  6000/13183          
c   -- var.elim.:  7000/13183          
c   -- var.elim.:  8000/13183          
c   -- var.elim.:  9000/13183          
c   -- var.elim.:  10000/13183          
c   -- var.elim.:  11000/13183          
c   -- var.elim.:  12000/13183          
c   -- var.elim.:  13000/13183          
c   -- var.elim.:  13183/13183          
c   -- var.elim.:  1000/6660          
c   -- var.elim.:  2000/6660          
c   -- var.elim.:  3000/6660          
c   -- var.elim.:  4000/6660          
c   -- var.elim.:  5000/6660          
c   -- var.elim.:  6000/6660          
c   -- var.elim.:  6660/6660          
c   -- var.elim.:  1000/3697          
c   -- var.elim.:  2000/3697          
c   -- var.elim.:  3000/3697          
c   -- var.elim.:  3697/3697          
c   -- var.elim.:  1000/4463          
c   -- var.elim.:  2000/4463          
c   -- var.elim.:  3000/4463          
c   -- var.elim.:  4000/4463          
c   -- var.elim.:  4463/4463          
c   -- var.elim.:  1000/1504          
c   -- var.elim.:  1504/1504          
c   -- subsuming                       
c   -- var.elim.:  1000/4928          
c   -- var.elim.:  2000/4928          
c   -- var.elim.:  3000/4928          
c   -- var.elim.:  4000/4928          
c   -- var.elim.:  4928/4928          
c   -- var.elim.:  1000/2585          
c   -- var.elim.:  2000/2585          
c   -- var.elim.:  2585/2585          
c   -- var.elim.:  1000/2674          
c   -- var.elim.:  2000/2674          
c   -- var.elim.:  2674/2674          
c   -- var.elim.:  1000/1916          
c   -- var.elim.:  1916/1916          
c   -- var.elim.:  336/336          
c   -- subsuming                       
c |    264052 |   30106   168671 |      --    9734       --      -- |     --   | -6776/-17512
c |    264052 |   30106   168671 |   12042    9340   291996    31.3 |  7.482 % |
c |    264153 |   29892   166309 |   13152    9437   293226    31.1 |  8.389 % |
c ==============================================================================
c [1mOptimal solution: 60[0m
s OPTIMUM FOUND
v -v1 -v2 -v3 -v4 -v5 -v6 -v7 -v8 -v9 -v10 -v11 -v12 -v13 -v14 v15 -v16 -v17 -v18 -v19 -v20 -v21 -v22 -v23 -v24 -v25 -v26 -v27 -v28 -v29 -v30 -v31 -v32 -v33 -v34 -v35 v36 -v37 -v38 -v39 v40 -v41 -v42 -v43 v44 -v45 -v46 -v47 v48 v49 -v50 -v51 -v52 v53 -v54 -v55 -v56 -v57 -v58 -v59 -v60 -v61 v62 -v63 -v64 -v65 -v66 -v67 -v68 -v69 -v70 -v71 -v72 v73 v74 -v75 -v76 -v77 -v78 -v79 -v80 -v81 -v82 -v83 -v84 -v85 -v86 -v87 -v88 -v89 -v90 -v91 -v92 -v93 -v94 -v95 -v96 -v97 -v98 -v99 -v100 -v101 -v102 -v103 -v104 -v105 -v106 v107 v108 -v109 -v110 -v111 -v112 -v113 -v114 -v115 -v116 -v117 -v118 -v119 -v120 -v121 -v122 -v123 -v124 -v125 -v126 v127 v128 -v129 -v130 -v131 -v132 -v133 -v134 -v135 -v136 -v137 -v138 -v139 -v140 v141 -v142 -v143 -v144 -v145 -v146 -v147 v148 v149 v150 -v151 -v152 -v153 -v154 -v155 -v156 -v157 -v158 -v159 -v160 v161 -v162 -v163 -v164 -v165 -v166 -v167 -v168 -v169 -v170 -v171 v172 -v173 -v174 -v175 -v176 -v177 -v178 -v179 -v180 -v181 -v182 -v183 -v184 -v185 v186 -v187 -v188 -v189 -v190 -v191 -v192 -v193 -v194 -v195 -v196 -v197 -v198 -v199 -v200 v201 -v202 -v203 -v204 -v205 -v206 -v207 -v208 -v209 -v210 -v211 -v212 -v213 -v214 -v215 -v216 -v217 -v218 -v219 -v220 -v221 -v222 -v223 -v224 -v225 -v226 -v227 -v228 -v229 -v230 -v231 -v232 -v233 -v234 -v235 -v236 -v237 v238 -v239 -v240 v241 v242 -v243 -v244 -v245 -v246 -v247 -v248 -v249 -v250 -v251 -v252 -v253 -v254 v255 -v256 -v257 -v258 -v259 -v260 -v261 -v262 -v263 -v264 -v265 -v266 -v267 -v268 -v269 -v270 v271 -v272 -v273 -v274 -v275 -v276 -v277 -v278 -v279 -v280 -v281 v282 -v283 -v284 -v285 -v286 -v287 -v288 -v289 -v290 -v291 -v292 -v293 -v294 -v295 -v296 -v297 -v298 -v299 v300 -v301 -v302 -v303 -v304 -v305 -v306 -v307 -v308 -v309 -v310 -v311 v312 -v313 -v314 -v315 -v316 -v317 -v318 -v319 -v320 -v321 -v322 -v323 -v324 -v325 v326 -v327 -v328 -v329 v330 -v331 -v332 -v333 v334 -v335 -v336 -v337 -v338 -v339 v340 v341 -v342 -v343 -v344 -v345 -v346 -v347 -v348 -v349 -v350 -v351 -v352 -v353 -v354 v355 -v356 -v357 -v358 v359 -v360 -v361 -v362 -v363 -v364 -v365 v366 -v367 -v368 -v369 -v370 -v371 -v372 -v373 -v374 -v375 -v376 -v377 -v378 -v379 v380 -v381 -v382 -v383 -v384 -v385 -v386 -v387 -v388 -v389 -v390 -v391 -v392 -v393 -v394 -v395 -v396 -v397 -v398 -v399 -v400 -v401 -v402 -v403 -v404 -v405 -v406 -v407 v408 -v409 -v410 -v411 -v412 -v413 -v414 -v415 -v416 -v417 -v418 v419 -v420 -v421 -v422 -v423 -v424 -v425 -v426 -v427 -v428 -v429 -v430 v431 -v432 -v433 -v434 -v435 -v436 -v437 -v438 -v439 -v440 -v441 -v442 v443 -v444 -v445 -v446 -v447 -v448 -v449 -v450 -v451 -v452 -v453 -v454 -v455 -v456 -v457 -v458 -v459 -v460 -v461 -v462 v463 v464 -v465 -v466 -v467 -v468 -v469 -v470 -v471 -v472 -v473 -v474 -v475 -v476 -v477 -v478 -v479 -v480 -v481 -v482 -v483 -v484 -v485 -v486 -v487 v488 -v489 -v490 -v491 -v492 -v493 -v494 -v495 -v496 -v497 -v498 -v499 -v500 -v501 v502 -v503 -v504 -v505 -v506 -v507 -v508 -v509 -v510 -v511 -v512 -v513 -v514 -v515 -v516 -v517 -v518 -v519 -v520 -v521 -v522 v523 -v524 -v525 -v526 v527 -v528 -v529 -v530 -v531 -v532 -v533 v534 -v535 -v536 -v537 -v538 -v539 -v540 -v541 -v542 -v543 v544 -v545 -v546 v547 -v548 -v549 -v550 -v551 -v552 -v553 -v554 -v555 -v556 -v557 -v558 -v559 -v560 -v561 -v562 -v563 -v564 -v565 -v566 v567 -v568 -v569 -v570 -v571 -v572 -v573 -v574 -v575 -v576 -v577 v578 -v579 -v580 -v581 -v582 -v583 -v584 -v585 -v586 -v587 -v588 -v589 -v590 -v591 -v592 -v593 -v594 -v595 -v596 -v597 -v598 -v599 -v600 -v601 -v602 -v603 -v604 -v605 -v606 -v607 -v608 -v609 -v610 -v611 -v612 v613 -v614 -v615 -v616 -v617 -v618 -v619 -v620 -v621 -v622 -v623 -v624 -v625 -v626 -v627 -v628 -v629 -v630 -v631 -v632 -v633 -v634 -v635 -v636 -v637 -v638 -v639 v640 -v641 -v642 -v643 v644 -v645 -v646 -v647 -v648 -v649 -v650 -v651 -v652 -v653 -v654 -v655 -v656 -v657 -v658 -v659 -v660 -v661 v662 -v663 -v664 -v665 -v666 -v667 -v668 -v669 -v670 -v671 -v672 -v673 -v674 v675 -v676 -v677 -v678 -v679 -v680 -v681 -v682 -v683 -v684 -v685 -v686 -v687 -v688 -v689 -v690 -v691 -v692 -v693 -v694 -v695 -v696 -v697 -v698 -v699 -v700 -v701 -v702 -v703 -v704 -v705 v706 -v707 -v708 -v709 -v710 -v711 -v712 -v713 -v714 -v715 -v716 -v717 -v718 -v719 -v720
c _______________________________________________________________________________
c 
c restarts              : 47
c conflicts             : 264158         (525 /sec)
c decisions             : 433314         (861 /sec)
c propagations          : 47092040       (93617 /sec)
c inspects              : 686276022      (1364283 /sec)
c CPU time              : 503.031 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.95 0.90 2/54 26846
Raw data (stat): 26846 (runsolver) R 26845 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422093489 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.0011 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 1441 0 0 0 993 4 0 0 25 0 1 0 422093489 7491584 1409 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1829 1409 603 41 0 1788 0
vsize: 7316
[startup+20.0011 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 4930 0 0 0 1984 14 0 0 25 0 1 0 422093489 22454272 4766 4294967295 134512640 134672761 3221224560 3221223232 134631080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5482 4766 603 41 0 5441 0
vsize: 21928
[startup+30.0018 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 5105 0 0 0 2978 19 0 0 25 0 1 0 422093489 22892544 4890 4294967295 134512640 134672761 3221224560 3221223008 134643963 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5589 4890 603 41 0 5548 0
vsize: 22356
[startup+40.0013 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 5158 0 0 0 3977 20 0 0 25 0 1 0 422093489 23162880 4943 4294967295 134512640 134672761 3221224560 3221223008 134644040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5655 4943 603 41 0 5614 0
vsize: 22620
[startup+50.0022 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 5308 0 0 0 4977 21 0 0 25 0 1 0 422093489 23724032 5063 4294967295 134512640 134672761 3221224560 3221222544 134566493 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5792 5063 603 41 0 5751 0
vsize: 23168
[startup+60.0016 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 5308 0 0 0 5975 22 0 0 25 0 1 0 422093489 23195648 4966 4294967295 134512640 134672761 3221224560 3221223008 134644032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5663 4966 603 41 0 5622 0
vsize: 22652
[startup+70.0012 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 5309 0 0 0 6972 25 0 0 25 0 1 0 422093489 23195648 4967 4294967295 134512640 134672761 3221224560 3221223008 134643511 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5663 4967 603 41 0 5622 0
vsize: 22652
[startup+80.0025 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 5401 0 0 0 7972 25 0 0 25 0 1 0 422093489 23195648 4967 4294967295 134512640 134672761 3221224560 3221223008 134643542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5663 4967 603 41 0 5622 0
vsize: 22652
[startup+90.0015 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 5493 0 0 0 8971 26 0 0 25 0 1 0 422093489 23699456 5059 4294967295 134512640 134672761 3221224560 3221223052 134642768 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5786 5059 603 41 0 5745 0
vsize: 23144
[startup+100.001 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 5493 0 0 0 9970 28 0 0 25 0 1 0 422093489 23195648 4967 4294967295 134512640 134672761 3221224560 3221223008 134643715 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5663 4967 603 41 0 5622 0
vsize: 22652
[startup+110.001 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 5615 0 0 0 10969 28 0 0 25 0 1 0 422093489 23195648 4967 4294967295 134512640 134672761 3221224560 3221223008 134643570 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5663 4967 603 41 0 5622 0
vsize: 22652
[startup+120 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 6715 0 0 0 11967 31 0 0 25 0 1 0 422093489 27770880 6067 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6780 6067 603 41 0 6739 0
vsize: 27120
[startup+130 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 7512 0 0 0 12966 32 0 0 25 0 1 0 422093489 31072256 6864 4294967295 134512640 134672761 3221224560 3221223372 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7586 6864 603 41 0 7545 0
vsize: 30344
[startup+140 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 8453 0 0 0 13963 35 0 0 25 0 1 0 422093489 35082240 7805 4294967295 134512640 134672761 3221224560 3221223744 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8565 7805 603 41 0 8524 0
vsize: 34260
[startup+150 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 8456 0 0 0 14963 35 0 0 25 0 1 0 422093489 35082240 7808 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8565 7808 603 41 0 8524 0
vsize: 34260
[startup+160 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 8456 0 0 0 15963 35 0 0 25 0 1 0 422093489 35082240 7808 4294967295 134512640 134672761 3221224560 3221223696 134614727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8565 7808 603 41 0 8524 0
vsize: 34260
[startup+170 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 8462 0 0 0 16963 35 0 0 25 0 1 0 422093489 35082240 7814 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8565 7814 603 41 0 8524 0
vsize: 34260
[startup+180 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 8714 0 0 0 17963 36 0 0 25 0 1 0 422093489 36032512 8048 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8797 8048 603 41 0 8756 0
vsize: 35188
[startup+190 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 8714 0 0 0 18963 36 0 0 25 0 1 0 422093489 36032512 8048 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8797 8048 603 41 0 8756 0
vsize: 35188
[startup+200.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 8716 0 0 0 19963 36 0 0 25 0 1 0 422093489 36032512 8050 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8797 8050 603 41 0 8756 0
vsize: 35188
[startup+210.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 8717 0 0 0 20963 36 0 0 25 0 1 0 422093489 36032512 8051 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8797 8051 603 41 0 8756 0
vsize: 35188
[startup+220.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 8811 0 0 0 21963 37 0 0 25 0 1 0 422093489 36163584 8091 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8829 8091 603 41 0 8788 0
vsize: 35316
[startup+230.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 8814 0 0 0 22963 37 0 0 25 0 1 0 422093489 36163584 8094 4294967295 134512640 134672761 3221224560 3221223744 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8829 8094 603 41 0 8788 0
vsize: 35316
[startup+240.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 8837 0 0 0 23963 37 0 0 25 0 1 0 422093489 36360192 8117 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8877 8117 603 41 0 8836 0
vsize: 35508
[startup+250.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 8858 0 0 0 24964 37 0 0 25 0 1 0 422093489 36556800 8138 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8925 8138 603 41 0 8884 0
vsize: 35700
[startup+260.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 8872 0 0 0 25964 37 0 0 25 0 1 0 422093489 36556800 8152 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8925 8152 603 41 0 8884 0
vsize: 35700
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 8872 0 0 0 26964 37 0 0 25 0 1 0 422093489 36556800 8152 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8925 8152 603 41 0 8884 0
vsize: 35700
[startup+280.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 8876 0 0 0 27964 37 0 0 25 0 1 0 422093489 36556800 8156 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8925 8156 603 41 0 8884 0
vsize: 35700
[startup+290.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 8969 0 0 0 28964 37 0 0 25 0 1 0 422093489 36950016 8249 4294967295 134512640 134672761 3221224560 3221223616 134644275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9021 8249 603 41 0 8980 0
vsize: 36084
[startup+300.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 8975 0 0 0 29964 37 0 0 25 0 1 0 422093489 36687872 8196 4294967295 134512640 134672761 3221224560 3221223744 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8957 8196 603 41 0 8916 0
vsize: 35828
[startup+310.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 8999 0 0 0 30964 37 0 0 25 0 1 0 422093489 36884480 8220 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9005 8220 603 41 0 8964 0
vsize: 36020
[startup+320.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 9017 0 0 0 31964 37 0 0 25 0 1 0 422093489 36884480 8238 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9005 8238 603 41 0 8964 0
vsize: 36020
[startup+330.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 9036 0 0 0 32964 38 0 0 25 0 1 0 422093489 37146624 8257 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9069 8257 603 41 0 9028 0
vsize: 36276
[startup+340.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 9045 0 0 0 33965 38 0 0 25 0 1 0 422093489 37146624 8266 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9069 8266 603 41 0 9028 0
vsize: 36276
[startup+350.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 9045 0 0 0 34965 38 0 0 25 0 1 0 422093489 37146624 8266 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9069 8266 603 41 0 9028 0
vsize: 36276
[startup+360.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 10145 0 0 0 35957 45 0 0 25 0 1 0 422093489 40599552 8645 4294967295 134512640 134672761 3221224560 3221223008 134644008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9912 8645 603 41 0 9871 0
vsize: 39648
[startup+370.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 10145 0 0 0 36957 46 0 0 25 0 1 0 422093489 40599552 8645 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9912 8645 603 41 0 9871 0
vsize: 39648
[startup+380.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 10237 0 0 0 37956 47 0 0 25 0 1 0 422093489 40599552 8645 4294967295 134512640 134672761 3221224560 3221222840 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9912 8645 603 41 0 9871 0
vsize: 39648
[startup+390.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 10237 0 0 0 38956 47 0 0 25 0 1 0 422093489 40599552 8645 4294967295 134512640 134672761 3221224560 3221223008 134643977 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9912 8645 603 41 0 9871 0
vsize: 39648
[startup+400.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 10378 0 0 0 39955 48 0 0 25 0 1 0 422093489 40861696 8699 4294967295 134512640 134672761 3221224560 3221223616 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9976 8699 603 41 0 9935 0
vsize: 39904
[startup+410.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 10382 0 0 0 40955 48 0 0 25 0 1 0 422093489 40599552 8649 4294967295 134512640 134672761 3221224560 3221223600 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9912 8649 603 41 0 9871 0
vsize: 39648
[startup+420.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 10382 0 0 0 41956 48 0 0 25 0 1 0 422093489 40599552 8649 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9912 8649 603 41 0 9871 0
vsize: 39648
[startup+430.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 10382 0 0 0 42956 48 0 0 25 0 1 0 422093489 40599552 8649 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9912 8649 603 41 0 9871 0
vsize: 39648
[startup+440.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 10382 0 0 0 43956 48 0 0 25 0 1 0 422093489 40599552 8649 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9912 8649 603 41 0 9871 0
vsize: 39648
[startup+450.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 11673 0 0 0 44945 58 0 0 25 0 1 0 422093489 40738816 8802 4294967295 134512640 134672761 3221224560 3221223008 134643959 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9946 8802 603 41 0 9905 0
vsize: 39784
[startup+460.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 11673 0 0 0 45944 59 0 0 25 0 1 0 422093489 40738816 8802 4294967295 134512640 134672761 3221224560 3221223040 134541817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9946 8802 603 41 0 9905 0
vsize: 39784
[startup+470.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 13130 0 0 0 46935 69 0 0 25 0 1 0 422093489 40759296 8918 4294967295 134512640 134672761 3221224560 3221222736 134566718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9951 8918 603 41 0 9910 0
vsize: 39804
[startup+480.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 13130 0 0 0 47934 70 0 0 25 0 1 0 422093489 40759296 8918 4294967295 134512640 134672761 3221224560 3221223008 134643820 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9951 8918 603 41 0 9910 0
vsize: 39804
[startup+490.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 13222 0 0 0 48933 70 0 0 25 0 1 0 422093489 41488384 9010 4294967295 134512640 134672761 3221224560 3221222272 134566540 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10129 9010 603 41 0 10088 0
vsize: 40516
[startup+500.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 13222 0 0 0 49933 71 0 0 25 0 1 0 422093489 40759296 8918 4294967295 134512640 134672761 3221224560 3221223008 134643539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9951 8918 603 41 0 9910 0
vsize: 39804
[startup+503.749 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 26846
Raw data (stat): 26846 (minisat+) R 26845 22932 22931 0 -1 0 13222 0 0 0 49933 71 0 0 25 0 1 0 422093489 40759296 8918 4294967295 134512640 134672761 3221224560 3221223008 134643539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9951 8918 603 41 0 9910 0
vsize: 0

Child status: 30
Real time (s): 503.749
CPU time (s): 503.789
CPU user time (s): 503.043
CPU system time (s): 0.746886
CPU usage (%): 100.008
Max. virtual memory (Kb): 40516
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	60
#### END VERIFIER DATA ####