Some explanations

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

General information on the benchmark

Namemps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-afiro.opb
MD5SUM6cb229ab1cf181ca11759652604cb193
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -4121005
Optimality of the best value was proved NO
Number of terms in the objective function 150
Biggest coefficient in the objective function 134217728000
Number of bits for the biggest coefficient in the objective function 37
Sum of the numbers in the objective function 316753837785
Number of bits of the sum of numbers in the objective function 39
Biggest number in a constraint 1304059445248
Number of bits of the biggest number in a constraint 41
Biggest sum of numbers in a constraint 20964809094075
Number of bits of the biggest sum of numbers45
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.14
Number of variables960
Total number of constraints27
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints27
Minimum length of a constraint30
Maximum length of a constraint270

Trace number 2605

Launcher Data

LAUNCH ON wulflinc20 THE 2005-09-18 20:09:18 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2749 boxname=wulflinc20 idbench=405 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6cb229ab1cf181ca11759652604cb193  /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-afiro.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-afiro.opb
IDLAUNCH: 2749
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        906040 kB
Buffers:         35612 kB
Cached:          63720 kB
SwapCached:        832 kB
Active:          67388 kB
Inactive:        34612 kB
HighTotal:      131008 kB
HighFree:        63924 kB
LowTotal:       903652 kB
LowFree:        842116 kB
SwapTotal:     2097892 kB
SwapFree:      2096604 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5732 kB
Slab:            20988 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 20:29:28 (client local time) WITH STATUS 10 IN 1209.45 SECONDS
stats: 2749 7 1209.45 10

Solver Data

