PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-misc07.opb
MD5SUM	54df16ee65da54d5975ffedee80d2bb9
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1408128
Optimality of the best value was proved	NO
Number of terms in the objective function	21
Biggest coefficient in the objective function	1048576
Number of bits for the biggest coefficient in the objective function	21
Sum of the numbers in the objective function	2097151
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	1048576
Number of bits of the biggest number in a constraint	21
Biggest sum of numbers in a constraint	11486079
Number of bits of the biggest sum of numbers	24
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.01
Number of variables	280
Total number of constraints	471
Number of constraints which are clauses	127
Number of constraints which are cardinality constraints (but not clauses)	272
Number of constraints which are nor clauses,nor cardinality constraints	72
Minimum length of a constraint	1
Maximum length of a constraint	253
Trace number 18236

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-04-21 14:02:51 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18582 boxname=wulflinc6 idbench=1430 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  54df16ee65da54d5975ffedee80d2bb9  /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-13-7-misc07.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-13-7-misc07.opb
IDLAUNCH: 18582
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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.042
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:        755396 kB
Buffers:         29964 kB
Cached:         227884 kB
SwapCached:        552 kB
Active:          43508 kB
Inactive:       216304 kB
HighTotal:      131008 kB
HighFree:        31416 kB
LowTotal:       903652 kB
LowFree:        723980 kB
SwapTotal:     2097136 kB
SwapFree:      2095720 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5112 kB
Slab:            13756 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 14:22:54 (client local time) WITH STATUS 10 IN 1200.42 SECONDS
stats: 18582 7 1200.42 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 247 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###################################
c   -- Clauses(.)/Splits(s): ...............................................................................................................................
c ---[ 245]---> Adder-cost: 1695   maxlim: 1048703   bits: 22/21
c ---[ 243]---> BDD-cost:   51
c ---[ 241]---> BDD-cost:   51
c ---[ 239]---> BDD-cost:   51
c ---[ 237]---> BDD-cost:   51
c ---[ 235]---> BDD-cost:   51
c ---[ 233]---> BDD-cost:   51
c ---[ 231]---> BDD-cost:   51
c ---[ 230]---> BDD-cost:  239
c ---[ 229]---> BDD-cost:  239
c ---[ 228]---> BDD-cost:  239
c ---[  99]---> Sorter-cost:  127     Base:
c ---[  97]---> Sorter-cost:  127     Base:
c ---[  95]---> Sorter-cost:  127     Base:
c ---[  93]---> Sorter-cost:  127     Base:
c ---[  91]---> Sorter-cost:  127     Base:
c ---[  89]---> Sorter-cost:  127     Base:
c ---[  87]---> Sorter-cost:  127     Base:
c ---[  85]---> Sorter-cost:  127     Base:
c ---[  83]---> Sorter-cost:  127     Base:
c ---[  81]---> Sorter-cost:  127     Base:
c ---[  79]---> Sorter-cost:  127     Base:
c ---[  77]---> Sorter-cost:  127     Base:
c ---[  75]---> Sorter-cost:  127     Base:
c ---[  73]---> Sorter-cost:  127     Base:
c ---[  71]---> Sorter-cost:  127     Base:
c ---[  69]---> Sorter-cost:  127     Base:
c ---[  67]---> Sorter-cost:  127     Base:
c ---[  65]---> Sorter-cost:  127     Base:
c ---[  63]---> Sorter-cost:  127     Base:
c ---[  61]---> Sorter-cost:  127     Base:
c ---[  59]---> Sorter-cost:  127     Base:
c ---[  57]---> Sorter-cost:  127     Base:
c ---[  55]---> Sorter-cost:  127     Base:
c ---[  53]---> Sorter-cost:  127     Base:
c ---[  51]---> Sorter-cost:  127     Base:
c ---[  49]---> Sorter-cost:  127     Base:
c ---[  47]---> Sorter-cost:  127     Base:
c ---[  46]---> BDD-cost:   23
c ---[  45]---> BDD-cost:   23
c ---[  44]---> BDD-cost:   23
c ---[  43]---> BDD-cost:    7
c ---[  42]---> BDD-cost:    7
c ---[  41]---> BDD-cost:   27
c ---[  40]---> BDD-cost:   27
c ---[  39]---> BDD-cost:   27
c ---[  38]---> BDD-cost:   27
c ---[  37]---> BDD-cost:   27
c ---[  36]---> BDD-cost:   27
c ---[  35]---> BDD-cost:   50
c ---[  34]---> BDD-cost:   50
c ---[  33]---> BDD-cost:   50
c ---[  32]---> BDD-cost:   27
c ---[  31]---> BDD-cost:   27
c ---[  30]---> BDD-cost:   27
c ---[  29]---> BDD-cost:   48
c ---[  28]---> BDD-cost:   48
c ---[  27]---> BDD-cost:   48
c ---[  26]---> BDD-cost:   27
c ---[  25]---> BDD-cost:   27
c ---[  24]---> BDD-cost:   27
c ---[  23]---> BDD-cost:   50
c ---[  22]---> BDD-cost:   50
c ---[  21]---> BDD-cost:   50
c ---[  20]---> BDD-cost:   27
c ---[  19]---> BDD-cost:   27
c ---[  18]---> BDD-cost:   27
c ---[  17]---> BDD-cost:   48
c ---[  16]---> BDD-cost:   48
c ---[  15]---> BDD-cost:   48
c ---[  14]---> BDD-cost:   27
c ---[  13]---> BDD-cost:   27
c ---[  12]---> BDD-cost:   27
c ---[  11]---> BDD-cost:   50
c ---[  10]---> BDD-cost:   50
c ---[   9]---> BDD-cost:   50
c ---[   8]---> BDD-cost:   27
c ---[   7]---> BDD-cost:   27
c ---[   6]---> BDD-cost:   27
c ---[   5]---> BDD-cost:   48
c ---[   4]---> BDD-cost:   48
c ---[   3]---> BDD-cost:   48
c ---[   2]---> BDD-cost:   27
c ---[   1]---> BDD-cost:   27
c ---[   0]---> BDD-cost:   27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   25782    84321 |    8594       0        0     nan |  0.000 % |
c |       104 |   25782    84321 |    9453     104     6117    58.8 |  2.677 % |
c ==============================================================================
c [1mFound solution: 1611648[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       123 |   25795    84354 |    8598     123     6748    54.9 |  2.677 % |
c ==============================================================================
c [1mFound solution: 1508608[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       125 |   25808    84385 |    8602     125     6762    54.1 |  2.677 % |
c |       226 |   25808    84385 |    9462     226    17913    79.3 |  2.700 % |
c |       376 |   25808    84385 |   10408     376    23984    63.8 |  2.700 % |
c |       602 |   25808    84385 |   11449     602    49428    82.1 |  2.700 % |
c |       939 |   25787    84310 |   12594     937    66619    71.1 |  2.715 % |
c |      1446 |   25787    84310 |   13853    1444   118779    82.3 |  2.715 % |
c |      2206 |   25732    84151 |   15238    2192   175466    80.0 |  2.845 % |
c ==============================================================================
c [1mFound solution: 1476608[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2813 |   25675    84026 |    8558    2786   202362    72.6 |  2.845 % |
c |      2914 |   25675    84026 |    9413    2887   216333    74.9 |  3.131 % |
c |      3064 |   25675    84026 |   10355    3037   232590    76.6 |  3.131 % |
c |      3290 |   25651    83953 |   11390    3260   236544    72.6 |  3.189 % |
c |      3628 |   25623    83890 |   12529    3595   279647    77.8 |  3.290 % |
c |      4136 |   25623    83890 |   13782    4103   311959    76.0 |  3.290 % |
c |      4896 |   25623    83890 |   15161    4863   391121    80.4 |  3.290 % |
c |      6037 |   25623    83890 |   16677    6004   489351    81.5 |  3.290 % |
c |      7749 |   25574    83745 |   18344    7708   650986    84.5 |  3.391 % |
c ==============================================================================
c [1mFound solution: 1470848[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8367 |   25534    83606 |    8511    8319   709343    85.3 |  3.391 % |
c |      8467 |   25513    83531 |    9362    8416   712125    84.6 |  3.502 % |
c |      8618 |   25513    83531 |   10298    8567   720411    84.1 |  3.502 % |
c |      8846 |   25513    83531 |   11328    8795   739938    84.1 |  3.502 % |
c |      9183 |   25513    83531 |   12460    9132   783046    85.7 |  3.502 % |
c |      9690 |   25400    83151 |   13707    9625   842609    87.5 |  3.675 % |
c ==============================================================================
c [1mFound solution: 1465728[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10436 |   25402    83160 |    8467   10369   916955    88.4 |  3.675 % |
c |     10536 |   25402    83160 |    9313    5285   386079    73.1 |  3.729 % |
c |     10686 |   25361    83069 |   10245    5426   393377    72.5 |  3.902 % |
c |     10911 |   25361    83069 |   11269    5651   409599    72.5 |  3.902 % |
c |     11249 |   25361    83069 |   12396    5989   450093    75.2 |  3.902 % |
c |     11755 |   25328    82952 |   13636    6486   476029    73.4 |  3.930 % |
c |     12517 |   25328    82952 |   14999    7248   532015    73.4 |  3.930 % |
c |     13656 |   25328    82952 |   16499    8387   624983    74.5 |  3.930 % |
c |     15365 |   25328    82952 |   18149   10096   891959    88.3 |  3.930 % |
c |     17927 |   25321    82937 |   19964   12657  1137466    89.9 |  3.959 % |
c ==============================================================================
c [1mFound solution: 1459328[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18442 |   25337    82974 |    8445   13172  1195556    90.8 |  3.959 % |
c |     18544 |   25337    82974 |    9289    6688   584306    87.4 |  3.969 % |
c |     18698 |   25337    82974 |   10218    6842   607049    88.7 |  3.969 % |
c |     18923 |   25232    82626 |   11240    7056   627855    89.0 |  4.170 % |
c |     19263 |   25187    82494 |   12364    7389   652013    88.2 |  4.285 % |
c |     19770 |   25170    82456 |   13600    7895   721465    91.4 |  4.357 % |
c |     20529 |   25170    82456 |   14960    8654   806216    93.2 |  4.357 % |
c |     21671 |   25127    82305 |   16456    9793   890194    90.9 |  4.443 % |
c ==============================================================================
c [1mFound solution: 1440128[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22665 |   25125    82307 |    8375   10784  1014528    94.1 |  4.443 % |
c |     22765 |   25125    82307 |    9212    5492   368580    67.1 |  4.497 % |
c |     22916 |   25125    82307 |   10133    5643   371798    65.9 |  4.497 % |
c |     23143 |   25114    82283 |   11147    5869   407568    69.4 |  4.540 % |
c |     23480 |   25114    82283 |   12261    6206   427989    69.0 |  4.540 % |
c ==============================================================================
c [1mFound solution: 1429248[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23792 |   25125    82313 |    8375    6518   470528    72.2 |  4.540 % |
c |     23896 |   25125    82313 |    9212    6622   482346    72.8 |  4.550 % |
c |     24046 |   25044    82051 |   10133    6765   493619    73.0 |  4.722 % |
c |     24274 |   24863    81448 |   11147    6973   507046    72.7 |  5.038 % |
c |     24613 |   24844    81404 |   12261    7307   529616    72.5 |  5.110 % |
c |     25119 |   24844    81404 |   13488    7813   610135    78.1 |  5.110 % |
c |     25880 |   24844    81404 |   14836    8574   646861    75.4 |  5.110 % |
c |     27022 |   24824    81360 |   16320    9711   732271    75.4 |  5.196 % |
c |     28734 |   24824    81360 |   17952   11423   891715    78.1 |  5.196 % |
c |     31297 |   24824    81360 |   19747   13986  1292109    92.4 |  5.196 % |
c |     35141 |   24802    81312 |   21722   17826  1712988    96.1 |  5.282 % |
c |     40907 |   24784    81273 |   23894   23589  2293176    97.2 |  5.354 % |
c |     49556 |   24773    81249 |   26284   20011  2092469   104.6 |  5.397 % |
c |     62530 |   24740    81132 |   28912   19252  1361391    70.7 |  5.426 % |
c |     81991 |   24660    80889 |   31804   23203  1916008    82.6 |  5.641 % |
c ==============================================================================
c [1mFound solution: 1419008[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86665 |   24652    80876 |    8217   27873  2312061    82.9 |  5.641 % |
c |     86765 |   24652    80876 |    9038    7069   359139    50.8 |  5.734 % |
c |     86915 |   24589    80694 |    9942    7212   361365    50.1 |  5.906 % |
c |     87140 |   24589    80694 |   10936    7437   379936    51.1 |  5.906 % |
c |     87478 |   24543    80590 |   12030    7770   392965    50.6 |  6.121 % |
c |     87985 |   24543    80590 |   13233    8277   449311    54.3 |  6.121 % |
c |     88744 |   24543    80590 |   14556    9036   528727    58.5 |  6.121 % |
c |     89885 |   24543    80590 |   16012   10177   658551    64.7 |  6.121 % |
c |     91595 |   24543    80590 |   17613   11887   865744    72.8 |  6.121 % |
c |     94157 |   24493    80427 |   19375   14439  1148273    79.5 |  6.221 % |
c |     98002 |   24449    80290 |   21312   18275  1436698    78.6 |  6.322 % |
c |    103768 |   24432    80252 |   23444   12999   898365    69.1 |  6.393 % |
c |    112417 |   24421    80228 |   25788   21646  1813298    83.8 |  6.436 % |
c |    125391 |   24421    80228 |   28367   20828  1681241    80.7 |  6.436 % |
c |    144852 |   24406    80175 |   31204   24623  2133182    86.6 |  6.451 % |
c ==============================================================================
c [1mFound solution: 1415168[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    162569 |   24351    80012 |    8117   23650  2252373    95.2 |  6.451 % |
c |    162670 |   24351    80012 |    8928    6014   408136    67.9 |  6.645 % |
c |    162820 |   24351    80012 |    9821    6164   422946    68.6 |  6.645 % |
c |    163045 |   24351    80012 |   10803    6389   443258    69.4 |  6.645 % |
c |    163382 |   24351    80012 |   11884    6726   487694    72.5 |  6.645 % |
c |    163888 |   24351    80012 |   13072    7232   518741    71.7 |  6.645 % |
c |    164651 |   24338    79983 |   14379    7993   606780    75.9 |  6.702 % |
c |    165792 |   24338    79983 |   15817    9134   770652    84.4 |  6.702 % |
c |    167500 |   24338    79983 |   17399   10842   883396    81.5 |  6.702 % |
c |    170062 |   24329    79952 |   19139   13401  1257807    93.9 |  6.716 % |
c |    173906 |   24318    79928 |   21053   17243  1583558    91.8 |  6.759 % |
c |    179672 |   24318    79928 |   23158   11574   882126    76.2 |  6.759 % |
c |    188322 |   24318    79928 |   25474   20224  1960555    96.9 |  6.759 % |
c |    201298 |   24296    79880 |   28022   20015  1816864    90.8 |  6.845 % |
c ==============================================================================
c [1mFound solution: 1408128[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    209149 |   24306    79907 |    8102   27866  2723490    97.7 |  6.845 % |
c |    209250 |   24306    79907 |    8912    7068   466379    66.0 |  6.853 % |
c |    209401 |   24306    79907 |    9803    7219   479276    66.4 |  6.853 % |
c |    209627 |   24306    79907 |   10783    7445   508961    68.4 |  6.853 % |
c |    209967 |   24306    79907 |   11862    7785   532660    68.4 |  6.853 % |
c |    210473 |   24306    79907 |   13048    8291   602654    72.7 |  6.853 % |
c |    211232 |   24241    79734 |   14353    9039   675578    74.7 |  7.067 % |
c |    212372 |   24241    79734 |   15788   10179   812871    79.9 |  7.067 % |
c |    214080 |   24230    79710 |   17367   11884   928908    78.2 |  7.110 % |
c |    216643 |   24224    79690 |   19104   14443  1193339    82.6 |  7.124 % |
c |    220487 |   24224    79690 |   21014   18287  1514845    82.8 |  7.124 % |
c |    226254 |   24224    79690 |   23115   13248  1001035    75.6 |  7.124 % |
c |    234904 |   24224    79690 |   25427   21898  1857367    84.8 |  7.124 % |
c |    247878 |   24201    79627 |   27970   21357  1844939    86.4 |  7.210 % |
c |    267340 |   24011    79030 |   30767   25653  2211361    86.2 |  7.639 % |
c |    296534 |   23994    78992 |   33844   22302  2056277    92.2 |  7.711 % |
c |    340323 |   23969    78936 |   37228   27120  2364139    87.2 |  7.811 % |
#### 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.66 0.85 0.88 2/54 17534
Raw data (stat): 17534 (runsolver) R 17533 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487425665 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0006 s]
Raw data (loadavg): 0.71 0.86 0.88 2/54 17534
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 1867 0 0 0 994 4 0 0 25 0 1 0 487425665 9039872 1798 4294967295 134512640 134672761 3221224624 3221223808 134559613 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2207 1798 603 41 0 2166 0
vsize: 8828
[startup+20.0021 s]
Raw data (loadavg): 0.75 0.86 0.88 2/54 17534
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 2256 0 0 0 1993 6 0 0 25 0 1 0 487425665 10678272 2187 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2607 2187 603 41 0 2566 0
vsize: 10428
[startup+30.0027 s]
Raw data (loadavg): 0.79 0.86 0.88 2/54 17534
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 2524 0 0 0 2991 8 0 0 25 0 1 0 487425665 11747328 2455 4294967295 134512640 134672761 3221224624 3221223792 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2868 2455 603 41 0 2827 0
vsize: 11472
[startup+40.0034 s]
Raw data (loadavg): 0.82 0.87 0.88 2/54 17534
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 2609 0 0 0 3991 9 0 0 25 0 1 0 487425665 12152832 2540 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2967 2540 603 41 0 2926 0
vsize: 11868
[startup+50.0045 s]
Raw data (loadavg): 0.85 0.87 0.89 2/54 17534
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 2609 0 0 0 4991 9 0 0 25 0 1 0 487425665 12152832 2540 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2967 2540 603 41 0 2926 0
vsize: 11868
[startup+60.0051 s]
Raw data (loadavg): 0.87 0.87 0.89 2/54 17534
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 2885 0 0 0 5990 10 0 0 25 0 1 0 487425665 13209600 2816 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3225 2816 603 41 0 3184 0
vsize: 12900
[startup+70.0055 s]
Raw data (loadavg): 0.89 0.88 0.89 2/54 17534
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 3422 0 0 0 6988 13 0 0 25 0 1 0 487425665 15462400 3353 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3775 3353 603 41 0 3734 0
vsize: 15100
[startup+80.0066 s]
Raw data (loadavg): 0.91 0.88 0.89 2/54 17534
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 3909 0 0 0 7987 15 0 0 25 0 1 0 487425665 17473536 3840 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4266 3840 603 41 0 4225 0
vsize: 17064
[startup+90.0065 s]
Raw data (loadavg): 0.92 0.89 0.89 2/54 17534
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 3942 0 0 0 8987 15 0 0 25 0 1 0 487425665 17604608 3873 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4298 3873 603 41 0 4257 0
vsize: 17192
[startup+100.007 s]
Raw data (loadavg): 0.93 0.89 0.89 2/54 17534
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 3942 0 0 0 9987 15 0 0 25 0 1 0 487425665 17604608 3873 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4298 3873 603 41 0 4257 0
vsize: 17192
[startup+110.008 s]
Raw data (loadavg): 0.94 0.89 0.89 2/54 17534
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 4140 0 0 0 10987 16 0 0 25 0 1 0 487425665 18423808 4071 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4498 4071 603 41 0 4457 0
vsize: 17992
[startup+120.009 s]
Raw data (loadavg): 0.95 0.89 0.89 2/54 17534
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 4296 0 0 0 11987 16 0 0 25 0 1 0 487425665 19087360 4227 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4660 4227 603 41 0 4619 0
vsize: 18640
[startup+130.009 s]
Raw data (loadavg): 0.96 0.90 0.89 2/54 17534
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 4296 0 0 0 12987 16 0 0 25 0 1 0 487425665 19087360 4227 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4660 4227 603 41 0 4619 0
vsize: 18640
[startup+140.009 s]
Raw data (loadavg): 0.96 0.90 0.89 2/54 17534
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 4296 0 0 0 13987 16 0 0 25 0 1 0 487425665 19087360 4227 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4660 4227 603 41 0 4619 0
vsize: 18640
[startup+150.009 s]
Raw data (loadavg): 0.97 0.90 0.90 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 4297 0 0 0 14988 16 0 0 25 0 1 0 487425665 19087360 4228 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4660 4228 603 41 0 4619 0
vsize: 18640
[startup+160.01 s]
Raw data (loadavg): 0.97 0.91 0.90 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 4299 0 0 0 15988 16 0 0 25 0 1 0 487425665 19087360 4230 4294967295 134512640 134672761 3221224624 3221223728 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4660 4230 603 41 0 4619 0
vsize: 18640
[startup+170.01 s]
Raw data (loadavg): 0.98 0.91 0.90 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 4300 0 0 0 16988 16 0 0 25 0 1 0 487425665 19087360 4231 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4660 4231 603 41 0 4619 0
vsize: 18640
[startup+180.01 s]
Raw data (loadavg): 0.98 0.91 0.90 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 4300 0 0 0 17989 16 0 0 25 0 1 0 487425665 19087360 4231 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4660 4231 603 41 0 4619 0
vsize: 18640
[startup+190.011 s]
Raw data (loadavg): 0.98 0.91 0.90 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 4300 0 0 0 18989 16 0 0 25 0 1 0 487425665 19087360 4231 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4660 4231 603 41 0 4619 0
vsize: 18640
[startup+200.011 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 4300 0 0 0 19989 16 0 0 25 0 1 0 487425665 19087360 4231 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4660 4231 603 41 0 4619 0
vsize: 18640
[startup+210.011 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 4300 0 0 0 20990 16 0 0 25 0 1 0 487425665 19087360 4231 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4660 4231 603 41 0 4619 0
vsize: 18640
[startup+220.011 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 4300 0 0 0 21990 16 0 0 25 0 1 0 487425665 19087360 4231 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4660 4231 603 41 0 4619 0
vsize: 18640
[startup+230.012 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 4300 0 0 0 22990 16 0 0 25 0 1 0 487425665 19087360 4231 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4660 4231 603 41 0 4619 0
vsize: 18640
[startup+240.012 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 4300 0 0 0 23991 16 0 0 25 0 1 0 487425665 19087360 4231 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4660 4231 603 41 0 4619 0
vsize: 18640
[startup+250.012 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 4300 0 0 0 24991 16 0 0 25 0 1 0 487425665 19087360 4231 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4660 4231 603 41 0 4619 0
vsize: 18640
[startup+260.012 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 4300 0 0 0 25991 16 0 0 25 0 1 0 487425665 19087360 4231 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4660 4231 603 41 0 4619 0
vsize: 18640
[startup+270.012 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 4300 0 0 0 26992 16 0 0 25 0 1 0 487425665 19087360 4231 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4660 4231 603 41 0 4619 0
vsize: 18640
[startup+280.012 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 4337 0 0 0 27992 16 0 0 25 0 1 0 487425665 19218432 4268 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4692 4268 603 41 0 4651 0
vsize: 18768
[startup+290.013 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 4341 0 0 0 28992 16 0 0 25 0 1 0 487425665 19218432 4272 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4692 4272 603 41 0 4651 0
vsize: 18768
[startup+300.013 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 4357 0 0 0 29993 16 0 0 25 0 1 0 487425665 19218432 4288 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4692 4288 603 41 0 4651 0
vsize: 18768
[startup+310.013 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 4809 0 0 0 30992 17 0 0 25 0 1 0 487425665 21086208 4740 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5148 4740 603 41 0 5107 0
vsize: 20592
[startup+320.017 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 4809 0 0 0 31993 17 0 0 25 0 1 0 487425665 21086208 4740 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5148 4740 603 41 0 5107 0
vsize: 20592
[startup+330.022 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 4809 0 0 0 32994 17 0 0 25 0 1 0 487425665 21086208 4740 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5148 4740 603 41 0 5107 0
vsize: 20592
[startup+340.023 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 4820 0 0 0 33994 17 0 0 25 0 1 0 487425665 21221376 4751 4294967295 134512640 134672761 3221224624 3221223808 134559365 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5181 4751 603 41 0 5140 0
vsize: 20724
[startup+350.023 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 4834 0 0 0 34994 17 0 0 25 0 1 0 487425665 21221376 4765 4294967295 134512640 134672761 3221224624 3221223792 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5181 4765 603 41 0 5140 0
vsize: 20724
[startup+360.024 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 4992 0 0 0 35994 18 0 0 25 0 1 0 487425665 22020096 4923 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5376 4923 603 41 0 5335 0
vsize: 21504
[startup+370.025 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5315 0 0 0 36993 19 0 0 25 0 1 0 487425665 23359488 5246 4294967295 134512640 134672761 3221224624 3221223744 134542715 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5703 5246 603 41 0 5662 0
vsize: 22812
[startup+380.025 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5316 0 0 0 37994 19 0 0 25 0 1 0 487425665 23359488 5247 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5703 5247 603 41 0 5662 0
vsize: 22812
[startup+390.025 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5316 0 0 0 38994 19 0 0 25 0 1 0 487425665 23359488 5247 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5703 5247 603 41 0 5662 0
vsize: 22812
[startup+400.025 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5316 0 0 0 39994 19 0 0 25 0 1 0 487425665 23359488 5247 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5703 5247 603 41 0 5662 0
vsize: 22812
[startup+410.026 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5316 0 0 0 40995 19 0 0 25 0 1 0 487425665 23359488 5247 4294967295 134512640 134672761 3221224624 3221223792 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5703 5247 603 41 0 5662 0
vsize: 22812
[startup+420.026 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5316 0 0 0 41995 19 0 0 25 0 1 0 487425665 23359488 5247 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5703 5247 603 41 0 5662 0
vsize: 22812
[startup+430.027 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5316 0 0 0 42995 19 0 0 25 0 1 0 487425665 23359488 5247 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5703 5247 603 41 0 5662 0
vsize: 22812
[startup+440.027 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5316 0 0 0 43996 19 0 0 25 0 1 0 487425665 23359488 5247 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5703 5247 603 41 0 5662 0
vsize: 22812
[startup+450.027 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5316 0 0 0 44996 19 0 0 25 0 1 0 487425665 23359488 5247 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5703 5247 603 41 0 5662 0
vsize: 22812
[startup+460.027 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5316 0 0 0 45996 19 0 0 25 0 1 0 487425665 23359488 5247 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5703 5247 603 41 0 5662 0
vsize: 22812
[startup+470.029 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5316 0 0 0 46997 19 0 0 25 0 1 0 487425665 23359488 5247 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5703 5247 603 41 0 5662 0
vsize: 22812
[startup+480.029 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5316 0 0 0 47997 19 0 0 25 0 1 0 487425665 23359488 5247 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5703 5247 603 41 0 5662 0
vsize: 22812
[startup+490.029 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5316 0 0 0 48997 19 0 0 25 0 1 0 487425665 23359488 5247 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5703 5247 603 41 0 5662 0
vsize: 22812
[startup+500.03 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5316 0 0 0 49998 19 0 0 25 0 1 0 487425665 23359488 5247 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5703 5247 603 41 0 5662 0
vsize: 22812
[startup+510.031 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5316 0 0 0 50998 19 0 0 25 0 1 0 487425665 23359488 5247 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5703 5247 603 41 0 5662 0
vsize: 22812
[startup+520.031 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5316 0 0 0 51999 19 0 0 25 0 1 0 487425665 23359488 5247 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5703 5247 603 41 0 5662 0
vsize: 22812
[startup+530.031 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5316 0 0 0 52999 19 0 0 25 0 1 0 487425665 23359488 5247 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5703 5247 603 41 0 5662 0
vsize: 22812
[startup+540.033 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5316 0 0 0 53999 19 0 0 25 0 1 0 487425665 23359488 5247 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5703 5247 603 41 0 5662 0
vsize: 22812
[startup+550.033 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5316 0 0 0 55000 19 0 0 25 0 1 0 487425665 23359488 5247 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5703 5247 603 41 0 5662 0
vsize: 22812
[startup+560.033 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5316 0 0 0 56000 19 0 0 25 0 1 0 487425665 23359488 5247 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5703 5247 603 41 0 5662 0
vsize: 22812
[startup+570.034 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5316 0 0 0 57000 19 0 0 25 0 1 0 487425665 23359488 5247 4294967295 134512640 134672761 3221224624 3221223728 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5703 5247 603 41 0 5662 0
vsize: 22812
[startup+580.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5316 0 0 0 58001 19 0 0 25 0 1 0 487425665 23359488 5247 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5703 5247 603 41 0 5662 0
vsize: 22812
[startup+590.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5316 0 0 0 59001 19 0 0 25 0 1 0 487425665 23359488 5247 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5703 5247 603 41 0 5662 0
vsize: 22812
[startup+600.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5316 0 0 0 60001 19 0 0 25 0 1 0 487425665 23359488 5247 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5703 5247 603 41 0 5662 0
vsize: 22812
[startup+610.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5316 0 0 0 61002 19 0 0 25 0 1 0 487425665 23359488 5247 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5703 5247 603 41 0 5662 0
vsize: 22812
[startup+620.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5316 0 0 0 62002 19 0 0 25 0 1 0 487425665 23359488 5247 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5703 5247 603 41 0 5662 0
vsize: 22812
[startup+630.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5316 0 0 0 63003 19 0 0 25 0 1 0 487425665 23359488 5247 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5703 5247 603 41 0 5662 0
vsize: 22812
[startup+640.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5316 0 0 0 64003 19 0 0 25 0 1 0 487425665 23359488 5247 4294967295 134512640 134672761 3221224624 3221223808 134558775 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5703 5247 603 41 0 5662 0
vsize: 22812
[startup+650.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5316 0 0 0 65004 19 0 0 25 0 1 0 487425665 23359488 5247 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5703 5247 603 41 0 5662 0
vsize: 22812
[startup+660.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5316 0 0 0 66004 19 0 0 25 0 1 0 487425665 23359488 5247 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5703 5247 603 41 0 5662 0
vsize: 22812
[startup+670.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5316 0 0 0 67004 19 0 0 25 0 1 0 487425665 23359488 5247 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5703 5247 603 41 0 5662 0
vsize: 22812
[startup+680.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5316 0 0 0 68005 19 0 0 25 0 1 0 487425665 23359488 5247 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5703 5247 603 41 0 5662 0
vsize: 22812
[startup+690.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5316 0 0 0 69005 19 0 0 25 0 1 0 487425665 23359488 5247 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5703 5247 603 41 0 5662 0
vsize: 22812
[startup+700.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5316 0 0 0 70005 19 0 0 25 0 1 0 487425665 23359488 5247 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5703 5247 603 41 0 5662 0
vsize: 22812
[startup+710.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5376 0 0 0 71006 20 0 0 25 0 1 0 487425665 23625728 5307 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5768 5307 603 41 0 5727 0
vsize: 23072
[startup+720.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5376 0 0 0 72006 20 0 0 25 0 1 0 487425665 23625728 5307 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5768 5307 603 41 0 5727 0
vsize: 23072
[startup+730.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5388 0 0 0 73006 20 0 0 25 0 1 0 487425665 23625728 5319 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5768 5319 603 41 0 5727 0
vsize: 23072
[startup+740.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5388 0 0 0 74007 20 0 0 25 0 1 0 487425665 23625728 5319 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5768 5319 603 41 0 5727 0
vsize: 23072
[startup+750.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5420 0 0 0 75007 20 0 0 25 0 1 0 487425665 23769088 5351 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5803 5351 603 41 0 5762 0
vsize: 23212
[startup+760.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5450 0 0 0 76007 20 0 0 25 0 1 0 487425665 23932928 5381 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5843 5381 603 41 0 5802 0
vsize: 23372
[startup+770.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5466 0 0 0 77007 20 0 0 25 0 1 0 487425665 24096768 5397 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5883 5397 603 41 0 5842 0
vsize: 23532
[startup+780.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5487 0 0 0 78008 20 0 0 25 0 1 0 487425665 24096768 5418 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5883 5418 603 41 0 5842 0
vsize: 23532
[startup+790.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5504 0 0 0 79008 20 0 0 25 0 1 0 487425665 24260608 5435 4294967295 134512640 134672761 3221224624 3221223760 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5923 5435 603 41 0 5882 0
vsize: 23692
[startup+800.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5611 0 0 0 80008 20 0 0 25 0 1 0 487425665 24686592 5542 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6027 5542 603 41 0 5986 0
vsize: 24108
[startup+810.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5826 0 0 0 81007 22 0 0 25 0 1 0 487425665 25690112 5757 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6272 5757 603 41 0 6231 0
vsize: 25088
[startup+820.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5907 0 0 0 82007 22 0 0 25 0 1 0 487425665 25956352 5838 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6337 5838 603 41 0 6296 0
vsize: 25348
[startup+830.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5907 0 0 0 83007 22 0 0 25 0 1 0 487425665 25956352 5838 4294967295 134512640 134672761 3221224624 3221223792 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6337 5838 603 41 0 6296 0
vsize: 25348
[startup+840.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5926 0 0 0 84008 22 0 0 25 0 1 0 487425665 26112000 5857 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6375 5857 603 41 0 6334 0
vsize: 25500
[startup+850.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5965 0 0 0 85008 22 0 0 25 0 1 0 487425665 26275840 5896 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6415 5896 603 41 0 6374 0
vsize: 25660
[startup+860.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 5991 0 0 0 86007 22 0 0 25 0 1 0 487425665 26439680 5922 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6455 5922 603 41 0 6414 0
vsize: 25820
[startup+870.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 6014 0 0 0 87007 22 0 0 25 0 1 0 487425665 26603520 5945 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6495 5945 603 41 0 6454 0
vsize: 25980
[startup+880.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 6017 0 0 0 88008 22 0 0 25 0 1 0 487425665 26603520 5948 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6495 5948 603 41 0 6454 0
vsize: 25980
[startup+890.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 6104 0 0 0 89007 23 0 0 25 0 1 0 487425665 27000832 6035 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6592 6035 603 41 0 6551 0
vsize: 26368
[startup+900.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 6469 0 0 0 90007 24 0 0 25 0 1 0 487425665 28471296 6400 4294967295 134512640 134672761 3221224624 3221223792 134561372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6951 6400 603 41 0 6910 0
vsize: 27804
[startup+910.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 6469 0 0 0 91007 24 0 0 25 0 1 0 487425665 28471296 6400 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6951 6400 603 41 0 6910 0
vsize: 27804
[startup+920.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 6469 0 0 0 92007 24 0 0 25 0 1 0 487425665 28471296 6400 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6951 6400 603 41 0 6910 0
vsize: 27804
[startup+930.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 6469 0 0 0 93008 24 0 0 25 0 1 0 487425665 28471296 6400 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6951 6400 603 41 0 6910 0
vsize: 27804
[startup+940.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 6469 0 0 0 94008 24 0 0 25 0 1 0 487425665 28471296 6400 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6951 6400 603 41 0 6910 0
vsize: 27804
[startup+950.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 6469 0 0 0 95008 24 0 0 25 0 1 0 487425665 28471296 6400 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6951 6400 603 41 0 6910 0
vsize: 27804
[startup+960.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 6470 0 0 0 96009 24 0 0 25 0 1 0 487425665 28471296 6401 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6951 6401 603 41 0 6910 0
vsize: 27804
[startup+970.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 6470 0 0 0 97009 24 0 0 25 0 1 0 487425665 28471296 6401 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6951 6401 603 41 0 6910 0
vsize: 27804
[startup+980.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 6470 0 0 0 98009 24 0 0 25 0 1 0 487425665 28471296 6401 4294967295 134512640 134672761 3221224624 3221223760 134560650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6951 6401 603 41 0 6910 0
vsize: 27804
[startup+990.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 6470 0 0 0 99009 24 0 0 25 0 1 0 487425665 28471296 6401 4294967295 134512640 134672761 3221224624 3221223728 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6951 6401 603 41 0 6910 0
vsize: 27804
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 6470 0 0 0 100009 24 0 0 25 0 1 0 487425665 28471296 6401 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6951 6401 603 41 0 6910 0
vsize: 27804
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 6470 0 0 0 101009 24 0 0 25 0 1 0 487425665 28471296 6401 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6951 6401 603 41 0 6910 0
vsize: 27804
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 6470 0 0 0 102009 24 0 0 25 0 1 0 487425665 28471296 6401 4294967295 134512640 134672761 3221224624 3221223728 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6951 6401 603 41 0 6910 0
vsize: 27804
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 6476 0 0 0 103010 24 0 0 25 0 1 0 487425665 28471296 6407 4294967295 134512640 134672761 3221224624 3221223808 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6951 6407 603 41 0 6910 0
vsize: 27804
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 6477 0 0 0 104010 24 0 0 25 0 1 0 487425665 28471296 6408 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6951 6408 603 41 0 6910 0
vsize: 27804
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 6477 0 0 0 105010 24 0 0 25 0 1 0 487425665 28471296 6408 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6951 6408 603 41 0 6910 0
vsize: 27804
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 6477 0 0 0 106011 24 0 0 25 0 1 0 487425665 28471296 6408 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6951 6408 603 41 0 6910 0
vsize: 27804
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 6485 0 0 0 107011 24 0 0 25 0 1 0 487425665 28471296 6416 4294967295 134512640 134672761 3221224624 3221223760 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6951 6416 603 41 0 6910 0
vsize: 27804
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 6485 0 0 0 108012 24 0 0 25 0 1 0 487425665 28471296 6416 4294967295 134512640 134672761 3221224624 3221223728 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6951 6416 603 41 0 6910 0
vsize: 27804
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 6485 0 0 0 109012 24 0 0 25 0 1 0 487425665 28471296 6416 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6951 6416 603 41 0 6910 0
vsize: 27804
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 6509 0 0 0 110012 24 0 0 25 0 1 0 487425665 28606464 6440 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6984 6440 603 41 0 6943 0
vsize: 27936
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 6516 0 0 0 111012 24 0 0 25 0 1 0 487425665 28606464 6447 4294967295 134512640 134672761 3221224624 3221223792 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6984 6447 603 41 0 6943 0
vsize: 27936
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 6520 0 0 0 112013 24 0 0 25 0 1 0 487425665 28606464 6451 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6984 6451 603 41 0 6943 0
vsize: 27936
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 6522 0 0 0 113013 24 0 0 25 0 1 0 487425665 28606464 6453 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6984 6453 603 41 0 6943 0
vsize: 27936
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 6556 0 0 0 114013 25 0 0 25 0 1 0 487425665 28798976 6487 4294967295 134512640 134672761 3221224624 3221223792 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7031 6487 603 41 0 6990 0
vsize: 28124
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 6560 0 0 0 115014 25 0 0 25 0 1 0 487425665 28798976 6491 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7031 6491 603 41 0 6990 0
vsize: 28124
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 6581 0 0 0 116014 25 0 0 25 0 1 0 487425665 28962816 6512 4294967295 134512640 134672761 3221224624 3221223808 134558761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7071 6512 603 41 0 7030 0
vsize: 28284
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 6581 0 0 0 117014 25 0 0 25 0 1 0 487425665 28962816 6512 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7071 6512 603 41 0 7030 0
vsize: 28284
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 6597 0 0 0 118014 25 0 0 25 0 1 0 487425665 28962816 6528 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7071 6528 603 41 0 7030 0
vsize: 28284
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 6603 0 0 0 119015 25 0 0 25 0 1 0 487425665 29126656 6534 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7111 6534 603 41 0 7070 0
vsize: 28444
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17536
Raw data (stat): 17534 (minisat+) R 17533 29653 29652 0 -1 0 6620 0 0 0 120015 25 0 0 25 0 1 0 487425665 29126656 6551 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7111 6551 603 41 0 7070 0
vsize: 28444
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 17536
Raw data (stat): 17534 (minisat+) Z 17533 29653 29652 0 -1 12 6623 0 0 0 120015 26 0 0 25 0 1 0 487425665 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.05
CPU time (s): 1200.42
CPU user time (s): 1200.16
CPU system time (s): 0.263959
CPU usage (%): 100.03
Max. virtual memory (Kb): 28444
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####