PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-neos5.opb
MD5SUM	e6bff154156b54af3a9a38f7579209b6
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	17324
Optimality of the best value was proved	NO
Number of terms in the objective function	163
Biggest coefficient in the objective function	1024
Number of bits for the biggest coefficient in the objective function	11
Sum of the numbers in the objective function	74742
Number of bits of the sum of numbers in the objective function	17
Biggest number in a constraint	8192
Number of bits of the biggest number in a constraint	14
Biggest sum of numbers in a constraint	74742
Number of bits of the biggest sum of numbers	17
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.06984
Number of variables	163
Total number of constraints	126
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	56
Number of constraints which are nor clauses,nor cardinality constraints	70
Minimum length of a constraint	1
Maximum length of a constraint	102
Trace number 32122

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-05-27 08:12:35 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23488 boxname=wulflinc4 idbench=1132 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  e6bff154156b54af3a9a38f7579209b6  /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-neos5.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-neos5.opb
IDLAUNCH: 23488
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        814724 kB
Buffers:         33684 kB
Cached:         165736 kB
SwapCached:        500 kB
Active:          52624 kB
Inactive:       149164 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        814472 kB
SwapTotal:     2097136 kB
SwapFree:      2096004 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5788 kB
Slab:            12404 kB
Committed_AS:    71792 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-27 08:33:05 (client local time) WITH STATUS 152 IN 1229.85 SECONDS
stats: 23488 7 1229.85 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 73 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[  72]---> BDD-cost:   10
c ---[  71]---> BDD-cost:   10
c ---[  70]---> BDD-cost:   10
c ---[  69]---> BDD-cost:   10
c ---[  68]---> BDD-cost:   10
c ---[  67]---> BDD-cost:   10
c ---[  66]---> BDD-cost:   10
c ---[  65]---> BDD-cost:   10
c ---[  64]---> BDD-cost:   10
c ---[  63]---> BDD-cost:   10
c ---[  62]---> BDD-cost:  199
c ---[  61]---> BDD-cost:  363
c ---[  60]---> BDD-cost:  147
c ---[  59]---> BDD-cost:  768
c ---[  58]---> BDD-cost:  468
c ---[  57]---> BDD-cost:  147
c ---[  56]---> BDD-cost:  608
c ---[  55]---> BDD-cost:  468
c ---[  54]---> BDD-cost:  468
c ---[  53]---> BDD-cost:  147
c ---[  52]---> BDD-cost:  608
c ---[  51]---> BDD-cost:  100
c ---[  50]---> BDD-cost:  468
c ---[  49]---> BDD-cost:  606
c ---[  48]---> BDD-cost:  250
c ---[  47]---> BDD-cost:  174
c ---[  46]---> BDD-cost:  177
c ---[  45]---> BDD-cost:  129
c ---[  44]---> BDD-cost:  176
c ---[  43]---> BDD-cost:  177
c ---[  42]---> BDD-cost:  129
c ---[  41]---> BDD-cost:  176
c ---[  40]---> BDD-cost:  171
c ---[  39]---> BDD-cost:  129
c ---[  38]---> BDD-cost:  581
c ---[  37]---> BDD-cost:  176
c ---[  36]---> BDD-cost:  177
c ---[  35]---> BDD-cost:  129
c ---[  34]---> BDD-cost:  176
c ---[  33]---> BDD-cost:  129
c ---[  32]---> BDD-cost:  581
c ---[  31]---> BDD-cost:  177
c ---[  30]---> BDD-cost:  129
c ---[  29]---> BDD-cost:  173
c ---[  28]---> BDD-cost:  444
c ---[  27]---> BDD-cost:  581
c ---[  26]---> BDD-cost:  110
c ---[  25]---> BDD-cost:  110
c ---[  24]---> BDD-cost:  110
c ---[  23]---> BDD-cost:  150
c ---[  22]---> BDD-cost:  110
c ---[  21]---> BDD-cost:  110
c ---[  20]---> BDD-cost:  110
c ---[  19]---> BDD-cost:  150
c ---[  18]---> BDD-cost:  175
c ---[  17]---> BDD-cost:  110
c ---[  16]---> BDD-cost:  110
c ---[  15]---> BDD-cost:  150
c ---[  14]---> BDD-cost:  110
c ---[  13]---> BDD-cost:  150
c ---[  12]---> BDD-cost:  110
c ---[  11]---> BDD-cost:  418
c ---[  10]---> BDD-cost:   90
c ---[   9]---> BDD-cost:   90
c ---[   8]---> BDD-cost:   90
c ---[   7]---> BDD-cost:  175
c ---[   6]---> BDD-cost:   90
c ---[   5]---> BDD-cost:  122
c ---[   4]---> BDD-cost:   90
c ---[   3]---> BDD-cost:   69
c ---[   2]---> BDD-cost:  181
c ---[   1]---> BDD-cost:  193
c ---[   0]---> BDD-cost:  147
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   38216   113117 |   12738       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 29697[0m
c ---[   0]---> Sorter-cost: 3374     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   44970   128900 |   14990       0        0     nan |  0.000 % |
c |       100 |   44970   128900 |   16489     100      596     6.0 |  0.428 % |
c |       251 |   44970   128900 |   18137     251     1549     6.2 |  0.428 % |
c ==============================================================================
c [1mFound solution: 21963[0m
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       450 |   45047   129099 |   15015     450     2812     6.2 |  0.428 % |
c |       550 |   45047   129099 |   16516     550     4172     7.6 |  0.433 % |
c |       700 |   45047   129099 |   18168     700     5822     8.3 |  0.433 % |
c |       925 |   45047   129099 |   19984     925     8796     9.5 |  0.433 % |
c ==============================================================================
c [1mFound solution: 20219[0m
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       979 |   45072   129163 |   15024     979     9148     9.3 |  0.433 % |
c |      1082 |   45072   129163 |   16526    1082    10773    10.0 |  0.438 % |
c |      1232 |   45072   129163 |   18179    1232    11901     9.7 |  0.438 % |
c |      1457 |   45072   129163 |   19996    1457    13547     9.3 |  0.438 % |
c |      1795 |   45072   129163 |   21996    1795    24684    13.8 |  0.438 % |
c |      2303 |   45072   129163 |   24196    2303    31039    13.5 |  0.438 % |
c |      3063 |   45072   129163 |   26615    3063    48131    15.7 |  0.438 % |
c |      4202 |   45072   129163 |   29277    4202    71867    17.1 |  0.438 % |
c ==============================================================================
c [1mFound solution: 19943[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5451 |   45080   129188 |   15026    5451    86358    15.8 |  0.438 % |
c |      5551 |   45080   129188 |   16528    5551    87646    15.8 |  0.444 % |
c |      5704 |   45080   129188 |   18181    5704    89470    15.7 |  0.444 % |
c |      5929 |   45080   129188 |   19999    5929    94156    15.9 |  0.444 % |
c |      6267 |   45080   129188 |   21999    6267    97789    15.6 |  0.444 % |
c |      6773 |   45080   129188 |   24199    6773   104367    15.4 |  0.444 % |
c ==============================================================================
c [1mFound solution: 19942[0m
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7273 |   45108   129262 |   15036    7273   109570    15.1 |  0.444 % |
c |      7373 |   45108   129262 |   16539    7373   111221    15.1 |  0.449 % |
c |      7523 |   45108   129262 |   18193    7523   112313    14.9 |  0.449 % |
c |      7748 |   45108   129262 |   20012    7748   116589    15.0 |  0.449 % |
c |      8085 |   45108   129262 |   22014    8085   120472    14.9 |  0.449 % |
c ==============================================================================
c [1mFound solution: 18550[0m
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8459 |   45118   129289 |   15039    8459   129457    15.3 |  0.449 % |
c ==============================================================================
c [1mFound solution: 18329[0m
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8512 |   45148   129369 |   15049    8512   130576    15.3 |  0.449 % |
c |      8612 |   45142   129357 |   16553    8582   132027    15.4 |  0.477 % |
c |      8762 |   45142   129357 |   18209    8732   134291    15.4 |  0.477 % |
c |      8990 |   45142   129357 |   20030    8960   137640    15.4 |  0.477 % |
c |      9328 |   45142   129357 |   22033    9298   143509    15.4 |  0.477 % |
c |      9836 |   45142   129357 |   24236    9806   155537    15.9 |  0.477 % |
c |     10595 |   45142   129357 |   26660   10565   172988    16.4 |  0.477 % |
c |     11735 |   45142   129357 |   29326   11705   185659    15.9 |  0.477 % |
c |     13444 |   45142   129357 |   32258   13414   225240    16.8 |  0.477 % |
c |     16007 |   45142   129357 |   35484   15977   337754    21.1 |  0.477 % |
c |     19851 |   45142   129357 |   39033   19821   429705    21.7 |  0.477 % |
c ==============================================================================
c [1mFound solution: 17910[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22838 |   45148   129377 |   15049   22808   493591    21.6 |  0.477 % |
c |     22938 |   45148   129377 |   16553   11504   278856    24.2 |  0.483 % |
c |     23089 |   45148   129377 |   18209   11655   283539    24.3 |  0.483 % |
c |     23314 |   45148   129377 |   20030   11880   289063    24.3 |  0.483 % |
c |     23651 |   45148   129377 |   22033   12217   296504    24.3 |  0.483 % |
c |     24158 |   45148   129377 |   24236   12724   312622    24.6 |  0.483 % |
c |     24917 |   45148   129377 |   26660   13483   336779    25.0 |  0.483 % |
c |     26058 |   45148   129377 |   29326   14624   360791    24.7 |  0.483 % |
c |     27766 |   45148   129377 |   32258   16332   390294    23.9 |  0.483 % |
c ==============================================================================
c [1mFound solution: 17908[0m
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28097 |   45156   129405 |   15052   16663   395852    23.8 |  0.483 % |
c |     28198 |   45156   129405 |   16557    8433   163786    19.4 |  0.489 % |
c |     28349 |   45156   129405 |   18212    8584   166466    19.4 |  0.489 % |
c |     28575 |   45156   129405 |   20034    8810   174167    19.8 |  0.489 % |
c |     28913 |   45156   129405 |   22037    9148   180336    19.7 |  0.489 % |
c |     29419 |   45156   129405 |   24241    9654   193330    20.0 |  0.489 % |
c |     30178 |   45154   129401 |   26665   10410   227671    21.9 |  0.494 % |
c |     31318 |   45154   129401 |   29332   11550   256723    22.2 |  0.494 % |
c |     33027 |   45154   129401 |   32265   13259   304794    23.0 |  0.494 % |
c |     35589 |   45154   129401 |   35491   15821   369487    23.4 |  0.494 % |
c |     39433 |   45154   129401 |   39041   19665   470920    23.9 |  0.494 % |
c ==============================================================================
c [1mFound solution: 17907[0m
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     44851 |   45156   129411 |   15052   21563   494051    22.9 |  0.494 % |
c |     44951 |   45156   129411 |   16557   10806   191548    17.7 |  0.511 % |
c |     45101 |   45156   129411 |   18212   10956   194077    17.7 |  0.511 % |
c |     45326 |   45156   129411 |   20034   11181   197764    17.7 |  0.511 % |
c |     45664 |   45156   129411 |   22037   11519   207314    18.0 |  0.511 % |
c |     46170 |   45156   129411 |   24241   12025   216411    18.0 |  0.511 % |
c |     46931 |   45156   129411 |   26665   12786   230651    18.0 |  0.511 % |
c ==============================================================================
c [1mFound solution: 17906[0m
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     47662 |   45164   129435 |   15054   13517   240957    17.8 |  0.511 % |
c |     47762 |   45164   129435 |   16559   13617   243021    17.8 |  0.517 % |
c |     47914 |   45164   129435 |   18215   13769   247263    18.0 |  0.517 % |
c |     48140 |   45164   129435 |   20036   13995   252411    18.0 |  0.517 % |
c |     48477 |   45164   129435 |   22040   14332   255755    17.8 |  0.517 % |
c |     48984 |   45164   129435 |   24244   14839   266946    18.0 |  0.517 % |
c |     49744 |   45164   129435 |   26669   15599   276261    17.7 |  0.517 % |
c |     50883 |   45164   129435 |   29335   16738   302685    18.1 |  0.517 % |
c |     52592 |   45164   129435 |   32269   18447   323906    17.6 |  0.517 % |
c ==============================================================================
c [1mFound solution: 17881[0m
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     54227 |   45164   129438 |   15054   20070   346105    17.2 |  0.517 % |
c |     54328 |   45164   129438 |   16559   10136   133874    13.2 |  0.540 % |
c |     54480 |   45164   129438 |   18215   10288   135748    13.2 |  0.540 % |
c |     54707 |   45164   129438 |   20036   10515   139720    13.3 |  0.540 % |
c |     55045 |   45164   129438 |   22040   10853   145470    13.4 |  0.540 % |
c |     55551 |   45164   129438 |   24244   11359   157053    13.8 |  0.540 % |
c |     56310 |   45164   129438 |   26669   12118   172998    14.3 |  0.540 % |
c |     57451 |   45164   129438 |   29335   13259   217181    16.4 |  0.540 % |
c |     59159 |   45161   129431 |   32269   14735   235735    16.0 |  0.551 % |
c |     61721 |   45161   129431 |   35496   17297   289577    16.7 |  0.551 % |
c |     65566 |   45161   129431 |   39046   21142   451859    21.4 |  0.551 % |
c |     71332 |   45161   129431 |   42950   26908   626497    23.3 |  0.551 % |
c ==============================================================================
c [1mFound solution: 17744[0m
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     73974 |   45174   129462 |   15058   29550   656185    22.2 |  0.551 % |
c |     74074 |   45174   129462 |   16563   14875   330355    22.2 |  0.557 % |
c ==============================================================================
c [1mFound solution: 17708[0m
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     74180 |   45186   129491 |   15062   14981   332367    22.2 |  0.557 % |
c |     74281 |   45186   129491 |   16568   15082   333790    22.1 |  0.562 % |
c |     74431 |   45186   129491 |   18225   15232   337872    22.2 |  0.562 % |
c |     74657 |   45186   129491 |   20047   15458   342958    22.2 |  0.562 % |
c |     74995 |   45186   129491 |   22052   15796   351839    22.3 |  0.562 % |
c |     75503 |   45186   129491 |   24257   16304   374147    22.9 |  0.562 % |
c |     76262 |   45186   129491 |   26683   17063   403068    23.6 |  0.562 % |
c |     77403 |   45186   129491 |   29351   18204   448840    24.7 |  0.562 % |
c |     79111 |   45186   129491 |   32286   19912   527956    26.5 |  0.562 % |
c |     81673 |   45186   129491 |   35515   22474   603312    26.8 |  0.562 % |
c |     85517 |   45186   129491 |   39066   26318   719234    27.3 |  0.562 % |
c |     91283 |   45186   129491 |   42973   32084   873913    27.2 |  0.562 % |
c ==============================================================================
c [1mFound solution: 17707[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     94080 |   45195   129512 |   15065   34881   917537    26.3 |  0.562 % |
c |     94180 |   45195   129512 |   16571    8100   107641    13.3 |  0.568 % |
c |     94330 |   45195   129512 |   18228    8250   110659    13.4 |  0.568 % |
c |     94555 |   45195   129512 |   20051    8475   113822    13.4 |  0.568 % |
c |     94893 |   45195   129512 |   22056    8813   119387    13.5 |  0.568 % |
c ==============================================================================
c [1mFound solution: 17705[0m
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     95339 |   45206   129538 |   15068    9259   126252    13.6 |  0.568 % |
c |     95439 |   45206   129538 |   16574    9359   127798    13.7 |  0.574 % |
c |     95590 |   45206   129538 |   18232    9510   129902    13.7 |  0.574 % |
c |     95816 |   45206   129538 |   20055    9736   132417    13.6 |  0.573 % |
c |     96154 |   45206   129538 |   22061   10074   138763    13.8 |  0.574 % |
c ==============================================================================
c [1mFound solution: 17704[0m
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     96397 |   45217   129564 |   15072   10317   141901    13.8 |  0.574 % |
c |     96497 |   45217   129564 |   16579   10417   143886    13.8 |  0.579 % |
c |     96648 |   45217   129564 |   18237   10568   146385    13.9 |  0.579 % |
c |     96873 |   45217   129564 |   20060   10793   148416    13.8 |  0.579 % |
c |     97211 |   45217   129564 |   22066   11131   156231    14.0 |  0.579 % |
c |     97718 |   45217   129564 |   24273   11638   165552    14.2 |  0.579 % |
c |     98478 |   45217   129564 |   26700   12398   197214    15.9 |  0.579 % |
c |     99618 |   45217   129564 |   29371   13538   214443    15.8 |  0.579 % |
c |    101326 |   45217   129564 |   32308   15246   241163    15.8 |  0.579 % |
c |    103888 |   45217   129564 |   35538   17808   293941    16.5 |  0.579 % |
c |    107732 |   45217   129564 |   39092   21652   452320    20.9 |  0.579 % |
c ==============================================================================
c [1mFound solution: 17670[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    108763 |   45226   129584 |   15075   22683   470067    20.7 |  0.579 % |
c |    108863 |   45226   129584 |   16582   11442   249439    21.8 |  0.585 % |
c |    109014 |   45226   129584 |   18240   11593   251875    21.7 |  0.585 % |
c |    109239 |   45226   129584 |   20064   11818   258172    21.8 |  0.585 % |
c |    109576 |   45226   129584 |   22071   12155   264006    21.7 |  0.585 % |
c |    110082 |   45226   129584 |   24278   12661   272113    21.5 |  0.585 % |
c |    110841 |   45226   129584 |   26706   13420   301628    22.5 |  0.585 % |
c |    111981 |   45226   129584 |   29376   14560   353324    24.3 |  0.585 % |
c ==============================================================================
c [1mFound solution: 17666[0m
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    113497 |   45237   129609 |   15079   16076   376343    23.4 |  0.585 % |
c |    113597 |   45235   129605 |   16586    8137   142448    17.5 |  0.596 % |
c |    113747 |   45235   129605 |   18245    8287   145023    17.5 |  0.596 % |
c |    113972 |   45235   129605 |   20070    8512   148477    17.4 |  0.596 % |
c |    114309 |   45235   129605 |   22077    8849   154191    17.4 |  0.596 % |
c |    114818 |   45235   129605 |   24284    9358   175848    18.8 |  0.596 % |
c |    115579 |   45235   129605 |   26713   10119   188714    18.6 |  0.596 % |
c |    116718 |   45235   129605 |   29384   11258   216825    19.3 |  0.596 % |
c |    118428 |   45235   129605 |   32323   12968   239716    18.5 |  0.596 % |
c |    120991 |   45235   129605 |   35555   15531   280360    18.1 |  0.596 % |
c |    124835 |   45235   129605 |   39111   19375   355471    18.3 |  0.596 % |
c |    130601 |   45235   129605 |   43022   25141   522403    20.8 |  0.596 % |
c |    139250 |   45235   129605 |   47324   33790   721872    21.4 |  0.596 % |
c ==============================================================================
c [1mFound solution: 17665[0m
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    139503 |   45245   129627 |   15081   34043   725424    21.3 |  0.596 % |
c |    139603 |   45245   129627 |   16589    8341   109622    13.1 |  0.602 % |
c |    139753 |   45245   129627 |   18248    8491   111234    13.1 |  0.602 % |
c |    139978 |   45245   129627 |   20072    8716   114482    13.1 |  0.602 % |
c |    140315 |   45245   129627 |   22080    9053   121179    13.4 |  0.602 % |
c ==============================================================================
c [1mFound solution: 17664[0m
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    140528 |   45256   129652 |   15085    9266   124871    13.5 |  0.602 % |
c |    140628 |   45256   129652 |   16593    9366   127928    13.7 |  0.607 % |
c |    140778 |   45256   129652 |   18252    9516   129663    13.6 |  0.607 % |
c |    141003 |   45256   129652 |   20078    9741   134269    13.8 |  0.607 % |
c |    141341 |   45256   129652 |   22085   10079   138173    13.7 |  0.607 % |
c |    141848 |   45256   129652 |   24294   10586   156334    14.8 |  0.607 % |
c |    142607 |   45256   129652 |   26723   11345   173302    15.3 |  0.607 % |
c ==============================================================================
c [1mFound solution: 17591[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    143326 |   45262   129666 |   15087   12064   193899    16.1 |  0.607 % |
c |    143426 |   45262   129666 |   16595   12164   196104    16.1 |  0.613 % |
c |    143577 |   45262   129666 |   18255   12315   199946    16.2 |  0.613 % |
c |    143804 |   45262   129666 |   20080   12542   203900    16.3 |  0.613 % |
c |    144141 |   45262   129666 |   22088   12879   213936    16.6 |  0.613 % |
c |    144647 |   45262   129666 |   24297   13385   221679    16.6 |  0.613 % |
c |    145407 |   45262   129666 |   26727   14145   249299    17.6 |  0.613 % |
c |    146548 |   45262   129666 |   29400   15286   273392    17.9 |  0.613 % |
c |    148256 |   45262   129666 |   32340   16994   307763    18.1 |  0.613 % |
c ==============================================================================
c [1mFound solution: 17590[0m
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    149001 |   45271   129688 |   15090   17739   320641    18.1 |  0.613 % |
c |    149101 |   45271   129688 |   16599    8970   135776    15.1 |  0.618 % |
c |    149252 |   45271   129688 |   18258    9121   138552    15.2 |  0.618 % |
c |    149477 |   45271   129688 |   20084    9346   141060    15.1 |  0.618 % |
c |    149814 |   45271   129688 |   22093    9683   148185    15.3 |  0.618 % |
c |    150320 |   45271   129688 |   24302   10189   155152    15.2 |  0.618 % |
c |    151079 |   45271   129688 |   26732   10948   178788    16.3 |  0.618 % |
c |    152218 |   45271   129688 |   29406   12087   198860    16.5 |  0.618 % |
c ==============================================================================
c [1mFound solution: 17586[0m
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    153213 |   45280   129710 |   15093   13082   214979    16.4 |  0.618 % |
c |    153313 |   45280   129710 |   16602   13182   217732    16.5 |  0.624 % |
c |    153463 |   45280   129710 |   18262   13332   220002    16.5 |  0.624 % |
c |    153689 |   45280   129710 |   20088   13558   226210    16.7 |  0.624 % |
c |    154027 |   45280   129710 |   22097   13896   235837    17.0 |  0.624 % |
c ==============================================================================
c [1mFound solution: 17585[0m
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    154341 |   45289   129732 |   15096   14210   241346    17.0 |  0.624 % |
c |    154441 |   45289   129732 |   16605   14310   244266    17.1 |  0.629 % |
c |    154591 |   45289   129732 |   18266   14460   247696    17.1 |  0.629 % |
c |    154816 |   45289   129732 |   20092   14685   251985    17.2 |  0.629 % |
c |    155153 |   45287   129728 |   22102   15021   254936    17.0 |  0.635 % |
c |    155659 |   45287   129728 |   24312   15527   264999    17.1 |  0.635 % |
c |    156419 |   45287   129728 |   26743   16287   275773    16.9 |  0.635 % |
c |    157558 |   45287   129728 |   29417   17426   288256    16.5 |  0.635 % |
c |    159266 |   45287   129728 |   32359   19134   331560    17.3 |  0.635 % |
c |    161828 |   45287   129728 |   35595   21696   407434    18.8 |  0.635 % |
c ==============================================================================
c [1mFound solution: 17584[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    163924 |   45296   129749 |   15098   23792   454862    19.1 |  0.635 % |
c |    164025 |   45296   129749 |   16607   11997   198621    16.6 |  0.641 % |
c |    164176 |   45296   129749 |   18268   12148   202316    16.7 |  0.641 % |
c |    164401 |   45296   129749 |   20095   12373   205680    16.6 |  0.641 % |
c |    164738 |   45296   129749 |   22104   12710   212026    16.7 |  0.641 % |
c |    165246 |   45296   129749 |   24315   13218   230408    17.4 |  0.641 % |
c |    166006 |   45296   129749 |   26747   13978   249559    17.9 |  0.641 % |
c ==============================================================================
c [1mFound solution: 17526[0m
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    166765 |   45303   129764 |   15101   14737   265748    18.0 |  0.641 % |
c |    166866 |   45303   129764 |   16611   14838   268020    18.1 |  0.646 % |
c |    167016 |   45303   129764 |   18272   14988   270599    18.1 |  0.646 % |
c |    167241 |   45303   129764 |   20099   15213   273825    18.0 |  0.646 % |
c |    167578 |   45303   129764 |   22109   15550   281856    18.1 |  0.646 % |
c ==============================================================================
c [1mFound solution: 17525[0m
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    167931 |   45310   129784 |   15103   15903   287964    18.1 |  0.646 % |
c |    168031 |   45310   129784 |   16613    8052   104714    13.0 |  0.652 % |
c |    168181 |   45310   129784 |   18274    8202   105679    12.9 |  0.652 % |
c |    168409 |   45310   129784 |   20102    8430   108145    12.8 |  0.652 % |
c |    168750 |   45310   129784 |   22112    8771   115494    13.2 |  0.652 % |
c |    169258 |   45310   129784 |   24323    9279   130507    14.1 |  0.652 % |
c |    170017 |   45310   129784 |   26755   10038   149123    14.9 |  0.652 % |
c |    171156 |   45310   129784 |   29431   11177   163357    14.6 |  0.652 % |
c |    172864 |   45310   129784 |   32374   12885   210231    16.3 |  0.652 % |
c ==============================================================================
c [1mFound solution: 17494[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    173207 |   45320   129807 |   15106   13228   214195    16.2 |  0.652 % |
c |    173308 |   45320   129807 |   16616   13329   216012    16.2 |  0.657 % |
c |    173458 |   45320   129807 |   18278   13479   217357    16.1 |  0.657 % |
c |    173683 |   45318   129803 |   20106   13701   219583    16.0 |  0.663 % |
c |    174020 |   45318   129803 |   22116   14038   225445    16.1 |  0.663 % |
c |    174526 |   45318   129803 |   24328   14544   230665    15.9 |  0.663 % |
c ==============================================================================
c [1mFound solution: 17446[0m
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    175063 |   45326   129821 |   15108   15081   239249    15.9 |  0.663 % |
c |    175163 |   45326   129821 |   16618   15181   240968    15.9 |  0.669 % |
c |    175314 |   45326   129821 |   18280   15332   243534    15.9 |  0.669 % |
c |    175539 |   45326   129821 |   20108   15557   248220    16.0 |  0.669 % |
c |    175876 |   45326   129821 |   22119   15894   256913    16.2 |  0.669 % |
c |    176382 |   45326   129821 |   24331   16400   264900    16.2 |  0.669 % |
c |    177141 |   45326   129821 |   26764   17159   286459    16.7 |  0.669 % |
c ==============================================================================
c [1mFound solution: 17445[0m
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    177433 |   45337   129847 |   15112   17451   290547    16.6 |  0.669 % |
c |    177533 |   45337   129847 |   16623    8826    95481    10.8 |  0.674 % |
c |    177683 |   45337   129847 |   18285    8976    98347    11.0 |  0.674 % |
c |    177908 |   45337   129847 |   20114    9201   101894    11.1 |  0.674 % |
c |    178245 |   45337   129847 |   22125    9538   107326    11.3 |  0.674 % |
c |    178752 |   45337   129847 |   24338   10045   116787    11.6 |  0.674 % |
c ==============================================================================
c [1mFound solution: 17430[0m
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    179088 |   45344   129862 |   15114   10381   122242    11.8 |  0.674 % |
c |    179188 |   45344   129862 |   16625   10481   126796    12.1 |  0.680 % |
c |    179338 |   45344   129862 |   18287   10631   131016    12.3 |  0.680 % |
c ==============================================================================
c [1mFound solution: 17429[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    179541 |   45353   129882 |   15117   10834   132998    12.3 |  0.680 % |
c |    179641 |   45353   129882 |   16628   10934   134549    12.3 |  0.685 % |
c |    179791 |   45353   129882 |   18291   11084   137114    12.4 |  0.685 % |
c |    180016 |   45353   129882 |   20120   11309   142304    12.6 |  0.685 % |
c |    180354 |   45353   129882 |   22132   11647   149217    12.8 |  0.685 % |
c |    180860 |   45353   129882 |   24346   12153   159113    13.1 |  0.685 % |
c ==============================================================================
c [1mFound solution: 17428[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    181577 |   45362   129903 |   15120   12870   179956    14.0 |  0.685 % |
c |    181677 |   45362   129903 |   16632   12970   182391    14.1 |  0.691 % |
c |    181827 |   45362   129903 |   18295   13120   185776    14.2 |  0.691 % |
c |    182053 |   45362   129903 |   20124   13346   191843    14.4 |  0.691 % |
c |    182390 |   45362   129903 |   22137   13683   201566    14.7 |  0.691 % |
c |    182897 |   45362   129903 |   24350   14190   216587    15.3 |  0.691 % |
c |    183656 |   45362   129903 |   26786   14949   233329    15.6 |  0.691 % |
c |    184795 |   45362   129903 |   29464   16088   264289    16.4 |  0.691 % |
c |    186503 |   45362   129903 |   32411   17796   315662    17.7 |  0.691 % |
c ==============================================================================
c [1mFound solution: 17427[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    186822 |   45371   129924 |   15123   18115   321510    17.7 |  0.691 % |
c |    186922 |   45371   129924 |   16635    9158   136413    14.9 |  0.697 % |
c |    187072 |   45371   129924 |   18298    9308   138870    14.9 |  0.697 % |
c |    187298 |   45371   129924 |   20128    9534   145509    15.3 |  0.697 % |
c |    187635 |   45371   129924 |   22141    9871   154695    15.7 |  0.697 % |
c |    188142 |   45371   129924 |   24355   10378   169704    16.4 |  0.697 % |
c ==============================================================================
c [1mFound solution: 17426[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    188256 |   45380   129944 |   15126   10492   171355    16.3 |  0.697 % |
c |    188356 |   45380   129944 |   16638   10592   173408    16.4 |  0.702 % |
c |    188509 |   45380   129944 |   18302   10745   176703    16.4 |  0.702 % |
c |    188735 |   45380   129944 |   20132   10971   182669    16.7 |  0.702 % |
c |    189072 |   45380   129944 |   22145   11308   188064    16.6 |  0.702 % |
c |    189579 |   45380   129944 |   24360   11815   195762    16.6 |  0.702 % |
c |    190339 |   45380   129944 |   26796   12575   209096    16.6 |  0.702 % |
c |    191482 |   45380   129944 |   29476   13718   233710    17.0 |  0.702 % |
c |    193190 |   45380   129944 |   32423   15426   263074    17.1 |  0.702 % |
c |    195752 |   45380   129944 |   35666   17988   333864    18.6 |  0.702 % |
c ==============================================================================
c [1mFound solution: 17425[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    196158 |   45389   129964 |   15129   18394   340225    18.5 |  0.702 % |
c |    196258 |   45389   129964 |   16641    9297   128447    13.8 |  0.708 % |
c |    196408 |   45389   129964 |   18306    9447   132555    14.0 |  0.708 % |
c |    196633 |   45389   129964 |   20136    9672   137237    14.2 |  0.708 % |
c |    196971 |   45389   129964 |   22150   10010   145208    14.5 |  0.708 % |
c |    197478 |   45389   129964 |   24365   10517   155366    14.8 |  0.708 % |
c |    198237 |   45389   129964 |   26801   11276   173759    15.4 |  0.708 % |
c |    199377 |   45389   129964 |   29482   12416   192821    15.5 |  0.708 % |
c |    201085 |   45389   129964 |   32430   14124   226614    16.0 |  0.708 % |
c |    203649 |   45389   129964 |   35673   16688   287311    17.2 |  0.708 % |
c ==============================================================================
c [1mFound solution: 17422[0m
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    205292 |   45401   129991 |   15133   18331   343530    18.7 |  0.708 % |
c |    205392 |   45401   129991 |   16646    9266   143788    15.5 |  0.713 % |
c |    205542 |   45401   129991 |   18310    9416   145392    15.4 |  0.713 % |
c |    205768 |   45401   129991 |   20142    9642   148989    15.5 |  0.713 % |
c |    206105 |   45401   129991 |   22156    9979   155217    15.6 |  0.713 % |
c |    206611 |   45401   129991 |   24371   10485   168291    16.1 |  0.713 % |
c |    207370 |   45401   129991 |   26809   11244   182328    16.2 |  0.713 % |
c ==============================================================================
c [1mFound solution: 16390[0m
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    207976 |   45409   130011 |   15136   11850   199471    16.8 |  0.713 % |
c |    208077 |   45409   130011 |   16649   11951   201946    16.9 |  0.719 % |
c |    208227 |   45409   130011 |   18314   12101   204961    16.9 |  0.719 % |
c |    208452 |   45409   130011 |   20146   12326   209392    17.0 |  0.719 % |
c |    208790 |   45409   130011 |   22160   12664   218390    17.2 |  0.719 % |
c |    209297 |   45409   130011 |   24376   13171   225716    17.1 |  0.719 % |
c |    210056 |   45409   130011 |   26814   13930   244150    17.5 |  0.719 % |
c |    211195 |   45409   130011 |   29495   15069   276080    18.3 |  0.719 % |
c |    212904 |   45409   130011 |   32445   16778   325749    19.4 |  0.719 % |
c ==============================================================================
c [1mFound solution: 16386[0m
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    214943 |   45414   130022 |   15138   18817   362124    19.2 |  0.719 % |
c |    215043 |   45414   130022 |   16651    9509   131383    13.8 |  0.724 % |
c |    215193 |   45414   130022 |   18316    9659   135268    14.0 |  0.724 % |
c |    215419 |   45414   130022 |   20148    9885   139858    14.1 |  0.724 % |
c |    215756 |   45414   130022 |   22163   10222   150133    14.7 |  0.724 % |
c |    216264 |   45414   130022 |   24379   10730   164196    15.3 |  0.724 % |
c |    217026 |   45414   130022 |   26817   11492   180266    15.7 |  0.724 % |
c |    218166 |   45414   130022 |   29499   12632   195116    15.4 |  0.724 % |
c |    219874 |   45414   130022 |   32449   14340   243475    17.0 |  0.724 % |
c ==============================================================================
c [1mFound solution: 16385[0m
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    221263 |   45420   130035 |   15140   15729   302709    19.2 |  0.724 % |
c |    221367 |   45420   130035 |   16654    7969   132837    16.7 |  0.730 % |
c |    221518 |   45420   130035 |   18319    8120   136244    16.8 |  0.730 % |
c |    221745 |   45420   130035 |   20151    8347   143499    17.2 |  0.730 % |
c |    222084 |   45420   130035 |   22166    8686   151348    17.4 |  0.730 % |
c |    222591 |   45420   130035 |   24383    9193   164491    17.9 |  0.730 % |
c |    223351 |   45420   130035 |   26821    9953   186282    18.7 |  0.730 % |
c |    224490 |   45420   130035 |   29503   11092   208715    18.8 |  0.730 % |
c |    226199 |   45420   130035 |   32453   12801   260651    20.4 |  0.730 % |
c |    228761 |   45420   130035 |   35699   15363   321071    20.9 |  0.730 % |
c |    232606 |   45420   130035 |   39269   19208   530660    27.6 |  0.730 % |
c |    238372 |   45420   130035 |   43196   24974   614466    24.6 |  0.730 % |
c |    247022 |   45411   130016 |   47515   33618   958943    28.5 |  0.759 % |
c |    259996 |   45411   130016 |   52267   46592  1403324    30.1 |  0.759 % |
c ==============================================================================
c [1mFound solution: 16384[0m
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    276964 |   45416   130027 |   15138   28788   924703    32.1 |  0.759 % |
c |    277066 |   45416   130027 |   16651   14496   431943    29.8 |  0.764 % |
c |    277216 |   45416   130027 |   18316   14646   434769    29.7 |  0.764 % |
c |    277441 |   45416   130027 |   20148   14871   439986    29.6 |  0.764 % |
c |    277779 |   45416   130027 |   22163   15209   442704    29.1 |  0.764 % |
c |    278286 |   45416   130027 |   24379   15716   453389    28.8 |  0.764 % |
c |    279045 |   45416   130027 |   26817   16475   465559    28.3 |  0.764 % |
c |    280184 |   45416   130027 |   29499   17614   493455    28.0 |  0.764 % |
c |    281892 |   45416   130027 |   32449   19322   555797    28.8 |  0.764 % |
c |    284454 |   45416   130027 |   35694   21884   650442    29.7 |  0.764 % |
c |    288298 |   45416   130027 |   39264   25728   850219    33.0 |  0.764 % |
c |    294064 |   45416   130027 |   43190   31494  1089927    34.6 |  0.764 % |
c |    302713 |   45416   130027 |   47509   40143  1450889    36.1 |  0.764 % |
c |    315689 |   45416   130027 |   52260   23375   631232    27.0 |  0.764 % |
c ==============================================================================
c [1mFound solution: 16333[0m
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    329262 |   45434   130073 |   15144   36948  1669939    45.2 |  0.764 % |
c |    329365 |   45434   130073 |   16658    8441   468180    55.5 |  0.786 % |
c |    329517 |   45434   130073 |   18324    8593   471798    54.9 |  0.786 % |
c |    329743 |   45434   130073 |   20156    8819   477245    54.1 |  0.786 % |
c |    330081 |   45434   130073 |   22172    9157   484368    52.9 |  0.786 % |
c |    330587 |   45434   130073 |   24389    9663   496174    51.3 |  0.786 % |
c |    331346 |   45434   130073 |   26828   10422   516398    49.5 |  0.786 % |
c |    332485 |   45434   130073 |   29511   11561   544250    47.1 |  0.786 % |
c |    334193 |   45434   130073 |   32462   13269   602950    45.4 |  0.786 % |
c |    336756 |   45434   130073 |   35708   15832   678476    42.9 |  0.786 % |
c |    340602 |   45434   130073 |   39279   19678   809481    41.1 |  0.786 % |
c |    346368 |   45434   130073 |   43207   25444   977814    38.4 |  0.786 % |
c |    355019 |   45434   130073 |   47528   34095  1346596    39.5 |  0.786 % |
c |    367995 |   45434   130073 |   52281   47071  1869611    39.7 |  0.786 % |
c |    387457 |   45434   130073 |   57509   32553   988593    30.4 |  0.786 % |
c |    416649 |   45434   130073 |   63260   21643   507948    23.5 |  0.786 % |
c ==============================================================================
c [1mFound solution: 16118[0m
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    459125 |   45442   130094 |   15147   64119  2195192    34.2 |  0.786 % |
c |    459227 |   45442   130094 |   16661    9929   219902    22.1 |  0.792 % |
c |    459377 |   45442   130094 |   18327   10079   224220    22.2 |  0.792 % |
c |    459602 |   45442   130094 |   20160   10304   230028    22.3 |  0.792 % |
c |    459939 |   45442   130094 |   22176   10641   241843    22.7 |  0.792 % |
c |    460446 |   45442   130094 |   24394   11148   259194    23.3 |  0.792 % |
c |    461205 |   45442   130094 |   26833   11907   280344    23.5 |  0.792 % |
c |    462344 |   45442   130094 |   29517   13046   318586    24.4 |  0.792 % |
c |    464053 |   45442   130094 |   32468   14755   376570    25.5 |  0.792 % |
c |    466615 |   45442   130094 |   35715   17317   467468    27.0 |  0.792 % |
c |    470460 |   45442   130094 |   39287   21162   616474    29.1 |  0.792 % |
c |    476228 |   45442   130094 |   43216   26930   840213    31.2 |  0.792 % |
c |    484879 |   45442   130094 |   47537   35581  1198988    33.7 |  0.792 % |
c |    497853 |   45442   130094 |   52291   18763   578014    30.8 |  0.792 % |
c |    517316 |   45442   130094 |   57520   38226  1367300    35.8 |  0.792 % |
c |    546510 |   45442   130094 |   63272   29077   944571    32.5 |  0.792 % |
c |    590301 |   45442   130094 |   69600   29740   936634    31.5 |  0.792 % |
c |    655986 |   45442   130094 |   76560   47036  1551733    33.0 |  0.792 % |
c ==============================================================================
c [1mFound solution: 16115[0m
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    695134 |   45449   130113 |   15149   25950  1109611    42.8 |  0.792 % |
c |    695235 |   45449   130113 |   16663   13076   383986    29.4 |  0.797 % |
c |    695387 |   45449   130113 |   18330   13228   385208    29.1 |  0.797 % |
c |    695612 |   45449   130113 |   20163   13453   387240    28.8 |  0.797 % |
c |    695949 |   45449   130113 |   22179   13790   390894    28.3 |  0.797 % |
c |    696455 |   45449   130113 |   24397   14296   402721    28.2 |  0.797 % |
c |    697214 |   45449   130113 |   26837   15055   428611    28.5 |  0.797 % |
c |    698353 |   45449   130113 |   29521   16194   463269    28.6 |  0.797 % |
c |    700061 |   45449   130113 |   32473   17902   511684    28.6 |  0.797 % |
c |    702624 |   45449   130113 |   35720   20465   587691    28.7 |  0.797 % |
c |    706468 |   45449   130113 |   39292   24309   723802    29.8 |  0.797 % |
c |    712234 |   45449   130113 |   43221   30075   910355    30.3 |  0.797 % |
c |    720883 |   45449   130113 |   47544   38724  1193104    30.8 |  0.797 % |
c ==============================================================================
c [1mFound solution: 16114[0m
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    730427 |   45456   130131 |   15152   48268  1482551    30.7 |  0.797 % |
c |    730527 |   45456   130131 |   16667    8762   115223    13.2 |  0.803 % |
c |    730677 |   45456   130131 |   18333    8912   118418    13.3 |  0.803 % |
c |    730903 |   45456   130131 |   20167    9138   124304    13.6 |  0.803 % |
c |    731240 |   45456   130131 |   22184    9475   131690    13.9 |  0.803 % |
c |    731746 |   45456   130131 |   24402    9981   145132    14.5 |  0.803 % |
c |    732505 |   45456   130131 |   26842   10740   167390    15.6 |  0.803 % |
c |    733644 |   45456   130131 |   29526   11879   201857    17.0 |  0.803 % |
c |    735353 |   45456   130131 |   32479   13588   253888    18.7 |  0.803 % |
c |    737915 |   45456   130131 |   35727   16150   333515    20.7 |  0.803 % |
c |    741759 |   45456   130131 |   39300   19994   451995    22.6 |  0.803 % |
c |    747526 |   45456   130131 |   43230   25761   632647    24.6 |  0.803 % |
c |    756176 |   45456   130131 |   47553   34411  1045292    30.4 |  0.803 % |
c |    769151 |   45456   130131 |   52308   47386  1633754    34.5 |  0.803 % |
c |    788614 |   45456   130131 |   57539   32322   970970    30.0 |  0.803 % |
c ==============================================================================
c [1mFound solution: 16106[0m
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    813879 |   45465   130155 |   15155   57587  2028556    35.2 |  0.803 % |
c |    813979 |   45465   130155 |   16670    8829   169193    19.2 |  0.808 % |
c |    814130 |   45465   130155 |   18337    8980   171065    19.0 |  0.808 % |
c |    814355 |   45465   130155 |   20171    9205   175061    19.0 |  0.808 % |
c |    814692 |   45465   130155 |   22188    9542   181094    19.0 |  0.808 % |
c |    815200 |   45465   130155 |   24407   10050   190585    19.0 |  0.808 % |
c |    815960 |   45465   130155 |   26848   10810   206527    19.1 |  0.808 % |
c |    817100 |   45465   130155 |   29532   11950   226939    19.0 |  0.808 % |
c |    818808 |   45465   130155 |   32486   13658   259149    19.0 |  0.808 % |
c |    821370 |   45465   130155 |   35734   16220   301543    18.6 |  0.808 % |
c |    825214 |   45465   130155 |   39308   20064   365377    18.2 |  0.808 % |
c |    830982 |   45459   130142 |   43238   25827   515423    20.0 |  0.819 % |
c |    839632 |   45459   130142 |   47562   34477   805724    23.4 |  0.819 % |
c |    852606 |   45459   130142 |   52319   47451  1286882    27.1 |  0.819 % |
c ==============================================================================
c [1mFound solution: 16104[0m
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    869468 |   45466   130160 |   15155   25565   995028    38.9 |  0.819 % |
c |    869568 |   45466   130160 |   16670   12883   558145    43.3 |  0.825 % |
c |    869718 |   45466   130160 |   18337   13033   560781    43.0 |  0.825 % |
c |    869943 |   45466   130160 |   20171   13258   564608    42.6 |  0.825 % |
c |    870282 |   45466   130160 |   22188   13597   572034    42.1 |  0.825 % |
c |    870788 |   45466   130160 |   24407   14103   583959    41.4 |  0.825 % |
c |    871549 |   45466   130160 |   26848   14864   599332    40.3 |  0.825 % |
c |    872688 |   45466   130160 |   29532   16003   630638    39.4 |  0.825 % |
c |    874398 |   45466   130160 |   32486   17713   691293    39.0 |  0.825 % |
c |    876962 |   45466   130160 |   35734   20277   778850    38.4 |  0.825 % |
c |    880807 |   45466   130160 |   39308   24122   895786    37.1 |  0.825 % |
c |    886573 |   45466   130160 |   43238   29888  1086512    36.4 |  0.825 % |
c |    895222 |   45466   130160 |   47562   38537  1370282    35.6 |  0.825 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 14890 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.98 0.93 2/54 14886
Raw data (stat): 14886 (runsolver) R 14885 21152 21151 0 -1 64 0 0 0 0 0 0 0 0 19 0 1 0 796397627 1052672 97 4294967295 134512640 135381576 3221224464 3221219904 134514522 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 97 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.93 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0018 s]
Raw data (loadavg): 0.94 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0017 s]
Raw data (loadavg): 0.95 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0022 s]
Raw data (loadavg): 0.96 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.002 s]
Raw data (loadavg): 0.96 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0025 s]
Raw data (loadavg): 0.97 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0028 s]
Raw data (loadavg): 0.97 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0026 s]
Raw data (loadavg): 0.98 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0029 s]
Raw data (loadavg): 0.98 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.002 s]
Raw data (loadavg): 0.98 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.004 s]
Raw data (loadavg): 0.98 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.026 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.027 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.027 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.027 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.027 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.027 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.027 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.031 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.031 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.034 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.034 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.034 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.035 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.035 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.035 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.036 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.035 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.035 s]
Raw data (loadavg): 1.07 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.037 s]
Raw data (loadavg): 1.06 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.036 s]
Raw data (loadavg): 1.05 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.036 s]
Raw data (loadavg): 1.04 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.036 s]
Raw data (loadavg): 1.04 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.037 s]
Raw data (loadavg): 1.03 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.036 s]
Raw data (loadavg): 1.03 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.037 s]
Raw data (loadavg): 1.02 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.037 s]
Raw data (loadavg): 1.02 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.037 s]
Raw data (loadavg): 1.01 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.037 s]
Raw data (loadavg): 1.01 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.037 s]
Raw data (loadavg): 1.01 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.037 s]
Raw data (loadavg): 1.01 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.037 s]
Raw data (loadavg): 1.01 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.037 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.038 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.039 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.038 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.038 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.039 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.039 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.046 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.046 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.046 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.047 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.047 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.047 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.047 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.047 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.047 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.048 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.047 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.049 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.049 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.049 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.054 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.053 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.054 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.054 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.055 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.055 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.055 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.062 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.7 s]
Raw data (loadavg): 1.00 1.00 0.94 1/53 14890
Raw data (stat): 14886 (minisat+_script) S 14885 21152 21151 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 796397627 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.7
CPU time (s): 1229.85
CPU user time (s): 1229.59
CPU system time (s): 0.25796
CPU usage (%): 100.012
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####