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/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-ran14x18.opb
MD5SUM	a7baaeaa26a0026c630e11c495604909
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1091178
Optimality of the best value was proved	NO
Number of terms in the objective function	5292
Biggest coefficient in the objective function	5242880
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	1421968313
Number of bits of the sum of numbers in the objective function	31
Biggest number in a constraint	5242880
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	1421968313
Number of bits of the biggest sum of numbers	31
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.08
Number of variables	5292
Total number of constraints	284
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	284
Minimum length of a constraint	21
Maximum length of a constraint	360
Trace number 31270

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-05-25 23:39:31 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22669 boxname=wulflinc2 idbench=1485 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  a7baaeaa26a0026c630e11c495604909  /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-ran14x18.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-ran14x18.opb
IDLAUNCH: 22669
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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.191
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:        750712 kB
Buffers:         33128 kB
Cached:         230772 kB
SwapCached:        552 kB
Active:          31656 kB
Inactive:       234500 kB
HighTotal:      131008 kB
HighFree:        56420 kB
LowTotal:       903652 kB
LowFree:        694292 kB
SwapTotal:     2097136 kB
SwapFree:      2095844 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5588 kB
Slab:            12108 kB
Committed_AS:    71788 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-26 00:00:01 (client local time) WITH STATUS 152 IN 1229.88 SECONDS
stats: 22669 7 1229.88 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 316 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 314]---> Adder-cost: 386   maxlim: 47470   bits: 16/16
c ---[ 312]---> Adder-cost: 386   maxlim: 47726   bits: 16/16
c ---[ 310]---> Adder-cost: 386   maxlim: 47342   bits: 16/16
c ---[ 308]---> Adder-cost: 388   maxlim: 58222   bits: 16/16
c ---[ 306]---> Adder-cost: 386   maxlim: 47342   bits: 16/16
c ---[ 304]---> Adder-cost: 386   maxlim: 46830   bits: 16/16
c ---[ 302]---> Adder-cost: 386   maxlim: 47086   bits: 16/16
c ---[ 300]---> Adder-cost: 372   maxlim: 32494   bits: 16/15
c ---[ 298]---> Adder-cost: 386   maxlim: 46702   bits: 16/16
c ---[ 296]---> Adder-cost: 386   maxlim: 46958   bits: 16/16
c ---[ 294]---> Adder-cost: 372   maxlim: 32494   bits: 16/15
c ---[ 292]---> Adder-cost: 386   maxlim: 48110   bits: 16/16
c ---[ 290]---> Adder-cost: 386   maxlim: 47982   bits: 16/16
c ---[ 288]---> Adder-cost: 388   maxlim: 57582   bits: 16/16
c ---[ 286]---> Adder-cost: 260   maxlim: 13554   bits: 14/14
c ---[ 284]---> Adder-cost: 286   maxlim: 26994   bits: 15/15
c ---[ 282]---> Adder-cost: 260   maxlim: 13426   bits: 14/14
c ---[ 280]---> Adder-cost: 310   maxlim: 50930   bits: 16/16
c ---[ 278]---> Adder-cost: 286   maxlim: 26866   bits: 15/15
c ---[ 276]---> Adder-cost: 310   maxlim: 50418   bits: 16/16
c ---[ 274]---> Adder-cost: 312   maxlim: 57202   bits: 16/16
c ---[ 272]---> Adder-cost: 312   maxlim: 55666   bits: 16/16
c ---[ 270]---> Adder-cost: 286   maxlim: 27250   bits: 15/15
c ---[ 268]---> Adder-cost: 286   maxlim: 27634   bits: 15/15
c ---[ 266]---> Adder-cost: 310   maxlim: 50546   bits: 16/16
c ---[ 264]---> Adder-cost: 286   maxlim: 27250   bits: 15/15
c ---[ 262]---> Adder-cost: 310   maxlim: 50674   bits: 16/16
c ---[ 260]---> Adder-cost: 260   maxlim: 13810   bits: 14/14
c ---[ 258]---> Adder-cost: 312   maxlim: 56946   bits: 16/16
c ---[ 256]---> Adder-cost: 286   maxlim: 26994   bits: 15/15
c ---[ 254]---> Adder-cost: 310   maxlim: 50674   bits: 16/16
c ---[ 252]---> Adder-cost: 286   maxlim: 27506   bits: 15/15
c ---[ 251]---> BDD-cost:   12
c ---[ 250]---> BDD-cost:   15
c ---[ 249]---> BDD-cost:   13
c ---[ 248]---> BDD-cost:   13
c ---[ 247]---> BDD-cost:   16
c ---[ 246]---> BDD-cost:   14
c ---[ 245]---> BDD-cost:   16
c ---[ 244]---> BDD-cost:   17
c ---[ 243]---> BDD-cost:   17
c ---[ 242]---> BDD-cost:   15
c ---[ 241]---> BDD-cost:   12
c ---[ 240]---> BDD-cost:   12
c ---[ 239]---> BDD-cost:   14
c ---[ 238]---> BDD-cost:   16
c ---[ 237]---> BDD-cost:   14
c ---[ 236]---> BDD-cost:   14
c ---[ 235]---> BDD-cost:   14
c ---[ 234]---> BDD-cost:   11
c ---[ 233]---> BDD-cost:   14
c ---[ 232]---> BDD-cost:   14
c ---[ 231]---> BDD-cost:   14
c ---[ 230]---> BDD-cost:   15
c ---[ 229]---> BDD-cost:   13
c ---[ 228]---> BDD-cost:   14
c ---[ 227]---> BDD-cost:   14
c ---[ 226]---> BDD-cost:   14
c ---[ 225]---> BDD-cost:   14
c ---[ 224]---> BDD-cost:   14
c ---[ 223]---> BDD-cost:   14
c ---[ 222]---> BDD-cost:   14
c ---[ 221]---> BDD-cost:   12
c ---[ 220]---> BDD-cost:   12
c ---[ 219]---> BDD-cost:   15
c ---[ 218]---> BDD-cost:   13
c ---[ 217]---> BDD-cost:   15
c ---[ 216]---> BDD-cost:   17
c ---[ 215]---> BDD-cost:   13
c ---[ 214]---> BDD-cost:   11
c ---[ 213]---> BDD-cost:   13
c ---[ 212]---> BDD-cost:   15
c ---[ 211]---> BDD-cost:   13
c ---[ 210]---> BDD-cost:   15
c ---[ 209]---> BDD-cost:   13
c ---[ 208]---> BDD-cost:   13
c ---[ 207]---> BDD-cost:   14
c ---[ 206]---> BDD-cost:   13
c ---[ 205]---> BDD-cost:   17
c ---[ 204]---> BDD-cost:   13
c ---[ 203]---> BDD-cost:   13
c ---[ 202]---> BDD-cost:   15
c ---[ 201]---> BDD-cost:   12
c ---[ 200]---> BDD-cost:   12
c ---[ 199]---> BDD-cost:   15
c ---[ 198]---> BDD-cost:   17
c ---[ 197]---> BDD-cost:   15
c ---[ 196]---> BDD-cost:   17
c ---[ 195]---> BDD-cost:   11
c ---[ 194]---> BDD-cost:   17
c ---[ 193]---> BDD-cost:   17
c ---[ 192]---> BDD-cost:   15
c ---[ 191]---> BDD-cost:   17
c ---[ 190]---> BDD-cost:   15
c ---[ 189]---> BDD-cost:   13
c ---[ 188]---> BDD-cost:   17
c ---[ 187]---> BDD-cost:   14
c ---[ 186]---> BDD-cost:   17
c ---[ 185]---> BDD-cost:   17
c ---[ 184]---> BDD-cost:   17
c ---[ 183]---> BDD-cost:   15
c ---[ 182]---> BDD-cost:   15
c ---[ 181]---> BDD-cost:   12
c ---[ 180]---> BDD-cost:   12
c ---[ 179]---> BDD-cost:   15
c ---[ 178]---> BDD-cost:   17
c ---[ 177]---> BDD-cost:   15
c ---[ 176]---> BDD-cost:   15
c ---[ 175]---> BDD-cost:   11
c ---[ 174]---> BDD-cost:   19
c ---[ 173]---> BDD-cost:   15
c ---[ 172]---> BDD-cost:   12
c ---[ 171]---> BDD-cost:   15
c ---[ 170]---> BDD-cost:   15
c ---[ 169]---> BDD-cost:   13
c ---[ 168]---> BDD-cost:   16
c ---[ 167]---> BDD-cost:   14
c ---[ 166]---> BDD-cost:   16
c ---[ 165]---> BDD-cost:   19
c ---[ 164]---> BDD-cost:   18
c ---[ 163]---> BDD-cost:   15
c ---[ 162]---> BDD-cost:   12
c ---[ 161]---> BDD-cost:   12
c ---[ 160]---> BDD-cost:   12
c ---[ 159]---> BDD-cost:   15
c ---[ 158]---> BDD-cost:   17
c ---[ 157]---> BDD-cost:   15
c ---[ 156]---> BDD-cost:   15
c ---[ 155]---> BDD-cost:   11
c ---[ 154]---> BDD-cost:   16
c ---[ 153]---> BDD-cost:   15
c ---[ 152]---> BDD-cost:   15
c ---[ 151]---> BDD-cost:   15
c ---[ 150]---> BDD-cost:   15
c ---[ 149]---> BDD-cost:   13
c ---[ 148]---> BDD-cost:   16
c ---[ 147]---> BDD-cost:   14
c ---[ 146]---> BDD-cost:   16
c ---[ 145]---> BDD-cost:   16
c ---[ 144]---> BDD-cost:   16
c ---[ 143]---> BDD-cost:   15
c ---[ 142]---> BDD-cost:   12
c ---[ 141]---> BDD-cost:   12
c ---[ 140]---> BDD-cost:   15
c ---[ 139]---> BDD-cost:   17
c ---[ 138]---> BDD-cost:   17
c ---[ 137]---> BDD-cost:   17
c ---[ 136]---> BDD-cost:   15
c ---[ 135]---> BDD-cost:   15
c ---[ 134]---> BDD-cost:   11
c ---[ 133]---> BDD-cost:   19
c ---[ 132]---> BDD-cost:   15
c ---[ 131]---> BDD-cost:   15
c ---[ 130]---> BDD-cost:   15
c ---[ 129]---> BDD-cost:   13
c ---[ 128]---> BDD-cost:   16
c ---[ 127]---> BDD-cost:   15
c ---[ 126]---> BDD-cost:   14
c ---[ 125]---> BDD-cost:   16
c ---[ 124]---> BDD-cost:   19
c ---[ 123]---> BDD-cost:   19
c ---[ 122]---> BDD-cost:   15
c ---[ 121]---> BDD-cost:   12
c ---[ 120]---> BDD-cost:   12
c ---[ 119]---> BDD-cost:   15
c ---[ 118]---> BDD-cost:   17
c ---[ 117]---> BDD-cost:   15
c ---[ 116]---> BDD-cost:   17
c ---[ 115]---> BDD-cost:   15
c ---[ 114]---> BDD-cost:   11
c ---[ 113]---> BDD-cost:   16
c ---[ 112]---> BDD-cost:   15
c ---[ 111]---> BDD-cost:   15
c ---[ 110]---> BDD-cost:   15
c ---[ 109]---> BDD-cost:   13
c ---[ 108]---> BDD-cost:   16
c ---[ 107]---> BDD-cost:   14
c ---[ 106]---> BDD-cost:   16
c ---[ 105]---> BDD-cost:   11
c ---[ 104]---> BDD-cost:   16
c ---[ 103]---> BDD-cost:   16
c ---[ 102]---> BDD-cost:   15
c ---[ 101]---> BDD-cost:   12
c ---[ 100]---> BDD-cost:   12
c ---[  99]---> BDD-cost:   15
c ---[  98]---> BDD-cost:   17
c ---[  97]---> BDD-cost:   15
c ---[  96]---> BDD-cost:   15
c ---[  95]---> BDD-cost:   11
c ---[  94]---> BDD-cost:   17
c ---[  93]---> BDD-cost:   16
c ---[  92]---> BDD-cost:   15
c ---[  91]---> BDD-cost:   15
c ---[  90]---> BDD-cost:   15
c ---[  89]---> BDD-cost:   13
c ---[  88]---> BDD-cost:   16
c ---[  87]---> BDD-cost:   14
c ---[  86]---> BDD-cost:   16
c ---[  85]---> BDD-cost:   16
c ---[  84]---> BDD-cost:   16
c ---[  83]---> BDD-cost:   15
c ---[  82]---> BDD-cost:   15
c ---[  81]---> BDD-cost:   12
c ---[  80]---> BDD-cost:   17
c ---[  79]---> BDD-cost:   15
c ---[  78]---> BDD-cost:   13
c ---[  77]---> BDD-cost:   16
c ---[  76]---> BDD-cost:   15
c ---[  75]---> BDD-cost:   14
c ---[  74]---> BDD-cost:   17
c ---[  73]---> BDD-cost:   17
c ---[  72]---> BDD-cost:   17
c ---[  71]---> BDD-cost:   15
c ---[  70]---> BDD-cost:   12
c ---[  69]---> BDD-cost:   12
c ---[  68]---> BDD-cost:   15
c ---[  67]---> BDD-cost:   17
c ---[  66]---> BDD-cost:   15
c ---[  65]---> BDD-cost:   15
c ---[  64]---> BDD-cost:   15
c ---[  63]---> BDD-cost:   11
c ---[  62]---> BDD-cost:   14
c ---[  61]---> BDD-cost:   15
c ---[  60]---> BDD-cost:   15
c ---[  59]---> BDD-cost:   15
c ---[  58]---> BDD-cost:   13
c ---[  57]---> BDD-cost:   16
c ---[  56]---> BDD-cost:   14
c ---[  55]---> BDD-cost:   16
c ---[  54]---> BDD-cost:   11
c ---[  53]---> BDD-cost:   14
c ---[  52]---> BDD-cost:   14
c ---[  51]---> BDD-cost:   15
c ---[  50]---> BDD-cost:   12
c ---[  49]---> BDD-cost:   12
c ---[  48]---> BDD-cost:   14
c ---[  47]---> BDD-cost:   14
c ---[  46]---> BDD-cost:   14
c ---[  45]---> BDD-cost:   14
c ---[  44]---> BDD-cost:   11
c ---[  43]---> BDD-cost:   17
c ---[  42]---> BDD-cost:   14
c ---[  41]---> BDD-cost:   14
c ---[  40]---> BDD-cost:   14
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   13
c ---[  37]---> BDD-cost:   14
c ---[  36]---> BDD-cost:   14
c ---[  35]---> BDD-cost:   14
c ---[  34]---> BDD-cost:   14
c ---[  33]---> BDD-cost:   14
c ---[  32]---> BDD-cost:   15
c ---[  31]---> BDD-cost:   14
c ---[  30]---> BDD-cost:   12
c ---[  29]---> BDD-cost:   12
c ---[  28]---> BDD-cost:   15
c ---[  27]---> BDD-cost:   17
c ---[  26]---> BDD-cost:   15
c ---[  25]---> BDD-cost:   15
c ---[  24]---> BDD-cost:   11
c ---[  23]---> BDD-cost:   17
c ---[  22]---> BDD-cost:   15
c ---[  21]---> BDD-cost:   15
c ---[  20]---> BDD-cost:   15
c ---[  19]---> BDD-cost:   15
c ---[  18]---> BDD-cost:   13
c ---[  17]---> BDD-cost:   16
c ---[  16]---> BDD-cost:   14
c ---[  15]---> BDD-cost:   16
c ---[  14]---> BDD-cost:   17
c ---[  13]---> BDD-cost:   17
c ---[  12]---> BDD-cost:   15
c ---[  11]---> BDD-cost:   12
c ---[  10]---> BDD-cost:   15
c ---[   9]---> BDD-cost:   12
c ---[   8]---> BDD-cost:   15
c ---[   7]---> BDD-cost:   17
c ---[   6]---> BDD-cost:   15
c ---[   5]---> BDD-cost:   15
c ---[   4]---> BDD-cost:   11
c ---[   3]---> BDD-cost:   17
c ---[   2]---> BDD-cost:   15
c ---[   1]---> BDD-cost:   15
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   76494   265887 |   25498       0        0     nan |  0.000 % |
c |       100 |   76494   265887 |   28047     100      309     3.1 | 19.261 % |
c |       250 |   76198   264881 |   30852     212      675     3.2 | 19.559 % |
c |       475 |   76079   264494 |   33937     423     1362     3.2 | 19.683 % |
c |       812 |   75642   263011 |   37331     709     2311     3.3 | 20.121 % |
c |      1318 |   75345   262018 |   41064    1185     3870     3.3 | 20.431 % |
c |      2077 |   75042   260989 |   45171    1907     6270     3.3 | 20.729 % |
c |      3216 |   74558   259349 |   49688    2990    10323     3.5 | 21.212 % |
c |      4924 |   74342   258613 |   54657    4678    17235     3.7 | 21.426 % |
c |      7486 |   74267   258370 |   60122    7229    40363     5.6 | 21.499 % |
c |     11330 |   74032   257569 |   66135   11046    75972     6.9 | 21.741 % |
c |     17096 |   73933   257226 |   72748   16796   132604     7.9 | 21.825 % |
c |     25745 |   73786   256727 |   80023   25428   204683     8.0 | 21.982 % |
c |     38720 |   73759   256638 |   88026   38400   801127    20.9 | 22.010 % |
c |     58183 |   73700   256443 |   96828   57853  1460313    25.2 | 22.067 % |
c |     87375 |   73273   254982 |  106511   86985  1951309    22.4 | 22.516 % |
c |    131164 |   73124   254477 |  117162   42552   521709    12.3 | 22.679 % |
c |    196850 |   72914   253747 |  128878  108213  4215539    39.0 | 22.904 % |
c |    295376 |   72764   253241 |  141766   84108 13534946   160.9 | 23.062 % |
c |    443166 |   72588   252661 |  155943  102246  3394701    33.2 | 23.242 % |
c ==============================================================================
c [1mFound solution: 5467074[0m
c ---[   0]---> Adder-cost: 10447   maxlim: 3522551   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    460023 |  145618   513567 |   48539  119103  3820988    32.1 | 23.242 % |
c |    460123 |  145618   513567 |   53392   23952   412223    17.2 | 14.692 % |
c |    460274 |  145618   513567 |   58732   24103   413189    17.1 | 14.692 % |
c |    460499 |  145618   513567 |   64605   24328   414327    17.0 | 14.692 % |
c |    460836 |  145618   513567 |   71065   24665   416208    16.9 | 14.692 % |
c |    461342 |  145618   513567 |   78172   25171   419558    16.7 | 14.692 % |
c |    462101 |  145618   513567 |   85989   25930   428983    16.5 | 14.692 % |
c |    463241 |  145618   513567 |   94588   27070   460493    17.0 | 14.692 % |
c |    464950 |  145618   513567 |  104047   28779   500695    17.4 | 14.692 % |
c |    467512 |  145618   513567 |  114452   31341   521748    16.6 | 14.692 % |
c |    471356 |  145593   513486 |  125897   35182   555697    15.8 | 14.710 % |
c |    477122 |  145584   513457 |  138487   40947   616878    15.1 | 14.717 % |
c |    485771 |  145584   513457 |  152336   49596   712992    14.4 | 14.717 % |
c |    498745 |  145543   513324 |  167569   62565   902980    14.4 | 14.745 % |
c |    518207 |  145477   513106 |  184326   82018  1162971    14.2 | 14.791 % |
c |    547400 |  145420   512921 |  202759  111203  1727419    15.5 | 14.830 % |
c ==============================================================================
c [1mFound solution: 5360551[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3629074   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    551206 |  145432   513041 |   48477  115008  1895574    16.5 | 14.830 % |
c |    551306 |  145432   513041 |   53324   28345   426298    15.0 | 14.856 % |
c |    551456 |  145432   513041 |   58657   28495   427062    15.0 | 14.856 % |
c |    551682 |  145423   513012 |   64522   28720   428255    14.9 | 14.864 % |
c |    552019 |  145423   513012 |   70975   29057   430615    14.8 | 14.864 % |
c |    552525 |  145423   513012 |   78072   29563   434142    14.7 | 14.864 % |
c |    553284 |  145423   513012 |   85879   30322   443274    14.6 | 14.864 % |
c |    554423 |  145423   513012 |   94467   31461   451990    14.4 | 14.864 % |
c |    556131 |  145423   513012 |  103914   33169   465384    14.0 | 14.864 % |
c |    558693 |  145423   513012 |  114306   35731   486963    13.6 | 14.864 % |
c |    562537 |  145423   513012 |  125736   39575   524400    13.3 | 14.864 % |
c |    568303 |  145414   512983 |  138310   45340   583510    12.9 | 14.871 % |
c |    576952 |  145397   512922 |  152141   53986   720187    13.3 | 14.878 % |
c |    589926 |  145374   512847 |  167355   66957   876759    13.1 | 14.892 % |
c |    609387 |  145356   512789 |  184091   86416  1220556    14.1 | 14.906 % |
c |    638580 |  145356   512789 |  202500  115609  3504893    30.3 | 14.906 % |
c ==============================================================================
c [1mFound solution: 5340590[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3649035   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    675869 |  145303   512698 |   48434  152886  5353930    35.0 | 14.906 % |
c |    675969 |  145303   512698 |   53277   29691   545649    18.4 | 14.969 % |
c |    676120 |  145303   512698 |   58605   29842   546502    18.3 | 14.969 % |
c |    676345 |  145303   512698 |   64465   30067   547830    18.2 | 14.969 % |
c |    676682 |  145303   512698 |   70912   30404   549685    18.1 | 14.969 % |
c |    677188 |  145303   512698 |   78003   30910   552898    17.9 | 14.969 % |
c |    677947 |  145294   512669 |   85803   31668   557313    17.6 | 14.976 % |
c |    679089 |  145294   512669 |   94384   32810   564777    17.2 | 14.976 % |
c |    680797 |  145294   512669 |  103822   34518   577841    16.7 | 14.976 % |
c |    683360 |  145294   512669 |  114204   37081   598635    16.1 | 14.976 % |
c |    687204 |  145294   512669 |  125625   40925   642603    15.7 | 14.976 % |
c |    692970 |  145287   512646 |  138187   46689   692573    14.8 | 14.979 % |
c |    701620 |  145287   512646 |  152006   55339   804799    14.5 | 14.979 % |
c |    714594 |  145281   512626 |  167207   68311   949293    13.9 | 14.983 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 18896 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### 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.92 0.97 0.92 2/54 18892
Raw data (stat): 18892 (runsolver) R 18891 31399 31398 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 784689388 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 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+9.99926 s]
Raw data (loadavg): 0.94 0.97 0.92 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0003 s]
Raw data (loadavg): 0.95 0.97 0.92 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.001 s]
Raw data (loadavg): 0.95 0.97 0.92 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0014 s]
Raw data (loadavg): 0.96 0.97 0.92 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0024 s]
Raw data (loadavg): 0.97 0.97 0.92 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0021 s]
Raw data (loadavg): 0.97 0.97 0.92 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0025 s]
Raw data (loadavg): 0.97 0.97 0.92 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0026 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0032 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.003 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.004 s]
Raw data (loadavg): 1.06 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.004 s]
Raw data (loadavg): 1.05 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.005 s]
Raw data (loadavg): 1.04 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.005 s]
Raw data (loadavg): 1.04 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.004 s]
Raw data (loadavg): 1.03 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.005 s]
Raw data (loadavg): 1.02 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.005 s]
Raw data (loadavg): 1.02 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.005 s]
Raw data (loadavg): 1.02 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.006 s]
Raw data (loadavg): 1.01 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.006 s]
Raw data (loadavg): 1.01 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.006 s]
Raw data (loadavg): 1.01 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.006 s]
Raw data (loadavg): 1.01 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.008 s]
Raw data (loadavg): 1.01 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.008 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.009 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.009 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.009 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.009 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.011 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.011 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.011 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.011 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.011 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.012 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.011 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.011 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.012 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.012 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.013 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.013 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.012 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.012 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.012 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.013 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.013 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.016 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.016 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.017 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.017 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.034 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.053 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.054 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.053 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.053 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.054 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.054 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.054 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.054 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.055 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.054 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.055 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.056 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.055 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.056 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.056 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.056 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.057 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.056 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.057 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.057 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.057 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.058 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.058 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.058 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.057 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.058 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.059 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.058 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.059 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.059 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.06 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.06 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.061 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.062 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.061 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.062 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.063 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.063 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.063 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.064 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.064 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.06 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.7 s]
Raw data (loadavg): 1.00 0.99 0.93 1/53 18896
Raw data (stat): 18892 (minisat+_script) S 18891 31399 31398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784689388 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.7
CPU time (s): 1229.88
CPU user time (s): 1229.04
CPU system time (s): 0.832873
CPU usage (%): 100.014
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####