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/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:20:4.5:0.95:100.opb
MD5SUM	f82b685b64af240616b701a750c82883
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	10
Optimality of the best value was proved	NO
Number of terms in the objective function	934
Biggest coefficient in the objective function	546
Number of bits for the biggest coefficient in the objective function	10
Sum of the numbers in the objective function	2594
Number of bits of the sum of numbers in the objective function	12
Biggest number in a constraint	546
Number of bits of the biggest number in a constraint	10
Biggest sum of numbers in a constraint	2594
Number of bits of the biggest sum of numbers	12
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03784
Number of variables	934
Total number of constraints	1996
Number of constraints which are clauses	879
Number of constraints which are cardinality constraints (but not clauses)	1117
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	20
Trace number 5685

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-04-14 01:23:36 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4127 boxname=wulflinc19 idbench=367 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f82b685b64af240616b701a750c82883  /oldhome/oroussel/tmp/wulflinc19/normalized-10:20:4.5:0.95:100.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc19/normalized-10:20:4.5:0.95:100.opb /oldhome/oroussel/tmp/wulflinc19/normalized-10:20:4.5:0.95:100.opb
IDLAUNCH: 4127
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 3
cpu MHz		: 451.037
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:        883192 kB
Buffers:         35056 kB
Cached:          82460 kB
SwapCached:         56 kB
Active:          48352 kB
Inactive:        72092 kB
HighTotal:      131008 kB
HighFree:        44492 kB
LowTotal:       903652 kB
LowFree:        838700 kB
SwapTotal:     2097892 kB
SwapFree:      2097836 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7028 kB
Slab:            25296 kB
Committed_AS:    63708 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 01:43:39 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 4127 7 1200.23 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1062 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[ 190]---> BDD-cost:   11
c ---[ 189]---> BDD-cost:   11
c ---[ 188]---> BDD-cost:   17
c ---[ 187]---> BDD-cost:   20
c ---[ 186]---> BDD-cost:   20
c ---[ 185]---> BDD-cost:   17
c ---[ 184]---> BDD-cost:   23
c ---[ 183]---> BDD-cost:   26
c ---[ 182]---> BDD-cost:   23
c ---[ 181]---> BDD-cost:   17
c ---[ 180]---> BDD-cost:   23
c ---[ 179]---> BDD-cost:   17
c ---[ 178]---> BDD-cost:   17
c ---[ 177]---> BDD-cost:   17
c ---[ 176]---> BDD-cost:   17
c ---[ 175]---> BDD-cost:   11
c ---[ 174]---> BDD-cost:    5
c ---[ 173]---> BDD-cost:   14
c ---[ 172]---> BDD-cost:   17
c ---[ 171]---> BDD-cost:   23
c ---[ 170]---> BDD-cost:   21
c ---[ 169]---> BDD-cost:   29
c ---[ 168]---> BDD-cost:   26
c ---[ 167]---> BDD-cost:   26
c ---[ 166]---> BDD-cost:   27
c ---[ 165]---> BDD-cost:   38
c ---[ 164]---> BDD-cost:   29
c ---[ 163]---> BDD-cost:   29
c ---[ 162]---> BDD-cost:   26
c ---[ 161]---> BDD-cost:   23
c ---[ 160]---> BDD-cost:   20
c ---[ 159]---> BDD-cost:   20
c ---[ 158]---> BDD-cost:   17
c ---[ 156]---> BDD-cost:   20
c ---[ 155]---> BDD-cost:   23
c ---[ 154]---> BDD-cost:   26
c ---[ 153]---> BDD-cost:   32
c ---[ 152]---> BDD-cost:   35
c ---[ 151]---> BDD-cost:   29
c ---[ 150]---> BDD-cost:   41
c ---[ 149]---> BDD-cost:   38
c ---[ 148]---> BDD-cost:   36
c ---[ 147]---> BDD-cost:   32
c ---[ 146]---> BDD-cost:   32
c ---[ 145]---> BDD-cost:   29
c ---[ 144]---> BDD-cost:   29
c ---[ 143]---> BDD-cost:   26
c ---[ 142]---> BDD-cost:   26
c ---[ 141]---> BDD-cost:   13
c ---[ 140]---> BDD-cost:    9
c ---[ 138]---> BDD-cost:    7
c ---[ 136]---> BDD-cost:   21
c ---[ 135]---> BDD-cost:   29
c ---[ 134]---> BDD-cost:   35
c ---[ 133]---> BDD-cost:   32
c ---[ 132]---> BDD-cost:   44
c ---[ 131]---> BDD-cost:   44
c ---[ 130]---> BDD-cost:   44
c ---[ 129]---> BDD-cost:   38
c ---[ 128]---> BDD-cost:   38
c ---[ 127]---> BDD-cost:   32
c ---[ 126]---> BDD-cost:   35
c ---[ 125]---> BDD-cost:   32
c ---[ 124]---> BDD-cost:   38
c ---[ 123]---> BDD-cost:   32
c ---[ 122]---> BDD-cost:   26
c ---[ 121]---> BDD-cost:   20
c ---[ 120]---> BDD-cost:   18
c ---[ 118]---> BDD-cost:    7
c ---[ 117]---> BDD-cost:    5
c ---[ 116]---> BDD-cost:   29
c ---[ 115]---> BDD-cost:   32
c ---[ 114]---> BDD-cost:   38
c ---[ 113]---> BDD-cost:   44
c ---[ 112]---> BDD-cost:   50
c ---[ 111]---> BDD-cost:   41
c ---[ 110]---> BDD-cost:   42
c ---[ 109]---> BDD-cost:   38
c ---[ 108]---> BDD-cost:   41
c ---[ 107]---> BDD-cost:   35
c ---[ 106]---> BDD-cost:   38
c ---[ 105]---> BDD-cost:   38
c ---[ 104]---> BDD-cost:   35
c ---[ 103]---> BDD-cost:   32
c ---[ 102]---> BDD-cost:   26
c ---[ 101]---> BDD-cost:   23
c ---[ 100]---> BDD-cost:   26
c ---[  99]---> BDD-cost:   17
c ---[  98]---> BDD-cost:   17
c ---[  97]---> BDD-cost:    5
c ---[  96]---> BDD-cost:   23
c ---[  95]---> BDD-cost:   35
c ---[  94]---> BDD-cost:   41
c ---[  93]---> BDD-cost:   41
c ---[  92]---> BDD-cost:   47
c ---[  91]---> BDD-cost:   50
c ---[  90]---> BDD-cost:   53
c ---[  89]---> BDD-cost:   47
c ---[  88]---> BDD-cost:   38
c ---[  87]---> BDD-cost:   38
c ---[  86]---> BDD-cost:   35
c ---[  85]---> BDD-cost:   32
c ---[  84]---> BDD-cost:   32
c ---[  83]---> BDD-cost:   29
c ---[  82]---> BDD-cost:   32
c ---[  81]---> BDD-cost:   32
c ---[  80]---> BDD-cost:   26
c ---[  79]---> BDD-cost:   20
c ---[  78]---> BDD-cost:   14
c ---[  77]---> BDD-cost:    8
c ---[  76]---> BDD-cost:   23
c ---[  75]---> BDD-cost:   29
c ---[  74]---> BDD-cost:   32
c ---[  73]---> BDD-cost:   41
c ---[  72]---> BDD-cost:   41
c ---[  71]---> BDD-cost:   47
c ---[  70]---> BDD-cost:   44
c ---[  69]---> BDD-cost:   44
c ---[  68]---> BDD-cost:   26
c ---[  67]---> BDD-cost:   32
c ---[  66]---> BDD-cost:   32
c ---[  65]---> BDD-cost:   32
c ---[  64]---> BDD-cost:   33
c ---[  63]---> BDD-cost:   32
c ---[  62]---> BDD-cost:   26
c ---[  61]---> BDD-cost:   29
c ---[  60]---> BDD-cost:   23
c ---[  59]---> BDD-cost:   20
c ---[  58]---> BDD-cost:   14
c ---[  57]---> BDD-cost:    5
c ---[  56]---> BDD-cost:   17
c ---[  55]---> BDD-cost:   26
c ---[  54]---> BDD-cost:   23
c ---[  53]---> BDD-cost:   29
c ---[  52]---> BDD-cost:   32
c ---[  51]---> BDD-cost:   38
c ---[  50]---> BDD-cost:   32
c ---[  49]---> BDD-cost:   35
c ---[  48]---> BDD-cost:   26
c ---[  47]---> BDD-cost:   26
c ---[  46]---> BDD-cost:   26
c ---[  45]---> BDD-cost:   29
c ---[  44]---> BDD-cost:   26
c ---[  43]---> BDD-cost:   29
c ---[  42]---> BDD-cost:   20
c ---[  41]---> BDD-cost:   20
c ---[  40]---> BDD-cost:   14
c ---[  39]---> BDD-cost:   18
c ---[  36]---> BDD-cost:   11
c ---[  35]---> BDD-cost:   17
c ---[  34]---> BDD-cost:   20
c ---[  33]---> BDD-cost:   23
c ---[  32]---> BDD-cost:   26
c ---[  31]---> BDD-cost:   29
c ---[  30]---> BDD-cost:   23
c ---[  29]---> BDD-cost:   26
c ---[  28]---> BDD-cost:   20
c ---[  27]---> BDD-cost:   23
c ---[  26]---> BDD-cost:   26
c ---[  25]---> BDD-cost:   26
c ---[  24]---> BDD-cost:   14
c ---[  23]---> BDD-cost:   14
c ---[  22]---> BDD-cost:   14
c ---[  21]---> BDD-cost:   15
c ---[  20]---> BDD-cost:    9
c ---[  18]---> BDD-cost:    5
c ---[  17]---> BDD-cost:   14
c ---[  16]---> BDD-cost:   14
c ---[  15]---> BDD-cost:   23
c ---[  14]---> BDD-cost:   20
c ---[  13]---> BDD-cost:   20
c ---[  12]---> BDD-cost:   17
c ---[  11]---> BDD-cost:   20
c ---[  10]---> BDD-cost:   17
c ---[   9]---> BDD-cost:   20
c ---[   8]---> BDD-cost:   11
c ---[   7]---> BDD-cost:   17
c ---[   6]---> BDD-cost:   14
c ---[   5]---> BDD-cost:   14
c ---[   4]---> BDD-cost:   14
c ---[   3]---> BDD-cost:    7
c ---[   2]---> BDD-cost:    8
c ---[   1]---> BDD-cost:    7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   11765    33737 |    3529       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5466          
c   -- var.elim.:  2000/5466          
c   -- var.elim.:  3000/5466          
c   -- var.elim.:  4000/5466          
c   -- var.elim.:  5000/5466          
c   -- var.elim.:  5466/5466          
c   -- var.elim.:  1000/2642          
c   -- var.elim.:  2000/2642          
c   -- var.elim.:  2642/2642          
c   -- subsuming                       
c   -- var.elim.:  1000/2450          
c   -- var.elim.:  2000/2450          
c   -- var.elim.:  2450/2450          
c   -- var.elim.:  1000/1264          
c   -- var.elim.:  1264/1264          
c   -- subsuming                       
c   -- var.elim.:  5/5          
c   -- var.elim.:  4/4          
c |         0 |    8805    32627 |      --       0       --      -- |     --   | -2960/-561
c |         0 |    8805    32627 |    3522       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.631903 s)
c ==============================================================================
c [1mFound solution: 1013[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2083   maxlim: 489   bits: 10/9
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   23289    84329 |    6986       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3021          
c   -- var.elim.:  2000/3021          
c   -- var.elim.:  3000/3021          
c   -- var.elim.:  3021/3021          
c   -- var.elim.:  39/39          
c |         0 |   23144    83638 |      --       0       --      -- |     --   | -145/-685
c |         0 |   23144    83638 |    9257       0        0     nan |  0.000 % |
c |       100 |   23144    83638 |   10183     100      679     6.8 |  3.226 % |
c |       250 |   23144    83638 |   11201     250     1336     5.3 |  3.226 % |
c |       476 |   23144    83638 |   12321     476     2639     5.5 |  3.226 % |
c ==============================================================================
c (current CPU-time: 1.55576 s)
c ==============================================================================
c [1mFound solution: 149[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 6   maxlim: 1353   bits: 12/11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       561 |   23207    83850 |    6962     561     3206     5.7 |  3.226 % |
c   -- subsuming                       
c   -- var.elim.:  42/42          
c   -- var.elim.:  16/16          
c |       561 |   23195    83835 |      --     561       --      -- |     --   | -12/-10
c |       561 |   23195    83835 |    9278     561     3206     5.7 |  3.226 % |
c |       661 |   23195    83835 |   10205     661     3948     6.0 |  3.304 % |
c |       811 |   23195    83835 |   11226     811     4932     6.1 |  3.304 % |
c |      1037 |   23195    83835 |   12349    1037     6213     6.0 |  3.304 % |
c |      1375 |   23195    83835 |   13583    1375    10382     7.6 |  3.304 % |
c |      1881 |   23195    83835 |   14942    1881    12600     6.7 |  3.304 % |
c |      2640 |   23195    83835 |   16436    2640    42804    16.2 |  3.304 % |
c ==============================================================================
c (current CPU-time: 3.40548 s)
c ==============================================================================
c [1mFound solution: 148[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1354   bits: 12/11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2802 |   23222    83930 |    6966    2802    44656    15.9 |  3.304 % |
c   -- subsuming                       
c   -- var.elim.:  29/29          
c   -- var.elim.:  17/17          
c   -- var.elim.:  14/14          
c |      2802 |   23210    83925 |      --    2802       --      -- |     --   | -12/-4
c |      2802 |   23210    83925 |    9284    2802    44656    15.9 |  3.304 % |
c |      2902 |   23210    83925 |   10212    2902    45261    15.6 |  3.319 % |
c ==============================================================================
c (current CPU-time: 3.81742 s)
c ==============================================================================
c [1mFound solution: 131[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1371   bits: 12/11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2989 |   23229    83999 |    6968    2989    45888    15.4 |  3.319 % |
c   -- subsuming                       
c   -- var.elim.:  23/23          
c   -- var.elim.:  13/13          
c |      2989 |   23222    83977 |      --    2989       --      -- |     --   | -7/-19
c |      2989 |   23222    83977 |    9288    2989    45888    15.4 |  3.319 % |
c ==============================================================================
c (current CPU-time: 4.11337 s)
c ==============================================================================
c [1mFound solution: 127[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1375   bits: 12/11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3026 |   23223    83985 |    6966    3026    46059    15.2 |  3.319 % |
c   -- subsuming                       
c   -- var.elim.:  18/18          
c   -- var.elim.:  9/9          
c |      3026 |   23216    83951 |      --    3026       --      -- |     --   | -3/1
c |      3026 |   23216    83951 |    9286    3026    46059    15.2 |  3.319 % |
c |      3126 |   23216    83951 |   10215    3126    47744    15.3 |  3.384 % |
c |      3276 |   23216    83951 |   11236    3276    49254    15.0 |  3.384 % |
c |      3502 |   23216    83951 |   12360    3502    50678    14.5 |  3.384 % |
c |      3841 |   23216    83951 |   13596    3841    54496    14.2 |  3.384 % |
c |      4347 |   23216    83951 |   14955    4347    64607    14.9 |  3.384 % |
c |      5106 |   23216    83951 |   16451    5106    77748    15.2 |  3.384 % |
c |      6245 |   23216    83951 |   18096    6245    98889    15.8 |  3.384 % |
c |      7953 |   23216    83951 |   19906    7953   192928    24.3 |  3.384 % |
c |     10517 |   23216    83951 |   21896   10517   352429    33.5 |  3.384 % |
c ==============================================================================
c (current CPU-time: 9.2236 s)
c ==============================================================================
c [1mFound solution: 126[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1376   bits: 12/11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     10622 |   23235    84014 |    6970   10622   354458    33.4 |  3.384 % |
c   -- subsuming                       
c   -- var.elim.:  26/26          
c   -- var.elim.:  19/19          
c |     10622 |   23224    84030 |      --   10622       --      -- |     --   | -11/17
c |     10622 |   23224    84030 |    9289   10622   354458    33.4 |  3.384 % |
c |     10722 |   23224    84030 |   10218    7182   280744    39.1 |  3.400 % |
c |     10873 |   23224    84030 |   11240    7333   282054    38.5 |  3.400 % |
c |     11098 |   23224    84030 |   12364    7558   291514    38.6 |  3.400 % |
c |     11435 |   23224    84030 |   13600    7895   297338    37.7 |  3.400 % |
c ==============================================================================
c (current CPU-time: 10.1835 s)
c ==============================================================================
c [1mFound solution: 113[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1389   bits: 12/11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     11510 |   23236    84089 |    6970    7970   297958    37.4 |  3.400 % |
c   -- subsuming                       
c   -- var.elim.:  24/24          
c   -- var.elim.:  17/17          
c |     11510 |   23223    84059 |      --    7970       --      -- |     --   | -13/-27
c |     11510 |   23223    84059 |    9289    7970   297958    37.4 |  3.400 % |
c |     11611 |   23223    84059 |   10218    8071   300151    37.2 |  3.449 % |
c |     11761 |   23223    84059 |   11239    8221   301355    36.7 |  3.449 % |
c |     11986 |   23223    84059 |   12363    8446   309613    36.7 |  3.449 % |
c |     12323 |   23223    84059 |   13600    8783   321903    36.7 |  3.449 % |
c |     12830 |   23223    84059 |   14960    9290   334528    36.0 |  3.449 % |
c |     13590 |   23223    84059 |   16456   10050   359498    35.8 |  3.449 % |
c |     14729 |   23223    84059 |   18102   11189   445849    39.8 |  3.449 % |
c |     16437 |   23223    84059 |   19912   12897   547347    42.4 |  3.449 % |
c ==============================================================================
c (current CPU-time: 14.0669 s)
c ==============================================================================
c [1mFound solution: 106[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1396   bits: 12/11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     17405 |   23242    84148 |    6972   13865   589759    42.5 |  3.449 % |
c   -- subsuming                       
c   -- var.elim.:  21/21          
c   -- var.elim.:  14/14          
c |     17405 |   23233    84114 |      --   13865       --      -- |     --   | -4/22
c |     17405 |   23233    84114 |    9293   13865   589759    42.5 |  3.449 % |
c |     17505 |   23233    84114 |   10222    9344   335541    35.9 |  3.498 % |
c |     17656 |   23233    84114 |   11244    9495   337034    35.5 |  3.498 % |
c |     17882 |   23233    84114 |   12369    9721   341821    35.2 |  3.498 % |
c |     18219 |   23233    84114 |   13606   10058   351061    34.9 |  3.498 % |
c |     18726 |   23233    84114 |   14966   10565   364148    34.5 |  3.498 % |
c |     19485 |   23233    84114 |   16463   11324   390820    34.5 |  3.498 % |
c |     20626 |   23233    84114 |   18109   12465   449901    36.1 |  3.498 % |
c |     22336 |   23233    84114 |   19920   14175   533235    37.6 |  3.498 % |
c |     24898 |   23233    84114 |   21912   16737   715170    42.7 |  3.498 % |
c |     28743 |   23233    84114 |   24104   20582   923473    44.9 |  3.498 % |
c |     34509 |   23233    84114 |   26514   26348  1597683    60.6 |  3.498 % |
c |     43161 |   23233    84114 |   29166   20267  1672986    82.5 |  3.498 % |
c |     56135 |   23233    84114 |   32082   12969  2044133   157.6 |  3.498 % |
c |     75596 |   23233    84114 |   35290   32430  4654816   143.5 |  3.498 % |
c |    104788 |   23233    84114 |   38820   38918  4215924   108.3 |  3.498 % |
c |    148577 |   23233    84114 |   42702   30051  3910902   130.1 |  3.498 % |
c |    214263 |   23233    84114 |   46972   30311  4203116   138.7 |  3.498 % |
c |    312792 |   23233    84114 |   51669   24606  5771922   234.6 |  3.498 % |
c |    460581 |   23233    84114 |   56836   17623  4226673   239.8 |  3.498 % |
c ==============================================================================
c (current CPU-time: 1027.28 s)
c ==============================================================================
c [1mFound solution: 104[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1398   bits: 12/11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    477766 |   23243    84163 |    6972   34808  5914625   169.9 |  3.498 % |
c   -- subsuming                       
c   -- var.elim.:  18/18          
c   -- var.elim.:  14/14          
c |    477766 |   23239    84168 |      --   34808       --      -- |     --   | -4/7
c |    477766 |   23239    84168 |    9295   34808  5914625   169.9 |  3.498 % |
c |    477867 |   23239    84168 |   10225    9026   761323    84.3 |  3.530 % |
c |    478017 |   23239    84168 |   11247    9176   761973    83.0 |  3.530 % |
c |    478242 |   23239    84168 |   12372    9401   764010    81.3 |  3.530 % |
c |    478580 |   23239    84168 |   13609    9739   765871    78.6 |  3.530 % |
c |    479086 |   23239    84168 |   14970   10245   769818    75.1 |  3.530 % |
c |    479845 |   23239    84168 |   16467   11004   805144    73.2 |  3.530 % |
c |    480984 |   23239    84168 |   18114   12143   822512    67.7 |  3.530 % |
c |    482692 |   23239    84168 |   19925   13851   995522    71.9 |  3.530 % |
c |    485254 |   23239    84168 |   21918   16413  1255524    76.5 |  3.530 % |
c |    489098 |   23239    84168 |   24110   20257  1589965    78.5 |  3.530 % |
c |    494864 |   23239    84168 |   26521   14230  1062650    74.7 |  3.530 % |
c |    503515 |   23239    84168 |   29173   22881  1697846    74.2 |  3.530 % |
c |    516490 |   23239    84168 |   32090   18767  1535378    81.8 |  3.530 % |
c |    535951 |   23239    84168 |   35300   17770  2753117   154.9 |  3.530 % |
c |    565144 |   23239    84168 |   38830   20888  2493249   119.4 |  3.530 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -v853 v782 -v197 -v102 v21 v2 -v855 -v103 v1 v785 -v384 -v272 -v196 v20 v3 -v856 v786 v76 -v55 -v23 v4 -v383 -v275 v202 v75 -v54 -v11 -v763 -v387 -v276 v200 -v56 -v24 v5 -v762 -v247 -v150 v77 -v57 v26 -v6 -v764 v613 -v388 v201 -v79 -v58 -v39 v27 -v7 -v765 v612 -v513 v250 -v205 -v149 -v65 v38 v766 -v618 v251 -v80 -v59 v40 -v773 -v617 -v512 v326 -v155 v125 -v82 -v60 v41 -v767 v619 -v153 -v83 -v61 v42 -v768 v623 v593 -v573 -v518 v128 -v49 -v769 v622 -v577 -v516 -v154 -v129 v43 -v729 v620 v596 -v576 -v158 v44 v621 v597 -v517 v45 v881 -v728 -v521 -v852 v781 v192 -v104 -v17 -v857 v787 -v537 -v468 -v271 -v198 v22 v14 -v541 -v71 v25 v15 -v859 -v385 -v277 v203 -v108 -v70 v29 -v10 -v860 -v389 v28 -v790 -v246 v206 -v145 v78 -v68 -v8 -v204 v81 -v69 -v811 -v776 -v638 -v508 -v391 -v322 -v280 v252 -v151 -v85 -v64 -v777 -v642 v614 -v392 -v84 -v772 v615 -v514 v325 -v156 v124 -v62 v52 v616 v53 -v770 v627 v592 -v519 -v255 -v159 v130 -v48 -v572 -v157 -v877 v598 -v574 -v522 -v46 -v578 -v520 v880 -v730 v133 v601 -v854 v783 -v464 -v267 -v105 v13 -v858 -v379 v191 -v16 v12 -v862 v788 -v536 -v488 -v467 -v378 -v273 v193 -v109 -v18 -v861 -v540 -v492 -v199 -v107 v19 -v791 -v386 -v278 v242 v195 -v67 v33 -v789 v390 v207 -v72 -v66 -v807 -v775 -v394 v301 -v281 -v248 -v73 -v9 -v774 -v393 -v279 -v144 v74 -v810 -v637 -v321 v253 -v146 -v120 -v89 v51 -v641 -v507 -v152 v50 v630 -v588 -v509 v327 v256 -v148 v126 -v63 v631 -v515 v254 -v160 -v771 v626 v594 -v511 v131 -v725 -v523 v876 -v724 v709 v624 v59#### 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.93 0.98 0.93 2/55 27780
Raw data (stat): 27780 (runsolver) R 27779 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480598539 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+9.99967 s]
Raw data (loadavg): 0.94 0.98 0.93 2/55 27780
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 3631 0 0 0 986 12 0 0 25 0 1 0 480598539 13553664 2777 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3309 2777 603 41 0 3268 0
vsize: 13236
[startup+20.0001 s]
Raw data (loadavg): 0.95 0.98 0.93 2/55 27780
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 4244 0 0 0 1984 14 0 0 25 0 1 0 480598539 15380480 3195 4294967295 134512640 134672761 3221224544 3221223464 1075347210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3755 3195 603 41 0 3714 0
vsize: 15020
[startup+30.0003 s]
Raw data (loadavg): 0.95 0.98 0.93 2/55 27780
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 5408 0 0 0 2981 17 0 0 25 0 1 0 480598539 20168704 4359 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4924 4359 603 41 0 4883 0
vsize: 19696
[startup+40.0001 s]
Raw data (loadavg): 0.96 0.98 0.93 2/55 27780
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 5814 0 0 0 3980 18 0 0 25 0 1 0 480598539 21753856 4765 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5311 4765 603 41 0 5270 0
vsize: 21244
[startup+50.0012 s]
Raw data (loadavg): 0.97 0.98 0.93 2/55 27780
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 7144 0 0 0 4976 22 0 0 25 0 1 0 480598539 27164672 6095 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6632 6095 603 41 0 6591 0
vsize: 26528
[startup+60.0008 s]
Raw data (loadavg): 0.97 0.98 0.93 2/55 27780
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 7565 0 0 0 5975 23 0 0 25 0 1 0 480598539 29278208 6516 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7148 6516 603 41 0 7107 0
vsize: 28592
[startup+70.0005 s]
Raw data (loadavg): 0.97 0.98 0.93 2/55 27780
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 7565 0 0 0 6975 23 0 0 25 0 1 0 480598539 29278208 6516 4294967295 134512640 134672761 3221224544 3221223728 134615567 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7148 6516 603 41 0 7107 0
vsize: 28592
[startup+80.0017 s]
Raw data (loadavg): 0.98 0.98 0.93 2/55 27780
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 8440 0 0 0 7974 25 0 0 25 0 1 0 480598539 32698368 7391 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7983 7391 603 41 0 7942 0
vsize: 31932
[startup+90.0011 s]
Raw data (loadavg): 0.98 0.98 0.93 2/55 27780
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 8882 0 0 0 8972 26 0 0 25 0 1 0 480598539 34246656 7796 4294967295 134512640 134672761 3221224544 3221223728 134615773 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8361 7796 603 41 0 8320 0
vsize: 33444
[startup+100.001 s]
Raw data (loadavg): 0.98 0.98 0.93 2/55 27780
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 8882 0 0 0 9972 26 0 0 25 0 1 0 480598539 34246656 7796 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8361 7796 603 41 0 8320 0
vsize: 33444
[startup+110.001 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27780
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 8882 0 0 0 10972 26 0 0 25 0 1 0 480598539 34246656 7796 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8361 7796 603 41 0 8320 0
vsize: 33444
[startup+120.001 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27780
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 8928 0 0 0 11972 27 0 0 25 0 1 0 480598539 34242560 7802 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8360 7802 603 41 0 8319 0
vsize: 33440
[startup+130 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27780
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 8928 0 0 0 12972 27 0 0 25 0 1 0 480598539 34242560 7802 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8360 7802 603 41 0 8319 0
vsize: 33440
[startup+140.001 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27780
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 8928 0 0 0 13972 27 0 0 25 0 1 0 480598539 34242560 7802 4294967295 134512640 134672761 3221224544 3221223728 134616004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8360 7802 603 41 0 8319 0
vsize: 33440
[startup+150.001 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27780
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 8969 0 0 0 14972 27 0 0 25 0 1 0 480598539 34504704 7843 4294967295 134512640 134672761 3221224544 3221223640 134616263 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8424 7843 603 41 0 8383 0
vsize: 33696
[startup+160.001 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27782
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 8969 0 0 0 15973 27 0 0 25 0 1 0 480598539 34242560 7803 4294967295 134512640 134672761 3221224544 3221223728 134615711 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8360 7803 603 41 0 8319 0
vsize: 33440
[startup+170.001 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27782
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 8969 0 0 0 16973 27 0 0 25 0 1 0 480598539 34242560 7803 4294967295 134512640 134672761 3221224544 3221223584 134603552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8360 7803 603 41 0 8319 0
vsize: 33440
[startup+180.001 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27782
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 8969 0 0 0 17972 27 0 0 25 0 1 0 480598539 34242560 7803 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8360 7803 603 41 0 8319 0
vsize: 33440
[startup+190.001 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27782
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 9933 0 0 0 18970 30 0 0 25 0 1 0 480598539 38203392 8767 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9327 8767 603 41 0 9286 0
vsize: 37308
[startup+200.001 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27782
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 10989 0 0 0 19967 33 0 0 25 0 1 0 480598539 42557440 9823 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10390 9823 603 41 0 10349 0
vsize: 41560
[startup+210.001 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27782
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 11301 0 0 0 20966 34 0 0 25 0 1 0 480598539 43696128 10089 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10668 10089 603 41 0 10627 0
vsize: 42672
[startup+220.001 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27782
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 11301 0 0 0 21966 34 0 0 25 0 1 0 480598539 43696128 10089 4294967295 134512640 134672761 3221224544 3221223536 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10668 10089 603 41 0 10627 0
vsize: 42672
[startup+230.001 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27782
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 11301 0 0 0 22967 34 0 0 25 0 1 0 480598539 43696128 10089 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10668 10089 603 41 0 10627 0
vsize: 42672
[startup+240 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27782
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 11301 0 0 0 23967 34 0 0 25 0 1 0 480598539 43696128 10089 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10668 10089 603 41 0 10627 0
vsize: 42672
[startup+250 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27782
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 11301 0 0 0 24967 34 0 0 25 0 1 0 480598539 43696128 10089 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10668 10089 603 41 0 10627 0
vsize: 42672
[startup+260 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27782
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 11813 0 0 0 25965 36 0 0 25 0 1 0 480598539 45817856 10601 4294967295 134512640 134672761 3221224544 3221223416 1075353266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11186 10601 603 41 0 11145 0
vsize: 44744
[startup+270 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27782
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 12716 0 0 0 26963 38 0 0 25 0 1 0 480598539 49508352 11504 4294967295 134512640 134672761 3221224544 3221223584 134614256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12087 11504 603 41 0 12046 0
vsize: 48348
[startup+280 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27782
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 13476 0 0 0 27962 40 0 0 25 0 1 0 480598539 52678656 12264 4294967295 134512640 134672761 3221224544 3221223632 134605969 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12861 12264 603 41 0 12820 0
vsize: 51444
[startup+290 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27782
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 13476 0 0 0 28962 40 0 0 25 0 1 0 480598539 52416512 12218 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12797 12218 603 41 0 12756 0
vsize: 51188
[startup+300 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27782
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 13476 0 0 0 29962 40 0 0 25 0 1 0 480598539 52416512 12218 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12797 12218 603 41 0 12756 0
vsize: 51188
[startup+310 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27782
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 13476 0 0 0 30962 40 0 0 25 0 1 0 480598539 52416512 12218 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12797 12218 603 41 0 12756 0
vsize: 51188
[startup+320 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27782
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 13476 0 0 0 31962 40 0 0 25 0 1 0 480598539 52416512 12218 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12797 12218 603 41 0 12756 0
vsize: 51188
[startup+330.001 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27782
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 13530 0 0 0 32962 40 0 0 25 0 1 0 480598539 52416512 12223 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12797 12223 603 41 0 12756 0
vsize: 51188
[startup+340 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27782
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 13530 0 0 0 33962 40 0 0 25 0 1 0 480598539 52416512 12223 4294967295 134512640 134672761 3221224544 3221223584 134612606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12797 12223 603 41 0 12756 0
vsize: 51188
[startup+350.001 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27782
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 13530 0 0 0 34962 40 0 0 25 0 1 0 480598539 52416512 12223 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12797 12223 603 41 0 12756 0
vsize: 51188
[startup+360.001 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27782
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 13530 0 0 0 35963 40 0 0 25 0 1 0 480598539 52416512 12223 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12797 12223 603 41 0 12756 0
vsize: 51188
[startup+370.001 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27782
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 13530 0 0 0 36963 40 0 0 25 0 1 0 480598539 52416512 12223 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12797 12223 603 41 0 12756 0
vsize: 51188
[startup+380.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27782
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 13530 0 0 0 37963 40 0 0 25 0 1 0 480598539 52416512 12223 4294967295 134512640 134672761 3221224544 3221223536 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12797 12223 603 41 0 12756 0
vsize: 51188
[startup+390.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27782
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 13530 0 0 0 38963 40 0 0 25 0 1 0 480598539 52416512 12223 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12797 12223 603 41 0 12756 0
vsize: 51188
[startup+400.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27782
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 13530 0 0 0 39963 40 0 0 25 0 1 0 480598539 52416512 12223 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12797 12223 603 41 0 12756 0
vsize: 51188
[startup+410.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27782
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 13579 0 0 0 40963 41 0 0 25 0 1 0 480598539 52416512 12223 4294967295 134512640 134672761 3221224544 3221223536 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12797 12223 603 41 0 12756 0
vsize: 51188
[startup+420.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27782
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 13579 0 0 0 41963 41 0 0 25 0 1 0 480598539 52416512 12223 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12797 12223 603 41 0 12756 0
vsize: 51188
[startup+430.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27782
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 13579 0 0 0 42963 41 0 0 25 0 1 0 480598539 52416512 12223 4294967295 134512640 134672761 3221224544 3221223584 134612604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12797 12223 603 41 0 12756 0
vsize: 51188
[startup+440.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27782
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 13579 0 0 0 43964 41 0 0 25 0 1 0 480598539 52416512 12223 4294967295 134512640 134672761 3221224544 3221223728 134616017 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12797 12223 603 41 0 12756 0
vsize: 51188
[startup+450.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27782
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 13579 0 0 0 44964 41 0 0 25 0 1 0 480598539 52416512 12223 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12797 12223 603 41 0 12756 0
vsize: 51188
[startup+460.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27784
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 13579 0 0 0 45964 41 0 0 25 0 1 0 480598539 52416512 12223 4294967295 134512640 134672761 3221224544 3221223712 134615864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12797 12223 603 41 0 12756 0
vsize: 51188
[startup+470.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27784
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 13579 0 0 0 46964 41 0 0 25 0 1 0 480598539 52416512 12223 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12797 12223 603 41 0 12756 0
vsize: 51188
[startup+480.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27784
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 13579 0 0 0 47964 41 0 0 25 0 1 0 480598539 52416512 12223 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12797 12223 603 41 0 12756 0
vsize: 51188
[startup+490.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27784
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 13579 0 0 0 48964 41 0 0 25 0 1 0 480598539 52416512 12223 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12797 12223 603 41 0 12756 0
vsize: 51188
[startup+500.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27784
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 14327 0 0 0 49962 44 0 0 25 0 1 0 480598539 55586816 12971 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13571 12971 603 41 0 13530 0
vsize: 54284
[startup+510.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27784
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 14962 0 0 0 50961 45 0 0 25 0 1 0 480598539 58089472 13606 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14182 13606 603 41 0 14141 0
vsize: 56728
[startup+520.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27784
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 15538 0 0 0 51959 47 0 0 25 0 1 0 480598539 60465152 14182 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14762 14182 603 41 0 14721 0
vsize: 59048
[startup+530.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27784
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 15851 0 0 0 52959 47 0 0 25 0 1 0 480598539 61661184 14477 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14477 603 41 0 15013 0
vsize: 60216
[startup+540.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27784
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 15851 0 0 0 53959 47 0 0 25 0 1 0 480598539 61661184 14477 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14477 603 41 0 15013 0
vsize: 60216
[startup+550.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27784
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 15853 0 0 0 54959 48 0 0 25 0 1 0 480598539 61661184 14479 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14479 603 41 0 15013 0
vsize: 60216
[startup+560.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27784
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 15854 0 0 0 55959 48 0 0 25 0 1 0 480598539 61661184 14480 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14480 603 41 0 15013 0
vsize: 60216
[startup+570.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27784
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 15854 0 0 0 56959 48 0 0 25 0 1 0 480598539 61661184 14480 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14480 603 41 0 15013 0
vsize: 60216
[startup+580.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27784
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 15854 0 0 0 57958 48 0 0 25 0 1 0 480598539 61661184 14480 4294967295 134512640 134672761 3221224544 3221223552 134522368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15054 14480 603 41 0 15013 0
vsize: 60216
[startup+590.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27784
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 15854 0 0 0 58959 48 0 0 25 0 1 0 480598539 61661184 14480 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14480 603 41 0 15013 0
vsize: 60216
[startup+600.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27784
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 15854 0 0 0 59959 48 0 0 25 0 1 0 480598539 61661184 14480 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14480 603 41 0 15013 0
vsize: 60216
[startup+610.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27784
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 15854 0 0 0 60959 48 0 0 25 0 1 0 480598539 61661184 14480 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14480 603 41 0 15013 0
vsize: 60216
[startup+620.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27784
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 15857 0 0 0 61959 48 0 0 25 0 1 0 480598539 61661184 14483 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14483 603 41 0 15013 0
vsize: 60216
[startup+630.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27784
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 16400 0 0 0 62958 49 0 0 25 0 1 0 480598539 63774720 15004 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15570 15004 603 41 0 15529 0
vsize: 62280
[startup+640.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27784
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 16400 0 0 0 63958 49 0 0 25 0 1 0 480598539 63774720 15004 4294967295 134512640 134672761 3221224544 3221223728 134615505 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15570 15004 603 41 0 15529 0
vsize: 62280
[startup+650.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27784
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 16400 0 0 0 64958 49 0 0 25 0 1 0 480598539 63774720 15004 4294967295 134512640 134672761 3221224544 3221223312 1075352340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15570 15004 603 41 0 15529 0
vsize: 62280
[startup+660.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27784
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 16400 0 0 0 65958 50 0 0 25 0 1 0 480598539 63774720 15004 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15570 15004 603 41 0 15529 0
vsize: 62280
[startup+670.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27784
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 16400 0 0 0 66958 50 0 0 25 0 1 0 480598539 63774720 15004 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15570 15004 603 41 0 15529 0
vsize: 62280
[startup+680.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27784
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 16400 0 0 0 67958 50 0 0 25 0 1 0 480598539 63774720 15004 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15570 15004 603 41 0 15529 0
vsize: 62280
[startup+690.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27784
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 16400 0 0 0 68959 50 0 0 25 0 1 0 480598539 63774720 15004 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15570 15004 603 41 0 15529 0
vsize: 62280
[startup+700.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27784
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 16400 0 0 0 69959 50 0 0 25 0 1 0 480598539 63774720 15004 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15570 15004 603 41 0 15529 0
vsize: 62280
[startup+710.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27784
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 16400 0 0 0 70959 50 0 0 25 0 1 0 480598539 63774720 15004 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15570 15004 603 41 0 15529 0
vsize: 62280
[startup+720.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27784
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 16403 0 0 0 71959 50 0 0 25 0 1 0 480598539 63766528 15005 4294967295 134512640 134672761 3221224544 3221223640 134616183 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15568 15005 603 41 0 15527 0
vsize: 62272
[startup+730.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27784
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 16403 0 0 0 72959 50 0 0 25 0 1 0 480598539 63766528 15005 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15568 15005 603 41 0 15527 0
vsize: 62272
[startup+740.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27784
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 16403 0 0 0 73959 50 0 0 25 0 1 0 480598539 63766528 15005 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15568 15005 603 41 0 15527 0
vsize: 62272
[startup+750.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27784
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 16403 0 0 0 74959 50 0 0 25 0 1 0 480598539 63766528 15005 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15568 15005 603 41 0 15527 0
vsize: 62272
[startup+760.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27786
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 16403 0 0 0 75959 50 0 0 25 0 1 0 480598539 63766528 15005 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15568 15005 603 41 0 15527 0
vsize: 62272
[startup+770.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27786
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 16403 0 0 0 76959 50 0 0 25 0 1 0 480598539 63766528 15005 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15568 15005 603 41 0 15527 0
vsize: 62272
[startup+780.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27786
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 16403 0 0 0 77960 50 0 0 25 0 1 0 480598539 63766528 15005 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15568 15005 603 41 0 15527 0
vsize: 62272
[startup+790.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27786
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 16403 0 0 0 78960 50 0 0 25 0 1 0 480598539 63766528 15005 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15568 15005 603 41 0 15527 0
vsize: 62272
[startup+800.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27786
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 16403 0 0 0 79960 50 0 0 25 0 1 0 480598539 63766528 15005 4294967295 134512640 134672761 3221224544 3221223584 134612992 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15568 15005 603 41 0 15527 0
vsize: 62272
[startup+810.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27786
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 16501 0 0 0 80960 50 0 0 25 0 1 0 480598539 64290816 15103 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15696 15103 603 41 0 15655 0
vsize: 62784
[startup+820.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27786
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 17541 0 0 0 81958 53 0 0 25 0 1 0 480598539 68481024 16143 4294967295 134512640 134672761 3221224544 3221223584 134612630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16719 16144 603 41 0 16678 0
vsize: 66876
[startup+830.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27786
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 18538 0 0 0 82956 55 0 0 25 0 1 0 480598539 72540160 17140 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17710 17140 603 41 0 17669 0
vsize: 70840
[startup+840.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27786
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 19157 0 0 0 83955 56 0 0 25 0 1 0 480598539 75202560 17759 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18360 17759 603 41 0 18319 0
vsize: 73440
[startup+850.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27786
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 19835 0 0 0 84953 58 0 0 25 0 1 0 480598539 77975552 18437 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19037 18437 603 41 0 18996 0
vsize: 76148
[startup+860.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27786
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 20538 0 0 0 85951 60 0 0 25 0 1 0 480598539 80744448 19140 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19713 19140 603 41 0 19672 0
vsize: 78852
[startup+870.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27786
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 21223 0 0 0 86949 63 0 0 25 0 1 0 480598539 83660800 19825 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20425 19825 603 41 0 20384 0
vsize: 81700
[startup+880.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27786
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 21818 0 0 0 87948 64 0 0 25 0 1 0 480598539 85753856 20366 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20936 20366 603 41 0 20895 0
vsize: 83744
[startup+890.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27786
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 21818 0 0 0 88948 64 0 0 25 0 1 0 480598539 85753856 20366 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20936 20366 603 41 0 20895 0
vsize: 83744
[startup+900.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27786
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 21818 0 0 0 89948 64 0 0 25 0 1 0 480598539 85753856 20366 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20936 20366 603 41 0 20895 0
vsize: 83744
[startup+910.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27786
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 21818 0 0 0 90948 64 0 0 25 0 1 0 480598539 85753856 20366 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20936 20366 603 41 0 20895 0
vsize: 83744
[startup+920.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27786
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 21818 0 0 0 91948 64 0 0 25 0 1 0 480598539 85753856 20366 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20936 20366 603 41 0 20895 0
vsize: 83744
[startup+930.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27786
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 21818 0 0 0 92948 64 0 0 25 0 1 0 480598539 85753856 20366 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20936 20366 603 41 0 20895 0
vsize: 83744
[startup+940.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27786
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 21818 0 0 0 93948 64 0 0 25 0 1 0 480598539 85753856 20366 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20936 20366 603 41 0 20895 0
vsize: 83744
[startup+950.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27786
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 21818 0 0 0 94949 65 0 0 25 0 1 0 480598539 85753856 20366 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20936 20366 603 41 0 20895 0
vsize: 83744
[startup+960.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27786
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 21818 0 0 0 95949 65 0 0 25 0 1 0 480598539 85753856 20366 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20936 20366 603 41 0 20895 0
vsize: 83744
[startup+970.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27786
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 21818 0 0 0 96949 65 0 0 25 0 1 0 480598539 85753856 20366 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20936 20366 603 41 0 20895 0
vsize: 83744
[startup+980.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27786
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 21818 0 0 0 97949 65 0 0 25 0 1 0 480598539 85753856 20366 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20936 20366 603 41 0 20895 0
vsize: 83744
[startup+990.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27786
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 21818 0 0 0 98949 65 0 0 25 0 1 0 480598539 85753856 20366 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20936 20366 603 41 0 20895 0
vsize: 83744
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27786
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 21819 0 0 0 99949 65 0 0 25 0 1 0 480598539 85753856 20367 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20936 20367 603 41 0 20895 0
vsize: 83744
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27786
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 21874 0 0 0 100949 65 0 0 25 0 1 0 480598539 85745664 20365 4294967295 134512640 134672761 3221224544 3221223680 134614727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20934 20365 603 41 0 20893 0
vsize: 83736
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27786
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 21874 0 0 0 101949 65 0 0 25 0 1 0 480598539 85745664 20365 4294967295 134512640 134672761 3221224544 3221223728 134615788 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20934 20365 603 41 0 20893 0
vsize: 83736
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27786
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 21880 0 0 0 102949 65 0 0 25 0 1 0 480598539 85745664 20371 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20934 20371 603 41 0 20893 0
vsize: 83736
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27786
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 21880 0 0 0 103949 65 0 0 25 0 1 0 480598539 85745664 20371 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20934 20371 603 41 0 20893 0
vsize: 83736
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27786
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 21880 0 0 0 104949 65 0 0 25 0 1 0 480598539 85745664 20371 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20934 20371 603 41 0 20893 0
vsize: 83736
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27788
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 21880 0 0 0 105949 65 0 0 25 0 1 0 480598539 85745664 20371 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20934 20371 603 41 0 20893 0
vsize: 83736
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27788
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 21880 0 0 0 106950 65 0 0 25 0 1 0 480598539 85745664 20371 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20934 20371 603 41 0 20893 0
vsize: 83736
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27788
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 21880 0 0 0 107950 65 0 0 25 0 1 0 480598539 85745664 20371 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20934 20371 603 41 0 20893 0
vsize: 83736
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27788
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 21880 0 0 0 108950 66 0 0 25 0 1 0 480598539 85745664 20371 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20934 20371 603 41 0 20893 0
vsize: 83736
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27788
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 21880 0 0 0 109950 66 0 0 25 0 1 0 480598539 85745664 20371 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20934 20371 603 41 0 20893 0
vsize: 83736
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27788
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 21880 0 0 0 110950 66 0 0 25 0 1 0 480598539 85745664 20371 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20934 20371 603 41 0 20893 0
vsize: 83736
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27788
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 21880 0 0 0 111950 66 0 0 25 0 1 0 480598539 85745664 20371 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20934 20371 603 41 0 20893 0
vsize: 83736
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27788
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 21880 0 0 0 112950 66 0 0 25 0 1 0 480598539 85745664 20371 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20934 20371 603 41 0 20893 0
vsize: 83736
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27788
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 21880 0 0 0 113950 66 0 0 25 0 1 0 480598539 85745664 20371 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20934 20371 603 41 0 20893 0
vsize: 83736
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27788
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 21880 0 0 0 114951 66 0 0 25 0 1 0 480598539 85745664 20371 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20934 20371 603 41 0 20893 0
vsize: 83736
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27788
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 21880 0 0 0 115951 66 0 0 25 0 1 0 480598539 85745664 20371 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20934 20371 603 41 0 20893 0
vsize: 83736
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27788
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 21880 0 0 0 116951 66 0 0 25 0 1 0 480598539 85745664 20371 4294967295 134512640 134672761 3221224544 3221223584 134614333 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20934 20371 603 41 0 20893 0
vsize: 83736
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27788
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 21880 0 0 0 117951 66 0 0 25 0 1 0 480598539 85745664 20371 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20934 20371 603 41 0 20893 0
vsize: 83736
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27788
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 21880 0 0 0 118951 66 0 0 25 0 1 0 480598539 85745664 20371 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20934 20371 603 41 0 20893 0
vsize: 83736
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 27788
Raw data (stat): 27780 (minisat+) R 27779 22929 22928 0 -1 0 21880 0 0 0 119951 66 0 0 25 0 1 0 480598539 85745664 20371 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20934 20371 603 41 0 20893 0
vsize: 83736
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.98 0.93 1/55 27788
Raw data (stat): 27780 (minisat+) Z 27779 22929 22928 0 -1 12 21881 0 0 0 119951 70 0 0 25 0 1 0 480598539 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.06
CPU time (s): 1200.23
CPU user time (s): 1199.52
CPU system time (s): 0.706892
CPU usage (%): 100.014
Max. virtual memory (Kb): 83744
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####