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 15734

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc29 THE 2005-04-21 05:41:35 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16756 boxname=wulflinc29 idbench=1289 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  098fe473d82d5f7d4121673eb775be76  /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-cracpb1.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-cracpb1.opb /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-cracpb1.opb
IDLAUNCH: 16756
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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.020
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:        839420 kB
Buffers:         22296 kB
Cached:         144588 kB
SwapCached:        464 kB
Active:          44940 kB
Inactive:       124136 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        839168 kB
SwapTotal:     2097892 kB
SwapFree:      2096700 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5296 kB
Slab:            20292 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 06:01:38 (client local time) WITH STATUS 10 IN 1200.49 SECONDS
stats: 16756 7 1200.49 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]---> BDD-cost:198569
c ---[ 213]---> BDD-cost:  391
c ---[ 212]---> BDD-cost:  131
c ---[ 211]---> BDD-cost:  129
c ---[ 210]---> BDD-cost:  107
c ---[ 209]---> BDD-cost:  149
c ---[ 208]---> BDD-cost:  183
c ---[ 207]---> BDD-cost:  153
c ---[ 206]---> BDD-cost:   71
c ---[ 205]---> BDD-cost:  239
c ---[ 204]---> BDD-cost:   49
c ---[ 203]---> BDD-cost:   43
c ---[ 202]---> BDD-cost:   34
c ---[ 201]---> BDD-cost:   80
c ---[ 200]---> BDD-cost:   29
c ---[ 199]---> BDD-cost:   89
c ---[ 198]---> BDD-cost:   31
c ---[ 197]---> BDD-cost:   21
c ---[ 195]---> BDD-cost:  305
c ---[ 193]---> BDD-cost:   41
c ---[ 191]---> BDD-cost:  147
c ---[ 189]---> BDD-cost:  117
c ---[ 187]---> BDD-cost:  247
c ---[ 185]---> BDD-cost:  132
c ---[ 183]---> BDD-cost:  173
c ---[ 181]---> BDD-cost:   93
c ---[ 179]---> BDD-cost:  189
c ---[ 177]---> BDD-cost:   78
c ---[ 175]---> BDD-cost:   33
c ---[ 173]---> BDD-cost:  102
c ---[ 171]---> BDD-cost:   67
c ---[ 169]---> BDD-cost:   37
c ---[ 167]---> BDD-cost:   87
c ---[ 165]---> BDD-cost:   78
c ---[ 163]---> BDD-cost:   29
c ---[ 161]---> BDD-cost:   25
c ---[ 159]---> BDD-cost: 1509
c ---[ 157]---> BDD-cost:  459
c ---[ 155]---> BDD-cost:  517
c ---[ 153]---> BDD-cost:  434
c ---[ 151]---> BDD-cost:  536
c ---[ 149]---> BDD-cost:  717
c ---[ 147]---> BDD-cost:  577
c ---[ 145]---> BDD-cost:  263
c ---[ 143]---> BDD-cost:  837
c ---[ 141]---> BDD-cost:  228
c ---[ 139]---> BDD-cost:  135
c ---[ 137]---> BDD-cost:  177
c ---[ 135]---> BDD-cost:  317
c ---[ 133]---> BDD-cost:  127
c ---[ 131]---> BDD-cost:  337
c ---[ 129]---> BDD-cost:   77
c ---[ 127]---> BDD-cost:   66
c ---[ 126]---> BDD-cost:166596
c ---[ 125]---> BDD-cost:111032
c ---[ 124]---> BDD-cost: 5767
c ---[ 123]---> BDD-cost:   27
c ---[ 122]---> BDD-cost:   35
c ---[ 121]---> BDD-cost:   83
c ---[ 120]---> BDD-cost:   31
c ---[ 118]---> BDD-cost:   51
c ---[ 115]---> BDD-cost:   72
c ---[ 114]---> BDD-cost:  169
c ---[ 113]---> BDD-cost:  272
c ---[ 112]---> BDD-cost:  134
c ---[ 111]---> BDD-cost:   21
c ---[ 110]---> BDD-cost:  249
c ---[ 109]---> BDD-cost:   29
c ---[ 108]---> BDD-cost:   19
c ---[ 106]---> BDD-cost:   17
c ---[ 104]---> BDD-cost:   17
c ---[ 102]---> BDD-cost:    5
c ---[ 100]---> BDD-cost:   43
c ---[  98]---> BDD-cost:   93
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:   15
c ---[  72]---> BDD-cost:   39
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:   15
c ---[  48]---> BDD-cost:   25
c ---[  46]---> BDD-cost:    5
c ---[  44]---> BDD-cost:   13
c ---[  42]---> BDD-cost:   11
c ---[  40]---> BDD-cost:   13
c ---[  38]---> BDD-cost:   17
c ---[  36]---> BDD-cost:   19
c ---[  34]---> BDD-cost:   15
c ---[  32]---> BDD-cost:   19
c ---[  30]---> BDD-cost:   11
c ---[  28]---> BDD-cost:    5
c ---[  26]---> BDD-cost:   11
c ---[  24]---> BDD-cost:   15
c ---[  22]---> BDD-cost:   15
c ---[  20]---> BDD-cost:   49
c ---[  18]---> BDD-cost:   51
c ---[  16]---> BDD-cost:   10
c ---[  14]---> BDD-cost:    7
c ---[  12]---> BDD-cost:   51
c ---[  10]---> BDD-cost:    7
c ---[   8]---> BDD-cost:   13
c ---[   6]---> BDD-cost:   43
c ---[   4]---> BDD-cost:   31
c ---[   2]---> BDD-cost:   21
c ---[   0]---> BDD-cost:   17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 2017413  6040743 |  672471       0        0     nan |  0.000 % |
c |       100 | 2017413  6040743 |  739718     100     5565    55.6 |  0.025 % |
c |       254 | 2016609  6039135 |  813689     253    15136    59.8 |  0.106 % |
c |       479 | 2012702  6028744 |  895058     474    21248    44.8 |  0.278 % |
c |       818 | 1990570  5965222 |  984564     731    31877    43.6 |  1.235 % |
c |      1325 | 1990570  5965222 | 1083021    1238    74321    60.0 |  1.235 % |
c |      2084 | 1914234  5737543 | 1191323    1705   100970    59.2 |  4.569 % |
c |      3223 | 1913063  5734050 | 1310455    2842   274111    96.5 |  4.649 % |
c |      4932 | 1906572  5714577 | 1441501    4506   449354    99.7 |  5.019 % |
c |      7494 | 1904506  5708379 | 1585651    7018   625998    89.2 |  5.088 % |
c ==============================================================================
c [1mFound solution: 129868[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:201838     Base: 2 2 2 3 3 3 2 11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8221 | 2480071  7052159 |  826690    7698   682041    88.6 |  5.088 % |
c ==============================================================================
c [1mFound solution: 117210[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 3 3 3 2 11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8299 | 2482600  7059295 |  827533    7776   686356    88.3 |  5.088 % |
c |      8399 | 2482600  7059295 |  910286    7876   687799    87.3 |  3.663 % |
c |      8549 | 2482273  7058558 | 1001314    8023   688555    85.8 |  3.675 % |
c |      8774 | 2480275  7054004 | 1101446    8239   692103    84.0 |  3.756 % |
c |      9111 | 2480275  7054004 | 1211591    8576   694707    81.0 |  3.756 % |
c |      9617 | 2480176  7053783 | 1332750    9081   698522    76.9 |  3.759 % |
c |     10376 | 2479864  7053078 | 1466025    9832   705477    71.8 |  3.771 % |
c |     11516 | 2474362  7040492 | 1612627   10928   749486    68.6 |  4.003 % |
c |     13224 | 2462618  7005413 | 1773890   12478   829241    66.5 |  4.568 % |
c |     15787 | 2456454  6986921 | 1951279   14809  1101912    74.4 |  4.717 % |
c ==============================================================================
c [1mFound solution: 115568[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 3 3 3 2 11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19127 | 2454571  6982494 |  818190   18050  1408179    78.0 |  4.717 % |
c |     19229 | 2454571  6982494 |  900009   18152  1415852    78.0 |  4.775 % |
c |     19379 | 2454571  6982494 |  990009   18302  1447648    79.1 |  4.775 % |
c |     19606 | 2454444  6982209 | 1089010   18526  1465424    79.1 |  4.781 % |
c |     19945 | 2454444  6982209 | 1197911   18865  1488223    78.9 |  4.781 % |
c |     20451 | 2429821  6908340 | 1317703   19199  1531933    79.8 |  5.573 % |
c |     21210 | 2429196  6906919 | 1449473   19956  1586994    79.5 |  5.599 % |
c |     22349 | 2422428  6887290 | 1594420   20991  1648122    78.5 |  5.898 % |
c |     24058 | 2422296  6886894 | 1753862   22689  1762587    77.7 |  5.901 % |
c |     26620 | 2422296  6886894 | 1929249   25251  1929891    76.4 |  5.901 % |
c |     30466 | 2422296  6886894 | 2122174   29097  2157524    74.1 |  5.901 % |
c |     36232 | 2380924  6776148 | 2334391   34509  2408613    69.8 |  7.437 % |
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 -GPT00360_bit0 -GPT00361_bit0 -GPT00362_bit0 -GPT00363_bit0 -GPT00364_bit0 -GPT00365_bit0 -GPT00366_bit0 -GPT00367_bit0 -GPT00368_bit0 -GPT00369_bit0 -GPT00370_bit0 -GPT00371_bit0 -GPT00372_bit0 -GPT00373_bit0 -GPT00374_bit0 -GPT00375_bit0 -GPT00376_bit0 -GPT00377_bit0 -GPT00378_bit0 -GPT00379_bit0 -GPT00380_bit0 -GPT00381_bit0 -GPT00382_bit0 -GPT00383_bit0 -GPT00384_bit0 -GPT00385_bit0 -GPT00386_bit0 -GPT00387_bit0 GPT00388_bit0 -GPT00389_bit0 -GPT00390_bit0 -GPT00391_bit0 -GPT00392_bit0 -GPT00393_bit0 -GPT00394_bit0 -GPT00395_bit0 -GPT00396_bit0 -GPT00397_bit0 -GPT00398_bit0 -GPT00399_bit0 -GPT00400_bit0 -GPT00401_bit0 -GPT00402_bit0 -GPT00403_bit0 -GPT00404_bit0 -GPT00405_bit0 -GPT00406_bit0 -GPT00407_bit0 -GPT00408_bit0 -GPT00409_bit0 -GPT00410_bit0 -GPT00411_bit0 -GPT00412_bit0 -GPT00413_bit0 -GPT00414_bit0 -GPT00415_bit0 -GPT00416_bit0 -GPT00417_bit0 -GPT00418_bit0 -GPT00419_bit0 -GPT00420_bit0 -GPT00421_bit0 -GPT00422_bit0 -GPT00423_bit0 -GPT00424_bit0 -GPT00425_bit0 -GPT00426_bit0 -GPT00427_bit0 -GPT00428_bit0 -GPT00429_bit0 -GPT00430_bit0 -GPT00431_bit0 -GPT00432_bit0 GPT00433_bit0 -GPT00434_bit0 -GPT00435_bit0 -GPT00436_bit0 -GPT00437_bit0 -GPT00438_bit0 -GPT00439_bit0 -GPT00440_bit0 -GPT00441_bit0 -GPT00442_bit0 -GPT00443_bit0 -GPT00444_bit0 -GPT00445_bit0 -GPT00446_bit0 -GPT00447_bit0 -GPT00448_bit0 -GPT00449_bit0 -GPT00450_bit0 GPT00451_bit0 -GPT00452_bit0 -GPT00453_bit0 -GPT00454_bit0 -GPT00455_bit0 -GPT00456_bit0 -GPT00457_bit0 -GPT00458_bit0 -GPT00459_bit0 -GPT00460_bit0 -GPT00461_bit0 -GPT00462_bit0 -GPT00463_bit0 -GPT00464_bit0 -GPT00465_bit0 -GPT00466_bit0 -GPT00467_bit0 -GPT00468_bit0 -GPT00469_bit0 -GPT00470_bit0 -GPT00471_bit0 -GPT00472_bit0 -GPT00473_bit0 -GPT00474_bit0 -GPT00475_bit0 -GPT00476_bit0 -GPT00477_bit0 -GPT00478_bit0 -GPT00479_bit0 -GPT00480_bit0 -GPT00481_bit0 -GPT00482_bit0 -GPT00483_bit0 -GPT00484_bit0 -GPT00485_bit0 -GPT00486_bit0 -GPT00487_bit0 -GPT00488_bit0 -GPT00489_bit0 -GPT00490_bit0 -GPT00491_bit0 -GPT00492_bit0 -GPT00493_bit0 -GPT00494_bit0 -GPT00495_bit0 -GPT00496_bit0 -GPT00497_bit0 -GPT00498_bit0 -GPT00499_bit0 -GPT00500_bit0 -GPT00501_bit0 -GPT00502_bit0 -GPT00503_bit0 -GPT00504_bit0 -GPT00505_bit0 -GPT00506_bit0 -GPT00507_bit0 -GPT00508_bit0 -GPT00509_bit0 -GPT00510_bit0 -GPT00511_bit0 -GPT00512_bit0 -GPT00513_bit0 -GPT00514_bit0 -GPT00515_bit0 -GPT00516_bit0 -GPT00517_bit0 -GPT00518_bit0 ECAR0001_bit0 -ECAR0002_bit0 ECAR0003_bit0 ECAR0004_bit0 -ECAR0005_bit0 -ECAR0006_bit0 ECAR0007_bit0 -ECAR0008_bit0 ECAR0009_bit0 -ECAR0010_bit0 ECAR0011_bit0 -ECAR0012_bit0 -ECAR0013_bit0 ECAR0014_bit0 ECAR0015_bit0 ECAR0016_bit0 ECAR0017_bit0 -ECAR0018_bit0 -ECAR0019_bit0 -ECAR0020_bit0 -ECAR0021_bit0 -ECAR0022_bit0 ECAR0023_bit0 -ECAR0024_bit0 ECAR0025_bit0 -ECAR0026_bit0 -ECAR0027_bit0 ECAR0028_bit0 -ECAR00#### 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): 1.02 0.99 0.97 2/54 22854
Raw data (stat): 22854 (runsolver) R 22853 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542636652 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.0013 s]
Raw data (loadavg): 1.02 0.99 0.97 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 7112 0 0 0 982 16 0 0 25 0 1 0 542636652 20447232 4566 4294967295 134512640 134672761 3221224528 3221209296 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4992 4566 603 41 0 4951 0
vsize: 19968
[startup+20.002 s]
Raw data (loadavg): 1.02 0.99 0.97 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 13236 0 0 0 1969 30 0 0 25 0 1 0 542636652 31326208 7136 4294967295 134512640 134672761 3221224528 3221216768 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7648 7136 603 41 0 7607 0
vsize: 30592
[startup+30.0015 s]
Raw data (loadavg): 1.01 0.99 0.97 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 53545 0 0 0 2875 124 0 0 25 0 1 0 542636652 198168576 46443 4294967295 134512640 134672761 3221224528 3221223828 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48381 46443 603 41 0 48340 0
vsize: 193524
[startup+40.002 s]
Raw data (loadavg): 1.01 0.99 0.97 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 53891 0 0 0 3873 125 0 0 25 0 1 0 542636652 198979584 46789 4294967295 134512640 134672761 3221224528 3221223700 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48579 46789 603 41 0 48538 0
vsize: 194316
[startup+50.0025 s]
Raw data (loadavg): 1.01 0.99 0.97 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 54037 0 0 0 4872 126 0 0 25 0 1 0 542636652 198979584 46935 4294967295 134512640 134672761 3221224528 3221223700 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48579 46935 603 41 0 48538 0
vsize: 194316
[startup+60.0029 s]
Raw data (loadavg): 1.09 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 54046 0 0 0 5871 126 0 0 25 0 1 0 542636652 198979584 46944 4294967295 134512640 134672761 3221224528 3221223632 134560322 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48579 46944 603 41 0 48538 0
vsize: 194316
[startup+70.0029 s]
Raw data (loadavg): 1.07 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 54099 0 0 0 6871 126 0 0 25 0 1 0 542636652 199311360 46997 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48660 46997 603 41 0 48619 0
vsize: 194640
[startup+80.0028 s]
Raw data (loadavg): 1.06 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 54105 0 0 0 7871 126 0 0 25 0 1 0 542636652 199311360 47003 4294967295 134512640 134672761 3221224528 3221223700 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48660 47003 603 41 0 48619 0
vsize: 194640
[startup+90.0032 s]
Raw data (loadavg): 1.05 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 54105 0 0 0 8871 126 0 0 25 0 1 0 542636652 199311360 47003 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48660 47003 603 41 0 48619 0
vsize: 194640
[startup+100.004 s]
Raw data (loadavg): 1.04 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 54195 0 0 0 9870 127 0 0 25 0 1 0 542636652 199311360 47093 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48660 47093 603 41 0 48619 0
vsize: 194640
[startup+110.005 s]
Raw data (loadavg): 1.04 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 54223 0 0 0 10870 127 0 0 25 0 1 0 542636652 199446528 47121 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48693 47121 603 41 0 48652 0
vsize: 194772
[startup+120.006 s]
Raw data (loadavg): 1.03 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 54272 0 0 0 11870 127 0 0 25 0 1 0 542636652 199577600 47170 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48725 47170 603 41 0 48684 0
vsize: 194900
[startup+130.006 s]
Raw data (loadavg): 1.02 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 54317 0 0 0 12870 127 0 0 25 0 1 0 542636652 199712768 47215 4294967295 134512640 134672761 3221224528 3221223632 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48758 47215 603 41 0 48717 0
vsize: 195032
[startup+140.006 s]
Raw data (loadavg): 1.02 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 54390 0 0 0 13870 128 0 0 25 0 1 0 542636652 200110080 47288 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48855 47288 603 41 0 48814 0
vsize: 195420
[startup+150.007 s]
Raw data (loadavg): 1.02 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 54390 0 0 0 14870 128 0 0 25 0 1 0 542636652 200110080 47288 4294967295 134512640 134672761 3221224528 3221223700 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48855 47288 603 41 0 48814 0
vsize: 195420
[startup+160.008 s]
Raw data (loadavg): 1.01 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 54390 0 0 0 15870 128 0 0 25 0 1 0 542636652 200110080 47288 4294967295 134512640 134672761 3221224528 3221223632 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48855 47288 603 41 0 48814 0
vsize: 195420
[startup+170.009 s]
Raw data (loadavg): 1.01 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 54390 0 0 0 16870 128 0 0 25 0 1 0 542636652 200110080 47288 4294967295 134512640 134672761 3221224528 3221223632 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48855 47288 603 41 0 48814 0
vsize: 195420
[startup+180.008 s]
Raw data (loadavg): 1.01 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 54401 0 0 0 17870 128 0 0 25 0 1 0 542636652 200110080 47299 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48855 47299 603 41 0 48814 0
vsize: 195420
[startup+190.008 s]
Raw data (loadavg): 1.01 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 54412 0 0 0 18870 128 0 0 25 0 1 0 542636652 200245248 47310 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48888 47310 603 41 0 48847 0
vsize: 195552
[startup+200.008 s]
Raw data (loadavg): 1.01 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 54426 0 0 0 19870 129 0 0 25 0 1 0 542636652 200245248 47324 4294967295 134512640 134672761 3221224528 3221223632 134560226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48888 47324 603 41 0 48847 0
vsize: 195552
[startup+210.009 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 54449 0 0 0 20871 129 0 0 25 0 1 0 542636652 200380416 47347 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48921 47347 603 41 0 48880 0
vsize: 195684
[startup+220.009 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 54475 0 0 0 21871 129 0 0 25 0 1 0 542636652 200515584 47373 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48954 47373 603 41 0 48913 0
vsize: 195816
[startup+230.008 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 54493 0 0 0 22871 129 0 0 25 0 1 0 542636652 200515584 47391 4294967295 134512640 134672761 3221224528 3221223732 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48954 47391 603 41 0 48913 0
vsize: 195816
[startup+240.009 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 54497 0 0 0 23871 129 0 0 25 0 1 0 542636652 200515584 47395 4294967295 134512640 134672761 3221224528 3221223696 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48954 47395 603 41 0 48913 0
vsize: 195816
[startup+250.009 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 54519 0 0 0 24871 129 0 0 25 0 1 0 542636652 200650752 47417 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48987 47417 603 41 0 48946 0
vsize: 195948
[startup+260.01 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 54570 0 0 0 25871 129 0 0 25 0 1 0 542636652 200921088 47468 4294967295 134512640 134672761 3221224528 3221223712 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49053 47468 603 41 0 49012 0
vsize: 196212
[startup+270.009 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 54625 0 0 0 26871 129 0 0 25 0 1 0 542636652 201056256 47523 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49086 47523 603 41 0 49045 0
vsize: 196344
[startup+280.01 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 54647 0 0 0 27871 130 0 0 25 0 1 0 542636652 201191424 47545 4294967295 134512640 134672761 3221224528 3221223728 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49119 47545 603 41 0 49078 0
vsize: 196476
[startup+290.01 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 54661 0 0 0 28871 130 0 0 25 0 1 0 542636652 201191424 47559 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49119 47559 603 41 0 49078 0
vsize: 196476
[startup+300.01 s]
Raw data (loadavg): 1.08 1.02 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 62506 0 0 0 29853 148 0 0 25 0 1 0 542636652 261226496 54086 4294967295 134512640 134672761 3221224528 3221173488 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63776 54087 603 41 0 63735 0
vsize: 255104
[startup+310.011 s]
Raw data (loadavg): 1.07 1.02 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 72580 0 0 0 30830 171 0 0 25 0 1 0 542636652 301760512 64147 4294967295 134512640 134672761 3221224528 3221223696 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73672 64147 603 41 0 73631 0
vsize: 294688
[startup+320.012 s]
Raw data (loadavg): 1.06 1.01 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 72583 0 0 0 31830 171 0 0 25 0 1 0 542636652 301760512 64150 4294967295 134512640 134672761 3221224528 3221223692 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73672 64150 603 41 0 73631 0
vsize: 294688
[startup+330.011 s]
Raw data (loadavg): 1.05 1.01 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 72614 0 0 0 32830 171 0 0 25 0 1 0 542636652 301953024 64181 4294967295 134512640 134672761 3221224528 3221223700 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73719 64181 603 41 0 73678 0
vsize: 294876
[startup+340.011 s]
Raw data (loadavg): 1.04 1.01 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 72615 0 0 0 33830 171 0 0 25 0 1 0 542636652 301953024 64182 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73719 64182 603 41 0 73678 0
vsize: 294876
[startup+350.012 s]
Raw data (loadavg): 1.03 1.01 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 72630 0 0 0 34831 171 0 0 25 0 1 0 542636652 301953024 64197 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73719 64197 603 41 0 73678 0
vsize: 294876
[startup+360.012 s]
Raw data (loadavg): 1.03 1.01 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 72648 0 0 0 35831 171 0 0 25 0 1 0 542636652 302084096 64215 4294967295 134512640 134672761 3221224528 3221223692 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73751 64215 603 41 0 73710 0
vsize: 295004
[startup+370.012 s]
Raw data (loadavg): 1.02 1.01 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 72658 0 0 0 36831 171 0 0 25 0 1 0 542636652 302084096 64225 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73751 64225 603 41 0 73710 0
vsize: 295004
[startup+380.012 s]
Raw data (loadavg): 1.02 1.01 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 72677 0 0 0 37831 171 0 0 25 0 1 0 542636652 302219264 64244 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73784 64244 603 41 0 73743 0
vsize: 295136
[startup+390.013 s]
Raw data (loadavg): 1.02 1.01 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 72700 0 0 0 38831 172 0 0 25 0 1 0 542636652 302354432 64267 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73817 64267 603 41 0 73776 0
vsize: 295268
[startup+400.013 s]
Raw data (loadavg): 1.01 1.01 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 72713 0 0 0 39831 172 0 0 25 0 1 0 542636652 302354432 64280 4294967295 134512640 134672761 3221224528 3221223696 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73817 64280 603 41 0 73776 0
vsize: 295268
[startup+410.014 s]
Raw data (loadavg): 1.01 1.01 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 72732 0 0 0 40832 172 0 0 25 0 1 0 542636652 302354432 64299 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73817 64299 603 41 0 73776 0
vsize: 295268
[startup+420.014 s]
Raw data (loadavg): 1.01 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 72740 0 0 0 41832 172 0 0 25 0 1 0 542636652 302489600 64307 4294967295 134512640 134672761 3221224528 3221223700 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73850 64307 603 41 0 73809 0
vsize: 295400
[startup+430.014 s]
Raw data (loadavg): 1.01 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 72740 0 0 0 42832 172 0 0 25 0 1 0 542636652 302489600 64307 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73850 64307 603 41 0 73809 0
vsize: 295400
[startup+440.015 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 72750 0 0 0 43832 172 0 0 25 0 1 0 542636652 302489600 64317 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73850 64317 603 41 0 73809 0
vsize: 295400
[startup+450.015 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 72768 0 0 0 44832 172 0 0 25 0 1 0 542636652 302624768 64335 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73883 64335 603 41 0 73842 0
vsize: 295532
[startup+460.017 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 72776 0 0 0 45832 172 0 0 25 0 1 0 542636652 302624768 64343 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73883 64343 603 41 0 73842 0
vsize: 295532
[startup+470.017 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 72789 0 0 0 46832 172 0 0 25 0 1 0 542636652 302624768 64356 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73883 64356 603 41 0 73842 0
vsize: 295532
[startup+480.017 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 72817 0 0 0 47832 172 0 0 25 0 1 0 542636652 302759936 64384 4294967295 134512640 134672761 3221224528 3221223696 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73916 64384 603 41 0 73875 0
vsize: 295664
[startup+490.018 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 72847 0 0 0 48832 173 0 0 25 0 1 0 542636652 302895104 64414 4294967295 134512640 134672761 3221224528 3221223712 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73949 64414 603 41 0 73908 0
vsize: 295796
[startup+500.018 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 72880 0 0 0 49832 173 0 0 25 0 1 0 542636652 303030272 64447 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73982 64447 603 41 0 73941 0
vsize: 295928
[startup+510.018 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 72924 0 0 0 50832 173 0 0 25 0 1 0 542636652 303165440 64491 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74015 64491 603 41 0 73974 0
vsize: 296060
[startup+520.019 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 72961 0 0 0 51832 173 0 0 25 0 1 0 542636652 303300608 64528 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74048 64528 603 41 0 74007 0
vsize: 296192
[startup+530.019 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 72997 0 0 0 52832 174 0 0 25 0 1 0 542636652 303431680 64564 4294967295 134512640 134672761 3221224528 3221223696 134560785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74080 64564 603 41 0 74039 0
vsize: 296320
[startup+540.02 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73020 0 0 0 53832 174 0 0 25 0 1 0 542636652 303566848 64587 4294967295 134512640 134672761 3221224528 3221223696 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74113 64587 603 41 0 74072 0
vsize: 296452
[startup+550.02 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73043 0 0 0 54832 174 0 0 25 0 1 0 542636652 303697920 64610 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74145 64610 603 41 0 74104 0
vsize: 296580
[startup+560.02 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73075 0 0 0 55832 174 0 0 25 0 1 0 542636652 303828992 64642 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74177 64642 603 41 0 74136 0
vsize: 296708
[startup+570.02 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73100 0 0 0 56832 174 0 0 25 0 1 0 542636652 303964160 64667 4294967295 134512640 134672761 3221224528 3221223676 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74210 64667 603 41 0 74169 0
vsize: 296840
[startup+580.02 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73126 0 0 0 57832 174 0 0 25 0 1 0 542636652 303964160 64693 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74210 64693 603 41 0 74169 0
vsize: 296840
[startup+590.021 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73156 0 0 0 58832 174 0 0 25 0 1 0 542636652 304226304 64723 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74274 64723 603 41 0 74233 0
vsize: 297096
[startup+600.02 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73183 0 0 0 59832 174 0 0 25 0 1 0 542636652 304361472 64750 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74307 64750 603 41 0 74266 0
vsize: 297228
[startup+610.021 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73185 0 0 0 60832 174 0 0 25 0 1 0 542636652 304361472 64752 4294967295 134512640 134672761 3221224528 3221223696 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74307 64752 603 41 0 74266 0
vsize: 297228
[startup+620.021 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73193 0 0 0 61832 174 0 0 25 0 1 0 542636652 304361472 64760 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74307 64760 603 41 0 74266 0
vsize: 297228
[startup+630.021 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73194 0 0 0 62833 174 0 0 25 0 1 0 542636652 304361472 64761 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74307 64761 603 41 0 74266 0
vsize: 297228
[startup+640.021 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73222 0 0 0 63833 174 0 0 25 0 1 0 542636652 304496640 64789 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74340 64789 603 41 0 74299 0
vsize: 297360
[startup+650.02 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73251 0 0 0 64833 175 0 0 25 0 1 0 542636652 304631808 64818 4294967295 134512640 134672761 3221224528 3221223632 134560355 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74373 64818 603 41 0 74332 0
vsize: 297492
[startup+660.021 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73290 0 0 0 65833 175 0 0 25 0 1 0 542636652 304766976 64857 4294967295 134512640 134672761 3221224528 3221223696 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74406 64857 603 41 0 74365 0
vsize: 297624
[startup+670.021 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73365 0 0 0 66832 175 0 0 25 0 1 0 542636652 304922624 64919 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74444 64919 603 41 0 74403 0
vsize: 297776
[startup+680.021 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73367 0 0 0 67832 175 0 0 25 0 1 0 542636652 305057792 64921 4294967295 134512640 134672761 3221224528 3221223632 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74477 64921 603 41 0 74436 0
vsize: 297908
[startup+690.021 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73396 0 0 0 68833 175 0 0 25 0 1 0 542636652 305057792 64950 4294967295 134512640 134672761 3221224528 3221223744 134561999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74477 64950 603 41 0 74436 0
vsize: 297908
[startup+700.021 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73416 0 0 0 69833 175 0 0 25 0 1 0 542636652 305192960 64970 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74510 64970 603 41 0 74469 0
vsize: 298040
[startup+710.022 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73426 0 0 0 70833 175 0 0 25 0 1 0 542636652 305192960 64980 4294967295 134512640 134672761 3221224528 3221223736 134561962 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74510 64980 603 41 0 74469 0
vsize: 298040
[startup+720.022 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73429 0 0 0 71832 176 0 0 25 0 1 0 542636652 305192960 64983 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74510 64983 603 41 0 74469 0
vsize: 298040
[startup+730.021 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73452 0 0 0 72832 176 0 0 25 0 1 0 542636652 305328128 65006 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74543 65006 603 41 0 74502 0
vsize: 298172
[startup+740.021 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73463 0 0 0 73832 176 0 0 25 0 1 0 542636652 305328128 65017 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74543 65017 603 41 0 74502 0
vsize: 298172
[startup+750.021 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73473 0 0 0 74832 176 0 0 25 0 1 0 542636652 305463296 65027 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74576 65027 603 41 0 74535 0
vsize: 298304
[startup+760.022 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73506 0 0 0 75832 176 0 0 25 0 1 0 542636652 305598464 65060 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74609 65060 603 41 0 74568 0
vsize: 298436
[startup+770.023 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73515 0 0 0 76833 176 0 0 25 0 1 0 542636652 305598464 65069 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74609 65069 603 41 0 74568 0
vsize: 298436
[startup+780.022 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73543 0 0 0 77833 177 0 0 25 0 1 0 542636652 305733632 65097 4294967295 134512640 134672761 3221224528 3221223632 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74642 65097 603 41 0 74601 0
vsize: 298568
[startup+790.022 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73558 0 0 0 78833 177 0 0 25 0 1 0 542636652 305733632 65112 4294967295 134512640 134672761 3221224528 3221223664 134560634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74642 65112 603 41 0 74601 0
vsize: 298568
[startup+800.022 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73564 0 0 0 79833 177 0 0 25 0 1 0 542636652 305733632 65118 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74642 65118 603 41 0 74601 0
vsize: 298568
[startup+810.023 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73571 0 0 0 80833 177 0 0 25 0 1 0 542636652 305868800 65125 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74675 65125 603 41 0 74634 0
vsize: 298700
[startup+820.023 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73599 0 0 0 81833 177 0 0 25 0 1 0 542636652 305868800 65153 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74675 65153 603 41 0 74634 0
vsize: 298700
[startup+830.023 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73622 0 0 0 82833 177 0 0 25 0 1 0 542636652 306003968 65176 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74708 65176 603 41 0 74667 0
vsize: 298832
[startup+840.023 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73647 0 0 0 83833 177 0 0 25 0 1 0 542636652 306139136 65201 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74741 65201 603 41 0 74700 0
vsize: 298964
[startup+850.023 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73681 0 0 0 84833 178 0 0 25 0 1 0 542636652 306274304 65235 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74774 65235 603 41 0 74733 0
vsize: 299096
[startup+860.024 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73694 0 0 0 85833 178 0 0 25 0 1 0 542636652 306274304 65248 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74774 65248 603 41 0 74733 0
vsize: 299096
[startup+870.024 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73707 0 0 0 86833 178 0 0 25 0 1 0 542636652 306409472 65261 4294967295 134512640 134672761 3221224528 3221223696 134561372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74807 65261 603 41 0 74766 0
vsize: 299228
[startup+880.025 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73725 0 0 0 87833 178 0 0 25 0 1 0 542636652 306409472 65279 4294967295 134512640 134672761 3221224528 3221223696 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74807 65279 603 41 0 74766 0
vsize: 299228
[startup+890.025 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73751 0 0 0 88833 178 0 0 25 0 1 0 542636652 306544640 65305 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74840 65305 603 41 0 74799 0
vsize: 299360
[startup+900.026 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73786 0 0 0 89834 178 0 0 25 0 1 0 542636652 306679808 65340 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74873 65340 603 41 0 74832 0
vsize: 299492
[startup+910.027 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73830 0 0 0 90834 178 0 0 25 0 1 0 542636652 306814976 65384 4294967295 134512640 134672761 3221224528 3221223712 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74906 65384 603 41 0 74865 0
vsize: 299624
[startup+920.027 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73865 0 0 0 91834 178 0 0 25 0 1 0 542636652 306950144 65419 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74939 65419 603 41 0 74898 0
vsize: 299756
[startup+930.027 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73890 0 0 0 92834 178 0 0 25 0 1 0 542636652 307085312 65444 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74972 65444 603 41 0 74931 0
vsize: 299888
[startup+940.027 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73916 0 0 0 93834 178 0 0 25 0 1 0 542636652 307220480 65470 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75005 65470 603 41 0 74964 0
vsize: 300020
[startup+950.027 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73951 0 0 0 94834 178 0 0 25 0 1 0 542636652 307351552 65505 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75037 65505 603 41 0 74996 0
vsize: 300148
[startup+960.027 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 73992 0 0 0 95834 178 0 0 25 0 1 0 542636652 307486720 65546 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75070 65546 603 41 0 75029 0
vsize: 300280
[startup+970.026 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 74034 0 0 0 96834 178 0 0 25 0 1 0 542636652 307621888 65588 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75103 65588 603 41 0 75062 0
vsize: 300412
[startup+980.026 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 74075 0 0 0 97834 179 0 0 25 0 1 0 542636652 307892224 65629 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75169 65629 603 41 0 75128 0
vsize: 300676
[startup+990.027 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 74107 0 0 0 98834 179 0 0 25 0 1 0 542636652 308027392 65661 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75202 65661 603 41 0 75161 0
vsize: 300808
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 74145 0 0 0 99834 179 0 0 25 0 1 0 542636652 308162560 65699 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75235 65699 603 41 0 75194 0
vsize: 300940
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 74166 0 0 0 100835 179 0 0 25 0 1 0 542636652 308162560 65720 4294967295 134512640 134672761 3221224528 3221223696 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75235 65720 603 41 0 75194 0
vsize: 300940
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 74167 0 0 0 101835 179 0 0 25 0 1 0 542636652 308162560 65721 4294967295 134512640 134672761 3221224528 3221223736 134561960 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75235 65721 603 41 0 75194 0
vsize: 300940
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 74169 0 0 0 102835 179 0 0 25 0 1 0 542636652 308297728 65723 4294967295 134512640 134672761 3221224528 3221223700 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75268 65723 603 41 0 75227 0
vsize: 301072
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 74169 0 0 0 103835 179 0 0 25 0 1 0 542636652 308297728 65723 4294967295 134512640 134672761 3221224528 3221223732 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75268 65723 603 41 0 75227 0
vsize: 301072
[startup+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 74189 0 0 0 104835 179 0 0 25 0 1 0 542636652 308297728 65743 4294967295 134512640 134672761 3221224528 3221223696 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75268 65743 603 41 0 75227 0
vsize: 301072
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 74208 0 0 0 105835 179 0 0 25 0 1 0 542636652 308436992 65762 4294967295 134512640 134672761 3221224528 3221223632 134560399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75302 65762 603 41 0 75261 0
vsize: 301208
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 74263 0 0 0 106835 180 0 0 25 0 1 0 542636652 308572160 65817 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75335 65817 603 41 0 75294 0
vsize: 301340
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 74269 0 0 0 107835 180 0 0 25 0 1 0 542636652 308572160 65823 4294967295 134512640 134672761 3221224528 3221223700 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75335 65823 603 41 0 75294 0
vsize: 301340
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 74269 0 0 0 108835 180 0 0 25 0 1 0 542636652 308572160 65823 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75335 65823 603 41 0 75294 0
vsize: 301340
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 22854
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 74307 0 0 0 109836 180 0 0 25 0 1 0 542636652 308969472 65861 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75432 65861 603 41 0 75391 0
vsize: 301728
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 22855
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 74307 0 0 0 110836 180 0 0 25 0 1 0 542636652 308969472 65861 4294967295 134512640 134672761 3221224528 3221223700 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75432 65861 603 41 0 75391 0
vsize: 301728
[startup+1120.21 s]
Raw data (loadavg): 1.08 1.02 0.99 3/56 22901
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 74307 0 0 0 111853 180 0 0 25 0 1 0 542636652 308969472 65861 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75432 65861 603 41 0 75391 0
vsize: 301728
[startup+1130.21 s]
Raw data (loadavg): 1.14 1.03 1.00 2/54 22907
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 74311 0 0 0 112853 180 0 0 25 0 1 0 542636652 308969472 65865 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75432 65865 603 41 0 75391 0
vsize: 301728
[startup+1140.21 s]
Raw data (loadavg): 1.12 1.03 1.00 2/54 22907
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 74325 0 0 0 113853 180 0 0 25 0 1 0 542636652 308969472 65879 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75432 65879 603 41 0 75391 0
vsize: 301728
[startup+1150.21 s]
Raw data (loadavg): 1.10 1.03 1.00 2/54 22907
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 74351 0 0 0 114853 180 0 0 25 0 1 0 542636652 309104640 65905 4294967295 134512640 134672761 3221224528 3221223632 134559946 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75465 65905 603 41 0 75424 0
vsize: 301860
[startup+1160.21 s]
Raw data (loadavg): 1.08 1.03 1.00 2/54 22907
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 74367 0 0 0 115853 180 0 0 25 0 1 0 542636652 309104640 65921 4294967295 134512640 134672761 3221224528 3221223700 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75465 65921 603 41 0 75424 0
vsize: 301860
[startup+1170.21 s]
Raw data (loadavg): 1.07 1.03 1.00 2/54 22907
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 74380 0 0 0 116854 180 0 0 25 0 1 0 542636652 309239808 65934 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75498 65934 603 41 0 75457 0
vsize: 301992
[startup+1180.21 s]
Raw data (loadavg): 1.06 1.03 1.00 2/54 22907
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 74386 0 0 0 117853 181 0 0 25 0 1 0 542636652 309239808 65940 4294967295 134512640 134672761 3221224528 3221223700 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75498 65940 603 41 0 75457 0
vsize: 301992
[startup+1190.21 s]
Raw data (loadavg): 1.05 1.02 1.00 2/54 22909
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 74409 0 0 0 118854 181 0 0 25 0 1 0 542636652 309374976 65963 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75531 65963 603 41 0 75490 0
vsize: 302124
[startup+1200.21 s]
Raw data (loadavg): 1.04 1.02 1.00 2/54 22909
Raw data (stat): 22854 (minisat+) R 22853 27222 27221 0 -1 0 74426 0 0 0 119854 181 0 0 25 0 1 0 542636652 309374976 65980 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75531 65980 603 41 0 75490 0
vsize: 302124
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.35 s]
Raw data (loadavg): 1.04 1.02 1.00 1/54 22909
Raw data (stat): 22854 (minisat+) Z 22853 27222 27221 0 -1 12 74429 0 0 0 119854 194 0 0 25 0 1 0 542636652 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.34
CPU time (s): 1200.49
CPU user time (s): 1198.55
CPU system time (s): 1.9407
CPU usage (%): 100.012
Max. virtual memory (Kb): 302124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####