PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/submitted/een/normalized-p0201.opb
MD5SUM	ff4eb45c2603a47e5b79b2649e926ba4
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1523
Optimality of the best value was proved	NO
Number of terms in the objective function	201
Biggest coefficient in the objective function	1920
Number of bits for the biggest coefficient in the objective function	11
Sum of the numbers in the objective function	19980
Number of bits of the sum of numbers in the objective function	15
Biggest number in a constraint	1920
Number of bits of the biggest number in a constraint	11
Biggest sum of numbers in a constraint	19980
Number of bits of the biggest sum of numbers	15
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.01984
Number of variables	195
Total number of constraints	133
Number of constraints which are clauses	20
Number of constraints which are cardinality constraints (but not clauses)	26
Number of constraints which are nor clauses,nor cardinality constraints	87
Minimum length of a constraint	3
Maximum length of a constraint	65
Trace number 7132

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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:        863948 kB
Buffers:         36068 kB
Cached:         113800 kB
SwapCached:          4 kB
Active:          62048 kB
Inactive:        90688 kB
HighTotal:      131008 kB
HighFree:        13384 kB
LowTotal:       903652 kB
LowFree:        850564 kB
SwapTotal:     2097136 kB
SwapFree:      2097132 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            12316 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 21:45:51 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 5161 7 1200.19 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 133 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###################
c   -- Clauses(.)/Splits(s): .sssss
c ---[ 137]---> BDD-cost:    3
c ---[ 136]---> BDD-cost:    3
c ---[ 135]---> BDD-cost:    3
c ---[ 134]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:    3
c ---[ 132]---> BDD-cost:    3
c ---[ 131]---> BDD-cost:    3
c ---[ 130]---> BDD-cost:    3
c ---[ 129]---> BDD-cost:    3
c ---[ 128]---> BDD-cost:   11
c ---[ 127]---> BDD-cost:   11
c ---[ 126]---> BDD-cost:   11
c ---[ 125]---> BDD-cost:   11
c ---[ 124]---> BDD-cost:   11
c ---[ 123]---> BDD-cost:   11
c ---[ 122]---> BDD-cost:   11
c ---[ 121]---> BDD-cost:   11
c ---[ 120]---> BDD-cost:   11
c ---[ 119]---> BDD-cost:   11
c ---[ 118]---> BDD-cost:   11
c ---[ 117]---> BDD-cost:   11
c ---[ 116]---> BDD-cost:   11
c ---[ 115]---> BDD-cost:   11
c ---[ 114]---> BDD-cost:   11
c ---[ 113]---> BDD-cost:   11
c ---[ 112]---> BDD-cost:   11
c ---[ 111]---> BDD-cost:   11
c ---[ 110]---> BDD-cost:   11
c ---[ 109]---> BDD-cost:   11
c ---[ 108]---> BDD-cost:   11
c ---[ 107]---> BDD-cost:   11
c ---[ 106]---> BDD-cost:   11
c ---[ 105]---> BDD-cost:   11
c ---[ 104]---> BDD-cost:   11
c ---[ 103]---> BDD-cost:   11
c ---[ 102]---> BDD-cost:   11
c ---[ 101]---> BDD-cost:   11
c ---[ 100]---> BDD-cost:   11
c ---[  99]---> BDD-cost:   11
c ---[  98]---> BDD-cost:   11
c ---[  97]---> BDD-cost:   11
c ---[  96]---> BDD-cost:   11
c ---[  95]---> BDD-cost:   11
c ---[  94]---> BDD-cost:   11
c ---[  93]---> BDD-cost:   11
c ---[  92]---> BDD-cost:   11
c ---[  91]---> BDD-cost:   11
c ---[  90]---> BDD-cost:   11
c ---[  89]---> BDD-cost:   11
c ---[  88]---> BDD-cost:   11
c ---[  87]---> BDD-cost:   11
c ---[  86]---> BDD-cost:   11
c ---[  85]---> BDD-cost:   11
c ---[  84]---> BDD-cost:   11
c ---[  83]---> BDD-cost:   11
c ---[  82]---> BDD-cost:   11
c ---[  81]---> BDD-cost:   11
c ---[  80]---> BDD-cost:   11
c ---[  79]---> BDD-cost:   11
c ---[  78]---> BDD-cost:   11
c ---[  77]---> BDD-cost:   11
c ---[  76]---> BDD-cost:   11
c ---[  75]---> BDD-cost:   11
c ---[  74]---> BDD-cost:   11
c ---[  72]---> BDD-cost:   13
c ---[  70]---> BDD-cost:   15
c ---[  68]---> BDD-cost:   15
c ---[  66]---> BDD-cost:   13
c ---[  64]---> BDD-cost:   13
c ---[  62]---> BDD-cost:   13
c ---[  60]---> BDD-cost:   13
c ---[  58]---> BDD-cost:   13
c ---[  56]---> BDD-cost:   13
c ---[  54]---> BDD-cost:   13
c ---[  52]---> BDD-cost:   13
c ---[  50]---> BDD-cost:   13
c ---[  48]---> BDD-cost:   13
c ---[  46]---> BDD-cost:   13
c ---[  44]---> BDD-cost:   13
c ---[  42]---> BDD-cost:   13
c ---[  40]---> BDD-cost:   13
c ---[  38]---> BDD-cost:   13
c ---[  36]---> BDD-cost:   13
c ---[  31]---> BDD-cost:   39
c ---[  28]---> BDD-cost:   54
c ---[  27]---> BDD-cost:   42
c ---[  26]---> BDD-cost:   42
c ---[  25]---> BDD-cost:   73
c ---[  24]---> BDD-cost:   73
c ---[  23]---> BDD-cost:   98
c ---[  22]---> BDD-cost:  160
c ---[  21]---> BDD-cost:   85
c ---[  20]---> BDD-cost:   85
c ---[  19]---> BDD-cost:  201
c ---[  18]---> BDD-cost:  107
c ---[  17]---> BDD-cost:  107
c ---[  16]---> BDD-cost:  241
c ---[  15]---> BDD-cost:  128
c ---[  14]---> BDD-cost:  128
c ---[  13]---> BDD-cost:  150
c ---[  12]---> BDD-cost:  150
c ---[  11]---> BDD-cost:  281
c ---[  10]---> BDD-cost:  321
c ---[   9]---> BDD-cost:  172
c ---[   8]---> BDD-cost:  172
c ---[   7]---> BDD-cost:  194
c ---[   6]---> BDD-cost:  194
c ---[   5]---> BDD-cost:  361
c ---[   4]---> BDD-cost:    1
c ---[   3]---> BDD-cost:    1
c ---[   2]---> BDD-cost:    1
c ---[   1]---> BDD-cost:    1
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   23531    68434 |    7843       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 2296[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:21989     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        22 |   80729   202427 |   26909      21      108     5.1 |  0.000 % |
c |       122 |   80671   202261 |   29599     115     1245    10.8 |  0.539 % |
c |       272 |   80607   202081 |   32559     262     2329     8.9 |  0.590 % |
c |       497 |   79839   200336 |   35815     475     4544     9.6 |  1.457 % |
c |       834 |   78984   198386 |   39397     802     6875     8.6 |  2.450 % |
c |      1341 |   77774   195601 |   43337    1281    11334     8.8 |  3.987 % |
c ==============================================================================
c [1mFound solution: 2260[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1360 |   78277   196976 |   26092    1299    11529     8.9 |  3.987 % |
c |      1460 |   76817   193605 |   28701    1381    14371    10.4 |  5.797 % |
c |      1614 |   75176   189821 |   31571    1488    16095    10.8 |  7.900 % |
c |      1839 |   74894   189171 |   34728    1706    18800    11.0 |  8.273 % |
c ==============================================================================
c [1mFound solution: 2225[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2095 |   71689   181767 |   23896    1854    19047    10.3 |  8.273 % |
c ==============================================================================
c [1mFound solution: 2222[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2134 |   71847   182157 |   23949    1893    21222    11.2 |  8.273 % |
c |      2236 |   71738   181904 |   26343    1994    22884    11.5 | 12.638 % |
c |      2386 |   71738   181904 |   28978    2144    23643    11.0 | 12.638 % |
c ==============================================================================
c [1mFound solution: 2216[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2463 |   71471   181303 |   23823    2167    23986    11.1 | 12.638 % |
c |      2563 |   71471   181303 |   26205    2267    33672    14.9 | 12.956 % |
c |      2713 |   71471   181303 |   28825    2417    35578    14.7 | 12.956 % |
c |      2940 |   69205   176055 |   31708    2524    35371    14.0 | 15.953 % |
c |      3277 |   68480   174357 |   34879    2822    42982    15.2 | 16.928 % |
c |      3783 |   67567   172221 |   38367    3300    54108    16.4 | 18.088 % |
c ==============================================================================
c [1mFound solution: 2069[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4252 |   67727   172614 |   22575    3767    60896    16.2 | 18.088 % |
c ==============================================================================
c [1mFound solution: 2059[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4330 |   67138   171242 |   22379    3812    62369    16.4 | 18.088 % |
c |      4430 |   67138   171242 |   24616    3912    63480    16.2 | 18.929 % |
c |      4580 |   66536   169843 |   27078    4010    63467    15.8 | 19.749 % |
c |      4805 |   65247   166850 |   29786    4199    65952    15.7 | 21.432 % |
c |      5143 |   65082   166389 |   32765    4526    75788    16.7 | 21.584 % |
c |      5649 |   64109   164137 |   36041    5023    89406    17.8 | 22.871 % |
c |      6408 |   64109   164137 |   39645    5782    95477    16.5 | 22.871 % |
c |      7549 |   63855   163547 |   43610    6825   152565    22.4 | 23.220 % |
c ==============================================================================
c [1mFound solution: 2039[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 3290     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8209 |   67953   173126 |   22651    7481   186895    25.0 | 23.220 % |
c |      8310 |   67953   173126 |   24916    7582   187819    24.8 | 22.973 % |
c |      8462 |   67953   173126 |   27407    7734   188917    24.4 | 22.973 % |
c |      8687 |   67113   171184 |   30148    7879   189688    24.1 | 24.042 % |
c ==============================================================================
c [1mFound solution: 2037[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8712 |   67127   171218 |   22375    7904   190960    24.2 | 24.042 % |
c |      8812 |   66569   169934 |   24612    7949   191688    24.1 | 24.720 % |
c |      8962 |   65320   167027 |   27073    7991   194947    24.4 | 26.319 % |
c |      9187 |   65320   167027 |   29781    8216   201744    24.6 | 26.319 % |
c |      9524 |   64810   165845 |   32759    8541   211626    24.8 | 26.943 % |
c |     10030 |   64119   164237 |   36035    8969   231199    25.8 | 27.807 % |
c ==============================================================================
c [1mFound solution: 2017[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10062 |   64127   164257 |   21375    9001   234024    26.0 | 27.807 % |
c |     10163 |   64116   164224 |   23512    9101   236083    25.9 | 27.816 % |
c |     10315 |   62958   161511 |   25863    9080   236623    26.1 | 29.261 % |
c |     10540 |   61111   157218 |   28450    9187   239521    26.1 | 31.637 % |
c |     10878 |   60467   155723 |   31295    9488   242329    25.5 | 33.094 % |
c |     11384 |   59421   153275 |   34424    9877   267031    27.0 | 33.816 % |
c |     12145 |   59378   153168 |   37867   10632   298204    28.0 | 33.864 % |
c ==============================================================================
c [1mFound solution: 1964[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12208 |   59427   153293 |   19809   10695   299110    28.0 | 33.864 % |
c ==============================================================================
c [1mFound solution: 1957[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12216 |   59437   153319 |   19812   10703   299443    28.0 | 33.864 % |
c |     12316 |   59437   153319 |   21793   10803   300393    27.8 | 33.849 % |
c |     12466 |   59427   153295 |   23972   10949   309945    28.3 | 33.864 % |
c |     12692 |   59427   153295 |   26369   11175   316566    28.3 | 33.864 % |
c |     13029 |   59413   153257 |   29006   11510   330263    28.7 | 33.876 % |
c |     13535 |   58606   151369 |   31907   11746   342179    29.1 | 34.865 % |
c ==============================================================================
c [1mFound solution: 1956[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14186 |   58539   151201 |   19513   12388   376049    30.4 | 34.865 % |
c |     14286 |   58539   151201 |   21464   12488   382965    30.7 | 34.964 % |
c |     14438 |   58534   151186 |   23610   12639   384230    30.4 | 34.968 % |
c |     14663 |   58188   150368 |   25971   12783   389124    30.4 | 35.423 % |
c |     15000 |   58178   150338 |   28568   13117   411162    31.3 | 35.431 % |
c |     15509 |   58122   150201 |   31425   13590   430789    31.7 | 35.506 % |
c ==============================================================================
c [1mFound solution: 1946[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16240 |   58124   150205 |   19374   14321   472111    33.0 | 35.506 % |
c |     16346 |   58113   150172 |   21311   14426   478583    33.2 | 35.512 % |
c |     16496 |   58113   150172 |   23442   14576   485518    33.3 | 35.512 % |
c |     16721 |   58113   150172 |   25786   14801   493856    33.4 | 35.512 % |
c |     17058 |   58113   150172 |   28365   15138   499389    33.0 | 35.512 % |
c ==============================================================================
c [1mFound solution: 1919[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17100 |   58118   150185 |   19372   15180   502805    33.1 | 35.512 % |
c |     17202 |   58078   150094 |   21309   15266   503782    33.0 | 35.556 % |
c |     17352 |   58062   150056 |   23440   15415   505086    32.8 | 35.580 % |
c |     17577 |   58005   149885 |   25784   15637   523565    33.5 | 35.619 % |
c |     17915 |   57103   147805 |   28362   15911   532906    33.5 | 36.713 % |
c |     18421 |   56670   146806 |   31198   16210   534468    33.0 | 37.251 % |
c |     19180 |   56445   146250 |   34318   16950   579990    34.2 | 37.526 % |
c |     20320 |   55914   145028 |   37750   17978   626397    34.8 | 38.173 % |
c ==============================================================================
c [1mFound solution: 1893[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20413 |   56013   145269 |   18671   18071   629212    34.8 | 38.173 % |
c |     20513 |   56013   145269 |   20538   18171   634431    34.9 | 38.182 % |
c |     20663 |   56002   145236 |   22591   18320   637251    34.8 | 38.190 % |
c |     20888 |   55957   145133 |   24851   18543   644496    34.8 | 38.229 % |
c |     21226 |   55952   145118 |   27336   18879   657962    34.9 | 38.233 % |
c |     21732 |   55952   145118 |   30069   19384   682401    35.2 | 38.240 % |
c ==============================================================================
c [1mFound solution: 1829[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22150 |   55949   145105 |   18649   19802   696757    35.2 | 38.240 % |
c |     22250 |   55873   144926 |   20513   19901   697735    35.1 | 38.350 % |
c |     22402 |   55873   144926 |   22565   20053   706353    35.2 | 38.350 % |
c ==============================================================================
c [1mFound solution: 1821[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22449 |   55898   144989 |   18632   20100   708097    35.2 | 38.350 % |
c |     22549 |   55898   144989 |   20495   20200   712108    35.3 | 38.340 % |
c |     22699 |   55898   144989 |   22544   20350   715036    35.1 | 38.340 % |
c |     22925 |   55898   144989 |   24799   20576   733546    35.7 | 38.340 % |
c ==============================================================================
c [1mFound solution: 1815[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23083 |   55916   145035 |   18638   20734   746706    36.0 | 38.340 % |
c |     23186 |   55916   145035 |   20501   20837   752931    36.1 | 38.336 % |
c ==============================================================================
c [1mFound solution: 1814[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23309 |   55928   145065 |   18642   20960   756446    36.1 | 38.336 % |
c |     23409 |   55928   145065 |   20506   21060   757796    36.0 | 38.334 % |
c |     23561 |   55031   142976 |   22556   21075   757498    35.9 | 39.465 % |
c |     23786 |   54923   142721 |   24812   21292   762478    35.8 | 39.590 % |
c ==============================================================================
c [1mFound solution: 1777[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23929 |   54930   142738 |   18310   21435   766447    35.8 | 39.590 % |
c |     24029 |   54925   142723 |   20141   21534   774712    36.0 | 39.593 % |
c |     24179 |   54925   142723 |   22155   21684   778071    35.9 | 39.593 % |
c |     24405 |   54925   142723 |   24370   21910   780686    35.6 | 39.593 % |
c |     24743 |   54652   142103 |   26807   21808   778396    35.7 | 39.910 % |
c |     25249 |   54652   142103 |   29488   22314   819133    36.7 | 39.910 % |
c |     26008 |   54652   142103 |   32437   23073   842338    36.5 | 39.910 % |
c |     27148 |   54652   142103 |   35681   24213   872528    36.0 | 39.910 % |
c |     28858 |   54652   142103 |   39249   25923   949632    36.6 | 39.910 % |
c |     31420 |   54652   142103 |   43174   28485  1092166    38.3 | 39.910 % |
c ==============================================================================
c [1mFound solution: 1769[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34221 |   54659   142121 |   18219   31285  1305968    41.7 | 39.910 % |
c |     34321 |   54641   142067 |   20040   15740   580944    36.9 | 39.923 % |
c |     34472 |   54641   142067 |   22044   15891   591823    37.2 | 39.923 % |
c |     34698 |   54497   141732 |   24249   16096   597265    37.1 | 40.107 % |
c |     35035 |   54437   141593 |   26674   16432   601480    36.6 | 40.185 % |
c |     35543 |   54231   141116 |   29341   16931   622718    36.8 | 40.428 % |
c |     36303 |   54180   140998 |   32276   17675   652675    36.9 | 40.494 % |
c |     37442 |   54180   140998 |   35503   18814   695988    37.0 | 40.494 % |
c ==============================================================================
c [1mFound solution: 1737[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38253 |   54190   141022 |   18063   19624   754870    38.5 | 40.494 % |
c |     38355 |   54190   141022 |   19869   19726   759028    38.5 | 40.494 % |
c |     38505 |   54190   141022 |   21856   19876   761907    38.3 | 40.494 % |
c |     38731 |   54190   141022 |   24041   20102   767372    38.2 | 40.494 % |
c |     39068 |   54170   140967 |   26446   20437   774159    37.9 | 40.506 % |
c |     39575 |   54170   140967 |   29090   20944   806479    38.5 | 40.506 % |
c |     40334 |   54165   140952 |   31999   21701   837843    38.6 | 40.510 % |
c |     41473 |   54165   140952 |   35199   22840   911402    39.9 | 40.510 % |
c |     43183 |   54122   140829 |   38719   24546  1013189    41.3 | 40.541 % |
c ==============================================================================
c [1mFound solution: 1734[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     44485 |   54111   140797 |   18037   25845  1083166    41.9 | 40.541 % |
c |     44587 |   54111   140797 |   19840   25947  1086748    41.9 | 40.554 % |
c |     44737 |   54111   140797 |   21824   26097  1094527    41.9 | 40.554 % |
c |     44963 |   54111   140797 |   24007   26323  1105254    42.0 | 40.554 % |
c |     45300 |   54111   140797 |   26407   26660  1118684    42.0 | 40.554 % |
c |     45806 |   54111   140797 |   29048   27166  1127480    41.5 | 40.554 % |
c ==============================================================================
c [1mFound solution: 1726[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46275 |   54121   140821 |   18040   27635  1170285    42.3 | 40.554 % |
c |     46379 |   54121   140821 |   19844   27739  1176853    42.4 | 40.551 % |
c |     46529 |   54121   140821 |   21828   27889  1182695    42.4 | 40.551 % |
c |     46755 |   54105   140783 |   24011   28112  1187196    42.2 | 40.567 % |
c |     47092 |   54105   140783 |   26412   28449  1194205    42.0 | 40.567 % |
c |     47599 |   54076   140712 |   29053   28952  1208488    41.7 | 40.598 % |
c |     48358 |   54076   140712 |   31958   29711  1239638    41.7 | 40.598 % |
c ==============================================================================
c [1mFound solution: 1718[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     48883 |   54089   140743 |   18029   30236  1282651    42.4 | 40.598 % |
c |     48983 |   54089   140743 |   19831   15218   469594    30.9 | 40.594 % |
c ==============================================================================
c [1mFound solution: 1703[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     49021 |   54099   140767 |   18033   15256   471258    30.9 | 40.594 % |
c |     49121 |   54099   140767 |   19836   15356   477300    31.1 | 40.592 % |
c |     49271 |   54039   140627 |   21819   15504   484678    31.3 | 40.674 % |
c |     49497 |   54039   140627 |   24001   15730   490492    31.2 | 40.674 % |
c |     49834 |   54039   140627 |   26402   16067   505493    31.5 | 40.674 % |
c |     50340 |   54039   140627 |   29042   16573   526636    31.8 | 40.674 % |
c |     51099 |   54039   140627 |   31946   17332   576108    33.2 | 40.674 % |
c |     52238 |   54039   140627 |   35141   18471   650640    35.2 | 40.674 % |
c |     53947 |   54039   140627 |   38655   20180   700223    34.7 | 40.674 % |
c |     56509 |   54039   140627 |   42520   22742   799726    35.2 | 40.674 % |
c |     60354 |   54030   140604 |   46772   26584  1053009    39.6 | 40.682 % |
c |     66120 |   54030   140604 |   51450   32350  1374320    42.5 | 40.682 % |
c |     74770 |   54026   140594 |   56595   40999  1900935    46.4 | 40.685 % |
c |     87745 |   54026   140594 |   62254   53974  2643117    49.0 | 40.685 % |
c ==============================================================================
c [1mFound solution: 1697[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     96694 |   54025   140591 |   18008   62922  3161516    50.2 | 40.685 % |
c |     96794 |   54025   140591 |   19808   21651   824860    38.1 | 40.690 % |
c |     96944 |   54025   140591 |   21789   21801   832037    38.2 | 40.690 % |
c |     97169 |   53915   140338 |   23968   21999   843347    38.3 | 40.819 % |
c |     97506 |   53915   140338 |   26365   22336   852432    38.2 | 40.819 % |
c ==============================================================================
c [1mFound solution: 1680[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     97614 |   53924   140361 |   17974   22444   858847    38.3 | 40.819 % |
c |     97715 |   53924   140361 |   19771   22545   865740    38.4 | 40.818 % |
c |     97865 |   53924   140361 |   21748   22695   877311    38.7 | 40.818 % |
c |     98091 |   53924   140361 |   23923   22921   884007    38.6 | 40.818 % |
c |     98428 |   53924   140361 |   26315   23258   900506    38.7 | 40.818 % |
c |     98934 |   53924   140361 |   28947   23764   930234    39.1 | 40.818 % |
c |     99693 |   53924   140361 |   31842   24523   970667    39.6 | 40.818 % |
c |    100836 |   53924   140361 |   35026   25666  1049657    40.9 | 40.818 % |
c |    102545 |   53924   140361 |   38528   27375  1136002    41.5 | 40.818 % |
c |    105107 |   53919   140346 |   42381   29936  1261862    42.2 | 40.822 % |
c |    108951 |   53919   140346 |   46619   33780  1541543    45.6 | 40.822 % |
c |    114718 |   53919   140346 |   51281   39547  1964624    49.7 | 40.822 % |
c |    123367 |   53864   140216 |   56410   48190  2348991    48.7 | 40.888 % |
c ==============================================================================
c [1mFound solution: 1673[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    129859 |   53714   139791 |   17904   54662  2740951    50.1 | 40.888 % |
c |    129959 |   53714   139791 |   19694   23209   764760    33.0 | 41.024 % |
c |    130110 |   53714   139791 |   21663   23360   772780    33.1 | 41.024 % |
c |    130335 |   53714   139791 |   23830   23585   786571    33.4 | 41.024 % |
c |    130672 |   53714   139791 |   26213   23922   806337    33.7 | 41.024 % |
c |    131178 |   53714   139791 |   28834   24428   835439    34.2 | 41.024 % |
c |    131937 |   53714   139791 |   31718   25187   856000    34.0 | 41.024 % |
c |    133077 |   53714   139791 |   34889   26327   905158    34.4 | 41.024 % |
c |    134787 |   53714   139791 |   38378   28037   986052    35.2 | 41.024 % |
c |    137350 |   53714   139791 |   42216   30600  1153034    37.7 | 41.024 % |
c |    141196 |   53714   139791 |   46438   34446  1308042    38.0 | 41.024 % |
c ==============================================================================
c [1mFound solution: 1664[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    141220 |   53719   139804 |   17906   34470  1309576    38.0 | 41.024 % |
c |    141320 |   53719   139804 |   19696   17335   500796    28.9 | 41.025 % |
c |    141473 |   53719   139804 |   21666   17488   512235    29.3 | 41.025 % |
c |    141699 |   53719   139804 |   23832   17714   526839    29.7 | 41.025 % |
c |    142036 |   53719   139804 |   26216   18051   542750    30.1 | 41.025 % |
c |    142542 |   53719   139804 |   28837   18557   580273    31.3 | 41.025 % |
c |    143301 |   53719   139804 |   31721   19316   616075    31.9 | 41.025 % |
c |    144441 |   53719   139804 |   34893   20456   668100    32.7 | 41.025 % |
c |    146149 |   53621   139569 |   38383   22158   766791    34.6 | 41.146 % |
c |    148712 |   53621   139569 |   42221   24721   890481    36.0 | 41.146 % |
c |    152556 |   53621   139569 |   46443   28565  1156068    40.5 | 41.146 % |
c |    158324 |   53614   139548 |   51087   34328  1447025    42.2 | 41.150 % |
c |    166973 |   53255   138705 |   56196   42945  1975254    46.0 | 41.611 % |
c ==============================================================================
c [1mFound solution: 1662[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    170439 |   53264   138728 |   17754   46411  2225567    48.0 | 41.611 % |
c |    170539 |   53259   138713 |   19529   21271   881753    41.5 | 41.614 % |
c |    170690 |   53164   138495 |   21482   21408   884389    41.3 | 41.723 % |
c |    170916 |   52564   137095 |   23630   21529   884617    41.1 | 42.508 % |
c |    171253 |   52564   137095 |   25993   21866   898469    41.1 | 42.508 % |
c |    171759 |   52564   137095 |   28592   22372   921313    41.2 | 42.508 % |
c |    172518 |   52564   137095 |   31452   23131   971715    42.0 | 42.508 % |
c |    173657 |   52564   137095 |   34597   24270  1028424    42.4 | 42.508 % |
c |    175365 |   52564   137095 |   38057   25978  1138367    43.8 | 42.508 % |
c |    177927 |   52564   137095 |   41863   28540  1314971    46.1 | 42.508 % |
c ==============================================================================
c [1mFound solution: 1656[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    180416 |   52586   137150 |   17528   31029  1498770    48.3 | 42.508 % |
c |    180516 |   52417   136756 |   19280   15610   601787    38.6 | 42.707 % |
c |    180666 |   52417   136756 |   21208   15760   607655    38.6 | 42.707 % |
c |    180891 |   52417   136756 |   23329   15985   618258    38.7 | 42.707 % |
c |    181228 |   52417   136756 |   25662   16322   630945    38.7 | 42.707 % |
c |    181738 |   52417   136756 |   28229   16832   651243    38.7 | 42.707 % |
c |    182497 |   52417   136756 |   31051   17591   682311    38.8 | 42.707 % |
c |    183636 |   52417   136756 |   34157   18730   787851    42.1 | 42.707 % |
c |    185344 |   52408   136731 |   37572   20434   865914    42.4 | 42.714 % |
c |    187907 |   52408   136731 |   41330   22997   990046    43.1 | 42.714 % |
c |    191751 |   52399   136708 |   45463   26838  1219054    45.4 | 42.722 % |
c |    197517 |   52391   136686 |   50009   32603  1447077    44.4 | 42.730 % |
c |    206168 |   52391   136686 |   55010   41254  1947476    47.2 | 42.730 % |
c |    219145 |   52386   136673 |   60511   54230  2642865    48.7 | 42.734 % |
c ==============================================================================
c [1mFound solution: 1647[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    233070 |   52400   136705 |   17466   68153  3203452    47.0 | 42.734 % |
c |    233170 |   52400   136705 |   19212   21930   595786    27.2 | 42.732 % |
c |    233320 |   52400   136705 |   21133   22080   604908    27.4 | 42.732 % |
c |    233545 |   52400   136705 |   23247   22305   614311    27.5 | 42.732 % |
c |    233883 |   52400   136705 |   25571   22643   630700    27.9 | 42.732 % |
c |    234389 |   52386   136673 |   28129   23146   672085    29.0 | 42.747 % |
c |    235148 |   52386   136673 |   30942   23905   725474    30.3 | 42.747 % |
c |    236287 |   52386   136673 |   34036   25044   797844    31.9 | 42.747 % |
c |    237998 |   52381   136658 |   37439   26752   918667    34.3 | 42.751 % |
#### 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.91 2/54 32737
Raw data (stat): 32737 (runsolver) R 32736 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 429598076 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.93 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 2475 0 0 0 992 5 0 0 25 0 1 0 429598076 12189696 2401 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2976 2401 603 41 0 2935 0
vsize: 11904
[startup+20.0015 s]
Raw data (loadavg): 0.94 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 2583 0 0 0 1990 6 0 0 25 0 1 0 429598076 12677120 2509 4294967295 134512640 134672761 3221224576 3221223732 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3095 2509 603 41 0 3054 0
vsize: 12380
[startup+30.002 s]
Raw data (loadavg): 0.95 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 2810 0 0 0 2988 7 0 0 25 0 1 0 429598076 13389824 2736 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3269 2736 603 41 0 3228 0
vsize: 13076
[startup+40.0013 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 2920 0 0 0 3988 8 0 0 25 0 1 0 429598076 13922304 2846 4294967295 134512640 134672761 3221224576 3221223680 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3399 2846 603 41 0 3358 0
vsize: 13596
[startup+50.0023 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 3070 0 0 0 4988 8 0 0 25 0 1 0 429598076 14426112 2996 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3522 2996 603 41 0 3481 0
vsize: 14088
[startup+60.0023 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 3196 0 0 0 5987 9 0 0 25 0 1 0 429598076 15028224 3122 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3669 3122 603 41 0 3628 0
vsize: 14676
[startup+70.0034 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 3340 0 0 0 6986 10 0 0 25 0 1 0 429598076 15585280 3266 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3805 3266 603 41 0 3764 0
vsize: 15220
[startup+80.0044 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 3430 0 0 0 7985 10 0 0 25 0 1 0 429598076 15929344 3356 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3889 3356 603 41 0 3848 0
vsize: 15556
[startup+90.0041 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 3540 0 0 0 8985 10 0 0 25 0 1 0 429598076 16453632 3466 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4017 3466 603 41 0 3976 0
vsize: 16068
[startup+100.005 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 3678 0 0 0 9985 11 0 0 25 0 1 0 429598076 16982016 3604 4294967295 134512640 134672761 3221224576 3221223744 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4146 3604 603 41 0 4105 0
vsize: 16584
[startup+110.005 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 3845 0 0 0 10984 12 0 0 25 0 1 0 429598076 17645568 3771 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4308 3771 603 41 0 4267 0
vsize: 17232
[startup+120.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 4053 0 0 0 11984 12 0 0 25 0 1 0 429598076 18444288 3979 4294967295 134512640 134672761 3221224576 3221223744 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4503 3979 603 41 0 4462 0
vsize: 18012
[startup+130.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 4053 0 0 0 12984 12 0 0 25 0 1 0 429598076 18444288 3979 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4503 3979 603 41 0 4462 0
vsize: 18012
[startup+140.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 4053 0 0 0 13984 12 0 0 25 0 1 0 429598076 18444288 3979 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4503 3979 603 41 0 4462 0
vsize: 18012
[startup+150.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 4053 0 0 0 14984 12 0 0 25 0 1 0 429598076 18444288 3979 4294967295 134512640 134672761 3221224576 3221223680 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4503 3979 603 41 0 4462 0
vsize: 18012
[startup+160.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 4053 0 0 0 15985 12 0 0 25 0 1 0 429598076 18444288 3979 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4503 3979 603 41 0 4462 0
vsize: 18012
[startup+170.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 4053 0 0 0 16985 12 0 0 25 0 1 0 429598076 18444288 3979 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4503 3979 603 41 0 4462 0
vsize: 18012
[startup+180.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 4063 0 0 0 17986 12 0 0 25 0 1 0 429598076 18579456 3989 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4536 3989 603 41 0 4495 0
vsize: 18144
[startup+190.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 4099 0 0 0 18986 13 0 0 25 0 1 0 429598076 18649088 4025 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4553 4025 603 41 0 4512 0
vsize: 18212
[startup+200.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 4099 0 0 0 19986 13 0 0 25 0 1 0 429598076 18649088 4025 4294967295 134512640 134672761 3221224576 3221223744 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4553 4025 603 41 0 4512 0
vsize: 18212
[startup+210.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 4099 0 0 0 20986 13 0 0 25 0 1 0 429598076 18649088 4025 4294967295 134512640 134672761 3221224576 3221223744 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4553 4025 603 41 0 4512 0
vsize: 18212
[startup+220.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 4099 0 0 0 21986 13 0 0 25 0 1 0 429598076 18649088 4025 4294967295 134512640 134672761 3221224576 3221223744 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4553 4025 603 41 0 4512 0
vsize: 18212
[startup+230.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 4099 0 0 0 22986 13 0 0 25 0 1 0 429598076 18649088 4025 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4553 4025 603 41 0 4512 0
vsize: 18212
[startup+240.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 4099 0 0 0 23986 13 0 0 25 0 1 0 429598076 18649088 4025 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4553 4025 603 41 0 4512 0
vsize: 18212
[startup+250.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 4130 0 0 0 24986 13 0 0 25 0 1 0 429598076 18780160 4056 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4585 4056 603 41 0 4544 0
vsize: 18340
[startup+260.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 4245 0 0 0 25986 13 0 0 25 0 1 0 429598076 19304448 4171 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4713 4171 603 41 0 4672 0
vsize: 18852
[startup+270.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 4337 0 0 0 26986 13 0 0 25 0 1 0 429598076 19828736 4263 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4841 4263 603 41 0 4800 0
vsize: 19364
[startup+280.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 4454 0 0 0 27986 14 0 0 25 0 1 0 429598076 20226048 4380 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4938 4380 603 41 0 4897 0
vsize: 19752
[startup+290.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 4603 0 0 0 28985 14 0 0 25 0 1 0 429598076 20885504 4529 4294967295 134512640 134672761 3221224576 3221223744 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5099 4529 603 41 0 5058 0
vsize: 20396
[startup+300.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 4766 0 0 0 29985 15 0 0 25 0 1 0 429598076 21544960 4692 4294967295 134512640 134672761 3221224576 3221223712 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5260 4692 603 41 0 5219 0
vsize: 21040
[startup+310.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 4870 0 0 0 30984 16 0 0 25 0 1 0 429598076 21938176 4796 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5356 4796 603 41 0 5315 0
vsize: 21424
[startup+320.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 4986 0 0 0 31985 16 0 0 25 0 1 0 429598076 22470656 4912 4294967295 134512640 134672761 3221224576 3221223744 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5486 4912 603 41 0 5445 0
vsize: 21944
[startup+330.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 5082 0 0 0 32984 16 0 0 25 0 1 0 429598076 22863872 5008 4294967295 134512640 134672761 3221224576 3221223712 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5582 5008 603 41 0 5541 0
vsize: 22328
[startup+340.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 5193 0 0 0 33984 17 0 0 25 0 1 0 429598076 23261184 5119 4294967295 134512640 134672761 3221224576 3221223680 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5679 5119 603 41 0 5638 0
vsize: 22716
[startup+350.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 5294 0 0 0 34984 17 0 0 25 0 1 0 429598076 23654400 5220 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5775 5220 603 41 0 5734 0
vsize: 23100
[startup+360.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 5397 0 0 0 35984 17 0 0 25 0 1 0 429598076 24047616 5323 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5871 5323 603 41 0 5830 0
vsize: 23484
[startup+370.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 5486 0 0 0 36984 17 0 0 25 0 1 0 429598076 24444928 5412 4294967295 134512640 134672761 3221224576 3221223680 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5968 5412 603 41 0 5927 0
vsize: 23872
[startup+380.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 5623 0 0 0 37984 18 0 0 25 0 1 0 429598076 24981504 5549 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6099 5549 603 41 0 6058 0
vsize: 24396
[startup+390.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 5746 0 0 0 38983 18 0 0 25 0 1 0 429598076 25522176 5672 4294967295 134512640 134672761 3221224576 3221223680 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6231 5672 603 41 0 6190 0
vsize: 24924
[startup+400.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 5846 0 0 0 39983 19 0 0 25 0 1 0 429598076 25923584 5772 4294967295 134512640 134672761 3221224576 3221223712 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6329 5772 603 41 0 6288 0
vsize: 25316
[startup+410.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 5940 0 0 0 40983 19 0 0 25 0 1 0 429598076 26316800 5866 4294967295 134512640 134672761 3221224576 3221223680 134559902 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6425 5866 603 41 0 6384 0
vsize: 25700
[startup+420.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6045 0 0 0 41983 19 0 0 25 0 1 0 429598076 26722304 5971 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6524 5971 603 41 0 6483 0
vsize: 26096
[startup+430.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6158 0 0 0 42983 20 0 0 25 0 1 0 429598076 27246592 6084 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6652 6084 603 41 0 6611 0
vsize: 26608
[startup+440.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6279 0 0 0 43983 20 0 0 25 0 1 0 429598076 27664384 6205 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6754 6205 603 41 0 6713 0
vsize: 27016
[startup+450.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6321 0 0 0 44983 20 0 0 25 0 1 0 429598076 27799552 6247 4294967295 134512640 134672761 3221224576 3221223680 134560412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6787 6247 603 41 0 6746 0
vsize: 27148
[startup+460.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6321 0 0 0 45983 20 0 0 25 0 1 0 429598076 27799552 6247 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6787 6247 603 41 0 6746 0
vsize: 27148
[startup+470.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6321 0 0 0 46983 20 0 0 25 0 1 0 429598076 27799552 6247 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6787 6247 603 41 0 6746 0
vsize: 27148
[startup+480.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6322 0 0 0 47983 20 0 0 25 0 1 0 429598076 27799552 6248 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6787 6248 603 41 0 6746 0
vsize: 27148
[startup+490.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6322 0 0 0 48983 20 0 0 25 0 1 0 429598076 27799552 6248 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6787 6248 603 41 0 6746 0
vsize: 27148
[startup+500.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6322 0 0 0 49984 20 0 0 25 0 1 0 429598076 27799552 6248 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6787 6248 603 41 0 6746 0
vsize: 27148
[startup+510.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6322 0 0 0 50984 20 0 0 25 0 1 0 429598076 27799552 6248 4294967295 134512640 134672761 3221224576 3221223744 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6787 6248 603 41 0 6746 0
vsize: 27148
[startup+520.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6322 0 0 0 51984 20 0 0 25 0 1 0 429598076 27799552 6248 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6787 6248 603 41 0 6746 0
vsize: 27148
[startup+530.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6322 0 0 0 52984 20 0 0 25 0 1 0 429598076 27799552 6248 4294967295 134512640 134672761 3221224576 3221223712 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6787 6248 603 41 0 6746 0
vsize: 27148
[startup+540.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6323 0 0 0 53984 20 0 0 25 0 1 0 429598076 27799552 6249 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6787 6249 603 41 0 6746 0
vsize: 27148
[startup+550.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6323 0 0 0 54984 20 0 0 25 0 1 0 429598076 27799552 6249 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6787 6249 603 41 0 6746 0
vsize: 27148
[startup+560.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6323 0 0 0 55985 20 0 0 25 0 1 0 429598076 27799552 6249 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6787 6249 603 41 0 6746 0
vsize: 27148
[startup+570.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6323 0 0 0 56985 20 0 0 25 0 1 0 429598076 27799552 6249 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6787 6249 603 41 0 6746 0
vsize: 27148
[startup+580.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6323 0 0 0 57985 20 0 0 25 0 1 0 429598076 27799552 6249 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6787 6249 603 41 0 6746 0
vsize: 27148
[startup+590.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6323 0 0 0 58985 20 0 0 25 0 1 0 429598076 27799552 6249 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6787 6249 603 41 0 6746 0
vsize: 27148
[startup+600.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6323 0 0 0 59985 20 0 0 25 0 1 0 429598076 27799552 6249 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6787 6249 603 41 0 6746 0
vsize: 27148
[startup+610.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6324 0 0 0 60986 20 0 0 25 0 1 0 429598076 27799552 6250 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6787 6250 603 41 0 6746 0
vsize: 27148
[startup+620.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6332 0 0 0 61986 20 0 0 25 0 1 0 429598076 27910144 6258 4294967295 134512640 134672761 3221224576 3221223680 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6258 603 41 0 6773 0
vsize: 27256
[startup+630.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6332 0 0 0 62986 20 0 0 25 0 1 0 429598076 27910144 6258 4294967295 134512640 134672761 3221224576 3221223532 1075349707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6258 603 41 0 6773 0
vsize: 27256
[startup+640.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6332 0 0 0 63986 20 0 0 25 0 1 0 429598076 27910144 6258 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6258 603 41 0 6773 0
vsize: 27256
[startup+650.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6332 0 0 0 64986 20 0 0 25 0 1 0 429598076 27910144 6258 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6258 603 41 0 6773 0
vsize: 27256
[startup+660.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6332 0 0 0 65986 20 0 0 25 0 1 0 429598076 27910144 6258 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6258 603 41 0 6773 0
vsize: 27256
[startup+670.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6332 0 0 0 66987 20 0 0 25 0 1 0 429598076 27910144 6258 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6258 603 41 0 6773 0
vsize: 27256
[startup+680.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6332 0 0 0 67987 20 0 0 25 0 1 0 429598076 27910144 6258 4294967295 134512640 134672761 3221224576 3221223744 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6258 603 41 0 6773 0
vsize: 27256
[startup+690.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6332 0 0 0 68987 21 0 0 25 0 1 0 429598076 27910144 6258 4294967295 134512640 134672761 3221224576 3221223736 134561238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6258 603 41 0 6773 0
vsize: 27256
[startup+700.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6332 0 0 0 69987 21 0 0 25 0 1 0 429598076 27910144 6258 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6258 603 41 0 6773 0
vsize: 27256
[startup+710.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6332 0 0 0 70987 21 0 0 25 0 1 0 429598076 27910144 6258 4294967295 134512640 134672761 3221224576 3221223728 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6258 603 41 0 6773 0
vsize: 27256
[startup+720.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6333 0 0 0 71987 21 0 0 25 0 1 0 429598076 27910144 6259 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6259 603 41 0 6773 0
vsize: 27256
[startup+730.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6333 0 0 0 72987 21 0 0 25 0 1 0 429598076 27910144 6259 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6259 603 41 0 6773 0
vsize: 27256
[startup+740.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6333 0 0 0 73988 21 0 0 25 0 1 0 429598076 27910144 6259 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6259 603 41 0 6773 0
vsize: 27256
[startup+750.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6333 0 0 0 74988 21 0 0 25 0 1 0 429598076 27910144 6259 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6259 603 41 0 6773 0
vsize: 27256
[startup+760.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6333 0 0 0 75988 21 0 0 25 0 1 0 429598076 27910144 6259 4294967295 134512640 134672761 3221224576 3221223760 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6259 603 41 0 6773 0
vsize: 27256
[startup+770.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6333 0 0 0 76988 21 0 0 25 0 1 0 429598076 27910144 6259 4294967295 134512640 134672761 3221224576 3221223680 134559841 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6259 603 41 0 6773 0
vsize: 27256
[startup+780.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6333 0 0 0 77988 21 0 0 25 0 1 0 429598076 27910144 6259 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6259 603 41 0 6773 0
vsize: 27256
[startup+790.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6333 0 0 0 78989 21 0 0 25 0 1 0 429598076 27910144 6259 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6259 603 41 0 6773 0
vsize: 27256
[startup+800.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6333 0 0 0 79989 21 0 0 25 0 1 0 429598076 27910144 6259 4294967295 134512640 134672761 3221224576 3221223776 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6259 603 41 0 6773 0
vsize: 27256
[startup+810.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6333 0 0 0 80989 21 0 0 25 0 1 0 429598076 27910144 6259 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6259 603 41 0 6773 0
vsize: 27256
[startup+820.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6333 0 0 0 81989 21 0 0 25 0 1 0 429598076 27910144 6259 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6259 603 41 0 6773 0
vsize: 27256
[startup+830.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6336 0 0 0 82989 21 0 0 25 0 1 0 429598076 27910144 6262 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6262 603 41 0 6773 0
vsize: 27256
[startup+840.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6336 0 0 0 83990 21 0 0 25 0 1 0 429598076 27910144 6262 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6262 603 41 0 6773 0
vsize: 27256
[startup+850.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6336 0 0 0 84990 21 0 0 25 0 1 0 429598076 27910144 6262 4294967295 134512640 134672761 3221224576 3221223532 1075350790 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6262 603 41 0 6773 0
vsize: 27256
[startup+860.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6336 0 0 0 85990 21 0 0 25 0 1 0 429598076 27910144 6262 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6262 603 41 0 6773 0
vsize: 27256
[startup+870.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6336 0 0 0 86990 21 0 0 25 0 1 0 429598076 27910144 6262 4294967295 134512640 134672761 3221224576 3221223744 134561275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6262 603 41 0 6773 0
vsize: 27256
[startup+880.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6336 0 0 0 87990 21 0 0 25 0 1 0 429598076 27910144 6262 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6262 603 41 0 6773 0
vsize: 27256
[startup+890.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6336 0 0 0 88990 21 0 0 25 0 1 0 429598076 27910144 6262 4294967295 134512640 134672761 3221224576 3221223744 134561156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6262 603 41 0 6773 0
vsize: 27256
[startup+900.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6336 0 0 0 89990 21 0 0 25 0 1 0 429598076 27910144 6262 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6262 603 41 0 6773 0
vsize: 27256
[startup+910.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6336 0 0 0 90991 21 0 0 25 0 1 0 429598076 27910144 6262 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6262 603 41 0 6773 0
vsize: 27256
[startup+920.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6336 0 0 0 91991 21 0 0 25 0 1 0 429598076 27910144 6262 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6262 603 41 0 6773 0
vsize: 27256
[startup+930.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6336 0 0 0 92991 21 0 0 25 0 1 0 429598076 27910144 6262 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6262 603 41 0 6773 0
vsize: 27256
[startup+940.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6336 0 0 0 93991 21 0 0 25 0 1 0 429598076 27910144 6262 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6262 603 41 0 6773 0
vsize: 27256
[startup+950.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6336 0 0 0 94991 21 0 0 25 0 1 0 429598076 27910144 6262 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6262 603 41 0 6773 0
vsize: 27256
[startup+960.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6336 0 0 0 95992 21 0 0 25 0 1 0 429598076 27910144 6262 4294967295 134512640 134672761 3221224576 3221223712 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6262 603 41 0 6773 0
vsize: 27256
[startup+970.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6336 0 0 0 96992 21 0 0 25 0 1 0 429598076 27910144 6262 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6262 603 41 0 6773 0
vsize: 27256
[startup+980.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6336 0 0 0 97992 21 0 0 25 0 1 0 429598076 27910144 6262 4294967295 134512640 134672761 3221224576 3221223680 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6262 603 41 0 6773 0
vsize: 27256
[startup+990.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6336 0 0 0 98992 21 0 0 25 0 1 0 429598076 27910144 6262 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6262 603 41 0 6773 0
vsize: 27256
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6336 0 0 0 99992 21 0 0 25 0 1 0 429598076 27910144 6262 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6262 603 41 0 6773 0
vsize: 27256
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6336 0 0 0 100992 21 0 0 25 0 1 0 429598076 27910144 6262 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6262 603 41 0 6773 0
vsize: 27256
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6336 0 0 0 101992 21 0 0 25 0 1 0 429598076 27910144 6262 4294967295 134512640 134672761 3221224576 3221223680 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6262 603 41 0 6773 0
vsize: 27256
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6336 0 0 0 102993 21 0 0 25 0 1 0 429598076 27910144 6262 4294967295 134512640 134672761 3221224576 3221223744 134560785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6262 603 41 0 6773 0
vsize: 27256
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6336 0 0 0 103993 21 0 0 25 0 1 0 429598076 27910144 6262 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6262 603 41 0 6773 0
vsize: 27256
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6336 0 0 0 104993 21 0 0 25 0 1 0 429598076 27910144 6262 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6262 603 41 0 6773 0
vsize: 27256
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6336 0 0 0 105993 21 0 0 25 0 1 0 429598076 27910144 6262 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6262 603 41 0 6773 0
vsize: 27256
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6336 0 0 0 106993 21 0 0 25 0 1 0 429598076 27910144 6262 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6262 603 41 0 6773 0
vsize: 27256
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6337 0 0 0 107994 21 0 0 25 0 1 0 429598076 27910144 6263 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6263 603 41 0 6773 0
vsize: 27256
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6338 0 0 0 108994 21 0 0 25 0 1 0 429598076 27910144 6264 4294967295 134512640 134672761 3221224576 3221223680 134559979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6264 603 41 0 6773 0
vsize: 27256
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6338 0 0 0 109994 21 0 0 25 0 1 0 429598076 27910144 6264 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6264 603 41 0 6773 0
vsize: 27256
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6339 0 0 0 110994 21 0 0 25 0 1 0 429598076 27910144 6265 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6265 603 41 0 6773 0
vsize: 27256
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6339 0 0 0 111994 21 0 0 25 0 1 0 429598076 27910144 6265 4294967295 134512640 134672761 3221224576 3221223712 134560652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6265 603 41 0 6773 0
vsize: 27256
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6339 0 0 0 112995 21 0 0 25 0 1 0 429598076 27910144 6265 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6265 603 41 0 6773 0
vsize: 27256
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6339 0 0 0 113995 21 0 0 25 0 1 0 429598076 27910144 6265 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6265 603 41 0 6773 0
vsize: 27256
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6400 0 0 0 114995 21 0 0 25 0 1 0 429598076 28176384 6326 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6879 6326 603 41 0 6838 0
vsize: 27516
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6463 0 0 0 115995 21 0 0 25 0 1 0 429598076 28704768 6389 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7008 6389 603 41 0 6967 0
vsize: 28032
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6567 0 0 0 116994 22 0 0 25 0 1 0 429598076 29106176 6493 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7106 6493 603 41 0 7065 0
vsize: 28424
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6625 0 0 0 117995 22 0 0 25 0 1 0 429598076 29294592 6551 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7152 6551 603 41 0 7111 0
vsize: 28608
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6625 0 0 0 118995 22 0 0 25 0 1 0 429598076 29294592 6551 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7152 6551 603 41 0 7111 0
vsize: 28608
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 20937 20936 0 -1 0 6625 0 0 0 119995 22 0 0 25 0 1 0 429598076 29294592 6551 4294967295 134512640 134672761 3221224576 3221223680 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7152 6551 603 41 0 7111 0
vsize: 28608
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.98 0.91 1/54 32737
Raw data (stat): 32737 (minisat+) Z 32736 20937 20936 0 -1 12 6628 0 0 0 119995 23 0 0 25 0 1 0 429598076 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.04
CPU time (s): 1200.19
CPU user time (s): 1199.95
CPU system time (s): 0.238963
CPU usage (%): 100.013
Max. virtual memory (Kb): 28608
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####