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/miplib/normalized-mps-v2-13-7-misc07.opb
MD5SUM	9cc94d1db4d494288ef67a8d5ad5d77e
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 19133

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-21 18:02:10 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17009 boxname=wulflinc13 idbench=1309 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  9cc94d1db4d494288ef67a8d5ad5d77e  /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-misc07.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-misc07.opb
IDLAUNCH: 17009
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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.242
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        375544 kB
Buffers:         35720 kB
Cached:         600992 kB
SwapCached:        176 kB
Active:         273520 kB
Inactive:       365968 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        375292 kB
SwapTotal:     2097136 kB
SwapFree:      2096860 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6812 kB
Slab:            14012 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 18:22:12 (client local time) WITH STATUS 10 IN 1200.16 SECONDS
stats: 17009 7 1200.16 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.80 0.95 0.91 1/54 22054
Raw data (stat): 22054 (runsolver) D 22053 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 18 0 1 0 488866515 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 3225161850 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.83 0.95 0.91 2/54 22054
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 1866 0 0 0 991 4 0 0 25 0 1 0 488866515 9039872 1797 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2207 1797 603 41 0 2166 0
vsize: 8828
[startup+20.0007 s]
Raw data (loadavg): 0.85 0.95 0.91 2/54 22054
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 2256 0 0 0 1989 5 0 0 25 0 1 0 488866515 10678272 2187 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2607 2187 603 41 0 2566 0
vsize: 10428
[startup+30.0016 s]
Raw data (loadavg): 0.88 0.95 0.91 2/54 22054
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 2519 0 0 0 2988 6 0 0 25 0 1 0 488866515 11747328 2450 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2868 2450 603 41 0 2827 0
vsize: 11472
[startup+40.0017 s]
Raw data (loadavg): 0.89 0.95 0.91 2/54 22054
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 2609 0 0 0 3988 7 0 0 25 0 1 0 488866515 12152832 2540 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2967 2540 603 41 0 2926 0
vsize: 11868
[startup+50.0012 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 22054
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 2609 0 0 0 4988 7 0 0 25 0 1 0 488866515 12152832 2540 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2967 2540 603 41 0 2926 0
vsize: 11868
[startup+60.0006 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 22054
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 2887 0 0 0 5987 7 0 0 25 0 1 0 488866515 13209600 2818 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3225 2818 603 41 0 3184 0
vsize: 12900
[startup+70.0009 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 22054
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 3426 0 0 0 6985 9 0 0 25 0 1 0 488866515 15462400 3357 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3775 3357 603 41 0 3734 0
vsize: 15100
[startup+80.0015 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 22054
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 3915 0 0 0 7983 11 0 0 25 0 1 0 488866515 17473536 3846 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4266 3846 603 41 0 4225 0
vsize: 17064
[startup+90.0017 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 22054
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 3942 0 0 0 8983 11 0 0 25 0 1 0 488866515 17604608 3873 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4298 3873 603 41 0 4257 0
vsize: 17192
[startup+100.002 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 22054
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 3942 0 0 0 9982 12 0 0 25 0 1 0 488866515 17604608 3873 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4298 3873 603 41 0 4257 0
vsize: 17192
[startup+110.002 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 22054
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 4152 0 0 0 10981 13 0 0 25 0 1 0 488866515 18423808 4083 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4498 4083 603 41 0 4457 0
vsize: 17992
[startup+120.002 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 22054
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 4296 0 0 0 11980 14 0 0 25 0 1 0 488866515 19087360 4227 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4660 4227 603 41 0 4619 0
vsize: 18640
[startup+130.003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 22054
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 4296 0 0 0 12980 14 0 0 25 0 1 0 488866515 19087360 4227 4294967295 134512640 134672761 3221224624 3221223760 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4660 4227 603 41 0 4619 0
vsize: 18640
[startup+140.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 22054
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 4296 0 0 0 13980 14 0 0 25 0 1 0 488866515 19087360 4227 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4660 4227 603 41 0 4619 0
vsize: 18640
[startup+150.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 22054
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 4297 0 0 0 14980 15 0 0 25 0 1 0 488866515 19087360 4228 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4660 4228 603 41 0 4619 0
vsize: 18640
[startup+160.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 22054
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 4299 0 0 0 15980 15 0 0 25 0 1 0 488866515 19087360 4230 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4660 4230 603 41 0 4619 0
vsize: 18640
[startup+170.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 22054
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 4300 0 0 0 16979 16 0 0 25 0 1 0 488866515 19087360 4231 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4660 4231 603 41 0 4619 0
vsize: 18640
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22054
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 4300 0 0 0 17979 16 0 0 25 0 1 0 488866515 19087360 4231 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4660 4231 603 41 0 4619 0
vsize: 18640
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22054
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 4300 0 0 0 18979 16 0 0 25 0 1 0 488866515 19087360 4231 4294967295 134512640 134672761 3221224624 3221223824 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4660 4231 603 41 0 4619 0
vsize: 18640
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22054
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 4300 0 0 0 19979 16 0 0 25 0 1 0 488866515 19087360 4231 4294967295 134512640 134672761 3221224624 3221223728 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4660 4231 603 41 0 4619 0
vsize: 18640
[startup+210.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22054
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 4300 0 0 0 20979 17 0 0 25 0 1 0 488866515 19087360 4231 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4660 4231 603 41 0 4619 0
vsize: 18640
[startup+220.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22054
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 4300 0 0 0 21979 17 0 0 25 0 1 0 488866515 19087360 4231 4294967295 134512640 134672761 3221224624 3221223808 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4660 4231 603 41 0 4619 0
vsize: 18640
[startup+230.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22054
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 4300 0 0 0 22979 17 0 0 25 0 1 0 488866515 19087360 4231 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4660 4231 603 41 0 4619 0
vsize: 18640
[startup+240.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22054
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 4300 0 0 0 23978 17 0 0 25 0 1 0 488866515 19087360 4231 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4660 4231 603 41 0 4619 0
vsize: 18640
[startup+250.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 4300 0 0 0 24978 18 0 0 25 0 1 0 488866515 19087360 4231 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4660 4231 603 41 0 4619 0
vsize: 18640
[startup+260.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 4300 0 0 0 25978 18 0 0 25 0 1 0 488866515 19087360 4231 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4660 4231 603 41 0 4619 0
vsize: 18640
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 4337 0 0 0 26978 18 0 0 25 0 1 0 488866515 19218432 4268 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4692 4268 603 41 0 4651 0
vsize: 18768
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 4337 0 0 0 27977 19 0 0 25 0 1 0 488866515 19218432 4268 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4692 4268 603 41 0 4651 0
vsize: 18768
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 4343 0 0 0 28977 19 0 0 25 0 1 0 488866515 19218432 4274 4294967295 134512640 134672761 3221224624 3221223808 134558914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4692 4274 603 41 0 4651 0
vsize: 18768
[startup+300.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 4451 0 0 0 29976 20 0 0 25 0 1 0 488866515 19623936 4382 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4791 4382 603 41 0 4750 0
vsize: 19164
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 4809 0 0 0 30975 21 0 0 25 0 1 0 488866515 21086208 4740 4294967295 134512640 134672761 3221224624 3221223792 134561198 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.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 4809 0 0 0 31976 21 0 0 25 0 1 0 488866515 21086208 4740 4294967295 134512640 134672761 3221224624 3221223792 134561188 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.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 4809 0 0 0 32976 21 0 0 25 0 1 0 488866515 21086208 4740 4294967295 134512640 134672761 3221224624 3221223792 134560983 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.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 4820 0 0 0 33976 21 0 0 25 0 1 0 488866515 21221376 4751 4294967295 134512640 134672761 3221224624 3221223824 134557842 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.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 4838 0 0 0 34976 21 0 0 25 0 1 0 488866515 21221376 4769 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5181 4769 603 41 0 5140 0
vsize: 20724
[startup+360.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5185 0 0 0 35975 22 0 0 25 0 1 0 488866515 22822912 5116 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5572 5116 603 41 0 5531 0
vsize: 22288
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5315 0 0 0 36975 22 0 0 25 0 1 0 488866515 23359488 5246 4294967295 134512640 134672761 3221224624 3221223808 134559334 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5316 0 0 0 37975 22 0 0 25 0 1 0 488866515 23359488 5247 4294967295 134512640 134672761 3221224624 3221223728 134560180 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.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5316 0 0 0 38976 22 0 0 25 0 1 0 488866515 23359488 5247 4294967295 134512640 134672761 3221224624 3221223792 134560956 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.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5316 0 0 0 39976 22 0 0 25 0 1 0 488866515 23359488 5247 4294967295 134512640 134672761 3221224624 3221223728 134560399 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5316 0 0 0 40976 22 0 0 25 0 1 0 488866515 23359488 5247 4294967295 134512640 134672761 3221224624 3221223808 134559405 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.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5316 0 0 0 41976 22 0 0 25 0 1 0 488866515 23359488 5247 4294967295 134512640 134672761 3221224624 3221223728 134560355 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.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5316 0 0 0 42976 22 0 0 25 0 1 0 488866515 23359488 5247 4294967295 134512640 134672761 3221224624 3221223728 134560196 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.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5316 0 0 0 43977 22 0 0 25 0 1 0 488866515 23359488 5247 4294967295 134512640 134672761 3221224624 3221223788 134559748 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5316 0 0 0 44977 22 0 0 25 0 1 0 488866515 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+460.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5316 0 0 0 45977 22 0 0 25 0 1 0 488866515 23359488 5247 4294967295 134512640 134672761 3221224624 3221223792 134560983 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5316 0 0 0 46977 22 0 0 25 0 1 0 488866515 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+480.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5316 0 0 0 47977 22 0 0 25 0 1 0 488866515 23359488 5247 4294967295 134512640 134672761 3221224624 3221223792 134561161 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.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5316 0 0 0 48977 22 0 0 25 0 1 0 488866515 23359488 5247 4294967295 134512640 134672761 3221224624 3221223728 134560235 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.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5316 0 0 0 49978 22 0 0 25 0 1 0 488866515 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.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5316 0 0 0 50978 22 0 0 25 0 1 0 488866515 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+520.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5316 0 0 0 51978 22 0 0 25 0 1 0 488866515 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+530.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5316 0 0 0 52978 22 0 0 25 0 1 0 488866515 23359488 5247 4294967295 134512640 134672761 3221224624 3221223728 134560399 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.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5316 0 0 0 53978 22 0 0 25 0 1 0 488866515 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+550.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5316 0 0 0 54978 22 0 0 25 0 1 0 488866515 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+560.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5316 0 0 0 55979 22 0 0 25 0 1 0 488866515 23359488 5247 4294967295 134512640 134672761 3221224624 3221223792 134561193 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.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5316 0 0 0 56979 22 0 0 25 0 1 0 488866515 23359488 5247 4294967295 134512640 134672761 3221224624 3221223792 134560903 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.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5316 0 0 0 57979 22 0 0 25 0 1 0 488866515 23359488 5247 4294967295 134512640 134672761 3221224624 3221223760 134560718 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5316 0 0 0 58979 22 0 0 25 0 1 0 488866515 23359488 5247 4294967295 134512640 134672761 3221224624 3221223792 134561005 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.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5316 0 0 0 59979 22 0 0 25 0 1 0 488866515 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+610.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5316 0 0 0 60979 22 0 0 25 0 1 0 488866515 23359488 5247 4294967295 134512640 134672761 3221224624 3221223728 134559943 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5316 0 0 0 61979 22 0 0 25 0 1 0 488866515 23359488 5247 4294967295 134512640 134672761 3221224624 3221223632 134565745 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5316 0 0 0 62980 22 0 0 25 0 1 0 488866515 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+640.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5316 0 0 0 63980 22 0 0 25 0 1 0 488866515 23359488 5247 4294967295 134512640 134672761 3221224624 3221223792 134560874 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5316 0 0 0 64980 22 0 0 25 0 1 0 488866515 23359488 5247 4294967295 134512640 134672761 3221224624 3221223792 134561133 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5316 0 0 0 65980 22 0 0 25 0 1 0 488866515 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+670.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5316 0 0 0 66980 22 0 0 25 0 1 0 488866515 23359488 5247 4294967295 134512640 134672761 3221224624 3221223580 1075350205 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.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5316 0 0 0 67983 22 0 0 25 0 1 0 488866515 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+690.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5316 0 0 0 68983 22 0 0 25 0 1 0 488866515 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.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5376 0 0 0 69983 23 0 0 25 0 1 0 488866515 23625728 5307 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5768 5307 603 41 0 5727 0
vsize: 23072
[startup+710.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5376 0 0 0 70983 23 0 0 25 0 1 0 488866515 23625728 5307 4294967295 134512640 134672761 3221224624 3221223792 134561127 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.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5388 0 0 0 71983 23 0 0 25 0 1 0 488866515 23625728 5319 4294967295 134512640 134672761 3221224624 3221223808 134559376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5768 5319 603 41 0 5727 0
vsize: 23072
[startup+730.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5405 0 0 0 72983 23 0 0 25 0 1 0 488866515 23769088 5336 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5803 5336 603 41 0 5762 0
vsize: 23212
[startup+740.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5425 0 0 0 73983 23 0 0 25 0 1 0 488866515 23769088 5356 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5803 5356 603 41 0 5762 0
vsize: 23212
[startup+750.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5450 0 0 0 74984 23 0 0 25 0 1 0 488866515 23932928 5381 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5843 5381 603 41 0 5802 0
vsize: 23372
[startup+760.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5472 0 0 0 75984 23 0 0 25 0 1 0 488866515 24096768 5403 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5883 5403 603 41 0 5842 0
vsize: 23532
[startup+770.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5487 0 0 0 76984 23 0 0 25 0 1 0 488866515 24096768 5418 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5883 5418 603 41 0 5842 0
vsize: 23532
[startup+780.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5518 0 0 0 77984 23 0 0 25 0 1 0 488866515 24260608 5449 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5923 5449 603 41 0 5882 0
vsize: 23692
[startup+790.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5685 0 0 0 78983 24 0 0 25 0 1 0 488866515 25079808 5616 4294967295 134512640 134672761 3221224624 3221223808 134559182 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6123 5616 603 41 0 6082 0
vsize: 24492
[startup+800.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5876 0 0 0 79983 24 0 0 25 0 1 0 488866515 25825280 5807 4294967295 134512640 134672761 3221224624 3221223792 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6305 5807 603 41 0 6264 0
vsize: 25220
[startup+810.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5907 0 0 0 80983 25 0 0 25 0 1 0 488866515 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+820.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5913 0 0 0 81983 25 0 0 25 0 1 0 488866515 26112000 5844 4294967295 134512640 134672761 3221224624 3221223808 134559683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6375 5844 603 41 0 6334 0
vsize: 25500
[startup+830.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5934 0 0 0 82983 25 0 0 25 0 1 0 488866515 26112000 5865 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6375 5865 603 41 0 6334 0
vsize: 25500
[startup+840.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5976 0 0 0 83983 25 0 0 25 0 1 0 488866515 26439680 5907 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6455 5907 603 41 0 6414 0
vsize: 25820
[startup+850.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 5998 0 0 0 84982 26 0 0 25 0 1 0 488866515 26439680 5929 4294967295 134512640 134672761 3221224624 3221223792 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6455 5929 603 41 0 6414 0
vsize: 25820
[startup+860.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6014 0 0 0 85982 26 0 0 25 0 1 0 488866515 26603520 5945 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6495 5945 603 41 0 6454 0
vsize: 25980
[startup+870.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6017 0 0 0 86982 26 0 0 25 0 1 0 488866515 26603520 5948 4294967295 134512640 134672761 3221224624 3221223792 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6495 5948 603 41 0 6454 0
vsize: 25980
[startup+880.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6257 0 0 0 87981 27 0 0 25 0 1 0 488866515 27533312 6188 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6722 6188 603 41 0 6681 0
vsize: 26888
[startup+890.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6469 0 0 0 88980 28 0 0 25 0 1 0 488866515 28471296 6400 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6951 6400 603 41 0 6910 0
vsize: 27804
[startup+900.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6469 0 0 0 89980 28 0 0 25 0 1 0 488866515 28471296 6400 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 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 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6469 0 0 0 90980 28 0 0 25 0 1 0 488866515 28471296 6400 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 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 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6469 0 0 0 91980 29 0 0 25 0 1 0 488866515 28471296 6400 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6951 6400 603 41 0 6910 0
vsize: 27804
[startup+930.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6469 0 0 0 92980 29 0 0 25 0 1 0 488866515 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.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6470 0 0 0 93980 29 0 0 25 0 1 0 488866515 28471296 6401 4294967295 134512640 134672761 3221224624 3221223808 134559176 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6951 6401 603 41 0 6910 0
vsize: 27804
[startup+950.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6470 0 0 0 94980 29 0 0 25 0 1 0 488866515 28471296 6401 4294967295 134512640 134672761 3221224624 3221223760 134560611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6951 6401 603 41 0 6910 0
vsize: 27804
[startup+960.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6470 0 0 0 95980 29 0 0 25 0 1 0 488866515 28471296 6401 4294967295 134512640 134672761 3221224624 3221223772 134560552 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.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6470 0 0 0 96980 29 0 0 25 0 1 0 488866515 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+980.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6470 0 0 0 97980 29 0 0 25 0 1 0 488866515 28471296 6401 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6951 6401 603 41 0 6910 0
vsize: 27804
[startup+990.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6470 0 0 0 98980 29 0 0 25 0 1 0 488866515 28471296 6401 4294967295 134512640 134672761 3221224624 3221223728 134560370 0 0 5 16386 0 0 0 17 1 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 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6470 0 0 0 99981 29 0 0 25 0 1 0 488866515 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+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6476 0 0 0 100981 29 0 0 25 0 1 0 488866515 28471296 6407 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6951 6407 603 41 0 6910 0
vsize: 27804
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6477 0 0 0 101981 29 0 0 25 0 1 0 488866515 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+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6477 0 0 0 102981 29 0 0 25 0 1 0 488866515 28471296 6408 4294967295 134512640 134672761 3221224624 3221223792 134564734 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6951 6408 603 41 0 6910 0
vsize: 27804
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6477 0 0 0 103981 29 0 0 25 0 1 0 488866515 28471296 6408 4294967295 134512640 134672761 3221224624 3221223792 134560869 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 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6478 0 0 0 104982 29 0 0 25 0 1 0 488866515 28471296 6409 4294967295 134512640 134672761 3221224624 3221223808 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6951 6409 603 41 0 6910 0
vsize: 27804
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6485 0 0 0 105982 29 0 0 25 0 1 0 488866515 28471296 6416 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6951 6416 603 41 0 6910 0
vsize: 27804
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6485 0 0 0 106982 29 0 0 25 0 1 0 488866515 28471296 6416 4294967295 134512640 134672761 3221224624 3221223760 134560577 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 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6509 0 0 0 107982 29 0 0 25 0 1 0 488866515 28606464 6440 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6984 6440 603 41 0 6943 0
vsize: 27936
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6516 0 0 0 108982 29 0 0 25 0 1 0 488866515 28606464 6447 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6984 6447 603 41 0 6943 0
vsize: 27936
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6520 0 0 0 109982 29 0 0 25 0 1 0 488866515 28606464 6451 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6984 6451 603 41 0 6943 0
vsize: 27936
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6523 0 0 0 110982 29 0 0 25 0 1 0 488866515 28606464 6454 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6984 6454 603 41 0 6943 0
vsize: 27936
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6557 0 0 0 111983 29 0 0 25 0 1 0 488866515 28798976 6488 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7031 6488 603 41 0 6990 0
vsize: 28124
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6560 0 0 0 112983 29 0 0 25 0 1 0 488866515 28798976 6491 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7031 6491 603 41 0 6990 0
vsize: 28124
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6581 0 0 0 113983 29 0 0 25 0 1 0 488866515 28962816 6512 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7071 6512 603 41 0 7030 0
vsize: 28284
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6581 0 0 0 114983 29 0 0 25 0 1 0 488866515 28962816 6512 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7071 6512 603 41 0 7030 0
vsize: 28284
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6597 0 0 0 115983 29 0 0 25 0 1 0 488866515 28962816 6528 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7071 6528 603 41 0 7030 0
vsize: 28284
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6604 0 0 0 116983 29 0 0 25 0 1 0 488866515 29126656 6535 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7111 6535 603 41 0 7070 0
vsize: 28444
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6620 0 0 0 117984 29 0 0 25 0 1 0 488866515 29126656 6551 4294967295 134512640 134672761 3221224624 3221223760 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7111 6551 603 41 0 7070 0
vsize: 28444
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6628 0 0 0 118984 29 0 0 25 0 1 0 488866515 29126656 6559 4294967295 134512640 134672761 3221224624 3221223792 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7111 6559 603 41 0 7070 0
vsize: 28444
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22056
Raw data (stat): 22054 (minisat+) R 22053 30701 30700 0 -1 0 6639 0 0 0 119984 29 0 0 25 0 1 0 488866515 29323264 6570 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7159 6570 603 41 0 7118 0
vsize: 28636
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 22056
Raw data (stat): 22054 (minisat+) Z 22053 30701 30700 0 -1 12 6642 0 0 0 119984 30 0 0 25 0 1 0 488866515 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.06
CPU time (s): 1200.16
CPU user time (s): 1199.85
CPU system time (s): 0.309952
CPU usage (%): 100.008
Max. virtual memory (Kb): 28636
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####