c Parsing PB file...
c Converting 35 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ########
c   -- Clauses(.)/Splits(s): ss
c ---[  35]---> BDD-cost:  145
c ---[  33]---> Sorter-cost: 1542     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2
c ---[  31]---> Sorter-cost: 1565     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  29]---> Adder-cost: 589   maxlim: 26214350   bits: 26/25
c ---[  27]---> Sorter-cost:  720     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  25]---> Sorter-cost: 1695     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2
c ---[  23]---> Adder-cost: 620   maxlim: 52428700   bits: 27/26
c ---[  21]---> Sorter-cost: 1982     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  20]---> BDD-cost:   16
c ---[  19]---> BDD-cost:   60
c ---[  18]---> BDD-cost:   52
c ---[  17]---> BDD-cost:   52
c ---[  16]---> BDD-cost:   52
c ---[  15]---> Sorter-cost: 1057     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5
c ---[  13]---> BDD-cost:   66
c ---[  12]---> BDD-cost:   52
c ---[  11]---> BDD-cost:   52
c ---[  10]---> BDD-cost:   52
c ---[   9]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5
c ---[   8]---> Adder-cost: 1890   maxlim: 4856199074   bits: 33/33
c ---[   7]---> Sorter-cost: 3181     Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   6]---> Adder-cost: 788   maxlim: 198966863   bits: 29/28
c ---[   4]---> Adder-cost: 797   maxlim: 407370522   bits: 30/29
c ---[   3]---> BDD-cost:   83
c ---[   2]---> BDD-cost:   88
c ---[   1]---> BDD-cost:   13
c ---[   0]---> Sorter-cost: 2580     Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   72289   210130 |   24096       0        0     nan |  0.000 % |
c |       100 |   72282   210115 |   26505      99      624     6.3 |  4.777 % |
c |       250 |   72240   210019 |   29156     248     2949    11.9 |  4.837 % |
c |       475 |   72240   210019 |   32071     473     7762    16.4 |  4.837 % |
c |       812 |   72222   209977 |   35278     809    11867    14.7 |  4.857 % |
c |      1318 |   72105   209670 |   38806    1299    17237    13.3 |  4.993 % |
c |      2077 |   72036   209515 |   42687    2052    30721    15.0 |  5.094 % |
c |      3218 |   71770   208916 |   46956    3169    50288    15.9 |  5.497 % |
c |      4928 |   71607   208533 |   51651    4867    93101    19.1 |  5.714 % |
c |      7491 |   71398   207969 |   56817    7407   146223    19.7 |  5.931 % |
c |     11336 |   71298   207745 |   62498   11236   240159    21.4 |  6.062 % |
c |     17103 |   71223   207577 |   68748   16990   398518    23.5 |  6.162 % |
c |     25754 |   71144   207391 |   75623   25634   619317    24.2 |  6.268 % |
c |     38729 |   71093   207268 |   83185   38604  1009610    26.2 |  6.329 % |
c |     58190 |   70964   206939 |   91504   58049  1634735    28.2 |  6.475 % |
c |     87382 |   70932   206850 |  100654   87233  2838746    32.5 |  6.510 % |
c |    131171 |   70821   206570 |  110720   44210  1648689    37.3 |  6.651 % |
c ==============================================================================
c Found solution: -939884
c ---[   0]---> Sorter-cost: 5556     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    165774 |   85451   240745 |   28483   78794  2862315    36.3 |  6.651 % |
c |    165874 |   85451   240745 |   31331   18019   466393    25.9 |  5.499 % |
c |    166024 |   85451   240745 |   34464   18169   468086    25.8 |  5.499 % |
c |    166250 |   85451   240745 |   37910   18395   470271    25.6 |  5.499 % |
c |    166588 |   85451   240745 |   41701   18733   484272    25.9 |  5.499 % |
c |    167094 |   85426   240690 |   45872   19238   492725    25.6 |  5.527 % |
c |    167855 |   85395   240621 |   50459   19997   506436    25.3 |  5.559 % |
c |    168995 |   85395   240621 |   55505   21137   535394    25.3 |  5.559 % |
c |    170703 |   85395   240621 |   61055   22845   583733    25.6 |  5.559 % |
c |    173265 |   85375   240565 |   67161   25404   672150    26.5 |  5.575 % |
c |    177109 |   85375   240565 |   73877   29248   778653    26.6 |  5.575 % |
c ==============================================================================
c Found solution: -983297
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    181867 |   85475   240886 |   28491   34005   927025    27.3 |  5.575 % |
c |    181967 |   85475   240886 |   31340   16620   372237    22.4 |  5.573 % |
c |    182118 |   85475   240886 |   34474   16771   374143    22.3 |  5.573 % |
c |    182343 |   85447   240824 |   37921   16995   377444    22.2 |  5.605 % |
c |    182681 |   85447   240824 |   41713   17333   387124    22.3 |  5.605 % |
c |    183187 |   85447   240824 |   45885   17839   401752    22.5 |  5.605 % |
c |    183946 |   85447   240824 |   50473   18598   423950    22.8 |  5.605 % |
c |    185088 |   85447   240824 |   55520   19740   468638    23.7 |  5.605 % |
c |    186796 |   85447   240824 |   61072   21448   518506    24.2 |  5.605 % |
c |    189358 |   85447   240824 |   67180   24010   585663    24.4 |  5.605 % |
c |    193203 |   85447   240824 |   73898   27855   694448    24.9 |  5.605 % |
c |    198969 |   85447   240824 |   81288   33621   918948    27.3 |  5.605 % |
c |    207618 |   85256   240390 |   89416   42262  1223144    28.9 |  5.797 % |
c ==============================================================================
c Found solution: -985507
c ---[   0]---> Sorter-cost: 1475     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    210921 |   88674   248407 |   29558   45565  1348924    29.6 |  5.797 % |
c |    211022 |   88674   248407 |   32513   18678   465794    24.9 |  5.537 % |
c |    211173 |   88636   248321 |   35765   18826   467473    24.8 |  5.579 % |
c |    211400 |   88636   248321 |   39341   19053   472963    24.8 |  5.579 % |
c |    211737 |   88636   248321 |   43275   19390   481019    24.8 |  5.579 % |
c |    212245 |   88636   248321 |   47603   19898   493299    24.8 |  5.579 % |
c |    213006 |   88636   248321 |   52363   20659   507992    24.6 |  5.579 % |
c |    214146 |   88636   248321 |   57600   21799   530936    24.4 |  5.579 % |
c |    215854 |   88636   248321 |   63360   23507   592764    25.2 |  5.579 % |
c |    218416 |   88636   248321 |   69696   26069   686338    26.3 |  5.579 % |
c |    222262 |   88636   248321 |   76665   29915   777069    26.0 |  5.579 % |
c |    228029 |   88619   248278 |   84332   35679  1095746    30.7 |  5.594 % |
c |    236679 |   88554   248132 |   92765   44324  1519219    34.3 |  5.663 % |
c ==============================================================================
c Found solution: -1250179
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    238998 |   88640   248382 |   29546   46642  1589626    34.1 |  5.663 % |
c |    239098 |   88640   248382 |   32500   18685   577923    30.9 |  5.660 % |
c |    239248 |   88640   248382 |   35750   18835   581872    30.9 |  5.660 % |
c |    239474 |   88640   248382 |   39325   19061   585881    30.7 |  5.660 % |
c |    239811 |   88640   248382 |   43258   19398   590640    30.4 |  5.660 % |
c |    240318 |   88640   248382 |   47584   19905   602929    30.3 |  5.660 % |
c |    241078 |   88640   248382 |   52342   20665   618345    29.9 |  5.660 % |
c |    242217 |   88640   248382 |   57576   21804   647814    29.7 |  5.660 % |
c |    243926 |   88629   248358 |   63334   23512   688023    29.3 |  5.671 % |
c |    246488 |   88629   248358 |   69667   26074   778690    29.9 |  5.671 % |
c |    250332 |   88629   248358 |   76634   29918   879850    29.4 |  5.671 % |
c |    256099 |   88629   248358 |   84298   35685  1120223    31.4 |  5.671 % |
c ==============================================================================
c Found solution: -1250566
c ---[   0]---> Sorter-cost:   21     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    260603 |   88627   248370 |   29542   40188  1273799    31.7 |  5.671 % |
c |    260703 |   88627   248370 |   32496   17929   466945    26.0 |  5.695 % |
c |    260853 |   88627   248370 |   35745   18079   469576    26.0 |  5.695 % |
c |    261079 |   88627   248370 |   39320   18305   471205    25.7 |  5.695 % |
c |    261416 |   88627   248370 |   43252   18642   475550    25.5 |  5.695 % |
c |    261922 |   88627   248370 |   47577   19148   484301    25.3 |  5.695 % |
c |    262681 |   88627   248370 |   52335   19907   499178    25.1 |  5.695 % |
c |    263820 |   88627   248370 |   57569   21046   529981    25.2 |  5.695 % |
c |    265529 |   88627   248370 |   63325   22755   588875    25.9 |  5.695 % |
c |    268094 |   88587   248283 |   69658   25319   682037    26.9 |  5.745 % |
c |    271939 |   88587   248283 |   76624   29164   823285    28.2 |  5.745 % |
c |    277705 |   88587   248283 |   84286   34930  1015111    29.1 |  5.745 % |
c ==============================================================================
c Found solution: -8102161
c ---[   0]---> Sorter-cost: 1730     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    279952 |   92764   258060 |   30921   37166  1138664    30.6 |  5.745 % |
c |    280052 |   92764   258060 |   34013   17396   473610    27.2 |  5.671 % |
c |    280203 |   92764   258060 |   37414   17547   475646    27.1 |  5.671 % |
c |    280428 |   92114   256038 |   41155   17356   470073    27.1 |  6.060 % |
c |    280767 |   91422   254488 |   45271   17348   459091    26.5 |  6.724 % |
c |    281274 |   91422   254488 |   49798   17855   469409    26.3 |  6.724 % |
c |    282033 |   91422   254488 |   54778   18614   481414    25.9 |  6.724 % |
c |    283173 |   91422   254488 |   60256   19754   537640    27.2 |  6.724 % |
c |    284881 |   91422   254488 |   66281   21462   581025    27.1 |  6.724 % |
c |    287446 |   91422   254488 |   72910   24027   679689    28.3 |  6.724 % |
c |    291290 |   91422   254488 |   80201   27871   916008    32.9 |  6.724 % |
c ==============================================================================
c Found solution: -8226529
c ---[   0]---> Sorter-cost: 1476     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    296289 |   94872   262566 |   31624   32870  1093833    33.3 |  6.724 % |
c |    296390 |   94872   262566 |   34786   32971  1095499    33.2 |  6.442 % |
c |    296540 |   94656   261853 |   38265   33102  1098714    33.2 |  6.521 % |
c |    296765 |   94621   261777 |   42091   33323  1101916    33.1 |  6.556 % |
c |    297102 |   94621   261777 |   46300   33660  1109662    33.0 |  6.556 % |
c |    297611 |   94289   260680 |   50930   34124  1124033    32.9 |  6.715 % |
c |    298370 |   94289   260680 |   56023   34883  1150591    33.0 |  6.715 % |
c |    299509 |   94282   260665 |   61626   36021  1184935    32.9 |  6.721 % |
c |    301218 |   94282   260665 |   67788   37730  1250596    33.1 |  6.721 % |
c |    303781 |   94260   260617 |   74567   40291  1396153    34.7 |  6.742 % |
c |    307625 |   94245   260584 |   82024   44133  1522088    34.5 |  6.756 % |
c |    313391 |   94245   260584 |   90226   49899  1679357    33.7 |  6.756 % |
c ==============================================================================
c Found solution: -8579837
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    316137 |   94305   260762 |   31435   52645  1759724    33.4 |  6.756 % |
c |    316237 |   94305   260762 |   34578   19181   391864    20.4 |  6.754 % |
c |    316388 |   94305   260762 |   38036   19332   394613    20.4 |  6.754 % |
c |    316613 |   94305   260762 |   41839   19557   398258    20.4 |  6.754 % |
c |    316951 |   94305   260762 |   46023   19895   405540    20.4 |  6.754 % |
c |    317457 |   94305   260762 |   50626   20401   416403    20.4 |  6.754 % |
c |    318216 |   94305   260762 |   55689   21160   436357    20.6 |  6.754 % |
c |    319356 |   94305   260762 |   61257   22300   459627    20.6 |  6.754 % |
c |    321064 |   94305   260762 |   67383   24008   504516    21.0 |  6.754 % |
c |    323626 |   94305   260762 |   74122   26570   567129    21.3 |  6.754 % |
c |    327471 |   94305   260762 |   81534   30415   688826    22.6 |  6.754 % |
c |    333238 |   94305   260762 |   89687   36182  1067582    29.5 |  6.754 % |
c |    341887 |   94301   260753 |   98656   44830  1531878    34.2 |  6.757 % |
c ==============================================================================
c Found solution: -8621307
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    346370 |   94314   260801 |   31438   49313  1675513    34.0 |  6.757 % |
c |    346472 |   94314   260801 |   34581   18775   608700    32.4 |  6.759 % |
c |    346622 |   94314   260801 |   38039   18925   611848    32.3 |  6.759 % |
c |    346847 |   94314   260801 |   41843   19150   615641    32.1 |  6.759 % |
c |    347185 |   94314   260801 |   46028   19488   628568    32.3 |  6.759 % |
c |    347694 |   94314   260801 |   50631   19997   638032    31.9 |  6.759 % |
c |    348453 |   94314   260801 |   55694   20756   655512    31.6 |  6.759 % |
c |    349592 |   94273   260710 |   61263   21894   679836    31.1 |  6.800 % |
c |    351302 |   94273   260710 |   67390   23604   722415    30.6 |  6.800 % |
c |    353866 |   94237   260630 |   74129   26166   803378    30.7 |  6.834 % |
c |    357711 |   94233   260621 |   81542   30010   913378    30.4 |  6.838 % |
c |    363477 |   94231   260615 |   89696   35768  1080197    30.2 |  6.841 % |
c ==============================================================================
c Found solution: -8666624
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    368574 |   94286   260753 |   31428   40863  1214975    29.7 |  6.841 % |
c |    368674 |   94286   260753 |   34570   18249   348384    19.1 |  6.855 % |
c |    368825 |   94286   260753 |   38027   18400   350111    19.0 |  6.855 % |
c |    369050 |   94286   260753 |   41830   18625   353652    19.0 |  6.855 % |
c |    369391 |   94286   260753 |   46013   18966   358755    18.9 |  6.855 % |
c |    369898 |   94286   260753 |   50615   19473   366573    18.8 |  6.855 % |
c |    370657 |   94271   260719 |   55676   20230   407843    20.2 |  6.869 % |
c |    371796 |   94271   260719 |   61244   21369   439731    20.6 |  6.869 % |
c |    373504 |   94271   260719 |   67368   23077   478415    20.7 |  6.869 % |
c |    376067 |   94271   260719 |   74105   25640   548309    21.4 |  6.869 % |
c |    379912 |   94271   260719 |   81516   29485   684383    23.2 |  6.869 % |
c |    385678 |   94177   260508 |   89667   35249   881979    25.0 |  6.955 % |
c |    394328 |   94133   260409 |   98634   43896  1155863    26.3 |  7.000 % |
c ==============================================================================
c Found solution: -8700288
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    397896 |   94145   260445 |   31381   47464  1340605    28.2 |  7.000 % |
c |    397996 |   94145   260445 |   34519   19017   485826    25.5 |  7.001 % |
c |    398147 |   94145   260445 |   37971   19168   487970    25.5 |  7.001 % |
c |    398372 |   94145   260445 |   41768   19393   491026    25.3 |  7.001 % |
c |    398709 |   94145   260445 |   45944   19730   495225    25.1 |  7.001 % |
c |    399217 |   94145   260445 |   50539   20238   507093    25.1 |  7.001 % |
c |    399978 |   94145   260445 |   55593   20999   526948    25.1 |  7.001 % |
c |    401118 |   94042   260216 |   61152   22135   559086    25.3 |  7.098 % |
c |    402827 |   94027   260165 |   67267   23836   606749    25.5 |  7.105 % |
c |    405391 |   94027   260165 |   73994   26400   701319    26.6 |  7.105 % |
c ==============================================================================
c Found solution: -8715502
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    408018 |   94049   260213 |   31349   29027   797749    27.5 |  7.105 % |
c |    408122 |   94049   260213 |   34483   29131   800660    27.5 |  7.106 % |
c |    408272 |   94049   260213 |   37932   29281   802369    27.4 |  7.106 % |
c |    408499 |   94049   260213 |   41725   29508   805642    27.3 |  7.106 % |
c |    408836 |   94049   260213 |   45898   29845   812759    27.2 |  7.106 % |
c |    409342 |   94049   260213 |   50487   30351   828341    27.3 |  7.106 % |
c |    410102 |   94049   260213 |   55536   31111   859300    27.6 |  7.106 % |
c |    411241 |   94049   260213 |   61090   32250   886086    27.5 |  7.106 % |
c |    412949 |   94049   260213 |   67199   33958   929880    27.4 |  7.106 % |
c |    415512 |   94049   260213 |   73919   36521   999541    27.4 |  7.106 % |
c ==============================================================================
c Found solution: -8721144
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    419239 |   94090   260314 |   31363   40248  1112393    27.6 |  7.106 % |
c |    419340 |   94090   260314 |   34499   19679   377827    19.2 |  7.104 % |
c |    419491 |   94090   260314 |   37949   19830   380335    19.2 |  7.104 % |
c |    419716 |   94090   260314 |   41744   20055   382864    19.1 |  7.104 % |
c |    420053 |   94090   260314 |   45918   20392   388991    19.1 |  7.104 % |
c |    420560 |   94090   260314 |   50510   20899   400656    19.2 |  7.104 % |
c |    421320 |   94090   260314 |   55561   21659   416263    19.2 |  7.104 % |
c |    422459 |   94090   260314 |   61117   22798   440616    19.3 |  7.104 % |
c |    424167 |   94090   260314 |   67229   24506   483311    19.7 |  7.104 % |
c |    426729 |   94083   260298 |   73952   27067   561312    20.7 |  7.111 % |
c |    430575 |   94083   260298 |   81347   30913   676503    21.9 |  7.111 % |
c |    436341 |   94083   260298 |   89482   36679   849719    23.2 |  7.111 % |
c ==============================================================================
c Found solution: -8888309
c ---[   0]---> Sorter-cost:   19     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    439505 |   94108   260358 |   31369   39843   959472    24.1 |  7.111 % |
c |    439607 |   94108   260358 |   34505   20024   409922    20.5 |  7.112 % |
c |    439759 |   94108   260358 |   37956   20176   412969    20.5 |  7.112 % |
c |    439984 |   94108   260358 |   41752   20401   416435    20.4 |  7.112 % |
c |    440321 |   94108   260358 |   45927   20738   422538    20.4 |  7.112 % |
c |    440827 |   94093   260307 |   50520   21243   433245    20.4 |  7.119 % |
c |    441587 |   94093   260307 |   55572   22003   450068    20.5 |  7.119 % |
c |    442726 |   94093   260307 |   61129   23142   476740    20.6 |  7.119 % |
c |    444434 |   94082   260282 |   67242   24848   526243    21.2 |  7.129 % |
c |    446996 |   94082   260282 |   73966   27410   610930    22.3 |  7.129 % |
c |    450841 |   94082   260282 |   81363   31255   744432    23.8 |  7.129 % |
c |    456607 |   94041   260191 |   89499   37018   925105    25.0 |  7.167 % |
c ==============================================================================
c Found solution: -8888600
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    462336 |   93972   259930 |   31324   41926  1165540    27.8 |  7.167 % |
c |    462437 |   93972   259930 |   34456   20103   487376    24.2 |  7.185 % |
c |    462588 |   93935   259802 |   37902   20249   490451    24.2 |  7.196 % |
c |    462813 |   93935   259802 |   41692   20474   496191    24.2 |  7.196 % |
c |    463151 |   93935   259802 |   45861   20812   502342    24.1 |  7.196 % |
c |    463657 |   93935   259802 |   50447   21318   521851    24.5 |  7.196 % |
c |    464417 |   93723   259120 |   55492   22068   535358    24.3 |  7.295 % |
c |    465556 |   93723   259120 |   61041   23207   563353    24.3 |  7.295 % |
c |    467265 |   93723   259120 |   67145   24916   633466    25.4 |  7.295 % |
c |    469827 |   93673   259002 |   73860   27473   704301    25.6 |  7.340 % |
c ==============================================================================
c Found solution: -8890619
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    470924 |   93689   259039 |   31229   28570   728321    25.5 |  7.340 % |
c |    471024 |   93689   259039 |   34351   28670   730301    25.5 |  7.341 % |
c |    471174 |   93689   259039 |   37787   28820   732903    25.4 |  7.341 % |
c |    471399 |   93689   259039 |   41565   29045   736661    25.4 |  7.341 % |
c |    471736 |   93689   259039 |   45722   29382   741221    25.2 |  7.341 % |
c |    472242 |   93689   259039 |   50294   29888   756252    25.3 |  7.341 % |
c |    473002 |   93689   259039 |   55324   30648   769765    25.1 |  7.341 % |
c |    474144 |   93678   259014 |   60856   31788   802743    25.3 |  7.351 % |
c |    475852 |   93678   259014 |   66942   33496   860503    25.7 |  7.351 % |
c |    478414 |   93678   259014 |   73636   36058   941131    26.1 |  7.351 % |
c |    482260 |   93678   259014 |   80999   39904  1112521    27.9 |  7.351 % |
c |    488028 |   93678   259014 |   89099   45672  1371593    30.0 |  7.351 % |
c |    496677 |   93553   258574 |   98009   54285  1904144    35.1 |  7.386 % |
c ==============================================================================
c Found solution: -8896763
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    509030 |   93552   258575 |   31184   66637  2470886    37.1 |  7.386 % |
c |    509130 |   93552   258575 |   34302   19357   590982    30.5 |  7.398 % |
c |    509280 |   92716   256609 |   37732   19482   594057    30.5 |  8.177 % |
c |    509505 |   92716   256609 |   41505   19707   598648    30.4 |  8.177 % |
c |    509844 |   92716   256609 |   45656   20046   612256    30.5 |  8.177 % |
c |    510350 |   92701   256574 |   50222   20551   622163    30.3 |  8.195 % |
c |    511109 |   92701   256574 |   55244   21310   635254    29.8 |  8.195 % |
c |    512248 |   92701   256574 |   60768   22449   653138    29.1 |  8.195 % |
c |    513959 |   92692   256543 |   66845   24159   690596    28.6 |  8.198 % |
c |    516521 |   92677   256510 |   73530   26720   763545    28.6 |  8.219 % |
c |    520366 |   92677   256510 |   80883   30565   862565    28.2 |  8.219 % |
c |    526132 |   92677   256510 |   88971   36331  1142403    31.4 |  8.219 % |
c ==============================================================================
c Found solution: -9200016
c ---[   0]---> Sorter-cost: 1534     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    526781 |   96289   264961 |   32096   36980  1159724    31.4 |  8.219 % |
c |    526883 |   96289   264961 |   35305   17263   451541    26.2 |  7.923 % |
c |    527033 |   96289   264961 |   38836   17413   454651    26.1 |  7.923 % |
c |    527259 |   96289   264961 |   42719   17639   457788    26.0 |  7.923 % |
c |    527596 |   96289   264961 |   46991   17976   465944    25.9 |  7.923 % |
c |    528102 |   96289   264961 |   51690   18482   476186    25.8 |  7.923 % |
c |    528861 |   96289   264961 |   56860   19241   495983    25.8 |  7.923 % |
c |    530000 |   96289   264961 |   62546   20380   516998    25.4 |  7.923 % |
c |    531710 |   96281   264943 |   68800   22089   560746    25.4 |  7.930 % |
c |    534272 |   96281   264943 |   75680   24651   636399    25.8 |  7.930 % |
c |    538116 |   96281   264943 |   83248   28495   759238    26.6 |  7.930 % |
c |    543882 |   95856   263560 |   91573   34196   953022    27.9 |  8.153 % |
c ==============================================================================
c Found solution: -9314760
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    549997 |   96012   263940 |   32004   40311  1157113    28.7 |  8.153 % |
c |    550098 |   96012   263940 |   35204   18299   427370    23.4 |  8.133 % |
c |    550249 |   96012   263940 |   38724   18450   429122    23.3 |  8.133 % |
c |    550476 |   96012   263940 |   42597   18677   433784    23.2 |  8.133 % |
c |    550814 |   96012   263940 |   46857   19015   438516    23.1 |  8.133 % |
c |    551320 |   96012   263940 |   51542   19521   449327    23.0 |  8.133 % |
c |    552079 |   96003   263909 |   56697   20278   469871    23.2 |  8.136 % |
c |    553218 |   96003   263909 |   62366   21417   497639    23.2 |  8.136 % |
c |    554926 |   96003   263909 |   68603   23125   625749    27.1 |  8.136 % |
c |    557488 |   96003   263909 |   75463   25687   698540    27.2 |  8.136 % |
c |    561332 |   96003   263909 |   83010   29531   843454    28.6 |  8.136 % |
c ==============================================================================
c Found solution: -9470115
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    566001 |   96013   263941 |   32004   34198  1021808    29.9 |  8.136 % |
c |    566101 |   96013   263941 |   35204   34298  1023488    29.8 |  8.141 % |
c |    566251 |   95996   263904 |   38724   34445  1025423    29.8 |  8.158 % |
c |    566479 |   95996   263904 |   42597   34673  1033404    29.8 |  8.158 % |
c |    566816 |   95973   263853 |   46857   35005  1044773    29.8 |  8.177 % |
c |    567323 |   95973   263853 |   51542   35512  1059645    29.8 |  8.177 % |
c |    568082 |   95973   263853 |   56697   36271  1077196    29.7 |  8.177 % |
c |    569223 |   95823   263343 |   62366   37389  1115322    29.8 |  8.249 % |
c |    570931 |   95823   263343 |   68603   39097  1159965    29.7 |  8.250 % |
c |    573495 |   95823   263343 |   75463   41661  1219947    29.3 |  8.249 % |
c ==============================================================================
c Found solution: -9470836
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    576918 |   95842   263390 |   31947   45084  1348356    29.9 |  8.249 % |
c |    577018 |   95827   263356 |   35141   20251   408082    20.2 |  8.263 % |
c |    577171 |   95827   263356 |   38655   20404   411066    20.1 |  8.263 % |
c |    577396 |   95827   263356 |   42521   20629   415499    20.1 |  8.263 % |
c |    577734 |   95827   263356 |   46773   20967   420850    20.1 |  8.263 % |
c |    578241 |   95827   263356 |   51450   21474   436686    20.3 |  8.263 % |
c |    579001 |   95799   263294 |   56596   22231   457648    20.6 |  8.290 % |
c |    580140 |   95799   263294 |   62255   23370   493047    21.1 |  8.290 % |
c |    581849 |   95799   263294 |   68481   25079   535190    21.3 |  8.290 % |
c |    584411 |   95799   263294 |   75329   27641   625970    22.6 |  8.290 % |
c |    588255 |   95799   263294 |   82862   31485   766418    24.3 |  8.290 % |
c ==============================================================================
c Found solution: -9470975
c ---[   0]---> Sorter-cost:   19     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    592741 |   95794   263290 |   31931   35969   932720    25.9 |  8.290 % |
c |    592841 |   95794   263290 |   35124   18085   420838    23.3 |  8.314 % |
c |    592992 |   95794   263290 |   38636   18236   426139    23.4 |  8.314 % |
c |    593218 |   95794   263290 |   42500   18462   428483    23.2 |  8.314 % |
c |    593555 |   95794   263290 |   46750   18799   433933    23.1 |  8.314 % |
c |    594063 |   95794   263290 |   51425   19307   442242    22.9 |  8.314 % |
c |    594822 |   95794   263290 |   56567   20066   456127    22.7 |  8.314 % |
c |    595961 |   95794   263290 |   62224   21205   493014    23.2 |  8.314 % |
c |    597669 |   95794   263290 |   68446   22913   529113    23.1 |  8.314 % |
c |    600232 |   95794   263290 |   75291   25476   625995    24.6 |  8.314 % |
c |    604076 |   95794   263290 |   82820   29320   737591    25.2 |  8.314 % |
c |    609842 |   95794   263290 |   91102   35086   914441    26.1 |  8.314 % |
c |    618492 |   95739   263167 |  100213   43735  1244184    28.4 |  8.360 % |
c ==============================================================================
c Found solution: -9476276
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    622869 |   95740   263140 |   31913   48101  1408379    29.3 |  8.360 % |
c |    622969 |   95740   263140 |   35104   21290   503749    23.7 |  8.373 % |
c |    623122 |   95740   263140 |   38614   21443   506578    23.6 |  8.373 % |
c |    623348 |   95740   263140 |   42476   21669   511706    23.6 |  8.373 % |
c |    623686 |   95740   263140 |   46723   22007   518971    23.6 |  8.373 % |
c |    624192 |   95740   263140 |   51396   22513   529490    23.5 |  8.373 % |
c |    624953 |   95662   262877 |   56535   23248   551082    23.7 |  8.432 % |
c |    626092 |   95662   262877 |   62189   24387   570853    23.4 |  8.432 % |
c |    627802 |   95662   262877 |   68408   26097   627074    24.0 |  8.432 % |
c |    630366 |   95662   262877 |   75249   28661   693960    24.2 |  8.432 % |
c |    634210 |   95302   262056 |   82774   32459   809163    24.9 |  8.766 % |
c |    639978 |   95266   261974 |   91051   38224   973176    25.5 |  8.802 % |
c |    648627 |   95266   261974 |  100156   46873  1451359    31.0 |  8.802 % |
c ==============================================================================
c Found solution: -9493755
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    661033 |   95230   261876 |   31743   59275  1835451    31.0 |  8.802 % |
c |    661133 |   95230   261876 |   34917   22481   439504    19.6 |  8.847 % |
c |    661283 |   95230   261876 |   38409   22631   442076    19.5 |  8.847 % |
c |    661508 |   95230   261876 |   42249   22856   445755    19.5 |  8.847 % |
c |    661847 |   95230   261876 |   46474   23195   452181    19.5 |  8.847 % |
c |    662355 |   95215   261842 |   51122   23702   462012    19.5 |  8.860 % |
c |    663115 |   95215   261842 |   56234   24462   483501    19.8 |  8.860 % |
c |    664255 |   95215   261842 |   61858   25602   507986    19.8 |  8.860 % |
c |    665963 |   95215   261842 |   68043   27310   569362    20.8 |  8.860 % |
c |    668525 |   95215   261842 |   74848   29872   658470    22.0 |  8.860 % |
c |    672369 |   95215   261842 |   82333   33716   797185    23.6 |  8.860 % |
c |    678135 |   95193   261790 |   90566   39480   969658    24.6 |  8.880 % |
c ==============================================================================
c Found solution: -9494778
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    685880 |   95202   261820 |   31734   47225  1252332    26.5 |  8.880 % |
c |    685980 |   95202   261820 |   34907   20639   439584    21.3 |  8.882 % |
c |    686130 |   95202   261820 |   38398   20789   441988    21.3 |  8.882 % |
c |    686355 |   95168   261743 |   42237   21010   446059    21.2 |  8.918 % |
c |    686692 |   95168   261743 |   46461   21347   453396    21.2 |  8.918 % |
c |    687198 |   95168   261743 |   51107   21853   467217    21.4 |  8.918 % |
c |    687957 |   95168   261743 |   56218   22612   483850    21.4 |  8.918 % |
c |    689096 |   95168   261743 |   61840   23751   524878    22.1 |  8.918 % |
c |    690804 |   95168   261743 |   68024   25459   559745    22.0 |  8.918 % |
c |    693369 |   95168   261743 |   74827   28024   672176    24.0 |  8.918 % |
c |    697214 |   95168   261743 |   82309   31869   776133    24.4 |  8.918 % |
c |    702981 |   95168   261743 |   90540   37636  1003679    26.7 |  8.918 % |
c |    711632 |   95168   261743 |   99594   46287  1344578    29.0 |  8.918 % |
c |    724608 |   95142   261667 |  109554   59260  1842718    31.1 |  8.934 % |
c ==============================================================================
c Found solution: -9501954
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    730974 |   95157   261705 |   31719   65626  2060488    31.4 |  8.934 % |
c |    731075 |   95157   261705 |   34890   21355   453278    21.2 |  8.936 % |
c |    731226 |   95157   261705 |   38379   21506   456685    21.2 |  8.936 % |
c |    731451 |   95157   261705 |   42217   21731   461020    21.2 |  8.936 % |
c |    731789 |   95157   261705 |   46439   22069   466252    21.1 |  8.936 % |
c |    732295 |   95157   261705 |   51083   22575   474792    21.0 |  8.936 % |
c |    733055 |   95157   261705 |   56192   23335   494451    21.2 |  8.936 % |
c |    734194 |   95157   261705 |   61811   24474   523296    21.4 |  8.936 % |
c |    735902 |   95157   261705 |   67992   26182   571285    21.8 |  8.936 % |
c |    738469 |   95157   261705 |   74791   28749   670427    23.3 |  8.936 % |
c |    742313 |   94838   260975 |   82270   32579   760477    23.3 |  9.198 % |
c ==============================================================================
c Found solution: -9501981
c ---[   0]---> Sorter-cost: 1677     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    743769 |   98985   270675 |   32995   34035   800957    23.5 |  9.198 % |
c |    743869 |   98985   270675 |   36294   34135   802938    23.5 |  8.815 % |
c |    744021 |   98985   270675 |   39923   34287   805830    23.5 |  8.815 % |
c |    744246 |   98985   270675 |   43916   34512   811167    23.5 |  8.815 % |
c |    744585 |   98985   270675 |   48307   34851   819102    23.5 |  8.815 % |
c |    745092 |   98985   270675 |   53138   35358   830217    23.5 |  8.815 % |
c |    745852 |   98985   270675 |   58452   36118   849843    23.5 |  8.815 % |
c |    746991 |   98985   270675 |   64297   37257   870206    23.4 |  8.815 % |
c |    748699 |   98985   270675 |   70727   38965   961961    24.7 |  8.815 % |
c ==============================================================================
c Found solution: -9502326
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    749602 |   99017   270776 |   33005   39868   994491    24.9 |  8.815 % |
c |    749702 |   99017   270776 |   36305   20034   370604    18.5 |  8.814 % |
c |    749853 |   99017   270776 |   39936   20185   375652    18.6 |  8.814 % |
c |    750079 |   99017   270776 |   43929   20411   379317    18.6 |  8.814 % |
c |    750416 |   99017   270776 |   48322   20748   386919    18.6 |  8.814 % |
c |    750925 |   99017   270776 |   53154   21257   409609    19.3 |  8.814 % |
c |    751684 |   99017   270776 |   58470   22016   435978    19.8 |  8.814 % |
c |    752823 |   99017   270776 |   64317   23155   476762    20.6 |  8.814 % |
c |    754531 |   99017   270776 |   70749   24863   543855    21.9 |  8.814 % |
c |    757093 |   99017   270776 |   77824   27425   633931    23.1 |  8.814 % |
c |    760937 |   99017   270776 |   85606   31269   749382    24.0 |  8.814 % |
c |    766704 |   99017   270776 |   94167   37036   938955    25.4 |  8.814 % |
c ==============================================================================
c Found solution: -9502475
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    775324 |   99037   270825 |   33012   45656  1347798    29.5 |  8.814 % |
c |    775424 |   99037   270825 |   36313   20610   565744    27.4 |  8.814 % |
c |    775575 |   99037   270825 |   39944   20761   568050    27.4 |  8.814 % |
c |    775800 |   99037   270825 |   43938   20986   572986    27.3 |  8.814 % |
c |    776137 |   99037   270825 |   48332   21323   578512    27.1 |  8.814 % |
c |    776644 |   99037   270825 |   53166   21830   588540    27.0 |  8.814 % |
c |    777403 |   99037   270825 |   58482   22589   606313    26.8 |  8.814 % |
c |    778542 |   99037   270825 |   64331   23728   635509    26.8 |  8.814 % |
c ==============================================================================
c Found solution: -9918740
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    779920 |   99094   270967 |   33031   25106   679017    27.0 |  8.814 % |
c |    780020 |   99094   270967 |   36334   25206   680342    27.0 |  8.811 % |
c |    780173 |   99094   270967 |   39967   25359   683377    26.9 |  8.811 % |
c |    780399 |   99094   270967 |   43964   25585   686958    26.9 |  8.811 % |
c |    780736 |   99094   270967 |   48360   25922   696648    26.9 |  8.811 % |
c |    781242 |   99094   270967 |   53196   26428   708915    26.8 |  8.811 % |
c |    782001 |   99094   270967 |   58516   27187   724058    26.6 |  8.811 % |
c |    783141 |   99094   270967 |   64368   28327   752067    26.5 |  8.811 % |
c |    784850 |   99094   270967 |   70804   30036   804332    26.8 |  8.811 % |
c |    787413 |   99081   270939 |   77885   32598   868130    26.6 |  8.823 % |
c |    791258 |   99081   270939 |   85673   36443   967300    26.5 |  8.823 % |
c |    797024 |   99081   270939 |   94241   42209  1140218    27.0 |  8.823 % |
c |    805673 |   99081   270939 |  103665   50858  1485290    29.2 |  8.823 % |
c |    818647 |   99081   270939 |  114031   63832  1944233    30.5 |  8.823 % |
c ==============================================================================
c Found solution: -9919741
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    822574 |   99094   270971 |   33031   67759  2061079    30.4 |  8.823 % |
c |    822674 |   99094   270971 |   36334   22167   507287    22.9 |  8.825 % |
c |    822825 |   99094   270971 |   39967   22318   510839    22.9 |  8.825 % |
c |    823051 |   99094   270971 |   43964   22544   516663    22.9 |  8.825 % |
c |    823388 |   99049   270872 |   48360   22877   522572    22.8 |  8.865 % |
c |    823895 |   99049   270872 |   53196   23384   537790    23.0 |  8.865 % |
c |    824655 |   99049   270872 |   58516   24144   559231    23.2 |  8.865 % |
c |    825794 |   99049   270872 |   64368   25283   599732    23.7 |  8.865 % |
c |    827502 |   99049   270872 |   70804   26991   675678    25.0 |  8.865 % |
c |    830064 |   99049   270872 |   77885   29553   784705    26.6 |  8.865 % |
c |    833909 |   99049   270872 |   85673   33398   901353    27.0 |  8.865 % |
c |    839675 |   99049   270872 |   94241   39164  1083049    27.7 |  8.865 % |
c |    848324 |   99049   270872 |  103665   47813  1332699    27.9 |  8.865 % |
c ==============================================================================
c Found solution: -9961736
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    851725 |   99056   270899 |   33018   51214  1443695    28.2 |  8.865 % |
c |    851825 |   99056   270899 |   36319   21257   408696    19.2 |  8.867 % |
c |    851975 |   99056   270899 |   39951   21407   410379    19.2 |  8.867 % |
c |    852200 |   99056   270899 |   43946   21632   413747    19.1 |  8.867 % |
c |    852538 |   99056   270899 |   48341   21970   421279    19.2 |  8.867 % |
c |    853044 |   99056   270899 |   53175   22476   430909    19.2 |  8.867 % |
c |    853803 |   99056   270899 |   58493   23235   463081    19.9 |  8.867 % |
c |    854943 |   99056   270899 |   64342   24375   501805    20.6 |  8.867 % |
c |    856652 |   99056   270899 |   70777   26084   569058    21.8 |  8.867 % |
c ==============================================================================
c Found solution: -10002683
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    858736 |   99125   271068 |   33041   28168   635190    22.6 |  8.867 % |
c |    858836 |   99125   271068 |   36345   28268   638801    22.6 |  8.862 % |
c |    858986 |   99125   271068 |   39979   28418   641441    22.6 |  8.862 % |
c |    859211 |   99125   271068 |   43977   28643   645700    22.5 |  8.862 % |
c |    859548 |   99125   271068 |   48375   28980   653529    22.6 |  8.862 % |
c |    860054 |   99125   271068 |   53212   29486   668603    22.7 |  8.862 % |
c |    860813 |   99125   271068 |   58534   30245   682079    22.6 |  8.862 % |
c |    861953 |   99125   271068 |   64387   31385   721674    23.0 |  8.862 % |
c |    863662 |   99125   271068 |   70826   33094   771522    23.3 |  8.862 % |
c |    866224 |   99125   271068 |   77908   35656   852052    23.9 |  8.862 % |
c |    870069 |   99125   271068 |   85699   39501   971737    24.6 |  8.862 % |
c ==============================================================================
c Found solution: -10035469
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    873125 |   99137   271105 |   33045   42557  1059604    24.9 |  8.862 % |
c |    873226 |   99137   271105 |   36349   20719   396117    19.1 |  8.863 % |
c |    873377 |   99137   271105 |   39984   20870   398156    19.1 |  8.863 % |
c |    873603 |   99137   271105 |   43982   21096   403534    19.1 |  8.863 % |
c |    873940 |   99137   271105 |   48381   21433   410111    19.1 |  8.863 % |
c |    874447 |   99137   271105 |   53219   21940   422166    19.2 |  8.863 % |
c |    875210 |   99137   271105 |   58541   22703   436337    19.2 |  8.863 % |
c |    876350 |   99137   271105 |   64395   23843   482989    20.3 |  8.863 % |
c |    878058 |   99137   271105 |   70834   25551   523819    20.5 |  8.863 % |
c |    880620 |   99137   271105 |   77918   28113   594466    21.1 |  8.863 % |
c |    884466 |   99137   271105 |   85710   31959   693369    21.7 |  8.863 % |
c |    890232 |   99137   271105 |   94281   37725   857953    22.7 |  8.863 % |
c ==============================================================================
c Found solution: -10090748
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    893828 |   99140   271119 |   33046   41319   961598    23.3 |  8.863 % |
c |    893930 |   99140   271119 |   36350   20576   363440    17.7 |  8.873 % |
c |    894081 |   99140   271119 |   39985   20727   365566    17.6 |  8.873 % |
c |    894307 |   99140   271119 |   43984   20953   370617    17.7 |  8.873 % |
c |    894644 |   99140   271119 |   48382   21290   375940    17.7 |  8.873 % |
c |    895151 |   99140   271119 |   53220   21797   388209    17.8 |  8.873 % |
c |    895910 |   99140   271119 |   58543   22556   406229    18.0 |  8.873 % |
c |    897050 |   99140   271119 |   64397   23696   434516    18.3 |  8.873 % |
c |    898758 |   99140   271119 |   70837   25404   487591    19.2 |  8.873 % |
c |    901321 |   99131   271088 |   77920   27964   555404    19.9 |  8.876 % |
c |    905165 |   99131   271088 |   85712   31808   659322    20.7 |  8.876 % |
c |    910931 |   99131   271088 |   94284   37574   867744    23.1 |  8.876 % |
c |    919583 |   99131   271088 |  103712   46226  1215174    26.3 |  8.876 % |
c ==============================================================================
c Found solution: -10356985
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    929616 |   99105   271033 |   33035   56252  1553529    27.6 |  8.876 % |
c |    929716 |   99105   271033 |   36338   20717   461159    22.3 |  8.912 % |
c |    929869 |   99105   271033 |   39972   20870   464338    22.2 |  8.912 % |
c |    930095 |   99105   271033 |   43969   21096   467807    22.2 |  8.912 % |
c |    930432 |   99105   271033 |   48366   21433   474300    22.1 |  8.912 % |
c |    930938 |   99105   271033 |   53203   21939   491435    22.4 |  8.912 % |
c |    931697 |   99105   271033 |   58523   22698   509153    22.4 |  8.912 % |
c |    932836 |   97683   266368 |   64375   21380   476818    22.3 |  9.616 % |
c |    934545 |   97683   266368 |   70813   23089   525273    22.7 |  9.616 % |
c |    937109 |   97596   266172 |   77894   25647   592957    23.1 |  9.693 % |
c |    940953 |   97594   266166 |   85684   29470   694254    23.6 |  9.696 % |
c |    946719 |   97578   266129 |   94252   35234   863120    24.5 |  9.715 % |
c |    955369 |   97578   266129 |  103677   43884  1109394    25.3 |  9.715 % |
c ==============================================================================
c Found solution: -10383617
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    968226 |   97577   266134 |   32525   56740  1526832    26.9 |  9.715 % |
c |    968327 |   97577   266134 |   35777   21844   442384    20.3 |  9.728 % |
c |    968478 |   97577   266134 |   39355   21995   445335    20.2 |  9.728 % |
c |    968703 |   97577   266134 |   43290   22220   450421    20.3 |  9.728 % |
c |    969040 |   97577   266134 |   47619   22557   455852    20.2 |  9.728 % |
c |    969547 |   97577   266134 |   52381   23064   473916    20.5 |  9.728 % |
c |    970306 |   97577   266134 |   57620   23823   491179    20.6 |  9.728 % |
c |    971445 |   97577   266134 |   63382   24962   538852    21.6 |  9.728 % |
c |    973153 |   97577   266134 |   69720   26670   589020    22.1 |  9.728 % |
c |    975718 |   97577   266134 |   76692   29235   667456    22.8 |  9.728 % |
c |    979563 |   97577   266134 |   84361   33080   807010    24.4 |  9.728 % |
c |    985329 |   97577   266134 |   92797   38846   967628    24.9 |  9.728 % |
c |    993978 |   97577   266134 |  102077   47495  1379611    29.0 |  9.728 % |
c |   1006953 |   97577   266134 |  112285   60470  1951982    32.3 |  9.728 % |
c |   1026415 |   97534   266039 |  123513   79926  2870638    35.9 |  9.765 % |
c ==============================================================================
c Found solution: -10384638
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1047105 |   97551   266084 |   32517  100616  4010576    39.9 |  9.765 % |
c |   1047205 |   97551   266084 |   35768   18945   775083    40.9 |  9.765 % |
c |   1047356 |   97551   266084 |   39345   19096   777230    40.7 |  9.765 % |
c |   1047582 |   97551   266084 |   43280   19322   781834    40.5 |  9.765 % |
c |   1047919 |   97551   266084 |   47608   19659   788113    40.1 |  9.765 % |
c |   1048426 |   97551   266084 |   52368   20166   796723    39.5 |  9.765 % |
c |   1049185 |   97551   266084 |   57605   20925   809824    38.7 |  9.765 % |
c |   1050324 |   97466   265878 |   63366   22048   836609    37.9 |  9.858 % |
c |   1052033 |   97451   265844 |   69703   23756   873956    36.8 |  9.871 % |
c |   1054596 |   97449   265840 |   76673   26318   925335    35.2 |  9.874 % |
c |   1058440 |   97449   265840 |   84340   30162  1004658    33.3 |  9.874 % |
c |   1064206 |   97449   265840 |   92774   35928  1126342    31.3 |  9.874 % |
c |   1072855 |   97449   265840 |  102052   44577  1391482    31.2 |  9.874 % |
c |   1085830 |   97449   265840 |  112257   57552  1896368    33.0 |  9.874 % |
c ==============================================================================
c Found solution: -10395901
c ---[   0]---> Sorter-cost:   97     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1094994 |   97535   266043 |   32511   66711  2214945    33.2 |  9.874 % |
c |   1095094 |   97535   266043 |   35762   20013   520387    26.0 |  9.868 % |
c |   1095246 |   97535   266043 |   39338   20165   522779    25.9 |  9.868 % |
c |   1095471 |   97535   266043 |   43272   20390   526721    25.8 |  9.868 % |
c |   1095810 |   97535   266043 |   47599   20729   533253    25.7 |  9.868 % |
c |   1096316 |   97535   266043 |   52359   21235   541290    25.5 |  9.868 % |
c |   1097076 |   97535   266043 |   57595   21995   558786    25.4 |  9.868 % |
c |   1098215 |   97535   266043 |   63354   23134   586486    25.4 |  9.868 % |
c |   1099923 |   97535   266043 |   69690   24842   623907    25.1 |  9.868 % |
c |   1102485 |   97535   266043 |   76659   27404   733224    26.8 |  9.868 % |
c |   1106329 |   97535   266043 |   84325   31248   859196    27.5 |  9.868 % |
c |   1112097 |   97535   266043 |   92757   37016  1112222    30.0 |  9.868 % |
c |   1120749 |   97500   265940 |  102033   45665  1345384    29.5 |  9.896 % |
c ==============================================================================
c Found solution: -10435834
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1124102 |   97515   265980 |   32505   49018  1496273    30.5 |  9.896 % |
c |   1124203 |   97515   265980 |   35755   21834   425313    19.5 |  9.897 % |
c |   1124354 |   97515   265980 |   39331   21985   427883    19.5 |  9.897 % |
c |   1124581 |   97515   265980 |   43264   22212   430749    19.4 |  9.897 % |
c |   1124918 |   97460   265854 |   47590   22545   435949    19.3 |  9.953 % |
c |   1125426 |   97460   265854 |   52349   23053   446208    19.4 |  9.953 % |
c |   1126185 |   97460   265854 |   57584   23812   460776    19.4 |  9.953 % |
c |   1127324 |   97460   265854 |   63343   24951   490716    19.7 |  9.953 % |
c |   1129032 |   97460   265854 |   69677   26659   551183    20.7 |  9.953 % |
c ==============================================================================
c Found solution: -11794676
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1130356 |   97518   265991 |   32506   27983   588621    21.0 |  9.953 % |
c |   1130456 |   97518   265991 |   35756   28083   590601    21.0 |  9.946 % |
c |   1130607 |   97518   265991 |   39332   28234   593425    21.0 |  9.946 % |
c |   1130833 |   97518   265991 |   43265   28460   597500    21.0 |  9.946 % |
c |   1131172 |   97518   265991 |   47592   28799   603072    20.9 |  9.946 % |
c |   1131678 |   97518   265991 |   52351   29305   611709    20.9 |  9.946 % |
c |   1132438 |   96570   263842 |   57586   30015   633380    21.1 | 10.789 % |
c |   1133577 |   96555   263808 |   63344   31153   656357    21.1 | 10.805 % |
c |   1135286 |   91321   251443 |   69679   28960   592559    20.5 | 15.568 % |
c ==============================================================================
c Found solution: -11805006
c ---[   0]---> Sorter-cost: 1224     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1137351 |   93249   255997 |   31083   30861   670121    21.7 | 15.568 % |
c |   1137452 |   93056   255351 |   34191   30817   669536    21.7 | 16.076 % |
c |   1137602 |   93056   255351 |   37610   30967   672302    21.7 | 16.076 % |
c |   1137830 |   92833   254599 |   41371   31039   672044    21.7 | 16.172 % |
c |   1138167 |   92833   254599 |   45508   31376   680023    21.7 | 16.172 % |
c |   1138673 |   92520   253569 |   50059   31300   681067    21.8 | 16.344 % |
c |   1139432 |   92159   252501 |   55065   31772   685640    21.6 | 16.548 % |
c |   1140571 |   91644   250827 |   60571   31524   671164    21.3 | 16.810 % |
c |   1142280 |   91644   250827 |   66629   33233   738837    22.2 | 16.810 % |
c ==============================================================================
c Found solution: -11810562
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1144659 |   91658   250875 |   30552   35612   800860    22.5 | 16.810 % |
c |   1144760 |   88234   242916 |   33607   35508   796118    22.4 | 20.253 % |
c |   1144911 |   88234   242916 |   36967   35659   800651    22.5 | 20.253 % |
c |   1145136 |   88234   242916 |   40664   35884   805278    22.4 | 20.253 % |
c |   1145476 |   88049   242381 |   44731   36190   809698    22.4 | 20.370 % |
c |   1145982 |   88049   242381 |   49204   36696   826083    22.5 | 20.370 % |
c |   1146742 |   87212   240433 |   54124   37373   849466    22.7 | 21.113 % |
c |   1147881 |   87212   240433 |   59537   38512   901321    23.4 | 21.113 % |
c |   1149589 |   85603   236636 |   65490   39958   938100    23.5 | 22.620 % |
c |   1152151 |   85582   236561 |   72040   42505  1039150    24.4 | 22.632 % |
c ==============================================================================
c Found solution: -11810566
c ---[   0]---> Sorter-cost: 1837     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1155889 |   89766   246167 |   29922   46146  1211542    26.3 | 22.632 % |
c |   1155989 |   89766   246167 |   32914   21056   486668    23.1 | 21.695 % |
c |   1156139 |   89547   245492 |   36205   20984   487173    23.2 | 21.824 % |
c |   1156366 |   89547   245492 |   39826   21211   493405    23.3 | 21.824 % |
c |   1156703 |   89212   244368 |   43808   21476   498880    23.2 | 21.953 % |
c |   1157210 |   89159   244181 |   48189   21940   514619    23.5 | 21.979 % |
c |   1157970 |   88759   243011 |   53008   22668   535837    23.6 | 22.252 % |
c |   1159109 |   88759   243011 |   58309   23807   582364    24.5 | 22.252 % |
c |   1160817 |   88260   241728 |   64140   25466   648053    25.4 | 22.703 % |
c |   1163380 |   88058   241077 |   70554   28009   753079    26.9 | 22.795 % |
c |   1167227 |   87589   239655 |   77609   31808   851143    26.8 | 23.062 % |
c ==============================================================================
c Found solution: -11811067
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1169670 |   87593   239687 |   29197   34245   931895    27.2 | 23.062 % |
c |   1169770 |   87416   239101 |   32116   34282   931805    27.2 | 23.191 % |
c |   1169921 |   87416   239101 |   35328   34433   935235    27.2 | 23.191 % |
c |   1170146 |   87395   239030 |   38861   34655   940566    27.1 | 23.200 % |
c |   1170484 |   87271   238605 |   42747   34917   950661    27.2 | 23.283 % |
c |   1170990 |   87254   238546 |   47022   35420   961650    27.1 | 23.292 % |
c |   1171750 |   87254   238546 |   51724   36180   989033    27.3 | 23.292 % |
c |   1172893 |   87121   238153 |   56896   37269  1021896    27.4 | 23.361 % |
c |   1174601 |   87121   238153 |   62586   38977  1067981    27.4 | 23.361 % |
c ==============================================================================
c Found solution: -11829510
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1175835 |   87162   238263 |   29054   40200  1099898    27.4 | 23.361 % |
c |   1175935 |   87162   238263 |   31959   20200   363469    18.0 | 23.355 % |
c |   1176085 |   87162   238263 |   35155   20350   365140    17.9 | 23.355 % |
c |   1176311 |   87162   238263 |   38670   20576   371623    18.1 | 23.355 % |
c |   1176649 |   87162   238263 |   42537   20914   378074    18.1 | 23.355 % |
c |   1177155 |   87162   238263 |   46791   21420   390340    18.2 | 23.355 % |
c |   1177915 |   87082   237981 |   51470   22164   414093    18.7 | 23.384 % |
c |   1179054 |   86810   237140 |   56618   23263   440872    19.0 | 23.553 % |
c |   1180762 |   86810   237140 |   62279   24971   500301    20.0 | 23.553 % |
c |   1183324 |   86791   237098 |   68507   27532   593995    21.6 | 23.568 % |
c ==============================================================================
c Found solution: -11829548
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1185602 |   86802   237128 |   28934   29810   670718    22.5 | 23.568 % |
c |   1185703 |   86802   237128 |   31827   29911   672475    22.5 | 23.566 % |
c |   1185854 |   86802   237128 |   35010   30062   674852    22.4 | 23.566 % |
c |   1186081 |   86802   237128 |   38511   30289   680560    22.5 | 23.566 % |
c |   1186418 |   86802   237128 |   42362   30626   690629    22.6 | 23.566 % |
c |   1186926 |   86802   237128 |   46598   31134   706594    22.7 | 23.566 % |
c ==============================================================================
c Found solution: -11830019
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1187505 |   86813   237156 |   28937   31713   729344    23.0 | 23.566 % |
c |   1187605 |   86813   237156 |   31830   31813   730795    23.0 | 23.564 % |
c |   1187755 |   86813   237156 |   35013   31963   733645    23.0 | 23.564 % |
c |   1187980 |   86813   237156 |   38515   32188   737947    22.9 | 23.564 % |
c |   1188317 |   86813   237156 |   42366   32525   744189    22.9 | 23.564 % |
c |   1188826 |   86813   237156 |   46603   33034   752944    22.8 | 23.564 % |
c |   1189585 |   86813   237156 |   51263   33793   778897    23.0 | 23.564 % |
c |   1190724 |   86813   237156 |   56390   34932   820877    23.5 | 23.564 % |
c |   1192432 |   86813   237156 |   62029   36640   906092    24.7 | 23.564 % |
c ==============================================================================
c Found solution: -11830110
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1193143 |   86828   237193 |   28942   37351   947660    25.4 | 23.564 % |
c |   1193243 |   86828   237193 |   31836   18776   403216    21.5 | 23.561 % |
c |   1193394 |   86828   237193 |   35019   18927   405350    21.4 | 23.561 % |
c |   1193619 |   86828   237193 |   38521   19152   408518    21.3 | 23.561 % |
c |   1193958 |   86828   237193 |   42373   19491   416451    21.4 | 23.561 % |
c |   1194464 |   86828   237193 |   46611   19997   430086    21.5 | 23.561 % |
c |   1195223 |   86754   236925 |   51272   20744   449415    21.7 | 23.596 % |
c |   1196363 |   86625   236616 |   56399   21880   480085    21.9 | 23.710 % |
c |   1198072 |   86625   236616 |   62039   23589   526181    22.3 | 23.710 % |
c |   1200635 |   86614   236592 |   68243   26151   603001    23.1 | 23.719 % |
c |   1204480 |   86614   236592 |   75068   29996   686594    22.9 | 23.719 % |
c ==============================================================================
c Found solution: -11831691
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1209726 |   86179   235590 |   28726   35216   885313    25.1 | 23.719 % |
c |   1209827 |   86179   235590 |   31598   35317   887076    25.1 | 24.114 % |
c |   1209978 |   86167   235563 |   34758   35463   889381    25.1 | 24.128 % |
c |   1210206 |   86167   235563 |   38234   35691   893975    25.0 | 24.128 % |
c |   1210543 |   86167   235563 |   42057   36028   901331    25.0 | 24.128 % |
c |   1211051 |   86167   235563 |   46263   36536   912818    25.0 | 24.128 % |
c |   1211810 |   85224   233359 |   50889   37197   931812    25.1 | 24.956 % |
c |   1212949 |   85224   233359 |   55978   38336   975249    25.4 | 24.956 % |
c |   1214661 |   85051   232965 |   61576   40041  1031905    25.8 | 25.096 % |
c |   1217223 |   84981   232805 |   67734   42599  1132156    26.6 | 25.162 % |
c ==============================================================================
c Found solution: -11831872
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1220708 |   84847   232448 |   28282   46067  1249091    27.1 | 25.162 % |
c |   1220809 |   84847   232448 |   31110   21674   450563    20.8 | 25.291 % |
c |   1220960 |   84847   232448 |   34221   21825   452360    20.7 | 25.291 % |
c |   1221185 |   84847   232448 |   37643   22050   455273    20.6 | 25.291 % |
c |   1221523 |   84847   232448 |   41407   22388   461849    20.6 | 25.291 % |
c |   1222030 |   84847   232448 |   45548   22895   471635    20.6 | 25.291 % |
c |   1222789 |   84836   232409 |   50103   23571   481909    20.4 | 25.297 % |
c |   1223929 |   84836   232409 |   55113   24711   522516    21.1 | 25.297 % |
c |   1225637 |   84836   232409 |   60624   26419   586412    22.2 | 25.297 % |
c ==============================================================================
c Found solution: -11831937
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1227363 |   84851   232446 |   28283   28145   661850    23.5 | 25.297 % |
c |   1227463 |   84851   232446 |   31111   28245   664796    23.5 | 25.293 % |
c |   1227613 |   84851   232446 |   34222   28395   667303    23.5 | 25.293 % |
c |   1227840 |   84851   232446 |   37644   28622   673326    23.5 | 25.293 % |
c |   1228178 |   84851   232446 |   41409   28960   678835    23.4 | 25.293 % |
c |   1228684 |   84811   232357 |   45550   29465   686762    23.3 | 25.325 % |
c |   1229443 |   84811   232357 |   50105   30224   709516    23.5 | 25.325 % |
c |   1230584 |   84568   231800 |   55115   31362   748095    23.9 | 25.537 % |
c |   1232292 |   84463   231500 |   60627   33068   806805    24.4 | 25.625 % |
c |   1234854 |   84409   231320 |   66689   35605   903022    25.4 | 25.643 % |
c |   1238701 |   84409   231320 |   73358   39452   989709    25.1 | 25.643 % |
c ==============================================================================
c Found solution: -11831957
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1241419 |   84427   231363 |   28142   42170  1073037    25.4 | 25.643 % |
c |   1241520 |   84427   231363 |   30956   21186   391329    18.5 | 25.638 % |
c |   1241671 |   84427   231363 |   34051   21337   394020    18.5 | 25.638 % |
c |   1241900 |   84427   231363 |   37457   21566   398463    18.5 | 25.638 % |
c |   1242238 |   84427   231363 |   41202   21904   404793    18.5 | 25.638 % |
c |   1242744 |   84427   231363 |   45322   22410   414265    18.5 | 25.638 % |
c |   1243505 |   84427   231363 |   49855   23171   455124    19.6 | 25.638 % |
c |   1244645 |   84427   231363 |   54840   24311   484024    19.9 | 25.638 % |
c |   1246354 |   84427   231363 |   60324   26020   545550    21.0 | 25.638 % |
c ==============================================================================
c Found solution: -11850813
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1247799 |   84487   231511 |   28162   27465   594782    21.7 | 25.638 % |
c |   1247901 |   84487   231511 |   30978   27567   596980    21.7 | 25.617 % |
c |   1248051 |   84487   231511 |   34076   27717   598994    21.6 | 25.617 % |
c |   1248278 |   84487   231511 |   37483   27944   604141    21.6 | 25.617 % |
c |   1248615 |   84473   231479 |   41231   28280   609968    21.6 | 25.634 % |
c |   1249121 |   84473   231479 |   45355   28786   618534    21.5 | 25.634 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -X02_bit_10 -X02_bit_9 X02_bit_8 -X02_bit_7 X02_bit_6 -X02_bit_5 -X02_bit_4 -X02_bit_3 -X02_bit_2 X02_bit_1 X02_bit0 X02_bit1 X02_bit2 -X02_bit3 X02_bit4 -X02_bit5 -X02_bit6 -X02_bit7 -X02_bit8 -X02_bit9 -X02_bit10 -X02_bit11 -X02_bit12 -X02_bit13 -X02_bit14 -X02_bit15 -X02_bit16 -X02_bit17 -X02_bit18 -X02_bit19 X14_bit_10 X14_bit_9 X14_bit_8 -X14_bit_7 X14_bit_6 X14_bit_5 X14_bit_4 X14_bit_3 -X14_bit_2 X14_bit_1 -X14_bit0 -X14_bit1 -X14_bit2 -X14_bit3 X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 -X14_bit13 -X14_bit14 -X14_bit15 -X14_bit16 -X14_bit17 -X14_bit18 -X14_bit19 X23_bit_10 X23_bit_9 X23_bit_8 -X23_bit_7 X23_bit_6 -X23_bit_5 -X23_bit_4 X23_bit_3 X23_bit_2 -X23_bit_1 -X23_bit0 -X23_bit1 X23_bit2 X23_bit3 X23_bit4 -X23_bit5 X23_bit6 X23_bit7 X23_bit8 -X23_bit9 -X23_bit10 -X23_bit11 -X23_bit12 -X23_bit13 -X23_bit14 -X23_bit15 -X23_bit16 -X23_bit17 -X23_bit18 -X23_bit19 X36_bit_10 X36_bit_9 X36_bit_8 X36_bit_7 X36_bit_6 -X36_bit_5 -X36_bit_4 -X36_bit_3 X36_bit_2 -X36_bit_1 -X36_bit0 -X36_bit1 X36_bit2 -X36_bit3 X36_bit4 -X36_bit5 X36_bit6 -X36_bit7 X36_bit8 -X36_bit9 -X36_bit10 -X36_bit11 -X36_bit12 -X36_bit13 -X36_bit14 -X36_bit15 -X36_bit16 -X36_bit17 -X36_bit18 -X36_bit19 -X39_bit_10 -X39_bit_9 -X39_bit_8 X39_bit_7 -X39_bit_6 X39_bit_5 X39_bit_4 -X39_bit_3 -X39_bit_2 -X39_bit_1 -X39_bit0 -X39_bit1 -X39_bit2 -X39_bit3 -X39_bit4 -X39_bit5 -X39_bit6 -X39_bit7 -X39_bit8 -X39_bit9 -X39_bit10 -X39_bit11 -X39_bit12 -X39_bit13 -X39_bit14 -X39_bit15 -X39_bit16 -X39_bit17 -X39_bit18 -X39_bit19 -X01_bit_10 -X01_bit_9 X01_bit_8 X01_bit_7 X01_bit_6 -X01_bit_5 -X01_bit_4 -X01_bit_3 -X01_bit_2 -X01_bit_1 -X01_bit0 X01_bit1 X01_bit2 X01_bit3 -X01_bit4 -X01_bit5 X01_bit6 -X01_bit7 -X01_bit8 -X01_bit9 -X01_bit10 -X01_bit11 -X01_bit12 -X01_bit13 -X01_bit14 -X01_bit15 -X01_bit16 -X01_bit17 -X01_bit18 -X01_bit19 -X03_bit_10 -X03_bit_9 -X03_bit_8 X03_bit_7 -X03_bit_6 -X03_bit_5 -X03_bit_4 -X03_bit_3 -X03_bit_2 X03_bit_1 -X03_bit0 X03_bit1 X03_bit2 -X03_bit3 X03_bit4 X03_bit5 -X03_bit6 -X03_bit7 -X03_bit8 -X03_bit9 -X03_bit10 -X03_bit11 -X03_bit12 -X03_bit13 -X03_bit14 -X03_bit15 -X03_bit16 -X03_bit17 -X03_bit18 -X03_bit19 -X04_bit_10 X04_bit_9 X04_bit_8 -X04_bit_7 X04_bit_6 -X04_bit_5 X04_bit_4 X04_bit_3 -X04_bit_2 X04_bit_1 -X04_bit0 X04_bit1 -X04_bit2 -X04_bit3 X04_bit4 -X04_bit5 X04_bit6 -X04_bit7 -X04_bit8 -X04_bit9 -X04_bit10 -X04_bit11 -X04_bit12 -X04_bit13 -X04_bit14 -X04_bit15 -X04_bit16 -X04_bit17 -X04_bit18 -X04_bit19 -X06_bit_10 X06_bit_9 -X06_bit_8 X06_bit_7 -X06_bit_6 X06_bit_5 X06_bit_4 -X06_bit_3 -X06_bit_2 X06_bit_1 -X06_bit0 -X06_bit1 X06_bit2 -X06_bit3 -X06_bit4 -X06_bit5 X06_bit6 -X06_bit7 -X06_bit8 -X06_bit9 -X06_bit10 -X06_bit11 -X06_bit12 -X06_bit13 -X06_bit14 -X06_bit15 -X06_bit16 -X06_bit17 -X06_bit18 -X06_bit19 -X07_bit_10 -X07_bit_9 -X07_bit_8 -X07_bit_7 -X07_bit_6 -X07_bit_5 -X07_bit_4 -X07_bit_3 -X07_bit_2 -X07_bit_1 -X07_bit0 -X07_bit1 -X07_bit2 -X07_bit3 -X07_bit4 -X07_bit5 -X07_bit6 -X07_bit7 -X07_bit8 -X07_bit9 -X07_bit10 -X07_bit11 -X07_bit12 -X07_bit13 -X07_bit14 -X07_bit15 -X07_bit16 -X07_bit17 -X07_bit18 -X07_bit19 -X08_bit_10 -X08_bit_9 -X08_bit_8 -X08_bit_7 -X08_bit_6 -X08_bit_5 -X08_bit_4 -X08_bit_3 -X08_bit_2 -X08_bit_1 -X08_bit0 -X08_bit1 -X08_bit2 -X08_bit3 -X08_bit4 -X08_bit5 -X08_bit6 -X08_bit7 -X08_bit8 -X08_bit9 -X08_bit10 -X08_bit11 -X08_bit12 -X08_bit13 -X08_bit14 -X08_bit15 -X08_bit16 -X08_bit17 -X08_bit18 -X08_bit19 -X09_bit_10 -X09_bit_9 -X09_bit_8 -X09_bit_7 -X09_bit_6 -X09_bit_5 -X09_bit_4 -X09_bit_3 -X09_bit_2 -X09_bit_1 -X09_bit0 -X09_bit1 -X09_bit2 -X09_bit3 -X09_bit4 -X09_bit5 -X09_bit6 -X09_bit7 -X09_bit8 -X09_bit9 -X09_bit10 -X09_bit11 -X09_bit12 -X09_bit13 -X09_bit14 -X09_bit15 -X09_bit16 -X09_bit17 -X09_bit18 -X09_bit19 X15_bit_10 X15_bit_9 -X15_bit_8 -X15_bit_7 X15_bit_6 X15_bit_5 X15_bit_4 -X15_bit_3 X15_bit_2 X15_bit_1 X15_bit0 X15_bit1 -X15_bit2 -X15_bit3 X15_bit4 X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 -X15_bit13 -X15_bit14 -X15_bit15 -X15_bit16 -X15_bit17 -X15_bit18 -X15_bit19 X16_bit_10 -X16_bit_9 -X16_bit_8 -X16_bit_7 -X16_bit_6 X16_bit_5 X16_bit_4 X16_bit_3 -X16_bit_2 X16_bit_1 -X16_bit0 -X16_bit1 -X16_bit2 X16_bit3 -X16_bit4 -X16_bit5 X16_bit6 -X16_bit7 -X16_bit8 -X16_bit9 -X16_bit10 -X16_bit11 -X16_bit12 -X16_bit13 -X16_bit14 -X16_bit15 -X16_bit16 -X16_bit17 -X16_bit18 -X16_bit19 -X22_bit_10 -X22_bit_9 -X22_bit_8 -X22_bit_7 -X22_bit_6 -X22_bit_5 -X22_bit_4 -X22_bit_3 -X22_bit_2 -X22_bit_1 -X22_bit0 -X22_bit1 X22_bit2 -X22_bit3 X22_bit4 X22_bit5 X22_bit6 X22_bit7 X22_bit8 -X22_bit9 -X22_bit10 -X22_bit11 -X22_bit12 -X22_bit13 -X22_bit14 -X22_bit15 -X22_bit16 -X22_bit17 -X22_bit18 -X22_bit19 X24_bit_10 X24_bit_9 -X24_bit_8 -X24_bit_7 X24_bit_6 X24_bit_5 X24_bit_4 X24_bit_3 X24_bit_2 -X24_bit_1 X24_bit0 X24_bit1 X24_bit2 -X24_bit3 X24_bit4 -X24_bit5 -X24_bit6 -X24_bit7 -X24_bit8 -X24_bit9 -X24_bit10 -X24_bit11 -X24_bit12 -X24_bit13 -X24_bit14 -X24_bit15 -X24_bit16 -X24_bit17 -X24_bit18 -X24_bit19 -X25_bit_10 X25_bit_9 X25_bit_8 -X25_bit_7 X25_bit_6 X25_bit_5 X25_bit_4 -X25_bit_3 -X25_bit_2 -X25_bit_1 -X25_bit0 -X25_bit1 -X25_bit2 -X25_bit3 -X25_bit4 -X25_bit5 -X25_bit6 -X25_bit7 -X25_bit8 -X25_bit9 -X25_bit10 -X25_bit11 -X25_bit12 -X25_bit13 -X25_bit14 -X25_bit15 -X25_bit16 -X25_bit17 -X25_bit18 -X25_bit19 -X26_bit_10 -X26_bit_9 -X26_bit_8 -X26_bit_7 -X26_bit_6 -X26_bit_5 -X26_bit_4 -X26_bit_3 -X26_bit_2 -X26_bit_1 X26_bit0 X26_bit1 X26_bit2 -X26_bit3 X26_bit4 -X26_bit5 X26_bit6 X26_bit7 -X26_bit8 -X26_bit9 -X26_bit10 -X26_bit11 -X26_bit12 -X26_bit13 -X26_bit14 -X26_bit15 -X26_bit16 -X26_bit17 -X26_bit18 -X26_bit19 -X28_bit_10 X28_bit_9 -X28_bit_8 -X28_bit_7 X28_bit_6 -X28_bit_5 -X28_bit_4 -X28_bit_3 -X28_bit_2 -X28_bit_1 -X28_bit0 X28_bit1 X28_bit2 X28_bit3 X28_bit4 X28_bit5 -X28_bit6 X28_bit7 -X28_bit8 -X28_bit9 -X28_bit10 -X28_bit11 -X28_bit12 -X28_bit13 -X28_bit14 -X28_bit15 -X28_bit16 -X28_bit17 -X28_bit18 -X28_bit19 -X29_bit_10 X29_bit_9 X29_bit_8 -X29_bit_7 X29_bit_6 -X29_bit_5 -X29_bit_4 -X29_bit_3 -X29_bit_2 -X29_bit_1 -X29_bit0 -X29_bit1 -X29_bit2 -X29_bit3 -X29_bit4 -X29_bit5 -X29_bit6 -X29_bit7 -X29_bit8 -X29_bit9 -X29_bit10 -X29_bit11 -X29_bit12 -X29_bit13 -X29_bit14 -X29_bit15 -X29_bit16 -X29_bit17 -X29_bit18 -X29_bit19 -X30_bit_10 -X30_bit_9 -X30_bit_8 -X30_bit_7 -X30_bit_6 -X30_bit_5 -X30_bit_4 -X30_bit_3 -X30_bit_2 -X30_bit_1 -X30_bit0 -X30_bit1 -X30_bit2 -X30_bit3 -X30_bit4 -X30_bit5 -X30_bit6 -X30_bit7 -X30_bit8 -X30_bit9 -X30_bit10 -X30_bit11 -X30_bit12 -X30_bit13 -X30_bit14 -X30_bit15 -X30_bit16 -X30_bit17 -X30_bit18 -X30_bit19 -X31_bit_10 -X31_bit_9 -X31_bit_8 -X31_bit_7 -X31_bit_6 -X31_bit_5 -X31_bit_4 -X31_bit_3 -X31_bit_2 -X31_bit_1 -X31_bit0 -X31_bit1 -X31_bit2 -X31_bit3 -X31_bit4 -X31_bit5 -X31_bit6 -X31_bit7 -X31_bit8 -X31_bit9 -X31_bit10 -X31_bit11 -X31_bit12 -X31_bit13 -X31_bit14 -X31_bit15 -X31_bit16 -X31_bit17 -X31_bit18 -X31_bit19 -X38_bit_10 X38_bit_9 X38_bit_8 X38_bit_7 X38_bit_6 -X38_bit_5 X38_bit_4 X38_bit_3 -X38_bit_2 X38_bit_1 X38_bit0 -X38_bit1 -X38_bit2 -X38_bit3 X38_bit4 -X38_bit5 X38_bit6 -X38_bit7 -X38_bit8 -X38_bit9 -X38_bit10 -X38_bit11 -X38_bit12 -X38_bit13 -X38_bit14 -X38_bit15 -X38_bit16 -X38_bit17 -X38_bit18 -X38_bit19 X37_bit_10 X37_bit_9 X37_bit_8 X37_bit_7 -X37_bit_6 -X37_bit_5 -X37_bit_4 X37_bit_3 -X37_bit_2 -X37_bit_1 -X37_bit0 X37_bit1 -X37_bit2 -X37_bit3 -X37_bit4 -X37_bit5 X37_bit6 X37_bit7 -X37_bit8 -X37_bit9 -X37_bit10 -X37_bit11 -X37_bit12 -X37_bit13 -X37_bit14 -X37_bit15 -X37_bit16 -X37_bit17 -X37_bit18 -X37_bit19 -X10_bit_10 -X10_bit_9 -X10_bit_8 -X10_bit_7 -X10_bit_6 -X10_bit_5 -X10_bit_4 -X10_bit_3 -X10_bit_2 -X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 -X10_bit13 -X10_bit14 -X10_bit15 -X10_bit16 -X10_bit17 -X10_bit18 -X10_bit19 X11_bit_10 -X11_bit_9 -X11_bit_8 -X11_bit_7 -X11_bit_6 -X11_bit_5 -X11_bit_4 -X11_bit_3 -X11_bit_2 -X11_bit_1 -X11_bit0 -X11_bit1 -X11_bit2 -X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 -X11_bit13 -X11_bit14 -X11_bi

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/15323/stat): 15323 (minisat+_script) R 15322 15323 2660 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1844021610 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/15323/statm): 174 3 169 147 0 27 0
[pid=15323] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=15324
New process pid=15325
New process pid=15326
execve syscall for /bin/sed executable
One traced child (pid=15325) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=15326) exited with status: 0
One traced child (pid=15324) exited with status: 0
New process pid=15327
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-afiro.opb

