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-1pb.opb
MD5SUM	9f27aad2edb50c2232eec4dba5ec2271
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	62
Optimality of the best value was proved	NO
Number of terms in the objective function	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.03484
Number of variables	672
Total number of constraints	2028
Number of constraints which are clauses	2004
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 5519

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-04-14 00:31:18 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3997 boxname=wulflinc17 idbench=237 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  9f27aad2edb50c2232eec4dba5ec2271  /oldhome/oroussel/tmp/wulflinc17/normalized-s4-4-3-1pb.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc17/normalized-s4-4-3-1pb.opb /oldhome/oroussel/tmp/wulflinc17/normalized-s4-4-3-1pb.opb
IDLAUNCH: 3997
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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	: 3
cpu MHz		: 451.072
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:        827352 kB
Buffers:         34996 kB
Cached:         137524 kB
SwapCached:       2376 kB
Active:          57856 kB
Inactive:       120012 kB
HighTotal:      131008 kB
HighFree:          644 kB
LowTotal:       903652 kB
LowFree:        826708 kB
SwapTotal:     2097892 kB
SwapFree:      2095516 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7036 kB
Slab:            23696 kB
Committed_AS:    63700 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 00:40:50 (client local time) WITH STATUS 30 IN 571.493 SECONDS
stats: 3997 0 571.493 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2028 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################################################################
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[2022]---> BDD-cost:    1
c ---[2004]---> BDD-cost:    1
c ---[1966]---> BDD-cost:    1
c ---[1956]---> BDD-cost:    1
c ---[1954]---> BDD-cost:    1
c ---[1928]---> BDD-cost:    1
c ---[1910]---> BDD-cost:    1
c ---[1885]---> BDD-cost:    1
c ---[1879]---> BDD-cost:    1
c ---[1862]---> BDD-cost:    1
c ---[1824]---> BDD-cost:    1
c ---[1814]---> BDD-cost:    1
c ---[1804]---> BDD-cost:    1
c ---[1794]---> BDD-cost:    1
c ---[1744]---> BDD-cost:    1
c ---[1742]---> BDD-cost:    1
c ---[1728]---> BDD-cost:    1
c ---[1702]---> BDD-cost:    1
c ---[1680]---> BDD-cost:    1
c ---[1670]---> BDD-cost:    1
c ---[1652]---> BDD-cost:    1
c ---[1630]---> BDD-cost:    1
c ---[1605]---> BDD-cost:    1
c ---[1599]---> BDD-cost:    1
c ---[1589]---> BDD-cost:    1
c ---[1579]---> BDD-cost:    1
c ---[1530]---> BDD-cost:    1
c ---[1528]---> BDD-cost:    1
c ---[1510]---> BDD-cost:    1
c ---[1489]---> BDD-cost:    1
c ---[1463]---> BDD-cost:    1
c ---[1457]---> BDD-cost:    1
c ---[1455]---> BDD-cost:    1
c ---[1429]---> BDD-cost:    1
c ---[1411]---> BDD-cost:    1
c ---[1385]---> BDD-cost:    1
c ---[1348]---> BDD-cost:    1
c ---[1326]---> BDD-cost:    1
c ---[1320]---> BDD-cost:    1
c ---[1314]---> BDD-cost:    1
c ---[1265]---> BDD-cost:    1
c ---[1255]---> BDD-cost:    1
c ---[1245]---> BDD-cost:    1
c ---[1243]---> BDD-cost:    1
c ---[1241]---> BDD-cost:    1
c ---[1215]---> BDD-cost:    1
c ---[1198]---> BDD-cost:    1
c ---[1172]---> BDD-cost:    1
c ---[1154]---> BDD-cost:    1
c ---[1132]---> BDD-cost:    1
c ---[1106]---> BDD-cost:    1
c ---[1100]---> BDD-cost:    1
c ---[1063]---> BDD-cost:    1
c ---[1041]---> BDD-cost:    1
c ---[1035]---> BDD-cost:    1
c ---[1029]---> BDD-cost:    1
c ---[1019]---> BDD-cost:    1
c ---[1009]---> BDD-cost:    1
c ---[ 959]---> BDD-cost:    1
c ---[ 957]---> BDD-cost:    1
c ---[ 955]---> BDD-cost:    1
c ---[ 929]---> BDD-cost:    1
c ---[ 911]---> BDD-cost:    1
c ---[ 885]---> BDD-cost:    1
c ---[ 883]---> BDD-cost:    1
c ---[ 857]---> BDD-cost:    1
c ---[ 839]---> BDD-cost:    1
c ---[ 813]---> BDD-cost:    1
c ---[ 811]---> BDD-cost:    1
c ---[ 785]---> BDD-cost:    1
c ---[ 768]---> BDD-cost:    1
c ---[ 742]---> BDD-cost:    1
c ---[ 736]---> BDD-cost:    1
c ---[ 718]---> BDD-cost:    1
c ---[ 680]---> BDD-cost:    1
c ---[ 670]---> BDD-cost:    1
c ---[ 656]---> BDD-cost:    1
c ---[ 630]---> BDD-cost:    1
c ---[ 608]---> BDD-cost:    1
c ---[ 598]---> BDD-cost:    1
c ---[ 592]---> BDD-cost:    1
c ---[ 575]---> BDD-cost:    1
c ---[ 537]---> BDD-cost:    1
c ---[ 527]---> BDD-cost:    1
c ---[ 521]---> BDD-cost:    1
c ---[ 504]---> BDD-cost:    1
c ---[ 466]---> BDD-cost:    1
c ---[ 456]---> BDD-cost:    1
c ---[ 438]---> BDD-cost:    1
c ---[ 416]---> BDD-cost:    1
c ---[ 390]---> BDD-cost:    1
c ---[ 384]---> BDD-cost:    1
c ---[ 370]---> BDD-cost:    1
c ---[ 344]---> BDD-cost:    1
c ---[ 322]---> BDD-cost:    1
c ---[ 312]---> BDD-cost:    1
c ---[ 294]---> BDD-cost:    1
c ---[ 272]---> BDD-cost:    1
c ---[ 246]---> BDD-cost:    1
c ---[ 240]---> BDD-cost:    1
c ---[ 238]---> BDD-cost:    1
c ---[ 212]---> BDD-cost:    1
c ---[ 194]---> BDD-cost:    1
c ---[ 168]---> BDD-cost:    1
c ---[ 166]---> BDD-cost:    1
c ---[ 140]---> BDD-cost:    1
c ---[ 122]---> 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 |    8412    24334 |    2523       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 |    8268    23894 |      --       0       --      -- |     --   | -144/-144
c |         0 |    8268    23894 |    3307       0        0     nan |  0.000 % |
c |       101 |    8268    23894 |    3637     101     4289    42.5 |  4.509 % |
c |       253 |    8268    23894 |    4001     253     8417    33.3 |  4.509 % |
c |       478 |    8268    23894 |    4401     478    13516    28.3 |  4.509 % |
c |       815 |    8268    23894 |    4842     815    27155    33.3 |  4.509 % |
c |      1321 |    8268    23894 |    5326    1321    46514    35.2 |  4.509 % |
c |      2084 |    8268    23894 |    5858    2084    85425    41.0 |  4.509 % |
c |      3227 |    8268    23894 |    6444    3227   118332    36.7 |  4.509 % |
c |      4937 |    8268    23894 |    7089    4937   153849    31.2 |  4.509 % |
c ==============================================================================
c (current CPU-time: 1.73873 s)
c ==============================================================================
c [1mFound solution: 72[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:30564     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5523 |   43691   106535 |   13107    5523   179158    32.4 |  4.509 % |
c   -- subsuming                       
c   -- var.elim.:  1000/23746          
c   -- var.elim.:  2000/23746          
c   -- var.elim.:  3000/23746          
c   -- var.elim.:  4000/23746          
c   -- var.elim.:  5000/23746          
c   -- var.elim.:  6000/23746          
c   -- var.elim.:  7000/23746          
c   -- var.elim.:  8000/23746          
c   -- var.elim.:  9000/23746          
c   -- var.elim.:  10000/23746          
c   -- var.elim.:  11000/23746          
c   -- var.elim.:  12000/23746          
c   -- var.elim.:  13000/23746          
c   -- var.elim.:  14000/23746          
c   -- var.elim.:  15000/23746          
c   -- var.elim.:  16000/23746          
c   -- var.elim.:  17000/23746          
c   -- var.elim.:  18000/23746          
c   -- var.elim.:  19000/23746          
c   -- var.elim.:  20000/23746          
c   -- var.elim.:  21000/23746          
c   -- var.elim.:  22000/23746          
c   -- var.elim.:  23000/23746          
c   -- var.elim.:  23746/23746          
c   -- var.elim.:  1000/11833          
c   -- var.elim.:  2000/11833          
c   -- var.elim.:  3000/11833          
c   -- var.elim.:  4000/11833          
c   -- var.elim.:  5000/11833          
c   -- var.elim.:  6000/11833          
c   -- var.elim.:  7000/11833          
c   -- var.elim.:  8000/11833          
c   -- var.elim.:  9000/11833          
c   -- var.elim.:  10000/11833          
c   -- var.elim.:  11000/11833          
c   -- var.elim.:  11833/11833          
c   -- var.elim.:  1000/6574          
c   -- var.elim.:  2000/6574          
c   -- var.elim.:  3000/6574          
c   -- var.elim.:  4000/6574          
c   -- var.elim.:  5000/6574          
c   -- var.elim.:  6000/6574          
c   -- var.elim.:  6574/6574          
c   -- var.elim.:  1000/6944          
c   -- var.elim.:  2000/6944          
c   -- var.elim.:  3000/6944          
c   -- var.elim.:  4000/6944          
c   -- var.elim.:  5000/6944          
c   -- var.elim.:  6000/6944          
c   -- var.elim.:  6944/6944          
c   -- var.elim.:  1000/3630          
c   -- var.elim.:  2000/3630          
c   -- var.elim.:  3000/3630          
c   -- var.elim.:  3630/3630          
c   -- var.elim.:  389/389          
c   -- subsuming                       
c   -- var.elim.:  1000/10139          
c   -- var.elim.:  2000/10139          
c   -- var.elim.:  3000/10139          
c   -- var.elim.:  4000/10139          
c   -- var.elim.:  5000/10139          
c   -- var.elim.:  6000/10139          
c   -- var.elim.:  7000/10139          
c   -- var.elim.:  8000/10139          
c   -- var.elim.:  9000/10139          
c   -- var.elim.:  10000/10139          
c   -- var.elim.:  10139/10139          
c   -- var.elim.:  1000/4771          
c   -- var.elim.:  2000/4771          
c   -- var.elim.:  3000/4771          
c   -- var.elim.:  4000/4771          
c   -- var.elim.:  4771/4771          
c   -- var.elim.:  1000/5415          
c   -- var.elim.:  2000/5415          
c   -- var.elim.:  3000/5415          
c   -- var.elim.:  4000/5415          
c   -- var.elim.:  5000/5415          
c   -- var.elim.:  5415/5415          
c   -- var.elim.:  1000/5691          
c   -- var.elim.:  2000/5691          
c   -- var.elim.:  3000/5691          
c   -- var.elim.:  4000/5691          
c   -- var.elim.:  5000/5691          
c   -- var.elim.:  5691/5691          
c   -- var.elim.:  1000/4661          
c   -- var.elim.:  2000/4661          
c   -- var.elim.:  3000/4661          
c   -- var.elim.:  4000/4661          
c   -- var.elim.:  4661/4661          
c   -- var.elim.:  168/168          
c   -- subsuming                       
c   -- var.elim.:  1000/6357          
c   -- var.elim.:  2000/6357          
c   -- var.elim.:  3000/6357          
c   -- var.elim.:  4000/6357          
c   -- var.elim.:  5000/6357          
c   -- var.elim.:  6000/6357          
c   -- var.elim.:  6357/6357          
c   -- var.elim.:  1000/4685          
c   -- var.elim.:  2000/4685          
c   -- var.elim.:  3000/4685          
c   -- var.elim.:  4000/4685          
c   -- var.elim.:  4685/4685          
c   -- var.elim.:  1000/2272          
c   -- var.elim.:  2000/2272          
c   -- var.elim.:  2272/2272          
c   -- var.elim.:  1000/1133          
c   -- var.elim.:  1133/1133          
c   -- var.elim.:  372/372          
c   -- subsuming                       
c   -- var.elim.:  1000/5128          
c   -- var.elim.:  2000/5128          
c   -- var.elim.:  3000/5128          
c   -- var.elim.:  4000/5128          
c   -- var.elim.:  5000/5128          
c   -- var.elim.:  5128/5128          
c   -- var.elim.:  1000/2931          
c   -- var.elim.:  2000/2931          
c   -- var.elim.:  2931/2931          
c   -- var.elim.:  1000/1235          
c   -- var.elim.:  1235/1235          
c   -- var.elim.:  1000/2079          
c   -- var.elim.:  2000/2079          
c   -- var.elim.:  2079/2079          
c   -- subsuming                       
c   -- var.elim.:  1000/2729          
c   -- var.elim.:  2000/2729          
c   -- var.elim.:  2729/2729          
c |      5523 |   30109   178656 |      --    5523       --      -- |     --   | -13414/72576
c |      5523 |   30109   178656 |   12043    5523   179158    32.4 |  4.509 % |
c |      5624 |   30109   178656 |   13247    5624   182202    32.4 |  1.946 % |
c |      5774 |   30109   178656 |   14572    5774   185596    32.1 |  1.946 % |
c |      6001 |   30109   178656 |   16030    6001   192444    32.1 |  1.946 % |
c |      6338 |   30109   178656 |   17633    6338   206457    32.6 |  1.946 % |
c |      6844 |   30109   178656 |   19396    6844   227965    33.3 |  1.946 % |
c |      7604 |   30109   178656 |   21335    7604   259709    34.2 |  1.946 % |
c |      8746 |   30109   178656 |   23469    8746   303453    34.7 |  1.946 % |
c |     10454 |   30109   178656 |   25816   10454   380426    36.4 |  1.946 % |
c |     13017 |   30109   178656 |   28398   13017   501476    38.5 |  1.946 % |
c |     16861 |   30109   178656 |   31237   16861   689041    40.9 |  1.946 % |
c ==============================================================================
c (current CPU-time: 94.9546 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 |     17842 |   37691   200059 |   11307   17842   731427    41.0 |  1.946 % |
c   -- subsuming                       
c   -- var.elim.:  1000/12702          
c   -- var.elim.:  2000/12702          
c   -- var.elim.:  3000/12702          
c   -- var.elim.:  4000/12702          
c   -- var.elim.:  5000/12702          
c   -- var.elim.:  6000/12702          
c   -- var.elim.:  7000/12702          
c   -- var.elim.:  8000/12702          
c   -- var.elim.:  9000/12702          
c   -- var.elim.:  10000/12702          
c   -- var.elim.:  11000/12702          
c   -- var.elim.:  12000/12702          
c   -- var.elim.:  12702/12702          
c   -- var.elim.:  1000/6286          
c   -- var.elim.:  2000/6286          
c   -- var.elim.:  3000/6286          
c   -- var.elim.:  4000/6286          
c   -- var.elim.:  5000/6286          
c   -- var.elim.:  6000/6286          
c   -- var.elim.:  6286/6286          
c   -- var.elim.:  1000/4540          
c   -- var.elim.:  2000/4540          
c   -- var.elim.:  3000/4540          
c   -- var.elim.:  4000/4540          
c   -- var.elim.:  4540/4540          
c   -- var.elim.:  1000/5276          
c   -- var.elim.:  2000/5276          
c   -- var.elim.:  3000/5276          
c   -- var.elim.:  4000/5276          
c   -- var.elim.:  5000/5276          
c   -- var.elim.:  5276/5276          
c   -- var.elim.:  1000/2261          
c   -- var.elim.:  2000/2261          
c   -- var.elim.:  2261/2261          
c   -- subsuming                       
c   -- var.elim.:  1000/5079          
c   -- var.elim.:  2000/5079          
c   -- var.elim.:  3000/5079          
c   -- var.elim.:  4000/5079          
c   -- var.elim.:  5000/5079          
c   -- var.elim.:  5079/5079          
c   -- var.elim.:  1000/2559          
c   -- var.elim.:  2000/2559          
c   -- var.elim.:  2559/2559          
c   -- var.elim.:  1000/2709          
c   -- var.elim.:  2000/2709          
c   -- var.elim.:  2709/2709          
c   -- var.elim.:  1000/2143          
c   -- var.elim.:  2000/2143          
c   -- var.elim.:  2143/2143          
c   -- var.elim.:  1000/1098          
c   -- var.elim.:  1098/1098          
c   -- subsuming                       
c   -- var.elim.:  929/929          
c |     17842 |   30264   178571 |      --   17842       --      -- |     --   | -7418/-21335
c |     17842 |   30264   178571 |   12105   17842   731427    41.0 |  1.946 % |
c |     17942 |   30264   178571 |   13316   11518   500591    43.5 |  1.968 % |
c |     18094 |   30264   178571 |   14647   11670   503996    43.2 |  1.968 % |
c |     18320 |   30264   178571 |   16112   11896   507085    42.6 |  1.968 % |
c |     18657 |   30264   178571 |   17723   12233   518371    42.4 |  1.968 % |
c |     19170 |   30264   178571 |   19496   12746   536627    42.1 |  1.968 % |
c |     19929 |   30264   178571 |   21445   13505   564941    41.8 |  1.968 % |
c |     21070 |   30264   178571 |   23590   14646   611377    41.7 |  1.968 % |
c |     22779 |   30264   178571 |   25949   16355   673025    41.2 |  1.968 % |
c |     25341 |   30221   178147 |   28503   18915   781980    41.3 |  2.079 % |
c |     29187 |   30210   178026 |   31342   22760   949504    41.7 |  2.117 % |
c ==============================================================================
c (current CPU-time: 142.142 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 |     30648 |   36384   195470 |   10915   24221  1016288    42.0 |  2.117 % |
c   -- subsuming                       
c   -- var.elim.:  1000/12276          
c   -- var.elim.:  2000/12276          
c   -- var.elim.:  3000/12276          
c   -- var.elim.:  4000/12276          
c   -- var.elim.:  5000/12276          
c   -- var.elim.:  6000/12276          
c   -- var.elim.:  7000/12276          
c   -- var.elim.:  8000/12276          
c   -- var.elim.:  9000/12276          
c   -- var.elim.:  10000/12276          
c   -- var.elim.:  11000/12276          
c   -- var.elim.:  12000/12276          
c   -- var.elim.:  12276/12276          
c   -- var.elim.:  1000/5387          
c   -- var.elim.:  2000/5387          
c   -- var.elim.:  3000/5387          
c   -- var.elim.:  4000/5387          
c   -- var.elim.:  5000/5387          
c   -- var.elim.:  5387/5387          
c   -- var.elim.:  1000/2313          
c   -- var.elim.:  2000/2313          
c   -- var.elim.:  2313/2313          
c   -- var.elim.:  1000/3883          
c   -- var.elim.:  2000/3883          
c   -- var.elim.:  3000/3883          
c   -- var.elim.:  3883/3883          
c   -- var.elim.:  1000/1498          
c   -- var.elim.:  1498/1498          
c   -- var.elim.:  1000/1204          
c   -- var.elim.:  1204/1204          
c   -- var.elim.:  482/482          
c   -- subsuming                       
c   -- var.elim.:  1000/4368          
c   -- var.elim.:  2000/4368          
c   -- var.elim.:  3000/4368          
c   -- var.elim.:  4000/4368          
c   -- var.elim.:  4368/4368          
c   -- var.elim.:  1000/2602          
c   -- var.elim.:  2000/2602          
c   -- var.elim.:  2602/2602          
c   -- var.elim.:  1000/2912          
c   -- var.elim.:  2000/2912          
c   -- var.elim.:  2912/2912          
c   -- var.elim.:  1000/2278          
c   -- var.elim.:  2000/2278          
c   -- var.elim.:  2278/2278          
c   -- var.elim.:  1000/1780          
c   -- var.elim.:  1780/1780          
c   -- var.elim.:  1000/1002          
c   -- var.elim.:  1002/1002          
c   -- var.elim.:  26/26          
c   -- subsuming                       
c   -- var.elim.:  1000/1068          
c   -- var.elim.:  1068/1068          
c |     30648 |   30243   181395 |      --   24221       --      -- |     --   | -6126/-13924
c |     30648 |   30243   181395 |   12097   24221  1016288    42.0 |  2.117 % |
c |     30750 |   30243   181395 |   13306    8562   326659    38.2 |  2.170 % |
c |     30901 |   30243   181395 |   14637    8713   332984    38.2 |  2.170 % |
c |     31126 |   30243   181395 |   16101    8938   343465    38.4 |  2.170 % |
c |     31465 |   30243   181395 |   17711    9277   357132    38.5 |  2.170 % |
c |     31973 |   30243   181395 |   19482    9785   379247    38.8 |  2.170 % |
c |     32734 |   30243   181395 |   21430   10546   416907    39.5 |  2.170 % |
c |     33873 |   30243   181395 |   23574   11685   491065    42.0 |  2.170 % |
c |     35581 |   30212   181189 |   25904   13391   566432    42.3 |  2.267 % |
c |     38146 |   30212   181189 |   28495   15956   667307    41.8 |  2.267 % |
c ==============================================================================
c (current CPU-time: 179.747 s)
c ==============================================================================
c [1mFound solution: 64[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:27554     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     40845 |   62523   256248 |   18756   18612   786388    42.3 |  2.267 % |
c   -- subsuming                       
c   -- var.elim.:  1000/29275          
c   -- var.elim.:  2000/29275          
c   -- var.elim.:  3000/29275          
c   -- var.elim.:  4000/29275          
c   -- var.elim.:  5000/29275          
c   -- var.elim.:  6000/29275          
c   -- var.elim.:  7000/29275          
c   -- var.elim.:  8000/29275          
c   -- var.elim.:  9000/29275          
c   -- var.elim.:  10000/29275          
c   -- var.elim.:  11000/29275          
c   -- var.elim.:  12000/29275          
c   -- var.elim.:  13000/29275          
c   -- var.elim.:  14000/29275          
c   -- var.elim.:  15000/29275          
c   -- var.elim.:  16000/29275          
c   -- var.elim.:  17000/29275          
c   -- var.elim.:  18000/29275          
c   -- var.elim.:  19000/29275          
c   -- var.elim.:  20000/29275          
c   -- var.elim.:  21000/29275          
c   -- var.elim.:  22000/29275          
c   -- var.elim.:  23000/29275          
c   -- var.elim.:  24000/29275          
c   -- var.elim.:  25000/29275          
c   -- var.elim.:  26000/29275          
c   -- var.elim.:  27000/29275          
c   -- var.elim.:  28000/29275          
c   -- var.elim.:  29000/29275          
c   -- var.elim.:  29275/29275          
c   -- var.elim.:  1000/12683          
c   -- var.elim.:  2000/12683          
c   -- var.elim.:  3000/12683          
c   -- var.elim.:  4000/12683          
c   -- var.elim.:  5000/12683          
c   -- var.elim.:  6000/12683          
c   -- var.elim.:  7000/12683          
c   -- var.elim.:  8000/12683          
c   -- var.elim.:  9000/12683          
c   -- var.elim.:  10000/12683          
c   -- var.elim.:  11000/12683          
c   -- var.elim.:  12000/12683          
c   -- var.elim.:  12683/12683          
c   -- var.elim.:  1000/3657          
c   -- var.elim.:  2000/3657          
c   -- var.elim.:  3000/3657          
c   -- var.elim.:  3657/3657          
c   -- var.elim.:  1000/4767          
c   -- var.elim.:  2000/4767          
c   -- var.elim.:  3000/4767          
c   -- var.elim.:  4000/4767          
c   -- var.elim.:  4767/4767          
c   -- var.elim.:  1000/3149          
c   -- var.elim.:  2000/3149          
c   -- var.elim.:  3000/3149          
c   -- var.elim.:  3149/3149          
c   -- var.elim.:  368/368          
c   -- subsuming                       
c   -- var.elim.:  1000/11351          
c   -- var.elim.:  2000/11351          
c   -- var.elim.:  3000/11351          
c   -- var.elim.:  4000/11351          
c   -- var.elim.:  5000/11351          
c   -- var.elim.:  6000/11351          
c   -- var.elim.:  7000/11351          
c   -- var.elim.:  8000/11351          
c   -- var.elim.:  9000/11351          
c   -- var.elim.:  10000/11351          
c   -- var.elim.:  11000/11351          
c   -- var.elim.:  11351/11351          
c   -- var.elim.:  1000/4551          
c   -- var.elim.:  2000/4551          
c   -- var.elim.:  3000/4551          
c   -- var.elim.:  4000/4551          
c   -- var.elim.:  4551/4551          
c   -- var.elim.:  1000/5345          
c   -- var.elim.:  2000/5345          
c   -- var.elim.:  3000/5345          
c   -- var.elim.:  4000/5345          
c   -- var.elim.:  5000/5345          
c   -- var.elim.:  5345/5345          
c   -- var.elim.:  1000/6167          
c   -- var.elim.:  2000/6167          
c   -- var.elim.:  3000/6167          
c   -- var.elim.:  4000/6167          
c   -- var.elim.:  5000/6167          
c   -- var.elim.:  6000/6167          
c   -- var.elim.:  6167/6167          
c   -- var.elim.:  1000/3543          
c   -- var.elim.:  2000/3543          
c   -- var.elim.:  3000/3543          
c   -- var.elim.:  3543/3543          
c   -- subsuming                       
c   -- var.elim.:  1000/6393          
c   -- var.elim.:  2000/6393          
c   -- var.elim.:  3000/6393          
c   -- var.elim.:  4000/6393          
c   -- var.elim.:  5000/6393          
c   -- var.elim.:  6000/6393          
c   -- var.elim.:  6393/6393          
c   -- var.elim.:  1000/4337          
c   -- var.elim.:  2000/4337          
c   -- var.elim.:  3000/4337          
c   -- var.elim.:  4000/4337          
c   -- var.elim.:  4337/4337          
c   -- var.elim.:  1000/4631          
c   -- var.elim.:  2000/4631          
c   -- var.elim.:  3000/4631          
c   -- var.elim.:  4000/4631          
c   -- var.elim.:  4631/4631          
c   -- var.elim.:  1000/3771          
c   -- var.elim.:  2000/3771          
c   -- var.elim.:  3000/3771          
c   -- var.elim.:  3771/3771          
c   -- subsuming                       
c   -- var.elim.:  1000/5091          
c   -- var.elim.:  2000/5091          
c   -- var.elim.:  3000/5091          
c   -- var.elim.:  4000/5091          
c   -- var.elim.:  5000/5091          
c   -- var.elim.:  5091/5091          
c   -- var.elim.:  1000/2191          
c   -- var.elim.:  2000/2191          
c   -- var.elim.:  2191/2191          
c   -- var.elim.:  1000/1476          
c   -- var.elim.:  1476/1476          
c   -- var.elim.:  1000/3034          
c   -- var.elim.:  2000/3034          
c   -- var.elim.:  3000/3034          
c   -- var.elim.:  3034/3034          
c   -- subsuming                       
c   -- var.elim.:  1000/3098          
c   -- var.elim.:  2000/3098          
c   -- var.elim.:  3000/3098          
c   -- var.elim.:  3098/3098          
c   -- var.elim.:  1000/1250          
c   -- var.elim.:  1250/1250          
c   -- var.elim.:  7/7          
c   -- var.elim.:  266/266          
c |     40845 |   49294   324886 |      --   18612       --      -- |     --   | -13229/68639
c |     40845 |   49294   324886 |   19717   18612   786388    42.3 |  2.267 % |
c |     40945 |   49260   324613 |   21674   16362   659823    40.3 |  1.847 % |
c |     41095 |   49209   324206 |   23817   16510   666055    40.3 |  1.959 % |
c |     41321 |   49076   323039 |   26128   16731   674580    40.3 |  2.250 % |
c |     41658 |   48840   321075 |   28602   17042   684054    40.1 |  2.683 % |
c |     42167 |   48221   305021 |   31064   17540   705827    40.2 |  3.417 % |
c |     42926 |   48113   304223 |   34094   18288   732352    40.0 |  3.574 % |
c ==============================================================================
c (current CPU-time: 330.111 s)
c ==============================================================================
c [1mFound solution: 62[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:28818     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     43511 |   81262   380659 |   24378   18859   765813    40.6 |  3.574 % |
c   -- subsuming                       
c   -- var.elim.:  1000/34084          
c   -- var.elim.:  2000/34084          
c   -- var.elim.:  3000/34084          
c   -- var.elim.:  4000/34084          
c   -- var.elim.:  5000/34084          
c   -- var.elim.:  6000/34084          
c   -- var.elim.:  7000/34084          
c   -- var.elim.:  8000/34084          
c   -- var.elim.:  9000/34084          
c   -- var.elim.:  10000/34084          
c   -- var.elim.:  11000/34084          
c   -- var.elim.:  12000/34084          
c   -- var.elim.:  13000/34084          
c   -- var.elim.:  14000/34084          
c   -- var.elim.:  15000/34084          
c   -- var.elim.:  16000/34084          
c   -- var.elim.:  17000/34084          
c   -- var.elim.:  18000/34084          
c   -- var.elim.:  19000/34084          
c   -- var.elim.:  20000/34084          
c   -- var.elim.:  21000/34084          
c   -- var.elim.:  22000/34084          
c   -- var.elim.:  23000/34084          
c   -- var.elim.:  24000/34084          
c   -- var.elim.:  25000/34084          
c   -- var.elim.:  26000/34084          
c   -- var.elim.:  27000/34084          
c   -- var.elim.:  28000/34084          
c   -- var.elim.:  29000/34084          
c   -- var.elim.:  30000/34084          
c   -- var.elim.:  31000/34084          
c   -- var.elim.:  32000/34084          
c   -- var.elim.:  33000/34084          
c   -- var.elim.:  34000/34084          
c   -- var.elim.:  34084/34084          
c   -- var.elim.:  1000/19052          
c   -- var.elim.:  2000/19052          
c   -- var.elim.:  3000/19052          
c   -- var.elim.:  4000/19052          
c   -- var.elim.:  5000/19052          
c   -- var.elim.:  6000/19052          
c   -- var.elim.:  7000/19052          
c   -- var.elim.:  8000/19052          
c   -- var.elim.:  9000/19052          
c   -- var.elim.:  10000/19052          
c   -- var.elim.:  11000/19052          
c   -- var.elim.:  12000/19052          
c   -- var.elim.:  13000/19052          
c   -- var.elim.:  14000/19052          
c   -- var.elim.:  15000/19052          
c   -- var.elim.:  16000/19052          
c   -- var.elim.:  17000/19052          
c   -- var.elim.:  18000/19052          
c   -- var.elim.:  19000/19052          
c   -- var.elim.:  19052/19052          
c   -- var.elim.:  1000/4752          
c   -- var.elim.:  2000/4752          
c   -- var.elim.:  3000/4752          
c   -- var.elim.:  4000/4752          
c   -- var.elim.:  4752/4752          
c   -- var.elim.:  1000/5782          
c   -- var.elim.:  2000/5782          
c   -- var.elim.:  3000/5782          
c   -- var.elim.:  4000/5782          
c   -- var.elim.:  5000/5782          
c   -- var.elim.:  5782/5782          
c   -- var.elim.:  1000/5019          
c   -- var.elim.:  2000/5019          
c   -- var.elim.:  3000/5019          
c   -- var.elim.:  4000/5019          
c   -- var.elim.:  5000/5019          
c   -- var.elim.:  5019/5019          
c   -- var.elim.:  313/313          
c   -- subsuming                       
c   -- var.elim.:  1000/14793          
c   -- var.elim.:  2000/14793          
c   -- var.elim.:  3000/14793          
c   -- var.elim.:  4000/14793          
c   -- var.elim.:  5000/14793          
c   -- var.elim.:  6000/14793          
c   -- var.elim.:  7000/14793          
c   -- var.elim.:  8000/14793          
c   -- var.elim.:  9000/14793          
c   -- var.elim.:  10000/14793          
c   -- var.elim.:  11000/14793          
c   -- var.elim.:  12000/14793          
c   -- var.elim.:  13000/14793          
c   -- var.elim.:  14000/14793          
c   -- var.elim.:  14793/14793          
c   -- var.elim.:  1000/9562          
c   -- var.elim.:  2000/9562          
c   -- var.elim.:  3000/9562          
c   -- var.elim.:  4000/9562          
c   -- var.elim.:  5000/9562          
c   -- var.elim.:  6000/9562          
c   -- var.elim.:  7000/9562          
c   -- var.elim.:  8000/9562          
c   -- var.elim.:  9000/9562          
c   -- var.elim.:  9562/9562          
c   -- var.elim.:  1000/5333          
c   -- var.elim.:  2000/5333          
c   -- var.elim.:  3000/5333          
c   -- var.elim.:  4000/5333          
c   -- var.elim.:  5000/5333          
c   -- var.elim.:  5333/5333          
c   -- var.elim.:  1000/8002          
c   -- var.elim.:  2000/8002          
c   -- var.elim.:  3000/8002          
c   -- var.elim.:  4000/8002          
c   -- var.elim.:  5000/8002          
c   -- var.elim.:  6000/8002          
c   -- var.elim.:  7000/8002          
c   -- var.elim.:  8000/8002          
c   -- var.elim.:  8002/8002          
c   -- var.elim.:  1000/7993          
c   -- var.elim.:  2000/7993          
c   -- var.elim.:  3000/7993          
c   -- var.elim.:  4000/7993          
c   -- var.elim.:  5000/7993          
c   -- var.elim.:  6000/7993          
c   -- var.elim.:  7000/7993          
c   -- var.elim.:  7993/7993          
c   -- var.elim.:  1000/2116          
c   -- var.elim.:  2000/2116          
c   -- var.elim.:  2116/2116          
c   -- subsuming                       
c   -- var.elim.:  1000/11706          
c   -- var.elim.:  2000/11706          
c   -- var.elim.:  3000/11706          
c   -- var.elim.:  4000/11706          
c   -- var.elim.:  5000/11706          
c   -- var.elim.:  6000/11706          
c   -- var.elim.:  7000/11706          
c   -- var.elim.:  8000/11706          
c   -- var.elim.:  9000/11706          
c   -- var.elim.:  10000/11706          
c   -- var.elim.:  11000/11706          
c   -- var.elim.:  11706/11706          
c   -- var.elim.:  1000/4792          
c   -- var.elim.:  2000/4792          
c   -- var.elim.:  3000/4792          
c   -- var.elim.:  4000/4792          
c   -- var.elim.:  4792/4792          
c   -- var.elim.:  1000/5810          
c   -- var.elim.:  2000/5810          
c   -- var.elim.:  3000/5810          
c   -- var.elim.:  4000/5810          
c   -- var.elim.:  5000/5810          
c   -- var.elim.:  5810/5810          
c   -- var.elim.:  1000/4617          
c   -- var.elim.:  2000/4617          
c   -- var.elim.:  3000/4617          
c   -- var.elim.:  4000/4617          
c   -- var.elim.:  4617/4617          
c   -- subsuming                       
c   -- var.elim.:  1000/8427          
c   -- var.elim.:  2000/8427          
c   -- var.elim.:  3000/8427          
c   -- var.elim.:  4000/8427          
c   -- var.elim.:  5000/8427          
c   -- var.elim.:  6000/8427          
c   -- var.elim.:  7000/8427          
c   -- var.elim.:  8000/8427          
c   -- var.elim.:  8427/8427          
c   -- var.elim.:  1000/3572          
c   -- var.elim.:  2000/3572          
c   -- var.elim.:  3000/3572          
c   -- var.elim.:  3572/3572          
c   -- subsuming                       
c   -- var.elim.:  1000/2766          
c   -- var.elim.:  2000/2766          
c   -- var.elim.:  2766/2766          
c |     43511 |   67872   465024 |      --   18859       --      -- |     --   | -13390/84366
c |     43511 |   67872   465024 |   27148   17533   685683    39.1 |  3.574 % |
c |     43611 |   67872   465024 |   29863   17633   691148    39.2 |  2.853 % |
c |     43765 |   67708   463608 |   32770   17782   703336    39.6 |  3.046 % |
c |     43991 |   67672   463293 |   36028   18001   723214    40.2 |  3.103 % |
c |     44329 |   67672   463293 |   39631   18339   734021    40.0 |  3.103 % |
c |     44835 |   67540   462149 |   43509   18836   756257    40.1 |  3.268 % |
c |     45595 |   67307   460225 |   47695   19579   803719    41.1 |  3.620 % |
c |     46734 |   66428   437969 |   51779   20669   908546    44.0 |  4.406 % |
c |     48442 |   66041   433053 |   56625   22356  1099461    49.2 |  4.840 % |
c |     51005 |   65841   431329 |   62099   24907  1455813    58.4 |  5.094 % |
c ==============================================================================
c [1mOptimal solution: 62[0m
s OPTIMUM FOUND
v -v1 -v2 -v3 -v4 -v5 -v6 -v7 -v8 -v9 v10 v11 -v12 -v13 -v14 -v15 -v16 -v17 -v18 -v19 -v20 v21 -v22 -v23 -v24 -v25 -v26 -v27 v28 v29 -v30 -v31 -v32 -v33 -v34 -v35 -v36 -v37 -v38 -v39 -v40 v41 -v42 -v43 -v44 v45 -v46 -v47 -v48 -v49 -v50 -v51 -v52 -v53 -v54 v55 -v56 -v57 -v58 -v59 -v60 -v61 -v62 -v63 -v64 -v65 -v66 -v67 -v68 -v69 -v70 -v71 -v72 -v73 -v74 -v75 v76 -v77 -v78 -v79 v80 v81 -v82 -v83 -v84 -v85 -v86 -v87 -v88 -v89 v90 -v91 -v92 -v93 -v94 -v95 -v96 -v97 -v98 -v99 -v100 v101 -v102 v103 -v104 -v105 -v106 -v107 -v108 -v109 -v110 v111 -v112 -v113 v114 -v115 -v116 -v117 -v118 -v119 -v120 -v121 -v122 -v123 -v124 -v125 -v126 -v127 v128 -v129 -v130 -v131 -v132 -v133 -v134 -v135 -v136 -v137 -v138 v139 -v140 -v141 v142 -v143 -v144 -v145 -v146 -v147 -v148 -v149 -v150 v151 -v152 -v153 -v154 -v155 -v156 -v157 -v158 -v159 -v160 v161 -v162 -v163 -v164 -v165 -v166 -v167 -v168 -v169 -v170 -v171 -v172 -v173 -v174 -v175 -v176 -v177 -v178 v179 -v180 -v181 -v182 -v183 -v184 -v185 -v186 -v187 -v188 -v189 -v190 v191 -v192 -v193 -v194 -v195 -v196 -v197 -v198 -v199 -v200 -v201 -v202 -v203 v204 -v205 -v206 v207 -v208 -v209 -v210 v211 -v212 -v213 -v214 v215 -v216 -v217 -v218 -v219 -v220 -v221 v222 -v223 v224 -v225 -v226 -v227 -v228 -v229 -v230 -v231 -v232 -v233 -v234 v235 -v236 -v237 -v238 -v239 -v240 -v241 -v242 -v243 -v244 -v245 v246 -v247 -v248 -v249 -v250 -v251 -v252 -v253 -v254 -v255 -v256 -v257 -v258 -v259 v260 -v261 -v262 -v263 -v264 -v265 -v266 -v267 -v268 -v269 -v270 -v271 -v272 -v273 v274 v275 -v276 -v277 -v278 -v279 -v280 -v281 -v282 -v283 -v284 -v285 -v286 v287 -v288 -v289 v290 -v291 -v292 -v293 -v294 -v295 -v296 -v297 -v298 -v299 -v300 -v301 -v302 -v303 -v304 -v305 -v306 -v307 -v308 -v309 -v310 -v311 -v312 v313 -v314 -v315 -v316 -v317 -v318 -v319 -v320 -v321 -v322 -v323 -v324 -v325 v326 -v327 -v328 -v329 v330 -v331 -v332 -v333 -v334 -v335 -v336 -v337 -v338 -v339 -v340 -v341 -v342 -v343 -v344 -v345 -v346 -v347 -v348 v349 -v350 -v351 -v352 -v353 -v354 -v355 -v356 -v357 -v358 -v359 -v360 -v361 -v362 v363 v364 v365 -v366 -v367 -v368 -v369 -v370 -v371 -v372 -v373 -v374 v375 -v376 -v377 -v378 -v379 -v380 -v381 -v382 -v383 -v384 -v385 -v386 -v387 -v388 -v389 -v390 -v391 -v392 -v393 v394 -v395 -v396 v397 -v398 -v399 -v400 v401 -v402 -v403 -v404 v405 -v406 -v407 -v408 -v409 -v410 -v411 -v412 -v413 v414 -v415 -v416 -v417 -v418 -v419 -v420 -v421 -v422 -v423 -v424 -v425 -v426 -v427 v428 -v429 -v430 -v431 v432 -v433 -v434 -v435 -v436 -v437 -v438 -v439 -v440 -v441 -v442 -v443 -v444 -v445 -v446 -v447 -v448 -v449 -v450 -v451 v452 -v453 -v454 -v455 -v456 -v457 -v458 -v459 -v460 -v461 -v462 -v463 -v464 -v465 -v466 -v467 v468 -v469 -v470 -v471 -v472 -v473 -v474 -v475 -v476 -v477 -v478 -v479 -v480 -v481 -v482 -v483 -v484 -v485 -v486 -v487 -v488 v489 -v490 -v491 -v492 -v493 -v494 -v495 -v496 -v497 -v498 -v499 -v500 -v501 -v502 -v503 -v504 -v505 -v506 -v507 -v508 -v509 -v510 -v511 -v512 v513 -v514 -v515 -v516 -v517 -v518 -v519 -v520 -v521 -v522 -v523 -v524 -v525 -v526 -v527 -v528 v529 -v530 -v531 -v532 -v533 -v534 -v535 -v536 -v537 -v538 -v539 -v540 v541 -v542 -v543 -v544 -v545 -v546 -v547 -v548 -v549 -v550 -v551 -v552 -v553 -v554 -v555 -v556 -v557 -v558 -v559 -v560 -v561 -v562 -v563 v564 -v565 -v566 -v567 -v568 -v569 -v570 -v571 -v572 -v573 -v574 -v575 -v576 v577 -v578 -v579 -v580 -v581 -v582 -v583 -v584 -v585 -v586 -v587 -v588 -v589 -v590 -v591 -v592 -v593 -v594 -v595 -v596 -v597 -v598 -v599 -v600 -v601 -v602 -v603 -v604 -v605 -v606 -v607 -v608 -v609 -v610 -v611 -v612 -v613 -v614 -v615 v616 -v617 -v618 -v619 -v620 -v621 -v622 -v623 -v624 -v625 -v626 v627 -v628 -v629 -v630 -v631 -v632 -v633 -v634 -v635 -v636 -v637 -v638 -v639 -v640 -v641 -v642 -v643 -v644 -v645 -v646 -v647 -v648 -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              : 58
c conflicts             : 52499          (92 /sec)
c decisions             : 119693         (210 /sec)
c propagations          : 21261686       (37286 /sec)
c inspects              : 85740988       (150362 /sec)
c CPU time              : 570.229 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.78 0.94 0.90 2/55 27014
Raw data (stat): 27014 (runsolver) R 27013 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480296792 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.0001 s]
Raw data (loadavg): 0.81 0.94 0.90 2/55 27014
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 4195 0 0 0 985 14 0 0 25 0 1 0 480296792 19709952 4041 4294967295 134512640 134672761 3221224560 3221223008 134643474 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4812 4041 603 41 0 4771 0
vsize: 19248
[startup+20.0011 s]
Raw data (loadavg): 0.84 0.94 0.90 2/55 27014
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 4256 0 0 0 1983 16 0 0 25 0 1 0 480296792 19976192 4102 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4877 4102 603 41 0 4836 0
vsize: 19508
[startup+30.0017 s]
Raw data (loadavg): 0.87 0.94 0.90 2/55 27014
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 4393 0 0 0 2982 17 0 0 25 0 1 0 480296792 20463616 4216 4294967295 134512640 134672761 3221224560 3221223104 134621051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4996 4216 603 41 0 4955 0
vsize: 19984
[startup+40.0008 s]
Raw data (loadavg): 0.89 0.94 0.90 2/55 27014
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 4394 0 0 0 3980 19 0 0 25 0 1 0 480296792 19996672 4129 4294967295 134512640 134672761 3221224560 3221223008 134643532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4129 603 41 0 4841 0
vsize: 19528
[startup+50.0017 s]
Raw data (loadavg): 0.90 0.94 0.90 2/55 27014
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 4397 0 0 0 4979 20 0 0 25 0 1 0 480296792 20123648 4132 4294967295 134512640 134672761 3221224560 3221223008 134644014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4913 4132 603 41 0 4872 0
vsize: 19652
[startup+60.0015 s]
Raw data (loadavg): 0.92 0.94 0.91 2/55 27014
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 4511 0 0 0 5978 20 0 0 25 0 1 0 480296792 20119552 4159 4294967295 134512640 134672761 3221224560 3221223008 134643954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4912 4159 603 41 0 4871 0
vsize: 19648
[startup+70.0016 s]
Raw data (loadavg): 0.93 0.95 0.91 2/55 27014
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 4590 0 0 0 6977 21 0 0 25 0 1 0 480296792 20516864 4238 4294967295 134512640 134672761 3221224560 3221223104 134621049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5009 4238 603 41 0 4968 0
vsize: 20036
[startup+80.0015 s]
Raw data (loadavg): 0.94 0.95 0.91 2/55 27014
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 4590 0 0 0 7976 22 0 0 25 0 1 0 480296792 20119552 4159 4294967295 134512640 134672761 3221224560 3221223008 134644032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4912 4159 603 41 0 4871 0
vsize: 19648
[startup+90.0011 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 27014
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 4756 0 0 0 8976 22 0 0 25 0 1 0 480296792 20561920 4239 4294967295 134512640 134672761 3221224560 3221223744 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5020 4239 603 41 0 4979 0
vsize: 20080
[startup+100.001 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 27014
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 6368 0 0 0 9966 32 0 0 25 0 1 0 480296792 26595328 5243 4294967295 134512640 134672761 3221224560 3221223008 134643580 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6493 5243 603 41 0 6452 0
vsize: 25972
[startup+110.001 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 27014
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 6368 0 0 0 10965 33 0 0 25 0 1 0 480296792 26595328 5243 4294967295 134512640 134672761 3221224560 3221223008 134643948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6493 5243 603 41 0 6452 0
vsize: 25972
[startup+120.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 27014
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 6453 0 0 0 11964 34 0 0 25 0 1 0 480296792 27029504 5328 4294967295 134512640 134672761 3221224560 3221223104 134621062 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6599 5328 603 41 0 6558 0
vsize: 26396
[startup+130.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 27014
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 6453 0 0 0 12963 35 0 0 25 0 1 0 480296792 26607616 5248 4294967295 134512640 134672761 3221224560 3221223008 134643474 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6496 5248 603 41 0 6455 0
vsize: 25984
[startup+140.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 27014
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 6627 0 0 0 13963 36 0 0 25 0 1 0 480296792 27000832 5338 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6592 5338 603 41 0 6551 0
vsize: 26368
[startup+150.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 27014
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 8408 0 0 0 14954 45 0 0 25 0 1 0 480296792 28594176 5822 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6981 5822 603 41 0 6940 0
vsize: 27924
[startup+160.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 27014
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 8504 0 0 0 15952 46 0 0 25 0 1 0 480296792 29102080 5917 4294967295 134512640 134672761 3221224560 3221222640 134566712 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7105 5917 603 41 0 7064 0
vsize: 28420
[startup+170.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 27014
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 8504 0 0 0 16951 47 0 0 25 0 1 0 480296792 28508160 5822 4294967295 134512640 134672761 3221224560 3221223008 134643511 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6960 5822 603 41 0 6919 0
vsize: 27840
[startup+180.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27014
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 8602 0 0 0 17950 48 0 0 25 0 1 0 480296792 28704768 5838 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7008 5838 603 41 0 6967 0
vsize: 28032
[startup+190.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27014
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 11844 0 0 0 18933 64 0 0 25 0 1 0 480296792 34930688 7904 4294967295 134512640 134672761 3221224560 3221223008 134643548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8528 7904 603 41 0 8487 0
vsize: 34112
[startup+200.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27014
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 11844 0 0 0 19932 66 0 0 25 0 1 0 480296792 34930688 7904 4294967295 134512640 134672761 3221224560 3221223008 134643954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8528 7904 603 41 0 8487 0
vsize: 34112
[startup+210.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27014
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 11863 0 0 0 20930 67 0 0 25 0 1 0 480296792 35065856 7923 4294967295 134512640 134672761 3221224560 3221223008 134643624 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8561 7923 603 41 0 8520 0
vsize: 34244
[startup+220.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27014
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 12044 0 0 0 21930 67 0 0 25 0 1 0 480296792 36233216 8104 4294967295 134512640 134672761 3221224560 3221223104 134621186 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8846 8104 603 41 0 8805 0
vsize: 35384
[startup+230.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27014
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 12044 0 0 0 22926 71 0 0 25 0 1 0 480296792 35065856 7955 4294967295 134512640 134672761 3221224560 3221223008 134643542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8561 7955 603 41 0 8520 0
vsize: 34244
[startup+240.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27014
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 12044 0 0 0 23925 72 0 0 25 0 1 0 480296792 35065856 7955 4294967295 134512640 134672761 3221224560 3221223008 134643984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8561 7955 603 41 0 8520 0
vsize: 34244
[startup+250.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27014
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 12168 0 0 0 24925 72 0 0 25 0 1 0 480296792 35835904 8079 4294967295 134512640 134672761 3221224560 3221223104 134621062 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8749 8079 603 41 0 8708 0
vsize: 34996
[startup+260.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27016
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 12168 0 0 0 25924 73 0 0 25 0 1 0 480296792 35065856 7955 4294967295 134512640 134672761 3221224560 3221223008 134643580 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8561 7955 603 41 0 8520 0
vsize: 34244
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27016
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 12173 0 0 0 26924 74 0 0 25 0 1 0 480296792 35168256 7960 4294967295 134512640 134672761 3221224560 3221223008 134643542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8586 7960 603 41 0 8545 0
vsize: 34344
[startup+280.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27016
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 12365 0 0 0 27924 74 0 0 25 0 1 0 480296792 36110336 8134 4294967295 134512640 134672761 3221224560 3221223024 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8816 8134 603 41 0 8775 0
vsize: 35264
[startup+290.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27016
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 12365 0 0 0 28923 75 0 0 25 0 1 0 480296792 35168256 7980 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8586 7980 603 41 0 8545 0
vsize: 34344
[startup+300.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27016
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 12365 0 0 0 29923 75 0 0 25 0 1 0 480296792 35168256 7980 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8586 7980 603 41 0 8545 0
vsize: 34344
[startup+310.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27016
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 12550 0 0 0 30922 76 0 0 25 0 1 0 480296792 35987456 8142 4294967295 134512640 134672761 3221224560 3221222896 134603527 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8786 8142 603 41 0 8745 0
vsize: 35144
[startup+320.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27016
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 12550 0 0 0 31923 76 0 0 25 0 1 0 480296792 35168256 7980 4294967295 134512640 134672761 3221224560 3221223008 134643961 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8586 7980 603 41 0 8545 0
vsize: 34344
[startup+330.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27016
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 12552 0 0 0 32922 76 0 0 25 0 1 0 480296792 35168256 7982 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8586 7982 603 41 0 8545 0
vsize: 34344
[startup+340.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27016
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 17244 0 0 0 33901 98 0 0 25 0 1 0 480296792 50237440 10369 4294967295 134512640 134672761 3221224560 3221223008 134643548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12265 10369 603 41 0 12224 0
vsize: 49060
[startup+350.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27016
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 17339 0 0 0 34899 99 0 0 25 0 1 0 480296792 50638848 10464 4294967295 134512640 134672761 3221224560 3221223008 134643511 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12363 10464 603 41 0 12322 0
vsize: 49452
[startup+360.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27016
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 17363 0 0 0 35898 100 0 0 25 0 1 0 480296792 50655232 10454 4294967295 134512640 134672761 3221224560 3221223008 134643499 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12367 10454 603 41 0 12326 0
vsize: 49468
[startup+370.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27016
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 17363 0 0 0 36897 101 0 0 25 0 1 0 480296792 50556928 10453 4294967295 134512640 134672761 3221224560 3221223040 134541817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12343 10453 603 41 0 12302 0
vsize: 49372
[startup+380.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27016
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 17367 0 0 0 37896 102 0 0 25 0 1 0 480296792 50524160 10454 4294967295 134512640 134672761 3221224560 3221223008 134643719 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12335 10454 603 41 0 12294 0
vsize: 49340
[startup+390.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27016
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 17626 0 0 0 38896 103 0 0 25 0 1 0 480296792 51736576 10679 4294967295 134512640 134672761 3221224560 3221222896 134603548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12631 10679 603 41 0 12590 0
vsize: 50524
[startup+400.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27016
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 17627 0 0 0 39896 103 0 0 25 0 1 0 480296792 51736576 10680 4294967295 134512640 134672761 3221224560 3221223104 134621173 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12631 10680 603 41 0 12590 0
vsize: 50524
[startup+410.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27016
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 17640 0 0 0 40893 106 0 0 25 0 1 0 480296792 50470912 10458 4294967295 134512640 134672761 3221224560 3221223008 134643984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12322 10458 603 41 0 12281 0
vsize: 49288
[startup+420.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27016
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 17649 0 0 0 41893 107 0 0 25 0 1 0 480296792 50470912 10467 4294967295 134512640 134672761 3221224560 3221223008 134643565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12322 10467 603 41 0 12281 0
vsize: 49288
[startup+430.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27016
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 17649 0 0 0 42890 109 0 0 25 0 1 0 480296792 50470912 10467 4294967295 134512640 134672761 3221224560 3221223008 134643542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12322 10467 603 41 0 12281 0
vsize: 49288
[startup+440.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27016
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 17652 0 0 0 43889 110 0 0 25 0 1 0 480296792 50470912 10470 4294967295 134512640 134672761 3221224560 3221223008 134643580 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12322 10470 603 41 0 12281 0
vsize: 49288
[startup+450.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27016
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 17655 0 0 0 44889 110 0 0 25 0 1 0 480296792 50470912 10473 4294967295 134512640 134672761 3221224560 3221223008 134643548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12322 10473 603 41 0 12281 0
vsize: 49288
[startup+460.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27016
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 17897 0 0 0 45889 111 0 0 25 0 1 0 480296792 51716096 10703 4294967295 134512640 134672761 3221224560 3221222416 134566721 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12626 10703 603 41 0 12585 0
vsize: 50504
[startup+470.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27016
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 17897 0 0 0 46889 111 0 0 25 0 1 0 480296792 51716096 10703 4294967295 134512640 134672761 3221224560 3221223104 134621242 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12626 10703 603 41 0 12585 0
vsize: 50504
[startup+480.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27016
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 17897 0 0 0 47888 112 0 0 25 0 1 0 480296792 50565120 10502 4294967295 134512640 134672761 3221224560 3221223008 134643511 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12345 10502 603 41 0 12304 0
vsize: 49380
[startup+490.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27016
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 17897 0 0 0 48888 112 0 0 25 0 1 0 480296792 50565120 10502 4294967295 134512640 134672761 3221224560 3221223008 134643996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12345 10502 603 41 0 12304 0
vsize: 49380
[startup+500.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27016
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 17897 0 0 0 49887 114 0 0 25 0 1 0 480296792 50556928 10500 4294967295 134512640 134672761 3221224560 3221222744 1075352058 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12343 10500 603 41 0 12302 0
vsize: 49372
[startup+510.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27016
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 18098 0 0 0 50887 114 0 0 25 0 1 0 480296792 51773440 10701 4294967295 134512640 134672761 3221224560 3221223056 134606977 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12640 10701 603 41 0 12599 0
vsize: 50560
[startup+520.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27016
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 18098 0 0 0 51886 115 0 0 25 0 1 0 480296792 50556928 10500 4294967295 134512640 134672761 3221224560 3221223072 134638283 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12343 10500 603 41 0 12302 0
vsize: 49372
[startup+530.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27016
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 18098 0 0 0 52886 115 0 0 25 0 1 0 480296792 50556928 10500 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12343 10500 603 41 0 12302 0
vsize: 49372
[startup+540.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27016
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 18294 0 0 0 53885 116 0 0 25 0 1 0 480296792 50556928 10500 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12343 10500 603 41 0 12302 0
vsize: 49372
[startup+550.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27016
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 18297 0 0 0 54886 116 0 0 25 0 1 0 480296792 50556928 10503 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12343 10503 603 41 0 12302 0
vsize: 49372
[startup+560.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27018
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 18610 0 0 0 55885 117 0 0 25 0 1 0 480296792 51875840 10816 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12665 10816 603 41 0 12624 0
vsize: 50660
[startup+570.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27018
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 19073 0 0 0 56884 118 0 0 25 0 1 0 480296792 53866496 11279 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13151 11279 603 41 0 13110 0
vsize: 52604
[startup+571.474 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 27018
Raw data (stat): 27014 (minisat+) R 27013 20838 20837 0 -1 0 19073 0 0 0 56884 118 0 0 25 0 1 0 480296792 53866496 11279 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13151 11279 603 41 0 13110 0
vsize: 0

Child status: 30
Real time (s): 571.473
CPU time (s): 571.493
CPU user time (s): 570.262
CPU system time (s): 1.23081
CPU usage (%): 100.003
Max. virtual memory (Kb): 52604
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	62
#### END VERIFIER DATA ####