PB'05 competition: run trace

Some explanations

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

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        802740 kB
Buffers:         23336 kB
Cached:         188216 kB
SwapCached:        744 kB
Active:          67400 kB
Inactive:       146088 kB
HighTotal:      131008 kB
HighFree:        36960 kB
LowTotal:       903652 kB
LowFree:        765780 kB
SwapTotal:     2097892 kB
SwapFree:      2096220 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           4992 kB
Slab:            12668 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 13:51:24 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 18587 7 1200.21 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.65 0.86 0.87 2/54 6996
Raw data (stat): 6996 (runsolver) R 6995 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545469219 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.70 0.86 0.87 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 1325 0 0 0 996 3 0 0 25 0 1 0 545469219 7213056 1302 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1761 1302 603 41 0 1720 0
vsize: 7044
[startup+20.0006 s]
Raw data (loadavg): 0.75 0.87 0.87 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 2135 0 0 0 1992 6 0 0 25 0 1 0 545469219 10432512 2112 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2547 2112 603 41 0 2506 0
vsize: 10188
[startup+30.0008 s]
Raw data (loadavg): 0.79 0.87 0.88 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 2389 0 0 0 2991 8 0 0 25 0 1 0 545469219 11530240 2366 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2815 2366 603 41 0 2774 0
vsize: 11260
[startup+40.0008 s]
Raw data (loadavg): 0.82 0.87 0.88 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 2413 0 0 0 3991 8 0 0 25 0 1 0 545469219 11665408 2390 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2848 2390 603 41 0 2807 0
vsize: 11392
[startup+50.0015 s]
Raw data (loadavg): 0.85 0.88 0.88 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 2494 0 0 0 4991 8 0 0 25 0 1 0 545469219 11931648 2471 4294967295 134512640 134672761 3221224544 3221223648 134560196 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.0016 s]
Raw data (loadavg): 0.87 0.88 0.88 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 2627 0 0 0 5990 9 0 0 25 0 1 0 545469219 12603392 2604 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3077 2604 603 41 0 3036 0
vsize: 12308
[startup+70.0017 s]
Raw data (loadavg): 0.89 0.89 0.88 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 2832 0 0 0 6989 11 0 0 25 0 1 0 545469219 13402112 2809 4294967295 134512640 134672761 3221224544 3221223712 134561229 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.0023 s]
Raw data (loadavg): 0.91 0.89 0.88 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 3118 0 0 0 7987 12 0 0 25 0 1 0 545469219 14479360 3095 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3535 3095 603 41 0 3494 0
vsize: 14140
[startup+90.0014 s]
Raw data (loadavg): 0.92 0.89 0.88 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 3619 0 0 0 8985 15 0 0 25 0 1 0 545469219 16621568 3596 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.002 s]
Raw data (loadavg): 0.93 0.89 0.88 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 3619 0 0 0 9985 15 0 0 25 0 1 0 545469219 16621568 3596 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4058 3596 603 41 0 4017 0
vsize: 16232
[startup+110.003 s]
Raw data (loadavg): 0.94 0.90 0.88 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 3742 0 0 0 10984 16 0 0 25 0 1 0 545469219 17018880 3719 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.003 s]
Raw data (loadavg): 0.95 0.90 0.88 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 3742 0 0 0 11984 16 0 0 25 0 1 0 545469219 17018880 3719 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4155 3719 603 41 0 4114 0
vsize: 16620
[startup+130.003 s]
Raw data (loadavg): 0.96 0.90 0.89 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 3742 0 0 0 12985 16 0 0 25 0 1 0 545469219 17018880 3719 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4155 3719 603 41 0 4114 0
vsize: 16620
[startup+140.003 s]
Raw data (loadavg): 0.96 0.91 0.89 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 3742 0 0 0 13985 16 0 0 25 0 1 0 545469219 17018880 3719 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4155 3719 603 41 0 4114 0
vsize: 16620
[startup+150.003 s]
Raw data (loadavg): 0.97 0.91 0.89 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 3744 0 0 0 14985 16 0 0 25 0 1 0 545469219 17018880 3721 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4155 3721 603 41 0 4114 0
vsize: 16620
[startup+160.003 s]
Raw data (loadavg): 0.97 0.91 0.89 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 3744 0 0 0 15985 16 0 0 25 0 1 0 545469219 17018880 3721 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4155 3721 603 41 0 4114 0
vsize: 16620
[startup+170.002 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 3744 0 0 0 16985 16 0 0 25 0 1 0 545469219 17018880 3721 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4155 3721 603 41 0 4114 0
vsize: 16620
[startup+180.003 s]
Raw data (loadavg): 0.98 0.92 0.89 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 3745 0 0 0 17985 16 0 0 25 0 1 0 545469219 17018880 3722 4294967295 134512640 134672761 3221224544 3221223712 134561121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4155 3722 603 41 0 4114 0
vsize: 16620
[startup+190.003 s]
Raw data (loadavg): 0.98 0.92 0.89 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 3745 0 0 0 18985 16 0 0 25 0 1 0 545469219 17018880 3722 4294967295 134512640 134672761 3221224544 3221223648 134560237 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4155 3722 603 41 0 4114 0
vsize: 16620
[startup+200.003 s]
Raw data (loadavg): 0.98 0.92 0.89 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 3745 0 0 0 19985 16 0 0 25 0 1 0 545469219 17018880 3722 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4155 3722 603 41 0 4114 0
vsize: 16620
[startup+210.003 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 3745 0 0 0 20986 16 0 0 25 0 1 0 545469219 17018880 3722 4294967295 134512640 134672761 3221224544 3221223696 134560074 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4155 3722 603 41 0 4114 0
vsize: 16620
[startup+220.002 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 3745 0 0 0 21986 16 0 0 25 0 1 0 545469219 17018880 3722 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4155 3722 603 41 0 4114 0
vsize: 16620
[startup+230.003 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 3745 0 0 0 22986 16 0 0 25 0 1 0 545469219 17018880 3722 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4155 3722 603 41 0 4114 0
vsize: 16620
[startup+240.002 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 3745 0 0 0 23986 16 0 0 25 0 1 0 545469219 17018880 3722 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4155 3722 603 41 0 4114 0
vsize: 16620
[startup+250.003 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 3745 0 0 0 24986 16 0 0 25 0 1 0 545469219 17018880 3722 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4155 3722 603 41 0 4114 0
vsize: 16620
[startup+260.004 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 3745 0 0 0 25987 16 0 0 25 0 1 0 545469219 17018880 3722 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4155 3722 603 41 0 4114 0
vsize: 16620
[startup+270.003 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 3787 0 0 0 26987 16 0 0 25 0 1 0 545469219 17285120 3764 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4220 3764 603 41 0 4179 0
vsize: 16880
[startup+280.003 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 3798 0 0 0 27987 16 0 0 25 0 1 0 545469219 17285120 3775 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4220 3775 603 41 0 4179 0
vsize: 16880
[startup+290.003 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 3835 0 0 0 28987 16 0 0 25 0 1 0 545469219 17575936 3812 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4291 3812 603 41 0 4250 0
vsize: 17164
[startup+300.003 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 4166 0 0 0 29986 18 0 0 25 0 1 0 545469219 18911232 4143 4294967295 134512640 134672761 3221224544 3221223728 134558667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4617 4143 603 41 0 4576 0
vsize: 18468
[startup+310.003 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 4244 0 0 0 30986 18 0 0 25 0 1 0 545469219 19177472 4221 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4682 4221 603 41 0 4641 0
vsize: 18728
[startup+320.002 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 4257 0 0 0 31986 18 0 0 25 0 1 0 545469219 19312640 4234 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4715 4234 603 41 0 4674 0
vsize: 18860
[startup+330.003 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 4286 0 0 0 32986 18 0 0 25 0 1 0 545469219 19460096 4263 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4751 4263 603 41 0 4710 0
vsize: 19004
[startup+340.002 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 4320 0 0 0 33986 18 0 0 25 0 1 0 545469219 19603456 4297 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4786 4297 603 41 0 4745 0
vsize: 19144
[startup+350.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 4344 0 0 0 34986 18 0 0 25 0 1 0 545469219 19750912 4321 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4822 4321 603 41 0 4781 0
vsize: 19288
[startup+360.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 4511 0 0 0 35986 18 0 0 25 0 1 0 545469219 20418560 4488 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4985 4488 603 41 0 4944 0
vsize: 19940
[startup+370.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 4511 0 0 0 36986 18 0 0 25 0 1 0 545469219 20418560 4488 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4985 4488 603 41 0 4944 0
vsize: 19940
[startup+380.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 4514 0 0 0 37986 18 0 0 25 0 1 0 545469219 20418560 4491 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4985 4491 603 41 0 4944 0
vsize: 19940
[startup+390.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 4526 0 0 0 38986 18 0 0 25 0 1 0 545469219 20418560 4503 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4985 4503 603 41 0 4944 0
vsize: 19940
[startup+400.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 4808 0 0 0 39986 19 0 0 25 0 1 0 545469219 21618688 4785 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5278 4785 603 41 0 5237 0
vsize: 21112
[startup+410.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 4808 0 0 0 40986 19 0 0 25 0 1 0 545469219 21618688 4785 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5278 4785 603 41 0 5237 0
vsize: 21112
[startup+420.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 4816 0 0 0 41986 19 0 0 25 0 1 0 545469219 21618688 4793 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5278 4793 603 41 0 5237 0
vsize: 21112
[startup+430.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 5263 0 0 0 42985 21 0 0 25 0 1 0 545469219 23470080 5240 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5730 5240 603 41 0 5689 0
vsize: 22920
[startup+440.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 5328 0 0 0 43985 21 0 0 25 0 1 0 545469219 23736320 5305 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5795 5305 603 41 0 5754 0
vsize: 23180
[startup+450.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 5328 0 0 0 44985 21 0 0 25 0 1 0 545469219 23736320 5305 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5795 5305 603 41 0 5754 0
vsize: 23180
[startup+460.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 5328 0 0 0 45985 21 0 0 25 0 1 0 545469219 23736320 5305 4294967295 134512640 134672761 3221224544 3221223680 134560667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5795 5305 603 41 0 5754 0
vsize: 23180
[startup+470.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 5328 0 0 0 46985 21 0 0 25 0 1 0 545469219 23736320 5305 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5795 5305 603 41 0 5754 0
vsize: 23180
[startup+480.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 5513 0 0 0 47984 22 0 0 25 0 1 0 545469219 24657920 5490 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6020 5490 603 41 0 5979 0
vsize: 24080
[startup+490.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 5513 0 0 0 48985 22 0 0 25 0 1 0 545469219 24657920 5490 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6020 5490 603 41 0 5979 0
vsize: 24080
[startup+500.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 5513 0 0 0 49985 22 0 0 25 0 1 0 545469219 24657920 5490 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6020 5490 603 41 0 5979 0
vsize: 24080
[startup+510.004 s]
Raw data (loadavg): 1.07 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 5513 0 0 0 50985 22 0 0 25 0 1 0 545469219 24657920 5490 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6020 5490 603 41 0 5979 0
vsize: 24080
[startup+520.003 s]
Raw data (loadavg): 1.06 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 5513 0 0 0 51985 22 0 0 25 0 1 0 545469219 24657920 5490 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6020 5490 603 41 0 5979 0
vsize: 24080
[startup+530.004 s]
Raw data (loadavg): 1.05 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 5513 0 0 0 52985 22 0 0 25 0 1 0 545469219 24657920 5490 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6020 5490 603 41 0 5979 0
vsize: 24080
[startup+540.003 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 5514 0 0 0 53985 22 0 0 25 0 1 0 545469219 24657920 5491 4294967295 134512640 134672761 3221224544 3221223648 134560326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6020 5491 603 41 0 5979 0
vsize: 24080
[startup+550.003 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 5515 0 0 0 54986 22 0 0 25 0 1 0 545469219 24657920 5492 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6020 5492 603 41 0 5979 0
vsize: 24080
[startup+560.003 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 5516 0 0 0 55986 22 0 0 25 0 1 0 545469219 24657920 5493 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6020 5493 603 41 0 5979 0
vsize: 24080
[startup+570.002 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 5516 0 0 0 56986 22 0 0 25 0 1 0 545469219 24657920 5493 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6020 5493 603 41 0 5979 0
vsize: 24080
[startup+580.002 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 5517 0 0 0 57986 22 0 0 25 0 1 0 545469219 24657920 5494 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6020 5494 603 41 0 5979 0
vsize: 24080
[startup+590.001 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 5517 0 0 0 58986 22 0 0 25 0 1 0 545469219 24657920 5494 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6020 5494 603 41 0 5979 0
vsize: 24080
[startup+600.002 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 5742 0 0 0 59985 23 0 0 25 0 1 0 545469219 25600000 5719 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6250 5719 603 41 0 6209 0
vsize: 25000
[startup+610.002 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 5742 0 0 0 60985 23 0 0 25 0 1 0 545469219 25600000 5719 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6250 5719 603 41 0 6209 0
vsize: 25000
[startup+620.001 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 5742 0 0 0 61985 23 0 0 25 0 1 0 545469219 25600000 5719 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6250 5719 603 41 0 6209 0
vsize: 25000
[startup+630.001 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 5742 0 0 0 62985 23 0 0 25 0 1 0 545469219 25600000 5719 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6250 5719 603 41 0 6209 0
vsize: 25000
[startup+640 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 5991 0 0 0 63984 24 0 0 25 0 1 0 545469219 26533888 5968 4294967295 134512640 134672761 3221224544 3221223728 134558768 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6478 5968 603 41 0 6437 0
vsize: 25912
[startup+650.001 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6284 0 0 0 64984 25 0 0 25 0 1 0 545469219 27729920 6261 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6770 6261 603 41 0 6729 0
vsize: 27080
[startup+660.001 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6284 0 0 0 65984 25 0 0 25 0 1 0 545469219 27729920 6261 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6770 6261 603 41 0 6729 0
vsize: 27080
[startup+670.001 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6284 0 0 0 66984 25 0 0 25 0 1 0 545469219 27729920 6261 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6770 6261 603 41 0 6729 0
vsize: 27080
[startup+680.001 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6284 0 0 0 67984 25 0 0 25 0 1 0 545469219 27729920 6261 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6770 6261 603 41 0 6729 0
vsize: 27080
[startup+690 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6284 0 0 0 68984 25 0 0 25 0 1 0 545469219 27729920 6261 4294967295 134512640 134672761 3221224544 3221223680 134560654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6770 6261 603 41 0 6729 0
vsize: 27080
[startup+700.001 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6392 0 0 0 69984 26 0 0 25 0 1 0 545469219 28139520 6369 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6870 6369 603 41 0 6829 0
vsize: 27480
[startup+710.001 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6392 0 0 0 70984 26 0 0 25 0 1 0 545469219 28139520 6369 4294967295 134512640 134672761 3221224544 3221223648 134560201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6870 6369 603 41 0 6829 0
vsize: 27480
[startup+720 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6392 0 0 0 71984 26 0 0 25 0 1 0 545469219 28139520 6369 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6870 6369 603 41 0 6829 0
vsize: 27480
[startup+730.001 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6392 0 0 0 72985 26 0 0 25 0 1 0 545469219 28139520 6369 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6870 6369 603 41 0 6829 0
vsize: 27480
[startup+740 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6392 0 0 0 73985 26 0 0 25 0 1 0 545469219 28139520 6369 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6870 6369 603 41 0 6829 0
vsize: 27480
[startup+750.001 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6392 0 0 0 74985 26 0 0 25 0 1 0 545469219 28139520 6369 4294967295 134512640 134672761 3221224544 3221223648 134554656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6870 6369 603 41 0 6829 0
vsize: 27480
[startup+760.001 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6392 0 0 0 75985 26 0 0 25 0 1 0 545469219 28139520 6369 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6870 6369 603 41 0 6829 0
vsize: 27480
[startup+770 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6392 0 0 0 76985 26 0 0 25 0 1 0 545469219 28139520 6369 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6870 6369 603 41 0 6829 0
vsize: 27480
[startup+780 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6392 0 0 0 77986 26 0 0 25 0 1 0 545469219 28139520 6369 4294967295 134512640 134672761 3221224544 3221223712 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6870 6369 603 41 0 6829 0
vsize: 27480
[startup+790 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6392 0 0 0 78986 26 0 0 25 0 1 0 545469219 28139520 6369 4294967295 134512640 134672761 3221224544 3221223648 134560226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6870 6369 603 41 0 6829 0
vsize: 27480
[startup+800 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6392 0 0 0 79986 26 0 0 25 0 1 0 545469219 28139520 6369 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6870 6369 603 41 0 6829 0
vsize: 27480
[startup+810 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6392 0 0 0 80986 26 0 0 25 0 1 0 545469219 28139520 6369 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6870 6369 603 41 0 6829 0
vsize: 27480
[startup+819.999 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6392 0 0 0 81986 26 0 0 25 0 1 0 545469219 28139520 6369 4294967295 134512640 134672761 3221224544 3221223680 134560716 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6870 6369 603 41 0 6829 0
vsize: 27480
[startup+829.999 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6392 0 0 0 82986 26 0 0 25 0 1 0 545469219 28139520 6369 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6870 6369 603 41 0 6829 0
vsize: 27480
[startup+839.999 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6393 0 0 0 83987 26 0 0 25 0 1 0 545469219 28139520 6370 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6870 6370 603 41 0 6829 0
vsize: 27480
[startup+850 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6394 0 0 0 84987 26 0 0 25 0 1 0 545469219 28139520 6371 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6870 6371 603 41 0 6829 0
vsize: 27480
[startup+860 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6394 0 0 0 85986 26 0 0 25 0 1 0 545469219 28139520 6371 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6870 6371 603 41 0 6829 0
vsize: 27480
[startup+869.999 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6396 0 0 0 86986 26 0 0 25 0 1 0 545469219 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+880 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6396 0 0 0 87986 26 0 0 25 0 1 0 545469219 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 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6396 0 0 0 88986 27 0 0 25 0 1 0 545469219 28139520 6373 4294967295 134512640 134672761 3221224544 3221223712 134560983 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 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6396 0 0 0 89986 27 0 0 25 0 1 0 545469219 28139520 6373 4294967295 134512640 134672761 3221224544 3221223712 134560954 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 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6396 0 0 0 90986 27 0 0 25 0 1 0 545469219 28139520 6373 4294967295 134512640 134672761 3221224544 3221223648 134555116 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 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6396 0 0 0 91986 27 0 0 25 0 1 0 545469219 28139520 6373 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.001 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6396 0 0 0 92986 28 0 0 25 0 1 0 545469219 28139520 6373 4294967295 134512640 134672761 3221224544 3221223712 134560906 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.001 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6437 0 0 0 93986 28 0 0 25 0 1 0 545469219 28409856 6414 4294967295 134512640 134672761 3221224544 3221223744 134557842 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.001 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6437 0 0 0 94985 28 0 0 25 0 1 0 545469219 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+960.001 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6443 0 0 0 95985 29 0 0 25 0 1 0 545469219 28409856 6420 4294967295 134512640 134672761 3221224544 3221223712 134561014 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.001 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6453 0 0 0 96985 29 0 0 25 0 1 0 545469219 28409856 6430 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6936 6430 603 41 0 6895 0
vsize: 27744
[startup+980.001 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6477 0 0 0 97985 30 0 0 25 0 1 0 545469219 28545024 6454 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6969 6454 603 41 0 6928 0
vsize: 27876
[startup+990.002 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6483 0 0 0 98984 31 0 0 25 0 1 0 545469219 28545024 6460 4294967295 134512640 134672761 3221224544 3221223712 134560876 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 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6500 0 0 0 99984 31 0 0 25 0 1 0 545469219 28692480 6477 4294967295 134512640 134672761 3221224544 3221223680 134560706 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 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6500 0 0 0 100984 31 0 0 25 0 1 0 545469219 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+1020 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6500 0 0 0 101983 32 0 0 25 0 1 0 545469219 28692480 6477 4294967295 134512640 134672761 3221224544 3221223712 134560898 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 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6500 0 0 0 102983 32 0 0 25 0 1 0 545469219 28692480 6477 4294967295 134512640 134672761 3221224544 3221223712 134560852 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 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6500 0 0 0 103983 32 0 0 25 0 1 0 545469219 28692480 6477 4294967295 134512640 134672761 3221224544 3221223712 134560917 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 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6501 0 0 0 104983 33 0 0 25 0 1 0 545469219 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+1060 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6501 0 0 0 105983 33 0 0 25 0 1 0 545469219 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 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6501 0 0 0 106982 33 0 0 25 0 1 0 545469219 28692480 6478 4294967295 134512640 134672761 3221224544 3221223712 134560956 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 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6501 0 0 0 107982 34 0 0 25 0 1 0 545469219 28692480 6478 4294967295 134512640 134672761 3221224544 3221223648 134560289 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.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6501 0 0 0 108982 34 0 0 25 0 1 0 545469219 28692480 6478 4294967295 134512640 134672761 3221224544 3221223648 134560405 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.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6502 0 0 0 109982 34 0 0 25 0 1 0 545469219 28692480 6479 4294967295 134512640 134672761 3221224544 3221223648 134560196 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.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6530 0 0 0 110982 35 0 0 25 0 1 0 545469219 28827648 6507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7038 6507 603 41 0 6997 0
vsize: 28152
[startup+1120 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6846 0 0 0 111980 36 0 0 25 0 1 0 545469219 30048256 6823 4294967295 134512640 134672761 3221224544 3221223680 134560640 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.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6846 0 0 0 112980 37 0 0 25 0 1 0 545469219 30048256 6823 4294967295 134512640 134672761 3221224544 3221223712 134560983 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 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6849 0 0 0 113980 37 0 0 25 0 1 0 545469219 30048256 6826 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6853 0 0 0 114980 37 0 0 25 0 1 0 545469219 30048256 6830 4294967295 134512640 134672761 3221224544 3221223712 134561193 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.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6860 0 0 0 115980 37 0 0 25 0 1 0 545469219 30195712 6837 4294967295 134512640 134672761 3221224544 3221223728 134558645 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.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6860 0 0 0 116980 37 0 0 25 0 1 0 545469219 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.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6906 0 0 0 117980 37 0 0 25 0 1 0 545469219 30330880 6883 4294967295 134512640 134672761 3221224544 3221223696 134561035 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.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6906 0 0 0 118980 38 0 0 25 0 1 0 545469219 30330880 6883 4294967295 134512640 134672761 3221224544 3221223712 134560903 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.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 28099 28098 0 -1 0 6906 0 0 0 119980 38 0 0 25 0 1 0 545469219 30330880 6883 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.02 s]
Raw data (loadavg): 1.00 0.98 0.91 1/54 6996
Raw data (stat): 6996 (minisat+) Z 6995 28099 28098 0 -1 12 6909 0 0 0 119980 39 0 0 25 0 1 0 545469219 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.02
CPU time (s): 1200.21
CPU user time (s): 1199.81
CPU system time (s): 0.398939
CPU usage (%): 100.015
Max. virtual memory (Kb): 29620
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####