PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-gr4x6.opb
MD5SUM	c1c7537cd9b3e10215a81ec1ca3be5cb
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2605440
Optimality of the best value was proved	NO
Number of terms in the objective function	504
Biggest coefficient in the objective function	148373504
Number of bits for the biggest coefficient in the objective function	28
Sum of the numbers in the objective function	3393589600
Number of bits of the sum of numbers in the objective function	32
Biggest number in a constraint	148373504
Number of bits of the biggest number in a constraint	28
Biggest sum of numbers in a constraint	3393589600
Number of bits of the biggest sum of numbers	32
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.01
Number of variables	504
Total number of constraints	34
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	34
Minimum length of a constraint	21
Maximum length of a constraint	120
Trace number 17850

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-04-21 12:23:06 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18990 boxname=wulflinc1 idbench=1461 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c1c7537cd9b3e10215a81ec1ca3be5cb  /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-gr4x6.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-gr4x6.opb /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-gr4x6.opb
IDLAUNCH: 18990
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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	: 2
cpu MHz		: 451.053
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:        779388 kB
Buffers:          3552 kB
Cached:         226764 kB
SwapCached:          0 kB
Active:          48448 kB
Inactive:       185012 kB
HighTotal:      131008 kB
HighFree:        49224 kB
LowTotal:       903652 kB
LowFree:        730164 kB
SwapTotal:     2097136 kB
SwapFree:      2096968 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7220 kB
Slab:            16044 kB
Committed_AS:    92820 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 12:43:08 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 18990 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 44 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##########
c   -- Clauses(.)/Splits(s): (none)
c ---[  42]---> Adder-cost: 114   maxlim: 14714   bits: 15/14
c ---[  40]---> Adder-cost: 114   maxlim: 15994   bits: 15/14
c ---[  38]---> Adder-cost: 110   maxlim: 13818   bits: 14/14
c ---[  36]---> Adder-cost: 108   maxlim: 8314   bits: 14/14
c ---[  34]---> Adder-cost: 76   maxlim: 18044   bits: 15/15
c ---[  32]---> Adder-cost: 72   maxlim: 10492   bits: 14/14
c ---[  30]---> Adder-cost: 72   maxlim: 11132   bits: 14/14
c ---[  28]---> Adder-cost: 66   maxlim: 6268   bits: 13/13
c ---[  26]---> Adder-cost: 60   maxlim: 3452   bits: 12/12
c ---[  24]---> Adder-cost: 60   maxlim: 3452   bits: 12/12
c ---[  23]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  22]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  21]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  20]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  19]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  18]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  17]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  16]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  15]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  14]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  13]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  12]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  11]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  10]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   9]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   8]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[   7]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[   6]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   5]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[   4]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[   3]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[   2]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[   1]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[   0]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    6403    23572 |    2134       0        0     nan |  0.000 % |
c |       100 |    6371    23468 |    2347      96      474     4.9 | 39.214 % |
c |       250 |    6356    23421 |    2582     245     1156     4.7 | 39.369 % |
c |       475 |    6340    23369 |    2840     467     2188     4.7 | 39.524 % |
c |       812 |    6302    23247 |    3124     799     3914     4.9 | 39.886 % |
c |      1318 |    6302    23247 |    3436    1305     7315     5.6 | 39.886 % |
c |      2077 |    6293    23218 |    3780    2063    13300     6.4 | 39.990 % |
c ==============================================================================
c [1mFound solution: 6122733[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2190   maxlim: 5736563   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2376 |   21507    77582 |    7169    2362    15580     6.6 | 39.990 % |
c |      2476 |   21507    77582 |    7885    2462    16329     6.6 | 18.974 % |
c ==============================================================================
c [1mFound solution: 5825217[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 6034079   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2570 |   21523    77696 |    7174    2556    16965     6.6 | 18.974 % |
c |      2671 |   21523    77696 |    7891    2657    17698     6.7 | 19.091 % |
c |      2821 |   21523    77696 |    8680    2807    19081     6.8 | 19.091 % |
c |      3048 |   21523    77696 |    9548    3034    26702     8.8 | 19.091 % |
c |      3386 |   21523    77696 |   10503    3372    29942     8.9 | 19.091 % |
c ==============================================================================
c [1mFound solution: 5523396[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 6335900   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3648 |   21558    77965 |    7186    3634    33003     9.1 | 19.091 % |
c |      3749 |   21558    77965 |    7904    3735    34053     9.1 | 19.297 % |
c |      3899 |   21558    77965 |    8695    3885    35595     9.2 | 19.297 % |
c |      4124 |   21558    77965 |    9564    4110    41065    10.0 | 19.297 % |
c ==============================================================================
c [1mFound solution: 4832915[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7026381   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4440 |   21571    78152 |    7190    4426    47088    10.6 | 19.297 % |
c |      4540 |   21571    78152 |    7909    4526    49143    10.9 | 19.525 % |
c ==============================================================================
c [1mFound solution: 4735459[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7123837   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4583 |   21591    78372 |    7197    4569    50088    11.0 | 19.525 % |
c |      4683 |   21591    78372 |    7916    4669    51235    11.0 | 19.718 % |
c |      4833 |   21591    78372 |    8708    4819    73980    15.4 | 19.718 % |
c |      5058 |   21591    78372 |    9579    5044    77578    15.4 | 19.718 % |
c |      5395 |   21591    78372 |   10537    5381    85526    15.9 | 19.718 % |
c |      5902 |   21591    78372 |   11590    5888   120742    20.5 | 19.718 % |
c |      6662 |   21591    78372 |   12749    6648   200551    30.2 | 19.718 % |
c ==============================================================================
c [1mFound solution: 4593765[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7265531   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7034 |   21611    78589 |    7203    7020   207237    29.5 | 19.718 % |
c |      7134 |   21611    78589 |    7923    7120   219943    30.9 | 19.929 % |
c |      7284 |   21611    78589 |    8715    7270   221256    30.4 | 19.929 % |
c |      7509 |   21611    78589 |    9587    7495   235583    31.4 | 19.929 % |
c |      7846 |   21611    78589 |   10545    7832   257954    32.9 | 19.929 % |
c ==============================================================================
c [1mFound solution: 3854040[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 8005256   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8129 |   21625    78725 |    7208    8115   263974    32.5 | 19.929 % |
c |      8230 |   21625    78725 |    7928    4159   149490    35.9 | 20.076 % |
c |      8380 |   21625    78725 |    8721    4309   151460    35.1 | 20.076 % |
c |      8605 |   21625    78725 |    9593    4534   160331    35.4 | 20.076 % |
c |      8944 |   21625    78725 |   10553    4873   173060    35.5 | 20.076 % |
c |      9451 |   21625    78725 |   11608    5380   183701    34.1 | 20.076 % |
c |     10211 |   21625    78725 |   12769    6140   208793    34.0 | 20.076 % |
c |     11352 |   21625    78725 |   14046    7281   322521    44.3 | 20.076 % |
c |     13061 |   21625    78725 |   15450    8990   530459    59.0 | 20.076 % |
c |     15623 |   21619    78708 |   16996   11543   764613    66.2 | 20.100 % |
c |     19467 |   21619    78708 |   18695   15387  1260359    81.9 | 20.100 % |
c |     25233 |   21619    78708 |   20565   11020  1000005    90.7 | 20.100 % |
c |     33884 |   21619    78708 |   22621   19671  1724919    87.7 | 20.100 % |
c |     46859 |   21619    78708 |   24883   20766   915356    44.1 | 20.100 % |
c ==============================================================================
c [1mFound solution: 3662453[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 8196843   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46949 |   21635    78865 |    7211   20856   917327    44.0 | 20.100 % |
c |     47050 |   21635    78865 |    7932    5315   142136    26.7 | 20.236 % |
c |     47200 |   21635    78865 |    8725    5465   143289    26.2 | 20.236 % |
c |     47425 |   21635    78865 |    9597    5690   146229    25.7 | 20.236 % |
c |     47762 |   21635    78865 |   10557    6027   156578    26.0 | 20.236 % |
c |     48268 |   21635    78865 |   11613    6533   168527    25.8 | 20.236 % |
c |     49028 |   21635    78865 |   12774    7293   184505    25.3 | 20.236 % |
c |     50167 |   21635    78865 |   14052    8432   354219    42.0 | 20.236 % |
c |     51878 |   21635    78865 |   15457   10143   434668    42.9 | 20.236 % |
c |     54442 |   21635    78865 |   17003   12707   587089    46.2 | 20.236 % |
c |     58286 |   21635    78865 |   18703   16551  1033586    62.4 | 20.236 % |
c |     64053 |   21635    78865 |   20573   11706  1119531    95.6 | 20.236 % |
c |     72703 |   21635    78865 |   22631   20356  2068027   101.6 | 20.236 % |
c |     85677 |   21635    78865 |   24894   20721  2597160   125.3 | 20.236 % |
c |    105138 |   21635    78865 |   27383   26264  1841809    70.1 | 20.236 % |
c |    134331 |   21635    78865 |   30122   26245  2479170    94.5 | 20.236 % |
c |    178120 |   21635    78865 |   33134   19882  1828734    92.0 | 20.236 % |
c |    243804 |   21635    78865 |   36447   27042  1819816    67.3 | 20.236 % |
c ==============================================================================
c [1mFound solution: 3659903[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 8199393   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    285063 |   21646    78982 |    7215   20208  3539248   175.1 | 20.236 % |
c |    285163 |   21646    78982 |    7936    5152   476264    92.4 | 20.325 % |
c |    285314 |   21646    78982 |    8730    5303   477244    90.0 | 20.325 % |
c |    285540 |   21646    78982 |    9603    5529   479227    86.7 | 20.325 % |
c |    285877 |   21646    78982 |   10563    5866   503383    85.8 | 20.325 % |
c |    286383 |   21646    78982 |   11619    6372   524422    82.3 | 20.325 % |
c |    287143 |   21646    78982 |   12781    7132   569583    79.9 | 20.325 % |
c |    288283 |   21646    78982 |   14059    8272   607213    73.4 | 20.325 % |
c |    289991 |   21646    78982 |   15465    9980   662028    66.3 | 20.325 % |
c |    292554 |   21646    78982 |   17012   12543   750130    59.8 | 20.325 % |
c |    296399 |   21638    78960 |   18713   16387   936050    57.1 | 20.373 % |
c ==============================================================================
c [1mFound solution: 3619559[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 8239737   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    296948 |   21654    79137 |    7218   16936   949328    56.1 | 20.373 % |
c |    297048 |   21654    79137 |    7939    4334   139957    32.3 | 20.531 % |
c |    297198 |   21654    79137 |    8733    4484   142416    31.8 | 20.531 % |
c |    297424 |   21654    79137 |    9607    4710   147871    31.4 | 20.531 % |
c |    297761 |   21654    79137 |   10567    5047   196233    38.9 | 20.531 % |
c |    298268 |   21654    79137 |   11624    5554   251201    45.2 | 20.531 % |
c |    299027 |   21654    79137 |   12787    6313   330776    52.4 | 20.531 % |
c |    300167 |   21654    79137 |   14065    7453   408567    54.8 | 20.531 % |
c |    301876 |   21654    79137 |   15472    9162   530966    58.0 | 20.531 % |
c |    304438 |   21654    79137 |   17019   11724   826627    70.5 | 20.531 % |
c |    308285 |   21654    79137 |   18721   15571   936410    60.1 | 20.531 % |
c ==============================================================================
c [1mFound solution: 3083963[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 8775333   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    308658 |   21567    77835 |    7189   14809   915619    61.8 | 20.531 % |
c |    308758 |   21567    77835 |    7907    7505   278505    37.1 | 20.777 % |
c |    308908 |   21567    77835 |    8698    7655   280923    36.7 | 20.777 % |
c ==============================================================================
c [1mFound solution: 2976000[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 8883296   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    309087 |   21583    77952 |    7194    7834   285403    36.4 | 20.777 % |
c |    309187 |   21583    77952 |    7913    7934   292076    36.8 | 20.886 % |
c |    309337 |   21583    77952 |    8704    8084   293512    36.3 | 20.886 % |
c |    309562 |   21583    77952 |    9575    8309   297529    35.8 | 20.886 % |
c |    309899 |   21583    77952 |   10532    8646   304895    35.3 | 20.886 % |
c |    310405 |   21583    77952 |   11586    9152   316183    34.5 | 20.886 % |
c |    311165 |   21583    77952 |   12744    9912   337421    34.0 | 20.886 % |
c |    312304 |   21583    77952 |   14019   11051   398235    36.0 | 20.886 % |
c |    314016 |   21583    77952 |   15420   12763   454138    35.6 | 20.886 % |
c |    316578 |   21583    77952 |   16963   15325   548630    35.8 | 20.886 % |
c |    320424 |   21583    77952 |   18659   10173   249897    24.6 | 20.886 % |
c |    326191 |   21583    77952 |   20525   15940   476326    29.9 | 20.886 % |
c |    334842 |   21583    77952 |   22577   13718   506798    36.9 | 20.886 % |
c |    347818 |   21583    77952 |   24835   14649   971340    66.3 | 20.886 % |
c |    367279 |   21583    77952 |   27319   20666  1253617    60.7 | 20.886 % |
c |    396474 |   21583    77952 |   30051   21155  1037976    49.1 | 20.886 % |
c |    440263 |   21583    77952 |   33056   17673   705521    39.9 | 20.886 % |
c |    505947 |   21583    77952 |   36361   30427  1177558    38.7 | 20.886 % |
c |    604474 |   21583    77952 |   39998   28597  1036903    36.3 | 20.886 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -X0_bit_7 -X0_bit_6 -X0_bit_5 -X0_bit_4 -X0_bit_3 -X0_bit_2 -X0_bit_1 -X0_bit0 -X0_bit1 X0_bit2 -X0_bit3 X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X1_bit_7 -X1_bit_6 -X1_bit_5 -X1_bit_4 -X1_bit_3 -X1_bit_2 -X1_bit_1 -X1_bit0 -X1_bit1 X1_bit2 -X1_bit3 X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 -X2_bit_7 -X2_bit_6 -X2_bit_5 -X2_bit_4 -X2_bit_3 -X2_bit_2 -X2_bit_1 -X2_bit0 -X2_bit1 -X2_bit2 -X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 -X3_bit_7 -X3_bit_6 -X3_bit_5 -X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 -X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 -X4_bit_7 -X4_bit_6 -X4_bit_5 -X4_bit_4 -X4_bit_3 -X4_bit_2 -X4_bit_1 X4_bit0 -X4_bit1 X4_bit2 -X4_bit3 -X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 -X5_bit_7 -X5_bit_6 -X5_bit_5 -X5_bit_4 -X5_bit_3 -X5_bit_2 -X5_bit_1 -X5_bit0 -X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X6_bit_7 -X6_bit_6 -X6_bit_5 -X6_bit_4 -X6_bit_3 -X6_bit_2 -X6_bit_1 -X6_bit0 -X6_bit1 -X6_bit2 -X6_bit3 -X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X7_bit_7 -X7_bit_6 -X7_bit_5 -X7_bit_4 -X7_bit_3 -X7_bit_2 -X7_bit_1 -X7_bit0 X7_bit1 -X7_bit2 X7_bit3 -X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 -X8_bit_7 -X8_bit_6 -X8_bit_5 -X8_bit_4 -X8_bit_3 -X8_bit_2 -X8_bit_1 X8_bit0 -X8_bit1 -X8_bit2 X8_bit3 X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 -X9_bit_7 -X9_bit_6 -X9_bit_5 -X9_bit_4 -X9_bit_3 -X9_bit_2 -X9_bit_1 -X9_bit0 -X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 -X10_bit_7 -X10_bit_6 -X10_bit_5 -X10_bit_4 -X10_bit_3 -X10_bit_2 -X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 -X11_bit_7 -X11_bit_6 -X11_bit_5 -X11_bit_4 -X11_bit_3 -X11_bit_2 -X11_bit_1 -X11_bit0 -X11_bit1 -X11_bit2 -X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 -X12_bit_7 -X12_bit_6 -X12_bit_5 -X12_bit_4 -X12_bit_3 -X12_bit_2 -X12_bit_1 X12_bit0 X12_bit1 X12_bit2 X12_bit3 -X12_bit4 -X12_bit5 -X12_bit6 -X12_bit7 -X12_bit8 -X12_bit9 -X12_bit10 -X12_bit11 -X12_bit12 -X13_bit_7 -X13_bit_6 -X13_bit_5 -X13_bit_4 -X13_bit_3 -X13_bit_2 -X13_bit_1 -X13_bit0 -X13_bit1 -X13_bit2 -X13_bit3 -X13_bit4 -X13_bit5 -X13_bit6 -X13_bit7 -X13_bit8 -X13_bit9 -X13_bit10 -X13_bit11 -X13_bit12 -X14_bit_7 -X14_bit_6 -X14_bit_5 -X14_bit_4 -X14_bit_3 -X14_bit_2 -X14_bit_1 -X14_bit0 -X14_bit1 -X14_bit2 -X14_bit3 -X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 -X15_bit_7 -X15_bit_6 -X15_bit_5 -X15_bit_4 -X15_bit_3 -X15_bit_2 -X15_bit_1 -X15_bit0 -X15_bit1 -X15_bit2 -X15_bit3 -X15_bit4 -X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 -X16_bit_7 -X16_bit_6 -X16_bit_5 -X16_bit_4 -X16_bit_3 -X16_bit_2 -X16_bit_1 -X16_bit0 -X16_bit1 -X16_bit2 -X16_bit3 -X16_bit4 -X16_bit5 -X16_bit6 -X16_bit7 -X16_bit8 -X16_bit9 -X16_bit10 -X16_bit11 -X16_bit12 -X17_bit_7 -X17_bit_6 -X17_bit_5 -X17_bit_4 -X17_bit_3 -X17_bit_2 -X17_bit_1 X17_bit0 -X17_bit1 X17_bit2 -X17_bit3 -X17_bit4 -X17_bit5 -X17_bit6 -X17_bit7 -X17_bit8 -X17_bit9 -X17_bit10 -X17_bit11 -X17_bit12 -X18_bit_7 -X18_bit_6 -X18_bit_5 -X18_bit_4 -X18_bit_3 -X18_bit_2 -X18_bit_1 -X18_bit0 -X18_bit1 -X18_bit2 -X18_bit3 -X18_bit4 -X18_bit5 -X18_bit6 -X18_bit7 -X18_bit8 -X18_bit9 -X18_bit10 -X18_bit11 -X18_bit12 -X19_bit_7 -X19_bit_6 -X19_bit_5 -X19_bit_4 -X19_bit_3 -X19_bit_2 -X19_bit_1 -X19_bit0 -X19_bit1 -X19_bit2 -X19_bit3 -X19_bit4 -X19_bit5 -X19_bit6 -X19_bit7 -X19_bit8 -X19_bit9 -X19_bit10 -X19_bit11 -X19_bit12 -X20_bit_7 -X20_bit_6 -X20_bit_5 -X20_bit_4 -X20_bit_3 -X20_bit_2 -X20_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.91 0.95 0.95 2/56 27722
Raw data (stat): 27722 (runsolver) R 27721 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 429972608 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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+10.0004 s]
Raw data (loadavg): 0.93 0.95 0.95 2/56 27722
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 1485 0 0 0 994 4 0 0 25 0 1 0 429972608 7901184 1462 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1929 1462 603 41 0 1888 0
vsize: 7716
[startup+20.0011 s]
Raw data (loadavg): 0.94 0.96 0.95 2/56 27722
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 2467 0 0 0 1992 6 0 0 25 0 1 0 429972608 11923456 2444 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2911 2444 603 41 0 2870 0
vsize: 11644
[startup+30.001 s]
Raw data (loadavg): 0.95 0.96 0.95 2/56 27722
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 2771 0 0 0 2991 8 0 0 25 0 1 0 429972608 13119488 2748 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3203 2748 603 41 0 3162 0
vsize: 12812
[startup+40.0007 s]
Raw data (loadavg): 0.95 0.96 0.95 2/56 27722
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 2916 0 0 0 3991 8 0 0 25 0 1 0 429972608 13787136 2893 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3366 2893 603 41 0 3325 0
vsize: 13464
[startup+50.002 s]
Raw data (loadavg): 0.96 0.96 0.95 2/56 27722
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 2920 0 0 0 4991 8 0 0 25 0 1 0 429972608 13787136 2897 4294967295 134512640 134672761 3221224544 3221223680 134565149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3366 2897 603 41 0 3325 0
vsize: 13464
[startup+60.0023 s]
Raw data (loadavg): 0.97 0.96 0.95 2/56 27722
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 2920 0 0 0 5991 8 0 0 25 0 1 0 429972608 13787136 2897 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3366 2897 603 41 0 3325 0
vsize: 13464
[startup+70.0031 s]
Raw data (loadavg): 0.97 0.96 0.95 2/56 27722
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 2920 0 0 0 6991 8 0 0 25 0 1 0 429972608 13787136 2897 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3366 2897 603 41 0 3325 0
vsize: 13464
[startup+80.0029 s]
Raw data (loadavg): 0.98 0.96 0.95 2/56 27722
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 3396 0 0 0 7990 9 0 0 25 0 1 0 429972608 15671296 3373 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3826 3373 603 41 0 3785 0
vsize: 15304
[startup+90.0027 s]
Raw data (loadavg): 0.98 0.96 0.95 2/56 27722
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 3635 0 0 0 8989 10 0 0 25 0 1 0 429972608 16601088 3612 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4053 3612 603 41 0 4012 0
vsize: 16212
[startup+100.002 s]
Raw data (loadavg): 0.98 0.96 0.95 2/56 27722
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 3635 0 0 0 9989 10 0 0 25 0 1 0 429972608 16601088 3612 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4053 3612 603 41 0 4012 0
vsize: 16212
[startup+110.004 s]
Raw data (loadavg): 0.98 0.96 0.95 2/56 27722
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 4238 0 0 0 10988 12 0 0 25 0 1 0 429972608 19136512 4215 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4672 4215 603 41 0 4631 0
vsize: 18688
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27724
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 4238 0 0 0 11987 12 0 0 25 0 1 0 429972608 19136512 4215 4294967295 134512640 134672761 3221224544 3221223648 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4672 4215 603 41 0 4631 0
vsize: 18688
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27724
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 4239 0 0 0 12987 13 0 0 25 0 1 0 429972608 19136512 4216 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4672 4216 603 41 0 4631 0
vsize: 18688
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27724
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 4239 0 0 0 13987 13 0 0 25 0 1 0 429972608 19136512 4216 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4672 4216 603 41 0 4631 0
vsize: 18688
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27724
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 4239 0 0 0 14987 13 0 0 25 0 1 0 429972608 19136512 4216 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4672 4216 603 41 0 4631 0
vsize: 18688
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27724
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 4239 0 0 0 15987 13 0 0 25 0 1 0 429972608 19136512 4216 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4672 4216 603 41 0 4631 0
vsize: 18688
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27724
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 4275 0 0 0 16987 13 0 0 25 0 1 0 429972608 19271680 4252 4294967295 134512640 134672761 3221224544 3221223712 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4705 4252 603 41 0 4664 0
vsize: 18820
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27724
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 4283 0 0 0 17987 13 0 0 25 0 1 0 429972608 19271680 4260 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4705 4260 603 41 0 4664 0
vsize: 18820
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27724
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 4362 0 0 0 18987 14 0 0 25 0 1 0 429972608 19673088 4339 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4803 4339 603 41 0 4762 0
vsize: 19212
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27724
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 4389 0 0 0 19987 14 0 0 25 0 1 0 429972608 19673088 4366 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4803 4366 603 41 0 4762 0
vsize: 19212
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27724
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 4389 0 0 0 20987 14 0 0 25 0 1 0 429972608 19673088 4366 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4803 4366 603 41 0 4762 0
vsize: 19212
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27724
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 4391 0 0 0 21987 14 0 0 25 0 1 0 429972608 19673088 4368 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4803 4368 603 41 0 4762 0
vsize: 19212
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27724
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 4459 0 0 0 22987 14 0 0 25 0 1 0 429972608 19939328 4436 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4868 4436 603 41 0 4827 0
vsize: 19472
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27724
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 4459 0 0 0 23987 14 0 0 25 0 1 0 429972608 19939328 4436 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4868 4436 603 41 0 4827 0
vsize: 19472
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27724
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 4462 0 0 0 24987 14 0 0 25 0 1 0 429972608 20086784 4439 4294967295 134512640 134672761 3221224544 3221223648 134560361 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4904 4439 603 41 0 4863 0
vsize: 19616
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27724
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 4497 0 0 0 25988 14 0 0 25 0 1 0 429972608 20348928 4474 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4968 4474 603 41 0 4927 0
vsize: 19872
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27724
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 4497 0 0 0 26987 15 0 0 25 0 1 0 429972608 20348928 4474 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4968 4474 603 41 0 4927 0
vsize: 19872
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27724
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 4497 0 0 0 27987 15 0 0 25 0 1 0 429972608 20348928 4474 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4968 4474 603 41 0 4927 0
vsize: 19872
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27724
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 4497 0 0 0 28987 15 0 0 25 0 1 0 429972608 20348928 4474 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4968 4474 603 41 0 4927 0
vsize: 19872
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27724
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 4497 0 0 0 29987 15 0 0 25 0 1 0 429972608 20348928 4474 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4968 4474 603 41 0 4927 0
vsize: 19872
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27724
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 4497 0 0 0 30987 15 0 0 25 0 1 0 429972608 20348928 4474 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4968 4474 603 41 0 4927 0
vsize: 19872
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27724
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 4497 0 0 0 31988 15 0 0 25 0 1 0 429972608 20348928 4474 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4968 4474 603 41 0 4927 0
vsize: 19872
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27724
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 4497 0 0 0 32988 15 0 0 25 0 1 0 429972608 20348928 4474 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4968 4474 603 41 0 4927 0
vsize: 19872
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27724
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 4498 0 0 0 33988 15 0 0 25 0 1 0 429972608 20348928 4475 4294967295 134512640 134672761 3221224544 3221223680 134565110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4968 4475 603 41 0 4927 0
vsize: 19872
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27724
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 4499 0 0 0 34988 15 0 0 25 0 1 0 429972608 20348928 4476 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4968 4476 603 41 0 4927 0
vsize: 19872
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27724
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 4499 0 0 0 35988 15 0 0 25 0 1 0 429972608 20348928 4476 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4968 4476 603 41 0 4927 0
vsize: 19872
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27724
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 4580 0 0 0 36988 15 0 0 25 0 1 0 429972608 20611072 4557 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4557 603 41 0 4991 0
vsize: 20128
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27724
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 5095 0 0 0 37987 17 0 0 25 0 1 0 429972608 22728704 5072 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5549 5072 603 41 0 5508 0
vsize: 22196
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27724
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 5612 0 0 0 38986 18 0 0 25 0 1 0 429972608 24862720 5589 4294967295 134512640 134672761 3221224544 3221223728 134559581 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6070 5589 603 41 0 6029 0
vsize: 24280
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27724
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 6097 0 0 0 39983 21 0 0 25 0 1 0 429972608 26857472 6074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6557 6074 603 41 0 6516 0
vsize: 26228
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27724
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 6557 0 0 0 40983 21 0 0 25 0 1 0 429972608 28721152 6534 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7012 6534 603 41 0 6971 0
vsize: 28048
[startup+420.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27726
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 6979 0 0 0 41982 23 0 0 25 0 1 0 429972608 30441472 6956 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7432 6956 603 41 0 7391 0
vsize: 29728
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27726
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7392 0 0 0 42980 25 0 0 25 0 1 0 429972608 32169984 7369 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7854 7369 603 41 0 7813 0
vsize: 31416
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27726
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7817 0 0 0 43979 26 0 0 25 0 1 0 429972608 33894400 7794 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8275 7794 603 41 0 8234 0
vsize: 33100
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27726
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7875 0 0 0 44979 26 0 0 25 0 1 0 429972608 34156544 7852 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8339 7852 603 41 0 8298 0
vsize: 33356
[startup+460.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27726
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7875 0 0 0 45979 26 0 0 25 0 1 0 429972608 34156544 7852 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7852 603 41 0 8298 0
vsize: 33356
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27726
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7875 0 0 0 46979 26 0 0 25 0 1 0 429972608 34156544 7852 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7852 603 41 0 8298 0
vsize: 33356
[startup+480.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27726
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 47979 26 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27726
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 48979 27 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27726
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 49979 27 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27726
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 50979 27 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27726
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 51979 27 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27726
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 52979 27 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27726
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 53979 27 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+550.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27726
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 54979 27 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27726
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 55979 28 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+570.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27726
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 56979 28 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+580.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27726
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 57979 28 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+590.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27726
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 58979 28 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+600.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27726
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 59979 28 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+610.016 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27726
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 60979 28 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+620.016 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27726
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 61979 28 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+630.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27726
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 62980 28 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+640.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27726
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 63980 28 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+650.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27726
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 64980 28 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+660.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27726
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 65980 29 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+670.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27726
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 66980 29 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+680.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27726
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 67980 29 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+690.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27726
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 68981 29 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+700.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27726
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 69981 29 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+710.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27726
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 70981 29 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+720.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27728
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 71981 29 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+730.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27728
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 72981 29 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+740.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27728
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 73981 29 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+750.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27728
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 74981 29 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+760.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27728
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 75982 29 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+770.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27728
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 76982 29 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+780.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27728
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 77982 29 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+790.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27728
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 78982 29 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+800.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27728
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 79982 29 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+810.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27728
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 80982 29 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+820.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27728
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 81982 29 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+830.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27728
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 82982 29 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+840.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27728
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 83982 29 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+850.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27728
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7876 0 0 0 84983 29 0 0 25 0 1 0 429972608 34156544 7853 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7853 603 41 0 8298 0
vsize: 33356
[startup+860.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27728
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7877 0 0 0 85983 29 0 0 25 0 1 0 429972608 34156544 7854 4294967295 134512640 134672761 3221224544 3221223728 134559295 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7854 603 41 0 8298 0
vsize: 33356
[startup+870.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27728
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7877 0 0 0 86982 30 0 0 25 0 1 0 429972608 34156544 7854 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7854 603 41 0 8298 0
vsize: 33356
[startup+880.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27728
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7877 0 0 0 87983 30 0 0 25 0 1 0 429972608 34156544 7854 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7854 603 41 0 8298 0
vsize: 33356
[startup+890.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27728
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7877 0 0 0 88983 30 0 0 25 0 1 0 429972608 34156544 7854 4294967295 134512640 134672761 3221224544 3221223704 134542657 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7854 603 41 0 8298 0
vsize: 33356
[startup+900.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27728
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7877 0 0 0 89983 30 0 0 25 0 1 0 429972608 34156544 7854 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7854 603 41 0 8298 0
vsize: 33356
[startup+910.029 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27728
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7877 0 0 0 90983 30 0 0 25 0 1 0 429972608 34156544 7854 4294967295 134512640 134672761 3221224544 3221223648 134560477 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7854 603 41 0 8298 0
vsize: 33356
[startup+920.029 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27728
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7877 0 0 0 91983 30 0 0 25 0 1 0 429972608 34156544 7854 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7854 603 41 0 8298 0
vsize: 33356
[startup+930.029 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27728
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7877 0 0 0 92983 30 0 0 25 0 1 0 429972608 34156544 7854 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7854 603 41 0 8298 0
vsize: 33356
[startup+940.029 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27728
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7877 0 0 0 93983 30 0 0 25 0 1 0 429972608 34156544 7854 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7854 603 41 0 8298 0
vsize: 33356
[startup+950.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27728
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7877 0 0 0 94984 30 0 0 25 0 1 0 429972608 34156544 7854 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7854 603 41 0 8298 0
vsize: 33356
[startup+960.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27728
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7877 0 0 0 95984 30 0 0 25 0 1 0 429972608 34156544 7854 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7854 603 41 0 8298 0
vsize: 33356
[startup+970.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27728
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7877 0 0 0 96984 30 0 0 25 0 1 0 429972608 34156544 7854 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7854 603 41 0 8298 0
vsize: 33356
[startup+980.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27728
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7877 0 0 0 97984 30 0 0 25 0 1 0 429972608 34156544 7854 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7854 603 41 0 8298 0
vsize: 33356
[startup+990.031 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27728
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7877 0 0 0 98984 30 0 0 25 0 1 0 429972608 34156544 7854 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7854 603 41 0 8298 0
vsize: 33356
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27728
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7877 0 0 0 99984 30 0 0 25 0 1 0 429972608 34156544 7854 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7854 603 41 0 8298 0
vsize: 33356
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27728
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7879 0 0 0 100984 31 0 0 25 0 1 0 429972608 34156544 7856 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7856 603 41 0 8298 0
vsize: 33356
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27730
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7879 0 0 0 101983 31 0 0 25 0 1 0 429972608 34156544 7856 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7856 603 41 0 8298 0
vsize: 33356
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27730
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7879 0 0 0 102983 31 0 0 25 0 1 0 429972608 34156544 7856 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7856 603 41 0 8298 0
vsize: 33356
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27730
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7879 0 0 0 103983 31 0 0 25 0 1 0 429972608 34156544 7856 4294967295 134512640 134672761 3221224544 3221223712 134561121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7856 603 41 0 8298 0
vsize: 33356
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27730
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7879 0 0 0 104983 31 0 0 25 0 1 0 429972608 34156544 7856 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7856 603 41 0 8298 0
vsize: 33356
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27730
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7879 0 0 0 105983 31 0 0 25 0 1 0 429972608 34156544 7856 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7856 603 41 0 8298 0
vsize: 33356
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27730
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7879 0 0 0 106984 31 0 0 25 0 1 0 429972608 34156544 7856 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7856 603 41 0 8298 0
vsize: 33356
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27730
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7879 0 0 0 107983 32 0 0 25 0 1 0 429972608 34156544 7856 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7856 603 41 0 8298 0
vsize: 33356
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27730
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7879 0 0 0 108984 32 0 0 25 0 1 0 429972608 34156544 7856 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7856 603 41 0 8298 0
vsize: 33356
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27730
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7879 0 0 0 109984 32 0 0 25 0 1 0 429972608 34156544 7856 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7856 603 41 0 8298 0
vsize: 33356
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27730
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7879 0 0 0 110984 32 0 0 25 0 1 0 429972608 34156544 7856 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7856 603 41 0 8298 0
vsize: 33356
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27730
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7879 0 0 0 111984 32 0 0 25 0 1 0 429972608 34156544 7856 4294967295 134512640 134672761 3221224544 3221223712 134561275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7856 603 41 0 8298 0
vsize: 33356
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27730
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7879 0 0 0 112984 32 0 0 25 0 1 0 429972608 34156544 7856 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7856 603 41 0 8298 0
vsize: 33356
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27730
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7879 0 0 0 113983 33 0 0 25 0 1 0 429972608 34156544 7856 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8339 7856 603 41 0 8298 0
vsize: 33356
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27730
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7879 0 0 0 114984 33 0 0 25 0 1 0 429972608 34156544 7856 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8339 7856 603 41 0 8298 0
vsize: 33356
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27730
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7879 0 0 0 115984 33 0 0 25 0 1 0 429972608 34156544 7856 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8339 7856 603 41 0 8298 0
vsize: 33356
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27730
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7879 0 0 0 116984 33 0 0 25 0 1 0 429972608 34156544 7856 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8339 7856 603 41 0 8298 0
vsize: 33356
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27730
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7879 0 0 0 117984 33 0 0 25 0 1 0 429972608 34156544 7856 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8339 7856 603 41 0 8298 0
vsize: 33356
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27730
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7879 0 0 0 118984 33 0 0 25 0 1 0 429972608 34156544 7856 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8339 7856 603 41 0 8298 0
vsize: 33356
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 27730
Raw data (stat): 27722 (minisat+) R 27721 12452 12451 0 -1 0 7879 0 0 0 119984 33 0 0 25 0 1 0 429972608 34156544 7856 4294967295 134512640 134672761 3221224544 3221222464 134565848 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8339 7856 603 41 0 8298 0
vsize: 33356
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.95 1/56 27730
Raw data (stat): 27722 (minisat+) Z 27721 12452 12451 0 -1 12 7882 0 0 0 119985 34 0 0 25 0 1 0 429972608 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.06
CPU time (s): 1200.2
CPU user time (s): 1199.85
CPU system time (s): 0.347947
CPU usage (%): 100.012
Max. virtual memory (Kb): 33356
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####