[startup+10.0039 s]
Raw data (loadavg): 0.56 0.78 0.88 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 895 0 0 0 990 3 0 0 25 0 1 0 1844021615 2584576 548 4294967295 134512640 135094434 3221224432 3221220928 134600291 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 631 548 145 145 0 486 0
[pid=15327] vsize: 2524
Current children cumulated CPU time (s) 9.94
Current children cumulated vsize (Kb) 4648

[startup+20.0046 s]
Raw data (loadavg): 0.63 0.79 0.88 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 895 0 0 0 1990 3 0 0 25 0 1 0 1844021615 2584576 548 4294967295 134512640 135094434 3221224432 3221221344 134677091 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 631 548 145 145 0 486 0
[pid=15327] vsize: 2524
Current children cumulated CPU time (s) 19.94
Current children cumulated vsize (Kb) 4648

[startup+30.0053 s]
Raw data (loadavg): 0.69 0.79 0.88 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 961 0 0 0 2990 3 0 0 25 0 1 0 1844021615 2674688 572 4294967295 134512640 135094434 3221224432 3221219424 134676328 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 653 572 145 145 0 508 0
[pid=15327] vsize: 2612
Current children cumulated CPU time (s) 29.94
Current children cumulated vsize (Kb) 4736

[startup+40.0061 s]
Raw data (loadavg): 0.73 0.80 0.88 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 2509 0 0 0 3976 9 0 0 25 0 1 0 1844021615 9924608 2110 4294967295 134512640 135094434 3221224432 3221223104 134555802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 2423 2110 145 145 0 2278 0
[pid=15327] vsize: 9692
Current children cumulated CPU time (s) 39.86
Current children cumulated vsize (Kb) 11816

