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 17091

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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:        807688 kB
Buffers:         18932 kB
Cached:         182524 kB
SwapCached:        844 kB
Active:          42636 kB
Inactive:       160912 kB
HighTotal:      131008 kB
HighFree:        29428 kB
LowTotal:       903652 kB
LowFree:        778260 kB
SwapTotal:     2097892 kB
SwapFree:      2096168 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5096 kB
Slab:            17752 kB
Committed_AS:    63816 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 09:58:48 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 11757 7 1200.22 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.91 0.95 0.90 2/55 26927
Raw data (stat): 26927 (runsolver) R 26926 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 544054178 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.93 0.95 0.90 2/55 26927
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 2297 0 0 0 993 5 0 0 25 0 1 0 544054178 11763712 2217 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2872 2217 603 41 0 2831 0
vsize: 11488
[startup+20.0027 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 26927
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 2696 0 0 0 1992 6 0 0 25 0 1 0 544054178 13385728 2616 4294967295 134512640 134672761 3221224624 3221223808 134558629 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3268 2616 603 41 0 3227 0
vsize: 13072
[startup+30.0031 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 26927
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 3337 0 0 0 2990 8 0 0 25 0 1 0 544054178 15978496 3257 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3901 3257 603 41 0 3860 0
vsize: 15604
[startup+40.0032 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 26927
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 3693 0 0 0 3989 9 0 0 25 0 1 0 544054178 17453056 3613 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4261 3613 603 41 0 4220 0
vsize: 17044
[startup+50.0041 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 26927
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 4461 0 0 0 4987 11 0 0 25 0 1 0 544054178 20676608 4381 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5048 4381 603 41 0 5007 0
vsize: 20192
[startup+60.0038 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 26927
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 5139 0 0 0 5985 13 0 0 25 0 1 0 544054178 23498752 5059 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5737 5059 603 41 0 5696 0
vsize: 22948
[startup+70.0053 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 26927
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 5502 0 0 0 6984 14 0 0 25 0 1 0 544054178 24981504 5422 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6099 5422 603 41 0 6058 0
vsize: 24396
[startup+80.0059 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 26927
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 6013 0 0 0 7983 15 0 0 25 0 1 0 544054178 27004928 5933 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6593 5933 603 41 0 6552 0
vsize: 26372
[startup+90.0056 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 26927
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 6582 0 0 0 8981 17 0 0 25 0 1 0 544054178 29290496 6502 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7151 6502 603 41 0 7110 0
vsize: 28604
[startup+100.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 26927
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 7195 0 0 0 9979 20 0 0 25 0 1 0 544054178 31817728 7115 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7768 7115 603 41 0 7727 0
vsize: 31072
[startup+110.007 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 26927
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 7576 0 0 0 10977 21 0 0 25 0 1 0 544054178 33423360 7496 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8160 7496 603 41 0 8119 0
vsize: 32640
[startup+120.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26929
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 8011 0 0 0 11976 22 0 0 25 0 1 0 544054178 35168256 7931 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8586 7931 603 41 0 8545 0
vsize: 34344
[startup+130.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26929
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 8468 0 0 0 12975 24 0 0 25 0 1 0 544054178 37318656 8388 4294967295 134512640 134672761 3221224624 3221223808 134559572 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9111 8388 603 41 0 9070 0
vsize: 36444
[startup+140.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26929
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 8934 0 0 0 13974 25 0 0 25 0 1 0 544054178 39194624 8854 4294967295 134512640 134672761 3221224624 3221223792 134560968 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9569 8854 603 41 0 9528 0
vsize: 38276
[startup+150.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26929
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 9379 0 0 0 14973 27 0 0 25 0 1 0 544054178 40939520 9299 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9995 9299 603 41 0 9954 0
vsize: 39980
[startup+160.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26929
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 9839 0 0 0 15971 28 0 0 25 0 1 0 544054178 42815488 9759 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10453 9759 603 41 0 10412 0
vsize: 41812
[startup+170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26929
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 10289 0 0 0 16969 30 0 0 25 0 1 0 544054178 44707840 10209 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10915 10209 603 41 0 10874 0
vsize: 43660
[startup+180.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26929
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 10745 0 0 0 17968 32 0 0 25 0 1 0 544054178 46583808 10665 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11373 10665 603 41 0 11332 0
vsize: 45492
[startup+190.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26929
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 11132 0 0 0 18968 32 0 0 25 0 1 0 544054178 48189440 11052 4294967295 134512640 134672761 3221224624 3221223728 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11765 11052 603 41 0 11724 0
vsize: 47060
[startup+200.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26929
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 11541 0 0 0 19967 33 0 0 25 0 1 0 544054178 49807360 11461 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12160 11461 603 41 0 12119 0
vsize: 48640
[startup+210.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26929
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 11953 0 0 0 20966 35 0 0 25 0 1 0 544054178 51429376 11873 4294967295 134512640 134672761 3221224624 3221223620 1075351233 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.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26929
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 11953 0 0 0 21966 35 0 0 25 0 1 0 544054178 51429376 11873 4294967295 134512640 134672761 3221224624 3221223792 134560830 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26929
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 11953 0 0 0 22966 35 0 0 25 0 1 0 544054178 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+240.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26929
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 11953 0 0 0 23966 35 0 0 25 0 1 0 544054178 51429376 11873 4294967295 134512640 134672761 3221224624 3221223728 134560057 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.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26929
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 11953 0 0 0 24967 35 0 0 25 0 1 0 544054178 51429376 11873 4294967295 134512640 134672761 3221224624 3221223728 134560196 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.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26929
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 11953 0 0 0 25967 35 0 0 25 0 1 0 544054178 51429376 11873 4294967295 134512640 134672761 3221224624 3221223728 134560246 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.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26929
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 11953 0 0 0 26967 35 0 0 25 0 1 0 544054178 51429376 11873 4294967295 134512640 134672761 3221224624 3221223792 134560940 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.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26929
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 11953 0 0 0 27967 35 0 0 25 0 1 0 544054178 51429376 11873 4294967295 134512640 134672761 3221224624 3221223728 134560010 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.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26929
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 11953 0 0 0 28967 35 0 0 25 0 1 0 544054178 51429376 11873 4294967295 134512640 134672761 3221224624 3221223792 134561378 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.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26929
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 11953 0 0 0 29967 35 0 0 25 0 1 0 544054178 51429376 11873 4294967295 134512640 134672761 3221224624 3221223748 134566037 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.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26929
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 11953 0 0 0 30967 35 0 0 25 0 1 0 544054178 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+320.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26929
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 11953 0 0 0 31968 35 0 0 25 0 1 0 544054178 51429376 11873 4294967295 134512640 134672761 3221224624 3221223728 134560318 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26929
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 11953 0 0 0 32968 35 0 0 25 0 1 0 544054178 51429376 11873 4294967295 134512640 134672761 3221224624 3221223796 134556634 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26929
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 11953 0 0 0 33968 35 0 0 25 0 1 0 544054178 51429376 11873 4294967295 134512640 134672761 3221224624 3221223792 134561198 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.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26929
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 14551 0 0 0 34962 41 0 0 25 0 1 0 544054178 59981824 13893 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14644 13893 603 41 0 14603 0
vsize: 58576
[startup+360.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26929
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 14554 0 0 0 35961 42 0 0 25 0 1 0 544054178 59981824 13896 4294967295 134512640 134672761 3221224624 3221223792 134560828 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.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26929
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 14554 0 0 0 36961 42 0 0 25 0 1 0 544054178 59981824 13896 4294967295 134512640 134672761 3221224624 3221223768 134560630 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.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26929
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 14554 0 0 0 37962 42 0 0 25 0 1 0 544054178 59981824 13896 4294967295 134512640 134672761 3221224624 3221223796 134556682 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.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26929
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 14554 0 0 0 38962 42 0 0 25 0 1 0 544054178 59981824 13896 4294967295 134512640 134672761 3221224624 3221223796 134556641 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.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26929
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 14554 0 0 0 39962 42 0 0 25 0 1 0 544054178 59981824 13896 4294967295 134512640 134672761 3221224624 3221223824 134557842 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.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26929
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 14554 0 0 0 40962 42 0 0 25 0 1 0 544054178 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+420.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26931
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 14554 0 0 0 41962 42 0 0 25 0 1 0 544054178 59981824 13896 4294967295 134512640 134672761 3221224624 3221223792 134560876 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.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26931
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 14554 0 0 0 42962 42 0 0 25 0 1 0 544054178 59981824 13896 4294967295 134512640 134672761 3221224624 3221223792 134560871 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.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26931
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 14554 0 0 0 43963 42 0 0 25 0 1 0 544054178 59981824 13896 4294967295 134512640 134672761 3221224624 3221223792 134561229 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.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26931
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 14554 0 0 0 44963 42 0 0 25 0 1 0 544054178 59981824 13896 4294967295 134512640 134672761 3221224624 3221223792 134561001 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.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26931
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 14554 0 0 0 45963 42 0 0 25 0 1 0 544054178 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+470.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26931
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 14554 0 0 0 46963 42 0 0 25 0 1 0 544054178 59981824 13896 4294967295 134512640 134672761 3221224624 3221223796 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14644 13896 603 41 0 14603 0
vsize: 58576
[startup+480.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26931
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 14554 0 0 0 47963 42 0 0 25 0 1 0 544054178 59981824 13896 4294967295 134512640 134672761 3221224624 3221223796 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14644 13896 603 41 0 14603 0
vsize: 58576
[startup+490.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26931
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 14555 0 0 0 48963 42 0 0 25 0 1 0 544054178 59981824 13897 4294967295 134512640 134672761 3221224624 3221223728 134560408 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14644 13897 603 41 0 14603 0
vsize: 58576
[startup+500.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26931
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 14555 0 0 0 49964 42 0 0 25 0 1 0 544054178 59981824 13897 4294967295 134512640 134672761 3221224624 3221223792 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14644 13897 603 41 0 14603 0
vsize: 58576
[startup+510.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26931
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 14555 0 0 0 50964 42 0 0 25 0 1 0 544054178 59981824 13897 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14644 13897 603 41 0 14603 0
vsize: 58576
[startup+520.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26931
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 14556 0 0 0 51964 42 0 0 25 0 1 0 544054178 59981824 13898 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14644 13898 603 41 0 14603 0
vsize: 58576
[startup+530.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26931
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 14559 0 0 0 52964 42 0 0 25 0 1 0 544054178 59981824 13901 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14644 13901 603 41 0 14603 0
vsize: 58576
[startup+540.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26931
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 14561 0 0 0 53964 42 0 0 25 0 1 0 544054178 59981824 13903 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14644 13903 603 41 0 14603 0
vsize: 58576
[startup+550.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26931
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 14563 0 0 0 54964 42 0 0 25 0 1 0 544054178 59981824 13905 4294967295 134512640 134672761 3221224624 3221223856 134541850 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14644 13905 603 41 0 14603 0
vsize: 58576
[startup+560.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26931
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 14567 0 0 0 55964 42 0 0 25 0 1 0 544054178 59981824 13909 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14644 13909 603 41 0 14603 0
vsize: 58576
[startup+570.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26931
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 14570 0 0 0 56965 42 0 0 25 0 1 0 544054178 59981824 13912 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14644 13912 603 41 0 14603 0
vsize: 58576
[startup+580.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26931
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 14650 0 0 0 57965 42 0 0 25 0 1 0 544054178 60379136 13992 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14741 13992 603 41 0 14700 0
vsize: 58964
[startup+590.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26931
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 14914 0 0 0 58964 43 0 0 25 0 1 0 544054178 61456384 14256 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15004 14256 603 41 0 14963 0
vsize: 60016
[startup+600.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26931
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 15085 0 0 0 59964 43 0 0 25 0 1 0 544054178 62128128 14427 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15168 14427 603 41 0 15127 0
vsize: 60672
[startup+610.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26931
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 15327 0 0 0 60963 44 0 0 25 0 1 0 544054178 63070208 14669 4294967295 134512640 134672761 3221224624 3221223760 134560683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15398 14669 603 41 0 15357 0
vsize: 61592
[startup+620.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26931
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 15660 0 0 0 61962 45 0 0 25 0 1 0 544054178 64409600 15002 4294967295 134512640 134672761 3221224624 3221223728 134560034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15725 15002 603 41 0 15684 0
vsize: 62900
[startup+630.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26931
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 16000 0 0 0 62961 47 0 0 25 0 1 0 544054178 65781760 15342 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16060 15342 603 41 0 16019 0
vsize: 64240
[startup+640.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26931
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 16227 0 0 0 63960 48 0 0 25 0 1 0 544054178 66711552 15569 4294967295 134512640 134672761 3221224624 3221223792 134561121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16287 15569 603 41 0 16246 0
vsize: 65148
[startup+650.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26931
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 16349 0 0 0 64960 48 0 0 25 0 1 0 544054178 67252224 15691 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16419 15691 603 41 0 16378 0
vsize: 65676
[startup+660.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26931
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 16537 0 0 0 65959 49 0 0 25 0 1 0 544054178 68059136 15879 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16616 15879 603 41 0 16575 0
vsize: 66464
[startup+670.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26931
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 16681 0 0 0 66959 50 0 0 25 0 1 0 544054178 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+680.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26931
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 16681 0 0 0 67959 50 0 0 25 0 1 0 544054178 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+690.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26931
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 16681 0 0 0 68959 50 0 0 25 0 1 0 544054178 68587520 16023 4294967295 134512640 134672761 3221224624 3221223728 134559841 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16745 16023 603 41 0 16704 0
vsize: 66980
[startup+700.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26931
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 16681 0 0 0 69959 50 0 0 25 0 1 0 544054178 68587520 16023 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16745 16023 603 41 0 16704 0
vsize: 66980
[startup+710.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26931
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 16681 0 0 0 70959 50 0 0 25 0 1 0 544054178 68587520 16023 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16745 16023 603 41 0 16704 0
vsize: 66980
[startup+720.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26933
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 16681 0 0 0 71959 50 0 0 25 0 1 0 544054178 68587520 16023 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16745 16023 603 41 0 16704 0
vsize: 66980
[startup+730.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26933
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 16681 0 0 0 72960 50 0 0 25 0 1 0 544054178 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+740.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26933
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 16681 0 0 0 73960 50 0 0 25 0 1 0 544054178 68587520 16023 4294967295 134512640 134672761 3221224624 3221223760 134560642 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.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26933
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 16681 0 0 0 74960 50 0 0 25 0 1 0 544054178 68587520 16023 4294967295 134512640 134672761 3221224624 3221223792 134560869 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.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26933
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 16681 0 0 0 75960 50 0 0 25 0 1 0 544054178 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+770.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26933
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 16681 0 0 0 76960 50 0 0 25 0 1 0 544054178 68587520 16023 4294967295 134512640 134672761 3221224624 3221223792 134560869 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.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26933
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 16681 0 0 0 77960 50 0 0 25 0 1 0 544054178 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.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26933
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 16681 0 0 0 78960 50 0 0 25 0 1 0 544054178 68587520 16023 4294967295 134512640 134672761 3221224624 3221223792 134561118 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.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26933
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 16681 0 0 0 79960 50 0 0 25 0 1 0 544054178 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+810.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26933
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 16681 0 0 0 80960 50 0 0 25 0 1 0 544054178 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+820.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26933
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 16681 0 0 0 81961 50 0 0 25 0 1 0 544054178 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+830.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26933
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 16681 0 0 0 82961 50 0 0 25 0 1 0 544054178 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.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26933
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 16681 0 0 0 83961 50 0 0 25 0 1 0 544054178 68587520 16023 4294967295 134512640 134672761 3221224624 3221223792 134560869 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.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26933
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 16681 0 0 0 84961 50 0 0 25 0 1 0 544054178 68587520 16023 4294967295 134512640 134672761 3221224624 3221223728 134559916 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.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26933
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 16681 0 0 0 85961 50 0 0 25 0 1 0 544054178 68587520 16023 4294967295 134512640 134672761 3221224624 3221223792 134561133 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.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26933
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 16681 0 0 0 86961 50 0 0 25 0 1 0 544054178 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+880.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26933
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 16681 0 0 0 87962 50 0 0 25 0 1 0 544054178 68587520 16023 4294967295 134512640 134672761 3221224624 3221223728 134559862 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.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26933
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 16681 0 0 0 88962 50 0 0 25 0 1 0 544054178 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+900.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26933
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 16796 0 0 0 89962 50 0 0 25 0 1 0 544054178 69115904 16138 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16874 16138 603 41 0 16833 0
vsize: 67496
[startup+910.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26933
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 17198 0 0 0 90961 52 0 0 25 0 1 0 544054178 70729728 16540 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17268 16540 603 41 0 17227 0
vsize: 69072
[startup+920.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26933
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 17613 0 0 0 91960 52 0 0 25 0 1 0 544054178 72458240 16955 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17690 16955 603 41 0 17649 0
vsize: 70760
[startup+930.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26933
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 17995 0 0 0 92959 54 0 0 25 0 1 0 544054178 74067968 17337 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18083 17337 603 41 0 18042 0
vsize: 72332
[startup+940.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26933
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 18367 0 0 0 93958 55 0 0 25 0 1 0 544054178 75538432 17709 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18442 17709 603 41 0 18401 0
vsize: 73768
[startup+950.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26933
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 18695 0 0 0 94957 56 0 0 25 0 1 0 544054178 76873728 18037 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18768 18037 603 41 0 18727 0
vsize: 75072
[startup+960.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26933
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 18996 0 0 0 95956 57 0 0 25 0 1 0 544054178 78065664 18338 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19059 18338 603 41 0 19018 0
vsize: 76236
[startup+970.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26933
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 19285 0 0 0 96955 58 0 0 25 0 1 0 544054178 79282176 18627 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19356 18627 603 41 0 19315 0
vsize: 77424
[startup+980.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26933
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 19517 0 0 0 97955 59 0 0 25 0 1 0 544054178 80228352 18859 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19587 18859 603 41 0 19546 0
vsize: 78348
[startup+990.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26933
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 19789 0 0 0 98954 60 0 0 25 0 1 0 544054178 81444864 19131 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19884 19131 603 41 0 19843 0
vsize: 79536
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26933
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 20071 0 0 0 99953 60 0 0 25 0 1 0 544054178 82526208 19413 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20148 19413 603 41 0 20107 0
vsize: 80592
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26933
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 20343 0 0 0 100952 62 0 0 25 0 1 0 544054178 83591168 19685 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20408 19685 603 41 0 20367 0
vsize: 81632
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26935
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 20700 0 0 0 101951 63 0 0 25 0 1 0 544054178 85176320 20042 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20795 20042 603 41 0 20754 0
vsize: 83180
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26935
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 21045 0 0 0 102949 65 0 0 25 0 1 0 544054178 86511616 20387 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21121 20387 603 41 0 21080 0
vsize: 84484
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26935
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 21409 0 0 0 103948 66 0 0 25 0 1 0 544054178 87977984 20751 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21479 20751 603 41 0 21438 0
vsize: 85916
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26935
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 21790 0 0 0 104946 68 0 0 25 0 1 0 544054178 89567232 21132 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21867 21132 603 41 0 21826 0
vsize: 87468
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26935
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 22210 0 0 0 105944 70 0 0 25 0 1 0 544054178 91279360 21552 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22285 21552 603 41 0 22244 0
vsize: 89140
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26935
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 22536 0 0 0 106943 70 0 0 25 0 1 0 544054178 92602368 21878 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22608 21878 603 41 0 22567 0
vsize: 90432
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26935
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 22833 0 0 0 107942 71 0 0 25 0 1 0 544054178 94318592 22175 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23027 22175 603 41 0 22986 0
vsize: 92108
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26935
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 23139 0 0 0 108942 73 0 0 25 0 1 0 544054178 95645696 22481 4294967295 134512640 134672761 3221224624 3221223824 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23351 22481 603 41 0 23310 0
vsize: 93404
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26935
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 23460 0 0 0 109941 73 0 0 25 0 1 0 544054178 96972800 22802 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23675 22802 603 41 0 23634 0
vsize: 94700
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26935
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 23749 0 0 0 110941 74 0 0 25 0 1 0 544054178 98168832 23091 4294967295 134512640 134672761 3221224624 3221223728 134560492 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23967 23091 603 41 0 23926 0
vsize: 95868
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26935
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 24055 0 0 0 111940 74 0 0 25 0 1 0 544054178 99360768 23397 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24258 23397 603 41 0 24217 0
vsize: 97032
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26935
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 24224 0 0 0 112940 75 0 0 25 0 1 0 544054178 100028416 23566 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24421 23566 603 41 0 24380 0
vsize: 97684
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26935
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 24399 0 0 0 113939 76 0 0 25 0 1 0 544054178 100700160 23741 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24585 23741 603 41 0 24544 0
vsize: 98340
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26935
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 24561 0 0 0 114939 76 0 0 25 0 1 0 544054178 101376000 23903 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24750 23903 603 41 0 24709 0
vsize: 99000
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26935
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 24676 0 0 0 115939 76 0 0 25 0 1 0 544054178 101916672 24018 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24882 24018 603 41 0 24841 0
vsize: 99528
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26935
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 24678 0 0 0 116939 76 0 0 25 0 1 0 544054178 101916672 24020 4294967295 134512640 134672761 3221224624 3221223624 1075350544 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24882 24020 603 41 0 24841 0
vsize: 99528
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26935
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 24678 0 0 0 117939 76 0 0 25 0 1 0 544054178 101916672 24020 4294967295 134512640 134672761 3221224624 3221223728 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24882 24020 603 41 0 24841 0
vsize: 99528
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26935
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 24678 0 0 0 118940 76 0 0 25 0 1 0 544054178 101916672 24020 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24882 24020 603 41 0 24841 0
vsize: 99528
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26935
Raw data (stat): 26927 (minisat+) R 26926 20024 20023 0 -1 0 24678 0 0 0 119940 76 0 0 25 0 1 0 544054178 101916672 24020 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24882 24020 603 41 0 24841 0
vsize: 99528
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 26935
Raw data (stat): 26927 (minisat+) Z 26926 20024 20023 0 -1 12 24681 0 0 0 119940 81 0 0 25 0 1 0 544054178 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.1
CPU time (s): 1200.22
CPU user time (s): 1199.4
CPU system time (s): 0.812876
CPU usage (%): 100.01
Max. virtual memory (Kb): 99528
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####