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 19127

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-04-21 18:01:16 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17014 boxname=wulflinc5 idbench=1309 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  9cc94d1db4d494288ef67a8d5ad5d77e  /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-misc07.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-misc07.opb /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-misc07.opb
IDLAUNCH: 17014
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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.007
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:        637420 kB
Buffers:         11408 kB
Cached:         365008 kB
SwapCached:        304 kB
Active:          54824 kB
Inactive:       324032 kB
HighTotal:      131008 kB
HighFree:         2380 kB
LowTotal:       903652 kB
LowFree:        635040 kB
SwapTotal:     2097136 kB
SwapFree:      2096444 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           5728 kB
Slab:            12952 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 18:21:18 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 17014 7 1200.2 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]---> Adder-cost: 30   maxlim: 26   bits: 5/5
c ---[ 241]---> Adder-cost: 32   maxlim: 26   bits: 5/5
c ---[ 239]---> Adder-cost: 30   maxlim: 26   bits: 5/5
c ---[ 237]---> Adder-cost: 32   maxlim: 26   bits: 5/5
c ---[ 235]---> Adder-cost: 34   maxlim: 26   bits: 5/5
c ---[ 233]---> Adder-cost: 32   maxlim: 26   bits: 5/5
c ---[ 231]---> Adder-cost: 32   maxlim: 26   bits: 5/5
c ---[ 230]---> Adder-cost: 114   maxlim: 59   bits: 6/6
c ---[ 229]---> Adder-cost: 114   maxlim: 59   bits: 6/6
c ---[ 228]---> Adder-cost: 114   maxlim: 59   bits: 6/6
c ---[  99]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[  97]---> Adder-cost: 26   maxlim: 8   bits: 5/4
c ---[  95]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[  93]---> Adder-cost: 28   maxlim: 8   bits: 5/4
c ---[  91]---> Adder-cost: 28   maxlim: 8   bits: 5/4
c ---[  89]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[  87]---> Adder-cost: 26   maxlim: 8   bits: 5/4
c ---[  85]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[  83]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[  81]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[  79]---> Adder-cost: 26   maxlim: 8   bits: 5/4
c ---[  77]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[  75]---> Adder-cost: 28   maxlim: 8   bits: 5/4
c ---[  73]---> Adder-cost: 28   maxlim: 8   bits: 5/4
c ---[  71]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[  69]---> Adder-cost: 26   maxlim: 8   bits: 5/4
c ---[  67]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[  65]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[  63]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[  61]---> Adder-cost: 26   maxlim: 8   bits: 5/4
c ---[  59]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[  57]---> Adder-cost: 28   maxlim: 8   bits: 5/4
c ---[  55]---> Adder-cost: 28   maxlim: 8   bits: 5/4
c ---[  53]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[  51]---> Adder-cost: 26   maxlim: 8   bits: 5/4
c ---[  49]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[  47]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[  46]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[  45]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[  44]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[  43]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[  42]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[  41]---> Adder-cost: 24   maxlim: 16   bits: 5/5
c ---[  40]---> Adder-cost: 24   maxlim: 16   bits: 5/5
c ---[  39]---> Adder-cost: 24   maxlim: 16   bits: 5/5
c ---[  38]---> Adder-cost: 24   maxlim: 16   bits: 5/5
c ---[  37]---> Adder-cost: 24   maxlim: 16   bits: 5/5
c ---[  36]---> Adder-cost: 24   maxlim: 16   bits: 5/5
c ---[  35]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[  34]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[  33]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[  32]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[  31]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[  30]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[  29]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[  28]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[  27]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[  26]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[  25]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[  24]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[  23]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[  22]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[  21]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[  20]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[  19]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[  18]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[  17]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[  16]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[  15]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[  14]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[  13]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[  12]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[  11]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[  10]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[   9]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[   8]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[   7]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[   6]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[   5]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[   4]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[   3]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[   2]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[   1]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[   0]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   23690    90323 |    7896       0        0     nan |  0.000 % |
c |       100 |   23690    90323 |    8685     100      415     4.2 | 16.778 % |
c |       250 |   23564    89891 |    9554     242     1281     5.3 | 16.985 % |
c |       475 |   23531    89780 |   10509     462     2960     6.4 | 17.124 % |
c |       814 |   23365    89202 |   11560     785     6479     8.3 | 17.677 % |
c |      1323 |   23054    88157 |   12716    1267    12285     9.7 | 18.760 % |
c |      2083 |   22463    86082 |   13988    1977    27191    13.8 | 20.166 % |
c ==============================================================================
c [1mFound solution: 1604608[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 27   maxlim: 3847   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2923 |   22120    84908 |    7373    2756    45642    16.6 | 20.166 % |
c |      3024 |   21911    84175 |    8110    2847    47329    16.6 | 22.421 % |
c |      3174 |   21911    84175 |    8921    2997    53494    17.8 | 22.421 % |
c |      3400 |   21816    83844 |    9813    3203    60017    18.7 | 22.809 % |
c |      3738 |   21452    82586 |   10794    3513    81053    23.1 | 23.862 % |
c |      4244 |   21020    81082 |   11874    3994   100703    25.2 | 25.235 % |
c ==============================================================================
c [1mFound solution: 1599488[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 19   maxlim: 3887   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4381 |   21119    81432 |    7039    4131   111560    27.0 | 25.235 % |
c |      4482 |   21045    81176 |    7742    4225   112735    26.7 | 25.409 % |
c |      4632 |   20888    80621 |    8517    4371   122482    28.0 | 25.910 % |
c |      4857 |   20591    79584 |    9368    4584   128679    28.1 | 26.843 % |
c |      5195 |   20591    79584 |   10305    4922   154872    31.5 | 26.843 % |
c |      5702 |   20383    78876 |   11336    5407   179816    33.3 | 27.662 % |
c ==============================================================================
c [1mFound solution: 1595648[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 27   maxlim: 3917   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5944 |   20533    79420 |    6844    5649   201225    35.6 | 27.662 % |
c |      6045 |   20533    79420 |    7528    5750   202801    35.3 | 27.624 % |
c |      6195 |   20533    79420 |    8281    5900   212086    35.9 | 27.624 % |
c |      6424 |   20533    79420 |    9109    6129   224757    36.7 | 27.624 % |
c |      6763 |   20533    79420 |   10020    6468   238649    36.9 | 27.624 % |
c ==============================================================================
c [1mFound solution: 1585408[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 19   maxlim: 3997   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6919 |   20651    79869 |    6883    6624   245822    37.1 | 27.624 % |
c ==============================================================================
c [1mFound solution: 1582848[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 21   maxlim: 4017   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6962 |   20731    80163 |    6910    6661   247504    37.2 | 27.624 % |
c |      7062 |   20731    80163 |    7601    6761   253239    37.5 | 27.757 % |
c ==============================================================================
c [1mFound solution: 1562368[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 24   maxlim: 4177   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7171 |   20819    80458 |    6939    6870   257143    37.4 | 27.757 % |
c |      7273 |   20819    80458 |    7632    6972   263100    37.7 | 27.673 % |
c |      7424 |   20819    80458 |    8396    7123   272341    38.2 | 27.673 % |
c |      7650 |   20819    80458 |    9235    7349   297545    40.5 | 27.673 % |
c ==============================================================================
c [1mFound solution: 1561728[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 26   maxlim: 4182   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7777 |   20932    80868 |    6977    7476   304640    40.7 | 27.673 % |
c |      7880 |   20932    80868 |    7674    7579   310812    41.0 | 27.610 % |
c |      8030 |   20932    80868 |    8442    7729   320526    41.5 | 27.610 % |
c ==============================================================================
c [1mFound solution: 1539968[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 24   maxlim: 4352   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8141 |   21010    81114 |    7003    7840   336201    42.9 | 27.610 % |
c |      8242 |   21010    81114 |    7703    7941   338684    42.7 | 27.513 % |
c ==============================================================================
c [1mFound solution: 1517568[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 18   maxlim: 4527   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8284 |   21093    81409 |    7031    7983   339978    42.6 | 27.513 % |
c |      8385 |   21093    81409 |    7734    8084   351195    43.4 | 27.484 % |
c |      8537 |   21093    81409 |    8507    8236   354990    43.1 | 27.484 % |
c |      8762 |   21086    81386 |    9358    8460   370069    43.7 | 27.506 % |
c |      9099 |   21086    81386 |   10294    8797   384385    43.7 | 27.506 % |
c ==============================================================================
c [1mFound solution: 1468928[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 22   maxlim: 4907   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9406 |   21189    81756 |    7063    9104   423486    46.5 | 27.506 % |
c |      9507 |   21189    81756 |    7769    4653   191812    41.2 | 27.469 % |
c |      9658 |   21173    81704 |    8546    4798   200234    41.7 | 27.534 % |
c |      9884 |   21173    81704 |    9400    5024   229503    45.7 | 27.534 % |
c |     10221 |   21173    81704 |   10340    5361   246622    46.0 | 27.534 % |
c |     10727 |   21158    81651 |   11375    5860   316141    53.9 | 27.556 % |
c |     11488 |   21158    81651 |   12512    6621   361496    54.6 | 27.556 % |
c |     12628 |   21113    81498 |   13763    7750   434281    56.0 | 27.685 % |
c |     14338 |   21113    81498 |   15140    9460   623542    65.9 | 27.685 % |
c |     16901 |   21113    81498 |   16654   12023   788673    65.6 | 27.685 % |
c |     20746 |   21113    81498 |   18319   15868  1194482    75.3 | 27.685 % |
c ==============================================================================
c [1mFound solution: 1456128[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 16   maxlim: 5007   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23761 |   21145    81619 |    7048   18872  1358153    72.0 | 27.685 % |
c |     23861 |   21145    81619 |    7752    4818   150859    31.3 | 27.840 % |
c |     24012 |   21145    81619 |    8528    4969   155342    31.3 | 27.840 % |
c |     24237 |   21129    81567 |    9380    5191   165849    31.9 | 27.904 % |
c |     24576 |   21129    81567 |   10318    5530   185640    33.6 | 27.904 % |
c |     25084 |   21122    81544 |   11350    6036   211203    35.0 | 27.926 % |
c ==============================================================================
c [1mFound solution: 1454848[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 20   maxlim: 5017   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25507 |   21230    81948 |    7076    6459   284842    44.1 | 27.926 % |
c |     25607 |   21230    81948 |    7783    6559   286055    43.6 | 27.914 % |
c |     25757 |   21230    81948 |    8561    6709   291492    43.4 | 27.914 % |
c |     25982 |   21230    81948 |    9418    6934   305975    44.1 | 27.914 % |
c |     26320 |   21215    81895 |   10359    7266   328543    45.2 | 27.936 % |
c |     26827 |   21215    81895 |   11395    7773   352905    45.4 | 27.936 % |
c |     27590 |   21215    81895 |   12535    8536   392398    46.0 | 27.936 % |
c |     28729 |   21206    81864 |   13789    9673   519811    53.7 | 27.957 % |
c |     30441 |   21206    81864 |   15168   11385   619598    54.4 | 27.957 % |
c |     33004 |   21164    81720 |   16684   13933   895538    64.3 | 28.064 % |
c |     36848 |   21164    81720 |   18353   17777  1299213    73.1 | 28.064 % |
c ==============================================================================
c [1mFound solution: 1438208[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 18   maxlim: 5147   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39387 |   21223    81930 |    7074   10319   566300    54.9 | 28.064 % |
c |     39487 |   21223    81930 |    7781    5260   134244    25.5 | 28.054 % |
c |     39637 |   21223    81930 |    8559    5410   150499    27.8 | 28.054 % |
c |     39862 |   21223    81930 |    9415    5635   160492    28.5 | 28.054 % |
c |     40200 |   21223    81930 |   10357    5973   202537    33.9 | 28.054 % |
c |     40706 |   21208    81879 |   11392    6474   227985    35.2 | 28.097 % |
c |     41466 |   21208    81879 |   12532    7234   265036    36.6 | 28.097 % |
c |     42606 |   21175    81764 |   13785    8364   394992    47.2 | 28.161 % |
c |     44314 |   21175    81764 |   15163   10072   503290    50.0 | 28.161 % |
c |     46876 |   21175    81764 |   16680   12634   832989    65.9 | 28.161 % |
c |     50721 |   21175    81764 |   18348   16479  1207125    73.3 | 28.161 % |
c |     56487 |   21160    81711 |   20182   11820   909314    76.9 | 28.182 % |
c |     65136 |   21112    81545 |   22201   20453  1923892    94.1 | 28.289 % |
c |     78110 |   21097    81492 |   24421   20735  2091567   100.9 | 28.310 % |
c |     97572 |   21064    81377 |   26863   13877   971997    70.0 | 28.374 % |
c ==============================================================================
c [1mFound solution: 1436928[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 22   maxlim: 5157   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    102544 |   21148    81673 |    7049   18846  1382009    73.3 | 28.374 % |
c |    102645 |   21148    81673 |    7753    4813   176580    36.7 | 28.339 % |
c |    102795 |   21148    81673 |    8529    4963   178362    35.9 | 28.339 % |
c |    103020 |   21148    81673 |    9382    5188   192852    37.2 | 28.339 % |
c |    103357 |   21148    81673 |   10320    5525   212777    38.5 | 28.339 % |
c |    103866 |   21106    81529 |   11352    6026   248615    41.3 | 28.466 % |
c ==============================================================================
c [1mFound solution: 1431808[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 20   maxlim: 5197   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    103959 |   21195    81854 |    7065    6119   255256    41.7 | 28.466 % |
c |    104059 |   21195    81854 |    7771    6219   265546    42.7 | 28.436 % |
c |    104211 |   21195    81854 |    8548    6371   282933    44.4 | 28.436 % |
c |    104436 |   21195    81854 |    9403    6596   307369    46.6 | 28.436 % |
c |    104776 |   21195    81854 |   10343    6936   359485    51.8 | 28.436 % |
c |    105282 |   21195    81854 |   11378    7442   410530    55.2 | 28.436 % |
c |    106042 |   21195    81854 |   12516    8202   447320    54.5 | 28.436 % |
c |    107182 |   21195    81854 |   13767    9342   575405    61.6 | 28.436 % |
c |    108891 |   21195    81854 |   15144   11051   779063    70.5 | 28.436 % |
c |    111453 |   21183    81812 |   16658   13610   913109    67.1 | 28.457 % |
c |    115297 |   21183    81812 |   18324   17454  1413066    81.0 | 28.457 % |
c ==============================================================================
c [1mFound solution: 1422208[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 20   maxlim: 5272   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    119445 |   21282    82174 |    7094   11610   869213    74.9 | 28.457 % |
c |    119548 |   21282    82174 |    7803    5908   284993    48.2 | 28.422 % |
c |    119698 |   21282    82174 |    8583    6058   298177    49.2 | 28.422 % |
c |    119924 |   21282    82174 |    9442    6284   315160    50.2 | 28.422 % |
c |    120262 |   21282    82174 |   10386    6622   345477    52.2 | 28.422 % |
c |    120769 |   21282    82174 |   11424    7129   424218    59.5 | 28.422 % |
c |    121528 |   21282    82174 |   12567    7888   465520    59.0 | 28.422 % |
c |    122669 |   21273    82143 |   13824    9026   531046    58.8 | 28.443 % |
c |    124377 |   21273    82143 |   15206   10734   790795    73.7 | 28.443 % |
c |    126940 |   21264    82112 |   16727   13294   901118    67.8 | 28.464 % |
c |    130784 |   21264    82112 |   18400   17138  1452791    84.8 | 28.464 % |
c |    136550 |   21236    82014 |   20240   12195  1115653    91.5 | 28.527 % |
c |    145200 |   21236    82014 |   22264   20845  1643841    78.9 | 28.527 % |
c |    158174 |   21215    81941 |   24490   21386  1594239    74.5 | 28.568 % |
c |    177635 |   21206    81910 |   26939   14267  1203685    84.4 | 28.589 % |
c |    206828 |   21206    81910 |   29633   28940  2519609    87.1 | 28.589 % |
c |    250619 |   21206    81910 |   32596   25338  2523060    99.6 | 28.589 % |
c |    316303 |   21188    81848 |   35856   20976  2175012   103.7 | 28.631 % |
c |    414831 |   21164    81766 |   39442   35660  3358500    94.2 | 28.694 % |
#### 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.95 0.97 0.96 2/54 26870
Raw data (stat): 26870 (runsolver) R 26869 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488857236 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0005 s]
Raw data (loadavg): 0.95 0.97 0.96 2/54 26870
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 1325 0 0 0 996 2 0 0 25 0 1 0 488857236 7213056 1302 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1761 1302 603 41 0 1720 0
vsize: 7044
[startup+20.0014 s]
Raw data (loadavg): 0.96 0.97 0.96 2/54 26870
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 2133 0 0 0 1993 4 0 0 25 0 1 0 488857236 10432512 2110 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2547 2110 603 41 0 2506 0
vsize: 10188
[startup+30.002 s]
Raw data (loadavg): 0.97 0.97 0.96 2/54 26870
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 2389 0 0 0 2992 6 0 0 25 0 1 0 488857236 11530240 2366 4294967295 134512640 134672761 3221224544 3221223600 134565116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2815 2366 603 41 0 2774 0
vsize: 11260
[startup+40.0019 s]
Raw data (loadavg): 0.97 0.97 0.96 2/54 26870
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 2416 0 0 0 3991 6 0 0 25 0 1 0 488857236 11665408 2393 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2848 2393 603 41 0 2807 0
vsize: 11392
[startup+50.0026 s]
Raw data (loadavg): 0.98 0.97 0.96 2/54 26870
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 2494 0 0 0 4991 6 0 0 25 0 1 0 488857236 11931648 2471 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2913 2471 603 41 0 2872 0
vsize: 11652
[startup+60.0021 s]
Raw data (loadavg): 0.98 0.97 0.96 2/54 26870
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 2629 0 0 0 5991 6 0 0 25 0 1 0 488857236 12603392 2606 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3077 2606 603 41 0 3036 0
vsize: 12308
[startup+70.0032 s]
Raw data (loadavg): 0.98 0.97 0.96 2/54 26870
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 2832 0 0 0 6991 7 0 0 25 0 1 0 488857236 13402112 2809 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3272 2809 603 41 0 3231 0
vsize: 13088
[startup+80.0039 s]
Raw data (loadavg): 0.98 0.97 0.96 2/54 26870
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 3121 0 0 0 7990 8 0 0 25 0 1 0 488857236 14614528 3098 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3568 3098 603 41 0 3527 0
vsize: 14272
[startup+90.0033 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26870
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 3619 0 0 0 8988 10 0 0 25 0 1 0 488857236 16621568 3596 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4058 3596 603 41 0 4017 0
vsize: 16232
[startup+100.004 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26870
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 3619 0 0 0 9988 10 0 0 25 0 1 0 488857236 16621568 3596 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4058 3596 603 41 0 4017 0
vsize: 16232
[startup+110.004 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26870
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 3742 0 0 0 10988 10 0 0 25 0 1 0 488857236 17018880 3719 4294967295 134512640 134672761 3221224544 3221223604 1075346557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4155 3719 603 41 0 4114 0
vsize: 16620
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26870
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 3742 0 0 0 11988 10 0 0 25 0 1 0 488857236 17018880 3719 4294967295 134512640 134672761 3221224544 3221223728 134558651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4155 3719 603 41 0 4114 0
vsize: 16620
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26870
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 3742 0 0 0 12988 10 0 0 25 0 1 0 488857236 17018880 3719 4294967295 134512640 134672761 3221224544 3221223648 134560287 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4155 3719 603 41 0 4114 0
vsize: 16620
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26870
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 3742 0 0 0 13988 10 0 0 25 0 1 0 488857236 17018880 3719 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4155 3719 603 41 0 4114 0
vsize: 16620
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26870
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 3744 0 0 0 14988 11 0 0 25 0 1 0 488857236 17018880 3721 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4155 3721 603 41 0 4114 0
vsize: 16620
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26870
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 3744 0 0 0 15988 11 0 0 25 0 1 0 488857236 17018880 3721 4294967295 134512640 134672761 3221224544 3221223648 134560231 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4155 3721 603 41 0 4114 0
vsize: 16620
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26870
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 3744 0 0 0 16989 11 0 0 25 0 1 0 488857236 17018880 3721 4294967295 134512640 134672761 3221224544 3221223668 134566031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4155 3721 603 41 0 4114 0
vsize: 16620
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26870
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 3745 0 0 0 17989 11 0 0 25 0 1 0 488857236 17018880 3722 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4155 3722 603 41 0 4114 0
vsize: 16620
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26870
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 3745 0 0 0 18989 11 0 0 25 0 1 0 488857236 17018880 3722 4294967295 134512640 134672761 3221224544 3221223648 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4155 3722 603 41 0 4114 0
vsize: 16620
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26870
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 3745 0 0 0 19989 11 0 0 25 0 1 0 488857236 17018880 3722 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4155 3722 603 41 0 4114 0
vsize: 16620
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26870
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 3745 0 0 0 20989 11 0 0 25 0 1 0 488857236 17018880 3722 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4155 3722 603 41 0 4114 0
vsize: 16620
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26870
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 3745 0 0 0 21989 11 0 0 25 0 1 0 488857236 17018880 3722 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4155 3722 603 41 0 4114 0
vsize: 16620
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26870
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 3745 0 0 0 22990 11 0 0 25 0 1 0 488857236 17018880 3722 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4155 3722 603 41 0 4114 0
vsize: 16620
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26870
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 3745 0 0 0 23990 11 0 0 25 0 1 0 488857236 17018880 3722 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4155 3722 603 41 0 4114 0
vsize: 16620
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26870
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 3745 0 0 0 24990 11 0 0 25 0 1 0 488857236 17018880 3722 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4155 3722 603 41 0 4114 0
vsize: 16620
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 3745 0 0 0 25990 11 0 0 25 0 1 0 488857236 17018880 3722 4294967295 134512640 134672761 3221224544 3221223648 134555105 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4155 3722 603 41 0 4114 0
vsize: 16620
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 3787 0 0 0 26990 11 0 0 25 0 1 0 488857236 17285120 3764 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4220 3764 603 41 0 4179 0
vsize: 16880
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 3793 0 0 0 27990 11 0 0 25 0 1 0 488857236 17285120 3770 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4220 3770 603 41 0 4179 0
vsize: 16880
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 3835 0 0 0 28990 11 0 0 25 0 1 0 488857236 17575936 3812 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4291 3812 603 41 0 4250 0
vsize: 17164
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 4093 0 0 0 29990 12 0 0 25 0 1 0 488857236 18509824 4070 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4519 4070 603 41 0 4478 0
vsize: 18076
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 4244 0 0 0 30990 12 0 0 25 0 1 0 488857236 19177472 4221 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4682 4221 603 41 0 4641 0
vsize: 18728
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 4250 0 0 0 31990 12 0 0 25 0 1 0 488857236 19177472 4227 4294967295 134512640 134672761 3221224544 3221223728 134558648 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4682 4227 603 41 0 4641 0
vsize: 18728
[startup+330.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 4280 0 0 0 32990 12 0 0 25 0 1 0 488857236 19312640 4257 4294967295 134512640 134672761 3221224544 3221223648 134560226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4715 4257 603 41 0 4674 0
vsize: 18860
[startup+340.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 4313 0 0 0 33990 12 0 0 25 0 1 0 488857236 19603456 4290 4294967295 134512640 134672761 3221224544 3221223728 134559556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4786 4290 603 41 0 4745 0
vsize: 19144
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 4344 0 0 0 34990 12 0 0 25 0 1 0 488857236 19750912 4321 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4822 4321 603 41 0 4781 0
vsize: 19288
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 4511 0 0 0 35990 13 0 0 25 0 1 0 488857236 20418560 4488 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4985 4488 603 41 0 4944 0
vsize: 19940
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 4511 0 0 0 36990 13 0 0 25 0 1 0 488857236 20418560 4488 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4985 4488 603 41 0 4944 0
vsize: 19940
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 4514 0 0 0 37990 13 0 0 25 0 1 0 488857236 20418560 4491 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4985 4491 603 41 0 4944 0
vsize: 19940
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 4523 0 0 0 38991 13 0 0 25 0 1 0 488857236 20418560 4500 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4985 4500 603 41 0 4944 0
vsize: 19940
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 4808 0 0 0 39990 14 0 0 25 0 1 0 488857236 21618688 4785 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5278 4785 603 41 0 5237 0
vsize: 21112
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 4808 0 0 0 40990 14 0 0 25 0 1 0 488857236 21618688 4785 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5278 4785 603 41 0 5237 0
vsize: 21112
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 4815 0 0 0 41990 14 0 0 25 0 1 0 488857236 21618688 4792 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5278 4792 603 41 0 5237 0
vsize: 21112
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 5167 0 0 0 42989 15 0 0 25 0 1 0 488857236 23068672 5144 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5632 5144 603 41 0 5591 0
vsize: 22528
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 5328 0 0 0 43988 16 0 0 25 0 1 0 488857236 23736320 5305 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5795 5305 603 41 0 5754 0
vsize: 23180
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 5328 0 0 0 44988 16 0 0 25 0 1 0 488857236 23736320 5305 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5795 5305 603 41 0 5754 0
vsize: 23180
[startup+460.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 5328 0 0 0 45989 16 0 0 25 0 1 0 488857236 23736320 5305 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5795 5305 603 41 0 5754 0
vsize: 23180
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 5328 0 0 0 46989 16 0 0 25 0 1 0 488857236 23736320 5305 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5795 5305 603 41 0 5754 0
vsize: 23180
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 5513 0 0 0 47988 17 0 0 25 0 1 0 488857236 24657920 5490 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6020 5490 603 41 0 5979 0
vsize: 24080
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 5513 0 0 0 48988 17 0 0 25 0 1 0 488857236 24657920 5490 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6020 5490 603 41 0 5979 0
vsize: 24080
[startup+500.014 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 5513 0 0 0 49989 17 0 0 25 0 1 0 488857236 24657920 5490 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6020 5490 603 41 0 5979 0
vsize: 24080
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 5513 0 0 0 50989 17 0 0 25 0 1 0 488857236 24657920 5490 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6020 5490 603 41 0 5979 0
vsize: 24080
[startup+520.015 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 5513 0 0 0 51989 17 0 0 25 0 1 0 488857236 24657920 5490 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6020 5490 603 41 0 5979 0
vsize: 24080
[startup+530.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 5513 0 0 0 52989 17 0 0 25 0 1 0 488857236 24657920 5490 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6020 5490 603 41 0 5979 0
vsize: 24080
[startup+540.015 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 5514 0 0 0 53989 17 0 0 25 0 1 0 488857236 24657920 5491 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6020 5491 603 41 0 5979 0
vsize: 24080
[startup+550.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 5515 0 0 0 54990 17 0 0 25 0 1 0 488857236 24657920 5492 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6020 5492 603 41 0 5979 0
vsize: 24080
[startup+560.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 5516 0 0 0 55990 17 0 0 25 0 1 0 488857236 24657920 5493 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6020 5493 603 41 0 5979 0
vsize: 24080
[startup+570.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 5516 0 0 0 56990 17 0 0 25 0 1 0 488857236 24657920 5493 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6020 5493 603 41 0 5979 0
vsize: 24080
[startup+580.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 5516 0 0 0 57990 17 0 0 25 0 1 0 488857236 24657920 5493 4294967295 134512640 134672761 3221224544 3221223712 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6020 5493 603 41 0 5979 0
vsize: 24080
[startup+590.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 5517 0 0 0 58990 17 0 0 25 0 1 0 488857236 24657920 5494 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6020 5494 603 41 0 5979 0
vsize: 24080
[startup+600.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 5742 0 0 0 59990 17 0 0 25 0 1 0 488857236 25600000 5719 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6250 5719 603 41 0 6209 0
vsize: 25000
[startup+610.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 5742 0 0 0 60990 17 0 0 25 0 1 0 488857236 25600000 5719 4294967295 134512640 134672761 3221224544 3221223604 1075346600 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6250 5719 603 41 0 6209 0
vsize: 25000
[startup+620.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 5742 0 0 0 61990 18 0 0 25 0 1 0 488857236 25600000 5719 4294967295 134512640 134672761 3221224544 3221223680 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6250 5719 603 41 0 6209 0
vsize: 25000
[startup+630.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 5742 0 0 0 62990 18 0 0 25 0 1 0 488857236 25600000 5719 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6250 5719 603 41 0 6209 0
vsize: 25000
[startup+640.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 5807 0 0 0 63990 18 0 0 25 0 1 0 488857236 25866240 5784 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6315 5784 603 41 0 6274 0
vsize: 25260
[startup+650.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6284 0 0 0 64989 19 0 0 25 0 1 0 488857236 27729920 6261 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6770 6261 603 41 0 6729 0
vsize: 27080
[startup+660.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6284 0 0 0 65989 19 0 0 25 0 1 0 488857236 27729920 6261 4294967295 134512640 134672761 3221224544 3221223648 134559853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6770 6261 603 41 0 6729 0
vsize: 27080
[startup+670.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6284 0 0 0 66990 19 0 0 25 0 1 0 488857236 27729920 6261 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6770 6261 603 41 0 6729 0
vsize: 27080
[startup+680.019 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6284 0 0 0 67990 19 0 0 25 0 1 0 488857236 27729920 6261 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6770 6261 603 41 0 6729 0
vsize: 27080
[startup+690.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6284 0 0 0 68990 19 0 0 25 0 1 0 488857236 27729920 6261 4294967295 134512640 134672761 3221224544 3221223728 134558883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6770 6261 603 41 0 6729 0
vsize: 27080
[startup+700.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6392 0 0 0 69990 19 0 0 25 0 1 0 488857236 28139520 6369 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6870 6369 603 41 0 6829 0
vsize: 27480
[startup+710.019 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6392 0 0 0 70990 19 0 0 25 0 1 0 488857236 28139520 6369 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6870 6369 603 41 0 6829 0
vsize: 27480
[startup+720.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6392 0 0 0 71991 19 0 0 25 0 1 0 488857236 28139520 6369 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6870 6369 603 41 0 6829 0
vsize: 27480
[startup+730.019 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6392 0 0 0 72991 19 0 0 25 0 1 0 488857236 28139520 6369 4294967295 134512640 134672761 3221224544 3221223648 134560248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6870 6369 603 41 0 6829 0
vsize: 27480
[startup+740.019 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6392 0 0 0 73991 19 0 0 25 0 1 0 488857236 28139520 6369 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6870 6369 603 41 0 6829 0
vsize: 27480
[startup+750.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6392 0 0 0 74991 19 0 0 25 0 1 0 488857236 28139520 6369 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6870 6369 603 41 0 6829 0
vsize: 27480
[startup+760.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6392 0 0 0 75991 19 0 0 25 0 1 0 488857236 28139520 6369 4294967295 134512640 134672761 3221224544 3221223680 134565048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6870 6369 603 41 0 6829 0
vsize: 27480
[startup+770.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6392 0 0 0 76991 19 0 0 25 0 1 0 488857236 28139520 6369 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6870 6369 603 41 0 6829 0
vsize: 27480
[startup+780.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6392 0 0 0 77992 19 0 0 25 0 1 0 488857236 28139520 6369 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6870 6369 603 41 0 6829 0
vsize: 27480
[startup+790.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6392 0 0 0 78992 19 0 0 25 0 1 0 488857236 28139520 6369 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6870 6369 603 41 0 6829 0
vsize: 27480
[startup+800.021 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6392 0 0 0 79992 19 0 0 25 0 1 0 488857236 28139520 6369 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6870 6369 603 41 0 6829 0
vsize: 27480
[startup+810.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6392 0 0 0 80992 19 0 0 25 0 1 0 488857236 28139520 6369 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6870 6369 603 41 0 6829 0
vsize: 27480
[startup+820.021 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6392 0 0 0 81992 19 0 0 25 0 1 0 488857236 28139520 6369 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6870 6369 603 41 0 6829 0
vsize: 27480
[startup+830.022 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6392 0 0 0 82993 19 0 0 25 0 1 0 488857236 28139520 6369 4294967295 134512640 134672761 3221224544 3221223648 134559760 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6870 6369 603 41 0 6829 0
vsize: 27480
[startup+840.022 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6392 0 0 0 83993 19 0 0 25 0 1 0 488857236 28139520 6369 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6870 6369 603 41 0 6829 0
vsize: 27480
[startup+850.023 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6393 0 0 0 84993 19 0 0 25 0 1 0 488857236 28139520 6370 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6870 6370 603 41 0 6829 0
vsize: 27480
[startup+860.024 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6394 0 0 0 85993 19 0 0 25 0 1 0 488857236 28139520 6371 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6870 6371 603 41 0 6829 0
vsize: 27480
[startup+870.024 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6396 0 0 0 86992 19 0 0 25 0 1 0 488857236 28139520 6373 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6870 6373 603 41 0 6829 0
vsize: 27480
[startup+880.024 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6396 0 0 0 87991 20 0 0 25 0 1 0 488857236 28139520 6373 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6870 6373 603 41 0 6829 0
vsize: 27480
[startup+890.023 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6396 0 0 0 88992 20 0 0 25 0 1 0 488857236 28139520 6373 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6870 6373 603 41 0 6829 0
vsize: 27480
[startup+900.024 s]
Raw data (loadavg): 1.07 0.99 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6396 0 0 0 89992 20 0 0 25 0 1 0 488857236 28139520 6373 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6870 6373 603 41 0 6829 0
vsize: 27480
[startup+910.024 s]
Raw data (loadavg): 1.06 0.99 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6396 0 0 0 90992 20 0 0 25 0 1 0 488857236 28139520 6373 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6870 6373 603 41 0 6829 0
vsize: 27480
[startup+920.025 s]
Raw data (loadavg): 1.05 0.99 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6396 0 0 0 91992 20 0 0 25 0 1 0 488857236 28139520 6373 4294967295 134512640 134672761 3221224544 3221223648 134555105 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6870 6373 603 41 0 6829 0
vsize: 27480
[startup+930.025 s]
Raw data (loadavg): 1.04 0.99 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6396 0 0 0 92992 20 0 0 25 0 1 0 488857236 28139520 6373 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6870 6373 603 41 0 6829 0
vsize: 27480
[startup+940.025 s]
Raw data (loadavg): 1.04 0.99 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6437 0 0 0 93993 20 0 0 25 0 1 0 488857236 28409856 6414 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6936 6414 603 41 0 6895 0
vsize: 27744
[startup+950.026 s]
Raw data (loadavg): 1.03 0.99 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6437 0 0 0 94993 20 0 0 25 0 1 0 488857236 28409856 6414 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6936 6414 603 41 0 6895 0
vsize: 27744
[startup+960.027 s]
Raw data (loadavg): 1.03 0.99 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6443 0 0 0 95993 20 0 0 25 0 1 0 488857236 28409856 6420 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6936 6420 603 41 0 6895 0
vsize: 27744
[startup+970.027 s]
Raw data (loadavg): 1.02 0.99 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6446 0 0 0 96993 20 0 0 25 0 1 0 488857236 28409856 6423 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6936 6423 603 41 0 6895 0
vsize: 27744
[startup+980.028 s]
Raw data (loadavg): 1.02 0.99 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6470 0 0 0 97994 20 0 0 25 0 1 0 488857236 28545024 6447 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6969 6447 603 41 0 6928 0
vsize: 27876
[startup+990.029 s]
Raw data (loadavg): 1.01 0.99 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6483 0 0 0 98994 20 0 0 25 0 1 0 488857236 28545024 6460 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6969 6460 603 41 0 6928 0
vsize: 27876
[startup+1000.03 s]
Raw data (loadavg): 1.01 0.99 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6500 0 0 0 99994 20 0 0 25 0 1 0 488857236 28692480 6477 4294967295 134512640 134672761 3221224544 3221223712 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7005 6477 603 41 0 6964 0
vsize: 28020
[startup+1010.03 s]
Raw data (loadavg): 1.01 0.99 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6500 0 0 0 100994 20 0 0 25 0 1 0 488857236 28692480 6477 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7005 6477 603 41 0 6964 0
vsize: 28020
[startup+1020.03 s]
Raw data (loadavg): 1.01 0.99 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6500 0 0 0 101994 20 0 0 25 0 1 0 488857236 28692480 6477 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7005 6477 603 41 0 6964 0
vsize: 28020
[startup+1030.03 s]
Raw data (loadavg): 1.01 0.99 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6500 0 0 0 102994 20 0 0 25 0 1 0 488857236 28692480 6477 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7005 6477 603 41 0 6964 0
vsize: 28020
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6500 0 0 0 103994 20 0 0 25 0 1 0 488857236 28692480 6477 4294967295 134512640 134672761 3221224544 3221223712 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7005 6477 603 41 0 6964 0
vsize: 28020
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6501 0 0 0 104995 20 0 0 25 0 1 0 488857236 28692480 6478 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7005 6478 603 41 0 6964 0
vsize: 28020
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6501 0 0 0 105995 20 0 0 25 0 1 0 488857236 28692480 6478 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7005 6478 603 41 0 6964 0
vsize: 28020
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6501 0 0 0 106995 20 0 0 25 0 1 0 488857236 28692480 6478 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7005 6478 603 41 0 6964 0
vsize: 28020
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6501 0 0 0 107995 20 0 0 25 0 1 0 488857236 28692480 6478 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7005 6478 603 41 0 6964 0
vsize: 28020
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6501 0 0 0 108996 20 0 0 25 0 1 0 488857236 28692480 6478 4294967295 134512640 134672761 3221224544 3221223648 134560477 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7005 6478 603 41 0 6964 0
vsize: 28020
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6502 0 0 0 109996 20 0 0 25 0 1 0 488857236 28692480 6479 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7005 6479 603 41 0 6964 0
vsize: 28020
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6516 0 0 0 110996 20 0 0 25 0 1 0 488857236 28692480 6493 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7005 6493 603 41 0 6964 0
vsize: 28020
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6846 0 0 0 111995 21 0 0 25 0 1 0 488857236 30048256 6823 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7336 6823 603 41 0 7295 0
vsize: 29344
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6846 0 0 0 112996 21 0 0 25 0 1 0 488857236 30048256 6823 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7336 6823 603 41 0 7295 0
vsize: 29344
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6849 0 0 0 113996 21 0 0 25 0 1 0 488857236 30048256 6826 4294967295 134512640 134672761 3221224544 3221223680 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7336 6826 603 41 0 7295 0
vsize: 29344
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6853 0 0 0 114996 21 0 0 25 0 1 0 488857236 30048256 6830 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7336 6830 603 41 0 7295 0
vsize: 29344
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6860 0 0 0 115996 21 0 0 25 0 1 0 488857236 30195712 6837 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7372 6837 603 41 0 7331 0
vsize: 29488
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6860 0 0 0 116996 21 0 0 25 0 1 0 488857236 30195712 6837 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7372 6837 603 41 0 7331 0
vsize: 29488
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6906 0 0 0 117996 21 0 0 25 0 1 0 488857236 30330880 6883 4294967295 134512640 134672761 3221224544 3221223648 134560260 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7405 6883 603 41 0 7364 0
vsize: 29620
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6906 0 0 0 118997 21 0 0 25 0 1 0 488857236 30330880 6883 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7405 6883 603 41 0 7364 0
vsize: 29620
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 26872
Raw data (stat): 26870 (minisat+) R 26869 24215 24214 0 -1 0 6906 0 0 0 119997 21 0 0 25 0 1 0 488857236 30330880 6883 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7405 6883 603 41 0 7364 0
vsize: 29620
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.96 1/54 26872
Raw data (stat): 26870 (minisat+) Z 26869 24215 24214 0 -1 12 6909 0 0 0 119997 22 0 0 25 0 1 0 488857236 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.229965
CPU usage (%): 100.013
Max. virtual memory (Kb): 29620
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####