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 22316

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        317344 kB
Buffers:         30244 kB
Cached:         665260 kB
SwapCached:          0 kB
Active:         182088 kB
Inactive:       516316 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        317092 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6952 kB
Slab:            13408 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 03:08:12 (client local time) WITH STATUS 10 IN 1200.33 SECONDS
stats: 11764 7 1200.33 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): 0.88 0.91 0.95 2/54 12558
Raw data (stat): 12558 (runsolver) R 12557 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478453763 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99958 s]
Raw data (loadavg): 0.90 0.91 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 7101 0 0 0 983 15 0 0 25 0 1 0 478453763 20447232 4555 4294967295 134512640 134672761 3221224528 3221209280 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4992 4555 603 41 0 4951 0
vsize: 19968
[startup+20.0008 s]
Raw data (loadavg): 0.91 0.91 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 13236 0 0 0 1971 27 0 0 25 0 1 0 478453763 31326208 7136 4294967295 134512640 134672761 3221224528 3221208128 134594214 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.0017 s]
Raw data (loadavg): 0.93 0.92 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 53189 0 0 0 2877 122 0 0 25 0 1 0 478453763 197087232 46087 4294967295 134512640 134672761 3221224528 3221205264 134541828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48117 46087 603 41 0 48076 0
vsize: 192468
[startup+40.0019 s]
Raw data (loadavg): 0.94 0.92 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 53891 0 0 0 3875 123 0 0 25 0 1 0 478453763 198979584 46789 4294967295 134512640 134672761 3221224528 3221223700 134556596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48579 46789 603 41 0 48538 0
vsize: 194316
[startup+50.0031 s]
Raw data (loadavg): 0.95 0.92 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 54037 0 0 0 4875 124 0 0 25 0 1 0 478453763 198979584 46935 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48579 46935 603 41 0 48538 0
vsize: 194316
[startup+60.003 s]
Raw data (loadavg): 0.96 0.92 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 54046 0 0 0 5875 124 0 0 25 0 1 0 478453763 198979584 46944 4294967295 134512640 134672761 3221224528 3221223728 134557919 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.0033 s]
Raw data (loadavg): 0.96 0.92 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 54097 0 0 0 6874 125 0 0 25 0 1 0 478453763 199311360 46995 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48660 46995 603 41 0 48619 0
vsize: 194640
[startup+80.0035 s]
Raw data (loadavg): 0.97 0.93 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 54105 0 0 0 7874 125 0 0 25 0 1 0 478453763 199311360 47003 4294967295 134512640 134672761 3221224528 3221223732 134561964 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.0043 s]
Raw data (loadavg): 0.97 0.93 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 54105 0 0 0 8874 125 0 0 25 0 1 0 478453763 199311360 47003 4294967295 134512640 134672761 3221224528 3221223664 134560677 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.005 s]
Raw data (loadavg): 0.98 0.93 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 54194 0 0 0 9874 125 0 0 25 0 1 0 478453763 199311360 47092 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48660 47092 603 41 0 48619 0
vsize: 194640
[startup+110.005 s]
Raw data (loadavg): 0.98 0.93 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 54222 0 0 0 10874 125 0 0 25 0 1 0 478453763 199446528 47120 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48693 47120 603 41 0 48652 0
vsize: 194772
[startup+120.006 s]
Raw data (loadavg): 0.98 0.93 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 54270 0 0 0 11874 126 0 0 25 0 1 0 478453763 199577600 47168 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48725 47168 603 41 0 48684 0
vsize: 194900
[startup+130.005 s]
Raw data (loadavg): 0.98 0.94 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 54315 0 0 0 12874 126 0 0 25 0 1 0 478453763 199712768 47213 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48758 47213 603 41 0 48717 0
vsize: 195032
[startup+140.006 s]
Raw data (loadavg): 0.99 0.94 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 54390 0 0 0 13874 126 0 0 25 0 1 0 478453763 200110080 47288 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48855 47288 603 41 0 48814 0
vsize: 195420
[startup+150.007 s]
Raw data (loadavg): 0.99 0.94 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 54390 0 0 0 14875 126 0 0 25 0 1 0 478453763 200110080 47288 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48855 47288 603 41 0 48814 0
vsize: 195420
[startup+160.006 s]
Raw data (loadavg): 0.99 0.94 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 54390 0 0 0 15875 126 0 0 25 0 1 0 478453763 200110080 47288 4294967295 134512640 134672761 3221224528 3221223632 134560287 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48855 47288 603 41 0 48814 0
vsize: 195420
[startup+170.006 s]
Raw data (loadavg): 0.99 0.94 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 54390 0 0 0 16875 126 0 0 25 0 1 0 478453763 200110080 47288 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48855 47288 603 41 0 48814 0
vsize: 195420
[startup+180.006 s]
Raw data (loadavg): 0.99 0.94 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 54400 0 0 0 17875 126 0 0 25 0 1 0 478453763 200110080 47298 4294967295 134512640 134672761 3221224528 3221223696 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48855 47298 603 41 0 48814 0
vsize: 195420
[startup+190.007 s]
Raw data (loadavg): 0.99 0.94 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 54412 0 0 0 18875 126 0 0 25 0 1 0 478453763 200245248 47310 4294967295 134512640 134672761 3221224528 3221223632 134560207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48888 47310 603 41 0 48847 0
vsize: 195552
[startup+200.006 s]
Raw data (loadavg): 0.99 0.95 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 54424 0 0 0 19875 126 0 0 25 0 1 0 478453763 200245248 47322 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48888 47322 603 41 0 48847 0
vsize: 195552
[startup+210.006 s]
Raw data (loadavg): 1.07 0.96 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 54448 0 0 0 20876 126 0 0 25 0 1 0 478453763 200380416 47346 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48921 47346 603 41 0 48880 0
vsize: 195684
[startup+220.007 s]
Raw data (loadavg): 1.06 0.96 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 54472 0 0 0 21876 126 0 0 25 0 1 0 478453763 200515584 47370 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48954 47370 603 41 0 48913 0
vsize: 195816
[startup+230.007 s]
Raw data (loadavg): 1.05 0.97 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 54493 0 0 0 22876 126 0 0 25 0 1 0 478453763 200515584 47391 4294967295 134512640 134672761 3221224528 3221223700 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48954 47391 603 41 0 48913 0
vsize: 195816
[startup+240.008 s]
Raw data (loadavg): 1.04 0.97 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 54495 0 0 0 23876 126 0 0 25 0 1 0 478453763 200515584 47393 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48954 47393 603 41 0 48913 0
vsize: 195816
[startup+250.007 s]
Raw data (loadavg): 1.04 0.97 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 54517 0 0 0 24876 126 0 0 25 0 1 0 478453763 200650752 47415 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48987 47415 603 41 0 48946 0
vsize: 195948
[startup+260.007 s]
Raw data (loadavg): 1.03 0.97 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 54565 0 0 0 25876 126 0 0 25 0 1 0 478453763 200785920 47463 4294967295 134512640 134672761 3221224528 3221223696 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49020 47463 603 41 0 48979 0
vsize: 196080
[startup+270.007 s]
Raw data (loadavg): 1.03 0.97 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 54621 0 0 0 26876 126 0 0 25 0 1 0 478453763 201056256 47519 4294967295 134512640 134672761 3221224528 3221223696 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49086 47519 603 41 0 49045 0
vsize: 196344
[startup+280.007 s]
Raw data (loadavg): 1.02 0.97 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 54647 0 0 0 27876 126 0 0 25 0 1 0 478453763 201191424 47545 4294967295 134512640 134672761 3221224528 3221223700 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49119 47545 603 41 0 49078 0
vsize: 196476
[startup+290.007 s]
Raw data (loadavg): 1.02 0.97 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 54658 0 0 0 28876 126 0 0 25 0 1 0 478453763 201191424 47556 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49119 47556 603 41 0 49078 0
vsize: 196476
[startup+300.007 s]
Raw data (loadavg): 1.01 0.97 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 60340 0 0 0 29862 141 0 0 25 0 1 0 478453763 224075776 51920 4294967295 134512640 134672761 3221224528 3221170848 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54706 51921 603 41 0 54665 0
vsize: 218824
[startup+310.007 s]
Raw data (loadavg): 1.01 0.97 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 72580 0 0 0 30831 172 0 0 25 0 1 0 478453763 301760512 64147 4294967295 134512640 134672761 3221224528 3221223728 134557887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73672 64147 603 41 0 73631 0
vsize: 294688
[startup+320.007 s]
Raw data (loadavg): 1.01 0.97 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 72583 0 0 0 31831 172 0 0 25 0 1 0 478453763 301760512 64150 4294967295 134512640 134672761 3221224528 3221223744 134561979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73672 64150 603 41 0 73631 0
vsize: 294688
[startup+330.006 s]
Raw data (loadavg): 1.01 0.97 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 72614 0 0 0 32831 173 0 0 25 0 1 0 478453763 301953024 64181 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73719 64181 603 41 0 73678 0
vsize: 294876
[startup+340.006 s]
Raw data (loadavg): 1.01 0.97 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 72615 0 0 0 33831 173 0 0 25 0 1 0 478453763 301953024 64182 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73719 64182 603 41 0 73678 0
vsize: 294876
[startup+350.006 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 72629 0 0 0 34831 173 0 0 25 0 1 0 478453763 301953024 64196 4294967295 134512640 134672761 3221224528 3221223632 134560051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73719 64196 603 41 0 73678 0
vsize: 294876
[startup+360.006 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 72646 0 0 0 35831 173 0 0 25 0 1 0 478453763 302084096 64213 4294967295 134512640 134672761 3221224528 3221223632 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73751 64213 603 41 0 73710 0
vsize: 295004
[startup+370.007 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 72658 0 0 0 36831 173 0 0 25 0 1 0 478453763 302084096 64225 4294967295 134512640 134672761 3221224528 3221223700 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73751 64225 603 41 0 73710 0
vsize: 295004
[startup+380.006 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 72676 0 0 0 37831 173 0 0 25 0 1 0 478453763 302219264 64243 4294967295 134512640 134672761 3221224528 3221223664 134560703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73784 64243 603 41 0 73743 0
vsize: 295136
[startup+390.007 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 72699 0 0 0 38832 173 0 0 25 0 1 0 478453763 302354432 64266 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73817 64266 603 41 0 73776 0
vsize: 295268
[startup+400.007 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 72711 0 0 0 39832 173 0 0 25 0 1 0 478453763 302354432 64278 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73817 64278 603 41 0 73776 0
vsize: 295268
[startup+410.007 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 72731 0 0 0 40832 173 0 0 25 0 1 0 478453763 302354432 64298 4294967295 134512640 134672761 3221224528 3221223664 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73817 64298 603 41 0 73776 0
vsize: 295268
[startup+420.008 s]
Raw data (loadavg): 1.08 0.99 0.96 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 72740 0 0 0 41832 173 0 0 25 0 1 0 478453763 302489600 64307 4294967295 134512640 134672761 3221224528 3221223700 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73850 64307 603 41 0 73809 0
vsize: 295400
[startup+430.007 s]
Raw data (loadavg): 1.14 1.00 0.96 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 72740 0 0 0 42832 173 0 0 25 0 1 0 478453763 302489600 64307 4294967295 134512640 134672761 3221224528 3221223700 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73850 64307 603 41 0 73809 0
vsize: 295400
[startup+440.008 s]
Raw data (loadavg): 1.12 1.00 0.96 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 72750 0 0 0 43832 173 0 0 25 0 1 0 478453763 302489600 64317 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73850 64317 603 41 0 73809 0
vsize: 295400
[startup+450.008 s]
Raw data (loadavg): 1.10 1.00 0.96 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 72768 0 0 0 44833 173 0 0 25 0 1 0 478453763 302624768 64335 4294967295 134512640 134672761 3221224528 3221223632 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73883 64335 603 41 0 73842 0
vsize: 295532
[startup+460.008 s]
Raw data (loadavg): 1.08 1.00 0.96 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 72775 0 0 0 45833 173 0 0 25 0 1 0 478453763 302624768 64342 4294967295 134512640 134672761 3221224528 3221223632 134560287 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73883 64342 603 41 0 73842 0
vsize: 295532
[startup+470.007 s]
Raw data (loadavg): 1.07 1.00 0.96 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 72788 0 0 0 46833 173 0 0 25 0 1 0 478453763 302624768 64355 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73883 64355 603 41 0 73842 0
vsize: 295532
[startup+480.007 s]
Raw data (loadavg): 1.06 1.00 0.96 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 72816 0 0 0 47833 173 0 0 25 0 1 0 478453763 302759936 64383 4294967295 134512640 134672761 3221224528 3221223696 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73916 64383 603 41 0 73875 0
vsize: 295664
[startup+490.008 s]
Raw data (loadavg): 1.05 1.00 0.96 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 72845 0 0 0 48833 173 0 0 25 0 1 0 478453763 302895104 64412 4294967295 134512640 134672761 3221224528 3221223696 134561372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73949 64412 603 41 0 73908 0
vsize: 295796
[startup+500.008 s]
Raw data (loadavg): 1.04 1.00 0.96 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 72879 0 0 0 49833 174 0 0 25 0 1 0 478453763 303030272 64446 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73982 64446 603 41 0 73941 0
vsize: 295928
[startup+510.007 s]
Raw data (loadavg): 1.04 1.00 0.96 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 72924 0 0 0 50833 174 0 0 25 0 1 0 478453763 303165440 64491 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74015 64491 603 41 0 73974 0
vsize: 296060
[startup+520.008 s]
Raw data (loadavg): 1.03 1.00 0.96 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 72961 0 0 0 51833 174 0 0 25 0 1 0 478453763 303300608 64528 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74048 64528 603 41 0 74007 0
vsize: 296192
[startup+530.008 s]
Raw data (loadavg): 1.02 1.00 0.96 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 72997 0 0 0 52833 174 0 0 25 0 1 0 478453763 303431680 64564 4294967295 134512640 134672761 3221224528 3221223696 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74080 64564 603 41 0 74039 0
vsize: 296320
[startup+540.009 s]
Raw data (loadavg): 1.02 1.00 0.96 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73019 0 0 0 53832 174 0 0 25 0 1 0 478453763 303566848 64586 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74113 64586 603 41 0 74072 0
vsize: 296452
[startup+550.01 s]
Raw data (loadavg): 1.02 1.00 0.96 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73042 0 0 0 54833 174 0 0 25 0 1 0 478453763 303697920 64609 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74145 64609 603 41 0 74104 0
vsize: 296580
[startup+560.009 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73075 0 0 0 55833 174 0 0 25 0 1 0 478453763 303828992 64642 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74177 64642 603 41 0 74136 0
vsize: 296708
[startup+570.009 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73099 0 0 0 56833 175 0 0 25 0 1 0 478453763 303964160 64666 4294967295 134512640 134672761 3221224528 3221223696 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74210 64666 603 41 0 74169 0
vsize: 296840
[startup+580.009 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73126 0 0 0 57833 175 0 0 25 0 1 0 478453763 303964160 64693 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74210 64693 603 41 0 74169 0
vsize: 296840
[startup+590.01 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73156 0 0 0 58833 175 0 0 25 0 1 0 478453763 304226304 64723 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74274 64723 603 41 0 74233 0
vsize: 297096
[startup+600.01 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73182 0 0 0 59833 175 0 0 25 0 1 0 478453763 304361472 64749 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74307 64749 603 41 0 74266 0
vsize: 297228
[startup+610.009 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73185 0 0 0 60833 175 0 0 25 0 1 0 478453763 304361472 64752 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74307 64752 603 41 0 74266 0
vsize: 297228
[startup+620.009 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73193 0 0 0 61833 175 0 0 25 0 1 0 478453763 304361472 64760 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74307 64760 603 41 0 74266 0
vsize: 297228
[startup+630.009 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73194 0 0 0 62833 175 0 0 25 0 1 0 478453763 304361472 64761 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74307 64761 603 41 0 74266 0
vsize: 297228
[startup+640.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73222 0 0 0 63833 175 0 0 25 0 1 0 478453763 304496640 64789 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74340 64789 603 41 0 74299 0
vsize: 297360
[startup+650.009 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73251 0 0 0 64833 175 0 0 25 0 1 0 478453763 304631808 64818 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74373 64818 603 41 0 74332 0
vsize: 297492
[startup+660.01 s]
Raw data (loadavg): 1.00 1.00 0.96 3/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73289 0 0 0 65833 175 0 0 25 0 1 0 478453763 304766976 64856 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74406 64856 603 41 0 74365 0
vsize: 297624
[startup+670.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73365 0 0 0 66834 175 0 0 25 0 1 0 478453763 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.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73367 0 0 0 67833 176 0 0 25 0 1 0 478453763 305057792 64921 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74477 64921 603 41 0 74436 0
vsize: 297908
[startup+690.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73396 0 0 0 68833 176 0 0 25 0 1 0 478453763 305057792 64950 4294967295 134512640 134672761 3221224528 3221223700 134556658 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74477 64950 603 41 0 74436 0
vsize: 297908
[startup+700.011 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73415 0 0 0 69833 176 0 0 25 0 1 0 478453763 305192960 64969 4294967295 134512640 134672761 3221224528 3221223676 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74510 64969 603 41 0 74469 0
vsize: 298040
[startup+710.011 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12558
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73426 0 0 0 70833 176 0 0 25 0 1 0 478453763 305192960 64980 4294967295 134512640 134672761 3221224528 3221223700 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74510 64980 603 41 0 74469 0
vsize: 298040
[startup+720.011 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12611
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73429 0 0 0 71833 176 0 0 25 0 1 0 478453763 305192960 64983 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74510 64983 603 41 0 74469 0
vsize: 298040
[startup+730.012 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12611
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73452 0 0 0 72833 177 0 0 25 0 1 0 478453763 305328128 65006 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74543 65006 603 41 0 74502 0
vsize: 298172
[startup+740.013 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12611
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73463 0 0 0 73833 177 0 0 25 0 1 0 478453763 305328128 65017 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74543 65017 603 41 0 74502 0
vsize: 298172
[startup+750.012 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12611
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73473 0 0 0 74833 177 0 0 25 0 1 0 478453763 305463296 65027 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74576 65027 603 41 0 74535 0
vsize: 298304
[startup+760.012 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12611
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73506 0 0 0 75832 178 0 0 25 0 1 0 478453763 305598464 65060 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74609 65060 603 41 0 74568 0
vsize: 298436
[startup+770.013 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12611
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73515 0 0 0 76833 178 0 0 25 0 1 0 478453763 305598464 65069 4294967295 134512640 134672761 3221224528 3221223664 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74609 65069 603 41 0 74568 0
vsize: 298436
[startup+780.013 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12611
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73543 0 0 0 77832 178 0 0 25 0 1 0 478453763 305733632 65097 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74642 65097 603 41 0 74601 0
vsize: 298568
[startup+790.014 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12613
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73558 0 0 0 78832 178 0 0 25 0 1 0 478453763 305733632 65112 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74642 65112 603 41 0 74601 0
vsize: 298568
[startup+800.014 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12613
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73564 0 0 0 79832 178 0 0 25 0 1 0 478453763 305733632 65118 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74642 65118 603 41 0 74601 0
vsize: 298568
[startup+810.014 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12613
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73571 0 0 0 80832 179 0 0 25 0 1 0 478453763 305868800 65125 4294967295 134512640 134672761 3221224528 3221223696 134560845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74675 65125 603 41 0 74634 0
vsize: 298700
[startup+820.014 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12613
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73599 0 0 0 81832 179 0 0 25 0 1 0 478453763 305868800 65153 4294967295 134512640 134672761 3221224528 3221223664 134560611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74675 65153 603 41 0 74634 0
vsize: 298700
[startup+830.014 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12613
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73622 0 0 0 82832 179 0 0 25 0 1 0 478453763 306003968 65176 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74708 65176 603 41 0 74667 0
vsize: 298832
[startup+840.014 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12613
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73646 0 0 0 83832 180 0 0 25 0 1 0 478453763 306139136 65200 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74741 65200 603 41 0 74700 0
vsize: 298964
[startup+850.015 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12613
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73681 0 0 0 84832 180 0 0 25 0 1 0 478453763 306274304 65235 4294967295 134512640 134672761 3221224528 3221223696 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74774 65235 603 41 0 74733 0
vsize: 299096
[startup+860.015 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12613
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73694 0 0 0 85832 180 0 0 25 0 1 0 478453763 306274304 65248 4294967295 134512640 134672761 3221224528 3221223792 134562492 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74774 65248 603 41 0 74733 0
vsize: 299096
[startup+870.015 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12613
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73707 0 0 0 86832 180 0 0 25 0 1 0 478453763 306409472 65261 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74807 65261 603 41 0 74766 0
vsize: 299228
[startup+880.016 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12613
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73725 0 0 0 87832 180 0 0 25 0 1 0 478453763 306409472 65279 4294967295 134512640 134672761 3221224528 3221223696 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74807 65279 603 41 0 74766 0
vsize: 299228
[startup+890.016 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12613
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73751 0 0 0 88832 181 0 0 25 0 1 0 478453763 306544640 65305 4294967295 134512640 134672761 3221224528 3221223696 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74840 65305 603 41 0 74799 0
vsize: 299360
[startup+900.017 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12613
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73785 0 0 0 89831 181 0 0 25 0 1 0 478453763 306679808 65339 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74873 65339 603 41 0 74832 0
vsize: 299492
[startup+910.018 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12613
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73828 0 0 0 90832 181 0 0 25 0 1 0 478453763 306814976 65382 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74906 65382 603 41 0 74865 0
vsize: 299624
[startup+920.019 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12613
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73865 0 0 0 91831 182 0 0 25 0 1 0 478453763 306950144 65419 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74939 65419 603 41 0 74898 0
vsize: 299756
[startup+930.018 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12613
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73890 0 0 0 92831 182 0 0 25 0 1 0 478453763 307085312 65444 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74972 65444 603 41 0 74931 0
vsize: 299888
[startup+940.019 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12613
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73916 0 0 0 93831 182 0 0 25 0 1 0 478453763 307220480 65470 4294967295 134512640 134672761 3221224528 3221223696 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75005 65470 603 41 0 74964 0
vsize: 300020
[startup+950.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12613
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73950 0 0 0 94831 182 0 0 25 0 1 0 478453763 307351552 65504 4294967295 134512640 134672761 3221224528 3221223632 134560318 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75037 65504 603 41 0 74996 0
vsize: 300148
[startup+960.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12613
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 73991 0 0 0 95831 183 0 0 25 0 1 0 478453763 307486720 65545 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75070 65545 603 41 0 75029 0
vsize: 300280
[startup+970.021 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12613
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 74033 0 0 0 96831 183 0 0 25 0 1 0 478453763 307621888 65587 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75103 65587 603 41 0 75062 0
vsize: 300412
[startup+980.021 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12613
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 74074 0 0 0 97831 183 0 0 25 0 1 0 478453763 307892224 65628 4294967295 134512640 134672761 3221224528 3221223696 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75169 65628 603 41 0 75128 0
vsize: 300676
[startup+990.022 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12613
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 74105 0 0 0 98832 183 0 0 25 0 1 0 478453763 308027392 65659 4294967295 134512640 134672761 3221224528 3221223696 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75202 65659 603 41 0 75161 0
vsize: 300808
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12613
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 74144 0 0 0 99832 183 0 0 25 0 1 0 478453763 308162560 65698 4294967295 134512640 134672761 3221224528 3221223696 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75235 65698 603 41 0 75194 0
vsize: 300940
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12613
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 74166 0 0 0 100832 183 0 0 25 0 1 0 478453763 308162560 65720 4294967295 134512640 134672761 3221224528 3221223700 134556598 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.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12615
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 74167 0 0 0 101832 183 0 0 25 0 1 0 478453763 308162560 65721 4294967295 134512640 134672761 3221224528 3221223700 134556634 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.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12615
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 74169 0 0 0 102832 183 0 0 25 0 1 0 478453763 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.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12615
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 74169 0 0 0 103833 183 0 0 25 0 1 0 478453763 308297728 65723 4294967295 134512640 134672761 3221224528 3221223700 134556598 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.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12615
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 74187 0 0 0 104833 183 0 0 25 0 1 0 478453763 308297728 65741 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75268 65741 603 41 0 75227 0
vsize: 301072
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12615
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 74207 0 0 0 105833 183 0 0 25 0 1 0 478453763 308436992 65761 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75302 65761 603 41 0 75261 0
vsize: 301208
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12615
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 74257 0 0 0 106833 183 0 0 25 0 1 0 478453763 308572160 65811 4294967295 134512640 134672761 3221224528 3221223680 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75335 65811 603 41 0 75294 0
vsize: 301340
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12615
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 74268 0 0 0 107833 183 0 0 25 0 1 0 478453763 308572160 65822 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75335 65822 603 41 0 75294 0
vsize: 301340
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12615
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 74269 0 0 0 108833 183 0 0 25 0 1 0 478453763 308572160 65823 4294967295 134512640 134672761 3221224528 3221223696 134560898 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.96 2/54 12615
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 74307 0 0 0 109834 183 0 0 25 0 1 0 478453763 308969472 65861 4294967295 134512640 134672761 3221224528 3221223696 134561193 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.96 2/54 12615
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 74307 0 0 0 110834 183 0 0 25 0 1 0 478453763 308969472 65861 4294967295 134512640 134672761 3221224528 3221223696 134561205 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.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12615
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 74307 0 0 0 111834 183 0 0 25 0 1 0 478453763 308969472 65861 4294967295 134512640 134672761 3221224528 3221223664 134560588 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.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12615
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 74308 0 0 0 112834 183 0 0 25 0 1 0 478453763 308969472 65862 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75432 65862 603 41 0 75391 0
vsize: 301728
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12615
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 74324 0 0 0 113834 183 0 0 25 0 1 0 478453763 308969472 65878 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75432 65878 603 41 0 75391 0
vsize: 301728
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12615
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 74346 0 0 0 114835 183 0 0 25 0 1 0 478453763 309104640 65900 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75465 65900 603 41 0 75424 0
vsize: 301860
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12615
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 74363 0 0 0 115835 183 0 0 25 0 1 0 478453763 309104640 65917 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75465 65917 603 41 0 75424 0
vsize: 301860
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12615
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 74378 0 0 0 116835 183 0 0 25 0 1 0 478453763 309239808 65932 4294967295 134512640 134672761 3221224528 3221223664 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75498 65932 603 41 0 75457 0
vsize: 301992
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12615
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 74386 0 0 0 117835 183 0 0 25 0 1 0 478453763 309239808 65940 4294967295 134512640 134672761 3221224528 3221223728 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75498 65940 603 41 0 75457 0
vsize: 301992
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12615
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 74403 0 0 0 118835 184 0 0 25 0 1 0 478453763 309239808 65957 4294967295 134512640 134672761 3221224528 3221223664 134560585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75498 65957 603 41 0 75457 0
vsize: 301992
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 12615
Raw data (stat): 12558 (minisat+) R 12557 26667 26666 0 -1 0 74421 0 0 0 119835 184 0 0 25 0 1 0 478453763 309374976 65975 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75531 65975 603 41 0 75490 0
vsize: 302124
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.17 s]
Raw data (loadavg): 1.00 1.00 0.96 1/54 12615
Raw data (stat): 12558 (minisat+) Z 12557 26667 26666 0 -1 12 74424 0 0 0 119835 197 0 0 25 0 1 0 478453763 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.17
CPU time (s): 1200.33
CPU user time (s): 1198.35
CPU system time (s): 1.9727
CPU usage (%): 100.013
Max. virtual memory (Kb): 302124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####