[startup+50.0068 s]
Raw data (loadavg): 0.77 0.81 0.88 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 3121 0 0 0 4966 14 0 0 25 0 1 0 1844021615 12460032 2722 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 3042 2722 145 145 0 2897 0
[pid=15327] vsize: 12168
Current children cumulated CPU time (s) 49.81
Current children cumulated vsize (Kb) 14292

[startup+60.0075 s]
Raw data (loadavg): 0.81 0.81 0.88 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 3775 0 0 0 5954 19 0 0 25 0 1 0 1844021615 15204352 3376 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 3712 3376 145 145 0 3567 0
[pid=15327] vsize: 14848
Current children cumulated CPU time (s) 59.74
Current children cumulated vsize (Kb) 16972

[startup+70.0082 s]
Raw data (loadavg): 0.84 0.82 0.88 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 4252 0 0 0 6946 22 0 0 25 0 1 0 1844021615 17113088 3853 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 4178 3853 145 145 0 4033 0
[pid=15327] vsize: 16712
Current children cumulated CPU time (s) 69.69
Current children cumulated vsize (Kb) 18836

[startup+80.009 s]
Raw data (loadavg): 0.86 0.82 0.89 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 4847 0 0 0 7936 27 0 0 25 0 1 0 1844021615 19492864 4448 4294967295 134512640 135094434 3221224432 3221223024 134557175 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 4759 4448 145 145 0 4614 0
[pid=15327] vsize: 19036
Current children cumulated CPU time (s) 79.64
Current children cumulated vsize (Kb) 21160

