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/plato.asu.edu/pub/fctp/normalized-mps-v2-20-10-ran8x32.opb
MD5SUM	14da1db0c6acfbdddee3af5ad3788f2d
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	12128256
Optimality of the best value was proved	NO
Number of terms in the objective function	7936
Biggest coefficient in the objective function	5368709120
Number of bits for the biggest coefficient in the objective function	33
Sum of the numbers in the objective function	1548380176990
Number of bits of the sum of numbers in the objective function	41
Biggest number in a constraint	5368709120
Number of bits of the biggest number in a constraint	33
Biggest sum of numbers in a constraint	1548380176990
Number of bits of the biggest sum of numbers	41
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1231.81
Number of variables	7936
Total number of constraints	296
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	296
Minimum length of a constraint	31
Maximum length of a constraint	960
Trace number 30901

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-05-25 20:37:45 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22290 boxname=wulflinc6 idbench=1106 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  14da1db0c6acfbdddee3af5ad3788f2d  /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-20-10-ran8x32.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-20-10-ran8x32.opb
IDLAUNCH: 22290
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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.042
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:        895576 kB
Buffers:         28964 kB
Cached:          85952 kB
SwapCached:        412 kB
Active:          23228 kB
Inactive:        94004 kB
HighTotal:      131008 kB
HighFree:        54544 kB
LowTotal:       903652 kB
LowFree:        841032 kB
SwapTotal:     2097136 kB
SwapFree:      2096036 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5696 kB
Slab:            16272 kB
Committed_AS:    63736 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 20:58:15 (client local time) WITH STATUS 152 IN 1229.88 SECONDS
stats: 22290 7 1229.88 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 336 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 334]---> Adder-cost: 832   maxlim: 367584   bits: 19/19
c ---[ 332]---> Adder-cost: 856   maxlim: 559072   bits: 20/20
c ---[ 330]---> Adder-cost: 856   maxlim: 540640   bits: 20/20
c ---[ 328]---> Adder-cost: 856   maxlim: 571360   bits: 20/20
c ---[ 326]---> Adder-cost: 856   maxlim: 575456   bits: 20/20
c ---[ 324]---> Adder-cost: 856   maxlim: 575456   bits: 20/20
c ---[ 322]---> Adder-cost: 856   maxlim: 563168   bits: 20/20
c ---[ 320]---> Adder-cost: 856   maxlim: 517088   bits: 20/19
c ---[ 318]---> Sorter-cost: 1455     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 316]---> Sorter-cost: 1723     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 314]---> Sorter-cost: 1589     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 312]---> Sorter-cost: 2063     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 310]---> Sorter-cost: 1927     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 308]---> Sorter-cost: 1723     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 306]---> Sorter-cost: 1723     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 304]---> Sorter-cost: 1589     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 302]---> Sorter-cost: 1723     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 300]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 298]---> Sorter-cost: 1927     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 296]---> Sorter-cost: 1589     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 294]---> Sorter-cost: 2063     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 292]---> Sorter-cost: 1455     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 290]---> Sorter-cost: 1589     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 288]---> Sorter-cost: 1589     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 286]---> Sorter-cost: 1927     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 284]---> Sorter-cost: 1723     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 282]---> Sorter-cost: 1455     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 280]---> Sorter-cost: 1589     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 278]---> Sorter-cost: 1589     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 276]---> Sorter-cost: 2063     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 274]---> Sorter-cost: 1723     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 272]---> Sorter-cost: 1455     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 270]---> Sorter-cost: 1723     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 268]---> Sorter-cost: 1723     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 266]---> Sorter-cost: 1927     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 264]---> Sorter-cost: 1589     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 262]---> Sorter-cost: 1455     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 260]---> Sorter-cost: 1927     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 258]---> Sorter-cost: 1723     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 256]---> Sorter-cost: 1723     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 255]---> BDD-cost:   13
c ---[ 254]---> BDD-cost:   18
c ---[ 253]---> BDD-cost:   15
c ---[ 252]---> BDD-cost:   19
c ---[ 251]---> BDD-cost:   16
c ---[ 250]---> BDD-cost:   13
c ---[ 249]---> BDD-cost:   19
c ---[ 248]---> BDD-cost:   17
c ---[ 247]---> BDD-cost:   18
c ---[ 246]---> BDD-cost:   15
c ---[ 245]---> BDD-cost:   19
c ---[ 244]---> BDD-cost:   19
c ---[ 243]---> BDD-cost:   18
c ---[ 242]---> BDD-cost:   18
c ---[ 241]---> BDD-cost:   15
c ---[ 240]---> BDD-cost:   16
c ---[ 239]---> BDD-cost:   17
c ---[ 238]---> BDD-cost:   12
c ---[ 237]---> BDD-cost:   19
c ---[ 236]---> BDD-cost:   14
c ---[ 235]---> BDD-cost:   14
c ---[ 234]---> BDD-cost:   16
c ---[ 233]---> BDD-cost:   16
c ---[ 232]---> BDD-cost:   20
c ---[ 231]---> BDD-cost:   18
c ---[ 230]---> BDD-cost:   18
c ---[ 229]---> BDD-cost:   13
c ---[ 228]---> BDD-cost:   15
c ---[ 227]---> BDD-cost:   15
c ---[ 226]---> BDD-cost:   21
c ---[ 225]---> BDD-cost:   18
c ---[ 224]---> BDD-cost:   18
c ---[ 223]---> BDD-cost:   18
c ---[ 222]---> BDD-cost:   13
c ---[ 221]---> BDD-cost:   18
c ---[ 220]---> BDD-cost:   18
c ---[ 219]---> BDD-cost:   20
c ---[ 218]---> BDD-cost:   14
c ---[ 217]---> BDD-cost:   19
c ---[ 216]---> BDD-cost:   16
c ---[ 215]---> BDD-cost:   13
c ---[ 214]---> BDD-cost:   19
c ---[ 213]---> BDD-cost:   17
c ---[ 212]---> BDD-cost:   18
c ---[ 211]---> BDD-cost:   15
c ---[ 210]---> BDD-cost:   20
c ---[ 209]---> BDD-cost:   15
c ---[ 208]---> BDD-cost:   19
c ---[ 207]---> BDD-cost:   18
c ---[ 206]---> BDD-cost:   15
c ---[ 205]---> BDD-cost:   16
c ---[ 204]---> BDD-cost:   17
c ---[ 203]---> BDD-cost:   12
c ---[ 202]---> BDD-cost:   19
c ---[ 201]---> BDD-cost:   14
c ---[ 200]---> BDD-cost:   14
c ---[ 199]---> BDD-cost:   16
c ---[ 198]---> BDD-cost:   16
c ---[ 197]---> BDD-cost:   16
c ---[ 196]---> BDD-cost:   20
c ---[ 195]---> BDD-cost:   18
c ---[ 194]---> BDD-cost:   13
c ---[ 193]---> BDD-cost:   15
c ---[ 192]---> BDD-cost:   15
c ---[ 191]---> BDD-cost:   21
c ---[ 190]---> BDD-cost:   18
c ---[ 189]---> BDD-cost:   18
c ---[ 188]---> BDD-cost:   18
c ---[ 187]---> BDD-cost:   17
c ---[ 186]---> BDD-cost:   13
c ---[ 185]---> BDD-cost:   18
c ---[ 184]---> BDD-cost:   20
c ---[ 183]---> BDD-cost:   14
c ---[ 182]---> BDD-cost:   19
c ---[ 181]---> BDD-cost:   16
c ---[ 180]---> BDD-cost:   13
c ---[ 179]---> BDD-cost:   19
c ---[ 178]---> BDD-cost:   17
c ---[ 177]---> BDD-cost:   18
c ---[ 176]---> BDD-cost:   12
c ---[ 175]---> BDD-cost:   15
c ---[ 174]---> BDD-cost:   20
c ---[ 173]---> BDD-cost:   19
c ---[ 172]---> BDD-cost:   18
c ---[ 171]---> BDD-cost:   15
c ---[ 170]---> BDD-cost:   16
c ---[ 169]---> BDD-cost:   17
c ---[ 168]---> BDD-cost:   12
c ---[ 167]---> BDD-cost:   19
c ---[ 166]---> BDD-cost:   14
c ---[ 165]---> BDD-cost:   18
c ---[ 164]---> BDD-cost:   14
c ---[ 163]---> BDD-cost:   16
c ---[ 162]---> BDD-cost:   16
c ---[ 161]---> BDD-cost:   20
c ---[ 160]---> BDD-cost:   18
c ---[ 159]---> BDD-cost:   13
c ---[ 158]---> BDD-cost:   15
c ---[ 157]---> BDD-cost:   15
c ---[ 156]---> BDD-cost:   21
c ---[ 155]---> BDD-cost:   18
c ---[ 154]---> BDD-cost:   14
c ---[ 153]---> BDD-cost:   18
c ---[ 152]---> BDD-cost:   18
c ---[ 151]---> BDD-cost:   13
c ---[ 150]---> BDD-cost:   18
c ---[ 149]---> BDD-cost:   20
c ---[ 148]---> BDD-cost:   14
c ---[ 147]---> BDD-cost:   19
c ---[ 146]---> BDD-cost:   16
c ---[ 145]---> BDD-cost:   13
c ---[ 144]---> BDD-cost:   19
c ---[ 143]---> BDD-cost:   18
c ---[ 142]---> BDD-cost:   14
c ---[ 141]---> BDD-cost:   17
c ---[ 140]---> BDD-cost:   18
c ---[ 139]---> BDD-cost:   15
c ---[ 138]---> BDD-cost:   22
c ---[ 137]---> BDD-cost:   19
c ---[ 136]---> BDD-cost:   18
c ---[ 135]---> BDD-cost:   15
c ---[ 134]---> BDD-cost:   16
c ---[ 133]---> BDD-cost:   17
c ---[ 132]---> BDD-cost:   12
c ---[ 131]---> BDD-cost:   16
c ---[ 130]---> BDD-cost:   19
c ---[ 129]---> BDD-cost:   14
c ---[ 128]---> BDD-cost:   14
c ---[ 127]---> BDD-cost:   16
c ---[ 126]---> BDD-cost:   16
c ---[ 125]---> BDD-cost:   20
c ---[ 124]---> BDD-cost:   18
c ---[ 123]---> BDD-cost:   13
c ---[ 122]---> BDD-cost:   15
c ---[ 121]---> BDD-cost:   15
c ---[ 120]---> BDD-cost:   16
c ---[ 119]---> BDD-cost:   21
c ---[ 118]---> BDD-cost:   18
c ---[ 117]---> BDD-cost:   18
c ---[ 116]---> BDD-cost:   18
c ---[ 115]---> BDD-cost:   13
c ---[ 114]---> BDD-cost:   18
c ---[ 113]---> BDD-cost:   20
c ---[ 112]---> BDD-cost:   14
c ---[ 111]---> BDD-cost:   19
c ---[ 110]---> BDD-cost:   16
c ---[ 109]---> BDD-cost:   18
c ---[ 108]---> BDD-cost:   13
c ---[ 107]---> BDD-cost:   19
c ---[ 106]---> BDD-cost:   17
c ---[ 105]---> BDD-cost:   18
c ---[ 104]---> BDD-cost:   15
c ---[ 103]---> BDD-cost:   22
c ---[ 102]---> BDD-cost:   19
c ---[ 101]---> BDD-cost:   18
c ---[ 100]---> BDD-cost:   15
c ---[  99]---> BDD-cost:   16
c ---[  98]---> BDD-cost:   18
c ---[  97]---> BDD-cost:   17
c ---[  96]---> BDD-cost:   12
c ---[  95]---> BDD-cost:   19
c ---[  94]---> BDD-cost:   14
c ---[  93]---> BDD-cost:   14
c ---[  92]---> BDD-cost:   16
c ---[  91]---> BDD-cost:   16
c ---[  90]---> BDD-cost:   20
c ---[  89]---> BDD-cost:   18
c ---[  88]---> BDD-cost:   13
c ---[  87]---> BDD-cost:   13
c ---[  86]---> BDD-cost:   15
c ---[  85]---> BDD-cost:   15
c ---[  84]---> BDD-cost:   21
c ---[  83]---> BDD-cost:   18
c ---[  82]---> BDD-cost:   18
c ---[  81]---> BDD-cost:   18
c ---[  80]---> BDD-cost:   15
c ---[  79]---> BDD-cost:   15
c ---[  78]---> BDD-cost:   18
c ---[  77]---> BDD-cost:   18
c ---[  76]---> BDD-cost:   14
c ---[  75]---> BDD-cost:   18
c ---[  74]---> BDD-cost:   18
c ---[  73]---> BDD-cost:   13
c ---[  72]---> BDD-cost:   18
c ---[  71]---> BDD-cost:   20
c ---[  70]---> BDD-cost:   14
c ---[  69]---> BDD-cost:   19
c ---[  68]---> BDD-cost:   16
c ---[  67]---> BDD-cost:   13
c ---[  66]---> BDD-cost:   19
c ---[  65]---> BDD-cost:   18
c ---[  64]---> BDD-cost:   17
c ---[  63]---> BDD-cost:   18
c ---[  62]---> BDD-cost:   15
c ---[  61]---> BDD-cost:   22
c ---[  60]---> BDD-cost:   19
c ---[  59]---> BDD-cost:   18
c ---[  58]---> BDD-cost:   15
c ---[  57]---> BDD-cost:   16
c ---[  56]---> BDD-cost:   17
c ---[  55]---> BDD-cost:   12
c ---[  54]---> BDD-cost:   16
c ---[  53]---> BDD-cost:   19
c ---[  52]---> BDD-cost:   14
c ---[  51]---> BDD-cost:   14
c ---[  50]---> BDD-cost:   16
c ---[  49]---> BDD-cost:   16
c ---[  48]---> BDD-cost:   20
c ---[  47]---> BDD-cost:   18
c ---[  46]---> BDD-cost:   13
c ---[  45]---> BDD-cost:   15
c ---[  44]---> BDD-cost:   15
c ---[  43]---> BDD-cost:   13
c ---[  42]---> BDD-cost:   21
c ---[  41]---> BDD-cost:   18
c ---[  40]---> BDD-cost:   18
c ---[  39]---> BDD-cost:   18
c ---[  38]---> BDD-cost:   13
c ---[  37]---> BDD-cost:   18
c ---[  36]---> BDD-cost:   20
c ---[  35]---> BDD-cost:   14
c ---[  34]---> BDD-cost:   19
c ---[  33]---> BDD-cost:   16
c ---[  32]---> BDD-cost:   18
c ---[  31]---> BDD-cost:   13
c ---[  30]---> BDD-cost:   19
c ---[  29]---> BDD-cost:   17
c ---[  28]---> BDD-cost:   18
c ---[  27]---> BDD-cost:   15
c ---[  26]---> BDD-cost:   22
c ---[  25]---> BDD-cost:   19
c ---[  24]---> BDD-cost:   18
c ---[  23]---> BDD-cost:   15
c ---[  22]---> BDD-cost:   16
c ---[  21]---> BDD-cost:   17
c ---[  20]---> BDD-cost:   17
c ---[  19]---> BDD-cost:   12
c ---[  18]---> BDD-cost:   19
c ---[  17]---> BDD-cost:   14
c ---[  16]---> BDD-cost:   14
c ---[  15]---> BDD-cost:   16
c ---[  14]---> BDD-cost:   16
c ---[  13]---> BDD-cost:   20
c ---[  12]---> BDD-cost:   18
c ---[  11]---> BDD-cost:   13
c ---[  10]---> BDD-cost:   18
c ---[   9]---> BDD-cost:   15
c ---[   8]---> BDD-cost:   15
c ---[   7]---> BDD-cost:   21
c ---[   6]---> BDD-cost:   18
c ---[   5]---> BDD-cost:   18
c ---[   4]---> BDD-cost:   18
c ---[   3]---> BDD-cost:   13
c ---[   2]---> BDD-cost:   18
c ---[   1]---> BDD-cost:   19
c ---[   0]---> BDD-cost:   14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  190237   505136 |   63412       0        0     nan |  0.000 % |
c |       100 |  189904   504372 |   69753      72      246     3.4 | 10.202 % |
c |       250 |  189885   504329 |   76728     219      847     3.9 | 10.211 % |
c |       475 |  189629   503747 |   84401     428     1586     3.7 | 10.336 % |
c |       812 |  189509   503470 |   92841     755     2856     3.8 | 10.394 % |
c |      1321 |  189387   503195 |  102125    1252     4752     3.8 | 10.450 % |
c |      2080 |  189275   502940 |  112338    2005     7638     3.8 | 10.504 % |
c |      3219 |  188841   501889 |  123572    3099    12038     3.9 | 10.703 % |
c |      4927 |  188353   500779 |  135929    4745    18757     4.0 | 10.934 % |
c |      7489 |  187765   499426 |  149522    7255    29010     4.0 | 11.216 % |
c |     11335 |  187011   497678 |  164474   11033    44738     4.1 | 11.583 % |
c |     17101 |  185292   493710 |  180921   16648    68374     4.1 | 12.439 % |
c |     25750 |  182723   487779 |  199014   25045   106051     4.2 | 13.729 % |
c |     38724 |  181827   485685 |  218915   37926   453278    12.0 | 14.174 % |
c |     58185 |  178993   479013 |  240806   57050   658476    11.5 | 15.585 % |
c |     87378 |  177827   476122 |  264887   86070  1244613    14.5 | 16.163 % |
c |    131167 |  177370   475003 |  291376  129805  3028228    23.3 | 16.392 % |
c |    196851 |  177290   474807 |  320514  195479  8156029    41.7 | 16.435 % |
c ==============================================================================
c [1mFound solution: 44221936[0m
c ---[   0]---> Adder-cost: 13413   maxlim: 27038830   bits: 26/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    219007 |  271069   809848 |   90356  217634  8947036    41.1 | 16.435 % |
c |    219107 |  271062   809830 |   99391   32383   572989    17.7 | 13.565 % |
c |    219257 |  271012   809714 |  109330   32528   573589    17.6 | 13.588 % |
c |    219482 |  271001   809689 |  120263   32752   574619    17.5 | 13.594 % |
c |    219819 |  270976   809632 |  132290   33088   576027    17.4 | 13.604 % |
c |    220325 |  270976   809632 |  145519   33594   578771    17.2 | 13.604 % |
c |    221084 |  270934   809532 |  160071   34351   582701    17.0 | 13.625 % |
c |    222223 |  270915   809489 |  176078   35489   590596    16.6 | 13.633 % |
c |    223932 |  270809   809242 |  193686   37190   601342    16.2 | 13.679 % |
c |    226494 |  270727   809052 |  213054   39744   623592    15.7 | 13.716 % |
c |    230339 |  270608   808771 |  234360   43580   689318    15.8 | 13.771 % |
c |    236105 |  270449   808401 |  257796   49336   741484    15.0 | 13.843 % |
c |    244754 |  270326   808116 |  283575   57958   829338    14.3 | 13.895 % |
c |    257729 |  270185   807730 |  311933   70911  1231196    17.4 | 13.945 % |
c |    277190 |  269924   807046 |  343126   90327  1608462    17.8 | 14.047 % |
c |    306382 |  269688   806381 |  377439  119477  2818375    23.6 | 14.128 % |
c |    350172 |  269562   806068 |  415183  163248  6008102    36.8 | 14.177 % |
c ==============================================================================
c [1mFound solution: 34566369[0m
c ---[   0]---> Adder-cost: 2   maxlim: 36694397   bits: 27/26
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    393024 |  269505   806224 |   89835  206085  9878021    47.9 | 14.177 % |
c |    393125 |  269505   806224 |   98818   35700  1503721    42.1 | 14.243 % |
c |    393275 |  269505   806224 |  108700   35850  1504352    42.0 | 14.243 % |
c |    393500 |  269505   806224 |  119570   36075  1505363    41.7 | 14.243 % |
c |    393837 |  269505   806224 |  131527   36412  1507151    41.4 | 14.243 % |
c |    394343 |  269490   806189 |  144680   36916  1510412    40.9 | 14.251 % |
c |    395102 |  269483   806173 |  159148   37674  1515155    40.2 | 14.253 % |
c |    396241 |  269471   806146 |  175063   38811  1525995    39.3 | 14.260 % |
c |    397949 |  269457   806113 |  192569   40517  1544901    38.1 | 14.267 % |
c |    400511 |  269457   806113 |  211826   43079  1581595    36.7 | 14.267 % |
c |    404355 |  269430   806050 |  233008   46920  1618823    34.5 | 14.277 % |
c |    410121 |  269418   806022 |  256309   52684  1673714    31.8 | 14.284 % |
c |    418770 |  269408   805999 |  281940   61331  1763107    28.7 | 14.288 % |
c |    431744 |  269370   805912 |  310134   74295  2159793    29.1 | 14.303 % |
c |    451205 |  269257   805641 |  341148   93736  2463278    26.3 | 14.351 % |
c |    480397 |  269168   805413 |  375263  122912  3241597    26.4 | 14.383 % |
c ==============================================================================
c [1mFound solution: 18978750[0m
c ---[   0]---> Adder-cost: 0   maxlim: 52282016   bits: 27/26
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    498274 |  269142   805494 |   89714  140783  4709466    33.5 | 14.383 % |
c |    498374 |  269142   805494 |   98685   32221  1279969    39.7 | 14.416 % |
c |    498524 |  269082   805355 |  108553   32366  1280561    39.6 | 14.442 % |
c |    498749 |  269076   805341 |  119409   32588  1281491    39.3 | 14.446 % |
c |    499086 |  269070   805327 |  131350   32924  1283028    39.0 | 14.449 % |
c |    499592 |  269070   805327 |  144485   33430  1285739    38.5 | 14.449 % |
c |    500352 |  269057   805297 |  158933   34188  1289714    37.7 | 14.455 % |
c |    501491 |  269057   805297 |  174827   35327  1295660    36.7 | 14.455 % |
c |    503199 |  269057   805297 |  192309   37035  1304293    35.2 | 14.455 % |
c |    505761 |  268980   805116 |  211540   39582  1317439    33.3 | 14.487 % |
c |    509605 |  268894   804919 |  232695   43409  1338383    30.8 | 14.525 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 10993 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.98 0.94 2/54 10989
Raw data (stat): 10989 (runsolver) R 10988 25568 25567 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 783594650 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.99984 s]
Raw data (loadavg): 0.93 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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+19.9996 s]
Raw data (loadavg): 0.94 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.0004 s]
Raw data (loadavg): 0.95 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.0002 s]
Raw data (loadavg): 0.96 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.0001 s]
Raw data (loadavg): 0.96 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.0125 s]
Raw data (loadavg): 0.97 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.0257 s]
Raw data (loadavg): 0.97 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.0255 s]
Raw data (loadavg): 0.98 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.0253 s]
Raw data (loadavg): 0.98 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.025 s]
Raw data (loadavg): 0.98 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.025 s]
Raw data (loadavg): 0.98 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.025 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.026 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.025 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.026 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.026 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.026 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.025 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.025 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.025 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.025 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.025 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.025 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.024 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.024 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.024 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.024 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.024 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.024 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.024 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.024 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.024 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.024 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.024 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.024 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.024 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.022 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.022 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.024 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.024 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.024 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.024 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.025 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.024 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.024 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.026 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.026 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.026 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.026 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.026 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.026 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.027 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.027 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.027 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.027 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.028 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.028 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.029 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.029 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.031 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.031 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.031 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.031 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.037 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.036 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.037 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.036 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.037 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.037 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.038 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.038 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.039 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.039 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.039 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.041 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.58 s]
Raw data (loadavg): 0.99 0.98 0.94 1/53 10993
Raw data (stat): 10989 (minisat+_script) S 10988 25568 25567 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 783594650 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.58
CPU time (s): 1229.88
CPU user time (s): 1228.92
CPU system time (s): 0.964853
CPU usage (%): 100.025
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####