PB'05 competition: run trace

Some explanations

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

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

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        811604 kB
Buffers:         36632 kB
Cached:         163140 kB
SwapCached:       3276 kB
Active:          86968 kB
Inactive:       118892 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        811352 kB
SwapTotal:     2097136 kB
SwapFree:      2093860 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            11600 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 21:44:55 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 5158 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 133 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###################
c   -- Clauses(.)/Splits(s): .sssss
c ---[ 137]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 136]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 135]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 134]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 133]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 132]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 131]---> Adder-cost: 7   maxlim: 5   bits: 4/3
c ---[ 130]---> Adder-cost: 7   maxlim: 5   bits: 4/3
c ---[ 129]---> Adder-cost: 7   maxlim: 5   bits: 4/3
c ---[ 128]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 127]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 126]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 125]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 124]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 123]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 122]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 121]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 120]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 119]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 118]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 117]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 116]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 115]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 114]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 113]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 112]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 111]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 110]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 109]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 108]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 107]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 106]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 105]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 104]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 103]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 102]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 101]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 100]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  99]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  98]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  97]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  96]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  95]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  94]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  93]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  92]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  91]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  90]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  89]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  88]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  87]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  86]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  85]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  84]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  83]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  82]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  81]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  80]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  79]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  78]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  77]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  76]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  75]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  74]---> Adder-cost: 8   maxlim: 7   bits: 4/3
c ---[  72]---> Adder-cost: 8   maxlim: 8   bits: 4/4
c ---[  70]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[  68]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[  66]---> Adder-cost: 8   maxlim: 8   bits: 4/4
c ---[  64]---> Adder-cost: 8   maxlim: 8   bits: 4/4
c ---[  62]---> Adder-cost: 8   maxlim: 8   bits: 4/4
c ---[  60]---> Adder-cost: 8   maxlim: 8   bits: 4/4
c ---[  58]---> Adder-cost: 8   maxlim: 8   bits: 4/4
c ---[  56]---> Adder-cost: 8   maxlim: 8   bits: 4/4
c ---[  54]---> Adder-cost: 8   maxlim: 8   bits: 4/4
c ---[  52]---> Adder-cost: 8   maxlim: 8   bits: 4/4
c ---[  50]---> Adder-cost: 8   maxlim: 8   bits: 4/4
c ---[  48]---> Adder-cost: 8   maxlim: 8   bits: 4/4
c ---[  46]---> Adder-cost: 8   maxlim: 8   bits: 4/4
c ---[  44]---> Adder-cost: 8   maxlim: 8   bits: 4/4
c ---[  42]---> Adder-cost: 8   maxlim: 8   bits: 4/4
c ---[  40]---> Adder-cost: 8   maxlim: 8   bits: 4/4
c ---[  38]---> Adder-cost: 8   maxlim: 8   bits: 4/4
c ---[  36]---> Adder-cost: 8   maxlim: 8   bits: 4/4
c ---[  31]---> Adder-cost: 42   maxlim: 9   bits: 5/4
c ---[  28]---> Adder-cost: 45   maxlim: 14   bits: 5/4
c ---[  27]---> Adder-cost: 62   maxlim: 14   bits: 5/4
c ---[  26]---> Adder-cost: 62   maxlim: 14   bits: 5/4
c ---[  25]---> Adder-cost: 53   maxlim: 19   bits: 6/5
c ---[  24]---> Adder-cost: 53   maxlim: 19   bits: 6/5
c ---[  23]---> Adder-cost: 57   maxlim: 19   bits: 6/5
c ---[  22]---> Adder-cost: 64   maxlim: 24   bits: 6/5
c ---[  21]---> Adder-cost: 57   maxlim: 24   bits: 6/5
c ---[  20]---> Adder-cost: 57   maxlim: 24   bits: 6/5
c ---[  19]---> Adder-cost: 71   maxlim: 29   bits: 6/5
c ---[  18]---> Adder-cost: 65   maxlim: 29   bits: 6/5
c ---[  17]---> Adder-cost: 65   maxlim: 29   bits: 6/5
c ---[  16]---> Adder-cost: 80   maxlim: 34   bits: 7/6
c ---[  15]---> Adder-cost: 82   maxlim: 34   bits: 7/6
c ---[  14]---> Adder-cost: 82   maxlim: 34   bits: 7/6
c ---[  13]---> Adder-cost: 78   maxlim: 39   bits: 7/6
c ---[  12]---> Adder-cost: 78   maxlim: 39   bits: 7/6
c ---[  11]---> Adder-cost: 83   maxlim: 39   bits: 7/6
c ---[  10]---> Adder-cost: 99   maxlim: 44   bits: 7/6
c ---[   9]---> Adder-cost: 95   maxlim: 44   bits: 7/6
c ---[   8]---> Adder-cost: 95   maxlim: 44   bits: 7/6
c ---[   7]---> Adder-cost: 91   maxlim: 49   bits: 7/6
c ---[   6]---> Adder-cost: 91   maxlim: 49   bits: 7/6
c ---[   5]---> Adder-cost: 100   maxlim: 49   bits: 7/6
c ---[   4]---> Adder-cost: 6   maxlim: 4   bits: 4/3
c ---[   3]---> Adder-cost: 6   maxlim: 4   bits: 4/3
c ---[   2]---> Adder-cost: 6   maxlim: 4   bits: 4/3
c ---[   1]---> Adder-cost: 6   maxlim: 9   bits: 5/4
c ---[   0]---> Adder-cost: 6   maxlim: 9   bits: 5/4
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   13725    48884 |    4575       0        0     nan |  0.000 % |
c |       100 |   13711    48838 |    5032      98      654     6.7 | 15.131 % |
c |       251 |   13671    48702 |    5535     245     1856     7.6 | 15.346 % |
c |       476 |   13621    48524 |    6089     465     3637     7.8 | 15.525 % |
c |       813 |   13531    48202 |    6698     796     6264     7.9 | 15.884 % |
c |      1320 |   13356    47579 |    7368    1277    10652     8.3 | 16.493 % |
c ==============================================================================
c [1mFound solution: 2438[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1192   maxlim: 17542   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1712 |   21490    76632 |    7163    1661    13904     8.4 | 16.493 % |
c ==============================================================================
c [1mFound solution: 2435[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 17545   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1745 |   21496    76670 |    7165    1694    14398     8.5 | 16.493 % |
c |      1845 |   21429    76435 |    7881    1788    15026     8.4 | 12.387 % |
c |      1996 |   21382    76266 |    8669    1932    16396     8.5 | 12.487 % |
c |      2221 |   21307    75995 |    9536    2140    20958     9.8 | 12.663 % |
c |      2559 |   21213    75653 |   10490    2448    24662    10.1 | 12.788 % |
c |      3066 |   21120    75314 |   11539    2946    29837    10.1 | 12.914 % |
c |      3825 |   21120    75314 |   12693    3705    52872    14.3 | 12.914 % |
c ==============================================================================
c [1mFound solution: 2237[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 17743   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4494 |   21114    75302 |    7038    4373    78705    18.0 | 12.914 % |
c |      4594 |   21114    75302 |    7741    4473    79658    17.8 | 13.004 % |
c ==============================================================================
c [1mFound solution: 2140[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 17840   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4734 |   21122    75350 |    7040    4613    85087    18.4 | 13.004 % |
c |      4837 |   21090    75239 |    7744    4711    86390    18.3 | 13.217 % |
c |      4987 |   21090    75239 |    8518    4861    91666    18.9 | 13.217 % |
c |      5212 |   21083    75215 |    9370    5083   101178    19.9 | 13.292 % |
c |      5549 |   21074    75184 |   10307    5416   108840    20.1 | 13.317 % |
c |      6055 |   21074    75184 |   11337    5922   126350    21.3 | 13.317 % |
c |      6815 |   21074    75184 |   12471    6682   144582    21.6 | 13.317 % |
c ==============================================================================
c [1mFound solution: 2074[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 17906   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7853 |   21079    75233 |    7026    7720   221427    28.7 | 13.317 % |
c |      7953 |   21079    75233 |    7728    3960   128082    32.3 | 13.425 % |
c |      8104 |   21079    75233 |    8501    4111   132529    32.2 | 13.425 % |
c |      8329 |   21079    75233 |    9351    4336   139710    32.2 | 13.425 % |
c |      8666 |   21079    75233 |   10286    4673   147979    31.7 | 13.425 % |
c |      9173 |   21025    75041 |   11315    5178   167366    32.3 | 13.575 % |
c |      9932 |   21025    75041 |   12446    5937   213023    35.9 | 13.575 % |
c ==============================================================================
c [1mFound solution: 2008[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 17972   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10183 |   21035    75104 |    7011    6188   217176    35.1 | 13.575 % |
c |     10284 |   21035    75104 |    7712    6289   220959    35.1 | 13.679 % |
c |     10434 |   21035    75104 |    8483    6439   224951    34.9 | 13.679 % |
c |     10660 |   21035    75104 |    9331    6665   229787    34.5 | 13.680 % |
c |     10997 |   21035    75104 |   10264    7002   245934    35.1 | 13.679 % |
c |     11504 |   21035    75104 |   11291    7509   279944    37.3 | 13.679 % |
c |     12264 |   21026    75073 |   12420    8263   299882    36.3 | 13.704 % |
c |     13404 |   21019    75050 |   13662    9402   339391    36.1 | 13.730 % |
c |     15114 |   21019    75050 |   15028   11112   400309    36.0 | 13.729 % |
c |     17678 |   21019    75050 |   16531   13676   552098    40.4 | 13.729 % |
c ==============================================================================
c [1mFound solution: 1856[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 230   maxlim: 16204   bits: 15/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19810 |   22569    80600 |    7523   15780   671358    42.5 | 13.729 % |
c |     19910 |   22569    80600 |    8275    7990   317307    39.7 | 13.230 % |
c |     20060 |   22569    80600 |    9102    8140   321498    39.5 | 13.230 % |
c |     20285 |   22569    80600 |   10013    8365   330030    39.5 | 13.230 % |
c |     20622 |   22569    80600 |   11014    8702   343671    39.5 | 13.230 % |
c |     21129 |   22569    80600 |   12115    9209   371727    40.4 | 13.230 % |
c |     21889 |   22569    80600 |   13327    9969   394809    39.6 | 13.230 % |
c |     23030 |   22556    80559 |   14660   11105   455110    41.0 | 13.277 % |
c |     24742 |   22490    80333 |   16126   12791   562865    44.0 | 13.489 % |
c |     27305 |   22490    80333 |   17738   15354   662102    43.1 | 13.489 % |
c |     31151 |   22490    80333 |   19512   19200   890919    46.4 | 13.489 % |
c |     36918 |   22481    80304 |   21463   14584   676465    46.4 | 13.536 % |
c |     45569 |   22481    80304 |   23610   11994   529332    44.1 | 13.536 % |
c |     58545 |   22481    80304 |   25971   24970  1527732    61.2 | 13.536 % |
c |     78006 |   22460    80235 |   28568   17764   570159    32.1 | 13.724 % |
c |    107198 |   22460    80235 |   31425   29903  1870870    62.6 | 13.724 % |
c ==============================================================================
c [1mFound solution: 1848[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 16212   bits: 15/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    110654 |   22466    80282 |    7488   33359  2088185    62.6 | 13.724 % |
c |    110754 |   22457    80251 |    8236    7289   321929    44.2 | 13.799 % |
c |    110904 |   22457    80251 |    9060    7439   325676    43.8 | 13.799 % |
c |    111129 |   22457    80251 |    9966    7664   332802    43.4 | 13.799 % |
c |    111468 |   22457    80251 |   10963    8003   338721    42.3 | 13.799 % |
c |    111977 |   22457    80251 |   12059    8512   352464    41.4 | 13.799 % |
c |    112738 |   22457    80251 |   13265    9273   413740    44.6 | 13.799 % |
c |    113878 |   22457    80251 |   14591   10413   468719    45.0 | 13.799 % |
c |    115587 |   22448    80220 |   16051   12118   538017    44.4 | 13.822 % |
c |    118151 |   22441    80198 |   17656   14680   671898    45.8 | 13.916 % |
c |    121995 |   22426    80147 |   19421   18519   931201    50.3 | 13.963 % |
c |    127761 |   22366    79929 |   21364   14173   704204    49.7 | 14.034 % |
c |    136411 |   22359    79905 |   23500   22822  1223391    53.6 | 14.104 % |
c |    149389 |   22359    79905 |   25850   22973  1499674    65.3 | 14.104 % |
c |    168850 |   22338    79835 |   28435   15110   784901    51.9 | 14.245 % |
c |    198043 |   22331    79811 |   31279   28539  1962333    68.8 | 14.316 % |
c ==============================================================================
c [1mFound solution: 1845[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 16215   bits: 15/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    199150 |   22332    79824 |    7444   29646  2017749    68.1 | 14.316 % |
c |    199250 |   22332    79824 |    8188    7512   270786    36.0 | 14.336 % |
c |    199402 |   22332    79824 |    9007    7664   276034    36.0 | 14.336 % |
c |    199631 |   22332    79824 |    9907    7893   286816    36.3 | 14.336 % |
c |    199968 |   22332    79824 |   10898    8230   297953    36.2 | 14.336 % |
c |    200474 |   22332    79824 |   11988    8736   316447    36.2 | 14.336 % |
c |    201233 |   22332    79824 |   13187    9495   363622    38.3 | 14.336 % |
c |    202372 |   22332    79824 |   14506   10634   420217    39.5 | 14.336 % |
c |    204080 |   22332    79824 |   15956   12342   512945    41.6 | 14.336 % |
c ==============================================================================
c [1mFound solution: 1842[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 16218   bits: 15/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    204478 |   22336    79859 |    7445   12740   533613    41.9 | 14.336 % |
c |    204580 |   22336    79859 |    8189    6472   207617    32.1 | 14.370 % |
c |    204731 |   22336    79859 |    9008    6623   211594    31.9 | 14.370 % |
c |    204957 |   22336    79859 |    9909    6849   218810    31.9 | 14.370 % |
c ==============================================================================
c [1mFound solution: 1839[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 16221   bits: 15/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    205103 |   22338    79888 |    7446    6995   225886    32.3 | 14.370 % |
c |    205203 |   22338    79888 |    8190    7095   227499    32.1 | 14.410 % |
c |    205356 |   22305    79775 |    9009    7243   230489    31.8 | 14.504 % |
c |    205581 |   22291    79730 |    9910    7462   238824    32.0 | 14.621 % |
c |    205918 |   22291    79730 |   10901    7799   249392    32.0 | 14.621 % |
c |    206427 |   22291    79730 |   11991    8308   272762    32.8 | 14.621 % |
c |    207188 |   22291    79730 |   13191    9069   343572    37.9 | 14.621 % |
c |    208327 |   22273    79667 |   14510   10200   409544    40.2 | 14.738 % |
c |    210035 |   22273    79667 |   15961   11908   494835    41.6 | 14.738 % |
c ==============================================================================
c [1mFound solution: 1807[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 16253   bits: 15/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    211815 |   22272    79707 |    7424   13684   599413    43.8 | 14.738 % |
c |    211915 |   22272    79707 |    8166    6942   232707    33.5 | 14.851 % |
c |    212069 |   22272    79707 |    8983    7096   238589    33.6 | 14.851 % |
c |    212295 |   22272    79707 |    9881    7322   244509    33.4 | 14.851 % |
c |    212634 |   22272    79707 |   10869    7661   261324    34.1 | 14.851 % |
c |    213140 |   22272    79707 |   11956    8167   271843    33.3 | 14.851 % |
c |    213899 |   22272    79707 |   13152    8926   316962    35.5 | 14.851 % |
c |    215039 |   22265    79686 |   14467   10065   379924    37.7 | 14.898 % |
c |    216748 |   22265    79686 |   15914   11774   465233    39.5 | 14.898 % |
c ==============================================================================
c [1mFound solution: 1795[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 16265   bits: 15/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    217386 |   22274    79741 |    7424   12412   509376    41.0 | 14.898 % |
c |    217486 |   22274    79741 |    8166    6306   208979    33.1 | 14.951 % |
c |    217637 |   22223    79558 |    8983    6454   212523    32.9 | 15.021 % |
c |    217862 |   22223    79558 |    9881    6679   218730    32.7 | 15.021 % |
c |    218200 |   22223    79558 |   10869    7017   231130    32.9 | 15.021 % |
c |    218707 |   22223    79558 |   11956    7524   261194    34.7 | 15.021 % |
c |    219468 |   22223    79558 |   13152    8285   290670    35.1 | 15.021 % |
c |    220607 |   22223    79558 |   14467    9424   356613    37.8 | 15.021 % |
c |    222318 |   22214    79527 |   15914   11130   430256    38.7 | 15.044 % |
c |    224880 |   22214    79527 |   17505   13692   567691    41.5 | 15.044 % |
c ==============================================================================
c [1mFound solution: 1673[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 16387   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    228322 |   22154    79147 |    7384   16605   771132    46.4 | 15.044 % |
c |    228422 |   22154    79147 |    8122    4252   180612    42.5 | 15.341 % |
c |    228572 |   22154    79147 |    8934    4402   185321    42.1 | 15.341 % |
c |    228800 |   22154    79147 |    9828    4630   197947    42.8 | 15.341 % |
c |    229137 |   22154    79147 |   10810    4967   216890    43.7 | 15.341 % |
c |    229643 |   22154    79147 |   11892    5473   231508    42.3 | 15.341 % |
c |    230402 |   22154    79147 |   13081    6232   283614    45.5 | 15.341 % |
c |    231541 |   22154    79147 |   14389    7371   323674    43.9 | 15.341 % |
c |    233251 |   22154    79147 |   15828    9081   437575    48.2 | 15.341 % |
c |    235813 |   22154    79147 |   17411   11643   585810    50.3 | 15.341 % |
c |    239658 |   22154    79147 |   19152   15488   782256    50.5 | 15.341 % |
c |    245427 |   22154    79147 |   21067   11005   431921    39.2 | 15.341 % |
c |    254078 |   22154    79147 |   23174   19656   956421    48.7 | 15.341 % |
c |    267052 |   22154    79147 |   25491   20439   937291    45.9 | 15.341 % |
c |    286513 |   22145    79116 |   28040   26532  1264208    47.6 | 15.365 % |
c |    315705 |   22138    79095 |   30844   25821  1753069    67.9 | 15.412 % |
c |    359494 |   22138    79095 |   33929   17339  1247412    71.9 | 15.412 % |
c |    425178 |   22138    79095 |   37322   25229  1550626    61.5 | 15.412 % |
c |    523705 |   22138    79095 |   41054   37624  2029182    53.9 | 15.412 % |
c |    671495 |   22122    79040 |   45159   36035  2342488    65.0 | 15.505 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.97 0.90 2/54 24269
Raw data (stat): 24269 (runsolver) R 24268 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 429586722 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 1366 0 0 0 996 2 0 0 25 0 1 0 429586722 7217152 1343 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1762 1343 603 41 0 1721 0
vsize: 7048
[startup+20.0017 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 1677 0 0 0 1994 4 0 0 25 0 1 0 429586722 8761344 1654 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2139 1654 603 41 0 2098 0
vsize: 8556
[startup+30.0012 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 1977 0 0 0 2992 5 0 0 25 0 1 0 429586722 9969664 1954 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2434 1954 603 41 0 2393 0
vsize: 9736
[startup+40.0011 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 2150 0 0 0 3992 6 0 0 25 0 1 0 429586722 10641408 2127 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2598 2127 603 41 0 2557 0
vsize: 10392
[startup+50.0012 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 2356 0 0 0 4991 7 0 0 25 0 1 0 429586722 11448320 2333 4294967295 134512640 134672761 3221224576 3221223680 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2795 2333 603 41 0 2754 0
vsize: 11180
[startup+60.0017 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 2714 0 0 0 5990 8 0 0 25 0 1 0 429586722 12922880 2691 4294967295 134512640 134672761 3221224576 3221223680 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3155 2691 603 41 0 3114 0
vsize: 12620
[startup+70.002 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 2714 0 0 0 6990 8 0 0 25 0 1 0 429586722 12922880 2691 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3155 2691 603 41 0 3114 0
vsize: 12620
[startup+80.0018 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 2714 0 0 0 7990 8 0 0 25 0 1 0 429586722 12922880 2691 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3155 2691 603 41 0 3114 0
vsize: 12620
[startup+90.0023 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 2718 0 0 0 8990 8 0 0 25 0 1 0 429586722 12922880 2695 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3155 2695 603 41 0 3114 0
vsize: 12620
[startup+100.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 2718 0 0 0 9990 8 0 0 25 0 1 0 429586722 12922880 2695 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3155 2695 603 41 0 3114 0
vsize: 12620
[startup+110.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3025 0 0 0 10990 9 0 0 25 0 1 0 429586722 14131200 3002 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3450 3002 603 41 0 3409 0
vsize: 13800
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3434 0 0 0 11989 10 0 0 25 0 1 0 429586722 16003072 3411 4294967295 134512640 134672761 3221224576 3221223776 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3907 3411 603 41 0 3866 0
vsize: 15628
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3434 0 0 0 12989 10 0 0 25 0 1 0 429586722 16003072 3411 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3907 3411 603 41 0 3866 0
vsize: 15628
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3434 0 0 0 13989 10 0 0 25 0 1 0 429586722 16003072 3411 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3907 3411 603 41 0 3866 0
vsize: 15628
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3434 0 0 0 14989 10 0 0 25 0 1 0 429586722 16003072 3411 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3907 3411 603 41 0 3866 0
vsize: 15628
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3434 0 0 0 15990 10 0 0 25 0 1 0 429586722 16003072 3411 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3907 3411 603 41 0 3866 0
vsize: 15628
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3434 0 0 0 16990 10 0 0 25 0 1 0 429586722 16003072 3411 4294967295 134512640 134672761 3221224576 3221223760 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3907 3411 603 41 0 3866 0
vsize: 15628
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3434 0 0 0 17989 11 0 0 25 0 1 0 429586722 16003072 3411 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3907 3411 603 41 0 3866 0
vsize: 15628
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3434 0 0 0 18989 11 0 0 25 0 1 0 429586722 16003072 3411 4294967295 134512640 134672761 3221224576 3221223296 134565768 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3907 3411 603 41 0 3866 0
vsize: 15628
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3434 0 0 0 19988 11 0 0 25 0 1 0 429586722 16003072 3411 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3907 3411 603 41 0 3866 0
vsize: 15628
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3434 0 0 0 20989 11 0 0 25 0 1 0 429586722 16003072 3411 4294967295 134512640 134672761 3221224576 3221223744 134561156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3907 3411 603 41 0 3866 0
vsize: 15628
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3444 0 0 0 21989 11 0 0 25 0 1 0 429586722 16003072 3421 4294967295 134512640 134672761 3221224576 3221223760 134558930 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3907 3421 603 41 0 3866 0
vsize: 15628
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3449 0 0 0 22989 11 0 0 25 0 1 0 429586722 16003072 3426 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3907 3426 603 41 0 3866 0
vsize: 15628
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3589 0 0 0 23989 11 0 0 25 0 1 0 429586722 16535552 3566 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4037 3566 603 41 0 3996 0
vsize: 16148
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3609 0 0 0 24989 11 0 0 25 0 1 0 429586722 16732160 3586 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4085 3586 603 41 0 4044 0
vsize: 16340
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3609 0 0 0 25989 11 0 0 25 0 1 0 429586722 16732160 3586 4294967295 134512640 134672761 3221224576 3221223680 134554629 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4085 3586 603 41 0 4044 0
vsize: 16340
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3609 0 0 0 26989 11 0 0 25 0 1 0 429586722 16732160 3586 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4085 3586 603 41 0 4044 0
vsize: 16340
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3609 0 0 0 27989 11 0 0 25 0 1 0 429586722 16732160 3586 4294967295 134512640 134672761 3221224576 3221223756 134559056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4085 3586 603 41 0 4044 0
vsize: 16340
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3609 0 0 0 28990 11 0 0 25 0 1 0 429586722 16732160 3586 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4085 3586 603 41 0 4044 0
vsize: 16340
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3609 0 0 0 29990 11 0 0 25 0 1 0 429586722 16732160 3586 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4085 3586 603 41 0 4044 0
vsize: 16340
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3609 0 0 0 30990 11 0 0 25 0 1 0 429586722 16732160 3586 4294967295 134512640 134672761 3221224576 3221223680 134555211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4085 3586 603 41 0 4044 0
vsize: 16340
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3609 0 0 0 31990 11 0 0 25 0 1 0 429586722 16732160 3586 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4085 3586 603 41 0 4044 0
vsize: 16340
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3609 0 0 0 32990 12 0 0 25 0 1 0 429586722 16732160 3586 4294967295 134512640 134672761 3221224576 3221223744 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4085 3586 603 41 0 4044 0
vsize: 16340
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3609 0 0 0 33990 12 0 0 25 0 1 0 429586722 16732160 3586 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4085 3586 603 41 0 4044 0
vsize: 16340
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3609 0 0 0 34991 12 0 0 25 0 1 0 429586722 16732160 3586 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4085 3586 603 41 0 4044 0
vsize: 16340
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3653 0 0 0 35991 12 0 0 25 0 1 0 429586722 16863232 3630 4294967295 134512640 134672761 3221224576 3221223680 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4117 3630 603 41 0 4076 0
vsize: 16468
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3662 0 0 0 36991 12 0 0 25 0 1 0 429586722 16863232 3639 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4117 3639 603 41 0 4076 0
vsize: 16468
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3662 0 0 0 37991 12 0 0 25 0 1 0 429586722 16863232 3639 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4117 3639 603 41 0 4076 0
vsize: 16468
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3818 0 0 0 38991 12 0 0 25 0 1 0 429586722 17530880 3795 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4280 3795 603 41 0 4239 0
vsize: 17120
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3818 0 0 0 39991 12 0 0 25 0 1 0 429586722 17530880 3795 4294967295 134512640 134672761 3221224576 3221223680 134559941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4280 3795 603 41 0 4239 0
vsize: 17120
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3818 0 0 0 40991 12 0 0 25 0 1 0 429586722 17530880 3795 4294967295 134512640 134672761 3221224576 3221223744 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4280 3795 603 41 0 4239 0
vsize: 17120
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3818 0 0 0 41991 12 0 0 25 0 1 0 429586722 17530880 3795 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4280 3795 603 41 0 4239 0
vsize: 17120
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3818 0 0 0 42991 12 0 0 25 0 1 0 429586722 17530880 3795 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4280 3795 603 41 0 4239 0
vsize: 17120
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3819 0 0 0 43992 12 0 0 25 0 1 0 429586722 17530880 3796 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4280 3796 603 41 0 4239 0
vsize: 17120
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3819 0 0 0 44992 12 0 0 25 0 1 0 429586722 17530880 3796 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4280 3796 603 41 0 4239 0
vsize: 17120
[startup+460.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 3988 0 0 0 45991 13 0 0 25 0 1 0 429586722 18198528 3965 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4443 3965 603 41 0 4402 0
vsize: 17772
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4302 0 0 0 46990 15 0 0 25 0 1 0 429586722 19542016 4279 4294967295 134512640 134672761 3221224576 3221223760 134559538 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4771 4279 603 41 0 4730 0
vsize: 19084
[startup+480.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4302 0 0 0 47990 15 0 0 25 0 1 0 429586722 19542016 4279 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4771 4279 603 41 0 4730 0
vsize: 19084
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4307 0 0 0 48990 15 0 0 25 0 1 0 429586722 19542016 4284 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4771 4284 603 41 0 4730 0
vsize: 19084
[startup+500.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4314 0 0 0 49990 15 0 0 25 0 1 0 429586722 19542016 4291 4294967295 134512640 134672761 3221224576 3221223760 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4771 4291 603 41 0 4730 0
vsize: 19084
[startup+510.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4329 0 0 0 50990 15 0 0 25 0 1 0 429586722 19701760 4306 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4810 4306 603 41 0 4769 0
vsize: 19240
[startup+520.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4333 0 0 0 51990 15 0 0 25 0 1 0 429586722 19701760 4310 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4810 4310 603 41 0 4769 0
vsize: 19240
[startup+530.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4335 0 0 0 52991 15 0 0 25 0 1 0 429586722 19701760 4312 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4810 4312 603 41 0 4769 0
vsize: 19240
[startup+540.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4336 0 0 0 53991 15 0 0 25 0 1 0 429586722 19701760 4313 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4810 4313 603 41 0 4769 0
vsize: 19240
[startup+550.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4434 0 0 0 54991 15 0 0 25 0 1 0 429586722 20099072 4411 4294967295 134512640 134672761 3221224576 3221223680 134554948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4907 4411 603 41 0 4866 0
vsize: 19628
[startup+560.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4434 0 0 0 55991 15 0 0 25 0 1 0 429586722 20099072 4411 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4907 4411 603 41 0 4866 0
vsize: 19628
[startup+570.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4434 0 0 0 56991 15 0 0 25 0 1 0 429586722 20099072 4411 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4907 4411 603 41 0 4866 0
vsize: 19628
[startup+580.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4436 0 0 0 57991 15 0 0 25 0 1 0 429586722 20099072 4413 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4907 4413 603 41 0 4866 0
vsize: 19628
[startup+590.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4436 0 0 0 58992 15 0 0 25 0 1 0 429586722 20099072 4413 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4907 4413 603 41 0 4866 0
vsize: 19628
[startup+600.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4436 0 0 0 59992 15 0 0 25 0 1 0 429586722 20099072 4413 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4907 4413 603 41 0 4866 0
vsize: 19628
[startup+610.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4436 0 0 0 60992 15 0 0 25 0 1 0 429586722 20099072 4413 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4907 4413 603 41 0 4866 0
vsize: 19628
[startup+620.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4436 0 0 0 61992 15 0 0 25 0 1 0 429586722 20099072 4413 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4907 4413 603 41 0 4866 0
vsize: 19628
[startup+630.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4436 0 0 0 62992 15 0 0 25 0 1 0 429586722 20099072 4413 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4907 4413 603 41 0 4866 0
vsize: 19628
[startup+640.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4436 0 0 0 63993 15 0 0 25 0 1 0 429586722 20099072 4413 4294967295 134512640 134672761 3221224576 3221223680 134560399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4907 4413 603 41 0 4866 0
vsize: 19628
[startup+650.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4436 0 0 0 64993 15 0 0 25 0 1 0 429586722 20099072 4413 4294967295 134512640 134672761 3221224576 3221223776 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4907 4413 603 41 0 4866 0
vsize: 19628
[startup+660.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4436 0 0 0 65993 15 0 0 25 0 1 0 429586722 20099072 4413 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4907 4413 603 41 0 4866 0
vsize: 19628
[startup+670.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4436 0 0 0 66993 15 0 0 25 0 1 0 429586722 20099072 4413 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4907 4413 603 41 0 4866 0
vsize: 19628
[startup+680.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4436 0 0 0 67993 15 0 0 25 0 1 0 429586722 20099072 4413 4294967295 134512640 134672761 3221224576 3221223720 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4907 4413 603 41 0 4866 0
vsize: 19628
[startup+690.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4444 0 0 0 68994 15 0 0 25 0 1 0 429586722 20099072 4421 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4907 4421 603 41 0 4866 0
vsize: 19628
[startup+700.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4444 0 0 0 69994 15 0 0 25 0 1 0 429586722 20099072 4421 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4907 4421 603 41 0 4866 0
vsize: 19628
[startup+710.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4444 0 0 0 70994 15 0 0 25 0 1 0 429586722 20099072 4421 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4907 4421 603 41 0 4866 0
vsize: 19628
[startup+720.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4444 0 0 0 71994 15 0 0 25 0 1 0 429586722 20099072 4421 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4907 4421 603 41 0 4866 0
vsize: 19628
[startup+730.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4447 0 0 0 72994 15 0 0 25 0 1 0 429586722 20099072 4424 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4907 4424 603 41 0 4866 0
vsize: 19628
[startup+740.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4449 0 0 0 73994 15 0 0 25 0 1 0 429586722 20099072 4426 4294967295 134512640 134672761 3221224576 3221223728 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4907 4426 603 41 0 4866 0
vsize: 19628
[startup+750.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4453 0 0 0 74994 15 0 0 25 0 1 0 429586722 20099072 4430 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4907 4430 603 41 0 4866 0
vsize: 19628
[startup+760.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4462 0 0 0 75994 15 0 0 25 0 1 0 429586722 20099072 4439 4294967295 134512640 134672761 3221224576 3221223680 134560269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4907 4439 603 41 0 4866 0
vsize: 19628
[startup+770.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4465 0 0 0 76994 15 0 0 25 0 1 0 429586722 20242432 4442 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4942 4442 603 41 0 4901 0
vsize: 19768
[startup+780.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4479 0 0 0 77995 16 0 0 25 0 1 0 429586722 20242432 4456 4294967295 134512640 134672761 3221224576 3221223760 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4942 4456 603 41 0 4901 0
vsize: 19768
[startup+790.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4479 0 0 0 78995 16 0 0 25 0 1 0 429586722 20242432 4456 4294967295 134512640 134672761 3221224576 3221223744 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4942 4456 603 41 0 4901 0
vsize: 19768
[startup+800.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4479 0 0 0 79995 16 0 0 25 0 1 0 429586722 20242432 4456 4294967295 134512640 134672761 3221224576 3221223680 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4942 4456 603 41 0 4901 0
vsize: 19768
[startup+810.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4489 0 0 0 80995 16 0 0 25 0 1 0 429586722 20242432 4466 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4942 4466 603 41 0 4901 0
vsize: 19768
[startup+820.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4489 0 0 0 81995 16 0 0 25 0 1 0 429586722 20242432 4466 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4942 4466 603 41 0 4901 0
vsize: 19768
[startup+830.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4512 0 0 0 82995 16 0 0 25 0 1 0 429586722 20377600 4489 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4975 4489 603 41 0 4934 0
vsize: 19900
[startup+840.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4519 0 0 0 83995 16 0 0 25 0 1 0 429586722 20377600 4496 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4975 4496 603 41 0 4934 0
vsize: 19900
[startup+850.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4526 0 0 0 84995 16 0 0 25 0 1 0 429586722 20377600 4503 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4975 4503 603 41 0 4934 0
vsize: 19900
[startup+860.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4532 0 0 0 85996 16 0 0 25 0 1 0 429586722 20520960 4509 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5010 4509 603 41 0 4969 0
vsize: 20040
[startup+870.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4703 0 0 0 86995 16 0 0 25 0 1 0 429586722 21184512 4680 4294967295 134512640 134672761 3221224576 3221223680 134554656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5172 4680 603 41 0 5131 0
vsize: 20688
[startup+880.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4703 0 0 0 87996 16 0 0 25 0 1 0 429586722 21184512 4680 4294967295 134512640 134672761 3221224576 3221223760 134559041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5172 4680 603 41 0 5131 0
vsize: 20688
[startup+890.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4703 0 0 0 88996 16 0 0 25 0 1 0 429586722 21184512 4680 4294967295 134512640 134672761 3221224576 3221223744 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5172 4680 603 41 0 5131 0
vsize: 20688
[startup+900.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4711 0 0 0 89996 16 0 0 25 0 1 0 429586722 21184512 4688 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5172 4688 603 41 0 5131 0
vsize: 20688
[startup+910.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4712 0 0 0 90996 17 0 0 25 0 1 0 429586722 21184512 4689 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5172 4689 603 41 0 5131 0
vsize: 20688
[startup+920.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4942 0 0 0 91996 17 0 0 25 0 1 0 429586722 22122496 4919 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5401 4919 603 41 0 5360 0
vsize: 21604
[startup+930.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4942 0 0 0 92996 17 0 0 25 0 1 0 429586722 22122496 4919 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5401 4919 603 41 0 5360 0
vsize: 21604
[startup+940.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4947 0 0 0 93996 17 0 0 25 0 1 0 429586722 22278144 4924 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5439 4924 603 41 0 5398 0
vsize: 21756
[startup+950.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4955 0 0 0 94996 17 0 0 25 0 1 0 429586722 22278144 4932 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5439 4932 603 41 0 5398 0
vsize: 21756
[startup+960.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 4970 0 0 0 95996 17 0 0 25 0 1 0 429586722 22278144 4947 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5439 4947 603 41 0 5398 0
vsize: 21756
[startup+970.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 5222 0 0 0 96996 18 0 0 25 0 1 0 429586722 23359488 5199 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5703 5199 603 41 0 5662 0
vsize: 22812
[startup+980.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 5222 0 0 0 97996 18 0 0 25 0 1 0 429586722 23359488 5199 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5703 5199 603 41 0 5662 0
vsize: 22812
[startup+990.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 5223 0 0 0 98996 18 0 0 25 0 1 0 429586722 23359488 5200 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5703 5200 603 41 0 5662 0
vsize: 22812
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 5223 0 0 0 99996 18 0 0 25 0 1 0 429586722 23359488 5200 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5703 5200 603 41 0 5662 0
vsize: 22812
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 5223 0 0 0 100996 18 0 0 25 0 1 0 429586722 23359488 5200 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5703 5200 603 41 0 5662 0
vsize: 22812
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 5280 0 0 0 101996 18 0 0 25 0 1 0 429586722 23629824 5257 4294967295 134512640 134672761 3221224576 3221223680 134554671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5769 5257 603 41 0 5728 0
vsize: 23076
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 5280 0 0 0 102996 18 0 0 25 0 1 0 429586722 23629824 5257 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5769 5257 603 41 0 5728 0
vsize: 23076
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 5280 0 0 0 103996 18 0 0 25 0 1 0 429586722 23629824 5257 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5769 5257 603 41 0 5728 0
vsize: 23076
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 5281 0 0 0 104996 18 0 0 25 0 1 0 429586722 23629824 5258 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5769 5258 603 41 0 5728 0
vsize: 23076
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 5291 0 0 0 105997 18 0 0 25 0 1 0 429586722 23629824 5268 4294967295 134512640 134672761 3221224576 3221223668 1075346528 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5769 5268 603 41 0 5728 0
vsize: 23076
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 5297 0 0 0 106997 18 0 0 25 0 1 0 429586722 23629824 5274 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5769 5274 603 41 0 5728 0
vsize: 23076
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 5695 0 0 0 107996 20 0 0 25 0 1 0 429586722 25235456 5672 4294967295 134512640 134672761 3221224576 3221223532 1075350060 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6161 5672 603 41 0 6120 0
vsize: 24644
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 5754 0 0 0 108996 20 0 0 25 0 1 0 429586722 25501696 5731 4294967295 134512640 134672761 3221224576 3221223680 134560248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6226 5731 603 41 0 6185 0
vsize: 24904
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 5754 0 0 0 109996 20 0 0 25 0 1 0 429586722 25501696 5731 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6226 5731 603 41 0 6185 0
vsize: 24904
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 5754 0 0 0 110996 20 0 0 25 0 1 0 429586722 25501696 5731 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6226 5731 603 41 0 6185 0
vsize: 24904
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 5754 0 0 0 111996 20 0 0 25 0 1 0 429586722 25501696 5731 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6226 5731 603 41 0 6185 0
vsize: 24904
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 6017 0 0 0 112996 21 0 0 25 0 1 0 429586722 26578944 5994 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6489 5994 603 41 0 6448 0
vsize: 25956
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 6345 0 0 0 113995 21 0 0 25 0 1 0 429586722 27930624 6322 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6819 6322 603 41 0 6778 0
vsize: 27276
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 6426 0 0 0 114995 21 0 0 25 0 1 0 429586722 28340224 6403 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6919 6403 603 41 0 6878 0
vsize: 27676
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 6426 0 0 0 115995 21 0 0 25 0 1 0 429586722 28340224 6403 4294967295 134512640 134672761 3221224576 3221223744 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6919 6403 603 41 0 6878 0
vsize: 27676
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 6426 0 0 0 116996 21 0 0 25 0 1 0 429586722 28340224 6403 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6919 6403 603 41 0 6878 0
vsize: 27676
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 6426 0 0 0 117996 21 0 0 25 0 1 0 429586722 28340224 6403 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6919 6403 603 41 0 6878 0
vsize: 27676
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 6426 0 0 0 118996 21 0 0 25 0 1 0 429586722 28340224 6403 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6919 6403 603 41 0 6878 0
vsize: 27676
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24269
Raw data (stat): 24269 (minisat+) R 24268 10720 10719 0 -1 0 6426 0 0 0 119996 21 0 0 25 0 1 0 429586722 28340224 6403 4294967295 134512640 134672761 3221224576 3221223680 134554636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6919 6403 603 41 0 6878 0
vsize: 27676
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 24269
Raw data (stat): 24269 (minisat+) Z 24268 10720 10719 0 -1 12 6429 0 0 0 119996 23 0 0 25 0 1 0 429586722 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.2
CPU user time (s): 1199.97
CPU system time (s): 0.232964
CPU usage (%): 100.012
Max. virtual memory (Kb): 27676
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####