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-3pb.opb
MD5SUM	c267b57d74142f6538ad16680277f9bf
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	62
Optimality of the best value was proved	NO
Number of terms in the objective function	648
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	648
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	648
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.02984
Number of variables	648
Total number of constraints	1954
Number of constraints which are clauses	1930
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	27
Trace number 5522

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-04-14 00:33:54 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3999 boxname=wulflinc19 idbench=239 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c267b57d74142f6538ad16680277f9bf  /oldhome/oroussel/tmp/wulflinc19/normalized-s4-4-3-3pb.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc19/normalized-s4-4-3-3pb.opb /oldhome/oroussel/tmp/wulflinc19/normalized-s4-4-3-3pb.opb
IDLAUNCH: 3999
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 3
cpu MHz		: 451.037
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:        889156 kB
Buffers:         34400 kB
Cached:          77472 kB
SwapCached:         56 kB
Active:          47964 kB
Inactive:        66888 kB
HighTotal:      131008 kB
HighFree:        49448 kB
LowTotal:       903652 kB
LowFree:        839708 kB
SwapTotal:     2097892 kB
SwapFree:      2097836 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7028 kB
Slab:            25032 kB
Committed_AS:    63708 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 00:42:57 (client local time) WITH STATUS 30 IN 543.419 SECONDS
stats: 3999 0 543.419 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1954 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ############################################################################################################
c   -- Clauses(.)/Splits(s): ..................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[1944]---> BDD-cost:    1
c ---[1934]---> BDD-cost:    1
c ---[1885]---> BDD-cost:    1
c ---[1883]---> BDD-cost:    1
c ---[1869]---> BDD-cost:    1
c ---[1843]---> BDD-cost:    1
c ---[1821]---> BDD-cost:    1
c ---[1811]---> BDD-cost:    1
c ---[1778]---> BDD-cost:    1
c ---[1752]---> BDD-cost:    1
c ---[1750]---> BDD-cost:    1
c ---[1740]---> BDD-cost:    1
c ---[1726]---> BDD-cost:    1
c ---[1700]---> BDD-cost:    1
c ---[1678]---> BDD-cost:    1
c ---[1668]---> BDD-cost:    1
c ---[1654]---> BDD-cost:    1
c ---[1628]---> BDD-cost:    1
c ---[1606]---> BDD-cost:    1
c ---[1596]---> BDD-cost:    1
c ---[1594]---> BDD-cost:    1
c ---[1568]---> BDD-cost:    1
c ---[1550]---> BDD-cost:    1
c ---[1525]---> BDD-cost:    1
c ---[1507]---> BDD-cost:    1
c ---[1485]---> BDD-cost:    1
c ---[1459]---> BDD-cost:    1
c ---[1453]---> BDD-cost:    1
c ---[1435]---> BDD-cost:    1
c ---[1413]---> BDD-cost:    1
c ---[1387]---> BDD-cost:    1
c ---[1381]---> BDD-cost:    1
c ---[1333]---> BDD-cost:    1
c ---[1323]---> BDD-cost:    1
c ---[1313]---> BDD-cost:    1
c ---[1311]---> BDD-cost:    1
c ---[1258]---> BDD-cost:    1
c ---[1248]---> BDD-cost:    1
c ---[1242]---> BDD-cost:    1
c ---[1240]---> BDD-cost:    1
c ---[1203]---> BDD-cost:    1
c ---[1181]---> BDD-cost:    1
c ---[1175]---> BDD-cost:    1
c ---[1169]---> BDD-cost:    1
c ---[1167]---> BDD-cost:    1
c ---[1141]---> BDD-cost:    1
c ---[1123]---> BDD-cost:    1
c ---[1097]---> BDD-cost:    1
c ---[1060]---> BDD-cost:    1
c ---[1038]---> BDD-cost:    1
c ---[1032]---> BDD-cost:    1
c ---[1026]---> BDD-cost:    1
c ---[1024]---> BDD-cost:    1
c ---[ 998]---> BDD-cost:    1
c ---[ 980]---> BDD-cost:    1
c ---[ 954]---> BDD-cost:    1
c ---[ 952]---> BDD-cost:    1
c ---[ 926]---> BDD-cost:    1
c ---[ 908]---> BDD-cost:    1
c ---[ 882]---> BDD-cost:    1
c ---[ 868]---> BDD-cost:    1
c ---[ 842]---> BDD-cost:    1
c ---[ 820]---> BDD-cost:    1
c ---[ 810]---> BDD-cost:    1
c ---[ 792]---> BDD-cost:    1
c ---[ 771]---> BDD-cost:    1
c ---[ 745]---> BDD-cost:    1
c ---[ 739]---> BDD-cost:    1
c ---[ 722]---> BDD-cost:    1
c ---[ 700]---> BDD-cost:    1
c ---[ 674]---> BDD-cost:    1
c ---[ 668]---> BDD-cost:    1
c ---[ 658]---> BDD-cost:    1
c ---[ 648]---> BDD-cost:    1
c ---[ 598]---> BDD-cost:    1
c ---[ 596]---> BDD-cost:    1
c ---[ 586]---> BDD-cost:    1
c ---[ 576]---> BDD-cost:    1
c ---[ 526]---> BDD-cost:    1
c ---[ 524]---> BDD-cost:    1
c ---[ 487]---> BDD-cost:    1
c ---[ 465]---> BDD-cost:    1
c ---[ 459]---> BDD-cost:    1
c ---[ 453]---> BDD-cost:    1
c ---[ 400]---> BDD-cost:    1
c ---[ 390]---> BDD-cost:    1
c ---[ 384]---> BDD-cost:    1
c ---[ 382]---> BDD-cost:    1
c ---[ 372]---> BDD-cost:    1
c ---[ 362]---> BDD-cost:    1
c ---[ 312]---> BDD-cost:    1
c ---[ 310]---> BDD-cost:    1
c ---[ 304]---> BDD-cost:    1
c ---[ 286]---> BDD-cost:    1
c ---[ 248]---> BDD-cost:    1
c ---[ 238]---> BDD-cost:    1
c ---[ 236]---> BDD-cost:    1
c ---[ 210]---> BDD-cost:    1
c ---[ 192]---> BDD-cost:    1
c ---[ 166]---> BDD-cost:    1
c ---[ 129]---> BDD-cost:    1
c ---[ 107]---> BDD-cost:    1
c ---[ 101]---> BDD-cost:    1
c ---[  95]---> 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:   95
c ---[  22]---> BDD-cost:   95
c ---[  21]---> BDD-cost:   95
c ---[  20]---> BDD-cost:   95
c ---[  19]---> BDD-cost:   95
c ---[  18]---> BDD-cost:   95
c ---[  17]---> BDD-cost:   95
c ---[  16]---> BDD-cost:   95
c ---[  15]---> BDD-cost:   95
c ---[  14]---> BDD-cost:   95
c ---[  13]---> BDD-cost:   95
c ---[  12]---> BDD-cost:   95
c ---[  11]---> BDD-cost:   95
c ---[  10]---> BDD-cost:   95
c ---[   9]---> BDD-cost:   95
c ---[   8]---> BDD-cost:   95
c ---[   7]---> BDD-cost:   95
c ---[   6]---> BDD-cost:   95
c ---[   5]---> BDD-cost:   95
c ---[   4]---> BDD-cost:   95
c ---[   3]---> BDD-cost:   95
c ---[   2]---> BDD-cost:   95
c ---[   1]---> BDD-cost:   95
c ---[   0]---> BDD-cost:   95
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    8074    23340 |    2422       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2904          
c   -- var.elim.:  2000/2904          
c   -- var.elim.:  2904/2904          
c   -- var.elim.:  336/336          
c   -- subsuming                       
c   -- var.elim.:  216/216          
c   -- var.elim.:  264/264          
c   -- subsuming                       
c |         0 |    7930    22908 |      --       0       --      -- |     --   | -144/-144
c |         0 |    7930    22908 |    3172       0        0     nan |  0.000 % |
c |       101 |    7930    22908 |    3489     101     1580    15.6 |  4.564 % |
c |       251 |    7930    22908 |    3838     251     5753    22.9 |  4.564 % |
c |       478 |    7930    22908 |    4221     478    11975    25.1 |  4.564 % |
c |       817 |    7930    22908 |    4644     817    29803    36.5 |  4.564 % |
c |      1323 |    7930    22908 |    5108    1323    47907    36.2 |  4.564 % |
c |      2084 |    7930    22908 |    5619    2084    81212    39.0 |  4.564 % |
c |      3227 |    7930    22908 |    6181    3227   125840    39.0 |  4.564 % |
c |      4936 |    7930    22908 |    6799    4936   199647    40.4 |  4.564 % |
c ==============================================================================
c (current CPU-time: 2.03969 s)
c ==============================================================================
c [1mFound solution: 70[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:29320     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      6677 |   41811   101983 |   12543    6677   275535    41.3 |  4.564 % |
c   -- subsuming                       
c   -- var.elim.:  1000/22863          
c   -- var.elim.:  2000/22863          
c   -- var.elim.:  3000/22863          
c   -- var.elim.:  4000/22863          
c   -- var.elim.:  5000/22863          
c   -- var.elim.:  6000/22863          
c   -- var.elim.:  7000/22863          
c   -- var.elim.:  8000/22863          
c   -- var.elim.:  9000/22863          
c   -- var.elim.:  10000/22863          
c   -- var.elim.:  11000/22863          
c   -- var.elim.:  12000/22863          
c   -- var.elim.:  13000/22863          
c   -- var.elim.:  14000/22863          
c   -- var.elim.:  15000/22863          
c   -- var.elim.:  16000/22863          
c   -- var.elim.:  17000/22863          
c   -- var.elim.:  18000/22863          
c   -- var.elim.:  19000/22863          
c   -- var.elim.:  20000/22863          
c   -- var.elim.:  21000/22863          
c   -- var.elim.:  22000/22863          
c   -- var.elim.:  22863/22863          
c   -- var.elim.:  1000/11373          
c   -- var.elim.:  2000/11373          
c   -- var.elim.:  3000/11373          
c   -- var.elim.:  4000/11373          
c   -- var.elim.:  5000/11373          
c   -- var.elim.:  6000/11373          
c   -- var.elim.:  7000/11373          
c   -- var.elim.:  8000/11373          
c   -- var.elim.:  9000/11373          
c   -- var.elim.:  10000/11373          
c   -- var.elim.:  11000/11373          
c   -- var.elim.:  11373/11373          
c   -- var.elim.:  1000/3613          
c   -- var.elim.:  2000/3613          
c   -- var.elim.:  3000/3613          
c   -- var.elim.:  3613/3613          
c   -- var.elim.:  1000/5550          
c   -- var.elim.:  2000/5550          
c   -- var.elim.:  3000/5550          
c   -- var.elim.:  4000/5550          
c   -- var.elim.:  5000/5550          
c   -- var.elim.:  5550/5550          
c   -- var.elim.:  1000/4392          
c   -- var.elim.:  2000/4392          
c   -- var.elim.:  3000/4392          
c   -- var.elim.:  4000/4392          
c   -- var.elim.:  4392/4392          
c   -- var.elim.:  1000/1296          
c   -- var.elim.:  1296/1296          
c   -- subsuming                       
c   -- var.elim.:  1000/10076          
c   -- var.elim.:  2000/10076          
c   -- var.elim.:  3000/10076          
c   -- var.elim.:  4000/10076          
c   -- var.elim.:  5000/10076          
c   -- var.elim.:  6000/10076          
c   -- var.elim.:  7000/10076          
c   -- var.elim.:  8000/10076          
c   -- var.elim.:  9000/10076          
c   -- var.elim.:  10000/10076          
c   -- var.elim.:  10076/10076          
c   -- var.elim.:  1000/4794          
c   -- var.elim.:  2000/4794          
c   -- var.elim.:  3000/4794          
c   -- var.elim.:  4000/4794          
c   -- var.elim.:  4794/4794          
c   -- var.elim.:  1000/5925          
c   -- var.elim.:  2000/5925          
c   -- var.elim.:  3000/5925          
c   -- var.elim.:  4000/5925          
c   -- var.elim.:  5000/5925          
c   -- var.elim.:  5925/5925          
c   -- var.elim.:  1000/6295          
c   -- var.elim.:  2000/6295          
c   -- var.elim.:  3000/6295          
c   -- var.elim.:  4000/6295          
c   -- var.elim.:  5000/6295          
c   -- var.elim.:  6000/6295          
c   -- var.elim.:  6295/6295          
c   -- var.elim.:  1000/5102          
c   -- var.elim.:  2000/5102          
c   -- var.elim.:  3000/5102          
c   -- var.elim.:  4000/5102          
c   -- var.elim.:  5000/5102          
c   -- var.elim.:  5102/5102          
c   -- var.elim.:  1000/1604          
c   -- var.elim.:  1604/1604          
c   -- subsuming                       
c   -- var.elim.:  1000/6679          
c   -- var.elim.:  2000/6679          
c   -- var.elim.:  3000/6679          
c   -- var.elim.:  4000/6679          
c   -- var.elim.:  5000/6679          
c   -- var.elim.:  6000/6679          
c   -- var.elim.:  6679/6679          
c   -- var.elim.:  1000/5239          
c   -- var.elim.:  2000/5239          
c   -- var.elim.:  3000/5239          
c   -- var.elim.:  4000/5239          
c   -- var.elim.:  5000/5239          
c   -- var.elim.:  5239/5239          
c   -- var.elim.:  1000/4184          
c   -- var.elim.:  2000/4184          
c   -- var.elim.:  3000/4184          
c   -- var.elim.:  4000/4184          
c   -- var.elim.:  4184/4184          
c   -- var.elim.:  1000/4858          
c   -- var.elim.:  2000/4858          
c   -- var.elim.:  3000/4858          
c   -- var.elim.:  4000/4858          
c   -- var.elim.:  4858/4858          
c   -- var.elim.:  352/352          
c   -- subsuming                       
c   -- var.elim.:  1000/5261          
c   -- var.elim.:  2000/5261          
c   -- var.elim.:  3000/5261          
c   -- var.elim.:  4000/5261          
c   -- var.elim.:  5000/5261          
c   -- var.elim.:  5261/5261          
c   -- var.elim.:  1000/3761          
c   -- var.elim.:  2000/3761          
c   -- var.elim.:  3000/3761          
c   -- var.elim.:  3761/3761          
c |      6677 |   28934   179333 |      --    6677       --      -- |     --   | -12866/77383
c |      6677 |   28934   179333 |   11573    6677   275535    41.3 |  4.564 % |
c |      6782 |   28934   179333 |   12730    6782   279567    41.2 |  1.130 % |
c |      6932 |   28934   179333 |   14004    6932   284207    41.0 |  1.130 % |
c |      7157 |   28934   179333 |   15404    7157   291612    40.7 |  1.130 % |
c |      7496 |   28934   179333 |   16944    7496   302592    40.4 |  1.130 % |
c |      8002 |   28934   179333 |   18639    8002   319027    39.9 |  1.130 % |
c |      8761 |   28934   179333 |   20503    8761   345225    39.4 |  1.130 % |
c |      9900 |   28934   179333 |   22553    9900   382142    38.6 |  1.130 % |
c |     11609 |   28934   179333 |   24809   11609   453476    39.1 |  1.130 % |
c |     14171 |   28934   179333 |   27289   14171   546126    38.5 |  1.130 % |
c |     18016 |   28934   179333 |   30018   18016   693718    38.5 |  1.130 % |
c |     23783 |   28934   179333 |   33020   23783   914020    38.4 |  1.130 % |
c |     32435 |   28934   179333 |   36322   32435  1341492    41.4 |  1.130 % |
c |     45409 |   28934   179333 |   39955   21953   975127    44.4 |  1.130 % |
c |     64873 |   28934   179333 |   43950   15704   582114    37.1 |  1.130 % |
c ==============================================================================
c (current CPU-time: 231.522 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 |     81221 |   36343   199888 |   10902   32051  1541475    48.1 |  1.130 % |
c   -- subsuming                       
c   -- var.elim.:  1000/13603          
c   -- var.elim.:  2000/13603          
c   -- var.elim.:  3000/13603          
c   -- var.elim.:  4000/13603          
c   -- var.elim.:  5000/13603          
c   -- var.elim.:  6000/13603          
c   -- var.elim.:  7000/13603          
c   -- var.elim.:  8000/13603          
c   -- var.elim.:  9000/13603          
c   -- var.elim.:  10000/13603          
c   -- var.elim.:  11000/13603          
c   -- var.elim.:  12000/13603          
c   -- var.elim.:  13000/13603          
c   -- var.elim.:  13603/13603          
c   -- var.elim.:  1000/6559          
c   -- var.elim.:  2000/6559          
c   -- var.elim.:  3000/6559          
c   -- var.elim.:  4000/6559          
c   -- var.elim.:  5000/6559          
c   -- var.elim.:  6000/6559          
c   -- var.elim.:  6559/6559          
c   -- var.elim.:  1000/2522          
c   -- var.elim.:  2000/2522          
c   -- var.elim.:  2522/2522          
c   -- var.elim.:  1000/3971          
c   -- var.elim.:  2000/3971          
c   -- var.elim.:  3000/3971          
c   -- var.elim.:  3971/3971          
c   -- var.elim.:  1000/2710          
c   -- var.elim.:  2000/2710          
c   -- var.elim.:  2710/2710          
c   -- subsuming                       
c   -- var.elim.:  1000/5690          
c   -- var.elim.:  2000/5690          
c   -- var.elim.:  3000/5690          
c   -- var.elim.:  4000/5690          
c   -- var.elim.:  5000/5690          
c   -- var.elim.:  5690/5690          
c   -- var.elim.:  1000/3468          
c   -- var.elim.:  2000/3468          
c   -- var.elim.:  3000/3468          
c   -- var.elim.:  3468/3468          
c   -- var.elim.:  1000/4067          
c   -- var.elim.:  2000/4067          
c   -- var.elim.:  3000/4067          
c   -- var.elim.:  4000/4067          
c   -- var.elim.:  4067/4067          
c   -- var.elim.:  1000/3488          
c   -- var.elim.:  2000/3488          
c   -- var.elim.:  3000/3488          
c   -- var.elim.:  3488/3488          
c   -- var.elim.:  5/5          
c   -- subsuming                       
c   -- var.elim.:  1000/3575          
c   -- var.elim.:  2000/3575          
c   -- var.elim.:  3000/3575          
c   -- var.elim.:  3575/3575          
c   -- var.elim.:  1000/2304          
c   -- var.elim.:  2000/2304          
c   -- var.elim.:  2304/2304          
c   -- var.elim.:  1000/2294          
c   -- var.elim.:  2000/2294          
c   -- var.elim.:  2294/2294          
c   -- var.elim.:  210/210          
c |     81221 |   29131   182122 |      --   32051       --      -- |     --   | -7200/-17409
c |     81221 |   29131   182122 |   11652   32051  1541475    48.1 |  1.130 % |
c |     81324 |   29131   182122 |   12817    9605   464096    48.3 |  1.218 % |
c |     81474 |   29131   182122 |   14099    9755   470634    48.2 |  1.218 % |
c |     81702 |   29131   182122 |   15509    9983   480493    48.1 |  1.218 % |
c |     82040 |   29131   182122 |   17060   10321   495168    48.0 |  1.218 % |
c |     82548 |   29131   182122 |   18766   10829   519959    48.0 |  1.218 % |
c |     83307 |   29131   182122 |   20642   11588   558169    48.2 |  1.218 % |
c |     84450 |   29131   182122 |   22707   12731   619899    48.7 |  1.218 % |
c |     86159 |   29131   182122 |   24977   14440   695503    48.2 |  1.218 % |
c |     88722 |   29131   182122 |   27475   17003   820367    48.2 |  1.218 % |
c |     92566 |   29122   182029 |   30213   20845  1004766    48.2 |  1.249 % |
c |     98337 |   29122   182029 |   33235   26616  1281274    48.1 |  1.249 % |
c |    106994 |   29122   182029 |   36558   15591   640759    41.1 |  1.249 % |
c |    119969 |   29097   181845 |   40180   28565  1405231    49.2 |  1.342 % |
c ==============================================================================
c (current CPU-time: 358.751 s)
c ==============================================================================
c [1mFound solution: 64[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 |    123685 |   35744   200347 |   10723   32279  1591843    49.3 |  1.342 % |
c   -- subsuming                       
c   -- var.elim.:  1000/14174          
c   -- var.elim.:  2000/14174          
c   -- var.elim.:  3000/14174          
c   -- var.elim.:  4000/14174          
c   -- var.elim.:  5000/14174          
c   -- var.elim.:  6000/14174          
c   -- var.elim.:  7000/14174          
c   -- var.elim.:  8000/14174          
c   -- var.elim.:  9000/14174          
c   -- var.elim.:  10000/14174          
c   -- var.elim.:  11000/14174          
c   -- var.elim.:  12000/14174          
c   -- var.elim.:  13000/14174          
c   -- var.elim.:  14000/14174          
c   -- var.elim.:  14174/14174          
c   -- var.elim.:  1000/7371          
c   -- var.elim.:  2000/7371          
c   -- var.elim.:  3000/7371          
c   -- var.elim.:  4000/7371          
c   -- var.elim.:  5000/7371          
c   -- var.elim.:  6000/7371          
c   -- var.elim.:  7000/7371          
c   -- var.elim.:  7371/7371          
c   -- var.elim.:  1000/4885          
c   -- var.elim.:  2000/4885          
c   -- var.elim.:  3000/4885          
c   -- var.elim.:  4000/4885          
c   -- var.elim.:  4885/4885          
c   -- var.elim.:  1000/5267          
c   -- var.elim.:  2000/5267          
c   -- var.elim.:  3000/5267          
c   -- var.elim.:  4000/5267          
c   -- var.elim.:  5000/5267          
c   -- var.elim.:  5267/5267          
c   -- var.elim.:  1000/1916          
c   -- var.elim.:  1916/1916          
c   -- var.elim.:  63/63          
c   -- subsuming                       
c   -- var.elim.:  1000/4921          
c   -- var.elim.:  2000/4921          
c   -- var.elim.:  3000/4921          
c   -- var.elim.:  4000/4921          
c   -- var.elim.:  4921/4921          
c   -- var.elim.:  1000/2733          
c   -- var.elim.:  2000/2733          
c   -- var.elim.:  2733/2733          
c   -- var.elim.:  1000/2686          
c   -- var.elim.:  2000/2686          
c   -- var.elim.:  2686/2686          
c   -- var.elim.:  1000/2360          
c   -- var.elim.:  2000/2360          
c   -- var.elim.:  2360/2360          
c   -- var.elim.:  1000/1618          
c   -- var.elim.:  1618/1618          
c   -- var.elim.:  553/553          
c   -- var.elim.:  166/166          
c   -- subsuming                       
c   -- var.elim.:  133/133          
c |    123685 |   28546   174696 |      --   32279       --      -- |     --   | -6955/-17911
c |    123685 |   28546   174696 |   11418   32178  1574133    48.9 |  1.342 % |
c |    123788 |   28546   174696 |   12560    9906   407949    41.2 |  1.846 % |
c |    123940 |   28546   174696 |   13816   10058   414662    41.2 |  1.846 % |
c |    124165 |   28546   174696 |   15197   10283   422559    41.1 |  1.846 % |
c |    124505 |   28546   174696 |   16717   10623   437797    41.2 |  1.846 % |
c |    125012 |   28546   174696 |   18389   11130   457912    41.1 |  1.846 % |
c |    125771 |   28546   174696 |   20228   11889   502095    42.2 |  1.846 % |
c |    126910 |   28546   174696 |   22251   13028   561692    43.1 |  1.846 % |
c |    128618 |   28546   174696 |   24476   14736   651471    44.2 |  1.846 % |
c ==============================================================================
c (current CPU-time: 406.606 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 |    128699 |   36995   198523 |   11098   14817   655416    44.2 |  1.846 % |
c   -- subsuming                       
c   -- var.elim.:  1000/14083          
c   -- var.elim.:  2000/14083          
c   -- var.elim.:  3000/14083          
c   -- var.elim.:  4000/14083          
c   -- var.elim.:  5000/14083          
c   -- var.elim.:  6000/14083          
c   -- var.elim.:  7000/14083          
c   -- var.elim.:  8000/14083          
c   -- var.elim.:  9000/14083          
c   -- var.elim.:  10000/14083          
c   -- var.elim.:  11000/14083          
c   -- var.elim.:  12000/14083          
c   -- var.elim.:  13000/14083          
c   -- var.elim.:  14000/14083          
c   -- var.elim.:  14083/14083          
c   -- var.elim.:  1000/7022          
c   -- var.elim.:  2000/7022          
c   -- var.elim.:  3000/7022          
c   -- var.elim.:  4000/7022          
c   -- var.elim.:  5000/7022          
c   -- var.elim.:  6000/7022          
c   -- var.elim.:  7000/7022          
c   -- var.elim.:  7022/7022          
c   -- var.elim.:  1000/5507          
c   -- var.elim.:  2000/5507          
c   -- var.elim.:  3000/5507          
c   -- var.elim.:  4000/5507          
c   -- var.elim.:  5000/5507          
c   -- var.elim.:  5507/5507          
c   -- var.elim.:  1000/5381          
c   -- var.elim.:  2000/5381          
c   -- var.elim.:  3000/5381          
c   -- var.elim.:  4000/5381          
c   -- var.elim.:  5000/5381          
c   -- var.elim.:  5381/5381          
c   -- var.elim.:  1000/3333          
c   -- var.elim.:  2000/3333          
c   -- var.elim.:  3000/3333          
c   -- var.elim.:  3333/3333          
c   -- subsuming                       
c   -- var.elim.:  1000/5364          
c   -- var.elim.:  2000/5364          
c   -- var.elim.:  3000/5364          
c   -- var.elim.:  4000/5364          
c   -- var.elim.:  5000/5364          
c   -- var.elim.:  5364/5364          
c   -- var.elim.:  1000/3503          
c   -- var.elim.:  2000/3503          
c   -- var.elim.:  3000/3503          
c   -- var.elim.:  3503/3503          
c   -- var.elim.:  1000/3216          
c   -- var.elim.:  2000/3216          
c   -- var.elim.:  3000/3216          
c   -- var.elim.:  3216/3216          
c   -- var.elim.:  1000/3236          
c   -- var.elim.:  2000/3236          
c   -- var.elim.:  3000/3236          
c   -- var.elim.:  3236/3236          
c   -- var.elim.:  1000/2462          
c   -- var.elim.:  2000/2462          
c   -- var.elim.:  2462/2462          
c   -- subsuming                       
c   -- var.elim.:  1000/1984          
c   -- var.elim.:  1984/1984          
c   -- var.elim.:  1000/1729          
c   -- var.elim.:  1729/1729          
c   -- var.elim.:  1000/1692          
c   -- var.elim.:  1692/1692          
c   -- var.elim.:  64/64          
c |    128699 |   28667   176037 |      --   14817       --      -- |     --   | -8305/-22216
c |    128699 |   28667   176037 |   11466   14650   627412    42.8 |  1.846 % |
c |    128800 |   28667   176037 |   12613    9868   394970    40.0 |  1.912 % |
c |    128950 |   28667   176037 |   13874   10018   401484    40.1 |  1.912 % |
c |    129175 |   28667   176037 |   15262   10243   417912    40.8 |  1.912 % |
c |    129515 |   28667   176037 |   16788   10583   435696    41.2 |  1.912 % |
c |    130021 |   28630   175721 |   18443   11087   458573    41.4 |  2.054 % |
c |    130783 |   28604   175457 |   20269   11848   510479    43.1 |  2.157 % |
c |    131923 |   28571   175115 |   22270   12981   566080    43.6 |  2.275 % |
c |    133632 |   28083   152147 |   24079   14687   672310    45.8 |  3.057 % |
c |    136195 |   28083   152147 |   26487   17250   820015    47.5 |  3.057 % |
c |    140039 |   28006   151570 |   29056   21090  1027786    48.7 |  3.357 % |
c |    145806 |   27710   148781 |   31623   26838  1389311    51.8 |  4.274 % |
c |    154455 |   27393   146426 |   34388   18917   982981    52.0 |  5.474 % |
c ==============================================================================
c [1mOptimal solution: 62[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
c _______________________________________________________________________________
c 
c restarts              : 60
c conflicts             : 161109         (297 /sec)
c decisions             : 265820         (490 /sec)
c propagations          : 33080529       (60973 /sec)
c inspects              : 423229370      (780089 /sec)
c CPU time              : 542.54 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.84 0.94 0.90 2/55 27432
Raw data (stat): 27432 (runsolver) R 27431 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480300238 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.0006 s]
Raw data (loadavg): 0.87 0.94 0.90 2/55 27432
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 4193 0 0 0 985 14 0 0 25 0 1 0 480300238 19165184 4054 4294967295 134512640 134672761 3221224560 3221223008 134644014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4679 4054 603 41 0 4638 0
vsize: 18716
[startup+20.0007 s]
Raw data (loadavg): 0.89 0.94 0.90 2/55 27432
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 4260 0 0 0 1981 17 0 0 25 0 1 0 480300238 19378176 4121 4294967295 134512640 134672761 3221224560 3221223040 134541817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4731 4121 603 41 0 4690 0
vsize: 18924
[startup+30.0015 s]
Raw data (loadavg): 0.90 0.94 0.90 2/55 27432
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 4274 0 0 0 2981 17 0 0 25 0 1 0 480300238 19513344 4135 4294967295 134512640 134672761 3221224560 3221223008 134643542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4764 4135 603 41 0 4723 0
vsize: 19056
[startup+40.0011 s]
Raw data (loadavg): 0.92 0.94 0.90 2/55 27432
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 4417 0 0 0 3980 18 0 0 25 0 1 0 480300238 19988480 4257 4294967295 134512640 134672761 3221224560 3221222960 134605852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4880 4257 603 41 0 4839 0
vsize: 19520
[startup+50.0021 s]
Raw data (loadavg): 0.93 0.94 0.90 2/55 27432
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 4417 0 0 0 4980 18 0 0 25 0 1 0 480300238 19988480 4257 4294967295 134512640 134672761 3221224560 3221223104 134621035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4880 4257 603 41 0 4839 0
vsize: 19520
[startup+60.002 s]
Raw data (loadavg): 0.94 0.95 0.90 2/55 27432
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 4419 0 0 0 5976 22 0 0 25 0 1 0 480300238 19456000 4155 4294967295 134512640 134672761 3221224560 3221223008 134643548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4750 4155 603 41 0 4709 0
vsize: 19000
[startup+70.0014 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 27432
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 4423 0 0 0 6972 26 0 0 25 0 1 0 480300238 19591168 4159 4294967295 134512640 134672761 3221224560 3221223008 134643963 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4783 4159 603 41 0 4742 0
vsize: 19132
[startup+80.0026 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 27432
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 4531 0 0 0 7972 26 0 0 25 0 1 0 480300238 19992576 4259 4294967295 134512640 134672761 3221224560 3221222960 134604086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4881 4259 603 41 0 4840 0
vsize: 19524
[startup+90.0024 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 27432
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 4531 0 0 0 8970 27 0 0 25 0 1 0 480300238 19591168 4177 4294967295 134512640 134672761 3221224560 3221223008 134643474 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4783 4177 603 41 0 4742 0
vsize: 19132
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 27432
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 4534 0 0 0 9967 30 0 0 25 0 1 0 480300238 19591168 4180 4294967295 134512640 134672761 3221224560 3221223008 134643565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4783 4180 603 41 0 4742 0
vsize: 19132
[startup+110.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 27432
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 4543 0 0 0 10967 31 0 0 25 0 1 0 480300238 19591168 4189 4294967295 134512640 134672761 3221224560 3221223008 134643516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4783 4189 603 41 0 4742 0
vsize: 19132
[startup+120.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 27432
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 4543 0 0 0 11967 31 0 0 25 0 1 0 480300238 19591168 4189 4294967295 134512640 134672761 3221224560 3221223008 134643948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4783 4189 603 41 0 4742 0
vsize: 19132
[startup+130.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 27432
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 4680 0 0 0 12967 31 0 0 25 0 1 0 480300238 20201472 4298 4294967295 134512640 134672761 3221224560 3221223056 134606971 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4932 4298 603 41 0 4891 0
vsize: 19728
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 27434
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 4680 0 0 0 13967 31 0 0 25 0 1 0 480300238 20201472 4298 4294967295 134512640 134672761 3221224560 3221223104 134621242 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4932 4298 603 41 0 4891 0
vsize: 19728
[startup+150.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 27434
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 4680 0 0 0 14967 31 0 0 25 0 1 0 480300238 19595264 4190 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4784 4190 603 41 0 4743 0
vsize: 19136
[startup+160.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27434
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 5082 0 0 0 15967 32 0 0 25 0 1 0 480300238 21299200 4592 4294967295 134512640 134672761 3221224560 3221223712 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5200 4592 603 41 0 5159 0
vsize: 20800
[startup+170.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27434
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 5880 0 0 0 16965 34 0 0 25 0 1 0 480300238 24662016 5390 4294967295 134512640 134672761 3221224560 3221223744 134615752 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6021 5390 603 41 0 5980 0
vsize: 24084
[startup+180.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27434
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 6193 0 0 0 17964 34 0 0 25 0 1 0 480300238 25833472 5667 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6307 5667 603 41 0 6266 0
vsize: 25228
[startup+190.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27434
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 6209 0 0 0 18964 35 0 0 25 0 1 0 480300238 25997312 5683 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6347 5683 603 41 0 6306 0
vsize: 25388
[startup+200.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27434
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 6294 0 0 0 19964 35 0 0 25 0 1 0 480300238 26406912 5768 4294967295 134512640 134672761 3221224560 3221223744 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6447 5768 603 41 0 6406 0
vsize: 25788
[startup+210.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27434
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 6621 0 0 0 20963 36 0 0 25 0 1 0 480300238 27705344 6086 4294967295 134512640 134672761 3221224560 3221223712 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6764 6086 603 41 0 6723 0
vsize: 27056
[startup+220.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27434
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 6625 0 0 0 21963 36 0 0 25 0 1 0 480300238 27705344 6090 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6764 6090 603 41 0 6723 0
vsize: 27056
[startup+230.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27434
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 6626 0 0 0 22963 36 0 0 25 0 1 0 480300238 27705344 6091 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6764 6091 603 41 0 6723 0
vsize: 27056
[startup+240.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27434
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 7552 0 0 0 23954 45 0 0 25 0 1 0 480300238 29331456 6515 4294967295 134512640 134672761 3221224560 3221223008 134643516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7161 6515 603 41 0 7120 0
vsize: 28644
[startup+250.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27434
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 7552 0 0 0 24953 46 0 0 25 0 1 0 480300238 29331456 6515 4294967295 134512640 134672761 3221224560 3221223008 134643565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7161 6515 603 41 0 7120 0
vsize: 28644
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27434
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 7552 0 0 0 25953 46 0 0 25 0 1 0 480300238 29331456 6515 4294967295 134512640 134672761 3221224560 3221222384 134566484 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7161 6515 603 41 0 7120 0
vsize: 28644
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27434
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 7552 0 0 0 26952 47 0 0 25 0 1 0 480300238 29331456 6515 4294967295 134512640 134672761 3221224560 3221223008 134643959 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7161 6515 603 41 0 7120 0
vsize: 28644
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27434
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 7552 0 0 0 27951 48 0 0 25 0 1 0 480300238 29331456 6515 4294967295 134512640 134672761 3221224560 3221223008 134643961 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7161 6515 603 41 0 7120 0
vsize: 28644
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27434
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 7593 0 0 0 28951 49 0 0 25 0 1 0 480300238 29331456 6515 4294967295 134512640 134672761 3221224560 3221223008 134643542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7161 6515 603 41 0 7120 0
vsize: 28644
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27434
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 7593 0 0 0 29951 49 0 0 25 0 1 0 480300238 29331456 6515 4294967295 134512640 134672761 3221224560 3221223008 134644032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7161 6515 603 41 0 7120 0
vsize: 28644
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27434
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 7593 0 0 0 30951 49 0 0 25 0 1 0 480300238 29331456 6515 4294967295 134512640 134672761 3221224560 3221223744 134616014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7161 6515 603 41 0 7120 0
vsize: 28644
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27434
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 7593 0 0 0 31951 49 0 0 25 0 1 0 480300238 29331456 6515 4294967295 134512640 134672761 3221224560 3221223744 134615686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7161 6515 603 41 0 7120 0
vsize: 28644
[startup+330.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27434
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 7594 0 0 0 32951 49 0 0 25 0 1 0 480300238 29331456 6516 4294967295 134512640 134672761 3221224560 3221223744 134615632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7161 6516 603 41 0 7120 0
vsize: 28644
[startup+340.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27434
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 7594 0 0 0 33951 49 0 0 25 0 1 0 480300238 29331456 6516 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7161 6516 603 41 0 7120 0
vsize: 28644
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27434
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 7594 0 0 0 34951 49 0 0 25 0 1 0 480300238 29331456 6516 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7161 6516 603 41 0 7120 0
vsize: 28644
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27434
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 8606 0 0 0 35944 57 0 0 25 0 1 0 480300238 33411072 7026 4294967295 134512640 134672761 3221224560 3221223104 134621035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8157 7026 603 41 0 8116 0
vsize: 32628
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27434
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 8606 0 0 0 36940 60 0 0 25 0 1 0 480300238 33087488 6985 4294967295 134512640 134672761 3221224560 3221223008 134643959 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8078 6985 603 41 0 8037 0
vsize: 32312
[startup+380.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27434
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 8606 0 0 0 37939 61 0 0 25 0 1 0 480300238 33087488 6985 4294967295 134512640 134672761 3221224560 3221223008 134643548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8078 6985 603 41 0 8037 0
vsize: 32312
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27434
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 8688 0 0 0 38938 62 0 0 25 0 1 0 480300238 33087488 6985 4294967295 134512640 134672761 3221224560 3221223008 134643624 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8078 6985 603 41 0 8037 0
vsize: 32312
[startup+400.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27434
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 8688 0 0 0 39937 63 0 0 25 0 1 0 480300238 33087488 6985 4294967295 134512640 134672761 3221224560 3221223008 134643963 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8078 6985 603 41 0 8037 0
vsize: 32312
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27434
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 10056 0 0 0 40924 76 0 0 25 0 1 0 480300238 32841728 7044 4294967295 134512640 134672761 3221224560 3221223008 134643574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8018 7044 603 41 0 7977 0
vsize: 32072
[startup+420.01 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 27434
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 10056 0 0 0 41924 76 0 0 25 0 1 0 480300238 32841728 7044 4294967295 134512640 134672761 3221224560 3221223008 134643954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8018 7044 603 41 0 7977 0
vsize: 32072
[startup+430.011 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 27434
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 10056 0 0 0 42921 79 0 0 25 0 1 0 480300238 32841728 7044 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8018 7044 603 41 0 7977 0
vsize: 32072
[startup+440.011 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 27436
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 10056 0 0 0 43921 79 0 0 25 0 1 0 480300238 32841728 7044 4294967295 134512640 134672761 3221224560 3221223040 134541817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8018 7044 603 41 0 7977 0
vsize: 32072
[startup+450.012 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 27436
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 10156 0 0 0 44921 79 0 0 25 0 1 0 480300238 32645120 7029 4294967295 134512640 134672761 3221224560 3221222780 1075349746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7970 7029 603 41 0 7929 0
vsize: 31880
[startup+460.012 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 27436
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 10156 0 0 0 45920 80 0 0 25 0 1 0 480300238 32645120 7029 4294967295 134512640 134672761 3221224560 3221223008 134644008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7970 7029 603 41 0 7929 0
vsize: 31880
[startup+470.012 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 27436
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 10156 0 0 0 46920 80 0 0 25 0 1 0 480300238 32645120 7029 4294967295 134512640 134672761 3221224560 3221223008 134643545 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7970 7029 603 41 0 7929 0
vsize: 31880
[startup+480.013 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 27436
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 10266 0 0 0 47919 81 0 0 25 0 1 0 480300238 32645120 7029 4294967295 134512640 134672761 3221224560 3221223008 134643524 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7970 7029 603 41 0 7929 0
vsize: 31880
[startup+490.012 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 27436
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 10266 0 0 0 48919 81 0 0 25 0 1 0 480300238 32641024 7028 4294967295 134512640 134672761 3221224560 3221223744 134615767 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7969 7028 603 41 0 7928 0
vsize: 31876
[startup+500.014 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 27436
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 10268 0 0 0 49920 81 0 0 25 0 1 0 480300238 32641024 7030 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7969 7030 603 41 0 7928 0
vsize: 31876
[startup+510.013 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 27436
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 10270 0 0 0 50920 81 0 0 25 0 1 0 480300238 32641024 7032 4294967295 134512640 134672761 3221224560 3221223600 134612764 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7969 7032 603 41 0 7928 0
vsize: 31876
[startup+520.013 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 27436
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 10306 0 0 0 51920 82 0 0 25 0 1 0 480300238 32903168 7068 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8033 7068 603 41 0 7992 0
vsize: 32132
[startup+530.014 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 27436
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 10479 0 0 0 52919 82 0 0 25 0 1 0 480300238 33529856 7241 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8186 7241 603 41 0 8145 0
vsize: 32744
[startup+540.014 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 27436
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 10481 0 0 0 53919 83 0 0 25 0 1 0 480300238 33677312 7243 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8222 7243 603 41 0 8181 0
vsize: 32888
[startup+543.409 s]
Raw data (loadavg): 1.01 0.99 0.91 1/54 27436
Raw data (stat): 27432 (minisat+) R 27431 22929 22928 0 -1 0 10481 0 0 0 53919 83 0 0 25 0 1 0 480300238 33677312 7243 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8222 7243 603 41 0 8181 0
vsize: 0

Child status: 30
Real time (s): 543.409
CPU time (s): 543.419
CPU user time (s): 542.552
CPU system time (s): 0.867868
CPU usage (%): 100.002
Max. virtual memory (Kb): 32888
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	62
#### END VERIFIER DATA ####