[startup+90.0097 s]
Raw data (loadavg): 0.88 0.83 0.89 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 5515 0 0 0 8923 33 0 0 25 0 1 0 1844021615 22441984 5116 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 5479 5116 145 145 0 5334 0
[pid=15327] vsize: 21916
Current children cumulated CPU time (s) 89.57
Current children cumulated vsize (Kb) 24040

[startup+100.01 s]
Raw data (loadavg): 0.90 0.83 0.89 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 5859 0 0 0 9917 35 0 0 25 0 1 0 1844021615 23826432 5460 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 5817 5460 145 145 0 5672 0
[pid=15327] vsize: 23268
Current children cumulated CPU time (s) 99.53
Current children cumulated vsize (Kb) 25392

[startup+110.011 s]
Raw data (loadavg): 0.92 0.84 0.89 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 6287 0 0 0 10911 38 0 0 25 0 1 0 1844021615 25534464 5888 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 6234 5888 145 145 0 6089 0
[pid=15327] vsize: 24936
Current children cumulated CPU time (s) 109.5
Current children cumulated vsize (Kb) 27060

[startup+120.012 s]
Raw data (loadavg): 0.93 0.84 0.89 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 6867 0 0 0 11901 43 0 0 25 0 1 0 1844021615 27865088 6468 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 6803 6468 145 145 0 6658 0
[pid=15327] vsize: 27212
Current children cumulated CPU time (s) 119.45
Current children cumulated vsize (Kb) 29336

