PB'05 competition: run trace

Some explanations

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

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

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc26 THE 2005-04-21 15:56:54 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17691 boxname=wulflinc26 idbench=1361 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a3dd3cd7dd293e24bffaff8bb73da54c  /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-misc07.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-misc07.opb /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-misc07.opb
IDLAUNCH: 17691
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        643448 kB
Buffers:         30620 kB
Cached:         332908 kB
SwapCached:         68 kB
Active:          48000 kB
Inactive:       318456 kB
HighTotal:      131008 kB
HighFree:         8708 kB
LowTotal:       903652 kB
LowFree:        634740 kB
SwapTotal:     2097892 kB
SwapFree:      2097800 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6876 kB
Slab:            18980 kB
Committed_AS:    63732 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 16:16:56 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 17691 7 1200.18 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 247 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###################################
c   -- Clauses(.)/Splits(s): ...............................................................................................................................
c ---[ 245]---> Adder-cost: 1695   maxlim: 1048703   bits: 22/21
c ---[ 244]---> BDD-cost:  239
c ---[ 233]---> BDD-cost:  239
c ---[ 200]---> Sorter-cost:  127     Base:
c ---[ 197]---> Sorter-cost:  127     Base:
c ---[ 195]---> Sorter-cost:  127     Base:
c ---[ 193]---> Sorter-cost:  127     Base:
c ---[ 191]---> Sorter-cost:  127     Base:
c ---[ 189]---> Sorter-cost:  127     Base:
c ---[ 187]---> Sorter-cost:  127     Base:
c ---[ 185]---> Sorter-cost:  127     Base:
c ---[ 183]---> Sorter-cost:  127     Base:
c ---[ 181]---> Sorter-cost:  127     Base:
c ---[ 179]---> Sorter-cost:  127     Base:
c ---[ 176]---> Sorter-cost:  127     Base:
c ---[ 174]---> Sorter-cost:  127     Base:
c ---[ 172]---> Sorter-cost:  127     Base:
c ---[ 170]---> Sorter-cost:  127     Base:
c ---[ 168]---> Sorter-cost:  127     Base:
c ---[ 166]---> Sorter-cost:  127     Base:
c ---[ 164]---> Sorter-cost:  127     Base:
c ---[ 162]---> Sorter-cost:  127     Base:
c ---[ 160]---> Sorter-cost:  127     Base:
c ---[ 158]---> Sorter-cost:  127     Base:
c ---[ 155]---> Sorter-cost:  127     Base:
c ---[ 153]---> Sorter-cost:  127     Base:
c ---[ 151]---> Sorter-cost:  127     Base:
c ---[ 149]---> Sorter-cost:  127     Base:
c ---[ 147]---> Sorter-cost:  127     Base:
c ---[ 145]---> Sorter-cost:  127     Base:
c ---[ 144]---> BDD-cost:   23
c ---[ 143]---> BDD-cost:   23
c ---[ 142]---> BDD-cost:   23
c ---[ 141]---> BDD-cost:    7
c ---[ 139]---> BDD-cost:    7
c ---[ 138]---> BDD-cost:   50
c ---[ 137]---> BDD-cost:   27
c ---[ 136]---> BDD-cost:   27
c ---[ 135]---> BDD-cost:   27
c ---[ 134]---> BDD-cost:   27
c ---[ 133]---> BDD-cost:   27
c ---[ 132]---> BDD-cost:   50
c ---[ 131]---> BDD-cost:   50
c ---[ 130]---> BDD-cost:   50
c ---[ 128]---> BDD-cost:   27
c ---[ 127]---> BDD-cost:   27
c ---[ 126]---> BDD-cost:   27
c ---[ 125]---> BDD-cost:   48
c ---[ 124]---> BDD-cost:   48
c ---[ 123]---> BDD-cost:   48
c ---[ 122]---> BDD-cost:   27
c ---[ 121]---> BDD-cost:   27
c ---[ 120]---> BDD-cost:   27
c ---[ 119]---> BDD-cost:   50
c ---[ 117]---> BDD-cost:   50
c ---[ 116]---> BDD-cost:   50
c ---[ 115]---> BDD-cost:   27
c ---[ 114]---> BDD-cost:   27
c ---[ 113]---> BDD-cost:   27
c ---[ 112]---> BDD-cost:   48
c ---[ 111]---> BDD-cost:   48
c ---[ 110]---> BDD-cost:   48
c ---[ 109]---> BDD-cost:   27
c ---[ 108]---> BDD-cost:   27
c ---[ 106]---> BDD-cost:   51
c ---[ 104]---> BDD-cost:   27
c ---[ 103]---> BDD-cost:   50
c ---[ 102]---> BDD-cost:   50
c ---[ 101]---> BDD-cost:   50
c ---[ 100]---> BDD-cost:   27
c ---[  99]---> BDD-cost:   27
c ---[  98]---> BDD-cost:   27
c ---[  97]---> BDD-cost:   48
c ---[  96]---> BDD-cost:   48
c ---[  95]---> BDD-cost:   48
c ---[  93]---> BDD-cost:   27
c ---[  92]---> BDD-cost:   27
c ---[  91]---> BDD-cost:   27
c ---[  81]---> BDD-cost:   51
c ---[  69]---> BDD-cost:   51
c ---[  57]---> BDD-cost:   51
c ---[  45]---> BDD-cost:   51
c ---[  33]---> BDD-cost:   51
c ---[  21]---> BDD-cost:   51
c ---[  10]---> BDD-cost:  216
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   25920    84925 |    7775       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/6727          
c   -- var.elim.:  2000/6727          
c   -- var.elim.:  3000/6727          
c   -- var.elim.:  4000/6727          
c   -- var.elim.:  5000/6727          
c   -- var.elim.:  6000/6727          
c   -- var.elim.:  6727/6727          
c   -- var.elim.:  1000/1675          
c   -- var.elim.:  1675/1675          
c   -- var.elim.:  27/27          
c   -- subsuming                       
c   -- var.elim.:  158/158          
c   -- var.elim.:  152/152          
c   -- subsuming                       
c   -- var.elim.:  30/30          
c |         0 |   24670    85296 |      --       0       --      -- |     --   | -1097/1311
c |         0 |   24670    85296 |    9868       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 1.3078 s)
c ==============================================================================
c [1mFound solution: 1659648[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   12
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |        40 |   24668    85263 |    7400      38     1621    42.7 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  44/44          
c   -- var.elim.:  43/43          
c |        40 |   24653    85265 |      --      38       --      -- |     --   | -15/3
c |        40 |   24653    85265 |    9861      36     1571    43.6 |  0.000 % |
c ==============================================================================
c (current CPU-time: 1.39079 s)
c ==============================================================================
c [1mFound solution: 1595648[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   12
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |        54 |   24666    85296 |    7399      50     2175    43.5 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  30/30          
c   -- var.elim.:  13/13          
c |        54 |   24652    85253 |      --      50       --      -- |     --   | -14/-42
c |        54 |   24652    85253 |    9860      50     2175    43.5 |  0.000 % |
c ==============================================================================
c (current CPU-time: 1.46078 s)
c ==============================================================================
c [1mFound solution: 1552128[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |        66 |   24663    85284 |    7398      62     2490    40.2 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  20/20          
c   -- var.elim.:  13/13          
c |        66 |   24648    85244 |      --      62       --      -- |     --   | -15/-39
c |        66 |   24648    85244 |    9859      62     2490    40.2 |  0.000 % |
c |       166 |   24648    85244 |   10845     162     8614    53.2 |  3.422 % |
c ==============================================================================
c (current CPU-time: 1.71674 s)
c ==============================================================================
c [1mFound solution: 1549568[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       223 |   24661    85277 |    7398     219    15995    73.0 |  3.422 % |
c   -- subsuming                       
c   -- var.elim.:  20/20          
c   -- var.elim.:  13/13          
c |       223 |   24650    85257 |      --     219       --      -- |     --   | -11/-19
c |       223 |   24650    85257 |    9860     219    15995    73.0 |  3.422 % |
c |       323 |   24618    85126 |   10831     316    16890    53.4 |  3.474 % |
c |       474 |   24611    85098 |   11911     466    28703    61.6 |  3.491 % |
c |       700 |   24611    85098 |   13102     692    66248    95.7 |  3.491 % |
c |      1038 |   24575    84949 |   14392    1027    75705    73.7 |  3.526 % |
c |      1545 |   24544    84817 |   15811    1530   129469    84.6 |  3.543 % |
c |      2305 |   24419    84310 |   17303    2285   214319    93.8 |  3.648 % |
c |      3445 |   24419    84310 |   19034    3425   443575   129.5 |  3.648 % |
c ==============================================================================
c (current CPU-time: 6.02608 s)
c ==============================================================================
c [1mFound solution: 1544448[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   10
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3891 |   24433    84344 |    7329    3871   497022   128.4 |  3.648 % |
c   -- subsuming                       
c   -- var.elim.:  169/169          
c   -- var.elim.:  65/65          
c   -- var.elim.:  6/6          
c |      3891 |   24408    84255 |      --    3871       --      -- |     --   | -25/-88
c |      3891 |   24408    84255 |    9763    3515   380111   108.1 |  3.648 % |
c |      3993 |   24408    84255 |   10739    3617   381164   105.4 |  3.671 % |
c |      4143 |   24408    84255 |   11813    3767   392935   104.3 |  3.671 % |
c |      4369 |   24382    84145 |   12980    3991   401226   100.5 |  3.688 % |
c |      4707 |   24382    84145 |   14279    4329   450586   104.1 |  3.688 % |
c |      5214 |   24382    84145 |   15706    4836   488812   101.1 |  3.688 % |
c ==============================================================================
c (current CPU-time: 8.19775 s)
c ==============================================================================
c [1mFound solution: 1543808[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   13
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5421 |   24393    84175 |    7317    5043   509464   101.0 |  3.688 % |
c   -- subsuming                       
c   -- var.elim.:  51/51          
c   -- var.elim.:  14/14          
c |      5421 |   24378    84119 |      --    5043       --      -- |     --   | -15/-55
c |      5421 |   24378    84119 |    9751    5043   509464   101.0 |  3.688 % |
c ==============================================================================
c (current CPU-time: 8.36373 s)
c ==============================================================================
c [1mFound solution: 1532928[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   10
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5447 |   24388    84145 |    7316    5069   514167   101.4 |  3.688 % |
c   -- subsuming                       
c   -- var.elim.:  16/16          
c   -- var.elim.:  14/14          
c |      5447 |   24377    84109 |      --    5069       --      -- |     --   | -11/-35
c |      5447 |   24377    84109 |    9750    5069   514167   101.4 |  3.688 % |
c |      5547 |   24329    83933 |   10704    5164   517809   100.3 |  3.809 % |
c |      5697 |   24329    83933 |   11775    5314   537173   101.1 |  3.809 % |
c |      5922 |   24296    83819 |   12935    5531   557335   100.8 |  3.897 % |
c |      6265 |   24296    83819 |   14228    5874   586107    99.8 |  3.897 % |
c ==============================================================================
c (current CPU-time: 10.4174 s)
c ==============================================================================
c [1mFound solution: 1532288[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   13
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      6688 |   24286    83768 |    7285    6295   623564    99.1 |  3.897 % |
c   -- subsuming                       
c   -- var.elim.:  94/94          
c   -- var.elim.:  68/68          
c   -- var.elim.:  15/15          
c |      6688 |   24255    83721 |      --    6295       --      -- |     --   | -31/-46
c |      6688 |   24255    83721 |    9702    6295   623564    99.1 |  3.897 % |
c |      6788 |   24255    83721 |   10672    6395   637908    99.8 |  3.991 % |
c |      6940 |   24247    83691 |   11735    5665   453916    80.1 |  4.008 % |
c |      7165 |   24247    83691 |   12909    5890   476583    80.9 |  4.008 % |
c |      7503 |   24247    83691 |   14200    6228   524655    84.2 |  4.008 % |
c ==============================================================================
c (current CPU-time: 12.1442 s)
c ==============================================================================
c [1mFound solution: 1492608[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   10
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      7873 |   24247    83673 |    7274    6597   560773    85.0 |  4.008 % |
c   -- subsuming                       
c   -- var.elim.:  59/59          
c   -- var.elim.:  32/32          
c |      7873 |   24227    83630 |      --    6597       --      -- |     --   | -20/-42
c |      7873 |   24227    83630 |    9690    6476   536301    82.8 |  4.008 % |
c ==============================================================================
c (current CPU-time: 12.3681 s)
c ==============================================================================
c [1mFound solution: 1465728[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      7922 |   24241    83666 |    7272    6525   542777    83.2 |  4.008 % |
c   -- subsuming                       
c   -- var.elim.:  28/28          
c   -- var.elim.:  14/14          
c |      7922 |   24225    83616 |      --    6525       --      -- |     --   | -16/-49
c |      7922 |   24225    83616 |    9690    6525   542777    83.2 |  4.008 % |
c ==============================================================================
c (current CPU-time: 12.5221 s)
c ==============================================================================
c [1mFound solution: 1461248[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   10
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      7973 |   24223    83592 |    7266    6575   549931    83.6 |  4.008 % |
c   -- subsuming                       
c   -- var.elim.:  36/36          
c   -- var.elim.:  20/20          
c |      7973 |   24209    83557 |      --    6575       --      -- |     --   | -14/-34
c |      7973 |   24209    83557 |    9683    6552   543122    82.9 |  4.008 % |
c |      8074 |   24209    83557 |   10651    6653   553170    83.1 |  4.097 % |
c |      8224 |   24209    83557 |   11717    6803   576623    84.8 |  4.097 % |
c |      8450 |   24187    83471 |   12877    7025   596286    84.9 |  4.132 % |
c |      8788 |   24187    83471 |   14164    7363   620796    84.3 |  4.132 % |
c |      9294 |   24187    83471 |   15581    7869   717379    91.2 |  4.132 % |
c |     10054 |   24149    83308 |   17112    8625   816409    94.7 |  4.149 % |
c |     11196 |   24137    83260 |   18814    9764   964120    98.7 |  4.167 % |
c ==============================================================================
c (current CPU-time: 18.9811 s)
c ==============================================================================
c [1mFound solution: 1433728[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   12
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     11771 |   24151    83294 |    7245   10339  1024697    99.1 |  4.167 % |
c   -- subsuming                       
c   -- var.elim.:  65/65          
c   -- var.elim.:  35/35          
c   -- var.elim.:  15/15          
c |     11771 |   24125    83246 |      --   10339       --      -- |     --   | -26/-47
c |     11771 |   24125    83246 |    9650    9293   814444    87.6 |  4.167 % |
c |     11872 |   24125    83246 |   10615    9394   826573    88.0 |  4.205 % |
c |     12022 |   24125    83246 |   11676    9544   846370    88.7 |  4.205 % |
c |     12247 |   24125    83246 |   12844    9769   878434    89.9 |  4.205 % |
c |     12584 |   24125    83246 |   14128   10106   901259    89.2 |  4.205 % |
c |     13090 |   24125    83246 |   15541   10612   979193    92.3 |  4.205 % |
c |     13850 |   24097    83133 |   17075   11367  1070684    94.2 |  4.258 % |
c |     14991 |   24097    83133 |   18783   12508  1278119   102.2 |  4.258 % |
c |     16700 |   24097    83133 |   20661   14217  1652435   116.2 |  4.258 % |
c |     19262 |   24097    83133 |   22727   16779  2056126   122.5 |  4.258 % |
c ==============================================================================
c (current CPU-time: 35.1267 s)
c ==============================================================================
c [1mFound solution: 1429248[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    8
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     20282 |   24100    83128 |    7229   17794  2201557   123.7 |  4.258 % |
c   -- subsuming                       
c   -- var.elim.:  67/67          
c   -- var.elim.:  62/62          
c |     20282 |   24078    83112 |      --   17794       --      -- |     --   | -22/-15
c |     20282 |   24078    83112 |    9631   13593  1190114    87.6 |  4.258 % |
c |     20382 |   24078    83112 |   10594    9108   721324    79.2 |  4.299 % |
c |     20536 |   24078    83112 |   11653    9262   730448    78.9 |  4.299 % |
c |     20762 |   24078    83112 |   12819    9488   761063    80.2 |  4.299 % |
c |     21099 |   24078    83112 |   14101    9825   811033    82.5 |  4.299 % |
c |     21605 |   24078    83112 |   15511   10331   885359    85.7 |  4.299 % |
c |     22364 |   24078    83112 |   17062   11090  1030021    92.9 |  4.299 % |
c |     23503 |   24078    83112 |   18768   12229  1214722    99.3 |  4.299 % |
c |     25211 |   24060    83048 |   20629   13936  1538594   110.4 |  4.334 % |
c |     27773 |   24060    83048 |   22692   16498  1970903   119.5 |  4.334 % |
c |     31618 |   24060    83048 |   24962   20343  2733278   134.4 |  4.334 % |
c |     37384 |   23936    82584 |   27316   26095  3802631   145.7 |  4.562 % |
c ==============================================================================
c (current CPU-time: 91.936 s)
c ==============================================================================
c [1mFound solution: 1422208[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   12
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     45193 |   23932    82543 |    7179   19717  3339689   169.4 |  4.562 % |
c   -- subsuming                       
c   -- var.elim.:  155/155          
c   -- var.elim.:  122/122          
c   -- subsuming                       
c   -- var.elim.:  31/31          
c   -- var.elim.:  15/15          
c |     45193 |   23897    82506 |      --   19717       --      -- |     --   | -35/-36
c |     45193 |   23897    82506 |    9558   13759  1129171    82.1 |  4.562 % |
c |     45295 |   23897    82506 |   10514    9275   720089    77.6 |  4.613 % |
c |     45445 |   23897    82506 |   11566    9425   748454    79.4 |  4.613 % |
c |     45671 |   23897    82506 |   12722    9651   757024    78.4 |  4.613 % |
c |     46009 |   23885    82457 |   13988    9984   790632    79.2 |  4.630 % |
c |     46515 |   23885    82457 |   15386   10490   824384    78.6 |  4.630 % |
c |     47277 |   23851    82314 |   16901   11247   960486    85.4 |  4.648 % |
c |     48418 |   23851    82314 |   18591   12388  1115591    90.1 |  4.648 % |
c |     50128 |   23851    82314 |   20450   14098  1435354   101.8 |  4.648 % |
c |     52690 |   23840    82273 |   22485   16659  1903049   114.2 |  4.666 % |
c |     56534 |   23774    82020 |   24665   20493  2777033   135.5 |  4.754 % |
c |     62300 |   23764    81981 |   27120   26257  3983711   151.7 |  4.771 % |
c |     70951 |   23754    81942 |   29820   22485  3734530   166.1 |  4.789 % |
c ==============================================================================
c (current CPU-time: 200.585 s)
c ==============================================================================
c [1mFound solution: 1421568[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    8
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     77770 |   23771    81982 |    7131   29304  5776686   197.1 |  4.789 % |
c   -- subsuming                       
c   -- var.elim.:  129/129          
c   -- var.elim.:  95/95          
c   -- subsuming                       
c   -- var.elim.:  13/13          
c |     77770 |   23738    81919 |      --   29304       --      -- |     --   | -33/-62
c |     77770 |   23738    81919 |    9495   18323  1674990    91.4 |  4.789 % |
c |     77871 |   23729    81886 |   10440    6725   335368    49.9 |  4.837 % |
c |     78022 |   23729    81886 |   11484    6876   377373    54.9 |  4.837 % |
c |     78247 |   23729    81886 |   12633    7101   402174    56.6 |  4.837 % |
c |     78584 |   23729    81886 |   13896    7438   508314    68.3 |  4.837 % |
c |     79090 |   23729    81886 |   15286    7944   648744    81.7 |  4.837 % |
c |     79849 |   23729    81886 |   16814    8703   754452    86.7 |  4.837 % |
c |     80988 |   23729    81886 |   18496    9842   923309    93.8 |  4.837 % |
c |     82697 |   23729    81886 |   20346   11551  1145083    99.1 |  4.837 % |
c |     85261 |   23687    81715 |   22341   14110  1526086   108.2 |  4.872 % |
c |     89106 |   23687    81715 |   24575   17955  2312740   128.8 |  4.872 % |
c |     94872 |   23678    81682 |   27022   23720  3447511   145.3 |  4.890 % |
c |    103521 |   23678    81682 |   29724   20467  3552666   173.6 |  4.890 % |
c ==============================================================================
c (current CPU-time: 289.265 s)
c ==============================================================================
c [1mFound solution: 1419648[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   10
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    108173 |   23665    81611 |    7099   25114  4605672   183.4 |  4.890 % |
c   -- subsuming                       
c   -- var.elim.:  108/108          
c   -- var.elim.:  61/61          
c   -- var.elim.:  9/9          
c |    108173 |   23633    81546 |      --   25114       --      -- |     --   | -32/-64
c |    108173 |   23633    81546 |    9453   15139  1311418    86.6 |  4.890 % |
c ==============================================================================
c (current CPU-time: 290.054 s)
c ==============================================================================
c [1mFound solution: 1408128[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    108214 |   23647    81582 |    7094    9337   598644    64.1 |  4.890 % |
c   -- subsuming                       
c   -- var.elim.:  28/28          
c   -- var.elim.:  14/14          
c |    108214 |   23631    81538 |      --    9337       --      -- |     --   | -16/-43
c |    108214 |   23631    81538 |    9452    9337   598644    64.1 |  4.890 % |
c |    108314 |   23631    81538 |   10397    9437   616314    65.3 |  5.019 % |
c |    108464 |   23631    81538 |   11437    9587   633830    66.1 |  5.019 % |
c |    108691 |   23592    81400 |   12560    9800   651219    66.5 |  5.108 % |
c |    109028#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.95 0.90 2/54 1917
Raw data (stat): 1917 (runsolver) R 1916 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546336996 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.0003 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 1917
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 3671 0 0 0 987 11 0 0 25 0 1 0 546336996 11468800 2384 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2800 2384 603 41 0 2759 0
vsize: 11200
[startup+19.9998 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 1917
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 4996 0 0 0 1982 15 0 0 25 0 1 0 546336996 13791232 2950 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3367 2950 603 41 0 3326 0
vsize: 13468
[startup+30.0004 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 1917
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 5664 0 0 0 2980 17 0 0 25 0 1 0 546336996 16547840 3618 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4040 3618 603 41 0 3999 0
vsize: 16160
[startup+40.0002 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 1917
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 6409 0 0 0 3977 19 0 0 25 0 1 0 546336996 19107840 4238 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4665 4238 603 41 0 4624 0
vsize: 18660
[startup+50.0003 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 1917
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 6409 0 0 0 4978 19 0 0 25 0 1 0 546336996 19107840 4238 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4665 4238 603 41 0 4624 0
vsize: 18660
[startup+60.0005 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 1917
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 6889 0 0 0 5977 21 0 0 25 0 1 0 546336996 21090304 4718 4294967295 134512640 134672761 3221224544 3221223728 134616020 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5149 4718 603 41 0 5108 0
vsize: 20596
[startup+70.0002 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 1917
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 7612 0 0 0 6974 23 0 0 25 0 1 0 546336996 24125440 5441 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5890 5441 603 41 0 5849 0
vsize: 23560
[startup+80.0009 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 1917
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 8489 0 0 0 7971 26 0 0 25 0 1 0 546336996 27668480 6318 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6755 6318 603 41 0 6714 0
vsize: 27020
[startup+90.0005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 1917
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 8888 0 0 0 8971 27 0 0 25 0 1 0 546336996 29220864 6717 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7134 6717 603 41 0 7093 0
vsize: 28536
[startup+100 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 1917
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 9135 0 0 0 9970 28 0 0 25 0 1 0 546336996 29405184 6721 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7179 6721 603 41 0 7138 0
vsize: 28716
[startup+110.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1917
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 9135 0 0 0 10970 28 0 0 25 0 1 0 546336996 29405184 6721 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7179 6721 603 41 0 7138 0
vsize: 28716
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1917
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 9135 0 0 0 11970 28 0 0 25 0 1 0 546336996 29405184 6721 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7179 6721 603 41 0 7138 0
vsize: 28716
[startup+130.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1917
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 9135 0 0 0 12970 28 0 0 25 0 1 0 546336996 29405184 6721 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7179 6721 603 41 0 7138 0
vsize: 28716
[startup+140.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1917
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 9135 0 0 0 13970 28 0 0 25 0 1 0 546336996 29405184 6721 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7179 6721 603 41 0 7138 0
vsize: 28716
[startup+150.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1917
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 9164 0 0 0 14970 28 0 0 25 0 1 0 546336996 29405184 6750 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7179 6750 603 41 0 7138 0
vsize: 28716
[startup+160 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1917
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 9164 0 0 0 15970 28 0 0 25 0 1 0 546336996 29405184 6750 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7179 6750 603 41 0 7138 0
vsize: 28716
[startup+170 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1917
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 9164 0 0 0 16970 28 0 0 25 0 1 0 546336996 29405184 6750 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7179 6750 603 41 0 7138 0
vsize: 28716
[startup+180.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1917
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 9497 0 0 0 17969 29 0 0 25 0 1 0 546336996 30871552 7083 4294967295 134512640 134672761 3221224544 3221223728 134615505 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7537 7083 603 41 0 7496 0
vsize: 30148
[startup+190 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1920
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 9963 0 0 0 18968 30 0 0 25 0 1 0 546336996 32714752 7549 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7987 7549 603 41 0 7946 0
vsize: 31948
[startup+200 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 1970
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 10456 0 0 0 19966 32 0 0 25 0 1 0 546336996 34824192 8042 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8502 8042 603 41 0 8461 0
vsize: 34008
[startup+210.001 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 1970
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 10823 0 0 0 20964 33 0 0 25 0 1 0 546336996 35127296 8150 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8576 8150 603 41 0 8535 0
vsize: 34304
[startup+220.001 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 1970
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 10823 0 0 0 21964 33 0 0 25 0 1 0 546336996 35127296 8150 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8576 8150 603 41 0 8535 0
vsize: 34304
[startup+230.002 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 1970
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 10823 0 0 0 22965 33 0 0 25 0 1 0 546336996 35127296 8150 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8576 8150 603 41 0 8535 0
vsize: 34304
[startup+240.002 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 1970
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 10823 0 0 0 23965 33 0 0 25 0 1 0 546336996 35127296 8150 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8576 8150 603 41 0 8535 0
vsize: 34304
[startup+250.003 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 1970
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 10823 0 0 0 24964 33 0 0 25 0 1 0 546336996 35127296 8150 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8576 8150 603 41 0 8535 0
vsize: 34304
[startup+260.002 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 1972
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 10823 0 0 0 25965 33 0 0 25 0 1 0 546336996 35127296 8150 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8576 8150 603 41 0 8535 0
vsize: 34304
[startup+270.002 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 1972
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 10823 0 0 0 26965 33 0 0 25 0 1 0 546336996 35127296 8150 4294967295 134512640 134672761 3221224544 3221223792 134618072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8576 8150 603 41 0 8535 0
vsize: 34304
[startup+280.003 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 1972
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 10823 0 0 0 27965 33 0 0 25 0 1 0 546336996 35127296 8150 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8576 8150 603 41 0 8535 0
vsize: 34304
[startup+290.004 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1972
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 10947 0 0 0 28964 34 0 0 25 0 1 0 546336996 34988032 8116 4294967295 134512640 134672761 3221224544 3221223800 134616336 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8542 8116 603 41 0 8501 0
vsize: 34168
[startup+300.003 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1972
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 11054 0 0 0 29963 35 0 0 25 0 1 0 546336996 34988032 8116 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8542 8116 603 41 0 8501 0
vsize: 34168
[startup+310.004 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1972
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 11054 0 0 0 30962 35 0 0 25 0 1 0 546336996 34988032 8116 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8542 8116 603 41 0 8501 0
vsize: 34168
[startup+320.005 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1972
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 11054 0 0 0 31962 35 0 0 25 0 1 0 546336996 34988032 8116 4294967295 134512640 134672761 3221224544 3221223728 134615752 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8542 8116 603 41 0 8501 0
vsize: 34168
[startup+330.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1972
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 11054 0 0 0 32962 35 0 0 25 0 1 0 546336996 34988032 8116 4294967295 134512640 134672761 3221224544 3221223688 134616293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8542 8116 603 41 0 8501 0
vsize: 34168
[startup+340.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1972
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 11054 0 0 0 33962 35 0 0 25 0 1 0 546336996 34988032 8116 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8542 8116 603 41 0 8501 0
vsize: 34168
[startup+350.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1972
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 11054 0 0 0 34962 35 0 0 25 0 1 0 546336996 34988032 8116 4294967295 134512640 134672761 3221224544 3221223584 134603552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8542 8116 603 41 0 8501 0
vsize: 34168
[startup+360.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1972
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 11054 0 0 0 35962 35 0 0 25 0 1 0 546336996 34988032 8116 4294967295 134512640 134672761 3221224544 3221223536 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8542 8116 603 41 0 8501 0
vsize: 34168
[startup+370.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1972
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 11054 0 0 0 36962 35 0 0 25 0 1 0 546336996 34988032 8116 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8542 8116 603 41 0 8501 0
vsize: 34168
[startup+380.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1972
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 11054 0 0 0 37963 35 0 0 25 0 1 0 546336996 34988032 8116 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8542 8116 603 41 0 8501 0
vsize: 34168
[startup+390.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1972
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 11055 0 0 0 38963 35 0 0 25 0 1 0 546336996 34988032 8117 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8542 8117 603 41 0 8501 0
vsize: 34168
[startup+400.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1972
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 11055 0 0 0 39963 36 0 0 25 0 1 0 546336996 34988032 8117 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8542 8117 603 41 0 8501 0
vsize: 34168
[startup+410.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1972
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 11055 0 0 0 40963 36 0 0 25 0 1 0 546336996 34988032 8117 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8542 8117 603 41 0 8501 0
vsize: 34168
[startup+420.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1972
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 11055 0 0 0 41963 36 0 0 25 0 1 0 546336996 34988032 8117 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8542 8117 603 41 0 8501 0
vsize: 34168
[startup+430.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1972
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 11055 0 0 0 42963 36 0 0 25 0 1 0 546336996 34988032 8117 4294967295 134512640 134672761 3221224544 3221223728 134615964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8542 8117 603 41 0 8501 0
vsize: 34168
[startup+440.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1972
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 11329 0 0 0 43962 37 0 0 25 0 1 0 546336996 36167680 8391 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8830 8391 603 41 0 8789 0
vsize: 35320
[startup+450.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1972
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 11923 0 0 0 44961 39 0 0 25 0 1 0 546336996 38666240 8985 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9440 8985 603 41 0 9399 0
vsize: 37760
[startup+460.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1972
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 12515 0 0 0 45959 40 0 0 25 0 1 0 546336996 41029632 9577 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10017 9577 603 41 0 9976 0
vsize: 40068
[startup+470.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1972
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 13056 0 0 0 46958 42 0 0 25 0 1 0 546336996 43237376 10118 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10556 10118 603 41 0 10515 0
vsize: 42224
[startup+480.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1972
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 13528 0 0 0 47957 43 0 0 25 0 1 0 546336996 45207552 10590 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11037 10590 603 41 0 10996 0
vsize: 44148
[startup+490.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1972
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 13924 0 0 0 48956 45 0 0 25 0 1 0 546336996 47075328 10986 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11493 10986 603 41 0 11452 0
vsize: 45972
[startup+500.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1972
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 14073 0 0 0 49955 45 0 0 25 0 1 0 546336996 47419392 11102 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11577 11102 603 41 0 11536 0
vsize: 46308
[startup+510.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1972
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 14073 0 0 0 50956 45 0 0 25 0 1 0 546336996 47419392 11102 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11577 11102 603 41 0 11536 0
vsize: 46308
[startup+520.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1972
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 14073 0 0 0 51956 45 0 0 25 0 1 0 546336996 47419392 11102 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11577 11102 603 41 0 11536 0
vsize: 46308
[startup+530.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 14073 0 0 0 52956 45 0 0 25 0 1 0 546336996 47419392 11102 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11577 11102 603 41 0 11536 0
vsize: 46308
[startup+540.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 14073 0 0 0 53956 45 0 0 25 0 1 0 546336996 47419392 11102 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11577 11102 603 41 0 11536 0
vsize: 46308
[startup+550.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 14075 0 0 0 54956 45 0 0 25 0 1 0 546336996 47419392 11104 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11577 11104 603 41 0 11536 0
vsize: 46308
[startup+560.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 14075 0 0 0 55956 45 0 0 25 0 1 0 546336996 47419392 11104 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11577 11104 603 41 0 11536 0
vsize: 46308
[startup+570.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 14076 0 0 0 56956 45 0 0 25 0 1 0 546336996 47419392 11105 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11577 11105 603 41 0 11536 0
vsize: 46308
[startup+580.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 14411 0 0 0 57956 46 0 0 25 0 1 0 546336996 48869376 11440 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11931 11440 603 41 0 11890 0
vsize: 47724
[startup+590.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 14858 0 0 0 58954 48 0 0 25 0 1 0 546336996 50712576 11887 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12381 11887 603 41 0 12340 0
vsize: 49524
[startup+600.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 15233 0 0 0 59953 49 0 0 25 0 1 0 546336996 52301824 12262 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12769 12262 603 41 0 12728 0
vsize: 51076
[startup+610.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 15703 0 0 0 60952 51 0 0 25 0 1 0 546336996 54185984 12732 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13229 12732 603 41 0 13188 0
vsize: 52916
[startup+620.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 16137 0 0 0 61951 52 0 0 25 0 1 0 546336996 56057856 13166 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13686 13166 603 41 0 13645 0
vsize: 54744
[startup+630.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 16547 0 0 0 62949 54 0 0 25 0 1 0 546336996 57794560 13576 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14110 13576 603 41 0 14069 0
vsize: 56440
[startup+640.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 16941 0 0 0 63948 55 0 0 25 0 1 0 546336996 59342848 13970 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14488 13970 603 41 0 14447 0
vsize: 57952
[startup+650.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17033 0 0 0 64948 56 0 0 25 0 1 0 546336996 59650048 14057 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14563 14057 603 41 0 14522 0
vsize: 58252
[startup+660.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17033 0 0 0 65948 56 0 0 25 0 1 0 546336996 59650048 14057 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14563 14057 603 41 0 14522 0
vsize: 58252
[startup+670.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17033 0 0 0 66948 56 0 0 25 0 1 0 546336996 59650048 14057 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14563 14057 603 41 0 14522 0
vsize: 58252
[startup+680.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17033 0 0 0 67948 56 0 0 25 0 1 0 546336996 59650048 14057 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14563 14057 603 41 0 14522 0
vsize: 58252
[startup+690.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17033 0 0 0 68948 56 0 0 25 0 1 0 546336996 59650048 14057 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14563 14057 603 41 0 14522 0
vsize: 58252
[startup+700.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17033 0 0 0 69948 56 0 0 25 0 1 0 546336996 59650048 14057 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14563 14057 603 41 0 14522 0
vsize: 58252
[startup+710.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17033 0 0 0 70949 56 0 0 25 0 1 0 546336996 59650048 14057 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14563 14057 603 41 0 14522 0
vsize: 58252
[startup+720.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17033 0 0 0 71949 56 0 0 25 0 1 0 546336996 59650048 14057 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14563 14057 603 41 0 14522 0
vsize: 58252
[startup+730.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17033 0 0 0 72949 56 0 0 25 0 1 0 546336996 59650048 14057 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14563 14057 603 41 0 14522 0
vsize: 58252
[startup+740.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17033 0 0 0 73949 56 0 0 25 0 1 0 546336996 59650048 14057 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14563 14057 603 41 0 14522 0
vsize: 58252
[startup+750.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17034 0 0 0 74949 56 0 0 25 0 1 0 546336996 59650048 14058 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14563 14058 603 41 0 14522 0
vsize: 58252
[startup+760.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17070 0 0 0 75949 57 0 0 25 0 1 0 546336996 59596800 14045 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14550 14045 603 41 0 14509 0
vsize: 58200
[startup+770.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17070 0 0 0 76949 57 0 0 25 0 1 0 546336996 59596800 14045 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14550 14045 603 41 0 14509 0
vsize: 58200
[startup+780.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17070 0 0 0 77949 57 0 0 25 0 1 0 546336996 59596800 14045 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14550 14045 603 41 0 14509 0
vsize: 58200
[startup+790.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17070 0 0 0 78949 57 0 0 25 0 1 0 546336996 59596800 14045 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14550 14045 603 41 0 14509 0
vsize: 58200
[startup+800.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17070 0 0 0 79949 57 0 0 25 0 1 0 546336996 59596800 14045 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14550 14045 603 41 0 14509 0
vsize: 58200
[startup+810.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17070 0 0 0 80950 57 0 0 25 0 1 0 546336996 59596800 14045 4294967295 134512640 134672761 3221224544 3221223728 134615585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14550 14045 603 41 0 14509 0
vsize: 58200
[startup+820.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17070 0 0 0 81950 57 0 0 25 0 1 0 546336996 59596800 14045 4294967295 134512640 134672761 3221224544 3221223728 134615794 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14550 14045 603 41 0 14509 0
vsize: 58200
[startup+830.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17070 0 0 0 82950 57 0 0 25 0 1 0 546336996 59596800 14045 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14550 14045 603 41 0 14509 0
vsize: 58200
[startup+840.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17070 0 0 0 83950 57 0 0 25 0 1 0 546336996 59596800 14045 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14550 14045 603 41 0 14509 0
vsize: 58200
[startup+850.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17070 0 0 0 84950 57 0 0 25 0 1 0 546336996 59596800 14045 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14550 14045 603 41 0 14509 0
vsize: 58200
[startup+860.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17070 0 0 0 85950 57 0 0 25 0 1 0 546336996 59596800 14045 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14550 14045 603 41 0 14509 0
vsize: 58200
[startup+870.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17074 0 0 0 86950 57 0 0 25 0 1 0 546336996 59596800 14049 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14550 14049 603 41 0 14509 0
vsize: 58200
[startup+880.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17076 0 0 0 87951 58 0 0 25 0 1 0 546336996 59596800 14051 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14550 14051 603 41 0 14509 0
vsize: 58200
[startup+890.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17077 0 0 0 88951 58 0 0 25 0 1 0 546336996 59596800 14052 4294967295 134512640 134672761 3221224544 3221223728 134616017 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14550 14052 603 41 0 14509 0
vsize: 58200
[startup+900.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17083 0 0 0 89951 58 0 0 25 0 1 0 546336996 59596800 14058 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14550 14058 603 41 0 14509 0
vsize: 58200
[startup+910.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17084 0 0 0 90951 58 0 0 25 0 1 0 546336996 59596800 14059 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14550 14059 603 41 0 14509 0
vsize: 58200
[startup+920.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17474 0 0 0 91950 59 0 0 25 0 1 0 546336996 61063168 14409 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14908 14409 603 41 0 14867 0
vsize: 59632
[startup+930.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17474 0 0 0 92950 59 0 0 25 0 1 0 546336996 61063168 14409 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14908 14409 603 41 0 14867 0
vsize: 59632
[startup+940.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17474 0 0 0 93950 59 0 0 25 0 1 0 546336996 61063168 14409 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14908 14409 603 41 0 14867 0
vsize: 59632
[startup+950.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17474 0 0 0 94950 59 0 0 25 0 1 0 546336996 61063168 14409 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14908 14409 603 41 0 14867 0
vsize: 59632
[startup+960.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17474 0 0 0 95951 59 0 0 25 0 1 0 546336996 61063168 14409 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14908 14409 603 41 0 14867 0
vsize: 59632
[startup+970.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17474 0 0 0 96951 59 0 0 25 0 1 0 546336996 61063168 14409 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14908 14409 603 41 0 14867 0
vsize: 59632
[startup+980.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17474 0 0 0 97951 59 0 0 25 0 1 0 546336996 61063168 14409 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14908 14409 603 41 0 14867 0
vsize: 59632
[startup+990.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17474 0 0 0 98951 59 0 0 25 0 1 0 546336996 61063168 14409 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14908 14409 603 41 0 14867 0
vsize: 59632
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17474 0 0 0 99951 59 0 0 25 0 1 0 546336996 61063168 14409 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14908 14409 603 41 0 14867 0
vsize: 59632
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17474 0 0 0 100951 59 0 0 25 0 1 0 546336996 61063168 14409 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14908 14409 603 41 0 14867 0
vsize: 59632
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17474 0 0 0 101951 59 0 0 25 0 1 0 546336996 61063168 14409 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14908 14409 603 41 0 14867 0
vsize: 59632
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17474 0 0 0 102952 59 0 0 25 0 1 0 546336996 61063168 14409 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14908 14409 603 41 0 14867 0
vsize: 59632
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17484 0 0 0 103952 59 0 0 25 0 1 0 546336996 61259776 14419 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14956 14419 603 41 0 14915 0
vsize: 59824
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17484 0 0 0 104952 60 0 0 25 0 1 0 546336996 61259776 14419 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14956 14419 603 41 0 14915 0
vsize: 59824
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17493 0 0 0 105952 60 0 0 25 0 1 0 546336996 61259776 14428 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14956 14428 603 41 0 14915 0
vsize: 59824
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17577 0 0 0 106952 60 0 0 25 0 1 0 546336996 61652992 14512 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15052 14512 603 41 0 15011 0
vsize: 60208
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 17915 0 0 0 107951 61 0 0 25 0 1 0 546336996 63008768 14850 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15383 14850 603 41 0 15342 0
vsize: 61532
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 18182 0 0 0 108951 61 0 0 25 0 1 0 546336996 64225280 15117 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15680 15117 603 41 0 15639 0
vsize: 62720
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 18329 0 0 0 109950 62 0 0 25 0 1 0 546336996 64573440 15224 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15765 15224 603 41 0 15724 0
vsize: 63060
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 18329 0 0 0 110951 62 0 0 25 0 1 0 546336996 64573440 15224 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15765 15224 603 41 0 15724 0
vsize: 63060
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 18329 0 0 0 111951 62 0 0 25 0 1 0 546336996 64573440 15224 4294967295 134512640 134672761 3221224544 3221223356 1075350544 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15765 15224 603 41 0 15724 0
vsize: 63060
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 18329 0 0 0 112951 62 0 0 25 0 1 0 546336996 64573440 15224 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15765 15224 603 41 0 15724 0
vsize: 63060
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 18330 0 0 0 113951 62 0 0 25 0 1 0 546336996 64573440 15225 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15765 15225 603 41 0 15724 0
vsize: 63060
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 18330 0 0 0 114951 62 0 0 25 0 1 0 546336996 64573440 15225 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15765 15225 603 41 0 15724 0
vsize: 63060
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 18332 0 0 0 115951 62 0 0 25 0 1 0 546336996 64573440 15227 4294967295 134512640 134672761 3221224544 3221223536 134565130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15765 15227 603 41 0 15724 0
vsize: 63060
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 18332 0 0 0 116951 62 0 0 25 0 1 0 546336996 64573440 15227 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15765 15227 603 41 0 15724 0
vsize: 63060
[startup+1180.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 18332 0 0 0 117951 63 0 0 25 0 1 0 546336996 64573440 15227 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15765 15227 603 41 0 15724 0
vsize: 63060
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 18332 0 0 0 118952 63 0 0 25 0 1 0 546336996 64573440 15227 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15765 15227 603 41 0 15724 0
vsize: 63060
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1974
Raw data (stat): 1917 (minisat+) R 1916 22612 22611 0 -1 0 18332 0 0 0 119952 63 0 0 25 0 1 0 546336996 64573440 15227 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15765 15227 603 41 0 15724 0
vsize: 63060
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 1974
Raw data (stat): 1917 (minisat+) Z 1916 22612 22611 0 -1 12 18333 0 0 0 119952 66 0 0 25 0 1 0 546336996 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.05
CPU time (s): 1200.18
CPU user time (s): 1199.52
CPU system time (s): 0.661899
CPU usage (%): 100.011
Max. virtual memory (Kb): 63060
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####