PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-rout.opb
MD5SUM	76f802a1f3708b934101fc21122cc5bf
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	31
Biggest coefficient in the objective function	1073741824
Number of bits for the biggest coefficient in the objective function	31
Sum of the numbers in the objective function	2147483647
Number of bits of the sum of numbers in the objective function	31
Biggest number in a constraint	26904326400
Number of bits of the biggest number in a constraint	35
Biggest sum of numbers in a constraint	81230087655
Number of bits of the biggest sum of numbers	37
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.250961
Number of variables	7561
Total number of constraints	606
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	314
Number of constraints which are nor clauses,nor cardinality constraints	292
Minimum length of a constraint	1
Maximum length of a constraint	917
Trace number 30851

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-05-25 20:10:47 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22251 boxname=wulflinc8 idbench=1067 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  76f802a1f3708b934101fc21122cc5bf  /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-20-10-rout.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-20-10-rout.opb
IDLAUNCH: 22251
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        361012 kB
Buffers:         37508 kB
Cached:         609648 kB
SwapCached:          0 kB
Active:          24000 kB
Inactive:       630072 kB
HighTotal:      131008 kB
HighFree:        20720 kB
LowTotal:       903652 kB
LowFree:        340292 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           7068 kB
Slab:            13924 kB
Committed_AS:    63736 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 20:31:17 (client local time) WITH STATUS 152 IN 1229.86 SECONDS
stats: 22251 7 1229.86 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 337 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###############################
c   -- Clauses(.)/Splits(s): ...............
c ---[ 320]---> Adder-cost: 3908   maxlim: 27410865895   bits: 36/35
c ---[ 319]---> Adder-cost: 604   maxlim: 25598   bits: 15/15
c ---[ 318]---> Adder-cost: 604   maxlim: 25598   bits: 15/15
c ---[ 317]---> Adder-cost: 604   maxlim: 25598   bits: 15/15
c ---[ 316]---> Adder-cost: 604   maxlim: 25598   bits: 15/15
c ---[ 315]---> Adder-cost: 604   maxlim: 25598   bits: 15/15
c ---[ 314]---> BDD-cost:   37
c ---[ 313]---> BDD-cost:   37
c ---[ 312]---> BDD-cost:   84
c ---[ 311]---> BDD-cost:   37
c ---[ 310]---> BDD-cost:   37
c ---[ 309]---> BDD-cost:   37
c ---[ 308]---> BDD-cost:   37
c ---[ 307]---> BDD-cost:   37
c ---[ 306]---> BDD-cost:   37
c ---[ 305]---> BDD-cost:   37
c ---[ 304]---> BDD-cost:   37
c ---[ 303]---> BDD-cost:   37
c ---[ 302]---> BDD-cost:   37
c ---[ 301]---> BDD-cost:   37
c ---[ 300]---> BDD-cost:   37
c ---[ 298]---> Sorter-cost:  441     Base: 2
c ---[ 296]---> Sorter-cost:  441     Base: 2
c ---[ 294]---> Sorter-cost:  441     Base: 2
c ---[ 292]---> Sorter-cost:  441     Base: 2
c ---[ 290]---> Sorter-cost:  441     Base: 2
c ---[ 288]---> Sorter-cost:  347     Base: 2
c ---[ 286]---> Sorter-cost:  347     Base: 2
c ---[ 284]---> Sorter-cost:  347     Base: 2
c ---[ 282]---> Sorter-cost:  347     Base: 2
c ---[ 280]---> Sorter-cost:  347     Base: 2
c ---[ 278]---> Sorter-cost:  515     Base: 2
c ---[ 276]---> Sorter-cost:  515     Base: 2
c ---[ 274]---> Sorter-cost:  515     Base: 2
c ---[ 272]---> Sorter-cost:  515     Base: 2
c ---[ 270]---> Sorter-cost:  515     Base: 2
c ---[ 268]---> Adder-cost: 698   maxlim: 172017   bits: 19/18
c ---[ 266]---> Adder-cost: 698   maxlim: 172017   bits: 19/18
c ---[ 264]---> Adder-cost: 698   maxlim: 172017   bits: 19/18
c ---[ 262]---> Adder-cost: 698   maxlim: 172017   bits: 19/18
c ---[ 260]---> Adder-cost: 698   maxlim: 172017   bits: 19/18
c ---[ 258]---> Adder-cost: 586   maxlim: 73719   bits: 18/17
c ---[ 256]---> Adder-cost: 586   maxlim: 73719   bits: 18/17
c ---[ 254]---> Adder-cost: 586   maxlim: 73719   bits: 18/17
c ---[ 252]---> Adder-cost: 586   maxlim: 73719   bits: 18/17
c ---[ 250]---> Adder-cost: 586   maxlim: 73719   bits: 18/17
c ---[ 248]---> Adder-cost: 776   maxlim: 172011   bits: 19/18
c ---[ 246]---> Adder-cost: 776   maxlim: 172011   bits: 19/18
c ---[ 244]---> Adder-cost: 776   maxlim: 172011   bits: 19/18
c ---[ 242]---> Adder-cost: 776   maxlim: 172011   bits: 19/18
c ---[ 240]---> Adder-cost: 776   maxlim: 172011   bits: 19/18
c ---[ 239]---> BDD-cost:   16
c ---[ 238]---> BDD-cost:   16
c ---[ 237]---> BDD-cost:   16
c ---[ 236]---> BDD-cost:   16
c ---[ 235]---> BDD-cost:   16
c ---[ 234]---> BDD-cost:   16
c ---[ 233]---> BDD-cost:   16
c ---[ 232]---> BDD-cost:   16
c ---[ 231]---> BDD-cost:   16
c ---[ 230]---> BDD-cost:   16
c ---[ 229]---> BDD-cost:   16
c ---[ 228]---> BDD-cost:   16
c ---[ 227]---> BDD-cost:   16
c ---[ 226]---> BDD-cost:   16
c ---[ 225]---> BDD-cost:   16
c ---[ 224]---> BDD-cost:   16
c ---[ 223]---> BDD-cost:   16
c ---[ 222]---> BDD-cost:   16
c ---[ 221]---> BDD-cost:   16
c ---[ 220]---> BDD-cost:   16
c ---[ 219]---> BDD-cost:   16
c ---[ 218]---> BDD-cost:   16
c ---[ 217]---> BDD-cost:   16
c ---[ 216]---> BDD-cost:   16
c ---[ 215]---> BDD-cost:   16
c ---[ 214]---> BDD-cost:   16
c ---[ 213]---> BDD-cost:   16
c ---[ 212]---> BDD-cost:   16
c ---[ 211]---> BDD-cost:   16
c ---[ 210]---> BDD-cost:   16
c ---[ 209]---> BDD-cost:   16
c ---[ 208]---> BDD-cost:   16
c ---[ 207]---> BDD-cost:   16
c ---[ 206]---> BDD-cost:   16
c ---[ 205]---> BDD-cost:   16
c ---[ 204]---> BDD-cost:   16
c ---[ 203]---> BDD-cost:   16
c ---[ 202]---> BDD-cost:   16
c ---[ 201]---> BDD-cost:   16
c ---[ 200]---> BDD-cost:   16
c ---[ 199]---> BDD-cost:   16
c ---[ 198]---> BDD-cost:   16
c ---[ 197]---> BDD-cost:   16
c ---[ 196]---> BDD-cost:   16
c ---[ 195]---> BDD-cost:   16
c ---[ 194]---> BDD-cost:   16
c ---[ 193]---> BDD-cost:   16
c ---[ 192]---> BDD-cost:   16
c ---[ 191]---> BDD-cost:   16
c ---[ 190]---> BDD-cost:   16
c ---[ 189]---> BDD-cost:   28
c ---[ 188]---> BDD-cost:   28
c ---[ 187]---> BDD-cost:   28
c ---[ 186]---> BDD-cost:   28
c ---[ 185]---> BDD-cost:   28
c ---[ 184]---> BDD-cost:   28
c ---[ 183]---> BDD-cost:   28
c ---[ 182]---> BDD-cost:   28
c ---[ 181]---> BDD-cost:   28
c ---[ 180]---> BDD-cost:   28
c ---[ 179]---> BDD-cost:   16
c ---[ 178]---> BDD-cost:   16
c ---[ 177]---> BDD-cost:   16
c ---[ 176]---> BDD-cost:   16
c ---[ 175]---> BDD-cost:   16
c ---[ 174]---> BDD-cost:   16
c ---[ 173]---> BDD-cost:   16
c ---[ 172]---> BDD-cost:   16
c ---[ 171]---> BDD-cost:   16
c ---[ 170]---> BDD-cost:   16
c ---[ 169]---> BDD-cost:   16
c ---[ 168]---> BDD-cost:   16
c ---[ 167]---> BDD-cost:   16
c ---[ 166]---> BDD-cost:   16
c ---[ 165]---> BDD-cost:   16
c ---[ 164]---> BDD-cost:   16
c ---[ 163]---> BDD-cost:   16
c ---[ 162]---> BDD-cost:   16
c ---[ 161]---> BDD-cost:   16
c ---[ 160]---> BDD-cost:   16
c ---[ 159]---> BDD-cost:   16
c ---[ 158]---> BDD-cost:   16
c ---[ 157]---> BDD-cost:   16
c ---[ 156]---> BDD-cost:   16
c ---[ 155]---> BDD-cost:   16
c ---[ 154]---> BDD-cost:   16
c ---[ 153]---> BDD-cost:   16
c ---[ 152]---> BDD-cost:   16
c ---[ 151]---> BDD-cost:   16
c ---[ 150]---> BDD-cost:   16
c ---[ 149]---> BDD-cost:   16
c ---[ 148]---> BDD-cost:   16
c ---[ 147]---> BDD-cost:   16
c ---[ 146]---> BDD-cost:   16
c ---[ 145]---> BDD-cost:   16
c ---[ 144]---> BDD-cost:   16
c ---[ 143]---> BDD-cost:   16
c ---[ 142]---> BDD-cost:   16
c ---[ 141]---> BDD-cost:   16
c ---[ 140]---> BDD-cost:   16
c ---[ 139]---> BDD-cost:   16
c ---[ 138]---> BDD-cost:   16
c ---[ 137]---> BDD-cost:   16
c ---[ 136]---> BDD-cost:   16
c ---[ 135]---> BDD-cost:   16
c ---[ 134]---> BDD-cost:   16
c ---[ 133]---> BDD-cost:   16
c ---[ 132]---> BDD-cost:   16
c ---[ 131]---> BDD-cost:   16
c ---[ 130]---> BDD-cost:   16
c ---[ 129]---> BDD-cost:   16
c ---[ 128]---> BDD-cost:   16
c ---[ 127]---> BDD-cost:   16
c ---[ 126]---> BDD-cost:   16
c ---[ 125]---> BDD-cost:   16
c ---[ 124]---> BDD-cost:   16
c ---[ 123]---> BDD-cost:   16
c ---[ 122]---> BDD-cost:   16
c ---[ 121]---> BDD-cost:   16
c ---[ 120]---> BDD-cost:   16
c ---[ 119]---> BDD-cost:   16
c ---[ 118]---> BDD-cost:   16
c ---[ 117]---> BDD-cost:   16
c ---[ 116]---> BDD-cost:   16
c ---[ 115]---> BDD-cost:   16
c ---[ 114]---> BDD-cost:   16
c ---[ 113]---> BDD-cost:   16
c ---[ 112]---> BDD-cost:   16
c ---[ 111]---> BDD-cost:   16
c ---[ 110]---> BDD-cost:   16
c ---[ 109]---> BDD-cost:   16
c ---[ 108]---> BDD-cost:   16
c ---[ 107]---> BDD-cost:   16
c ---[ 106]---> BDD-cost:   16
c ---[ 105]---> BDD-cost:   16
c ---[ 104]---> BDD-cost:   16
c ---[ 103]---> BDD-cost:   16
c ---[ 102]---> BDD-cost:   16
c ---[ 101]---> BDD-cost:   16
c ---[ 100]---> BDD-cost:   16
c ---[  99]---> BDD-cost:   16
c ---[  98]---> BDD-cost:   16
c ---[  97]---> BDD-cost:   16
c ---[  96]---> BDD-cost:   16
c ---[  95]---> BDD-cost:   16
c ---[  94]---> BDD-cost:   16
c ---[  93]---> BDD-cost:   16
c ---[  92]---> BDD-cost:   16
c ---[  91]---> BDD-cost:   16
c ---[  90]---> BDD-cost:   16
c ---[  89]---> BDD-cost:   16
c ---[  88]---> BDD-cost:   16
c ---[  87]---> BDD-cost:   16
c ---[  86]---> BDD-cost:   16
c ---[  85]---> BDD-cost:   16
c ---[  84]---> BDD-cost:   16
c ---[  83]---> BDD-cost:   16
c ---[  82]---> BDD-cost:   16
c ---[  81]---> BDD-cost:   16
c ---[  80]---> BDD-cost:   16
c ---[  79]---> BDD-cost:   16
c ---[  78]---> BDD-cost:   16
c ---[  77]---> BDD-cost:   16
c ---[  76]---> BDD-cost:   16
c ---[  75]---> BDD-cost:   16
c ---[  74]---> BDD-cost:   16
c ---[  73]---> BDD-cost:   16
c ---[  72]---> BDD-cost:   16
c ---[  71]---> BDD-cost:   16
c ---[  70]---> BDD-cost:   16
c ---[  69]---> BDD-cost:   16
c ---[  68]---> BDD-cost:   16
c ---[  67]---> BDD-cost:   16
c ---[  66]---> BDD-cost:   16
c ---[  65]---> BDD-cost:   16
c ---[  64]---> BDD-cost:   16
c ---[  63]---> BDD-cost:   16
c ---[  62]---> BDD-cost:   16
c ---[  61]---> BDD-cost:   16
c ---[  60]---> BDD-cost:   16
c ---[  59]---> BDD-cost:   16
c ---[  58]---> BDD-cost:   16
c ---[  57]---> BDD-cost:   16
c ---[  56]---> BDD-cost:   16
c ---[  55]---> BDD-cost:   16
c ---[  54]---> BDD-cost:   16
c ---[  53]---> BDD-cost:   16
c ---[  52]---> BDD-cost:   16
c ---[  51]---> BDD-cost:   16
c ---[  50]---> BDD-cost:   16
c ---[  49]---> BDD-cost:   16
c ---[  48]---> BDD-cost:   16
c ---[  47]---> BDD-cost:   16
c ---[  46]---> BDD-cost:   16
c ---[  45]---> BDD-cost:   16
c ---[  44]---> BDD-cost:   16
c ---[  43]---> BDD-cost:   16
c ---[  42]---> BDD-cost:   16
c ---[  41]---> BDD-cost:   16
c ---[  40]---> BDD-cost:   16
c ---[  39]---> BDD-cost:   16
c ---[  38]---> BDD-cost:   16
c ---[  37]---> BDD-cost:   16
c ---[  36]---> BDD-cost:   16
c ---[  35]---> BDD-cost:   16
c ---[  34]---> BDD-cost:   16
c ---[  33]---> BDD-cost:   16
c ---[  32]---> BDD-cost:   16
c ---[  31]---> BDD-cost:   16
c ---[  30]---> BDD-cost:   16
c ---[  29]---> BDD-cost:   16
c ---[  28]---> BDD-cost:   16
c ---[  27]---> BDD-cost:   16
c ---[  26]---> BDD-cost:   16
c ---[  25]---> BDD-cost:   16
c ---[  24]---> BDD-cost:   16
c ---[  23]---> BDD-cost:   16
c ---[  22]---> BDD-cost:   16
c ---[  21]---> BDD-cost:   16
c ---[  20]---> BDD-cost:   16
c ---[  19]---> BDD-cost:   16
c ---[  18]---> BDD-cost:   16
c ---[  17]---> BDD-cost:   16
c ---[  16]---> BDD-cost:   16
c ---[  15]---> BDD-cost:   16
c ---[  14]---> BDD-cost:   16
c ---[  13]---> BDD-cost:   16
c ---[  12]---> BDD-cost:   16
c ---[  11]---> BDD-cost:   16
c ---[  10]---> BDD-cost:   16
c ---[   9]---> BDD-cost:   16
c ---[   8]---> BDD-cost:   16
c ---[   7]---> BDD-cost:   16
c ---[   6]---> BDD-cost:   16
c ---[   5]---> BDD-cost:   16
c ---[   4]---> BDD-cost:   16
c ---[   3]---> BDD-cost:   16
c ---[   2]---> BDD-cost:   16
c ---[   1]---> BDD-cost:   16
c ---[   0]---> BDD-cost:   16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  140564   474144 |   46854       0        0     nan |  0.000 % |
c |       100 |  140564   474144 |   51539     100     7325    73.2 | 16.154 % |
c |       252 |  140491   473981 |   56693     250    15197    60.8 | 16.210 % |
c |       477 |  140431   473810 |   62362     470    23333    49.6 | 16.256 % |
c |       815 |  140406   473729 |   68598     804    27142    33.8 | 16.271 % |
c |      1322 |  140298   473479 |   75458    1307    49686    38.0 | 16.352 % |
c |      2082 |  139843   472454 |   83004    2045    86075    42.1 | 16.749 % |
c |      3221 |  139822   472386 |   91305    3181   150904    47.4 | 16.765 % |
c |      4929 |  139671   472025 |  100435    4881   310154    63.5 | 16.885 % |
c |      7492 |  139117   470686 |  110479    7402   424240    57.3 | 17.366 % |
c |     11337 |  139066   470561 |  121527   11245   733188    65.2 | 17.409 % |
c |     17107 |  138665   469475 |  133679   16933   966991    57.1 | 17.712 % |
c ==============================================================================
c [1mFound solution: 1075451904[0m
c ---[   0]---> BDD-cost:   19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19989 |  138507   469082 |   46169   19784  1125553    56.9 | 17.712 % |
c |     20091 |  138457   468967 |   50785   19880  1126139    56.6 | 17.917 % |
c |     20241 |  138366   468751 |   55864   20022  1127769    56.3 | 18.001 % |
c |     20466 |  138083   468085 |   61450   20202  1134449    56.2 | 18.260 % |
c |     20804 |  137906   467666 |   67596   20525  1162730    56.6 | 18.432 % |
c |     21310 |  137881   467585 |   74355   21028  1184160    56.3 | 18.432 % |
c |     22070 |  137881   467585 |   81791   21788  1224002    56.2 | 18.432 % |
c |     23209 |  137839   467483 |   89970   22922  1290475    56.3 | 18.466 % |
c |     24918 |  137401   466479 |   98967   24595  1479624    60.2 | 18.855 % |
c |     27480 |  137262   466163 |  108864   27148  1673578    61.6 | 18.984 % |
c |     31324 |  137185   465950 |  119750   30984  1770364    57.1 | 19.040 % |
c |     37090 |  136955   465223 |  131725   36721  2071982    56.4 | 19.135 % |
c |     45739 |  136419   463920 |  144898   45230  2779461    61.5 | 19.610 % |
c |     58713 |  135817   462324 |  159387   58130  3708684    63.8 | 20.073 % |
c |     78174 |  135505   461432 |  175326   77546  5106182    65.8 | 20.276 % |
c |    107366 |  135091   460268 |  192859  106681  7652969    71.7 | 20.557 % |
c ==============================================================================
c [1mFound solution: 1075444480[0m
c ---[   0]---> BDD-cost:   22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    138563 |  134135   457744 |   44711  136657 12024674    88.0 | 20.557 % |
c |    138663 |  134135   457744 |   49182   23392  2192426    93.7 | 21.320 % |
c |    138813 |  134135   457744 |   54100   23542  2202287    93.5 | 21.320 % |
c |    139041 |  134092   457618 |   59510   23766  2206627    92.8 | 21.345 % |
c |    139378 |  134092   457618 |   65461   24103  2216425    92.0 | 21.345 % |
c |    139884 |  134092   457618 |   72007   24609  2255337    91.6 | 21.345 % |
c |    140643 |  134035   457417 |   79208   25362  2339416    92.2 | 21.357 % |
c |    141783 |  133858   456937 |   87129   26477  2392692    90.4 | 21.502 % |
c |    143492 |  133858   456937 |   95841   28186  2469508    87.6 | 21.502 % |
c |    146054 |  133858   456937 |  105426   30748  2918734    94.9 | 21.502 % |
c |    149898 |  133778   456667 |  115968   34570  3083904    89.2 | 21.527 % |
c ==============================================================================
c [1mFound solution: 1075406592[0m
c ---[   0]---> BDD-cost:   21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    154268 |  133186   454579 |   44395   38821  3611291    93.0 | 21.527 % |
c |    154370 |  133153   454464 |   48834   38918  3613379    92.8 | 21.746 % |
c |    154520 |  133153   454464 |   53717   39068  3617747    92.6 | 21.746 % |
c |    154745 |  133130   454385 |   59089   39282  3623367    92.2 | 21.758 % |
c |    155082 |  133130   454385 |   64998   39619  3636792    91.8 | 21.758 % |
c |    155588 |  133130   454385 |   71498   40125  3706174    92.4 | 21.758 % |
c |    156348 |  133130   454385 |   78648   40885  3805084    93.1 | 21.758 % |
c |    157489 |  132980   454025 |   86513   42002  3879337    92.4 | 21.924 % |
c |    159197 |  132980   454025 |   95164   43710  3909316    89.4 | 21.924 % |
c |    161759 |  132980   454025 |  104681   46272  4165307    90.0 | 21.924 % |
c |    165605 |  132880   453682 |  115149   50102  4493828    89.7 | 21.955 % |
c |    171371 |  132609   452870 |  126664   55824  5196562    93.1 | 22.122 % |
c |    180026 |  132453   452324 |  139330   64434  6336350    98.3 | 22.174 % |
c |    193000 |  132027   450886 |  153263   77350  8405914   108.7 | 22.325 % |
c |    212461 |  131956   450658 |  168589   96802 10957901   113.2 | 22.359 % |
c ==============================================================================
c [1mFound solution: 1075404544[0m
c ---[   0]---> BDD-cost:   20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    218266 |  131921   450570 |   43973  102604 11561173   112.7 | 22.359 % |
c |    218367 |  131921   450570 |   48370   22654  2004502    88.5 | 22.420 % |
c |    218517 |  131921   450570 |   53207   22804  2007922    88.1 | 22.420 % |
c |    218743 |  131921   450570 |   58528   23030  2012369    87.4 | 22.420 % |
c |    219080 |  131870   450436 |   64380   23357  2021560    86.6 | 22.457 % |
c |    219589 |  131777   450117 |   70818   23856  2044071    85.7 | 22.491 % |
c |    220350 |  131777   450117 |   77900   24617  2170588    88.2 | 22.491 % |
c |    221489 |  131694   449828 |   85690   25741  2283127    88.7 | 22.519 % |
c |    223198 |  131682   449786 |   94260   27446  2363218    86.1 | 22.522 % |
c |    225760 |  131682   449786 |  103686   30008  2602449    86.7 | 22.522 % |
c |    229605 |  131543   449301 |  114054   33794  2870934    85.0 | 22.590 % |
c |    235371 |  131543   449301 |  125460   39560  3346729    84.6 | 22.590 % |
c |    244020 |  131346   448753 |  138006   48174  3766775    78.2 | 22.738 % |
c |    256996 |  131265   448543 |  151806   61130  4876538    79.8 | 22.802 % |
c ==============================================================================
c [1mFound solution: 1075335424[0m
c ---[   0]---> BDD-cost:   22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    258890 |  131290   448598 |   43763   63024  5199528    82.5 | 22.802 % |
c |    258990 |  131281   448567 |   48139   21856  1396698    63.9 | 22.803 % |
c |    259141 |  131281   448567 |   52953   22007  1402113    63.7 | 22.803 % |
c |    259366 |  131281   448567 |   58248   22232  1454970    65.4 | 22.803 % |
c |    259704 |  131219   448393 |   64073   22567  1465264    64.9 | 22.849 % |
c |    260210 |  131219   448393 |   70480   23073  1490413    64.6 | 22.849 % |
c |    260969 |  131219   448393 |   77528   23832  1567365    65.8 | 22.849 % |
c |    262109 |  131219   448393 |   85281   24972  1730186    69.3 | 22.849 % |
c |    263817 |  131198   448320 |   93809   26677  1862493    69.8 | 22.855 % |
c |    266379 |  131198   448320 |  103190   29239  2196681    75.1 | 22.855 % |
c |    270223 |  131134   448108 |  113509   33074  2688965    81.3 | 22.883 % |
c |    275994 |  131107   448015 |  124860   38842  3349565    86.2 | 22.892 % |
c |    284643 |  131063   447863 |  137347   47482  5096222   107.3 | 22.911 % |
c |    297617 |  131055   447844 |  151081   60455  6644882   109.9 | 22.920 % |
c |    317078 |  130891   447394 |  166189   79908  9013487   112.8 | 23.074 % |
c ==============================================================================
c [1mFound solution: 1075298560[0m
c ---[   0]---> BDD-cost:   19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    318435 |  130798   447082 |   43599   81251  9201853   113.3 | 23.074 % |
c |    318535 |  130748   446968 |   47958   23400  1864648    79.7 | 23.168 % |
c |    318687 |  130748   446968 |   52754   23552  1873673    79.6 | 23.168 % |
c |    318912 |  130748   446968 |   58030   23777  1881204    79.1 | 23.168 % |
c |    319253 |  130748   446968 |   63833   24118  1897097    78.7 | 23.168 % |
c |    319759 |  130748   446968 |   70216   24624  1919367    77.9 | 23.168 % |
c |    320521 |  130729   446907 |   77238   25385  1939170    76.4 | 23.178 % |
c |    321660 |  130729   446907 |   84962   26524  1987179    74.9 | 23.178 % |
c |    323369 |  130418   445937 |   93458   28198  2170876    77.0 | 23.365 % |
c |    325931 |  130418   445937 |  102804   30760  2421508    78.7 | 23.365 % |
c ==============================================================================
c [1mFound solution: 1075128832[0m
c ---[   0]---> BDD-cost:   21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    329376 |  130386   445792 |   43462   34197  2671836    78.1 | 23.365 % |
c |    329476 |  130386   445792 |   47808   34297  2678626    78.1 | 23.381 % |
c |    329626 |  130386   445792 |   52589   34447  2684743    77.9 | 23.381 % |
c |    329854 |  130386   445792 |   57847   34675  2693204    77.7 | 23.381 % |
c |    330191 |  130326   445592 |   63632   35004  2772933    79.2 | 23.415 % |
c |    330701 |  130309   445533 |   69995   35511  2819239    79.4 | 23.425 % |
c |    331460 |  130260   445362 |   76995   36264  2858463    78.8 | 23.446 % |
c |    332602 |  130260   445362 |   84695   37406  3011492    80.5 | 23.446 % |
c |    334312 |  130260   445362 |   93164   39116  3107285    79.4 | 23.446 % |
c |    336876 |  130235   445294 |  102481   41676  3558348    85.4 | 23.468 % |
c |    340721 |  130235   445294 |  112729   45521  4152206    91.2 | 23.468 % |
c |    346487 |  130206   445193 |  124002   51282  4916005    95.9 | 23.480 % |
c |    355137 |  130200   445173 |  136402   59930  6002932   100.2 | 23.483 % |
c |    368111 |  129993   444491 |  150042   72868  8056211   110.6 | 23.578 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 22291 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 22287
Raw data (stat): 22287 (runsolver) R 22286 3132 3131 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 769867643 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.93 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0012 s]
Raw data (loadavg): 0.94 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0017 s]
Raw data (loadavg): 0.95 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0018 s]
Raw data (loadavg): 0.96 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0026 s]
Raw data (loadavg): 0.96 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.003 s]
Raw data (loadavg): 0.97 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0031 s]
Raw data (loadavg): 0.97 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0039 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0034 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 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 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.73 s]
Raw data (loadavg): 0.99 0.97 0.92 1/53 22291
Raw data (stat): 22287 (minisat+_script) S 22286 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769867643 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.73
CPU time (s): 1229.86
CPU user time (s): 1229.32
CPU system time (s): 0.547916
CPU usage (%): 100.01
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####