PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-neos5.opb
MD5SUM	4f5f6e30a602f3968daa9ca41c7da043
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2058
Optimality of the best value was proved	NO
Number of terms in the objective function	133
Biggest coefficient in the objective function	128
Number of bits for the biggest coefficient in the objective function	8
Sum of the numbers in the objective function	9334
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	1024
Number of bits of the biggest number in a constraint	11
Biggest sum of numbers in a constraint	9334
Number of bits of the biggest sum of numbers	14
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.05284
Number of variables	133
Total number of constraints	126
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	56
Number of constraints which are nor clauses,nor cardinality constraints	70
Minimum length of a constraint	1
Maximum length of a constraint	81
Trace number 14624

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-04-21 00:25:38 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19720 boxname=wulflinc5 idbench=1517 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4f5f6e30a602f3968daa9ca41c7da043  /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-neos5.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-neos5.opb /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-neos5.opb
IDLAUNCH: 19720
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        441360 kB
Buffers:         39272 kB
Cached:         528636 kB
SwapCached:       2272 kB
Active:         220176 kB
Inactive:       352868 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        441108 kB
SwapTotal:     2097136 kB
SwapFree:      2094864 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6940 kB
Slab:            14468 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 00:45:40 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 19720 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 73 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[  72]---> BDD-cost:    7
c ---[  71]---> BDD-cost:    7
c ---[  70]---> BDD-cost:    7
c ---[  69]---> BDD-cost:    7
c ---[  68]---> BDD-cost:    7
c ---[  67]---> BDD-cost:    7
c ---[  66]---> BDD-cost:    7
c ---[  65]---> BDD-cost:    7
c ---[  64]---> BDD-cost:    7
c ---[  63]---> BDD-cost:    7
c ---[  62]---> BDD-cost:  199
c ---[  61]---> BDD-cost:  309
c ---[  60]---> BDD-cost:  147
c ---[  59]---> BDD-cost:  579
c ---[  58]---> BDD-cost:  378
c ---[  57]---> BDD-cost:  147
c ---[  56]---> BDD-cost:  473
c ---[  55]---> BDD-cost:  378
c ---[  54]---> BDD-cost:  378
c ---[  53]---> BDD-cost:  147
c ---[  52]---> BDD-cost:  473
c ---[  51]---> BDD-cost:  100
c ---[  50]---> BDD-cost:  378
c ---[  49]---> BDD-cost:  471
c ---[  48]---> BDD-cost:  223
c ---[  47]---> BDD-cost:  174
c ---[  46]---> BDD-cost:  177
c ---[  45]---> BDD-cost:  129
c ---[  44]---> BDD-cost:  176
c ---[  43]---> BDD-cost:  177
c ---[  42]---> BDD-cost:  129
c ---[  41]---> BDD-cost:  176
c ---[  40]---> BDD-cost:  171
c ---[  39]---> BDD-cost:  129
c ---[  38]---> BDD-cost:  446
c ---[  37]---> BDD-cost:  176
c ---[  36]---> BDD-cost:  177
c ---[  35]---> BDD-cost:  129
c ---[  34]---> BDD-cost:  176
c ---[  33]---> BDD-cost:  129
c ---[  32]---> BDD-cost:  446
c ---[  31]---> BDD-cost:  177
c ---[  30]---> BDD-cost:  129
c ---[  29]---> BDD-cost:  173
c ---[  28]---> BDD-cost:  354
c ---[  27]---> BDD-cost:  446
c ---[  26]---> BDD-cost:  110
c ---[  25]---> BDD-cost:  110
c ---[  24]---> BDD-cost:  110
c ---[  23]---> BDD-cost:  150
c ---[  22]---> BDD-cost:  110
c ---[  21]---> BDD-cost:  110
c ---[  20]---> BDD-cost:  110
c ---[  19]---> BDD-cost:  150
c ---[  18]---> BDD-cost:  175
c ---[  17]---> BDD-cost:  110
c ---[  16]---> BDD-cost:  110
c ---[  15]---> BDD-cost:  150
c ---[  14]---> BDD-cost:  110
c ---[  13]---> BDD-cost:  150
c ---[  12]---> BDD-cost:  110
c ---[  11]---> BDD-cost:  328
c ---[  10]---> BDD-cost:   90
c ---[   9]---> BDD-cost:   90
c ---[   8]---> BDD-cost:   90
c ---[   7]---> BDD-cost:  175
c ---[   6]---> BDD-cost:   90
c ---[   5]---> BDD-cost:  122
c ---[   4]---> BDD-cost:   90
c ---[   3]---> BDD-cost:   69
c ---[   2]---> BDD-cost:  181
c ---[   1]---> BDD-cost:  193
c ---[   0]---> BDD-cost:  147
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   33911   100622 |   11303       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 3713[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 2729     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   38898   112283 |   12966       0        0     nan |  0.000 % |
c |       100 |   38898   112283 |   14262     100      915     9.2 |  0.492 % |
c ==============================================================================
c [1mFound solution: 2710[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       216 |   38991   112524 |   12997     216     1659     7.7 |  0.492 % |
c |       317 |   38991   112524 |   14296     317     2305     7.3 |  0.497 % |
c ==============================================================================
c [1mFound solution: 2578[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       431 |   39004   112564 |   13001     431     3130     7.3 |  0.497 % |
c |       531 |   39004   112564 |   14301     531     4162     7.8 |  0.503 % |
c ==============================================================================
c [1mFound solution: 2558[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       674 |   39012   112582 |   13004     674     5947     8.8 |  0.503 % |
c |       774 |   39012   112582 |   14304     774     7065     9.1 |  0.510 % |
c |       924 |   39012   112582 |   15734     924     8684     9.4 |  0.510 % |
c |      1149 |   39012   112582 |   17308    1149    11311     9.8 |  0.510 % |
c |      1487 |   39012   112582 |   19039    1487    16005    10.8 |  0.510 % |
c |      1993 |   39012   112582 |   20943    1993    22485    11.3 |  0.510 % |
c |      2754 |   39012   112582 |   23037    2754    32826    11.9 |  0.510 % |
c ==============================================================================
c [1mFound solution: 2534[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3128 |   39033   112638 |   13011    3128    38552    12.3 |  0.510 % |
c |      3229 |   39033   112638 |   14312    3229    39501    12.2 |  0.516 % |
c |      3379 |   39033   112638 |   15743    3379    40724    12.1 |  0.516 % |
c |      3605 |   39033   112638 |   17317    3605    46529    12.9 |  0.516 % |
c |      3942 |   39033   112638 |   19049    3942    51933    13.2 |  0.516 % |
c |      4449 |   39033   112638 |   20954    4449    58341    13.1 |  0.516 % |
c ==============================================================================
c [1mFound solution: 2277[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4742 |   39062   112717 |   13020    4742    62046    13.1 |  0.516 % |
c |      4842 |   39062   112717 |   14322    4842    63099    13.0 |  0.522 % |
c |      4993 |   39062   112717 |   15754    4993    64889    13.0 |  0.522 % |
c |      5221 |   39062   112717 |   17329    5221    67757    13.0 |  0.522 % |
c |      5560 |   39062   112717 |   19062    5560    71459    12.9 |  0.522 % |
c |      6067 |   39062   112717 |   20968    6067    80605    13.3 |  0.522 % |
c ==============================================================================
c [1mFound solution: 2226[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6796 |   39070   112741 |   13023    6796    88271    13.0 |  0.522 % |
c |      6898 |   39070   112741 |   14325    6898    90654    13.1 |  0.528 % |
c |      7048 |   39070   112741 |   15757    7048    92973    13.2 |  0.528 % |
c |      7273 |   39070   112741 |   17333    7273    95774    13.2 |  0.528 % |
c |      7611 |   39070   112741 |   19066    7611   101834    13.4 |  0.528 % |
c |      8118 |   39070   112741 |   20973    8118   111260    13.7 |  0.528 % |
c |      8877 |   39070   112741 |   23071    8877   127946    14.4 |  0.528 % |
c |     10016 |   39070   112741 |   25378   10016   153990    15.4 |  0.528 % |
c ==============================================================================
c [1mFound solution: 2214[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10839 |   39075   112753 |   13025   10839   168906    15.6 |  0.528 % |
c |     10940 |   39075   112753 |   14327   10940   172014    15.7 |  0.535 % |
c |     11090 |   39075   112753 |   15760   11090   176255    15.9 |  0.535 % |
c |     11315 |   39075   112753 |   17336   11315   180028    15.9 |  0.535 % |
c |     11653 |   39075   112753 |   19069   11653   185458    15.9 |  0.535 % |
c |     12160 |   39075   112753 |   20976   12160   201326    16.6 |  0.535 % |
c |     12920 |   39075   112753 |   23074   12920   219136    17.0 |  0.535 % |
c |     14059 |   39075   112753 |   25382   14059   250319    17.8 |  0.535 % |
c |     15769 |   39075   112753 |   27920   15769   295387    18.7 |  0.535 % |
c |     18331 |   39075   112753 |   30712   18331   382998    20.9 |  0.535 % |
c ==============================================================================
c [1mFound solution: 2198[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18608 |   39081   112766 |   13027   18608   389598    20.9 |  0.535 % |
c |     18708 |   39081   112766 |   14329    9404   219670    23.4 |  0.541 % |
c |     18859 |   39081   112766 |   15762    9555   222889    23.3 |  0.541 % |
c |     19085 |   39081   112766 |   17338    9781   228854    23.4 |  0.541 % |
c |     19423 |   39081   112766 |   19072   10119   239796    23.7 |  0.541 % |
c |     19929 |   39081   112766 |   20980   10625   256430    24.1 |  0.541 % |
c |     20689 |   39081   112766 |   23078   11385   273717    24.0 |  0.541 % |
c |     21828 |   39081   112766 |   25385   12524   308011    24.6 |  0.541 % |
c |     23536 |   39081   112766 |   27924   14232   329831    23.2 |  0.541 % |
c |     26098 |   39081   112766 |   30716   16794   446902    26.6 |  0.541 % |
c |     29944 |   39081   112766 |   33788   20640   593395    28.7 |  0.541 % |
c ==============================================================================
c [1mFound solution: 2197[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33488 |   39084   112773 |   13028   24153   662202    27.4 |  0.541 % |
c |     33588 |   39084   112773 |   14330   12177   326973    26.9 |  0.561 % |
c |     33738 |   39084   112773 |   15763   12327   328428    26.6 |  0.561 % |
c |     33964 |   39084   112773 |   17340   12553   331968    26.4 |  0.561 % |
c |     34302 |   39084   112773 |   19074   12891   338602    26.3 |  0.561 % |
c ==============================================================================
c [1mFound solution: 2194[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34788 |   39090   112786 |   13030   13377   355016    26.5 |  0.561 % |
c |     34889 |   39090   112786 |   14333    6790   105552    15.5 |  0.567 % |
c |     35039 |   39090   112786 |   15766    6940   109010    15.7 |  0.567 % |
c |     35264 |   39090   112786 |   17342    7165   112498    15.7 |  0.567 % |
c |     35602 |   39090   112786 |   19077    7503   123086    16.4 |  0.567 % |
c |     36109 |   39090   112786 |   20984    8010   133240    16.6 |  0.567 % |
c |     36868 |   39090   112786 |   23083    8769   151960    17.3 |  0.567 % |
c |     38007 |   39090   112786 |   25391    9908   173908    17.6 |  0.567 % |
c ==============================================================================
c [1mFound solution: 2182[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39387 |   39095   112797 |   13031   11288   199430    17.7 |  0.567 % |
c |     39488 |   39095   112797 |   14334   11389   201112    17.7 |  0.574 % |
c |     39638 |   39095   112797 |   15767   11539   203455    17.6 |  0.574 % |
c |     39863 |   39095   112797 |   17344   11764   206157    17.5 |  0.574 % |
c |     40200 |   39095   112797 |   19078   12101   213060    17.6 |  0.574 % |
c |     40707 |   39095   112797 |   20986   12608   221599    17.6 |  0.574 % |
c ==============================================================================
c [1mFound solution: 2181[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41064 |   39100   112808 |   13033   12965   225861    17.4 |  0.574 % |
c |     41164 |   39100   112808 |   14336   13065   228032    17.5 |  0.580 % |
c |     41315 |   39100   112808 |   15769   13216   229867    17.4 |  0.580 % |
c |     41540 |   39100   112808 |   17346   13441   232162    17.3 |  0.580 % |
c |     41879 |   39100   112808 |   19081   13780   239794    17.4 |  0.580 % |
c |     42385 |   39100   112808 |   20989   14286   250802    17.6 |  0.580 % |
c ==============================================================================
c [1mFound solution: 2180[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42464 |   39110   112835 |   13036   14365   251613    17.5 |  0.580 % |
c |     42564 |   39110   112835 |   14339    7283    94911    13.0 |  0.587 % |
c |     42714 |   39110   112835 |   15773    7433    97580    13.1 |  0.587 % |
c ==============================================================================
c [1mFound solution: 2179[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42773 |   39117   112851 |   13039    7492    98398    13.1 |  0.587 % |
c |     42873 |   39117   112851 |   14342    7592   100096    13.2 |  0.593 % |
c |     43023 |   39117   112851 |   15777    7742   103512    13.4 |  0.593 % |
c |     43249 |   39117   112851 |   17354    7968   106173    13.3 |  0.593 % |
c |     43587 |   39117   112851 |   19090    8306   111505    13.4 |  0.593 % |
c |     44093 |   39117   112851 |   20999    8812   127245    14.4 |  0.593 % |
c |     44852 |   39117   112851 |   23099    9571   140492    14.7 |  0.593 % |
c ==============================================================================
c [1mFound solution: 2178[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45190 |   39124   112867 |   13041    9909   145231    14.7 |  0.593 % |
c |     45290 |   39124   112867 |   14345   10009   146867    14.7 |  0.600 % |
c |     45441 |   39124   112867 |   15779   10160   150101    14.8 |  0.600 % |
c |     45666 |   39124   112867 |   17357   10385   153677    14.8 |  0.600 % |
c |     46004 |   39124   112867 |   19093   10723   160889    15.0 |  0.600 % |
c |     46510 |   39124   112867 |   21002   11229   172904    15.4 |  0.600 % |
c |     47270 |   39124   112867 |   23102   11989   194129    16.2 |  0.600 % |
c |     48409 |   39124   112867 |   25413   13128   230083    17.5 |  0.600 % |
c |     50117 |   39124   112867 |   27954   14836   265720    17.9 |  0.600 % |
c ==============================================================================
c [1mFound solution: 2118[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     51555 |   39133   112892 |   13044   16274   329483    20.2 |  0.600 % |
c |     51656 |   39133   112892 |   14348    8238   177098    21.5 |  0.606 % |
c |     51806 |   39133   112892 |   15783    8388   180206    21.5 |  0.606 % |
c |     52032 |   39133   112892 |   17361    8614   184942    21.5 |  0.606 % |
c |     52370 |   39133   112892 |   19097    8952   190096    21.2 |  0.606 % |
c |     52876 |   39133   112892 |   21007    9458   198770    21.0 |  0.606 % |
c |     53635 |   39133   112892 |   23108   10217   223410    21.9 |  0.606 % |
c |     54774 |   39133   112892 |   25419   11356   239738    21.1 |  0.606 % |
c |     56483 |   39133   112892 |   27960   13065   277316    21.2 |  0.606 % |
c |     59045 |   39133   112892 |   30757   15627   356100    22.8 |  0.606 % |
c |     62891 |   39133   112892 |   33832   19473   448248    23.0 |  0.606 % |
c ==============================================================================
c [1mFound solution: 2113[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     63186 |   39140   112908 |   13046   19768   453358    22.9 |  0.606 % |
c |     63286 |   39140   112908 |   14350    9984   197679    19.8 |  0.613 % |
c |     63436 |   39140   112908 |   15785   10134   201781    19.9 |  0.613 % |
c |     63661 |   39140   112908 |   17364   10359   205325    19.8 |  0.613 % |
c |     63998 |   39140   112908 |   19100   10696   210724    19.7 |  0.613 % |
c |     64507 |   39140   112908 |   21010   11205   228279    20.4 |  0.613 % |
c |     65266 |   39140   112908 |   23111   11964   241822    20.2 |  0.613 % |
c |     66410 |   39140   112908 |   25422   13108   269151    20.5 |  0.613 % |
c |     68119 |   39140   112908 |   27965   14817   326657    22.0 |  0.613 % |
c |     70681 |   39140   112908 |   30761   17379   373421    21.5 |  0.613 % |
c |     74525 |   39140   112908 |   33837   21223   458843    21.6 |  0.613 % |
c |     80292 |   39140   112908 |   37221   26990   707568    26.2 |  0.613 % |
c |     88941 |   39140   112908 |   40943   35639  1070103    30.0 |  0.613 % |
c ==============================================================================
c [1mFound solution: 2108[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     91101 |   39149   112929 |   13049   37799  1190486    31.5 |  0.613 % |
c |     91201 |   39149   112929 |   14353    7733   232503    30.1 |  0.619 % |
c |     91351 |   39147   112925 |   15789    7881   233984    29.7 |  0.626 % |
c |     91576 |   39147   112925 |   17368    8106   237486    29.3 |  0.626 % |
c |     91913 |   39147   112925 |   19105    8443   244004    28.9 |  0.626 % |
c |     92421 |   39147   112925 |   21015    8951   252559    28.2 |  0.626 % |
c |     93180 |   39147   112925 |   23117    9710   265335    27.3 |  0.626 % |
c |     94321 |   39147   112925 |   25428   10851   286293    26.4 |  0.626 % |
c |     96031 |   39147   112925 |   27971   12561   324430    25.8 |  0.626 % |
c |     98595 |   39147   112925 |   30768   15125   381915    25.3 |  0.626 % |
c ==============================================================================
c [1mFound solution: 2086[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     99390 |   39152   112936 |   13050   15920   392230    24.6 |  0.626 % |
c |     99490 |   39152   112936 |   14355    8060   123820    15.4 |  0.632 % |
c |     99641 |   39152   112936 |   15790    8211   126017    15.3 |  0.632 % |
c |     99866 |   39152   112936 |   17369    8436   128818    15.3 |  0.632 % |
c |    100203 |   39152   112936 |   19106    8773   135875    15.5 |  0.632 % |
c |    100710 |   39152   112936 |   21017    9280   144258    15.5 |  0.632 % |
c |    101469 |   39152   112936 |   23118   10039   157672    15.7 |  0.632 % |
c |    102609 |   39152   112936 |   25430   11179   178631    16.0 |  0.632 % |
c ==============================================================================
c [1mFound solution: 2084[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    104126 |   39159   112952 |   13053   12696   214227    16.9 |  0.632 % |
c |    104226 |   39159   112952 |   14358   12796   218101    17.0 |  0.638 % |
c |    104379 |   39159   112952 |   15794   12949   221494    17.1 |  0.638 % |
c |    104604 |   39159   112952 |   17373   13174   225818    17.1 |  0.638 % |
c |    104942 |   39159   112952 |   19110   13512   230644    17.1 |  0.638 % |
c |    105448 |   39159   112952 |   21021   14018   237233    16.9 |  0.638 % |
c |    106207 |   39159   112952 |   23124   14777   251872    17.0 |  0.638 % |
c |    107346 |   39159   112952 |   25436   15916   284816    17.9 |  0.638 % |
c ==============================================================================
c [1mFound solution: 2054[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    108040 |   39164   112963 |   13054   16610   296982    17.9 |  0.638 % |
c |    108140 |   39164   112963 |   14359    8405   125008    14.9 |  0.645 % |
c |    108291 |   39164   112963 |   15795    8556   128637    15.0 |  0.645 % |
c |    108516 |   39164   112963 |   17374    8781   134950    15.4 |  0.645 % |
c |    108855 |   39164   112963 |   19112    9120   141445    15.5 |  0.645 % |
c |    109363 |   39164   112963 |   21023    9628   154186    16.0 |  0.645 % |
c |    110122 |   39164   112963 |   23125   10387   168963    16.3 |  0.645 % |
c |    111261 |   39164   112963 |   25438   11526   199481    17.3 |  0.645 % |
c ==============================================================================
c [1mFound solution: 2053[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    112223 |   39170   112976 |   13056   12488   218124    17.5 |  0.645 % |
c |    112323 |   39170   112976 |   14361   12588   220064    17.5 |  0.651 % |
c |    112473 |   39170   112976 |   15797   12738   222376    17.5 |  0.651 % |
c ==============================================================================
c [1mFound solution: 2052[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    112587 |   39176   112989 |   13058   12852   224961    17.5 |  0.651 % |
c |    112688 |   39176   112989 |   14363   12953   227121    17.5 |  0.658 % |
c |    112838 |   39176   112989 |   15800   13103   231056    17.6 |  0.658 % |
c |    113063 |   39176   112989 |   17380   13328   236720    17.8 |  0.658 % |
c |    113401 |   39176   112989 |   19118   13666   242970    17.8 |  0.658 % |
c |    113908 |   39176   112989 |   21030   14173   248818    17.6 |  0.658 % |
c |    114668 |   39176   112989 |   23133   14933   259678    17.4 |  0.658 % |
c ==============================================================================
c [1mFound solution: 2051[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    115732 |   39183   113004 |   13061   15997   300594    18.8 |  0.658 % |
c |    115832 |   39183   113004 |   14367    8099   119026    14.7 |  0.664 % |
c |    115982 |   39183   113004 |   15803    8249   121516    14.7 |  0.664 % |
c |    116208 |   39183   113004 |   17384    8475   125658    14.8 |  0.664 % |
c |    116545 |   39183   113004 |   19122    8812   134437    15.3 |  0.664 % |
c |    117051 |   39183   113004 |   21034    9318   144441    15.5 |  0.664 % |
c |    117810 |   39183   113004 |   23138   10077   158441    15.7 |  0.664 % |
c |    118949 |   39183   113004 |   25452   11216   177286    15.8 |  0.664 % |
c |    120657 |   39183   113004 |   27997   12924   222332    17.2 |  0.664 % |
c ==============================================================================
c [1mFound solution: 2050[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    122005 |   39190   113019 |   13063   14272   264416    18.5 |  0.664 % |
c |    122105 |   39190   113019 |   14369    7236   118286    16.3 |  0.671 % |
c |    122255 |   39190   113019 |   15806    7386   120790    16.4 |  0.671 % |
c |    122480 |   39190   113019 |   17386    7611   124288    16.3 |  0.671 % |
c |    122818 |   39190   113019 |   19125    7949   127889    16.1 |  0.671 % |
c |    123325 |   39190   113019 |   21038    8456   136221    16.1 |  0.671 % |
c |    124086 |   39190   113019 |   23141    9217   163643    17.8 |  0.671 % |
c |    125225 |   39190   113019 |   25456   10356   191362    18.5 |  0.671 % |
c |    126933 |   39190   113019 |   28001   12064   237174    19.7 |  0.671 % |
c |    129495 |   39187   113012 |   30801   14509   347040    23.9 |  0.684 % |
c |    133343 |   39187   113012 |   33882   18357   531606    29.0 |  0.684 % |
c |    139109 |   39187   113012 |   37270   24123   755871    31.3 |  0.684 % |
c ==============================================================================
c [1mFound solution: 2049[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    144688 |   39192   113023 |   13064   29702   944308    31.8 |  0.684 % |
c |    144788 |   39192   113023 |   14370    7526   155241    20.6 |  0.690 % |
c |    144940 |   39192   113023 |   15807    7678   157505    20.5 |  0.690 % |
c |    145165 |   39192   113023 |   17388    7903   162421    20.6 |  0.690 % |
c |    145503 |   39192   113023 |   19127    8241   168934    20.5 |  0.690 % |
c |    146013 |   39192   113023 |   21039    8751   179552    20.5 |  0.690 % |
c |    146774 |   39192   113023 |   23143    9512   190278    20.0 |  0.690 % |
c |    147913 |   39190   113019 |   25458   10650   219684    20.6 |  0.697 % |
c |    149622 |   39190   113019 |   28003   12359   257758    20.9 |  0.697 % |
c |    152184 |   39190   113019 |   30804   14921   332505    22.3 |  0.697 % |
c |    156030 |   39190   113019 |   33884   18767   416429    22.2 |  0.697 % |
c |    161797 |   39190   113019 |   37273   24534   516462    21.1 |  0.697 % |
c ==============================================================================
c [1mFound solution: 2048[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    164737 |   39199   113039 |   13066   27474   601402    21.9 |  0.697 % |
c |    164837 |   39199   113039 |   14372    6969   110704    15.9 |  0.703 % |
c |    164989 |   39199   113039 |   15809    7121   112243    15.8 |  0.703 % |
c |    165214 |   39199   113039 |   17390    7346   116712    15.9 |  0.703 % |
c |    165551 |   39199   113039 |   19129    7683   124270    16.2 |  0.703 % |
c |    166058 |   39199   113039 |   21042    8190   131152    16.0 |  0.703 % |
c |    166817 |   39199   113039 |   23147    8949   146515    16.4 |  0.703 % |
c |    167956 |   39199   113039 |   25461   10088   173923    17.2 |  0.703 % |
c |    169665 |   39199   113039 |   28008   11797   221617    18.8 |  0.703 % |
c |    172227 |   39199   113039 |   30808   14359   304218    21.2 |  0.703 % |
c |    176071 |   39199   113039 |   33889   18203   409817    22.5 |  0.703 % |
c |    181838 |   39199   113039 |   37278   23970   535018    22.3 |  0.703 % |
c |    190487 |   39199   113039 |   41006   32619   809512    24.8 |  0.703 % |
c |    203461 |   39199   113039 |   45107   19849   514697    25.9 |  0.703 % |
c ==============================================================================
c [1mFound solution: 2022[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    219104 |   39215   113080 |   13071   35492  1638422    46.2 |  0.703 % |
c |    219206 |   39215   113080 |   14378    7685   342507    44.6 |  0.709 % |
c |    219356 |   39215   113080 |   15815    7835   345471    44.1 |  0.709 % |
c |    219584 |   39215   113080 |   17397    8063   348088    43.2 |  0.709 % |
c |    219922 |   39215   113080 |   19137    8401   357441    42.5 |  0.709 % |
c |    220428 |   39215   113080 |   21050    8907   366831    41.2 |  0.709 % |
c |    221187 |   39215   113080 |   23156    9666   380360    39.4 |  0.709 % |
c |    222326 |   39215   113080 |   25471   10805   400433    37.1 |  0.709 % |
c |    224035 |   39215   113080 |   28018   12514   458854    36.7 |  0.709 % |
c |    226597 |   39215   113080 |   30820   15076   511688    33.9 |  0.709 % |
c |    230442 |   39215   113080 |   33902   18921   595632    31.5 |  0.709 % |
c |    236208 |   39215   113080 |   37293   24687   716653    29.0 |  0.709 % |
c |    244857 |   39215   113080 |   41022   33336   956691    28.7 |  0.709 % |
c |    257832 |   39215   113080 |   45124   19491   624862    32.1 |  0.709 % |
c |    277293 |   39215   113080 |   49637   38952  1587769    40.8 |  0.709 % |
c |    306485 |   39215   113080 |   54600   32539   847118    26.0 |  0.709 % |
c ==============================================================================
c [1mFound solution: 2020[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    345044 |   39220   113096 |   13073   30496  1280501    42.0 |  0.709 % |
c |    345144 |   39220   113096 |   14380    7724   164218    21.3 |  0.716 % |
c |    345295 |   39220   113096 |   15818    7875   166112    21.1 |  0.716 % |
c |    345520 |   39220   113096 |   17400    8100   170123    21.0 |  0.716 % |
c |    345859 |   39220   113096 |   19140    8439   174731    20.7 |  0.716 % |
c |    346366 |   39220   113096 |   21054    8946   182386    20.4 |  0.716 % |
c |    347130 |   39215   113085 |   23159    9698   199767    20.6 |  0.735 % |
c |    348273 |   39215   113085 |   25475   10841   221330    20.4 |  0.735 % |
c |    349981 |   39215   113085 |   28023   12549   255128    20.3 |  0.735 % |
c |    352545 |   39215   113085 |   30825   15113   305897    20.2 |  0.735 % |
c |    356389 |   39215   113085 |   33907   18957   380955    20.1 |  0.735 % |
c |    362155 |   39215   113085 |   37298   24723   543954    22.0 |  0.735 % |
c |    370804 |   39215   113085 |   41028   33372   690051    20.7 |  0.735 % |
c |    383778 |   39215   113085 |   45131   20751   703195    33.9 |  0.735 % |
c |    403239 |   39215   113085 |   49644   40212  1938012    48.2 |  0.735 % |
c ==============================================================================
c [1mFound solution: 2019[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    413668 |   39221   113100 |   13073   18494   529233    28.6 |  0.735 % |
c |    413768 |   39221   113100 |   14380    9347   209360    22.4 |  0.742 % |
c |    413919 |   39221   113100 |   15818    9498   211857    22.3 |  0.742 % |
c |    414144 |   39221   113100 |   17400    9723   215991    22.2 |  0.742 % |
c |    414481 |   39221   113100 |   19140   10060   221556    22.0 |  0.742 % |
c |    414987 |   39221   113100 |   21054   10566   230833    21.8 |  0.742 % |
c |    415747 |   39221   113100 |   23159   11326   248579    21.9 |  0.742 % |
c |    416886 |   39221   113100 |   25475   12465   268279    21.5 |  0.742 % |
c |    418596 |   39221   113100 |   28023   14175   303062    21.4 |  0.742 % |
c |    421160 |   39221   113100 |   30825   16739   374019    22.3 |  0.742 % |
c |    425005 |   39221   113100 |   33907   20584   457277    22.2 |  0.742 % |
c |    430772 |   39221   113100 |   37298   26351   554524    21.0 |  0.742 % |
c |    439421 |   39221   113100 |   41028   35000  1026168    29.3 |  0.742 % |
c |    452396 |   39221   113100 |   45131   22551   990398    43.9 |  0.742 % |
c |    471857 |   39221   113100 |   49644   42012  2141032    51.0 |  0.742 % |
c |    501049 |   39221   113100 |   54609   35709  1166547    32.7 |  0.742 % |
c ==============================================================================
c [1mFound solution: 2018[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    516644 |   39227   113115 |   13075   51304  2106940    41.1 |  0.742 % |
c |    516744 |   39227   113115 |   14382    8377   255250    30.5 |  0.748 % |
c |    516895 |   39227   113115 |   15820    8528   258995    30.4 |  0.748 % |
c |    517124 |   39227   113115 |   17402    8757   265447    30.3 |  0.748 % |
c |    517461 |   39227   113115 |   19143    9094   272822    30.0 |  0.748 % |
c |    517969 |   39227   113115 |   21057    9602   284892    29.7 |  0.748 % |
c |    518729 |   39227   113115 |   23163   10362   299097    28.9 |  0.748 % |
c |    519869 |   39227   113115 |   25479   11502   336446    29.3 |  0.748 % |
c |    521578 |   39227   113115 |   28027   13211   387412    29.3 |  0.748 % |
c |    524141 |   39227   113115 |   30830   15774   452571    28.7 |  0.748 % |
c |    527987 |   39227   113115 |   33913   19620   556397    28.4 |  0.748 % |
c |    533753 |   39227   113115 |   37304   25386   762984    30.1 |  0.748 % |
c |    542402 |   39227   113115 |   41034   34035  1081862    31.8 |  0.748 % |
c ==============================================================================
c [1mFound solution: 2017[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    549661 |   39233   113130 |   13077   41294  1270505    30.8 |  0.748 % |
c |    549761 |   39233   113130 |   14384    8570   124264    14.5 |  0.754 % |
c |    549911 |   39233   113130 |   15823    8720   126840    14.5 |  0.754 % |
c |    550136 |   39233   113130 |   17405    8945   130346    14.6 |  0.754 % |
c |    550473 |   39233   113130 |   19146    9282   136791    14.7 |  0.754 % |
c |    550983 |   39233   113130 |   21060    9792   150415    15.4 |  0.754 % |
c |    551742 |   39233   113130 |   23166   10551   166685    15.8 |  0.754 % |
c |    552881 |   39233   113130 |   25483   11690   182816    15.6 |  0.754 % |
c |    554591 |   39233   113130 |   28031   13400   227750    17.0 |  0.754 % |
c |    557154 |   39233   113130 |   30834   15963   292954    18.4 |  0.754 % |
c |    560998 |   39233   113130 |   33918   19807   385678    19.5 |  0.754 % |
c |    566766 |   39233   113130 |   37310   25575   528204    20.7 |  0.754 % |
c |    575415 |   39233   113130 |   41041   34224   909593    26.6 |  0.754 % |
c |    588389 |   39233   113130 |   45145   18961   528667    27.9 |  0.754 % |
c |    607851 |   39233   113130 |   49659   38423  1022299    26.6 |  0.755 % |
c |    637044 |   39233   113130 |   54625   34500  1479658    42.9 |  0.754 % |
c |    680833 |   39233   113130 |   60088   38207  1141570    29.9 |  0.755 % |
c ==============================================================================
c [1mFound solution: 2016[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    712040 |   39239   113145 |   13079   23500   914500    38.9 |  0.755 % |
c |    712140 |   39239   113145 |   14386   11850   577102    48.7 |  0.761 % |
c |    712290 |   39239   113145 |   15825   12000   579032    48.3 |  0.761 % |
c |    712516 |   39239   113145 |   17408   12226   583747    47.7 |  0.761 % |
c |    712854 |   39239   113145 |   19148   12564   589558    46.9 |  0.761 % |
c |    713360 |   39239   113145 |   21063   13070   605699    46.3 |  0.761 % |
c |    714120 |   39239   113145 |   23170   13830   625085    45.2 |  0.761 % |
c |    715259 |   39239   113145 |   25487   14969   655852    43.8 |  0.761 % |
c |    716967 |   39239   113145 |   28035   16677   708245    42.5 |  0.761 % |
c |    719531 |   39239   113145 |   30839   19241   786345    40.9 |  0.761 % |
c |    723375 |   39239   113145 |   33923   23085   932446    40.4 |  0.761 % |
c |    729141 |   39239   113145 |   37315   28851  1125574    39.0 |  0.761 % |
c ==============================================================================
c [1mFound solution: 2006[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    736188 |   39245   113159 |   13081   35898  1371377    38.2 |  0.761 % |
c |    736288 |   39245   113159 |   14389    8356   107806    12.9 |  0.767 % |
c |    736438 |   39245   113159 |   15828    8506   110493    13.0 |  0.767 % |
c |    736664 |   39245   113159 |   17410    8732   114630    13.1 |  0.767 % |
c |    737003 |   39245   113159 |   19151    9071   119717    13.2 |  0.767 % |
c |    737510 |   39245   113159 |   21067    9578   129395    13.5 |  0.767 % |
c |    738269 |   39245   113159 |   23173   10337   151025    14.6 |  0.767 % |
c |    739408 |   39245   113159 |   25491   11476   183982    16.0 |  0.767 % |
c |    741117 |   39245   113159 |   28040   13185   240450    18.2 |  0.767 % |
c |    743680 |   39245   113159 |   30844   15748   321035    20.4 |  0.767 % |
c ==============================================================================
c [1mFound solution: 2005[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    746764 |   39251   113173 |   13083   18832   416684    22.1 |  0.767 % |
c |    746864 |   39251   113173 |   14391    9516   186005    19.5 |  0.774 % |
c |    747014 |   39251   113173 |   15830    9666   190248    19.7 |  0.774 % |
c |    747239 |   39251   113173 |   17413    9891   196259    19.8 |  0.774 % |
c |    747577 |   39251   113173 |   19154   10229   205501    20.1 |  0.774 % |
c |    748083 |   39251   113173 |   21070   10735   219323    20.4 |  0.774 % |
c |    748842 |   39251   113173 |   23177   11494   240973    21.0 |  0.774 % |
c ==============================================================================
c [1mFound solution: 1998[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    749443 |   39260   113194 |   13086   12095   263797    21.8 |  0.774 % |
c |    749544 |   39260   113194 |   14394   12196   266861    21.9 |  0.780 % |
c |    749695 |   39260   113194 |   15834   12347   271873    22.0 |  0.780 % |
c |    749920 |   39260   113194 |   17417   12572   275432    21.9 |  0.780 % |
c |    750257 |   39260   113194 |   19159   12909   279411    21.6 |  0.780 % |
c |    750763 |   39260   113194 |   21075   13415   285346    21.3 |  0.780 % |
c |    751522 |   39260   113194 |   23182   14174   305973    21.6 |  0.780 % |
c |    752661 |   39260   113194 |   25500   15313   331679    21.7 |  0.780 % |
c |    754369 |   39260   113194 |   28051   17021   360309    21.2 |  0.780 % |
c |    756932 |   39260   113194 |   30856   19584   442144    22.6 |  0.780 % |
c |    760778 |   39260   113194 |   33941   23430   557363    23.8 |  0.780 % |
c |    766544 |   39260   113194 |   37335   29196   737982    25.3 |  0.780 % |
c |    775193 |   39260   113194 |   41069   17046   406925    23.9 |  0.780 % |
c ==============================================================================
c [1mFound solution: 1996[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    781405 |   39269   113215 |   13089   23258   615788    26.5 |  0.780 % |
c |    781505 |   39269   113215 |   14397   11729   254937    21.7 |  0.786 % |
c |    781660 |   39269   113215 |   15837   11884   259362    21.8 |  0.786 % |
c |    781886 |   39269   113215 |   17421   12110   266809    22.0 |  0.786 % |
c |    782223 |   39269   113215 |   19163   12447   275155    22.1 |  0.786 % |
c |    782729 |   39269   113215 |   21079   12953   292925    22.6 |  0.786 % |
c |    783488 |   39269   113215 |   23187   13712   306853    22.4 |  0.786 % |
c |    784627 |   39269   113215 |   25506   14851   340029    22.9 |  0.786 % |
c |    786335 |   39269   113215 |   28057   16559   394345    23.8 |  0.786 % |
c |    788899 |   39269   113215 |   30863   19123   490108    25.6 |  0.786 % |
c |    792745 |   39269   113215 |   33949   22969   600146    26.1 |  0.786 % |
c |    798512 |   39269   113215 |   37344   28736   819817    28.5 |  0.786 % |
c |    807162 |   39269   113215 |   41078   37386  1106840    29.6 |  0.786 % |
c |    820136 |   39259   113193 |   45186   26222   712569    27.2 |  0.825 % |
c ==============================================================================
c [1mFound solution: 1995[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    831545 |   39268   113214 |   13089   37631  1257604    33.4 |  0.825 % |
c |    831646 |   39268   113214 |   14397    8371   284428    34.0 |  0.832 % |
c |    831796 |   39268   113214 |   15837    8521   287306    33.7 |  0.832 % |
c |    832021 |   39268   113214 |   17421    8746   292432    33.4 |  0.832 % |
c |    832358 |   39268   113214 |   19163    9083   299700    33.0 |  0.832 % |
c |    832865 |   39268   113214 |   21079    9590   313068    32.6 |  0.832 % |
c |    833624 |   39268   113214 |   23187   10349   329581    31.8 |  0.832 % |
c |    834763 |   39268   113214 |   25506   11488   356496    31.0 |  0.832 % |
c |    836471 |   39268   113214 |   28057   13196   407735    30.9 |  0.832 % |
c |    839034 |   39268   113214 |   30863   15759   484410    30.7 |  0.832 % |
c |    842878 |   39268   113214 |   33949   19603   590220    30.1 |  0.832 % |
c |    848645 |   39268   113214 |   37344   25370   777976    30.7 |  0.832 % |
c ==============================================================================
c [1mFound solution: 1994[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    853834 |   39277   113235 |   13092   30559   899600    29.4 |  0.832 % |
c |    853935 |   39277   113235 |   14401    7741    90993    11.8 |  0.838 % |
c |    854085 |   39277   113235 |   15841    7891    93905    11.9 |  0.838 % |
c |    854312 |   39277   113235 |   17425    8118   100603    12.4 |  0.838 % |
c |    854650 |   39277   113235 |   19167    8456   111345    13.2 |  0.838 % |
c |    855158 |   39277   113235 |   21084    8964   126635    14.1 |  0.838 % |
c |    855917 |   39277   113235 |   23193    9723   150345    15.5 |  0.838 % |
c |    857056 |   39277   113235 |   25512   10862   187597    17.3 |  0.838 % |
c |    858764 |   39277   113235 |   28063   12570   244480    19.4 |  0.838 % |
c |    861326 |   39277   113235 |   30870   15132   332740    22.0 |  0.838 % |
c |    865171 |   39277   113235 |   33957   18977   471211    24.8 |  0.838 % |
c |    870937 |   39277   113235 |   37353   24743   656602    26.5 |  0.838 % |
c |    879587 |   39277   113235 |   41088   33393   931635    27.9 |  0.838 % |
c |    892561 |   39277   113235 |   45197   19566   467043    23.9 |  0.838 % |
c |    912022 |   39277   113235 |   49716   39027   969843    24.9 |  0.838 % |
c |    941214 |   39277   113235 |   54688   36738   982641    26.7 |  0.838 % |
c |    985003 |   39277   113235 |   60157   42175  1106581    26.2 |  0.838 % |
c ==============================================================================
c [1mFound solution: 1993[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    995602 |   39286   113256 |   13095   52774  1721731    32.6 |  0.838 % |
c |    995704 |   39286   113256 |   14404    8775   378088    43.1 |  0.844 % |
c |    995856 |   39286   113256 |   15844    8927   382919    42.9 |  0.844 % |
c |    996083 |   39286   113256 |   17429    9154   388160    42.4 |  0.844 % |
c |    996420 |   39286   113256 |   19172    9491   397955    41.9 |  0.844 % |
c |    996926 |   39286   113256 |   21089    9997   415034    41.5 |  0.844 % |
c |    997685 |   39286   113256 |   23198   10756   439293    40.8 |  0.844 % |
c |    998824 |   39286   113256 |   25518   11895   482514    40.6 |  0.844 % |
c |   1000532 |   39286   113256 |   28070   13603   541679    39.8 |  0.844 % |
c |   1003094 |   39286   113256 |   30877   16165   621066    38.4 |  0.844 % |
c |   1006938 |   39286   113256 |   33965   20009   754003    37.7 |  0.844 % |
c |   1012704 |   39286   113256 |   37361   25775   954909    37.0 |  0.844 % |
c |   1021353 |   39286   113256 |   41097   34424  1287036    37.4 |  0.844 % |
#### 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.95 0.90 2/54 12941
Raw data (stat): 12941 (runsolver) R 12940 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 482522525 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0011 s]
Raw data (loadavg): 0.87 0.95 0.90 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 2051 0 0 0 994 4 0 0 25 0 1 0 482522525 10203136 2026 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2491 2026 603 41 0 2450 0
vsize: 9964
[startup+20.0023 s]
Raw data (loadavg): 0.89 0.95 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 2380 0 0 0 1992 6 0 0 25 0 1 0 482522525 11542528 2355 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2818 2355 603 41 0 2777 0
vsize: 11272
[startup+30.003 s]
Raw data (loadavg): 0.90 0.95 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 2486 0 0 0 2992 6 0 0 25 0 1 0 482522525 11948032 2461 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2917 2461 603 41 0 2876 0
vsize: 11668
[startup+40.0032 s]
Raw data (loadavg): 0.92 0.95 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 2486 0 0 0 3991 7 0 0 25 0 1 0 482522525 11948032 2461 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2917 2461 603 41 0 2876 0
vsize: 11668
[startup+50.0035 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 2486 0 0 0 4991 7 0 0 25 0 1 0 482522525 11948032 2461 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2917 2461 603 41 0 2876 0
vsize: 11668
[startup+60.0033 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 2827 0 0 0 5990 8 0 0 25 0 1 0 482522525 13287424 2802 4294967295 134512640 134672761 3221224544 3221223728 134558632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3244 2802 603 41 0 3203 0
vsize: 12976
[startup+70.0045 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 3235 0 0 0 6989 9 0 0 25 0 1 0 482522525 15015936 3210 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3666 3210 603 41 0 3625 0
vsize: 14664
[startup+80.0048 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 3236 0 0 0 7988 10 0 0 25 0 1 0 482522525 15015936 3211 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3666 3211 603 41 0 3625 0
vsize: 14664
[startup+90.0045 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 3237 0 0 0 8988 10 0 0 25 0 1 0 482522525 15015936 3212 4294967295 134512640 134672761 3221224544 3221223728 134558839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3666 3212 603 41 0 3625 0
vsize: 14664
[startup+100.005 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 3237 0 0 0 9988 10 0 0 25 0 1 0 482522525 15015936 3212 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3666 3212 603 41 0 3625 0
vsize: 14664
[startup+110.005 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 3237 0 0 0 10987 11 0 0 25 0 1 0 482522525 15015936 3212 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3666 3212 603 41 0 3625 0
vsize: 14664
[startup+120.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 3237 0 0 0 11987 11 0 0 25 0 1 0 482522525 15015936 3212 4294967295 134512640 134672761 3221224544 3221223692 134565030 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3666 3212 603 41 0 3625 0
vsize: 14664
[startup+130.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 3237 0 0 0 12987 11 0 0 25 0 1 0 482522525 15015936 3212 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3666 3212 603 41 0 3625 0
vsize: 14664
[startup+140.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 3237 0 0 0 13986 11 0 0 25 0 1 0 482522525 15015936 3212 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3666 3212 603 41 0 3625 0
vsize: 14664
[startup+150.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 3330 0 0 0 14986 11 0 0 25 0 1 0 482522525 15421440 3305 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3765 3305 603 41 0 3724 0
vsize: 15060
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 3358 0 0 0 15986 12 0 0 25 0 1 0 482522525 15556608 3333 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3798 3333 603 41 0 3757 0
vsize: 15192
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 3915 0 0 0 16985 13 0 0 25 0 1 0 482522525 17842176 3890 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4356 3890 603 41 0 4315 0
vsize: 17424
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 3928 0 0 0 17985 13 0 0 25 0 1 0 482522525 17842176 3903 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4356 3903 603 41 0 4315 0
vsize: 17424
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 3928 0 0 0 18985 13 0 0 25 0 1 0 482522525 17842176 3903 4294967295 134512640 134672761 3221224544 3221223680 134565149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4356 3903 603 41 0 4315 0
vsize: 17424
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 3928 0 0 0 19985 13 0 0 25 0 1 0 482522525 17842176 3903 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4356 3903 603 41 0 4315 0
vsize: 17424
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 3928 0 0 0 20985 13 0 0 25 0 1 0 482522525 17842176 3903 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4356 3903 603 41 0 4315 0
vsize: 17424
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 3928 0 0 0 21985 13 0 0 25 0 1 0 482522525 17842176 3903 4294967295 134512640 134672761 3221224544 3221223648 134560396 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4356 3903 603 41 0 4315 0
vsize: 17424
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 4187 0 0 0 22985 14 0 0 25 0 1 0 482522525 18911232 4162 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4617 4162 603 41 0 4576 0
vsize: 18468
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 4485 0 0 0 23984 15 0 0 25 0 1 0 482522525 20119552 4460 4294967295 134512640 134672761 3221224544 3221223648 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4912 4460 603 41 0 4871 0
vsize: 19648
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 4485 0 0 0 24984 15 0 0 25 0 1 0 482522525 20119552 4460 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4912 4460 603 41 0 4871 0
vsize: 19648
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 4485 0 0 0 25984 15 0 0 25 0 1 0 482522525 20119552 4460 4294967295 134512640 134672761 3221224544 3221223680 134565134 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4912 4460 603 41 0 4871 0
vsize: 19648
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 4485 0 0 0 26985 15 0 0 25 0 1 0 482522525 20119552 4460 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4912 4460 603 41 0 4871 0
vsize: 19648
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 4700 0 0 0 27984 16 0 0 25 0 1 0 482522525 21065728 4675 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5143 4675 603 41 0 5102 0
vsize: 20572
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5087 0 0 0 28983 17 0 0 25 0 1 0 482522525 22589440 5062 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5515 5062 603 41 0 5474 0
vsize: 22060
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5088 0 0 0 29983 17 0 0 25 0 1 0 482522525 22589440 5063 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5515 5063 603 41 0 5474 0
vsize: 22060
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5088 0 0 0 30983 17 0 0 25 0 1 0 482522525 22589440 5063 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5515 5063 603 41 0 5474 0
vsize: 22060
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5088 0 0 0 31983 17 0 0 25 0 1 0 482522525 22589440 5063 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5515 5063 603 41 0 5474 0
vsize: 22060
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5088 0 0 0 32984 17 0 0 25 0 1 0 482522525 22589440 5063 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5515 5063 603 41 0 5474 0
vsize: 22060
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5088 0 0 0 33984 17 0 0 25 0 1 0 482522525 22589440 5063 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5515 5063 603 41 0 5474 0
vsize: 22060
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5088 0 0 0 34984 17 0 0 25 0 1 0 482522525 22589440 5063 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5515 5063 603 41 0 5474 0
vsize: 22060
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5088 0 0 0 35984 17 0 0 25 0 1 0 482522525 22589440 5063 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5515 5063 603 41 0 5474 0
vsize: 22060
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5088 0 0 0 36984 17 0 0 25 0 1 0 482522525 22589440 5063 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5515 5063 603 41 0 5474 0
vsize: 22060
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5088 0 0 0 37984 17 0 0 25 0 1 0 482522525 22589440 5063 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5515 5063 603 41 0 5474 0
vsize: 22060
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5088 0 0 0 38985 17 0 0 25 0 1 0 482522525 22589440 5063 4294967295 134512640 134672761 3221224544 3221223680 134560611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5515 5063 603 41 0 5474 0
vsize: 22060
[startup+400.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5088 0 0 0 39985 17 0 0 25 0 1 0 482522525 22589440 5063 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5515 5063 603 41 0 5474 0
vsize: 22060
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5089 0 0 0 40985 17 0 0 25 0 1 0 482522525 22589440 5064 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5515 5064 603 41 0 5474 0
vsize: 22060
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5089 0 0 0 41985 17 0 0 25 0 1 0 482522525 22589440 5064 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5515 5064 603 41 0 5474 0
vsize: 22060
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5089 0 0 0 42985 17 0 0 25 0 1 0 482522525 22589440 5064 4294967295 134512640 134672761 3221224544 3221223680 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5515 5064 603 41 0 5474 0
vsize: 22060
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5089 0 0 0 43986 17 0 0 25 0 1 0 482522525 22589440 5064 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5515 5064 603 41 0 5474 0
vsize: 22060
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5089 0 0 0 44986 17 0 0 25 0 1 0 482522525 22589440 5064 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5515 5064 603 41 0 5474 0
vsize: 22060
[startup+460.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5089 0 0 0 45986 17 0 0 25 0 1 0 482522525 22589440 5064 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5515 5064 603 41 0 5474 0
vsize: 22060
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5164 0 0 0 46986 18 0 0 25 0 1 0 482522525 22994944 5139 4294967295 134512640 134672761 3221224544 3221223728 134559041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5614 5139 603 41 0 5573 0
vsize: 22456
[startup+480.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5289 0 0 0 47986 18 0 0 25 0 1 0 482522525 23400448 5264 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5713 5264 603 41 0 5672 0
vsize: 22852
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5308 0 0 0 48986 18 0 0 25 0 1 0 482522525 23547904 5283 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5749 5283 603 41 0 5708 0
vsize: 22996
[startup+500.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5320 0 0 0 49986 18 0 0 25 0 1 0 482522525 23547904 5295 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5749 5295 603 41 0 5708 0
vsize: 22996
[startup+510.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5326 0 0 0 50986 18 0 0 25 0 1 0 482522525 23687168 5301 4294967295 134512640 134672761 3221224544 3221223712 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5783 5301 603 41 0 5742 0
vsize: 23132
[startup+520.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5335 0 0 0 51986 18 0 0 25 0 1 0 482522525 23687168 5310 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5783 5310 603 41 0 5742 0
vsize: 23132
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5335 0 0 0 52986 18 0 0 25 0 1 0 482522525 23687168 5310 4294967295 134512640 134672761 3221224544 3221223712 134561133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5783 5310 603 41 0 5742 0
vsize: 23132
[startup+540.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5335 0 0 0 53986 18 0 0 25 0 1 0 482522525 23687168 5310 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5783 5310 603 41 0 5742 0
vsize: 23132
[startup+550.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5335 0 0 0 54986 18 0 0 25 0 1 0 482522525 23687168 5310 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5783 5310 603 41 0 5742 0
vsize: 23132
[startup+560.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5335 0 0 0 55986 18 0 0 25 0 1 0 482522525 23687168 5310 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5783 5310 603 41 0 5742 0
vsize: 23132
[startup+570.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5341 0 0 0 56986 18 0 0 25 0 1 0 482522525 23687168 5316 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5783 5316 603 41 0 5742 0
vsize: 23132
[startup+580.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5343 0 0 0 57987 18 0 0 25 0 1 0 482522525 23687168 5318 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5783 5318 603 41 0 5742 0
vsize: 23132
[startup+590.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5343 0 0 0 58987 18 0 0 25 0 1 0 482522525 23687168 5318 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5783 5318 603 41 0 5742 0
vsize: 23132
[startup+600.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5344 0 0 0 59986 19 0 0 25 0 1 0 482522525 23687168 5319 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5783 5319 603 41 0 5742 0
vsize: 23132
[startup+610.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5370 0 0 0 60986 19 0 0 25 0 1 0 482522525 23834624 5345 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5819 5345 603 41 0 5778 0
vsize: 23276
[startup+620.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5391 0 0 0 61987 19 0 0 25 0 1 0 482522525 24031232 5366 4294967295 134512640 134672761 3221224544 3221223648 134559929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5867 5366 603 41 0 5826 0
vsize: 23468
[startup+630.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5391 0 0 0 62987 19 0 0 25 0 1 0 482522525 24031232 5366 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5867 5366 603 41 0 5826 0
vsize: 23468
[startup+640.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5392 0 0 0 63987 19 0 0 25 0 1 0 482522525 24031232 5367 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5867 5367 603 41 0 5826 0
vsize: 23468
[startup+650.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5392 0 0 0 64987 19 0 0 25 0 1 0 482522525 24031232 5367 4294967295 134512640 134672761 3221224544 3221223696 134560074 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5867 5367 603 41 0 5826 0
vsize: 23468
[startup+660.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5392 0 0 0 65987 19 0 0 25 0 1 0 482522525 24031232 5367 4294967295 134512640 134672761 3221224544 3221223680 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5867 5367 603 41 0 5826 0
vsize: 23468
[startup+670.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5392 0 0 0 66987 19 0 0 25 0 1 0 482522525 24031232 5367 4294967295 134512640 134672761 3221224544 3221223744 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5867 5367 603 41 0 5826 0
vsize: 23468
[startup+680.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5414 0 0 0 67988 19 0 0 25 0 1 0 482522525 24031232 5389 4294967295 134512640 134672761 3221224544 3221223728 134558775 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5867 5389 603 41 0 5826 0
vsize: 23468
[startup+690.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5416 0 0 0 68988 19 0 0 25 0 1 0 482522525 24031232 5391 4294967295 134512640 134672761 3221224544 3221223728 134559540 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5867 5391 603 41 0 5826 0
vsize: 23468
[startup+700.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5416 0 0 0 69988 19 0 0 25 0 1 0 482522525 24031232 5391 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5867 5391 603 41 0 5826 0
vsize: 23468
[startup+710.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5425 0 0 0 70988 19 0 0 25 0 1 0 482522525 24227840 5400 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5915 5400 603 41 0 5874 0
vsize: 23660
[startup+720.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5425 0 0 0 71988 19 0 0 25 0 1 0 482522525 24227840 5400 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5915 5400 603 41 0 5874 0
vsize: 23660
[startup+730.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5425 0 0 0 72989 19 0 0 25 0 1 0 482522525 24227840 5400 4294967295 134512640 134672761 3221224544 3221223648 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5915 5400 603 41 0 5874 0
vsize: 23660
[startup+740.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5426 0 0 0 73989 19 0 0 25 0 1 0 482522525 24227840 5401 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5915 5401 603 41 0 5874 0
vsize: 23660
[startup+750.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5440 0 0 0 74989 19 0 0 25 0 1 0 482522525 24227840 5415 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5915 5415 603 41 0 5874 0
vsize: 23660
[startup+760.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5440 0 0 0 75989 19 0 0 25 0 1 0 482522525 24227840 5415 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5915 5415 603 41 0 5874 0
vsize: 23660
[startup+770.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5445 0 0 0 76989 19 0 0 25 0 1 0 482522525 24227840 5420 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5915 5420 603 41 0 5874 0
vsize: 23660
[startup+780.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5460 0 0 0 77989 19 0 0 25 0 1 0 482522525 24375296 5435 4294967295 134512640 134672761 3221224544 3221223648 134560174 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5951 5435 603 41 0 5910 0
vsize: 23804
[startup+790.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5460 0 0 0 78990 19 0 0 25 0 1 0 482522525 24375296 5435 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5951 5435 603 41 0 5910 0
vsize: 23804
[startup+800.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5461 0 0 0 79990 19 0 0 25 0 1 0 482522525 24375296 5436 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5951 5436 603 41 0 5910 0
vsize: 23804
[startup+810.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5461 0 0 0 80990 19 0 0 25 0 1 0 482522525 24375296 5436 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5951 5436 603 41 0 5910 0
vsize: 23804
[startup+820.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5461 0 0 0 81990 19 0 0 25 0 1 0 482522525 24375296 5436 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5951 5436 603 41 0 5910 0
vsize: 23804
[startup+830.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5483 0 0 0 82990 19 0 0 25 0 1 0 482522525 24375296 5458 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5951 5458 603 41 0 5910 0
vsize: 23804
[startup+840.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5524 0 0 0 83991 19 0 0 25 0 1 0 482522525 24702976 5499 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6031 5499 603 41 0 5990 0
vsize: 24124
[startup+850.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5524 0 0 0 84991 19 0 0 25 0 1 0 482522525 24702976 5499 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6031 5499 603 41 0 5990 0
vsize: 24124
[startup+860.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5524 0 0 0 85991 19 0 0 25 0 1 0 482522525 24702976 5499 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6031 5499 603 41 0 5990 0
vsize: 24124
[startup+870.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5524 0 0 0 86991 19 0 0 25 0 1 0 482522525 24702976 5499 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6031 5499 603 41 0 5990 0
vsize: 24124
[startup+880.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5525 0 0 0 87992 19 0 0 25 0 1 0 482522525 24702976 5500 4294967295 134512640 134672761 3221224544 3221223648 134560198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6031 5500 603 41 0 5990 0
vsize: 24124
[startup+890.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5543 0 0 0 88992 19 0 0 25 0 1 0 482522525 24702976 5518 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6031 5518 603 41 0 5990 0
vsize: 24124
[startup+900.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5543 0 0 0 89992 19 0 0 25 0 1 0 482522525 24702976 5518 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6031 5518 603 41 0 5990 0
vsize: 24124
[startup+910.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5543 0 0 0 90992 19 0 0 25 0 1 0 482522525 24702976 5518 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6031 5518 603 41 0 5990 0
vsize: 24124
[startup+920.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5543 0 0 0 91992 19 0 0 25 0 1 0 482522525 24702976 5518 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6031 5518 603 41 0 5990 0
vsize: 24124
[startup+930.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5543 0 0 0 92992 19 0 0 25 0 1 0 482522525 24702976 5518 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6031 5518 603 41 0 5990 0
vsize: 24124
[startup+940.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5543 0 0 0 93992 19 0 0 25 0 1 0 482522525 24702976 5518 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6031 5518 603 41 0 5990 0
vsize: 24124
[startup+950.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5554 0 0 0 94993 19 0 0 25 0 1 0 482522525 24899584 5529 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6079 5529 603 41 0 6038 0
vsize: 24316
[startup+960.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5569 0 0 0 95993 19 0 0 25 0 1 0 482522525 24899584 5544 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6079 5544 603 41 0 6038 0
vsize: 24316
[startup+970.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5575 0 0 0 96993 20 0 0 25 0 1 0 482522525 24899584 5550 4294967295 134512640 134672761 3221224544 3221223712 134561156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6079 5550 603 41 0 6038 0
vsize: 24316
[startup+980.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5590 0 0 0 97993 20 0 0 25 0 1 0 482522525 24899584 5565 4294967295 134512640 134672761 3221224544 3221223712 134561136 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6079 5565 603 41 0 6038 0
vsize: 24316
[startup+990.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5591 0 0 0 98993 20 0 0 25 0 1 0 482522525 24899584 5566 4294967295 134512640 134672761 3221224544 3221223712 134560785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6079 5566 603 41 0 6038 0
vsize: 24316
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5591 0 0 0 99993 20 0 0 25 0 1 0 482522525 24899584 5566 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6079 5566 603 41 0 6038 0
vsize: 24316
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5592 0 0 0 100993 20 0 0 25 0 1 0 482522525 24899584 5567 4294967295 134512640 134672761 3221224544 3221223680 134560640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6079 5567 603 41 0 6038 0
vsize: 24316
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5592 0 0 0 101995 20 0 0 25 0 1 0 482522525 24899584 5567 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6079 5567 603 41 0 6038 0
vsize: 24316
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5592 0 0 0 102996 20 0 0 25 0 1 0 482522525 24899584 5567 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6079 5567 603 41 0 6038 0
vsize: 24316
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5592 0 0 0 103996 20 0 0 25 0 1 0 482522525 24899584 5567 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6079 5567 603 41 0 6038 0
vsize: 24316
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5592 0 0 0 104996 20 0 0 25 0 1 0 482522525 24899584 5567 4294967295 134512640 134672761 3221224544 3221223648 134560326 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6079 5567 603 41 0 6038 0
vsize: 24316
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5602 0 0 0 105996 20 0 0 25 0 1 0 482522525 25096192 5577 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6127 5577 603 41 0 6086 0
vsize: 24508
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5609 0 0 0 106996 20 0 0 25 0 1 0 482522525 25096192 5584 4294967295 134512640 134672761 3221224544 3221223712 134561156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6127 5584 603 41 0 6086 0
vsize: 24508
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5628 0 0 0 107996 20 0 0 25 0 1 0 482522525 25096192 5603 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6127 5603 603 41 0 6086 0
vsize: 24508
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5647 0 0 0 108996 20 0 0 25 0 1 0 482522525 25292800 5622 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6175 5622 603 41 0 6134 0
vsize: 24700
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5667 0 0 0 109996 20 0 0 25 0 1 0 482522525 25292800 5642 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6175 5642 603 41 0 6134 0
vsize: 24700
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5667 0 0 0 110997 20 0 0 25 0 1 0 482522525 25292800 5642 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6175 5642 603 41 0 6134 0
vsize: 24700
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5671 0 0 0 111997 20 0 0 25 0 1 0 482522525 25292800 5646 4294967295 134512640 134672761 3221224544 3221223648 134560326 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6175 5646 603 41 0 6134 0
vsize: 24700
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5671 0 0 0 112997 20 0 0 25 0 1 0 482522525 25292800 5646 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6175 5646 603 41 0 6134 0
vsize: 24700
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5672 0 0 0 113997 20 0 0 25 0 1 0 482522525 25292800 5647 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6175 5647 603 41 0 6134 0
vsize: 24700
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5672 0 0 0 114997 20 0 0 25 0 1 0 482522525 25292800 5647 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6175 5647 603 41 0 6134 0
vsize: 24700
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5672 0 0 0 115998 20 0 0 25 0 1 0 482522525 25292800 5647 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6175 5647 603 41 0 6134 0
vsize: 24700
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5672 0 0 0 116998 20 0 0 25 0 1 0 482522525 25292800 5647 4294967295 134512640 134672761 3221224544 3221223712 134561115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6175 5647 603 41 0 6134 0
vsize: 24700
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5683 0 0 0 117998 20 0 0 25 0 1 0 482522525 25456640 5658 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6215 5658 603 41 0 6174 0
vsize: 24860
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5710 0 0 0 118997 21 0 0 25 0 1 0 482522525 25620480 5685 4294967295 134512640 134672761 3221224544 3221223648 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6255 5685 603 41 0 6214 0
vsize: 25020
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12941
Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5734 0 0 0 119998 21 0 0 25 0 1 0 482522525 25620480 5709 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6255 5709 603 41 0 6214 0
vsize: 25020
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 12941
Raw data (stat): 12941 (minisat+) Z 12940 24215 24214 0 -1 12 5737 0 0 0 119998 22 0 0 25 0 1 0 482522525 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.06
CPU time (s): 1200.21
CPU user time (s): 1199.98
CPU system time (s): 0.222966
CPU usage (%): 100.012
Max. virtual memory (Kb): 25020
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####