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 15776

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        557500 kB
Buffers:          6704 kB
Cached:         443288 kB
SwapCached:        168 kB
Active:         278296 kB
Inactive:       175004 kB
HighTotal:      131008 kB
HighFree:        17752 kB
LowTotal:       903652 kB
LowFree:        539748 kB
SwapTotal:     2097136 kB
SwapFree:      2096968 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7220 kB
Slab:            18160 kB
Committed_AS:    92820 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 06:04:38 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 16749 7 1200.24 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 215 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #########################################################################################
c   -- Clauses(.)/Splits(s): ...
c ---[ 214]---> Adder-cost: 1416   maxlim: 2733   bits: 12/12
c ---[ 213]---> Sorter-cost:  634     Base:
c ---[ 212]---> Sorter-cost:  238     Base:
c ---[ 211]---> Sorter-cost:  238     Base:
c ---[ 210]---> Sorter-cost:  206     Base:
c ---[ 209]---> Sorter-cost:  356     Base:
c ---[ 208]---> Sorter-cost:  356     Base:
c ---[ 207]---> Sorter-cost:  264     Base:
c ---[ 206]---> Sorter-cost:  126     Base:
c ---[ 205]---> Sorter-cost:  356     Base:
c ---[ 204]---> Sorter-cost:  106     Base:
c ---[ 203]---> BDD-cost:   43
c ---[ 202]---> BDD-cost:   34
c ---[ 201]---> Sorter-cost:  170     Base:
c ---[ 200]---> BDD-cost:   29
c ---[ 199]---> Sorter-cost:  180     Base:
c ---[ 198]---> BDD-cost:   31
c ---[ 197]---> BDD-cost:   21
c ---[ 195]---> Sorter-cost:  561     Base:
c ---[ 193]---> BDD-cost:   41
c ---[ 191]---> Sorter-cost:  255     Base:
c ---[ 189]---> Sorter-cost:  207     Base:
c ---[ 187]---> Sorter-cost:  491     Base:
c ---[ 185]---> Sorter-cost:  239     Base:
c ---[ 183]---> Sorter-cost:  281     Base:
c ---[ 181]---> Sorter-cost:  181     Base:
c ---[ 179]---> Sorter-cost:  291     Base:
c ---[ 177]---> Sorter-cost:  127     Base:
c ---[ 175]---> BDD-cost:   33
c ---[ 173]---> Sorter-cost:  207     Base:
c ---[ 171]---> Sorter-cost:  117     Base:
c ---[ 169]---> Sorter-cost:   77     Base:
c ---[ 167]---> Sorter-cost:  171     Base:
c ---[ 165]---> Sorter-cost:  127     Base:
c ---[ 163]---> BDD-cost:   29
c ---[ 161]---> BDD-cost:   25
c ---[ 159]---> Adder-cost: 155   maxlim: 27   bits: 6/5
c ---[ 157]---> Sorter-cost:  631     Base:
c ---[ 155]---> Sorter-cost:  689     Base:
c ---[ 153]---> Sorter-cost:  609     Base:
c ---[ 151]---> Sorter-cost:  971     Base:
c ---[ 149]---> Sorter-cost:  991     Base:
c ---[ 147]---> Sorter-cost:  755     Base:
c ---[ 145]---> Sorter-cost:  371     Base:
c ---[ 143]---> Sorter-cost:  927     Base:
c ---[ 141]---> Sorter-cost:  355     Base:
c ---[ 139]---> Sorter-cost:  313     Base:
c ---[ 137]---> Sorter-cost:  279     Base:
c ---[ 135]---> Sorter-cost:  501     Base:
c ---[ 133]---> Sorter-cost:  225     Base:
c ---[ 131]---> Sorter-cost:  517     Base:
c ---[ 129]---> Sorter-cost:  197     Base:
c ---[ 127]---> BDD-cost:   66
c ---[ 126]---> Adder-cost: 732   maxlim: 1601   bits: 12/11
c ---[ 125]---> Adder-cost: 1184   maxlim: 406   bits: 10/9
c ---[ 124]---> Adder-cost: 255   maxlim: 863   bits: 11/10
c ---[ 123]---> BDD-cost:   27
c ---[ 122]---> BDD-cost:   35
c ---[ 121]---> Sorter-cost:  172     Base:
c ---[ 120]---> BDD-cost:   31
c ---[ 118]---> BDD-cost:   51
c ---[ 115]---> BDD-cost:   80
c ---[ 114]---> Sorter-cost:  238     Base:
c ---[ 113]---> Sorter-cost:  478     Base:
c ---[ 112]---> Sorter-cost:  254     Base:
c ---[ 111]---> BDD-cost:   21
c ---[ 110]---> Sorter-cost:  474     Base:
c ---[ 109]---> BDD-cost:   29
c ---[ 108]---> BDD-cost:   23
c ---[ 106]---> BDD-cost:   16
c ---[ 104]---> BDD-cost:   17
c ---[ 102]---> BDD-cost:    5
c ---[ 100]---> BDD-cost:   43
c ---[  98]---> BDD-cost:   92
c ---[  96]---> BDD-cost:  183
c ---[  94]---> BDD-cost:   11
c ---[  92]---> BDD-cost:   29
c ---[  90]---> BDD-cost:   29
c ---[  88]---> BDD-cost:   19
c ---[  86]---> BDD-cost:   11
c ---[  84]---> BDD-cost:   11
c ---[  82]---> BDD-cost:   31
c ---[  80]---> BDD-cost:   23
c ---[  78]---> BDD-cost:    7
c ---[  76]---> BDD-cost:   13
c ---[  74]---> BDD-cost:   14
c ---[  72]---> BDD-cost:   38
c ---[  70]---> BDD-cost:   23
c ---[  68]---> BDD-cost:   35
c ---[  66]---> BDD-cost:   37
c ---[  64]---> BDD-cost:    7
c ---[  62]---> BDD-cost:   17
c ---[  60]---> BDD-cost:   17
c ---[  58]---> BDD-cost:   43
c ---[  56]---> BDD-cost:   11
c ---[  54]---> BDD-cost:   29
c ---[  52]---> BDD-cost:    7
c ---[  50]---> BDD-cost:   16
c ---[  48]---> BDD-cost:   24
c ---[  46]---> BDD-cost:    5
c ---[  44]---> BDD-cost:   14
c ---[  42]---> BDD-cost:   11
c ---[  40]---> BDD-cost:   13
c ---[  38]---> BDD-cost:   16
c ---[  36]---> BDD-cost:   19
c ---[  34]---> BDD-cost:   14
c ---[  32]---> BDD-cost:   19
c ---[  30]---> BDD-cost:   11
c ---[  28]---> BDD-cost:    4
c ---[  26]---> BDD-cost:   11
c ---[  24]---> BDD-cost:   14
c ---[  22]---> BDD-cost:   15
c ---[  20]---> BDD-cost:   48
c ---[  18]---> BDD-cost:   51
c ---[  16]---> BDD-cost:   11
c ---[  14]---> BDD-cost:    6
c ---[  12]---> BDD-cost:   51
c ---[  10]---> BDD-cost:    8
c ---[   8]---> BDD-cost:   14
c ---[   6]---> BDD-cost:   43
c ---[   4]---> BDD-cost:   31
c ---[   2]---> BDD-cost:   22
c ---[   0]---> BDD-cost:   17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   59268   172692 |   19756       0        0     nan |  0.000 % |
c |       100 |   58967   172015 |   21731      54      378     7.0 |  2.982 % |
c |       250 |   58871   171801 |   23904     194     2163    11.1 |  3.144 % |
c |       478 |   58643   171296 |   26295     390     6723    17.2 |  3.542 % |
c |       817 |   58486   170918 |   28924     712    11817    16.6 |  3.778 % |
c |      1326 |   58486   170918 |   31817    1221    20748    17.0 |  3.778 % |
c |      2085 |   58029   169847 |   34998    1939    28436    14.7 |  4.505 % |
c |      3226 |   57206   167973 |   38498    2938    45487    15.5 |  5.901 % |
c |      4935 |   56852   167094 |   42348    4588    80961    17.6 |  6.397 % |
c |      7501 |   55779   164665 |   46583    6967   212735    30.5 |  8.306 % |
c |     11348 |   55700   164452 |   51241   10794   356680    33.0 |  8.428 % |
c |     17115 |   55398   163695 |   56366   16515   718991    43.5 |  8.872 % |
c |     25765 |   54846   162412 |   62002   25097  1273366    50.7 |  9.875 % |
c |     38739 |   54722   162120 |   68203   38032  2543822    66.9 | 10.083 % |
c |     58200 |   54453   161440 |   75023   57412  4736486    82.5 | 10.481 % |
c |     87392 |   54220   160887 |   82525   18335  2211078   120.6 | 10.885 % |
c |    131185 |   53722   159704 |   90778   62096  8034036   129.4 | 11.710 % |
c ==============================================================================
c [1mFound solution: 72848[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 4504   maxlim: 473010   bits: 20/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    137357 |   84969   271519 |   28323   68249  8557934   125.4 | 11.710 % |
c |    137457 |   84969   271519 |   31155   18289  1526343    83.5 |  9.573 % |
c |    137608 |   84969   271519 |   34270   18440  1531269    83.0 |  9.573 % |
c |    137833 |   84969   271519 |   37697   18665  1540508    82.5 |  9.573 % |
c |    138173 |   84969   271519 |   41467   19005  1552871    81.7 |  9.573 % |
c |    138679 |   84969   271519 |   45614   19511  1569702    80.5 |  9.573 % |
c |    139438 |   84897   271358 |   50175   20263  1642598    81.1 |  9.669 % |
c |    140578 |   84809   271158 |   55193   21391  1698960    79.4 |  9.797 % |
c |    142286 |   84638   270736 |   60712   23085  1760646    76.3 |  9.989 % |
c |    144851 |   84610   270643 |   66784   25646  1921260    74.9 | 10.003 % |
c |    148695 |   84610   270643 |   73462   29490  2086893    70.8 | 10.003 % |
c |    154464 |   84557   270524 |   80808   35250  2416240    68.5 | 10.072 % |
c |    163115 |   84531   270467 |   88889   43897  3145277    71.7 | 10.104 % |
c |    176093 |   84489   270353 |   97778   56863  4179607    73.5 | 10.145 % |
c |    195554 |   84380   270057 |  107556   76306  5512864    72.2 | 10.273 % |
c |    224747 |   84133   269463 |  118312  105473  8398966    79.6 | 10.598 % |
c |    268536 |   83772   268630 |  130143   47858  3799427    79.4 | 11.092 % |
c |    334220 |   83640   268329 |  143157  113532 12757707   112.4 | 11.262 % |
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 -ECAR002#### 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.84 0.94 0.91 2/56 21367
Raw data (stat): 21367 (runsolver) R 21366 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 427581295 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.87 0.94 0.91 2/56 21367
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 2299 0 0 0 993 5 0 0 25 0 1 0 427581295 11763712 2219 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2872 2219 603 41 0 2831 0
vsize: 11488
[startup+20.0001 s]
Raw data (loadavg): 0.89 0.94 0.91 2/56 21367
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 2720 0 0 0 1992 6 0 0 25 0 1 0 427581295 13516800 2640 4294967295 134512640 134672761 3221224624 3221223728 134560520 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3300 2640 603 41 0 3259 0
vsize: 13200
[startup+30.001 s]
Raw data (loadavg): 0.90 0.94 0.91 3/56 21369
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 3345 0 0 0 2991 8 0 0 25 0 1 0 427581295 16113664 3265 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3934 3265 603 41 0 3893 0
vsize: 15736
[startup+40.0007 s]
Raw data (loadavg): 0.92 0.94 0.91 2/56 21369
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 3739 0 0 0 3990 9 0 0 25 0 1 0 427581295 17588224 3659 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4294 3659 603 41 0 4253 0
vsize: 17176
[startup+50.0015 s]
Raw data (loadavg): 0.93 0.94 0.91 2/56 21369
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 4513 0 0 0 4988 11 0 0 25 0 1 0 427581295 20946944 4433 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5114 4433 603 41 0 5073 0
vsize: 20456
[startup+60.0017 s]
Raw data (loadavg): 0.94 0.95 0.91 2/56 21369
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 5140 0 0 0 5986 13 0 0 25 0 1 0 427581295 23498752 5060 4294967295 134512640 134672761 3221224624 3221223796 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5737 5060 603 41 0 5696 0
vsize: 22948
[startup+70.0021 s]
Raw data (loadavg): 0.95 0.95 0.91 2/56 21369
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 5559 0 0 0 6985 14 0 0 25 0 1 0 427581295 25116672 5479 4294967295 134512640 134672761 3221224624 3221223792 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6132 5479 603 41 0 6091 0
vsize: 24528
[startup+80.0029 s]
Raw data (loadavg): 0.96 0.95 0.91 2/56 21369
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 6085 0 0 0 7984 16 0 0 25 0 1 0 427581295 27275264 6005 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6659 6005 603 41 0 6618 0
vsize: 26636
[startup+90.0026 s]
Raw data (loadavg): 0.96 0.95 0.91 2/56 21369
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 6664 0 0 0 8982 17 0 0 25 0 1 0 427581295 29691904 6584 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7249 6584 603 41 0 7208 0
vsize: 28996
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/56 21369
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 7293 0 0 0 9981 18 0 0 25 0 1 0 427581295 32219136 7213 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7866 7213 603 41 0 7825 0
vsize: 31464
[startup+110.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/56 21369
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 7650 0 0 0 10981 19 0 0 25 0 1 0 427581295 33693696 7570 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8226 7570 603 41 0 8185 0
vsize: 32904
[startup+120.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 21369
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 8092 0 0 0 11980 20 0 0 25 0 1 0 427581295 35438592 8012 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8652 8012 603 41 0 8611 0
vsize: 34608
[startup+130.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 21369
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 8565 0 0 0 12979 22 0 0 25 0 1 0 427581295 37724160 8485 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9210 8485 603 41 0 9169 0
vsize: 36840
[startup+140.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 21369
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 9037 0 0 0 13978 22 0 0 25 0 1 0 427581295 39596032 8957 4294967295 134512640 134672761 3221224624 3221223728 134554910 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9667 8957 603 41 0 9626 0
vsize: 38668
[startup+150.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 21369
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 9485 0 0 0 14977 24 0 0 25 0 1 0 427581295 41345024 9405 4294967295 134512640 134672761 3221224624 3221223728 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10094 9405 603 41 0 10053 0
vsize: 40376
[startup+160.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 21369
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 9958 0 0 0 15976 25 0 0 25 0 1 0 427581295 43356160 9878 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10585 9878 603 41 0 10544 0
vsize: 42340
[startup+170.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 21369
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 10411 0 0 0 16974 26 0 0 25 0 1 0 427581295 45113344 10331 4294967295 134512640 134672761 3221224624 3221223696 134553549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11014 10331 603 41 0 10973 0
vsize: 44056
[startup+180.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 21369
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 10860 0 0 0 17973 28 0 0 25 0 1 0 427581295 46985216 10780 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11471 10780 603 41 0 11430 0
vsize: 45884
[startup+190.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 21369
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 11257 0 0 0 18971 30 0 0 25 0 1 0 427581295 48594944 11177 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11864 11177 603 41 0 11823 0
vsize: 47456
[startup+200.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 21369
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 11666 0 0 0 19971 31 0 0 25 0 1 0 427581295 50348032 11586 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12292 11586 603 41 0 12251 0
vsize: 49168
[startup+210.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 21369
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 11953 0 0 0 20970 32 0 0 25 0 1 0 427581295 51429376 11873 4294967295 134512640 134672761 3221224624 3221223760 134560716 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12556 11873 603 41 0 12515 0
vsize: 50224
[startup+220.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 21369
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 11953 0 0 0 21969 32 0 0 25 0 1 0 427581295 51429376 11873 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12556 11873 603 41 0 12515 0
vsize: 50224
[startup+230.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 21369
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 11953 0 0 0 22970 32 0 0 25 0 1 0 427581295 51429376 11873 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12556 11873 603 41 0 12515 0
vsize: 50224
[startup+240.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 21369
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 11953 0 0 0 23970 32 0 0 25 0 1 0 427581295 51429376 11873 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12556 11873 603 41 0 12515 0
vsize: 50224
[startup+250.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 21369
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 11953 0 0 0 24970 32 0 0 25 0 1 0 427581295 51429376 11873 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12556 11873 603 41 0 12515 0
vsize: 50224
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21369
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 11953 0 0 0 25970 33 0 0 25 0 1 0 427581295 51429376 11873 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12556 11873 603 41 0 12515 0
vsize: 50224
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21369
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 11953 0 0 0 26970 33 0 0 25 0 1 0 427581295 51429376 11873 4294967295 134512640 134672761 3221224624 3221223808 134559611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12556 11873 603 41 0 12515 0
vsize: 50224
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21369
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 11953 0 0 0 27970 33 0 0 25 0 1 0 427581295 51429376 11873 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12556 11873 603 41 0 12515 0
vsize: 50224
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21369
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 11953 0 0 0 28970 33 0 0 25 0 1 0 427581295 51429376 11873 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12556 11873 603 41 0 12515 0
vsize: 50224
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21369
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 11953 0 0 0 29970 33 0 0 25 0 1 0 427581295 51429376 11873 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12556 11873 603 41 0 12515 0
vsize: 50224
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21369
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 11953 0 0 0 30970 33 0 0 25 0 1 0 427581295 51429376 11873 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12556 11873 603 41 0 12515 0
vsize: 50224
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21369
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 11953 0 0 0 31970 33 0 0 25 0 1 0 427581295 51429376 11873 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12556 11873 603 41 0 12515 0
vsize: 50224
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21371
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 11953 0 0 0 32970 34 0 0 25 0 1 0 427581295 51429376 11873 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12556 11873 603 41 0 12515 0
vsize: 50224
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21371
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 11953 0 0 0 33970 34 0 0 25 0 1 0 427581295 51429376 11873 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12556 11873 603 41 0 12515 0
vsize: 50224
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21371
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 14554 0 0 0 34962 41 0 0 25 0 1 0 427581295 59981824 13896 4294967295 134512640 134672761 3221224624 3221223792 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14644 13896 603 41 0 14603 0
vsize: 58576
[startup+360.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21371
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 14554 0 0 0 35963 41 0 0 25 0 1 0 427581295 59981824 13896 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14644 13896 603 41 0 14603 0
vsize: 58576
[startup+370.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21371
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 14554 0 0 0 36963 41 0 0 25 0 1 0 427581295 59981824 13896 4294967295 134512640 134672761 3221224624 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14644 13896 603 41 0 14603 0
vsize: 58576
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21371
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 14554 0 0 0 37963 41 0 0 25 0 1 0 427581295 59981824 13896 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14644 13896 603 41 0 14603 0
vsize: 58576
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21371
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 14554 0 0 0 38963 42 0 0 25 0 1 0 427581295 59981824 13896 4294967295 134512640 134672761 3221224624 3221223760 134560683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14644 13896 603 41 0 14603 0
vsize: 58576
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21371
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 14554 0 0 0 39963 42 0 0 25 0 1 0 427581295 59981824 13896 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14644 13896 603 41 0 14603 0
vsize: 58576
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21371
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 14554 0 0 0 40963 42 0 0 25 0 1 0 427581295 59981824 13896 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14644 13896 603 41 0 14603 0
vsize: 58576
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21371
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 14554 0 0 0 41963 42 0 0 25 0 1 0 427581295 59981824 13896 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14644 13896 603 41 0 14603 0
vsize: 58576
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21371
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 14554 0 0 0 42963 42 0 0 25 0 1 0 427581295 59981824 13896 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14644 13896 603 41 0 14603 0
vsize: 58576
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21371
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 14554 0 0 0 43963 42 0 0 25 0 1 0 427581295 59981824 13896 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14644 13896 603 41 0 14603 0
vsize: 58576
[startup+450.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21371
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 14554 0 0 0 44963 42 0 0 25 0 1 0 427581295 59981824 13896 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14644 13896 603 41 0 14603 0
vsize: 58576
[startup+460.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21371
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 14554 0 0 0 45963 42 0 0 25 0 1 0 427581295 59981824 13896 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14644 13896 603 41 0 14603 0
vsize: 58576
[startup+470.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21371
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 14554 0 0 0 46963 42 0 0 25 0 1 0 427581295 59981824 13896 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14644 13896 603 41 0 14603 0
vsize: 58576
[startup+480.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21371
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 14554 0 0 0 47963 42 0 0 25 0 1 0 427581295 59981824 13896 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14644 13896 603 41 0 14603 0
vsize: 58576
[startup+490.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21371
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 14555 0 0 0 48963 42 0 0 25 0 1 0 427581295 59981824 13897 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14644 13897 603 41 0 14603 0
vsize: 58576
[startup+500.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21371
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 14555 0 0 0 49964 42 0 0 25 0 1 0 427581295 59981824 13897 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14644 13897 603 41 0 14603 0
vsize: 58576
[startup+510.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21371
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 14555 0 0 0 50964 42 0 0 25 0 1 0 427581295 59981824 13897 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14644 13897 603 41 0 14603 0
vsize: 58576
[startup+520.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21371
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 14558 0 0 0 51964 42 0 0 25 0 1 0 427581295 59981824 13900 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14644 13900 603 41 0 14603 0
vsize: 58576
[startup+530.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21371
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 14561 0 0 0 52964 42 0 0 25 0 1 0 427581295 59981824 13903 4294967295 134512640 134672761 3221224624 3221223760 134565149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14644 13903 603 41 0 14603 0
vsize: 58576
[startup+540.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21371
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 14563 0 0 0 53964 42 0 0 25 0 1 0 427581295 59981824 13905 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14644 13905 603 41 0 14603 0
vsize: 58576
[startup+550.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21371
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 14566 0 0 0 54965 42 0 0 25 0 1 0 427581295 59981824 13908 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14644 13908 603 41 0 14603 0
vsize: 58576
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21371
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 14570 0 0 0 55965 43 0 0 25 0 1 0 427581295 59981824 13912 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14644 13912 603 41 0 14603 0
vsize: 58576
[startup+570.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21371
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 14572 0 0 0 56965 43 0 0 25 0 1 0 427581295 59981824 13914 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14644 13914 603 41 0 14603 0
vsize: 58576
[startup+580.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21371
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 14868 0 0 0 57964 43 0 0 25 0 1 0 427581295 61186048 14210 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14938 14210 603 41 0 14897 0
vsize: 59752
[startup+590.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21371
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 15031 0 0 0 58964 44 0 0 25 0 1 0 427581295 61861888 14373 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15103 14373 603 41 0 15062 0
vsize: 60412
[startup+600.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21371
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 15278 0 0 0 59963 45 0 0 25 0 1 0 427581295 62935040 14620 4294967295 134512640 134672761 3221224624 3221223728 134559841 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15365 14620 603 41 0 15324 0
vsize: 61460
[startup+610.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21371
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 15558 0 0 0 60962 46 0 0 25 0 1 0 427581295 64008192 14900 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15627 14900 603 41 0 15586 0
vsize: 62508
[startup+620.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21371
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 15917 0 0 0 61962 47 0 0 25 0 1 0 427581295 65511424 15259 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15994 15259 603 41 0 15953 0
vsize: 63976
[startup+630.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21373
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 16176 0 0 0 62960 48 0 0 25 0 1 0 427581295 66580480 15518 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16255 15518 603 41 0 16214 0
vsize: 65020
[startup+640.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21373
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 16303 0 0 0 63960 48 0 0 25 0 1 0 427581295 67117056 15645 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16386 15645 603 41 0 16345 0
vsize: 65544
[startup+650.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21373
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 16488 0 0 0 64960 49 0 0 25 0 1 0 427581295 67788800 15830 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16550 15830 603 41 0 16509 0
vsize: 66200
[startup+660.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21373
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 16681 0 0 0 65959 50 0 0 25 0 1 0 427581295 68587520 16023 4294967295 134512640 134672761 3221224624 3221223088 134565798 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16745 16023 603 41 0 16704 0
vsize: 66980
[startup+670.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21373
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 16681 0 0 0 66959 50 0 0 25 0 1 0 427581295 68587520 16023 4294967295 134512640 134672761 3221224624 3221223808 134559522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16745 16023 603 41 0 16704 0
vsize: 66980
[startup+680.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21373
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 16681 0 0 0 67959 50 0 0 25 0 1 0 427581295 68587520 16023 4294967295 134512640 134672761 3221224624 3221223792 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16745 16023 603 41 0 16704 0
vsize: 66980
[startup+690.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21373
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 16681 0 0 0 68960 50 0 0 25 0 1 0 427581295 68587520 16023 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16745 16023 603 41 0 16704 0
vsize: 66980
[startup+700.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21373
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 16681 0 0 0 69960 50 0 0 25 0 1 0 427581295 68587520 16023 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16745 16023 603 41 0 16704 0
vsize: 66980
[startup+710.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21373
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 16681 0 0 0 70960 50 0 0 25 0 1 0 427581295 68587520 16023 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16745 16023 603 41 0 16704 0
vsize: 66980
[startup+720.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21373
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 16681 0 0 0 71960 50 0 0 25 0 1 0 427581295 68587520 16023 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16745 16023 603 41 0 16704 0
vsize: 66980
[startup+730.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21373
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 16681 0 0 0 72961 50 0 0 25 0 1 0 427581295 68587520 16023 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16745 16023 603 41 0 16704 0
vsize: 66980
[startup+740.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21373
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 16681 0 0 0 73961 50 0 0 25 0 1 0 427581295 68587520 16023 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16745 16023 603 41 0 16704 0
vsize: 66980
[startup+750.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21373
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 16681 0 0 0 74961 50 0 0 25 0 1 0 427581295 68587520 16023 4294967295 134512640 134672761 3221224624 3221223808 134559116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16745 16023 603 41 0 16704 0
vsize: 66980
[startup+760.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21373
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 16681 0 0 0 75961 50 0 0 25 0 1 0 427581295 68587520 16023 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16745 16023 603 41 0 16704 0
vsize: 66980
[startup+770.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21373
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 16681 0 0 0 76961 50 0 0 25 0 1 0 427581295 68587520 16023 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16745 16023 603 41 0 16704 0
vsize: 66980
[startup+780.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21373
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 16681 0 0 0 77961 50 0 0 25 0 1 0 427581295 68587520 16023 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16745 16023 603 41 0 16704 0
vsize: 66980
[startup+790.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21373
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 16681 0 0 0 78961 50 0 0 25 0 1 0 427581295 68587520 16023 4294967295 134512640 134672761 3221224624 3221223780 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16745 16023 603 41 0 16704 0
vsize: 66980
[startup+800.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21373
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 16681 0 0 0 79961 50 0 0 25 0 1 0 427581295 68587520 16023 4294967295 134512640 134672761 3221224624 3221223728 134559964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16745 16023 603 41 0 16704 0
vsize: 66980
[startup+810.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21373
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 16681 0 0 0 80961 50 0 0 25 0 1 0 427581295 68587520 16023 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16745 16023 603 41 0 16704 0
vsize: 66980
[startup+820.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21373
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 16681 0 0 0 81961 51 0 0 25 0 1 0 427581295 68587520 16023 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16745 16023 603 41 0 16704 0
vsize: 66980
[startup+830.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21373
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 16681 0 0 0 82961 51 0 0 25 0 1 0 427581295 68587520 16023 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16745 16023 603 41 0 16704 0
vsize: 66980
[startup+840.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21373
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 16681 0 0 0 83961 51 0 0 25 0 1 0 427581295 68587520 16023 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16745 16023 603 41 0 16704 0
vsize: 66980
[startup+850.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21373
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 16681 0 0 0 84961 51 0 0 25 0 1 0 427581295 68587520 16023 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16745 16023 603 41 0 16704 0
vsize: 66980
[startup+860.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21373
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 16681 0 0 0 85961 51 0 0 25 0 1 0 427581295 68587520 16023 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16745 16023 603 41 0 16704 0
vsize: 66980
[startup+870.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21373
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 16681 0 0 0 86961 51 0 0 25 0 1 0 427581295 68587520 16023 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16745 16023 603 41 0 16704 0
vsize: 66980
[startup+880.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21373
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 16681 0 0 0 87961 51 0 0 25 0 1 0 427581295 68587520 16023 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16745 16023 603 41 0 16704 0
vsize: 66980
[startup+890.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21373
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 16784 0 0 0 88961 51 0 0 25 0 1 0 427581295 68984832 16126 4294967295 134512640 134672761 3221224624 3221223792 134561234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16842 16126 603 41 0 16801 0
vsize: 67368
[startup+900.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21373
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 17194 0 0 0 89959 53 0 0 25 0 1 0 427581295 70729728 16536 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17268 16536 603 41 0 17227 0
vsize: 69072
[startup+910.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21373
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 17616 0 0 0 90958 54 0 0 25 0 1 0 427581295 72458240 16958 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17690 16958 603 41 0 17649 0
vsize: 70760
[startup+920.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21373
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 18001 0 0 0 91957 55 0 0 25 0 1 0 427581295 74067968 17343 4294967295 134512640 134672761 3221224624 3221223792 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18083 17343 603 41 0 18042 0
vsize: 72332
[startup+930.026 s]
Raw data (loadavg): 0.99 0.97 0.91 3/58 21415
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 18372 0 0 0 92956 56 0 0 25 0 1 0 427581295 75538432 17714 4294967295 134512640 134672761 3221224624 3221223792 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18442 17714 603 41 0 18401 0
vsize: 73768
[startup+940.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21428
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 18707 0 0 0 93955 57 0 0 25 0 1 0 427581295 76873728 18049 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18768 18049 603 41 0 18727 0
vsize: 75072
[startup+950.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21428
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 19003 0 0 0 94955 58 0 0 25 0 1 0 427581295 78200832 18345 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19092 18345 603 41 0 19051 0
vsize: 76368
[startup+960.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21428
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 19293 0 0 0 95955 59 0 0 25 0 1 0 427581295 79417344 18635 4294967295 134512640 134672761 3221224624 3221223808 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19389 18635 603 41 0 19348 0
vsize: 77556
[startup+970.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21428
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 19523 0 0 0 96954 60 0 0 25 0 1 0 427581295 80367616 18865 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19621 18865 603 41 0 19580 0
vsize: 78484
[startup+980.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21428
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 19809 0 0 0 97953 61 0 0 25 0 1 0 427581295 81444864 19151 4294967295 134512640 134672761 3221224624 3221223728 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19884 19151 603 41 0 19843 0
vsize: 79536
[startup+990.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21430
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 20087 0 0 0 98952 62 0 0 25 0 1 0 427581295 82657280 19429 4294967295 134512640 134672761 3221224624 3221223728 134560424 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20180 19429 603 41 0 20139 0
vsize: 80720
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21430
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 20364 0 0 0 99951 63 0 0 25 0 1 0 427581295 83726336 19706 4294967295 134512640 134672761 3221224624 3221223728 134560350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20441 19706 603 41 0 20400 0
vsize: 81764
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21432
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 20724 0 0 0 100950 64 0 0 25 0 1 0 427581295 85176320 20066 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20795 20066 603 41 0 20754 0
vsize: 83180
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21432
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 21076 0 0 0 101949 65 0 0 25 0 1 0 427581295 86642688 20418 4294967295 134512640 134672761 3221224624 3221223728 134559841 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21153 20418 603 41 0 21112 0
vsize: 84612
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21432
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 21435 0 0 0 102949 66 0 0 25 0 1 0 427581295 88113152 20777 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21512 20777 603 41 0 21471 0
vsize: 86048
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21432
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 21821 0 0 0 103948 67 0 0 25 0 1 0 427581295 89698304 21163 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21899 21163 603 41 0 21858 0
vsize: 87596
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21432
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 22229 0 0 0 104947 68 0 0 25 0 1 0 427581295 91414528 21571 4294967295 134512640 134672761 3221224624 3221223728 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22318 21571 603 41 0 22277 0
vsize: 89272
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21432
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 22556 0 0 0 105946 69 0 0 25 0 1 0 427581295 92733440 21898 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22640 21898 603 41 0 22599 0
vsize: 90560
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21432
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 22854 0 0 0 106946 70 0 0 25 0 1 0 427581295 94453760 22196 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23060 22196 603 41 0 23019 0
vsize: 92240
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21432
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 23158 0 0 0 107944 71 0 0 25 0 1 0 427581295 95645696 22500 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23351 22500 603 41 0 23310 0
vsize: 93404
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21432
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 23482 0 0 0 108944 72 0 0 25 0 1 0 427581295 96972800 22824 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23675 22824 603 41 0 23634 0
vsize: 94700
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21432
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 23777 0 0 0 109944 72 0 0 25 0 1 0 427581295 98168832 23119 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23967 23119 603 41 0 23926 0
vsize: 95868
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21432
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 24068 0 0 0 110943 73 0 0 25 0 1 0 427581295 99360768 23410 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24258 23410 603 41 0 24217 0
vsize: 97032
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21432
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 24224 0 0 0 111943 73 0 0 25 0 1 0 427581295 100028416 23566 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24421 23566 603 41 0 24380 0
vsize: 97684
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21432
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 24410 0 0 0 112943 74 0 0 25 0 1 0 427581295 100835328 23752 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24618 23752 603 41 0 24577 0
vsize: 98472
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21432
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 24574 0 0 0 113942 75 0 0 25 0 1 0 427581295 101511168 23916 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24783 23916 603 41 0 24742 0
vsize: 99132
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21432
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 24678 0 0 0 114942 75 0 0 25 0 1 0 427581295 101916672 24020 4294967295 134512640 134672761 3221224624 3221223088 134565768 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24882 24020 603 41 0 24841 0
vsize: 99528
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21432
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 24678 0 0 0 115942 75 0 0 25 0 1 0 427581295 101916672 24020 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24882 24020 603 41 0 24841 0
vsize: 99528
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21432
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 24678 0 0 0 116942 75 0 0 25 0 1 0 427581295 101916672 24020 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24882 24020 603 41 0 24841 0
vsize: 99528
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21432
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 24678 0 0 0 117942 75 0 0 25 0 1 0 427581295 101916672 24020 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24882 24020 603 41 0 24841 0
vsize: 99528
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21432
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 24678 0 0 0 118942 75 0 0 25 0 1 0 427581295 101916672 24020 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24882 24020 603 41 0 24841 0
vsize: 99528
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21432
Raw data (stat): 21367 (minisat+) R 21366 12452 12451 0 -1 0 24678 0 0 0 119943 75 0 0 25 0 1 0 427581295 101916672 24020 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24882 24020 603 41 0 24841 0
vsize: 99528
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 1/56 21432
Raw data (stat): 21367 (minisat+) Z 21366 12452 12451 0 -1 12 24681 0 0 0 119943 80 0 0 25 0 1 0 427581295 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.09
CPU time (s): 1200.24
CPU user time (s): 1199.43
CPU system time (s): 0.805877
CPU usage (%): 100.012
Max. virtual memory (Kb): 99528
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####