PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-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.1944
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 17060

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        659088 kB
Buffers:         20348 kB
Cached:         324616 kB
SwapCached:         68 kB
Active:          31192 kB
Inactive:       316628 kB
HighTotal:      131008 kB
HighFree:        89236 kB
LowTotal:       903652 kB
LowFree:        569852 kB
SwapTotal:     2097892 kB
SwapFree:      2097800 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6876 kB
Slab:            21988 kB
Committed_AS:    63716 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 09:56:08 (client local time) WITH STATUS 10 IN 1200.28 SECONDS
stats: 11763 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: 124.626 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.71 0.84 0.88 2/54 29153
Raw data (stat): 29153 (runsolver) R 29152 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 544051870 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.75 0.85 0.88 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 4040 0 0 0 987 12 0 0 25 0 1 0 544051870 18165760 3632 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4435 3632 603 41 0 4394 0
vsize: 17740
[startup+20.002 s]
Raw data (loadavg): 0.79 0.85 0.88 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 4959 0 0 0 1983 15 0 0 25 0 1 0 544051870 21913600 4551 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5350 4551 603 41 0 5309 0
vsize: 21400
[startup+30.0022 s]
Raw data (loadavg): 0.82 0.86 0.88 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 5482 0 0 0 2982 17 0 0 25 0 1 0 544051870 24039424 5074 4294967295 134512640 134672761 3221224544 3221223688 134616336 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5869 5074 603 41 0 5828 0
vsize: 23476
[startup+40.0027 s]
Raw data (loadavg): 0.85 0.86 0.88 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 6405 0 0 0 3979 20 0 0 25 0 1 0 544051870 27750400 5997 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6775 5997 603 41 0 6734 0
vsize: 27100
[startup+50.0037 s]
Raw data (loadavg): 0.87 0.86 0.89 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 7025 0 0 0 4977 23 0 0 25 0 1 0 544051870 30404608 6617 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7423 6617 603 41 0 7382 0
vsize: 29692
[startup+60.0039 s]
Raw data (loadavg): 0.89 0.87 0.89 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 7649 0 0 0 5975 24 0 0 25 0 1 0 544051870 32923648 7241 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8038 7241 603 41 0 7997 0
vsize: 32152
[startup+70.0036 s]
Raw data (loadavg): 0.91 0.87 0.89 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 8254 0 0 0 6973 26 0 0 25 0 1 0 544051870 35450880 7846 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8655 7846 603 41 0 8614 0
vsize: 34620
[startup+80.0038 s]
Raw data (loadavg): 0.92 0.88 0.89 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 8910 0 0 0 7971 28 0 0 25 0 1 0 544051870 38105088 8502 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9303 8502 603 41 0 9262 0
vsize: 37212
[startup+90.0042 s]
Raw data (loadavg): 0.93 0.88 0.89 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 9485 0 0 0 8970 29 0 0 25 0 1 0 544051870 40378368 9077 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9858 9077 603 41 0 9817 0
vsize: 39432
[startup+100.004 s]
Raw data (loadavg): 0.94 0.88 0.89 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 10132 0 0 0 9968 31 0 0 25 0 1 0 544051870 43003904 9724 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10499 9724 603 41 0 10458 0
vsize: 41996
[startup+110.005 s]
Raw data (loadavg): 0.95 0.89 0.89 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 10682 0 0 0 10967 33 0 0 25 0 1 0 544051870 45514752 10274 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11112 10274 603 41 0 11071 0
vsize: 44448
[startup+120.004 s]
Raw data (loadavg): 0.96 0.89 0.89 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 11657 0 0 0 11964 36 0 0 25 0 1 0 544051870 49602560 11249 4294967295 134512640 134672761 3221224544 3221223584 134614258 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12110 11249 603 41 0 12069 0
vsize: 48440
[startup+130.004 s]
Raw data (loadavg): 0.96 0.89 0.89 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 15611 0 0 0 12953 47 0 0 25 0 1 0 544051870 61759488 14031 4294967295 134512640 134672761 3221224544 3221223728 134615991 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.005 s]
Raw data (loadavg): 0.97 0.90 0.89 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 15611 0 0 0 13953 47 0 0 25 0 1 0 544051870 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+150.005 s]
Raw data (loadavg): 0.97 0.90 0.89 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 15611 0 0 0 14952 47 0 0 25 0 1 0 544051870 61759488 14031 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15078 14031 603 41 0 15037 0
vsize: 60312
[startup+160.006 s]
Raw data (loadavg): 0.98 0.90 0.90 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 15611 0 0 0 15953 47 0 0 25 0 1 0 544051870 61759488 14031 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15078 14031 603 41 0 15037 0
vsize: 60312
[startup+170.006 s]
Raw data (loadavg): 0.98 0.90 0.90 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 15611 0 0 0 16953 47 0 0 25 0 1 0 544051870 61759488 14031 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15078 14031 603 41 0 15037 0
vsize: 60312
[startup+180.005 s]
Raw data (loadavg): 0.98 0.91 0.90 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 15611 0 0 0 17953 47 0 0 25 0 1 0 544051870 61759488 14031 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15078 14031 603 41 0 15037 0
vsize: 60312
[startup+190.006 s]
Raw data (loadavg): 0.98 0.91 0.90 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 15611 0 0 0 18953 47 0 0 25 0 1 0 544051870 61759488 14031 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15078 14031 603 41 0 15037 0
vsize: 60312
[startup+200.006 s]
Raw data (loadavg): 0.99 0.91 0.90 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 15611 0 0 0 19953 47 0 0 25 0 1 0 544051870 61759488 14031 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15078 14031 603 41 0 15037 0
vsize: 60312
[startup+210.006 s]
Raw data (loadavg): 0.99 0.91 0.90 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 15612 0 0 0 20954 47 0 0 25 0 1 0 544051870 61759488 14032 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15078 14032 603 41 0 15037 0
vsize: 60312
[startup+220.006 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 15612 0 0 0 21954 47 0 0 25 0 1 0 544051870 61759488 14032 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15078 14032 603 41 0 15037 0
vsize: 60312
[startup+230.006 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 15612 0 0 0 22954 47 0 0 25 0 1 0 544051870 61759488 14032 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15078 14032 603 41 0 15037 0
vsize: 60312
[startup+240.006 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 15612 0 0 0 23954 47 0 0 25 0 1 0 544051870 61759488 14032 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15078 14032 603 41 0 15037 0
vsize: 60312
[startup+250.006 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 15612 0 0 0 24954 47 0 0 25 0 1 0 544051870 61759488 14032 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15078 14032 603 41 0 15037 0
vsize: 60312
[startup+260.007 s]
Raw data (loadavg): 0.99 0.92 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 15612 0 0 0 25954 47 0 0 25 0 1 0 544051870 61759488 14032 4294967295 134512640 134672761 3221224544 3221223728 134615585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15078 14032 603 41 0 15037 0
vsize: 60312
[startup+270.008 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 15612 0 0 0 26955 48 0 0 25 0 1 0 544051870 61759488 14032 4294967295 134512640 134672761 3221224544 3221223728 134615964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15078 14032 603 41 0 15037 0
vsize: 60312
[startup+280.007 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 15838 0 0 0 27954 49 0 0 25 0 1 0 544051870 62681088 14258 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15303 14258 603 41 0 15262 0
vsize: 61212
[startup+290.007 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 16184 0 0 0 28953 49 0 0 25 0 1 0 544051870 64139264 14604 4294967295 134512640 134672761 3221224544 3221223688 134616170 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15659 14604 603 41 0 15618 0
vsize: 62636
[startup+300.007 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 16561 0 0 0 29952 50 0 0 25 0 1 0 544051870 65732608 14981 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16048 14981 603 41 0 16007 0
vsize: 64192
[startup+310.007 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 16997 0 0 0 30951 51 0 0 25 0 1 0 544051870 67448832 15417 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16467 15417 603 41 0 16426 0
vsize: 65868
[startup+320.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 17353 0 0 0 31950 53 0 0 25 0 1 0 544051870 68902912 15773 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16822 15773 603 41 0 16781 0
vsize: 67288
[startup+330.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 17599 0 0 0 32949 54 0 0 25 0 1 0 544051870 69963776 16019 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17081 16019 603 41 0 17040 0
vsize: 68324
[startup+340.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 17899 0 0 0 33949 54 0 0 25 0 1 0 544051870 71151616 16319 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17371 16319 603 41 0 17330 0
vsize: 69484
[startup+350.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 18179 0 0 0 34948 55 0 0 25 0 1 0 544051870 72220672 16599 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17632 16599 603 41 0 17591 0
vsize: 70528
[startup+360.008 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 18546 0 0 0 35948 56 0 0 25 0 1 0 544051870 73809920 16966 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18020 16966 603 41 0 17979 0
vsize: 72080
[startup+370.008 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 18860 0 0 0 36946 57 0 0 25 0 1 0 544051870 74993664 17280 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18309 17280 603 41 0 18268 0
vsize: 73236
[startup+380.008 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 19342 0 0 0 37945 59 0 0 25 0 1 0 544051870 76976128 17762 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18793 17762 603 41 0 18752 0
vsize: 75172
[startup+390.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 19953 0 0 0 38943 61 0 0 25 0 1 0 544051870 79478784 18373 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19404 18373 603 41 0 19363 0
vsize: 77616
[startup+400.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 20402 0 0 0 39941 63 0 0 25 0 1 0 544051870 81326080 18822 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19855 18822 603 41 0 19814 0
vsize: 79420
[startup+410.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 20834 0 0 0 40941 64 0 0 25 0 1 0 544051870 83058688 19254 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20278 19254 603 41 0 20237 0
vsize: 81112
[startup+420.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 21144 0 0 0 41940 65 0 0 25 0 1 0 544051870 84402176 19564 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20606 19564 603 41 0 20565 0
vsize: 82424
[startup+430.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 21495 0 0 0 42939 66 0 0 25 0 1 0 544051870 85721088 19915 4294967295 134512640 134672761 3221224544 3221223688 134616139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20928 19915 603 41 0 20887 0
vsize: 83712
[startup+440.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 21782 0 0 0 43939 66 0 0 25 0 1 0 544051870 86913024 20202 4294967295 134512640 134672761 3221224544 3221223688 134616132 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21219 20202 603 41 0 21178 0
vsize: 84876
[startup+450.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 22116 0 0 0 44938 68 0 0 25 0 1 0 544051870 88244224 20536 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21544 20536 603 41 0 21503 0
vsize: 86176
[startup+460.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 22566 0 0 0 45937 69 0 0 25 0 1 0 544051870 90087424 20986 4294967295 134512640 134672761 3221224544 3221223728 134615611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21994 20986 603 41 0 21953 0
vsize: 87976
[startup+470.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 23116 0 0 0 46935 71 0 0 25 0 1 0 544051870 92327936 21536 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22541 21536 603 41 0 22500 0
vsize: 90164
[startup+480.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 23400 0 0 0 47935 71 0 0 25 0 1 0 544051870 93532160 21820 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22835 21820 603 41 0 22794 0
vsize: 91340
[startup+490.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 23893 0 0 0 48934 72 0 0 25 0 1 0 544051870 95506432 22313 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23317 22313 603 41 0 23276 0
vsize: 93268
[startup+500.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 24124 0 0 0 49933 73 0 0 25 0 1 0 544051870 97087488 22544 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23703 22544 603 41 0 23662 0
vsize: 94812
[startup+510.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 24427 0 0 0 50933 74 0 0 25 0 1 0 544051870 98275328 22847 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23993 22847 603 41 0 23952 0
vsize: 95972
[startup+520.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 24921 0 0 0 51931 76 0 0 25 0 1 0 544051870 100253696 23341 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24476 23341 603 41 0 24435 0
vsize: 97904
[startup+530.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 25503 0 0 0 52930 77 0 0 25 0 1 0 544051870 102621184 23923 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25054 23923 603 41 0 25013 0
vsize: 100216
[startup+540.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26003 0 0 0 53929 79 0 0 25 0 1 0 544051870 104734720 24423 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25570 24423 603 41 0 25529 0
vsize: 102280
[startup+550.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 54928 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615523 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+560.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 55929 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+570.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 56929 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+580.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 57929 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+590.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 58929 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+600.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 59929 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615767 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+610.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 60930 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+620.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 61930 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+630.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 62930 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+640.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 63930 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+650.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 64930 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+660.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 65931 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+670.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 66931 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+680.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 67931 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+690.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 68931 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+700.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 69931 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+710.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 70932 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+720.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 71932 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+730.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 72932 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+740.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 73932 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+750.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 74933 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+760.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 75933 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+770.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 76933 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+780.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 77933 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+790.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 78933 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 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.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 79933 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223744 134610705 0 0 5 16386 0 0 0 17 0 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.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 80934 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+820.019 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 81934 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+830.019 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 82934 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+840.019 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 83934 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+850.019 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 84934 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223688 134616183 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+860.02 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 85935 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+870.02 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 86935 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+880.02 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 87935 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615794 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+890.02 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26348 0 0 0 88935 79 0 0 25 0 1 0 544051870 105500672 24630 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25757 24630 603 41 0 25716 0
vsize: 103028
[startup+900.019 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26417 0 0 0 89935 79 0 0 25 0 1 0 544051870 105897984 24699 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25854 24699 603 41 0 25813 0
vsize: 103416
[startup+910.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 26720 0 0 0 90934 80 0 0 25 0 1 0 544051870 107094016 25002 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26146 25002 603 41 0 26105 0
vsize: 104584
[startup+920.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 27112 0 0 0 91934 81 0 0 25 0 1 0 544051870 108683264 25394 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26534 25394 603 41 0 26493 0
vsize: 106136
[startup+930.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 27505 0 0 0 92933 82 0 0 25 0 1 0 544051870 110272512 25787 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26922 25787 603 41 0 26881 0
vsize: 107688
[startup+940.02 s]
Raw data (loadavg): 1.16 1.02 0.93 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 27886 0 0 0 93933 83 0 0 25 0 1 0 544051870 111857664 26168 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27309 26168 603 41 0 27268 0
vsize: 109236
[startup+950.02 s]
Raw data (loadavg): 1.14 1.02 0.93 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 28267 0 0 0 94932 83 0 0 25 0 1 0 544051870 113442816 26549 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27696 26549 603 41 0 27655 0
vsize: 110784
[startup+960.021 s]
Raw data (loadavg): 1.11 1.02 0.93 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 28636 0 0 0 95931 84 0 0 25 0 1 0 544051870 114888704 26918 4294967295 134512640 134672761 3221224544 3221223584 134614205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28049 26918 603 41 0 28008 0
vsize: 112196
[startup+970.02 s]
Raw data (loadavg): 1.10 1.02 0.93 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 29042 0 0 0 96930 86 0 0 25 0 1 0 544051870 116604928 27324 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28468 27324 603 41 0 28427 0
vsize: 113872
[startup+980.021 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 29512 0 0 0 97928 88 0 0 25 0 1 0 544051870 118575104 27794 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28949 27794 603 41 0 28908 0
vsize: 115796
[startup+990.021 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 29947 0 0 0 98927 89 0 0 25 0 1 0 544051870 120295424 28229 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29369 28229 603 41 0 29328 0
vsize: 117476
[startup+1000.02 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 30413 0 0 0 99927 89 0 0 25 0 1 0 544051870 122269696 28695 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29851 28695 603 41 0 29810 0
vsize: 119404
[startup+1010.02 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 30774 0 0 0 100926 91 0 0 25 0 1 0 544051870 123727872 29056 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30207 29056 603 41 0 30166 0
vsize: 120828
[startup+1020.02 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 31118 0 0 0 101925 92 0 0 25 0 1 0 544051870 125050880 29400 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30530 29400 603 41 0 30489 0
vsize: 122120
[startup+1030.02 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 31583 0 0 0 102924 93 0 0 25 0 1 0 544051870 127041536 29865 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31016 29865 603 41 0 30975 0
vsize: 124064
[startup+1040.02 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 32146 0 0 0 103922 95 0 0 25 0 1 0 544051870 129290240 30428 4294967295 134512640 134672761 3221224544 3221223680 134614825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31565 30428 603 41 0 31524 0
vsize: 126260
[startup+1050.02 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 32571 0 0 0 104921 96 0 0 25 0 1 0 544051870 131010560 30853 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31985 30853 603 41 0 31944 0
vsize: 127940
[startup+1060.02 s]
Raw data (loadavg): 1.09 1.02 0.93 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 32968 0 0 0 105920 97 0 0 25 0 1 0 544051870 132591616 31250 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32371 31250 603 41 0 32330 0
vsize: 129484
[startup+1070.02 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 33434 0 0 0 106917 100 0 0 25 0 1 0 544051870 134578176 31716 4294967295 134512640 134672761 3221224544 3221223584 134603522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32856 31716 603 41 0 32815 0
vsize: 131424
[startup+1080.02 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 33870 0 0 0 107916 101 0 0 25 0 1 0 544051870 136302592 32152 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33277 32152 603 41 0 33236 0
vsize: 133108
[startup+1090.02 s]
Raw data (loadavg): 1.06 1.02 0.93 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 34329 0 0 0 108916 102 0 0 25 0 1 0 544051870 138276864 32611 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33759 32611 603 41 0 33718 0
vsize: 135036
[startup+1100.02 s]
Raw data (loadavg): 1.05 1.02 0.93 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 34861 0 0 0 109914 104 0 0 25 0 1 0 544051870 140378112 33143 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34272 33143 603 41 0 34231 0
vsize: 137088
[startup+1110.02 s]
Raw data (loadavg): 1.04 1.02 0.93 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 35354 0 0 0 110913 105 0 0 25 0 1 0 544051870 142491648 33636 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34788 33636 603 41 0 34747 0
vsize: 139152
[startup+1120.02 s]
Raw data (loadavg): 1.03 1.02 0.93 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 35877 0 0 0 111911 107 0 0 25 0 1 0 544051870 144613376 34159 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35306 34159 603 41 0 35265 0
vsize: 141224
[startup+1130.02 s]
Raw data (loadavg): 1.03 1.02 0.93 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 36339 0 0 0 112911 108 0 0 25 0 1 0 544051870 146464768 34621 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35758 34621 603 41 0 35717 0
vsize: 143032
[startup+1140.02 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 36625 0 0 0 113910 109 0 0 25 0 1 0 544051870 147161088 34710 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35928 34710 603 41 0 35887 0
vsize: 143712
[startup+1150.02 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 36625 0 0 0 114910 109 0 0 25 0 1 0 544051870 147161088 34710 4294967295 134512640 134672761 3221224544 3221223584 134603542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35928 34710 603 41 0 35887 0
vsize: 143712
[startup+1160.02 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 36625 0 0 0 115910 109 0 0 25 0 1 0 544051870 147161088 34710 4294967295 134512640 134672761 3221224544 3221223584 134613768 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35928 34710 603 41 0 35887 0
vsize: 143712
[startup+1170.02 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 36626 0 0 0 116910 109 0 0 25 0 1 0 544051870 147161088 34711 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35928 34711 603 41 0 35887 0
vsize: 143712
[startup+1180.02 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 36626 0 0 0 117910 109 0 0 25 0 1 0 544051870 147161088 34711 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35928 34711 603 41 0 35887 0
vsize: 143712
[startup+1190.03 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 36626 0 0 0 118911 109 0 0 25 0 1 0 544051870 147161088 34711 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35928 34711 603 41 0 35887 0
vsize: 143712
[startup+1200.03 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 29153
Raw data (stat): 29153 (minisat+) R 29152 22612 22611 0 -1 0 36626 0 0 0 119912 109 0 0 25 0 1 0 544051870 147161088 34711 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35928 34711 603 41 0 35887 0
vsize: 143712
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.2 s]
Raw data (loadavg): 1.01 1.01 0.93 1/54 29153
Raw data (stat): 29153 (minisat+) Z 29152 22612 22611 0 -1 12 36627 0 0 0 119912 116 0 0 24 0 1 0 544051870 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.2
CPU time (s): 1200.28
CPU user time (s): 1199.12
CPU system time (s): 1.16082
CPU usage (%): 100.007
Max. virtual memory (Kb): 143712
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####