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-7pb.opb
MD5SUM	24909033929a72aa74b2fd8b12f27bce
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	64
Optimality of the best value was proved	NO
Number of terms in the objective function	672
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	672
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	672
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.02884
Number of variables	672
Total number of constraints	2030
Number of constraints which are clauses	2006
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	28
Trace number 5525

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-04-14 00:35:17 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4003 boxname=wulflinc11 idbench=243 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  24909033929a72aa74b2fd8b12f27bce  /oldhome/oroussel/tmp/wulflinc11/normalized-s4-4-3-7pb.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc11/normalized-s4-4-3-7pb.opb /oldhome/oroussel/tmp/wulflinc11/normalized-s4-4-3-7pb.opb
IDLAUNCH: 4003
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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:        914344 kB
Buffers:         34980 kB
Cached:          61068 kB
SwapCached:       4932 kB
Active:          55912 kB
Inactive:        47920 kB
HighTotal:      131008 kB
HighFree:        66136 kB
LowTotal:       903652 kB
LowFree:        848208 kB
SwapTotal:     2097136 kB
SwapFree:      2092204 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10784 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:32 (client local time) WITH STATUS 30 IN 494.556 SECONDS
stats: 4003 0 494.556 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2030 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################################################################
c   -- Clauses(.)/Splits(s): ......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[2016]---> BDD-cost:    1
c ---[1991]---> BDD-cost:    1
c ---[1969]---> BDD-cost:    1
c ---[1959]---> BDD-cost:    1
c ---[1941]---> BDD-cost:    1
c ---[1919]---> BDD-cost:    1
c ---[1893]---> BDD-cost:    1
c ---[1887]---> BDD-cost:    1
c ---[1877]---> BDD-cost:    1
c ---[1867]---> BDD-cost:    1
c ---[1817]---> BDD-cost:    1
c ---[1815]---> BDD-cost:    1
c ---[1813]---> BDD-cost:    1
c ---[1787]---> BDD-cost:    1
c ---[1769]---> BDD-cost:    1
c ---[1743]---> BDD-cost:    1
c ---[1729]---> BDD-cost:    1
c ---[1703]---> BDD-cost:    1
c ---[1681]---> BDD-cost:    1
c ---[1671]---> BDD-cost:    1
c ---[1665]---> BDD-cost:    1
c ---[1647]---> BDD-cost:    1
c ---[1609]---> BDD-cost:    1
c ---[1599]---> BDD-cost:    1
c ---[1582]---> BDD-cost:    1
c ---[1560]---> BDD-cost:    1
c ---[1534]---> BDD-cost:    1
c ---[1528]---> BDD-cost:    1
c ---[1526]---> BDD-cost:    1
c ---[1500]---> BDD-cost:    1
c ---[1482]---> BDD-cost:    1
c ---[1456]---> BDD-cost:    1
c ---[1446]---> BDD-cost:    1
c ---[1436]---> BDD-cost:    1
c ---[1386]---> BDD-cost:    1
c ---[1384]---> BDD-cost:    1
c ---[1366]---> BDD-cost:    1
c ---[1344]---> BDD-cost:    1
c ---[1318]---> BDD-cost:    1
c ---[1312]---> BDD-cost:    1
c ---[1310]---> BDD-cost:    1
c ---[1284]---> BDD-cost:    1
c ---[1266]---> BDD-cost:    1
c ---[1240]---> BDD-cost:    1
c ---[1234]---> BDD-cost:    1
c ---[1216]---> BDD-cost:    1
c ---[1178]---> BDD-cost:    1
c ---[1168]---> BDD-cost:    1
c ---[1166]---> BDD-cost:    1
c ---[1140]---> BDD-cost:    1
c ---[1122]---> BDD-cost:    1
c ---[1096]---> BDD-cost:    1
c ---[1094]---> BDD-cost:    1
c ---[1068]---> BDD-cost:    1
c ---[1050]---> BDD-cost:    1
c ---[1024]---> BDD-cost:    1
c ---[1014]---> BDD-cost:    1
c ---[1004]---> BDD-cost:    1
c ---[ 954]---> BDD-cost:    1
c ---[ 952]---> BDD-cost:    1
c ---[ 934]---> BDD-cost:    1
c ---[ 912]---> BDD-cost:    1
c ---[ 886]---> BDD-cost:    1
c ---[ 880]---> BDD-cost:    1
c ---[ 870]---> BDD-cost:    1
c ---[ 860]---> BDD-cost:    1
c ---[ 811]---> BDD-cost:    1
c ---[ 809]---> BDD-cost:    1
c ---[ 799]---> BDD-cost:    1
c ---[ 789]---> BDD-cost:    1
c ---[ 739]---> BDD-cost:    1
c ---[ 737]---> BDD-cost:    1
c ---[ 684]---> BDD-cost:    1
c ---[ 674]---> BDD-cost:    1
c ---[ 668]---> BDD-cost:    1
c ---[ 666]---> BDD-cost:    1
c ---[ 617]---> BDD-cost:    1
c ---[ 607]---> BDD-cost:    1
c ---[ 597]---> BDD-cost:    1
c ---[ 595]---> BDD-cost:    1
c ---[ 542]---> BDD-cost:    1
c ---[ 532]---> 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 ---[ 435]---> BDD-cost:    1
c ---[ 413]---> BDD-cost:    1
c ---[ 387]---> BDD-cost:    1
c ---[ 381]---> BDD-cost:    1
c ---[ 332]---> BDD-cost:    1
c ---[ 322]---> 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 ---[ 224]---> BDD-cost:    1
c ---[ 198]---> BDD-cost:    1
c ---[ 176]---> BDD-cost:    1
c ---[ 166]---> BDD-cost:    1
c ---[ 114]---> BDD-cost:    1
c ---[ 104]---> BDD-cost:    1
c ---[  98]---> BDD-cost:    1
c ---[  96]---> BDD-cost:    1
c ---[  94]---> BDD-cost:    1
c ---[  68]---> BDD-cost:    1
c ---[  50]---> BDD-cost:    1
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:   99
c ---[  22]---> BDD-cost:   99
c ---[  21]---> BDD-cost:   99
c ---[  20]---> BDD-cost:   99
c ---[  19]---> BDD-cost:   99
c ---[  18]---> BDD-cost:   99
c ---[  17]---> BDD-cost:   99
c ---[  16]---> BDD-cost:   99
c ---[  15]---> BDD-cost:   99
c ---[  14]---> BDD-cost:   99
c ---[  13]---> BDD-cost:   99
c ---[  12]---> BDD-cost:   99
c ---[  11]---> BDD-cost:   99
c ---[  10]---> BDD-cost:   99
c ---[   9]---> BDD-cost:   99
c ---[   8]---> BDD-cost:   99
c ---[   7]---> BDD-cost:   99
c ---[   6]---> BDD-cost:   99
c ---[   5]---> BDD-cost:   99
c ---[   4]---> BDD-cost:   99
c ---[   3]---> BDD-cost:   99
c ---[   2]---> BDD-cost:   99
c ---[   1]---> BDD-cost:   99
c ---[   0]---> BDD-cost:   99
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    8414    24352 |    2524       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3024          
c   -- var.elim.:  2000/3024          
c   -- var.elim.:  3000/3024          
c   -- var.elim.:  3024/3024          
c   -- var.elim.:  336/336          
c   -- subsuming                       
c   -- var.elim.:  216/216          
c   -- var.elim.:  264/264          
c   -- subsuming                       
c |         0 |    8270    23912 |      --       0       --      -- |     --   | -144/-144
c |         0 |    8270    23912 |    3308       0        0     nan |  0.000 % |
c |       101 |    8270    23912 |    3638     101     1474    14.6 |  4.509 % |
c |       252 |    8270    23912 |    4002     252     8385    33.3 |  4.509 % |
c |       477 |    8270    23912 |    4402     477    19184    40.2 |  4.509 % |
c |       814 |    8270    23912 |    4843     814    28885    35.5 |  4.509 % |
c |      1320 |    8270    23912 |    5327    1320    42094    31.9 |  4.509 % |
c |      2084 |    8270    23912 |    5860    2084    75882    36.4 |  4.509 % |
c |      3225 |    8270    23912 |    6446    3225   115068    35.7 |  4.509 % |
c |      4937 |    8270    23912 |    7090    4937   201976    40.9 |  4.509 % |
c |      7501 |    8270    23912 |    7800    5038   197982    39.3 |  4.509 % |
c |     11353 |    8270    23912 |    8580    6076   274799    45.2 |  4.509 % |
c |     17120 |    8252    23856 |    9417    5955   301554    50.6 |  4.675 % |
c |     25772 |    8232    23793 |   10334    7497   317155    42.3 |  4.741 % |
c |     38746 |    8232    23793 |   11367    9841   491302    49.9 |  4.741 % |
c |     58207 |    8232    23793 |   12504    9916   392898    39.6 |  4.741 % |
c ==============================================================================
c (current CPU-time: 38.6291 s)
c ==============================================================================
c [1mFound solution: 72[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:30394     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     75644 |   43433   105904 |   13029   10313   382721    37.1 |  4.741 % |
c   -- subsuming                       
c   -- var.elim.:  1000/23751          
c   -- var.elim.:  2000/23751          
c   -- var.elim.:  3000/23751          
c   -- var.elim.:  4000/23751          
c   -- var.elim.:  5000/23751          
c   -- var.elim.:  6000/23751          
c   -- var.elim.:  7000/23751          
c   -- var.elim.:  8000/23751          
c   -- var.elim.:  9000/23751          
c   -- var.elim.:  10000/23751          
c   -- var.elim.:  11000/23751          
c   -- var.elim.:  12000/23751          
c   -- var.elim.:  13000/23751          
c   -- var.elim.:  14000/23751          
c   -- var.elim.:  15000/23751          
c   -- var.elim.:  16000/23751          
c   -- var.elim.:  17000/23751          
c   -- var.elim.:  18000/23751          
c   -- var.elim.:  19000/23751          
c   -- var.elim.:  20000/23751          
c   -- var.elim.:  21000/23751          
c   -- var.elim.:  22000/23751          
c   -- var.elim.:  23000/23751          
c   -- var.elim.:  23751/23751          
c   -- var.elim.:  1000/11819          
c   -- var.elim.:  2000/11819          
c   -- var.elim.:  3000/11819          
c   -- var.elim.:  4000/11819          
c   -- var.elim.:  5000/11819          
c   -- var.elim.:  6000/11819          
c   -- var.elim.:  7000/11819          
c   -- var.elim.:  8000/11819          
c   -- var.elim.:  9000/11819          
c   -- var.elim.:  10000/11819          
c   -- var.elim.:  11000/11819          
c   -- var.elim.:  11819/11819          
c   -- var.elim.:  1000/3692          
c   -- var.elim.:  2000/3692          
c   -- var.elim.:  3000/3692          
c   -- var.elim.:  3692/3692          
c   -- var.elim.:  1000/5608          
c   -- var.elim.:  2000/5608          
c   -- var.elim.:  3000/5608          
c   -- var.elim.:  4000/5608          
c   -- var.elim.:  5000/5608          
c   -- var.elim.:  5608/5608          
c   -- var.elim.:  1000/5863          
c   -- var.elim.:  2000/5863          
c   -- var.elim.:  3000/5863          
c   -- var.elim.:  4000/5863          
c   -- var.elim.:  5000/5863          
c   -- var.elim.:  5863/5863          
c   -- var.elim.:  1000/1847          
c   -- var.elim.:  1847/1847          
c   -- subsuming                       
c   -- var.elim.:  1000/10425          
c   -- var.elim.:  2000/10425          
c   -- var.elim.:  3000/10425          
c   -- var.elim.:  4000/10425          
c   -- var.elim.:  5000/10425          
c   -- var.elim.:  6000/10425          
c   -- var.elim.:  7000/10425          
c   -- var.elim.:  8000/10425          
c   -- var.elim.:  9000/10425          
c   -- var.elim.:  10000/10425          
c   -- var.elim.:  10425/10425          
c   -- var.elim.:  1000/5213          
c   -- var.elim.:  2000/5213          
c   -- var.elim.:  3000/5213          
c   -- var.elim.:  4000/5213          
c   -- var.elim.:  5000/5213          
c   -- var.elim.:  5213/5213          
c   -- var.elim.:  1000/5846          
c   -- var.elim.:  2000/5846          
c   -- var.elim.:  3000/5846          
c   -- var.elim.:  4000/5846          
c   -- var.elim.:  5000/5846          
c   -- var.elim.:  5846/5846          
c   -- var.elim.:  1000/5876          
c   -- var.elim.:  2000/5876          
c   -- var.elim.:  3000/5876          
c   -- var.elim.:  4000/5876          
c   -- var.elim.:  5000/5876          
c   -- var.elim.:  5876/5876          
c   -- var.elim.:  1000/3661          
c   -- var.elim.:  2000/3661          
c   -- var.elim.:  3000/3661          
c   -- var.elim.:  3661/3661          
c   -- var.elim.:  15/15          
c   -- subsuming                       
c   -- var.elim.:  1000/6692          
c   -- var.elim.:  2000/6692          
c   -- var.elim.:  3000/6692          
c   -- var.elim.:  4000/6692          
c   -- var.elim.:  5000/6692          
c   -- var.elim.:  6000/6692          
c   -- var.elim.:  6692/6692          
c   -- var.elim.:  1000/4987          
c   -- var.elim.:  2000/4987          
c   -- var.elim.:  3000/4987          
c   -- var.elim.:  4000/4987          
c   -- var.elim.:  4987/4987          
c   -- var.elim.:  1000/3703          
c   -- var.elim.:  2000/3703          
c   -- var.elim.:  3000/3703          
c   -- var.elim.:  3703/3703          
c   -- var.elim.:  1000/1531          
c   -- var.elim.:  1531/1531          
c   -- subsuming                       
c   -- var.elim.:  1000/5105          
c   -- var.elim.:  2000/5105          
c   -- var.elim.:  3000/5105          
c   -- var.elim.:  4000/5105          
c   -- var.elim.:  5000/5105          
c   -- var.elim.:  5105/5105          
c   -- var.elim.:  1000/1297          
c   -- var.elim.:  1297/1297          
c   -- var.elim.:  878/878          
c |     75644 |   30290   186670 |      --   10313       --      -- |     --   | -13087/80927
c |     75644 |   30290   186670 |   12116   10302   382380    37.1 |  4.741 % |
c |     75746 |   30290   186670 |   13327   10404   384412    36.9 |  1.441 % |
c |     75897 |   30290   186670 |   14660   10555   390088    37.0 |  1.441 % |
c |     76123 |   30290   186670 |   16126   10781   396725    36.8 |  1.441 % |
c |     76464 |   30290   186670 |   17739   11122   406713    36.6 |  1.441 % |
c |     76970 |   30290   186670 |   19512   11628   427285    36.7 |  1.441 % |
c |     77730 |   30290   186670 |   21464   12388   456738    36.9 |  1.441 % |
c |     78870 |   30290   186670 |   23610   13528   511248    37.8 |  1.441 % |
c |     80581 |   30290   186670 |   25971   15239   580144    38.1 |  1.441 % |
c |     83144 |   30290   186670 |   28568   17802   691141    38.8 |  1.441 % |
c |     86988 |   30290   186670 |   31425   21646   880200    40.7 |  1.441 % |
c |     92757 |   30290   186670 |   34568   27415  1150613    42.0 |  1.441 % |
c |    101406 |   30290   186670 |   38025   14529   625261    43.0 |  1.441 % |
c |    114381 |   30256   186169 |   41780   27502  1301663    47.3 |  1.546 % |
c |    133842 |   30256   186169 |   45958   18285  1004105    54.9 |  1.546 % |
c ==============================================================================
c (current CPU-time: 218.531 s)
c ==============================================================================
c [1mFound solution: 70[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 |    138185 |   37008   205278 |   11102   22628  1269682    56.1 |  1.546 % |
c   -- subsuming                       
c   -- var.elim.:  1000/13189          
c   -- var.elim.:  2000/13189          
c   -- var.elim.:  3000/13189          
c   -- var.elim.:  4000/13189          
c   -- var.elim.:  5000/13189          
c   -- var.elim.:  6000/13189          
c   -- var.elim.:  7000/13189          
c   -- var.elim.:  8000/13189          
c   -- var.elim.:  9000/13189          
c   -- var.elim.:  10000/13189          
c   -- var.elim.:  11000/13189          
c   -- var.elim.:  12000/13189          
c   -- var.elim.:  13000/13189          
c   -- var.elim.:  13189/13189          
c   -- var.elim.:  1000/5831          
c   -- var.elim.:  2000/5831          
c   -- var.elim.:  3000/5831          
c   -- var.elim.:  4000/5831          
c   -- var.elim.:  5000/5831          
c   -- var.elim.:  5831/5831          
c   -- var.elim.:  1000/3388          
c   -- var.elim.:  2000/3388          
c   -- var.elim.:  3000/3388          
c   -- var.elim.:  3388/3388          
c   -- var.elim.:  1000/3561          
c   -- var.elim.:  2000/3561          
c   -- var.elim.:  3000/3561          
c   -- var.elim.:  3561/3561          
c   -- var.elim.:  279/279          
c   -- var.elim.:  160/160          
c   -- subsuming                       
c   -- var.elim.:  1000/5118          
c   -- var.elim.:  2000/5118          
c   -- var.elim.:  3000/5118          
c   -- var.elim.:  4000/5118          
c   -- var.elim.:  5000/5118          
c   -- var.elim.:  5118/5118          
c   -- var.elim.:  1000/2879          
c   -- var.elim.:  2000/2879          
c   -- var.elim.:  2879/2879          
c   -- var.elim.:  1000/3623          
c   -- var.elim.:  2000/3623          
c   -- var.elim.:  3000/3623          
c   -- var.elim.:  3623/3623          
c   -- var.elim.:  1000/3110          
c   -- var.elim.:  2000/3110          
c   -- var.elim.:  3000/3110          
c   -- var.elim.:  3110/3110          
c   -- var.elim.:  846/846          
c   -- subsuming                       
c   -- var.elim.:  1000/2544          
c   -- var.elim.:  2000/2544          
c   -- var.elim.:  2544/2544          
c   -- var.elim.:  1000/3201          
c   -- var.elim.:  2000/3201          
c   -- var.elim.:  3000/3201          
c   -- var.elim.:  3201/3201          
c   -- var.elim.:  1000/1621          
c   -- var.elim.:  1621/1621          
c   -- var.elim.:  432/432          
c |    138185 |   30396   190599 |      --   22628       --      -- |     --   | -6601/-14444
c |    138185 |   30396   190599 |   12158   22628  1269682    56.1 |  1.546 % |
c |    138286 |   30396   190599 |   13374    9767   495949    50.8 |  1.571 % |
c |    138437 |   30396   190599 |   14711    9918   502003    50.6 |  1.571 % |
c |    138663 |   30396   190599 |   16182   10144   511290    50.4 |  1.571 % |
c |    139002 |   30396   190599 |   17801   10483   525260    50.1 |  1.571 % |
c |    139508 |   30396   190599 |   19581   10989   547896    49.9 |  1.571 % |
c |    140268 |   30396   190599 |   21539   11749   578909    49.3 |  1.571 % |
c |    141410 |   30396   190599 |   23693   12891   650724    50.5 |  1.571 % |
c |    143118 |   30396   190599 |   26062   14599   731718    50.1 |  1.571 % |
c |    145682 |   30396   190599 |   28668   17163   861277    50.2 |  1.571 % |
c |    149528 |   30396   190599 |   31535   21009  1003880    47.8 |  1.571 % |
c |    155294 |   30371   190364 |   34660   26774  1332362    49.8 |  1.660 % |
c |    163946 |   30371   190364 |   38126   15364   722712    47.0 |  1.660 % |
c |    176920 |   30284   189625 |   41819   28334  1380648    48.7 |  1.980 % |
c |    196382 |   29384   179948 |   44634   19048   819876    43.0 |  4.824 % |
c ==============================================================================
c (current CPU-time: 371.229 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 |    207031 |   36077   198708 |   10823   29695  1333783    44.9 |  4.824 % |
c   -- subsuming                       
c   -- var.elim.:  1000/15191          
c   -- var.elim.:  2000/15191          
c   -- var.elim.:  3000/15191          
c   -- var.elim.:  4000/15191          
c   -- var.elim.:  5000/15191          
c   -- var.elim.:  6000/15191          
c   -- var.elim.:  7000/15191          
c   -- var.elim.:  8000/15191          
c   -- var.elim.:  9000/15191          
c   -- var.elim.:  10000/15191          
c   -- var.elim.:  11000/15191          
c   -- var.elim.:  12000/15191          
c   -- var.elim.:  13000/15191          
c   -- var.elim.:  14000/15191          
c   -- var.elim.:  15000/15191          
c   -- var.elim.:  15191/15191          
c   -- var.elim.:  1000/6910          
c   -- var.elim.:  2000/6910          
c   -- var.elim.:  3000/6910          
c   -- var.elim.:  4000/6910          
c   -- var.elim.:  5000/6910          
c   -- var.elim.:  6000/6910          
c   -- var.elim.:  6910/6910          
c   -- var.elim.:  1000/4566          
c   -- var.elim.:  2000/4566          
c   -- var.elim.:  3000/4566          
c   -- var.elim.:  4000/4566          
c   -- var.elim.:  4566/4566          
c   -- var.elim.:  1000/4442          
c   -- var.elim.:  2000/4442          
c   -- var.elim.:  3000/4442          
c   -- var.elim.:  4000/4442          
c   -- var.elim.:  4442/4442          
c   -- var.elim.:  1000/3416          
c   -- var.elim.:  2000/3416          
c   -- var.elim.:  3000/3416          
c   -- var.elim.:  3416/3416          
c   -- var.elim.:  1000/2563          
c   -- var.elim.:  2000/2563          
c   -- var.elim.:  2563/2563          
c   -- var.elim.:  1000/2108          
c   -- var.elim.:  2000/2108          
c   -- var.elim.:  2108/2108          
c   -- var.elim.:  862/862          
c   -- var.elim.:  66/66          
c   -- subsuming                       
c   -- var.elim.:  212/212          
c   -- var.elim.:  15/15          
c |    207031 |   29192   179277 |      --   29695       --      -- |     --   | -6878/-19385
c |    207031 |   29192   179277 |   11676   29690  1332906    44.9 |  4.824 % |
c |    207135 |   29192   179277 |   12844   10032   390945    39.0 |  5.281 % |
c |    207285 |   29192   179277 |   14128   10182   396996    39.0 |  5.281 % |
c |    207511 |   29192   179277 |   15541   10408   406658    39.1 |  5.281 % |
c |    207848 |   29192   179277 |   17096   10745   420368    39.1 |  5.281 % |
c |    208355 |   29192   179277 |   18805   11252   441272    39.2 |  5.281 % |
c |    209116 |   29192   179277 |   20686   12013   473895    39.4 |  5.281 % |
c |    210256 |   29192   179277 |   22754   13153   529507    40.3 |  5.281 % |
c |    211964 |   29192   179277 |   25030   14861   605198    40.7 |  5.281 % |
c |    214527 |   29192   179277 |   27533   17424   717927    41.2 |  5.281 % |
c ==============================================================================
c (current CPU-time: 413.264 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 |    215805 |   36565   200071 |   10969   18702   778317    41.6 |  5.281 % |
c   -- subsuming                       
c   -- var.elim.:  1000/13465          
c   -- var.elim.:  2000/13465          
c   -- var.elim.:  3000/13465          
c   -- var.elim.:  4000/13465          
c   -- var.elim.:  5000/13465          
c   -- var.elim.:  6000/13465          
c   -- var.elim.:  7000/13465          
c   -- var.elim.:  8000/13465          
c   -- var.elim.:  9000/13465          
c   -- var.elim.:  10000/13465          
c   -- var.elim.:  11000/13465          
c   -- var.elim.:  12000/13465          
c   -- var.elim.:  13000/13465          
c   -- var.elim.:  13465/13465          
c   -- var.elim.:  1000/7890          
c   -- var.elim.:  2000/7890          
c   -- var.elim.:  3000/7890          
c   -- var.elim.:  4000/7890          
c   -- var.elim.:  5000/7890          
c   -- var.elim.:  6000/7890          
c   -- var.elim.:  7000/7890          
c   -- var.elim.:  7890/7890          
c   -- var.elim.:  1000/4732          
c   -- var.elim.:  2000/4732          
c   -- var.elim.:  3000/4732          
c   -- var.elim.:  4000/4732          
c   -- var.elim.:  4732/4732          
c   -- var.elim.:  1000/4604          
c   -- var.elim.:  2000/4604          
c   -- var.elim.:  3000/4604          
c   -- var.elim.:  4000/4604          
c   -- var.elim.:  4604/4604          
c   -- var.elim.:  1000/2175          
c   -- var.elim.:  2000/2175          
c   -- var.elim.:  2175/2175          
c   -- var.elim.:  52/52          
c   -- subsuming                       
c   -- var.elim.:  1000/5871          
c   -- var.elim.:  2000/5871          
c   -- var.elim.:  3000/5871          
c   -- var.elim.:  4000/5871          
c   -- var.elim.:  5000/5871          
c   -- var.elim.:  5871/5871          
c   -- var.elim.:  1000/3584          
c   -- var.elim.:  2000/3584          
c   -- var.elim.:  3000/3584          
c   -- var.elim.:  3584/3584          
c   -- var.elim.:  1000/3605          
c   -- var.elim.:  2000/3605          
c   -- var.elim.:  3000/3605          
c   -- var.elim.:  3605/3605          
c   -- var.elim.:  1000/3017          
c   -- var.elim.:  2000/3017          
c   -- var.elim.:  3000/3017          
c   -- var.elim.:  3017/3017          
c   -- var.elim.:  6/6          
c   -- subsuming                       
c   -- var.elim.:  1000/2906          
c   -- var.elim.:  2000/2906          
c   -- var.elim.:  2906/2906          
c   -- var.elim.:  1000/1206          
c   -- var.elim.:  1206/1206          
c   -- var.elim.:  1000/1120          
c   -- var.elim.:  1120/1120          
c   -- var.elim.:  392/392          
c   -- var.elim.:  171/171          
c |    215805 |   29164   174108 |      --   18702       --      -- |     --   | -7227/-14633
c |    215805 |   29164   174108 |   11665   18685   776335    41.5 |  5.281 % |
c |    215905 |   29164   174108 |   12832    8405   310717    37.0 |  5.532 % |
c |    216057 |   29164   174108 |   14115    8557   316272    37.0 |  5.532 % |
c |    216282 |   29164   174108 |   15526    8782   324576    37.0 |  5.532 % |
c |    216622 |   29164   174108 |   17079    9122   336653    36.9 |  5.532 % |
c |    217129 |   29164   174108 |   18787    9629   354786    36.8 |  5.532 % |
c |    217888 |   29164   174108 |   20666   10388   385497    37.1 |  5.532 % |
c |    219027 |   29164   174108 |   22732   11527   431982    37.5 |  5.532 % |
c |    220738 |   29060   173251 |   24917   13233   514705    38.9 |  5.884 % |
c |    223300 |   29060   173251 |   27408   15795   627643    39.7 |  5.884 % |
c |    227146 |   29060   173251 |   30149   19641   793241    40.4 |  5.884 % |
c |    232914 |   28998   172730 |   33093   25408  1042333    41.0 |  6.079 % |
c ==============================================================================
c [1mOptimal solution: 64[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
c _______________________________________________________________________________
c 
c restarts              : 67
c conflicts             : 237032         (480 /sec)
c decisions             : 364739         (739 /sec)
c propagations          : 34504100       (69876 /sec)
c inspects              : 549242718      (1112291 /sec)
c CPU time              : 493.794 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 5858
Raw data (stat): 5858 (runsolver) R 5857 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422089823 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0011 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 1458 0 0 0 995 3 0 0 25 0 1 0 422089823 7614464 1435 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1859 1435 603 41 0 1818 0
vsize: 7436
[startup+20.0023 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 1672 0 0 0 1994 4 0 0 25 0 1 0 422089823 8482816 1649 4294967295 134512640 134672761 3221224560 3221223600 134612653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2071 1649 603 41 0 2030 0
vsize: 8284
[startup+30.0027 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 1708 0 0 0 2993 4 0 0 25 0 1 0 422089823 8564736 1685 4294967295 134512640 134672761 3221224560 3221223600 134612978 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2091 1685 603 41 0 2050 0
vsize: 8364
[startup+40.0034 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 4726 0 0 0 3983 13 0 0 25 0 1 0 422089823 21655552 4513 4294967295 134512640 134672761 3221224560 3221222976 134541828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5287 4513 603 41 0 5246 0
vsize: 21148
[startup+50.0046 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 4843 0 0 0 4980 16 0 0 25 0 1 0 422089823 22192128 4630 4294967295 134512640 134672761 3221224560 3221223040 134541817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5418 4630 603 41 0 5377 0
vsize: 21672
[startup+60.0051 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 4910 0 0 0 5977 19 0 0 25 0 1 0 422089823 22466560 4697 4294967295 134512640 134672761 3221224560 3221223008 134643516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5485 4697 603 41 0 5444 0
vsize: 21940
[startup+70.0056 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 5052 0 0 0 6977 19 0 0 25 0 1 0 422089823 22966272 4816 4294967295 134512640 134672761 3221224560 3221223024 134644235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5607 4816 603 41 0 5566 0
vsize: 22428
[startup+80.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 5052 0 0 0 7976 20 0 0 25 0 1 0 422089823 22966272 4816 4294967295 134512640 134672761 3221224560 3221222952 1075352943 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5607 4816 603 41 0 5566 0
vsize: 22428
[startup+90.0065 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 5052 0 0 0 8974 21 0 0 25 0 1 0 422089823 22499328 4726 4294967295 134512640 134672761 3221224560 3221223008 134643524 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5493 4726 603 41 0 5452 0
vsize: 21972
[startup+100.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 5052 0 0 0 9971 24 0 0 25 0 1 0 422089823 22499328 4726 4294967295 134512640 134672761 3221224560 3221223008 134643987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5493 4726 603 41 0 5452 0
vsize: 21972
[startup+110.007 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 5138 0 0 0 10971 24 0 0 25 0 1 0 422089823 23027712 4806 4294967295 134512640 134672761 3221224560 3221223272 134643316 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5622 4806 603 41 0 5581 0
vsize: 22488
[startup+120.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 5138 0 0 0 11970 24 0 0 25 0 1 0 422089823 23027712 4806 4294967295 134512640 134672761 3221224560 3221223104 134621186 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5622 4806 603 41 0 5581 0
vsize: 22488
[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 5138 0 0 0 12969 25 0 0 25 0 1 0 422089823 22499328 4726 4294967295 134512640 134672761 3221224560 3221223008 134643577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5493 4726 603 41 0 5452 0
vsize: 21972
[startup+140.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 5268 0 0 0 13969 26 0 0 25 0 1 0 422089823 23076864 4825 4294967295 134512640 134672761 3221224560 3221223104 134621086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5634 4825 603 41 0 5593 0
vsize: 22536
[startup+150.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 5365 0 0 0 14969 26 0 0 25 0 1 0 422089823 22892544 4823 4294967295 134512640 134672761 3221224560 3221223600 134612835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5589 4823 603 41 0 5548 0
vsize: 22356
[startup+160.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 5973 0 0 0 15967 29 0 0 25 0 1 0 422089823 25571328 5431 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6243 5431 603 41 0 6202 0
vsize: 24972
[startup+170.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 6453 0 0 0 16965 30 0 0 25 0 1 0 422089823 27582464 5911 4294967295 134512640 134672761 3221224560 3221223824 134618040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6734 5911 603 41 0 6693 0
vsize: 26936
[startup+180.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 6594 0 0 0 17965 31 0 0 25 0 1 0 422089823 28344320 6052 4294967295 134512640 134672761 3221224560 3221223600 134612739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6920 6052 603 41 0 6879 0
vsize: 27680
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 6627 0 0 0 18965 31 0 0 25 0 1 0 422089823 28344320 6085 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6920 6085 603 41 0 6879 0
vsize: 27680
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 6888 0 0 0 19965 31 0 0 25 0 1 0 422089823 29458432 6346 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7192 6346 603 41 0 7151 0
vsize: 28768
[startup+210.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 7367 0 0 0 20964 32 0 0 25 0 1 0 422089823 31424512 6825 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7672 6825 603 41 0 7631 0
vsize: 30688
[startup+220.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 8320 0 0 0 21958 38 0 0 25 0 1 0 422089823 32518144 7239 4294967295 134512640 134672761 3221224560 3221223104 134621336 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7939 7239 603 41 0 7898 0
vsize: 31756
[startup+230.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 8320 0 0 0 22954 41 0 0 25 0 1 0 422089823 32518144 7239 4294967295 134512640 134672761 3221224560 3221223040 134541821 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7939 7239 603 41 0 7898 0
vsize: 31756
[startup+240.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 8320 0 0 0 23952 44 0 0 25 0 1 0 422089823 32518144 7239 4294967295 134512640 134672761 3221224560 3221222896 134603506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7939 7239 603 41 0 7898 0
vsize: 31756
[startup+250.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 8320 0 0 0 24950 45 0 0 25 0 1 0 422089823 32518144 7239 4294967295 134512640 134672761 3221224560 3221223008 134643542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7939 7239 603 41 0 7898 0
vsize: 31756
[startup+260.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 8362 0 0 0 25949 46 0 0 25 0 1 0 422089823 32825344 7281 4294967295 134512640 134672761 3221224560 3221223024 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8014 7281 603 41 0 7973 0
vsize: 32056
[startup+270.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 8363 0 0 0 26948 46 0 0 25 0 1 0 422089823 32518144 7239 4294967295 134512640 134672761 3221224560 3221223040 134541816 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7939 7239 603 41 0 7898 0
vsize: 31756
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 8366 0 0 0 27948 46 0 0 25 0 1 0 422089823 32518144 7242 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7939 7242 603 41 0 7898 0
vsize: 31756
[startup+290.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 8366 0 0 0 28948 46 0 0 25 0 1 0 422089823 32518144 7242 4294967295 134512640 134672761 3221224560 3221223744 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7939 7242 603 41 0 7898 0
vsize: 31756
[startup+300.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 8366 0 0 0 29949 46 0 0 25 0 1 0 422089823 32518144 7242 4294967295 134512640 134672761 3221224560 3221223744 134615794 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7939 7242 603 41 0 7898 0
vsize: 31756
[startup+310.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 8366 0 0 0 30949 47 0 0 25 0 1 0 422089823 32518144 7242 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7939 7242 603 41 0 7898 0
vsize: 31756
[startup+320.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 8366 0 0 0 31949 47 0 0 25 0 1 0 422089823 32518144 7242 4294967295 134512640 134672761 3221224560 3221223744 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7939 7242 603 41 0 7898 0
vsize: 31756
[startup+330.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 8368 0 0 0 32949 47 0 0 25 0 1 0 422089823 32518144 7244 4294967295 134512640 134672761 3221224560 3221223600 134614205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7939 7244 603 41 0 7898 0
vsize: 31756
[startup+340.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 8368 0 0 0 33949 47 0 0 25 0 1 0 422089823 32518144 7244 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7939 7244 603 41 0 7898 0
vsize: 31756
[startup+350.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 8368 0 0 0 34950 47 0 0 25 0 1 0 422089823 32518144 7244 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7939 7244 603 41 0 7898 0
vsize: 31756
[startup+360.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 8412 0 0 0 35950 47 0 0 25 0 1 0 422089823 32518144 7245 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7939 7245 603 41 0 7898 0
vsize: 31756
[startup+370.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 8412 0 0 0 36950 47 0 0 25 0 1 0 422089823 32518144 7245 4294967295 134512640 134672761 3221224560 3221223744 134615926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7939 7245 603 41 0 7898 0
vsize: 31756
[startup+380.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 9399 0 0 0 37940 56 0 0 25 0 1 0 422089823 36179968 7724 4294967295 134512640 134672761 3221224560 3221223008 134643511 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8833 7724 603 41 0 8792 0
vsize: 35332
[startup+390.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 9399 0 0 0 38940 57 0 0 25 0 1 0 422089823 36179968 7724 4294967295 134512640 134672761 3221224560 3221223040 134541816 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8833 7724 603 41 0 8792 0
vsize: 35332
[startup+400.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 9399 0 0 0 39939 58 0 0 25 0 1 0 422089823 36179968 7724 4294967295 134512640 134672761 3221224560 3221223008 134643542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8833 7724 603 41 0 8792 0
vsize: 35332
[startup+410.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 9443 0 0 0 40939 58 0 0 25 0 1 0 422089823 36179968 7725 4294967295 134512640 134672761 3221224560 3221223744 134615660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8833 7725 603 41 0 8792 0
vsize: 35332
[startup+420.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 10715 0 0 0 41929 68 0 0 25 0 1 0 422089823 36245504 7846 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8849 7846 603 41 0 8808 0
vsize: 35396
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 10715 0 0 0 42928 69 0 0 25 0 1 0 422089823 36245504 7846 4294967295 134512640 134672761 3221224560 3221222832 1075349701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8849 7846 603 41 0 8808 0
vsize: 35396
[startup+440.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 10801 0 0 0 43928 69 0 0 25 0 1 0 422089823 36917248 7932 4294967295 134512640 134672761 3221224560 3221223104 134621211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9013 7932 603 41 0 8972 0
vsize: 36052
[startup+450.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 10801 0 0 0 44926 71 0 0 25 0 1 0 422089823 36245504 7846 4294967295 134512640 134672761 3221224560 3221223008 134643612 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8849 7846 603 41 0 8808 0
vsize: 35396
[startup+460.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 10844 0 0 0 45925 71 0 0 25 0 1 0 422089823 36569088 7889 4294967295 134512640 134672761 3221224560 3221223024 134644235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8928 7889 603 41 0 8887 0
vsize: 35712
[startup+470.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 10844 0 0 0 46925 72 0 0 25 0 1 0 422089823 36245504 7846 4294967295 134512640 134672761 3221224560 3221223684 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8849 7846 603 41 0 8808 0
vsize: 35396
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 10844 0 0 0 47925 72 0 0 25 0 1 0 422089823 36245504 7846 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8849 7846 603 41 0 8808 0
vsize: 35396
[startup+490.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 10844 0 0 0 48925 72 0 0 25 0 1 0 422089823 36245504 7846 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8849 7846 603 41 0 8808 0
vsize: 35396
[startup+494.596 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 5858
Raw data (stat): 5858 (minisat+) R 5857 32461 32460 0 -1 0 10844 0 0 0 48925 72 0 0 25 0 1 0 422089823 36245504 7846 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8849 7846 603 41 0 8808 0
vsize: 0

Child status: 30
Real time (s): 494.596
CPU time (s): 494.556
CPU user time (s): 493.803
CPU system time (s): 0.752885
CPU usage (%): 99.9919
Max. virtual memory (Kb): 36052
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	64
#### END VERIFIER DATA ####