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/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-neos5.opb
MD5SUM	4f5f6e30a602f3968daa9ca41c7da043
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2058
Optimality of the best value was proved	NO
Number of terms in the objective function	133
Biggest coefficient in the objective function	128
Number of bits for the biggest coefficient in the objective function	8
Sum of the numbers in the objective function	9334
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	1024
Number of bits of the biggest number in a constraint	11
Biggest sum of numbers in a constraint	9334
Number of bits of the biggest sum of numbers	14
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.05284
Number of variables	133
Total number of constraints	126
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	56
Number of constraints which are nor clauses,nor cardinality constraints	70
Minimum length of a constraint	1
Maximum length of a constraint	81
Trace number 14625

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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:        732664 kB
Buffers:         33200 kB
Cached:         245340 kB
SwapCached:         56 kB
Active:          13140 kB
Inactive:       268296 kB
HighTotal:      131008 kB
HighFree:        59612 kB
LowTotal:       903652 kB
LowFree:        673052 kB
SwapTotal:     2097136 kB
SwapFree:      2096992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6816 kB
Slab:            14652 kB
Committed_AS:    71672 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 00:45:46 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 19718 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 73 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[  72]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  71]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  70]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  69]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  68]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  67]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  66]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  65]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  64]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  63]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  62]---> Adder-cost: 59   maxlim: 7   bits: 4/3
c ---[  61]---> Adder-cost: 99   maxlim: 895   bits: 11/10
c ---[  60]---> Adder-cost: 45   maxlim: 895   bits: 11/10
c ---[  59]---> Adder-cost: 119   maxlim: 895   bits: 11/10
c ---[  58]---> Adder-cost: 113   maxlim: 895   bits: 11/10
c ---[  57]---> Adder-cost: 47   maxlim: 895   bits: 11/10
c ---[  56]---> Adder-cost: 113   maxlim: 895   bits: 11/10
c ---[  55]---> Adder-cost: 111   maxlim: 895   bits: 11/10
c ---[  54]---> Adder-cost: 115   maxlim: 895   bits: 11/10
c ---[  53]---> Adder-cost: 49   maxlim: 895   bits: 11/10
c ---[  52]---> Adder-cost: 119   maxlim: 895   bits: 11/10
c ---[  51]---> Adder-cost: 43   maxlim: 7   bits: 4/3
c ---[  50]---> Adder-cost: 111   maxlim: 895   bits: 11/10
c ---[  49]---> Adder-cost: 129   maxlim: 895   bits: 11/10
c ---[  48]---> Adder-cost: 63   maxlim: 767   bits: 11/10
c ---[  47]---> Adder-cost: 39   maxlim: 767   bits: 11/10
c ---[  46]---> Adder-cost: 39   maxlim: 767   bits: 11/10
c ---[  45]---> Adder-cost: 41   maxlim: 767   bits: 11/10
c ---[  44]---> Adder-cost: 39   maxlim: 767   bits: 11/10
c ---[  43]---> Adder-cost: 35   maxlim: 767   bits: 11/10
c ---[  42]---> Adder-cost: 37   maxlim: 767   bits: 11/10
c ---[  41]---> Adder-cost: 39   maxlim: 767   bits: 11/10
c ---[  40]---> Adder-cost: 39   maxlim: 1023   bits: 11/10
c ---[  39]---> Adder-cost: 39   maxlim: 767   bits: 11/10
c ---[  38]---> Adder-cost: 115   maxlim: 767   bits: 11/10
c ---[  37]---> Adder-cost: 39   maxlim: 767   bits: 11/10
c ---[  36]---> Adder-cost: 35   maxlim: 767   bits: 11/10
c ---[  35]---> Adder-cost: 37   maxlim: 767   bits: 11/10
c ---[  34]---> Adder-cost: 39   maxlim: 767   bits: 11/10
c ---[  33]---> Adder-cost: 39   maxlim: 767   bits: 11/10
c ---[  32]---> Adder-cost: 115   maxlim: 767   bits: 11/10
c ---[  31]---> Adder-cost: 47   maxlim: 767   bits: 11/10
c ---[  30]---> Adder-cost: 43   maxlim: 767   bits: 11/10
c ---[  29]---> Adder-cost: 33   maxlim: 1023   bits: 11/10
c ---[  28]---> Adder-cost: 105   maxlim: 767   bits: 11/10
c ---[  27]---> Adder-cost: 125   maxlim: 767   bits: 11/10
c ---[  26]---> Adder-cost: 33   maxlim: 639   bits: 11/10
c ---[  25]---> Adder-cost: 33   maxlim: 639   bits: 11/10
c ---[  24]---> Adder-cost: 33   maxlim: 639   bits: 11/10
c ---[  23]---> Adder-cost: 35   maxlim: 639   bits: 11/10
c ---[  22]---> Adder-cost: 35   maxlim: 639   bits: 11/10
c ---[  21]---> Adder-cost: 33   maxlim: 639   bits: 11/10
c ---[  20]---> Adder-cost: 33   maxlim: 639   bits: 11/10
c ---[  19]---> Adder-cost: 35   maxlim: 639   bits: 11/10
c ---[  18]---> Adder-cost: 33   maxlim: 1023   bits: 11/10
c ---[  17]---> Adder-cost: 35   maxlim: 639   bits: 11/10
c ---[  16]---> Adder-cost: 35   maxlim: 639   bits: 11/10
c ---[  15]---> Adder-cost: 33   maxlim: 639   bits: 11/10
c ---[  14]---> Adder-cost: 37   maxlim: 639   bits: 11/10
c ---[  13]---> Adder-cost: 41   maxlim: 639   bits: 11/10
c ---[  12]---> Adder-cost: 37   maxlim: 639   bits: 11/10
c ---[  11]---> Adder-cost: 99   maxlim: 639   bits: 11/10
c ---[  10]---> Adder-cost: 30   maxlim: 511   bits: 10/9
c ---[   9]---> Adder-cost: 30   maxlim: 511   bits: 10/9
c ---[   8]---> Adder-cost: 30   maxlim: 511   bits: 10/9
c ---[   7]---> Adder-cost: 33   maxlim: 1023   bits: 11/10
c ---[   6]---> Adder-cost: 30   maxlim: 511   bits: 10/9
c ---[   5]---> Adder-cost: 30   maxlim: 511   bits: 10/9
c ---[   4]---> Adder-cost: 34   maxlim: 511   bits: 10/9
c ---[   3]---> Adder-cost: 30   maxlim: 383   bits: 10/9
c ---[   2]---> Adder-cost: 39   maxlim: 6   bits: 4/3
c ---[   1]---> Adder-cost: 39   maxlim: 895   bits: 11/10
c ---[   0]---> Adder-cost: 33   maxlim: 895   bits: 11/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   20654    73549 |    6884       0        0     nan |  0.000 % |
c |       100 |   20654    73549 |    7572     100      462     4.6 |  5.563 % |
c |       250 |   20654    73549 |    8329     250     1641     6.6 |  5.563 % |
c ==============================================================================
c [1mFound solution: 2984[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 174   maxlim: 6350   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       376 |   21815    77700 |    7271     376     2304     6.1 |  5.563 % |
c |       477 |   21815    77700 |    7998     477     3277     6.9 |  5.507 % |
c ==============================================================================
c [1mFound solution: 2965[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 6369   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       603 |   21821    77740 |    7273     603     4878     8.1 |  5.507 % |
c |       703 |   21821    77740 |    8000     703     5325     7.6 |  5.557 % |
c |       855 |   21821    77740 |    8800     855     6810     8.0 |  5.557 % |
c ==============================================================================
c [1mFound solution: 2857[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 6477   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       967 |   21831    77807 |    7277     967     8014     8.3 |  5.557 % |
c ==============================================================================
c [1mFound solution: 2609[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 6725   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1018 |   21837    77855 |    7279    1018     8396     8.2 |  5.557 % |
c ==============================================================================
c [1mFound solution: 2534[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 6800   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1089 |   21844    77905 |    7281    1089     9038     8.3 |  5.557 % |
c ==============================================================================
c [1mFound solution: 2505[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 6829   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1141 |   21850    77958 |    7283    1141     9288     8.1 |  5.557 % |
c |      1241 |   21850    77958 |    8011    1241    10339     8.3 |  5.949 % |
c |      1391 |   21850    77958 |    8812    1391    11220     8.1 |  5.949 % |
c |      1617 |   21850    77958 |    9693    1617    13418     8.3 |  5.949 % |
c ==============================================================================
c [1mFound solution: 2497[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 6837   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1736 |   21854    77998 |    7284    1736    14187     8.2 |  5.949 % |
c |      1836 |   21854    77998 |    8012    1836    14889     8.1 |  6.022 % |
c |      1986 |   21854    77998 |    8813    1986    16124     8.1 |  6.022 % |
c ==============================================================================
c [1mFound solution: 2493[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 6841   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2148 |   21856    78024 |    7285    2148    18425     8.6 |  6.022 % |
c |      2248 |   21856    78024 |    8013    2248    19346     8.6 |  6.072 % |
c |      2398 |   21856    78024 |    8814    2398    21372     8.9 |  6.072 % |
c |      2624 |   21856    78024 |    9696    2624    23851     9.1 |  6.072 % |
c |      2962 |   21856    78024 |   10665    2962    28258     9.5 |  6.072 % |
c |      3469 |   21856    78024 |   11732    3469    34118     9.8 |  6.072 % |
c ==============================================================================
c [1mFound solution: 2487[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 6847   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3770 |   21858    78035 |    7286    3770    39583    10.5 |  6.072 % |
c |      3870 |   21858    78035 |    8014    3870    40936    10.6 |  6.095 % |
c |      4020 |   21858    78035 |    8816    4020    43131    10.7 |  6.095 % |
c |      4245 |   21858    78035 |    9697    4245    46244    10.9 |  6.095 % |
c ==============================================================================
c [1mFound solution: 2431[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 6903   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4364 |   21863    78072 |    7287    4364    47285    10.8 |  6.095 % |
c |      4465 |   21863    78072 |    8015    4465    48507    10.9 |  6.166 % |
c |      4616 |   21863    78072 |    8817    4616    50433    10.9 |  6.166 % |
c |      4843 |   21863    78072 |    9698    4843    54588    11.3 |  6.166 % |
c ==============================================================================
c [1mFound solution: 2377[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 6957   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5119 |   21871    78131 |    7290    5119    57182    11.2 |  6.166 % |
c |      5220 |   21871    78131 |    8019    5220    58003    11.1 |  6.285 % |
c |      5370 |   21871    78131 |    8820    5370    59609    11.1 |  6.285 % |
c |      5595 |   21871    78131 |    9702    5595    63625    11.4 |  6.285 % |
c |      5932 |   21871    78131 |   10673    5932    69789    11.8 |  6.285 % |
c |      6438 |   21871    78131 |   11740    6438    85351    13.3 |  6.285 % |
c |      7198 |   21871    78131 |   12914    7198    97441    13.5 |  6.285 % |
c |      8338 |   21871    78131 |   14206    8338   120296    14.4 |  6.285 % |
c |     10049 |   21871    78131 |   15626   10049   168443    16.8 |  6.285 % |
c |     12612 |   21871    78131 |   17189   12612   238616    18.9 |  6.285 % |
c |     16456 |   21871    78131 |   18908   16456   329721    20.0 |  6.285 % |
c |     22222 |   21871    78131 |   20799   12483   291200    23.3 |  6.285 % |
c ==============================================================================
c [1mFound solution: 2359[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 6975   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23345 |   21873    78142 |    7291   13606   313161    23.0 |  6.285 % |
c |     23446 |   21873    78142 |    8020    6904   141231    20.5 |  6.307 % |
c |     23596 |   21873    78142 |    8822    7054   142868    20.3 |  6.307 % |
c |     23821 |   21873    78142 |    9704    7279   146568    20.1 |  6.307 % |
c |     24159 |   21873    78142 |   10674    7617   153360    20.1 |  6.307 % |
c |     24669 |   21873    78142 |   11742    8127   163292    20.1 |  6.307 % |
c |     25428 |   21873    78142 |   12916    8886   182905    20.6 |  6.307 % |
c |     26568 |   21873    78142 |   14208   10026   197856    19.7 |  6.307 % |
c |     28277 |   21873    78142 |   15628   11735   241070    20.5 |  6.307 % |
c |     30840 |   21873    78142 |   17191   14298   293102    20.5 |  6.307 % |
c |     34687 |   21873    78142 |   18910    9369   187209    20.0 |  6.307 % |
c ==============================================================================
c [1mFound solution: 2354[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 6980   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35148 |   21876    78172 |    7292    9830   199356    20.3 |  6.307 % |
c |     35248 |   21876    78172 |    8021    5015   103272    20.6 |  6.355 % |
c ==============================================================================
c [1mFound solution: 2339[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 6995   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35328 |   21879    78198 |    7293    5095   104572    20.5 |  6.355 % |
c |     35428 |   21879    78198 |    8022    5195   105224    20.3 |  6.403 % |
c |     35578 |   21879    78198 |    8824    5345   107003    20.0 |  6.403 % |
c |     35804 |   21879    78198 |    9706    5571   112292    20.2 |  6.403 % |
c |     36143 |   21879    78198 |   10677    5910   116949    19.8 |  6.403 % |
c |     36649 |   21879    78198 |   11745    6416   125377    19.5 |  6.403 % |
c ==============================================================================
c [1mFound solution: 2331[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7003   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36858 |   21881    78223 |    7293    6625   128663    19.4 |  6.403 % |
c |     36959 |   21881    78223 |    8022    6726   129569    19.3 |  6.452 % |
c |     37109 |   21881    78223 |    8824    6876   131822    19.2 |  6.452 % |
c |     37335 |   21881    78223 |    9706    7102   135764    19.1 |  6.452 % |
c |     37672 |   21881    78223 |   10677    7439   142012    19.1 |  6.452 % |
c |     38182 |   21881    78223 |   11745    7949   151876    19.1 |  6.452 % |
c |     38942 |   21881    78223 |   12919    8709   169649    19.5 |  6.452 % |
c |     40081 |   21881    78223 |   14211    9848   192911    19.6 |  6.452 % |
c |     41789 |   21881    78223 |   15633   11556   251364    21.8 |  6.452 % |
c |     44352 |   21881    78223 |   17196   14119   317012    22.5 |  6.452 % |
c |     48201 |   21881    78223 |   18916    9150   219087    23.9 |  6.452 % |
c ==============================================================================
c [1mFound solution: 2133[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7201   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     50988 |   21890    78272 |    7296   11937   279527    23.4 |  6.452 % |
c |     51089 |   21890    78272 |    8025    6070   120037    19.8 |  6.522 % |
c |     51240 |   21890    78272 |    8828    6221   123310    19.8 |  6.522 % |
c |     51466 |   21890    78272 |    9710    6447   126549    19.6 |  6.522 % |
c |     51805 |   21890    78272 |   10682    6786   131548    19.4 |  6.522 % |
c |     52313 |   21890    78272 |   11750    7294   143520    19.7 |  6.522 % |
c |     53074 |   21890    78272 |   12925    8055   161266    20.0 |  6.522 % |
c |     54213 |   21890    78272 |   14217    9194   181205    19.7 |  6.522 % |
c |     55921 |   21890    78272 |   15639   10902   230029    21.1 |  6.522 % |
c |     58487 |   21890    78272 |   17203   13468   277422    20.6 |  6.522 % |
c |     62331 |   21890    78272 |   18923   17312   389923    22.5 |  6.522 % |
c ==============================================================================
c [1mFound solution: 2126[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7208   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     66073 |   21894    78301 |    7298   10869   248179    22.8 |  6.522 % |
c |     66175 |   21894    78301 |    8027    5537   115679    20.9 |  6.567 % |
c |     66328 |   21894    78301 |    8830    5690   117428    20.6 |  6.567 % |
c |     66553 |   21894    78301 |    9713    5915   120621    20.4 |  6.567 % |
c |     66890 |   21894    78301 |   10685    6252   129031    20.6 |  6.567 % |
c |     67397 |   21894    78301 |   11753    6759   137646    20.4 |  6.567 % |
c |     68157 |   21894    78301 |   12928    7519   156196    20.8 |  6.567 % |
c |     69296 |   21894    78301 |   14221    8658   173513    20.0 |  6.567 % |
c |     71005 |   21894    78301 |   15643   10367   214186    20.7 |  6.567 % |
c |     73568 |   21894    78301 |   17208   12930   256002    19.8 |  6.567 % |
c |     77412 |   21894    78301 |   18929   16774   329698    19.7 |  6.567 % |
c |     83179 |   21894    78301 |   20822   12893   269106    20.9 |  6.567 % |
c |     91829 |   21894    78301 |   22904   21543   634560    29.5 |  6.567 % |
c |    104805 |   21894    78301 |   25194   22588   640028    28.3 |  6.567 % |
c |    124266 |   21888    78284 |   27714   15099   687347    45.5 |  6.593 % |
c |    153459 |   21888    78284 |   30485   14180   269896    19.0 |  6.593 % |
c ==============================================================================
c [1mFound solution: 2125[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7209   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    173987 |   21890    78300 |    7296   14467   655008    45.3 |  6.593 % |
c |    174087 |   21890    78300 |    8025    7334   266686    36.4 |  6.616 % |
c |    174237 |   21890    78300 |    8828    7484   267648    35.8 |  6.616 % |
c |    174464 |   21890    78300 |    9710    7711   270296    35.1 |  6.616 % |
c |    174801 |   21890    78300 |   10682    8048   273599    34.0 |  6.616 % |
c |    175309 |   21890    78300 |   11750    8556   282119    33.0 |  6.616 % |
c |    176068 |   21890    78300 |   12925    9315   300961    32.3 |  6.616 % |
c |    177207 |   21890    78300 |   14217   10454   322054    30.8 |  6.616 % |
c |    178917 |   21890    78300 |   15639   12164   363906    29.9 |  6.616 % |
c |    181479 |   21890    78300 |   17203   14726   429365    29.2 |  6.616 % |
c |    185325 |   21890    78300 |   18923   18572   533358    28.7 |  6.616 % |
c |    191092 |   21890    78300 |   20816   14434   332439    23.0 |  6.616 % |
c |    199741 |   21890    78300 |   22897   12499   269125    21.5 |  6.616 % |
c ==============================================================================
c [1mFound solution: 2115[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7219   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    203378 |   21894    78327 |    7298   16136   402992    25.0 |  6.616 % |
c |    203478 |   21894    78327 |    8027    4134   115704    28.0 |  6.661 % |
c |    203628 |   21894    78327 |    8830    4284   117553    27.4 |  6.661 % |
c |    203854 |   21894    78327 |    9713    4510   120846    26.8 |  6.661 % |
c |    204191 |   21894    78327 |   10685    4847   126623    26.1 |  6.661 % |
c |    204697 |   21894    78327 |   11753    5353   135194    25.3 |  6.661 % |
c |    205456 |   21894    78327 |   12928    6112   154226    25.2 |  6.661 % |
c |    206597 |   21894    78327 |   14221    7253   172150    23.7 |  6.661 % |
c |    208305 |   21894    78327 |   15643    8961   222631    24.8 |  6.661 % |
c |    210868 |   21894    78327 |   17208   11524   298474    25.9 |  6.661 % |
c |    214713 |   21894    78327 |   18929   15369   405858    26.4 |  6.661 % |
c |    220479 |   21894    78327 |   20822   11495   243461    21.2 |  6.661 % |
c ==============================================================================
c [1mFound solution: 2114[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7220   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    227293 |   21896    78344 |    7298   18309   409566    22.4 |  6.661 % |
c |    227393 |   21896    78344 |    8027    4678    93825    20.1 |  6.684 % |
c |    227543 |   21896    78344 |    8830    4828    94557    19.6 |  6.684 % |
c |    227769 |   21896    78344 |    9713    5054    96082    19.0 |  6.684 % |
c |    228106 |   21896    78344 |   10685    5391   100784    18.7 |  6.684 % |
c |    228614 |   21896    78344 |   11753    5899   111676    18.9 |  6.684 % |
c |    229373 |   21896    78344 |   12928    6658   129617    19.5 |  6.684 % |
c |    230513 |   21896    78344 |   14221    7798   155293    19.9 |  6.684 % |
c |    232221 |   21896    78344 |   15643    9506   196420    20.7 |  6.684 % |
c |    234783 |   21896    78344 |   17208   12068   252184    20.9 |  6.684 % |
c ==============================================================================
c [1mFound solution: 2107[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7227   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    237953 |   21900    78372 |    7300   15238   338264    22.2 |  6.684 % |
c |    238053 |   21900    78372 |    8030    3910    77392    19.8 |  6.729 % |
c |    238204 |   21900    78372 |    8833    4061    79052    19.5 |  6.729 % |
c |    238433 |   21900    78372 |    9716    4290    84314    19.7 |  6.729 % |
c |    238770 |   21900    78372 |   10687    4627    94624    20.5 |  6.729 % |
c |    239276 |   21900    78372 |   11756    5133   101311    19.7 |  6.729 % |
c |    240035 |   21900    78372 |   12932    5892   115168    19.5 |  6.729 % |
c |    241174 |   21900    78372 |   14225    7031   142815    20.3 |  6.729 % |
c |    242885 |   21900    78372 |   15648    8742   195748    22.4 |  6.729 % |
c |    245447 |   21900    78372 |   17213   11304   247001    21.9 |  6.729 % |
c |    249291 |   21900    78372 |   18934   15148   327538    21.6 |  6.729 % |
c |    255057 |   21900    78372 |   20827   11269   193421    17.2 |  6.729 % |
c |    263706 |   21900    78372 |   22910   19918   443428    22.3 |  6.729 % |
c ==============================================================================
c [1mFound solution: 2106[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7228   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    265622 |   21902    78389 |    7300   21834   494265    22.6 |  6.729 % |
c |    265723 |   21902    78389 |    8030    5560   122289    22.0 |  6.752 % |
c |    265873 |   21902    78389 |    8833    5710   124067    21.7 |  6.752 % |
c |    266098 |   21902    78389 |    9716    5935   126759    21.4 |  6.752 % |
c |    266435 |   21902    78389 |   10687    6272   133257    21.2 |  6.752 % |
c |    266941 |   21902    78389 |   11756    6778   144572    21.3 |  6.752 % |
c |    267703 |   21902    78389 |   12932    7540   161013    21.4 |  6.752 % |
c |    268843 |   21902    78389 |   14225    8680   190381    21.9 |  6.752 % |
c |    270552 |   21902    78389 |   15648   10389   247942    23.9 |  6.752 % |
c |    273115 |   21902    78389 |   17213   12952   284422    22.0 |  6.752 % |
c ==============================================================================
c [1mFound solution: 2105[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7229   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    275153 |   21904    78405 |    7301   14990   340218    22.7 |  6.752 % |
c |    275256 |   21904    78405 |    8031    7598   141075    18.6 |  6.774 % |
c |    275408 |   21904    78405 |    8834    7750   143710    18.5 |  6.774 % |
c |    275634 |   21904    78405 |    9717    7976   148188    18.6 |  6.774 % |
c |    275971 |   21904    78405 |   10689    8313   154302    18.6 |  6.774 % |
c |    276478 |   21904    78405 |   11758    8820   164130    18.6 |  6.774 % |
c |    277238 |   21904    78405 |   12934    9580   179073    18.7 |  6.774 % |
c |    278378 |   21904    78405 |   14227   10720   206948    19.3 |  6.774 % |
c |    280088 |   21904    78405 |   15650   12430   258760    20.8 |  6.774 % |
c |    282650 |   21904    78405 |   17215   14992   304678    20.3 |  6.774 % |
c |    286498 |   21904    78405 |   18936   10046   220391    21.9 |  6.774 % |
c |    292264 |   21904    78405 |   20830   15812   430931    27.3 |  6.774 % |
c |    300914 |   21904    78405 |   22913   13684   438139    32.0 |  6.774 % |
c |    313889 |   21904    78405 |   25205   14274   412105    28.9 |  6.774 % |
c |    333350 |   21904    78405 |   27725   20630   392994    19.0 |  6.774 % |
c |    362543 |   21904    78405 |   30498   21169   475774    22.5 |  6.774 % |
c |    406332 |   21904    78405 |   33547   29605  1848035    62.4 |  6.774 % |
c |    472019 |   21904    78405 |   36902   13230   444014    33.6 |  6.774 % |
c ==============================================================================
c [1mFound solution: 2104[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7230   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    518248 |   21906    78422 |    7302   37198  1228224    33.0 |  6.774 % |
c |    518348 |   21906    78422 |    8032    4012    75098    18.7 |  6.797 % |
c |    518499 |   21906    78422 |    8835    4163    77446    18.6 |  6.797 % |
c |    518724 |   21906    78422 |    9718    4388    82918    18.9 |  6.797 % |
c |    519063 |   21906    78422 |   10690    4727    87470    18.5 |  6.797 % |
c |    519569 |   21906    78422 |   11759    5233    93966    18.0 |  6.797 % |
c |    520328 |   21906    78422 |   12935    5992   113422    18.9 |  6.797 % |
c |    521467 |   21906    78422 |   14229    7131   144523    20.3 |  6.797 % |
c |    523176 |   21906    78422 |   15652    8840   187866    21.3 |  6.797 % |
c |    525738 |   21906    78422 |   17217   11402   234722    20.6 |  6.797 % |
c |    529582 |   21906    78422 |   18939   15246   349615    22.9 |  6.797 % |
c |    535348 |   21906    78422 |   20833   11377   283202    24.9 |  6.797 % |
c |    543998 |   21906    78422 |   22916   20027   530795    26.5 |  6.797 % |
c |    556974 |   21906    78422 |   25208   21334   533223    25.0 |  6.797 % |
c |    576436 |   21906    78422 |   27729   15159   508997    33.6 |  6.797 % |
c |    605633 |   21906    78422 |   30502   15464   451795    29.2 |  6.797 % |
c |    649422 |   21906    78422 |   33552   24312  1246350    51.3 |  6.797 % |
c ==============================================================================
c [1mFound solution: 2091[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7243   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    662221 |   21912    78457 |    7304   15342   538355    35.1 |  6.797 % |
c |    662323 |   21912    78457 |    8034    3938   110161    28.0 |  6.864 % |
c |    662473 |   21912    78457 |    8837    4088   111416    27.3 |  6.864 % |
c |    662698 |   21912    78457 |    9721    4313   113354    26.3 |  6.864 % |
c |    663035 |   21912    78457 |   10693    4650   118904    25.6 |  6.864 % |
c |    663541 |   21912    78457 |   11763    5156   123735    24.0 |  6.864 % |
c |    664302 |   21912    78457 |   12939    5917   140126    23.7 |  6.864 % |
c |    665441 |   21912    78457 |   14233    7056   167603    23.8 |  6.864 % |
c |    667149 |   21912    78457 |   15656    8764   202743    23.1 |  6.864 % |
c |    669712 |   21912    78457 |   17222   11327   258747    22.8 |  6.864 % |
c |    673556 |   21912    78457 |   18944   15171   419528    27.7 |  6.864 % |
c |    679324 |   21912    78457 |   20839   11265   307026    27.3 |  6.864 % |
c |    687973 |   21912    78457 |   22923   19914   548236    27.5 |  6.864 % |
c ==============================================================================
c [1mFound solution: 2075[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7259   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    694070 |   21918    78498 |    7306   14251   496372    34.8 |  6.864 % |
c |    694172 |   21918    78498 |    8036    7228   278948    38.6 |  6.931 % |
c |    694324 |   21918    78498 |    8840    7380   281371    38.1 |  6.931 % |
c |    694549 |   21918    78498 |    9724    7605   286496    37.7 |  6.931 % |
c |    694886 |   21918    78498 |   10696    7942   294244    37.0 |  6.931 % |
c ==============================================================================
c [1mFound solution: 2073[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7261   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    694949 |   21920    78513 |    7306    8005   295565    36.9 |  6.931 % |
c |    695051 |   21920    78513 |    8036    4105    97260    23.7 |  6.954 % |
c |    695201 |   21920    78513 |    8840    4255    99642    23.4 |  6.954 % |
c |    695426 |   21920    78513 |    9724    4480   103219    23.0 |  6.954 % |
c |    695764 |   21920    78513 |   10696    4818   107637    22.3 |  6.954 % |
c |    696270 |   21920    78513 |   11766    5324   114802    21.6 |  6.954 % |
c |    697029 |   21920    78513 |   12943    6083   126634    20.8 |  6.954 % |
c |    698170 |   21920    78513 |   14237    7224   149830    20.7 |  6.954 % |
c |    699878 |   21920    78513 |   15661    8932   189028    21.2 |  6.954 % |
c |    702442 |   21920    78513 |   17227   11496   269968    23.5 |  6.954 % |
c |    706286 |   21920    78513 |   18949   15340   375591    24.5 |  6.954 % |
c |    712053 |   21920    78513 |   20844   11446   228852    20.0 |  6.954 % |
c |    720702 |   21920    78513 |   22929   20095   545982    27.2 |  6.954 % |
c |    733677 |   21920    78513 |   25222   21359   619872    29.0 |  6.954 % |
c |    753138 |   21920    78513 |   27744   14959   651707    43.6 |  6.954 % |
c |    782330 |   21920    78513 |   30518   14446   375041    26.0 |  6.954 % |
c |    826124 |   21920    78513 |   33570   23530   909562    38.7 |  6.954 % |
c |    891809 |   21920    78513 |   36927   31921   612963    19.2 |  6.954 % |
c ==============================================================================
c [1mFound solution: 2070[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7264   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    932187 |   21923    78539 |    7307   24711  1733709    70.2 |  6.954 % |
c |    932289 |   21923    78539 |    8037    6280   252789    40.3 |  7.000 % |
c |    932439 |   21923    78539 |    8841    6430   253808    39.5 |  7.000 % |
c |    932664 |   21923    78539 |    9725    6655   256081    38.5 |  7.000 % |
c |    933003 |   21923    78539 |   10698    6994   260122    37.2 |  7.000 % |
c |    933509 |   21923    78539 |   11767    7500   266792    35.6 |  7.000 % |
c |    934269 |   21923    78539 |   12944    8260   289050    35.0 |  7.000 % |
c |    935408 |   21923    78539 |   14239    9399   314552    33.5 |  7.000 % |
c |    937118 |   21923    78539 |   15663   11109   356127    32.1 |  7.000 % |
c |    939681 |   21923    78539 |   17229   13672   433944    31.7 |  7.000 % |
c |    943526 |   21923    78539 |   18952   17517   555167    31.7 |  7.000 % |
c ==============================================================================
c [1mFound solution: 2069[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7265   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    945120 |   21925    78552 |    7308   19111   606029    31.7 |  7.000 % |
c |    945220 |   21925    78552 |    8038    4878   116476    23.9 |  7.023 % |
c |    945371 |   21925    78552 |    8842    5029   119239    23.7 |  7.023 % |
c |    945596 |   21925    78552 |    9726    5254   124780    23.7 |  7.023 % |
c |    945935 |   21925    78552 |   10699    5593   131248    23.5 |  7.023 % |
c |    946441 |   21925    78552 |   11769    6099   142681    23.4 |  7.023 % |
c |    947200 |   21925    78552 |   12946    6858   162656    23.7 |  7.023 % |
c |    948340 |   21925    78552 |   14241    7998   193511    24.2 |  7.023 % |
c |    950050 |   21925    78552 |   15665    9708   241446    24.9 |  7.023 % |
c |    952613 |   21925    78552 |   17231   12271   294238    24.0 |  7.023 % |
c |    956457 |   21925    78552 |   18955   16115   435454    27.0 |  7.023 % |
c |    962223 |   21925    78552 |   20850   12223   276343    22.6 |  7.023 % |
c ==============================================================================
c [1mFound solution: 2067[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7267   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    964759 |   21927    78567 |    7309   14759   334126    22.6 |  7.023 % |
c |    964859 |   21927    78567 |    8039    7480   129831    17.4 |  7.045 % |
c |    965012 |   21927    78567 |    8843    7633   132383    17.3 |  7.045 % |
c |    965237 |   21927    78567 |    9728    7858   136727    17.4 |  7.045 % |
c |    965574 |   21927    78567 |   10701    8195   144412    17.6 |  7.045 % |
c |    966080 |   21927    78567 |   11771    8701   154023    17.7 |  7.045 % |
c |    966839 |   21927    78567 |   12948    9460   170897    18.1 |  7.045 % |
c |    967978 |   21927    78567 |   14243   10599   196554    18.5 |  7.045 % |
c |    969687 |   21927    78567 |   15667   12308   238986    19.4 |  7.045 % |
c ==============================================================================
c [1mFound solution: 2065[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7269   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    971239 |   21929    78582 |    7309   13860   296318    21.4 |  7.045 % |
c |    971340 |   21929    78582 |    8039    7031   154831    22.0 |  7.067 % |
c |    971490 |   21929    78582 |    8843    7181   158543    22.1 |  7.067 % |
c |    971716 |   21929    78582 |    9728    7407   162295    21.9 |  7.067 % |
c |    972055 |   21929    78582 |   10701    7746   170225    22.0 |  7.067 % |
c |    972561 |   21929    78582 |   11771    8252   182623    22.1 |  7.067 % |
c |    973320 |   21929    78582 |   12948    9011   200614    22.3 |  7.067 % |
c |    974459 |   21929    78582 |   14243   10150   227187    22.4 |  7.067 % |
c |    976167 |   21929    78582 |   15667   11858   275336    23.2 |  7.067 % |
c |    978730 |   21929    78582 |   17234   14421   326781    22.7 |  7.067 % |
c |    982576 |   21929    78582 |   18957    9455   169560    17.9 |  7.067 % |
c |    988344 |   21929    78582 |   20853   15223   434024    28.5 |  7.067 % |
c |    996994 |   21929    78582 |   22938   12592   496834    39.5 |  7.067 % |
c |   1009971 |   21929    78582 |   25232   13937   273018    19.6 |  7.067 % |
c |   1029432 |   21929    78582 |   27755   19584   824302    42.1 |  7.067 % |
c ==============================================================================
c [1mFound solution: 2062[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7272   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1038458 |   21933    78612 |    7311   28610  1158956    40.5 |  7.067 % |
c |   1038559 |   21933    78612 |    8042    7254   217945    30.0 |  7.111 % |
c |   1038711 |   21933    78612 |    8846    7406   219082    29.6 |  7.111 % |
c |   1038936 |   21933    78612 |    9730    7631   222280    29.1 |  7.111 % |
c |   1039276 |   21933    78612 |   10704    7971   232571    29.2 |  7.111 % |
c |   1039783 |   21933    78612 |   11774    8478   249176    29.4 |  7.111 % |
c |   1040543 |   21933    78612 |   12951    9238   276411    29.9 |  7.111 % |
c |   1041682 |   21933    78612 |   14247   10377   307039    29.6 |  7.111 % |
c |   1043391 |   21933    78612 |   15671   12086   337293    27.9 |  7.111 % |
c |   1045953 |   21933    78612 |   17238   14648   444148    30.3 |  7.111 % |
c |   1049797 |   21933    78612 |   18962    9597   286150    29.8 |  7.111 % |
c |   1055563 |   21933    78612 |   20859   15363   516723    33.6 |  7.111 % |
c ==============================================================================
c [1mFound solution: 2059[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7275   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1063557 |   21935    78626 |    7311   12602   377240    29.9 |  7.111 % |
c |   1063658 |   21935    78626 |    8042    6402   174337    27.2 |  7.134 % |
c |   1063808 |   21935    78626 |    8846    6552   176118    26.9 |  7.134 % |
c |   1064033 |   21935    78626 |    9730    6777   178788    26.4 |  7.134 % |
c |   1064371 |   21935    78626 |   10704    7115   183733    25.8 |  7.134 % |
c |   1064878 |   21935    78626 |   11774    7622   196438    25.8 |  7.134 % |
c |   1065638 |   21935    78626 |   12951    8382   226405    27.0 |  7.134 % |
c |   1066779 |   21935    78626 |   14247    9523   251132    26.4 |  7.134 % |
c |   1068488 |   21935    78626 |   15671   11232   303835    27.1 |  7.134 % |
c |   1071050 |   21935    78626 |   17238   13794   382891    27.8 |  7.134 % |
c |   1074896 |   21935    78626 |   18962   17640   503151    28.5 |  7.134 % |
c |   1080662 |   21935    78626 |   20859   13730   360452    26.3 |  7.134 % |
c ==============================================================================
c [1mFound solution: 2058[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7276   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1088545 |   21937    78642 |    7312   21613   770316    35.6 |  7.134 % |
c |   1088646 |   21937    78642 |    8043    5505   273532    49.7 |  7.156 % |
c |   1088796 |   21937    78642 |    8847    5655   276020    48.8 |  7.156 % |
c |   1089021 |   21937    78642 |    9732    5880   277697    47.2 |  7.156 % |
c |   1089358 |   21937    78642 |   10705    6217   283629    45.6 |  7.156 % |
c |   1089865 |   21937    78642 |   11776    6724   295190    43.9 |  7.156 % |
c |   1090626 |   21937    78642 |   12953    7485   313677    41.9 |  7.156 % |
c |   1091765 |   21937    78642 |   14249    8624   351824    40.8 |  7.156 % |
c |   1093473 |   21937    78642 |   15673   10332   376569    36.4 |  7.156 % |
c |   1096035 |   21937    78642 |   17241   12894   421713    32.7 |  7.156 % |
c |   1099879 |   21937    78642 |   18965   16738   528523    31.6 |  7.156 % |
c |   1105646 |   21937    78642 |   20861   12542   392780    31.3 |  7.156 % |
c |   1114295 |   21937    78642 |   22948   21191   624601    29.5 |  7.156 % |
c ==============================================================================
c [1mFound solution: 2054[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7280   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1121975 |   21941    78670 |    7313   17102   459217    26.9 |  7.156 % |
c |   1122075 |   21941    78670 |    8044    4376    98438    22.5 |  7.200 % |
c |   1122225 |   21941    78670 |    8848    4526   100176    22.1 |  7.200 % |
c |   1122450 |   21941    78670 |    9733    4751   102839    21.6 |  7.200 % |
c |   1122788 |   21941    78670 |   10706    5089   109383    21.5 |  7.200 % |
c |   1123294 |   21941    78670 |   11777    5595   121295    21.7 |  7.200 % |
c |   1124056 |   21941    78670 |   12955    6357   139701    22.0 |  7.200 % |
c |   1125196 |   21941    78670 |   14250    7497   174944    23.3 |  7.200 % |
c |   1126905 |   21941    78670 |   15676    9206   222300    24.1 |  7.200 % |
c |   1129468 |   21941    78670 |   17243   11769   294370    25.0 |  7.200 % |
c |   1133312 |   21941    78670 |   18968   15613   431694    27.6 |  7.200 % |
c |   1139078 |   21941    78670 |   20864   11411   402980    35.3 |  7.200 % |
c ==============================================================================
c [1mFound solution: 2052[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7282   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1146189 |   21944    78701 |    7314   18522   668311    36.1 |  7.200 % |
c |   1146289 |   21944    78701 |    8045    4731   127404    26.9 |  7.246 % |
c |   1146440 |   21944    78701 |    8849    4882   130121    26.7 |  7.246 % |
c |   1146665 |   21944    78701 |    9734    5107   136000    26.6 |  7.246 % |
c |   1147003 |   21944    78701 |   10708    5445   140779    25.9 |  7.246 % |
c |   1147509 |   21944    78701 |   11779    5951   149263    25.1 |  7.246 % |
c |   1148270 |   21944    78701 |   12957    6712   165737    24.7 |  7.246 % |
c |   1149410 |   21944    78701 |   14252    7852   190787    24.3 |  7.246 % |
c |   1151118 |   21944    78701 |   15678    9560   220654    23.1 |  7.246 % |
c |   1153680 |   21944    78701 |   17246   12122   272820    22.5 |  7.246 % |
c |   1157524 |   21944    78701 |   18970   15966   370727    23.2 |  7.246 % |
c |   1163291 |   21944    78701 |   20867   12079   252884    20.9 |  7.246 % |
c |   1171940 |   21944    78701 |   22954   20728   694473    33.5 |  7.246 % |
c ==============================================================================
c [1mFound solution: 2051[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7283   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1176466 |   21946    78715 |    7315   13475   556475    41.3 |  7.246 % |
c |   1176570 |   21946    78715 |    8046    6842   173053    25.3 |  7.268 % |
c |   1176721 |   21946    78715 |    8851    6993   175888    25.2 |  7.268 % |
c |   1176946 |   21946    78715 |    9736    7218   182682    25.3 |  7.268 % |
c |   1177283 |   21946    78715 |   10709    7555   188598    25.0 |  7.268 % |
c |   1177790 |   21946    78715 |   11780    8062   202632    25.1 |  7.268 % |
c |   1178551 |   21946    78715 |   12958    8823   222566    25.2 |  7.268 % |
c |   1179691 |   21946    78715 |   14254    9963   245419    24.6 |  7.268 % |
c |   1181401 |   21946    78715 |   15680   11673   277064    23.7 |  7.268 % |
c |   1183966 |   21946    78715 |   17248   14238   362752    25.5 |  7.268 % |
c |   1187810 |   21946    78715 |   18973    9273   179001    19.3 |  7.268 % |
c |   1193577 |   21946    78715 |   20870   15040   299946    19.9 |  7.268 % |
c |   1202226 |   21946    78715 |   22957   12487   308168    24.7 |  7.268 % |
c |   1215200 |   21946    78715 |   25253   13806   364462    26.4 |  7.268 % |
c |   1234662 |   21946    78715 |   27778   20195   670377    33.2 |  7.268 % |
c ==============================================================================
c [1mFound solution: 2050[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7284   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1249580 |   21948    78730 |    7316   20707   765571    37.0 |  7.268 % |
c |   1249680 |   21948    78730 |    8047    5277   223622    42.4 |  7.290 % |
c |   1249830 |   21948    78730 |    8852    5427   224682    41.4 |  7.290 % |
c |   1250056 |   21948    78730 |    9737    5653   226455    40.1 |  7.290 % |
c |   1250393 |   21948    78730 |   10711    5990   231864    38.7 |  7.290 % |
c |   1250900 |   21948    78730 |   11782    6497   239711    36.9 |  7.290 % |
c |   1251659 |   21948    78730 |   12960    7256   260468    35.9 |  7.290 % |
c |   1252798 |   21948    78730 |   14256    8395   286203    34.1 |  7.290 % |
c |   1254509 |   21948    78730 |   15682   10106   334285    33.1 |  7.290 % |
c |   1257071 |   21948    78730 |   17250   12668   396636    31.3 |  7.290 % |
c |   1260915 |   21948    78730 |   18975   16512   507124    30.7 |  7.290 % |
c |   1266683 |   21948    78730 |   20873   12615   252261    20.0 |  7.290 % |
c |   1275333 |   21948    78730 |   22960   21265   462633    21.8 |  7.290 % |
c |   1288307 |   21948    78730 |   25256   22302   603439    27.1 |  7.290 % |
c |   1307772 |   21948    78730 |   27782   16174   309939    19.2 |  7.290 % |
c |   1336964 |   21948    78730 |   30560   13509   482083    35.7 |  7.290 % |
c |   1380754 |   21948    78730 |   33616   23113   726768    31.4 |  7.290 % |
c |   1446439 |   21948    78730 |   36978   28054  1572013    56.0 |  7.290 % |
c ==============================================================================
c [1mFound solution: 2049[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7285   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1453924 |   21950    78745 |    7316   35539  1816955    51.1 |  7.290 % |
c |   1454024 |   21950    78745 |    8047    4052   107547    26.5 |  7.312 % |
c |   1454175 |   21950    78745 |    8852    4203   109589    26.1 |  7.312 % |
c |   1454401 |   21950    78745 |    9737    4429   114050    25.8 |  7.312 % |
c |   1454739 |   21950    78745 |   10711    4767   120668    25.3 |  7.312 % |
c |   1455246 |   21950    78745 |   11782    5274   132128    25.1 |  7.312 % |
c |   1456006 |   21950    78745 |   12960    6034   153904    25.5 |  7.312 % |
c |   1457146 |   21950    78745 |   14256    7174   171215    23.9 |  7.312 % |
c |   1458855 |   21950    78745 |   15682    8883   226752    25.5 |  7.312 % |
c |   1461417 |   21950    78745 |   17250   11445   340097    29.7 |  7.312 % |
c |   1465262 |   21950    78745 |   18975   15290   475624    31.1 |  7.312 % |
c |   1471029 |   21950    78745 |   20873   11312   343128    30.3 |  7.312 % |
c |   1479678 |   21950    78745 |   22960   19961   597511    29.9 |  7.312 % |
c |   1492652 |   21950    78745 |   25256   21177   739935    34.9 |  7.312 % |
c |   1512113 |   21950    78745 |   27782   14788   478777    32.4 |  7.312 % |
c ==============================================================================
c [1mFound solution: 2048[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7286   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1526206 |   21952    78762 |    7317   28881  1284962    44.5 |  7.312 % |
c |   1526308 |   21952    78762 |    8048    6525   324269    49.7 |  7.334 % |
c |   1526458 |   21952    78762 |    8853    6675   325408    48.8 |  7.334 % |
c |   1526683 |   21952    78762 |    9738    6900   328493    47.6 |  7.334 % |
c |   1527020 |   21952    78762 |   10712    7237   332500    45.9 |  7.334 % |
c |   1527526 |   21952    78762 |   11784    7743   336524    43.5 |  7.334 % |
c |   1528285 |   21952    78762 |   12962    8502   345911    40.7 |  7.334 % |
c |   1529426 |   21952    78762 |   14258    9643   381702    39.6 |  7.334 % |
c |   1531134 |   21952    78762 |   15684   11351   427733    37.7 |  7.334 % |
c |   1533696 |   21952    78762 |   17253   13913   479030    34.4 |  7.334 % |
c |   1537541 |   21952    78762 |   18978   17758   588469    33.1 |  7.334 % |
c |   1543307 |   21952    78762 |   20876   13813   325198    23.5 |  7.334 % |
c |   1551958 |   21952    78762 |   22963   11431   304337    26.6 |  7.334 % |
c |   1564932 |   21952    78762 |   25260   12637   426430    33.7 |  7.334 % |
#### 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.83 0.88 0.90 2/54 29757
Raw data (stat): 29757 (runsolver) R 29756 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 482518444 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.001 s]
Raw data (loadavg): 0.85 0.88 0.90 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 1393 0 0 0 995 2 0 0 25 0 1 0 482518444 7311360 1371 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1785 1371 603 41 0 1744 0
vsize: 7140
[startup+20.0016 s]
Raw data (loadavg): 0.87 0.89 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 1413 0 0 0 1994 3 0 0 25 0 1 0 482518444 7446528 1391 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1818 1391 603 41 0 1777 0
vsize: 7272
[startup+30.0025 s]
Raw data (loadavg): 0.89 0.89 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 1476 0 0 0 2993 4 0 0 25 0 1 0 482518444 7716864 1454 4294967295 134512640 134672761 3221224544 3221223728 134559542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1884 1454 603 41 0 1843 0
vsize: 7536
[startup+40.004 s]
Raw data (loadavg): 0.91 0.89 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 1571 0 0 0 3992 4 0 0 25 0 1 0 482518444 7987200 1549 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1950 1549 603 41 0 1909 0
vsize: 7800
[startup+50.0051 s]
Raw data (loadavg): 0.92 0.89 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 1899 0 0 0 4992 5 0 0 25 0 1 0 482518444 9342976 1877 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2281 1877 603 41 0 2240 0
vsize: 9124
[startup+60.0059 s]
Raw data (loadavg): 0.93 0.90 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 2072 0 0 0 5991 6 0 0 25 0 1 0 482518444 10149888 2050 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2478 2050 603 41 0 2437 0
vsize: 9912
[startup+70.0064 s]
Raw data (loadavg): 0.94 0.90 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 2346 0 0 0 6991 7 0 0 25 0 1 0 482518444 11218944 2324 4294967295 134512640 134672761 3221224544 3221223712 134553603 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2739 2324 603 41 0 2698 0
vsize: 10956
[startup+80.0067 s]
Raw data (loadavg): 0.95 0.90 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 2418 0 0 0 7990 7 0 0 25 0 1 0 482518444 11522048 2396 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2813 2396 603 41 0 2772 0
vsize: 11252
[startup+90.0065 s]
Raw data (loadavg): 0.96 0.91 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 2418 0 0 0 8991 7 0 0 25 0 1 0 482518444 11522048 2396 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2813 2396 603 41 0 2772 0
vsize: 11252
[startup+100.007 s]
Raw data (loadavg): 0.96 0.91 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 2508 0 0 0 9990 7 0 0 25 0 1 0 482518444 11927552 2486 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2912 2486 603 41 0 2871 0
vsize: 11648
[startup+110.007 s]
Raw data (loadavg): 0.97 0.91 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 2508 0 0 0 10990 7 0 0 25 0 1 0 482518444 11927552 2486 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2912 2486 603 41 0 2871 0
vsize: 11648
[startup+120.008 s]
Raw data (loadavg): 0.97 0.91 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 2509 0 0 0 11990 7 0 0 25 0 1 0 482518444 11927552 2487 4294967295 134512640 134672761 3221224544 3221223696 134541817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2912 2487 603 41 0 2871 0
vsize: 11648
[startup+130.008 s]
Raw data (loadavg): 0.98 0.92 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 2509 0 0 0 12990 7 0 0 25 0 1 0 482518444 11927552 2487 4294967295 134512640 134672761 3221224544 3221223712 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2912 2487 603 41 0 2871 0
vsize: 11648
[startup+140.009 s]
Raw data (loadavg): 0.98 0.92 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 2509 0 0 0 13991 7 0 0 25 0 1 0 482518444 11927552 2487 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2912 2487 603 41 0 2871 0
vsize: 11648
[startup+150.009 s]
Raw data (loadavg): 0.98 0.92 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 2509 0 0 0 14991 8 0 0 25 0 1 0 482518444 11927552 2487 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2912 2487 603 41 0 2871 0
vsize: 11648
[startup+160.009 s]
Raw data (loadavg): 0.98 0.92 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 2509 0 0 0 15991 8 0 0 25 0 1 0 482518444 11927552 2487 4294967295 134512640 134672761 3221224544 3221223712 134564451 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2912 2487 603 41 0 2871 0
vsize: 11648
[startup+170.009 s]
Raw data (loadavg): 0.99 0.92 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 2509 0 0 0 16991 8 0 0 25 0 1 0 482518444 11927552 2487 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2912 2487 603 41 0 2871 0
vsize: 11648
[startup+180.008 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 2509 0 0 0 17991 8 0 0 25 0 1 0 482518444 11927552 2487 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2912 2487 603 41 0 2871 0
vsize: 11648
[startup+190.009 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 2513 0 0 0 18991 8 0 0 25 0 1 0 482518444 11927552 2491 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2912 2491 603 41 0 2871 0
vsize: 11648
[startup+200.009 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 2514 0 0 0 19991 8 0 0 25 0 1 0 482518444 11927552 2492 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2912 2492 603 41 0 2871 0
vsize: 11648
[startup+210.01 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 2528 0 0 0 20991 8 0 0 25 0 1 0 482518444 12066816 2506 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2946 2506 603 41 0 2905 0
vsize: 11784
[startup+220.011 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 2583 0 0 0 21992 8 0 0 25 0 1 0 482518444 12197888 2561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2978 2561 603 41 0 2937 0
vsize: 11912
[startup+230.011 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3107 0 0 0 22990 10 0 0 25 0 1 0 482518444 14356480 3085 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3505 3085 603 41 0 3464 0
vsize: 14020
[startup+240.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3505 0 0 0 23989 11 0 0 25 0 1 0 482518444 15974400 3483 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3900 3483 603 41 0 3859 0
vsize: 15600
[startup+250.011 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3517 0 0 0 24989 11 0 0 25 0 1 0 482518444 16113664 3495 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3934 3495 603 41 0 3893 0
vsize: 15736
[startup+260.011 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3818 0 0 0 25988 12 0 0 25 0 1 0 482518444 17453056 3796 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4261 3796 603 41 0 4220 0
vsize: 17044
[startup+270.011 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3818 0 0 0 26989 12 0 0 25 0 1 0 482518444 17453056 3796 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4261 3796 603 41 0 4220 0
vsize: 17044
[startup+280.011 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3818 0 0 0 27989 12 0 0 25 0 1 0 482518444 17453056 3796 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4261 3796 603 41 0 4220 0
vsize: 17044
[startup+290.012 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3820 0 0 0 28989 12 0 0 25 0 1 0 482518444 17453056 3798 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4261 3798 603 41 0 4220 0
vsize: 17044
[startup+300.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3820 0 0 0 29989 12 0 0 25 0 1 0 482518444 17453056 3798 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4261 3798 603 41 0 4220 0
vsize: 17044
[startup+310.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3820 0 0 0 30989 12 0 0 25 0 1 0 482518444 17453056 3798 4294967295 134512640 134672761 3221224544 3221223712 134561533 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4261 3798 603 41 0 4220 0
vsize: 17044
[startup+320.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3820 0 0 0 31989 12 0 0 25 0 1 0 482518444 17453056 3798 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4261 3798 603 41 0 4220 0
vsize: 17044
[startup+330.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3820 0 0 0 32990 12 0 0 25 0 1 0 482518444 17453056 3798 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4261 3798 603 41 0 4220 0
vsize: 17044
[startup+340.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3823 0 0 0 33990 12 0 0 25 0 1 0 482518444 17453056 3801 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4261 3801 603 41 0 4220 0
vsize: 17044
[startup+350.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3823 0 0 0 34990 12 0 0 25 0 1 0 482518444 17453056 3801 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4261 3801 603 41 0 4220 0
vsize: 17044
[startup+360.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3823 0 0 0 35990 12 0 0 25 0 1 0 482518444 17453056 3801 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4261 3801 603 41 0 4220 0
vsize: 17044
[startup+370.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3823 0 0 0 36990 12 0 0 25 0 1 0 482518444 17453056 3801 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4261 3801 603 41 0 4220 0
vsize: 17044
[startup+380.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3823 0 0 0 37991 12 0 0 25 0 1 0 482518444 17453056 3801 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4261 3801 603 41 0 4220 0
vsize: 17044
[startup+390.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3823 0 0 0 38991 12 0 0 25 0 1 0 482518444 17453056 3801 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4261 3801 603 41 0 4220 0
vsize: 17044
[startup+400.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3823 0 0 0 39991 12 0 0 25 0 1 0 482518444 17453056 3801 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4261 3801 603 41 0 4220 0
vsize: 17044
[startup+410.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3823 0 0 0 40991 12 0 0 25 0 1 0 482518444 17453056 3801 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4261 3801 603 41 0 4220 0
vsize: 17044
[startup+420.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3823 0 0 0 41991 12 0 0 25 0 1 0 482518444 17453056 3801 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4261 3801 603 41 0 4220 0
vsize: 17044
[startup+430.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3823 0 0 0 42991 12 0 0 25 0 1 0 482518444 17453056 3801 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4261 3801 603 41 0 4220 0
vsize: 17044
[startup+440.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3823 0 0 0 43992 12 0 0 25 0 1 0 482518444 17453056 3801 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4261 3801 603 41 0 4220 0
vsize: 17044
[startup+450.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3823 0 0 0 44992 12 0 0 25 0 1 0 482518444 17453056 3801 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4261 3801 603 41 0 4220 0
vsize: 17044
[startup+460.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3823 0 0 0 45992 12 0 0 25 0 1 0 482518444 17453056 3801 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4261 3801 603 41 0 4220 0
vsize: 17044
[startup+470.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3823 0 0 0 46992 12 0 0 25 0 1 0 482518444 17453056 3801 4294967295 134512640 134672761 3221224544 3221223712 134561018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4261 3801 603 41 0 4220 0
vsize: 17044
[startup+480.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3823 0 0 0 47992 12 0 0 25 0 1 0 482518444 17453056 3801 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4261 3801 603 41 0 4220 0
vsize: 17044
[startup+490.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3981 0 0 0 48992 12 0 0 25 0 1 0 482518444 18124800 3959 4294967295 134512640 134672761 3221224544 3221223024 134565829 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4425 3959 603 41 0 4384 0
vsize: 17700
[startup+500.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3981 0 0 0 49992 12 0 0 25 0 1 0 482518444 18124800 3959 4294967295 134512640 134672761 3221224544 3221223728 134559583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4425 3959 603 41 0 4384 0
vsize: 17700
[startup+510.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3981 0 0 0 50992 12 0 0 25 0 1 0 482518444 18124800 3959 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4425 3959 603 41 0 4384 0
vsize: 17700
[startup+520.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3981 0 0 0 51993 12 0 0 25 0 1 0 482518444 18124800 3959 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4425 3959 603 41 0 4384 0
vsize: 17700
[startup+530.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3981 0 0 0 52993 12 0 0 25 0 1 0 482518444 18124800 3959 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4425 3959 603 41 0 4384 0
vsize: 17700
[startup+540.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3981 0 0 0 53993 12 0 0 25 0 1 0 482518444 18124800 3959 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4425 3959 603 41 0 4384 0
vsize: 17700
[startup+550.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3981 0 0 0 54994 12 0 0 25 0 1 0 482518444 18124800 3959 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4425 3959 603 41 0 4384 0
vsize: 17700
[startup+560.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3981 0 0 0 55994 12 0 0 25 0 1 0 482518444 18124800 3959 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4425 3959 603 41 0 4384 0
vsize: 17700
[startup+570.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3981 0 0 0 56994 12 0 0 25 0 1 0 482518444 18124800 3959 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4425 3959 603 41 0 4384 0
vsize: 17700
[startup+580.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3983 0 0 0 57994 12 0 0 25 0 1 0 482518444 18124800 3961 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4425 3961 603 41 0 4384 0
vsize: 17700
[startup+590.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3983 0 0 0 58995 12 0 0 25 0 1 0 482518444 18124800 3961 4294967295 134512640 134672761 3221224544 3221223648 134554673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4425 3961 603 41 0 4384 0
vsize: 17700
[startup+600.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3983 0 0 0 59995 12 0 0 25 0 1 0 482518444 18124800 3961 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4425 3961 603 41 0 4384 0
vsize: 17700
[startup+610.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3993 0 0 0 60996 12 0 0 25 0 1 0 482518444 18124800 3971 4294967295 134512640 134672761 3221224544 3221223648 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4425 3971 603 41 0 4384 0
vsize: 17700
[startup+620.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3993 0 0 0 61996 12 0 0 25 0 1 0 482518444 18124800 3971 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4425 3971 603 41 0 4384 0
vsize: 17700
[startup+630.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 3993 0 0 0 62996 13 0 0 25 0 1 0 482518444 18124800 3971 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4425 3971 603 41 0 4384 0
vsize: 17700
[startup+640.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 4015 0 0 0 63996 13 0 0 25 0 1 0 482518444 18305024 3993 4294967295 134512640 134672761 3221224544 3221223712 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4469 3993 603 41 0 4428 0
vsize: 17876
[startup+650.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 4030 0 0 0 64997 13 0 0 25 0 1 0 482518444 18305024 4008 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4469 4008 603 41 0 4428 0
vsize: 17876
[startup+660.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 4051 0 0 0 65997 13 0 0 25 0 1 0 482518444 18501632 4029 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4029 603 41 0 4476 0
vsize: 18068
[startup+670.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 4051 0 0 0 66997 13 0 0 25 0 1 0 482518444 18501632 4029 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4029 603 41 0 4476 0
vsize: 18068
[startup+680.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 4061 0 0 0 67997 13 0 0 25 0 1 0 482518444 18501632 4039 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4039 603 41 0 4476 0
vsize: 18068
[startup+690.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 4066 0 0 0 68997 13 0 0 25 0 1 0 482518444 18501632 4044 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4044 603 41 0 4476 0
vsize: 18068
[startup+700.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 4086 0 0 0 69997 13 0 0 25 0 1 0 482518444 18636800 4064 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4550 4064 603 41 0 4509 0
vsize: 18200
[startup+710.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 4715 0 0 0 70996 14 0 0 25 0 1 0 482518444 21192704 4693 4294967295 134512640 134672761 3221224544 3221223648 134560285 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5174 4693 603 41 0 5133 0
vsize: 20696
[startup+720.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5265 0 0 0 71995 16 0 0 25 0 1 0 482518444 23539712 5243 4294967295 134512640 134672761 3221224544 3221223648 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5747 5243 603 41 0 5706 0
vsize: 22988
[startup+730.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5265 0 0 0 72995 16 0 0 25 0 1 0 482518444 23539712 5243 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5747 5243 603 41 0 5706 0
vsize: 22988
[startup+740.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5265 0 0 0 73995 16 0 0 25 0 1 0 482518444 23535616 5243 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5746 5243 603 41 0 5705 0
vsize: 22984
[startup+750.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5265 0 0 0 74995 16 0 0 25 0 1 0 482518444 23322624 5211 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5211 603 41 0 5653 0
vsize: 22776
[startup+760.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5265 0 0 0 75995 16 0 0 25 0 1 0 482518444 23322624 5211 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5211 603 41 0 5653 0
vsize: 22776
[startup+770.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5265 0 0 0 76996 16 0 0 25 0 1 0 482518444 23322624 5211 4294967295 134512640 134672761 3221224544 3221223636 1075351210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5211 603 41 0 5653 0
vsize: 22776
[startup+780.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5265 0 0 0 77996 16 0 0 25 0 1 0 482518444 23322624 5211 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5211 603 41 0 5653 0
vsize: 22776
[startup+790.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5265 0 0 0 78996 16 0 0 25 0 1 0 482518444 23322624 5211 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5211 603 41 0 5653 0
vsize: 22776
[startup+800.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5265 0 0 0 79996 16 0 0 25 0 1 0 482518444 23322624 5211 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5211 603 41 0 5653 0
vsize: 22776
[startup+810.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5265 0 0 0 80996 16 0 0 25 0 1 0 482518444 23322624 5211 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5211 603 41 0 5653 0
vsize: 22776
[startup+820.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5265 0 0 0 81996 16 0 0 25 0 1 0 482518444 23322624 5211 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5211 603 41 0 5653 0
vsize: 22776
[startup+830.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5265 0 0 0 82997 16 0 0 25 0 1 0 482518444 23322624 5211 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5211 603 41 0 5653 0
vsize: 22776
[startup+840.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5265 0 0 0 83997 16 0 0 25 0 1 0 482518444 23322624 5211 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5211 603 41 0 5653 0
vsize: 22776
[startup+850.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5265 0 0 0 84997 16 0 0 25 0 1 0 482518444 23322624 5211 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5211 603 41 0 5653 0
vsize: 22776
[startup+860.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5265 0 0 0 85997 16 0 0 25 0 1 0 482518444 23322624 5211 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5211 603 41 0 5653 0
vsize: 22776
[startup+870.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5265 0 0 0 86997 16 0 0 25 0 1 0 482518444 23322624 5211 4294967295 134512640 134672761 3221224544 3221223648 134560399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5211 603 41 0 5653 0
vsize: 22776
[startup+880.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5265 0 0 0 87997 16 0 0 25 0 1 0 482518444 23322624 5211 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5211 603 41 0 5653 0
vsize: 22776
[startup+890.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5265 0 0 0 88997 16 0 0 25 0 1 0 482518444 23322624 5211 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5211 603 41 0 5653 0
vsize: 22776
[startup+900.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5265 0 0 0 89997 17 0 0 25 0 1 0 482518444 23322624 5211 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5211 603 41 0 5653 0
vsize: 22776
[startup+910.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5265 0 0 0 90997 17 0 0 25 0 1 0 482518444 23322624 5211 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5211 603 41 0 5653 0
vsize: 22776
[startup+920.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5265 0 0 0 91998 17 0 0 25 0 1 0 482518444 23322624 5211 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5211 603 41 0 5653 0
vsize: 22776
[startup+930.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5265 0 0 0 92998 17 0 0 25 0 1 0 482518444 23322624 5211 4294967295 134512640 134672761 3221224544 3221223712 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5211 603 41 0 5653 0
vsize: 22776
[startup+940.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5265 0 0 0 93998 17 0 0 25 0 1 0 482518444 23322624 5211 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5211 603 41 0 5653 0
vsize: 22776
[startup+950.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5265 0 0 0 94998 17 0 0 25 0 1 0 482518444 23322624 5211 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5211 603 41 0 5653 0
vsize: 22776
[startup+960.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5265 0 0 0 95998 17 0 0 25 0 1 0 482518444 23322624 5211 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5211 603 41 0 5653 0
vsize: 22776
[startup+970.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5265 0 0 0 96998 17 0 0 25 0 1 0 482518444 23322624 5211 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5211 603 41 0 5653 0
vsize: 22776
[startup+980.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5265 0 0 0 97998 17 0 0 25 0 1 0 482518444 23322624 5211 4294967295 134512640 134672761 3221224544 3221223744 134557922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5211 603 41 0 5653 0
vsize: 22776
[startup+990.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5265 0 0 0 98999 17 0 0 25 0 1 0 482518444 23322624 5211 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5211 603 41 0 5653 0
vsize: 22776
[startup+1000.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5265 0 0 0 99999 17 0 0 25 0 1 0 482518444 23322624 5211 4294967295 134512640 134672761 3221224544 3221223640 1075347141 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5211 603 41 0 5653 0
vsize: 22776
[startup+1010.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5266 0 0 0 100999 17 0 0 25 0 1 0 482518444 23322624 5212 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5212 603 41 0 5653 0
vsize: 22776
[startup+1020.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5266 0 0 0 101999 17 0 0 25 0 1 0 482518444 23322624 5212 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5212 603 41 0 5653 0
vsize: 22776
[startup+1030.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5266 0 0 0 103000 17 0 0 25 0 1 0 482518444 23322624 5212 4294967295 134512640 134672761 3221224544 3221223648 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5212 603 41 0 5653 0
vsize: 22776
[startup+1040.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5266 0 0 0 104000 17 0 0 25 0 1 0 482518444 23322624 5212 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5212 603 41 0 5653 0
vsize: 22776
[startup+1050.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5266 0 0 0 105000 17 0 0 25 0 1 0 482518444 23322624 5212 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5212 603 41 0 5653 0
vsize: 22776
[startup+1060.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5266 0 0 0 106000 17 0 0 25 0 1 0 482518444 23322624 5212 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5212 603 41 0 5653 0
vsize: 22776
[startup+1070.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5267 0 0 0 107000 17 0 0 25 0 1 0 482518444 23322624 5213 4294967295 134512640 134672761 3221224544 3221223712 134561226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5213 603 41 0 5653 0
vsize: 22776
[startup+1080.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5267 0 0 0 108000 17 0 0 25 0 1 0 482518444 23322624 5213 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5213 603 41 0 5653 0
vsize: 22776
[startup+1090.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5267 0 0 0 109001 17 0 0 25 0 1 0 482518444 23322624 5213 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5213 603 41 0 5653 0
vsize: 22776
[startup+1100.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5267 0 0 0 110001 17 0 0 25 0 1 0 482518444 23322624 5213 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5213 603 41 0 5653 0
vsize: 22776
[startup+1110.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5267 0 0 0 111001 17 0 0 25 0 1 0 482518444 23322624 5213 4294967295 134512640 134672761 3221224544 3221223728 134559542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5213 603 41 0 5653 0
vsize: 22776
[startup+1120.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5267 0 0 0 112001 17 0 0 25 0 1 0 482518444 23322624 5213 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5213 603 41 0 5653 0
vsize: 22776
[startup+1130.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5267 0 0 0 113001 17 0 0 25 0 1 0 482518444 23322624 5213 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5213 603 41 0 5653 0
vsize: 22776
[startup+1140.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5267 0 0 0 114001 17 0 0 25 0 1 0 482518444 23322624 5213 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5213 603 41 0 5653 0
vsize: 22776
[startup+1150.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5267 0 0 0 115002 17 0 0 25 0 1 0 482518444 23322624 5213 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5213 603 41 0 5653 0
vsize: 22776
[startup+1160.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5267 0 0 0 116002 17 0 0 25 0 1 0 482518444 23322624 5213 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5213 603 41 0 5653 0
vsize: 22776
[startup+1170.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5268 0 0 0 117002 17 0 0 25 0 1 0 482518444 23322624 5214 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5214 603 41 0 5653 0
vsize: 22776
[startup+1180.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5268 0 0 0 118002 17 0 0 25 0 1 0 482518444 23322624 5214 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5214 603 41 0 5653 0
vsize: 22776
[startup+1190.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5268 0 0 0 119002 17 0 0 25 0 1 0 482518444 23322624 5214 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5214 603 41 0 5653 0
vsize: 22776
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29757
Raw data (stat): 29757 (minisat+) R 29756 5897 5896 0 -1 0 5268 0 0 0 120002 17 0 0 25 0 1 0 482518444 23322624 5214 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5214 603 41 0 5653 0
vsize: 22776
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 29757
Raw data (stat): 29757 (minisat+) Z 29756 5897 5896 0 -1 12 5271 0 0 0 120002 18 0 0 25 0 1 0 482518444 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.08
CPU time (s): 1200.21
CPU user time (s): 1200.03
CPU system time (s): 0.184971
CPU usage (%): 100.011
Max. virtual memory (Kb): 22988
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####