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-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-markshare2_1.opb
MD5SUM	a84a96a9314212f3d8ecd5227c500cef
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	91392
Optimality of the best value was proved	NO
Number of terms in the objective function	210
Biggest coefficient in the objective function	536870912
Number of bits for the biggest coefficient in the objective function	30
Sum of the numbers in the objective function	7516192761
Number of bits of the sum of numbers in the objective function	33
Biggest number in a constraint	536870912
Number of bits of the biggest number in a constraint	30
Biggest sum of numbers in a constraint	7516192761
Number of bits of the biggest sum of numbers	33
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1202.31
Number of variables	330
Total number of constraints	67
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	54
Number of constraints which are nor clauses,nor cardinality constraints	13
Minimum length of a constraint	1
Maximum length of a constraint	150
Trace number 20768

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-04-21 21:47:14 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=14493 boxname=wulflinc17 idbench=1115 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a84a96a9314212f3d8ecd5227c500cef  /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-markshare2_1.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-markshare2_1.opb /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-markshare2_1.opb
IDLAUNCH: 14493
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
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:        453848 kB
Buffers:         25780 kB
Cached:         529440 kB
SwapCached:        408 kB
Active:         140692 kB
Inactive:       417100 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        453596 kB
SwapTotal:     2097892 kB
SwapFree:      2097056 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5860 kB
Slab:            17380 kB
Committed_AS:    63820 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 22:07:17 (client local time) WITH STATUS 10 IN 1200.49 SECONDS
stats: 14493 7 1200.49 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 20 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######
c   -- Clauses(.)/Splits(s): (none)
c ---[  19]---> BDD-cost:   10
c ---[  18]---> BDD-cost:   10
c ---[  17]---> BDD-cost:   10
c ---[  16]---> BDD-cost:   10
c ---[  15]---> BDD-cost:   10
c ---[  14]---> BDD-cost:   10
c ---[  12]---> Adder-cost: 708   maxlim: 3756758   bits: 23/22
c ---[  10]---> Adder-cost: 758   maxlim: 4064912   bits: 23/22
c ---[   8]---> Adder-cost: 714   maxlim: 3859164   bits: 23/22
c ---[   6]---> Adder-cost: 676   maxlim: 4153021   bits: 23/22
c ---[   4]---> Adder-cost: 812   maxlim: 3812158   bits: 23/22
c ---[   2]---> Adder-cost: 766   maxlim: 4131466   bits: 23/22
c ---[   0]---> Adder-cost: 692   maxlim: 3780388   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   35547   127928 |   10664       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5238          
c   -- var.elim.:  2000/5238          
c   -- var.elim.:  3000/5238          
c   -- var.elim.:  4000/5238          
c   -- var.elim.:  5000/5238          
c   -- var.elim.:  5238/5238          
c   -- var.elim.:  512/512          
c   -- var.elim.:  12/12          
c   -- subsuming                       
c   -- var.elim.:  96/96          
c   -- var.elim.:  10/10          
c |         0 |   34379   122132 |      --       0       --      -- |     --   | -526/-1495
c |         0 |   34379   122132 |   13751       0        0     nan |  0.000 % |
c |       100 |   34379   122132 |   15126     100      439     4.4 |  7.388 % |
c |       250 |   34379   122132 |   16639     250     1146     4.6 |  7.388 % |
c |       475 |   34379   122132 |   18303     475     3214     6.8 |  7.388 % |
c |       812 |   34379   122132 |   20133     812     6837     8.4 |  7.388 % |
c ==============================================================================
c (current CPU-time: 1.54577 s)
c ==============================================================================
c [1mFound solution: 2182466[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 2156     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1153 |   39855   134917 |   11956    1153    10919     9.5 |  7.388 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2026          
c   -- var.elim.:  2000/2026          
c   -- var.elim.:  2026/2026          
c   -- var.elim.:  1000/1087          
c   -- var.elim.:  1087/1087          
c   -- subsuming                       
c   -- var.elim.:  64/64          
c   -- var.elim.:  6/6          
c |      1153 |   39163   136582 |      --    1153       --      -- |     --   | -692/1666
c |      1153 |   39163   136582 |   15665    1153    10919     9.5 |  7.388 % |
c |      1253 |   39163   136582 |   17231    1253    24045    19.2 |  6.250 % |
c |      1403 |   39163   136582 |   18954    1403    24926    17.8 |  6.250 % |
c |      1628 |   39163   136582 |   20850    1628    27636    17.0 |  6.250 % |
c |      1966 |   39163   136582 |   22935    1966    39086    19.9 |  6.250 % |
c |      2472 |   39163   136582 |   25228    2472    43381    17.5 |  6.250 % |
c ==============================================================================
c (current CPU-time: 2.76958 s)
c ==============================================================================
c [1mFound solution: 1914856[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   20     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2700 |   39458   137393 |   11837    2700    54224    20.1 |  6.250 % |
c   -- subsuming                       
c   -- var.elim.:  487/487          
c   -- var.elim.:  293/293          
c   -- subsuming                       
c   -- var.elim.:  5/5          
c |      2700 |   39300   137356 |      --    2700       --      -- |     --   | -158/-36
c |      2700 |   39300   137356 |   15720    2700    54224    20.1 |  6.250 % |
c |      2800 |   39300   137356 |   17292    2800    55231    19.7 |  6.227 % |
c |      2951 |   39300   137356 |   19021    2951    56340    19.1 |  6.227 % |
c |      3176 |   39300   137356 |   20923    3176    59117    18.6 |  6.227 % |
c |      3514 |   39300   137356 |   23015    3514    66152    18.8 |  6.227 % |
c |      4021 |   39300   137356 |   25317    4021    76568    19.0 |  6.227 % |
c |      4780 |   39300   137356 |   27848    4780    94809    19.8 |  6.227 % |
c |      5919 |   39300   137356 |   30633    5919   137161    23.2 |  6.227 % |
c |      7628 |   39300   137356 |   33697    7628   207524    27.2 |  6.227 % |
c |     10191 |   39300   137356 |   37066   10191   293064    28.8 |  6.227 % |
c |     14035 |   39300   137356 |   40773   14035   530793    37.8 |  6.227 % |
c |     19802 |   39300   137356 |   44850   19802   812971    41.1 |  6.227 % |
c ==============================================================================
c (current CPU-time: 20.4289 s)
c ==============================================================================
c [1mFound solution: 975708[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   19     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     27542 |   39376   137624 |   11812   27542  1127263    40.9 |  6.227 % |
c   -- subsuming                       
c   -- var.elim.:  220/220          
c   -- var.elim.:  199/199          
c   -- var.elim.:  30/30          
c   -- var.elim.:  9/9          
c   -- var.elim.:  11/11          
c   -- subsuming                       
c   -- var.elim.:  28/28          
c   -- var.elim.:  17/17          
c |     27542 |   39259   137640 |      --   27542       --      -- |     --   | -75/160
c |     27542 |   39259   137640 |   15703   25326   960881    37.9 |  6.227 % |
c |     27643 |   39259   137640 |   17273   12053   422412    35.0 |  6.366 % |
c |     27793 |   39259   137640 |   19001   12203   428614    35.1 |  6.366 % |
c |     28018 |   39233   137500 |   20887   12426   431784    34.7 |  6.427 % |
c |     28356 |   39233   137500 |   22976   12764   438083    34.3 |  6.427 % |
c |     28862 |   39233   137500 |   25274   13270   466970    35.2 |  6.427 % |
c |     29622 |   39233   137500 |   27801   14030   482566    34.4 |  6.427 % |
c |     30761 |   39233   137500 |   30581   15169   530742    35.0 |  6.427 % |
c |     32470 |   39233   137500 |   33639   16878   584857    34.7 |  6.427 % |
c |     35032 |   39233   137500 |   37003   19440   682570    35.1 |  6.427 % |
c |     38876 |   39233   137500 |   40704   23284   911907    39.2 |  6.427 % |
c |     44642 |   39233   137500 |   44774   29050  1173376    40.4 |  6.427 % |
c |     53291 |   39177   137259 |   49181   37697  1761993    46.7 |  6.550 % |
c |     66266 |   39177   137259 |   54099   50672  2844743    56.1 |  6.550 % |
c |     85727 |   39149   137136 |   59467   30633  2294940    74.9 |  6.596 % |
c |    114920 |   39123   137054 |   65370   59825  4945015    82.7 |  6.673 % |
c |    158709 |   39123   137054 |   71907   51713  3447419    66.7 |  6.673 % |
c |    224393 |   39123   137054 |   79098   57050  5097557    89.4 |  6.673 % |
c |    322920 |   39119   137040 |   86999   20107  3081705   153.3 |  6.688 % |
c ==============================================================================
c (current CPU-time: 980.813 s)
c ==============================================================================
c [1mFound solution: 941748[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    424184 |   39187   137292 |   11756   49294  6110489   124.0 |  6.688 % |
c   -- subsuming                       
c   -- var.elim.:  247/247          
c   -- var.elim.:  189/189          
c   -- var.elim.:  11/11          
c   -- var.elim.:  49/49          
c   -- var.elim.:  45/45          
c   -- var.elim.:  50/50          
c   -- var.elim.:  29/29          
c   -- var.elim.:  29/29          
c   -- var.elim.:  42/42          
c |    424184 |   39011   136420 |      --   49294       --      -- |     --   | -176/-871
c |    424184 |   39011   136420 |   15604   43149  4914159   113.9 |  6.688 % |
c |    424285 |   39011   136420 |   17164   14970  2170511   145.0 |  6.770 % |
c |    424435 |   39011   136420 |   18881   15120  2172275   143.7 |  6.770 % |
c |    424661 |   39011   136420 |   20769   15346  2176590   141.8 |  6.770 % |
c |    424999 |   39011   136420 |   22846   15684  2186337   139.4 |  6.770 % |
c |    425507 |   39011   136420 |   25131   16192  2208094   136.4 |  6.770 % |
c |    426266 |   39011   136420 |   27644   16951  2228658   131.5 |  6.770 % |
c |    427405 |   39011   136420 |   30408   18090  2286141   126.4 |  6.770 % |
c |    429113 |   39011   136420 |   33449   19798  2396030   121.0 |  6.770 % |
c |    431675 |   39011   136420 |   36794   22360  2496479   111.6 |  6.770 % |
c |    435520 |   39011   136420 |   40473   26205  2709363   103.4 |  6.770 % |
c |    441287 |   39011   136420 |   44521   31972  3266666   102.2 |  6.770 % |
c ==============================================================================
c (current CPU-time: 1003.63 s)
c ==============================================================================
c [1mFound solution: 669952[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    442560 |   39073   136655 |   11721   33245  3328643   100.1 |  6.770 % |
c   -- subsuming                       
c   -- var.elim.:  186/186          
c   -- var.elim.:  144/144          
c   -- var.elim.:  14/14          
c |    442560 |   39028   136708 |      --   33245       --      -- |     --   | -45/54
c |    442560 |   39028   136708 |   15611   33245  3328643   100.1 |  6.770 % |
c |    442660 |   39028   136708 |   17172   14505   902124    62.2 |  6.783 % |
c |    442811 |   39028   136708 |   18889   14656   903058    61.6 |  6.783 % |
c |    443037 |   39028   136708 |   20778   14882   908851    61.1 |  6.783 % |
c |    443374 |   39028   136708 |   22856   15219   917139    60.3 |  6.783 % |
c |    443880 |   39028   136708 |   25141   15725   933377    59.4 |  6.783 % |
c |    444639 |   39028   136708 |   27656   16484   962526    58.4 |  6.783 % |
c |    445778 |   39028   136708 |   30421   17623  1028615    58.4 |  6.783 % |
c |    447486 |   39028   136708 |   33463   19331  1219494    63.1 |  6.783 % |
c |    450050 |   39028   136708 |   36810   21895  1380696    63.1 |  6.783 % |
c |    453894 |   39028   136708 |   40491   25739  1527264    59.3 |  6.783 % |
c |    459661 |   39014   136646 |   44524   31504  1762447    55.9 |  6.813 % |
c |    468310 |   39014   136646 |   48977   40153  3318129    82.6 |  6.813 % |
c |    481284 |   38989   136554 |   53840   17867  1018308    57.0 |  6.859 % |
c |    500746 |   38989   136554 |   59224   37329  2280068    61.1 |  6.859 % |
c |    529939 |   38989   136554 |   65146   20419  1634904    80.1 |  6.859 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -s01_bit_10 -s01_bit_9 -s01_bit_8 -s01_bit_7 -s01_bit_6 -s01_bit_5 -s01_bit_4 -s01_bit_3 s01_bit_2 s01_bit_1 -s01_bit0 s01_bit1 s01_bit2 -s01_bit3 -s01_bit4 s01_bit5 -s01_bit6 s01_bit7 -s01_bit8 -s01_bit9 -s01_bit10 -s01_bit11 -s01_bit12 -s01_bit13 -s01_bit14 -s01_bit15 -s01_bit16 -s01_bit17 -s01_bit18 -s01_bit19 -s11_bit_10 -s11_bit_9 -s11_bit_8 -s11_bit_7 -s11_bit_6 -s11_bit_5 -s11_bit_4 -s11_bit_3 -s11_bit_2 s11_bit_1 -s11_bit0 -s11_bit1 s11_bit2 s11_bit3 -s11_bit4 -s11_bit5 -s11_bit6 -s11_bit7 -s11_bit8 -s11_bit9 -s11_bit10 -s11_bit11 -s11_bit12 -s11_bit13 -s11_bit14 -s11_bit15 -s11_bit16 -s11_bit17 -s11_bit18 -s11_bit19 -s21_bit_10 -s21_bit_9 -s21_bit_8 -s21_bit_7 -s21_bit_6 -s21_bit_5 -s21_bit_4 -s21_bit_3 s21_bit_2 s21_bit_1 -s21_bit0 s21_bit1 s21_bit2 -s21_bit3 s21_bit4 s21_bit5 -s21_bit6 -s21_bit7 -s21_bit8 -s21_bit9 -s21_bit10 -s21_bit11 -s21_bit12 -s21_bit13 -s21_bit14 -s21_bit15 -s21_bit16 -s21_bit17 -s21_bit18 -s21_bit19 -s31_bit_10 -s31_bit_9 -s31_bit_8 -s31_bit_7 -s31_bit_6 -s31_bit_5 -s31_bit_4 -s31_bit_3 -s31_bit_2 s31_bit_1 -s31_bit0 s31_bit1 s31_bit2 s31_bit3 -s31_bit4 s31_bit5 -s31_bit6 -s31_bit7 -s31_bit8 -s31_bit9 -s31_bit10 -s31_bit11 -s31_bit12 -s31_bit13 -s31_bit14 -s31_bit15 -s31_bit16 -s31_bit17 -s31_bit18 -s31_bit19 -s41_bit_10 -s41_bit_9 -s41_bit_8 -s41_bit_7 -s41_bit_6 -s41_bit_5 -s41_bit_4 -s41_bit_3 s41_bit_2 -s41_bit_1 s41_bit0 -s41_bit1 s41_bit2 s41_bit3 s41_bit4 -s41_bit5 -s41_bit6 s41_bit7 -s41_bit8 -s41_bit9 -s41_bit10 -s41_bit11 -s41_bit12 -s41_bit13 -s41_bit14 -s41_bit15 -s41_bit16 -s41_bit17 -s41_bit18 -s41_bit19 -s51_bit_10 -s51_bit_9 -s51_bit_8 -s51_bit_7 -s51_bit_6 -s51_bit_5 -s51_bit_4 -s51_bit_3 -s51_bit_2 -s51_bit_1 -s51_bit0 -s51_bit1 -s51_bit2 s51_bit3 s51_bit4 -s51_bit5 -s51_bit6 -s51_bit7 -s51_bit8 -s51_bit9 -s51_bit10 -s51_bit11 -s51_bit12 -s51_bit13 -s51_bit14 -s51_bit15 -s51_bit16 -s51_bit17 -s51_bit18 -s51_bit19 -s61_bit_10 -s61_bit_9 -s61_bit_8 -s61_bit_7 -s61_bit_6 -s61_bit_5 -s61_bit_4 -s61_bit_3 -s61_bit_2 s61_bit_1 -s61_bit0 -s61_bit1 -s61_bit2 -s61_bit3 -s61_bit4 -s61_bit5 s61_bit6 s61_bit7 -s61_bit8 -s61_bit9 -s61_bit10 -s61_bit11 -s61_bit12 -s61_bit13 -s61_bit14 -s61_bit15 -s61_bit16 -s61_bit17 -s61_bit18 -s61_bit19 x0_bit0 -x1_bit0 -x2_bit0 x3_bit0 -x4_bit0 -x5_bit0 -x6_bit0 -x7_bit0 -x8_bit0 -x9_bit0 x10_bit0 x11_bit0 -x12_bit0 -x13_bit0 x14_bit0 x15_bit0 x16_bit0 -x17_bit0 -x18_bit0 -x19_bit0 x20_bit0 x21_bit0 -x22_bit0 x23_bit0 x24_bit0 -x25_bit0 x26_bit0 -x27_bit0 -x28_bit0 x29_bit0 x30_bit0 x31_bit0 -x32_bit0 x33_bit0 x34_bit0 -x35_bit0 x36_bit0 x37_bit0 -x38_bit0 x39_bit0 -x40_bit0 -x41_bit0 x42_bit0 -x43_bit0 x44_bit0 -x45_bit0 x46_bit0 -x47_bit0 -x48_bit0 -x49_bit0 -x50_bit0 -x51_bit0 x52_bit0 -x53_bit0 -x54_bit_10 -x54_bit_9 -x54_bit_8 -x54_bit_7 -x54_bit_6 -x54_bit_5 -x54_bit_4 -x54_bit_3 -x54_bit_2 -x54_bit_1 x54_bit0 -x55_bit_10 -x55_bit_9 -x55_bit_8 -x55_bit_7 -x55_bit_6 -x55_bit_5 -x55_bit_4 -x55_bit_3 -x55_bit_2 -x55_bit_1 -x55_bit0 -x56_bit_10 -x56_bit_9 -x56_bit_8 -x56_bit_7 -x56_bi#### 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.84 0.94 0.91 2/55 6077
Raw data (stat): 6077 (runsolver) R 6076 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 548442477 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99965 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 6077
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 3030 0 0 0 990 7 0 0 25 0 1 0 548442477 11767808 2413 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2873 2413 603 41 0 2832 0
vsize: 11492
[startup+19.9991 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 6077
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 3848 0 0 0 1988 10 0 0 25 0 1 0 548442477 15114240 3231 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3690 3231 603 41 0 3649 0
vsize: 14760
[startup+30 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 6077
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 4236 0 0 0 2987 11 0 0 25 0 1 0 548442477 15933440 3432 4294967295 134512640 134672761 3221224528 3221223712 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3890 3432 603 41 0 3849 0
vsize: 15560
[startup+39.9993 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 6077
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 4613 0 0 0 3986 12 0 0 25 0 1 0 548442477 17649664 3809 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4309 3809 603 41 0 4268 0
vsize: 17236
[startup+50.0001 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 6077
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 5247 0 0 0 4984 14 0 0 25 0 1 0 548442477 20279296 4443 4294967295 134512640 134672761 3221224528 3221223728 134610644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4951 4443 603 41 0 4910 0
vsize: 19804
[startup+59.9998 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 6077
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 5837 0 0 0 5982 16 0 0 25 0 1 0 548442477 22650880 5033 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5530 5033 603 41 0 5489 0
vsize: 22120
[startup+69.9991 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 6077
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 6525 0 0 0 6980 18 0 0 25 0 1 0 548442477 25468928 5721 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6218 5721 603 41 0 6177 0
vsize: 24872
[startup+79.9997 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 6077
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 6525 0 0 0 7980 18 0 0 25 0 1 0 548442477 25468928 5721 4294967295 134512640 134672761 3221224528 3221223712 134615660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6218 5721 603 41 0 6177 0
vsize: 24872
[startup+89.9996 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 6077
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 6525 0 0 0 8980 18 0 0 25 0 1 0 548442477 25468928 5721 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6218 5721 603 41 0 6177 0
vsize: 24872
[startup+99.9999 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 6077
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 6525 0 0 0 9981 18 0 0 25 0 1 0 548442477 25468928 5721 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6218 5721 603 41 0 6177 0
vsize: 24872
[startup+110 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6079
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 6534 0 0 0 10981 18 0 0 25 0 1 0 548442477 25468928 5730 4294967295 134512640 134672761 3221224528 3221223712 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6218 5730 603 41 0 6177 0
vsize: 24872
[startup+119.999 s]
Raw data (loadavg): 1.23 1.02 0.93 2/55 6079
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 7003 0 0 0 11980 19 0 0 25 0 1 0 548442477 27443200 6199 4294967295 134512640 134672761 3221224528 3221223340 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6700 6199 603 41 0 6659 0
vsize: 26800
[startup+130 s]
Raw data (loadavg): 1.27 1.03 0.94 2/55 6079
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 7579 0 0 0 12979 20 0 0 25 0 1 0 548442477 29831168 6775 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7283 6775 603 41 0 7242 0
vsize: 29132
[startup+139.999 s]
Raw data (loadavg): 1.22 1.03 0.94 2/55 6079
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 8056 0 0 0 13978 21 0 0 25 0 1 0 548442477 31821824 7252 4294967295 134512640 134672761 3221224528 3221223712 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7769 7252 603 41 0 7728 0
vsize: 31076
[startup+150 s]
Raw data (loadavg): 1.19 1.03 0.94 2/55 6079
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 8566 0 0 0 14977 23 0 0 25 0 1 0 548442477 33796096 7762 4294967295 134512640 134672761 3221224528 3221223712 134615611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8251 7762 603 41 0 8210 0
vsize: 33004
[startup+160 s]
Raw data (loadavg): 1.16 1.03 0.94 2/55 6079
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 8944 0 0 0 15975 24 0 0 25 0 1 0 548442477 35651584 8140 4294967295 134512640 134672761 3221224528 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8704 8140 603 41 0 8663 0
vsize: 34816
[startup+169.999 s]
Raw data (loadavg): 1.13 1.03 0.94 2/55 6079
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 9059 0 0 0 16975 25 0 0 25 0 1 0 548442477 35725312 8190 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8722 8190 603 41 0 8681 0
vsize: 34888
[startup+180 s]
Raw data (loadavg): 1.11 1.03 0.94 2/55 6079
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 9059 0 0 0 17975 25 0 0 25 0 1 0 548442477 35725312 8190 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8722 8190 603 41 0 8681 0
vsize: 34888
[startup+189.999 s]
Raw data (loadavg): 1.10 1.02 0.94 2/55 6079
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 9059 0 0 0 18976 25 0 0 25 0 1 0 548442477 35725312 8190 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8722 8190 603 41 0 8681 0
vsize: 34888
[startup+199.999 s]
Raw data (loadavg): 1.08 1.02 0.94 2/55 6079
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 9059 0 0 0 19976 25 0 0 25 0 1 0 548442477 35725312 8190 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8722 8190 603 41 0 8681 0
vsize: 34888
[startup+210.006 s]
Raw data (loadavg): 1.07 1.02 0.94 2/55 6079
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 9059 0 0 0 20977 25 0 0 25 0 1 0 548442477 35725312 8190 4294967295 134512640 134672761 3221224528 3221223712 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8722 8190 603 41 0 8681 0
vsize: 34888
[startup+220.005 s]
Raw data (loadavg): 1.06 1.02 0.94 2/55 6079
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 9059 0 0 0 21977 25 0 0 25 0 1 0 548442477 35725312 8190 4294967295 134512640 134672761 3221224528 3221223520 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8722 8190 603 41 0 8681 0
vsize: 34888
[startup+230.006 s]
Raw data (loadavg): 1.05 1.02 0.94 2/55 6079
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 9059 0 0 0 22977 25 0 0 25 0 1 0 548442477 35725312 8190 4294967295 134512640 134672761 3221224528 3221223712 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8722 8190 603 41 0 8681 0
vsize: 34888
[startup+240.009 s]
Raw data (loadavg): 1.04 1.02 0.94 2/55 6079
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 9059 0 0 0 23977 25 0 0 25 0 1 0 548442477 35725312 8190 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8722 8190 603 41 0 8681 0
vsize: 34888
[startup+250.014 s]
Raw data (loadavg): 1.03 1.02 0.94 2/55 6079
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 9060 0 0 0 24977 25 0 0 25 0 1 0 548442477 35725312 8191 4294967295 134512640 134672761 3221224528 3221223568 134612701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8722 8191 603 41 0 8681 0
vsize: 34888
[startup+260.014 s]
Raw data (loadavg): 1.03 1.02 0.94 2/55 6079
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 9193 0 0 0 25977 26 0 0 25 0 1 0 548442477 36253696 8324 4294967295 134512640 134672761 3221224528 3221223712 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8851 8324 603 41 0 8810 0
vsize: 35404
[startup+270.014 s]
Raw data (loadavg): 1.02 1.02 0.94 2/55 6079
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 9495 0 0 0 26976 27 0 0 25 0 1 0 548442477 37150720 8552 4294967295 134512640 134672761 3221224528 3221223464 1075350544 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9070 8552 603 41 0 9029 0
vsize: 36280
[startup+280.014 s]
Raw data (loadavg): 1.02 1.02 0.94 2/55 6079
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 9495 0 0 0 27976 27 0 0 25 0 1 0 548442477 37150720 8552 4294967295 134512640 134672761 3221224528 3221223712 134615689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9070 8552 603 41 0 9029 0
vsize: 36280
[startup+290.013 s]
Raw data (loadavg): 1.02 1.01 0.94 2/55 6079
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 9495 0 0 0 28976 27 0 0 25 0 1 0 548442477 37150720 8552 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9070 8552 603 41 0 9029 0
vsize: 36280
[startup+300.013 s]
Raw data (loadavg): 1.01 1.01 0.94 2/55 6079
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 9496 0 0 0 29976 27 0 0 25 0 1 0 548442477 37150720 8553 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9070 8553 603 41 0 9029 0
vsize: 36280
[startup+310.014 s]
Raw data (loadavg): 1.01 1.01 0.94 2/55 6079
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 9496 0 0 0 30977 27 0 0 25 0 1 0 548442477 37150720 8553 4294967295 134512640 134672761 3221224528 3221223712 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9070 8553 603 41 0 9029 0
vsize: 36280
[startup+320.014 s]
Raw data (loadavg): 1.01 1.01 0.94 2/55 6079
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 9496 0 0 0 31977 27 0 0 25 0 1 0 548442477 37150720 8553 4294967295 134512640 134672761 3221224528 3221223712 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9070 8553 603 41 0 9029 0
vsize: 36280
[startup+330.014 s]
Raw data (loadavg): 1.01 1.01 0.94 2/55 6079
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 9496 0 0 0 32977 27 0 0 25 0 1 0 548442477 37150720 8553 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9070 8553 603 41 0 9029 0
vsize: 36280
[startup+340.014 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 6079
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 9496 0 0 0 33977 27 0 0 25 0 1 0 548442477 37150720 8553 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9070 8553 603 41 0 9029 0
vsize: 36280
[startup+350.014 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 6079
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 9497 0 0 0 34977 27 0 0 25 0 1 0 548442477 37150720 8554 4294967295 134512640 134672761 3221224528 3221223712 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9070 8554 603 41 0 9029 0
vsize: 36280
[startup+360.014 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 6079
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 9497 0 0 0 35977 27 0 0 25 0 1 0 548442477 37150720 8554 4294967295 134512640 134672761 3221224528 3221223712 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9070 8554 603 41 0 9029 0
vsize: 36280
[startup+370.014 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 6079
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 9497 0 0 0 36978 27 0 0 25 0 1 0 548442477 37150720 8554 4294967295 134512640 134672761 3221224528 3221223712 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9070 8554 603 41 0 9029 0
vsize: 36280
[startup+380.014 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 6079
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 9497 0 0 0 37978 27 0 0 25 0 1 0 548442477 37150720 8554 4294967295 134512640 134672761 3221224528 3221223712 134615994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9070 8554 603 41 0 9029 0
vsize: 36280
[startup+390.016 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6079
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 9497 0 0 0 38978 27 0 0 25 0 1 0 548442477 37150720 8554 4294967295 134512640 134672761 3221224528 3221223712 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9070 8554 603 41 0 9029 0
vsize: 36280
[startup+400.023 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6079
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 9781 0 0 0 39978 28 0 0 25 0 1 0 548442477 38350848 8838 4294967295 134512640 134672761 3221224528 3221223712 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9363 8838 603 41 0 9322 0
vsize: 37452
[startup+410.023 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6081
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 10446 0 0 0 40976 30 0 0 25 0 1 0 548442477 41119744 9503 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10039 9503 603 41 0 9998 0
vsize: 40156
[startup+420.036 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6081
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 11133 0 0 0 41975 33 0 0 25 0 1 0 548442477 43880448 10190 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10713 10190 603 41 0 10672 0
vsize: 42852
[startup+430.036 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6081
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 11778 0 0 0 42974 35 0 0 25 0 1 0 548442477 46522368 10835 4294967295 134512640 134672761 3221224528 3221223568 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11358 10835 603 41 0 11317 0
vsize: 45432
[startup+440.036 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6081
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 12303 0 0 0 43973 36 0 0 25 0 1 0 548442477 48390144 11247 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11814 11247 603 41 0 11773 0
vsize: 47256
[startup+450.036 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6081
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 12304 0 0 0 44973 36 0 0 25 0 1 0 548442477 48390144 11248 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11814 11248 603 41 0 11773 0
vsize: 47256
[startup+460.037 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6081
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 12304 0 0 0 45973 36 0 0 25 0 1 0 548442477 48390144 11248 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11814 11248 603 41 0 11773 0
vsize: 47256
[startup+470.036 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6081
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 12304 0 0 0 46973 36 0 0 25 0 1 0 548442477 48390144 11248 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11814 11248 603 41 0 11773 0
vsize: 47256
[startup+480.036 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6081
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 12304 0 0 0 47973 36 0 0 25 0 1 0 548442477 48390144 11248 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11814 11248 603 41 0 11773 0
vsize: 47256
[startup+490.036 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6081
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 12304 0 0 0 48973 36 0 0 25 0 1 0 548442477 48390144 11248 4294967295 134512640 134672761 3221224528 3221223712 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11814 11248 603 41 0 11773 0
vsize: 47256
[startup+500.035 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6081
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 12304 0 0 0 49974 36 0 0 25 0 1 0 548442477 48390144 11248 4294967295 134512640 134672761 3221224528 3221223712 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11814 11248 603 41 0 11773 0
vsize: 47256
[startup+510.035 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6081
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 12304 0 0 0 50974 36 0 0 25 0 1 0 548442477 48390144 11248 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11814 11248 603 41 0 11773 0
vsize: 47256
[startup+520.039 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6081
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 12304 0 0 0 51974 36 0 0 25 0 1 0 548442477 48390144 11248 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11814 11248 603 41 0 11773 0
vsize: 47256
[startup+530.044 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6081
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 12304 0 0 0 52975 36 0 0 25 0 1 0 548442477 48390144 11248 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11814 11248 603 41 0 11773 0
vsize: 47256
[startup+540.044 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6081
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 12304 0 0 0 53975 36 0 0 25 0 1 0 548442477 48390144 11248 4294967295 134512640 134672761 3221224528 3221223712 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11814 11248 603 41 0 11773 0
vsize: 47256
[startup+550.048 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6081
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 12304 0 0 0 54976 36 0 0 25 0 1 0 548442477 48390144 11248 4294967295 134512640 134672761 3221224528 3221223712 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11814 11248 603 41 0 11773 0
vsize: 47256
[startup+560.048 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6081
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 12304 0 0 0 55976 36 0 0 25 0 1 0 548442477 48390144 11248 4294967295 134512640 134672761 3221224528 3221223712 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11814 11248 603 41 0 11773 0
vsize: 47256
[startup+570.047 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6081
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 12304 0 0 0 56976 36 0 0 25 0 1 0 548442477 48390144 11248 4294967295 134512640 134672761 3221224528 3221223712 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11814 11248 603 41 0 11773 0
vsize: 47256
[startup+580.052 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6081
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 12304 0 0 0 57976 36 0 0 25 0 1 0 548442477 48390144 11248 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11814 11248 603 41 0 11773 0
vsize: 47256
[startup+590.053 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6081
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 12304 0 0 0 58977 36 0 0 25 0 1 0 548442477 48390144 11248 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11814 11248 603 41 0 11773 0
vsize: 47256
[startup+600.159 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6081
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 12304 0 0 0 59988 36 0 0 25 0 1 0 548442477 48390144 11248 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11814 11248 603 41 0 11773 0
vsize: 47256
[startup+610.159 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6081
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 12845 0 0 0 60986 38 0 0 25 0 1 0 548442477 50647040 11789 4294967295 134512640 134672761 3221224528 3221223568 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12365 11789 603 41 0 12324 0
vsize: 49460
[startup+620.16 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6081
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 13307 0 0 0 61985 39 0 0 25 0 1 0 548442477 52637696 12251 4294967295 134512640 134672761 3221224528 3221223712 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12851 12251 603 41 0 12810 0
vsize: 51404
[startup+630.164 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6081
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 13730 0 0 0 62984 40 0 0 25 0 1 0 548442477 53915648 12594 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13163 12594 603 41 0 13122 0
vsize: 52652
[startup+640.181 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6081
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 13730 0 0 0 63986 41 0 0 25 0 1 0 548442477 53915648 12594 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13163 12594 603 41 0 13122 0
vsize: 52652
[startup+650.213 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6081
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 13730 0 0 0 64990 41 0 0 25 0 1 0 548442477 53915648 12594 4294967295 134512640 134672761 3221224528 3221223492 1075346947 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13163 12594 603 41 0 13122 0
vsize: 52652
[startup+660.218 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6081
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 13730 0 0 0 65990 41 0 0 25 0 1 0 548442477 53915648 12594 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13163 12594 603 41 0 13122 0
vsize: 52652
[startup+670.231 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6081
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 13730 0 0 0 66992 41 0 0 25 0 1 0 548442477 53915648 12594 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13163 12594 603 41 0 13122 0
vsize: 52652
[startup+680.231 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6081
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 13730 0 0 0 67992 41 0 0 25 0 1 0 548442477 53915648 12594 4294967295 134512640 134672761 3221224528 3221223712 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13163 12594 603 41 0 13122 0
vsize: 52652
[startup+690.231 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6081
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 13730 0 0 0 68992 41 0 0 25 0 1 0 548442477 53915648 12594 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13163 12594 603 41 0 13122 0
vsize: 52652
[startup+700.235 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6081
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 13730 0 0 0 69993 41 0 0 25 0 1 0 548442477 53915648 12594 4294967295 134512640 134672761 3221224528 3221223712 134615643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13163 12594 603 41 0 13122 0
vsize: 52652
[startup+710.235 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6083
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 13730 0 0 0 70993 41 0 0 25 0 1 0 548442477 53915648 12594 4294967295 134512640 134672761 3221224528 3221223712 134616005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13163 12594 603 41 0 13122 0
vsize: 52652
[startup+720.235 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6083
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 13730 0 0 0 71993 41 0 0 25 0 1 0 548442477 53915648 12594 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13163 12594 603 41 0 13122 0
vsize: 52652
[startup+730.235 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6083
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 13730 0 0 0 72993 41 0 0 25 0 1 0 548442477 53915648 12594 4294967295 134512640 134672761 3221224528 3221223712 134615591 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13163 12594 603 41 0 13122 0
vsize: 52652
[startup+740.236 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6083
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 13730 0 0 0 73993 41 0 0 25 0 1 0 548442477 53915648 12594 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13163 12594 603 41 0 13122 0
vsize: 52652
[startup+750.236 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6083
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 13730 0 0 0 74994 41 0 0 25 0 1 0 548442477 53915648 12594 4294967295 134512640 134672761 3221224528 3221223712 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13163 12594 603 41 0 13122 0
vsize: 52652
[startup+760.236 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6083
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 13730 0 0 0 75994 41 0 0 25 0 1 0 548442477 53915648 12594 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13163 12594 603 41 0 13122 0
vsize: 52652
[startup+770.236 s]
Raw data (loadavg): 1.00 1.00 0.94 3/57 6106
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 13730 0 0 0 76994 41 0 0 25 0 1 0 548442477 53915648 12594 4294967295 134512640 134672761 3221224528 3221223664 134614756 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13163 12594 603 41 0 13122 0
vsize: 52652
[startup+780.236 s]
Raw data (loadavg): 1.07 1.02 0.94 2/55 6136
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 13815 0 0 0 77994 41 0 0 25 0 1 0 548442477 54300672 12679 4294967295 134512640 134672761 3221224528 3221223568 134612827 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13257 12680 603 41 0 13216 0
vsize: 53028
[startup+790.236 s]
Raw data (loadavg): 1.06 1.02 0.94 2/55 6136
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 14113 0 0 0 78992 42 0 0 25 0 1 0 548442477 55619584 12977 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13579 12977 603 41 0 13538 0
vsize: 54316
[startup+800.236 s]
Raw data (loadavg): 1.05 1.01 0.94 2/55 6136
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 14386 0 0 0 79992 43 0 0 25 0 1 0 548442477 56672256 13250 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13836 13250 603 41 0 13795 0
vsize: 55344
[startup+810.236 s]
Raw data (loadavg): 1.04 1.01 0.94 2/55 6136
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 14722 0 0 0 80991 44 0 0 25 0 1 0 548442477 58015744 13586 4294967295 134512640 134672761 3221224528 3221223712 134615830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14164 13586 603 41 0 14123 0
vsize: 56656
[startup+820.236 s]
Raw data (loadavg): 1.04 1.01 0.94 2/55 6136
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 14995 0 0 0 81991 44 0 0 25 0 1 0 548442477 59195392 13859 4294967295 134512640 134672761 3221224528 3221223712 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14452 13859 603 41 0 14411 0
vsize: 57808
[startup+830.236 s]
Raw data (loadavg): 1.03 1.01 0.94 2/55 6136
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 15270 0 0 0 82990 45 0 0 25 0 1 0 548442477 60395520 14134 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14745 14134 603 41 0 14704 0
vsize: 58980
[startup+840.236 s]
Raw data (loadavg): 1.02 1.01 0.94 2/55 6136
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 15591 0 0 0 83989 47 0 0 25 0 1 0 548442477 61706240 14455 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15065 14455 603 41 0 15024 0
vsize: 60260
[startup+850.237 s]
Raw data (loadavg): 1.02 1.01 0.94 2/55 6138
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 15957 0 0 0 84989 47 0 0 25 0 1 0 548442477 63229952 14821 4294967295 134512640 134672761 3221224528 3221223712 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15437 14821 603 41 0 15396 0
vsize: 61748
[startup+860.237 s]
Raw data (loadavg): 1.02 1.01 0.94 2/55 6138
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 16280 0 0 0 85988 48 0 0 25 0 1 0 548442477 64557056 15144 4294967295 134512640 134672761 3221224528 3221223652 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15761 15144 603 41 0 15720 0
vsize: 63044
[startup+870.237 s]
Raw data (loadavg): 1.01 1.01 0.94 2/55 6138
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 16547 0 0 0 86988 49 0 0 25 0 1 0 548442477 65622016 15411 4294967295 134512640 134672761 3221224528 3221223712 134615585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16021 15411 603 41 0 15980 0
vsize: 64084
[startup+880.238 s]
Raw data (loadavg): 1.01 1.01 0.94 2/55 6138
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 16883 0 0 0 87986 50 0 0 25 0 1 0 548442477 67063808 15747 4294967295 134512640 134672761 3221224528 3221223360 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16373 15747 603 41 0 16332 0
vsize: 65492
[startup+890.237 s]
Raw data (loadavg): 1.01 1.01 0.94 2/55 6138
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 17238 0 0 0 88985 52 0 0 25 0 1 0 548442477 68501504 16102 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16724 16102 603 41 0 16683 0
vsize: 66896
[startup+900.238 s]
Raw data (loadavg): 1.01 1.00 0.94 2/55 6138
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 17618 0 0 0 89985 53 0 0 25 0 1 0 548442477 69492736 16361 4294967295 134512640 134672761 3221224528 3221223712 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16966 16361 603 41 0 16925 0
vsize: 67864
[startup+910.237 s]
Raw data (loadavg): 1.01 1.00 0.94 2/55 6138
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 17618 0 0 0 90985 53 0 0 25 0 1 0 548442477 69492736 16361 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16966 16361 603 41 0 16925 0
vsize: 67864
[startup+920.237 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6138
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 17618 0 0 0 91985 53 0 0 25 0 1 0 548442477 69492736 16361 4294967295 134512640 134672761 3221224528 3221223712 134615611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16966 16361 603 41 0 16925 0
vsize: 67864
[startup+930.237 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6138
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 17618 0 0 0 92985 53 0 0 25 0 1 0 548442477 69492736 16361 4294967295 134512640 134672761 3221224528 3221223712 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16966 16361 603 41 0 16925 0
vsize: 67864
[startup+940.237 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6138
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 17618 0 0 0 93985 53 0 0 25 0 1 0 548442477 69492736 16361 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16966 16361 603 41 0 16925 0
vsize: 67864
[startup+950.245 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6138
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 17618 0 0 0 94986 53 0 0 25 0 1 0 548442477 69492736 16361 4294967295 134512640 134672761 3221224528 3221223680 134565098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16966 16361 603 41 0 16925 0
vsize: 67864
[startup+960.247 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6138
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 17618 0 0 0 95986 53 0 0 25 0 1 0 548442477 69492736 16361 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16966 16361 603 41 0 16925 0
vsize: 67864
[startup+970.247 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6138
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 17618 0 0 0 96987 53 0 0 25 0 1 0 548442477 69492736 16361 4294967295 134512640 134672761 3221224528 3221223712 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16966 16361 603 41 0 16925 0
vsize: 67864
[startup+980.255 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6138
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 17618 0 0 0 97987 53 0 0 25 0 1 0 548442477 69492736 16361 4294967295 134512640 134672761 3221224528 3221223664 134614505 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16966 16361 603 41 0 16925 0
vsize: 67864
[startup+990.262 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6138
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 17749 0 0 0 98986 54 0 0 25 0 1 0 548442477 69443584 16352 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16954 16352 603 41 0 16913 0
vsize: 67816
[startup+1000.26 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6138
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 17749 0 0 0 99986 54 0 0 25 0 1 0 548442477 69443584 16352 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16954 16352 603 41 0 16913 0
vsize: 67816
[startup+1010.26 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6140
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 17861 0 0 0 100985 55 0 0 25 0 1 0 548442477 69443584 16353 4294967295 134512640 134672761 3221224528 3221223520 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16954 16353 603 41 0 16913 0
vsize: 67816
[startup+1020.27 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6140
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 17861 0 0 0 101986 55 0 0 25 0 1 0 548442477 69443584 16353 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16954 16353 603 41 0 16913 0
vsize: 67816
[startup+1030.27 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6140
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 17861 0 0 0 102987 55 0 0 25 0 1 0 548442477 69443584 16353 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16954 16353 603 41 0 16913 0
vsize: 67816
[startup+1040.27 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6140
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 17861 0 0 0 103987 55 0 0 25 0 1 0 548442477 69443584 16353 4294967295 134512640 134672761 3221224528 3221223712 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16954 16353 603 41 0 16913 0
vsize: 67816
[startup+1050.27 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6140
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 17861 0 0 0 104987 55 0 0 25 0 1 0 548442477 69443584 16353 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16954 16353 603 41 0 16913 0
vsize: 67816
[startup+1060.28 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6140
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 17861 0 0 0 105987 55 0 0 25 0 1 0 548442477 69443584 16353 4294967295 134512640 134672761 3221224528 3221223712 134615673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16954 16353 603 41 0 16913 0
vsize: 67816
[startup+1070.27 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6140
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 17861 0 0 0 106987 55 0 0 25 0 1 0 548442477 69443584 16353 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16954 16353 603 41 0 16913 0
vsize: 67816
[startup+1080.28 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6140
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 17861 0 0 0 107987 55 0 0 25 0 1 0 548442477 69443584 16353 4294967295 134512640 134672761 3221224528 3221223712 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16954 16353 603 41 0 16913 0
vsize: 67816
[startup+1090.28 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6140
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 17861 0 0 0 108988 55 0 0 25 0 1 0 548442477 69443584 16353 4294967295 134512640 134672761 3221224528 3221223712 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16954 16353 603 41 0 16913 0
vsize: 67816
[startup+1100.28 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6142
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 17911 0 0 0 109988 55 0 0 25 0 1 0 548442477 69443584 16353 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16954 16353 603 41 0 16913 0
vsize: 67816
[startup+1110.28 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6142
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 17911 0 0 0 110988 55 0 0 25 0 1 0 548442477 69443584 16353 4294967295 134512640 134672761 3221224528 3221223520 134565064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16954 16353 603 41 0 16913 0
vsize: 67816
[startup+1120.28 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6142
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 17911 0 0 0 111988 55 0 0 25 0 1 0 548442477 69443584 16353 4294967295 134512640 134672761 3221224528 3221223712 134616014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16954 16353 603 41 0 16913 0
vsize: 67816
[startup+1130.28 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6142
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 17911 0 0 0 112988 55 0 0 25 0 1 0 548442477 69443584 16353 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16954 16353 603 41 0 16913 0
vsize: 67816
[startup+1140.28 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6142
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 17911 0 0 0 113988 55 0 0 25 0 1 0 548442477 69443584 16353 4294967295 134512640 134672761 3221224528 3221223712 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16954 16353 603 41 0 16913 0
vsize: 67816
[startup+1150.28 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6142
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 17911 0 0 0 114989 55 0 0 25 0 1 0 548442477 69443584 16353 4294967295 134512640 134672761 3221224528 3221223712 134615830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16954 16353 603 41 0 16913 0
vsize: 67816
[startup+1160.28 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6142
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 17971 0 0 0 115989 55 0 0 25 0 1 0 548442477 69443584 16353 4294967295 134512640 134672761 3221224528 3221223712 134615643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16954 16353 603 41 0 16913 0
vsize: 67816
[startup+1170.28 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6142
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 17971 0 0 0 116989 55 0 0 25 0 1 0 548442477 69394432 16341 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16942 16341 603 41 0 16901 0
vsize: 67768
[startup+1180.28 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6142
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 17971 0 0 0 117989 55 0 0 25 0 1 0 548442477 69394432 16341 4294967295 134512640 134672761 3221224528 3221223728 134610614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16942 16341 603 41 0 16901 0
vsize: 67768
[startup+1190.28 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6142
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 17971 0 0 0 118989 55 0 0 25 0 1 0 548442477 69394432 16341 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16942 16341 603 41 0 16901 0
vsize: 67768
[startup+1200.28 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 6142
Raw data (stat): 6077 (minisat+) R 6076 20838 20837 0 -1 0 17971 0 0 0 119990 55 0 0 25 0 1 0 548442477 69394432 16341 4294967295 134512640 134672761 3221224528 3221223568 134612696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16942 16341 603 41 0 16901 0
vsize: 67768
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.31 s]
Raw data (loadavg): 1.00 1.00 0.94 1/55 6142
Raw data (stat): 6077 (minisat+) Z 6076 20838 20837 0 -1 12 17972 0 0 0 119990 59 0 0 25 0 1 0 548442477 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.31
CPU time (s): 1200.49
CPU user time (s): 1199.9
CPU system time (s): 0.59091
CPU usage (%): 100.015
Max. virtual memory (Kb): 67864
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####