[startup+130.013 s]
Raw data (loadavg): 0.94 0.85 0.89 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7073 0 0 0 12898 44 0 0 25 0 1 0 1844021615 28696576 6674 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7006 6674 145 145 0 6861 0
[pid=15327] vsize: 28024
Current children cumulated CPU time (s) 129.43
Current children cumulated vsize (Kb) 30148

[startup+140.013 s]
Raw data (loadavg): 0.95 0.85 0.89 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7073 0 0 0 13898 44 0 0 25 0 1 0 1844021615 28696576 6674 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7006 6674 145 145 0 6861 0
[pid=15327] vsize: 28024
Current children cumulated CPU time (s) 139.43
Current children cumulated vsize (Kb) 30148

[startup+150.014 s]
Raw data (loadavg): 0.95 0.86 0.89 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7073 0 0 0 14898 45 0 0 25 0 1 0 1844021615 28696576 6674 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7006 6674 145 145 0 6861 0
[pid=15327] vsize: 28024
Current children cumulated CPU time (s) 149.44
Current children cumulated vsize (Kb) 30148

[startup+160.015 s]
Raw data (loadavg): 0.96 0.86 0.89 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7073 0 0 0 15898 45 0 0 25 0 1 0 1844021615 28696576 6674 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7006 6674 145 145 0 6861 0
[pid=15327] vsize: 28024
Current children cumulated CPU time (s) 159.44
Current children cumulated vsize (Kb) 30148

[startup+170.015 s]
Raw data (loadavg): 0.97 0.86 0.89 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7073 0 0 0 16898 45 0 0 25 0 1 0 1844021615 28696576 6674 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7006 6674 145 145 0 6861 0
[pid=15327] vsize: 28024
Current children cumulated CPU time (s) 169.44
Current children cumulated vsize (Kb) 30148

[startup+180.016 s]
Raw data (loadavg): 0.97 0.87 0.89 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7174 0 0 0 17898 45 0 0 25 0 1 0 1844021615 28778496 6775 4294967295 134512640 135094434 3221224432 3221223088 134558232 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7026 6775 145 145 0 6881 0
[pid=15327] vsize: 28104
Current children cumulated CPU time (s) 179.44
Current children cumulated vsize (Kb) 30228

