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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-pk1.opb
MD5SUMb6007187ad037f56a5e2b97a0b86cea8
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 5120
Optimality of the best value was proved NO
Number of terms in the objective function 20
Biggest coefficient in the objective function 524288
Number of bits for the biggest coefficient in the objective function 20
Sum of the numbers in the objective function 1048575
Number of bits of the sum of numbers in the objective function 20
Biggest number in a constraint 524288
Number of bits of the biggest number in a constraint 20
Biggest sum of numbers in a constraint 2421502
Number of bits of the biggest sum of numbers22
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1175.03
Number of variables675
Total number of constraints100
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)55
Number of constraints which are nor clauses,nor cardinality constraints45
Minimum length of a constraint1
Maximum length of a constraint95

Trace number 17973 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-04-21 12:56:39 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18751 boxname=wulflinc23 idbench=1443 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  b6007187ad037f56a5e2b97a0b86cea8  /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-pk1.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-pk1.opb
IDLAUNCH: 18751
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        207932 kB
Buffers:         31288 kB
Cached:         767356 kB
SwapCached:        492 kB
Active:         387884 kB
Inactive:       412880 kB
HighTotal:      131008 kB
HighFree:          280 kB
LowTotal:       903652 kB
LowFree:        207652 kB
SwapTotal:     2097136 kB
SwapFree:      2095852 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5224 kB
Slab:            20156 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 13:16:41 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 18751 7 1200.24 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 60 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###############
c   -- Clauses(.)/Splits(s): (none)
c ---[  58]---> Adder-cost: 358   maxlim: 1151871   bits: 22/21
c ---[  56]---> Adder-cost: 382   maxlim: 1183231   bits: 22/21
c ---[  54]---> Adder-cost: 338   maxlim: 1135231   bits: 22/21
c ---[  52]---> Adder-cost: 362   maxlim: 1185791   bits: 22/21
c ---[  50]---> Adder-cost: 360   maxlim: 1161855   bits: 22/21
c ---[  48]---> Adder-cost: 354   maxlim: 1184383   bits: 22/21
c ---[  46]---> Adder-cost: 362   maxlim: 1156479   bits: 22/21
c ---[  45]---> BDD-cost:   58
c ---[  44]---> BDD-cost:   58
c ---[  43]---> BDD-cost:   58
c ---[  42]---> BDD-cost:   58
c ---[  40]---> Adder-cost: 352   maxlim: 1176959   bits: 22/21
c ---[  39]---> BDD-cost:   58
c ---[  38]---> BDD-cost:   58
c ---[  37]---> BDD-cost:   58
c ---[  36]---> BDD-cost:   58
c ---[  35]---> BDD-cost:   58
c ---[  34]---> BDD-cost:   58
c ---[  33]---> BDD-cost:   58
c ---[  32]---> BDD-cost:   58
c ---[  31]---> BDD-cost:   58
c ---[  30]---> BDD-cost:   58
c ---[  28]---> Adder-cost: 368   maxlim: 1155967   bits: 22/21
c ---[  27]---> BDD-cost:   58
c ---[  26]---> BDD-cost:   58
c ---[  25]---> BDD-cost:   58
c ---[  24]---> BDD-cost:   58
c ---[  23]---> BDD-cost:   58
c ---[  22]---> BDD-cost:   58
c ---[  21]---> BDD-cost:   58
c ---[  20]---> BDD-cost:   58
c ---[  19]---> BDD-cost:   58
c ---[  18]---> BDD-cost:   58
c ---[  16]---> Adder-cost: 362   maxlim: 1178367   bits: 22/21
c ---[  15]---> BDD-cost:   58
c ---[  14]---> BDD-cost:   58
c ---[  13]---> BDD-cost:   58
c ---[  12]---> BDD-cost:   58
c ---[  11]---> BDD-cost:   58
c ---[  10]---> BDD-cost:   58
c ---[   8]---> Adder-cost: 374   maxlim: 1184767   bits: 22/21
c ---[   6]---> Adder-cost: 348   maxlim: 1169791   bits: 22/21
c ---[   4]---> Adder-cost: 352   maxlim: 1145087   bits: 22/21
c ---[   2]---> Adder-cost: 368   maxlim: 1171455   bits: 22/21
c ---[   0]---> Adder-cost: 384   maxlim: 1175295   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   39453   136875 |   13151       0        0     nan |  0.000 % |
c |       100 |   39447   136857 |   14466      99      387     3.9 |  8.290 % |
c |       250 |   39439   136831 |   15912     248     1467     5.9 |  8.303 % |
c |       475 |   39425   136787 |   17503     471     2953     6.3 |  8.327 % |
c |       812 |   39401   136709 |   19254     805     6605     8.2 |  8.364 % |
c |      1318 |   39303   136389 |   21179    1293    11310     8.7 |  8.523 % |
c |      2077 |   39272   136288 |   23297    2048    17663     8.6 |  8.572 % |
c |      3217 |   39045   135547 |   25627    3144    35150    11.2 |  8.953 % |
c |      4925 |   39022   135472 |   28190    4849    68728    14.2 |  8.989 % |
c |      7487 |   38936   135194 |   31009    7394   126289    17.1 |  9.137 % |
c ==============================================================================
c Found solution: 1032188
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11175 |   38568   133999 |   12856   10992   196903    17.9 |  9.137 % |
c |     11275 |   38568   133999 |   14141   11092   198350    17.9 |  9.782 % |
c |     11425 |   38568   133999 |   15555   11242   199569    17.8 |  9.782 % |
c ==============================================================================
c Found solution: 1031144
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11488 |   38562   133978 |   12854   11300   200581    17.8 |  9.782 % |
c ==============================================================================
c Found solution: 966644
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11582 |   38572   134012 |   12857   11394   202866    17.8 |  9.782 % |
c |     11682 |   38572   134012 |   14142   11494   204176    17.8 |  9.814 % |
c |     11835 |   38572   134012 |   15556   11647   208208    17.9 |  9.814 % |
c ==============================================================================
c Found solution: 704252
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11852 |   38585   134051 |   12861   11664   208446    17.9 |  9.814 % |
c ==============================================================================
c Found solution: 638444
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11943 |   38599   134091 |   12866   11755   210120    17.9 |  9.814 % |
c |     12043 |   38599   134091 |   14152   11855   211416    17.8 |  9.817 % |
c |     12193 |   38599   134091 |   15567   12005   214274    17.8 |  9.817 % |
c |     12418 |   38549   133927 |   17124   12218   217327    17.8 |  9.902 % |
c ==============================================================================
c Found solution: 634740
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12598 |   38563   133966 |   12854   12398   221123    17.8 |  9.902 % |
c |     12698 |   38555   133940 |   14139   12497   221914    17.8 |  9.916 % |
c |     12851 |   38528   133853 |   15553   12645   224342    17.7 |  9.965 % |
c |     13076 |   38505   133776 |   17108   12864   228674    17.8 | 10.001 % |
c ==============================================================================
c Found solution: 561404
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13248 |   38469   133643 |   12823   13023   230579    17.7 | 10.001 % |
c |     13349 |   38461   133617 |   14105   13123   231205    17.6 | 10.104 % |
c ==============================================================================
c Found solution: 536796
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13401 |   38470   133631 |   12823   13174   231808    17.6 | 10.104 % |
c |     13502 |   38470   133631 |   14105   13275   234073    17.6 | 10.119 % |
c |     13652 |   38470   133631 |   15515   13425   236300    17.6 | 10.119 % |
c |     13877 |   38470   133631 |   17067   13650   241990    17.7 | 10.119 % |
c ==============================================================================
c Found solution: 536776
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13899 |   38486   133668 |   12828   13672   242427    17.7 | 10.119 % |
c |     14000 |   38486   133668 |   14110    6937   104258    15.0 | 10.124 % |
c |     14150 |   38486   133668 |   15521    7087   105830    14.9 | 10.124 % |
c |     14375 |   38478   133642 |   17074    7311   108146    14.8 | 10.136 % |
c |     14712 |   38470   133616 |   18781    7647   113145    14.8 | 10.148 % |
c |     15218 |   38470   133616 |   20659    8153   120077    14.7 | 10.148 % |
c |     15977 |   38463   133593 |   22725    8910   142352    16.0 | 10.161 % |
c ==============================================================================
c Found solution: 405692
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16404 |   38139   132575 |   12713    9337   149986    16.1 | 10.161 % |
c ==============================================================================
c Found solution: 340164
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16492 |   38156   132615 |   12718    9425   151098    16.0 | 10.161 % |
c |     16593 |   38156   132615 |   13989    9526   152464    16.0 | 11.636 % |
c ==============================================================================
c Found solution: 274680
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16656 |   38169   132648 |   12723    9589   153561    16.0 | 11.636 % |
c |     16756 |   38169   132648 |   13995    9689   155118    16.0 | 11.641 % |
c ==============================================================================
c Found solution: 274612
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16786 |   38185   132686 |   12728    9719   155574    16.0 | 11.641 % |
c ==============================================================================
c Found solution: 274604
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16862 |   38201   132723 |   12733    9795   156532    16.0 | 11.641 % |
c |     16962 |   38201   132723 |   14006    9895   157987    16.0 | 11.646 % |
c ==============================================================================
c Found solution: 172180
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17097 |   37878   131716 |   12626   10028   160131    16.0 | 11.646 % |
c |     17198 |   37878   131716 |   13888   10129   161854    16.0 | 13.110 % |
c ==============================================================================
c Found solution: 99472
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17227 |   37551   130704 |   12517   10158   162238    16.0 | 13.110 % |
c |     17328 |   37551   130704 |   13768   10259   164222    16.0 | 14.576 % |
c |     17480 |   37551   130704 |   15145   10411   165899    15.9 | 14.576 % |
c |     17706 |   37543   130678 |   16660   10636   168693    15.9 | 14.588 % |
c ==============================================================================
c Found solution: 83156
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17801 |   37558   130713 |   12519   10731   170725    15.9 | 14.588 % |
c ==============================================================================
c Found solution: 73932
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17893 |   37572   130745 |   12524   10823   171950    15.9 | 14.588 % |
c ==============================================================================
c Found solution: 65716
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17979 |   37578   130758 |   12526   10909   173738    15.9 | 14.588 % |
c |     18079 |   37578   130758 |   13778   11009   174390    15.8 | 14.596 % |
c |     18229 |   37578   130758 |   15156   11159   176906    15.9 | 14.596 % |
c ==============================================================================
c Found solution: 65704
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18385 |   37592   130789 |   12530   11315   180045    15.9 | 14.596 % |
c |     18486 |   37592   130789 |   13783   11416   181776    15.9 | 14.599 % |
c |     18638 |   37592   130789 |   15161   11568   183341    15.8 | 14.599 % |
c ==============================================================================
c Found solution: 65676
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18678 |   37605   130817 |   12535   11608   184039    15.9 | 14.599 % |
c |     18778 |   37605   130817 |   13788   11708   185011    15.8 | 14.604 % |
c ==============================================================================
c Found solution: 65620
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18905 |   37617   130843 |   12539   11835   187961    15.9 | 14.604 % |
c ==============================================================================
c Found solution: 65556
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18941 |   37628   130866 |   12542   11871   188755    15.9 | 14.604 % |
c ==============================================================================
c Found solution: 65544
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19037 |   37640   130891 |   12546   11967   190163    15.9 | 14.604 % |
c |     19137 |   37640   130891 |   13800   12067   191420    15.9 | 14.628 % |
c |     19287 |   37640   130891 |   15180   12217   196847    16.1 | 14.628 % |
c ==============================================================================
c Found solution: 32980
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19349 |   37295   129827 |   12431   12269   198216    16.2 | 14.628 % |
c |     19450 |   37295   129827 |   13674   12370   200186    16.2 | 16.094 % |
c ==============================================================================
c Found solution: 32860
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19501 |   37306   129851 |   12435   12421   200695    16.2 | 16.094 % |
c ==============================================================================
c Found solution: 32856
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19573 |   37320   129882 |   12440   12493   202253    16.2 | 16.094 % |
c |     19674 |   37320   129882 |   13684   12594   205633    16.3 | 16.103 % |
c |     19824 |   37320   129882 |   15052   12744   212259    16.7 | 16.103 % |
c |     20049 |   37320   129882 |   16557   12969   218484    16.8 | 16.103 % |
c |     20387 |   37320   129882 |   18213   13307   226661    17.0 | 16.103 % |
c ==============================================================================
c Found solution: 32588
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> BDD-cost:    2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20763 |   36973   128829 |   12324   13675   236274    17.3 | 16.103 % |
c |     20863 |   36973   128829 |   13556   13775   237179    17.2 | 17.563 % |
c |     21013 |   36973   128829 |   14912   13925   240722    17.3 | 17.563 % |
c |     21239 |   36973   128829 |   16403   14151   245500    17.3 | 17.563 % |
c ==============================================================================
c Found solution: 27724
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21328 |   36980   128847 |   12326   14240   246885    17.3 | 17.563 % |
c |     21428 |   36980   128847 |   13558    7220   110151    15.3 | 17.566 % |
c |     21578 |   36980   128847 |   14914    7370   111696    15.2 | 17.566 % |
c |     21804 |   36980   128847 |   16405    7596   115686    15.2 | 17.566 % |
c ==============================================================================
c Found solution: 24652
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22104 |   36985   128859 |   12328    7896   120059    15.2 | 17.566 % |
c |     22205 |   36985   128859 |   13560    7997   123433    15.4 | 17.574 % |
c |     22356 |   36985   128859 |   14916    8148   126289    15.5 | 17.574 % |
c |     22583 |   36985   128859 |   16408    8375   132396    15.8 | 17.574 % |
c |     22922 |   36985   128859 |   18049    8714   142766    16.4 | 17.574 % |
c ==============================================================================
c Found solution: 21580
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    4
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23287 |   36992   128876 |   12330    9079   152398    16.8 | 17.574 % |
c |     23388 |   36992   128876 |   13563    9180   153672    16.7 | 17.576 % |
c |     23540 |   36992   128876 |   14919    9332   157066    16.8 | 17.576 % |
c |     23765 |   36992   128876 |   16411    9557   158745    16.6 | 17.576 % |
c ==============================================================================
c Found solution: 18760
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23933 |   37004   128904 |   12334    9725   162344    16.7 | 17.576 % |
c |     24035 |   37004   128904 |   13567    9827   165182    16.8 | 17.573 % |
c |     24186 |   36998   128886 |   14924    9977   167273    16.8 | 17.585 % |
c |     24411 |   36998   128886 |   16416   10202   171813    16.8 | 17.585 % |
c |     24748 |   36998   128886 |   18058   10539   179086    17.0 | 17.585 % |
c |     25255 |   36998   128886 |   19864   11046   193504    17.5 | 17.585 % |
c ==============================================================================
c Found solution: 18716
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25531 |   37010   128913 |   12336   11322   199943    17.7 | 17.585 % |
c |     25632 |   37010   128913 |   13569   11423   201393    17.6 | 17.584 % |
c |     25782 |   37010   128913 |   14926   11573   204007    17.6 | 17.584 % |
c |     26007 |   37010   128913 |   16419   11798   209459    17.8 | 17.584 % |
c |     26344 |   37010   128913 |   18061   12135   212641    17.5 | 17.584 % |
c ==============================================================================
c Found solution: 18712
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26671 |   37022   128940 |   12340   12462   218103    17.5 | 17.584 % |
c |     26771 |   37022   128940 |   13574   12562   219317    17.5 | 17.584 % |
c |     26923 |   37022   128940 |   14931   12714   221360    17.4 | 17.584 % |
c |     27149 |   37022   128940 |   16424   12940   225287    17.4 | 17.584 % |
c |     27486 |   37022   128940 |   18066   13277   236236    17.8 | 17.584 % |
c |     27993 |   37022   128940 |   19873   13784   249846    18.1 | 17.584 % |
c |     28753 |   37022   128940 |   21861   14544   272834    18.8 | 17.584 % |
c |     29892 |   37022   128940 |   24047   15683   313694    20.0 | 17.584 % |
c ==============================================================================
c Found solution: 17560
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30369 |   37034   128967 |   12344   16160   326003    20.2 | 17.584 % |
c |     30470 |   37034   128967 |   13578    8181   160913    19.7 | 17.583 % |
c |     30621 |   37034   128967 |   14936    8332   161936    19.4 | 17.583 % |
c |     30847 |   37034   128967 |   16429    8558   166492    19.5 | 17.583 % |
c |     31187 |   37034   128967 |   18072    8898   171342    19.3 | 17.583 % |
c |     31695 |   37034   128967 |   19880    9406   186433    19.8 | 17.583 % |
c |     32455 |   37034   128967 |   21868   10166   197541    19.4 | 17.583 % |
c ==============================================================================
c Found solution: 17556
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32804 |   37043   128987 |   12347   10515   206452    19.6 | 17.583 % |
c |     32906 |   37043   128987 |   13581   10617   208277    19.6 | 17.586 % |
c |     33059 |   37043   128987 |   14939   10770   212420    19.7 | 17.586 % |
c |     33286 |   37043   128987 |   16433   10997   217190    19.7 | 17.586 % |
c ==============================================================================
c Found solution: 17548
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33381 |   37052   129007 |   12350   11092   218887    19.7 | 17.586 % |
c |     33481 |   37052   129007 |   13585   11192   221019    19.7 | 17.590 % |
c |     33631 |   37052   129007 |   14943   11342   224205    19.8 | 17.590 % |
c |     33857 |   37052   129007 |   16437   11568   226882    19.6 | 17.590 % |
c |     34194 |   37052   129007 |   18081   11905   233133    19.6 | 17.590 % |
c |     34701 |   37052   129007 |   19889   12412   247672    20.0 | 17.590 % |
c |     35460 |   37052   129007 |   21878   13171   272707    20.7 | 17.590 % |
c |     36600 |   37052   129007 |   24066   14311   300343    21.0 | 17.590 % |
c ==============================================================================
c Found solution: 17080
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36791 |   37065   129037 |   12355   14502   302718    20.9 | 17.590 % |
c |     36893 |   37065   129037 |   13590    7353   137991    18.8 | 17.587 % |
c |     37043 |   37065   129037 |   14949    7503   141126    18.8 | 17.587 % |
c |     37268 |   37065   129037 |   16444    7728   145800    18.9 | 17.587 % |
c |     37605 |   37065   129037 |   18088    8065   154117    19.1 | 17.587 % |
c |     38113 |   37065   129037 |   19897    8573   170882    19.9 | 17.587 % |
c |     38873 |   37065   129037 |   21887    9333   191524    20.5 | 17.587 % |
c |     40013 |   37065   129037 |   24076   10473   232083    22.2 | 17.587 % |
c ==============================================================================
c Found solution: 16556
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41105 |   37069   129046 |   12356   11565   269434    23.3 | 17.587 % |
c |     41205 |   37069   129046 |   13591   11665   270352    23.2 | 17.595 % |
c |     41356 |   37069   129046 |   14950   11816   271963    23.0 | 17.595 % |
c |     41581 |   37069   129046 |   16445   12041   274207    22.8 | 17.595 % |
c ==============================================================================
c Found solution: 16540
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41908 |   37080   129070 |   12360   12368   280970    22.7 | 17.595 % |
c |     42008 |   37080   129070 |   13596   12468   281553    22.6 | 17.599 % |
c |     42158 |   37080   129070 |   14955   12618   283122    22.4 | 17.599 % |
c |     42383 |   37080   129070 |   16451   12843   288039    22.4 | 17.599 % |
c |     42721 |   37080   129070 |   18096   13181   297320    22.6 | 17.599 % |
c |     43229 |   37080   129070 |   19905   13689   311318    22.7 | 17.599 % |
c |     43988 |   37080   129070 |   21896   14448   329266    22.8 | 17.599 % |
c |     45127 |   37080   129070 |   24086   15587   369092    23.7 | 17.599 % |
c |     46836 |   37080   129070 |   26494   17296   446521    25.8 | 17.599 % |
c |     49399 |   37080   129070 |   29144   19859   536416    27.0 | 17.599 % |
c ==============================================================================
c Found solution: 16532
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     52024 |   37083   129077 |   12361   22484   633612    28.2 | 17.599 % |
c |     52125 |   37083   129077 |   13597   11343   344777    30.4 | 17.606 % |
c |     52276 |   37083   129077 |   14956   11494   346522    30.1 | 17.606 % |
c |     52501 |   37083   129077 |   16452   11719   348687    29.8 | 17.606 % |
c |     52838 |   37083   129077 |   18097   12056   359179    29.8 | 17.606 % |
c |     53345 |   37083   129077 |   19907   12563   368022    29.3 | 17.606 % |
c |     54104 |   37083   129077 |   21898   13322   389049    29.2 | 17.606 % |
c |     55243 |   37083   129077 |   24088   14461   439082    30.4 | 17.606 % |
c |     56951 |   37075   129051 |   26496   16168   484419    30.0 | 17.618 % |
c ==============================================================================
c Found solution: 16528
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     58026 |   37081   129064 |   12360   17243   521406    30.2 | 17.618 % |
c |     58126 |   37081   129064 |   13596    8722   218614    25.1 | 17.626 % |
c |     58276 |   37081   129064 |   14955    8872   220304    24.8 | 17.626 % |
c |     58502 |   37081   129064 |   16451    9098   222584    24.5 | 17.626 % |
c |     58840 |   37081   129064 |   18096    9436   228336    24.2 | 17.626 % |
c |     59346 |   37081   129064 |   19905    9942   237155    23.9 | 17.626 % |
c |     60107 |   37081   129064 |   21896   10703   252417    23.6 | 17.626 % |
c |     61246 |   37081   129064 |   24086   11842   270812    22.9 | 17.626 % |
c ==============================================================================
c Found solution: 16524
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     61928 |   37087   129077 |   12362   12524   292726    23.4 | 17.626 % |
c |     62030 |   37087   129077 |   13598   12626   294036    23.3 | 17.634 % |
c |     62180 |   37087   129077 |   14958   12776   296493    23.2 | 17.634 % |
c |     62405 |   37087   129077 |   16453   13001   301543    23.2 | 17.634 % |
c |     62743 |   37087   129077 |   18099   13339   308376    23.1 | 17.634 % |
c |     63249 |   37087   129077 |   19909   13845   326447    23.6 | 17.634 % |
c |     64008 |   37087   129077 |   21900   14604   343474    23.5 | 17.634 % |
c ==============================================================================
c Found solution: 16516
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     64239 |   37098   129101 |   12366   14835   349233    23.5 | 17.634 % |
c |     64340 |   37098   129101 |   13602    7519   135522    18.0 | 17.637 % |
c |     64491 |   37098   129101 |   14962    7670   137344    17.9 | 17.637 % |
c |     64716 |   37098   129101 |   16459    7895   139116    17.6 | 17.637 % |
c |     65053 |   37098   129101 |   18105    8232   143661    17.5 | 17.637 % |
c |     65560 |   37098   129101 |   19915    8739   155504    17.8 | 17.637 % |
c |     66319 |   37098   129101 |   21907    9498   176894    18.6 | 17.637 % |
c |     67459 |   37098   129101 |   24097   10638   210209    19.8 | 17.637 % |
c ==============================================================================
c Found solution: 16512
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     67937 |   37106   129118 |   12368   11116   222929    20.1 | 17.637 % |
c |     68039 |   37106   129118 |   13604   11218   223470    19.9 | 17.645 % |
c |     68190 |   37106   129118 |   14965   11369   224735    19.8 | 17.645 % |
c |     68415 |   37106   129118 |   16461   11594   227946    19.7 | 17.645 % |
c |     68757 |   37106   129118 |   18107   11936   236617    19.8 | 17.645 % |
c |     69263 |   37106   129118 |   19918   12442   247497    19.9 | 17.645 % |
c |     70023 |   37106   129118 |   21910   13202   269094    20.4 | 17.645 % |
c |     71162 |   37106   129118 |   24101   14341   303968    21.2 | 17.645 % |
c |     72871 |   37106   129118 |   26511   16050   386241    24.1 | 17.645 % |
c |     75433 |   37106   129118 |   29163   18612   465857    25.0 | 17.645 % |
c |     79278 |   37106   129118 |   32079   22457   615691    27.4 | 17.645 % |
c ==============================================================================
c Found solution: 16504
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     80824 |   37116   129140 |   12372   24003   664874    27.7 | 17.645 % |
c |     80925 |   37116   129140 |   13609   12103   379895    31.4 | 17.651 % |
c |     81077 |   37116   129140 |   14970   12255   381862    31.2 | 17.651 % |
c |     81302 |   37116   129140 |   16467   12480   383962    30.8 | 17.651 % |
c |     81640 |   37116   129140 |   18113   12818   389090    30.4 | 17.651 % |
c ==============================================================================
c Found solution: 16500
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     81961 |   37124   129157 |   12374   13139   395756    30.1 | 17.651 % |
c |     82061 |   37124   129157 |   13611   13239   397502    30.0 | 17.658 % |
c |     82211 |   37124   129157 |   14972   13389   400793    29.9 | 17.658 % |
c |     82436 |   37124   129157 |   16469   13614   408307    30.0 | 17.658 % |
c |     82773 |   37124   129157 |   18116   13951   412967    29.6 | 17.658 % |
c |     83279 |   37124   129157 |   19928   14457   426367    29.5 | 17.658 % |
c |     84039 |   37124   129157 |   21921   15217   441500    29.0 | 17.658 % |
c |     85178 |   37124   129157 |   24113   16356   466137    28.5 | 17.658 % |
c ==============================================================================
c Found solution: 16488
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86320 |   37134   129179 |   12378   17498   496049    28.3 | 17.658 % |
c |     86422 |   37134   129179 |   13615    8851   177064    20.0 | 17.664 % |
c |     86572 |   37134   129179 |   14977    9001   178882    19.9 | 17.664 % |
c |     86797 |   37134   129179 |   16475    9226   182559    19.8 | 17.664 % |
c |     87134 |   37134   129179 |   18122    9563   190029    19.9 | 17.664 % |
c |     87640 |   37134   129179 |   19934   10069   204014    20.3 | 17.664 % |
c |     88399 |   37134   129179 |   21928   10828   222616    20.6 | 17.664 % |
c |     89538 |   37134   129179 |   24121   11967   257753    21.5 | 17.664 % |
c |     91246 |   37134   129179 |   26533   13675   329656    24.1 | 17.664 % |
c |     93808 |   37134   129179 |   29186   16237   415390    25.6 | 17.664 % |
c ==============================================================================
c Found solution: 16460
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     93998 |   37137   129186 |   12379   16427   418344    25.5 | 17.664 % |
c |     94101 |   37137   129186 |   13616    8317   223723    26.9 | 17.672 % |
c |     94252 |   37137   129186 |   14978    8468   225189    26.6 | 17.672 % |
c |     94477 |   37137   129186 |   16476    8693   229024    26.3 | 17.672 % |
c |     94814 |   37137   129186 |   18124    9030   232250    25.7 | 17.672 % |
c |     95320 |   37137   129186 |   19936    9536   247973    26.0 | 17.672 % |
c |     96080 |   37137   129186 |   21930   10296   271482    26.4 | 17.672 % |
c ==============================================================================
c Found solution: 16452
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     96824 |   37147   129208 |   12382   11040   287820    26.1 | 17.672 % |
c |     96924 |   37147   129208 |   13620   11140   289151    26.0 | 17.677 % |
c |     97075 |   37147   129208 |   14982   11291   290270    25.7 | 17.677 % |
c |     97300 |   37147   129208 |   16480   11516   292592    25.4 | 17.677 % |
c |     97638 |   37147   129208 |   18128   11854   300238    25.3 | 17.677 % |
c |     98145 |   37147   129208 |   19941   12361   312304    25.3 | 17.677 % |
c |     98904 |   37147   129208 |   21935   13120   335137    25.5 | 17.677 % |
c |    100043 |   37147   129208 |   24129   14259   369429    25.9 | 17.677 % |
c ==============================================================================
c Found solution: 16448
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    100848 |   37156   129227 |   12385   15064   388932    25.8 | 17.677 % |
c |    100948 |   37156   129227 |   13623    7632   162216    21.3 | 17.685 % |
c |    101098 |   37156   129227 |   14985    7782   163545    21.0 | 17.685 % |
c |    101324 |   37156   129227 |   16484    8008   167343    20.9 | 17.685 % |
c |    101661 |   37156   129227 |   18132    8345   173989    20.8 | 17.685 % |
c |    102167 |   37156   129227 |   19946    8851   180335    20.4 | 17.685 % |
c |    102927 |   37156   129227 |   21940    9611   209049    21.8 | 17.685 % |
c |    104066 |   37156   129227 |   24134   10750   244016    22.7 | 17.685 % |
c |    105774 |   37156   129227 |   26548   12458   294409    23.6 | 17.685 % |
c |    108336 |   37156   129227 |   29203   15020   393656    26.2 | 17.685 % |
c |    112183 |   37156   129227 |   32123   18867   534476    28.3 | 17.685 % |
c |    117950 |   37156   129227 |   35335   24634   746317    30.3 | 17.685 % |
c ==============================================================================
c Found solution: 16432
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    122155 |   37167   129251 |   12389   28839   924422    32.1 | 17.685 % |
c |    122255 |   37167   129251 |   13627   13761   450156    32.7 | 17.690 % |
c |    122407 |   37167   129251 |   14990   13913   451277    32.4 | 17.690 % |
c |    122632 |   37167   129251 |   16489   14138   453496    32.1 | 17.690 % |
c |    122970 |   37167   129251 |   18138   14476   460020    31.8 | 17.690 % |
c |    123476 |   37167   129251 |   19952   14982   466466    31.1 | 17.690 % |
c |    124235 |   37167   129251 |   21947   15741   487091    30.9 | 17.690 % |
c |    125374 |   37167   129251 |   24142   16880   530976    31.5 | 17.690 % |
c |    127082 |   37167   129251 |   26556   18588   585597    31.5 | 17.690 % |
c |    129644 |   37167   129251 |   29212   21150   690971    32.7 | 17.690 % |
c ==============================================================================
c Found solution: 16424
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    131778 |   37176   129270 |   12392   23284   780446    33.5 | 17.690 % |
c |    131878 |   37176   129270 |   13631   11742   346045    29.5 | 17.698 % |
c |    132030 |   37176   129270 |   14994   11894   349496    29.4 | 17.698 % |
c |    132256 |   37176   129270 |   16493   12120   353012    29.1 | 17.698 % |
c |    132593 |   37176   129270 |   18143   12457   361084    29.0 | 17.698 % |
c |    133099 |   37176   129270 |   19957   12963   372419    28.7 | 17.698 % |
c |    133858 |   37176   129270 |   21953   13722   388704    28.3 | 17.698 % |
c |    134999 |   37176   129270 |   24148   14863   419339    28.2 | 17.698 % |
c |    136707 |   37176   129270 |   26563   16571   470190    28.4 | 17.698 % |
c ==============================================================================
c Found solution: 16420
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    137801 |   37189   129298 |   12396   17665   493443    27.9 | 17.698 % |
c |    137901 |   37189   129298 |   13635    8933   196444    22.0 | 17.702 % |
c |    138051 |   37189   129298 |   14999    9083   197983    21.8 | 17.702 % |
c |    138276 |   37189   129298 |   16499    9308   200764    21.6 | 17.702 % |
c |    138614 |   37189   129298 |   18148    9646   205320    21.3 | 17.702 % |
c |    139121 |   37189   129298 |   19963   10153   221440    21.8 | 17.702 % |
c |    139881 |   37189   129298 |   21960   10913   242466    22.2 | 17.702 % |
c ==============================================================================
c Found solution: 16416
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    140185 |   37199   129319 |   12399   11217   246808    22.0 | 17.702 % |
c |    140285 |   37199   129319 |   13638   11317   248756    22.0 | 17.709 % |
c |    140438 |   37199   129319 |   15002   11470   251430    21.9 | 17.709 % |
c |    140663 |   37199   129319 |   16503   11695   253215    21.7 | 17.709 % |
c |    141000 |   37199   129319 |   18153   12032   260135    21.6 | 17.709 % |
c |    141507 |   37199   129319 |   19968   12539   272302    21.7 | 17.709 % |
c |    142268 |   37199   129319 |   21965   13300   293345    22.1 | 17.709 % |
c |    143407 |   37199   129319 |   24162   14439   333700    23.1 | 17.709 % |
c |    145115 |   37199   129319 |   26578   16147   388140    24.0 | 17.709 % |
c |    147678 |   37199   129319 |   29236   18710   481688    25.7 | 17.709 % |
c ==============================================================================
c Found solution: 16404
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    149635 |   37208   129338 |   12402   20667   547986    26.5 | 17.709 % |
c |    149735 |   37208   129338 |   13642   10434   285878    27.4 | 17.717 % |
c |    149886 |   37208   129338 |   15006   10585   288320    27.2 | 17.717 % |
c |    150111 |   37208   129338 |   16507   10810   290318    26.9 | 17.717 % |
c ==============================================================================
c Found solution: 16400
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    150446 |   37217   129357 |   12405   11145   296350    26.6 | 17.717 % |
c |    150547 |   37217   129357 |   13645   11246   296868    26.4 | 17.725 % |
c |    150698 |   37217   129357 |   15010   11397   298085    26.2 | 17.725 % |
c |    150924 |   37217   129357 |   16511   11623   301344    25.9 | 17.725 % |
c |    151262 |   37217   129357 |   18162   11961   306553    25.6 | 17.725 % |
c ==============================================================================
c Found solution: 16396
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    151536 |   37226   129376 |   12408   12235   311840    25.5 | 17.725 % |
c |    151637 |   37226   129376 |   13648   12336   312692    25.3 | 17.732 % |
c |    151787 |   37226   129376 |   15013   12486   315825    25.3 | 17.732 % |
c |    152012 |   37226   129376 |   16515   12711   321417    25.3 | 17.732 % |
c |    152351 |   37226   129376 |   18166   13050   324455    24.9 | 17.732 % |
c |    152858 |   37226   129376 |   19983   13557   344295    25.4 | 17.732 % |
c |    153618 |   37226   129376 |   21981   14317   369718    25.8 | 17.732 % |
c |    154758 |   37226   129376 |   24179   15457   404991    26.2 | 17.732 % |
c |    156466 |   37226   129376 |   26597   17165   462502    26.9 | 17.732 % |
c |    159030 |   37226   129376 |   29257   19729   559359    28.4 | 17.732 % |
c |    162876 |   37226   129376 |   32183   23575   695271    29.5 | 17.732 % |
c ==============================================================================
c Found solution: 16392
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    163302 |   37236   129397 |   12412   24001   710398    29.6 | 17.732 % |
c |    163403 |   37236   129397 |   13653   12102   375489    31.0 | 17.740 % |
c |    163553 |   37236   129397 |   15018   12252   378297    30.9 | 17.740 % |
c |    163778 |   37236   129397 |   16520   12477   382979    30.7 | 17.740 % |
c |    164116 |   37236   129397 |   18172   12815   392084    30.6 | 17.740 % |
c |    164622 |   37236   129397 |   19989   13321   405149    30.4 | 17.740 % |
c |    165381 |   37236   129397 |   21988   14080   425880    30.2 | 17.740 % |
c |    166522 |   37236   129397 |   24187   15221   462219    30.4 | 17.740 % |
c |    168232 |   37236   129397 |   26606   16931   523100    30.9 | 17.740 % |
c ==============================================================================
c Found solution: 16388
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    168729 |   37245   129416 |   12415   17428   535342    30.7 | 17.740 % |
c |    168829 |   37245   129416 |   13656    8814   223158    25.3 | 17.748 % |
c |    168980 |   37245   129416 |   15022    8965   224506    25.0 | 17.748 % |
c |    169206 |   37245   129416 |   16524    9191   227224    24.7 | 17.748 % |
c |    169544 |   37245   129416 |   18176    9529   230639    24.2 | 17.748 % |
c |    170050 |   37245   129416 |   19994   10035   240382    24.0 | 17.748 % |
c |    170810 |   37245   129416 |   21993   10795   253811    23.5 | 17.748 % |
c |    171950 |   37245   129416 |   24193   11935   291963    24.5 | 17.748 % |
c |    173658 |   37245   129416 |   26612   13643   335777    24.6 | 17.748 % |
c ==============================================================================
c Found solution: 16384
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    175011 |   36855   128235 |   12285   14768   360577    24.4 | 17.748 % |
c |    175112 |   36855   128235 |   13513    7485   152865    20.4 | 19.185 % |
c |    175264 |   36855   128235 |   14864    7637   154943    20.3 | 19.185 % |
c |    175489 |   36855   128235 |   16351    7862   156487    19.9 | 19.185 % |
c |    175826 |   36855   128235 |   17986    8199   162426    19.8 | 19.185 % |
c |    176333 |   36855   128235 |   19785    8706   170420    19.6 | 19.185 % |
c ==============================================================================
c Found solution: 14440
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    176655 |   36862   128252 |   12287    9028   174326    19.3 | 19.185 % |
c |    176755 |   36862   128252 |   13515    9128   174905    19.2 | 19.190 % |
c |    176905 |   36862   128252 |   14867    9278   175770    18.9 | 19.190 % |
c |    177130 |   36862   128252 |   16353    9503   179131    18.8 | 19.190 % |
c |    177467 |   36862   128252 |   17989    9840   190451    19.4 | 19.190 % |
c |    177973 |   36862   128252 |   19788   10346   198780    19.2 | 19.190 % |
c ==============================================================================
c Found solution: 14416
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> BDD-cost:    6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    178422 |   36872   128276 |   12290   10795   209395    19.4 | 19.190 % |
c |    178523 |   36872   128276 |   13519   10896   211462    19.4 | 19.191 % |
c |    178674 |   36872   128276 |   14870   11047   217527    19.7 | 19.191 % |
c |    178899 |   36872   128276 |   16357   11272   220579    19.6 | 19.191 % |
c |    179236 |   36872   128276 |   17993   11609   229018    19.7 | 19.191 % |
c |    179744 |   36872   128276 |   19793   12117   243911    20.1 | 19.191 % |
c |    180503 |   36872   128276 |   21772   12876   265974    20.7 | 19.191 % |
c |    181642 |   36872   128276 |   23949   14015   302604    21.6 | 19.191 % |
c ==============================================================================
c Found solution: 14396
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    181832 |   36879   128293 |   12293   14205   305978    21.5 | 19.191 % |
c |    181932 |   36879   128293 |   13522    7203   143074    19.9 | 19.196 % |
c |    182084 |   36879   128293 |   14874    7355   144369    19.6 | 19.196 % |
c |    182309 |   36879   128293 |   16361    7580   146364    19.3 | 19.196 % |
c |    182647 |   36879   128293 |   17998    7918   152984    19.3 | 19.196 % |
c |    183153 |   36879   128293 |   19797    8424   164310    19.5 | 19.196 % |
c |    183914 |   36879   128293 |   21777    9185   188938    20.6 | 19.196 % |
c |    185054 |   36879   128293 |   23955   10325   219386    21.2 | 19.196 % |
c |    186762 |   36879   128293 |   26351   12033   273624    22.7 | 19.196 % |
c ==============================================================================
c Found solution: 14372
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    187174 |   36887   128312 |   12295   12445   283372    22.8 | 19.196 % |
c |    187274 |   36887   128312 |   13524   12545   283979    22.6 | 19.201 % |
c |    187425 |   36887   128312 |   14876   12696   285166    22.5 | 19.201 % |
c |    187650 |   36887   128312 |   16364   12921   288019    22.3 | 19.201 % |
c |    187987 |   36887   128312 |   18001   13258   295751    22.3 | 19.201 % |
c |    188494 |   36887   128312 |   19801   13765   305853    22.2 | 19.201 % |
c |    189255 |   36887   128312 |   21781   14526   325167    22.4 | 19.201 % |
c |    190397 |   36887   128312 |   23959   15668   369211    23.6 | 19.201 % |
c |    192106 |   36887   128312 |   26355   17377   421736    24.3 | 19.201 % |
c |    194669 |   36887   128312 |   28990   19940   502991    25.2 | 19.201 % |
c |    198513 |   36887   128312 |   31890   23784   654106    27.5 | 19.201 % |
c ==============================================================================
c Found solution: 14364
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> BDD-cost:    4
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    198667 |   36893   128327 |   12297   23938   657855    27.5 | 19.201 % |
c |    198768 |   36893   128327 |   13526   12070   353019    29.2 | 19.206 % |
c |    198918 |   36893   128327 |   14879   12220   355161    29.1 | 19.206 % |
c |    199143 |   36893   128327 |   16367   12445   361077    29.0 | 19.206 % |
c |    199483 |   36893   128327 |   18004   12785   367740    28.8 | 19.206 % |
c |    199989 |   36893   128327 |   19804   13291   380800    28.7 | 19.206 % |
c |    200748 |   36893   128327 |   21784   14050   403115    28.7 | 19.206 % |
c ==============================================================================
c Found solution: 12436
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    201574 |   36897   128337 |   12299   14876   425733    28.6 | 19.206 % |
c |    201674 |   36897   128337 |   13528    7538   188795    25.0 | 19.213 % |
c |    201824 |   36897   128337 |   14881    7688   194134    25.3 | 19.213 % |
c |    202049 |   36897   128337 |   16369    7913   195616    24.7 | 19.213 % |
c |    202387 |   36897   128337 |   18006    8251   200070    24.2 | 19.213 % |
c |    202893 |   36897   128337 |   19807    8757   213952    24.4 | 19.213 % |
c |    203652 |   36897   128337 |   21788    9516   230512    24.2 | 19.213 % |
c |    204791 |   36897   128337 |   23967   10655   267616    25.1 | 19.213 % |
c |    206499 |   36897   128337 |   26363   12363   312395    25.3 | 19.213 % |
c |    209062 |   36897   128337 |   29000   14926   405598    27.2 | 19.213 % |
c |    212907 |   36897   128337 |   31900   18771   563929    30.0 | 19.213 % |
c ==============================================================================
c Found solution: 12244
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    214381 |   36901   128350 |   12300   20245   602064    29.7 | 19.213 % |
c |    214481 |   36901   128350 |   13530   10223   307376    30.1 | 19.218 % |
c |    214631 |   36901   128350 |   14883   10373   310524    29.9 | 19.218 % |
c |    214858 |   36901   128350 |   16371   10600   314973    29.7 | 19.218 % |
c |    215195 |   36901   128350 |   18008   10937   321760    29.4 | 19.218 % |
c |    215701 |   36901   128350 |   19809   11443   336383    29.4 | 19.218 % |
c |    216460 |   36901   128350 |   21790   12202   361696    29.6 | 19.218 % |
c |    217601 |   36901   128350 |   23969   13343   391726    29.4 | 19.218 % |
c |    219310 |   36901   128350 |   26366   15052   458932    30.5 | 19.218 % |
c |    221873 |   36901   128350 |   29002   17615   533351    30.3 | 19.218 % |
c |    225717 |   36901   128350 |   31903   21459   677192    31.6 | 19.218 % |
c |    231483 |   36901   128350 |   35093   27225   903500    33.2 | 19.218 % |
c |    240133 |   36901   128350 |   38602   35875  1207393    33.7 | 19.218 % |
c ==============================================================================
c Found solution: 12056
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    251054 |   36905   128362 |   12301   19029   707928    37.2 | 19.218 % |
c |    251154 |   36905   128362 |   13531    9615   399827    41.6 | 19.223 % |
c |    251304 |   36905   128362 |   14884    9765   400766    41.0 | 19.223 % |
c |    251529 |   36905   128362 |   16372    9990   404148    40.5 | 19.223 % |
c |    251866 |   36905   128362 |   18009   10327   410501    39.8 | 19.223 % |
c |    252372 |   36905   128362 |   19810   10833   421508    38.9 | 19.223 % |
c |    253132 |   36905   128362 |   21791   11593   431597    37.2 | 19.223 % |
c |    254272 |   36905   128362 |   23971   12733   462355    36.3 | 19.223 % |
c |    255980 |   36905   128362 |   26368   14441   509608    35.3 | 19.223 % |
c |    258542 |   36905   128362 |   29005   17003   595474    35.0 | 19.223 % |
c |    262386 |   36905   128362 |   31905   20847   753217    36.1 | 19.223 % |
c |    268153 |   36905   128362 |   35096   26614   997642    37.5 | 19.223 % |
c |    276802 |   36905   128362 |   38605   35263  1395701    39.6 | 19.223 % |
c |    289776 |   36905   128362 |   42466   21599   864327    40.0 | 19.223 % |
c |    309238 |   36905   128362 |   46713   41061  1743143    42.5 | 19.223 % |
c ==============================================================================
c Found solution: 11880
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    321874 |   36912   128380 |   12304   18678   737848    39.5 | 19.223 % |
c |    321974 |   36912   128380 |   13534    9439   373711    39.6 | 19.226 % |
c |    322125 |   36912   128380 |   14887    9590   375513    39.2 | 19.226 % |
c |    322350 |   36912   128380 |   16376    9815   378184    38.5 | 19.226 % |
c |    322687 |   36912   128380 |   18014   10152   383033    37.7 | 19.226 % |
c |    323194 |   36912   128380 |   19815   10659   394533    37.0 | 19.226 % |
c |    323953 |   36912   128380 |   21797   11418   405347    35.5 | 19.226 % |
c |    325094 |   36912   128380 |   23977   12559   445184    35.4 | 19.226 % |
c |    326802 |   36912   128380 |   26374   14267   496900    34.8 | 19.226 % |
c |    329364 |   36912   128380 |   29012   16829   583024    34.6 | 19.226 % |
c |    333208 |   36912   128380 |   31913   20673   758338    36.7 | 19.226 % |
c |    338975 |   36912   128380 |   35104   26440  1020984    38.6 | 19.226 % |
c |    347625 |   36899   128339 |   38615   35088  1349595    38.5 | 19.249 % |
c |    360599 |   36899   128339 |   42476   21248   865775    40.7 | 19.249 % |
c |    380063 |   36899   128339 |   46724   40712  1669910    41.0 | 19.249 % |
c |    409255 |   36899   128339 |   51396   35718  1604764    44.9 | 19.249 % |
c |    453045 |   36899   128339 |   56536   40760  1826066    44.8 | 19.249 % |
c |    518729 |   36899   128339 |   62190   18010   733311    40.7 | 19.249 % |
c |    617256 |   36899   128339 |   68409   22685   885447    39.0 | 19.249 % |
c ==============================================================================
c Found solution: 11412
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    668801 |   36903   128349 |   12301   18414   672261    36.5 | 19.249 % |
c |    668903 |   36903   128349 |   13531    9309   324405    34.8 | 19.254 % |
c |    669054 |   36903   128349 |   14884    9460   326091    34.5 | 19.254 % |
c |    669279 |   36903   128349 |   16372    9685   328658    33.9 | 19.254 % |
c |    669616 |   36903   128349 |   18009   10022   335691    33.5 | 19.254 % |
c |    670122 |   36903   128349 |   19810   10528   345151    32.8 | 19.254 % |
c |    670882 |   36903   128349 |   21791   11288   362623    32.1 | 19.254 % |
c |    672021 |   36903   128349 |   23971   12427   400556    32.2 | 19.254 % |
c |    673729 |   36903   128349 |   26368   14135   449000    31.8 | 19.254 % |
c |    676292 |   36903   128349 |   29005   16698   546999    32.8 | 19.254 % |
c |    680136 |   36903   128349 |   31905   20542   674841    32.9 | 19.254 % |
c |    685903 |   36903   128349 |   35096   26309   906556    34.5 | 19.254 % |
c |    694552 |   36903   128349 |   38605   34958  1288612    36.9 | 19.254 % |
c |    707527 |   36903   128349 |   42466   20330   919538    45.2 | 19.254 % |
c ==============================================================================
c Found solution: 11404
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    710098 |   36907   128359 |   12302   22901  1007724    44.0 | 19.254 % |
c |    710199 |   36907   128359 |   13532   11552   475993    41.2 | 19.259 % |
c |    710349 |   36907   128359 |   14885   11702   477996    40.8 | 19.259 % |
c |    710576 |   36907   128359 |   16373   11929   480558    40.3 | 19.259 % |
c |    710913 |   36907   128359 |   18011   12266   489365    39.9 | 19.259 % |
c |    711419 |   36907   128359 |   19812   12772   496661    38.9 | 19.259 % |
c |    712180 |   36907   128359 |   21793   13533   517533    38.2 | 19.259 % |
c |    713320 |   36907   128359 |   23973   14673   552787    37.7 | 19.259 % |
c |    715028 |   36907   128359 |   26370   16381   611139    37.3 | 19.259 % |
c |    717592 |   36907   128359 |   29007   18945   698671    36.9 | 19.259 % |
c |    721436 |   36907   128359 |   31908   22789   877781    38.5 | 19.259 % |
c |    727203 |   36907   128359 |   35099   28556  1106335    38.7 | 19.259 % |
c |    735853 |   36907   128359 |   38608   37206  1535658    41.3 | 19.259 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -d_bit_7 -d_bit_6 d_bit_5 d_bit_4 -d_bit_3 -d_bit_2 -d_bit_1 d_bit0 -d_bit1 -d_bit2 d_bit3 d_bit4 -d_bit5 d_bit6 -d_bit7 -d_bit8 -d_bit9 -d_bit10 -d_bit11 -d_bit12 -X1_bit0 -X2_bit0 -X3_bit0 -X4_bit0 -X5_bit0 X6_bit0 -X7_bit0 X8_bit0 X9_bit0 -X10_bit0 X11_bit0 X12_bit0 X13_bit0 -X14_bit0 X15_bit0 X16_bit0 -X17_bit0 -X18_bit0 -X19_bit0 -X20_bit0 X21_bit0 X22_bit0 -X23_bit0 X24_bit0 X25_bit0 X26_bit0 -X27_bit0 -X28_bit0 X29_bit0 -X30_bit0 -X31_bit0 -X32_bit0 -X33_bit0 -X34_bit0 X35_bit0 X36_bit0 X37_bit0 -X38_bit0 -X39_bit0 X40_bit0 -X41_bit0 -X42_bit0 -X43_bit0 X44_bit0 -X45_bit0 -X46_bit0 X47_bit0 X48_bit0 -X49_bit0 -X50_bit0 X51_bit0 X52_bit0 -X53_bit0 -X54_bit0 X55_bit0 -S1_bit_7 -S1_bit_6 -S1_bit_5 -S1_bit_4 -S1_bit_3 -S1_bit_2 -S1_bit_1 -S1_bit0 -S1_bit1 -S1_bit2 -S1_bit3 -S1_bit4 -S1_bit5 -S1_bit6 -S1_bit7 -S1_bit8 -S1_bit9 -S1_bit10 -S1_bit11 -S1_bit12 -T1_bit_7 -T1_bit_6 -T1_bit_5 -T1_bit_4 -T1_bit_3 -T1_bit_2 -T1_bit_1 -T1_bit0 T1_bit1 T1_bit2 -T1_bit3 T1_bit4 -T1_bit5 T1_bit6 -T1_bit7 -T1_bit8 -T1_bit9 -T1_bit10 -T1_bit11 -T1_bit12 -S10_bit_7 -S10_bit_6 -S10_bit_5 -S10_bit_4 -S10_bit_3 -S10_bit_2 -S10_bit_1 -S10_bit0 -S10_bit1 -S10_bit2 -S10_bit3 -S10_bit4 S10_bit5 -S10_bit6 -S10_bit7 -S10_bit8 -S10_bit9 -S10_bit10 -S10_bit11 -S10_bit12 -T10_bit_7 -T10_bit_6 -T10_bit_5 -T10_bit_4 -T10_bit_3 -T10_bit_2 -T10_bit_1 T10_bit0 -T10_bit1 -T10_bit2 -T10_bit3 T10_bit4 -T10_bit5 -T10_bit6 -T10_bit7 -T10_bit8 -T10_bit9 -T10_bit10 -T10_bit11 -T10_bit12 -S11_bit_7 -S11_bit_6 -S11_bit_5 -S11_bit_4 -S11_bit_3 -S11_bit_2 -S11_bit_1 S11_bit0 -S11_bit1 -S11_bit2 -S11_bit3 -S11_bit4 -S11_bit5 S11_bit6 -S11_bit7 -S11_bit8 -S11_bit9 -S11_bit10 -S11_bit11 -S11_bit12 -T11_bit_7 -T11_bit_6 -T11_bit_5 -T11_bit_4 -T11_bit_3 -T11_bit_2 -T11_bit_1 -T11_bit0 -T11_bit1 T11_bit2 -T11_bit3 -T11_bit4 -T11_bit5 -T11_bit6 -T11_bit7 -T11_bit8 -T11_bit9 -T11_bit10 -T11_bit11 -T11_bit12 -S12_bit_7 -S12_bit_6 -S12_bit_5 -S12_bit_4 -S12_bit_3 -S12_bit_2 -S12_bit_1 -S12_bit0 S12_bit1 -S12_bit2 -S12_bit3 -S12_bit4 -S12_bit5 -S12_bit6 -S12_bit7 -S12_bit8 -S12_bit9 -S12_bit10 -S12_bit11 -S12_bit12 -T12_bit_7 -T12_bit_6 -T12_bit_5 -T12_bit_4 -T12_bit_3 -T12_bit_2 -T12_bit_1 -T12_bit0 -T12_bit1 -T12_bit2 -T12_bit3 -T12_bit4 T12_bit5 -T12_bit6 -T12_bit7 -T12_bit8 -T12_bit9 -T12_bit10 -T12_bit11 -T12_bit12 -S13_bit_7 -S13_bit_6 -S13_bit_5 -S13_bit_4 -S13_bit_3 -S13_bit_2 -S13_bit_1 -S13_bit0 -S13_bit1 -S13_bit2 -S13_bit3 -S13_bit4 -S13_bit5 -S13_bit6 -S13_bit7 -S13_bit8 -S13_bit9 -S13_bit10 -S13_bit11 -S13_bit12 -T13_bit_7 -T13_bit_6 -T13_bit_5 -T13_bit_4 -T13_bit_3 -T13_bit_2 -T13_bit_1 -T13_bit0 T13_bit1 -T13_bit2 -T13_bit3 T13_bit4 -T13_bit5 T13_bit6 -T13_bit7 -T13_bit8 -T13_bit9 -T13_bit10 -T13_bit11 -T13_bit12 -S14_bit_7 -S14_bit_6 -S14_bit_5 -S14_bit_4 -S14_bit_3 -S14_bit_2 -S14_bit_1 -S14_bit0 S14_bit1 -S14_bit2 -S14_bit3 S14_bit4 -S14_bit5 -S14_bit6 -S14_bit7 -S14_bit8 -S14_bit9 -S14_bit10 -S14_bit11 -S14_bit12 -T14_bit_7 -T14_bit_6 -T14_bit_5 -T14_bit_4 -T14_bit_3 -T14_bit_2 -T14_bit_1 -T14_bit0 -T14_bit1 -T14_bit2 -T14_bit3 -T14_bit4 -T14_bit5 -T14_bit6 -T14_bit7 -T14_bit8 -T14_bit9 -T14_bit10 -T14_bit11 -T14_bit12 -S15_bit_7 -S15_bit_6 -S15_bit_5 -S15_bit_4 -S15_bit_3 -S15_bit_2 -S15_bit_1 S15_bit0 -S15_bit1 -S15_bit2 S15_bit3 S15_bit4 -S15_bit5 S15_bit6 -S15_bit7 -S15_bit8 -S15_bit9 -S15_bit10 -S15_bit11 -S15_bit12 -T15_bit_7 -T15_bit_6 -T15_bit_5 -T15_bit_4 -T15_bit_3 -T15_bit_2 -T15_bit_1 -T15_bit0 T15_bit1 T15_bit2 T15_bit3 -T15_bit4 -T15_bit5 -T15_bit6 -T15_bit7 -T15_bit8 -T15_bit9 -T15_bit10 -T15_bit11 -T15_bit12 -S2_bit_7 -S2_bit_6 -S2_bit_5 -S2_bit_4 -S2_bit_3 -S2_bit_2 -S2_bit_1 -S2_bit0 S2_bit1 -S2_bit2 -S2_bit3 -S2_bit4 -S2_bit5 -S2_bit6 -S2_bit7 -S2_bit8 -S2_bit9 -S2_bit10 -S2_bit11 -S2_bit12 -T2_bit_7 -T2_bit_6 -T2_bit_5 -T2_bit_4 -T2_bit_3 -T2_bit_2 -T2_bit_1 -T2_bit0 -T2_bit1 -T2_bit2 -T2_bit3 T2_bit4 -T2_bit5 T2_bit6 -T2_bit7 -T2_bit8 -T2_bit9 -T2_bit10 -T2_bit11 -T2_bit12 -S3_bit_7 -S3_bit_6 -S3_bit_5 -S3_bit_4 -S3_bit_3 -S3_bit_2 -S3_bit_1 S3_bit0 -S3_bit1 -S3_bit2 -S3_bit3 S3_bit4 S3_bit5 -#### 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 4543
Raw data (stat): 4543 (runsolver) R 4542 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545249870 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0012 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 1501 0 0 0 994 4 0 0 25 0 1 0 545249870 7757824 1476 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1894 1476 603 41 0 1853 0
vsize: 7576
[startup+20.0013 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 1639 0 0 0 1993 5 0 0 25 0 1 0 545249870 8634368 1614 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2108 1614 603 41 0 2067 0
vsize: 8432
[startup+30.0022 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 1789 0 0 0 2992 6 0 0 25 0 1 0 545249870 9306112 1764 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2272 1764 603 41 0 2231 0
vsize: 9088
[startup+40.0018 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 1973 0 0 0 3991 7 0 0 25 0 1 0 545249870 10047488 1948 4294967295 134512640 134672761 3221224624 3221223792 134560900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2453 1948 603 41 0 2412 0
vsize: 9812
[startup+50.0012 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2204 0 0 0 4991 7 0 0 25 0 1 0 545249870 10989568 2179 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2683 2179 603 41 0 2642 0
vsize: 10732
[startup+60.0011 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2204 0 0 0 5991 8 0 0 25 0 1 0 545249870 10989568 2179 4294967295 134512640 134672761 3221224624 3221223808 134559055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2683 2179 603 41 0 2642 0
vsize: 10732
[startup+70.0018 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2278 0 0 0 6990 8 0 0 25 0 1 0 545249870 11259904 2253 4294967295 134512640 134672761 3221224624 3221223840 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2749 2253 603 41 0 2708 0
vsize: 10996
[startup+80.0021 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2325 0 0 0 7990 8 0 0 25 0 1 0 545249870 11530240 2300 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2815 2300 603 41 0 2774 0
vsize: 11260
[startup+90.0021 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2325 0 0 0 8990 8 0 0 25 0 1 0 545249870 11530240 2300 4294967295 134512640 134672761 3221224624 3221223792 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2815 2300 603 41 0 2774 0
vsize: 11260
[startup+100.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2332 0 0 0 9990 8 0 0 25 0 1 0 545249870 11530240 2307 4294967295 134512640 134672761 3221224624 3221223792 134561139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2815 2307 603 41 0 2774 0
vsize: 11260
[startup+110.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2680 0 0 0 10989 9 0 0 25 0 1 0 545249870 12877824 2655 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3144 2655 603 41 0 3103 0
vsize: 12576
[startup+120.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2698 0 0 0 11989 10 0 0 25 0 1 0 545249870 13012992 2673 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3177 2673 603 41 0 3136 0
vsize: 12708
[startup+130.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2698 0 0 0 12989 10 0 0 25 0 1 0 545249870 13012992 2673 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3177 2673 603 41 0 3136 0
vsize: 12708
[startup+140.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2699 0 0 0 13990 10 0 0 25 0 1 0 545249870 13012992 2674 4294967295 134512640 134672761 3221224624 3221223792 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3177 2674 603 41 0 3136 0
vsize: 12708
[startup+150.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2699 0 0 0 14990 10 0 0 25 0 1 0 545249870 13012992 2674 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3177 2674 603 41 0 3136 0
vsize: 12708
[startup+160.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2699 0 0 0 15990 10 0 0 25 0 1 0 545249870 13012992 2674 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3177 2674 603 41 0 3136 0
vsize: 12708
[startup+170.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2699 0 0 0 16990 10 0 0 25 0 1 0 545249870 13012992 2674 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3177 2674 603 41 0 3136 0
vsize: 12708
[startup+180.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2699 0 0 0 17990 10 0 0 25 0 1 0 545249870 13012992 2674 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3177 2674 603 41 0 3136 0
vsize: 12708
[startup+190.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2699 0 0 0 18990 10 0 0 25 0 1 0 545249870 13012992 2674 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3177 2674 603 41 0 3136 0
vsize: 12708
[startup+200.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2699 0 0 0 19990 10 0 0 25 0 1 0 545249870 13012992 2674 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3177 2674 603 41 0 3136 0
vsize: 12708
[startup+210.004 s]
Raw data (loadavg): 1.07 0.98 0.91 2/54 4596
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2699 0 0 0 20990 10 0 0 25 0 1 0 545249870 13012992 2674 4294967295 134512640 134672761 3221224624 3221223792 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3177 2674 603 41 0 3136 0
vsize: 12708
[startup+220.004 s]
Raw data (loadavg): 1.06 0.98 0.91 2/54 4596
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2945 0 0 0 21989 11 0 0 25 0 1 0 545249870 13942784 2920 4294967295 134512640 134672761 3221224624 3221223824 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3404 2920 603 41 0 3363 0
vsize: 13616
[startup+230.004 s]
Raw data (loadavg): 1.05 0.98 0.91 2/54 4596
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3346 0 0 0 22988 13 0 0 25 0 1 0 545249870 15683584 3321 4294967295 134512640 134672761 3221224624 3221223792 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3829 3321 603 41 0 3788 0
vsize: 15316
[startup+240.005 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 4596
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3484 0 0 0 23988 13 0 0 25 0 1 0 545249870 16224256 3459 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3961 3459 603 41 0 3920 0
vsize: 15844
[startup+250.005 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 4596
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3484 0 0 0 24987 14 0 0 25 0 1 0 545249870 16224256 3459 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3961 3459 603 41 0 3920 0
vsize: 15844
[startup+260.005 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 4596
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3484 0 0 0 25987 15 0 0 25 0 1 0 545249870 16224256 3459 4294967295 134512640 134672761 3221224624 3221223800 134559059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3961 3459 603 41 0 3920 0
vsize: 15844
[startup+270.004 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 4596
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3484 0 0 0 26987 15 0 0 25 0 1 0 545249870 16224256 3459 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3961 3459 603 41 0 3920 0
vsize: 15844
[startup+280.005 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 4598
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3656 0 0 0 27986 16 0 0 25 0 1 0 545249870 17022976 3631 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4156 3631 603 41 0 4115 0
vsize: 16624
[startup+290.006 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 4598
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3709 0 0 0 28985 17 0 0 25 0 1 0 545249870 17158144 3684 4294967295 134512640 134672761 3221224624 3221223792 134564746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4189 3684 603 41 0 4148 0
vsize: 16756
[startup+300.006 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 4598
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3709 0 0 0 29985 17 0 0 25 0 1 0 545249870 17158144 3684 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4189 3684 603 41 0 4148 0
vsize: 16756
[startup+310.007 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 4598
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3709 0 0 0 30985 17 0 0 25 0 1 0 545249870 17158144 3684 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4189 3684 603 41 0 4148 0
vsize: 16756
[startup+320.007 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 4598
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3709 0 0 0 31985 18 0 0 25 0 1 0 545249870 17158144 3684 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4189 3684 603 41 0 4148 0
vsize: 16756
[startup+330.008 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 4598
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3981 0 0 0 32983 20 0 0 25 0 1 0 545249870 18366464 3956 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4484 3956 603 41 0 4443 0
vsize: 17936
[startup+340.008 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 4598
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4219 0 0 0 33982 21 0 0 25 0 1 0 545249870 19308544 4194 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4714 4194 603 41 0 4673 0
vsize: 18856
[startup+350.008 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4598
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4367 0 0 0 34981 22 0 0 25 0 1 0 545249870 19849216 4342 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4846 4342 603 41 0 4805 0
vsize: 19384
[startup+360.009 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4598
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4367 0 0 0 35981 22 0 0 25 0 1 0 545249870 19849216 4342 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4846 4342 603 41 0 4805 0
vsize: 19384
[startup+370.009 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4598
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4367 0 0 0 36981 23 0 0 25 0 1 0 545249870 19849216 4342 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4846 4342 603 41 0 4805 0
vsize: 19384
[startup+380.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4598
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4367 0 0 0 37981 23 0 0 25 0 1 0 545249870 19849216 4342 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4846 4342 603 41 0 4805 0
vsize: 19384
[startup+390.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4598
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4367 0 0 0 38981 24 0 0 25 0 1 0 545249870 19849216 4342 4294967295 134512640 134672761 3221224624 3221223764 134560629 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4846 4342 603 41 0 4805 0
vsize: 19384
[startup+400.009 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4598
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4367 0 0 0 39980 24 0 0 25 0 1 0 545249870 19849216 4342 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4846 4342 603 41 0 4805 0
vsize: 19384
[startup+410.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4598
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4367 0 0 0 40980 24 0 0 25 0 1 0 545249870 19849216 4342 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4846 4342 603 41 0 4805 0
vsize: 19384
[startup+420.009 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4598
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4367 0 0 0 41980 25 0 0 25 0 1 0 545249870 19849216 4342 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4846 4342 603 41 0 4805 0
vsize: 19384
[startup+430.009 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4598
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4367 0 0 0 42980 25 0 0 25 0 1 0 545249870 19849216 4342 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4846 4342 603 41 0 4805 0
vsize: 19384
[startup+440.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4598
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4367 0 0 0 43979 26 0 0 25 0 1 0 545249870 19849216 4342 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4846 4342 603 41 0 4805 0
vsize: 19384
[startup+450.009 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4598
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4367 0 0 0 44979 26 0 0 25 0 1 0 545249870 19849216 4342 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4846 4342 603 41 0 4805 0
vsize: 19384
[startup+460.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4598
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4433 0 0 0 45979 27 0 0 25 0 1 0 545249870 20111360 4408 4294967295 134512640 134672761 3221224624 3221223792 134561139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4910 4408 603 41 0 4869 0
vsize: 19640
[startup+470.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4598
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4550 0 0 0 46978 27 0 0 25 0 1 0 545249870 20639744 4525 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5039 4525 603 41 0 4998 0
vsize: 20156
[startup+480.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4598
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4553 0 0 0 47978 28 0 0 25 0 1 0 545249870 20639744 4528 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5039 4528 603 41 0 4998 0
vsize: 20156
[startup+490.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4598
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4560 0 0 0 48978 28 0 0 25 0 1 0 545249870 20639744 4535 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5039 4535 603 41 0 4998 0
vsize: 20156
[startup+500.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4598
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4567 0 0 0 49978 28 0 0 25 0 1 0 545249870 20774912 4542 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5072 4542 603 41 0 5031 0
vsize: 20288
[startup+510.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4598
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4573 0 0 0 50978 29 0 0 25 0 1 0 545249870 20774912 4548 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5072 4548 603 41 0 5031 0
vsize: 20288
[startup+520.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4573 0 0 0 51977 30 0 0 25 0 1 0 545249870 20774912 4548 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5072 4548 603 41 0 5031 0
vsize: 20288
[startup+530.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4612 0 0 0 52977 30 0 0 25 0 1 0 545249870 20910080 4587 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4587 603 41 0 5064 0
vsize: 20420
[startup+540.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4798 0 0 0 53976 31 0 0 25 0 1 0 545249870 21716992 4773 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5302 4773 603 41 0 5261 0
vsize: 21208
[startup+550.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4980 0 0 0 54976 31 0 0 25 0 1 0 545249870 22384640 4955 4294967295 134512640 134672761 3221224624 3221223728 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5465 4955 603 41 0 5424 0
vsize: 21860
[startup+560.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4980 0 0 0 55976 32 0 0 25 0 1 0 545249870 22384640 4955 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5465 4955 603 41 0 5424 0
vsize: 21860
[startup+570.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4980 0 0 0 56976 32 0 0 25 0 1 0 545249870 22384640 4955 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5465 4955 603 41 0 5424 0
vsize: 21860
[startup+580.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4980 0 0 0 57975 33 0 0 25 0 1 0 545249870 22384640 4955 4294967295 134512640 134672761 3221224624 3221223792 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5465 4955 603 41 0 5424 0
vsize: 21860
[startup+590.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4980 0 0 0 58975 33 0 0 25 0 1 0 545249870 22384640 4955 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5465 4955 603 41 0 5424 0
vsize: 21860
[startup+600.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4980 0 0 0 59975 34 0 0 25 0 1 0 545249870 22384640 4955 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5465 4955 603 41 0 5424 0
vsize: 21860
[startup+610.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4980 0 0 0 60974 34 0 0 25 0 1 0 545249870 22384640 4955 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5465 4955 603 41 0 5424 0
vsize: 21860
[startup+620.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4980 0 0 0 61974 35 0 0 25 0 1 0 545249870 22384640 4955 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5465 4955 603 41 0 5424 0
vsize: 21860
[startup+630.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4980 0 0 0 62974 35 0 0 25 0 1 0 545249870 22384640 4955 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5465 4955 603 41 0 5424 0
vsize: 21860
[startup+640.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5157 0 0 0 63973 36 0 0 25 0 1 0 545249870 23056384 5132 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5629 5132 603 41 0 5588 0
vsize: 22516
[startup+650.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5176 0 0 0 64973 37 0 0 25 0 1 0 545249870 23195648 5151 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5663 5151 603 41 0 5622 0
vsize: 22652
[startup+660.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5176 0 0 0 65972 37 0 0 25 0 1 0 545249870 23195648 5151 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5663 5151 603 41 0 5622 0
vsize: 22652
[startup+670.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5176 0 0 0 66972 38 0 0 25 0 1 0 545249870 23195648 5151 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5663 5151 603 41 0 5622 0
vsize: 22652
[startup+680.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5176 0 0 0 67972 38 0 0 25 0 1 0 545249870 23195648 5151 4294967295 134512640 134672761 3221224624 3221223792 134560785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5663 5151 603 41 0 5622 0
vsize: 22652
[startup+690.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5177 0 0 0 68972 39 0 0 25 0 1 0 545249870 23195648 5152 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5663 5152 603 41 0 5622 0
vsize: 22652
[startup+700.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5177 0 0 0 69971 39 0 0 25 0 1 0 545249870 23195648 5152 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5663 5152 603 41 0 5622 0
vsize: 22652
[startup+710.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5177 0 0 0 70971 40 0 0 25 0 1 0 545249870 23195648 5152 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5663 5152 603 41 0 5622 0
vsize: 22652
[startup+720.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5177 0 0 0 71971 40 0 0 25 0 1 0 545249870 23195648 5152 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5663 5152 603 41 0 5622 0
vsize: 22652
[startup+730.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5177 0 0 0 72971 40 0 0 25 0 1 0 545249870 23195648 5152 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5663 5152 603 41 0 5622 0
vsize: 22652
[startup+740.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5179 0 0 0 73970 41 0 0 25 0 1 0 545249870 23195648 5154 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5663 5154 603 41 0 5622 0
vsize: 22652
[startup+750.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5180 0 0 0 74970 41 0 0 25 0 1 0 545249870 23195648 5155 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5663 5155 603 41 0 5622 0
vsize: 22652
[startup+760.017 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5312 0 0 0 75970 42 0 0 25 0 1 0 545249870 23728128 5287 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5793 5287 603 41 0 5752 0
vsize: 23172
[startup+770.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5330 0 0 0 76969 43 0 0 25 0 1 0 545249870 23859200 5305 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5825 5305 603 41 0 5784 0
vsize: 23300
[startup+780.017 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5330 0 0 0 77969 43 0 0 25 0 1 0 545249870 23859200 5305 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5825 5305 603 41 0 5784 0
vsize: 23300
[startup+790.017 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5330 0 0 0 78969 44 0 0 25 0 1 0 545249870 23859200 5305 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5825 5305 603 41 0 5784 0
vsize: 23300
[startup+800.017 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5330 0 0 0 79968 44 0 0 25 0 1 0 545249870 23859200 5305 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5825 5305 603 41 0 5784 0
vsize: 23300
[startup+810.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5330 0 0 0 80968 45 0 0 25 0 1 0 545249870 23859200 5305 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5825 5305 603 41 0 5784 0
vsize: 23300
[startup+820.017 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5330 0 0 0 81968 45 0 0 25 0 1 0 545249870 23859200 5305 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5825 5305 603 41 0 5784 0
vsize: 23300
[startup+830.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5330 0 0 0 82968 45 0 0 25 0 1 0 545249870 23859200 5305 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5825 5305 603 41 0 5784 0
vsize: 23300
[startup+840.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5336 0 0 0 83967 46 0 0 25 0 1 0 545249870 23859200 5311 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5825 5311 603 41 0 5784 0
vsize: 23300
[startup+850.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5418 0 0 0 84967 47 0 0 25 0 1 0 545249870 24260608 5393 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5923 5393 603 41 0 5882 0
vsize: 23692
[startup+860.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5592 0 0 0 85965 48 0 0 25 0 1 0 545249870 24948736 5567 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6091 5567 603 41 0 6050 0
vsize: 24364
[startup+870.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5835 0 0 0 86964 49 0 0 25 0 1 0 545249870 26017792 5810 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6352 5810 603 41 0 6311 0
vsize: 25408
[startup+880.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5939 0 0 0 87964 50 0 0 25 0 1 0 545249870 26419200 5914 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6450 5914 603 41 0 6409 0
vsize: 25800
[startup+890.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5939 0 0 0 88964 51 0 0 25 0 1 0 545249870 26419200 5914 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6450 5914 603 41 0 6409 0
vsize: 25800
[startup+900.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5939 0 0 0 89963 51 0 0 25 0 1 0 545249870 26419200 5914 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6450 5914 603 41 0 6409 0
vsize: 25800
[startup+910.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5945 0 0 0 90963 52 0 0 25 0 1 0 545249870 26419200 5920 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6450 5920 603 41 0 6409 0
vsize: 25800
[startup+920.021 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5954 0 0 0 91963 52 0 0 25 0 1 0 545249870 26419200 5929 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6450 5929 603 41 0 6409 0
vsize: 25800
[startup+930.022 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5964 0 0 0 92963 52 0 0 25 0 1 0 545249870 26566656 5939 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6486 5939 603 41 0 6445 0
vsize: 25944
[startup+940.022 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5971 0 0 0 93963 53 0 0 25 0 1 0 545249870 26566656 5946 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6486 5946 603 41 0 6445 0
vsize: 25944
[startup+950.022 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5972 0 0 0 94963 53 0 0 25 0 1 0 545249870 26566656 5947 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6486 5947 603 41 0 6445 0
vsize: 25944
[startup+960.023 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5976 0 0 0 95963 53 0 0 25 0 1 0 545249870 26566656 5951 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6486 5951 603 41 0 6445 0
vsize: 25944
[startup+970.023 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5982 0 0 0 96962 54 0 0 25 0 1 0 545249870 26566656 5957 4294967295 134512640 134672761 3221224624 3221223728 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6486 5957 603 41 0 6445 0
vsize: 25944
[startup+980.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 5982 0 0 0 97962 55 0 0 25 0 1 0 545249870 26566656 5957 4294967295 134512640 134672761 3221224624 3221223792 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6486 5957 603 41 0 6445 0
vsize: 25944
[startup+990.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 6082 0 0 0 98961 56 0 0 25 0 1 0 545249870 26963968 6057 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6583 6057 603 41 0 6542 0
vsize: 26332
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 6082 0 0 0 99961 56 0 0 25 0 1 0 545249870 26963968 6057 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6583 6057 603 41 0 6542 0
vsize: 26332
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 6082 0 0 0 100960 57 0 0 25 0 1 0 545249870 26963968 6057 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6583 6057 603 41 0 6542 0
vsize: 26332
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 6082 0 0 0 101960 57 0 0 25 0 1 0 545249870 26963968 6057 4294967295 134512640 134672761 3221224624 3221223776 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6583 6057 603 41 0 6542 0
vsize: 26332
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 6082 0 0 0 102960 58 0 0 25 0 1 0 545249870 26963968 6057 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6583 6057 603 41 0 6542 0
vsize: 26332
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 6082 0 0 0 103960 58 0 0 25 0 1 0 545249870 26963968 6057 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6583 6057 603 41 0 6542 0
vsize: 26332
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 6082 0 0 0 104960 58 0 0 25 0 1 0 545249870 26963968 6057 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6583 6057 603 41 0 6542 0
vsize: 26332
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 6082 0 0 0 105959 59 0 0 25 0 1 0 545249870 26963968 6057 4294967295 134512640 134672761 3221224624 3221223792 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6583 6057 603 41 0 6542 0
vsize: 26332
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 6094 0 0 0 106959 60 0 0 25 0 1 0 545249870 27123712 6069 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6622 6069 603 41 0 6581 0
vsize: 26488
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 6094 0 0 0 107959 60 0 0 25 0 1 0 545249870 27123712 6069 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6622 6069 603 41 0 6581 0
vsize: 26488
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 6147 0 0 0 108958 61 0 0 25 0 1 0 545249870 27258880 6122 4294967295 134512640 134672761 3221224624 3221223792 134561121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6655 6122 603 41 0 6614 0
vsize: 26620
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 6414 0 0 0 109957 62 0 0 25 0 1 0 545249870 28602368 6389 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6983 6389 603 41 0 6942 0
vsize: 27932
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 6420 0 0 0 110957 63 0 0 25 0 1 0 545249870 28602368 6395 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6983 6395 603 41 0 6942 0
vsize: 27932
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 6420 0 0 0 111956 63 0 0 25 0 1 0 545249870 28602368 6395 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6983 6395 603 41 0 6942 0
vsize: 27932
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 6420 0 0 0 112956 64 0 0 25 0 1 0 545249870 28602368 6395 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6983 6395 603 41 0 6942 0
vsize: 27932
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 6420 0 0 0 113956 64 0 0 25 0 1 0 545249870 28602368 6395 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6983 6395 603 41 0 6942 0
vsize: 27932
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 6420 0 0 0 114956 64 0 0 25 0 1 0 545249870 28602368 6395 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6983 6395 603 41 0 6942 0
vsize: 27932
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 6420 0 0 0 115956 65 0 0 25 0 1 0 545249870 28602368 6395 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6983 6395 603 41 0 6942 0
vsize: 27932
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 6420 0 0 0 116955 65 0 0 25 0 1 0 545249870 28602368 6395 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6983 6395 603 41 0 6942 0
vsize: 27932
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 6420 0 0 0 117955 66 0 0 25 0 1 0 545249870 28602368 6395 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6983 6395 603 41 0 6942 0
vsize: 27932
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 6420 0 0 0 118955 66 0 0 25 0 1 0 545249870 28602368 6395 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6983 6395 603 41 0 6942 0
vsize: 27932
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4600
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 6420 0 0 0 119954 67 0 0 25 0 1 0 545249870 28602368 6395 4294967295 134512640 134672761 3221224624 3221223728 134560287 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6983 6395 603 41 0 6942 0
vsize: 27932
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.98 0.91 1/54 4600
Raw data (stat): 4543 (minisat+) Z 4542 3260 3259 0 -1 12 6423 0 0 0 119955 68 0 0 25 0 1 0 545249870 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.05
CPU time (s): 1200.24
CPU user time (s): 1199.55
CPU system time (s): 0.684895
CPU usage (%): 100.016
Max. virtual memory (Kb): 27932
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####