PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-cracpb1.opb
MD5SUM	098fe473d82d5f7d4121673eb775be76
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	22199
Optimality of the best value was proved	NO
Number of terms in the objective function	572
Biggest coefficient in the objective function	5000
Number of bits for the biggest coefficient in the objective function	13
Sum of the numbers in the objective function	547769
Number of bits of the sum of numbers in the objective function	20
Biggest number in a constraint	5000
Number of bits of the biggest number in a constraint	13
Biggest sum of numbers in a constraint	547769
Number of bits of the biggest sum of numbers	20
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	30.8603
Number of variables	572
Total number of constraints	716
Number of constraints which are clauses	3
Number of constraints which are cardinality constraints (but not clauses)	644
Number of constraints which are nor clauses,nor cardinality constraints	69
Minimum length of a constraint	1
Maximum length of a constraint	518
Trace number 19275

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc28 THE 2005-04-21 18:36:25 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16755 boxname=wulflinc28 idbench=1289 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  098fe473d82d5f7d4121673eb775be76  /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-cracpb1.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-cracpb1.opb /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-cracpb1.opb
IDLAUNCH: 16755
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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.077
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:        503640 kB
Buffers:         33896 kB
Cached:         470220 kB
SwapCached:        104 kB
Active:         206392 kB
Inactive:       300152 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        503388 kB
SwapTotal:     2097640 kB
SwapFree:      2097068 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6056 kB
Slab:            18872 kB
Committed_AS:    63584 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 18:56:27 (client local time) WITH STATUS 10 IN 1200.28 SECONDS
stats: 16755 7 1200.28 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 215 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #########################################################################################
c   -- Clauses(.)/Splits(s): ...
c ---[ 214]---> Adder-cost: 1416   maxlim: 2733   bits: 12/12
c ---[ 213]---> Sorter-cost:  634     Base:
c ---[ 212]---> Sorter-cost:  238     Base:
c ---[ 211]---> Sorter-cost:  238     Base:
c ---[ 210]---> Sorter-cost:  206     Base:
c ---[ 209]---> Sorter-cost:  356     Base:
c ---[ 208]---> Sorter-cost:  356     Base:
c ---[ 207]---> Sorter-cost:  264     Base:
c ---[ 206]---> Sorter-cost:  126     Base:
c ---[ 205]---> Sorter-cost:  356     Base:
c ---[ 204]---> Sorter-cost:  106     Base:
c ---[ 203]---> BDD-cost:   43
c ---[ 202]---> BDD-cost:   34
c ---[ 201]---> Sorter-cost:  170     Base:
c ---[ 200]---> BDD-cost:   29
c ---[ 199]---> Sorter-cost:  180     Base:
c ---[ 198]---> BDD-cost:   31
c ---[ 197]---> BDD-cost:   21
c ---[ 195]---> Sorter-cost:  561     Base:
c ---[ 193]---> BDD-cost:   41
c ---[ 191]---> Sorter-cost:  255     Base:
c ---[ 189]---> Sorter-cost:  207     Base:
c ---[ 187]---> Sorter-cost:  491     Base:
c ---[ 185]---> Sorter-cost:  239     Base:
c ---[ 183]---> Sorter-cost:  281     Base:
c ---[ 181]---> Sorter-cost:  181     Base:
c ---[ 179]---> Sorter-cost:  291     Base:
c ---[ 177]---> Sorter-cost:  127     Base:
c ---[ 175]---> BDD-cost:   33
c ---[ 173]---> Sorter-cost:  207     Base:
c ---[ 171]---> Sorter-cost:  117     Base:
c ---[ 169]---> Sorter-cost:   77     Base:
c ---[ 167]---> Sorter-cost:  171     Base:
c ---[ 165]---> Sorter-cost:  127     Base:
c ---[ 163]---> BDD-cost:   29
c ---[ 161]---> BDD-cost:   25
c ---[ 159]---> Adder-cost: 155   maxlim: 27   bits: 6/5
c ---[ 157]---> Sorter-cost:  631     Base:
c ---[ 155]---> Sorter-cost:  689     Base:
c ---[ 153]---> Sorter-cost:  609     Base:
c ---[ 151]---> Sorter-cost:  971     Base:
c ---[ 149]---> Sorter-cost:  991     Base:
c ---[ 147]---> Sorter-cost:  755     Base:
c ---[ 145]---> Sorter-cost:  371     Base:
c ---[ 143]---> Sorter-cost:  927     Base:
c ---[ 141]---> Sorter-cost:  355     Base:
c ---[ 139]---> Sorter-cost:  313     Base:
c ---[ 137]---> Sorter-cost:  279     Base:
c ---[ 135]---> Sorter-cost:  501     Base:
c ---[ 133]---> Sorter-cost:  225     Base:
c ---[ 131]---> Sorter-cost:  517     Base:
c ---[ 129]---> Sorter-cost:  197     Base:
c ---[ 127]---> BDD-cost:   66
c ---[ 126]---> Adder-cost: 732   maxlim: 1601   bits: 12/11
c ---[ 125]---> Adder-cost: 1184   maxlim: 406   bits: 10/9
c ---[ 124]---> Adder-cost: 255   maxlim: 863   bits: 11/10
c ---[ 123]---> BDD-cost:   27
c ---[ 122]---> BDD-cost:   35
c ---[ 121]---> Sorter-cost:  172     Base:
c ---[ 120]---> BDD-cost:   31
c ---[ 118]---> BDD-cost:   51
c ---[ 115]---> BDD-cost:   80
c ---[ 114]---> Sorter-cost:  238     Base:
c ---[ 113]---> Sorter-cost:  478     Base:
c ---[ 112]---> Sorter-cost:  254     Base:
c ---[ 111]---> BDD-cost:   21
c ---[ 110]---> Sorter-cost:  474     Base:
c ---[ 109]---> BDD-cost:   29
c ---[ 108]---> BDD-cost:   23
c ---[ 106]---> BDD-cost:   16
c ---[ 104]---> BDD-cost:   17
c ---[ 102]---> BDD-cost:    5
c ---[ 100]---> BDD-cost:   43
c ---[  98]---> BDD-cost:   92
c ---[  96]---> BDD-cost:  183
c ---[  94]---> BDD-cost:   11
c ---[  92]---> BDD-cost:   29
c ---[  90]---> BDD-cost:   29
c ---[  88]---> BDD-cost:   19
c ---[  86]---> BDD-cost:   11
c ---[  84]---> BDD-cost:   11
c ---[  82]---> BDD-cost:   31
c ---[  80]---> BDD-cost:   23
c ---[  78]---> BDD-cost:    7
c ---[  76]---> BDD-cost:   13
c ---[  74]---> BDD-cost:   14
c ---[  72]---> BDD-cost:   38
c ---[  70]---> BDD-cost:   23
c ---[  68]---> BDD-cost:   35
c ---[  66]---> BDD-cost:   37
c ---[  64]---> BDD-cost:    7
c ---[  62]---> BDD-cost:   17
c ---[  60]---> BDD-cost:   17
c ---[  58]---> BDD-cost:   43
c ---[  56]---> BDD-cost:   11
c ---[  54]---> BDD-cost:   29
c ---[  52]---> BDD-cost:    7
c ---[  50]---> BDD-cost:   16
c ---[  48]---> BDD-cost:   24
c ---[  46]---> BDD-cost:    5
c ---[  44]---> BDD-cost:   14
c ---[  42]---> BDD-cost:   11
c ---[  40]---> BDD-cost:   13
c ---[  38]---> BDD-cost:   16
c ---[  36]---> BDD-cost:   19
c ---[  34]---> BDD-cost:   14
c ---[  32]---> BDD-cost:   19
c ---[  30]---> BDD-cost:   11
c ---[  28]---> BDD-cost:    4
c ---[  26]---> BDD-cost:   11
c ---[  24]---> BDD-cost:   14
c ---[  22]---> BDD-cost:   15
c ---[  20]---> BDD-cost:   48
c ---[  18]---> BDD-cost:   51
c ---[  16]---> BDD-cost:   11
c ---[  14]---> BDD-cost:    6
c ---[  12]---> BDD-cost:   51
c ---[  10]---> BDD-cost:    8
c ---[   8]---> BDD-cost:   14
c ---[   6]---> BDD-cost:   43
c ---[   4]---> BDD-cost:   31
c ---[   2]---> BDD-cost:   22
c ---[   0]---> BDD-cost:   17
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   59709   173659 |   17912       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/16904          
c   -- var.elim.:  2000/16904          
c   -- var.elim.:  3000/16904          
c   -- var.elim.:  4000/16904          
c   -- var.elim.:  5000/16904          
c   -- var.elim.:  6000/16904          
c   -- var.elim.:  7000/16904          
c   -- var.elim.:  8000/16904          
c   -- var.elim.:  9000/16904          
c   -- var.elim.:  10000/16904          
c   -- var.elim.:  11000/16904          
c   -- var.elim.:  12000/16904          
c   -- var.elim.:  13000/16904          
c   -- var.elim.:  14000/16904          
c   -- var.elim.:  15000/16904          
c   -- var.elim.:  16000/16904          
c   -- var.elim.:  16904/16904          
c   -- var.elim.:  1000/6550          
c   -- var.elim.:  2000/6550          
c   -- var.elim.:  3000/6550          
c   -- var.elim.:  4000/6550          
c   -- var.elim.:  5000/6550          
c   -- var.elim.:  6000/6550          
c   -- var.elim.:  6550/6550          
c   -- var.elim.:  125/125          
c   -- var.elim.:  4/4          
c   -- subsuming                       
c   -- var.elim.:  1000/1916          
c   -- var.elim.:  1916/1916          
c   -- var.elim.:  719/719          
c   -- var.elim.:  4/4          
c   -- subsuming                       
c   -- var.elim.:  305/305          
c   -- var.elim.:  55/55          
c |         0 |   54383   181287 |      --       0       --      -- |     --   | -4874/9160
c |         0 |   54383   181287 |   21753       0        0     nan |  0.000 % |
c |       100 |   54288   180931 |   23886      90     1298    14.4 |  3.854 % |
c |       251 |   53990   179829 |   26131     206     2782    13.5 |  4.204 % |
c |       476 |   53594   178461 |   28533     409     5544    13.6 |  4.684 % |
c |       813 |   53125   176902 |   31112     702     9879    14.1 |  5.283 % |
c |      1321 |   52658   175282 |   33922    1134    15704    13.8 |  5.926 % |
c |      2080 |   52303   173978 |   37063    1858    43808    23.6 |  6.388 % |
c |      3219 |   51506   171029 |   40148    2931    89812    30.6 |  7.399 % |
c |      4927 |   51200   169953 |   43900    4597   179062    39.0 |  7.827 % |
c |      7489 |   51050   169381 |   48149    7134   384901    54.0 |  7.972 % |
c |     11336 |   50050   165911 |   51926   10794  1051563    97.4 |  9.291 % |
c |     17105 |   49655   164471 |   56668   16480  1314754    79.8 |  9.779 % |
c |     25754 |   49248   163033 |   61824   25052  1826237    72.9 | 10.421 % |
c |     38729 |   48959   162000 |   67607   37983  3084200    81.2 | 10.747 % |
c |     58190 |   48779   161345 |   74095   57396  5045678    87.9 | 10.944 % |
c ==============================================================================
c (current CPU-time: 121.816 s)
c ==============================================================================
c [1mFound solution: 72444[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 4526   maxlim: 473907   bits: 20/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     74708 |   80267   273823 |   24080   73875  7550948   102.2 | 10.944 % |
c   -- subsuming                       
c   -- var.elim.:  1000/8089          
c   -- var.elim.:  2000/8089          
c   -- var.elim.:  3000/8089          
c   -- var.elim.:  4000/8089          
c   -- var.elim.:  5000/8089          
c   -- var.elim.:  6000/8089          
c   -- var.elim.:  7000/8089          
c   -- var.elim.:  8000/8089          
c   -- var.elim.:  8089/8089          
c   -- var.elim.:  1000/1558          
c   -- var.elim.:  1558/1558          
c   -- var.elim.:  150/150          
c   -- var.elim.:  53/53          
c   -- subsuming                       
c   -- var.elim.:  272/272          
c   -- var.elim.:  107/107          
c |     74708 |   79471   272142 |      --   73875       --      -- |     --   | -796/-1670
c |     74708 |   79471   272142 |   31788   47937  2127459    44.4 | 10.944 % |
c |     74808 |   79471   272142 |   34967   11198   402337    35.9 |  8.272 % |
c |     74958 |   79444   272045 |   38450   11344   404507    35.7 |  8.297 % |
c |     75184 |   79369   271753 |   42256   11568   407685    35.2 |  8.367 % |
c |     75521 |   79369   271753 |   46481   11905   418715    35.2 |  8.367 % |
c |     76027 |   79342   271656 |   51112   12409   430255    34.7 |  8.392 % |
c |     76786 |   79342   271656 |   56223   13168   508408    38.6 |  8.392 % |
c |     77928 |   79342   271656 |   61846   14310   553464    38.7 |  8.392 % |
c |     79636 |   79319   271585 |   68010   16016   664391    41.5 |  8.417 % |
c |     82202 |   79275   271428 |   74770   18580   785430    42.3 |  8.455 % |
c |     86047 |   79202   271161 |   82171   22417  1240005    55.3 |  8.531 % |
c |     91815 |   79193   271132 |   90378   28181  1644166    58.3 |  8.544 % |
c |    100466 |   79156   270994 |   99370   36828  3246189    88.1 |  8.582 % |
c |    113441 |   79024   270537 |  109124   49786  4454406    89.5 |  8.702 % |
c |    132902 |   78943   270227 |  119914   69219  6710962    97.0 |  8.759 % |
c |    162094 |   78613   269054 |  131354   98373 10097246   102.6 |  9.006 % |
c |    205884 |   78515   268687 |  144309   21889  3260483   149.0 |  9.075 % |
c |    271568 |   78280   267797 |  158265   87548 12948753   147.9 |  9.234 % |
c |    370094 |   78086   267055 |  173660   35720  9699510   271.5 |  9.417 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -GPT00001_bit0 -GPT00002_bit0 GPT00003_bit0 -GPT00004_bit0 -GPT00005_bit0 -GPT00006_bit0 -GPT00007_bit0 -GPT00008_bit0 -GPT00009_bit0 -GPT00010_bit0 -GPT00011_bit0 -GPT00012_bit0 -GPT00013_bit0 -GPT00014_bit0 -GPT00015_bit0 -GPT00016_bit0 GPT00017_bit0 -GPT00018_bit0 GPT00019_bit0 -GPT00020_bit0 -GPT00021_bit0 -GPT00022_bit0 GPT00023_bit0 -GPT00024_bit0 -GPT00025_bit0 -GPT00026_bit0 -GPT00027_bit0 GPT00028_bit0 -GPT00029_bit0 -GPT00030_bit0 -GPT00031_bit0 -GPT00032_bit0 -GPT00033_bit0 GPT00034_bit0 -GPT00035_bit0 -GPT00036_bit0 -GPT00037_bit0 GPT00038_bit0 -GPT00039_bit0 -GPT00040_bit0 -GPT00041_bit0 -GPT00042_bit0 -GPT00043_bit0 -GPT00044_bit0 -GPT00045_bit0 -GPT00046_bit0 -GPT00047_bit0 -GPT00048_bit0 GPT00049_bit0 -GPT00050_bit0 -GPT00051_bit0 -GPT00052_bit0 -GPT00053_bit0 -GPT00054_bit0 -GPT00055_bit0 -GPT00056_bit0 -GPT00057_bit0 -GPT00058_bit0 GPT00059_bit0 -GPT00060_bit0 -GPT00061_bit0 -GPT00062_bit0 -GPT00063_bit0 -GPT00064_bit0 -GPT00065_bit0 -GPT00066_bit0 -GPT00067_bit0 -GPT00068_bit0 GPT00069_bit0 -GPT00070_bit0 -GPT00071_bit0 -GPT00072_bit0 -GPT00073_bit0 GPT00074_bit0 -GPT00075_bit0 -GPT00076_bit0 -GPT00077_bit0 -GPT00078_bit0 -GPT00079_bit0 -GPT00080_bit0 -GPT00081_bit0 -GPT00082_bit0 -GPT00083_bit0 GPT00084_bit0 -GPT00085_bit0 -GPT00086_bit0 -GPT00087_bit0 -GPT00088_bit0 -GPT00089_bit0 -GPT00090_bit0 -GPT00091_bit0 -GPT00092_bit0 -GPT00093_bit0 -GPT00094_bit0 -GPT00095_bit0 -GPT00096_bit0 -GPT00097_bit0 -GPT00098_bit0 -GPT00099_bit0 -GPT00100_bit0 -GPT00101_bit0 -GPT00102_bit0 -GPT00103_bit0 -GPT00104_bit0 -GPT00105_bit0 -GPT00106_bit0 -GPT00107_bit0 -GPT00108_bit0 -GPT00109_bit0 -GPT00110_bit0 -GPT00111_bit0 GPT00112_bit0 -GPT00113_bit0 -GPT00114_bit0 -GPT00115_bit0 -GPT00116_bit0 GPT00117_bit0 -GPT00118_bit0 -GPT00119_bit0 -GPT00120_bit0 -GPT00121_bit0 -GPT00122_bit0 -GPT00123_bit0 -GPT00124_bit0 -GPT00125_bit0 -GPT00126_bit0 -GPT00127_bit0 -GPT00128_bit0 -GPT00129_bit0 -GPT00130_bit0 -GPT00131_bit0 -GPT00132_bit0 -GPT00133_bit0 -GPT00134_bit0 -GPT00135_bit0 -GPT00136_bit0 -GPT00137_bit0 GPT00138_bit0 -GPT00139_bit0 -GPT00140_bit0 -GPT00141_bit0 -GPT00142_bit0 -GPT00143_bit0 -GPT00144_bit0 -GPT00145_bit0 -GPT00146_bit0 -GPT00147_bit0 -GPT00148_bit0 -GPT00149_bit0 -GPT00150_bit0 GPT00151_bit0 -GPT00152_bit0 -GPT00153_bit0 -GPT00154_bit0 -GPT00155_bit0 -GPT00156_bit0 -GPT00157_bit0 -GPT00158_bit0 -GPT00159_bit0 -GPT00160_bit0 -GPT00161_bit0 GPT00162_bit0 -GPT00163_bit0 -GPT00164_bit0 -GPT00165_bit0 -GPT00166_bit0 -GPT00167_bit0 -GPT00168_bit0 -GPT00169_bit0 -GPT00170_bit0 -GPT00171_bit0 -GPT00172_bit0 -GPT00173_bit0 -GPT00174_bit0 -GPT00175_bit0 -GPT00176_bit0 -GPT00177_bit0 -GPT00178_bit0 -GPT00179_bit0 -GPT00180_bit0 -GPT00181_bit0 -GPT00182_bit0 -GPT00183_bit0 -GPT00184_bit0 -GPT00185_bit0 -GPT00186_bit0 -GPT00187_bit0 -GPT00188_bit0 -GPT00189_bit0 -GPT00190_bit0 GPT00191_bit0 -GPT00192_bit0 -GPT00193_bit0 -GPT00194_bit0 -GPT00195_bit0 -GPT00196_bit0 -GPT00197_bit0 -GPT00198_bit0 -GPT00199_bit0 -GPT00200_bit0 -GPT00201_bit0 -GPT00202_bit0 GPT00203_bit0 -GPT00204_bit0 -GPT00205_bit0 -GPT00206_bit0 -GPT00207_bit0 -GPT00208_bit0 -GPT00209_bit0 -GPT00210_bit0 -GPT00211_bit0 -GPT00212_bit0 -GPT00213_bit0 -GPT00214_bit0 GPT00215_bit0 -GPT00216_bit0 -GPT00217_bit0 -GPT00218_bit0 -GPT00219_bit0 -GPT00220_bit0 -GPT00221_bit0 -GPT00222_bit0 -GPT00223_bit0 -GPT00224_bit0 -GPT00225_bit0 GPT00226_bit0 -GPT00227_bit0 -GPT00228_bit0 -GPT00229_bit0 -GPT00230_bit0 -GPT00231_bit0 -GPT00232_bit0 -GPT00233_bit0 GPT00234_bit0 -GPT00235_bit0 -GPT00236_bit0 -GPT00237_bit0 -GPT00238_bit0 -GPT00239_bit0 -GPT00240_bit0 -GPT00241_bit0 -GPT00242_bit0 -GPT00243_bit0 -GPT00244_bit0 -GPT00245_bit0 -GPT00246_bit0 -GPT00247_bit0 GPT00248_bit0 -GPT00249_bit0 -GPT00250_bit0 -GPT00251_bit0 -GPT00252_bit0 GPT00253_bit0 -GPT00254_bit0 -GPT00255_bit0 -GPT00256_bit0 -GPT00257_bit0 -GPT00258_bit0 -GPT00259_bit0 -GPT00260_bit0 -GPT00261_bit0 -GPT00262_bit0 -GPT00263_bit0 -GPT00264_bit0 -GPT00265_bit0 GPT00266_bit0 -GPT00267_bit0 -GPT00268_bit0 -GPT00269_bit0 -GPT00270_bit0 -GPT00271_bit0 -GPT00272_bit0 -GPT00273_bit0 -GPT00274_bit0 GPT00275_bit0 -GPT00276_bit0 -GPT00277_bit0 GPT00278_bit0 -GPT00279_bit0 -GPT00280_bit0 GPT00281_bit0 -GPT00282_bit0 -GPT00283_bit0 -GPT00284_bit0 -GPT00285_bit0 -GPT00286_bit0 -GPT00287_bit0 GPT00288_bit0 -GPT00289_bit0 -GPT00290_bit0 -GPT00291_bit0 -GPT00292_bit0 -GPT00293_bit0 -GPT00294_bit0 -GPT00295_bit0 GPT00296_bit0 -GPT00297_bit0 -GPT00298_bit0 -GPT00299_bit0 -GPT00300_bit0 -GPT00301_bit0 -GPT00302_bit0 -GPT00303_bit0 -GPT00304_bit0 -GPT00305_bit0 -GPT00306_bit0 -GPT00307_bit0 -GPT00308_bit0 -GPT00309_bit0 -GPT00310_bit0 -GPT00311_bit0 -GPT00312_bit0 -GPT00313_bit0 GPT00314_bit0 -GPT00315_bit0 -GPT00316_bit0 -GPT00317_bit0 -GPT00318_bit0 -GPT00319_bit0 -GPT00320_bit0 -GPT00321_bit0 -GPT00322_bit0 GPT00323_bit0 -GPT00324_bit0 -GPT00325_bit0 GPT00326_bit0 -GPT00327_bit0 -GPT00328_bit0 -GPT00329_bit0 -GPT00330_bit0 -GPT00331_bit0 -GPT00332_bit0 -GPT00333_bit0 -GPT00334_bit0 -GPT00335_bit0 -GPT00336_bit0 GPT00337_bit0 -GPT00338_bit0 -GPT00339_bit0 -GPT00340_bit0 -GPT00341_bit0 -GPT00342_bit0 -GPT00343_bit0 -GPT00344_bit0 GPT00345_bit0 -GPT00346_bit0 -GPT00347_bit0 -GPT00348_bit0 -GPT00349_bit0 -GPT00350_bit0 -GPT00351_bit0 -GPT00352_bit0 -GPT00353_bit0 -GPT00354_bit0 -GPT00355_bit0 -GPT00356_bit0 -GPT00357_bit0 -GPT00358_bit0 -GPT00359_bit0 #### 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.85 0.97 0.95 2/54 29663
Raw data (stat): 29663 (runsolver) R 29662 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547294045 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0013 s]
Raw data (loadavg): 0.87 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 4036 0 0 0 986 11 0 0 25 0 1 0 547294045 18034688 3628 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4403 3628 603 41 0 4362 0
vsize: 17612
[startup+20.0016 s]
Raw data (loadavg): 0.89 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 4965 0 0 0 1985 13 0 0 25 0 1 0 547294045 21913600 4557 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5350 4557 603 41 0 5309 0
vsize: 21400
[startup+30.0016 s]
Raw data (loadavg): 0.91 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 5482 0 0 0 2983 15 0 0 25 0 1 0 547294045 24039424 5074 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5869 5074 603 41 0 5828 0
vsize: 23476
[startup+40.002 s]
Raw data (loadavg): 0.92 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 6439 0 0 0 3980 18 0 0 25 0 1 0 547294045 27881472 6031 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6807 6031 603 41 0 6766 0
vsize: 27228
[startup+50.0016 s]
Raw data (loadavg): 0.93 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 7039 0 0 0 4979 19 0 0 25 0 1 0 547294045 30535680 6631 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7455 6631 603 41 0 7414 0
vsize: 29820
[startup+60.0026 s]
Raw data (loadavg): 0.94 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 7721 0 0 0 5977 21 0 0 25 0 1 0 547294045 33320960 7313 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8135 7313 603 41 0 8094 0
vsize: 32540
[startup+70.003 s]
Raw data (loadavg): 0.95 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 8289 0 0 0 6976 23 0 0 25 0 1 0 547294045 35586048 7881 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8688 7881 603 41 0 8647 0
vsize: 34752
[startup+80.0027 s]
Raw data (loadavg): 0.96 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 9043 0 0 0 7974 25 0 0 25 0 1 0 547294045 38641664 8635 4294967295 134512640 134672761 3221224544 3221223728 134615686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9434 8635 603 41 0 9393 0
vsize: 37736
[startup+90.0026 s]
Raw data (loadavg): 0.96 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 9575 0 0 0 8973 26 0 0 25 0 1 0 547294045 40771584 9167 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9954 9167 603 41 0 9913 0
vsize: 39816
[startup+100.002 s]
Raw data (loadavg): 0.97 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 10220 0 0 0 9972 28 0 0 25 0 1 0 547294045 43397120 9812 4294967295 134512640 134672761 3221224544 3221223728 134615673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10595 9812 603 41 0 10554 0
vsize: 42380
[startup+110.003 s]
Raw data (loadavg): 0.97 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 10960 0 0 0 10971 29 0 0 25 0 1 0 547294045 46706688 10552 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11403 10552 603 41 0 11362 0
vsize: 45612
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 11778 0 0 0 11969 31 0 0 25 0 1 0 547294045 49999872 11370 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12207 11370 603 41 0 12166 0
vsize: 48828
[startup+130.003 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 15611 0 0 0 12958 41 0 0 25 0 1 0 547294045 61759488 14031 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15078 14031 603 41 0 15037 0
vsize: 60312
[startup+140.003 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 15611 0 0 0 13958 41 0 0 25 0 1 0 547294045 61759488 14031 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15078 14031 603 41 0 15037 0
vsize: 60312
[startup+150.003 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 15611 0 0 0 14958 41 0 0 25 0 1 0 547294045 61759488 14031 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15078 14031 603 41 0 15037 0
vsize: 60312
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 15611 0 0 0 15958 41 0 0 25 0 1 0 547294045 61759488 14031 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15078 14031 603 41 0 15037 0
vsize: 60312
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 15611 0 0 0 16959 41 0 0 25 0 1 0 547294045 61759488 14031 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15078 14031 603 41 0 15037 0
vsize: 60312
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 15611 0 0 0 17959 41 0 0 25 0 1 0 547294045 61759488 14031 4294967295 134512640 134672761 3221224544 3221223796 134617908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15078 14031 603 41 0 15037 0
vsize: 60312
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 15611 0 0 0 18959 41 0 0 25 0 1 0 547294045 61759488 14031 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15078 14031 603 41 0 15037 0
vsize: 60312
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 15611 0 0 0 19959 41 0 0 25 0 1 0 547294045 61759488 14031 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15078 14031 603 41 0 15037 0
vsize: 60312
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 15612 0 0 0 20959 41 0 0 25 0 1 0 547294045 61759488 14032 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15078 14032 603 41 0 15037 0
vsize: 60312
[startup+220.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 15612 0 0 0 21959 41 0 0 25 0 1 0 547294045 61759488 14032 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15078 14032 603 41 0 15037 0
vsize: 60312
[startup+230.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 15612 0 0 0 22960 41 0 0 25 0 1 0 547294045 61759488 14032 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15078 14032 603 41 0 15037 0
vsize: 60312
[startup+240.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 15612 0 0 0 23960 41 0 0 25 0 1 0 547294045 61759488 14032 4294967295 134512640 134672761 3221224544 3221223728 134615638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15078 14032 603 41 0 15037 0
vsize: 60312
[startup+250.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 15612 0 0 0 24960 41 0 0 25 0 1 0 547294045 61759488 14032 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15078 14032 603 41 0 15037 0
vsize: 60312
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 15612 0 0 0 25960 41 0 0 25 0 1 0 547294045 61759488 14032 4294967295 134512640 134672761 3221224544 3221223688 134616314 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15078 14032 603 41 0 15037 0
vsize: 60312
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 15746 0 0 0 26960 42 0 0 25 0 1 0 547294045 62414848 14166 4294967295 134512640 134672761 3221224544 3221223728 134615996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15238 14166 603 41 0 15197 0
vsize: 60952
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 16087 0 0 0 27959 43 0 0 25 0 1 0 547294045 63737856 14507 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15561 14507 603 41 0 15520 0
vsize: 62244
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 16445 0 0 0 28958 44 0 0 25 0 1 0 547294045 65196032 14865 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15917 14865 603 41 0 15876 0
vsize: 63668
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 16946 0 0 0 29957 46 0 0 25 0 1 0 547294045 67313664 15366 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16434 15366 603 41 0 16393 0
vsize: 65736
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 17318 0 0 0 30956 47 0 0 25 0 1 0 547294045 68771840 15738 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16790 15738 603 41 0 16749 0
vsize: 67160
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 17576 0 0 0 31955 48 0 0 25 0 1 0 547294045 69832704 15996 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17049 15996 603 41 0 17008 0
vsize: 68196
[startup+330.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 17891 0 0 0 32954 49 0 0 25 0 1 0 547294045 71151616 16311 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17371 16311 603 41 0 17330 0
vsize: 69484
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 18177 0 0 0 33953 50 0 0 25 0 1 0 547294045 72220672 16597 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17632 16597 603 41 0 17591 0
vsize: 70528
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 18553 0 0 0 34952 51 0 0 25 0 1 0 547294045 73809920 16973 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18020 16973 603 41 0 17979 0
vsize: 72080
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 18886 0 0 0 35952 52 0 0 25 0 1 0 547294045 75128832 17306 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18342 17306 603 41 0 18301 0
vsize: 73368
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 19415 0 0 0 36950 54 0 0 25 0 1 0 547294045 77234176 17835 4294967295 134512640 134672761 3221224544 3221223728 134615581 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18856 17835 603 41 0 18815 0
vsize: 75424
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 19998 0 0 0 37948 56 0 0 25 0 1 0 547294045 79609856 18418 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19436 18418 603 41 0 19395 0
vsize: 77744
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 20483 0 0 0 38947 57 0 0 25 0 1 0 547294045 81596416 18903 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19921 18903 603 41 0 19880 0
vsize: 79684
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 20933 0 0 0 39946 58 0 0 25 0 1 0 547294045 83460096 19353 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20376 19353 603 41 0 20335 0
vsize: 81504
[startup+410.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 21220 0 0 0 40945 59 0 0 25 0 1 0 547294045 84668416 19640 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20671 19640 603 41 0 20630 0
vsize: 82684
[startup+420.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 21564 0 0 0 41945 60 0 0 25 0 1 0 547294045 85987328 19984 4294967295 134512640 134672761 3221224544 3221223728 134615785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20993 19984 603 41 0 20952 0
vsize: 83972
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 21842 0 0 0 42944 61 0 0 25 0 1 0 547294045 87183360 20262 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21285 20262 603 41 0 21244 0
vsize: 85140
[startup+440.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 22245 0 0 0 43943 63 0 0 25 0 1 0 547294045 88768512 20665 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21672 20665 603 41 0 21631 0
vsize: 86688
[startup+450.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 22776 0 0 0 44941 65 0 0 25 0 1 0 547294045 91013120 21196 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22220 21196 603 41 0 22179 0
vsize: 88880
[startup+460.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 23233 0 0 0 45940 66 0 0 25 0 1 0 547294045 92860416 21653 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22671 21653 603 41 0 22630 0
vsize: 90684
[startup+470.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 23618 0 0 0 46939 67 0 0 25 0 1 0 547294045 94466048 22038 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23063 22038 603 41 0 23022 0
vsize: 92252
[startup+480.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 23989 0 0 0 47938 68 0 0 25 0 1 0 547294045 95899648 22409 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23413 22409 603 41 0 23372 0
vsize: 93652
[startup+490.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 24297 0 0 0 48938 68 0 0 25 0 1 0 547294045 97746944 22717 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23864 22717 603 41 0 23823 0
vsize: 95456
[startup+500.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 24699 0 0 0 49937 70 0 0 25 0 1 0 547294045 99323904 23119 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24249 23119 603 41 0 24208 0
vsize: 96996
[startup+510.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 25277 0 0 0 50936 71 0 0 25 0 1 0 547294045 101699584 23697 4294967295 134512640 134672761 3221224544 3221223584 134613818 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24829 23697 603 41 0 24788 0
vsize: 99316
[startup+520.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 25823 0 0 0 51935 72 0 0 25 0 1 0 547294045 103944192 24243 4294967295 134512640 134672761 3221224544 3221223744 134610675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25377 24243 603 41 0 25336 0
vsize: 101508
[startup+530.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26348 0 0 0 52934 74 0 0 25 0 1 0 547294045 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+540.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26348 0 0 0 53934 74 0 0 25 0 1 0 547294045 105500672 24630 4294967295 134512640 134672761 3221224544 3221223536 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+550.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26348 0 0 0 54934 74 0 0 25 0 1 0 547294045 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+560.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26348 0 0 0 55934 74 0 0 25 0 1 0 547294045 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+570.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26348 0 0 0 56934 74 0 0 25 0 1 0 547294045 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+580.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26348 0 0 0 57935 74 0 0 25 0 1 0 547294045 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+590.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26348 0 0 0 58935 74 0 0 25 0 1 0 547294045 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+600.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26348 0 0 0 59935 74 0 0 25 0 1 0 547294045 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+610.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26348 0 0 0 60935 74 0 0 25 0 1 0 547294045 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+620.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26348 0 0 0 61935 74 0 0 25 0 1 0 547294045 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+630.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26348 0 0 0 62936 74 0 0 25 0 1 0 547294045 105500672 24630 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+640.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26348 0 0 0 63936 74 0 0 25 0 1 0 547294045 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+650.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26348 0 0 0 64936 74 0 0 25 0 1 0 547294045 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+660.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26348 0 0 0 65936 74 0 0 25 0 1 0 547294045 105500672 24630 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+670.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26348 0 0 0 66936 74 0 0 25 0 1 0 547294045 105500672 24630 4294967295 134512640 134672761 3221224544 3221223680 134614724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+680.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26348 0 0 0 67936 74 0 0 25 0 1 0 547294045 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+690.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26348 0 0 0 68937 74 0 0 25 0 1 0 547294045 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+700.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26348 0 0 0 69937 74 0 0 25 0 1 0 547294045 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+710.016 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26348 0 0 0 70937 74 0 0 25 0 1 0 547294045 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+720.017 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26348 0 0 0 71937 74 0 0 25 0 1 0 547294045 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+730.016 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26348 0 0 0 72937 74 0 0 25 0 1 0 547294045 105500672 24630 4294967295 134512640 134672761 3221224544 3221223688 134616317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+740.017 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26348 0 0 0 73938 74 0 0 25 0 1 0 547294045 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+750.017 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26348 0 0 0 74938 74 0 0 25 0 1 0 547294045 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615796 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+760.017 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26348 0 0 0 75938 74 0 0 25 0 1 0 547294045 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+770.018 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26348 0 0 0 76938 74 0 0 25 0 1 0 547294045 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+780.018 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26348 0 0 0 77938 74 0 0 25 0 1 0 547294045 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+790.018 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26348 0 0 0 78939 74 0 0 25 0 1 0 547294045 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+800.019 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26348 0 0 0 79939 74 0 0 25 0 1 0 547294045 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+810.019 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26348 0 0 0 80939 74 0 0 25 0 1 0 547294045 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+820.018 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26348 0 0 0 81939 74 0 0 25 0 1 0 547294045 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615951 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+830.018 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26348 0 0 0 82939 74 0 0 25 0 1 0 547294045 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+840.019 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26348 0 0 0 83940 74 0 0 25 0 1 0 547294045 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+850.018 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26348 0 0 0 84940 74 0 0 25 0 1 0 547294045 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615788 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+860.018 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26348 0 0 0 85940 74 0 0 25 0 1 0 547294045 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+870.019 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26390 0 0 0 86940 74 0 0 25 0 1 0 547294045 105762816 24672 4294967295 134512640 134672761 3221224544 3221223688 134616263 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25821 24672 603 41 0 25780 0
vsize: 103284
[startup+880.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 26665 0 0 0 87940 75 0 0 25 0 1 0 547294045 106827776 24947 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26081 24947 603 41 0 26040 0
vsize: 104324
[startup+890.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 27074 0 0 0 88939 76 0 0 25 0 1 0 547294045 108544000 25356 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26500 25356 603 41 0 26459 0
vsize: 106000
[startup+900.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 27478 0 0 0 89938 77 0 0 25 0 1 0 547294045 110137344 25760 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26889 25760 603 41 0 26848 0
vsize: 107556
[startup+910.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 27870 0 0 0 90937 78 0 0 25 0 1 0 547294045 111857664 26152 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27309 26152 603 41 0 27268 0
vsize: 109236
[startup+920.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 28262 0 0 0 91936 80 0 0 25 0 1 0 547294045 113442816 26544 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27696 26544 603 41 0 27655 0
vsize: 110784
[startup+930.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 28643 0 0 0 92935 81 0 0 25 0 1 0 547294045 115019776 26925 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28081 26925 603 41 0 28040 0
vsize: 112324
[startup+940.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 29063 0 0 0 93934 82 0 0 25 0 1 0 547294045 116736000 27345 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28500 27345 603 41 0 28459 0
vsize: 114000
[startup+950.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 29551 0 0 0 94932 84 0 0 25 0 1 0 547294045 118710272 27833 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28982 27833 603 41 0 28941 0
vsize: 115928
[startup+960.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 29987 0 0 0 95931 85 0 0 25 0 1 0 547294045 120430592 28269 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29402 28269 603 41 0 29361 0
vsize: 117608
[startup+970.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 30463 0 0 0 96930 86 0 0 25 0 1 0 547294045 122400768 28745 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29883 28745 603 41 0 29842 0
vsize: 119532
[startup+980.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 30837 0 0 0 97929 88 0 0 25 0 1 0 547294045 123994112 29119 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30272 29119 603 41 0 30231 0
vsize: 121088
[startup+990.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 31193 0 0 0 98928 89 0 0 25 0 1 0 547294045 125448192 29475 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30627 29475 603 41 0 30586 0
vsize: 122508
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 31702 0 0 0 99927 90 0 0 25 0 1 0 547294045 127442944 29984 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31114 29984 603 41 0 31073 0
vsize: 124456
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 32269 0 0 0 100925 92 0 0 25 0 1 0 547294045 129818624 30551 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31694 30551 603 41 0 31653 0
vsize: 126776
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 32675 0 0 0 101924 94 0 0 25 0 1 0 547294045 131403776 30957 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32081 30957 603 41 0 32040 0
vsize: 128324
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 33076 0 0 0 102923 94 0 0 25 0 1 0 547294045 133120000 31358 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32500 31358 603 41 0 32459 0
vsize: 130000
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 33581 0 0 0 103922 96 0 0 25 0 1 0 547294045 135241728 31863 4294967295 134512640 134672761 3221224544 3221223728 134615635 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33018 31863 603 41 0 32977 0
vsize: 132072
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 34028 0 0 0 104920 98 0 0 25 0 1 0 547294045 136962048 32310 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33438 32310 603 41 0 33397 0
vsize: 133752
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 34504 0 0 0 105919 99 0 0 25 0 1 0 547294045 138936320 32786 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33920 32786 603 41 0 33879 0
vsize: 135680
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 35062 0 0 0 106919 99 0 0 25 0 1 0 547294045 141295616 33344 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34496 33344 603 41 0 34455 0
vsize: 137984
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 35579 0 0 0 107917 101 0 0 25 0 1 0 547294045 143286272 33861 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34982 33861 603 41 0 34941 0
vsize: 139928
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 36090 0 0 0 108916 102 0 0 25 0 1 0 547294045 145403904 34372 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35499 34372 603 41 0 35458 0
vsize: 141996
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 36625 0 0 0 109915 103 0 0 25 0 1 0 547294045 147161088 34710 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35928 34710 603 41 0 35887 0
vsize: 143712
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 36625 0 0 0 110916 103 0 0 25 0 1 0 547294045 147161088 34710 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35928 34710 603 41 0 35887 0
vsize: 143712
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 36625 0 0 0 111916 103 0 0 25 0 1 0 547294045 147161088 34710 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35928 34710 603 41 0 35887 0
vsize: 143712
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 36625 0 0 0 112916 103 0 0 25 0 1 0 547294045 147161088 34710 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35928 34710 603 41 0 35887 0
vsize: 143712
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 36626 0 0 0 113916 103 0 0 25 0 1 0 547294045 147161088 34711 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35928 34711 603 41 0 35887 0
vsize: 143712
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 36626 0 0 0 114916 103 0 0 25 0 1 0 547294045 147161088 34711 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35928 34711 603 41 0 35887 0
vsize: 143712
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 36626 0 0 0 115916 103 0 0 25 0 1 0 547294045 147161088 34711 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35928 34711 603 41 0 35887 0
vsize: 143712
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 36626 0 0 0 116917 103 0 0 25 0 1 0 547294045 147161088 34711 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35928 34711 603 41 0 35887 0
vsize: 143712
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 36626 0 0 0 117917 103 0 0 25 0 1 0 547294045 147161088 34711 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35928 34711 603 41 0 35887 0
vsize: 143712
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 36626 0 0 0 118917 103 0 0 25 0 1 0 547294045 147161088 34711 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35928 34711 603 41 0 35887 0
vsize: 143712
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29663
Raw data (stat): 29663 (minisat+) R 29662 10614 10613 0 -1 0 36626 0 0 0 119917 103 0 0 25 0 1 0 547294045 147161088 34711 4294967295 134512640 134672761 3221224544 3221223688 134616347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35928 34711 603 41 0 35887 0
vsize: 143712
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.95 1/54 29663
Raw data (stat): 29663 (minisat+) Z 29662 10614 10613 0 -1 12 36627 0 0 0 119917 110 0 0 25 0 1 0 547294045 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.09
CPU time (s): 1200.28
CPU user time (s): 1199.18
CPU system time (s): 1.10883
CPU usage (%): 100.016
Max. virtual memory (Kb): 143712
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####