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-6pb.opb
MD5SUM	c12951e903009dc00793ce72594cf3ba
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	66
Optimality of the best value was proved	NO
Number of terms in the objective function	624
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	624
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	624
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.03684
Number of variables	624
Total number of constraints	1884
Number of constraints which are clauses	1860
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	26
Trace number 5518

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-04-14 00:34:51 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4002 boxname=wulflinc12 idbench=242 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c12951e903009dc00793ce72594cf3ba  /oldhome/oroussel/tmp/wulflinc12/normalized-s4-4-3-6pb.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc12/normalized-s4-4-3-6pb.opb /oldhome/oroussel/tmp/wulflinc12/normalized-s4-4-3-6pb.opb
IDLAUNCH: 4002
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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.091
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:        915060 kB
Buffers:         35124 kB
Cached:          65296 kB
SwapCached:         16 kB
Active:          61016 kB
Inactive:        42244 kB
HighTotal:      131008 kB
HighFree:        61796 kB
LowTotal:       903652 kB
LowFree:        853264 kB
SwapTotal:     2097136 kB
SwapFree:      2097120 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            10720 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:40:20 (client local time) WITH STATUS 30 IN 329.049 SECONDS
stats: 4002 0 329.049 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1884 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################################################################################
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[1882]---> BDD-cost:    1
c ---[1856]---> BDD-cost:    1
c ---[1838]---> BDD-cost:    1
c ---[1812]---> BDD-cost:    1
c ---[1798]---> BDD-cost:    1
c ---[1772]---> 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 ---[1666]---> BDD-cost:    1
c ---[1640]---> BDD-cost:    1
c ---[1622]---> BDD-cost:    1
c ---[1596]---> BDD-cost:    1
c ---[1578]---> BDD-cost:    1
c ---[1556]---> BDD-cost:    1
c ---[1530]---> BDD-cost:    1
c ---[1524]---> BDD-cost:    1
c ---[1514]---> BDD-cost:    1
c ---[1504]---> BDD-cost:    1
c ---[1454]---> BDD-cost:    1
c ---[1452]---> BDD-cost:    1
c ---[1450]---> BDD-cost:    1
c ---[1424]---> BDD-cost:    1
c ---[1407]---> BDD-cost:    1
c ---[1381]---> BDD-cost:    1
c ---[1363]---> BDD-cost:    1
c ---[1342]---> BDD-cost:    1
c ---[1316]---> BDD-cost:    1
c ---[1310]---> BDD-cost:    1
c ---[1300]---> BDD-cost:    1
c ---[1290]---> BDD-cost:    1
c ---[1240]---> BDD-cost:    1
c ---[1238]---> BDD-cost:    1
c ---[1189]---> BDD-cost:    1
c ---[1179]---> BDD-cost:    1
c ---[1169]---> BDD-cost:    1
c ---[1167]---> BDD-cost:    1
c ---[1165]---> BDD-cost:    1
c ---[1139]---> BDD-cost:    1
c ---[1121]---> BDD-cost:    1
c ---[1095]---> BDD-cost:    1
c ---[1093]---> BDD-cost:    1
c ---[1067]---> BDD-cost:    1
c ---[1049]---> BDD-cost:    1
c ---[1023]---> BDD-cost:    1
c ---[1009]---> BDD-cost:    1
c ---[ 983]---> BDD-cost:    1
c ---[ 961]---> BDD-cost:    1
c ---[ 951]---> BDD-cost:    1
c ---[ 933]---> BDD-cost:    1
c ---[ 911]---> BDD-cost:    1
c ---[ 885]---> BDD-cost:    1
c ---[ 879]---> BDD-cost:    1
c ---[ 877]---> BDD-cost:    1
c ---[ 851]---> BDD-cost:    1
c ---[ 833]---> BDD-cost:    1
c ---[ 807]---> BDD-cost:    1
c ---[ 789]---> BDD-cost:    1
c ---[ 767]---> BDD-cost:    1
c ---[ 741]---> BDD-cost:    1
c ---[ 735]---> BDD-cost:    1
c ---[ 733]---> BDD-cost:    1
c ---[ 707]---> BDD-cost:    1
c ---[ 689]---> BDD-cost:    1
c ---[ 663]---> BDD-cost:    1
c ---[ 657]---> BDD-cost:    1
c ---[ 639]---> BDD-cost:    1
c ---[ 601]---> BDD-cost:    1
c ---[ 591]---> BDD-cost:    1
c ---[ 585]---> BDD-cost:    1
c ---[ 567]---> BDD-cost:    1
c ---[ 529]---> BDD-cost:    1
c ---[ 519]---> BDD-cost:    1
c ---[ 483]---> BDD-cost:    1
c ---[ 461]---> BDD-cost:    1
c ---[ 455]---> BDD-cost:    1
c ---[ 449]---> BDD-cost:    1
c ---[ 397]---> BDD-cost:    1
c ---[ 387]---> BDD-cost:    1
c ---[ 381]---> BDD-cost:    1
c ---[ 379]---> BDD-cost:    1
c ---[ 373]---> BDD-cost:    1
c ---[ 355]---> BDD-cost:    1
c ---[ 318]---> BDD-cost:    1
c ---[ 308]---> BDD-cost:    1
c ---[ 298]---> BDD-cost:    1
c ---[ 289]---> BDD-cost:    1
c ---[ 239]---> BDD-cost:    1
c ---[ 237]---> BDD-cost:    1
c ---[ 188]---> BDD-cost:    1
c ---[ 178]---> BDD-cost:    1
c ---[ 168]---> BDD-cost:    1
c ---[ 166]---> BDD-cost:    1
c ---[ 117]---> BDD-cost:    1
c ---[ 107]---> BDD-cost:    1
c ---[  97]---> BDD-cost:    1
c ---[  95]---> BDD-cost:    1
c ---[  46]---> BDD-cost:    1
c ---[  36]---> BDD-cost:    1
c ---[  26]---> BDD-cost:    1
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:   91
c ---[  22]---> BDD-cost:   91
c ---[  21]---> BDD-cost:   91
c ---[  20]---> BDD-cost:   91
c ---[  19]---> BDD-cost:   91
c ---[  18]---> BDD-cost:   91
c ---[  17]---> BDD-cost:   91
c ---[  16]---> BDD-cost:   91
c ---[  15]---> BDD-cost:   91
c ---[  14]---> BDD-cost:   91
c ---[  13]---> BDD-cost:   91
c ---[  12]---> BDD-cost:   91
c ---[  11]---> BDD-cost:   91
c ---[  10]---> BDD-cost:   91
c ---[   9]---> BDD-cost:   91
c ---[   8]---> BDD-cost:   91
c ---[   7]---> BDD-cost:   91
c ---[   6]---> BDD-cost:   91
c ---[   5]---> BDD-cost:   91
c ---[   4]---> BDD-cost:   91
c ---[   3]---> BDD-cost:   91
c ---[   2]---> BDD-cost:   91
c ---[   1]---> BDD-cost:   91
c ---[   0]---> BDD-cost:   91
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    7740    22400 |    2321       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2784          
c   -- var.elim.:  2000/2784          
c   -- var.elim.:  2784/2784          
c   -- var.elim.:  336/336          
c   -- subsuming                       
c   -- var.elim.:  216/216          
c   -- var.elim.:  264/264          
c   -- subsuming                       
c |         0 |    7596    21976 |      --       0       --      -- |     --   | -144/-144
c |         0 |    7596    21976 |    3038       0        0     nan |  0.000 % |
c |       100 |    7596    21976 |    3342     100     1484    14.8 |  4.625 % |
c |       250 |    7596    21976 |    3676     250     4803    19.2 |  4.624 % |
c |       475 |    7596    21976 |    4044     475    11008    23.2 |  4.624 % |
c |       812 |    7596    21976 |    4448     812    22947    28.3 |  4.624 % |
c |      1319 |    7596    21976 |    4893    1319    41402    31.4 |  4.624 % |
c |      2080 |    7596    21976 |    5382    2080    69637    33.5 |  4.624 % |
c |      3220 |    7596    21976 |    5920    3220   106910    33.2 |  4.624 % |
c |      4928 |    7596    21976 |    6513    4928   209715    42.6 |  4.624 % |
c |      7491 |    7596    21976 |    7164    5170   245425    47.5 |  4.624 % |
c ==============================================================================
c (current CPU-time: 3.3135 s)
c ==============================================================================
c [1mFound solution: 70[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:28228     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     10221 |   40195    98072 |   12058    5381   263800    49.0 |  4.624 % |
c   -- subsuming                       
c   -- var.elim.:  1000/22002          
c   -- var.elim.:  2000/22002          
c   -- var.elim.:  3000/22002          
c   -- var.elim.:  4000/22002          
c   -- var.elim.:  5000/22002          
c   -- var.elim.:  6000/22002          
c   -- var.elim.:  7000/22002          
c   -- var.elim.:  8000/22002          
c   -- var.elim.:  9000/22002          
c   -- var.elim.:  10000/22002          
c   -- var.elim.:  11000/22002          
c   -- var.elim.:  12000/22002          
c   -- var.elim.:  13000/22002          
c   -- var.elim.:  14000/22002          
c   -- var.elim.:  15000/22002          
c   -- var.elim.:  16000/22002          
c   -- var.elim.:  17000/22002          
c   -- var.elim.:  18000/22002          
c   -- var.elim.:  19000/22002          
c   -- var.elim.:  20000/22002          
c   -- var.elim.:  21000/22002          
c   -- var.elim.:  22000/22002          
c   -- var.elim.:  22002/22002          
c   -- var.elim.:  1000/10955          
c   -- var.elim.:  2000/10955          
c   -- var.elim.:  3000/10955          
c   -- var.elim.:  4000/10955          
c   -- var.elim.:  5000/10955          
c   -- var.elim.:  6000/10955          
c   -- var.elim.:  7000/10955          
c   -- var.elim.:  8000/10955          
c   -- var.elim.:  9000/10955          
c   -- var.elim.:  10000/10955          
c   -- var.elim.:  10955/10955          
c   -- var.elim.:  1000/3773          
c   -- var.elim.:  2000/3773          
c   -- var.elim.:  3000/3773          
c   -- var.elim.:  3773/3773          
c   -- var.elim.:  1000/4971          
c   -- var.elim.:  2000/4971          
c   -- var.elim.:  3000/4971          
c   -- var.elim.:  4000/4971          
c   -- var.elim.:  4971/4971          
c   -- var.elim.:  1000/6146          
c   -- var.elim.:  2000/6146          
c   -- var.elim.:  3000/6146          
c   -- var.elim.:  4000/6146          
c   -- var.elim.:  5000/6146          
c   -- var.elim.:  6000/6146          
c   -- var.elim.:  6146/6146          
c   -- subsuming                       
c   -- var.elim.:  1000/9597          
c   -- var.elim.:  2000/9597          
c   -- var.elim.:  3000/9597          
c   -- var.elim.:  4000/9597          
c   -- var.elim.:  5000/9597          
c   -- var.elim.:  6000/9597          
c   -- var.elim.:  7000/9597          
c   -- var.elim.:  8000/9597          
c   -- var.elim.:  9000/9597          
c   -- var.elim.:  9597/9597          
c   -- var.elim.:  1000/4629          
c   -- var.elim.:  2000/4629          
c   -- var.elim.:  3000/4629          
c   -- var.elim.:  4000/4629          
c   -- var.elim.:  4629/4629          
c   -- var.elim.:  1000/5192          
c   -- var.elim.:  2000/5192          
c   -- var.elim.:  3000/5192          
c   -- var.elim.:  4000/5192          
c   -- var.elim.:  5000/5192          
c   -- var.elim.:  5192/5192          
c   -- var.elim.:  1000/6383          
c   -- var.elim.:  2000/6383          
c   -- var.elim.:  3000/6383          
c   -- var.elim.:  4000/6383          
c   -- var.elim.:  5000/6383          
c   -- var.elim.:  6000/6383          
c   -- var.elim.:  6383/6383          
c   -- var.elim.:  1000/5220          
c   -- var.elim.:  2000/5220          
c   -- var.elim.:  3000/5220          
c   -- var.elim.:  4000/5220          
c   -- var.elim.:  5000/5220          
c   -- var.elim.:  5220/5220          
c   -- var.elim.:  1000/1166          
c   -- var.elim.:  1166/1166          
c   -- subsuming                       
c   -- var.elim.:  1000/6824          
c   -- var.elim.:  2000/6824          
c   -- var.elim.:  3000/6824          
c   -- var.elim.:  4000/6824          
c   -- var.elim.:  5000/6824          
c   -- var.elim.:  6000/6824          
c   -- var.elim.:  6824/6824          
c   -- var.elim.:  1000/4342          
c   -- var.elim.:  2000/4342          
c   -- var.elim.:  3000/4342          
c   -- var.elim.:  4000/4342          
c   -- var.elim.:  4342/4342          
c   -- var.elim.:  1000/3516          
c   -- var.elim.:  2000/3516          
c   -- var.elim.:  3000/3516          
c   -- var.elim.:  3516/3516          
c   -- var.elim.:  1000/3103          
c   -- var.elim.:  2000/3103          
c   -- var.elim.:  3000/3103          
c   -- var.elim.:  3103/3103          
c   -- var.elim.:  1000/1801          
c   -- var.elim.:  1801/1801          
c   -- subsuming                       
c   -- var.elim.:  1000/4455          
c   -- var.elim.:  2000/4455          
c   -- var.elim.:  3000/4455          
c   -- var.elim.:  4000/4455          
c   -- var.elim.:  4455/4455          
c   -- var.elim.:  1000/2509          
c   -- var.elim.:  2000/2509          
c   -- var.elim.:  2509/2509          
c |     10221 |   28123   177816 |      --    5381       --      -- |     --   | -12061/79777
c |     10221 |   28123   177816 |   11249    5381   263800    49.0 |  4.624 % |
c |     10322 |   28123   177816 |   12374    5482   268013    48.9 |  1.126 % |
c |     10474 |   28123   177816 |   13611    5634   274120    48.7 |  1.126 % |
c |     10701 |   28123   177816 |   14972    5861   281716    48.1 |  1.126 % |
c |     11040 |   28123   177816 |   16469    6200   292548    47.2 |  1.126 % |
c |     11546 |   28123   177816 |   18116    6706   308712    46.0 |  1.126 % |
c |     12308 |   28123   177816 |   19928    7468   333447    44.7 |  1.126 % |
c |     13447 |   28123   177816 |   21921    8607   364085    42.3 |  1.126 % |
c |     15156 |   28123   177816 |   24113   10316   405504    39.3 |  1.126 % |
c |     17718 |   28123   177816 |   26525   12878   484465    37.6 |  1.126 % |
c |     21562 |   28123   177816 |   29177   16722   608774    36.4 |  1.126 % |
c |     27330 |   28091   177639 |   32058   22486   776836    34.5 |  1.215 % |
c |     35979 |   28091   177639 |   35264   31135  1118157    35.9 |  1.215 % |
c |     48953 |   28009   176949 |   38677   20552   895904    43.6 |  1.448 % |
c ==============================================================================
c (current CPU-time: 160.551 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 |     58129 |   34489   195422 |   10346   29725  1309379    44.0 |  1.448 % |
c   -- subsuming                       
c   -- var.elim.:  1000/12886          
c   -- var.elim.:  2000/12886          
c   -- var.elim.:  3000/12886          
c   -- var.elim.:  4000/12886          
c   -- var.elim.:  5000/12886          
c   -- var.elim.:  6000/12886          
c   -- var.elim.:  7000/12886          
c   -- var.elim.:  8000/12886          
c   -- var.elim.:  9000/12886          
c   -- var.elim.:  10000/12886          
c   -- var.elim.:  11000/12886          
c   -- var.elim.:  12000/12886          
c   -- var.elim.:  12886/12886          
c   -- var.elim.:  1000/6031          
c   -- var.elim.:  2000/6031          
c   -- var.elim.:  3000/6031          
c   -- var.elim.:  4000/6031          
c   -- var.elim.:  5000/6031          
c   -- var.elim.:  6000/6031          
c   -- var.elim.:  6031/6031          
c   -- var.elim.:  1000/2228          
c   -- var.elim.:  2000/2228          
c   -- var.elim.:  2228/2228          
c   -- var.elim.:  1000/3379          
c   -- var.elim.:  2000/3379          
c   -- var.elim.:  3000/3379          
c   -- var.elim.:  3379/3379          
c   -- var.elim.:  1000/2533          
c   -- var.elim.:  2000/2533          
c   -- var.elim.:  2533/2533          
c   -- subsuming                       
c   -- var.elim.:  1000/5378          
c   -- var.elim.:  2000/5378          
c   -- var.elim.:  3000/5378          
c   -- var.elim.:  4000/5378          
c   -- var.elim.:  5000/5378          
c   -- var.elim.:  5378/5378          
c   -- var.elim.:  1000/3586          
c   -- var.elim.:  2000/3586          
c   -- var.elim.:  3000/3586          
c   -- var.elim.:  3586/3586          
c   -- var.elim.:  1000/3627          
c   -- var.elim.:  2000/3627          
c   -- var.elim.:  3000/3627          
c   -- var.elim.:  3627/3627          
c   -- var.elim.:  1000/2668          
c   -- var.elim.:  2000/2668          
c   -- var.elim.:  2668/2668          
c   -- var.elim.:  427/427          
c   -- subsuming                       
c   -- var.elim.:  1000/3465          
c   -- var.elim.:  2000/3465          
c   -- var.elim.:  3000/3465          
c   -- var.elim.:  3465/3465          
c   -- var.elim.:  1000/3559          
c   -- var.elim.:  2000/3559          
c   -- var.elim.:  3000/3559          
c   -- var.elim.:  3559/3559          
c   -- var.elim.:  1000/2351          
c   -- var.elim.:  2000/2351          
c   -- var.elim.:  2351/2351          
c   -- var.elim.:  1000/2078          
c   -- var.elim.:  2000/2078          
c   -- var.elim.:  2078/2078          
c   -- subsuming                       
c   -- var.elim.:  1000/3100          
c   -- var.elim.:  2000/3100          
c   -- var.elim.:  3000/3100          
c   -- var.elim.:  3100/3100          
c |     58129 |   28155   178089 |      --   29725       --      -- |     --   | -6322/-17089
c |     58129 |   28155   178089 |   11262   29571  1302583    44.0 |  1.448 % |
c |     58229 |   28151   178075 |   12386    8458   322861    38.2 |  1.500 % |
c |     58380 |   28111   176850 |   13605    8608   326789    38.0 |  1.524 % |
c |     58607 |   28111   176850 |   14966    8835   333169    37.7 |  1.524 % |
c |     58944 |   28111   176850 |   16462    9172   344605    37.6 |  1.524 % |
c |     59450 |   28111   176850 |   18109    9678   360782    37.3 |  1.524 % |
c |     60209 |   28111   176850 |   19920   10437   386962    37.1 |  1.524 % |
c |     61351 |   28111   176850 |   21912   11579   427354    36.9 |  1.524 % |
c |     63059 |   28111   176850 |   24103   13287   481487    36.2 |  1.524 % |
c |     65622 |   28111   176850 |   26513   15850   558187    35.2 |  1.524 % |
c |     69470 |   28111   176850 |   29165   19698   715581    36.3 |  1.524 % |
c |     75236 |   28083   176715 |   32049   25452   938236    36.9 |  1.540 % |
c |     83887 |   28021   176169 |   35176   16165   535155    33.1 |  1.644 % |
c |     96861 |   27842   174884 |   38447   29129  1136219    39.0 |  2.229 % |
c |    116324 |   27165   165485 |   41263   24702  1065389    43.1 |  4.290 % |
c ==============================================================================
c [1mOptimal solution: 66[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
c _______________________________________________________________________________
c 
c restarts              : 39
c conflicts             : 121663         (370 /sec)
c decisions             : 208380         (634 /sec)
c propagations          : 19460564       (59228 /sec)
c inspects              : 223712384      (680865 /sec)
c CPU time              : 328.571 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/54 29691
Raw data (stat): 29691 (runsolver) R 29690 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422086387 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 29691
Raw data (stat): 29691 (minisat+) R 29690 25285 25284 0 -1 0 4177 0 0 0 982 15 0 0 25 0 1 0 422086387 18771968 3967 4294967295 134512640 134672761 3221224560 3221223008 134643636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4583 3967 603 41 0 4542 0
vsize: 18332
[startup+20.001 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 29691
Raw data (stat): 29691 (minisat+) R 29690 25285 25284 0 -1 0 4245 0 0 0 1980 18 0 0 25 0 1 0 422086387 19017728 4035 4294967295 134512640 134672761 3221224560 3221223008 134643959 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4643 4035 603 41 0 4602 0
vsize: 18572
[startup+30.0015 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 29691
Raw data (stat): 29691 (minisat+) R 29690 25285 25284 0 -1 0 4258 0 0 0 2980 18 0 0 25 0 1 0 422086387 19017728 4048 4294967295 134512640 134672761 3221224560 3221223008 134643516 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4643 4048 603 41 0 4602 0
vsize: 18572
[startup+40.0017 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 29691
Raw data (stat): 29691 (minisat+) R 29690 25285 25284 0 -1 0 4390 0 0 0 3980 18 0 0 25 0 1 0 422086387 19595264 4156 4294967295 134512640 134672761 3221224560 3221222272 134566484 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4784 4156 603 41 0 4743 0
vsize: 19136
[startup+50.0025 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 29691
Raw data (stat): 29691 (minisat+) R 29690 25285 25284 0 -1 0 4407 0 0 0 4980 18 0 0 25 0 1 0 422086387 19857408 4173 4294967295 134512640 134672761 3221224560 3221223104 134621211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4848 4173 603 41 0 4807 0
vsize: 19392
[startup+60.0021 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 29691
Raw data (stat): 29691 (minisat+) R 29690 25285 25284 0 -1 0 4408 0 0 0 5977 22 0 0 25 0 1 0 422086387 19128320 4077 4294967295 134512640 134672761 3221224560 3221223008 134643499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4670 4077 603 41 0 4629 0
vsize: 18680
[startup+70.0032 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 29691
Raw data (stat): 29691 (minisat+) R 29690 25285 25284 0 -1 0 4408 0 0 0 6974 25 0 0 25 0 1 0 422086387 19128320 4077 4294967295 134512640 134672761 3221224560 3221223008 134643499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4670 4077 603 41 0 4629 0
vsize: 18680
[startup+80.0041 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 29691
Raw data (stat): 29691 (minisat+) R 29690 25285 25284 0 -1 0 4488 0 0 0 7974 25 0 0 25 0 1 0 422086387 19591168 4157 4294967295 134512640 134672761 3221224560 3221223104 134621211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4783 4157 603 41 0 4742 0
vsize: 19132
[startup+90.0036 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 29691
Raw data (stat): 29691 (minisat+) R 29690 25285 25284 0 -1 0 4488 0 0 0 8974 25 0 0 25 0 1 0 422086387 19128320 4077 4294967295 134512640 134672761 3221224560 3221223008 134643577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4670 4077 603 41 0 4629 0
vsize: 18680
[startup+100.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 29691
Raw data (stat): 29691 (minisat+) R 29690 25285 25284 0 -1 0 4488 0 0 0 9974 26 0 0 25 0 1 0 422086387 19128320 4077 4294967295 134512640 134672761 3221224560 3221223008 134643996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4670 4077 603 41 0 4629 0
vsize: 18680
[startup+110.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 29691
Raw data (stat): 29691 (minisat+) R 29690 25285 25284 0 -1 0 4488 0 0 0 10973 26 0 0 25 0 1 0 422086387 19128320 4077 4294967295 134512640 134672761 3221224560 3221223008 134643542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4670 4077 603 41 0 4629 0
vsize: 18680
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29691
Raw data (stat): 29691 (minisat+) R 29690 25285 25284 0 -1 0 4576 0 0 0 11973 26 0 0 25 0 1 0 422086387 19582976 4165 4294967295 134512640 134672761 3221224560 3221223104 134621216 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4781 4165 603 41 0 4740 0
vsize: 19124
[startup+130.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29691
Raw data (stat): 29691 (minisat+) R 29690 25285 25284 0 -1 0 4576 0 0 0 12973 26 0 0 25 0 1 0 422086387 19140608 4080 4294967295 134512640 134672761 3221224560 3221223008 134643471 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4673 4080 603 41 0 4632 0
vsize: 18692
[startup+140.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29691
Raw data (stat): 29691 (minisat+) R 29690 25285 25284 0 -1 0 5130 0 0 0 13972 28 0 0 25 0 1 0 422086387 21557248 4634 4294967295 134512640 134672761 3221224560 3221223744 134616017 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5263 4634 603 41 0 5222 0
vsize: 21052
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29691
Raw data (stat): 29691 (minisat+) R 29690 25285 25284 0 -1 0 5866 0 0 0 14971 29 0 0 25 0 1 0 422086387 24485888 5334 4294967295 134512640 134672761 3221224560 3221223372 1075349993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5978 5334 603 41 0 5937 0
vsize: 23912
[startup+160.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29691
Raw data (stat): 29691 (minisat+) R 29690 25285 25284 0 -1 0 5891 0 0 0 15971 29 0 0 25 0 1 0 422086387 24649728 5359 4294967295 134512640 134672761 3221224560 3221223484 1075346551 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6018 5359 603 41 0 5977 0
vsize: 24072
[startup+170.008 s]
Raw data (loadavg): 1.07 0.97 0.91 2/54 29691
Raw data (stat): 29691 (minisat+) R 29690 25285 25284 0 -1 0 7064 0 0 0 16963 37 0 0 25 0 1 0 422086387 25784320 5747 4294967295 134512640 134672761 3221224560 3221223008 134644032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6295 5747 603 41 0 6254 0
vsize: 25180
[startup+180.008 s]
Raw data (loadavg): 1.06 0.97 0.91 2/54 29691
Raw data (stat): 29691 (minisat+) R 29690 25285 25284 0 -1 0 7064 0 0 0 17961 38 0 0 25 0 1 0 422086387 25784320 5747 4294967295 134512640 134672761 3221224560 3221223008 134644040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6295 5747 603 41 0 6254 0
vsize: 25180
[startup+190.008 s]
Raw data (loadavg): 1.05 0.97 0.91 2/54 29691
Raw data (stat): 29691 (minisat+) R 29690 25285 25284 0 -1 0 7187 0 0 0 18961 38 0 0 25 0 1 0 422086387 26210304 5855 4294967295 134512640 134672761 3221224560 3221223120 134608004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6399 5855 603 41 0 6358 0
vsize: 25596
[startup+200.009 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 29691
Raw data (stat): 29691 (minisat+) R 29690 25285 25284 0 -1 0 7187 0 0 0 19960 39 0 0 25 0 1 0 422086387 25743360 5757 4294967295 134512640 134672761 3221224560 3221223008 134643984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6285 5757 603 41 0 6244 0
vsize: 25140
[startup+210.01 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 29691
Raw data (stat): 29691 (minisat+) R 29690 25285 25284 0 -1 0 7187 0 0 0 20959 41 0 0 25 0 1 0 422086387 25743360 5757 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6285 5757 603 41 0 6244 0
vsize: 25140
[startup+220.01 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 29691
Raw data (stat): 29691 (minisat+) R 29690 25285 25284 0 -1 0 7267 0 0 0 21958 41 0 0 25 0 1 0 422086387 25722880 5752 4294967295 134512640 134672761 3221224560 3221223008 134643548 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6280 5752 603 41 0 6239 0
vsize: 25120
[startup+230.011 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 29691
Raw data (stat): 29691 (minisat+) R 29690 25285 25284 0 -1 0 7267 0 0 0 22958 42 0 0 25 0 1 0 422086387 25722880 5752 4294967295 134512640 134672761 3221224560 3221223008 134644016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6280 5752 603 41 0 6239 0
vsize: 25120
[startup+240.01 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 29691
Raw data (stat): 29691 (minisat+) R 29690 25285 25284 0 -1 0 7330 0 0 0 23958 42 0 0 25 0 1 0 422086387 26189824 5815 4294967295 134512640 134672761 3221224560 3221222960 134604052 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6394 5815 603 41 0 6353 0
vsize: 25576
[startup+250.01 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 29691
Raw data (stat): 29691 (minisat+) R 29690 25285 25284 0 -1 0 7330 0 0 0 24958 42 0 0 25 0 1 0 422086387 25722880 5752 4294967295 134512640 134672761 3221224560 3221223600 134612589 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6280 5752 603 41 0 6239 0
vsize: 25120
[startup+260.01 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 29691
Raw data (stat): 29691 (minisat+) R 29690 25285 25284 0 -1 0 7333 0 0 0 25958 42 0 0 25 0 1 0 422086387 25722880 5755 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6280 5755 603 41 0 6239 0
vsize: 25120
[startup+270.011 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 29691
Raw data (stat): 29691 (minisat+) R 29690 25285 25284 0 -1 0 7385 0 0 0 26958 42 0 0 25 0 1 0 422086387 26083328 5807 4294967295 134512640 134672761 3221224560 3221223616 134644281 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6368 5807 603 41 0 6327 0
vsize: 25472
[startup+280.011 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 29691
Raw data (stat): 29691 (minisat+) R 29690 25285 25284 0 -1 0 7385 0 0 0 27958 42 0 0 25 0 1 0 422086387 25952256 5806 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6336 5806 603 41 0 6295 0
vsize: 25344
[startup+290.011 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 29691
Raw data (stat): 29691 (minisat+) R 29690 25285 25284 0 -1 0 7387 0 0 0 28958 42 0 0 25 0 1 0 422086387 25952256 5808 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6336 5808 603 41 0 6295 0
vsize: 25344
[startup+300.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29691
Raw data (stat): 29691 (minisat+) R 29690 25285 25284 0 -1 0 7507 0 0 0 29958 43 0 0 25 0 1 0 422086387 26505216 5928 4294967295 134512640 134672761 3221224560 3221223744 134616004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6471 5928 603 41 0 6430 0
vsize: 25884
[startup+310.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29691
Raw data (stat): 29691 (minisat+) R 29690 25285 25284 0 -1 0 7783 0 0 0 30957 44 0 0 25 0 1 0 422086387 27430912 6165 4294967295 134512640 134672761 3221224560 3221223744 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6697 6165 603 41 0 6656 0
vsize: 26788
[startup+320.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29691
Raw data (stat): 29691 (minisat+) R 29690 25285 25284 0 -1 0 7783 0 0 0 31957 44 0 0 25 0 1 0 422086387 27430912 6165 4294967295 134512640 134672761 3221224560 3221223600 134614266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6697 6165 603 41 0 6656 0
vsize: 26788
[startup+329.042 s]
Raw data (loadavg): 1.00 0.97 0.91 1/53 29691
Raw data (stat): 29691 (minisat+) R 29690 25285 25284 0 -1 0 7783 0 0 0 31957 44 0 0 25 0 1 0 422086387 27430912 6165 4294967295 134512640 134672761 3221224560 3221223600 134614266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6697 6165 603 41 0 6656 0
vsize: 0

Child status: 30
Real time (s): 329.042
CPU time (s): 329.049
CPU user time (s): 328.582
CPU system time (s): 0.466929
CPU usage (%): 100.002
Max. virtual memory (Kb): 26788
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	66
#### END VERIFIER DATA ####