[startup+190.017 s]
Raw data (loadavg): 0.98 0.87 0.90 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7205 0 0 0 18898 46 0 0 25 0 1 0 1844021615 28938240 6806 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7065 6806 145 145 0 6920 0
[pid=15327] vsize: 28260
Current children cumulated CPU time (s) 189.45
Current children cumulated vsize (Kb) 30384

[startup+200.018 s]
Raw data (loadavg): 0.98 0.88 0.90 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7205 0 0 0 19898 46 0 0 25 0 1 0 1844021615 28938240 6806 4294967295 134512640 135094434 3221224432 3221223068 134557639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7065 6806 145 145 0 6920 0
[pid=15327] vsize: 28260
Current children cumulated CPU time (s) 199.45
Current children cumulated vsize (Kb) 30384

[startup+210.018 s]
Raw data (loadavg): 0.98 0.88 0.90 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7226 0 0 0 20898 46 0 0 25 0 1 0 1844021615 28938240 6827 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7065 6827 145 145 0 6920 0
[pid=15327] vsize: 28260
Current children cumulated CPU time (s) 209.45
Current children cumulated vsize (Kb) 30384

[startup+220.018 s]
Raw data (loadavg): 0.98 0.88 0.90 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7226 0 0 0 21898 46 0 0 25 0 1 0 1844021615 28938240 6827 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7065 6827 145 145 0 6920 0
[pid=15327] vsize: 28260
Current children cumulated CPU time (s) 219.45
Current children cumulated vsize (Kb) 30384

[startup+230.019 s]
Raw data (loadavg): 0.99 0.89 0.90 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7226 0 0 0 22898 46 0 0 25 0 1 0 1844021615 28938240 6827 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7065 6827 145 145 0 6920 0
[pid=15327] vsize: 28260
Current children cumulated CPU time (s) 229.45
Current children cumulated vsize (Kb) 30384

[startup+240.02 s]
Raw data (loadavg): 0.99 0.89 0.90 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7228 0 0 0 23898 47 0 0 25 0 1 0 1844021615 28938240 6829 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7065 6829 145 145 0 6920 0
[pid=15327] vsize: 28260
Current children cumulated CPU time (s) 239.46
Current children cumulated vsize (Kb) 30384

[startup+250.02 s]
Raw data (loadavg): 0.99 0.89 0.90 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7228 0 0 0 24898 47 0 0 25 0 1 0 1844021615 28938240 6829 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7065 6829 145 145 0 6920 0
[pid=15327] vsize: 28260
Current children cumulated CPU time (s) 249.46
Current children cumulated vsize (Kb) 30384

[startup+260.021 s]
Raw data (loadavg): 0.99 0.90 0.90 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7228 0 0 0 25898 47 0 0 25 0 1 0 1844021615 28938240 6829 4294967295 134512640 135094434 3221224432 3221223024 134557016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15327/statm): 7065 6829 145 145 0 6920 0
[pid=15327] vsize: 28260
Current children cumulated CPU time (s) 259.46
Current children cumulated vsize (Kb) 30384

[startup+270.022 s]
Raw data (loadavg): 0.99 0.90 0.90 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7255 0 0 0 26897 47 0 0 25 0 1 0 1844021615 28938240 6856 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7065 6856 145 145 0 6920 0
[pid=15327] vsize: 28260
Current children cumulated CPU time (s) 269.45
Current children cumulated vsize (Kb) 30384

[startup+280.023 s]
Raw data (loadavg): 0.99 0.90 0.90 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7281 0 0 0 27897 48 0 0 25 0 1 0 1844021615 29593600 6882 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6882 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 279.46
Current children cumulated vsize (Kb) 31024

[startup+290.024 s]
Raw data (loadavg): 0.99 0.90 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7281 0 0 0 28897 48 0 0 25 0 1 0 1844021615 29593600 6882 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6882 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 289.46
Current children cumulated vsize (Kb) 31024

[startup+300.025 s]
Raw data (loadavg): 0.99 0.91 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7285 0 0 0 29897 48 0 0 25 0 1 0 1844021615 29593600 6886 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6886 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 299.46
Current children cumulated vsize (Kb) 31024

[startup+310.026 s]
Raw data (loadavg): 0.99 0.91 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7285 0 0 0 30897 48 0 0 25 0 1 0 1844021615 29593600 6886 4294967295 134512640 135094434 3221224432 3221223056 134562085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6886 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 309.46
Current children cumulated vsize (Kb) 31024

[startup+320.025 s]
Raw data (loadavg): 0.99 0.91 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7286 0 0 0 31897 48 0 0 25 0 1 0 1844021615 29593600 6887 4294967295 134512640 135094434 3221224432 3221223056 134562085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6887 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 319.46
Current children cumulated vsize (Kb) 31024

[startup+330.026 s]
Raw data (loadavg): 0.99 0.91 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7286 0 0 0 32897 48 0 0 25 0 1 0 1844021615 29593600 6887 4294967295 134512640 135094434 3221224432 3221223072 134562128 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6887 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 329.46
Current children cumulated vsize (Kb) 31024

[startup+340.027 s]
Raw data (loadavg): 0.99 0.92 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7286 0 0 0 33897 48 0 0 25 0 1 0 1844021615 29593600 6887 4294967295 134512640 135094434 3221224432 3221223072 134562165 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6887 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 339.46
Current children cumulated vsize (Kb) 31024

[startup+350.029 s]
Raw data (loadavg): 0.99 0.92 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7286 0 0 0 34897 48 0 0 25 0 1 0 1844021615 29593600 6887 4294967295 134512640 135094434 3221224432 3221223104 134555687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6887 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 349.46
Current children cumulated vsize (Kb) 31024

[startup+360.029 s]
Raw data (loadavg): 0.99 0.92 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7286 0 0 0 35898 48 0 0 25 0 1 0 1844021615 29593600 6887 4294967295 134512640 135094434 3221224432 3221223056 134557627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6887 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 359.47
Current children cumulated vsize (Kb) 31024

[startup+370.03 s]
Raw data (loadavg): 0.99 0.92 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7286 0 0 0 36898 49 0 0 25 0 1 0 1844021615 29593600 6887 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6887 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 369.48
Current children cumulated vsize (Kb) 31024

[startup+380.031 s]
Raw data (loadavg): 0.99 0.92 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7286 0 0 0 37898 49 0 0 25 0 1 0 1844021615 29593600 6887 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6887 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 379.48
Current children cumulated vsize (Kb) 31024

[startup+390.031 s]
Raw data (loadavg): 0.99 0.93 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7287 0 0 0 38898 49 0 0 25 0 1 0 1844021615 29593600 6888 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6888 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 389.48
Current children cumulated vsize (Kb) 31024

[startup+400.032 s]
Raw data (loadavg): 0.99 0.93 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7287 0 0 0 39898 49 0 0 25 0 1 0 1844021615 29593600 6888 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6888 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 399.48
Current children cumulated vsize (Kb) 31024

[startup+410.033 s]
Raw data (loadavg): 0.99 0.93 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7287 0 0 0 40898 49 0 0 25 0 1 0 1844021615 29593600 6888 4294967295 134512640 135094434 3221224432 3221223104 134556094 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6888 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 409.48
Current children cumulated vsize (Kb) 31024

[startup+420.034 s]
Raw data (loadavg): 0.99 0.93 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7287 0 0 0 41898 49 0 0 25 0 1 0 1844021615 29593600 6888 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6888 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 419.48
Current children cumulated vsize (Kb) 31024

[startup+430.034 s]
Raw data (loadavg): 0.99 0.93 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7287 0 0 0 42898 49 0 0 25 0 1 0 1844021615 29593600 6888 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6888 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 429.48
Current children cumulated vsize (Kb) 31024

[startup+440.034 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7287 0 0 0 43898 49 0 0 25 0 1 0 1844021615 29593600 6888 4294967295 134512640 135094434 3221224432 3221223056 134557604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6888 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 439.48
Current children cumulated vsize (Kb) 31024

[startup+450.036 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7287 0 0 0 44899 49 0 0 25 0 1 0 1844021615 29593600 6888 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6888 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 449.49
Current children cumulated vsize (Kb) 31024

[startup+460.036 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7287 0 0 0 45899 49 0 0 25 0 1 0 1844021615 29593600 6888 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6888 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 459.49
Current children cumulated vsize (Kb) 31024

[startup+470.037 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7287 0 0 0 46899 49 0 0 25 0 1 0 1844021615 29593600 6888 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6888 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 469.49
Current children cumulated vsize (Kb) 31024

[startup+480.038 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7287 0 0 0 47899 49 0 0 25 0 1 0 1844021615 29593600 6888 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6888 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 479.49
Current children cumulated vsize (Kb) 31024

[startup+490.039 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7310 0 0 0 48899 49 0 0 25 0 1 0 1844021615 29593600 6911 4294967295 134512640 135094434 3221224432 3221223072 134562108 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6911 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 489.49
Current children cumulated vsize (Kb) 31024

[startup+500.039 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7310 0 0 0 49899 50 0 0 25 0 1 0 1844021615 29593600 6911 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6911 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 499.5
Current children cumulated vsize (Kb) 31024

[startup+510.04 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7314 0 0 0 50899 50 0 0 25 0 1 0 1844021615 29593600 6915 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6915 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 509.5
Current children cumulated vsize (Kb) 31024

[startup+520.041 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7314 0 0 0 51899 50 0 0 25 0 1 0 1844021615 29593600 6915 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6915 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 519.5
Current children cumulated vsize (Kb) 31024

[startup+530.042 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7314 0 0 0 52899 50 0 0 25 0 1 0 1844021615 29593600 6915 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6915 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 529.5
Current children cumulated vsize (Kb) 31024

[startup+540.042 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7314 0 0 0 53900 50 0 0 25 0 1 0 1844021615 29593600 6915 4294967295 134512640 135094434 3221224432 3221223220 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6915 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 539.51
Current children cumulated vsize (Kb) 31024

[startup+550.044 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7314 0 0 0 54900 50 0 0 25 0 1 0 1844021615 29593600 6915 4294967295 134512640 135094434 3221224432 3221223104 134556502 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6915 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 549.51
Current children cumulated vsize (Kb) 31024

[startup+560.045 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7314 0 0 0 55900 50 0 0 25 0 1 0 1844021615 29593600 6915 4294967295 134512640 135094434 3221224432 3221223088 134561744 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6915 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 559.51
Current children cumulated vsize (Kb) 31024

[startup+570.045 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7314 0 0 0 56900 50 0 0 25 0 1 0 1844021615 29593600 6915 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6915 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 569.51
Current children cumulated vsize (Kb) 31024

[startup+580.046 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7314 0 0 0 57900 51 0 0 25 0 1 0 1844021615 29593600 6915 4294967295 134512640 135094434 3221224432 3221223088 134561748 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6915 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 579.52
Current children cumulated vsize (Kb) 31024

[startup+590.047 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7314 0 0 0 58900 51 0 0 25 0 1 0 1844021615 29593600 6915 4294967295 134512640 135094434 3221224432 3221223056 134557619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6915 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 589.52
Current children cumulated vsize (Kb) 31024

[startup+600.048 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7314 0 0 0 59900 51 0 0 25 0 1 0 1844021615 29593600 6915 4294967295 134512640 135094434 3221224432 3221223056 134557583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6915 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 599.52
Current children cumulated vsize (Kb) 31024

[startup+610.048 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7314 0 0 0 60900 51 0 0 25 0 1 0 1844021615 29593600 6915 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6915 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 609.52
Current children cumulated vsize (Kb) 31024

[startup+620.049 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7314 0 0 0 61900 51 0 0 25 0 1 0 1844021615 29593600 6915 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6915 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 619.52
Current children cumulated vsize (Kb) 31024

[startup+630.05 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7314 0 0 0 62901 51 0 0 25 0 1 0 1844021615 29593600 6915 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6915 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 629.53
Current children cumulated vsize (Kb) 31024

[startup+640.051 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7314 0 0 0 63901 51 0 0 25 0 1 0 1844021615 29593600 6915 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6915 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 639.53
Current children cumulated vsize (Kb) 31024

[startup+650.052 s]
Raw data (loadavg): 1.07 0.98 0.91 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7314 0 0 0 64901 51 0 0 25 0 1 0 1844021615 29593600 6915 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6915 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 649.53
Current children cumulated vsize (Kb) 31024

[startup+660.053 s]
Raw data (loadavg): 1.14 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7314 0 0 0 65901 51 0 0 25 0 1 0 1844021615 29593600 6915 4294967295 134512640 135094434 3221224432 3221223088 134558411 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6915 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 659.53
Current children cumulated vsize (Kb) 31024

[startup+670.054 s]
Raw data (loadavg): 1.11 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7314 0 0 0 66901 51 0 0 25 0 1 0 1844021615 29593600 6915 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6915 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 669.53
Current children cumulated vsize (Kb) 31024

[startup+680.054 s]
Raw data (loadavg): 1.10 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7314 0 0 0 67901 51 0 0 25 0 1 0 1844021615 29593600 6915 4294967295 134512640 135094434 3221224432 3221223024 134557393 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6915 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 679.53
Current children cumulated vsize (Kb) 31024

[startup+690.055 s]
Raw data (loadavg): 1.08 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7316 0 0 0 68901 53 0 0 25 0 1 0 1844021615 29593600 6917 4294967295 134512640 135094434 3221224432 3221223088 134558232 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6917 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 689.55
Current children cumulated vsize (Kb) 31024

[startup+700.056 s]
Raw data (loadavg): 1.07 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7340 0 0 0 69900 53 0 0 25 0 1 0 1844021615 29593600 6941 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6941 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 699.54
Current children cumulated vsize (Kb) 31024

[startup+710.057 s]
Raw data (loadavg): 1.06 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7346 0 0 0 70900 53 0 0 25 0 1 0 1844021615 29593600 6947 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6947 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 709.54
Current children cumulated vsize (Kb) 31024

[startup+720.057 s]
Raw data (loadavg): 1.05 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7346 0 0 0 71900 54 0 0 25 0 1 0 1844021615 29593600 6947 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6947 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 719.55
Current children cumulated vsize (Kb) 31024

[startup+730.058 s]
Raw data (loadavg): 1.04 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7347 0 0 0 72900 54 0 0 25 0 1 0 1844021615 29593600 6948 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6948 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 729.55
Current children cumulated vsize (Kb) 31024

[startup+740.058 s]
Raw data (loadavg): 1.03 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7347 0 0 0 73900 54 0 0 25 0 1 0 1844021615 29593600 6948 4294967295 134512640 135094434 3221224432 3221223104 134555896 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6948 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 739.55
Current children cumulated vsize (Kb) 31024

[startup+750.058 s]
Raw data (loadavg): 1.03 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7347 0 0 0 74900 54 0 0 25 0 1 0 1844021615 29593600 6948 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6948 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 749.55
Current children cumulated vsize (Kb) 31024

[startup+760.059 s]
Raw data (loadavg): 1.02 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7347 0 0 0 75900 54 0 0 25 0 1 0 1844021615 29593600 6948 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6948 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 759.55
Current children cumulated vsize (Kb) 31024

[startup+770.06 s]
Raw data (loadavg): 1.02 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7349 0 0 0 76900 55 0 0 25 0 1 0 1844021615 29593600 6950 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6950 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 769.56
Current children cumulated vsize (Kb) 31024

[startup+780.061 s]
Raw data (loadavg): 1.02 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7349 0 0 0 77900 55 0 0 25 0 1 0 1844021615 29593600 6950 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6950 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 779.56
Current children cumulated vsize (Kb) 31024

[startup+790.061 s]
Raw data (loadavg): 1.01 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7349 0 0 0 78899 55 0 0 25 0 1 0 1844021615 29593600 6950 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6950 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 789.55
Current children cumulated vsize (Kb) 31024

[startup+800.062 s]
Raw data (loadavg): 1.01 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7349 0 0 0 79899 55 0 0 25 0 1 0 1844021615 29593600 6950 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6950 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 799.55
Current children cumulated vsize (Kb) 31024

[startup+810.063 s]
Raw data (loadavg): 1.01 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7350 0 0 0 80899 55 0 0 25 0 1 0 1844021615 29593600 6951 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6951 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 809.55
Current children cumulated vsize (Kb) 31024

[startup+820.063 s]
Raw data (loadavg): 1.01 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7350 0 0 0 81900 55 0 0 25 0 1 0 1844021615 29593600 6951 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6951 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 819.56
Current children cumulated vsize (Kb) 31024

[startup+830.065 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7350 0 0 0 82900 56 0 0 25 0 1 0 1844021615 29593600 6951 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6951 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 829.57
Current children cumulated vsize (Kb) 31024

[startup+840.066 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7350 0 0 0 83900 56 0 0 25 0 1 0 1844021615 29593600 6951 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6951 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 839.57
Current children cumulated vsize (Kb) 31024

[startup+850.067 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7350 0 0 0 84900 56 0 0 25 0 1 0 1844021615 29593600 6951 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6951 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 849.57
Current children cumulated vsize (Kb) 31024

[startup+860.067 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7350 0 0 0 85900 56 0 0 25 0 1 0 1844021615 29593600 6951 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6951 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 859.57
Current children cumulated vsize (Kb) 31024

[startup+870.068 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7350 0 0 0 86900 56 0 0 25 0 1 0 1844021615 29593600 6951 4294967295 134512640 135094434 3221224432 3221223056 134557604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6951 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 869.57
Current children cumulated vsize (Kb) 31024

[startup+880.069 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7350 0 0 0 87900 56 0 0 25 0 1 0 1844021615 29593600 6951 4294967295 134512640 135094434 3221224432 3221223088 134558392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6951 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 879.57
Current children cumulated vsize (Kb) 31024

[startup+890.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7350 0 0 0 88900 56 0 0 25 0 1 0 1844021615 29593600 6951 4294967295 134512640 135094434 3221224432 3221223104 134556297 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6951 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 889.57
Current children cumulated vsize (Kb) 31024

[startup+900.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7350 0 0 0 89900 56 0 0 25 0 1 0 1844021615 29593600 6951 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6951 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 899.57
Current children cumulated vsize (Kb) 31024

[startup+910.071 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7350 0 0 0 90901 57 0 0 25 0 1 0 1844021615 29593600 6951 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6951 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 909.59
Current children cumulated vsize (Kb) 31024

[startup+920.072 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7350 0 0 0 91901 57 0 0 25 0 1 0 1844021615 29593600 6951 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6951 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 919.59
Current children cumulated vsize (Kb) 31024

[startup+930.073 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7350 0 0 0 92901 57 0 0 25 0 1 0 1844021615 29593600 6951 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6951 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 929.59
Current children cumulated vsize (Kb) 31024

[startup+940.074 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7350 0 0 0 93901 57 0 0 25 0 1 0 1844021615 29593600 6951 4294967295 134512640 135094434 3221224432 3221223088 134558156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7225 6951 145 145 0 7080 0
[pid=15327] vsize: 28900
Current children cumulated CPU time (s) 939.59
Current children cumulated vsize (Kb) 31024

[startup+950.076 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 7454 0 0 0 94899 58 0 0 25 0 1 0 1844021615 30019584 7055 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7329 7055 145 145 0 7184 0
[pid=15327] vsize: 29316
Current children cumulated CPU time (s) 949.58
Current children cumulated vsize (Kb) 31440

[startup+960.077 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 8018 0 0 0 95889 63 0 0 25 0 1 0 1844021615 32329728 7619 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 7893 7619 145 145 0 7748 0
[pid=15327] vsize: 31572
Current children cumulated CPU time (s) 959.53
Current children cumulated vsize (Kb) 33696

[startup+970.076 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 8526 0 0 0 96879 68 0 0 25 0 1 0 1844021615 34410496 8127 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 8401 8127 145 145 0 8256 0
[pid=15327] vsize: 33604
Current children cumulated CPU time (s) 969.48
Current children cumulated vsize (Kb) 35728

[startup+980.077 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 8995 0 0 0 97871 72 0 0 25 0 1 0 1844021615 36343808 8596 4294967295 134512640 135094434 3221224432 3221223056 134557633 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 8873 8596 145 145 0 8728 0
[pid=15327] vsize: 35492
Current children cumulated CPU time (s) 979.44
Current children cumulated vsize (Kb) 37616

[startup+990.078 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 9358 0 0 0 98864 75 0 0 25 0 1 0 1844021615 37826560 8959 4294967295 134512640 135094434 3221224432 3221223088 134557882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 9235 8959 145 145 0 9090 0
[pid=15327] vsize: 36940
Current children cumulated CPU time (s) 989.4
Current children cumulated vsize (Kb) 39064

[startup+1000.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 9549 0 0 0 99861 77 0 0 25 0 1 0 1844021615 38633472 9150 4294967295 134512640 135094434 3221224432 3221223104 134555553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 9432 9150 145 145 0 9287 0
[pid=15327] vsize: 37728
Current children cumulated CPU time (s) 999.39
Current children cumulated vsize (Kb) 39852

[startup+1010.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 9549 0 0 0 100861 77 0 0 25 0 1 0 1844021615 38633472 9150 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 9432 9150 145 145 0 9287 0
[pid=15327] vsize: 37728
Current children cumulated CPU time (s) 1009.39
Current children cumulated vsize (Kb) 39852

[startup+1020.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 9549 0 0 0 101861 77 0 0 25 0 1 0 1844021615 38633472 9150 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 9432 9150 145 145 0 9287 0
[pid=15327] vsize: 37728
Current children cumulated CPU time (s) 1019.39
Current children cumulated vsize (Kb) 39852

[startup+1030.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 9549 0 0 0 102861 77 0 0 25 0 1 0 1844021615 38633472 9150 4294967295 134512640 135094434 3221224432 3221223088 134557896 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 9432 9150 145 145 0 9287 0
[pid=15327] vsize: 37728
Current children cumulated CPU time (s) 1029.39
Current children cumulated vsize (Kb) 39852

[startup+1040.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 9549 0 0 0 103861 77 0 0 25 0 1 0 1844021615 38633472 9150 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 9432 9150 145 145 0 9287 0
[pid=15327] vsize: 37728
Current children cumulated CPU time (s) 1039.39
Current children cumulated vsize (Kb) 39852

[startup+1050.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 9550 0 0 0 104861 77 0 0 25 0 1 0 1844021615 38633472 9151 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 9432 9151 145 145 0 9287 0
[pid=15327] vsize: 37728
Current children cumulated CPU time (s) 1049.39
Current children cumulated vsize (Kb) 39852

[startup+1060.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 9550 0 0 0 105862 77 0 0 25 0 1 0 1844021615 38633472 9151 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 9432 9151 145 145 0 9287 0
[pid=15327] vsize: 37728
Current children cumulated CPU time (s) 1059.4
Current children cumulated vsize (Kb) 39852

[startup+1070.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 9550 0 0 0 106862 77 0 0 25 0 1 0 1844021615 38633472 9151 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 9432 9151 145 145 0 9287 0
[pid=15327] vsize: 37728
Current children cumulated CPU time (s) 1069.4
Current children cumulated vsize (Kb) 39852

[startup+1080.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 9550 0 0 0 107862 77 0 0 25 0 1 0 1844021615 38633472 9151 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 9432 9151 145 145 0 9287 0
[pid=15327] vsize: 37728
Current children cumulated CPU time (s) 1079.4
Current children cumulated vsize (Kb) 39852

[startup+1090.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 9662 0 0 0 108862 78 0 0 25 0 1 0 1844021615 40468480 9263 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 9880 9263 145 145 0 9735 0
[pid=15327] vsize: 39520
Current children cumulated CPU time (s) 1089.41
Current children cumulated vsize (Kb) 41644

[startup+1100.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 9665 0 0 0 109861 78 0 0 25 0 1 0 1844021615 40468480 9266 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 9880 9266 145 145 0 9735 0
[pid=15327] vsize: 39520
Current children cumulated CPU time (s) 1099.4
Current children cumulated vsize (Kb) 41644

[startup+1110.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 9689 0 0 0 110861 78 0 0 25 0 1 0 1844021615 40468480 9290 4294967295 134512640 135094434 3221224432 3221223120 134554705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 9880 9290 145 145 0 9735 0
[pid=15327] vsize: 39520
Current children cumulated CPU time (s) 1109.4
Current children cumulated vsize (Kb) 41644

[startup+1120.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 9689 0 0 0 111861 78 0 0 25 0 1 0 1844021615 40468480 9290 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 9880 9290 145 145 0 9735 0
[pid=15327] vsize: 39520
Current children cumulated CPU time (s) 1119.4
Current children cumulated vsize (Kb) 41644

[startup+1130.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 9698 0 0 0 112862 78 0 0 25 0 1 0 1844021615 40468480 9299 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 9880 9299 145 145 0 9735 0
[pid=15327] vsize: 39520
Current children cumulated CPU time (s) 1129.41
Current children cumulated vsize (Kb) 41644

[startup+1140.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 9698 0 0 0 113862 78 0 0 25 0 1 0 1844021615 40468480 9299 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 9880 9299 145 145 0 9735 0
[pid=15327] vsize: 39520
Current children cumulated CPU time (s) 1139.41
Current children cumulated vsize (Kb) 41644

[startup+1150.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 9698 0 0 0 114862 78 0 0 25 0 1 0 1844021615 40468480 9299 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 9880 9299 145 145 0 9735 0
[pid=15327] vsize: 39520
Current children cumulated CPU time (s) 1149.41
Current children cumulated vsize (Kb) 41644

[startup+1160.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 9698 0 0 0 115862 78 0 0 25 0 1 0 1844021615 40468480 9299 4294967295 134512640 135094434 3221224432 3221221456 134677351 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 9880 9299 145 145 0 9735 0
[pid=15327] vsize: 39520
Current children cumulated CPU time (s) 1159.41
Current children cumulated vsize (Kb) 41644

[startup+1170.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 9698 0 0 0 116863 78 0 0 25 0 1 0 1844021615 40468480 9299 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 9880 9299 145 145 0 9735 0
[pid=15327] vsize: 39520
Current children cumulated CPU time (s) 1169.42
Current children cumulated vsize (Kb) 41644

[startup+1180.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 9698 0 0 0 117862 79 0 0 25 0 1 0 1844021615 40468480 9299 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 9880 9299 145 145 0 9735 0
[pid=15327] vsize: 39520
Current children cumulated CPU time (s) 1179.42
Current children cumulated vsize (Kb) 41644

[startup+1190.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 9698 0 0 0 118863 79 0 0 25 0 1 0 1844021615 40468480 9299 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 9880 9299 145 145 0 9735 0
[pid=15327] vsize: 39520
Current children cumulated CPU time (s) 1189.43
Current children cumulated vsize (Kb) 41644

[startup+1200.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 9698 0 0 0 119863 79 0 0 25 0 1 0 1844021615 40468480 9299 4294967295 134512640 135094434 3221224432 3221223092 134556596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 9880 9299 145 145 0 9735 0
[pid=15327] vsize: 39520
Current children cumulated CPU time (s) 1199.43
Current children cumulated vsize (Kb) 41644

[startup+1210.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 9698 0 0 0 120863 79 0 0 25 0 1 0 1844021615 40468480 9299 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 9880 9299 145 145 0 9735 0
[pid=15327] vsize: 39520
Current children cumulated CPU time (s) 1209.43
Current children cumulated vsize (Kb) 41644



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 15327
Raw data (/proc/15323/stat): 15323 (minisat+_script) S 15322 15323 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844021610 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15323/statm): 531 226 485 147 0 384 0
[pid=15323] vsize: 2124
Raw data (/proc/15327/stat): 15327 (minisat+_64-bit) R 15323 15323 2660 0 -1 0 9698 0 0 0 120863 79 0 0 25 0 1 0 1844021615 40468480 9299 4294967295 134512640 135094434 3221224432 3221223056 134557694 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15327/statm): 9880 9299 145 145 0 9735 0
[pid=15327] vsize: 39520
Current children cumulated CPU time (s) 1209.43
Current children cumulated vsize (Kb) 41644

Sending SIGTERM to -15323
Sleeping 2 seconds
One traced child (pid=15323) ended because it received signal 15 (SIGTERM)
One traced child (pid=15327) exited with status: 10
All traced children have exited ! Game is over.

Child status: 10
Real time (s): 1210.12
CPU time (s): 1209.45
CPU user time (s): 1208.64
CPU system time (s): 0.811876
CPU usage (%): 99.9445
Max. virtual memory (cumulated for all children) (Kb): 41644

Verifier Data

ERROR: no interpretation found !